src/HOL/Arith.ML
changeset 4089 96fba19bcbe2
parent 3919 c036caebfc75
child 4158 47c7490c74fe
     1.1 --- a/src/HOL/Arith.ML	Mon Nov 03 12:12:10 1997 +0100
     1.2 +++ b/src/HOL/Arith.ML	Mon Nov 03 12:13:18 1997 +0100
     1.3 @@ -35,7 +35,7 @@
     1.4  AddIffs [pred_le];
     1.5  
     1.6  goalw Arith.thy [pred_def] "m<=n --> pred(m) <= pred(n)";
     1.7 -by(simp_tac (!simpset addsplits [expand_nat_case]) 1);
     1.8 +by(simp_tac (simpset() addsplits [expand_nat_case]) 1);
     1.9  qed_spec_mp "pred_le_mono";
    1.10  
    1.11  goal Arith.thy "!!n. n ~= 0 ==> pred n < n";
    1.12 @@ -124,7 +124,7 @@
    1.13  
    1.14  goal Arith.thy "(pred (m+n) = 0) = (m=0 & pred n = 0 | pred m = 0 & n=0)";
    1.15  by (induct_tac "m" 1);
    1.16 -by (ALLGOALS (fast_tac (!claset addss (!simpset))));
    1.17 +by (ALLGOALS (fast_tac (claset() addss (simpset()))));
    1.18  qed "pred_add_is_0";
    1.19  Addsimps [pred_add_is_0];
    1.20  
    1.21 @@ -140,7 +140,7 @@
    1.22  goal Arith.thy "i<j --> (EX k. j = Suc(i+k))";
    1.23  by (induct_tac "j" 1);
    1.24  by (Simp_tac 1);
    1.25 -by (blast_tac (!claset addSEs [less_SucE] 
    1.26 +by (blast_tac (claset() addSEs [less_SucE] 
    1.27                         addSIs [add_0_right RS sym, add_Suc_right RS sym]) 1);
    1.28  val lemma = result();
    1.29  
    1.30 @@ -149,8 +149,8 @@
    1.31  
    1.32  goal Arith.thy "!!m. m<n --> (? k. n=Suc(m+k))";
    1.33  by (induct_tac "n" 1);
    1.34 -by (ALLGOALS (simp_tac (!simpset addsimps [less_Suc_eq])));
    1.35 -by (blast_tac (!claset addSEs [less_SucE] 
    1.36 +by (ALLGOALS (simp_tac (simpset() addsimps [less_Suc_eq])));
    1.37 +by (blast_tac (claset() addSEs [less_SucE] 
    1.38                         addSIs [add_0_right RS sym, add_Suc_right RS sym]) 1);
    1.39  qed_spec_mp "less_eq_Suc_add";
    1.40  
    1.41 @@ -162,7 +162,7 @@
    1.42  qed "le_add2";
    1.43  
    1.44  goal Arith.thy "n <= ((n + m)::nat)";
    1.45 -by (simp_tac (!simpset addsimps add_ac) 1);
    1.46 +by (simp_tac (simpset() addsimps add_ac) 1);
    1.47  by (rtac le_add2 1);
    1.48  qed "le_add1";
    1.49  
    1.50 @@ -185,7 +185,7 @@
    1.51  by (etac rev_mp 1);
    1.52  by (induct_tac "j" 1);
    1.53  by (ALLGOALS Asm_simp_tac);
    1.54 -by (blast_tac (!claset addDs [Suc_lessD]) 1);
    1.55 +by (blast_tac (claset() addDs [Suc_lessD]) 1);
    1.56  qed "add_lessD1";
    1.57  
    1.58  goal Arith.thy "!!i::nat. ~ (i+j < i)";
    1.59 @@ -194,7 +194,7 @@
    1.60  qed "not_add_less1";
    1.61  
    1.62  goal Arith.thy "!!i::nat. ~ (j+i < i)";
    1.63 -by (simp_tac (!simpset addsimps [add_commute, not_add_less1]) 1);
    1.64 +by (simp_tac (simpset() addsimps [add_commute, not_add_less1]) 1);
    1.65  qed "not_add_less2";
    1.66  AddIffs [not_add_less1, not_add_less2];
    1.67  
    1.68 @@ -211,25 +211,25 @@
    1.69  goal Arith.thy "m+k<=n --> m<=(n::nat)";
    1.70  by (induct_tac "k" 1);
    1.71  by (ALLGOALS Asm_simp_tac);
    1.72 -by (blast_tac (!claset addDs [Suc_leD]) 1);
    1.73 +by (blast_tac (claset() addDs [Suc_leD]) 1);
    1.74  qed_spec_mp "add_leD1";
    1.75  
    1.76  goal Arith.thy "!!n::nat. m+k<=n ==> k<=n";
    1.77 -by (full_simp_tac (!simpset addsimps [add_commute]) 1);
    1.78 +by (full_simp_tac (simpset() addsimps [add_commute]) 1);
    1.79  by (etac add_leD1 1);
    1.80  qed_spec_mp "add_leD2";
    1.81  
    1.82  goal Arith.thy "!!n::nat. m+k<=n ==> m<=n & k<=n";
    1.83 -by (blast_tac (!claset addDs [add_leD1, add_leD2]) 1);
    1.84 +by (blast_tac (claset() addDs [add_leD1, add_leD2]) 1);
    1.85  bind_thm ("add_leE", result() RS conjE);
    1.86  
    1.87  goal Arith.thy "!!k l::nat. [| k<l; m+l = k+n |] ==> m<n";
    1.88 -by (safe_tac (!claset addSDs [less_eq_Suc_add]));
    1.89 +by (safe_tac (claset() addSDs [less_eq_Suc_add]));
    1.90  by (asm_full_simp_tac
    1.91 -    (!simpset delsimps [add_Suc_right]
    1.92 +    (simpset() delsimps [add_Suc_right]
    1.93                  addsimps ([add_Suc_right RS sym, add_left_cancel] @add_ac)) 1);
    1.94  by (etac subst 1);
    1.95 -by (simp_tac (!simpset addsimps [less_add_Suc1]) 1);
    1.96 +by (simp_tac (simpset() addsimps [less_add_Suc1]) 1);
    1.97  qed "less_add_eq_less";
    1.98  
    1.99  
   1.100 @@ -255,8 +255,8 @@
   1.101  \        i <= j                                 \
   1.102  \     |] ==> f(i) <= (f(j)::nat)";
   1.103  by (cut_facts_tac [le] 1);
   1.104 -by (asm_full_simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1);
   1.105 -by (blast_tac (!claset addSIs [lt_mono]) 1);
   1.106 +by (asm_full_simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
   1.107 +by (blast_tac (claset() addSIs [lt_mono]) 1);
   1.108  qed "less_mono_imp_le_mono";
   1.109  
   1.110  (*non-strict, in 1st argument*)
   1.111 @@ -269,7 +269,7 @@
   1.112  (*non-strict, in both arguments*)
   1.113  goal Arith.thy "!!k l::nat. [|i<=j;  k<=l |] ==> i + k <= j + l";
   1.114  by (etac (add_le_mono1 RS le_trans) 1);
   1.115 -by (simp_tac (!simpset addsimps [add_commute]) 1);
   1.116 +by (simp_tac (simpset() addsimps [add_commute]) 1);
   1.117  (*j moves to the end because it is free while k, l are bound*)
   1.118  by (etac add_le_mono1 1);
   1.119  qed "add_le_mono";
   1.120 @@ -284,7 +284,7 @@
   1.121  (*right successor law for multiplication*)
   1.122  qed_goal "mult_Suc_right" Arith.thy  "m * Suc(n) = m + (m * n)"
   1.123   (fn _ => [induct_tac "m" 1,
   1.124 -           ALLGOALS(asm_simp_tac (!simpset addsimps add_ac))]);
   1.125 +           ALLGOALS(asm_simp_tac (simpset() addsimps add_ac))]);
   1.126  
   1.127  Addsimps [mult_0_right, mult_Suc_right];
   1.128  
   1.129 @@ -303,16 +303,16 @@
   1.130  (*addition distributes over multiplication*)
   1.131  qed_goal "add_mult_distrib" Arith.thy "(m + n)*k = (m*k) + ((n*k)::nat)"
   1.132   (fn _ => [induct_tac "m" 1,
   1.133 -           ALLGOALS(asm_simp_tac (!simpset addsimps add_ac))]);
   1.134 +           ALLGOALS(asm_simp_tac (simpset() addsimps add_ac))]);
   1.135  
   1.136  qed_goal "add_mult_distrib2" Arith.thy "k*(m + n) = (k*m) + ((k*n)::nat)"
   1.137   (fn _ => [induct_tac "m" 1,
   1.138 -           ALLGOALS(asm_simp_tac (!simpset addsimps add_ac))]);
   1.139 +           ALLGOALS(asm_simp_tac (simpset() addsimps add_ac))]);
   1.140  
   1.141  (*Associative law for multiplication*)
   1.142  qed_goal "mult_assoc" Arith.thy "(m * n) * k = m * ((n * k)::nat)"
   1.143    (fn _ => [induct_tac "m" 1, 
   1.144 -            ALLGOALS (asm_simp_tac (!simpset addsimps [add_mult_distrib]))]);
   1.145 +            ALLGOALS (asm_simp_tac (simpset() addsimps [add_mult_distrib]))]);
   1.146  
   1.147  qed_goal "mult_left_commute" Arith.thy "x*(y*z) = y*((x*z)::nat)"
   1.148   (fn _ => [rtac trans 1, rtac mult_commute 1, rtac trans 1,
   1.149 @@ -345,11 +345,11 @@
   1.150  qed_spec_mp "add_diff_inverse";
   1.151  
   1.152  goal Arith.thy "!!m. n<=m ==> n+(m-n) = (m::nat)";
   1.153 -by (asm_simp_tac (!simpset addsimps [add_diff_inverse, not_less_iff_le]) 1);
   1.154 +by (asm_simp_tac (simpset() addsimps [add_diff_inverse, not_less_iff_le]) 1);
   1.155  qed "le_add_diff_inverse";
   1.156  
   1.157  goal Arith.thy "!!m. n<=m ==> (m-n)+n = (m::nat)";
   1.158 -by (asm_simp_tac (!simpset addsimps [le_add_diff_inverse, add_commute]) 1);
   1.159 +by (asm_simp_tac (simpset() addsimps [le_add_diff_inverse, add_commute]) 1);
   1.160  qed "le_add_diff_inverse2";
   1.161  
   1.162  Addsimps  [le_add_diff_inverse, le_add_diff_inverse2];
   1.163 @@ -367,7 +367,7 @@
   1.164  goal Arith.thy "m - n < Suc(m)";
   1.165  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   1.166  by (etac less_SucE 3);
   1.167 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [less_Suc_eq])));
   1.168 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq])));
   1.169  qed "diff_less_Suc";
   1.170  
   1.171  goal Arith.thy "!!m::nat. m - n <= m";
   1.172 @@ -383,14 +383,14 @@
   1.173  
   1.174  (*This and the next few suggested by Florian Kammueller*)
   1.175  goal Arith.thy "!!i::nat. i-j-k = i-k-j";
   1.176 -by (simp_tac (!simpset addsimps [diff_diff_left, add_commute]) 1);
   1.177 +by (simp_tac (simpset() addsimps [diff_diff_left, add_commute]) 1);
   1.178  qed "diff_commute";
   1.179  
   1.180  goal Arith.thy "!!i j k:: nat. k<=j --> j<=i --> i - (j - k) = i - j + k";
   1.181  by (res_inst_tac [("m","i"),("n","j")] diff_induct 1);
   1.182  by (ALLGOALS Asm_simp_tac);
   1.183  by (asm_simp_tac
   1.184 -    (!simpset addsimps [Suc_diff_n, le_imp_less_Suc, le_Suc_eq]) 1);
   1.185 +    (simpset() addsimps [Suc_diff_n, le_imp_less_Suc, le_Suc_eq]) 1);
   1.186  qed_spec_mp "diff_diff_right";
   1.187  
   1.188  goal Arith.thy "!!i j k:: nat. k<=j --> (i + j) - k = i + (j - k)";
   1.189 @@ -405,7 +405,7 @@
   1.190  Addsimps [diff_add_inverse];
   1.191  
   1.192  goal Arith.thy "!!n::nat.(m+n) - n = m";
   1.193 -by (simp_tac (!simpset addsimps [diff_add_assoc]) 1);
   1.194 +by (simp_tac (simpset() addsimps [diff_add_assoc]) 1);
   1.195  qed "diff_add_inverse2";
   1.196  Addsimps [diff_add_inverse2];
   1.197  
   1.198 @@ -417,7 +417,7 @@
   1.199  val [prem] = goal Arith.thy "m < Suc(n) ==> m-n = 0";
   1.200  by (rtac (prem RS rev_mp) 1);
   1.201  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   1.202 -by (asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
   1.203 +by (asm_simp_tac (simpset() addsimps [less_Suc_eq]) 1);
   1.204  by (ALLGOALS Asm_simp_tac);
   1.205  qed "less_imp_diff_is_0";
   1.206  
   1.207 @@ -433,7 +433,7 @@
   1.208  qed "less_imp_diff_positive";
   1.209  
   1.210  goal Arith.thy "Suc(m)-n = (if m<n then 0 else Suc(m-n))";
   1.211 -by (simp_tac (!simpset addsimps [less_imp_diff_is_0, not_less_eq, Suc_diff_n]
   1.212 +by (simp_tac (simpset() addsimps [less_imp_diff_is_0, not_less_eq, Suc_diff_n]
   1.213                         addsplits [expand_if]) 1);
   1.214  qed "if_Suc_diff_n";
   1.215  
   1.216 @@ -456,7 +456,7 @@
   1.217  
   1.218  goal Arith.thy "!!m::nat. (m+k) - (n+k) = m - n";
   1.219  val add_commute_k = read_instantiate [("n","k")] add_commute;
   1.220 -by (asm_simp_tac (!simpset addsimps ([add_commute_k])) 1);
   1.221 +by (asm_simp_tac (simpset() addsimps ([add_commute_k])) 1);
   1.222  qed "diff_cancel2";
   1.223  Addsimps [diff_cancel2];
   1.224  
   1.225 @@ -470,9 +470,9 @@
   1.226  by (subgoal_tac "Suc na <= m --> n <= m --> Suc na <= n --> \
   1.227  \                Suc (m - Suc na) - Suc (n - Suc na) = m-n" 1);
   1.228  by (Asm_full_simp_tac 1);
   1.229 -by (blast_tac (!claset addIs [le_trans]) 1);
   1.230 -by (auto_tac (!claset addIs [Suc_leD], !simpset delsimps [diff_Suc_Suc]));
   1.231 -by (asm_full_simp_tac (!simpset delsimps [Suc_less_eq] 
   1.232 +by (blast_tac (claset() addIs [le_trans]) 1);
   1.233 +by (auto_tac (claset() addIs [Suc_leD], simpset() delsimps [diff_Suc_Suc]));
   1.234 +by (asm_full_simp_tac (simpset() delsimps [Suc_less_eq] 
   1.235  		       addsimps [Suc_diff_n RS sym, le_eq_less_Suc]) 1);
   1.236  qed "diff_right_cancel";
   1.237  
   1.238 @@ -491,7 +491,7 @@
   1.239  
   1.240  goal Arith.thy "!!m::nat. k * (m - n) = (k * m) - (k * n)";
   1.241  val mult_commute_k = read_instantiate [("m","k")] mult_commute;
   1.242 -by (simp_tac (!simpset addsimps [diff_mult_distrib, mult_commute_k]) 1);
   1.243 +by (simp_tac (simpset() addsimps [diff_mult_distrib, mult_commute_k]) 1);
   1.244  qed "diff_mult_distrib2" ;
   1.245  (*NOT added as rewrites, since sometimes they are used from right-to-left*)
   1.246  
   1.247 @@ -500,7 +500,7 @@
   1.248  
   1.249  goal Arith.thy "!!i::nat. i<=j ==> i*k<=j*k";
   1.250  by (induct_tac "k" 1);
   1.251 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [add_le_mono])));
   1.252 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_le_mono])));
   1.253  qed "mult_le_mono1";
   1.254  
   1.255  (*<=monotonicity, BOTH arguments*)
   1.256 @@ -509,7 +509,7 @@
   1.257  by (rtac le_trans 1);
   1.258  by (stac mult_commute 2);
   1.259  by (etac mult_le_mono1 2);
   1.260 -by (simp_tac (!simpset addsimps [mult_commute]) 1);
   1.261 +by (simp_tac (simpset() addsimps [mult_commute]) 1);
   1.262  qed "mult_le_mono";
   1.263  
   1.264  (*strict, in 1st argument; proof is by induction on k>0*)
   1.265 @@ -517,12 +517,12 @@
   1.266  by (eres_inst_tac [("i","0")] less_natE 1);
   1.267  by (Asm_simp_tac 1);
   1.268  by (induct_tac "x" 1);
   1.269 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [add_less_mono])));
   1.270 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_less_mono])));
   1.271  qed "mult_less_mono2";
   1.272  
   1.273  goal Arith.thy "!!i::nat. [| i<j; 0<k |] ==> i*k < j*k";
   1.274  by (dtac mult_less_mono2 1);
   1.275 -by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [mult_commute])));
   1.276 +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [mult_commute])));
   1.277  qed "mult_less_mono1";
   1.278  
   1.279  goal Arith.thy "(0 < m*n) = (0<m & 0<n)";
   1.280 @@ -536,18 +536,18 @@
   1.281  by (Simp_tac 1);
   1.282  by (induct_tac "n" 1);
   1.283  by (Simp_tac 1);
   1.284 -by (fast_tac (!claset addss !simpset) 1);
   1.285 +by (fast_tac (claset() addss simpset()) 1);
   1.286  qed "mult_eq_1_iff";
   1.287  
   1.288  goal Arith.thy "!!k. 0<k ==> (m*k < n*k) = (m<n)";
   1.289 -by (safe_tac (!claset addSIs [mult_less_mono1]));
   1.290 +by (safe_tac (claset() addSIs [mult_less_mono1]));
   1.291  by (cut_facts_tac [less_linear] 1);
   1.292 -by (blast_tac (!claset addDs [mult_less_mono1] addEs [less_asym]) 1);
   1.293 +by (blast_tac (claset() addDs [mult_less_mono1] addEs [less_asym]) 1);
   1.294  qed "mult_less_cancel2";
   1.295  
   1.296  goal Arith.thy "!!k. 0<k ==> (k*m < k*n) = (m<n)";
   1.297  by (dtac mult_less_cancel2 1);
   1.298 -by (asm_full_simp_tac (!simpset addsimps [mult_commute]) 1);
   1.299 +by (asm_full_simp_tac (simpset() addsimps [mult_commute]) 1);
   1.300  qed "mult_less_cancel1";
   1.301  Addsimps [mult_less_cancel1, mult_less_cancel2];
   1.302  
   1.303 @@ -561,7 +561,7 @@
   1.304  
   1.305  goal Arith.thy "!!k. 0<k ==> (k*m = k*n) = (m=n)";
   1.306  by (dtac mult_cancel2 1);
   1.307 -by (asm_full_simp_tac (!simpset addsimps [mult_commute]) 1);
   1.308 +by (asm_full_simp_tac (simpset() addsimps [mult_commute]) 1);
   1.309  qed "mult_cancel1";
   1.310  Addsimps [mult_cancel1, mult_cancel2];
   1.311  
   1.312 @@ -572,9 +572,9 @@
   1.313  by (dtac sym 1);
   1.314  by (rtac disjCI 1);
   1.315  by (rtac nat_less_cases 1 THEN assume_tac 2);
   1.316 -by (fast_tac (!claset addSEs [less_SucE] addss !simpset) 1);
   1.317 -by (best_tac (!claset addDs [mult_less_mono2] 
   1.318 -                      addss (!simpset addsimps [zero_less_eq RS sym])) 1);
   1.319 +by (fast_tac (claset() addSEs [less_SucE] addss simpset()) 1);
   1.320 +by (best_tac (claset() addDs [mult_less_mono2] 
   1.321 +                      addss (simpset() addsimps [zero_less_eq RS sym])) 1);
   1.322  qed "mult_eq_self_implies_10";
   1.323  
   1.324  
   1.325 @@ -584,7 +584,7 @@
   1.326  by (subgoal_tac "c+(a-c) < c+(b-c)" 1);
   1.327  by (Full_simp_tac 1);
   1.328  by (subgoal_tac "c <= b" 1);
   1.329 -by (blast_tac (!claset addIs [less_imp_le, le_trans]) 2);
   1.330 +by (blast_tac (claset() addIs [less_imp_le, le_trans]) 2);
   1.331  by (Asm_simp_tac 1);
   1.332  qed "diff_less_mono";
   1.333  
   1.334 @@ -596,18 +596,18 @@
   1.335  
   1.336  goal Arith.thy "!! n. n <= m ==> Suc m - n = Suc (m - n)";
   1.337  by (rtac Suc_diff_n 1);
   1.338 -by (asm_full_simp_tac (!simpset addsimps [le_eq_less_Suc]) 1);
   1.339 +by (asm_full_simp_tac (simpset() addsimps [le_eq_less_Suc]) 1);
   1.340  qed "Suc_diff_le";
   1.341  
   1.342  goal Arith.thy "!! n. Suc i <= n ==> Suc (n - Suc i) = n - i";
   1.343  by (asm_full_simp_tac
   1.344 -    (!simpset addsimps [Suc_diff_n RS sym, le_eq_less_Suc]) 1);
   1.345 +    (simpset() addsimps [Suc_diff_n RS sym, le_eq_less_Suc]) 1);
   1.346  qed "Suc_diff_Suc";
   1.347  
   1.348  goal Arith.thy "!! i::nat. i <= n ==> n - (n - i) = i";
   1.349  by (etac rev_mp 1);
   1.350  by (res_inst_tac [("m","n"),("n","i")] diff_induct 1);
   1.351 -by (ALLGOALS (asm_simp_tac  (!simpset addsimps [Suc_diff_le])));
   1.352 +by (ALLGOALS (asm_simp_tac  (simpset() addsimps [Suc_diff_le])));
   1.353  qed "diff_diff_cancel";
   1.354  Addsimps [diff_diff_cancel];
   1.355  
   1.356 @@ -615,7 +615,7 @@
   1.357  by (etac rev_mp 1);
   1.358  by (res_inst_tac [("m", "k"), ("n", "n")] diff_induct 1);
   1.359  by (Simp_tac 1);
   1.360 -by (simp_tac (!simpset addsimps [less_add_Suc2, less_imp_le]) 1);
   1.361 +by (simp_tac (simpset() addsimps [less_add_Suc2, less_imp_le]) 1);
   1.362  by (Simp_tac 1);
   1.363  qed "le_add_diff";
   1.364  
   1.365 @@ -626,7 +626,7 @@
   1.366  goal Arith.thy "!!n::nat. m<=n --> (m-l) <= (n-l)";
   1.367  by (induct_tac "n" 1);
   1.368  by (Simp_tac 1);
   1.369 -by (simp_tac (!simpset addsimps [le_Suc_eq]) 1);
   1.370 +by (simp_tac (simpset() addsimps [le_Suc_eq]) 1);
   1.371  by (rtac impI 1);
   1.372  by (etac impE 1);
   1.373  by (atac 1);
   1.374 @@ -640,8 +640,8 @@
   1.375  by (Simp_tac 1);
   1.376  by (case_tac "n <= l" 1);
   1.377  by (subgoal_tac "m <= l" 1);
   1.378 -by (asm_simp_tac (!simpset addsimps [Suc_diff_le]) 1);
   1.379 -by (fast_tac (!claset addEs [le_trans]) 1);
   1.380 +by (asm_simp_tac (simpset() addsimps [Suc_diff_le]) 1);
   1.381 +by (fast_tac (claset() addEs [le_trans]) 1);
   1.382  by (dtac not_leE 1);
   1.383 -by (asm_simp_tac (!simpset addsimps [if_Suc_diff_n]) 1);
   1.384 +by (asm_simp_tac (simpset() addsimps [if_Suc_diff_n]) 1);
   1.385  qed_spec_mp "diff_le_mono2";