# HG changeset patch
# User wenzelm
# Date 1377728282 -7200
# Node ID addd7b9b2bff8bd30f99b9273711ea4f3001815b
# Parent  082d0972096bb8b9c922b111fc889d739e9fbc15
tuned proofs;

diff -r 082d0972096b -r addd7b9b2bff src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 28 23:48:45 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Aug 29 00:18:02 2013 +0200
@@ -49,6 +49,7 @@
     continuous_on (s \<union> t) (\<lambda>x. if P x then f x else g x)"
   by (rule continuous_on_If) auto
 
+
 subsection {* Topological Basis *}
 
 context topological_space
@@ -117,41 +118,51 @@
   by (simp add: topological_basis_def)
 
 lemma topological_basis_imp_subbasis:
-  assumes B: "topological_basis B" shows "open = generate_topology B"
+  assumes B: "topological_basis B"
+  shows "open = generate_topology B"
 proof (intro ext iffI)
-  fix S :: "'a set" assume "open S"
+  fix S :: "'a set"
+  assume "open S"
   with B obtain B' where "B' \<subseteq> B" "S = \<Union>B'"
     unfolding topological_basis_def by blast
   then show "generate_topology B S"
     by (auto intro: generate_topology.intros dest: topological_basis_open)
 next
-  fix S :: "'a set" assume "generate_topology B S" then show "open S"
+  fix S :: "'a set"
+  assume "generate_topology B S"
+  then show "open S"
     by induct (auto dest: topological_basis_open[OF B])
 qed
 
 lemma basis_dense:
-  fixes B::"'a set set" and f::"'a set \<Rightarrow> 'a"
+  fixes B::"'a set set"
+    and f::"'a set \<Rightarrow> 'a"
   assumes "topological_basis B"
-  assumes choosefrom_basis: "\<And>B'. B' \<noteq> {} \<Longrightarrow> f B' \<in> B'"
+    and choosefrom_basis: "\<And>B'. B' \<noteq> {} \<Longrightarrow> f B' \<in> B'"
   shows "(\<forall>X. open X \<longrightarrow> X \<noteq> {} \<longrightarrow> (\<exists>B' \<in> B. f B' \<in> X))"
 proof (intro allI impI)
-  fix X::"'a set" assume "open X" "X \<noteq> {}"
+  fix X::"'a set"
+  assume "open X" "X \<noteq> {}"
   from topological_basisE[OF `topological_basis B` `open X` choosefrom_basis[OF `X \<noteq> {}`]]
   guess B' . note B' = this
-  thus "\<exists>B'\<in>B. f B' \<in> X" by (auto intro!: choosefrom_basis)
+  then show "\<exists>B'\<in>B. f B' \<in> X"
+    by (auto intro!: choosefrom_basis)
 qed
 
 end
 
 lemma topological_basis_prod:
-  assumes A: "topological_basis A" and B: "topological_basis B"
+  assumes A: "topological_basis A"
+    and B: "topological_basis B"
   shows "topological_basis ((\<lambda>(a, b). a \<times> b) ` (A \<times> B))"
   unfolding topological_basis_def
 proof (safe, simp_all del: ex_simps add: subset_image_iff ex_simps(1)[symmetric])
-  fix S :: "('a \<times> 'b) set" assume "open S"
+  fix S :: "('a \<times> 'b) set"
+  assume "open S"
   then show "\<exists>X\<subseteq>A \<times> B. (\<Union>(a,b)\<in>X. a \<times> b) = S"
   proof (safe intro!: exI[of _ "{x\<in>A \<times> B. fst x \<times> snd x \<subseteq> S}"])
-    fix x y assume "(x, y) \<in> S"
+    fix x y
+    assume "(x, y) \<in> S"
     from open_prod_elim[OF `open S` this]
     obtain a b where a: "open a""x \<in> a" and b: "open b" "y \<in> b" and "a \<times> b \<subseteq> S"
       by (metis mem_Sigma_iff)
@@ -162,6 +173,7 @@
   qed auto
 qed (metis A B topological_basis_open open_Times)
 
+
 subsection {* Countable Basis *}
 
 locale countable_basis =
@@ -173,12 +185,14 @@
 lemma open_countable_basis_ex:
   assumes "open X"
   shows "\<exists>B' \<subseteq> B. X = Union B'"
-  using assms countable_basis is_basis unfolding topological_basis_def by blast
+  using assms countable_basis is_basis
+  unfolding topological_basis_def by blast
 
 lemma open_countable_basisE:
   assumes "open X"
   obtains B' where "B' \<subseteq> B" "X = Union B'"
-  using assms open_countable_basis_ex by (atomize_elim) simp
+  using assms open_countable_basis_ex
+  by (atomize_elim) simp
 
 lemma countable_dense_exists:
   shows "\<exists>D::'a set. countable D \<and> (\<forall>X. open X \<longrightarrow> X \<noteq> {} \<longrightarrow> (\<exists>d \<in> D. d \<in> X))"
@@ -213,34 +227,47 @@
 proof atomize_elim
   from first_countable_basisE[of x] guess A' . note A' = this
   def A \<equiv> "(\<lambda>N. \<Inter>((\<lambda>n. from_nat_into A' n) ` N)) ` (Collect finite::nat set set)"
-  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>
+  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>
         (\<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)"
   proof (safe intro!: exI[where x=A])
-    show "countable A" unfolding A_def by (intro countable_image countable_Collect_finite)
-    fix a assume "a \<in> A"
-    thus "x \<in> a" "open a" using A'(4)[OF open_UNIV] by (auto simp: A_def intro: A' from_nat_into)
+    show "countable A"
+      unfolding A_def by (intro countable_image countable_Collect_finite)
+    fix a
+    assume "a \<in> A"
+    then show "x \<in> a" "open a"
+      using A'(4)[OF open_UNIV] by (auto simp: A_def intro: A' from_nat_into)
   next
     let ?int = "\<lambda>N. \<Inter>(from_nat_into A' ` N)"
-    fix a b assume "a \<in> A" "b \<in> A"
-    then obtain N M where "a = ?int N" "b = ?int M" "finite (N \<union> M)" by (auto simp: A_def)
-    thus "a \<inter> b \<in> A" by (auto simp: A_def intro!: image_eqI[where x="N \<union> M"])
+    fix a b
+    assume "a \<in> A" "b \<in> A"
+    then obtain N M where "a = ?int N" "b = ?int M" "finite (N \<union> M)"
+      by (auto simp: A_def)
+    then show "a \<inter> b \<in> A"
+      by (auto simp: A_def intro!: image_eqI[where x="N \<union> M"])
   next
-    fix S assume "open S" "x \<in> S" then obtain a where a: "a\<in>A'" "a \<subseteq> S" using A' by blast
-    thus "\<exists>a\<in>A. a \<subseteq> S" using a A'
+    fix S
+    assume "open S" "x \<in> S"
+    then obtain a where a: "a\<in>A'" "a \<subseteq> S" using A' by blast
+    then show "\<exists>a\<in>A. a \<subseteq> S" using a A'
       by (intro bexI[where x=a]) (auto simp: A_def intro: image_eqI[where x="{to_nat_on A' a}"])
   qed
 qed
 
 lemma (in topological_space) first_countableI:
-  assumes "countable A" and 1: "\<And>a. a \<in> A \<Longrightarrow> x \<in> a" "\<And>a. a \<in> A \<Longrightarrow> open a"
-   and 2: "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>a\<in>A. a \<subseteq> S"
+  assumes "countable A"
+    and 1: "\<And>a. a \<in> A \<Longrightarrow> x \<in> a" "\<And>a. a \<in> A \<Longrightarrow> open a"
+    and 2: "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>a\<in>A. a \<subseteq> S"
   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))"
 proof (safe intro!: exI[of _ "from_nat_into A"])
+  fix i
   have "A \<noteq> {}" using 2[of UNIV] by auto
