# HG changeset patch
# User huffman
# Date 1272392270 25200
# Node ID 027879c5637d7b10217f4340d2fa1703b0eac9fb
# Parent  e62e32e163a49d7304ebb7a29c12082d9d6a9778# Parent  cc8db72952495bcc97ef2f460d1b7fb018bd0009
merged

diff -r cc8db7295249 -r 027879c5637d src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Tue Apr 27 16:24:57 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Tue Apr 27 11:17:50 2010 -0700
@@ -1430,550 +1430,4 @@
   unfolding interval_bij_def split_conv Cart_eq Cart_lambda_beta
   apply(rule,insert assms,erule_tac x=i in allE) by auto
 
-subsection {*Fashoda meet theorem. *}
-
-lemma infnorm_2: "infnorm (x::real^2) = max (abs(x$1)) (abs(x$2))"
-  unfolding infnorm_def UNIV_2 apply(rule Sup_eq) by auto
-
-lemma infnorm_eq_1_2: "infnorm (x::real^2) = 1 \<longleftrightarrow>
-        (abs(x$1) \<le> 1 \<and> abs(x$2) \<le> 1 \<and> (x$1 = -1 \<or> x$1 = 1 \<or> x$2 = -1 \<or> x$2 = 1))"
-  unfolding infnorm_2 by auto
-
-lemma infnorm_eq_1_imp: assumes "infnorm (x::real^2) = 1" shows "abs(x$1) \<le> 1" "abs(x$2) \<le> 1"
-  using assms unfolding infnorm_eq_1_2 by auto
-
-lemma fashoda_unit: fixes f g::"real \<Rightarrow> real^2"
-  assumes "f ` {- 1..1} \<subseteq> {- 1..1}" "g ` {- 1..1} \<subseteq> {- 1..1}"
-  "continuous_on {- 1..1} f"  "continuous_on {- 1..1} g"
-  "f (- 1)$1 = - 1" "f 1$1 = 1" "g (- 1) $2 = -1" "g 1 $2 = 1"
-  shows "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. f s = g t" proof(rule ccontr)
-  case goal1 note as = this[unfolded bex_simps,rule_format]
-  def sqprojection \<equiv> "\<lambda>z::real^2. (inverse (infnorm z)) *\<^sub>R z" 
-  def negatex \<equiv> "\<lambda>x::real^2. (vector [-(x$1), x$2])::real^2" 
-  have lem1:"\<forall>z::real^2. infnorm(negatex z) = infnorm z"
-    unfolding negatex_def infnorm_2 vector_2 by auto
-  have lem2:"\<forall>z. z\<noteq>0 \<longrightarrow> infnorm(sqprojection z) = 1" unfolding sqprojection_def
-    unfolding infnorm_mul[unfolded smult_conv_scaleR] unfolding abs_inverse real_abs_infnorm
-    unfolding infnorm_eq_0[THEN sym] by auto
-  let ?F = "(\<lambda>w::real^2. (f \<circ> (\<lambda>x. x$1)) w - (g \<circ> (\<lambda>x. x$2)) w)"
-  have *:"\<And>i. (\<lambda>x::real^2. x $ i) ` {- 1..1} = {- 1..1::real}"
-    apply(rule set_ext) unfolding image_iff Bex_def mem_interval apply rule defer 
-    apply(rule_tac x="vec x" in exI) by auto
-  { fix x assume "x \<in> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w) ` {- 1..1::real^2}"
-    then guess w unfolding image_iff .. note w = this
-    hence "x \<noteq> 0" using as[of "w$1" "w$2"] unfolding mem_interval by auto} note x0=this
-  have 21:"\<And>i::2. i\<noteq>1 \<Longrightarrow> i=2" using UNIV_2 by auto
-  have 1:"{- 1<..<1::real^2} \<noteq> {}" unfolding interval_eq_empty by auto
-  have 2:"continuous_on {- 1..1} (negatex \<circ> sqprojection \<circ> ?F)" apply(rule continuous_on_intros continuous_on_component continuous_on_vec1)+
-    prefer 2 apply(rule continuous_on_intros continuous_on_component continuous_on_vec1)+ unfolding *
-    apply(rule assms)+ apply(rule continuous_on_compose,subst sqprojection_def)
-    apply(rule continuous_on_mul ) apply(rule continuous_at_imp_continuous_on,rule) apply(rule continuous_at_inv[unfolded o_def])
-    apply(rule continuous_at_infnorm) unfolding infnorm_eq_0 defer apply(rule continuous_on_id) apply(rule linear_continuous_on) proof-
-    show "bounded_linear negatex" apply(rule bounded_linearI') unfolding Cart_eq proof(rule_tac[!] allI) fix i::2 and x y::"real^2" and c::real
-      show "negatex (x + y) $ i = (negatex x + negatex y) $ i" "negatex (c *s x) $ i = (c *s negatex x) $ i"
-	apply-apply(case_tac[!] "i\<noteq>1") prefer 3 apply(drule_tac[1-2] 21) 
-	unfolding negatex_def by(auto simp add:vector_2 ) qed qed(insert x0, auto)
-  have 3:"(negatex \<circ> sqprojection \<circ> ?F) ` {- 1..1} \<subseteq> {- 1..1}" unfolding subset_eq apply rule proof-
-    case goal1 then guess y unfolding image_iff .. note y=this have "?F y \<noteq> 0" apply(rule x0) using y(1) by auto
-    hence *:"infnorm (sqprojection (?F y)) = 1" unfolding y o_def apply- by(rule lem2[rule_format])
-    have "infnorm x = 1" unfolding *[THEN sym] y o_def by(rule lem1[rule_format])
-    thus "x\<in>{- 1..1}" unfolding mem_interval infnorm_2 apply- apply rule
-    proof-case goal1 thus ?case apply(cases "i=1") defer apply(drule 21) by auto qed qed
-  guess x apply(rule brouwer_weak[of "{- 1..1::real^2}" "negatex \<circ> sqprojection \<circ> ?F"])
-    apply(rule compact_interval convex_interval)+ unfolding interior_closed_interval
-    apply(rule 1 2 3)+ . note x=this
-  have "?F x \<noteq> 0" apply(rule x0) using x(1) by auto
-  hence *:"infnorm (sqprojection (?F x)) = 1" unfolding o_def by(rule lem2[rule_format])
-  have nx:"infnorm x = 1" apply(subst x(2)[THEN sym]) unfolding *[THEN sym] o_def by(rule lem1[rule_format])
-  have "\<forall>x i. x \<noteq> 0 \<longrightarrow> (0 < (sqprojection x)$i \<longleftrightarrow> 0 < x$i)"    "\<forall>x i. x \<noteq> 0 \<longrightarrow> ((sqprojection x)$i < 0 \<longleftrightarrow> x$i < 0)"
-    apply- apply(rule_tac[!] allI impI)+ proof- fix x::"real^2" and i::2 assume x:"x\<noteq>0"
-    have "inverse (infnorm x) > 0" using x[unfolded infnorm_pos_lt[THEN sym]] by auto
-    thus "(0 < sqprojection x $ i) = (0 < x $ i)"   "(sqprojection x $ i < 0) = (x $ i < 0)"
-      unfolding sqprojection_def vector_component_simps Cart_nth.scaleR real_scaleR_def
-      unfolding zero_less_mult_iff mult_less_0_iff by(auto simp add:field_simps) qed
-  note lem3 = this[rule_format]
-  have x1:"x $ 1 \<in> {- 1..1::real}" "x $ 2 \<in> {- 1..1::real}" using x(1) unfolding mem_interval by auto
-  hence nz:"f (x $ 1) - g (x $ 2) \<noteq> 0" unfolding right_minus_eq apply-apply(rule as) by auto
-  have "x $ 1 = -1 \<or> x $ 1 = 1 \<or> x $ 2 = -1 \<or> x $ 2 = 1" using nx unfolding infnorm_eq_1_2 by auto 
-  thus False proof- fix P Q R S 
-    presume "P \<or> Q \<or> R \<or> S" "P\<Longrightarrow>False" "Q\<Longrightarrow>False" "R\<Longrightarrow>False" "S\<Longrightarrow>False" thus False by auto
-  next assume as:"x$1 = 1"
-    hence *:"f (x $ 1) $ 1 = 1" using assms(6) by auto
-    have "sqprojection (f (x$1) - g (x$2)) $ 1 < 0"
-      using x(2)[unfolded o_def Cart_eq,THEN spec[where x=1]]
-      unfolding as negatex_def vector_2 by auto moreover
-    from x1 have "g (x $ 2) \<in> {- 1..1}" apply-apply(rule assms(2)[unfolded subset_eq,rule_format]) by auto
-    ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval 
-      apply(erule_tac x=1 in allE) by auto 
-  next assume as:"x$1 = -1"
-    hence *:"f (x $ 1) $ 1 = - 1" using assms(5) by auto
-    have "sqprojection (f (x$1) - g (x$2)) $ 1 > 0"
-      using x(2)[unfolded o_def Cart_eq,THEN spec[where x=1]]
-      unfolding as negatex_def vector_2 by auto moreover
-    from x1 have "g (x $ 2) \<in> {- 1..1}" apply-apply(rule assms(2)[unfolded subset_eq,rule_format]) by auto
-    ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval 
-      apply(erule_tac x=1 in allE) by auto
-  next assume as:"x$2 = 1"
-    hence *:"g (x $ 2) $ 2 = 1" using assms(8) by auto
-    have "sqprojection (f (x$1) - g (x$2)) $ 2 > 0"
-      using x(2)[unfolded o_def Cart_eq,THEN spec[where x=2]]
-      unfolding as negatex_def vector_2 by auto moreover
-    from x1 have "f (x $ 1) \<in> {- 1..1}" apply-apply(rule assms(1)[unfolded subset_eq,rule_format]) by auto
-    ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval 
-     apply(erule_tac x=2 in allE) by auto
- next assume as:"x$2 = -1"
-    hence *:"g (x $ 2) $ 2 = - 1" using assms(7) by auto
-    have "sqprojection (f (x$1) - g (x$2)) $ 2 < 0"
-      using x(2)[unfolded o_def Cart_eq,THEN spec[where x=2]]
-      unfolding as negatex_def vector_2 by auto moreover
-    from x1 have "f (x $ 1) \<in> {- 1..1}" apply-apply(rule assms(1)[unfolded subset_eq,rule_format]) by auto
-    ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval 
-      apply(erule_tac x=2 in allE) by auto qed(auto) qed
-
-lemma fashoda_unit_path: fixes f ::"real \<Rightarrow> real^2" and g ::"real \<Rightarrow> real^2"
-  assumes "path f" "path g" "path_image f \<subseteq> {- 1..1}" "path_image g \<subseteq> {- 1..1}"
-  "(pathstart f)$1 = -1" "(pathfinish f)$1 = 1"  "(pathstart g)$2 = -1" "(pathfinish g)$2 = 1"
-  obtains z where "z \<in> path_image f" "z \<in> path_image g" proof-
-  note assms=assms[unfolded path_def pathstart_def pathfinish_def path_image_def]
-  def iscale \<equiv> "\<lambda>z::real. inverse 2 *\<^sub>R (z + 1)"
-  have isc:"iscale ` {- 1..1} \<subseteq> {0..1}" unfolding iscale_def by(auto)
-  have "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. (f \<circ> iscale) s = (g \<circ> iscale) t" proof(rule fashoda_unit) 
-    show "(f \<circ> iscale) ` {- 1..1} \<subseteq> {- 1..1}" "(g \<circ> iscale) ` {- 1..1} \<subseteq> {- 1..1}"
-      using isc and assms(3-4) unfolding image_compose by auto
-    have *:"continuous_on {- 1..1} iscale" unfolding iscale_def by(rule continuous_on_intros)+
-    show "continuous_on {- 1..1} (f \<circ> iscale)" "continuous_on {- 1..1} (g \<circ> iscale)"
-      apply-apply(rule_tac[!] continuous_on_compose[OF *]) apply(rule_tac[!] continuous_on_subset[OF _ isc])
-      by(rule assms)+ have *:"(1 / 2) *\<^sub>R (1 + (1::real^1)) = 1" unfolding Cart_eq by auto
-    show "(f \<circ> iscale) (- 1) $ 1 = - 1" "(f \<circ> iscale) 1 $ 1 = 1" "(g \<circ> iscale) (- 1) $ 2 = -1" "(g \<circ> iscale) 1 $ 2 = 1"
-      unfolding o_def iscale_def using assms by(auto simp add:*) qed
-  then guess s .. from this(2) guess t .. note st=this
-  show thesis apply(rule_tac z="f (iscale s)" in that)
-    using st `s\<in>{- 1..1}` unfolding o_def path_image_def image_iff apply-
-    apply(rule_tac x="iscale s" in bexI) prefer 3 apply(rule_tac x="iscale t" in bexI)
-    using isc[unfolded subset_eq, rule_format] by auto qed
-
-lemma fashoda: fixes b::"real^2"
-  assumes "path f" "path g" "path_image f \<subseteq> {a..b}" "path_image g \<subseteq> {a..b}"
-  "(pathstart f)$1 = a$1" "(pathfinish f)$1 = b$1"
-  "(pathstart g)$2 = a$2" "(pathfinish g)$2 = b$2"
-  obtains z where "z \<in> path_image f" "z \<in> path_image g" proof-
-  fix P Q S presume "P \<or> Q \<or> S" "P \<Longrightarrow> thesis" "Q \<Longrightarrow> thesis" "S \<Longrightarrow> thesis" thus thesis by auto
-next have "{a..b} \<noteq> {}" using assms(3) using path_image_nonempty by auto
-  hence "a \<le> b" unfolding interval_eq_empty vector_le_def by(auto simp add: not_less)
-  thus "a$1 = b$1 \<or> a$2 = b$2 \<or> (a$1 < b$1 \<and> a$2 < b$2)" unfolding vector_le_def forall_2 by auto
-next assume as:"a$1 = b$1" have "\<exists>z\<in>path_image g. z$2 = (pathstart f)$2" apply(rule connected_ivt_component)
-    apply(rule connected_path_image assms)+apply(rule pathstart_in_path_image,rule pathfinish_in_path_image)
-    unfolding assms using assms(3)[unfolded path_image_def subset_eq,rule_format,of "f 0"]
-    unfolding pathstart_def by(auto simp add: vector_le_def) then guess z .. note z=this
-  have "z \<in> {a..b}" using z(1) assms(4) unfolding path_image_def by blast 
-  hence "z = f 0" unfolding Cart_eq forall_2 unfolding z(2) pathstart_def
-    using assms(3)[unfolded path_image_def subset_eq mem_interval,rule_format,of "f 0" 1]
-    unfolding mem_interval apply(erule_tac x=1 in allE) using as by auto
-  thus thesis apply-apply(rule that[OF _ z(1)]) unfolding path_image_def by auto
-next assume as:"a$2 = b$2" have "\<exists>z\<in>path_image f. z$1 = (pathstart g)$1" apply(rule connected_ivt_component)
-    apply(rule connected_path_image assms)+apply(rule pathstart_in_path_image,rule pathfinish_in_path_image)
-    unfolding assms using assms(4)[unfolded path_image_def subset_eq,rule_format,of "g 0"]
-    unfolding pathstart_def by(auto simp add: vector_le_def) then guess z .. note z=this
-  have "z \<in> {a..b}" using z(1) assms(3) unfolding path_image_def by blast 
-  hence "z = g 0" unfolding Cart_eq forall_2 unfolding z(2) pathstart_def
-    using assms(4)[unfolded path_image_def subset_eq mem_interval,rule_format,of "g 0" 2]
-    unfolding mem_interval apply(erule_tac x=2 in allE) using as by auto
-  thus thesis apply-apply(rule that[OF z(1)]) unfolding path_image_def by auto
-next assume as:"a $ 1 < b $ 1 \<and> a $ 2 < b $ 2"
-  have int_nem:"{- 1..1::real^2} \<noteq> {}" unfolding interval_eq_empty by auto
-  guess z apply(rule fashoda_unit_path[of "interval_bij (a,b) (- 1,1) \<circ> f" "interval_bij (a,b) (- 1,1) \<circ> g"]) 
-    unfolding path_def path_image_def pathstart_def pathfinish_def
-    apply(rule_tac[1-2] continuous_on_compose) apply(rule assms[unfolded path_def] continuous_on_interval_bij)+
-    unfolding subset_eq apply(rule_tac[1-2] ballI)
-  proof- fix x assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> f) ` {0..1}"
-    then guess y unfolding image_iff .. note y=this
-    show "x \<in> {- 1..1}" unfolding y o_def apply(rule in_interval_interval_bij)
-      using y(1) using assms(3)[unfolded path_image_def subset_eq] int_nem by auto
-  next fix x assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> g) ` {0..1}"
-    then guess y unfolding image_iff .. note y=this
-    show "x \<in> {- 1..1}" unfolding y o_def apply(rule in_interval_interval_bij)
-      using y(1) using assms(4)[unfolded path_image_def subset_eq] int_nem by auto
-  next show "(interval_bij (a, b) (- 1, 1) \<circ> f) 0 $ 1 = -1"
-      "(interval_bij (a, b) (- 1, 1) \<circ> f) 1 $ 1 = 1"
-      "(interval_bij (a, b) (- 1, 1) \<circ> g) 0 $ 2 = -1"
-      "(interval_bij (a, b) (- 1, 1) \<circ> g) 1 $ 2 = 1" unfolding interval_bij_def Cart_lambda_beta vector_component_simps o_def split_conv
-      unfolding assms[unfolded pathstart_def pathfinish_def] using as by auto qed note z=this
-  from z(1) guess zf unfolding image_iff .. note zf=this
-  from z(2) guess zg unfolding image_iff .. note zg=this
-  have *:"\<forall>i. (- 1) $ i < (1::real^2) $ i \<and> a $ i < b $ i" unfolding forall_2 using as by auto
-  show thesis apply(rule_tac z="interval_bij (- 1,1) (a,b) z" in that)
-    apply(subst zf) defer apply(subst zg) unfolding o_def interval_bij_bij[OF *] path_image_def
-    using zf(1) zg(1) by auto qed
-
-subsection {*Some slightly ad hoc lemmas I use below*}
-
-lemma segment_vertical: fixes a::"real^2" assumes "a$1 = b$1"
-  shows "x \<in> closed_segment a b \<longleftrightarrow> (x$1 = a$1 \<and> x$1 = b$1 \<and>
-           (a$2 \<le> x$2 \<and> x$2 \<le> b$2 \<or> b$2 \<le> x$2 \<and> x$2 \<le> a$2))" (is "_ = ?R")
-proof- 
-  let ?L = "\<exists>u. (x $ 1 = (1 - u) * a $ 1 + u * b $ 1 \<and> x $ 2 = (1 - u) * a $ 2 + u * b $ 2) \<and> 0 \<le> u \<and> u \<le> 1"
-  { presume "?L \<Longrightarrow> ?R" "?R \<Longrightarrow> ?L" thus ?thesis unfolding closed_segment_def mem_Collect_eq
-      unfolding Cart_eq forall_2 smult_conv_scaleR[THEN sym] vector_component_simps by blast }
-  { assume ?L then guess u apply-apply(erule exE)apply(erule conjE)+ . note u=this
-    { fix b a assume "b + u * a > a + u * b"
-      hence "(1 - u) * b > (1 - u) * a" by(auto simp add:field_simps)
-      hence "b \<ge> a" apply(drule_tac mult_less_imp_less_left) using u by auto
-      hence "u * a \<le> u * b" apply-apply(rule mult_left_mono[OF _ u(3)]) 
-        using u(3-4) by(auto simp add:field_simps) } note * = this
-    { fix a b assume "u * b > u * a" hence "(1 - u) * a \<le> (1 - u) * b" apply-apply(rule mult_left_mono)
-        apply(drule mult_less_imp_less_left) using u by auto
-      hence "a + u * b \<le> b + u * a" by(auto simp add:field_simps) } note ** = this
-    thus ?R unfolding u assms using u by(auto simp add:field_simps not_le intro:* **) }
-  { assume ?R thus ?L proof(cases "x$2 = b$2")
-      case True thus ?L apply(rule_tac x="(x$2 - a$2) / (b$2 - a$2)" in exI) unfolding assms True
-        using `?R` by(auto simp add:field_simps)
-    next case False thus ?L apply(rule_tac x="1 - (x$2 - b$2) / (a$2 - b$2)" in exI) unfolding assms using `?R`
-        by(auto simp add:field_simps)
-    qed } qed
-
-lemma segment_horizontal: fixes a::"real^2" assumes "a$2 = b$2"
-  shows "x \<in> closed_segment a b \<longleftrightarrow> (x$2 = a$2 \<and> x$2 = b$2 \<and>
-           (a$1 \<le> x$1 \<and> x$1 \<le> b$1 \<or> b$1 \<le> x$1 \<and> x$1 \<le> a$1))" (is "_ = ?R")
-proof- 
-  let ?L = "\<exists>u. (x $ 1 = (1 - u) * a $ 1 + u * b $ 1 \<and> x $ 2 = (1 - u) * a $ 2 + u * b $ 2) \<and> 0 \<le> u \<and> u \<le> 1"
-  { presume "?L \<Longrightarrow> ?R" "?R \<Longrightarrow> ?L" thus ?thesis unfolding closed_segment_def mem_Collect_eq
-      unfolding Cart_eq forall_2 smult_conv_scaleR[THEN sym] vector_component_simps by blast }
-  { assume ?L then guess u apply-apply(erule exE)apply(erule conjE)+ . note u=this
-    { fix b a assume "b + u * a > a + u * b"
-      hence "(1 - u) * b > (1 - u) * a" by(auto simp add:field_simps)
-      hence "b \<ge> a" apply(drule_tac mult_less_imp_less_left) using u by auto
-      hence "u * a \<le> u * b" apply-apply(rule mult_left_mono[OF _ u(3)]) 
-        using u(3-4) by(auto simp add:field_simps) } note * = this
-    { fix a b assume "u * b > u * a" hence "(1 - u) * a \<le> (1 - u) * b" apply-apply(rule mult_left_mono)
-        apply(drule mult_less_imp_less_left) using u by auto
-      hence "a + u * b \<le> b + u * a" by(auto simp add:field_simps) } note ** = this
-    thus ?R unfolding u assms using u by(auto simp add:field_simps not_le intro:* **) }
-  { assume ?R thus ?L proof(cases "x$1 = b$1")
-      case True thus ?L apply(rule_tac x="(x$1 - a$1) / (b$1 - a$1)" in exI) unfolding assms True
-        using `?R` by(auto simp add:field_simps)
-    next case False thus ?L apply(rule_tac x="1 - (x$1 - b$1) / (a$1 - b$1)" in exI) unfolding assms using `?R`
-        by(auto simp add:field_simps)
-    qed } qed
-
-subsection {*useful Fashoda corollary pointed out to me by Tom Hales. *}
-
-lemma fashoda_interlace: fixes a::"real^2"
-  assumes "path f" "path g"
-  "path_image f \<subseteq> {a..b}" "path_image g \<subseteq> {a..b}"
-  "(pathstart f)$2 = a$2" "(pathfinish f)$2 = a$2"
-  "(pathstart g)$2 = a$2" "(pathfinish g)$2 = a$2"
-  "(pathstart f)$1 < (pathstart g)$1" "(pathstart g)$1 < (pathfinish f)$1"
-  "(pathfinish f)$1 < (pathfinish g)$1"
-  obtains z where "z \<in> path_image f" "z \<in> path_image g"
-proof-
-  have "{a..b} \<noteq> {}" using path_image_nonempty using assms(3) by auto
-  note ab=this[unfolded interval_eq_empty not_ex forall_2 not_less]
-  have "pathstart f \<in> {a..b}" "pathfinish f \<in> {a..b}" "pathstart g \<in> {a..b}" "pathfinish g \<in> {a..b}"
-    using pathstart_in_path_image pathfinish_in_path_image using assms(3-4) by auto
-  note startfin = this[unfolded mem_interval forall_2]
-  let ?P1 = "linepath (vector[a$1 - 2, a$2 - 2]) (vector[(pathstart f)$1,a$2 - 2]) +++
-     linepath(vector[(pathstart f)$1,a$2 - 2])(pathstart f) +++ f +++
-     linepath(pathfinish f)(vector[(pathfinish f)$1,a$2 - 2]) +++
-     linepath(vector[(pathfinish f)$1,a$2 - 2])(vector[b$1 + 2,a$2 - 2])" 
-  let ?P2 = "linepath(vector[(pathstart g)$1, (pathstart g)$2 - 3])(pathstart g) +++ g +++
-     linepath(pathfinish g)(vector[(pathfinish g)$1,a$2 - 1]) +++
-     linepath(vector[(pathfinish g)$1,a$2 - 1])(vector[b$1 + 1,a$2 - 1]) +++
-     linepath(vector[b$1 + 1,a$2 - 1])(vector[b$1 + 1,b$2 + 3])"
-  let ?a = "vector[a$1 - 2, a$2 - 3]"
-  let ?b = "vector[b$1 + 2, b$2 + 3]"
-  have P1P2:"path_image ?P1 = path_image (linepath (vector[a$1 - 2, a$2 - 2]) (vector[(pathstart f)$1,a$2 - 2])) \<union>
-      path_image (linepath(vector[(pathstart f)$1,a$2 - 2])(pathstart f)) \<union> path_image f \<union>
-      path_image (linepath(pathfinish f)(vector[(pathfinish f)$1,a$2 - 2])) \<union>
-      path_image (linepath(vector[(pathfinish f)$1,a$2 - 2])(vector[b$1 + 2,a$2 - 2]))"
-    "path_image ?P2 = path_image(linepath(vector[(pathstart g)$1, (pathstart g)$2 - 3])(pathstart g)) \<union> path_image g \<union>
-      path_image(linepath(pathfinish g)(vector[(pathfinish g)$1,a$2 - 1])) \<union>
-      path_image(linepath(vector[(pathfinish g)$1,a$2 - 1])(vector[b$1 + 1,a$2 - 1])) \<union>
-      path_image(linepath(vector[b$1 + 1,a$2 - 1])(vector[b$1 + 1,b$2 + 3]))" using assms(1-2)
-      by(auto simp add: path_image_join path_linepath)
-  have abab: "{a..b} \<subseteq> {?a..?b}" by(auto simp add:vector_le_def forall_2 vector_2)
-  guess z apply(rule fashoda[of ?P1 ?P2 ?a ?b])
-    unfolding pathstart_join pathfinish_join pathstart_linepath pathfinish_linepath vector_2 proof-
-    show "path ?P1" "path ?P2" using assms by auto
-    have "path_image ?P1 \<subseteq> {?a .. ?b}" unfolding P1P2 path_image_linepath apply(rule Un_least)+ defer 3
-      apply(rule_tac[1-4] convex_interval(1)[unfolded convex_contains_segment,rule_format])
-      unfolding mem_interval forall_2 vector_2 using ab startfin abab assms(3)
-      using assms(9-) unfolding assms by(auto simp add:field_simps)
-    thus "path_image ?P1  \<subseteq> {?a .. ?b}" .
-    have "path_image ?P2 \<subseteq> {?a .. ?b}" unfolding P1P2 path_image_linepath apply(rule Un_least)+ defer 2
-      apply(rule_tac[1-4] convex_interval(1)[unfolded convex_contains_segment,rule_format])
-      unfolding mem_interval forall_2 vector_2 using ab startfin abab assms(4)
-      using assms(9-) unfolding assms  by(auto simp add:field_simps)
-    thus "path_image ?P2  \<subseteq> {?a .. ?b}" . 
-    show "a $ 1 - 2 = a $ 1 - 2"  "b $ 1 + 2 = b $ 1 + 2" "pathstart g $ 2 - 3 = a $ 2 - 3"  "b $ 2 + 3 = b $ 2 + 3"
-      by(auto simp add: assms)
-  qed note z=this[unfolded P1P2 path_image_linepath]
-  show thesis apply(rule that[of z]) proof-
-    have "(z \<in> closed_segment (vector [a $ 1 - 2, a $ 2 - 2]) (vector [pathstart f $ 1, a $ 2 - 2]) \<or>
-     z \<in> closed_segment (vector [pathstart f $ 1, a $ 2 - 2]) (pathstart f)) \<or>
-   z \<in> closed_segment (pathfinish f) (vector [pathfinish f $ 1, a $ 2 - 2]) \<or>
-  z \<in> closed_segment (vector [pathfinish f $ 1, a $ 2 - 2]) (vector [b $ 1 + 2, a $ 2 - 2]) \<Longrightarrow>
-  (((z \<in> closed_segment (vector [pathstart g $ 1, pathstart g $ 2 - 3]) (pathstart g)) \<or>
-    z \<in> closed_segment (pathfinish g) (vector [pathfinish g $ 1, a $ 2 - 1])) \<or>
-   z \<in> closed_segment (vector [pathfinish g $ 1, a $ 2 - 1]) (vector [b $ 1 + 1, a $ 2 - 1])) \<or>
-  z \<in> closed_segment (vector [b $ 1 + 1, a $ 2 - 1]) (vector [b $ 1 + 1, b $ 2 + 3]) \<Longrightarrow> False"
-      apply(simp only: segment_vertical segment_horizontal vector_2) proof- case goal1 note as=this
-      have "pathfinish f \<in> {a..b}" using assms(3) pathfinish_in_path_image[of f] by auto 
-      hence "1 + b $ 1 \<le> pathfinish f $ 1 \<Longrightarrow> False" unfolding mem_interval forall_2 by auto
-      hence "z$1 \<noteq> pathfinish f$1" using as(2) using assms ab by(auto simp add:field_simps)
-      moreover have "pathstart f \<in> {a..b}" using assms(3) pathstart_in_path_image[of f] by auto 
-      hence "1 + b $ 1 \<le> pathstart f $ 1 \<Longrightarrow> False" unfolding mem_interval forall_2 by auto
-      hence "z$1 \<noteq> pathstart f$1" using as(2) using assms ab by(auto simp add:field_simps)
-      ultimately have *:"z$2 = a$2 - 2" using goal1(1) by auto
-      have "z$1 \<noteq> pathfinish g$1" using as(2) using assms ab by(auto simp add:field_simps *)
-      moreover have "pathstart g \<in> {a..b}" using assms(4) pathstart_in_path_image[of g] by auto 
-      note this[unfolded mem_interval forall_2]
-      hence "z$1 \<noteq> pathstart g$1" using as(1) using assms ab by(auto simp add:field_simps *)
-      ultimately have "a $ 2 - 1 \<le> z $ 2 \<and> z $ 2 \<le> b $ 2 + 3 \<or> b $ 2 + 3 \<le> z $ 2 \<and> z $ 2 \<le> a $ 2 - 1"
-        using as(2) unfolding * assms by(auto simp add:field_simps)
-      thus False unfolding * using ab by auto
-    qed hence "z \<in> path_image f \<or> z \<in> path_image g" using z unfolding Un_iff by blast
-    hence z':"z\<in>{a..b}" using assms(3-4) by auto
-    have "a $ 2 = z $ 2 \<Longrightarrow> (z $ 1 = pathstart f $ 1 \<or> z $ 1 = pathfinish f $ 1) \<Longrightarrow> (z = pathstart f \<or> z = pathfinish f)"
-      unfolding Cart_eq forall_2 assms by auto
-    with z' show "z\<in>path_image f" using z(1) unfolding Un_iff mem_interval forall_2 apply-
-      apply(simp only: segment_vertical segment_horizontal vector_2) unfolding assms by auto
-    have "a $ 2 = z $ 2 \<Longrightarrow> (z $ 1 = pathstart g $ 1 \<or> z $ 1 = pathfinish g $ 1) \<Longrightarrow> (z = pathstart g \<or> z = pathfinish g)"
-      unfolding Cart_eq forall_2 assms by auto
-    with z' show "z\<in>path_image g" using z(2) unfolding Un_iff mem_interval forall_2 apply-
-      apply(simp only: segment_vertical segment_horizontal vector_2) unfolding assms by auto
-  qed qed
-
-(** The Following still needs to be translated. Maybe I will do that later.
-
-(* ------------------------------------------------------------------------- *)
-(* Complement in dimension N >= 2 of set homeomorphic to any interval in     *)
-(* any dimension is (path-)connected. This naively generalizes the argument  *)
-(* in Ryuji Maehara's paper "The Jordan curve theorem via the Brouwer        *)
-(* fixed point theorem", American Mathematical Monthly 1984.                 *)
-(* ------------------------------------------------------------------------- *)
-
-let RETRACTION_INJECTIVE_IMAGE_INTERVAL = prove
- (`!p:real^M->real^N a b.
-        ~(interval[a,b] = {}) /\
-        p continuous_on interval[a,b] /\
-        (!x y. x IN interval[a,b] /\ y IN interval[a,b] /\ p x = p y ==> x = y)
-        ==> ?f. f continuous_on (:real^N) /\
-                IMAGE f (:real^N) SUBSET (IMAGE p (interval[a,b])) /\
-                (!x. x IN (IMAGE p (interval[a,b])) ==> f x = x)`,
-  REPEAT STRIP_TAC THEN
-  FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [INJECTIVE_ON_LEFT_INVERSE]) THEN
-  DISCH_THEN(X_CHOOSE_TAC `q:real^N->real^M`) THEN
-  SUBGOAL_THEN `(q:real^N->real^M) continuous_on
-                (IMAGE p (interval[a:real^M,b]))`
-  ASSUME_TAC THENL
-   [MATCH_MP_TAC CONTINUOUS_ON_INVERSE THEN ASM_REWRITE_TAC[COMPACT_INTERVAL];
-    ALL_TAC] THEN
-  MP_TAC(ISPECL [`q:real^N->real^M`;
-                 `IMAGE (p:real^M->real^N)
-                 (interval[a,b])`;
-                 `a:real^M`; `b:real^M`]
-        TIETZE_CLOSED_INTERVAL) THEN
-  ASM_SIMP_TAC[COMPACT_INTERVAL; COMPACT_CONTINUOUS_IMAGE;
-               COMPACT_IMP_CLOSED] THEN
-  ANTS_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
-  DISCH_THEN(X_CHOOSE_THEN `r:real^N->real^M` STRIP_ASSUME_TAC) THEN
-  EXISTS_TAC `(p:real^M->real^N) o (r:real^N->real^M)` THEN
-  REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; o_THM; IN_UNIV] THEN
-  CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
-  MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN ASM_REWRITE_TAC[] THEN
-  FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP(REWRITE_RULE[IMP_CONJ]
-        CONTINUOUS_ON_SUBSET)) THEN ASM SET_TAC[]);;
-
-let UNBOUNDED_PATH_COMPONENTS_COMPLEMENT_HOMEOMORPHIC_INTERVAL = prove
- (`!s:real^N->bool a b:real^M.
-        s homeomorphic (interval[a,b])
-        ==> !x. ~(x IN s) ==> ~bounded(path_component((:real^N) DIFF s) x)`,
-  REPEAT GEN_TAC THEN REWRITE_TAC[homeomorphic; homeomorphism] THEN
-  REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
-  MAP_EVERY X_GEN_TAC [`p':real^N->real^M`; `p:real^M->real^N`] THEN
-  DISCH_TAC THEN
-  SUBGOAL_THEN
-   `!x y. x IN interval[a,b] /\ y IN interval[a,b] /\
-          (p:real^M->real^N) x = p y ==> x = y`
-  ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
-  FIRST_X_ASSUM(MP_TAC o funpow 4 CONJUNCT2) THEN
-  DISCH_THEN(CONJUNCTS_THEN2 (SUBST1_TAC o SYM) ASSUME_TAC) THEN
-  ASM_CASES_TAC `interval[a:real^M,b] = {}` THEN
-  ASM_REWRITE_TAC[IMAGE_CLAUSES; DIFF_EMPTY; PATH_COMPONENT_UNIV;
-                  NOT_BOUNDED_UNIV] THEN
-  ABBREV_TAC `s = (:real^N) DIFF (IMAGE p (interval[a:real^M,b]))` THEN
-  X_GEN_TAC `c:real^N` THEN REPEAT STRIP_TAC THEN
-  SUBGOAL_THEN `(c:real^N) IN s` ASSUME_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
-  SUBGOAL_THEN `bounded((path_component s c) UNION
-                        (IMAGE (p:real^M->real^N) (interval[a,b])))`
-  MP_TAC THENL
-   [ASM_SIMP_TAC[BOUNDED_UNION; COMPACT_IMP_BOUNDED; COMPACT_IMP_BOUNDED;
-                 COMPACT_CONTINUOUS_IMAGE; COMPACT_INTERVAL];
-    ALL_TAC] THEN
-  DISCH_THEN(MP_TAC o SPEC `c:real^N` o MATCH_MP BOUNDED_SUBSET_BALL) THEN
-  REWRITE_TAC[UNION_SUBSET] THEN
-  DISCH_THEN(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC) THEN
-  MP_TAC(ISPECL [`p:real^M->real^N`; `a:real^M`; `b:real^M`]
-    RETRACTION_INJECTIVE_IMAGE_INTERVAL) THEN
-  ASM_REWRITE_TAC[SUBSET; IN_UNIV] THEN
-  DISCH_THEN(X_CHOOSE_THEN `r:real^N->real^N` MP_TAC) THEN
-  DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC
-   (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC)) THEN
-  REWRITE_TAC[FORALL_IN_IMAGE; IN_UNIV] THEN DISCH_TAC THEN
-  ABBREV_TAC `q = \z:real^N. if z IN path_component s c then r(z) else z` THEN
-  SUBGOAL_THEN
-    `(q:real^N->real^N) continuous_on
-     (closure(path_component s c) UNION ((:real^N) DIFF (path_component s c)))`
-  MP_TAC THENL
-   [EXPAND_TAC "q" THEN MATCH_MP_TAC CONTINUOUS_ON_CASES THEN
-    REWRITE_TAC[CLOSED_CLOSURE; CONTINUOUS_ON_ID; GSYM OPEN_CLOSED] THEN
-    REPEAT CONJ_TAC THENL
-     [MATCH_MP_TAC OPEN_PATH_COMPONENT THEN EXPAND_TAC "s" THEN
-      ASM_SIMP_TAC[GSYM CLOSED_OPEN; COMPACT_IMP_CLOSED;
-                   COMPACT_CONTINUOUS_IMAGE; COMPACT_INTERVAL];
-      ASM_MESON_TAC[CONTINUOUS_ON_SUBSET; SUBSET_UNIV];
-      ALL_TAC] THEN
-    X_GEN_TAC `z:real^N` THEN
-    REWRITE_TAC[SET_RULE `~(z IN (s DIFF t) /\ z IN t)`] THEN
-    STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
-    MP_TAC(ISPECL
-     [`path_component s (z:real^N)`; `path_component s (c:real^N)`]
-     OPEN_INTER_CLOSURE_EQ_EMPTY) THEN
-    ASM_REWRITE_TAC[GSYM DISJOINT; PATH_COMPONENT_DISJOINT] THEN ANTS_TAC THENL
-     [MATCH_MP_TAC OPEN_PATH_COMPONENT THEN EXPAND_TAC "s" THEN
-      ASM_SIMP_TAC[GSYM CLOSED_OPEN; COMPACT_IMP_CLOSED;
-                   COMPACT_CONTINUOUS_IMAGE; COMPACT_INTERVAL];
-      REWRITE_TAC[DISJOINT; EXTENSION; IN_INTER; NOT_IN_EMPTY] THEN
-      DISCH_THEN(MP_TAC o SPEC `z:real^N`) THEN ASM_REWRITE_TAC[] THEN
-      GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [IN] THEN
-      REWRITE_TAC[PATH_COMPONENT_REFL_EQ] THEN ASM SET_TAC[]];
-    ALL_TAC] THEN
-  SUBGOAL_THEN
-   `closure(path_component s c) UNION ((:real^N) DIFF (path_component s c)) =
-    (:real^N)`
-  SUBST1_TAC THENL
-   [MATCH_MP_TAC(SET_RULE `s SUBSET t ==> t UNION (UNIV DIFF s) = UNIV`) THEN
-    REWRITE_TAC[CLOSURE_SUBSET];
-    DISCH_TAC] THEN
-  MP_TAC(ISPECL
-   [`(\x. &2 % c - x) o
-     (\x. c + B / norm(x - c) % (x - c)) o (q:real^N->real^N)`;
-    `cball(c:real^N,B)`]
-    BROUWER) THEN
-  REWRITE_TAC[NOT_IMP; GSYM CONJ_ASSOC; COMPACT_CBALL; CONVEX_CBALL] THEN
-  ASM_SIMP_TAC[CBALL_EQ_EMPTY; REAL_LT_IMP_LE; REAL_NOT_LT] THEN
-  SUBGOAL_THEN `!x. ~((q:real^N->real^N) x = c)` ASSUME_TAC THENL
-   [X_GEN_TAC `x:real^N` THEN EXPAND_TAC "q" THEN
-    REWRITE_TAC[NORM_EQ_0; VECTOR_SUB_EQ] THEN COND_CASES_TAC THEN
-    ASM SET_TAC[PATH_COMPONENT_REFL_EQ];
-    ALL_TAC] THEN
-  REPEAT CONJ_TAC THENL
-   [MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
-    SIMP_TAC[CONTINUOUS_ON_SUB; CONTINUOUS_ON_ID; CONTINUOUS_ON_CONST] THEN
-    MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN CONJ_TAC THENL
-     [ASM_MESON_TAC[CONTINUOUS_ON_SUBSET; SUBSET_UNIV]; ALL_TAC] THEN
-    MATCH_MP_TAC CONTINUOUS_ON_ADD THEN REWRITE_TAC[CONTINUOUS_ON_CONST] THEN
-    MATCH_MP_TAC CONTINUOUS_ON_MUL THEN
-    SIMP_TAC[CONTINUOUS_ON_SUB; CONTINUOUS_ON_ID; CONTINUOUS_ON_CONST] THEN
-    REWRITE_TAC[o_DEF; real_div; LIFT_CMUL] THEN
-    MATCH_MP_TAC CONTINUOUS_ON_CMUL THEN
-    MATCH_MP_TAC(REWRITE_RULE[o_DEF] CONTINUOUS_ON_INV) THEN
-    ASM_REWRITE_TAC[FORALL_IN_IMAGE; NORM_EQ_0; VECTOR_SUB_EQ] THEN
-    SUBGOAL_THEN
-     `(\x:real^N. lift(norm(x - c))) = (lift o norm) o (\x. x - c)`
-    SUBST1_TAC THENL [REWRITE_TAC[o_DEF]; ALL_TAC] THEN
-    MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
-    ASM_SIMP_TAC[CONTINUOUS_ON_SUB; CONTINUOUS_ON_ID; CONTINUOUS_ON_CONST;
-                 CONTINUOUS_ON_LIFT_NORM];
-    REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_CBALL; o_THM; dist] THEN
-    X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
-    REWRITE_TAC[VECTOR_ARITH `c - (&2 % c - (c + x)) = x`] THEN
-    REWRITE_TAC[NORM_MUL; REAL_ABS_DIV; REAL_ABS_NORM] THEN
-    ASM_SIMP_TAC[REAL_DIV_RMUL; NORM_EQ_0; VECTOR_SUB_EQ] THEN
-    ASM_REAL_ARITH_TAC;
-    REWRITE_TAC[NOT_EXISTS_THM; TAUT `~(c /\ b) <=> c ==> ~b`] THEN
-    REWRITE_TAC[IN_CBALL; o_THM; dist] THEN
-    X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
-    REWRITE_TAC[VECTOR_ARITH `&2 % c - (c + x') = x <=> --x' = x - c`] THEN
-    ASM_CASES_TAC `(x:real^N) IN path_component s c` THENL
-     [MATCH_MP_TAC(NORM_ARITH `norm(y) < B /\ norm(x) = B ==> ~(--x = y)`) THEN
-      REWRITE_TAC[NORM_MUL; REAL_ABS_DIV; REAL_ABS_NORM] THEN
-      ASM_SIMP_TAC[REAL_DIV_RMUL; NORM_EQ_0; VECTOR_SUB_EQ] THEN
-      ASM_SIMP_TAC[REAL_ARITH `&0 < B ==> abs B = B`] THEN
-      UNDISCH_TAC `path_component s c SUBSET ball(c:real^N,B)` THEN
-      REWRITE_TAC[SUBSET; IN_BALL] THEN ASM_MESON_TAC[dist; NORM_SUB];
-      EXPAND_TAC "q" THEN REWRITE_TAC[] THEN ASM_REWRITE_TAC[] THEN
-      REWRITE_TAC[VECTOR_ARITH `--(c % x) = x <=> (&1 + c) % x = vec 0`] THEN
-      ASM_REWRITE_TAC[DE_MORGAN_THM; VECTOR_SUB_EQ; VECTOR_MUL_EQ_0] THEN
-      SUBGOAL_THEN `~(x:real^N = c)` ASSUME_TAC THENL
-       [ASM_MESON_TAC[PATH_COMPONENT_REFL; IN]; ALL_TAC] THEN
-      ASM_REWRITE_TAC[] THEN
-      MATCH_MP_TAC(REAL_ARITH `&0 < x ==> ~(&1 + x = &0)`) THEN
-      ASM_SIMP_TAC[REAL_LT_DIV; NORM_POS_LT; VECTOR_SUB_EQ]]]);;
-
-let PATH_CONNECTED_COMPLEMENT_HOMEOMORPHIC_INTERVAL = prove
- (`!s:real^N->bool a b:real^M.
-        2 <= dimindex(:N) /\ s homeomorphic interval[a,b]
-        ==> path_connected((:real^N) DIFF s)`,
-  REPEAT STRIP_TAC THEN REWRITE_TAC[PATH_CONNECTED_IFF_PATH_COMPONENT] THEN
-  FIRST_ASSUM(MP_TAC o MATCH_MP
-    UNBOUNDED_PATH_COMPONENTS_COMPLEMENT_HOMEOMORPHIC_INTERVAL) THEN
-  ASM_REWRITE_TAC[SET_RULE `~(x IN s) <=> x IN (UNIV DIFF s)`] THEN
-  ABBREV_TAC `t = (:real^N) DIFF s` THEN
-  DISCH_TAC THEN MAP_EVERY X_GEN_TAC [`x:real^N`; `y:real^N`] THEN
-  STRIP_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP HOMEOMORPHIC_COMPACTNESS) THEN
-  REWRITE_TAC[COMPACT_INTERVAL] THEN
-  DISCH_THEN(MP_TAC o MATCH_MP COMPACT_IMP_BOUNDED) THEN
-  REWRITE_TAC[BOUNDED_POS; LEFT_IMP_EXISTS_THM] THEN
-  X_GEN_TAC `B:real` THEN STRIP_TAC THEN
-  SUBGOAL_THEN `(?u:real^N. u IN path_component t x /\ B < norm(u)) /\
-                (?v:real^N. v IN path_component t y /\ B < norm(v))`
-  STRIP_ASSUME_TAC THENL
-   [ASM_MESON_TAC[BOUNDED_POS; REAL_NOT_LE]; ALL_TAC] THEN
-  MATCH_MP_TAC PATH_COMPONENT_TRANS THEN EXISTS_TAC `u:real^N` THEN
-  CONJ_TAC THENL [ASM_MESON_TAC[IN]; ALL_TAC] THEN
-  MATCH_MP_TAC PATH_COMPONENT_SYM THEN
-  MATCH_MP_TAC PATH_COMPONENT_TRANS THEN EXISTS_TAC `v:real^N` THEN
-  CONJ_TAC THENL [ASM_MESON_TAC[IN]; ALL_TAC] THEN
-  MATCH_MP_TAC PATH_COMPONENT_OF_SUBSET THEN
-  EXISTS_TAC `(:real^N) DIFF cball(vec 0,B)` THEN CONJ_TAC THENL
-   [EXPAND_TAC "t" THEN MATCH_MP_TAC(SET_RULE
-     `s SUBSET t ==> (u DIFF t) SUBSET (u DIFF s)`) THEN
-    ASM_REWRITE_TAC[SUBSET; IN_CBALL_0];
-    MP_TAC(ISPEC `cball(vec 0:real^N,B)`
-       PATH_CONNECTED_COMPLEMENT_BOUNDED_CONVEX) THEN
-    ASM_REWRITE_TAC[BOUNDED_CBALL; CONVEX_CBALL] THEN
-    REWRITE_TAC[PATH_CONNECTED_IFF_PATH_COMPONENT] THEN
-    DISCH_THEN MATCH_MP_TAC THEN
-    ASM_REWRITE_TAC[IN_DIFF; IN_UNIV; IN_CBALL_0; REAL_NOT_LE]]);;
-
-(* ------------------------------------------------------------------------- *)
-(* In particular, apply all these to the special case of an arc.             *)
-(* ------------------------------------------------------------------------- *)
-
-let RETRACTION_ARC = prove
- (`!p. arc p
-       ==> ?f. f continuous_on (:real^N) /\
-               IMAGE f (:real^N) SUBSET path_image p /\
-               (!x. x IN path_image p ==> f x = x)`,
-  REWRITE_TAC[arc; path; path_image] THEN REPEAT STRIP_TAC THEN
-  MATCH_MP_TAC RETRACTION_INJECTIVE_IMAGE_INTERVAL THEN
-  ASM_REWRITE_TAC[INTERVAL_EQ_EMPTY_1; DROP_VEC; REAL_NOT_LT; REAL_POS]);;
-
-let PATH_CONNECTED_ARC_COMPLEMENT = prove
- (`!p. 2 <= dimindex(:N) /\ arc p
-       ==> path_connected((:real^N) DIFF path_image p)`,
-  REWRITE_TAC[arc; path] THEN REPEAT STRIP_TAC THEN SIMP_TAC[path_image] THEN
-  MP_TAC(ISPECL [`path_image p:real^N->bool`; `vec 0:real^1`; `vec 1:real^1`]
-    PATH_CONNECTED_COMPLEMENT_HOMEOMORPHIC_INTERVAL) THEN
-  ASM_REWRITE_TAC[path_image] THEN DISCH_THEN MATCH_MP_TAC THEN
-  ONCE_REWRITE_TAC[HOMEOMORPHIC_SYM] THEN
-  MATCH_MP_TAC HOMEOMORPHIC_COMPACT THEN
-  EXISTS_TAC `p:real^1->real^N` THEN ASM_REWRITE_TAC[COMPACT_INTERVAL]);;
-
-let CONNECTED_ARC_COMPLEMENT = prove
- (`!p. 2 <= dimindex(:N) /\ arc p
-       ==> connected((:real^N) DIFF path_image p)`,
-  SIMP_TAC[PATH_CONNECTED_ARC_COMPLEMENT; PATH_CONNECTED_IMP_CONNECTED]);; *)
-
 end
