src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 53255 addd7b9b2bff
parent 53015 a1119cf551e8
child 53282 9d6e263fa921
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 28 23:48:45 2013 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Aug 29 00:18:02 2013 +0200
     1.3 @@ -49,6 +49,7 @@
     1.4      continuous_on (s \<union> t) (\<lambda>x. if P x then f x else g x)"
     1.5    by (rule continuous_on_If) auto
     1.6  
     1.7 +
     1.8  subsection {* Topological Basis *}
     1.9  
    1.10  context topological_space
    1.11 @@ -117,41 +118,51 @@
    1.12    by (simp add: topological_basis_def)
    1.13  
    1.14  lemma topological_basis_imp_subbasis:
    1.15 -  assumes B: "topological_basis B" shows "open = generate_topology B"
    1.16 +  assumes B: "topological_basis B"
    1.17 +  shows "open = generate_topology B"
    1.18  proof (intro ext iffI)
    1.19 -  fix S :: "'a set" assume "open S"
    1.20 +  fix S :: "'a set"
    1.21 +  assume "open S"
    1.22    with B obtain B' where "B' \<subseteq> B" "S = \<Union>B'"
    1.23      unfolding topological_basis_def by blast
    1.24    then show "generate_topology B S"
    1.25      by (auto intro: generate_topology.intros dest: topological_basis_open)
    1.26  next
    1.27 -  fix S :: "'a set" assume "generate_topology B S" then show "open S"
    1.28 +  fix S :: "'a set"
    1.29 +  assume "generate_topology B S"
    1.30 +  then show "open S"
    1.31      by induct (auto dest: topological_basis_open[OF B])
    1.32  qed
    1.33  
    1.34  lemma basis_dense:
    1.35 -  fixes B::"'a set set" and f::"'a set \<Rightarrow> 'a"
    1.36 +  fixes B::"'a set set"
    1.37 +    and f::"'a set \<Rightarrow> 'a"
    1.38    assumes "topological_basis B"
    1.39 -  assumes choosefrom_basis: "\<And>B'. B' \<noteq> {} \<Longrightarrow> f B' \<in> B'"
    1.40 +    and choosefrom_basis: "\<And>B'. B' \<noteq> {} \<Longrightarrow> f B' \<in> B'"
    1.41    shows "(\<forall>X. open X \<longrightarrow> X \<noteq> {} \<longrightarrow> (\<exists>B' \<in> B. f B' \<in> X))"
    1.42  proof (intro allI impI)
    1.43 -  fix X::"'a set" assume "open X" "X \<noteq> {}"
    1.44 +  fix X::"'a set"
    1.45 +  assume "open X" "X \<noteq> {}"
    1.46    from topological_basisE[OF `topological_basis B` `open X` choosefrom_basis[OF `X \<noteq> {}`]]
    1.47    guess B' . note B' = this
    1.48 -  thus "\<exists>B'\<in>B. f B' \<in> X" by (auto intro!: choosefrom_basis)
    1.49 +  then show "\<exists>B'\<in>B. f B' \<in> X"
    1.50 +    by (auto intro!: choosefrom_basis)
    1.51  qed
    1.52  
    1.53  end
    1.54  
    1.55  lemma topological_basis_prod:
    1.56 -  assumes A: "topological_basis A" and B: "topological_basis B"
    1.57 +  assumes A: "topological_basis A"
    1.58 +    and B: "topological_basis B"
    1.59    shows "topological_basis ((\<lambda>(a, b). a \<times> b) ` (A \<times> B))"
    1.60    unfolding topological_basis_def
    1.61  proof (safe, simp_all del: ex_simps add: subset_image_iff ex_simps(1)[symmetric])
    1.62 -  fix S :: "('a \<times> 'b) set" assume "open S"
    1.63 +  fix S :: "('a \<times> 'b) set"
    1.64 +  assume "open S"
    1.65    then show "\<exists>X\<subseteq>A \<times> B. (\<Union>(a,b)\<in>X. a \<times> b) = S"
    1.66    proof (safe intro!: exI[of _ "{x\<in>A \<times> B. fst x \<times> snd x \<subseteq> S}"])
    1.67 -    fix x y assume "(x, y) \<in> S"
    1.68 +    fix x y
    1.69 +    assume "(x, y) \<in> S"
    1.70      from open_prod_elim[OF `open S` this]
    1.71      obtain a b where a: "open a""x \<in> a" and b: "open b" "y \<in> b" and "a \<times> b \<subseteq> S"
    1.72        by (metis mem_Sigma_iff)
    1.73 @@ -162,6 +173,7 @@
    1.74    qed auto
    1.75  qed (metis A B topological_basis_open open_Times)
    1.76  
    1.77 +
    1.78  subsection {* Countable Basis *}
    1.79  
    1.80  locale countable_basis =
    1.81 @@ -173,12 +185,14 @@
    1.82  lemma open_countable_basis_ex:
    1.83    assumes "open X"
    1.84    shows "\<exists>B' \<subseteq> B. X = Union B'"
    1.85 -  using assms countable_basis is_basis unfolding topological_basis_def by blast
    1.86 +  using assms countable_basis is_basis
    1.87 +  unfolding topological_basis_def by blast
    1.88  
    1.89  lemma open_countable_basisE:
    1.90    assumes "open X"
    1.91    obtains B' where "B' \<subseteq> B" "X = Union B'"
    1.92 -  using assms open_countable_basis_ex by (atomize_elim) simp
    1.93 +  using assms open_countable_basis_ex
    1.94 +  by (atomize_elim) simp
    1.95  
    1.96  lemma countable_dense_exists:
    1.97    shows "\<exists>D::'a set. countable D \<and> (\<forall>X. open X \<longrightarrow> X \<noteq> {} \<longrightarrow> (\<exists>d \<in> D. d \<in> X))"
    1.98 @@ -213,34 +227,47 @@
    1.99  proof atomize_elim
   1.100    from first_countable_basisE[of x] guess A' . note A' = this
   1.101    def A \<equiv> "(\<lambda>N. \<Inter>((\<lambda>n. from_nat_into A' n) ` N)) ` (Collect finite::nat set set)"
   1.102 -  thus "\<exists>A. countable A \<and> (\<forall>a. a \<in> A \<longrightarrow> x \<in> a) \<and> (\<forall>a. a \<in> A \<longrightarrow> open a) \<and>
   1.103 +  then show "\<exists>A. countable A \<and> (\<forall>a. a \<in> A \<longrightarrow> x \<in> a) \<and> (\<forall>a. a \<in> A \<longrightarrow> open a) \<and>
   1.104          (\<forall>S. open S \<longrightarrow> x \<in> S \<longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)) \<and> (\<forall>a b. a \<in> A \<longrightarrow> b \<in> A \<longrightarrow> a \<inter> b \<in> A)"
   1.105    proof (safe intro!: exI[where x=A])
   1.106 -    show "countable A" unfolding A_def by (intro countable_image countable_Collect_finite)
   1.107 -    fix a assume "a \<in> A"
   1.108 -    thus "x \<in> a" "open a" using A'(4)[OF open_UNIV] by (auto simp: A_def intro: A' from_nat_into)
   1.109 +    show "countable A"
   1.110 +      unfolding A_def by (intro countable_image countable_Collect_finite)
   1.111 +    fix a
   1.112 +    assume "a \<in> A"
   1.113 +    then show "x \<in> a" "open a"
   1.114 +      using A'(4)[OF open_UNIV] by (auto simp: A_def intro: A' from_nat_into)
   1.115    next
   1.116      let ?int = "\<lambda>N. \<Inter>(from_nat_into A' ` N)"
   1.117 -    fix a b assume "a \<in> A" "b \<in> A"
   1.118 -    then obtain N M where "a = ?int N" "b = ?int M" "finite (N \<union> M)" by (auto simp: A_def)
   1.119 -    thus "a \<inter> b \<in> A" by (auto simp: A_def intro!: image_eqI[where x="N \<union> M"])
   1.120 +    fix a b
   1.121 +    assume "a \<in> A" "b \<in> A"
   1.122 +    then obtain N M where "a = ?int N" "b = ?int M" "finite (N \<union> M)"
   1.123 +      by (auto simp: A_def)
   1.124 +    then show "a \<inter> b \<in> A"
   1.125 +      by (auto simp: A_def intro!: image_eqI[where x="N \<union> M"])
   1.126    next
   1.127 -    fix S assume "open S" "x \<in> S" then obtain a where a: "a\<in>A'" "a \<subseteq> S" using A' by blast
   1.128 -    thus "\<exists>a\<in>A. a \<subseteq> S" using a A'
   1.129 +    fix S
   1.130 +    assume "open S" "x \<in> S"
   1.131 +    then obtain a where a: "a\<in>A'" "a \<subseteq> S" using A' by blast
   1.132 +    then show "\<exists>a\<in>A. a \<subseteq> S" using a A'
   1.133        by (intro bexI[where x=a]) (auto simp: A_def intro: image_eqI[where x="{to_nat_on A' a}"])
   1.134    qed
   1.135  qed
   1.136  
   1.137  lemma (in topological_space) first_countableI:
   1.138 -  assumes "countable A" and 1: "\<And>a. a \<in> A \<Longrightarrow> x \<in> a" "\<And>a. a \<in> A \<Longrightarrow> open a"
   1.139 -   and 2: "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>a\<in>A. a \<subseteq> S"
   1.140 +  assumes "countable A"
   1.141 +    and 1: "\<And>a. a \<in> A \<Longrightarrow> x \<in> a" "\<And>a. a \<in> A \<Longrightarrow> open a"
   1.142 +    and 2: "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>a\<in>A. a \<subseteq> S"
   1.143    shows "\<exists>A::nat \<Rightarrow> 'a set. (\<forall>i. x \<in> A i \<and> open (A i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A i \<subseteq> S))"
   1.144  proof (safe intro!: exI[of _ "from_nat_into A"])
   1.145 +  fix i
   1.146    have "A \<noteq> {}" using 2[of UNIV] by auto
   1.147 -  { fix i show "x \<in> from_nat_into A i" "open (from_nat_into A i)"
   1.148 -      using range_from_nat_into_subset[OF `A \<noteq> {}`] 1 by auto }
   1.149 -  { fix S assume "open S" "x\<in>S" from 2[OF this] show "\<exists>i. from_nat_into A i \<subseteq> S"
   1.150 -      using subset_range_from_nat_into[OF `countable A`] by auto }
   1.151 +  show "x \<in> from_nat_into A i" "open (from_nat_into A i)"
   1.152 +    using range_from_nat_into_subset[OF `A \<noteq> {}`] 1 by auto
   1.153 +next
   1.154 +  fix S
   1.155 +  assume "open S" "x\<in>S" from 2[OF this]
   1.156 +  show "\<exists>i. from_nat_into A i \<subseteq> S"
   1.157 +    using subset_range_from_nat_into[OF `countable A`] by auto
   1.158  qed
   1.159  
   1.160  instance prod :: (first_countable_topology, first_countable_topology) first_countable_topology
   1.161 @@ -250,11 +277,13 @@
   1.162    from first_countable_basisE[of "snd x"] guess B :: "'b set set" . note B = this
   1.163    show "\<exists>A::nat \<Rightarrow> ('a \<times> 'b) set. (\<forall>i. x \<in> A i \<and> open (A i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A i \<subseteq> S))"
   1.164    proof (rule first_countableI[of "(\<lambda>(a, b). a \<times> b) ` (A \<times> B)"], safe)
   1.165 -    fix a b assume x: "a \<in> A" "b \<in> B"
   1.166 +    fix a b
   1.167 +    assume x: "a \<in> A" "b \<in> B"
   1.168      with A(2, 3)[of a] B(2, 3)[of b] show "x \<in> a \<times> b" "open (a \<times> b)"
   1.169        unfolding mem_Times_iff by (auto intro: open_Times)
   1.170    next
   1.171 -    fix S assume "open S" "x \<in> S"
   1.172 +    fix S
   1.173 +    assume "open S" "x \<in> S"
   1.174      from open_prod_elim[OF this] guess a' b' .
   1.175      moreover with A(4)[of a'] B(4)[of b']
   1.176      obtain a b where "a \<in> A" "a \<subseteq> a'" "b \<in> B" "b \<subseteq> b'" by auto
   1.177 @@ -269,18 +298,22 @@
   1.178  
   1.179  lemma ex_countable_basis: "\<exists>B::'a set set. countable B \<and> topological_basis B"
   1.180  proof -
   1.181 -  from ex_countable_subbasis obtain B where B: "countable B" "open = generate_topology B" by blast
   1.182 +  from ex_countable_subbasis obtain B where B: "countable B" "open = generate_topology B"
   1.183 +    by blast
   1.184    let ?B = "Inter ` {b. finite b \<and> b \<subseteq> B }"
   1.185  
   1.186    show ?thesis
   1.187    proof (intro exI conjI)
   1.188      show "countable ?B"
   1.189        by (intro countable_image countable_Collect_finite_subset B)
   1.190 -    { fix S assume "open S"
   1.191 +    {
   1.192 +      fix S
   1.193 +      assume "open S"
   1.194        then have "\<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. (\<Union>b\<in>B'. \<Inter>b) = S"
   1.195          unfolding B
   1.196        proof induct
   1.197 -        case UNIV show ?case by (intro exI[of _ "{{}}"]) simp
   1.198 +        case UNIV
   1.199 +        show ?case by (intro exI[of _ "{{}}"]) simp
   1.200        next
   1.201          case (Int a b)
   1.202          then obtain x y where x: "a = UNION x Inter" "\<And>i. i \<in> x \<Longrightarrow> finite i \<and> i \<subseteq> B"
   1.203 @@ -296,7 +329,8 @@
   1.204          then show "\<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. UNION B' Inter = \<Union>K"
   1.205            by (intro exI[of _ "UNION K k"]) auto
   1.206        next
   1.207 -        case (Basis S) then show ?case
   1.208 +        case (Basis S)
   1.209 +        then show ?case
   1.210            by (intro exI[of _ "{{S}}"]) auto
   1.211        qed
   1.212        then have "(\<exists>B'\<subseteq>Inter ` {b. finite b \<and> b \<subseteq> B}. \<Union>B' = S)"
   1.213 @@ -339,6 +373,7 @@
   1.214         (fastforce simp: topological_space_class.topological_basis_def)+
   1.215  qed
   1.216  
   1.217 +
   1.218  subsection {* Polish spaces *}
   1.219  
   1.220  text {* Textbooks define Polish spaces as completely metrizable.
   1.221 @@ -348,7 +383,9 @@
   1.222  
   1.223  subsection {* General notion of a topology as a value *}
   1.224  
   1.225 -definition "istopology L \<longleftrightarrow> L {} \<and> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>K. Ball K L \<longrightarrow> L (\<Union> K))"
   1.226 +definition "istopology L \<longleftrightarrow>
   1.227 +  L {} \<and> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>K. Ball K L \<longrightarrow> L (\<Union> K))"
   1.228 +
   1.229  typedef 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"
   1.230    morphisms "openin" "topology"
   1.231    unfolding istopology_def by blast
   1.232 @@ -363,16 +400,14 @@
   1.233    using topology_inverse[of U] istopology_open_in[of "topology U"] by auto
   1.234  
   1.235  lemma topology_eq: "T1 = T2 \<longleftrightarrow> (\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S)"
   1.236 -proof-
   1.237 -  { assume "T1=T2"
   1.238 -    hence "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S" by simp }
   1.239 -  moreover
   1.240 -  { assume H: "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S"
   1.241 -    hence "openin T1 = openin T2" by (simp add: fun_eq_iff)
   1.242 -    hence "topology (openin T1) = topology (openin T2)" by simp
   1.243 -    hence "T1 = T2" unfolding openin_inverse .
   1.244 -  }
   1.245 -  ultimately show ?thesis by blast
   1.246 +proof
   1.247 +  assume "T1 = T2"
   1.248 +  then show "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S" by simp
   1.249 +next
   1.250 +  assume H: "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S"
   1.251 +  then have "openin T1 = openin T2" by (simp add: fun_eq_iff)
   1.252 +  then have "topology (openin T1) = topology (openin T2)" by simp
   1.253 +  then show "T1 = T2" unfolding openin_inverse .
   1.254  qed
   1.255  
   1.256  text{* Infer the "universe" from union of all sets in the topology. *}
   1.257 @@ -391,7 +426,9 @@
   1.258  
   1.259  lemma openin_subset[intro]: "openin U S \<Longrightarrow> S \<subseteq> topspace U"
   1.260    unfolding topspace_def by blast
   1.261 -lemma openin_empty[simp]: "openin U {}" by (simp add: openin_clauses)
   1.262 +
   1.263 +lemma openin_empty[simp]: "openin U {}"
   1.264 +  by (simp add: openin_clauses)
   1.265  
   1.266  lemma openin_Int[intro]: "openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S \<inter> T)"
   1.267    using openin_clauses by simp
   1.268 @@ -402,7 +439,8 @@
   1.269  lemma openin_Un[intro]: "openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S \<union> T)"
   1.270    using openin_Union[of "{S,T}" U] by auto
   1.271  
   1.272 -lemma openin_topspace[intro, simp]: "openin U (topspace U)" by (simp add: openin_Union topspace_def)
   1.273 +lemma openin_topspace[intro, simp]: "openin U (topspace U)"
   1.274 +  by (simp add: openin_Union topspace_def)
   1.275  
   1.276  lemma openin_subopen: "openin U S \<longleftrightarrow> (\<forall>x \<in> S. \<exists>T. openin U T \<and> x \<in> T \<and> T \<subseteq> S)"
   1.277    (is "?lhs \<longleftrightarrow> ?rhs")
   1.278 @@ -422,42 +460,63 @@
   1.279  
   1.280  definition "closedin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> openin U (topspace U - S)"
   1.281  
   1.282 -lemma closedin_subset: "closedin U S \<Longrightarrow> S \<subseteq> topspace U" by (metis closedin_def)
   1.283 -lemma closedin_empty[simp]: "closedin U {}" by (simp add: closedin_def)
   1.284 -lemma closedin_topspace[intro,simp]:
   1.285 -  "closedin U (topspace U)" by (simp add: closedin_def)
   1.286 +lemma closedin_subset: "closedin U S \<Longrightarrow> S \<subseteq> topspace U"
   1.287 +  by (metis closedin_def)
   1.288 +
   1.289 +lemma closedin_empty[simp]: "closedin U {}"
   1.290 +  by (simp add: closedin_def)
   1.291 +
   1.292 +lemma closedin_topspace[intro, simp]: "closedin U (topspace U)"
   1.293 +  by (simp add: closedin_def)
   1.294 +
   1.295  lemma closedin_Un[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<union> T)"
   1.296    by (auto simp add: Diff_Un closedin_def)
   1.297  
   1.298 -lemma Diff_Inter[intro]: "A - \<Inter>S = \<Union> {A - s|s. s\<in>S}" by auto
   1.299 -lemma closedin_Inter[intro]: assumes Ke: "K \<noteq> {}" and Kc: "\<forall>S \<in>K. closedin U S"
   1.300 -  shows "closedin U (\<Inter> K)"  using Ke Kc unfolding closedin_def Diff_Inter by auto
   1.301 +lemma Diff_Inter[intro]: "A - \<Inter>S = \<Union> {A - s|s. s\<in>S}"
   1.302 +  by auto
   1.303 +
   1.304 +lemma closedin_Inter[intro]:
   1.305 +  assumes Ke: "K \<noteq> {}"
   1.306 +    and Kc: "\<forall>S \<in>K. closedin U S"
   1.307 +  shows "closedin U (\<Inter> K)"
   1.308 +  using Ke Kc unfolding closedin_def Diff_Inter by auto
   1.309  
   1.310  lemma closedin_Int[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<inter> T)"
   1.311    using closedin_Inter[of "{S,T}" U] by auto
   1.312  
   1.313 -lemma Diff_Diff_Int: "A - (A - B) = A \<inter> B" by blast
   1.314 +lemma Diff_Diff_Int: "A - (A - B) = A \<inter> B"
   1.315 +  by blast
   1.316 +
   1.317  lemma openin_closedin_eq: "openin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> closedin U (topspace U - S)"
   1.318    apply (auto simp add: closedin_def Diff_Diff_Int inf_absorb2)
   1.319    apply (metis openin_subset subset_eq)
   1.320    done
   1.321  
   1.322 -lemma openin_closedin:  "S \<subseteq> topspace U \<Longrightarrow> (openin U S \<longleftrightarrow> closedin U (topspace U - S))"
   1.323 +lemma openin_closedin: "S \<subseteq> topspace U \<Longrightarrow> (openin U S \<longleftrightarrow> closedin U (topspace U - S))"
   1.324    by (simp add: openin_closedin_eq)
   1.325  
   1.326 -lemma openin_diff[intro]: assumes oS: "openin U S" and cT: "closedin U T" shows "openin U (S - T)"
   1.327 -proof-
   1.328 +lemma openin_diff[intro]:
   1.329 +  assumes oS: "openin U S"
   1.330 +    and cT: "closedin U T"
   1.331 +  shows "openin U (S - T)"
   1.332 +proof -
   1.333    have "S - T = S \<inter> (topspace U - T)" using openin_subset[of U S]  oS cT
   1.334      by (auto simp add: topspace_def openin_subset)
   1.335    then show ?thesis using oS cT by (auto simp add: closedin_def)
   1.336  qed
   1.337  
   1.338 -lemma closedin_diff[intro]: assumes oS: "closedin U S" and cT: "openin U T" shows "closedin U (S - T)"
   1.339 -proof-
   1.340 -  have "S - T = S \<inter> (topspace U - T)" using closedin_subset[of U S]  oS cT
   1.341 -    by (auto simp add: topspace_def )
   1.342 -  then show ?thesis using oS cT by (auto simp add: openin_closedin_eq)
   1.343 -qed
   1.344 +lemma closedin_diff[intro]:
   1.345 +  assumes oS: "closedin U S"
   1.346 +    and cT: "openin U T"
   1.347 +  shows "closedin U (S - T)"
   1.348 +proof -
   1.349 +  have "S - T = S \<inter> (topspace U - T)"
   1.350 +    using closedin_subset[of U S] oS cT
   1.351 +    by (auto simp add: topspace_def)
   1.352 +  then show ?thesis
   1.353 +    using oS cT by (auto simp add: openin_closedin_eq)
   1.354 +qed
   1.355 +
   1.356  
   1.357  subsubsection {* Subspace topology *}
   1.358  
   1.359 @@ -465,48 +524,59 @@
   1.360  
   1.361  lemma istopology_subtopology: "istopology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"
   1.362    (is "istopology ?L")
   1.363 -proof-
   1.364 +proof -
   1.365    have "?L {}" by blast
   1.366 -  {fix A B assume A: "?L A" and B: "?L B"
   1.367 -    from A B obtain Sa and Sb where Sa: "openin U Sa" "A = Sa \<inter> V" and Sb: "openin U Sb" "B = Sb \<inter> V" by blast
   1.368 -    have "A\<inter>B = (Sa \<inter> Sb) \<inter> V" "openin U (Sa \<inter> Sb)"  using Sa Sb by blast+
   1.369 -    then have "?L (A \<inter> B)" by blast}
   1.370 +  {
   1.371 +    fix A B
   1.372 +    assume A: "?L A" and B: "?L B"
   1.373 +    from A B obtain Sa and Sb where Sa: "openin U Sa" "A = Sa \<inter> V" and Sb: "openin U Sb" "B = Sb \<inter> V"
   1.374 +      by blast
   1.375 +    have "A \<inter> B = (Sa \<inter> Sb) \<inter> V" "openin U (Sa \<inter> Sb)"
   1.376 +      using Sa Sb by blast+
   1.377 +    then have "?L (A \<inter> B)" by blast
   1.378 +  }
   1.379    moreover
   1.380 -  {fix K assume K: "K \<subseteq> Collect ?L"
   1.381 +  {
   1.382 +    fix K assume K: "K \<subseteq> Collect ?L"
   1.383      have th0: "Collect ?L = (\<lambda>S. S \<inter> V) ` Collect (openin U)"
   1.384        apply (rule set_eqI)
   1.385        apply (simp add: Ball_def image_iff)
   1.386 -      by metis
   1.387 +      apply metis
   1.388 +      done
   1.389      from K[unfolded th0 subset_image_iff]
   1.390 -    obtain Sk where Sk: "Sk \<subseteq> Collect (openin U)" "K = (\<lambda>S. S \<inter> V) ` Sk" by blast
   1.391 -    have "\<Union>K = (\<Union>Sk) \<inter> V" using Sk by auto
   1.392 -    moreover have "openin U (\<Union> Sk)" using Sk by (auto simp add: subset_eq)
   1.393 -    ultimately have "?L (\<Union>K)" by blast}
   1.394 +    obtain Sk where Sk: "Sk \<subseteq> Collect (openin U)" "K = (\<lambda>S. S \<inter> V) ` Sk"
   1.395 +      by blast
   1.396 +    have "\<Union>K = (\<Union>Sk) \<inter> V"
   1.397 +      using Sk by auto
   1.398 +    moreover have "openin U (\<Union> Sk)"
   1.399 +      using Sk by (auto simp add: subset_eq)
   1.400 +    ultimately have "?L (\<Union>K)" by blast
   1.401 +  }
   1.402    ultimately show ?thesis
   1.403      unfolding subset_eq mem_Collect_eq istopology_def by blast
   1.404  qed
   1.405  
   1.406 -lemma openin_subtopology:
   1.407 -  "openin (subtopology U V) S \<longleftrightarrow> (\<exists> T. (openin U T) \<and> (S = T \<inter> V))"
   1.408 +lemma openin_subtopology: "openin (subtopology U V) S \<longleftrightarrow> (\<exists>T. openin U T \<and> S = T \<inter> V)"
   1.409    unfolding subtopology_def topology_inverse'[OF istopology_subtopology]
   1.410    by auto
   1.411  
   1.412 -lemma topspace_subtopology: "topspace(subtopology U V) = topspace U \<inter> V"
   1.413 +lemma topspace_subtopology: "topspace (subtopology U V) = topspace U \<inter> V"
   1.414    by (auto simp add: topspace_def openin_subtopology)
   1.415  
   1.416 -lemma closedin_subtopology:
   1.417 -  "closedin (subtopology U V) S \<longleftrightarrow> (\<exists>T. closedin U T \<and> S = T \<inter> V)"
   1.418 +lemma closedin_subtopology: "closedin (subtopology U V) S \<longleftrightarrow> (\<exists>T. closedin U T \<and> S = T \<inter> V)"
   1.419    unfolding closedin_def topspace_subtopology
   1.420    apply (simp add: openin_subtopology)
   1.421    apply (rule iffI)
   1.422    apply clarify
   1.423    apply (rule_tac x="topspace U - T" in exI)
   1.424 -  by auto
   1.425 +  apply auto
   1.426 +  done
   1.427  
   1.428  lemma openin_subtopology_refl: "openin (subtopology U V) V \<longleftrightarrow> V \<subseteq> topspace U"
   1.429    unfolding openin_subtopology
   1.430    apply (rule iffI, clarify)
   1.431 -  apply (frule openin_subset[of U])  apply blast
   1.432 +  apply (frule openin_subset[of U])
   1.433 +  apply blast
   1.434    apply (rule exI[where x="topspace U"])
   1.435    apply auto
   1.436    done
   1.437 @@ -514,17 +584,28 @@
   1.438  lemma subtopology_superset:
   1.439    assumes UV: "topspace U \<subseteq> V"
   1.440    shows "subtopology U V = U"
   1.441 -proof-
   1.442 -  {fix S
   1.443 -    {fix T assume T: "openin U T" "S = T \<inter> V"
   1.444 -      from T openin_subset[OF T(1)] UV have eq: "S = T" by blast
   1.445 -      have "openin U S" unfolding eq using T by blast}
   1.446 +proof -
   1.447 +  {
   1.448 +    fix S
   1.449 +    {
   1.450 +      fix T
   1.451 +      assume T: "openin U T" "S = T \<inter> V"
   1.452 +      from T openin_subset[OF T(1)] UV have eq: "S = T"
   1.453 +        by blast
   1.454 +      have "openin U S"
   1.455 +        unfolding eq using T by blast
   1.456 +    }
   1.457      moreover
   1.458 -    {assume S: "openin U S"
   1.459 -      hence "\<exists>T. openin U T \<and> S = T \<inter> V"
   1.460 -        using openin_subset[OF S] UV by auto}
   1.461 -    ultimately have "(\<exists>T. openin U T \<and> S = T \<inter> V) \<longleftrightarrow> openin U S" by blast}
   1.462 -  then show ?thesis unfolding topology_eq openin_subtopology by blast
   1.463 +    {
   1.464 +      assume S: "openin U S"
   1.465 +      then have "\<exists>T. openin U T \<and> S = T \<inter> V"
   1.466 +        using openin_subset[OF S] UV by auto
   1.467 +    }
   1.468 +    ultimately have "(\<exists>T. openin U T \<and> S = T \<inter> V) \<longleftrightarrow> openin U S"
   1.469 +      by blast
   1.470 +  }
   1.471 +  then show ?thesis
   1.472 +    unfolding topology_eq openin_subtopology by blast
   1.473  qed
   1.474  
   1.475  lemma subtopology_topspace[simp]: "subtopology U (topspace U) = U"
   1.476 @@ -533,11 +614,11 @@
   1.477  lemma subtopology_UNIV[simp]: "subtopology U UNIV = U"
   1.478    by (simp add: subtopology_superset)
   1.479  
   1.480 +
   1.481  subsubsection {* The standard Euclidean topology *}
   1.482  
   1.483 -definition
   1.484 -  euclidean :: "'a::topological_space topology" where
   1.485 -  "euclidean = topology open"
   1.486 +definition euclidean :: "'a::topological_space topology"
   1.487 +  where "euclidean = topology open"
   1.488  
   1.489  lemma open_openin: "open S \<longleftrightarrow> openin euclidean S"
   1.490    unfolding euclidean_def
   1.491 @@ -549,7 +630,8 @@
   1.492  lemma topspace_euclidean: "topspace euclidean = UNIV"
   1.493    apply (simp add: topspace_def)
   1.494    apply (rule set_eqI)
   1.495 -  by (auto simp add: open_openin[symmetric])
   1.496 +  apply (auto simp add: open_openin[symmetric])
   1.497 +  done
   1.498  
   1.499  lemma topspace_euclidean_subtopology[simp]: "topspace (subtopology euclidean S) = S"
   1.500    by (simp add: topspace_euclidean topspace_subtopology)
   1.501 @@ -569,10 +651,10 @@
   1.502    by (auto simp add: openin_open)
   1.503  
   1.504  lemma open_openin_trans[trans]:
   1.505 - "open S \<Longrightarrow> open T \<Longrightarrow> T \<subseteq> S \<Longrightarrow> openin (subtopology euclidean S) T"
   1.506 +  "open S \<Longrightarrow> open T \<Longrightarrow> T \<subseteq> S \<Longrightarrow> openin (subtopology euclidean S) T"
   1.507    by (metis Int_absorb1  openin_open_Int)
   1.508  
   1.509 -lemma open_subset:  "S \<subseteq> T \<Longrightarrow> open S \<Longrightarrow> openin (subtopology euclidean T) S"
   1.510 +lemma open_subset: "S \<subseteq> T \<Longrightarrow> open S \<Longrightarrow> openin (subtopology euclidean T) S"
   1.511    by (auto simp add: openin_open)
   1.512  
   1.513  lemma closedin_closed: "closedin (subtopology euclidean U) S \<longleftrightarrow> (\<exists>T. closed T \<and> S = U \<inter> T)"
   1.514 @@ -593,10 +675,12 @@
   1.515  
   1.516  lemma openin_euclidean_subtopology_iff:
   1.517    fixes S U :: "'a::metric_space set"
   1.518 -  shows "openin (subtopology euclidean U) S
   1.519 -  \<longleftrightarrow> S \<subseteq> U \<and> (\<forall>x\<in>S. \<exists>e>0. \<forall>x'\<in>U. dist x' x < e \<longrightarrow> x'\<in> S)" (is "?lhs \<longleftrightarrow> ?rhs")
   1.520 +  shows "openin (subtopology euclidean U) S \<longleftrightarrow>
   1.521 +    S \<subseteq> U \<and> (\<forall>x\<in>S. \<exists>e>0. \<forall>x'\<in>U. dist x' x < e \<longrightarrow> x'\<in> S)"
   1.522 +  (is "?lhs \<longleftrightarrow> ?rhs")
   1.523  proof
   1.524 -  assume ?lhs thus ?rhs unfolding openin_open open_dist by blast
   1.525 +  assume ?lhs
   1.526 +  then show ?rhs unfolding openin_open open_dist by blast
   1.527  next
   1.528    def T \<equiv> "{x. \<exists>a\<in>S. \<exists>d>0. (\<forall>y\<in>U. dist y a < d \<longrightarrow> y \<in> S) \<and> dist x a < d}"
   1.529    have 1: "\<forall>x\<in>T. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> T"
   1.530 @@ -620,17 +704,17 @@
   1.531  
   1.532  text {* These "transitivity" results are handy too *}
   1.533  
   1.534 -lemma openin_trans[trans]: "openin (subtopology euclidean T) S \<Longrightarrow> openin (subtopology euclidean U) T
   1.535 -  \<Longrightarrow> openin (subtopology euclidean U) S"
   1.536 +lemma openin_trans[trans]:
   1.537 +  "openin (subtopology euclidean T) S \<Longrightarrow> openin (subtopology euclidean U) T \<Longrightarrow>
   1.538 +    openin (subtopology euclidean U) S"
   1.539    unfolding open_openin openin_open by blast
   1.540  
   1.541  lemma openin_open_trans: "openin (subtopology euclidean T) S \<Longrightarrow> open T \<Longrightarrow> open S"
   1.542    by (auto simp add: openin_open intro: openin_trans)
   1.543  
   1.544  lemma closedin_trans[trans]:
   1.545 - "closedin (subtopology euclidean T) S \<Longrightarrow>
   1.546 -           closedin (subtopology euclidean U) T
   1.547 -           ==> closedin (subtopology euclidean U) S"
   1.548 +  "closedin (subtopology euclidean T) S \<Longrightarrow> closedin (subtopology euclidean U) T \<Longrightarrow>
   1.549 +    closedin (subtopology euclidean U) S"
   1.550    by (auto simp add: closedin_closed closed_closedin closed_Inter Int_assoc)
   1.551  
   1.552  lemma closedin_closed_trans: "closedin (subtopology euclidean T) S \<Longrightarrow> closed T \<Longrightarrow> closed S"
   1.553 @@ -639,13 +723,11 @@
   1.554  
   1.555  subsection {* Open and closed balls *}
   1.556  
   1.557 -definition
   1.558 -  ball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set" where
   1.559 -  "ball x e = {y. dist x y < e}"
   1.560 -
   1.561 -definition
   1.562 -  cball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set" where
   1.563 -  "cball x e = {y. dist x y \<le> e}"
   1.564 +definition ball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
   1.565 +  where "ball x e = {y. dist x y < e}"
   1.566 +
   1.567 +definition cball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
   1.568 +  where "cball x e = {y. dist x y \<le> e}"
   1.569  
   1.570  lemma mem_ball [simp]: "y \<in> ball x e \<longleftrightarrow> dist x y < e"
   1.571    by (simp add: ball_def)
   1.572 @@ -669,20 +751,33 @@
   1.573  lemma centre_in_cball: "x \<in> cball x e \<longleftrightarrow> 0 \<le> e"
   1.574    by simp
   1.575  
   1.576 -lemma ball_subset_cball[simp,intro]: "ball x e \<subseteq> cball x e" by (simp add: subset_eq)
   1.577 -lemma subset_ball[intro]: "d <= e ==> ball x d \<subseteq> ball x e" by (simp add: subset_eq)
   1.578 -lemma subset_cball[intro]: "d <= e ==> cball x d \<subseteq> cball x e" by (simp add: subset_eq)
   1.579 +lemma ball_subset_cball[simp,intro]: "ball x e \<subseteq> cball x e"
   1.580 +  by (simp add: subset_eq)
   1.581 +
   1.582 +lemma subset_ball[intro]: "d <= e ==> ball x d \<subseteq> ball x e"
   1.583 +  by (simp add: subset_eq)
   1.584 +
   1.585 +lemma subset_cball[intro]: "d <= e ==> cball x d \<subseteq> cball x e"
   1.586 +  by (simp add: subset_eq)
   1.587 +
   1.588  lemma ball_max_Un: "ball a (max r s) = ball a r \<union> ball a s"
   1.589    by (simp add: set_eq_iff) arith
   1.590  
   1.591  lemma ball_min_Int: "ball a (min r s) = ball a r \<inter> ball a s"
   1.592    by (simp add: set_eq_iff)
   1.593  
   1.594 -lemma diff_less_iff: "(a::real) - b > 0 \<longleftrightarrow> a > b"
   1.595 +lemma diff_less_iff:
   1.596 +  "(a::real) - b > 0 \<longleftrightarrow> a > b"
   1.597    "(a::real) - b < 0 \<longleftrightarrow> a < b"
   1.598 -  "a - b < c \<longleftrightarrow> a < c +b" "a - b > c \<longleftrightarrow> a > c +b" by arith+
   1.599 -lemma diff_le_iff: "(a::real) - b \<ge> 0 \<longleftrightarrow> a \<ge> b" "(a::real) - b \<le> 0 \<longleftrightarrow> a \<le> b"
   1.600 -  "a - b \<le> c \<longleftrightarrow> a \<le> c +b" "a - b \<ge> c \<longleftrightarrow> a \<ge> c +b"  by arith+
   1.601 +  "a - b < c \<longleftrightarrow> a < c + b" "a - b > c \<longleftrightarrow> a > c + b"
   1.602 +  by arith+
   1.603 +
   1.604 +lemma diff_le_iff:
   1.605 +  "(a::real) - b \<ge> 0 \<longleftrightarrow> a \<ge> b"
   1.606 +  "(a::real) - b \<le> 0 \<longleftrightarrow> a \<le> b"
   1.607 +  "a - b \<le> c \<longleftrightarrow> a \<le> c + b"
   1.608 +  "a - b \<ge> c \<longleftrightarrow> a \<ge> c + b"
   1.609 +  by arith+
   1.610  
   1.611  lemma open_ball[intro, simp]: "open (ball x e)"
   1.612    unfolding open_dist ball_def mem_Collect_eq Ball_def
   1.613 @@ -730,30 +825,41 @@
   1.614    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"
   1.615  proof -
   1.616    def e' \<equiv> "e / (2 * sqrt (real (DIM ('a))))"
   1.617 -  then have e: "0 < e'" using assms by (auto intro!: divide_pos_pos simp: DIM_positive)
   1.618 +  then have e: "0 < e'"
   1.619 +    using assms by (auto intro!: divide_pos_pos simp: DIM_positive)
   1.620    have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> y < x \<bullet> i \<and> x \<bullet> i - y < e'" (is "\<forall>i. ?th i")
   1.621    proof
   1.622 -    fix i from Rats_dense_in_real[of "x \<bullet> i - e'" "x \<bullet> i"] e show "?th i" by auto
   1.623 +    fix i
   1.624 +    from Rats_dense_in_real[of "x \<bullet> i - e'" "x \<bullet> i"] e
   1.625 +    show "?th i" by auto
   1.626    qed
   1.627    from choice[OF this] guess a .. note a = this
   1.628    have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> x \<bullet> i < y \<and> y - x \<bullet> i < e'" (is "\<forall>i. ?th i")
   1.629    proof
   1.630 -    fix i from Rats_dense_in_real[of "x \<bullet> i" "x \<bullet> i + e'"] e show "?th i" by auto
   1.631 +    fix i
   1.632 +    from Rats_dense_in_real[of "x \<bullet> i" "x \<bullet> i + e'"] e
   1.633 +    show "?th i" by auto
   1.634    qed
   1.635    from choice[OF this] guess b .. note b = this
   1.636    let ?a = "\<Sum>i\<in>Basis. a i *\<^sub>R i" and ?b = "\<Sum>i\<in>Basis. b i *\<^sub>R i"
   1.637    show ?thesis
   1.638    proof (rule exI[of _ ?a], rule exI[of _ ?b], safe)
   1.639 -    fix y :: 'a assume *: "y \<in> box ?a ?b"
   1.640 +    fix y :: 'a
   1.641 +    assume *: "y \<in> box ?a ?b"
   1.642      have "dist x y = sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2)"
   1.643        unfolding setL2_def[symmetric] by (rule euclidean_dist_l2)
   1.644      also have "\<dots> < sqrt (\<Sum>(i::'a)\<in>Basis. e^2 / real (DIM('a)))"
   1.645      proof (rule real_sqrt_less_mono, rule setsum_strict_mono)
   1.646 -      fix i :: "'a" assume i: "i \<in> Basis"
   1.647 -      have "a i < y\<bullet>i \<and> y\<bullet>i < b i" using * i by (auto simp: box_def)
   1.648 -      moreover have "a i < x\<bullet>i" "x\<bullet>i - a i < e'" using a by auto
   1.649 -      moreover have "x\<bullet>i < b i" "b i - x\<bullet>i < e'" using b by auto
   1.650 -      ultimately have "\<bar>x\<bullet>i - y\<bullet>i\<bar> < 2 * e'" by auto
   1.651 +      fix i :: "'a"
   1.652 +      assume i: "i \<in> Basis"
   1.653 +      have "a i < y\<bullet>i \<and> y\<bullet>i < b i"
   1.654 +        using * i by (auto simp: box_def)
   1.655 +      moreover have "a i < x\<bullet>i" "x\<bullet>i - a i < e'"
   1.656 +        using a by auto
   1.657 +      moreover have "x\<bullet>i < b i" "b i - x\<bullet>i < e'"
   1.658 +        using b by auto
   1.659 +      ultimately have "\<bar>x\<bullet>i - y\<bullet>i\<bar> < 2 * e'"
   1.660 +        by auto
   1.661        then have "dist (x \<bullet> i) (y \<bullet> i) < e/sqrt (real (DIM('a)))"
   1.662          unfolding e'_def by (auto simp: dist_real_def)
   1.663        then have "(dist (x \<bullet> i) (y \<bullet> i))\<^sup>2 < (e/sqrt (real (DIM('a))))\<^sup>2"
   1.664 @@ -761,8 +867,10 @@
   1.665        then show "(dist (x \<bullet> i) (y \<bullet> i))\<^sup>2 < e\<^sup>2 / real DIM('a)"
   1.666          by (simp add: power_divide)
   1.667      qed auto
   1.668 -    also have "\<dots> = e" using `0 < e` by (simp add: real_eq_of_nat)
   1.669 -    finally show "y \<in> ball x e" by (auto simp: ball_def)
   1.670 +    also have "\<dots> = e"
   1.671 +      using `0 < e` by (simp add: real_eq_of_nat)
   1.672 +    finally show "y \<in> ball x e"
   1.673 +      by (auto simp: ball_def)
   1.674    qed (insert a b, auto simp: box_def)
   1.675  qed
   1.676  
   1.677 @@ -792,51 +900,67 @@
   1.678  subsection{* Connectedness *}
   1.679  
   1.680  lemma connected_local:
   1.681 - "connected S \<longleftrightarrow> ~(\<exists>e1 e2.
   1.682 -                 openin (subtopology euclidean S) e1 \<and>
   1.683 -                 openin (subtopology euclidean S) e2 \<and>
   1.684 -                 S \<subseteq> e1 \<union> e2 \<and>
   1.685 -                 e1 \<inter> e2 = {} \<and>
   1.686 -                 ~(e1 = {}) \<and>
   1.687 -                 ~(e2 = {}))"
   1.688 -unfolding connected_def openin_open by (safe, blast+)
   1.689 + "connected S \<longleftrightarrow>
   1.690 +  \<not> (\<exists>e1 e2.
   1.691 +      openin (subtopology euclidean S) e1 \<and>
   1.692 +      openin (subtopology euclidean S) e2 \<and>
   1.693 +      S \<subseteq> e1 \<union> e2 \<and>
   1.694 +      e1 \<inter> e2 = {} \<and>
   1.695 +      e1 \<noteq> {} \<and>
   1.696 +      e2 \<noteq> {})"
   1.697 +  unfolding connected_def openin_open by (safe, blast+)
   1.698  
   1.699  lemma exists_diff:
   1.700    fixes P :: "'a set \<Rightarrow> bool"
   1.701    shows "(\<exists>S. P(- S)) \<longleftrightarrow> (\<exists>S. P S)" (is "?lhs \<longleftrightarrow> ?rhs")
   1.702 -proof-
   1.703 -  {assume "?lhs" hence ?rhs by blast }
   1.704 +proof -
   1.705 +  {
   1.706 +    assume "?lhs"
   1.707 +    then have ?rhs by blast
   1.708 +  }
   1.709    moreover
   1.710 -  {fix S assume H: "P S"
   1.711 +  {
   1.712 +    fix S
   1.713 +    assume H: "P S"
   1.714      have "S = - (- S)" by auto
   1.715 -    with H have "P (- (- S))" by metis }
   1.716 +    with H have "P (- (- S))" by metis
   1.717 +  }
   1.718    ultimately show ?thesis by metis
   1.719  qed
   1.720  
   1.721  lemma connected_clopen: "connected S \<longleftrightarrow>
   1.722 -        (\<forall>T. openin (subtopology euclidean S) T \<and>
   1.723 -            closedin (subtopology euclidean S) T \<longrightarrow> T = {} \<or> T = S)" (is "?lhs \<longleftrightarrow> ?rhs")
   1.724 -proof-
   1.725 -  have " \<not> connected S \<longleftrightarrow> (\<exists>e1 e2. open e1 \<and> open (- e2) \<and> S \<subseteq> e1 \<union> (- e2) \<and> e1 \<inter> (- e2) \<inter> S = {} \<and> e1 \<inter> S \<noteq> {} \<and> (- e2) \<inter> S \<noteq> {})"
   1.726 +  (\<forall>T. openin (subtopology euclidean S) T \<and>
   1.727 +     closedin (subtopology euclidean S) T \<longrightarrow> T = {} \<or> T = S)" (is "?lhs \<longleftrightarrow> ?rhs")
   1.728 +proof -
   1.729 +  have "\<not> connected S \<longleftrightarrow>
   1.730 +    (\<exists>e1 e2. open e1 \<and> open (- e2) \<and> S \<subseteq> e1 \<union> (- e2) \<and> e1 \<inter> (- e2) \<inter> S = {} \<and> e1 \<inter> S \<noteq> {} \<and> (- e2) \<inter> S \<noteq> {})"
   1.731      unfolding connected_def openin_open closedin_closed
   1.732      apply (subst exists_diff)
   1.733      apply blast
   1.734      done
   1.735 -  hence th0: "connected S \<longleftrightarrow> \<not> (\<exists>e2 e1. closed e2 \<and> open e1 \<and> S \<subseteq> e1 \<union> (- e2) \<and> e1 \<inter> (- e2) \<inter> S = {} \<and> e1 \<inter> S \<noteq> {} \<and> (- e2) \<inter> S \<noteq> {})"
   1.736 +  hence th0: "connected S \<longleftrightarrow>
   1.737 +    \<not> (\<exists>e2 e1. closed e2 \<and> open e1 \<and> S \<subseteq> e1 \<union> (- e2) \<and> e1 \<inter> (- e2) \<inter> S = {} \<and> e1 \<inter> S \<noteq> {} \<and> (- e2) \<inter> S \<noteq> {})"
   1.738      (is " _ \<longleftrightarrow> \<not> (\<exists>e2 e1. ?P e2 e1)")
   1.739      apply (simp add: closed_def)
   1.740      apply metis
   1.741      done
   1.742 -
   1.743    have th1: "?rhs \<longleftrightarrow> \<not> (\<exists>t' t. closed t'\<and>t = S\<inter>t' \<and> t\<noteq>{} \<and> t\<noteq>S \<and> (\<exists>t'. open t' \<and> t = S \<inter> t'))"
   1.744      (is "_ \<longleftrightarrow> \<not> (\<exists>t' t. ?Q t' t)")
   1.745      unfolding connected_def openin_open closedin_closed by auto
   1.746 -  {fix e2
   1.747 -    {fix e1 have "?P e2 e1 \<longleftrightarrow> (\<exists>t.  closed e2 \<and> t = S\<inter>e2 \<and> open e1 \<and> t = S\<inter>e1 \<and> t\<noteq>{} \<and> t\<noteq>S)"
   1.748 -        by auto}
   1.749 -    then have "(\<exists>e1. ?P e2 e1) \<longleftrightarrow> (\<exists>t. ?Q e2 t)" by metis}
   1.750 -  then have "\<forall>e2. (\<exists>e1. ?P e2 e1) \<longleftrightarrow> (\<exists>t. ?Q e2 t)" by blast
   1.751 -  then show ?thesis unfolding th0 th1 by simp
   1.752 +  {
   1.753 +    fix e2
   1.754 +    {
   1.755 +      fix e1
   1.756 +      have "?P e2 e1 \<longleftrightarrow> (\<exists>t.  closed e2 \<and> t = S\<inter>e2 \<and> open e1 \<and> t = S\<inter>e1 \<and> t\<noteq>{} \<and> t\<noteq>S)"
   1.757 +        by auto
   1.758 +    }
   1.759 +    then have "(\<exists>e1. ?P e2 e1) \<longleftrightarrow> (\<exists>t. ?Q e2 t)"
   1.760 +      by metis
   1.761 +  }
   1.762 +  then have "\<forall>e2. (\<exists>e1. ?P e2 e1) \<longleftrightarrow> (\<exists>t. ?Q e2 t)"
   1.763 +    by blast
   1.764 +  then show ?thesis
   1.765 +    unfolding th0 th1 by simp
   1.766  qed
   1.767  
   1.768  lemma connected_empty[simp, intro]: "connected {}"  (* FIXME duplicate? *)
   1.769 @@ -845,9 +969,8 @@
   1.770  
   1.771  subsection{* Limit points *}
   1.772  
   1.773 -definition (in topological_space)
   1.774 -  islimpt:: "'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixr "islimpt" 60) where
   1.775 -  "x islimpt S \<longleftrightarrow> (\<forall>T. x\<in>T \<longrightarrow> open T \<longrightarrow> (\<exists>y\<in>S. y\<in>T \<and> y\<noteq>x))"
   1.776 +definition (in topological_space) islimpt:: "'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixr "islimpt" 60)
   1.777 +  where "x islimpt S \<longleftrightarrow> (\<forall>T. x\<in>T \<longrightarrow> open T \<longrightarrow> (\<exists>y\<in>S. y\<in>T \<and> y\<noteq>x))"
   1.778  
   1.779  lemma islimptI:
   1.780    assumes "\<And>T. x \<in> T \<Longrightarrow> open T \<Longrightarrow> \<exists>y\<in>S. y \<in> T \<and> y \<noteq> x"
   1.781 @@ -862,7 +985,7 @@
   1.782  lemma islimpt_iff_eventually: "x islimpt S \<longleftrightarrow> \<not> eventually (\<lambda>y. y \<notin> S) (at x)"
   1.783    unfolding islimpt_def eventually_at_topological by auto
   1.784  
   1.785 -lemma islimpt_subset: "\<lbrakk>x islimpt S; S \<subseteq> T\<rbrakk> \<Longrightarrow> x islimpt T"
   1.786 +lemma islimpt_subset: "x islimpt S \<Longrightarrow> S \<subseteq> T \<Longrightarrow> x islimpt T"
   1.787    unfolding islimpt_def by fast
   1.788  
   1.789  lemma islimpt_approachable:
   1.790 @@ -892,8 +1015,8 @@
   1.791  lemma perfect_choose_dist:
   1.792    fixes x :: "'a::{perfect_space, metric_space}"
   1.793    shows "0 < r \<Longrightarrow> \<exists>a. a \<noteq> x \<and> dist a x < r"
   1.794 -using islimpt_UNIV [of x]
   1.795 -by (simp add: islimpt_approachable)
   1.796 +  using islimpt_UNIV [of x]
   1.797 +  by (simp add: islimpt_approachable)
   1.798  
   1.799  lemma closed_limpt: "closed S \<longleftrightarrow> (\<forall>x. x islimpt S \<longrightarrow> x \<in> S)"
   1.800    unfolding closed_def
   1.801 @@ -907,20 +1030,29 @@
   1.802  
   1.803  lemma finite_set_avoid:
   1.804    fixes a :: "'a::metric_space"
   1.805 -  assumes fS: "finite S" shows  "\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<longrightarrow> d <= dist a x"
   1.806 -proof(induct rule: finite_induct[OF fS])
   1.807 -  case 1 thus ?case by (auto intro: zero_less_one)
   1.808 +  assumes fS: "finite S"
   1.809 +  shows  "\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<longrightarrow> d <= dist a x"
   1.810 +proof (induct rule: finite_induct[OF fS])
   1.811 +  case 1
   1.812 +  then show ?case by (auto intro: zero_less_one)
   1.813  next
   1.814    case (2 x F)
   1.815 -  from 2 obtain d where d: "d >0" "\<forall>x\<in>F. x\<noteq>a \<longrightarrow> d \<le> dist a x" by blast
   1.816 -  {assume "x = a" hence ?case using d by auto  }
   1.817 -  moreover
   1.818 -  {assume xa: "x\<noteq>a"
   1.819 +  from 2 obtain d where d: "d >0" "\<forall>x\<in>F. x\<noteq>a \<longrightarrow> d \<le> dist a x"
   1.820 +    by blast
   1.821 +  show ?case
   1.822 +  proof (cases "x = a")
   1.823 +    case True
   1.824 +    then show ?thesis using d by auto
   1.825 +  next
   1.826 +    case False
   1.827      let ?d = "min d (dist a x)"
   1.828 -    have dp: "?d > 0" using xa d(1) using dist_nz by auto
   1.829 -    from d have d': "\<forall>x\<in>F. x\<noteq>a \<longrightarrow> ?d \<le> dist a x" by auto
   1.830 -    with dp xa have ?case by(auto intro!: exI[where x="?d"]) }
   1.831 -  ultimately show ?case by blast
   1.832 +    have dp: "?d > 0"
   1.833 +      using False d(1) using dist_nz by auto
   1.834 +    from d have d': "\<forall>x\<in>F. x\<noteq>a \<longrightarrow> ?d \<le> dist a x"
   1.835 +      by auto
   1.836 +    with dp False show ?thesis
   1.837 +      by (auto intro!: exI[where x="?d"])
   1.838 +  qed
   1.839  qed
   1.840  
   1.841  lemma islimpt_Un: "x islimpt (S \<union> T) \<longleftrightarrow> x islimpt S \<or> x islimpt T"
   1.842 @@ -928,20 +1060,27 @@
   1.843  
   1.844  lemma discrete_imp_closed:
   1.845    fixes S :: "'a::metric_space set"
   1.846 -  assumes e: "0 < e" and d: "\<forall>x \<in> S. \<forall>y \<in> S. dist y x < e \<longrightarrow> y = x"
   1.847 +  assumes e: "0 < e"
   1.848 +    and d: "\<forall>x \<in> S. \<forall>y \<in> S. dist y x < e \<longrightarrow> y = x"
   1.849    shows "closed S"
   1.850 -proof-
   1.851 -  {fix x assume C: "\<forall>e>0. \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e"
   1.852 +proof -
   1.853 +  {
   1.854 +    fix x
   1.855 +    assume C: "\<forall>e>0. \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e"
   1.856      from e have e2: "e/2 > 0" by arith
   1.857 -    from C[rule_format, OF e2] obtain y where y: "y \<in> S" "y\<noteq>x" "dist y x < e/2" by blast
   1.858 +    from C[rule_format, OF e2] obtain y where y: "y \<in> S" "y\<noteq>x" "dist y x < e/2"
   1.859 +      by blast
   1.860      let ?m = "min (e/2) (dist x y) "
   1.861 -    from e2 y(2) have mp: "?m > 0" by (simp add: dist_nz[THEN sym])
   1.862 -    from C[rule_format, OF mp] obtain z where z: "z \<in> S" "z\<noteq>x" "dist z x < ?m" by blast
   1.863 +    from e2 y(2) have mp: "?m > 0"
   1.864 +      by (simp add: dist_nz[THEN sym])
   1.865 +    from C[rule_format, OF mp] obtain z where z: "z \<in> S" "z\<noteq>x" "dist z x < ?m"
   1.866 +      by blast
   1.867      have th: "dist z y < e" using z y
   1.868        by (intro dist_triangle_lt [where z=x], simp)
   1.869      from d[rule_format, OF y(1) z(1) th] y z
   1.870      have False by (auto simp add: dist_commute)}
   1.871 -  then show ?thesis by (metis islimpt_approachable closed_limpt [where 'a='a])
   1.872 +  then show ?thesis
   1.873 +    by (metis islimpt_approachable closed_limpt [where 'a='a])
   1.874  qed
   1.875  
   1.876  
   1.877 @@ -1005,7 +1144,8 @@
   1.878  
   1.879  lemma interior_limit_point [intro]:
   1.880    fixes x :: "'a::perfect_space"
   1.881 -  assumes x: "x \<in> interior S" shows "x islimpt S"
   1.882 +  assumes x: "x \<in> interior S"
   1.883 +  shows "x islimpt S"
   1.884    using x islimpt_UNIV [of x]
   1.885    unfolding interior_def islimpt_def
   1.886    apply (clarsimp, rename_tac T T')
   1.887 @@ -1014,15 +1154,16 @@
   1.888    done
   1.889  
   1.890  lemma interior_closed_Un_empty_interior:
   1.891 -  assumes cS: "closed S" and iT: "interior T = {}"
   1.892 +  assumes cS: "closed S"
   1.893 +    and iT: "interior T = {}"
   1.894    shows "interior (S \<union> T) = interior S"
   1.895  proof
   1.896    show "interior S \<subseteq> interior (S \<union> T)"
   1.897 -    by (rule interior_mono, rule Un_upper1)
   1.898 -next
   1.899 +    by (rule interior_mono) (rule Un_upper1)
   1.900    show "interior (S \<union> T) \<subseteq> interior S"
   1.901    proof
   1.902 -    fix x assume "x \<in> interior (S \<union> T)"
   1.903 +    fix x
   1.904 +    assume "x \<in> interior (S \<union> T)"
   1.905      then obtain R where "open R" "x \<in> R" "R \<subseteq> S \<union> T" ..
   1.906      show "x \<in> interior S"
   1.907      proof (rule ccontr)
   1.908 @@ -1043,14 +1184,17 @@
   1.909      by (intro Sigma_mono interior_subset)
   1.910    show "open (interior A \<times> interior B)"
   1.911      by (intro open_Times open_interior)
   1.912 -  fix T assume "T \<subseteq> A \<times> B" and "open T" thus "T \<subseteq> interior A \<times> interior B"
   1.913 +  fix T
   1.914 +  assume "T \<subseteq> A \<times> B" and "open T"
   1.915 +  then show "T \<subseteq> interior A \<times> interior B"
   1.916    proof (safe)
   1.917 -    fix x y assume "(x, y) \<in> T"
   1.918 +    fix x y
   1.919 +    assume "(x, y) \<in> T"
   1.920      then obtain C D where "open C" "open D" "C \<times> D \<subseteq> T" "x \<in> C" "y \<in> D"
   1.921        using `open T` unfolding open_prod_def by fast
   1.922 -    hence "open C" "open D" "C \<subseteq> A" "D \<subseteq> B" "x \<in> C" "y \<in> D"
   1.923 +    then have "open C" "open D" "C \<subseteq> A" "D \<subseteq> B" "x \<in> C" "y \<in> D"
   1.924        using `T \<subseteq> A \<times> B` by auto
   1.925 -    thus "x \<in> interior A" and "y \<in> interior B"
   1.926 +    then show "x \<in> interior A" and "y \<in> interior B"
   1.927        by (auto intro: interiorI)
   1.928    qed
   1.929  qed
   1.930 @@ -1091,8 +1235,9 @@
   1.931    unfolding closure_hull by (rule hull_minimal)
   1.932  
   1.933  lemma closure_unique:
   1.934 -  assumes "S \<subseteq> T" and "closed T"
   1.935 -  assumes "\<And>T'. S \<subseteq> T' \<Longrightarrow> closed T' \<Longrightarrow> T \<subseteq> T'"
   1.936 +  assumes "S \<subseteq> T"
   1.937 +    and "closed T"
   1.938 +    and "\<And>T'. S \<subseteq> T' \<Longrightarrow> closed T' \<Longrightarrow> T \<subseteq> T'"
   1.939    shows "closure S = T"
   1.940    using assms unfolding closure_hull by (rule hull_unique)
   1.941  
   1.942 @@ -1125,7 +1270,8 @@
   1.943  proof
   1.944    fix x
   1.945    assume as: "open S" "x \<in> S \<inter> closure T"
   1.946 -  { assume *:"x islimpt T"
   1.947 +  {
   1.948 +    assume *:"x islimpt T"
   1.949      have "x islimpt (S \<inter> T)"
   1.950      proof (rule islimptI)
   1.951        fix A
   1.952 @@ -1134,9 +1280,9 @@
   1.953          by (simp_all add: open_Int)
   1.954        with * obtain y where "y \<in> T" "y \<in> A \<inter> S" "y \<noteq> x"
   1.955          by (rule islimptE)
   1.956 -      hence "y \<in> S \<inter> T" "y \<in> A \<and> y \<noteq> x"
   1.957 +      then have "y \<in> S \<inter> T" "y \<in> A \<and> y \<noteq> x"
   1.958          by simp_all
   1.959 -      thus "\<exists>y\<in>(S \<inter> T). y \<in> A \<and> y \<noteq> x" ..
   1.960 +      then show "\<exists>y\<in>(S \<inter> T). y \<in> A \<and> y \<noteq> x" ..
   1.961      qed
   1.962    }
   1.963    then show "x \<in> closure (S \<inter> T)" using as
   1.964 @@ -1167,7 +1313,6 @@
   1.965      done
   1.966  qed
   1.967  
   1.968 -
   1.969  lemma islimpt_in_closure: "(x islimpt S) = (x:closure(S-{x}))"
   1.970    unfolding closure_def using islimpt_punctured by blast
   1.971  
   1.972 @@ -1176,7 +1321,7 @@
   1.973  
   1.974  definition "frontier S = closure S - interior S"
   1.975  
   1.976 -lemma frontier_closed: "closed(frontier S)"
   1.977 +lemma frontier_closed: "closed (frontier S)"
   1.978    by (simp add: frontier_def closed_Diff)
   1.979  
   1.980  lemma frontier_closures: "frontier S = (closure S) \<inter> (closure(- S))"
   1.981 @@ -1196,11 +1341,14 @@
   1.982  
   1.983  lemma frontier_subset_eq: "frontier S \<subseteq> S \<longleftrightarrow> closed S"
   1.984  proof-
   1.985 -  { assume "frontier S \<subseteq> S"
   1.986 -    hence "closure S \<subseteq> S" using interior_subset unfolding frontier_def by auto
   1.987 -    hence "closed S" using closure_subset_eq by auto
   1.988 +  {
   1.989 +    assume "frontier S \<subseteq> S"
   1.990 +    then have "closure S \<subseteq> S"
   1.991 +      using interior_subset unfolding frontier_def by auto
   1.992 +    then have "closed S"
   1.993 +      using closure_subset_eq by auto
   1.994    }
   1.995 -  thus ?thesis using frontier_subset_closed[of S] ..
   1.996 +  then show ?thesis using frontier_subset_closed[of S] ..
   1.997  qed
   1.998  
   1.999  lemma frontier_complement: "frontier(- S) = frontier S"
  1.1000 @@ -1221,7 +1369,7 @@
  1.1001  lemma trivial_limit_within: "trivial_limit (at a within S) \<longleftrightarrow> \<not> a islimpt S"
  1.1002  proof
  1.1003    assume "trivial_limit (at a within S)"
  1.1004 -  thus "\<not> a islimpt S"
  1.1005 +  then show "\<not> a islimpt S"
  1.1006      unfolding trivial_limit_def
  1.1007      unfolding eventually_at_topological
  1.1008      unfolding islimpt_def
  1.1009 @@ -1231,7 +1379,7 @@
  1.1010      done
  1.1011  next
  1.1012    assume "\<not> a islimpt S"
  1.1013 -  thus "trivial_limit (at a within S)"
  1.1014 +  then show "trivial_limit (at a within S)"
  1.1015      unfolding trivial_limit_def
  1.1016      unfolding eventually_at_topological
  1.1017      unfolding islimpt_def
  1.1018 @@ -1266,9 +1414,9 @@
  1.1019  
  1.1020  lemma eventually_at2:
  1.1021    "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
  1.1022 -unfolding eventually_at dist_nz by auto
  1.1023 -
  1.1024 -lemma eventually_happens: "eventually P net ==> trivial_limit net \<or> (\<exists>x. P x)"
  1.1025 +  unfolding eventually_at dist_nz by auto
  1.1026 +
  1.1027 +lemma eventually_happens: "eventually P net \<Longrightarrow> trivial_limit net \<or> (\<exists>x. P x)"
  1.1028    unfolding trivial_limit_def
  1.1029    by (auto elim: eventually_rev_mp)
  1.1030  
  1.1031 @@ -1282,7 +1430,7 @@
  1.1032  
  1.1033  lemma eventually_rev_mono:
  1.1034    "eventually P net \<Longrightarrow> (\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually Q net"
  1.1035 -using eventually_mono [of P Q] by fast
  1.1036 +  using eventually_mono [of P Q] by fast
  1.1037  
  1.1038  lemma not_eventually: "(\<forall>x. \<not> P x ) \<Longrightarrow> ~(trivial_limit net) ==> ~(eventually (\<lambda>x. P x) net)"
  1.1039    by (simp add: eventually_False)
  1.1040 @@ -1291,7 +1439,7 @@
  1.1041  subsection {* Limits *}
  1.1042  
  1.1043  lemma Lim:
  1.1044 - "(f ---> l) net \<longleftrightarrow>
  1.1045 +  "(f ---> l) net \<longleftrightarrow>
  1.1046          trivial_limit net \<or>
  1.1047          (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
  1.1048    unfolding tendsto_iff trivial_limit_eq by auto
  1.1049 @@ -1322,7 +1470,8 @@
  1.1050  lemma Lim_within_empty: "(f ---> l) (at x within {})"
  1.1051    unfolding tendsto_def eventually_at_filter by simp
  1.1052  
  1.1053 -lemma Lim_Un: assumes "(f ---> l) (at x within S)" "(f ---> l) (at x within T)"
  1.1054 +lemma Lim_Un:
  1.1055 +  assumes "(f ---> l) (at x within S)" "(f ---> l) (at x within T)"
  1.1056    shows "(f ---> l) (at x within (S \<union> T))"
  1.1057    using assms unfolding tendsto_def eventually_at_filter
  1.1058    apply clarify
  1.1059 @@ -1332,36 +1481,36 @@
  1.1060    done
  1.1061  
  1.1062  lemma Lim_Un_univ:
  1.1063 - "(f ---> l) (at x within S) \<Longrightarrow> (f ---> l) (at x within T) \<Longrightarrow>  S \<union> T = UNIV
  1.1064 -        ==> (f ---> l) (at x)"
  1.1065 +  "(f ---> l) (at x within S) \<Longrightarrow> (f ---> l) (at x within T) \<Longrightarrow>  
  1.1066 +    S \<union> T = UNIV \<Longrightarrow> (f ---> l) (at x)"
  1.1067    by (metis Lim_Un)
  1.1068  
  1.1069  text{* Interrelations between restricted and unrestricted limits. *}
  1.1070  
  1.1071 -
  1.1072  lemma Lim_at_within: (* FIXME: rename *)
  1.1073    "(f ---> l) (at x) \<Longrightarrow> (f ---> l) (at x within S)"
  1.1074    by (metis order_refl filterlim_mono subset_UNIV at_le)
  1.1075  
  1.1076  lemma eventually_within_interior:
  1.1077    assumes "x \<in> interior S"
  1.1078 -  shows "eventually P (at x within S) \<longleftrightarrow> eventually P (at x)" (is "?lhs = ?rhs")
  1.1079 -proof -
  1.1080 +  shows "eventually P (at x within S) \<longleftrightarrow> eventually P (at x)"
  1.1081 +  (is "?lhs = ?rhs")
  1.1082 +proof
  1.1083    from assms obtain T where T: "open T" "x \<in> T" "T \<subseteq> S" ..
  1.1084 -  { assume "?lhs"
  1.1085 +  {
  1.1086 +    assume "?lhs"
  1.1087      then obtain A where "open A" "x \<in> A" "\<forall>y\<in>A. y \<noteq> x \<longrightarrow> y \<in> S \<longrightarrow> P y"
  1.1088        unfolding eventually_at_topological
  1.1089        by auto
  1.1090      with T have "open (A \<inter> T)" "x \<in> A \<inter> T" "\<forall>y\<in>(A \<inter> T). y \<noteq> x \<longrightarrow> P y"
  1.1091        by auto
  1.1092 -    then have "?rhs"
  1.1093 +    then show "?rhs"
  1.1094        unfolding eventually_at_topological by auto
  1.1095 -  }
  1.1096 -  moreover
  1.1097 -  { assume "?rhs" hence "?lhs"
  1.1098 +  next
  1.1099 +    assume "?rhs"
  1.1100 +    then show "?lhs"
  1.1101        by (auto elim: eventually_elim1 simp: eventually_at_filter)
  1.1102    }
  1.1103 -  ultimately show "?thesis" ..
  1.1104  qed
  1.1105  
  1.1106  lemma at_within_interior:
  1.1107 @@ -1379,24 +1528,31 @@
  1.1108    fixes f :: "'a :: {linorder_topology, conditionally_complete_linorder, no_top} \<Rightarrow>
  1.1109      'b::{linorder_topology, conditionally_complete_linorder}"
  1.1110    assumes mono: "\<And>a b. a \<in> I \<Longrightarrow> b \<in> I \<Longrightarrow> x < a \<Longrightarrow> a \<le> b \<Longrightarrow> f a \<le> f b"
  1.1111 -  assumes bnd: "\<And>a. a \<in> I \<Longrightarrow> x < a \<Longrightarrow> K \<le> f a"
  1.1112 +    and bnd: "\<And>a. a \<in> I \<Longrightarrow> x < a \<Longrightarrow> K \<le> f a"
  1.1113    shows "(f ---> Inf (f ` ({x<..} \<inter> I))) (at x within ({x<..} \<inter> I))"
  1.1114  proof cases
  1.1115 -  assume "{x<..} \<inter> I = {}" then show ?thesis by (simp add: Lim_within_empty)
  1.1116 +  assume "{x<..} \<inter> I = {}"
  1.1117 +  then show ?thesis by (simp add: Lim_within_empty)
  1.1118  next
  1.1119    assume e: "{x<..} \<inter> I \<noteq> {}"
  1.1120    show ?thesis
  1.1121    proof (rule order_tendstoI)
  1.1122      fix a assume a: "a < Inf (f ` ({x<..} \<inter> I))"
  1.1123 -    { fix y assume "y \<in> {x<..} \<inter> I"
  1.1124 +    {
  1.1125 +      fix y
  1.1126 +      assume "y \<in> {x<..} \<inter> I"
  1.1127        with e bnd have "Inf (f ` ({x<..} \<inter> I)) \<le> f y"
  1.1128          by (auto intro: cInf_lower)
  1.1129 -      with a have "a < f y" by (blast intro: less_le_trans) }
  1.1130 +      with a have "a < f y"
  1.1131 +        by (blast intro: less_le_trans)
  1.1132 +    }
  1.1133      then show "eventually (\<lambda>x. a < f x) (at x within ({x<..} \<inter> I))"
  1.1134        by (auto simp: eventually_at_filter intro: exI[of _ 1] zero_less_one)
  1.1135    next
  1.1136 -    fix a assume "Inf (f ` ({x<..} \<inter> I)) < a"
  1.1137 -    from cInf_lessD[OF _ this] e obtain y where y: "x < y" "y \<in> I" "f y < a" by auto
  1.1138 +    fix a
  1.1139 +    assume "Inf (f ` ({x<..} \<inter> I)) < a"
  1.1140 +    from cInf_lessD[OF _ this] e obtain y where y: "x < y" "y \<in> I" "f y < a"
  1.1141 +      by auto
  1.1142      then have "eventually (\<lambda>x. x \<in> I \<longrightarrow> f x < a) (at_right x)"
  1.1143        unfolding eventually_at_right by (metis less_imp_le le_less_trans mono)
  1.1144      then show "eventually (\<lambda>x. f x < a) (at x within ({x<..} \<inter> I))"
  1.1145 @@ -1414,27 +1570,33 @@
  1.1146    assume ?lhs
  1.1147    from countable_basis_at_decseq[of x] guess A . note A = this
  1.1148    def f \<equiv> "\<lambda>n. SOME y. y \<in> S \<and> y \<in> A n \<and> x \<noteq> y"
  1.1149 -  { fix n
  1.1150 +  {
  1.1151 +    fix n
  1.1152      from `?lhs` have "\<exists>y. y \<in> S \<and> y \<in> A n \<and> x \<noteq> y"
  1.1153        unfolding islimpt_def using A(1,2)[of n] by auto
  1.1154      then have "f n \<in> S \<and> f n \<in> A n \<and> x \<noteq> f n"
  1.1155        unfolding f_def by (rule someI_ex)
  1.1156 -    then have "f n \<in> S" "f n \<in> A n" "x \<noteq> f n" by auto }
  1.1157 +    then have "f n \<in> S" "f n \<in> A n" "x \<noteq> f n" by auto
  1.1158 +  }
  1.1159    then have "\<forall>n. f n \<in> S - {x}" by auto
  1.1160    moreover have "(\<lambda>n. f n) ----> x"
  1.1161    proof (rule topological_tendstoI)
  1.1162 -    fix S assume "open S" "x \<in> S"
  1.1163 +    fix S
  1.1164 +    assume "open S" "x \<in> S"
  1.1165      from A(3)[OF this] `\<And>n. f n \<in> A n`
  1.1166 -    show "eventually (\<lambda>x. f x \<in> S) sequentially" by (auto elim!: eventually_elim1)
  1.1167 +    show "eventually (\<lambda>x. f x \<in> S) sequentially"
  1.1168 +      by (auto elim!: eventually_elim1)
  1.1169    qed
  1.1170    ultimately show ?rhs by fast
  1.1171  next
  1.1172    assume ?rhs
  1.1173 -  then obtain f :: "nat \<Rightarrow> 'a" where f: "\<And>n. f n \<in> S - {x}" and lim: "f ----> x" by auto
  1.1174 +  then obtain f :: "nat \<Rightarrow> 'a" where f: "\<And>n. f n \<in> S - {x}" and lim: "f ----> x"
  1.1175 +    by auto
  1.1176    show ?lhs
  1.1177      unfolding islimpt_def
  1.1178    proof safe
  1.1179 -    fix T assume "open T" "x \<in> T"
  1.1180 +    fix T
  1.1181 +    assume "open T" "x \<in> T"
  1.1182      from lim[THEN topological_tendstoD, OF this] f
  1.1183      show "\<exists>y\<in>S. y \<in> T \<and> y \<noteq> x"
  1.1184        unfolding eventually_sequentially by auto
  1.1185 @@ -1442,8 +1604,10 @@
  1.1186  qed
  1.1187  
  1.1188  lemma Lim_inv: (* TODO: delete *)
  1.1189 -  fixes f :: "'a \<Rightarrow> real" and A :: "'a filter"
  1.1190 -  assumes "(f ---> l) A" and "l \<noteq> 0"
  1.1191 +  fixes f :: "'a \<Rightarrow> real"
  1.1192 +    and A :: "'a filter"
  1.1193 +  assumes "(f ---> l) A"
  1.1194 +    and "l \<noteq> 0"
  1.1195    shows "((inverse o f) ---> inverse l) A"
  1.1196    unfolding o_def using assms by (rule tendsto_inverse)
  1.1197  
  1.1198 @@ -1459,13 +1623,14 @@
  1.1199  proof (rule metric_tendsto_imp_tendsto)
  1.1200    show "(g ---> 0) net" by fact
  1.1201    show "eventually (\<lambda>x. dist (f x) 0 \<le> dist (g x) 0) net"
  1.1202 -    using assms(1) by (rule eventually_elim1, simp add: dist_norm)
  1.1203 +    using assms(1) by (rule eventually_elim1) (simp add: dist_norm)
  1.1204  qed
  1.1205  
  1.1206  lemma Lim_transform_bound:
  1.1207    fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
  1.1208 -  fixes g :: "'a \<Rightarrow> 'c::real_normed_vector"
  1.1209 -  assumes "eventually (\<lambda>n. norm(f n) <= norm(g n)) net"  "(g ---> 0) net"
  1.1210 +    and g :: "'a \<Rightarrow> 'c::real_normed_vector"
  1.1211 +  assumes "eventually (\<lambda>n. norm(f n) <= norm(g n)) net"
  1.1212 +    and "(g ---> 0) net"
  1.1213    shows "(f ---> 0) net"
  1.1214    using assms(1) tendsto_norm_zero [OF assms(2)]
  1.1215    by (rule Lim_null_comparison)
  1.1216 @@ -1473,7 +1638,9 @@
  1.1217  text{* Deducing things about the limit from the elements. *}
  1.1218  
  1.1219  lemma Lim_in_closed_set:
  1.1220 -  assumes "closed S" "eventually (\<lambda>x. f(x) \<in> S) net" "\<not>(trivial_limit net)" "(f ---> l) net"
  1.1221 +  assumes "closed S"
  1.1222 +    and "eventually (\<lambda>x. f(x) \<in> S) net"
  1.1223 +    and "\<not>(trivial_limit net)" "(f ---> l) net"
  1.1224    shows "l \<in> S"
  1.1225  proof (rule ccontr)
  1.1226    assume "l \<notin> S"
  1.1227 @@ -1490,32 +1657,42 @@
  1.1228  text{* Need to prove closed(cball(x,e)) before deducing this as a corollary. *}
  1.1229  
  1.1230  lemma Lim_dist_ubound:
  1.1231 -  assumes "\<not>(trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. dist a (f x) <= e) net"
  1.1232 +  assumes "\<not>(trivial_limit net)"
  1.1233 +    and "(f ---> l) net"
  1.1234 +    and "eventually (\<lambda>x. dist a (f x) <= e) net"
  1.1235    shows "dist a l <= e"
  1.1236  proof -
  1.1237    have "dist a l \<in> {..e}"
  1.1238    proof (rule Lim_in_closed_set)
  1.1239 -    show "closed {..e}" by simp
  1.1240 -    show "eventually (\<lambda>x. dist a (f x) \<in> {..e}) net" by (simp add: assms)
  1.1241 -    show "\<not> trivial_limit net" by fact
  1.1242 -    show "((\<lambda>x. dist a (f x)) ---> dist a l) net" by (intro tendsto_intros assms)
  1.1243 +    show "closed {..e}"
  1.1244 +      by simp
  1.1245 +    show "eventually (\<lambda>x. dist a (f x) \<in> {..e}) net"
  1.1246 +      by (simp add: assms)
  1.1247 +    show "\<not> trivial_limit net"
  1.1248 +      by fact
  1.1249 +    show "((\<lambda>x. dist a (f x)) ---> dist a l) net"
  1.1250 +      by (intro tendsto_intros assms)
  1.1251    qed
  1.1252 -  thus ?thesis by simp
  1.1253 +  then show ?thesis by simp
  1.1254  qed
  1.1255  
  1.1256  lemma Lim_norm_ubound:
  1.1257    fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
  1.1258 -  assumes "\<not>(trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. norm(f x) <= e) net"
  1.1259 -  shows "norm(l) <= e"
  1.1260 +  assumes "\<not>(trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. norm(f x) \<le> e) net"
  1.1261 +  shows "norm(l) \<le> e"
  1.1262  proof -
  1.1263    have "norm l \<in> {..e}"
  1.1264    proof (rule Lim_in_closed_set)
  1.1265 -    show "closed {..e}" by simp
  1.1266 -    show "eventually (\<lambda>x. norm (f x) \<in> {..e}) net" by (simp add: assms)
  1.1267 -    show "\<not> trivial_limit net" by fact
  1.1268 -    show "((\<lambda>x. norm (f x)) ---> norm l) net" by (intro tendsto_intros assms)
  1.1269 +    show "closed {..e}"
  1.1270 +      by simp
  1.1271 +    show "eventually (\<lambda>x. norm (f x) \<in> {..e}) net"
  1.1272 +      by (simp add: assms)
  1.1273 +    show "\<not> trivial_limit net"
  1.1274 +      by fact
  1.1275 +    show "((\<lambda>x. norm (f x)) ---> norm l) net"
  1.1276 +      by (intro tendsto_intros assms)
  1.1277    qed
  1.1278 -  thus ?thesis by simp
  1.1279 +  then show ?thesis by simp
  1.1280  qed
  1.1281  
  1.1282  lemma Lim_norm_lbound:
  1.1283 @@ -1525,12 +1702,16 @@
  1.1284  proof -
  1.1285    have "norm l \<in> {e..}"
  1.1286    proof (rule Lim_in_closed_set)
  1.1287 -    show "closed {e..}" by simp
  1.1288 -    show "eventually (\<lambda>x. norm (f x) \<in> {e..}) net" by (simp add: assms)
  1.1289 -    show "\<not> trivial_limit net" by fact
  1.1290 -    show "((\<lambda>x. norm (f x)) ---> norm l) net" by (intro tendsto_intros assms)
  1.1291 +    show "closed {e..}"
  1.1292 +      by simp
  1.1293 +    show "eventually (\<lambda>x. norm (f x) \<in> {e..}) net"
  1.1294 +      by (simp add: assms)
  1.1295 +    show "\<not> trivial_limit net"
  1.1296 +      by fact
  1.1297 +    show "((\<lambda>x. norm (f x)) ---> norm l) net"
  1.1298 +      by (intro tendsto_intros assms)
  1.1299    qed
  1.1300 -  thus ?thesis by simp
  1.1301 +  then show ?thesis by simp
  1.1302  qed
  1.1303  
  1.1304  text{* Limit under bilinear function *}