tuned ML code, more antiquotations;
authorwenzelm
Sat Mar 01 15:01:03 2008 +0100 (2008-03-01)
changeset 26190cf51a23c0cd0
parent 26189 9808cca5c54d
child 26191 ae537f315b34
tuned ML code, more antiquotations;
src/ZF/Bin.thy
src/ZF/Inductive_ZF.thy
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/numeral_syntax.ML
src/ZF/int_arith.ML
     1.1 --- a/src/ZF/Bin.thy	Sat Mar 01 14:10:15 2008 +0100
     1.2 +++ b/src/ZF/Bin.thy	Sat Mar 01 15:01:03 2008 +0100
     1.3 @@ -18,7 +18,7 @@
     1.4  
     1.5  theory Bin
     1.6  imports Int_ZF Datatype_ZF
     1.7 -uses "Tools/numeral_syntax.ML"
     1.8 +uses ("Tools/numeral_syntax.ML")
     1.9  begin
    1.10  
    1.11  consts  bin :: i
    1.12 @@ -27,6 +27,8 @@
    1.13          | Min
    1.14          | Bit ("w: bin", "b: bool")	(infixl "BIT" 90)
    1.15  
    1.16 +use "Tools/numeral_syntax.ML"
    1.17 +
    1.18  syntax
    1.19    "_Int"    :: "xnum => i"        ("_")
    1.20  
     2.1 --- a/src/ZF/Inductive_ZF.thy	Sat Mar 01 14:10:15 2008 +0100
     2.2 +++ b/src/ZF/Inductive_ZF.thy	Sat Mar 01 15:01:03 2008 +0100
     2.3 @@ -42,9 +42,6 @@
     2.4  setup DatatypeTactics.setup
     2.5  
     2.6  ML_setup {*
     2.7 -val iT = Ind_Syntax.iT
     2.8 -and oT = FOLogic.oT;
     2.9 -
    2.10  structure Lfp =
    2.11    struct
    2.12    val oper      = @{const lfp}
     3.1 --- a/src/ZF/Tools/datatype_package.ML	Sat Mar 01 14:10:15 2008 +0100
     3.2 +++ b/src/ZF/Tools/datatype_package.ML	Sat Mar 01 15:01:03 2008 +0100
     3.3 @@ -92,7 +92,7 @@
     3.4    (** Define the constructors **)
     3.5  
     3.6    (*The empty tuple is 0*)
     3.7 -  fun mk_tuple [] = Const("0",iT)
     3.8 +  fun mk_tuple [] = @{const "0"}
     3.9      | mk_tuple args = foldr1 (fn (t1, t2) => Pr.pair $ t1 $ t2) args;
    3.10  
    3.11    fun mk_inject n k u = BalancedTree.access
    3.12 @@ -119,10 +119,10 @@
    3.13  
    3.14    (*Combine split terms using case; yields the case operator for one part*)
    3.15    fun call_case case_list =
    3.16 -    let fun call_f (free,[]) = Abs("null", iT, free)
    3.17 +    let fun call_f (free,[]) = Abs("null", @{typ i}, free)
    3.18            | call_f (free,args) =
    3.19                  CP.ap_split (foldr1 CP.mk_prod (map (#2 o dest_Free) args))
    3.20 -                            Ind_Syntax.iT
    3.21 +                            @{typ i}
    3.22                              free
    3.23      in  BalancedTree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_f case_list)  end;
    3.24  
    3.25 @@ -147,7 +147,7 @@
    3.26    val (_, case_lists) = foldr add_case_list (1,[]) con_ty_lists;
    3.27  
    3.28    (*extract the types of all the variables*)
    3.29 -  val case_typ = List.concat (map (map (#2 o #1)) con_ty_lists) ---> (iT-->iT);
    3.30 +  val case_typ = List.concat (map (map (#2 o #1)) con_ty_lists) ---> @{typ "i => i"};
    3.31  
    3.32    val case_base_name = big_rec_base_name ^ "_case";
    3.33    val case_name = full_name case_base_name;
    3.34 @@ -166,7 +166,7 @@
    3.35        Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
    3.36  
    3.37    (*a recursive call for x is the application rec`x  *)
    3.38 -  val rec_call = @{const apply} $ Free ("rec", iT);
    3.39 +  val rec_call = @{const apply} $ Free ("rec", @{typ i});
    3.40  
    3.41    (*look back down the "case args" (which have been reversed) to
    3.42      determine the de Bruijn index*)
    3.43 @@ -203,7 +203,7 @@
    3.44    (*Add an argument position for each occurrence of a recursive set.
    3.45      Strictly speaking, the recursive arguments are the LAST of the function
    3.46      variable, but they all have type "i" anyway*)
    3.47 -  fun add_rec_args args' T = (map (fn _ => iT) args') ---> T
    3.48 +  fun add_rec_args args' T = (map (fn _ => @{typ i}) args') ---> T
    3.49  
    3.50    (*Plug in the function variable type needed for the recursor
    3.51      as well as the new arguments (recursive calls)*)
    3.52 @@ -219,8 +219,7 @@
    3.53    val (_, recursor_lists) = foldr add_case_list (1,[]) rec_ty_lists;
    3.54  
    3.55    (*extract the types of all the variables*)
    3.56 -  val recursor_typ = List.concat (map (map (#2 o #1)) rec_ty_lists)
    3.57 -                         ---> (iT-->iT);
    3.58 +  val recursor_typ = List.concat (map (map (#2 o #1)) rec_ty_lists) ---> @{typ "i => i"};
    3.59  
    3.60    val recursor_base_name = big_rec_base_name ^ "_rec";
    3.61    val recursor_name = full_name recursor_base_name;
    3.62 @@ -238,7 +237,7 @@
    3.63        PrimitiveDefs.mk_defpair
    3.64          (recursor_tm,
    3.65           @{const Univ.Vrecursor} $
    3.66 -           absfree ("rec", iT, list_comb (case_const, recursor_cases)));
    3.67 +           absfree ("rec", @{typ i}, list_comb (case_const, recursor_cases)));
    3.68  
    3.69    (* Build the new theory *)
    3.70  
    3.71 @@ -406,7 +405,7 @@
    3.72  fun add_datatype (sdom, srec_tms) scon_ty_lists (raw_monos, raw_type_intrs, raw_type_elims) thy =
    3.73    let
    3.74      val ctxt = ProofContext.init thy;
    3.75 -    val read_i = Sign.simple_read_term thy Ind_Syntax.iT;
    3.76 +    val read_i = Sign.simple_read_term thy @{typ i};
    3.77      val rec_tms = map read_i srec_tms;
    3.78      val con_ty_lists = Ind_Syntax.read_constructs thy scon_ty_lists;
    3.79      val dom_sum =
     4.1 --- a/src/ZF/Tools/numeral_syntax.ML	Sat Mar 01 14:10:15 2008 +0100
     4.2 +++ b/src/ZF/Tools/numeral_syntax.ML	Sat Mar 01 15:01:03 2008 +0100
     4.3 @@ -20,15 +20,12 @@
     4.4  
     4.5  (* Bits *)
     4.6  
     4.7 -val zero = Const("0", iT);
     4.8 -val succ = Const("succ", iT --> iT);
     4.9 -
    4.10 -fun mk_bit 0 = zero
    4.11 -  | mk_bit 1 = succ$zero
    4.12 +fun mk_bit 0 = @{term "0"}
    4.13 +  | mk_bit 1 = @{term "succ(0)"}
    4.14    | mk_bit _ = sys_error "mk_bit";
    4.15  
    4.16 -fun dest_bit (Const ("0", _)) = 0
    4.17 -  | dest_bit (Const ("succ", _) $ Const ("0", _)) = 1
    4.18 +fun dest_bit (Const (@{const_name "0"}, _)) = 0
    4.19 +  | dest_bit (Const (@{const_name succ}, _) $ Const (@{const_name "0"}, _)) = 1
    4.20    | dest_bit _ = raise Match;
    4.21  
    4.22  
    4.23 @@ -38,18 +35,14 @@
    4.24    | prefix_len pred (x :: xs) =
    4.25        if pred x then 1 + prefix_len pred xs else 0;
    4.26  
    4.27 -val pls_const = Const ("Bin.bin.Pls", iT)
    4.28 -and min_const = Const ("Bin.bin.Min", iT)
    4.29 -and bit_const = Const ("Bin.bin.Bit", [iT, iT] ---> iT);
    4.30 -
    4.31  fun mk_bin i =
    4.32    let fun bin_of_int 0  = []
    4.33    	    | bin_of_int ~1 = [~1]
    4.34      	| bin_of_int n  = (n mod 2) :: bin_of_int (n div 2);
    4.35  
    4.36 -      fun term_of []   = pls_const
    4.37 -	    | term_of [~1] = min_const
    4.38 -	    | term_of (b :: bs) = bit_const $ term_of bs $ mk_bit b;
    4.39 +      fun term_of [] = @{const Pls}
    4.40 +	    | term_of [~1] = @{const Min}
    4.41 +	    | term_of (b :: bs) = @{const Bit} $ term_of bs $ mk_bit b;
    4.42    in
    4.43      term_of (bin_of_int i)
    4.44    end;
     5.1 --- a/src/ZF/int_arith.ML	Sat Mar 01 14:10:15 2008 +0100
     5.2 +++ b/src/ZF/int_arith.ML	Sat Mar 01 15:01:03 2008 +0100
     5.3 @@ -95,7 +95,7 @@
     5.4  
     5.5  (*Utilities*)
     5.6  
     5.7 -val integ_of_const = Const (@{const_name "Bin.integ_of"}, iT --> iT);
     5.8 +val integ_of_const = Const (@{const_name "Bin.integ_of"}, @{typ "i => i"});
     5.9  
    5.10  fun mk_numeral n = integ_of_const $ NumeralSyntax.mk_bin n;
    5.11  
    5.12 @@ -113,9 +113,7 @@
    5.13  val zero = mk_numeral 0;
    5.14  val mk_plus = FOLogic.mk_binop @{const_name "zadd"};
    5.15  
    5.16 -val iT = Ind_Syntax.iT;
    5.17 -
    5.18 -val zminus_const = Const (@{const_name "zminus"}, iT --> iT);
    5.19 +val zminus_const = Const (@{const_name "zminus"}, @{typ "i => i"});
    5.20  
    5.21  (*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
    5.22  fun mk_sum []        = zero
    5.23 @@ -126,7 +124,7 @@
    5.24  fun long_mk_sum []        = zero
    5.25    | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
    5.26  
    5.27 -val dest_plus = FOLogic.dest_bin @{const_name "zadd"} iT;
    5.28 +val dest_plus = FOLogic.dest_bin @{const_name "zadd"} @{typ i};
    5.29  
    5.30  (*decompose additions AND subtractions as a sum*)
    5.31  fun dest_summing (pos, Const (@{const_name "zadd"}, _) $ t $ u, ts) =
    5.32 @@ -139,7 +137,7 @@
    5.33  fun dest_sum t = dest_summing (true, t, []);
    5.34  
    5.35  val mk_diff = FOLogic.mk_binop @{const_name "zdiff"};
    5.36 -val dest_diff = FOLogic.dest_bin @{const_name "zdiff"} iT;
    5.37 +val dest_diff = FOLogic.dest_bin @{const_name "zdiff"} @{typ i};
    5.38  
    5.39  val one = mk_numeral 1;
    5.40  val mk_times = FOLogic.mk_binop @{const_name "zmult"};
    5.41 @@ -149,7 +147,7 @@
    5.42    | mk_prod (t :: ts) = if t = one then mk_prod ts
    5.43                          else mk_times (t, mk_prod ts);
    5.44  
    5.45 -val dest_times = FOLogic.dest_bin @{const_name "zmult"} iT;
    5.46 +val dest_times = FOLogic.dest_bin @{const_name "zmult"} @{typ i};
    5.47  
    5.48  fun dest_prod t =
    5.49        let val (t,u) = dest_times t
    5.50 @@ -255,7 +253,7 @@
    5.51   (open CancelNumeralsCommon
    5.52    val prove_conv = ArithData.prove_conv "intless_cancel_numerals"
    5.53    val mk_bal   = FOLogic.mk_binrel @{const_name "zless"}
    5.54 -  val dest_bal = FOLogic.dest_bin @{const_name "zless"} iT
    5.55 +  val dest_bal = FOLogic.dest_bin @{const_name "zless"} @{typ i}
    5.56    val bal_add1 = less_add_iff1 RS iff_trans
    5.57    val bal_add2 = less_add_iff2 RS iff_trans
    5.58  );
    5.59 @@ -264,7 +262,7 @@
    5.60   (open CancelNumeralsCommon
    5.61    val prove_conv = ArithData.prove_conv "intle_cancel_numerals"
    5.62    val mk_bal   = FOLogic.mk_binrel @{const_name "zle"}
    5.63 -  val dest_bal = FOLogic.dest_bin @{const_name "zle"} iT
    5.64 +  val dest_bal = FOLogic.dest_bin @{const_name "zle"} @{typ i}
    5.65    val bal_add1 = le_add_iff1 RS iff_trans
    5.66    val bal_add2 = le_add_iff2 RS iff_trans
    5.67  );