author paulson Tue Nov 25 10:37:03 2003 +0100 (2003-11-25) changeset 14267 b963e9cee2a0 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 file | annotate | diff | revisions src/HOL/Divides_lemmas.ML file | annotate | diff | revisions src/HOL/Integ/Int.thy file | annotate | diff | revisions src/HOL/Integ/nat_simprocs.ML file | annotate | diff | revisions src/HOL/IsaMakefile file | annotate | diff | revisions src/HOL/Nat.thy file | annotate | diff | revisions src/HOL/Ring_and_Field.thy file | annotate | diff | revisions
```     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.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.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.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.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.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.91 +
1.92 +lemma mod_mult_self1 [simp]: "(m + k*n) mod n = m mod (n::nat)"
1.93 +apply (induct_tac "k")
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.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.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.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.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.158 +done
1.159 +
1.160 +lemma div_mod_equality2: "(n*(m div n) + m mod n) + k = (m::nat) + k"
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.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.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.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.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.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.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.299 +
1.300 +(*NOT suitable for rewriting: the RHS has an instance of the LHS*)
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.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.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.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.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.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.391 +
1.392 +lemma div_mult_self1 [simp]: "!!n::nat. 0<n ==> (m + k*n) div n = k + m div n"
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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.102 -
2.103 -Goal "(n+m) mod n = m mod (n::nat)";
2.106 -
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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.462 -
2.463 -Goal "0<n ==> (n+m) div n = Suc (m div n)";
2.466 -
2.467 -Goal "!!n::nat. 0<n ==> (m + k*n) div n = k + m div n";
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.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.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.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.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.585 -
2.586 -Goalw [dvd_def] "Suc 0 dvd k";
2.587 -by (Simp_tac 1);
2.588 -qed "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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.352    done
6.353
6.354 -text {* Addition is an AC-operator *}
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.374    done
6.375
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.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.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.417 +
6.418 +lemma add_mult_distrib2: "k * (m + n) = (k * m) + ((k * n)::nat)"
6.420 +
6.421 +text {* Associative law for multiplication *}
6.422 +lemma nat_mult_assoc: "(m * n) * k = m * ((n * k)::nat)"
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.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.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.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.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.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.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.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.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.524
6.525  text {* needs @{text "!!k"} for @{text add_ac} to work *}
6.526 @@ -758,106 +845,6 @@
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.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.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.585 -
6.586 -lemma add_mult_distrib2: "k * (m + n) = (k * m) + ((k * n)::nat)"
6.588 -
6.589 -text {* Associative law for multiplication *}
6.590 -lemma mult_assoc: "(m * n) * k = m * ((n * k)::nat)"
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.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.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.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.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.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.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.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.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.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.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.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.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.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"},
```