-  { fix i show "x \<in> from_nat_into A i" "open (from_nat_into A i)"
-      using range_from_nat_into_subset[OF `A \<noteq> {}`] 1 by auto }
-  { fix S assume "open S" "x\<in>S" from 2[OF this] show "\<exists>i. from_nat_into A i \<subseteq> S"
-      using subset_range_from_nat_into[OF `countable A`] by auto }
+  show "x \<in> from_nat_into A i" "open (from_nat_into A i)"
+    using range_from_nat_into_subset[OF `A \<noteq> {}`] 1 by auto
+next
+  fix S
+  assume "open S" "x\<in>S" from 2[OF this]
+  show "\<exists>i. from_nat_into A i \<subseteq> S"
+    using subset_range_from_nat_into[OF `countable A`] by auto
 qed
 
 instance prod :: (first_countable_topology, first_countable_topology) first_countable_topology
@@ -250,11 +277,13 @@
   from first_countable_basisE[of "snd x"] guess B :: "'b set set" . note B = this
   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))"
   proof (rule first_countableI[of "(\<lambda>(a, b). a \<times> b) ` (A \<times> B)"], safe)
-    fix a b assume x: "a \<in> A" "b \<in> B"
+    fix a b
+    assume x: "a \<in> A" "b \<in> B"
     with A(2, 3)[of a] B(2, 3)[of b] show "x \<in> a \<times> b" "open (a \<times> b)"
       unfolding mem_Times_iff by (auto intro: open_Times)
   next
-    fix S assume "open S" "x \<in> S"
+    fix S
+    assume "open S" "x \<in> S"
     from open_prod_elim[OF this] guess a' b' .
     moreover with A(4)[of a'] B(4)[of b']
     obtain a b where "a \<in> A" "a \<subseteq> a'" "b \<in> B" "b \<subseteq> b'" by auto
@@ -269,18 +298,22 @@
 
 lemma ex_countable_basis: "\<exists>B::'a set set. countable B \<and> topological_basis B"
 proof -
-  from ex_countable_subbasis obtain B where B: "countable B" "open = generate_topology B" by blast
+  from ex_countable_subbasis obtain B where B: "countable B" "open = generate_topology B"
+    by blast
   let ?B = "Inter ` {b. finite b \<and> b \<subseteq> B }"
 
   show ?thesis
   proof (intro exI conjI)
     show "countable ?B"
       by (intro countable_image countable_Collect_finite_subset B)
-    { fix S assume "open S"
+    {
+      fix S
+      assume "open S"
       then have "\<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. (\<Union>b\<in>B'. \<Inter>b) = S"
         unfolding B
       proof induct
-        case UNIV show ?case by (intro exI[of _ "{{}}"]) simp
+        case UNIV
+        show ?case by (intro exI[of _ "{{}}"]) simp
       next
         case (Int a b)
         then obtain x y where x: "a = UNION x Inter" "\<And>i. i \<in> x \<Longrightarrow> finite i \<and> i \<subseteq> B"
@@ -296,7 +329,8 @@
         then show "\<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. UNION B' Inter = \<Union>K"
           by (intro exI[of _ "UNION K k"]) auto
       next
-        case (Basis S) then show ?case
+        case (Basis S)
+        then show ?case
           by (intro exI[of _ "{{S}}"]) auto
       qed
       then have "(\<exists>B'\<subseteq>Inter ` {b. finite b \<and> b \<subseteq> B}. \<Union>B' = S)"
@@ -339,6 +373,7 @@
        (fastforce simp: topological_space_class.topological_basis_def)+
 qed
 
+
 subsection {* Polish spaces *}
 
 text {* Textbooks define Polish spaces as completely metrizable.
@@ -348,7 +383,9 @@
 
 subsection {* General notion of a topology as a value *}
 
-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))"
+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))"
+
 typedef 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"
   morphisms "openin" "topology"
   unfolding istopology_def by blast
@@ -363,16 +400,14 @@
   using topology_inverse[of U] istopology_open_in[of "topology U"] by auto
 
 lemma topology_eq: "T1 = T2 \<longleftrightarrow> (\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S)"
-proof-
-  { assume "T1=T2"
-    hence "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S" by simp }
-  moreover
-  { assume H: "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S"
-    hence "openin T1 = openin T2" by (simp add: fun_eq_iff)
-    hence "topology (openin T1) = topology (openin T2)" by simp
-    hence "T1 = T2" unfolding openin_inverse .
-  }
-  ultimately show ?thesis by blast
+proof
+  assume "T1 = T2"
+  then show "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S" by simp
+next
+  assume H: "\<forall>S. openin T1 S \<longleftrightarrow> openin T2 S"
+  then have "openin T1 = openin T2" by (simp add: fun_eq_iff)
+  then have "topology (openin T1) = topology (openin T2)" by simp
+  then show "T1 = T2" unfolding openin_inverse .
 qed
 
 text{* Infer the "universe" from union of all sets in the topology. *}
@@ -391,7 +426,9 @@
 
 lemma openin_subset[intro]: "openin U S \<Longrightarrow> S \<subseteq> topspace U"
   unfolding topspace_def by blast
-lemma openin_empty[simp]: "openin U {}" by (simp add: openin_clauses)
+
+lemma openin_empty[simp]: "openin U {}"
+  by (simp add: openin_clauses)
 
 lemma openin_Int[intro]: "openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S \<inter> T)"
   using openin_clauses by simp
@@ -402,7 +439,8 @@
 lemma openin_Un[intro]: "openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S \<union> T)"
   using openin_Union[of "{S,T}" U] by auto
 
-lemma openin_topspace[intro, simp]: "openin U (topspace U)" by (simp add: openin_Union topspace_def)
+lemma openin_topspace[intro, simp]: "openin U (topspace U)"
+  by (simp add: openin_Union topspace_def)
 
 lemma openin_subopen: "openin U S \<longleftrightarrow> (\<forall>x \<in> S. \<exists>T. openin U T \<and> x \<in> T \<and> T \<subseteq> S)"
   (is "?lhs \<longleftrightarrow> ?rhs")
@@ -422,42 +460,63 @@
 
 definition "closedin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> openin U (topspace U - S)"
 
-lemma closedin_subset: "closedin U S \<Longrightarrow> S \<subseteq> topspace U" by (metis closedin_def)
-lemma closedin_empty[simp]: "closedin U {}" by (simp add: closedin_def)
-lemma closedin_topspace[intro,simp]:
-  "closedin U (topspace U)" by (simp add: closedin_def)
+lemma closedin_subset: "closedin U S \<Longrightarrow> S \<subseteq> topspace U"
+  by (metis closedin_def)
+
+lemma closedin_empty[simp]: "closedin U {}"
+  by (simp add: closedin_def)
+
+lemma closedin_topspace[intro, simp]: "closedin U (topspace U)"
+  by (simp add: closedin_def)
+
 lemma closedin_Un[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<union> T)"
   by (auto simp add: Diff_Un closedin_def)
 
-lemma Diff_Inter[intro]: "A - \<Inter>S = \<Union> {A - s|s. s\<in>S}" by auto
-lemma closedin_Inter[intro]: assumes Ke: "K \<noteq> {}" and Kc: "\<forall>S \<in>K. closedin U S"
-  shows "closedin U (\<Inter> K)"  using Ke Kc unfolding closedin_def Diff_Inter by auto
+lemma Diff_Inter[intro]: "A - \<Inter>S = \<Union> {A - s|s. s\<in>S}"
+  by auto
+
+lemma closedin_Inter[intro]:
+  assumes Ke: "K \<noteq> {}"
+    and Kc: "\<forall>S \<in>K. closedin U S"
+  shows "closedin U (\<Inter> K)"
+  using Ke Kc unfolding closedin_def Diff_Inter by auto
 
 lemma closedin_Int[intro]: "closedin U S \<Longrightarrow> closedin U T \<Longrightarrow> closedin U (S \<inter> T)"
   using closedin_Inter[of "{S,T}" U] by auto
 
