# Theory Bonk_Schramm_Extension

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

section ‹The Bonk Schramm extension›

theory Bonk_Schramm_Extension
imports Morse_Gromov_Theorem
begin

text ‹We want to show that any metric space is isometrically embedded in a
metric space which is geodesic (i.e., there is an embedded geodesic between any
two points) and complete. There are many such constructions, but a very interesting one
has been given by Bonk and Schramm in~\<^cite>‹"bonk_schramm"›, together with an additional property of the
completion: if the space is delta-hyperbolic (in the sense of Gromov), then its
completion also is, with the same constant delta. It follows in particular that a $0$-hyperbolic
space embeds in a $0$-hyperbolic geodesic space, i.e., a metric tree (there is an easier
direct construction in this case).

Another embedding of a metric space in a geodesic one is constructed by Mineyev~\<^cite>‹"mineyev"›,
it is more canonical in a sense (isometries of the original space extend
to the new space), but it is not clear if it preserves hyperbolicity.

The argument of Bonk and Schramm goes as follows:
- first, if one wants to add the middle of a pair of points $a$ and $b$ in a space $E$, there is a
nice formula for the distance on a new space $E \cup \{*\}$ (where $*$ will by construction be a middle
of $a$ and $b$).
- by transfinite induction on all the pair of points in the space, one adds
all the missing middles
- then one completes the space
- then one adds all the middles
- then one goes on like that, transfinitely many times
- at some point, the process stops for cardinality reasons

The resulting space is complete and has middles for all pairs of points. It is then
standard that it is geodesic (this is proved in \verb+Geodesic_Spaces.thy+).

Implementing this construction in Isabelle is interesting and nontrivial,
as transfinite induction is not that easy, especially when intermingled with metric completion
(i.e., taking the quotient space of all Cauchy sequences). In particular, taking sequences of
metric completions would mean changing types at each step, along a transfinite number of steps.
It does not seem possible to do it naively in this way.

We avoid taking quotients in the middle of the argument, as this is too messy.
Instead, we define a pseudo-distance (i.e., a function satisyfing the
triangular inequality, but such that $d(x,y)$ can vanish even if $x$ and $y$ are different)
on an increasing set, which should contain middles and limits of Cauchy sequences
(identified with their defining Cauchy sequence). Thus, we consider a datatype containing
points in the original space and closed under two operations: taking a pair of points in the datatype
(we think of the resulting pair as the middle of the pair) and taking a sequence with
values in the datatype (we think of the resulting sequence as the limit of the sequence if
it is Cauchy, for a distance yet to be defined, and as something we discard if the sequence
is not Cauchy).

Defining such an object is apparently not trivial. However, it is
well defined, for cardinality reasons, as this process will end
after the continuum cardinality iterations (as a sequence taking value in the continuum
cardinality is in fact contained in a strictly smaller ordinal, which means that all
sequences in the construction will appear at a step strictly before the continuum cardinality).
The datatype construction in Isabelle/HOL contains these cardinality considerations
as an automatic process, and is thus able to construct the datatype directly,
without the need for any additional proof!

Then, we define a wellorder on the datatype, such that every middle and every sequence appear
after each of its ancestors. This construction of a wellorder should work for any datatype,
but we provide a naive proof in our use case.

Then, we define, inductively on $z$, a pseudodistance on the pair of points in
$\{x : x \leq z\}$. In the induction, one should add one point at a time. If it is
a middle, one uses the Bonk-Schramm recipe. If it is a sequence, then either the sequence
is Cauchy and one uses the limit of the distances to the points in the sequence,
or it is not Cauchy and one discards the new point by setting $d(a,a) = 1$.
(This means that, in the Bonk-Schramm recipe, we only use the points with $d(x,x) = 0$,
and show the triangular inequality there).

In the end, we obtain a space with a pseudodistance. The desired space is obtained
by quotienting out the space $\{x : d(x,x) = 0\}$ by the equivalence relation
given by $d(x,y) = 0$. The triangular inequality for the pseudo-distance shows
that it descends to a genuine distance on the quotient. This is the desired
geodesic complete extension of the original space.
›

subsection ‹Unfolded Bonk Schramm extension›

text ‹The unfolded Bonk Schramm extension, as explained at the beginning of this file, is a type made
of the initial type, adding all possible middles and all possible limits of Cauchy sequences,
without any quotienting process›

datatype 'a Bonk_Schramm_extension_unfolded =
basepoint 'a
| middle "'a Bonk_Schramm_extension_unfolded" "'a Bonk_Schramm_extension_unfolded"
| would_be_Cauchy "nat ⇒ 'a Bonk_Schramm_extension_unfolded"

context metric_space
begin

text ‹The construction of the distance will be done by transfinite induction,
with respect to a well-order for which the basepoints form an initial segment,
and for which middles of would-be Cauchy sequences are larger than the elements
they are made of. We will first prove the existence of such a well-order.

The idea is first to construct a function \verb+map_aux+ to another type, with a
well-order \verb+wo_aux+, such
that the image of \verb+middle a b+ is larger than the images of \verb+a+ and
\verb+b+ (take for instance the successor of the maximum of the two), and likewise
for a Cauchy sequence. A definition by induction works if the target cardinal is large
enough.

Then, pullback the well-order \verb+wo_aux+ by the map \verb+map_aux+: this gives a relation
that satisfies all the required properties, except that two different elements can be equal for
the order. Extending it essentially arbitrarily to distinguish between all elements (this is done
in Lemma \verb+Well_order_pullback+) gives the desired well-order›

definition Bonk_Schramm_extension_unfolded_wo where
"Bonk_Schramm_extension_unfolded_wo = (SOME (r::'a Bonk_Schramm_extension_unfolded rel).
well_order_on UNIV r
∧ (∀x ∈ range basepoint. ∀y ∈ - range basepoint. (x, y) ∈ r)
∧ (∀ a b. (a, middle a b) ∈ r)
∧ (∀ a b. (b, middle a b) ∈ r)
∧ (∀ u n. (u n, would_be_Cauchy u) ∈ r))"

text ‹We prove the existence of the well order›

definition wo_aux where
"wo_aux = (SOME (r:: (nat + 'a Bonk_Schramm_extension_unfolded set) rel).
Card_order r ∧ ¬finite(Field r) ∧ regularCard r ∧ |UNIV::'a Bonk_Schramm_extension_unfolded set| <o r)"

