# HG changeset patch
# User paulson
# Date 1069753023 -3600
# Node ID b963e9cee2a0877f08921315abfa2e3c1f7d88f2
# Parent  08b34c902618a16f49167dec08461c22304eb31b
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
to Isar script.

diff -r 08b34c902618 -r b963e9cee2a0 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Mon Nov 24 15:33:07 2003 +0100
+++ b/src/HOL/Divides.thy	Tue Nov 25 10:37:03 2003 +0100
@@ -6,7 +6,7 @@
 The division operators div, mod and the divides relation "dvd"
 *)
 
-theory Divides = NatArith files("Divides_lemmas.ML"):
+theory Divides = NatArith:
 
 (*We use the same class for div and mod;
   moreover, dvd is defined whenever multiplication is*)
@@ -32,7 +32,7 @@
                           (%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m"
 
 (*The definition of dvd is polymorphic!*)
-  dvd_def:   "m dvd n == EX k. n = m*k"
+  dvd_def:   "m dvd n == \<exists>k. n = m*k"
 
 (*This definition helps prove the harder properties of div and mod.
   It is copied from IntDiv.thy; should it be overloaded?*)
@@ -40,11 +40,612 @@
   quorem :: "(nat*nat) * (nat*nat) => bool"
     "quorem == %((a,b), (q,r)).
                       a = b*q + r &
-                      (if 0<b then 0<=r & r<b else b<r & r <=0)"
+                      (if 0<b then 0\<le>r & r<b else b<r & r \<le>0)"
+
+
+
+subsection{*Initial Lemmas*}
+
+lemmas wf_less_trans = 
+       def_wfrec [THEN trans, OF eq_reflection wf_pred_nat [THEN wf_trancl],
+                  standard]
+
+lemma mod_eq: "(%m. m mod n) = 
+              wfrec (trancl pred_nat) (%f j. if j<n | n=0 then j else f (j-n))"
+by (simp add: mod_def)
+
+lemma div_eq: "(%m. m div n) = wfrec (trancl pred_nat)  
+               (%f j. if j<n | n=0 then 0 else Suc (f (j-n)))"
+by (simp add: div_def)
+
+
+(** Aribtrary definitions for division by zero.  Useful to simplify 
+    certain equations **)
+
+lemma DIVISION_BY_ZERO_DIV [simp]: "a div 0 = (0::nat)"
+by (rule div_eq [THEN wf_less_trans], simp)
+
+lemma DIVISION_BY_ZERO_MOD [simp]: "a mod 0 = (a::nat)"
+by (rule mod_eq [THEN wf_less_trans], simp)
+
+
+subsection{*Remainder*}
+
+lemma mod_less [simp]: "m<n ==> m mod n = (m::nat)"
+by (rule mod_eq [THEN wf_less_trans], simp)
+
+lemma mod_geq: "~ m < (n::nat) ==> m mod n = (m-n) mod n"
+apply (case_tac "n=0", simp) 
+apply (rule mod_eq [THEN wf_less_trans])
+apply (simp add: diff_less cut_apply less_eq)
+done
+
+(*Avoids the ugly ~m<n above*)
+lemma le_mod_geq: "(n::nat) \<le> m ==> m mod n = (m-n) mod n"
+by (simp add: mod_geq not_less_iff_le)
+
+lemma mod_if: "m mod (n::nat) = (if m<n then m else (m-n) mod n)"
+by (simp add: mod_geq)
+
+lemma mod_1 [simp]: "m mod Suc 0 = 0"
+apply (induct_tac "m")
+apply (simp_all (no_asm_simp) add: mod_geq)
+done
+
+lemma mod_self [simp]: "n mod n = (0::nat)"
+apply (case_tac "n=0")
+apply (simp_all add: mod_geq)
+done
+
+lemma mod_add_self2 [simp]: "(m+n) mod n = m mod (n::nat)"
+apply (subgoal_tac " (n + m) mod n = (n+m-n) mod n") 
+apply (simp add: add_commute)
+apply (subst mod_geq [symmetric], simp_all)
+done
+
+lemma mod_add_self1 [simp]: "(n+m) mod n = m mod (n::nat)"
+by (simp add: add_commute mod_add_self2)
+
+lemma mod_mult_self1 [simp]: "(m + k*n) mod n = m mod (n::nat)"
+apply (induct_tac "k")
+apply (simp_all add: add_left_commute [of _ n])
+done
+
+lemma mod_mult_self2 [simp]: "(m + n*k) mod n = m mod (n::nat)"
+by (simp add: mult_commute mod_mult_self1)
+
+lemma mod_mult_distrib: "(m mod n) * (k::nat) = (m*k) mod (n*k)"
+apply (case_tac "n=0", simp)
+apply (case_tac "k=0", simp)
+apply (induct_tac "m" rule: nat_less_induct)
+apply (subst mod_if, simp)
+apply (simp add: mod_geq diff_less diff_mult_distrib)
+done
+
+lemma mod_mult_distrib2: "(k::nat) * (m mod n) = (k*m) mod (k*n)"
+by (simp add: mult_commute [of k] mod_mult_distrib)
+
+lemma mod_mult_self_is_0 [simp]: "(m*n) mod n = (0::nat)"
+apply (case_tac "n=0", simp)
+apply (induct_tac "m", simp)
+apply (rename_tac "k")
+apply (cut_tac m = "k*n" and n = n in mod_add_self2)
+apply (simp add: add_commute)
+done
+
+lemma mod_mult_self1_is_0 [simp]: "(n*m) mod n = (0::nat)"
+by (simp add: mult_commute mod_mult_self_is_0)
+
+
+subsection{*Quotient*}
+
+lemma div_less [simp]: "m<n ==> m div n = (0::nat)"
+by (rule div_eq [THEN wf_less_trans], simp)
+
+lemma div_geq: "[| 0<n;  ~m<n |] ==> m div n = Suc((m-n) div n)"
+apply (rule div_eq [THEN wf_less_trans])
+apply (simp add: diff_less cut_apply less_eq)
+done
+
+(*Avoids the ugly ~m<n above*)
+lemma le_div_geq: "[| 0<n;  n\<le>m |] ==> m div n = Suc((m-n) div n)"
+by (simp add: div_geq not_less_iff_le)
+
+lemma div_if: "0<n ==> m div n = (if m<n then 0 else Suc((m-n) div n))"
+by (simp add: div_geq)
+
+
+(*Main Result about quotient and remainder.*)
+lemma mod_div_equality: "(m div n)*n + m mod n = (m::nat)"
+apply (case_tac "n=0", simp)
+apply (induct_tac "m" rule: nat_less_induct)
+apply (subst mod_if)
+apply (simp_all (no_asm_simp) add: add_assoc div_geq add_diff_inverse diff_less)
+done
+
+lemma mod_div_equality2: "n * (m div n) + m mod n = (m::nat)"
+apply(cut_tac m = m and n = n in mod_div_equality)
+apply(simp add: mult_commute)
+done
+
+subsection{*Simproc for Cancelling Div and Mod*}
+
+lemma div_mod_equality: "((m div n)*n + m mod n) + k = (m::nat) + k"
+apply(simp add: mod_div_equality)
+done
+
+lemma div_mod_equality2: "(n*(m div n) + m mod n) + k = (m::nat) + k"
+apply(simp add: mod_div_equality2)
+done
+
+ML
+{*
+val div_mod_equality = thm "div_mod_equality";
+val div_mod_equality2 = thm "div_mod_equality2";
+
+
+structure CancelDivModData =
+struct
+
+val div_name = "Divides.op div";
+val mod_name = "Divides.op mod";
+val mk_binop = HOLogic.mk_binop;
+val mk_sum = NatArithUtils.mk_sum;
+val dest_sum = NatArithUtils.dest_sum;
+
+(*logic*)
+
+val div_mod_eqs = map mk_meta_eq [div_mod_equality,div_mod_equality2]
+
+val trans = trans
+
+val prove_eq_sums =
+  let val simps = add_0 :: add_0_right :: add_ac
+  in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all simps) end
+
+end;
+
+structure CancelDivMod = CancelDivModFun(CancelDivModData);
+
+val cancel_div_mod_proc = NatArithUtils.prep_simproc
+      ("cancel_div_mod", ["(m::nat) + n"], CancelDivMod.proc);
+
+Addsimprocs[cancel_div_mod_proc];
+*}
+
+
+(* a simple rearrangement of mod_div_equality: *)
+lemma mult_div_cancel: "(n::nat) * (m div n) = m - (m mod n)"
+by (cut_tac m = m and n = n in mod_div_equality2, arith)
+
+lemma mod_less_divisor [simp]: "0<n ==> m mod n < (n::nat)"
+apply (induct_tac "m" rule: nat_less_induct)
+apply (case_tac "na<n", simp) 
+txt{*case @{term "n \<le> na"}*}
+apply (simp add: mod_geq diff_less)
+done
+
+lemma div_mult_self_is_m [simp]: "0<n ==> (m*n) div n = (m::nat)"
+by (cut_tac m = "m*n" and n = n in mod_div_equality, auto)
+
+lemma div_mult_self1_is_m [simp]: "0<n ==> (n*m) div n = (m::nat)"
+by (simp add: mult_commute div_mult_self_is_m)
+
+(*mod_mult_distrib2 above is the counterpart for remainder*)
+
+
+subsection{*Proving facts about Quotient and Remainder*}
+
+lemma unique_quotient_lemma:
+     "[| b*q' + r'  \<le> b*q + r;  0 < b;  r < b |]  
+      ==> q' \<le> (q::nat)"
+apply (rule leI)
+apply (subst less_iff_Suc_add)
+apply (auto simp add: add_mult_distrib2)
+done
+
+lemma unique_quotient:
+     "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  0 < b |]  
+      ==> q = q'"
+apply (simp add: split_ifs quorem_def)
+apply (blast intro: order_antisym 
+             dest: order_eq_refl [THEN unique_quotient_lemma] sym)+
+done
+
+lemma unique_remainder:
+     "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  0 < b |]  
+      ==> r = r'"
+apply (subgoal_tac "q = q'")
+prefer 2 apply (blast intro: unique_quotient)
+apply (simp add: quorem_def)
+done
+
+lemma quorem_div_mod: "0 < b ==> quorem ((a, b), (a div b, a mod b))"
+by (auto simp add: quorem_def)
+
+lemma quorem_div: "[| quorem((a,b),(q,r));  0 < b |] ==> a div b = q"
+by (simp add: quorem_div_mod [THEN unique_quotient])
+
+lemma quorem_mod: "[| quorem((a,b),(q,r));  0 < b |] ==> a mod b = r"
+by (simp add: quorem_div_mod [THEN unique_remainder])
+
+(** A dividend of zero **)
+
+lemma div_0 [simp]: "0 div m = (0::nat)"
+by (case_tac "m=0", simp_all)
+
+lemma mod_0 [simp]: "0 mod m = (0::nat)"
+by (case_tac "m=0", simp_all)
+
+(** proving (a*b) div c = a * (b div c) + a * (b mod c) **)
+
+lemma quorem_mult1_eq:
+     "[| quorem((b,c),(q,r));  0 < c |]  
+      ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))"
+apply (auto simp add: split_ifs mult_ac quorem_def add_mult_distrib2)
+done
+
+lemma div_mult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::nat)"
+apply (case_tac "c = 0", simp)
+apply (blast intro: quorem_div_mod [THEN quorem_mult1_eq, THEN quorem_div])
+done
+
+lemma mod_mult1_eq: "(a*b) mod c = a*(b mod c) mod (c::nat)"
+apply (case_tac "c = 0", simp)
+apply (blast intro: quorem_div_mod [THEN quorem_mult1_eq, THEN quorem_mod])
+done
+
+lemma mod_mult1_eq': "(a*b) mod (c::nat) = ((a mod c) * b) mod c"
+apply (rule trans)
+apply (rule_tac s = "b*a mod c" in trans)
+apply (rule_tac [2] mod_mult1_eq)
+apply (simp_all (no_asm) add: mult_commute)
+done
+
+lemma mod_mult_distrib_mod: "(a*b) mod (c::nat) = ((a mod c) * (b mod c)) mod c"
+apply (rule mod_mult1_eq' [THEN trans])
+apply (rule mod_mult1_eq)
+done
+
+(** proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) **)
+
+lemma quorem_add1_eq:
+     "[| quorem((a,c),(aq,ar));  quorem((b,c),(bq,br));  0 < c |]  
+      ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))"
+by (auto simp add: split_ifs mult_ac quorem_def add_mult_distrib2)
+
+(*NOT suitable for rewriting: the RHS has an instance of the LHS*)
+lemma div_add1_eq:
+     "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
+apply (case_tac "c = 0", simp)
+apply (blast intro: quorem_add1_eq [THEN quorem_div] quorem_div_mod quorem_div_mod)
+done
+
+lemma mod_add1_eq: "(a+b) mod (c::nat) = (a mod c + b mod c) mod c"
+apply (case_tac "c = 0", simp)
+apply (blast intro: quorem_div_mod quorem_div_mod
+                    quorem_add1_eq [THEN quorem_mod])
+done
+
+
+subsection{*Proving @{term "a div (b*c) = (a div b) div c"}*}
+
+(** first, a lemma to bound the remainder **)
+
+lemma mod_lemma: "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c"
+apply (cut_tac m = q and n = c in mod_less_divisor)
+apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
+apply (erule_tac P = "%x. ?lhs < ?rhs x" in ssubst)
+apply (simp add: add_mult_distrib2)
+done
 
