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.
--- 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";
--- 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)
--- 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
--- 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)
--- 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
--- 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
--- 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
--- 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)
--- 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";
--- 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";