More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
authorpaulson
Tue Nov 25 10:37:03 2003 +0100 (2003-11-25)
changeset 14267b963e9cee2a0
parent 14266 08b34c902618
child 14268 5cf13e80be0e
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
to Isar script.
src/HOL/Divides.thy
src/HOL/Divides_lemmas.ML
src/HOL/Integ/Int.thy
src/HOL/Integ/nat_simprocs.ML
src/HOL/IsaMakefile
src/HOL/Nat.thy
src/HOL/Ring_and_Field.thy
     1.1 --- a/src/HOL/Divides.thy	Mon Nov 24 15:33:07 2003 +0100
     1.2 +++ b/src/HOL/Divides.thy	Tue Nov 25 10:37:03 2003 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  The division operators div, mod and the divides relation "dvd"
     1.5  *)
     1.6  
     1.7 -theory Divides = NatArith files("Divides_lemmas.ML"):
     1.8 +theory Divides = NatArith:
     1.9  
    1.10  (*We use the same class for div and mod;
    1.11    moreover, dvd is defined whenever multiplication is*)
    1.12 @@ -32,7 +32,7 @@
    1.13                            (%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m"
    1.14  
    1.15  (*The definition of dvd is polymorphic!*)
    1.16 -  dvd_def:   "m dvd n == EX k. n = m*k"
    1.17 +  dvd_def:   "m dvd n == \<exists>k. n = m*k"
    1.18  
    1.19  (*This definition helps prove the harder properties of div and mod.
    1.20    It is copied from IntDiv.thy; should it be overloaded?*)
    1.21 @@ -40,11 +40,612 @@
    1.22    quorem :: "(nat*nat) * (nat*nat) => bool"
    1.23      "quorem == %((a,b), (q,r)).
    1.24                        a = b*q + r &
    1.25 -                      (if 0<b then 0<=r & r<b else b<r & r <=0)"
    1.26 +                      (if 0<b then 0\<le>r & r<b else b<r & r \<le>0)"
    1.27 +
    1.28 +
    1.29 +
    1.30 +subsection{*Initial Lemmas*}
    1.31 +
    1.32 +lemmas wf_less_trans = 
    1.33 +       def_wfrec [THEN trans, OF eq_reflection wf_pred_nat [THEN wf_trancl],
    1.34 +                  standard]
    1.35 +
    1.36 +lemma mod_eq: "(%m. m mod n) = 
    1.37 +              wfrec (trancl pred_nat) (%f j. if j<n | n=0 then j else f (j-n))"
    1.38 +by (simp add: mod_def)
    1.39 +
    1.40 +lemma div_eq: "(%m. m div n) = wfrec (trancl pred_nat)  
    1.41 +               (%f j. if j<n | n=0 then 0 else Suc (f (j-n)))"
    1.42 +by (simp add: div_def)
    1.43 +
    1.44 +
    1.45 +(** Aribtrary definitions for division by zero.  Useful to simplify 
    1.46 +    certain equations **)
    1.47 +
    1.48 +lemma DIVISION_BY_ZERO_DIV [simp]: "a div 0 = (0::nat)"
    1.49 +by (rule div_eq [THEN wf_less_trans], simp)
    1.50 +
    1.51 +lemma DIVISION_BY_ZERO_MOD [simp]: "a mod 0 = (a::nat)"
    1.52 +by (rule mod_eq [THEN wf_less_trans], simp)
    1.53 +
    1.54 +
    1.55 +subsection{*Remainder*}
    1.56 +
    1.57 +lemma mod_less [simp]: "m<n ==> m mod n = (m::nat)"
    1.58 +by (rule mod_eq [THEN wf_less_trans], simp)
    1.59 +
    1.60 +lemma mod_geq: "~ m < (n::nat) ==> m mod n = (m-n) mod n"
    1.61 +apply (case_tac "n=0", simp) 
    1.62 +apply (rule mod_eq [THEN wf_less_trans])
    1.63 +apply (simp add: diff_less cut_apply less_eq)
    1.64 +done
    1.65 +
    1.66 +(*Avoids the ugly ~m<n above*)
    1.67 +lemma le_mod_geq: "(n::nat) \<le> m ==> m mod n = (m-n) mod n"
    1.68 +by (simp add: mod_geq not_less_iff_le)
    1.69 +
    1.70 +lemma mod_if: "m mod (n::nat) = (if m<n then m else (m-n) mod n)"
    1.71 +by (simp add: mod_geq)
    1.72 +
    1.73 +lemma mod_1 [simp]: "m mod Suc 0 = 0"
    1.74 +apply (induct_tac "m")
    1.75 +apply (simp_all (no_asm_simp) add: mod_geq)
    1.76 +done
    1.77 +
    1.78 +lemma mod_self [simp]: "n mod n = (0::nat)"
    1.79 +apply (case_tac "n=0")
    1.80 +apply (simp_all add: mod_geq)
    1.81 +done
    1.82 +
    1.83 +lemma mod_add_self2 [simp]: "(m+n) mod n = m mod (n::nat)"
    1.84 +apply (subgoal_tac " (n + m) mod n = (n+m-n) mod n") 
    1.85 +apply (simp add: add_commute)
    1.86 +apply (subst mod_geq [symmetric], simp_all)
    1.87 +done
    1.88 +
    1.89 +lemma mod_add_self1 [simp]: "(n+m) mod n = m mod (n::nat)"
    1.90 +by (simp add: add_commute mod_add_self2)
    1.91 +
    1.92 +lemma mod_mult_self1 [simp]: "(m + k*n) mod n = m mod (n::nat)"
    1.93 +apply (induct_tac "k")
    1.94 +apply (simp_all add: add_left_commute [of _ n])
    1.95 +done
    1.96 +
    1.97 +lemma mod_mult_self2 [simp]: "(m + n*k) mod n = m mod (n::nat)"
    1.98 +by (simp add: mult_commute mod_mult_self1)
    1.99 +
   1.100 +lemma mod_mult_distrib: "(m mod n) * (k::nat) = (m*k) mod (n*k)"
   1.101 +apply (case_tac "n=0", simp)
   1.102 +apply (case_tac "k=0", simp)
   1.103 +apply (induct_tac "m" rule: nat_less_induct)
   1.104 +apply (subst mod_if, simp)
   1.105 +apply (simp add: mod_geq diff_less diff_mult_distrib)
   1.106 +done
   1.107 +
   1.108 +lemma mod_mult_distrib2: "(k::nat) * (m mod n) = (k*m) mod (k*n)"
   1.109 +by (simp add: mult_commute [of k] mod_mult_distrib)
   1.110 +
   1.111 +lemma mod_mult_self_is_0 [simp]: "(m*n) mod n = (0::nat)"
   1.112 +apply (case_tac "n=0", simp)
   1.113 +apply (induct_tac "m", simp)
   1.114 +apply (rename_tac "k")
   1.115 +apply (cut_tac m = "k*n" and n = n in mod_add_self2)
   1.116 +apply (simp add: add_commute)
   1.117 +done
   1.118 +
   1.119 +lemma mod_mult_self1_is_0 [simp]: "(n*m) mod n = (0::nat)"
   1.120 +by (simp add: mult_commute mod_mult_self_is_0)
   1.121 +
   1.122 +
   1.123 +subsection{*Quotient*}
   1.124 +
   1.125 +lemma div_less [simp]: "m<n ==> m div n = (0::nat)"
   1.126 +by (rule div_eq [THEN wf_less_trans], simp)
   1.127 +
   1.128 +lemma div_geq: "[| 0<n;  ~m<n |] ==> m div n = Suc((m-n) div n)"
   1.129 +apply (rule div_eq [THEN wf_less_trans])
   1.130 +apply (simp add: diff_less cut_apply less_eq)
   1.131 +done
   1.132 +
   1.133 +(*Avoids the ugly ~m<n above*)
   1.134 +lemma le_div_geq: "[| 0<n;  n\<le>m |] ==> m div n = Suc((m-n) div n)"
   1.135 +by (simp add: div_geq not_less_iff_le)
   1.136 +
   1.137 +lemma div_if: "0<n ==> m div n = (if m<n then 0 else Suc((m-n) div n))"
   1.138 +by (simp add: div_geq)
   1.139 +
   1.140 +
   1.141 +(*Main Result about quotient and remainder.*)
   1.142 +lemma mod_div_equality: "(m div n)*n + m mod n = (m::nat)"
   1.143 +apply (case_tac "n=0", simp)
   1.144 +apply (induct_tac "m" rule: nat_less_induct)
   1.145 +apply (subst mod_if)
   1.146 +apply (simp_all (no_asm_simp) add: add_assoc div_geq add_diff_inverse diff_less)
   1.147 +done
   1.148 +
   1.149 +lemma mod_div_equality2: "n * (m div n) + m mod n = (m::nat)"
   1.150 +apply(cut_tac m = m and n = n in mod_div_equality)
   1.151 +apply(simp add: mult_commute)
   1.152 +done
   1.153 +
   1.154 +subsection{*Simproc for Cancelling Div and Mod*}
   1.155 +
   1.156 +lemma div_mod_equality: "((m div n)*n + m mod n) + k = (m::nat) + k"
   1.157 +apply(simp add: mod_div_equality)
   1.158 +done
   1.159 +
   1.160 +lemma div_mod_equality2: "(n*(m div n) + m mod n) + k = (m::nat) + k"
   1.161 +apply(simp add: mod_div_equality2)
   1.162 +done
   1.163 +
   1.164 +ML
   1.165 +{*
   1.166 +val div_mod_equality = thm "div_mod_equality";
   1.167 +val div_mod_equality2 = thm "div_mod_equality2";
   1.168 +
   1.169 +
   1.170 +structure CancelDivModData =
   1.171 +struct
   1.172 +
   1.173 +val div_name = "Divides.op div";
   1.174 +val mod_name = "Divides.op mod";
   1.175 +val mk_binop = HOLogic.mk_binop;
   1.176 +val mk_sum = NatArithUtils.mk_sum;
   1.177 +val dest_sum = NatArithUtils.dest_sum;
   1.178 +
   1.179 +(*logic*)
   1.180 +
   1.181 +val div_mod_eqs = map mk_meta_eq [div_mod_equality,div_mod_equality2]
   1.182 +
   1.183 +val trans = trans
   1.184 +
   1.185 +val prove_eq_sums =
   1.186 +  let val simps = add_0 :: add_0_right :: add_ac
   1.187 +  in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all simps) end
   1.188 +
   1.189 +end;
   1.190 +
   1.191 +structure CancelDivMod = CancelDivModFun(CancelDivModData);
   1.192 +
   1.193 +val cancel_div_mod_proc = NatArithUtils.prep_simproc
   1.194 +      ("cancel_div_mod", ["(m::nat) + n"], CancelDivMod.proc);
   1.195 +
   1.196 +Addsimprocs[cancel_div_mod_proc];
   1.197 +*}
   1.198 +
   1.199 +
   1.200 +(* a simple rearrangement of mod_div_equality: *)
   1.201 +lemma mult_div_cancel: "(n::nat) * (m div n) = m - (m mod n)"
   1.202 +by (cut_tac m = m and n = n in mod_div_equality2, arith)
   1.203 +
   1.204 +lemma mod_less_divisor [simp]: "0<n ==> m mod n < (n::nat)"
   1.205 +apply (induct_tac "m" rule: nat_less_induct)
   1.206 +apply (case_tac "na<n", simp) 
   1.207 +txt{*case @{term "n \<le> na"}*}
   1.208 +apply (simp add: mod_geq diff_less)
   1.209 +done
   1.210 +
   1.211 +lemma div_mult_self_is_m [simp]: "0<n ==> (m*n) div n = (m::nat)"
   1.212 +by (cut_tac m = "m*n" and n = n in mod_div_equality, auto)
   1.213 +
   1.214 +lemma div_mult_self1_is_m [simp]: "0<n ==> (n*m) div n = (m::nat)"
   1.215 +by (simp add: mult_commute div_mult_self_is_m)
   1.216 +
   1.217 +(*mod_mult_distrib2 above is the counterpart for remainder*)
   1.218 +
   1.219 +
   1.220 +subsection{*Proving facts about Quotient and Remainder*}
   1.221 +
   1.222 +lemma unique_quotient_lemma:
   1.223 +     "[| b*q' + r'  \<le> b*q + r;  0 < b;  r < b |]  
   1.224 +      ==> q' \<le> (q::nat)"
   1.225 +apply (rule leI)
   1.226 +apply (subst less_iff_Suc_add)
   1.227 +apply (auto simp add: add_mult_distrib2)
   1.228 +done
   1.229 +
   1.230 +lemma unique_quotient:
   1.231 +     "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  0 < b |]  
   1.232 +      ==> q = q'"
   1.233 +apply (simp add: split_ifs quorem_def)
   1.234 +apply (blast intro: order_antisym 
   1.235 +             dest: order_eq_refl [THEN unique_quotient_lemma] sym)+
   1.236 +done
   1.237 +
   1.238 +lemma unique_remainder:
   1.239 +     "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  0 < b |]  
   1.240 +      ==> r = r'"
   1.241 +apply (subgoal_tac "q = q'")
   1.242 +prefer 2 apply (blast intro: unique_quotient)
   1.243 +apply (simp add: quorem_def)
   1.244 +done
   1.245 +
   1.246 +lemma quorem_div_mod: "0 < b ==> quorem ((a, b), (a div b, a mod b))"
   1.247 +by (auto simp add: quorem_def)
   1.248 +
   1.249 +lemma quorem_div: "[| quorem((a,b),(q,r));  0 < b |] ==> a div b = q"
   1.250 +by (simp add: quorem_div_mod [THEN unique_quotient])
   1.251 +
   1.252 +lemma quorem_mod: "[| quorem((a,b),(q,r));  0 < b |] ==> a mod b = r"
   1.253 +by (simp add: quorem_div_mod [THEN unique_remainder])
   1.254 +
   1.255 +(** A dividend of zero **)
   1.256 +
   1.257 +lemma div_0 [simp]: "0 div m = (0::nat)"
   1.258 +by (case_tac "m=0", simp_all)
   1.259 +
   1.260 +lemma mod_0 [simp]: "0 mod m = (0::nat)"
   1.261 +by (case_tac "m=0", simp_all)
   1.262 +
   1.263 +(** proving (a*b) div c = a * (b div c) + a * (b mod c) **)
   1.264 +
   1.265 +lemma quorem_mult1_eq:
   1.266 +     "[| quorem((b,c),(q,r));  0 < c |]  
   1.267 +      ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))"
   1.268 +apply (auto simp add: split_ifs mult_ac quorem_def add_mult_distrib2)
   1.269 +done
   1.270 +
   1.271 +lemma div_mult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::nat)"
   1.272 +apply (case_tac "c = 0", simp)
   1.273 +apply (blast intro: quorem_div_mod [THEN quorem_mult1_eq, THEN quorem_div])
   1.274 +done
   1.275 +
   1.276 +lemma mod_mult1_eq: "(a*b) mod c = a*(b mod c) mod (c::nat)"
   1.277 +apply (case_tac "c = 0", simp)
   1.278 +apply (blast intro: quorem_div_mod [THEN quorem_mult1_eq, THEN quorem_mod])
   1.279 +done
   1.280 +
   1.281 +lemma mod_mult1_eq': "(a*b) mod (c::nat) = ((a mod c) * b) mod c"
   1.282 +apply (rule trans)
   1.283 +apply (rule_tac s = "b*a mod c" in trans)
   1.284 +apply (rule_tac [2] mod_mult1_eq)
   1.285 +apply (simp_all (no_asm) add: mult_commute)
   1.286 +done
   1.287 +
   1.288 +lemma mod_mult_distrib_mod: "(a*b) mod (c::nat) = ((a mod c) * (b mod c)) mod c"
   1.289 +apply (rule mod_mult1_eq' [THEN trans])
   1.290 +apply (rule mod_mult1_eq)
   1.291 +done
   1.292 +
   1.293 +(** proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) **)
   1.294 +
   1.295 +lemma quorem_add1_eq:
   1.296 +     "[| quorem((a,c),(aq,ar));  quorem((b,c),(bq,br));  0 < c |]  
   1.297 +      ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))"
   1.298 +by (auto simp add: split_ifs mult_ac quorem_def add_mult_distrib2)
   1.299 +
   1.300 +(*NOT suitable for rewriting: the RHS has an instance of the LHS*)
   1.301 +lemma div_add1_eq:
   1.302 +     "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
   1.303 +apply (case_tac "c = 0", simp)
   1.304 +apply (blast intro: quorem_add1_eq [THEN quorem_div] quorem_div_mod quorem_div_mod)
   1.305 +done
   1.306 +
   1.307 +lemma mod_add1_eq: "(a+b) mod (c::nat) = (a mod c + b mod c) mod c"
   1.308 +apply (case_tac "c = 0", simp)
   1.309 +apply (blast intro: quorem_div_mod quorem_div_mod
   1.310 +                    quorem_add1_eq [THEN quorem_mod])
   1.311 +done
   1.312 +
   1.313 +
   1.314 +subsection{*Proving @{term "a div (b*c) = (a div b) div c"}*}
   1.315 +
   1.316 +(** first, a lemma to bound the remainder **)
   1.317 +
   1.318 +lemma mod_lemma: "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c"
   1.319 +apply (cut_tac m = q and n = c in mod_less_divisor)
   1.320 +apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
   1.321 +apply (erule_tac P = "%x. ?lhs < ?rhs x" in ssubst)
   1.322 +apply (simp add: add_mult_distrib2)
   1.323 +done
   1.324  
   1.325 -use "Divides_lemmas.ML"
   1.326 +lemma quorem_mult2_eq: "[| quorem ((a,b), (q,r));  0 < b;  0 < c |]  
   1.327 +      ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))"
   1.328 +apply (auto simp add: mult_ac quorem_def add_mult_distrib2 [symmetric] mod_lemma)
   1.329 +done
   1.330 +
   1.331 +lemma div_mult2_eq: "a div (b*c) = (a div b) div (c::nat)"
   1.332 +apply (case_tac "b=0", simp)
   1.333 +apply (case_tac "c=0", simp)
   1.334 +apply (force simp add: quorem_div_mod [THEN quorem_mult2_eq, THEN quorem_div])
   1.335 +done
   1.336 +
   1.337 +lemma mod_mult2_eq: "a mod (b*c) = b*(a div b mod c) + a mod (b::nat)"
   1.338 +apply (case_tac "b=0", simp)
   1.339 +apply (case_tac "c=0", simp)
   1.340 +apply (auto simp add: mult_commute quorem_div_mod [THEN quorem_mult2_eq, THEN quorem_mod])
   1.341 +done
   1.342 +
   1.343 +
   1.344 +subsection{*Cancellation of Common Factors in Division*}
   1.345 +
   1.346 +lemma div_mult_mult_lemma:
   1.347 +     "[| (0::nat) < b;  0 < c |] ==> (c*a) div (c*b) = a div b"
   1.348 +by (auto simp add: div_mult2_eq)
   1.349 +
   1.350 +lemma div_mult_mult1 [simp]: "(0::nat) < c ==> (c*a) div (c*b) = a div b"
   1.351 +apply (case_tac "b = 0")
   1.352 +apply (auto simp add: linorder_neq_iff [of b] div_mult_mult_lemma)
   1.353 +done
   1.354 +
   1.355 +lemma div_mult_mult2 [simp]: "(0::nat) < c ==> (a*c) div (b*c) = a div b"
   1.356 +apply (drule div_mult_mult1)
   1.357 +apply (auto simp add: mult_commute)
   1.358 +done
   1.359 +
   1.360 +
   1.361 +(*Distribution of Factors over Remainders:
   1.362 +
   1.363 +Could prove these as in Integ/IntDiv.ML, but we already have
   1.364 +mod_mult_distrib and mod_mult_distrib2 above!
   1.365 +
   1.366 +Goal "(c*a) mod (c*b) = (c::nat) * (a mod b)"
   1.367 +qed "mod_mult_mult1";
   1.368 +
   1.369 +Goal "(a*c) mod (b*c) = (a mod b) * (c::nat)";
   1.370 +qed "mod_mult_mult2";
   1.371 + ***)
   1.372 +
   1.373 +subsection{*Further Facts about Quotient and Remainder*}
   1.374 +
   1.375 +lemma div_1 [simp]: "m div Suc 0 = m"
   1.376 +apply (induct_tac "m")
   1.377 +apply (simp_all (no_asm_simp) add: div_geq)
   1.378 +done
   1.379 +
   1.380 +lemma div_self [simp]: "0<n ==> n div n = (1::nat)"
   1.381 +by (simp add: div_geq)
   1.382 +
   1.383 +lemma div_add_self2: "0<n ==> (m+n) div n = Suc (m div n)"
   1.384 +apply (subgoal_tac " (n + m) div n = Suc ((n+m-n) div n) ")
   1.385 +apply (simp add: add_commute)
   1.386 +apply (subst div_geq [symmetric], simp_all)
   1.387 +done
   1.388 +
   1.389 +lemma div_add_self1: "0<n ==> (n+m) div n = Suc (m div n)"
   1.390 +by (simp add: add_commute div_add_self2)
   1.391 +
   1.392 +lemma div_mult_self1 [simp]: "!!n::nat. 0<n ==> (m + k*n) div n = k + m div n"
   1.393 +apply (subst div_add1_eq)
   1.394 +apply (subst div_mult1_eq, simp)
   1.395 +done
   1.396 +
   1.397 +lemma div_mult_self2 [simp]: "0<n ==> (m + n*k) div n = k + m div (n::nat)"
   1.398 +by (simp add: mult_commute div_mult_self1)
   1.399 +
   1.400 +
   1.401 +(* Monotonicity of div in first argument *)
   1.402 +lemma div_le_mono [rule_format (no_asm)]:
   1.403 +     "\<forall>m::nat. m \<le> n --> (m div k) \<le> (n div k)"
   1.404 +apply (case_tac "k=0", simp)
   1.405 +apply (induct_tac "n" rule: nat_less_induct, clarify)
   1.406 +apply (case_tac "n<k")
   1.407 +(* 1  case n<k *)
   1.408 +apply simp
   1.409 +(* 2  case n >= k *)
   1.410 +apply (case_tac "m<k")
   1.411 +(* 2.1  case m<k *)
   1.412 +apply simp
   1.413 +(* 2.2  case m>=k *)
   1.414 +apply (simp add: div_geq diff_less diff_le_mono)
   1.415 +done
   1.416 +
   1.417 +(* Antimonotonicity of div in second argument *)
   1.418 +lemma div_le_mono2: "!!m::nat. [| 0<m; m\<le>n |] ==> (k div n) \<le> (k div m)"
   1.419 +apply (subgoal_tac "0<n")
   1.420 + prefer 2 apply simp 
   1.421 +apply (induct_tac "k" rule: nat_less_induct)
   1.422 +apply (rename_tac "k")
   1.423 +apply (case_tac "k<n", simp)
   1.424 +apply (subgoal_tac "~ (k<m) ")
   1.425 + prefer 2 apply simp 
   1.426 +apply (simp add: div_geq)
   1.427 +apply (subgoal_tac " (k-n) div n \<le> (k-m) div n")
   1.428 + prefer 2
   1.429 + apply (blast intro: div_le_mono diff_le_mono2)
   1.430 +apply (rule le_trans, simp)
   1.431 +apply (simp add: diff_less)
   1.432 +done
   1.433 +
   1.434 +lemma div_le_dividend [simp]: "m div n \<le> (m::nat)"
   1.435 +apply (case_tac "n=0", simp)
   1.436 +apply (subgoal_tac "m div n \<le> m div 1", simp)
   1.437 +apply (rule div_le_mono2)
   1.438 +apply (simp_all (no_asm_simp))
   1.439 +done
   1.440 +
   1.441 +(* Similar for "less than" *) 
   1.442 +lemma div_less_dividend [rule_format, simp]:
   1.443 +     "!!n::nat. 1<n ==> 0 < m --> m div n < m"
   1.444 +apply (induct_tac "m" rule: nat_less_induct)
   1.445 +apply (rename_tac "m")
   1.446 +apply (case_tac "m<n", simp)
   1.447 +apply (subgoal_tac "0<n")
   1.448 + prefer 2 apply simp 
   1.449 +apply (simp add: div_geq)
   1.450 +apply (case_tac "n<m")
   1.451 + apply (subgoal_tac " (m-n) div n < (m-n) ")
   1.452 +  apply (rule impI less_trans_Suc)+
   1.453 +apply assumption
   1.454 +  apply (simp_all add: diff_less)
   1.455 +done
   1.456 +
   1.457 +text{*A fact for the mutilated chess board*}
   1.458 +lemma mod_Suc: "Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))"
   1.459 +apply (case_tac "n=0", simp)
   1.460 +apply (induct_tac "m" rule: nat_less_induct)
   1.461 +apply (case_tac "Suc (na) <n")
   1.462 +(* case Suc(na) < n *)
   1.463 +apply (frule lessI [THEN less_trans], simp add: less_not_refl3)
   1.464 +(* case n \<le> Suc(na) *)
   1.465 +apply (simp add: not_less_iff_le le_Suc_eq mod_geq)
   1.466 +apply (auto simp add: Suc_diff_le diff_less le_mod_geq)
   1.467 +done
   1.468 +
   1.469 +
   1.470 +subsection{*The Divides Relation*}
   1.471 +
   1.472 +lemma dvdI [intro?]: "n = m * k ==> m dvd n"
   1.473 +by (unfold dvd_def, blast)
   1.474 +
   1.475 +lemma dvdE [elim?]: "!!P. [|m dvd n;  !!k. n = m*k ==> P|] ==> P"
   1.476 +by (unfold dvd_def, blast)
   1.477  
   1.478 -declare dvdI [intro?]  dvdE [elim?]  dvd_trans [trans]
   1.479 +lemma dvd_0_right [iff]: "m dvd (0::nat)"
   1.480 +apply (unfold dvd_def)
   1.481 +apply (blast intro: mult_0_right [symmetric])
   1.482 +done
   1.483 +
   1.484 +lemma dvd_0_left: "0 dvd m ==> m = (0::nat)"
   1.485 +by (force simp add: dvd_def)
   1.486 +
   1.487 +lemma dvd_0_left_iff [iff]: "(0 dvd (m::nat)) = (m = 0)"
   1.488 +by (blast intro: dvd_0_left)
   1.489 +
   1.490 +lemma dvd_1_left [iff]: "Suc 0 dvd k"
   1.491 +by (unfold dvd_def, simp)
   1.492 +
   1.493 +lemma dvd_1_iff_1 [simp]: "(m dvd Suc 0) = (m = Suc 0)"
   1.494 +by (simp add: dvd_def)
   1.495 +
   1.496 +lemma dvd_refl [simp]: "m dvd (m::nat)"
   1.497 +apply (unfold dvd_def)
   1.498 +apply (blast intro: mult_1_right [symmetric])
   1.499 +done
   1.500 +
   1.501 +lemma dvd_trans [trans]: "[| m dvd n; n dvd p |] ==> m dvd (p::nat)"
   1.502 +apply (unfold dvd_def)
   1.503 +apply (blast intro: mult_assoc)
   1.504 +done
   1.505 +
   1.506 +lemma dvd_anti_sym: "[| m dvd n; n dvd m |] ==> m = (n::nat)"
   1.507 +apply (unfold dvd_def)
   1.508 +apply (force dest: mult_eq_self_implies_10 simp add: mult_assoc mult_eq_1_iff)
   1.509 +done
   1.510 +
   1.511 +lemma dvd_add: "[| k dvd m; k dvd n |] ==> k dvd (m+n :: nat)"
   1.512 +apply (unfold dvd_def)
   1.513 +apply (blast intro: add_mult_distrib2 [symmetric])
   1.514 +done
   1.515 +
   1.516 +lemma dvd_diff: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"
   1.517 +apply (unfold dvd_def)
   1.518 +apply (blast intro: diff_mult_distrib2 [symmetric])
   1.519 +done
   1.520 +
   1.521 +lemma dvd_diffD: "[| k dvd m-n; k dvd n; n\<le>m |] ==> k dvd (m::nat)"
   1.522 +apply (erule not_less_iff_le [THEN iffD2, THEN add_diff_inverse, THEN subst])
   1.523 +apply (blast intro: dvd_add)
   1.524 +done
   1.525 +
   1.526 +lemma dvd_diffD1: "[| k dvd m-n; k dvd m; n\<le>m |] ==> k dvd (n::nat)"
   1.527 +by (drule_tac m = m in dvd_diff, auto)
   1.528 +
   1.529 +lemma dvd_mult: "k dvd n ==> k dvd (m*n :: nat)"
   1.530 +apply (unfold dvd_def)
   1.531 +apply (blast intro: mult_left_commute)
   1.532 +done
   1.533 +
   1.534 +lemma dvd_mult2: "k dvd m ==> k dvd (m*n :: nat)"
   1.535 +apply (subst mult_commute)
   1.536 +apply (erule dvd_mult)
   1.537 +done
   1.538 +
   1.539 +(* k dvd (m*k) *)
   1.540 +declare dvd_refl [THEN dvd_mult, iff] dvd_refl [THEN dvd_mult2, iff]
   1.541 +
   1.542 +lemma dvd_reduce: "(k dvd n + k) = (k dvd (n::nat))"
   1.543 +apply (rule iffI)
   1.544 +apply (erule_tac [2] dvd_add)
   1.545 +apply (rule_tac [2] dvd_refl)
   1.546 +apply (subgoal_tac "n = (n+k) -k")
   1.547 + prefer 2 apply simp 
   1.548 +apply (erule ssubst)
   1.549 +apply (erule dvd_diff)
   1.550 +apply (rule dvd_refl)
   1.551 +done
   1.552 +
   1.553 +lemma dvd_mod: "!!n::nat. [| f dvd m; f dvd n |] ==> f dvd m mod n"
   1.554 +apply (unfold dvd_def)
   1.555 +apply (case_tac "n=0", auto)
   1.556 +apply (blast intro: mod_mult_distrib2 [symmetric])
   1.557 +done
   1.558 +
   1.559 +lemma dvd_mod_imp_dvd: "[| (k::nat) dvd m mod n;  k dvd n |] ==> k dvd m"
   1.560 +apply (subgoal_tac "k dvd (m div n) *n + m mod n")
   1.561 + apply (simp add: mod_div_equality)
   1.562 +apply (simp only: dvd_add dvd_mult)
   1.563 +done
   1.564 +
   1.565 +lemma dvd_mod_iff: "k dvd n ==> ((k::nat) dvd m mod n) = (k dvd m)"
   1.566 +by (blast intro: dvd_mod_imp_dvd dvd_mod)
   1.567 +
   1.568 +lemma dvd_mult_cancel: "!!k::nat. [| k*m dvd k*n; 0<k |] ==> m dvd n"
   1.569 +apply (unfold dvd_def)
   1.570 +apply (erule exE)
   1.571 +apply (simp add: mult_ac)
   1.572 +done
   1.573 +
   1.574 +lemma dvd_mult_cancel1: "0<m ==> (m*n dvd m) = (n = (1::nat))"
   1.575 +apply auto
   1.576 +apply (subgoal_tac "m*n dvd m*1")
   1.577 +apply (drule dvd_mult_cancel, auto)
   1.578 +done
   1.579 +
   1.580 +lemma dvd_mult_cancel2: "0<m ==> (n*m dvd m) = (n = (1::nat))"
   1.581 +apply (subst mult_commute)
   1.582 +apply (erule dvd_mult_cancel1)
   1.583 +done
   1.584 +
   1.585 +lemma mult_dvd_mono: "[| i dvd m; j dvd n|] ==> i*j dvd (m*n :: nat)"
   1.586 +apply (unfold dvd_def, clarify)
   1.587 +apply (rule_tac x = "k*ka" in exI)
   1.588 +apply (simp add: mult_ac)
   1.589 +done
   1.590 +
   1.591 +lemma dvd_mult_left: "(i*j :: nat) dvd k ==> i dvd k"
   1.592 +by (simp add: dvd_def mult_assoc, blast)
   1.593 +
   1.594 +lemma dvd_mult_right: "(i*j :: nat) dvd k ==> j dvd k"
   1.595 +apply (unfold dvd_def, clarify)
   1.596 +apply (rule_tac x = "i*k" in exI)
   1.597 +apply (simp add: mult_ac)
   1.598 +done
   1.599 +
   1.600 +lemma dvd_imp_le: "[| k dvd n; 0 < n |] ==> k \<le> (n::nat)"
   1.601 +apply (unfold dvd_def, clarify)
   1.602 +apply (simp_all (no_asm_use) add: zero_less_mult_iff)
   1.603 +apply (erule conjE)
   1.604 +apply (rule le_trans)
   1.605 +apply (rule_tac [2] le_refl [THEN mult_le_mono])
   1.606 +apply (erule_tac [2] Suc_leI, simp)
   1.607 +done
   1.608 +
   1.609 +lemma dvd_eq_mod_eq_0: "!!k::nat. (k dvd n) = (n mod k = 0)"
   1.610 +apply (unfold dvd_def)
   1.611 +apply (case_tac "k=0", simp, safe)
   1.612 +apply (simp add: mult_commute)
   1.613 +apply (rule_tac t = n and n1 = k in mod_div_equality [THEN subst])
   1.614 +apply (subst mult_commute, simp)
   1.615 +done
   1.616 +
   1.617 +lemma dvd_mult_div_cancel: "n dvd m ==> n * (m div n) = (m::nat)"
   1.618 +apply (subgoal_tac "m mod n = 0")
   1.619 + apply (simp add: mult_div_cancel)
   1.620 +apply (simp only: dvd_eq_mod_eq_0)
   1.621 +done
   1.622 +
   1.623 +lemma mod_eq_0_iff: "(m mod d = 0) = (\<exists>q::nat. m = d*q)"
   1.624 +by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
   1.625 +declare mod_eq_0_iff [THEN iffD1, dest!]
   1.626 +
   1.627 +(*Loses information, namely we also have r<d provided d is nonzero*)
   1.628 +lemma mod_eqD: "(m mod d = r) ==> \<exists>q::nat. m = r + q*d"
   1.629 +apply (cut_tac m = m in mod_div_equality)
   1.630 +apply (simp only: add_ac)
   1.631 +apply (blast intro: sym)
   1.632 +done
   1.633 +
   1.634  
   1.635  lemma split_div:
   1.636   "P(n div k :: nat) =
   1.637 @@ -87,7 +688,7 @@
   1.638  qed
   1.639  
   1.640  lemma split_div_lemma:
   1.641 -  "0 < n \<Longrightarrow> (n * q <= m \<and> m < n * (Suc q)) = (q = ((m::nat) div n))"
   1.642 +  "0 < n \<Longrightarrow> (n * q \<le> m \<and> m < n * (Suc q)) = (q = ((m::nat) div n))"
   1.643    apply (rule iffI)
   1.644    apply (rule_tac a=m and r = "m - n * q" and r' = "m mod n" in unique_quotient)
   1.645    apply (simp_all add: quorem_def, arith)
   1.646 @@ -103,7 +704,7 @@
   1.647  
   1.648  theorem split_div':
   1.649    "P ((m::nat) div n) = ((n = 0 \<and> P 0) \<or>
   1.650 -   (\<exists>q. (n * q <= m \<and> m < n * (Suc q)) \<and> P q))"
   1.651 +   (\<exists>q. (n * q \<le> m \<and> m < n * (Suc q)) \<and> P q))"
   1.652    apply (case_tac "0 < n")
   1.653    apply (simp only: add: split_div_lemma)
   1.654    apply (simp_all add: DIVISION_BY_ZERO_DIV)
   1.655 @@ -148,6 +749,106 @@
   1.656    apply arith
   1.657    done
   1.658  
   1.659 +ML
   1.660 +{*
   1.661 +val div_def = thm "div_def"
   1.662 +val mod_def = thm "mod_def"
   1.663 +val dvd_def = thm "dvd_def"
   1.664 +val quorem_def = thm "quorem_def"
   1.665 +
   1.666 +val wf_less_trans = thm "wf_less_trans";
   1.667 +val mod_eq = thm "mod_eq";
   1.668 +val div_eq = thm "div_eq";
   1.669 +val DIVISION_BY_ZERO_DIV = thm "DIVISION_BY_ZERO_DIV";
   1.670 +val DIVISION_BY_ZERO_MOD = thm "DIVISION_BY_ZERO_MOD";
   1.671 +val mod_less = thm "mod_less";
   1.672 +val mod_geq = thm "mod_geq";
   1.673 +val le_mod_geq = thm "le_mod_geq";
   1.674 +val mod_if = thm "mod_if";
   1.675 +val mod_1 = thm "mod_1";
   1.676 +val mod_self = thm "mod_self";
   1.677 +val mod_add_self2 = thm "mod_add_self2";
   1.678 +val mod_add_self1 = thm "mod_add_self1";
   1.679 +val mod_mult_self1 = thm "mod_mult_self1";
   1.680 +val mod_mult_self2 = thm "mod_mult_self2";
   1.681 +val mod_mult_distrib = thm "mod_mult_distrib";
   1.682 +val mod_mult_distrib2 = thm "mod_mult_distrib2";
   1.683 +val mod_mult_self_is_0 = thm "mod_mult_self_is_0";
   1.684 +val mod_mult_self1_is_0 = thm "mod_mult_self1_is_0";
   1.685 +val div_less = thm "div_less";
   1.686 +val div_geq = thm "div_geq";
   1.687 +val le_div_geq = thm "le_div_geq";
   1.688 +val div_if = thm "div_if";
   1.689 +val mod_div_equality = thm "mod_div_equality";
   1.690 +val mod_div_equality2 = thm "mod_div_equality2";
   1.691 +val div_mod_equality = thm "div_mod_equality";
   1.692 +val div_mod_equality2 = thm "div_mod_equality2";
   1.693 +val mult_div_cancel = thm "mult_div_cancel";
   1.694 +val mod_less_divisor = thm "mod_less_divisor";
   1.695 +val div_mult_self_is_m = thm "div_mult_self_is_m";
   1.696 +val div_mult_self1_is_m = thm "div_mult_self1_is_m";
   1.697 +val unique_quotient_lemma = thm "unique_quotient_lemma";
   1.698 +val unique_quotient = thm "unique_quotient";
   1.699 +val unique_remainder = thm "unique_remainder";
   1.700 +val div_0 = thm "div_0";
   1.701 +val mod_0 = thm "mod_0";
   1.702 +val div_mult1_eq = thm "div_mult1_eq";
   1.703 +val mod_mult1_eq = thm "mod_mult1_eq";
   1.704 +val mod_mult1_eq' = thm "mod_mult1_eq'";
   1.705 +val mod_mult_distrib_mod = thm "mod_mult_distrib_mod";
   1.706 +val div_add1_eq = thm "div_add1_eq";
   1.707 +val mod_add1_eq = thm "mod_add1_eq";
   1.708 +val mod_lemma = thm "mod_lemma";
   1.709 +val div_mult2_eq = thm "div_mult2_eq";
   1.710 +val mod_mult2_eq = thm "mod_mult2_eq";
   1.711 +val div_mult_mult_lemma = thm "div_mult_mult_lemma";
   1.712 +val div_mult_mult1 = thm "div_mult_mult1";
   1.713 +val div_mult_mult2 = thm "div_mult_mult2";
   1.714 +val div_1 = thm "div_1";
   1.715 +val div_self = thm "div_self";
   1.716 +val div_add_self2 = thm "div_add_self2";
   1.717 +val div_add_self1 = thm "div_add_self1";
   1.718 +val div_mult_self1 = thm "div_mult_self1";
   1.719 +val div_mult_self2 = thm "div_mult_self2";
   1.720 +val div_le_mono = thm "div_le_mono";
   1.721 +val div_le_mono2 = thm "div_le_mono2";
   1.722 +val div_le_dividend = thm "div_le_dividend";
   1.723 +val div_less_dividend = thm "div_less_dividend";
   1.724 +val mod_Suc = thm "mod_Suc";
   1.725 +val dvdI = thm "dvdI";
   1.726 +val dvdE = thm "dvdE";
   1.727 +val dvd_0_right = thm "dvd_0_right";
   1.728 +val dvd_0_left = thm "dvd_0_left";
   1.729 +val dvd_0_left_iff = thm "dvd_0_left_iff";
   1.730 +val dvd_1_left = thm "dvd_1_left";
   1.731 +val dvd_1_iff_1 = thm "dvd_1_iff_1";
   1.732 +val dvd_refl = thm "dvd_refl";
   1.733 +val dvd_trans = thm "dvd_trans";
   1.734 +val dvd_anti_sym = thm "dvd_anti_sym";
   1.735 +val dvd_add = thm "dvd_add";
   1.736 +val dvd_diff = thm "dvd_diff";
   1.737 +val dvd_diffD = thm "dvd_diffD";
   1.738 +val dvd_diffD1 = thm "dvd_diffD1";
   1.739 +val dvd_mult = thm "dvd_mult";
   1.740 +val dvd_mult2 = thm "dvd_mult2";
   1.741 +val dvd_reduce = thm "dvd_reduce";
   1.742 +val dvd_mod = thm "dvd_mod";
   1.743 +val dvd_mod_imp_dvd = thm "dvd_mod_imp_dvd";
   1.744 +val dvd_mod_iff = thm "dvd_mod_iff";
   1.745 +val dvd_mult_cancel = thm "dvd_mult_cancel";
   1.746 +val dvd_mult_cancel1 = thm "dvd_mult_cancel1";
   1.747 +val dvd_mult_cancel2 = thm "dvd_mult_cancel2";
   1.748 +val mult_dvd_mono = thm "mult_dvd_mono";
   1.749 +val dvd_mult_left = thm "dvd_mult_left";
   1.750 +val dvd_mult_right = thm "dvd_mult_right";
   1.751 +val dvd_imp_le = thm "dvd_imp_le";
   1.752 +val dvd_eq_mod_eq_0 = thm "dvd_eq_mod_eq_0";
   1.753 +val dvd_mult_div_cancel = thm "dvd_mult_div_cancel";
   1.754 +val mod_eq_0_iff = thm "mod_eq_0_iff";
   1.755 +val mod_eqD = thm "mod_eqD";
   1.756 +*}
   1.757 +
   1.758 +
   1.759  (*
   1.760  lemma split_div:
   1.761  assumes m: "m \<noteq> 0"
     2.1 --- a/src/HOL/Divides_lemmas.ML	Mon Nov 24 15:33:07 2003 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,734 +0,0 @@
     2.4 -(*  Title:      HOL/Divides.ML
     2.5 -    ID:         $Id$
     2.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 -    Copyright   1993  University of Cambridge
     2.8 -
     2.9 -The division operators div, mod and the divides relation "dvd"
    2.10 -*)
    2.11 -
    2.12 -(* ML legacy bindings *)
    2.13 -
    2.14 -val div_def = thm "div_def";
    2.15 -val mod_def = thm "mod_def";
    2.16 -val dvd_def = thm "dvd_def";
    2.17 -val quorem_def = thm "quorem_def";
    2.18 -
    2.19 -structure Divides =
    2.20 -struct
    2.21 - val div_def = div_def
    2.22 - val mod_def = mod_def
    2.23 - val dvd_def = dvd_def
    2.24 - val quorem_def = quorem_def
    2.25 -end;
    2.26 -
    2.27 -(** Less-then properties **)
    2.28 -
    2.29 -bind_thm ("wf_less_trans", [eq_reflection, wf_pred_nat RS wf_trancl] MRS 
    2.30 -                    def_wfrec RS trans);
    2.31 -
    2.32 -Goal "(%m. m mod n) = wfrec (trancl pred_nat) \
    2.33 -\                           (%f j. if j<n | n=0 then j else f (j-n))";
    2.34 -by (simp_tac (simpset() addsimps [mod_def]) 1);
    2.35 -qed "mod_eq";
    2.36 -
    2.37 -Goal "(%m. m div n) = wfrec (trancl pred_nat) \
    2.38 -\            (%f j. if j<n | n=0 then 0 else Suc (f (j-n)))";
    2.39 -by (simp_tac (simpset() addsimps [div_def]) 1);
    2.40 -qed "div_eq";
    2.41 -
    2.42 -
    2.43 -(** Aribtrary definitions for division by zero.  Useful to simplify 
    2.44 -    certain equations **)
    2.45 -
    2.46 -Goal "a div 0 = (0::nat)";
    2.47 -by (rtac (div_eq RS wf_less_trans) 1);
    2.48 -by (Asm_simp_tac 1);
    2.49 -qed "DIVISION_BY_ZERO_DIV";  (*NOT for adding to default simpset*)
    2.50 -
    2.51 -Goal "a mod 0 = (a::nat)";
    2.52 -by (rtac (mod_eq RS wf_less_trans) 1);
    2.53 -by (Asm_simp_tac 1);
    2.54 -qed "DIVISION_BY_ZERO_MOD";  (*NOT for adding to default simpset*)
    2.55 -
    2.56 -fun div_undefined_case_tac s i =
    2.57 -  case_tac s i THEN 
    2.58 -  Full_simp_tac (i+1) THEN
    2.59 -  asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO_DIV, 
    2.60 -				    DIVISION_BY_ZERO_MOD]) i;
    2.61 -
    2.62 -(*** Remainder ***)
    2.63 -
    2.64 -Goal "m<n ==> m mod n = (m::nat)";
    2.65 -by (rtac (mod_eq RS wf_less_trans) 1);
    2.66 -by (Asm_simp_tac 1);
    2.67 -qed "mod_less";
    2.68 -Addsimps [mod_less];
    2.69 -
    2.70 -Goal "~ m < (n::nat) ==> m mod n = (m-n) mod n";
    2.71 -by (div_undefined_case_tac "n=0" 1);
    2.72 -by (rtac (mod_eq RS wf_less_trans) 1);
    2.73 -by (asm_simp_tac (simpset() addsimps [diff_less, cut_apply, less_eq]) 1);
    2.74 -qed "mod_geq";
    2.75 -
    2.76 -(*Avoids the ugly ~m<n above*)
    2.77 -Goal "(n::nat) <= m ==> m mod n = (m-n) mod n";
    2.78 -by (asm_simp_tac (simpset() addsimps [mod_geq, not_less_iff_le]) 1);
    2.79 -qed "le_mod_geq";
    2.80 -
    2.81 -Goal "m mod (n::nat) = (if m<n then m else (m-n) mod n)";
    2.82 -by (asm_simp_tac (simpset() addsimps [mod_geq]) 1);
    2.83 -qed "mod_if";
    2.84 -
    2.85 -Goal "m mod Suc 0 = 0";
    2.86 -by (induct_tac "m" 1);
    2.87 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_geq])));
    2.88 -qed "mod_1";
    2.89 -Addsimps [mod_1];
    2.90 -
    2.91 -Goal "n mod n = (0::nat)";
    2.92 -by (div_undefined_case_tac "n=0" 1);
    2.93 -by (asm_simp_tac (simpset() addsimps [mod_geq]) 1);
    2.94 -qed "mod_self";
    2.95 -Addsimps [mod_self];
    2.96 -
    2.97 -Goal "(m+n) mod n = m mod (n::nat)";
    2.98 -by (subgoal_tac "(n + m) mod n = (n+m-n) mod n" 1);
    2.99 -by (stac (mod_geq RS sym) 2);
   2.100 -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_commute])));
   2.101 -qed "mod_add_self2";
   2.102 -
   2.103 -Goal "(n+m) mod n = m mod (n::nat)";
   2.104 -by (asm_simp_tac (simpset() addsimps [add_commute, mod_add_self2]) 1);
   2.105 -qed "mod_add_self1";
   2.106 -
   2.107 -Addsimps [mod_add_self1, mod_add_self2];
   2.108 -
   2.109 -Goal "(m + k*n) mod n = m mod (n::nat)";
   2.110 -by (induct_tac "k" 1);
   2.111 -by (ALLGOALS
   2.112 -    (asm_simp_tac 
   2.113 -     (simpset() addsimps [read_instantiate [("y","n")] add_left_commute])));
   2.114 -qed "mod_mult_self1";
   2.115 -
   2.116 -Goal "(m + n*k) mod n = m mod (n::nat)";
   2.117 -by (asm_simp_tac (simpset() addsimps [mult_commute, mod_mult_self1]) 1);
   2.118 -qed "mod_mult_self2";
   2.119 -
   2.120 -Addsimps [mod_mult_self1, mod_mult_self2];
   2.121 -
   2.122 -Goal "(m mod n) * (k::nat) = (m*k) mod (n*k)";
   2.123 -by (div_undefined_case_tac "n=0" 1);
   2.124 -by (div_undefined_case_tac "k=0" 1);
   2.125 -by (induct_thm_tac nat_less_induct "m" 1);
   2.126 -by (stac mod_if 1);
   2.127 -by (Asm_simp_tac 1);
   2.128 -by (asm_simp_tac (simpset() addsimps [mod_geq, 
   2.129 -				      diff_less, diff_mult_distrib]) 1);
   2.130 -qed "mod_mult_distrib";
   2.131 -
   2.132 -Goal "(k::nat) * (m mod n) = (k*m) mod (k*n)";
   2.133 -by (asm_simp_tac 
   2.134 -    (simpset() addsimps [read_instantiate [("m","k")] mult_commute, 
   2.135 -			 mod_mult_distrib]) 1);
   2.136 -qed "mod_mult_distrib2";
   2.137 -
   2.138 -Goal "(m*n) mod n = (0::nat)";
   2.139 -by (div_undefined_case_tac "n=0" 1);
   2.140 -by (induct_tac "m" 1);
   2.141 -by (Asm_simp_tac 1);
   2.142 -by (rename_tac "k" 1);
   2.143 -by (cut_inst_tac [("m","k*n"),("n","n")] mod_add_self2 1);
   2.144 -by (asm_full_simp_tac (simpset() addsimps [add_commute]) 1);
   2.145 -qed "mod_mult_self_is_0";
   2.146 -
   2.147 -Goal "(n*m) mod n = (0::nat)";
   2.148 -by (simp_tac (simpset() addsimps [mult_commute, mod_mult_self_is_0]) 1);
   2.149 -qed "mod_mult_self1_is_0";
   2.150 -Addsimps [mod_mult_self_is_0, mod_mult_self1_is_0];
   2.151 -
   2.152 -
   2.153 -(*** Quotient ***)
   2.154 -
   2.155 -Goal "m<n ==> m div n = (0::nat)";
   2.156 -by (rtac (div_eq RS wf_less_trans) 1);
   2.157 -by (Asm_simp_tac 1);
   2.158 -qed "div_less";
   2.159 -Addsimps [div_less];
   2.160 -
   2.161 -Goal "[| 0<n;  ~m<n |] ==> m div n = Suc((m-n) div n)";
   2.162 -by (rtac (div_eq RS wf_less_trans) 1);
   2.163 -by (asm_simp_tac (simpset() addsimps [diff_less, cut_apply, less_eq]) 1);
   2.164 -qed "div_geq";
   2.165 -
   2.166 -(*Avoids the ugly ~m<n above*)
   2.167 -Goal "[| 0<n;  n<=m |] ==> m div n = Suc((m-n) div n)";
   2.168 -by (asm_simp_tac (simpset() addsimps [div_geq, not_less_iff_le]) 1);
   2.169 -qed "le_div_geq";
   2.170 -
   2.171 -Goal "0<n ==> m div n = (if m<n then 0 else Suc((m-n) div n))";
   2.172 -by (asm_simp_tac (simpset() addsimps [div_geq]) 1);
   2.173 -qed "div_if";
   2.174 -
   2.175 -
   2.176 -(*Main Result about quotient and remainder.*)
   2.177 -Goal "(m div n)*n + m mod n = (m::nat)";
   2.178 -by (div_undefined_case_tac "n=0" 1);
   2.179 -by (induct_thm_tac nat_less_induct "m" 1);
   2.180 -by (stac mod_if 1);
   2.181 -by (ALLGOALS (asm_simp_tac 
   2.182 -	      (simpset() addsimps [add_assoc, div_geq,
   2.183 -				   add_diff_inverse, diff_less])));
   2.184 -qed "mod_div_equality";
   2.185 -
   2.186 -Goal "n * (m div n) + m mod n = (m::nat)";
   2.187 -by(cut_inst_tac [("m","m"),("n","n")] mod_div_equality 1);
   2.188 -by(asm_full_simp_tac (simpset() addsimps [mult_commute]) 1);
   2.189 -qed "mod_div_equality2";
   2.190 -
   2.191 -(*-----------------------------------------------------------------------*)
   2.192 -(*Simproc for cancelling div and mod                                     *)
   2.193 -(*-----------------------------------------------------------------------*)
   2.194 -
   2.195 -Goal "((m div n)*n + m mod n) + k = (m::nat) + k";
   2.196 -by(simp_tac (simpset() addsimps [mod_div_equality]) 1);
   2.197 -qed "div_mod_equality";
   2.198 -
   2.199 -Goal "(n*(m div n) + m mod n) + k = (m::nat) + k";
   2.200 -by(simp_tac (simpset() addsimps [thm"mod_div_equality2"]) 1);
   2.201 -qed "div_mod_equality2";
   2.202 -
   2.203 -structure CancelDivModData =
   2.204 -struct
   2.205 -
   2.206 -val div_name = "Divides.op div";
   2.207 -val mod_name = "Divides.op mod";
   2.208 -val mk_binop = HOLogic.mk_binop;
   2.209 -val mk_sum = NatArithUtils.mk_sum;
   2.210 -val dest_sum = NatArithUtils.dest_sum;
   2.211 -
   2.212 -(*logic*)
   2.213 -
   2.214 -val div_mod_eqs = map mk_meta_eq [div_mod_equality,div_mod_equality2]
   2.215 -
   2.216 -val trans = trans
   2.217 -
   2.218 -val prove_eq_sums =
   2.219 -  let val simps = add_0 :: add_0_right :: add_ac
   2.220 -  in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all simps) end
   2.221 -
   2.222 -end;
   2.223 -
   2.224 -structure CancelDivMod = CancelDivModFun(CancelDivModData);
   2.225 -
   2.226 -val cancel_div_mod_proc = NatArithUtils.prep_simproc
   2.227 -      ("cancel_div_mod", ["(m::nat) + n"], CancelDivMod.proc);
   2.228 -
   2.229 -Addsimprocs[cancel_div_mod_proc];
   2.230 -
   2.231 -
   2.232 -(* a simple rearrangement of mod_div_equality: *)
   2.233 -Goal "(n::nat) * (m div n) = m - (m mod n)";
   2.234 -by (cut_inst_tac [("m","m"),("n","n")] mod_div_equality2 1);
   2.235 -by (arith_tac 1);
   2.236 -qed "mult_div_cancel";
   2.237 -
   2.238 -Goal "0<n ==> m mod n < (n::nat)";
   2.239 -by (induct_thm_tac nat_less_induct "m" 1);
   2.240 -by (case_tac "na<n" 1);
   2.241 -(*case n le na*)
   2.242 -by (asm_full_simp_tac (simpset() addsimps [mod_geq, diff_less]) 2);
   2.243 -(*case na<n*)
   2.244 -by (Asm_simp_tac 1);
   2.245 -qed "mod_less_divisor";
   2.246 -Addsimps [mod_less_divisor];
   2.247 -
   2.248 -(*** More division laws ***)
   2.249 -
   2.250 -Goal "0<n ==> (m*n) div n = (m::nat)";
   2.251 -by (cut_inst_tac [("m", "m*n"),("n","n")] mod_div_equality 1);
   2.252 -by Auto_tac;
   2.253 -qed "div_mult_self_is_m";
   2.254 -
   2.255 -Goal "0<n ==> (n*m) div n = (m::nat)";
   2.256 -by (asm_simp_tac (simpset() addsimps [mult_commute, div_mult_self_is_m]) 1);
   2.257 -qed "div_mult_self1_is_m";
   2.258 -Addsimps [div_mult_self_is_m, div_mult_self1_is_m];
   2.259 -
   2.260 -(*mod_mult_distrib2 above is the counterpart for remainder*)
   2.261 -
   2.262 -
   2.263 -(*** Proving facts about div and mod using quorem ***)
   2.264 -
   2.265 -Goal "[| b*q' + r'  <= b*q + r;  0 < b;  r < b |] \
   2.266 -\     ==> q' <= (q::nat)";
   2.267 -by (rtac leI 1); 
   2.268 -by (stac less_iff_Suc_add 1);
   2.269 -by (auto_tac (claset(), simpset() addsimps [add_mult_distrib2]));   
   2.270 -qed "unique_quotient_lemma";
   2.271 -
   2.272 -Goal "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  0 < b |] \
   2.273 -\     ==> q = q'";
   2.274 -by (asm_full_simp_tac 
   2.275 -    (simpset() addsimps split_ifs @ [Divides.quorem_def]) 1);  
   2.276 -by (REPEAT 
   2.277 -    (blast_tac (claset() addIs [order_antisym]
   2.278 -			 addDs [order_eq_refl RS unique_quotient_lemma, 
   2.279 -				sym]) 1));
   2.280 -qed "unique_quotient";
   2.281 -
   2.282 -Goal "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  0 < b |] \
   2.283 -\     ==> r = r'";
   2.284 -by (subgoal_tac "q = q'" 1);
   2.285 -by (blast_tac (claset() addIs [unique_quotient]) 2);
   2.286 -by (asm_full_simp_tac (simpset() addsimps [Divides.quorem_def]) 1);
   2.287 -qed "unique_remainder";
   2.288 -
   2.289 -Goal "0 < b ==> quorem ((a, b), (a div b, a mod b))";
   2.290 -by (auto_tac
   2.291 -    (claset() addEs [sym],
   2.292 -     simpset() addsimps mult_ac@[Divides.quorem_def]));
   2.293 -qed "quorem_div_mod";
   2.294 -
   2.295 -Goal "[| quorem((a,b),(q,r));  0 < b |] ==> a div b = q";
   2.296 -by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS unique_quotient]) 1);
   2.297 -qed "quorem_div";
   2.298 -
   2.299 -Goal "[| quorem((a,b),(q,r));  0 < b |] ==> a mod b = r";
   2.300 -by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS unique_remainder]) 1);
   2.301 -qed "quorem_mod";
   2.302 -
   2.303 -(** A dividend of zero **)
   2.304 -
   2.305 -Goal "0 div m = (0::nat)";
   2.306 -by (div_undefined_case_tac "m=0" 1);
   2.307 -by (Asm_simp_tac 1);
   2.308 -qed "div_0"; 
   2.309 -
   2.310 -Goal "0 mod m = (0::nat)";
   2.311 -by (div_undefined_case_tac "m=0" 1);
   2.312 -by (Asm_simp_tac 1);
   2.313 -qed "mod_0"; 
   2.314 -Addsimps [div_0, mod_0];
   2.315 -
   2.316 -(** proving (a*b) div c = a * (b div c) + a * (b mod c) **)
   2.317 -
   2.318 -Goal "[| quorem((b,c),(q,r));  0 < c |] \
   2.319 -\     ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))";
   2.320 -by (auto_tac
   2.321 -    (claset(),
   2.322 -     simpset() addsimps split_ifs@mult_ac@
   2.323 -                        [Divides.quorem_def, add_mult_distrib2]));
   2.324 -val lemma = result();
   2.325 -
   2.326 -Goal "(a*b) div c = a*(b div c) + a*(b mod c) div (c::nat)";
   2.327 -by (div_undefined_case_tac "c = 0" 1);
   2.328 -by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_div]) 1);
   2.329 -qed "div_mult1_eq";
   2.330 -
   2.331 -Goal "(a*b) mod c = a*(b mod c) mod (c::nat)";
   2.332 -by (div_undefined_case_tac "c = 0" 1);
   2.333 -by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_mod]) 1);
   2.334 -qed "mod_mult1_eq";
   2.335 -
   2.336 -Goal "(a*b) mod (c::nat) = ((a mod c) * b) mod c";
   2.337 -by (rtac trans 1);
   2.338 -by (res_inst_tac [("s","b*a mod c")] trans 1);
   2.339 -by (rtac mod_mult1_eq 2);
   2.340 -by (ALLGOALS (simp_tac (simpset() addsimps [mult_commute])));
   2.341 -qed "mod_mult1_eq'";
   2.342 -
   2.343 -Goal "(a*b) mod (c::nat) = ((a mod c) * (b mod c)) mod c";
   2.344 -by (rtac (mod_mult1_eq' RS trans) 1);
   2.345 -by (rtac mod_mult1_eq 1);
   2.346 -qed "mod_mult_distrib_mod";
   2.347 -
   2.348 -(** proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) **)
   2.349 -
   2.350 -Goal "[| quorem((a,c),(aq,ar));  quorem((b,c),(bq,br));  0 < c |] \
   2.351 -\     ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))";
   2.352 -by (auto_tac
   2.353 -    (claset(),
   2.354 -     simpset() addsimps split_ifs@mult_ac@
   2.355 -                        [Divides.quorem_def, add_mult_distrib2]));
   2.356 -val lemma = result();
   2.357 -
   2.358 -(*NOT suitable for rewriting: the RHS has an instance of the LHS*)
   2.359 -Goal "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)";
   2.360 -by (div_undefined_case_tac "c = 0" 1);
   2.361 -by (blast_tac (claset() addIs [[quorem_div_mod,quorem_div_mod]
   2.362 -			       MRS lemma RS quorem_div]) 1);
   2.363 -qed "div_add1_eq";
   2.364 -
   2.365 -Goal "(a+b) mod (c::nat) = (a mod c + b mod c) mod c";
   2.366 -by (div_undefined_case_tac "c = 0" 1);
   2.367 -by (blast_tac (claset() addIs [[quorem_div_mod,quorem_div_mod]
   2.368 -			       MRS lemma RS quorem_mod]) 1);
   2.369 -qed "mod_add1_eq";
   2.370 -
   2.371 -
   2.372 -(*** proving  a div (b*c) = (a div b) div c ***)
   2.373 -
   2.374 -(** first, a lemma to bound the remainder **)
   2.375 -
   2.376 -Goal "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c";
   2.377 -by (cut_inst_tac [("m","q"),("n","c")] mod_less_divisor 1);
   2.378 -by (dres_inst_tac [("m","q mod c")] less_imp_Suc_add 2); 
   2.379 -by Auto_tac;  
   2.380 -by (eres_inst_tac [("P","%x. ?lhs < ?rhs x")] ssubst 1); 
   2.381 -by (asm_simp_tac (simpset() addsimps [add_mult_distrib2]) 1);
   2.382 -val mod_lemma = result();
   2.383 -
   2.384 -Goal "[| quorem ((a,b), (q,r));  0 < b;  0 < c |] \
   2.385 -\     ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))";
   2.386 -by (auto_tac  
   2.387 -    (claset(),
   2.388 -     simpset() addsimps mult_ac@
   2.389 -                        [Divides.quorem_def, add_mult_distrib2 RS sym,
   2.390 -			 mod_lemma]));
   2.391 -val lemma = result();
   2.392 -
   2.393 -Goal "a div (b*c) = (a div b) div (c::nat)";
   2.394 -by (div_undefined_case_tac "b=0" 1);
   2.395 -by (div_undefined_case_tac "c=0" 1);
   2.396 -by (force_tac (claset(),
   2.397 -	       simpset() addsimps [quorem_div_mod RS lemma RS quorem_div]) 1);
   2.398 -qed "div_mult2_eq";
   2.399 -
   2.400 -Goal "a mod (b*c) = b*(a div b mod c) + a mod (b::nat)";
   2.401 -by (div_undefined_case_tac "b=0" 1);
   2.402 -by (div_undefined_case_tac "c=0" 1);
   2.403 -by (auto_tac (claset(),
   2.404 -	       simpset() addsimps [mult_commute, 
   2.405 -				   quorem_div_mod RS lemma RS quorem_mod]));
   2.406 -qed "mod_mult2_eq";
   2.407 -
   2.408 -
   2.409 -(*** Cancellation of common factors in "div" ***)
   2.410 -
   2.411 -Goal "[| (0::nat) < b;  0 < c |] ==> (c*a) div (c*b) = a div b";
   2.412 -by (stac div_mult2_eq 1);
   2.413 -by Auto_tac;
   2.414 -val lemma1 = result();
   2.415 -
   2.416 -Goal "(0::nat) < c ==> (c*a) div (c*b) = a div b";
   2.417 -by (div_undefined_case_tac "b = 0" 1);
   2.418 -by (auto_tac
   2.419 -    (claset(), 
   2.420 -     simpset() addsimps [read_instantiate [("x", "b")] linorder_neq_iff, 
   2.421 -			 lemma1, lemma2]));
   2.422 -qed "div_mult_mult1";
   2.423 -
   2.424 -Goal "(0::nat) < c ==> (a*c) div (b*c) = a div b";
   2.425 -by (dtac div_mult_mult1 1);
   2.426 -by (auto_tac (claset(), simpset() addsimps [mult_commute]));
   2.427 -qed "div_mult_mult2";
   2.428 -
   2.429 -Addsimps [div_mult_mult1, div_mult_mult2];
   2.430 -
   2.431 -
   2.432 -(*** Distribution of factors over "mod"
   2.433 -
   2.434 -Could prove these as in Integ/IntDiv.ML, but we already have
   2.435 -mod_mult_distrib and mod_mult_distrib2 above!
   2.436 -
   2.437 -Goal "(c*a) mod (c*b) = (c::nat) * (a mod b)";
   2.438 -qed "mod_mult_mult1";
   2.439 -
   2.440 -Goal "(a*c) mod (b*c) = (a mod b) * (c::nat)";
   2.441 -qed "mod_mult_mult2";
   2.442 - ***)
   2.443 -
   2.444 -(*** Further facts about div and mod ***)
   2.445 -
   2.446 -Goal "m div Suc 0 = m";
   2.447 -by (induct_tac "m" 1);
   2.448 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [div_geq])));
   2.449 -qed "div_1";
   2.450 -Addsimps [div_1];
   2.451 -
   2.452 -Goal "0<n ==> n div n = (1::nat)";
   2.453 -by (asm_simp_tac (simpset() addsimps [div_geq]) 1);
   2.454 -qed "div_self";
   2.455 -Addsimps [div_self];
   2.456 -
   2.457 -Goal "0<n ==> (m+n) div n = Suc (m div n)";
   2.458 -by (subgoal_tac "(n + m) div n = Suc ((n+m-n) div n)" 1);
   2.459 -by (stac (div_geq RS sym) 2);
   2.460 -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_commute])));
   2.461 -qed "div_add_self2";
   2.462 -
   2.463 -Goal "0<n ==> (n+m) div n = Suc (m div n)";
   2.464 -by (asm_simp_tac (simpset() addsimps [add_commute, div_add_self2]) 1);
   2.465 -qed "div_add_self1";
   2.466 -
   2.467 -Goal "!!n::nat. 0<n ==> (m + k*n) div n = k + m div n";
   2.468 -by (stac div_add1_eq 1); 
   2.469 -by (stac div_mult1_eq 1); 
   2.470 -by (Asm_simp_tac 1); 
   2.471 -qed "div_mult_self1";
   2.472 -
   2.473 -Goal "0<n ==> (m + n*k) div n = k + m div (n::nat)";
   2.474 -by (asm_simp_tac (simpset() addsimps [mult_commute, div_mult_self1]) 1);
   2.475 -qed "div_mult_self2";
   2.476 -
   2.477 -Addsimps [div_mult_self1, div_mult_self2];
   2.478 -
   2.479 -(* Monotonicity of div in first argument *)
   2.480 -Goal "ALL m::nat. m <= n --> (m div k) <= (n div k)";
   2.481 -by (div_undefined_case_tac "k=0" 1);
   2.482 -by (induct_thm_tac nat_less_induct "n" 1);
   2.483 -by (Clarify_tac 1);
   2.484 -by (case_tac "n<k" 1);
   2.485 -(* 1  case n<k *)
   2.486 -by (Asm_simp_tac 1);
   2.487 -(* 2  case n >= k *)
   2.488 -by (case_tac "m<k" 1);
   2.489 -(* 2.1  case m<k *)
   2.490 -by (Asm_simp_tac 1);
   2.491 -(* 2.2  case m>=k *)
   2.492 -by (asm_simp_tac (simpset() addsimps [div_geq, diff_less, diff_le_mono]) 1);
   2.493 -qed_spec_mp "div_le_mono";
   2.494 -
   2.495 -(* Antimonotonicity of div in second argument *)
   2.496 -Goal "!!m::nat. [| 0<m; m<=n |] ==> (k div n) <= (k div m)";
   2.497 -by (subgoal_tac "0<n" 1);
   2.498 - by (Asm_simp_tac 2);
   2.499 -by (induct_thm_tac nat_less_induct "k" 1);
   2.500 -by (rename_tac "k" 1);
   2.501 -by (case_tac "k<n" 1);
   2.502 - by (Asm_simp_tac 1);
   2.503 -by (subgoal_tac "~(k<m)" 1);
   2.504 - by (Asm_simp_tac 2);
   2.505 -by (asm_simp_tac (simpset() addsimps [div_geq]) 1);
   2.506 -by (subgoal_tac "(k-n) div n <= (k-m) div n" 1);
   2.507 - by (REPEAT (ares_tac [div_le_mono,diff_le_mono2] 2));
   2.508 -by (rtac le_trans 1);
   2.509 -by (Asm_simp_tac 1);
   2.510 -by (asm_simp_tac (simpset() addsimps [diff_less]) 1);
   2.511 -qed "div_le_mono2";
   2.512 -
   2.513 -Goal "m div n <= (m::nat)";
   2.514 -by (div_undefined_case_tac "n=0" 1);
   2.515 -by (subgoal_tac "m div n <= m div 1" 1);
   2.516 -by (Asm_full_simp_tac 1);
   2.517 -by (rtac div_le_mono2 1);
   2.518 -by (ALLGOALS Asm_simp_tac);
   2.519 -qed "div_le_dividend";
   2.520 -Addsimps [div_le_dividend];
   2.521 -
   2.522 -(* Similar for "less than" *)
   2.523 -Goal "!!n::nat. 1<n ==> (0 < m) --> (m div n < m)";
   2.524 -by (induct_thm_tac nat_less_induct "m" 1);
   2.525 -by (rename_tac "m" 1);
   2.526 -by (case_tac "m<n" 1);
   2.527 - by (Asm_full_simp_tac 1);
   2.528 -by (subgoal_tac "0<n" 1);
   2.529 - by (Asm_simp_tac 2);
   2.530 -by (asm_full_simp_tac (simpset() addsimps [div_geq]) 1);
   2.531 -by (case_tac "n<m" 1);
   2.532 - by (subgoal_tac "(m-n) div n < (m-n)" 1);
   2.533 -  by (REPEAT (ares_tac [impI,less_trans_Suc] 1));
   2.534 -  by (asm_full_simp_tac (simpset() addsimps [diff_less]) 1);
   2.535 - by (asm_full_simp_tac (simpset() addsimps [diff_less]) 1);
   2.536 -(* case n=m *)
   2.537 -by (subgoal_tac "m=n" 1);
   2.538 - by (Asm_simp_tac 2);
   2.539 -by (Asm_simp_tac 1);
   2.540 -qed_spec_mp "div_less_dividend";
   2.541 -Addsimps [div_less_dividend];
   2.542 -
   2.543 -(*** Further facts about mod (mainly for the mutilated chess board ***)
   2.544 -
   2.545 -Goal "Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))";
   2.546 -by (div_undefined_case_tac "n=0" 1);
   2.547 -by (induct_thm_tac nat_less_induct "m" 1);
   2.548 -by (case_tac "Suc(na)<n" 1);
   2.549 -(* case Suc(na) < n *)
   2.550 -by (forward_tac [lessI RS less_trans] 1 
   2.551 -    THEN asm_simp_tac (simpset() addsimps [less_not_refl3]) 1);
   2.552 -(* case n <= Suc(na) *)
   2.553 -by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, le_Suc_eq, 
   2.554 -					   mod_geq]) 1);
   2.555 -by (auto_tac (claset(), 
   2.556 -	      simpset() addsimps [Suc_diff_le, diff_less, le_mod_geq]));
   2.557 -qed "mod_Suc";
   2.558 -
   2.559 -
   2.560 -(************************************************)
   2.561 -(** Divides Relation                           **)
   2.562 -(************************************************)
   2.563 -
   2.564 -Goalw [dvd_def] "n = m * k ==> m dvd n";
   2.565 -by (Blast_tac 1); 
   2.566 -qed "dvdI";
   2.567 -
   2.568 -Goalw [dvd_def] "!!P. [|m dvd n;  !!k. n = m*k ==> P|] ==> P";
   2.569 -by (Blast_tac 1); 
   2.570 -qed "dvdE";
   2.571 -
   2.572 -Goalw [dvd_def] "m dvd (0::nat)";
   2.573 -by (blast_tac (claset() addIs [mult_0_right RS sym]) 1);
   2.574 -qed "dvd_0_right";
   2.575 -AddIffs [dvd_0_right];
   2.576 -
   2.577 -Goalw [dvd_def] "0 dvd m ==> m = (0::nat)";
   2.578 -by Auto_tac;
   2.579 -qed "dvd_0_left";
   2.580 -
   2.581 -Goal "(0 dvd (m::nat)) = (m = 0)";
   2.582 -by (blast_tac (claset() addIs [dvd_0_left]) 1); 
   2.583 -qed "dvd_0_left_iff";
   2.584 -AddIffs [dvd_0_left_iff];
   2.585 -
   2.586 -Goalw [dvd_def] "Suc 0 dvd k";
   2.587 -by (Simp_tac 1);
   2.588 -qed "dvd_1_left";
   2.589 -AddIffs [dvd_1_left];
   2.590 -
   2.591 -Goal "(m dvd Suc 0) = (m = Suc 0)";
   2.592 -by (simp_tac (simpset() addsimps [dvd_def]) 1); 
   2.593 -qed "dvd_1_iff_1";
   2.594 -Addsimps [dvd_1_iff_1];
   2.595 -
   2.596 -Goalw [dvd_def] "m dvd (m::nat)";
   2.597 -by (blast_tac (claset() addIs [mult_1_right RS sym]) 1);
   2.598 -qed "dvd_refl";
   2.599 -Addsimps [dvd_refl];
   2.600 -
   2.601 -Goalw [dvd_def] "[| m dvd n; n dvd p |] ==> m dvd (p::nat)";
   2.602 -by (blast_tac (claset() addIs [mult_assoc] ) 1);
   2.603 -qed "dvd_trans";
   2.604 -
   2.605 -Goalw [dvd_def] "[| m dvd n; n dvd m |] ==> m = (n::nat)";
   2.606 -by (force_tac (claset() addDs [mult_eq_self_implies_10],
   2.607 -	       simpset() addsimps [mult_assoc, mult_eq_1_iff]) 1);
   2.608 -qed "dvd_anti_sym";
   2.609 -
   2.610 -Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m+n :: nat)";
   2.611 -by (blast_tac (claset() addIs [add_mult_distrib2 RS sym]) 1);
   2.612 -qed "dvd_add";
   2.613 -
   2.614 -Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)";
   2.615 -by (blast_tac (claset() addIs [diff_mult_distrib2 RS sym]) 1);
   2.616 -qed "dvd_diff";
   2.617 -
   2.618 -Goal "[| k dvd m-n; k dvd n; n<=m |] ==> k dvd (m::nat)";
   2.619 -by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1);
   2.620 -by (blast_tac (claset() addIs [dvd_add]) 1);
   2.621 -qed "dvd_diffD";
   2.622 -
   2.623 -Goal "[| k dvd m-n; k dvd m; n<=m |] ==> k dvd (n::nat)";
   2.624 -by (dres_inst_tac [("m","m")] dvd_diff 1);
   2.625 -by Auto_tac;  
   2.626 -qed "dvd_diffD1";
   2.627 -
   2.628 -Goalw [dvd_def] "k dvd n ==> k dvd (m*n :: nat)";
   2.629 -by (blast_tac (claset() addIs [mult_left_commute]) 1);
   2.630 -qed "dvd_mult";
   2.631 -
   2.632 -Goal "k dvd m ==> k dvd (m*n :: nat)";
   2.633 -by (stac mult_commute 1);
   2.634 -by (etac dvd_mult 1);
   2.635 -qed "dvd_mult2";
   2.636 -
   2.637 -(* k dvd (m*k) *)
   2.638 -AddIffs [dvd_refl RS dvd_mult, dvd_refl RS dvd_mult2];
   2.639 -
   2.640 -Goal "(k dvd n + k) = (k dvd (n::nat))";
   2.641 -by (rtac iffI 1);
   2.642 -by (etac dvd_add 2);
   2.643 -by (rtac dvd_refl 2);
   2.644 -by (subgoal_tac "n = (n+k)-k" 1);
   2.645 -by  (Simp_tac 2);
   2.646 -by (etac ssubst 1);
   2.647 -by (etac dvd_diff 1);
   2.648 -by (rtac dvd_refl 1);
   2.649 -qed "dvd_reduce";
   2.650 -
   2.651 -Goalw [dvd_def] "!!n::nat. [| f dvd m; f dvd n |] ==> f dvd m mod n";
   2.652 -by (div_undefined_case_tac "n=0" 1);
   2.653 -by Auto_tac; 
   2.654 -by (blast_tac (claset() addIs [mod_mult_distrib2 RS sym]) 1);  
   2.655 -qed "dvd_mod";
   2.656 -
   2.657 -Goal "[| (k::nat) dvd m mod n;  k dvd n |] ==> k dvd m";
   2.658 -by (subgoal_tac "k dvd (m div n)*n + m mod n" 1);
   2.659 -by (asm_simp_tac (HOL_basic_ss addsimps [dvd_add, dvd_mult]) 2);
   2.660 -by (asm_full_simp_tac (simpset() addsimps [mod_div_equality]) 1);
   2.661 -qed "dvd_mod_imp_dvd";
   2.662 -
   2.663 -Goal "k dvd n ==> ((k::nat) dvd m mod n) = (k dvd m)";
   2.664 -by (blast_tac (claset() addIs [dvd_mod_imp_dvd, dvd_mod]) 1); 
   2.665 -qed "dvd_mod_iff";
   2.666 -
   2.667 -Goalw [dvd_def]  "!!k::nat. [| k*m dvd k*n; 0<k |] ==> m dvd n";
   2.668 -by (etac exE 1);
   2.669 -by (asm_full_simp_tac (simpset() addsimps mult_ac) 1);
   2.670 -qed "dvd_mult_cancel";
   2.671 -
   2.672 -Goal "0<m ==> (m*n dvd m) = (n = (1::nat))";
   2.673 -by Auto_tac;  
   2.674 -by (subgoal_tac "m*n dvd m*1" 1);
   2.675 -by (dtac dvd_mult_cancel 1); 
   2.676 -by Auto_tac;  
   2.677 -qed "dvd_mult_cancel1";
   2.678 -
   2.679 -Goal "0<m ==> (n*m dvd m) = (n = (1::nat))";
   2.680 -by (stac mult_commute 1); 
   2.681 -by (etac dvd_mult_cancel1 1); 
   2.682 -qed "dvd_mult_cancel2";
   2.683 -
   2.684 -Goalw [dvd_def] "[| i dvd m; j dvd n|] ==> i*j dvd (m*n :: nat)";
   2.685 -by (Clarify_tac 1);
   2.686 -by (res_inst_tac [("x","k*ka")] exI 1);
   2.687 -by (asm_simp_tac (simpset() addsimps mult_ac) 1);
   2.688 -qed "mult_dvd_mono";
   2.689 -
   2.690 -Goalw [dvd_def] "(i*j :: nat) dvd k ==> i dvd k";
   2.691 -by (full_simp_tac (simpset() addsimps [mult_assoc]) 1);
   2.692 -by (Blast_tac 1);
   2.693 -qed "dvd_mult_left";
   2.694 -
   2.695 -Goalw [dvd_def] "(i*j :: nat) dvd k ==> j dvd k";
   2.696 -by (Clarify_tac 1);
   2.697 -by (res_inst_tac [("x","i*k")] exI 1);
   2.698 -by (simp_tac (simpset() addsimps mult_ac) 1);
   2.699 -qed "dvd_mult_right";
   2.700 -
   2.701 -Goalw [dvd_def] "[| k dvd n; 0 < n |] ==> k <= (n::nat)";
   2.702 -by (Clarify_tac 1);
   2.703 -by (ALLGOALS (full_simp_tac (simpset() addsimps [zero_less_mult_iff])));
   2.704 -by (etac conjE 1);
   2.705 -by (rtac le_trans 1);
   2.706 -by (rtac (le_refl RS mult_le_mono) 2);
   2.707 -by (etac Suc_leI 2);
   2.708 -by (Simp_tac 1);
   2.709 -qed "dvd_imp_le";
   2.710 -
   2.711 -Goalw [dvd_def] "!!k::nat. (k dvd n) = (n mod k = 0)";
   2.712 -by (div_undefined_case_tac "k=0" 1);
   2.713 -by Safe_tac;
   2.714 -by (asm_simp_tac (simpset() addsimps [mult_commute]) 1);
   2.715 -by (res_inst_tac [("t","n"),("n1","k")] (mod_div_equality RS subst) 1);
   2.716 -by (stac mult_commute 1);
   2.717 -by (Asm_simp_tac 1);
   2.718 -qed "dvd_eq_mod_eq_0";
   2.719 -
   2.720 -Goal "n dvd m ==> n * (m div n) = (m::nat)";
   2.721 -by (subgoal_tac "m mod n = 0" 1);
   2.722 - by (asm_full_simp_tac (simpset() addsimps [mult_div_cancel]) 1);
   2.723 -by (asm_full_simp_tac (HOL_basic_ss addsimps [dvd_eq_mod_eq_0]) 1);
   2.724 -qed "dvd_mult_div_cancel";
   2.725 -
   2.726 -Goal "(m mod d = 0) = (EX q::nat. m = d*q)";
   2.727 -by (auto_tac (claset(), 
   2.728 -     simpset() addsimps [dvd_eq_mod_eq_0 RS sym, dvd_def]));  
   2.729 -qed "mod_eq_0_iff";
   2.730 -AddSDs [mod_eq_0_iff RS iffD1];
   2.731 -
   2.732 -(*Loses information, namely we also have r<d provided d is nonzero*)
   2.733 -Goal "(m mod d = r) ==> EX q::nat. m = r + q*d";
   2.734 -by (cut_inst_tac [("m","m")] mod_div_equality 1);
   2.735 -by (full_simp_tac (HOL_basic_ss addsimps add_ac) 1); 
   2.736 -by (blast_tac (claset() addIs [sym]) 1); 
   2.737 -qed "mod_eqD";
     3.1 --- a/src/HOL/Integ/Int.thy	Mon Nov 24 15:33:07 2003 +0100
     3.2 +++ b/src/HOL/Integ/Int.thy	Tue Nov 25 10:37:03 2003 +0100
     3.3 @@ -239,15 +239,6 @@
     3.4  
     3.5  subsection{*Instances of the equations above, for zero*}
     3.6  
     3.7 -(*instantiate a variable to zero and simplify*)
     3.8 -
     3.9 -declare zless_zminus [of 0, simplified, simp]
    3.10 -declare zminus_zless [of _ 0, simplified, simp]
    3.11 -declare zle_zminus   [of 0, simplified, simp]
    3.12 -declare zminus_zle [of _ 0, simplified, simp]
    3.13 -declare equation_zminus [of 0, simplified, simp]
    3.14 -declare zminus_equation [of _ 0, simplified, simp]
    3.15 -
    3.16  lemma negative_zless_0: "- (int (Suc n)) < 0"
    3.17  by (simp add: zless_def)
    3.18  
    3.19 @@ -343,53 +334,10 @@
    3.20  apply (auto simp add: nat_mono_iff linorder_not_less)
    3.21  done
    3.22  
    3.23 -(* a case theorem distinguishing non-negative and negative int *)  
    3.24 -
    3.25 -lemma int_cases: 
    3.26 -     "[|!! n. z = int n ==> P;  !! n. z =  - (int (Suc n)) ==> P |] ==> P"
    3.27 -apply (case_tac "neg z")
    3.28 -apply (fast dest!: negD)
    3.29 -apply (drule not_neg_nat [symmetric], auto) 
    3.30 -done
    3.31 -
    3.32 -
    3.33 -subsection{*Monotonicity of Multiplication*}
    3.34 -
    3.35 -lemma zmult_zle_mono1_lemma: "i \<le> (j::int) ==> i * int k \<le> j * int k"
    3.36 -apply (induct_tac "k")
    3.37 -apply (simp_all (no_asm_simp) add: int_Suc zadd_zmult_distrib2 zadd_zle_mono int_Suc0_eq_1)
    3.38 -done
    3.39 -
    3.40 -lemma zmult_zle_mono1: "[| i \<le> j;  (0::int) \<le> k |] ==> i*k \<le> j*k"
    3.41 -apply (rule_tac t = k in not_neg_nat [THEN subst])
    3.42 -apply (erule_tac [2] zmult_zle_mono1_lemma)
    3.43 -apply (simp (no_asm_use) add: not_neg_eq_ge_0)
    3.44 -done
    3.45  
    3.46 -lemma zmult_zle_mono1_neg: "[| i \<le> j;  k \<le> (0::int) |] ==> j*k \<le> i*k"
    3.47 -apply (rule zminus_zle_zminus [THEN iffD1])
    3.48 -apply (simp add: zmult_zminus_right [symmetric] zmult_zle_mono1 zle_zminus)
    3.49 -done
    3.50 -
    3.51 -lemma zmult_zle_mono2: "[| i \<le> j;  (0::int) \<le> k |] ==> k*i \<le> k*j"
    3.52 -apply (drule zmult_zle_mono1)
    3.53 -apply (simp_all add: zmult_commute)
    3.54 -done
    3.55 +subsection{*Strict Monotonicity of Multiplication*}
    3.56  
    3.57 -lemma zmult_zle_mono2_neg: "[| i \<le> j;  k \<le> (0::int) |] ==> k*j \<le> k*i"
    3.58 -apply (drule zmult_zle_mono1_neg)
    3.59 -apply (simp_all add: zmult_commute)
    3.60 -done
    3.61 -
    3.62 -(* \<le> monotonicity, BOTH arguments*)
    3.63 -lemma zmult_zle_mono: "[| i \<le> j;  k \<le> l;  (0::int) \<le> j;  (0::int) \<le> k |] ==> i*k \<le> j*l"
    3.64 -apply (erule zmult_zle_mono1 [THEN order_trans], assumption)
    3.65 -apply (erule zmult_zle_mono2, assumption)
    3.66 -done
    3.67 -
    3.68 -
    3.69 -subsection{*strict, in 1st argument; proof is by induction on k>0*}
    3.70 -
    3.71 +text{*strict, in 1st argument; proof is by induction on k>0*}
    3.72  lemma zmult_zless_mono2_lemma: "i<j ==> 0<k --> int k * i < int k * j"
    3.73  apply (induct_tac "k", simp) 
    3.74  apply (simp add: int_Suc)
    3.75 @@ -423,6 +371,25 @@
    3.76    show "\<bar>i\<bar> = (if i < 0 then -i else i)" by (simp only: zabs_def)
    3.77  qed
    3.78  
    3.79 +subsection{*Monotonicity of Multiplication*}
    3.80 +
    3.81 +lemma zmult_zle_mono1: "[| i \<le> j;  (0::int) \<le> k |] ==> i*k \<le> j*k"
    3.82 +  by (rule mult_right_mono)
    3.83 +
    3.84 +lemma zmult_zle_mono1_neg: "[| i \<le> j;  k \<le> (0::int) |] ==> j*k \<le> i*k"
    3.85 +  by (rule mult_right_mono_neg)
    3.86 +
    3.87 +lemma zmult_zle_mono2: "[| i \<le> j;  (0::int) \<le> k |] ==> k*i \<le> k*j"
    3.88 +  by (rule mult_left_mono)
    3.89 +
    3.90 +lemma zmult_zle_mono2_neg: "[| i \<le> j;  k \<le> (0::int) |] ==> k*j \<le> k*i"
    3.91 +  by (rule mult_left_mono_neg)
    3.92 +
    3.93 +(* \<le> monotonicity, BOTH arguments*)
    3.94 +lemma zmult_zle_mono:
    3.95 +     "[| i \<le> j;  k \<le> l;  (0::int) \<le> j;  (0::int) \<le> k |] ==> i*k \<le> j*l"
    3.96 +  by (rule mult_mono)
    3.97 +
    3.98  lemma zmult_zless_mono1: "[| i<j;  (0::int) < k |] ==> i*k < j*k"
    3.99    by (rule Ring_and_Field.mult_strict_right_mono)
   3.100  
   3.101 @@ -467,6 +434,16 @@
   3.102  apply (auto simp add: int_Suc symmetric zdiff_def)
   3.103  done
   3.104  
   3.105 +(* a case theorem distinguishing non-negative and negative int *)  
   3.106 +
   3.107 +lemma int_cases: 
   3.108 +     "[|!! n. z = int n ==> P;  !! n. z =  - (int (Suc n)) ==> P |] ==> P"
   3.109 +apply (case_tac "neg z")
   3.110 +apply (fast dest!: negD)
   3.111 +apply (drule not_neg_nat [symmetric], auto) 
   3.112 +done
   3.113 +
   3.114 +
   3.115  
   3.116  
   3.117  ML
     4.1 --- a/src/HOL/Integ/nat_simprocs.ML	Mon Nov 24 15:33:07 2003 +0100
     4.2 +++ b/src/HOL/Integ/nat_simprocs.ML	Tue Nov 25 10:37:03 2003 +0100
     4.3 @@ -211,7 +211,7 @@
     4.4  
     4.5  (*Simplify 1*n and n*1 to n*)
     4.6  val add_0s  = map rename_numerals [add_0, add_0_right];
     4.7 -val mult_1s = map rename_numerals [mult_1, mult_1_right];
     4.8 +val mult_1s = map rename_numerals [thm"nat_mult_1", thm"nat_mult_1_right"];
     4.9  
    4.10  (*Final simplification: cancel + and *; replace Numeral0 by 0 and Numeral1 by 1*)
    4.11  
     5.1 --- a/src/HOL/IsaMakefile	Mon Nov 24 15:33:07 2003 +0100
     5.2 +++ b/src/HOL/IsaMakefile	Tue Nov 25 10:37:03 2003 +0100
     5.3 @@ -80,7 +80,7 @@
     5.4    $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML \
     5.5    $(SRC)/TFL/rules.ML $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML \
     5.6    $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML \
     5.7 -  Datatype.thy Datatype_Universe.ML Datatype_Universe.thy Divides_lemmas.ML \
     5.8 +  Datatype.thy Datatype_Universe.ML Datatype_Universe.thy \
     5.9    Divides.thy Extraction.thy Finite_Set.ML Finite_Set.thy \
    5.10    Fun.thy Gfp.ML Gfp.thy \
    5.11    Hilbert_Choice.thy Hilbert_Choice_lemmas.ML HOL.ML \
     6.1 --- a/src/HOL/Nat.thy	Mon Nov 24 15:33:07 2003 +0100
     6.2 +++ b/src/HOL/Nat.thy	Tue Nov 25 10:37:03 2003 +0100
     6.3 @@ -21,7 +21,7 @@
     6.4  axioms
     6.5    -- {* the axiom of infinity in 2 parts *}
     6.6    inj_Suc_Rep:          "inj Suc_Rep"
     6.7 -  Suc_Rep_not_Zero_Rep: "Suc_Rep x ~= Zero_Rep"
     6.8 +  Suc_Rep_not_Zero_Rep: "Suc_Rep x \<noteq> Zero_Rep"
     6.9  
    6.10  
    6.11  subsection {* Type nat *}
    6.12 @@ -64,7 +64,7 @@
    6.13  
    6.14    less_def: "m < n == (m, n) : trancl pred_nat"
    6.15  
    6.16 -  le_def: "m <= (n::nat) == ~ (n < m)"
    6.17 +  le_def: "m \<le> (n::nat) == ~ (n < m)"
    6.18  
    6.19  
    6.20  text {* Induction *}
    6.21 @@ -91,14 +91,14 @@
    6.22  
    6.23  text {* Distinctness of constructors *}
    6.24  
    6.25 -lemma Suc_not_Zero [iff]: "Suc m ~= 0"
    6.26 +lemma Suc_not_Zero [iff]: "Suc m \<noteq> 0"
    6.27    apply (unfold Zero_nat_def Suc_def)
    6.28    apply (rule inj_on_Abs_Nat [THEN inj_on_contraD])
    6.29    apply (rule Suc_Rep_not_Zero_Rep)
    6.30    apply (rule Rep_Nat Nat.Suc_RepI Nat.Zero_RepI)+
    6.31    done
    6.32  
    6.33 -lemma Zero_not_Suc [iff]: "0 ~= Suc m"
    6.34 +lemma Zero_not_Suc [iff]: "0 \<noteq> Suc m"
    6.35    by (rule not_sym, rule Suc_not_Zero not_sym)
    6.36  
    6.37  lemma Suc_neq_Zero: "Suc m = 0 ==> R"
    6.38 @@ -127,7 +127,7 @@
    6.39    apply (erule arg_cong)
    6.40    done
    6.41  
    6.42 -lemma nat_not_singleton: "(ALL x. x = (0::nat)) = False"
    6.43 +lemma nat_not_singleton: "(\<forall>x. x = (0::nat)) = False"
    6.44    by auto
    6.45  
    6.46  text {* @{typ nat} is a datatype *}
    6.47 @@ -137,10 +137,10 @@
    6.48    inject    Suc_Suc_eq
    6.49    induction nat_induct
    6.50  
    6.51 -lemma n_not_Suc_n: "n ~= Suc n"
    6.52 +lemma n_not_Suc_n: "n \<noteq> Suc n"
    6.53    by (induct n) simp_all
    6.54  
    6.55 -lemma Suc_n_not_n: "Suc t ~= t"
    6.56 +lemma Suc_n_not_n: "Suc t \<noteq> t"
    6.57    by (rule not_sym, rule n_not_Suc_n)
    6.58  
    6.59  text {* A special form of induction for reasoning
    6.60 @@ -219,9 +219,9 @@
    6.61  lemma less_irrefl [elim!]: "(n::nat) < n ==> R"
    6.62    by (rule notE, rule less_not_refl)
    6.63  
    6.64 -lemma less_not_refl2: "n < m ==> m ~= (n::nat)" by blast
    6.65 +lemma less_not_refl2: "n < m ==> m \<noteq> (n::nat)" by blast
    6.66  
    6.67 -lemma less_not_refl3: "(s::nat) < t ==> s ~= t"
    6.68 +lemma less_not_refl3: "(s::nat) < t ==> s \<noteq> t"
    6.69    by (rule not_sym, rule less_not_refl2)
    6.70  
    6.71  lemma lessE:
    6.72 @@ -268,7 +268,7 @@
    6.73    apply (blast intro: Suc_mono less_SucI elim: lessE)
    6.74    done
    6.75  
    6.76 -lemma nat_neq_iff: "((m::nat) ~= n) = (m < n | n < m)"
    6.77 +lemma nat_neq_iff: "((m::nat) \<noteq> n) = (m < n | n < m)"
    6.78    using less_linear by blast
    6.79  
    6.80  lemma nat_less_cases: assumes major: "(m::nat) < n ==> P n m"
    6.81 @@ -284,7 +284,7 @@
    6.82  
    6.83  subsubsection {* Inductive (?) properties *}
    6.84  
    6.85 -lemma Suc_lessI: "m < n ==> Suc m ~= n ==> Suc m < n"
    6.86 +lemma Suc_lessI: "m < n ==> Suc m \<noteq> n ==> Suc m < n"
    6.87    apply (simp add: nat_neq_iff)
    6.88    apply (blast elim!: less_irrefl less_SucE elim: less_asym)
    6.89    done
    6.90 @@ -324,7 +324,7 @@
    6.91  
    6.92  text {* Complete induction, aka course-of-values induction *}
    6.93  lemma nat_less_induct:
    6.94 -  assumes prem: "!!n. ALL m::nat. m < n --> P m ==> P n" shows "P n"
    6.95 +  assumes prem: "!!n. \<forall>m::nat. m < n --> P m ==> P n" shows "P n"
    6.96    apply (rule_tac a=n in wf_induct)
    6.97    apply (rule wf_pred_nat [THEN wf_trancl])
    6.98    apply (rule prem)
    6.99 @@ -336,119 +336,119 @@
   6.100  subsection {* Properties of "less than or equal" *}
   6.101  
   6.102  text {* Was @{text le_eq_less_Suc}, but this orientation is more useful *}
   6.103 -lemma less_Suc_eq_le: "(m < Suc n) = (m <= n)"
   6.104 +lemma less_Suc_eq_le: "(m < Suc n) = (m \<le> n)"
   6.105    by (unfold le_def, rule not_less_eq [symmetric])
   6.106  
   6.107 -lemma le_imp_less_Suc: "m <= n ==> m < Suc n"
   6.108 +lemma le_imp_less_Suc: "m \<le> n ==> m < Suc n"
   6.109    by (rule less_Suc_eq_le [THEN iffD2])
   6.110  
   6.111 -lemma le0 [iff]: "(0::nat) <= n"
   6.112 +lemma le0 [iff]: "(0::nat) \<le> n"
   6.113    by (unfold le_def, rule not_less0)
   6.114  
   6.115 -lemma Suc_n_not_le_n: "~ Suc n <= n"
   6.116 +lemma Suc_n_not_le_n: "~ Suc n \<le> n"
   6.117    by (simp add: le_def)
   6.118  
   6.119 -lemma le_0_eq [iff]: "((i::nat) <= 0) = (i = 0)"
   6.120 +lemma le_0_eq [iff]: "((i::nat) \<le> 0) = (i = 0)"
   6.121    by (induct i) (simp_all add: le_def)
   6.122  
   6.123 -lemma le_Suc_eq: "(m <= Suc n) = (m <= n | m = Suc n)"
   6.124 +lemma le_Suc_eq: "(m \<le> Suc n) = (m \<le> n | m = Suc n)"
   6.125    by (simp del: less_Suc_eq_le add: less_Suc_eq_le [symmetric] less_Suc_eq)
   6.126  
   6.127 -lemma le_SucE: "m <= Suc n ==> (m <= n ==> R) ==> (m = Suc n ==> R) ==> R"
   6.128 +lemma le_SucE: "m \<le> Suc n ==> (m \<le> n ==> R) ==> (m = Suc n ==> R) ==> R"
   6.129    by (drule le_Suc_eq [THEN iffD1], rules+)
   6.130  
   6.131 -lemma leI: "~ n < m ==> m <= (n::nat)" by (simp add: le_def)
   6.132 +lemma leI: "~ n < m ==> m \<le> (n::nat)" by (simp add: le_def)
   6.133  
   6.134 -lemma leD: "m <= n ==> ~ n < (m::nat)"
   6.135 +lemma leD: "m \<le> n ==> ~ n < (m::nat)"
   6.136    by (simp add: le_def)
   6.137  
   6.138  lemmas leE = leD [elim_format]
   6.139  
   6.140 -lemma not_less_iff_le: "(~ n < m) = (m <= (n::nat))"
   6.141 +lemma not_less_iff_le: "(~ n < m) = (m \<le> (n::nat))"
   6.142    by (blast intro: leI elim: leE)
   6.143  
   6.144 -lemma not_leE: "~ m <= n ==> n<(m::nat)"
   6.145 +lemma not_leE: "~ m \<le> n ==> n<(m::nat)"
   6.146    by (simp add: le_def)
   6.147  
   6.148 -lemma not_le_iff_less: "(~ n <= m) = (m < (n::nat))"
   6.149 +lemma not_le_iff_less: "(~ n \<le> m) = (m < (n::nat))"
   6.150    by (simp add: le_def)
   6.151  
   6.152 -lemma Suc_leI: "m < n ==> Suc(m) <= n"
   6.153 +lemma Suc_leI: "m < n ==> Suc(m) \<le> n"
   6.154    apply (simp add: le_def less_Suc_eq)
   6.155    apply (blast elim!: less_irrefl less_asym)
   6.156    done -- {* formerly called lessD *}
   6.157  
   6.158 -lemma Suc_leD: "Suc(m) <= n ==> m <= n"
   6.159 +lemma Suc_leD: "Suc(m) \<le> n ==> m \<le> n"
   6.160    by (simp add: le_def less_Suc_eq)
   6.161  
   6.162  text {* Stronger version of @{text Suc_leD} *}
   6.163 -lemma Suc_le_lessD: "Suc m <= n ==> m < n"
   6.164 +lemma Suc_le_lessD: "Suc m \<le> n ==> m < n"
   6.165    apply (simp add: le_def less_Suc_eq)
   6.166    using less_linear
   6.167    apply blast
   6.168    done
   6.169  
   6.170 -lemma Suc_le_eq: "(Suc m <= n) = (m < n)"
   6.171 +lemma Suc_le_eq: "(Suc m \<le> n) = (m < n)"
   6.172    by (blast intro: Suc_leI Suc_le_lessD)
   6.173  
   6.174 -lemma le_SucI: "m <= n ==> m <= Suc n"
   6.175 +lemma le_SucI: "m \<le> n ==> m \<le> Suc n"
   6.176    by (unfold le_def) (blast dest: Suc_lessD)
   6.177  
   6.178 -lemma less_imp_le: "m < n ==> m <= (n::nat)"
   6.179 +lemma less_imp_le: "m < n ==> m \<le> (n::nat)"
   6.180    by (unfold le_def) (blast elim: less_asym)
   6.181  
   6.182 -text {* For instance, @{text "(Suc m < Suc n) = (Suc m <= n) = (m < n)"} *}
   6.183 +text {* For instance, @{text "(Suc m < Suc n) = (Suc m \<le> n) = (m < n)"} *}
   6.184  lemmas le_simps = less_imp_le less_Suc_eq_le Suc_le_eq
   6.185  
   6.186  
   6.187 -text {* Equivalence of @{term "m <= n"} and @{term "m < n | m = n"} *}
   6.188 +text {* Equivalence of @{term "m \<le> n"} and @{term "m < n | m = n"} *}
   6.189  
   6.190 -lemma le_imp_less_or_eq: "m <= n ==> m < n | m = (n::nat)"
   6.191 +lemma le_imp_less_or_eq: "m \<le> n ==> m < n | m = (n::nat)"
   6.192    apply (unfold le_def)
   6.193    using less_linear
   6.194    apply (blast elim: less_irrefl less_asym)
   6.195    done
   6.196  
   6.197 -lemma less_or_eq_imp_le: "m < n | m = n ==> m <= (n::nat)"
   6.198 +lemma less_or_eq_imp_le: "m < n | m = n ==> m \<le> (n::nat)"
   6.199    apply (unfold le_def)
   6.200    using less_linear
   6.201    apply (blast elim!: less_irrefl elim: less_asym)
   6.202    done
   6.203  
   6.204 -lemma le_eq_less_or_eq: "(m <= (n::nat)) = (m < n | m=n)"
   6.205 +lemma le_eq_less_or_eq: "(m \<le> (n::nat)) = (m < n | m=n)"
   6.206    by (rules intro: less_or_eq_imp_le le_imp_less_or_eq)
   6.207  
   6.208  text {* Useful with @{text Blast}. *}
   6.209 -lemma eq_imp_le: "(m::nat) = n ==> m <= n"
   6.210 +lemma eq_imp_le: "(m::nat) = n ==> m \<le> n"
   6.211    by (rule less_or_eq_imp_le, rule disjI2)
   6.212  
   6.213 -lemma le_refl: "n <= (n::nat)"
   6.214 +lemma le_refl: "n \<le> (n::nat)"
   6.215    by (simp add: le_eq_less_or_eq)
   6.216  
   6.217 -lemma le_less_trans: "[| i <= j; j < k |] ==> i < (k::nat)"
   6.218 +lemma le_less_trans: "[| i \<le> j; j < k |] ==> i < (k::nat)"
   6.219    by (blast dest!: le_imp_less_or_eq intro: less_trans)
   6.220  
   6.221 -lemma less_le_trans: "[| i < j; j <= k |] ==> i < (k::nat)"
   6.222 +lemma less_le_trans: "[| i < j; j \<le> k |] ==> i < (k::nat)"
   6.223    by (blast dest!: le_imp_less_or_eq intro: less_trans)
   6.224  
   6.225 -lemma le_trans: "[| i <= j; j <= k |] ==> i <= (k::nat)"
   6.226 +lemma le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::nat)"
   6.227    by (blast dest!: le_imp_less_or_eq intro: less_or_eq_imp_le less_trans)
   6.228  
   6.229 -lemma le_anti_sym: "[| m <= n; n <= m |] ==> m = (n::nat)"
   6.230 +lemma le_anti_sym: "[| m \<le> n; n \<le> m |] ==> m = (n::nat)"
   6.231    by (blast dest!: le_imp_less_or_eq elim!: less_irrefl elim: less_asym)
   6.232  
   6.233 -lemma Suc_le_mono [iff]: "(Suc n <= Suc m) = (n <= m)"
   6.234 +lemma Suc_le_mono [iff]: "(Suc n \<le> Suc m) = (n \<le> m)"
   6.235    by (simp add: le_simps)
   6.236  
   6.237  text {* Axiom @{text order_less_le} of class @{text order}: *}
   6.238 -lemma nat_less_le: "((m::nat) < n) = (m <= n & m ~= n)"
   6.239 +lemma nat_less_le: "((m::nat) < n) = (m \<le> n & m \<noteq> n)"
   6.240    by (simp add: le_def nat_neq_iff) (blast elim!: less_asym)
   6.241  
   6.242 -lemma le_neq_implies_less: "(m::nat) <= n ==> m ~= n ==> m < n"
   6.243 +lemma le_neq_implies_less: "(m::nat) \<le> n ==> m \<noteq> n ==> m < n"
   6.244    by (rule iffD2, rule nat_less_le, rule conjI)
   6.245  
   6.246  text {* Axiom @{text linorder_linear} of class @{text linorder}: *}
   6.247 -lemma nat_le_linear: "(m::nat) <= n | n <= m"
   6.248 +lemma nat_le_linear: "(m::nat) \<le> n | n \<le> m"
   6.249    apply (simp add: le_eq_less_or_eq)
   6.250    using less_linear
   6.251    apply blast
   6.252 @@ -460,10 +460,10 @@
   6.253  
   6.254  text {*
   6.255    Rewrite @{term "n < Suc m"} to @{term "n = m"}
   6.256 -  if @{term "~ n < m"} or @{term "m <= n"} hold.
   6.257 +  if @{term "~ n < m"} or @{term "m \<le> n"} hold.
   6.258    Not suitable as default simprules because they often lead to looping
   6.259  *}
   6.260 -lemma le_less_Suc_eq: "m <= n ==> (n < Suc m) = (n = m)"
   6.261 +lemma le_less_Suc_eq: "m \<le> n ==> (n < Suc m) = (n = m)"
   6.262    by (rule not_less_less_Suc_eq, rule leD)
   6.263  
   6.264  lemmas not_less_simps = not_less_less_Suc_eq le_less_Suc_eq
   6.265 @@ -526,20 +526,20 @@
   6.266  lemma def_nat_rec_Suc: "(!!n. f n == nat_rec c h n) ==> f (Suc n) = h n (f n)"
   6.267    by simp
   6.268  
   6.269 -lemma not0_implies_Suc: "n ~= 0 ==> EX m. n = Suc m"
   6.270 +lemma not0_implies_Suc: "n \<noteq> 0 ==> \<exists>m. n = Suc m"
   6.271    by (case_tac n) simp_all
   6.272  
   6.273 -lemma gr_implies_not0: "!!n::nat. m<n ==> n ~= 0"
   6.274 +lemma gr_implies_not0: "!!n::nat. m<n ==> n \<noteq> 0"
   6.275    by (case_tac n) simp_all
   6.276  
   6.277 -lemma neq0_conv [iff]: "!!n::nat. (n ~= 0) = (0 < n)"
   6.278 +lemma neq0_conv [iff]: "!!n::nat. (n \<noteq> 0) = (0 < n)"
   6.279    by (case_tac n) simp_all
   6.280  
   6.281  text {* This theorem is useful with @{text blast} *}
   6.282  lemma gr0I: "((n::nat) = 0 ==> False) ==> 0 < n"
   6.283    by (rule iffD1, rule neq0_conv, rules)
   6.284  
   6.285 -lemma gr0_conv_Suc: "(0 < n) = (EX m. n = Suc m)"
   6.286 +lemma gr0_conv_Suc: "(0 < n) = (\<exists>m. n = Suc m)"
   6.287    by (fast intro: not0_implies_Suc)
   6.288  
   6.289  lemma not_gr0 [iff]: "!!n::nat. (~ (0 < n)) = (n = 0)"
   6.290 @@ -547,11 +547,11 @@
   6.291    apply (rule ccontr, simp_all)
   6.292    done
   6.293  
   6.294 -lemma Suc_le_D: "(Suc n <= m') ==> (? m. m' = Suc m)"
   6.295 +lemma Suc_le_D: "(Suc n \<le> m') ==> (? m. m' = Suc m)"
   6.296    by (induct m') simp_all
   6.297  
   6.298  text {* Useful in certain inductive arguments *}
   6.299 -lemma less_Suc_eq_0_disj: "(m < Suc n) = (m = 0 | (EX j. m = Suc j & j < n))"
   6.300 +lemma less_Suc_eq_0_disj: "(m < Suc n) = (m = 0 | (\<exists>j. m = Suc j & j < n))"
   6.301    by (case_tac m) simp_all
   6.302  
   6.303  lemma nat_induct2: "P 0 ==> P (Suc 0) ==> (!!k. P k ==> P (Suc (Suc k))) ==> P n"
   6.304 @@ -567,21 +567,21 @@
   6.305  lemmas Least_le = wellorder_Least_le
   6.306  lemmas not_less_Least = wellorder_not_less_Least
   6.307  
   6.308 -lemma Least_Suc: "[| P n; ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
   6.309 +lemma Least_Suc:
   6.310 +     "[| P n; ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
   6.311    apply (case_tac "n", auto)
   6.312    apply (frule LeastI)
   6.313    apply (drule_tac P = "%x. P (Suc x) " in LeastI)
   6.314 -  apply (subgoal_tac " (LEAST x. P x) <= Suc (LEAST x. P (Suc x))")
   6.315 +  apply (subgoal_tac " (LEAST x. P x) \<le> Suc (LEAST x. P (Suc x))")
   6.316    apply (erule_tac [2] Least_le)
   6.317    apply (case_tac "LEAST x. P x", auto)
   6.318    apply (drule_tac P = "%x. P (Suc x) " in Least_le)
   6.319    apply (blast intro: order_antisym)
   6.320    done
   6.321  
   6.322 -lemma Least_Suc2: "[|P n; Q m; ~P 0; !k. P (Suc k) = Q k|] ==> Least P = Suc (Least Q)"
   6.323 -  apply (erule (1) Least_Suc [THEN ssubst])
   6.324 -  apply simp
   6.325 -  done
   6.326 +lemma Least_Suc2:
   6.327 +     "[|P n; Q m; ~P 0; !k. P (Suc k) = Q k|] ==> Least P = Suc (Least Q)"
   6.328 +  by (erule (1) Least_Suc [THEN ssubst], simp)
   6.329  
   6.330  
   6.331  
   6.332 @@ -640,29 +640,26 @@
   6.333  
   6.334  
   6.335  text {* Associative law for addition *}
   6.336 -lemma add_assoc: "(m + n) + k = m + ((n + k)::nat)"
   6.337 +lemma nat_add_assoc: "(m + n) + k = m + ((n + k)::nat)"
   6.338    by (induct m) simp_all
   6.339  
   6.340  text {* Commutative law for addition *}
   6.341 -lemma add_commute: "m + n = n + (m::nat)"
   6.342 +lemma nat_add_commute: "m + n = n + (m::nat)"
   6.343    by (induct m) simp_all
   6.344  
   6.345 -lemma add_left_commute: "x + (y + z) = y + ((x + z)::nat)"
   6.346 +lemma nat_add_left_commute: "x + (y + z) = y + ((x + z)::nat)"
   6.347    apply (rule mk_left_commute [of "op +"])
   6.348 -  apply (rule add_assoc)
   6.349 -  apply (rule add_commute)
   6.350 +  apply (rule nat_add_assoc)
   6.351 +  apply (rule nat_add_commute)
   6.352    done
   6.353  
   6.354 -text {* Addition is an AC-operator *}
   6.355 -lemmas add_ac = add_assoc add_commute add_left_commute
   6.356 -
   6.357  lemma add_left_cancel [simp]: "(k + m = k + n) = (m = (n::nat))"
   6.358    by (induct k) simp_all
   6.359  
   6.360  lemma add_right_cancel [simp]: "(m + k = n + k) = (m=(n::nat))"
   6.361    by (induct k) simp_all
   6.362  
   6.363 -lemma add_left_cancel_le [simp]: "(k + m <= k + n) = (m<=(n::nat))"
   6.364 +lemma add_left_cancel_le [simp]: "(k + m \<le> k + n) = (m\<le>(n::nat))"
   6.365    by (induct k) simp_all
   6.366  
   6.367  lemma add_left_cancel_less [simp]: "(k + m < k + n) = (m<(n::nat))"
   6.368 @@ -684,24 +681,114 @@
   6.369  
   6.370  lemma add_eq_self_zero: "!!m::nat. m + n = m ==> n = 0"
   6.371    apply (drule add_0_right [THEN ssubst])
   6.372 -  apply (simp add: add_assoc del: add_0_right)
   6.373 +  apply (simp add: nat_add_assoc del: add_0_right)
   6.374    done
   6.375  
   6.376 -subsection {* Additional theorems about "less than" *}
   6.377 +subsection {* Monotonicity of Addition *}
   6.378 +
   6.379 +text {* strict, in 1st argument *}
   6.380 +lemma add_less_mono1: "i < j ==> i + k < j + (k::nat)"
   6.381 +  by (induct k) simp_all
   6.382  
   6.383 -text {* Deleted @{text less_natE}; instead use @{text "less_imp_Suc_add RS exE"} *}
   6.384 -lemma less_imp_Suc_add: "m < n ==> (EX k. n = Suc (m + k))"
   6.385 +text {* strict, in both arguments *}
   6.386 +lemma add_less_mono: "[|i < j; k < l|] ==> i + k < j + (l::nat)"
   6.387 +  apply (rule add_less_mono1 [THEN less_trans], assumption+)
   6.388 +  apply (induct_tac j, simp_all)
   6.389 +  done
   6.390 +
   6.391 +text {* Deleted @{text less_natE}; use @{text "less_imp_Suc_add RS exE"} *}
   6.392 +lemma less_imp_Suc_add: "m < n ==> (\<exists>k. n = Suc (m + k))"
   6.393    apply (induct n)
   6.394    apply (simp_all add: order_le_less)
   6.395    apply (blast elim!: less_SucE intro!: add_0_right [symmetric] add_Suc_right [symmetric])
   6.396    done
   6.397  
   6.398 -lemma le_add2: "n <= ((m + n)::nat)"
   6.399 +
   6.400 +subsection {* Multiplication *}
   6.401 +
   6.402 +text {* right annihilation in product *}
   6.403 +lemma mult_0_right [simp]: "(m::nat) * 0 = 0"
   6.404 +  by (induct m) simp_all
   6.405 +
   6.406 +text {* right successor law for multiplication *}
   6.407 +lemma mult_Suc_right [simp]: "m * Suc n = m + (m * n)"
   6.408 +  by (induct m) (simp_all add: nat_add_left_commute)
   6.409 +
   6.410 +text {* Commutative law for multiplication *}
   6.411 +lemma nat_mult_commute: "m * n = n * (m::nat)"
   6.412 +  by (induct m) simp_all
   6.413 +
   6.414 +text {* addition distributes over multiplication *}
   6.415 +lemma add_mult_distrib: "(m + n) * k = (m * k) + ((n * k)::nat)"
   6.416 +  by (induct m) (simp_all add: nat_add_assoc nat_add_left_commute)
   6.417 +
   6.418 +lemma add_mult_distrib2: "k * (m + n) = (k * m) + ((k * n)::nat)"
   6.419 +  by (induct m) (simp_all add: nat_add_assoc)
   6.420 +
   6.421 +text {* Associative law for multiplication *}
   6.422 +lemma nat_mult_assoc: "(m * n) * k = m * ((n * k)::nat)"
   6.423 +  by (induct m) (simp_all add: add_mult_distrib)
   6.424 +
   6.425 +lemma mult_is_0 [simp]: "((m::nat) * n = 0) = (m=0 | n=0)"
   6.426 +  apply (induct_tac m)
   6.427 +  apply (induct_tac [2] n, simp_all)
   6.428 +  done
   6.429 +
   6.430 +text {* strict, in 1st argument; proof is by induction on @{text "k > 0"} *}
   6.431 +lemma mult_less_mono2: "(i::nat) < j ==> 0 < k ==> k * i < k * j"
   6.432 +  apply (erule_tac m1 = 0 in less_imp_Suc_add [THEN exE], simp)
   6.433 +  apply (induct_tac x) 
   6.434 +  apply (simp_all add: add_less_mono)
   6.435 +  done
   6.436 +
   6.437 +text{*The Naturals Form an Ordered Semiring*}
   6.438 +instance nat :: ordered_semiring
   6.439 +proof
   6.440 +  fix i j k :: nat
   6.441 +  show "(i + j) + k = i + (j + k)" by (rule nat_add_assoc)
   6.442 +  show "i + j = j + i" by (rule nat_add_commute)
   6.443 +  show "0 + i = i" by simp
   6.444 +  show "(i * j) * k = i * (j * k)" by (rule nat_mult_assoc)
   6.445 +  show "i * j = j * i" by (rule nat_mult_commute)
   6.446 +  show "1 * i = i" by simp
   6.447 +  show "(i + j) * k = i * k + j * k" by (simp add: add_mult_distrib)
   6.448 +  show "0 \<noteq> (1::nat)" by simp
   6.449 +  show "i \<le> j ==> k + i \<le> k + j" by simp
   6.450 +  show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: mult_less_mono2)
   6.451 +qed
   6.452 +
   6.453 +lemma nat_mult_1: "(1::nat) * n = n"
   6.454 +  by simp
   6.455 +
   6.456 +lemma nat_mult_1_right: "n * (1::nat) = n"
   6.457 +  by simp
   6.458 +
   6.459 +
   6.460 +subsection {* Additional theorems about "less than" *}
   6.461 +
   6.462 +text {* A [clumsy] way of lifting @{text "<"}
   6.463 +  monotonicity to @{text "\<le>"} monotonicity *}
   6.464 +lemma less_mono_imp_le_mono:
   6.465 +  assumes lt_mono: "!!i j::nat. i < j ==> f i < f j"
   6.466 +  and le: "i \<le> j" shows "f i \<le> ((f j)::nat)" using le
   6.467 +  apply (simp add: order_le_less)
   6.468 +  apply (blast intro!: lt_mono)
   6.469 +  done
   6.470 +
   6.471 +text {* non-strict, in 1st argument *}
   6.472 +lemma add_le_mono1: "i \<le> j ==> i + k \<le> j + (k::nat)"
   6.473 +  by (rule add_right_mono)
   6.474 +
   6.475 +text {* non-strict, in both arguments *}
   6.476 +lemma add_le_mono: "[| i \<le> j;  k \<le> l |] ==> i + k \<le> j + (l::nat)"
   6.477 +  by (rule add_mono)
   6.478 +
   6.479 +lemma le_add2: "n \<le> ((m + n)::nat)"
   6.480    apply (induct m, simp_all)
   6.481    apply (erule le_SucI)
   6.482    done
   6.483  
   6.484 -lemma le_add1: "n <= ((n + m)::nat)"
   6.485 +lemma le_add1: "n \<le> ((n + m)::nat)"
   6.486    apply (simp add: add_ac)
   6.487    apply (rule le_add2)
   6.488    done
   6.489 @@ -712,14 +799,14 @@
   6.490  lemma less_add_Suc2: "i < Suc (m + i)"
   6.491    by (rule le_less_trans, rule le_add2, rule lessI)
   6.492  
   6.493 -lemma less_iff_Suc_add: "(m < n) = (EX k. n = Suc (m + k))"
   6.494 +lemma less_iff_Suc_add: "(m < n) = (\<exists>k. n = Suc (m + k))"
   6.495    by (rules intro!: less_add_Suc1 less_imp_Suc_add)
   6.496  
   6.497  
   6.498 -lemma trans_le_add1: "(i::nat) <= j ==> i <= j + m"
   6.499 +lemma trans_le_add1: "(i::nat) \<le> j ==> i \<le> j + m"
   6.500    by (rule le_trans, assumption, rule le_add1)
   6.501  
   6.502 -lemma trans_le_add2: "(i::nat) <= j ==> i <= m + j"
   6.503 +lemma trans_le_add2: "(i::nat) \<le> j ==> i \<le> m + j"
   6.504    by (rule le_trans, assumption, rule le_add2)
   6.505  
   6.506  lemma trans_less_add1: "(i::nat) < j ==> i < j + m"
   6.507 @@ -741,15 +828,15 @@
   6.508  lemma not_add_less2 [iff]: "~ (j + i < (i::nat))"
   6.509    by (simp add: add_commute not_add_less1)
   6.510  
   6.511 -lemma add_leD1: "m + k <= n ==> m <= (n::nat)"
   6.512 +lemma add_leD1: "m + k \<le> n ==> m \<le> (n::nat)"
   6.513    by (induct k) (simp_all add: le_simps)
   6.514  
   6.515 -lemma add_leD2: "m + k <= n ==> k <= (n::nat)"
   6.516 +lemma add_leD2: "m + k \<le> n ==> k \<le> (n::nat)"
   6.517    apply (simp add: add_commute)
   6.518    apply (erule add_leD1)
   6.519    done
   6.520  
   6.521 -lemma add_leE: "(m::nat) + k <= n ==> (m <= n ==> k <= n ==> R) ==> R"
   6.522 +lemma add_leE: "(m::nat) + k \<le> n ==> (m \<le> n ==> k \<le> n ==> R) ==> R"
   6.523    by (blast dest: add_leD1 add_leD2)
   6.524  
   6.525  text {* needs @{text "!!k"} for @{text add_ac} to work *}
   6.526 @@ -758,106 +845,6 @@
   6.527      simp add: less_iff_Suc_add add_Suc_right [symmetric] add_ac)
   6.528  
   6.529  
   6.530 -subsection {* Monotonicity of Addition *}
   6.531 -
   6.532 -text {* strict, in 1st argument *}
   6.533 -lemma add_less_mono1: "i < j ==> i + k < j + (k::nat)"
   6.534 -  by (induct k) simp_all
   6.535 -
   6.536 -text {* strict, in both arguments *}
   6.537 -lemma add_less_mono: "[|i < j; k < l|] ==> i + k < j + (l::nat)"
   6.538 -  apply (rule add_less_mono1 [THEN less_trans], assumption+)
   6.539 -  apply (induct_tac j, simp_all)
   6.540 -  done
   6.541 -
   6.542 -text {* A [clumsy] way of lifting @{text "<"}
   6.543 -  monotonicity to @{text "<="} monotonicity *}
   6.544 -lemma less_mono_imp_le_mono:
   6.545 -  assumes lt_mono: "!!i j::nat. i < j ==> f i < f j"
   6.546 -  and le: "i <= j" shows "f i <= ((f j)::nat)" using le
   6.547 -  apply (simp add: order_le_less)
   6.548 -  apply (blast intro!: lt_mono)
   6.549 -  done
   6.550 -
   6.551 -text {* non-strict, in 1st argument *}
   6.552 -lemma add_le_mono1: "i <= j ==> i + k <= j + (k::nat)"
   6.553 -  apply (rule_tac f = "%j. j + k" in less_mono_imp_le_mono)
   6.554 -  apply (erule add_less_mono1, assumption)
   6.555 -  done
   6.556 -
   6.557 -text {* non-strict, in both arguments *}
   6.558 -lemma add_le_mono: "[| i <= j;  k <= l |] ==> i + k <= j + (l::nat)"
   6.559 -  apply (erule add_le_mono1 [THEN le_trans])
   6.560 -  apply (simp add: add_commute)
   6.561 -  done
   6.562 -
   6.563 -
   6.564 -subsection {* Multiplication *}
   6.565 -
   6.566 -text {* right annihilation in product *}
   6.567 -lemma mult_0_right [simp]: "(m::nat) * 0 = 0"
   6.568 -  by (induct m) simp_all
   6.569 -
   6.570 -text {* right successor law for multiplication *}
   6.571 -lemma mult_Suc_right [simp]: "m * Suc n = m + (m * n)"
   6.572 -  by (induct m) (simp_all add: add_ac)
   6.573 -
   6.574 -lemma mult_1: "(1::nat) * n = n" by simp
   6.575 -
   6.576 -lemma mult_1_right: "n * (1::nat) = n" by simp
   6.577 -
   6.578 -text {* Commutative law for multiplication *}
   6.579 -lemma mult_commute: "m * n = n * (m::nat)"
   6.580 -  by (induct m) simp_all
   6.581 -
   6.582 -text {* addition distributes over multiplication *}
   6.583 -lemma add_mult_distrib: "(m + n) * k = (m * k) + ((n * k)::nat)"
   6.584 -  by (induct m) (simp_all add: add_ac)
   6.585 -
   6.586 -lemma add_mult_distrib2: "k * (m + n) = (k * m) + ((k * n)::nat)"
   6.587 -  by (induct m) (simp_all add: add_ac)
   6.588 -
   6.589 -text {* Associative law for multiplication *}
   6.590 -lemma mult_assoc: "(m * n) * k = m * ((n * k)::nat)"
   6.591 -  by (induct m) (simp_all add: add_mult_distrib)
   6.592 -
   6.593 -lemma mult_left_commute: "x * (y * z) = y * ((x * z)::nat)"
   6.594 -  apply (rule mk_left_commute [of "op *"])
   6.595 -  apply (rule mult_assoc)
   6.596 -  apply (rule mult_commute)
   6.597 -  done
   6.598 -
   6.599 -lemmas mult_ac = mult_assoc mult_commute mult_left_commute
   6.600 -
   6.601 -lemma mult_is_0 [simp]: "((m::nat) * n = 0) = (m=0 | n=0)"
   6.602 -  apply (induct_tac m)
   6.603 -  apply (induct_tac [2] n, simp_all)
   6.604 -  done
   6.605 -
   6.606 -text {* strict, in 1st argument; proof is by induction on @{text "k > 0"} *}
   6.607 -lemma mult_less_mono2: "(i::nat) < j ==> 0 < k ==> k * i < k * j"
   6.608 -  apply (erule_tac m1 = 0 in less_imp_Suc_add [THEN exE], simp)
   6.609 -  apply (induct_tac x)
   6.610 -  apply (simp_all add: add_less_mono)
   6.611 -  done
   6.612 -
   6.613 -text{*The Naturals Form an Ordered Semiring*}
   6.614 -instance nat :: ordered_semiring
   6.615 -proof
   6.616 -  fix i j k :: nat
   6.617 -  show "(i + j) + k = i + (j + k)" by (rule add_assoc)
   6.618 -  show "i + j = j + i" by (rule add_commute)
   6.619 -  show "0 + i = i" by simp
   6.620 -  show "(i * j) * k = i * (j * k)" by (rule mult_assoc)
   6.621 -  show "i * j = j * i" by (rule mult_commute)
   6.622 -  show "1 * i = i" by simp
   6.623 -  show "(i + j) * k = i * k + j * k" by (simp add: add_mult_distrib)
   6.624 -  show "0 \<noteq> (1::nat)" by simp
   6.625 -  show "i \<le> j ==> k + i \<le> k + j" by simp
   6.626 -  show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: mult_less_mono2)
   6.627 -qed
   6.628 -
   6.629 -
   6.630  
   6.631  subsection {* Difference *}
   6.632  
   6.633 @@ -865,20 +852,20 @@
   6.634    by (induct m) simp_all
   6.635  
   6.636  text {* Addition is the inverse of subtraction:
   6.637 -  if @{term "n <= m"} then @{term "n + (m - n) = m"}. *}
   6.638 +  if @{term "n \<le> m"} then @{term "n + (m - n) = m"}. *}
   6.639  lemma add_diff_inverse: "~  m < n ==> n + (m - n) = (m::nat)"
   6.640    by (induct m n rule: diff_induct) simp_all
   6.641  
   6.642 -lemma le_add_diff_inverse [simp]: "n <= m ==> n + (m - n) = (m::nat)"
   6.643 +lemma le_add_diff_inverse [simp]: "n \<le> m ==> n + (m - n) = (m::nat)"
   6.644    by (simp add: add_diff_inverse not_less_iff_le)
   6.645  
   6.646 -lemma le_add_diff_inverse2 [simp]: "n <= m ==> (m - n) + n = (m::nat)"
   6.647 +lemma le_add_diff_inverse2 [simp]: "n \<le> m ==> (m - n) + n = (m::nat)"
   6.648    by (simp add: le_add_diff_inverse add_commute)
   6.649  
   6.650  
   6.651  subsection {* More results about difference *}
   6.652  
   6.653 -lemma Suc_diff_le: "n <= m ==> Suc m - n = Suc (m - n)"
   6.654 +lemma Suc_diff_le: "n \<le> m ==> Suc m - n = Suc (m - n)"
   6.655    by (induct m n rule: diff_induct) simp_all
   6.656  
   6.657  lemma diff_less_Suc: "m - n < Suc m"
   6.658 @@ -887,7 +874,7 @@
   6.659    apply (simp_all add: less_Suc_eq)
   6.660    done
   6.661  
   6.662 -lemma diff_le_self [simp]: "m - n <= (m::nat)"
   6.663 +lemma diff_le_self [simp]: "m - n \<le> (m::nat)"
   6.664    by (induct m n rule: diff_induct) (simp_all add: le_SucI)
   6.665  
   6.666  lemma less_imp_diff_less: "(j::nat) < k ==> j - n < k"
   6.667 @@ -908,10 +895,10 @@
   6.668  lemma diff_commute: "(i::nat) - j - k = i - k - j"
   6.669    by (simp add: diff_diff_left add_commute)
   6.670  
   6.671 -lemma diff_add_assoc: "k <= (j::nat) ==> (i + j) - k = i + (j - k)"
   6.672 +lemma diff_add_assoc: "k \<le> (j::nat) ==> (i + j) - k = i + (j - k)"
   6.673    by (induct j k rule: diff_induct) simp_all
   6.674  
   6.675 -lemma diff_add_assoc2: "k <= (j::nat) ==> (j + i) - k = (j - k) + i"
   6.676 +lemma diff_add_assoc2: "k \<le> (j::nat) ==> (j + i) - k = (j - k) + i"
   6.677    by (simp add: add_commute diff_add_assoc)
   6.678  
   6.679  lemma diff_add_inverse: "(n + m) - n = (m::nat)"
   6.680 @@ -920,21 +907,21 @@
   6.681  lemma diff_add_inverse2: "(m + n) - n = (m::nat)"
   6.682    by (simp add: diff_add_assoc)
   6.683  
   6.684 -lemma le_imp_diff_is_add: "i <= (j::nat) ==> (j - i = k) = (j = k + i)"
   6.685 +lemma le_imp_diff_is_add: "i \<le> (j::nat) ==> (j - i = k) = (j = k + i)"
   6.686    apply safe
   6.687    apply (simp_all add: diff_add_inverse2)
   6.688    done
   6.689  
   6.690 -lemma diff_is_0_eq [simp]: "((m::nat) - n = 0) = (m <= n)"
   6.691 +lemma diff_is_0_eq [simp]: "((m::nat) - n = 0) = (m \<le> n)"
   6.692    by (induct m n rule: diff_induct) simp_all
   6.693  
   6.694 -lemma diff_is_0_eq' [simp]: "m <= n ==> (m::nat) - n = 0"
   6.695 +lemma diff_is_0_eq' [simp]: "m \<le> n ==> (m::nat) - n = 0"
   6.696    by (rule iffD2, rule diff_is_0_eq)
   6.697  
   6.698  lemma zero_less_diff [simp]: "(0 < n - (m::nat)) = (m < n)"
   6.699    by (induct m n rule: diff_induct) simp_all
   6.700  
   6.701 -lemma less_imp_add_positive: "i < j  ==> EX k::nat. 0 < k & i + k = j"
   6.702 +lemma less_imp_add_positive: "i < j  ==> \<exists>k::nat. 0 < k & i + k = j"
   6.703    apply (rule_tac x = "j - i" in exI)
   6.704    apply (simp (no_asm_simp) add: add_diff_inverse less_not_sym)
   6.705    done
   6.706 @@ -975,16 +962,16 @@
   6.707  
   6.708  subsection {* Monotonicity of Multiplication *}
   6.709  
   6.710 -lemma mult_le_mono1: "i <= (j::nat) ==> i * k <= j * k"
   6.711 +lemma mult_le_mono1: "i \<le> (j::nat) ==> i * k \<le> j * k"
   6.712    by (induct k) (simp_all add: add_le_mono)
   6.713  
   6.714 -lemma mult_le_mono2: "i <= (j::nat) ==> k * i <= k * j"
   6.715 +lemma mult_le_mono2: "i \<le> (j::nat) ==> k * i \<le> k * j"
   6.716    apply (drule mult_le_mono1)
   6.717    apply (simp add: mult_commute)
   6.718    done
   6.719  
   6.720 -text {* @{text "<="} monotonicity, BOTH arguments *}
   6.721 -lemma mult_le_mono: "i <= (j::nat) ==> k <= l ==> i * k <= j * l"
   6.722 +text {* @{text "\<le>"} monotonicity, BOTH arguments *}
   6.723 +lemma mult_le_mono: "i \<le> (j::nat) ==> k \<le> l ==> i * k \<le> j * l"
   6.724    apply (erule mult_le_mono1 [THEN le_trans])
   6.725    apply (erule mult_le_mono2)
   6.726    done
   6.727 @@ -999,7 +986,7 @@
   6.728    apply (case_tac [2] n, simp_all)
   6.729    done
   6.730  
   6.731 -lemma one_le_mult_iff [simp]: "(Suc 0 <= m * n) = (1 <= m & 1 <= n)"
   6.732 +lemma one_le_mult_iff [simp]: "(Suc 0 \<le> m * n) = (1 \<le> m & 1 \<le> n)"
   6.733    apply (induct m)
   6.734    apply (case_tac [2] n, simp_all)
   6.735    done
   6.736 @@ -1026,10 +1013,10 @@
   6.737  
   6.738  declare mult_less_cancel2 [simp]
   6.739  
   6.740 -lemma mult_le_cancel1 [simp]: "(k * (m::nat) <= k * n) = (0 < k --> m <= n)"
   6.741 +lemma mult_le_cancel1 [simp]: "(k * (m::nat) \<le> k * n) = (0 < k --> m \<le> n)"
   6.742  by (simp add: linorder_not_less [symmetric], auto)
   6.743  
   6.744 -lemma mult_le_cancel2 [simp]: "((m::nat) * k <= n * k) = (0 < k --> m <= n)"
   6.745 +lemma mult_le_cancel2 [simp]: "((m::nat) * k \<le> n * k) = (0 < k --> m \<le> n)"
   6.746  by (simp add: linorder_not_less [symmetric], auto)
   6.747  
   6.748  lemma mult_cancel2: "(m * k = n * k) = (m = n | (k = (0::nat)))"
   6.749 @@ -1045,7 +1032,7 @@
   6.750  lemma Suc_mult_less_cancel1: "(Suc k * m < Suc k * n) = (m < n)"
   6.751    by (subst mult_less_cancel1) simp
   6.752  
   6.753 -lemma Suc_mult_le_cancel1: "(Suc k * m <= Suc k * n) = (m <= n)"
   6.754 +lemma Suc_mult_le_cancel1: "(Suc k * m \<le> Suc k * n) = (m \<le> n)"
   6.755    by (subst mult_le_cancel1) simp
   6.756  
   6.757  lemma Suc_mult_cancel1: "(Suc k * m = Suc k * n) = (m = n)"
     7.1 --- a/src/HOL/Ring_and_Field.thy	Mon Nov 24 15:33:07 2003 +0100
     7.2 +++ b/src/HOL/Ring_and_Field.thy	Tue Nov 25 10:37:03 2003 +0100
     7.3 @@ -22,7 +22,7 @@
     7.4  
     7.5    mult_assoc: "(a * b) * c = a * (b * c)"
     7.6    mult_commute: "a * b = b * a"
     7.7 -  left_one [simp]: "1 * a = a"
     7.8 +  mult_1 [simp]: "1 * a = a"
     7.9  
    7.10    left_distrib: "(a + b) * c = a * c + b * c"
    7.11    zero_neq_one [simp]: "0 \<noteq> 1"
    7.12 @@ -133,10 +133,10 @@
    7.13  
    7.14  subsection {* Derived rules for multiplication *}
    7.15  
    7.16 -lemma right_one [simp]: "a = a * (1::'a::semiring)"
    7.17 +lemma mult_1_right [simp]: "a * (1::'a::semiring) = a"
    7.18  proof -
    7.19 -  have "a = 1 * a" by simp
    7.20 -  also have "... = a * 1" by (simp add: mult_commute)
    7.21 +  have "a * 1 = 1 * a" by (simp add: mult_commute)
    7.22 +  also have "... = a" by simp
    7.23    finally show ?thesis .
    7.24  qed
    7.25  
    7.26 @@ -217,6 +217,12 @@
    7.27  lemma add_right_mono: "a \<le> (b::'a::ordered_semiring) ==> a + c \<le> b + c"
    7.28  by (simp add: add_commute [of _ c] add_left_mono)
    7.29  
    7.30 +text {* non-strict, in both arguments *}
    7.31 +lemma add_mono: "[|a \<le> b;  c \<le> d|] ==> a + c \<le> b + (d::'a::ordered_semiring)"
    7.32 +  apply (erule add_right_mono [THEN order_trans])
    7.33 +  apply (simp add: add_commute add_left_mono)
    7.34 +  done
    7.35 +
    7.36  lemma le_imp_neg_le:
    7.37     assumes "a \<le> (b::'a::ordered_ring)" shows "-b \<le> -a"
    7.38    proof -
    7.39 @@ -261,12 +267,14 @@
    7.40  by (simp add: mult_commute [of _ c] mult_strict_left_mono)
    7.41  
    7.42  lemma mult_left_mono:
    7.43 -     "[|a \<le> b; 0 < c|] ==> c * a \<le> c * (b::'a::ordered_semiring)"
    7.44 -by (force simp add: mult_strict_left_mono order_le_less) 
    7.45 +     "[|a \<le> b; 0 \<le> c|] ==> c * a \<le> c * (b::'a::ordered_ring)"
    7.46 +  apply (case_tac "c=0", simp)
    7.47 +  apply (force simp add: mult_strict_left_mono order_le_less) 
    7.48 +  done
    7.49  
    7.50  lemma mult_right_mono:
    7.51 -     "[|a \<le> b; 0 < c|] ==> a*c \<le> b * (c::'a::ordered_semiring)"
    7.52 -by (force simp add: mult_strict_right_mono order_le_less) 
    7.53 +     "[|a \<le> b; 0 \<le> c|] ==> a*c \<le> b * (c::'a::ordered_ring)"
    7.54 +  by (simp add: mult_left_mono mult_commute [of _ c]) 
    7.55  
    7.56  lemma mult_strict_left_mono_neg:
    7.57       "[|b < a; c < 0|] ==> c * a < c * (b::'a::ordered_ring)"
    7.58 @@ -281,12 +289,14 @@
    7.59  done
    7.60  
    7.61  lemma mult_left_mono_neg:
    7.62 -     "[|b \<le> a; c < 0|] ==> c * a \<le> c * (b::'a::ordered_ring)"
    7.63 -by (force simp add: mult_strict_left_mono_neg order_le_less) 
    7.64 +     "[|b \<le> a; c \<le> 0|] ==> c * a \<le> c * (b::'a::ordered_ring)"
    7.65 +apply (drule mult_left_mono [of _ _ "-c"]) 
    7.66 +apply (simp_all add: minus_mult_left [symmetric]) 
    7.67 +done
    7.68  
    7.69  lemma mult_right_mono_neg:
    7.70 -     "[|b \<le> a; c < 0|] ==> a * c \<le> b * (c::'a::ordered_ring)"
    7.71 -by (force simp add: mult_strict_right_mono_neg order_le_less) 
    7.72 +     "[|b \<le> a; c \<le> 0|] ==> a * c \<le> b * (c::'a::ordered_ring)"
    7.73 +  by (simp add: mult_left_mono_neg mult_commute [of _ c]) 
    7.74  
    7.75  text{*Strict monotonicity in both arguments*}
    7.76  lemma mult_strict_mono:
    7.77 @@ -295,6 +305,14 @@
    7.78  apply (erule mult_strict_left_mono, assumption)
    7.79  done
    7.80  
    7.81 +lemma mult_mono:
    7.82 +     "[|a \<le> b; c \<le> d; 0 \<le> b; 0 \<le> c|] 
    7.83 +      ==> a * c  \<le>  b * (d::'a::ordered_ring)"
    7.84 +apply (erule mult_right_mono [THEN order_trans], assumption)
    7.85 +apply (erule mult_left_mono, assumption)
    7.86 +done
    7.87 +
    7.88 +
    7.89  subsection{*Cancellation Laws for Relationships With a Common Factor*}
    7.90  
    7.91  text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},