merged
authorpaulson
Fri Sep 08 15:27:48 2017 +0100 (21 months ago)
changeset 66644b40abdf82145
parent 66642 88f86bcba5b3
parent 66643 f7e38b8583a0
child 66645 db317febaf0b
merged
     1.1 --- a/NEWS	Fri Sep 08 16:20:47 2017 +0200
     1.2 +++ b/NEWS	Fri Sep 08 15:27:48 2017 +0100
     1.3 @@ -220,7 +220,7 @@
     1.4  * Theory "HOL-Library.Permutations": theorem bij_swap_ompose_bij has
     1.5  been renamed to bij_swap_compose_bij. INCOMPATIBILITY.
     1.6  
     1.7 -* New theory "HOL-Library.Going_To_Filter" providing the "f going_to F" 
     1.8 +* New theory "HOL-Library.Going_To_Filter" providing the "f going_to F"
     1.9  filter for describing points x such that f(x) is in the filter F.
    1.10  
    1.11  * Theory "HOL-Library.Formal_Power_Series": constants X/E/L/F have been
    1.12 @@ -255,7 +255,7 @@
    1.13  
    1.14  * Session HOL-Analysis: more material involving arcs, paths, covering
    1.15  spaces, innessential maps, retracts, infinite products, simplicial complexes.
    1.16 -Baire Category theory. Major results include the Jordan Curve Theorem and the Great Picard
    1.17 +Baire Category theorem. Major results include the Jordan Curve Theorem and the Great Picard
    1.18  Theorem.
    1.19  
    1.20  * Session HOL-Algebra has been extended by additional lattice theory:
     2.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Fri Sep 08 16:20:47 2017 +0200
     2.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Fri Sep 08 15:27:48 2017 +0100
     2.3 @@ -140,10 +140,8 @@
     2.4    apply safe
     2.5       apply fastforce
     2.6      apply fastforce
     2.7 -   apply (erule_tac x="x" in allE)
     2.8 -   apply simp
     2.9 -   apply (rule_tac x="{x}" in exI)
    2.10 -  apply auto
    2.11 +   apply (erule_tac x=x in allE, simp)
    2.12 +   apply (rule_tac x="{x}" in exI, auto)
    2.13    done
    2.14  
    2.15  lemma topological_basis_iff:
    2.16 @@ -275,7 +273,7 @@
    2.17    assumes "open X"
    2.18    obtains B' where "B' \<subseteq> B" "X = \<Union>B'"
    2.19    using assms open_countable_basis_ex
    2.20 -  by (atomize_elim) simp
    2.21 +  by atomize_elim simp
    2.22  
    2.23  lemma countable_dense_exists:
    2.24    "\<exists>D::'a set. countable D \<and> (\<forall>X. open X \<longrightarrow> X \<noteq> {} \<longrightarrow> (\<exists>d \<in> D. d \<in> X))"
    2.25 @@ -299,8 +297,7 @@
    2.26    using first_countable_basis[of x]
    2.27    apply atomize_elim
    2.28    apply (elim exE)
    2.29 -  apply (rule_tac x="range A" in exI)
    2.30 -  apply auto
    2.31 +  apply (rule_tac x="range A" in exI, auto)
    2.32    done
    2.33  
    2.34  lemma (in first_countable_topology) first_countable_basis_Int_stableE:
    2.35 @@ -647,7 +644,7 @@
    2.36    using openin_Union[of "{S,T}" U] by auto
    2.37  
    2.38  lemma openin_topspace[intro, simp]: "openin U (topspace U)"
    2.39 -  by (force simp add: openin_Union topspace_def)
    2.40 +  by (force simp: openin_Union topspace_def)
    2.41  
    2.42  lemma openin_subopen: "openin U S \<longleftrightarrow> (\<forall>x \<in> S. \<exists>T. openin U T \<and> x \<in> T \<and> T \<subseteq> S)"
    2.43    (is "?lhs \<longleftrightarrow> ?rhs")
    2.44 @@ -657,7 +654,7 @@
    2.45  next
    2.46    assume H: ?rhs
    2.47    let ?t = "\<Union>{T. openin U T \<and> T \<subseteq> S}"
    2.48 -  have "openin U ?t" by (force simp add: openin_Union)
    2.49 +  have "openin U ?t" by (force simp: openin_Union)
    2.50    also have "?t = S" using H by auto
    2.51    finally show "openin U S" .
    2.52  qed
    2.53 @@ -666,7 +663,7 @@
    2.54    assumes "finite I"
    2.55            "\<And>i. i \<in> I \<Longrightarrow> openin T (U i)"
    2.56    shows "openin T ((\<Inter>i \<in> I. U i) \<inter> topspace T)"
    2.57 -using assms by (induct, auto simp add: inf_sup_aci(2) openin_Int)
    2.58 +using assms by (induct, auto simp: inf_sup_aci(2) openin_Int)
    2.59  
    2.60  lemma openin_INT2 [intro]:
    2.61    assumes "finite I" "I \<noteq> {}"
    2.62 @@ -694,7 +691,7 @@
    2.63    by (simp add: closedin_def)
    2.64  
    2.65  lemma closedin_Un[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<union> T)"
    2.66 -  by (auto simp add: Diff_Un closedin_def)
    2.67 +  by (auto simp: Diff_Un closedin_def)
    2.68  
    2.69  lemma Diff_Inter[intro]: "A - \<Inter>S = \<Union>{A - s|s. s\<in>S}"
    2.70    by auto
    2.71 @@ -722,7 +719,7 @@
    2.72    using closedin_Inter[of "{S,T}" U] by auto
    2.73  
    2.74  lemma openin_closedin_eq: "openin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> closedin U (topspace U - S)"
    2.75 -  apply (auto simp add: closedin_def Diff_Diff_Int inf_absorb2)
    2.76 +  apply (auto simp: closedin_def Diff_Diff_Int inf_absorb2)
    2.77    apply (metis openin_subset subset_eq)
    2.78    done
    2.79  
    2.80 @@ -735,9 +732,9 @@
    2.81    shows "openin U (S - T)"
    2.82  proof -
    2.83    have "S - T = S \<inter> (topspace U - T)" using openin_subset[of U S]  oS cT
    2.84 -    by (auto simp add: topspace_def openin_subset)
    2.85 +    by (auto simp: topspace_def openin_subset)
    2.86    then show ?thesis using oS cT
    2.87 -    by (auto simp add: closedin_def)
    2.88 +    by (auto simp: closedin_def)
    2.89  qed
    2.90  
    2.91  lemma closedin_diff[intro]:
    2.92 @@ -746,9 +743,9 @@
    2.93    shows "closedin U (S - T)"
    2.94  proof -
    2.95    have "S - T = S \<inter> (topspace U - T)"
    2.96 -    using closedin_subset[of U S] oS cT by (auto simp add: topspace_def)
    2.97 +    using closedin_subset[of U S] oS cT by (auto simp: topspace_def)
    2.98    then show ?thesis
    2.99 -    using oS cT by (auto simp add: openin_closedin_eq)
   2.100 +    using oS cT by (auto simp: openin_closedin_eq)
   2.101  qed
   2.102  
   2.103  
   2.104 @@ -781,7 +778,7 @@
   2.105      have "\<Union>K = (\<Union>Sk) \<inter> V"
   2.106        using Sk by auto
   2.107      moreover have "openin U (\<Union>Sk)"
   2.108 -      using Sk by (auto simp add: subset_eq)
   2.109 +      using Sk by (auto simp: subset_eq)
   2.110      ultimately have "?L (\<Union>K)" by blast
   2.111    }
   2.112    ultimately show ?thesis
   2.113 @@ -793,11 +790,11 @@
   2.114    by auto
   2.115  
   2.116  lemma topspace_subtopology: "topspace (subtopology U V) = topspace U \<inter> V"
   2.117 -  by (auto simp add: topspace_def openin_subtopology)
   2.118 +  by (auto simp: topspace_def openin_subtopology)
   2.119  
   2.120  lemma closedin_subtopology: "closedin (subtopology U V) S \<longleftrightarrow> (\<exists>T. closedin U T \<and> S = T \<inter> V)"
   2.121    unfolding closedin_def topspace_subtopology
   2.122 -  by (auto simp add: openin_subtopology)
   2.123 +  by (auto simp: openin_subtopology)
   2.124  
   2.125  lemma openin_subtopology_refl: "openin (subtopology U V) V \<longleftrightarrow> V \<subseteq> topspace U"
   2.126    unfolding openin_subtopology
   2.127 @@ -871,13 +868,13 @@
   2.128    unfolding euclidean_def
   2.129    apply (rule cong[where x=S and y=S])
   2.130    apply (rule topology_inverse[symmetric])
   2.131 -  apply (auto simp add: istopology_def)
   2.132 +  apply (auto simp: istopology_def)
   2.133    done
   2.134  
   2.135  declare open_openin [symmetric, simp]
   2.136  
   2.137  lemma topspace_euclidean [simp]: "topspace euclidean = UNIV"
   2.138 -  by (force simp add: topspace_def)
   2.139 +  by (force simp: topspace_def)
   2.140  
   2.141  lemma topspace_euclidean_subtopology[simp]: "topspace (subtopology euclidean S) = S"
   2.142    by (simp add: topspace_subtopology)
   2.143 @@ -894,7 +891,7 @@
   2.144  text \<open>Basic "localization" results are handy for connectedness.\<close>
   2.145  
   2.146  lemma openin_open: "openin (subtopology euclidean U) S \<longleftrightarrow> (\<exists>T. open T \<and> (S = U \<inter> T))"
   2.147 -  by (auto simp add: openin_subtopology)
   2.148 +  by (auto simp: openin_subtopology)
   2.149  
   2.150  lemma openin_Int_open:
   2.151     "\<lbrakk>openin (subtopology euclidean U) S; open T\<rbrakk>
   2.152 @@ -902,14 +899,14 @@
   2.153  by (metis open_Int Int_assoc openin_open)
   2.154  
   2.155  lemma openin_open_Int[intro]: "open S \<Longrightarrow> openin (subtopology euclidean U) (U \<inter> S)"
   2.156 -  by (auto simp add: openin_open)
   2.157 +  by (auto simp: openin_open)
   2.158  
   2.159  lemma open_openin_trans[trans]:
   2.160    "open S \<Longrightarrow> open T \<Longrightarrow> T \<subseteq> S \<Longrightarrow> openin (subtopology euclidean S) T"
   2.161    by (metis Int_absorb1  openin_open_Int)
   2.162  
   2.163  lemma open_subset: "S \<subseteq> T \<Longrightarrow> open S \<Longrightarrow> openin (subtopology euclidean T) S"
   2.164 -  by (auto simp add: openin_open)
   2.165 +  by (auto simp: openin_open)
   2.166  
   2.167  lemma closedin_closed: "closedin (subtopology euclidean U) S \<longleftrightarrow> (\<exists>T. closed T \<and> S = U \<inter> T)"
   2.168    by (simp add: closedin_subtopology closed_closedin Int_ac)
   2.169 @@ -918,7 +915,7 @@
   2.170    by (metis closedin_closed)
   2.171  
   2.172  lemma closed_subset: "S \<subseteq> T \<Longrightarrow> closed S \<Longrightarrow> closedin (subtopology euclidean T) S"
   2.173 -  by (auto simp add: closedin_closed)
   2.174 +  by (auto simp: closedin_closed)
   2.175  
   2.176  lemma closedin_closed_subset:
   2.177   "\<lbrakk>closedin (subtopology euclidean U) V; T \<subseteq> U; S = V \<inter> T\<rbrakk>
   2.178 @@ -974,8 +971,7 @@
   2.179                   openin (subtopology euclidean s) e2 \<and>
   2.180                   e1 \<union> e2 = s \<and> e1 \<inter> e2 = {} \<and>
   2.181                   e1 \<noteq> {} \<and> e2 \<noteq> {})"
   2.182 -  apply (simp add: connected_openin, safe)
   2.183 -  apply blast
   2.184 +  apply (simp add: connected_openin, safe, blast)
   2.185    by (metis Int_lower1 Un_subset_iff openin_open subset_antisym)
   2.186  
   2.187  lemma connected_closedin:
   2.188 @@ -1016,8 +1012,7 @@
   2.189                   closedin (subtopology euclidean s) e2 \<and>
   2.190                   e1 \<union> e2 = s \<and> e1 \<inter> e2 = {} \<and>
   2.191                   e1 \<noteq> {} \<and> e2 \<noteq> {})"
   2.192 -  apply (simp add: connected_closedin, safe)
   2.193 -  apply blast
   2.194 +  apply (simp add: connected_closedin, safe, blast)
   2.195    by (metis Int_lower1 Un_subset_iff closedin_closed subset_antisym)
   2.196  
   2.197  text \<open>These "transitivity" results are handy too\<close>
   2.198 @@ -1028,15 +1023,15 @@
   2.199    unfolding open_openin openin_open by blast
   2.200  
   2.201  lemma openin_open_trans: "openin (subtopology euclidean T) S \<Longrightarrow> open T \<Longrightarrow> open S"
   2.202 -  by (auto simp add: openin_open intro: openin_trans)
   2.203 +  by (auto simp: openin_open intro: openin_trans)
   2.204  
   2.205  lemma closedin_trans[trans]:
   2.206    "closedin (subtopology euclidean T) S \<Longrightarrow> closedin (subtopology euclidean U) T \<Longrightarrow>
   2.207      closedin (subtopology euclidean U) S"
   2.208 -  by (auto simp add: closedin_closed closed_closedin closed_Inter Int_assoc)
   2.209 +  by (auto simp: closedin_closed closed_closedin closed_Inter Int_assoc)
   2.210  
   2.211  lemma closedin_closed_trans: "closedin (subtopology euclidean T) S \<Longrightarrow> closed T \<Longrightarrow> closed S"
   2.212 -  by (auto simp add: closedin_closed intro: closedin_trans)
   2.213 +  by (auto simp: closedin_closed intro: closedin_trans)
   2.214  
   2.215  lemma openin_subtopology_Int_subset:
   2.216     "\<lbrakk>openin (subtopology euclidean u) (u \<inter> S); v \<subseteq> u\<rbrakk> \<Longrightarrow> openin (subtopology euclidean v) (v \<inter> S)"
   2.217 @@ -1198,8 +1193,7 @@
   2.218  apply (simp add: openin_contains_ball)
   2.219  apply (rule iffI)
   2.220  apply (auto dest!: bspec)
   2.221 -apply (rule_tac x="e/2" in exI)
   2.222 -apply force+
   2.223 +apply (rule_tac x="e/2" in exI, force+)
   2.224  done
   2.225  
   2.226  lemma ball_eq_empty[simp]: "ball x e = {} \<longleftrightarrow> e \<le> 0"
   2.227 @@ -1295,7 +1289,7 @@
   2.228  lemma rational_boxes:
   2.229    fixes x :: "'a::euclidean_space"
   2.230    assumes "e > 0"
   2.231 -  shows "\<exists>a b. (\<forall>i\<in>Basis. a \<bullet> i \<in> \<rat> \<and> b \<bullet> i \<in> \<rat> ) \<and> x \<in> box a b \<and> box a b \<subseteq> ball x e"
   2.232 +  shows "\<exists>a b. (\<forall>i\<in>Basis. a \<bullet> i \<in> \<rat> \<and> b \<bullet> i \<in> \<rat>) \<and> x \<in> box a b \<and> box a b \<subseteq> ball x e"
   2.233  proof -
   2.234    define e' where "e' = e / (2 * sqrt (real (DIM ('a))))"
   2.235    then have e: "e' > 0"
   2.236 @@ -1610,7 +1604,7 @@
   2.237          then have "c \<bullet> j < ?x \<bullet> j \<and> ?x \<bullet> j < d \<bullet> j"
   2.238            apply (cases "j = i")
   2.239            using as(2)[THEN bspec[where x=j]] i
   2.240 -          apply (auto simp add: as2)
   2.241 +          apply (auto simp: as2)
   2.242            done
   2.243        }
   2.244        then have "?x\<in>box c d"
   2.245 @@ -1636,7 +1630,7 @@
   2.246          then have "d \<bullet> j > ?x \<bullet> j \<and> ?x \<bullet> j > c \<bullet> j"
   2.247            apply (cases "j = i")
   2.248            using as(2)[THEN bspec[where x=j]]
   2.249 -          apply (auto simp add: as2)
   2.250 +          apply (auto simp: as2)
   2.251            done
   2.252        }
   2.253        then have "?x\<in>box c d"
   2.254 @@ -1691,7 +1685,7 @@
   2.255    then have "cbox a b \<subseteq> cbox c d" "cbox c d \<subseteq> cbox a b"
   2.256      by auto
   2.257    then show ?rhs
   2.258 -    by (force simp add: subset_box box_eq_empty intro: antisym euclidean_eqI)
   2.259 +    by (force simp: subset_box box_eq_empty intro: antisym euclidean_eqI)
   2.260  next
   2.261    assume ?rhs
   2.262    then show ?lhs
   2.263 @@ -1737,13 +1731,13 @@
   2.264  qed
   2.265  
   2.266  lemma subset_box_complex:
   2.267 -   "cbox a b \<subseteq> cbox c d \<longleftrightarrow> 
   2.268 +   "cbox a b \<subseteq> cbox c d \<longleftrightarrow>
   2.269        (Re a \<le> Re b \<and> Im a \<le> Im b) \<longrightarrow> Re a \<ge> Re c \<and> Im a \<ge> Im c \<and> Re b \<le> Re d \<and> Im b \<le> Im d"
   2.270 -   "cbox a b \<subseteq> box c d \<longleftrightarrow> 
   2.271 +   "cbox a b \<subseteq> box c d \<longleftrightarrow>
   2.272        (Re a \<le> Re b \<and> Im a \<le> Im b) \<longrightarrow> Re a > Re c \<and> Im a > Im c \<and> Re b < Re d \<and> Im b < Im d"
   2.273     "box a b \<subseteq> cbox c d \<longleftrightarrow>
   2.274        (Re a < Re b \<and> Im a < Im b) \<longrightarrow> Re a \<ge> Re c \<and> Im a \<ge> Im c \<and> Re b \<le> Re d \<and> Im b \<le> Im d"
   2.275 -   "box a b \<subseteq> box c d \<longleftrightarrow> 
   2.276 +   "box a b \<subseteq> box c d \<longleftrightarrow>
   2.277        (Re a < Re b \<and> Im a < Im b) \<longrightarrow> Re a \<ge> Re c \<and> Im a \<ge> Im c \<and> Re b \<le> Re d \<and> Im b \<le> Im d"
   2.278    by (subst subset_box; force simp: Basis_complex_def)+
   2.279  
   2.280 @@ -1841,7 +1835,7 @@
   2.281    define y where
   2.282      "y = rec_list (s j) (\<lambda>j _ Y. (\<Sum>i\<in>Basis. (if i = j then s i \<bullet> i else Y \<bullet> i) *\<^sub>R i))"
   2.283    have "x = (\<Sum>i\<in>Basis. (if i \<in> set bs then s i \<bullet> i else s j \<bullet> i) *\<^sub>R i)"
   2.284 -    using bs by (auto simp add: s(1)[symmetric] euclidean_representation)
   2.285 +    using bs by (auto simp: s(1)[symmetric] euclidean_representation)
   2.286    also have [symmetric]: "y bs = \<dots>"
   2.287      using bs(2) bs(1)[THEN equalityD1]
   2.288      by (induct bs) (auto simp: y_def euclidean_representation intro!: euclidean_eqI[where 'a='a])
   2.289 @@ -1880,7 +1874,7 @@
   2.290      by blast
   2.291  qed
   2.292  
   2.293 -  
   2.294 +
   2.295  subsection \<open>Connectedness\<close>
   2.296  
   2.297  lemma connected_local:
   2.298 @@ -1996,7 +1990,7 @@
   2.299    done
   2.300  
   2.301  lemma islimpt_EMPTY[simp]: "\<not> x islimpt {}"
   2.302 -  by (auto simp add: islimpt_def)
   2.303 +  by (auto simp: islimpt_def)
   2.304  
   2.305  lemma finite_set_avoid:
   2.306    fixes a :: "'a::metric_space"
   2.307 @@ -2047,7 +2041,7 @@
   2.308      from z y have "dist z y < e"
   2.309        by (intro dist_triangle_lt [where z=x]) simp
   2.310      from d[rule_format, OF y(1) z(1) this] y z show ?thesis
   2.311 -      by (auto simp add: dist_commute)
   2.312 +      by (auto simp: dist_commute)
   2.313    qed
   2.314    then show ?thesis
   2.315      by (metis islimpt_approachable closed_limpt [where 'a='a])
   2.316 @@ -2065,7 +2059,7 @@
   2.317  lemma closed_Ints [simp]: "closed (\<int> :: 'a :: real_normed_algebra_1 set)"
   2.318    unfolding Ints_def by (rule closed_of_int_image)
   2.319  
   2.320 -lemma closed_subset_Ints: 
   2.321 +lemma closed_subset_Ints:
   2.322    fixes A :: "'a :: real_normed_algebra_1 set"
   2.323    assumes "A \<subseteq> \<int>"
   2.324    shows   "closed A"
   2.325 @@ -2095,10 +2089,10 @@
   2.326    by (simp add: interior_def open_Union)
   2.327  
   2.328  lemma interior_subset: "interior S \<subseteq> S"
   2.329 -  by (auto simp add: interior_def)
   2.330 +  by (auto simp: interior_def)
   2.331  
   2.332  lemma interior_maximal: "T \<subseteq> S \<Longrightarrow> open T \<Longrightarrow> T \<subseteq> interior S"
   2.333 -  by (auto simp add: interior_def)
   2.334 +  by (auto simp: interior_def)
   2.335  
   2.336  lemma interior_open: "open S \<Longrightarrow> interior S = S"
   2.337    by (intro equalityI interior_subset interior_maximal subset_refl)
   2.338 @@ -2119,7 +2113,7 @@
   2.339    using open_interior by (rule interior_open)
   2.340  
   2.341  lemma interior_mono: "S \<subseteq> T \<Longrightarrow> interior S \<subseteq> interior T"
   2.342 -  by (auto simp add: interior_def)
   2.343 +  by (auto simp: interior_def)
   2.344  
   2.345  lemma interior_unique:
   2.346    assumes "T \<subseteq> S" and "open T"
   2.347 @@ -2129,8 +2123,7 @@
   2.348  
   2.349  lemma interior_singleton [simp]: "interior {a} = {}"
   2.350    for a :: "'a::perfect_space"
   2.351 -  apply (rule interior_unique)
   2.352 -    apply simp_all
   2.353 +  apply (rule interior_unique, simp_all)
   2.354    using not_open_singleton subset_singletonD
   2.355    apply fastforce
   2.356    done
   2.357 @@ -2154,7 +2147,7 @@
   2.358    unfolding interior_def islimpt_def
   2.359    apply (clarsimp, rename_tac T T')
   2.360    apply (drule_tac x="T \<inter> T'" in spec)
   2.361 -  apply (auto simp add: open_Int)
   2.362 +  apply (auto simp: open_Int)
   2.363    done
   2.364  
   2.365  lemma interior_closed_Un_empty_interior:
   2.366 @@ -2251,7 +2244,7 @@
   2.367  definition "closure S = S \<union> {x | x. x islimpt S}"
   2.368  
   2.369  lemma interior_closure: "interior S = - (closure (- S))"
   2.370 -  by (auto simp add: interior_def closure_def islimpt_def)
   2.371 +  by (auto simp: interior_def closure_def islimpt_def)
   2.372  
   2.373  lemma closure_interior: "closure S = - interior (- S)"
   2.374    by (simp add: interior_closure)
   2.375 @@ -2263,7 +2256,7 @@
   2.376    by (simp add: closure_def)
   2.377  
   2.378  lemma closure_hull: "closure S = closed hull S"
   2.379 -  by (auto simp add: hull_def closure_interior interior_def)
   2.380 +  by (auto simp: hull_def closure_interior interior_def)
   2.381  
   2.382  lemma closure_eq: "closure S = S \<longleftrightarrow> closed S"
   2.383    unfolding closure_hull using closed_Inter by (rule hull_eq)
   2.384 @@ -2345,14 +2338,12 @@
   2.385    fix T
   2.386    assume "A \<times> B \<subseteq> T" and "closed T"
   2.387    then show "closure A \<times> closure B \<subseteq> T"
   2.388 -    apply (simp add: closed_def open_prod_def)
   2.389 -    apply clarify
   2.390 +    apply (simp add: closed_def open_prod_def, clarify)
   2.391      apply (rule ccontr)
   2.392      apply (drule_tac x="(a, b)" in bspec, simp, clarify, rename_tac C D)
   2.393      apply (simp add: closure_interior interior_def)
   2.394      apply (drule_tac x=C in spec)
   2.395 -    apply (drule_tac x=D in spec)
   2.396 -    apply auto
   2.397 +    apply (drule_tac x=D in spec, auto)
   2.398      done
   2.399  qed
   2.400  
   2.401 @@ -2406,8 +2397,7 @@
   2.402    "closedin (subtopology euclidean T) S \<longleftrightarrow> S \<subseteq> T \<and> (\<forall>x. x islimpt S \<and> x \<in> T \<longrightarrow> x \<in> S)"
   2.403    apply (simp add: closedin_closed, safe)
   2.404     apply (simp add: closed_limpt islimpt_subset)
   2.405 -  apply (rule_tac x="closure S" in exI)
   2.406 -  apply simp
   2.407 +  apply (rule_tac x="closure S" in exI, simp)
   2.408    apply (force simp: closure_def)
   2.409    done
   2.410  
   2.411 @@ -2651,11 +2641,9 @@
   2.412  lemma connected_component_eq_eq:
   2.413    "connected_component_set s x = connected_component_set s y \<longleftrightarrow>
   2.414      x \<notin> s \<and> y \<notin> s \<or> x \<in> s \<and> y \<in> s \<and> connected_component s x y"
   2.415 -  apply (cases "y \<in> s")
   2.416 -   apply (simp add:)
   2.417 +  apply (cases "y \<in> s", simp)
   2.418     apply (metis connected_component_eq connected_component_eq_empty connected_component_refl_eq mem_Collect_eq)
   2.419 -  apply (cases "x \<in> s")
   2.420 -   apply (simp add:)
   2.421 +  apply (cases "x \<in> s", simp)
   2.422     apply (metis connected_component_eq_empty)
   2.423    using connected_component_eq_empty
   2.424    apply blast
   2.425 @@ -2864,8 +2852,7 @@
   2.426    by (meson connected_component_def connected_component_trans)
   2.427  
   2.428  lemma exists_component_superset: "\<lbrakk>t \<subseteq> s; s \<noteq> {}; connected t\<rbrakk> \<Longrightarrow> \<exists>c. c \<in> components s \<and> t \<subseteq> c"
   2.429 -  apply (cases "t = {}")
   2.430 -   apply force
   2.431 +  apply (cases "t = {}", force)
   2.432    apply (metis components_def ex_in_conv connected_component_maximal contra_subsetD image_eqI)
   2.433    done
   2.434  
   2.435 @@ -2911,13 +2898,12 @@
   2.436    have *: "connected_component_set s x \<subseteq> s \<inter> closure (connected_component_set s x)"
   2.437      by (auto simp: closure_def connected_component_in)
   2.438    have "connected_component s x y \<Longrightarrow> s \<inter> closure (connected_component_set s x) \<subseteq> connected_component_set s x"
   2.439 -    apply (rule connected_component_maximal)
   2.440 -      apply simp
   2.441 +    apply (rule connected_component_maximal, simp)
   2.442      using closure_subset connected_component_in apply fastforce
   2.443      using * connected_intermediate_closure apply blast+
   2.444      done
   2.445    with y * show ?thesis
   2.446 -    by (auto simp add: Topology_Euclidean_Space.closedin_closed)
   2.447 +    by (auto simp: Topology_Euclidean_Space.closedin_closed)
   2.448  qed
   2.449  
   2.450  
   2.451 @@ -2929,13 +2915,13 @@
   2.452    by (simp add: frontier_def closed_Diff)
   2.453  
   2.454  lemma frontier_closures: "frontier S = closure S \<inter> closure (- S)"
   2.455 -  by (auto simp add: frontier_def interior_closure)
   2.456 +  by (auto simp: frontier_def interior_closure)
   2.457  
   2.458  lemma frontier_straddle:
   2.459    fixes a :: "'a::metric_space"
   2.460    shows "a \<in> frontier S \<longleftrightarrow> (\<forall>e>0. (\<exists>x\<in>S. dist a x < e) \<and> (\<exists>x. x \<notin> S \<and> dist a x < e))"
   2.461    unfolding frontier_def closure_interior
   2.462 -  by (auto simp add: mem_interior subset_eq ball_def)
   2.463 +  by (auto simp: mem_interior subset_eq ball_def)
   2.464  
   2.465  lemma frontier_subset_closed: "closed S \<Longrightarrow> frontier S \<subseteq> S"
   2.466    by (metis frontier_def closure_closed Diff_subset)
   2.467 @@ -2956,7 +2942,7 @@
   2.468  qed
   2.469  
   2.470  lemma frontier_complement [simp]: "frontier (- S) = frontier S"
   2.471 -  by (auto simp add: frontier_def closure_complement interior_complement)
   2.472 +  by (auto simp: frontier_def closure_complement interior_complement)
   2.473  
   2.474  lemma frontier_disjoint_eq: "frontier S \<inter> S = {} \<longleftrightarrow> open S"
   2.475    using frontier_complement frontier_subset_eq[of "- S"]
   2.476 @@ -3054,33 +3040,31 @@
   2.477  
   2.478  lemma Lim_within_le: "(f \<longlongrightarrow> l)(at a within S) \<longleftrightarrow>
   2.479      (\<forall>e>0. \<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a \<le> d \<longrightarrow> dist (f x) l < e)"
   2.480 -  by (auto simp add: tendsto_iff eventually_at_le)
   2.481 +  by (auto simp: tendsto_iff eventually_at_le)
   2.482  
   2.483  lemma Lim_within: "(f \<longlongrightarrow> l) (at a within S) \<longleftrightarrow>
   2.484      (\<forall>e >0. \<exists>d>0. \<forall>x \<in> S. 0 < dist x a \<and> dist x a  < d \<longrightarrow> dist (f x) l < e)"
   2.485 -  by (auto simp add: tendsto_iff eventually_at)
   2.486 +  by (auto simp: tendsto_iff eventually_at)
   2.487  
   2.488  corollary Lim_withinI [intro?]:
   2.489    assumes "\<And>e. e > 0 \<Longrightarrow> \<exists>d>0. \<forall>x \<in> S. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l \<le> e"
   2.490    shows "(f \<longlongrightarrow> l) (at a within S)"
   2.491    apply (simp add: Lim_within, clarify)
   2.492 -  apply (rule ex_forward [OF assms [OF half_gt_zero]])
   2.493 -  apply auto
   2.494 +  apply (rule ex_forward [OF assms [OF half_gt_zero]], auto)
   2.495    done
   2.496  
   2.497  lemma Lim_at: "(f \<longlongrightarrow> l) (at a) \<longleftrightarrow>
   2.498      (\<forall>e >0. \<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d  \<longrightarrow> dist (f x) l < e)"
   2.499 -  by (auto simp add: tendsto_iff eventually_at)
   2.500 +  by (auto simp: tendsto_iff eventually_at)
   2.501  
   2.502  lemma Lim_at_infinity: "(f \<longlongrightarrow> l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x. norm x \<ge> b \<longrightarrow> dist (f x) l < e)"
   2.503 -  by (auto simp add: tendsto_iff eventually_at_infinity)
   2.504 +  by (auto simp: tendsto_iff eventually_at_infinity)
   2.505  
   2.506  corollary Lim_at_infinityI [intro?]:
   2.507    assumes "\<And>e. e > 0 \<Longrightarrow> \<exists>B. \<forall>x. norm x \<ge> B \<longrightarrow> dist (f x) l \<le> e"
   2.508    shows "(f \<longlongrightarrow> l) at_infinity"
   2.509    apply (simp add: Lim_at_infinity, clarify)
   2.510 -  apply (rule ex_forward [OF assms [OF half_gt_zero]])
   2.511 -   apply auto
   2.512 +  apply (rule ex_forward [OF assms [OF half_gt_zero]], auto)
   2.513    done
   2.514  
   2.515  lemma Lim_eventually: "eventually (\<lambda>x. f x = l) net \<Longrightarrow> (f \<longlongrightarrow> l) net"
   2.516 @@ -3538,7 +3522,7 @@
   2.517  lemma closure_approachable:
   2.518    fixes S :: "'a::metric_space set"
   2.519    shows "x \<in> closure S \<longleftrightarrow> (\<forall>e>0. \<exists>y\<in>S. dist y x < e)"
   2.520 -  apply (auto simp add: closure_def islimpt_approachable)
   2.521 +  apply (auto simp: closure_def islimpt_approachable)
   2.522    apply (metis dist_self)
   2.523    done
   2.524  
   2.525 @@ -3567,7 +3551,7 @@
   2.526      with assms obtain x where "x \<in> S" "x < Inf S + e"
   2.527        by (subst (asm) cInf_less_iff) auto
   2.528      with * have "\<exists>x\<in>S. dist x (Inf S) < e"
   2.529 -      by (intro bexI[of _ x]) (auto simp add: dist_real_def)
   2.530 +      by (intro bexI[of _ x]) (auto simp: dist_real_def)
   2.531    }
   2.532    then show ?thesis unfolding closure_approachable by auto
   2.533  qed
   2.534 @@ -3647,7 +3631,7 @@
   2.535    by (simp add: infdist_def)
   2.536  
   2.537  lemma infdist_nonneg: "0 \<le> infdist x A"
   2.538 -  by (auto simp add: infdist_def intro: cINF_greatest)
   2.539 +  by (auto simp: infdist_def intro: cINF_greatest)
   2.540  
   2.541  lemma infdist_le: "a \<in> A \<Longrightarrow> infdist x A \<le> dist x a"
   2.542    by (auto intro: cINF_lower simp add: infdist_def)
   2.543 @@ -3772,8 +3756,7 @@
   2.544  lemma seq_offset_neg: (* TODO: move to Topological_Spaces.thy *)
   2.545    "(f \<longlongrightarrow> l) sequentially \<Longrightarrow> ((\<lambda>i. f(i - k)) \<longlongrightarrow> l) sequentially"
   2.546    apply (erule filterlim_compose)
   2.547 -  apply (simp add: filterlim_def le_sequentially eventually_filtermap eventually_sequentially)
   2.548 -  apply arith
   2.549 +  apply (simp add: filterlim_def le_sequentially eventually_filtermap eventually_sequentially, arith)
   2.550    done
   2.551  
   2.552  lemma seq_harmonic: "((\<lambda>n. inverse (real n)) \<longlongrightarrow> 0) sequentially"
   2.553 @@ -3803,8 +3786,7 @@
   2.554      assume "x\<in>S" "e>0" "cball x e \<subseteq> S"
   2.555      then have "\<exists>d>0. ball x d \<subseteq> S"
   2.556        unfolding subset_eq
   2.557 -      apply(rule_tac x="e/2" in exI)
   2.558 -      apply auto
   2.559 +      apply (rule_tac x="e/2" in exI, auto)
   2.560        done
   2.561    }
   2.562    ultimately show ?thesis
   2.563 @@ -3816,7 +3798,7 @@
   2.564  
   2.565  lemma mem_interior_cball: "x \<in> interior S \<longleftrightarrow> (\<exists>e>0. cball x e \<subseteq> S)"
   2.566    apply (simp add: interior_def, safe)
   2.567 -  apply (force simp add: open_contains_cball)
   2.568 +  apply (force simp: open_contains_cball)
   2.569    apply (rule_tac x="ball x e" in exI)
   2.570    apply (simp add: subset_trans [OF ball_subset_cball])
   2.571    done
   2.572 @@ -3866,18 +3848,18 @@
   2.573            also have "\<dots> = \<bar>- 1 + d / (2 * norm (x - y))\<bar> * norm (x - y)"
   2.574              using scaleR_left_distrib[of "- 1" "d / (2 * norm (y - x))", symmetric, of "y - x"]
   2.575              unfolding scaleR_minus_left scaleR_one
   2.576 -            by (auto simp add: norm_minus_commute)
   2.577 +            by (auto simp: norm_minus_commute)
   2.578            also have "\<dots> = \<bar>- norm (x - y) + d / 2\<bar>"
   2.579              unfolding abs_mult_pos[of "norm (x - y)", OF norm_ge_zero[of "x - y"]]
   2.580              unfolding distrib_right using \<open>x\<noteq>y\<close>  by auto
   2.581            also have "\<dots> \<le> e - d/2" using \<open>d \<le> dist x y\<close> and \<open>d>0\<close> and \<open>?rhs\<close>
   2.582 -            by (auto simp add: dist_norm)
   2.583 +            by (auto simp: dist_norm)
   2.584            finally have "y - (d / (2 * dist y x)) *\<^sub>R (y - x) \<in> ball x e" using \<open>d>0\<close>
   2.585              by auto
   2.586            moreover
   2.587            have "(d / (2*dist y x)) *\<^sub>R (y - x) \<noteq> 0"
   2.588              using \<open>x\<noteq>y\<close>[unfolded dist_nz] \<open>d>0\<close> unfolding scaleR_eq_0_iff
   2.589 -            by (auto simp add: dist_commute)
   2.590 +            by (auto simp: dist_commute)
   2.591            moreover
   2.592            have "dist (y - (d / (2 * dist y x)) *\<^sub>R (y - x)) y < d"
   2.593              unfolding dist_norm
   2.594 @@ -3905,14 +3887,13 @@
   2.595              unfolding \<open>x = y\<close>
   2.596              using \<open>z \<noteq> y\<close> **
   2.597              apply (rule_tac x=z in bexI)
   2.598 -            apply (auto simp add: dist_commute)
   2.599 +            apply (auto simp: dist_commute)
   2.600              done
   2.601          next
   2.602            case False
   2.603            then show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
   2.604              using \<open>d>0\<close> \<open>d > dist x y\<close> \<open>?rhs\<close>
   2.605 -            apply (rule_tac x=x in bexI)
   2.606 -            apply auto
   2.607 +            apply (rule_tac x=x in bexI, auto)
   2.608              done
   2.609          qed
   2.610        qed
   2.611 @@ -3971,8 +3952,7 @@
   2.612    apply (simp add: le_less [where 'a=real])
   2.613    apply (erule disjE)
   2.614    apply (rule subsetD [OF closure_subset], simp)
   2.615 -  apply (simp add: closure_def)
   2.616 -  apply clarify
   2.617 +  apply (simp add: closure_def, clarify)
   2.618    apply (rule closure_ball_lemma)
   2.619    apply (simp add: zero_less_dist_iff)
   2.620    done
   2.621 @@ -4010,7 +3990,7 @@
   2.622        using perfect_choose_dist [of d] by auto
   2.623      have "xa \<in> S"
   2.624        using d[THEN spec[where x = xa]]
   2.625 -      using xa by (auto simp add: dist_commute)
   2.626 +      using xa by (auto simp: dist_commute)
   2.627      then have xa_cball: "xa \<in> cball x e"
   2.628        using as(1) by auto
   2.629      then have "y \<in> ball x e"
   2.630 @@ -4031,15 +4011,15 @@
   2.631          unfolding zero_less_norm_iff[symmetric] using \<open>d>0\<close> by auto
   2.632        have "dist (y + (d / 2 / dist y x) *\<^sub>R (y - x)) x =
   2.633          norm (y + (d / (2 * norm (y - x))) *\<^sub>R y - (d / (2 * norm (y - x))) *\<^sub>R x - x)"
   2.634 -        by (auto simp add: dist_norm algebra_simps)
   2.635 +        by (auto simp: dist_norm algebra_simps)
   2.636        also have "\<dots> = norm ((1 + d / (2 * norm (y - x))) *\<^sub>R (y - x))"
   2.637 -        by (auto simp add: algebra_simps)
   2.638 +        by (auto simp: algebra_simps)
   2.639        also have "\<dots> = \<bar>1 + d / (2 * norm (y - x))\<bar> * norm (y - x)"
   2.640          using ** by auto
   2.641        also have "\<dots> = (dist y x) + d/2"
   2.642 -        using ** by (auto simp add: distrib_right dist_norm)
   2.643 +        using ** by (auto simp: distrib_right dist_norm)
   2.644        finally have "e \<ge> dist x y +d/2"
   2.645 -        using *[unfolded mem_cball] by (auto simp add: dist_commute)
   2.646 +        using *[unfolded mem_cball] by (auto simp: dist_commute)
   2.647        then show "y \<in> ball x e"
   2.648          unfolding mem_ball using \<open>d>0\<close> by auto
   2.649      qed
   2.650 @@ -4081,14 +4061,14 @@
   2.651    obtain a where "a \<noteq> x" "dist a x < e"
   2.652      using perfect_choose_dist [OF e] by auto
   2.653    then have "a \<noteq> x" "dist x a \<le> e"
   2.654 -    by (auto simp add: dist_commute)
   2.655 -  with e show ?thesis by (auto simp add: set_eq_iff)
   2.656 +    by (auto simp: dist_commute)
   2.657 +  with e show ?thesis by (auto simp: set_eq_iff)
   2.658  qed auto
   2.659  
   2.660  lemma cball_sing:
   2.661    fixes x :: "'a::metric_space"
   2.662    shows "e = 0 \<Longrightarrow> cball x e = {x}"
   2.663 -  by (auto simp add: set_eq_iff)
   2.664 +  by (auto simp: set_eq_iff)
   2.665  
   2.666  lemma ball_divide_subset: "d \<ge> 1 \<Longrightarrow> ball x (e/d) \<subseteq> ball x e"
   2.667    apply (cases "e \<le> 0")
   2.668 @@ -4179,15 +4159,14 @@
   2.669  lemma bounded_cball[simp,intro]: "bounded (cball x e)"
   2.670    apply (simp add: bounded_def)
   2.671    apply (rule_tac x=x in exI)
   2.672 -  apply (rule_tac x=e in exI)
   2.673 -  apply auto
   2.674 +  apply (rule_tac x=e in exI, auto)
   2.675    done
   2.676  
   2.677  lemma bounded_ball[simp,intro]: "bounded (ball x e)"
   2.678    by (metis ball_subset_cball bounded_cball bounded_subset)
   2.679  
   2.680  lemma bounded_Un[simp]: "bounded (S \<union> T) \<longleftrightarrow> bounded S \<and> bounded T"
   2.681 -  by (auto simp add: bounded_def) (metis Un_iff bounded_any_center le_max_iff_disj)
   2.682 +  by (auto simp: bounded_def) (metis Un_iff bounded_any_center le_max_iff_disj)
   2.683  
   2.684  lemma bounded_Union[intro]: "finite F \<Longrightarrow> \<forall>S\<in>F. bounded S \<Longrightarrow> bounded (\<Union>F)"
   2.685    by (induct rule: finite_induct[of F]) auto
   2.686 @@ -4249,7 +4228,7 @@
   2.687  
   2.688  lemma not_bounded_UNIV[simp]:
   2.689    "\<not> bounded (UNIV :: 'a::{real_normed_vector, perfect_space} set)"
   2.690 -proof (auto simp add: bounded_pos not_le)
   2.691 +proof (auto simp: bounded_pos not_le)
   2.692    obtain x :: 'a where "x \<noteq> 0"
   2.693      using perfect_choose_dist [OF zero_less_one] by fast
   2.694    fix b :: real
   2.695 @@ -4287,7 +4266,7 @@
   2.696    from assms(1) obtain b where b: "b > 0" "\<forall>x\<in>S. norm x \<le> b"
   2.697      unfolding bounded_pos by auto
   2.698    from assms(2) obtain B where B: "B > 0" "\<forall>x. norm (f x) \<le> B * norm x"
   2.699 -    using bounded_linear.pos_bounded by (auto simp add: ac_simps)
   2.700 +    using bounded_linear.pos_bounded by (auto simp: ac_simps)
   2.701    {
   2.702      fix x
   2.703      assume "x \<in> S"
   2.704 @@ -4302,14 +4281,13 @@
   2.705    then show ?thesis
   2.706      unfolding bounded_pos
   2.707      apply (rule_tac x="b*B" in exI)
   2.708 -    using b B by (auto simp add: mult.commute)
   2.709 +    using b B by (auto simp: mult.commute)
   2.710  qed
   2.711  
   2.712  lemma bounded_scaling:
   2.713    fixes S :: "'a::real_normed_vector set"
   2.714    shows "bounded S \<Longrightarrow> bounded ((\<lambda>x. c *\<^sub>R x) ` S)"
   2.715 -  apply (rule bounded_linear_image)
   2.716 -  apply assumption
   2.717 +  apply (rule bounded_linear_image, assumption)
   2.718    apply (rule bounded_linear_scaleR_right)
   2.719    done
   2.720  
   2.721 @@ -4347,7 +4325,7 @@
   2.722  lemma bounded_uminus [simp]:
   2.723    fixes X :: "'a::real_normed_vector set"
   2.724    shows "bounded (uminus ` X) \<longleftrightarrow> bounded X"
   2.725 -by (auto simp: bounded_def dist_norm; rule_tac x="-x" in exI; force simp add: add.commute norm_minus_commute)
   2.726 +by (auto simp: bounded_def dist_norm; rule_tac x="-x" in exI; force simp: add.commute norm_minus_commute)
   2.727  
   2.728  lemma uminus_bounded_comp [simp]:
   2.729    fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
   2.730 @@ -4374,7 +4352,7 @@
   2.731    "bounded (f ` S) \<Longrightarrow> bounded (g ` S) \<Longrightarrow> bounded ((\<lambda>x. f x - g x) ` S)"
   2.732    for f g::"'a \<Rightarrow> 'b::real_normed_vector"
   2.733    using bounded_plus_comp[of "f" S "\<lambda>x. - g x"]
   2.734 -  by (auto simp: )
   2.735 +  by auto
   2.736  
   2.737  
   2.738  subsection\<open>Some theorems on sups and infs using the notion "bounded".\<close>
   2.739 @@ -4898,7 +4876,7 @@
   2.740      with A(2)[THEN spec, of "X - {U}"] have "U \<inter> \<Inter>(X - {U}) \<noteq> {}"
   2.741        by auto
   2.742      with X show "(INF a:X. principal a) \<noteq> bot"
   2.743 -      by (auto simp add: INF_principal_finite principal_eq_bot_iff)
   2.744 +      by (auto simp: INF_principal_finite principal_eq_bot_iff)
   2.745    qed
   2.746    moreover
   2.747    have "F \<le> principal U"
   2.748 @@ -5133,7 +5111,7 @@
   2.749        moreover have "eventually (\<lambda>x. x \<in> A (Suc n)) (nhds x)"
   2.750          using A(1,2)[of "Suc n"] by (auto simp: eventually_nhds)
   2.751        ultimately have "eventually (\<lambda>x. False) ?F"
   2.752 -        by (auto simp add: eventually_inf)
   2.753 +        by (auto simp: eventually_inf)
   2.754        with x show False
   2.755          by (simp add: eventually_False)
   2.756      qed
   2.757 @@ -5583,7 +5561,7 @@
   2.758    obtain l1 r1 where r1: "strict_mono r1" and l1: "(\<lambda>n. fst (f (r1 n))) \<longlonglongrightarrow> l1"
   2.759      using bounded_imp_convergent_subsequence [OF s1] unfolding o_def by fast
   2.760    from f have s2: "bounded (range (snd \<circ> f \<circ> r1))"
   2.761 -    by (auto simp add: image_comp intro: bounded_snd bounded_subset)
   2.762 +    by (auto simp: image_comp intro: bounded_snd bounded_subset)
   2.763    obtain l2 r2 where r2: "strict_mono r2" and l2: "((\<lambda>n. snd (f (r1 (r2 n)))) \<longlongrightarrow> l2) sequentially"
   2.764      using bounded_imp_convergent_subsequence [OF s2]
   2.765      unfolding o_def by fast
   2.766 @@ -5674,7 +5652,7 @@
   2.767      done
   2.768  qed
   2.769  
   2.770 -text\<open>The Baire propery of dense sets\<close>
   2.771 +text\<open>The Baire property of dense sets\<close>
   2.772  theorem Baire:
   2.773    fixes S::"'a::{real_normed_vector,heine_borel} set"
   2.774    assumes "closed S" "countable \<G>"
   2.775 @@ -5693,14 +5671,14 @@
   2.776    proof (clarsimp simp: closure_approachable)
   2.777      fix x and e::real
   2.778      assume "x \<in> S" "0 < e"
   2.779 -    obtain TF where opeF: "\<And>n. openin (subtopology euclidean S) (TF n)" 
   2.780 -               and ne: "\<And>n. TF n \<noteq> {}" 
   2.781 +    obtain TF where opeF: "\<And>n. openin (subtopology euclidean S) (TF n)"
   2.782 +               and ne: "\<And>n. TF n \<noteq> {}"
   2.783                 and subg: "\<And>n. S \<inter> closure(TF n) \<subseteq> ?g n"
   2.784 -               and subball: "\<And>n. closure(TF n) \<subseteq> ball x e" 
   2.785 +               and subball: "\<And>n. closure(TF n) \<subseteq> ball x e"
   2.786                 and decr: "\<And>n. TF(Suc n) \<subseteq> TF n"
   2.787      proof -
   2.788        have *: "\<exists>Y. (openin (subtopology euclidean S) Y \<and> Y \<noteq> {} \<and>
   2.789 -                   S \<inter> closure Y \<subseteq> ?g n \<and> closure Y \<subseteq> ball x e) \<and> Y \<subseteq> U" 
   2.790 +                   S \<inter> closure Y \<subseteq> ?g n \<and> closure Y \<subseteq> ball x e) \<and> Y \<subseteq> U"
   2.791          if opeU: "openin (subtopology euclidean S) U" and "U \<noteq> {}" and cloU: "closure U \<subseteq> ball x e" for U n
   2.792        proof -
   2.793          obtain T where T: "open T" "U = T \<inter> S"
   2.794 @@ -5714,7 +5692,7 @@
   2.795          moreover have "openin (subtopology euclidean S) (U \<inter> ?g n)"
   2.796            using gin ope opeU by blast
   2.797          ultimately obtain d where U: "U \<inter> ?g n \<subseteq> S" and "d > 0" and d: "ball y d \<inter> S \<subseteq> U \<inter> ?g n"
   2.798 -          by (force simp add: openin_contains_ball)
   2.799 +          by (force simp: openin_contains_ball)
   2.800          show ?thesis
   2.801          proof (intro exI conjI)
   2.802            show "openin (subtopology euclidean S) (S \<inter> ball y (d/2))"
   2.803 @@ -5742,7 +5720,7 @@
   2.804              using ball_divide_subset_numeral d by blast
   2.805          qed
   2.806        qed
   2.807 -      let ?\<Phi> = "\<lambda>n X. openin (subtopology euclidean S) X \<and> X \<noteq> {} \<and> 
   2.808 +      let ?\<Phi> = "\<lambda>n X. openin (subtopology euclidean S) X \<and> X \<noteq> {} \<and>
   2.809                        S \<inter> closure X \<subseteq> ?g n \<and> closure X \<subseteq> ball x e"
   2.810        have "closure (S \<inter> ball x (e / 2)) \<subseteq> closure(ball x (e/2))"
   2.811          by (simp add: closure_mono)
   2.812 @@ -5765,7 +5743,7 @@
   2.813      proof (rule compact_nest)
   2.814        show "\<And>n. compact (S \<inter> closure (TF n))"
   2.815          by (metis closed_closure subball bounded_subset_ballI compact_eq_bounded_closed closed_Int_compact [OF \<open>closed S\<close>])
   2.816 -      show "\<And>n. S \<inter> closure (TF n) \<noteq> {}" 
   2.817 +      show "\<And>n. S \<inter> closure (TF n) \<noteq> {}"
   2.818          by (metis Int_absorb1 opeF \<open>closed S\<close> closure_eq_empty closure_minimal ne openin_imp_subset)
   2.819        show "\<And>m n. m \<le> n \<Longrightarrow> S \<inter> closure (TF n) \<subseteq> S \<inter> closure (TF m)"
   2.820          by (meson closure_mono decr dual_order.refl inf_mono lift_Suc_antimono_le)
   2.821 @@ -5815,8 +5793,7 @@
   2.822        from as(2) obtain N where N:"\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (f m) (f n) < e/2"
   2.823          unfolding cauchy_def
   2.824          using \<open>e > 0\<close>
   2.825 -        apply (erule_tac x="e/2" in allE)
   2.826 -        apply auto
   2.827 +        apply (erule_tac x="e/2" in allE, auto)
   2.828          done
   2.829        from lr(3)[unfolded lim_sequentially, THEN spec[where x="e/2"]]
   2.830        obtain M where M:"\<forall>n\<ge>M. dist ((f \<circ> r) n) l < e/2"
   2.831 @@ -5832,7 +5809,7 @@
   2.832            using N and n by auto
   2.833          ultimately have "dist (f n) l < e"
   2.834            using dist_triangle_half_r[of "f (r n)" "f n" e l]
   2.835 -          by (auto simp add: dist_commute)
   2.836 +          by (auto simp: dist_commute)
   2.837        }
   2.838        then have "\<exists>N. \<forall>n\<ge>N. dist (f n) l < e" by blast
   2.839      }
   2.840 @@ -5952,10 +5929,7 @@
   2.841    shows "bounded (range s)"
   2.842  proof -
   2.843    from assms obtain N :: nat where "\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (s m) (s n) < 1"
   2.844 -    unfolding cauchy_def
   2.845 -    apply (erule_tac x= 1 in allE)
   2.846 -    apply auto
   2.847 -    done
   2.848 +    unfolding cauchy_def by force
   2.849    then have N:"\<forall>n. N \<le> n \<longrightarrow> dist (s N) (s n) < 1" by auto
   2.850    moreover
   2.851    have "bounded (s ` {0..N})"
   2.852 @@ -5964,11 +5938,9 @@
   2.853      unfolding bounded_any_center [where a="s N"] by auto
   2.854    ultimately show "?thesis"
   2.855      unfolding bounded_any_center [where a="s N"]
   2.856 -    apply (rule_tac x="max a 1" in exI)
   2.857 -    apply auto
   2.858 +    apply (rule_tac x="max a 1" in exI, auto)
   2.859      apply (erule_tac x=y in allE)
   2.860 -    apply (erule_tac x=y in ballE)
   2.861 -    apply auto
   2.862 +    apply (erule_tac x=y in ballE, auto)
   2.863      done
   2.864  qed
   2.865  
   2.866 @@ -6114,7 +6086,7 @@
   2.867      shows "summable (\<lambda>n. of_real(norm(a n)) * w ^ n)"
   2.868  proof -
   2.869    obtain M where M: "\<And>x. norm (a x * z ^ x) \<le> M"
   2.870 -    using summable_imp_bounded [OF sum] by (force simp add: bounded_iff)
   2.871 +    using summable_imp_bounded [OF sum] by (force simp: bounded_iff)
   2.872    then have *: "summable (\<lambda>n. norm (a n) * norm w ^ n)"
   2.873      by (rule_tac M=M in Abel_lemma) (auto simp: norm_mult norm_power intro: no)
   2.874    show ?thesis
   2.875 @@ -6259,8 +6231,7 @@
   2.876    "continuous (at x within s) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. \<forall>x'\<in> s.  dist x' x < d --> dist (f x') (f x) < e)"
   2.877    unfolding continuous_within and Lim_within
   2.878    apply auto
   2.879 -  apply (metis dist_nz dist_self)
   2.880 -  apply blast
   2.881 +  apply (metis dist_nz dist_self, blast)
   2.882    done
   2.883  
   2.884  corollary continuous_at_eps_delta:
   2.885 @@ -6272,26 +6243,20 @@
   2.886    assumes nondecF: "\<And>x y. x \<le> y \<Longrightarrow> f x \<le> f y"
   2.887    shows "continuous (at_right a) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. f (a + d) - f a < e)"
   2.888    apply (simp add: greaterThan_def dist_real_def continuous_within Lim_within_le)
   2.889 -  apply (intro all_cong ex_cong)
   2.890 -  apply safe
   2.891 -  apply (erule_tac x="a + d" in allE)
   2.892 -  apply simp
   2.893 +  apply (intro all_cong ex_cong, safe)
   2.894 +  apply (erule_tac x="a + d" in allE, simp)
   2.895    apply (simp add: nondecF field_simps)
   2.896 -  apply (drule nondecF)
   2.897 -  apply simp
   2.898 +  apply (drule nondecF, simp)
   2.899    done
   2.900  
   2.901  lemma continuous_at_left_real_increasing:
   2.902    assumes nondecF: "\<And> x y. x \<le> y \<Longrightarrow> f x \<le> ((f y) :: real)"
   2.903    shows "(continuous (at_left (a :: real)) f) = (\<forall>e > 0. \<exists>delta > 0. f a - f (a - delta) < e)"
   2.904    apply (simp add: lessThan_def dist_real_def continuous_within Lim_within_le)
   2.905 -  apply (intro all_cong ex_cong)
   2.906 -  apply safe
   2.907 -  apply (erule_tac x="a - d" in allE)
   2.908 -  apply simp
   2.909 +  apply (intro all_cong ex_cong, safe)
   2.910 +  apply (erule_tac x="a - d" in allE, simp)
   2.911    apply (simp add: nondecF field_simps)
   2.912 -  apply (cut_tac x="a - d" and y="x" in nondecF)
   2.913 -  apply simp_all
   2.914 +  apply (cut_tac x="a - d" and y=x in nondecF, simp_all)
   2.915    done
   2.916  
   2.917  text\<open>Versions in terms of open balls.\<close>
   2.918 @@ -6312,25 +6277,23 @@
   2.919        assume "y \<in> f ` (ball x d \<inter> s)"
   2.920        then have "y \<in> ball (f x) e"
   2.921          using d(2)
   2.922 -        apply (auto simp add: dist_commute)
   2.923 -        apply (erule_tac x=xa in ballE)
   2.924 -        apply auto
   2.925 +        apply (auto simp: dist_commute)
   2.926 +        apply (erule_tac x=xa in ballE, auto)
   2.927          using \<open>e > 0\<close>
   2.928          apply auto
   2.929          done
   2.930      }
   2.931      then have "\<exists>d>0. f ` (ball x d \<inter> s) \<subseteq> ball (f x) e"
   2.932        using \<open>d > 0\<close>
   2.933 -      unfolding subset_eq ball_def by (auto simp add: dist_commute)
   2.934 +      unfolding subset_eq ball_def by (auto simp: dist_commute)
   2.935    }
   2.936    then show ?rhs by auto
   2.937  next
   2.938    assume ?rhs
   2.939    then show ?lhs
   2.940      unfolding continuous_within Lim_within ball_def subset_eq
   2.941 -    apply (auto simp add: dist_commute)
   2.942 -    apply (erule_tac x=e in allE)
   2.943 -    apply auto
   2.944 +    apply (auto simp: dist_commute)
   2.945 +    apply (erule_tac x=e in allE, auto)
   2.946      done
   2.947  qed
   2.948  
   2.949 @@ -6341,24 +6304,20 @@
   2.950    then show ?rhs
   2.951      unfolding continuous_at Lim_at subset_eq Ball_def Bex_def image_iff mem_ball
   2.952      apply auto
   2.953 -    apply (erule_tac x=e in allE)
   2.954 -    apply auto
   2.955 -    apply (rule_tac x=d in exI)
   2.956 -    apply auto
   2.957 +    apply (erule_tac x=e in allE, auto)
   2.958 +    apply (rule_tac x=d in exI, auto)
   2.959      apply (erule_tac x=xa in allE)
   2.960 -    apply (auto simp add: dist_commute)
   2.961 +    apply (auto simp: dist_commute)
   2.962      done
   2.963  next
   2.964    assume ?rhs
   2.965    then show ?lhs
   2.966      unfolding continuous_at Lim_at subset_eq Ball_def Bex_def image_iff mem_ball
   2.967      apply auto
   2.968 -    apply (erule_tac x=e in allE)
   2.969 -    apply auto
   2.970 -    apply (rule_tac x=d in exI)
   2.971 -    apply auto
   2.972 +    apply (erule_tac x=e in allE, auto)
   2.973 +    apply (rule_tac x=d in exI, auto)
   2.974      apply (erule_tac x="f xa" in allE)
   2.975 -    apply (auto simp add: dist_commute)
   2.976 +    apply (auto simp: dist_commute)
   2.977      done
   2.978  qed
   2.979  
   2.980 @@ -6528,7 +6487,7 @@
   2.981        "\<forall>x. 0 < x \<longrightarrow> fst (fa x) \<in> s \<and> snd (fa x) \<in> s \<and> dist (fst (fa x)) (snd (fa x)) < x \<and> \<not> dist (f (fst (fa x))) (f (snd (fa x))) < e"
   2.982        using choice[of "\<lambda>d x. d>0 \<longrightarrow> fst x \<in> s \<and> snd x \<in> s \<and> dist (snd x) (fst x) < d \<and> \<not> dist (f (snd x)) (f (fst x)) < e"]
   2.983        unfolding Bex_def
   2.984 -      by (auto simp add: dist_commute)
   2.985 +      by (auto simp: dist_commute)
   2.986      define x where "x n = fst (fa (inverse (real n + 1)))" for n
   2.987      define y where "y n = snd (fa (inverse (real n + 1)))" for n
   2.988      have xyn: "\<forall>n. x n \<in> s \<and> y n \<in> s"
   2.989 @@ -6579,7 +6538,7 @@
   2.990    shows "continuous (at x within s) g"
   2.991    using assms
   2.992    unfolding continuous_within
   2.993 -  by (force simp add: intro: Lim_transform_within)
   2.994 +  by (force intro: Lim_transform_within)
   2.995  
   2.996  
   2.997  subsubsection \<open>Structural rules for pointwise continuity\<close>
   2.998 @@ -6944,7 +6903,7 @@
   2.999      using image_closure_subset[OF assms(1) closed_cball[of 0 b] *] assms(3)
  2.1000      unfolding subset_eq
  2.1001      apply (erule_tac x="f x" in ballE)
  2.1002 -    apply (auto simp add: dist_norm)
  2.1003 +    apply (auto simp: dist_norm)
  2.1004      done
  2.1005  qed
  2.1006  
  2.1007 @@ -7505,8 +7464,7 @@
  2.1008          by auto
  2.1009      }
  2.1010      ultimately have "\<exists>e>0. \<forall>x'. dist x' (c *\<^sub>R x) < e \<longrightarrow> x' \<in> op *\<^sub>R c ` s"
  2.1011 -      apply (rule_tac x="e * \<bar>c\<bar>" in exI)
  2.1012 -      apply auto
  2.1013 +      apply (rule_tac x="e * \<bar>c\<bar>" in exI, auto)
  2.1014        done
  2.1015    }
  2.1016    then show ?thesis unfolding open_dist by auto
  2.1017 @@ -7563,7 +7521,7 @@
  2.1018      unfolding mem_interior by auto
  2.1019    then have "ball (x - a) e \<subseteq> S"
  2.1020      unfolding subset_eq Ball_def mem_ball dist_norm
  2.1021 -    by (auto simp add: diff_diff_eq)
  2.1022 +    by (auto simp: diff_diff_eq)
  2.1023    then show "x \<in> op + a ` interior S"
  2.1024      unfolding image_iff
  2.1025      apply (rule_tac x="x - a" in bexI)
  2.1026 @@ -7654,12 +7612,12 @@
  2.1027          have "dist (x + (\<Sum>i\<in>Basis. (u \<bullet> i) *\<^sub>R inv f i)) x \<le> (\<Sum>i\<in>Basis. norm ((u \<bullet> i) *\<^sub>R inv f i))"
  2.1028            by (simp add: dist_norm sum_norm_le)
  2.1029          also have "... = (\<Sum>i\<in>Basis. \<bar>u \<bullet> i\<bar> * norm (inv f i))"
  2.1030 -          by (simp add: )
  2.1031 +          by simp
  2.1032          also have "... \<le> (\<Sum>i\<in>Basis. \<bar>u \<bullet> i\<bar>) * B"
  2.1033            by (simp add: B sum_distrib_right sum_mono mult_left_mono)
  2.1034          also have "... \<le> DIM('b) * dist y (f x) * B"
  2.1035            apply (rule mult_right_mono [OF sum_bounded_above])
  2.1036 -          using \<open>0 < B\<close> by (auto simp add: Basis_le_norm dist_norm u_def)
  2.1037 +          using \<open>0 < B\<close> by (auto simp: Basis_le_norm dist_norm u_def)
  2.1038          also have "... < e"
  2.1039            by (metis mult.commute mult.left_commute that)
  2.1040          finally show "x + (\<Sum>i\<in>Basis. (u \<bullet> i) *\<^sub>R inv f i) \<in> A"
  2.1041 @@ -7679,7 +7637,7 @@
  2.1042  proof
  2.1043    assume "open(f ` A)"
  2.1044    then have "open(f -` (f ` A))"
  2.1045 -    using assms by (force simp add: linear_continuous_at linear_conv_bounded_linear continuous_open_vimage)
  2.1046 +    using assms by (force simp: linear_continuous_at linear_conv_bounded_linear continuous_open_vimage)
  2.1047    then show "open A"
  2.1048      by (simp add: assms bij_is_inj inj_vimage_image_eq)
  2.1049  next
  2.1050 @@ -7705,7 +7663,7 @@
  2.1051    then show "f x \<in> interior (f ` S)"
  2.1052      by (meson assms imageI image_mono interiorI interior_subset open_bijective_linear_image_eq open_interior)
  2.1053  qed
  2.1054 -  
  2.1055 +
  2.1056  lemma interior_injective_linear_image:
  2.1057    fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
  2.1058    assumes "linear f" "inj f"
  2.1059 @@ -7778,8 +7736,7 @@
  2.1060        from \<open>finite D\<close> show "finite ?D"
  2.1061          by (rule finite_imageI)
  2.1062        from \<open>S \<subseteq> \<Union>D\<close> show "S \<subseteq> \<Union>?D"
  2.1063 -        apply (rule subset_trans)
  2.1064 -        apply clarsimp
  2.1065 +        apply (rule subset_trans, clarsimp)
  2.1066          apply (frule subsetD [OF \<open>D \<subseteq> ?C\<close>, THEN f_inv_into_f])
  2.1067          apply (erule rev_bexI, fast)
  2.1068          done
  2.1069 @@ -7935,14 +7892,10 @@
  2.1070    unfolding Lim_at
  2.1071    unfolding dist_norm
  2.1072    apply auto
  2.1073 -  apply (erule_tac x=e in allE)
  2.1074 -  apply auto
  2.1075 -  apply (rule_tac x=d in exI)
  2.1076 -  apply auto
  2.1077 -  apply (erule_tac x=x' in allE)
  2.1078 -  apply auto
  2.1079 -  apply (erule_tac x=e in allE)
  2.1080 -  apply auto
  2.1081 +  apply (erule_tac x=e in allE, auto)
  2.1082 +  apply (rule_tac x=d in exI, auto)
  2.1083 +  apply (erule_tac x=x' in allE, auto)
  2.1084 +  apply (erule_tac x=e in allE, auto)
  2.1085    done
  2.1086  
  2.1087  lemma continuous_on_real_range:
  2.1088 @@ -7997,7 +7950,7 @@
  2.1089    obtain x y a b where "\<forall>z\<in>s. dist x z \<le> a" "\<forall>z\<in>t. dist y z \<le> b"
  2.1090      using assms [unfolded bounded_def] by auto
  2.1091    then have "\<forall>z\<in>s \<times> t. dist (x, y) z \<le> sqrt (a\<^sup>2 + b\<^sup>2)"
  2.1092 -    by (auto simp add: dist_Pair_Pair real_sqrt_le_mono add_mono power_mono)
  2.1093 +    by (auto simp: dist_Pair_Pair real_sqrt_le_mono add_mono power_mono)
  2.1094    then show ?thesis unfolding bounded_any_center [where a="(x, y)"] by auto
  2.1095  qed
  2.1096  
  2.1097 @@ -8065,7 +8018,7 @@
  2.1098      finally have "s \<times> t \<subseteq> (\<Union>x\<in>e. \<Union>d x)" .
  2.1099    }
  2.1100    ultimately show "\<exists>C'\<subseteq>C. finite C' \<and> s \<times> t \<subseteq> \<Union>C'"
  2.1101 -    by (intro exI[of _ "(\<Union>x\<in>e. d x)"]) (auto simp add: subset_eq)
  2.1102 +    by (intro exI[of _ "(\<Union>x\<in>e. d x)"]) (auto simp: subset_eq)
  2.1103  qed
  2.1104  
  2.1105  text\<open>Hence some useful properties follow quite easily.\<close>
  2.1106 @@ -8115,8 +8068,7 @@
  2.1107  proof-
  2.1108    have "{x - y | x y. x\<in>s \<and> y \<in> t} =  {x + y | x y. x \<in> s \<and> y \<in> (uminus ` t)}"
  2.1109      apply auto
  2.1110 -    apply (rule_tac x= xa in exI)
  2.1111 -    apply auto
  2.1112 +    apply (rule_tac x= xa in exI, auto)
  2.1113      done
  2.1114    then show ?thesis
  2.1115      using compact_sums[OF assms(1) compact_negations[OF assms(2)]] by auto
  2.1116 @@ -8199,7 +8151,7 @@
  2.1117    ultimately have "dist x y \<le> (SUP (x,y):s\<times>s. dist x y)"
  2.1118      by (rule cSUP_upper2) simp
  2.1119    with \<open>x \<in> s\<close> show ?thesis
  2.1120 -    by (auto simp add: diameter_def)
  2.1121 +    by (auto simp: diameter_def)
  2.1122  qed
  2.1123  
  2.1124  lemma diameter_lower_bounded:
  2.1125 @@ -8210,7 +8162,7 @@
  2.1126  proof (rule ccontr)
  2.1127    assume contr: "\<not> ?thesis"
  2.1128    moreover have "s \<noteq> {}"
  2.1129 -    using d by (auto simp add: diameter_def)
  2.1130 +    using d by (auto simp: diameter_def)
  2.1131    ultimately have "diameter s \<le> d"
  2.1132      by (auto simp: not_less diameter_def intro!: cSUP_least)
  2.1133    with \<open>d < diameter s\<close> show False by auto
  2.1134 @@ -8236,8 +8188,7 @@
  2.1135    then have "diameter s \<le> dist x y"
  2.1136      unfolding diameter_def
  2.1137      apply clarsimp
  2.1138 -    apply (rule cSUP_least)
  2.1139 -    apply fast+
  2.1140 +    apply (rule cSUP_least, fast+)
  2.1141      done
  2.1142    then show ?thesis
  2.1143      by (metis b diameter_bounded_bound order_antisym xys)
  2.1144 @@ -8424,7 +8375,7 @@
  2.1145    shows "closed ((\<lambda>x. c *\<^sub>R x) ` S)"
  2.1146  proof (cases "c = 0")
  2.1147    case True then show ?thesis
  2.1148 -    by (auto simp add: image_constant_conv)
  2.1149 +    by (auto simp: image_constant_conv)
  2.1150  next
  2.1151    case False
  2.1152    from assms have "closed ((\<lambda>x. inverse c *\<^sub>R x) -` S)"
  2.1153 @@ -8467,8 +8418,7 @@
  2.1154        using \<open>l' \<in> S\<close>
  2.1155        apply auto
  2.1156        apply (rule_tac x=l' in exI)
  2.1157 -      apply (rule_tac x="l - l'" in exI)
  2.1158 -      apply auto
  2.1159 +      apply (rule_tac x="l - l'" in exI, auto)
  2.1160        done
  2.1161    }
  2.1162    moreover have "?S = (\<Union>x\<in> S. \<Union>y \<in> T. {x + y})"
  2.1163 @@ -8524,17 +8474,15 @@
  2.1164  lemma translation_Compl:
  2.1165    fixes a :: "'a::ab_group_add"
  2.1166    shows "(\<lambda>x. a + x) ` (- t) = - ((\<lambda>x. a + x) ` t)"
  2.1167 -  apply (auto simp add: image_iff)
  2.1168 -  apply (rule_tac x="x - a" in bexI)
  2.1169 -  apply auto
  2.1170 +  apply (auto simp: image_iff)
  2.1171 +  apply (rule_tac x="x - a" in bexI, auto)
  2.1172    done
  2.1173  
  2.1174  lemma translation_UNIV:
  2.1175    fixes a :: "'a::ab_group_add"
  2.1176    shows "range (\<lambda>x. a + x) = UNIV"
  2.1177 -  apply (auto simp add: image_iff)
  2.1178 -  apply (rule_tac x="x - a" in exI)
  2.1179 -  apply auto
  2.1180 +  apply (auto simp: image_iff)
  2.1181 +  apply (rule_tac x="x - a" in exI, auto)
  2.1182    done
  2.1183  
  2.1184  lemma translation_diff:
  2.1185 @@ -8554,8 +8502,7 @@
  2.1186    have *: "op + a ` (- s) = - op + a ` s"
  2.1187      apply auto
  2.1188      unfolding image_iff
  2.1189 -    apply (rule_tac x="x - a" in bexI)
  2.1190 -    apply auto
  2.1191 +    apply (rule_tac x="x - a" in bexI, auto)
  2.1192      done
  2.1193    show ?thesis
  2.1194      unfolding closure_interior translation_Compl
  2.1195 @@ -8644,10 +8591,9 @@
  2.1196    show ?thesis
  2.1197      using separate_compact_closed[OF assms(2,1) *]
  2.1198      apply auto
  2.1199 -    apply (rule_tac x=d in exI)
  2.1200 -    apply auto
  2.1201 +    apply (rule_tac x=d in exI, auto)
  2.1202      apply (erule_tac x=y in ballE)
  2.1203 -    apply (auto simp add: dist_commute)
  2.1204 +    apply (auto simp: dist_commute)
  2.1205      done
  2.1206  qed
  2.1207  
  2.1208 @@ -8788,7 +8734,7 @@
  2.1209   "(f \<longlongrightarrow> l) (at x within (s \<union> t)) \<longleftrightarrow>
  2.1210    (f \<longlongrightarrow> l) (at x within s) \<and> (f \<longlongrightarrow> l) (at x within t)"
  2.1211    unfolding tendsto_def
  2.1212 -  by (auto simp add: eventually_within_Un)
  2.1213 +  by (auto simp: eventually_within_Un)
  2.1214  
  2.1215  lemma Lim_topological:
  2.1216    "(f \<longlongrightarrow> l) net \<longleftrightarrow>
  2.1217 @@ -8885,7 +8831,7 @@
  2.1218    have "open (\<Inter>i\<in>Basis. (op \<bullet> i) -` {a \<bullet> i <..< b \<bullet> i})"
  2.1219      by (auto intro!: continuous_open_vimage continuous_inner continuous_ident continuous_const)
  2.1220    also have "(\<Inter>i\<in>Basis. (op \<bullet> i) -` {a \<bullet> i <..< b \<bullet> i}) = box a b"
  2.1221 -    by (auto simp add: box_def inner_commute)
  2.1222 +    by (auto simp: box_def inner_commute)
  2.1223    finally show ?thesis .
  2.1224  qed
  2.1225  
  2.1226 @@ -8907,7 +8853,7 @@
  2.1227      show "\<exists>B'\<subseteq>B. \<Union>B' = A"
  2.1228        apply (rule exI[of _ "{b\<in>B. b \<subseteq> A}"])
  2.1229        apply (subst (3) open_UNION_box[OF \<open>open A\<close>])
  2.1230 -      apply (auto simp add: a b B_def)
  2.1231 +      apply (auto simp: a b B_def)
  2.1232        done
  2.1233    qed
  2.1234    ultimately
  2.1235 @@ -8931,7 +8877,7 @@
  2.1236      by (intro closed_INT ballI continuous_closed_vimage allI
  2.1237        linear_continuous_at closed_real_atLeastAtMost finite_Basis bounded_linear_inner_left)
  2.1238    also have "(\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i .. b\<bullet>i}) = cbox a b"
  2.1239 -    by (auto simp add: cbox_def)
  2.1240 +    by (auto simp: cbox_def)
  2.1241    finally show "closed (cbox a b)" .
  2.1242  qed
  2.1243  
  2.1244 @@ -8991,8 +8937,7 @@
  2.1245      }
  2.1246      then have "(\<Sum>i\<in>Basis. \<bar>x \<bullet> i\<bar>) \<le> ?b"
  2.1247        apply -
  2.1248 -      apply (rule sum_mono)
  2.1249 -      apply auto
  2.1250 +      apply (rule sum_mono, auto)
  2.1251        done
  2.1252      then have "norm x \<le> ?b"
  2.1253        using norm_le_l1[of x] by auto
  2.1254 @@ -9168,7 +9113,7 @@
  2.1255          unfolding inverse_le_1_iff by auto
  2.1256        have "(inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b)) + (1 - inverse (real n + 1)) *\<^sub>R x =
  2.1257          x + (inverse (real n + 1)) *\<^sub>R (((1 / 2) *\<^sub>R (a + b)) - x)"
  2.1258 -        by (auto simp add: algebra_simps)
  2.1259 +        by (auto simp: algebra_simps)
  2.1260        then have "f n <e b" and "a <e f n"
  2.1261          using open_cbox_convex[OF box_midpoint[OF assms] as *]
  2.1262          unfolding f_def by (auto simp: box_def eucl_less_def)
  2.1263 @@ -9183,7 +9128,7 @@
  2.1264          assume "e > 0"
  2.1265          then have "\<exists>N::nat. inverse (real (N + 1)) < e"
  2.1266            using real_arch_inverse[of e]
  2.1267 -          apply (auto simp add: Suc_pred')
  2.1268 +          apply (auto simp: Suc_pred')
  2.1269            apply (metis Suc_pred' of_nat_Suc)
  2.1270            done
  2.1271          then obtain N :: nat where N: "inverse (real (N + 1)) < e"
  2.1272 @@ -9193,7 +9138,7 @@
  2.1273          then have "\<exists>N::nat. \<forall>n\<ge>N. inverse (real n + 1) < e" by auto
  2.1274        }
  2.1275        then have "((\<lambda>n. inverse (real n + 1)) \<longlongrightarrow> 0) sequentially"
  2.1276 -        unfolding lim_sequentially by(auto simp add: dist_norm)
  2.1277 +        unfolding lim_sequentially by(auto simp: dist_norm)
  2.1278        then have "(f \<longlongrightarrow> x) sequentially"
  2.1279          unfolding f_def
  2.1280          using tendsto_add[OF tendsto_const, of "\<lambda>n::nat. (inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b) - x)" 0 sequentially x]
  2.1281 @@ -9283,7 +9228,7 @@
  2.1282  lemma diameter_cbox:
  2.1283    fixes a b::"'a::euclidean_space"
  2.1284    shows "(\<forall>i \<in> Basis. a \<bullet> i \<le> b \<bullet> i) \<Longrightarrow> diameter (cbox a b) = dist a b"
  2.1285 -  by (force simp add: diameter_def intro!: cSup_eq_maximum setL2_mono
  2.1286 +  by (force simp: diameter_def intro!: cSup_eq_maximum setL2_mono
  2.1287       simp: euclidean_dist_l2[where 'a='a] cbox_def dist_norm)
  2.1288  
  2.1289  lemma eucl_less_eq_halfspaces:
  2.1290 @@ -9329,7 +9274,7 @@
  2.1291        done
  2.1292    }
  2.1293    moreover have "c \<in> cbox (m *\<^sub>R a + c) (m *\<^sub>R b + c)"
  2.1294 -    unfolding True by (auto simp add: cbox_sing)
  2.1295 +    unfolding True by (auto simp: cbox_sing)
  2.1296    ultimately show ?thesis using True by (auto simp: cbox_def)
  2.1297  next
  2.1298    case False
  2.1299 @@ -9344,7 +9289,7 @@
  2.1300      fix y
  2.1301      assume "\<forall>i\<in>Basis. a \<bullet> i \<le> y \<bullet> i" "\<forall>i\<in>Basis. y \<bullet> i \<le> b \<bullet> i" "m < 0"
  2.1302      then have "\<forall>i\<in>Basis. (m *\<^sub>R b + c) \<bullet> i \<le> (m *\<^sub>R y + c) \<bullet> i" and "\<forall>i\<in>Basis. (m *\<^sub>R y + c) \<bullet> i \<le> (m *\<^sub>R a + c) \<bullet> i"
  2.1303 -      by (auto simp add: mult_left_mono_neg inner_distrib)
  2.1304 +      by (auto simp: mult_left_mono_neg inner_distrib)
  2.1305    }
  2.1306    moreover
  2.1307    {
  2.1308 @@ -9353,7 +9298,7 @@
  2.1309      then have "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` cbox a b"
  2.1310        unfolding image_iff Bex_def mem_box
  2.1311        apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
  2.1312 -      apply (auto simp add: pos_le_divide_eq pos_divide_le_eq mult.commute inner_distrib inner_diff_left)
  2.1313 +      apply (auto simp: pos_le_divide_eq pos_divide_le_eq mult.commute inner_distrib inner_diff_left)
  2.1314        done
  2.1315    }
  2.1316    moreover
  2.1317 @@ -9363,7 +9308,7 @@
  2.1318      then have "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` cbox a b"
  2.1319        unfolding image_iff Bex_def mem_box
  2.1320        apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
  2.1321 -      apply (auto simp add: neg_le_divide_eq neg_divide_le_eq mult.commute inner_distrib inner_diff_left)
  2.1322 +      apply (auto simp: neg_le_divide_eq neg_divide_le_eq mult.commute inner_distrib inner_diff_left)
  2.1323        done
  2.1324    }
  2.1325    ultimately show ?thesis using False by (auto simp: cbox_def)
  2.1326 @@ -9442,7 +9387,7 @@
  2.1327  proof -
  2.1328    from assms have "{a ..< b} = {a} \<union> {a <..< b}" by auto
  2.1329    also have "closure \<dots> = {a .. b}" unfolding closure_Un
  2.1330 -    by (auto simp add: assms less_imp_le)
  2.1331 +    by (auto simp: assms less_imp_le)
  2.1332    finally show ?thesis .
  2.1333  qed
  2.1334  
  2.1335 @@ -9453,7 +9398,7 @@
  2.1336  proof -
  2.1337    from assms have "{a <.. b} = {b} \<union> {a <..< b}" by auto
  2.1338    also have "closure \<dots> = {a .. b}" unfolding closure_Un
  2.1339 -    by (auto simp add: assms less_imp_le)
  2.1340 +    by (auto simp: assms less_imp_le)
  2.1341    finally show ?thesis .
  2.1342  qed
  2.1343  
  2.1344 @@ -9497,7 +9442,7 @@
  2.1345  
  2.1346  lemma homeomorphic_empty [iff]:
  2.1347       "S homeomorphic {} \<longleftrightarrow> S = {}" "{} homeomorphic S \<longleftrightarrow> S = {}"
  2.1348 -  by (auto simp add: homeomorphic_def homeomorphism_def)
  2.1349 +  by (auto simp: homeomorphic_def homeomorphism_def)
  2.1350  
  2.1351  lemma homeomorphic_refl: "s homeomorphic s"
  2.1352    unfolding homeomorphic_def homeomorphism_def
  2.1353 @@ -9591,10 +9536,10 @@
  2.1354  next
  2.1355    assume R: ?rhs
  2.1356    with finite_same_card_bij obtain h where "bij_betw h S T"
  2.1357 -    by (auto simp: )
  2.1358 +    by auto
  2.1359    with R show ?lhs
  2.1360      apply (auto simp: homeomorphic_def homeomorphism_def continuous_on_finite)
  2.1361 -    apply (rule_tac x="h" in exI)
  2.1362 +    apply (rule_tac x=h in exI)
  2.1363      apply (rule_tac x="inv_into S h" in exI)
  2.1364      apply (auto simp:  bij_betw_inv_into_left bij_betw_inv_into_right bij_betw_imp_surj_on inv_into_into bij_betwE)
  2.1365      apply (metis bij_betw_def bij_betw_inv_into)
  2.1366 @@ -9672,7 +9617,7 @@
  2.1367    apply (rule_tac x="\<lambda>x. c *\<^sub>R x" in exI)
  2.1368    apply (rule_tac x="\<lambda>x. (1 / c) *\<^sub>R x" in exI)
  2.1369    using assms
  2.1370 -  apply (auto simp add: continuous_intros)
  2.1371 +  apply (auto simp: continuous_intros)
  2.1372    done
  2.1373  
  2.1374  lemma homeomorphic_translation:
  2.1375 @@ -9874,7 +9819,7 @@
  2.1376      then have x: "\<forall>n. x n \<in> s" "\<forall>n. g n = f (x n)" by auto
  2.1377      then have "f \<circ> x = g" by (simp add: fun_eq_iff)
  2.1378      then obtain l where "l\<in>s" and l:"(x \<longlongrightarrow> l) sequentially"
  2.1379 -      using cs[unfolded complete_def, THEN spec[where x="x"]]
  2.1380 +      using cs[unfolded complete_def, THEN spec[where x=x]]
  2.1381        using cauchy_isometric[OF \<open>0 < e\<close> s f normf] and cfg and x(1)
  2.1382        by auto
  2.1383      then show ?thesis
  2.1384 @@ -10190,7 +10135,7 @@
  2.1385          using mult_right_mono[OF * order_less_imp_le[OF **]]
  2.1386          by (simp add: mult.assoc)
  2.1387        also have "\<dots> < (e * (1 - c) / d) * d * (1 - c ^ (m - n)) / (1 - c)"
  2.1388 -        using mult_strict_right_mono[OF N **] by (auto simp add: mult.assoc)
  2.1389 +        using mult_strict_right_mono[OF N **] by (auto simp: mult.assoc)
  2.1390        also from c \<open>d > 0\<close> \<open>1 - c > 0\<close> have "\<dots> = e * (1 - c ^ (m - n))"
  2.1391          by simp
  2.1392        also from c \<open>1 - c ^ (m - n) > 0\<close> \<open>e > 0\<close> have "\<dots> \<le> e"
  2.1393 @@ -10204,7 +10149,7 @@
  2.1394      next
  2.1395        case False
  2.1396        with *[of n m] *[of m n] and that show ?thesis
  2.1397 -        by (auto simp add: dist_commute nat_neq_iff)
  2.1398 +        by (auto simp: dist_commute nat_neq_iff)
  2.1399      qed
  2.1400      then show ?thesis by auto
  2.1401    qed
  2.1402 @@ -10313,8 +10258,8 @@
  2.1403      proof (cases "a = a'")
  2.1404        case True
  2.1405        then show ?thesis
  2.1406 -        using subsetD [where c = "a + r *\<^sub>R (SOME i. i \<in> Basis)", OF \<open>?lhs\<close>] subsetD [where c = "a", OF \<open>?lhs\<close>]
  2.1407 -        by (force simp add: SOME_Basis dist_norm)
  2.1408 +        using subsetD [where c = "a + r *\<^sub>R (SOME i. i \<in> Basis)", OF \<open>?lhs\<close>] subsetD [where c = a, OF \<open>?lhs\<close>]
  2.1409 +        by (force simp: SOME_Basis dist_norm)
  2.1410      next
  2.1411        case False
  2.1412        have "norm (a' - (a + (r / norm (a - a')) *\<^sub>R (a - a'))) = norm (a' - a - (r / norm (a - a')) *\<^sub>R (a - a'))"
  2.1413 @@ -10355,8 +10300,8 @@
  2.1414      proof (cases "a = a'")
  2.1415        case True
  2.1416        then show ?thesis
  2.1417 -        using subsetD [where c = "a + r *\<^sub>R (SOME i. i \<in> Basis)", OF \<open>?lhs\<close>] subsetD [where c = "a", OF \<open>?lhs\<close>]
  2.1418 -        by (force simp add: SOME_Basis dist_norm)
  2.1419 +        using subsetD [where c = "a + r *\<^sub>R (SOME i. i \<in> Basis)", OF \<open>?lhs\<close>] subsetD [where c = a, OF \<open>?lhs\<close>]
  2.1420 +        by (force simp: SOME_Basis dist_norm)
  2.1421      next
  2.1422        case False
  2.1423        have False if "norm (a - a') + r \<ge> r'"
  2.1424 @@ -10444,14 +10389,14 @@
  2.1425    next
  2.1426      case False
  2.1427      with \<open>?lhs\<close> show ?rhs
  2.1428 -      apply (auto simp add: set_eq_subset ball_subset_ball_iff dist_norm norm_minus_commute algebra_simps)
  2.1429 +      apply (auto simp: set_eq_subset ball_subset_ball_iff dist_norm norm_minus_commute algebra_simps)
  2.1430        apply (metis add_le_same_cancel1 le_add_same_cancel1 norm_ge_zero norm_pths(2) order_trans)
  2.1431        apply (metis add_increasing2 add_le_imp_le_right eq_iff norm_ge_zero)
  2.1432        done
  2.1433    qed
  2.1434  next
  2.1435    assume ?rhs then show ?lhs
  2.1436 -    by (auto simp add: set_eq_subset ball_subset_ball_iff)
  2.1437 +    by (auto simp: set_eq_subset ball_subset_ball_iff)
  2.1438  qed
  2.1439  
  2.1440  lemma cball_eq_cball_iff:
  2.1441 @@ -10468,14 +10413,14 @@
  2.1442    next
  2.1443      case False
  2.1444      with \<open>?lhs\<close> show ?rhs
  2.1445 -      apply (auto simp add: set_eq_subset cball_subset_cball_iff dist_norm norm_minus_commute algebra_simps)
  2.1446 +      apply (auto simp: set_eq_subset cball_subset_cball_iff dist_norm norm_minus_commute algebra_simps)
  2.1447        apply (metis add_le_same_cancel1 le_add_same_cancel1 norm_ge_zero norm_pths(2) order_trans)
  2.1448        apply (metis add_increasing2 add_le_imp_le_right eq_iff norm_ge_zero)
  2.1449        done
  2.1450    qed
  2.1451  next
  2.1452    assume ?rhs then show ?lhs
  2.1453 -    by (auto simp add: set_eq_subset cball_subset_cball_iff)
  2.1454 +    by (auto simp: set_eq_subset cball_subset_cball_iff)
  2.1455  qed
  2.1456  
  2.1457  lemma ball_eq_cball_iff:
  2.1458 @@ -10484,7 +10429,7 @@
  2.1459  proof
  2.1460    assume ?lhs
  2.1461    then show ?rhs
  2.1462 -    apply (auto simp add: set_eq_subset ball_subset_cball_iff cball_subset_ball_iff algebra_simps)
  2.1463 +    apply (auto simp: set_eq_subset ball_subset_cball_iff cball_subset_ball_iff algebra_simps)
  2.1464      apply (metis add_increasing2 add_le_cancel_right add_less_same_cancel1 dist_not_less_zero less_le_trans zero_le_dist)
  2.1465      apply (metis add_less_same_cancel1 dist_not_less_zero less_le_trans not_le)
  2.1466      using \<open>?lhs\<close> ball_eq_empty cball_eq_empty apply blast+
  2.1467 @@ -11333,7 +11278,7 @@
  2.1468  proof cases
  2.1469    assume le: "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
  2.1470    from bounded obtain c where f_bound: "\<forall>x\<in>f ` cbox a b. dist undefined x \<le> c"
  2.1471 -    by (auto simp add: bounded_any_center[where a=undefined])
  2.1472 +    by (auto simp: bounded_any_center[where a=undefined])
  2.1473    then show ?thesis
  2.1474      by (auto intro!: exI[where x=c] clamp_in_interval[OF le[rule_format]]
  2.1475          simp: bounded_any_center[where a=undefined])