-lemma Diff_Diff_Int: "A - (A - B) = A \<inter> B" by blast
+lemma Diff_Diff_Int: "A - (A - B) = A \<inter> B"
+  by blast
+
 lemma openin_closedin_eq: "openin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> closedin U (topspace U - S)"
   apply (auto simp add: closedin_def Diff_Diff_Int inf_absorb2)
   apply (metis openin_subset subset_eq)
   done
 
-lemma openin_closedin:  "S \<subseteq> topspace U \<Longrightarrow> (openin U S \<longleftrightarrow> closedin U (topspace U - S))"
+lemma openin_closedin: "S \<subseteq> topspace U \<Longrightarrow> (openin U S \<longleftrightarrow> closedin U (topspace U - S))"
   by (simp add: openin_closedin_eq)
 
-lemma openin_diff[intro]: assumes oS: "openin U S" and cT: "closedin U T" shows "openin U (S - T)"
-proof-
+lemma openin_diff[intro]:
+  assumes oS: "openin U S"
+    and cT: "closedin U T"
+  shows "openin U (S - T)"
+proof -
   have "S - T = S \<inter> (topspace U - T)" using openin_subset[of U S]  oS cT
     by (auto simp add: topspace_def openin_subset)
   then show ?thesis using oS cT by (auto simp add: closedin_def)
 qed
 
-lemma closedin_diff[intro]: assumes oS: "closedin U S" and cT: "openin U T" shows "closedin U (S - T)"
-proof-
-  have "S - T = S \<inter> (topspace U - T)" using closedin_subset[of U S]  oS cT
-    by (auto simp add: topspace_def )
-  then show ?thesis using oS cT by (auto simp add: openin_closedin_eq)
-qed
+lemma closedin_diff[intro]:
+  assumes oS: "closedin U S"
+    and cT: "openin U T"
+  shows "closedin U (S - T)"
+proof -
+  have "S - T = S \<inter> (topspace U - T)"
+    using closedin_subset[of U S] oS cT
+    by (auto simp add: topspace_def)
+  then show ?thesis
+    using oS cT by (auto simp add: openin_closedin_eq)
+qed
+
 
 subsubsection {* Subspace topology *}
 
@@ -465,48 +524,59 @@
 
 lemma istopology_subtopology: "istopology (\<lambda>T. \<exists>S. T = S \<inter> V \<and> openin U S)"
   (is "istopology ?L")
-proof-
+proof -
   have "?L {}" by blast
-  {fix A B assume A: "?L A" and B: "?L B"
-    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
-    have "A\<inter>B = (Sa \<inter> Sb) \<inter> V" "openin U (Sa \<inter> Sb)"  using Sa Sb by blast+
-    then have "?L (A \<inter> B)" by blast}
+  {
+    fix A B
+    assume A: "?L A" and B: "?L B"
+    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
+    have "A \<inter> B = (Sa \<inter> Sb) \<inter> V" "openin U (Sa \<inter> Sb)"
+      using Sa Sb by blast+
+    then have "?L (A \<inter> B)" by blast
+  }
   moreover
-  {fix K assume K: "K \<subseteq> Collect ?L"
+  {
+    fix K assume K: "K \<subseteq> Collect ?L"
     have th0: "Collect ?L = (\<lambda>S. S \<inter> V) ` Collect (openin U)"
       apply (rule set_eqI)
       apply (simp add: Ball_def image_iff)
-      by metis
+      apply metis
+      done
     from K[unfolded th0 subset_image_iff]
-    obtain Sk where Sk: "Sk \<subseteq> Collect (openin U)" "K = (\<lambda>S. S \<inter> V) ` Sk" by blast
-    have "\<Union>K = (\<Union>Sk) \<inter> V" using Sk by auto
-    moreover have "openin U (\<Union> Sk)" using Sk by (auto simp add: subset_eq)
-    ultimately have "?L (\<Union>K)" by blast}
+    obtain Sk where Sk: "Sk \<subseteq> Collect (openin U)" "K = (\<lambda>S. S \<inter> V) ` Sk"
+      by blast
+    have "\<Union>K = (\<Union>Sk) \<inter> V"
+      using Sk by auto
+    moreover have "openin U (\<Union> Sk)"
+      using Sk by (auto simp add: subset_eq)
+    ultimately have "?L (\<Union>K)" by blast
+  }
   ultimately show ?thesis
     unfolding subset_eq mem_Collect_eq istopology_def by blast
 qed
 
-lemma openin_subtopology:
-  "openin (subtopology U V) S \<longleftrightarrow> (\<exists> T. (openin U T) \<and> (S = T \<inter> V))"
+lemma openin_subtopology: "openin (subtopology U V) S \<longleftrightarrow> (\<exists>T. openin U T \<and> S = T \<inter> V)"
   unfolding subtopology_def topology_inverse'[OF istopology_subtopology]
   by auto
 
-lemma topspace_subtopology: "topspace(subtopology U V) = topspace U \<inter> V"
+lemma topspace_subtopology: "topspace (subtopology U V) = topspace U \<inter> V"
   by (auto simp add: topspace_def openin_subtopology)
 
-lemma closedin_subtopology:
-  "closedin (subtopology U V) S \<longleftrightarrow> (\<exists>T. closedin U T \<and> S = T \<inter> V)"
+lemma closedin_subtopology: "closedin (subtopology U V) S \<longleftrightarrow> (\<exists>T. closedin U T \<and> S = T \<inter> V)"
   unfolding closedin_def topspace_subtopology
   apply (simp add: openin_subtopology)
   apply (rule iffI)
   apply clarify
   apply (rule_tac x="topspace U - T" in exI)
-  by auto
+  apply auto
+  done
 
 lemma openin_subtopology_refl: "openin (subtopology U V) V \<longleftrightarrow> V \<subseteq> topspace U"
   unfolding openin_subtopology
   apply (rule iffI, clarify)
-  apply (frule openin_subset[of U])  apply blast
+  apply (frule openin_subset[of U])
+  apply blast
   apply (rule exI[where x="topspace U"])
   apply auto
   done
@@ -514,17 +584,28 @@
 lemma subtopology_superset:
   assumes UV: "topspace U \<subseteq> V"
   shows "subtopology U V = U"
-proof-
-  {fix S
-    {fix T assume T: "openin U T" "S = T \<inter> V"
-      from T openin_subset[OF T(1)] UV have eq: "S = T" by blast
-      have "openin U S" unfolding eq using T by blast}
+proof -
+  {
+    fix S
+    {
+      fix T
+      assume T: "openin U T" "S = T \<inter> V"
+      from T openin_subset[OF T(1)] UV have eq: "S = T"
+        by blast
+      have "openin U S"
+        unfolding eq using T by blast
+    }
     moreover
-    {assume S: "openin U S"
-      hence "\<exists>T. openin U T \<and> S = T \<inter> V"
-        using openin_subset[OF S] UV by auto}
-    ultimately have "(\<exists>T. openin U T \<and> S = T \<inter> V) \<longleftrightarrow> openin U S" by blast}
-  then show ?thesis unfolding topology_eq openin_subtopology by blast
+    {
+      assume S: "openin U S"
+      then have "\<exists>T. openin U T \<and> S = T \<inter> V"
+        using openin_subset[OF S] UV by auto
+    }
+    ultimately have "(\<exists>T. openin U T \<and> S = T \<inter> V) \<longleftrightarrow> openin U S"
+      by blast
+  }
+  then show ?thesis
+    unfolding topology_eq openin_subtopology by blast
 qed
 
 lemma subtopology_topspace[simp]: "subtopology U (topspace U) = U"
@@ -533,11 +614,11 @@
 lemma subtopology_UNIV[simp]: "subtopology U UNIV = U"
   by (simp add: subtopology_superset)
 
+
 subsubsection {* The standard Euclidean topology *}
 
-definition
-  euclidean :: "'a::topological_space topology" where
-  "euclidean = topology open"
+definition euclidean :: "'a::topological_space topology"
+  where "euclidean = topology open"
 
 lemma open_openin: "open S \<longleftrightarrow> openin euclidean S"
   unfolding euclidean_def
@@ -549,7 +630,8 @@
 lemma topspace_euclidean: "topspace euclidean = UNIV"
   apply (simp add: topspace_def)
   apply (rule set_eqI)