-use "Divides_lemmas.ML"
+lemma quorem_mult2_eq: "[| quorem ((a,b), (q,r));  0 < b;  0 < c |]  
+      ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))"
+apply (auto simp add: mult_ac quorem_def add_mult_distrib2 [symmetric] mod_lemma)
+done
+
+lemma div_mult2_eq: "a div (b*c) = (a div b) div (c::nat)"
+apply (case_tac "b=0", simp)
+apply (case_tac "c=0", simp)
+apply (force simp add: quorem_div_mod [THEN quorem_mult2_eq, THEN quorem_div])
+done
+
+lemma mod_mult2_eq: "a mod (b*c) = b*(a div b mod c) + a mod (b::nat)"
+apply (case_tac "b=0", simp)
+apply (case_tac "c=0", simp)
+apply (auto simp add: mult_commute quorem_div_mod [THEN quorem_mult2_eq, THEN quorem_mod])
+done
+
+
+subsection{*Cancellation of Common Factors in Division*}
+
+lemma div_mult_mult_lemma:
+     "[| (0::nat) < b;  0 < c |] ==> (c*a) div (c*b) = a div b"
+by (auto simp add: div_mult2_eq)
+
+lemma div_mult_mult1 [simp]: "(0::nat) < c ==> (c*a) div (c*b) = a div b"
+apply (case_tac "b = 0")
+apply (auto simp add: linorder_neq_iff [of b] div_mult_mult_lemma)
+done
+
+lemma div_mult_mult2 [simp]: "(0::nat) < c ==> (a*c) div (b*c) = a div b"
+apply (drule div_mult_mult1)
+apply (auto simp add: mult_commute)
+done
+
+
+(*Distribution of Factors over Remainders:
+
+Could prove these as in Integ/IntDiv.ML, but we already have
+mod_mult_distrib and mod_mult_distrib2 above!
+
+Goal "(c*a) mod (c*b) = (c::nat) * (a mod b)"
+qed "mod_mult_mult1";
+
+Goal "(a*c) mod (b*c) = (a mod b) * (c::nat)";
+qed "mod_mult_mult2";
+ ***)
+
+subsection{*Further Facts about Quotient and Remainder*}
+
+lemma div_1 [simp]: "m div Suc 0 = m"
+apply (induct_tac "m")
+apply (simp_all (no_asm_simp) add: div_geq)
+done
+
+lemma div_self [simp]: "0<n ==> n div n = (1::nat)"
+by (simp add: div_geq)
+
+lemma div_add_self2: "0<n ==> (m+n) div n = Suc (m div n)"
+apply (subgoal_tac " (n + m) div n = Suc ((n+m-n) div n) ")
+apply (simp add: add_commute)
+apply (subst div_geq [symmetric], simp_all)
+done
+
+lemma div_add_self1: "0<n ==> (n+m) div n = Suc (m div n)"
+by (simp add: add_commute div_add_self2)
+
+lemma div_mult_self1 [simp]: "!!n::nat. 0<n ==> (m + k*n) div n = k + m div n"
+apply (subst div_add1_eq)
+apply (subst div_mult1_eq, simp)
+done
+
+lemma div_mult_self2 [simp]: "0<n ==> (m + n*k) div n = k + m div (n::nat)"
+by (simp add: mult_commute div_mult_self1)
+
+
+(* Monotonicity of div in first argument *)
+lemma div_le_mono [rule_format (no_asm)]:
+     "\<forall>m::nat. m \<le> n --> (m div k) \<le> (n div k)"
+apply (case_tac "k=0", simp)
+apply (induct_tac "n" rule: nat_less_induct, clarify)
+apply (case_tac "n<k")
+(* 1  case n<k *)
+apply simp
+(* 2  case n >= k *)
+apply (case_tac "m<k")
+(* 2.1  case m<k *)
+apply simp
+(* 2.2  case m>=k *)
+apply (simp add: div_geq diff_less diff_le_mono)
+done
+
+(* Antimonotonicity of div in second argument *)
+lemma div_le_mono2: "!!m::nat. [| 0<m; m\<le>n |] ==> (k div n) \<le> (k div m)"
+apply (subgoal_tac "0<n")
+ prefer 2 apply simp 
+apply (induct_tac "k" rule: nat_less_induct)
+apply (rename_tac "k")
+apply (case_tac "k<n", simp)
+apply (subgoal_tac "~ (k<m) ")
+ prefer 2 apply simp 
+apply (simp add: div_geq)
+apply (subgoal_tac " (k-n) div n \<le> (k-m) div n")
+ prefer 2
+ apply (blast intro: div_le_mono diff_le_mono2)
+apply (rule le_trans, simp)
+apply (simp add: diff_less)
+done
+
+lemma div_le_dividend [simp]: "m div n \<le> (m::nat)"
+apply (case_tac "n=0", simp)
+apply (subgoal_tac "m div n \<le> m div 1", simp)
+apply (rule div_le_mono2)
+apply (simp_all (no_asm_simp))
+done
+
+(* Similar for "less than" *) 
+lemma div_less_dividend [rule_format, simp]:
+     "!!n::nat. 1<n ==> 0 < m --> m div n < m"
+apply (induct_tac "m" rule: nat_less_induct)
+apply (rename_tac "m")
+apply (case_tac "m<n", simp)
+apply (subgoal_tac "0<n")
+ prefer 2 apply simp 
+apply (simp add: div_geq)
+apply (case_tac "n<m")
+ apply (subgoal_tac " (m-n) div n < (m-n) ")
+  apply (rule impI less_trans_Suc)+
+apply assumption
+  apply (simp_all add: diff_less)
+done
+
+text{*A fact for the mutilated chess board*}
+lemma mod_Suc: "Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))"
+apply (case_tac "n=0", simp)
+apply (induct_tac "m" rule: nat_less_induct)
+apply (case_tac "Suc (na) <n")
+(* case Suc(na) < n *)
+apply (frule lessI [THEN less_trans], simp add: less_not_refl3)
+(* case n \<le> Suc(na) *)
+apply (simp add: not_less_iff_le le_Suc_eq mod_geq)
+apply (auto simp add: Suc_diff_le diff_less le_mod_geq)
+done
+
+
+subsection{*The Divides Relation*}
+
+lemma dvdI [intro?]: "n = m * k ==> m dvd n"
+by (unfold dvd_def, blast)
+
+lemma dvdE [elim?]: "!!P. [|m dvd n;  !!k. n = m*k ==> P|] ==> P"
+by (unfold dvd_def, blast)
 
-declare dvdI [intro?]  dvdE [elim?]  dvd_trans [trans]
+lemma dvd_0_right [iff]: "m dvd (0::nat)"
+apply (unfold dvd_def)
+apply (blast intro: mult_0_right [symmetric])
+done
+
+lemma dvd_0_left: "0 dvd m ==> m = (0::nat)"
+by (force simp add: dvd_def)
+
+lemma dvd_0_left_iff [iff]: "(0 dvd (m::nat)) = (m = 0)"
+by (blast intro: dvd_0_left)
+
+lemma dvd_1_left [iff]: "Suc 0 dvd k"
+by (unfold dvd_def, simp)
+
+lemma dvd_1_iff_1 [simp]: "(m dvd Suc 0) = (m = Suc 0)"
+by (simp add: dvd_def)
+
+lemma dvd_refl [simp]: "m dvd (m::nat)"
+apply (unfold dvd_def)
+apply (blast intro: mult_1_right [symmetric])
+done
+
+lemma dvd_trans [trans]: "[| m dvd n; n dvd p |] ==> m dvd (p::nat)"
+apply (unfold dvd_def)
+apply (blast intro: mult_assoc)
+done
+
+lemma dvd_anti_sym: "[| m dvd n; n dvd m |] ==> m = (n::nat)"
+apply (unfold dvd_def)
+apply (force dest: mult_eq_self_implies_10 simp add: mult_assoc mult_eq_1_iff)
+done
+
+lemma dvd_add: "[| k dvd m; k dvd n |] ==> k dvd (m+n :: nat)"
+apply (unfold dvd_def)
+apply (blast intro: add_mult_distrib2 [symmetric])
+done
+
+lemma dvd_diff: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"
+apply (unfold dvd_def)
+apply (blast intro: diff_mult_distrib2 [symmetric])
+done
+
+lemma dvd_diffD: "[| k dvd m-n; k dvd n; n\<le>m |] ==> k dvd (m::nat)"
+apply (erule not_less_iff_le [THEN iffD2, THEN add_diff_inverse, THEN subst])
+apply (blast intro: dvd_add)
+done
+
+lemma dvd_diffD1: "[| k dvd m-n; k dvd m; n\<le>m |] ==> k dvd (n::nat)"
+by (drule_tac m = m in dvd_diff, auto)
+
+lemma dvd_mult: "k dvd n ==> k dvd (m*n :: nat)"
+apply (unfold dvd_def)
+apply (blast intro: mult_left_commute)
+done
+
+lemma dvd_mult2: "k dvd m ==> k dvd (m*n :: nat)"
+apply (subst mult_commute)
+apply (erule dvd_mult)
+done
+
+(* k dvd (m*k) *)
+declare dvd_refl [THEN dvd_mult, iff] dvd_refl [THEN dvd_mult2, iff]
+
+lemma dvd_reduce: "(k dvd n + k) = (k dvd (n::nat))"
+apply (rule iffI)
+apply (erule_tac [2] dvd_add)
+apply (rule_tac [2] dvd_refl)
+apply (subgoal_tac "n = (n+k) -k")
+ prefer 2 apply simp 
+apply (erule ssubst)
+apply (erule dvd_diff)
+apply (rule dvd_refl)
+done
+
+lemma dvd_mod: "!!n::nat. [| f dvd m; f dvd n |] ==> f dvd m mod n"
+apply (unfold dvd_def)
+apply (case_tac "n=0", auto)
+apply (blast intro: mod_mult_distrib2 [symmetric])
+done
+
+lemma dvd_mod_imp_dvd: "[| (k::nat) dvd m mod n;  k dvd n |] ==> k dvd m"
+apply (subgoal_tac "k dvd (m div n) *n + m mod n")
+ apply (simp add: mod_div_equality)
+apply (simp only: dvd_add dvd_mult)
+done
+
+lemma dvd_mod_iff: "k dvd n ==> ((k::nat) dvd m mod n) = (k dvd m)"
+by (blast intro: dvd_mod_imp_dvd dvd_mod)
+
+lemma dvd_mult_cancel: "!!k::nat. [| k*m dvd k*n; 0<k |] ==> m dvd n"
+apply (unfold dvd_def)
+apply (erule exE)
+apply (simp add: mult_ac)
+done
+
+lemma dvd_mult_cancel1: "0<m ==> (m*n dvd m) = (n = (1::nat))"
+apply auto
+apply (subgoal_tac "m*n dvd m*1")
+apply (drule dvd_mult_cancel, auto)
+done
+
+lemma dvd_mult_cancel2: "0<m ==> (n*m dvd m) = (n = (1::nat))"
+apply (subst mult_commute)
+apply (erule dvd_mult_cancel1)
+done
+
+lemma mult_dvd_mono: "[| i dvd m; j dvd n|] ==> i*j dvd (m*n :: nat)"
+apply (unfold dvd_def, clarify)
+apply (rule_tac x = "k*ka" in exI)
+apply (simp add: mult_ac)
+done
+
+lemma dvd_mult_left: "(i*j :: nat) dvd k ==> i dvd k"
+by (simp add: dvd_def mult_assoc, blast)
+
+lemma dvd_mult_right: "(i*j :: nat) dvd k ==> j dvd k"
+apply (unfold dvd_def, clarify)
+apply (rule_tac x = "i*k" in exI)
+apply (simp add: mult_ac)
+done
+
+lemma dvd_imp_le: "[| k dvd n; 0 < n |] ==> k \<le> (n::nat)"
+apply (unfold dvd_def, clarify)
+apply (simp_all (no_asm_use) add: zero_less_mult_iff)
+apply (erule conjE)
+apply (rule le_trans)
+apply (rule_tac [2] le_refl [THEN mult_le_mono])
+apply (erule_tac [2] Suc_leI, simp)
+done
+
+lemma dvd_eq_mod_eq_0: "!!k::nat. (k dvd n) = (n mod k = 0)"
+apply (unfold dvd_def)
+apply (case_tac "k=0", simp, safe)
+apply (simp add: mult_commute)
+apply (rule_tac t = n and n1 = k in mod_div_equality [THEN subst])
+apply (subst mult_commute, simp)
+done
+
+lemma dvd_mult_div_cancel: "n dvd m ==> n * (m div n) = (m::nat)"
+apply (subgoal_tac "m mod n = 0")
+ apply (simp add: mult_div_cancel)
+apply (simp only: dvd_eq_mod_eq_0)
+done
+
+lemma mod_eq_0_iff: "(m mod d = 0) = (\<exists>q::nat. m = d*q)"
+by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
+declare mod_eq_0_iff [THEN iffD1, dest!]
+
+(*Loses information, namely we also have r<d provided d is nonzero*)
+lemma mod_eqD: "(m mod d = r) ==> \<exists>q::nat. m = r + q*d"
+apply (cut_tac m = m in mod_div_equality)
+apply (simp only: add_ac)
+apply (blast intro: sym)
+done
+
 
 lemma split_div:
  "P(n div k :: nat) =
@@ -87,7 +688,7 @@
 qed
 
 lemma split_div_lemma:
-  "0 < n \<Longrightarrow> (n * q <= m \<and> m < n * (Suc q)) = (q = ((m::nat) div n))"
+  "0 < n \<Longrightarrow> (n * q \<le> m \<and> m < n * (Suc q)) = (q = ((m::nat) div n))"
   apply (rule iffI)
   apply (rule_tac a=m and r = "m - n * q" and r' = "m mod n" in unique_quotient)
   apply (simp_all add: quorem_def, arith)
@@ -103,7 +704,7 @@
 
 theorem split_div':
   "P ((m::nat) div n) = ((n = 0 \<and> P 0) \<or>
-   (\<exists>q. (n * q <= m \<and> m < n * (Suc q)) \<and> P q))"
+   (\<exists>q. (n * q \<le> m \<and> m < n * (Suc q)) \<and> P q))"
   apply (case_tac "0 < n")
   apply (simp only: add: split_div_lemma)
   apply (simp_all add: DIVISION_BY_ZERO_DIV)
@@ -148,6 +749,106 @@
   apply arith
   done
 
