# HG changeset patch
# User nipkow
# Date 1575036364 -3600
# Node ID 7fac205dd73725f01081c1dbc6c323c584064cf1
# Parent  caede3159e237761e65b262b65915f9b89bce333
tuned

diff -r caede3159e23 -r 7fac205dd737 src/HOL/Analysis/Abstract_Topology_2.thy
--- a/src/HOL/Analysis/Abstract_Topology_2.thy	Fri Nov 29 11:04:47 2019 +0100
+++ b/src/HOL/Analysis/Abstract_Topology_2.thy	Fri Nov 29 15:06:04 2019 +0100
@@ -706,7 +706,7 @@
   unfolding continuous_map_openin_preimage_eq
 proof (intro conjI allI impI)
   show "g ` topspace X \<subseteq> topspace Y"
-    using g cont continuous_map_image_subset_topspace topspace_subtopology by fastforce
+    using g cont continuous_map_image_subset_topspace by fastforce
 next
   fix U
   assume Y: "openin Y U"
@@ -747,7 +747,7 @@
   unfolding continuous_map_closedin_preimage_eq
 proof (intro conjI allI impI)
   show "g ` topspace X \<subseteq> topspace Y"
-    using g cont continuous_map_image_subset_topspace topspace_subtopology by fastforce
+    using g cont continuous_map_image_subset_topspace by fastforce
 next
   fix U
   assume Y: "closedin Y U"
diff -r caede3159e23 -r 7fac205dd737 src/HOL/Analysis/Convex.thy
--- a/src/HOL/Analysis/Convex.thy	Fri Nov 29 11:04:47 2019 +0100
+++ b/src/HOL/Analysis/Convex.thy	Fri Nov 29 15:06:04 2019 +0100
@@ -1998,7 +1998,7 @@
 
 lemma convex_hull_subset:
     "s \<subseteq> convex hull t \<Longrightarrow> convex hull s \<subseteq> convex hull t"
-  by (simp add: convex_convex_hull subset_hull)
+  by (simp add: subset_hull)
 
 lemma convex_hull_eq: "convex hull s = s \<longleftrightarrow> convex s"
   by (metis convex_convex_hull hull_same)
diff -r caede3159e23 -r 7fac205dd737 src/HOL/Analysis/Derivative.thy
--- a/src/HOL/Analysis/Derivative.thy	Fri Nov 29 11:04:47 2019 +0100
+++ b/src/HOL/Analysis/Derivative.thy	Fri Nov 29 15:06:04 2019 +0100
@@ -2441,7 +2441,7 @@
   moreover
   have ev_dist: "\<forall>\<^sub>F xy in at (x, y) within X \<times> Y. dist xy (x, y) < d" if "d > 0" for d
     using eventually_at_ball[OF that]
-    by (rule eventually_elim2) (auto simp: dist_commute mem_ball intro!: eventually_True)
+    by (rule eventually_elim2) (auto simp: dist_commute intro!: eventually_True)
   note ev_dist[OF \<open>0 < d\<close>]
   ultimately
   have "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y.
diff -r caede3159e23 -r 7fac205dd737 src/HOL/Analysis/Elementary_Metric_Spaces.thy
--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Fri Nov 29 11:04:47 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Fri Nov 29 15:06:04 2019 +0100
@@ -63,7 +63,7 @@
   by (simp add: subset_eq)
 
 lemma mem_ball_imp_mem_cball: "x \<in> ball y e \<Longrightarrow> x \<in> cball y e"
-  by (auto simp: mem_ball mem_cball)
+  by (auto)
 
 lemma sphere_cball [simp,intro]: "sphere z r \<subseteq> cball z r"
   by force
@@ -78,10 +78,10 @@
   by (simp add: subset_eq)
 
 lemma mem_ball_leI: "x \<in> ball y e \<Longrightarrow> e \<le> f \<Longrightarrow> x \<in> ball y f"
-  by (auto simp: mem_ball mem_cball)
+  by (auto)
 
 lemma mem_cball_leI: "x \<in> cball y e \<Longrightarrow> e \<le> f \<Longrightarrow> x \<in> cball y f"
-  by (auto simp: mem_ball mem_cball)
+  by (auto)
 
 lemma cball_trans: "y \<in> cball z b \<Longrightarrow> x \<in> cball y a \<Longrightarrow> x \<in> cball z (b + a)"
   by metric
