# Theory Isometries

(*  Author:  Sébastien Gouëzel   sebastien.gouezel@univ-rennes1.fr
*)

section ‹Isometries›

theory Isometries
imports Library_Complements Hausdorff_Distance
begin

text ‹Isometries, i.e., functions that preserve distances, show up very often in mathematics.
We introduce a dedicated definition, and show its basic properties.›

definition isometry_on::"('a::metric_space) set ⇒ ('a ⇒ ('b::metric_space)) ⇒ bool"
where "isometry_on X f = (∀x ∈ X. ∀y ∈ X. dist (f x) (f y) = dist x y)"

definition isometry :: "('a::metric_space ⇒ 'b::metric_space) ⇒ bool"
where "isometry f ≡ isometry_on UNIV f ∧ range f = UNIV"

lemma isometry_on_subset:
assumes "isometry_on X f"
"Y ⊆ X"
shows "isometry_on Y f"
using assms unfolding isometry_on_def by auto

lemma isometry_onI [intro?]:
assumes "⋀x y. x ∈ X ⟹ y ∈ X ⟹ dist (f x) (f y) = dist x y"
shows "isometry_on X f"
using assms unfolding isometry_on_def by auto

lemma isometry_onD:
assumes "isometry_on X f"
"x ∈ X" "y ∈ X"
shows "dist (f x) (f y) = dist x y"
using assms unfolding isometry_on_def by auto

lemma isometryI [intro?]:
assumes "⋀x y. dist (f x) (f y) = dist x y"
"range f = UNIV"
shows "isometry f"
unfolding isometry_def isometry_on_def using assms by auto

lemma
assumes "isometry_on X f"
shows isometry_on_lipschitz: "1-lipschitz_on X f"
and isometry_on_uniformly_continuous: "uniformly_continuous_on X f"
and isometry_on_continuous: "continuous_on X f"
proof -
show "1-lipschitz_on X f" apply (rule lipschitz_onI) using isometry_onD[OF assms] by auto
then show "uniformly_continuous_on X f" "continuous_on X f"
using lipschitz_on_uniformly_continuous lipschitz_on_continuous_on by auto
qed

lemma isometryD:
assumes "isometry f"
shows "isometry_on UNIV f"
"dist (f x) (f y) = dist x y"
"range f = UNIV"
"1-lipschitz_on UNIV f"
"uniformly_continuous_on UNIV f"
"continuous_on UNIV f"
using assms unfolding isometry_def isometry_on_def apply auto
using isometry_on_lipschitz isometry_on_uniformly_continuous isometry_on_continuous assms unfolding isometry_def by blast+

lemma isometry_on_injective:
assumes "isometry_on X f"
shows "inj_on f X"
using assms inj_on_def isometry_on_def by force

lemma isometry_on_compose:
assumes "isometry_on X f"
"isometry_on (fX) g"
shows "isometry_on X (λx. g(f x))"
using assms unfolding isometry_on_def by auto

lemma isometry_on_cong:
assumes "isometry_on X f"
"⋀x. x ∈ X ⟹ g x = f x"
shows "isometry_on X g"
using assms unfolding isometry_on_def by auto

lemma isometry_on_inverse:
assumes "isometry_on X f"
shows "isometry_on (fX) (inv_into X f)"
"⋀x. x ∈ X ⟹ (inv_into X f) (f x) = x"
"⋀y. y ∈ fX ⟹ f (inv_into X f y) = y"
"bij_betw f X (fX)"
proof -
show *: "bij_betw f X (fX)"
using assms unfolding bij_betw_def inj_on_def isometry_on_def by force
show "isometry_on (fX) (inv_into X f)"
using assms unfolding isometry_on_def
by (auto) (metis (mono_tags, lifting) dist_eq_0_iff inj_on_def inv_into_f_f)
fix x assume "x ∈ X"
then show "(inv_into X f) (f x) = x"
using * by (simp add: bij_betw_def)
next
fix y assume "y ∈ fX"
then show "f (inv_into X f y) = y"
qed

lemma isometry_inverse:
assumes "isometry f"
shows "isometry (inv f)"
"bij f"
using isometry_on_inverse[OF isometryD(1)[OF assms]] isometryD(3)[OF assms]
unfolding isometry_def by (auto simp add: bij_imp_bij_inv bij_is_surj)

lemma isometry_on_homeomorphism:
assumes "isometry_on X f"
shows "homeomorphism X (fX) f (inv_into X f)"
"homeomorphism_on X f"
"X homeomorphic fX"
proof -
show *: "homeomorphism X (fX) f (inv_into X f)"
apply (rule homeomorphismI) using uniformly_continuous_imp_continuous[OF isometry_on_uniformly_continuous]
isometry_on_inverse[OF assms] assms by auto
then show "X homeomorphic fX"
unfolding homeomorphic_def by auto
show "homeomorphism_on X f"
unfolding homeomorphism_on_def using * by auto
qed

lemma isometry_homeomorphism:
fixes f::"('a::metric_space) ⇒ ('b::metric_space)"
assumes "isometry f"
shows "homeomorphism UNIV UNIV f (inv f)"
"(UNIV::'a set) homeomorphic (UNIV::'b set)"
using isometry_on_homeomorphism[OF isometryD(1)[OF assms]] isometryD(3)[OF assms] by auto

lemma isometry_on_closure:
assumes "isometry_on X f"
"continuous_on (closure X) f"
shows "isometry_on (closure X) f"
proof (rule isometry_onI)
fix x y assume "x ∈ closure X" "y ∈ closure X"
obtain u v::"nat ⇒ 'a" where *: "⋀n. u n ∈ X" "u ⇢ x"
"⋀n. v n ∈ X" "v ⇢ y"
using ‹x ∈ closure X› ‹y ∈ closure X› unfolding closure_sequential by blast
have "(λn. f (u n)) ⇢ f x"
using *(1) *(2) ‹x ∈ closure X› ‹continuous_on (closure X) f›
unfolding comp_def continuous_on_closure_sequentially[of X f] by auto
moreover have "(λn. f (v n)) ⇢ f y"
using *(3) *(4) ‹y ∈ closure X› ‹continuous_on (closure X) f›
unfolding comp_def continuous_on_closure_sequentially[of X f] by auto
ultimately have "(λn. dist (f (u n)) (f (v n))) ⇢ dist (f x) (f y)"
then have "(λn. dist (u n) (v n)) ⇢ dist (f x) (f y)"
using assms(1) *(1) *(3) unfolding isometry_on_def by auto
moreover have "(λn. dist (u n) (v n)) ⇢ dist x y"
using *(2) *(4) by (simp add: tendsto_dist)
ultimately show "dist (f x) (f y) = dist x y" using LIMSEQ_unique by auto
qed

lemma isometry_extend_closure:
fixes f::"('a::metric_space) ⇒ ('b::complete_space)"
assumes "isometry_on X f"
shows "∃g. isometry_on (closure X) g ∧ (∀x∈X. g x = f x)"
proof -
obtain g where g: "⋀x. x ∈ X ⟹ g x = f x" "uniformly_continuous_on (closure X) g"
using uniformly_continuous_on_extension_on_closure[OF isometry_on_uniformly_continuous[OF assms]] by metis
have "isometry_on (closure X) g"
apply (rule isometry_on_closure, rule isometry_on_cong[OF assms])
using g uniformly_continuous_imp_continuous[OF g(2)] by auto
then show ?thesis using g(1) by auto
qed

