src/HOL/Arith.ML
changeset 3381 2bac33ec2b0d
parent 3366 2402c6ab1561
child 3396 aa74c71c3982
     1.1 --- a/src/HOL/Arith.ML	Fri May 30 16:37:20 1997 +0200
     1.2 +++ b/src/HOL/Arith.ML	Mon Jun 02 12:12:27 1997 +0200
     1.3 @@ -325,12 +325,20 @@
     1.4  Addsimps [diff_self_eq_0];
     1.5  
     1.6  (*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
     1.7 -val [prem] = goal Arith.thy "~ m<n ==> n+(m-n) = (m::nat)";
     1.8 -by (rtac (prem RS rev_mp) 1);
     1.9 +goal Arith.thy "~ m<n --> n+(m-n) = (m::nat)";
    1.10  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.11  by (ALLGOALS Asm_simp_tac);
    1.12 -qed "add_diff_inverse";
    1.13 +qed_spec_mp "add_diff_inverse";
    1.14 +
    1.15 +goal Arith.thy "!!m. n<=m ==> n+(m-n) = (m::nat)";
    1.16 +by (asm_simp_tac (!simpset addsimps [add_diff_inverse, not_less_iff_le]) 1);
    1.17 +qed "le_add_diff_inverse";
    1.18  
    1.19 +goal Arith.thy "!!m. n<=m ==> (m-n)+n = (m::nat)";
    1.20 +by (asm_simp_tac (!simpset addsimps [le_add_diff_inverse, add_commute]) 1);
    1.21 +qed "le_add_diff_inverse2";
    1.22 +
    1.23 +Addsimps  [le_add_diff_inverse, le_add_diff_inverse2];
    1.24  Delsimps  [diff_Suc];
    1.25  
    1.26  
    1.27 @@ -368,8 +376,6 @@
    1.28  by (ALLGOALS Asm_simp_tac);
    1.29  by (asm_simp_tac
    1.30      (!simpset addsimps [Suc_diff_n, le_imp_less_Suc, le_Suc_eq]) 1);
    1.31 -by (simp_tac
    1.32 -    (!simpset addsimps [add_diff_inverse, not_less_iff_le, add_commute]) 1);
    1.33  qed_spec_mp "diff_diff_right";
    1.34  
    1.35  goal Arith.thy "!!i j k:: nat. k<=j --> (i + j) - k = i + (j - k)";
    1.36 @@ -390,9 +396,7 @@
    1.37  
    1.38  goal Arith.thy "!!i j k::nat. i<=j ==> (j-i=k) = (j=k+i)";
    1.39  by (Step_tac 1);
    1.40 -by (ALLGOALS 
    1.41 -    (asm_simp_tac
    1.42 -     (!simpset addsimps [add_diff_inverse, not_less_iff_le, add_commute])));
    1.43 +by (ALLGOALS Asm_simp_tac);
    1.44  qed "le_imp_diff_is_add";
    1.45  
    1.46  val [prem] = goal Arith.thy "m < Suc(n) ==> m-n = 0";
    1.47 @@ -563,10 +567,10 @@
    1.48  
    1.49  goal Arith.thy "!! a b c::nat. [| a < b; c <= a |] ==> a-c < b-c";
    1.50  by (subgoal_tac "c+(a-c) < c+(b-c)" 1);
    1.51 -by (Asm_full_simp_tac 1);
    1.52 +by (Full_simp_tac 1);
    1.53  by (subgoal_tac "c <= b" 1);
    1.54  by (blast_tac (!claset addIs [less_imp_le, le_trans]) 2);
    1.55 -by (asm_simp_tac (!simpset addsimps [leD RS add_diff_inverse]) 1);
    1.56 +by (Asm_simp_tac 1);
    1.57  qed "diff_less_mono";
    1.58  
    1.59  goal Arith.thy "!! a b c::nat. a+b < c ==> a < c-b";
    1.60 @@ -587,10 +591,10 @@
    1.61  
    1.62  goal Arith.thy "!! i::nat. i <= n ==> n - (n - i) = i";
    1.63  by (subgoal_tac "(n-i) + (n - (n-i)) = (n-i) + i" 1);
    1.64 -by (Asm_full_simp_tac 1);
    1.65 -by (asm_simp_tac (!simpset addsimps [leD RS add_diff_inverse, diff_le_self, 
    1.66 -				     add_commute]) 1);
    1.67 +by (Full_simp_tac 1);
    1.68 +by (asm_simp_tac (!simpset addsimps [diff_le_self, add_commute]) 1);
    1.69  qed "diff_diff_cancel";
    1.70 +Addsimps [diff_diff_cancel];
    1.71  
    1.72  goal Arith.thy "!!k::nat. k <= n ==> m <= n + m - k";
    1.73  be rev_mp 1;