@@ -177,7 +177,7 @@
 lemma atLeastAtMost_eq_cball:
   fixes a b::real
   shows "{a .. b} = cball ((a + b)/2) ((b - a)/2)"
-  by (auto simp: dist_real_def field_simps mem_cball)
+  by (auto simp: dist_real_def field_simps)
 
 lemma cball_eq_atLeastAtMost:
   fixes a b::real
@@ -187,7 +187,7 @@
 lemma greaterThanLessThan_eq_ball:
   fixes a b::real
   shows "{a <..< b} = ball ((a + b)/2) ((b - a)/2)"
-  by (auto simp: dist_real_def field_simps mem_ball)
+  by (auto simp: dist_real_def field_simps)
 
 lemma ball_eq_greaterThanLessThan:
   fixes a b::real
@@ -251,7 +251,7 @@
   apply (drule_tac x="e/2" in spec)
   apply (auto simp: simp del: less_divide_eq_numeral1)
   apply (drule_tac x="dist x' x" in spec)
-  apply (auto simp: zero_less_dist_iff simp del: less_divide_eq_numeral1)
+  apply (auto simp del: less_divide_eq_numeral1)
   apply metric
   done
 
@@ -1713,7 +1713,7 @@
         fix r :: real and N n m
         assume "1 / Suc N < r" "Suc N \<le> n" "Suc N \<le> m"
         then have "(f \<circ> t) n \<in> F (Suc N)" "(f \<circ> t) m \<in> F (Suc N)" "2 * e N < r"
-          using F_dec t by (auto simp: e_def field_simps of_nat_Suc)
+          using F_dec t by (auto simp: e_def field_simps)
         with F[of N] obtain x where "dist x ((f \<circ> t) n) < e N" "dist x ((f \<circ> t) m) < e N"
           by (auto simp: subset_eq)
         with \<open>2 * e N < r\<close> show "dist ((f \<circ> t) m) ((f \<circ> t) n) < r"
@@ -3164,7 +3164,7 @@
     apply (rule antisym)
      using False closure_subset apply (blast intro: setdist_subset_left)
     using False *
-    apply (force simp add: closure_eq_empty intro!: le_setdistI)
+    apply (force intro!: le_setdistI)
     done
 qed
 
diff -r caede3159e23 -r 7fac205dd737 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Fri Nov 29 11:04:47 2019 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Fri Nov 29 15:06:04 2019 +0100
@@ -1779,7 +1779,7 @@
       have 0: "0 \<le> prj1 (vf X - uf X)"
         using \<open>X \<in> \<D>\<close> prj1_def vu_pos by fastforce
       have "(measure lebesgue \<circ> fbx) X \<le> (2 * B * DIM('M)) ^ DIM('N) * content (cbox (uf X) (vf X))"
-        apply (simp add: fbx_def content_cbox_cases algebra_simps BM_ge0 \<open>X \<in> \<D>'\<close> prod_constant)
+        apply (simp add: fbx_def content_cbox_cases algebra_simps BM_ge0 \<open>X \<in> \<D>'\<close>)
         apply (simp add: power_mult_distrib \<open>0 < B\<close> prj1_eq [symmetric])
         using MleN 0 1 uvz \<open>X \<in> \<D>\<close>
         apply (fastforce simp add: box_ne_empty power_decreasing)
diff -r caede3159e23 -r 7fac205dd737 src/HOL/Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Fri Nov 29 11:04:47 2019 +0100
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Fri Nov 29 15:06:04 2019 +0100
@@ -796,8 +796,7 @@
              [@{thm plus_vec_def}, @{thm times_vec_def},
               @{thm minus_vec_def}, @{thm uminus_vec_def},
               @{thm one_vec_def}, @{thm zero_vec_def}, @{thm vec_def},
-              @{thm scaleR_vec_def},
-              @{thm vec_lambda_beta}, @{thm vector_scalar_mult_def}])
+              @{thm scaleR_vec_def}, @{thm vector_scalar_mult_def}])
   fun vector_arith_tac ctxt ths =
     simp_tac (put_simpset ss1 ctxt)
     THEN' (fn i => resolve_tac ctxt @{thms Finite_Cartesian_Product.sum_cong_aux} i
