--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy Mon Oct 07 21:51:31 2019 +0200
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy Tue Oct 08 10:26:40 2019 +0000
@@ -2126,7 +2126,6 @@
apply (rule_tac x = "dd x / k" in exI)
apply (simp add: field_simps that)
apply (simp add: vector_add_divide_simps algebra_simps)
- apply (metis (no_types) \<open>k \<noteq> 0\<close> divide_inverse_commute inverse_eq_divide mult.left_commute right_inverse)
done
ultimately show ?thesis
using segsub by (auto simp: rel_frontier_def)
--- a/src/HOL/Analysis/Change_Of_Vars.thy Mon Oct 07 21:51:31 2019 +0200
+++ b/src/HOL/Analysis/Change_Of_Vars.thy Tue Oct 08 10:26:40 2019 +0000
@@ -515,7 +515,7 @@
obtain \<zeta> where "0 < \<zeta>"
and \<zeta>: "\<And>y. \<lbrakk>y \<in> S; y \<noteq> x; dist y x < \<zeta>\<rbrakk>
\<Longrightarrow> norm (f y - (f x + f' x (y - x))) / norm (y - x) < k"
- using lim0 \<open>k > 0\<close> by (force simp: Lim_within field_simps)
+ using lim0 \<open>k > 0\<close> by (simp add: Lim_within) (auto simp add: field_simps)
define r where "r \<equiv> min (min l (\<zeta>/2)) (min 1 (d/2))"
show ?thesis
proof (intro exI conjI)
@@ -1738,8 +1738,9 @@
then obtain d where "d>0"
and d: "\<And>y. y\<in>S \<Longrightarrow> 0 < dist y x \<and> dist y x < d \<longrightarrow> norm (f y - f x - f' x (y - x)) / (norm (y - x))
< e/2"
- using f [OF \<open>x \<in> S\<close>] unfolding Deriv.has_derivative_at_within Lim_within
- by (auto simp: field_simps dest: spec [of _ "e/2"])
+ using f [OF \<open>x \<in> S\<close>]
+ by (simp add: Deriv.has_derivative_at_within Lim_within)
+ (auto simp add: field_simps dest: spec [of _ "e/2"])
let ?A = "matrix(f' x) - (\<chi> i j. if i = m \<and> j = n then e / 4 else 0)"
obtain B where BRats: "\<And>i j. B$i$j \<in> \<rat>" and Bo_e6: "onorm((*v) (?A - B)) < e/6"
using matrix_rational_approximation \<open>e > 0\<close>
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Mon Oct 07 21:51:31 2019 +0200
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Tue Oct 08 10:26:40 2019 +0000
@@ -779,7 +779,7 @@
have zball: "z \<in> ball c d"
using mem_ball z_def dist_norm[of c]
using y and assms(4,5)
- by (auto simp:field_simps norm_minus_commute)
+ by (simp add: norm_minus_commute) (simp add: field_simps)
have "x \<in> affine hull S"
using closure_affine_hull assms by auto
moreover have "y \<in> affine hull S"
@@ -790,7 +790,7 @@
using z_def affine_affine_hull[of S]
mem_affine_3_minus [of "affine hull S" c x y "(1 - e) / e"]
assms
- by (auto simp: field_simps)
+ by simp
then have "z \<in> S" using d zball by auto
obtain d1 where "d1 > 0" and d1: "ball z d1 \<le> ball c d"
using zball open_ball[of c d] openE[of "ball c d" z] by auto
@@ -2218,7 +2218,7 @@
fix y
assume "y \<in> cbox (x - ?d) (x + ?d)"
then have "inverse (2 * d) *\<^sub>R (y - (x - ?d)) \<in> cbox 0 (\<Sum>Basis)"
- using assms by (simp add: mem_box field_simps inner_simps)
+ using assms by (simp add: mem_box inner_simps) (simp add: field_simps)
with \<open>0 < d\<close> show "y \<in> (\<lambda>y. x - sum ((*\<^sub>R) d) Basis + (2 * d) *\<^sub>R y) ` cbox 0 One"
by (auto intro: image_eqI[where x= "inverse (2 * d) *\<^sub>R (y - (x - ?d))"])
next
--- a/src/HOL/Analysis/Derivative.thy Mon Oct 07 21:51:31 2019 +0200
+++ b/src/HOL/Analysis/Derivative.thy Tue Oct 08 10:26:40 2019 +0000
@@ -2419,7 +2419,7 @@
from fx[unfolded has_derivative_within, THEN conjunct2, THEN tendstoD, OF \<open>0 < e\<close>]
have "\<forall>\<^sub>F x' in at x within X. ?le x'"
by eventually_elim
- (auto simp: dist_norm divide_simps blinfun.bilinear_simps field_simps split: if_split_asm)
+ (simp add: dist_norm divide_simps diff_diff_add ac_simps split: if_split_asm)
then have "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. ?le x'"
by (rule eventually_at_Pair_within_TimesI1)
(simp add: blinfun.bilinear_simps)
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Mon Oct 07 21:51:31 2019 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Tue Oct 08 10:26:40 2019 +0000
@@ -1279,8 +1279,9 @@
proof (subst negligible_on_intervals, intro allI)
fix u v
show "negligible ((+) (- a) ` S \<inter> cbox u v)"
- using \<open>closed S\<close> eq1 by (auto simp add: negligible_iff_null_sets field_simps
+ using \<open>closed S\<close> eq1 by (auto simp add: negligible_iff_null_sets algebra_simps
intro!: closed_translation_subtract starlike_negligible_compact cong: image_cong_simp)
+ (metis add_diff_eq diff_add_cancel scale_right_diff_distrib)
qed
then show ?thesis
by (rule negligible_translation_rev)
--- a/src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy Mon Oct 07 21:51:31 2019 +0200
+++ b/src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy Tue Oct 08 10:26:40 2019 +0000
@@ -390,7 +390,7 @@
unfolding i_def \<Phi>_def BOX_def
by (simp add: algebra_simps content_cbox_plus norm_minus_commute)
finally have "measure lebesgue (\<Phi> D) * \<mu> \<le> norm (content (\<Phi> D) *\<^sub>R f(tag D) - integral (\<Phi> D) f)"
- using m_\<Phi> by (simp add: field_simps)
+ using m_\<Phi> by simp (simp add: field_simps)
then show "\<exists>y\<in>(\<lambda>D. (tag D, \<Phi> D)) ` \<G>.
snd y = \<Phi> D \<and> measure lebesgue (\<Phi> D) * \<mu> \<le> (case y of (x, k) \<Rightarrow> norm (content k *\<^sub>R f x - integral k f))"
using \<open>D \<in> \<G>\<close> by auto
@@ -643,7 +643,7 @@
using that by (auto simp: dist_norm)
qed
then show ?thesis
- using that by (simp add: dist_norm i_def BOX_def field_simps flip: scaleR_diff_right)
+ using that by (simp add: dist_norm i_def BOX_def flip: scaleR_diff_right) (simp add: field_simps)
qed
qed
qed
--- a/src/HOL/Analysis/Fashoda_Theorem.thy Mon Oct 07 21:51:31 2019 +0200
+++ b/src/HOL/Analysis/Fashoda_Theorem.thy Tue Oct 08 10:26:40 2019 +0000
@@ -17,8 +17,9 @@
lemma interval_bij_affine:
"interval_bij (a,b) (u,v) = (\<lambda>x. (\<Sum>i\<in>Basis. ((v\<bullet>i - u\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (x\<bullet>i)) *\<^sub>R i) +
(\<Sum>i\<in>Basis. (u\<bullet>i - (v\<bullet>i - u\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (a\<bullet>i)) *\<^sub>R i))"
- by (auto simp: sum.distrib[symmetric] scaleR_add_left[symmetric] interval_bij_def fun_eq_iff
- field_simps inner_simps add_divide_distrib[symmetric] intro!: sum.cong)
+ by (auto simp add: interval_bij_def sum.distrib [symmetric] scaleR_add_left [symmetric]
+ fun_eq_iff intro!: sum.cong)
+ (simp add: algebra_simps diff_divide_distrib [symmetric])
lemma continuous_interval_bij:
fixes a b :: "'a::euclidean_space"
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Mon Oct 07 21:51:31 2019 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Tue Oct 08 10:26:40 2019 +0000
@@ -3585,7 +3585,7 @@
proof
assume ?lhs
from has_integral_affinity'[OF this, of "1 / m" "-c /\<^sub>R m"] and \<open>m > 0\<close>
- show ?rhs by (simp add: field_simps vector_add_divide_simps)
+ show ?rhs by (simp add: vector_add_divide_simps) (simp add: field_simps)
next
assume ?rhs
from has_integral_affinity'[OF this, of m c] and \<open>m > 0\<close>
@@ -4253,7 +4253,7 @@
show "norm (?SUM p - integral {a..t} f) < e/3"
using d2_fin by blast
show "norm ((c - t) *\<^sub>R f c) < e/3"
- using w cwt \<open>t < c\<close> by (auto simp add: field_simps)
+ using w cwt \<open>t < c\<close> by simp (simp add: field_simps)
qed
then show ?thesis by simp
qed
--- a/src/HOL/Analysis/Homeomorphism.thy Mon Oct 07 21:51:31 2019 +0200
+++ b/src/HOL/Analysis/Homeomorphism.thy Tue Oct 08 10:26:40 2019 +0000
@@ -533,9 +533,8 @@
unfolding f_def using \<open>norm b = 1\<close> norm_eq_1
by (force simp: field_simps inner_add_right inner_diff_right)
moreover have "f ` T \<subseteq> T"
- unfolding f_def using assms
- apply (auto simp: field_simps inner_add_right inner_diff_right)
- by (metis add_0 diff_zero mem_affine_3_minus)
+ unfolding f_def using assms \<open>subspace T\<close>
+ by (auto simp add: inner_add_right inner_diff_right mem_affine_3_minus subspace_mul)
moreover have "{x. b\<bullet>x = 0} \<inter> T \<subseteq> f ` ({x. norm x = 1 \<and> b\<bullet>x \<noteq> 1} \<inter> T)"
apply clarify
apply (rule_tac x = "g x" in image_eqI, auto)
--- a/src/HOL/Analysis/Homotopy.thy Mon Oct 07 21:51:31 2019 +0200
+++ b/src/HOL/Analysis/Homotopy.thy Tue Oct 08 10:26:40 2019 +0000
@@ -4701,16 +4701,18 @@
assume x: "norm (x - a) \<le> r" and "x \<in> T"
have "\<exists>v \<in> {0..1}. ((1 - v) * r - norm ((x - a) - v *\<^sub>R (u - a))) \<bullet> 1 = 0"
by (rule ivt_decreasing_component_on_1) (auto simp: x continuous_intros)
- then obtain v where "0\<le>v" "v\<le>1" and v: "(1 - v) * r = norm ((x - a) - v *\<^sub>R (u - a))"
+ then obtain v where "0 \<le> v" "v \<le> 1"
+ and v: "(1 - v) * r = norm ((x - a) - v *\<^sub>R (u - a))"
by auto
+ then have n: "norm (a - (x - v *\<^sub>R (u - a))) = r - r * v"
+ by (simp add: field_simps norm_minus_commute)
show "x \<in> f ` (cball a r \<inter> T)"
proof (rule image_eqI)
show "x = f (x - v *\<^sub>R (u - a))"
- using \<open>r > 0\<close> v by (simp add: f_def field_simps)
+ using \<open>r > 0\<close> v by (simp add: f_def) (simp add: field_simps)
have "x - v *\<^sub>R (u - a) \<in> cball a r"
- using \<open>r > 0\<close> v \<open>0 \<le> v\<close>
- apply (simp add: field_simps dist_norm norm_minus_commute)
- by (metis le_add_same_cancel2 order.order_iff_strict zero_le_mult_iff)
+ using \<open>r > 0\<close>\<open>0 \<le> v\<close>
+ by (simp add: dist_norm n)
moreover have "x - v *\<^sub>R (u - a) \<in> T"
by (simp add: f_def \<open>affine T\<close> \<open>u \<in> T\<close> \<open>x \<in> T\<close> assms mem_affine_3_minus2)
ultimately show "x - v *\<^sub>R (u - a) \<in> cball a r \<inter> T"
--- a/src/HOL/Analysis/Path_Connected.thy Mon Oct 07 21:51:31 2019 +0200
+++ b/src/HOL/Analysis/Path_Connected.thy Tue Oct 08 10:26:40 2019 +0000
@@ -3307,7 +3307,7 @@
have "\<bar>norm (z + C *\<^sub>R (z-a)) - norm (C *\<^sub>R (z-a))\<bar> \<le> norm z"
by (metis add_diff_cancel norm_triangle_ineq3)
moreover have "norm (C *\<^sub>R (z-a)) > norm z + B"
- using zna \<open>B>0\<close> by (simp add: C_def le_max_iff_disj field_simps)
+ using zna \<open>B>0\<close> by (simp add: C_def le_max_iff_disj)
ultimately have C: "norm (z + C *\<^sub>R (z-a)) > B" by linarith
{ fix u::real
assume u: "0\<le>u" "u\<le>1" and ins: "(1 - u) *\<^sub>R z + u *\<^sub>R (z + C *\<^sub>R (z - a)) \<in> s"
--- a/src/HOL/Analysis/Starlike.thy Mon Oct 07 21:51:31 2019 +0200
+++ b/src/HOL/Analysis/Starlike.thy Tue Oct 08 10:26:40 2019 +0000
@@ -956,7 +956,7 @@
unfolding that(1) by (auto simp add:algebra_simps)
show "norm (a - x) *\<^sub>R (x - b) = norm (x - b) *\<^sub>R (a - x)"
unfolding norm_minus_commute[of x a] * using \<open>0 \<le> u\<close> \<open>u \<le> 1\<close>
- by (auto simp add: field_simps)
+ by simp
qed
moreover have "\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1" if "dist a b = dist a x + dist x b"
proof -
@@ -1160,8 +1160,7 @@
have "z \<in> interior S"
apply (rule interior_mono[OF d,unfolded subset_eq,rule_format])
unfolding interior_open[OF open_ball] mem_ball z_def dist_norm using y and assms(4,5)
- apply (auto simp add:field_simps norm_minus_commute)
- done
+ by simp (simp add: field_simps norm_minus_commute)
then show ?thesis
unfolding *
using mem_interior_convex_shrink \<open>y \<in> S\<close> assms by blast
@@ -5565,7 +5564,8 @@
have "e / norm (x - a) \<ge> k"
using k_def by linarith
then have "a + k *\<^sub>R (x - a) \<in> cball a e"
- using \<open>0 < k\<close> False by (simp add: dist_norm field_simps)
+ using \<open>0 < k\<close> False
+ by (simp add: dist_norm) (simp add: field_simps)
then have T: "a + k *\<^sub>R (x - a) \<in> T"
using e by blast
have S: "a + k *\<^sub>R (x - a) \<in> S"
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Mon Oct 07 21:51:31 2019 +0200
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Tue Oct 08 10:26:40 2019 +0000
@@ -132,7 +132,7 @@
also have "... = norm ((-1 - (r / norm (a - a'))) *\<^sub>R (a - a'))"
by (simp add: algebra_simps)
also from \<open>a \<noteq> a'\<close> have "... = \<bar>- norm (a - a') - r\<bar>"
- by (simp add: abs_mult_pos field_simps)
+ by simp (simp add: field_simps)
finally have [simp]: "norm (a' - (a + (r / norm (a - a')) *\<^sub>R (a - a'))) = \<bar>norm (a - a') + r\<bar>"
by linarith
from \<open>a \<noteq> a'\<close> show ?thesis
@@ -176,8 +176,10 @@
(metis \<open>0 \<le> r\<close> \<open>?lhs\<close> centre_in_cball dist_commute dist_norm less_asym mem_ball subset_eq)
then show ?thesis
using subsetD [where c = "a + (r' / norm(a - a') - 1) *\<^sub>R (a - a')", OF \<open>?lhs\<close>] \<open>a \<noteq> a'\<close>
- by (simp add: dist_norm field_simps)
- (simp add: diff_divide_distrib scaleR_left_diff_distrib)
+ apply (simp add: dist_norm)
+ apply (simp add: scaleR_left_diff_distrib)
+ apply (simp add: field_simps)
+ done
qed
then show ?thesis by force
qed
--- a/src/HOL/Complex.thy Mon Oct 07 21:51:31 2019 +0200
+++ b/src/HOL/Complex.thy Tue Oct 08 10:26:40 2019 +0000
@@ -480,7 +480,7 @@
((\<lambda>x. Re (f x)) has_field_derivative (Re x)) F \<and>
((\<lambda>x. Im (f x)) has_field_derivative (Im x)) F"
by (simp add: has_vector_derivative_def has_field_derivative_def has_derivative_def
- tendsto_complex_iff field_simps bounded_linear_scaleR_left bounded_linear_mult_right)
+ tendsto_complex_iff algebra_simps bounded_linear_scaleR_left bounded_linear_mult_right)
lemma has_field_derivative_Re[derivative_intros]:
"(f has_vector_derivative D) F \<Longrightarrow> ((\<lambda>x. Re (f x)) has_field_derivative (Re D)) F"
--- a/src/HOL/Modules.thy Mon Oct 07 21:51:31 2019 +0200
+++ b/src/HOL/Modules.thy Tue Oct 08 10:26:40 2019 +0000
@@ -86,8 +86,30 @@
lemma sum_constant_scale: "(\<Sum>x\<in>A. y) = scale (of_nat (card A)) y"
by (induct A rule: infinite_finite_induct) (simp_all add: algebra_simps)
+end
+
+setup \<open>Sign.add_const_constraint (\<^const_name>\<open>divide\<close>, SOME \<^typ>\<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>)\<close>
+
+context module
+begin
+
+lemma [field_simps]:
+ shows scale_left_distrib_NO_MATCH: "NO_MATCH (x div y) c \<Longrightarrow> (a + b) *s x = a *s x + b *s x"
+ and scale_right_distrib_NO_MATCH: "NO_MATCH (x div y) a \<Longrightarrow> a *s (x + y) = a *s x + a *s y"
+ and scale_left_diff_distrib_NO_MATCH: "NO_MATCH (x div y) c \<Longrightarrow> (a - b) *s x = a *s x - b *s x"
+ and scale_right_diff_distrib_NO_MATCH: "NO_MATCH (x div y) a \<Longrightarrow> a *s (x - y) = a *s x - a *s y"
+ by (rule scale_left_distrib scale_right_distrib scale_left_diff_distrib scale_right_diff_distrib)+
+
+end
+
+setup \<open>Sign.add_const_constraint (\<^const_name>\<open>divide\<close>, SOME \<^typ>\<open>'a::divide \<Rightarrow> 'a \<Rightarrow> 'a\<close>)\<close>
+
+
section \<open>Subspace\<close>
+context module
+begin
+
definition subspace :: "'b set \<Rightarrow> bool"
where "subspace S \<longleftrightarrow> 0 \<in> S \<and> (\<forall>x\<in>S. \<forall>y\<in>S. x + y \<in> S) \<and> (\<forall>c. \<forall>x\<in>S. c *s x \<in> S)"
--- a/src/HOL/Real_Vector_Spaces.thy Mon Oct 07 21:51:31 2019 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy Tue Oct 08 10:26:40 2019 +0000
@@ -113,6 +113,19 @@
lemmas scaleR_cancel_left = real_vector.scale_cancel_left
lemmas scaleR_cancel_right = real_vector.scale_cancel_right
+lemma [field_simps]:
+ "c \<noteq> 0 \<Longrightarrow> a = b /\<^sub>R c \<longleftrightarrow> c *\<^sub>R a = b"
+ "c \<noteq> 0 \<Longrightarrow> b /\<^sub>R c = a \<longleftrightarrow> b = c *\<^sub>R a"
+ "c \<noteq> 0 \<Longrightarrow> a + b /\<^sub>R c = (c *\<^sub>R a + b) /\<^sub>R c"
+ "c \<noteq> 0 \<Longrightarrow> a /\<^sub>R c + b = (a + c *\<^sub>R b) /\<^sub>R c"
+ "c \<noteq> 0 \<Longrightarrow> a - b /\<^sub>R c = (c *\<^sub>R a - b) /\<^sub>R c"
+ "c \<noteq> 0 \<Longrightarrow> a /\<^sub>R c - b = (a - c *\<^sub>R b) /\<^sub>R c"
+ "c \<noteq> 0 \<Longrightarrow> - (a /\<^sub>R c) + b = (- a + c *\<^sub>R b) /\<^sub>R c"
+ "c \<noteq> 0 \<Longrightarrow> - (a /\<^sub>R c) - b = (- a - c *\<^sub>R b) /\<^sub>R c"
+ for a b :: "'a :: real_vector"
+ by (auto simp add: scaleR_add_right scaleR_add_left scaleR_diff_right scaleR_diff_left)
+
+
text \<open>Legacy names\<close>
lemmas scaleR_left_distrib = scaleR_add_left
@@ -444,13 +457,15 @@
and scaleR_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> x \<Longrightarrow> a *\<^sub>R x \<le> b *\<^sub>R x"
begin
-lemma scaleR_mono: "a \<le> b \<Longrightarrow> x \<le> y \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> x \<Longrightarrow> a *\<^sub>R x \<le> b *\<^sub>R y"
- by (meson local.dual_order.trans local.scaleR_left_mono local.scaleR_right_mono)
-
-lemma scaleR_mono': "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c \<Longrightarrow> a *\<^sub>R c \<le> b *\<^sub>R d"
+lemma scaleR_mono:
+ "a \<le> b \<Longrightarrow> x \<le> y \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> x \<Longrightarrow> a *\<^sub>R x \<le> b *\<^sub>R y"
+ by (meson order_trans scaleR_left_mono scaleR_right_mono)
+
+lemma scaleR_mono':
+ "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c \<Longrightarrow> a *\<^sub>R c \<le> b *\<^sub>R d"
by (rule scaleR_mono) (auto intro: order.trans)
-lemma pos_le_divideR_eq:
+lemma pos_le_divideR_eq [field_simps]:
"a \<le> b /\<^sub>R c \<longleftrightarrow> c *\<^sub>R a \<le> b" (is "?P \<longleftrightarrow> ?Q") if "0 < c"
proof
assume ?P
@@ -466,35 +481,35 @@
by (simp add: scaleR_one scaleR_scaleR inverse_eq_divide)
qed
-lemma pos_less_divideR_eq:
+lemma pos_less_divideR_eq [field_simps]:
"a < b /\<^sub>R c \<longleftrightarrow> c *\<^sub>R a < b" if "c > 0"
using that pos_le_divideR_eq [of c a b]
by (auto simp add: le_less scaleR_scaleR scaleR_one)
-lemma pos_divideR_le_eq:
+lemma pos_divideR_le_eq [field_simps]:
"b /\<^sub>R c \<le> a \<longleftrightarrow> b \<le> c *\<^sub>R a" if "c > 0"
using that pos_le_divideR_eq [of "inverse c" b a] by simp
-lemma pos_divideR_less_eq:
+lemma pos_divideR_less_eq [field_simps]:
"b /\<^sub>R c < a \<longleftrightarrow> b < c *\<^sub>R a" if "c > 0"
using that pos_less_divideR_eq [of "inverse c" b a] by simp
-lemma pos_le_minus_divideR_eq:
+lemma pos_le_minus_divideR_eq [field_simps]:
"a \<le> - (b /\<^sub>R c) \<longleftrightarrow> c *\<^sub>R a \<le> - b" if "c > 0"
using that by (metis add_minus_cancel diff_0 left_minus minus_minus neg_le_iff_le
scaleR_add_right uminus_add_conv_diff pos_le_divideR_eq)
-lemma pos_less_minus_divideR_eq:
+lemma pos_less_minus_divideR_eq [field_simps]:
"a < - (b /\<^sub>R c) \<longleftrightarrow> c *\<^sub>R a < - b" if "c > 0"
using that by (metis le_less less_le_not_le pos_divideR_le_eq
pos_divideR_less_eq pos_le_minus_divideR_eq)
-lemma pos_minus_divideR_le_eq:
+lemma pos_minus_divideR_le_eq [field_simps]:
"- (b /\<^sub>R c) \<le> a \<longleftrightarrow> - b \<le> c *\<^sub>R a" if "c > 0"
using that by (metis pos_divideR_le_eq pos_le_minus_divideR_eq that
inverse_positive_iff_positive le_imp_neg_le minus_minus)
-lemma pos_minus_divideR_less_eq:
+lemma pos_minus_divideR_less_eq [field_simps]:
"- (b /\<^sub>R c) < a \<longleftrightarrow> - b < c *\<^sub>R a" if "c > 0"
using that by (simp add: less_le_not_le pos_le_minus_divideR_eq pos_minus_divideR_le_eq)
@@ -506,32 +521,32 @@
end
-lemma neg_le_divideR_eq:
+lemma neg_le_divideR_eq [field_simps]:
"a \<le> b /\<^sub>R c \<longleftrightarrow> b \<le> c *\<^sub>R a" (is "?P \<longleftrightarrow> ?Q") if "c < 0"
for a b :: "'a :: ordered_real_vector"
using that pos_le_divideR_eq [of "- c" a "- b"] by simp
-lemma neg_less_divideR_eq:
+lemma neg_less_divideR_eq [field_simps]:
"a < b /\<^sub>R c \<longleftrightarrow> b < c *\<^sub>R a" if "c < 0"
for a b :: "'a :: ordered_real_vector"
using that neg_le_divideR_eq [of c a b] by (auto simp add: le_less)
-lemma neg_divideR_le_eq:
+lemma neg_divideR_le_eq [field_simps]:
"b /\<^sub>R c \<le> a \<longleftrightarrow> c *\<^sub>R a \<le> b" if "c < 0"
for a b :: "'a :: ordered_real_vector"
using that pos_divideR_le_eq [of "- c" "- b" a] by simp
-lemma neg_divideR_less_eq:
+lemma neg_divideR_less_eq [field_simps]:
"b /\<^sub>R c < a \<longleftrightarrow> c *\<^sub>R a < b" if "c < 0"
for a b :: "'a :: ordered_real_vector"
using that neg_divideR_le_eq [of c b a] by (auto simp add: le_less)
-lemma neg_le_minus_divideR_eq:
+lemma neg_le_minus_divideR_eq [field_simps]:
"a \<le> - (b /\<^sub>R c) \<longleftrightarrow> - b \<le> c *\<^sub>R a" if "c < 0"
for a b :: "'a :: ordered_real_vector"
using that pos_le_minus_divideR_eq [of "- c" a "- b"] by (simp add: minus_le_iff)
-lemma neg_less_minus_divideR_eq:
+lemma neg_less_minus_divideR_eq [field_simps]:
"a < - (b /\<^sub>R c) \<longleftrightarrow> - b < c *\<^sub>R a" if "c < 0"
for a b :: "'a :: ordered_real_vector"
proof -
@@ -541,12 +556,12 @@
show ?thesis by (auto simp add: le_less *)
qed
-lemma neg_minus_divideR_le_eq:
+lemma neg_minus_divideR_le_eq [field_simps]:
"- (b /\<^sub>R c) \<le> a \<longleftrightarrow> c *\<^sub>R a \<le> - b" if "c < 0"
for a b :: "'a :: ordered_real_vector"
using that pos_minus_divideR_le_eq [of "- c" "- b" a] by (simp add: le_minus_iff)
-lemma neg_minus_divideR_less_eq:
+lemma neg_minus_divideR_less_eq [field_simps]:
"- (b /\<^sub>R c) < a \<longleftrightarrow> c *\<^sub>R a < - b" if "c < 0"
for a b :: "'a :: ordered_real_vector"
using that by (simp add: less_le_not_le neg_le_minus_divideR_eq neg_minus_divideR_le_eq)
--- a/src/HOL/Vector_Spaces.thy Mon Oct 07 21:51:31 2019 +0200
+++ b/src/HOL/Vector_Spaces.thy Tue Oct 08 10:26:40 2019 +0000
@@ -66,7 +66,7 @@
context vector_space begin
sublocale module scale rewrites "module_hom = linear"
- by (unfold_locales) (fact vector_space_assms module_hom_eq_linear)+
+ by unfold_locales (fact vector_space_assms module_hom_eq_linear)+
lemmas\<comment> \<open>from \<open>module\<close>\<close>
linear_id = module_hom_id