lemma isometry_on_complete_image:
assumes "isometry_on X f"
"complete X"
shows "complete (fX)"
proof (rule completeI)
fix u :: "nat ⇒ 'b" assume u: "∀n. u n ∈ fX" "Cauchy u"
define v where "v = (λn. inv_into X f (u n))"
have "v n ∈ X" for n
unfolding v_def by (simp add: inv_into_into u(1))
have "dist (v n) (v m) = dist (u n) (u m)" for m n
using u(1) isometry_on_inverse[OF ‹isometry_on X f›] unfolding isometry_on_def v_def by (auto simp add: inv_into_into)
then have "Cauchy v"
using u(2) unfolding Cauchy_def by auto
obtain l where "l ∈ X" "v ⇢ l"
apply (rule completeE[OF ‹complete X› _ ‹Cauchy v›]) using ‹⋀n. v n ∈ X› by auto
have "(λn. f (v n)) ⇢ f l"
apply (rule continuous_on_tendsto_compose[OF isometry_on_continuous[OF ‹isometry_on X f›]])
using ‹⋀n. v n ∈ X› ‹l ∈ X› ‹v ⇢ l› by auto
moreover have "f(v n) = u n" for n
unfolding v_def by (simp add: f_inv_into_f u(1))
ultimately have "u ⇢ f l" by auto
then show "∃m ∈ fX. u ⇢ m" using ‹l ∈ X› by auto
qed

lemma isometry_on_id [simp]:
"isometry_on A (λx. x)"
"isometry_on A id"
unfolding isometry_on_def by auto

"isometry_on A (λx. x + (t::'a::real_normed_vector))"
unfolding isometry_on_def by auto

lemma isometry_on_minus [simp]:
"isometry_on A (λ(x::'a::real_normed_vector). -x)"
unfolding isometry_on_def by (auto simp add: dist_minus)

lemma isometry_on_diff [simp]:
"isometry_on A (λx. (t::'a::real_normed_vector) - x)"

lemma isometry_preserves_bounded:
assumes "isometry_on X f"
"A ⊆ X"
shows "bounded (fA) ⟷ bounded A"
unfolding bounded_two_points using assms(2) isometry_onD[OF assms(1)] by auto (metis assms(2) rev_subsetD)+

lemma isometry_preserves_infdist:
"infdist (f x) (fA) = infdist x A"
if "isometry_on X f" "A ⊆ X" "x ∈ X"
using that by (simp add: infdist_def image_comp isometry_on_def subset_iff)

lemma isometry_preserves_hausdorff_distance:
"hausdorff_distance (fA) (fB) = hausdorff_distance A B"
if "isometry_on X f" "A ⊆ X" "B ⊆ X"
using that isometry_preserves_infdist [OF that(1) that(2)]
isometry_preserves_infdist [OF that(1) that(3)]
isometry_preserves_bounded [OF that(1) that(2)]
isometry_preserves_bounded [OF that(1) that(3)]
by (simp add: hausdorff_distance_def image_comp subset_eq)

lemma isometry_on_UNIV_iterates:
fixes f::"('a::metric_space) ⇒ 'a"
assumes "isometry_on UNIV f"
shows "isometry_on UNIV (f^^n)"
by (induction n, auto, rule isometry_on_compose[of _ _ f], auto intro: isometry_on_subset[OF assms])

lemma isometry_iterates:
fixes f::"('a::metric_space) ⇒ 'a"
assumes "isometry f"
shows "isometry (f^^n)"
using isometry_on_UNIV_iterates[OF isometryD(1)[OF assms], of n] bij_fn[OF isometry_inverse(2)[OF assms], of n]
unfolding isometry_def by (simp add: bij_is_surj)

section ‹Geodesic spaces›

text ‹A geodesic space is a metric space in which any pair of points can be joined by a geodesic segment,
i.e., an isometrically embedded copy of a segment in the real line. Most spaces in geometry are
geodesic. We introduce in this section the corresponding class of metric spaces. First, we study
properties of general geodesic segments in metric spaces.›

subsection ‹Geodesic segments in general metric spaces›

definition geodesic_segment_between::"('a::metric_space) set ⇒ 'a ⇒ 'a ⇒ bool"
where "geodesic_segment_between G x y = (∃g::(real ⇒ 'a). g 0 = x ∧ g (dist x y) = y ∧ isometry_on {0..dist x y} g ∧ G = g{0..dist x y})"

definition geodesic_segment::"('a::metric_space) set ⇒ bool"
where "geodesic_segment G = (∃x y. geodesic_segment_between G x y)"

text ‹We also introduce the parametrization of a geodesic segment. It is convenient to use the
following definition, which guarantees that the point is on $G$ even without checking that $G$
is a geodesic segment or that the parameter is in the reasonable range: this shortens some
arguments below.›

definition geodesic_segment_param::"('a::metric_space) set ⇒ 'a ⇒ real ⇒ 'a"
where "geodesic_segment_param G x t = (if ∃w. w ∈ G ∧ dist x w = t then SOME w. w ∈ G ∧ dist x w = t else SOME w. w ∈ G)"

lemma geodesic_segment_betweenI:
assumes "g 0 = x" "g (dist x y) = y" "isometry_on {0..dist x y} g" "G = g{0..dist x y}"
shows "geodesic_segment_between G x y"
unfolding geodesic_segment_between_def apply (rule exI[of _ g]) using assms by auto

lemma geodesic_segmentI [intro, simp]:
assumes "geodesic_segment_between G x y"
shows "geodesic_segment G"
unfolding geodesic_segment_def using assms by auto

lemma geodesic_segmentI2 [intro]:
assumes "isometry_on {a..b} g" "a ≤ (b::real)"
shows "geodesic_segment_between (g{a..b}) (g a) (g b)"
"geodesic_segment (g{a..b})"
proof -
define h where "h = (λt. g (t+a))"
have *: "isometry_on {0..b-a} h"
apply (rule isometry_onI)
using ‹isometry_on {a..b} g› ‹a ≤ b› by (auto simp add: isometry_on_def h_def)
have **: "dist (h 0) (h (b-a)) = b-a"
using isometry_onD[OF ‹isometry_on {0..b-a} h›, of 0 "b-a"] ‹a ≤ b› unfolding dist_real_def by auto
have "geodesic_segment_between (h{0..b-a}) (h 0) (h (b-a))"
unfolding geodesic_segment_between_def apply (rule exI[of _ h]) unfolding ** using * by auto
moreover have "g{a..b} = h{0..b-a}"
unfolding h_def apply (auto simp add: image_iff)
moreover have "h 0 = g a" "h (b-a) = g b" unfolding h_def by auto
ultimately show "geodesic_segment_between (g{a..b}) (g a) (g b)" by auto
then show "geodesic_segment (g{a..b})" unfolding geodesic_segment_def by auto
qed

lemma geodesic_segmentD:
assumes "geodesic_segment_between G x y"
shows "∃g::(real ⇒ _). (g t = x ∧ g (t + dist x y) = y ∧ isometry_on {t..t+dist x y} g ∧ G = g{t..t+dist x y})"
proof -
obtain h where h: "h 0 = x" "h (dist x y) = y" "isometry_on {0..dist x y} h" "G = h{0..dist x y}"
by (meson ‹geodesic_segment_between G x y› geodesic_segment_between_def)
have * [simp]: "(λx. x - t)  {t..t + dist x y} = {0..dist x y}" by auto
define g where "g = (λs. h (s - t))"
have "g t = x" "g (t + dist x y) = y" using h assms(1) unfolding g_def by auto
moreover have "isometry_on {t..t+dist x y} g"
unfolding g_def apply (rule isometry_on_compose[of _ _ h])
moreover have "g {t..t + dist x y} = G" unfolding g_def h(4) using * by (metis image_image)
ultimately show ?thesis by auto
qed

lemma geodesic_segment_endpoints [simp]:
assumes "geodesic_segment_between G x y"
shows "x ∈ G" "y ∈ G" "G ≠ {}"
using assms unfolding geodesic_segment_between_def
by (auto, metis atLeastAtMost_iff image_eqI less_eq_real_def zero_le_dist)