+ML
+{*
+val div_def = thm "div_def"
+val mod_def = thm "mod_def"
+val dvd_def = thm "dvd_def"
+val quorem_def = thm "quorem_def"
+
+val wf_less_trans = thm "wf_less_trans";
+val mod_eq = thm "mod_eq";
+val div_eq = thm "div_eq";
+val DIVISION_BY_ZERO_DIV = thm "DIVISION_BY_ZERO_DIV";
+val DIVISION_BY_ZERO_MOD = thm "DIVISION_BY_ZERO_MOD";
+val mod_less = thm "mod_less";
+val mod_geq = thm "mod_geq";
+val le_mod_geq = thm "le_mod_geq";
+val mod_if = thm "mod_if";
+val mod_1 = thm "mod_1";
+val mod_self = thm "mod_self";
+val mod_add_self2 = thm "mod_add_self2";
+val mod_add_self1 = thm "mod_add_self1";
+val mod_mult_self1 = thm "mod_mult_self1";
+val mod_mult_self2 = thm "mod_mult_self2";
+val mod_mult_distrib = thm "mod_mult_distrib";
+val mod_mult_distrib2 = thm "mod_mult_distrib2";
+val mod_mult_self_is_0 = thm "mod_mult_self_is_0";
+val mod_mult_self1_is_0 = thm "mod_mult_self1_is_0";
+val div_less = thm "div_less";
+val div_geq = thm "div_geq";
+val le_div_geq = thm "le_div_geq";
+val div_if = thm "div_if";
+val mod_div_equality = thm "mod_div_equality";
+val mod_div_equality2 = thm "mod_div_equality2";
+val div_mod_equality = thm "div_mod_equality";
+val div_mod_equality2 = thm "div_mod_equality2";
+val mult_div_cancel = thm "mult_div_cancel";
+val mod_less_divisor = thm "mod_less_divisor";
+val div_mult_self_is_m = thm "div_mult_self_is_m";
+val div_mult_self1_is_m = thm "div_mult_self1_is_m";
+val unique_quotient_lemma = thm "unique_quotient_lemma";
+val unique_quotient = thm "unique_quotient";
+val unique_remainder = thm "unique_remainder";
+val div_0 = thm "div_0";
+val mod_0 = thm "mod_0";
+val div_mult1_eq = thm "div_mult1_eq";
+val mod_mult1_eq = thm "mod_mult1_eq";
+val mod_mult1_eq' = thm "mod_mult1_eq'";
+val mod_mult_distrib_mod = thm "mod_mult_distrib_mod";
+val div_add1_eq = thm "div_add1_eq";
+val mod_add1_eq = thm "mod_add1_eq";
+val mod_lemma = thm "mod_lemma";
+val div_mult2_eq = thm "div_mult2_eq";
+val mod_mult2_eq = thm "mod_mult2_eq";
+val div_mult_mult_lemma = thm "div_mult_mult_lemma";
+val div_mult_mult1 = thm "div_mult_mult1";
+val div_mult_mult2 = thm "div_mult_mult2";
+val div_1 = thm "div_1";
+val div_self = thm "div_self";
+val div_add_self2 = thm "div_add_self2";
+val div_add_self1 = thm "div_add_self1";
+val div_mult_self1 = thm "div_mult_self1";
+val div_mult_self2 = thm "div_mult_self2";
+val div_le_mono = thm "div_le_mono";
+val div_le_mono2 = thm "div_le_mono2";
+val div_le_dividend = thm "div_le_dividend";
+val div_less_dividend = thm "div_less_dividend";
+val mod_Suc = thm "mod_Suc";
+val dvdI = thm "dvdI";
+val dvdE = thm "dvdE";
+val dvd_0_right = thm "dvd_0_right";
+val dvd_0_left = thm "dvd_0_left";
+val dvd_0_left_iff = thm "dvd_0_left_iff";
+val dvd_1_left = thm "dvd_1_left";
+val dvd_1_iff_1 = thm "dvd_1_iff_1";
+val dvd_refl = thm "dvd_refl";
+val dvd_trans = thm "dvd_trans";
+val dvd_anti_sym = thm "dvd_anti_sym";
+val dvd_add = thm "dvd_add";
+val dvd_diff = thm "dvd_diff";
+val dvd_diffD = thm "dvd_diffD";
+val dvd_diffD1 = thm "dvd_diffD1";
+val dvd_mult = thm "dvd_mult";
+val dvd_mult2 = thm "dvd_mult2";
+val dvd_reduce = thm "dvd_reduce";
+val dvd_mod = thm "dvd_mod";
+val dvd_mod_imp_dvd = thm "dvd_mod_imp_dvd";
+val dvd_mod_iff = thm "dvd_mod_iff";
+val dvd_mult_cancel = thm "dvd_mult_cancel";
+val dvd_mult_cancel1 = thm "dvd_mult_cancel1";
+val dvd_mult_cancel2 = thm "dvd_mult_cancel2";
+val mult_dvd_mono = thm "mult_dvd_mono";
+val dvd_mult_left = thm "dvd_mult_left";
+val dvd_mult_right = thm "dvd_mult_right";
+val dvd_imp_le = thm "dvd_imp_le";
+val dvd_eq_mod_eq_0 = thm "dvd_eq_mod_eq_0";
+val dvd_mult_div_cancel = thm "dvd_mult_div_cancel";
+val mod_eq_0_iff = thm "mod_eq_0_iff";
+val mod_eqD = thm "mod_eqD";
+*}
+
+
 (*
 lemma split_div:
 assumes m: "m \<noteq> 0"
diff -r 08b34c902618 -r b963e9cee2a0 src/HOL/Divides_lemmas.ML
--- a/src/HOL/Divides_lemmas.ML	Mon Nov 24 15:33:07 2003 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,734 +0,0 @@
-(*  Title:      HOL/Divides.ML
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1993  University of Cambridge
-
-The division operators div, mod and the divides relation "dvd"
-*)
-
-(* ML legacy bindings *)
-
-val div_def = thm "div_def";
-val mod_def = thm "mod_def";
-val dvd_def = thm "dvd_def";
-val quorem_def = thm "quorem_def";
-
-structure Divides =
-struct
- val div_def = div_def
- val mod_def = mod_def
- val dvd_def = dvd_def
- val quorem_def = quorem_def
-end;
-
-(** Less-then properties **)
-
-bind_thm ("wf_less_trans", [eq_reflection, wf_pred_nat RS wf_trancl] MRS 
-                    def_wfrec RS trans);
-
-Goal "(%m. m mod n) = wfrec (trancl pred_nat) \
-\                           (%f j. if j<n | n=0 then j else f (j-n))";
-by (simp_tac (simpset() addsimps [mod_def]) 1);
-qed "mod_eq";
-
-Goal "(%m. m div n) = wfrec (trancl pred_nat) \
-\            (%f j. if j<n | n=0 then 0 else Suc (f (j-n)))";
-by (simp_tac (simpset() addsimps [div_def]) 1);
-qed "div_eq";
-
-
-(** Aribtrary definitions for division by zero.  Useful to simplify 
-    certain equations **)
-
-Goal "a div 0 = (0::nat)";
-by (rtac (div_eq RS wf_less_trans) 1);
-by (Asm_simp_tac 1);
-qed "DIVISION_BY_ZERO_DIV";  (*NOT for adding to default simpset*)
-
-Goal "a mod 0 = (a::nat)";
-by (rtac (mod_eq RS wf_less_trans) 1);
-by (Asm_simp_tac 1);
-qed "DIVISION_BY_ZERO_MOD";  (*NOT for adding to default simpset*)
-
-fun div_undefined_case_tac s i =
-  case_tac s i THEN 
-  Full_simp_tac (i+1) THEN
-  asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO_DIV, 
-				    DIVISION_BY_ZERO_MOD]) i;
-
-(*** Remainder ***)
-
-Goal "m<n ==> m mod n = (m::nat)";
-by (rtac (mod_eq RS wf_less_trans) 1);
-by (Asm_simp_tac 1);
-qed "mod_less";
-Addsimps [mod_less];
-
-Goal "~ m < (n::nat) ==> m mod n = (m-n) mod n";
-by (div_undefined_case_tac "n=0" 1);
-by (rtac (mod_eq RS wf_less_trans) 1);
-by (asm_simp_tac (simpset() addsimps [diff_less, cut_apply, less_eq]) 1);
-qed "mod_geq";
-
-(*Avoids the ugly ~m<n above*)
-Goal "(n::nat) <= m ==> m mod n = (m-n) mod n";
-by (asm_simp_tac (simpset() addsimps [mod_geq, not_less_iff_le]) 1);
-qed "le_mod_geq";
-
-Goal "m mod (n::nat) = (if m<n then m else (m-n) mod n)";
-by (asm_simp_tac (simpset() addsimps [mod_geq]) 1);
-qed "mod_if";
-
-Goal "m mod Suc 0 = 0";
-by (induct_tac "m" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_geq])));
-qed "mod_1";
-Addsimps [mod_1];
-
-Goal "n mod n = (0::nat)";
-by (div_undefined_case_tac "n=0" 1);
-by (asm_simp_tac (simpset() addsimps [mod_geq]) 1);
-qed "mod_self";
-Addsimps [mod_self];
-
-Goal "(m+n) mod n = m mod (n::nat)";
-by (subgoal_tac "(n + m) mod n = (n+m-n) mod n" 1);
-by (stac (mod_geq RS sym) 2);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_commute])));
-qed "mod_add_self2";
-
-Goal "(n+m) mod n = m mod (n::nat)";
-by (asm_simp_tac (simpset() addsimps [add_commute, mod_add_self2]) 1);
-qed "mod_add_self1";
-
-Addsimps [mod_add_self1, mod_add_self2];
-
-Goal "(m + k*n) mod n = m mod (n::nat)";
-by (induct_tac "k" 1);
-by (ALLGOALS
-    (asm_simp_tac 
-     (simpset() addsimps [read_instantiate [("y","n")] add_left_commute])));
-qed "mod_mult_self1";
-
-Goal "(m + n*k) mod n = m mod (n::nat)";
-by (asm_simp_tac (simpset() addsimps [mult_commute, mod_mult_self1]) 1);
-qed "mod_mult_self2";
-
-Addsimps [mod_mult_self1, mod_mult_self2];
-
-Goal "(m mod n) * (k::nat) = (m*k) mod (n*k)";
-by (div_undefined_case_tac "n=0" 1);
-by (div_undefined_case_tac "k=0" 1);
-by (induct_thm_tac nat_less_induct "m" 1);
-by (stac mod_if 1);
-by (Asm_simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [mod_geq, 
-				      diff_less, diff_mult_distrib]) 1);
-qed "mod_mult_distrib";
-
-Goal "(k::nat) * (m mod n) = (k*m) mod (k*n)";
-by (asm_simp_tac 
-    (simpset() addsimps [read_instantiate [("m","k")] mult_commute, 
-			 mod_mult_distrib]) 1);
-qed "mod_mult_distrib2";
-
-Goal "(m*n) mod n = (0::nat)";
-by (div_undefined_case_tac "n=0" 1);
-by (induct_tac "m" 1);
-by (Asm_simp_tac 1);
-by (rename_tac "k" 1);
-by (cut_inst_tac [("m","k*n"),("n","n")] mod_add_self2 1);
-by (asm_full_simp_tac (simpset() addsimps [add_commute]) 1);
-qed "mod_mult_self_is_0";
-
-Goal "(n*m) mod n = (0::nat)";
-by (simp_tac (simpset() addsimps [mult_commute, mod_mult_self_is_0]) 1);
-qed "mod_mult_self1_is_0";
-Addsimps [mod_mult_self_is_0, mod_mult_self1_is_0];
-
-
-(*** Quotient ***)
-
-Goal "m<n ==> m div n = (0::nat)";
-by (rtac (div_eq RS wf_less_trans) 1);
-by (Asm_simp_tac 1);
-qed "div_less";
-Addsimps [div_less];
-
-Goal "[| 0<n;  ~m<n |] ==> m div n = Suc((m-n) div n)";
-by (rtac (div_eq RS wf_less_trans) 1);
-by (asm_simp_tac (simpset() addsimps [diff_less, cut_apply, less_eq]) 1);
-qed "div_geq";
-
-(*Avoids the ugly ~m<n above*)
-Goal "[| 0<n;  n<=m |] ==> m div n = Suc((m-n) div n)";
-by (asm_simp_tac (simpset() addsimps [div_geq, not_less_iff_le]) 1);
-qed "le_div_geq";
-
-Goal "0<n ==> m div n = (if m<n then 0 else Suc((m-n) div n))";
-by (asm_simp_tac (simpset() addsimps [div_geq]) 1);
-qed "div_if";
-
-
-(*Main Result about quotient and remainder.*)
-Goal "(m div n)*n + m mod n = (m::nat)";
-by (div_undefined_case_tac "n=0" 1);
-by (induct_thm_tac nat_less_induct "m" 1);
-by (stac mod_if 1);
-by (ALLGOALS (asm_simp_tac 
-	      (simpset() addsimps [add_assoc, div_geq,
-				   add_diff_inverse, diff_less])));
-qed "mod_div_equality";
-
-Goal "n * (m div n) + m mod n = (m::nat)";
-by(cut_inst_tac [("m","m"),("n","n")] mod_div_equality 1);
-by(asm_full_simp_tac (simpset() addsimps [mult_commute]) 1);
-qed "mod_div_equality2";
-
-(*-----------------------------------------------------------------------*)
-(*Simproc for cancelling div and mod                                     *)
-(*-----------------------------------------------------------------------*)
-
-Goal "((m div n)*n + m mod n) + k = (m::nat) + k";
-by(simp_tac (simpset() addsimps [mod_div_equality]) 1);
-qed "div_mod_equality";
-
-Goal "(n*(m div n) + m mod n) + k = (m::nat) + k";
-by(simp_tac (simpset() addsimps [thm"mod_div_equality2"]) 1);
-qed "div_mod_equality2";
-
-structure CancelDivModData =
-struct
-
-val div_name = "Divides.op div";
-val mod_name = "Divides.op mod";
-val mk_binop = HOLogic.mk_binop;
-val mk_sum = NatArithUtils.mk_sum;
-val dest_sum = NatArithUtils.dest_sum;
-
-(*logic*)
-
-val div_mod_eqs = map mk_meta_eq [div_mod_equality,div_mod_equality2]
-
-val trans = trans
-
-val prove_eq_sums =
-  let val simps = add_0 :: add_0_right :: add_ac
-  in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all simps) end
-
-end;
-
-structure CancelDivMod = CancelDivModFun(CancelDivModData);
-
-val cancel_div_mod_proc = NatArithUtils.prep_simproc
-      ("cancel_div_mod", ["(m::nat) + n"], CancelDivMod.proc);
-
-Addsimprocs[cancel_div_mod_proc];
-
-
-(* a simple rearrangement of mod_div_equality: *)
-Goal "(n::nat) * (m div n) = m - (m mod n)";
-by (cut_inst_tac [("m","m"),("n","n")] mod_div_equality2 1);
-by (arith_tac 1);
-qed "mult_div_cancel";
-
-Goal "0<n ==> m mod n < (n::nat)";
-by (induct_thm_tac nat_less_induct "m" 1);
-by (case_tac "na<n" 1);
-(*case n le na*)
-by (asm_full_simp_tac (simpset() addsimps [mod_geq, diff_less]) 2);
-(*case na<n*)
-by (Asm_simp_tac 1);
-qed "mod_less_divisor";
-Addsimps [mod_less_divisor];
-
-(*** More division laws ***)
-
-Goal "0<n ==> (m*n) div n = (m::nat)";
-by (cut_inst_tac [("m", "m*n"),("n","n")] mod_div_equality 1);
-by Auto_tac;
-qed "div_mult_self_is_m";
-
-Goal "0<n ==> (n*m) div n = (m::nat)";
-by (asm_simp_tac (simpset() addsimps [mult_commute, div_mult_self_is_m]) 1);
-qed "div_mult_self1_is_m";
-Addsimps [div_mult_self_is_m, div_mult_self1_is_m];
-
-(*mod_mult_distrib2 above is the counterpart for remainder*)
-
-
-(*** Proving facts about div and mod using quorem ***)
-
-Goal "[| b*q' + r'  <= b*q + r;  0 < b;  r < b |] \
-\     ==> q' <= (q::nat)";
-by (rtac leI 1); 
-by (stac less_iff_Suc_add 1);
-by (auto_tac (claset(), simpset() addsimps [add_mult_distrib2]));   
-qed "unique_quotient_lemma";
-
-Goal "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  0 < b |] \
-\     ==> q = q'";
-by (asm_full_simp_tac 
-    (simpset() addsimps split_ifs @ [Divides.quorem_def]) 1);  
-by (REPEAT 
-    (blast_tac (claset() addIs [order_antisym]
-			 addDs [order_eq_refl RS unique_quotient_lemma, 
-				sym]) 1));
-qed "unique_quotient";
-
-Goal "[| quorem ((a,b), (q,r));  quorem ((a,b), (q',r'));  0 < b |] \
-\     ==> r = r'";
-by (subgoal_tac "q = q'" 1);
-by (blast_tac (claset() addIs [unique_quotient]) 2);
-by (asm_full_simp_tac (simpset() addsimps [Divides.quorem_def]) 1);
-qed "unique_remainder";
-
-Goal "0 < b ==> quorem ((a, b), (a div b, a mod b))";
-by (auto_tac
-    (claset() addEs [sym],
-     simpset() addsimps mult_ac@[Divides.quorem_def]));
-qed "quorem_div_mod";
-
-Goal "[| quorem((a,b),(q,r));  0 < b |] ==> a div b = q";
-by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS unique_quotient]) 1);
-qed "quorem_div";
-
-Goal "[| quorem((a,b),(q,r));  0 < b |] ==> a mod b = r";
-by (asm_simp_tac (simpset() addsimps [quorem_div_mod RS unique_remainder]) 1);
-qed "quorem_mod";
-
-(** A dividend of zero **)
-
-Goal "0 div m = (0::nat)";
-by (div_undefined_case_tac "m=0" 1);
-by (Asm_simp_tac 1);
-qed "div_0"; 
-
-Goal "0 mod m = (0::nat)";
-by (div_undefined_case_tac "m=0" 1);
-by (Asm_simp_tac 1);
-qed "mod_0"; 
-Addsimps [div_0, mod_0];
-
-(** proving (a*b) div c = a * (b div c) + a * (b mod c) **)
-
-Goal "[| quorem((b,c),(q,r));  0 < c |] \
-\     ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))";
-by (auto_tac
-    (claset(),
-     simpset() addsimps split_ifs@mult_ac@
-                        [Divides.quorem_def, add_mult_distrib2]));
-val lemma = result();
-
-Goal "(a*b) div c = a*(b div c) + a*(b mod c) div (c::nat)";
-by (div_undefined_case_tac "c = 0" 1);
-by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_div]) 1);
-qed "div_mult1_eq";
-
-Goal "(a*b) mod c = a*(b mod c) mod (c::nat)";
-by (div_undefined_case_tac "c = 0" 1);
-by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_mod]) 1);
-qed "mod_mult1_eq";
-
-Goal "(a*b) mod (c::nat) = ((a mod c) * b) mod c";
-by (rtac trans 1);
-by (res_inst_tac [("s","b*a mod c")] trans 1);
-by (rtac mod_mult1_eq 2);
-by (ALLGOALS (simp_tac (simpset() addsimps [mult_commute])));
-qed "mod_mult1_eq'";
-
-Goal "(a*b) mod (c::nat) = ((a mod c) * (b mod c)) mod c";
-by (rtac (mod_mult1_eq' RS trans) 1);
-by (rtac mod_mult1_eq 1);
-qed "mod_mult_distrib_mod";
-
-(** proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) **)
-
-Goal "[| quorem((a,c),(aq,ar));  quorem((b,c),(bq,br));  0 < c |] \
-\     ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))";
-by (auto_tac
-    (claset(),
-     simpset() addsimps split_ifs@mult_ac@
-                        [Divides.quorem_def, add_mult_distrib2]));
-val lemma = result();
-
-(*NOT suitable for rewriting: the RHS has an instance of the LHS*)
-Goal "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)";
-by (div_undefined_case_tac "c = 0" 1);
-by (blast_tac (claset() addIs [[quorem_div_mod,quorem_div_mod]
-			       MRS lemma RS quorem_div]) 1);
-qed "div_add1_eq";
-
-Goal "(a+b) mod (c::nat) = (a mod c + b mod c) mod c";
-by (div_undefined_case_tac "c = 0" 1);
-by (blast_tac (claset() addIs [[quorem_div_mod,quorem_div_mod]
-			       MRS lemma RS quorem_mod]) 1);
-qed "mod_add1_eq";
-
-
-(*** proving  a div (b*c) = (a div b) div c ***)
-
-(** first, a lemma to bound the remainder **)
-
-Goal "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c";
-by (cut_inst_tac [("m","q"),("n","c")] mod_less_divisor 1);
-by (dres_inst_tac [("m","q mod c")] less_imp_Suc_add 2); 
-by Auto_tac;  
-by (eres_inst_tac [("P","%x. ?lhs < ?rhs x")] ssubst 1); 
-by (asm_simp_tac (simpset() addsimps [add_mult_distrib2]) 1);
-val mod_lemma = result();
-
-Goal "[| quorem ((a,b), (q,r));  0 < b;  0 < c |] \
-\     ==> quorem ((a, b*c), (q div c, b*(q mod c) + r))";
-by (auto_tac  
-    (claset(),
-     simpset() addsimps mult_ac@
-                        [Divides.quorem_def, add_mult_distrib2 RS sym,
-			 mod_lemma]));
-val lemma = result();
-
-Goal "a div (b*c) = (a div b) div (c::nat)";
-by (div_undefined_case_tac "b=0" 1);
-by (div_undefined_case_tac "c=0" 1);
-by (force_tac (claset(),
-	       simpset() addsimps [quorem_div_mod RS lemma RS quorem_div]) 1);
-qed "div_mult2_eq";
-
-Goal "a mod (b*c) = b*(a div b mod c) + a mod (b::nat)";
-by (div_undefined_case_tac "b=0" 1);
-by (div_undefined_case_tac "c=0" 1);
-by (auto_tac (claset(),
-	       simpset() addsimps [mult_commute, 
-				   quorem_div_mod RS lemma RS quorem_mod]));
-qed "mod_mult2_eq";
-
-
-(*** Cancellation of common factors in "div" ***)
-
-Goal "[| (0::nat) < b;  0 < c |] ==> (c*a) div (c*b) = a div b";
-by (stac div_mult2_eq 1);
-by Auto_tac;
-val lemma1 = result();
-
-Goal "(0::nat) < c ==> (c*a) div (c*b) = a div b";
-by (div_undefined_case_tac "b = 0" 1);
-by (auto_tac
-    (claset(), 
-     simpset() addsimps [read_instantiate [("x", "b")] linorder_neq_iff, 
-			 lemma1, lemma2]));
-qed "div_mult_mult1";
-
-Goal "(0::nat) < c ==> (a*c) div (b*c) = a div b";
-by (dtac div_mult_mult1 1);
-by (auto_tac (claset(), simpset() addsimps [mult_commute]));
-qed "div_mult_mult2";
-
-Addsimps [div_mult_mult1, div_mult_mult2];
-
-
-(*** Distribution of factors over "mod"
-
-Could prove these as in Integ/IntDiv.ML, but we already have
-mod_mult_distrib and mod_mult_distrib2 above!
-
-Goal "(c*a) mod (c*b) = (c::nat) * (a mod b)";
-qed "mod_mult_mult1";
-
-Goal "(a*c) mod (b*c) = (a mod b) * (c::nat)";
-qed "mod_mult_mult2";
- ***)
-
-(*** Further facts about div and mod ***)
-
-Goal "m div Suc 0 = m";
-by (induct_tac "m" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [div_geq])));
-qed "div_1";
-Addsimps [div_1];
-
-Goal "0<n ==> n div n = (1::nat)";
-by (asm_simp_tac (simpset() addsimps [div_geq]) 1);
-qed "div_self";
-Addsimps [div_self];
-
-Goal "0<n ==> (m+n) div n = Suc (m div n)";
-by (subgoal_tac "(n + m) div n = Suc ((n+m-n) div n)" 1);
-by (stac (div_geq RS sym) 2);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_commute])));
-qed "div_add_self2";
-
-Goal "0<n ==> (n+m) div n = Suc (m div n)";
-by (asm_simp_tac (simpset() addsimps [add_commute, div_add_self2]) 1);
-qed "div_add_self1";
-
-Goal "!!n::nat. 0<n ==> (m + k*n) div n = k + m div n";
-by (stac div_add1_eq 1); 
-by (stac div_mult1_eq 1); 
-by (Asm_simp_tac 1); 
-qed "div_mult_self1";
-
-Goal "0<n ==> (m + n*k) div n = k + m div (n::nat)";
-by (asm_simp_tac (simpset() addsimps [mult_commute, div_mult_self1]) 1);
-qed "div_mult_self2";
-
-Addsimps [div_mult_self1, div_mult_self2];
-
-(* Monotonicity of div in first argument *)
-Goal "ALL m::nat. m <= n --> (m div k) <= (n div k)";
-by (div_undefined_case_tac "k=0" 1);
-by (induct_thm_tac nat_less_induct "n" 1);
-by (Clarify_tac 1);
-by (case_tac "n<k" 1);
-(* 1  case n<k *)
-by (Asm_simp_tac 1);
-(* 2  case n >= k *)
-by (case_tac "m<k" 1);
-(* 2.1  case m<k *)
-by (Asm_simp_tac 1);
-(* 2.2  case m>=k *)
-by (asm_simp_tac (simpset() addsimps [div_geq, diff_less, diff_le_mono]) 1);
-qed_spec_mp "div_le_mono";
-
-(* Antimonotonicity of div in second argument *)
-Goal "!!m::nat. [| 0<m; m<=n |] ==> (k div n) <= (k div m)";
-by (subgoal_tac "0<n" 1);
- by (Asm_simp_tac 2);
-by (induct_thm_tac nat_less_induct "k" 1);
-by (rename_tac "k" 1);
-by (case_tac "k<n" 1);
- by (Asm_simp_tac 1);
-by (subgoal_tac "~(k<m)" 1);
- by (Asm_simp_tac 2);
-by (asm_simp_tac (simpset() addsimps [div_geq]) 1);
-by (subgoal_tac "(k-n) div n <= (k-m) div n" 1);
- by (REPEAT (ares_tac [div_le_mono,diff_le_mono2] 2));
-by (rtac le_trans 1);
-by (Asm_simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [diff_less]) 1);
-qed "div_le_mono2";
-
-Goal "m div n <= (m::nat)";
-by (div_undefined_case_tac "n=0" 1);
-by (subgoal_tac "m div n <= m div 1" 1);
-by (Asm_full_simp_tac 1);
-by (rtac div_le_mono2 1);
-by (ALLGOALS Asm_simp_tac);
-qed "div_le_dividend";
-Addsimps [div_le_dividend];
-
-(* Similar for "less than" *)
-Goal "!!n::nat. 1<n ==> (0 < m) --> (m div n < m)";
-by (induct_thm_tac nat_less_induct "m" 1);
-by (rename_tac "m" 1);
-by (case_tac "m<n" 1);
- by (Asm_full_simp_tac 1);
-by (subgoal_tac "0<n" 1);
- by (Asm_simp_tac 2);
-by (asm_full_simp_tac (simpset() addsimps [div_geq]) 1);
-by (case_tac "n<m" 1);
- by (subgoal_tac "(m-n) div n < (m-n)" 1);
-  by (REPEAT (ares_tac [impI,less_trans_Suc] 1));
-  by (asm_full_simp_tac (simpset() addsimps [diff_less]) 1);
- by (asm_full_simp_tac (simpset() addsimps [diff_less]) 1);
-(* case n=m *)
-by (subgoal_tac "m=n" 1);
- by (Asm_simp_tac 2);
-by (Asm_simp_tac 1);
-qed_spec_mp "div_less_dividend";
-Addsimps [div_less_dividend];
-
-(*** Further facts about mod (mainly for the mutilated chess board ***)
-
-Goal "Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))";
-by (div_undefined_case_tac "n=0" 1);
-by (induct_thm_tac nat_less_induct "m" 1);
-by (case_tac "Suc(na)<n" 1);
-(* case Suc(na) < n *)
-by (forward_tac [lessI RS less_trans] 1 
-    THEN asm_simp_tac (simpset() addsimps [less_not_refl3]) 1);
-(* case n <= Suc(na) *)
-by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, le_Suc_eq, 
-					   mod_geq]) 1);
-by (auto_tac (claset(), 
-	      simpset() addsimps [Suc_diff_le, diff_less, le_mod_geq]));
-qed "mod_Suc";
-
-
-(************************************************)
-(** Divides Relation                           **)
-(************************************************)
-
-Goalw [dvd_def] "n = m * k ==> m dvd n";
-by (Blast_tac 1); 
-qed "dvdI";
-
-Goalw [dvd_def] "!!P. [|m dvd n;  !!k. n = m*k ==> P|] ==> P";
-by (Blast_tac 1); 
-qed "dvdE";
-
-Goalw [dvd_def] "m dvd (0::nat)";
-by (blast_tac (claset() addIs [mult_0_right RS sym]) 1);
-qed "dvd_0_right";
-AddIffs [dvd_0_right];
-
-Goalw [dvd_def] "0 dvd m ==> m = (0::nat)";
-by Auto_tac;
-qed "dvd_0_left";
-
-Goal "(0 dvd (m::nat)) = (m = 0)";
-by (blast_tac (claset() addIs [dvd_0_left]) 1); 
-qed "dvd_0_left_iff";
-AddIffs [dvd_0_left_iff];
-
-Goalw [dvd_def] "Suc 0 dvd k";
-by (Simp_tac 1);
-qed "dvd_1_left";
-AddIffs [dvd_1_left];
-
-Goal "(m dvd Suc 0) = (m = Suc 0)";
-by (simp_tac (simpset() addsimps [dvd_def]) 1); 
-qed "dvd_1_iff_1";
-Addsimps [dvd_1_iff_1];
-
-Goalw [dvd_def] "m dvd (m::nat)";
-by (blast_tac (claset() addIs [mult_1_right RS sym]) 1);
-qed "dvd_refl";
-Addsimps [dvd_refl];
-
-Goalw [dvd_def] "[| m dvd n; n dvd p |] ==> m dvd (p::nat)";
-by (blast_tac (claset() addIs [mult_assoc] ) 1);
-qed "dvd_trans";
-
-Goalw [dvd_def] "[| m dvd n; n dvd m |] ==> m = (n::nat)";
-by (force_tac (claset() addDs [mult_eq_self_implies_10],
-	       simpset() addsimps [mult_assoc, mult_eq_1_iff]) 1);
-qed "dvd_anti_sym";
-
-Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m+n :: nat)";
-by (blast_tac (claset() addIs [add_mult_distrib2 RS sym]) 1);
-qed "dvd_add";
-
-Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)";
-by (blast_tac (claset() addIs [diff_mult_distrib2 RS sym]) 1);
-qed "dvd_diff";
-
-Goal "[| k dvd m-n; k dvd n; n<=m |] ==> k dvd (m::nat)";
-by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1);
-by (blast_tac (claset() addIs [dvd_add]) 1);
-qed "dvd_diffD";
-
-Goal "[| k dvd m-n; k dvd m; n<=m |] ==> k dvd (n::nat)";
-by (dres_inst_tac [("m","m")] dvd_diff 1);
-by Auto_tac;  
-qed "dvd_diffD1";
-
-Goalw [dvd_def] "k dvd n ==> k dvd (m*n :: nat)";
-by (blast_tac (claset() addIs [mult_left_commute]) 1);
-qed "dvd_mult";
-
-Goal "k dvd m ==> k dvd (m*n :: nat)";
-by (stac mult_commute 1);
-by (etac dvd_mult 1);
-qed "dvd_mult2";
-
-(* k dvd (m*k) *)
-AddIffs [dvd_refl RS dvd_mult, dvd_refl RS dvd_mult2];
-
-Goal "(k dvd n + k) = (k dvd (n::nat))";
-by (rtac iffI 1);
-by (etac dvd_add 2);
-by (rtac dvd_refl 2);
-by (subgoal_tac "n = (n+k)-k" 1);
-by  (Simp_tac 2);
-by (etac ssubst 1);
-by (etac dvd_diff 1);
-by (rtac dvd_refl 1);
-qed "dvd_reduce";
-
-Goalw [dvd_def] "!!n::nat. [| f dvd m; f dvd n |] ==> f dvd m mod n";
-by (div_undefined_case_tac "n=0" 1);
-by Auto_tac; 
-by (blast_tac (claset() addIs [mod_mult_distrib2 RS sym]) 1);  
-qed "dvd_mod";
-
-Goal "[| (k::nat) dvd m mod n;  k dvd n |] ==> k dvd m";
-by (subgoal_tac "k dvd (m div n)*n + m mod n" 1);
-by (asm_simp_tac (HOL_basic_ss addsimps [dvd_add, dvd_mult]) 2);
-by (asm_full_simp_tac (simpset() addsimps [mod_div_equality]) 1);
-qed "dvd_mod_imp_dvd";
-
-Goal "k dvd n ==> ((k::nat) dvd m mod n) = (k dvd m)";
-by (blast_tac (claset() addIs [dvd_mod_imp_dvd, dvd_mod]) 1); 
-qed "dvd_mod_iff";
-
-Goalw [dvd_def]  "!!k::nat. [| k*m dvd k*n; 0<k |] ==> m dvd n";
-by (etac exE 1);
-by (asm_full_simp_tac (simpset() addsimps mult_ac) 1);
-qed "dvd_mult_cancel";
-
-Goal "0<m ==> (m*n dvd m) = (n = (1::nat))";
-by Auto_tac;  
-by (subgoal_tac "m*n dvd m*1" 1);
-by (dtac dvd_mult_cancel 1); 
-by Auto_tac;  
-qed "dvd_mult_cancel1";
-
-Goal "0<m ==> (n*m dvd m) = (n = (1::nat))";
-by (stac mult_commute 1); 
-by (etac dvd_mult_cancel1 1); 
-qed "dvd_mult_cancel2";
-
-Goalw [dvd_def] "[| i dvd m; j dvd n|] ==> i*j dvd (m*n :: nat)";
-by (Clarify_tac 1);
-by (res_inst_tac [("x","k*ka")] exI 1);
-by (asm_simp_tac (simpset() addsimps mult_ac) 1);
-qed "mult_dvd_mono";
-
-Goalw [dvd_def] "(i*j :: nat) dvd k ==> i dvd k";
-by (full_simp_tac (simpset() addsimps [mult_assoc]) 1);
-by (Blast_tac 1);
-qed "dvd_mult_left";
-
-Goalw [dvd_def] "(i*j :: nat) dvd k ==> j dvd k";
-by (Clarify_tac 1);
-by (res_inst_tac [("x","i*k")] exI 1);
-by (simp_tac (simpset() addsimps mult_ac) 1);
-qed "dvd_mult_right";
-
-Goalw [dvd_def] "[| k dvd n; 0 < n |] ==> k <= (n::nat)";
-by (Clarify_tac 1);
-by (ALLGOALS (full_simp_tac (simpset() addsimps [zero_less_mult_iff])));
-by (etac conjE 1);
-by (rtac le_trans 1);
-by (rtac (le_refl RS mult_le_mono) 2);
-by (etac Suc_leI 2);
-by (Simp_tac 1);
-qed "dvd_imp_le";
-
-Goalw [dvd_def] "!!k::nat. (k dvd n) = (n mod k = 0)";
-by (div_undefined_case_tac "k=0" 1);
-by Safe_tac;
-by (asm_simp_tac (simpset() addsimps [mult_commute]) 1);
-by (res_inst_tac [("t","n"),("n1","k")] (mod_div_equality RS subst) 1);
-by (stac mult_commute 1);
-by (Asm_simp_tac 1);
-qed "dvd_eq_mod_eq_0";
-
-Goal "n dvd m ==> n * (m div n) = (m::nat)";
-by (subgoal_tac "m mod n = 0" 1);
- by (asm_full_simp_tac (simpset() addsimps [mult_div_cancel]) 1);
-by (asm_full_simp_tac (HOL_basic_ss addsimps [dvd_eq_mod_eq_0]) 1);
-qed "dvd_mult_div_cancel";
-
-Goal "(m mod d = 0) = (EX q::nat. m = d*q)";
-by (auto_tac (claset(), 
-     simpset() addsimps [dvd_eq_mod_eq_0 RS sym, dvd_def]));  
-qed "mod_eq_0_iff";
-AddSDs [mod_eq_0_iff RS iffD1];
-
-(*Loses information, namely we also have r<d provided d is nonzero*)
-Goal "(m mod d = r) ==> EX q::nat. m = r + q*d";
-by (cut_inst_tac [("m","m")] mod_div_equality 1);
-by (full_simp_tac (HOL_basic_ss addsimps add_ac) 1); 
-by (blast_tac (claset() addIs [sym]) 1); 
-qed "mod_eqD";
diff -r 08b34c902618 -r b963e9cee2a0 src/HOL/Integ/Int.thy
--- a/src/HOL/Integ/Int.thy	Mon Nov 24 15:33:07 2003 +0100
+++ b/src/HOL/Integ/Int.thy	Tue Nov 25 10:37:03 2003 +0100
@@ -239,15 +239,6 @@
 
 subsection{*Instances of the equations above, for zero*}
 
