# HG changeset patch
# User paulson
# Date 1073382015 -3600
# Node ID a09441bd4f1e7166552d583ca499863fd5a53818
# Parent  bc93ffa674cc5fcbc301cadcfdd60a03cff30b79
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
This allows more theorems to be proved for semirings, but
requires a redundant axiom to be proved for rings, etc.

diff -r bc93ffa674cc -r a09441bd4f1e src/HOL/Complex/Complex.thy
--- a/src/HOL/Complex/Complex.thy	Tue Jan 06 10:38:14 2004 +0100
+++ b/src/HOL/Complex/Complex.thy	Tue Jan 06 10:40:15 2004 +0100
@@ -343,20 +343,18 @@
 done
 declare complex_add_minus_right_zero [simp]
 
-lemma complex_add_minus_left_zero:
+lemma complex_add_minus_left:
       "-z + z = (0::complex)"
 apply (unfold complex_add_def complex_minus_def complex_zero_def)
 apply (simp (no_asm))
 done
-declare complex_add_minus_left_zero [simp]
 
 lemma complex_add_minus_cancel: "z + (- z + w) = (w::complex)"
 apply (simp (no_asm) add: complex_add_assoc [symmetric])
 done
 
 lemma complex_minus_add_cancel: "(-z) + (z + w) = (w::complex)"
-apply (simp (no_asm) add: complex_add_assoc [symmetric])
-done
+by (simp add: complex_add_minus_left complex_add_assoc [symmetric])
 
 declare complex_add_minus_cancel [simp] complex_minus_add_cancel [simp]
 
@@ -373,7 +371,7 @@
 lemma complex_add_left_cancel: "((x::complex) + y = x + z) = (y = z)"
 apply safe
 apply (drule_tac f = "%t.-x + t" in arg_cong)
-apply (simp add: complex_add_assoc [symmetric])
+apply (simp add: complex_add_minus_left complex_add_assoc [symmetric])
 done
 declare complex_add_left_cancel [iff]
 
@@ -413,7 +411,7 @@
 done
 
 lemma complex_diff_eq_eq: "((x::complex) - y = z) = (x = z + y)"
-by (auto simp add: complex_diff_def complex_add_assoc)
+by (auto simp add: complex_add_minus_left complex_diff_def complex_add_assoc)
 
 
 subsection{*Multiplication*}
@@ -552,7 +550,7 @@
   show "0 + z = z"
     by (rule complex_add_zero_left) 
   show "-z + z = 0"
-    by (rule complex_add_minus_left_zero) 
+    by (rule complex_add_minus_left) 
   show "z - w = z + -w"
     by (simp add: complex_diff_def)
   show "(u * v) * w = u * (v * w)"
@@ -561,10 +559,16 @@
     by (rule complex_mult_commute) 
   show "1 * z = z"
     by (rule complex_mult_one_left) 
-  show "0 \<noteq> (1::complex)"  --{*for some reason it has to be early*}
+  show "0 \<noteq> (1::complex)"
     by (rule complex_zero_not_eq_one) 
   show "(u + v) * w = u * w + v * w"
     by (rule complex_add_mult_distrib) 
+  show "z+u = z+v ==> u=v"
+    proof -
+      assume eq: "z+u = z+v" 
+      hence "(-z + z) + u = (-z + z) + v" by (simp only: eq complex_add_assoc)
+      thus "u = v" by (simp add: complex_add_minus_left)
+    qed
   assume neq: "w \<noteq> 0"
   thus "z / w = z * inverse w"
     by (simp add: complex_divide_def)
@@ -1700,7 +1704,6 @@
 val complex_add_zero_left = thm"complex_add_zero_left";
 val complex_add_zero_right = thm"complex_add_zero_right";
 val complex_add_minus_right_zero = thm"complex_add_minus_right_zero";
-val complex_add_minus_left_zero = thm"complex_add_minus_left_zero";
 val complex_add_minus_cancel = thm"complex_add_minus_cancel";
 val complex_minus_add_cancel = thm"complex_minus_add_cancel";
 val complex_add_minus_eq_minus = thm"complex_add_minus_eq_minus";
diff -r bc93ffa674cc -r a09441bd4f1e src/HOL/Complex/NSComplex.thy
--- a/src/HOL/Complex/NSComplex.thy	Tue Jan 06 10:38:14 2004 +0100
+++ b/src/HOL/Complex/NSComplex.thy	Tue Jan 06 10:40:15 2004 +0100
@@ -481,6 +481,13 @@
     by (rule hcomplex_zero_not_eq_one)
   show "(u + v) * w = u * w + v * w"
     by (simp add: hcomplex_add_mult_distrib)
+  show "z+u = z+v ==> u=v"
+    proof -
+      assume eq: "z+u = z+v" 
+      hence "(-z + z) + u = (-z + z) + v" by (simp only: eq hcomplex_add_assoc)
+      thus "u = v" 
+        by (simp only: hcomplex_add_minus_left hcomplex_add_zero_left)
+    qed
   assume neq: "w \<noteq> 0"
   thus "z / w = z * inverse w"
     by (simp add: hcomplex_divide_def)
