src/HOL/Tools/nat_arith.ML
changeset 48372 868dc809c8a2
parent 38864 4abe644fcea5
child 48559 686cc7c47589
     1.1 --- a/src/HOL/Tools/nat_arith.ML	Thu Jul 19 22:21:59 2012 +0200
     1.2 +++ b/src/HOL/Tools/nat_arith.ML	Fri Jul 20 10:53:25 2012 +0200
     1.3 @@ -49,13 +49,11 @@
     1.4  struct
     1.5    val mk_sum = mk_norm_sum;
     1.6    val dest_sum = dest_sum;
     1.7 -  val prove_conv = Arith_Data.prove_conv2;
     1.8 +  val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
     1.9    val norm_tac1 = Arith_Data.simp_all_tac [@{thm add_Suc}, @{thm add_Suc_right},
    1.10      @{thm Nat.add_0}, @{thm Nat.add_0_right}];
    1.11    val norm_tac2 = Arith_Data.simp_all_tac @{thms add_ac};
    1.12    fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss;
    1.13 -  fun gen_uncancel_tac rule = let val rule' = rule RS @{thm subst_equals}
    1.14 -    in fn ct => rtac (instantiate' [] [NONE, SOME ct] rule') 1 end;
    1.15  end;
    1.16  
    1.17  structure EqCancelSums = CancelSumsFun
    1.18 @@ -63,7 +61,7 @@
    1.19    open CommonCancelSums;
    1.20    val mk_bal = HOLogic.mk_eq;
    1.21    val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT;
    1.22 -  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel"};
    1.23 +  val cancel_rule = mk_meta_eq @{thm nat_add_left_cancel};
    1.24  end);
    1.25  
    1.26  structure LessCancelSums = CancelSumsFun
    1.27 @@ -71,7 +69,7 @@
    1.28    open CommonCancelSums;
    1.29    val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less};
    1.30    val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT;
    1.31 -  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_less"};
    1.32 +  val cancel_rule = mk_meta_eq @{thm nat_add_left_cancel_less};
    1.33  end);
    1.34  
    1.35  structure LeCancelSums = CancelSumsFun
    1.36 @@ -79,7 +77,7 @@
    1.37    open CommonCancelSums;
    1.38    val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq};
    1.39    val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT;
    1.40 -  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_le"};
    1.41 +  val cancel_rule = mk_meta_eq @{thm nat_add_left_cancel_le};
    1.42  end);
    1.43  
    1.44  structure DiffCancelSums = CancelSumsFun
    1.45 @@ -87,7 +85,7 @@
    1.46    open CommonCancelSums;
    1.47    val mk_bal = HOLogic.mk_binop @{const_name Groups.minus};
    1.48    val dest_bal = HOLogic.dest_bin @{const_name Groups.minus} HOLogic.natT;
    1.49 -  val uncancel_tac = gen_uncancel_tac @{thm "diff_cancel"};
    1.50 +  val cancel_rule = mk_meta_eq @{thm diff_cancel};
    1.51  end);
    1.52  
    1.53  val nat_cancel_sums_add =