-(*instantiate a variable to zero and simplify*)
-
-declare zless_zminus [of 0, simplified, simp]
-declare zminus_zless [of _ 0, simplified, simp]
-declare zle_zminus   [of 0, simplified, simp]
-declare zminus_zle [of _ 0, simplified, simp]
-declare equation_zminus [of 0, simplified, simp]
-declare zminus_equation [of _ 0, simplified, simp]
-
 lemma negative_zless_0: "- (int (Suc n)) < 0"
 by (simp add: zless_def)
 
@@ -343,53 +334,10 @@
 apply (auto simp add: nat_mono_iff linorder_not_less)
 done
 
-(* a case theorem distinguishing non-negative and negative int *)  
-
-lemma int_cases: 
-     "[|!! n. z = int n ==> P;  !! n. z =  - (int (Suc n)) ==> P |] ==> P"
-apply (case_tac "neg z")
-apply (fast dest!: negD)
-apply (drule not_neg_nat [symmetric], auto) 
-done
-
-
-subsection{*Monotonicity of Multiplication*}
-
-lemma zmult_zle_mono1_lemma: "i \<le> (j::int) ==> i * int k \<le> j * int k"
-apply (induct_tac "k")
-apply (simp_all (no_asm_simp) add: int_Suc zadd_zmult_distrib2 zadd_zle_mono int_Suc0_eq_1)
-done
-
-lemma zmult_zle_mono1: "[| i \<le> j;  (0::int) \<le> k |] ==> i*k \<le> j*k"
-apply (rule_tac t = k in not_neg_nat [THEN subst])
-apply (erule_tac [2] zmult_zle_mono1_lemma)
-apply (simp (no_asm_use) add: not_neg_eq_ge_0)
-done
 
