src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 54780 6fae499e0827
parent 54775 2d3df8633dad
child 54797 be020ec8560c
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Dec 16 17:08:22 2013 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Dec 16 17:08:22 2013 +0100
     1.3 @@ -5993,544 +5993,8 @@
     1.4      done
     1.5  qed
     1.6  
     1.7 -
     1.8  subsection {* Intervals *}
     1.9  
    1.10 -lemma interval:
    1.11 -  fixes a :: "'a::ordered_euclidean_space"
    1.12 -  shows "box a b = {x::'a. \<forall>i\<in>Basis. a\<bullet>i < x\<bullet>i \<and> x\<bullet>i < b\<bullet>i}"
    1.13 -    and "{a .. b} = {x::'a. \<forall>i\<in>Basis. a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i}"
    1.14 -  by (auto simp add:set_eq_iff eucl_le[where 'a='a] box_def)
    1.15 -
    1.16 -lemma mem_interval:
    1.17 -  fixes a :: "'a::ordered_euclidean_space"
    1.18 -  shows "x \<in> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < x\<bullet>i \<and> x\<bullet>i < b\<bullet>i)"
    1.19 -    and "x \<in> {a .. b} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i)"
    1.20 -  using interval[of a b]
    1.21 -  by auto
    1.22 -
    1.23 -lemma interval_eq_empty:
    1.24 -  fixes a :: "'a::ordered_euclidean_space"
    1.25 -  shows "(box a b = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i))" (is ?th1)
    1.26 -    and "({a  ..  b} = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i < a\<bullet>i))" (is ?th2)
    1.27 -proof -
    1.28 -  {
    1.29 -    fix i x
    1.30 -    assume i: "i\<in>Basis" and as:"b\<bullet>i \<le> a\<bullet>i" and x:"x\<in>box a b"
    1.31 -    then have "a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i"
    1.32 -      unfolding mem_interval by auto
    1.33 -    then have "a\<bullet>i < b\<bullet>i" by auto
    1.34 -    then have False using as by auto
    1.35 -  }
    1.36 -  moreover
    1.37 -  {
    1.38 -    assume as: "\<forall>i\<in>Basis. \<not> (b\<bullet>i \<le> a\<bullet>i)"
    1.39 -    let ?x = "(1/2) *\<^sub>R (a + b)"
    1.40 -    {
    1.41 -      fix i :: 'a
    1.42 -      assume i: "i \<in> Basis"
    1.43 -      have "a\<bullet>i < b\<bullet>i"
    1.44 -        using as[THEN bspec[where x=i]] i by auto
    1.45 -      then have "a\<bullet>i < ((1/2) *\<^sub>R (a+b)) \<bullet> i" "((1/2) *\<^sub>R (a+b)) \<bullet> i < b\<bullet>i"
    1.46 -        by (auto simp: inner_add_left)
    1.47 -    }
    1.48 -    then have "box a b \<noteq> {}"
    1.49 -      using mem_interval(1)[of "?x" a b] by auto
    1.50 -  }
    1.51 -  ultimately show ?th1 by blast
    1.52 -
    1.53 -  {
    1.54 -    fix i x
    1.55 -    assume i: "i \<in> Basis" and as:"b\<bullet>i < a\<bullet>i" and x:"x\<in>{a .. b}"
    1.56 -    then have "a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i"
    1.57 -      unfolding mem_interval by auto
    1.58 -    then have "a\<bullet>i \<le> b\<bullet>i" by auto
    1.59 -    then have False using as by auto
    1.60 -  }
    1.61 -  moreover
    1.62 -  {
    1.63 -    assume as:"\<forall>i\<in>Basis. \<not> (b\<bullet>i < a\<bullet>i)"
    1.64 -    let ?x = "(1/2) *\<^sub>R (a + b)"
    1.65 -    {
    1.66 -      fix i :: 'a
    1.67 -      assume i:"i \<in> Basis"
    1.68 -      have "a\<bullet>i \<le> b\<bullet>i"
    1.69 -        using as[THEN bspec[where x=i]] i by auto
    1.70 -      then have "a\<bullet>i \<le> ((1/2) *\<^sub>R (a+b)) \<bullet> i" "((1/2) *\<^sub>R (a+b)) \<bullet> i \<le> b\<bullet>i"
    1.71 -        by (auto simp: inner_add_left)
    1.72 -    }
    1.73 -    then have "{a .. b} \<noteq> {}"
    1.74 -      using mem_interval(2)[of "?x" a b] by auto
    1.75 -  }
    1.76 -  ultimately show ?th2 by blast
    1.77 -qed
    1.78 -
    1.79 -lemma interval_ne_empty:
    1.80 -  fixes a :: "'a::ordered_euclidean_space"
    1.81 -  shows "{a  ..  b} \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i)"
    1.82 -  and "box a b \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)"
    1.83 -  unfolding interval_eq_empty[of a b] by fastforce+
    1.84 -
    1.85 -lemma interval_sing:
    1.86 -  fixes a :: "'a::ordered_euclidean_space"
    1.87 -  shows "{a .. a} = {a}"
    1.88 -    and "box a a = {}"
    1.89 -  unfolding set_eq_iff mem_interval eq_iff [symmetric]
    1.90 -  by (auto intro: euclidean_eqI simp: ex_in_conv)
    1.91 -
    1.92 -lemma subset_interval_imp:
    1.93 -  fixes a :: "'a::ordered_euclidean_space"
    1.94 -  shows "(\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i) \<Longrightarrow> {c .. d} \<subseteq> {a .. b}"
    1.95 -    and "(\<forall>i\<in>Basis. a\<bullet>i < c\<bullet>i \<and> d\<bullet>i < b\<bullet>i) \<Longrightarrow> {c .. d} \<subseteq> box a b"
    1.96 -    and "(\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i) \<Longrightarrow> box c d \<subseteq> {a .. b}"
    1.97 -    and "(\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i) \<Longrightarrow> box c d \<subseteq> box a b"
    1.98 -  unfolding subset_eq[unfolded Ball_def] unfolding mem_interval
    1.99 -  by (best intro: order_trans less_le_trans le_less_trans less_imp_le)+
   1.100 -
   1.101 -lemma interval_open_subset_closed:
   1.102 -  fixes a :: "'a::ordered_euclidean_space"
   1.103 -  shows "box a b \<subseteq> {a .. b}"
   1.104 -  unfolding subset_eq [unfolded Ball_def] mem_interval
   1.105 -  by (fast intro: less_imp_le)
   1.106 -
   1.107 -lemma subset_interval:
   1.108 -  fixes a :: "'a::ordered_euclidean_space"
   1.109 -  shows "{c .. d} \<subseteq> {a .. b} \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i \<le> d\<bullet>i) --> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th1)
   1.110 -    and "{c .. d} \<subseteq> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i \<le> d\<bullet>i) --> (\<forall>i\<in>Basis. a\<bullet>i < c\<bullet>i \<and> d\<bullet>i < b\<bullet>i)" (is ?th2)
   1.111 -    and "box c d \<subseteq> {a .. b} \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i) --> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th3)
   1.112 -    and "box c d \<subseteq> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i) --> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th4)
   1.113 -proof -
   1.114 -  show ?th1
   1.115 -    unfolding subset_eq and Ball_def and mem_interval
   1.116 -    by (auto intro: order_trans)
   1.117 -  show ?th2
   1.118 -    unfolding subset_eq and Ball_def and mem_interval
   1.119 -    by (auto intro: le_less_trans less_le_trans order_trans less_imp_le)
   1.120 -  {
   1.121 -    assume as: "box c d \<subseteq> {a .. b}" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
   1.122 -    then have "box c d \<noteq> {}"
   1.123 -      unfolding interval_eq_empty by auto
   1.124 -    fix i :: 'a
   1.125 -    assume i: "i \<in> Basis"
   1.126 -    (** TODO combine the following two parts as done in the HOL_light version. **)
   1.127 -    {
   1.128 -      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.129 -      assume as2: "a\<bullet>i > c\<bullet>i"
   1.130 -      {
   1.131 -        fix j :: 'a
   1.132 -        assume j: "j \<in> Basis"
   1.133 -        then have "c \<bullet> j < ?x \<bullet> j \<and> ?x \<bullet> j < d \<bullet> j"
   1.134 -          apply (cases "j = i")
   1.135 -          using as(2)[THEN bspec[where x=j]] i
   1.136 -          apply (auto simp add: as2)
   1.137 -          done
   1.138 -      }
   1.139 -      then have "?x\<in>box c d"
   1.140 -        using i unfolding mem_interval by auto
   1.141 -      moreover
   1.142 -      have "?x \<notin> {a .. b}"
   1.143 -        unfolding mem_interval
   1.144 -        apply auto
   1.145 -        apply (rule_tac x=i in bexI)
   1.146 -        using as(2)[THEN bspec[where x=i]] and as2 i
   1.147 -        apply auto
   1.148 -        done
   1.149 -      ultimately have False using as by auto
   1.150 -    }
   1.151 -    then have "a\<bullet>i \<le> c\<bullet>i" by (rule ccontr) auto
   1.152 -    moreover
   1.153 -    {
   1.154 -      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.155 -      assume as2: "b\<bullet>i < d\<bullet>i"
   1.156 -      {
   1.157 -        fix j :: 'a
   1.158 -        assume "j\<in>Basis"
   1.159 -        then have "d \<bullet> j > ?x \<bullet> j \<and> ?x \<bullet> j > c \<bullet> j"
   1.160 -          apply (cases "j = i")
   1.161 -          using as(2)[THEN bspec[where x=j]]
   1.162 -          apply (auto simp add: as2)
   1.163 -          done
   1.164 -      }
   1.165 -      then have "?x\<in>box c d"
   1.166 -        unfolding mem_interval by auto
   1.167 -      moreover
   1.168 -      have "?x\<notin>{a .. b}"
   1.169 -        unfolding mem_interval
   1.170 -        apply auto
   1.171 -        apply (rule_tac x=i in bexI)
   1.172 -        using as(2)[THEN bspec[where x=i]] and as2 using i
   1.173 -        apply auto
   1.174 -        done
   1.175 -      ultimately have False using as by auto
   1.176 -    }
   1.177 -    then have "b\<bullet>i \<ge> d\<bullet>i" by (rule ccontr) auto
   1.178 -    ultimately
   1.179 -    have "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i" by auto
   1.180 -  } note part1 = this
   1.181 -  show ?th3
   1.182 -    unfolding subset_eq and Ball_def and mem_interval
   1.183 -    apply (rule, rule, rule, rule)
   1.184 -    apply (rule part1)
   1.185 -    unfolding subset_eq and Ball_def and mem_interval
   1.186 -    prefer 4
   1.187 -    apply auto
   1.188 -    apply (erule_tac x=xa in allE, erule_tac x=xa in allE, fastforce)+
   1.189 -    done
   1.190 -  {
   1.191 -    assume as: "box c d \<subseteq> box a b" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
   1.192 -    fix i :: 'a
   1.193 -    assume i:"i\<in>Basis"
   1.194 -    from as(1) have "box c d \<subseteq> {a..b}"
   1.195 -      using interval_open_subset_closed[of a b] by auto
   1.196 -    then have "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i"
   1.197 -      using part1 and as(2) using i by auto
   1.198 -  } note * = this
   1.199 -  show ?th4
   1.200 -    unfolding subset_eq and Ball_def and mem_interval
   1.201 -    apply (rule, rule, rule, rule)
   1.202 -    apply (rule *)
   1.203 -    unfolding subset_eq and Ball_def and mem_interval
   1.204 -    prefer 4
   1.205 -    apply auto
   1.206 -    apply (erule_tac x=xa in allE, simp)+
   1.207 -    done
   1.208 -qed
   1.209 -
   1.210 -lemma inter_interval:
   1.211 -  fixes a :: "'a::ordered_euclidean_space"
   1.212 -  shows "{a .. b} \<inter> {c .. d} =
   1.213 -    {(\<Sum>i\<in>Basis. max (a\<bullet>i) (c\<bullet>i) *\<^sub>R i) .. (\<Sum>i\<in>Basis. min (b\<bullet>i) (d\<bullet>i) *\<^sub>R i)}"
   1.214 -  unfolding set_eq_iff and Int_iff and mem_interval
   1.215 -  by auto
   1.216 -
   1.217 -lemma disjoint_interval:
   1.218 -  fixes a::"'a::ordered_euclidean_space"
   1.219 -  shows "{a .. b} \<inter> {c .. d} = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i < a\<bullet>i \<or> d\<bullet>i < c\<bullet>i \<or> b\<bullet>i < c\<bullet>i \<or> d\<bullet>i < a\<bullet>i))" (is ?th1)
   1.220 -    and "{a .. b} \<inter> box c d = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i < a\<bullet>i \<or> d\<bullet>i \<le> c\<bullet>i \<or> b\<bullet>i \<le> c\<bullet>i \<or> d\<bullet>i \<le> a\<bullet>i))" (is ?th2)
   1.221 -    and "box a b \<inter> {c .. d} = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i \<le> a\<bullet>i \<or> d\<bullet>i < c\<bullet>i \<or> b\<bullet>i \<le> c\<bullet>i \<or> d\<bullet>i \<le> a\<bullet>i))" (is ?th3)
   1.222 -    and "box a b \<inter> box c d = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i \<le> a\<bullet>i \<or> d\<bullet>i \<le> c\<bullet>i \<or> b\<bullet>i \<le> c\<bullet>i \<or> d\<bullet>i \<le> a\<bullet>i))" (is ?th4)
   1.223 -proof -
   1.224 -  let ?z = "(\<Sum>i\<in>Basis. (((max (a\<bullet>i) (c\<bullet>i)) + (min (b\<bullet>i) (d\<bullet>i))) / 2) *\<^sub>R i)::'a"
   1.225 -  have **: "\<And>P Q. (\<And>i :: 'a. i \<in> Basis \<Longrightarrow> Q ?z i \<Longrightarrow> P i) \<Longrightarrow>
   1.226 -      (\<And>i x :: 'a. i \<in> Basis \<Longrightarrow> P i \<Longrightarrow> Q x i) \<Longrightarrow> (\<forall>x. \<exists>i\<in>Basis. Q x i) \<longleftrightarrow> (\<exists>i\<in>Basis. P i)"
   1.227 -    by blast
   1.228 -  note * = set_eq_iff Int_iff empty_iff mem_interval ball_conj_distrib[symmetric] eq_False ball_simps(10)
   1.229 -  show ?th1 unfolding * by (intro **) auto
   1.230 -  show ?th2 unfolding * by (intro **) auto
   1.231 -  show ?th3 unfolding * by (intro **) auto
   1.232 -  show ?th4 unfolding * by (intro **) auto
   1.233 -qed
   1.234 -
   1.235 -(* Moved interval_open_subset_closed a bit upwards *)
   1.236 -
   1.237 -lemma open_interval[intro]:
   1.238 -  fixes a b :: "'a::ordered_euclidean_space"
   1.239 -  shows "open (box a b)"
   1.240 -proof -
   1.241 -  have "open (\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i<..<b\<bullet>i})"
   1.242 -    by (intro open_INT finite_lessThan ballI continuous_open_vimage allI
   1.243 -      linear_continuous_at open_real_greaterThanLessThan finite_Basis bounded_linear_inner_left)
   1.244 -  also have "(\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i<..<b\<bullet>i}) = box a b"
   1.245 -    by (auto simp add: interval)
   1.246 -  finally show "open (box a b)" .
   1.247 -qed
   1.248 -
   1.249 -lemma closed_interval[intro]:
   1.250 -  fixes a b :: "'a::ordered_euclidean_space"
   1.251 -  shows "closed {a .. b}"
   1.252 -proof -
   1.253 -  have "closed (\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i .. b\<bullet>i})"
   1.254 -    by (intro closed_INT ballI continuous_closed_vimage allI
   1.255 -      linear_continuous_at closed_real_atLeastAtMost finite_Basis bounded_linear_inner_left)
   1.256 -  also have "(\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i .. b\<bullet>i}) = {a .. b}"
   1.257 -    by (auto simp add: eucl_le [where 'a='a])
   1.258 -  finally show "closed {a .. b}" .
   1.259 -qed
   1.260 -
   1.261 -lemma interior_closed_interval [intro]:
   1.262 -  fixes a b :: "'a::ordered_euclidean_space"
   1.263 -  shows "interior {a..b} = box a b" (is "?L = ?R")
   1.264 -proof(rule subset_antisym)
   1.265 -  show "?R \<subseteq> ?L"
   1.266 -    using interval_open_subset_closed open_interval
   1.267 -    by (rule interior_maximal)
   1.268 -  {
   1.269 -    fix x
   1.270 -    assume "x \<in> interior {a..b}"
   1.271 -    then obtain s where s: "open s" "x \<in> s" "s \<subseteq> {a..b}" ..
   1.272 -    then obtain e where "e>0" and e:"\<forall>x'. dist x' x < e \<longrightarrow> x' \<in> {a..b}"
   1.273 -      unfolding open_dist and subset_eq by auto
   1.274 -    {
   1.275 -      fix i :: 'a
   1.276 -      assume i: "i \<in> Basis"
   1.277 -      have "dist (x - (e / 2) *\<^sub>R i) x < e"
   1.278 -        and "dist (x + (e / 2) *\<^sub>R i) x < e"
   1.279 -        unfolding dist_norm
   1.280 -        apply auto
   1.281 -        unfolding norm_minus_cancel
   1.282 -        using norm_Basis[OF i] `e>0`
   1.283 -        apply auto
   1.284 -        done
   1.285 -      then have "a \<bullet> i \<le> (x - (e / 2) *\<^sub>R i) \<bullet> i" and "(x + (e / 2) *\<^sub>R i) \<bullet> i \<le> b \<bullet> i"
   1.286 -        using e[THEN spec[where x="x - (e/2) *\<^sub>R i"]]
   1.287 -          and e[THEN spec[where x="x + (e/2) *\<^sub>R i"]]
   1.288 -        unfolding mem_interval
   1.289 -        using i
   1.290 -        by blast+
   1.291 -      then have "a \<bullet> i < x \<bullet> i" and "x \<bullet> i < b \<bullet> i"
   1.292 -        using `e>0` i
   1.293 -        by (auto simp: inner_diff_left inner_Basis inner_add_left)
   1.294 -    }
   1.295 -    then have "x \<in> box a b"
   1.296 -      unfolding mem_interval by auto
   1.297 -  }
   1.298 -  then show "?L \<subseteq> ?R" ..
   1.299 -qed
   1.300 -
   1.301 -lemma bounded_closed_interval:
   1.302 -  fixes a :: "'a::ordered_euclidean_space"
   1.303 -  shows "bounded {a .. b}"
   1.304 -proof -
   1.305 -  let ?b = "\<Sum>i\<in>Basis. \<bar>a\<bullet>i\<bar> + \<bar>b\<bullet>i\<bar>"
   1.306 -  {
   1.307 -    fix x :: "'a"
   1.308 -    assume x: "\<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i"
   1.309 -    {
   1.310 -      fix i :: 'a
   1.311 -      assume "i \<in> Basis"
   1.312 -      then have "\<bar>x\<bullet>i\<bar> \<le> \<bar>a\<bullet>i\<bar> + \<bar>b\<bullet>i\<bar>"
   1.313 -        using x[THEN bspec[where x=i]] by auto
   1.314 -    }
   1.315 -    then have "(\<Sum>i\<in>Basis. \<bar>x \<bullet> i\<bar>) \<le> ?b"
   1.316 -      apply -
   1.317 -      apply (rule setsum_mono)
   1.318 -      apply auto
   1.319 -      done
   1.320 -    then have "norm x \<le> ?b"
   1.321 -      using norm_le_l1[of x] by auto
   1.322 -  }
   1.323 -  then show ?thesis
   1.324 -    unfolding interval and bounded_iff by auto
   1.325 -qed
   1.326 -
   1.327 -lemma bounded_interval:
   1.328 -  fixes a :: "'a::ordered_euclidean_space"
   1.329 -  shows "bounded {a .. b} \<and> bounded (box a b)"
   1.330 -  using bounded_closed_interval[of a b]
   1.331 -  using interval_open_subset_closed[of a b]
   1.332 -  using bounded_subset[of "{a..b}" "box a b"]
   1.333 -  by simp
   1.334 -
   1.335 -lemma not_interval_univ:
   1.336 -  fixes a :: "'a::ordered_euclidean_space"
   1.337 -  shows "{a .. b} \<noteq> UNIV \<and> box a b \<noteq> UNIV"
   1.338 -  using bounded_interval[of a b] by auto
   1.339 -
   1.340 -lemma compact_interval:
   1.341 -  fixes a :: "'a::ordered_euclidean_space"
   1.342 -  shows "compact {a .. b}"
   1.343 -  using bounded_closed_imp_seq_compact[of "{a..b}"] using bounded_interval[of a b]
   1.344 -  by (auto simp: compact_eq_seq_compact_metric)
   1.345 -
   1.346 -lemma open_interval_midpoint:
   1.347 -  fixes a :: "'a::ordered_euclidean_space"
   1.348 -  assumes "box a b \<noteq> {}"
   1.349 -  shows "((1/2) *\<^sub>R (a + b)) \<in> box a b"
   1.350 -proof -
   1.351 -  {
   1.352 -    fix i :: 'a
   1.353 -    assume "i \<in> Basis"
   1.354 -    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.355 -      using assms[unfolded interval_ne_empty, THEN bspec[where x=i]] by (auto simp: inner_add_left)
   1.356 -  }
   1.357 -  then show ?thesis unfolding mem_interval by auto
   1.358 -qed
   1.359 -
   1.360 -lemma open_closed_interval_convex:
   1.361 -  fixes x :: "'a::ordered_euclidean_space"
   1.362 -  assumes x: "x \<in> box a b"
   1.363 -    and y: "y \<in> {a .. b}"
   1.364 -    and e: "0 < e" "e \<le> 1"
   1.365 -  shows "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<in> box a b"
   1.366 -proof -
   1.367 -  {
   1.368 -    fix i :: 'a
   1.369 -    assume i: "i \<in> Basis"
   1.370 -    have "a \<bullet> i = e * (a \<bullet> i) + (1 - e) * (a \<bullet> i)"
   1.371 -      unfolding left_diff_distrib by simp
   1.372 -    also have "\<dots> < e * (x \<bullet> i) + (1 - e) * (y \<bullet> i)"
   1.373 -      apply (rule add_less_le_mono)
   1.374 -      using e unfolding mult_less_cancel_left and mult_le_cancel_left
   1.375 -      apply simp_all
   1.376 -      using x unfolding mem_interval using i
   1.377 -      apply simp
   1.378 -      using y unfolding mem_interval using i
   1.379 -      apply simp
   1.380 -      done
   1.381 -    finally have "a \<bullet> i < (e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i"
   1.382 -      unfolding inner_simps by auto
   1.383 -    moreover
   1.384 -    {
   1.385 -      have "b \<bullet> i = e * (b\<bullet>i) + (1 - e) * (b\<bullet>i)"
   1.386 -        unfolding left_diff_distrib by simp
   1.387 -      also have "\<dots> > e * (x \<bullet> i) + (1 - e) * (y \<bullet> i)"
   1.388 -        apply (rule add_less_le_mono)
   1.389 -        using e unfolding mult_less_cancel_left and mult_le_cancel_left
   1.390 -        apply simp_all
   1.391 -        using x
   1.392 -        unfolding mem_interval
   1.393 -        using i
   1.394 -        apply simp
   1.395 -        using y
   1.396 -        unfolding mem_interval
   1.397 -        using i
   1.398 -        apply simp
   1.399 -        done
   1.400 -      finally have "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i < b \<bullet> i"
   1.401 -        unfolding inner_simps by auto
   1.402 -    }
   1.403 -    ultimately have "a \<bullet> i < (e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i \<and> (e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i < b \<bullet> i"
   1.404 -      by auto
   1.405 -  }
   1.406 -  then show ?thesis
   1.407 -    unfolding mem_interval by auto
   1.408 -qed
   1.409 -
   1.410 -lemma closure_open_interval:
   1.411 -  fixes a :: "'a::ordered_euclidean_space"
   1.412 -  assumes "box a b \<noteq> {}"
   1.413 -  shows "closure (box a b) = {a .. b}"
   1.414 -proof -
   1.415 -  have ab: "a <e b"
   1.416 -    using assms by (simp add: eucl_less_def interval_ne_empty)
   1.417 -  let ?c = "(1 / 2) *\<^sub>R (a + b)"
   1.418 -  {
   1.419 -    fix x
   1.420 -    assume as:"x \<in> {a .. b}"
   1.421 -    def f \<equiv> "\<lambda>n::nat. x + (inverse (real n + 1)) *\<^sub>R (?c - x)"
   1.422 -    {
   1.423 -      fix n
   1.424 -      assume fn: "f n <e b \<longrightarrow> a <e f n \<longrightarrow> f n = x" and xc: "x \<noteq> ?c"
   1.425 -      have *: "0 < inverse (real n + 1)" "inverse (real n + 1) \<le> 1"
   1.426 -        unfolding inverse_le_1_iff by auto
   1.427 -      have "(inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b)) + (1 - inverse (real n + 1)) *\<^sub>R x =
   1.428 -        x + (inverse (real n + 1)) *\<^sub>R (((1 / 2) *\<^sub>R (a + b)) - x)"
   1.429 -        by (auto simp add: algebra_simps)
   1.430 -      then have "f n <e b" and "a <e f n"
   1.431 -        using open_closed_interval_convex[OF open_interval_midpoint[OF assms] as *]
   1.432 -        unfolding f_def by (auto simp: interval eucl_less_def)
   1.433 -      then have False
   1.434 -        using fn unfolding f_def using xc by auto
   1.435 -    }
   1.436 -    moreover
   1.437 -    {
   1.438 -      assume "\<not> (f ---> x) sequentially"
   1.439 -      {
   1.440 -        fix e :: real
   1.441 -        assume "e > 0"
   1.442 -        then have "\<exists>N::nat. inverse (real (N + 1)) < e"
   1.443 -          using real_arch_inv[of e]
   1.444 -          apply (auto simp add: Suc_pred')
   1.445 -          apply (rule_tac x="n - 1" in exI)
   1.446 -          apply auto
   1.447 -          done
   1.448 -        then obtain N :: nat where "inverse (real (N + 1)) < e"
   1.449 -          by auto
   1.450 -        then have "\<forall>n\<ge>N. inverse (real n + 1) < e"
   1.451 -          apply auto
   1.452 -          apply (metis Suc_le_mono le_SucE less_imp_inverse_less nat_le_real_less order_less_trans
   1.453 -            real_of_nat_Suc real_of_nat_Suc_gt_zero)
   1.454 -          done
   1.455 -        then have "\<exists>N::nat. \<forall>n\<ge>N. inverse (real n + 1) < e" by auto
   1.456 -      }
   1.457 -      then have "((\<lambda>n. inverse (real n + 1)) ---> 0) sequentially"
   1.458 -        unfolding LIMSEQ_def by(auto simp add: dist_norm)
   1.459 -      then have "(f ---> x) sequentially"
   1.460 -        unfolding f_def
   1.461 -        using tendsto_add[OF tendsto_const, of "\<lambda>n::nat. (inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b) - x)" 0 sequentially x]
   1.462 -        using tendsto_scaleR [OF _ tendsto_const, of "\<lambda>n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"]
   1.463 -        by auto
   1.464 -    }
   1.465 -    ultimately have "x \<in> closure (box a b)"
   1.466 -      using as and open_interval_midpoint[OF assms]
   1.467 -      unfolding closure_def
   1.468 -      unfolding islimpt_sequential
   1.469 -      by (cases "x=?c") (auto simp: in_box_eucl_less)
   1.470 -  }
   1.471 -  then show ?thesis
   1.472 -    using closure_minimal[OF interval_open_subset_closed closed_interval, of a b] by blast
   1.473 -qed
   1.474 -
   1.475 -lemma bounded_subset_open_interval_symmetric:
   1.476 -  fixes s::"('a::ordered_euclidean_space) set"
   1.477 -  assumes "bounded s"
   1.478 -  shows "\<exists>a. s \<subseteq> box (-a) a"
   1.479 -proof -
   1.480 -  obtain b where "b>0" and b: "\<forall>x\<in>s. norm x \<le> b"
   1.481 -    using assms[unfolded bounded_pos] by auto
   1.482 -  def a \<equiv> "(\<Sum>i\<in>Basis. (b + 1) *\<^sub>R i)::'a"
   1.483 -  {
   1.484 -    fix x
   1.485 -    assume "x \<in> s"
   1.486 -    fix i :: 'a
   1.487 -    assume i: "i \<in> Basis"
   1.488 -    then have "(-a)\<bullet>i < x\<bullet>i" and "x\<bullet>i < a\<bullet>i"
   1.489 -      using b[THEN bspec[where x=x], OF `x\<in>s`]
   1.490 -      using Basis_le_norm[OF i, of x]
   1.491 -      unfolding inner_simps and a_def
   1.492 -      by auto
   1.493 -  }
   1.494 -  then show ?thesis
   1.495 -    by (auto intro: exI[where x=a] simp add: interval)
   1.496 -qed
   1.497 -
   1.498 -lemma bounded_subset_open_interval:
   1.499 -  fixes s :: "('a::ordered_euclidean_space) set"
   1.500 -  shows "bounded s \<Longrightarrow> (\<exists>a b. s \<subseteq> box a b)"
   1.501 -  by (auto dest!: bounded_subset_open_interval_symmetric)
   1.502 -
   1.503 -lemma bounded_subset_closed_interval_symmetric:
   1.504 -  fixes s :: "('a::ordered_euclidean_space) set"
   1.505 -  assumes "bounded s"
   1.506 -  shows "\<exists>a. s \<subseteq> {-a .. a}"
   1.507 -proof -
   1.508 -  obtain a where "s \<subseteq> box (-a) a"
   1.509 -    using bounded_subset_open_interval_symmetric[OF assms] by auto
   1.510 -  then show ?thesis
   1.511 -    using interval_open_subset_closed[of "-a" a] by auto
   1.512 -qed
   1.513 -
   1.514 -lemma bounded_subset_closed_interval:
   1.515 -  fixes s :: "('a::ordered_euclidean_space) set"
   1.516 -  shows "bounded s \<Longrightarrow> \<exists>a b. s \<subseteq> {a .. b}"
   1.517 -  using bounded_subset_closed_interval_symmetric[of s] by auto
   1.518 -
   1.519 -lemma frontier_closed_interval:
   1.520 -  fixes a b :: "'a::ordered_euclidean_space"
   1.521 -  shows "frontier {a .. b} = {a .. b} - box a b"
   1.522 -  unfolding frontier_def unfolding interior_closed_interval and closure_closed[OF closed_interval] ..
   1.523 -
   1.524 -lemma frontier_open_interval:
   1.525 -  fixes a b :: "'a::ordered_euclidean_space"
   1.526 -  shows "frontier (box a b) = (if box a b = {} then {} else {a .. b} - box a b)"
   1.527 -proof (cases "box a b = {}")
   1.528 -  case True
   1.529 -  then show ?thesis
   1.530 -    using frontier_empty by auto
   1.531 -next
   1.532 -  case False
   1.533 -  then show ?thesis
   1.534 -    unfolding frontier_def and closure_open_interval[OF False] and interior_open[OF open_interval]
   1.535 -    by auto
   1.536 -qed
   1.537 -
   1.538 -lemma inter_interval_mixed_eq_empty:
   1.539 -  fixes a :: "'a::ordered_euclidean_space"
   1.540 -  assumes "box c d \<noteq> {}"
   1.541 -  shows "box a b \<inter> {c .. d} = {} \<longleftrightarrow> box a b \<inter> box c d = {}"
   1.542 -  unfolding closure_open_interval[OF assms, symmetric]
   1.543 -  unfolding open_inter_closure_eq_empty[OF open_interval] ..
   1.544 -
   1.545  lemma open_box: "open (box a b)"
   1.546  proof -
   1.547    have "open (\<Inter>i\<in>Basis. (op \<bullet> i) -` {a \<bullet> i <..< b \<bullet> i})"
   1.548 @@ -6574,26 +6038,6 @@
   1.549  
   1.550  instance euclidean_space \<subseteq> polish_space ..
   1.551  
   1.552 -text {* Intervals in general, including infinite and mixtures of open and closed. *}
   1.553 -
   1.554 -definition "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow>
   1.555 -  (\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i\<in>Basis. ((a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i) \<or> (b\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> a\<bullet>i))) \<longrightarrow> x \<in> s)"
   1.556 -
   1.557 -lemma is_interval_interval: "is_interval {a .. b::'a::ordered_euclidean_space}" (is ?th1)
   1.558 -  "is_interval (box a b)" (is ?th2) proof -
   1.559 -  show ?th1 ?th2  unfolding is_interval_def mem_interval Ball_def atLeastAtMost_iff
   1.560 -    by(meson order_trans le_less_trans less_le_trans less_trans)+ qed
   1.561 -
   1.562 -lemma is_interval_empty:
   1.563 - "is_interval {}"
   1.564 -  unfolding is_interval_def
   1.565 -  by simp
   1.566 -
   1.567 -lemma is_interval_univ:
   1.568 - "is_interval UNIV"
   1.569 -  unfolding is_interval_def
   1.570 -  by simp
   1.571 -
   1.572  
   1.573  subsection {* Closure of halfspaces and hyperplanes *}
   1.574  
   1.575 @@ -6704,50 +6148,6 @@
   1.576  lemma open_halfspace_component_gt: "open {x::'a::euclidean_space. x\<bullet>i > a}"
   1.577    by (simp add: open_Collect_less)
   1.578  
   1.579 -text{* Instantiation for intervals on @{text ordered_euclidean_space} *}
   1.580 -
   1.581 -lemma eucl_lessThan_eq_halfspaces:
   1.582 -  fixes a :: "'a\<Colon>ordered_euclidean_space"
   1.583 -  shows "{x. x <e a} = (\<Inter>i\<in>Basis. {x. x \<bullet> i < a \<bullet> i})"
   1.584 -  by (auto simp: eucl_less_def)
   1.585 -
   1.586 -lemma eucl_greaterThan_eq_halfspaces:
   1.587 -  fixes a :: "'a\<Colon>ordered_euclidean_space"
   1.588 -  shows "{x. a <e x} = (\<Inter>i\<in>Basis. {x. a \<bullet> i < x \<bullet> i})"
   1.589 -  by (auto simp: eucl_less_def)
   1.590 -
   1.591 -lemma eucl_atMost_eq_halfspaces:
   1.592 -  fixes a :: "'a\<Colon>ordered_euclidean_space"
   1.593 -  shows "{.. a} = (\<Inter>i\<in>Basis. {x. x \<bullet> i \<le> a \<bullet> i})"
   1.594 -  by (auto simp: eucl_le[where 'a='a])
   1.595 -
   1.596 -lemma eucl_atLeast_eq_halfspaces:
   1.597 -  fixes a :: "'a\<Colon>ordered_euclidean_space"
   1.598 -  shows "{a ..} = (\<Inter>i\<in>Basis. {x. a \<bullet> i \<le> x \<bullet> i})"
   1.599 -  by (auto simp: eucl_le[where 'a='a])
   1.600 -
   1.601 -lemma open_eucl_lessThan[simp, intro]:
   1.602 -  fixes a :: "'a\<Colon>ordered_euclidean_space"
   1.603 -  shows "open {x. x <e a}"
   1.604 -  by (auto simp: eucl_lessThan_eq_halfspaces open_halfspace_component_lt)
   1.605 -
   1.606 -lemma open_eucl_greaterThan[simp, intro]:
   1.607 -  fixes a :: "'a\<Colon>ordered_euclidean_space"
   1.608 -  shows "open {x. a <e x}"
   1.609 -  by (auto simp: eucl_greaterThan_eq_halfspaces open_halfspace_component_gt)
   1.610 -
   1.611 -lemma closed_eucl_atMost[simp, intro]:
   1.612 -  fixes a :: "'a\<Colon>ordered_euclidean_space"
   1.613 -  shows "closed {.. a}"
   1.614 -  unfolding eucl_atMost_eq_halfspaces
   1.615 -  by (simp add: closed_INT closed_Collect_le)
   1.616 -
   1.617 -lemma closed_eucl_atLeast[simp, intro]:
   1.618 -  fixes a :: "'a\<Colon>ordered_euclidean_space"
   1.619 -  shows "closed {a ..}"
   1.620 -  unfolding eucl_atLeast_eq_halfspaces
   1.621 -  by (simp add: closed_INT closed_Collect_le)
   1.622 -
   1.623  text {* This gives a simple derivation of limit component bounds. *}
   1.624  
   1.625  lemma Lim_component_le:
   1.626 @@ -7339,69 +6739,6 @@
   1.627   "(m::'a::linordered_field) \<noteq> 0 \<Longrightarrow> (y = m * x + c  \<longleftrightarrow> inverse(m) * y + -(c / m) = x)"
   1.628    by (simp add: field_simps inverse_eq_divide)
   1.629  
   1.630 -lemma image_affinity_interval: fixes m::real
   1.631 -  fixes a b c :: "'a::ordered_euclidean_space"
   1.632 -  shows "(\<lambda>x. m *\<^sub>R x + c) ` {a .. b} =
   1.633 -    (if {a .. b} = {} then {}
   1.634 -     else (if 0 \<le> m then {m *\<^sub>R a + c .. m *\<^sub>R b + c}
   1.635 -     else {m *\<^sub>R b + c .. m *\<^sub>R a + c}))"
   1.636 -proof (cases "m = 0")
   1.637 -  case True
   1.638 -  {
   1.639 -    fix x
   1.640 -    assume "x \<le> c" "c \<le> x"
   1.641 -    then have "x = c"
   1.642 -      unfolding eucl_le[where 'a='a]
   1.643 -      apply -
   1.644 -      apply (subst euclidean_eq_iff)
   1.645 -      apply (auto intro: order_antisym)
   1.646 -      done
   1.647 -  }
   1.648 -  moreover have "c \<in> {m *\<^sub>R a + c..m *\<^sub>R b + c}"
   1.649 -    unfolding True by (auto simp add: eucl_le[where 'a='a])
   1.650 -  ultimately show ?thesis using True by auto
   1.651 -next
   1.652 -  case False
   1.653 -  {
   1.654 -    fix y
   1.655 -    assume "a \<le> y" "y \<le> b" "m > 0"
   1.656 -    then have "m *\<^sub>R a + c \<le> m *\<^sub>R y + c" and "m *\<^sub>R y + c \<le> m *\<^sub>R b + c"
   1.657 -      unfolding eucl_le[where 'a='a] by (auto simp: inner_distrib)
   1.658 -  }
   1.659 -  moreover
   1.660 -  {
   1.661 -    fix y
   1.662 -    assume "a \<le> y" "y \<le> b" "m < 0"
   1.663 -    then have "m *\<^sub>R b + c \<le> m *\<^sub>R y + c" and "m *\<^sub>R y + c \<le> m *\<^sub>R a + c"
   1.664 -      unfolding eucl_le[where 'a='a] by (auto simp add: mult_left_mono_neg inner_distrib)
   1.665 -  }
   1.666 -  moreover
   1.667 -  {
   1.668 -    fix y
   1.669 -    assume "m > 0" and "m *\<^sub>R a + c \<le> y" and "y \<le> m *\<^sub>R b + c"
   1.670 -    then have "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}"
   1.671 -      unfolding image_iff Bex_def mem_interval eucl_le[where 'a='a]
   1.672 -      apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
   1.673 -      apply (auto simp add: pos_le_divide_eq pos_divide_le_eq mult_commute diff_le_iff inner_distrib inner_diff_left)
   1.674 -      done
   1.675 -  }
   1.676 -  moreover
   1.677 -  {
   1.678 -    fix y
   1.679 -    assume "m *\<^sub>R b + c \<le> y" "y \<le> m *\<^sub>R a + c" "m < 0"
   1.680 -    then have "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}"
   1.681 -      unfolding image_iff Bex_def mem_interval eucl_le[where 'a='a]
   1.682 -      apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
   1.683 -      apply (auto simp add: neg_le_divide_eq neg_divide_le_eq mult_commute diff_le_iff inner_distrib inner_diff_left)
   1.684 -      done
   1.685 -  }
   1.686 -  ultimately show ?thesis using False by auto
   1.687 -qed
   1.688 -
   1.689 -lemma image_smult_interval:"(\<lambda>x. m *\<^sub>R (x::_::ordered_euclidean_space)) ` {a..b} =
   1.690 -  (if {a..b} = {} then {} else if 0 \<le> m then {m *\<^sub>R a..m *\<^sub>R b} else {m *\<^sub>R b..m *\<^sub>R a})"
   1.691 -  using image_affinity_interval[of m 0 a b] by auto
   1.692 -
   1.693  
   1.694  subsection {* Banach fixed point theorem (not really topological...) *}
   1.695