diff -r cc8db7295249 -r 027879c5637d src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Apr 27 16:24:57 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Apr 27 11:17:50 2010 -0700
@@ -15,17 +15,11 @@
 
 declare vector_add_ldistrib[simp] vector_ssub_ldistrib[simp] vector_smult_assoc[simp] vector_smult_rneg[simp]
 declare vector_sadd_rdistrib[simp] vector_sub_rdistrib[simp]
-declare UNIV_1[simp]
 
 (*lemma dim1in[intro]:"Suc 0 \<in> {1::nat .. CARD(1)}" by auto*)
 
 lemmas vector_component_simps = vector_minus_component vector_smult_component vector_add_component vector_le_def Cart_lambda_beta basis_component vector_uminus_component
 
-lemma dest_vec1_simps[simp]: fixes a::"real^1"
-  shows "a$1 = 0 \<longleftrightarrow> a = 0" (*"a \<le> 1 \<longleftrightarrow> dest_vec1 a \<le> 1" "0 \<le> a \<longleftrightarrow> 0 \<le> dest_vec1 a"*)
-  "a \<le> b \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 b" "dest_vec1 (1::real^1) = 1"
-  by(auto simp add: vector_le_def Cart_eq)
-
 lemma norm_not_0:"(x::real^'n)\<noteq>0 \<Longrightarrow> norm x \<noteq> 0" by auto
 
 lemma setsum_delta_notmem: assumes "x\<notin>s"
@@ -47,31 +41,10 @@
 
 lemma if_smult:"(if P then x else (y::real)) *\<^sub>R v = (if P then x *\<^sub>R v else y *\<^sub>R v)" by auto
 
-lemma mem_interval_1: fixes x :: "real^1" shows
- "(x \<in> {a .. b} \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b)"
- "(x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)"
-by(simp_all add: Cart_eq vector_less_def vector_le_def)
-
 lemma image_smult_interval:"(\<lambda>x. m *\<^sub>R (x::real^'n)) ` {a..b} =
   (if {a..b} = {} then {} else if 0 \<le> m then {m *\<^sub>R a..m *\<^sub>R b} else {m *\<^sub>R b..m *\<^sub>R a})"
   using image_affinity_interval[of m 0 a b] by auto
 
-lemma dest_vec1_inverval:
-  "dest_vec1 ` {a .. b} = {dest_vec1 a .. dest_vec1 b}"
-  "dest_vec1 ` {a<.. b} = {dest_vec1 a<.. dest_vec1 b}"
-  "dest_vec1 ` {a ..<b} = {dest_vec1 a ..<dest_vec1 b}"
-  "dest_vec1 ` {a<..<b} = {dest_vec1 a<..<dest_vec1 b}"
-  apply(rule_tac [!] equalityI)
-  unfolding subset_eq Ball_def Bex_def mem_interval_1 image_iff
-  apply(rule_tac [!] allI)apply(rule_tac [!] impI)
-  apply(rule_tac[2] x="vec1 x" in exI)apply(rule_tac[4] x="vec1 x" in exI)
-  apply(rule_tac[6] x="vec1 x" in exI)apply(rule_tac[8] x="vec1 x" in exI)
-  by (auto simp add: vector_less_def vector_le_def)
-
-lemma dest_vec1_setsum: assumes "finite S"
-  shows " dest_vec1 (setsum f S) = setsum (\<lambda>x. dest_vec1 (f x)) S"
-  using dest_vec1_sum[OF assms] by auto
-
 lemma dist_triangle_eq:
   fixes x y z :: "real ^ _"
   shows "dist x z = dist x y + dist y z \<longleftrightarrow> norm (x - y) *\<^sub>R (y - z) = norm (y - z) *\<^sub>R (x - y)"
@@ -359,9 +332,6 @@
   shows "((1 - u) *\<^sub>R a + u *\<^sub>R b) \<in> s"
   using assms unfolding convex_alt by auto
 
-lemma convex_vec1:"convex (vec1 ` s) = convex (s::real set)"
-  unfolding convex_def Ball_def forall_vec1 unfolding vec1_dest_vec1_simps image_iff by auto
-
 lemma convex_empty[intro]: "convex {}"
   unfolding convex_def by simp
 
@@ -1292,29 +1262,14 @@
   qed
 qed
 
-lemma open_dest_vec1_vimage: "open S \<Longrightarrow> open (dest_vec1 -` S)"
-unfolding open_vector_def forall_1 by auto
-
-lemma tendsto_dest_vec1 [tendsto_intros]:
-  "(f ---> l) net \<Longrightarrow> ((\<lambda>x. dest_vec1 (f x)) ---> dest_vec1 l) net"
-by(rule tendsto_Cart_nth)
-
-lemma continuous_dest_vec1: "continuous net f \<Longrightarrow> continuous net (\<lambda>x. dest_vec1 (f x))"
-  unfolding continuous_def by (rule tendsto_dest_vec1)
-
 (* TODO: move *)
 lemma compact_real_interval:
   fixes a b :: real shows "compact {a..b}"
-proof -
-  have "continuous_on {vec1 a .. vec1 b} dest_vec1"
-    unfolding continuous_on
-    by (simp add: tendsto_dest_vec1 Lim_at_within Lim_ident_at)
-  moreover have "compact {vec1 a .. vec1 b}" by (rule compact_interval)
-  ultimately have "compact (dest_vec1 ` {vec1 a .. vec1 b})"
-    by (rule compact_continuous_image)
-  also have "dest_vec1 ` {vec1 a .. vec1 b} = {a..b}"
-    by (auto simp add: image_def Bex_def exists_vec1)
-  finally show ?thesis .
+proof (rule bounded_closed_imp_compact)
+  have "\<forall>y\<in>{a..b}. dist a y \<le> dist a b"
+    unfolding dist_real_def by auto
+  thus "bounded {a..b}" unfolding bounded_def by fast
+  show "closed {a..b}" by (rule closed_real_atLeastAtMost)
 qed
 
 lemma compact_convex_combinations:
@@ -2015,13 +1970,11 @@
 proof-
   obtain b where b:"b>0" "\<forall>x\<in>s. norm x \<le> b" using compact_imp_bounded[OF assms(1), unfolded bounded_pos] by auto
   let ?A = "{y. \<exists>u. 0 \<le> u \<and> u \<le> b / norm(x) \<and> (y = u *\<^sub>R x)}"
-  have A:"?A = (\<lambda>u. dest_vec1 u *\<^sub>R x) ` {0 .. vec1 (b / norm x)}"
-    unfolding image_image[of "\<lambda>u. u *\<^sub>R x" "\<lambda>x. dest_vec1 x", THEN sym]
-    unfolding dest_vec1_inverval vec1_dest_vec1 by auto
+  have A:"?A = (\<lambda>u. u *\<^sub>R x) ` {0 .. b / norm x}"
+    by auto
   have "compact ?A" unfolding A apply(rule compact_continuous_image, rule continuous_at_imp_continuous_on)
     apply(rule, rule continuous_vmul)
-    apply (rule continuous_dest_vec1)
-    apply(rule continuous_at_id) by(rule compact_interval)
+    apply(rule continuous_at_id) by(rule compact_real_interval)
   moreover have "{y. \<exists>u\<ge>0. u \<le> b / norm x \<and> y = u *\<^sub>R x} \<inter> s \<noteq> {}" apply(rule not_disjointI[OF _ assms(2)])
     unfolding mem_Collect_eq using `b>0` assms(3) by(auto intro!: divide_nonneg_pos)
   ultimately obtain u y where obt: "u\<ge>0" "u \<le> b / norm x" "y = u *\<^sub>R x"
@@ -2232,10 +2185,6 @@
 
 lemma mem_epigraph: "(x, y) \<in> epigraph s f \<longleftrightarrow> x \<in> s \<and> f x \<le> y" unfolding epigraph_def by auto
 
-(** move this**)
-lemma forall_dest_vec1: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P(dest_vec1 x))" 
-  apply safe defer apply(erule_tac x="vec1 x" in allE) by auto
-
 (** This might break sooner or later. In fact it did already once. **)
 lemma convex_epigraph: 
   "convex(epigraph s f) \<longleftrightarrow> convex_on s f \<and> convex s"
@@ -2264,16 +2213,11 @@
   "(\<forall>p. P (fstcart p) (sndcart p)) \<longleftrightarrow> (\<forall>x y. P x y)" apply meson
   apply(erule_tac x="pastecart x y" in allE) unfolding o_def by auto
 
-lemma forall_of_dest_vec1: "(\<forall>v. P (\<lambda>x. dest_vec1 (v x))) \<longleftrightarrow> (\<forall>x. P x)"
-  apply rule apply rule apply(erule_tac x="(vec1 \<circ> x)" in allE) unfolding o_def vec1_dest_vec1 by auto 
-
-lemma forall_of_dest_vec1': "(\<forall>v. P (dest_vec1 v)) \<longleftrightarrow> (\<forall>x. P x)"
-  apply rule apply rule apply(erule_tac x="(vec1 x)" in allE) defer apply rule 
-  apply(erule_tac x="dest_vec1 v" in allE) unfolding o_def vec1_dest_vec1 by auto
-
+(* TODO: move *)
 lemma fst_setsum: "fst (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. fst (f x))"
 by (cases "finite A", induct set: finite, simp_all)
 
+(* TODO: move *)
 lemma snd_setsum: "snd (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. snd (f x))"
 by (cases "finite A", induct set: finite, simp_all)
 
@@ -2322,6 +2266,7 @@
 lemma convex_interval: "convex {a .. b}" "convex {a<..<b::real^'n}"
   apply(rule_tac[!] is_interval_convex) using is_interval_interval by auto
 
+(* FIXME: rewrite these lemmas without using vec1
 subsection {* On @{text "real^1"}, @{text "is_interval"}, @{text "convex"} and @{text "connected"} are all equivalent. *}
 
 lemma is_interval_1:
@@ -2350,33 +2295,33 @@
 lemma convex_connected_1:
   "connected s \<longleftrightarrow> convex (s::(real^1) set)" 
 by(metis is_interval_convex convex_connected is_interval_connected_1)
-
+*)
 subsection {* Another intermediate value theorem formulation. *}
 
-lemma ivt_increasing_component_on_1: fixes f::"real^1 \<Rightarrow> real^'n"
-  assumes "dest_vec1 a \<le> dest_vec1 b" "continuous_on {a .. b} f" "(f a)$k \<le> y" "y \<le> (f b)$k"
+lemma ivt_increasing_component_on_1: fixes f::"real \<Rightarrow> real^'n"
+  assumes "a \<le> b" "continuous_on {a .. b} f" "(f a)$k \<le> y" "y \<le> (f b)$k"
   shows "\<exists>x\<in>{a..b}. (f x)$k = y"
 proof- have "f a \<in> f ` {a..b}" "f b \<in> f ` {a..b}" apply(rule_tac[!] imageI) 
     using assms(1) by(auto simp add: vector_le_def)
   thus ?thesis using connected_ivt_component[of "f ` {a..b}" "f a" "f b" k y]
