Theory NumeralType

header {* Numeral Syntax for Types *}

theory NumeralType imports Main begin

subsection {* Type constructors *}

text "Define types without any constants"
text "(typedecl would work just as well)"

typedef pls = "UNIV::unit set" ..
typedef min = "UNIV::unit set" ..
typedef 'a bit0 = "UNIV::unit set" ..
typedef 'a bit1 = "UNIV::unit set" ..

subsection {* Syntax *}

syntax
  "_NumeralType" :: "num_const => type"  ("_")
  "_NumeralType0" :: type ("0")
  "_NumeralType1" :: type ("1")

translations
  "_NumeralType1" => (type) "pls bit1"
  "_NumeralType0" == (type) "pls"
  (type) "-1"     <= (type) "min"

parse_translation {*
let

val pls_const = Syntax.const "NumeralType.pls";
val min_const = Syntax.const "NumeralType.min";
val B0_const = Syntax.const "NumeralType.bit0";
val B1_const = Syntax.const "NumeralType.bit1";

fun mk_bintype n =
  let
    fun mk_bit n = if n = 0 then B0_const else B1_const;
    fun bin_of n =
      if n = 0 then pls_const
      else if n = ~1 then min_const
      else
        let val (q, r) = IntInf.divMod (n, 2);
        in mk_bit r $ bin_of q end;
  in bin_of n end;

fun numeral_tr (*"_NumeralType"*) [Const (str, _)] =
      mk_bintype (valOf (IntInf.fromString str))
  | numeral_tr (*"_NumeralType"*) ts = raise TERM ("numeral_tr", ts);

in [("_NumeralType", numeral_tr)] end;
*}

print_translation {*
let
fun prefix_len _ [] = 0
  | prefix_len pred (x :: xs) =
      if pred x then 1 + prefix_len pred xs else 0;

fun int_of [] = 0
  | int_of (b :: bs) = IntInf.fromInt b + (2 * int_of bs);

fun bin_of (Const ("pls", _)) = []
  | bin_of (Const ("min", _)) = [~1]
  | bin_of (Const ("bit0", _) $ bs) = 0 :: bin_of bs
  | bin_of (Const ("bit1", _) $ bs) = 1 :: bin_of bs
  | bin_of t = raise TERM("bin_of", [t]);

fun bit_tr' b [t] =
  let
    val rev_digs = b :: bin_of t handle TERM _ => raise Match
    val (sign, zs) =
      (case rev rev_digs of
        ~1 :: bs => ("-", prefix_len (equal 1) bs)
      | bs => ("", prefix_len (equal 0) bs));
    val i = int_of rev_digs;
    val num = IntInf.toString (IntInf.abs i);
    val str = sign ^ implode (replicate zs "0") ^ num;
  in
    Syntax.const "_NumeralType" $ Syntax.free str
  end
  | bit_tr' b _ = raise Match;

in [("bit0", bit_tr' 0), ("bit1", bit_tr' 1)] end;
*}

subsection {* Types with @{typ int} values *}

axclass numeral < type

consts bin_of_type :: "'a::numeral itself => int"

instance pls :: numeral ..
instance min :: numeral ..
instance bit0 :: (numeral) numeral ..
instance bit1 :: (numeral) numeral ..

defs (overloaded)
  bin_of_type_pls_def:
   "bin_of_type (t::pls itself) ≡ Numeral.Pls"

  bin_of_type_min_def:
   "bin_of_type (t::min itself) ≡ Numeral.Min"

  bin_of_type_bit0_def:
   "bin_of_type (t::'a::numeral bit0 itself) ≡
    bin_of_type TYPE('a) BIT bit.B0"

  bin_of_type_bit1_def:
   "bin_of_type (t::'a::numeral bit1 itself) ≡
    bin_of_type TYPE('a) BIT bit.B1"

lemmas bin_of_type_defs [simp] =
  bin_of_type_pls_def
  bin_of_type_min_def
  bin_of_type_bit0_def
  bin_of_type_bit1_def

definition
  int_of_type :: "'a::numeral itself => int" where
  "int_of_type t = number_of (bin_of_type t)"

axclass numeral0 < numeral
  zero_le_int_of_type: "0 ≤ int_of_type TYPE('a::numeral)"

axclass numeral1 < numeral
  one_le_int_of_type: "1 ≤ int_of_type TYPE('a::numeral)"

axclass numeral2 < numeral
  two_le_int_of_type: "2 ≤ int_of_type TYPE('a::numeral)"

lemma zero_less_int_of_type: "0 < int_of_type TYPE('a::numeral1)"
apply (rule int_one_le_iff_zero_less [THEN iffD1])
apply (rule one_le_int_of_type)
done

lemma one_less_int_of_type: "1 < int_of_type TYPE('a::numeral2)"
by (cut_tac 'a = 'a in two_le_int_of_type, simp)

instance numeral1 < numeral0
proof
  have "0 < int_of_type TYPE('a)" by (rule zero_less_int_of_type)
  thus "0 ≤ int_of_type TYPE('a)" by (rule order_less_imp_le)
qed

instance numeral2 < numeral1
proof
  have "1 < int_of_type TYPE('a)" by (rule one_less_int_of_type)
  thus "1 ≤ int_of_type TYPE('a)" by (rule order_less_imp_le)
qed

instance pls :: numeral0
by intro_classes (simp add: int_of_type_def)

instance bit0 :: (numeral0) numeral0
proof
  have "0 ≤ int_of_type TYPE('a)" by (rule zero_le_int_of_type)
  thus "0 ≤ int_of_type TYPE('a bit0)" by (simp add: int_of_type_def)
qed

instance bit0 :: (numeral1) numeral2
proof
  have "1 ≤ int_of_type TYPE('a)" by (rule one_le_int_of_type)
  thus "2 ≤ int_of_type TYPE('a bit0)" by (simp add: int_of_type_def)
qed

instance bit1 :: (numeral0) numeral1
proof
  have "0 ≤ int_of_type TYPE('a)" by (rule zero_le_int_of_type)
  thus "1 ≤ int_of_type TYPE('a bit1)" by (simp add: int_of_type_def)
qed

instance bit1 :: (numeral1) numeral2
proof
  have "1 ≤ int_of_type TYPE('a)" by (rule one_le_int_of_type)
  thus "2 ≤ int_of_type TYPE('a bit1)" by (simp add: int_of_type_def)
qed

subsection {* Types with @{typ nat} values *}

definition
  nat_of_type :: "'a::numeral0 itself => nat" where
  "nat_of_type t = number_of (bin_of_type t)"

lemma nat_of_type_eq: "nat_of_type t = nat (int_of_type t)"
by (simp add: nat_of_type_def int_of_type_def)

lemma zero_less_nat_of_type:
  "0 < nat_of_type TYPE('a::numeral1)"
by (simp add: nat_of_type_eq zero_less_int_of_type)

end