# Theory 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›

definition✐‹tag important› interval_bij :: "'a × 'a ⇒ 'a × 'a ⇒ 'a ⇒ 'a::euclidean_space"
where "interval_bij =
(λ(a, b) (u, v) x. (∑i∈Basis. (u∙i + (x∙i - a∙i) / (b∙i - a∙i) * (v∙i - u∙i)) *⇩R i))"

lemma interval_bij_affine:
"interval_bij (a,b) (u,v) = (λx. (∑i∈Basis. ((v∙i - u∙i) / (b∙i - a∙i) * (x∙i)) *⇩R i) +
(∑i∈Basis. (u∙i - (v∙i - u∙i) / (b∙i - a∙i) * (a∙i)) *⇩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. a∙i < b∙i ∧ u∙i < v∙i ⟹
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 "∃z∈path_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 "∃z∈path_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)
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

subsection✐‹tag 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
```