-    using connected_continuous_image[OF assms(2) convex_connected[OF convex_interval(1)]]
+    using connected_continuous_image[OF assms(2) convex_connected[OF convex_real_interval(5)]]
     using assms by(auto intro!: imageI) qed
 
-lemma ivt_increasing_component_1: fixes f::"real^1 \<Rightarrow> real^'n"
-  shows "dest_vec1 a \<le> dest_vec1 b \<Longrightarrow> \<forall>x\<in>{a .. b}. continuous (at x) f
+lemma ivt_increasing_component_1: fixes f::"real \<Rightarrow> real^'n"
+  shows "a \<le> b \<Longrightarrow> \<forall>x\<in>{a .. b}. continuous (at x) f
    \<Longrightarrow> f a$k \<le> y \<Longrightarrow> y \<le> f b$k \<Longrightarrow> \<exists>x\<in>{a..b}. (f x)$k = y"
 by(rule ivt_increasing_component_on_1)
   (auto simp add: continuous_at_imp_continuous_on)
 
-lemma ivt_decreasing_component_on_1: fixes f::"real^1 \<Rightarrow> real^'n"
-  assumes "dest_vec1 a \<le> dest_vec1 b" "continuous_on {a .. b} f" "(f b)$k \<le> y" "y \<le> (f a)$k"
+lemma ivt_decreasing_component_on_1: fixes f::"real \<Rightarrow> real^'n"
+  assumes "a \<le> b" "continuous_on {a .. b} f" "(f b)$k \<le> y" "y \<le> (f a)$k"
   shows "\<exists>x\<in>{a..b}. (f x)$k = y"
   apply(subst neg_equal_iff_equal[THEN sym]) unfolding vector_uminus_component[THEN sym]
   apply(rule ivt_increasing_component_on_1) using assms using continuous_on_neg
   by auto
 
-lemma ivt_decreasing_component_1: fixes f::"real^1 \<Rightarrow> real^'n"
-  shows "dest_vec1 a \<le> dest_vec1 b \<Longrightarrow> \<forall>x\<in>{a .. b}. continuous (at x) f
+lemma ivt_decreasing_component_1: fixes f::"real \<Rightarrow> real^'n"
+  shows "a \<le> b \<Longrightarrow> \<forall>x\<in>{a .. b}. continuous (at x) f
     \<Longrightarrow> f b$k \<le> y \<Longrightarrow> y \<le> f a$k \<Longrightarrow> \<exists>x\<in>{a..b}. (f x)$k = y"
 by(rule ivt_decreasing_component_on_1)
   (auto simp: continuous_at_imp_continuous_on)
@@ -2872,41 +2817,38 @@
 
 subsection {* Paths. *}
 
-text {* TODO: Once @{const continuous_on} is generalized to arbitrary
-topological spaces, all of these concepts should be similarly generalized. *}
-
 definition
-  path :: "(real \<Rightarrow> 'a::metric_space) \<Rightarrow> bool"
+  path :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool"
   where "path g \<longleftrightarrow> continuous_on {0 .. 1} g"
 
 definition
-  pathstart :: "(real \<Rightarrow> 'a::metric_space) \<Rightarrow> 'a"
+  pathstart :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a"
   where "pathstart g = g 0"
 
 definition
-  pathfinish :: "(real \<Rightarrow> 'a::metric_space) \<Rightarrow> 'a"
+  pathfinish :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a"
   where "pathfinish g = g 1"
 
 definition
-  path_image :: "(real \<Rightarrow> 'a::metric_space) \<Rightarrow> 'a set"
+  path_image :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> 'a set"
   where "path_image g = g ` {0 .. 1}"
 
 definition