lemma geodesic_segment_commute:
assumes "geodesic_segment_between G x y"
shows "geodesic_segment_between G y x"
proof -
obtain g::"real⇒'a" where g: "g 0 = x" "g (dist x y) = y" "isometry_on {0..dist x y} g" "G = g{0..dist x y}"
by (meson ‹geodesic_segment_between G x y› geodesic_segment_between_def)
define h::"real⇒'a" where "h = (λt. g(dist x y-t))"
have "(λt. dist x y -t){0..dist x y} = {0..dist x y}" by auto
then have "h{0..dist x y} = G" unfolding g(4) h_def by (metis image_image)
moreover have "h 0 = y" "h (dist x y) = x" unfolding h_def using g by auto
moreover have "isometry_on {0..dist x y} h"
unfolding h_def apply (rule isometry_on_compose[of _ _ g]) using g(3) by auto
ultimately show ?thesis
unfolding geodesic_segment_between_def by (auto simp add: dist_commute)
qed

lemma geodesic_segment_dist:
assumes "geodesic_segment_between G x y" "a ∈ G"
shows "dist x a + dist a y = dist x y"
proof -
obtain g where g: "g 0 = x" "g (dist x y) = y" "isometry_on {0..dist x y} g" "G = g{0..dist x y}"
by (meson ‹geodesic_segment_between G x y› geodesic_segment_between_def)
obtain t where t: "t ∈ {0..dist x y}" "a = g t"
using g(4) assms by auto
have "dist x a = t" using isometry_onD[OF g(3) _ t(1), of 0]
unfolding g(1) dist_real_def t(2) using t(1) by auto
moreover have "dist a y = dist x y - t" using isometry_onD[OF g(3) _ t(1), of "dist x y"]
unfolding g(2) dist_real_def t(2) using t(1) by (auto simp add: dist_commute)
ultimately show ?thesis by auto
qed

lemma geodesic_segment_dist_unique:
assumes "geodesic_segment_between G x y" "a ∈ G" "b ∈ G" "dist x a = dist x b"
shows "a = b"
proof -
obtain g where g: "g 0 = x" "g (dist x y) = y" "isometry_on {0..dist x y} g" "G = g{0..dist x y}"
by (meson ‹geodesic_segment_between G x y› geodesic_segment_between_def)
obtain ta where ta: "ta ∈ {0..dist x y}" "a = g ta"
using g(4) assms by auto
have *: "dist x a = ta"
unfolding g(1)[symmetric] ta(2) using isometry_onD[OF g(3), of 0 ta]
unfolding dist_real_def using ta(1) by auto
obtain tb where tb: "tb ∈ {0..dist x y}" "b = g tb"
using g(4) assms by auto
have "dist x b = tb"
unfolding g(1)[symmetric] tb(2) using isometry_onD[OF g(3), of 0 tb]
unfolding dist_real_def using tb(1) by auto
then have "ta = tb" using * ‹dist x a = dist x b› by auto
then show "a = b" using ta(2) tb(2) by auto
qed

lemma geodesic_segment_union:
assumes "dist x z = dist x y + dist y z"
"geodesic_segment_between G x y" "geodesic_segment_between H y z"
shows "geodesic_segment_between (G ∪ H) x z"
"G ∩ H = {y}"
proof -
obtain g where g: "g 0 = x" "g (dist x y) = y" "isometry_on {0..dist x y} g" "G = g{0..dist x y}"
by (meson ‹geodesic_segment_between G x y› geodesic_segment_between_def)
obtain h where h: "h (dist x y) = y" "h (dist x z) = z" "isometry_on {dist x y..dist x z} h" "H = h{dist x y..dist x z}"
unfolding ‹dist x z = dist x y + dist y z›
using geodesic_segmentD[OF ‹geodesic_segment_between H y z›, of "dist x y"] by auto
define f where "f = (λt. if t ≤ dist x y then g t else h t)"
have fg: "f t = g t" if "t ≤ dist x y" for t
unfolding f_def using that by auto
have fh: "f t = h t" if "t ≥ dist x y" for t
unfolding f_def apply (cases "t > dist x y") using that g(2) h(1) by auto

have "f 0 = x" "f (dist x z) = z" using fg fh g(1) h(2) assms(1) by auto

have "f{0..dist x z} = f{0..dist x y} ∪ f{dist x y..dist x z}"
unfolding assms(1) image_Un[symmetric] by (simp add: ivl_disj_un_two_touch(4))
moreover have "f{0..dist x y} = G"
unfolding g(4) using fg image_cong by force
moreover have "f{dist x y..dist x z} = H"
unfolding h(4) using fh image_cong by force
ultimately have "f{0..dist x z} = G ∪ H" by simp

have Ifg: "dist (f s) (f t) = s-t" if "0 ≤ t" "t ≤ s" "s ≤ dist x y" for s t
using that fg[of s] fg[of t] isometry_onD[OF g(3), of s t] unfolding dist_real_def by auto
have Ifh: "dist (f s) (f t) = s-t" if "dist x y ≤ t" "t ≤ s" "s ≤ dist x z" for s t
using that fh[of s] fh[of t] isometry_onD[OF h(3), of s t] unfolding dist_real_def by auto

have I: "dist (f s) (f t) = s-t" if "0 ≤ t" "t ≤ s" "s ≤ dist x z" for s t
proof -
consider "t ≤ dist x y ∧ s ≥ dist x y" | "s ≤ dist x y" | "t ≥ dist x y" by fastforce
then show ?thesis
proof (cases)
case 1
have "dist (f t) (f s) ≤ dist (f t) (f (dist x y)) + dist (f (dist x y)) (f s)"
using dist_triangle by auto
also have "... ≤ (dist x y - t) + (s - dist x y)"
using that 1 Ifg[of t "dist x y"] Ifh[of "dist x y" s] by (auto simp add: dist_commute intro: mono_intros)
finally have *: "dist (f t) (f s) ≤ s - t" by simp

have "dist x z ≤ dist (f 0) (f t) + dist (f t) (f s) + dist (f s) (f (dist x z))"
unfolding ‹f 0 = x› ‹f (dist x z) = z› using dist_triangle4 by auto
also have "... ≤ t + dist (f t) (f s) + (dist x z - s)"
using that 1 Ifg[of 0 t] Ifh[of s "dist x z"] by (auto simp add: dist_commute intro: mono_intros)
finally have "s - t ≤ dist (f t) (f s)" by auto
then show "dist (f s) (f t) = s-t" using * dist_commute by auto
next
case 2
then show ?thesis using Ifg that by auto
next
case 3
then show ?thesis using Ifh that by auto
qed
qed
have "isometry_on {0..dist x z} f"
unfolding isometry_on_def dist_real_def using I
by (auto, metis abs_of_nonneg dist_commute dist_real_def le_cases zero_le_dist)
then show "geodesic_segment_between (G ∪ H) x z"
unfolding geodesic_segment_between_def
using ‹f 0 = x› ‹f (dist x z) = z› ‹f{0..dist x z} = G ∪ H› by auto
have "G ∩ H ⊆ {y}"
proof (auto)
fix a assume a: "a ∈ G" "a ∈ H"
obtain s where s: "s ∈ {0..dist x y}" "a = g s" using a g(4) by auto
obtain t where t: "t ∈ {dist x y..dist x z}" "a = h t" using a h(4) by auto
have "a = f s" using fg s by auto
moreover have "a = f t" using fh t by auto
ultimately have "s = t" using isometry_onD[OF ‹isometry_on {0..dist x z} f›, of s t] s(1) t(1) by auto
then have "s = dist x y" using s t by auto
then show "a = y" using s(2) g by auto
qed
then show "G ∩ H = {y}" using assms by auto
qed

lemma geodesic_segment_dist_le:
assumes "geodesic_segment_between G x y" "a ∈ G" "b ∈ G"
shows "dist a b ≤ dist x y"
proof -
obtain g where g: "g 0 = x" "g (dist x y) = y" "isometry_on {0..dist x y} g" "G = g{0..dist x y}"
by (meson ‹geodesic_segment_between G x y› geodesic_segment_between_def)
obtain s t where st: "s ∈ {0..dist x y}" "t ∈ {0..dist x y}" "a = g s" "b = g t"
using g(4) assms by auto
have "dist a b = abs(s-t)" using isometry_onD[OF g(3) st(1) st(2)]
unfolding st(3) st(4) dist_real_def by simp
then show "dist a b ≤ dist x y" using st(1) st(2) unfolding dist_real_def by auto
qed