-  by (auto simp add: open_openin[symmetric])
+  apply (auto simp add: open_openin[symmetric])
+  done
 
 lemma topspace_euclidean_subtopology[simp]: "topspace (subtopology euclidean S) = S"
   by (simp add: topspace_euclidean topspace_subtopology)
@@ -569,10 +651,10 @@
   by (auto simp add: openin_open)
 
 lemma open_openin_trans[trans]:
- "open S \<Longrightarrow> open T \<Longrightarrow> T \<subseteq> S \<Longrightarrow> openin (subtopology euclidean S) T"
+  "open S \<Longrightarrow> open T \<Longrightarrow> T \<subseteq> S \<Longrightarrow> openin (subtopology euclidean S) T"
   by (metis Int_absorb1  openin_open_Int)
 
-lemma open_subset:  "S \<subseteq> T \<Longrightarrow> open S \<Longrightarrow> openin (subtopology euclidean T) S"
+lemma open_subset: "S \<subseteq> T \<Longrightarrow> open S \<Longrightarrow> openin (subtopology euclidean T) S"
   by (auto simp add: openin_open)
 
 lemma closedin_closed: "closedin (subtopology euclidean U) S \<longleftrightarrow> (\<exists>T. closed T \<and> S = U \<inter> T)"
@@ -593,10 +675,12 @@
 
 lemma openin_euclidean_subtopology_iff:
   fixes S U :: "'a::metric_space set"
-  shows "openin (subtopology euclidean U) S
-  \<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")
+  shows "openin (subtopology euclidean U) S \<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")
 proof
-  assume ?lhs thus ?rhs unfolding openin_open open_dist by blast
+  assume ?lhs
+  then show ?rhs unfolding openin_open open_dist by blast
 next
   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}"
   have 1: "\<forall>x\<in>T. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> T"
@@ -620,17 +704,17 @@
 
 text {* These "transitivity" results are handy too *}
 
-lemma openin_trans[trans]: "openin (subtopology euclidean T) S \<Longrightarrow> openin (subtopology euclidean U) T
-  \<Longrightarrow> openin (subtopology euclidean U) S"
+lemma openin_trans[trans]:
+  "openin (subtopology euclidean T) S \<Longrightarrow> openin (subtopology euclidean U) T \<Longrightarrow>
+    openin (subtopology euclidean U) S"
   unfolding open_openin openin_open by blast
 
 lemma openin_open_trans: "openin (subtopology euclidean T) S \<Longrightarrow> open T \<Longrightarrow> open S"
   by (auto simp add: openin_open intro: openin_trans)
 
 lemma closedin_trans[trans]:
- "closedin (subtopology euclidean T) S \<Longrightarrow>
-           closedin (subtopology euclidean U) T
-           ==> closedin (subtopology euclidean U) S"
+  "closedin (subtopology euclidean T) S \<Longrightarrow> closedin (subtopology euclidean U) T \<Longrightarrow>
+    closedin (subtopology euclidean U) S"
   by (auto simp add: closedin_closed closed_closedin closed_Inter Int_assoc)
 
 lemma closedin_closed_trans: "closedin (subtopology euclidean T) S \<Longrightarrow> closed T \<Longrightarrow> closed S"
@@ -639,13 +723,11 @@
 
 subsection {* Open and closed balls *}
 
-definition
-  ball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set" where
-  "ball x e = {y. dist x y < e}"
-
-definition
-  cball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set" where
-  "cball x e = {y. dist x y \<le> e}"
+definition ball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
+  where "ball x e = {y. dist x y < e}"
+
+definition cball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
+  where "cball x e = {y. dist x y \<le> e}"
 
 lemma mem_ball [simp]: "y \<in> ball x e \<longleftrightarrow> dist x y < e"
   by (simp add: ball_def)
@@ -669,20 +751,33 @@
 lemma centre_in_cball: "x \<in> cball x e \<longleftrightarrow> 0 \<le> e"
   by simp
 
-lemma ball_subset_cball[simp,intro]: "ball x e \<subseteq> cball x e" by (simp add: subset_eq)
-lemma subset_ball[intro]: "d <= e ==> ball x d \<subseteq> ball x e" by (simp add: subset_eq)
-lemma subset_cball[intro]: "d <= e ==> cball x d \<subseteq> cball x e" by (simp add: subset_eq)
+lemma ball_subset_cball[simp,intro]: "ball x e \<subseteq> cball x e"
+  by (simp add: subset_eq)
+
+lemma subset_ball[intro]: "d <= e ==> ball x d \<subseteq> ball x e"
+  by (simp add: subset_eq)
+
+lemma subset_cball[intro]: "d <= e ==> cball x d \<subseteq> cball x e"
+  by (simp add: subset_eq)
+
 lemma ball_max_Un: "ball a (max r s) = ball a r \<union> ball a s"
   by (simp add: set_eq_iff) arith
 
 lemma ball_min_Int: "ball a (min r s) = ball a r \<inter> ball a s"
   by (simp add: set_eq_iff)
 
-lemma diff_less_iff: "(a::real) - b > 0 \<longleftrightarrow> a > b"
+lemma diff_less_iff:
+  "(a::real) - b > 0 \<longleftrightarrow> a > b"
   "(a::real) - b < 0 \<longleftrightarrow> a < b"
-  "a - b < c \<longleftrightarrow> a < c +b" "a - b > c \<longleftrightarrow> a > c +b" by arith+
-lemma diff_le_iff: "(a::real) - b \<ge> 0 \<longleftrightarrow> a \<ge> b" "(a::real) - b \<le> 0 \<longleftrightarrow> a \<le> b"
-  "a - b \<le> c \<longleftrightarrow> a \<le> c +b" "a - b \<ge> c \<longleftrightarrow> a \<ge> c +b"  by arith+
+  "a - b < c \<longleftrightarrow> a < c + b" "a - b > c \<longleftrightarrow> a > c + b"
+  by arith+
+
+lemma diff_le_iff:
+  "(a::real) - b \<ge> 0 \<longleftrightarrow> a \<ge> b"
+  "(a::real) - b \<le> 0 \<longleftrightarrow> a \<le> b"
+  "a - b \<le> c \<longleftrightarrow> a \<le> c + b"
+  "a - b \<ge> c \<longleftrightarrow> a \<ge> c + b"
+  by arith+
 
 lemma open_ball[intro, simp]: "open (ball x e)"
   unfolding open_dist ball_def mem_Collect_eq Ball_def
@@ -730,30 +825,41 @@
   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"
 proof -
   def e' \<equiv> "e / (2 * sqrt (real (DIM ('a))))"
-  then have e: "0 < e'" using assms by (auto intro!: divide_pos_pos simp: DIM_positive)
+  then have e: "0 < e'"
+    using assms by (auto intro!: divide_pos_pos simp: DIM_positive)
   have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> y < x \<bullet> i \<and> x \<bullet> i - y < e'" (is "\<forall>i. ?th i")
   proof
-    fix i from Rats_dense_in_real[of "x \<bullet> i - e'" "x \<bullet> i"] e show "?th i" by auto
+    fix i
+    from Rats_dense_in_real[of "x \<bullet> i - e'" "x \<bullet> i"] e
+    show "?th i" by auto
   qed
   from choice[OF this] guess a .. note a = this
   have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> x \<bullet> i < y \<and> y - x \<bullet> i < e'" (is "\<forall>i. ?th i")
   proof
-    fix i from Rats_dense_in_real[of "x \<bullet> i" "x \<bullet> i + e'"] e show "?th i" by auto
+    fix i
+    from Rats_dense_in_real[of "x \<bullet> i" "x \<bullet> i + e'"] e
+    show "?th i" by auto
   qed
   from choice[OF this] guess b .. note b = this
   let ?a = "\<Sum>i\<in>Basis. a i *\<^sub>R i" and ?b = "\<Sum>i\<in>Basis. b i *\<^sub>R i"
   show ?thesis
   proof (rule exI[of _ ?a], rule exI[of _ ?b], safe)
