--- a/src/HOL/Deriv.thy Wed Apr 09 09:37:47 2014 +0200
+++ b/src/HOL/Deriv.thy Wed Apr 09 09:37:48 2014 +0200
@@ -427,7 +427,7 @@
shows "((\<lambda>x. f x / g x) has_derivative
(\<lambda>h. - f x * (inverse (g x) * g' h * inverse (g x)) + f' h / g x)) (at x within s)"
using has_derivative_mult[OF f has_derivative_inverse[OF x g]]
- by (simp add: divide_inverse field_simps)
+ by (simp add: field_simps)
text{*Conventional form requires mult-AC laws. Types real and complex only.*}
@@ -439,7 +439,7 @@
{ fix h
have "f' h / g x - f x * (inverse (g x) * g' h * inverse (g x)) =
(f' h * g x - f x * g' h) / (g x * g x)"
- by (simp add: divide_inverse field_simps nonzero_inverse_mult_distrib x)
+ by (simp add: field_simps x)
}
then show ?thesis
using has_derivative_divide [OF f g] x
@@ -728,7 +728,7 @@
(g has_field_derivative E) (at x within s) \<Longrightarrow> g x \<noteq> 0 \<Longrightarrow>
((\<lambda>x. f x / g x) has_field_derivative (D * g x - f x * E) / (g x * g x)) (at x within s)"
by (rule has_derivative_imp_has_field_derivative[OF has_derivative_divide])
- (auto dest: has_field_derivative_imp_has_derivative simp: field_simps nonzero_inverse_mult_distrib divide_inverse)
+ (auto dest: has_field_derivative_imp_has_derivative simp: field_simps)
lemma DERIV_quotient:
"(f has_field_derivative d) (at x within s) \<Longrightarrow>
--- a/src/HOL/Fields.thy Wed Apr 09 09:37:47 2014 +0200
+++ b/src/HOL/Fields.thy Wed Apr 09 09:37:48 2014 +0200
@@ -131,7 +131,7 @@
lemma divide_zero_left [simp]: "0 / a = 0"
by (simp add: divide_inverse)
-lemma inverse_eq_divide: "inverse a = 1 / a"
+lemma inverse_eq_divide [field_simps]: "inverse a = 1 / a"
by (simp add: divide_inverse)
lemma add_divide_distrib: "(a+b) / c = a/c + b/c"
@@ -174,13 +174,11 @@
finally show ?thesis .
qed
-lemma nonzero_neg_divide_eq_eq[field_simps]:
- "b \<noteq> 0 \<Longrightarrow> -(a/b) = c \<longleftrightarrow> -a = c*b"
-using nonzero_divide_eq_eq[of b "-a" c] by (simp add: divide_minus_left)
+lemma nonzero_neg_divide_eq_eq [field_simps]: "b \<noteq> 0 \<Longrightarrow> - (a / b) = c \<longleftrightarrow> - a = c * b"
+ using nonzero_divide_eq_eq[of b "-a" c] by (simp add: divide_minus_left)
-lemma nonzero_neg_divide_eq_eq2[field_simps]:
- "b \<noteq> 0 \<Longrightarrow> c = -(a/b) \<longleftrightarrow> c*b = -a"
-using nonzero_neg_divide_eq_eq[of b a c] by auto
+lemma nonzero_neg_divide_eq_eq2 [field_simps]: "b \<noteq> 0 \<Longrightarrow> c = - (a / b) \<longleftrightarrow> c * b = - a"
+ using nonzero_neg_divide_eq_eq[of b a c] by auto
lemma divide_eq_imp: "c \<noteq> 0 \<Longrightarrow> b = a * c \<Longrightarrow> b / c = a"
by (simp add: divide_inverse mult_assoc)
@@ -200,10 +198,18 @@
"z \<noteq> 0 \<Longrightarrow> x - y / z = (x * z - y) / z"
by (simp add: diff_divide_distrib nonzero_eq_divide_eq eq_diff_eq)
+lemma minus_divide_add_eq_iff [field_simps]:
+ "z \<noteq> 0 \<Longrightarrow> - (x / z) + y = (- x + y * z) / z"
+ by (simp add: add_divide_distrib diff_divide_eq_iff divide_minus_left)
+
lemma divide_diff_eq_iff [field_simps]:
"z \<noteq> 0 \<Longrightarrow> x / z - y = (x - y * z) / z"
by (simp add: field_simps)
+lemma minus_divide_diff_eq_iff [field_simps]:
+ "z \<noteq> 0 \<Longrightarrow> - (x / z) - y = (- x - y * z) / z"
+ by (simp add: divide_diff_eq_iff[symmetric] divide_minus_left)
+
end
class division_ring_inverse_zero = division_ring +
@@ -635,7 +641,7 @@
"0 < a \<Longrightarrow> a \<le> 1 \<Longrightarrow> 1 \<le> inverse a"
using le_imp_inverse_le [of a 1, unfolded inverse_1] .
-lemma pos_le_divide_eq [field_simps]: "0 < c ==> (a \<le> b/c) = (a*c \<le> b)"
+lemma pos_le_divide_eq [field_simps]: "0 < c \<Longrightarrow> a \<le> b / c \<longleftrightarrow> a * c \<le> b"
proof -
assume less: "0<c"
hence "(a \<le> b/c) = (a*c \<le> (b/c)*c)"
@@ -645,7 +651,7 @@
finally show ?thesis .
qed
-lemma neg_le_divide_eq [field_simps]: "c < 0 ==> (a \<le> b/c) = (b \<le> a*c)"
+lemma neg_le_divide_eq [field_simps]: "c < 0 \<Longrightarrow> a \<le> b / c \<longleftrightarrow> b \<le> a * c"
proof -
assume less: "c<0"
hence "(a \<le> b/c) = ((b/c)*c \<le> a*c)"
@@ -655,8 +661,7 @@
finally show ?thesis .
qed
-lemma pos_less_divide_eq [field_simps]:
- "0 < c ==> (a < b/c) = (a*c < b)"
+lemma pos_less_divide_eq [field_simps]: "0 < c \<Longrightarrow> a < b / c \<longleftrightarrow> a * c < b"
proof -
assume less: "0<c"
hence "(a < b/c) = (a*c < (b/c)*c)"
@@ -666,8 +671,7 @@
finally show ?thesis .
qed
-lemma neg_less_divide_eq [field_simps]:
- "c < 0 ==> (a < b/c) = (b < a*c)"
+lemma neg_less_divide_eq [field_simps]: "c < 0 \<Longrightarrow> a < b / c \<longleftrightarrow> b < a * c"
proof -
assume less: "c<0"
hence "(a < b/c) = ((b/c)*c < a*c)"
@@ -677,8 +681,7 @@
finally show ?thesis .
qed
-lemma pos_divide_less_eq [field_simps]:
- "0 < c ==> (b/c < a) = (b < a*c)"
+lemma pos_divide_less_eq [field_simps]: "0 < c \<Longrightarrow> b / c < a \<longleftrightarrow> b < a * c"
proof -
assume less: "0<c"
hence "(b/c < a) = ((b/c)*c < a*c)"
@@ -688,8 +691,7 @@
finally show ?thesis .
qed
-lemma neg_divide_less_eq [field_simps]:
- "c < 0 ==> (b/c < a) = (a*c < b)"
+lemma neg_divide_less_eq [field_simps]: "c < 0 \<Longrightarrow> b / c < a \<longleftrightarrow> a * c < b"
proof -
assume less: "c<0"
hence "(b/c < a) = (a*c < (b/c)*c)"
@@ -699,7 +701,7 @@
finally show ?thesis .
qed
-lemma pos_divide_le_eq [field_simps]: "0 < c ==> (b/c \<le> a) = (b \<le> a*c)"
+lemma pos_divide_le_eq [field_simps]: "0 < c \<Longrightarrow> b / c \<le> a \<longleftrightarrow> b \<le> a * c"
proof -
assume less: "0<c"
hence "(b/c \<le> a) = ((b/c)*c \<le> a*c)"
@@ -709,7 +711,7 @@
finally show ?thesis .
qed
-lemma neg_divide_le_eq [field_simps]: "c < 0 ==> (b/c \<le> a) = (a*c \<le> b)"
+lemma neg_divide_le_eq [field_simps]: "c < 0 \<Longrightarrow> b / c \<le> a \<longleftrightarrow> a * c \<le> b"
proof -
assume less: "c<0"
hence "(b/c \<le> a) = (a*c \<le> (b/c)*c)"
@@ -719,6 +721,33 @@
finally show ?thesis .
qed
+text{* The following @{text field_simps} rules are necessary, as minus is always moved atop of
+division but we want to get rid of division. *}
+
+lemma pos_le_minus_divide_eq [field_simps]: "0 < c \<Longrightarrow> a \<le> - (b / c) \<longleftrightarrow> a * c \<le> - b"
+ unfolding minus_divide_left by (rule pos_le_divide_eq)
+
+lemma neg_le_minus_divide_eq [field_simps]: "c < 0 \<Longrightarrow> a \<le> - (b / c) \<longleftrightarrow> - b \<le> a * c"
+ unfolding minus_divide_left by (rule neg_le_divide_eq)
+
+lemma pos_less_minus_divide_eq [field_simps]: "0 < c \<Longrightarrow> a < - (b / c) \<longleftrightarrow> a * c < - b"
+ unfolding minus_divide_left by (rule pos_less_divide_eq)
+
+lemma neg_less_minus_divide_eq [field_simps]: "c < 0 \<Longrightarrow> a < - (b / c) \<longleftrightarrow> - b < a * c"
+ unfolding minus_divide_left by (rule neg_less_divide_eq)
+
+lemma pos_minus_divide_less_eq [field_simps]: "0 < c \<Longrightarrow> - (b / c) < a \<longleftrightarrow> - b < a * c"
+ unfolding minus_divide_left by (rule pos_divide_less_eq)
+
+lemma neg_minus_divide_less_eq [field_simps]: "c < 0 \<Longrightarrow> - (b / c) < a \<longleftrightarrow> a * c < - b"
+ unfolding minus_divide_left by (rule neg_divide_less_eq)
+
+lemma pos_minus_divide_le_eq [field_simps]: "0 < c \<Longrightarrow> - (b / c) \<le> a \<longleftrightarrow> - b \<le> a * c"
+ unfolding minus_divide_left by (rule pos_divide_le_eq)
+
+lemma neg_minus_divide_le_eq [field_simps]: "c < 0 \<Longrightarrow> - (b / c) \<le> a \<longleftrightarrow> a * c \<le> - b"
+ unfolding minus_divide_left by (rule neg_divide_le_eq)
+
lemma frac_less_eq:
"y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y < w / z \<longleftrightarrow> (x * z - w * y) / (y * z) < 0"
by (subst less_iff_diff_less_0) (simp add: diff_frac_eq )
@@ -897,15 +926,6 @@
class linordered_field_inverse_zero = linordered_field + field_inverse_zero
begin
-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)"
-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)"
apply (cases "a = 0", simp)
@@ -926,26 +946,11 @@
"inverse a \<le> 0 \<longleftrightarrow> a \<le> 0"
by (simp add: not_less [symmetric])
-lemma one_less_inverse_iff:
- "1 < inverse x \<longleftrightarrow> 0 < x \<and> x < 1"
-proof cases
- assume "0 < x"
- with inverse_less_iff_less [OF zero_less_one, of x]
- show ?thesis by simp
-next
- assume notless: "~ (0 < x)"
- have "~ (1 < inverse x)"
- proof
- assume *: "1 < inverse x"
- also from notless and * have "... \<le> 0" by simp
- also have "... < 1" by (rule zero_less_one)
- finally show False by auto
- qed
- with notless show ?thesis by simp
-qed
+lemma one_less_inverse_iff: "1 < inverse x \<longleftrightarrow> 0 < x \<and> x < 1"
+ using less_trans[of 1 x 0 for x]
+ by (cases x 0 rule: linorder_cases) (auto simp add: field_simps)
-lemma one_le_inverse_iff:
- "1 \<le> inverse x \<longleftrightarrow> 0 < x \<and> x \<le> 1"
+lemma one_le_inverse_iff: "1 \<le> inverse x \<longleftrightarrow> 0 < x \<and> x \<le> 1"
proof (cases "x = 1")
case True then show ?thesis by simp
next
@@ -955,78 +960,37 @@
with False show ?thesis by (auto simp add: one_less_inverse_iff)
qed
-lemma inverse_less_1_iff:
- "inverse x < 1 \<longleftrightarrow> x \<le> 0 \<or> 1 < x"
+lemma inverse_less_1_iff: "inverse x < 1 \<longleftrightarrow> x \<le> 0 \<or> 1 < x"
by (simp add: not_le [symmetric] one_le_inverse_iff)
-lemma inverse_le_1_iff:
- "inverse x \<le> 1 \<longleftrightarrow> x \<le> 0 \<or> 1 \<le> x"
+lemma inverse_le_1_iff: "inverse x \<le> 1 \<longleftrightarrow> x \<le> 0 \<or> 1 \<le> x"
by (simp add: not_less [symmetric] one_less_inverse_iff)
-lemma divide_le_eq:
- "(b/c \<le> a) =
- (if 0 < c then b \<le> a*c
- else if c < 0 then a*c \<le> b
- else 0 \<le> a)"
-apply (cases "c=0", simp)
-apply (force simp add: pos_divide_le_eq neg_divide_le_eq)
-done
-
-lemma less_divide_eq:
- "(a < b/c) =
- (if 0 < c then a*c < b
- else if c < 0 then b < a*c
- else a < 0)"
-apply (cases "c=0", simp)
-apply (force simp add: pos_less_divide_eq neg_less_divide_eq)
-done
-
-lemma divide_less_eq:
- "(b/c < a) =
- (if 0 < c then b < a*c
- else if c < 0 then a*c < b
- else 0 < a)"
-apply (cases "c=0", simp)
-apply (force simp add: pos_divide_less_eq neg_divide_less_eq)
-done
+lemma
+ shows le_divide_eq: "a \<le> b / c \<longleftrightarrow> (if 0 < c then a * c \<le> b else if c < 0 then b \<le> a * c else a \<le> 0)"
+ and divide_le_eq: "b / c \<le> a \<longleftrightarrow> (if 0 < c then b \<le> a * c else if c < 0 then a * c \<le> b else 0 \<le> a)"
+ and less_divide_eq: "a < b / c \<longleftrightarrow> (if 0 < c then a * c < b else if c < 0 then b < a * c else a < 0)"
+ and divide_less_eq: "b / c < a \<longleftrightarrow> (if 0 < c then b < a * c else if c < 0 then a * c < b else 0 < a)"
+ by (auto simp: field_simps not_less dest: antisym)
text {*Division and Signs*}
-lemma zero_less_divide_iff:
- "(0 < a/b) = (0 < a & 0 < b | a < 0 & b < 0)"
-by (simp add: divide_inverse zero_less_mult_iff)
-
-lemma divide_less_0_iff:
- "(a/b < 0) =
- (0 < a & b < 0 | a < 0 & 0 < b)"
-by (simp add: divide_inverse mult_less_0_iff)
-
-lemma zero_le_divide_iff:
- "(0 \<le> a/b) =
- (0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)"
-by (simp add: divide_inverse zero_le_mult_iff)
-
-lemma divide_le_0_iff:
- "(a/b \<le> 0) =
- (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"
-by (simp add: divide_inverse mult_le_0_iff)
+lemma
+ shows zero_less_divide_iff: "0 < a / b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
+ and divide_less_0_iff: "a / b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"
+ and zero_le_divide_iff: "0 \<le> a / b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0"
+ and divide_le_0_iff: "a / b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b"
+ by (simp_all add: divide_inverse zero_less_mult_iff mult_less_0_iff zero_le_mult_iff mult_le_0_iff)
text {* Division and the Number One *}
text{*Simplify expressions equated with 1*}
-lemma zero_eq_1_divide_iff [simp]:
- "(0 = 1/a) = (a = 0)"
-apply (cases "a=0", simp)
-apply (auto simp add: nonzero_eq_divide_eq)
-done
+lemma zero_eq_1_divide_iff [simp]: "0 = 1 / a \<longleftrightarrow> a = 0"
+ by (cases "a = 0") (auto simp: field_simps)
-lemma one_divide_eq_0_iff [simp]:
- "(1/a = 0) = (a = 0)"
-apply (cases "a=0", simp)
-apply (insert zero_neq_one [THEN not_sym])
-apply (auto simp add: nonzero_divide_eq_eq)
-done
+lemma one_divide_eq_0_iff [simp]: "1 / a = 0 \<longleftrightarrow> a = 0"
+ using zero_eq_1_divide_iff[of a] by simp
text{*Simplify expressions such as @{text "0 < 1/x"} to @{text "0 < x"}*}
@@ -1062,37 +1026,17 @@
apply (auto simp add: mult_commute)
done
-lemma inverse_le_iff:
- "inverse a \<le> inverse b \<longleftrightarrow> (0 < a * b \<longrightarrow> b \<le> a) \<and> (a * b \<le> 0 \<longrightarrow> a \<le> b)"
-proof -
- { assume "a < 0"
- then have "inverse a < 0" by simp
- moreover assume "0 < b"
- then have "0 < inverse b" by simp
- ultimately have "inverse a < inverse b" by (rule less_trans)
- then have "inverse a \<le> inverse b" by simp }
- moreover
- { assume "b < 0"
- then have "inverse b < 0" by simp
- moreover assume "0 < a"
- then have "0 < inverse a" by simp
- ultimately have "inverse b < inverse a" by (rule less_trans)
- then have "\<not> inverse a \<le> inverse b" by simp }
- ultimately show ?thesis
- by (cases a 0 b 0 rule: linorder_cases[case_product linorder_cases])
- (auto simp: not_less zero_less_mult_iff mult_le_0_iff)
-qed
+lemma inverse_le_iff: "inverse a \<le> inverse b \<longleftrightarrow> (0 < a * b \<longrightarrow> b \<le> a) \<and> (a * b \<le> 0 \<longrightarrow> a \<le> b)"
+ by (cases a 0 b 0 rule: linorder_cases[case_product linorder_cases])
+ (auto simp add: field_simps zero_less_mult_iff mult_le_0_iff)
-lemma inverse_less_iff:
- "inverse a < inverse b \<longleftrightarrow> (0 < a * b \<longrightarrow> b < a) \<and> (a * b \<le> 0 \<longrightarrow> a < b)"
+lemma inverse_less_iff: "inverse a < inverse b \<longleftrightarrow> (0 < a * b \<longrightarrow> b < a) \<and> (a * b \<le> 0 \<longrightarrow> a < b)"
by (subst less_le) (auto simp: inverse_le_iff)
-lemma divide_le_cancel:
- "a / c \<le> b / c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
+lemma divide_le_cancel: "a / c \<le> b / c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
by (simp add: divide_inverse mult_le_cancel_right)
-lemma divide_less_cancel:
- "a / c < b / c \<longleftrightarrow> (0 < c \<longrightarrow> a < b) \<and> (c < 0 \<longrightarrow> b < a) \<and> c \<noteq> 0"
+lemma divide_less_cancel: "a / c < b / c \<longleftrightarrow> (0 < c \<longrightarrow> a < b) \<and> (c < 0 \<longrightarrow> b < a) \<and> c \<noteq> 0"
by (auto simp add: divide_inverse mult_less_cancel_right)
text{*Simplify quotients that are compared with the value 1.*}
--- a/src/HOL/Library/Formal_Power_Series.thy Wed Apr 09 09:37:47 2014 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy Wed Apr 09 09:37:48 2014 +0200
@@ -2006,17 +2006,8 @@
*)
lemma eq_divide_imp':
- assumes c0: "(c::'a::field) \<noteq> 0"
- and eq: "a * c = b"
- shows "a = b / c"
-proof -
- from eq have "a * c * inverse c = b * inverse c"
- by simp
- then have "a * (inverse c * c) = b/c"
- by (simp only: field_simps divide_inverse)
- then show "a = b/c"
- unfolding field_inverse[OF c0] by simp
-qed
+ fixes c :: "'a::field" shows "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> a = b / c"
+ by (simp add: field_simps)
lemma radical_unique:
assumes r0: "(r (Suc k) (b$0)) ^ Suc k = b$0"
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Wed Apr 09 09:37:47 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Wed Apr 09 09:37:48 2014 +0200
@@ -5964,10 +5964,10 @@
by (auto simp add: field_simps)
then have "inverse d * (x \<bullet> i * 2) \<le> 2 + inverse d * (y \<bullet> i * 2)"
"inverse d * (y \<bullet> i * 2) \<le> 2 + inverse d * (x \<bullet> i * 2)"
- by (auto simp add:field_simps) }
+ using `0<d` by (auto simp add: field_simps) }
then have "inverse (2 * d) *\<^sub>R (y - (x - ?d)) \<in> cbox 0 (\<Sum>Basis)"
unfolding mem_box using assms
- by (auto simp add: field_simps inner_simps)
+ by (auto simp add: field_simps inner_simps simp del: inverse_eq_divide)
then show "\<exists>z\<in>cbox 0 (\<Sum>Basis). y = x - ?d + (2 * d) *\<^sub>R z"
apply -
apply (rule_tac x="inverse (2 * d) *\<^sub>R (y - (x - ?d))" in bexI)
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Wed Apr 09 09:37:47 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Wed Apr 09 09:37:48 2014 +0200
@@ -569,12 +569,8 @@
unfolding real_of_nat_def by (rule ex_le_of_nat)
lemma real_arch_inv: "0 < e \<longleftrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> 0 < inverse (real n) \<and> inverse (real n) < e)"
- using reals_Archimedean
- apply (auto simp add: field_simps)
- apply (subgoal_tac "inverse (real n) > 0")
- apply arith
- apply simp
- done
+ using reals_Archimedean[of e] less_trans[of 0 "1 / real n" e for n::nat]
+ by (auto simp add: field_simps cong: conj_cong)
lemma real_pow_lbound: "0 \<le> x \<Longrightarrow> 1 + real n * x \<le> (1 + x) ^ n"
proof (induct n)
@@ -629,7 +625,7 @@
from real_arch_pow[OF ix, of "1/y"]
obtain n where n: "1/y < (1/x)^n" by blast
then show ?thesis using y `x > 0`
- by (auto simp add: field_simps power_divide)
+ by (auto simp add: field_simps)
next
case False
with y x1 show ?thesis
@@ -1147,7 +1143,7 @@
using fS SP vS by auto
have "setsum (\<lambda>v. ?u v *\<^sub>R v) ?S =
setsum (\<lambda>v. (- (inverse (u ?a))) *\<^sub>R (u v *\<^sub>R v)) S - ?u v *\<^sub>R v"
- using fS vS uv by (simp add: setsum_diff1 divide_inverse field_simps)
+ using fS vS uv by (simp add: setsum_diff1 field_simps)
also have "\<dots> = ?a"
unfolding scaleR_right.setsum [symmetric] u using uv by simp
finally have "setsum (\<lambda>v. ?u v *\<^sub>R v) ?S = ?a" .
--- a/src/HOL/Power.thy Wed Apr 09 09:37:47 2014 +0200
+++ b/src/HOL/Power.thy Wed Apr 09 09:37:48 2014 +0200
@@ -108,7 +108,7 @@
context comm_monoid_mult
begin
-lemma power_mult_distrib:
+lemma power_mult_distrib [field_simps]:
"(a * b) ^ n = (a ^ n) * (b ^ n)"
by (induct n) (simp_all add: mult_ac)
@@ -661,7 +661,7 @@
"1 / (a::'a::{field_inverse_zero, power}) ^ n = (1 / a) ^ n"
by (simp add: divide_inverse) (rule power_inverse)
-lemma power_divide:
+lemma power_divide [field_simps]:
"(a / b) ^ n = (a::'a::field_inverse_zero) ^ n / b ^ n"
apply (cases "b = 0")
apply (simp add: power_0_left)
--- a/src/HOL/Rings.thy Wed Apr 09 09:37:47 2014 +0200
+++ b/src/HOL/Rings.thy Wed Apr 09 09:37:48 2014 +0200
@@ -830,22 +830,12 @@
then show "a * b \<noteq> 0" by (simp add: neq_iff)
qed
-lemma zero_less_mult_iff:
- "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
- apply (auto simp add: mult_pos_pos mult_neg_neg)
- apply (simp_all add: not_less le_less)
- apply (erule disjE) apply assumption defer
- apply (erule disjE) defer apply (drule sym) apply simp
- apply (erule disjE) defer apply (drule sym) apply simp
- apply (erule disjE) apply assumption apply (drule sym) apply simp
- apply (drule sym) apply simp
- apply (blast dest: zero_less_mult_pos)
- apply (blast dest: zero_less_mult_pos2)
- done
+lemma zero_less_mult_iff: "0 < a * b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0"
+ by (cases a 0 b 0 rule: linorder_cases[case_product linorder_cases])
+ (auto simp add: mult_pos_pos mult_neg_neg not_less le_less dest: zero_less_mult_pos zero_less_mult_pos2)
-lemma zero_le_mult_iff:
- "0 \<le> a * b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0"
-by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff)
+lemma zero_le_mult_iff: "0 \<le> a * b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0"
+ by (auto simp add: eq_commute [of 0] le_less not_less zero_less_mult_iff)
lemma mult_less_0_iff:
"a * b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b"
--- a/src/HOL/Set_Interval.thy Wed Apr 09 09:37:47 2014 +0200
+++ b/src/HOL/Set_Interval.thy Wed Apr 09 09:37:48 2014 +0200
@@ -1594,13 +1594,7 @@
proof -
from assms obtain y where "y = x - 1" and "y \<noteq> 0" by simp_all
moreover have "(\<Sum>i<n. (y + 1) ^ i) = ((y + 1) ^ n - 1) / y"
- proof (induct n)
- case 0 then show ?case by simp
- next
- case (Suc n)
- moreover from Suc `y \<noteq> 0` have "(1 + y) ^ n = (y * inverse y) * (1 + y) ^ n" by simp
- ultimately show ?case by (simp add: field_simps divide_inverse)
- qed
+ by (induct n) (simp_all add: field_simps `y \<noteq> 0`)
ultimately show ?thesis by simp
qed