# HG changeset patch
# User nipkow
# Date 1574978782 -3600
# Node ID 575b3a818de59d5d1d43ef3833f6e8d2a3114b5c
# Parent  a25b6f79043f29a93f050e76f99dde01881ea995
tuned

diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Abstract_Euclidean_Space.thy
--- a/src/HOL/Analysis/Abstract_Euclidean_Space.thy	Thu Nov 28 20:38:07 2019 +0100
+++ b/src/HOL/Analysis/Abstract_Euclidean_Space.thy	Thu Nov 28 23:06:22 2019 +0100
@@ -144,7 +144,7 @@
     unfolding homeomorphic_space_def homeomorphic_maps_def
     apply (rule_tac x="\<lambda>f. restrict f {..<n}" in exI)
     apply (rule_tac x="\<lambda>f i. if i < n then f i else 0" in exI)
-    apply (simp add: Euclidean_space_def topspace_subtopology continuous_map_in_subtopology)
+    apply (simp add: Euclidean_space_def continuous_map_in_subtopology)
     apply (intro conjI continuous_map_from_subtopology)
        apply (force simp: continuous_map_componentwise cm intro: continuous_map_product_projection)+
     done
@@ -247,7 +247,7 @@
   define p:: "nat \<Rightarrow> real" where "p \<equiv> \<lambda>i. if i = k then 1 else 0"
   have "p \<in> topspace(nsphere n)"
     using assms
-    by (simp add: nsphere topspace_subtopology p_def power2_eq_square if_distrib [where f = "\<lambda>x. x * _"] cong: if_cong)
+    by (simp add: nsphere p_def power2_eq_square if_distrib [where f = "\<lambda>x. x * _"] cong: if_cong)
   let ?g = "\<lambda>x i. x i / sqrt(\<Sum>j\<le>n. x j ^ 2)"
   let ?h = "\<lambda>(t,q) i. (1 - t) * q i + t * p i"
   let ?Y = "subtopology (Euclidean_space (Suc n)) {x. 0 \<le> x k \<and> (\<exists>i\<le>n. x i \<noteq> 0)}"
@@ -262,7 +262,7 @@
       by (metis add.commute add_le_same_cancel2 diff_ge_0_iff_ge diff_zero less_eq_real_def mult_eq_0_iff mult_nonneg_nonneg not_le numeral_One zero_neq_numeral)
     show "continuous_map (prod_topology (top_of_set {0..1}) (subtopology (nsphere n) {x. 0 \<le> x k})) ?Y ?h"
       using assms