-  reversepath :: "(real \<Rightarrow> 'a::metric_space) \<Rightarrow> (real \<Rightarrow> 'a)"
+  reversepath :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> (real \<Rightarrow> 'a)"
   where "reversepath g = (\<lambda>x. g(1 - x))"
 
 definition
-  joinpaths :: "(real \<Rightarrow> 'a::metric_space) \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> (real \<Rightarrow> 'a)"
+  joinpaths :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> (real \<Rightarrow> 'a)"
     (infixr "+++" 75)
   where "g1 +++ g2 = (\<lambda>x. if x \<le> 1/2 then g1 (2 * x) else g2 (2 * x - 1))"
 
 definition
-  simple_path :: "(real \<Rightarrow> 'a::metric_space) \<Rightarrow> bool"
+  simple_path :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool"
   where "simple_path g \<longleftrightarrow>
   (\<forall>x\<in>{0..1}. \<forall>y\<in>{0..1}. g x = g y \<longrightarrow> x = y \<or> x = 0 \<and> y = 1 \<or> x = 1 \<and> y = 0)"
 
 definition
-  injective_path :: "(real \<Rightarrow> 'a::metric_space) \<Rightarrow> bool"
+  injective_path :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool"
   where "injective_path g \<longleftrightarrow> (\<forall>x\<in>{0..1}. \<forall>y\<in>{0..1}. g x = g y \<longrightarrow> x = y)"
 
 subsection {* Some lemmas about these concepts. *}
@@ -3037,7 +2979,7 @@
 lemma simple_path_reversepath: assumes "simple_path g" shows "simple_path (reversepath g)"
   using assms unfolding simple_path_def reversepath_def apply- apply(rule ballI)+
   apply(erule_tac x="1-x" in ballE, erule_tac x="1-y" in ballE)
-  unfolding mem_interval_1 by auto
+  by auto
 
 lemma simple_path_join_loop:
   assumes "injective_path g1" "injective_path g2" "pathfinish g2 = pathstart g1"
@@ -3050,36 +2992,36 @@
     assume as:"x \<le> 1 / 2" "y \<le> 1 / 2"
     hence "g1 (2 *\<^sub>R x) = g1 (2 *\<^sub>R y)" using xy(3) unfolding joinpaths_def by auto
     moreover have "2 *\<^sub>R x \<in> {0..1}" "2 *\<^sub>R y \<in> {0..1}" using xy(1,2) as
-      unfolding mem_interval_1 by auto
+      by auto
     ultimately show ?thesis using inj(1)[of "2*\<^sub>R x" "2*\<^sub>R y"] by auto
   next assume as:"x > 1 / 2" "y > 1 / 2"
     hence "g2 (2 *\<^sub>R x - 1) = g2 (2 *\<^sub>R y - 1)" using xy(3) unfolding joinpaths_def by auto
-    moreover have "2 *\<^sub>R x - 1 \<in> {0..1}" "2 *\<^sub>R y - 1 \<in> {0..1}" using xy(1,2) as unfolding mem_interval_1 by auto
+    moreover have "2 *\<^sub>R x - 1 \<in> {0..1}" "2 *\<^sub>R y - 1 \<in> {0..1}" using xy(1,2) as by auto
     ultimately show ?thesis using inj(2)[of "2*\<^sub>R x - 1" "2*\<^sub>R y - 1"] by auto
   next assume as:"x \<le> 1 / 2" "y > 1 / 2"
     hence "?g x \<in> path_image g1" "?g y \<in> path_image g2" unfolding path_image_def joinpaths_def
-      using xy(1,2)[unfolded mem_interval_1] by auto
+      using xy(1,2) by auto
     moreover have "?g y \<noteq> pathstart g2" using as(2) unfolding pathstart_def joinpaths_def
-      using inj(2)[of "2 *\<^sub>R y - 1" 0] and xy(2)[unfolded mem_interval_1]
+      using inj(2)[of "2 *\<^sub>R y - 1" 0] and xy(2)
       by (auto simp add: field_simps)
     ultimately have *:"?g x = pathstart g1" using assms(4) unfolding xy(3) by auto
-    hence "x = 0" unfolding pathstart_def joinpaths_def using as(1) and xy(1)[unfolded mem_interval_1]
+    hence "x = 0" unfolding pathstart_def joinpaths_def using as(1) and xy(1)
       using inj(1)[of "2 *\<^sub>R x" 0] by auto
     moreover have "y = 1" using * unfolding xy(3) assms(3)[THEN sym]
-      unfolding joinpaths_def pathfinish_def using as(2) and xy(2)[unfolded mem_interval_1]
+      unfolding joinpaths_def pathfinish_def using as(2) and xy(2)
       using inj(2)[of "2 *\<^sub>R y - 1" 1] by auto
     ultimately show ?thesis by auto
   next assume as:"x > 1 / 2" "y \<le> 1 / 2"
     hence "?g x \<in> path_image g2" "?g y \<in> path_image g1" unfolding path_image_def joinpaths_def
-      using xy(1,2)[unfolded mem_interval_1] by auto
+      using xy(1,2) by auto
     moreover have "?g x \<noteq> pathstart g2" using as(1) unfolding pathstart_def joinpaths_def
-      using inj(2)[of "2 *\<^sub>R x - 1" 0] and xy(1)[unfolded mem_interval_1]
+      using inj(2)[of "2 *\<^sub>R x - 1" 0] and xy(1)
       by (auto simp add: field_simps)
     ultimately have *:"?g y = pathstart g1" using assms(4) unfolding xy(3) by auto
-    hence "y = 0" unfolding pathstart_def joinpaths_def using as(2) and xy(2)[unfolded mem_interval_1]
+    hence "y = 0" unfolding pathstart_def joinpaths_def using as(2) and xy(2)
       using inj(1)[of "2 *\<^sub>R y" 0] by auto
     moreover have "x = 1" using * unfolding xy(3)[THEN sym] assms(3)[THEN sym]
-      unfolding joinpaths_def pathfinish_def using as(1) and xy(1)[unfolded mem_interval_1]
+      unfolding joinpaths_def pathfinish_def using as(1) and xy(1)
       using inj(2)[of "2 *\<^sub>R x - 1" 1] by auto
     ultimately show ?thesis by auto qed qed
 
@@ -3092,29 +3034,29 @@
   fix x y assume xy:"x \<in> {0..1}" "y \<in> {0..1}" "(g1 +++ g2) x = (g1 +++ g2) y"
   show "x = y" proof(cases "x \<le> 1/2", case_tac[!] "y \<le> 1/2", unfold not_le)
     assume "x \<le> 1 / 2" "y \<le> 1 / 2" thus ?thesis using inj(1)[of "2*\<^sub>R x" "2*\<^sub>R y"] and xy
-      unfolding mem_interval_1 joinpaths_def by auto
+      unfolding joinpaths_def by auto
   next assume "x > 1 / 2" "y > 1 / 2" thus ?thesis using inj(2)[of "2*\<^sub>R x - 1" "2*\<^sub>R y - 1"] and xy
-      unfolding mem_interval_1 joinpaths_def by auto
+      unfolding joinpaths_def by auto
   next assume as:"x \<le> 1 / 2" "y > 1 / 2" 
     hence "?g x \<in> path_image g1" "?g y \<in> path_image g2" unfolding path_image_def joinpaths_def
-      using xy(1,2)[unfolded mem_interval_1] by auto
+      using xy(1,2) by auto
     hence "?g x = pathfinish g1" "?g y = pathstart g2" using assms(4) unfolding assms(3) xy(3) by auto
     thus ?thesis using as and inj(1)[of "2 *\<^sub>R x" 1] inj(2)[of "2 *\<^sub>R y - 1" 0] and xy(1,2)
-      unfolding pathstart_def pathfinish_def joinpaths_def mem_interval_1
+      unfolding pathstart_def pathfinish_def joinpaths_def
       by auto
   next assume as:"x > 1 / 2" "y \<le> 1 / 2" 
     hence "?g x \<in> path_image g2" "?g y \<in> path_image g1" unfolding path_image_def joinpaths_def
-      using xy(1,2)[unfolded mem_interval_1] by auto
+      using xy(1,2) by auto
     hence "?g x = pathstart g2" "?g y = pathfinish g1" using assms(4) unfolding assms(3) xy(3) by auto
     thus ?thesis using as and inj(2)[of "2 *\<^sub>R x - 1" 0] inj(1)[of "2 *\<^sub>R y" 1] and xy(1,2)
-      unfolding pathstart_def pathfinish_def joinpaths_def mem_interval_1
+      unfolding pathstart_def pathfinish_def joinpaths_def
       by auto qed qed
 
 lemmas join_paths_simps = path_join path_image_join pathstart_join pathfinish_join
  
 subsection {* Reparametrizing a closed curve to start at some chosen point. *}
 
-definition "shiftpath a (f::real \<Rightarrow> 'a::metric_space) =
+definition "shiftpath a (f::real \<Rightarrow> 'a::topological_space) =
   (\<lambda>x. if (a + x) \<le> 1 then f(a + x) else f(a + x - 1))"
 
 lemma pathstart_shiftpath: "a \<le> 1 \<Longrightarrow> pathstart(shiftpath a g) = g a"
@@ -3178,8 +3120,7 @@
   unfolding pathfinish_def linepath_def by auto
 
 lemma continuous_linepath_at[intro]: "continuous (at x) (linepath a b)"
-  unfolding linepath_def
-  by (intro continuous_intros continuous_dest_vec1)
+  unfolding linepath_def by (intro continuous_intros)
 
 lemma continuous_on_linepath[intro]: "continuous_on s (linepath a b)"
   using continuous_linepath_at by(auto intro!: continuous_at_imp_continuous_on)
diff -r cc8db7295249 -r 027879c5637d src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Apr 27 16:24:57 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Apr 27 11:17:50 2010 -0700
@@ -6,16 +6,13 @@
 header {* Multivariate calculus in Euclidean space. *}
 
 theory Derivative
-imports Brouwer_Fixpoint RealVector
+imports Brouwer_Fixpoint Vec1 RealVector
 begin
 
 
 (* Because I do not want to type this all the time *)
 lemmas linear_linear = linear_conv_bounded_linear[THEN sym]
 
-(** move this **)
-declare norm_vec1[simp]
-
 subsection {* Derivatives *}
 
 text {* The definition is slightly tricky since we make it work over
@@ -94,16 +91,6 @@
 
 subsection {* Derivatives on real = Derivatives on @{typ "real^1"} *}
 
-lemma dist_vec1_0[simp]: "dist(vec1 (x::real)) 0 = norm x" unfolding vector_dist_norm by auto
-
-lemma bounded_linear_vec1_dest_vec1: fixes f::"real \<Rightarrow> real"
-  shows "linear (vec1 \<circ> f \<circ> dest_vec1) = bounded_linear f" (is "?l = ?r") proof-
-  { assume ?l guess K using linear_bounded[OF `?l`] ..
-    hence "\<exists>K. \<forall>x. \<bar>f x\<bar> \<le> \<bar>x\<bar> * K" apply(rule_tac x=K in exI)
-      unfolding vec1_dest_vec1_simps by (auto simp add:field_simps) }
-  thus ?thesis unfolding linear_def bounded_linear_def additive_def bounded_linear_axioms_def o_def
-    unfolding vec1_dest_vec1_simps by auto qed 
-
 lemma has_derivative_within_vec1_dest_vec1: fixes f::"real\<Rightarrow>real" shows
   "((vec1 \<circ> f \<circ> dest_vec1) has_derivative (vec1 \<circ> f' \<circ> dest_vec1)) (at (vec1 x) within vec1 ` s)
   = (f has_derivative f') (at x within s)"
@@ -156,14 +143,14 @@
 lemma has_derivative_const: "((\<lambda>x. c) has_derivative (\<lambda>h. 0)) net"
   unfolding has_derivative_def apply(rule,rule bounded_linear_zero) by(simp add: Lim_const)
 
-lemma (in bounded_linear) cmul: shows "bounded_linear (\<lambda>x. (c::real) *\<^sub>R f x)" proof
-  guess K using pos_bounded ..
-  thus "\<exists>K. \<forall>x. norm ((c::real) *\<^sub>R f x) \<le> norm x * K" apply(rule_tac x="abs c * K" in exI) proof
-    fix x case goal1
-    hence "abs c * norm (f x) \<le> abs c * (norm x * K)" apply-apply(erule conjE,erule_tac x=x in allE)  
-      apply(rule mult_left_mono) by auto
-    thus ?case by(auto simp add:field_simps)
-  qed qed(auto simp add: scaleR.add_right add scaleR)
+lemma (in bounded_linear) cmul: shows "bounded_linear (\<lambda>x. (c::real) *\<^sub>R f x)"
+proof -
+  have "bounded_linear (\<lambda>x. c *\<^sub>R x)"
+    by (rule scaleR.bounded_linear_right)
+  moreover have "bounded_linear f" ..
+  ultimately show ?thesis
+    by (rule bounded_linear_compose)
+qed
 
 lemma has_derivative_cmul: assumes "(f has_derivative f') net" shows "((\<lambda>x. c *\<^sub>R f(x)) has_derivative (\<lambda>h. c *\<^sub>R f'(h))) net"
   unfolding has_derivative_def apply(rule,rule bounded_linear.cmul)
@@ -647,11 +634,6 @@
 
 subsection {* The traditional Rolle theorem in one dimension. *}
 
-lemma vec1_le[simp]:fixes a::real shows "vec1 a \<le> vec1 b \<longleftrightarrow> a \<le> b"
-  unfolding vector_le_def by auto
-lemma vec1_less[simp]:fixes a::real shows "vec1 a < vec1 b \<longleftrightarrow> a < b"
-  unfolding vector_less_def by auto 
-
 lemma rolle: fixes f::"real\<Rightarrow>real"
   assumes "a < b" "f a = f b" "continuous_on {a..b} f"
   "\<forall>x\<in>{a<..<b}. (f has_derivative f'(x)) (at x)"
@@ -763,6 +745,9 @@
   have 4:"{norm (f x) |x. norm x = 1} = (\<lambda>x. norm (f x)) ` {x. norm x=1}" by auto
   show ?thesis unfolding onorm_def 1 2 3 4 by(simp add:Sup_finite_Max) qed
 
+lemma convex_vec1:"convex (vec1 ` s) = convex (s::real set)"
+  unfolding convex_def Ball_def forall_vec1 unfolding vec1_dest_vec1_simps image_iff by auto
+
 lemma differentiable_bound_real: fixes f::"real \<Rightarrow> real"
   assumes "convex s" "\<forall>x\<in>s. (f has_derivative f' x) (at x within s)" "\<forall>x\<in>s. onorm(f' x) \<le> B" and x:"x\<in>s" and y:"y\<in>s"
   shows "norm(f x - f y) \<le> B * norm(x - y)" 
diff -r cc8db7295249 -r 027879c5637d src/HOL/Multivariate_Analysis/Determinants.thy
--- a/src/HOL/Multivariate_Analysis/Determinants.thy	Tue Apr 27 16:24:57 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy	Tue Apr 27 11:17:50 2010 -0700
@@ -5,7 +5,7 @@
 header {* Traces, Determinant of square matrices and some properties *}
 
 theory Determinants
-imports Euclidean_Space Permutations
+imports Euclidean_Space Permutations Vec1
 begin
 
 subsection{* First some facts about products*}
diff -r cc8db7295249 -r 027879c5637d src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Tue Apr 27 16:24:57 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Tue Apr 27 11:17:50 2010 -0700
@@ -12,56 +12,6 @@
 uses "positivstellensatz.ML" ("normarith.ML")
 begin
 
-text{* Some common special cases.*}
-
-lemma forall_1[simp]: "(\<forall>i::1. P i) \<longleftrightarrow> P 1"
-  by (metis num1_eq_iff)
-
-lemma ex_1[simp]: "(\<exists>x::1. P x) \<longleftrightarrow> P 1"
-  by auto (metis num1_eq_iff)
-
-lemma exhaust_2:
-  fixes x :: 2 shows "x = 1 \<or> x = 2"
-proof (induct x)
-  case (of_int z)
-  then have "0 <= z" and "z < 2" by simp_all
-  then have "z = 0 | z = 1" by arith
-  then show ?case by auto
-qed
-
-lemma forall_2: "(\<forall>i::2. P i) \<longleftrightarrow> P 1 \<and> P 2"
-  by (metis exhaust_2)
-
-lemma exhaust_3:
-  fixes x :: 3 shows "x = 1 \<or> x = 2 \<or> x = 3"
-proof (induct x)
-  case (of_int z)
-  then have "0 <= z" and "z < 3" by simp_all
-  then have "z = 0 \<or> z = 1 \<or> z = 2" by arith
-  then show ?case by auto
-qed
-
-lemma forall_3: "(\<forall>i::3. P i) \<longleftrightarrow> P 1 \<and> P 2 \<and> P 3"
-  by (metis exhaust_3)
-
-lemma UNIV_1: "UNIV = {1::1}"
-  by (auto simp add: num1_eq_iff)
-
-lemma UNIV_2: "UNIV = {1::2, 2::2}"
-  using exhaust_2 by auto
-
-lemma UNIV_3: "UNIV = {1::3, 2::3, 3::3}"
-  using exhaust_3 by auto
-
-lemma setsum_1: "setsum f (UNIV::1 set) = f 1"
-  unfolding UNIV_1 by simp
-
-lemma setsum_2: "setsum f (UNIV::2 set) = f 1 + f 2"
-  unfolding UNIV_2 by simp
-
-lemma setsum_3: "setsum f (UNIV::3 set) = f 1 + f 2 + f 3"
-  unfolding UNIV_3 by (simp add: add_ac)
-
 subsection{* Basic componentwise operations on vectors. *}
 
 instantiation cart :: (plus,finite) plus
@@ -114,7 +64,7 @@
   instance by (intro_classes)
 end
 
-text{* The ordering on @{typ "real^1"} is linear. *}
+text{* The ordering on one-dimensional vectors is linear. *}
 
 class cart_one = assumes UNIV_one: "card (UNIV \<Colon> 'a set) = Suc 0"
 begin
@@ -123,11 +73,6 @@
       by (auto intro!: card_ge_0_finite) qed
 end
 
-instantiation num1 :: cart_one begin
-instance proof
-  show "CARD(1) = Suc 0" by auto
-qed end
-
 instantiation cart :: (linorder,cart_one) linorder begin
 instance proof
   guess a B using UNIV_one[where 'a='b] unfolding card_Suc_eq apply- by(erule exE)+
@@ -654,39 +599,6 @@
 
 end
 
-lemma setsum_squares_eq_0_iff: assumes fS: "finite F" and fp: "\<forall>x \<in> F. f x \<ge> (0 ::'a::ordered_ab_group_add)" shows "setsum f F = 0 \<longleftrightarrow> (ALL x:F. f x = 0)"
-using fS fp setsum_nonneg[OF fp]
-proof (induct set: finite)
-  case empty thus ?case by simp
-next
-  case (insert x F)
-  from insert.prems have Fx: "f x \<ge> 0" and Fp: "\<forall> a \<in> F. f a \<ge> 0" by simp_all
-  from insert.hyps Fp setsum_nonneg[OF Fp]
-  have h: "setsum f F = 0 \<longleftrightarrow> (\<forall>a \<in>F. f a = 0)" by metis
-  from add_nonneg_eq_0_iff[OF Fx  setsum_nonneg[OF Fp]] insert.hyps(1,2)
-  show ?case by (simp add: h)
-qed
-
-subsection{* The collapse of the general concepts to dimension one. *}
-
-lemma vector_one: "(x::'a ^1) = (\<chi> i. (x$1))"
-  by (simp add: Cart_eq)
-
-lemma forall_one: "(\<forall>(x::'a ^1). P x) \<longleftrightarrow> (\<forall>x. P(\<chi> i. x))"
-  apply auto
-  apply (erule_tac x= "x$1" in allE)
-  apply (simp only: vector_one[symmetric])
-  done
-
-lemma norm_vector_1: "norm (x :: _^1) = norm (x$1)"
-  by (simp add: norm_vector_def UNIV_1)
-
-lemma norm_real: "norm(x::real ^ 1) = abs(x$1)"
-  by (simp add: norm_vector_1)
-
-lemma dist_real: "dist(x::real ^ 1) y = abs((x$1) - (y$1))"
-  by (auto simp add: norm_real dist_norm)
-
 subsection {* A connectedness or intermediate value lemma with several applications. *}
 
 lemma connected_real_lemma:
@@ -747,7 +659,7 @@
     ultimately show ?thesis using alb by metis
 qed
 
-text{* One immediately useful corollary is the existence of square roots! --- Should help to get rid of all the development of square-root for reals as a special case @{typ "real^1"} *}
+text{* One immediately useful corollary is the existence of square roots! --- Should help to get rid of all the development of square-root for reals as a special case *}
 
 lemma square_bound_lemma: "(x::real) < (1 + x) * (1 + x)"
 proof-
@@ -1364,67 +1276,6 @@
 lemma orthogonal_commute: "orthogonal (x::real ^'n)y \<longleftrightarrow> orthogonal y x"
   by (simp add: orthogonal_def inner_commute)
 
-subsection{* Explicit vector construction from lists. *}
-
-primrec from_nat :: "nat \<Rightarrow> 'a::{monoid_add,one}"
-where "from_nat 0 = 0" | "from_nat (Suc n) = 1 + from_nat n"
-
-lemma from_nat [simp]: "from_nat = of_nat"
-by (rule ext, induct_tac x, simp_all)
-
-primrec
-  list_fun :: "nat \<Rightarrow> _ list \<Rightarrow> _ \<Rightarrow> _"
-where
-  "list_fun n [] = (\<lambda>x. 0)"
-| "list_fun n (x # xs) = fun_upd (list_fun (Suc n) xs) (from_nat n) x"
-
-definition "vector l = (\<chi> i. list_fun 1 l i)"
-(*definition "vector l = (\<chi> i. if i <= length l then l ! (i - 1) else 0)"*)
-
-lemma vector_1: "(vector[x]) $1 = x"
-  unfolding vector_def by simp
-
-lemma vector_2:
- "(vector[x,y]) $1 = x"
- "(vector[x,y] :: 'a^2)$2 = (y::'a::zero)"
-  unfolding vector_def by simp_all
-
-lemma vector_3:
- "(vector [x,y,z] ::('a::zero)^3)$1 = x"
- "(vector [x,y,z] ::('a::zero)^3)$2 = y"
- "(vector [x,y,z] ::('a::zero)^3)$3 = z"
-  unfolding vector_def by simp_all
-
-lemma forall_vector_1: "(\<forall>v::'a::zero^1. P v) \<longleftrightarrow> (\<forall>x. P(vector[x]))"
-  apply auto
-  apply (erule_tac x="v$1" in allE)
-  apply (subgoal_tac "vector [v$1] = v")
-  apply simp
-  apply (vector vector_def)
-  apply simp
-  done
-
-lemma forall_vector_2: "(\<forall>v::'a::zero^2. P v) \<longleftrightarrow> (\<forall>x y. P(vector[x, y]))"
-  apply auto
-  apply (erule_tac x="v$1" in allE)
-  apply (erule_tac x="v$2" in allE)
-  apply (subgoal_tac "vector [v$1, v$2] = v")
-  apply simp
-  apply (vector vector_def)
-  apply (simp add: forall_2)
-  done
-
-lemma forall_vector_3: "(\<forall>v::'a::zero^3. P v) \<longleftrightarrow> (\<forall>x y z. P(vector[x, y, z]))"
-  apply auto
-  apply (erule_tac x="v$1" in allE)
-  apply (erule_tac x="v$2" in allE)
-  apply (erule_tac x="v$3" in allE)
-  apply (subgoal_tac "vector [v$1, v$2, v$3] = v")
-  apply simp
-  apply (vector vector_def)
-  apply (simp add: forall_3)
-  done
-
 subsection{* Linear functions. *}
 
 definition "linear f \<longleftrightarrow> (\<forall>x y. f(x + y) = f x + f y) \<and> (\<forall>c x. f(c *s x) = c *s f x)"
@@ -2216,33 +2067,6 @@
   apply (rule onorm_triangle)
   by assumption+
 
-(* "lift" from 'a to 'a^1 and "drop" from 'a^1 to 'a -- FIXME: potential use of transfer *)
-
-abbreviation vec1:: "'a \<Rightarrow> 'a ^ 1" where "vec1 x \<equiv> vec x"
-
-abbreviation dest_vec1:: "'a ^1 \<Rightarrow> 'a"
-  where "dest_vec1 x \<equiv> (x$1)"
-
-lemma vec1_component[simp]: "(vec1 x)$1 = x"
-  by simp
-
-lemma vec1_dest_vec1: "vec1(dest_vec1 x) = x" "dest_vec1(vec1 y) = y"
-  by (simp_all add:  Cart_eq)
-
-declare vec1_dest_vec1(1) [simp]
-
-lemma forall_vec1: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (vec1 x))"
-  by (metis vec1_dest_vec1(1))
-
-lemma exists_vec1: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P(vec1 x))"
-  by (metis vec1_dest_vec1(1))
-
-lemma vec1_eq[simp]:  "vec1 x = vec1 y \<longleftrightarrow> x = y"
-  by (metis vec1_dest_vec1(2))
-
-lemma dest_vec1_eq[simp]: "dest_vec1 x = dest_vec1 y \<longleftrightarrow> x = y"
-  by (metis vec1_dest_vec1(1))
-
 lemma vec_in_image_vec: "vec x \<in> (vec ` S) \<longleftrightarrow> x \<in> S" by auto
 
 lemma vec_add: "vec(x + y) = vec x + vec y"  by (vector vec_def)
@@ -2250,9 +2074,6 @@
 lemma vec_cmul: "vec(c* x) = c *s vec x " by (vector vec_def)
 lemma vec_neg: "vec(- x) = - vec x " by (vector vec_def)
 
-lemma range_vec1[simp]:"range vec1 = UNIV" apply(rule set_ext,rule) unfolding image_iff defer
-  apply(rule_tac x="dest_vec1 x" in bexI) by auto
-
 lemma vec_setsum: assumes fS: "finite S"
   shows "vec(setsum f S) = setsum (vec o f) S"
   apply (induct rule: finite_induct[OF fS])
@@ -2260,70 +2081,6 @@
   apply (auto simp add: vec_add)
   done
 
-lemma dest_vec1_lambda: "dest_vec1(\<chi> i. x i) = x 1"
-  by (simp)
-
-lemma dest_vec1_vec: "dest_vec1(vec x) = x"
-  by (simp)
-
-lemma dest_vec1_sum: assumes fS: "finite S"
-  shows "dest_vec1(setsum f S) = setsum (dest_vec1 o f) S"
-  apply (induct rule: finite_induct[OF fS])
-  apply simp
-  apply auto
-  done
-
-lemma norm_vec1: "norm(vec1 x) = abs(x)"
-  by (simp add: vec_def norm_real)
-
-lemma dist_vec1: "dist(vec1 x) (vec1 y) = abs(x - y)"
-  by (simp only: dist_real vec1_component)
-lemma abs_dest_vec1: "norm x = \<bar>dest_vec1 x\<bar>"
-  by (metis vec1_dest_vec1(1) norm_vec1)
-
-lemmas vec1_dest_vec1_simps = forall_vec1 vec_add[THEN sym] dist_vec1 vec_sub[THEN sym] vec1_dest_vec1 norm_vec1 vector_smult_component
-   vec1_eq vec_cmul[THEN sym] smult_conv_scaleR[THEN sym] o_def dist_real_def norm_vec1 real_norm_def
-
-lemma bounded_linear_vec1:"bounded_linear (vec1::real\<Rightarrow>real^1)"
-  unfolding bounded_linear_def additive_def bounded_linear_axioms_def 
-  unfolding smult_conv_scaleR[THEN sym] unfolding vec1_dest_vec1_simps
-  apply(rule conjI) defer apply(rule conjI) defer apply(rule_tac x=1 in exI) by auto
-
-lemma linear_vmul_dest_vec1:
-  fixes f:: "'a::semiring_1^_ \<Rightarrow> 'a^1"
-  shows "linear f \<Longrightarrow> linear (\<lambda>x. dest_vec1(f x) *s v)"
-  apply (rule linear_vmul_component)
-  by auto
-
-lemma linear_from_scalars:
-  assumes lf: "linear (f::'a::comm_ring_1 ^1 \<Rightarrow> 'a^_)"
-  shows "f = (\<lambda>x. dest_vec1 x *s column 1 (matrix f))"
-  apply (rule ext)
-  apply (subst matrix_works[OF lf, symmetric])
-  apply (auto simp add: Cart_eq matrix_vector_mult_def column_def  mult_commute UNIV_1)
-  done
-
-lemma linear_to_scalars: assumes lf: "linear (f::real ^'n \<Rightarrow> real^1)"
-  shows "f = (\<lambda>x. vec1(row 1 (matrix f) \<bullet> x))"
-  apply (rule ext)
-  apply (subst matrix_works[OF lf, symmetric])
-  apply (simp add: Cart_eq matrix_vector_mult_def row_def inner_vector_def mult_commute)
-  done
-
-lemma dest_vec1_eq_0: "dest_vec1 x = 0 \<longleftrightarrow> x = 0"
-  by (simp add: dest_vec1_eq[symmetric])
-
-lemma setsum_scalars: assumes fS: "finite S"
-  shows "setsum f S = vec1 (setsum (dest_vec1 o f) S)"
-  unfolding vec_setsum[OF fS] by simp
-
-lemma dest_vec1_wlog_le: "(\<And>(x::'a::linorder ^ 1) y. P x y \<longleftrightarrow> P y x)  \<Longrightarrow> (\<And>x y. dest_vec1 x <= dest_vec1 y ==> P x y) \<Longrightarrow> P x y"
-  apply (cases "dest_vec1 x \<le> dest_vec1 y")
-  apply simp
-  apply (subgoal_tac "dest_vec1 y \<le> dest_vec1 x")
-  apply (auto)
-  done
-
 text{* Pasting vectors. *}
 
 lemma linear_fstcart[intro]: "linear fstcart"
diff -r cc8db7295249 -r 027879c5637d src/HOL/Multivariate_Analysis/Fashoda.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Multivariate_Analysis/Fashoda.thy	Tue Apr 27 11:17:50 2010 -0700
@@ -0,0 +1,556 @@
+(* Author:                     John Harrison
+   Translation from HOL light: Robert Himmelmann, TU Muenchen *)
+
+header {* Fashoda meet theorem. *}
+
+theory Fashoda
+imports Brouwer_Fixpoint Vec1
+begin
+
+subsection {*Fashoda meet theorem. *}
+
+lemma infnorm_2: "infnorm (x::real^2) = max (abs(x$1)) (abs(x$2))"
+  unfolding infnorm_def UNIV_2 apply(rule Sup_eq) by auto
+
+lemma infnorm_eq_1_2: "infnorm (x::real^2) = 1 \<longleftrightarrow>
+        (abs(x$1) \<le> 1 \<and> abs(x$2) \<le> 1 \<and> (x$1 = -1 \<or> x$1 = 1 \<or> x$2 = -1 \<or> x$2 = 1))"
+  unfolding infnorm_2 by auto
+
+lemma infnorm_eq_1_imp: assumes "infnorm (x::real^2) = 1" shows "abs(x$1) \<le> 1" "abs(x$2) \<le> 1"
+  using assms unfolding infnorm_eq_1_2 by auto
+
+lemma fashoda_unit: fixes f g::"real \<Rightarrow> real^2"
+  assumes "f ` {- 1..1} \<subseteq> {- 1..1}" "g ` {- 1..1} \<subseteq> {- 1..1}"
+  "continuous_on {- 1..1} f"  "continuous_on {- 1..1} g"
+  "f (- 1)$1 = - 1" "f 1$1 = 1" "g (- 1) $2 = -1" "g 1 $2 = 1"
+  shows "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. f s = g t" proof(rule ccontr)
+  case goal1 note as = this[unfolded bex_simps,rule_format]
+  def sqprojection \<equiv> "\<lambda>z::real^2. (inverse (infnorm z)) *\<^sub>R z" 
+  def negatex \<equiv> "\<lambda>x::real^2. (vector [-(x$1), x$2])::real^2" 
+  have lem1:"\<forall>z::real^2. infnorm(negatex z) = infnorm z"
+    unfolding negatex_def infnorm_2 vector_2 by auto
+  have lem2:"\<forall>z. z\<noteq>0 \<longrightarrow> infnorm(sqprojection z) = 1" unfolding sqprojection_def
+    unfolding infnorm_mul[unfolded smult_conv_scaleR] unfolding abs_inverse real_abs_infnorm
+    unfolding infnorm_eq_0[THEN sym] by auto
+  let ?F = "(\<lambda>w::real^2. (f \<circ> (\<lambda>x. x$1)) w - (g \<circ> (\<lambda>x. x$2)) w)"
+  have *:"\<And>i. (\<lambda>x::real^2. x $ i) ` {- 1..1} = {- 1..1::real}"
+    apply(rule set_ext) unfolding image_iff Bex_def mem_interval apply rule defer 
+    apply(rule_tac x="vec x" in exI) by auto
+  { fix x assume "x \<in> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w) ` {- 1..1::real^2}"
+    then guess w unfolding image_iff .. note w = this
+    hence "x \<noteq> 0" using as[of "w$1" "w$2"] unfolding mem_interval by auto} note x0=this
+  have 21:"\<And>i::2. i\<noteq>1 \<Longrightarrow> i=2" using UNIV_2 by auto
+  have 1:"{- 1<..<1::real^2} \<noteq> {}" unfolding interval_eq_empty by auto
+  have 2:"continuous_on {- 1..1} (negatex \<circ> sqprojection \<circ> ?F)" apply(rule continuous_on_intros continuous_on_component continuous_on_vec1)+
+    prefer 2 apply(rule continuous_on_intros continuous_on_component continuous_on_vec1)+ unfolding *
+    apply(rule assms)+ apply(rule continuous_on_compose,subst sqprojection_def)
+    apply(rule continuous_on_mul ) apply(rule continuous_at_imp_continuous_on,rule) apply(rule continuous_at_inv[unfolded o_def])
+    apply(rule continuous_at_infnorm) unfolding infnorm_eq_0 defer apply(rule continuous_on_id) apply(rule linear_continuous_on) proof-
+    show "bounded_linear negatex" apply(rule bounded_linearI') unfolding Cart_eq proof(rule_tac[!] allI) fix i::2 and x y::"real^2" and c::real
+      show "negatex (x + y) $ i = (negatex x + negatex y) $ i" "negatex (c *s x) $ i = (c *s negatex x) $ i"
+	apply-apply(case_tac[!] "i\<noteq>1") prefer 3 apply(drule_tac[1-2] 21) 
+	unfolding negatex_def by(auto simp add:vector_2 ) qed qed(insert x0, auto)
+  have 3:"(negatex \<circ> sqprojection \<circ> ?F) ` {- 1..1} \<subseteq> {- 1..1}" unfolding subset_eq apply rule proof-
+    case goal1 then guess y unfolding image_iff .. note y=this have "?F y \<noteq> 0" apply(rule x0) using y(1) by auto
+    hence *:"infnorm (sqprojection (?F y)) = 1" unfolding y o_def apply- by(rule lem2[rule_format])
+    have "infnorm x = 1" unfolding *[THEN sym] y o_def by(rule lem1[rule_format])
+    thus "x\<in>{- 1..1}" unfolding mem_interval infnorm_2 apply- apply rule
+    proof-case goal1 thus ?case apply(cases "i=1") defer apply(drule 21) by auto qed qed
+  guess x apply(rule brouwer_weak[of "{- 1..1::real^2}" "negatex \<circ> sqprojection \<circ> ?F"])
+    apply(rule compact_interval convex_interval)+ unfolding interior_closed_interval
+    apply(rule 1 2 3)+ . note x=this
+  have "?F x \<noteq> 0" apply(rule x0) using x(1) by auto
+  hence *:"infnorm (sqprojection (?F x)) = 1" unfolding o_def by(rule lem2[rule_format])
+  have nx:"infnorm x = 1" apply(subst x(2)[THEN sym]) unfolding *[THEN sym] o_def by(rule lem1[rule_format])
+  have "\<forall>x i. x \<noteq> 0 \<longrightarrow> (0 < (sqprojection x)$i \<longleftrightarrow> 0 < x$i)"    "\<forall>x i. x \<noteq> 0 \<longrightarrow> ((sqprojection x)$i < 0 \<longleftrightarrow> x$i < 0)"
+    apply- apply(rule_tac[!] allI impI)+ proof- fix x::"real^2" and i::2 assume x:"x\<noteq>0"
+    have "inverse (infnorm x) > 0" using x[unfolded infnorm_pos_lt[THEN sym]] by auto
+    thus "(0 < sqprojection x $ i) = (0 < x $ i)"   "(sqprojection x $ i < 0) = (x $ i < 0)"
+      unfolding sqprojection_def vector_component_simps Cart_nth.scaleR real_scaleR_def
+      unfolding zero_less_mult_iff mult_less_0_iff by(auto simp add:field_simps) qed
+  note lem3 = this[rule_format]
+  have x1:"x $ 1 \<in> {- 1..1::real}" "x $ 2 \<in> {- 1..1::real}" using x(1) unfolding mem_interval by auto
+  hence nz:"f (x $ 1) - g (x $ 2) \<noteq> 0" unfolding right_minus_eq apply-apply(rule as) by auto
+  have "x $ 1 = -1 \<or> x $ 1 = 1 \<or> x $ 2 = -1 \<or> x $ 2 = 1" using nx unfolding infnorm_eq_1_2 by auto 
+  thus False proof- fix P Q R S 
+    presume "P \<or> Q \<or> R \<or> S" "P\<Longrightarrow>False" "Q\<Longrightarrow>False" "R\<Longrightarrow>False" "S\<Longrightarrow>False" thus False by auto
+  next assume as:"x$1 = 1"
+    hence *:"f (x $ 1) $ 1 = 1" using assms(6) by auto
+    have "sqprojection (f (x$1) - g (x$2)) $ 1 < 0"
+      using x(2)[unfolded o_def Cart_eq,THEN spec[where x=1]]
+      unfolding as negatex_def vector_2 by auto moreover
+    from x1 have "g (x $ 2) \<in> {- 1..1}" apply-apply(rule assms(2)[unfolded subset_eq,rule_format]) by auto
+    ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval 
+      apply(erule_tac x=1 in allE) by auto 
+  next assume as:"x$1 = -1"
+    hence *:"f (x $ 1) $ 1 = - 1" using assms(5) by auto
+    have "sqprojection (f (x$1) - g (x$2)) $ 1 > 0"
+      using x(2)[unfolded o_def Cart_eq,THEN spec[where x=1]]
+      unfolding as negatex_def vector_2 by auto moreover
+    from x1 have "g (x $ 2) \<in> {- 1..1}" apply-apply(rule assms(2)[unfolded subset_eq,rule_format]) by auto
+    ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval 
+      apply(erule_tac x=1 in allE) by auto
+  next assume as:"x$2 = 1"
+    hence *:"g (x $ 2) $ 2 = 1" using assms(8) by auto
+    have "sqprojection (f (x$1) - g (x$2)) $ 2 > 0"
+      using x(2)[unfolded o_def Cart_eq,THEN spec[where x=2]]
+      unfolding as negatex_def vector_2 by auto moreover
+    from x1 have "f (x $ 1) \<in> {- 1..1}" apply-apply(rule assms(1)[unfolded subset_eq,rule_format]) by auto
+    ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval 
+     apply(erule_tac x=2 in allE) by auto
+ next assume as:"x$2 = -1"
+    hence *:"g (x $ 2) $ 2 = - 1" using assms(7) by auto
+    have "sqprojection (f (x$1) - g (x$2)) $ 2 < 0"
+      using x(2)[unfolded o_def Cart_eq,THEN spec[where x=2]]
+      unfolding as negatex_def vector_2 by auto moreover
+    from x1 have "f (x $ 1) \<in> {- 1..1}" apply-apply(rule assms(1)[unfolded subset_eq,rule_format]) by auto
+    ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval 
+      apply(erule_tac x=2 in allE) by auto qed(auto) qed
+
+lemma fashoda_unit_path: fixes f ::"real \<Rightarrow> real^2" and g ::"real \<Rightarrow> real^2"
+  assumes "path f" "path g" "path_image f \<subseteq> {- 1..1}" "path_image g \<subseteq> {- 1..1}"
+  "(pathstart f)$1 = -1" "(pathfinish f)$1 = 1"  "(pathstart g)$2 = -1" "(pathfinish g)$2 = 1"
+  obtains z where "z \<in> path_image f" "z \<in> path_image g" proof-
+  note assms=assms[unfolded path_def pathstart_def pathfinish_def path_image_def]
+  def iscale \<equiv> "\<lambda>z::real. inverse 2 *\<^sub>R (z + 1)"
+  have isc:"iscale ` {- 1..1} \<subseteq> {0..1}" unfolding iscale_def by(auto)
+  have "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. (f \<circ> iscale) s = (g \<circ> iscale) t" proof(rule fashoda_unit) 
+    show "(f \<circ> iscale) ` {- 1..1} \<subseteq> {- 1..1}" "(g \<circ> iscale) ` {- 1..1} \<subseteq> {- 1..1}"
+      using isc and assms(3-4) unfolding image_compose by auto
+    have *:"continuous_on {- 1..1} iscale" unfolding iscale_def by(rule continuous_on_intros)+
+    show "continuous_on {- 1..1} (f \<circ> iscale)" "continuous_on {- 1..1} (g \<circ> iscale)"
+      apply-apply(rule_tac[!] continuous_on_compose[OF *]) apply(rule_tac[!] continuous_on_subset[OF _ isc])
+      by(rule assms)+ have *:"(1 / 2) *\<^sub>R (1 + (1::real^1)) = 1" unfolding Cart_eq by auto
+    show "(f \<circ> iscale) (- 1) $ 1 = - 1" "(f \<circ> iscale) 1 $ 1 = 1" "(g \<circ> iscale) (- 1) $ 2 = -1" "(g \<circ> iscale) 1 $ 2 = 1"
+      unfolding o_def iscale_def using assms by(auto simp add:*) qed
+  then guess s .. from this(2) guess t .. note st=this
+  show thesis apply(rule_tac z="f (iscale s)" in that)
+    using st `s\<in>{- 1..1}` unfolding o_def path_image_def image_iff apply-
+    apply(rule_tac x="iscale s" in bexI) prefer 3 apply(rule_tac x="iscale t" in bexI)
+    using isc[unfolded subset_eq, rule_format] by auto qed
+
+lemma fashoda: fixes b::"real^2"
+  assumes "path f" "path g" "path_image f \<subseteq> {a..b}" "path_image g \<subseteq> {a..b}"
+  "(pathstart f)$1 = a$1" "(pathfinish f)$1 = b$1"
+  "(pathstart g)$2 = a$2" "(pathfinish g)$2 = b$2"
+  obtains z where "z \<in> path_image f" "z \<in> path_image g" proof-
+  fix P Q S presume "P \<or> Q \<or> S" "P \<Longrightarrow> thesis" "Q \<Longrightarrow> thesis" "S \<Longrightarrow> thesis" thus thesis by auto
+next have "{a..b} \<noteq> {}" using assms(3) using path_image_nonempty by auto
+  hence "a \<le> b" unfolding interval_eq_empty vector_le_def by(auto simp add: not_less)
+  thus "a$1 = b$1 \<or> a$2 = b$2 \<or> (a$1 < b$1 \<and> a$2 < b$2)" unfolding vector_le_def forall_2 by auto
+next assume as:"a$1 = b$1" have "\<exists>z\<in>path_image g. z$2 = (pathstart f)$2" apply(rule connected_ivt_component)
+    apply(rule connected_path_image assms)+apply(rule pathstart_in_path_image,rule pathfinish_in_path_image)
+    unfolding assms using assms(3)[unfolded path_image_def subset_eq,rule_format,of "f 0"]
+    unfolding pathstart_def by(auto simp add: vector_le_def) then guess z .. note z=this
+  have "z \<in> {a..b}" using z(1) assms(4) unfolding path_image_def by blast 
+  hence "z = f 0" unfolding Cart_eq forall_2 unfolding z(2) pathstart_def
+    using assms(3)[unfolded path_image_def subset_eq mem_interval,rule_format,of "f 0" 1]
+    unfolding mem_interval apply(erule_tac x=1 in allE) using as by auto
+  thus thesis apply-apply(rule that[OF _ z(1)]) unfolding path_image_def by auto
+next assume as:"a$2 = b$2" have "\<exists>z\<in>path_image f. z$1 = (pathstart g)$1" apply(rule connected_ivt_component)
+    apply(rule connected_path_image assms)+apply(rule pathstart_in_path_image,rule pathfinish_in_path_image)
+    unfolding assms using assms(4)[unfolded path_image_def subset_eq,rule_format,of "g 0"]
+    unfolding pathstart_def by(auto simp add: vector_le_def) then guess z .. note z=this
+  have "z \<in> {a..b}" using z(1) assms(3) unfolding path_image_def by blast 
+  hence "z = g 0" unfolding Cart_eq forall_2 unfolding z(2) pathstart_def
+    using assms(4)[unfolded path_image_def subset_eq mem_interval,rule_format,of "g 0" 2]
+    unfolding mem_interval apply(erule_tac x=2 in allE) using as by auto
+  thus thesis apply-apply(rule that[OF z(1)]) unfolding path_image_def by auto
+next assume as:"a $ 1 < b $ 1 \<and> a $ 2 < b $ 2"
+  have int_nem:"{- 1..1::real^2} \<noteq> {}" unfolding interval_eq_empty by auto
+  guess z apply(rule fashoda_unit_path[of "interval_bij (a,b) (- 1,1) \<circ> f" "interval_bij (a,b) (- 1,1) \<circ> g"]) 
+    unfolding path_def path_image_def pathstart_def pathfinish_def
+    apply(rule_tac[1-2] continuous_on_compose) apply(rule assms[unfolded path_def] continuous_on_interval_bij)+
+    unfolding subset_eq apply(rule_tac[1-2] ballI)
+  proof- fix x assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> f) ` {0..1}"
+    then guess y unfolding image_iff .. note y=this
+    show "x \<in> {- 1..1}" unfolding y o_def apply(rule in_interval_interval_bij)
+      using y(1) using assms(3)[unfolded path_image_def subset_eq] int_nem by auto
+  next fix x assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> g) ` {0..1}"
+    then guess y unfolding image_iff .. note y=this
+    show "x \<in> {- 1..1}" unfolding y o_def apply(rule in_interval_interval_bij)
+      using y(1) using assms(4)[unfolded path_image_def subset_eq] int_nem by auto
+  next show "(interval_bij (a, b) (- 1, 1) \<circ> f) 0 $ 1 = -1"
+      "(interval_bij (a, b) (- 1, 1) \<circ> f) 1 $ 1 = 1"
+      "(interval_bij (a, b) (- 1, 1) \<circ> g) 0 $ 2 = -1"
+      "(interval_bij (a, b) (- 1, 1) \<circ> g) 1 $ 2 = 1" unfolding interval_bij_def Cart_lambda_beta vector_component_simps o_def split_conv
+      unfolding assms[unfolded pathstart_def pathfinish_def] using as by auto qed note z=this
+  from z(1) guess zf unfolding image_iff .. note zf=this
+  from z(2) guess zg unfolding image_iff .. note zg=this
+  have *:"\<forall>i. (- 1) $ i < (1::real^2) $ i \<and> a $ i < b $ i" unfolding forall_2 using as by auto
+  show thesis apply(rule_tac z="interval_bij (- 1,1) (a,b) z" in that)
+    apply(subst zf) defer apply(subst zg) unfolding o_def interval_bij_bij[OF *] path_image_def
+    using zf(1) zg(1) by auto qed
+
+subsection {*Some slightly ad hoc lemmas I use below*}
+
+lemma segment_vertical: fixes a::"real^2" assumes "a$1 = b$1"
+  shows "x \<in> closed_segment a b \<longleftrightarrow> (x$1 = a$1 \<and> x$1 = b$1 \<and>
+           (a$2 \<le> x$2 \<and> x$2 \<le> b$2 \<or> b$2 \<le> x$2 \<and> x$2 \<le> a$2))" (is "_ = ?R")
+proof- 
+  let ?L = "\<exists>u. (x $ 1 = (1 - u) * a $ 1 + u * b $ 1 \<and> x $ 2 = (1 - u) * a $ 2 + u * b $ 2) \<and> 0 \<le> u \<and> u \<le> 1"
+  { presume "?L \<Longrightarrow> ?R" "?R \<Longrightarrow> ?L" thus ?thesis unfolding closed_segment_def mem_Collect_eq
+      unfolding Cart_eq forall_2 smult_conv_scaleR[THEN sym] vector_component_simps by blast }
+  { assume ?L then guess u apply-apply(erule exE)apply(erule conjE)+ . note u=this
+    { fix b a assume "b + u * a > a + u * b"
+      hence "(1 - u) * b > (1 - u) * a" by(auto simp add:field_simps)
+      hence "b \<ge> a" apply(drule_tac mult_less_imp_less_left) using u by auto
+      hence "u * a \<le> u * b" apply-apply(rule mult_left_mono[OF _ u(3)]) 
+        using u(3-4) by(auto simp add:field_simps) } note * = this
+    { fix a b assume "u * b > u * a" hence "(1 - u) * a \<le> (1 - u) * b" apply-apply(rule mult_left_mono)
+        apply(drule mult_less_imp_less_left) using u by auto
+      hence "a + u * b \<le> b + u * a" by(auto simp add:field_simps) } note ** = this
+    thus ?R unfolding u assms using u by(auto simp add:field_simps not_le intro:* **) }
+  { assume ?R thus ?L proof(cases "x$2 = b$2")
+      case True thus ?L apply(rule_tac x="(x$2 - a$2) / (b$2 - a$2)" in exI) unfolding assms True
+        using `?R` by(auto simp add:field_simps)
+    next case False thus ?L apply(rule_tac x="1 - (x$2 - b$2) / (a$2 - b$2)" in exI) unfolding assms using `?R`
+        by(auto simp add:field_simps)
+    qed } qed
+
+lemma segment_horizontal: fixes a::"real^2" assumes "a$2 = b$2"
+  shows "x \<in> closed_segment a b \<longleftrightarrow> (x$2 = a$2 \<and> x$2 = b$2 \<and>
+           (a$1 \<le> x$1 \<and> x$1 \<le> b$1 \<or> b$1 \<le> x$1 \<and> x$1 \<le> a$1))" (is "_ = ?R")
+proof- 
+  let ?L = "\<exists>u. (x $ 1 = (1 - u) * a $ 1 + u * b $ 1 \<and> x $ 2 = (1 - u) * a $ 2 + u * b $ 2) \<and> 0 \<le> u \<and> u \<le> 1"
+  { presume "?L \<Longrightarrow> ?R" "?R \<Longrightarrow> ?L" thus ?thesis unfolding closed_segment_def mem_Collect_eq
+      unfolding Cart_eq forall_2 smult_conv_scaleR[THEN sym] vector_component_simps by blast }
+  { assume ?L then guess u apply-apply(erule exE)apply(erule conjE)+ . note u=this
+    { fix b a assume "b + u * a > a + u * b"
+      hence "(1 - u) * b > (1 - u) * a" by(auto simp add:field_simps)
+      hence "b \<ge> a" apply(drule_tac mult_less_imp_less_left) using u by auto
+      hence "u * a \<le> u * b" apply-apply(rule mult_left_mono[OF _ u(3)]) 
+        using u(3-4) by(auto simp add:field_simps) } note * = this
+    { fix a b assume "u * b > u * a" hence "(1 - u) * a \<le> (1 - u) * b" apply-apply(rule mult_left_mono)
+        apply(drule mult_less_imp_less_left) using u by auto
+      hence "a + u * b \<le> b + u * a" by(auto simp add:field_simps) } note ** = this
+    thus ?R unfolding u assms using u by(auto simp add:field_simps not_le intro:* **) }
+  { assume ?R thus ?L proof(cases "x$1 = b$1")
+      case True thus ?L apply(rule_tac x="(x$1 - a$1) / (b$1 - a$1)" in exI) unfolding assms True
+        using `?R` by(auto simp add:field_simps)
+    next case False thus ?L apply(rule_tac x="1 - (x$1 - b$1) / (a$1 - b$1)" in exI) unfolding assms using `?R`
+        by(auto simp add:field_simps)
+    qed } qed
+
+subsection {*useful Fashoda corollary pointed out to me by Tom Hales. *}
+
+lemma fashoda_interlace: fixes a::"real^2"
+  assumes "path f" "path g"
+  "path_image f \<subseteq> {a..b}" "path_image g \<subseteq> {a..b}"
+  "(pathstart f)$2 = a$2" "(pathfinish f)$2 = a$2"
+  "(pathstart g)$2 = a$2" "(pathfinish g)$2 = a$2"
+  "(pathstart f)$1 < (pathstart g)$1" "(pathstart g)$1 < (pathfinish f)$1"
+  "(pathfinish f)$1 < (pathfinish g)$1"
+  obtains z where "z \<in> path_image f" "z \<in> path_image g"
+proof-
+  have "{a..b} \<noteq> {}" using path_image_nonempty using assms(3) by auto
+  note ab=this[unfolded interval_eq_empty not_ex forall_2 not_less]
+  have "pathstart f \<in> {a..b}" "pathfinish f \<in> {a..b}" "pathstart g \<in> {a..b}" "pathfinish g \<in> {a..b}"
+    using pathstart_in_path_image pathfinish_in_path_image using assms(3-4) by auto
+  note startfin = this[unfolded mem_interval forall_2]
+  let ?P1 = "linepath (vector[a$1 - 2, a$2 - 2]) (vector[(pathstart f)$1,a$2 - 2]) +++
+     linepath(vector[(pathstart f)$1,a$2 - 2])(pathstart f) +++ f +++
+     linepath(pathfinish f)(vector[(pathfinish f)$1,a$2 - 2]) +++
+     linepath(vector[(pathfinish f)$1,a$2 - 2])(vector[b$1 + 2,a$2 - 2])" 
+  let ?P2 = "linepath(vector[(pathstart g)$1, (pathstart g)$2 - 3])(pathstart g) +++ g +++
+     linepath(pathfinish g)(vector[(pathfinish g)$1,a$2 - 1]) +++
+     linepath(vector[(pathfinish g)$1,a$2 - 1])(vector[b$1 + 1,a$2 - 1]) +++
+     linepath(vector[b$1 + 1,a$2 - 1])(vector[b$1 + 1,b$2 + 3])"
+  let ?a = "vector[a$1 - 2, a$2 - 3]"
+  let ?b = "vector[b$1 + 2, b$2 + 3]"
+  have P1P2:"path_image ?P1 = path_image (linepath (vector[a$1 - 2, a$2 - 2]) (vector[(pathstart f)$1,a$2 - 2])) \<union>
+      path_image (linepath(vector[(pathstart f)$1,a$2 - 2])(pathstart f)) \<union> path_image f \<union>
+      path_image (linepath(pathfinish f)(vector[(pathfinish f)$1,a$2 - 2])) \<union>
+      path_image (linepath(vector[(pathfinish f)$1,a$2 - 2])(vector[b$1 + 2,a$2 - 2]))"
+    "path_image ?P2 = path_image(linepath(vector[(pathstart g)$1, (pathstart g)$2 - 3])(pathstart g)) \<union> path_image g \<union>
+      path_image(linepath(pathfinish g)(vector[(pathfinish g)$1,a$2 - 1])) \<union>
+      path_image(linepath(vector[(pathfinish g)$1,a$2 - 1])(vector[b$1 + 1,a$2 - 1])) \<union>
+      path_image(linepath(vector[b$1 + 1,a$2 - 1])(vector[b$1 + 1,b$2 + 3]))" using assms(1-2)
+      by(auto simp add: path_image_join path_linepath)
+  have abab: "{a..b} \<subseteq> {?a..?b}" by(auto simp add:vector_le_def forall_2 vector_2)
+  guess z apply(rule fashoda[of ?P1 ?P2 ?a ?b])
+    unfolding pathstart_join pathfinish_join pathstart_linepath pathfinish_linepath vector_2 proof-
+    show "path ?P1" "path ?P2" using assms by auto
+    have "path_image ?P1 \<subseteq> {?a .. ?b}" unfolding P1P2 path_image_linepath apply(rule Un_least)+ defer 3
+      apply(rule_tac[1-4] convex_interval(1)[unfolded convex_contains_segment,rule_format])
+      unfolding mem_interval forall_2 vector_2 using ab startfin abab assms(3)
+      using assms(9-) unfolding assms by(auto simp add:field_simps)
+    thus "path_image ?P1  \<subseteq> {?a .. ?b}" .
+    have "path_image ?P2 \<subseteq> {?a .. ?b}" unfolding P1P2 path_image_linepath apply(rule Un_least)+ defer 2
+      apply(rule_tac[1-4] convex_interval(1)[unfolded convex_contains_segment,rule_format])
+      unfolding mem_interval forall_2 vector_2 using ab startfin abab assms(4)
+      using assms(9-) unfolding assms  by(auto simp add:field_simps)
+    thus "path_image ?P2  \<subseteq> {?a .. ?b}" . 
+    show "a $ 1 - 2 = a $ 1 - 2"  "b $ 1 + 2 = b $ 1 + 2" "pathstart g $ 2 - 3 = a $ 2 - 3"  "b $ 2 + 3 = b $ 2 + 3"
+      by(auto simp add: assms)
+  qed note z=this[unfolded P1P2 path_image_linepath]
+  show thesis apply(rule that[of z]) proof-
+    have "(z \<in> closed_segment (vector [a $ 1 - 2, a $ 2 - 2]) (vector [pathstart f $ 1, a $ 2 - 2]) \<or>
+     z \<in> closed_segment (vector [pathstart f $ 1, a $ 2 - 2]) (pathstart f)) \<or>
+   z \<in> closed_segment (pathfinish f) (vector [pathfinish f $ 1, a $ 2 - 2]) \<or>
+  z \<in> closed_segment (vector [pathfinish f $ 1, a $ 2 - 2]) (vector [b $ 1 + 2, a $ 2 - 2]) \<Longrightarrow>
+  (((z \<in> closed_segment (vector [pathstart g $ 1, pathstart g $ 2 - 3]) (pathstart g)) \<or>
+    z \<in> closed_segment (pathfinish g) (vector [pathfinish g $ 1, a $ 2 - 1])) \<or>
+   z \<in> closed_segment (vector [pathfinish g $ 1, a $ 2 - 1]) (vector [b $ 1 + 1, a $ 2 - 1])) \<or>
+  z \<in> closed_segment (vector [b $ 1 + 1, a $ 2 - 1]) (vector [b $ 1 + 1, b $ 2 + 3]) \<Longrightarrow> False"
+      apply(simp only: segment_vertical segment_horizontal vector_2) proof- case goal1 note as=this
+      have "pathfinish f \<in> {a..b}" using assms(3) pathfinish_in_path_image[of f] by auto 
+      hence "1 + b $ 1 \<le> pathfinish f $ 1 \<Longrightarrow> False" unfolding mem_interval forall_2 by auto
+      hence "z$1 \<noteq> pathfinish f$1" using as(2) using assms ab by(auto simp add:field_simps)
+      moreover have "pathstart f \<in> {a..b}" using assms(3) pathstart_in_path_image[of f] by auto 
+      hence "1 + b $ 1 \<le> pathstart f $ 1 \<Longrightarrow> False" unfolding mem_interval forall_2 by auto
+      hence "z$1 \<noteq> pathstart f$1" using as(2) using assms ab by(auto simp add:field_simps)
+      ultimately have *:"z$2 = a$2 - 2" using goal1(1) by auto
+      have "z$1 \<noteq> pathfinish g$1" using as(2) using assms ab by(auto simp add:field_simps *)
+      moreover have "pathstart g \<in> {a..b}" using assms(4) pathstart_in_path_image[of g] by auto 
+      note this[unfolded mem_interval forall_2]
+      hence "z$1 \<noteq> pathstart g$1" using as(1) using assms ab by(auto simp add:field_simps *)
+      ultimately have "a $ 2 - 1 \<le> z $ 2 \<and> z $ 2 \<le> b $ 2 + 3 \<or> b $ 2 + 3 \<le> z $ 2 \<and> z $ 2 \<le> a $ 2 - 1"
+        using as(2) unfolding * assms by(auto simp add:field_simps)
+      thus False unfolding * using ab by auto
+    qed hence "z \<in> path_image f \<or> z \<in> path_image g" using z unfolding Un_iff by blast
+    hence z':"z\<in>{a..b}" using assms(3-4) by auto
+    have "a $ 2 = z $ 2 \<Longrightarrow> (z $ 1 = pathstart f $ 1 \<or> z $ 1 = pathfinish f $ 1) \<Longrightarrow> (z = pathstart f \<or> z = pathfinish f)"
+      unfolding Cart_eq forall_2 assms by auto
+    with z' show "z\<in>path_image f" using z(1) unfolding Un_iff mem_interval forall_2 apply-
+      apply(simp only: segment_vertical segment_horizontal vector_2) unfolding assms by auto
+    have "a $ 2 = z $ 2 \<Longrightarrow> (z $ 1 = pathstart g $ 1 \<or> z $ 1 = pathfinish g $ 1) \<Longrightarrow> (z = pathstart g \<or> z = pathfinish g)"
+      unfolding Cart_eq forall_2 assms by auto
+    with z' show "z\<in>path_image g" using z(2) unfolding Un_iff mem_interval forall_2 apply-
+      apply(simp only: segment_vertical segment_horizontal vector_2) unfolding assms by auto
+  qed qed
+
+(** The Following still needs to be translated. Maybe I will do that later.
+
+(* ------------------------------------------------------------------------- *)
+(* Complement in dimension N >= 2 of set homeomorphic to any interval in     *)
+(* any dimension is (path-)connected. This naively generalizes the argument  *)
+(* in Ryuji Maehara's paper "The Jordan curve theorem via the Brouwer        *)
+(* fixed point theorem", American Mathematical Monthly 1984.                 *)
+(* ------------------------------------------------------------------------- *)
+
+let RETRACTION_INJECTIVE_IMAGE_INTERVAL = prove
+ (`!p:real^M->real^N a b.
+        ~(interval[a,b] = {}) /\
+        p continuous_on interval[a,b] /\
+        (!x y. x IN interval[a,b] /\ y IN interval[a,b] /\ p x = p y ==> x = y)
+        ==> ?f. f continuous_on (:real^N) /\
+                IMAGE f (:real^N) SUBSET (IMAGE p (interval[a,b])) /\
+                (!x. x IN (IMAGE p (interval[a,b])) ==> f x = x)`,
+  REPEAT STRIP_TAC THEN
+  FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [INJECTIVE_ON_LEFT_INVERSE]) THEN
+  DISCH_THEN(X_CHOOSE_TAC `q:real^N->real^M`) THEN
+  SUBGOAL_THEN `(q:real^N->real^M) continuous_on
+                (IMAGE p (interval[a:real^M,b]))`
+  ASSUME_TAC THENL
+   [MATCH_MP_TAC CONTINUOUS_ON_INVERSE THEN ASM_REWRITE_TAC[COMPACT_INTERVAL];
+    ALL_TAC] THEN
+  MP_TAC(ISPECL [`q:real^N->real^M`;
+                 `IMAGE (p:real^M->real^N)
+                 (interval[a,b])`;
+                 `a:real^M`; `b:real^M`]
+        TIETZE_CLOSED_INTERVAL) THEN
+  ASM_SIMP_TAC[COMPACT_INTERVAL; COMPACT_CONTINUOUS_IMAGE;
+               COMPACT_IMP_CLOSED] THEN
+  ANTS_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
+  DISCH_THEN(X_CHOOSE_THEN `r:real^N->real^M` STRIP_ASSUME_TAC) THEN
+  EXISTS_TAC `(p:real^M->real^N) o (r:real^N->real^M)` THEN
+  REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; o_THM; IN_UNIV] THEN
+  CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
+  MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN ASM_REWRITE_TAC[] THEN
+  FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP(REWRITE_RULE[IMP_CONJ]
+        CONTINUOUS_ON_SUBSET)) THEN ASM SET_TAC[]);;
+
+let UNBOUNDED_PATH_COMPONENTS_COMPLEMENT_HOMEOMORPHIC_INTERVAL = prove
+ (`!s:real^N->bool a b:real^M.
+        s homeomorphic (interval[a,b])
+        ==> !x. ~(x IN s) ==> ~bounded(path_component((:real^N) DIFF s) x)`,
+  REPEAT GEN_TAC THEN REWRITE_TAC[homeomorphic; homeomorphism] THEN
+  REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
+  MAP_EVERY X_GEN_TAC [`p':real^N->real^M`; `p:real^M->real^N`] THEN
+  DISCH_TAC THEN
+  SUBGOAL_THEN
+   `!x y. x IN interval[a,b] /\ y IN interval[a,b] /\
+          (p:real^M->real^N) x = p y ==> x = y`
+  ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
+  FIRST_X_ASSUM(MP_TAC o funpow 4 CONJUNCT2) THEN
+  DISCH_THEN(CONJUNCTS_THEN2 (SUBST1_TAC o SYM) ASSUME_TAC) THEN
+  ASM_CASES_TAC `interval[a:real^M,b] = {}` THEN
+  ASM_REWRITE_TAC[IMAGE_CLAUSES; DIFF_EMPTY; PATH_COMPONENT_UNIV;
+                  NOT_BOUNDED_UNIV] THEN
+  ABBREV_TAC `s = (:real^N) DIFF (IMAGE p (interval[a:real^M,b]))` THEN
+  X_GEN_TAC `c:real^N` THEN REPEAT STRIP_TAC THEN
+  SUBGOAL_THEN `(c:real^N) IN s` ASSUME_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
+  SUBGOAL_THEN `bounded((path_component s c) UNION
+                        (IMAGE (p:real^M->real^N) (interval[a,b])))`
+  MP_TAC THENL
+   [ASM_SIMP_TAC[BOUNDED_UNION; COMPACT_IMP_BOUNDED; COMPACT_IMP_BOUNDED;
+                 COMPACT_CONTINUOUS_IMAGE; COMPACT_INTERVAL];
+    ALL_TAC] THEN
+  DISCH_THEN(MP_TAC o SPEC `c:real^N` o MATCH_MP BOUNDED_SUBSET_BALL) THEN
+  REWRITE_TAC[UNION_SUBSET] THEN
+  DISCH_THEN(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC) THEN
+  MP_TAC(ISPECL [`p:real^M->real^N`; `a:real^M`; `b:real^M`]
+    RETRACTION_INJECTIVE_IMAGE_INTERVAL) THEN
+  ASM_REWRITE_TAC[SUBSET; IN_UNIV] THEN
+  DISCH_THEN(X_CHOOSE_THEN `r:real^N->real^N` MP_TAC) THEN
+  DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC
+   (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC)) THEN
+  REWRITE_TAC[FORALL_IN_IMAGE; IN_UNIV] THEN DISCH_TAC THEN
+  ABBREV_TAC `q = \z:real^N. if z IN path_component s c then r(z) else z` THEN
+  SUBGOAL_THEN
+    `(q:real^N->real^N) continuous_on
+     (closure(path_component s c) UNION ((:real^N) DIFF (path_component s c)))`
+  MP_TAC THENL
+   [EXPAND_TAC "q" THEN MATCH_MP_TAC CONTINUOUS_ON_CASES THEN
+    REWRITE_TAC[CLOSED_CLOSURE; CONTINUOUS_ON_ID; GSYM OPEN_CLOSED] THEN
+    REPEAT CONJ_TAC THENL
+     [MATCH_MP_TAC OPEN_PATH_COMPONENT THEN EXPAND_TAC "s" THEN
+      ASM_SIMP_TAC[GSYM CLOSED_OPEN; COMPACT_IMP_CLOSED;
+                   COMPACT_CONTINUOUS_IMAGE; COMPACT_INTERVAL];
+      ASM_MESON_TAC[CONTINUOUS_ON_SUBSET; SUBSET_UNIV];
+      ALL_TAC] THEN
+    X_GEN_TAC `z:real^N` THEN
+    REWRITE_TAC[SET_RULE `~(z IN (s DIFF t) /\ z IN t)`] THEN
+    STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
+    MP_TAC(ISPECL
+     [`path_component s (z:real^N)`; `path_component s (c:real^N)`]
+     OPEN_INTER_CLOSURE_EQ_EMPTY) THEN
+    ASM_REWRITE_TAC[GSYM DISJOINT; PATH_COMPONENT_DISJOINT] THEN ANTS_TAC THENL
+     [MATCH_MP_TAC OPEN_PATH_COMPONENT THEN EXPAND_TAC "s" THEN
+      ASM_SIMP_TAC[GSYM CLOSED_OPEN; COMPACT_IMP_CLOSED;
+                   COMPACT_CONTINUOUS_IMAGE; COMPACT_INTERVAL];
+      REWRITE_TAC[DISJOINT; EXTENSION; IN_INTER; NOT_IN_EMPTY] THEN
+      DISCH_THEN(MP_TAC o SPEC `z:real^N`) THEN ASM_REWRITE_TAC[] THEN
+      GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [IN] THEN
+      REWRITE_TAC[PATH_COMPONENT_REFL_EQ] THEN ASM SET_TAC[]];
+    ALL_TAC] THEN
+  SUBGOAL_THEN
+   `closure(path_component s c) UNION ((:real^N) DIFF (path_component s c)) =
+    (:real^N)`
+  SUBST1_TAC THENL
+   [MATCH_MP_TAC(SET_RULE `s SUBSET t ==> t UNION (UNIV DIFF s) = UNIV`) THEN
+    REWRITE_TAC[CLOSURE_SUBSET];
+    DISCH_TAC] THEN
+  MP_TAC(ISPECL
+   [`(\x. &2 % c - x) o
+     (\x. c + B / norm(x - c) % (x - c)) o (q:real^N->real^N)`;
+    `cball(c:real^N,B)`]
+    BROUWER) THEN
+  REWRITE_TAC[NOT_IMP; GSYM CONJ_ASSOC; COMPACT_CBALL; CONVEX_CBALL] THEN
+  ASM_SIMP_TAC[CBALL_EQ_EMPTY; REAL_LT_IMP_LE; REAL_NOT_LT] THEN
+  SUBGOAL_THEN `!x. ~((q:real^N->real^N) x = c)` ASSUME_TAC THENL
+   [X_GEN_TAC `x:real^N` THEN EXPAND_TAC "q" THEN
+    REWRITE_TAC[NORM_EQ_0; VECTOR_SUB_EQ] THEN COND_CASES_TAC THEN
+    ASM SET_TAC[PATH_COMPONENT_REFL_EQ];
+    ALL_TAC] THEN
+  REPEAT CONJ_TAC THENL
+   [MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
+    SIMP_TAC[CONTINUOUS_ON_SUB; CONTINUOUS_ON_ID; CONTINUOUS_ON_CONST] THEN
+    MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN CONJ_TAC THENL
+     [ASM_MESON_TAC[CONTINUOUS_ON_SUBSET; SUBSET_UNIV]; ALL_TAC] THEN
+    MATCH_MP_TAC CONTINUOUS_ON_ADD THEN REWRITE_TAC[CONTINUOUS_ON_CONST] THEN
+    MATCH_MP_TAC CONTINUOUS_ON_MUL THEN
+    SIMP_TAC[CONTINUOUS_ON_SUB; CONTINUOUS_ON_ID; CONTINUOUS_ON_CONST] THEN
+    REWRITE_TAC[o_DEF; real_div; LIFT_CMUL] THEN
+    MATCH_MP_TAC CONTINUOUS_ON_CMUL THEN
+    MATCH_MP_TAC(REWRITE_RULE[o_DEF] CONTINUOUS_ON_INV) THEN
+    ASM_REWRITE_TAC[FORALL_IN_IMAGE; NORM_EQ_0; VECTOR_SUB_EQ] THEN
+    SUBGOAL_THEN
+     `(\x:real^N. lift(norm(x - c))) = (lift o norm) o (\x. x - c)`
+    SUBST1_TAC THENL [REWRITE_TAC[o_DEF]; ALL_TAC] THEN
+    MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
+    ASM_SIMP_TAC[CONTINUOUS_ON_SUB; CONTINUOUS_ON_ID; CONTINUOUS_ON_CONST;
+                 CONTINUOUS_ON_LIFT_NORM];
+    REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_CBALL; o_THM; dist] THEN
+    X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
+    REWRITE_TAC[VECTOR_ARITH `c - (&2 % c - (c + x)) = x`] THEN
+    REWRITE_TAC[NORM_MUL; REAL_ABS_DIV; REAL_ABS_NORM] THEN
+    ASM_SIMP_TAC[REAL_DIV_RMUL; NORM_EQ_0; VECTOR_SUB_EQ] THEN
+    ASM_REAL_ARITH_TAC;
+    REWRITE_TAC[NOT_EXISTS_THM; TAUT `~(c /\ b) <=> c ==> ~b`] THEN
+    REWRITE_TAC[IN_CBALL; o_THM; dist] THEN
+    X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
+    REWRITE_TAC[VECTOR_ARITH `&2 % c - (c + x') = x <=> --x' = x - c`] THEN
+    ASM_CASES_TAC `(x:real^N) IN path_component s c` THENL
+     [MATCH_MP_TAC(NORM_ARITH `norm(y) < B /\ norm(x) = B ==> ~(--x = y)`) THEN
+      REWRITE_TAC[NORM_MUL; REAL_ABS_DIV; REAL_ABS_NORM] THEN
+      ASM_SIMP_TAC[REAL_DIV_RMUL; NORM_EQ_0; VECTOR_SUB_EQ] THEN
+      ASM_SIMP_TAC[REAL_ARITH `&0 < B ==> abs B = B`] THEN
+      UNDISCH_TAC `path_component s c SUBSET ball(c:real^N,B)` THEN
+      REWRITE_TAC[SUBSET; IN_BALL] THEN ASM_MESON_TAC[dist; NORM_SUB];
+      EXPAND_TAC "q" THEN REWRITE_TAC[] THEN ASM_REWRITE_TAC[] THEN
+      REWRITE_TAC[VECTOR_ARITH `--(c % x) = x <=> (&1 + c) % x = vec 0`] THEN
+      ASM_REWRITE_TAC[DE_MORGAN_THM; VECTOR_SUB_EQ; VECTOR_MUL_EQ_0] THEN
+      SUBGOAL_THEN `~(x:real^N = c)` ASSUME_TAC THENL
+       [ASM_MESON_TAC[PATH_COMPONENT_REFL; IN]; ALL_TAC] THEN
+      ASM_REWRITE_TAC[] THEN
+      MATCH_MP_TAC(REAL_ARITH `&0 < x ==> ~(&1 + x = &0)`) THEN
+      ASM_SIMP_TAC[REAL_LT_DIV; NORM_POS_LT; VECTOR_SUB_EQ]]]);;
+
+let PATH_CONNECTED_COMPLEMENT_HOMEOMORPHIC_INTERVAL = prove
+ (`!s:real^N->bool a b:real^M.
+        2 <= dimindex(:N) /\ s homeomorphic interval[a,b]
+        ==> path_connected((:real^N) DIFF s)`,
+  REPEAT STRIP_TAC THEN REWRITE_TAC[PATH_CONNECTED_IFF_PATH_COMPONENT] THEN
+  FIRST_ASSUM(MP_TAC o MATCH_MP
+    UNBOUNDED_PATH_COMPONENTS_COMPLEMENT_HOMEOMORPHIC_INTERVAL) THEN
+  ASM_REWRITE_TAC[SET_RULE `~(x IN s) <=> x IN (UNIV DIFF s)`] THEN
+  ABBREV_TAC `t = (:real^N) DIFF s` THEN
+  DISCH_TAC THEN MAP_EVERY X_GEN_TAC [`x:real^N`; `y:real^N`] THEN
+  STRIP_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP HOMEOMORPHIC_COMPACTNESS) THEN
+  REWRITE_TAC[COMPACT_INTERVAL] THEN
+  DISCH_THEN(MP_TAC o MATCH_MP COMPACT_IMP_BOUNDED) THEN
+  REWRITE_TAC[BOUNDED_POS; LEFT_IMP_EXISTS_THM] THEN
+  X_GEN_TAC `B:real` THEN STRIP_TAC THEN
+  SUBGOAL_THEN `(?u:real^N. u IN path_component t x /\ B < norm(u)) /\
+                (?v:real^N. v IN path_component t y /\ B < norm(v))`
+  STRIP_ASSUME_TAC THENL
+   [ASM_MESON_TAC[BOUNDED_POS; REAL_NOT_LE]; ALL_TAC] THEN
+  MATCH_MP_TAC PATH_COMPONENT_TRANS THEN EXISTS_TAC `u:real^N` THEN
+  CONJ_TAC THENL [ASM_MESON_TAC[IN]; ALL_TAC] THEN
+  MATCH_MP_TAC PATH_COMPONENT_SYM THEN
+  MATCH_MP_TAC PATH_COMPONENT_TRANS THEN EXISTS_TAC `v:real^N` THEN
+  CONJ_TAC THENL [ASM_MESON_TAC[IN]; ALL_TAC] THEN
+  MATCH_MP_TAC PATH_COMPONENT_OF_SUBSET THEN
+  EXISTS_TAC `(:real^N) DIFF cball(vec 0,B)` THEN CONJ_TAC THENL
+   [EXPAND_TAC "t" THEN MATCH_MP_TAC(SET_RULE
+     `s SUBSET t ==> (u DIFF t) SUBSET (u DIFF s)`) THEN
+    ASM_REWRITE_TAC[SUBSET; IN_CBALL_0];
+    MP_TAC(ISPEC `cball(vec 0:real^N,B)`
+       PATH_CONNECTED_COMPLEMENT_BOUNDED_CONVEX) THEN
+    ASM_REWRITE_TAC[BOUNDED_CBALL; CONVEX_CBALL] THEN
+    REWRITE_TAC[PATH_CONNECTED_IFF_PATH_COMPONENT] THEN
+    DISCH_THEN MATCH_MP_TAC THEN
+    ASM_REWRITE_TAC[IN_DIFF; IN_UNIV; IN_CBALL_0; REAL_NOT_LE]]);;
+
+(* ------------------------------------------------------------------------- *)
+(* In particular, apply all these to the special case of an arc.             *)
+(* ------------------------------------------------------------------------- *)
+
+let RETRACTION_ARC = prove
+ (`!p. arc p
+       ==> ?f. f continuous_on (:real^N) /\
+               IMAGE f (:real^N) SUBSET path_image p /\
+               (!x. x IN path_image p ==> f x = x)`,
+  REWRITE_TAC[arc; path; path_image] THEN REPEAT STRIP_TAC THEN
+  MATCH_MP_TAC RETRACTION_INJECTIVE_IMAGE_INTERVAL THEN
+  ASM_REWRITE_TAC[INTERVAL_EQ_EMPTY_1; DROP_VEC; REAL_NOT_LT; REAL_POS]);;
+
+let PATH_CONNECTED_ARC_COMPLEMENT = prove
+ (`!p. 2 <= dimindex(:N) /\ arc p
+       ==> path_connected((:real^N) DIFF path_image p)`,
+  REWRITE_TAC[arc; path] THEN REPEAT STRIP_TAC THEN SIMP_TAC[path_image] THEN
+  MP_TAC(ISPECL [`path_image p:real^N->bool`; `vec 0:real^1`; `vec 1:real^1`]
+    PATH_CONNECTED_COMPLEMENT_HOMEOMORPHIC_INTERVAL) THEN
+  ASM_REWRITE_TAC[path_image] THEN DISCH_THEN MATCH_MP_TAC THEN
+  ONCE_REWRITE_TAC[HOMEOMORPHIC_SYM] THEN
+  MATCH_MP_TAC HOMEOMORPHIC_COMPACT THEN
+  EXISTS_TAC `p:real^1->real^N` THEN ASM_REWRITE_TAC[COMPACT_INTERVAL]);;
+
+let CONNECTED_ARC_COMPLEMENT = prove
+ (`!p. 2 <= dimindex(:N) /\ arc p
+       ==> connected((:real^N) DIFF path_image p)`,
+  SIMP_TAC[PATH_CONNECTED_ARC_COMPLEMENT; PATH_CONNECTED_IMP_CONNECTED]);; *)
+
+end
diff -r cc8db7295249 -r 027879c5637d src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy
--- a/src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy	Tue Apr 27 16:24:57 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy	Tue Apr 27 11:17:50 2010 -0700
@@ -1,5 +1,5 @@
 theory Multivariate_Analysis
