changed Suc_diff_n to Suc_diff_le, with premise n <= m instead of n < Suc(m)
authorpaulson
Tue Sep 01 15:03:10 1998 +0200 (1998-09-01)
changeset 54148a458866637c
parent 5413 9d11f2d39b13
child 5415 13a199e94877
changed Suc_diff_n to Suc_diff_le, with premise n <= m instead of n < Suc(m)
src/HOL/Arith.ML
     1.1 --- a/src/HOL/Arith.ML	Tue Sep 01 10:25:05 1998 +0200
     1.2 +++ b/src/HOL/Arith.ML	Tue Sep 01 15:03:10 1998 +0200
     1.3 @@ -331,11 +331,11 @@
     1.4  
     1.5  (*** More results about difference ***)
     1.6  
     1.7 -Goal "n < Suc(m) ==> Suc(m)-n = Suc(m-n)";
     1.8 +Goal "n <= m ==> Suc(m)-n = Suc(m-n)";
     1.9  by (etac rev_mp 1);
    1.10  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.11  by (ALLGOALS Asm_simp_tac);
    1.12 -qed "Suc_diff_n";
    1.13 +qed "Suc_diff_le";
    1.14  
    1.15  Goal "m - n < Suc(m)";
    1.16  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.17 @@ -372,7 +372,7 @@
    1.18  Goal "i<n ==> n - Suc i < n - i";
    1.19  by (exhaust_tac "n" 1);
    1.20  by Safe_tac;
    1.21 -by (asm_simp_tac (simpset() addsimps [Suc_diff_n]) 1);
    1.22 +by (asm_simp_tac (simpset() addsimps [le_eq_less_Suc, Suc_diff_le]) 1);
    1.23  qed "diff_Suc_less_diff";
    1.24  
    1.25  Goal "m - n <= Suc m - n";
    1.26 @@ -388,8 +388,7 @@
    1.27  Goal "!!i j k:: nat. k<=j --> j<=i --> i - (j - k) = i - j + k";
    1.28  by (res_inst_tac [("m","i"),("n","j")] diff_induct 1);
    1.29  by (ALLGOALS Asm_simp_tac);
    1.30 -by (asm_simp_tac
    1.31 -    (simpset() addsimps [Suc_diff_n, le_imp_less_Suc, le_Suc_eq]) 1);
    1.32 +by (asm_simp_tac (simpset() addsimps [Suc_diff_le, le_Suc_eq]) 1);
    1.33  qed_spec_mp "diff_diff_right";
    1.34  
    1.35  Goal "!!i j k:: nat. k<=j --> (i + j) - k = i + (j - k)";
    1.36 @@ -440,12 +439,11 @@
    1.37  qed "less_imp_add_positive";
    1.38  
    1.39  Goal "Suc(m)-n = (if m<n then 0 else Suc(m-n))";
    1.40 -by (simp_tac (simpset() addsimps [leI, Suc_le_eq, 
    1.41 -				  le_imp_less_Suc RS Suc_diff_n]) 1);
    1.42 -qed "if_Suc_diff_n";
    1.43 +by (simp_tac (simpset() addsimps [leI, Suc_le_eq, Suc_diff_le]) 1);
    1.44 +qed "if_Suc_diff_le";
    1.45  
    1.46  Goal "Suc(m)-n <= Suc(m-n)";
    1.47 -by (simp_tac (simpset() addsimps [if_Suc_diff_n]) 1);
    1.48 +by (simp_tac (simpset() addsimps [if_Suc_diff_le]) 1);
    1.49  qed "diff_Suc_le_Suc_diff";
    1.50  
    1.51  Goal "P(k) --> (!n. P(Suc(n))--> P(n)) --> P(k-i)";
    1.52 @@ -471,20 +469,13 @@
    1.53  qed "diff_cancel2";
    1.54  Addsimps [diff_cancel2];
    1.55  
    1.56 -(*From Clemens Ballarin*)
    1.57 +(*From Clemens Ballarin, proof by lcp*)
    1.58  Goal "!!n::nat. [| k<=n; n<=m |] ==> (m-k) - (n-k) = m-n";
    1.59 -by (subgoal_tac "k<=n --> n<=m --> (m-k) - (n-k) = m-n" 1);
    1.60 -by (Asm_full_simp_tac 1);
    1.61 -by (induct_tac "k" 1);
    1.62 -by (Simp_tac 1);
    1.63 -(* Induction step *)
    1.64 -by (subgoal_tac "Suc na <= m --> n <= m --> Suc na <= n --> \
    1.65 -\                Suc (m - Suc na) - Suc (n - Suc na) = m-n" 1);
    1.66 -by (Asm_full_simp_tac 1);
    1.67 -by (blast_tac (claset() addIs [le_trans]) 1);
    1.68 -by (auto_tac (claset() addIs [Suc_leD], simpset() delsimps [diff_Suc_Suc]));
    1.69 -by (asm_full_simp_tac (simpset() delsimps [Suc_less_eq] 
    1.70 -		       addsimps [le_imp_less_Suc RS Suc_diff_n RS sym]) 1);
    1.71 +by (REPEAT (etac rev_mp 1));
    1.72 +by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.73 +by (ALLGOALS Asm_simp_tac);
    1.74 +(*a confluence problem*)
    1.75 +by (asm_simp_tac (simpset() addsimps [Suc_diff_le, le_Suc_eq]) 1);
    1.76  qed "diff_right_cancel";
    1.77  
    1.78  Goal "!!n::nat. n - (n+m) = 0";
    1.79 @@ -622,13 +613,8 @@
    1.80  by (Asm_full_simp_tac 1);
    1.81  qed "add_less_imp_less_diff";
    1.82  
    1.83 -Goal "n <= m ==> Suc m - n = Suc (m - n)";
    1.84 -by (asm_full_simp_tac (simpset() addsimps [le_imp_less_Suc RS Suc_diff_n]) 1);
    1.85 -qed "Suc_diff_le";
    1.86 -
    1.87  Goal "Suc i <= n ==> Suc (n - Suc i) = n - i";
    1.88 -by (asm_full_simp_tac
    1.89 -    (simpset() addsimps [Suc_diff_n RS sym, le_eq_less_Suc]) 1);
    1.90 +by (asm_simp_tac (simpset() addsimps [Suc_diff_le RS sym]) 1);
    1.91  qed "Suc_diff_Suc";
    1.92  
    1.93  Goal "!! i::nat. i <= n ==> n - (n - i) = i";
    1.94 @@ -687,6 +673,18 @@
    1.95  by (auto_tac (claset(), simpset() addsimps [Suc_le_eq]));
    1.96  qed "less_pred_eq";
    1.97  
    1.98 +(*In ordinary notation: if 0<n and n<=m then m-n < m *)
    1.99 +Goal "[| 0<n; ~ m<n |] ==> m - n < m";
   1.100 +by (subgoal_tac "0<n --> ~ m<n --> m - n < m" 1);
   1.101 +by (Blast_tac 1);
   1.102 +by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   1.103 +by (ALLGOALS(asm_simp_tac(simpset() addsimps [diff_less_Suc])));
   1.104 +qed "diff_less";
   1.105 +
   1.106 +Goal "[| 0<n; n<=m |] ==> m - n < m";
   1.107 +by (asm_simp_tac (simpset() addsimps [diff_less, not_less_iff_le]) 1);
   1.108 +qed "le_diff_less";
   1.109 +
   1.110  
   1.111  
   1.112  (** (Anti)Monotonicity of subtraction -- by Stefan Merz **)
   1.113 @@ -707,5 +705,5 @@
   1.114  by (asm_simp_tac (simpset() addsimps [Suc_diff_le]) 1);
   1.115  by (fast_tac (claset() addEs [le_trans]) 1);
   1.116  by (dtac not_leE 1);
   1.117 -by (asm_simp_tac (simpset() addsimps [if_Suc_diff_n]) 1);
   1.118 +by (asm_simp_tac (simpset() addsimps [if_Suc_diff_le]) 1);
   1.119  qed_spec_mp "diff_le_mono2";