Theory HOL-Analysis.Fashoda_Theorem

(*  Author:     John Harrison
    Author:     Robert Himmelmann, TU Muenchen (translation from HOL light)
*)

section ‹Fashoda Meet Theorem›

theory Fashoda_Theorem
imports Brouwer_Fixpoint Path_Connected Cartesian_Euclidean_Space
begin

subsection ‹Bijections between intervals›

definitiontag important› interval_bij :: "'a × 'a  'a × 'a  'a  'a::euclidean_space"
  where "interval_bij =
    (λ(a, b) (u, v) x. (iBasis. (ui + (xi - ai) / (bi - ai) * (vi - ui)) *R i))"

lemma interval_bij_affine:
  "interval_bij (a,b) (u,v) = (λx. (iBasis. ((vi - ui) / (bi - ai) * (xi)) *R i) +
    (iBasis. (ui - (vi - ui) / (bi - ai) * (ai)) *R i))"
  by (simp add: interval_bij_def algebra_simps add_divide_distrib diff_divide_distrib flip: sum.distrib scaleR_add_left)


lemma continuous_interval_bij:
  fixes a b :: "'a::euclidean_space"
  shows "continuous (at x) (interval_bij (a, b) (u, v))"
  by (auto simp add: divide_inverse interval_bij_def intro!: continuous_sum continuous_intros)

lemma continuous_on_interval_bij: "continuous_on s (interval_bij (a, b) (u, v))"
  by (metis continuous_at_imp_continuous_on continuous_interval_bij)

lemma in_interval_interval_bij:
  fixes a b u v x :: "'a::euclidean_space"
  assumes "x  cbox a b"
    and "cbox u v  {}"
  shows "interval_bij (a, b) (u, v) x  cbox u v"
proof -
  have "i. i  Basis  u  i  u  i + (x  i - a  i) / (b  i - a  i) * (v  i - u  i)"
    by (smt (verit) assms box_ne_empty(1) divide_nonneg_nonneg mem_box(2) mult_nonneg_nonneg)
  moreover
  have "i. i  Basis  u  i + (x  i - a  i) / (b  i - a  i) * (v  i - u  i)  v  i"
    apply (simp add: divide_simps algebra_simps)
    by (smt (verit, best) assms box_ne_empty(1) left_diff_distrib mem_box(2) mult.commute mult_left_mono)
  ultimately show ?thesis
    by (force simp only: interval_bij_def split_conv mem_box inner_sum_left_Basis)
qed

lemma interval_bij_bij:
  "(i::'a::euclidean_space)Basis. ai < bi  ui < vi 
    interval_bij (a, b) (u, v) (interval_bij (u, v) (a, b) x) = x"
  by (auto simp: interval_bij_def euclidean_eq_iff[where 'a='a])

lemma interval_bij_bij_cart: fixes x::"real^'n" assumes "i. a$i < b$i  u$i < v$i"
  shows "interval_bij (a,b) (u,v) (interval_bij (u,v) (a,b) x) = x"
  using assms by (intro interval_bij_bij) (auto simp: Basis_vec_def inner_axis)


subsection ‹Fashoda meet theorem›

lemma infnorm_2:
  fixes x :: "real^2"
  shows "infnorm x = max ¦x$1¦ ¦x$2¦"
  unfolding infnorm_cart UNIV_2 by (rule cSup_eq) auto

lemma infnorm_eq_1_2:
  fixes x :: "real^2"
  shows "infnorm x = 1 
    ¦x$1¦  1  ¦x$2¦  1  (x$1 = -1  x$1 = 1  x$2 = -1  x$2 = 1)"
  unfolding infnorm_2 by auto

lemma infnorm_eq_1_imp:
  fixes x :: "real^2"
  assumes "infnorm x = 1"
  shows "¦x$1¦  1" and "¦x$2¦  1"
  using assms unfolding infnorm_eq_1_2 by auto

proposition fashoda_unit:
  fixes f g :: "real  real^2"
  assumes "f ` {-1 .. 1}  cbox (-1) 1"
    and "g ` {-1 .. 1}  cbox (-1) 1"
    and "continuous_on {-1 .. 1} f"
    and "continuous_on {-1 .. 1} g"
    and "f (- 1)$1 = - 1"
    and "f 1$1 = 1" "g (- 1) $2 = -1"
    and "g 1 $2 = 1"
  shows "s{-1 .. 1}. t{-1 .. 1}. f s = g t"
