src/HOL/Analysis/Topology_Euclidean_Space.thy
changeset 68120 2f161c6910f7
parent 68072 493b818e8e10
child 68188 2af1f142f855
     1.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sun May 06 23:59:14 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue May 08 10:32:07 2018 +0100
     1.3 @@ -47,19 +47,19 @@
     1.4  lemma support_on_if_subset: "support_on A (\<lambda>x. if P x then a else 0) \<subseteq> {x \<in> A. P x}"
     1.5    by (auto simp: support_on_def)
     1.6  
     1.7 -lemma finite_support[intro]: "finite s \<Longrightarrow> finite (support_on s f)"
     1.8 +lemma finite_support[intro]: "finite S \<Longrightarrow> finite (support_on S f)"
     1.9    unfolding support_on_def by auto
    1.10  
    1.11  (* TODO: is supp_sum really needed? TODO: Generalize to Finite_Set.fold *)
    1.12  definition (in comm_monoid_add) supp_sum :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
    1.13 -  where "supp_sum f s = (\<Sum>x\<in>support_on s f. f x)"
    1.14 +  where "supp_sum f S = (\<Sum>x\<in>support_on S f. f x)"
    1.15  
    1.16  lemma supp_sum_empty[simp]: "supp_sum f {} = 0"
    1.17    unfolding supp_sum_def by auto
    1.18  
    1.19  lemma supp_sum_insert[simp]:
    1.20 -  "finite (support_on s f) \<Longrightarrow>
    1.21 -    supp_sum f (insert x s) = (if x \<in> s then supp_sum f s else f x + supp_sum f s)"
    1.22 +  "finite (support_on S f) \<Longrightarrow>
    1.23 +    supp_sum f (insert x S) = (if x \<in> S then supp_sum f S else f x + supp_sum f S)"
    1.24    by (simp add: supp_sum_def in_support_on insert_absorb)
    1.25  
    1.26  lemma supp_sum_divide_distrib: "supp_sum f A / (r::'a::field) = supp_sum (\<lambda>n. f n / r) A"
    1.27 @@ -70,17 +70,36 @@
    1.28  
    1.29  lemma image_affinity_interval:
    1.30    fixes c :: "'a::ordered_real_vector"
    1.31 -  shows "((\<lambda>x. m *\<^sub>R x + c) ` {a..b}) = (if {a..b}={} then {}
    1.32 -            else if 0 <= m then {m *\<^sub>R a + c .. m  *\<^sub>R b + c}
    1.33 +  shows "((\<lambda>x. m *\<^sub>R x + c) ` {a..b}) = 
    1.34 +           (if {a..b}={} then {}
    1.35 +            else if 0 \<le> m then {m *\<^sub>R a + c .. m  *\<^sub>R b + c}
    1.36              else {m *\<^sub>R b + c .. m *\<^sub>R a + c})"
    1.37 -  apply (case_tac "m=0", force)
    1.38 -  apply (auto simp: scaleR_left_mono)
    1.39 -  apply (rule_tac x="inverse m *\<^sub>R (x-c)" in rev_image_eqI, auto simp: pos_le_divideR_eq le_diff_eq scaleR_left_mono_neg)
    1.40 -  apply (metis diff_le_eq inverse_inverse_eq order.not_eq_order_implies_strict pos_le_divideR_eq positive_imp_inverse_positive)
    1.41 -  apply (rule_tac x="inverse m *\<^sub>R (x-c)" in rev_image_eqI, auto simp: not_le neg_le_divideR_eq diff_le_eq)
    1.42 -  using le_diff_eq scaleR_le_cancel_left_neg
    1.43 -  apply fastforce
    1.44 -  done
    1.45 +         (is "?lhs = ?rhs")
    1.46 +proof (cases "m=0")
    1.47 +  case True
    1.48 +  then show ?thesis
    1.49 +    by force
    1.50 +next
    1.51 +  case False
    1.52 +  show ?thesis
    1.53 +  proof
    1.54 +    show "?lhs \<subseteq> ?rhs"
    1.55 +      by (auto simp: scaleR_left_mono scaleR_left_mono_neg)
    1.56 +    show "?rhs \<subseteq> ?lhs"
    1.57 +    proof (clarsimp, intro conjI impI subsetI)
    1.58 +      show "\<lbrakk>0 \<le> m; a \<le> b; x \<in> {m *\<^sub>R a + c..m *\<^sub>R b + c}\<rbrakk>
    1.59 +            \<Longrightarrow> x \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}" for x
    1.60 +        apply (rule_tac x="inverse m *\<^sub>R (x-c)" in rev_image_eqI)
    1.61 +        using False apply (auto simp: le_diff_eq pos_le_divideRI)
    1.62 +        using diff_le_eq pos_le_divideR_eq by force
    1.63 +      show "\<lbrakk>\<not> 0 \<le> m; a \<le> b;  x \<in> {m *\<^sub>R b + c..m *\<^sub>R a + c}\<rbrakk>
    1.64 +            \<Longrightarrow> x \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}" for x
    1.65 +        apply (rule_tac x="inverse m *\<^sub>R (x-c)" in rev_image_eqI)
    1.66 +        apply (auto simp: diff_le_eq neg_le_divideR_eq)
    1.67 +        using diff_eq_diff_less_eq linordered_field_class.sign_simps(11) minus_diff_eq not_less scaleR_le_cancel_left_neg by fastforce
    1.68 +    qed
    1.69 +  qed
    1.70 +qed
    1.71  
    1.72  lemma countable_PiE:
    1.73    "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (Pi\<^sub>E I F)"
    1.74 @@ -286,78 +305,83 @@
    1.75  end
    1.76  
    1.77  lemma (in first_countable_topology) first_countable_basisE:
    1.78 -  obtains A where "countable A" "\<And>a. a \<in> A \<Longrightarrow> x \<in> a" "\<And>a. a \<in> A \<Longrightarrow> open a"
    1.79 -    "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)"
    1.80 -  using first_countable_basis[of x]
    1.81 -  apply atomize_elim
    1.82 -  apply (elim exE)
    1.83 -  apply (rule_tac x="range A" in exI, auto)
    1.84 -  done
    1.85 +  fixes x :: 'a
    1.86 +  obtains \<A> where "countable \<A>" "\<And>A. A \<in> \<A> \<Longrightarrow> x \<in> A" "\<And>A. A \<in> \<A> \<Longrightarrow> open A"
    1.87 +    "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>A\<in>\<A>. A \<subseteq> S)"
    1.88 +proof -
    1.89 +  obtain \<A> where \<A>: "(\<forall>i::nat. x \<in> \<A> i \<and> open (\<A> i))" "(\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. \<A> i \<subseteq> S))"
    1.90 +    using first_countable_basis[of x] by metis
    1.91 +  show thesis
    1.92 +  proof 
    1.93 +    show "countable (range \<A>)"
    1.94 +      by simp
    1.95 +  qed (use \<A> in auto)
    1.96 +qed
    1.97  
    1.98  lemma (in first_countable_topology) first_countable_basis_Int_stableE:
    1.99 -  obtains A where "countable A" "\<And>a. a \<in> A \<Longrightarrow> x \<in> a" "\<And>a. a \<in> A \<Longrightarrow> open a"
   1.100 -    "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)"
   1.101 -    "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<inter> b \<in> A"
   1.102 +  obtains \<A> where "countable \<A>" "\<And>A. A \<in> \<A> \<Longrightarrow> x \<in> A" "\<And>A. A \<in> \<A> \<Longrightarrow> open A"
   1.103 +    "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>A\<in>\<A>. A \<subseteq> S)"
   1.104 +    "\<And>A B. A \<in> \<A> \<Longrightarrow> B \<in> \<A> \<Longrightarrow> A \<inter> B \<in> \<A>"
   1.105  proof atomize_elim
   1.106 -  obtain A' where A':
   1.107 -    "countable A'"
   1.108 -    "\<And>a. a \<in> A' \<Longrightarrow> x \<in> a"
   1.109 -    "\<And>a. a \<in> A' \<Longrightarrow> open a"
   1.110 -    "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>a\<in>A'. a \<subseteq> S"
   1.111 +  obtain \<B> where \<B>:
   1.112 +    "countable \<B>"
   1.113 +    "\<And>B. B \<in> \<B> \<Longrightarrow> x \<in> B"
   1.114 +    "\<And>B. B \<in> \<B> \<Longrightarrow> open B"
   1.115 +    "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>B\<in>\<B>. B \<subseteq> S"
   1.116      by (rule first_countable_basisE) blast
   1.117 -  define A where [abs_def]:
   1.118 -    "A = (\<lambda>N. \<Inter>((\<lambda>n. from_nat_into A' n) ` N)) ` (Collect finite::nat set set)"
   1.119 -  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.120 -        (\<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.121 -  proof (safe intro!: exI[where x=A])
   1.122 -    show "countable A"
   1.123 -      unfolding A_def by (intro countable_image countable_Collect_finite)
   1.124 -    fix a
   1.125 -    assume "a \<in> A"
   1.126 -    then show "x \<in> a" "open a"
   1.127 -      using A'(4)[OF open_UNIV] by (auto simp: A_def intro: A' from_nat_into)
   1.128 +  define \<A> where [abs_def]:
   1.129 +    "\<A> = (\<lambda>N. \<Inter>((\<lambda>n. from_nat_into \<B> n) ` N)) ` (Collect finite::nat set set)"
   1.130 +  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.131 +        (\<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.132 +  proof (safe intro!: exI[where x=\<A>])
   1.133 +    show "countable \<A>"
   1.134 +      unfolding \<A>_def by (intro countable_image countable_Collect_finite)
   1.135 +    fix A
   1.136 +    assume "A \<in> \<A>"
   1.137 +    then show "x \<in> A" "open A"
   1.138 +      using \<B>(4)[OF open_UNIV] by (auto simp: \<A>_def intro: \<B> from_nat_into)
   1.139    next
   1.140 -    let ?int = "\<lambda>N. \<Inter>(from_nat_into A' ` N)"
   1.141 -    fix a b
   1.142 -    assume "a \<in> A" "b \<in> A"
   1.143 -    then obtain N M where "a = ?int N" "b = ?int M" "finite (N \<union> M)"
   1.144 -      by (auto simp: A_def)
   1.145 -    then show "a \<inter> b \<in> A"
   1.146 -      by (auto simp: A_def intro!: image_eqI[where x="N \<union> M"])
   1.147 +    let ?int = "\<lambda>N. \<Inter>(from_nat_into \<B> ` N)"
   1.148 +    fix A B
   1.149 +    assume "A \<in> \<A>" "B \<in> \<A>"
   1.150 +    then obtain N M where "A = ?int N" "B = ?int M" "finite (N \<union> M)"
   1.151 +      by (auto simp: \<A>_def)
   1.152 +    then show "A \<inter> B \<in> \<A>"
   1.153 +      by (auto simp: \<A>_def intro!: image_eqI[where x="N \<union> M"])
   1.154    next
   1.155      fix S
   1.156      assume "open S" "x \<in> S"
   1.157 -    then obtain a where a: "a\<in>A'" "a \<subseteq> S" using A' by blast
   1.158 -    then show "\<exists>a\<in>A. a \<subseteq> S" using a A'
   1.159 -      by (intro bexI[where x=a]) (auto simp: A_def intro: image_eqI[where x="{to_nat_on A' a}"])
   1.160 +    then obtain a where a: "a\<in>\<B>" "a \<subseteq> S" using \<B> by blast
   1.161 +    then show "\<exists>a\<in>\<A>. a \<subseteq> S" using a \<B>
   1.162 +      by (intro bexI[where x=a]) (auto simp: \<A>_def intro: image_eqI[where x="{to_nat_on \<B> a}"])
   1.163    qed
   1.164  qed
   1.165  
   1.166  lemma (in topological_space) first_countableI:
   1.167 -  assumes "countable A"
   1.168 -    and 1: "\<And>a. a \<in> A \<Longrightarrow> x \<in> a" "\<And>a. a \<in> A \<Longrightarrow> open a"
   1.169 -    and 2: "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>a\<in>A. a \<subseteq> S"
   1.170 -  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.171 -proof (safe intro!: exI[of _ "from_nat_into A"])
   1.172 +  assumes "countable \<A>"
   1.173 +    and 1: "\<And>A. A \<in> \<A> \<Longrightarrow> x \<in> A" "\<And>A. A \<in> \<A> \<Longrightarrow> open A"
   1.174 +    and 2: "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>A\<in>\<A>. A \<subseteq> S"
   1.175 +  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.176 +proof (safe intro!: exI[of _ "from_nat_into \<A>"])
   1.177    fix i
   1.178 -  have "A \<noteq> {}" using 2[of UNIV] by auto
   1.179 -  show "x \<in> from_nat_into A i" "open (from_nat_into A i)"
   1.180 -    using range_from_nat_into_subset[OF \<open>A \<noteq> {}\<close>] 1 by auto
   1.181 +  have "\<A> \<noteq> {}" using 2[of UNIV] by auto
   1.182 +  show "x \<in> from_nat_into \<A> i" "open (from_nat_into \<A> i)"
   1.183 +    using range_from_nat_into_subset[OF \<open>\<A> \<noteq> {}\<close>] 1 by auto
   1.184  next
   1.185    fix S
   1.186    assume "open S" "x\<in>S" from 2[OF this]
   1.187 -  show "\<exists>i. from_nat_into A i \<subseteq> S"
   1.188 -    using subset_range_from_nat_into[OF \<open>countable A\<close>] by auto
   1.189 +  show "\<exists>i. from_nat_into \<A> i \<subseteq> S"
   1.190 +    using subset_range_from_nat_into[OF \<open>countable \<A>\<close>] by auto
   1.191  qed
   1.192  
   1.193  instance prod :: (first_countable_topology, first_countable_topology) first_countable_topology
   1.194  proof
   1.195    fix x :: "'a \<times> 'b"
   1.196 -  obtain A where A:
   1.197 -      "countable A"
   1.198 -      "\<And>a. a \<in> A \<Longrightarrow> fst x \<in> a"
   1.199 -      "\<And>a. a \<in> A \<Longrightarrow> open a"
   1.200 -      "\<And>S. open S \<Longrightarrow> fst x \<in> S \<Longrightarrow> \<exists>a\<in>A. a \<subseteq> S"
   1.201 +  obtain \<A> where \<A>:
   1.202 +      "countable \<A>"
   1.203 +      "\<And>a. a \<in> \<A> \<Longrightarrow> fst x \<in> a"
   1.204 +      "\<And>a. a \<in> \<A> \<Longrightarrow> open a"
   1.205 +      "\<And>S. open S \<Longrightarrow> fst x \<in> S \<Longrightarrow> \<exists>a\<in>\<A>. a \<subseteq> S"
   1.206      by (rule first_countable_basisE[of "fst x"]) blast
   1.207    obtain B where B:
   1.208        "countable B"
   1.209 @@ -365,27 +389,28 @@
   1.210        "\<And>a. a \<in> B \<Longrightarrow> open a"
   1.211        "\<And>S. open S \<Longrightarrow> snd x \<in> S \<Longrightarrow> \<exists>a\<in>B. a \<subseteq> S"
   1.212      by (rule first_countable_basisE[of "snd x"]) blast
   1.213 -  show "\<exists>A::nat \<Rightarrow> ('a \<times> 'b) set.
   1.214 -    (\<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.215 -  proof (rule first_countableI[of "(\<lambda>(a, b). a \<times> b) ` (A \<times> B)"], safe)
   1.216 +  show "\<exists>\<A>::nat \<Rightarrow> ('a \<times> 'b) set.
   1.217 +    (\<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.218 +  proof (rule first_countableI[of "(\<lambda>(a, b). a \<times> b) ` (\<A> \<times> B)"], safe)
   1.219      fix a b
   1.220 -    assume x: "a \<in> A" "b \<in> B"
   1.221 -    with A(2, 3)[of a] B(2, 3)[of b] show "x \<in> a \<times> b" and "open (a \<times> b)"
   1.222 -      unfolding mem_Times_iff
   1.223 -      by (auto intro: open_Times)
   1.224 +    assume x: "a \<in> \<A>" "b \<in> B"
   1.225 +    show "x \<in> a \<times> b" 
   1.226 +      by (simp add: \<A>(2) B(2) mem_Times_iff x)
   1.227 +    show "open (a \<times> b)"
   1.228 +      by (simp add: \<A>(3) B(3) open_Times x)
   1.229    next
   1.230      fix S
   1.231      assume "open S" "x \<in> S"
   1.232      then obtain a' b' where a'b': "open a'" "open b'" "x \<in> a' \<times> b'" "a' \<times> b' \<subseteq> S"
   1.233        by (rule open_prod_elim)
   1.234      moreover
   1.235 -    from a'b' A(4)[of a'] B(4)[of b']
   1.236 -    obtain a b where "a \<in> A" "a \<subseteq> a'" "b \<in> B" "b \<subseteq> b'"
   1.237 +    from a'b' \<A>(4)[of a'] B(4)[of b']
   1.238 +    obtain a b where "a \<in> \<A>" "a \<subseteq> a'" "b \<in> B" "b \<subseteq> b'"
   1.239        by auto
   1.240      ultimately
   1.241 -    show "\<exists>a\<in>(\<lambda>(a, b). a \<times> b) ` (A \<times> B). a \<subseteq> S"
   1.242 +    show "\<exists>a\<in>(\<lambda>(a, b). a \<times> b) ` (\<A> \<times> B). a \<subseteq> S"
   1.243        by (auto intro!: bexI[of _ "a \<times> b"] bexI[of _ a] bexI[of _ b])
   1.244 -  qed (simp add: A B)
   1.245 +  qed (simp add: \<A> B)
   1.246  qed
   1.247  
   1.248  class second_countable_topology = topological_space +
   1.249 @@ -962,61 +987,60 @@
   1.250  qed
   1.251  
   1.252  lemma connected_openin:
   1.253 -      "connected s \<longleftrightarrow>
   1.254 -       ~(\<exists>e1 e2. openin (subtopology euclidean s) e1 \<and>
   1.255 -                 openin (subtopology euclidean s) e2 \<and>
   1.256 -                 s \<subseteq> e1 \<union> e2 \<and> e1 \<inter> e2 = {} \<and> e1 \<noteq> {} \<and> e2 \<noteq> {})"
   1.257 +      "connected S \<longleftrightarrow>
   1.258 +       ~(\<exists>E1 E2. openin (subtopology euclidean S) E1 \<and>
   1.259 +                 openin (subtopology euclidean S) E2 \<and>
   1.260 +                 S \<subseteq> E1 \<union> E2 \<and> E1 \<inter> E2 = {} \<and> E1 \<noteq> {} \<and> E2 \<noteq> {})"
   1.261    apply (simp add: connected_def openin_open disjoint_iff_not_equal, safe)
   1.262    apply (simp_all, blast+)  (* SLOW *)
   1.263    done
   1.264  
   1.265  lemma connected_openin_eq:
   1.266 -      "connected s \<longleftrightarrow>
   1.267 -       ~(\<exists>e1 e2. openin (subtopology euclidean s) e1 \<and>
   1.268 -                 openin (subtopology euclidean s) e2 \<and>
   1.269 -                 e1 \<union> e2 = s \<and> e1 \<inter> e2 = {} \<and>
   1.270 -                 e1 \<noteq> {} \<and> e2 \<noteq> {})"
   1.271 +      "connected S \<longleftrightarrow>
   1.272 +       ~(\<exists>E1 E2. openin (subtopology euclidean S) E1 \<and>
   1.273 +                 openin (subtopology euclidean S) E2 \<and>
   1.274 +                 E1 \<union> E2 = S \<and> E1 \<inter> E2 = {} \<and>
   1.275 +                 E1 \<noteq> {} \<and> E2 \<noteq> {})"
   1.276    apply (simp add: connected_openin, safe, blast)
   1.277    by (metis Int_lower1 Un_subset_iff openin_open subset_antisym)
   1.278  
   1.279  lemma connected_closedin:
   1.280 -      "connected s \<longleftrightarrow>
   1.281 -       ~(\<exists>e1 e2.
   1.282 -             closedin (subtopology euclidean s) e1 \<and>
   1.283 -             closedin (subtopology euclidean s) e2 \<and>
   1.284 -             s \<subseteq> e1 \<union> e2 \<and> e1 \<inter> e2 = {} \<and>
   1.285 -             e1 \<noteq> {} \<and> e2 \<noteq> {})"
   1.286 -proof -
   1.287 -  { fix A B x x'
   1.288 -    assume s_sub: "s \<subseteq> A \<union> B"
   1.289 -       and disj: "A \<inter> B \<inter> s = {}"
   1.290 -       and x: "x \<in> s" "x \<in> B" and x': "x' \<in> s" "x' \<in> A"
   1.291 -       and cl: "closed A" "closed B"
   1.292 -    assume "\<forall>e1. (\<forall>T. closed T \<longrightarrow> e1 \<noteq> s \<inter> T) \<or> (\<forall>e2. e1 \<inter> e2 = {} \<longrightarrow> s \<subseteq> e1 \<union> e2 \<longrightarrow> (\<forall>T. closed T \<longrightarrow> e2 \<noteq> s \<inter> T) \<or> e1 = {} \<or> e2 = {})"
   1.293 -    then have "\<And>C D. s \<inter> C = {} \<or> s \<inter> D = {} \<or> s \<inter> (C \<inter> (s \<inter> D)) \<noteq> {} \<or> \<not> s \<subseteq> s \<inter> (C \<union> D) \<or> \<not> closed C \<or> \<not> closed D"
   1.294 -      by (metis (no_types) Int_Un_distrib Int_assoc)
   1.295 -    moreover have "s \<inter> (A \<inter> B) = {}" "s \<inter> (A \<union> B) = s" "s \<inter> B \<noteq> {}"
   1.296 -      using disj s_sub x by blast+
   1.297 -    ultimately have "s \<inter> A = {}"
   1.298 -      using cl by (metis inf.left_commute inf_bot_right order_refl)
   1.299 -    then have False
   1.300 -      using x' by blast
   1.301 -  } note * = this
   1.302 -  show ?thesis
   1.303 -    apply (simp add: connected_closed closedin_closed)
   1.304 -    apply (safe; simp)
   1.305 -    apply blast
   1.306 -    apply (blast intro: *)
   1.307 -    done
   1.308 +      "connected S \<longleftrightarrow>
   1.309 +       (\<nexists>E1 E2.
   1.310 +        closedin (subtopology euclidean S) E1 \<and>
   1.311 +        closedin (subtopology euclidean S) E2 \<and>
   1.312 +        S \<subseteq> E1 \<union> E2 \<and> E1 \<inter> E2 = {} \<and> E1 \<noteq> {} \<and> E2 \<noteq> {})"
   1.313 +       (is "?lhs = ?rhs")
   1.314 +proof
   1.315 +  assume ?lhs
   1.316 +  then show ?rhs 
   1.317 +    by (auto simp add: connected_closed closedin_closed)
   1.318 +next
   1.319 +  assume R: ?rhs
   1.320 +  then show ?lhs 
   1.321 +  proof (clarsimp simp add: connected_closed closedin_closed)
   1.322 +    fix A B 
   1.323 +    assume s_sub: "S \<subseteq> A \<union> B" "B \<inter> S \<noteq> {}"
   1.324 +      and disj: "A \<inter> B \<inter> S = {}"
   1.325 +      and cl: "closed A" "closed B"
   1.326 +    have "S \<inter> (A \<union> B) = S"
   1.327 +      using s_sub(1) by auto
   1.328 +    have "S - A = B \<inter> S"
   1.329 +      using Diff_subset_conv Un_Diff_Int disj s_sub(1) by auto
   1.330 +    then have "S \<inter> A = {}"
   1.331 +      by (metis Diff_Diff_Int Diff_disjoint Un_Diff_Int R cl closedin_closed_Int inf_commute order_refl s_sub(2))
   1.332 +    then show "A \<inter> S = {}"
   1.333 +      by blast
   1.334 +  qed
   1.335  qed
   1.336  
   1.337  lemma connected_closedin_eq:
   1.338 -      "connected s \<longleftrightarrow>
   1.339 -           ~(\<exists>e1 e2.
   1.340 -                 closedin (subtopology euclidean s) e1 \<and>
   1.341 -                 closedin (subtopology euclidean s) e2 \<and>
   1.342 -                 e1 \<union> e2 = s \<and> e1 \<inter> e2 = {} \<and>
   1.343 -                 e1 \<noteq> {} \<and> e2 \<noteq> {})"
   1.344 +      "connected S \<longleftrightarrow>
   1.345 +           ~(\<exists>E1 E2.
   1.346 +                 closedin (subtopology euclidean S) E1 \<and>
   1.347 +                 closedin (subtopology euclidean S) E2 \<and>
   1.348 +                 E1 \<union> E2 = S \<and> E1 \<inter> E2 = {} \<and>
   1.349 +                 E1 \<noteq> {} \<and> E2 \<noteq> {})"
   1.350    apply (simp add: connected_closedin, safe, blast)
   1.351    by (metis Int_lower1 Un_subset_iff closedin_closed subset_antisym)
   1.352  
   1.353 @@ -1662,100 +1686,48 @@
   1.354      and "box c d \<subseteq> cbox a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i) \<longrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th3)
   1.355      and "box c d \<subseteq> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i) \<longrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th4)
   1.356  proof -
   1.357 -  show ?th1
   1.358 -    unfolding subset_eq and Ball_def and mem_box
   1.359 -    by (auto intro: order_trans)
   1.360 -  show ?th2
   1.361 -    unfolding subset_eq and Ball_def and mem_box
   1.362 -    by (auto intro: le_less_trans less_le_trans order_trans less_imp_le)
   1.363 -  {
   1.364 -    assume as: "box c d \<subseteq> cbox a b" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
   1.365 -    then have "box c d \<noteq> {}"
   1.366 -      unfolding box_eq_empty by auto
   1.367 -    fix i :: 'a
   1.368 -    assume i: "i \<in> Basis"
   1.369 -    (** TODO combine the following two parts as done in the HOL_light version. **)
   1.370 -    {
   1.371 -      let ?x = "(\<Sum>j\<in>Basis. (if j=i then ((min (a\<bullet>j) (d\<bullet>j))+c\<bullet>j)/2 else (c\<bullet>j+d\<bullet>j)/2) *\<^sub>R j)::'a"
   1.372 -      assume as2: "a\<bullet>i > c\<bullet>i"
   1.373 -      {
   1.374 -        fix j :: 'a
   1.375 -        assume j: "j \<in> Basis"
   1.376 -        then have "c \<bullet> j < ?x \<bullet> j \<and> ?x \<bullet> j < d \<bullet> j"
   1.377 -          apply (cases "j = i")
   1.378 -          using as(2)[THEN bspec[where x=j]] i
   1.379 -          apply (auto simp: as2)
   1.380 -          done
   1.381 -      }
   1.382 -      then have "?x\<in>box c d"
   1.383 -        using i unfolding mem_box by auto
   1.384 -      moreover
   1.385 -      have "?x \<notin> cbox a b"
   1.386 -        unfolding mem_box
   1.387 -        apply auto
   1.388 -        apply (rule_tac x=i in bexI)
   1.389 -        using as(2)[THEN bspec[where x=i]] and as2 i
   1.390 -        apply auto
   1.391 -        done
   1.392 -      ultimately have False using as by auto
   1.393 +  let ?lesscd = "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
   1.394 +  let ?lerhs = "\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i"
   1.395 +  show ?th1 ?th2
   1.396 +    by (fastforce simp: mem_box)+
   1.397 +  have acdb: "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i"
   1.398 +    if i: "i \<in> Basis" and box: "box c d \<subseteq> cbox a b" and cd: "\<And>i. i \<in> Basis \<Longrightarrow> c\<bullet>i < d\<bullet>i" for i
   1.399 +  proof -
   1.400 +    have "box c d \<noteq> {}"
   1.401 +      using that
   1.402 +      unfolding box_eq_empty by force
   1.403 +    { let ?x = "(\<Sum>j\<in>Basis. (if j=i then ((min (a\<bullet>j) (d\<bullet>j))+c\<bullet>j)/2 else (c\<bullet>j+d\<bullet>j)/2) *\<^sub>R j)::'a"
   1.404 +      assume *: "a\<bullet>i > c\<bullet>i"
   1.405 +      then have "c \<bullet> j < ?x \<bullet> j \<and> ?x \<bullet> j < d \<bullet> j" if "j \<in> Basis" for j
   1.406 +        using cd that by (fastforce simp add: i *)
   1.407 +      then have "?x \<in> box c d"
   1.408 +        unfolding mem_box by auto
   1.409 +      moreover have "?x \<notin> cbox a b"
   1.410 +        using i cd * by (force simp: mem_box)
   1.411 +      ultimately have False using box by auto
   1.412      }
   1.413 -    then have "a\<bullet>i \<le> c\<bullet>i" by (rule ccontr) auto
   1.414 +    then have "a\<bullet>i \<le> c\<bullet>i" by force
   1.415      moreover
   1.416 -    {
   1.417 -      let ?x = "(\<Sum>j\<in>Basis. (if j=i then ((max (b\<bullet>j) (c\<bullet>j))+d\<bullet>j)/2 else (c\<bullet>j+d\<bullet>j)/2) *\<^sub>R j)::'a"
   1.418 -      assume as2: "b\<bullet>i < d\<bullet>i"
   1.419 -      {
   1.420 -        fix j :: 'a
   1.421 -        assume "j\<in>Basis"
   1.422 -        then have "d \<bullet> j > ?x \<bullet> j \<and> ?x \<bullet> j > c \<bullet> j"
   1.423 -          apply (cases "j = i")
   1.424 -          using as(2)[THEN bspec[where x=j]]
   1.425 -          apply (auto simp: as2)
   1.426 -          done
   1.427 -      }
   1.428 -      then have "?x\<in>box c d"
   1.429 +    { let ?x = "(\<Sum>j\<in>Basis. (if j=i then ((max (b\<bullet>j) (c\<bullet>j))+d\<bullet>j)/2 else (c\<bullet>j+d\<bullet>j)/2) *\<^sub>R j)::'a"
   1.430 +      assume *: "b\<bullet>i < d\<bullet>i"
   1.431 +      then have "d \<bullet> j > ?x \<bullet> j \<and> ?x \<bullet> j > c \<bullet> j" if "j \<in> Basis" for j
   1.432 +        using cd that by (fastforce simp add: i *)
   1.433 +      then have "?x \<in> box c d"
   1.434          unfolding mem_box by auto
   1.435 -      moreover
   1.436 -      have "?x\<notin>cbox a b"
   1.437 -        unfolding mem_box
   1.438 -        apply auto
   1.439 -        apply (rule_tac x=i in bexI)
   1.440 -        using as(2)[THEN bspec[where x=i]] and as2 using i
   1.441 -        apply auto
   1.442 -        done
   1.443 -      ultimately have False using as by auto
   1.444 +      moreover have "?x \<notin> cbox a b"
   1.445 +        using i cd * by (force simp: mem_box)
   1.446 +      ultimately have False using box by auto
   1.447      }
   1.448      then have "b\<bullet>i \<ge> d\<bullet>i" by (rule ccontr) auto
   1.449 -    ultimately
   1.450 -    have "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i" by auto
   1.451 -  } note part1 = this
   1.452 +    ultimately show ?thesis by auto
   1.453 +  qed
   1.454    show ?th3
   1.455 -    unfolding subset_eq and Ball_def and mem_box
   1.456 -    apply (rule, rule, rule, rule)
   1.457 -    apply (rule part1)
   1.458 -    unfolding subset_eq and Ball_def and mem_box
   1.459 -    prefer 4
   1.460 -    apply auto
   1.461 -    apply (erule_tac x=xa in allE, erule_tac x=xa in allE, fastforce)+
   1.462 -    done
   1.463 -  {
   1.464 -    assume as: "box c d \<subseteq> box a b" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
   1.465 -    fix i :: 'a
   1.466 -    assume i:"i\<in>Basis"
   1.467 -    from as(1) have "box c d \<subseteq> cbox a b"
   1.468 -      using box_subset_cbox[of a b] by auto
   1.469 -    then have "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i"
   1.470 -      using part1 and as(2) using i by auto
   1.471 -  } note * = this
   1.472 +    using acdb by (fastforce simp add: mem_box)
   1.473 +  have acdb': "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i"
   1.474 +    if "i \<in> Basis" "box c d \<subseteq> box a b" "\<And>i. i \<in> Basis \<Longrightarrow> c\<bullet>i < d\<bullet>i" for i
   1.475 +      using box_subset_cbox[of a b] that acdb by auto
   1.476    show ?th4
   1.477 -    unfolding subset_eq and Ball_def and mem_box
   1.478 -    apply (rule, rule, rule, rule)
   1.479 -    apply (rule *)
   1.480 -    unfolding subset_eq and Ball_def and mem_box
   1.481 -    prefer 4
   1.482 -    apply auto
   1.483 -    apply (erule_tac x=xa in allE, simp)+
   1.484 -    done
   1.485 +    using acdb' by (fastforce simp add: mem_box)
   1.486  qed
   1.487  
   1.488  lemma eq_cbox: "cbox a b = cbox c d \<longleftrightarrow> cbox a b = {} \<and> cbox c d = {} \<or> a = c \<and> b = d"
   1.489 @@ -1775,19 +1747,14 @@
   1.490  lemma eq_cbox_box [simp]: "cbox a b = box c d \<longleftrightarrow> cbox a b = {} \<and> box c d = {}"
   1.491    (is "?lhs \<longleftrightarrow> ?rhs")
   1.492  proof
   1.493 -  assume ?lhs
   1.494 -  then have "cbox a b \<subseteq> box c d" "box c d \<subseteq>cbox a b"
   1.495 +  assume L: ?lhs
   1.496 +  then have "cbox a b \<subseteq> box c d" "box c d \<subseteq> cbox a b"
   1.497      by auto
   1.498    then show ?rhs
   1.499      apply (simp add: subset_box)
   1.500 -    using \<open>cbox a b = box c d\<close> box_ne_empty box_sing
   1.501 -    apply (fastforce simp add:)
   1.502 +    using L box_ne_empty box_sing apply (fastforce simp add:)
   1.503      done
   1.504 -next
   1.505 -  assume ?rhs
   1.506 -  then show ?lhs
   1.507 -    by force
   1.508 -qed
   1.509 +qed force
   1.510  
   1.511  lemma eq_box_cbox [simp]: "box a b = cbox c d \<longleftrightarrow> box a b = {} \<and> cbox c d = {}"
   1.512    by (metis eq_cbox_box)
   1.513 @@ -1795,20 +1762,16 @@
   1.514  lemma eq_box: "box a b = box c d \<longleftrightarrow> box a b = {} \<and> box c d = {} \<or> a = c \<and> b = d"
   1.515    (is "?lhs \<longleftrightarrow> ?rhs")
   1.516  proof
   1.517 -  assume ?lhs
   1.518 +  assume L: ?lhs
   1.519    then have "box a b \<subseteq> box c d" "box c d \<subseteq> box a b"
   1.520      by auto
   1.521    then show ?rhs
   1.522      apply (simp add: subset_box)
   1.523 -    using box_ne_empty(2) \<open>box a b = box c d\<close>
   1.524 +    using box_ne_empty(2) L
   1.525      apply auto
   1.526       apply (meson euclidean_eqI less_eq_real_def not_less)+
   1.527      done
   1.528 -next
   1.529 -  assume ?rhs
   1.530 -  then show ?lhs
   1.531 -    by force
   1.532 -qed
   1.533 +qed force
   1.534  
   1.535  lemma subset_box_complex:
   1.536     "cbox a b \<subseteq> cbox c d \<longleftrightarrow>
   1.537 @@ -2140,7 +2103,7 @@
   1.538      and d: "\<forall>x \<in> S. \<forall>y \<in> S. dist y x < e \<longrightarrow> y = x"
   1.539    shows "closed S"
   1.540  proof -
   1.541 -  have False if C: "\<forall>e>0. \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e" for x
   1.542 +  have False if C: "\<And>e. e>0 \<Longrightarrow> \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e" for x
   1.543    proof -
   1.544      from e have e2: "e/2 > 0" by arith
   1.545      from C[rule_format, OF e2] obtain y where y: "y \<in> S" "y \<noteq> x" "dist y x < e/2"
   1.546 @@ -2148,7 +2111,7 @@
   1.547      let ?m = "min (e/2) (dist x y) "
   1.548      from e2 y(2) have mp: "?m > 0"
   1.549        by simp
   1.550 -    from C[rule_format, OF mp] obtain z where z: "z \<in> S" "z \<noteq> x" "dist z x < ?m"
   1.551 +    from C[OF mp] obtain z where z: "z \<in> S" "z \<noteq> x" "dist z x < ?m"
   1.552        by blast
   1.553      from z y have "dist z y < e"
   1.554        by (intro dist_triangle_lt [where z=x]) simp
   1.555 @@ -2991,9 +2954,9 @@
   1.556          assume "m < n"
   1.557          have "dist (f(Suc n)) x = dist (y (min (inverse(2 ^ (Suc n))) (dist (f n) x))) x"
   1.558            by simp
   1.559 -        also have "... < dist (f n) x"
   1.560 +        also have "\<dots> < dist (f n) x"
   1.561            by (metis dist_pos_lt f min.strict_order_iff min_less_iff_conj y)
   1.562 -        also have "... < dist (f m) x"
   1.563 +        also have "\<dots> < dist (f m) x"
   1.564            using Suc.IH \<open>m < n\<close> by blast
   1.565          finally show ?thesis .
   1.566        next
   1.567 @@ -3127,9 +3090,9 @@
   1.568    proof -
   1.569      have "\<bar>f x\<bar> * norm (g x) \<le> \<bar>f x\<bar> * B"
   1.570        by (simp add: mult_left_mono g)
   1.571 -    also have "... \<le> \<bar>f x\<bar> * (\<bar>B\<bar> + 1)"
   1.572 +    also have "\<dots> \<le> \<bar>f x\<bar> * (\<bar>B\<bar> + 1)"
   1.573        by (simp add: mult_left_mono)
   1.574 -    also have "... < \<epsilon>"
   1.575 +    also have "\<dots> < \<epsilon>"
   1.576        by (rule f)
   1.577      finally show ?thesis .
   1.578    qed
   1.579 @@ -3290,7 +3253,7 @@
   1.580  lemma closure_approachableD:
   1.581    assumes "x \<in> closure S" "e>0"
   1.582    shows "\<exists>y\<in>S. dist x y < e"
   1.583 -  using assms unfolding closure_approachable by (auto simp add: dist_commute)
   1.584 +  using assms unfolding closure_approachable by (auto simp: dist_commute)
   1.585  
   1.586  lemma closed_approachable:
   1.587    fixes S :: "'a::metric_space set"
   1.588 @@ -5262,9 +5225,9 @@
   1.589    shows "((\<lambda>n. f (x n)) \<longlongrightarrow> f a) F"
   1.590  proof -
   1.591    have *: "filterlim x (inf (nhds a) (principal s)) F"
   1.592 -    using assms(2) assms(3) unfolding at_within_def filterlim_inf by (auto simp add: filterlim_principal eventually_mono)
   1.593 +    using assms(2) assms(3) unfolding at_within_def filterlim_inf by (auto simp: filterlim_principal eventually_mono)
   1.594    show ?thesis
   1.595 -    by (auto simp add: assms(1) continuous_within[symmetric] tendsto_at_within_iff_tendsto_nhds[symmetric] intro!: filterlim_compose[OF _ *])
   1.596 +    by (auto simp: assms(1) continuous_within[symmetric] tendsto_at_within_iff_tendsto_nhds[symmetric] intro!: filterlim_compose[OF _ *])
   1.597  qed
   1.598  
   1.599  lemma continuous_within_tendsto_compose':
   1.600 @@ -5402,7 +5365,7 @@
   1.601  
   1.602  lemma continuous_closed_imp_Cauchy_continuous:
   1.603    fixes S :: "('a::complete_space) set"
   1.604 -  shows "\<lbrakk>continuous_on S f; closed S; Cauchy \<sigma>; \<And>n. (\<sigma> n) \<in> S\<rbrakk> \<Longrightarrow> Cauchy(f o \<sigma>)"
   1.605 +  shows "\<lbrakk>continuous_on S f; closed S; Cauchy \<sigma>; \<And>n. (\<sigma> n) \<in> S\<rbrakk> \<Longrightarrow> Cauchy(f \<circ> \<sigma>)"
   1.606    apply (simp add: complete_eq_closed [symmetric] continuous_on_sequentially)
   1.607    by (meson LIMSEQ_imp_Cauchy complete_def)
   1.608  
   1.609 @@ -5876,30 +5839,20 @@
   1.610    let ?b = "\<Sum>i\<in>Basis. \<bar>a\<bullet>i\<bar> + \<bar>b\<bullet>i\<bar>"
   1.611    {
   1.612      fix x :: "'a"
   1.613 -    assume x: "\<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i"
   1.614 -    {
   1.615 -      fix i :: 'a
   1.616 -      assume "i \<in> Basis"
   1.617 -      then have "\<bar>x\<bullet>i\<bar> \<le> \<bar>a\<bullet>i\<bar> + \<bar>b\<bullet>i\<bar>"
   1.618 -        using x[THEN bspec[where x=i]] by auto
   1.619 -    }
   1.620 +    assume "\<And>i. i\<in>Basis \<Longrightarrow> a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i"
   1.621      then have "(\<Sum>i\<in>Basis. \<bar>x \<bullet> i\<bar>) \<le> ?b"
   1.622 -      apply -
   1.623 -      apply (rule sum_mono, auto)
   1.624 -      done
   1.625 +      by (force simp: intro!: sum_mono)
   1.626      then have "norm x \<le> ?b"
   1.627        using norm_le_l1[of x] by auto
   1.628    }
   1.629    then show ?thesis
   1.630 -    unfolding cbox_def bounded_iff by auto
   1.631 +    unfolding cbox_def bounded_iff by force
   1.632  qed
   1.633  
   1.634  lemma bounded_box [simp]:
   1.635    fixes a :: "'a::euclidean_space"
   1.636    shows "bounded (box a b)"
   1.637 -  using bounded_cbox[of a b]
   1.638 -  using box_subset_cbox[of a b]
   1.639 -  using bounded_subset[of "cbox a b" "box a b"]
   1.640 +  using bounded_cbox[of a b] box_subset_cbox[of a b] bounded_subset[of "cbox a b" "box a b"]
   1.641    by simp
   1.642  
   1.643  lemma not_interval_UNIV [simp]:
   1.644 @@ -5923,12 +5876,8 @@
   1.645    assumes "box a b \<noteq> {}"
   1.646    shows "((1/2) *\<^sub>R (a + b)) \<in> box a b"
   1.647  proof -
   1.648 -  {
   1.649 -    fix i :: 'a
   1.650 -    assume "i \<in> Basis"
   1.651 -    then have "a \<bullet> i < ((1 / 2) *\<^sub>R (a + b)) \<bullet> i \<and> ((1 / 2) *\<^sub>R (a + b)) \<bullet> i < b \<bullet> i"
   1.652 -      using assms[unfolded box_ne_empty, THEN bspec[where x=i]] by (auto simp: inner_add_left)
   1.653 -  }
   1.654 +  have "a \<bullet> i < ((1 / 2) *\<^sub>R (a + b)) \<bullet> i \<and> ((1 / 2) *\<^sub>R (a + b)) \<bullet> i < b \<bullet> i" if "i \<in> Basis" for i
   1.655 +    using assms that by (auto simp: inner_add_left box_ne_empty)
   1.656    then show ?thesis unfolding mem_box by auto
   1.657  qed
   1.658  
   1.659 @@ -5945,14 +5894,12 @@
   1.660      have "a \<bullet> i = e * (a \<bullet> i) + (1 - e) * (a \<bullet> i)"
   1.661        unfolding left_diff_distrib by simp
   1.662      also have "\<dots> < e * (x \<bullet> i) + (1 - e) * (y \<bullet> i)"
   1.663 -      apply (rule add_less_le_mono)
   1.664 -      using e unfolding mult_less_cancel_left and mult_le_cancel_left
   1.665 -      apply simp_all
   1.666 -      using x unfolding mem_box using i
   1.667 -      apply simp
   1.668 -      using y unfolding mem_box using i
   1.669 -      apply simp
   1.670 -      done
   1.671 +    proof (rule add_less_le_mono)
   1.672 +      show "e * (a \<bullet> i) < e * (x \<bullet> i)"
   1.673 +        using \<open>0 < e\<close> i mem_box(1) x by auto
   1.674 +      show "(1 - e) * (a \<bullet> i) \<le> (1 - e) * (y \<bullet> i)"
   1.675 +        by (meson diff_ge_0_iff_ge \<open>e \<le> 1\<close> i mem_box(2) mult_left_mono y)
   1.676 +    qed
   1.677      finally have "a \<bullet> i < (e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i"
   1.678        unfolding inner_simps by auto
   1.679      moreover
   1.680 @@ -5962,9 +5909,9 @@
   1.681        also have "\<dots> > e * (x \<bullet> i) + (1 - e) * (y \<bullet> i)"
   1.682        proof (rule add_less_le_mono)
   1.683          show "e * (x \<bullet> i) < e * (b \<bullet> i)"
   1.684 -          using e(1) i mem_box(1) x by auto
   1.685 +          using \<open>0 < e\<close> i mem_box(1) x by auto
   1.686          show "(1 - e) * (y \<bullet> i) \<le> (1 - e) * (b \<bullet> i)"
   1.687 -          by (meson diff_ge_0_iff_ge e(2) i mem_box(2) ordered_comm_semiring_class.comm_mult_left_mono y)
   1.688 +          by (meson diff_ge_0_iff_ge \<open>e \<le> 1\<close> i mem_box(2) mult_left_mono y)
   1.689        qed
   1.690        finally have "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i < b \<bullet> i"
   1.691          unfolding inner_simps by auto
   1.692 @@ -6011,13 +5958,8 @@
   1.693        {
   1.694          fix e :: real
   1.695          assume "e > 0"
   1.696 -        then have "\<exists>N::nat. inverse (real (N + 1)) < e"
   1.697 -          using real_arch_inverse[of e]
   1.698 -          apply (auto simp: Suc_pred')
   1.699 -          apply (metis Suc_pred' of_nat_Suc)
   1.700 -          done
   1.701          then obtain N :: nat where N: "inverse (real (N + 1)) < e"
   1.702 -          by auto
   1.703 +          using reals_Archimedean by auto
   1.704          have "inverse (real n + 1) < e" if "N \<le> n" for n
   1.705            by (auto intro!: that le_less_trans [OF _ N])
   1.706          then have "\<exists>N::nat. \<forall>n\<ge>N. inverse (real n + 1) < e" by auto
   1.707 @@ -6031,9 +5973,8 @@
   1.708          by auto
   1.709      }
   1.710      ultimately have "x \<in> closure (box a b)"
   1.711 -      using as and box_midpoint[OF assms]
   1.712 -      unfolding closure_def
   1.713 -      unfolding islimpt_sequential
   1.714 +      using as box_midpoint[OF assms]
   1.715 +      unfolding closure_def islimpt_sequential
   1.716        by (cases "x=?c") (auto simp: in_box_eucl_less)
   1.717    }
   1.718    then show ?thesis
   1.719 @@ -6041,49 +5982,31 @@
   1.720  qed
   1.721  
   1.722  lemma bounded_subset_box_symmetric:
   1.723 -  fixes s::"('a::euclidean_space) set"
   1.724 -  assumes "bounded s"
   1.725 -  shows "\<exists>a. s \<subseteq> box (-a) a"
   1.726 +  fixes S :: "('a::euclidean_space) set"
   1.727 +  assumes "bounded S"
   1.728 +  obtains a where "S \<subseteq> box (-a) a"
   1.729  proof -
   1.730 -  obtain b where "b>0" and b: "\<forall>x\<in>s. norm x \<le> b"
   1.731 +  obtain b where "b>0" and b: "\<forall>x\<in>S. norm x \<le> b"
   1.732      using assms[unfolded bounded_pos] by auto
   1.733    define a :: 'a where "a = (\<Sum>i\<in>Basis. (b + 1) *\<^sub>R i)"
   1.734 -  {
   1.735 -    fix x
   1.736 -    assume "x \<in> s"
   1.737 -    fix i :: 'a
   1.738 -    assume i: "i \<in> Basis"
   1.739 -    then have "(-a)\<bullet>i < x\<bullet>i" and "x\<bullet>i < a\<bullet>i"
   1.740 -      using b[THEN bspec[where x=x], OF \<open>x\<in>s\<close>]
   1.741 -      using Basis_le_norm[OF i, of x]
   1.742 -      unfolding inner_simps and a_def
   1.743 -      by auto
   1.744 -  }
   1.745 -  then show ?thesis
   1.746 -    by (auto intro: exI[where x=a] simp add: box_def)
   1.747 +  have "(-a)\<bullet>i < x\<bullet>i" and "x\<bullet>i < a\<bullet>i" if "x \<in> S" and i: "i \<in> Basis" for x i
   1.748 +    using b Basis_le_norm[OF i, of x] that by (auto simp: a_def)
   1.749 +  then have "S \<subseteq> box (-a) a"
   1.750 +    by (auto simp: simp add: box_def)
   1.751 +  then show ?thesis ..
   1.752  qed
   1.753  
   1.754 -lemma bounded_subset_open_interval:
   1.755 -  fixes s :: "('a::euclidean_space) set"
   1.756 -  shows "bounded s \<Longrightarrow> (\<exists>a b. s \<subseteq> box a b)"
   1.757 -  by (auto dest!: bounded_subset_box_symmetric)
   1.758 -
   1.759  lemma bounded_subset_cbox_symmetric:
   1.760 -  fixes s :: "('a::euclidean_space) set"
   1.761 -   assumes "bounded s"
   1.762 -  shows "\<exists>a. s \<subseteq> cbox (-a) a"
   1.763 +  fixes S :: "('a::euclidean_space) set"
   1.764 +  assumes "bounded S"
   1.765 +  obtains a where "S \<subseteq> cbox (-a) a"
   1.766  proof -
   1.767 -  obtain a where "s \<subseteq> box (-a) a"
   1.768 +  obtain a where "S \<subseteq> box (-a) a"
   1.769      using bounded_subset_box_symmetric[OF assms] by auto
   1.770    then show ?thesis
   1.771 -    using box_subset_cbox[of "-a" a] by auto
   1.772 +    by (meson box_subset_cbox dual_order.trans that)
   1.773  qed
   1.774  
   1.775 -lemma bounded_subset_cbox:
   1.776 -  fixes s :: "('a::euclidean_space) set"
   1.777 -  shows "bounded s \<Longrightarrow> \<exists>a b. s \<subseteq> cbox a b"
   1.778 -  using bounded_subset_cbox_symmetric[of s] by auto
   1.779 -
   1.780  lemma frontier_cbox:
   1.781    fixes a b :: "'a::euclidean_space"
   1.782    shows "frontier (cbox a b) = cbox a b - box a b"
   1.783 @@ -6113,13 +6036,12 @@
   1.784  lemma eucl_less_eq_halfspaces:
   1.785    fixes a :: "'a::euclidean_space"
   1.786    shows "{x. x <e a} = (\<Inter>i\<in>Basis. {x. x \<bullet> i < a \<bullet> i})"
   1.787 -    "{x. a <e x} = (\<Inter>i\<in>Basis. {x. a \<bullet> i < x \<bullet> i})"
   1.788 +        "{x. a <e x} = (\<Inter>i\<in>Basis. {x. a \<bullet> i < x \<bullet> i})"
   1.789    by (auto simp: eucl_less_def)
   1.790  
   1.791  lemma open_Collect_eucl_less[simp, intro]:
   1.792    fixes a :: "'a::euclidean_space"
   1.793 -  shows "open {x. x <e a}"
   1.794 -    "open {x. a <e x}"
   1.795 +  shows "open {x. x <e a}" "open {x. a <e x}"
   1.796    by (auto simp: eucl_less_eq_halfspaces open_halfspace_component_lt open_halfspace_component_gt)
   1.797  
   1.798  no_notation