diff -r bc93ffa674cc -r a09441bd4f1e src/HOL/Hyperreal/HyperDef.thy
--- a/src/HOL/Hyperreal/HyperDef.thy	Tue Jan 06 10:38:14 2004 +0100
+++ b/src/HOL/Hyperreal/HyperDef.thy	Tue Jan 06 10:40:15 2004 +0100
@@ -474,6 +474,9 @@
   show "0 \<noteq> (1::hypreal)" by (rule hypreal_zero_not_eq_one)
   show "x \<noteq> 0 ==> inverse x * x = 1" by (simp add: hypreal_mult_inverse_left)
   show "y \<noteq> 0 ==> x / y = x * inverse y" by (simp add: hypreal_divide_def)
+  assume eq: "z+x = z+y" 
+    hence "(-z + z) + x = (-z + z) + y" by (simp only: eq hypreal_add_assoc)
+    thus "x = y" by (simp add: hypreal_add_minus_left)
 qed
 
 
diff -r bc93ffa674cc -r a09441bd4f1e src/HOL/Integ/Int.thy
--- a/src/HOL/Integ/Int.thy	Tue Jan 06 10:38:14 2004 +0100
+++ b/src/HOL/Integ/Int.thy	Tue Jan 06 10:40:15 2004 +0100
@@ -47,12 +47,6 @@
 lemma not_iszero_1: "~ iszero 1"
 by (simp only: Zero_int_def One_int_def One_nat_def iszero_def int_int_eq)
 
-lemma int_0_less_1: "0 < (1::int)"
-by (simp only: Zero_int_def One_int_def One_nat_def zless_int)
-
-lemma int_0_neq_1 [simp]: "0 \<noteq> (1::int)"
-by (simp only: Zero_int_def One_int_def One_nat_def int_int_eq)
-
 
 subsection{*nat: magnitide of an integer, as a natural number*}
 
@@ -154,16 +148,6 @@
 instance int :: ordered_ring
 proof
   fix i j k :: int
-  show "(i + j) + k = i + (j + k)" by (simp add: zadd_assoc)
-  show "i + j = j + i" by (simp add: zadd_commute)
-  show "0 + i = i" by simp
-  show "- i + i = 0" by simp
-  show "i - j = i + (-j)" by (simp add: zdiff_def)
-  show "(i * j) * k = i * (j * k)" by (rule zmult_assoc)
-  show "i * j = j * i" by (rule zmult_commute)
-  show "1 * i = i" by simp
-  show "(i + j) * k = i * k + j * k" by (simp add: int_distrib)
-  show "0 \<noteq> (1::int)" 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: zmult_zless_mono2)
   show "\<bar>i\<bar> = (if i < 0 then -i else i)" by (simp only: zabs_def)
diff -r bc93ffa674cc -r a09441bd4f1e src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Tue Jan 06 10:38:14 2004 +0100
+++ b/src/HOL/Integ/IntDef.thy	Tue Jan 06 10:40:15 2004 +0100
@@ -96,6 +96,10 @@
 apply (simp add: intrel_def)
 done
 
+lemma int_int_eq [iff]: "(int m = int n) = (m = n)"
+by (fast elim!: inj_int [THEN injD])
+
+
 
 subsection{*zminus: unary negation on Integ*}
 
@@ -327,7 +331,27 @@
 by (rule trans [OF zmult_commute zmult_1])
 
 
-(* Theorems about less and less_equal *)
+text{*The Integers Form A Ring*}
+instance int :: ring
+proof
+  fix i j k :: int
+  show "(i + j) + k = i + (j + k)" by (simp add: zadd_assoc)
+  show "i + j = j + i" by (simp add: zadd_commute)
+  show "0 + i = i" by simp
+  show "- i + i = 0" by simp
+  show "i - j = i + (-j)" by (simp add: zdiff_def)
+  show "(i * j) * k = i * (j * k)" by (rule zmult_assoc)
+  show "i * j = j * i" by (rule zmult_commute)
+  show "1 * i = i" by simp
+  show "(i + j) * k = i * k + j * k" by (simp add: int_distrib)
+  show "0 \<noteq> (1::int)" by (simp only: Zero_int_def One_int_def One_nat_def int_int_eq)
+  assume eq: "k+i = k+j" 
+    hence "(-k + k) + i = (-k + k) + j" by (simp only: eq zadd_assoc)
+    thus "i = j" by simp
+qed
+
+
+subsection{*Theorems about the Ordering*}
 
 (*This lemma allows direct proofs of other <-properties*)
 lemma zless_iff_Suc_zadd: 
@@ -382,9 +406,6 @@
 (*** eliminates ~= in premises ***)
 lemmas int_neqE = int_neq_iff [THEN iffD1, THEN disjE, standard]
 
-lemma int_int_eq [iff]: "(int m = int n) = (m = n)"
-by (fast elim!: inj_int [THEN injD])
-
 lemma int_eq_0_conv [simp]: "(int n = 0) = (n = 0)"
 by (simp add: Zero_int_def)
 
@@ -397,8 +418,14 @@
 lemma zero_less_int_conv [simp]: "(0 < int n) = (0 < n)"
 by (simp add: Zero_int_def)
 
