src/HOL/Arith.ML
changeset 2682 13cdbf95ed92
parent 2498 7914881f47c0
child 2922 580647a879cf
     1.1 --- a/src/HOL/Arith.ML	Tue Feb 25 15:11:12 1997 +0100
     1.2 +++ b/src/HOL/Arith.ML	Tue Feb 25 15:11:56 1997 +0100
     1.3 @@ -19,13 +19,7 @@
     1.4  by(Simp_tac 1);
     1.5  qed "pred_Suc";
     1.6  
     1.7 -val [add_0,add_Suc] = nat_recs add_def; 
     1.8 -val [mult_0,mult_Suc] = nat_recs mult_def;
     1.9 -store_thm("add_0",add_0);
    1.10 -store_thm("add_Suc",add_Suc);
    1.11 -store_thm("mult_0",mult_0);
    1.12 -store_thm("mult_Suc",mult_Suc);
    1.13 -Addsimps [pred_0,pred_Suc,add_0,add_Suc,mult_0,mult_Suc];
    1.14 +Addsimps [pred_0,pred_Suc];
    1.15  
    1.16  (** pred **)
    1.17  
    1.18 @@ -38,20 +32,18 @@
    1.19  
    1.20  (** Difference **)
    1.21  
    1.22 -bind_thm("diff_0", diff_def RS def_nat_rec_0);
    1.23 -
    1.24 -qed_goalw "diff_0_eq_0" Arith.thy [diff_def, pred_def]
    1.25 +qed_goalw "diff_0_eq_0" Arith.thy [pred_def]
    1.26      "0 - n = 0"
    1.27   (fn _ => [nat_ind_tac "n" 1,  ALLGOALS Asm_simp_tac]);
    1.28  
    1.29  (*Must simplify BEFORE the induction!!  (Else we get a critical pair)
    1.30    Suc(m) - Suc(n)   rewrites to   pred(Suc(m) - n)  *)
    1.31 -qed_goalw "diff_Suc_Suc" Arith.thy [diff_def, pred_def]
    1.32 +qed_goalw "diff_Suc_Suc" Arith.thy [pred_def]
    1.33      "Suc(m) - Suc(n) = m - n"
    1.34   (fn _ =>
    1.35    [Simp_tac 1, nat_ind_tac "n" 1, ALLGOALS Asm_simp_tac]);
    1.36  
    1.37 -Addsimps [diff_0, diff_0_eq_0, diff_Suc_Suc];
    1.38 +Addsimps [diff_0_eq_0, diff_Suc_Suc];
    1.39  
    1.40  
    1.41  goal Arith.thy "!!k. 0<k ==> EX j. k = Suc(j)";
    1.42 @@ -179,6 +171,10 @@
    1.43  
    1.44  (*** Difference ***)
    1.45  
    1.46 +qed_goal "pred_Suc_diff" Arith.thy "pred(Suc m - n) = m - n"
    1.47 + (fn _ => [nat_ind_tac "n" 1, ALLGOALS Asm_simp_tac]);
    1.48 +Addsimps [pred_Suc_diff];
    1.49 +
    1.50  qed_goal "diff_self_eq_0" Arith.thy "m - m = 0"
    1.51   (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
    1.52  Addsimps [diff_self_eq_0];