-      apply (auto simp: * nsphere topspace_subtopology continuous_map_componentwise_UNIV
+      apply (auto simp: * nsphere continuous_map_componentwise_UNIV
                prod_topology_subtopology subtopology_subtopology case_prod_unfold
                continuous_map_in_subtopology Euclidean_space_def p_def if_distrib [where f = "\<lambda>x. _ * x"] cong: if_cong)
       apply (intro continuous_map_prod_snd continuous_intros continuous_map_from_subtopology)
@@ -286,7 +286,7 @@
   moreover have "(?g \<circ> ?h) (0, x) = x"
     if "x \<in> topspace (subtopology (nsphere n) {x. 0 \<le> x k})" for x
     using that
-    by (simp add: assms topspace_subtopology nsphere)
+    by (simp add: assms nsphere)
   moreover
   have "(?g \<circ> ?h) (1, x) = p"
     if "x \<in> topspace (subtopology (nsphere n) {x. 0 \<le> x k})" for x
diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Abstract_Limits.thy
--- a/src/HOL/Analysis/Abstract_Limits.thy	Thu Nov 28 20:38:07 2019 +0100
+++ b/src/HOL/Analysis/Abstract_Limits.thy	Thu Nov 28 23:06:22 2019 +0100
@@ -79,16 +79,16 @@
     have "\<forall>\<^sub>F b in F. f b \<in> topspace X \<inter> S"
       by (metis (no_types) limitin_def openin_topspace topspace_subtopology)
     with L show ?rhs
-      apply (clarsimp simp add: limitin_def eventually_mono topspace_subtopology openin_subtopology_alt)
+      apply (clarsimp simp add: limitin_def eventually_mono openin_subtopology_alt)
       apply (drule_tac x="S \<inter> U" in spec, force simp: elim: eventually_mono)
       done
   next
     assume ?rhs
     then show ?lhs
       using eventually_elim2
-      by (fastforce simp add: limitin_def topspace_subtopology openin_subtopology_alt)
+      by (fastforce simp add: limitin_def openin_subtopology_alt)
   qed
-qed (auto simp: limitin_def topspace_subtopology)
+qed (auto simp: limitin_def)
 
 
 lemma limitin_canonical_iff_gen [simp]:
diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Abstract_Topology.thy
--- a/src/HOL/Analysis/Abstract_Topology.thy	Thu Nov 28 20:38:07 2019 +0100
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Thu Nov 28 23:06:22 2019 +0100
@@ -299,7 +299,7 @@
 
 lemma topspace_subtopology_subset:
    "S \<subseteq> topspace X \<Longrightarrow> topspace(subtopology X S) = S"
-  by (simp add: inf.absorb_iff2 topspace_subtopology)
+  by (simp add: inf.absorb_iff2)
 
 lemma closedin_subtopology: "closedin (subtopology U V) S \<longleftrightarrow> (\<exists>T. closedin U T \<and> S = T \<inter> V)"
   unfolding closedin_def topspace_subtopology
@@ -391,7 +391,7 @@
 
 lemma closedin_imp_subset:
    "closedin (subtopology U S) T \<Longrightarrow> T \<subseteq> S"
-by (simp add: closedin_def topspace_subtopology)
+by (simp add: closedin_def)
 
 lemma openin_open_subtopology:
      "openin X S \<Longrightarrow> openin (subtopology X S) T \<longleftrightarrow> openin X T \<and> T \<subseteq> S"
@@ -436,7 +436,7 @@
   by (force simp: topspace_def)
 
 lemma topspace_euclidean_subtopology[simp]: "topspace (top_of_set S) = S"
-  by (simp add: topspace_subtopology)
+  by (simp)
 
 lemma closed_closedin: "closed S \<longleftrightarrow> closedin euclidean S"
   by (simp add: closed_def closedin_def Compl_eq_Diff_UNIV)
@@ -623,7 +623,7 @@
 
 lemma derived_set_of_subtopology:
    "(subtopology X U) derived_set_of S = U \<inter> (X derived_set_of (U \<inter> S))"
-  by (simp add: derived_set_of_def openin_subtopology topspace_subtopology) blast
+  by (simp add: derived_set_of_def openin_subtopology) blast
 
 lemma derived_set_of_subset_subtopology:
    "(subtopology X S) derived_set_of T \<subseteq> S"
@@ -666,7 +666,7 @@
 lemma subtopology_eq_discrete_topology_eq:
    "subtopology X U = discrete_topology U \<longleftrightarrow> U \<subseteq> topspace X \<and> U \<inter> X derived_set_of U = {}"
   using discrete_topology_unique_derived_set [of U "subtopology X U"]
-  by (auto simp: eq_commute topspace_subtopology derived_set_of_subtopology)
+  by (auto simp: eq_commute derived_set_of_subtopology)
 
 lemma subtopology_eq_discrete_topology:
    "S \<subseteq> topspace X \<and> S \<inter> X derived_set_of S = {}
@@ -816,7 +816,7 @@
 lemma closedin_derived_set:
      "closedin (subtopology X T) S \<longleftrightarrow>
       S \<subseteq> topspace X \<and> S \<subseteq> T \<and> (\<forall>x. x \<in> X derived_set_of S \<and> x \<in> T \<longrightarrow> x \<in> S)"
-  by (auto simp: closedin_contains_derived_set topspace_subtopology derived_set_of_subtopology Int_absorb1)
+  by (auto simp: closedin_contains_derived_set derived_set_of_subtopology Int_absorb1)
 
 lemma closedin_Int_closure_of:
      "closedin (subtopology X S) T \<longleftrightarrow> S \<inter> X closure_of T = T"
@@ -1348,7 +1348,7 @@
     with fin show "finite {U \<in> \<A>. U \<inter> (S \<inter> V) \<noteq> {}}"
       using finite_subset by auto
     show "x \<in> S \<inter> V"
-      using x \<open>x \<in> V\<close> by (simp add: topspace_subtopology)
+      using x \<open>x \<in> V\<close> by (simp)
   qed
 next
   show "\<And>x A. \<lbrakk>x \<in> A; A \<in> \<A>\<rbrakk> \<Longrightarrow> x \<in> topspace (subtopology X S)"
@@ -1672,13 +1672,13 @@
   show ?lhs
     using R
     unfolding continuous_map
-    by (auto simp: topspace_subtopology openin_subtopology eq)
+    by (auto simp: openin_subtopology eq)
 qed
 
 
 lemma continuous_map_from_subtopology:
      "continuous_map X X' f \<Longrightarrow> continuous_map (subtopology X S) X' f"
-  by (auto simp: continuous_map topspace_subtopology openin_subtopology)
+  by (auto simp: continuous_map openin_subtopology)
 
 lemma continuous_map_into_fulltopology:
    "continuous_map X (subtopology X' T) f \<Longrightarrow> continuous_map X X' f"
@@ -2134,17 +2134,17 @@
     unfolding quotient_map_def
   proof (intro conjI allI impI)
     show "f ` topspace (subtopology X U) = topspace (subtopology Y V)"
-      using sub U fim by (auto simp: topspace_subtopology)
+      using sub U fim by (auto)
   next
     fix Y' :: "'b set"
     assume "Y' \<subseteq> topspace (subtopology Y V)"
     then have "Y' \<subseteq> topspace Y" "Y' \<subseteq> V"
-      by (simp_all add: topspace_subtopology)
+      by (simp_all)
     then have eq: "{x \<in> topspace X. x \<in> U \<and> f x \<in> Y'} = {x \<in> topspace X. f x \<in> Y'}"
       using U by blast
     then show "openin (subtopology X U) {x \<in> topspace (subtopology X U). f x \<in> Y'} = openin (subtopology Y V) Y'"
       using U V Y \<open>openin X U\<close>  \<open>Y' \<subseteq> topspace Y\<close> \<open>Y' \<subseteq> V\<close>
-      by (simp add: topspace_subtopology openin_open_subtopology eq) (auto simp: openin_closedin_eq)
+      by (simp add: openin_open_subtopology eq) (auto simp: openin_closedin_eq)
   qed
 next
   assume V: "closedin Y V"
@@ -2159,17 +2159,17 @@
     unfolding quotient_map_closedin
   proof (intro conjI allI impI)
     show "f ` topspace (subtopology X U) = topspace (subtopology Y V)"
-      using sub U fim by (auto simp: topspace_subtopology)
+      using sub U fim by (auto)
   next
     fix Y' :: "'b set"
     assume "Y' \<subseteq> topspace (subtopology Y V)"
     then have "Y' \<subseteq> topspace Y" "Y' \<subseteq> V"
-      by (simp_all add: topspace_subtopology)
+      by (simp_all)
     then have eq: "{x \<in> topspace X. x \<in> U \<and> f x \<in> Y'} = {x \<in> topspace X. f x \<in> Y'}"
       using U by blast
     then show "closedin (subtopology X U) {x \<in> topspace (subtopology X U). f x \<in> Y'} = closedin (subtopology Y V) Y'"
       using U V Y \<open>closedin X U\<close>  \<open>Y' \<subseteq> topspace Y\<close> \<open>Y' \<subseteq> V\<close>
-      by (simp add: topspace_subtopology closedin_closed_subtopology eq) (auto simp: closedin_def)
+      by (simp add: closedin_closed_subtopology eq) (auto simp: closedin_def)
   qed
 qed
 
@@ -2264,7 +2264,7 @@
 
 lemma separatedin_subtopology:
      "separatedin (subtopology X U) S T \<longleftrightarrow> S \<subseteq> U \<and> T \<subseteq> U \<and> separatedin X S T"
-  apply (simp add: separatedin_def closure_of_subtopology topspace_subtopology)
+  apply (simp add: separatedin_def closure_of_subtopology)
   apply (safe; metis Int_absorb1 inf.assoc inf.orderE insert_disjoint(2) mk_disjoint_insert)
   done
 
@@ -2715,13 +2715,13 @@
    "\<lbrakk>homeomorphic_maps X Y f g;  f ` (topspace X \<inter> S) = topspace Y \<inter> T\<rbrakk>
         \<Longrightarrow> homeomorphic_maps (subtopology X S) (subtopology Y T) f g"
   unfolding homeomorphic_maps_def
-  by (force simp: continuous_map_from_subtopology topspace_subtopology continuous_map_in_subtopology)
+  by (force simp: continuous_map_from_subtopology continuous_map_in_subtopology)
 
 lemma homeomorphic_maps_subtopologies_alt:
      "\<lbrakk>homeomorphic_maps X Y f g; f ` (topspace X \<inter> S) \<subseteq> T; g ` (topspace Y \<inter> T) \<subseteq> S\<rbrakk>
       \<Longrightarrow> homeomorphic_maps (subtopology X S) (subtopology Y T) f g"
   unfolding homeomorphic_maps_def
-  by (force simp: continuous_map_from_subtopology topspace_subtopology continuous_map_in_subtopology)
+  by (force simp: continuous_map_from_subtopology continuous_map_in_subtopology)
 
 lemma homeomorphic_map_subtopologies:
    "\<lbrakk>homeomorphic_map X Y f; f ` (topspace X \<inter> S) = topspace Y \<inter> T\<rbrakk>
@@ -2810,7 +2810,7 @@
 
 lemma connectedin_subtopology:
      "connectedin (subtopology X S) T \<longleftrightarrow> connectedin X T \<and> T \<subseteq> S"
-  by (force simp: connectedin_def subtopology_subtopology topspace_subtopology inf_absorb2)
+  by (force simp: connectedin_def subtopology_subtopology inf_absorb2)
 
 lemma connected_space_eq:
      "connected_space X \<longleftrightarrow>
@@ -3256,7 +3256,7 @@
   have eq: "(\<forall>U \<in> \<U>. \<exists>Y. openin X Y \<and> U = Y \<inter> S) \<longleftrightarrow> \<U> \<subseteq> (\<lambda>Y. Y \<inter> S) ` {y. openin X y}" for \<U>
     by auto
   show ?thesis
-    by (auto simp: compactin_def topspace_subtopology openin_subtopology eq imp_conjL all_subset_image ex_finite_subset_image)
+    by (auto simp: compactin_def openin_subtopology eq imp_conjL all_subset_image ex_finite_subset_image)
 qed
 
 lemma compactin_subspace: "compactin X S \<longleftrightarrow> S \<subseteq> topspace X \<and> compact_space (subtopology X S)"
@@ -3267,7 +3267,7 @@
   by (simp add: compactin_subspace)
 
 lemma compactin_subtopology: "compactin (subtopology X S) T \<longleftrightarrow> compactin X T \<and> T \<subseteq> S"
-apply (simp add: compactin_subspace topspace_subtopology)
+apply (simp add: compactin_subspace)
   by (metis inf.orderE inf_commute subtopology_subtopology)
 
 
@@ -3361,7 +3361,7 @@
 lemma compactin_subtopology_imp_compact:
   assumes "compactin (subtopology X S) K" shows "compactin X K"
   using assms
-proof (clarsimp simp add: compactin_def topspace_subtopology)
+proof (clarsimp simp add: compactin_def)
   fix \<U>
   define \<V> where "\<V> \<equiv> (\<lambda>U. U \<inter> S) ` \<U>"
   assume "K \<subseteq> topspace X" and "K \<subseteq> S" and "\<forall>x\<in>\<U>. openin X x" and "K \<subseteq> \<Union>\<U>"
@@ -3394,7 +3394,7 @@
 lemma compact_imp_compactin_subtopology:
   assumes "compactin X K" "K \<subseteq> S" shows "compactin (subtopology X S) K"
   using assms
-proof (clarsimp simp add: compactin_def topspace_subtopology)
+proof (clarsimp simp add: compactin_def)
   fix \<U> :: "'a set set"
   define \<V> where "\<V> \<equiv> {V. openin X V \<and> (\<exists>U \<in> \<U>. U = V \<inter> S)}"
   assume "K \<subseteq> S" and "K \<subseteq> topspace X" and "\<forall>U\<in>\<U>. openin (subtopology X S) U" and "K \<subseteq> \<Union>\<U>"
@@ -3556,7 +3556,7 @@
 lemma compactin_imp_Bolzano_Weierstrass:
    "\<lbrakk>compactin X S; infinite T \<and> T \<subseteq> S\<rbrakk> \<Longrightarrow> S \<inter> X derived_set_of T \<noteq> {}"
   using compact_space_imp_Bolzano_Weierstrass [of "subtopology X S"]
-  by (simp add: compactin_subspace derived_set_of_subtopology inf_absorb2 topspace_subtopology)
+  by (simp add: compactin_subspace derived_set_of_subtopology inf_absorb2)
 
 lemma compact_closure_of_imp_Bolzano_Weierstrass:
    "\<lbrakk>compactin X (X closure_of S); infinite T; T \<subseteq> S; T \<subseteq> topspace X\<rbrakk> \<Longrightarrow> X derived_set_of T \<noteq> {}"
@@ -3739,7 +3739,7 @@
 lemma section_imp_embedding_map:
    "section_map X Y f \<Longrightarrow> embedding_map X Y f"
   unfolding section_map_def embedding_map_def homeomorphic_map_maps retraction_maps_def homeomorphic_maps_def
-  by (force simp: continuous_map_in_subtopology continuous_map_from_subtopology topspace_subtopology)
+  by (force simp: continuous_map_in_subtopology continuous_map_from_subtopology)
 
 lemma retraction_imp_quotient_map:
   assumes "retraction_map X Y f"
diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Abstract_Topology_2.thy
--- a/src/HOL/Analysis/Abstract_Topology_2.thy	Thu Nov 28 20:38:07 2019 +0100
+++ b/src/HOL/Analysis/Abstract_Topology_2.thy	Thu Nov 28 23:06:22 2019 +0100
@@ -87,7 +87,7 @@
     assume int: "x \<in> interior A"
     then obtain U where U: "open U" "x \<in> U" "U \<subseteq> A" unfolding interior_def by auto
     hence "\<forall>y\<in>U. indicator A y = (1::real)" unfolding indicator_def by auto
-    hence "continuous_on U (indicator A)" by (simp add: continuous_on_const indicator_eq_1_iff)
+    hence "continuous_on U (indicator A)" by (simp add: indicator_eq_1_iff)
     thus ?thesis using U continuous_on_eq_continuous_at by auto
   next
     assume ext: "x \<in> interior (-A)"
@@ -388,7 +388,7 @@
       and "a \<in> s \<Longrightarrow> f a = g a"
     shows "continuous_on s (\<lambda>t. if t \<le> a then f(t) else g(t))"
 using assms
-by (auto simp: continuous_on_id intro: continuous_on_cases_le [where h = id, simplified])
+by (auto intro: continuous_on_cases_le [where h = id, simplified])
 
 
 subsection\<^marker>\<open>tag unimportant\<close>\<open>Inverse function property for open/closed maps\<close>
@@ -1249,7 +1249,7 @@
 
 lemma path_connectedin_absolute [simp]:
      "path_connectedin (subtopology X S) S \<longleftrightarrow> path_connectedin X S"
-  by (simp add: path_connectedin_def subtopology_subtopology topspace_subtopology)
+  by (simp add: path_connectedin_def subtopology_subtopology)
 
 lemma path_connectedin_subset_topspace:
      "path_connectedin X S \<Longrightarrow> S \<subseteq> topspace X"
@@ -1257,14 +1257,14 @@
 
 lemma path_connectedin_subtopology:
      "path_connectedin (subtopology X S) T \<longleftrightarrow> path_connectedin X T \<and> T \<subseteq> S"
-  by (auto simp: path_connectedin_def subtopology_subtopology topspace_subtopology inf.absorb2)
+  by (auto simp: path_connectedin_def subtopology_subtopology inf.absorb2)
 
 lemma path_connectedin:
      "path_connectedin X S \<longleftrightarrow>
         S \<subseteq> topspace X \<and>
         (\<forall>x \<in> S. \<forall>y \<in> S. \<exists>g. pathin X g \<and> g ` {0..1} \<subseteq> S \<and> g 0 = x \<and> g 1 = y)"
   unfolding path_connectedin_def path_connected_space_def pathin_def continuous_map_in_subtopology
-  by (intro conj_cong refl ball_cong) (simp_all add: inf.absorb_iff2 topspace_subtopology)
+  by (intro conj_cong refl ball_cong) (simp_all add: inf.absorb_iff2)
 
 lemma path_connectedin_topspace:
      "path_connectedin X (topspace X) \<longleftrightarrow> path_connected_space X"
diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Bounded_Continuous_Function.thy
--- a/src/HOL/Analysis/Bounded_Continuous_Function.thy	Thu Nov 28 20:38:07 2019 +0100
+++ b/src/HOL/Analysis/Bounded_Continuous_Function.thy	Thu Nov 28 23:06:22 2019 +0100
@@ -33,7 +33,7 @@
   by (blast intro: apply_bcontfun_cases assms )
 
 lemma const_bcontfun: "(\<lambda>x. b) \<in> bcontfun"
-  by (auto simp: bcontfun_def continuous_on_const image_def)
+  by (auto simp: bcontfun_def image_def)
 
 lift_definition const_bcontfun::"'b::metric_space \<Rightarrow> ('a::topological_space \<Rightarrow>\<^sub>C 'b)" is "\<lambda>c _. c"
   by (rule const_bcontfun)
diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Bounded_Linear_Function.thy
--- a/src/HOL/Analysis/Bounded_Linear_Function.thy	Thu Nov 28 20:38:07 2019 +0100
+++ b/src/HOL/Analysis/Bounded_Linear_Function.thy	Thu Nov 28 23:06:22 2019 +0100
@@ -548,7 +548,7 @@
     fix e::real
     let ?d = "real_of_nat DIM('a) * real_of_nat DIM('b)"
     assume "e > 0"
-    hence "e / ?d > 0" by (simp add: DIM_positive)
+    hence "e / ?d > 0" by (simp)
     with l have "eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) i) (l i) < e / ?d) sequentially"
       by simp
     moreover
diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Thu Nov 28 20:38:07 2019 +0100
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Thu Nov 28 23:06:22 2019 +0100
@@ -717,7 +717,7 @@
     then have "a = enum 0"
       using \<open>a \<in> s\<close> na by (subst enum_0_bot) (auto simp: le_less intro!: less[of a _ n])
     then have s_eq: "s - {a} = enum ` Suc ` {.. n}"
-      using s_eq by (simp add: atMost_Suc_eq_insert_0 insert_ident zero_notin_Suc_image in_enum_image subset_eq)
+      using s_eq by (simp add: atMost_Suc_eq_insert_0 insert_ident in_enum_image subset_eq)
     then have "enum 1 \<in> s - {a}"
       by auto
     then have "upd 0 = n"
@@ -1212,7 +1212,7 @@
         have "c = t.enum (Suc l)" unfolding c_eq ..
         also have "t.enum (Suc l) = b.enum (Suc i')"
           using u \<open>l < k\<close> \<open>k \<le> n\<close> \<open>Suc i' < n\<close>
-          by (simp_all add: enum_Suc t.enum_Suc l b.enum_Suc \<open>b.enum i' = enum i'\<close> swap_apply1)
+          by (simp_all add: enum_Suc t.enum_Suc l b.enum_Suc \<open>b.enum i' = enum i'\<close>)
              (simp add: Suc_i')
         also have "\<dots> = b.enum i"
           using i by (simp add: i'_def)
@@ -1576,7 +1576,7 @@
 proof (rule ccontr)
   define n where "n = DIM('a)"
   have n: "1 \<le> n" "0 < n" "n \<noteq> 0"
-    unfolding n_def by (auto simp: Suc_le_eq DIM_positive)
+    unfolding n_def by (auto simp: Suc_le_eq)
   assume "\<not> ?thesis"
   then have *: "\<not> (\<exists>x\<in>cbox 0 One. f x - x = 0)"
     by auto
@@ -1633,7 +1633,7 @@
       \<bar>(f(z) - z)\<bullet>i\<bar> < d / (real n)"
   proof -
     have d': "d / real n / 8 > 0"
-      using d(1) by (simp add: n_def DIM_positive)
+      using d(1) by (simp add: n_def)
     have *: "uniformly_continuous_on (cbox 0 One) f"
       by (rule compact_uniformly_continuous[OF assms(1) compact_cbox])
     obtain e where e:
@@ -1732,7 +1732,7 @@
   { fix x :: "nat \<Rightarrow> nat" and i assume "\<forall>i<n. x i \<le> p" "i < n" "x i = p \<or> x i = 0"
     then have "(\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<in> (cbox 0 One::'a set)"
       using b'_Basis
-      by (auto simp: cbox_def inner_simps bij_betw_def zero_le_divide_iff divide_le_eq_1) }
+      by (auto simp: cbox_def bij_betw_def zero_le_divide_iff divide_le_eq_1) }
   note cube = this
   have q2: "\<forall>x. (\<forall>i<n. x i \<le> p) \<longrightarrow> (\<forall>i<n. x i = 0 \<longrightarrow>
       (label (\<Sum>i\<in>Basis. (real (x (b' i)) / real p) *\<^sub>R i) \<circ> b) i = 0)"
@@ -1855,7 +1855,7 @@
   proof (rule interiorI)
     let ?I = "(\<Inter>i\<in>Basis. {x::'a. 0 < x \<bullet> i} \<inter> {x. x \<bullet> i < 1})"
     show "open ?I"
-      by (intro open_INT finite_Basis ballI open_Int, auto intro: open_Collect_less simp: continuous_on_inner continuous_on_const continuous_on_id)
+      by (intro open_INT finite_Basis ballI open_Int, auto intro: open_Collect_less simp: continuous_on_inner)
     show "\<Sum>Basis /\<^sub>R 2 \<in> ?I"
       by simp
     show "?I \<subseteq> cbox 0 One"
@@ -1963,7 +1963,7 @@
   case False
   then show ?thesis
     unfolding contractible_def nullhomotopic_from_sphere_extension
-    using continuous_on_const less_eq_real_def by auto
+    using less_eq_real_def by auto
 qed
 
 corollary connected_sphere_eq:
@@ -2028,9 +2028,7 @@
   have "continuous_on (closure S \<union> closure(-S)) g"
     unfolding g_def
     apply (rule continuous_on_cases)
-    using fros fid frontier_closures
-        apply (auto simp: contf continuous_on_id)
-    done
+    using fros fid frontier_closures by (auto simp: contf)
   moreover have "closure S \<union> closure(- S) = UNIV"
     using closure_Un by fastforce
   ultimately have contg: "continuous_on UNIV g" by metis
diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu Nov 28 20:38:07 2019 +0100
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu Nov 28 23:06:22 2019 +0100
@@ -127,7 +127,7 @@
 lemma component_le_onorm:
   fixes f :: "real^'m \<Rightarrow> real^'n"
   shows "linear f \<Longrightarrow> \<bar>matrix f $ i $ j\<bar> \<le> onorm f"
-  by (metis linear_matrix_vector_mul_eq matrix_component_le_onorm matrix_vector_mul)
+  by (metis matrix_component_le_onorm matrix_vector_mul(2))
 
 lemma onorm_le_matrix_component_sum:
   fixes A :: "real^'n^'m"
@@ -223,7 +223,7 @@
   unfolding continuous_on_def by (auto intro: tendsto_vec_lambda)
 
 lemma closed_positive_orthant: "closed {x::real^'n. \<forall>i. 0 \<le>x$i}"
-  by (simp add: Collect_all_eq closed_INT closed_Collect_le continuous_on_const continuous_on_id continuous_on_component)
+  by (simp add: Collect_all_eq closed_INT closed_Collect_le continuous_on_component)
 
 lemma bounded_component_cart: "bounded s \<Longrightarrow> bounded ((\<lambda>x. x $ i) ` s)"
   unfolding bounded_def
@@ -243,7 +243,7 @@
 proof -
   have "\<forall>d' \<subseteq> d. ?th d'"
     by (rule compact_lemma_general[where unproj=vec_lambda])
-      (auto intro!: f bounded_component_cart simp: vec_lambda_eta)
+      (auto intro!: f bounded_component_cart)
   then show "?th d" by simp
 qed
 
@@ -372,12 +372,12 @@
 lemma closed_interval_left_cart:
   fixes b :: "real^'n"
   shows "closed {x::real^'n. \<forall>i. x$i \<le> b$i}"
-  by (simp add: Collect_all_eq closed_INT closed_Collect_le continuous_on_const continuous_on_id continuous_on_component)
+  by (simp add: Collect_all_eq closed_INT closed_Collect_le continuous_on_component)
 
 lemma closed_interval_right_cart:
   fixes a::"real^'n"
   shows "closed {x::real^'n. \<forall>i. a$i \<le> x$i}"
-  by (simp add: Collect_all_eq closed_INT closed_Collect_le continuous_on_const continuous_on_id continuous_on_component)
+  by (simp add: Collect_all_eq closed_INT closed_Collect_le continuous_on_component)
 
 lemma is_interval_cart:
   "is_interval (s::(real^'n) set) \<longleftrightarrow>
@@ -430,7 +430,7 @@
 proof -
   { fix i::'n
     have "closed {x::'a ^ 'n. P i \<longrightarrow> x$i = 0}"
-      by (cases "P i") (simp_all add: closed_Collect_eq continuous_on_const continuous_on_id continuous_on_component) }
+      by (cases "P i") (simp_all add: closed_Collect_eq continuous_on_component) }
   thus ?thesis
     unfolding Collect_all_eq by (simp add: closed_INT)
 qed
diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Thu Nov 28 20:38:07 2019 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Thu Nov 28 23:06:22 2019 +0100
@@ -406,10 +406,10 @@
   by (simp add: C1_differentiable_on_eq differentiable_at_imp_differentiable_on)
 
 lemma C1_differentiable_on_ident [simp, derivative_intros]: "(\<lambda>x. x) C1_differentiable_on S"
-  by (auto simp: C1_differentiable_on_eq continuous_on_const)
+  by (auto simp: C1_differentiable_on_eq)
 
 lemma C1_differentiable_on_const [simp, derivative_intros]: "(\<lambda>z. a) C1_differentiable_on S"
-  by (auto simp: C1_differentiable_on_eq continuous_on_const)
+  by (auto simp: C1_differentiable_on_eq)
 
 lemma C1_differentiable_on_add [simp, derivative_intros]:
   "f C1_differentiable_on S \<Longrightarrow> g C1_differentiable_on S \<Longrightarrow> (\<lambda>x. f x + g x) C1_differentiable_on S"
@@ -498,7 +498,7 @@
 proof (cases "m = 0")
   case True
   then show ?thesis
-    unfolding o_def by (auto simp: piecewise_C1_differentiable_on_def continuous_on_const)
+    unfolding o_def by (auto simp: piecewise_C1_differentiable_on_def)
 next
   case False
   have *: "\<And>x. finite (S \<inter> {y. m * y + c = x})"