lemma geodesic_segment_param [simp]:
assumes "geodesic_segment_between G x y"
shows "geodesic_segment_param G x 0 = x"
"geodesic_segment_param G x (dist x y) = y"
"t ∈ {0..dist x y} ⟹ geodesic_segment_param G x t ∈ G"
"isometry_on {0..dist x y} (geodesic_segment_param G x)"
"(geodesic_segment_param G x){0..dist x y} = G"
"t ∈ {0..dist x y} ⟹ dist x (geodesic_segment_param G x t) = t"
"s ∈ {0..dist x y} ⟹ t ∈ {0..dist x y} ⟹ dist (geodesic_segment_param G x s) (geodesic_segment_param G x t) = abs(s-t)"
"z ∈ G ⟹ z = geodesic_segment_param G x (dist x z)"
proof -
obtain g::"real⇒'a" where g: "g 0 = x" "g (dist x y) = y" "isometry_on {0..dist x y} g" "G = g{0..dist x y}"
by (meson ‹geodesic_segment_between G x y› geodesic_segment_between_def)
have *: "g t ∈ G ∧ dist x (g t) = t" if "t ∈ {0..dist x y}" for t
using isometry_onD[OF g(3), of 0 t] that g(1) g(4) unfolding dist_real_def by auto
have G: "geodesic_segment_param G x t = g t" if "t ∈ {0..dist x y}" for t
proof -
have A: "geodesic_segment_param G x t ∈ G ∧ dist x (geodesic_segment_param G x t) = t"
using *[OF that] unfolding geodesic_segment_param_def apply auto
using *[OF that] by (metis (mono_tags, lifting) someI)+
obtain s where s: "geodesic_segment_param G x t = g s" "s ∈ {0..dist x y}"
using A g(4) by auto
have "s = t" using *[OF ‹s ∈ {0..dist x y}›] A unfolding s(1) by auto
then show ?thesis using s by auto
qed
show "geodesic_segment_param G x 0 = x"
"geodesic_segment_param G x (dist x y) = y"
"t ∈ {0..dist x y} ⟹ geodesic_segment_param G x t ∈ G"
"isometry_on {0..dist x y} (geodesic_segment_param G x)"
"(geodesic_segment_param G x){0..dist x y} = G"
"t ∈ {0..dist x y} ⟹ dist x (geodesic_segment_param G x t) = t"
"s ∈ {0..dist x y} ⟹ t ∈ {0..dist x y} ⟹ dist (geodesic_segment_param G x s) (geodesic_segment_param G x t) = abs(s-t)"
"z ∈ G ⟹ z = geodesic_segment_param G x (dist x z)"
using G g apply (auto simp add: rev_image_eqI)
using G isometry_on_cong * atLeastAtMost_iff apply blast
using G isometry_on_cong * atLeastAtMost_iff apply blast
by (auto simp add: * dist_real_def isometry_onD)
qed

lemma geodesic_segment_param_in_segment:
assumes "G ≠ {}"
shows "geodesic_segment_param G x t ∈ G"
unfolding geodesic_segment_param_def
apply (auto, metis (mono_tags, lifting) someI)
using assms some_in_eq by fastforce

lemma geodesic_segment_reverse_param:
assumes "geodesic_segment_between G x y"
"t ∈ {0..dist x y}"
shows "geodesic_segment_param G y (dist x y - t) = geodesic_segment_param G x t"
proof -
have * [simp]: "geodesic_segment_between G y x"
using geodesic_segment_commute[OF assms(1)] by simp
have "geodesic_segment_param G y (dist x y - t) ∈ G"
apply (rule geodesic_segment_param(3)[of _ _ x])
using assms(2) by (auto simp add: dist_commute)
moreover have "dist (geodesic_segment_param G y (dist x y - t)) x = t"
using geodesic_segment_param(2)[OF *] geodesic_segment_param(7)[OF *, of "dist x y -t" "dist x y"] assms(2) by (auto simp add: dist_commute)
moreover have "geodesic_segment_param G x t ∈ G"
apply (rule geodesic_segment_param(3)[OF assms(1)])
using assms(2) by auto
moreover have "dist (geodesic_segment_param G x t) x = t"
using geodesic_segment_param(6)[OF assms] by (simp add: dist_commute)
ultimately show ?thesis
using geodesic_segment_dist_unique[OF assms(1)] by (simp add: dist_commute)
qed

lemma dist_along_geodesic_wrt_endpoint:
assumes "geodesic_segment_between G x y"
"u ∈ G" "v ∈ G"
shows "dist u v = abs(dist u x - dist v x)"
proof -
have *: "u = geodesic_segment_param G x (dist x u)" "v = geodesic_segment_param G x (dist x v)"
using assms by auto
have "dist u v = dist (geodesic_segment_param G x (dist x u)) (geodesic_segment_param G x (dist x v))"
using * by auto
also have "... = abs(dist x u - dist x v)"
apply (rule geodesic_segment_param(7)[OF assms(1)]) using assms apply auto
using geodesic_segment_dist_le geodesic_segment_endpoints(1) by blast+
finally show ?thesis by (simp add: dist_commute)
qed

text ‹One often needs to restrict a geodesic segment to a subsegment. We introduce the tools
to express this conveniently.›
definition geodesic_subsegment::"('a::metric_space) set ⇒ 'a ⇒ real ⇒ real ⇒ 'a set"
where "geodesic_subsegment G x s t = G ∩ {z. dist x z ≥ s ∧ dist x z ≤ t}"

text ‹A subsegment is always contained in the original segment.›
lemma geodesic_subsegment_subset:
"geodesic_subsegment G x s t ⊆ G"
unfolding geodesic_subsegment_def by simp

text ‹A subsegment is indeed a geodesic segment, and its endpoints and parametrization can be
expressed in terms of the original segment.›
lemma geodesic_subsegment:
assumes "geodesic_segment_between G x y"
"0 ≤ s" "s ≤ t" "t ≤ dist x y"
shows "geodesic_subsegment G x s t = (geodesic_segment_param G x){s..t}"
"geodesic_segment_between (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (geodesic_segment_param G x t)"
"⋀u. s ≤ u ⟹ u ≤ t ⟹ geodesic_segment_param (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (u - s) = geodesic_segment_param G x u"
proof -
show A: "geodesic_subsegment G x s t = (geodesic_segment_param G x){s..t}"
proof (auto)
fix y assume y: "y ∈ geodesic_subsegment G x s t"
have "y = geodesic_segment_param G x (dist x y)"
apply (rule geodesic_segment_param(8)[OF assms(1)])
using y geodesic_subsegment_subset by force
moreover have "dist x y ≥ s ∧ dist x y ≤ t"
using y unfolding geodesic_subsegment_def by auto
ultimately show "y ∈ geodesic_segment_param G x  {s..t}" by auto
next
fix u assume H: "s ≤ u" "u ≤ t"
have *: "dist x (geodesic_segment_param G x u) = u"
apply (rule geodesic_segment_param(6)[OF assms(1)]) using H assms by auto
show "geodesic_segment_param G x u ∈ geodesic_subsegment G x s t"
unfolding geodesic_subsegment_def
using geodesic_segment_param_in_segment[OF geodesic_segment_endpoints(3)[OF assms(1)]] by (auto simp add: * H)
qed

have *: "isometry_on {s..t} (geodesic_segment_param G x)"
by (rule isometry_on_subset[of "{0..dist x y}"]) (auto simp add: assms)
show B: "geodesic_segment_between (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (geodesic_segment_param G x t)"
unfolding A apply (rule geodesic_segmentI2) using * assms by auto