-lemma zmult_zle_mono1_neg: "[| i \<le> j;  k \<le> (0::int) |] ==> j*k \<le> i*k"
-apply (rule zminus_zle_zminus [THEN iffD1])
-apply (simp add: zmult_zminus_right [symmetric] zmult_zle_mono1 zle_zminus)
-done
-
-lemma zmult_zle_mono2: "[| i \<le> j;  (0::int) \<le> k |] ==> k*i \<le> k*j"
-apply (drule zmult_zle_mono1)
-apply (simp_all add: zmult_commute)
-done
+subsection{*Strict Monotonicity of Multiplication*}
 
-lemma zmult_zle_mono2_neg: "[| i \<le> j;  k \<le> (0::int) |] ==> k*j \<le> k*i"
-apply (drule zmult_zle_mono1_neg)
-apply (simp_all add: zmult_commute)
-done
-
-(* \<le> monotonicity, BOTH arguments*)
-lemma zmult_zle_mono: "[| i \<le> j;  k \<le> l;  (0::int) \<le> j;  (0::int) \<le> k |] ==> i*k \<le> j*l"
-apply (erule zmult_zle_mono1 [THEN order_trans], assumption)
-apply (erule zmult_zle_mono2, assumption)
-done
-
-
-subsection{*strict, in 1st argument; proof is by induction on k>0*}
-
+text{*strict, in 1st argument; proof is by induction on k>0*}
 lemma zmult_zless_mono2_lemma: "i<j ==> 0<k --> int k * i < int k * j"
 apply (induct_tac "k", simp) 
 apply (simp add: int_Suc)
@@ -423,6 +371,25 @@
   show "\<bar>i\<bar> = (if i < 0 then -i else i)" by (simp only: zabs_def)
 qed
 
+subsection{*Monotonicity of Multiplication*}
+
+lemma zmult_zle_mono1: "[| i \<le> j;  (0::int) \<le> k |] ==> i*k \<le> j*k"
+  by (rule mult_right_mono)
+
+lemma zmult_zle_mono1_neg: "[| i \<le> j;  k \<le> (0::int) |] ==> j*k \<le> i*k"
+  by (rule mult_right_mono_neg)
+
+lemma zmult_zle_mono2: "[| i \<le> j;  (0::int) \<le> k |] ==> k*i \<le> k*j"
+  by (rule mult_left_mono)
+
+lemma zmult_zle_mono2_neg: "[| i \<le> j;  k \<le> (0::int) |] ==> k*j \<le> k*i"
+  by (rule mult_left_mono_neg)
+
+(* \<le> monotonicity, BOTH arguments*)
+lemma zmult_zle_mono:
+     "[| i \<le> j;  k \<le> l;  (0::int) \<le> j;  (0::int) \<le> k |] ==> i*k \<le> j*l"
+  by (rule mult_mono)
+
 lemma zmult_zless_mono1: "[| i<j;  (0::int) < k |] ==> i*k < j*k"
   by (rule Ring_and_Field.mult_strict_right_mono)
 
@@ -467,6 +434,16 @@
 apply (auto simp add: int_Suc symmetric zdiff_def)
 done
 
+(* a case theorem distinguishing non-negative and negative int *)  
+
+lemma int_cases: 
+     "[|!! n. z = int n ==> P;  !! n. z =  - (int (Suc n)) ==> P |] ==> P"
+apply (case_tac "neg z")
+apply (fast dest!: negD)
+apply (drule not_neg_nat [symmetric], auto) 
+done
+
+
 
 
 ML
diff -r 08b34c902618 -r b963e9cee2a0 src/HOL/Integ/nat_simprocs.ML
--- a/src/HOL/Integ/nat_simprocs.ML	Mon Nov 24 15:33:07 2003 +0100
+++ b/src/HOL/Integ/nat_simprocs.ML	Tue Nov 25 10:37:03 2003 +0100
@@ -211,7 +211,7 @@
 
 (*Simplify 1*n and n*1 to n*)
 val add_0s  = map rename_numerals [add_0, add_0_right];