@@ -919,7 +919,7 @@
     unfolding reversepath_def
     apply (rule C1_differentiable_compose [of "\<lambda>x::real. 1-x" _ g, unfolded o_def])
     using S
-    by (force simp: finite_vimageI inj_on_def C1_differentiable_on_eq continuous_on_const elim!: continuous_on_subset)+
+    by (force simp: finite_vimageI inj_on_def C1_differentiable_on_eq elim!: continuous_on_subset)+
   ultimately show ?thesis using assms
     by (auto simp: valid_path_def piecewise_C1_differentiable_on_def path_def [symmetric])
 qed
@@ -1342,7 +1342,7 @@
 lemma has_contour_integral_linepath:
   shows "(f has_contour_integral i) (linepath a b) \<longleftrightarrow>
          ((\<lambda>x. f(linepath a b x) * (b - a)) has_integral i) {0..1}"
-  by (simp add: has_contour_integral vector_derivative_linepath_at)
+  by (simp add: has_contour_integral)
 
 lemma linepath_in_path:
   shows "x \<in> {0..1} \<Longrightarrow> linepath a b x \<in> closed_segment a b"
@@ -1432,7 +1432,7 @@
   using has_contour_integral_subpath_refl contour_integrable_on_def by blast
 
 lemma contour_integral_subpath_refl [simp]: "contour_integral (subpath u u g) f = 0"
-  by (simp add: has_contour_integral_subpath_refl contour_integral_unique)
+  by (simp add: contour_integral_unique)
 
 lemma has_contour_integral_subpath:
   assumes f: "f contour_integrable_on g" and g: "valid_path g"
@@ -1544,14 +1544,14 @@
       apply simp
       apply (elim disjE)
       apply (auto simp: * contour_integral_reversepath contour_integrable_subpath
-                   valid_path_reversepath valid_path_subpath algebra_simps)
+               valid_path_subpath algebra_simps)
       done
 next
   case False
   then show ?thesis
-    apply (auto simp: contour_integral_subpath_refl)
+    apply (auto)
     using assms
-    by (metis eq_neg_iff_add_eq_0 contour_integrable_subpath contour_integral_reversepath reversepath_subpath valid_path_subpath)
+    by (metis eq_neg_iff_add_eq_0 contour_integral_reversepath reversepath_subpath valid_path_subpath)
 qed
 
 lemma contour_integral_integral:
@@ -1699,10 +1699,10 @@
   done
 
 lemma contour_integrable_on_const [iff]: "(\<lambda>x. c) contour_integrable_on (linepath a b)"
-  by (simp add: continuous_on_const contour_integrable_continuous_linepath)
+  by (simp add: contour_integrable_continuous_linepath)
 
 lemma contour_integrable_on_id [iff]: "(\<lambda>x. x) contour_integrable_on (linepath a b)"
-  by (simp add: continuous_on_id contour_integrable_continuous_linepath)
+  by (simp add: contour_integrable_continuous_linepath)
 
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Arithmetical combining theorems\<close>
 
@@ -4546,7 +4546,7 @@
     moreover have "\<bar>Re (winding_number \<gamma> z')\<bar> < 1/2"
       apply (rule winding_number_lt_half [OF \<gamma> *])
       using azb \<open>d>0\<close> pag
-      apply (auto simp: add_strict_increasing anz field_split_simps algebra_simps dest!: subsetD)
+      apply (auto simp: add_strict_increasing anz field_split_simps dest!: subsetD)
       done
     ultimately have False
       by simp
@@ -5719,7 +5719,7 @@
           using \<open>x \<in> path_image \<gamma>\<close> ball_divide_subset_numeral d by fastforce
         then show ?thesis
         using \<open>d > 0\<close> apply (simp add: ff_def norm_mult norm_divide norm_power dist_norm canc)
-        using dpow_le apply (simp add: algebra_simps field_split_simps mult_less_0_iff)
+        using dpow_le apply (simp add: field_split_simps)
         done
       qed
       have ub: "u \<in> ball w (d/2)"
@@ -6187,7 +6187,7 @@
     apply (rule deriv_cmult)
     apply (rule analytic_on_imp_differentiable_at [OF _ Suc.prems])
     apply (rule analytic_on_compose_gen [where g="(deriv ^^ n) f" and T=T, unfolded o_def])
-      apply (simp add: analytic_on_linear)
+      apply (simp)
      apply (simp add: analytic_on_open f holomorphic_higher_deriv T)
     apply (blast intro: fg)
     done
@@ -6195,7 +6195,7 @@
       apply (subst complex_derivative_chain [where g = "(deriv ^^ n) f" and f = "(*) u", unfolded o_def])
       apply (rule derivative_intros)
       using Suc.prems field_differentiable_def f fg has_field_derivative_higher_deriv T apply blast
-      apply (simp add: deriv_linear)
+      apply (simp)
       done
   finally show ?case
     by simp
@@ -6540,7 +6540,7 @@
   assumes "f holomorphic_on UNIV" and "(f \<longlongrightarrow> l) at_infinity"
     shows "f z = l"
   using Liouville_weak_0 [of "\<lambda>z. f z - l"]
-  by (simp add: assms holomorphic_on_const holomorphic_on_diff LIM_zero)
+  by (simp add: assms holomorphic_on_diff LIM_zero)
 
 proposition Liouville_weak_inverse:
   assumes "f holomorphic_on UNIV" and unbounded: "\<And>B. eventually (\<lambda>x. norm (f x) \<ge> B) at_infinity"
@@ -6548,11 +6548,11 @@
 proof -
   { assume f: "\<And>z. f z \<noteq> 0"
     have 1: "(\<lambda>x. 1 / f x) holomorphic_on UNIV"
-      by (simp add: holomorphic_on_divide holomorphic_on_const assms f)
+      by (simp add: holomorphic_on_divide assms f)
     have 2: "((\<lambda>x. 1 / f x) \<longlongrightarrow> 0) at_infinity"
       apply (rule tendstoI [OF eventually_mono])
       apply (rule_tac B="2/e" in unbounded)
-      apply (simp add: dist_norm norm_divide field_split_simps mult_ac)
+      apply (simp add: dist_norm norm_divide field_split_simps)
       done
     have False
       using Liouville_weak_0 [OF 1 2] f by simp
@@ -7473,7 +7473,7 @@
         apply (rule mult_mono)
         using that D interior_subset apply blast
         using \<open>L>0\<close> \<open>e>0\<close> \<open>D>0\<close> DL2
-        apply (auto simp: norm_divide field_split_simps algebra_simps)
+        apply (auto simp: norm_divide field_split_simps)
         done
       finally show ?thesis .
     qed
diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Change_Of_Vars.thy
--- a/src/HOL/Analysis/Change_Of_Vars.thy	Thu Nov 28 20:38:07 2019 +0100
+++ b/src/HOL/Analysis/Change_Of_Vars.thy	Thu Nov 28 23:06:22 2019 +0100
@@ -1433,7 +1433,7 @@
             with \<open>r > 0\<close> \<open>d > 0\<close> \<open>e > 0\<close> show ?thesis
               apply (simp add: content_cbox_if_cart mem_box_cart)
               apply (auto simp: prod_nonneg)
-              apply (simp add: abs if_distrib prod.delta_remove prod_constant field_simps power_diff split: if_split_asm)
+              apply (simp add: abs if_distrib prod.delta_remove field_simps power_diff split: if_split_asm)
               done
           qed
           also have "\<dots> \<le> e/2 * measure lebesgue (cball ?x' (min d r))"
diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Connected.thy
--- a/src/HOL/Analysis/Connected.thy	Thu Nov 28 20:38:07 2019 +0100
+++ b/src/HOL/Analysis/Connected.thy	Thu Nov 28 23:06:22 2019 +0100
@@ -726,7 +726,7 @@
       apply (subst tus [symmetric])
       apply (rule continuous_on_cases_local)
       using clt clu tue
-      apply (auto simp: tus continuous_on_const)
+      apply (auto simp: tus)
       done
     have fi: "finite ((\<lambda>x. if x \<in> t then 0 else 1) ` S)"
       by (rule finite_subset [of _ "{0,1}"]) auto
diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Continuous_Extension.thy
--- a/src/HOL/Analysis/Continuous_Extension.thy	Thu Nov 28 20:38:07 2019 +0100
+++ b/src/HOL/Analysis/Continuous_Extension.thy	Thu Nov 28 23:06:22 2019 +0100
@@ -91,7 +91,7 @@
           done
       qed
       moreover have "\<lbrakk>U \<in> \<C>; x \<in> S\<rbrakk> \<Longrightarrow> 0 \<le> F U x" for U x
-        using nonneg [of x] by (simp add: F_def field_split_simps setdist_pos_le)
+        using nonneg [of x] by (simp add: F_def field_split_simps)
       ultimately show "\<And>U. U \<in> \<C> \<Longrightarrow> continuous_on S (F U) \<and> (\<forall>x\<in>S. 0 \<le> F U x)"
         by metis
     next
@@ -194,7 +194,7 @@
     show ?thesis
     proof (cases "T = U")
       case True with \<open>S = {}\<close> \<open>a \<noteq> b\<close> show ?thesis
-        by (rule_tac f = "\<lambda>x. b" in that) (auto simp: continuous_on_const)
+        by (rule_tac f = "\<lambda>x. b" in that) (auto)
     next
       case False
       with UT closedin_subset obtain c where c: "c \<in> U" "c \<notin> T"
@@ -220,7 +220,7 @@
     case True show ?thesis
     proof (cases "S = U")
       case True with \<open>T = {}\<close> \<open>a \<noteq> b\<close> show ?thesis
-        by (rule_tac f = "\<lambda>x. a" in that) (auto simp: continuous_on_const)
+        by (rule_tac f = "\<lambda>x. a" in that) (auto)
     next
       case False
       with US closedin_subset obtain c where c: "c \<in> U" "c \<notin> S"
@@ -260,7 +260,7 @@
           "\<And>x. x \<in> T \<Longrightarrow> f x = b"
 proof (cases "a = b")
   case True then show ?thesis
-    by (rule_tac f = "\<lambda>x. b" in that) (auto simp: continuous_on_const)
+    by (rule_tac f = "\<lambda>x. b" in that) (auto)
 next
   case False
   then show ?thesis
diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Thu Nov 28 20:38:07 2019 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Thu Nov 28 23:06:22 2019 +0100
@@ -2233,7 +2233,7 @@
       unfolding 2
       by (clarsimp simp: dist_norm) (metis inner_commute inner_diff_right norm_bound_Basis_le)
     have e': "e = (\<Sum>(i::'a)\<in>Basis. d)"