+lemma int_0_less_1: "0 < (1::int)"
+by (simp only: Zero_int_def One_int_def One_nat_def zless_int)
 
-(*** Properties of <= ***)
+lemma int_0_neq_1 [simp]: "0 \<noteq> (1::int)"
+by (simp only: Zero_int_def One_int_def One_nat_def int_int_eq)
+
+
+subsection{*Properties of the @{text "\<le>"} Relation*}
 
 lemma zle_int [simp]: "(int m <= int n) = (m<=n)"
 by (simp add: zle_def le_def)
@@ -456,12 +483,6 @@
 apply (blast elim!: zless_asym)
 done
 
-lemma zadd_left_cancel [simp]: "!!w::int. (z + w' = z + w) = (w' = w)"
-apply safe
-apply (drule_tac f = "%x. x + (-z) " in arg_cong)
-apply (simp add: Zero_int_def [symmetric] zadd_ac)
-done
-
 instance int :: order
 proof qed (assumption | rule zle_refl zle_trans zle_anti_sym int_less_le)+
 
@@ -472,6 +493,10 @@
 proof qed (rule zle_linear)
 
 
+lemma zadd_left_cancel [simp]: "!!w::int. (z + w' = z + w) = (w' = w)"
+  by (rule add_left_cancel) 
+
+
 ML
 {*
 val int_def = thm "int_def";
@@ -564,14 +589,6 @@
 val zle_anti_sym = thm "zle_anti_sym";
 val int_less_le = thm "int_less_le";
 val zadd_left_cancel = thm "zadd_left_cancel";
-
-val diff_less_eq = thm"diff_less_eq";
-val less_diff_eq = thm"less_diff_eq";
-val eq_diff_eq = thm"eq_diff_eq";
-val diff_eq_eq = thm"diff_eq_eq";
-val diff_le_eq = thm"diff_le_eq";
-val le_diff_eq = thm"le_diff_eq";
-val compare_rls = thms "compare_rls";
 *}
 
 end
diff -r bc93ffa674cc -r a09441bd4f1e src/HOL/Library/Rational_Numbers.thy
--- a/src/HOL/Library/Rational_Numbers.thy	Tue Jan 06 10:38:14 2004 +0100
+++ b/src/HOL/Library/Rational_Numbers.thy	Tue Jan 06 10:40:15 2004 +0100
@@ -475,17 +475,28 @@
 
 subsubsection {* The ordered field of rational numbers *}
 
+lemma rat_add_assoc: "(q + r) + s = q + (r + (s::rat))"
+  by (induct q, induct r, induct s) 
+     (simp add: add_rat zadd_ac zmult_ac int_distrib)
+
+lemma rat_add_0: "0 + q = (q::rat)"
+  by (induct q) (simp add: zero_rat add_rat)
+
+lemma rat_left_minus: "(-q) + q = (0::rat)"
+  by (induct q) (simp add: zero_rat minus_rat add_rat eq_rat)
+
+
 instance rat :: field
 proof
   fix q r s :: rat
   show "(q + r) + s = q + (r + s)"
-    by (induct q, induct r, induct s) (simp add: add_rat zadd_ac zmult_ac int_distrib)
+    by (rule rat_add_assoc)
   show "q + r = r + q"
     by (induct q, induct r) (simp add: add_rat zadd_ac zmult_ac)
   show "0 + q = q"
     by (induct q) (simp add: zero_rat add_rat)
   show "(-q) + q = 0"
-    by (induct q) (simp add: zero_rat minus_rat add_rat eq_rat)
+    by (rule rat_left_minus)
   show "q - r = q + (-r)"
     by (induct q, induct r) (simp add: add_rat minus_rat diff_rat)
   show "(q * r) * s = q * (r * s)"
@@ -495,14 +506,19 @@
   show "1 * q = q"
     by (induct q) (simp add: one_rat mult_rat)
   show "(q + r) * s = q * s + r * s"
-    by (induct q, induct r, induct s) (simp add: add_rat mult_rat eq_rat int_distrib)
+    by (induct q, induct r, induct s) 
+       (simp add: add_rat mult_rat eq_rat int_distrib)
   show "q \<noteq> 0 ==> inverse q * q = 1"
     by (induct q) (simp add: inverse_rat mult_rat one_rat zero_rat eq_rat)
   show "r \<noteq> 0 ==> q / r = q * inverse r"
-    by (induct q, induct r) (simp add: mult_rat divide_rat inverse_rat zero_rat eq_rat)
+    by (induct q, induct r)
+       (simp add: mult_rat divide_rat inverse_rat zero_rat eq_rat)
   show "0 \<noteq> (1::rat)"
     by (simp add: zero_rat_def one_rat_def rat_of_equality 
                   zero_fraction_def one_fraction_def) 
+  assume eq: "s+q = s+r" 
+    hence "(-s + s) + q = (-s + s) + r" by (simp only: eq rat_add_assoc)
+    thus "q = r" by (simp add: rat_left_minus rat_add_0)
 qed
 
 instance rat :: linorder