diff -r caede3159e23 -r 7fac205dd737 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Nov 29 11:04:47 2019 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Nov 29 15:06:04 2019 +0100
@@ -3492,7 +3492,7 @@
       by (simp add: inner_simps field_simps)
     ultimately show ?thesis
       by (simp add: image_affinity_cbox True content_cbox'
-        prod.distrib prod_constant inner_diff_left)
+        prod.distrib inner_diff_left)
   next
     case False
     with \<open>cbox a b \<noteq> {}\<close> have "cbox (m *\<^sub>R b + c) (m *\<^sub>R a + c) \<noteq> {}"
diff -r caede3159e23 -r 7fac205dd737 src/HOL/Analysis/Lipschitz.thy
--- a/src/HOL/Analysis/Lipschitz.thy	Fri Nov 29 11:04:47 2019 +0100
+++ b/src/HOL/Analysis/Lipschitz.thy	Fri Nov 29 15:06:04 2019 +0100
@@ -544,7 +544,7 @@
   show "\<exists>u>0. \<exists>L. \<forall>t\<in>cball t u \<inter> T. L-lipschitz_on  (cball x u \<inter> X) (f (g t))"
     using d \<open>0 < u\<close>
     by (fastforce intro: exI[where x="(min d u)/2"] exI[where x=L]
-      intro!: less_imp_le[OF d(2)] lipschitz_on_subset[OF l] simp: dist_commute mem_ball mem_cball)
+      intro!: less_imp_le[OF d(2)] lipschitz_on_subset[OF l] simp: dist_commute)
 qed
 
 context
@@ -610,7 +610,7 @@
     finally have "dist x a < u" .
     then have "x \<in> cball a u \<inter> T"
       using \<open>x \<in> T\<close>
-      by (auto simp: dist_commute mem_cball)
+      by (auto simp: dist_commute)
     have "dist (f x y) (f a b) \<le> dist (f x y) (f x b) + dist (f x b) (f a b)"
       by (rule dist_triangle)
     also have "(L + 1)-lipschitz_on (cball b u \<inter> X) (f x)"
@@ -711,7 +711,7 @@
       "eventually (\<lambda>n. ?t n \<in> ball lt u) sequentially"
       "eventually (\<lambda>n. ?y n \<in> ball lx u) sequentially"
       "eventually (\<lambda>n. ?x n \<in> ball lx u) sequentially"
-      by (auto simp: dist_commute Lim mem_ball)
+      by (auto simp: dist_commute Lim)
     moreover have "eventually (\<lambda>n. n > L) sequentially"
       by (metis filterlim_at_top_dense filterlim_real_sequentially)
     ultimately
@@ -721,7 +721,7 @@
       hence "dist (f (?t n) (?y n)) (f (?t n) (?x n)) \<le> L * dist (?y n) (?x n)"
         using assms xy t
         unfolding dist_norm[symmetric]
-        by (intro lipschitz_onD[OF L(2)]) (auto simp: mem_ball mem_cball)
+        by (intro lipschitz_onD[OF L(2)]) (auto)
       also have "\<dots> \<le> n * dist (?y n) (?x n)"
         using elim by (intro mult_right_mono) auto
       also have "\<dots> \<le> rx (ry (rt n)) * dist (?y n) (?x n)"
@@ -772,7 +772,7 @@
     by metis
   then show "\<exists>u>0. \<exists>L. \<forall>t\<in>cball t u \<inter> A. L-lipschitz_on (cball x u \<inter> B) (\<lambda>b. (f t b, g t b))"
     by (intro exI[where x="min u v"])
-      (force intro: lipschitz_on_subset intro!: lipschitz_on_Pair simp: mem_cball)
+      (force intro: lipschitz_on_subset intro!: lipschitz_on_Pair)
 qed
 
 lemma local_lipschitz_constI: "local_lipschitz S T (\<lambda>t x. f t)"
