src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
 changeset 50526 899c9c4e4a4c parent 50324 0a1242d5e7d4 child 50881 ae630bab13da
```     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Dec 14 14:46:01 2012 +0100
1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Dec 14 15:46:01 2012 +0100
1.3 @@ -13,9 +13,17 @@
1.4    "~~/src/HOL/Library/Countable_Set"
1.5    Linear_Algebra
1.6    "~~/src/HOL/Library/Glbs"
1.7 +  "~~/src/HOL/Library/FuncSet"
1.8    Norm_Arith
1.9  begin
1.10
1.11 +lemma countable_PiE:
1.12 +  "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (PiE I F)"
1.13 +  by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq)
1.14 +
1.15 +lemma countable_rat: "countable \<rat>"
1.16 +  unfolding Rats_def by auto
1.17 +
1.18  subsection {* Topological Basis *}
1.19
1.20  context topological_space
1.21 @@ -593,86 +601,74 @@
1.22
1.23  lemma ball_empty[intro]: "e \<le> 0 ==> ball x e = {}" by simp
1.24
1.25 +lemma euclidean_dist_l2:
1.26 +  fixes x y :: "'a :: euclidean_space"
1.27 +  shows "dist x y = setL2 (\<lambda>i. dist (x \<bullet> i) (y \<bullet> i)) Basis"
1.28 +  unfolding dist_norm norm_eq_sqrt_inner setL2_def
1.29 +  by (subst euclidean_inner) (simp add: power2_eq_square inner_diff_left)
1.30 +
1.31 +definition "box a b = {x. \<forall>i\<in>Basis. a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i}"
1.32 +
1.33  lemma rational_boxes:
1.34 -  fixes x :: "'a\<Colon>ordered_euclidean_space"
1.35 +  fixes x :: "'a\<Colon>euclidean_space"
1.36    assumes "0 < e"
1.37 -  shows "\<exists>a b. (\<forall>i. a \$\$ i \<in> \<rat>) \<and> (\<forall>i. b \$\$ i \<in> \<rat>) \<and> x \<in> {a <..< b} \<and> {a <..< b} \<subseteq> ball x e"
1.38 +  shows "\<exists>a b. (\<forall>i\<in>Basis. a \<bullet> i \<in> \<rat> \<and> b \<bullet> i \<in> \<rat> ) \<and> x \<in> box a b \<and> box a b \<subseteq> ball x e"
1.39  proof -
1.40    def e' \<equiv> "e / (2 * sqrt (real (DIM ('a))))"
1.41 -  then have e: "0 < e'" using assms by (auto intro!: divide_pos_pos)
1.42 -  have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> y < x \$\$ i \<and> x \$\$ i - y < e'" (is "\<forall>i. ?th i")
1.43 +  then have e: "0 < e'" using assms by (auto intro!: divide_pos_pos simp: DIM_positive)
1.44 +  have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> y < x \<bullet> i \<and> x \<bullet> i - y < e'" (is "\<forall>i. ?th i")
1.45    proof
1.46 -    fix i from Rats_dense_in_real[of "x \$\$ i - e'" "x \$\$ i"] e
1.47 -    show "?th i" by auto
1.48 +    fix i from Rats_dense_in_real[of "x \<bullet> i - e'" "x \<bullet> i"] e show "?th i" by auto
1.49    qed
1.50    from choice[OF this] guess a .. note a = this
1.51 -  have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> x \$\$ i < y \<and> y - x \$\$ i < e'" (is "\<forall>i. ?th i")
1.52 +  have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> x \<bullet> i < y \<and> y - x \<bullet> i < e'" (is "\<forall>i. ?th i")
1.53    proof
1.54 -    fix i from Rats_dense_in_real[of "x \$\$ i" "x \$\$ i + e'"] e
1.55 -    show "?th i" by auto
1.56 +    fix i from Rats_dense_in_real[of "x \<bullet> i" "x \<bullet> i + e'"] e show "?th i" by auto
1.57    qed
1.58    from choice[OF this] guess b .. note b = this
1.59 -  { fix y :: 'a assume *: "Chi a < y" "y < Chi b"
1.60 -    have "dist x y = sqrt (\<Sum>i<DIM('a). (dist (x \$\$ i) (y \$\$ i))\<twosuperior>)"
1.61 +  let ?a = "\<Sum>i\<in>Basis. a i *\<^sub>R i" and ?b = "\<Sum>i\<in>Basis. b i *\<^sub>R i"
1.62 +  show ?thesis
1.63 +  proof (rule exI[of _ ?a], rule exI[of _ ?b], safe)
1.64 +    fix y :: 'a assume *: "y \<in> box ?a ?b"
1.65 +    have "dist x y = sqrt (\<Sum>i\<in>Basis. (dist (x \<bullet> i) (y \<bullet> i))\<twosuperior>)"
1.66        unfolding setL2_def[symmetric] by (rule euclidean_dist_l2)
1.67 -    also have "\<dots> < sqrt (\<Sum>i<DIM('a). e^2 / real (DIM('a)))"
1.68 +    also have "\<dots> < sqrt (\<Sum>(i::'a)\<in>Basis. e^2 / real (DIM('a)))"
1.69      proof (rule real_sqrt_less_mono, rule setsum_strict_mono)
1.70 -      fix i assume i: "i \<in> {..<DIM('a)}"
1.71 -      have "a i < y\$\$i \<and> y\$\$i < b i" using * i eucl_less[where 'a='a] by auto
1.72 -      moreover have "a i < x\$\$i" "x\$\$i - a i < e'" using a by auto
1.73 -      moreover have "x\$\$i < b i" "b i - x\$\$i < e'" using b by auto
1.74 -      ultimately have "\<bar>x\$\$i - y\$\$i\<bar> < 2 * e'" by auto
1.75 -      then have "dist (x \$\$ i) (y \$\$ i) < e/sqrt (real (DIM('a)))"
1.76 +      fix i :: "'a" assume i: "i \<in> Basis"
1.77 +      have "a i < y\<bullet>i \<and> y\<bullet>i < b i" using * i by (auto simp: box_def)
1.78 +      moreover have "a i < x\<bullet>i" "x\<bullet>i - a i < e'" using a by auto
1.79 +      moreover have "x\<bullet>i < b i" "b i - x\<bullet>i < e'" using b by auto
1.80 +      ultimately have "\<bar>x\<bullet>i - y\<bullet>i\<bar> < 2 * e'" by auto
1.81 +      then have "dist (x \<bullet> i) (y \<bullet> i) < e/sqrt (real (DIM('a)))"
1.82          unfolding e'_def by (auto simp: dist_real_def)
1.83 -      then have "(dist (x \$\$ i) (y \$\$ i))\<twosuperior> < (e/sqrt (real (DIM('a))))\<twosuperior>"
1.84 +      then have "(dist (x \<bullet> i) (y \<bullet> i))\<twosuperior> < (e/sqrt (real (DIM('a))))\<twosuperior>"
1.85          by (rule power_strict_mono) auto
1.86 -      then show "(dist (x \$\$ i) (y \$\$ i))\<twosuperior> < e\<twosuperior> / real DIM('a)"
1.87 +      then show "(dist (x \<bullet> i) (y \<bullet> i))\<twosuperior> < e\<twosuperior> / real DIM('a)"
1.89      qed auto
1.90 -    also have "\<dots> = e" using `0 < e` by (simp add: real_eq_of_nat DIM_positive)
1.91 -    finally have "dist x y < e" . }
1.92 -  with a b show ?thesis
1.93 -    apply (rule_tac exI[of _ "Chi a"])
1.94 -    apply (rule_tac exI[of _ "Chi b"])
1.95 -    using eucl_less[where 'a='a] by auto
1.96 -qed
1.97 -
1.98 -lemma ex_rat_list:
1.99 -  fixes x :: "'a\<Colon>ordered_euclidean_space"
1.100 -  assumes "\<And> i. x \$\$ i \<in> \<rat>"
1.101 -  shows "\<exists> r. length r = DIM('a) \<and> (\<forall> i < DIM('a). of_rat (r ! i) = x \$\$ i)"
1.102 -proof -
1.103 -  have "\<forall>i. \<exists>r. x \$\$ i = of_rat r" using assms unfolding Rats_def by blast
1.104 -  from choice[OF this] guess r ..
1.105 -  then show ?thesis by (auto intro!: exI[of _ "map r [0 ..< DIM('a)]"])
1.106 -qed
1.107 -
1.108 -lemma open_UNION:
1.109 -  fixes M :: "'a\<Colon>ordered_euclidean_space set"
1.110 -  assumes "open M"
1.111 -  shows "M = UNION {(a, b) | a b. {Chi (of_rat \<circ> op ! a) <..< Chi (of_rat \<circ> op ! b)} \<subseteq> M}
1.112 -                   (\<lambda> (a, b). {Chi (of_rat \<circ> op ! a) <..< Chi (of_rat \<circ> op ! b)})"
1.113 -    (is "M = UNION ?idx ?box")
1.114 +    also have "\<dots> = e" using `0 < e` by (simp add: real_eq_of_nat)
1.115 +    finally show "y \<in> ball x e" by (auto simp: ball_def)
1.116 +  qed (insert a b, auto simp: box_def)
1.117 +qed
1.118 +
1.119 +lemma open_UNION_box:
1.120 +  fixes M :: "'a\<Colon>euclidean_space set"
1.121 +  assumes "open M"
1.122 +  defines "a' \<equiv> \<lambda>f :: 'a \<Rightarrow> real \<times> real. (\<Sum>(i::'a)\<in>Basis. fst (f i) *\<^sub>R i)"
1.123 +  defines "b' \<equiv> \<lambda>f :: 'a \<Rightarrow> real \<times> real. (\<Sum>(i::'a)\<in>Basis. snd (f i) *\<^sub>R i)"
1.124 +  defines "I \<equiv> {f\<in>Basis \<rightarrow>\<^isub>E \<rat> \<times> \<rat>. box (a' f) (b' f) \<subseteq> M}"
1.125 +  shows "M = (\<Union>f\<in>I. box (a' f) (b' f))"
1.126  proof safe
1.127    fix x assume "x \<in> M"
1.128    obtain e where e: "e > 0" "ball x e \<subseteq> M"
1.129 -    using openE[OF assms `x \<in> M`] by auto
1.130 -  then obtain a b where ab: "x \<in> {a <..< b}" "\<And>i. a \$\$ i \<in> \<rat>" "\<And>i. b \$\$ i \<in> \<rat>" "{a <..< b} \<subseteq> ball x e"
1.131 -    using rational_boxes[OF e(1)] by blast
1.132 -  then obtain p q where pq: "length p = DIM ('a)"
1.133 -                            "length q = DIM ('a)"
1.134 -                            "\<forall> i < DIM ('a). of_rat (p ! i) = a \$\$ i \<and> of_rat (q ! i) = b \$\$ i"
1.135 -    using ex_rat_list[OF ab(2)] ex_rat_list[OF ab(3)] by blast
1.136 -  hence p: "Chi (of_rat \<circ> op ! p) = a"
1.137 -    using euclidean_eq[of "Chi (of_rat \<circ> op ! p)" a]
1.138 -    unfolding o_def by auto
1.139 -  from pq have q: "Chi (of_rat \<circ> op ! q) = b"
1.140 -    using euclidean_eq[of "Chi (of_rat \<circ> op ! q)" b]
1.141 -    unfolding o_def by auto
1.142 -  have "x \<in> ?box (p, q)"
1.143 -    using p q ab by auto
1.144 -  thus "x \<in> UNION ?idx ?box" using ab e p q exI[of _ p] exI[of _ q] by auto
1.145 -qed auto
1.146 +    using openE[OF `open M` `x \<in> M`] by auto
1.147 +  moreover then obtain a b where ab: "x \<in> box a b"
1.148 +    "\<forall>i \<in> Basis. a \<bullet> i \<in> \<rat>" "\<forall>i\<in>Basis. b \<bullet> i \<in> \<rat>" "box a b \<subseteq> ball x e"
1.149 +    using rational_boxes[OF e(1)] by metis
1.150 +  ultimately show "x \<in> (\<Union>f\<in>I. box (a' f) (b' f))"
1.151 +     by (intro UN_I[of "\<lambda>i\<in>Basis. (a \<bullet> i, b \<bullet> i)"])
1.152 +        (auto simp: euclidean_representation I_def a'_def b'_def)
1.153 +qed (auto simp: I_def)
1.154
1.155  subsection{* Connectedness *}
1.156
1.157 @@ -1156,14 +1152,10 @@
1.158    "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
1.159  unfolding eventually_at dist_nz by auto
1.160
1.161 -lemma eventually_within: "eventually P (at a within S) \<longleftrightarrow>
1.162 +lemma eventually_within: (* FIXME: this replaces Limits.eventually_within *)
1.163 +  "eventually P (at a within S) \<longleftrightarrow>
1.164          (\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
1.165 -unfolding eventually_within eventually_at dist_nz by auto
1.166 -
1.167 -lemma eventually_within_le: "eventually P (at a within S) \<longleftrightarrow>
1.168 -        (\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a <= d \<longrightarrow> P x)" (is "?lhs = ?rhs")
1.169 -unfolding eventually_within
1.170 -by auto (metis dense order_le_less_trans)
1.171 +  by (rule eventually_within_less)
1.172
1.173  lemma eventually_happens: "eventually P net ==> trivial_limit net \<or> (\<exists>x. P x)"
1.174    unfolding trivial_limit_def
1.175 @@ -1721,7 +1713,7 @@
1.176      assume "\<not> (\<exists>y\<in>A. dist y x < e)"
1.177      hence "infdist x A \<ge> e" using `a \<in> A`
1.178        unfolding infdist_def
1.179 -      by (force intro: Inf_greatest simp: dist_commute)
1.180 +      by (force simp: dist_commute)
1.181      with x `0 < e` show False by auto
1.182    qed
1.183  qed
1.184 @@ -2374,56 +2366,41 @@
1.185      by auto
1.186  qed
1.187
1.188 -lemma bounded_component: "bounded s \<Longrightarrow> bounded ((\<lambda>x. x \$\$ i) ` s)"
1.189 -  apply (erule bounded_linear_image)
1.190 -  apply (rule bounded_linear_euclidean_component)
1.191 -  done
1.192 -
1.193  lemma compact_lemma:
1.194    fixes f :: "nat \<Rightarrow> 'a::euclidean_space"
1.195    assumes "bounded s" and "\<forall>n. f n \<in> s"
1.196 -  shows "\<forall>d. \<exists>l::'a. \<exists> r. subseq r \<and>
1.197 -        (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \$\$ i) (l \$\$ i) < e) sequentially)"
1.198 -proof
1.199 -  fix d'::"nat set" def d \<equiv> "d' \<inter> {..<DIM('a)}"
1.200 -  have "finite d" "d\<subseteq>{..<DIM('a)}" unfolding d_def by auto
1.201 -  hence "\<exists>l::'a. \<exists>r. subseq r \<and>
1.202 -      (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \$\$ i) (l \$\$ i) < e) sequentially)"
1.203 +  shows "\<forall>d\<subseteq>Basis. \<exists>l::'a. \<exists> r. subseq r \<and>
1.204 +        (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially)"
1.205 +proof safe
1.206 +  fix d :: "'a set" assume d: "d \<subseteq> Basis"
1.207 +  with finite_Basis have "finite d" by (blast intro: finite_subset)
1.208 +  from this d show "\<exists>l::'a. \<exists>r. subseq r \<and>
1.209 +      (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially)"
1.210    proof(induct d) case empty thus ?case unfolding subseq_def by auto
1.211 -  next case (insert k d) have k[intro]:"k<DIM('a)" using insert by auto
1.212 -    have s': "bounded ((\<lambda>x. x \$\$ k) ` s)" using `bounded s` by (rule bounded_component)
1.213 +  next case (insert k d) have k[intro]:"k\<in>Basis" using insert by auto
1.214 +    have s': "bounded ((\<lambda>x. x \<bullet> k) ` s)" using `bounded s`
1.215 +      by (auto intro!: bounded_linear_image bounded_linear_inner_left)
1.216      obtain l1::"'a" and r1 where r1:"subseq r1" and
1.217 -      lr1:"\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) \$\$ i) (l1 \$\$ i) < e) sequentially"
1.218 +      lr1:"\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) \<bullet> i) (l1 \<bullet> i) < e) sequentially"
1.219        using insert(3) using insert(4) by auto
1.220 -    have f': "\<forall>n. f (r1 n) \$\$ k \<in> (\<lambda>x. x \$\$ k) ` s" using `\<forall>n. f n \<in> s` by simp
1.221 -    obtain l2 r2 where r2:"subseq r2" and lr2:"((\<lambda>i. f (r1 (r2 i)) \$\$ k) ---> l2) sequentially"
1.222 +    have f': "\<forall>n. f (r1 n) \<bullet> k \<in> (\<lambda>x. x \<bullet> k) ` s" using `\<forall>n. f n \<in> s` by simp
1.223 +    obtain l2 r2 where r2:"subseq r2" and lr2:"((\<lambda>i. f (r1 (r2 i)) \<bullet> k) ---> l2) sequentially"
1.224        using bounded_imp_convergent_subsequence[OF s' f'] unfolding o_def by auto
1.225      def r \<equiv> "r1 \<circ> r2" have r:"subseq r"
1.226        using r1 and r2 unfolding r_def o_def subseq_def by auto
1.227      moreover
1.228 -    def l \<equiv> "(\<chi>\<chi> i. if i = k then l2 else l1\$\$i)::'a"
1.229 +    def l \<equiv> "(\<Sum>i\<in>Basis. (if i = k then l2 else l1\<bullet>i) *\<^sub>R i)::'a"
1.230      { fix e::real assume "e>0"
1.231 -      from lr1 `e>0` have N1:"eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) \$\$ i) (l1 \$\$ i) < e) sequentially" by blast
1.232 -      from lr2 `e>0` have N2:"eventually (\<lambda>n. dist (f (r1 (r2 n)) \$\$ k) l2 < e) sequentially" by (rule tendstoD)
1.233 -      from r2 N1 have N1': "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 (r2 n)) \$\$ i) (l1 \$\$ i) < e) sequentially"
1.234 +      from lr1 `e>0` have N1:"eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) \<bullet> i) (l1 \<bullet> i) < e) sequentially" by blast
1.235 +      from lr2 `e>0` have N2:"eventually (\<lambda>n. dist (f (r1 (r2 n)) \<bullet> k) l2 < e) sequentially" by (rule tendstoD)
1.236 +      from r2 N1 have N1': "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 (r2 n)) \<bullet> i) (l1 \<bullet> i) < e) sequentially"
1.237          by (rule eventually_subseq)
1.238 -      have "eventually (\<lambda>n. \<forall>i\<in>(insert k d). dist (f (r n) \$\$ i) (l \$\$ i) < e) sequentially"
1.239 -        using N1' N2 apply(rule eventually_elim2) unfolding l_def r_def o_def
1.240 -        using insert.prems by auto
1.241 +      have "eventually (\<lambda>n. \<forall>i\<in>(insert k d). dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially"
1.242 +        using N1' N2
1.243 +        by eventually_elim (insert insert.prems, auto simp: l_def r_def o_def)
1.244      }
1.245      ultimately show ?case by auto
1.246    qed
1.247 -  thus "\<exists>l::'a. \<exists>r. subseq r \<and>
1.248 -      (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d'. dist (f (r n) \$\$ i) (l \$\$ i) < e) sequentially)"
1.249 -    apply safe apply(rule_tac x=l in exI,rule_tac x=r in exI) apply safe
1.250 -    apply(erule_tac x=e in allE) unfolding d_def eventually_sequentially apply safe
1.251 -    apply(rule_tac x=N in exI) apply safe apply(erule_tac x=n in allE,safe)
1.252 -    apply(erule_tac x=i in ballE)
1.253 -  proof- fix i and r::"nat=>nat" and n::nat and e::real and l::'a
1.254 -    assume "i\<in>d'" "i \<notin> d' \<inter> {..<DIM('a)}" and e:"e>0"
1.255 -    hence *:"i\<ge>DIM('a)" by auto
1.256 -    thus "dist (f (r n) \$\$ i) (l \$\$ i) < e" using e by auto
1.257 -  qed
1.258  qed
1.259
1.260  instance euclidean_space \<subseteq> heine_borel
1.261 @@ -2431,22 +2408,20 @@
1.262    fix s :: "'a set" and f :: "nat \<Rightarrow> 'a"
1.263    assume s: "bounded s" and f: "\<forall>n. f n \<in> s"
1.264    then obtain l::'a and r where r: "subseq r"
1.265 -    and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>UNIV. dist (f (r n) \$\$ i) (l \$\$ i) < e) sequentially"
1.266 +    and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially"
1.267      using compact_lemma [OF s f] by blast
1.268 -  let ?d = "{..<DIM('a)}"
1.269    { fix e::real assume "e>0"
1.270 -    hence "0 < e / (real_of_nat (card ?d))"
1.271 -      using DIM_positive using divide_pos_pos[of e, of "real_of_nat (card ?d)"] by auto
1.272 -    with l have "eventually (\<lambda>n. \<forall>i. dist (f (r n) \$\$ i) (l \$\$ i) < e / (real_of_nat (card ?d))) sequentially"
1.273 +    hence "0 < e / real_of_nat DIM('a)" by (auto intro!: divide_pos_pos DIM_positive)
1.274 +    with l have "eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e / (real_of_nat DIM('a))) sequentially"
1.275        by simp
1.276      moreover
1.277 -    { fix n assume n: "\<forall>i. dist (f (r n) \$\$ i) (l \$\$ i) < e / (real_of_nat (card ?d))"
1.278 -      have "dist (f (r n)) l \<le> (\<Sum>i\<in>?d. dist (f (r n) \$\$ i) (l \$\$ i))"
1.279 +    { fix n assume n: "\<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e / (real_of_nat DIM('a))"
1.280 +      have "dist (f (r n)) l \<le> (\<Sum>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i))"
1.281          apply(subst euclidean_dist_l2) using zero_le_dist by (rule setL2_le_setsum)
1.282 -      also have "\<dots> < (\<Sum>i\<in>?d. e / (real_of_nat (card ?d)))"
1.283 +      also have "\<dots> < (\<Sum>i\<in>(Basis::'a set). e / (real_of_nat DIM('a)))"
1.284          apply(rule setsum_strict_mono) using n by auto
1.285 -      finally have "dist (f (r n)) l < e" unfolding setsum_constant
1.286 -        using DIM_positive[where 'a='a] by auto
1.287 +      finally have "dist (f (r n)) l < e"
1.288 +        by auto
1.289      }
1.290      ultimately have "eventually (\<lambda>n. dist (f (r n)) l < e) sequentially"
1.291        by (rule eventually_elim1)
1.292 @@ -3885,10 +3860,6 @@
1.293    shows "continuous F (\<lambda>x. inner (f x) (g x))"
1.294    using assms unfolding continuous_def by (rule tendsto_inner)
1.295
1.296 -lemma continuous_euclidean_component:
1.297 -  shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. f x \$\$ i)"
1.298 -  unfolding continuous_def by (rule tendsto_euclidean_component)
1.299 -
1.300  lemma continuous_inverse:
1.301    fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra"
1.302    assumes "continuous F f" and "f (netlimit F) \<noteq> 0"
1.303 @@ -3909,10 +3880,8 @@
1.304
1.305  lemmas continuous_intros = continuous_at_id continuous_within_id
1.306    continuous_const continuous_dist continuous_norm continuous_infnorm
1.308 -  continuous_scaleR continuous_mult
1.309 -  continuous_inner continuous_euclidean_component
1.310 -  continuous_at_inverse continuous_at_within_inverse
1.311 +  continuous_add continuous_minus continuous_diff continuous_scaleR continuous_mult
1.312 +  continuous_inner continuous_at_inverse continuous_at_within_inverse
1.313
1.314  subsubsection {* Structural rules for setwise continuity *}
1.315
1.316 @@ -3976,11 +3945,6 @@
1.317    using bounded_bilinear_inner assms
1.318    by (rule bounded_bilinear.continuous_on)
1.319
1.320 -lemma continuous_on_euclidean_component:
1.321 -  "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. f x \$\$ i)"
1.322 -  using bounded_linear_euclidean_component
1.323 -  by (rule bounded_linear.continuous_on)
1.324 -
1.325  lemma continuous_on_inverse:
1.326    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_div_algebra"
1.327    assumes "continuous_on s f" and "\<forall>x\<in>s. f x \<noteq> 0"
1.328 @@ -4110,7 +4074,7 @@
1.329    continuous_on_compose continuous_on_norm continuous_on_infnorm
1.331    continuous_on_scaleR continuous_on_mult continuous_on_inverse
1.332 -  continuous_on_inner continuous_on_euclidean_component
1.333 +  continuous_on_inner
1.334    uniformly_continuous_on_id uniformly_continuous_on_const
1.335    uniformly_continuous_on_dist uniformly_continuous_on_norm
1.337 @@ -5070,65 +5034,64 @@
1.338  subsection {* Intervals *}
1.339
1.340  lemma interval: fixes a :: "'a::ordered_euclidean_space" shows
1.341 -  "{a <..< b} = {x::'a. \<forall>i<DIM('a). a\$\$i < x\$\$i \<and> x\$\$i < b\$\$i}" and
1.342 -  "{a .. b} = {x::'a. \<forall>i<DIM('a). a\$\$i \<le> x\$\$i \<and> x\$\$i \<le> b\$\$i}"
1.343 +  "{a <..< b} = {x::'a. \<forall>i\<in>Basis. a\<bullet>i < x\<bullet>i \<and> x\<bullet>i < b\<bullet>i}" and
1.344 +  "{a .. b} = {x::'a. \<forall>i\<in>Basis. a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i}"
1.345    by(auto simp add:set_eq_iff eucl_le[where 'a='a] eucl_less[where 'a='a])
1.346
1.347  lemma mem_interval: fixes a :: "'a::ordered_euclidean_space" shows
1.348 -  "x \<in> {a<..<b} \<longleftrightarrow> (\<forall>i<DIM('a). a\$\$i < x\$\$i \<and> x\$\$i < b\$\$i)"
1.349 -  "x \<in> {a .. b} \<longleftrightarrow> (\<forall>i<DIM('a). a\$\$i \<le> x\$\$i \<and> x\$\$i \<le> b\$\$i)"
1.350 +  "x \<in> {a<..<b} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < x\<bullet>i \<and> x\<bullet>i < b\<bullet>i)"
1.351 +  "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.352    using interval[of a b] by(auto simp add: set_eq_iff eucl_le[where 'a='a] eucl_less[where 'a='a])
1.353
1.354  lemma interval_eq_empty: fixes a :: "'a::ordered_euclidean_space" shows
1.355 - "({a <..< b} = {} \<longleftrightarrow> (\<exists>i<DIM('a). b\$\$i \<le> a\$\$i))" (is ?th1) and
1.356 - "({a  ..  b} = {} \<longleftrightarrow> (\<exists>i<DIM('a). b\$\$i < a\$\$i))" (is ?th2)
1.357 + "({a <..< b} = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i))" (is ?th1) and
1.358 + "({a  ..  b} = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i < a\<bullet>i))" (is ?th2)
1.359  proof-
1.360 -  { fix i x assume i:"i<DIM('a)" and as:"b\$\$i \<le> a\$\$i" and x:"x\<in>{a <..< b}"
1.361 -    hence "a \$\$ i < x \$\$ i \<and> x \$\$ i < b \$\$ i" unfolding mem_interval by auto
1.362 -    hence "a\$\$i < b\$\$i" by auto
1.363 +  { fix i x assume i:"i\<in>Basis" and as:"b\<bullet>i \<le> a\<bullet>i" and x:"x\<in>{a <..< b}"
1.364 +    hence "a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i" unfolding mem_interval by auto
1.365 +    hence "a\<bullet>i < b\<bullet>i" by auto
1.366      hence False using as by auto  }
1.367    moreover
1.368 -  { assume as:"\<forall>i<DIM('a). \<not> (b\$\$i \<le> a\$\$i)"
1.369 +  { assume as:"\<forall>i\<in>Basis. \<not> (b\<bullet>i \<le> a\<bullet>i)"
1.370      let ?x = "(1/2) *\<^sub>R (a + b)"
1.371 -    { fix i assume i:"i<DIM('a)"
1.372 -      have "a\$\$i < b\$\$i" using as[THEN spec[where x=i]] using i by auto
1.373 -      hence "a\$\$i < ((1/2) *\<^sub>R (a+b)) \$\$ i" "((1/2) *\<^sub>R (a+b)) \$\$ i < b\$\$i"
1.374 -        unfolding euclidean_simps by auto }
1.375 +    { fix i :: 'a assume i:"i\<in>Basis"
1.376 +      have "a\<bullet>i < b\<bullet>i" using as[THEN bspec[where x=i]] i by auto
1.377 +      hence "a\<bullet>i < ((1/2) *\<^sub>R (a+b)) \<bullet> i" "((1/2) *\<^sub>R (a+b)) \<bullet> i < b\<bullet>i"
1.378 +        by (auto simp: inner_add_left) }
1.379      hence "{a <..< b} \<noteq> {}" using mem_interval(1)[of "?x" a b] by auto  }
1.380    ultimately show ?th1 by blast
1.381
1.382 -  { fix i x assume i:"i<DIM('a)" and as:"b\$\$i < a\$\$i" and x:"x\<in>{a .. b}"
1.383 -    hence "a \$\$ i \<le> x \$\$ i \<and> x \$\$ i \<le> b \$\$ i" unfolding mem_interval by auto
1.384 -    hence "a\$\$i \<le> b\$\$i" by auto
1.385 +  { fix i x assume i:"i\<in>Basis" and as:"b\<bullet>i < a\<bullet>i" and x:"x\<in>{a .. b}"
1.386 +    hence "a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i" unfolding mem_interval by auto
1.387 +    hence "a\<bullet>i \<le> b\<bullet>i" by auto
1.388      hence False using as by auto  }
1.389    moreover
1.390 -  { assume as:"\<forall>i<DIM('a). \<not> (b\$\$i < a\$\$i)"
1.391 +  { assume as:"\<forall>i\<in>Basis. \<not> (b\<bullet>i < a\<bullet>i)"
1.392      let ?x = "(1/2) *\<^sub>R (a + b)"
1.393 -    { fix i assume i:"i<DIM('a)"
1.394 -      have "a\$\$i \<le> b\$\$i" using as[THEN spec[where x=i]] by auto
1.395 -      hence "a\$\$i \<le> ((1/2) *\<^sub>R (a+b)) \$\$ i" "((1/2) *\<^sub>R (a+b)) \$\$ i \<le> b\$\$i"
1.396 -        unfolding euclidean_simps by auto }
1.397 +    { fix i :: 'a assume i:"i\<in>Basis"
1.398 +      have "a\<bullet>i \<le> b\<bullet>i" using as[THEN bspec[where x=i]] i by auto
1.399 +      hence "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.400 +        by (auto simp: inner_add_left) }
1.401      hence "{a .. b} \<noteq> {}" using mem_interval(2)[of "?x" a b] by auto  }
1.402    ultimately show ?th2 by blast
1.403  qed
1.404
1.405  lemma interval_ne_empty: fixes a :: "'a::ordered_euclidean_space" shows
1.406 -  "{a  ..  b} \<noteq> {} \<longleftrightarrow> (\<forall>i<DIM('a). a\$\$i \<le> b\$\$i)" and
1.407 -  "{a <..< b} \<noteq> {} \<longleftrightarrow> (\<forall>i<DIM('a). a\$\$i < b\$\$i)"
1.408 +  "{a  ..  b} \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i)" and
1.409 +  "{a <..< b} \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)"
1.410    unfolding interval_eq_empty[of a b] by fastforce+
1.411
1.412  lemma interval_sing:
1.413    fixes a :: "'a::ordered_euclidean_space"
1.414    shows "{a .. a} = {a}" and "{a<..<a} = {}"
1.415    unfolding set_eq_iff mem_interval eq_iff [symmetric]
1.416 -  by (auto simp add: euclidean_eq[where 'a='a] eq_commute
1.417 -    eucl_less[where 'a='a] eucl_le[where 'a='a])
1.418 +  by (auto intro: euclidean_eqI simp: ex_in_conv)
1.419
1.420  lemma subset_interval_imp: fixes a :: "'a::ordered_euclidean_space" shows
1.421 - "(\<forall>i<DIM('a). a\$\$i \<le> c\$\$i \<and> d\$\$i \<le> b\$\$i) \<Longrightarrow> {c .. d} \<subseteq> {a .. b}" and
1.422 - "(\<forall>i<DIM('a). a\$\$i < c\$\$i \<and> d\$\$i < b\$\$i) \<Longrightarrow> {c .. d} \<subseteq> {a<..<b}" and
1.423 - "(\<forall>i<DIM('a). a\$\$i \<le> c\$\$i \<and> d\$\$i \<le> b\$\$i) \<Longrightarrow> {c<..<d} \<subseteq> {a .. b}" and
1.424 - "(\<forall>i<DIM('a). a\$\$i \<le> c\$\$i \<and> d\$\$i \<le> b\$\$i) \<Longrightarrow> {c<..<d} \<subseteq> {a<..<b}"
1.425 + "(\<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}" and
1.426 + "(\<forall>i\<in>Basis. a\<bullet>i < c\<bullet>i \<and> d\<bullet>i < b\<bullet>i) \<Longrightarrow> {c .. d} \<subseteq> {a<..<b}" and
1.427 + "(\<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}" and
1.428 + "(\<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.429    unfolding subset_eq[unfolded Ball_def] unfolding mem_interval
1.430    by (best intro: order_trans less_le_trans le_less_trans less_imp_le)+
1.431
1.432 @@ -5139,94 +5102,96 @@
1.433    by (fast intro: less_imp_le)
1.434
1.435  lemma subset_interval: fixes a :: "'a::ordered_euclidean_space" shows
1.436 - "{c .. d} \<subseteq> {a .. b} \<longleftrightarrow> (\<forall>i<DIM('a). c\$\$i \<le> d\$\$i) --> (\<forall>i<DIM('a). a\$\$i \<le> c\$\$i \<and> d\$\$i \<le> b\$\$i)" (is ?th1) and
1.437 - "{c .. d} \<subseteq> {a<..<b} \<longleftrightarrow> (\<forall>i<DIM('a). c\$\$i \<le> d\$\$i) --> (\<forall>i<DIM('a). a\$\$i < c\$\$i \<and> d\$\$i < b\$\$i)" (is ?th2) and
1.438 - "{c<..<d} \<subseteq> {a .. b} \<longleftrightarrow> (\<forall>i<DIM('a). c\$\$i < d\$\$i) --> (\<forall>i<DIM('a). a\$\$i \<le> c\$\$i \<and> d\$\$i \<le> b\$\$i)" (is ?th3) and
1.439 - "{c<..<d} \<subseteq> {a<..<b} \<longleftrightarrow> (\<forall>i<DIM('a). c\$\$i < d\$\$i) --> (\<forall>i<DIM('a). a\$\$i \<le> c\$\$i \<and> d\$\$i \<le> b\$\$i)" (is ?th4)
1.440 + "{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) and
1.441 + "{c .. d} \<subseteq> {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) and
1.442 + "{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) and
1.443 + "{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 ?th4)
1.444  proof-
1.445    show ?th1 unfolding subset_eq and Ball_def and mem_interval by (auto intro: order_trans)
1.446    show ?th2 unfolding subset_eq and Ball_def and mem_interval by (auto intro: le_less_trans less_le_trans order_trans less_imp_le)
1.447 -  { assume as: "{c<..<d} \<subseteq> {a .. b}" "\<forall>i<DIM('a). c\$\$i < d\$\$i"
1.448 +  { assume as: "{c<..<d} \<subseteq> {a .. b}" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
1.449      hence "{c<..<d} \<noteq> {}" unfolding interval_eq_empty by auto
1.450 -    fix i assume i:"i<DIM('a)"
1.451 +    fix i :: 'a assume i:"i\<in>Basis"
1.452      (** TODO combine the following two parts as done in the HOL_light version. **)
1.453 -    { let ?x = "(\<chi>\<chi> j. (if j=i then ((min (a\$\$j) (d\$\$j))+c\$\$j)/2 else (c\$\$j+d\$\$j)/2))::'a"
1.454 -      assume as2: "a\$\$i > c\$\$i"
1.455 -      { fix j assume j:"j<DIM('a)"
1.456 -        hence "c \$\$ j < ?x \$\$ j \<and> ?x \$\$ j < d \$\$ j"
1.457 -          apply(cases "j=i") using as(2)[THEN spec[where x=j]] i
1.458 +    { 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.459 +      assume as2: "a\<bullet>i > c\<bullet>i"
1.460 +      { fix j :: 'a assume j:"j\<in>Basis"
1.461 +        hence "c \<bullet> j < ?x \<bullet> j \<and> ?x \<bullet> j < d \<bullet> j"
1.462 +          apply(cases "j=i") using as(2)[THEN bspec[where x=j]] i
1.463            by (auto simp add: as2)  }
1.464        hence "?x\<in>{c<..<d}" using i unfolding mem_interval by auto
1.465        moreover
1.466        have "?x\<notin>{a .. b}"
1.467 -        unfolding mem_interval apply auto apply(rule_tac x=i in exI)
1.468 -        using as(2)[THEN spec[where x=i]] and as2 i
1.469 +        unfolding mem_interval apply auto apply(rule_tac x=i in bexI)
1.470 +        using as(2)[THEN bspec[where x=i]] and as2 i
1.471          by auto
1.472        ultimately have False using as by auto  }
1.473 -    hence "a\$\$i \<le> c\$\$i" by(rule ccontr)auto
1.474 +    hence "a\<bullet>i \<le> c\<bullet>i" by(rule ccontr)auto
1.475      moreover
1.476 -    { let ?x = "(\<chi>\<chi> j. (if j=i then ((max (b\$\$j) (c\$\$j))+d\$\$j)/2 else (c\$\$j+d\$\$j)/2))::'a"
1.477 -      assume as2: "b\$\$i < d\$\$i"
1.478 -      { fix j assume "j<DIM('a)"
1.479 -        hence "d \$\$ j > ?x \$\$ j \<and> ?x \$\$ j > c \$\$ j"
1.480 -          apply(cases "j=i") using as(2)[THEN spec[where x=j]]
1.481 -          by (auto simp add: as2)  }
1.482 +    { 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.483 +      assume as2: "b\<bullet>i < d\<bullet>i"
1.484 +      { fix j :: 'a assume "j\<in>Basis"
1.485 +        hence "d \<bullet> j > ?x \<bullet> j \<and> ?x \<bullet> j > c \<bullet> j"
1.486 +          apply(cases "j=i") using as(2)[THEN bspec[where x=j]]
1.487 +          by (auto simp add: as2) }
1.488        hence "?x\<in>{c<..<d}" unfolding mem_interval by auto
1.489        moreover
1.490        have "?x\<notin>{a .. b}"
1.491 -        unfolding mem_interval apply auto apply(rule_tac x=i in exI)
1.492 -        using as(2)[THEN spec[where x=i]] and as2 using i
1.493 +        unfolding mem_interval apply auto apply(rule_tac x=i in bexI)
1.494 +        using as(2)[THEN bspec[where x=i]] and as2 using i
1.495          by auto
1.496        ultimately have False using as by auto  }
1.497 -    hence "b\$\$i \<ge> d\$\$i" by(rule ccontr)auto
1.498 +    hence "b\<bullet>i \<ge> d\<bullet>i" by(rule ccontr)auto
1.499      ultimately
1.500 -    have "a\$\$i \<le> c\$\$i \<and> d\$\$i \<le> b\$\$i" by auto
1.501 +    have "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i" by auto
1.502    } note part1 = this
1.503 -  show ?th3 unfolding subset_eq and Ball_def and mem_interval
1.504 -    apply(rule,rule,rule,rule) apply(rule part1) unfolding subset_eq and Ball_def and mem_interval
1.505 -    prefer 4 apply auto by(erule_tac x=i in allE,erule_tac x=i in allE,fastforce)+
1.506 -  { assume as:"{c<..<d} \<subseteq> {a<..<b}" "\<forall>i<DIM('a). c\$\$i < d\$\$i"
1.507 -    fix i assume i:"i<DIM('a)"
1.508 +  show ?th3
1.509 +    unfolding subset_eq and Ball_def and mem_interval
1.510 +    apply(rule,rule,rule,rule)
1.511 +    apply(rule part1)
1.512 +    unfolding subset_eq and Ball_def and mem_interval
1.513 +    prefer 4
1.514 +    apply auto
1.515 +    by(erule_tac x=xa in allE,erule_tac x=xa in allE,fastforce)+
1.516 +  { assume as:"{c<..<d} \<subseteq> {a<..<b}" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i"
1.517 +    fix i :: 'a assume i:"i\<in>Basis"
1.518      from as(1) have "{c<..<d} \<subseteq> {a..b}" using interval_open_subset_closed[of a b] by auto
1.519 -    hence "a\$\$i \<le> c\$\$i \<and> d\$\$i \<le> b\$\$i" using part1 and as(2) using i by auto  } note * = this
1.520 +    hence "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i" using part1 and as(2) using i by auto  } note * = this
1.521    show ?th4 unfolding subset_eq and Ball_def and mem_interval
1.522      apply(rule,rule,rule,rule) apply(rule *) unfolding subset_eq and Ball_def and mem_interval prefer 4
1.523 -    apply auto by(erule_tac x=i in allE, simp)+
1.524 -qed
1.525 -
1.526 -lemma disjoint_interval: fixes a::"'a::ordered_euclidean_space" shows
1.527 -  "{a .. b} \<inter> {c .. d} = {} \<longleftrightarrow> (\<exists>i<DIM('a). (b\$\$i < a\$\$i \<or> d\$\$i < c\$\$i \<or> b\$\$i < c\$\$i \<or> d\$\$i < a\$\$i))" (is ?th1) and
1.528 -  "{a .. b} \<inter> {c<..<d} = {} \<longleftrightarrow> (\<exists>i<DIM('a). (b\$\$i < a\$\$i \<or> d\$\$i \<le> c\$\$i \<or> b\$\$i \<le> c\$\$i \<or> d\$\$i \<le> a\$\$i))" (is ?th2) and
1.529 -  "{a<..<b} \<inter> {c .. d} = {} \<longleftrightarrow> (\<exists>i<DIM('a). (b\$\$i \<le> a\$\$i \<or> d\$\$i < c\$\$i \<or> b\$\$i \<le> c\$\$i \<or> d\$\$i \<le> a\$\$i))" (is ?th3) and
1.530 -  "{a<..<b} \<inter> {c<..<d} = {} \<longleftrightarrow> (\<exists>i<DIM('a). (b\$\$i \<le> a\$\$i \<or> d\$\$i \<le> c\$\$i \<or> b\$\$i \<le> c\$\$i \<or> d\$\$i \<le> a\$\$i))" (is ?th4)
1.531 -proof-
1.532 -  let ?z = "(\<chi>\<chi> i. ((max (a\$\$i) (c\$\$i)) + (min (b\$\$i) (d\$\$i))) / 2)::'a"
1.533 -  note * = set_eq_iff Int_iff empty_iff mem_interval all_conj_distrib[THEN sym] eq_False
1.534 -  show ?th1 unfolding * apply safe apply(erule_tac x="?z" in allE)
1.535 -    unfolding not_all apply(erule exE,rule_tac x=x in exI) apply(erule_tac[2-] x=i in allE) by auto
1.536 -  show ?th2 unfolding * apply safe apply(erule_tac x="?z" in allE)
1.537 -    unfolding not_all apply(erule exE,rule_tac x=x in exI) apply(erule_tac[2-] x=i in allE) by auto
1.538 -  show ?th3 unfolding * apply safe apply(erule_tac x="?z" in allE)
1.539 -    unfolding not_all apply(erule exE,rule_tac x=x in exI) apply(erule_tac[2-] x=i in allE) by auto
1.540 -  show ?th4 unfolding * apply safe apply(erule_tac x="?z" in allE)
1.541 -    unfolding not_all apply(erule exE,rule_tac x=x in exI) apply(erule_tac[2-] x=i in allE) by auto
1.542 +    apply auto by(erule_tac x=xa in allE, simp)+
1.543  qed
1.544
1.545  lemma inter_interval: fixes a :: "'a::ordered_euclidean_space" shows
1.546 - "{a .. b} \<inter> {c .. d} =  {(\<chi>\<chi> i. max (a\$\$i) (c\$\$i)) .. (\<chi>\<chi> i. min (b\$\$i) (d\$\$i))}"
1.547 -  unfolding set_eq_iff and Int_iff and mem_interval
1.548 -  by auto
1.549 + "{a .. b} \<inter> {c .. d} =  {(\<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.550 +  unfolding set_eq_iff and Int_iff and mem_interval by auto
1.551 +
1.552 +lemma disjoint_interval: fixes a::"'a::ordered_euclidean_space" shows
1.553 +  "{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) and
1.554 +  "{a .. b} \<inter> {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) and
1.555 +  "{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) and
1.556 +  "{a<..<b} \<inter> {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.557 +proof-
1.558 +  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.559 +  have **: "\<And>P Q. (\<And>i :: 'a. i \<in> Basis \<Longrightarrow> Q ?z i \<Longrightarrow> P i) \<Longrightarrow>
1.560 +      (\<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.561 +    by blast
1.562 +  note * = set_eq_iff Int_iff empty_iff mem_interval ball_conj_distrib[symmetric] eq_False ball_simps(10)
1.563 +  show ?th1 unfolding * by (intro **) auto
1.564 +  show ?th2 unfolding * by (intro **) auto
1.565 +  show ?th3 unfolding * by (intro **) auto
1.566 +  show ?th4 unfolding * by (intro **) auto
1.567 +qed
1.568
1.569  (* Moved interval_open_subset_closed a bit upwards *)
1.570
1.571  lemma open_interval[intro]:
1.572    fixes a b :: "'a::ordered_euclidean_space" shows "open {a<..<b}"
1.573  proof-
1.574 -  have "open (\<Inter>i<DIM('a). (\<lambda>x. x\$\$i) -` {a\$\$i<..<b\$\$i})"
1.575 +  have "open (\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i<..<b\<bullet>i})"
1.576      by (intro open_INT finite_lessThan ballI continuous_open_vimage allI
1.577 -      linear_continuous_at bounded_linear_euclidean_component
1.578 -      open_real_greaterThanLessThan)
1.579 -  also have "(\<Inter>i<DIM('a). (\<lambda>x. x\$\$i) -` {a\$\$i<..<b\$\$i}) = {a<..<b}"
1.580 +      linear_continuous_at open_real_greaterThanLessThan finite_Basis bounded_linear_inner_left)
1.581 +  also have "(\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i<..<b\<bullet>i}) = {a<..<b}"
1.582      by (auto simp add: eucl_less [where 'a='a])
1.583    finally show "open {a<..<b}" .
1.584  qed
1.585 @@ -5234,11 +5199,10 @@
1.586  lemma closed_interval[intro]:
1.587    fixes a b :: "'a::ordered_euclidean_space" shows "closed {a .. b}"
1.588  proof-
1.589 -  have "closed (\<Inter>i<DIM('a). (\<lambda>x. x\$\$i) -` {a\$\$i .. b\$\$i})"
1.590 +  have "closed (\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i .. b\<bullet>i})"
1.591      by (intro closed_INT ballI continuous_closed_vimage allI
1.592 -      linear_continuous_at bounded_linear_euclidean_component
1.593 -      closed_real_atLeastAtMost)
1.594 -  also have "(\<Inter>i<DIM('a). (\<lambda>x. x\$\$i) -` {a\$\$i .. b\$\$i}) = {a .. b}"
1.595 +      linear_continuous_at closed_real_atLeastAtMost finite_Basis bounded_linear_inner_left)
1.596 +  also have "(\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i .. b\<bullet>i}) = {a .. b}"
1.597      by (auto simp add: eucl_le [where 'a='a])
1.598    finally show "closed {a .. b}" .
1.599  qed
1.600 @@ -5253,29 +5217,29 @@
1.601    { fix x assume "x \<in> interior {a..b}"
1.602      then obtain s where s:"open s" "x \<in> s" "s \<subseteq> {a..b}" ..
1.603      then obtain e where "e>0" and e:"\<forall>x'. dist x' x < e \<longrightarrow> x' \<in> {a..b}" unfolding open_dist and subset_eq by auto
1.604 -    { fix i assume i:"i<DIM('a)"
1.605 -      have "dist (x - (e / 2) *\<^sub>R basis i) x < e"
1.606 -           "dist (x + (e / 2) *\<^sub>R basis i) x < e"
1.607 +    { fix i :: 'a assume i:"i\<in>Basis"
1.608 +      have "dist (x - (e / 2) *\<^sub>R i) x < e"
1.609 +           "dist (x + (e / 2) *\<^sub>R i) x < e"
1.610          unfolding dist_norm apply auto
1.611 -        unfolding norm_minus_cancel using norm_basis and `e>0` by auto
1.612 -      hence "a \$\$ i \<le> (x - (e / 2) *\<^sub>R basis i) \$\$ i"
1.613 -                     "(x + (e / 2) *\<^sub>R basis i) \$\$ i \<le> b \$\$ i"
1.614 -        using e[THEN spec[where x="x - (e/2) *\<^sub>R basis i"]]
1.615 -        and   e[THEN spec[where x="x + (e/2) *\<^sub>R basis i"]]
1.616 +        unfolding norm_minus_cancel using norm_Basis[OF i] `e>0` by auto
1.617 +      hence "a \<bullet> i \<le> (x - (e / 2) *\<^sub>R i) \<bullet> i"
1.618 +                     "(x + (e / 2) *\<^sub>R i) \<bullet> i \<le> b \<bullet> i"
1.619 +        using e[THEN spec[where x="x - (e/2) *\<^sub>R i"]]
1.620 +        and   e[THEN spec[where x="x + (e/2) *\<^sub>R i"]]
1.621          unfolding mem_interval using i by blast+
1.622 -      hence "a \$\$ i < x \$\$ i" and "x \$\$ i < b \$\$ i" unfolding euclidean_simps
1.623 -        unfolding basis_component using `e>0` i by auto  }
1.624 +      hence "a \<bullet> i < x \<bullet> i" and "x \<bullet> i < b \<bullet> i"
1.625 +        using `e>0` i by (auto simp: inner_diff_left inner_Basis inner_add_left) }
1.626      hence "x \<in> {a<..<b}" unfolding mem_interval by auto  }
1.627    thus "?L \<subseteq> ?R" ..
1.628  qed
1.629
1.630  lemma bounded_closed_interval: fixes a :: "'a::ordered_euclidean_space" shows "bounded {a .. b}"
1.631  proof-
1.632 -  let ?b = "\<Sum>i<DIM('a). \<bar>a\$\$i\<bar> + \<bar>b\$\$i\<bar>"
1.633 -  { fix x::"'a" assume x:"\<forall>i<DIM('a). a \$\$ i \<le> x \$\$ i \<and> x \$\$ i \<le> b \$\$ i"
1.634 -    { fix i assume "i<DIM('a)"
1.635 -      hence "\<bar>x\$\$i\<bar> \<le> \<bar>a\$\$i\<bar> + \<bar>b\$\$i\<bar>" using x[THEN spec[where x=i]] by auto  }
1.636 -    hence "(\<Sum>i<DIM('a). \<bar>x \$\$ i\<bar>) \<le> ?b" apply-apply(rule setsum_mono) by auto
1.637 +  let ?b = "\<Sum>i\<in>Basis. \<bar>a\<bullet>i\<bar> + \<bar>b\<bullet>i\<bar>"
1.638 +  { fix x::"'a" assume x:"\<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i"
1.639 +    { fix i :: 'a assume "i\<in>Basis"
1.640 +      hence "\<bar>x\<bullet>i\<bar> \<le> \<bar>a\<bullet>i\<bar> + \<bar>b\<bullet>i\<bar>" using x[THEN bspec[where x=i]] by auto  }
1.641 +    hence "(\<Sum>i\<in>Basis. \<bar>x \<bullet> i\<bar>) \<le> ?b" apply-apply(rule setsum_mono) by auto
1.642      hence "norm x \<le> ?b" using norm_le_l1[of x] by auto  }
1.643    thus ?thesis unfolding interval and bounded_iff by auto
1.644  qed
1.645 @@ -5298,10 +5262,9 @@
1.646  lemma open_interval_midpoint: fixes a :: "'a::ordered_euclidean_space"
1.647    assumes "{a<..<b} \<noteq> {}" shows "((1/2) *\<^sub>R (a + b)) \<in> {a<..<b}"
1.648  proof-
1.649 -  { fix i assume "i<DIM('a)"
1.650 -    hence "a \$\$ i < ((1 / 2) *\<^sub>R (a + b)) \$\$ i \<and> ((1 / 2) *\<^sub>R (a + b)) \$\$ i < b \$\$ i"
1.651 -      using assms[unfolded interval_ne_empty, THEN spec[where x=i]]
1.652 -      unfolding euclidean_simps by auto  }
1.653 +  { fix i :: 'a assume "i\<in>Basis"
1.654 +    hence "a \<bullet> i < ((1 / 2) *\<^sub>R (a + b)) \<bullet> i \<and> ((1 / 2) *\<^sub>R (a + b)) \<bullet> i < b \<bullet> i"
1.655 +      using assms[unfolded interval_ne_empty, THEN bspec[where x=i]] by (auto simp: inner_add_left)  }
1.656    thus ?thesis unfolding mem_interval by auto
1.657  qed
1.658
1.659 @@ -5309,23 +5272,23 @@
1.660    assumes x:"x \<in> {a<..<b}" and y:"y \<in> {a .. b}" and e:"0 < e" "e \<le> 1"
1.661    shows "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<in> {a<..<b}"
1.662  proof-
1.663 -  { fix i assume i:"i<DIM('a)"
1.664 -    have "a \$\$ i = e * a\$\$i + (1 - e) * a\$\$i" unfolding left_diff_distrib by simp
1.665 -    also have "\<dots> < e * x \$\$ i + (1 - e) * y \$\$ i" apply(rule add_less_le_mono)
1.666 +  { fix i :: 'a assume i:"i\<in>Basis"
1.667 +    have "a \<bullet> i = e * (a \<bullet> i) + (1 - e) * (a \<bullet> i)" unfolding left_diff_distrib by simp
1.668 +    also have "\<dots> < e * (x \<bullet> i) + (1 - e) * (y \<bullet> i)" apply(rule add_less_le_mono)
1.669        using e unfolding mult_less_cancel_left and mult_le_cancel_left apply simp_all
1.670        using x unfolding mem_interval using i apply simp
1.671        using y unfolding mem_interval using i apply simp
1.672        done
1.673 -    finally have "a \$\$ i < (e *\<^sub>R x + (1 - e) *\<^sub>R y) \$\$ i" unfolding euclidean_simps by auto
1.674 +    finally have "a \<bullet> i < (e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i" unfolding inner_simps by auto
1.675      moreover {
1.676 -    have "b \$\$ i = e * b\$\$i + (1 - e) * b\$\$i" unfolding left_diff_distrib by simp
1.677 -    also have "\<dots> > e * x \$\$ i + (1 - e) * y \$\$ i" apply(rule add_less_le_mono)
1.678 +    have "b \<bullet> i = e * (b\<bullet>i) + (1 - e) * (b\<bullet>i)" unfolding left_diff_distrib by simp
1.679 +    also have "\<dots> > e * (x \<bullet> i) + (1 - e) * (y \<bullet> i)" apply(rule add_less_le_mono)
1.680        using e unfolding mult_less_cancel_left and mult_le_cancel_left apply simp_all
1.681        using x unfolding mem_interval using i apply simp
1.682        using y unfolding mem_interval using i apply simp
1.683        done
1.684 -    finally have "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \$\$ i < b \$\$ i" unfolding euclidean_simps by auto
1.685 -    } ultimately have "a \$\$ i < (e *\<^sub>R x + (1 - e) *\<^sub>R y) \$\$ i \<and> (e *\<^sub>R x + (1 - e) *\<^sub>R y) \$\$ i < b \$\$ i" by auto }
1.686 +    finally have "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i < b \<bullet> i" unfolding inner_simps by auto
1.687 +    } 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" by auto }
1.688    thus ?thesis unfolding mem_interval by auto
1.689  qed
1.690
1.691 @@ -5365,11 +5328,11 @@
1.692    assumes "bounded s"  shows "\<exists>a. s \<subseteq> {-a<..<a}"
1.693  proof-
1.694    obtain b where "b>0" and b:"\<forall>x\<in>s. norm x \<le> b" using assms[unfolded bounded_pos] by auto
1.695 -  def a \<equiv> "(\<chi>\<chi> i. b+1)::'a"
1.696 +  def a \<equiv> "(\<Sum>i\<in>Basis. (b + 1) *\<^sub>R i)::'a"
1.697    { fix x assume "x\<in>s"
1.698 -    fix i assume i:"i<DIM('a)"
1.699 -    hence "(-a)\$\$i < x\$\$i" and "x\$\$i < a\$\$i" using b[THEN bspec[where x=x], OF `x\<in>s`]
1.700 -      and component_le_norm[of x i] unfolding euclidean_simps and a_def by auto  }
1.701 +    fix i :: 'a assume i:"i\<in>Basis"
1.702 +    hence "(-a)\<bullet>i < x\<bullet>i" and "x\<bullet>i < a\<bullet>i" using b[THEN bspec[where x=x], OF `x\<in>s`]
1.703 +      and Basis_le_norm[OF i, of x] unfolding inner_simps and a_def by auto }
1.704    thus ?thesis by(auto intro: exI[where x=a] simp add: eucl_less[where 'a='a])
1.705  qed
1.706
1.707 @@ -5413,59 +5376,61 @@
1.708  (* Some stuff for half-infinite intervals too; FIXME: notation?  *)
1.709
1.710  lemma closed_interval_left: fixes b::"'a::euclidean_space"
1.711 -  shows "closed {x::'a. \<forall>i<DIM('a). x\$\$i \<le> b\$\$i}"
1.712 +  shows "closed {x::'a. \<forall>i\<in>Basis. x\<bullet>i \<le> b\<bullet>i}"
1.713  proof-
1.714 -  { fix i assume i:"i<DIM('a)"
1.715 -    fix x::"'a" assume x:"\<forall>e>0. \<exists>x'\<in>{x. \<forall>i<DIM('a). x \$\$ i \<le> b \$\$ i}. x' \<noteq> x \<and> dist x' x < e"
1.716 -    { assume "x\$\$i > b\$\$i"
1.717 -      then obtain y where "y \$\$ i \<le> b \$\$ i"  "y \<noteq> x"  "dist y x < x\$\$i - b\$\$i"
1.718 -        using x[THEN spec[where x="x\$\$i - b\$\$i"]] using i by auto
1.719 -      hence False using component_le_norm[of "y - x" i] unfolding dist_norm euclidean_simps using i
1.720 -        by auto   }
1.721 -    hence "x\$\$i \<le> b\$\$i" by(rule ccontr)auto  }
1.722 +  { fix i :: 'a assume i:"i\<in>Basis"
1.723 +    fix x::"'a" assume x:"\<forall>e>0. \<exists>x'\<in>{x. \<forall>i\<in>Basis. x \<bullet> i \<le> b \<bullet> i}. x' \<noteq> x \<and> dist x' x < e"
1.724 +    { assume "x\<bullet>i > b\<bullet>i"
1.725 +      then obtain y where "y \<bullet> i \<le> b \<bullet> i"  "y \<noteq> x"  "dist y x < x\<bullet>i - b\<bullet>i"
1.726 +        using x[THEN spec[where x="x\<bullet>i - b\<bullet>i"]] using i by auto
1.727 +      hence False using Basis_le_norm[OF i, of "y - x"] unfolding dist_norm inner_simps using i
1.728 +        by auto }
1.729 +    hence "x\<bullet>i \<le> b\<bullet>i" by(rule ccontr)auto  }
1.730    thus ?thesis unfolding closed_limpt unfolding islimpt_approachable by blast
1.731  qed
1.732
1.733  lemma closed_interval_right: fixes a::"'a::euclidean_space"
1.734 -  shows "closed {x::'a. \<forall>i<DIM('a). a\$\$i \<le> x\$\$i}"
1.735 +  shows "closed {x::'a. \<forall>i\<in>Basis. a\<bullet>i \<le> x\<bullet>i}"
1.736  proof-
1.737 -  { fix i assume i:"i<DIM('a)"
1.738 -    fix x::"'a" assume x:"\<forall>e>0. \<exists>x'\<in>{x. \<forall>i<DIM('a). a \$\$ i \<le> x \$\$ i}. x' \<noteq> x \<and> dist x' x < e"
1.739 -    { assume "a\$\$i > x\$\$i"
1.740 -      then obtain y where "a \$\$ i \<le> y \$\$ i"  "y \<noteq> x"  "dist y x < a\$\$i - x\$\$i"
1.741 -        using x[THEN spec[where x="a\$\$i - x\$\$i"]] i by auto
1.742 -      hence False using component_le_norm[of "y - x" i] unfolding dist_norm and euclidean_simps by auto   }
1.743 -    hence "a\$\$i \<le> x\$\$i" by(rule ccontr)auto  }
1.744 +  { fix i :: 'a assume i:"i\<in>Basis"
1.745 +    fix x::"'a" assume x:"\<forall>e>0. \<exists>x'\<in>{x. \<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i}. x' \<noteq> x \<and> dist x' x < e"
1.746 +    { assume "a\<bullet>i > x\<bullet>i"
1.747 +      then obtain y where "a \<bullet> i \<le> y \<bullet> i"  "y \<noteq> x"  "dist y x < a\<bullet>i - x\<bullet>i"
1.748 +        using x[THEN spec[where x="a\<bullet>i - x\<bullet>i"]] i by auto
1.749 +      hence False using Basis_le_norm[OF i, of "y - x"] unfolding dist_norm inner_simps by auto }
1.750 +    hence "a\<bullet>i \<le> x\<bullet>i" by(rule ccontr)auto  }
1.751    thus ?thesis unfolding closed_limpt unfolding islimpt_approachable by blast
1.752  qed
1.753
1.754 -instance ordered_euclidean_space \<subseteq> countable_basis_space
1.755 +lemma open_box: "open (box a b)"
1.756 +proof -
1.757 +  have "open (\<Inter>i\<in>Basis. (op \<bullet> i) -` {a \<bullet> i <..< b \<bullet> i})"
1.758 +    by (auto intro!: continuous_open_vimage continuous_inner continuous_at_id continuous_const)
1.759 +  also have "(\<Inter>i\<in>Basis. (op \<bullet> i) -` {a \<bullet> i <..< b \<bullet> i}) = box a b"
1.760 +    by (auto simp add: box_def inner_commute)
1.761 +  finally show ?thesis .
1.762 +qed
1.763 +
1.764 +instance euclidean_space \<subseteq> countable_basis_space
1.765  proof
1.766 -  def to_cube \<equiv> "\<lambda>(a, b). {Chi (real_of_rat \<circ> op ! a)<..<Chi (real_of_rat \<circ> op ! b)}::'a set"
1.767 -  def B \<equiv> "(\<lambda>n. (to_cube (from_nat n)::'a set)) ` UNIV"
1.768 -  have "countable B" unfolding B_def by simp
1.769 +  def a \<equiv> "\<lambda>f :: 'a \<Rightarrow> (real \<times> real). \<Sum>i\<in>Basis. fst (f i) *\<^sub>R i"
1.770 +  then have a: "\<And>f. (\<Sum>i\<in>Basis. fst (f i) *\<^sub>R i) = a f" by simp
1.771 +  def b \<equiv> "\<lambda>f :: 'a \<Rightarrow> (real \<times> real). \<Sum>i\<in>Basis. snd (f i) *\<^sub>R i"
1.772 +  then have b: "\<And>f. (\<Sum>i\<in>Basis. snd (f i) *\<^sub>R i) = b f" by simp
1.773 +  def B \<equiv> "(\<lambda>f. box (a f) (b f)) ` (Basis \<rightarrow>\<^isub>E (\<rat> \<times> \<rat>))"
1.774 +
1.775 +  have "countable B" unfolding B_def
1.776 +    by (intro countable_image countable_PiE finite_Basis countable_SIGMA countable_rat)
1.777    moreover
1.778 -  have "Ball B open" unfolding B_def
1.779 +  have "Ball B open" by (simp add: B_def open_box)
1.780 +  moreover have "(\<forall>A. open A \<longrightarrow> (\<exists>B'\<subseteq>B. \<Union>B' = A))"
1.781    proof safe
1.782 -    fix n show "open (to_cube (from_nat n))"
1.783 -      by (cases "from_nat n::rat list \<times> rat list")
1.784 -         (simp add: open_interval to_cube_def)
1.785 -  qed
1.786 -  moreover have "(\<forall>x. open x \<longrightarrow> (\<exists>B'\<subseteq>B. \<Union>B' = x))"
1.787 -  proof safe
1.788 -    fix x::"'a set" assume "open x"
1.789 -    def lists \<equiv> "{(a, b) |a b. to_cube (a, b) \<subseteq> x}"
1.790 -    from open_UNION[OF `open x`]
1.791 -    have "\<Union>(to_cube ` lists) = x" unfolding lists_def to_cube_def
1.792 -     by simp
1.793 -    moreover have "to_cube ` lists \<subseteq> B"
1.794 -    proof
1.795 -      fix x assume "x \<in> to_cube ` lists"
1.796 -      then obtain l where "l \<in> lists" "x = to_cube l" by auto
1.797 -      thus "x \<in> B" by (auto simp add: B_def intro!: image_eqI[where x="to_nat l"])
1.798 -    qed
1.799 -    ultimately
1.800 -    show "\<exists>B'\<subseteq>B. \<Union>B' = x" by blast
1.801 +    fix A::"'a set" assume "open A"
1.802 +    show "\<exists>B'\<subseteq>B. \<Union>B' = A"
1.803 +      apply (rule exI[of _ "{b\<in>B. b \<subseteq> A}"])
1.804 +      apply (subst (3) open_UNION_box[OF `open A`])
1.805 +      apply (auto simp add: a b B_def)
1.806 +      done
1.807    qed
1.808    ultimately
1.809    show "\<exists>B::'a set set. countable B \<and> topological_basis B" unfolding topological_basis_def by blast
1.810 @@ -5476,7 +5441,7 @@
1.811  text {* Intervals in general, including infinite and mixtures of open and closed. *}
1.812
1.813  definition "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow>
1.814 -  (\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i<DIM('a). ((a\$\$i \<le> x\$\$i \<and> x\$\$i \<le> b\$\$i) \<or> (b\$\$i \<le> x\$\$i \<and> x\$\$i \<le> a\$\$i))) \<longrightarrow> x \<in> s)"
1.815 +  (\<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.816
1.817  lemma is_interval_interval: "is_interval {a .. b::'a::ordered_euclidean_space}" (is ?th1)
1.818    "is_interval {a<..<b}" (is ?th2) proof -
1.819 @@ -5560,9 +5525,6 @@
1.820  lemma continuous_at_inner: "continuous (at x) (inner a)"
1.821    unfolding continuous_at by (intro tendsto_intros)
1.822
1.823 -lemma continuous_at_euclidean_component[intro!, simp]: "continuous (at x) (\<lambda>x. x \$\$ i)"
1.824 -  unfolding euclidean_component_def by (rule continuous_at_inner)
1.825 -
1.826  lemma closed_halfspace_le: "closed {x. inner a x \<le> b}"
1.828
1.829 @@ -5573,11 +5535,11 @@
1.831
1.832  lemma closed_halfspace_component_le:
1.833 -  shows "closed {x::'a::euclidean_space. x\$\$i \<le> a}"
1.834 +  shows "closed {x::'a::euclidean_space. x\<bullet>i \<le> a}"
1.836
1.837  lemma closed_halfspace_component_ge:
1.838 -  shows "closed {x::'a::euclidean_space. x\$\$i \<ge> a}"
1.839 +  shows "closed {x::'a::euclidean_space. x\<bullet>i \<ge> a}"
1.841
1.842  text {* Openness of halfspaces. *}
1.843 @@ -5589,33 +5551,33 @@
1.845
1.846  lemma open_halfspace_component_lt:
1.847 -  shows "open {x::'a::euclidean_space. x\$\$i < a}"
1.848 +  shows "open {x::'a::euclidean_space. x\<bullet>i < a}"
1.850
1.851  lemma open_halfspace_component_gt:
1.852 -  shows "open {x::'a::euclidean_space. x\$\$i > a}"
1.853 +  shows "open {x::'a::euclidean_space. x\<bullet>i > a}"
1.855
1.856  text{* Instantiation for intervals on @{text ordered_euclidean_space} *}
1.857
1.858  lemma eucl_lessThan_eq_halfspaces:
1.859    fixes a :: "'a\<Colon>ordered_euclidean_space"
1.860 -  shows "{..<a} = (\<Inter>i<DIM('a). {x. x \$\$ i < a \$\$ i})"
1.861 +  shows "{..<a} = (\<Inter>i\<in>Basis. {x. x \<bullet> i < a \<bullet> i})"
1.862   by (auto simp: eucl_less[where 'a='a])
1.863
1.864  lemma eucl_greaterThan_eq_halfspaces:
1.865    fixes a :: "'a\<Colon>ordered_euclidean_space"
1.866 -  shows "{a<..} = (\<Inter>i<DIM('a). {x. a \$\$ i < x \$\$ i})"
1.867 +  shows "{a<..} = (\<Inter>i\<in>Basis. {x. a \<bullet> i < x \<bullet> i})"
1.868   by (auto simp: eucl_less[where 'a='a])
1.869
1.870  lemma eucl_atMost_eq_halfspaces:
1.871    fixes a :: "'a\<Colon>ordered_euclidean_space"
1.872 -  shows "{.. a} = (\<Inter>i<DIM('a). {x. x \$\$ i \<le> a \$\$ i})"
1.873 +  shows "{.. a} = (\<Inter>i\<in>Basis. {x. x \<bullet> i \<le> a \<bullet> i})"
1.874   by (auto simp: eucl_le[where 'a='a])
1.875
1.876  lemma eucl_atLeast_eq_halfspaces:
1.877    fixes a :: "'a\<Colon>ordered_euclidean_space"
1.878 -  shows "{a ..} = (\<Inter>i<DIM('a). {x. a \$\$ i \<le> x \$\$ i})"
1.879 +  shows "{a ..} = (\<Inter>i\<in>Basis. {x. a \<bullet> i \<le> x \<bullet> i})"
1.880   by (auto simp: eucl_le[where 'a='a])
1.881
1.882  lemma open_eucl_lessThan[simp, intro]:
1.883 @@ -5640,35 +5602,24 @@
1.884    unfolding eucl_atLeast_eq_halfspaces
1.885    by (simp add: closed_INT closed_Collect_le)
1.886
1.887 -lemma open_vimage_euclidean_component: "open S \<Longrightarrow> open ((\<lambda>x. x \$\$ i) -` S)"
1.888 -  by (auto intro!: continuous_open_vimage)
1.889 -
1.890  text {* This gives a simple derivation of limit component bounds. *}
1.891
1.892  lemma Lim_component_le: fixes f :: "'a \<Rightarrow> 'b::euclidean_space"
1.893 -  assumes "(f ---> l) net" "\<not> (trivial_limit net)"  "eventually (\<lambda>x. f(x)\$\$i \<le> b) net"
1.894 -  shows "l\$\$i \<le> b"
1.895 -proof-
1.896 -  { fix x have "x \<in> {x::'b. inner (basis i) x \<le> b} \<longleftrightarrow> x\$\$i \<le> b"
1.897 -      unfolding euclidean_component_def by auto  } note * = this
1.898 -  show ?thesis using Lim_in_closed_set[of "{x. inner (basis i) x \<le> b}" f net l] unfolding *
1.899 -    using closed_halfspace_le[of "(basis i)::'b" b] and assms(1,2,3) by auto
1.900 -qed
1.901 +  assumes "(f ---> l) net" "\<not> (trivial_limit net)"  "eventually (\<lambda>x. f(x)\<bullet>i \<le> b) net"
1.902 +  shows "l\<bullet>i \<le> b"
1.903 +  by (rule tendsto_le[OF assms(2) tendsto_const tendsto_inner[OF assms(1) tendsto_const] assms(3)])
1.904
1.905  lemma Lim_component_ge: fixes f :: "'a \<Rightarrow> 'b::euclidean_space"
1.906 -  assumes "(f ---> l) net"  "\<not> (trivial_limit net)"  "eventually (\<lambda>x. b \<le> (f x)\$\$i) net"
1.907 -  shows "b \<le> l\$\$i"
1.908 -proof-
1.909 -  { fix x have "x \<in> {x::'b. inner (basis i) x \<ge> b} \<longleftrightarrow> x\$\$i \<ge> b"
1.910 -      unfolding euclidean_component_def by auto  } note * = this
1.911 -  show ?thesis using Lim_in_closed_set[of "{x. inner (basis i) x \<ge> b}" f net l] unfolding *
1.912 -    using closed_halfspace_ge[of b "(basis i)"] and assms(1,2,3) by auto
1.913 -qed
1.914 +  assumes "(f ---> l) net"  "\<not> (trivial_limit net)"  "eventually (\<lambda>x. b \<le> (f x)\<bullet>i) net"
1.915 +  shows "b \<le> l\<bullet>i"
1.916 +  by (rule tendsto_le[OF assms(2) tendsto_inner[OF assms(1) tendsto_const] tendsto_const assms(3)])
1.917
1.918  lemma Lim_component_eq: fixes f :: "'a \<Rightarrow> 'b::euclidean_space"
1.919 -  assumes net:"(f ---> l) net" "~(trivial_limit net)" and ev:"eventually (\<lambda>x. f(x)\$\$i = b) net"
1.920 -  shows "l\$\$i = b"
1.921 -  using ev[unfolded order_eq_iff eventually_conj_iff] using Lim_component_ge[OF net, of b i] and Lim_component_le[OF net, of i b] by auto
1.922 +  assumes net:"(f ---> l) net" "~(trivial_limit net)" and ev:"eventually (\<lambda>x. f(x)\<bullet>i = b) net"
1.923 +  shows "l\<bullet>i = b"
1.924 +  using ev[unfolded order_eq_iff eventually_conj_iff]
1.925 +  using Lim_component_ge[OF net, of b i] and Lim_component_le[OF net, of i b] by auto
1.926 +
1.927  text{* Limits relative to a union.                                               *}
1.928
1.929  lemma eventually_within_Un:
1.930 @@ -5726,9 +5677,8 @@
1.931  qed
1.932
1.933  lemma connected_ivt_component: fixes x::"'a::euclidean_space" shows
1.934 - "connected s \<Longrightarrow> x \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow> x\$\$k \<le> a \<Longrightarrow> a \<le> y\$\$k \<Longrightarrow> (\<exists>z\<in>s.  z\$\$k = a)"
1.935 -  using connected_ivt_hyperplane[of s x y "(basis k)::'a" a]
1.936 -  unfolding euclidean_component_def by auto
1.937 + "connected s \<Longrightarrow> x \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow> x\<bullet>k \<le> a \<Longrightarrow> a \<le> y\<bullet>k \<Longrightarrow> (\<exists>z\<in>s.  z\<bullet>k = a)"
1.938 +  using connected_ivt_hyperplane[of s x y "k::'a" a] by (auto simp: inner_commute)
1.939
1.940
1.941  subsection {* Homeomorphisms *}
1.942 @@ -5998,95 +5948,91 @@
1.943  subsection {* Some properties of a canonical subspace *}
1.944
1.945  lemma subspace_substandard:
1.946 -  "subspace {x::'a::euclidean_space. (\<forall>i<DIM('a). P i \<longrightarrow> x\$\$i = 0)}"
1.947 -  unfolding subspace_def by auto
1.948 +  "subspace {x::'a::euclidean_space. (\<forall>i\<in>Basis. P i \<longrightarrow> x\<bullet>i = 0)}"
1.949 +  unfolding subspace_def by (auto simp: inner_add_left)
1.950
1.951  lemma closed_substandard:
1.952 - "closed {x::'a::euclidean_space. \<forall>i<DIM('a). P i --> x\$\$i = 0}" (is "closed ?A")
1.953 + "closed {x::'a::euclidean_space. \<forall>i\<in>Basis. P i --> x\<bullet>i = 0}" (is "closed ?A")
1.954  proof-
1.955 -  let ?D = "{i. P i} \<inter> {..<DIM('a)}"
1.956 -  have "closed (\<Inter>i\<in>?D. {x::'a. x\$\$i = 0})"
1.957 +  let ?D = "{i\<in>Basis. P i}"
1.958 +  have "closed (\<Inter>i\<in>?D. {x::'a. x\<bullet>i = 0})"
1.959      by (simp add: closed_INT closed_Collect_eq)
1.960 -  also have "(\<Inter>i\<in>?D. {x::'a. x\$\$i = 0}) = ?A"
1.961 +  also have "(\<Inter>i\<in>?D. {x::'a. x\<bullet>i = 0}) = ?A"
1.962      by auto
1.963    finally show "closed ?A" .
1.964  qed
1.965
1.966 -lemma dim_substandard: assumes "d\<subseteq>{..<DIM('a::euclidean_space)}"
1.967 -  shows "dim {x::'a::euclidean_space. \<forall>i<DIM('a). i \<notin> d \<longrightarrow> x\$\$i = 0} = card d" (is "dim ?A = _")
1.968 +lemma dim_substandard: assumes d: "d \<subseteq> Basis"
1.969 +  shows "dim {x::'a::euclidean_space. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0} = card d" (is "dim ?A = _")
1.970  proof-
1.971 -  let ?D = "{..<DIM('a)}"
1.972 -  let ?B = "(basis::nat => 'a) ` d"
1.973 -  let ?bas = "basis::nat \<Rightarrow> 'a"
1.974 -  have "?B \<subseteq> ?A" by auto
1.975 +  let ?D = "Basis :: 'a set"
1.976 +  have "d \<subseteq> ?A" using d by (auto simp: inner_Basis)
1.977    moreover
1.978 -  { fix x::"'a" assume "x\<in>?A"
1.979 -    hence "finite d" "x\<in>?A" using assms by(auto intro:finite_subset)
1.980 -    hence "x\<in> span ?B"
1.981 +  { fix x::"'a" assume "x \<in> ?A"
1.982 +    hence "finite d" "x \<in> ?A" using assms by(auto intro: finite_subset[OF _ finite_Basis])
1.983 +    from this d have "x \<in> span d"
1.984      proof(induct d arbitrary: x)
1.985 -      case empty hence "x=0" apply(subst euclidean_eq) by auto
1.986 +      case empty hence "x=0" apply(rule_tac euclidean_eqI) by auto
1.987        thus ?case using subspace_0[OF subspace_span[of "{}"]] by auto
1.988      next
1.989        case (insert k F)
1.990 -      hence *:"\<forall>i<DIM('a). i \<notin> insert k F \<longrightarrow> x \$\$ i = 0" by auto
1.991 +      hence *:"\<forall>i\<in>Basis. i \<notin> insert k F \<longrightarrow> x \<bullet> i = 0" by auto
1.992        have **:"F \<subseteq> insert k F" by auto
1.993 -      def y \<equiv> "x - x\$\$k *\<^sub>R basis k"
1.994 -      have y:"x = y + (x\$\$k) *\<^sub>R basis k" unfolding y_def by auto
1.995 -      { fix i assume i':"i \<notin> F"
1.996 -        hence "y \$\$ i = 0" unfolding y_def
1.997 -          using *[THEN spec[where x=i]] by auto }
1.998 -      hence "y \<in> span (basis ` F)" using insert(3) by auto
1.999 -      hence "y \<in> span (basis ` (insert k F))"
1.1000 -        using span_mono[of "?bas ` F" "?bas ` (insert k F)"]
1.1001 -        using image_mono[OF **, of basis] using assms by auto
1.1002 +      def y \<equiv> "x - (x\<bullet>k) *\<^sub>R k"
1.1003 +      have y:"x = y + (x\<bullet>k) *\<^sub>R k" unfolding y_def by auto
1.1004 +      { fix i assume i': "i \<notin> F" "i \<in> Basis"
1.1005 +        hence "y \<bullet> i = 0" unfolding y_def
1.1006 +          using *[THEN bspec[where x=i]] insert by (auto simp: inner_simps inner_Basis) }
1.1007 +      hence "y \<in> span F" using insert by auto
1.1008 +      hence "y \<in> span (insert k F)"
1.1009 +        using span_mono[of F "insert k F"] using assms by auto
1.1010        moreover
1.1011 -      have "basis k \<in> span (?bas ` (insert k F))" by(rule span_superset, auto)
1.1012 -      hence "x\$\$k *\<^sub>R basis k \<in> span (?bas ` (insert k F))"
1.1013 +      have "k \<in> span (insert k F)" by(rule span_superset, auto)
1.1014 +      hence "(x\<bullet>k) *\<^sub>R k \<in> span (insert k F)"
1.1015          using span_mul by auto
1.1016        ultimately
1.1017 -      have "y + x\$\$k *\<^sub>R basis k \<in> span (?bas ` (insert k F))"
1.1018 +      have "y + (x\<bullet>k) *\<^sub>R k \<in> span (insert k F)"
1.1020        thus ?case using y by auto
1.1021      qed
1.1022    }
1.1023 -  hence "?A \<subseteq> span ?B" by auto
1.1024 +  hence "?A \<subseteq> span d" by auto
1.1025    moreover
1.1026 -  { fix x assume "x \<in> ?B"
1.1027 -    hence "x\<in>{(basis i)::'a |i. i \<in> ?D}" using assms by auto  }
1.1028 -  hence "independent ?B" using independent_mono[OF independent_basis, of ?B] and assms by auto
1.1029 +  { fix x assume "x \<in> d" hence "x \<in> ?D" using assms by auto  }
1.1030 +  hence "independent d" using independent_mono[OF independent_Basis, of d] and assms by auto
1.1031    moreover
1.1032    have "d \<subseteq> ?D" unfolding subset_eq using assms by auto
1.1033 -  hence *:"inj_on (basis::nat\<Rightarrow>'a) d" using subset_inj_on[OF basis_inj, of "d"] by auto
1.1034 -  have "card ?B = card d" unfolding card_image[OF *] by auto
1.1035 -  ultimately show ?thesis using dim_unique[of "basis ` d" ?A] by auto
1.1036 +  ultimately show ?thesis using dim_unique[of d ?A] by auto
1.1037  qed
1.1038
1.1039  text{* Hence closure and completeness of all subspaces.                          *}
1.1040
1.1041 -lemma closed_subspace_lemma: "n \<le> card (UNIV::'n::finite set) \<Longrightarrow> \<exists>A::'n set. card A = n"
1.1042 -apply (induct n)
1.1043 -apply (rule_tac x="{}" in exI, simp)
1.1044 -apply clarsimp
1.1045 -apply (subgoal_tac "\<exists>x. x \<notin> A")
1.1046 -apply (erule exE)
1.1047 -apply (rule_tac x="insert x A" in exI, simp)
1.1048 -apply (subgoal_tac "A \<noteq> UNIV", auto)
1.1049 -done
1.1050 +lemma ex_card: assumes "n \<le> card A" shows "\<exists>S\<subseteq>A. card S = n"
1.1051 +proof cases
1.1052 +  assume "finite A"
1.1053 +  from ex_bij_betw_nat_finite[OF this] guess f ..
1.1054 +  moreover with `n \<le> card A` have "{..< n} \<subseteq> {..< card A}" "inj_on f {..< n}"
1.1055 +    by (auto simp: bij_betw_def intro: subset_inj_on)
1.1056 +  ultimately have "f ` {..< n} \<subseteq> A" "card (f ` {..< n}) = n"
1.1057 +    by (auto simp: bij_betw_def card_image)
1.1058 +  then show ?thesis by blast
1.1059 +next
1.1060 +  assume "\<not> finite A" with `n \<le> card A` show ?thesis by force
1.1061 +qed
1.1062
1.1063  lemma closed_subspace: fixes s::"('a::euclidean_space) set"
1.1064    assumes "subspace s" shows "closed s"
1.1065  proof-
1.1066 -  have *:"dim s \<le> DIM('a)" using dim_subset_UNIV by auto
1.1067 -  def d \<equiv> "{..<dim s}" have t:"card d = dim s" unfolding d_def by auto
1.1068 -  let ?t = "{x::'a. \<forall>i<DIM('a). i \<notin> d \<longrightarrow> x\$\$i = 0}"
1.1069 -  have "\<exists>f. linear f \<and> f ` {x::'a. \<forall>i<DIM('a). i \<notin> d \<longrightarrow> x \$\$ i = 0} = s \<and>
1.1070 -      inj_on f {x::'a. \<forall>i<DIM('a). i \<notin> d \<longrightarrow> x \$\$ i = 0}"
1.1071 -    apply(rule subspace_isomorphism[OF subspace_substandard[of "\<lambda>i. i \<notin> d"]])
1.1072 -    using dim_substandard[of d,where 'a='a] and t unfolding d_def using * assms by auto
1.1073 -  then guess f apply-by(erule exE conjE)+ note f = this
1.1074 +  have "dim s \<le> card (Basis :: 'a set)" using dim_subset_UNIV by auto
1.1075 +  with ex_card[OF this] obtain d :: "'a set" where t: "card d = dim s" and d: "d \<subseteq> Basis" by auto
1.1076 +  let ?t = "{x::'a. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0}"
1.1077 +  have "\<exists>f. linear f \<and> f ` {x::'a. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0} = s \<and>
1.1078 +      inj_on f {x::'a. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0}"
1.1079 +    using dim_substandard[of d] t d assms
1.1080 +    by (intro subspace_isomorphism[OF subspace_substandard[of "\<lambda>i. i \<notin> d"]]) (auto simp: inner_Basis)
1.1081 +  then guess f by (elim exE conjE) note f = this
1.1082    interpret f: bounded_linear f using f unfolding linear_conv_bounded_linear by auto
1.1083 -  have "\<forall>x\<in>?t. f x = 0 \<longrightarrow> x = 0" using f.zero using f(3)[unfolded inj_on_def]
1.1084 -    by(erule_tac x=0 in ballE) auto
1.1085 +  { fix x have "x\<in>?t \<Longrightarrow> f x = 0 \<Longrightarrow> x = 0" using f.zero d f(3)[THEN inj_onD, of x 0] by auto }
1.1086    moreover have "closed ?t" using closed_substandard .
1.1087    moreover have "subspace ?t" using subspace_substandard .
1.1088    ultimately show ?thesis using closed_injective_image_subspace[of ?t f]
1.1089 @@ -6144,7 +6090,7 @@
1.1090  proof(cases "m=0")
1.1091    { fix x assume "x \<le> c" "c \<le> x"
1.1092      hence "x=c" unfolding eucl_le[where 'a='a] apply-
1.1093 -      apply(subst euclidean_eq) by (auto intro: order_antisym) }
1.1094 +      apply(subst euclidean_eq_iff) by (auto intro: order_antisym) }
1.1095    moreover case True
1.1096    moreover have "c \<in> {m *\<^sub>R a + c..m *\<^sub>R b + c}" unfolding True by(auto simp add: eucl_le[where 'a='a])
1.1097    ultimately show ?thesis by auto
1.1098 @@ -6152,23 +6098,23 @@
1.1099    case False
1.1100    { fix y assume "a \<le> y" "y \<le> b" "m > 0"
1.1101      hence "m *\<^sub>R a + c \<le> m *\<^sub>R y + c"  "m *\<^sub>R y + c \<le> m *\<^sub>R b + c"
1.1102 -      unfolding eucl_le[where 'a='a] by auto
1.1103 +      unfolding eucl_le[where 'a='a] by (auto simp: inner_simps)
1.1104    } moreover
1.1105    { fix y assume "a \<le> y" "y \<le> b" "m < 0"
1.1106      hence "m *\<^sub>R b + c \<le> m *\<^sub>R y + c"  "m *\<^sub>R y + c \<le> m *\<^sub>R a + c"
1.1107 -      unfolding eucl_le[where 'a='a] by(auto simp add: mult_left_mono_neg)
1.1108 +      unfolding eucl_le[where 'a='a] by(auto simp add: mult_left_mono_neg inner_simps)
1.1109    } moreover
1.1110    { fix y assume "m > 0"  "m *\<^sub>R a + c \<le> y"  "y \<le> m *\<^sub>R b + c"
1.1111      hence "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}"
1.1112        unfolding image_iff Bex_def mem_interval eucl_le[where 'a='a]
1.1113        apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
1.1114 -      by(auto simp add: pos_le_divide_eq pos_divide_le_eq mult_commute diff_le_iff)
1.1115 +      by(auto simp add: pos_le_divide_eq pos_divide_le_eq mult_commute diff_le_iff inner_simps)
1.1116    } moreover
1.1117    { fix y assume "m *\<^sub>R b + c \<le> y" "y \<le> m *\<^sub>R a + c" "m < 0"
1.1118      hence "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}"
1.1119        unfolding image_iff Bex_def mem_interval eucl_le[where 'a='a]
1.1120        apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
1.1121 -      by(auto simp add: neg_le_divide_eq neg_divide_le_eq mult_commute diff_le_iff)
1.1122 +      by(auto simp add: neg_le_divide_eq neg_divide_le_eq mult_commute diff_le_iff inner_simps)
1.1123    }
1.1124    ultimately show ?thesis using False by auto
1.1125  qed
```