fix u assume u: "s ≤ u" "u ≤ t"
show "geodesic_segment_param (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (u - s) = geodesic_segment_param G x u"
proof (rule geodesic_segment_dist_unique[OF B])
show "geodesic_segment_param (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (u - s) ∈ geodesic_subsegment G x s t"
by (rule geodesic_segment_param_in_segment[OF geodesic_segment_endpoints(3)[OF B]])
show "geodesic_segment_param G x u ∈ geodesic_subsegment G x s t"
unfolding A using u by auto
have "dist (geodesic_segment_param G x s) (geodesic_segment_param (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (u - s)) = u - s"
using B assms u by auto
moreover have "dist (geodesic_segment_param G x s) (geodesic_segment_param G x u) = u -s"
using assms u by auto
ultimately show "dist (geodesic_segment_param G x s) (geodesic_segment_param (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (u - s)) =
dist (geodesic_segment_param G x s) (geodesic_segment_param G x u)"
by simp
qed
qed

text ‹The parameterizations of a segment and a subsegment sharing an endpoint coincide where defined.›
lemma geodesic_segment_subparam:
assumes "geodesic_segment_between G x z" "geodesic_segment_between H x y" "H ⊆ G" "t ∈ {0..dist x y}"
shows "geodesic_segment_param G x t = geodesic_segment_param H x t"
proof -
have "geodesic_segment_param H x t ∈ G"
using assms(3) geodesic_segment_param(3)[OF assms(2) assms(4)] by auto
then have "geodesic_segment_param H x t = geodesic_segment_param G x (dist x (geodesic_segment_param H x t))"
using geodesic_segment_param(8)[OF assms(1)] by auto
then show ?thesis using geodesic_segment_param(6)[OF assms(2) assms(4)] by auto
qed

text ‹A segment contains a subsegment between any of its points›
lemma geodesic_subsegment_exists:
assumes "geodesic_segment G" "x ∈ G" "y ∈ G"
shows "∃H. H ⊆ G ∧ geodesic_segment_between H x y"
proof -
obtain a0 b0 where Ga0b0: "geodesic_segment_between G a0 b0"
using assms(1) unfolding geodesic_segment_def by auto
text ‹Permuting the endpoints if necessary, we can ensure that the first endpoint $a$ is closer
to $x$ than $y$.›
have "∃ a b. geodesic_segment_between G a b ∧ dist x a ≤ dist y a"
proof (cases "dist x a0 ≤ dist y a0")
case True
show ?thesis
apply (rule exI[of _ a0], rule exI[of _ b0]) using True Ga0b0 by auto
next
case False
show ?thesis
apply (rule exI[of _ b0], rule exI[of _ a0])
using Ga0b0 geodesic_segment_commute geodesic_segment_dist[OF Ga0b0 ‹x ∈ G›] geodesic_segment_dist[OF Ga0b0 ‹y ∈ G›] False
qed
then obtain a b where Gab: "geodesic_segment_between G a b" "dist x a ≤ dist y a"
by auto
have *: "0 ≤ dist x a" "dist x a ≤ dist y a" "dist y a ≤ dist a b"
using Gab assms by (meson geodesic_segment_dist_le geodesic_segment_endpoints(1) zero_le_dist)+
have **: "x = geodesic_segment_param G a (dist x a)" "y = geodesic_segment_param G a (dist y a)"
using Gab ‹x ∈ G› ‹y ∈ G› by (metis dist_commute geodesic_segment_param(8))+
define H where "H = geodesic_subsegment G a (dist x a) (dist y a)"
have "H ⊆ G"
unfolding H_def by (rule geodesic_subsegment_subset)
moreover have "geodesic_segment_between H x y"
unfolding H_def using geodesic_subsegment(2)[OF Gab(1) *] ** by auto
ultimately show ?thesis by auto
qed

text ‹A geodesic segment is homeomorphic to an interval.›
lemma geodesic_segment_homeo_interval:
assumes "geodesic_segment_between G x y"
shows "{0..dist x y} homeomorphic G"
proof -
obtain g where g: "g 0 = x" "g (dist x y) = y" "isometry_on {0..dist x y} g" "G = g{0..dist x y}"
by (meson ‹geodesic_segment_between G x y› geodesic_segment_between_def)
show ?thesis using isometry_on_homeomorphism(3)[OF g(3)] unfolding g(4) by simp
qed

text ‹Just like an interval, a geodesic segment is compact, connected, path connected, bounded,
closed, nonempty, and proper.›
lemma geodesic_segment_topology:
assumes "geodesic_segment G"
shows "compact G" "connected G" "path_connected G" "bounded G" "closed G" "G ≠ {}" "proper G"
proof -
show "compact G"
using assms geodesic_segment_homeo_interval homeomorphic_compactness
unfolding geodesic_segment_def by force
show "path_connected G"
using assms is_interval_path_connected geodesic_segment_homeo_interval homeomorphic_path_connectedness
unfolding geodesic_segment_def
by (metis is_interval_cc)
then show "connected G"
using path_connected_imp_connected by auto
show "bounded G"
by (rule compact_imp_bounded, fact)
show "closed G"
by (rule compact_imp_closed, fact)
show "G ≠ {}"
using assms geodesic_segment_def geodesic_segment_endpoints(3) by auto
show "proper G"
using proper_of_compact ‹compact G› by auto
qed

lemma geodesic_segment_between_x_x [simp]:
"geodesic_segment_between {x} x x"
"geodesic_segment {x}"
"geodesic_segment_between G x x ⟷ G = {x}"
proof -
show *: "geodesic_segment_between {x} x x"
unfolding geodesic_segment_between_def apply (rule exI[of _ "λ_. x"]) unfolding isometry_on_def by auto
then show "geodesic_segment {x}" by auto
show "geodesic_segment_between G x x ⟷ G = {x}"
using geodesic_segment_dist_le geodesic_segment_endpoints(2) * by fastforce
qed

lemma geodesic_segment_disconnection:
assumes "geodesic_segment_between G x y" "z ∈ G"
shows "(connected (G - {z})) = (z = x ∨ z = y)"
proof -
obtain g where g: "g 0 = x" "g (dist x y) = y" "isometry_on {0..dist x y} g" "G = g{0..dist x y}"
by (meson ‹geodesic_segment_between G x y› geodesic_segment_between_def)
obtain t where t: "t ∈ {0..dist x y}" "z = g t" using ‹z ∈ G› g(4) by auto
have "({0..dist x y} - {t}) homeomorphic (G - {g t})"
proof -
have *: "isometry_on ({0..dist x y} - {t}) g"
apply (rule isometry_on_subset[OF g(3)]) by auto
have "({0..dist x y} - {t}) homeomorphic g({0..dist x y} - {t})"
by (rule isometry_on_homeomorphism(3)[OF *])
moreover have "g({0..dist x y} - {t}) = G - {g t}"
unfolding g(4) using isometry_on_injective[OF g(3)] t by (auto simp add: inj_onD)
ultimately show ?thesis by auto
qed
moreover have "connected({0..dist x y} - {t}) = (t = 0 ∨ t = dist x y)"
using t(1) by (auto simp add: connected_iff_interval, fastforce)
ultimately have "connected (G - {z}) = (t = 0 ∨ t = dist x y)"
unfolding ‹z = g t›[symmetric]using homeomorphic_connectedness by blast
moreover have "(t = 0 ∨ t = dist x y) = (z = x ∨ z = y)"
using t g apply auto
by (metis atLeastAtMost_iff isometry_on_inverse(2) order_refl zero_le_dist)+
ultimately show ?thesis by auto
qed

lemma geodesic_segment_unique_endpoints:
assumes "geodesic_segment_between G x y"
"geodesic_segment_between G a b"
shows "{x, y} = {a, b}"
by (metis geodesic_segment_disconnection assms(1) assms(2) doubleton_eq_iff geodesic_segment_endpoints(1) geodesic_segment_endpoints(2))