diff -r bc93ffa674cc -r a09441bd4f1e src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Tue Jan 06 10:38:14 2004 +0100
+++ b/src/HOL/Nat.thy	Tue Jan 06 10:40:15 2004 +0100
@@ -460,6 +460,14 @@
   apply blast
   done
 
+text {* Type {@typ nat} is a wellfounded linear order *}
+
+instance nat :: order by (intro_classes,
+  (assumption | rule le_refl le_trans le_anti_sym nat_less_le)+)
+instance nat :: linorder by (intro_classes, rule nat_le_linear)
+instance nat :: wellorder by (intro_classes, rule wf_less)
+
+
 lemma not_less_less_Suc_eq: "~ n < m ==> (n < Suc m) = (n = m)"
   by (blast elim!: less_SucE)
 
@@ -488,13 +496,6 @@
 lemma one_reorient: "(1 = x) = (x = 1)"
   by auto
 
-text {* Type {@typ nat} is a wellfounded linear order *}
-
-instance nat :: order by (intro_classes,
-  (assumption | rule le_refl le_trans le_anti_sym nat_less_le)+)
-instance nat :: linorder by (intro_classes, rule nat_le_linear)
-instance nat :: wellorder by (intro_classes, rule wf_less)
-
 subsection {* Arithmetic operators *}
 
 axclass power < type
@@ -525,7 +526,8 @@
   mult_0:   "0 * n = 0"
   mult_Suc: "Suc m * n = n + (m * n)"
 
-text {* These 2 rules ease the use of primitive recursion. NOTE USE OF @{text "=="} *}
+text {* These two rules ease the use of primitive recursion. 
+NOTE USE OF @{text "=="} *}
 lemma def_nat_rec_0: "(!!n. f n == nat_rec c h n) ==> f 0 = c"
   by simp
 
@@ -560,7 +562,7 @@
 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"
+lemma nat_induct2: "[|P 0; P (Suc 0); !!k. P k ==> P (Suc (Suc k))|] ==> P n"
   apply (rule nat_less_induct)
   apply (case_tac n)
   apply (case_tac [2] nat)
@@ -690,25 +692,6 @@
   apply (simp add: nat_add_assoc del: add_0_right)
   done
 
-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 {* 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
-
 
 subsection {* Multiplication *}
 
@@ -735,20 +718,9 @@
 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
+text{*The Naturals Form A Semiring*}
+instance nat :: semiring
 proof
   fix i j k :: nat
   show "(i + j) + k = i + (j + k)" by (rule nat_add_assoc)
@@ -759,6 +731,46 @@
   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
+  assume "k+i = k+j" thus "i=j" by simp
+qed
+
+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
+
+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 {* 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
+
+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 \<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
@@ -790,14 +802,10 @@
   by (rule add_mono)
 
 lemma le_add2: "n \<le> ((m + n)::nat)"
-  apply (induct m, simp_all)
-  apply (erule le_SucI)
-  done
+  by (insert add_right_mono [of 0 m n], simp) 
 
 lemma le_add1: "n \<le> ((n + m)::nat)"
-  apply (simp add: add_ac)
-  apply (rule le_add2)
-  done
+  by (simp add: add_commute, rule le_add2)
 
 lemma less_add_Suc1: "i < Suc (i + m)"
   by (rule le_less_trans, rule le_add1, rule lessI)
@@ -808,7 +816,6 @@
 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) \<le> j ==> i \<le> j + m"
   by (rule le_trans, assumption, rule le_add1)
 
@@ -822,8 +829,8 @@
   by (rule less_le_trans, assumption, rule le_add2)
 
 lemma add_lessD1: "i + j < (k::nat) ==> i < k"
-  apply (induct j, simp_all)
-  apply (blast dest: Suc_lessD)
+  apply (rule le_less_trans [of _ "i+j"]) 
+  apply (simp_all add: le_add1)
   done
 
 lemma not_add_less1 [iff]: "~ (i + j < (i::nat))"
@@ -835,7 +842,9 @@
   by (simp add: add_commute not_add_less1)
 
 lemma add_leD1: "m + k \<le> n ==> m \<le> (n::nat)"
-  by (induct k) (simp_all add: le_simps)
+  apply (rule order_trans [of _ "m+k"]) 
+  apply (simp_all add: le_add1)
+  done
 
 lemma add_leD2: "m + k \<le> n ==> k \<le> (n::nat)"
   apply (simp add: add_commute)
@@ -969,21 +978,17 @@
 subsection {* Monotonicity of Multiplication *}
 
 lemma mult_le_mono1: "i \<le> (j::nat) ==> i * k \<le> j * k"
-  by (induct k) (simp_all add: add_le_mono)
+  by (simp add: mult_right_mono) 
 
 lemma mult_le_mono2: "i \<le> (j::nat) ==> k * i \<le> k * j"
-  apply (drule mult_le_mono1)
-  apply (simp add: mult_commute)
-  done
+  by (simp add: mult_left_mono) 
 
 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
+  by (simp add: mult_mono) 
 
 lemma mult_less_mono1: "(i::nat) < j ==> 0 < k ==> i * k < j * k"
-  by (drule mult_less_mono2) (simp_all add: mult_commute)
+  by (simp add: mult_strict_right_mono) 
 
 text{*Differs from the standard @{text zero_less_mult_iff} in that
       there are no negative numbers.*}
@@ -1007,7 +1012,7 @@
   apply (rule_tac [2] mult_eq_1_iff, fastsimp)
   done
 
-lemma mult_less_cancel2: "((m::nat) * k < n * k) = (0 < k & m < n)"
+lemma mult_less_cancel2 [simp]: "((m::nat) * k < n * k) = (0 < k & m < n)"
   apply (safe intro!: mult_less_mono1)
   apply (case_tac k, auto)
   apply (simp del: le_0_eq add: linorder_not_le [symmetric])
@@ -1015,9 +1020,7 @@
   done
 
 lemma mult_less_cancel1 [simp]: "(k * (m::nat) < k * n) = (0 < k & m < n)"
-  by (simp add: mult_less_cancel2 mult_commute [of k])
-
-declare mult_less_cancel2 [simp]
+  by (simp add: mult_commute [of k])
 
 lemma mult_le_cancel1 [simp]: "(k * (m::nat) \<le> k * n) = (0 < k --> m \<le> n)"
 by (simp add: linorder_not_less [symmetric], auto)
@@ -1025,15 +1028,13 @@
 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)))"