-      by (simp add: d_def DIM_positive)
+      by (simp add: d_def)
     show "convex hull c \<subseteq> cball x e"
       unfolding 2
       apply clarsimp
diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Extended_Real_Limits.thy
--- a/src/HOL/Analysis/Extended_Real_Limits.thy	Thu Nov 28 20:38:07 2019 +0100
+++ b/src/HOL/Analysis/Extended_Real_Limits.thy	Thu Nov 28 23:06:22 2019 +0100
@@ -939,7 +939,7 @@
     apply (rule iffD1[OF continuous_on_cong, of "{..0}" _ "\<lambda>x. -x"])
     using less_eq_ereal_def apply (auto simp add: continuous_uminus_ereal)
     apply (rule iffD1[OF continuous_on_cong, of "{0..}" _ "\<lambda>x. x"])
-      apply (auto simp add: continuous_on_id)
+      apply (auto)
     done
   moreover have "(UNIV::ereal set) = {..0} \<union> {(0::ereal)..}" by auto
   ultimately show ?thesis by auto
diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Function_Topology.thy
--- a/src/HOL/Analysis/Function_Topology.thy	Thu Nov 28 20:38:07 2019 +0100
+++ b/src/HOL/Analysis/Function_Topology.thy	Thu Nov 28 23:06:22 2019 +0100
@@ -285,7 +285,7 @@
   unfolding topology_eq
   apply clarify
   apply (simp add: openin_product_topology flip: openin_relative_to)
-  apply (simp add: arbitrary_union_of_relative_to topspace_product_topology topspace_subtopology flip: PiE_Int)
+  apply (simp add: arbitrary_union_of_relative_to flip: PiE_Int)
   done
 qed
 
@@ -1960,8 +1960,7 @@
 lemma connectedin_PiE:
    "connectedin (product_topology X I) (PiE I S) \<longleftrightarrow>
         PiE I S = {} \<or> (\<forall>i \<in> I. connectedin (X i) (S i))"
-  by (fastforce simp add: connectedin_def subtopology_PiE connected_space_product_topology subset_PiE PiE_eq_empty_iff
-      topspace_subtopology_subset)
+  by (fastforce simp add: connectedin_def subtopology_PiE connected_space_product_topology subset_PiE PiE_eq_empty_iff)
 
 lemma path_connected_space_product_topology:
    "path_connected_space(product_topology X I) \<longleftrightarrow>
diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Further_Topology.thy
--- a/src/HOL/Analysis/Further_Topology.thy	Thu Nov 28 20:38:07 2019 +0100
+++ b/src/HOL/Analysis/Further_Topology.thy	Thu Nov 28 23:06:22 2019 +0100
@@ -1536,7 +1536,7 @@
     then obtain y where "y \<in> rel_frontier U"
       by auto
     with \<open>S = {}\<close> show ?thesis
-      by (rule_tac K="{}" and g="\<lambda>x. y" in that)  (auto simp: continuous_on_const)
+      by (rule_tac K="{}" and g="\<lambda>x. y" in that)  (auto)
   qed
 next
   case False
@@ -1662,7 +1662,7 @@
 proof (cases "r = 0")
   case True
   with fim show ?thesis
-    by (rule_tac K="{}" and g = "\<lambda>x. a" in that) (auto simp: continuous_on_const)
+    by (rule_tac K="{}" and g = "\<lambda>x. a" in that) (auto)
 next
   case False
   with assms have "0 < r" by auto
@@ -2836,7 +2836,7 @@
 proof -
   have "homotopic_loops S (f \<circ> exp \<circ> (\<lambda>t. of_real(2 * pi * t) * \<i>)) (g \<circ> exp \<circ> (\<lambda>t. of_real(2 * pi *  t) * \<i>))"
     apply (rule S [unfolded simply_connected_homotopic_loops, rule_format])
-    apply (simp add: homotopic_circlemaps_imp_homotopic_loops homotopic_with_refl contf fim contg gim)
+    apply (simp add: homotopic_circlemaps_imp_homotopic_loops contf fim contg gim)
     done
   then show ?thesis
     apply (rule homotopic_with_eq [OF homotopic_loops_imp_homotopic_circlemaps])
@@ -2854,8 +2854,7 @@
             shows "\<exists>a. homotopic_with_canon (\<lambda>h. True) (sphere 0 1) S h (\<lambda>x. a)"
     apply (rule_tac x="h 1" in exI)
     apply (rule hom)
-    using assms
-    by (auto simp: continuous_on_const)
+    using assms by (auto)
 
 lemma simply_connected_eq_homotopic_circlemaps2b:
   fixes S :: "'a::real_normed_vector set"
@@ -2869,7 +2868,7 @@
   assume "a \<in> S" "b \<in> S"
   then show "homotopic_loops S (linepath a a) (linepath b b)"
     using homotopic_circlemaps_imp_homotopic_loops [OF assms [of "\<lambda>x. a" "\<lambda>x. b"]]
-    by (auto simp: o_def continuous_on_const linepath_def)
+    by (auto simp: o_def linepath_def)
 qed
 
 lemma simply_connected_eq_homotopic_circlemaps3:
@@ -3876,7 +3875,7 @@
       apply (rule continuous_intros)
       using homotopic_with_imp_continuous [OF L] apply blast
       apply (rule continuous_on_subset [of "sphere 0 1", OF continuous_on_inverse])
-        apply (auto simp: continuous_on_id)
+        apply (auto)
       done
     have "homotopic_with_canon (\<lambda>x. True) S (sphere 0 1) (\<lambda>x. f x / g x) (\<lambda>x. 1)"
       using homotopic_with_sphere_times [OF L cont]
@@ -4473,7 +4472,7 @@
   apply (auto simp: retract_of_def retraction_def)
   apply (erule (1) Borsukian_retraction_gen)
   apply (meson retraction retraction_def)
-    apply (auto simp: continuous_on_id)
+    apply (auto)
     done
 
 lemma homeomorphic_Borsukian: "\<lbrakk>Borsukian S; S homeomorphic T\<rbrakk> \<Longrightarrow> Borsukian T"
@@ -5595,8 +5594,7 @@
   show ?rhs
   proof (cases "S = {}")
     case True
-    with a show ?thesis
-      using continuous_on_const by force
+    with a show ?thesis by force
   next
     case False
     have anr: "ANR (-{0::complex})"
diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Nov 28 20:38:07 2019 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Nov 28 23:06:22 2019 +0100
@@ -7263,7 +7263,7 @@
             \<le> e * content (cbox w z) / content ?CBOX/2 * content (cbox u v)"
         apply (rule integrable_bound [OF _ _ normint_wz])
         using cbp \<open>0 < e/content ?CBOX\<close>
-        apply (auto simp: field_split_simps content_pos_le integrable_diff int_integrable integrable_const)
+        apply (auto simp: field_split_simps integrable_diff int_integrable integrable_const)
         done
       also have "... \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX/2"
         by (simp add: content_Pair field_split_simps)
@@ -7430,7 +7430,7 @@
                inverse (real (Suc k)) powr (a + 1) / (a + 1)) {inverse (real (Suc k))..c}"
         using True a by (intro fundamental_theorem_of_calculus)
            (auto intro!: derivative_eq_intros continuous_on_powr' continuous_on_const
-             continuous_on_id simp: has_field_derivative_iff_has_vector_derivative [symmetric])
+              simp: has_field_derivative_iff_has_vector_derivative [symmetric])
       with True show ?thesis unfolding f_def F_def by (subst has_integral_restrict) simp_all
     next
       case False
diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Homeomorphism.thy
--- a/src/HOL/Analysis/Homeomorphism.thy	Thu Nov 28 20:38:07 2019 +0100
+++ b/src/HOL/Analysis/Homeomorphism.thy	Thu Nov 28 23:06:22 2019 +0100
@@ -177,7 +177,7 @@
       by (simp add: proj_def) (metis surf xy homeomorphism_def)
   qed
   have co01: "compact ?SPHER"
-    by (simp add: closed_affine_hull compact_Int_closed)
+    by (simp add: compact_Int_closed)
   show "?SMINUS homeomorphic ?SPHER"
     apply (subst homeomorphic_sym)
     apply (rule homeomorphic_compact [OF co01 cont_nosp [unfolded o_def] no_sp_im inj_spher])
@@ -293,7 +293,7 @@
     qed
   qed
   have co01: "compact ?CBALL"
-    by (simp add: closed_affine_hull compact_Int_closed)
+    by (simp add: compact_Int_closed)
   show "S homeomorphic ?CBALL"
     apply (subst homeomorphic_sym)
     apply (rule homeomorphic_compact [OF co01 cont_nosp2 [unfolded o_def] im_cball inj_cball])
@@ -1446,9 +1446,9 @@
       obtain t where "t \<in> tk" and t: "{real n / real N .. (1 + real n) / real N} \<subseteq> K t"
       proof (rule bexE [OF \<delta>])
         show "{real n / real N .. (1 + real n) / real N} \<subseteq> {0..1}"
-          using Suc.prems by (auto simp: field_split_simps algebra_simps)
+          using Suc.prems by (auto simp: field_split_simps)
         show diameter_less: "diameter {real n / real N .. (1 + real n) / real N} < \<delta>"
-          using \<open>0 < \<delta>\<close> N by (auto simp: field_split_simps algebra_simps)
+          using \<open>0 < \<delta>\<close> N by (auto simp: field_split_simps)
       qed blast
       have t01: "t \<in> {0..1}"
         using \<open>t \<in> tk\<close> \<open>tk \<subseteq> {0..1}\<close> by blast
@@ -1458,7 +1458,7 @@
                  and homuu: "\<And>U. U \<in> \<V> \<Longrightarrow> \<exists>q. homeomorphism U (UU (X t)) p q"
         using inUS [OF t01] UU by meson
       have n_div_N_in: "real n / real N \<in> {real n / real N .. (1 + real n) / real N}"
