Ring_and_Field now requires axiom add_left_imp_eq for semirings.
authorpaulson
Tue Jan 06 10:40:15 2004 +0100 (2004-01-06)
changeset 14341a09441bd4f1e
parent 14340 bc93ffa674cc
child 14342 6e564092d72d
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.
src/HOL/Complex/Complex.thy
src/HOL/Complex/NSComplex.thy
src/HOL/Hyperreal/HyperDef.thy
src/HOL/Integ/Int.thy
src/HOL/Integ/IntDef.thy
src/HOL/Library/Rational_Numbers.thy
src/HOL/Nat.thy
src/HOL/Real/Complex_Numbers.thy
src/HOL/Real/RealDef.thy
src/HOL/Ring_and_Field.thy
     1.1 --- a/src/HOL/Complex/Complex.thy	Tue Jan 06 10:38:14 2004 +0100
     1.2 +++ b/src/HOL/Complex/Complex.thy	Tue Jan 06 10:40:15 2004 +0100
     1.3 @@ -343,20 +343,18 @@
     1.4  done
     1.5  declare complex_add_minus_right_zero [simp]
     1.6  
     1.7 -lemma complex_add_minus_left_zero:
     1.8 +lemma complex_add_minus_left:
     1.9        "-z + z = (0::complex)"
    1.10  apply (unfold complex_add_def complex_minus_def complex_zero_def)
    1.11  apply (simp (no_asm))
    1.12  done
    1.13 -declare complex_add_minus_left_zero [simp]
    1.14  
    1.15  lemma complex_add_minus_cancel: "z + (- z + w) = (w::complex)"
    1.16  apply (simp (no_asm) add: complex_add_assoc [symmetric])
    1.17  done
    1.18  
    1.19  lemma complex_minus_add_cancel: "(-z) + (z + w) = (w::complex)"
    1.20 -apply (simp (no_asm) add: complex_add_assoc [symmetric])
    1.21 -done
    1.22 +by (simp add: complex_add_minus_left complex_add_assoc [symmetric])
    1.23  
    1.24  declare complex_add_minus_cancel [simp] complex_minus_add_cancel [simp]
    1.25  
    1.26 @@ -373,7 +371,7 @@
    1.27  lemma complex_add_left_cancel: "((x::complex) + y = x + z) = (y = z)"
    1.28  apply safe
    1.29  apply (drule_tac f = "%t.-x + t" in arg_cong)
    1.30 -apply (simp add: complex_add_assoc [symmetric])
    1.31 +apply (simp add: complex_add_minus_left complex_add_assoc [symmetric])
    1.32  done
    1.33  declare complex_add_left_cancel [iff]
    1.34  
    1.35 @@ -413,7 +411,7 @@
    1.36  done
    1.37  
    1.38  lemma complex_diff_eq_eq: "((x::complex) - y = z) = (x = z + y)"
    1.39 -by (auto simp add: complex_diff_def complex_add_assoc)
    1.40 +by (auto simp add: complex_add_minus_left complex_diff_def complex_add_assoc)
    1.41  
    1.42  
    1.43  subsection{*Multiplication*}
    1.44 @@ -552,7 +550,7 @@
    1.45    show "0 + z = z"
    1.46      by (rule complex_add_zero_left) 
    1.47    show "-z + z = 0"
    1.48 -    by (rule complex_add_minus_left_zero) 
    1.49 +    by (rule complex_add_minus_left) 
    1.50    show "z - w = z + -w"
    1.51      by (simp add: complex_diff_def)
    1.52    show "(u * v) * w = u * (v * w)"
    1.53 @@ -561,10 +559,16 @@
    1.54      by (rule complex_mult_commute) 
    1.55    show "1 * z = z"
    1.56      by (rule complex_mult_one_left) 
    1.57 -  show "0 \<noteq> (1::complex)"  --{*for some reason it has to be early*}
    1.58 +  show "0 \<noteq> (1::complex)"
    1.59      by (rule complex_zero_not_eq_one) 
    1.60    show "(u + v) * w = u * w + v * w"
    1.61      by (rule complex_add_mult_distrib) 
    1.62 +  show "z+u = z+v ==> u=v"
    1.63 +    proof -
    1.64 +      assume eq: "z+u = z+v" 
    1.65 +      hence "(-z + z) + u = (-z + z) + v" by (simp only: eq complex_add_assoc)
    1.66 +      thus "u = v" by (simp add: complex_add_minus_left)
    1.67 +    qed
    1.68    assume neq: "w \<noteq> 0"
    1.69    thus "z / w = z * inverse w"
    1.70      by (simp add: complex_divide_def)
    1.71 @@ -1700,7 +1704,6 @@
    1.72  val complex_add_zero_left = thm"complex_add_zero_left";
    1.73  val complex_add_zero_right = thm"complex_add_zero_right";
    1.74  val complex_add_minus_right_zero = thm"complex_add_minus_right_zero";
    1.75 -val complex_add_minus_left_zero = thm"complex_add_minus_left_zero";
    1.76  val complex_add_minus_cancel = thm"complex_add_minus_cancel";
    1.77  val complex_minus_add_cancel = thm"complex_minus_add_cancel";
    1.78  val complex_add_minus_eq_minus = thm"complex_add_minus_eq_minus";
     2.1 --- a/src/HOL/Complex/NSComplex.thy	Tue Jan 06 10:38:14 2004 +0100
     2.2 +++ b/src/HOL/Complex/NSComplex.thy	Tue Jan 06 10:40:15 2004 +0100
     2.3 @@ -481,6 +481,13 @@
     2.4      by (rule hcomplex_zero_not_eq_one)
     2.5    show "(u + v) * w = u * w + v * w"
     2.6      by (simp add: hcomplex_add_mult_distrib)
     2.7 +  show "z+u = z+v ==> u=v"
     2.8 +    proof -
     2.9 +      assume eq: "z+u = z+v" 
    2.10 +      hence "(-z + z) + u = (-z + z) + v" by (simp only: eq hcomplex_add_assoc)
    2.11 +      thus "u = v" 
    2.12 +        by (simp only: hcomplex_add_minus_left hcomplex_add_zero_left)
    2.13 +    qed
    2.14    assume neq: "w \<noteq> 0"
    2.15    thus "z / w = z * inverse w"
    2.16      by (simp add: hcomplex_divide_def)
     3.1 --- a/src/HOL/Hyperreal/HyperDef.thy	Tue Jan 06 10:38:14 2004 +0100
     3.2 +++ b/src/HOL/Hyperreal/HyperDef.thy	Tue Jan 06 10:40:15 2004 +0100
     3.3 @@ -474,6 +474,9 @@
     3.4    show "0 \<noteq> (1::hypreal)" by (rule hypreal_zero_not_eq_one)
     3.5    show "x \<noteq> 0 ==> inverse x * x = 1" by (simp add: hypreal_mult_inverse_left)
     3.6    show "y \<noteq> 0 ==> x / y = x * inverse y" by (simp add: hypreal_divide_def)
     3.7 +  assume eq: "z+x = z+y" 
     3.8 +    hence "(-z + z) + x = (-z + z) + y" by (simp only: eq hypreal_add_assoc)
     3.9 +    thus "x = y" by (simp add: hypreal_add_minus_left)
    3.10  qed
    3.11  
    3.12  
     4.1 --- a/src/HOL/Integ/Int.thy	Tue Jan 06 10:38:14 2004 +0100
     4.2 +++ b/src/HOL/Integ/Int.thy	Tue Jan 06 10:40:15 2004 +0100
     4.3 @@ -47,12 +47,6 @@
     4.4  lemma not_iszero_1: "~ iszero 1"
     4.5  by (simp only: Zero_int_def One_int_def One_nat_def iszero_def int_int_eq)
     4.6  
     4.7 -lemma int_0_less_1: "0 < (1::int)"
     4.8 -by (simp only: Zero_int_def One_int_def One_nat_def zless_int)
     4.9 -
    4.10 -lemma int_0_neq_1 [simp]: "0 \<noteq> (1::int)"
    4.11 -by (simp only: Zero_int_def One_int_def One_nat_def int_int_eq)
    4.12 -
    4.13  
    4.14  subsection{*nat: magnitide of an integer, as a natural number*}
    4.15  
    4.16 @@ -154,16 +148,6 @@
    4.17  instance int :: ordered_ring
    4.18  proof
    4.19    fix i j k :: int
    4.20 -  show "(i + j) + k = i + (j + k)" by (simp add: zadd_assoc)
    4.21 -  show "i + j = j + i" by (simp add: zadd_commute)
    4.22 -  show "0 + i = i" by simp
    4.23 -  show "- i + i = 0" by simp
    4.24 -  show "i - j = i + (-j)" by (simp add: zdiff_def)
    4.25 -  show "(i * j) * k = i * (j * k)" by (rule zmult_assoc)
    4.26 -  show "i * j = j * i" by (rule zmult_commute)
    4.27 -  show "1 * i = i" by simp
    4.28 -  show "(i + j) * k = i * k + j * k" by (simp add: int_distrib)
    4.29 -  show "0 \<noteq> (1::int)" by simp
    4.30    show "i \<le> j ==> k + i \<le> k + j" by simp
    4.31    show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: zmult_zless_mono2)
    4.32    show "\<bar>i\<bar> = (if i < 0 then -i else i)" by (simp only: zabs_def)
     5.1 --- a/src/HOL/Integ/IntDef.thy	Tue Jan 06 10:38:14 2004 +0100
     5.2 +++ b/src/HOL/Integ/IntDef.thy	Tue Jan 06 10:40:15 2004 +0100
     5.3 @@ -96,6 +96,10 @@
     5.4  apply (simp add: intrel_def)
     5.5  done
     5.6  
     5.7 +lemma int_int_eq [iff]: "(int m = int n) = (m = n)"
     5.8 +by (fast elim!: inj_int [THEN injD])
     5.9 +
    5.10 +
    5.11  
    5.12  subsection{*zminus: unary negation on Integ*}
    5.13  
    5.14 @@ -327,7 +331,27 @@
    5.15  by (rule trans [OF zmult_commute zmult_1])
    5.16  
    5.17  
    5.18 -(* Theorems about less and less_equal *)
    5.19 +text{*The Integers Form A Ring*}
    5.20 +instance int :: ring
    5.21 +proof
    5.22 +  fix i j k :: int
    5.23 +  show "(i + j) + k = i + (j + k)" by (simp add: zadd_assoc)
    5.24 +  show "i + j = j + i" by (simp add: zadd_commute)
    5.25 +  show "0 + i = i" by simp
    5.26 +  show "- i + i = 0" by simp
    5.27 +  show "i - j = i + (-j)" by (simp add: zdiff_def)
    5.28 +  show "(i * j) * k = i * (j * k)" by (rule zmult_assoc)
    5.29 +  show "i * j = j * i" by (rule zmult_commute)
    5.30 +  show "1 * i = i" by simp
    5.31 +  show "(i + j) * k = i * k + j * k" by (simp add: int_distrib)
    5.32 +  show "0 \<noteq> (1::int)" by (simp only: Zero_int_def One_int_def One_nat_def int_int_eq)
    5.33 +  assume eq: "k+i = k+j" 
    5.34 +    hence "(-k + k) + i = (-k + k) + j" by (simp only: eq zadd_assoc)
    5.35 +    thus "i = j" by simp
    5.36 +qed
    5.37 +
    5.38 +
    5.39 +subsection{*Theorems about the Ordering*}
    5.40  
    5.41  (*This lemma allows direct proofs of other <-properties*)
    5.42  lemma zless_iff_Suc_zadd: 
    5.43 @@ -382,9 +406,6 @@
    5.44  (*** eliminates ~= in premises ***)
    5.45  lemmas int_neqE = int_neq_iff [THEN iffD1, THEN disjE, standard]
    5.46  
    5.47 -lemma int_int_eq [iff]: "(int m = int n) = (m = n)"
    5.48 -by (fast elim!: inj_int [THEN injD])
    5.49 -
    5.50  lemma int_eq_0_conv [simp]: "(int n = 0) = (n = 0)"
    5.51  by (simp add: Zero_int_def)
    5.52  
    5.53 @@ -397,8 +418,14 @@
    5.54  lemma zero_less_int_conv [simp]: "(0 < int n) = (0 < n)"
    5.55  by (simp add: Zero_int_def)
    5.56  
    5.57 +lemma int_0_less_1: "0 < (1::int)"
    5.58 +by (simp only: Zero_int_def One_int_def One_nat_def zless_int)
    5.59  
    5.60 -(*** Properties of <= ***)
    5.61 +lemma int_0_neq_1 [simp]: "0 \<noteq> (1::int)"
    5.62 +by (simp only: Zero_int_def One_int_def One_nat_def int_int_eq)
    5.63 +
    5.64 +
    5.65 +subsection{*Properties of the @{text "\<le>"} Relation*}
    5.66  
    5.67  lemma zle_int [simp]: "(int m <= int n) = (m<=n)"
    5.68  by (simp add: zle_def le_def)
    5.69 @@ -456,12 +483,6 @@
    5.70  apply (blast elim!: zless_asym)
    5.71  done
    5.72  
    5.73 -lemma zadd_left_cancel [simp]: "!!w::int. (z + w' = z + w) = (w' = w)"
    5.74 -apply safe
    5.75 -apply (drule_tac f = "%x. x + (-z) " in arg_cong)
    5.76 -apply (simp add: Zero_int_def [symmetric] zadd_ac)
    5.77 -done
    5.78 -
    5.79  instance int :: order
    5.80  proof qed (assumption | rule zle_refl zle_trans zle_anti_sym int_less_le)+
    5.81  
    5.82 @@ -472,6 +493,10 @@
    5.83  proof qed (rule zle_linear)
    5.84  
    5.85  
    5.86 +lemma zadd_left_cancel [simp]: "!!w::int. (z + w' = z + w) = (w' = w)"
    5.87 +  by (rule add_left_cancel) 
    5.88 +
    5.89 +
    5.90  ML
    5.91  {*
    5.92  val int_def = thm "int_def";
    5.93 @@ -564,14 +589,6 @@
    5.94  val zle_anti_sym = thm "zle_anti_sym";
    5.95  val int_less_le = thm "int_less_le";
    5.96  val zadd_left_cancel = thm "zadd_left_cancel";
    5.97 -
    5.98 -val diff_less_eq = thm"diff_less_eq";
    5.99 -val less_diff_eq = thm"less_diff_eq";
   5.100 -val eq_diff_eq = thm"eq_diff_eq";
   5.101 -val diff_eq_eq = thm"diff_eq_eq";
   5.102 -val diff_le_eq = thm"diff_le_eq";
   5.103 -val le_diff_eq = thm"le_diff_eq";
   5.104 -val compare_rls = thms "compare_rls";
   5.105  *}
   5.106  
   5.107  end
     6.1 --- a/src/HOL/Library/Rational_Numbers.thy	Tue Jan 06 10:38:14 2004 +0100
     6.2 +++ b/src/HOL/Library/Rational_Numbers.thy	Tue Jan 06 10:40:15 2004 +0100
     6.3 @@ -475,17 +475,28 @@
     6.4  
     6.5  subsubsection {* The ordered field of rational numbers *}
     6.6  
     6.7 +lemma rat_add_assoc: "(q + r) + s = q + (r + (s::rat))"
     6.8 +  by (induct q, induct r, induct s) 
     6.9 +     (simp add: add_rat zadd_ac zmult_ac int_distrib)
    6.10 +
    6.11 +lemma rat_add_0: "0 + q = (q::rat)"
    6.12 +  by (induct q) (simp add: zero_rat add_rat)
    6.13 +
    6.14 +lemma rat_left_minus: "(-q) + q = (0::rat)"
    6.15 +  by (induct q) (simp add: zero_rat minus_rat add_rat eq_rat)
    6.16 +
    6.17 +
    6.18  instance rat :: field
    6.19  proof
    6.20    fix q r s :: rat
    6.21    show "(q + r) + s = q + (r + s)"
    6.22 -    by (induct q, induct r, induct s) (simp add: add_rat zadd_ac zmult_ac int_distrib)
    6.23 +    by (rule rat_add_assoc)
    6.24    show "q + r = r + q"
    6.25      by (induct q, induct r) (simp add: add_rat zadd_ac zmult_ac)
    6.26    show "0 + q = q"
    6.27      by (induct q) (simp add: zero_rat add_rat)
    6.28    show "(-q) + q = 0"
    6.29 -    by (induct q) (simp add: zero_rat minus_rat add_rat eq_rat)
    6.30 +    by (rule rat_left_minus)
    6.31    show "q - r = q + (-r)"
    6.32      by (induct q, induct r) (simp add: add_rat minus_rat diff_rat)
    6.33    show "(q * r) * s = q * (r * s)"
    6.34 @@ -495,14 +506,19 @@
    6.35    show "1 * q = q"
    6.36      by (induct q) (simp add: one_rat mult_rat)
    6.37    show "(q + r) * s = q * s + r * s"
    6.38 -    by (induct q, induct r, induct s) (simp add: add_rat mult_rat eq_rat int_distrib)
    6.39 +    by (induct q, induct r, induct s) 
    6.40 +       (simp add: add_rat mult_rat eq_rat int_distrib)
    6.41    show "q \<noteq> 0 ==> inverse q * q = 1"
    6.42      by (induct q) (simp add: inverse_rat mult_rat one_rat zero_rat eq_rat)
    6.43    show "r \<noteq> 0 ==> q / r = q * inverse r"
    6.44 -    by (induct q, induct r) (simp add: mult_rat divide_rat inverse_rat zero_rat eq_rat)
    6.45 +    by (induct q, induct r)
    6.46 +       (simp add: mult_rat divide_rat inverse_rat zero_rat eq_rat)
    6.47    show "0 \<noteq> (1::rat)"
    6.48      by (simp add: zero_rat_def one_rat_def rat_of_equality 
    6.49                    zero_fraction_def one_fraction_def) 
    6.50 +  assume eq: "s+q = s+r" 
    6.51 +    hence "(-s + s) + q = (-s + s) + r" by (simp only: eq rat_add_assoc)
    6.52 +    thus "q = r" by (simp add: rat_left_minus rat_add_0)
    6.53  qed
    6.54  
    6.55  instance rat :: linorder
     7.1 --- a/src/HOL/Nat.thy	Tue Jan 06 10:38:14 2004 +0100
     7.2 +++ b/src/HOL/Nat.thy	Tue Jan 06 10:40:15 2004 +0100
     7.3 @@ -460,6 +460,14 @@
     7.4    apply blast
     7.5    done
     7.6  
     7.7 +text {* Type {@typ nat} is a wellfounded linear order *}
     7.8 +
     7.9 +instance nat :: order by (intro_classes,
    7.10 +  (assumption | rule le_refl le_trans le_anti_sym nat_less_le)+)
    7.11 +instance nat :: linorder by (intro_classes, rule nat_le_linear)
    7.12 +instance nat :: wellorder by (intro_classes, rule wf_less)
    7.13 +
    7.14 +
    7.15  lemma not_less_less_Suc_eq: "~ n < m ==> (n < Suc m) = (n = m)"
    7.16    by (blast elim!: less_SucE)
    7.17  
    7.18 @@ -488,13 +496,6 @@
    7.19  lemma one_reorient: "(1 = x) = (x = 1)"
    7.20    by auto
    7.21  
    7.22 -text {* Type {@typ nat} is a wellfounded linear order *}
    7.23 -
    7.24 -instance nat :: order by (intro_classes,
    7.25 -  (assumption | rule le_refl le_trans le_anti_sym nat_less_le)+)
    7.26 -instance nat :: linorder by (intro_classes, rule nat_le_linear)
    7.27 -instance nat :: wellorder by (intro_classes, rule wf_less)
    7.28 -
    7.29  subsection {* Arithmetic operators *}
    7.30  
    7.31  axclass power < type
    7.32 @@ -525,7 +526,8 @@
    7.33    mult_0:   "0 * n = 0"
    7.34    mult_Suc: "Suc m * n = n + (m * n)"
    7.35  
    7.36 -text {* These 2 rules ease the use of primitive recursion. NOTE USE OF @{text "=="} *}
    7.37 +text {* These two rules ease the use of primitive recursion. 
    7.38 +NOTE USE OF @{text "=="} *}
    7.39  lemma def_nat_rec_0: "(!!n. f n == nat_rec c h n) ==> f 0 = c"
    7.40    by simp
    7.41  
    7.42 @@ -560,7 +562,7 @@
    7.43  lemma less_Suc_eq_0_disj: "(m < Suc n) = (m = 0 | (\<exists>j. m = Suc j & j < n))"
    7.44    by (case_tac m) simp_all
    7.45  
    7.46 -lemma nat_induct2: "P 0 ==> P (Suc 0) ==> (!!k. P k ==> P (Suc (Suc k))) ==> P n"
    7.47 +lemma nat_induct2: "[|P 0; P (Suc 0); !!k. P k ==> P (Suc (Suc k))|] ==> P n"
    7.48    apply (rule nat_less_induct)
    7.49    apply (case_tac n)
    7.50    apply (case_tac [2] nat)
    7.51 @@ -690,25 +692,6 @@
    7.52    apply (simp add: nat_add_assoc del: add_0_right)
    7.53    done
    7.54  
    7.55 -subsection {* Monotonicity of Addition *}
    7.56 -
    7.57 -text {* strict, in 1st argument *}
    7.58 -lemma add_less_mono1: "i < j ==> i + k < j + (k::nat)"
    7.59 -  by (induct k) simp_all
    7.60 -
    7.61 -text {* strict, in both arguments *}
    7.62 -lemma add_less_mono: "[|i < j; k < l|] ==> i + k < j + (l::nat)"
    7.63 -  apply (rule add_less_mono1 [THEN less_trans], assumption+)
    7.64 -  apply (induct_tac j, simp_all)
    7.65 -  done
    7.66 -
    7.67 -text {* Deleted @{text less_natE}; use @{text "less_imp_Suc_add RS exE"} *}
    7.68 -lemma less_imp_Suc_add: "m < n ==> (\<exists>k. n = Suc (m + k))"
    7.69 -  apply (induct n)
    7.70 -  apply (simp_all add: order_le_less)
    7.71 -  apply (blast elim!: less_SucE intro!: add_0_right [symmetric] add_Suc_right [symmetric])
    7.72 -  done
    7.73 -
    7.74  
    7.75  subsection {* Multiplication *}
    7.76  
    7.77 @@ -735,20 +718,9 @@
    7.78  lemma nat_mult_assoc: "(m * n) * k = m * ((n * k)::nat)"
    7.79    by (induct m) (simp_all add: add_mult_distrib)
    7.80  
    7.81 -lemma mult_is_0 [simp]: "((m::nat) * n = 0) = (m=0 | n=0)"
    7.82 -  apply (induct_tac m)
    7.83 -  apply (induct_tac [2] n, simp_all)
    7.84 -  done
    7.85  
    7.86 -text {* strict, in 1st argument; proof is by induction on @{text "k > 0"} *}
    7.87 -lemma mult_less_mono2: "(i::nat) < j ==> 0 < k ==> k * i < k * j"
    7.88 -  apply (erule_tac m1 = 0 in less_imp_Suc_add [THEN exE], simp)
    7.89 -  apply (induct_tac x) 
    7.90 -  apply (simp_all add: add_less_mono)
    7.91 -  done
    7.92 -
    7.93 -text{*The Naturals Form an Ordered Semiring*}
    7.94 -instance nat :: ordered_semiring
    7.95 +text{*The Naturals Form A Semiring*}
    7.96 +instance nat :: semiring
    7.97  proof
    7.98    fix i j k :: nat
    7.99    show "(i + j) + k = i + (j + k)" by (rule nat_add_assoc)
   7.100 @@ -759,6 +731,46 @@
   7.101    show "1 * i = i" by simp
   7.102    show "(i + j) * k = i * k + j * k" by (simp add: add_mult_distrib)
   7.103    show "0 \<noteq> (1::nat)" by simp
   7.104 +  assume "k+i = k+j" thus "i=j" by simp
   7.105 +qed
   7.106 +
   7.107 +lemma mult_is_0 [simp]: "((m::nat) * n = 0) = (m=0 | n=0)"
   7.108 +  apply (induct_tac m)
   7.109 +  apply (induct_tac [2] n, simp_all)
   7.110 +  done
   7.111 +
   7.112 +subsection {* Monotonicity of Addition *}
   7.113 +
   7.114 +text {* strict, in 1st argument *}
   7.115 +lemma add_less_mono1: "i < j ==> i + k < j + (k::nat)"
   7.116 +  by (induct k) simp_all
   7.117 +
   7.118 +text {* strict, in both arguments *}
   7.119 +lemma add_less_mono: "[|i < j; k < l|] ==> i + k < j + (l::nat)"
   7.120 +  apply (rule add_less_mono1 [THEN less_trans], assumption+)
   7.121 +  apply (induct_tac j, simp_all)
   7.122 +  done
   7.123 +
   7.124 +text {* Deleted @{text less_natE}; use @{text "less_imp_Suc_add RS exE"} *}
   7.125 +lemma less_imp_Suc_add: "m < n ==> (\<exists>k. n = Suc (m + k))"
   7.126 +  apply (induct n)
   7.127 +  apply (simp_all add: order_le_less)
   7.128 +  apply (blast elim!: less_SucE 
   7.129 +               intro!: add_0_right [symmetric] add_Suc_right [symmetric])
   7.130 +  done
   7.131 +
   7.132 +text {* strict, in 1st argument; proof is by induction on @{text "k > 0"} *}
   7.133 +lemma mult_less_mono2: "(i::nat) < j ==> 0 < k ==> k * i < k * j"
   7.134 +  apply (erule_tac m1 = 0 in less_imp_Suc_add [THEN exE], simp)
   7.135 +  apply (induct_tac x) 
   7.136 +  apply (simp_all add: add_less_mono)
   7.137 +  done
   7.138 +
   7.139 +
   7.140 +text{*The Naturals Form an Ordered Semiring*}
   7.141 +instance nat :: ordered_semiring
   7.142 +proof
   7.143 +  fix i j k :: nat
   7.144    show "i \<le> j ==> k + i \<le> k + j" by simp
   7.145    show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: mult_less_mono2)
   7.146  qed
   7.147 @@ -790,14 +802,10 @@
   7.148    by (rule add_mono)
   7.149  
   7.150  lemma le_add2: "n \<le> ((m + n)::nat)"
   7.151 -  apply (induct m, simp_all)
   7.152 -  apply (erule le_SucI)
   7.153 -  done
   7.154 +  by (insert add_right_mono [of 0 m n], simp) 
   7.155  
   7.156  lemma le_add1: "n \<le> ((n + m)::nat)"
   7.157 -  apply (simp add: add_ac)
   7.158 -  apply (rule le_add2)
   7.159 -  done
   7.160 +  by (simp add: add_commute, rule le_add2)
   7.161  
   7.162  lemma less_add_Suc1: "i < Suc (i + m)"
   7.163    by (rule le_less_trans, rule le_add1, rule lessI)
   7.164 @@ -808,7 +816,6 @@
   7.165  lemma less_iff_Suc_add: "(m < n) = (\<exists>k. n = Suc (m + k))"
   7.166    by (rules intro!: less_add_Suc1 less_imp_Suc_add)
   7.167  
   7.168 -
   7.169  lemma trans_le_add1: "(i::nat) \<le> j ==> i \<le> j + m"
   7.170    by (rule le_trans, assumption, rule le_add1)
   7.171  
   7.172 @@ -822,8 +829,8 @@
   7.173    by (rule less_le_trans, assumption, rule le_add2)
   7.174  
   7.175  lemma add_lessD1: "i + j < (k::nat) ==> i < k"
   7.176 -  apply (induct j, simp_all)
   7.177 -  apply (blast dest: Suc_lessD)
   7.178 +  apply (rule le_less_trans [of _ "i+j"]) 
   7.179 +  apply (simp_all add: le_add1)
   7.180    done
   7.181  
   7.182  lemma not_add_less1 [iff]: "~ (i + j < (i::nat))"
   7.183 @@ -835,7 +842,9 @@
   7.184    by (simp add: add_commute not_add_less1)
   7.185  
   7.186  lemma add_leD1: "m + k \<le> n ==> m \<le> (n::nat)"
   7.187 -  by (induct k) (simp_all add: le_simps)
   7.188 +  apply (rule order_trans [of _ "m+k"]) 
   7.189 +  apply (simp_all add: le_add1)
   7.190 +  done
   7.191  
   7.192  lemma add_leD2: "m + k \<le> n ==> k \<le> (n::nat)"
   7.193    apply (simp add: add_commute)
   7.194 @@ -969,21 +978,17 @@
   7.195  subsection {* Monotonicity of Multiplication *}
   7.196  
   7.197  lemma mult_le_mono1: "i \<le> (j::nat) ==> i * k \<le> j * k"
   7.198 -  by (induct k) (simp_all add: add_le_mono)
   7.199 +  by (simp add: mult_right_mono) 
   7.200  
   7.201  lemma mult_le_mono2: "i \<le> (j::nat) ==> k * i \<le> k * j"
   7.202 -  apply (drule mult_le_mono1)
   7.203 -  apply (simp add: mult_commute)
   7.204 -  done
   7.205 +  by (simp add: mult_left_mono) 
   7.206  
   7.207  text {* @{text "\<le>"} monotonicity, BOTH arguments *}
   7.208  lemma mult_le_mono: "i \<le> (j::nat) ==> k \<le> l ==> i * k \<le> j * l"
   7.209 -  apply (erule mult_le_mono1 [THEN le_trans])
   7.210 -  apply (erule mult_le_mono2)
   7.211 -  done
   7.212 +  by (simp add: mult_mono) 
   7.213  
   7.214  lemma mult_less_mono1: "(i::nat) < j ==> 0 < k ==> i * k < j * k"
   7.215 -  by (drule mult_less_mono2) (simp_all add: mult_commute)
   7.216 +  by (simp add: mult_strict_right_mono) 
   7.217  
   7.218  text{*Differs from the standard @{text zero_less_mult_iff} in that
   7.219        there are no negative numbers.*}
   7.220 @@ -1007,7 +1012,7 @@
   7.221    apply (rule_tac [2] mult_eq_1_iff, fastsimp)
   7.222    done
   7.223  
   7.224 -lemma mult_less_cancel2: "((m::nat) * k < n * k) = (0 < k & m < n)"
   7.225 +lemma mult_less_cancel2 [simp]: "((m::nat) * k < n * k) = (0 < k & m < n)"
   7.226    apply (safe intro!: mult_less_mono1)
   7.227    apply (case_tac k, auto)
   7.228    apply (simp del: le_0_eq add: linorder_not_le [symmetric])
   7.229 @@ -1015,9 +1020,7 @@
   7.230    done
   7.231  
   7.232  lemma mult_less_cancel1 [simp]: "(k * (m::nat) < k * n) = (0 < k & m < n)"
   7.233 -  by (simp add: mult_less_cancel2 mult_commute [of k])
   7.234 -
   7.235 -declare mult_less_cancel2 [simp]
   7.236 +  by (simp add: mult_commute [of k])
   7.237  
   7.238  lemma mult_le_cancel1 [simp]: "(k * (m::nat) \<le> k * n) = (0 < k --> m \<le> n)"
   7.239  by (simp add: linorder_not_less [symmetric], auto)
   7.240 @@ -1025,15 +1028,13 @@
   7.241  lemma mult_le_cancel2 [simp]: "((m::nat) * k \<le> n * k) = (0 < k --> m \<le> n)"
   7.242  by (simp add: linorder_not_less [symmetric], auto)
   7.243  
   7.244 -lemma mult_cancel2: "(m * k = n * k) = (m = n | (k = (0::nat)))"
   7.245 +lemma mult_cancel2 [simp]: "(m * k = n * k) = (m = n | (k = (0::nat)))"
   7.246    apply (cut_tac less_linear, safe, auto)
   7.247    apply (drule mult_less_mono1, assumption, simp)+
   7.248    done
   7.249  
   7.250  lemma mult_cancel1 [simp]: "(k * m = k * n) = (m = n | (k = (0::nat)))"
   7.251 -  by (simp add: mult_cancel2 mult_commute [of k])
   7.252 -
   7.253 -declare mult_cancel2 [simp]
   7.254 +  by (simp add: mult_commute [of k])
   7.255  
   7.256  lemma Suc_mult_less_cancel1: "(Suc k * m < Suc k * n) = (m < n)"
   7.257    by (subst mult_less_cancel1) simp
   7.258 @@ -1044,7 +1045,6 @@
   7.259  lemma Suc_mult_cancel1: "(Suc k * m = Suc k * n) = (m = n)"
   7.260    by (subst mult_cancel1) simp
   7.261  
   7.262 -
   7.263  text {* Lemma for @{text gcd} *}
   7.264  lemma mult_eq_self_implies_10: "(m::nat) = m * n ==> n = 1 | m = 0"
   7.265    apply (drule sym)
   7.266 @@ -1054,5 +1054,4 @@
   7.267    apply (fastsimp dest: mult_less_mono2)
   7.268    done
   7.269  
   7.270 -
   7.271  end
     8.1 --- a/src/HOL/Real/Complex_Numbers.thy	Tue Jan 06 10:38:14 2004 +0100
     8.2 +++ b/src/HOL/Real/Complex_Numbers.thy	Tue Jan 06 10:40:15 2004 +0100
     8.3 @@ -107,6 +107,12 @@
     8.4      by (simp add: zero_complex_def one_complex_def) 
     8.5    show "(u + v) * w = u * w + v * w"
     8.6      by (simp add: add_complex_def mult_complex_def ring_distrib)
     8.7 +  show "z+u = z+v ==> u=v"
     8.8 +    proof -
     8.9 +      assume eq: "z+u = z+v" 
    8.10 +      hence "(-z + z) + u = (-z + z) + v" by (simp add: eq add_complex_def)
    8.11 +      thus "u = v" by (simp add: add_complex_def)
    8.12 +    qed
    8.13    assume neq: "w \<noteq> 0"
    8.14    thus "z / w = z * inverse w"
    8.15      by (simp add: divide_complex_def)
     9.1 --- a/src/HOL/Real/RealDef.thy	Tue Jan 06 10:38:14 2004 +0100
     9.2 +++ b/src/HOL/Real/RealDef.thy	Tue Jan 06 10:40:15 2004 +0100
     9.3 @@ -330,6 +330,9 @@
     9.4  apply (rule someI2, auto)
     9.5  done
     9.6  
     9.7 +
     9.8 +subsection{*The Real Numbers form a Field*}
     9.9 +
    9.10  instance real :: field
    9.11  proof
    9.12    fix x y z :: real
    9.13 @@ -345,10 +348,13 @@
    9.14    show "0 \<noteq> (1::real)" by (rule real_zero_not_eq_one)
    9.15    show "x \<noteq> 0 ==> inverse x * x = 1" by (rule real_mult_inv_left)
    9.16    show "y \<noteq> 0 ==> x / y = x * inverse y" by (simp add: real_divide_def)
    9.17 +  assume eq: "z+x = z+y" 
    9.18 +    hence "(-z + z) + x = (-z + z) + y" by (simp only: eq real_add_assoc)
    9.19 +    thus "x = y" by (simp add: real_add_minus_left)
    9.20  qed
    9.21  
    9.22  
    9.23 -(** Inverse of zero!  Useful to simplify certain equations **)
    9.24 +text{*Inverse of zero!  Useful to simplify certain equations*}
    9.25  
    9.26  lemma INVERSE_ZERO: "inverse 0 = (0::real)"
    9.27  apply (unfold real_inverse_def)
    9.28 @@ -652,33 +658,6 @@
    9.29  done
    9.30  declare real_minus_zero_less_iff2 [simp]
    9.31  
    9.32 -ML
    9.33 -{*
    9.34 -val real_le_def = thm "real_le_def";
    9.35 -val real_diff_def = thm "real_diff_def";
    9.36 -val real_divide_def = thm "real_divide_def";
    9.37 -val real_of_nat_def = thm "real_of_nat_def";
    9.38 -
    9.39 -val preal_trans_lemma = thm"preal_trans_lemma";
    9.40 -val realrel_iff = thm"realrel_iff";
    9.41 -val realrel_refl = thm"realrel_refl";
    9.42 -val equiv_realrel = thm"equiv_realrel";
    9.43 -val equiv_realrel_iff = thm"equiv_realrel_iff";
    9.44 -val realrel_in_real = thm"realrel_in_real";
    9.45 -val inj_on_Abs_REAL = thm"inj_on_Abs_REAL";
    9.46 -val eq_realrelD = thm"eq_realrelD";
    9.47 -val inj_Rep_REAL = thm"inj_Rep_REAL";
    9.48 -val inj_real_of_preal = thm"inj_real_of_preal";
    9.49 -val eq_Abs_REAL = thm"eq_Abs_REAL";
    9.50 -val real_minus_congruent = thm"real_minus_congruent";
    9.51 -val real_minus = thm"real_minus";
    9.52 -val real_add = thm"real_add";
    9.53 -val real_add_commute = thm"real_add_commute";
    9.54 -val real_add_assoc = thm"real_add_assoc";
    9.55 -val real_add_zero_left = thm"real_add_zero_left";
    9.56 -val real_add_zero_right = thm"real_add_zero_right";
    9.57 -
    9.58 -*}
    9.59  
    9.60  subsection{*Properties of Less-Than Or Equals*}
    9.61  
    9.62 @@ -1068,6 +1047,30 @@
    9.63  {*
    9.64  val real_abs_def = thm "real_abs_def";
    9.65  
    9.66 +val real_le_def = thm "real_le_def";
    9.67 +val real_diff_def = thm "real_diff_def";
    9.68 +val real_divide_def = thm "real_divide_def";
    9.69 +val real_of_nat_def = thm "real_of_nat_def";
    9.70 +
    9.71 +val preal_trans_lemma = thm"preal_trans_lemma";
    9.72 +val realrel_iff = thm"realrel_iff";
    9.73 +val realrel_refl = thm"realrel_refl";
    9.74 +val equiv_realrel = thm"equiv_realrel";
    9.75 +val equiv_realrel_iff = thm"equiv_realrel_iff";
    9.76 +val realrel_in_real = thm"realrel_in_real";
    9.77 +val inj_on_Abs_REAL = thm"inj_on_Abs_REAL";
    9.78 +val eq_realrelD = thm"eq_realrelD";
    9.79 +val inj_Rep_REAL = thm"inj_Rep_REAL";
    9.80 +val inj_real_of_preal = thm"inj_real_of_preal";
    9.81 +val eq_Abs_REAL = thm"eq_Abs_REAL";
    9.82 +val real_minus_congruent = thm"real_minus_congruent";
    9.83 +val real_minus = thm"real_minus";
    9.84 +val real_add = thm"real_add";
    9.85 +val real_add_commute = thm"real_add_commute";
    9.86 +val real_add_assoc = thm"real_add_assoc";
    9.87 +val real_add_zero_left = thm"real_add_zero_left";
    9.88 +val real_add_zero_right = thm"real_add_zero_right";
    9.89 +
    9.90  val real_less_eq_diff = thm "real_less_eq_diff";
    9.91  
    9.92  val real_mult = thm"real_mult";
    10.1 --- a/src/HOL/Ring_and_Field.thy	Tue Jan 06 10:38:14 2004 +0100
    10.2 +++ b/src/HOL/Ring_and_Field.thy	Tue Jan 06 10:40:15 2004 +0100
    10.3 @@ -20,6 +20,11 @@
    10.4    add_assoc: "(a + b) + c = a + (b + c)"
    10.5    add_commute: "a + b = b + a"
    10.6    add_0 [simp]: "0 + a = a"
    10.7 +  add_left_imp_eq: "a + b = a + c ==> b=c"
    10.8 +    --{*This axiom is needed for semirings only: for rings, etc., it is
    10.9 +        redundant. Including it allows many more of the following results
   10.10 +        to be proved for semirings too. The drawback is that this redundant
   10.11 +        axiom must be proved for instances of rings.*}
   10.12  
   10.13    mult_assoc: "(a * b) * c = a * (b * c)"
   10.14    mult_commute: "a * b = b * a"
   10.15 @@ -82,19 +87,11 @@
   10.16  qed
   10.17  
   10.18  lemma add_left_cancel [simp]:
   10.19 -     "(a + b = a + c) = (b = (c::'a::ring))"
   10.20 -proof
   10.21 -  assume eq: "a + b = a + c"
   10.22 -  hence "(-a + a) + b = (-a + a) + c"
   10.23 -    by (simp only: eq add_assoc)
   10.24 -  thus "b = c" by simp
   10.25 -next
   10.26 -  assume eq: "b = c"
   10.27 -  thus "a + b = a + c" by simp
   10.28 -qed
   10.29 +     "(a + b = a + c) = (b = (c::'a::semiring))"
   10.30 +by (blast dest: add_left_imp_eq) 
   10.31  
   10.32  lemma add_right_cancel [simp]:
   10.33 -     "(b + a = c + a) = (b = (c::'a::ring))"
   10.34 +     "(b + a = c + a) = (b = (c::'a::semiring))"
   10.35    by (simp add: add_commute)
   10.36  
   10.37  lemma minus_minus [simp]: "- (- (a::'a::ring)) = a"
   10.38 @@ -169,14 +166,14 @@
   10.39  
   10.40  theorems mult_ac = mult_assoc mult_commute mult_left_commute
   10.41  
   10.42 -lemma mult_left_zero [simp]: "0 * a = (0::'a::ring)"
   10.43 +lemma mult_left_zero [simp]: "0 * a = (0::'a::semiring)"
   10.44  proof -
   10.45    have "0*a + 0*a = 0*a + 0"
   10.46      by (simp add: left_distrib [symmetric])
   10.47    thus ?thesis by (simp only: add_left_cancel)
   10.48  qed
   10.49  
   10.50 -lemma mult_right_zero [simp]: "a * 0 = (0::'a::ring)"
   10.51 +lemma mult_right_zero [simp]: "a * 0 = (0::'a::semiring)"
   10.52    by (simp add: mult_commute)
   10.53  
   10.54  
   10.55 @@ -237,55 +234,68 @@
   10.56    done
   10.57  
   10.58  lemma add_strict_left_mono:
   10.59 -     "a < b ==> c + a < c + (b::'a::ordered_ring)"
   10.60 +     "a < b ==> c + a < c + (b::'a::ordered_semiring)"
   10.61   by (simp add: order_less_le add_left_mono) 
   10.62  
   10.63  lemma add_strict_right_mono:
   10.64 -     "a < b ==> a + c < b + (c::'a::ordered_ring)"
   10.65 +     "a < b ==> a + c < b + (c::'a::ordered_semiring)"
   10.66   by (simp add: add_commute [of _ c] add_strict_left_mono)
   10.67  
   10.68  text{*Strict monotonicity in both arguments*}
   10.69 -lemma add_strict_mono: "[|a<b; c<d|] ==> a + c < b + (d::'a::ordered_ring)"
   10.70 +lemma add_strict_mono: "[|a<b; c<d|] ==> a + c < b + (d::'a::ordered_semiring)"
   10.71  apply (erule add_strict_right_mono [THEN order_less_trans])
   10.72  apply (erule add_strict_left_mono)
   10.73  done
   10.74  
   10.75 +lemma add_less_le_mono: "[| a<b; c\<le>d |] ==> a + c < b + (d::'a::ordered_semiring)"
   10.76 +apply (erule add_strict_right_mono [THEN order_less_le_trans])
   10.77 +apply (erule add_left_mono) 
   10.78 +done
   10.79 +
   10.80 +lemma add_le_less_mono:
   10.81 +     "[| a\<le>b; c<d |] ==> a + c < b + (d::'a::ordered_semiring)"
   10.82 +apply (erule add_right_mono [THEN order_le_less_trans])
   10.83 +apply (erule add_strict_left_mono) 
   10.84 +done
   10.85 +
   10.86  lemma add_less_imp_less_left:
   10.87 -      assumes less: "c + a < c + b"  shows "a < (b::'a::ordered_ring)"
   10.88 -  proof -
   10.89 -  have "-c + (c + a) < -c + (c + b)"
   10.90 -    by (rule add_strict_left_mono [OF less])
   10.91 -  thus "a < b" by (simp add: add_assoc [symmetric])
   10.92 +      assumes less: "c + a < c + b"  shows "a < (b::'a::ordered_semiring)"
   10.93 +  proof (rule ccontr)
   10.94 +    assume "~ a < b"
   10.95 +    hence "b \<le> a" by (simp add: linorder_not_less)
   10.96 +    hence "c+b \<le> c+a" by (rule add_left_mono)
   10.97 +    with this and less show False 
   10.98 +      by (simp add: linorder_not_less [symmetric])
   10.99    qed
  10.100  
  10.101  lemma add_less_imp_less_right:
  10.102 -      "a + c < b + c ==> a < (b::'a::ordered_ring)"
  10.103 +      "a + c < b + c ==> a < (b::'a::ordered_semiring)"
  10.104  apply (rule add_less_imp_less_left [of c])
  10.105  apply (simp add: add_commute)  
  10.106  done
  10.107  
  10.108  lemma add_less_cancel_left [simp]:
  10.109 -    "(c+a < c+b) = (a < (b::'a::ordered_ring))"
  10.110 +    "(c+a < c+b) = (a < (b::'a::ordered_semiring))"
  10.111  by (blast intro: add_less_imp_less_left add_strict_left_mono) 
  10.112  
  10.113  lemma add_less_cancel_right [simp]:
  10.114 -    "(a+c < b+c) = (a < (b::'a::ordered_ring))"
  10.115 +    "(a+c < b+c) = (a < (b::'a::ordered_semiring))"
  10.116  by (blast intro: add_less_imp_less_right add_strict_right_mono)
  10.117  
  10.118  lemma add_le_cancel_left [simp]:
  10.119 -    "(c+a \<le> c+b) = (a \<le> (b::'a::ordered_ring))"
  10.120 +    "(c+a \<le> c+b) = (a \<le> (b::'a::ordered_semiring))"
  10.121  by (simp add: linorder_not_less [symmetric]) 
  10.122  
  10.123  lemma add_le_cancel_right [simp]:
  10.124 -    "(a+c \<le> b+c) = (a \<le> (b::'a::ordered_ring))"
  10.125 +    "(a+c \<le> b+c) = (a \<le> (b::'a::ordered_semiring))"
  10.126  by (simp add: linorder_not_less [symmetric]) 
  10.127  
  10.128  lemma add_le_imp_le_left:
  10.129 -      "c + a \<le> c + b ==> a \<le> (b::'a::ordered_ring)"
  10.130 +      "c + a \<le> c + b ==> a \<le> (b::'a::ordered_semiring)"
  10.131  by simp
  10.132  
  10.133  lemma add_le_imp_le_right:
  10.134 -      "a + c \<le> b + c ==> a \<le> (b::'a::ordered_ring)"
  10.135 +      "a + c \<le> b + c ==> a \<le> (b::'a::ordered_semiring)"
  10.136  by simp
  10.137  
  10.138  
  10.139 @@ -465,13 +475,13 @@
  10.140  by (simp add: mult_commute [of _ c] mult_strict_left_mono)
  10.141  
  10.142  lemma mult_left_mono:
  10.143 -     "[|a \<le> b; 0 \<le> c|] ==> c * a \<le> c * (b::'a::ordered_ring)"
  10.144 +     "[|a \<le> b; 0 \<le> c|] ==> c * a \<le> c * (b::'a::ordered_semiring)"
  10.145    apply (case_tac "c=0", simp)
  10.146    apply (force simp add: mult_strict_left_mono order_le_less) 
  10.147    done
  10.148  
  10.149  lemma mult_right_mono:
  10.150 -     "[|a \<le> b; 0 \<le> c|] ==> a*c \<le> b * (c::'a::ordered_ring)"
  10.151 +     "[|a \<le> b; 0 \<le> c|] ==> a*c \<le> b * (c::'a::ordered_semiring)"
  10.152    by (simp add: mult_left_mono mult_commute [of _ c]) 
  10.153  
  10.154  lemma mult_strict_left_mono_neg:
  10.155 @@ -489,16 +499,17 @@
  10.156  
  10.157  subsection{* Products of Signs *}
  10.158  
  10.159 -lemma mult_pos: "[| (0::'a::ordered_ring) < a; 0 < b |] ==> 0 < a*b"
  10.160 +lemma mult_pos: "[| (0::'a::ordered_semiring) < a; 0 < b |] ==> 0 < a*b"
  10.161  by (drule mult_strict_left_mono [of 0 b], auto)
  10.162  
  10.163 -lemma mult_pos_neg: "[| (0::'a::ordered_ring) < a; b < 0 |] ==> a*b < 0"
  10.164 +lemma mult_pos_neg: "[| (0::'a::ordered_semiring) < a; b < 0 |] ==> a*b < 0"
  10.165  by (drule mult_strict_left_mono [of b 0], auto)
  10.166  
  10.167  lemma mult_neg: "[| a < (0::'a::ordered_ring); b < 0 |] ==> 0 < a*b"
  10.168  by (drule mult_strict_right_mono_neg, auto)
  10.169  
  10.170 -lemma zero_less_mult_pos: "[| 0 < a*b; 0 < a|] ==> 0 < (b::'a::ordered_ring)"
  10.171 +lemma zero_less_mult_pos:
  10.172 +     "[| 0 < a*b; 0 < a|] ==> 0 < (b::'a::ordered_semiring)"
  10.173  apply (case_tac "b\<le>0") 
  10.174   apply (auto simp add: order_le_less linorder_not_less)
  10.175  apply (drule_tac mult_pos_neg [of a b]) 
  10.176 @@ -513,7 +524,7 @@
  10.177  apply (blast dest: zero_less_mult_pos) 
  10.178  done
  10.179  
  10.180 -text{*A field has no "zero divisors", so this theorem should hold without the
  10.181 +text{*A field has no "zero divisors", and this theorem holds without the
  10.182        assumption of an ordering.  See @{text field_mult_eq_0_iff} below.*}
  10.183  lemma mult_eq_0_iff [simp]: "(a*b = (0::'a::ordered_ring)) = (a = 0 | b = 0)"
  10.184  apply (case_tac "a < 0")
  10.185 @@ -564,7 +575,7 @@
  10.186  
  10.187  text{*Strict monotonicity in both arguments*}
  10.188  lemma mult_strict_mono:
  10.189 -     "[|a<b; c<d; 0<b; 0\<le>c|] ==> a * c < b * (d::'a::ordered_ring)"
  10.190 +     "[|a<b; c<d; 0<b; 0\<le>c|] ==> a * c < b * (d::'a::ordered_semiring)"
  10.191  apply (case_tac "c=0")
  10.192   apply (simp add: mult_pos) 
  10.193  apply (erule mult_strict_right_mono [THEN order_less_trans])
  10.194 @@ -574,14 +585,14 @@
  10.195  
  10.196  text{*This weaker variant has more natural premises*}
  10.197  lemma mult_strict_mono':
  10.198 -     "[| a<b; c<d; 0 \<le> a; 0 \<le> c|] ==> a * c < b * (d::'a::ordered_ring)"
  10.199 +     "[| a<b; c<d; 0 \<le> a; 0 \<le> c|] ==> a * c < b * (d::'a::ordered_semiring)"
  10.200  apply (rule mult_strict_mono)
  10.201  apply (blast intro: order_le_less_trans)+
  10.202  done
  10.203  
  10.204  lemma mult_mono:
  10.205       "[|a \<le> b; c \<le> d; 0 \<le> b; 0 \<le> c|] 
  10.206 -      ==> a * c  \<le>  b * (d::'a::ordered_ring)"
  10.207 +      ==> a * c  \<le>  b * (d::'a::ordered_semiring)"
  10.208  apply (erule mult_right_mono [THEN order_trans], assumption)
  10.209  apply (erule mult_left_mono, assumption)
  10.210  done
  10.211 @@ -618,12 +629,19 @@
  10.212  by (simp add: mult_commute [of c] mult_le_cancel_right)
  10.213  
  10.214  lemma mult_less_imp_less_left:
  10.215 -    "[|c*a < c*b; 0 < c|] ==> a < (b::'a::ordered_ring)"
  10.216 -  by (force elim: order_less_asym simp add: mult_less_cancel_left)
  10.217 +      assumes less: "c*a < c*b" and nonneg: "0 \<le> c"
  10.218 +      shows "a < (b::'a::ordered_semiring)"
  10.219 +  proof (rule ccontr)
  10.220 +    assume "~ a < b"
  10.221 +    hence "b \<le> a" by (simp add: linorder_not_less)
  10.222 +    hence "c*b \<le> c*a" by (rule mult_left_mono)
  10.223 +    with this and less show False 
  10.224 +      by (simp add: linorder_not_less [symmetric])
  10.225 +  qed
  10.226  
  10.227  lemma mult_less_imp_less_right:
  10.228 -    "[|a*c < b*c; 0 < c|] ==> a < (b::'a::ordered_ring)"
  10.229 -  by (force elim: order_less_asym simp add: mult_less_cancel_right)
  10.230 +    "[|a*c < b*c; 0 \<le> c|] ==> a < (b::'a::ordered_semiring)"
  10.231 +  by (rule mult_less_imp_less_left, simp add: mult_commute)
  10.232  
  10.233  text{*Cancellation of equalities with a common factor*}
  10.234  lemma mult_cancel_right [simp]:
  10.235 @@ -1433,7 +1451,6 @@
  10.236  apply (simp add: nonzero_abs_inverse) 
  10.237  done
  10.238  
  10.239 -
  10.240  lemma nonzero_abs_divide:
  10.241       "b \<noteq> 0 ==> abs (a / (b::'a::ordered_field)) = abs a / abs b"
  10.242  by (simp add: divide_inverse abs_mult nonzero_abs_inverse) 
  10.243 @@ -1556,6 +1573,8 @@
  10.244  val add_strict_left_mono = thm"add_strict_left_mono";
  10.245  val add_strict_right_mono = thm"add_strict_right_mono";
  10.246  val add_strict_mono = thm"add_strict_mono";
  10.247 +val add_less_le_mono = thm"add_less_le_mono";
  10.248 +val add_le_less_mono = thm"add_le_less_mono";
  10.249  val add_less_imp_less_left = thm"add_less_imp_less_left";
  10.250  val add_less_imp_less_right = thm"add_less_imp_less_right";
  10.251  val add_less_cancel_left = thm"add_less_cancel_left";