Theory Bonk_Schramm_Extension

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

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_aux`S  Field wo_aux"
  shows "wo_aux.AboveS (map_aux`S)  {}"
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
    by (simp add: AboveS_Field wo_aux.suc_def)
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
    by (simp add: AboveS_Field wo_aux.suc_def)
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}"

lemma wo_adm_extend_distance:
  "wo.adm_wo extend_distance"
unfolding wo.adm_wo_def proof (auto)
  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 "ywo.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)"
using wo.worec_fixpoint[OF wo_adm_extend_distance] unfolding extend_distance_fp_def.

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)
    apply (simp add: that dist_commute)+
    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)"
    by (auto simp add: Bonk_Schramm_extension_unfolded_wo_props')
  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 wwo.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 (simp add: assms)
apply (rule SUP_cong)
apply (auto simp add: wo.max2_def)
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)"
    by (auto simp add: Bonk_Schramm_extension_unfolded_wo_props')
  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)
        by (simp add: underS_E 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 wwo.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 wwo.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 wwo.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)]
          by (auto simp add: bdd [OF that(2)] ab(1) T(1) add_diff_eq image_comp)
        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))"
            by (simp add: Cauchy_iff real_Cauchy_convergent)
          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"
          apply (auto intro!: tendsto_add)
          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"
          apply (auto intro!: tendsto_add)
          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 wwo.underS (middle a b)  extended_distance_set.
          extended_distance a w - max (extended_distance a w) (extended_distance b w))"
    apply (rule cSUP_upper)
    apply (simp add: assms(2) Bonk_Schramm_extension_unfolded_wo_props'(2))
    by (rule bdd_aboveI2[of _ _ 0], auto)
  ultimately have "0  (SUP wwo.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 wwo.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 wwo.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 wwo.underS (middle a b)  extended_distance_set.
          extended_distance b w - max (extended_distance a w) (extended_distance b w))"
    apply (rule cSUP_upper)
    apply (simp add: assms(1) Bonk_Schramm_extension_unfolded_wo_props'(1))
    by (rule bdd_aboveI2[of _ _ 0], auto)
  ultimately have "0  (SUP wwo.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 wwo.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 wwo.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))"
      by (simp add: Cauchy_iff real_Cauchy_convergent)
    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›

quotient_type (overloaded) 'a 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 = (xU. 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
    by (auto simp add: extended_distance_set_def)
  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
        apply (auto simp add: under_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)
        by (simp add: underS_E 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