@@ -809,7 +809,7 @@
   then have "compact (f' ` (cball t v \<times> cball x u))"
     by (auto intro!: compact_continuous_image continuous_on_subset[OF cont_f'])
   then obtain B where B: "B > 0" "\<And>s y. s \<in> cball t v \<Longrightarrow> y \<in> cball x u \<Longrightarrow> norm (f' (s, y)) \<le> B"
-    by (auto dest!: compact_imp_bounded simp: bounded_pos simp: mem_ball)
+    by (auto dest!: compact_imp_bounded simp: bounded_pos)
 
   have lipschitz: "B-lipschitz_on (cball x (min u v) \<inter> X) (f s)" if s: "s \<in> cball t v" for s
   proof -
@@ -824,13 +824,13 @@
       for y z
       using s that
       by (intro differentiable_bound[OF convex_cball deriv])
-        (auto intro!: B  simp: norm_blinfun.rep_eq[symmetric] mem_cball)
+        (auto intro!: B  simp: norm_blinfun.rep_eq[symmetric])
     then show ?thesis
       using \<open>0 < B\<close>
-      by (auto intro!: lipschitz_onI simp: dist_norm mem_cball)
+      by (auto intro!: lipschitz_onI simp: dist_norm)
   qed
   show "\<exists>u>0. \<exists>L. \<forall>t\<in>cball t u \<inter> T. L-lipschitz_on (cball x u \<inter> X) (f t)"
-    by (force intro: exI[where x="min u v"] exI[where x=B] intro!: lipschitz simp: u v mem_cball)
+    by (force intro: exI[where x="min u v"] exI[where x=B] intro!: lipschitz simp: u v)
 qed
 
 end
diff -r caede3159e23 -r 7fac205dd737 src/HOL/Analysis/Product_Vector.thy
--- a/src/HOL/Analysis/Product_Vector.thy	Fri Nov 29 11:04:47 2019 +0100
+++ b/src/HOL/Analysis/Product_Vector.thy	Fri Nov 29 15:06:04 2019 +0100
@@ -522,8 +522,7 @@
 
 lemma dimension_pair: "p.dimension = vs1.dimension + vs2.dimension"
   using dim_Times[OF vs1.subspace_UNIV vs2.subspace_UNIV]
-  by (auto simp: p.dim_UNIV vs1.dim_UNIV vs2.dim_UNIV
-      p.dimension_def vs1.dimension_def vs2.dimension_def)
+  by (auto simp: p.dimension_def vs1.dimension_def vs2.dimension_def)
 
 end
 
diff -r caede3159e23 -r 7fac205dd737 src/HOL/Analysis/Riemann_Mapping.thy
--- a/src/HOL/Analysis/Riemann_Mapping.thy	Fri Nov 29 11:04:47 2019 +0100
+++ b/src/HOL/Analysis/Riemann_Mapping.thy	Fri Nov 29 15:06:04 2019 +0100
@@ -99,7 +99,7 @@
                 "\<And>z. z \<in> ball 0 1 \<Longrightarrow> g (f z) = z"
 proof
   show "Moebius_function 0 a holomorphic_on ball 0 1"  "Moebius_function 0 (-a) holomorphic_on ball 0 1"
-    using Moebius_function_holomorphic assms mem_ball_0 by auto
+    using Moebius_function_holomorphic assms by auto
   show "Moebius_function 0 a a = 0"
     by (simp add: Moebius_function_eq_zero)
   show "Moebius_function 0 a ` ball 0 1 \<subseteq> ball 0 1"
diff -r caede3159e23 -r 7fac205dd737 src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Fri Nov 29 11:04:47 2019 +0100
+++ b/src/HOL/Analysis/Starlike.thy	Fri Nov 29 15:06:04 2019 +0100
@@ -1143,7 +1143,7 @@
       hence *: "0 < e/norm(z-x)" using e False by auto
       define y where "y = z + (e/norm(z-x)) *\<^sub>R (z-x)"
       have yball: "y \<in> cball z e"
-        using mem_cball y_def dist_norm[of z y] e by auto
+        using y_def dist_norm[of z y] e by auto
       have "x \<in> affine hull closure S"
         using x rel_interior_subset_closure hull_inc[of x "closure S"] by blast
       moreover have "z \<in> affine hull closure S"
diff -r caede3159e23 -r 7fac205dd737 src/HOL/Library/Cardinality.thy
--- a/src/HOL/Library/Cardinality.thy	Fri Nov 29 11:04:47 2019 +0100
+++ b/src/HOL/Library/Cardinality.thy	Fri Nov 29 15:06:04 2019 +0100
@@ -236,7 +236,7 @@
 instance
   by standard
     (auto simp add: finite_UNIV_integer_def card_UNIV_integer_def card_eq_0_iff
-      type_definition.univ [OF type_definition_integer] infinite_UNIV_int
+      type_definition.univ [OF type_definition_integer]
       dest!: finite_imageD intro: inj_onI)
 end