lemma geodesic_segment_subsegment:
assumes "geodesic_segment G" "H ⊆ G" "compact H" "connected H" "H ≠ {}"
shows "geodesic_segment H"
proof -
obtain x y where "geodesic_segment_between G x y"
using assms unfolding geodesic_segment_def by auto
obtain g where g: "g 0 = x" "g (dist x y) = y" "isometry_on {0..dist x y} g" "G = g{0..dist x y}"
by (meson ‹geodesic_segment_between G x y› geodesic_segment_between_def)
define L where "L = (inv_into {0..dist x y} g)H"
have "L ⊆ {0..dist x y}"
unfolding L_def using isometry_on_inverse[OF ‹isometry_on {0..dist x y} g›] assms(2) g(4) by auto
have "isometry_on G (inv_into {0..dist x y} g)"
using isometry_on_inverse[OF ‹isometry_on {0..dist x y} g›] g(4) by auto
then have "isometry_on H (inv_into {0..dist x y} g)"
using ‹H ⊆ G› isometry_on_subset by auto
then have "H homeomorphic L" unfolding L_def using isometry_on_homeomorphism(3) by auto
then have "compact L ∧ connected L"
using assms homeomorphic_compactness homeomorphic_connectedness by blast
then obtain a b where "L = {a..b}"
using connected_compact_interval_1[of L] by auto
have "a ≤ b" using ‹H ≠ {}› ‹L = {a..b}› unfolding L_def by auto
then have "0 ≤ a" "b ≤ dist x y" using ‹L ⊆ {0..dist x y}› ‹L = {a..b}› by auto
have *: "H = g{a..b}"
by (metis L_def ‹L = {a..b}› assms(2) g(4) image_inv_into_cancel)
show "geodesic_segment H"
unfolding * apply (rule geodesic_segmentI2[OF _ ‹a ≤ b›])
apply (rule isometry_on_subset[OF g(3)]) using ‹0 ≤ a› ‹b ≤ dist x y› by auto
qed

text ‹The image under an isometry of a geodesic segment is still obviously a geodesic segment.›
lemma isometry_preserves_geodesic_segment_between:
assumes "isometry_on X f"
"G ⊆ X" "geodesic_segment_between G x y"
shows "geodesic_segment_between (fG) (f x) (f y)"
proof -
obtain g where g: "g 0 = x" "g (dist x y) = y" "isometry_on {0..dist x y} g" "G = g{0..dist x y}"
by (meson ‹geodesic_segment_between G x y› geodesic_segment_between_def)
then have *: "fG = (f o g) {0..dist x y}" "f x = (f o g) 0" "f y = (f o g) (dist x y)"
by auto
show ?thesis
unfolding * apply (intro geodesic_segmentI2(1))
unfolding comp_def apply (rule isometry_on_compose[of _ g])
using g(3) g(4) assms by (auto intro: isometry_on_subset)
qed

text ‹The sum of distances $d(w, x) + d(w, y)$ can be controlled using the distance from $w$
to a geodesic segment between $x$ and $y$.›
lemma geodesic_segment_distance:
assumes "geodesic_segment_between G x y"
shows "dist w x + dist w y ≤ dist x y + 2 * infdist w G"
proof -
have "∃z ∈ G. infdist w G = dist w z"
apply (rule infdist_proper_attained) using assms by (auto simp add: geodesic_segment_topology)
then obtain z where z: "z ∈ G" "infdist w G = dist w z" by auto
have "dist w x + dist w y ≤ (dist w z + dist z x) + (dist w z + dist z y)"
by (intro mono_intros)
also have "... = dist x z + dist z y + 2 * dist w z"
also have "... = dist x y + 2 * infdist w G"
using z(1) assms geodesic_segment_dist unfolding z(2) by auto
finally show ?thesis by auto
qed

text ‹If a point $y$ is on a geodesic segment between $x$ and its closest projection $p$ on a set $A$,
then $p$ is also a closest projection of $y$, and the closest projection set of $y$ is contained in
that of $x$.›

lemma proj_set_geodesic_same_basepoint:
assumes "p ∈ proj_set x A" "geodesic_segment_between G p x" "y ∈ G"
shows "p ∈ proj_set y A"
proof (rule proj_setI)
show "p ∈ A"
using assms proj_setD by auto
have *: "dist y p ≤ dist y q" if "q ∈ A" for q
proof -
have "dist p y + dist y x = dist p x"
using assms geodesic_segment_dist by blast
also have "... ≤ dist q x"
using proj_set_dist_le[OF ‹q ∈ A› assms(1)] by (simp add: dist_commute)
also have "... ≤ dist q y + dist y x"
by (intro mono_intros)
finally show ?thesis
qed
have "dist y p ≤ Inf (dist y  A)"
apply (rule cINF_greatest) using ‹p ∈ A› * by auto
then show "dist y p ≤ infdist y A"
unfolding infdist_def using ‹p ∈ A› by auto
qed

lemma proj_set_subset:
assumes "p ∈ proj_set x A" "geodesic_segment_between G p x" "y ∈ G"
shows "proj_set y A ⊆ proj_set x A"
proof -
have "z ∈ proj_set x A" if "z ∈ proj_set y A" for z
proof (rule proj_setI)
show "z ∈ A" using that proj_setD by auto
have "dist x z ≤ dist x y + dist y z"
by (intro mono_intros)
also have "... ≤ dist x y + dist y p"
using proj_set_dist_le[OF proj_setD(1)[OF ‹p ∈ proj_set x A›] that] by auto
also have "... = dist x p"
using assms geodesic_segment_commute geodesic_segment_dist by blast
also have "... = infdist x A"
using proj_setD(2)[OF assms(1)] by simp
finally show "dist x z ≤ infdist x A"
by simp
qed
then show ?thesis by auto
qed

lemma proj_set_thickening:
assumes "p ∈ proj_set x Z"
"0 ≤ D"
"D ≤ dist p x"
"geodesic_segment_between G p x"
shows "geodesic_segment_param G p D ∈ proj_set x (⋃z∈Z. cball z D)"
proof (rule proj_setI')
have "dist p (geodesic_segment_param G p D) = D"
using geodesic_segment_param(7)[OF assms(4), of 0 D]
unfolding geodesic_segment_param(1)[OF assms(4)] using assms by simp
then show "geodesic_segment_param G p D ∈ (⋃z∈Z. cball z D)"
using proj_setD(1)[OF ‹p ∈ proj_set x Z›] by force
show "dist x (geodesic_segment_param G p D) ≤ dist x y" if "y ∈ (⋃z∈Z. cball z D)" for y
proof -
obtain z where y: "y ∈ cball z D" "z ∈ Z" using ‹y ∈ (⋃z∈Z. cball z D)› by auto
have "dist (geodesic_segment_param G p D) x + D = dist p x"
using geodesic_segment_param(7)[OF assms(4), of D "dist p x"]
unfolding geodesic_segment_param(2)[OF assms(4)] using assms by simp
also have "... ≤ dist z x"
using proj_setD(2)[OF ‹p ∈ proj_set x Z›] infdist_le[OF ‹z ∈ Z›, of x] by (simp add: dist_commute)
also have "... ≤ dist z y + dist y x"
by (intro mono_intros)
also have "... ≤ D + dist y x"
using y by simp
finally show ?thesis by (simp add: dist_commute)
qed
qed

lemma proj_set_thickening':
assumes "p ∈ proj_set x Z"
"0 ≤ D"
"D ≤ E"
"E ≤ dist p x"
"geodesic_segment_between G p x"
shows "geodesic_segment_param G p D ∈ proj_set (geodesic_segment_param G p E) (⋃z∈Z. cball z D)"
proof -
define H where "H = geodesic_subsegment G p D (dist p x)"
have H1: "geodesic_segment_between H (geodesic_segment_param G p D) x"
apply (subst geodesic_segment_param(2)[OF ‹geodesic_segment_between G p x›, symmetric])
unfolding H_def apply (rule geodesic_subsegment(2)) using assms by auto
have H2: "geodesic_segment_param G p E ∈ H"
unfolding H_def using assms geodesic_subsegment(1) by force
have "geodesic_segment_param G p D ∈ proj_set x (⋃z∈Z. cball z D)"
apply (rule proj_set_thickening) using assms by auto
then show ?thesis
by (rule proj_set_geodesic_same_basepoint[OF _ H1 H2])
qed

text ‹It is often convenient to use \emph{one} geodesic between $x$ and $y$, even if it is not unique.
We introduce a notation for such a choice of a geodesic, denoted \verb+{x--S--y}+ for such a geodesic
that moreover remains in the set $S$. We also enforce
the condition \verb+{x--S--y} = {y--S--x}+. When there is no such geodesic, we simply take
\verb+{x--S--y} = {x, y}+ for definiteness. It would be even better to enforce that, if
$a$ is on \verb+{x--S--y}+, then \verb+{x--S--y}+ is the union of \verb+{x--S--a}+ and \verb+{a--S--y}+, but
I do not know if such a choice is always possible -- such a choice of geodesics is
called a geodesic bicombing.
We also write \verb+{x--y}+ for \verb+{x--UNIV--y}+.›

definition some_geodesic_segment_between::"'a::metric_space ⇒ 'a set ⇒ 'a ⇒ 'a set" ("(1{_--_--_})")
where "some_geodesic_segment_between = (SOME f. ∀ x y S. f x S y = f y S x
∧ (if (∃G. geodesic_segment_between G x y ∧ G ⊆ S) then (geodesic_segment_between (f x S y) x y ∧ (f x S y ⊆ S))
else f x S y = {x, y}))"