-val mult_1s = map rename_numerals [mult_1, mult_1_right];
+val mult_1s = map rename_numerals [thm"nat_mult_1", thm"nat_mult_1_right"];
 
 (*Final simplification: cancel + and *; replace Numeral0 by 0 and Numeral1 by 1*)
 
diff -r 08b34c902618 -r b963e9cee2a0 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Nov 24 15:33:07 2003 +0100
+++ b/src/HOL/IsaMakefile	Tue Nov 25 10:37:03 2003 +0100
@@ -80,7 +80,7 @@
   $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML \
   $(SRC)/TFL/rules.ML $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML \
   $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML \
-  Datatype.thy Datatype_Universe.ML Datatype_Universe.thy Divides_lemmas.ML \
+  Datatype.thy Datatype_Universe.ML Datatype_Universe.thy \
   Divides.thy Extraction.thy Finite_Set.ML Finite_Set.thy \
   Fun.thy Gfp.ML Gfp.thy \
   Hilbert_Choice.thy Hilbert_Choice_lemmas.ML HOL.ML \
diff -r 08b34c902618 -r b963e9cee2a0 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Mon Nov 24 15:33:07 2003 +0100
+++ b/src/HOL/Nat.thy	Tue Nov 25 10:37:03 2003 +0100
@@ -21,7 +21,7 @@
 axioms
   -- {* the axiom of infinity in 2 parts *}
   inj_Suc_Rep:          "inj Suc_Rep"
-  Suc_Rep_not_Zero_Rep: "Suc_Rep x ~= Zero_Rep"
+  Suc_Rep_not_Zero_Rep: "Suc_Rep x \<noteq> Zero_Rep"
 
 
 subsection {* Type nat *}
@@ -64,7 +64,7 @@
 
   less_def: "m < n == (m, n) : trancl pred_nat"
 
-  le_def: "m <= (n::nat) == ~ (n < m)"
+  le_def: "m \<le> (n::nat) == ~ (n < m)"
 
 
 text {* Induction *}
@@ -91,14 +91,14 @@
 
 text {* Distinctness of constructors *}
 
-lemma Suc_not_Zero [iff]: "Suc m ~= 0"
+lemma Suc_not_Zero [iff]: "Suc m \<noteq> 0"
   apply (unfold Zero_nat_def Suc_def)
   apply (rule inj_on_Abs_Nat [THEN inj_on_contraD])
   apply (rule Suc_Rep_not_Zero_Rep)
   apply (rule Rep_Nat Nat.Suc_RepI Nat.Zero_RepI)+
   done
 
-lemma Zero_not_Suc [iff]: "0 ~= Suc m"
+lemma Zero_not_Suc [iff]: "0 \<noteq> Suc m"
   by (rule not_sym, rule Suc_not_Zero not_sym)
 
 lemma Suc_neq_Zero: "Suc m = 0 ==> R"
@@ -127,7 +127,7 @@
   apply (erule arg_cong)
   done
 
-lemma nat_not_singleton: "(ALL x. x = (0::nat)) = False"
+lemma nat_not_singleton: "(\<forall>x. x = (0::nat)) = False"
   by auto
 
 text {* @{typ nat} is a datatype *}
@@ -137,10 +137,10 @@
   inject    Suc_Suc_eq
   induction nat_induct
 
-lemma n_not_Suc_n: "n ~= Suc n"
+lemma n_not_Suc_n: "n \<noteq> Suc n"
   by (induct n) simp_all
 
-lemma Suc_n_not_n: "Suc t ~= t"
+lemma Suc_n_not_n: "Suc t \<noteq> t"
   by (rule not_sym, rule n_not_Suc_n)
 
 text {* A special form of induction for reasoning
@@ -219,9 +219,9 @@
 lemma less_irrefl [elim!]: "(n::nat) < n ==> R"
   by (rule notE, rule less_not_refl)
 
-lemma less_not_refl2: "n < m ==> m ~= (n::nat)" by blast
+lemma less_not_refl2: "n < m ==> m \<noteq> (n::nat)" by blast
 
-lemma less_not_refl3: "(s::nat) < t ==> s ~= t"
+lemma less_not_refl3: "(s::nat) < t ==> s \<noteq> t"
   by (rule not_sym, rule less_not_refl2)
 
 lemma lessE:
@@ -268,7 +268,7 @@
   apply (blast intro: Suc_mono less_SucI elim: lessE)
   done
 
-lemma nat_neq_iff: "((m::nat) ~= n) = (m < n | n < m)"
+lemma nat_neq_iff: "((m::nat) \<noteq> n) = (m < n | n < m)"
   using less_linear by blast
 
 lemma nat_less_cases: assumes major: "(m::nat) < n ==> P n m"
@@ -284,7 +284,7 @@
 
 subsubsection {* Inductive (?) properties *}
 
-lemma Suc_lessI: "m < n ==> Suc m ~= n ==> Suc m < n"
+lemma Suc_lessI: "m < n ==> Suc m \<noteq> n ==> Suc m < n"
   apply (simp add: nat_neq_iff)
   apply (blast elim!: less_irrefl less_SucE elim: less_asym)
   done
@@ -324,7 +324,7 @@
 
 text {* Complete induction, aka course-of-values induction *}
 lemma nat_less_induct:
-  assumes prem: "!!n. ALL m::nat. m < n --> P m ==> P n" shows "P n"
+  assumes prem: "!!n. \<forall>m::nat. m < n --> P m ==> P n" shows "P n"
   apply (rule_tac a=n in wf_induct)
   apply (rule wf_pred_nat [THEN wf_trancl])
   apply (rule prem)
@@ -336,119 +336,119 @@
 subsection {* Properties of "less than or equal" *}
 
 text {* Was @{text le_eq_less_Suc}, but this orientation is more useful *}
-lemma less_Suc_eq_le: "(m < Suc n) = (m <= n)"
+lemma less_Suc_eq_le: "(m < Suc n) = (m \<le> n)"
   by (unfold le_def, rule not_less_eq [symmetric])
 
-lemma le_imp_less_Suc: "m <= n ==> m < Suc n"
+lemma le_imp_less_Suc: "m \<le> n ==> m < Suc n"
   by (rule less_Suc_eq_le [THEN iffD2])
 
-lemma le0 [iff]: "(0::nat) <= n"
+lemma le0 [iff]: "(0::nat) \<le> n"
   by (unfold le_def, rule not_less0)
 
-lemma Suc_n_not_le_n: "~ Suc n <= n"
+lemma Suc_n_not_le_n: "~ Suc n \<le> n"
   by (simp add: le_def)
 
-lemma le_0_eq [iff]: "((i::nat) <= 0) = (i = 0)"
+lemma le_0_eq [iff]: "((i::nat) \<le> 0) = (i = 0)"
   by (induct i) (simp_all add: le_def)
 
-lemma le_Suc_eq: "(m <= Suc n) = (m <= n | m = Suc n)"
+lemma le_Suc_eq: "(m \<le> Suc n) = (m \<le> n | m = Suc n)"
   by (simp del: less_Suc_eq_le add: less_Suc_eq_le [symmetric] less_Suc_eq)
 
-lemma le_SucE: "m <= Suc n ==> (m <= n ==> R) ==> (m = Suc n ==> R) ==> R"
+lemma le_SucE: "m \<le> Suc n ==> (m \<le> n ==> R) ==> (m = Suc n ==> R) ==> R"
   by (drule le_Suc_eq [THEN iffD1], rules+)
 
-lemma leI: "~ n < m ==> m <= (n::nat)" by (simp add: le_def)
+lemma leI: "~ n < m ==> m \<le> (n::nat)" by (simp add: le_def)
 
-lemma leD: "m <= n ==> ~ n < (m::nat)"
+lemma leD: "m \<le> n ==> ~ n < (m::nat)"
   by (simp add: le_def)
 
 lemmas leE = leD [elim_format]
 
-lemma not_less_iff_le: "(~ n < m) = (m <= (n::nat))"
+lemma not_less_iff_le: "(~ n < m) = (m \<le> (n::nat))"
   by (blast intro: leI elim: leE)
 
-lemma not_leE: "~ m <= n ==> n<(m::nat)"
+lemma not_leE: "~ m \<le> n ==> n<(m::nat)"
   by (simp add: le_def)
 
-lemma not_le_iff_less: "(~ n <= m) = (m < (n::nat))"
+lemma not_le_iff_less: "(~ n \<le> m) = (m < (n::nat))"
   by (simp add: le_def)
 
-lemma Suc_leI: "m < n ==> Suc(m) <= n"
+lemma Suc_leI: "m < n ==> Suc(m) \<le> n"
   apply (simp add: le_def less_Suc_eq)
   apply (blast elim!: less_irrefl less_asym)
   done -- {* formerly called lessD *}
 
-lemma Suc_leD: "Suc(m) <= n ==> m <= n"
+lemma Suc_leD: "Suc(m) \<le> n ==> m \<le> n"
   by (simp add: le_def less_Suc_eq)
 
 text {* Stronger version of @{text Suc_leD} *}
-lemma Suc_le_lessD: "Suc m <= n ==> m < n"
+lemma Suc_le_lessD: "Suc m \<le> n ==> m < n"
   apply (simp add: le_def less_Suc_eq)
   using less_linear
   apply blast
   done
 
-lemma Suc_le_eq: "(Suc m <= n) = (m < n)"
+lemma Suc_le_eq: "(Suc m \<le> n) = (m < n)"
   by (blast intro: Suc_leI Suc_le_lessD)
 
-lemma le_SucI: "m <= n ==> m <= Suc n"
+lemma le_SucI: "m \<le> n ==> m \<le> Suc n"
   by (unfold le_def) (blast dest: Suc_lessD)
 
-lemma less_imp_le: "m < n ==> m <= (n::nat)"
+lemma less_imp_le: "m < n ==> m \<le> (n::nat)"
   by (unfold le_def) (blast elim: less_asym)
 
-text {* For instance, @{text "(Suc m < Suc n) = (Suc m <= n) = (m < n)"} *}
+text {* For instance, @{text "(Suc m < Suc n) = (Suc m \<le> n) = (m < n)"} *}
 lemmas le_simps = less_imp_le less_Suc_eq_le Suc_le_eq
 
 
-text {* Equivalence of @{term "m <= n"} and @{term "m < n | m = n"} *}
+text {* Equivalence of @{term "m \<le> n"} and @{term "m < n | m = n"} *}
 
-lemma le_imp_less_or_eq: "m <= n ==> m < n | m = (n::nat)"
+lemma le_imp_less_or_eq: "m \<le> n ==> m < n | m = (n::nat)"
   apply (unfold le_def)
   using less_linear
   apply (blast elim: less_irrefl less_asym)
   done
 
-lemma less_or_eq_imp_le: "m < n | m = n ==> m <= (n::nat)"
+lemma less_or_eq_imp_le: "m < n | m = n ==> m \<le> (n::nat)"
   apply (unfold le_def)
   using less_linear
   apply (blast elim!: less_irrefl elim: less_asym)
   done
 
-lemma le_eq_less_or_eq: "(m <= (n::nat)) = (m < n | m=n)"
+lemma le_eq_less_or_eq: "(m \<le> (n::nat)) = (m < n | m=n)"
   by (rules intro: less_or_eq_imp_le le_imp_less_or_eq)
 
 text {* Useful with @{text Blast}. *}
-lemma eq_imp_le: "(m::nat) = n ==> m <= n"
+lemma eq_imp_le: "(m::nat) = n ==> m \<le> n"
   by (rule less_or_eq_imp_le, rule disjI2)
 
-lemma le_refl: "n <= (n::nat)"
+lemma le_refl: "n \<le> (n::nat)"
   by (simp add: le_eq_less_or_eq)
 
-lemma le_less_trans: "[| i <= j; j < k |] ==> i < (k::nat)"
+lemma le_less_trans: "[| i \<le> j; j < k |] ==> i < (k::nat)"
   by (blast dest!: le_imp_less_or_eq intro: less_trans)
 
-lemma less_le_trans: "[| i < j; j <= k |] ==> i < (k::nat)"
+lemma less_le_trans: "[| i < j; j \<le> k |] ==> i < (k::nat)"
   by (blast dest!: le_imp_less_or_eq intro: less_trans)
 
-lemma le_trans: "[| i <= j; j <= k |] ==> i <= (k::nat)"
+lemma le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::nat)"
   by (blast dest!: le_imp_less_or_eq intro: less_or_eq_imp_le less_trans)
 
-lemma le_anti_sym: "[| m <= n; n <= m |] ==> m = (n::nat)"
+lemma le_anti_sym: "[| m \<le> n; n \<le> m |] ==> m = (n::nat)"
   by (blast dest!: le_imp_less_or_eq elim!: less_irrefl elim: less_asym)
 
-lemma Suc_le_mono [iff]: "(Suc n <= Suc m) = (n <= m)"
+lemma Suc_le_mono [iff]: "(Suc n \<le> Suc m) = (n \<le> m)"
   by (simp add: le_simps)
 
 text {* Axiom @{text order_less_le} of class @{text order}: *}
-lemma nat_less_le: "((m::nat) < n) = (m <= n & m ~= n)"
+lemma nat_less_le: "((m::nat) < n) = (m \<le> n & m \<noteq> n)"
   by (simp add: le_def nat_neq_iff) (blast elim!: less_asym)
 
-lemma le_neq_implies_less: "(m::nat) <= n ==> m ~= n ==> m < n"
+lemma le_neq_implies_less: "(m::nat) \<le> n ==> m \<noteq> n ==> m < n"
   by (rule iffD2, rule nat_less_le, rule conjI)
 
 text {* Axiom @{text linorder_linear} of class @{text linorder}: *}
-lemma nat_le_linear: "(m::nat) <= n | n <= m"
+lemma nat_le_linear: "(m::nat) \<le> n | n \<le> m"
   apply (simp add: le_eq_less_or_eq)
   using less_linear
   apply blast
@@ -460,10 +460,10 @@
 
 text {*
   Rewrite @{term "n < Suc m"} to @{term "n = m"}
-  if @{term "~ n < m"} or @{term "m <= n"} hold.
+  if @{term "~ n < m"} or @{term "m \<le> n"} hold.
   Not suitable as default simprules because they often lead to looping
 *}