lemma wo_aux_exists:
"Card_order wo_aux ∧ ¬finite (Field wo_aux) ∧ regularCard wo_aux ∧ |UNIV::'a Bonk_Schramm_extension_unfolded set| <o wo_aux"
proof -
have *: "∀r ∈ {|UNIV::'a Bonk_Schramm_extension_unfolded set|}. Card_order r" by auto
have **: "∃(r::(nat + 'a Bonk_Schramm_extension_unfolded set) rel).
Card_order r ∧ ¬finite(Field r) ∧ regularCard r ∧ ( |UNIV::'a Bonk_Schramm_extension_unfolded set| <o r)"
by (metis card_of_card_order_on Field_card_of singletonI infinite_regularCard_exists[OF *])
then show ?thesis unfolding wo_aux_def using someI_ex[OF **] by auto
qed

interpretation wo_aux: wo_rel wo_aux
using wo_aux_exists Card_order_wo_rel by auto

primrec map_aux::"'a Bonk_Schramm_extension_unfolded ⇒ nat + 'a Bonk_Schramm_extension_unfolded set" where
"map_aux (basepoint x) = wo_aux.zero"
| "map_aux (middle a b) = wo_aux.suc ({map_aux a} ∪ {map_aux b})"
| "map_aux (would_be_Cauchy u) = wo_aux.suc ((map_aux o u)UNIV)"

lemma map_aux_AboveS_not_empty:
assumes "map_auxS ⊆ Field wo_aux"
shows "wo_aux.AboveS (map_auxS) ≠ {}"
apply (rule AboveS_not_empty_in_regularCard'[of S])
using wo_aux_exists assms apply auto
using card_of_UNIV ordLeq_ordLess_trans by blast

lemma map_aux_in_Field:
"map_aux x ∈ Field wo_aux"
proof (induction)
case (basepoint x)
have "wo_aux.zero ∈ Field wo_aux"
using Card_order_infinite_not_under wo_aux_exists under_empty wo_aux.zero_in_Field by fastforce
then show ?case by auto
next
case mid: (middle a b)
have "({map_aux a} ∪ {map_aux b}) ⊆ Field wo_aux" using mid.IH by auto
then have "wo_aux.AboveS ({map_aux a} ∪ {map_aux b}) ≠ {}"
using map_aux_AboveS_not_empty[of "{a} ∪ {b}"] by auto
then show ?case
next
case cauchy: (would_be_Cauchy u)
have "(map_aux o u)UNIV ⊆ Field wo_aux" using cauchy.IH by auto
then have "wo_aux.AboveS ((map_aux o u)UNIV) ≠ {}"
using map_aux_AboveS_not_empty[of "u(UNIV)"] by (simp add: image_image)
then show ?case
qed

lemma middle_rel_a:
"(map_aux a, map_aux (middle a b)) ∈ wo_aux - Id"
proof -
have *: "({map_aux a} ∪ {map_aux b}) ⊆ Field wo_aux" using map_aux_in_Field by auto
then have "wo_aux.AboveS ({map_aux a} ∪ {map_aux b}) ≠ {}"
using map_aux_AboveS_not_empty[of "{a} ∪ {b}"] by auto
then show ?thesis
using * by (simp add: wo_aux.suc_greater Id_def)
qed

lemma middle_rel_b:
"(map_aux b, map_aux (middle a b)) ∈ wo_aux - Id"
proof -
have *: "({map_aux a} ∪ {map_aux b}) ⊆ Field wo_aux" using map_aux_in_Field by auto
then have "wo_aux.AboveS ({map_aux a} ∪ {map_aux b}) ≠ {}"
using map_aux_AboveS_not_empty[of "{a} ∪ {b}"] by auto
then show ?thesis
using * by (simp add: wo_aux.suc_greater Id_def)
qed

lemma cauchy_rel:
"(map_aux (u n), map_aux (would_be_Cauchy u)) ∈ wo_aux - Id"
proof -
have *: "(map_aux o u)UNIV ⊆ Field wo_aux" using map_aux_in_Field by auto
then have "wo_aux.AboveS ((map_aux o u)UNIV) ≠ {}"
using map_aux_AboveS_not_empty[of "u(UNIV)"] by (simp add: image_image)
then show ?thesis
using * by (simp add: wo_aux.suc_greater Id_def)
qed

text ‹From the above properties of \verb+wo_aux+, it follows using \verb+Well_order_pullback+
that an order satisfying all the properties we want of \verb+Bonk_Schramm_extension_unfolded_wo+
exists. Hence, we get the following lemma.›

lemma Bonk_Schramm_extension_unfolded_wo_props:
"well_order_on UNIV Bonk_Schramm_extension_unfolded_wo"
"∀x ∈ range basepoint. ∀y ∈ - range basepoint. (x, y) ∈ Bonk_Schramm_extension_unfolded_wo"
"∀ a b. (a, middle a b) ∈ Bonk_Schramm_extension_unfolded_wo"
"∀ a b. (b, middle a b) ∈ Bonk_Schramm_extension_unfolded_wo"
"∀u n. (u n, would_be_Cauchy u) ∈ Bonk_Schramm_extension_unfolded_wo"
proof -
obtain r::"'a Bonk_Schramm_extension_unfolded rel" where r:
"Well_order r"
"Field r = UNIV"
"⋀x y. (map_aux x, map_aux y) ∈ wo_aux - Id ⟹ (x, y) ∈ r"
using Well_order_pullback[of wo_aux map_aux] by (metis wo_aux.WELL)

have "(x, y) ∈ r" if "x ∈ range basepoint" "y ∈ - range basepoint" for x y
apply (rule r(3)) using that
apply (cases y)
apply (auto cong del: image_cong_simp)
apply (metis insert_is_Un map_aux.simps(2) map_aux_in_Field wo_aux.zero_smallest)
apply (metis Diff_iff insert_is_Un wo_aux.leq_zero_imp map_aux.simps(2) middle_rel_a pair_in_Id_conv)
apply (metis map_aux.simps(3) map_aux_in_Field wo_aux.zero_smallest)
apply (metis Diff_iff cauchy_rel wo_aux.leq_zero_imp map_aux.simps(3) pair_in_Id_conv)
done
moreover have "(a, middle a b) ∈ r" for a b
apply (rule r(3)) using middle_rel_a by auto
moreover have "(b, middle a b) ∈ r" for a b
apply (rule r(3)) using middle_rel_b by auto
moreover have "(u n, would_be_Cauchy u) ∈ r" for u n
apply (rule r(3)) using cauchy_rel by auto
moreover have "well_order_on UNIV r"
using r(1) r(2) by auto
ultimately have *: "∃ (r::'a Bonk_Schramm_extension_unfolded rel).
well_order_on UNIV r
∧ (∀x ∈ range basepoint. ∀y ∈ - range basepoint. (x, y) ∈ r)
∧ (∀ a b. (a, middle a b) ∈ r)
∧ (∀ a b. (b, middle a b) ∈ r)
∧ (∀u n. (u n, would_be_Cauchy u) ∈ r)"
by blast

show
"well_order_on UNIV Bonk_Schramm_extension_unfolded_wo"
"∀x ∈ range basepoint. ∀y ∈ - range basepoint. (x, y) ∈ Bonk_Schramm_extension_unfolded_wo"
"∀ a b. (a, middle a b) ∈ Bonk_Schramm_extension_unfolded_wo"
"∀ a b. (b, middle a b) ∈ Bonk_Schramm_extension_unfolded_wo"
"∀u n. (u n, would_be_Cauchy u) ∈ Bonk_Schramm_extension_unfolded_wo"
unfolding Bonk_Schramm_extension_unfolded_wo_def using someI_ex[OF *] by auto
qed

interpretation wo: wo_rel Bonk_Schramm_extension_unfolded_wo
using well_order_on_Well_order wo_rel_def wfrec_def Bonk_Schramm_extension_unfolded_wo_props(1) by blast

text ‹We reformulate in the interpretation \verb+wo+ the main properties of
\verb+Bonk_Schramm_extension_unfolded_wo+ that we established in Lemma~\verb+Bonk_Schramm_extension_unfolded_wo_props+›

lemma Bonk_Schramm_extension_unfolded_wo_props':
"a ∈ wo.underS (middle a b)"
"b ∈ wo.underS (middle a b)"
"u n ∈ wo.underS (would_be_Cauchy u)"
proof -
have "(a, middle a b) ∈ Bonk_Schramm_extension_unfolded_wo"
using Bonk_Schramm_extension_unfolded_wo_props(3) by auto
then show "a ∈ wo.underS (middle a b)"
by (metis Diff_iff middle_rel_a pair_in_Id_conv underS_I)
have "(b, middle a b) ∈ Bonk_Schramm_extension_unfolded_wo"
using Bonk_Schramm_extension_unfolded_wo_props(4) by auto
then show "b ∈ wo.underS (middle a b)"
by (metis Diff_iff middle_rel_b pair_in_Id_conv underS_I)
have "(u n, would_be_Cauchy u) ∈ Bonk_Schramm_extension_unfolded_wo"
using Bonk_Schramm_extension_unfolded_wo_props(5) by auto
then show "u n ∈ wo.underS (would_be_Cauchy u)"
by (metis Diff_iff cauchy_rel pair_in_Id_conv underS_I)
qed

text ‹We want to define by transfinite induction a distance on \verb+'a Bonk_Schramm_extension_unfolded+,
adding one point at a time (i.e., if the distance is defined on $E$, then one wants to define it
on $E \cup \{x\}$, if $x$ is a middle or a potential Cauchy sequence, by prescribing the distance
from $x$ to all the points in $E$.

Technically, we define a family of distances, indexed by $x$, on $\{y : y \leq x\}^2$. As all
functions should be defined everywhere, this will be a family of functions on $X \times X$, indexed
by points in $X$. They will have a compatibility condition, making it possible to define a global
distance by gluing them together.

Technically, transfinite induction is implemented in Isabelle/HOL by an updating rule: a function
that associates, to a family of distances indexed by $x$, a new family of distances indexed by $x$.
The result of the transfinite induction is obtained by starting from an arbitrary object, and then
applying the updating rule infinitely many times. The characteristic property of the result of this
transfinite induction is that it is a fixed point of the updating rule, as it should.

Below, this is implemented as follows:
\begin{itemize}
\item \verb+extend_distance+ is the updating rule.
\item Its fixed point \verb+extend_distance_fp+ is by definition \verb+wo.worec extend_distance+
(it only makes sense if the udpating rule satisfies a compatibility condition
\verb+wo.adm_wo extend_distance+ saying that the update of a family, at $x$,
only depends on the value of the family
strictly below $x$.
\item Finally, the global distance \verb+extended_distance+ is taken as the
value of the fixed point above, on $x y y'$ (i.e., using the distance indexed by $x$) for any $x \geq \max(y, y')$. For definiteness, we use $\max(y, y')$, but it does not matter as everything is
compatible.
\end{itemize}›

fun extend_distance::"('a Bonk_Schramm_extension_unfolded ⇒ ('a Bonk_Schramm_extension_unfolded ⇒ 'a Bonk_Schramm_extension_unfolded ⇒ real))
⇒ ('a Bonk_Schramm_extension_unfolded ⇒ ('a Bonk_Schramm_extension_unfolded ⇒ 'a Bonk_Schramm_extension_unfolded ⇒ real))"
where
"extend_distance f (basepoint x) = (λy z. if y ∈ range basepoint ∧ z ∈ range basepoint then
dist (SOME y'. y = basepoint y') (SOME z'. z = basepoint z') else 1)"
| "extend_distance f (middle a b) = (λy z.
if (y ∈ wo.underS (middle a b)) ∧ (z ∈ wo.underS (middle a b)) then f (wo.max2 y z) y z
else if (y ∈ wo.underS (middle a b)) ∧ (z = middle a b) then (f (wo.max2 a b) a b)/2 + (SUP w∈{z ∈ wo.underS (middle a b). f z z z = 0}. f (wo.max2 y w) y w - max (f (wo.max2 a w) a w) (f (wo.max2 b w) b w))
else if (y = middle a b) ∧ (z ∈ wo.underS (middle a b)) then (f (wo.max2 a b) a b)/2 + (SUP w∈{z ∈ wo.underS (middle a b). f z z z = 0}. f (wo.max2 z w) z w - max (f (wo.max2 a w) a w) (f (wo.max2 b w) b w))
else if (y = middle a b) ∧ (z = middle a b) ∧ (f a a a = 0) ∧ (f b b b = 0) then 0
else 1)"
| "extend_distance f (would_be_Cauchy u) = (λy z.
if (y ∈ wo.underS (would_be_Cauchy u)) ∧ (z ∈ wo.underS (would_be_Cauchy u)) then f (wo.max2 y z) y z
else if (¬(∀eps > (0::real). ∃N. ∀n ≥ N. ∀m ≥ N. f (wo.max2 (u n) (u m)) (u n) (u m) < eps)) then 1
else if (y ∈ wo.underS (would_be_Cauchy u)) ∧ (z = would_be_Cauchy u) then lim (λn. f (wo.max2 (u n) y) (u n) y)
else if (y = would_be_Cauchy u) ∧ (z ∈ wo.underS (would_be_Cauchy u)) then lim (λn. f (wo.max2 (u n) z) (u n) z)
else if (y = would_be_Cauchy u) ∧ (z = would_be_Cauchy u) ∧ (∀n. f (u n) (u n) (u n) = 0) then 0
else 1)"

definition "extend_distance_fp = wo.worec extend_distance"

definition "extended_distance x y = extend_distance_fp (wo.max2 x y) x y"

definition "extended_distance_set = {z. extended_distance z z = 0}"

fix f g::"'a Bonk_Schramm_extension_unfolded ⇒ 'a Bonk_Schramm_extension_unfolded ⇒ 'a Bonk_Schramm_extension_unfolded ⇒ real"
fix x::"'a Bonk_Schramm_extension_unfolded"
assume "∀y∈wo.underS x. f y = g y"
then have *: "f y = g y" if "y ∈ wo.underS x" for y using that by auto
show "extend_distance f x = extend_distance g x"
apply (cases x)
(* We use the basic properties of our good order (middles and sequences come after their generators,
and the fact that initial segments are stable under max2 *)
apply (insert Bonk_Schramm_extension_unfolded_wo_props' *)
apply auto
(* Deal with the case of a middle, treating separately all the ifs *)
apply (rule ext)+
apply (rule if_cong, simp, simp)+ apply (rule SUP_cong, fastforce, blast)
apply (rule if_cong, simp, simp)+ apply (rule SUP_cong, fastforce, blast)
apply (rule if_cong, simp, simp)+ apply simp
(* Deal with the case of a sequence, treating separately all the ifs *)
apply (rule ext)+
apply (rule if_cong, simp, simp)+
apply simp
done
qed

lemma extend_distance_fp:
"extend_distance_fp = extend_distance (extend_distance_fp)"

lemma extended_distance_symmetric:
"extended_distance x y = extended_distance y x"
proof -
have *: "extend_distance (extend_distance_fp) x x y = extend_distance (extend_distance_fp) x y x" if "y ∈ wo.underS x" for x y
apply (cases x)
by blast
have **: "extended_distance x y = extended_distance y x" if "y ∈ wo.underS x" for x y
unfolding extended_distance_def using that *[OF that] extend_distance_fp by simp
consider "y ∈ wo.underS x"|"x ∈ wo.underS y"|"x = y"
by (metis UNIV_I Bonk_Schramm_extension_unfolded_wo_props(1) that(1) underS_I well_order_on_Well_order wo.TOTALS)
then show ?thesis
apply (cases) using ** by auto
qed

lemma extended_distance_basepoint:
"extended_distance (basepoint x) (basepoint y) = dist x y"
proof -
consider "wo.max2 (basepoint x) (basepoint y) = basepoint x" | "wo.max2 (basepoint x) (basepoint y) = basepoint y"
by (meson wo.max2_def)
then show ?thesis
apply cases
unfolding extended_distance_def by (subst extend_distance_fp, simp)+
qed

lemma extended_distance_set_basepoint:
"basepoint x ∈ extended_distance_set"
unfolding extended_distance_set_def using extended_distance_basepoint by auto

lemma extended_distance_set_middle:
assumes "a ∈ extended_distance_set" "b ∈ extended_distance_set"
shows "middle a b ∈ extended_distance_set"
using assms unfolding extended_distance_set_def extended_distance_def apply auto
by (metis (no_types, lifting) extend_distance_fp extend_distance.simps(2) underS_E)

lemma extended_distance_set_middle':
assumes "middle a b ∈ extended_distance_set"
shows "a ∈ extended_distance_set ∩ wo.underS (middle a b)"
"b ∈ extended_distance_set ∩ wo.underS (middle a b)"
proof -
have "extend_distance (extend_distance_fp) (middle a b) (middle a b) (middle a b) = 0"
apply (subst extend_distance_fp[symmetric])
using assms unfolding extended_distance_set_def extended_distance_def by simp
then have "a ∈ extended_distance_set" "b ∈ extended_distance_set"
unfolding extended_distance_set_def extended_distance_def apply auto
by (metis zero_neq_one)+
moreover have "a ∈ wo.underS (middle a b)" "b ∈ wo.underS (middle a b)"
ultimately show "a ∈ extended_distance_set ∩ wo.underS (middle a b)"
"b ∈ extended_distance_set ∩ wo.underS (middle a b)"
by auto
qed

lemma extended_distance_middle_formula:
assumes "x ∈ wo.underS (middle a b)"
shows "extended_distance x (middle a b) = (extended_distance a b)/2
+ (SUP w∈wo.underS (middle a b) ∩ extended_distance_set.
extended_distance x w - max (extended_distance a w) (extended_distance b w))"
unfolding extended_distance_set_def extended_distance_def
apply (subst extend_distance_fp)
apply (rule SUP_cong)
done

lemma extended_distance_set_Cauchy:
assumes "(would_be_Cauchy u) ∈ extended_distance_set"
shows "u n ∈ extended_distance_set ∩ wo.underS (would_be_Cauchy u)"
"∀eps > (0::real). ∃N. ∀n ≥ N. ∀m ≥ N. extended_distance (u n) (u m) < eps"
proof -
have *: "extend_distance (extend_distance_fp) (would_be_Cauchy u) (would_be_Cauchy u) (would_be_Cauchy u) = 0"
apply (subst extend_distance_fp[symmetric])
using assms unfolding extended_distance_set_def extended_distance_def by simp
then have "u n ∈ extended_distance_set"
unfolding extended_distance_set_def extended_distance_def apply auto
by (metis (no_types, opaque_lifting) underS_notIn zero_neq_one)
moreover have "u n ∈ wo.underS (would_be_Cauchy u)"
ultimately show "u n ∈ extended_distance_set ∩ wo.underS (would_be_Cauchy u)"
by auto
show "∀eps > (0::real). ∃N. ∀n ≥ N. ∀m ≥ N. extended_distance (u n) (u m) < eps"
using * unfolding extended_distance_set_def extended_distance_def apply auto
by (metis (no_types, opaque_lifting) zero_neq_one)
qed

lemma extended_distance_triang_ineq:
assumes "x ∈ extended_distance_set"
"y ∈ extended_distance_set"
"z ∈ extended_distance_set"
shows "extended_distance x z ≤ extended_distance x y + extended_distance y z"
proof -
(* The proof of the triangular inequality is done by induction: one should show that adding
a middle or a Cauchy sequence does not spoil the estimates. Technically, we show that the
triangular inequality holds on all points under $t$, for all $t$, using a transfinite induction.
The conclusion of the lemma then follows by using for $t$ the maximum of $x$, $y$, $z$.*)
have ineq_rec: "∀x y z. x ∈ wo.under t ∩ extended_distance_set ⟶ y ∈ wo.under t ∩ extended_distance_set ⟶ z ∈ wo.under t ∩ extended_distance_set
⟶ extended_distance x z ≤ extended_distance x y + extended_distance y z" for t
proof (rule wo.well_order_induct[of _ t])
fix t
assume IH_orig: "∀t2. t2 ≠ t ∧ (t2, t) ∈ Bonk_Schramm_extension_unfolded_wo ⟶
(∀x y z. x ∈ wo.under t2 ∩ extended_distance_set ⟶
y ∈ wo.under t2 ∩ extended_distance_set ⟶
z ∈ wo.under t2 ∩ extended_distance_set ⟶
extended_distance x z ≤ extended_distance x y + extended_distance y z)"
(*Reformulate the induction assumption in more convenient terms*)
then have IH: "extended_distance x z ≤ extended_distance x y + extended_distance y z"
if "x ∈ wo.underS t ∩ extended_distance_set"
"y ∈ wo.underS t ∩ extended_distance_set"
"z ∈ wo.underS t ∩ extended_distance_set"
for x y z
proof -
define t2 where "t2 = wo.max2 (wo.max2 x y) z"
have "t2 ∈ wo.underS t" using that t2_def by auto
have "x ∈ wo.under t2" "y ∈ wo.under t2" "z ∈ wo.under t2" unfolding t2_def
by (metis UNIV_I Bonk_Schramm_extension_unfolded_wo_props(1) mem_Collect_eq under_def well_order_on_Well_order wo.TOTALS wo.max2_iff)+
then show ?thesis using that IH_orig ‹t2 ∈ wo.underS t› underS_E by fastforce
qed

have pos: "extended_distance x y ≥ 0" if "x ∈ wo.underS t ∩ extended_distance_set" "y ∈ wo.underS t ∩ extended_distance_set" for x y
proof -
have "0 = extended_distance x x" using that(1) extended_distance_set_def by auto
also have "... ≤ extended_distance x y + extended_distance y x"
using IH that by auto
also have "... = 2 * extended_distance x y"
using extended_distance_symmetric by auto
finally show ?thesis by auto
qed

(* The conclusion is easy if $t$ is not in \verb+extended_distance_set+, as there is no
additional point to consider for the triangular inequality. The interesting case is when
$t$ is admissible, then we will argue differently depending on its type.*)
consider "t ∉ extended_distance_set" | "t ∈ extended_distance_set" by auto
then show "∀x y z. x ∈ wo.under t ∩ extended_distance_set ⟶
y ∈ wo.under t ∩ extended_distance_set ⟶
z ∈ wo.under t ∩ extended_distance_set ⟶
extended_distance x z ≤ extended_distance x y + extended_distance y z"
proof (cases)
case 1
then have "wo.under t ∩ extended_distance_set = wo.underS t ∩ extended_distance_set"
apply auto
apply (metis mem_Collect_eq underS_I under_def)
then show ?thesis using IH by auto
next
case 2
(*We assume now that $t$ is admissible.
We will prove now the triangular inequality for points under t, in the two basic cases
where t is either the first point in the inequality, or the middle point.
All other cases can be reduced to this one by permuting the variables, or they are
trivial (if several variables are equal to t, for instance).*)
have main_ineq: "extended_distance x z ≤ extended_distance x t + extended_distance t z
∧ extended_distance x t ≤ extended_distance x z + extended_distance z t"
if "x ∈ wo.underS t ∩ extended_distance_set"
"z ∈ wo.underS t ∩ extended_distance_set"
for x z
proof (cases t)
(*In the case of a basepoint, the distance comes from the original distance, hence
it satisfies the triangular inequality*)
case A: (basepoint t')
then have "x ∈ range basepoint" using Bonk_Schramm_extension_unfolded_wo_props(2)
by (metis that(1) Compl_iff Int_iff range_eqI wo.max2_def wo.max2_underS'(2))
then obtain x' where x: "x = basepoint x'" by auto
have "z ∈ range basepoint" using Bonk_Schramm_extension_unfolded_wo_props(2) A
by (metis that(2) Compl_iff Int_iff range_eqI wo.max2_def wo.max2_underS'(2))
then obtain z' where z: "z = basepoint z'" by auto
show "extended_distance x z ≤ extended_distance x t + extended_distance t z
∧ extended_distance x t ≤ extended_distance x z + extended_distance z t"
unfolding x z A extended_distance_basepoint by (simp add: dist_triangle)
next
(*In the case of a middle, the triangular inequality follows from the specific formula
devised by Bonk and Schramm and (not very complicated) computations. The only mild difficulty
is that the formula is defined in terms of a supremum, so one should check that this
supremum is taken over a bounded set. This boundedness comes from the triangular inequality
for point strictly below $t$, i.e., our inductive assumption.*)
case M: (middle a b)
then have ab: "a ∈ extended_distance_set ∩ wo.underS (middle a b)"
"b ∈ extended_distance_set ∩ wo.underS (middle a b)"
using 2 extended_distance_set_middle'[of a b] by auto
have dxt: "extended_distance x t = (extended_distance a b)/2
+ (SUP w∈wo.underS (middle a b) ∩ extended_distance_set.
extended_distance x w - max (extended_distance a w) (extended_distance b w))"
using that(1) unfolding M using extended_distance_middle_formula by auto
have dzt: "extended_distance z t = (extended_distance a b)/2
+ (SUP w∈wo.underS (middle a b) ∩ extended_distance_set.
extended_distance z w - max (extended_distance a w) (extended_distance b w))"
using that(2) unfolding M using extended_distance_middle_formula by auto

have bdd: "bdd_above ((λw. extended_distance x w - max (extended_distance a w) (extended_distance b w)) (wo.underS (middle a b) ∩ extended_distance_set))"
if "x ∈ wo.underS t ∩ extended_distance_set" for x
proof (rule bdd_aboveI2)
fix w assume w: "w ∈ wo.underS (middle a b) ∩ extended_distance_set"
have "extended_distance x w ≤ extended_distance x a + extended_distance a w"
apply (rule IH) using ab w M that(1) by auto
also have "... ≤ extended_distance x a + max (extended_distance a w) (extended_distance b w)"
by auto
finally show "extended_distance x w - max (extended_distance a w) (extended_distance b w)
≤ extended_distance x a"
by auto
qed

have "(λw. extended_distance x z + extended_distance z w - max (extended_distance a w) (extended_distance b w))  (underS Bonk_Schramm_extension_unfolded_wo (middle a b) ∩ extended_distance_set)
= (λs. s + extended_distance x z) (λw. extended_distance z w - max (extended_distance a w) (extended_distance b w))  (underS Bonk_Schramm_extension_unfolded_wo (middle a b) ∩ extended_distance_set)"
by auto
moreover have "bdd_above ((λs. s + extended_distance x z) (λw. extended_distance z w - max (extended_distance a w) (extended_distance b w))  (underS Bonk_Schramm_extension_unfolded_wo (middle a b) ∩ extended_distance_set))"
apply (rule bdd_above_image_mono) using bdd that by (auto simp add: mono_def)
ultimately have bdd_3: "bdd_above ((λw. extended_distance x z + extended_distance z w - max (extended_distance a w) (extended_distance b w))  (underS Bonk_Schramm_extension_unfolded_wo (middle a b) ∩ extended_distance_set))"
by simp

have **: "max (extended_distance a a) (extended_distance b a) = extended_distance b a"
apply (rule max_absorb2) using pos ab extended_distance_set_def M by auto
then have "-extended_distance a b / 2 + extended_distance x a
= (extended_distance a b)/2 + extended_distance x a - max (extended_distance a a) (extended_distance b a)"
unfolding extended_distance_symmetric[of a b] by auto
also have "... ≤ extended_distance x t"
unfolding dxt apply (simp, rule cSUP_upper, simp) using bdd that M ab by auto
finally have D1: "-extended_distance a b / 2 + extended_distance x a ≤ extended_distance x t"
by simp

have **: "max (extended_distance a b) (extended_distance b b) = extended_distance a b"
apply (rule max_absorb1) using pos ab extended_distance_set_def M by auto
then have "-extended_distance a b / 2 + extended_distance x b
= (extended_distance a b)/2 + extended_distance x b - max (extended_distance a b) (extended_distance b b)"
unfolding extended_distance_symmetric[of a b] by auto
also have "... ≤ extended_distance x t"
unfolding dxt apply (simp, rule cSUP_upper, simp) using bdd that ab by auto
finally have "-extended_distance a b / 2 + extended_distance x b ≤ extended_distance x t"
by simp
then have D2: "-extended_distance a b / 2 + max (extended_distance x a) (extended_distance x b) ≤ extended_distance x t"
using D1 by auto

have "extended_distance x z = (-extended_distance a b / 2 + max (extended_distance x a) (extended_distance x b)) +
(extended_distance a b / 2 + extended_distance x z - max (extended_distance x a) (extended_distance x b))"
by auto
also have "... ≤ extended_distance x t +
(extended_distance a b / 2 + extended_distance z x - max (extended_distance a x) (extended_distance b x))"
using D2 extended_distance_symmetric by auto
also have "... ≤ extended_distance x t + extended_distance z t"
unfolding dzt apply (simp, rule cSUP_upper) using bdd that M ab by auto
finally have I: "extended_distance x z ≤ extended_distance x t + extended_distance z t"
using extended_distance_symmetric by auto

have T: "underS Bonk_Schramm_extension_unfolded_wo (middle a b) ∩ extended_distance_set ≠ {}"
"mono ((+) (extended_distance x z))"
"bij ((+) (extended_distance x z))"
using ab(1) apply blast
by (simp add: monoI, rule bij_betw_byWitness[of _ "λs. s - (extended_distance x z)"], auto)
have "extended_distance x t ≤ (extended_distance a b)/2
+ (SUP w∈wo.underS (middle a b) ∩ extended_distance_set.
extended_distance x z + extended_distance z w - max (extended_distance a w) (extended_distance b w))"
unfolding dxt apply (simp, rule cSUP_subset_mono)
using M that IH bdd_3 by (auto)
also have "... = extended_distance x z + extended_distance z t"
unfolding dzt apply simp
using mono_cSup_bij[of "(λw. extended_distance z w - max (extended_distance a w) (extended_distance b w))(wo.underS (middle a b) ∩ extended_distance_set)" "λs. extended_distance x z + s", OF _ _ T(2) T(3)]
finally have "extended_distance x t ≤ extended_distance x z + extended_distance z t" by simp
then show "extended_distance x z ≤ extended_distance x t + extended_distance t z
∧ extended_distance x t ≤ extended_distance x z + extended_distance z t"
using I extended_distance_symmetric by auto
next
(*For Cauchy sequences, the distance to the Cauchy sequence is the limit of the distances
to terms of the sequence, hence the triangular inequality follows from the triangular inequality
for points strictly below $t$ by passing to the limit.*)
case C: (would_be_Cauchy u)
then have un: "u n ∈ extended_distance_set ∩ wo.underS (would_be_Cauchy u)" for n
using extended_distance_set_Cauchy 2 by auto
have lim: "(λn. extended_distance y (u n)) ⇢ (extended_distance y (would_be_Cauchy u))"
if y: "y ∈ extended_distance_set ∩ wo.underS (would_be_Cauchy u)" for y
proof -
have "extend_distance extend_distance_fp (wo.max2 (would_be_Cauchy u) (would_be_Cauchy u)) (would_be_Cauchy u) (would_be_Cauchy u) = 0"
using 2 unfolding C extended_distance_set_def extended_distance_def
using extend_distance_fp by auto
then have cauch: "∃N. ∀n ≥ N. ∀m ≥ N. extend_distance_fp (wo.max2 (u n) (u m)) (u n) (u m) < e" if "e > 0" for e
apply auto using ‹e > 0› by (metis (no_types, opaque_lifting) zero_neq_one)
have "∃N. ∀n ≥ N. ∀m ≥ N. abs(extended_distance y (u n) - extended_distance y (u m)) < e" if "e > 0" for e
proof -
obtain N where *: "extend_distance_fp (wo.max2 (u n) (u m)) (u n) (u m) < e" if "n ≥ N" "m ≥ N" for m n
using cauch by (meson ‹0 < e›)
{
fix m n assume "m ≥ N" "n ≥ N"
then have e: "extended_distance (u n) (u m) < e" using * unfolding extended_distance_def by auto
have "extended_distance y (u n) ≤ extended_distance y (u m) + extended_distance (u m) (u n)"
using IH y un C by blast
then have 1: "extended_distance y (u n) - extended_distance y (u m) < e"
using e extended_distance_symmetric by auto
have "extended_distance y (u m) ≤ extended_distance y (u n) + extended_distance (u n) (u m)"
using IH y un C by blast
then have "extended_distance y (u m) - extended_distance y (u n) < e"
using e extended_distance_symmetric by auto
then have "abs(extended_distance y (u n) - extended_distance y (u m)) < e"
using 1 by auto
}
then show ?thesis by auto
qed
then have "convergent (λn. extended_distance y (u n))"
then have lim: "(λn. extended_distance y (u n)) ⇢ lim (λn. extended_distance y (u n))"
using convergent_LIMSEQ_iff by auto
have *: "wo.max2 y (would_be_Cauchy u) = would_be_Cauchy u" "y ≠ would_be_Cauchy u" using y by auto
have "extended_distance y (would_be_Cauchy u) = lim (λn. extended_distance (u n) y)"
unfolding extended_distance_def apply (subst extend_distance_fp) unfolding *
using *(2) y cauch by auto
then show "(λn. extended_distance y (u n)) ⇢ extended_distance y (would_be_Cauchy u)"
using lim extended_distance_symmetric by auto
qed
have "extended_distance x z ≤ extended_distance x (u n) + extended_distance (u n) z" for n
using IH un that C by auto
moreover have "(λn. extended_distance x (u n) + extended_distance (u n) z) ⇢ extended_distance x t + extended_distance t z"
using lim that extended_distance_symmetric unfolding C by auto
ultimately have I: "extended_distance x z ≤ extended_distance x t + extended_distance t z"
using LIMSEQ_le_const by blast

have "extended_distance x (u n) ≤ extended_distance x z + extended_distance z (u n)" for n
using IH un that C by auto
moreover have "(λn. extended_distance x (u n)) ⇢ extended_distance x t"
using lim that extended_distance_symmetric unfolding C by auto
moreover have "(λn. extended_distance x z + extended_distance z (u n)) ⇢ extended_distance x z + extended_distance z t"
using lim that extended_distance_symmetric unfolding C by auto
ultimately have "extended_distance x t ≤ extended_distance x z + extended_distance z t"
using LIMSEQ_le by blast
then show "extended_distance x z ≤ extended_distance x t + extended_distance t z
∧ extended_distance x t ≤ extended_distance x z + extended_distance z t"
using I by auto
qed

(* Now, we deduce (from the above bounds in specific cases) the general triangular inequality,
by considering separately if each point is equal to $t$ or strictly under it.*)
{
fix x y z assume H: "x ∈ wo.under t ∩ extended_distance_set"
"y ∈ wo.under t ∩ extended_distance_set"
"z ∈ wo.under t ∩ extended_distance_set"
have t: "extended_distance t t = 0" "extended_distance t t ≥ 0" using 2 extended_distance_set_def by auto
have *: "((x ∈ wo.underS t ∩ extended_distance_set) ∨ (x = t))
∧ ((y ∈ wo.underS t ∩ extended_distance_set) ∨ (y = t))
∧ ((z ∈ wo.underS t ∩ extended_distance_set) ∨ (z = t))"
using H by (simp add: underS_def under_def)
have "extended_distance x z ≤ extended_distance x y + extended_distance y z"
using * apply auto
using t main_ineq extended_distance_symmetric IH pos apply blast
using t main_ineq extended_distance_symmetric IH pos apply blast
using t main_ineq extended_distance_symmetric IH pos apply blast
using t main_ineq extended_distance_symmetric IH pos apply blast
using t main_ineq extended_distance_symmetric IH pos apply (metis * Int_commute add.commute underS_notIn)
using t main_ineq extended_distance_symmetric IH pos apply (metis (mono_tags, lifting) "*" extended_distance_set_def mem_Collect_eq underS_notIn)
using t by auto
}
then show ?thesis by auto
qed
qed (*End of the inductive proof*)

define t where "t = wo.max2 (wo.max2 x y) z"
have "x ∈ wo.under t" "y ∈ wo.under t" "z ∈ wo.under t"
unfolding t_def
by (metis UNIV_I Bonk_Schramm_extension_unfolded_wo_props(1) mem_Collect_eq under_def well_order_on_Well_order wo.max2_equals1 wo.max2_iff wo.max2_xx)+
then show ?thesis using assms ineq_rec by auto
qed

text ‹We can now show the two main properties of the construction: the middle is indeed a middle
from the metric point of view (in \verb+extended_distance_middle+), and Cauchy sequences have
a limit (the corresponding \verb+would_be_Cauchy+ point).›

lemma extended_distance_pos:
assumes "a ∈ extended_distance_set"
"b ∈ extended_distance_set"
shows "extended_distance a b ≥ 0"
using assms extended_distance_set_def extended_distance_triang_ineq[of a b a]
unfolding extended_distance_symmetric[of b a] by auto

lemma extended_distance_middle:
assumes "a ∈ extended_distance_set"
"b ∈ extended_distance_set"
shows "extended_distance a (middle a b) = extended_distance a b / 2"
"extended_distance b (middle a b) = extended_distance a b / 2"
proof -
have "0 = extended_distance a b - max (extended_distance a b) (extended_distance b b)"
using extended_distance_pos[OF assms] assms(2) extended_distance_set_def by auto
also have "... ≤ (SUP w∈wo.underS (middle a b) ∩ extended_distance_set.
extended_distance a w - max (extended_distance a w) (extended_distance b w))"
apply (rule cSUP_upper)
by (rule bdd_aboveI2[of _ _ 0], auto)
ultimately have "0 ≤ (SUP w∈wo.underS (middle a b) ∩ extended_distance_set.
extended_distance a w - max (extended_distance a w) (extended_distance b w))"
by auto
moreover have "(SUP w∈wo.underS (middle a b) ∩ extended_distance_set.
extended_distance a w - max (extended_distance a w) (extended_distance b w)) ≤ 0"
apply (rule cSUP_least)
using assms(1) Bonk_Schramm_extension_unfolded_wo_props'(1) by (fastforce, auto)
moreover have "extended_distance a (middle a b) = (extended_distance a b)/2
+ (SUP w∈wo.underS (middle a b) ∩ extended_distance_set.
extended_distance a w - max (extended_distance a w) (extended_distance b w))"
by (rule extended_distance_middle_formula, simp add: Bonk_Schramm_extension_unfolded_wo_props'(1))
ultimately show "extended_distance a (middle a b) = (extended_distance a b)/2"
by auto

have "0 = extended_distance b a - max (extended_distance a a) (extended_distance b a)"
using extended_distance_pos[OF assms] assms(1) extended_distance_set_def extended_distance_symmetric by auto
also have "... ≤ (SUP w∈wo.underS (middle a b) ∩ extended_distance_set.
extended_distance b w - max (extended_distance a w) (extended_distance b w))"
apply (rule cSUP_upper)
by (rule bdd_aboveI2[of _ _ 0], auto)
ultimately have "0 ≤ (SUP w∈wo.underS (middle a b) ∩ extended_distance_set.
extended_distance b w - max (extended_distance a w) (extended_distance b w))"
by auto
moreover have "(SUP w∈wo.underS (middle a b) ∩ extended_distance_set.
extended_distance b w - max (extended_distance a w) (extended_distance b w)) ≤ 0"
apply (rule cSUP_least)
using assms(1) Bonk_Schramm_extension_unfolded_wo_props'(1) by (fastforce, auto)
moreover have "extended_distance b (middle a b) = (extended_distance a b)/2
+ (SUP w∈wo.underS (middle a b) ∩ extended_distance_set.
extended_distance b w - max (extended_distance a w) (extended_distance b w))"
by (rule extended_distance_middle_formula, simp add: Bonk_Schramm_extension_unfolded_wo_props'(2))
ultimately show "extended_distance b (middle a b) = (extended_distance a b)/2"
by auto
qed

lemma extended_distance_Cauchy:
assumes "⋀(n::nat). u n ∈ extended_distance_set"
and "∀eps > (0::real). ∃N. ∀n ≥ N. ∀m ≥ N. extended_distance (u n) (u m) < eps"
shows "would_be_Cauchy u ∈ extended_distance_set"
"(λn. extended_distance (u n) (would_be_Cauchy u)) ⇢ 0"
proof -
show 2: "would_be_Cauchy u ∈ extended_distance_set"
unfolding extended_distance_set_def extended_distance_def apply (simp, subst extend_distance_fp)
using assms unfolding extended_distance_set_def extended_distance_def by simp

have lim: "(λn. extended_distance y (u n)) ⇢ (extended_distance y (would_be_Cauchy u))"
if y: "y ∈ extended_distance_set ∩ wo.underS (would_be_Cauchy u)" for y
proof -
have "∃N. ∀n ≥ N. ∀m ≥ N. abs(extended_distance y (u n) - extended_distance y (u m)) < e" if "e > 0" for e
proof -
obtain N where *: "extended_distance (u n) (u m) < e" if "n ≥ N" "m ≥ N" for m n
using assms(2) that ‹e > 0› by meson
{
fix m n assume "m ≥ N" "n ≥ N"
then have e: "extended_distance (u n) (u m) < e" using * by auto
have "extended_distance y (u n) ≤ extended_distance y (u m) + extended_distance (u m) (u n)"
using extended_distance_triang_ineq y assms(1) by blast
then have 1: "extended_distance y (u n) - extended_distance y (u m) < e"
using e extended_distance_symmetric by auto
have "extended_distance y (u m) ≤ extended_distance y (u n) + extended_distance (u n) (u m)"
using extended_distance_triang_ineq y assms(1) by blast
then have "extended_distance y (u m) - extended_distance y (u n) < e"
using e extended_distance_symmetric by auto
then have "abs(extended_distance y (u n) - extended_distance y (u m)) < e"
using 1 by auto
}
then show ?thesis by auto
qed
then have "convergent (λn. extended_distance y (u n))"
then have lim: "(λn. extended_distance y (u n)) ⇢ lim (λn. extended_distance y (u n))"
using convergent_LIMSEQ_iff by auto
have *: "wo.max2 y (would_be_Cauchy u) = would_be_Cauchy u" "y ≠ would_be_Cauchy u" using y by auto
have "extended_distance y (would_be_Cauchy u) = lim (λn. extended_distance (u n) y)"
unfolding extended_distance_def apply (subst extend_distance_fp) unfolding *
using *(2) y assms(2) extended_distance_def by auto
then show "(λn. extended_distance y (u n)) ⇢ extended_distance y (would_be_Cauchy u)"
using lim extended_distance_symmetric by auto
qed

have "∃N. ∀n ≥ N. abs(extended_distance (u n) (would_be_Cauchy u)) < e" if "e > 0" for e
proof -
obtain N where *: "extended_distance (u n) (u m) < e/2" if "n ≥ N" "m ≥ N" for m n
using assms(2) that ‹e > 0› by (meson half_gt_zero)
have "abs(extended_distance (u n) (would_be_Cauchy u)) ≤ e/2" if "n ≥ N" for n
proof -
have "eventually (λm. extended_distance (u n) (u m) ≤ e/2) sequentially"
apply (rule eventually_sequentiallyI[of N]) using *[OF ‹n ≥ N›] less_imp_le by auto
moreover have "(λm. extended_distance (u n) (u m)) ⇢ extended_distance (u n) (would_be_Cauchy u)"
apply (rule lim) using "2" extended_distance_set_Cauchy by auto
ultimately have "extended_distance (u n) (would_be_Cauchy u) ≤ e/2"
by (meson "*" LIMSEQ_le_const2 less_imp_le that)
then show ?thesis using extended_distance_pos[OF assms(1)[of n] 2] by auto
qed
then show ?thesis using ‹e > 0› by force
qed
then show "(λn. extended_distance (u n) (would_be_Cauchy u)) ⇢ 0"
using LIMSEQ_iff by force
qed

end (* of context \verb+metric_space+ *)

subsection ‹The Bonk Schramm extension›

"('a::metric_space) Bonk_Schramm_extension_unfolded"
/ partial: "λx y. (x ∈ extended_distance_set ∧ y ∈ extended_distance_set ∧ extended_distance x y = 0)"
unfolding part_equivp_def proof(auto intro!: ext simp: extended_distance_set_def)
show "∃x. extended_distance x x = 0"
using extended_distance_set_basepoint extended_distance_set_def by auto
next
fix x y z::"'a Bonk_Schramm_extension_unfolded"
assume H: "extended_distance x x = 0" "extended_distance y y = 0" "extended_distance z z = 0"
"extended_distance x y = 0" "extended_distance x z = 0"
have "extended_distance y z ≤ extended_distance y x + extended_distance x z"
apply (rule extended_distance_triang_ineq)
using H unfolding extended_distance_set_def by auto
also have "... ≤ 0"
by (auto simp add: extended_distance_symmetric H)
finally show "extended_distance y z = 0"
using extended_distance_pos[of y z] H unfolding extended_distance_set_def by auto
next
fix x y z::"'a Bonk_Schramm_extension_unfolded"
assume H: "extended_distance x x = 0" "extended_distance y y = 0" "extended_distance z z = 0"
"extended_distance x y = 0" "extended_distance y z = 0"
have "extended_distance x z ≤ extended_distance x y + extended_distance y z"
apply (rule extended_distance_triang_ineq)
using H unfolding extended_distance_set_def by auto
also have "... ≤ 0"
by (auto simp add: extended_distance_symmetric H)
finally show "extended_distance x z = 0"
using extended_distance_pos[of x z] H unfolding extended_distance_set_def by auto
qed (metis)

instantiation Bonk_Schramm_extension :: (metric_space) metric_space
begin

lift_definition dist_Bonk_Schramm_extension::"('a::metric_space) Bonk_Schramm_extension ⇒ 'a Bonk_Schramm_extension ⇒ real"
is "λx y. extended_distance x y"
proof -
fix x y z t::"'a Bonk_Schramm_extension_unfolded"
assume H: "x ∈ extended_distance_set ∧ y ∈ extended_distance_set ∧ extended_distance x y = 0"
"z ∈ extended_distance_set ∧ t ∈ extended_distance_set ∧ extended_distance z t = 0"
have "extended_distance x z ≤ extended_distance x y + extended_distance y t + extended_distance t z"
using extended_distance_triang_ineq[of x y z] extended_distance_triang_ineq[of y t z] H
by auto
also have "... = extended_distance y t"
using H by (auto simp add: extended_distance_symmetric)
finally have *: "extended_distance x z ≤ extended_distance y t" by simp
have "extended_distance y t ≤ extended_distance y x + extended_distance x z + extended_distance z t"
using extended_distance_triang_ineq[of y x t] extended_distance_triang_ineq[of x z t] H
by auto
also have "... = extended_distance x z"
using H by (auto simp add: extended_distance_symmetric)
finally show "extended_distance x z = extended_distance y t" using * by simp
qed

text ‹To define a metric space in the current library of Isabelle/HOL, one should also introduce
a uniformity structure and a topology, as follows (they are prescribed by the distance):›

definition uniformity_Bonk_Schramm_extension::"(('a Bonk_Schramm_extension) × ('a Bonk_Schramm_extension)) filter"
where "uniformity_Bonk_Schramm_extension = (INF e∈{0 <..}. principal {(x, y). dist x y < e})"

definition open_Bonk_Schramm_extension :: "'a Bonk_Schramm_extension set ⇒ bool"
where "open_Bonk_Schramm_extension U = (∀x∈U. eventually (λ(x', y). x' = x ⟶ y ∈ U) uniformity)"

instance proof
fix x y::"'a Bonk_Schramm_extension"
have C: "rep_Bonk_Schramm_extension x ∈ extended_distance_set"
"rep_Bonk_Schramm_extension y ∈ extended_distance_set"
using Quotient3_Bonk_Schramm_extension Quotient3_rep_reflp by fastforce+
show "(dist x y = 0) = (x = y)"
apply (subst Quotient3_rel_rep[OF Quotient3_Bonk_Schramm_extension, symmetric])
unfolding dist_Bonk_Schramm_extension_def using C by auto
next
fix x y z::"'a Bonk_Schramm_extension"
have C: "rep_Bonk_Schramm_extension x ∈ extended_distance_set"
"rep_Bonk_Schramm_extension y ∈ extended_distance_set"
"rep_Bonk_Schramm_extension z ∈ extended_distance_set"
using Quotient3_Bonk_Schramm_extension Quotient3_rep_reflp by fastforce+
show "dist x y ≤ dist x z + dist y z"
unfolding dist_Bonk_Schramm_extension_def apply auto
by (metis C extended_distance_symmetric extended_distance_triang_ineq)
qed (auto simp add: uniformity_Bonk_Schramm_extension_def open_Bonk_Schramm_extension_def)
end

instance Bonk_Schramm_extension :: (metric_space) complete_space
proof
fix X::"nat ⇒ 'a Bonk_Schramm_extension" assume "Cauchy X"
have *: "⋀n. rep_Bonk_Schramm_extension (X n) ∈ extended_distance_set"
using Quotient3_Bonk_Schramm_extension Quotient3_rep_reflp by fastforce
have **: "extended_distance (rep_Bonk_Schramm_extension (X n)) (rep_Bonk_Schramm_extension (X m)) = dist (X n) (X m)" for m n
unfolding dist_Bonk_Schramm_extension_def by auto
define y where "y = would_be_Cauchy (λn. rep_Bonk_Schramm_extension (X n))"
have "y ∈ extended_distance_set"
unfolding y_def apply (rule extended_distance_Cauchy)
using * ‹Cauchy X› unfolding Cauchy_def **[symmetric] by auto
define x where "x = abs_Bonk_Schramm_extension y"
have "dist (X n) x = extended_distance (rep_Bonk_Schramm_extension (X n)) y" for n
unfolding x_def apply (subst Quotient3_abs_rep[OF Quotient3_Bonk_Schramm_extension, symmetric])
apply (rule dist_Bonk_Schramm_extension.abs_eq) using * ‹y ∈ extended_distance_set›
moreover have "(λn. extended_distance (rep_Bonk_Schramm_extension (X n)) y) ⇢ 0"
unfolding y_def apply (rule extended_distance_Cauchy)
using * ‹Cauchy X› unfolding Cauchy_def **[symmetric] by auto
ultimately have *: "(λn. dist (X n) x) ⇢ 0" by simp
have "X ⇢ x"
apply (rule tendstoI) using * by (auto simp add: order_tendsto_iff)
then show "convergent X" unfolding convergent_def by auto
qed

instance Bonk_Schramm_extension :: (metric_space) geodesic_space
proof (rule complete_with_middles_imp_geodesic)
fix x y::"'a Bonk_Schramm_extension"
have H: "rep_Bonk_Schramm_extension x ∈ extended_distance_set"
"rep_Bonk_Schramm_extension y ∈ extended_distance_set"
using Quotient3_Bonk_Schramm_extension Quotient3_rep_reflp by fastforce+
define M where "M = middle (rep_Bonk_Schramm_extension x) (rep_Bonk_Schramm_extension y)"
then have M: "M ∈ extended_distance_set"
using extended_distance_set_middle[OF H] by simp
define m where "m = abs_Bonk_Schramm_extension M"

have "dist x m = extended_distance (rep_Bonk_Schramm_extension x) M"
apply (subst Quotient3_abs_rep[OF Quotient3_Bonk_Schramm_extension, symmetric]) unfolding m_def
apply (rule dist_Bonk_Schramm_extension.abs_eq)
using H M extended_distance_set_def by auto
also have "... = extended_distance (rep_Bonk_Schramm_extension x) (rep_Bonk_Schramm_extension y) / 2"
unfolding M_def by (rule extended_distance_middle[OF H])
also have "... = dist x y / 2"
unfolding dist_Bonk_Schramm_extension_def by auto
finally have *: "dist x m = dist x y / 2" by simp

have "dist m y = extended_distance M (rep_Bonk_Schramm_extension y)"
apply (subst Quotient3_abs_rep[OF Quotient3_Bonk_Schramm_extension, of y, symmetric]) unfolding m_def
apply (rule dist_Bonk_Schramm_extension.abs_eq)
using H M extended_distance_set_def by auto
also have "... = extended_distance (rep_Bonk_Schramm_extension x) (rep_Bonk_Schramm_extension y) / 2"
unfolding M_def using extended_distance_middle(2)[OF H] by (simp add: extended_distance_symmetric)
also have "... = dist x y / 2"
unfolding dist_Bonk_Schramm_extension_def by auto
finally have "dist m y = dist x y / 2" by simp
then show "∃m. dist x m = dist x y / 2 ∧ dist m y = dist x y / 2"
using * by auto
qed

definition to_Bonk_Schramm_extension::"'a::metric_space ⇒ 'a Bonk_Schramm_extension"
where "to_Bonk_Schramm_extension x = abs_Bonk_Schramm_extension (basepoint x)"

lemma to_Bonk_Schramm_extension_isometry:
"isometry_on UNIV to_Bonk_Schramm_extension"
proof (rule isometry_onI)
fix x y::'a
show "dist (to_Bonk_Schramm_extension x) (to_Bonk_Schramm_extension y) = dist x y"
unfolding to_Bonk_Schramm_extension_def apply (subst dist_Bonk_Schramm_extension.abs_eq)
unfolding extended_distance_set_def by (auto simp add: extended_distance_basepoint)
qed

section ‹Bonk-Schramm extension of hyperbolic spaces›

subsection ‹The Bonk-Schramm extension preserves hyperbolicity›

text ‹A central feature of the Bonk-Schramm extension is that it preserves hyperbolicity, with the
same hyperbolicity constant $\delta$, as we prove now.›

lemma (in Gromov_hyperbolic_space) Bonk_Schramm_extension_unfolded_hyperbolic:
fixes x y z t::"('a::metric_space) Bonk_Schramm_extension_unfolded"
assumes "x ∈ extended_distance_set"
"y ∈ extended_distance_set"
"z ∈ extended_distance_set"
"t ∈ extended_distance_set"
shows "extended_distance x y + extended_distance z t ≤ max (extended_distance x z + extended_distance y t) (extended_distance x t + extended_distance y z) + 2 * deltaG(TYPE('a))"
proof -
interpret wo: wo_rel Bonk_Schramm_extension_unfolded_wo
using well_order_on_Well_order wo_rel_def wfrec_def metric_space_class.Bonk_Schramm_extension_unfolded_wo_props(1) by blast

(*To prove the hyperbolicity inequality, we prove it on larger and larger sets, by induction, adding
one point $a$ at a time. Then the result will follow readily.*)
have ineq_rec: "∀x y z t. x ∈ wo.under a ∩ extended_distance_set ⟶ y ∈ wo.under a ∩ extended_distance_set ⟶ z ∈ wo.under a ∩ extended_distance_set ⟶ t ∈ wo.under a ∩ extended_distance_set
⟶ extended_distance x y + extended_distance z t ≤ max (extended_distance x z + extended_distance y t) (extended_distance x t + extended_distance y z) + 2 * deltaG(TYPE('a))"
for a::"'a Bonk_Schramm_extension_unfolded"
proof (rule wo.well_order_induct[of _ a])
fix a::"'a Bonk_Schramm_extension_unfolded"
assume IH_orig: "∀b. b ≠ a ∧ (b, a) ∈ Bonk_Schramm_extension_unfolded_wo ⟶
(∀x y z t. x ∈ wo.under b ∩ extended_distance_set ⟶
y ∈ wo.under b ∩ extended_distance_set ⟶
z ∈ wo.under b ∩ extended_distance_set ⟶
t ∈ wo.under b ∩ extended_distance_set ⟶
extended_distance x y + extended_distance z t ≤ max (extended_distance x z + extended_distance y t) (extended_distance x t + extended_distance y z) + 2 * deltaG(TYPE('a)))"
(*Reformulate the induction assumption in more convenient terms*)
then have IH: "extended_distance x y + extended_distance z t ≤ max (extended_distance x z + extended_distance y t) (extended_distance x t + extended_distance y z) + 2 * deltaG(TYPE('a))"
if "x ∈ wo.underS a ∩ extended_distance_set"
"y ∈ wo.underS a ∩ extended_distance_set"
"z ∈ wo.underS a ∩ extended_distance_set"
"t ∈ wo.underS a ∩ extended_distance_set"
for x y z t
proof -
define b where "b = wo.max2 (wo.max2 x y) (wo.max2 z t)"
have "b ∈ wo.underS a" using that b_def by auto
have "x ∈ wo.under b" "y ∈ wo.under b" "z ∈ wo.under b" "t ∈ wo.under b" unfolding b_def
by (metis UNIV_I metric_space_class.Bonk_Schramm_extension_unfolded_wo_props(1) mem_Collect_eq under_def well_order_on_Well_order wo.TOTALS wo.max2_iff)+
then show ?thesis using that IH_orig ‹b ∈ wo.underS a› underS_E by fastforce
qed

consider "a ∉ extended_distance_set" | "a ∈ extended_distance_set" by auto
then show "∀x y z t. x ∈ wo.under a ∩ extended_distance_set ⟶
y ∈ wo.under a ∩ extended_distance_set ⟶
z ∈ wo.under a ∩ extended_distance_set ⟶
t ∈ wo.under a ∩ extended_distance_set ⟶
extended_distance x y + extended_distance z t ≤ max (extended_distance x z + extended_distance y t) (extended_distance x t + extended_distance y z) + 2 * deltaG(TYPE('a))"
proof (cases)
(* If the point $a$ is not admissible for the distance, then we are not adding any point,
and the result follows readily from the assumption hypothesis.*)
case 1
then have "wo.under a ∩ extended_distance_set = wo.underS a ∩ extended_distance_set"
apply auto
apply (metis mem_Collect_eq underS_I under_def)
then show ?thesis using IH by auto
next
(*Now, we assume that the point $a$ is admissible. We will first check the desired
inequality when the first point is $a$, and the other points are strictly below $a$.
The general inequality will follow from this one by a simple reduction below*)
case 2
then have a: "extended_distance a a = 0" unfolding metric_space_class.extended_distance_set_def by auto
have main_ineq: "extended_distance a y + extended_distance z t ≤ max (extended_distance a z + extended_distance y t) (extended_distance a t + extended_distance y z) + 2 * deltaG(TYPE('a))"
if yzt: "y ∈ wo.underS a ∩ extended_distance_set"
"z ∈ wo.underS a ∩ extended_distance_set"
"t ∈ wo.underS a ∩ extended_distance_set"
for y z t
proof (cases a)
(*In the case of a basepoint, the desired inequality follows from the corresponding
inequality in the original --hyperbolic-- space.*)
case A: (basepoint a')
then have "y ∈ range basepoint" using metric_space_class.Bonk_Schramm_extension_unfolded_wo_props(2)
by (metis yzt(1) Compl_iff Int_iff range_eqI wo.max2_def wo.max2_underS'(2))
then obtain y' where y: "y = basepoint y'" by auto
have "z ∈ range basepoint" using metric_space_class.Bonk_Schramm_extension_unfolded_wo_props(2) A
by (metis yzt(2) Compl_iff Int_iff range_eqI wo.max2_def wo.max2_underS'(2))
then obtain z' where z: "z = basepoint z'" by auto
have "t ∈ range basepoint" using metric_space_class.Bonk_Schramm_extension_unfolded_wo_props(2) A
by (metis yzt(3) Compl_iff Int_iff range_eqI wo.max2_def wo.max2_underS'(2))
then obtain t' where t: "t = basepoint t'" by auto
show ?thesis
unfolding y z t A metric_space_class.extended_distance_basepoint
using hyperb_quad_ineq UNIV_I unfolding Gromov_hyperbolic_subset_def by auto
next
(*In the case of a Cauchy sequence, the desired inequality is obtained from the inequality
for the points defining the Cauchy sequence --which holds thanks to the induction
assumption-- by passing to the limit.*)
case C: (would_be_Cauchy u)
then have u: "would_be_Cauchy u ∈ extended_distance_set"
"u n ∈ extended_distance_set ∩ wo.underS (would_be_Cauchy u)" for n
using metric_space_class.extended_distance_set_Cauchy 2 by auto
have lim: "(λn. extended_distance y (u n)) ⇢ (extended_distance y (would_be_Cauchy u))"
if y: "y ∈ extended_distance_set" for y
proof -
have a: "abs(extended_distance y (u n) - extended_distance y (would_be_Cauchy u)) ≤ extended_distance (u n) (would_be_Cauchy u)" for n
using u(2)[of n] 2 y metric_space_class.extended_distance_triang_ineq unfolding C
apply (subst abs_le_iff) apply (auto simp add: algebra_simps)
by (metis metric_space_class.extended_distance_symmetric)
have b: "(λn. extended_distance (u n) (would_be_Cauchy u)) ⇢ 0"
unfolding C apply (rule metric_space_class.extended_distance_Cauchy(2))
using metric_space_class.extended_distance_set_Cauchy[of u] C 2 by auto
have "(λn. abs(extended_distance y (u n) - extended_distance y (would_be_Cauchy u))) ⇢ 0"
apply (rule tendsto_sandwich[of "λ_. 0", OF _ _ _ b]) using a by auto
then show "(λn. extended_distance y (u n)) ⇢ extended_distance y (would_be_Cauchy u)"
using Lim_null tendsto_rabs_zero_cancel by blast
qed
have "max (extended_distance (u n) z + extended_distance y t) (extended_distance (u n) t + extended_distance y z) + 2 * deltaG(TYPE('a)) - extended_distance (u n) y - extended_distance z t ≥ 0" for n
using IH[of "u n" y z t] u yzt C by auto
moreover have "(λn. max (extended_distance (u n) z + extended_distance y t) (extended_distance (u n) t + extended_distance y z) + 2 * deltaG(TYPE('a)) - extended_distance (u n) y - extended_distance z t)
⇢ max (extended_distance (would_be_Cauchy u) z + extended_distance y t) (extended_distance (would_be_Cauchy u) t + extended_distance y z) + 2 * deltaG(TYPE('a)) - extended_distance (would_be_Cauchy u) y - extended_distance z t"
apply (auto intro!: tendsto_intros)
using lim that u by (auto simp add: metric_space_class.extended_distance_symmetric)
ultimately have I: "max (extended_distance (would_be_Cauchy u) z + extended_distance y t) (extended_distance (would_be_Cauchy u) t + extended_distance y z) + 2 * deltaG(TYPE('a)) - extended_distance (would_be_Cauchy u) y - extended_distance z t ≥ 0"
using LIMSEQ_le_const by blast
then show ?thesis unfolding C by auto
next
(*In the case of a middle, the desired inequality follows from the formula defining
the distance to the middle, and simple computations, as explained by Bonk and Schramm.*)
case M: (middle c d)
then have cd: "c ∈ extended_distance_set ∩ wo.underS (middle c d)"
"d ∈ extended_distance_set ∩ wo.underS (middle c d)"
using 2 metric_space_class.extended_distance_set_middle'[of c d] by auto

have bdd: "bdd_above ((λw. extended_distance s w - max (extended_distance c w) (extended_distance d w)) (wo.underS (middle c d) ∩ extended_distance_set))"
if "s ∈ extended_distance_set" for s
proof (rule bdd_aboveI2)
fix w assume w: "w ∈ wo.underS (middle c d) ∩ extended_distance_set"
have "extended_distance s w ≤ extended_distance s c + extended_distance c w"
using w that metric_space_class.extended_distance_triang_ineq cd by auto
also have "... ≤ extended_distance s c + max (extended_distance c w) (extended_distance d w)"
by auto
finally show "extended_distance s w - max (extended_distance c w) (extended_distance d w)
≤ extended_distance s c"
by auto
qed

have I: "extended_distance y