src/HOL/Nat.ML
changeset 13450 17fec4798b91
parent 13438 527811f00c56
child 14331 8dbbb7cf3637
     1.1 --- a/src/HOL/Nat.ML	Mon Aug 05 14:27:42 2002 +0200
     1.2 +++ b/src/HOL/Nat.ML	Mon Aug 05 14:27:55 2002 +0200
     1.3 @@ -1,719 +1,243 @@
     1.4  (*  Title:      HOL/Nat.ML
     1.5      ID:         $Id$
     1.6 -    Author:     Lawrence C Paulson and Tobias Nipkow
     1.7 -
     1.8 -Proofs about natural numbers and elementary arithmetic: addition,
     1.9 -multiplication, etc.  Some from the Hoare example from Norbert Galm.
    1.10  *)
    1.11  
    1.12 -(** conversion rules for nat_rec **)
    1.13 +(** legacy ML bindings **)
    1.14  
    1.15 -val [nat_rec_0, nat_rec_Suc] = nat.recs;
    1.16 +structure nat =
    1.17 +struct
    1.18 +  val distinct = thms "nat.distinct";
    1.19 +  val inject = thms "nat.inject";
    1.20 +  val exhaust = thm "nat.exhaust";
    1.21 +  val cases = thms "nat.cases";
    1.22 +  val split = thm "nat.split";
    1.23 +  val split_asm = thm "nat.split_asm";
    1.24 +  val induct = thm "nat.induct";
    1.25 +  val recs = thms "nat.recs";
    1.26 +  val simps = thms "nat.simps";
    1.27 +end;
    1.28 +
    1.29 +val [nat_rec_0, nat_rec_Suc] = thms "nat.recs";
    1.30  bind_thm ("nat_rec_0", nat_rec_0);
    1.31  bind_thm ("nat_rec_Suc", nat_rec_Suc);
    1.32  
    1.33 -(*These 2 rules ease the use of primitive recursion.  NOTE USE OF == *)
    1.34 -val prems = Goal
    1.35 -    "[| !!n. f(n) == nat_rec c h n |] ==> f(0) = c";
    1.36 -by (simp_tac (simpset() addsimps prems) 1);
    1.37 -qed "def_nat_rec_0";
    1.38 -
    1.39 -val prems = Goal
    1.40 -    "[| !!n. f(n) == nat_rec c h n |] ==> f(Suc(n)) = h n (f n)";
    1.41 -by (simp_tac (simpset() addsimps prems) 1);
    1.42 -qed "def_nat_rec_Suc";
    1.43 -
    1.44 -val [nat_case_0, nat_case_Suc] = nat.cases;
    1.45 +val [nat_case_0, nat_case_Suc] = thms "nat.cases";
    1.46  bind_thm ("nat_case_0", nat_case_0);
    1.47  bind_thm ("nat_case_Suc", nat_case_Suc);
    1.48  
    1.49 -Goal "n ~= 0 ==> EX m. n = Suc m";
    1.50 -by (case_tac "n" 1);
    1.51 -by (REPEAT (Blast_tac 1));
    1.52 -qed "not0_implies_Suc";
    1.53 -
    1.54 -Goal "!!n::nat. m<n ==> n ~= 0";
    1.55 -by (case_tac "n" 1);
    1.56 -by (ALLGOALS Asm_full_simp_tac);
    1.57 -qed "gr_implies_not0";
    1.58 -
    1.59 -Goal "!!n::nat. (n ~= 0) = (0 < n)";
    1.60 -by (case_tac "n" 1);
    1.61 -by Auto_tac;
    1.62 -qed "neq0_conv";
    1.63 -AddIffs [neq0_conv];
    1.64 -
    1.65 -(*This theorem is useful with blast_tac: (n=0 ==> False) ==> 0<n *)
    1.66 -bind_thm ("gr0I", [neq0_conv, notI] MRS iffD1);
    1.67 -
    1.68 -Goal "(0<n) = (EX m. n = Suc m)";
    1.69 -by (fast_tac (claset() addIs [not0_implies_Suc]) 1);
    1.70 -qed "gr0_conv_Suc";
    1.71 -
    1.72 -Goal "!!n::nat. (~(0 < n)) = (n=0)";
    1.73 -by (rtac iffI 1);
    1.74 - by (rtac ccontr 1);
    1.75 - by (ALLGOALS Asm_full_simp_tac);
    1.76 -qed "not_gr0";
    1.77 -AddIffs [not_gr0];
    1.78 -
    1.79 -Goal "(Suc n <= m') --> (? m. m' = Suc m)";
    1.80 -by (induct_tac "m'" 1);
    1.81 -by  Auto_tac;
    1.82 -qed_spec_mp "Suc_le_D";
    1.83 -
    1.84 -(*Useful in certain inductive arguments*)
    1.85 -Goal "(m < Suc n) = (m=0 | (EX j. m = Suc j & j < n))";
    1.86 -by (case_tac "m" 1);
    1.87 -by Auto_tac;
    1.88 -qed "less_Suc_eq_0_disj";
    1.89 -
    1.90 -val prems = Goal "[| P 0; P(Suc 0); !!k. P k ==> P (Suc (Suc k)) |] ==> P n";
    1.91 -by (rtac nat_less_induct 1);
    1.92 -by (case_tac "n" 1);
    1.93 -by (case_tac "nat" 2);
    1.94 -by (ALLGOALS (blast_tac (claset() addIs prems@[less_trans])));
    1.95 -qed "nat_induct2";
    1.96 -
    1.97 -(** LEAST theorems for type "nat" by specialization **)
    1.98 -
    1.99 -bind_thm("LeastI", wellorder_LeastI);
   1.100 -bind_thm("Least_le", wellorder_Least_le);
   1.101 -bind_thm("not_less_Least", wellorder_not_less_Least);
   1.102 -
   1.103 -Goal "[| P n; ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))";
   1.104 -by (case_tac "n" 1);
   1.105 -by Auto_tac;  
   1.106 -by (ftac LeastI 1); 
   1.107 -by (dres_inst_tac [("P","%x. P (Suc x)")] LeastI 1);
   1.108 -by (subgoal_tac "(LEAST x. P x) <= Suc (LEAST x. P (Suc x))" 1); 
   1.109 -by (etac Least_le 2); 
   1.110 -by (case_tac "LEAST x. P x" 1);
   1.111 -by Auto_tac;  
   1.112 -by (dres_inst_tac [("P","%x. P (Suc x)")] Least_le 1);
   1.113 -by (blast_tac (claset() addIs [order_antisym]) 1); 
   1.114 -qed "Least_Suc";
   1.115 -
   1.116 -Goal "[|P n; Q m; ~P 0; !k. P (Suc k) = Q k|] ==> Least P = Suc (Least Q)";
   1.117 -by (eatac (Least_Suc RS ssubst) 1 1);
   1.118 -by (Asm_simp_tac 1);
   1.119 -qed "Least_Suc2";
   1.120 -
   1.121 -
   1.122 -(** min and max **)
   1.123 -
   1.124 -Goal "min 0 n = (0::nat)";
   1.125 -by (rtac min_leastL 1);
   1.126 -by (Simp_tac 1);
   1.127 -qed "min_0L";
   1.128 -
   1.129 -Goal "min n 0 = (0::nat)";
   1.130 -by (rtac min_leastR 1);
   1.131 -by (Simp_tac 1);
   1.132 -qed "min_0R";
   1.133 -
   1.134 -Goal "min (Suc m) (Suc n) = Suc (min m n)";
   1.135 -by (simp_tac (simpset() addsimps [min_of_mono]) 1);
   1.136 -qed "min_Suc_Suc";
   1.137 -
   1.138 -Addsimps [min_0L,min_0R,min_Suc_Suc];
   1.139 -
   1.140 -Goal "max 0 n = (n::nat)";
   1.141 -by (rtac max_leastL 1);
   1.142 -by (Simp_tac 1);
   1.143 -qed "max_0L";
   1.144 -
   1.145 -Goal "max n 0 = (n::nat)";
   1.146 -by (rtac max_leastR 1);
   1.147 -by (Simp_tac 1);
   1.148 -qed "max_0R";
   1.149 -
   1.150 -Goal "max (Suc m) (Suc n) = Suc(max m n)";
   1.151 -by (simp_tac (simpset() addsimps [max_of_mono]) 1);
   1.152 -qed "max_Suc_Suc";
   1.153 -
   1.154 -Addsimps [max_0L,max_0R,max_Suc_Suc];
   1.155 -
   1.156 -
   1.157 -(*** Basic rewrite rules for the arithmetic operators ***)
   1.158 -
   1.159 -(** Difference **)
   1.160 -
   1.161 -Goal "0 - n = (0::nat)";
   1.162 -by (induct_tac "n" 1);
   1.163 -by (ALLGOALS Asm_simp_tac);
   1.164 -qed "diff_0_eq_0";
   1.165 -
   1.166 -(*Must simplify BEFORE the induction!  (Else we get a critical pair)
   1.167 -  Suc(m) - Suc(n)   rewrites to   pred(Suc(m) - n)  *)
   1.168 -Goal "Suc(m) - Suc(n) = m - n";
   1.169 -by (Simp_tac 1);
   1.170 -by (induct_tac "n" 1);
   1.171 -by (ALLGOALS Asm_simp_tac);
   1.172 -qed "diff_Suc_Suc";
   1.173 -
   1.174 -Addsimps [diff_0_eq_0, diff_Suc_Suc];
   1.175 -
   1.176 -(* Could be (and is, below) generalized in various ways;
   1.177 -   However, none of the generalizations are currently in the simpset,
   1.178 -   and I dread to think what happens if I put them in *)
   1.179 -Goal "0 < n ==> Suc(n - Suc 0) = n";
   1.180 -by (asm_simp_tac (simpset() addsplits [nat.split]) 1);
   1.181 -qed "Suc_pred";
   1.182 -Addsimps [Suc_pred];
   1.183 -
   1.184 -Delsimps [diff_Suc];
   1.185 -
   1.186 -
   1.187 -(**** Inductive properties of the operators ****)
   1.188 -
   1.189 -(*** Addition ***)
   1.190 -
   1.191 -Goal "m + 0 = (m::nat)";
   1.192 -by (induct_tac "m" 1);
   1.193 -by (ALLGOALS Asm_simp_tac);
   1.194 -qed "add_0_right";
   1.195 -
   1.196 -Goal "m + Suc(n) = Suc(m+n)";
   1.197 -by (induct_tac "m" 1);
   1.198 -by (ALLGOALS Asm_simp_tac);
   1.199 -qed "add_Suc_right";
   1.200 -
   1.201 -Addsimps [add_0_right,add_Suc_right];
   1.202 -
   1.203 -
   1.204 -(*Associative law for addition*)
   1.205 -Goal "(m + n) + k = m + ((n + k)::nat)";
   1.206 -by (induct_tac "m" 1);
   1.207 -by (ALLGOALS Asm_simp_tac);
   1.208 -qed "add_assoc";
   1.209 -
   1.210 -(*Commutative law for addition*)
   1.211 -Goal "m + n = n + (m::nat)";
   1.212 -by (induct_tac "m" 1);
   1.213 -by (ALLGOALS Asm_simp_tac);
   1.214 -qed "add_commute";
   1.215 -
   1.216 -Goal "x+(y+z)=y+((x+z)::nat)";
   1.217 -by(rtac ([add_assoc,add_commute] MRS
   1.218 -         read_instantiate[("f","op +")](thm"mk_left_commute")) 1);
   1.219 -qed "add_left_commute";
   1.220 -
   1.221 -(*Addition is an AC-operator*)
   1.222 -bind_thms ("add_ac", [add_assoc, add_commute, add_left_commute]);
   1.223 -
   1.224 -Goal "(k + m = k + n) = (m=(n::nat))";
   1.225 -by (induct_tac "k" 1);
   1.226 -by (Simp_tac 1);
   1.227 -by (Asm_simp_tac 1);
   1.228 -qed "add_left_cancel";
   1.229 -
   1.230 -Goal "(m + k = n + k) = (m=(n::nat))";
   1.231 -by (induct_tac "k" 1);
   1.232 -by (Simp_tac 1);
   1.233 -by (Asm_simp_tac 1);
   1.234 -qed "add_right_cancel";
   1.235 -
   1.236 -Goal "(k + m <= k + n) = (m<=(n::nat))";
   1.237 -by (induct_tac "k" 1);
   1.238 -by (Simp_tac 1);
   1.239 -by (Asm_simp_tac 1);
   1.240 -qed "add_left_cancel_le";
   1.241 -
   1.242 -Goal "(k + m < k + n) = (m<(n::nat))";
   1.243 -by (induct_tac "k" 1);
   1.244 -by (Simp_tac 1);
   1.245 -by (Asm_simp_tac 1);
   1.246 -qed "add_left_cancel_less";
   1.247 -
   1.248 -Addsimps [add_left_cancel, add_right_cancel,
   1.249 -          add_left_cancel_le, add_left_cancel_less];
   1.250 -
   1.251 -(** Reasoning about m+0=0, etc. **)
   1.252 -
   1.253 -Goal "!!m::nat. (m+n = 0) = (m=0 & n=0)";
   1.254 -by (case_tac "m" 1);
   1.255 -by (Auto_tac);
   1.256 -qed "add_is_0";
   1.257 -AddIffs [add_is_0];
   1.258 -
   1.259 -Goal "(m+n= Suc 0) = (m= Suc 0 & n=0 | m=0 & n= Suc 0)";
   1.260 -by (case_tac "m" 1);
   1.261 -by (Auto_tac);
   1.262 -qed "add_is_1";
   1.263 -
   1.264 -Goal "(Suc 0 = m+n) = (m = Suc 0 & n=0 | m=0 & n = Suc 0)";
   1.265 -by (rtac ([eq_commute, add_is_1] MRS trans) 1);
   1.266 -qed "one_is_add";
   1.267 -
   1.268 -Goal "!!m::nat. (0<m+n) = (0<m | 0<n)";
   1.269 -by (simp_tac (simpset() delsimps [neq0_conv] addsimps [neq0_conv RS sym]) 1);
   1.270 -qed "add_gr_0";
   1.271 -AddIffs [add_gr_0];
   1.272 -
   1.273 -Goal "!!m::nat. m + n = m ==> n = 0";
   1.274 -by (dtac (add_0_right RS ssubst) 1);
   1.275 -by (asm_full_simp_tac (simpset() addsimps [add_assoc]
   1.276 -                                 delsimps [add_0_right]) 1);
   1.277 -qed "add_eq_self_zero";
   1.278 -
   1.279 -(**** Additional theorems about "less than" ****)
   1.280 -
   1.281 -(*Deleted less_natE; instead use less_imp_Suc_add RS exE*)
   1.282 -Goal "m<n --> (EX k. n=Suc(m+k))";
   1.283 -by (induct_tac "n" 1);
   1.284 -by (ALLGOALS (simp_tac (simpset() addsimps [order_le_less])));
   1.285 -by (blast_tac (claset() addSEs [less_SucE]
   1.286 -                        addSIs [add_0_right RS sym, add_Suc_right RS sym]) 1);
   1.287 -qed_spec_mp "less_imp_Suc_add";
   1.288 -
   1.289 -Goal "n <= ((m + n)::nat)";
   1.290 -by (induct_tac "m" 1);
   1.291 -by (ALLGOALS Simp_tac);
   1.292 -by (etac le_SucI 1);
   1.293 -qed "le_add2";
   1.294 -
   1.295 -Goal "n <= ((n + m)::nat)";
   1.296 -by (simp_tac (simpset() addsimps add_ac) 1);
   1.297 -by (rtac le_add2 1);
   1.298 -qed "le_add1";
   1.299 -
   1.300 -bind_thm ("less_add_Suc1", (lessI RS (le_add1 RS le_less_trans)));
   1.301 -bind_thm ("less_add_Suc2", (lessI RS (le_add2 RS le_less_trans)));
   1.302 -
   1.303 -Goal "(m<n) = (EX k. n=Suc(m+k))";
   1.304 -by (blast_tac (claset() addSIs [less_add_Suc1, less_imp_Suc_add]) 1);
   1.305 -qed "less_iff_Suc_add";
   1.306 -
   1.307 -
   1.308 -(*"i <= j ==> i <= j+m"*)
   1.309 -bind_thm ("trans_le_add1", le_add1 RSN (2,le_trans));
   1.310 -
   1.311 -(*"i <= j ==> i <= m+j"*)
   1.312 -bind_thm ("trans_le_add2", le_add2 RSN (2,le_trans));
   1.313 -
   1.314 -(*"i < j ==> i < j+m"*)
   1.315 -bind_thm ("trans_less_add1", le_add1 RSN (2,less_le_trans));
   1.316 -
   1.317 -(*"i < j ==> i < m+j"*)
   1.318 -bind_thm ("trans_less_add2", le_add2 RSN (2,less_le_trans));
   1.319 -
   1.320 -Goal "i+j < (k::nat) --> i<k";
   1.321 -by (induct_tac "j" 1);
   1.322 -by (ALLGOALS Asm_simp_tac);
   1.323 -by (blast_tac (claset() addDs [Suc_lessD]) 1);
   1.324 -qed_spec_mp "add_lessD1";
   1.325 -
   1.326 -Goal "~ (i+j < (i::nat))";
   1.327 -by (rtac notI 1);
   1.328 -by (etac (add_lessD1 RS less_irrefl) 1);
   1.329 -qed "not_add_less1";
   1.330 -
   1.331 -Goal "~ (j+i < (i::nat))";
   1.332 -by (simp_tac (simpset() addsimps [add_commute, not_add_less1]) 1);
   1.333 -qed "not_add_less2";
   1.334 -AddIffs [not_add_less1, not_add_less2];
   1.335 -
   1.336 -Goal "m+k<=n --> m<=(n::nat)";
   1.337 -by (induct_tac "k" 1);
   1.338 -by (ALLGOALS (asm_simp_tac (simpset() addsimps le_simps)));
   1.339 -qed_spec_mp "add_leD1";
   1.340 -
   1.341 -Goal "m+k<=n ==> k<=(n::nat)";
   1.342 -by (full_simp_tac (simpset() addsimps [add_commute]) 1);
   1.343 -by (etac add_leD1 1);
   1.344 -qed_spec_mp "add_leD2";
   1.345 -
   1.346 -Goal "m+k<=n ==> m<=n & k<=(n::nat)";
   1.347 -by (blast_tac (claset() addDs [add_leD1, add_leD2]) 1);
   1.348 -bind_thm ("add_leE", result() RS conjE);
   1.349 -
   1.350 -(*needs !!k for add_ac to work*)
   1.351 -Goal "!!k:: nat. [| k<l;  m+l = k+n |] ==> m<n";
   1.352 -by (force_tac (claset(),
   1.353 -              simpset() delsimps [add_Suc_right]
   1.354 -                        addsimps [less_iff_Suc_add,
   1.355 -                                  add_Suc_right RS sym] @ add_ac) 1);
   1.356 -qed "less_add_eq_less";
   1.357 -
   1.358 -
   1.359 -(*** Monotonicity of Addition ***)
   1.360 -
   1.361 -(*strict, in 1st argument*)
   1.362 -Goal "i < j ==> i + k < j + (k::nat)";
   1.363 -by (induct_tac "k" 1);
   1.364 -by (ALLGOALS Asm_simp_tac);
   1.365 -qed "add_less_mono1";
   1.366 -
   1.367 -(*strict, in both arguments*)
   1.368 -Goal "[|i < j; k < l|] ==> i + k < j + (l::nat)";
   1.369 -by (rtac (add_less_mono1 RS less_trans) 1);
   1.370 -by (REPEAT (assume_tac 1));
   1.371 -by (induct_tac "j" 1);
   1.372 -by (ALLGOALS Asm_simp_tac);
   1.373 -qed "add_less_mono";
   1.374 -
   1.375 -(*A [clumsy] way of lifting < monotonicity to <= monotonicity *)
   1.376 -val [lt_mono,le] = Goal
   1.377 -     "[| !!i j::nat. i<j ==> f(i) < f(j);       \
   1.378 -\        i <= j                                 \
   1.379 -\     |] ==> f(i) <= (f(j)::nat)";
   1.380 -by (cut_facts_tac [le] 1);
   1.381 -by (asm_full_simp_tac (simpset() addsimps [order_le_less]) 1);
   1.382 -by (blast_tac (claset() addSIs [lt_mono]) 1);
   1.383 -qed "less_mono_imp_le_mono";
   1.384 -
   1.385 -(*non-strict, in 1st argument*)
   1.386 -Goal "i<=j ==> i + k <= j + (k::nat)";
   1.387 -by (res_inst_tac [("f", "%j. j+k")] less_mono_imp_le_mono 1);
   1.388 -by (etac add_less_mono1 1);
   1.389 -by (assume_tac 1);
   1.390 -qed "add_le_mono1";
   1.391 -
   1.392 -(*non-strict, in both arguments*)
   1.393 -Goal "[|i<=j;  k<=l |] ==> i + k <= j + (l::nat)";
   1.394 -by (etac (add_le_mono1 RS le_trans) 1);
   1.395 -by (simp_tac (simpset() addsimps [add_commute]) 1);
   1.396 -qed "add_le_mono";
   1.397 -
   1.398 -
   1.399 -(*** Multiplication ***)
   1.400 -
   1.401 -(*right annihilation in product*)
   1.402 -Goal "!!m::nat. m * 0 = 0";
   1.403 -by (induct_tac "m" 1);
   1.404 -by (ALLGOALS Asm_simp_tac);
   1.405 -qed "mult_0_right";
   1.406 -
   1.407 -(*right successor law for multiplication*)
   1.408 -Goal  "m * Suc(n) = m + (m * n)";
   1.409 -by (induct_tac "m" 1);
   1.410 -by (ALLGOALS(asm_simp_tac (simpset() addsimps add_ac)));
   1.411 -qed "mult_Suc_right";
   1.412 -
   1.413 -Addsimps [mult_0_right, mult_Suc_right];
   1.414 -
   1.415 -Goal "(1::nat) * n = n";
   1.416 -by (Asm_simp_tac 1);
   1.417 -qed "mult_1";
   1.418 -
   1.419 -Goal "n * (1::nat) = n";
   1.420 -by (Asm_simp_tac 1);
   1.421 -qed "mult_1_right";
   1.422 -
   1.423 -(*Commutative law for multiplication*)
   1.424 -Goal "m * n = n * (m::nat)";
   1.425 -by (induct_tac "m" 1);
   1.426 -by (ALLGOALS Asm_simp_tac);
   1.427 -qed "mult_commute";
   1.428 -
   1.429 -(*addition distributes over multiplication*)
   1.430 -Goal "(m + n)*k = (m*k) + ((n*k)::nat)";
   1.431 -by (induct_tac "m" 1);
   1.432 -by (ALLGOALS(asm_simp_tac (simpset() addsimps add_ac)));
   1.433 -qed "add_mult_distrib";
   1.434 -
   1.435 -Goal "k*(m + n) = (k*m) + ((k*n)::nat)";
   1.436 -by (induct_tac "m" 1);
   1.437 -by (ALLGOALS(asm_simp_tac (simpset() addsimps add_ac)));
   1.438 -qed "add_mult_distrib2";
   1.439 -
   1.440 -(*Associative law for multiplication*)
   1.441 -Goal "(m * n) * k = m * ((n * k)::nat)";
   1.442 -by (induct_tac "m" 1);
   1.443 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_mult_distrib])));
   1.444 -qed "mult_assoc";
   1.445 -
   1.446 -Goal "x*(y*z) = y*((x*z)::nat)";
   1.447 -by(rtac ([mult_assoc,mult_commute] MRS
   1.448 -         read_instantiate[("f","op *")](thm"mk_left_commute")) 1);
   1.449 -qed "mult_left_commute";
   1.450 -
   1.451 -bind_thms ("mult_ac", [mult_assoc,mult_commute,mult_left_commute]);
   1.452 -
   1.453 -Goal "!!m::nat. (m*n = 0) = (m=0 | n=0)";
   1.454 -by (induct_tac "m" 1);
   1.455 -by (induct_tac "n" 2);
   1.456 -by (ALLGOALS Asm_simp_tac);
   1.457 -qed "mult_is_0";
   1.458 -Addsimps [mult_is_0];
   1.459 -
   1.460 -
   1.461 -(*** Difference ***)
   1.462 -
   1.463 -Goal "!!m::nat. m - m = 0";
   1.464 -by (induct_tac "m" 1);
   1.465 -by (ALLGOALS Asm_simp_tac);
   1.466 -qed "diff_self_eq_0";
   1.467 -
   1.468 -Addsimps [diff_self_eq_0];
   1.469 -
   1.470 -(*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
   1.471 -Goal "~ m<n --> n+(m-n) = (m::nat)";
   1.472 -by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   1.473 -by (ALLGOALS Asm_simp_tac);
   1.474 -qed_spec_mp "add_diff_inverse";
   1.475 -
   1.476 -Goal "n<=m ==> n+(m-n) = (m::nat)";
   1.477 -by (asm_simp_tac (simpset() addsimps [add_diff_inverse, not_less_iff_le]) 1);
   1.478 -qed "le_add_diff_inverse";
   1.479 -
   1.480 -Goal "n<=m ==> (m-n)+n = (m::nat)";
   1.481 -by (asm_simp_tac (simpset() addsimps [le_add_diff_inverse, add_commute]) 1);
   1.482 -qed "le_add_diff_inverse2";
   1.483 -
   1.484 -Addsimps  [le_add_diff_inverse, le_add_diff_inverse2];
   1.485 -
   1.486 -
   1.487 -(*** More results about difference ***)
   1.488 -
   1.489 -Goal "n <= m ==> Suc(m)-n = Suc(m-n)";
   1.490 -by (etac rev_mp 1);
   1.491 -by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   1.492 -by (ALLGOALS Asm_simp_tac);
   1.493 -qed "Suc_diff_le";
   1.494 -
   1.495 -Goal "m - n < Suc(m)";
   1.496 -by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   1.497 -by (etac less_SucE 3);
   1.498 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq])));
   1.499 -qed "diff_less_Suc";
   1.500 -
   1.501 -Goal "m - n <= (m::nat)";
   1.502 -by (res_inst_tac [("m","m"), ("n","n")] diff_induct 1);
   1.503 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [le_SucI])));
   1.504 -qed "diff_le_self";
   1.505 -Addsimps [diff_le_self];
   1.506 -
   1.507 -(* j<k ==> j-n < k *)
   1.508 -bind_thm ("less_imp_diff_less", diff_le_self RS le_less_trans);
   1.509 -
   1.510 -Goal "!!i::nat. i-j-k = i - (j+k)";
   1.511 -by (res_inst_tac [("m","i"),("n","j")] diff_induct 1);
   1.512 -by (ALLGOALS Asm_simp_tac);
   1.513 -qed "diff_diff_left";
   1.514 -
   1.515 -Goal "(Suc m - n) - Suc k = m - n - k";
   1.516 -by (simp_tac (simpset() addsimps [diff_diff_left]) 1);
   1.517 -qed "Suc_diff_diff";
   1.518 -Addsimps [Suc_diff_diff];
   1.519 -
   1.520 -Goal "0<n ==> n - Suc i < n";
   1.521 -by (case_tac "n" 1);
   1.522 -by Safe_tac;
   1.523 -by (asm_simp_tac (simpset() addsimps le_simps) 1);
   1.524 -qed "diff_Suc_less";
   1.525 -Addsimps [diff_Suc_less];
   1.526 -
   1.527 -(*This and the next few suggested by Florian Kammueller*)
   1.528 -Goal "!!i::nat. i-j-k = i-k-j";
   1.529 -by (simp_tac (simpset() addsimps [diff_diff_left, add_commute]) 1);
   1.530 -qed "diff_commute";
   1.531 -
   1.532 -Goal "k <= (j::nat) --> (i + j) - k = i + (j - k)";
   1.533 -by (res_inst_tac [("m","j"),("n","k")] diff_induct 1);
   1.534 -by (ALLGOALS Asm_simp_tac);
   1.535 -qed_spec_mp "diff_add_assoc";
   1.536 -
   1.537 -Goal "k <= (j::nat) --> (j + i) - k = (j - k) + i";
   1.538 -by (asm_simp_tac (simpset() addsimps [add_commute, diff_add_assoc]) 1);
   1.539 -qed_spec_mp "diff_add_assoc2";
   1.540 -
   1.541 -Goal "(n+m) - n = (m::nat)";
   1.542 -by (induct_tac "n" 1);
   1.543 -by (ALLGOALS Asm_simp_tac);
   1.544 -qed "diff_add_inverse";
   1.545 -
   1.546 -Goal "(m+n) - n = (m::nat)";
   1.547 -by (simp_tac (simpset() addsimps [diff_add_assoc]) 1);
   1.548 -qed "diff_add_inverse2";
   1.549 -
   1.550 -Goal "i <= (j::nat) ==> (j-i=k) = (j=k+i)";
   1.551 -by Safe_tac;
   1.552 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_add_inverse2])));
   1.553 -qed "le_imp_diff_is_add";
   1.554 -
   1.555 -Goal "!!m::nat. (m-n = 0) = (m <= n)";
   1.556 -by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   1.557 -by (ALLGOALS Asm_simp_tac);
   1.558 -qed "diff_is_0_eq";
   1.559 -Addsimps [diff_is_0_eq, diff_is_0_eq RS iffD2];
   1.560 -
   1.561 -Goal "!!m::nat. (0<n-m) = (m<n)";
   1.562 -by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   1.563 -by (ALLGOALS Asm_simp_tac);
   1.564 -qed "zero_less_diff";
   1.565 -Addsimps [zero_less_diff];
   1.566 -
   1.567 -Goal "i < j  ==> EX k::nat. 0<k & i+k = j";
   1.568 -by (res_inst_tac [("x","j - i")] exI 1);
   1.569 -by (asm_simp_tac (simpset() addsimps [add_diff_inverse, less_not_sym]) 1);
   1.570 -qed "less_imp_add_positive";
   1.571 -
   1.572 -Goal "P(k) --> (ALL n. P(Suc(n))--> P(n)) --> P(k-i)";
   1.573 -by (res_inst_tac [("m","k"),("n","i")] diff_induct 1);
   1.574 -by (ALLGOALS (Clarify_tac THEN' Simp_tac THEN' TRY o Blast_tac));
   1.575 -qed "zero_induct_lemma";
   1.576 -
   1.577 -val prems = Goal "[| P(k);  !!n. P(Suc(n)) ==> P(n) |] ==> P(0)";
   1.578 -by (rtac (diff_self_eq_0 RS subst) 1);
   1.579 -by (rtac (zero_induct_lemma RS mp RS mp) 1);
   1.580 -by (REPEAT (ares_tac ([impI,allI]@prems) 1));
   1.581 -qed "zero_induct";
   1.582 -
   1.583 -Goal "(k+m) - (k+n) = m - (n::nat)";
   1.584 -by (induct_tac "k" 1);
   1.585 -by (ALLGOALS Asm_simp_tac);
   1.586 -qed "diff_cancel";
   1.587 -
   1.588 -Goal "(m+k) - (n+k) = m - (n::nat)";
   1.589 -by (asm_simp_tac
   1.590 -    (simpset() addsimps [diff_cancel, inst "n" "k" add_commute]) 1);
   1.591 -qed "diff_cancel2";
   1.592 -
   1.593 -Goal "n - (n+m) = (0::nat)";
   1.594 -by (induct_tac "n" 1);
   1.595 -by (ALLGOALS Asm_simp_tac);
   1.596 -qed "diff_add_0";
   1.597 -
   1.598 -
   1.599 -(** Difference distributes over multiplication **)
   1.600 -
   1.601 -Goal "!!m::nat. (m - n) * k = (m * k) - (n * k)";
   1.602 -by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   1.603 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_cancel])));
   1.604 -qed "diff_mult_distrib" ;
   1.605 -
   1.606 -Goal "!!m::nat. k * (m - n) = (k * m) - (k * n)";
   1.607 -val mult_commute_k = read_instantiate [("m","k")] mult_commute;
   1.608 -by (simp_tac (simpset() addsimps [diff_mult_distrib, mult_commute_k]) 1);
   1.609 -qed "diff_mult_distrib2" ;
   1.610 -(*NOT added as rewrites, since sometimes they are used from right-to-left*)
   1.611 -
   1.612 -bind_thms ("nat_distrib",
   1.613 -  [add_mult_distrib, add_mult_distrib2, diff_mult_distrib, diff_mult_distrib2]);
   1.614 -
   1.615 -
   1.616 -(*** Monotonicity of Multiplication ***)
   1.617 -
   1.618 -Goal "i <= (j::nat) ==> i*k<=j*k";
   1.619 -by (induct_tac "k" 1);
   1.620 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_le_mono])));
   1.621 -qed "mult_le_mono1";
   1.622 -
   1.623 -Goal "i <= (j::nat) ==> k*i <= k*j";
   1.624 -by (dtac mult_le_mono1 1);
   1.625 -by (asm_simp_tac (simpset() addsimps [mult_commute]) 1);
   1.626 -qed "mult_le_mono2";
   1.627 -
   1.628 -(* <= monotonicity, BOTH arguments*)
   1.629 -Goal "[| i <= (j::nat); k <= l |] ==> i*k <= j*l";
   1.630 -by (etac (mult_le_mono1 RS le_trans) 1);
   1.631 -by (etac mult_le_mono2 1);
   1.632 -qed "mult_le_mono";
   1.633 -
   1.634 -(*strict, in 1st argument; proof is by induction on k>0*)
   1.635 -Goal "!!i::nat. [| i<j; 0<k |] ==> k*i < k*j";
   1.636 -by (eres_inst_tac [("m1","0")] (less_imp_Suc_add RS exE) 1);
   1.637 -by (Asm_simp_tac 1);
   1.638 -by (induct_tac "x" 1);
   1.639 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_less_mono])));
   1.640 -qed "mult_less_mono2";
   1.641 -
   1.642 -Goal "!!i::nat. [| i<j; 0<k |] ==> i*k < j*k";
   1.643 -by (dtac mult_less_mono2 1);
   1.644 -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [mult_commute])));
   1.645 -qed "mult_less_mono1";
   1.646 -
   1.647 -Goal "!!m::nat. (0 < m*n) = (0<m & 0<n)";
   1.648 -by (induct_tac "m" 1);
   1.649 -by (case_tac "n" 2);
   1.650 -by (ALLGOALS Asm_simp_tac);
   1.651 -qed "zero_less_mult_iff";
   1.652 -Addsimps [zero_less_mult_iff];
   1.653 -
   1.654 -Goal "(Suc 0 <= m*n) = (1<=m & 1<=n)";
   1.655 -by (induct_tac "m" 1);
   1.656 -by (case_tac "n" 2);
   1.657 -by (ALLGOALS Asm_simp_tac);
   1.658 -qed "one_le_mult_iff";
   1.659 -Addsimps [one_le_mult_iff];
   1.660 -
   1.661 -Goal "(m*n = Suc 0) = (m=1 & n=1)";
   1.662 -by (induct_tac "m" 1);
   1.663 -by (Simp_tac 1);
   1.664 -by (induct_tac "n" 1);
   1.665 -by (Simp_tac 1);
   1.666 -by (fast_tac (claset() addss simpset()) 1);
   1.667 -qed "mult_eq_1_iff";
   1.668 -Addsimps [mult_eq_1_iff];
   1.669 -
   1.670 -Goal "(Suc 0 = m*n) = (m=1 & n=1)";
   1.671 -by (rtac (mult_eq_1_iff RSN (2,trans)) 1);
   1.672 -by (fast_tac (claset() addss simpset()) 1);
   1.673 -qed "one_eq_mult_iff";
   1.674 -Addsimps [one_eq_mult_iff];
   1.675 -
   1.676 -Goal "!!m::nat. (m*k < n*k) = (0<k & m<n)";
   1.677 -by (safe_tac (claset() addSIs [mult_less_mono1]));
   1.678 -by (case_tac "k" 1);
   1.679 -by Auto_tac;  
   1.680 -by (full_simp_tac (simpset() delsimps [le_0_eq]
   1.681 -			     addsimps [linorder_not_le RS sym]) 1);
   1.682 -by (blast_tac (claset() addIs [mult_le_mono1]) 1); 
   1.683 -qed "mult_less_cancel2";
   1.684 -
   1.685 -Goal "!!m::nat. (k*m < k*n) = (0<k & m<n)";
   1.686 -by (simp_tac (simpset() addsimps [mult_less_cancel2, 
   1.687 -                                  inst "m" "k" mult_commute]) 1);
   1.688 -qed "mult_less_cancel1";
   1.689 -Addsimps [mult_less_cancel1, mult_less_cancel2];
   1.690 -
   1.691 -Goal "!!m::nat. (m*k <= n*k) = (0<k --> m<=n)";
   1.692 -by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
   1.693 -by Auto_tac;  
   1.694 -qed "mult_le_cancel2";
   1.695 -
   1.696 -Goal "!!m::nat. (k*m <= k*n) = (0<k --> m<=n)";
   1.697 -by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
   1.698 -by Auto_tac;  
   1.699 -qed "mult_le_cancel1";
   1.700 -Addsimps [mult_le_cancel1, mult_le_cancel2];
   1.701 -
   1.702 -Goal "(m*k = n*k) = (m=n | (k = (0::nat)))";
   1.703 -by (cut_facts_tac [less_linear] 1);
   1.704 -by Safe_tac;
   1.705 -by Auto_tac; 	
   1.706 -by (ALLGOALS (dtac mult_less_mono1 THEN' assume_tac));
   1.707 -by (ALLGOALS Asm_full_simp_tac);
   1.708 -qed "mult_cancel2";
   1.709 -
   1.710 -Goal "(k*m = k*n) = (m=n | (k = (0::nat)))";
   1.711 -by (simp_tac (simpset() addsimps [mult_cancel2, inst "m" "k" mult_commute]) 1);
   1.712 -qed "mult_cancel1";
   1.713 -Addsimps [mult_cancel1, mult_cancel2];
   1.714 -
   1.715 -Goal "(Suc k * m < Suc k * n) = (m < n)";
   1.716 -by (stac mult_less_cancel1 1);
   1.717 -by (Simp_tac 1);
   1.718 -qed "Suc_mult_less_cancel1";
   1.719 -
   1.720 -Goal "(Suc k * m <= Suc k * n) = (m <= n)";
   1.721 -by (stac mult_le_cancel1 1);
   1.722 -by (Simp_tac 1);
   1.723 -qed "Suc_mult_le_cancel1";
   1.724 -
   1.725 -Goal "(Suc k * m = Suc k * n) = (m = n)";
   1.726 -by (stac mult_cancel1 1);
   1.727 -by (Simp_tac 1);
   1.728 -qed "Suc_mult_cancel1";
   1.729 -
   1.730 -
   1.731 -(*Lemma for gcd*)
   1.732 -Goal "!!m::nat. m = m*n ==> n=1 | m=0";
   1.733 -by (dtac sym 1);
   1.734 -by (rtac disjCI 1);
   1.735 -by (rtac nat_less_cases 1 THEN assume_tac 2);
   1.736 -by (fast_tac (claset() addSEs [less_SucE] addss simpset()) 1);
   1.737 -by (best_tac (claset() addDs [mult_less_mono2] addss simpset()) 1);
   1.738 -qed "mult_eq_self_implies_10";
   1.739 +val LeastI = thm "LeastI";
   1.740 +val Least_Suc = thm "Least_Suc";
   1.741 +val Least_Suc2 = thm "Least_Suc2";
   1.742 +val Least_le = thm "Least_le";
   1.743 +val One_nat_def = thm "One_nat_def";
   1.744 +val Suc_Suc_eq = thm "Suc_Suc_eq";
   1.745 +val Suc_def = thm "Suc_def";
   1.746 +val Suc_diff_diff = thm "Suc_diff_diff";
   1.747 +val Suc_diff_le = thm "Suc_diff_le";
   1.748 +val Suc_inject = thm "Suc_inject";
   1.749 +val Suc_leD = thm "Suc_leD";
   1.750 +val Suc_leI = thm "Suc_leI";
   1.751 +val Suc_le_D = thm "Suc_le_D";
   1.752 +val Suc_le_eq = thm "Suc_le_eq";
   1.753 +val Suc_le_lessD = thm "Suc_le_lessD";
   1.754 +val Suc_le_mono = thm "Suc_le_mono";
   1.755 +val Suc_lessD = thm "Suc_lessD";
   1.756 +val Suc_lessE = thm "Suc_lessE";
   1.757 +val Suc_lessI = thm "Suc_lessI";
   1.758 +val Suc_less_SucD = thm "Suc_less_SucD";
   1.759 +val Suc_less_eq = thm "Suc_less_eq";
   1.760 +val Suc_mono = thm "Suc_mono";
   1.761 +val Suc_mult_cancel1 = thm "Suc_mult_cancel1";
   1.762 +val Suc_mult_le_cancel1 = thm "Suc_mult_le_cancel1";
   1.763 +val Suc_mult_less_cancel1 = thm "Suc_mult_less_cancel1";
   1.764 +val Suc_n_not_le_n = thm "Suc_n_not_le_n";
   1.765 +val Suc_n_not_n = thm "Suc_n_not_n";
   1.766 +val Suc_neq_Zero = thm "Suc_neq_Zero";
   1.767 +val Suc_not_Zero = thm "Suc_not_Zero";
   1.768 +val Suc_pred = thm "Suc_pred";
   1.769 +val Zero_nat_def = thm "Zero_nat_def";
   1.770 +val Zero_neq_Suc = thm "Zero_neq_Suc";
   1.771 +val Zero_not_Suc = thm "Zero_not_Suc";
   1.772 +val add_0 = thm "add_0";
   1.773 +val add_0_right = thm "add_0_right";
   1.774 +val add_Suc = thm "add_Suc";
   1.775 +val add_Suc_right = thm "add_Suc_right";
   1.776 +val add_ac = thms "add_ac";
   1.777 +val add_assoc = thm "add_assoc";
   1.778 +val add_commute = thm "add_commute";
   1.779 +val add_diff_inverse = thm "add_diff_inverse";
   1.780 +val add_eq_self_zero = thm "add_eq_self_zero";
   1.781 +val add_gr_0 = thm "add_gr_0";
   1.782 +val add_is_0 = thm "add_is_0";
   1.783 +val add_is_1 = thm "add_is_1";
   1.784 +val add_leD1 = thm "add_leD1";
   1.785 +val add_leD2 = thm "add_leD2";
   1.786 +val add_leE = thm "add_leE";
   1.787 +val add_le_mono = thm "add_le_mono";
   1.788 +val add_le_mono1 = thm "add_le_mono1";
   1.789 +val add_left_cancel = thm "add_left_cancel";
   1.790 +val add_left_cancel_le = thm "add_left_cancel_le";
   1.791 +val add_left_cancel_less = thm "add_left_cancel_less";
   1.792 +val add_left_commute = thm "add_left_commute";
   1.793 +val add_lessD1 = thm "add_lessD1";
   1.794 +val add_less_mono = thm "add_less_mono";
   1.795 +val add_less_mono1 = thm "add_less_mono1";
   1.796 +val add_mult_distrib = thm "add_mult_distrib";
   1.797 +val add_mult_distrib2 = thm "add_mult_distrib2";
   1.798 +val add_right_cancel = thm "add_right_cancel";
   1.799 +val def_nat_rec_0 = thm "def_nat_rec_0";
   1.800 +val def_nat_rec_Suc = thm "def_nat_rec_Suc";
   1.801 +val diff_0 = thm "diff_0";
   1.802 +val diff_0_eq_0 = thm "diff_0_eq_0";
   1.803 +val diff_Suc = thm "diff_Suc";
   1.804 +val diff_Suc_Suc = thm "diff_Suc_Suc";
   1.805 +val diff_Suc_less = thm "diff_Suc_less";
   1.806 +val diff_add_0 = thm "diff_add_0";
   1.807 +val diff_add_assoc = thm "diff_add_assoc";
   1.808 +val diff_add_assoc2 = thm "diff_add_assoc2";
   1.809 +val diff_add_inverse = thm "diff_add_inverse";
   1.810 +val diff_add_inverse2 = thm "diff_add_inverse2";
   1.811 +val diff_cancel = thm "diff_cancel";
   1.812 +val diff_cancel2 = thm "diff_cancel2";
   1.813 +val diff_commute = thm "diff_commute";
   1.814 +val diff_diff_left = thm "diff_diff_left";
   1.815 +val diff_induct = thm "diff_induct";
   1.816 +val diff_is_0_eq = thm "diff_is_0_eq";
   1.817 +val diff_le_self = thm "diff_le_self";
   1.818 +val diff_less_Suc = thm "diff_less_Suc";
   1.819 +val diff_mult_distrib = thm "diff_mult_distrib"; 
   1.820 +val diff_mult_distrib2 = thm "diff_mult_distrib2"; 
   1.821 +val diff_self_eq_0 = thm "diff_self_eq_0";
   1.822 +val eq_imp_le = thm "eq_imp_le";
   1.823 +val gr0I = thm "gr0I";
   1.824 +val gr0_conv_Suc = thm "gr0_conv_Suc";
   1.825 +val gr_implies_not0 = thm "gr_implies_not0";
   1.826 +val inj_Rep_Nat = thm "inj_Rep_Nat";
   1.827 +val inj_Suc = thm "inj_Suc";
   1.828 +val inj_on_Abs_Nat = thm "inj_on_Abs_Nat";
   1.829 +val le0 = thm "le0";
   1.830 +val leD = thm "leD";
   1.831 +val leE = thm "leE";
   1.832 +val leI = thm "leI";
   1.833 +val le_0_eq = thm "le_0_eq";
   1.834 +val le_SucE = thm "le_SucE";
   1.835 +val le_SucI = thm "le_SucI";
   1.836 +val le_Suc_eq = thm "le_Suc_eq";
   1.837 +val le_add1 = thm "le_add1";
   1.838 +val le_add2 = thm "le_add2";
   1.839 +val le_add_diff_inverse = thm "le_add_diff_inverse";
   1.840 +val le_add_diff_inverse2 = thm "le_add_diff_inverse2";
   1.841 +val le_anti_sym = thm "le_anti_sym";
   1.842 +val le_def = thm "le_def";
   1.843 +val le_eq_less_or_eq = thm "le_eq_less_or_eq";
   1.844 +val le_imp_diff_is_add = thm "le_imp_diff_is_add";
   1.845 +val le_imp_less_Suc = thm "le_imp_less_Suc";
   1.846 +val le_imp_less_or_eq = thm "le_imp_less_or_eq";
   1.847 +val le_less_trans = thm "le_less_trans";
   1.848 +val le_neq_implies_less = thm "le_neq_implies_less";
   1.849 +val le_refl = thm "le_refl";
   1.850 +val le_simps = thms "le_simps";
   1.851 +val le_trans = thm "le_trans";
   1.852 +val lessE = thm "lessE";
   1.853 +val lessI = thm "lessI";
   1.854 +val less_Suc0 = thm "less_Suc0";
   1.855 +val less_SucE = thm "less_SucE";
   1.856 +val less_SucI = thm "less_SucI";
   1.857 +val less_Suc_eq = thm "less_Suc_eq";
   1.858 +val less_Suc_eq_0_disj = thm "less_Suc_eq_0_disj";
   1.859 +val less_Suc_eq_le = thm "less_Suc_eq_le";
   1.860 +val less_add_Suc1 = thm "less_add_Suc1";
   1.861 +val less_add_Suc2 = thm "less_add_Suc2";
   1.862 +val less_add_eq_less = thm "less_add_eq_less";
   1.863 +val less_asym = thm "less_asym";
   1.864 +val less_def = thm "less_def";
   1.865 +val less_eq = thm "less_eq";
   1.866 +val less_iff_Suc_add = thm "less_iff_Suc_add";
   1.867 +val less_imp_Suc_add = thm "less_imp_Suc_add";
   1.868 +val less_imp_add_positive = thm "less_imp_add_positive";
   1.869 +val less_imp_diff_less = thm "less_imp_diff_less";
   1.870 +val less_imp_le = thm "less_imp_le";
   1.871 +val less_irrefl = thm "less_irrefl";
   1.872 +val less_le_trans = thm "less_le_trans";
   1.873 +val less_linear = thm "less_linear";
   1.874 +val less_mono_imp_le_mono = thm "less_mono_imp_le_mono";
   1.875 +val less_not_refl = thm "less_not_refl";
   1.876 +val less_not_refl2 = thm "less_not_refl2";
   1.877 +val less_not_refl3 = thm "less_not_refl3";
   1.878 +val less_not_sym = thm "less_not_sym";
   1.879 +val less_one = thm "less_one";
   1.880 +val less_or_eq_imp_le = thm "less_or_eq_imp_le";
   1.881 +val less_trans = thm "less_trans";
   1.882 +val less_trans_Suc = thm "less_trans_Suc";
   1.883 +val less_zeroE = thm "less_zeroE";
   1.884 +val max_0L = thm "max_0L";
   1.885 +val max_0R = thm "max_0R";
   1.886 +val max_Suc_Suc = thm "max_Suc_Suc";
   1.887 +val min_0L = thm "min_0L";
   1.888 +val min_0R = thm "min_0R";
   1.889 +val min_Suc_Suc = thm "min_Suc_Suc";
   1.890 +val mult_0 = thm "mult_0";
   1.891 +val mult_0_right = thm "mult_0_right";
   1.892 +val mult_1 = thm "mult_1";
   1.893 +val mult_1_right = thm "mult_1_right";
   1.894 +val mult_Suc = thm "mult_Suc";
   1.895 +val mult_Suc_right = thm "mult_Suc_right";
   1.896 +val mult_ac = thms "mult_ac";
   1.897 +val mult_assoc = thm "mult_assoc";
   1.898 +val mult_cancel1 = thm "mult_cancel1";
   1.899 +val mult_cancel2 = thm "mult_cancel2";
   1.900 +val mult_commute = thm "mult_commute";
   1.901 +val mult_eq_1_iff = thm "mult_eq_1_iff";
   1.902 +val mult_eq_self_implies_10 = thm "mult_eq_self_implies_10";
   1.903 +val mult_is_0 = thm "mult_is_0";
   1.904 +val mult_le_cancel1 = thm "mult_le_cancel1";
   1.905 +val mult_le_cancel2 = thm "mult_le_cancel2";
   1.906 +val mult_le_mono = thm "mult_le_mono";
   1.907 +val mult_le_mono1 = thm "mult_le_mono1";
   1.908 +val mult_le_mono2 = thm "mult_le_mono2";
   1.909 +val mult_left_commute = thm "mult_left_commute";
   1.910 +val mult_less_cancel1 = thm "mult_less_cancel1";
   1.911 +val mult_less_cancel2 = thm "mult_less_cancel2";
   1.912 +val mult_less_mono1 = thm "mult_less_mono1";
   1.913 +val mult_less_mono2 = thm "mult_less_mono2";
   1.914 +val n_not_Suc_n = thm "n_not_Suc_n";
   1.915 +val nat_distrib = thms "nat_distrib";
   1.916 +val nat_induct = thm "nat_induct";
   1.917 +val nat_induct2 = thm "nat_induct2";
   1.918 +val nat_le_linear = thm "nat_le_linear";
   1.919 +val nat_less_cases = thm "nat_less_cases";
   1.920 +val nat_less_induct = thm "nat_less_induct";
   1.921 +val nat_less_le = thm "nat_less_le";
   1.922 +val nat_neq_iff = thm "nat_neq_iff";
   1.923 +val nat_not_singleton = thm "nat_not_singleton";
   1.924 +val neq0_conv = thm "neq0_conv";
   1.925 +val not0_implies_Suc = thm "not0_implies_Suc";
   1.926 +val not_add_less1 = thm "not_add_less1";
   1.927 +val not_add_less2 = thm "not_add_less2";
   1.928 +val not_gr0 = thm "not_gr0";
   1.929 +val not_leE = thm "not_leE";
   1.930 +val not_le_iff_less = thm "not_le_iff_less";
   1.931 +val not_less0 = thm "not_less0";
   1.932 +val not_less_Least = thm "not_less_Least";
   1.933 +val not_less_eq = thm "not_less_eq";
   1.934 +val not_less_iff_le = thm "not_less_iff_le";
   1.935 +val not_less_less_Suc_eq = thm "not_less_less_Suc_eq";
   1.936 +val not_less_simps = thms "not_less_simps";
   1.937 +val one_eq_mult_iff = thm "one_eq_mult_iff";
   1.938 +val one_is_add = thm "one_is_add";
   1.939 +val one_le_mult_iff = thm "one_le_mult_iff";
   1.940 +val one_reorient = thm "one_reorient";
   1.941 +val powerI = thm "powerI";
   1.942 +val pred_nat_def = thm "pred_nat_def";
   1.943 +val trans_le_add1 = thm "trans_le_add1";
   1.944 +val trans_le_add2 = thm "trans_le_add2";
   1.945 +val trans_less_add1 = thm "trans_less_add1";
   1.946 +val trans_less_add2 = thm "trans_less_add2";
   1.947 +val wf_less = thm "wf_less";
   1.948 +val wf_pred_nat = thm "wf_pred_nat";
   1.949 +val zero_induct = thm "zero_induct";
   1.950 +val zero_induct_lemma = thm "zero_induct_lemma";
   1.951 +val zero_less_Suc = thm "zero_less_Suc";
   1.952 +val zero_less_diff = thm "zero_less_diff";
   1.953 +val zero_less_mult_iff = thm "zero_less_mult_iff";
   1.954 +val zero_reorient = thm "zero_reorient";