+lemma mult_cancel2 [simp]: "(m * k = n * k) = (m = n | (k = (0::nat)))"
   apply (cut_tac less_linear, safe, auto)
   apply (drule mult_less_mono1, assumption, simp)+
   done
 
 lemma mult_cancel1 [simp]: "(k * m = k * n) = (m = n | (k = (0::nat)))"
-  by (simp add: mult_cancel2 mult_commute [of k])
-
-declare mult_cancel2 [simp]
+  by (simp add: mult_commute [of k])
 
 lemma Suc_mult_less_cancel1: "(Suc k * m < Suc k * n) = (m < n)"
   by (subst mult_less_cancel1) simp
@@ -1044,7 +1045,6 @@
 lemma Suc_mult_cancel1: "(Suc k * m = Suc k * n) = (m = n)"
   by (subst mult_cancel1) simp
 
-
 text {* Lemma for @{text gcd} *}
 lemma mult_eq_self_implies_10: "(m::nat) = m * n ==> n = 1 | m = 0"
   apply (drule sym)
@@ -1054,5 +1054,4 @@
   apply (fastsimp dest: mult_less_mono2)
   done
 
-
 end
diff -r bc93ffa674cc -r a09441bd4f1e src/HOL/Real/Complex_Numbers.thy
--- a/src/HOL/Real/Complex_Numbers.thy	Tue Jan 06 10:38:14 2004 +0100
+++ b/src/HOL/Real/Complex_Numbers.thy	Tue Jan 06 10:40:15 2004 +0100
@@ -107,6 +107,12 @@
     by (simp add: zero_complex_def one_complex_def) 
   show "(u + v) * w = u * w + v * w"
     by (simp add: add_complex_def mult_complex_def ring_distrib)
+  show "z+u = z+v ==> u=v"
+    proof -
+      assume eq: "z+u = z+v" 
+      hence "(-z + z) + u = (-z + z) + v" by (simp add: eq add_complex_def)
+      thus "u = v" by (simp add: add_complex_def)
+    qed
   assume neq: "w \<noteq> 0"
   thus "z / w = z * inverse w"
     by (simp add: divide_complex_def)
diff -r bc93ffa674cc -r a09441bd4f1e src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Tue Jan 06 10:38:14 2004 +0100
+++ b/src/HOL/Real/RealDef.thy	Tue Jan 06 10:40:15 2004 +0100
@@ -330,6 +330,9 @@
 apply (rule someI2, auto)
 done
 
+
+subsection{*The Real Numbers form a Field*}
+
 instance real :: field
 proof
   fix x y z :: real
@@ -345,10 +348,13 @@
   show "0 \<noteq> (1::real)" by (rule real_zero_not_eq_one)
   show "x \<noteq> 0 ==> inverse x * x = 1" by (rule real_mult_inv_left)
   show "y \<noteq> 0 ==> x / y = x * inverse y" by (simp add: real_divide_def)
+  assume eq: "z+x = z+y" 
+    hence "(-z + z) + x = (-z + z) + y" by (simp only: eq real_add_assoc)
+    thus "x = y" by (simp add: real_add_minus_left)
 qed
 
 
-(** Inverse of zero!  Useful to simplify certain equations **)
+text{*Inverse of zero!  Useful to simplify certain equations*}
 
 lemma INVERSE_ZERO: "inverse 0 = (0::real)"
 apply (unfold real_inverse_def)
@@ -652,33 +658,6 @@
 done
 declare real_minus_zero_less_iff2 [simp]
 