-imports Determinants Integration Real_Integration
+imports Determinants Integration Real_Integration Fashoda
 begin
 
 end
diff -r cc8db7295249 -r 027879c5637d src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Apr 27 16:24:57 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Apr 27 11:17:50 2010 -0700
@@ -250,8 +250,6 @@
 lemma ball_min_Int: "ball a (min r s) = ball a r \<inter> ball a s"
   by (simp add: expand_set_eq)
 
-subsection{* Topological properties of open balls *}
-
 lemma diff_less_iff: "(a::real) - b > 0 \<longleftrightarrow> a > b"
   "(a::real) - b < 0 \<longleftrightarrow> a < b"
   "a - b < c \<longleftrightarrow> a < c +b" "a - b > c \<longleftrightarrow> a > c +b" by arith+
@@ -965,7 +963,9 @@
   using frontier_complement frontier_subset_eq[of "- S"]
   unfolding open_closed by auto
 
-subsection{* Common nets and The "within" modifier for nets. *}
+subsection {* Nets and the ``eventually true'' quantifier *}
+
+text {* Common nets and The "within" modifier for nets. *}
 
 definition
   at_infinity :: "'a::real_normed_vector net" where
@@ -989,7 +989,7 @@
   then show "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x \<and> Q x" ..
 qed auto
 
