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.88          by (simp add: power_divide)
    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.307 -  continuous_add continuous_minus continuous_diff
   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.330    continuous_on_add continuous_on_minus continuous_on_diff
   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.336    uniformly_continuous_on_compose uniformly_continuous_on_add
   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.827    by (simp add: closed_Collect_le)
   1.828  
   1.829 @@ -5573,11 +5535,11 @@
   1.830    by (simp add: closed_Collect_eq)
   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.835    by (simp add: closed_Collect_le)
   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.840    by (simp add: closed_Collect_le)
   1.841  
   1.842  text {* Openness of halfspaces. *}
   1.843 @@ -5589,33 +5551,33 @@
   1.844    by (simp add: open_Collect_less)
   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.849    by (simp add: open_Collect_less)
   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.854    by (simp add: open_Collect_less)
   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.1019          using span_add by auto
  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