src/ZF/arith_data.ML
changeset 9570 e16e168984e1
parent 9548 15bee2731e43
child 9649 89155e48fa53
     1.1 --- a/src/ZF/arith_data.ML	Thu Aug 10 00:45:23 2000 +0200
     1.2 +++ b/src/ZF/arith_data.ML	Thu Aug 10 11:27:34 2000 +0200
     1.3 @@ -8,9 +8,16 @@
     1.4  
     1.5  signature ARITH_DATA =
     1.6  sig
     1.7 +  (*the main outcome*)
     1.8    val nat_cancel: simproc list
     1.9 +  (*tools for use in similar applications*)
    1.10 +  val gen_trans_tac: thm -> thm option -> tactic
    1.11 +  val prove_conv: string -> tactic list -> Sign.sg -> 
    1.12 +                  thm list -> term * term -> thm option
    1.13 +  val simplify_meta_eq: thm list -> thm -> thm
    1.14  end;
    1.15  
    1.16 +
    1.17  structure ArithData: ARITH_DATA =
    1.18  struct
    1.19  
    1.20 @@ -21,11 +28,7 @@
    1.21  fun mk_succ t = succ $ t;
    1.22  val one = mk_succ zero;
    1.23  
    1.24 -(*Not FOLogic.mk_binop, since it calls fastype_of, which can fail*)
    1.25 -fun mk_binop_i  c (t,u) = Const (c, [iT,iT] ---> iT) $ t $ u;
    1.26 -fun mk_binrel_i c (t,u) = Const (c, [iT,iT] ---> oT) $ t $ u;
    1.27 -
    1.28 -val mk_plus = mk_binop_i "Arith.add";
    1.29 +val mk_plus = FOLogic.mk_binop "Arith.add";
    1.30  
    1.31  (*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
    1.32  fun mk_sum []        = zero
    1.33 @@ -81,7 +84,7 @@
    1.34  (*** Use CancelNumerals simproc without binary numerals, 
    1.35       just for cancellation ***)
    1.36  
    1.37 -val mk_times = mk_binop_i "Arith.mult";
    1.38 +val mk_times = FOLogic.mk_binop "Arith.mult";
    1.39  
    1.40  fun mk_prod [] = one
    1.41    | mk_prod [t] = t
    1.42 @@ -120,14 +123,14 @@
    1.43  val mult_1s = [mult_1_natify, mult_1_right_natify];
    1.44  val tc_rules = [natify_in_nat, add_type, diff_type, mult_type];
    1.45  val natifys = [natify_0, natify_ident, add_natify1, add_natify2,
    1.46 -               add_natify1, add_natify2, diff_natify1, diff_natify2];
    1.47 +               diff_natify1, diff_natify2];
    1.48  
    1.49  (*Final simplification: cancel + and **)
    1.50  fun simplify_meta_eq rules =
    1.51      mk_meta_eq o
    1.52      simplify (FOL_ss addeqcongs[eq_cong2,iff_cong2] 
    1.53                       delsimps iff_simps (*these could erase the whole rule!*)
    1.54 -		     addsimps rules)
    1.55 +		     addsimps rules);
    1.56  
    1.57  val final_rules = add_0s @ mult_1s @ [mult_0, mult_0_right];
    1.58  
    1.59 @@ -161,7 +164,7 @@
    1.60  structure LessCancelNumerals = CancelNumeralsFun
    1.61   (open CancelNumeralsCommon
    1.62    val prove_conv = prove_conv "natless_cancel_numerals"
    1.63 -  val mk_bal   = mk_binrel_i "Ordinal.op <"
    1.64 +  val mk_bal   = FOLogic.mk_binrel "Ordinal.op <"
    1.65    val dest_bal = FOLogic.dest_bin "Ordinal.op <" iT
    1.66    val bal_add1 = less_add_iff RS iff_trans
    1.67    val bal_add2 = less_add_iff RS iff_trans
    1.68 @@ -171,7 +174,7 @@
    1.69  structure DiffCancelNumerals = CancelNumeralsFun
    1.70   (open CancelNumeralsCommon
    1.71    val prove_conv = prove_conv "natdiff_cancel_numerals"
    1.72 -  val mk_bal   = mk_binop_i "Arith.diff"
    1.73 +  val mk_bal   = FOLogic.mk_binop "Arith.diff"
    1.74    val dest_bal = FOLogic.dest_bin "Arith.diff" iT
    1.75    val bal_add1 = diff_add_eq RS trans
    1.76    val bal_add2 = diff_add_eq RS trans