-subsection{* Identify Trivial limits, where we can't approach arbitrarily closely. *}
+text {* Identify Trivial limits, where we can't approach arbitrarily closely. *}
 
 definition
   trivial_limit :: "'a net \<Rightarrow> bool" where
@@ -1040,7 +1040,7 @@
 lemma trivial_limit_sequentially[intro]: "\<not> trivial_limit sequentially"
   by (auto simp add: trivial_limit_def eventually_sequentially)
 
-subsection{* Some property holds "sufficiently close" to the limit point. *}
+text {* Some property holds "sufficiently close" to the limit point. *}
 
 lemma eventually_at: (* FIXME: this replaces Limits.eventually_at *)
   "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
@@ -1096,7 +1096,7 @@
 lemma not_eventually: "(\<forall>x. \<not> P x ) \<Longrightarrow> ~(trivial_limit net) ==> ~(eventually (\<lambda>x. P x) net)"
   by (simp add: eventually_False)
 
-subsection{* Limits, defined as vacuously true when the limit is trivial. *}
+subsection {* Limits *}
 
   text{* Notation Lim to avoid collition with lim defined in analysis *}
 definition
@@ -1266,6 +1266,23 @@
   shows "(f ---> l) net \<Longrightarrow> (g ---> m) net \<Longrightarrow> ((\<lambda>x. f(x) - g(x)) ---> l - m) net"
   by (rule tendsto_diff)
 
+lemma Lim_mul:
+  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
+  assumes "(c ---> d) net"  "(f ---> l) net"
+  shows "((\<lambda>x. c(x) *\<^sub>R f x) ---> (d *\<^sub>R l)) net"
+  using assms by (rule scaleR.tendsto)
+
+lemma Lim_inv:
+  fixes f :: "'a \<Rightarrow> real"
+  assumes "(f ---> l) (net::'a net)"  "l \<noteq> 0"
+  shows "((inverse o f) ---> inverse l) net"
+  unfolding o_def using assms by (rule tendsto_inverse)
+
+lemma Lim_vmul:
+  fixes c :: "'a \<Rightarrow> real" and v :: "'b::real_normed_vector"
+  shows "(c ---> d) net ==> ((\<lambda>x. c(x) *\<^sub>R v) ---> d *\<^sub>R v) net"
+  by (intro tendsto_intros)
+
 lemma Lim_null:
   fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
   shows "(f ---> l) net \<longleftrightarrow> ((\<lambda>x. f(x) - l) ---> 0) net" by (simp add: Lim dist_norm)
@@ -1441,6 +1458,8 @@
   unfolding tendsto_def Limits.eventually_within eventually_at_topological
   by auto
 
+lemmas Lim_intros = Lim_add Lim_const Lim_sub Lim_cmul Lim_vmul Lim_within_id
+
 lemma Lim_at_id: "(id ---> a) (at a)"
 apply (subst within_UNIV[symmetric]) by (simp add: Lim_within_id)
 
@@ -1640,11 +1659,16 @@
 
 text{* Some other lemmas about sequences. *}
 
+lemma sequentially_offset:
+  assumes "eventually (\<lambda>i. P i) sequentially"
+  shows "eventually (\<lambda>i. P (i + k)) sequentially"
+  using assms unfolding eventually_sequentially by (metis trans_le_add1)
+
 lemma seq_offset:
-  fixes l :: "'a::metric_space" (* TODO: generalize *)
-  shows "(f ---> l) sequentially ==> ((\<lambda>i. f( i + k)) ---> l) sequentially"
-  apply (auto simp add: Lim_sequentially)
-  by (metis trans_le_add1 )
+  assumes "(f ---> l) sequentially"
+  shows "((\<lambda>i. f (i + k)) ---> l) sequentially"
+  using assms unfolding tendsto_def
+  by clarify (rule sequentially_offset, simp)
 
 lemma seq_offset_neg:
   "(f ---> l) sequentially ==> ((\<lambda>i. f(i - k)) ---> l) sequentially"
@@ -1673,7 +1697,7 @@
   thus ?thesis unfolding Lim_sequentially dist_norm by simp
 qed
 
-text{* More properties of closed balls. *}
+subsection {* More properties of closed balls. *}
 
 lemma closed_cball: "closed (cball x e)"
 unfolding cball_def closed_def
@@ -2156,7 +2180,9 @@
   apply (blast intro!: order_antisym dest!: isGlb_le_isLb)
   done
 
-subsection{* Compactness (the definition is the one based on convegent subsequences). *}
+subsection {* Equivalent versions of compactness *}
+
+subsubsection{* Sequential compactness *}
 
 definition
   compact :: "'a::metric_space set \<Rightarrow> bool" where (* TODO: generalize *)
@@ -2390,7 +2416,7 @@
     using l r by fast
 qed
 
-subsection{* Completeness. *}
+subsubsection{* Completeness *}
 
 lemma cauchy_def:
   "Cauchy s \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m n. m \<ge> N \<and> n \<ge> N --> dist(s m)(s n) < e)"
@@ -2537,7 +2563,7 @@
   unfolding image_def
   by auto
 
-subsection{* Total boundedness. *}
+subsubsection{* Total boundedness *}
 
 fun helper_1::"('a::metric_space set) \<Rightarrow> real \<Rightarrow> nat \<Rightarrow> 'a" where
   "helper_1 s e n = (SOME y::'a. y \<in> s \<and> (\<forall>m<n. \<not> (dist (helper_1 s e m) y < e)))"
@@ -2570,7 +2596,9 @@
     using x[THEN spec[where x="r (N+1)"], THEN spec[where x="r (N)"]] by auto
 qed
 
-subsection{* Heine-Borel theorem (following Burkill \& Burkill vol. 2) *}
+subsubsection{* Heine-Borel theorem *}
+
+text {* Following Burkill \& Burkill vol. 2. *}
 
 lemma heine_borel_lemma: fixes s::"'a::metric_space set"
   assumes "compact s"  "s \<subseteq> (\<Union> t)"  "\<forall>b \<in> t. open b"
@@ -2634,7 +2662,7 @@
   ultimately show "\<exists>f'\<subseteq>f. finite f' \<and> s \<subseteq> \<Union>f'" using bb k(2) by (rule_tac x="bb ` k" in exI) auto
 qed
 
-subsection{* Bolzano-Weierstrass property. *}
+subsubsection {* Bolzano-Weierstrass property *}
 
 lemma heine_borel_imp_bolzano_weierstrass:
   assumes "\<forall>f. (\<forall>t \<in> f. open t) \<and> s \<subseteq> (\<Union> f) --> (\<exists>f'. f' \<subseteq> f \<and> finite f' \<and> s \<subseteq> (\<Union> f'))"
@@ -2662,7 +2690,7 @@
   ultimately show False using g(2) using finite_subset by auto
 qed
 
-subsection{* Complete the chain of compactness variants. *}
+subsubsection {* Complete the chain of compactness variants *}
 
 primrec helper_2::"(real \<Rightarrow> 'a::metric_space) \<Rightarrow> nat \<Rightarrow> 'a" where
   "helper_2 beyond 0 = beyond 0" |
@@ -3098,7 +3126,9 @@
   ultimately show ?thesis by auto
 qed
 
-subsection{* Define continuity over a net to take in restrictions of the set. *}
+subsection {* Continuity *}
+
+text {* Define continuity over a net to take in restrictions of the set. *}
 
 definition
   continuous :: "'a::t2_space net \<Rightarrow> ('a \<Rightarrow> 'b::topological_space) \<Rightarrow> bool" where
@@ -3166,59 +3196,37 @@
     apply auto apply(erule_tac x=e in allE) apply auto apply(rule_tac x=d in exI) apply auto apply(erule_tac x="f xa" in allE) by (auto simp add: dist_commute dist_nz)
 qed
 
-text{* For setwise continuity, just start from the epsilon-delta definitions. *}
+text{* Define setwise continuity in terms of limits within the set. *}
 
 definition
   continuous_on ::
     "'a set \<Rightarrow> ('a::topological_space \<Rightarrow> 'b::topological_space) \<Rightarrow> bool"
 where
+  "continuous_on s f \<longleftrightarrow> (\<forall>x\<in>s. (f ---> f x) (at x within s))"
+
+lemma continuous_on_topological:
   "continuous_on s f \<longleftrightarrow>
     (\<forall>x\<in>s. \<forall>B. open B \<longrightarrow> f x \<in> B \<longrightarrow>
-      (\<exists>A. open A \<and> x \<in> A \<and> (\<forall>x'\<in>s. x' \<in> A \<longrightarrow> f x' \<in> B)))"
+      (\<exists>A. open A \<and> x \<in> A \<and> (\<forall>y\<in>s. y \<in> A \<longrightarrow> f y \<in> B)))"
+unfolding continuous_on_def tendsto_def
+unfolding Limits.eventually_within eventually_at_topological
+by (intro ball_cong [OF refl] all_cong imp_cong ex_cong conj_cong refl) auto
 
 lemma continuous_on_iff:
   "continuous_on s f \<longleftrightarrow>
-    (\<forall>x\<in>s. \<forall>e>0. \<exists>d>0. \<forall>x'\<in>s. dist x' x < d --> dist (f x') (f x) < e)"
-unfolding continuous_on_def
-apply safe
-apply (drule (1) bspec)
-apply (drule_tac x="ball (f x) e" in spec, simp, clarify)
-apply (drule (1) open_dist [THEN iffD1, THEN bspec])
-apply (clarify, rename_tac d)
-apply (rule_tac x=d in exI, clarify)
-apply (drule_tac x=x' in bspec, assumption)
-apply (drule_tac x=x' in spec, simp add: dist_commute)
-apply (drule_tac x=x in bspec, assumption)
-apply (drule (1) open_dist [THEN iffD1, THEN bspec], clarify)
-apply (drule_tac x=e in spec, simp, clarify)
-apply (rule_tac x="ball x d" in exI, simp, clarify)
-apply (drule_tac x=x' in bspec, assumption)
-apply (simp add: dist_commute)
+    (\<forall>x\<in>s. \<forall>e>0. \<exists>d>0. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e)"
+unfolding continuous_on_def Lim_within
+apply (intro ball_cong [OF refl] all_cong ex_cong)
+apply (rename_tac y, case_tac "y = x", simp)
+apply (simp add: dist_nz)
 done
 
 definition
   uniformly_continuous_on ::
-    "'a::metric_space set \<Rightarrow> ('a \<Rightarrow> 'b::metric_space) \<Rightarrow> bool" where
+    "'a set \<Rightarrow> ('a::metric_space \<Rightarrow> 'b::metric_space) \<Rightarrow> bool"
+where
   "uniformly_continuous_on s f \<longleftrightarrow>
-        (\<forall>e>0. \<exists>d>0. \<forall>x\<in>s. \<forall> x'\<in>s. dist x' x < d
-                           --> dist (f x') (f x) < e)"
-
-
-text{* Lifting and dropping *}
-
-lemma continuous_on_o_dest_vec1: fixes f::"real \<Rightarrow> 'a::real_normed_vector"
-  assumes "continuous_on {a..b::real} f" shows "continuous_on {vec1 a..vec1 b} (f o dest_vec1)"
-  using assms unfolding continuous_on_iff apply safe
-  apply(erule_tac x="x$1" in ballE,erule_tac x=e in allE) apply safe
-  apply(rule_tac x=d in exI) apply safe unfolding o_def dist_real_def dist_real 
-  apply(erule_tac x="dest_vec1 x'" in ballE) by(auto simp add:vector_le_def)
-
-lemma continuous_on_o_vec1: fixes f::"real^1 \<Rightarrow> 'a::real_normed_vector"
-  assumes "continuous_on {a..b} f" shows "continuous_on {dest_vec1 a..dest_vec1 b} (f o vec1)"
-  using assms unfolding continuous_on_iff apply safe
-  apply(erule_tac x="vec x" in ballE,erule_tac x=e in allE) apply safe
-  apply(rule_tac x=d in exI) apply safe unfolding o_def dist_real_def dist_real 
-  apply(erule_tac x="vec1 x'" in ballE) by(auto simp add:vector_le_def)
+    (\<forall>e>0. \<exists>d>0. \<forall>x\<in>s. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e)"
 
 text{* Some simple consequential lemmas. *}
 
@@ -3230,50 +3238,44 @@
  "continuous (at x) f ==> continuous (at x within s) f"
   unfolding continuous_within continuous_at using Lim_at_within by auto
 
+lemma Lim_trivial_limit: "trivial_limit net \<Longrightarrow> (f ---> l) net"
+unfolding tendsto_def by (simp add: trivial_limit_eq)
+
 lemma continuous_at_imp_continuous_on:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
-  assumes "(\<forall>x \<in> s. continuous (at x) f)"
+  assumes "\<forall>x\<in>s. continuous (at x) f"
   shows "continuous_on s f"
-proof(simp add: continuous_at continuous_on_iff, rule, rule, rule)
-  fix x and e::real assume "x\<in>s" "e>0"
-  hence "eventually (\<lambda>xa. dist (f xa) (f x) < e) (at x)" using assms unfolding continuous_at tendsto_iff by auto
-  then obtain d where d:"d>0" "\<forall>xa. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (f x) < e" unfolding eventually_at by auto
-  { fix x' assume "\<not> 0 < dist x' x"
-    hence "x=x'"
-      using dist_nz[of x' x] by auto
-    hence "dist (f x') (f x) < e" using `e>0` by auto
-  }
-  thus "\<exists>d>0. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e" using d by auto
+unfolding continuous_on_def
+proof
+  fix x assume "x \<in> s"
+  with assms have *: "(f ---> f (netlimit (at x))) (at x)"
+    unfolding continuous_def by simp
+  have "(f ---> f x) (at x)"
+  proof (cases "trivial_limit (at x)")
+    case True thus ?thesis
+      by (rule Lim_trivial_limit)
+  next
+    case False
+    hence "netlimit (at x) = x"
+      using netlimit_within [of x UNIV]
+      by (simp add: within_UNIV)
+    with * show ?thesis by simp
+  qed
+  thus "(f ---> f x) (at x within s)"
+    by (rule Lim_at_within)
 qed
 
 lemma continuous_on_eq_continuous_within:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
-  shows "continuous_on s f \<longleftrightarrow> (\<forall>x \<in> s. continuous (at x within s) f)"
-    (is "?lhs = ?rhs")
-proof
-  assume ?rhs
-  { fix x assume "x\<in>s"
-    fix e::real assume "e>0"
-    assume "\<exists>d>0. \<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (f x) < e"
-    then obtain d where "d>0" and d:"\<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (f x) < e" by auto
-    { fix x' assume as:"x'\<in>s" "dist x' x < d"
-      hence "dist (f x') (f x) < e" using `e>0` d `x'\<in>s` dist_eq_0_iff[of x' x] zero_le_dist[of x' x] as(2) by (metis dist_eq_0_iff dist_nz) }
-    hence "\<exists>d>0. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e" using `d>0` by auto
-  }
-  thus ?lhs using `?rhs` unfolding continuous_on_iff continuous_within Lim_within by auto
-next
-  assume ?lhs
-  thus ?rhs unfolding continuous_on_iff continuous_within Lim_within by blast
-qed
-
-lemma continuous_on:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
-  shows "continuous_on s f \<longleftrightarrow> (\<forall>x \<in> s. (f ---> f(x)) (at x within s))"
-  by (auto simp add: continuous_on_eq_continuous_within continuous_within)
-  (* BH: maybe this should be the definition? *)
+  "continuous_on s f \<longleftrightarrow> (\<forall>x \<in> s. continuous (at x within s) f)"
+unfolding continuous_on_def continuous_def
+apply (rule ball_cong [OF refl])
+apply (case_tac "trivial_limit (at x within s)")
+apply (simp add: Lim_trivial_limit)
+apply (simp add: netlimit_within)
+done
+
+lemmas continuous_on = continuous_on_def -- "legacy theorem name"
 
 lemma continuous_on_eq_continuous_at:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
   shows "open s ==> (continuous_on s f \<longleftrightarrow> (\<forall>x \<in> s. continuous (at x) f))"
   by (auto simp add: continuous_on continuous_at Lim_within_open)
 
@@ -3283,22 +3285,19 @@
   unfolding continuous_within by(metis Lim_within_subset)
 
 lemma continuous_on_subset:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
   shows "continuous_on s f \<Longrightarrow> t \<subseteq> s ==> continuous_on t f"
   unfolding continuous_on by (metis subset_eq Lim_within_subset)
 
 lemma continuous_on_interior:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
   shows "continuous_on s f \<Longrightarrow> x \<in> interior s ==> continuous (at x) f"
 unfolding interior_def
 apply simp
 by (meson continuous_on_eq_continuous_at continuous_on_subset)
 
 lemma continuous_on_eq:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
-  shows "(\<forall>x \<in> s. f x = g x) \<Longrightarrow> continuous_on s f
-           ==> continuous_on s g"
-  by (simp add: continuous_on_iff)
+  "(\<forall>x \<in> s. f x = g x) \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on s g"
+  unfolding continuous_on_def tendsto_def Limits.eventually_within
+  by simp
 
 text{* Characterization of various kinds of continuity in terms of sequences.  *}
 
@@ -3351,7 +3350,7 @@
   using continuous_within_sequentially[of a UNIV f] unfolding within_UNIV by auto
 
 lemma continuous_on_sequentially:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
   shows "continuous_on s f \<longleftrightarrow>
     (\<forall>x. \<forall>a \<in> s. (\<forall>n. x(n) \<in> s) \<and> (x ---> a) sequentially
                     --> ((f o x) ---> f(a)) sequentially)" (is "?lhs = ?rhs")
@@ -3361,24 +3360,23 @@
   assume ?lhs thus ?rhs unfolding continuous_on_eq_continuous_within using continuous_within_sequentially[of _ s f] by auto
 qed
 
-lemma uniformly_continuous_on_sequentially:
-  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
-  shows "uniformly_continuous_on s f \<longleftrightarrow> (\<forall>x y. (\<forall>n. x n \<in> s) \<and> (\<forall>n. y n \<in> s) \<and>
-                    ((\<lambda>n. x n - y n) ---> 0) sequentially
-                    \<longrightarrow> ((\<lambda>n. f(x n) - f(y n)) ---> 0) sequentially)" (is "?lhs = ?rhs")
+lemma uniformly_continuous_on_sequentially':
+  "uniformly_continuous_on s f \<longleftrightarrow> (\<forall>x y. (\<forall>n. x n \<in> s) \<and> (\<forall>n. y n \<in> s) \<and>
+                    ((\<lambda>n. dist (x n) (y n)) ---> 0) sequentially
+                    \<longrightarrow> ((\<lambda>n. dist (f(x n)) (f(y n))) ---> 0) sequentially)" (is "?lhs = ?rhs")
 proof
   assume ?lhs
-  { fix x y assume x:"\<forall>n. x n \<in> s" and y:"\<forall>n. y n \<in> s" and xy:"((\<lambda>n. x n - y n) ---> 0) sequentially"
+  { fix x y assume x:"\<forall>n. x n \<in> s" and y:"\<forall>n. y n \<in> s" and xy:"((\<lambda>n. dist (x n) (y n)) ---> 0) sequentially"
     { fix e::real assume "e>0"
       then obtain d where "d>0" and d:"\<forall>x\<in>s. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e"
         using `?lhs`[unfolded uniformly_continuous_on_def, THEN spec[where x=e]] by auto
-      obtain N where N:"\<forall>n\<ge>N. norm (x n - y n - 0) < d" using xy[unfolded Lim_sequentially dist_norm] and `d>0` by auto
+      obtain N where N:"\<forall>n\<ge>N. dist (x n) (y n) < d" using xy[unfolded Lim_sequentially dist_norm] and `d>0` by auto
       { fix n assume "n\<ge>N"
-        hence "norm (f (x n) - f (y n) - 0) < e"
+        hence "dist (f (x n)) (f (y n)) < e"
           using N[THEN spec[where x=n]] using d[THEN bspec[where x="x n"], THEN bspec[where x="y n"]] using x and y
-          unfolding dist_commute and dist_norm by simp  }
-      hence "\<exists>N. \<forall>n\<ge>N. norm (f (x n) - f (y n) - 0) < e"  by auto  }
-    hence "((\<lambda>n. f(x n) - f(y n)) ---> 0) sequentially" unfolding Lim_sequentially and dist_norm by auto  }
+          unfolding dist_commute by simp  }
+      hence "\<exists>N. \<forall>n\<ge>N. dist (f (x n)) (f (y n)) < e"  by auto  }
+    hence "((\<lambda>n. dist (f(x n)) (f(y n))) ---> 0) sequentially" unfolding Lim_sequentially and dist_real_def by auto  }
   thus ?rhs by auto
 next
   assume ?rhs
@@ -3391,25 +3389,32 @@
     def y \<equiv> "\<lambda>n::nat. snd (fa (inverse (real n + 1)))"
     have xyn:"\<forall>n. x n \<in> s \<and> y n \<in> s" and xy0:"\<forall>n. dist (x n) (y n) < inverse (real n + 1)" and fxy:"\<forall>n. \<not> dist (f (x n)) (f (y n)) < e"
       unfolding x_def and y_def using fa by auto
-    have 1:"\<And>(x::'a) y. dist (x - y) 0 = dist x y" unfolding dist_norm by auto
-    have 2:"\<And>(x::'b) y. dist (x - y) 0 = dist x y" unfolding dist_norm by auto
     { fix e::real assume "e>0"
       then obtain N::nat where "N \<noteq> 0" and N:"0 < inverse (real N) \<and> inverse (real N) < e" unfolding real_arch_inv[of e]   by auto
       { fix n::nat assume "n\<ge>N"
         hence "inverse (real n + 1) < inverse (real N)" using real_of_nat_ge_zero and `N\<noteq>0` by auto
         also have "\<dots> < e" using N by auto
         finally have "inverse (real n + 1) < e" by auto
-        hence "dist (x n - y n) 0 < e" unfolding 1 using xy0[THEN spec[where x=n]] by auto  }
-      hence "\<exists>N. \<forall>n\<ge>N. dist (x n - y n) 0 < e" by auto  }
-    hence "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (f (x n) - f (y n)) 0 < e" using `?rhs`[THEN spec[where x=x], THEN spec[where x=y]] and xyn unfolding Lim_sequentially by auto
-    hence False unfolding 2 using fxy and `e>0` by auto  }
+        hence "dist (x n) (y n) < e" using xy0[THEN spec[where x=n]] by auto  }
+      hence "\<exists>N. \<forall>n\<ge>N. dist (x n) (y n) < e" by auto  }
+    hence "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (f (x n)) (f (y n)) < e" using `?rhs`[THEN spec[where x=x], THEN spec[where x=y]] and xyn unfolding Lim_sequentially dist_real_def by auto
+    hence False using fxy and `e>0` by auto  }
   thus ?lhs unfolding uniformly_continuous_on_def by blast
 qed
 
+lemma uniformly_continuous_on_sequentially:
+  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
+  shows "uniformly_continuous_on s f \<longleftrightarrow> (\<forall>x y. (\<forall>n. x n \<in> s) \<and> (\<forall>n. y n \<in> s) \<and>
+                    ((\<lambda>n. x n - y n) ---> 0) sequentially
+                    \<longrightarrow> ((\<lambda>n. f(x n) - f(y n)) ---> 0) sequentially)" (is "?lhs = ?rhs")
+(* BH: maybe the previous lemma should replace this one? *)
+unfolding uniformly_continuous_on_sequentially'
+unfolding dist_norm Lim_null_norm [symmetric] ..
+
 text{* The usual transformation theorems. *}
 
 lemma continuous_transform_within:
-  fixes f g :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+  fixes f g :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
   assumes "0 < d" "x \<in> s" "\<forall>x' \<in> s. dist x' x < d --> f x' = g x'"
           "continuous (at x within s) f"
   shows "continuous (at x within s) g"
@@ -3425,7 +3430,7 @@
 qed
 
 lemma continuous_transform_at:
-  fixes f g :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+  fixes f g :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
   assumes "0 < d" "\<forall>x'. dist x' x < d --> f x' = g x'"
           "continuous (at x) f"
   shows "continuous (at x) g"
@@ -3475,26 +3480,26 @@
   unfolding continuous_on_def by auto
 
 lemma continuous_on_cmul:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
-  shows "continuous_on s f ==>  continuous_on s (\<lambda>x. c *\<^sub>R (f x))"
-  unfolding continuous_on_eq_continuous_within using continuous_cmul by blast
+  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
+  shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. c *\<^sub>R (f x))"
+  unfolding continuous_on_def by (auto intro: tendsto_intros)
 
 lemma continuous_on_neg:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. - f x)"
-  unfolding continuous_on_eq_continuous_within using continuous_neg by blast
+  unfolding continuous_on_def by (auto intro: tendsto_intros)
 
 lemma continuous_on_add:
-  fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+  fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   shows "continuous_on s f \<Longrightarrow> continuous_on s g
            \<Longrightarrow> continuous_on s (\<lambda>x. f x + g x)"
-  unfolding continuous_on_eq_continuous_within using continuous_add by blast
+  unfolding continuous_on_def by (auto intro: tendsto_intros)
 
 lemma continuous_on_sub:
-  fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+  fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   shows "continuous_on s f \<Longrightarrow> continuous_on s g
            \<Longrightarrow> continuous_on s (\<lambda>x. f x - g x)"
-  unfolding continuous_on_eq_continuous_within using continuous_sub by blast
+  unfolding continuous_on_def by (auto intro: tendsto_intros)
 
 text{* Same thing for uniform continuity, using sequential formulations. *}
 
@@ -3503,8 +3508,7 @@
   unfolding uniformly_continuous_on_def by simp
 
 lemma uniformly_continuous_on_cmul:
-  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
-    (* FIXME: generalize 'a to metric_space *)
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   assumes "uniformly_continuous_on s f"
   shows "uniformly_continuous_on s (\<lambda>x. c *\<^sub>R f(x))"
 proof-
@@ -3513,7 +3517,8 @@
       using Lim_cmul[of "(\<lambda>n. f (x n) - f (y n))" 0 sequentially c]
       unfolding scaleR_zero_right scaleR_right_diff_distrib by auto
   }
-  thus ?thesis using assms unfolding uniformly_continuous_on_sequentially by auto
+  thus ?thesis using assms unfolding uniformly_continuous_on_sequentially'
+    unfolding dist_norm Lim_null_norm [symmetric] by auto
 qed
 
 lemma dist_minus:
@@ -3528,7 +3533,7 @@
   unfolding uniformly_continuous_on_def dist_minus .
 
 lemma uniformly_continuous_on_add:
-  fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" (* FIXME: generalize 'a *)
+  fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   assumes "uniformly_continuous_on s f" "uniformly_continuous_on s g"
   shows "uniformly_continuous_on s (\<lambda>x. f x + g x)"
 proof-
@@ -3537,11 +3542,12 @@
     hence "((\<lambda>xa. f (x xa) - f (y xa) + (g (x xa) - g (y xa))) ---> 0 + 0) sequentially"
       using Lim_add[of "\<lambda> n. f (x n) - f (y n)" 0  sequentially "\<lambda> n. g (x n) - g (y n)" 0] by auto
     hence "((\<lambda>n. f (x n) + g (x n) - (f (y n) + g (y n))) ---> 0) sequentially" unfolding Lim_sequentially and add_diff_add [symmetric] by auto  }
-  thus ?thesis using assms unfolding uniformly_continuous_on_sequentially by auto
+  thus ?thesis using assms unfolding uniformly_continuous_on_sequentially'
+    unfolding dist_norm Lim_null_norm [symmetric] by auto
 qed
 
 lemma uniformly_continuous_on_sub:
-  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" (* FIXME: generalize 'a *)
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   shows "uniformly_continuous_on s f \<Longrightarrow> uniformly_continuous_on s g
            ==> uniformly_continuous_on s  (\<lambda>x. f x - g x)"
   unfolding ab_diff_minus
@@ -3560,7 +3566,7 @@
 
 lemma continuous_on_id:
  "continuous_on s (\<lambda>x. x)"
-  unfolding continuous_on_def by auto
+  unfolding continuous_on_def by (auto intro: tendsto_ident_at_within)
 
 lemma uniformly_continuous_on_id:
  "uniformly_continuous_on s (\<lambda>x. x)"
@@ -3568,25 +3574,21 @@
 
 text{* Continuity of all kinds is preserved under composition. *}
 
+lemma continuous_within_topological:
+  "continuous (at x within s) f \<longleftrightarrow>
+    (\<forall>B. open B \<longrightarrow> f x \<in> B \<longrightarrow>
+      (\<exists>A. open A \<and> x \<in> A \<and> (\<forall>y\<in>s. y \<in> A \<longrightarrow> f y \<in> B)))"
+unfolding continuous_within
+unfolding tendsto_def Limits.eventually_within eventually_at_topological
+by (intro ball_cong [OF refl] all_cong imp_cong ex_cong conj_cong refl) auto
+
 lemma continuous_within_compose:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
-  fixes g :: "'b::metric_space \<Rightarrow> 'c::metric_space"
-  assumes "continuous (at x within s) f"   "continuous (at (f x) within f ` s) g"
+  assumes "continuous (at x within s) f"
+  assumes "continuous (at (f x) within f ` s) g"
   shows "continuous (at x within s) (g o f)"
-proof-
-  { fix e::real assume "e>0"
-    with assms(2)[unfolded continuous_within Lim_within] obtain d  where "d>0" and d:"\<forall>xa\<in>f ` s. 0 < dist xa (f x) \<and> dist xa (f x) < d \<longrightarrow> dist (g xa) (g (f x)) < e" by auto
-    from assms(1)[unfolded continuous_within Lim_within] obtain d' where "d'>0" and d':"\<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d' \<longrightarrow> dist (f xa) (f x) < d" using `d>0` by auto
-    { fix y assume as:"y\<in>s"  "0 < dist y x"  "dist y x < d'"
-      hence "dist (f y) (f x) < d" using d'[THEN bspec[where x=y]] by (auto simp add:dist_commute)
-      hence "dist (g (f y)) (g (f x)) < e" using as(1) d[THEN bspec[where x="f y"]] unfolding dist_nz[THEN sym] using `e>0` by auto   }
-    hence "\<exists>d>0. \<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (g (f xa)) (g (f x)) < e" using `d'>0` by auto  }
-  thus ?thesis unfolding continuous_within Lim_within by auto
-qed
+using assms unfolding continuous_within_topological by simp metis
 
 lemma continuous_at_compose:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
-  fixes g :: "'b::metric_space \<Rightarrow> 'c::metric_space"
   assumes "continuous (at x) f"  "continuous (at (f x)) g"
   shows "continuous (at x) (g o f)"
 proof-
@@ -3595,10 +3597,8 @@
 qed
 
 lemma continuous_on_compose:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
-  fixes g :: "'b::metric_space \<Rightarrow> 'c::metric_space" (* TODO: generalize *)
-  shows "continuous_on s f \<Longrightarrow> continuous_on (f ` s) g \<Longrightarrow> continuous_on s (g o f)"
-  unfolding continuous_on_eq_continuous_within using continuous_within_compose[of _ s f g] by auto
+  "continuous_on s f \<Longrightarrow> continuous_on (f ` s) g \<Longrightarrow> continuous_on s (g o f)"
+  unfolding continuous_on_topological by simp metis
 
 lemma uniformly_continuous_on_compose:
   assumes "uniformly_continuous_on s f"  "uniformly_continuous_on (f ` s) g"
@@ -3614,75 +3614,55 @@
 text{* Continuity in terms of open preimages. *}
 
 lemma continuous_at_open:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