proof (rule ccontr)
  assume "¬ ?thesis"
  note as = this[unfolded bex_simps,rule_format]
  define sqprojection
    where [abs_def]: "sqprojection z = (inverse (infnorm z)) *R z" for z :: "real^2"
  define negatex :: "real^2  real^2"
    where "negatex x = (vector [-(x$1), x$2])" for x
  have inf_nega: "z::real^2. infnorm (negatex z) = infnorm z"
    unfolding negatex_def infnorm_2 vector_2 by auto
  have inf_eq1: "z. z  0  infnorm (sqprojection z) = 1"
    unfolding sqprojection_def infnorm_mul[unfolded scalar_mult_eq_scaleR]
    by (simp add: real_abs_infnorm infnorm_eq_0)
  let ?F = "λw::real^2. (f  (λx. x$1)) w - (g  (λx. x$2)) w"
  have *: "i. (λx::real^2. x $ i) ` cbox (- 1) 1 = {-1..1}"
  proof 
    show "(λx::real^2. x $ i) ` cbox (- 1) 1  {-1..1}" for i
      by (auto simp: mem_box_cart)
    show "{-1..1}  (λx::real^2. x $ i) ` cbox (- 1) 1" for i
      by (clarsimp simp: image_iff mem_box_cart Bex_def) (metis (no_types, opaque_lifting) vec_component)
  qed
  {
    fix x
    assume "x  (λw. (f  (λx. x $ 1)) w - (g  (λx. x $ 2)) w) ` (cbox (- 1) (1::real^2))"
    then obtain w :: "real^2" where w:
        "w  cbox (- 1) 1"
        "x = (f  (λx. x $ 1)) w - (g  (λx. x $ 2)) w"
      unfolding image_iff ..
    then have "x  0"
      using as[of "w$1" "w$2"] by (auto simp: mem_box_cart atLeastAtMost_iff)
  } note x0 = this
  let ?CB11 = "cbox (- 1) (1::real^2)"
  obtain x :: "real^2" where x:
      "x  cbox (- 1) 1"
      "(negatex  sqprojection  (λw. (f  (λx. x $ 1)) w - (g  (λx. x $ 2)) w)) x = x"
  proof (rule brouwer_weak[of ?CB11 "negatex  sqprojection  ?F"])
    show "compact ?CB11" "convex ?CB11"
      by (rule compact_cbox convex_box)+
    have "box (- 1) (1::real^2)  {}"
      unfolding interval_eq_empty_cart by auto
    then show "interior ?CB11  {}"
      by simp
    have "negatex (x + y) $ i = (negatex x + negatex y) $ i  negatex (c *R x) $ i = (c *R negatex x) $ i"
      for i x y c
      using exhaust_2 [of i] by (auto simp: negatex_def)
    then have "bounded_linear negatex"
      by (simp add: bounded_linearI' vec_eq_iff)
    then show "continuous_on ?CB11 (negatex  sqprojection  ?F)"
      unfolding sqprojection_def
      apply (intro continuous_intros continuous_on_component | use * assms in presburger)+
       apply (simp_all add: infnorm_eq_0 x0 linear_continuous_on)
      done
    have "(negatex  sqprojection  ?F) ` ?CB11  ?CB11"
    proof clarsimp
      fix y :: "real^2" 
      assume y: "y  ?CB11"
      have "?F y  0"
        by (rule x0) (use y in auto)
      then have *: "infnorm (sqprojection (?F y)) = 1"
        using inf_eq1 by blast
      show "negatex (sqprojection (f (y $ 1) - g (y $ 2)))  cbox (-1) 1"
        unfolding mem_box_cart interval_cbox_cart infnorm_2
        by (smt (verit, del_insts) "*" component_le_infnorm_cart inf_nega neg_one_index o_apply one_index)
    qed
    then show "negatex  sqprojection  ?F  ?CB11  ?CB11"
      by blast
  qed
  have "?F x  0"
    by (rule x0) (use x in auto)
  then have *: "infnorm (sqprojection (?F x)) = 1"
    using inf_eq1 by blast
  have nx: "infnorm x = 1"
    by (metis (no_types, lifting) "*" inf_nega o_apply x(2))
  have iff: "0 < sqprojection x$i  0 < x$i" "sqprojection x$i < 0  x$i < 0" if "x  0" for x i
  proof -
    have *: "inverse (infnorm x) > 0"
      by (simp add: infnorm_pos_lt that)
    then show "(0 < sqprojection x $ i) = (0 < x $ i)"
      by (simp add: sqprojection_def zero_less_mult_iff)
    show "(sqprojection x $ i < 0) = (x $ i < 0)"
      unfolding sqprojection_def
        by (metis * pos_less_divideR_eq scaleR_zero_right vector_scaleR_component)
  qed
  have x1: "x $ 1  {- 1..1::real}" "x $ 2  {- 1..1::real}"
    using x(1) unfolding mem_box_cart by auto
  then have nz: "f (x $ 1) - g (x $ 2)  0"
    using as by auto
  consider "x $ 1 = -1" | "x $ 1 = 1" | "x $ 2 = -1" | "x $ 2 = 1"
    using nx unfolding infnorm_eq_1_2 by auto
  then show False
  proof cases
    case 1
    then have *: "f (x $ 1) $ 1 = - 1"
      using assms(5) by auto
    have "sqprojection (f (x$1) - g (x$2)) $ 1 > 0"
      by (smt (verit) "1" negatex_def o_apply vector_2(1) x(2))
    moreover
    from x1 have "g (x $ 2)  cbox (-1) 1"
      using assms(2) by blast
    ultimately show False
      unfolding iff[OF nz] vector_component_simps * mem_box_cart
      using not_le by auto
  next
    case 2
    then have *: "f (x $ 1) $ 1 = 1"
      using assms(6) by auto
    have "sqprojection (f (x$1) - g (x$2)) $ 1 < 0"
      by (smt (verit) "2" negatex_def o_apply vector_2(1) x(2) zero_less_one)
    moreover have "g (x $ 2)  cbox (-1) 1"
      using assms(2) x1 by blast
    ultimately show False
      unfolding iff[OF nz] vector_component_simps * mem_box_cart
      using not_le by auto
  next
    case 3
    then have *: "g (x $ 2) $ 2 = - 1"
      using assms(7) by auto
    moreover have "sqprojection (f (x$1) - g (x$2)) $ 2 < 0"
      by (smt (verit, ccfv_SIG) "3" negatex_def o_apply vector_2(2) x(2))
    moreover from x1 have "f (x $ 1)  cbox (-1) 1"
      using assms(1) by blast
    ultimately show False
      by (smt (verit, del_insts) iff(2) mem_box_cart(2) neg_one_index nz vector_minus_component)
  next
    case 4
    then have *: "g (x $ 2) $ 2 = 1"
      using assms(8) by auto
    have "sqprojection (f (x$1) - g (x$2)) $ 2 > 0"
      by (smt (verit, best) "4" negatex_def o_apply vector_2(2) x(2))
    moreover
    from x1 have "f (x $ 1)  cbox (-1) 1"
      using assms(1) by blast
    ultimately show False
      by (smt (verit) "*" iff(1) mem_box_cart(2) nz one_index vector_minus_component)
  qed 
qed

proposition fashoda_unit_path:
  fixes f g :: "real  real^2"
  assumes "path f"
    and "path g"
    and "path_image f  cbox (-1) 1"
    and "path_image g  cbox (-1) 1"
    and "(pathstart f)$1 = -1"
    and "(pathfinish f)$1 = 1"
    and "(pathstart g)$2 = -1"
    and "(pathfinish g)$2 = 1"
  obtains z where "z  path_image f" and "z  path_image g"
proof -
  note assms = assms[unfolded path_def pathstart_def pathfinish_def path_image_def]
  define iscale where [abs_def]: "iscale z = inverse 2 *R (z + 1)" for z :: real
  have isc: "iscale ` {- 1..1}  {0..1}"
    unfolding iscale_def by auto
  have "s{- 1..1}. t{- 1..1}. (f  iscale) s = (g  iscale) t"
  proof (rule fashoda_unit)
    show "(f  iscale) ` {- 1..1}  cbox (- 1) 1" "(g  iscale) ` {- 1..1}  cbox (- 1) 1"
      using isc and assms(3-4) by (auto simp add: image_comp [symmetric])
    have *: "continuous_on {- 1..1} iscale"
      unfolding iscale_def by (rule continuous_intros)+
    show "continuous_on {- 1..1} (f  iscale)"
      using "*" assms(1) continuous_on_compose continuous_on_subset isc by blast
    show "continuous_on {- 1..1} (g  iscale)"
      by (meson "*" assms(2) continuous_on_compose continuous_on_subset isc)
    have *: "(1 / 2) *R (1 + (1::real^1)) = 1"
      unfolding vec_eq_iff by auto
    show "(f  iscale) (- 1) $ 1 = - 1"
      and "(f  iscale) 1 $ 1 = 1"
      and "(g  iscale) (- 1) $ 2 = -1"
      and "(g  iscale) 1 $ 2 = 1"
      unfolding o_def iscale_def using assms by (auto simp add: *)
  qed
  then obtain s t where st: "s  {- 1..1}" "t  {- 1..1}" "(f  iscale) s = (g  iscale) t"
    by auto
  show thesis
  proof
    show "f (iscale s)  path_image f"
      by (metis image_eqI image_subset_iff isc path_image_def st(1))
    show "f (iscale s)  path_image g"
      by (metis comp_def image_eqI image_subset_iff isc path_image_def st(2) st(3))
  qed
qed

theorem fashoda:
  fixes b :: "real^2"
  assumes "path f"
    and "path g"
    and "path_image f  cbox a b"
    and "path_image g  cbox a b"
    and "(pathstart f)$1 = a$1"
    and "(pathfinish f)$1 = b$1"
    and "(pathstart g)$2 = a$2"
    and "(pathfinish g)$2 = b$2"
  obtains z where "z  path_image f" and "z  path_image g"
proof -
  fix P Q S
  presume "P  Q  S" "P  thesis" and "Q  thesis" and "S  thesis"
  then show thesis
    by auto
next
  have "cbox a b  {}"
    using assms(3) using path_image_nonempty[of f] by auto
  then have "a  b"
    unfolding interval_eq_empty_cart less_eq_vec_def by (auto simp add: not_less)
  then show "a$1 = b$1  a$2 = b$2  (a$1 < b$1  a$2 < b$2)"
    unfolding less_eq_vec_def forall_2 by auto
next
  assume as: "a$1 = b$1"
  have "zpath_image g. z$2 = (pathstart f)$2"
  proof (rule connected_ivt_component_cart)
    show "pathstart g $ 2  pathstart f $ 2"
      by (metis assms(3) assms(7) mem_box_cart(2) pathstart_in_path_image subset_iff)
    show "pathstart f $ 2  pathfinish g $ 2"
      by (metis assms(3) assms(8) in_mono mem_box_cart(2) pathstart_in_path_image)
    show "connected (path_image g)"
      using assms(2) by blast
  qed (auto simp: path_defs)
  then obtain z :: "real^2" where z: "z  path_image g" "z $ 2 = pathstart f $ 2" ..
  have "z  cbox a b"
    using assms(4) z(1) by blast
  then have "z = f 0"
    by (smt (verit) as assms(5) exhaust_2 mem_box_cart(2) nle_le pathstart_def vec_eq_iff z(2))
  then show thesis
    by (metis path_defs(2) pathstart_in_path_image that z(1))
next
  assume as: "a$2 = b$2"
  have "zpath_image f. z$1 = (pathstart g)$1"
  proof (rule connected_ivt_component_cart)
    show "pathstart f $ 1  pathstart g $ 1"
      using assms(4) assms(5) mem_box_cart(2) by fastforce
    show "pathstart g $ 1  pathfinish f $ 1"
      using assms(4) assms(6) mem_box_cart(2) pathstart_in_path_image by fastforce
    show "connected (path_image f)"
      by (simp add: assms(1) connected_path_image)
  qed (auto simp: path_defs)
  then obtain z where z: "z  path_image f" "z $ 1 = pathstart g $ 1" ..
  have "z  cbox a b"
    using assms(3) z(1) by auto
  then have "z = g 0"
    by (smt (verit) as assms(7) exhaust_2 mem_box_cart(2) pathstart_def vec_eq_iff z(2))
  then show thesis
    by (metis path_defs(2) pathstart_in_path_image that z(1))
next
  assume as: "a $ 1 < b $ 1  a $ 2 < b $ 2"
  have int_nem: "cbox (-1) (1::real^2)  {}"
    unfolding interval_eq_empty_cart by auto
  obtain z :: "real^2" where z:
      "z  (interval_bij (a, b) (- 1, 1)  f) ` {0..1}"
      "z  (interval_bij (a, b) (- 1, 1)  g) ` {0..1}"
  proof (rule fashoda_unit_path)
    show "path (interval_bij (a, b) (- 1, 1)  f)"
      by (meson assms(1) continuous_on_interval_bij path_continuous_image)
    show "path (interval_bij (a, b) (- 1, 1)  g)"
      by (meson assms(2) continuous_on_interval_bij path_continuous_image)
    show "path_image (interval_bij (a, b) (- 1, 1)  f)  cbox (- 1) 1"
      using assms(3)
      by (simp add: path_image_def in_interval_interval_bij int_nem subset_eq)
    show "path_image (interval_bij (a, b) (- 1, 1)  g)  cbox (- 1) 1"
      using assms(4)
      by (simp add: path_image_def in_interval_interval_bij int_nem subset_eq)
    show "pathstart (interval_bij (a, b) (- 1, 1)  f) $ 1 = - 1"
         "pathfinish (interval_bij (a, b) (- 1, 1)  f) $ 1 = 1"
         "pathstart (interval_bij (a, b) (- 1, 1)  g) $ 2 = - 1"
         "pathfinish (interval_bij (a, b) (- 1, 1)  g) $ 2 = 1"
      using assms as
      by (simp_all add: cart_eq_inner_axis pathstart_def pathfinish_def interval_bij_def)
         (simp_all add: inner_axis)
  qed (auto simp: path_defs)
  then obtain zf zg where zf: "zf  {0..1}" "z = (interval_bij (a, b) (- 1, 1)  f) zf" 
                    and zg: "zg  {0..1}" "z = (interval_bij (a, b) (- 1, 1)  g) zg"
    by blast
  have *: "i. (- 1) $ i < (1::real^2) $ i  a $ i < b $ i"
    unfolding forall_2 using as by auto
  show thesis
  proof (rule_tac z="interval_bij (- 1,1) (a,b) z" in that)
    show "interval_bij (- 1, 1) (a, b) z  path_image f"
      using zf by (simp add: interval_bij_bij_cart[OF *] path_image_def)
    show "interval_bij (- 1, 1) (a, b) z  path_image g"
      using zg by (simp add: interval_bij_bij_cart[OF *] path_image_def)
  qed
qed


subsectiontag unimportant› ‹Some slightly ad hoc lemmas I use below›

lemma segment_vertical:
  fixes a :: "real^2"
  assumes "a$1 = b$1"
  shows "x  closed_segment a b 
    x$1 = a$1  x$1 = b$1  (a$2  x$2  x$2  b$2  b$2  x$2  x$2  a$2)"
  (is "_ = ?R")
proof -
  let ?L = "u. (x $ 1 = (1 - u) * a $ 1 + u * b $ 1  x $ 2 = (1 - u) * a $ 2 + u * b $ 2)  0  u  u  1"
  {
    presume "?L  ?R" and "?R  ?L"
    then show ?thesis
      unfolding closed_segment_def mem_Collect_eq
      unfolding vec_eq_iff forall_2 scalar_mult_eq_scaleR[symmetric] vector_component_simps
      by blast
  }
  {
    assume ?L
    then obtain u where u:
        "x $ 1 = (1 - u) * a $ 1 + u * b $ 1"
        "x $ 2 = (1 - u) * a $ 2 + u * b $ 2"
        "0  u" "u  1"
      by blast
    { fix b a
      assume "b + u * a > a + u * b"
      then have "(1 - u) * b > (1 - u) * a"
        by (auto simp add:field_simps)
      then have "b  a"
        using not_less_iff_gr_or_eq u(4) by fastforce
      then have "u * a  u * b"
        by (simp add: mult_left_mono u(3))
    } 
    moreover
    { fix a b
      assume "u * b > u * a"
      then have "(1 - u) * a  (1 - u) * b"
        using less_eq_real_def u(3) u(4) by force
      then have "a + u * b  b + u * a"
        by (auto simp add: field_simps)
    } ultimately show ?R
      by (force simp add: u assms field_simps not_le)
  }
  {
    assume ?R
    then show ?L
    proof (cases "x$2 = b$2")
      case True
      with ?R show ?L
        by (rule_tac x="(x$2 - a$2) / (b$2 - a$2)" in exI) (auto simp add: field_simps)
    next
      case False
      with ?R show ?L
          by (rule_tac x="1 - (x$2 - b$2) / (a$2 - b$2)" in exI) (auto simp add: field_simps)
    qed
  }
qed

text ‹Essentially duplicate proof that could be done by swapping co-ordinates›
lemma segment_horizontal:
  fixes a :: "real^2"
  assumes "a$2 = b$2"
  shows "x  closed_segment a b 
    x$2 = a$2  x$2 = b$2  (a$1  x$1  x$1  b$1  b$1  x$1  x$1  a$1)"
  (is "_ = ?R")
proof -
  let ?L = "u. (x $ 1 = (1 - u) * a $ 1 + u * b $ 1  x $ 2 = (1 - u) * a $ 2 + u * b $ 2)  0  u  u  1"
  {
    presume "?L  ?R" and "?R  ?L"
    then show ?thesis
      unfolding closed_segment_def mem_Collect_eq
      unfolding vec_eq_iff forall_2 scalar_mult_eq_scaleR[symmetric] vector_component_simps
      by blast
  }
  {
    assume ?L
    then obtain u where u:
        "x $ 1 = (1 - u) * a $ 1 + u * b $ 1"
        "x $ 2 = (1 - u) * a $ 2 + u * b $ 2"
        "0  u" "u  1"
      by blast
    { fix b a
      assume "b + u * a > a + u * b"
      then have "(1 - u) * b > (1 - u) * a"
        by (auto simp add: field_simps)
      then have "b  a"
        by (smt (verit, best) mult_left_mono u(4))
      then have "u * a  u * b"
        by (simp add: mult_left_mono u(3))
    } 
    moreover
    { fix a b
      assume "u * b > u * a"
      then have "(1 - u) * a  (1 - u) * b"
        using less_eq_real_def u(3) u(4) by force
      then have "a + u * b  b + u * a"
        by (auto simp add: field_simps)
    } 
    ultimately show ?R
      by (force simp add: u assms field_simps not_le intro: )
  }
  { assume ?R
    then show ?L
    proof (cases "x$1 = b$1")
      case True
      with ?R show ?L
        by (rule_tac x="(x$1 - a$1) / (b$1 - a$1)" in exI) (auto simp add: field_simps)
    next
      case False
      with ?R show ?L
        by (rule_tac x="1 - (x$1 - b$1) / (a$1 - b$1)" in exI) (auto simp add: field_simps)
    qed
  }
qed


subsection ‹Useful Fashoda corollary pointed out to me by Tom Hales›(*FIXME change title? *)

corollary fashoda_interlace:
  fixes a :: "real^2"
  assumes "path f"
    and "path g"
    and paf: "path_image f  cbox a b"
    and pag: "path_image g  cbox a b"
    and "(pathstart f)$2 = a$2"
    and "(pathfinish f)$2 = a$2"
    and "(pathstart g)$2 = a$2"
    and "(pathfinish g)$2 = a$2"
    and "(pathstart f)$1 < (pathstart g)$1"
    and "(pathstart g)$1 < (pathfinish f)$1"
    and "(pathfinish f)$1 < (pathfinish g)$1"
  obtains z where "z  path_image f" and "z  path_image g"
proof -
  have "cbox a b  {}"
    using path_image_nonempty[of f] using assms(3) by auto
  note ab=this[unfolded interval_eq_empty_cart not_ex forall_2 not_less]
  have "pathstart f  cbox a b"
    and "pathfinish f  cbox a b"
    and "pathstart g  cbox a b"
    and "pathfinish g  cbox a b"
    using pathstart_in_path_image pathfinish_in_path_image
    using assms(3-4)
    by auto
  note startfin = this[unfolded mem_box_cart 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])) 
      path_image (linepath(vector[(pathstart f)$1,a$2 - 2])(pathstart f))  path_image f 
      path_image (linepath(pathfinish f)(vector[(pathfinish f)$1,a$2 - 2])) 
      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))  path_image g 
      path_image(linepath(pathfinish g)(vector[(pathfinish g)$1,a$2 - 1])) 
      path_image(linepath(vector[(pathfinish g)$1,a$2 - 1])(vector[b$1 + 1,a$2 - 1])) 
      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)
  have abab: "cbox a b  cbox ?a ?b"
    unfolding interval_cbox_cart[symmetric]
    by (auto simp add:less_eq_vec_def forall_2)
  obtain z where
    "z  path_image
          (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]))"
    "z  path_image
          (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]))"
    apply (rule fashoda[of ?P1 ?P2 ?a ?b])
    unfolding pathstart_join pathfinish_join pathstart_linepath pathfinish_linepath vector_2
  proof -
    show "path ?P1" and "path ?P2"
      using assms by auto
    show "path_image ?P1  cbox ?a ?b" "path_image ?P2  cbox ?a ?b"
      unfolding P1P2 path_image_linepath using startfin paf pag
      by (auto simp: mem_box_cart segment_horizontal segment_vertical forall_2)
    show "a $ 1 - 2 = a $ 1 - 2"
      and "b $ 1 + 2 = b $ 1 + 2"
      and "pathstart g $ 2 - 3 = a $ 2 - 3"
      and "b $ 2 + 3 = b $ 2 + 3"
      by (auto simp add: assms)
  qed
  note z=this[unfolded P1P2 path_image_linepath]
  show thesis
  proof (rule that[of z])
    have "(z  closed_segment (vector [a $ 1 - 2, a $ 2 - 2]) (vector [pathstart f $ 1, a $ 2 - 2]) 
      z  closed_segment (vector [pathstart f $ 1, a $ 2 - 2]) (pathstart f)) 
      z  closed_segment (pathfinish f) (vector [pathfinish f $ 1, a $ 2 - 2]) 
      z  closed_segment (vector [pathfinish f $ 1, a $ 2 - 2]) (vector [b $ 1 + 2, a $ 2 - 2]) 
    (((z  closed_segment (vector [pathstart g $ 1, pathstart g $ 2 - 3]) (pathstart g)) 
      z  closed_segment (pathfinish g) (vector [pathfinish g $ 1, a $ 2 - 1])) 
      z  closed_segment (vector [pathfinish g $ 1, a $ 2 - 1]) (vector [b $ 1 + 1, a $ 2 - 1])) 
      z  closed_segment (vector [b $ 1 + 1, a $ 2 - 1]) (vector [b $ 1 + 1, b $ 2 + 3])  False"
    proof (simp only: segment_vertical segment_horizontal vector_2, goal_cases)
      case prems: 1
      have "pathfinish f  cbox a b"
        using assms(3) pathfinish_in_path_image[of f] by auto
      then have "1 + b $ 1  pathfinish f $ 1  False"
        unfolding mem_box_cart forall_2 by auto
      then have "z$1  pathfinish f$1"
        using assms(10) assms(11) prems(2) by auto
      moreover have "pathstart f  cbox a b"
        using assms(3) pathstart_in_path_image[of f]
        by auto
      then have "1 + b $ 1  pathstart f $ 1  False"
        unfolding mem_box_cart forall_2
        by auto
      then have "z$1  pathstart f$1"
        using prems(2) using assms ab
        by (auto simp add: field_simps)
      ultimately have *: "z$2 = a$2 - 2"
        using prems(1) by auto
      have "z$1  pathfinish g$1"
        using prems(2) assms ab
        by (auto simp add: field_simps *)
      moreover have "pathstart g  cbox a b"
        using assms(4) pathstart_in_path_image[of g]
        by auto
      note this[unfolded mem_box_cart forall_2]
      then have "z$1  pathstart g$1"
        using prems(1) assms ab
        by (auto simp add: field_simps *)
      ultimately have "a $ 2 - 1  z $ 2  z $ 2  b $ 2 + 3  b $ 2 + 3  z $ 2  z $ 2  a $ 2 - 1"
        using prems(2)  unfolding * assms by (auto simp add: field_simps)
      then show False
        unfolding * using ab by auto
    qed
    then have "z  path_image f  z  path_image g"
      using z unfolding Un_iff by blast
    then have z': "z  cbox a b"
      using assms(3-4) by auto
    have "a $ 2 = z $ 2  (z $ 1 = pathstart f $ 1  z $ 1 = pathfinish f $ 1) 
      z = pathstart f  z = pathfinish f"
      unfolding vec_eq_iff forall_2 assms
      by auto
    with z' show "z  path_image f"
      using z(1)
      unfolding Un_iff mem_box_cart forall_2
      using assms(5) assms(6) segment_horizontal segment_vertical by auto
    have "a $ 2 = z $ 2  (z $ 1 = pathstart g $ 1  z $ 1 = pathfinish g $ 1) 
      z = pathstart g  z = pathfinish g"
      unfolding vec_eq_iff forall_2 assms
      by auto
    with z' show "z  path_image g"
      using z(2)
      unfolding Un_iff mem_box_cart forall_2
      using assms(7) assms(8) segment_horizontal segment_vertical by auto
  qed
qed

end