author paulson Tue Jan 06 10:40:15 2004 +0100 (2004-01-06) changeset 14341 a09441bd4f1e 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 file | annotate | diff | revisions src/HOL/Complex/NSComplex.thy file | annotate | diff | revisions src/HOL/Hyperreal/HyperDef.thy file | annotate | diff | revisions src/HOL/Integ/Int.thy file | annotate | diff | revisions src/HOL/Integ/IntDef.thy file | annotate | diff | revisions src/HOL/Library/Rational_Numbers.thy file | annotate | diff | revisions src/HOL/Nat.thy file | annotate | diff | revisions src/HOL/Real/Complex_Numbers.thy file | annotate | diff | revisions src/HOL/Real/RealDef.thy file | annotate | diff | revisions src/HOL/Ring_and_Field.thy file | annotate | diff | revisions
```     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.6
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.14
1.15  lemma complex_add_minus_cancel: "z + (- z + w) = (w::complex)"
1.17  done
1.18
1.19  lemma complex_minus_add_cancel: "(-z) + (z + w) = (w::complex)"
1.21 -done
1.23
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.32  done
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.41
1.42
1.43  subsection{*Multiplication*}
1.44 @@ -552,7 +550,7 @@
1.45    show "0 + z = z"
1.47    show "-z + z = 0"
1.50    show "z - w = z + -w"
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.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.67 +    qed
1.68    assume neq: "w \<noteq> 0"
1.69    thus "z / w = z * inverse w"
1.71 @@ -1700,7 +1704,6 @@
```
```     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.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.13 +    qed
2.14    assume neq: "w \<noteq> 0"
2.15    thus "z / w = z * inverse w"
```
```     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.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.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.40
5.41  (*This lemma allows direct proofs of other <-properties*)
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.52
5.53 @@ -397,8 +418,14 @@
5.54  lemma zero_less_int_conv [simp]: "(0 < int n) = (0 < n)"
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.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.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.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.10 +
6.11 +lemma rat_add_0: "0 + q = (q::rat)"
6.13 +
6.14 +lemma rat_left_minus: "(-q) + q = (0::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.24    show "q + r = r + q"
6.26    show "0 + q = q"
6.28    show "(-q) + q = 0"
6.30 +    by (rule rat_left_minus)
6.31    show "q - r = q + (-r)"
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.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.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.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.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.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.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.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.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.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.159 -  done
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.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.180    done
7.181
7.182  lemma not_add_less1 [iff]: "~ (i + j < (i::nat))"
7.183 @@ -835,7 +842,9 @@
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.190 +  done
7.191
7.192  lemma add_leD2: "m + k \<le> n ==> k \<le> (n::nat)"
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.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.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.12 +    qed
8.13    assume neq: "w \<noteq> 0"
8.14    thus "z / w = z * inverse w"
```
```     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.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.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.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.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.31
10.33 -     "(b + a = c + a) = (b = (c::'a::ring))"
10.34 +     "(b + a = c + a) = (b = (c::'a::semiring))"
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.53
10.54
10.55 @@ -237,55 +234,68 @@
10.56    done
10.57
10.59 -     "a < b ==> c + a < c + (b::'a::ordered_ring)"
10.60 +     "a < b ==> c + a < c + (b::'a::ordered_semiring)"
10.62
10.64 -     "a < b ==> a + c < b + (c::'a::ordered_ring)"
10.65 +     "a < b ==> a + c < b + (c::'a::ordered_semiring)"
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.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.78 +done
10.79 +
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.84 +done
10.85 +
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.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.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.106  done
10.107
10.109 -    "(c+a < c+b) = (a < (b::'a::ordered_ring))"
10.110 +    "(c+a < c+b) = (a < (b::'a::ordered_semiring))"
10.112
10.114 -    "(a+c < b+c) = (a < (b::'a::ordered_ring))"
10.115 +    "(a+c < b+c) = (a < (b::'a::ordered_semiring))"
10.117
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.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.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.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.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.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 @@