-    fix y :: 'a assume *: "y \<in> box ?a ?b"
+    fix y :: 'a
+    assume *: "y \<in> box ?a ?b"
     have "dist x y = sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<^sup>2)"
       unfolding setL2_def[symmetric] by (rule euclidean_dist_l2)
     also have "\<dots> < sqrt (\<Sum>(i::'a)\<in>Basis. e^2 / real (DIM('a)))"
     proof (rule real_sqrt_less_mono, rule setsum_strict_mono)
-      fix i :: "'a" assume i: "i \<in> Basis"
-      have "a i < y\<bullet>i \<and> y\<bullet>i < b i" using * i by (auto simp: box_def)
-      moreover have "a i < x\<bullet>i" "x\<bullet>i - a i < e'" using a by auto
-      moreover have "x\<bullet>i < b i" "b i - x\<bullet>i < e'" using b by auto
-      ultimately have "\<bar>x\<bullet>i - y\<bullet>i\<bar> < 2 * e'" by auto
+      fix i :: "'a"
+      assume i: "i \<in> Basis"
+      have "a i < y\<bullet>i \<and> y\<bullet>i < b i"
+        using * i by (auto simp: box_def)
+      moreover have "a i < x\<bullet>i" "x\<bullet>i - a i < e'"
+        using a by auto
+      moreover have "x\<bullet>i < b i" "b i - x\<bullet>i < e'"
+        using b by auto
+      ultimately have "\<bar>x\<bullet>i - y\<bullet>i\<bar> < 2 * e'"
+        by auto
       then have "dist (x \<bullet> i) (y \<bullet> i) < e/sqrt (real (DIM('a)))"
         unfolding e'_def by (auto simp: dist_real_def)
       then have "(dist (x \<bullet> i) (y \<bullet> i))\<^sup>2 < (e/sqrt (real (DIM('a))))\<^sup>2"
@@ -761,8 +867,10 @@
       then show "(dist (x \<bullet> i) (y \<bullet> i))\<^sup>2 < e\<^sup>2 / real DIM('a)"
         by (simp add: power_divide)
     qed auto
-    also have "\<dots> = e" using `0 < e` by (simp add: real_eq_of_nat)
-    finally show "y \<in> ball x e" by (auto simp: ball_def)
+    also have "\<dots> = e"
+      using `0 < e` by (simp add: real_eq_of_nat)
+    finally show "y \<in> ball x e"
+      by (auto simp: ball_def)
   qed (insert a b, auto simp: box_def)
 qed
 
@@ -792,51 +900,67 @@
 subsection{* Connectedness *}
 
 lemma connected_local:
- "connected S \<longleftrightarrow> ~(\<exists>e1 e2.
-                 openin (subtopology euclidean S) e1 \<and>
-                 openin (subtopology euclidean S) e2 \<and>
-                 S \<subseteq> e1 \<union> e2 \<and>
-                 e1 \<inter> e2 = {} \<and>
-                 ~(e1 = {}) \<and>
-                 ~(e2 = {}))"
-unfolding connected_def openin_open by (safe, blast+)
+ "connected S \<longleftrightarrow>
+  \<not> (\<exists>e1 e2.
+      openin (subtopology euclidean S) e1 \<and>
+      openin (subtopology euclidean S) e2 \<and>
+      S \<subseteq> e1 \<union> e2 \<and>
+      e1 \<inter> e2 = {} \<and>
+      e1 \<noteq> {} \<and>
+      e2 \<noteq> {})"
+  unfolding connected_def openin_open by (safe, blast+)
 
 lemma exists_diff:
   fixes P :: "'a set \<Rightarrow> bool"
   shows "(\<exists>S. P(- S)) \<longleftrightarrow> (\<exists>S. P S)" (is "?lhs \<longleftrightarrow> ?rhs")
-proof-
-  {assume "?lhs" hence ?rhs by blast }
+proof -
+  {
+    assume "?lhs"
+    then have ?rhs by blast
+  }
   moreover
-  {fix S assume H: "P S"
+  {
+    fix S
+    assume H: "P S"
     have "S = - (- S)" by auto
-    with H have "P (- (- S))" by metis }
+    with H have "P (- (- S))" by metis
+  }
   ultimately show ?thesis by metis
 qed
 
 lemma connected_clopen: "connected S \<longleftrightarrow>
-        (\<forall>T. openin (subtopology euclidean S) T \<and>
-            closedin (subtopology euclidean S) T \<longrightarrow> T = {} \<or> T = S)" (is "?lhs \<longleftrightarrow> ?rhs")
-proof-
-  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> {})"
+  (\<forall>T. openin (subtopology euclidean S) T \<and>
+     closedin (subtopology euclidean S) T \<longrightarrow> T = {} \<or> T = S)" (is "?lhs \<longleftrightarrow> ?rhs")
+proof -
+  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> {})"
     unfolding connected_def openin_open closedin_closed
     apply (subst exists_diff)
     apply blast
     done
-  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> {})"
+  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> {})"
     (is " _ \<longleftrightarrow> \<not> (\<exists>e2 e1. ?P e2 e1)")
     apply (simp add: closed_def)
     apply metis
     done
-
   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'))"
     (is "_ \<longleftrightarrow> \<not> (\<exists>t' t. ?Q t' t)")
     unfolding connected_def openin_open closedin_closed by auto
-  {fix e2
-    {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)"
-        by auto}
-    then have "(\<exists>e1. ?P e2 e1) \<longleftrightarrow> (\<exists>t. ?Q e2 t)" by metis}
-  then have "\<forall>e2. (\<exists>e1. ?P e2 e1) \<longleftrightarrow> (\<exists>t. ?Q e2 t)" by blast
-  then show ?thesis unfolding th0 th1 by simp
+  {
+    fix e2
+    {
+      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)"
+        by auto
+    }
+    then have "(\<exists>e1. ?P e2 e1) \<longleftrightarrow> (\<exists>t. ?Q e2 t)"
+      by metis
+  }
+  then have "\<forall>e2. (\<exists>e1. ?P e2 e1) \<longleftrightarrow> (\<exists>t. ?Q e2 t)"
+    by blast
+  then show ?thesis
+    unfolding th0 th1 by simp
 qed
 
 lemma connected_empty[simp, intro]: "connected {}"  (* FIXME duplicate? *)
@@ -845,9 +969,8 @@
 
 subsection{* Limit points *}
 
-definition (in topological_space)
-  islimpt:: "'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixr "islimpt" 60) 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))"
+definition (in topological_space) islimpt:: "'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixr "islimpt" 60)
+  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))"
 
 lemma islimptI:
   assumes "\<And>T. x \<in> T \<Longrightarrow> open T \<Longrightarrow> \<exists>y\<in>S. y \<in> T \<and> y \<noteq> x"
@@ -862,7 +985,7 @@
 lemma islimpt_iff_eventually: "x islimpt S \<longleftrightarrow> \<not> eventually (\<lambda>y. y \<notin> S) (at x)"
   unfolding islimpt_def eventually_at_topological by auto
 
-lemma islimpt_subset: "\<lbrakk>x islimpt S; S \<subseteq> T\<rbrakk> \<Longrightarrow> x islimpt T"
+lemma islimpt_subset: "x islimpt S \<Longrightarrow> S \<subseteq> T \<Longrightarrow> x islimpt T"
   unfolding islimpt_def by fast
 
 lemma islimpt_approachable:
@@ -892,8 +1015,8 @@
 lemma perfect_choose_dist:
   fixes x :: "'a::{perfect_space, metric_space}"
   shows "0 < r \<Longrightarrow> \<exists>a. a \<noteq> x \<and> dist a x < r"
-using islimpt_UNIV [of x]
-by (simp add: islimpt_approachable)
+  using islimpt_UNIV [of x]
+  by (simp add: islimpt_approachable)
 
 lemma closed_limpt: "closed S \<longleftrightarrow> (\<forall>x. x islimpt S \<longrightarrow> x \<in> S)"
   unfolding closed_def
