--- a/src/ZF/Bin.thy Sat Mar 01 14:10:15 2008 +0100
+++ b/src/ZF/Bin.thy Sat Mar 01 15:01:03 2008 +0100
@@ -18,7 +18,7 @@
theory Bin
imports Int_ZF Datatype_ZF
-uses "Tools/numeral_syntax.ML"
+uses ("Tools/numeral_syntax.ML")
begin
consts bin :: i
@@ -27,6 +27,8 @@
| Min
| Bit ("w: bin", "b: bool") (infixl "BIT" 90)
+use "Tools/numeral_syntax.ML"
+
syntax
"_Int" :: "xnum => i" ("_")
--- a/src/ZF/Inductive_ZF.thy Sat Mar 01 14:10:15 2008 +0100
+++ b/src/ZF/Inductive_ZF.thy Sat Mar 01 15:01:03 2008 +0100
@@ -42,9 +42,6 @@
setup DatatypeTactics.setup
ML_setup {*
-val iT = Ind_Syntax.iT
-and oT = FOLogic.oT;
-
structure Lfp =
struct
val oper = @{const lfp}
--- a/src/ZF/Tools/datatype_package.ML Sat Mar 01 14:10:15 2008 +0100
+++ b/src/ZF/Tools/datatype_package.ML Sat Mar 01 15:01:03 2008 +0100
@@ -92,7 +92,7 @@
(** Define the constructors **)
(*The empty tuple is 0*)
- fun mk_tuple [] = Const("0",iT)
+ fun mk_tuple [] = @{const "0"}
| mk_tuple args = foldr1 (fn (t1, t2) => Pr.pair $ t1 $ t2) args;
fun mk_inject n k u = BalancedTree.access
@@ -119,10 +119,10 @@
(*Combine split terms using case; yields the case operator for one part*)
fun call_case case_list =
- let fun call_f (free,[]) = Abs("null", iT, free)
+ let fun call_f (free,[]) = Abs("null", @{typ i}, free)
| call_f (free,args) =
CP.ap_split (foldr1 CP.mk_prod (map (#2 o dest_Free) args))
- Ind_Syntax.iT
+ @{typ i}
free
in BalancedTree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_f case_list) end;
@@ -147,7 +147,7 @@
val (_, case_lists) = foldr add_case_list (1,[]) con_ty_lists;
(*extract the types of all the variables*)
- val case_typ = List.concat (map (map (#2 o #1)) con_ty_lists) ---> (iT-->iT);
+ val case_typ = List.concat (map (map (#2 o #1)) con_ty_lists) ---> @{typ "i => i"};
val case_base_name = big_rec_base_name ^ "_case";
val case_name = full_name case_base_name;
@@ -166,7 +166,7 @@
Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
(*a recursive call for x is the application rec`x *)
- val rec_call = @{const apply} $ Free ("rec", iT);
+ val rec_call = @{const apply} $ Free ("rec", @{typ i});
(*look back down the "case args" (which have been reversed) to
determine the de Bruijn index*)
@@ -203,7 +203,7 @@
(*Add an argument position for each occurrence of a recursive set.
Strictly speaking, the recursive arguments are the LAST of the function
variable, but they all have type "i" anyway*)
- fun add_rec_args args' T = (map (fn _ => iT) args') ---> T
+ fun add_rec_args args' T = (map (fn _ => @{typ i}) args') ---> T
(*Plug in the function variable type needed for the recursor
as well as the new arguments (recursive calls)*)
@@ -219,8 +219,7 @@
val (_, recursor_lists) = foldr add_case_list (1,[]) rec_ty_lists;
(*extract the types of all the variables*)
- val recursor_typ = List.concat (map (map (#2 o #1)) rec_ty_lists)
- ---> (iT-->iT);
+ val recursor_typ = List.concat (map (map (#2 o #1)) rec_ty_lists) ---> @{typ "i => i"};
val recursor_base_name = big_rec_base_name ^ "_rec";
val recursor_name = full_name recursor_base_name;
@@ -238,7 +237,7 @@
PrimitiveDefs.mk_defpair
(recursor_tm,
@{const Univ.Vrecursor} $
- absfree ("rec", iT, list_comb (case_const, recursor_cases)));
+ absfree ("rec", @{typ i}, list_comb (case_const, recursor_cases)));
(* Build the new theory *)
@@ -406,7 +405,7 @@
fun add_datatype (sdom, srec_tms) scon_ty_lists (raw_monos, raw_type_intrs, raw_type_elims) thy =
let
val ctxt = ProofContext.init thy;
- val read_i = Sign.simple_read_term thy Ind_Syntax.iT;
+ val read_i = Sign.simple_read_term thy @{typ i};
val rec_tms = map read_i srec_tms;
val con_ty_lists = Ind_Syntax.read_constructs thy scon_ty_lists;
val dom_sum =
--- a/src/ZF/Tools/numeral_syntax.ML Sat Mar 01 14:10:15 2008 +0100
+++ b/src/ZF/Tools/numeral_syntax.ML Sat Mar 01 15:01:03 2008 +0100
@@ -20,15 +20,12 @@
(* Bits *)
-val zero = Const("0", iT);
-val succ = Const("succ", iT --> iT);
-
-fun mk_bit 0 = zero
- | mk_bit 1 = succ$zero
+fun mk_bit 0 = @{term "0"}
+ | mk_bit 1 = @{term "succ(0)"}
| mk_bit _ = sys_error "mk_bit";
-fun dest_bit (Const ("0", _)) = 0
- | dest_bit (Const ("succ", _) $ Const ("0", _)) = 1
+fun dest_bit (Const (@{const_name "0"}, _)) = 0
+ | dest_bit (Const (@{const_name succ}, _) $ Const (@{const_name "0"}, _)) = 1
| dest_bit _ = raise Match;
@@ -38,18 +35,14 @@
| prefix_len pred (x :: xs) =
if pred x then 1 + prefix_len pred xs else 0;
-val pls_const = Const ("Bin.bin.Pls", iT)
-and min_const = Const ("Bin.bin.Min", iT)
-and bit_const = Const ("Bin.bin.Bit", [iT, iT] ---> iT);
-
fun mk_bin i =
let fun bin_of_int 0 = []
| bin_of_int ~1 = [~1]
| bin_of_int n = (n mod 2) :: bin_of_int (n div 2);
- fun term_of [] = pls_const
- | term_of [~1] = min_const
- | term_of (b :: bs) = bit_const $ term_of bs $ mk_bit b;
+ fun term_of [] = @{const Pls}
+ | term_of [~1] = @{const Min}
+ | term_of (b :: bs) = @{const Bit} $ term_of bs $ mk_bit b;
in
term_of (bin_of_int i)
end;
--- a/src/ZF/int_arith.ML Sat Mar 01 14:10:15 2008 +0100
+++ b/src/ZF/int_arith.ML Sat Mar 01 15:01:03 2008 +0100
@@ -95,7 +95,7 @@
(*Utilities*)
-val integ_of_const = Const (@{const_name "Bin.integ_of"}, iT --> iT);
+val integ_of_const = Const (@{const_name "Bin.integ_of"}, @{typ "i => i"});
fun mk_numeral n = integ_of_const $ NumeralSyntax.mk_bin n;
@@ -113,9 +113,7 @@
val zero = mk_numeral 0;
val mk_plus = FOLogic.mk_binop @{const_name "zadd"};
-val iT = Ind_Syntax.iT;
-
-val zminus_const = Const (@{const_name "zminus"}, iT --> iT);
+val zminus_const = Const (@{const_name "zminus"}, @{typ "i => i"});
(*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
fun mk_sum [] = zero
@@ -126,7 +124,7 @@
fun long_mk_sum [] = zero
| long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
-val dest_plus = FOLogic.dest_bin @{const_name "zadd"} iT;
+val dest_plus = FOLogic.dest_bin @{const_name "zadd"} @{typ i};
(*decompose additions AND subtractions as a sum*)
fun dest_summing (pos, Const (@{const_name "zadd"}, _) $ t $ u, ts) =
@@ -139,7 +137,7 @@
fun dest_sum t = dest_summing (true, t, []);
val mk_diff = FOLogic.mk_binop @{const_name "zdiff"};
-val dest_diff = FOLogic.dest_bin @{const_name "zdiff"} iT;
+val dest_diff = FOLogic.dest_bin @{const_name "zdiff"} @{typ i};
val one = mk_numeral 1;
val mk_times = FOLogic.mk_binop @{const_name "zmult"};
@@ -149,7 +147,7 @@
| mk_prod (t :: ts) = if t = one then mk_prod ts
else mk_times (t, mk_prod ts);
-val dest_times = FOLogic.dest_bin @{const_name "zmult"} iT;
+val dest_times = FOLogic.dest_bin @{const_name "zmult"} @{typ i};
fun dest_prod t =
let val (t,u) = dest_times t
@@ -255,7 +253,7 @@
(open CancelNumeralsCommon
val prove_conv = ArithData.prove_conv "intless_cancel_numerals"
val mk_bal = FOLogic.mk_binrel @{const_name "zless"}
- val dest_bal = FOLogic.dest_bin @{const_name "zless"} iT
+ val dest_bal = FOLogic.dest_bin @{const_name "zless"} @{typ i}
val bal_add1 = less_add_iff1 RS iff_trans
val bal_add2 = less_add_iff2 RS iff_trans
);
@@ -264,7 +262,7 @@
(open CancelNumeralsCommon
val prove_conv = ArithData.prove_conv "intle_cancel_numerals"
val mk_bal = FOLogic.mk_binrel @{const_name "zle"}
- val dest_bal = FOLogic.dest_bin @{const_name "zle"} iT
+ val dest_bal = FOLogic.dest_bin @{const_name "zle"} @{typ i}
val bal_add1 = le_add_iff1 RS iff_trans
val bal_add2 = le_add_iff2 RS iff_trans
);