--- a/NEWS Fri Apr 23 16:12:57 2010 +0200
+++ b/NEWS Fri Apr 23 19:32:37 2010 +0200
@@ -112,6 +112,13 @@
*** HOL ***
+* Abstract algebra:
+ * class division_by_zero includes division_ring;
+ * numerous lemmas have been ported from field to division_ring;
+ * dropped lemma eq_minus_self_iff which is a duplicate for equal_neg_zero.
+
+ INCOMPATIBILITY.
+
* Library theory 'RBT' renamed to 'RBT_Impl'; new library theory 'RBT'
provides abstract red-black tree type which is backed by RBT_Impl
as implementation. INCOMPATIBILTY.
--- a/src/HOL/Big_Operators.thy Fri Apr 23 16:12:57 2010 +0200
+++ b/src/HOL/Big_Operators.thy Fri Apr 23 19:32:37 2010 +0200
@@ -555,7 +555,7 @@
qed
lemma setsum_mono2:
-fixes f :: "'a \<Rightarrow> 'b :: {ordered_ab_semigroup_add_imp_le,comm_monoid_add}"
+fixes f :: "'a \<Rightarrow> 'b :: ordered_comm_monoid_add"
assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"
shows "setsum f A \<le> setsum f B"
proof -
@@ -1030,7 +1030,7 @@
lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
(setprod f (A - {a}) :: 'a :: {field}) =
(if a:A then setprod f A / f a else setprod f A)"
-by (erule finite_induct) (auto simp add: insert_Diff_if)
+ by (erule finite_induct) (auto simp add: insert_Diff_if)
lemma setprod_inversef:
fixes f :: "'b \<Rightarrow> 'a::{field,division_by_zero}"
--- a/src/HOL/Decision_Procs/mir_tac.ML Fri Apr 23 16:12:57 2010 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML Fri Apr 23 19:32:37 2010 +0200
@@ -33,7 +33,7 @@
@{thm "real_of_nat_number_of"},
@{thm "real_of_nat_Suc"}, @{thm "real_of_nat_one"}, @{thm "real_of_one"},
@{thm "real_of_int_zero"}, @{thm "real_of_nat_zero"},
- @{thm "Fields.divide_zero"},
+ @{thm "divide_zero"},
@{thm "divide_divide_eq_left"}, @{thm "times_divide_eq_right"},
@{thm "times_divide_eq_left"}, @{thm "divide_divide_eq_right"},
@{thm "diff_def"}, @{thm "minus_divide_left"}]
--- a/src/HOL/Fields.thy Fri Apr 23 16:12:57 2010 +0200
+++ b/src/HOL/Fields.thy Fri Apr 23 19:32:37 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)
+lemma times_divide_eq_left [simp]: "(b / c) * a = (b * a) / c"
+ 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,392 @@
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] del: times_divide_eq)
+ 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] del: times_divide_eq)
+ 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] del: times_divide_eq)
+ 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] del: times_divide_eq)
+ 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] del: times_divide_eq)
+ 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] del: times_divide_eq)
+ 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] del: times_divide_eq)
+ 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] del: times_divide_eq)
+ 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
+
+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 (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.*}
+
+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 +687,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 +705,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 +717,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 +726,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 +735,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 +744,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 +765,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 +793,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 +834,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 +886,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/Groebner_Basis.thy Fri Apr 23 16:12:57 2010 +0200
+++ b/src/HOL/Groebner_Basis.thy Fri Apr 23 19:32:37 2010 +0200
@@ -627,7 +627,7 @@
val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"},
@{thm "divide_Numeral1"},
- @{thm "Fields.divide_zero"}, @{thm "divide_Numeral0"},
+ @{thm "divide_zero"}, @{thm "divide_Numeral0"},
@{thm "divide_divide_eq_left"}, @{thm "mult_frac_frac"},
@{thm "mult_num_frac"}, @{thm "mult_frac_num"},
@{thm "mult_frac_frac"}, @{thm "times_divide_eq_right"},
--- a/src/HOL/Groups.thy Fri Apr 23 16:12:57 2010 +0200
+++ b/src/HOL/Groups.thy Fri Apr 23 19:32:37 2010 +0200
@@ -757,7 +757,7 @@
done
lemma less_diff_eq[algebra_simps]: "a < c - b \<longleftrightarrow> a + b < c"
-apply (subst less_iff_diff_less_0 [of "plus a b"])
+apply (subst less_iff_diff_less_0 [of "a + b"])
apply (subst less_iff_diff_less_0 [of a])
apply (simp add: diff_minus add_ac)
done
@@ -966,27 +966,26 @@
end
--- {* FIXME localize the following *}
+context ordered_comm_monoid_add
+begin
lemma add_increasing:
- fixes c :: "'a::{ordered_ab_semigroup_add_imp_le, comm_monoid_add}"
- shows "[|0\<le>a; b\<le>c|] ==> b \<le> a + c"
-by (insert add_mono [of 0 a b c], simp)
+ "0 \<le> a \<Longrightarrow> b \<le> c \<Longrightarrow> b \<le> a + c"
+ by (insert add_mono [of 0 a b c], simp)
lemma add_increasing2:
- fixes c :: "'a::{ordered_ab_semigroup_add_imp_le, comm_monoid_add}"
- shows "[|0\<le>c; b\<le>a|] ==> b \<le> a + c"
-by (simp add:add_increasing add_commute[of a])
+ "0 \<le> c \<Longrightarrow> b \<le> a \<Longrightarrow> b \<le> a + c"
+ by (simp add: add_increasing add_commute [of a])
lemma add_strict_increasing:
- fixes c :: "'a::{ordered_ab_semigroup_add_imp_le, comm_monoid_add}"
- shows "[|0<a; b\<le>c|] ==> b < a + c"
-by (insert add_less_le_mono [of 0 a b c], simp)
+ "0 < a \<Longrightarrow> b \<le> c \<Longrightarrow> b < a + c"
+ by (insert add_less_le_mono [of 0 a b c], simp)
lemma add_strict_increasing2:
- fixes c :: "'a::{ordered_ab_semigroup_add_imp_le, comm_monoid_add}"
- shows "[|0\<le>a; b<c|] ==> b < a + c"
-by (insert add_le_less_mono [of 0 a b c], simp)
+ "0 \<le> a \<Longrightarrow> b < c \<Longrightarrow> b < a + c"
+ by (insert add_le_less_mono [of 0 a b c], simp)
+
+end
class abs =
fixes abs :: "'a \<Rightarrow> 'a"
@@ -1036,7 +1035,7 @@
lemma abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>"
by (rule antisym)
- (auto intro!: abs_ge_self abs_leI order_trans [of "uminus (abs a)" zero "abs a"])
+ (auto intro!: abs_ge_self abs_leI order_trans [of "- \<bar>a\<bar>" 0 "\<bar>a\<bar>"])
lemma abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0"
proof -
@@ -1045,7 +1044,7 @@
assume zero: "\<bar>a\<bar> = 0"
with abs_ge_self show "a \<le> 0" by auto
from zero have "\<bar>-a\<bar> = 0" by simp
- with abs_ge_self [of "uminus a"] have "- a \<le> 0" by auto
+ with abs_ge_self [of "- a"] have "- a \<le> 0" by auto
with neg_le_0_iff_le show "0 \<le> a" by auto
qed
then show ?thesis by auto
@@ -1114,32 +1113,31 @@
by (insert abs_ge_self, blast intro: order_trans)
lemma abs_le_D2: "\<bar>a\<bar> \<le> b \<Longrightarrow> - a \<le> b"
-by (insert abs_le_D1 [of "uminus a"], simp)
+by (insert abs_le_D1 [of "- a"], simp)
lemma abs_le_iff: "\<bar>a\<bar> \<le> b \<longleftrightarrow> a \<le> b \<and> - a \<le> b"
by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)
lemma abs_triangle_ineq2: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>a - b\<bar>"
- apply (simp add: algebra_simps)
- apply (subgoal_tac "abs a = abs (plus b (minus a b))")
- apply (erule ssubst)
- apply (rule abs_triangle_ineq)
- apply (rule arg_cong[of _ _ abs])
- apply (simp add: algebra_simps)
-done
+proof -
+ have "\<bar>a\<bar> = \<bar>b + (a - b)\<bar>"
+ by (simp add: algebra_simps add_diff_cancel)
+ then have "\<bar>a\<bar> \<le> \<bar>b\<bar> + \<bar>a - b\<bar>"
+ by (simp add: abs_triangle_ineq)
+ then show ?thesis
+ by (simp add: algebra_simps)
+qed
+
+lemma abs_triangle_ineq2_sym: "\<bar>a\<bar> - \<bar>b\<bar> \<le> \<bar>b - a\<bar>"
+ by (simp only: abs_minus_commute [of b] abs_triangle_ineq2)
lemma abs_triangle_ineq3: "\<bar>\<bar>a\<bar> - \<bar>b\<bar>\<bar> \<le> \<bar>a - b\<bar>"
- apply (subst abs_le_iff)
- apply auto
- apply (rule abs_triangle_ineq2)
- apply (subst abs_minus_commute)
- apply (rule abs_triangle_ineq2)
-done
+ by (simp add: abs_le_iff abs_triangle_ineq2 abs_triangle_ineq2_sym)
lemma abs_triangle_ineq4: "\<bar>a - b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
proof -
- have "abs(a - b) = abs(a + - b)" by (subst diff_minus, rule refl)
- also have "... <= abs a + abs (- b)" by (rule abs_triangle_ineq)
+ have "\<bar>a - b\<bar> = \<bar>a + - b\<bar>" by (subst diff_minus, rule refl)
+ also have "... \<le> \<bar>a\<bar> + \<bar>- b\<bar>" by (rule abs_triangle_ineq)
finally show ?thesis by simp
qed
--- a/src/HOL/Library/Binomial.thy Fri Apr 23 16:12:57 2010 +0200
+++ b/src/HOL/Library/Binomial.thy Fri Apr 23 19:32:37 2010 +0200
@@ -391,13 +391,13 @@
assumes kn: "k \<le> n"
shows "(of_nat (n choose k) :: 'a::field_char_0) = of_nat (fact n) / (of_nat (fact k) * of_nat (fact (n - k)))"
using binomial_fact_lemma[OF kn]
- by (simp add: field_simps of_nat_mult[symmetric])
+ by (simp add: field_eq_simps of_nat_mult [symmetric])
lemma binomial_gbinomial: "of_nat (n choose k) = of_nat n gchoose k"
proof-
{assume kn: "k > n"
from kn binomial_eq_0[OF kn] have ?thesis
- by (simp add: gbinomial_pochhammer field_simps
+ by (simp add: gbinomial_pochhammer field_eq_simps
pochhammer_of_nat_eq_0_iff)}
moreover
{assume "k=0" then have ?thesis by simp}
@@ -420,7 +420,7 @@
from eq[symmetric]
have ?thesis using kn
apply (simp add: binomial_fact[OF kn, where ?'a = 'a]
- gbinomial_pochhammer field_simps pochhammer_Suc_setprod)
+ gbinomial_pochhammer field_eq_simps pochhammer_Suc_setprod)
apply (simp add: pochhammer_Suc_setprod fact_altdef_nat h of_nat_setprod setprod_timesf[symmetric] eq' del: One_nat_def power_Suc)
unfolding setprod_Un_disjoint[OF th0, unfolded eq3, of "of_nat:: nat \<Rightarrow> 'a"] eq[unfolded h]
unfolding mult_assoc[symmetric]
@@ -449,7 +449,7 @@
have "?r = ((- 1) ^n * pochhammer (- a) n / of_nat (fact n)) * (of_nat n - (- a + of_nat n))"
unfolding gbinomial_pochhammer
pochhammer_Suc fact_Suc of_nat_mult right_diff_distrib power_Suc
- by (simp add: field_simps del: of_nat_Suc)
+ by (simp add: field_eq_simps del: of_nat_Suc)
also have "\<dots> = ?l" unfolding gbinomial_pochhammer
by (simp add: ring_simps)
finally show ?thesis ..
--- a/src/HOL/Library/Formal_Power_Series.thy Fri Apr 23 16:12:57 2010 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy Fri Apr 23 19:32:37 2010 +0200
@@ -388,6 +388,8 @@
then show "a*b \<noteq> 0" unfolding fps_nonzero_nth by blast
qed
+instance fps :: (ring_1_no_zero_divisors) ring_1_no_zero_divisors ..
+
instance fps :: (idom) idom ..
instantiation fps :: (comm_ring_1) number_ring
@@ -586,7 +588,7 @@
from k have "real k > - log y x" by simp
then have "ln y * real k > - ln x" unfolding log_def
using ln_gt_zero_iff[OF yp] y1
- by (simp add: minus_divide_left field_simps del:minus_divide_left[symmetric] )
+ by (simp add: minus_divide_left field_simps field_eq_simps del:minus_divide_left[symmetric])
then have "ln y * real k + ln x > 0" by simp
then have "exp (real k * ln y + ln x) > exp 0"
by (simp add: mult_ac)
@@ -594,7 +596,7 @@
unfolding exp_zero exp_add exp_real_of_nat_mult
exp_ln[OF xp] exp_ln[OF yp] by simp
then have "x > (1/y)^k" using yp
- by (simp add: field_simps nonzero_power_divide )
+ by (simp add: field_simps field_eq_simps nonzero_power_divide)
then show ?thesis using kp by blast
qed
lemma X_nth[simp]: "X$n = (if n = 1 then 1 else 0)" by (simp add: X_def)
@@ -649,8 +651,7 @@
declare setsum_cong[fundef_cong]
-
-instantiation fps :: ("{comm_monoid_add,inverse, times, uminus}") inverse
+instantiation fps :: ("{comm_monoid_add, inverse, times, uminus}") inverse
begin
fun natfun_inverse:: "'a fps \<Rightarrow> nat \<Rightarrow> 'a" where
@@ -658,9 +659,12 @@
| "natfun_inverse f n = - inverse (f$0) * setsum (\<lambda>i. f$i * natfun_inverse f (n - i)) {1..n}"
definition fps_inverse_def:
- "inverse f = (if f$0 = 0 then 0 else Abs_fps (natfun_inverse f))"
+ "inverse f = (if f $ 0 = 0 then 0 else Abs_fps (natfun_inverse f))"
+
definition fps_divide_def: "divide = (\<lambda>(f::'a fps) g. f * inverse g)"
+
instance ..
+
end
lemma fps_inverse_zero[simp]:
@@ -671,10 +675,7 @@
apply (auto simp add: expand_fps_eq fps_inverse_def)
by (case_tac n, auto)
-instance fps :: ("{comm_monoid_add,inverse, times, uminus}") division_by_zero
- by default (rule fps_inverse_zero)
-
-lemma inverse_mult_eq_1[intro]: assumes f0: "f$0 \<noteq> (0::'a::field)"
+lemma inverse_mult_eq_1 [intro]: assumes f0: "f$0 \<noteq> (0::'a::field)"
shows "inverse f * f = 1"
proof-
have c: "inverse f * f = f * inverse f" by (simp add: mult_commute)
@@ -1687,7 +1688,7 @@
then have "setsum ?f ?Pnkn = of_nat (k+1) * ?r $ n * r (Suc k) (a $ 0) ^ k"
by (simp add: natpermute_max_card[OF nz, simplified])
also have "\<dots> = a$n - setsum ?f ?Pnknn"
- unfolding n1 using r00 a0 by (simp add: field_simps fps_radical_def del: of_nat_Suc )
+ unfolding n1 using r00 a0 by (simp add: field_eq_simps fps_radical_def del: of_nat_Suc)
finally have fn: "setsum ?f ?Pnkn = a$n - setsum ?f ?Pnknn" .
have "(?r ^ Suc k)$n = setsum ?f ?Pnkn + setsum ?f ?Pnknn"
unfolding fps_power_nth_Suc setsum_Un_disjoint[OF f d, unfolded eq] ..
@@ -1763,7 +1764,7 @@
shows "a = b / c"
proof-
from eq have "a * c * inverse c = b * inverse c" by simp
- hence "a * (inverse c * c) = b/c" by (simp only: field_simps divide_inverse)
+ hence "a * (inverse c * c) = b/c" by (simp only: field_eq_simps divide_inverse)
then show "a = b/c" unfolding field_inverse[OF c0] by simp
qed
@@ -1836,7 +1837,7 @@
show "a$(xs !i) = ?r$(xs!i)" .
qed
have th00: "\<And>(x::'a). of_nat (Suc k) * (x * inverse (of_nat (Suc k))) = x"
- by (simp add: field_simps del: of_nat_Suc)
+ by (simp add: field_eq_simps del: of_nat_Suc)
from H have "b$n = a^Suc k $ n" by (simp add: fps_eq_iff)
also have "a ^ Suc k$n = setsum ?g ?Pnkn + setsum ?g ?Pnknn"
unfolding fps_power_nth_Suc
@@ -1853,7 +1854,7 @@
then have "a$n = ?r $n"
apply (simp del: of_nat_Suc)
unfolding fps_radical_def n1
- by (simp add: field_simps n1 th00 del: of_nat_Suc)}
+ by (simp add: field_eq_simps n1 th00 del: of_nat_Suc)}
ultimately show "a$n = ?r $ n" by (cases n, auto)
qed}
then have "a = ?r" by (simp add: fps_eq_iff)}
@@ -2468,7 +2469,7 @@
proof-
let ?r = "fps_inv"
have ra0: "?r a $ 0 = 0" by (simp add: fps_inv_def)
- from a1 have ra1: "?r a $ 1 \<noteq> 0" by (simp add: fps_inv_def field_simps)
+ from a1 have ra1: "?r a $ 1 \<noteq> 0" by (simp add: fps_inv_def field_eq_simps)
have X0: "X$0 = 0" by simp
from fps_inv[OF ra0 ra1] have "?r (?r a) oo ?r a = X" .
then have "?r (?r a) oo ?r a oo a = X oo a" by simp
@@ -2485,7 +2486,7 @@
proof-
let ?r = "fps_ginv"
from c0 have rca0: "?r c a $0 = 0" by (simp add: fps_ginv_def)
- from a1 c1 have rca1: "?r c a $ 1 \<noteq> 0" by (simp add: fps_ginv_def field_simps)
+ from a1 c1 have rca1: "?r c a $ 1 \<noteq> 0" by (simp add: fps_ginv_def field_eq_simps)
from fps_ginv[OF rca0 rca1]
have "?r b (?r c a) oo ?r c a = b" .
then have "?r b (?r c a) oo ?r c a oo a = b oo a" by simp
@@ -2533,7 +2534,7 @@
proof-
{fix n
have "?l$n = ?r $ n"
- apply (auto simp add: E_def field_simps power_Suc[symmetric]simp del: fact_Suc of_nat_Suc power_Suc)
+ apply (auto simp add: E_def field_eq_simps power_Suc[symmetric]simp del: fact_Suc of_nat_Suc power_Suc)
by (simp add: of_nat_mult ring_simps)}
then show ?thesis by (simp add: fps_eq_iff)
qed
@@ -2544,13 +2545,13 @@
proof-
{assume d: ?lhs
from d have th: "\<And>n. a $ Suc n = c * a$n / of_nat (Suc n)"
- by (simp add: fps_deriv_def fps_eq_iff field_simps del: of_nat_Suc)
+ by (simp add: fps_deriv_def fps_eq_iff field_eq_simps del: of_nat_Suc)
{fix n have "a$n = a$0 * c ^ n/ (of_nat (fact n))"
apply (induct n)
apply simp
unfolding th
using fact_gt_zero_nat
- apply (simp add: field_simps del: of_nat_Suc fact_Suc)
+ apply (simp add: field_eq_simps del: of_nat_Suc fact_Suc)
apply (drule sym)
by (simp add: ring_simps of_nat_mult power_Suc)}
note th' = this
@@ -2653,13 +2654,13 @@
from E_add_mult[of a b]
have "(E (a + b)) $ n = (E a * E b)$n" by simp
then have "(a + b) ^ n = (\<Sum>i\<Colon>nat = 0\<Colon>nat..n. a ^ i * b ^ (n - i) * (of_nat (fact n) / of_nat (fact i * fact (n - i))))"
- by (simp add: field_simps fps_mult_nth of_nat_mult[symmetric] setsum_right_distrib)
+ by (simp add: field_eq_simps fps_mult_nth of_nat_mult[symmetric] setsum_right_distrib)
then show ?thesis
apply simp
apply (rule setsum_cong2)
apply simp
apply (frule binomial_fact[where ?'a = 'a, symmetric])
- by (simp add: field_simps of_nat_mult)
+ by (simp add: field_eq_simps of_nat_mult)
qed
text{* And the nat-form -- also available from Binomial.thy *}
@@ -2682,7 +2683,7 @@
by (simp add: L_def fps_eq_iff del: of_nat_Suc)
lemma L_nth: "L c $ n = (if n=0 then 0 else 1/c * ((- 1) ^ (n - 1) / of_nat n))"
- by (simp add: L_def field_simps)
+ by (simp add: L_def field_eq_simps)
lemma L_0[simp]: "L c $ 0 = 0" by (simp add: L_def)
lemma L_E_inv:
@@ -2712,7 +2713,7 @@
shows "L c + L d = fps_const (c+d) * L (c*d)"
(is "?r = ?l")
proof-
- from c0 d0 have eq: "1/c + 1/d = (c+d)/(c*d)" by (simp add: field_simps)
+ from c0 d0 have eq: "1/c + 1/d = (c+d)/(c*d)" by (simp add: field_eq_simps)
have "fps_deriv ?r = fps_const (1/c + 1/d) * inverse (1 + X)"
by (simp add: fps_deriv_L fps_const_add[symmetric] algebra_simps del: fps_const_add)
also have "\<dots> = fps_deriv ?l"
@@ -2752,7 +2753,7 @@
from lrn
have "a$ Suc n = ((c - of_nat n) / of_nat (Suc n)) * a $n"
apply (simp add: ring_simps del: of_nat_Suc)
- by (cases n, simp_all add: field_simps del: of_nat_Suc)
+ by (cases n, simp_all add: field_eq_simps del: of_nat_Suc)
}
note th0 = this
{fix n have "a$n = (c gchoose n) * a$0"
@@ -2761,7 +2762,7 @@
next
case (Suc m)
thus ?case unfolding th0
- apply (simp add: field_simps del: of_nat_Suc)
+ apply (simp add: field_eq_simps del: of_nat_Suc)
unfolding mult_assoc[symmetric] gbinomial_mult_1
by (simp add: ring_simps)
qed}
@@ -2879,7 +2880,7 @@
using kn pochhammer_minus'[where k=k and n=n and b=b]
apply (simp add: pochhammer_same)
using bn0
- by (simp add: field_simps power_add[symmetric])}
+ by (simp add: field_eq_simps power_add[symmetric])}
moreover
{assume nk: "k \<noteq> n"
have m1nk: "?m1 n = setprod (%i. - 1) {0..m}"
@@ -2904,7 +2905,7 @@
unfolding m1nk
unfolding m h pochhammer_Suc_setprod
- apply (simp add: field_simps del: fact_Suc id_def)
+ apply (simp add: field_eq_simps del: fact_Suc id_def)
unfolding fact_altdef_nat id_def
unfolding of_nat_setprod
unfolding setprod_timesf[symmetric]
@@ -2941,10 +2942,10 @@
apply auto
done
then have th2: "(?m1 n * ?p b n)/pochhammer (b - of_nat n + 1) k = setprod (%i. b - of_nat i) {0.. n - k - 1}"
- using nz' by (simp add: field_simps)
+ using nz' by (simp add: field_eq_simps)
have "(?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k) = ((?m1 k * ?p (of_nat n) k) / ?f n) * ((?m1 n * ?p b n)/pochhammer (b - of_nat n + 1) k)"
using bnz0
- by (simp add: field_simps)
+ by (simp add: field_eq_simps)
also have "\<dots> = b gchoose (n - k)"
unfolding th1 th2
using kn' by (simp add: gbinomial_def)
@@ -2958,15 +2959,15 @@
note th00 = this
have "?r = ((a + b) gchoose n) * (of_nat (fact n)/ (?m1 n * pochhammer (- b) n))"
unfolding gbinomial_pochhammer
- using bn0 by (auto simp add: field_simps)
+ using bn0 by (auto simp add: field_eq_simps)
also have "\<dots> = ?l"
unfolding gbinomial_Vandermonde[symmetric]
apply (simp add: th00)
unfolding gbinomial_pochhammer
- using bn0 apply (simp add: setsum_left_distrib setsum_right_distrib field_simps)
+ using bn0 apply (simp add: setsum_left_distrib setsum_right_distrib field_eq_simps)
apply (rule setsum_cong2)
apply (drule th00(2))
- by (simp add: field_simps power_add[symmetric])
+ by (simp add: field_eq_simps power_add[symmetric])
finally show ?thesis by simp
qed
@@ -2991,7 +2992,7 @@
have nz: "pochhammer c n \<noteq> 0" using c
by (simp add: pochhammer_eq_0_iff)
from Vandermonde_pochhammer_lemma[where a = "?a" and b="?b" and n=n, OF h, unfolded th0 th1]
- show ?thesis using nz by (simp add: field_simps setsum_right_distrib)
+ show ?thesis using nz by (simp add: field_eq_simps setsum_right_distrib)
qed
subsubsection{* Formal trigonometric functions *}
@@ -3013,9 +3014,9 @@
using en by (simp add: fps_sin_def)
also have "\<dots> = (- 1)^(n div 2) * c^Suc n * (of_nat (n+1) / (of_nat (Suc n) * of_nat (fact n)))"
unfolding fact_Suc of_nat_mult
- by (simp add: field_simps del: of_nat_add of_nat_Suc)
+ by (simp add: field_eq_simps del: of_nat_add of_nat_Suc)
also have "\<dots> = (- 1)^(n div 2) *c^Suc n / of_nat (fact n)"
- by (simp add: field_simps del: of_nat_add of_nat_Suc)
+ by (simp add: field_eq_simps del: of_nat_add of_nat_Suc)
finally have "?lhs $n = ?rhs$n" using en
by (simp add: fps_cos_def ring_simps power_Suc )}
then show "?lhs $ n = ?rhs $ n"
@@ -3037,9 +3038,9 @@
using en by (simp add: fps_cos_def)
also have "\<dots> = (- 1)^((n + 1) div 2)*c^Suc n * (of_nat (n+1) / (of_nat (Suc n) * of_nat (fact n)))"
unfolding fact_Suc of_nat_mult
- by (simp add: field_simps del: of_nat_add of_nat_Suc)
+ by (simp add: field_eq_simps del: of_nat_add of_nat_Suc)
also have "\<dots> = (- 1)^((n + 1) div 2) * c^Suc n / of_nat (fact n)"
- by (simp add: field_simps del: of_nat_add of_nat_Suc)
+ by (simp add: field_eq_simps del: of_nat_add of_nat_Suc)
also have "\<dots> = (- ((- 1)^((n - 1) div 2))) * c^Suc n / of_nat (fact n)"
unfolding th0 unfolding th1[OF en] by simp
finally have "?lhs $n = ?rhs$n" using en
@@ -3345,6 +3346,6 @@
shows "foldr (%c r. f c o r) cs (%c. g c a) c0 $ n =
foldr (%c r. (k c + of_nat n) * r) cs (g c0 a $ n)"
- by (induct cs arbitrary: c0, auto simp add: algebra_simps f )
+ by (induct cs arbitrary: c0, auto simp add: algebra_simps f)
end
--- a/src/HOL/Library/Fraction_Field.thy Fri Apr 23 16:12:57 2010 +0200
+++ b/src/HOL/Library/Fraction_Field.thy Fri Apr 23 19:32:37 2010 +0200
@@ -232,7 +232,7 @@
thm mult_eq_0_iff
end
-instantiation fract :: (idom) "{field, division_by_zero}"
+instantiation fract :: (idom) field
begin
definition
@@ -256,9 +256,6 @@
by (simp add: divide_fract_def)
instance proof
- show "inverse 0 = (0:: 'a fract)" by (simp add: fract_expand)
- (simp add: fract_collapse)
-next
fix q :: "'a fract"
assume "q \<noteq> 0"
then show "inverse q * q = 1" apply (cases q rule: Fract_cases_nonzero)
@@ -270,5 +267,11 @@
end
+instance fract :: (idom) division_by_zero
+proof
+ show "inverse 0 = (0:: 'a fract)" by (simp add: fract_expand)
+ (simp add: fract_collapse)
+qed
+
end
\ No newline at end of file
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Fri Apr 23 16:12:57 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Fri Apr 23 19:32:37 2010 +0200
@@ -2780,7 +2780,7 @@
from geometric_sum[OF x1, of "Suc n", unfolded x1']
have "(- (1 - x)) * setsum (\<lambda>i. x^i) {0 .. n} = - (1 - x^(Suc n))"
unfolding atLeastLessThanSuc_atLeastAtMost
- using x1' apply (auto simp only: field_simps)
+ using x1' apply (auto simp only: field_eq_simps)
apply (simp add: ring_simps)
done
then have ?thesis by (simp add: ring_simps) }
@@ -2815,7 +2815,7 @@
{assume x: "x = 1" hence ?thesis by simp}
moreover
{assume x: "x \<noteq> 1" hence nz: "1 - x \<noteq> 0" by simp
- from sum_gp_multiplied[OF nm, of x] nz have ?thesis by (simp add: field_simps)}
+ from sum_gp_multiplied[OF nm, of x] nz have ?thesis by (simp add: field_eq_simps)}
ultimately have ?thesis by metis
}
ultimately show ?thesis by metis
--- a/src/HOL/NSA/HDeriv.thy Fri Apr 23 16:12:57 2010 +0200
+++ b/src/HOL/NSA/HDeriv.thy Fri Apr 23 19:32:37 2010 +0200
@@ -204,7 +204,7 @@
apply (simp (no_asm) add: add_divide_distrib diff_divide_distrib)
apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+
apply (auto simp add: times_divide_eq_right [symmetric]
- simp del: times_divide_eq)
+ simp del: times_divide_eq_right times_divide_eq_left)
apply (drule_tac D = Db in lemma_nsderiv2, assumption+)
apply (drule_tac
approx_minus_iff [THEN iffD2, THEN bex_Infinitesimal_iff2 [THEN iffD2]])
--- a/src/HOL/Rat.thy Fri Apr 23 16:12:57 2010 +0200
+++ b/src/HOL/Rat.thy Fri Apr 23 19:32:37 2010 +0200
@@ -411,7 +411,7 @@
subsubsection {* The field of rational numbers *}
-instantiation rat :: "{field, division_by_zero}"
+instantiation rat :: field
begin
definition
@@ -433,9 +433,6 @@
by (simp add: divide_rat_def)
instance proof
- show "inverse 0 = (0::rat)" by (simp add: rat_number_expand)
- (simp add: rat_number_collapse)
-next
fix q :: rat
assume "q \<noteq> 0"
then show "inverse q * q = 1" by (cases q rule: Rat_cases_nonzero)
@@ -447,6 +444,9 @@
end
+instance rat :: division_by_zero proof
+qed (simp add: rat_number_expand, simp add: rat_number_collapse)
+
subsubsection {* Various *}
--- a/src/HOL/Rings.thy Fri Apr 23 16:12:57 2010 +0200
+++ b/src/HOL/Rings.thy Fri Apr 23 19:32:37 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 [simp]: "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
--- a/src/HOL/SetInterval.thy Fri Apr 23 16:12:57 2010 +0200
+++ b/src/HOL/SetInterval.thy Fri Apr 23 19:32:37 2010 +0200
@@ -1012,7 +1012,7 @@
qed
lemma setsum_le_included:
- fixes f :: "'a \<Rightarrow> 'b::{comm_monoid_add,ordered_ab_semigroup_add_imp_le}"
+ fixes f :: "'a \<Rightarrow> 'b::ordered_comm_monoid_add"
assumes "finite s" "finite t"
and "\<forall>y\<in>t. 0 \<le> g y" "(\<forall>x\<in>s. \<exists>y\<in>t. i y = x \<and> f x \<le> g y)"
shows "setsum f s \<le> setsum g t"
@@ -1085,9 +1085,21 @@
subsection {* The formula for geometric sums *}
lemma geometric_sum:
- "x ~= 1 ==> (\<Sum>i=0..<n. x ^ i) =
- (x ^ n - 1) / (x - 1::'a::{field})"
-by (induct "n") (simp_all add: field_simps)
+ assumes "x \<noteq> 1"
+ shows "(\<Sum>i=0..<n. x ^ i) = (x ^ n - 1) / (x - 1::'a::field)"
+proof -
+ from assms obtain y where "y = x - 1" and "y \<noteq> 0" by simp_all
+ moreover have "(\<Sum>i=0..<n. (y + 1) ^ i) = ((y + 1) ^ n - 1) / y"
+ proof (induct n)
+ case 0 then show ?case by simp
+ next
+ case (Suc n)
+ moreover with `y \<noteq> 0` have "(1 + y) ^ n = (y * inverse y) * (1 + y) ^ n" by simp
+ ultimately show ?case by (simp add: field_eq_simps divide_inverse)
+ qed
+ ultimately show ?thesis by simp
+qed
+
subsection {* The formula for arithmetic sums *}
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML Fri Apr 23 16:12:57 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Fri Apr 23 19:32:37 2010 +0200
@@ -12,6 +12,137 @@
structure Datatype_Codegen : DATATYPE_CODEGEN =
struct
+(** generic code generator **)
+
+(* liberal addition of code data for datatypes *)
+
+fun mk_constr_consts thy vs dtco cos =
+ let
+ val cs = map (fn (c, tys) => (c, tys ---> Type (dtco, map TFree vs))) cos;
+ val cs' = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) cs;
+ in if is_some (try (Code.constrset_of_consts thy) cs')
+ then SOME cs
+ else NONE
+ end;
+
+
+(* case certificates *)
+
+fun mk_case_cert thy tyco =
+ let
+ val raw_thms =
+ (#case_rewrites o Datatype_Data.the_info thy) tyco;
+ val thms as hd_thm :: _ = raw_thms
+ |> Conjunction.intr_balanced
+ |> Thm.unvarify_global
+ |> Conjunction.elim_balanced (length raw_thms)
+ |> map Simpdata.mk_meta_eq
+ |> map Drule.zero_var_indexes
+ val params = fold_aterms (fn (Free (v, _)) => insert (op =) v
+ | _ => I) (Thm.prop_of hd_thm) [];
+ val rhs = hd_thm
+ |> Thm.prop_of
+ |> Logic.dest_equals
+ |> fst
+ |> Term.strip_comb
+ |> apsnd (fst o split_last)
+ |> list_comb;
+ val lhs = Free (Name.variant params "case", Term.fastype_of rhs);
+ val asm = (Thm.cterm_of thy o Logic.mk_equals) (lhs, rhs);
+ in
+ thms
+ |> Conjunction.intr_balanced
+ |> MetaSimplifier.rewrite_rule [(Thm.symmetric o Thm.assume) asm]
+ |> Thm.implies_intr asm
+ |> Thm.generalize ([], params) 0
+ |> AxClass.unoverload thy
+ |> Thm.varifyT_global
+ end;
+
+
+(* equality *)
+
+fun mk_eq_eqns thy dtco =
+ let
+ val (vs, cos) = Datatype_Data.the_spec thy dtco;
+ val { descr, index, inject = inject_thms, distinct = distinct_thms, ... } =
+ Datatype_Data.the_info thy dtco;
+ val ty = Type (dtco, map TFree vs);
+ fun mk_eq (t1, t2) = Const (@{const_name eq_class.eq}, ty --> ty --> HOLogic.boolT)
+ $ t1 $ t2;
+ fun true_eq t12 = HOLogic.mk_eq (mk_eq t12, HOLogic.true_const);
+ fun false_eq t12 = HOLogic.mk_eq (mk_eq t12, HOLogic.false_const);
+ val triv_injects = map_filter
+ (fn (c, []) => SOME (HOLogic.mk_Trueprop (true_eq (Const (c, ty), Const (c, ty))))
+ | _ => NONE) cos;
+ fun prep_inject (trueprop $ (equiv $ (_ $ t1 $ t2) $ rhs)) =
+ trueprop $ (equiv $ mk_eq (t1, t2) $ rhs);
+ val injects = map prep_inject (nth (Datatype_Prop.make_injs [descr] vs) index);
+ fun prep_distinct (trueprop $ (not $ (_ $ t1 $ t2))) =
+ [trueprop $ false_eq (t1, t2), trueprop $ false_eq (t2, t1)];
+ val distincts = maps prep_distinct (snd (nth (Datatype_Prop.make_distincts [descr] vs) index));
+ val refl = HOLogic.mk_Trueprop (true_eq (Free ("x", ty), Free ("x", ty)));
+ val simpset = Simplifier.global_context thy (HOL_basic_ss addsimps
+ (map Simpdata.mk_eq (@{thm eq} :: @{thm eq_True} :: inject_thms @ distinct_thms)));
+ fun prove prop = Skip_Proof.prove_global thy [] [] prop (K (ALLGOALS (simp_tac simpset)))
+ |> Simpdata.mk_eq;
+ in (map prove (triv_injects @ injects @ distincts), prove refl) end;
+
+fun add_equality vs dtcos thy =
+ let
+ fun add_def dtco lthy =
+ let
+ val ty = Type (dtco, map TFree vs);
+ fun mk_side const_name = Const (const_name, ty --> ty --> HOLogic.boolT)
+ $ Free ("x", ty) $ Free ("y", ty);
+ val def = HOLogic.mk_Trueprop (HOLogic.mk_eq
+ (mk_side @{const_name eq_class.eq}, mk_side @{const_name "op ="}));
+ val def' = Syntax.check_term lthy def;
+ val ((_, (_, thm)), lthy') = Specification.definition
+ (NONE, (Attrib.empty_binding, def')) lthy;
+ val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy);
+ val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
+ in (thm', lthy') end;
+ fun tac thms = Class.intro_classes_tac []
+ THEN ALLGOALS (ProofContext.fact_tac thms);
+ fun add_eq_thms dtco =
+ Theory.checkpoint
+ #> `(fn thy => mk_eq_eqns thy dtco)
+ #-> (fn (thms, thm) =>
+ Code.add_nbe_eqn thm
+ #> fold_rev Code.add_eqn thms);
+ in
+ thy
+ |> Theory_Target.instantiation (dtcos, vs, [HOLogic.class_eq])
+ |> fold_map add_def dtcos
+ |-> (fn def_thms => Class.prove_instantiation_exit_result (map o Morphism.thm)
+ (fn _ => fn def_thms => tac def_thms) def_thms)
+ |-> (fn def_thms => fold Code.del_eqn def_thms)
+ |> fold add_eq_thms dtcos
+ end;
+
+
+(* register a datatype etc. *)
+
+fun add_all_code config dtcos thy =
+ let
+ val (vs :: _, coss) = (split_list o map (Datatype_Data.the_spec thy)) dtcos;
+ val any_css = map2 (mk_constr_consts thy vs) dtcos coss;
+ val css = if exists is_none any_css then []
+ else map_filter I any_css;
+ val case_rewrites = maps (#case_rewrites o Datatype_Data.the_info thy) dtcos;
+ val certs = map (mk_case_cert thy) dtcos;
+ in
+ if null css then thy
+ else thy
+ |> tap (fn _ => Datatype_Aux.message config "Registering datatype for code generator ...")
+ |> fold Code.add_datatype css
+ |> fold_rev Code.add_default_eqn case_rewrites
+ |> fold Code.add_case certs
+ |> add_equality vs dtcos
+ end;
+
+
(** SML code generator **)
open Codegen;
@@ -288,142 +419,11 @@
| datatype_tycodegen _ _ _ _ _ _ _ = NONE;
-(** generic code generator **)
-
-(* liberal addition of code data for datatypes *)
-
-fun mk_constr_consts thy vs dtco cos =
- let
- val cs = map (fn (c, tys) => (c, tys ---> Type (dtco, map TFree vs))) cos;
- val cs' = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) cs;
- in if is_some (try (Code.constrset_of_consts thy) cs')
- then SOME cs
- else NONE
- end;
-
-
-(* case certificates *)
-
-fun mk_case_cert thy tyco =
- let
- val raw_thms =
- (#case_rewrites o Datatype_Data.the_info thy) tyco;
- val thms as hd_thm :: _ = raw_thms
- |> Conjunction.intr_balanced
- |> Thm.unvarify_global
- |> Conjunction.elim_balanced (length raw_thms)
- |> map Simpdata.mk_meta_eq
- |> map Drule.zero_var_indexes
- val params = fold_aterms (fn (Free (v, _)) => insert (op =) v
- | _ => I) (Thm.prop_of hd_thm) [];
- val rhs = hd_thm
- |> Thm.prop_of
- |> Logic.dest_equals
- |> fst
- |> Term.strip_comb
- |> apsnd (fst o split_last)
- |> list_comb;
- val lhs = Free (Name.variant params "case", Term.fastype_of rhs);
- val asm = (Thm.cterm_of thy o Logic.mk_equals) (lhs, rhs);
- in
- thms
- |> Conjunction.intr_balanced
- |> MetaSimplifier.rewrite_rule [(Thm.symmetric o Thm.assume) asm]
- |> Thm.implies_intr asm
- |> Thm.generalize ([], params) 0
- |> AxClass.unoverload thy
- |> Thm.varifyT_global
- end;
-
-
-(* equality *)
-
-fun mk_eq_eqns thy dtco =
- let
- val (vs, cos) = Datatype_Data.the_spec thy dtco;
- val { descr, index, inject = inject_thms, distinct = distinct_thms, ... } =
- Datatype_Data.the_info thy dtco;
- val ty = Type (dtco, map TFree vs);
- fun mk_eq (t1, t2) = Const (@{const_name eq_class.eq}, ty --> ty --> HOLogic.boolT)
- $ t1 $ t2;
- fun true_eq t12 = HOLogic.mk_eq (mk_eq t12, HOLogic.true_const);
- fun false_eq t12 = HOLogic.mk_eq (mk_eq t12, HOLogic.false_const);
- val triv_injects = map_filter
- (fn (c, []) => SOME (HOLogic.mk_Trueprop (true_eq (Const (c, ty), Const (c, ty))))
- | _ => NONE) cos;
- fun prep_inject (trueprop $ (equiv $ (_ $ t1 $ t2) $ rhs)) =
- trueprop $ (equiv $ mk_eq (t1, t2) $ rhs);
- val injects = map prep_inject (nth (Datatype_Prop.make_injs [descr] vs) index);
- fun prep_distinct (trueprop $ (not $ (_ $ t1 $ t2))) =
- [trueprop $ false_eq (t1, t2), trueprop $ false_eq (t2, t1)];
- val distincts = maps prep_distinct (snd (nth (Datatype_Prop.make_distincts [descr] vs) index));
- val refl = HOLogic.mk_Trueprop (true_eq (Free ("x", ty), Free ("x", ty)));
- val simpset = Simplifier.global_context thy (HOL_basic_ss addsimps
- (map Simpdata.mk_eq (@{thm eq} :: @{thm eq_True} :: inject_thms @ distinct_thms)));
- fun prove prop = Skip_Proof.prove_global thy [] [] prop (K (ALLGOALS (simp_tac simpset)))
- |> Simpdata.mk_eq;
- in (map prove (triv_injects @ injects @ distincts), prove refl) end;
-
-fun add_equality vs dtcos thy =
- let
- fun add_def dtco lthy =
- let
- val ty = Type (dtco, map TFree vs);
- fun mk_side const_name = Const (const_name, ty --> ty --> HOLogic.boolT)
- $ Free ("x", ty) $ Free ("y", ty);
- val def = HOLogic.mk_Trueprop (HOLogic.mk_eq
- (mk_side @{const_name eq_class.eq}, mk_side @{const_name "op ="}));
- val def' = Syntax.check_term lthy def;
- val ((_, (_, thm)), lthy') = Specification.definition
- (NONE, (Attrib.empty_binding, def')) lthy;
- val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy);
- val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
- in (thm', lthy') end;
- fun tac thms = Class.intro_classes_tac []
- THEN ALLGOALS (ProofContext.fact_tac thms);
- fun add_eq_thms dtco =
- Theory.checkpoint
- #> `(fn thy => mk_eq_eqns thy dtco)
- #-> (fn (thms, thm) =>
- Code.add_nbe_eqn thm
- #> fold_rev Code.add_eqn thms);
- in
- thy
- |> Theory_Target.instantiation (dtcos, vs, [HOLogic.class_eq])
- |> fold_map add_def dtcos
- |-> (fn def_thms => Class.prove_instantiation_exit_result (map o Morphism.thm)
- (fn _ => fn def_thms => tac def_thms) def_thms)
- |-> (fn def_thms => fold Code.del_eqn def_thms)
- |> fold add_eq_thms dtcos
- end;
-
-
-(* register a datatype etc. *)
-
-fun add_all_code config dtcos thy =
- let
- val (vs :: _, coss) = (split_list o map (Datatype_Data.the_spec thy)) dtcos;
- val any_css = map2 (mk_constr_consts thy vs) dtcos coss;
- val css = if exists is_none any_css then []
- else map_filter I any_css;
- val case_rewrites = maps (#case_rewrites o Datatype_Data.the_info thy) dtcos;
- val certs = map (mk_case_cert thy) dtcos;
- in
- if null css then thy
- else thy
- |> tap (fn _ => Datatype_Aux.message config "Registering datatype for code generator ...")
- |> fold Code.add_datatype css
- |> fold_rev Code.add_default_eqn case_rewrites
- |> fold Code.add_case certs
- |> add_equality vs dtcos
- end;
-
-
(** theory setup **)
val setup =
- add_codegen "datatype" datatype_codegen
- #> add_tycodegen "datatype" datatype_tycodegen
- #> Datatype_Data.interpretation add_all_code
+ Datatype_Data.interpretation add_all_code
+ #> add_codegen "datatype" datatype_codegen
+ #> add_tycodegen "datatype" datatype_tycodegen;
end;