@@ -907,20 +1030,29 @@
 
 lemma finite_set_avoid:
   fixes a :: "'a::metric_space"
-  assumes fS: "finite S" shows  "\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<longrightarrow> d <= dist a x"
-proof(induct rule: finite_induct[OF fS])
-  case 1 thus ?case by (auto intro: zero_less_one)
+  assumes fS: "finite S"
+  shows  "\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<longrightarrow> d <= dist a x"
+proof (induct rule: finite_induct[OF fS])
+  case 1
+  then show ?case by (auto intro: zero_less_one)
 next
   case (2 x F)
-  from 2 obtain d where d: "d >0" "\<forall>x\<in>F. x\<noteq>a \<longrightarrow> d \<le> dist a x" by blast
-  {assume "x = a" hence ?case using d by auto  }
-  moreover
-  {assume xa: "x\<noteq>a"
+  from 2 obtain d where d: "d >0" "\<forall>x\<in>F. x\<noteq>a \<longrightarrow> d \<le> dist a x"
+    by blast
+  show ?case
+  proof (cases "x = a")
+    case True
+    then show ?thesis using d by auto
+  next
+    case False
     let ?d = "min d (dist a x)"
-    have dp: "?d > 0" using xa d(1) using dist_nz by auto
-    from d have d': "\<forall>x\<in>F. x\<noteq>a \<longrightarrow> ?d \<le> dist a x" by auto
-    with dp xa have ?case by(auto intro!: exI[where x="?d"]) }
-  ultimately show ?case by blast
+    have dp: "?d > 0"
+      using False d(1) using dist_nz by auto
+    from d have d': "\<forall>x\<in>F. x\<noteq>a \<longrightarrow> ?d \<le> dist a x"
+      by auto
+    with dp False show ?thesis
+      by (auto intro!: exI[where x="?d"])
+  qed
 qed
 
 lemma islimpt_Un: "x islimpt (S \<union> T) \<longleftrightarrow> x islimpt S \<or> x islimpt T"
@@ -928,20 +1060,27 @@
 
 lemma discrete_imp_closed:
   fixes S :: "'a::metric_space set"
-  assumes e: "0 < e" and d: "\<forall>x \<in> S. \<forall>y \<in> S. dist y x < e \<longrightarrow> y = x"
+  assumes e: "0 < e"
+    and d: "\<forall>x \<in> S. \<forall>y \<in> S. dist y x < e \<longrightarrow> y = x"
   shows "closed S"
