# HG changeset patch
# User haftmann
# Date 1570530400 0
# Node ID 160eaf566bcb5581995b4c25d19ecf2b61ef12ff
# Parent  5352449209b11d75e65e54279947900b46fed87b
formally augmented corresponding rules for field_simps

diff -r 5352449209b1 -r 160eaf566bcb src/HOL/Analysis/Brouwer_Fixpoint.thy
--- 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)
diff -r 5352449209b1 -r 160eaf566bcb src/HOL/Analysis/Change_Of_Vars.thy
--- 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>
diff -r 5352449209b1 -r 160eaf566bcb src/HOL/Analysis/Convex_Euclidean_Space.thy
--- 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
diff -r 5352449209b1 -r 160eaf566bcb src/HOL/Analysis/Derivative.thy
--- 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)
diff -r 5352449209b1 -r 160eaf566bcb src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- 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)
diff -r 5352449209b1 -r 160eaf566bcb src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy
--- 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
diff -r 5352449209b1 -r 160eaf566bcb src/HOL/Analysis/Fashoda_Theorem.thy
--- 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"
diff -r 5352449209b1 -r 160eaf566bcb src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- 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
diff -r 5352449209b1 -r 160eaf566bcb src/HOL/Analysis/Homeomorphism.thy
--- 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)
diff -r 5352449209b1 -r 160eaf566bcb src/HOL/Analysis/Homotopy.thy
--- 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"
diff -r 5352449209b1 -r 160eaf566bcb src/HOL/Analysis/Path_Connected.thy
--- 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"
diff -r 5352449209b1 -r 160eaf566bcb src/HOL/Analysis/Starlike.thy
--- 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"
diff -r 5352449209b1 -r 160eaf566bcb src/HOL/Analysis/Topology_Euclidean_Space.thy
--- 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
diff -r 5352449209b1 -r 160eaf566bcb src/HOL/Complex.thy
--- 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"
diff -r 5352449209b1 -r 160eaf566bcb src/HOL/Modules.thy
--- 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)"
 
diff -r 5352449209b1 -r 160eaf566bcb src/HOL/Real_Vector_Spaces.thy
--- 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)
diff -r 5352449209b1 -r 160eaf566bcb src/HOL/Vector_Spaces.thy
--- 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