src/HOL/Analysis/Fashoda_Theorem.thy
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (2 months ago)
changeset 69981 3dced198b9ec
parent 69722 b5163b2132c5
child 70136 f03a01a18c6e
permissions -rw-r--r--
more strict AFP properties;
     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_Theorem
     8 imports Brouwer_Fixpoint Path_Connected Cartesian_Euclidean_Space
     9 begin
    10 
    11 subsection \<open>Bijections between intervals\<close>
    12 
    13 definition%important interval_bij :: "'a \<times> 'a \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<Rightarrow> 'a::euclidean_space"
    14   where "interval_bij =
    15     (\<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))"
    16 
    17 lemma interval_bij_affine:
    18   "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) +
    19     (\<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))"
    20   by (auto simp: sum.distrib[symmetric] scaleR_add_left[symmetric] interval_bij_def fun_eq_iff
    21     field_simps inner_simps add_divide_distrib[symmetric] intro!: sum.cong)
    22 
    23 lemma continuous_interval_bij:
    24   fixes a b :: "'a::euclidean_space"
    25   shows "continuous (at x) (interval_bij (a, b) (u, v))"
    26   by (auto simp add: divide_inverse interval_bij_def intro!: continuous_sum continuous_intros)
    27 
    28 lemma continuous_on_interval_bij: "continuous_on s (interval_bij (a, b) (u, v))"
    29   apply(rule continuous_at_imp_continuous_on)
    30   apply (rule, rule continuous_interval_bij)
    31   done
    32 
    33 lemma in_interval_interval_bij:
    34   fixes a b u v x :: "'a::euclidean_space"
    35   assumes "x \<in> cbox a b"
    36     and "cbox u v \<noteq> {}"
    37   shows "interval_bij (a, b) (u, v) x \<in> cbox u v"
    38   apply (simp only: interval_bij_def split_conv mem_box inner_sum_left_Basis cong: ball_cong)
    39   apply safe
    40 proof -
    41   fix i :: 'a
    42   assume i: "i \<in> Basis"
    43   have "cbox a b \<noteq> {}"
    44     using assms by auto
    45   with i have *: "a\<bullet>i \<le> b\<bullet>i" "u\<bullet>i \<le> v\<bullet>i"
    46     using assms(2) by (auto simp add: box_eq_empty)
    47   have x: "a\<bullet>i\<le>x\<bullet>i" "x\<bullet>i\<le>b\<bullet>i"
    48     using assms(1)[unfolded mem_box] using i by auto
    49   have "0 \<le> (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i)"
    50     using * x by auto
    51   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)"
    52     using * by auto
    53   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)"
    54     apply (rule mult_right_mono)
    55     unfolding divide_le_eq_1
    56     using * x
    57     apply auto
    58     done
    59   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"
    60     using * by auto
    61 qed
    62 
    63 lemma interval_bij_bij:
    64   "\<forall>(i::'a::euclidean_space)\<in>Basis. a\<bullet>i < b\<bullet>i \<and> u\<bullet>i < v\<bullet>i \<Longrightarrow>
    65     interval_bij (a, b) (u, v) (interval_bij (u, v) (a, b) x) = x"
    66   by (auto simp: interval_bij_def euclidean_eq_iff[where 'a='a])
    67 
    68 lemma interval_bij_bij_cart: fixes x::"real^'n" assumes "\<forall>i. a$i < b$i \<and> u$i < v$i"
    69   shows "interval_bij (a,b) (u,v) (interval_bij (u,v) (a,b) x) = x"
    70   using assms by (intro interval_bij_bij) (auto simp: Basis_vec_def inner_axis)
    71 
    72 
    73 subsection \<open>Fashoda meet theorem\<close>
    74 
    75 lemma infnorm_2:
    76   fixes x :: "real^2"
    77   shows "infnorm x = max \<bar>x$1\<bar> \<bar>x$2\<bar>"
    78   unfolding infnorm_cart UNIV_2 by (rule cSup_eq) auto
    79 
    80 lemma infnorm_eq_1_2:
    81   fixes x :: "real^2"
    82   shows "infnorm x = 1 \<longleftrightarrow>
    83     \<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)"
    84   unfolding infnorm_2 by auto
    85 
    86 lemma infnorm_eq_1_imp:
    87   fixes x :: "real^2"
    88   assumes "infnorm x = 1"
    89   shows "\<bar>x$1\<bar> \<le> 1" and "\<bar>x$2\<bar> \<le> 1"
    90   using assms unfolding infnorm_eq_1_2 by auto
    91 
    92 proposition fashoda_unit:
    93   fixes f g :: "real \<Rightarrow> real^2"
    94   assumes "f ` {-1 .. 1} \<subseteq> cbox (-1) 1"
    95     and "g ` {-1 .. 1} \<subseteq> cbox (-1) 1"
    96     and "continuous_on {-1 .. 1} f"
    97     and "continuous_on {-1 .. 1} g"
    98     and "f (- 1)$1 = - 1"
    99     and "f 1$1 = 1" "g (- 1) $2 = -1"
   100     and "g 1 $2 = 1"
   101   shows "\<exists>s\<in>{-1 .. 1}. \<exists>t\<in>{-1 .. 1}. f s = g t"
   102 proof (rule ccontr)
   103   assume "\<not> ?thesis"
   104   note as = this[unfolded bex_simps,rule_format]
   105   define sqprojection
   106     where [abs_def]: "sqprojection z = (inverse (infnorm z)) *\<^sub>R z" for z :: "real^2"
   107   define negatex :: "real^2 \<Rightarrow> real^2"
   108     where "negatex x = (vector [-(x$1), x$2])" for x
   109   have lem1: "\<forall>z::real^2. infnorm (negatex z) = infnorm z"
   110     unfolding negatex_def infnorm_2 vector_2 by auto
   111   have lem2: "\<forall>z. z \<noteq> 0 \<longrightarrow> infnorm (sqprojection z) = 1"
   112     unfolding sqprojection_def infnorm_mul[unfolded scalar_mult_eq_scaleR]
   113     by (simp add: real_abs_infnorm infnorm_eq_0)
   114   let ?F = "\<lambda>w::real^2. (f \<circ> (\<lambda>x. x$1)) w - (g \<circ> (\<lambda>x. x$2)) w"
   115   have *: "\<And>i. (\<lambda>x::real^2. x $ i) ` cbox (- 1) 1 = {-1..1}"
   116   proof 
   117     show "(\<lambda>x::real^2. x $ i) ` cbox (- 1) 1 \<subseteq> {-1..1}" for i
   118       by (auto simp: mem_box_cart)
   119     show "{-1..1} \<subseteq> (\<lambda>x::real^2. x $ i) ` cbox (- 1) 1" for i
   120       by (clarsimp simp: image_iff mem_box_cart Bex_def) (metis (no_types, hide_lams) vec_component)
   121   qed
   122   {
   123     fix x
   124     assume "x \<in> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w) ` (cbox (- 1) (1::real^2))"
   125     then obtain w :: "real^2" where w:
   126         "w \<in> cbox (- 1) 1"
   127         "x = (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w"
   128       unfolding image_iff ..
   129     then have "x \<noteq> 0"
   130       using as[of "w$1" "w$2"]
   131       unfolding mem_box_cart atLeastAtMost_iff
   132       by auto
   133   } note x0 = this
   134   have 1: "box (- 1) (1::real^2) \<noteq> {}"
   135     unfolding interval_eq_empty_cart by auto
   136   have "negatex (x + y) $ i = (negatex x + negatex y) $ i \<and> negatex (c *\<^sub>R x) $ i = (c *\<^sub>R negatex x) $ i"
   137     for i x y c
   138     using exhaust_2 [of i] by (auto simp: negatex_def)
   139   then have "bounded_linear negatex"
   140     by (simp add: bounded_linearI' vec_eq_iff)
   141   then have 2: "continuous_on (cbox (- 1) 1) (negatex \<circ> sqprojection \<circ> ?F)"
   142     apply (intro continuous_intros continuous_on_component)
   143     unfolding * sqprojection_def
   144     apply (intro assms continuous_intros)+
   145      apply (simp_all add: infnorm_eq_0 x0 linear_continuous_on)
   146     done
   147   have 3: "(negatex \<circ> sqprojection \<circ> ?F) ` cbox (-1) 1 \<subseteq> cbox (-1) 1"
   148     unfolding subset_eq
   149   proof (rule, goal_cases)
   150     case (1 x)
   151     then obtain y :: "real^2" where y:
   152         "y \<in> cbox (- 1) 1"
   153         "x = (negatex \<circ> sqprojection \<circ> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w)) y"
   154       unfolding image_iff ..
   155     have "?F y \<noteq> 0"
   156       by (rule x0) (use y in auto)
   157     then have *: "infnorm (sqprojection (?F y)) = 1"
   158       unfolding y o_def
   159       by - (rule lem2[rule_format])
   160     have inf1: "infnorm x = 1"
   161       unfolding *[symmetric] y o_def
   162       by (rule lem1[rule_format])
   163     show "x \<in> cbox (-1) 1"
   164       unfolding mem_box_cart interval_cbox_cart infnorm_2
   165     proof 
   166       fix i
   167       show "(- 1) $ i \<le> x $ i \<and> x $ i \<le> 1 $ i"
   168         using exhaust_2 [of i] inf1 by (auto simp: infnorm_2)
   169     qed
   170   qed
   171   obtain x :: "real^2" where x:
   172       "x \<in> cbox (- 1) 1"
   173       "(negatex \<circ> sqprojection \<circ> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w)) x = x"
   174     apply (rule brouwer_weak[of "cbox (- 1) (1::real^2)" "negatex \<circ> sqprojection \<circ> ?F"])
   175     apply (rule compact_cbox convex_box)+
   176     unfolding interior_cbox
   177     apply (rule 1 2 3)+
   178     apply blast
   179     done
   180   have "?F x \<noteq> 0"
   181     by (rule x0) (use x in auto)
   182   then have *: "infnorm (sqprojection (?F x)) = 1"
   183     unfolding o_def
   184     by (rule lem2[rule_format])
   185   have nx: "infnorm x = 1"
   186     apply (subst x(2)[symmetric])
   187     unfolding *[symmetric] o_def
   188     apply (rule lem1[rule_format])
   189     done
   190   have iff: "0 < sqprojection x$i \<longleftrightarrow> 0 < x$i" "sqprojection x$i < 0 \<longleftrightarrow> x$i < 0" if "x \<noteq> 0" for x i
   191   proof -
   192     have "inverse (infnorm x) > 0"
   193       by (simp add: infnorm_pos_lt that)
   194     then show "(0 < sqprojection x $ i) = (0 < x $ i)"
   195       and "(sqprojection x $ i < 0) = (x $ i < 0)"
   196       unfolding sqprojection_def vector_component_simps vector_scaleR_component real_scaleR_def
   197       unfolding zero_less_mult_iff mult_less_0_iff
   198       by (auto simp add: field_simps)
   199   qed
   200   have x1: "x $ 1 \<in> {- 1..1::real}" "x $ 2 \<in> {- 1..1::real}"
   201     using x(1) unfolding mem_box_cart by auto
   202   then have nz: "f (x $ 1) - g (x $ 2) \<noteq> 0"
   203     using as by auto
   204   consider "x $ 1 = -1" | "x $ 1 = 1" | "x $ 2 = -1" | "x $ 2 = 1"
   205     using nx unfolding infnorm_eq_1_2 by auto
   206   then show False
   207   proof cases
   208     case 1
   209     then have *: "f (x $ 1) $ 1 = - 1"
   210       using assms(5) by auto
   211     have "sqprojection (f (x$1) - g (x$2)) $ 1 > 0"
   212       using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]]
   213       by (auto simp: negatex_def 1)
   214     moreover
   215     from x1 have "g (x $ 2) \<in> cbox (-1) 1"
   216       using assms(2) by blast
   217     ultimately show False
   218       unfolding iff[OF nz] vector_component_simps * mem_box_cart
   219       using not_le by auto
   220   next
   221     case 2
   222     then have *: "f (x $ 1) $ 1 = 1"
   223       using assms(6) by auto
   224     have "sqprojection (f (x$1) - g (x$2)) $ 1 < 0"
   225       using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]] 2
   226       by (auto simp: negatex_def)
   227     moreover have "g (x $ 2) \<in> cbox (-1) 1"
   228       using assms(2) x1 by blast
   229     ultimately show False
   230       unfolding iff[OF nz] vector_component_simps * mem_box_cart
   231       using not_le by auto
   232   next
   233     case 3
   234     then have *: "g (x $ 2) $ 2 = - 1"
   235       using assms(7) by auto
   236     have "sqprojection (f (x$1) - g (x$2)) $ 2 < 0"
   237       using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]] 3 by (auto simp: negatex_def)
   238     moreover
   239     from x1 have "f (x $ 1) \<in> cbox (-1) 1"
   240       using assms(1) by blast
   241     ultimately show False
   242       unfolding iff[OF nz] vector_component_simps * mem_box_cart
   243       by (erule_tac x=2 in allE) auto
   244   next
   245     case 4
   246     then have *: "g (x $ 2) $ 2 = 1"
   247       using assms(8) by auto
   248     have "sqprojection (f (x$1) - g (x$2)) $ 2 > 0"
   249       using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]] 4 by (auto simp: negatex_def)
   250     moreover
   251     from x1 have "f (x $ 1) \<in> cbox (-1) 1"
   252       using assms(1) by blast
   253     ultimately show False
   254       unfolding iff[OF nz] vector_component_simps * mem_box_cart
   255       by (erule_tac x=2 in allE) auto
   256   qed 
   257 qed
   258 
   259 proposition fashoda_unit_path:
   260   fixes f g :: "real \<Rightarrow> real^2"
   261   assumes "path f"
   262     and "path g"
   263     and "path_image f \<subseteq> cbox (-1) 1"
   264     and "path_image g \<subseteq> cbox (-1) 1"
   265     and "(pathstart f)$1 = -1"
   266     and "(pathfinish f)$1 = 1"
   267     and "(pathstart g)$2 = -1"
   268     and "(pathfinish g)$2 = 1"
   269   obtains z where "z \<in> path_image f" and "z \<in> path_image g"
   270 proof -
   271   note assms=assms[unfolded path_def pathstart_def pathfinish_def path_image_def]
   272   define iscale where [abs_def]: "iscale z = inverse 2 *\<^sub>R (z + 1)" for z :: real
   273   have isc: "iscale ` {- 1..1} \<subseteq> {0..1}"
   274     unfolding iscale_def by auto
   275   have "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. (f \<circ> iscale) s = (g \<circ> iscale) t"
   276   proof (rule fashoda_unit)
   277     show "(f \<circ> iscale) ` {- 1..1} \<subseteq> cbox (- 1) 1" "(g \<circ> iscale) ` {- 1..1} \<subseteq> cbox (- 1) 1"
   278       using isc and assms(3-4) by (auto simp add: image_comp [symmetric])
   279     have *: "continuous_on {- 1..1} iscale"
   280       unfolding iscale_def by (rule continuous_intros)+
   281     show "continuous_on {- 1..1} (f \<circ> iscale)" "continuous_on {- 1..1} (g \<circ> iscale)"
   282       apply -
   283       apply (rule_tac[!] continuous_on_compose[OF *])
   284       apply (rule_tac[!] continuous_on_subset[OF _ isc])
   285       apply (rule assms)+
   286       done
   287     have *: "(1 / 2) *\<^sub>R (1 + (1::real^1)) = 1"
   288       unfolding vec_eq_iff by auto
   289     show "(f \<circ> iscale) (- 1) $ 1 = - 1"
   290       and "(f \<circ> iscale) 1 $ 1 = 1"
   291       and "(g \<circ> iscale) (- 1) $ 2 = -1"
   292       and "(g \<circ> iscale) 1 $ 2 = 1"
   293       unfolding o_def iscale_def
   294       using assms
   295       by (auto simp add: *)
   296   qed
   297   then obtain s t where st:
   298       "s \<in> {- 1..1}"
   299       "t \<in> {- 1..1}"
   300       "(f \<circ> iscale) s = (g \<circ> iscale) t"
   301     by auto
   302   show thesis
   303     apply (rule_tac z = "f (iscale s)" in that)
   304     using st
   305     unfolding o_def path_image_def image_iff
   306     apply -
   307     apply (rule_tac x="iscale s" in bexI)
   308     prefer 3
   309     apply (rule_tac x="iscale t" in bexI)
   310     using isc[unfolded subset_eq, rule_format]
   311     apply auto
   312     done
   313 qed
   314 
   315 theorem fashoda:
   316   fixes b :: "real^2"
   317   assumes "path f"
   318     and "path g"
   319     and "path_image f \<subseteq> cbox a b"
   320     and "path_image g \<subseteq> cbox a b"
   321     and "(pathstart f)$1 = a$1"
   322     and "(pathfinish f)$1 = b$1"
   323     and "(pathstart g)$2 = a$2"
   324     and "(pathfinish g)$2 = b$2"
   325   obtains z where "z \<in> path_image f" and "z \<in> path_image g"
   326 proof -
   327   fix P Q S
   328   presume "P \<or> Q \<or> S" "P \<Longrightarrow> thesis" and "Q \<Longrightarrow> thesis" and "S \<Longrightarrow> thesis"
   329   then show thesis
   330     by auto
   331 next
   332   have "cbox a b \<noteq> {}"
   333     using assms(3) using path_image_nonempty[of f] by auto
   334   then have "a \<le> b"
   335     unfolding interval_eq_empty_cart less_eq_vec_def by (auto simp add: not_less)
   336   then show "a$1 = b$1 \<or> a$2 = b$2 \<or> (a$1 < b$1 \<and> a$2 < b$2)"
   337     unfolding less_eq_vec_def forall_2 by auto
   338 next
   339   assume as: "a$1 = b$1"
   340   have "\<exists>z\<in>path_image g. z$2 = (pathstart f)$2"
   341     apply (rule connected_ivt_component_cart)
   342     apply (rule connected_path_image assms)+
   343     apply (rule pathstart_in_path_image)
   344     apply (rule pathfinish_in_path_image)
   345     unfolding assms using assms(3)[unfolded path_image_def subset_eq,rule_format,of "f 0"]
   346     unfolding pathstart_def
   347     apply (auto simp add: less_eq_vec_def mem_box_cart)
   348     done
   349   then obtain z :: "real^2" where z: "z \<in> path_image g" "z $ 2 = pathstart f $ 2" ..
   350   have "z \<in> cbox a b"
   351     using z(1) assms(4)
   352     unfolding path_image_def
   353     by blast
   354   then have "z = f 0"
   355     unfolding vec_eq_iff forall_2
   356     unfolding z(2) pathstart_def
   357     using assms(3)[unfolded path_image_def subset_eq mem_box_cart,rule_format,of "f 0" 1]
   358     unfolding mem_box_cart
   359     apply (erule_tac x=1 in allE)
   360     using as
   361     apply auto
   362     done
   363   then show thesis
   364     apply -
   365     apply (rule that[OF _ z(1)])
   366     unfolding path_image_def
   367     apply auto
   368     done
   369 next
   370   assume as: "a$2 = b$2"
   371   have "\<exists>z\<in>path_image f. z$1 = (pathstart g)$1"
   372     apply (rule connected_ivt_component_cart)
   373     apply (rule connected_path_image assms)+
   374     apply (rule pathstart_in_path_image)
   375     apply (rule pathfinish_in_path_image)
   376     unfolding assms
   377     using assms(4)[unfolded path_image_def subset_eq,rule_format,of "g 0"]
   378     unfolding pathstart_def
   379     apply (auto simp add: less_eq_vec_def mem_box_cart)
   380     done
   381   then obtain z where z: "z \<in> path_image f" "z $ 1 = pathstart g $ 1" ..
   382   have "z \<in> cbox a b"
   383     using z(1) assms(3)
   384     unfolding path_image_def
   385     by blast
   386   then have "z = g 0"
   387     unfolding vec_eq_iff forall_2
   388     unfolding z(2) pathstart_def
   389     using assms(4)[unfolded path_image_def subset_eq mem_box_cart,rule_format,of "g 0" 2]
   390     unfolding mem_box_cart
   391     apply (erule_tac x=2 in allE)
   392     using as
   393     apply auto
   394     done
   395   then show thesis
   396     apply -
   397     apply (rule that[OF z(1)])
   398     unfolding path_image_def
   399     apply auto
   400     done
   401 next
   402   assume as: "a $ 1 < b $ 1 \<and> a $ 2 < b $ 2"
   403   have int_nem: "cbox (-1) (1::real^2) \<noteq> {}"
   404     unfolding interval_eq_empty_cart by auto
   405   obtain z :: "real^2" where z:
   406       "z \<in> (interval_bij (a, b) (- 1, 1) \<circ> f) ` {0..1}"
   407       "z \<in> (interval_bij (a, b) (- 1, 1) \<circ> g) ` {0..1}"
   408     apply (rule fashoda_unit_path[of "interval_bij (a,b) (- 1,1) \<circ> f" "interval_bij (a,b) (- 1,1) \<circ> g"])
   409     unfolding path_def path_image_def pathstart_def pathfinish_def
   410     apply (rule_tac[1-2] continuous_on_compose)
   411     apply (rule assms[unfolded path_def] continuous_on_interval_bij)+
   412     unfolding subset_eq
   413     apply(rule_tac[1-2] ballI)
   414   proof -
   415     fix x
   416     assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> f) ` {0..1}"
   417     then obtain y where y:
   418         "y \<in> {0..1}"
   419         "x = (interval_bij (a, b) (- 1, 1) \<circ> f) y"
   420       unfolding image_iff ..
   421     show "x \<in> cbox (- 1) 1"
   422       unfolding y o_def
   423       apply (rule in_interval_interval_bij)
   424       using y(1)
   425       using assms(3)[unfolded path_image_def subset_eq] int_nem
   426       apply auto
   427       done
   428   next
   429     fix x
   430     assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> g) ` {0..1}"
   431     then obtain y where y:
   432         "y \<in> {0..1}"
   433         "x = (interval_bij (a, b) (- 1, 1) \<circ> g) y"
   434       unfolding image_iff ..
   435     show "x \<in> cbox (- 1) 1"
   436       unfolding y o_def
   437       apply (rule in_interval_interval_bij)
   438       using y(1)
   439       using assms(4)[unfolded path_image_def subset_eq] int_nem
   440       apply auto
   441       done
   442   next
   443     show "(interval_bij (a, b) (- 1, 1) \<circ> f) 0 $ 1 = -1"
   444       and "(interval_bij (a, b) (- 1, 1) \<circ> f) 1 $ 1 = 1"
   445       and "(interval_bij (a, b) (- 1, 1) \<circ> g) 0 $ 2 = -1"
   446       and "(interval_bij (a, b) (- 1, 1) \<circ> g) 1 $ 2 = 1"
   447       using assms as
   448       by (simp_all add: cart_eq_inner_axis pathstart_def pathfinish_def interval_bij_def)
   449          (simp_all add: inner_axis)
   450   qed
   451   from z(1) obtain zf where zf:
   452       "zf \<in> {0..1}"
   453       "z = (interval_bij (a, b) (- 1, 1) \<circ> f) zf"
   454     unfolding image_iff ..
   455   from z(2) obtain zg where zg:
   456       "zg \<in> {0..1}"
   457       "z = (interval_bij (a, b) (- 1, 1) \<circ> g) zg"
   458     unfolding image_iff ..
   459   have *: "\<forall>i. (- 1) $ i < (1::real^2) $ i \<and> a $ i < b $ i"
   460     unfolding forall_2
   461     using as
   462     by auto
   463   show thesis
   464   proof (rule_tac z="interval_bij (- 1,1) (a,b) z" in that)
   465     show "interval_bij (- 1, 1) (a, b) z \<in> path_image f"
   466       using zf by (simp add: interval_bij_bij_cart[OF *] path_image_def)
   467     show "interval_bij (- 1, 1) (a, b) z \<in> path_image g"
   468       using zg by (simp add: interval_bij_bij_cart[OF *] path_image_def)
   469   qed
   470 qed
   471 
   472 
   473 subsection%unimportant \<open>Some slightly ad hoc lemmas I use below\<close>
   474 
   475 lemma segment_vertical:
   476   fixes a :: "real^2"
   477   assumes "a$1 = b$1"
   478   shows "x \<in> closed_segment a b \<longleftrightarrow>
   479     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)"
   480   (is "_ = ?R")
   481 proof -
   482   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"
   483   {
   484     presume "?L \<Longrightarrow> ?R" and "?R \<Longrightarrow> ?L"
   485     then show ?thesis
   486       unfolding closed_segment_def mem_Collect_eq
   487       unfolding vec_eq_iff forall_2 scalar_mult_eq_scaleR[symmetric] vector_component_simps
   488       by blast
   489   }
   490   {
   491     assume ?L
   492     then obtain u where u:
   493         "x $ 1 = (1 - u) * a $ 1 + u * b $ 1"
   494         "x $ 2 = (1 - u) * a $ 2 + u * b $ 2"
   495         "0 \<le> u"
   496         "u \<le> 1"
   497       by blast
   498     { fix b a
   499       assume "b + u * a > a + u * b"
   500       then have "(1 - u) * b > (1 - u) * a"
   501         by (auto simp add:field_simps)
   502       then have "b \<ge> a"
   503         apply (drule_tac mult_left_less_imp_less)
   504         using u
   505         apply auto
   506         done
   507       then have "u * a \<le> u * b"
   508         apply -
   509         apply (rule mult_left_mono[OF _ u(3)])
   510         using u(3-4)
   511         apply (auto simp add: field_simps)
   512         done
   513     } note * = this
   514     {
   515       fix a b
   516       assume "u * b > u * a"
   517       then have "(1 - u) * a \<le> (1 - u) * b"
   518         apply -
   519         apply (rule mult_left_mono)
   520         apply (drule mult_left_less_imp_less)
   521         using u
   522         apply auto
   523         done
   524       then have "a + u * b \<le> b + u * a"
   525         by (auto simp add: field_simps)
   526     } note ** = this
   527     then show ?R
   528       unfolding u assms
   529       using u
   530       by (auto simp add:field_simps not_le intro: * **)
   531   }
   532   {
   533     assume ?R
   534     then show ?L
   535     proof (cases "x$2 = b$2")
   536       case True
   537       then show ?L
   538         apply (rule_tac x="(x$2 - a$2) / (b$2 - a$2)" in exI)
   539         unfolding assms True using \<open>?R\<close> apply (auto simp add: field_simps)
   540         done
   541     next
   542       case False
   543       then show ?L
   544         apply (rule_tac x="1 - (x$2 - b$2) / (a$2 - b$2)" in exI)
   545         unfolding assms using \<open>?R\<close> apply (auto simp add: field_simps)
   546         done
   547     qed
   548   }
   549 qed
   550 
   551 lemma segment_horizontal:
   552   fixes a :: "real^2"
   553   assumes "a$2 = b$2"
   554   shows "x \<in> closed_segment a b \<longleftrightarrow>
   555     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)"
   556   (is "_ = ?R")
   557 proof -
   558   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"
   559   {
   560     presume "?L \<Longrightarrow> ?R" and "?R \<Longrightarrow> ?L"
   561     then show ?thesis
   562       unfolding closed_segment_def mem_Collect_eq
   563       unfolding vec_eq_iff forall_2 scalar_mult_eq_scaleR[symmetric] vector_component_simps
   564       by blast
   565   }
   566   {
   567     assume ?L
   568     then obtain u where u:
   569         "x $ 1 = (1 - u) * a $ 1 + u * b $ 1"
   570         "x $ 2 = (1 - u) * a $ 2 + u * b $ 2"
   571         "0 \<le> u"
   572         "u \<le> 1"
   573       by blast
   574     {
   575       fix b a
   576       assume "b + u * a > a + u * b"
   577       then have "(1 - u) * b > (1 - u) * a"
   578         by (auto simp add: field_simps)
   579       then have "b \<ge> a"
   580         apply (drule_tac mult_left_less_imp_less)
   581         using u
   582         apply auto
   583         done
   584       then have "u * a \<le> u * b"
   585         apply -
   586         apply (rule mult_left_mono[OF _ u(3)])
   587         using u(3-4)
   588         apply (auto simp add: field_simps)
   589         done
   590     } note * = this
   591     {
   592       fix a b
   593       assume "u * b > u * a"
   594       then have "(1 - u) * a \<le> (1 - u) * b"
   595         apply -
   596         apply (rule mult_left_mono)
   597         apply (drule mult_left_less_imp_less)
   598         using u
   599         apply auto
   600         done
   601       then have "a + u * b \<le> b + u * a"
   602         by (auto simp add: field_simps)
   603     } note ** = this
   604     then show ?R
   605       unfolding u assms
   606       using u
   607       by (auto simp add: field_simps not_le intro: * **)
   608   }
   609   {
   610     assume ?R
   611     then show ?L
   612     proof (cases "x$1 = b$1")
   613       case True
   614       then show ?L
   615         apply (rule_tac x="(x$1 - a$1) / (b$1 - a$1)" in exI)
   616         unfolding assms True
   617         using \<open>?R\<close>
   618         apply (auto simp add: field_simps)
   619         done
   620     next
   621       case False
   622       then show ?L
   623         apply (rule_tac x="1 - (x$1 - b$1) / (a$1 - b$1)" in exI)
   624         unfolding assms
   625         using \<open>?R\<close>
   626         apply (auto simp add: field_simps)
   627         done
   628     qed
   629   }
   630 qed
   631 
   632 
   633 subsection \<open>Useful Fashoda corollary pointed out to me by Tom Hales\<close>(*FIXME change title? *)
   634 
   635 corollary fashoda_interlace:
   636   fixes a :: "real^2"
   637   assumes "path f"
   638     and "path g"
   639     and paf: "path_image f \<subseteq> cbox a b"
   640     and pag: "path_image g \<subseteq> cbox a b"
   641     and "(pathstart f)$2 = a$2"
   642     and "(pathfinish f)$2 = a$2"
   643     and "(pathstart g)$2 = a$2"
   644     and "(pathfinish g)$2 = a$2"
   645     and "(pathstart f)$1 < (pathstart g)$1"
   646     and "(pathstart g)$1 < (pathfinish f)$1"
   647     and "(pathfinish f)$1 < (pathfinish g)$1"
   648   obtains z where "z \<in> path_image f" and "z \<in> path_image g"
   649 proof -
   650   have "cbox a b \<noteq> {}"
   651     using path_image_nonempty[of f] using assms(3) by auto
   652   note ab=this[unfolded interval_eq_empty_cart not_ex forall_2 not_less]
   653   have "pathstart f \<in> cbox a b"
   654     and "pathfinish f \<in> cbox a b"
   655     and "pathstart g \<in> cbox a b"
   656     and "pathfinish g \<in> cbox a b"
   657     using pathstart_in_path_image pathfinish_in_path_image
   658     using assms(3-4)
   659     by auto
   660   note startfin = this[unfolded mem_box_cart forall_2]
   661   let ?P1 = "linepath (vector[a$1 - 2, a$2 - 2]) (vector[(pathstart f)$1,a$2 - 2]) +++
   662      linepath(vector[(pathstart f)$1,a$2 - 2])(pathstart f) +++ f +++
   663      linepath(pathfinish f)(vector[(pathfinish f)$1,a$2 - 2]) +++
   664      linepath(vector[(pathfinish f)$1,a$2 - 2])(vector[b$1 + 2,a$2 - 2])"
   665   let ?P2 = "linepath(vector[(pathstart g)$1, (pathstart g)$2 - 3])(pathstart g) +++ g +++
   666      linepath(pathfinish g)(vector[(pathfinish g)$1,a$2 - 1]) +++
   667      linepath(vector[(pathfinish g)$1,a$2 - 1])(vector[b$1 + 1,a$2 - 1]) +++
   668      linepath(vector[b$1 + 1,a$2 - 1])(vector[b$1 + 1,b$2 + 3])"
   669   let ?a = "vector[a$1 - 2, a$2 - 3]"
   670   let ?b = "vector[b$1 + 2, b$2 + 3]"
   671   have P1P2: "path_image ?P1 = path_image (linepath (vector[a$1 - 2, a$2 - 2]) (vector[(pathstart f)$1,a$2 - 2])) \<union>
   672       path_image (linepath(vector[(pathstart f)$1,a$2 - 2])(pathstart f)) \<union> path_image f \<union>
   673       path_image (linepath(pathfinish f)(vector[(pathfinish f)$1,a$2 - 2])) \<union>
   674       path_image (linepath(vector[(pathfinish f)$1,a$2 - 2])(vector[b$1 + 2,a$2 - 2]))"
   675     "path_image ?P2 = path_image(linepath(vector[(pathstart g)$1, (pathstart g)$2 - 3])(pathstart g)) \<union> path_image g \<union>
   676       path_image(linepath(pathfinish g)(vector[(pathfinish g)$1,a$2 - 1])) \<union>
   677       path_image(linepath(vector[(pathfinish g)$1,a$2 - 1])(vector[b$1 + 1,a$2 - 1])) \<union>
   678       path_image(linepath(vector[b$1 + 1,a$2 - 1])(vector[b$1 + 1,b$2 + 3]))" using assms(1-2)
   679       by(auto simp add: path_image_join path_linepath)
   680   have abab: "cbox a b \<subseteq> cbox ?a ?b"
   681     unfolding interval_cbox_cart[symmetric]
   682     by (auto simp add:less_eq_vec_def forall_2 vector_2)
   683   obtain z where
   684     "z \<in> path_image
   685           (linepath (vector [a $ 1 - 2, a $ 2 - 2]) (vector [pathstart f $ 1, a $ 2 - 2]) +++
   686            linepath (vector [pathstart f $ 1, a $ 2 - 2]) (pathstart f) +++
   687            f +++
   688            linepath (pathfinish f) (vector [pathfinish f $ 1, a $ 2 - 2]) +++
   689            linepath (vector [pathfinish f $ 1, a $ 2 - 2]) (vector [b $ 1 + 2, a $ 2 - 2]))"
   690     "z \<in> path_image
   691           (linepath (vector [pathstart g $ 1, pathstart g $ 2 - 3]) (pathstart g) +++
   692            g +++
   693            linepath (pathfinish g) (vector [pathfinish g $ 1, a $ 2 - 1]) +++
   694            linepath (vector [pathfinish g $ 1, a $ 2 - 1]) (vector [b $ 1 + 1, a $ 2 - 1]) +++
   695            linepath (vector [b $ 1 + 1, a $ 2 - 1]) (vector [b $ 1 + 1, b $ 2 + 3]))"
   696     apply (rule fashoda[of ?P1 ?P2 ?a ?b])
   697     unfolding pathstart_join pathfinish_join pathstart_linepath pathfinish_linepath vector_2
   698   proof -
   699     show "path ?P1" and "path ?P2"
   700       using assms by auto
   701     show "path_image ?P1 \<subseteq> cbox ?a ?b" "path_image ?P2 \<subseteq> cbox ?a ?b"
   702       unfolding P1P2 path_image_linepath using startfin paf pag
   703       by (auto simp: mem_box_cart segment_horizontal segment_vertical forall_2)
   704     show "a $ 1 - 2 = a $ 1 - 2"
   705       and "b $ 1 + 2 = b $ 1 + 2"
   706       and "pathstart g $ 2 - 3 = a $ 2 - 3"
   707       and "b $ 2 + 3 = b $ 2 + 3"
   708       by (auto simp add: assms)
   709   qed
   710   note z=this[unfolded P1P2 path_image_linepath]
   711   show thesis
   712   proof (rule that[of z])
   713     have "(z \<in> closed_segment (vector [a $ 1 - 2, a $ 2 - 2]) (vector [pathstart f $ 1, a $ 2 - 2]) \<or>
   714       z \<in> closed_segment (vector [pathstart f $ 1, a $ 2 - 2]) (pathstart f)) \<or>
   715       z \<in> closed_segment (pathfinish f) (vector [pathfinish f $ 1, a $ 2 - 2]) \<or>
   716       z \<in> closed_segment (vector [pathfinish f $ 1, a $ 2 - 2]) (vector [b $ 1 + 2, a $ 2 - 2]) \<Longrightarrow>
   717     (((z \<in> closed_segment (vector [pathstart g $ 1, pathstart g $ 2 - 3]) (pathstart g)) \<or>
   718       z \<in> closed_segment (pathfinish g) (vector [pathfinish g $ 1, a $ 2 - 1])) \<or>
   719       z \<in> closed_segment (vector [pathfinish g $ 1, a $ 2 - 1]) (vector [b $ 1 + 1, a $ 2 - 1])) \<or>
   720       z \<in> closed_segment (vector [b $ 1 + 1, a $ 2 - 1]) (vector [b $ 1 + 1, b $ 2 + 3]) \<Longrightarrow> False"
   721     proof (simp only: segment_vertical segment_horizontal vector_2, goal_cases)
   722       case prems: 1
   723       have "pathfinish f \<in> cbox a b"
   724         using assms(3) pathfinish_in_path_image[of f] by auto
   725       then have "1 + b $ 1 \<le> pathfinish f $ 1 \<Longrightarrow> False"
   726         unfolding mem_box_cart forall_2 by auto
   727       then have "z$1 \<noteq> pathfinish f$1"
   728         using prems(2)
   729         using assms ab
   730         by (auto simp add: field_simps)
   731       moreover have "pathstart f \<in> cbox a b"
   732         using assms(3) pathstart_in_path_image[of f]
   733         by auto
   734       then have "1 + b $ 1 \<le> pathstart f $ 1 \<Longrightarrow> False"
   735         unfolding mem_box_cart forall_2
   736         by auto
   737       then have "z$1 \<noteq> pathstart f$1"
   738         using prems(2) using assms ab
   739         by (auto simp add: field_simps)
   740       ultimately have *: "z$2 = a$2 - 2"
   741         using prems(1) by auto
   742       have "z$1 \<noteq> pathfinish g$1"
   743         using prems(2) assms ab
   744         by (auto simp add: field_simps *)
   745       moreover have "pathstart g \<in> cbox a b"
   746         using assms(4) pathstart_in_path_image[of g]
   747         by auto
   748       note this[unfolded mem_box_cart forall_2]
   749       then have "z$1 \<noteq> pathstart g$1"
   750         using prems(1) assms ab
   751         by (auto simp add: field_simps *)
   752       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"
   753         using prems(2)  unfolding * assms by (auto simp add: field_simps)
   754       then show False
   755         unfolding * using ab by auto
   756     qed
   757     then have "z \<in> path_image f \<or> z \<in> path_image g"
   758       using z unfolding Un_iff by blast
   759     then have z': "z \<in> cbox a b"
   760       using assms(3-4) by auto
   761     have "a $ 2 = z $ 2 \<Longrightarrow> (z $ 1 = pathstart f $ 1 \<or> z $ 1 = pathfinish f $ 1) \<Longrightarrow>
   762       z = pathstart f \<or> z = pathfinish f"
   763       unfolding vec_eq_iff forall_2 assms
   764       by auto
   765     with z' show "z \<in> path_image f"
   766       using z(1)
   767       unfolding Un_iff mem_box_cart forall_2
   768       by (simp only: segment_vertical segment_horizontal vector_2) (auto simp: assms)
   769     have "a $ 2 = z $ 2 \<Longrightarrow> (z $ 1 = pathstart g $ 1 \<or> z $ 1 = pathfinish g $ 1) \<Longrightarrow>
   770       z = pathstart g \<or> z = pathfinish g"
   771       unfolding vec_eq_iff forall_2 assms
   772       by auto
   773     with z' show "z \<in> path_image g"
   774       using z(2)
   775       unfolding Un_iff mem_box_cart forall_2
   776       by (simp only: segment_vertical segment_horizontal vector_2) (auto simp: assms)
   777   qed
   778 qed
   779 
   780 end