abbreviation some_geodesic_segment_between_UNIV::"'a::metric_space ⇒ 'a ⇒ 'a set" ("(1{_--_})")
where "some_geodesic_segment_between_UNIV x y ≡ {x--UNIV--y}"

text ‹We prove that there is such a choice of geodesics, compatible with direction reversal. What
we do is choose arbitrarily a geodesic between $x$ and $y$ if it exists, and then use the geodesic
between $\min(x, y)$ and $\max(x,y)$, for any total order on the space, to ensure that we get the
same result from $x$ to $y$ or from $y$ to $x$.›

lemma some_geodesic_segment_between_exists:
"∃f. ∀ x y S. f x S y = f y S x
∧ (if (∃G. geodesic_segment_between G x y ∧ G ⊆ S) then (geodesic_segment_between (f x S y) x y ∧ (f x S y ⊆ S))
else f x S y = {x, y})"
proof -
define g::"'a ⇒ 'a set ⇒ 'a ⇒ 'a set" where
"g = (λx S y. if (∃G. geodesic_segment_between G x y ∧ G ⊆ S) then (SOME G. geodesic_segment_between G x y ∧ G ⊆ S) else {x, y})"
have g1: "geodesic_segment_between (g x S y) x y ∧ (g x S y ⊆ S)" if "∃G. geodesic_segment_between G x y ∧ G ⊆ S" for x y S
unfolding g_def using someI_ex[OF that] by auto
have g2: "g x S y = {x, y}" if "¬(∃G. geodesic_segment_between G x y ∧ G ⊆ S)" for x y S
unfolding g_def using that by auto
obtain r::"'a rel" where r: "well_order_on UNIV r"
using well_order_on by auto
have A: "x = y" if "(x, y) ∈ r" "(y, x) ∈ r" for x y
using r that unfolding well_order_on_def linear_order_on_def partial_order_on_def antisym_def by auto
have B: "(x, y) ∈ r ∨ (y, x) ∈ r" for x y
using r unfolding well_order_on_def linear_order_on_def total_on_def partial_order_on_def preorder_on_def refl_on_def by force

define f where "f = (λx S y. if (x, y) ∈ r then g x S y else g y S x)"
have "f x S y = f y S x" for x y S unfolding f_def using r A B by auto
moreover have "geodesic_segment_between (f x S y) x y ∧ (f x S y ⊆ S)" if "∃G. geodesic_segment_between G x y ∧ G ⊆ S" for x y S
unfolding f_def using g1 geodesic_segment_commute that by smt
moreover have "f x S y = {x, y}" if "¬(∃G. geodesic_segment_between G x y ∧ G ⊆ S)" for x y S
unfolding f_def using g2 that geodesic_segment_commute doubleton_eq_iff by metis
ultimately show ?thesis by metis
qed

lemma some_geodesic_commute:
"{x--S--y} = {y--S--x}"
unfolding some_geodesic_segment_between_def by (auto simp add: someI_ex[OF some_geodesic_segment_between_exists])

lemma some_geodesic_segment_description:
"(∃G. geodesic_segment_between G x y ∧ G ⊆ S) ⟹ geodesic_segment_between {x--S--y} x y"
"(¬(∃G. geodesic_segment_between G x y ∧ G ⊆ S)) ⟹ {x--S--y} = {x, y}"
unfolding some_geodesic_segment_between_def by (simp add: someI_ex[OF some_geodesic_segment_between_exists])+

text ‹Basic topological properties of our chosen set of geodesics.›

lemma some_geodesic_compact [simp]:
"compact {x--S--y}"
apply (cases "∃G. geodesic_segment_between G x y ∧ G ⊆ S")
using some_geodesic_segment_description[of x y] geodesic_segment_topology[of "{x--S--y}"] geodesic_segment_def apply auto
by blast

lemma some_geodesic_closed [simp]:
"closed {x--S--y}"
by (rule compact_imp_closed[OF some_geodesic_compact[of x S y]])

lemma some_geodesic_bounded [simp]:
"bounded {x--S--y}"
by (rule compact_imp_bounded[OF some_geodesic_compact[of x S y]])

lemma some_geodesic_endpoints [simp]:
"x ∈ {x--S--y}" "y ∈ {x--S--y}" "{x--S--y} ≠ {}"
apply (cases "∃G. geodesic_segment_between G x y ∧ G ⊆ S") using some_geodesic_segment_description[of x y S] apply auto
apply (cases "∃G. geodesic_segment_between G x y ∧ G ⊆ S") using some_geodesic_segment_description[of x y S] apply auto
apply (cases "∃G. geodesic_segment_between G x y ∧ G ⊆ S") using geodesic_segment_endpoints(3) by (auto, blast)

lemma some_geodesic_subsegment:
assumes "H ⊆ {x--S--y}" "compact H" "connected H" "H ≠ {}"
shows "geodesic_segment H"
apply (cases "∃G. geodesic_segment_between G x y ∧ G ⊆ S")
using some_geodesic_segment_description[of x y] geodesic_segment_subsegment[OF _ assms] geodesic_segment_def apply auto[1]
using some_geodesic_segment_description[of x y] assms
by (metis connected_finite_iff_sing finite.emptyI finite.insertI finite_subset geodesic_segment_between_x_x(2))

lemma some_geodesic_in_subset:
assumes "x ∈ S" "y ∈ S"
shows "{x--S--y} ⊆ S"
apply (cases "∃G. geodesic_segment_between G x y ∧ G ⊆ S")
unfolding some_geodesic_segment_between_def by (simp add: assms someI_ex[OF some_geodesic_segment_between_exists])+

lemma some_geodesic_same_endpoints [simp]:
"{x--S--x} = {x}"
apply (cases "∃G. geodesic_segment_between G x x ∧ G ⊆ S")
apply (meson geodesic_segment_between_x_x(3) some_geodesic_segment_description(1))

subsection ‹Geodesic subsets›

text ‹A subset is \emph{geodesic} if any two of its points can be joined by a geodesic segment.
We prove basic properties of such a subset in this paragraph -- notably connectedness. A basic
example is given by convex subsets of vector spaces, as closed segments are geodesic.›

definition geodesic_subset::"('a::metric_space) set ⇒ bool"
where "geodesic_subset S = (∀x∈S. ∀y∈S. ∃G. geodesic_segment_between G x y ∧ G ⊆ S)"

lemma geodesic_subsetD:
assumes "geodesic_subset S" "x ∈ S" "y ∈ S"
shows "geodesic_segment_between {x--S--y} x y"
using assms some_geodesic_segment_description(1) unfolding geodesic_subset_def by blast