-lemma le_less_Suc_eq: "m <= n ==> (n < Suc m) = (n = m)"
+lemma le_less_Suc_eq: "m \<le> n ==> (n < Suc m) = (n = m)"
   by (rule not_less_less_Suc_eq, rule leD)
 
 lemmas not_less_simps = not_less_less_Suc_eq le_less_Suc_eq
@@ -526,20 +526,20 @@
 lemma def_nat_rec_Suc: "(!!n. f n == nat_rec c h n) ==> f (Suc n) = h n (f n)"
   by simp
 
-lemma not0_implies_Suc: "n ~= 0 ==> EX m. n = Suc m"
+lemma not0_implies_Suc: "n \<noteq> 0 ==> \<exists>m. n = Suc m"
   by (case_tac n) simp_all
 
-lemma gr_implies_not0: "!!n::nat. m<n ==> n ~= 0"
+lemma gr_implies_not0: "!!n::nat. m<n ==> n \<noteq> 0"
   by (case_tac n) simp_all
 
-lemma neq0_conv [iff]: "!!n::nat. (n ~= 0) = (0 < n)"
+lemma neq0_conv [iff]: "!!n::nat. (n \<noteq> 0) = (0 < n)"
   by (case_tac n) simp_all
 
 text {* This theorem is useful with @{text blast} *}
 lemma gr0I: "((n::nat) = 0 ==> False) ==> 0 < n"
   by (rule iffD1, rule neq0_conv, rules)
 
-lemma gr0_conv_Suc: "(0 < n) = (EX m. n = Suc m)"
+lemma gr0_conv_Suc: "(0 < n) = (\<exists>m. n = Suc m)"
   by (fast intro: not0_implies_Suc)
 
 lemma not_gr0 [iff]: "!!n::nat. (~ (0 < n)) = (n = 0)"
@@ -547,11 +547,11 @@
   apply (rule ccontr, simp_all)
   done
 
-lemma Suc_le_D: "(Suc n <= m') ==> (? m. m' = Suc m)"
+lemma Suc_le_D: "(Suc n \<le> m') ==> (? m. m' = Suc m)"
   by (induct m') simp_all
 
 text {* Useful in certain inductive arguments *}
-lemma less_Suc_eq_0_disj: "(m < Suc n) = (m = 0 | (EX j. m = Suc j & j < n))"
+lemma less_Suc_eq_0_disj: "(m < Suc n) = (m = 0 | (\<exists>j. m = Suc j & j < n))"
   by (case_tac m) simp_all
 
 lemma nat_induct2: "P 0 ==> P (Suc 0) ==> (!!k. P k ==> P (Suc (Suc k))) ==> P n"
@@ -567,21 +567,21 @@
 lemmas Least_le = wellorder_Least_le
 lemmas not_less_Least = wellorder_not_less_Least
 
-lemma Least_Suc: "[| P n; ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
+lemma Least_Suc:
+     "[| P n; ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
   apply (case_tac "n", auto)
   apply (frule LeastI)
   apply (drule_tac P = "%x. P (Suc x) " in LeastI)
-  apply (subgoal_tac " (LEAST x. P x) <= Suc (LEAST x. P (Suc x))")
+  apply (subgoal_tac " (LEAST x. P x) \<le> Suc (LEAST x. P (Suc x))")
   apply (erule_tac [2] Least_le)
   apply (case_tac "LEAST x. P x", auto)
   apply (drule_tac P = "%x. P (Suc x) " in Least_le)
   apply (blast intro: order_antisym)
   done
 
-lemma Least_Suc2: "[|P n; Q m; ~P 0; !k. P (Suc k) = Q k|] ==> Least P = Suc (Least Q)"
-  apply (erule (1) Least_Suc [THEN ssubst])
-  apply simp
-  done
+lemma Least_Suc2:
+     "[|P n; Q m; ~P 0; !k. P (Suc k) = Q k|] ==> Least P = Suc (Least Q)"
+  by (erule (1) Least_Suc [THEN ssubst], simp)
 
 
 
@@ -640,29 +640,26 @@
 
 
 text {* Associative law for addition *}
-lemma add_assoc: "(m + n) + k = m + ((n + k)::nat)"
+lemma nat_add_assoc: "(m + n) + k = m + ((n + k)::nat)"
   by (induct m) simp_all
 
 text {* Commutative law for addition *}
-lemma add_commute: "m + n = n + (m::nat)"
+lemma nat_add_commute: "m + n = n + (m::nat)"
   by (induct m) simp_all
 
-lemma add_left_commute: "x + (y + z) = y + ((x + z)::nat)"
+lemma nat_add_left_commute: "x + (y + z) = y + ((x + z)::nat)"
   apply (rule mk_left_commute [of "op +"])
-  apply (rule add_assoc)
-  apply (rule add_commute)
+  apply (rule nat_add_assoc)
+  apply (rule nat_add_commute)
   done
 
-text {* Addition is an AC-operator *}
-lemmas add_ac = add_assoc add_commute add_left_commute
-
 lemma add_left_cancel [simp]: "(k + m = k + n) = (m = (n::nat))"
   by (induct k) simp_all
 
 lemma add_right_cancel [simp]: "(m + k = n + k) = (m=(n::nat))"
   by (induct k) simp_all
 
-lemma add_left_cancel_le [simp]: "(k + m <= k + n) = (m<=(n::nat))"
+lemma add_left_cancel_le [simp]: "(k + m \<le> k + n) = (m\<le>(n::nat))"
   by (induct k) simp_all
 
 lemma add_left_cancel_less [simp]: "(k + m < k + n) = (m<(n::nat))"
@@ -684,24 +681,114 @@
 
 lemma add_eq_self_zero: "!!m::nat. m + n = m ==> n = 0"
   apply (drule add_0_right [THEN ssubst])
-  apply (simp add: add_assoc del: add_0_right)
+  apply (simp add: nat_add_assoc del: add_0_right)
   done
 
-subsection {* Additional theorems about "less than" *}
+subsection {* Monotonicity of Addition *}
+
+text {* strict, in 1st argument *}
+lemma add_less_mono1: "i < j ==> i + k < j + (k::nat)"
+  by (induct k) simp_all
 
-text {* Deleted @{text less_natE}; instead use @{text "less_imp_Suc_add RS exE"} *}
-lemma less_imp_Suc_add: "m < n ==> (EX k. n = Suc (m + k))"
+text {* strict, in both arguments *}
+lemma add_less_mono: "[|i < j; k < l|] ==> i + k < j + (l::nat)"
+  apply (rule add_less_mono1 [THEN less_trans], assumption+)
+  apply (induct_tac j, simp_all)
+  done
+
+text {* Deleted @{text less_natE}; use @{text "less_imp_Suc_add RS exE"} *}
+lemma less_imp_Suc_add: "m < n ==> (\<exists>k. n = Suc (m + k))"
   apply (induct n)
   apply (simp_all add: order_le_less)
   apply (blast elim!: less_SucE intro!: add_0_right [symmetric] add_Suc_right [symmetric])
   done
 
-lemma le_add2: "n <= ((m + n)::nat)"
+
+subsection {* Multiplication *}
+
+text {* right annihilation in product *}
+lemma mult_0_right [simp]: "(m::nat) * 0 = 0"
+  by (induct m) simp_all
+
+text {* right successor law for multiplication *}
+lemma mult_Suc_right [simp]: "m * Suc n = m + (m * n)"
+  by (induct m) (simp_all add: nat_add_left_commute)
+
+text {* Commutative law for multiplication *}
+lemma nat_mult_commute: "m * n = n * (m::nat)"
+  by (induct m) simp_all
+
+text {* addition distributes over multiplication *}
+lemma add_mult_distrib: "(m + n) * k = (m * k) + ((n * k)::nat)"
+  by (induct m) (simp_all add: nat_add_assoc nat_add_left_commute)
+
+lemma add_mult_distrib2: "k * (m + n) = (k * m) + ((k * n)::nat)"
+  by (induct m) (simp_all add: nat_add_assoc)
+
+text {* Associative law for multiplication *}
+lemma nat_mult_assoc: "(m * n) * k = m * ((n * k)::nat)"
+  by (induct m) (simp_all add: add_mult_distrib)
+
+lemma mult_is_0 [simp]: "((m::nat) * n = 0) = (m=0 | n=0)"
+  apply (induct_tac m)
+  apply (induct_tac [2] n, simp_all)
+  done
+
+text {* strict, in 1st argument; proof is by induction on @{text "k > 0"} *}
+lemma mult_less_mono2: "(i::nat) < j ==> 0 < k ==> k * i < k * j"
+  apply (erule_tac m1 = 0 in less_imp_Suc_add [THEN exE], simp)
+  apply (induct_tac x) 
+  apply (simp_all add: add_less_mono)
+  done
+
+text{*The Naturals Form an Ordered Semiring*}
+instance nat :: ordered_semiring
+proof
+  fix i j k :: nat
+  show "(i + j) + k = i + (j + k)" by (rule nat_add_assoc)
+  show "i + j = j + i" by (rule nat_add_commute)
+  show "0 + i = i" by simp
+  show "(i * j) * k = i * (j * k)" by (rule nat_mult_assoc)
+  show "i * j = j * i" by (rule nat_mult_commute)
+  show "1 * i = i" by simp
+  show "(i + j) * k = i * k + j * k" by (simp add: add_mult_distrib)
+  show "0 \<noteq> (1::nat)" by simp
+  show "i \<le> j ==> k + i \<le> k + j" by simp
+  show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: mult_less_mono2)
+qed
+
+lemma nat_mult_1: "(1::nat) * n = n"
+  by simp
+
+lemma nat_mult_1_right: "n * (1::nat) = n"
+  by simp
+
+
+subsection {* Additional theorems about "less than" *}
+
+text {* A [clumsy] way of lifting @{text "<"}
+  monotonicity to @{text "\<le>"} monotonicity *}
+lemma less_mono_imp_le_mono:
+  assumes lt_mono: "!!i j::nat. i < j ==> f i < f j"
+  and le: "i \<le> j" shows "f i \<le> ((f j)::nat)" using le
+  apply (simp add: order_le_less)
+  apply (blast intro!: lt_mono)
+  done
+
+text {* non-strict, in 1st argument *}
+lemma add_le_mono1: "i \<le> j ==> i + k \<le> j + (k::nat)"
+  by (rule add_right_mono)
+
+text {* non-strict, in both arguments *}
+lemma add_le_mono: "[| i \<le> j;  k \<le> l |] ==> i + k \<le> j + (l::nat)"
+  by (rule add_mono)
+
+lemma le_add2: "n \<le> ((m + n)::nat)"
   apply (induct m, simp_all)
   apply (erule le_SucI)
   done
 
-lemma le_add1: "n <= ((n + m)::nat)"
+lemma le_add1: "n \<le> ((n + m)::nat)"
   apply (simp add: add_ac)
   apply (rule le_add2)
   done
@@ -712,14 +799,14 @@
 lemma less_add_Suc2: "i < Suc (m + i)"
   by (rule le_less_trans, rule le_add2, rule lessI)
 
-lemma less_iff_Suc_add: "(m < n) = (EX k. n = Suc (m + k))"
+lemma less_iff_Suc_add: "(m < n) = (\<exists>k. n = Suc (m + k))"
   by (rules intro!: less_add_Suc1 less_imp_Suc_add)
 
 
-lemma trans_le_add1: "(i::nat) <= j ==> i <= j + m"
+lemma trans_le_add1: "(i::nat) \<le> j ==> i \<le> j + m"
   by (rule le_trans, assumption, rule le_add1)
 
-lemma trans_le_add2: "(i::nat) <= j ==> i <= m + j"
+lemma trans_le_add2: "(i::nat) \<le> j ==> i \<le> m + j"
   by (rule le_trans, assumption, rule le_add2)
 
 lemma trans_less_add1: "(i::nat) < j ==> i < j + m"
@@ -741,15 +828,15 @@
 lemma not_add_less2 [iff]: "~ (j + i < (i::nat))"
   by (simp add: add_commute not_add_less1)
 
-lemma add_leD1: "m + k <= n ==> m <= (n::nat)"
+lemma add_leD1: "m + k \<le> n ==> m \<le> (n::nat)"
   by (induct k) (simp_all add: le_simps)
 
-lemma add_leD2: "m + k <= n ==> k <= (n::nat)"
+lemma add_leD2: "m + k \<le> n ==> k \<le> (n::nat)"
   apply (simp add: add_commute)
   apply (erule add_leD1)
   done
 
-lemma add_leE: "(m::nat) + k <= n ==> (m <= n ==> k <= n ==> R) ==> R"
+lemma add_leE: "(m::nat) + k \<le> n ==> (m \<le> n ==> k \<le> n ==> R) ==> R"
   by (blast dest: add_leD1 add_leD2)
 
 text {* needs @{text "!!k"} for @{text add_ac} to work *}
@@ -758,106 +845,6 @@
     simp add: less_iff_Suc_add add_Suc_right [symmetric] add_ac)
 
 