-ML
-{*
-val real_le_def = thm "real_le_def";
-val real_diff_def = thm "real_diff_def";
-val real_divide_def = thm "real_divide_def";
-val real_of_nat_def = thm "real_of_nat_def";
-
-val preal_trans_lemma = thm"preal_trans_lemma";
-val realrel_iff = thm"realrel_iff";
-val realrel_refl = thm"realrel_refl";
-val equiv_realrel = thm"equiv_realrel";
-val equiv_realrel_iff = thm"equiv_realrel_iff";
-val realrel_in_real = thm"realrel_in_real";
-val inj_on_Abs_REAL = thm"inj_on_Abs_REAL";
-val eq_realrelD = thm"eq_realrelD";
-val inj_Rep_REAL = thm"inj_Rep_REAL";
-val inj_real_of_preal = thm"inj_real_of_preal";
-val eq_Abs_REAL = thm"eq_Abs_REAL";
-val real_minus_congruent = thm"real_minus_congruent";
-val real_minus = thm"real_minus";
-val real_add = thm"real_add";
-val real_add_commute = thm"real_add_commute";
-val real_add_assoc = thm"real_add_assoc";
-val real_add_zero_left = thm"real_add_zero_left";
-val real_add_zero_right = thm"real_add_zero_right";
-
-*}
 
 subsection{*Properties of Less-Than Or Equals*}
 
