src/HOL/Multivariate_Analysis/Fashoda.thy
author hoelzl
Fri Feb 19 13:40:50 2016 +0100 (2016-02-19)
changeset 62378 85ed00c1fe7c
parent 61945 1135b8de26c3
child 62397 5ae24f33d343
permissions -rw-r--r--
generalize more theorems to support enat and ennreal
     1 (*  Author:     John Harrison
     2     Author:     Robert Himmelmann, TU Muenchen (translation from HOL light)
     3 *)
     4 
     5 section \<open>Fashoda meet theorem\<close>
     6 
     7 theory Fashoda
     8 imports Brouwer_Fixpoint Path_Connected Cartesian_Euclidean_Space
     9 begin
    10 
    11 (* move *)
    12 
    13 lemma cart_eq_inner_axis: "a $ i = a \<bullet> axis i 1"
    14   by (simp add: inner_axis)
    15 
    16 lemma axis_in_Basis: "a \<in> Basis \<Longrightarrow> axis i a \<in> Basis"
    17   by (auto simp add: Basis_vec_def axis_eq_axis)
    18 
    19 subsection \<open>Bijections between intervals.\<close>
    20 
    21 definition interval_bij :: "'a \<times> 'a \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<Rightarrow> 'a::euclidean_space"
    22   where "interval_bij =
    23     (\<lambda>(a, b) (u, v) x. (\<Sum>i\<in>Basis. (u\<bullet>i + (x\<bullet>i - a\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (v\<bullet>i - u\<bullet>i)) *\<^sub>R i))"
    24 
    25 lemma interval_bij_affine:
    26   "interval_bij (a,b) (u,v) = (\<lambda>x. (\<Sum>i\<in>Basis. ((v\<bullet>i - u\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (x\<bullet>i)) *\<^sub>R i) +
    27     (\<Sum>i\<in>Basis. (u\<bullet>i - (v\<bullet>i - u\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (a\<bullet>i)) *\<^sub>R i))"
    28   by (auto simp: setsum.distrib[symmetric] scaleR_add_left[symmetric] interval_bij_def fun_eq_iff
    29     field_simps inner_simps add_divide_distrib[symmetric] intro!: setsum.cong)
    30 
    31 lemma continuous_interval_bij:
    32   fixes a b :: "'a::euclidean_space"
    33   shows "continuous (at x) (interval_bij (a, b) (u, v))"
    34   by (auto simp add: divide_inverse interval_bij_def intro!: continuous_setsum continuous_intros)
    35 
    36 lemma continuous_on_interval_bij: "continuous_on s (interval_bij (a, b) (u, v))"
    37   apply(rule continuous_at_imp_continuous_on)
    38   apply (rule, rule continuous_interval_bij)
    39   done
    40 
    41 lemma in_interval_interval_bij:
    42   fixes a b u v x :: "'a::euclidean_space"
    43   assumes "x \<in> cbox a b"
    44     and "cbox u v \<noteq> {}"
    45   shows "interval_bij (a, b) (u, v) x \<in> cbox u v"
    46   apply (simp only: interval_bij_def split_conv mem_box inner_setsum_left_Basis cong: ball_cong)
    47   apply safe
    48 proof -
    49   fix i :: 'a
    50   assume i: "i \<in> Basis"
    51   have "cbox a b \<noteq> {}"
    52     using assms by auto
    53   with i have *: "a\<bullet>i \<le> b\<bullet>i" "u\<bullet>i \<le> v\<bullet>i"
    54     using assms(2) by (auto simp add: box_eq_empty)
    55   have x: "a\<bullet>i\<le>x\<bullet>i" "x\<bullet>i\<le>b\<bullet>i"
    56     using assms(1)[unfolded mem_box] using i by auto
    57   have "0 \<le> (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i)"
    58     using * x by auto
    59   then show "u \<bullet> i \<le> u \<bullet> i + (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i)"
    60     using * by auto
    61   have "((x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i)) * (v \<bullet> i - u \<bullet> i) \<le> 1 * (v \<bullet> i - u \<bullet> i)"
    62     apply (rule mult_right_mono)
    63     unfolding divide_le_eq_1
    64     using * x
    65     apply auto
    66     done
    67   then show "u \<bullet> i + (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i) \<le> v \<bullet> i"
    68     using * by auto
    69 qed
    70 
    71 lemma interval_bij_bij:
    72   "\<forall>(i::'a::euclidean_space)\<in>Basis. a\<bullet>i < b\<bullet>i \<and> u\<bullet>i < v\<bullet>i \<Longrightarrow>
    73     interval_bij (a, b) (u, v) (interval_bij (u, v) (a, b) x) = x"
    74   by (auto simp: interval_bij_def euclidean_eq_iff[where 'a='a])
    75 
    76 lemma interval_bij_bij_cart: fixes x::"real^'n" assumes "\<forall>i. a$i < b$i \<and> u$i < v$i" 
    77   shows "interval_bij (a,b) (u,v) (interval_bij (u,v) (a,b) x) = x"
    78   using assms by (intro interval_bij_bij) (auto simp: Basis_vec_def inner_axis)
    79 
    80 
    81 subsection \<open>Fashoda meet theorem\<close>
    82 
    83 lemma infnorm_2:
    84   fixes x :: "real^2"
    85   shows "infnorm x = max \<bar>x$1\<bar> \<bar>x$2\<bar>"
    86   unfolding infnorm_cart UNIV_2 by (rule cSup_eq) auto
    87 
    88 lemma infnorm_eq_1_2:
    89   fixes x :: "real^2"
    90   shows "infnorm x = 1 \<longleftrightarrow>
    91     \<bar>x$1\<bar> \<le> 1 \<and> \<bar>x$2\<bar> \<le> 1 \<and> (x$1 = -1 \<or> x$1 = 1 \<or> x$2 = -1 \<or> x$2 = 1)"
    92   unfolding infnorm_2 by auto
    93 
    94 lemma infnorm_eq_1_imp:
    95   fixes x :: "real^2"
    96   assumes "infnorm x = 1"
    97   shows "\<bar>x$1\<bar> \<le> 1" and "\<bar>x$2\<bar> \<le> 1"
    98   using assms unfolding infnorm_eq_1_2 by auto
    99 
   100 lemma fashoda_unit:
   101   fixes f g :: "real \<Rightarrow> real^2"
   102   assumes "f ` {-1 .. 1} \<subseteq> cbox (-1) 1"
   103     and "g ` {-1 .. 1} \<subseteq> cbox (-1) 1"
   104     and "continuous_on {-1 .. 1} f"
   105     and "continuous_on {-1 .. 1} g"
   106     and "f (- 1)$1 = - 1"
   107     and "f 1$1 = 1" "g (- 1) $2 = -1"
   108     and "g 1 $2 = 1"
   109   shows "\<exists>s\<in>{-1 .. 1}. \<exists>t\<in>{-1 .. 1}. f s = g t"
   110 proof (rule ccontr)
   111   assume "\<not> ?thesis"
   112   note as = this[unfolded bex_simps,rule_format]
   113   def sqprojection \<equiv> "\<lambda>z::real^2. (inverse (infnorm z)) *\<^sub>R z" 
   114   def negatex \<equiv> "\<lambda>x::real^2. (vector [-(x$1), x$2])::real^2"
   115   have lem1: "\<forall>z::real^2. infnorm (negatex z) = infnorm z"
   116     unfolding negatex_def infnorm_2 vector_2 by auto
   117   have lem2: "\<forall>z. z \<noteq> 0 \<longrightarrow> infnorm (sqprojection z) = 1"
   118     unfolding sqprojection_def
   119     unfolding infnorm_mul[unfolded scalar_mult_eq_scaleR]
   120     unfolding abs_inverse real_abs_infnorm
   121     apply (subst infnorm_eq_0[symmetric])
   122     apply auto
   123     done
   124   let ?F = "\<lambda>w::real^2. (f \<circ> (\<lambda>x. x$1)) w - (g \<circ> (\<lambda>x. x$2)) w"
   125   have *: "\<And>i. (\<lambda>x::real^2. x $ i) ` cbox (- 1) 1 = {-1 .. 1}"
   126     apply (rule set_eqI)
   127     unfolding image_iff Bex_def mem_interval_cart interval_cbox_cart
   128     apply rule
   129     defer
   130     apply (rule_tac x="vec x" in exI)
   131     apply auto
   132     done
   133   {
   134     fix x
   135     assume "x \<in> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w) ` (cbox (- 1) (1::real^2))"
   136     then obtain w :: "real^2" where w:
   137         "w \<in> cbox (- 1) 1"
   138         "x = (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w"
   139       unfolding image_iff ..
   140     then have "x \<noteq> 0"
   141       using as[of "w$1" "w$2"]
   142       unfolding mem_interval_cart atLeastAtMost_iff
   143       by auto
   144   } note x0 = this
   145   have 21: "\<And>i::2. i \<noteq> 1 \<Longrightarrow> i = 2"
   146     using UNIV_2 by auto
   147   have 1: "box (- 1) (1::real^2) \<noteq> {}"
   148     unfolding interval_eq_empty_cart by auto
   149   have 2: "continuous_on (cbox (- 1) 1) (negatex \<circ> sqprojection \<circ> ?F)"
   150     apply (intro continuous_intros continuous_on_component)
   151     unfolding *
   152     apply (rule assms)+
   153     apply (subst sqprojection_def)
   154     apply (intro continuous_intros)
   155     apply (simp add: infnorm_eq_0 x0)
   156     apply (rule linear_continuous_on)
   157   proof -
   158     show "bounded_linear negatex"
   159       apply (rule bounded_linearI')
   160       unfolding vec_eq_iff
   161     proof (rule_tac[!] allI)
   162       fix i :: 2
   163       fix x y :: "real^2"
   164       fix c :: real
   165       show "negatex (x + y) $ i =
   166         (negatex x + negatex y) $ i" "negatex (c *\<^sub>R x) $ i = (c *\<^sub>R negatex x) $ i"
   167         apply -
   168         apply (case_tac[!] "i\<noteq>1")
   169         prefer 3
   170         apply (drule_tac[1-2] 21) 
   171         unfolding negatex_def
   172         apply (auto simp add:vector_2)
   173         done
   174     qed
   175   qed
   176   have 3: "(negatex \<circ> sqprojection \<circ> ?F) ` cbox (-1) 1 \<subseteq> cbox (-1) 1"
   177     unfolding subset_eq
   178   proof (rule, goal_cases)
   179     case (1 x)
   180     then obtain y :: "real^2" where y:
   181         "y \<in> cbox (- 1) 1"
   182         "x = (negatex \<circ> sqprojection \<circ> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w)) y"
   183       unfolding image_iff ..
   184     have "?F y \<noteq> 0"
   185       apply (rule x0)
   186       using y(1)
   187       apply auto
   188       done
   189     then have *: "infnorm (sqprojection (?F y)) = 1"
   190       unfolding y o_def
   191       by - (rule lem2[rule_format])
   192     have "infnorm x = 1"
   193       unfolding *[symmetric] y o_def
   194       by (rule lem1[rule_format])
   195     then show "x \<in> cbox (-1) 1"
   196       unfolding mem_interval_cart interval_cbox_cart infnorm_2
   197       apply -
   198       apply rule
   199     proof -
   200       fix i
   201       assume "max \<bar>x $ 1\<bar> \<bar>x $ 2\<bar> = 1"
   202       then show "(- 1) $ i \<le> x $ i \<and> x $ i \<le> 1 $ i"
   203         apply (cases "i = 1")
   204         defer
   205         apply (drule 21)
   206         apply auto
   207         done
   208     qed
   209   qed
   210   obtain x :: "real^2" where x:
   211       "x \<in> cbox (- 1) 1"
   212       "(negatex \<circ> sqprojection \<circ> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w)) x = x"
   213     apply (rule brouwer_weak[of "cbox (- 1) (1::real^2)" "negatex \<circ> sqprojection \<circ> ?F"])
   214     apply (rule compact_cbox convex_box)+
   215     unfolding interior_cbox
   216     apply (rule 1 2 3)+
   217     apply blast
   218     done
   219   have "?F x \<noteq> 0"
   220     apply (rule x0)
   221     using x(1)
   222     apply auto
   223     done
   224   then have *: "infnorm (sqprojection (?F x)) = 1"
   225     unfolding o_def
   226     by (rule lem2[rule_format])
   227   have nx: "infnorm x = 1"
   228     apply (subst x(2)[symmetric])
   229     unfolding *[symmetric] o_def
   230     apply (rule lem1[rule_format])
   231     done
   232   have "\<forall>x i. x \<noteq> 0 \<longrightarrow> (0 < (sqprojection x)$i \<longleftrightarrow> 0 < x$i)"
   233     and "\<forall>x i. x \<noteq> 0 \<longrightarrow> ((sqprojection x)$i < 0 \<longleftrightarrow> x$i < 0)"
   234     apply -
   235     apply (rule_tac[!] allI impI)+
   236   proof -
   237     fix x :: "real^2"
   238     fix i :: 2
   239     assume x: "x \<noteq> 0"
   240     have "inverse (infnorm x) > 0"
   241       using x[unfolded infnorm_pos_lt[symmetric]] by auto
   242     then show "(0 < sqprojection x $ i) = (0 < x $ i)"
   243       and "(sqprojection x $ i < 0) = (x $ i < 0)"
   244       unfolding sqprojection_def vector_component_simps vector_scaleR_component real_scaleR_def
   245       unfolding zero_less_mult_iff mult_less_0_iff
   246       by (auto simp add: field_simps)
   247   qed
   248   note lem3 = this[rule_format]
   249   have x1: "x $ 1 \<in> {- 1..1::real}" "x $ 2 \<in> {- 1..1::real}"
   250     using x(1) unfolding mem_interval_cart by auto
   251   then have nz: "f (x $ 1) - g (x $ 2) \<noteq> 0"
   252     unfolding right_minus_eq
   253     apply -
   254     apply (rule as)
   255     apply auto
   256     done
   257   have "x $ 1 = -1 \<or> x $ 1 = 1 \<or> x $ 2 = -1 \<or> x $ 2 = 1"
   258     using nx unfolding infnorm_eq_1_2 by auto 
   259   then show False
   260   proof -
   261     fix P Q R S 
   262     presume "P \<or> Q \<or> R \<or> S"
   263       and "P \<Longrightarrow> False"
   264       and "Q \<Longrightarrow> False"
   265       and "R \<Longrightarrow> False"
   266       and "S \<Longrightarrow> False"
   267     then show False by auto
   268   next
   269     assume as: "x$1 = 1"
   270     then have *: "f (x $ 1) $ 1 = 1"
   271       using assms(6) by auto
   272     have "sqprojection (f (x$1) - g (x$2)) $ 1 < 0"
   273       using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]]
   274       unfolding as negatex_def vector_2
   275       by auto
   276     moreover
   277     from x1 have "g (x $ 2) \<in> cbox (-1) 1"
   278       apply -
   279       apply (rule assms(2)[unfolded subset_eq,rule_format])
   280       apply auto
   281       done
   282     ultimately show False
   283       unfolding lem3[OF nz] vector_component_simps * mem_interval_cart 
   284       apply (erule_tac x=1 in allE)
   285       apply auto
   286       done
   287   next
   288     assume as: "x$1 = -1"
   289     then have *: "f (x $ 1) $ 1 = - 1"
   290       using assms(5) by auto
   291     have "sqprojection (f (x$1) - g (x$2)) $ 1 > 0"
   292       using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]]
   293       unfolding as negatex_def vector_2
   294       by auto
   295     moreover
   296     from x1 have "g (x $ 2) \<in> cbox (-1) 1"
   297       apply -
   298       apply (rule assms(2)[unfolded subset_eq,rule_format])
   299       apply auto
   300       done
   301     ultimately show False
   302       unfolding lem3[OF nz] vector_component_simps * mem_interval_cart 
   303       apply (erule_tac x=1 in allE)
   304       apply auto
   305       done
   306   next
   307     assume as: "x$2 = 1"
   308     then have *: "g (x $ 2) $ 2 = 1"
   309       using assms(8) by auto
   310     have "sqprojection (f (x$1) - g (x$2)) $ 2 > 0"
   311       using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]]
   312       unfolding as negatex_def vector_2
   313       by auto
   314     moreover
   315     from x1 have "f (x $ 1) \<in> cbox (-1) 1"
   316       apply -
   317       apply (rule assms(1)[unfolded subset_eq,rule_format])
   318       apply auto
   319       done
   320     ultimately show False
   321       unfolding lem3[OF nz] vector_component_simps * mem_interval_cart
   322       apply (erule_tac x=2 in allE)
   323       apply auto
   324       done
   325   next
   326     assume as: "x$2 = -1"
   327     then have *: "g (x $ 2) $ 2 = - 1"
   328       using assms(7) by auto
   329     have "sqprojection (f (x$1) - g (x$2)) $ 2 < 0"
   330       using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]]
   331       unfolding as negatex_def vector_2
   332       by auto
   333     moreover
   334     from x1 have "f (x $ 1) \<in> cbox (-1) 1"
   335       apply -
   336       apply (rule assms(1)[unfolded subset_eq,rule_format])
   337       apply auto
   338       done
   339     ultimately show False
   340       unfolding lem3[OF nz] vector_component_simps * mem_interval_cart
   341       apply (erule_tac x=2 in allE)
   342       apply auto
   343       done
   344   qed auto
   345 qed
   346 
   347 lemma fashoda_unit_path:
   348   fixes f g :: "real \<Rightarrow> real^2"
   349   assumes "path f"
   350     and "path g"
   351     and "path_image f \<subseteq> cbox (-1) 1"
   352     and "path_image g \<subseteq> cbox (-1) 1"
   353     and "(pathstart f)$1 = -1"
   354     and "(pathfinish f)$1 = 1"
   355     and "(pathstart g)$2 = -1"
   356     and "(pathfinish g)$2 = 1"
   357   obtains z where "z \<in> path_image f" and "z \<in> path_image g"
   358 proof -
   359   note assms=assms[unfolded path_def pathstart_def pathfinish_def path_image_def]
   360   def iscale \<equiv> "\<lambda>z::real. inverse 2 *\<^sub>R (z + 1)"
   361   have isc: "iscale ` {- 1..1} \<subseteq> {0..1}"
   362     unfolding iscale_def by auto
   363   have "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. (f \<circ> iscale) s = (g \<circ> iscale) t"
   364   proof (rule fashoda_unit)
   365     show "(f \<circ> iscale) ` {- 1..1} \<subseteq> cbox (- 1) 1" "(g \<circ> iscale) ` {- 1..1} \<subseteq> cbox (- 1) 1"
   366       using isc and assms(3-4) by (auto simp add: image_comp [symmetric])
   367     have *: "continuous_on {- 1..1} iscale"
   368       unfolding iscale_def by (rule continuous_intros)+
   369     show "continuous_on {- 1..1} (f \<circ> iscale)" "continuous_on {- 1..1} (g \<circ> iscale)"
   370       apply -
   371       apply (rule_tac[!] continuous_on_compose[OF *])
   372       apply (rule_tac[!] continuous_on_subset[OF _ isc])
   373       apply (rule assms)+
   374       done
   375     have *: "(1 / 2) *\<^sub>R (1 + (1::real^1)) = 1"
   376       unfolding vec_eq_iff by auto
   377     show "(f \<circ> iscale) (- 1) $ 1 = - 1"
   378       and "(f \<circ> iscale) 1 $ 1 = 1"
   379       and "(g \<circ> iscale) (- 1) $ 2 = -1"
   380       and "(g \<circ> iscale) 1 $ 2 = 1"
   381       unfolding o_def iscale_def
   382       using assms
   383       by (auto simp add: *)
   384   qed
   385   then obtain s t where st:
   386       "s \<in> {- 1..1}"
   387       "t \<in> {- 1..1}"
   388       "(f \<circ> iscale) s = (g \<circ> iscale) t"
   389     by auto
   390   show thesis
   391     apply (rule_tac z = "f (iscale s)" in that)
   392     using st
   393     unfolding o_def path_image_def image_iff
   394     apply -
   395     apply (rule_tac x="iscale s" in bexI)
   396     prefer 3
   397     apply (rule_tac x="iscale t" in bexI)
   398     using isc[unfolded subset_eq, rule_format]
   399     apply auto
   400     done
   401 qed
   402 
   403 lemma fashoda:
   404   fixes b :: "real^2"
   405   assumes "path f"
   406     and "path g"
   407     and "path_image f \<subseteq> cbox a b"
   408     and "path_image g \<subseteq> cbox a b"
   409     and "(pathstart f)$1 = a$1"
   410     and "(pathfinish f)$1 = b$1"
   411     and "(pathstart g)$2 = a$2"
   412     and "(pathfinish g)$2 = b$2"
   413   obtains z where "z \<in> path_image f" and "z \<in> path_image g"
   414 proof -
   415   fix P Q S
   416   presume "P \<or> Q \<or> S" "P \<Longrightarrow> thesis" and "Q \<Longrightarrow> thesis" and "S \<Longrightarrow> thesis"
   417   then show thesis
   418     by auto
   419 next
   420   have "cbox a b \<noteq> {}"
   421     using assms(3) using path_image_nonempty[of f] by auto
   422   then have "a \<le> b"
   423     unfolding interval_eq_empty_cart less_eq_vec_def by (auto simp add: not_less)
   424   then show "a$1 = b$1 \<or> a$2 = b$2 \<or> (a$1 < b$1 \<and> a$2 < b$2)"
   425     unfolding less_eq_vec_def forall_2 by auto
   426 next
   427   assume as: "a$1 = b$1"
   428   have "\<exists>z\<in>path_image g. z$2 = (pathstart f)$2"
   429     apply (rule connected_ivt_component_cart)
   430     apply (rule connected_path_image assms)+
   431     apply (rule pathstart_in_path_image)
   432     apply (rule pathfinish_in_path_image)
   433     unfolding assms using assms(3)[unfolded path_image_def subset_eq,rule_format,of "f 0"]
   434     unfolding pathstart_def
   435     apply (auto simp add: less_eq_vec_def mem_interval_cart)
   436     done
   437   then obtain z :: "real^2" where z: "z \<in> path_image g" "z $ 2 = pathstart f $ 2" ..
   438   have "z \<in> cbox a b"
   439     using z(1) assms(4)
   440     unfolding path_image_def
   441     by blast
   442   then have "z = f 0"
   443     unfolding vec_eq_iff forall_2
   444     unfolding z(2) pathstart_def
   445     using assms(3)[unfolded path_image_def subset_eq mem_interval_cart,rule_format,of "f 0" 1]
   446     unfolding mem_interval_cart
   447     apply (erule_tac x=1 in allE)
   448     using as
   449     apply auto
   450     done
   451   then show thesis
   452     apply -
   453     apply (rule that[OF _ z(1)])
   454     unfolding path_image_def
   455     apply auto
   456     done
   457 next
   458   assume as: "a$2 = b$2"
   459   have "\<exists>z\<in>path_image f. z$1 = (pathstart g)$1"
   460     apply (rule connected_ivt_component_cart)
   461     apply (rule connected_path_image assms)+
   462     apply (rule pathstart_in_path_image)
   463     apply (rule pathfinish_in_path_image)
   464     unfolding assms
   465     using assms(4)[unfolded path_image_def subset_eq,rule_format,of "g 0"]
   466     unfolding pathstart_def
   467     apply (auto simp add: less_eq_vec_def mem_interval_cart)
   468     done
   469   then obtain z where z: "z \<in> path_image f" "z $ 1 = pathstart g $ 1" ..
   470   have "z \<in> cbox a b"
   471     using z(1) assms(3)
   472     unfolding path_image_def
   473     by blast
   474   then have "z = g 0"
   475     unfolding vec_eq_iff forall_2
   476     unfolding z(2) pathstart_def
   477     using assms(4)[unfolded path_image_def subset_eq mem_interval_cart,rule_format,of "g 0" 2]
   478     unfolding mem_interval_cart
   479     apply (erule_tac x=2 in allE)
   480     using as
   481     apply auto
   482     done
   483   then show thesis
   484     apply -
   485     apply (rule that[OF z(1)])
   486     unfolding path_image_def
   487     apply auto
   488     done
   489 next
   490   assume as: "a $ 1 < b $ 1 \<and> a $ 2 < b $ 2"
   491   have int_nem: "cbox (-1) (1::real^2) \<noteq> {}"
   492     unfolding interval_eq_empty_cart by auto
   493   obtain z :: "real^2" where z:
   494       "z \<in> (interval_bij (a, b) (- 1, 1) \<circ> f) ` {0..1}"
   495       "z \<in> (interval_bij (a, b) (- 1, 1) \<circ> g) ` {0..1}"
   496     apply (rule fashoda_unit_path[of "interval_bij (a,b) (- 1,1) \<circ> f" "interval_bij (a,b) (- 1,1) \<circ> g"]) 
   497     unfolding path_def path_image_def pathstart_def pathfinish_def
   498     apply (rule_tac[1-2] continuous_on_compose)
   499     apply (rule assms[unfolded path_def] continuous_on_interval_bij)+
   500     unfolding subset_eq
   501     apply(rule_tac[1-2] ballI)
   502   proof -
   503     fix x
   504     assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> f) ` {0..1}"
   505     then obtain y where y:
   506         "y \<in> {0..1}"
   507         "x = (interval_bij (a, b) (- 1, 1) \<circ> f) y"
   508       unfolding image_iff ..
   509     show "x \<in> cbox (- 1) 1"
   510       unfolding y o_def
   511       apply (rule in_interval_interval_bij)
   512       using y(1)
   513       using assms(3)[unfolded path_image_def subset_eq] int_nem
   514       apply auto
   515       done
   516   next
   517     fix x
   518     assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> g) ` {0..1}"
   519     then obtain y where y:
   520         "y \<in> {0..1}"
   521         "x = (interval_bij (a, b) (- 1, 1) \<circ> g) y"
   522       unfolding image_iff ..
   523     show "x \<in> cbox (- 1) 1"
   524       unfolding y o_def
   525       apply (rule in_interval_interval_bij)
   526       using y(1)
   527       using assms(4)[unfolded path_image_def subset_eq] int_nem
   528       apply auto
   529       done
   530   next
   531     show "(interval_bij (a, b) (- 1, 1) \<circ> f) 0 $ 1 = -1"
   532       and "(interval_bij (a, b) (- 1, 1) \<circ> f) 1 $ 1 = 1"
   533       and "(interval_bij (a, b) (- 1, 1) \<circ> g) 0 $ 2 = -1"
   534       and "(interval_bij (a, b) (- 1, 1) \<circ> g) 1 $ 2 = 1"
   535       using assms as
   536       by (simp_all add: axis_in_Basis cart_eq_inner_axis pathstart_def pathfinish_def interval_bij_def)
   537          (simp_all add: inner_axis)
   538   qed
   539   from z(1) obtain zf where zf:
   540       "zf \<in> {0..1}"
   541       "z = (interval_bij (a, b) (- 1, 1) \<circ> f) zf"
   542     unfolding image_iff ..
   543   from z(2) obtain zg where zg:
   544       "zg \<in> {0..1}"
   545       "z = (interval_bij (a, b) (- 1, 1) \<circ> g) zg"
   546     unfolding image_iff ..
   547   have *: "\<forall>i. (- 1) $ i < (1::real^2) $ i \<and> a $ i < b $ i"
   548     unfolding forall_2
   549     using as
   550     by auto
   551   show thesis
   552     apply (rule_tac z="interval_bij (- 1,1) (a,b) z" in that)
   553     apply (subst zf)
   554     defer
   555     apply (subst zg)
   556     unfolding o_def interval_bij_bij_cart[OF *] path_image_def
   557     using zf(1) zg(1)
   558     apply auto
   559     done
   560 qed
   561 
   562 
   563 subsection \<open>Some slightly ad hoc lemmas I use below\<close>
   564 
   565 lemma segment_vertical:
   566   fixes a :: "real^2"
   567   assumes "a$1 = b$1"
   568   shows "x \<in> closed_segment a b \<longleftrightarrow>
   569     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)"
   570   (is "_ = ?R")
   571 proof -
   572   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"
   573   {
   574     presume "?L \<Longrightarrow> ?R" and "?R \<Longrightarrow> ?L"
   575     then show ?thesis
   576       unfolding closed_segment_def mem_Collect_eq
   577       unfolding vec_eq_iff forall_2 scalar_mult_eq_scaleR[symmetric] vector_component_simps
   578       by blast
   579   }
   580   {
   581     assume ?L
   582     then obtain u where u:
   583         "x $ 1 = (1 - u) * a $ 1 + u * b $ 1"
   584         "x $ 2 = (1 - u) * a $ 2 + u * b $ 2"
   585         "0 \<le> u"
   586         "u \<le> 1"
   587       by blast
   588     { fix b a
   589       assume "b + u * a > a + u * b"
   590       then have "(1 - u) * b > (1 - u) * a"
   591         by (auto simp add:field_simps)
   592       then have "b \<ge> a"
   593         apply (drule_tac mult_left_less_imp_less)
   594         using u
   595         apply auto
   596         done
   597       then have "u * a \<le> u * b"
   598         apply -
   599         apply (rule mult_left_mono[OF _ u(3)]) 
   600         using u(3-4)
   601         apply (auto simp add: field_simps)
   602         done
   603     } note * = this
   604     {
   605       fix a b
   606       assume "u * b > u * a"
   607       then have "(1 - u) * a \<le> (1 - u) * b"
   608         apply -
   609         apply (rule mult_left_mono)
   610         apply (drule mult_left_less_imp_less)
   611         using u
   612         apply auto
   613         done
   614       then have "a + u * b \<le> b + u * a"
   615         by (auto simp add: field_simps)
   616     } note ** = this
   617     then show ?R
   618       unfolding u assms
   619       using u
   620       by (auto simp add:field_simps not_le intro: * **)
   621   }
   622   {
   623     assume ?R
   624     then show ?L
   625     proof (cases "x$2 = b$2")
   626       case True
   627       then show ?L
   628         apply (rule_tac x="(x$2 - a$2) / (b$2 - a$2)" in exI)
   629         unfolding assms True
   630         using \<open>?R\<close>
   631         apply (auto simp add: field_simps)
   632         done
   633     next
   634       case False
   635       then show ?L
   636         apply (rule_tac x="1 - (x$2 - b$2) / (a$2 - b$2)" in exI)
   637         unfolding assms
   638         using \<open>?R\<close>
   639         apply (auto simp add: field_simps)
   640         done
   641     qed
   642   }
   643 qed
   644 
   645 lemma segment_horizontal:
   646   fixes a :: "real^2"
   647   assumes "a$2 = b$2"
   648   shows "x \<in> closed_segment a b \<longleftrightarrow>
   649     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)"
   650   (is "_ = ?R")
   651 proof -
   652   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"
   653   {
   654     presume "?L \<Longrightarrow> ?R" and "?R \<Longrightarrow> ?L"
   655     then show ?thesis
   656       unfolding closed_segment_def mem_Collect_eq
   657       unfolding vec_eq_iff forall_2 scalar_mult_eq_scaleR[symmetric] vector_component_simps
   658       by blast
   659   }
   660   {
   661     assume ?L
   662     then obtain u where u:
   663         "x $ 1 = (1 - u) * a $ 1 + u * b $ 1"
   664         "x $ 2 = (1 - u) * a $ 2 + u * b $ 2"
   665         "0 \<le> u"
   666         "u \<le> 1"
   667       by blast
   668     {
   669       fix b a
   670       assume "b + u * a > a + u * b"
   671       then have "(1 - u) * b > (1 - u) * a"
   672         by (auto simp add: field_simps)
   673       then have "b \<ge> a"
   674         apply (drule_tac mult_left_less_imp_less)
   675         using u
   676         apply auto
   677         done
   678       then have "u * a \<le> u * b"
   679         apply -
   680         apply (rule mult_left_mono[OF _ u(3)])
   681         using u(3-4)
   682         apply (auto simp add: field_simps)
   683         done
   684     } note * = this
   685     {
   686       fix a b
   687       assume "u * b > u * a"
   688       then have "(1 - u) * a \<le> (1 - u) * b"
   689         apply -
   690         apply (rule mult_left_mono)
   691         apply (drule mult_left_less_imp_less)
   692         using u
   693         apply auto
   694         done
   695       then have "a + u * b \<le> b + u * a"
   696         by (auto simp add: field_simps)
   697     } note ** = this
   698     then show ?R
   699       unfolding u assms
   700       using u
   701       by (auto simp add: field_simps not_le intro: * **)
   702   }
   703   {
   704     assume ?R
   705     then show ?L
   706     proof (cases "x$1 = b$1")
   707       case True
   708       then show ?L
   709         apply (rule_tac x="(x$1 - a$1) / (b$1 - a$1)" in exI)
   710         unfolding assms True
   711         using \<open>?R\<close>
   712         apply (auto simp add: field_simps)
   713         done
   714     next
   715       case False
   716       then show ?L
   717         apply (rule_tac x="1 - (x$1 - b$1) / (a$1 - b$1)" in exI)
   718         unfolding assms
   719         using \<open>?R\<close>
   720         apply (auto simp add: field_simps)
   721         done
   722     qed
   723   }
   724 qed
   725 
   726 
   727 subsection \<open>Useful Fashoda corollary pointed out to me by Tom Hales\<close>
   728 
   729 lemma fashoda_interlace:
   730   fixes a :: "real^2"
   731   assumes "path f"
   732     and "path g"
   733     and "path_image f \<subseteq> cbox a b"
   734     and "path_image g \<subseteq> cbox a b"
   735     and "(pathstart f)$2 = a$2"
   736     and "(pathfinish f)$2 = a$2"
   737     and "(pathstart g)$2 = a$2"
   738     and "(pathfinish g)$2 = a$2"
   739     and "(pathstart f)$1 < (pathstart g)$1"
   740     and "(pathstart g)$1 < (pathfinish f)$1"
   741     and "(pathfinish f)$1 < (pathfinish g)$1"
   742   obtains z where "z \<in> path_image f" and "z \<in> path_image g"
   743 proof -
   744   have "cbox a b \<noteq> {}"
   745     using path_image_nonempty[of f] using assms(3) by auto
   746   note ab=this[unfolded interval_eq_empty_cart not_ex forall_2 not_less]
   747   have "pathstart f \<in> cbox a b"
   748     and "pathfinish f \<in> cbox a b"
   749     and "pathstart g \<in> cbox a b"
   750     and "pathfinish g \<in> cbox a b"
   751     using pathstart_in_path_image pathfinish_in_path_image
   752     using assms(3-4)
   753     by auto
   754   note startfin = this[unfolded mem_interval_cart forall_2]
   755   let ?P1 = "linepath (vector[a$1 - 2, a$2 - 2]) (vector[(pathstart f)$1,a$2 - 2]) +++
   756      linepath(vector[(pathstart f)$1,a$2 - 2])(pathstart f) +++ f +++
   757      linepath(pathfinish f)(vector[(pathfinish f)$1,a$2 - 2]) +++
   758      linepath(vector[(pathfinish f)$1,a$2 - 2])(vector[b$1 + 2,a$2 - 2])" 
   759   let ?P2 = "linepath(vector[(pathstart g)$1, (pathstart g)$2 - 3])(pathstart g) +++ g +++
   760      linepath(pathfinish g)(vector[(pathfinish g)$1,a$2 - 1]) +++
   761      linepath(vector[(pathfinish g)$1,a$2 - 1])(vector[b$1 + 1,a$2 - 1]) +++
   762      linepath(vector[b$1 + 1,a$2 - 1])(vector[b$1 + 1,b$2 + 3])"
   763   let ?a = "vector[a$1 - 2, a$2 - 3]"
   764   let ?b = "vector[b$1 + 2, b$2 + 3]"
   765   have P1P2: "path_image ?P1 = path_image (linepath (vector[a$1 - 2, a$2 - 2]) (vector[(pathstart f)$1,a$2 - 2])) \<union>
   766       path_image (linepath(vector[(pathstart f)$1,a$2 - 2])(pathstart f)) \<union> path_image f \<union>
   767       path_image (linepath(pathfinish f)(vector[(pathfinish f)$1,a$2 - 2])) \<union>
   768       path_image (linepath(vector[(pathfinish f)$1,a$2 - 2])(vector[b$1 + 2,a$2 - 2]))"
   769     "path_image ?P2 = path_image(linepath(vector[(pathstart g)$1, (pathstart g)$2 - 3])(pathstart g)) \<union> path_image g \<union>
   770       path_image(linepath(pathfinish g)(vector[(pathfinish g)$1,a$2 - 1])) \<union>
   771       path_image(linepath(vector[(pathfinish g)$1,a$2 - 1])(vector[b$1 + 1,a$2 - 1])) \<union>
   772       path_image(linepath(vector[b$1 + 1,a$2 - 1])(vector[b$1 + 1,b$2 + 3]))" using assms(1-2)
   773       by(auto simp add: path_image_join path_linepath)
   774   have abab: "cbox a b \<subseteq> cbox ?a ?b"
   775     unfolding interval_cbox_cart[symmetric]
   776     by (auto simp add:less_eq_vec_def forall_2 vector_2)
   777   obtain z where
   778     "z \<in> path_image
   779           (linepath (vector [a $ 1 - 2, a $ 2 - 2]) (vector [pathstart f $ 1, a $ 2 - 2]) +++
   780            linepath (vector [pathstart f $ 1, a $ 2 - 2]) (pathstart f) +++
   781            f +++
   782            linepath (pathfinish f) (vector [pathfinish f $ 1, a $ 2 - 2]) +++
   783            linepath (vector [pathfinish f $ 1, a $ 2 - 2]) (vector [b $ 1 + 2, a $ 2 - 2]))"
   784     "z \<in> path_image
   785           (linepath (vector [pathstart g $ 1, pathstart g $ 2 - 3]) (pathstart g) +++
   786            g +++
   787            linepath (pathfinish g) (vector [pathfinish g $ 1, a $ 2 - 1]) +++
   788            linepath (vector [pathfinish g $ 1, a $ 2 - 1]) (vector [b $ 1 + 1, a $ 2 - 1]) +++
   789            linepath (vector [b $ 1 + 1, a $ 2 - 1]) (vector [b $ 1 + 1, b $ 2 + 3]))"
   790     apply (rule fashoda[of ?P1 ?P2 ?a ?b])
   791     unfolding pathstart_join pathfinish_join pathstart_linepath pathfinish_linepath vector_2
   792   proof -
   793     show "path ?P1" and "path ?P2"
   794       using assms by auto
   795     have "path_image ?P1 \<subseteq> cbox ?a ?b"
   796       unfolding P1P2 path_image_linepath
   797       apply (rule Un_least)+
   798       defer 3
   799       apply (rule_tac[1-4] convex_box(1)[unfolded convex_contains_segment,rule_format])
   800       unfolding mem_interval_cart forall_2 vector_2
   801       using ab startfin abab assms(3)
   802       using assms(9-)
   803       unfolding assms
   804       apply (auto simp add: field_simps box_def)
   805       done
   806     then show "path_image ?P1 \<subseteq> cbox ?a ?b" .
   807     have "path_image ?P2 \<subseteq> cbox ?a ?b"
   808       unfolding P1P2 path_image_linepath
   809       apply (rule Un_least)+
   810       defer 2
   811       apply (rule_tac[1-4] convex_box(1)[unfolded convex_contains_segment,rule_format])
   812       unfolding mem_interval_cart forall_2 vector_2
   813       using ab startfin abab assms(4)
   814       using assms(9-)
   815       unfolding assms
   816       apply (auto simp add: field_simps box_def)
   817       done
   818     then show "path_image ?P2 \<subseteq> cbox ?a ?b" .
   819     show "a $ 1 - 2 = a $ 1 - 2"
   820       and "b $ 1 + 2 = b $ 1 + 2"
   821       and "pathstart g $ 2 - 3 = a $ 2 - 3"
   822       and "b $ 2 + 3 = b $ 2 + 3"
   823       by (auto simp add: assms)
   824   qed
   825   note z=this[unfolded P1P2 path_image_linepath]
   826   show thesis
   827     apply (rule that[of z])
   828   proof -
   829     have "(z \<in> closed_segment (vector [a $ 1 - 2, a $ 2 - 2]) (vector [pathstart f $ 1, a $ 2 - 2]) \<or>
   830       z \<in> closed_segment (vector [pathstart f $ 1, a $ 2 - 2]) (pathstart f)) \<or>
   831       z \<in> closed_segment (pathfinish f) (vector [pathfinish f $ 1, a $ 2 - 2]) \<or>
   832       z \<in> closed_segment (vector [pathfinish f $ 1, a $ 2 - 2]) (vector [b $ 1 + 2, a $ 2 - 2]) \<Longrightarrow>
   833     (((z \<in> closed_segment (vector [pathstart g $ 1, pathstart g $ 2 - 3]) (pathstart g)) \<or>
   834       z \<in> closed_segment (pathfinish g) (vector [pathfinish g $ 1, a $ 2 - 1])) \<or>
   835       z \<in> closed_segment (vector [pathfinish g $ 1, a $ 2 - 1]) (vector [b $ 1 + 1, a $ 2 - 1])) \<or>
   836       z \<in> closed_segment (vector [b $ 1 + 1, a $ 2 - 1]) (vector [b $ 1 + 1, b $ 2 + 3]) \<Longrightarrow> False"
   837     proof (simp only: segment_vertical segment_horizontal vector_2, goal_cases)
   838       case prems: 1
   839       have "pathfinish f \<in> cbox a b"
   840         using assms(3) pathfinish_in_path_image[of f] by auto 
   841       then have "1 + b $ 1 \<le> pathfinish f $ 1 \<Longrightarrow> False"
   842         unfolding mem_interval_cart forall_2 by auto
   843       then have "z$1 \<noteq> pathfinish f$1"
   844         using prems(2)
   845         using assms ab
   846         by (auto simp add: field_simps)
   847       moreover have "pathstart f \<in> cbox a b"
   848         using assms(3) pathstart_in_path_image[of f]
   849         by auto
   850       then have "1 + b $ 1 \<le> pathstart f $ 1 \<Longrightarrow> False"
   851         unfolding mem_interval_cart forall_2
   852         by auto
   853       then have "z$1 \<noteq> pathstart f$1"
   854         using prems(2) using assms ab
   855         by (auto simp add: field_simps)
   856       ultimately have *: "z$2 = a$2 - 2"
   857         using prems(1)
   858         by auto
   859       have "z$1 \<noteq> pathfinish g$1"
   860         using prems(2)
   861         using assms ab
   862         by (auto simp add: field_simps *)
   863       moreover have "pathstart g \<in> cbox a b"
   864         using assms(4) pathstart_in_path_image[of g]
   865         by auto 
   866       note this[unfolded mem_interval_cart forall_2]
   867       then have "z$1 \<noteq> pathstart g$1"
   868         using prems(1)
   869         using assms ab
   870         by (auto simp add: field_simps *)
   871       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"
   872         using prems(2)
   873         unfolding * assms
   874         by (auto simp add: field_simps)
   875       then show False
   876         unfolding * using ab by auto
   877     qed
   878     then have "z \<in> path_image f \<or> z \<in> path_image g"
   879       using z unfolding Un_iff by blast
   880     then have z': "z \<in> cbox a b"
   881       using assms(3-4)
   882       by auto
   883     have "a $ 2 = z $ 2 \<Longrightarrow> (z $ 1 = pathstart f $ 1 \<or> z $ 1 = pathfinish f $ 1) \<Longrightarrow>
   884       z = pathstart f \<or> z = pathfinish f"
   885       unfolding vec_eq_iff forall_2 assms
   886       by auto
   887     with z' show "z \<in> path_image f"
   888       using z(1)
   889       unfolding Un_iff mem_interval_cart forall_2
   890       apply -
   891       apply (simp only: segment_vertical segment_horizontal vector_2)
   892       unfolding assms
   893       apply auto
   894       done
   895     have "a $ 2 = z $ 2 \<Longrightarrow> (z $ 1 = pathstart g $ 1 \<or> z $ 1 = pathfinish g $ 1) \<Longrightarrow>
   896       z = pathstart g \<or> z = pathfinish g"
   897       unfolding vec_eq_iff forall_2 assms
   898       by auto
   899     with z' show "z \<in> path_image g"
   900       using z(2)
   901       unfolding Un_iff mem_interval_cart forall_2
   902       apply (simp only: segment_vertical segment_horizontal vector_2)
   903       unfolding assms
   904       apply auto
   905       done
   906   qed
   907 qed
   908 
   909 (** The Following still needs to be translated. Maybe I will do that later.
   910 
   911 (* ------------------------------------------------------------------------- *)
   912 (* Complement in dimension N >= 2 of set homeomorphic to any interval in     *)
   913 (* any dimension is (path-)connected. This naively generalizes the argument  *)
   914 (* in Ryuji Maehara's paper "The Jordan curve theorem via the Brouwer        *)
   915 (* fixed point theorem", American Mathematical Monthly 1984.                 *)
   916 (* ------------------------------------------------------------------------- *)
   917 
   918 let RETRACTION_INJECTIVE_IMAGE_INTERVAL = prove
   919  (`!p:real^M->real^N a b.
   920         ~(interval[a,b] = {}) /\
   921         p continuous_on interval[a,b] /\
   922         (!x y. x IN interval[a,b] /\ y IN interval[a,b] /\ p x = p y ==> x = y)
   923         ==> ?f. f continuous_on (:real^N) /\
   924                 IMAGE f (:real^N) SUBSET (IMAGE p (interval[a,b])) /\
   925                 (!x. x IN (IMAGE p (interval[a,b])) ==> f x = x)`,
   926   REPEAT STRIP_TAC THEN
   927   FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [INJECTIVE_ON_LEFT_INVERSE]) THEN
   928   DISCH_THEN(X_CHOOSE_TAC `q:real^N->real^M`) THEN
   929   SUBGOAL_THEN `(q:real^N->real^M) continuous_on
   930                 (IMAGE p (interval[a:real^M,b]))`
   931   ASSUME_TAC THENL
   932    [MATCH_MP_TAC CONTINUOUS_ON_INVERSE THEN ASM_REWRITE_TAC[COMPACT_INTERVAL];
   933     ALL_TAC] THEN
   934   MP_TAC(ISPECL [`q:real^N->real^M`;
   935                  `IMAGE (p:real^M->real^N)
   936                  (interval[a,b])`;
   937                  `a:real^M`; `b:real^M`]
   938         TIETZE_CLOSED_INTERVAL) THEN
   939   ASM_SIMP_TAC[COMPACT_INTERVAL; COMPACT_CONTINUOUS_IMAGE;
   940                COMPACT_IMP_CLOSED] THEN
   941   ANTS_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
   942   DISCH_THEN(X_CHOOSE_THEN `r:real^N->real^M` STRIP_ASSUME_TAC) THEN
   943   EXISTS_TAC `(p:real^M->real^N) o (r:real^N->real^M)` THEN
   944   REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; o_THM; IN_UNIV] THEN
   945   CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
   946   MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN ASM_REWRITE_TAC[] THEN
   947   FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP(REWRITE_RULE[IMP_CONJ]
   948         CONTINUOUS_ON_SUBSET)) THEN ASM SET_TAC[]);;
   949 
   950 let UNBOUNDED_PATH_COMPONENTS_COMPLEMENT_HOMEOMORPHIC_INTERVAL = prove
   951  (`!s:real^N->bool a b:real^M.
   952         s homeomorphic (interval[a,b])
   953         ==> !x. ~(x IN s) ==> ~bounded(path_component((:real^N) DIFF s) x)`,
   954   REPEAT GEN_TAC THEN REWRITE_TAC[homeomorphic; homeomorphism] THEN
   955   REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
   956   MAP_EVERY X_GEN_TAC [`p':real^N->real^M`; `p:real^M->real^N`] THEN
   957   DISCH_TAC THEN
   958   SUBGOAL_THEN
   959    `!x y. x IN interval[a,b] /\ y IN interval[a,b] /\
   960           (p:real^M->real^N) x = p y ==> x = y`
   961   ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
   962   FIRST_X_ASSUM(MP_TAC o funpow 4 CONJUNCT2) THEN
   963   DISCH_THEN(CONJUNCTS_THEN2 (SUBST1_TAC o SYM) ASSUME_TAC) THEN
   964   ASM_CASES_TAC `interval[a:real^M,b] = {}` THEN
   965   ASM_REWRITE_TAC[IMAGE_CLAUSES; DIFF_EMPTY; PATH_COMPONENT_UNIV;
   966                   NOT_BOUNDED_UNIV] THEN
   967   ABBREV_TAC `s = (:real^N) DIFF (IMAGE p (interval[a:real^M,b]))` THEN
   968   X_GEN_TAC `c:real^N` THEN REPEAT STRIP_TAC THEN
   969   SUBGOAL_THEN `(c:real^N) IN s` ASSUME_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
   970   SUBGOAL_THEN `bounded((path_component s c) UNION
   971                         (IMAGE (p:real^M->real^N) (interval[a,b])))`
   972   MP_TAC THENL
   973    [ASM_SIMP_TAC[BOUNDED_UNION; COMPACT_IMP_BOUNDED; COMPACT_IMP_BOUNDED;
   974                  COMPACT_CONTINUOUS_IMAGE; COMPACT_INTERVAL];
   975     ALL_TAC] THEN
   976   DISCH_THEN(MP_TAC o SPEC `c:real^N` o MATCH_MP BOUNDED_SUBSET_BALL) THEN
   977   REWRITE_TAC[UNION_SUBSET] THEN
   978   DISCH_THEN(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC) THEN
   979   MP_TAC(ISPECL [`p:real^M->real^N`; `a:real^M`; `b:real^M`]
   980     RETRACTION_INJECTIVE_IMAGE_INTERVAL) THEN
   981   ASM_REWRITE_TAC[SUBSET; IN_UNIV] THEN
   982   DISCH_THEN(X_CHOOSE_THEN `r:real^N->real^N` MP_TAC) THEN
   983   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC
   984    (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC)) THEN
   985   REWRITE_TAC[FORALL_IN_IMAGE; IN_UNIV] THEN DISCH_TAC THEN
   986   ABBREV_TAC `q = \z:real^N. if z IN path_component s c then r(z) else z` THEN
   987   SUBGOAL_THEN
   988     `(q:real^N->real^N) continuous_on
   989      (closure(path_component s c) UNION ((:real^N) DIFF (path_component s c)))`
   990   MP_TAC THENL
   991    [EXPAND_TAC "q" THEN MATCH_MP_TAC CONTINUOUS_ON_CASES THEN
   992     REWRITE_TAC[CLOSED_CLOSURE; CONTINUOUS_ON_ID; GSYM OPEN_CLOSED] THEN
   993     REPEAT CONJ_TAC THENL
   994      [MATCH_MP_TAC OPEN_PATH_COMPONENT THEN EXPAND_TAC "s" THEN
   995       ASM_SIMP_TAC[GSYM CLOSED_OPEN; COMPACT_IMP_CLOSED;
   996                    COMPACT_CONTINUOUS_IMAGE; COMPACT_INTERVAL];
   997       ASM_MESON_TAC[CONTINUOUS_ON_SUBSET; SUBSET_UNIV];
   998       ALL_TAC] THEN
   999     X_GEN_TAC `z:real^N` THEN
  1000     REWRITE_TAC[SET_RULE `~(z IN (s DIFF t) /\ z IN t)`] THEN
  1001     STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
  1002     MP_TAC(ISPECL
  1003      [`path_component s (z:real^N)`; `path_component s (c:real^N)`]
  1004      OPEN_INTER_CLOSURE_EQ_EMPTY) THEN
  1005     ASM_REWRITE_TAC[GSYM DISJOINT; PATH_COMPONENT_DISJOINT] THEN ANTS_TAC THENL
  1006      [MATCH_MP_TAC OPEN_PATH_COMPONENT THEN EXPAND_TAC "s" THEN
  1007       ASM_SIMP_TAC[GSYM CLOSED_OPEN; COMPACT_IMP_CLOSED;
  1008                    COMPACT_CONTINUOUS_IMAGE; COMPACT_INTERVAL];
  1009       REWRITE_TAC[DISJOINT; EXTENSION; IN_INTER; NOT_IN_EMPTY] THEN
  1010       DISCH_THEN(MP_TAC o SPEC `z:real^N`) THEN ASM_REWRITE_TAC[] THEN
  1011       GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [IN] THEN
  1012       REWRITE_TAC[PATH_COMPONENT_REFL_EQ] THEN ASM SET_TAC[]];
  1013     ALL_TAC] THEN
  1014   SUBGOAL_THEN
  1015    `closure(path_component s c) UNION ((:real^N) DIFF (path_component s c)) =
  1016     (:real^N)`
  1017   SUBST1_TAC THENL
  1018    [MATCH_MP_TAC(SET_RULE `s SUBSET t ==> t UNION (UNIV DIFF s) = UNIV`) THEN
  1019     REWRITE_TAC[CLOSURE_SUBSET];
  1020     DISCH_TAC] THEN
  1021   MP_TAC(ISPECL
  1022    [`(\x. &2 % c - x) o
  1023      (\x. c + B / norm(x - c) % (x - c)) o (q:real^N->real^N)`;
  1024     `cball(c:real^N,B)`]
  1025     BROUWER) THEN
  1026   REWRITE_TAC[NOT_IMP; GSYM CONJ_ASSOC; COMPACT_CBALL; CONVEX_CBALL] THEN
  1027   ASM_SIMP_TAC[CBALL_EQ_EMPTY; REAL_LT_IMP_LE; REAL_NOT_LT] THEN
  1028   SUBGOAL_THEN `!x. ~((q:real^N->real^N) x = c)` ASSUME_TAC THENL
  1029    [X_GEN_TAC `x:real^N` THEN EXPAND_TAC "q" THEN
  1030     REWRITE_TAC[NORM_EQ_0; VECTOR_SUB_EQ] THEN COND_CASES_TAC THEN
  1031     ASM SET_TAC[PATH_COMPONENT_REFL_EQ];
  1032     ALL_TAC] THEN
  1033   REPEAT CONJ_TAC THENL
  1034    [MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
  1035     SIMP_TAC[CONTINUOUS_ON_SUB; CONTINUOUS_ON_ID; CONTINUOUS_ON_CONST] THEN
  1036     MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN CONJ_TAC THENL
  1037      [ASM_MESON_TAC[CONTINUOUS_ON_SUBSET; SUBSET_UNIV]; ALL_TAC] THEN
  1038     MATCH_MP_TAC CONTINUOUS_ON_ADD THEN REWRITE_TAC[CONTINUOUS_ON_CONST] THEN
  1039     MATCH_MP_TAC CONTINUOUS_ON_MUL THEN
  1040     SIMP_TAC[CONTINUOUS_ON_SUB; CONTINUOUS_ON_ID; CONTINUOUS_ON_CONST] THEN
  1041     REWRITE_TAC[o_DEF; real_div; LIFT_CMUL] THEN
  1042     MATCH_MP_TAC CONTINUOUS_ON_CMUL THEN
  1043     MATCH_MP_TAC(REWRITE_RULE[o_DEF] CONTINUOUS_ON_INV) THEN
  1044     ASM_REWRITE_TAC[FORALL_IN_IMAGE; NORM_EQ_0; VECTOR_SUB_EQ] THEN
  1045     SUBGOAL_THEN
  1046      `(\x:real^N. lift(norm(x - c))) = (lift o norm) o (\x. x - c)`
  1047     SUBST1_TAC THENL [REWRITE_TAC[o_DEF]; ALL_TAC] THEN
  1048     MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
  1049     ASM_SIMP_TAC[CONTINUOUS_ON_SUB; CONTINUOUS_ON_ID; CONTINUOUS_ON_CONST;
  1050                  CONTINUOUS_ON_LIFT_NORM];
  1051     REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_CBALL; o_THM; dist] THEN
  1052     X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
  1053     REWRITE_TAC[VECTOR_ARITH `c - (&2 % c - (c + x)) = x`] THEN
  1054     REWRITE_TAC[NORM_MUL; REAL_ABS_DIV; REAL_ABS_NORM] THEN
  1055     ASM_SIMP_TAC[REAL_DIV_RMUL; NORM_EQ_0; VECTOR_SUB_EQ] THEN
  1056     ASM_REAL_ARITH_TAC;
  1057     REWRITE_TAC[NOT_EXISTS_THM; TAUT `~(c /\ b) <=> c ==> ~b`] THEN
  1058     REWRITE_TAC[IN_CBALL; o_THM; dist] THEN
  1059     X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
  1060     REWRITE_TAC[VECTOR_ARITH `&2 % c - (c + x') = x <=> --x' = x - c`] THEN
  1061     ASM_CASES_TAC `(x:real^N) IN path_component s c` THENL
  1062      [MATCH_MP_TAC(NORM_ARITH `norm(y) < B /\ norm(x) = B ==> ~(--x = y)`) THEN
  1063       REWRITE_TAC[NORM_MUL; REAL_ABS_DIV; REAL_ABS_NORM] THEN
  1064       ASM_SIMP_TAC[REAL_DIV_RMUL; NORM_EQ_0; VECTOR_SUB_EQ] THEN
  1065       ASM_SIMP_TAC[REAL_ARITH `&0 < B ==> abs B = B`] THEN
  1066       UNDISCH_TAC `path_component s c SUBSET ball(c:real^N,B)` THEN
  1067       REWRITE_TAC[SUBSET; IN_BALL] THEN ASM_MESON_TAC[dist; NORM_SUB];
  1068       EXPAND_TAC "q" THEN REWRITE_TAC[] THEN ASM_REWRITE_TAC[] THEN
  1069       REWRITE_TAC[VECTOR_ARITH `--(c % x) = x <=> (&1 + c) % x = vec 0`] THEN
  1070       ASM_REWRITE_TAC[DE_MORGAN_THM; VECTOR_SUB_EQ; VECTOR_MUL_EQ_0] THEN
  1071       SUBGOAL_THEN `~(x:real^N = c)` ASSUME_TAC THENL
  1072        [ASM_MESON_TAC[PATH_COMPONENT_REFL; IN]; ALL_TAC] THEN
  1073       ASM_REWRITE_TAC[] THEN
  1074       MATCH_MP_TAC(REAL_ARITH `&0 < x ==> ~(&1 + x = &0)`) THEN
  1075       ASM_SIMP_TAC[REAL_LT_DIV; NORM_POS_LT; VECTOR_SUB_EQ]]]);;
  1076 
  1077 let PATH_CONNECTED_COMPLEMENT_HOMEOMORPHIC_INTERVAL = prove
  1078  (`!s:real^N->bool a b:real^M.
  1079         2 <= dimindex(:N) /\ s homeomorphic interval[a,b]
  1080         ==> path_connected((:real^N) DIFF s)`,
  1081   REPEAT STRIP_TAC THEN REWRITE_TAC[PATH_CONNECTED_IFF_PATH_COMPONENT] THEN
  1082   FIRST_ASSUM(MP_TAC o MATCH_MP
  1083     UNBOUNDED_PATH_COMPONENTS_COMPLEMENT_HOMEOMORPHIC_INTERVAL) THEN
  1084   ASM_REWRITE_TAC[SET_RULE `~(x IN s) <=> x IN (UNIV DIFF s)`] THEN
  1085   ABBREV_TAC `t = (:real^N) DIFF s` THEN
  1086   DISCH_TAC THEN MAP_EVERY X_GEN_TAC [`x:real^N`; `y:real^N`] THEN
  1087   STRIP_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP HOMEOMORPHIC_COMPACTNESS) THEN
  1088   REWRITE_TAC[COMPACT_INTERVAL] THEN
  1089   DISCH_THEN(MP_TAC o MATCH_MP COMPACT_IMP_BOUNDED) THEN
  1090   REWRITE_TAC[BOUNDED_POS; LEFT_IMP_EXISTS_THM] THEN
  1091   X_GEN_TAC `B:real` THEN STRIP_TAC THEN
  1092   SUBGOAL_THEN `(?u:real^N. u IN path_component t x /\ B < norm(u)) /\
  1093                 (?v:real^N. v IN path_component t y /\ B < norm(v))`
  1094   STRIP_ASSUME_TAC THENL
  1095    [ASM_MESON_TAC[BOUNDED_POS; REAL_NOT_LE]; ALL_TAC] THEN
  1096   MATCH_MP_TAC PATH_COMPONENT_TRANS THEN EXISTS_TAC `u:real^N` THEN
  1097   CONJ_TAC THENL [ASM_MESON_TAC[IN]; ALL_TAC] THEN
  1098   MATCH_MP_TAC PATH_COMPONENT_SYM THEN
  1099   MATCH_MP_TAC PATH_COMPONENT_TRANS THEN EXISTS_TAC `v:real^N` THEN
  1100   CONJ_TAC THENL [ASM_MESON_TAC[IN]; ALL_TAC] THEN
  1101   MATCH_MP_TAC PATH_COMPONENT_OF_SUBSET THEN
  1102   EXISTS_TAC `(:real^N) DIFF cball(vec 0,B)` THEN CONJ_TAC THENL
  1103    [EXPAND_TAC "t" THEN MATCH_MP_TAC(SET_RULE
  1104      `s SUBSET t ==> (u DIFF t) SUBSET (u DIFF s)`) THEN
  1105     ASM_REWRITE_TAC[SUBSET; IN_CBALL_0];
  1106     MP_TAC(ISPEC `cball(vec 0:real^N,B)`
  1107        PATH_CONNECTED_COMPLEMENT_BOUNDED_CONVEX) THEN
  1108     ASM_REWRITE_TAC[BOUNDED_CBALL; CONVEX_CBALL] THEN
  1109     REWRITE_TAC[PATH_CONNECTED_IFF_PATH_COMPONENT] THEN
  1110     DISCH_THEN MATCH_MP_TAC THEN
  1111     ASM_REWRITE_TAC[IN_DIFF; IN_UNIV; IN_CBALL_0; REAL_NOT_LE]]);;
  1112 
  1113 (* ------------------------------------------------------------------------- *)
  1114 (* In particular, apply all these to the special case of an arc.             *)
  1115 (* ------------------------------------------------------------------------- *)
  1116 
  1117 let RETRACTION_ARC = prove
  1118  (`!p. arc p
  1119        ==> ?f. f continuous_on (:real^N) /\
  1120                IMAGE f (:real^N) SUBSET path_image p /\
  1121                (!x. x IN path_image p ==> f x = x)`,
  1122   REWRITE_TAC[arc; path; path_image] THEN REPEAT STRIP_TAC THEN
  1123   MATCH_MP_TAC RETRACTION_INJECTIVE_IMAGE_INTERVAL THEN
  1124   ASM_REWRITE_TAC[INTERVAL_EQ_EMPTY_CART_1; DROP_VEC; REAL_NOT_LT; REAL_POS]);;
  1125 
  1126 let PATH_CONNECTED_ARC_COMPLEMENT = prove
  1127  (`!p. 2 <= dimindex(:N) /\ arc p
  1128        ==> path_connected((:real^N) DIFF path_image p)`,
  1129   REWRITE_TAC[arc; path] THEN REPEAT STRIP_TAC THEN SIMP_TAC[path_image] THEN
  1130   MP_TAC(ISPECL [`path_image p:real^N->bool`; `vec 0:real^1`; `vec 1:real^1`]
  1131     PATH_CONNECTED_COMPLEMENT_HOMEOMORPHIC_INTERVAL) THEN
  1132   ASM_REWRITE_TAC[path_image] THEN DISCH_THEN MATCH_MP_TAC THEN
  1133   ONCE_REWRITE_TAC[HOMEOMORPHIC_SYM] THEN
  1134   MATCH_MP_TAC HOMEOMORPHIC_COMPACT THEN
  1135   EXISTS_TAC `p:real^1->real^N` THEN ASM_REWRITE_TAC[COMPACT_INTERVAL]);;
  1136 
  1137 let CONNECTED_ARC_COMPLEMENT = prove
  1138  (`!p. 2 <= dimindex(:N) /\ arc p
  1139        ==> connected((:real^N) DIFF path_image p)`,
  1140   SIMP_TAC[PATH_CONNECTED_ARC_COMPLEMENT; PATH_CONNECTED_IMP_CONNECTED]);; *)
  1141 
  1142 end