-proof-
-  {fix x assume C: "\<forall>e>0. \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e"
+proof -
+  {
+    fix x
+    assume C: "\<forall>e>0. \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e"
     from e have e2: "e/2 > 0" by arith
-    from C[rule_format, OF e2] obtain y where y: "y \<in> S" "y\<noteq>x" "dist y x < e/2" by blast
+    from C[rule_format, OF e2] obtain y where y: "y \<in> S" "y\<noteq>x" "dist y x < e/2"
+      by blast
     let ?m = "min (e/2) (dist x y) "
-    from e2 y(2) have mp: "?m > 0" by (simp add: dist_nz[THEN sym])
-    from C[rule_format, OF mp] obtain z where z: "z \<in> S" "z\<noteq>x" "dist z x < ?m" by blast
+    from e2 y(2) have mp: "?m > 0"
+      by (simp add: dist_nz[THEN sym])
+    from C[rule_format, OF mp] obtain z where z: "z \<in> S" "z\<noteq>x" "dist z x < ?m"
+      by blast
     have th: "dist z y < e" using z y
       by (intro dist_triangle_lt [where z=x], simp)
     from d[rule_format, OF y(1) z(1) th] y z
     have False by (auto simp add: dist_commute)}
-  then show ?thesis by (metis islimpt_approachable closed_limpt [where 'a='a])
+  then show ?thesis
+    by (metis islimpt_approachable closed_limpt [where 'a='a])
 qed
 
 
@@ -1005,7 +1144,8 @@
 
 lemma interior_limit_point [intro]:
   fixes x :: "'a::perfect_space"
-  assumes x: "x \<in> interior S" shows "x islimpt S"
+  assumes x: "x \<in> interior S"
+  shows "x islimpt S"
   using x islimpt_UNIV [of x]
   unfolding interior_def islimpt_def
   apply (clarsimp, rename_tac T T')
@@ -1014,15 +1154,16 @@
   done
 
 lemma interior_closed_Un_empty_interior:
-  assumes cS: "closed S" and iT: "interior T = {}"
+  assumes cS: "closed S"
+    and iT: "interior T = {}"
   shows "interior (S \<union> T) = interior S"
 proof
   show "interior S \<subseteq> interior (S \<union> T)"
-    by (rule interior_mono, rule Un_upper1)
-next
+    by (rule interior_mono) (rule Un_upper1)
   show "interior (S \<union> T) \<subseteq> interior S"
   proof
-    fix x assume "x \<in> interior (S \<union> T)"
+    fix x
+    assume "x \<in> interior (S \<union> T)"
     then obtain R where "open R" "x \<in> R" "R \<subseteq> S \<union> T" ..
     show "x \<in> interior S"
     proof (rule ccontr)
@@ -1043,14 +1184,17 @@
     by (intro Sigma_mono interior_subset)
   show "open (interior A \<times> interior B)"
     by (intro open_Times open_interior)
-  fix T assume "T \<subseteq> A \<times> B" and "open T" thus "T \<subseteq> interior A \<times> interior B"
+  fix T
+  assume "T \<subseteq> A \<times> B" and "open T"
+  then show "T \<subseteq> interior A \<times> interior B"
   proof (safe)
-    fix x y assume "(x, y) \<in> T"
+    fix x y
+    assume "(x, y) \<in> T"
     then obtain C D where "open C" "open D" "C \<times> D \<subseteq> T" "x \<in> C" "y \<in> D"
       using `open T` unfolding open_prod_def by fast
-    hence "open C" "open D" "C \<subseteq> A" "D \<subseteq> B" "x \<in> C" "y \<in> D"
+    then have "open C" "open D" "C \<subseteq> A" "D \<subseteq> B" "x \<in> C" "y \<in> D"
       using `T \<subseteq> A \<times> B` by auto
-    thus "x \<in> interior A" and "y \<in> interior B"
+    then show "x \<in> interior A" and "y \<in> interior B"
       by (auto intro: interiorI)
   qed
 qed
@@ -1091,8 +1235,9 @@
   unfolding closure_hull by (rule hull_minimal)
 
 lemma closure_unique:
-  assumes "S \<subseteq> T" and "closed T"
-  assumes "\<And>T'. S \<subseteq> T' \<Longrightarrow> closed T' \<Longrightarrow> T \<subseteq> T'"
+  assumes "S \<subseteq> T"
+    and "closed T"
+    and "\<And>T'. S \<subseteq> T' \<Longrightarrow> closed T' \<Longrightarrow> T \<subseteq> T'"
   shows "closure S = T"
   using assms unfolding closure_hull by (rule hull_unique)
 
@@ -1125,7 +1270,8 @@
 proof
   fix x
   assume as: "open S" "x \<in> S \<inter> closure T"
-  { assume *:"x islimpt T"
+  {
+    assume *:"x islimpt T"
     have "x islimpt (S \<inter> T)"
     proof (rule islimptI)
       fix A
@@ -1134,9 +1280,9 @@
         by (simp_all add: open_Int)
       with * obtain y where "y \<in> T" "y \<in> A \<inter> S" "y \<noteq> x"
         by (rule islimptE)
-      hence "y \<in> S \<inter> T" "y \<in> A \<and> y \<noteq> x"
+      then have "y \<in> S \<inter> T" "y \<in> A \<and> y \<noteq> x"
         by simp_all
-      thus "\<exists>y\<in>(S \<inter> T). y \<in> A \<and> y \<noteq> x" ..
+      then show "\<exists>y\<in>(S \<inter> T). y \<in> A \<and> y \<noteq> x" ..
     qed
   }
   then show "x \<in> closure (S \<inter> T)" using as
@@ -1167,7 +1313,6 @@
     done
 qed
 
-
 lemma islimpt_in_closure: "(x islimpt S) = (x:closure(S-{x}))"
   unfolding closure_def using islimpt_punctured by blast
 
@@ -1176,7 +1321,7 @@
 
 definition "frontier S = closure S - interior S"
 
-lemma frontier_closed: "closed(frontier S)"
+lemma frontier_closed: "closed (frontier S)"
   by (simp add: frontier_def closed_Diff)
 
 lemma frontier_closures: "frontier S = (closure S) \<inter> (closure(- S))"
@@ -1196,11 +1341,14 @@
 
 lemma frontier_subset_eq: "frontier S \<subseteq> S \<longleftrightarrow> closed S"
 proof-
-  { assume "frontier S \<subseteq> S"
-    hence "closure S \<subseteq> S" using interior_subset unfolding frontier_def by auto
-    hence "closed S" using closure_subset_eq by auto
+  {
+    assume "frontier S \<subseteq> S"
+    then have "closure S \<subseteq> S"
+      using interior_subset unfolding frontier_def by auto
+    then have "closed S"
+      using closure_subset_eq by auto
   }
-  thus ?thesis using frontier_subset_closed[of S] ..
+  then show ?thesis using frontier_subset_closed[of S] ..
 qed
 
 lemma frontier_complement: "frontier(- S) = frontier S"
@@ -1221,7 +1369,7 @@
 lemma trivial_limit_within: "trivial_limit (at a within S) \<longleftrightarrow> \<not> a islimpt S"
 proof
   assume "trivial_limit (at a within S)"
-  thus "\<not> a islimpt S"
+  then show "\<not> a islimpt S"
     unfolding trivial_limit_def
     unfolding eventually_at_topological
     unfolding islimpt_def
@@ -1231,7 +1379,7 @@
     done
 next
   assume "\<not> a islimpt S"
-  thus "trivial_limit (at a within S)"
+  then show "trivial_limit (at a within S)"
     unfolding trivial_limit_def
     unfolding eventually_at_topological
     unfolding islimpt_def
@@ -1266,9 +1414,9 @@
 
 lemma eventually_at2:
   "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
-unfolding eventually_at dist_nz by auto
-
-lemma eventually_happens: "eventually P net ==> trivial_limit net \<or> (\<exists>x. P x)"
+  unfolding eventually_at dist_nz by auto
+
+lemma eventually_happens: "eventually P net \<Longrightarrow> trivial_limit net \<or> (\<exists>x. P x)"
   unfolding trivial_limit_def
   by (auto elim: eventually_rev_mp)
 
@@ -1282,7 +1430,7 @@
 
 lemma eventually_rev_mono:
   "eventually P net \<Longrightarrow> (\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually Q net"
-using eventually_mono [of P Q] by fast
+  using eventually_mono [of P Q] by fast
 
 lemma not_eventually: "(\<forall>x. \<not> P x ) \<Longrightarrow> ~(trivial_limit net) ==> ~(eventually (\<lambda>x. P x) net)"
   by (simp add: eventually_False)
@@ -1291,7 +1439,7 @@
 subsection {* Limits *}
 
 lemma Lim:
- "(f ---> l) net \<longleftrightarrow>
+  "(f ---> l) net \<longleftrightarrow>
         trivial_limit net \<or>
         (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) net)"
   unfolding tendsto_iff trivial_limit_eq by auto
@@ -1322,7 +1470,8 @@
 lemma Lim_within_empty: "(f ---> l) (at x within {})"
   unfolding tendsto_def eventually_at_filter by simp
 
-lemma Lim_Un: assumes "(f ---> l) (at x within S)" "(f ---> l) (at x within T)"
+lemma Lim_Un:
+  assumes "(f ---> l) (at x within S)" "(f ---> l) (at x within T)"
   shows "(f ---> l) (at x within (S \<union> T))"
   using assms unfolding tendsto_def eventually_at_filter
   apply clarify
@@ -1332,36 +1481,36 @@
   done
 
 lemma Lim_Un_univ:
- "(f ---> l) (at x within S) \<Longrightarrow> (f ---> l) (at x within T) \<Longrightarrow>  S \<union> T = UNIV
-        ==> (f ---> l) (at x)"
+  "(f ---> l) (at x within S) \<Longrightarrow> (f ---> l) (at x within T) \<Longrightarrow>  
+    S \<union> T = UNIV \<Longrightarrow> (f ---> l) (at x)"
   by (metis Lim_Un)
 
 text{* Interrelations between restricted and unrestricted limits. *}
 
-
 lemma Lim_at_within: (* FIXME: rename *)
   "(f ---> l) (at x) \<Longrightarrow> (f ---> l) (at x within S)"
   by (metis order_refl filterlim_mono subset_UNIV at_le)
 
 lemma eventually_within_interior:
   assumes "x \<in> interior S"
-  shows "eventually P (at x within S) \<longleftrightarrow> eventually P (at x)" (is "?lhs = ?rhs")
-proof -
+  shows "eventually P (at x within S) \<longleftrightarrow> eventually P (at x)"
+  (is "?lhs = ?rhs")
+proof
   from assms obtain T where T: "open T" "x \<in> T" "T \<subseteq> S" ..
-  { assume "?lhs"
+  {
+    assume "?lhs"
     then obtain A where "open A" "x \<in> A" "\<forall>y\<in>A. y \<noteq> x \<longrightarrow> y \<in> S \<longrightarrow> P y"
       unfolding eventually_at_topological
       by auto
     with T have "open (A \<inter> T)" "x \<in> A \<inter> T" "\<forall>y\<in>(A \<inter> T). y \<noteq> x \<longrightarrow> P y"
       by auto
-    then have "?rhs"
+    then show "?rhs"
       unfolding eventually_at_topological by auto
-  }
-  moreover
-  { assume "?rhs" hence "?lhs"
+  next
+    assume "?rhs"
+    then show "?lhs"
       by (auto elim: eventually_elim1 simp: eventually_at_filter)
   }
-  ultimately show "?thesis" ..
 qed
 
 lemma at_within_interior:
@@ -1379,24 +1528,31 @@
   fixes f :: "'a :: {linorder_topology, conditionally_complete_linorder, no_top} \<Rightarrow>
     'b::{linorder_topology, conditionally_complete_linorder}"
   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"
-  assumes bnd: "\<And>a. a \<in> I \<Longrightarrow> x < a \<Longrightarrow> K \<le> f a"
+    and bnd: "\<And>a. a \<in> I \<Longrightarrow> x < a \<Longrightarrow> K \<le> f a"
   shows "(f ---> Inf (f ` ({x<..} \<inter> I))) (at x within ({x<..} \<inter> I))"
 proof cases
-  assume "{x<..} \<inter> I = {}" then show ?thesis by (simp add: Lim_within_empty)
+  assume "{x<..} \<inter> I = {}"
+  then show ?thesis by (simp add: Lim_within_empty)
 next
   assume e: "{x<..} \<inter> I \<noteq> {}"
   show ?thesis
   proof (rule order_tendstoI)
     fix a assume a: "a < Inf (f ` ({x<..} \<inter> I))"
-    { fix y assume "y \<in> {x<..} \<inter> I"
+    {
+      fix y
+      assume "y \<in> {x<..} \<inter> I"
       with e bnd have "Inf (f ` ({x<..} \<inter> I)) \<le> f y"
         by (auto intro: cInf_lower)
-      with a have "a < f y" by (blast intro: less_le_trans) }
+      with a have "a < f y"
+        by (blast intro: less_le_trans)
+    }
     then show "eventually (\<lambda>x. a < f x) (at x within ({x<..} \<inter> I))"
       by (auto simp: eventually_at_filter intro: exI[of _ 1] zero_less_one)
   next
-    fix a assume "Inf (f ` ({x<..} \<inter> I)) < a"
-    from cInf_lessD[OF _ this] e obtain y where y: "x < y" "y \<in> I" "f y < a" by auto
+    fix a
+    assume "Inf (f ` ({x<..} \<inter> I)) < a"
+    from cInf_lessD[OF _ this] e obtain y where y: "x < y" "y \<in> I" "f y < a"
+      by auto
     then have "eventually (\<lambda>x. x \<in> I \<longrightarrow> f x < a) (at_right x)"
       unfolding eventually_at_right by (metis less_imp_le le_less_trans mono)
     then show "eventually (\<lambda>x. f x < a) (at x within ({x<..} \<inter> I))"
@@ -1414,27 +1570,33 @@
   assume ?lhs
   from countable_basis_at_decseq[of x] guess A . note A = this
   def f \<equiv> "\<lambda>n. SOME y. y \<in> S \<and> y \<in> A n \<and> x \<noteq> y"
-  { fix n
+  {
+    fix n
     from `?lhs` have "\<exists>y. y \<in> S \<and> y \<in> A n \<and> x \<noteq> y"
       unfolding islimpt_def using A(1,2)[of n] by auto
     then have "f n \<in> S \<and> f n \<in> A n \<and> x \<noteq> f n"
       unfolding f_def by (rule someI_ex)
-    then have "f n \<in> S" "f n \<in> A n" "x \<noteq> f n" by auto }
+    then have "f n \<in> S" "f n \<in> A n" "x \<noteq> f n" by auto
+  }
   then have "\<forall>n. f n \<in> S - {x}" by auto
   moreover have "(\<lambda>n. f n) ----> x"
   proof (rule topological_tendstoI)
-    fix S assume "open S" "x \<in> S"
+    fix S
+    assume "open S" "x \<in> S"
     from A(3)[OF this] `\<And>n. f n \<in> A n`
-    show "eventually (\<lambda>x. f x \<in> S) sequentially" by (auto elim!: eventually_elim1)
+    show "eventually (\<lambda>x. f x \<in> S) sequentially"
+      by (auto elim!: eventually_elim1)
   qed
   ultimately show ?rhs by fast
 next
   assume ?rhs
-  then obtain f :: "nat \<Rightarrow> 'a" where f: "\<And>n. f n \<in> S - {x}" and lim: "f ----> x" by auto
+  then obtain f :: "nat \<Rightarrow> 'a" where f: "\<And>n. f n \<in> S - {x}" and lim: "f ----> x"
+    by auto
   show ?lhs
     unfolding islimpt_def
   proof safe
-    fix T assume "open T" "x \<in> T"
+    fix T
+    assume "open T" "x \<in> T"
     from lim[THEN topological_tendstoD, OF this] f
     show "\<exists>y\<in>S. y \<in> T \<and> y \<noteq> x"
       unfolding eventually_sequentially by auto
@@ -1442,8 +1604,10 @@
 qed
 
 lemma Lim_inv: (* TODO: delete *)
-  fixes f :: "'a \<Rightarrow> real" and A :: "'a filter"
-  assumes "(f ---> l) A" and "l \<noteq> 0"
+  fixes f :: "'a \<Rightarrow> real"
+    and A :: "'a filter"
+  assumes "(f ---> l) A"
+    and "l \<noteq> 0"
   shows "((inverse o f) ---> inverse l) A"
   unfolding o_def using assms by (rule tendsto_inverse)
 
@@ -1459,13 +1623,14 @@
 proof (rule metric_tendsto_imp_tendsto)
   show "(g ---> 0) net" by fact
   show "eventually (\<lambda>x. dist (f x) 0 \<le> dist (g x) 0) net"
-    using assms(1) by (rule eventually_elim1, simp add: dist_norm)
+    using assms(1) by (rule eventually_elim1) (simp add: dist_norm)
 qed
 
 lemma Lim_transform_bound:
   fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
-  fixes g :: "'a \<Rightarrow> 'c::real_normed_vector"
-  assumes "eventually (\<lambda>n. norm(f n) <= norm(g n)) net"  "(g ---> 0) net"
+    and g :: "'a \<Rightarrow> 'c::real_normed_vector"
+  assumes "eventually (\<lambda>n. norm(f n) <= norm(g n)) net"
+    and "(g ---> 0) net"
   shows "(f ---> 0) net"
   using assms(1) tendsto_norm_zero [OF assms(2)]
   by (rule Lim_null_comparison)
@@ -1473,7 +1638,9 @@
 text{* Deducing things about the limit from the elements. *}
 
 lemma Lim_in_closed_set:
-  assumes "closed S" "eventually (\<lambda>x. f(x) \<in> S) net" "\<not>(trivial_limit net)" "(f ---> l) net"
+  assumes "closed S"
+    and "eventually (\<lambda>x. f(x) \<in> S) net"
+    and "\<not>(trivial_limit net)" "(f ---> l) net"
   shows "l \<in> S"
 proof (rule ccontr)
   assume "l \<notin> S"
@@ -1490,32 +1657,42 @@
 text{* Need to prove closed(cball(x,e)) before deducing this as a corollary. *}
 
 lemma Lim_dist_ubound:
-  assumes "\<not>(trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. dist a (f x) <= e) net"
+  assumes "\<not>(trivial_limit net)"
+    and "(f ---> l) net"
+    and "eventually (\<lambda>x. dist a (f x) <= e) net"
   shows "dist a l <= e"
 proof -
   have "dist a l \<in> {..e}"
   proof (rule Lim_in_closed_set)
-    show "closed {..e}" by simp
-    show "eventually (\<lambda>x. dist a (f x) \<in> {..e}) net" by (simp add: assms)
-    show "\<not> trivial_limit net" by fact
-    show "((\<lambda>x. dist a (f x)) ---> dist a l) net" by (intro tendsto_intros assms)
+    show "closed {..e}"
+      by simp
+    show "eventually (\<lambda>x. dist a (f x) \<in> {..e}) net"
+      by (simp add: assms)
+    show "\<not> trivial_limit net"
+      by fact
+    show "((\<lambda>x. dist a (f x)) ---> dist a l) net"
+      by (intro tendsto_intros assms)
   qed
-  thus ?thesis by simp
+  then show ?thesis by simp
 qed
 
 lemma Lim_norm_ubound:
   fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
-  assumes "\<not>(trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. norm(f x) <= e) net"
-  shows "norm(l) <= e"
+  assumes "\<not>(trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. norm(f x) \<le> e) net"
+  shows "norm(l) \<le> e"
 proof -
   have "norm l \<in> {..e}"
   proof (rule Lim_in_closed_set)
-    show "closed {..e}" by simp
-    show "eventually (\<lambda>x. norm (f x) \<in> {..e}) net" by (simp add: assms)
-    show "\<not> trivial_limit net" by fact
-    show "((\<lambda>x. norm (f x)) ---> norm l) net" by (intro tendsto_intros assms)
+    show "closed {..e}"
+      by simp
+    show "eventually (\<lambda>x. norm (f x) \<in> {..e}) net"
+      by (simp add: assms)
+    show "\<not> trivial_limit net"
+      by fact
+    show "((\<lambda>x. norm (f x)) ---> norm l) net"
+      by (intro tendsto_intros assms)
   qed
-  thus ?thesis by simp
+  then show ?thesis by simp
 qed
 
 lemma Lim_norm_lbound:
@@ -1525,12 +1702,16 @@
 proof -
   have "norm l \<in> {e..}"
   proof (rule Lim_in_closed_set)
-    show "closed {e..}" by simp
-    show "eventually (\<lambda>x. norm (f x) \<in> {e..}) net" by (simp add: assms)
-    show "\<not> trivial_limit net" by fact
-    show "((\<lambda>x. norm (f x)) ---> norm l) net" by (intro tendsto_intros assms)
+    show "closed {e..}"
+      by simp
+    show "eventually (\<lambda>x. norm (f x) \<in> {e..}) net"
+      by (simp add: assms)
+    show "\<not> trivial_limit net"
+      by fact
+    show "((\<lambda>x. norm (f x)) ---> norm l) net"
+      by (intro tendsto_intros assms)
   qed
-  thus ?thesis by simp
+  then show ?thesis by simp
 qed
 
 text{* Limit under bilinear function *}