@@ -1068,6 +1047,30 @@
 {*
 val real_abs_def = thm "real_abs_def";
 
+val real_le_def = thm "real_le_def";
+val real_diff_def = thm "real_diff_def";
+val real_divide_def = thm "real_divide_def";
+val real_of_nat_def = thm "real_of_nat_def";
+
+val preal_trans_lemma = thm"preal_trans_lemma";
+val realrel_iff = thm"realrel_iff";
+val realrel_refl = thm"realrel_refl";
+val equiv_realrel = thm"equiv_realrel";
+val equiv_realrel_iff = thm"equiv_realrel_iff";
+val realrel_in_real = thm"realrel_in_real";
+val inj_on_Abs_REAL = thm"inj_on_Abs_REAL";
+val eq_realrelD = thm"eq_realrelD";
+val inj_Rep_REAL = thm"inj_Rep_REAL";
+val inj_real_of_preal = thm"inj_real_of_preal";
+val eq_Abs_REAL = thm"eq_Abs_REAL";
+val real_minus_congruent = thm"real_minus_congruent";
+val real_minus = thm"real_minus";
+val real_add = thm"real_add";
+val real_add_commute = thm"real_add_commute";
+val real_add_assoc = thm"real_add_assoc";
+val real_add_zero_left = thm"real_add_zero_left";
+val real_add_zero_right = thm"real_add_zero_right";
+
 val real_less_eq_diff = thm "real_less_eq_diff";
 
 val real_mult = thm"real_mult";
diff -r bc93ffa674cc -r a09441bd4f1e src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Tue Jan 06 10:38:14 2004 +0100
+++ b/src/HOL/Ring_and_Field.thy	Tue Jan 06 10:40:15 2004 +0100
@@ -20,6 +20,11 @@
   add_assoc: "(a + b) + c = a + (b + c)"
   add_commute: "a + b = b + a"
   add_0 [simp]: "0 + a = a"
+  add_left_imp_eq: "a + b = a + c ==> b=c"
+    --{*This axiom is needed for semirings only: for rings, etc., it is
+        redundant. Including it allows many more of the following results
+        to be proved for semirings too. The drawback is that this redundant
+        axiom must be proved for instances of rings.*}
 
   mult_assoc: "(a * b) * c = a * (b * c)"
   mult_commute: "a * b = b * a"
@@ -82,19 +87,11 @@
 qed
 
 lemma add_left_cancel [simp]:
-     "(a + b = a + c) = (b = (c::'a::ring))"
-proof
-  assume eq: "a + b = a + c"
-  hence "(-a + a) + b = (-a + a) + c"
-    by (simp only: eq add_assoc)
-  thus "b = c" by simp
-next
-  assume eq: "b = c"
-  thus "a + b = a + c" by simp
-qed
+     "(a + b = a + c) = (b = (c::'a::semiring))"
+by (blast dest: add_left_imp_eq) 
 
 lemma add_right_cancel [simp]:
-     "(b + a = c + a) = (b = (c::'a::ring))"
+     "(b + a = c + a) = (b = (c::'a::semiring))"
   by (simp add: add_commute)
 
 lemma minus_minus [simp]: "- (- (a::'a::ring)) = a"
@@ -169,14 +166,14 @@
 
 theorems mult_ac = mult_assoc mult_commute mult_left_commute
 
-lemma mult_left_zero [simp]: "0 * a = (0::'a::ring)"
+lemma mult_left_zero [simp]: "0 * a = (0::'a::semiring)"
 proof -
   have "0*a + 0*a = 0*a + 0"
     by (simp add: left_distrib [symmetric])
   thus ?thesis by (simp only: add_left_cancel)
 qed
 
-lemma mult_right_zero [simp]: "a * 0 = (0::'a::ring)"
+lemma mult_right_zero [simp]: "a * 0 = (0::'a::semiring)"
   by (simp add: mult_commute)
 
 
@@ -237,55 +234,68 @@
   done
 
 lemma add_strict_left_mono:
-     "a < b ==> c + a < c + (b::'a::ordered_ring)"
+     "a < b ==> c + a < c + (b::'a::ordered_semiring)"
  by (simp add: order_less_le add_left_mono) 
 
 lemma add_strict_right_mono:
-     "a < b ==> a + c < b + (c::'a::ordered_ring)"
+     "a < b ==> a + c < b + (c::'a::ordered_semiring)"
  by (simp add: add_commute [of _ c] add_strict_left_mono)
 
 text{*Strict monotonicity in both arguments*}
-lemma add_strict_mono: "[|a<b; c<d|] ==> a + c < b + (d::'a::ordered_ring)"
+lemma add_strict_mono: "[|a<b; c<d|] ==> a + c < b + (d::'a::ordered_semiring)"
 apply (erule add_strict_right_mono [THEN order_less_trans])
 apply (erule add_strict_left_mono)
 done
 
+lemma add_less_le_mono: "[| a<b; c\<le>d |] ==> a + c < b + (d::'a::ordered_semiring)"
+apply (erule add_strict_right_mono [THEN order_less_le_trans])
+apply (erule add_left_mono) 
+done
+
+lemma add_le_less_mono:
+     "[| a\<le>b; c<d |] ==> a + c < b + (d::'a::ordered_semiring)"
+apply (erule add_right_mono [THEN order_le_less_trans])
+apply (erule add_strict_left_mono) 
+done
+
 lemma add_less_imp_less_left:
-      assumes less: "c + a < c + b"  shows "a < (b::'a::ordered_ring)"
-  proof -
-  have "-c + (c + a) < -c + (c + b)"
-    by (rule add_strict_left_mono [OF less])
-  thus "a < b" by (simp add: add_assoc [symmetric])
+      assumes less: "c + a < c + b"  shows "a < (b::'a::ordered_semiring)"
+  proof (rule ccontr)
+    assume "~ a < b"
+    hence "b \<le> a" by (simp add: linorder_not_less)
+    hence "c+b \<le> c+a" by (rule add_left_mono)
+    with this and less show False 
+      by (simp add: linorder_not_less [symmetric])
   qed
 
 lemma add_less_imp_less_right:
-      "a + c < b + c ==> a < (b::'a::ordered_ring)"
+      "a + c < b + c ==> a < (b::'a::ordered_semiring)"
 apply (rule add_less_imp_less_left [of c])
 apply (simp add: add_commute)  
 done
 
 lemma add_less_cancel_left [simp]:
-    "(c+a < c+b) = (a < (b::'a::ordered_ring))"
+    "(c+a < c+b) = (a < (b::'a::ordered_semiring))"
 by (blast intro: add_less_imp_less_left add_strict_left_mono) 
 
 lemma add_less_cancel_right [simp]:
-    "(a+c < b+c) = (a < (b::'a::ordered_ring))"
+    "(a+c < b+c) = (a < (b::'a::ordered_semiring))"
 by (blast intro: add_less_imp_less_right add_strict_right_mono)
 
 lemma add_le_cancel_left [simp]:
-    "(c+a \<le> c+b) = (a \<le> (b::'a::ordered_ring))"
+    "(c+a \<le> c+b) = (a \<le> (b::'a::ordered_semiring))"
 by (simp add: linorder_not_less [symmetric]) 
 
 lemma add_le_cancel_right [simp]:
-    "(a+c \<le> b+c) = (a \<le> (b::'a::ordered_ring))"
+    "(a+c \<le> b+c) = (a \<le> (b::'a::ordered_semiring))"
 by (simp add: linorder_not_less [symmetric]) 
 
 lemma add_le_imp_le_left:
-      "c + a \<le> c + b ==> a \<le> (b::'a::ordered_ring)"
+      "c + a \<le> c + b ==> a \<le> (b::'a::ordered_semiring)"
 by simp
 
 lemma add_le_imp_le_right:
-      "a + c \<le> b + c ==> a \<le> (b::'a::ordered_ring)"
+      "a + c \<le> b + c ==> a \<le> (b::'a::ordered_semiring)"
 by simp
 
 
@@ -465,13 +475,13 @@
 by (simp add: mult_commute [of _ c] mult_strict_left_mono)
 
 lemma mult_left_mono:
-     "[|a \<le> b; 0 \<le> c|] ==> c * a \<le> c * (b::'a::ordered_ring)"
+     "[|a \<le> b; 0 \<le> c|] ==> c * a \<le> c * (b::'a::ordered_semiring)"
   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 \<le> c|] ==> a*c \<le> b * (c::'a::ordered_ring)"
+     "[|a \<le> b; 0 \<le> c|] ==> a*c \<le> b * (c::'a::ordered_semiring)"
   by (simp add: mult_left_mono mult_commute [of _ c]) 
 
 lemma mult_strict_left_mono_neg:
@@ -489,16 +499,17 @@
 
 subsection{* Products of Signs *}
 
-lemma mult_pos: "[| (0::'a::ordered_ring) < a; 0 < b |] ==> 0 < a*b"
+lemma mult_pos: "[| (0::'a::ordered_semiring) < a; 0 < b |] ==> 0 < a*b"
 by (drule mult_strict_left_mono [of 0 b], auto)
 
-lemma mult_pos_neg: "[| (0::'a::ordered_ring) < a; b < 0 |] ==> a*b < 0"
+lemma mult_pos_neg: "[| (0::'a::ordered_semiring) < a; b < 0 |] ==> a*b < 0"
 by (drule mult_strict_left_mono [of b 0], auto)
 
 lemma mult_neg: "[| a < (0::'a::ordered_ring); b < 0 |] ==> 0 < a*b"
 by (drule mult_strict_right_mono_neg, auto)
 
-lemma zero_less_mult_pos: "[| 0 < a*b; 0 < a|] ==> 0 < (b::'a::ordered_ring)"
+lemma zero_less_mult_pos:
+     "[| 0 < a*b; 0 < a|] ==> 0 < (b::'a::ordered_semiring)"
 apply (case_tac "b\<le>0") 
  apply (auto simp add: order_le_less linorder_not_less)
 apply (drule_tac mult_pos_neg [of a b]) 
@@ -513,7 +524,7 @@
 apply (blast dest: zero_less_mult_pos) 
 done
 
-text{*A field has no "zero divisors", so this theorem should hold without the
+text{*A field has no "zero divisors", and this theorem holds without the
       assumption of an ordering.  See @{text field_mult_eq_0_iff} below.*}
 lemma mult_eq_0_iff [simp]: "(a*b = (0::'a::ordered_ring)) = (a = 0 | b = 0)"
 apply (case_tac "a < 0")
@@ -564,7 +575,7 @@
 
 text{*Strict monotonicity in both arguments*}
 lemma mult_strict_mono:
-     "[|a<b; c<d; 0<b; 0\<le>c|] ==> a * c < b * (d::'a::ordered_ring)"
+     "[|a<b; c<d; 0<b; 0\<le>c|] ==> a * c < b * (d::'a::ordered_semiring)"
 apply (case_tac "c=0")
  apply (simp add: mult_pos) 
 apply (erule mult_strict_right_mono [THEN order_less_trans])
@@ -574,14 +585,14 @@
 
 text{*This weaker variant has more natural premises*}
 lemma mult_strict_mono':
-     "[| a<b; c<d; 0 \<le> a; 0 \<le> c|] ==> a * c < b * (d::'a::ordered_ring)"
+     "[| a<b; c<d; 0 \<le> a; 0 \<le> c|] ==> a * c < b * (d::'a::ordered_semiring)"
 apply (rule mult_strict_mono)
 apply (blast intro: order_le_less_trans)+
 done
 
 lemma mult_mono:
      "[|a \<le> b; c \<le> d; 0 \<le> b; 0 \<le> c|] 
-      ==> a * c  \<le>  b * (d::'a::ordered_ring)"
+      ==> a * c  \<le>  b * (d::'a::ordered_semiring)"
 apply (erule mult_right_mono [THEN order_trans], assumption)
 apply (erule mult_left_mono, assumption)
 done
@@ -618,12 +629,19 @@
 by (simp add: mult_commute [of c] mult_le_cancel_right)
 
 lemma mult_less_imp_less_left:
-    "[|c*a < c*b; 0 < c|] ==> a < (b::'a::ordered_ring)"
-  by (force elim: order_less_asym simp add: mult_less_cancel_left)
+      assumes less: "c*a < c*b" and nonneg: "0 \<le> c"
+      shows "a < (b::'a::ordered_semiring)"
+  proof (rule ccontr)
+    assume "~ a < b"
+    hence "b \<le> a" by (simp add: linorder_not_less)
+    hence "c*b \<le> c*a" by (rule mult_left_mono)
+    with this and less show False 
+      by (simp add: linorder_not_less [symmetric])
+  qed
 
 lemma mult_less_imp_less_right:
-    "[|a*c < b*c; 0 < c|] ==> a < (b::'a::ordered_ring)"
-  by (force elim: order_less_asym simp add: mult_less_cancel_right)
+    "[|a*c < b*c; 0 \<le> c|] ==> a < (b::'a::ordered_semiring)"
+  by (rule mult_less_imp_less_left, simp add: mult_commute)
 
 text{*Cancellation of equalities with a common factor*}
 lemma mult_cancel_right [simp]:
@@ -1433,7 +1451,6 @@
 apply (simp add: nonzero_abs_inverse) 
 done
 
-
 lemma nonzero_abs_divide:
      "b \<noteq> 0 ==> abs (a / (b::'a::ordered_field)) = abs a / abs b"
 by (simp add: divide_inverse abs_mult nonzero_abs_inverse) 
@@ -1556,6 +1573,8 @@
 val add_strict_left_mono = thm"add_strict_left_mono";
 val add_strict_right_mono = thm"add_strict_right_mono";
 val add_strict_mono = thm"add_strict_mono";
+val add_less_le_mono = thm"add_less_le_mono";
+val add_le_less_mono = thm"add_le_less_mono";
 val add_less_imp_less_left = thm"add_less_imp_less_left";
 val add_less_imp_less_right = thm"add_less_imp_less_right";
 val add_less_cancel_left = thm"add_less_cancel_left";