-  shows "continuous (at x) f \<longleftrightarrow> (\<forall>t. open t \<and> f x \<in> t --> (\<exists>s. open s \<and> x \<in> s \<and> (\<forall>x' \<in> s. (f x') \<in> t)))" (is "?lhs = ?rhs")
-proof
-  assume ?lhs
-  { fix t assume as: "open t" "f x \<in> t"
-    then obtain e where "e>0" and e:"ball (f x) e \<subseteq> t" unfolding open_contains_ball by auto
-
-    obtain d where "d>0" and d:"\<forall>y. 0 < dist y x \<and> dist y x < d \<longrightarrow> dist (f y) (f x) < e" using `e>0` using `?lhs`[unfolded continuous_at Lim_at open_dist] by auto
-
-    have "open (ball x d)" using open_ball by auto
-    moreover have "x \<in> ball x d" unfolding centre_in_ball using `d>0` by simp
-    moreover
-    { fix x' assume "x'\<in>ball x d" hence "f x' \<in> t"
-        using e[unfolded subset_eq Ball_def mem_ball, THEN spec[where x="f x'"]]    d[THEN spec[where x=x']]
-        unfolding mem_ball apply (auto simp add: dist_commute)
-        unfolding dist_nz[THEN sym] using as(2) by auto  }
-    hence "\<forall>x'\<in>ball x d. f x' \<in> t" by auto
-    ultimately have "\<exists>s. open s \<and> x \<in> s \<and> (\<forall>x'\<in>s. f x' \<in> t)"
-      apply(rule_tac x="ball x d" in exI) by simp  }
-  thus ?rhs by auto
-next
-  assume ?rhs
-  { fix e::real assume "e>0"
-    then obtain s where s: "open s"  "x \<in> s"  "\<forall>x'\<in>s. f x' \<in> ball (f x) e" using `?rhs`[unfolded continuous_at Lim_at, THEN spec[where x="ball (f x) e"]]
-      unfolding centre_in_ball[of "f x" e, THEN sym] by auto
-    then obtain d where "d>0" and d:"ball x d \<subseteq> s" unfolding open_contains_ball by auto
-    { fix y assume "0 < dist y x \<and> dist y x < d"
-      hence "dist (f y) (f x) < e" using d[unfolded subset_eq Ball_def mem_ball, THEN spec[where x=y]]
-        using s(3)[THEN bspec[where x=y], unfolded mem_ball] by (auto simp add: dist_commute)  }
-    hence "\<exists>d>0. \<forall>xa. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (f x) < e" using `d>0` by auto  }
-  thus ?lhs unfolding continuous_at Lim_at by auto
-qed
+  shows "continuous (at x) f \<longleftrightarrow> (\<forall>t. open t \<and> f x \<in> t --> (\<exists>s. open s \<and> x \<in> s \<and> (\<forall>x' \<in> s. (f x') \<in> t)))"
+unfolding continuous_within_topological [of x UNIV f, unfolded within_UNIV]
+unfolding imp_conjL by (intro all_cong imp_cong ex_cong conj_cong refl) auto
 
 lemma continuous_on_open:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
-   shows "continuous_on s f \<longleftrightarrow>
+  shows "continuous_on s f \<longleftrightarrow>
         (\<forall>t. openin (subtopology euclidean (f ` s)) t
             --> openin (subtopology euclidean s) {x \<in> s. f x \<in> t})" (is "?lhs = ?rhs")
-proof
-  assume ?lhs
-  { fix t assume as:"openin (subtopology euclidean (f ` s)) t"
-    have "{x \<in> s. f x \<in> t} \<subseteq> s" using as[unfolded openin_euclidean_subtopology_iff] by auto
-    moreover
-    { fix x assume as':"x\<in>{x \<in> s. f x \<in> t}"
-      then obtain e where e: "e>0" "\<forall>x'\<in>f ` s. dist x' (f x) < e \<longrightarrow> x' \<in> t" using as[unfolded openin_euclidean_subtopology_iff, THEN conjunct2, THEN bspec[where x="f x"]] by auto
-      from this(1) obtain d where d: "d>0" "\<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (f x) < e" using `?lhs`[unfolded continuous_on Lim_within, THEN bspec[where x=x]] using as' by auto
-      have "\<exists>e>0. \<forall>x'\<in>s. dist x' x < e \<longrightarrow> x' \<in> {x \<in> s. f x \<in> t}" using d e unfolding dist_nz[THEN sym] by (rule_tac x=d in exI, auto)  }
-    ultimately have "openin (subtopology euclidean s) {x \<in> s. f x \<in> t}" unfolding openin_euclidean_subtopology_iff by auto  }
-  thus ?rhs unfolding continuous_on Lim_within using openin by auto
+proof (safe)
+  fix t :: "'b set"
+  assume 1: "continuous_on s f"
+  assume 2: "openin (subtopology euclidean (f ` s)) t"
+  from 2 obtain B where B: "open B" and t: "t = f ` s \<inter> B"
+    unfolding openin_open by auto
+  def U == "\<Union>{A. open A \<and> (\<forall>x\<in>s. x \<in> A \<longrightarrow> f x \<in> B)}"
+  have "open U" unfolding U_def by (simp add: open_Union)
+  moreover have "\<forall>x\<in>s. x \<in> U \<longleftrightarrow> f x \<in> t"
+  proof (intro ballI iffI)
+    fix x assume "x \<in> s" and "x \<in> U" thus "f x \<in> t"
+      unfolding U_def t by auto
+  next
+    fix x assume "x \<in> s" and "f x \<in> t"
+    hence "x \<in> s" and "f x \<in> B"
+      unfolding t by auto
+    with 1 B obtain A where "open A" "x \<in> A" "\<forall>y\<in>s. y \<in> A \<longrightarrow> f y \<in> B"
+      unfolding t continuous_on_topological by metis
+    then show "x \<in> U"
+      unfolding U_def by auto
+  qed
+  ultimately have "open U \<and> {x \<in> s. f x \<in> t} = s \<inter> U" by auto
+  then show "openin (subtopology euclidean s) {x \<in> s. f x \<in> t}"
+    unfolding openin_open by fast
 next
-  assume ?rhs
-  { fix e::real and x assume "x\<in>s" "e>0"
-    { fix xa x' assume "dist (f xa) (f x) < e" "xa \<in> s" "x' \<in> s" "dist (f xa) (f x') < e - dist (f xa) (f x)"
-      hence "dist (f x') (f x) < e" using dist_triangle[of "f x'" "f x" "f xa"]
-        by (auto simp add: dist_commute)  }
-    hence "ball (f x) e \<inter> f ` s \<subseteq> f ` s \<and> (\<forall>xa\<in>ball (f x) e \<inter> f ` s. \<exists>ea>0. \<forall>x'\<in>f ` s. dist x' xa < ea \<longrightarrow> x' \<in> ball (f x) e \<inter> f ` s)" apply auto
-      apply(rule_tac x="e - dist (f xa) (f x)" in exI) using `e>0` by (auto simp add: dist_commute)
-    hence "\<forall>xa\<in>{xa \<in> s. f xa \<in> ball (f x) e \<inter> f ` s}. \<exists>ea>0. \<forall>x'\<in>s. dist x' xa < ea \<longrightarrow> x' \<in> {xa \<in> s. f xa \<in> ball (f x) e \<inter> f ` s}"
-      using `?rhs`[unfolded openin_euclidean_subtopology_iff, THEN spec[where x="ball (f x) e \<inter> f ` s"]] by auto
-    hence "\<exists>d>0. \<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (f x) < e" apply(erule_tac x=x in ballE) apply auto using `e>0` `x\<in>s` by (auto simp add: dist_commute)  }
-  thus ?lhs unfolding continuous_on Lim_within by auto
-qed
-
-(* ------------------------------------------------------------------------- *)
-(* Similarly in terms of closed sets.                                        *)
-(* ------------------------------------------------------------------------- *)
+  assume "?rhs" show "continuous_on s f"
+  unfolding continuous_on_topological
+  proof (clarify)
+    fix x and B assume "x \<in> s" and "open B" and "f x \<in> B"
+    have "openin (subtopology euclidean (f ` s)) (f ` s \<inter> B)"
+      unfolding openin_open using `open B` by auto
+    then have "openin (subtopology euclidean s) {x \<in> s. f x \<in> f ` s \<inter> B}"
+      using `?rhs` by fast
+    then show "\<exists>A. open A \<and> x \<in> A \<and> (\<forall>y\<in>s. y \<in> A \<longrightarrow> f y \<in> B)"
+      unfolding openin_open using `x \<in> s` and `f x \<in> B` by auto
+  qed
+qed
+
+text {* Similarly in terms of closed sets. *}
 
 lemma continuous_on_closed:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
   shows "continuous_on s f \<longleftrightarrow>  (\<forall>t. closedin (subtopology euclidean (f ` s)) t  --> closedin (subtopology euclidean s) {x \<in> s. f x \<in> t})" (is "?lhs = ?rhs")
 proof
   assume ?lhs
@@ -3707,7 +3687,6 @@
 text{* Half-global and completely global cases.                                  *}
 
 lemma continuous_open_in_preimage:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
   assumes "continuous_on s f"  "open t"
   shows "openin (subtopology euclidean s) {x \<in> s. f x \<in> t}"
 proof-
@@ -3718,7 +3697,6 @@
 qed
 
 lemma continuous_closed_in_preimage:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
   assumes "continuous_on s f"  "closed t"
   shows "closedin (subtopology euclidean s) {x \<in> s. f x \<in> t}"
 proof-
@@ -3730,7 +3708,6 @@
 qed
 
 lemma continuous_open_preimage:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
   assumes "continuous_on s f" "open s" "open t"
   shows "open {x \<in> s. f x \<in> t}"
 proof-
@@ -3740,7 +3717,6 @@
 qed
 
 lemma continuous_closed_preimage:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
   assumes "continuous_on s f" "closed s" "closed t"
   shows "closed {x \<in> s. f x \<in> t}"
 proof-
@@ -3750,26 +3726,22 @@
 qed
 
 lemma continuous_open_preimage_univ:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
   shows "\<forall>x. continuous (at x) f \<Longrightarrow> open s \<Longrightarrow> open {x. f x \<in> s}"
   using continuous_open_preimage[of UNIV f s] open_UNIV continuous_at_imp_continuous_on by auto
 
 lemma continuous_closed_preimage_univ:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
   shows "(\<forall>x. continuous (at x) f) \<Longrightarrow> closed s ==> closed {x. f x \<in> s}"
   using continuous_closed_preimage[of UNIV f s] closed_UNIV continuous_at_imp_continuous_on by auto
 
 lemma continuous_open_vimage:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
   shows "\<forall>x. continuous (at x) f \<Longrightarrow> open s \<Longrightarrow> open (f -` s)"
   unfolding vimage_def by (rule continuous_open_preimage_univ)
 
 lemma continuous_closed_vimage:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
   shows "\<forall>x. continuous (at x) f \<Longrightarrow> closed s \<Longrightarrow> closed (f -` s)"
   unfolding vimage_def by (rule continuous_closed_preimage_univ)
 
-lemma interior_image_subset: fixes f::"_::metric_space \<Rightarrow> _::metric_space"
+lemma interior_image_subset:
   assumes "\<forall>x. continuous (at x) f" "inj f"
   shows "interior (f ` s) \<subseteq> f ` (interior s)"
   apply rule unfolding interior_def mem_Collect_eq image_iff apply safe
@@ -3783,17 +3755,17 @@
 text{* Equality of continuous functions on closure and related results.          *}
 
 lemma continuous_closed_in_preimage_constant:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+  fixes f :: "_ \<Rightarrow> 'b::metric_space" (* class constraint due to closed_sing *)
   shows "continuous_on s f ==> closedin (subtopology euclidean s) {x \<in> s. f x = a}"
   using continuous_closed_in_preimage[of s f "{a}"] closed_sing by auto
 
 lemma continuous_closed_preimage_constant:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+  fixes f :: "_ \<Rightarrow> 'b::metric_space" (* class constraint due to closed_sing *)
   shows "continuous_on s f \<Longrightarrow> closed s ==> closed {x \<in> s. f x = a}"
   using continuous_closed_preimage[of s f "{a}"] closed_sing by auto
 
 lemma continuous_constant_on_closure:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+  fixes f :: "_ \<Rightarrow> 'b::metric_space" (* class constraint due to closed_sing *)
   assumes "continuous_on (closure s) f"
           "\<forall>x \<in> s. f x = a"
   shows "\<forall>x \<in> (closure s). f x = a"
@@ -3801,7 +3773,6 @@
     assms closure_minimal[of s "{x \<in> closure s. f x = a}"] closure_subset unfolding subset_eq by auto
 
 lemma image_closure_subset:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
   assumes "continuous_on (closure s) f"  "closed t"  "(f ` s) \<subseteq> t"
   shows "f ` (closure s) \<subseteq> t"
 proof-
@@ -3860,14 +3831,14 @@
 text{* Proving a function is constant by proving open-ness of level set.         *}
 
 lemma continuous_levelset_open_in_cases:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+  fixes f :: "_ \<Rightarrow> 'b::metric_space" (* class constraint due to closed_sing *)
   shows "connected s \<Longrightarrow> continuous_on s f \<Longrightarrow>
         openin (subtopology euclidean s) {x \<in> s. f x = a}
         ==> (\<forall>x \<in> s. f x \<noteq> a) \<or> (\<forall>x \<in> s. f x = a)"
 unfolding connected_clopen using continuous_closed_in_preimage_constant by auto
 
 lemma continuous_levelset_open_in:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+  fixes f :: "_ \<Rightarrow> 'b::metric_space" (* class constraint due to closed_sing *)
   shows "connected s \<Longrightarrow> continuous_on s f \<Longrightarrow>
         openin (subtopology euclidean s) {x \<in> s. f x = a} \<Longrightarrow>
         (\<exists>x \<in> s. f x = a)  ==> (\<forall>x \<in> s. f x = a)"
@@ -3875,7 +3846,7 @@
 by meson
 
 lemma continuous_levelset_open:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+  fixes f :: "_ \<Rightarrow> 'b::metric_space" (* class constraint due to closed_sing *)
   assumes "connected s"  "continuous_on s f"  "open {x \<in> s. f x = a}"  "\<exists>x \<in> s.  f x = a"
   shows "\<forall>x \<in> s. f x = a"
 using continuous_levelset_open_in[OF assms(1,2), of a, unfolded openin_open] using assms (3,4) by fast
@@ -3949,7 +3920,104 @@
   thus "x \<in> interior (op + a ` s)" unfolding mem_interior using `e>0` by auto
 qed
 
-subsection {* Preservation of compactness and connectedness under continuous function.  *}
+text {* We can now extend limit compositions to consider the scalar multiplier.   *}
+
+lemma continuous_vmul:
+  fixes c :: "'a::metric_space \<Rightarrow> real" and v :: "'b::real_normed_vector"
+  shows "continuous net c ==> continuous net (\<lambda>x. c(x) *\<^sub>R v)"
+  unfolding continuous_def using Lim_vmul[of c] by auto
+
+lemma continuous_mul:
+  fixes c :: "'a::metric_space \<Rightarrow> real"
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+  shows "continuous net c \<Longrightarrow> continuous net f
+             ==> continuous net (\<lambda>x. c(x) *\<^sub>R f x) "
+  unfolding continuous_def by (intro tendsto_intros)
+
+lemmas continuous_intros = continuous_add continuous_vmul continuous_cmul continuous_const continuous_sub continuous_at_id continuous_within_id continuous_mul
+
+lemma continuous_on_vmul:
+  fixes c :: "'a::metric_space \<Rightarrow> real" and v :: "'b::real_normed_vector"
+  shows "continuous_on s c ==> continuous_on s (\<lambda>x. c(x) *\<^sub>R v)"
+  unfolding continuous_on_eq_continuous_within using continuous_vmul[of _ c] by auto
+
+lemma continuous_on_mul:
+  fixes c :: "'a::metric_space \<Rightarrow> real"
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+  shows "continuous_on s c \<Longrightarrow> continuous_on s f
+             ==> continuous_on s (\<lambda>x. c(x) *\<^sub>R f x)"
+  unfolding continuous_on_eq_continuous_within using continuous_mul[of _ c] by auto
+
+lemmas continuous_on_intros = continuous_on_add continuous_on_const continuous_on_id continuous_on_compose continuous_on_cmul continuous_on_neg continuous_on_sub
+  uniformly_continuous_on_add uniformly_continuous_on_const uniformly_continuous_on_id uniformly_continuous_on_compose uniformly_continuous_on_cmul uniformly_continuous_on_neg uniformly_continuous_on_sub
+  continuous_on_mul continuous_on_vmul
+
+text{* And so we have continuity of inverse.                                     *}
+
+lemma continuous_inv:
+  fixes f :: "'a::metric_space \<Rightarrow> real"
+  shows "continuous net f \<Longrightarrow> f(netlimit net) \<noteq> 0
+           ==> continuous net (inverse o f)"
+  unfolding continuous_def using Lim_inv by auto
+
+lemma continuous_at_within_inv:
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_field"
+  assumes "continuous (at a within s) f" "f a \<noteq> 0"
+  shows "continuous (at a within s) (inverse o f)"
+  using assms unfolding continuous_within o_def
+  by (intro tendsto_intros)
+
+lemma continuous_at_inv:
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_field"
+  shows "continuous (at a) f \<Longrightarrow> f a \<noteq> 0
+         ==> continuous (at a) (inverse o f) "
+  using within_UNIV[THEN sym, of "at a"] using continuous_at_within_inv[of a UNIV] by auto
+
+text {* Topological properties of linear functions. *}
+
+lemma linear_lim_0:
+  assumes "bounded_linear f" shows "(f ---> 0) (at (0))"
+proof-
+  interpret f: bounded_linear f by fact
+  have "(f ---> f 0) (at 0)"
+    using tendsto_ident_at by (rule f.tendsto)
+  thus ?thesis unfolding f.zero .
+qed
+
+lemma linear_continuous_at:
+  assumes "bounded_linear f"  shows "continuous (at a) f"
+  unfolding continuous_at using assms
+  apply (rule bounded_linear.tendsto)
+  apply (rule tendsto_ident_at)
+  done
+
+lemma linear_continuous_within:
+  shows "bounded_linear f ==> continuous (at x within s) f"
+  using continuous_at_imp_continuous_within[of x f s] using linear_continuous_at[of f] by auto
+
+lemma linear_continuous_on:
+  shows "bounded_linear f ==> continuous_on s f"
+  using continuous_at_imp_continuous_on[of s f] using linear_continuous_at[of f] by auto
+
+text{* Also bilinear functions, in composition form.                             *}
+
+lemma bilinear_continuous_at_compose:
+  shows "continuous (at x) f \<Longrightarrow> continuous (at x) g \<Longrightarrow> bounded_bilinear h
+        ==> continuous (at x) (\<lambda>x. h (f x) (g x))"
+  unfolding continuous_at using Lim_bilinear[of f "f x" "(at x)" g "g x" h] by auto
+
+lemma bilinear_continuous_within_compose:
+  shows "continuous (at x within s) f \<Longrightarrow> continuous (at x within s) g \<Longrightarrow> bounded_bilinear h
+        ==> continuous (at x within s) (\<lambda>x. h (f x) (g x))"
+  unfolding continuous_within using Lim_bilinear[of f "f x"] by auto
+
+lemma bilinear_continuous_on_compose:
+  shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> bounded_bilinear h
+             ==> continuous_on s (\<lambda>x. h (f x) (g x))"
+  unfolding continuous_on_def
+  by (fast elim: bounded_bilinear.tendsto)
+
+text {* Preservation of compactness and connectedness under continuous function.  *}
 
 lemma compact_continuous_image:
   assumes "continuous_on s f"  "compact s"
@@ -3968,7 +4036,6 @@
 qed
 
 lemma connected_continuous_image:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
   assumes "continuous_on s f"  "connected s"
   shows "connected(f ` s)"
 proof-
@@ -4042,7 +4109,7 @@
   thus ?thesis unfolding continuous_on_closed by auto
 qed
 
-subsection{* A uniformly convergent limit of continuous functions is continuous.       *}
+text {* A uniformly convergent limit of continuous functions is continuous. *}
 
 lemma norm_triangle_lt:
   fixes x y :: "'a::real_normed_vector"
@@ -4072,54 +4139,6 @@
   thus ?thesis unfolding continuous_on_iff by auto
 qed
 
-subsection{* Topological properties of linear functions.                               *}
-
-lemma linear_lim_0:
-  assumes "bounded_linear f" shows "(f ---> 0) (at (0))"
-proof-
-  interpret f: bounded_linear f by fact
-  have "(f ---> f 0) (at 0)"
-    using tendsto_ident_at by (rule f.tendsto)
-  thus ?thesis unfolding f.zero .
-qed
-
-lemma linear_continuous_at:
-  assumes "bounded_linear f"  shows "continuous (at a) f"
-  unfolding continuous_at using assms
-  apply (rule bounded_linear.tendsto)
-  apply (rule tendsto_ident_at)
-  done
-
-lemma linear_continuous_within:
-  shows "bounded_linear f ==> continuous (at x within s) f"
-  using continuous_at_imp_continuous_within[of x f s] using linear_continuous_at[of f] by auto
-
-lemma linear_continuous_on:
-  shows "bounded_linear f ==> continuous_on s f"
-  using continuous_at_imp_continuous_on[of s f] using linear_continuous_at[of f] by auto
-
-lemma continuous_on_vec1:"continuous_on A (vec1::real\<Rightarrow>real^1)"
-  by(rule linear_continuous_on[OF bounded_linear_vec1])
-
-text{* Also bilinear functions, in composition form.                             *}
-
-lemma bilinear_continuous_at_compose:
-  shows "continuous (at x) f \<Longrightarrow> continuous (at x) g \<Longrightarrow> bounded_bilinear h
-        ==> continuous (at x) (\<lambda>x. h (f x) (g x))"
-  unfolding continuous_at using Lim_bilinear[of f "f x" "(at x)" g "g x" h] by auto
-
-lemma bilinear_continuous_within_compose:
-  shows "continuous (at x within s) f \<Longrightarrow> continuous (at x within s) g \<Longrightarrow> bounded_bilinear h
-        ==> continuous (at x within s) (\<lambda>x. h (f x) (g x))"
-  unfolding continuous_within using Lim_bilinear[of f "f x"] by auto
-
-lemma bilinear_continuous_on_compose:
-  fixes s :: "'a::metric_space set" (* TODO: generalize *)
-  shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> bounded_bilinear h
-             ==> continuous_on s (\<lambda>x. h (f x) (g x))"
-  unfolding continuous_on_eq_continuous_within apply auto apply(erule_tac x=x in ballE) apply auto apply(erule_tac x=x in ballE) apply auto
-  using bilinear_continuous_within_compose[of _ s f g h] by auto
-
 subsection{* Topological stuff lifted from and dropped to R                            *}
 
 
@@ -4164,10 +4183,8 @@
 lemma continuous_at_component: "continuous (at a) (\<lambda>x. x $ i)"
 unfolding continuous_at by (intro tendsto_intros)
 
-lemma continuous_on_component:
-  fixes s :: "('a::metric_space ^ 'n) set" (* TODO: generalize *)
-  shows "continuous_on s (\<lambda>x. x $ i)"
-unfolding continuous_on by (intro ballI tendsto_intros)
+lemma continuous_on_component: "continuous_on s (\<lambda>x. x $ i)"
+unfolding continuous_on_def by (intro ballI tendsto_intros)
 
 lemma continuous_at_infnorm: "continuous (at x) infnorm"
   unfolding continuous_at Lim_at o_def unfolding dist_norm
@@ -4275,79 +4292,7 @@
   thus ?thesis by fastsimp
 qed
 
-subsection{* We can now extend limit compositions to consider the scalar multiplier.   *}
-
-lemma Lim_mul:
-  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
-  assumes "(c ---> d) net"  "(f ---> l) net"
-  shows "((\<lambda>x. c(x) *\<^sub>R f x) ---> (d *\<^sub>R l)) net"
-  using assms by (rule scaleR.tendsto)
-
-lemma Lim_vmul:
-  fixes c :: "'a \<Rightarrow> real" and v :: "'b::real_normed_vector"
-  shows "(c ---> d) net ==> ((\<lambda>x. c(x) *\<^sub>R v) ---> d *\<^sub>R v) net"
-  by (intro tendsto_intros)
-
-lemmas Lim_intros = Lim_add Lim_const Lim_sub Lim_cmul Lim_vmul Lim_within_id
-
-lemma continuous_vmul:
-  fixes c :: "'a::metric_space \<Rightarrow> real" and v :: "'b::real_normed_vector"
-  shows "continuous net c ==> continuous net (\<lambda>x. c(x) *\<^sub>R v)"
-  unfolding continuous_def using Lim_vmul[of c] by auto
-
-lemma continuous_mul:
-  fixes c :: "'a::metric_space \<Rightarrow> real"
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
-  shows "continuous net c \<Longrightarrow> continuous net f
-             ==> continuous net (\<lambda>x. c(x) *\<^sub>R f x) "
-  unfolding continuous_def by (intro tendsto_intros)
-
-lemmas continuous_intros = continuous_add continuous_vmul continuous_cmul continuous_const continuous_sub continuous_at_id continuous_within_id continuous_mul
-
-lemma continuous_on_vmul:
-  fixes c :: "'a::metric_space \<Rightarrow> real" and v :: "'b::real_normed_vector"
-  shows "continuous_on s c ==> continuous_on s (\<lambda>x. c(x) *\<^sub>R v)"
-  unfolding continuous_on_eq_continuous_within using continuous_vmul[of _ c] by auto
-
-lemma continuous_on_mul:
-  fixes c :: "'a::metric_space \<Rightarrow> real"
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
-  shows "continuous_on s c \<Longrightarrow> continuous_on s f
-             ==> continuous_on s (\<lambda>x. c(x) *\<^sub>R f x)"
-  unfolding continuous_on_eq_continuous_within using continuous_mul[of _ c] by auto
-
-lemmas continuous_on_intros = continuous_on_add continuous_on_const continuous_on_id continuous_on_compose continuous_on_cmul continuous_on_neg continuous_on_sub
-  uniformly_continuous_on_add uniformly_continuous_on_const uniformly_continuous_on_id uniformly_continuous_on_compose uniformly_continuous_on_cmul uniformly_continuous_on_neg uniformly_continuous_on_sub
-  continuous_on_mul continuous_on_vmul
-
-text{* And so we have continuity of inverse.                                     *}
-
-lemma Lim_inv:
-  fixes f :: "'a \<Rightarrow> real"
-  assumes "(f ---> l) (net::'a net)"  "l \<noteq> 0"
-  shows "((inverse o f) ---> inverse l) net"
-  unfolding o_def using assms by (rule tendsto_inverse)
-
-lemma continuous_inv:
-  fixes f :: "'a::metric_space \<Rightarrow> real"
-  shows "continuous net f \<Longrightarrow> f(netlimit net) \<noteq> 0
-           ==> continuous net (inverse o f)"
-  unfolding continuous_def using Lim_inv by auto
-
-lemma continuous_at_within_inv:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_field"
-  assumes "continuous (at a within s) f" "f a \<noteq> 0"
-  shows "continuous (at a within s) (inverse o f)"
-  using assms unfolding continuous_within o_def
-  by (intro tendsto_intros)
-
-lemma continuous_at_inv:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_field"
-  shows "continuous (at a) f \<Longrightarrow> f a \<noteq> 0
-         ==> continuous (at a) (inverse o f) "
-  using within_UNIV[THEN sym, of "at a"] using continuous_at_within_inv[of a UNIV] by auto
-
-subsection{* Preservation properties for pasted sets.                                  *}
+subsection {* Pasted sets *}
 
 lemma bounded_pastecart:
   fixes s :: "('a::real_normed_vector ^ _) set" (* FIXME: generalize to metric_space *)
@@ -4710,7 +4655,7 @@
     by (auto simp add: dist_commute)
 qed
 
-(* A cute way of denoting open and closed intervals using overloading.       *)
+subsection {* Intervals *}
 
 lemma interval: fixes a :: "'a::ord^'n" shows
   "{a <..< b} = {x::'a^'n. \<forall>i. a$i < x$i \<and> x$i < b$i}" and
@@ -4722,20 +4667,6 @@
   "x \<in> {a .. b} \<longleftrightarrow> (\<forall>i. a$i \<le> x$i \<and> x$i \<le> b$i)"
   using interval[of a b] by(auto simp add: expand_set_eq vector_less_def vector_le_def)
 
-lemma mem_interval_1: fixes x :: "real^1" shows
- "(x \<in> {a .. b} \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b)"
- "(x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)"
-by(simp_all add: Cart_eq vector_less_def vector_le_def)
-
-lemma vec1_interval:fixes a::"real" shows
-  "vec1 ` {a .. b} = {vec1 a .. vec1 b}"
-  "vec1 ` {a<..<b} = {vec1 a<..<vec1 b}"
-  apply(rule_tac[!] set_ext) unfolding image_iff vector_less_def unfolding mem_interval
-  unfolding forall_1 unfolding vec1_dest_vec1_simps
-  apply rule defer apply(rule_tac x="dest_vec1 x" in bexI) prefer 3 apply rule defer
-  apply(rule_tac x="dest_vec1 x" in bexI) by auto
-
-
 lemma interval_eq_empty: fixes a :: "real^'n" shows
  "({a <..< b} = {} \<longleftrightarrow> (\<exists>i. b$i \<le> a$i))" (is ?th1) and
  "({a  ..  b} = {} \<longleftrightarrow> (\<exists>i. b$i < a$i))" (is ?th2)
@@ -4918,10 +4849,7 @@
 qed
 
 lemma open_interval_real[intro]: fixes a :: "real" shows "open {a<..<b}"
-  using open_interval[of "vec1 a" "vec1 b"] unfolding open_contains_ball
-  apply-apply(rule,erule_tac x="vec1 x" in ballE) apply(erule exE,rule_tac x=e in exI)
-  unfolding subset_eq mem_ball apply(rule) defer apply(rule,erule conjE,erule_tac x="vec1 xa" in ballE)
-  by(auto simp add: dist_vec1 dist_real_def vector_less_def)
+  by (rule open_real_greaterThanLessThan)
 
 lemma closed_interval[intro]: fixes a :: "real^'n" shows "closed {a .. b}"
 proof-
@@ -5112,56 +5040,6 @@
   unfolding closure_open_interval[OF assms, THEN sym] unfolding open_inter_closure_eq_empty[OF open_interval] ..
 
 
-(* Some special cases for intervals in R^1.                                  *)
-
-lemma interval_cases_1: fixes x :: "real^1" shows
- "x \<in> {a .. b} ==> x \<in> {a<..<b} \<or> (x = a) \<or> (x = b)"
-  unfolding Cart_eq vector_less_def vector_le_def mem_interval by(auto simp del:dest_vec1_eq)
-
-lemma in_interval_1: fixes x :: "real^1" shows
- "(x \<in> {a .. b} \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b) \<and>
-  (x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)"
-  unfolding Cart_eq vector_less_def vector_le_def mem_interval by(auto simp del:dest_vec1_eq)
-
-lemma interval_eq_empty_1: fixes a :: "real^1" shows
-  "{a .. b} = {} \<longleftrightarrow> dest_vec1 b < dest_vec1 a"
-  "{a<..<b} = {} \<longleftrightarrow> dest_vec1 b \<le> dest_vec1 a"
-  unfolding interval_eq_empty and ex_1 by auto
-
-lemma subset_interval_1: fixes a :: "real^1" shows
- "({a .. b} \<subseteq> {c .. d} \<longleftrightarrow>  dest_vec1 b < dest_vec1 a \<or>
-                dest_vec1 c \<le> dest_vec1 a \<and> dest_vec1 a \<le> dest_vec1 b \<and> dest_vec1 b \<le> dest_vec1 d)"
- "({a .. b} \<subseteq> {c<..<d} \<longleftrightarrow>  dest_vec1 b < dest_vec1 a \<or>
-                dest_vec1 c < dest_vec1 a \<and> dest_vec1 a \<le> dest_vec1 b \<and> dest_vec1 b < dest_vec1 d)"
- "({a<..<b} \<subseteq> {c .. d} \<longleftrightarrow>  dest_vec1 b \<le> dest_vec1 a \<or>
-                dest_vec1 c \<le> dest_vec1 a \<and> dest_vec1 a < dest_vec1 b \<and> dest_vec1 b \<le> dest_vec1 d)"
- "({a<..<b} \<subseteq> {c<..<d} \<longleftrightarrow> dest_vec1 b \<le> dest_vec1 a \<or>
-                dest_vec1 c \<le> dest_vec1 a \<and> dest_vec1 a < dest_vec1 b \<and> dest_vec1 b \<le> dest_vec1 d)"
-  unfolding subset_interval[of a b c d] unfolding forall_1 by auto
-
-lemma eq_interval_1: fixes a :: "real^1" shows
- "{a .. b} = {c .. d} \<longleftrightarrow>
-          dest_vec1 b < dest_vec1 a \<and> dest_vec1 d < dest_vec1 c \<or>
-          dest_vec1 a = dest_vec1 c \<and> dest_vec1 b = dest_vec1 d"
-unfolding set_eq_subset[of "{a .. b}" "{c .. d}"]
-unfolding subset_interval_1(1)[of a b c d]
-unfolding subset_interval_1(1)[of c d a b]
-by auto
-
-lemma disjoint_interval_1: fixes a :: "real^1" shows
-  "{a .. b} \<inter> {c .. d} = {} \<longleftrightarrow> dest_vec1 b < dest_vec1 a \<or> dest_vec1 d < dest_vec1 c  \<or>  dest_vec1 b < dest_vec1 c \<or> dest_vec1 d < dest_vec1 a"
-  "{a .. b} \<inter> {c<..<d} = {} \<longleftrightarrow> dest_vec1 b < dest_vec1 a \<or> dest_vec1 d \<le> dest_vec1 c  \<or>  dest_vec1 b \<le> dest_vec1 c \<or> dest_vec1 d \<le> dest_vec1 a"
-  "{a<..<b} \<inter> {c .. d} = {} \<longleftrightarrow> dest_vec1 b \<le> dest_vec1 a \<or> dest_vec1 d < dest_vec1 c  \<or>  dest_vec1 b \<le> dest_vec1 c \<or> dest_vec1 d \<le> dest_vec1 a"
-  "{a<..<b} \<inter> {c<..<d} = {} \<longleftrightarrow> dest_vec1 b \<le> dest_vec1 a \<or> dest_vec1 d \<le> dest_vec1 c  \<or>  dest_vec1 b \<le> dest_vec1 c \<or> dest_vec1 d \<le> dest_vec1 a"
-  unfolding disjoint_interval and ex_1 by auto
-
-lemma open_closed_interval_1: fixes a :: "real^1" shows
- "{a<..<b} = {a .. b} - {a, b}"
-  unfolding expand_set_eq apply simp unfolding vector_less_def and vector_le_def and forall_1 and dest_vec1_eq[THEN sym] by(auto simp del:dest_vec1_eq)
-
-lemma closed_open_interval_1: "dest_vec1 (a::real^1) \<le> dest_vec1 b ==> {a .. b} = {a<..<b} \<union> {a,b}"
-  unfolding expand_set_eq apply simp unfolding vector_less_def and vector_le_def and forall_1 and dest_vec1_eq[THEN sym] by(auto simp del:dest_vec1_eq)
-
 (* Some stuff for half-infinite intervals too; FIXME: notation?  *)
 
 lemma closed_interval_left: fixes b::"real^'n"
