--- a/src/HOL/Fields.thy Fri Apr 23 13:58:14 2010 +0200
+++ b/src/HOL/Fields.thy Fri Apr 23 13:58:14 2010 +0200
@@ -31,34 +31,6 @@
subclass idom ..
-lemma right_inverse_eq: "b \<noteq> 0 \<Longrightarrow> a / b = 1 \<longleftrightarrow> a = b"
-proof
- assume neq: "b \<noteq> 0"
- {
- hence "a = (a / b) * b" by (simp add: divide_inverse mult_ac)
- also assume "a / b = 1"
- finally show "a = b" by simp
- next
- assume "a = b"
- with neq show "a / b = 1" by (simp add: divide_inverse)
- }
-qed
-
-lemma nonzero_inverse_eq_divide: "a \<noteq> 0 \<Longrightarrow> inverse a = 1 / a"
-by (simp add: divide_inverse)
-
-lemma divide_self [simp]: "a \<noteq> 0 \<Longrightarrow> a / a = 1"
-by (simp add: divide_inverse)
-
-lemma divide_zero_left [simp]: "0 / a = 0"
-by (simp add: divide_inverse)
-
-lemma inverse_eq_divide: "inverse a = 1 / a"
-by (simp add: divide_inverse)
-
-lemma add_divide_distrib: "(a+b) / c = a/c + b/c"
-by (simp add: divide_inverse algebra_simps)
-
text{*There is no slick version using division by zero.*}
lemma inverse_add:
"[| a \<noteq> 0; b \<noteq> 0 |]
@@ -80,14 +52,8 @@
"\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (b * c) = a / b"
by (simp add: mult_commute [of _ c])
-lemma divide_1 [simp]: "a / 1 = a"
-by (simp add: divide_inverse)
-
-lemma times_divide_eq_right: "a * (b / c) = (a * b) / c"
-by (simp add: divide_inverse mult_assoc)
-
lemma times_divide_eq_left: "(b / c) * a = (b * a) / c"
-by (simp add: divide_inverse mult_ac)
+ by (simp add: divide_inverse mult_ac)
text {* These are later declared as simp rules. *}
lemmas times_divide_eq [no_atp] = times_divide_eq_right times_divide_eq_left
@@ -108,7 +74,7 @@
lemma nonzero_mult_divide_cancel_right [simp, no_atp]:
"b \<noteq> 0 \<Longrightarrow> a * b / b = a"
-using nonzero_mult_divide_mult_cancel_right [of 1 b a] by simp
+ using nonzero_mult_divide_mult_cancel_right [of 1 b a] by simp
lemma nonzero_mult_divide_cancel_left [simp, no_atp]:
"a \<noteq> 0 \<Longrightarrow> a * b / a = b"
@@ -130,58 +96,21 @@
"\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (c * b) = a / b"
using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: mult_ac)
-lemma minus_divide_left: "- (a / b) = (-a) / b"
-by (simp add: divide_inverse)
-
-lemma nonzero_minus_divide_right: "b \<noteq> 0 ==> - (a / b) = a / (- b)"
-by (simp add: divide_inverse nonzero_inverse_minus_eq)
-
-lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a) / (-b) = a / b"
-by (simp add: divide_inverse nonzero_inverse_minus_eq)
-
-lemma divide_minus_left [simp, no_atp]: "(-a) / b = - (a / b)"
-by (simp add: divide_inverse)
-
-lemma diff_divide_distrib: "(a - b) / c = a / c - b / c"
-by (simp add: diff_minus add_divide_distrib)
-
lemma add_divide_eq_iff:
"z \<noteq> 0 \<Longrightarrow> x + y / z = (z * x + y) / z"
-by (simp add: add_divide_distrib)
+ by (simp add: add_divide_distrib)
lemma divide_add_eq_iff:
"z \<noteq> 0 \<Longrightarrow> x / z + y = (x + z * y) / z"
-by (simp add: add_divide_distrib)
+ by (simp add: add_divide_distrib)
lemma diff_divide_eq_iff:
"z \<noteq> 0 \<Longrightarrow> x - y / z = (z * x - y) / z"
-by (simp add: diff_divide_distrib)
+ by (simp add: diff_divide_distrib)
lemma divide_diff_eq_iff:
"z \<noteq> 0 \<Longrightarrow> x / z - y = (x - z * y) / z"
-by (simp add: diff_divide_distrib)
-
-lemma nonzero_eq_divide_eq: "c \<noteq> 0 \<Longrightarrow> a = b / c \<longleftrightarrow> a * c = b"
-proof -
- assume [simp]: "c \<noteq> 0"
- have "a = b / c \<longleftrightarrow> a * c = (b / c) * c" by simp
- also have "... \<longleftrightarrow> a * c = b" by (simp add: divide_inverse mult_assoc)
- finally show ?thesis .
-qed
-
-lemma nonzero_divide_eq_eq: "c \<noteq> 0 \<Longrightarrow> b / c = a \<longleftrightarrow> b = a * c"
-proof -
- assume [simp]: "c \<noteq> 0"
- have "b / c = a \<longleftrightarrow> (b / c) * c = a * c" by simp
- also have "... \<longleftrightarrow> b = a * c" by (simp add: divide_inverse mult_assoc)
- finally show ?thesis .
-qed
-
-lemma divide_eq_imp: "c \<noteq> 0 \<Longrightarrow> b = a * c \<Longrightarrow> b / c = a"
-by simp
-
-lemma eq_divide_imp: "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> a = b / c"
-by (erule subst, simp)
+ by (simp add: diff_divide_distrib)
lemmas field_eq_simps[no_atp] = algebra_simps
(* pull / out*)
@@ -189,9 +118,7 @@
diff_divide_eq_iff divide_diff_eq_iff
(* multiply eqn *)
nonzero_eq_divide_eq nonzero_divide_eq_eq
-(* is added later:
times_divide_eq_left times_divide_eq_right
-*)
text{*An example:*}
lemma "\<lbrakk>a\<noteq>b; c\<noteq>d; e\<noteq>f\<rbrakk> \<Longrightarrow> ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) = 1"
@@ -202,68 +129,21 @@
lemma diff_frac_eq:
"y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y - w / z = (x * z - w * y) / (y * z)"
-by (simp add: field_eq_simps times_divide_eq)
+ by (simp add: field_eq_simps times_divide_eq)
lemma frac_eq_eq:
"y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> (x / y = w / z) = (x * z = w * y)"
-by (simp add: field_eq_simps times_divide_eq)
+ by (simp add: field_eq_simps times_divide_eq)
end
-class division_by_zero = zero + inverse +
- assumes inverse_zero [simp]: "inverse 0 = 0"
-
-lemma divide_zero [simp]:
- "a / 0 = (0::'a::{field,division_by_zero})"
-by (simp add: divide_inverse)
-
-lemma divide_self_if [simp]:
- "a / (a::'a::{field,division_by_zero}) = (if a=0 then 0 else 1)"
-by simp
-
-class linordered_field = field + linordered_idom
-
-lemma inverse_nonzero_iff_nonzero [simp]:
- "(inverse a = 0) = (a = (0::'a::{division_ring,division_by_zero}))"
-by (force dest: inverse_zero_imp_zero)
-
-lemma inverse_minus_eq [simp]:
- "inverse(-a) = -inverse(a::'a::{division_ring,division_by_zero})"
-proof cases
- assume "a=0" thus ?thesis by simp
-next
- assume "a\<noteq>0"
- thus ?thesis by (simp add: nonzero_inverse_minus_eq)
-qed
-
-lemma inverse_eq_imp_eq:
- "inverse a = inverse b ==> a = (b::'a::{division_ring,division_by_zero})"
-apply (cases "a=0 | b=0")
- apply (force dest!: inverse_zero_imp_zero
- simp add: eq_commute [of "0::'a"])
-apply (force dest!: nonzero_inverse_eq_imp_eq)
-done
-
-lemma inverse_eq_iff_eq [simp]:
- "(inverse a = inverse b) = (a = (b::'a::{division_ring,division_by_zero}))"
-by (force dest!: inverse_eq_imp_eq)
-
-lemma inverse_inverse_eq [simp]:
- "inverse(inverse (a::'a::{division_ring,division_by_zero})) = a"
- proof cases
- assume "a=0" thus ?thesis by simp
- next
- assume "a\<noteq>0"
- thus ?thesis by (simp add: nonzero_inverse_inverse_eq)
- qed
-
text{*This version builds in division by zero while also re-orienting
the right-hand side.*}
lemma inverse_mult_distrib [simp]:
"inverse(a*b) = inverse(a) * inverse(b::'a::{field,division_by_zero})"
proof cases
assume "a \<noteq> 0 & b \<noteq> 0"
- thus ?thesis by (simp add: nonzero_inverse_mult_distrib mult_commute)
+ thus ?thesis by (simp add: nonzero_inverse_mult_distrib mult_ac)
next
assume "~ (a \<noteq> 0 & b \<noteq> 0)"
thus ?thesis by force
@@ -271,10 +151,10 @@
lemma inverse_divide [simp]:
"inverse (a/b) = b / (a::'a::{field,division_by_zero})"
-by (simp add: divide_inverse mult_commute)
+ by (simp add: divide_inverse mult_commute)
-subsection {* Calculations with fractions *}
+text {* Calculations with fractions *}
text{* There is a whole bunch of simp-rules just for class @{text
field} but none for class @{text field} and @{text nonzero_divides}
@@ -301,7 +181,7 @@
by (simp add: divide_inverse mult_assoc)
-subsubsection{*Special Cancellation Simprules for Division*}
+text {*Special Cancellation Simprules for Division*}
lemma mult_divide_mult_cancel_left_if[simp,no_atp]:
fixes c :: "'a :: {field,division_by_zero}"
@@ -309,7 +189,7 @@
by (simp add: mult_divide_mult_cancel_left)
-subsection {* Division and Unary Minus *}
+text {* Division and Unary Minus *}
lemma minus_divide_right: "- (a/b) = a / -(b::'a::{field,division_by_zero})"
by (simp add: divide_inverse)
@@ -332,40 +212,74 @@
"(b/c = (a::'a::{field,division_by_zero})) = (if c\<noteq>0 then b = a*c else a=0)"
by (force simp add: nonzero_divide_eq_eq)
+lemma inverse_eq_1_iff [simp]:
+ "(inverse x = 1) = (x = (1::'a::{field,division_by_zero}))"
+by (insert inverse_eq_iff_eq [of x 1], simp)
-subsection {* Ordered Fields *}
+lemma divide_eq_0_iff [simp,no_atp]:
+ "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))"
+by (simp add: divide_inverse)
+
+lemma divide_cancel_right [simp,no_atp]:
+ "(a/c = b/c) = (c = 0 | a = (b::'a::{field,division_by_zero}))"
+apply (cases "c=0", simp)
+apply (simp add: divide_inverse)
+done
+
+lemma divide_cancel_left [simp,no_atp]:
+ "(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_by_zero}))"
+apply (cases "c=0", simp)
+apply (simp add: divide_inverse)
+done
+
+lemma divide_eq_1_iff [simp,no_atp]:
+ "(a/b = 1) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
+apply (cases "b=0", simp)
+apply (simp add: right_inverse_eq)
+done
+
+lemma one_eq_divide_iff [simp,no_atp]:
+ "(1 = a/b) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
+by (simp add: eq_commute [of 1])
+
+
+text {* Ordered Fields *}
+
+class linordered_field = field + linordered_idom
+begin
lemma positive_imp_inverse_positive:
-assumes a_gt_0: "0 < a" shows "0 < inverse (a::'a::linordered_field)"
+ assumes a_gt_0: "0 < a"
+ shows "0 < inverse a"
proof -
have "0 < a * inverse a"
- by (simp add: a_gt_0 [THEN order_less_imp_not_eq2])
+ by (simp add: a_gt_0 [THEN less_imp_not_eq2])
thus "0 < inverse a"
- by (simp add: a_gt_0 [THEN order_less_not_sym] zero_less_mult_iff)
+ by (simp add: a_gt_0 [THEN less_not_sym] zero_less_mult_iff)
qed
lemma negative_imp_inverse_negative:
- "a < 0 ==> inverse a < (0::'a::linordered_field)"
-by (insert positive_imp_inverse_positive [of "-a"],
- simp add: nonzero_inverse_minus_eq order_less_imp_not_eq)
+ "a < 0 \<Longrightarrow> inverse a < 0"
+ by (insert positive_imp_inverse_positive [of "-a"],
+ simp add: nonzero_inverse_minus_eq less_imp_not_eq)
lemma inverse_le_imp_le:
-assumes invle: "inverse a \<le> inverse b" and apos: "0 < a"
-shows "b \<le> (a::'a::linordered_field)"
+ assumes invle: "inverse a \<le> inverse b" and apos: "0 < a"
+ shows "b \<le> a"
proof (rule classical)
assume "~ b \<le> a"
hence "a < b" by (simp add: linorder_not_le)
- hence bpos: "0 < b" by (blast intro: apos order_less_trans)
+ hence bpos: "0 < b" by (blast intro: apos less_trans)
hence "a * inverse a \<le> a * inverse b"
- by (simp add: apos invle order_less_imp_le mult_left_mono)
+ by (simp add: apos invle less_imp_le mult_left_mono)
hence "(a * inverse a) * b \<le> (a * inverse b) * b"
- by (simp add: bpos order_less_imp_le mult_right_mono)
- thus "b \<le> a" by (simp add: mult_assoc apos bpos order_less_imp_not_eq2)
+ by (simp add: bpos less_imp_le mult_right_mono)
+ thus "b \<le> a" by (simp add: mult_assoc apos bpos less_imp_not_eq2)
qed
lemma inverse_positive_imp_positive:
-assumes inv_gt_0: "0 < inverse a" and nz: "a \<noteq> 0"
-shows "0 < (a::'a::linordered_field)"
+ assumes inv_gt_0: "0 < inverse a" and nz: "a \<noteq> 0"
+ shows "0 < a"
proof -
have "0 < inverse (inverse a)"
using inv_gt_0 by (rule positive_imp_inverse_positive)
@@ -373,21 +287,397 @@
using nz by (simp add: nonzero_inverse_inverse_eq)
qed
+lemma inverse_negative_imp_negative:
+ assumes inv_less_0: "inverse a < 0" and nz: "a \<noteq> 0"
+ shows "a < 0"
+proof -
+ have "inverse (inverse a) < 0"
+ using inv_less_0 by (rule negative_imp_inverse_negative)
+ thus "a < 0" using nz by (simp add: nonzero_inverse_inverse_eq)
+qed
+
+lemma linordered_field_no_lb:
+ "\<forall>x. \<exists>y. y < x"
+proof
+ fix x::'a
+ have m1: "- (1::'a) < 0" by simp
+ from add_strict_right_mono[OF m1, where c=x]
+ have "(- 1) + x < x" by simp
+ thus "\<exists>y. y < x" by blast
+qed
+
+lemma linordered_field_no_ub:
+ "\<forall> x. \<exists>y. y > x"
+proof
+ fix x::'a
+ have m1: " (1::'a) > 0" by simp
+ from add_strict_right_mono[OF m1, where c=x]
+ have "1 + x > x" by simp
+ thus "\<exists>y. y > x" by blast
+qed
+
+lemma less_imp_inverse_less:
+ assumes less: "a < b" and apos: "0 < a"
+ shows "inverse b < inverse a"
+proof (rule ccontr)
+ assume "~ inverse b < inverse a"
+ hence "inverse a \<le> inverse b" by simp
+ hence "~ (a < b)"
+ by (simp add: not_less inverse_le_imp_le [OF _ apos])
+ thus False by (rule notE [OF _ less])
+qed
+
+lemma inverse_less_imp_less:
+ "inverse a < inverse b \<Longrightarrow> 0 < a \<Longrightarrow> b < a"
+apply (simp add: less_le [of "inverse a"] less_le [of "b"])
+apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq)
+done
+
+text{*Both premises are essential. Consider -1 and 1.*}
+lemma inverse_less_iff_less [simp,no_atp]:
+ "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> inverse a < inverse b \<longleftrightarrow> b < a"
+ by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less)
+
+lemma le_imp_inverse_le:
+ "a \<le> b \<Longrightarrow> 0 < a \<Longrightarrow> inverse b \<le> inverse a"
+ by (force simp add: le_less less_imp_inverse_less)
+
+lemma inverse_le_iff_le [simp,no_atp]:
+ "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> inverse a \<le> inverse b \<longleftrightarrow> b \<le> a"
+ by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le)
+
+
+text{*These results refer to both operands being negative. The opposite-sign
+case is trivial, since inverse preserves signs.*}
+lemma inverse_le_imp_le_neg:
+ "inverse a \<le> inverse b \<Longrightarrow> b < 0 \<Longrightarrow> b \<le> a"
+apply (rule classical)
+apply (subgoal_tac "a < 0")
+ prefer 2 apply force
+apply (insert inverse_le_imp_le [of "-b" "-a"])
+apply (simp add: nonzero_inverse_minus_eq)
+done
+
+lemma less_imp_inverse_less_neg:
+ "a < b \<Longrightarrow> b < 0 \<Longrightarrow> inverse b < inverse a"
+apply (subgoal_tac "a < 0")
+ prefer 2 apply (blast intro: less_trans)
+apply (insert less_imp_inverse_less [of "-b" "-a"])
+apply (simp add: nonzero_inverse_minus_eq)
+done
+
+lemma inverse_less_imp_less_neg:
+ "inverse a < inverse b \<Longrightarrow> b < 0 \<Longrightarrow> b < a"
+apply (rule classical)
+apply (subgoal_tac "a < 0")
+ prefer 2
+ apply force
+apply (insert inverse_less_imp_less [of "-b" "-a"])
+apply (simp add: nonzero_inverse_minus_eq)
+done
+
+lemma inverse_less_iff_less_neg [simp,no_atp]:
+ "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> inverse a < inverse b \<longleftrightarrow> b < a"
+apply (insert inverse_less_iff_less [of "-b" "-a"])
+apply (simp del: inverse_less_iff_less
+ add: nonzero_inverse_minus_eq)
+done
+
+lemma le_imp_inverse_le_neg:
+ "a \<le> b \<Longrightarrow> b < 0 ==> inverse b \<le> inverse a"
+ by (force simp add: le_less less_imp_inverse_less_neg)
+
+lemma inverse_le_iff_le_neg [simp,no_atp]:
+ "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> inverse a \<le> inverse b \<longleftrightarrow> b \<le> a"
+ by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg)
+
+lemma pos_le_divide_eq: "0 < c ==> (a \<le> b/c) = (a*c \<le> b)"
+proof -
+ assume less: "0<c"
+ hence "(a \<le> b/c) = (a*c \<le> (b/c)*c)"
+ by (simp add: mult_le_cancel_right less_not_sym [OF less])
+ also have "... = (a*c \<le> b)"
+ by (simp add: less_imp_not_eq2 [OF less] divide_inverse mult_assoc)
+ finally show ?thesis .
+qed
+
+lemma neg_le_divide_eq: "c < 0 ==> (a \<le> b/c) = (b \<le> a*c)"
+proof -
+ assume less: "c<0"
+ hence "(a \<le> b/c) = ((b/c)*c \<le> a*c)"
+ by (simp add: mult_le_cancel_right less_not_sym [OF less])
+ also have "... = (b \<le> a*c)"
+ by (simp add: less_imp_not_eq [OF less] divide_inverse mult_assoc)
+ finally show ?thesis .
+qed
+
+lemma pos_less_divide_eq:
+ "0 < c ==> (a < b/c) = (a*c < b)"
+proof -
+ assume less: "0<c"
+ hence "(a < b/c) = (a*c < (b/c)*c)"
+ by (simp add: mult_less_cancel_right_disj less_not_sym [OF less])
+ also have "... = (a*c < b)"
+ by (simp add: less_imp_not_eq2 [OF less] divide_inverse mult_assoc)
+ finally show ?thesis .
+qed
+
+lemma neg_less_divide_eq:
+ "c < 0 ==> (a < b/c) = (b < a*c)"
+proof -
+ assume less: "c<0"
+ hence "(a < b/c) = ((b/c)*c < a*c)"
+ by (simp add: mult_less_cancel_right_disj less_not_sym [OF less])
+ also have "... = (b < a*c)"
+ by (simp add: less_imp_not_eq [OF less] divide_inverse mult_assoc)
+ finally show ?thesis .
+qed
+
+lemma pos_divide_less_eq:
+ "0 < c ==> (b/c < a) = (b < a*c)"
+proof -
+ assume less: "0<c"
+ hence "(b/c < a) = ((b/c)*c < a*c)"
+ by (simp add: mult_less_cancel_right_disj less_not_sym [OF less])
+ also have "... = (b < a*c)"
+ by (simp add: less_imp_not_eq2 [OF less] divide_inverse mult_assoc)
+ finally show ?thesis .
+qed
+
+lemma neg_divide_less_eq:
+ "c < 0 ==> (b/c < a) = (a*c < b)"
+proof -
+ assume less: "c<0"
+ hence "(b/c < a) = (a*c < (b/c)*c)"
+ by (simp add: mult_less_cancel_right_disj less_not_sym [OF less])
+ also have "... = (a*c < b)"
+ by (simp add: less_imp_not_eq [OF less] divide_inverse mult_assoc)
+ finally show ?thesis .
+qed
+
+lemma pos_divide_le_eq: "0 < c ==> (b/c \<le> a) = (b \<le> a*c)"
+proof -
+ assume less: "0<c"
+ hence "(b/c \<le> a) = ((b/c)*c \<le> a*c)"
+ by (simp add: mult_le_cancel_right less_not_sym [OF less])
+ also have "... = (b \<le> a*c)"
+ by (simp add: less_imp_not_eq2 [OF less] divide_inverse mult_assoc)
+ finally show ?thesis .
+qed
+
+lemma neg_divide_le_eq: "c < 0 ==> (b/c \<le> a) = (a*c \<le> b)"
+proof -
+ assume less: "c<0"
+ hence "(b/c \<le> a) = (a*c \<le> (b/c)*c)"
+ by (simp add: mult_le_cancel_right less_not_sym [OF less])
+ also have "... = (a*c \<le> b)"
+ by (simp add: less_imp_not_eq [OF less] divide_inverse mult_assoc)
+ finally show ?thesis .
+qed
+
+text{* Lemmas @{text field_simps} multiply with denominators in in(equations)
+if they can be proved to be non-zero (for equations) or positive/negative
+(for inequations). Can be too aggressive and is therefore separate from the
+more benign @{text algebra_simps}. *}
+
+lemmas field_simps[no_atp] = field_eq_simps
+ (* multiply ineqn *)
+ pos_divide_less_eq neg_divide_less_eq
+ pos_less_divide_eq neg_less_divide_eq
+ pos_divide_le_eq neg_divide_le_eq
+ pos_le_divide_eq neg_le_divide_eq
+
+thm field_eq_simps
+
+text{* Lemmas @{text sign_simps} is a first attempt to automate proofs
+of positivity/negativity needed for @{text field_simps}. Have not added @{text
+sign_simps} to @{text field_simps} because the former can lead to case
+explosions. *}
+
+lemmas sign_simps[no_atp] = group_simps
+ zero_less_mult_iff mult_less_0_iff
+
+(* Only works once linear arithmetic is installed:
+text{*An example:*}
+lemma fixes a b c d e f :: "'a::linordered_field"
+shows "\<lbrakk>a>b; c<d; e<f; 0 < u \<rbrakk> \<Longrightarrow>
+ ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) <
+ ((e-f)*(a-b)*(c-d))/((e-f)*(a-b)*(c-d)) + u"
+apply(subgoal_tac "(c-d)*(e-f)*(a-b) > 0")
+ prefer 2 apply(simp add:sign_simps)
+apply(subgoal_tac "(c-d)*(e-f)*(a-b)*u > 0")
+ prefer 2 apply(simp add:sign_simps)
+apply(simp add:field_simps)
+done
+*)
+
+lemma divide_pos_pos:
+ "0 < x ==> 0 < y ==> 0 < x / y"
+by(simp add:field_simps)
+
+lemma divide_nonneg_pos:
+ "0 <= x ==> 0 < y ==> 0 <= x / y"
+by(simp add:field_simps)
+
+lemma divide_neg_pos:
+ "x < 0 ==> 0 < y ==> x / y < 0"
+by(simp add:field_simps)
+
+lemma divide_nonpos_pos:
+ "x <= 0 ==> 0 < y ==> x / y <= 0"
+by(simp add:field_simps)
+
+lemma divide_pos_neg:
+ "0 < x ==> y < 0 ==> x / y < 0"
+by(simp add:field_simps)
+
+lemma divide_nonneg_neg:
+ "0 <= x ==> y < 0 ==> x / y <= 0"
+by(simp add:field_simps)
+
+lemma divide_neg_neg:
+ "x < 0 ==> y < 0 ==> 0 < x / y"
+by(simp add:field_simps)
+
+lemma divide_nonpos_neg:
+ "x <= 0 ==> y < 0 ==> 0 <= x / y"
+by(simp add:field_simps)
+
+lemma divide_strict_right_mono:
+ "[|a < b; 0 < c|] ==> a / c < b / c"
+by (simp add: less_imp_not_eq2 divide_inverse mult_strict_right_mono
+ positive_imp_inverse_positive)
+
+
+lemma divide_strict_right_mono_neg:
+ "[|b < a; c < 0|] ==> a / c < b / c"
+apply (drule divide_strict_right_mono [of _ _ "-c"], simp)
+apply (simp add: less_imp_not_eq nonzero_minus_divide_right [symmetric])
+done
+
+text{*The last premise ensures that @{term a} and @{term b}
+ have the same sign*}
+lemma divide_strict_left_mono:
+ "[|b < a; 0 < c; 0 < a*b|] ==> c / a < c / b"
+by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono)
+
+lemma divide_left_mono:
+ "[|b \<le> a; 0 \<le> c; 0 < a*b|] ==> c / a \<le> c / b"
+by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_right_mono)
+
+lemma divide_strict_left_mono_neg:
+ "[|a < b; c < 0; 0 < a*b|] ==> c / a < c / b"
+by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono_neg)
+
+lemma mult_imp_div_pos_le: "0 < y ==> x <= z * y ==>
+ x / y <= z"
+by (subst pos_divide_le_eq, assumption+)
+
+lemma mult_imp_le_div_pos: "0 < y ==> z * y <= x ==>
+ z <= x / y"
+by(simp add:field_simps)
+
+lemma mult_imp_div_pos_less: "0 < y ==> x < z * y ==>
+ x / y < z"
+by(simp add:field_simps)
+
+lemma mult_imp_less_div_pos: "0 < y ==> z * y < x ==>
+ z < x / y"
+by(simp add:field_simps)
+
+lemma frac_le: "0 <= x ==>
+ x <= y ==> 0 < w ==> w <= z ==> x / z <= y / w"
+ apply (rule mult_imp_div_pos_le)
+ apply simp
+ apply (subst times_divide_eq_left)
+ apply (rule mult_imp_le_div_pos, assumption)
+ apply (rule mult_mono)
+ apply simp_all
+done
+
+lemma frac_less: "0 <= x ==>
+ x < y ==> 0 < w ==> w <= z ==> x / z < y / w"
+ apply (rule mult_imp_div_pos_less)
+ apply simp
+ apply (subst times_divide_eq_left)
+ apply (rule mult_imp_less_div_pos, assumption)
+ apply (erule mult_less_le_imp_less)
+ apply simp_all
+done
+
+lemma frac_less2: "0 < x ==>
+ x <= y ==> 0 < w ==> w < z ==> x / z < y / w"
+ apply (rule mult_imp_div_pos_less)
+ apply simp_all
+ apply (subst times_divide_eq_left)
+ apply (rule mult_imp_less_div_pos, assumption)
+ apply (erule mult_le_less_imp_less)
+ apply simp_all
+done
+
+text{*It's not obvious whether these should be simprules or not.
+ Their effect is to gather terms into one big fraction, like
+ a*b*c / x*y*z. The rationale for that is unclear, but many proofs
+ seem to need them.*}
+
+declare times_divide_eq [simp]
+
+lemma less_half_sum: "a < b ==> a < (a+b) / (1+1)"
+by (simp add: field_simps zero_less_two)
+
+lemma gt_half_sum: "a < b ==> (a+b)/(1+1) < b"
+by (simp add: field_simps zero_less_two)
+
+subclass dense_linorder
+proof
+ fix x y :: 'a
+ from less_add_one show "\<exists>y. x < y" ..
+ from less_add_one have "x + (- 1) < (x + 1) + (- 1)" by (rule add_strict_right_mono)
+ then have "x - 1 < x + 1 - 1" by (simp only: diff_minus [symmetric])
+ then have "x - 1 < x" by (simp add: algebra_simps)
+ then show "\<exists>y. y < x" ..
+ show "x < y \<Longrightarrow> \<exists>z>x. z < y" by (blast intro!: less_half_sum gt_half_sum)
+qed
+
+lemma nonzero_abs_inverse:
+ "a \<noteq> 0 ==> \<bar>inverse a\<bar> = inverse \<bar>a\<bar>"
+apply (auto simp add: neq_iff abs_if nonzero_inverse_minus_eq
+ negative_imp_inverse_negative)
+apply (blast intro: positive_imp_inverse_positive elim: less_asym)
+done
+
+lemma nonzero_abs_divide:
+ "b \<noteq> 0 ==> \<bar>a / b\<bar> = \<bar>a\<bar> / \<bar>b\<bar>"
+ by (simp add: divide_inverse abs_mult nonzero_abs_inverse)
+
+lemma field_le_epsilon:
+ assumes e: "\<And>e. 0 < e \<Longrightarrow> x \<le> y + e"
+ shows "x \<le> y"
+proof (rule dense_le)
+ fix t assume "t < x"
+ hence "0 < x - t" by (simp add: less_diff_eq)
+ from e [OF this] have "x + 0 \<le> x + (y - t)" by (simp add: algebra_simps)
+ then have "0 \<le> y - t" by (simp only: add_le_cancel_left)
+ then show "t \<le> y" by (simp add: algebra_simps)
+qed
+
+end
+
+lemma le_divide_eq:
+ "(a \<le> b/c) =
+ (if 0 < c then a*c \<le> b
+ else if c < 0 then b \<le> a*c
+ else a \<le> (0::'a::{linordered_field,division_by_zero}))"
+apply (cases "c=0", simp)
+apply (force simp add: pos_le_divide_eq neg_le_divide_eq linorder_neq_iff)
+done
+
lemma inverse_positive_iff_positive [simp]:
"(0 < inverse a) = (0 < (a::'a::{linordered_field,division_by_zero}))"
apply (cases "a = 0", simp)
apply (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive)
done
-lemma inverse_negative_imp_negative:
-assumes inv_less_0: "inverse a < 0" and nz: "a \<noteq> 0"
-shows "a < (0::'a::linordered_field)"
-proof -
- have "inverse (inverse a) < 0"
- using inv_less_0 by (rule negative_imp_inverse_negative)
- thus "a < 0" using nz by (simp add: nonzero_inverse_inverse_eq)
-qed
-
lemma inverse_negative_iff_negative [simp]:
"(inverse a < 0) = (a < (0::'a::{linordered_field,division_by_zero}))"
apply (cases "a = 0", simp)
@@ -402,104 +692,6 @@
"(inverse a \<le> 0) = (a \<le> (0::'a::{linordered_field,division_by_zero}))"
by (simp add: linorder_not_less [symmetric])
-lemma linordered_field_no_lb: "\<forall> x. \<exists>y. y < (x::'a::linordered_field)"
-proof
- fix x::'a
- have m1: "- (1::'a) < 0" by simp
- from add_strict_right_mono[OF m1, where c=x]
- have "(- 1) + x < x" by simp
- thus "\<exists>y. y < x" by blast
-qed
-
-lemma linordered_field_no_ub: "\<forall> x. \<exists>y. y > (x::'a::linordered_field)"
-proof
- fix x::'a
- have m1: " (1::'a) > 0" by simp
- from add_strict_right_mono[OF m1, where c=x]
- have "1 + x > x" by simp
- thus "\<exists>y. y > x" by blast
-qed
-
-subsection{*Anti-Monotonicity of @{term inverse}*}
-
-lemma less_imp_inverse_less:
-assumes less: "a < b" and apos: "0 < a"
-shows "inverse b < inverse (a::'a::linordered_field)"
-proof (rule ccontr)
- assume "~ inverse b < inverse a"
- hence "inverse a \<le> inverse b" by (simp add: linorder_not_less)
- hence "~ (a < b)"
- by (simp add: linorder_not_less inverse_le_imp_le [OF _ apos])
- thus False by (rule notE [OF _ less])
-qed
-
-lemma inverse_less_imp_less:
- "[|inverse a < inverse b; 0 < a|] ==> b < (a::'a::linordered_field)"
-apply (simp add: order_less_le [of "inverse a"] order_less_le [of "b"])
-apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq)
-done
-
-text{*Both premises are essential. Consider -1 and 1.*}
-lemma inverse_less_iff_less [simp,no_atp]:
- "[|0 < a; 0 < b|] ==> (inverse a < inverse b) = (b < (a::'a::linordered_field))"
-by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less)
-
-lemma le_imp_inverse_le:
- "[|a \<le> b; 0 < a|] ==> inverse b \<le> inverse (a::'a::linordered_field)"
-by (force simp add: order_le_less less_imp_inverse_less)
-
-lemma inverse_le_iff_le [simp,no_atp]:
- "[|0 < a; 0 < b|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::linordered_field))"
-by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le)
-
-
-text{*These results refer to both operands being negative. The opposite-sign
-case is trivial, since inverse preserves signs.*}
-lemma inverse_le_imp_le_neg:
- "[|inverse a \<le> inverse b; b < 0|] ==> b \<le> (a::'a::linordered_field)"
-apply (rule classical)
-apply (subgoal_tac "a < 0")
- prefer 2 apply (force simp add: linorder_not_le intro: order_less_trans)
-apply (insert inverse_le_imp_le [of "-b" "-a"])
-apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)
-done
-
-lemma less_imp_inverse_less_neg:
- "[|a < b; b < 0|] ==> inverse b < inverse (a::'a::linordered_field)"
-apply (subgoal_tac "a < 0")
- prefer 2 apply (blast intro: order_less_trans)
-apply (insert less_imp_inverse_less [of "-b" "-a"])
-apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)
-done
-
-lemma inverse_less_imp_less_neg:
- "[|inverse a < inverse b; b < 0|] ==> b < (a::'a::linordered_field)"
-apply (rule classical)
-apply (subgoal_tac "a < 0")
- prefer 2
- apply (force simp add: linorder_not_less intro: order_le_less_trans)
-apply (insert inverse_less_imp_less [of "-b" "-a"])
-apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq)
-done
-
-lemma inverse_less_iff_less_neg [simp,no_atp]:
- "[|a < 0; b < 0|] ==> (inverse a < inverse b) = (b < (a::'a::linordered_field))"
-apply (insert inverse_less_iff_less [of "-b" "-a"])
-apply (simp del: inverse_less_iff_less
- add: order_less_imp_not_eq nonzero_inverse_minus_eq)
-done
-
-lemma le_imp_inverse_le_neg:
- "[|a \<le> b; b < 0|] ==> inverse b \<le> inverse (a::'a::linordered_field)"
-by (force simp add: order_le_less less_imp_inverse_less_neg)
-
-lemma inverse_le_iff_le_neg [simp,no_atp]:
- "[|a < 0; b < 0|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::linordered_field))"
-by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg)
-
-
-subsection{*Inverses and the Number One*}
-
lemma one_less_inverse_iff:
"(1 < inverse x) = (0 < x & x < (1::'a::{linordered_field,division_by_zero}))"
proof cases
@@ -518,10 +710,6 @@
with notless show ?thesis by simp
qed
-lemma inverse_eq_1_iff [simp]:
- "(inverse x = 1) = (x = (1::'a::{field,division_by_zero}))"
-by (insert inverse_eq_iff_eq [of x 1], simp)
-
lemma one_le_inverse_iff:
"(1 \<le> inverse x) = (0 < x & x \<le> (1::'a::{linordered_field,division_by_zero}))"
by (force simp add: order_le_less one_less_inverse_iff)
@@ -534,58 +722,6 @@
"(inverse x \<le> 1) = (x \<le> 0 | 1 \<le> (x::'a::{linordered_field,division_by_zero}))"
by (simp add: linorder_not_less [symmetric] one_less_inverse_iff)
-
-subsection{*Simplification of Inequalities Involving Literal Divisors*}
-
-lemma pos_le_divide_eq: "0 < (c::'a::linordered_field) ==> (a \<le> b/c) = (a*c \<le> b)"
-proof -
- assume less: "0<c"
- hence "(a \<le> b/c) = (a*c \<le> (b/c)*c)"
- by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
- also have "... = (a*c \<le> b)"
- by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc)
- finally show ?thesis .
-qed
-
-lemma neg_le_divide_eq: "c < (0::'a::linordered_field) ==> (a \<le> b/c) = (b \<le> a*c)"
-proof -
- assume less: "c<0"
- hence "(a \<le> b/c) = ((b/c)*c \<le> a*c)"
- by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
- also have "... = (b \<le> a*c)"
- by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc)
- finally show ?thesis .
-qed
-
-lemma le_divide_eq:
- "(a \<le> b/c) =
- (if 0 < c then a*c \<le> b
- else if c < 0 then b \<le> a*c
- else a \<le> (0::'a::{linordered_field,division_by_zero}))"
-apply (cases "c=0", simp)
-apply (force simp add: pos_le_divide_eq neg_le_divide_eq linorder_neq_iff)
-done
-
-lemma pos_divide_le_eq: "0 < (c::'a::linordered_field) ==> (b/c \<le> a) = (b \<le> a*c)"
-proof -
- assume less: "0<c"
- hence "(b/c \<le> a) = ((b/c)*c \<le> a*c)"
- by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
- also have "... = (b \<le> a*c)"
- by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc)
- finally show ?thesis .
-qed
-
-lemma neg_divide_le_eq: "c < (0::'a::linordered_field) ==> (b/c \<le> a) = (a*c \<le> b)"
-proof -
- assume less: "c<0"
- hence "(b/c \<le> a) = (a*c \<le> (b/c)*c)"
- by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
- also have "... = (a*c \<le> b)"
- by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc)
- finally show ?thesis .
-qed
-
lemma divide_le_eq:
"(b/c \<le> a) =
(if 0 < c then b \<le> a*c
@@ -595,28 +731,6 @@
apply (force simp add: pos_divide_le_eq neg_divide_le_eq linorder_neq_iff)
done
-lemma pos_less_divide_eq:
- "0 < (c::'a::linordered_field) ==> (a < b/c) = (a*c < b)"
-proof -
- assume less: "0<c"
- hence "(a < b/c) = (a*c < (b/c)*c)"
- by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
- also have "... = (a*c < b)"
- by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc)
- finally show ?thesis .
-qed
-
-lemma neg_less_divide_eq:
- "c < (0::'a::linordered_field) ==> (a < b/c) = (b < a*c)"
-proof -
- assume less: "c<0"
- hence "(a < b/c) = ((b/c)*c < a*c)"
- by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
- also have "... = (b < a*c)"
- by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc)
- finally show ?thesis .
-qed
-
lemma less_divide_eq:
"(a < b/c) =
(if 0 < c then a*c < b
@@ -626,28 +740,6 @@
apply (force simp add: pos_less_divide_eq neg_less_divide_eq linorder_neq_iff)
done
-lemma pos_divide_less_eq:
- "0 < (c::'a::linordered_field) ==> (b/c < a) = (b < a*c)"
-proof -
- assume less: "0<c"
- hence "(b/c < a) = ((b/c)*c < a*c)"
- by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
- also have "... = (b < a*c)"
- by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc)
- finally show ?thesis .
-qed
-
-lemma neg_divide_less_eq:
- "c < (0::'a::linordered_field) ==> (b/c < a) = (a*c < b)"
-proof -
- assume less: "c<0"
- hence "(b/c < a) = (a*c < (b/c)*c)"
- by (simp add: mult_less_cancel_right_disj order_less_not_sym [OF less])
- also have "... = (a*c < b)"
- by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc)
- finally show ?thesis .
-qed
-
lemma divide_less_eq:
"(b/c < a) =
(if 0 < c then b < a*c
@@ -657,45 +749,7 @@
apply (force simp add: pos_divide_less_eq neg_divide_less_eq linorder_neq_iff)
done
-
-subsection{*Field simplification*}
-
-text{* Lemmas @{text field_simps} multiply with denominators in in(equations)
-if they can be proved to be non-zero (for equations) or positive/negative
-(for inequations). Can be too aggressive and is therefore separate from the
-more benign @{text algebra_simps}. *}
-
-lemmas field_simps[no_atp] = field_eq_simps
- (* multiply ineqn *)
- pos_divide_less_eq neg_divide_less_eq
- pos_less_divide_eq neg_less_divide_eq
- pos_divide_le_eq neg_divide_le_eq
- pos_le_divide_eq neg_le_divide_eq
-
-text{* Lemmas @{text sign_simps} is a first attempt to automate proofs
-of positivity/negativity needed for @{text field_simps}. Have not added @{text
-sign_simps} to @{text field_simps} because the former can lead to case
-explosions. *}
-
-lemmas sign_simps[no_atp] = group_simps
- zero_less_mult_iff mult_less_0_iff
-
-(* Only works once linear arithmetic is installed:
-text{*An example:*}
-lemma fixes a b c d e f :: "'a::linordered_field"
-shows "\<lbrakk>a>b; c<d; e<f; 0 < u \<rbrakk> \<Longrightarrow>
- ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) <
- ((e-f)*(a-b)*(c-d))/((e-f)*(a-b)*(c-d)) + u"
-apply(subgoal_tac "(c-d)*(e-f)*(a-b) > 0")
- prefer 2 apply(simp add:sign_simps)
-apply(subgoal_tac "(c-d)*(e-f)*(a-b)*u > 0")
- prefer 2 apply(simp add:sign_simps)
-apply(simp add:field_simps)
-done
-*)
-
-
-subsection{*Division and Signs*}
+text {*Division and Signs*}
lemma zero_less_divide_iff:
"((0::'a::{linordered_field,division_by_zero}) < a/b) = (0 < a & 0 < b | a < 0 & b < 0)"
@@ -716,71 +770,9 @@
(0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"
by (simp add: divide_inverse mult_le_0_iff)
-lemma divide_eq_0_iff [simp,no_atp]:
- "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))"
-by (simp add: divide_inverse)
-
-lemma divide_pos_pos:
- "0 < (x::'a::linordered_field) ==> 0 < y ==> 0 < x / y"
-by(simp add:field_simps)
-
-
-lemma divide_nonneg_pos:
- "0 <= (x::'a::linordered_field) ==> 0 < y ==> 0 <= x / y"
-by(simp add:field_simps)
-
-lemma divide_neg_pos:
- "(x::'a::linordered_field) < 0 ==> 0 < y ==> x / y < 0"
-by(simp add:field_simps)
-
-lemma divide_nonpos_pos:
- "(x::'a::linordered_field) <= 0 ==> 0 < y ==> x / y <= 0"
-by(simp add:field_simps)
-
-lemma divide_pos_neg:
- "0 < (x::'a::linordered_field) ==> y < 0 ==> x / y < 0"
-by(simp add:field_simps)
-
-lemma divide_nonneg_neg:
- "0 <= (x::'a::linordered_field) ==> y < 0 ==> x / y <= 0"
-by(simp add:field_simps)
-
-lemma divide_neg_neg:
- "(x::'a::linordered_field) < 0 ==> y < 0 ==> 0 < x / y"
-by(simp add:field_simps)
-
-lemma divide_nonpos_neg:
- "(x::'a::linordered_field) <= 0 ==> y < 0 ==> 0 <= x / y"
-by(simp add:field_simps)
-
-
-subsection{*Cancellation Laws for Division*}
-
-lemma divide_cancel_right [simp,no_atp]:
- "(a/c = b/c) = (c = 0 | a = (b::'a::{field,division_by_zero}))"
-apply (cases "c=0", simp)
-apply (simp add: divide_inverse)
-done
-
-lemma divide_cancel_left [simp,no_atp]:
- "(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_by_zero}))"
-apply (cases "c=0", simp)
-apply (simp add: divide_inverse)
-done
-
-
-subsection {* Division and the Number One *}
+text {* Division and the Number One *}
text{*Simplify expressions equated with 1*}
-lemma divide_eq_1_iff [simp,no_atp]:
- "(a/b = 1) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
-apply (cases "b=0", simp)
-apply (simp add: right_inverse_eq)
-done
-
-lemma one_eq_divide_iff [simp,no_atp]:
- "(1 = a/b) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
-by (simp add: eq_commute [of 1])
lemma zero_eq_1_divide_iff [simp,no_atp]:
"((0::'a::{linordered_field,division_by_zero}) = 1/a) = (a = 0)"
@@ -806,49 +798,22 @@
declare zero_le_divide_1_iff [simp,no_atp]
declare divide_le_0_1_iff [simp,no_atp]
-
-subsection {* Ordering Rules for Division *}
-
-lemma divide_strict_right_mono:
- "[|a < b; 0 < c|] ==> a / c < b / (c::'a::linordered_field)"
-by (simp add: order_less_imp_not_eq2 divide_inverse mult_strict_right_mono
- positive_imp_inverse_positive)
-
lemma divide_right_mono:
"[|a \<le> b; 0 \<le> c|] ==> a/c \<le> b/(c::'a::{linordered_field,division_by_zero})"
by (force simp add: divide_strict_right_mono order_le_less)
-lemma divide_right_mono_neg: "(a::'a::{division_by_zero,linordered_field}) <= b
+lemma divide_right_mono_neg: "(a::'a::{linordered_field,division_by_zero}) <= b
==> c <= 0 ==> b / c <= a / c"
apply (drule divide_right_mono [of _ _ "- c"])
apply auto
done
-lemma divide_strict_right_mono_neg:
- "[|b < a; c < 0|] ==> a / c < b / (c::'a::linordered_field)"
-apply (drule divide_strict_right_mono [of _ _ "-c"], simp)
-apply (simp add: order_less_imp_not_eq nonzero_minus_divide_right [symmetric])
-done
-
-text{*The last premise ensures that @{term a} and @{term b}
- have the same sign*}
-lemma divide_strict_left_mono:
- "[|b < a; 0 < c; 0 < a*b|] ==> c / a < c / (b::'a::linordered_field)"
-by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono)
-
-lemma divide_left_mono:
- "[|b \<le> a; 0 \<le> c; 0 < a*b|] ==> c / a \<le> c / (b::'a::linordered_field)"
-by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_right_mono)
-
-lemma divide_left_mono_neg: "(a::'a::{division_by_zero,linordered_field}) <= b
+lemma divide_left_mono_neg: "(a::'a::{linordered_field,division_by_zero}) <= b
==> c <= 0 ==> 0 < a * b ==> c / a <= c / b"
apply (drule divide_left_mono [of _ _ "- c"])
apply (auto simp add: mult_commute)
done
-lemma divide_strict_left_mono_neg:
- "[|a < b; c < 0; 0 < a*b|] ==> c / a < c / (b::'a::linordered_field)"
-by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono_neg)
text{*Simplify quotients that are compared with the value 1.*}
@@ -874,7 +839,7 @@
by (auto simp add: divide_less_eq)
-subsection{*Conditional Simplification Rules: No Case Splits*}
+text {*Conditional Simplification Rules: No Case Splits*}
lemma le_divide_eq_1_pos [simp,no_atp]:
fixes a :: "'a :: {linordered_field,division_by_zero}"
@@ -926,125 +891,25 @@
shows "(b/a = 1) = ((a \<noteq> 0 & a = b))"
by (auto simp add: divide_eq_eq)
-
-subsection {* Reasoning about inequalities with division *}
-
-lemma mult_imp_div_pos_le: "0 < (y::'a::linordered_field) ==> x <= z * y ==>
- x / y <= z"
-by (subst pos_divide_le_eq, assumption+)
-
-lemma mult_imp_le_div_pos: "0 < (y::'a::linordered_field) ==> z * y <= x ==>
- z <= x / y"
-by(simp add:field_simps)
-
-lemma mult_imp_div_pos_less: "0 < (y::'a::linordered_field) ==> x < z * y ==>
- x / y < z"
-by(simp add:field_simps)
-
-lemma mult_imp_less_div_pos: "0 < (y::'a::linordered_field) ==> z * y < x ==>
- z < x / y"
-by(simp add:field_simps)
-
-lemma frac_le: "(0::'a::linordered_field) <= x ==>
- x <= y ==> 0 < w ==> w <= z ==> x / z <= y / w"
- apply (rule mult_imp_div_pos_le)
- apply simp
- apply (subst times_divide_eq_left)
- apply (rule mult_imp_le_div_pos, assumption)
- apply (rule mult_mono)
- apply simp_all
-done
-
-lemma frac_less: "(0::'a::linordered_field) <= x ==>
- x < y ==> 0 < w ==> w <= z ==> x / z < y / w"
- apply (rule mult_imp_div_pos_less)
- apply simp
- apply (subst times_divide_eq_left)
- apply (rule mult_imp_less_div_pos, assumption)
- apply (erule mult_less_le_imp_less)
- apply simp_all
-done
-
-lemma frac_less2: "(0::'a::linordered_field) < x ==>
- x <= y ==> 0 < w ==> w < z ==> x / z < y / w"
- apply (rule mult_imp_div_pos_less)
- apply simp_all
- apply (subst times_divide_eq_left)
- apply (rule mult_imp_less_div_pos, assumption)
- apply (erule mult_le_less_imp_less)
- apply simp_all
-done
-
-text{*It's not obvious whether these should be simprules or not.
- Their effect is to gather terms into one big fraction, like
- a*b*c / x*y*z. The rationale for that is unclear, but many proofs
- seem to need them.*}
-
-declare times_divide_eq [simp]
-
-
-subsection {* Ordered Fields are Dense *}
-
-lemma less_half_sum: "a < b ==> a < (a+b) / (1+1::'a::linordered_field)"
-by (simp add: field_simps zero_less_two)
-
-lemma gt_half_sum: "a < b ==> (a+b)/(1+1::'a::linordered_field) < b"
-by (simp add: field_simps zero_less_two)
-
-instance linordered_field < dense_linorder
-proof
- fix x y :: 'a
- have "x < x + 1" by simp
- then show "\<exists>y. x < y" ..
- have "x - 1 < x" by simp
- then show "\<exists>y. y < x" ..
- show "x < y \<Longrightarrow> \<exists>z>x. z < y" by (blast intro!: less_half_sum gt_half_sum)
-qed
-
-
-subsection {* Absolute Value *}
-
-lemma nonzero_abs_inverse:
- "a \<noteq> 0 ==> abs (inverse (a::'a::linordered_field)) = inverse (abs a)"
-apply (auto simp add: linorder_neq_iff abs_if nonzero_inverse_minus_eq
- negative_imp_inverse_negative)
-apply (blast intro: positive_imp_inverse_positive elim: order_less_asym)
-done
-
lemma abs_inverse [simp]:
- "abs (inverse (a::'a::{linordered_field,division_by_zero})) =
- inverse (abs a)"
+ "\<bar>inverse (a::'a::{linordered_field,division_by_zero})\<bar> =
+ inverse \<bar>a\<bar>"
apply (cases "a=0", simp)
apply (simp add: nonzero_abs_inverse)
done
-lemma nonzero_abs_divide:
- "b \<noteq> 0 ==> abs (a / (b::'a::linordered_field)) = abs a / abs b"
-by (simp add: divide_inverse abs_mult nonzero_abs_inverse)
-
lemma abs_divide [simp]:
- "abs (a / (b::'a::{linordered_field,division_by_zero})) = abs a / abs b"
+ "\<bar>a / (b::'a::{linordered_field,division_by_zero})\<bar> = \<bar>a\<bar> / \<bar>b\<bar>"
apply (cases "b=0", simp)
apply (simp add: nonzero_abs_divide)
done
-lemma abs_div_pos: "(0::'a::{division_by_zero,linordered_field}) < y ==>
- abs x / y = abs (x / y)"
+lemma abs_div_pos: "(0::'a::{linordered_field,division_by_zero}) < y ==>
+ \<bar>x\<bar> / y = \<bar>x / y\<bar>"
apply (subst abs_divide)
apply (simp add: order_less_imp_le)
done
-lemma field_le_epsilon:
- fixes x y :: "'a\<Colon>linordered_field"
- assumes e: "\<And>e. 0 < e \<Longrightarrow> x \<le> y + e"
- shows "x \<le> y"
-proof (rule dense_le)
- fix t assume "t < x"
- hence "0 < x - t" by (simp add: less_diff_eq)
- from e[OF this]
- show "t \<le> y" by (simp add: field_simps)
-qed
-
lemma field_le_mult_one_interval:
fixes x :: "'a\<Colon>{linordered_field,division_by_zero}"
assumes *: "\<And>z. \<lbrakk> 0 < z ; z < 1 \<rbrakk> \<Longrightarrow> z * x \<le> y"
--- a/src/HOL/Rings.thy Fri Apr 23 13:58:14 2010 +0200
+++ b/src/HOL/Rings.thy Fri Apr 23 13:58:14 2010 +0200
@@ -487,6 +487,125 @@
"a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a - inverse b = inverse a * (b - a) * inverse b"
by (simp add: algebra_simps)
+lemma right_inverse_eq: "b \<noteq> 0 \<Longrightarrow> a / b = 1 \<longleftrightarrow> a = b"
+proof
+ assume neq: "b \<noteq> 0"
+ {
+ hence "a = (a / b) * b" by (simp add: divide_inverse mult_assoc)
+ also assume "a / b = 1"
+ finally show "a = b" by simp
+ next
+ assume "a = b"
+ with neq show "a / b = 1" by (simp add: divide_inverse)
+ }
+qed
+
+lemma nonzero_inverse_eq_divide: "a \<noteq> 0 \<Longrightarrow> inverse a = 1 / a"
+by (simp add: divide_inverse)
+
+lemma divide_self [simp]: "a \<noteq> 0 \<Longrightarrow> a / a = 1"
+by (simp add: divide_inverse)
+
+lemma divide_zero_left [simp]: "0 / a = 0"
+by (simp add: divide_inverse)
+
+lemma inverse_eq_divide: "inverse a = 1 / a"
+by (simp add: divide_inverse)
+
+lemma add_divide_distrib: "(a+b) / c = a/c + b/c"
+by (simp add: divide_inverse algebra_simps)
+
+lemma divide_1 [simp]: "a / 1 = a"
+ by (simp add: divide_inverse)
+
+lemma times_divide_eq_right: "a * (b / c) = (a * b) / c"
+ by (simp add: divide_inverse mult_assoc)
+
+lemma minus_divide_left: "- (a / b) = (-a) / b"
+ by (simp add: divide_inverse)
+
+lemma nonzero_minus_divide_right: "b \<noteq> 0 ==> - (a / b) = a / (- b)"
+ by (simp add: divide_inverse nonzero_inverse_minus_eq)
+
+lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (-a) / (-b) = a / b"
+ by (simp add: divide_inverse nonzero_inverse_minus_eq)
+
+lemma divide_minus_left [simp, no_atp]: "(-a) / b = - (a / b)"
+ by (simp add: divide_inverse)
+
+lemma diff_divide_distrib: "(a - b) / c = a / c - b / c"
+ by (simp add: diff_minus add_divide_distrib)
+
+lemma nonzero_eq_divide_eq: "c \<noteq> 0 \<Longrightarrow> a = b / c \<longleftrightarrow> a * c = b"
+proof -
+ assume [simp]: "c \<noteq> 0"
+ have "a = b / c \<longleftrightarrow> a * c = (b / c) * c" by simp
+ also have "... \<longleftrightarrow> a * c = b" by (simp add: divide_inverse mult_assoc)
+ finally show ?thesis .
+qed
+
+lemma nonzero_divide_eq_eq: "c \<noteq> 0 \<Longrightarrow> b / c = a \<longleftrightarrow> b = a * c"
+proof -
+ assume [simp]: "c \<noteq> 0"
+ have "b / c = a \<longleftrightarrow> (b / c) * c = a * c" by simp
+ also have "... \<longleftrightarrow> b = a * c" by (simp add: divide_inverse mult_assoc)
+ finally show ?thesis .
+qed
+
+lemma divide_eq_imp: "c \<noteq> 0 \<Longrightarrow> b = a * c \<Longrightarrow> b / c = a"
+ by (simp add: divide_inverse mult_assoc)
+
+lemma eq_divide_imp: "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> a = b / c"
+ by (drule sym) (simp add: divide_inverse mult_assoc)
+
+end
+
+class division_by_zero = division_ring +
+ assumes inverse_zero [simp]: "inverse 0 = 0"
+begin
+
+lemma divide_zero [simp]:
+ "a / 0 = 0"
+ by (simp add: divide_inverse)
+
+lemma divide_self_if [simp]:
+ "a / a = (if a = 0 then 0 else 1)"
+ by simp
+
+lemma inverse_nonzero_iff_nonzero [simp]:
+ "inverse a = 0 \<longleftrightarrow> a = 0"
+ by rule (fact inverse_zero_imp_zero, simp)
+
+lemma inverse_minus_eq [simp]:
+ "inverse (- a) = - inverse a"
+proof cases
+ assume "a=0" thus ?thesis by simp
+next
+ assume "a\<noteq>0"
+ thus ?thesis by (simp add: nonzero_inverse_minus_eq)
+qed
+
+lemma inverse_eq_imp_eq:
+ "inverse a = inverse b \<Longrightarrow> a = b"
+apply (cases "a=0 | b=0")
+ apply (force dest!: inverse_zero_imp_zero
+ simp add: eq_commute [of "0::'a"])
+apply (force dest!: nonzero_inverse_eq_imp_eq)
+done
+
+lemma inverse_eq_iff_eq [simp]:
+ "inverse a = inverse b \<longleftrightarrow> a = b"
+ by (force dest!: inverse_eq_imp_eq)
+
+lemma inverse_inverse_eq [simp]:
+ "inverse (inverse a) = a"
+proof cases
+ assume "a=0" thus ?thesis by simp
+next
+ assume "a\<noteq>0"
+ thus ?thesis by (simp add: nonzero_inverse_inverse_eq)
+qed
+
end
class mult_mono = times + zero + ord +
@@ -533,17 +652,17 @@
subclass ordered_semiring ..
lemma mult_nonneg_nonneg: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"
-using mult_left_mono [of zero b a] by simp
+using mult_left_mono [of 0 b a] by simp
lemma mult_nonneg_nonpos: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> a * b \<le> 0"
-using mult_left_mono [of b zero a] by simp
+using mult_left_mono [of b 0 a] by simp
lemma mult_nonpos_nonneg: "a \<le> 0 \<Longrightarrow> 0 \<le> b \<Longrightarrow> a * b \<le> 0"
-using mult_right_mono [of a zero b] by simp
+using mult_right_mono [of a 0 b] by simp
text {* Legacy - use @{text mult_nonpos_nonneg} *}
lemma mult_nonneg_nonpos2: "0 \<le> a \<Longrightarrow> b \<le> 0 \<Longrightarrow> b * a \<le> 0"
-by (drule mult_right_mono [of b zero], auto)
+by (drule mult_right_mono [of b 0], auto)
lemma split_mult_neg_le: "(0 \<le> a & b \<le> 0) | (a \<le> 0 & 0 \<le> b) \<Longrightarrow> a * b \<le> 0"
by (auto simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)
@@ -597,17 +716,17 @@
by (force simp add: mult_strict_right_mono not_less [symmetric])
lemma mult_pos_pos: "0 < a \<Longrightarrow> 0 < b \<Longrightarrow> 0 < a * b"
-using mult_strict_left_mono [of zero b a] by simp
+using mult_strict_left_mono [of 0 b a] by simp
lemma mult_pos_neg: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> a * b < 0"
-using mult_strict_left_mono [of b zero a] by simp
+using mult_strict_left_mono [of b 0 a] by simp
lemma mult_neg_pos: "a < 0 \<Longrightarrow> 0 < b \<Longrightarrow> a * b < 0"
-using mult_strict_right_mono [of a zero b] by simp
+using mult_strict_right_mono [of a 0 b] by simp
text {* Legacy - use @{text mult_neg_pos} *}
lemma mult_pos_neg2: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0"
-by (drule mult_strict_right_mono [of b zero], auto)
+by (drule mult_strict_right_mono [of b 0], auto)
lemma zero_less_mult_pos:
"0 < a * b \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
@@ -763,18 +882,18 @@
lemma mult_left_mono_neg:
"b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> c * a \<le> c * b"
- apply (drule mult_left_mono [of _ _ "uminus c"])
+ apply (drule mult_left_mono [of _ _ "- c"])
apply simp_all
done
lemma mult_right_mono_neg:
"b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> a * c \<le> b * c"
- apply (drule mult_right_mono [of _ _ "uminus c"])
+ apply (drule mult_right_mono [of _ _ "- c"])
apply simp_all
done
lemma mult_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a * b"
-using mult_right_mono_neg [of a zero b] by simp
+using mult_right_mono_neg [of a 0 b] by simp
lemma split_mult_pos_le:
"(0 \<le> a \<and> 0 \<le> b) \<or> (a \<le> 0 \<and> b \<le> 0) \<Longrightarrow> 0 \<le> a * b"
@@ -821,7 +940,7 @@
using mult_strict_right_mono [of b a "- c"] by simp
lemma mult_neg_neg: "a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> 0 < a * b"
-using mult_strict_right_mono_neg [of a zero b] by simp
+using mult_strict_right_mono_neg [of a 0 b] by simp
subclass ring_no_zero_divisors
proof
@@ -973,7 +1092,7 @@
lemma pos_add_strict:
shows "0 < a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
- using add_strict_mono [of zero a b c] by simp
+ using add_strict_mono [of 0 a b c] by simp
lemma zero_le_one [simp]: "0 \<le> 1"
by (rule zero_less_one [THEN less_imp_le])
@@ -1074,7 +1193,7 @@
"sgn (a * b) = sgn a * sgn b"
by (auto simp add: sgn_if zero_less_mult_iff)
-lemma abs_sgn: "abs k = k * sgn k"
+lemma abs_sgn: "\<bar>k\<bar> = k * sgn k"
unfolding sgn_if abs_if by auto
lemma sgn_greater [simp]:
@@ -1085,14 +1204,14 @@
"sgn a < 0 \<longleftrightarrow> a < 0"
unfolding sgn_if by auto
-lemma abs_dvd_iff [simp]: "(abs m) dvd k \<longleftrightarrow> m dvd k"
+lemma abs_dvd_iff [simp]: "\<bar>m\<bar> dvd k \<longleftrightarrow> m dvd k"
by (simp add: abs_if)
-lemma dvd_abs_iff [simp]: "m dvd (abs k) \<longleftrightarrow> m dvd k"
+lemma dvd_abs_iff [simp]: "m dvd \<bar>k\<bar> \<longleftrightarrow> m dvd k"
by (simp add: abs_if)
lemma dvd_if_abs_eq:
- "abs l = abs (k) \<Longrightarrow> l dvd k"
+ "\<bar>l\<bar> = \<bar>k\<bar> \<Longrightarrow> l dvd k"
by(subst abs_dvd_iff[symmetric]) simp
end
@@ -1110,17 +1229,7 @@
mult_cancel_right1 mult_cancel_right2
mult_cancel_left1 mult_cancel_left2
--- {* FIXME continue localization here *}
-
-subsection {* Reasoning about inequalities with division *}
-
-lemma mult_right_le_one_le: "0 <= (x::'a::linordered_idom) ==> 0 <= y ==> y <= 1
- ==> x * y <= x"
-by (auto simp add: mult_le_cancel_left2)
-
-lemma mult_left_le_one_le: "0 <= (x::'a::linordered_idom) ==> 0 <= y ==> y <= 1
- ==> y * x <= x"
-by (auto simp add: mult_le_cancel_right2)
+text {* Reasoning about inequalities with division *}
context linordered_semidom
begin
@@ -1137,20 +1246,34 @@
end
+context linordered_idom
+begin
-subsection {* Absolute Value *}
+lemma mult_right_le_one_le:
+ "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> x * y \<le> x"
+ by (auto simp add: mult_le_cancel_left2)
+
+lemma mult_left_le_one_le:
+ "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> y * x \<le> x"
+ by (auto simp add: mult_le_cancel_right2)
+
+end
+
+text {* Absolute Value *}
context linordered_idom
begin
-lemma mult_sgn_abs: "sgn x * abs x = x"
+lemma mult_sgn_abs:
+ "sgn x * \<bar>x\<bar> = x"
unfolding abs_if sgn_if by auto
+lemma abs_one [simp]:
+ "\<bar>1\<bar> = 1"
+ by (simp add: abs_if zero_less_one [THEN less_not_sym])
+
end
-lemma abs_one [simp]: "abs 1 = (1::'a::linordered_idom)"
-by (simp add: abs_if zero_less_one [THEN order_less_not_sym])
-
class ordered_ring_abs = ordered_ring + ordered_ab_group_add_abs +
assumes abs_eq_mult:
"(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0) \<Longrightarrow> \<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>"
@@ -1162,39 +1285,35 @@
qed (auto simp add: abs_if not_less mult_less_0_iff)
lemma abs_mult:
- "abs (a * b) = abs a * abs b"
+ "\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>"
by (rule abs_eq_mult) auto
lemma abs_mult_self:
- "abs a * abs a = a * a"
+ "\<bar>a\<bar> * \<bar>a\<bar> = a * a"
by (simp add: abs_if)
-end
-
lemma abs_mult_less:
- "[| abs a < c; abs b < d |] ==> abs a * abs b < c*(d::'a::linordered_idom)"
+ "\<bar>a\<bar> < c \<Longrightarrow> \<bar>b\<bar> < d \<Longrightarrow> \<bar>a\<bar> * \<bar>b\<bar> < c * d"
proof -
- assume ac: "abs a < c"
- hence cpos: "0<c" by (blast intro: order_le_less_trans abs_ge_zero)
- assume "abs b < d"
+ assume ac: "\<bar>a\<bar> < c"
+ hence cpos: "0<c" by (blast intro: le_less_trans abs_ge_zero)
+ assume "\<bar>b\<bar> < d"
thus ?thesis by (simp add: ac cpos mult_strict_mono)
qed
-lemmas eq_minus_self_iff[no_atp] = equal_neg_zero
-
-lemma less_minus_self_iff: "(a < -a) = (a < (0::'a::linordered_idom))"
- unfolding order_less_le less_eq_neg_nonpos equal_neg_zero ..
+lemma less_minus_self_iff:
+ "a < - a \<longleftrightarrow> a < 0"
+ by (simp only: less_le less_eq_neg_nonpos equal_neg_zero)
-lemma abs_less_iff: "(abs a < b) = (a < b & -a < (b::'a::linordered_idom))"
-apply (simp add: order_less_le abs_le_iff)
-apply (auto simp add: abs_if)
-done
+lemma abs_less_iff:
+ "\<bar>a\<bar> < b \<longleftrightarrow> a < b \<and> - a < b"
+ by (simp add: less_le abs_le_iff) (auto simp add: abs_if)
-lemma abs_mult_pos: "(0::'a::linordered_idom) <= x ==>
- (abs y) * x = abs (y * x)"
- apply (subst abs_mult)
- apply simp
-done
+lemma abs_mult_pos:
+ "0 \<le> x \<Longrightarrow> \<bar>y\<bar> * x = \<bar>y * x\<bar>"
+ by (simp add: abs_mult)
+
+end
code_modulename SML
Rings Arith