# HG changeset patch # User wenzelm # Date 1204380063 -3600 # Node ID cf51a23c0cd00c7f3b393e138a1422f77fd9b087 # Parent 9808cca5c54dbe3dd72b793d7a0f3290463e65d4 tuned ML code, more antiquotations; diff -r 9808cca5c54d -r cf51a23c0cd0 src/ZF/Bin.thy --- 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" ("_") diff -r 9808cca5c54d -r cf51a23c0cd0 src/ZF/Inductive_ZF.thy --- 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} diff -r 9808cca5c54d -r cf51a23c0cd0 src/ZF/Tools/datatype_package.ML --- 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 = diff -r 9808cca5c54d -r cf51a23c0cd0 src/ZF/Tools/numeral_syntax.ML --- 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; diff -r 9808cca5c54d -r cf51a23c0cd0 src/ZF/int_arith.ML --- 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 );