lemma geodesic_subsetI:
assumes "⋀x y. x ∈ S ⟹ y ∈ S ⟹ ∃G. geodesic_segment_between G x y ∧ G ⊆ S"
shows "geodesic_subset S"
using assms unfolding geodesic_subset_def by auto

lemma geodesic_subset_empty:
"geodesic_subset {}"
using geodesic_subsetI by auto

lemma geodesic_subset_singleton:
"geodesic_subset {x}"
by (auto intro!: geodesic_subsetI geodesic_segment_between_x_x(1))

lemma geodesic_subset_path_connected:
assumes "geodesic_subset S"
shows "path_connected S"
proof -
have "∃g. path g ∧ path_image g ⊆ S ∧ pathstart g = x ∧ pathfinish g = y" if "x ∈ S" "y ∈ S" for x y
proof -
define G where "G = {x--S--y}"
have *: "geodesic_segment_between G x y" "G ⊆ S" "x ∈ G" "y ∈ G"
using assms that by (auto simp add: G_def geodesic_subsetD some_geodesic_in_subset that(1) that(2))
then have "path_connected G"
using geodesic_segment_topology(3) unfolding geodesic_segment_def by auto
then have "∃g. path g ∧ path_image g ⊆ G ∧ pathstart g = x ∧ pathfinish g = y"
using * unfolding path_connected_def by auto
then show ?thesis using ‹G ⊆ S› by auto
qed
then show ?thesis
unfolding path_connected_def by auto
qed

text ‹To show that a segment in a normed vector space is geodesic, we will need to use its
length parametrization, which is given in the next lemma.›

lemma closed_segment_as_isometric_image:
"((λt. x + (t/dist x y) *⇩R (y - x)){0..dist x y}) = closed_segment x y"
proof (auto simp add: closed_segment_def image_iff)
fix t assume H: "0 ≤ t" "t ≤ dist x y"
show "∃u. x + (t / dist x y) *⇩R (y - x) = (1 - u) *⇩R x + u *⇩R y ∧ 0 ≤ u ∧ u ≤ 1"
apply (rule exI[of _ "t/dist x y"])
using H apply (auto simp add: algebra_simps divide_simps)
done
next
fix u::real assume H: "0 ≤ u" "u ≤ 1"
show "∃t∈{0..dist x y}. (1 - u) *⇩R x + u *⇩R y = x + (t / dist x y) *⇩R (y - x)"
apply (rule bexI[of _ "u * dist x y"])
using H by (auto simp add: algebra_simps mult_left_le_one_le)
qed

proposition closed_segment_is_geodesic:
fixes x y::"'a::real_normed_vector"
shows "isometry_on {0..dist x y} (λt. x + (t/dist x y) *⇩R (y - x))"
"geodesic_segment_between (closed_segment x y) x y"
"geodesic_segment (closed_segment x y)"
proof -
show *: "isometry_on {0..dist x y} (λt. x + (t/dist x y) *⇩R (y - x))"
unfolding isometry_on_def dist_norm
apply (cases "x = y")
by (auto simp add: scaleR_diff_left[symmetric] diff_divide_distrib[symmetric] norm_minus_commute)
show "geodesic_segment_between (closed_segment x y) x y"
unfolding closed_segment_as_isometric_image[symmetric]
apply (rule geodesic_segment_betweenI[OF _ _ *]) by auto
then show "geodesic_segment (closed_segment x y)"
by auto
qed

text ‹We deduce that a convex set is geodesic.›

proposition convex_is_geodesic:
assumes "convex (S::'a::real_normed_vector set)"
shows "geodesic_subset S"
proof (rule geodesic_subsetI)
fix x y assume H: "x ∈ S" "y ∈ S"
show "∃G. geodesic_segment_between G x y ∧ G ⊆ S"
apply (rule exI[of _ "closed_segment x y"])
using H assms convex_contains_segment by blast
qed

subsection ‹Geodesic spaces›

text ‹In this subsection, we define geodesic spaces (metric spaces in which there is a geodesic
segment joining any pair of points). We specialize the previous statements on geodesic segments to
these situations.›

class geodesic_space = metric_space +
assumes geodesic: "geodesic_subset (UNIV::('a::metric_space) set)"

text ‹The simplest example of a geodesic space is a real normed vector space. Significant examples
also include graphs (with the graph distance), Riemannian manifolds, and $CAT(\kappa)$ spaces.›

instance real_normed_vector ⊆ geodesic_space

lemma (in geodesic_space) some_geodesic_is_geodesic_segment [simp]:
"geodesic_segment_between {x--y} x (y::'a)"
"geodesic_segment {x--y}"
using some_geodesic_segment_description(1)[of x y] geodesic_subsetD[OF geodesic] by (auto, blast)

lemma (in geodesic_space) some_geodesic_connected [simp]:
"connected {x--y}" "path_connected {x--y}"
by (auto intro!: geodesic_segment_topology)

text ‹In geodesic spaces, we restate as simp rules all properties of the geodesic segment
parametrizations.›

lemma (in geodesic_space) geodesic_segment_param_in_geodesic_spaces [simp]:
"geodesic_segment_param {x--y} x 0 = x"
"geodesic_segment_param {x--y} x (dist x y) = y"
"t ∈ {0..dist x y} ⟹ geodesic_segment_param {x--y} x t ∈ {x--y}"
"isometry_on {0..dist x y} (geodesic_segment_param {x--y} x)"
"(geodesic_segment_param {x--y} x){0..dist x y} = {x--y}"
"t ∈ {0..dist x y} ⟹ dist x (geodesic_segment_param {x--y} x t) = t"
"s ∈ {0..dist x y} ⟹ t ∈ {0..dist x y} ⟹ dist (geodesic_segment_param {x--y} x s) (geodesic_segment_param {x--y} x t) = abs(s-t)"
"z ∈ {x--y} ⟹ z = geodesic_segment_param {x--y} x (dist x z)"
using geodesic_segment_param[OF some_geodesic_is_geodesic_segment(1)[of x y]] by auto

subsection ‹Uniquely geodesic spaces›

text ‹In this subsection, we define uniquely geodesic spaces, i.e., geodesic spaces in which,
additionally, there is a unique geodesic between any pair of points.›

class uniquely_geodesic_space = geodesic_space +
assumes uniquely_geodesic: "⋀x y G H. geodesic_segment_between G x y ⟹ geodesic_segment_between H x y ⟹ G = H"

text ‹To prove that a geodesic space is uniquely geodesic, it suffices to show that there is no loop,
i.e., if two geodesic segments intersect only at their endpoints, then they coincide.

Indeed, assume this holds, and consider two geodesics with the same endpoints. If they differ at
some time $t$, then consider the last time $a$ before $t$ where they coincide, and the first time
$b$ after $t$ where they coincide. Then the restrictions of the two geodesics to $[a,b]$ give

lemma (in geodesic_space) uniquely_geodesic_spaceI:
assumes "⋀G H x (y::'a). geodesic_segment_between G x y ⟹ geodesic_segment_between H x y ⟹ G ∩ H = {x, y} ⟹ x = y"
"geodesic_segment_between G x y" "geodesic_segment_between H x (y::'a)"
shows "G = H"
proof -
obtain g where g: "g 0 = x" "g (dist x y) = y" "isometry_on {0..dist x y} g" "G = g{0..dist x y}"
by (meson ‹geodesic_segment_between G x y› geodesic_segment_between_def)
obtain h where h: "h 0 = x" "h (dist x y) = y" "isometry_on {0..dist x y} h" "H = h{0..dist x y}"
by (meson ‹geodesic_segment_between H x y› geodesic_segment_between_def)
have "g t = h t" if "t ∈ {0..dist x y}" for t
proof (rule ccontr)
assume "g t ≠ h t"
define Z where "Z = {s ∈ {0..dist x y}. g s = h s}"
have "0 ∈ Z" "dist x y ∈ Z" unfolding Z_def using g h by auto
have "t ∉ Z" unfolding Z_def using ‹g t ≠ h t› by