src/HOL/Tools/nat_arith.ML
changeset 35047 1b2bae06c796
parent 34974 18b41bba42b5
child 35064 1bdef0c013d3
equal deleted inserted replaced
35046:1266f04f42ec 35047:1b2bae06c796
    48 structure CommonCancelSums =
    48 structure CommonCancelSums =
    49 struct
    49 struct
    50   val mk_sum = mk_norm_sum;
    50   val mk_sum = mk_norm_sum;
    51   val dest_sum = dest_sum;
    51   val dest_sum = dest_sum;
    52   val prove_conv = Arith_Data.prove_conv2;
    52   val prove_conv = Arith_Data.prove_conv2;
    53   val norm_tac1 = Arith_Data.simp_all_tac [@{thm "add_Suc"}, @{thm "add_Suc_right"},
    53   val norm_tac1 = Arith_Data.simp_all_tac [@{thm add_Suc}, @{thm add_Suc_right},
    54     @{thm "add_0"}, @{thm "add_0_right"}];
    54     @{thm add_0}, @{thm Nat.add_0_right}];
    55   val norm_tac2 = Arith_Data.simp_all_tac @{thms add_ac};
    55   val norm_tac2 = Arith_Data.simp_all_tac @{thms add_ac};
    56   fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss;
    56   fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss;
    57   fun gen_uncancel_tac rule = let val rule' = rule RS @{thm subst_equals}
    57   fun gen_uncancel_tac rule = let val rule' = rule RS @{thm subst_equals}
    58     in fn ct => rtac (instantiate' [] [NONE, SOME ct] rule') 1 end;
    58     in fn ct => rtac (instantiate' [] [NONE, SOME ct] rule') 1 end;
    59 end;
    59 end;