@@ -5188,7 +5066,7 @@
   thus ?thesis unfolding closed_limpt unfolding islimpt_approachable by blast
 qed
 
-subsection{* Intervals in general, including infinite and mixtures of open and closed. *}
+text {* Intervals in general, including infinite and mixtures of open and closed. *}
 
 definition "is_interval s \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i. ((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)"
 
@@ -5295,14 +5173,6 @@
   shows "l$i = b"
   using ev[unfolded order_eq_iff eventually_and] using Lim_component_ge[OF net, of b i] and Lim_component_le[OF net, of i b] by auto
 
-lemma Lim_drop_le: fixes f :: "'a \<Rightarrow> real^1" shows
-  "(f ---> l) net \<Longrightarrow> ~(trivial_limit net) \<Longrightarrow> eventually (\<lambda>x. dest_vec1 (f x) \<le> b) net ==> dest_vec1 l \<le> b"
-  using Lim_component_le[of f l net 1 b] by auto
-
-lemma Lim_drop_ge: fixes f :: "'a \<Rightarrow> real^1" shows
- "(f ---> l) net \<Longrightarrow> ~(trivial_limit net) \<Longrightarrow> eventually (\<lambda>x. b \<le> dest_vec1 (f x)) net ==> b \<le> dest_vec1 l"
-  using Lim_component_ge[of f l net b 1] by auto
-
 text{* Limits relative to a union.                                               *}
 
 lemma eventually_within_Un:
@@ -5317,15 +5187,19 @@
   unfolding tendsto_def
   by (auto simp add: eventually_within_Un)
 
+lemma Lim_topological:
+ "(f ---> l) net \<longleftrightarrow>
+        trivial_limit net \<or>
+        (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net)"
+  unfolding tendsto_def trivial_limit_eq by auto
+
 lemma continuous_on_union:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
   assumes "closed s" "closed t" "continuous_on s f" "continuous_on t f"
   shows "continuous_on (s \<union> t) f"
-  using assms unfolding continuous_on unfolding Lim_within_union
-  unfolding Lim unfolding trivial_limit_within unfolding closed_limpt by auto
+  using assms unfolding continuous_on Lim_within_union
+  unfolding Lim_topological trivial_limit_within closed_limpt by auto
 
 lemma continuous_on_cases:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
   assumes "closed s" "closed t" "continuous_on s f" "continuous_on t g"
           "\<forall>x. (x\<in>s \<and> \<not> P x) \<or> (x \<in> t \<and> P x) \<longrightarrow> f x = g x"
   shows "continuous_on (s \<union> t) (\<lambda>x. if P x then f x else g x)"
@@ -5359,23 +5233,7 @@
  "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)"
   using connected_ivt_hyperplane[of s x y "(basis k)::real^'n" a] by (auto simp add: inner_basis)
 
-text{* Also more convenient formulations of monotone convergence.                *}
-
-lemma bounded_increasing_convergent: fixes s::"nat \<Rightarrow> real^1"
-  assumes "bounded {s n| n::nat. True}"  "\<forall>n. dest_vec1(s n) \<le> dest_vec1(s(Suc n))"
-  shows "\<exists>l. (s ---> l) sequentially"
-proof-
-  obtain a where a:"\<forall>n. \<bar>dest_vec1 (s n)\<bar> \<le>  a" using assms(1)[unfolded bounded_iff abs_dest_vec1] by auto
-  { fix m::nat
-    have "\<And> n. n\<ge>m \<longrightarrow> dest_vec1 (s m) \<le> dest_vec1 (s n)"
-      apply(induct_tac n) apply simp using assms(2) apply(erule_tac x="na" in allE) by(auto simp add: not_less_eq_eq)  }
-  hence "\<forall>m n. m \<le> n \<longrightarrow> dest_vec1 (s m) \<le> dest_vec1 (s n)" by auto
-  then obtain l where "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<bar>dest_vec1 (s n) - l\<bar> < e" using convergent_bounded_monotone[OF a] unfolding monoseq_def by auto
-  thus ?thesis unfolding Lim_sequentially apply(rule_tac x="vec1 l" in exI)
-    unfolding dist_norm unfolding abs_dest_vec1  by auto
-qed
-
-subsection{* Basic homeomorphism definitions.                                          *}
+subsection {* Homeomorphisms *}
 
 definition "homeomorphism s t f g \<equiv>
      (\<forall>x\<in>s. (g(f x) = x)) \<and> (f ` s = t) \<and> continuous_on s f \<and>
@@ -5431,13 +5289,7 @@
 apply(erule_tac x="f x" in ballE) apply(erule_tac x="x" in ballE)
 apply auto apply(rule_tac x="f x" in bexI) by auto
 
-subsection{* Relatively weak hypotheses if a set is compact.                           *}
-
-definition "inv_on f s = (\<lambda>x. SOME y. y\<in>s \<and> f y = x)"
-
-lemma assumes "inj_on f s" "x\<in>s"
-  shows "inv_on f s (f x) = x"
- using assms unfolding inj_on_def inv_on_def by auto
+text {* Relatively weak hypotheses if a set is compact. *}
 
 lemma homeomorphism_compact:
   fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel"
@@ -5772,7 +5624,7 @@
   thus ?thesis using dim_subset[OF closure_subset, of s] by auto
 qed
 
-text{* Affine transformations of intervals.                                      *}
+subsection {* Affine transformations of intervals *}
 
 lemma affinity_inverses:
   assumes m0: "m \<noteq> (0::'a::field)"
diff -r cc8db7295249 -r 027879c5637d src/HOL/Multivariate_Analysis/Vec1.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Multivariate_Analysis/Vec1.thy	Tue Apr 27 11:17:50 2010 -0700
@@ -0,0 +1,404 @@
+(*  Title:      Multivariate_Analysis/Vec1.thy
+    Author:     Amine Chaieb, University of Cambridge
+    Author:     Robert Himmelmann, TU Muenchen
+*)
+
+header {* Vectors of size 1, 2, or 3 *}
+
+theory Vec1
+imports Topology_Euclidean_Space
+begin
+
+text{* Some common special cases.*}
+
+lemma forall_1[simp]: "(\<forall>i::1. P i) \<longleftrightarrow> P 1"
+  by (metis num1_eq_iff)
+
+lemma ex_1[simp]: "(\<exists>x::1. P x) \<longleftrightarrow> P 1"
+  by auto (metis num1_eq_iff)
+
+lemma exhaust_2:
+  fixes x :: 2 shows "x = 1 \<or> x = 2"
+proof (induct x)
+  case (of_int z)
+  then have "0 <= z" and "z < 2" by simp_all
+  then have "z = 0 | z = 1" by arith
+  then show ?case by auto
+qed
+
+lemma forall_2: "(\<forall>i::2. P i) \<longleftrightarrow> P 1 \<and> P 2"
+  by (metis exhaust_2)
+
+lemma exhaust_3:
+  fixes x :: 3 shows "x = 1 \<or> x = 2 \<or> x = 3"
+proof (induct x)
+  case (of_int z)
+  then have "0 <= z" and "z < 3" by simp_all
+  then have "z = 0 \<or> z = 1 \<or> z = 2" by arith
+  then show ?case by auto
+qed
+
+lemma forall_3: "(\<forall>i::3. P i) \<longleftrightarrow> P 1 \<and> P 2 \<and> P 3"
+  by (metis exhaust_3)
+
+lemma UNIV_1 [simp]: "UNIV = {1::1}"
+  by (auto simp add: num1_eq_iff)
+
+lemma UNIV_2: "UNIV = {1::2, 2::2}"
+  using exhaust_2 by auto
+
+lemma UNIV_3: "UNIV = {1::3, 2::3, 3::3}"
+  using exhaust_3 by auto
+
+lemma setsum_1: "setsum f (UNIV::1 set) = f 1"
+  unfolding UNIV_1 by simp
+
+lemma setsum_2: "setsum f (UNIV::2 set) = f 1 + f 2"
+  unfolding UNIV_2 by simp
+
+lemma setsum_3: "setsum f (UNIV::3 set) = f 1 + f 2 + f 3"
+  unfolding UNIV_3 by (simp add: add_ac)
+
+instantiation num1 :: cart_one begin
+instance proof
+  show "CARD(1) = Suc 0" by auto
+qed end
+
+(* "lift" from 'a to 'a^1 and "drop" from 'a^1 to 'a -- FIXME: potential use of transfer *)
+
+abbreviation vec1:: "'a \<Rightarrow> 'a ^ 1" where "vec1 x \<equiv> vec x"
+
+abbreviation dest_vec1:: "'a ^1 \<Rightarrow> 'a"
+  where "dest_vec1 x \<equiv> (x$1)"
+
+lemma vec1_component[simp]: "(vec1 x)$1 = x"
+  by simp
+
+lemma vec1_dest_vec1: "vec1(dest_vec1 x) = x" "dest_vec1(vec1 y) = y"
+  by (simp_all add:  Cart_eq)
+
+declare vec1_dest_vec1(1) [simp]
+
+lemma forall_vec1: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (vec1 x))"
+  by (metis vec1_dest_vec1(1))
+
+lemma exists_vec1: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P(vec1 x))"
+  by (metis vec1_dest_vec1(1))
+
+lemma vec1_eq[simp]:  "vec1 x = vec1 y \<longleftrightarrow> x = y"
+  by (metis vec1_dest_vec1(2))
+
+lemma dest_vec1_eq[simp]: "dest_vec1 x = dest_vec1 y \<longleftrightarrow> x = y"
+  by (metis vec1_dest_vec1(1))
+
+subsection{* The collapse of the general concepts to dimension one. *}
+
+lemma vector_one: "(x::'a ^1) = (\<chi> i. (x$1))"
+  by (simp add: Cart_eq)
+
+lemma forall_one: "(\<forall>(x::'a ^1). P x) \<longleftrightarrow> (\<forall>x. P(\<chi> i. x))"
+  apply auto
+  apply (erule_tac x= "x$1" in allE)
+  apply (simp only: vector_one[symmetric])
+  done
+
+lemma norm_vector_1: "norm (x :: _^1) = norm (x$1)"
+  by (simp add: norm_vector_def)
+
+lemma norm_real: "norm(x::real ^ 1) = abs(x$1)"
+  by (simp add: norm_vector_1)
+
+lemma dist_real: "dist(x::real ^ 1) y = abs((x$1) - (y$1))"
+  by (auto simp add: norm_real dist_norm)
+
+subsection{* Explicit vector construction from lists. *}
+
+primrec from_nat :: "nat \<Rightarrow> 'a::{monoid_add,one}"
+where "from_nat 0 = 0" | "from_nat (Suc n) = 1 + from_nat n"
+
+lemma from_nat [simp]: "from_nat = of_nat"
+by (rule ext, induct_tac x, simp_all)
+
+primrec
+  list_fun :: "nat \<Rightarrow> _ list \<Rightarrow> _ \<Rightarrow> _"
+where
+  "list_fun n [] = (\<lambda>x. 0)"
+| "list_fun n (x # xs) = fun_upd (list_fun (Suc n) xs) (from_nat n) x"
+
+definition "vector l = (\<chi> i. list_fun 1 l i)"
+(*definition "vector l = (\<chi> i. if i <= length l then l ! (i - 1) else 0)"*)
+
+lemma vector_1: "(vector[x]) $1 = x"
+  unfolding vector_def by simp
+
+lemma vector_2:
+ "(vector[x,y]) $1 = x"
+ "(vector[x,y] :: 'a^2)$2 = (y::'a::zero)"
+  unfolding vector_def by simp_all
+
+lemma vector_3:
+ "(vector [x,y,z] ::('a::zero)^3)$1 = x"
+ "(vector [x,y,z] ::('a::zero)^3)$2 = y"
+ "(vector [x,y,z] ::('a::zero)^3)$3 = z"
+  unfolding vector_def by simp_all
+
+lemma forall_vector_1: "(\<forall>v::'a::zero^1. P v) \<longleftrightarrow> (\<forall>x. P(vector[x]))"
+  apply auto
+  apply (erule_tac x="v$1" in allE)
+  apply (subgoal_tac "vector [v$1] = v")
+  apply simp
+  apply (vector vector_def)
+  apply simp
+  done
+
+lemma forall_vector_2: "(\<forall>v::'a::zero^2. P v) \<longleftrightarrow> (\<forall>x y. P(vector[x, y]))"
+  apply auto
+  apply (erule_tac x="v$1" in allE)
+  apply (erule_tac x="v$2" in allE)
+  apply (subgoal_tac "vector [v$1, v$2] = v")
+  apply simp
+  apply (vector vector_def)
+  apply (simp add: forall_2)
+  done
+
+lemma forall_vector_3: "(\<forall>v::'a::zero^3. P v) \<longleftrightarrow> (\<forall>x y z. P(vector[x, y, z]))"
+  apply auto
+  apply (erule_tac x="v$1" in allE)
+  apply (erule_tac x="v$2" in allE)
+  apply (erule_tac x="v$3" in allE)
+  apply (subgoal_tac "vector [v$1, v$2, v$3] = v")
+  apply simp
+  apply (vector vector_def)
+  apply (simp add: forall_3)
+  done
+
+lemma range_vec1[simp]:"range vec1 = UNIV" apply(rule set_ext,rule) unfolding image_iff defer
+  apply(rule_tac x="dest_vec1 x" in bexI) by auto
+
+lemma dest_vec1_lambda: "dest_vec1(\<chi> i. x i) = x 1"
+  by (simp)
+
+lemma dest_vec1_vec: "dest_vec1(vec x) = x"
+  by (simp)
+
+lemma dest_vec1_sum: assumes fS: "finite S"
+  shows "dest_vec1(setsum f S) = setsum (dest_vec1 o f) S"
+  apply (induct rule: finite_induct[OF fS])
+  apply simp
+  apply auto
+  done
+
+lemma norm_vec1 [simp]: "norm(vec1 x) = abs(x)"
+  by (simp add: vec_def norm_real)
+
+lemma dist_vec1: "dist(vec1 x) (vec1 y) = abs(x - y)"
+  by (simp only: dist_real vec1_component)
+lemma abs_dest_vec1: "norm x = \<bar>dest_vec1 x\<bar>"
+  by (metis vec1_dest_vec1(1) norm_vec1)
+
+lemmas vec1_dest_vec1_simps = forall_vec1 vec_add[THEN sym] dist_vec1 vec_sub[THEN sym] vec1_dest_vec1 norm_vec1 vector_smult_component
+   vec1_eq vec_cmul[THEN sym] smult_conv_scaleR[THEN sym] o_def dist_real_def norm_vec1 real_norm_def
+
+lemma bounded_linear_vec1:"bounded_linear (vec1::real\<Rightarrow>real^1)"
+  unfolding bounded_linear_def additive_def bounded_linear_axioms_def 
+  unfolding smult_conv_scaleR[THEN sym] unfolding vec1_dest_vec1_simps
+  apply(rule conjI) defer apply(rule conjI) defer apply(rule_tac x=1 in exI) by auto
+
+lemma linear_vmul_dest_vec1:
+  fixes f:: "'a::semiring_1^_ \<Rightarrow> 'a^1"
+  shows "linear f \<Longrightarrow> linear (\<lambda>x. dest_vec1(f x) *s v)"
+  apply (rule linear_vmul_component)
+  by auto
+
+lemma linear_from_scalars:
+  assumes lf: "linear (f::'a::comm_ring_1 ^1 \<Rightarrow> 'a^_)"
+  shows "f = (\<lambda>x. dest_vec1 x *s column 1 (matrix f))"
+  apply (rule ext)
+  apply (subst matrix_works[OF lf, symmetric])
+  apply (auto simp add: Cart_eq matrix_vector_mult_def column_def mult_commute)
+  done
+
+lemma linear_to_scalars: assumes lf: "linear (f::real ^'n \<Rightarrow> real^1)"
+  shows "f = (\<lambda>x. vec1(row 1 (matrix f) \<bullet> x))"
+  apply (rule ext)
+  apply (subst matrix_works[OF lf, symmetric])
+  apply (simp add: Cart_eq matrix_vector_mult_def row_def inner_vector_def mult_commute)
+  done
+
+lemma dest_vec1_eq_0: "dest_vec1 x = 0 \<longleftrightarrow> x = 0"
+  by (simp add: dest_vec1_eq[symmetric])
+
+lemma setsum_scalars: assumes fS: "finite S"
+  shows "setsum f S = vec1 (setsum (dest_vec1 o f) S)"
+  unfolding vec_setsum[OF fS] by simp
+
+lemma dest_vec1_wlog_le: "(\<And>(x::'a::linorder ^ 1) y. P x y \<longleftrightarrow> P y x)  \<Longrightarrow> (\<And>x y. dest_vec1 x <= dest_vec1 y ==> P x y) \<Longrightarrow> P x y"
+  apply (cases "dest_vec1 x \<le> dest_vec1 y")
+  apply simp
+  apply (subgoal_tac "dest_vec1 y \<le> dest_vec1 x")
+  apply (auto)
+  done
+
+text{* Lifting and dropping *}
+
+lemma continuous_on_o_dest_vec1: fixes f::"real \<Rightarrow> 'a::real_normed_vector"
+  assumes "continuous_on {a..b::real} f" shows "continuous_on {vec1 a..vec1 b} (f o dest_vec1)"
+  using assms unfolding continuous_on_iff apply safe
+  apply(erule_tac x="x$1" in ballE,erule_tac x=e in allE) apply safe
+  apply(rule_tac x=d in exI) apply safe unfolding o_def dist_real_def dist_real 
+  apply(erule_tac x="dest_vec1 x'" in ballE) by(auto simp add:vector_le_def)
+
+lemma continuous_on_o_vec1: fixes f::"real^1 \<Rightarrow> 'a::real_normed_vector"
+  assumes "continuous_on {a..b} f" shows "continuous_on {dest_vec1 a..dest_vec1 b} (f o vec1)"
+  using assms unfolding continuous_on_iff apply safe
+  apply(erule_tac x="vec x" in ballE,erule_tac x=e in allE) apply safe
+  apply(rule_tac x=d in exI) apply safe unfolding o_def dist_real_def dist_real 
+  apply(erule_tac x="vec1 x'" in ballE) by(auto simp add:vector_le_def)
+
+lemma continuous_on_vec1:"continuous_on A (vec1::real\<Rightarrow>real^1)"
+  by(rule linear_continuous_on[OF bounded_linear_vec1])
+
+lemma mem_interval_1: fixes x :: "real^1" shows
+ "(x \<in> {a .. b} \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b)"
+ "(x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)"
+by(simp_all add: Cart_eq vector_less_def vector_le_def)
+
+lemma vec1_interval:fixes a::"real" shows
+  "vec1 ` {a .. b} = {vec1 a .. vec1 b}"
+  "vec1 ` {a<..<b} = {vec1 a<..<vec1 b}"
+  apply(rule_tac[!] set_ext) unfolding image_iff vector_less_def unfolding mem_interval
+  unfolding forall_1 unfolding vec1_dest_vec1_simps
+  apply rule defer apply(rule_tac x="dest_vec1 x" in bexI) prefer 3 apply rule defer
+  apply(rule_tac x="dest_vec1 x" in bexI) by auto
+
+(* Some special cases for intervals in R^1.                                  *)
+
+lemma interval_cases_1: fixes x :: "real^1" shows
+ "x \<in> {a .. b} ==> x \<in> {a<..<b} \<or> (x = a) \<or> (x = b)"
+  unfolding Cart_eq vector_less_def vector_le_def mem_interval by(auto simp del:dest_vec1_eq)
+
+lemma in_interval_1: fixes x :: "real^1" shows
+ "(x \<in> {a .. b} \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b) \<and>
+  (x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)"
+  unfolding Cart_eq vector_less_def vector_le_def mem_interval by(auto simp del:dest_vec1_eq)
+
+lemma interval_eq_empty_1: fixes a :: "real^1" shows
+  "{a .. b} = {} \<longleftrightarrow> dest_vec1 b < dest_vec1 a"
+  "{a<..<b} = {} \<longleftrightarrow> dest_vec1 b \<le> dest_vec1 a"
+  unfolding interval_eq_empty and ex_1 by auto
+
+lemma subset_interval_1: fixes a :: "real^1" shows
+ "({a .. b} \<subseteq> {c .. d} \<longleftrightarrow>  dest_vec1 b < dest_vec1 a \<or>
+                dest_vec1 c \<le> dest_vec1 a \<and> dest_vec1 a \<le> dest_vec1 b \<and> dest_vec1 b \<le> dest_vec1 d)"
+ "({a .. b} \<subseteq> {c<..<d} \<longleftrightarrow>  dest_vec1 b < dest_vec1 a \<or>
+                dest_vec1 c < dest_vec1 a \<and> dest_vec1 a \<le> dest_vec1 b \<and> dest_vec1 b < dest_vec1 d)"
+ "({a<..<b} \<subseteq> {c .. d} \<longleftrightarrow>  dest_vec1 b \<le> dest_vec1 a \<or>
+                dest_vec1 c \<le> dest_vec1 a \<and> dest_vec1 a < dest_vec1 b \<and> dest_vec1 b \<le> dest_vec1 d)"
+ "({a<..<b} \<subseteq> {c<..<d} \<longleftrightarrow> dest_vec1 b \<le> dest_vec1 a \<or>
+                dest_vec1 c \<le> dest_vec1 a \<and> dest_vec1 a < dest_vec1 b \<and> dest_vec1 b \<le> dest_vec1 d)"
+  unfolding subset_interval[of a b c d] unfolding forall_1 by auto
+
+lemma eq_interval_1: fixes a :: "real^1" shows
+ "{a .. b} = {c .. d} \<longleftrightarrow>
+          dest_vec1 b < dest_vec1 a \<and> dest_vec1 d < dest_vec1 c \<or>
+          dest_vec1 a = dest_vec1 c \<and> dest_vec1 b = dest_vec1 d"
+unfolding set_eq_subset[of "{a .. b}" "{c .. d}"]
+unfolding subset_interval_1(1)[of a b c d]
+unfolding subset_interval_1(1)[of c d a b]
+by auto
+
+lemma disjoint_interval_1: fixes a :: "real^1" shows
+  "{a .. b} \<inter> {c .. d} = {} \<longleftrightarrow> dest_vec1 b < dest_vec1 a \<or> dest_vec1 d < dest_vec1 c  \<or>  dest_vec1 b < dest_vec1 c \<or> dest_vec1 d < dest_vec1 a"
+  "{a .. b} \<inter> {c<..<d} = {} \<longleftrightarrow> dest_vec1 b < dest_vec1 a \<or> dest_vec1 d \<le> dest_vec1 c  \<or>  dest_vec1 b \<le> dest_vec1 c \<or> dest_vec1 d \<le> dest_vec1 a"
+  "{a<..<b} \<inter> {c .. d} = {} \<longleftrightarrow> dest_vec1 b \<le> dest_vec1 a \<or> dest_vec1 d < dest_vec1 c  \<or>  dest_vec1 b \<le> dest_vec1 c \<or> dest_vec1 d \<le> dest_vec1 a"
+  "{a<..<b} \<inter> {c<..<d} = {} \<longleftrightarrow> dest_vec1 b \<le> dest_vec1 a \<or> dest_vec1 d \<le> dest_vec1 c  \<or>  dest_vec1 b \<le> dest_vec1 c \<or> dest_vec1 d \<le> dest_vec1 a"
+  unfolding disjoint_interval and ex_1 by auto
+
+lemma open_closed_interval_1: fixes a :: "real^1" shows
+ "{a<..<b} = {a .. b} - {a, b}"
+  unfolding expand_set_eq apply simp unfolding vector_less_def and vector_le_def and forall_1 and dest_vec1_eq[THEN sym] by(auto simp del:dest_vec1_eq)
+
+lemma closed_open_interval_1: "dest_vec1 (a::real^1) \<le> dest_vec1 b ==> {a .. b} = {a<..<b} \<union> {a,b}"
+  unfolding expand_set_eq apply simp unfolding vector_less_def and vector_le_def and forall_1 and dest_vec1_eq[THEN sym] by(auto simp del:dest_vec1_eq)
+
+lemma Lim_drop_le: fixes f :: "'a \<Rightarrow> real^1" shows
+  "(f ---> l) net \<Longrightarrow> ~(trivial_limit net) \<Longrightarrow> eventually (\<lambda>x. dest_vec1 (f x) \<le> b) net ==> dest_vec1 l \<le> b"
+  using Lim_component_le[of f l net 1 b] by auto
+
+lemma Lim_drop_ge: fixes f :: "'a \<Rightarrow> real^1" shows
+ "(f ---> l) net \<Longrightarrow> ~(trivial_limit net) \<Longrightarrow> eventually (\<lambda>x. b \<le> dest_vec1 (f x)) net ==> b \<le> dest_vec1 l"
+  using Lim_component_ge[of f l net b 1] by auto
+
+text{* Also more convenient formulations of monotone convergence.                *}
+
+lemma bounded_increasing_convergent: fixes s::"nat \<Rightarrow> real^1"
+  assumes "bounded {s n| n::nat. True}"  "\<forall>n. dest_vec1(s n) \<le> dest_vec1(s(Suc n))"
+  shows "\<exists>l. (s ---> l) sequentially"
+proof-
+  obtain a where a:"\<forall>n. \<bar>dest_vec1 (s n)\<bar> \<le>  a" using assms(1)[unfolded bounded_iff abs_dest_vec1] by auto
+  { fix m::nat
+    have "\<And> n. n\<ge>m \<longrightarrow> dest_vec1 (s m) \<le> dest_vec1 (s n)"
+      apply(induct_tac n) apply simp using assms(2) apply(erule_tac x="na" in allE) by(auto simp add: not_less_eq_eq)  }
+  hence "\<forall>m n. m \<le> n \<longrightarrow> dest_vec1 (s m) \<le> dest_vec1 (s n)" by auto
+  then obtain l where "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<bar>dest_vec1 (s n) - l\<bar> < e" using convergent_bounded_monotone[OF a] unfolding monoseq_def by auto
+  thus ?thesis unfolding Lim_sequentially apply(rule_tac x="vec1 l" in exI)
+    unfolding dist_norm unfolding abs_dest_vec1  by auto
+qed
+
+lemma dest_vec1_simps[simp]: fixes a::"real^1"
+  shows "a$1 = 0 \<longleftrightarrow> a = 0" (*"a \<le> 1 \<longleftrightarrow> dest_vec1 a \<le> 1" "0 \<le> a \<longleftrightarrow> 0 \<le> dest_vec1 a"*)
+  "a \<le> b \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 b" "dest_vec1 (1::real^1) = 1"
+  by(auto simp add: vector_le_def Cart_eq)
+
+lemma dest_vec1_inverval:
+  "dest_vec1 ` {a .. b} = {dest_vec1 a .. dest_vec1 b}"
+  "dest_vec1 ` {a<.. b} = {dest_vec1 a<.. dest_vec1 b}"
+  "dest_vec1 ` {a ..<b} = {dest_vec1 a ..<dest_vec1 b}"
+  "dest_vec1 ` {a<..<b} = {dest_vec1 a<..<dest_vec1 b}"
+  apply(rule_tac [!] equalityI)
+  unfolding subset_eq Ball_def Bex_def mem_interval_1 image_iff
+  apply(rule_tac [!] allI)apply(rule_tac [!] impI)
+  apply(rule_tac[2] x="vec1 x" in exI)apply(rule_tac[4] x="vec1 x" in exI)
+  apply(rule_tac[6] x="vec1 x" in exI)apply(rule_tac[8] x="vec1 x" in exI)
+  by (auto simp add: vector_less_def vector_le_def)
+
+lemma dest_vec1_setsum: assumes "finite S"
+  shows " dest_vec1 (setsum f S) = setsum (\<lambda>x. dest_vec1 (f x)) S"
+  using dest_vec1_sum[OF assms] by auto
+
+lemma open_dest_vec1_vimage: "open S \<Longrightarrow> open (dest_vec1 -` S)"
+unfolding open_vector_def forall_1 by auto
+
+lemma tendsto_dest_vec1 [tendsto_intros]:
+  "(f ---> l) net \<Longrightarrow> ((\<lambda>x. dest_vec1 (f x)) ---> dest_vec1 l) net"
+by(rule tendsto_Cart_nth)
+
+lemma continuous_dest_vec1: "continuous net f \<Longrightarrow> continuous net (\<lambda>x. dest_vec1 (f x))"
+  unfolding continuous_def by (rule tendsto_dest_vec1)
+
+lemma forall_dest_vec1: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P(dest_vec1 x))" 
+  apply safe defer apply(erule_tac x="vec1 x" in allE) by auto
+
+lemma forall_of_dest_vec1: "(\<forall>v. P (\<lambda>x. dest_vec1 (v x))) \<longleftrightarrow> (\<forall>x. P x)"
+  apply rule apply rule apply(erule_tac x="(vec1 \<circ> x)" in allE) unfolding o_def vec1_dest_vec1 by auto 
+
+lemma forall_of_dest_vec1': "(\<forall>v. P (dest_vec1 v)) \<longleftrightarrow> (\<forall>x. P x)"
+  apply rule apply rule apply(erule_tac x="(vec1 x)" in allE) defer apply rule 
+  apply(erule_tac x="dest_vec1 v" in allE) unfolding o_def vec1_dest_vec1 by auto
+
+lemma dist_vec1_0[simp]: "dist(vec1 (x::real)) 0 = norm x" unfolding vector_dist_norm by auto
+
+lemma bounded_linear_vec1_dest_vec1: fixes f::"real \<Rightarrow> real"
+  shows "linear (vec1 \<circ> f \<circ> dest_vec1) = bounded_linear f" (is "?l = ?r") proof-
+  { assume ?l guess K using linear_bounded[OF `?l`] ..
+    hence "\<exists>K. \<forall>x. \<bar>f x\<bar> \<le> \<bar>x\<bar> * K" apply(rule_tac x=K in exI)
+      unfolding vec1_dest_vec1_simps by (auto simp add:field_simps) }
+  thus ?thesis unfolding linear_def bounded_linear_def additive_def bounded_linear_axioms_def o_def
+    unfolding vec1_dest_vec1_simps by auto qed
+
+lemma vec1_le[simp]:fixes a::real shows "vec1 a \<le> vec1 b \<longleftrightarrow> a \<le> b"
+  unfolding vector_le_def by auto
+lemma vec1_less[simp]:fixes a::real shows "vec1 a < vec1 b \<longleftrightarrow> a < b"
+  unfolding vector_less_def by auto
+
+end