-        using N by (auto simp: field_split_simps algebra_simps)
+        using N by (auto simp: field_split_simps)
       with t have nN_in_kkt: "real n / real N \<in> K t"
         by blast
       have "k (real n / real N, y) \<in> C \<inter> p -` UU (X t)"
@@ -1850,7 +1850,7 @@
              and hpk: "\<And>z. z \<in> {0..1} \<times> {0..1} \<Longrightarrow> h z = p (k z)"
     apply (rule covering_space_lift_homotopy_alt [OF cov conth him, of "\<lambda>x. h2 0"])
     using h1h2 ph1 ph2 apply (force simp: heq0 pathstart_def pathfinish_def)
-    using path_image_def pih2 continuous_on_const by fastforce+
+    using path_image_def pih2 by fastforce+
   have contg1: "continuous_on {0..1} g1" and contg2: "continuous_on {0..1} g2"
     using \<open>path g1\<close> \<open>path g2\<close> path_def by blast+
   have g1im: "g1 ` {0..1} \<subseteq> S" and g2im: "g2 ` {0..1} \<subseteq> S"
@@ -1892,7 +1892,7 @@
         by (intro continuous_intros continuous_on_compose2 [OF contk]) auto
       show "\<And>x. x \<in> {0..1} \<Longrightarrow> g1 1 = p ((k \<circ> Pair x) 1)"
         using heq1 hpk by auto
-    qed (use contk kim g1im h1im that in \<open>auto simp: ph1 continuous_on_const\<close>)
+    qed (use contk kim g1im h1im that in \<open>auto simp: ph1\<close>)
   qed (use contk kim in auto)
 qed
 