-subsection {* Monotonicity of Addition *}
-
-text {* strict, in 1st argument *}
-lemma add_less_mono1: "i < j ==> i + k < j + (k::nat)"
-  by (induct k) simp_all
-
-text {* strict, in both arguments *}
-lemma add_less_mono: "[|i < j; k < l|] ==> i + k < j + (l::nat)"
-  apply (rule add_less_mono1 [THEN less_trans], assumption+)
-  apply (induct_tac j, simp_all)
-  done
-
-text {* A [clumsy] way of lifting @{text "<"}
-  monotonicity to @{text "<="} monotonicity *}
-lemma less_mono_imp_le_mono:
-  assumes lt_mono: "!!i j::nat. i < j ==> f i < f j"
-  and le: "i <= j" shows "f i <= ((f j)::nat)" using le
-  apply (simp add: order_le_less)
-  apply (blast intro!: lt_mono)
-  done
-
-text {* non-strict, in 1st argument *}
-lemma add_le_mono1: "i <= j ==> i + k <= j + (k::nat)"
-  apply (rule_tac f = "%j. j + k" in less_mono_imp_le_mono)
-  apply (erule add_less_mono1, assumption)
-  done
-
-text {* non-strict, in both arguments *}
-lemma add_le_mono: "[| i <= j;  k <= l |] ==> i + k <= j + (l::nat)"
-  apply (erule add_le_mono1 [THEN le_trans])
-  apply (simp add: add_commute)
-  done
-
-
-subsection {* Multiplication *}
-
-text {* right annihilation in product *}
-lemma mult_0_right [simp]: "(m::nat) * 0 = 0"
-  by (induct m) simp_all
-
-text {* right successor law for multiplication *}
-lemma mult_Suc_right [simp]: "m * Suc n = m + (m * n)"
-  by (induct m) (simp_all add: add_ac)
-
-lemma mult_1: "(1::nat) * n = n" by simp
-
-lemma mult_1_right: "n * (1::nat) = n" by simp
-
-text {* Commutative law for multiplication *}
-lemma mult_commute: "m * n = n * (m::nat)"
-  by (induct m) simp_all
-
-text {* addition distributes over multiplication *}
-lemma add_mult_distrib: "(m + n) * k = (m * k) + ((n * k)::nat)"
-  by (induct m) (simp_all add: add_ac)
-
-lemma add_mult_distrib2: "k * (m + n) = (k * m) + ((k * n)::nat)"
-  by (induct m) (simp_all add: add_ac)
-
-text {* Associative law for multiplication *}
-lemma mult_assoc: "(m * n) * k = m * ((n * k)::nat)"
-  by (induct m) (simp_all add: add_mult_distrib)
-
-lemma mult_left_commute: "x * (y * z) = y * ((x * z)::nat)"
-  apply (rule mk_left_commute [of "op *"])
-  apply (rule mult_assoc)
-  apply (rule mult_commute)
-  done
-
-lemmas mult_ac = mult_assoc mult_commute mult_left_commute
-
-lemma mult_is_0 [simp]: "((m::nat) * n = 0) = (m=0 | n=0)"
-  apply (induct_tac m)
-  apply (induct_tac [2] n, simp_all)
-  done
-
-text {* strict, in 1st argument; proof is by induction on @{text "k > 0"} *}
-lemma mult_less_mono2: "(i::nat) < j ==> 0 < k ==> k * i < k * j"
-  apply (erule_tac m1 = 0 in less_imp_Suc_add [THEN exE], simp)
-  apply (induct_tac x)
-  apply (simp_all add: add_less_mono)
-  done
-
-text{*The Naturals Form an Ordered Semiring*}
-instance nat :: ordered_semiring
-proof
-  fix i j k :: nat
-  show "(i + j) + k = i + (j + k)" by (rule add_assoc)
-  show "i + j = j + i" by (rule add_commute)
-  show "0 + i = i" by simp
-  show "(i * j) * k = i * (j * k)" by (rule mult_assoc)
-  show "i * j = j * i" by (rule mult_commute)
-  show "1 * i = i" by simp
-  show "(i + j) * k = i * k + j * k" by (simp add: add_mult_distrib)
-  show "0 \<noteq> (1::nat)" by simp
-  show "i \<le> j ==> k + i \<le> k + j" by simp
-  show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: mult_less_mono2)
-qed
-
-
 
 subsection {* Difference *}
 
@@ -865,20 +852,20 @@
   by (induct m) simp_all
 
 text {* Addition is the inverse of subtraction:
-  if @{term "n <= m"} then @{term "n + (m - n) = m"}. *}
+  if @{term "n \<le> m"} then @{term "n + (m - n) = m"}. *}
 lemma add_diff_inverse: "~  m < n ==> n + (m - n) = (m::nat)"
   by (induct m n rule: diff_induct) simp_all
 
-lemma le_add_diff_inverse [simp]: "n <= m ==> n + (m - n) = (m::nat)"
+lemma le_add_diff_inverse [simp]: "n \<le> m ==> n + (m - n) = (m::nat)"
   by (simp add: add_diff_inverse not_less_iff_le)
 
-lemma le_add_diff_inverse2 [simp]: "n <= m ==> (m - n) + n = (m::nat)"
+lemma le_add_diff_inverse2 [simp]: "n \<le> m ==> (m - n) + n = (m::nat)"
   by (simp add: le_add_diff_inverse add_commute)
 
 
 subsection {* More results about difference *}
 
-lemma Suc_diff_le: "n <= m ==> Suc m - n = Suc (m - n)"
+lemma Suc_diff_le: "n \<le> m ==> Suc m - n = Suc (m - n)"
   by (induct m n rule: diff_induct) simp_all
 
 lemma diff_less_Suc: "m - n < Suc m"
@@ -887,7 +874,7 @@
   apply (simp_all add: less_Suc_eq)
   done
 
-lemma diff_le_self [simp]: "m - n <= (m::nat)"
+lemma diff_le_self [simp]: "m - n \<le> (m::nat)"
   by (induct m n rule: diff_induct) (simp_all add: le_SucI)
 
 lemma less_imp_diff_less: "(j::nat) < k ==> j - n < k"
@@ -908,10 +895,10 @@
 lemma diff_commute: "(i::nat) - j - k = i - k - j"
   by (simp add: diff_diff_left add_commute)
 
-lemma diff_add_assoc: "k <= (j::nat) ==> (i + j) - k = i + (j - k)"
+lemma diff_add_assoc: "k \<le> (j::nat) ==> (i + j) - k = i + (j - k)"
   by (induct j k rule: diff_induct) simp_all
 
-lemma diff_add_assoc2: "k <= (j::nat) ==> (j + i) - k = (j - k) + i"
+lemma diff_add_assoc2: "k \<le> (j::nat) ==> (j + i) - k = (j - k) + i"
   by (simp add: add_commute diff_add_assoc)
 
 lemma diff_add_inverse: "(n + m) - n = (m::nat)"
@@ -920,21 +907,21 @@
 lemma diff_add_inverse2: "(m + n) - n = (m::nat)"
   by (simp add: diff_add_assoc)
 
-lemma le_imp_diff_is_add: "i <= (j::nat) ==> (j - i = k) = (j = k + i)"
+lemma le_imp_diff_is_add: "i \<le> (j::nat) ==> (j - i = k) = (j = k + i)"
   apply safe
   apply (simp_all add: diff_add_inverse2)
   done
 
-lemma diff_is_0_eq [simp]: "((m::nat) - n = 0) = (m <= n)"
+lemma diff_is_0_eq [simp]: "((m::nat) - n = 0) = (m \<le> n)"
   by (induct m n rule: diff_induct) simp_all
 
-lemma diff_is_0_eq' [simp]: "m <= n ==> (m::nat) - n = 0"
+lemma diff_is_0_eq' [simp]: "m \<le> n ==> (m::nat) - n = 0"
   by (rule iffD2, rule diff_is_0_eq)
 
 lemma zero_less_diff [simp]: "(0 < n - (m::nat)) = (m < n)"
   by (induct m n rule: diff_induct) simp_all
 
-lemma less_imp_add_positive: "i < j  ==> EX k::nat. 0 < k & i + k = j"
+lemma less_imp_add_positive: "i < j  ==> \<exists>k::nat. 0 < k & i + k = j"
   apply (rule_tac x = "j - i" in exI)
   apply (simp (no_asm_simp) add: add_diff_inverse less_not_sym)
   done
@@ -975,16 +962,16 @@
 
 subsection {* Monotonicity of Multiplication *}
 
-lemma mult_le_mono1: "i <= (j::nat) ==> i * k <= j * k"
+lemma mult_le_mono1: "i \<le> (j::nat) ==> i * k \<le> j * k"
   by (induct k) (simp_all add: add_le_mono)
 
-lemma mult_le_mono2: "i <= (j::nat) ==> k * i <= k * j"
+lemma mult_le_mono2: "i \<le> (j::nat) ==> k * i \<le> k * j"
   apply (drule mult_le_mono1)
   apply (simp add: mult_commute)
   done
 
-text {* @{text "<="} monotonicity, BOTH arguments *}
-lemma mult_le_mono: "i <= (j::nat) ==> k <= l ==> i * k <= j * l"
+text {* @{text "\<le>"} monotonicity, BOTH arguments *}
+lemma mult_le_mono: "i \<le> (j::nat) ==> k \<le> l ==> i * k \<le> j * l"
   apply (erule mult_le_mono1 [THEN le_trans])
   apply (erule mult_le_mono2)
   done
@@ -999,7 +986,7 @@
   apply (case_tac [2] n, simp_all)
   done
 
-lemma one_le_mult_iff [simp]: "(Suc 0 <= m * n) = (1 <= m & 1 <= n)"
+lemma one_le_mult_iff [simp]: "(Suc 0 \<le> m * n) = (1 \<le> m & 1 \<le> n)"
   apply (induct m)
   apply (case_tac [2] n, simp_all)
   done
@@ -1026,10 +1013,10 @@
 
 declare mult_less_cancel2 [simp]
 
-lemma mult_le_cancel1 [simp]: "(k * (m::nat) <= k * n) = (0 < k --> m <= n)"
+lemma mult_le_cancel1 [simp]: "(k * (m::nat) \<le> k * n) = (0 < k --> m \<le> n)"
 by (simp add: linorder_not_less [symmetric], auto)
 
-lemma mult_le_cancel2 [simp]: "((m::nat) * k <= n * k) = (0 < k --> m <= n)"
+lemma mult_le_cancel2 [simp]: "((m::nat) * k \<le> n * k) = (0 < k --> m \<le> n)"
 by (simp add: linorder_not_less [symmetric], auto)
 
 lemma mult_cancel2: "(m * k = n * k) = (m = n | (k = (0::nat)))"
@@ -1045,7 +1032,7 @@
 lemma Suc_mult_less_cancel1: "(Suc k * m < Suc k * n) = (m < n)"
   by (subst mult_less_cancel1) simp
 
-lemma Suc_mult_le_cancel1: "(Suc k * m <= Suc k * n) = (m <= n)"
+lemma Suc_mult_le_cancel1: "(Suc k * m \<le> Suc k * n) = (m \<le> n)"
   by (subst mult_le_cancel1) simp
 
 lemma Suc_mult_cancel1: "(Suc k * m = Suc k * n) = (m = n)"
diff -r 08b34c902618 -r b963e9cee2a0 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Mon Nov 24 15:33:07 2003 +0100
+++ b/src/HOL/Ring_and_Field.thy	Tue Nov 25 10:37:03 2003 +0100
@@ -22,7 +22,7 @@
 
   mult_assoc: "(a * b) * c = a * (b * c)"
   mult_commute: "a * b = b * a"
-  left_one [simp]: "1 * a = a"
+  mult_1 [simp]: "1 * a = a"
 
   left_distrib: "(a + b) * c = a * c + b * c"
   zero_neq_one [simp]: "0 \<noteq> 1"
@@ -133,10 +133,10 @@
 
 subsection {* Derived rules for multiplication *}
 
-lemma right_one [simp]: "a = a * (1::'a::semiring)"
+lemma mult_1_right [simp]: "a * (1::'a::semiring) = a"
 proof -
-  have "a = 1 * a" by simp
-  also have "... = a * 1" by (simp add: mult_commute)
+  have "a * 1 = 1 * a" by (simp add: mult_commute)
+  also have "... = a" by simp
   finally show ?thesis .
 qed
 
@@ -217,6 +217,12 @@
 lemma add_right_mono: "a \<le> (b::'a::ordered_semiring) ==> a + c \<le> b + c"
 by (simp add: add_commute [of _ c] add_left_mono)
 
+text {* non-strict, in both arguments *}
+lemma add_mono: "[|a \<le> b;  c \<le> d|] ==> a + c \<le> b + (d::'a::ordered_semiring)"
+  apply (erule add_right_mono [THEN order_trans])
+  apply (simp add: add_commute add_left_mono)
+  done
+
 lemma le_imp_neg_le:
    assumes "a \<le> (b::'a::ordered_ring)" shows "-b \<le> -a"
   proof -
@@ -261,12 +267,14 @@
 by (simp add: mult_commute [of _ c] mult_strict_left_mono)
 
 lemma mult_left_mono:
-     "[|a \<le> b; 0 < c|] ==> c * a \<le> c * (b::'a::ordered_semiring)"
-by (force simp add: mult_strict_left_mono order_le_less) 
+     "[|a \<le> b; 0 \<le> c|] ==> c * a \<le> c * (b::'a::ordered_ring)"
+  apply (case_tac "c=0", simp)
+  apply (force simp add: mult_strict_left_mono order_le_less) 
+  done
 
 lemma mult_right_mono:
-     "[|a \<le> b; 0 < c|] ==> a*c \<le> b * (c::'a::ordered_semiring)"
-by (force simp add: mult_strict_right_mono order_le_less) 
+     "[|a \<le> b; 0 \<le> c|] ==> a*c \<le> b * (c::'a::ordered_ring)"
+  by (simp add: mult_left_mono mult_commute [of _ c]) 
 
 lemma mult_strict_left_mono_neg:
      "[|b < a; c < 0|] ==> c * a < c * (b::'a::ordered_ring)"
@@ -281,12 +289,14 @@
 done
 
 lemma mult_left_mono_neg:
-     "[|b \<le> a; c < 0|] ==> c * a \<le> c * (b::'a::ordered_ring)"
-by (force simp add: mult_strict_left_mono_neg order_le_less) 
+     "[|b \<le> a; c \<le> 0|] ==> c * a \<le> c * (b::'a::ordered_ring)"
+apply (drule mult_left_mono [of _ _ "-c"]) 
+apply (simp_all add: minus_mult_left [symmetric]) 
+done
 
 lemma mult_right_mono_neg:
-     "[|b \<le> a; c < 0|] ==> a * c \<le> b * (c::'a::ordered_ring)"
-by (force simp add: mult_strict_right_mono_neg order_le_less) 
+     "[|b \<le> a; c \<le> 0|] ==> a * c \<le> b * (c::'a::ordered_ring)"
+  by (simp add: mult_left_mono_neg mult_commute [of _ c]) 
 
 text{*Strict monotonicity in both arguments*}
 lemma mult_strict_mono:
@@ -295,6 +305,14 @@
 apply (erule mult_strict_left_mono, assumption)
 done
 
+lemma mult_mono:
+     "[|a \<le> b; c \<le> d; 0 \<le> b; 0 \<le> c|] 
+      ==> a * c  \<le>  b * (d::'a::ordered_ring)"
+apply (erule mult_right_mono [THEN order_trans], assumption)
+apply (erule mult_left_mono, assumption)
+done
+
+
 subsection{*Cancellation Laws for Relationships With a Common Factor*}
 
 text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},