@@ -1993,7 +1993,7 @@
       have "q' t = (h \<circ> (*\<^sub>R) 2) t" if "0 \<le> t" "t \<le> 1/2" for t
       proof (rule covering_space_lift_unique [OF cov, of q' 0 "h \<circ> (*\<^sub>R) 2" "{0..1/2}" "f \<circ> g \<circ> (*\<^sub>R) 2" t])
         show "q' 0 = (h \<circ> (*\<^sub>R) 2) 0"
-          by (metis \<open>pathstart q' = pathstart q\<close> comp_def g h pastq pathstart_def pth_4(2))
+          by (metis \<open>pathstart q' = pathstart q\<close> comp_def h pastq pathstart_def pth_4(2))
         show "continuous_on {0..1/2} (f \<circ> g \<circ> (*\<^sub>R) 2)"
           apply (intro continuous_intros continuous_on_compose continuous_on_path [OF \<open>path g\<close>] continuous_on_subset [OF contf])
           using g(2) path_image_def by fastforce+
diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Homotopy.thy
--- a/src/HOL/Analysis/Homotopy.thy	Thu Nov 28 20:38:07 2019 +0100
+++ b/src/HOL/Analysis/Homotopy.thy	Thu Nov 28 23:06:22 2019 +0100
@@ -217,7 +217,7 @@
                (k2 \<circ> (\<lambda>x. (2 *\<^sub>R fst x -1, snd x)))"
         apply (rule fst continuous_map_compose [OF _ contk2] continuous_intros continuous_map_into_subtopology | simp)+
           apply (rule continuous_intros fst continuous_map_from_subtopology | simp)+
-         apply (force simp: topspace_subtopology prod_topology_subtopology)
+         apply (force simp: prod_topology_subtopology)
         using continuous_map_snd  continuous_map_from_subtopology by blast
       show "(k1 \<circ> (\<lambda>x. (2 *\<^sub>R fst x, snd x))) y = (k2 \<circ> (\<lambda>x. (2 *\<^sub>R fst x -1, snd x))) y"
         if "y \<in> topspace ?X01" and "fst y = 1/2" for y
@@ -481,7 +481,7 @@
     have pab: "path_component T a b" if "a \<in> T" "b \<in> T" for a b
     proof -
       have "homotopic_with_canon (\<lambda>x. True) S T (\<lambda>x. a) (\<lambda>x. b)"
-        by (simp add: LHS continuous_on_const image_subset_iff that)
+        by (simp add: LHS image_subset_iff that)
       then show ?thesis
         using False homotopic_constant_maps [of "top_of_set S" "top_of_set T" a b] by auto
     qed
@@ -572,7 +572,7 @@
      "\<lbrakk>path p; path_image p \<subseteq> s; \<And>t. t \<in> {0..1} \<Longrightarrow> p t = q t\<rbrakk> \<Longrightarrow> homotopic_paths s p q"
   apply (simp add: homotopic_paths_def)
   apply (rule homotopic_with_eq)
-  apply (auto simp: path_def homotopic_with_refl pathstart_def pathfinish_def path_image_def elim: continuous_on_eq)
+  apply (auto simp: path_def pathstart_def pathfinish_def path_image_def elim: continuous_on_eq)
   done
 
 proposition homotopic_paths_reparametrize:
@@ -1414,7 +1414,7 @@
     obtains c where "homotopic_with_canon (\<lambda>h. True) S T f (\<lambda>x. c)"
 apply (rule nullhomotopic_through_contractible [OF f, of id T])
 using assms
-apply (auto simp: continuous_on_id)
+apply (auto)
 done
 
 lemma nullhomotopic_from_contractible:
@@ -3583,7 +3583,7 @@
         by (rule homotopic_with_trans [OF f])
     next
       show "retraction_maps X (subtopology X S) r id"
-        by (simp add: r req retraction_maps_def topspace_subtopology)
+        by (simp add: r req retraction_maps_def)
     qed
   qed (use True in \<open>auto simp: retraction_maps_def topspace_subtopology_subset continuous_map_in_subtopology\<close>)
   ultimately show ?thesis by simp
@@ -3824,8 +3824,6 @@
 qed
 
 
-
-
 lemma contractible_space_product_topology:
   "contractible_space(product_topology X I) \<longleftrightarrow>
     topspace (product_topology X I) = {} \<or> (\<forall>i \<in> I. contractible_space(X i))"
@@ -3846,7 +3844,7 @@
       using cs unfolding contractible_space_def by metis
     have "homotopic_with (\<lambda>x. True)
                          (product_topology X I) (product_topology X I) id (\<lambda>x. restrict f I)"
-      by (rule homotopic_with_eq [OF homotopic_with_product_topology [OF f]]) (auto simp: topspace_product_topology)
+      by (rule homotopic_with_eq [OF homotopic_with_product_topology [OF f]]) (auto)
     then show ?thesis
       by (auto simp: contractible_space_def)
   qed
@@ -4101,7 +4099,7 @@
     apply (rule_tac x="\<lambda>x. b" in exI)
     apply (rule_tac x="\<lambda>x. a" in exI)
     apply (intro assms conjI continuous_on_id' homotopic_into_contractible)
-    apply (auto simp: o_def continuous_on_const)
+    apply (auto simp: o_def)
     done
 qed
 
@@ -4578,7 +4576,7 @@
 proof (cases "S = {}")
   case True
   then show ?thesis
-    by (simp add: path_connected_empty)
+    by (simp)
 next
   case False
   show ?thesis
@@ -4714,7 +4712,7 @@
           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)
+          by (simp add: f_def \<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"
           by blast
       qed
@@ -4782,7 +4780,7 @@
         apply (simp add: ff_def)
         apply (rule continuous_on_cases)
         using homeomorphism_cont1 [OF hom]
-            apply (auto simp: affine_closed \<open>affine T\<close> continuous_on_id fid)
+            apply (auto simp: affine_closed \<open>affine T\<close> fid)
         done
       then show "continuous_on S ff"
         apply (rule continuous_on_subset)
@@ -4791,7 +4789,7 @@
         apply (simp add: gg_def)
         apply (rule continuous_on_cases)
         using homeomorphism_cont2 [OF hom]
-            apply (auto simp: affine_closed \<open>affine T\<close> continuous_on_id gid)
+            apply (auto simp: affine_closed \<open>affine T\<close> gid)
         done
       then show "continuous_on S gg"
         apply (rule continuous_on_subset)
@@ -5039,7 +5037,7 @@
       using assms by auto
     have "f ` {a..b} = {c..d}"
       unfolding f_def image_affinity_atLeastAtMost
-      using assms sum_sqs_eq by (auto simp: field_split_simps algebra_simps)
+      using assms sum_sqs_eq by (auto simp: field_split_simps)
     then show "f ` cbox a b = cbox c d"
       by auto
     show "inj_on f (cbox a b)"
@@ -5051,7 +5049,7 @@
     show "f a = c"
       by (simp add: f_def)
     show "f b = d"
-      using assms sum_sqs_eq [of a b] by (auto simp: f_def field_split_simps algebra_simps)
+      using assms sum_sqs_eq [of a b] by (auto simp: f_def field_split_simps)
   qed
 qed
 
@@ -5078,7 +5076,7 @@
     show "continuous_on (cbox a c) f"
       apply (simp add: f_def)
       apply (rule continuous_on_cases_le [OF continuous_on_subset [OF cf1] continuous_on_subset [OF cf2]])
-      using le eq apply (force simp: continuous_on_id)+
+      using le eq apply (force)+
       done
     have "f ` cbox a b = f1 ` cbox a b" "f ` cbox b c = f2 ` cbox b c"
       unfolding f_def using eq by force+
@@ -5390,7 +5388,7 @@
       using \<open>U \<noteq> {}\<close> \<open>K \<subseteq> S\<close> openin_imp_subset [OF opeU] by blast
     show ?thesis
       apply (rule that [of id id])
-      using \<open>K \<subseteq> U\<close> by (auto simp: continuous_on_id intro: homeomorphismI)
+      using \<open>K \<subseteq> U\<close> by (auto intro: homeomorphismI)
   next
     assume "aff_dim S = 1"
     then have "affine hull S homeomorphic (UNIV :: real set)"
diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Lebesgue_Measure.thy
--- a/src/HOL/Analysis/Lebesgue_Measure.thy	Thu Nov 28 20:38:07 2019 +0100
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Thu Nov 28 23:06:22 2019 +0100
@@ -363,7 +363,7 @@
   qed
   show "((\<lambda>a. ennreal (F b - F a)) \<longlongrightarrow> F b - F a) (at_left a)"
     by (rule continuous_on_tendsto_compose[where g="\<lambda>x. x" and s=UNIV])
-       (auto simp: continuous_on_ennreal continuous_on_diff cont_F continuous_on_const)
+       (auto simp: continuous_on_ennreal continuous_on_diff cont_F)
 qed (rule trivial_limit_at_left_real)
 
 lemma\<^marker>\<open>tag important\<close> sigma_finite_interval_measure:
@@ -745,7 +745,7 @@
   have "((\<lambda>f. f 1) -` {l..u} \<inter> space (Pi\<^sub>M {1} (\<lambda>b. interval_measure (\<lambda>x. x)))) = {1::real} \<rightarrow>\<^sub>E {l..u}"
     by (auto simp: space_PiM)
   then show ?thesis
-    by (simp add: lborel_def emeasure_distr emeasure_PiM emeasure_interval_measure_Icc continuous_on_id)
+    by (simp add: lborel_def emeasure_distr emeasure_PiM emeasure_interval_measure_Icc)
 qed
 
 lemma emeasure_lborel_Icc_eq: "emeasure lborel {l .. u} = ennreal (if l \<le> u then u - l else 0)"
@@ -821,7 +821,7 @@
 
 lemma emeasure_lborel_singleton[simp]: "emeasure lborel {x} = 0"
   using emeasure_lborel_cbox[of x x] nonempty_Basis
-  by (auto simp del: emeasure_lborel_cbox nonempty_Basis simp add: prod_constant)
+  by (auto simp del: emeasure_lborel_cbox nonempty_Basis)
 
 lemma fmeasurable_cbox [iff]: "cbox a b \<in> fmeasurable lborel"
   and fmeasurable_box [iff]: "box a b \<in> fmeasurable lborel"
@@ -872,14 +872,14 @@
     have "... \<le> (2::real) ^ card ?Ba * real (Suc n) ^ card ?Ba"
       apply (rule mult_left_mono)
       apply (metis DIM_positive One_nat_def less_eq_Suc_le less_imp_le of_nat_le_iff of_nat_power self_le_power zero_less_Suc)
-      apply (simp add: DIM_positive)
+      apply (simp)
       done
     finally have "real n \<le> (2::real) ^ card ?Ba * real (Suc n) ^ card ?Ba" .
   } note [intro!] = this
   show ?thesis
     unfolding UN_box_eq_UNIV[symmetric]
     apply (subst SUP_emeasure_incseq[symmetric])
-    apply (auto simp: incseq_def subset_box inner_add_left prod_constant
+    apply (auto simp: incseq_def subset_box inner_add_left
       simp del: Sup_eq_top_iff SUP_eq_top_iff
       intro!: ennreal_SUP_eq_top)
     done
@@ -1001,7 +1001,7 @@
     using c by (auto simp: box_def T_def field_simps inner_simps divide_less_eq)
   with le c show "emeasure ?D (box l u) = (\<Prod>b\<in>?B. (u - l) \<bullet> b)"
     by (auto simp: emeasure_density emeasure_distr nn_integral_multc emeasure_lborel_box_eq inner_simps
-                   field_simps field_split_simps ennreal_mult'[symmetric] prod_nonneg prod.distrib[symmetric]
+                   field_split_simps ennreal_mult'[symmetric] prod_nonneg prod.distrib[symmetric]
              intro!: prod.cong)
 qed simp
 
@@ -1153,7 +1153,7 @@
         apply (subst lebesgue_affine_euclidean[of "\<lambda>_. m" \<delta>])
         apply (simp_all add: emeasure_density trans_eq_T nn_integral_cmult emeasure_distr
                         del: space_completion emeasure_completion)
-        apply (simp add: vimage_comp s_comp_s prod_constant)
+        apply (simp add: vimage_comp s_comp_s)
         done
     next
       assume "S \<notin> sets lebesgue"
diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Locally.thy
--- a/src/HOL/Analysis/Locally.thy	Thu Nov 28 20:38:07 2019 +0100
+++ b/src/HOL/Analysis/Locally.thy	Thu Nov 28 23:06:22 2019 +0100
@@ -155,7 +155,7 @@
 lemma locally_path_connected_space_open_path_components:
    "locally_path_connected_space X \<longleftrightarrow>
         (\<forall>U c. openin X U \<and> c \<in> path_components_of(subtopology X U) \<longrightarrow> openin X c)"
-  apply (auto simp: locally_path_connected_space_eq_open_path_component_of path_components_of_def topspace_subtopology)
+  apply (auto simp: locally_path_connected_space_eq_open_path_component_of path_components_of_def)
   by (metis imageI inf.absorb_iff2 openin_closedin_eq)
 
 lemma openin_path_component_of_locally_path_connected_space:
@@ -275,7 +275,7 @@
           by (metis (no_types, lifting) \<open>f x \<in> C\<close> x disjnt_iff image_eqI)
       qed
       then show "?T \<subseteq> {x \<in> topspace X. f x \<in> C}"
-        by (force simp: path_component_of_equiv topspace_subtopology)
+        by (force simp: path_component_of_equiv)
     qed
   qed
   then show "openin Y C"
diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Thu Nov 28 20:38:07 2019 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy	Thu Nov 28 23:06:22 2019 +0100
@@ -457,7 +457,7 @@
 qed
 
 lemma path_join_imp: "\<lbrakk>path g1; path g2; pathfinish g1 = pathstart g2\<rbrakk> \<Longrightarrow> path(g1 +++ g2)"
-  by (simp add: path_join)
+  by (simp)
 
 lemma simple_path_join_loop:
   assumes "arc g1" "arc g2"
@@ -547,7 +547,7 @@
    } note * = this
   show ?thesis
     apply (simp add: arc_def inj_on_def)
-    apply (clarsimp simp add: arc_imp_path assms path_join)
+    apply (clarsimp simp add: arc_imp_path assms)
     apply (simp add: joinpaths_def split: if_split_asm)
     apply (force dest: inj_onD [OF injg1])
     apply (metis *)
@@ -831,7 +831,7 @@
 
 lemma sum_le_prod1:
   fixes a::real shows "\<lbrakk>a \<le> 1; b \<le> 1\<rbrakk> \<Longrightarrow> a + b \<le> 1 + a * b"
-by (metis add.commute affine_ineq less_eq_real_def mult.right_neutral)
+by (metis add.commute affine_ineq mult.right_neutral)
 
 lemma simple_path_subpath_eq:
   "simple_path(subpath u v g) \<longleftrightarrow>
@@ -1545,7 +1545,7 @@
   then obtain g where g: "path g" "path_image g \<subseteq> S" "pathstart g = x1" "pathfinish g = x2"
     using assms[unfolded path_connected_def,rule_format,of x1 x2] by auto
   have *: "connected {0..1::real}"
-    by (auto intro!: convex_connected convex_real_interval)
+    by (auto intro!: convex_connected)
   have "{0..1} \<subseteq> {x \<in> {0..1}. g x \<in> e1} \<union> {x \<in> {0..1}. g x \<in> e2}"
     using as(3) g(2)[unfolded path_defs] by blast
   moreover have "{x \<in> {0..1}. g x \<in> e1} \<inter> {x \<in> {0..1}. g x \<in> e2} = {}"
@@ -1691,7 +1691,7 @@
   apply clarify
   apply (rule_tac x="\<lambda>x. a" in exI)
   apply (simp add: image_constant_conv)
-  apply (simp add: path_def continuous_on_const)
+  apply (simp add: path_def)
   done
 
 lemma path_connected_Un:
@@ -1796,7 +1796,7 @@
   case True show ?thesis
     apply (rule subset_antisym)
     apply (simp add: path_component_subset)
-    by (simp add: True path_component_maximal path_component_refl path_connected_path_component)
+    by (simp add: True path_component_maximal path_component_refl)
 next
   case False then show ?thesis
     by (metis False empty_iff path_component_eq_empty)
@@ -2183,7 +2183,7 @@
   obtain a where "\<And>S. S \<in> \<A> \<Longrightarrow> a \<in> S"
     using assms by blast
   then have "\<And>x. x \<in> topspace (subtopology X (\<Union>\<A>)) \<Longrightarrow> path_component_of (subtopology X (\<Union>\<A>)) a x"
-    apply (simp add: topspace_subtopology)
+    apply (simp)
     by (meson Union_upper \<A> path_component_of path_connectedin_subtopology)
   then show ?thesis
     using \<A> unfolding path_connectedin_def
@@ -2429,11 +2429,11 @@
 proof (cases r "0::real" rule: linorder_cases)
   case less
   then show ?thesis
-    by (simp add: path_connected_empty)
+    by (simp)
 next
   case equal
   then show ?thesis
-    by (simp add: path_connected_singleton)
+    by (simp)
 next
   case greater
   then have eq: "(sphere (0::'a) r) = (\<lambda>x. (r / norm x) *\<^sub>R x) ` (- {0::'a})"
@@ -3303,7 +3303,7 @@
 qed
 
 lemma inside_empty [simp]: "inside {} = ({} :: 'a :: {real_normed_vector, perfect_space} set)"
-  by (simp add: inside_def connected_component_UNIV)
+  by (simp add: inside_def)
 
 lemma outside_empty [simp]: "outside {} = (UNIV :: 'a :: {real_normed_vector, perfect_space} set)"
 using inside_empty inside_Un_outside by blast
@@ -3346,7 +3346,7 @@
         by (simp add: scaleR_add_left [symmetric] field_split_simps)
       then have False
         using convexD_alt [OF s \<open>a \<in> s\<close> ins, of "1/(u*C + 1)"] \<open>C>0\<close> \<open>z \<notin> s\<close> Cpos u
-        by (simp add: * field_split_simps algebra_simps)
+        by (simp add: * field_split_simps)
     } note contra = this
     have "connected_component (- s) z (z + C *\<^sub>R (z-a))"
       apply (rule connected_componentI [OF connected_segment [of z "z + C *\<^sub>R (z-a)"]])
diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Retracts.thy
--- a/src/HOL/Analysis/Retracts.thy	Thu Nov 28 20:38:07 2019 +0100
+++ b/src/HOL/Analysis/Retracts.thy	Thu Nov 28 23:06:22 2019 +0100
@@ -604,7 +604,7 @@
       show "continuous_on W (\<lambda>x. if x \<in> W - V then a else h (j x, g x))"
         apply (subst Weq)
         apply (rule continuous_on_cases_local)
-            apply (simp_all add: Weq [symmetric] WWV continuous_on_const *)
+            apply (simp_all add: Weq [symmetric] WWV *)
           using WV' closedin_diff apply fastforce
          apply (auto simp: j0 j1)
         done
@@ -1408,7 +1408,7 @@
   proof (intro exI conjI)
     show "continuous_on (S \<union> T) (\<lambda>x. if x \<in> S then x else r x)"
       apply (rule continuous_on_cases_local [OF clS clT])
-      using r by (auto simp: continuous_on_id)
+      using r by (auto)
   qed (use r in auto)
   also have "\<dots> retract_of U"
     by (rule Un)
@@ -2136,7 +2136,7 @@
   proof
     have "continuous_on (T \<union> (S - T)) ?g"
       apply (rule continuous_on_cases_local)
-      using Seq clo ope by (auto simp: contf continuous_on_const intro: continuous_on_cases_local)
+      using Seq clo ope by (auto simp: contf intro: continuous_on_cases_local)
     with Seq show "continuous_on S ?g"
       by metis
     show "?g ` S \<subseteq> U"
diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Thu Nov 28 20:38:07 2019 +0100
+++ b/src/HOL/Analysis/Starlike.thy	Thu Nov 28 23:06:22 2019 +0100
@@ -644,7 +644,7 @@
     fix i :: 'a
     assume i: "i \<in> Basis"
     show "0 < ?a \<bullet> i"
-      unfolding **[OF i] by (auto simp add: Suc_le_eq DIM_positive)
+      unfolding **[OF i] by (auto simp add: Suc_le_eq)
   next
     have "sum ((\<bullet>) ?a) ?D = sum (\<lambda>i. inverse (2 * real DIM('a))) ?D"
       apply (rule sum.cong)
@@ -3676,7 +3676,7 @@
   case False
   { assume "card s = Suc (card Basis)"
     then have cs: "Suc 0 < card s"
-      by (simp add: DIM_positive)
+      by (simp)
     with subset_singletonD have "\<exists>y \<in> s. y \<noteq> x"
       by (cases "s \<le> {x}") fastforce+
   } note [dest!] = this
@@ -4242,9 +4242,9 @@
     show "{x. 0 < f x} \<inter> {x. f x < 0} = {}"
       by auto
     show "open {x. 0 < f x}"
-      by (simp add: open_Collect_less contf continuous_on_const)
+      by (simp add: open_Collect_less contf)
     show "open {x. f x < 0}"
-      by (simp add: open_Collect_less contf continuous_on_const)
+      by (simp add: open_Collect_less contf)
     show "S \<subseteq> {x. 0 < f x}"
       apply (clarsimp simp add: f_def setdist_sing_in_set)
       using assms
diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Nov 28 20:38:07 2019 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Nov 28 23:06:22 2019 +0100
@@ -347,7 +347,7 @@
   then have "span (cball 0 e) = (UNIV :: 'n::euclidean_space set)"
     by auto
   then show ?thesis
-    using dim_span[of "cball (0 :: 'n::euclidean_space) e"] by (auto simp: dim_UNIV)
+    using dim_span[of "cball (0 :: 'n::euclidean_space) e"] by (auto)
 qed
 
 
@@ -424,7 +424,7 @@
 proof -
   define e' where "e' = e / (2 * sqrt (real (DIM ('a))))"
   then have e: "e' > 0"
-    using assms by (auto simp: DIM_positive)
+    using assms by (auto)
   have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> y < x \<bullet> i \<and> x \<bullet> i - y < e'" (is "\<forall>i. ?th i")
   proof
     fix i
@@ -884,7 +884,7 @@
       by (simp add: dual_order.antisym euclidean_eqI)
   }
   moreover have "c \<in> cbox (m *\<^sub>R a + c) (m *\<^sub>R b + c)"
-    unfolding True by (auto simp: cbox_sing)
+    unfolding True by (auto)
   ultimately show ?thesis using True by (auto simp: cbox_def)
 next
   case False
@@ -1171,16 +1171,16 @@
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Openness of halfspaces.\<close>
 
 lemma open_halfspace_lt: "open {x. inner a x < b}"
-  by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id)
+  by (simp add: open_Collect_less continuous_on_inner)
 
 lemma open_halfspace_gt: "open {x. inner a x > b}"
-  by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id)
+  by (simp add: open_Collect_less continuous_on_inner)
 
 lemma open_halfspace_component_lt: "open {x::'a::euclidean_space. x\<bullet>i < a}"
-  by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id)
+  by (simp add: open_Collect_less continuous_on_inner)
 
 lemma open_halfspace_component_gt: "open {x::'a::euclidean_space. x\<bullet>i > a}"
-  by (simp add: open_Collect_less continuous_on_inner continuous_on_const continuous_on_id)
+  by (simp add: open_Collect_less continuous_on_inner)
 
 lemma eucl_less_eq_halfspaces:
   fixes a :: "'a::euclidean_space"
@@ -1199,29 +1199,29 @@
   unfolding continuous_at by (intro tendsto_intros)
 
 lemma closed_halfspace_le: "closed {x. inner a x \<le> b}"
-  by (simp add: closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id)
+  by (simp add: closed_Collect_le continuous_on_inner)
 
 lemma closed_halfspace_ge: "closed {x. inner a x \<ge> b}"
-  by (simp add: closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id)
+  by (simp add: closed_Collect_le continuous_on_inner)
 
 lemma closed_hyperplane: "closed {x. inner a x = b}"
-  by (simp add: closed_Collect_eq continuous_on_inner continuous_on_const continuous_on_id)
+  by (simp add: closed_Collect_eq continuous_on_inner)
 
 lemma closed_halfspace_component_le: "closed {x::'a::euclidean_space. x\<bullet>i \<le> a}"
-  by (simp add: closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id)
+  by (simp add: closed_Collect_le continuous_on_inner)
 
 lemma closed_halfspace_component_ge: "closed {x::'a::euclidean_space. x\<bullet>i \<ge> a}"
-  by (simp add: closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id)
+  by (simp add: closed_Collect_le continuous_on_inner)
 
 lemma closed_interval_left:
   fixes b :: "'a::euclidean_space"
   shows "closed {x::'a. \<forall>i\<in>Basis. x\<bullet>i \<le> b\<bullet>i}"
-  by (simp add: Collect_ball_eq closed_INT closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id)
+  by (simp add: Collect_ball_eq closed_INT closed_Collect_le continuous_on_inner)
 
 lemma closed_interval_right:
   fixes a :: "'a::euclidean_space"
   shows "closed {x::'a. \<forall>i\<in>Basis. a\<bullet>i \<le> x\<bullet>i}"
-  by (simp add: Collect_ball_eq closed_INT closed_Collect_le continuous_on_inner continuous_on_const continuous_on_id)
+  by (simp add: Collect_ball_eq closed_INT closed_Collect_le continuous_on_inner)
 
 lemma interior_halfspace_le [simp]:
   assumes "a \<noteq> 0"
@@ -1646,7 +1646,7 @@
   {
     fix e::real
     assume "e > 0"
-    hence "e / real_of_nat DIM('a) > 0" by (simp add: DIM_positive)
+    hence "e / real_of_nat DIM('a) > 0" by (simp)
     with l have "eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e / (real_of_nat DIM('a))) sequentially"
       by simp
     moreover
@@ -1948,7 +1948,7 @@
     fix e :: real
     assume "e > 0"
     moreover have "clamp a b x \<in> cbox a b"
-      by (simp add: clamp_in_interval le)
+      by (simp add: le)
     moreover note f_cont[simplified continuous_on_iff]
     ultimately
     obtain d where d: "0 < d"
@@ -2192,7 +2192,7 @@
     qed
     then show "\<forall>y. dist y (f x) < \<delta> \<longrightarrow> y \<in> f ` A"
       using \<open>e > 0\<close> \<open>B > 0\<close>
-      by (auto simp: \<delta>_def field_split_simps mult_less_0_iff)
+      by (auto simp: \<delta>_def field_split_simps)
   qed
 qed
 
@@ -2349,8 +2349,7 @@
 proof -
   let ?D = "{i\<in>Basis. P i}"
   have "closed (\<Inter>i\<in>?D. {x::'a. x\<bullet>i = 0})"
-    by (simp add: closed_INT closed_Collect_eq continuous_on_inner
-        continuous_on_const continuous_on_id)
+    by (simp add: closed_INT closed_Collect_eq continuous_on_inner)
   also have "(\<Inter>i\<in>?D. {x::'a. x\<bullet>i = 0}) = ?A"
     by auto
   finally show "closed ?A" .
@@ -2392,7 +2391,7 @@
 
 lemma closed_span [iff]: "closed (span s)"
   for s :: "'a::euclidean_space set"
-  by (simp add: closed_subspace subspace_span)
+  by (simp add: closed_subspace)
 
 lemma dim_closure [simp]: "dim (closure s) = dim s" (is "?dc = ?d")
   for s :: "'a::euclidean_space set"
diff -r a25b6f79043f -r 575b3a818de5 src/HOL/Analysis/Weierstrass_Theorems.thy
--- a/src/HOL/Analysis/Weierstrass_Theorems.thy	Thu Nov 28 20:38:07 2019 +0100
+++ b/src/HOL/Analysis/Weierstrass_Theorems.thy	Thu Nov 28 23:06:22 2019 +0100
@@ -526,7 +526,7 @@
       using Bernoulli_inequality [of "-e / card subA" "card subA"] e cardp
       by (auto simp: field_simps)
     also have "... = (\<Prod>w \<in> subA. 1 - e / card subA)"
-      by (simp add: prod_constant subA(2))
+      by (simp add: subA(2))
     also have "... < pff x"
       apply (simp add: pff_def)
       apply (rule prod_mono_strict [where f = "\<lambda>x. 1 - e / card subA", simplified])
@@ -1117,7 +1117,7 @@
     have "\<exists>p. real_polynomial_function p \<and> (\<forall>x \<in> S. \<bar>f x \<bullet> b - p x\<bar> < e / DIM('b))"
       apply (rule exE [OF Stone_Weierstrass_real_polynomial_function [OF S _, of "\<lambda>x. f x \<bullet> b" "e / card Basis"]])
       using e f
-      apply (auto simp: Euclidean_Space.DIM_positive intro: continuous_intros)
+      apply (auto intro: continuous_intros)
       done
   }
   then obtain pf where pf:
@@ -1140,7 +1140,7 @@
       apply (rule DIM_positive)
       done
     also have "... = e"
-      using DIM_positive by (simp add: field_simps)
+      by (simp add: field_simps)
     finally have "norm (\<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b - pf b x *\<^sub>R b) < e" .
   }
   ultimately