[STATEMENT]
lemma geodesic_segmentI2 [intro]:
  assumes "isometry_on {a..b} g" "a \<le> (b::real)"
  shows "geodesic_segment_between (g`{a..b}) (g a) (g b)"
        "geodesic_segment (g`{a..b})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_between (g ` {a..b}) (g a) (g b) &&& geodesic_segment (g ` {a..b})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. geodesic_segment_between (g ` {a..b}) (g a) (g b)
 2. geodesic_segment (g ` {a..b})
[PROOF STEP]
define h where "h = (\<lambda>t. g (t+a))"
[PROOF STATE]
proof (state)
this:
h = (\<lambda>t. g (t + a))

goal (2 subgoals):
 1. geodesic_segment_between (g ` {a..b}) (g a) (g b)
 2. geodesic_segment (g ` {a..b})
[PROOF STEP]
have *: "isometry_on {0..b-a} h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isometry_on {0..b - a} h
[PROOF STEP]
apply (rule isometry_onI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> {0..b - a}; y \<in> {0..b - a}\<rbrakk> \<Longrightarrow> dist (h x) (h y) = dist x y
[PROOF STEP]
using \<open>isometry_on {a..b} g\<close> \<open>a \<le> b\<close>
[PROOF STATE]
proof (prove)
using this:
isometry_on {a..b} g
a \<le> b

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> {0..b - a}; y \<in> {0..b - a}\<rbrakk> \<Longrightarrow> dist (h x) (h y) = dist x y
[PROOF STEP]
by (auto simp add: isometry_on_def h_def)
[PROOF STATE]
proof (state)
this:
isometry_on {0..b - a} h

goal (2 subgoals):
 1. geodesic_segment_between (g ` {a..b}) (g a) (g b)
 2. geodesic_segment (g ` {a..b})
[PROOF STEP]
have **: "dist (h 0) (h (b-a)) = b-a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (h 0) (h (b - a)) = b - a
[PROOF STEP]
using isometry_onD[OF \<open>isometry_on {0..b-a} h\<close>, of 0 "b-a"] \<open>a \<le> b\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 \<in> {0..b - a}; b - a \<in> {0..b - a}\<rbrakk> \<Longrightarrow> dist (h 0) (h (b - a)) = dist 0 (b - a)
a \<le> b

goal (1 subgoal):
 1. dist (h 0) (h (b - a)) = b - a
[PROOF STEP]
unfolding dist_real_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 \<in> {0..b - a}; b - a \<in> {0..b - a}\<rbrakk> \<Longrightarrow> dist (h 0) (h (b - a)) = \<bar>0 - (b - a)\<bar>
a \<le> b

goal (1 subgoal):
 1. dist (h 0) (h (b - a)) = b - a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (h 0) (h (b - a)) = b - a

goal (2 subgoals):
 1. geodesic_segment_between (g ` {a..b}) (g a) (g b)
 2. geodesic_segment (g ` {a..b})
[PROOF STEP]
have "geodesic_segment_between (h`{0..b-a}) (h 0) (h (b-a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_between (h ` {0..b - a}) (h 0) (h (b - a))
[PROOF STEP]
unfolding geodesic_segment_between_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>g. g 0 = h 0 \<and> g (dist (h 0) (h (b - a))) = h (b - a) \<and> isometry_on {0..dist (h 0) (h (b - a))} g \<and> h ` {0..b - a} = g ` {0..dist (h 0) (h (b - a))}
[PROOF STEP]
apply (rule exI[of _ h])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h 0 = h 0 \<and> h (dist (h 0) (h (b - a))) = h (b - a) \<and> isometry_on {0..dist (h 0) (h (b - a))} h \<and> h ` {0..b - a} = h ` {0..dist (h 0) (h (b - a))}
[PROOF STEP]
unfolding **
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h 0 = h 0 \<and> h (b - a) = h (b - a) \<and> isometry_on {0..b - a} h \<and> h ` {0..b - a} = h ` {0..b - a}
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
isometry_on {0..b - a} h

goal (1 subgoal):
 1. h 0 = h 0 \<and> h (b - a) = h (b - a) \<and> isometry_on {0..b - a} h \<and> h ` {0..b - a} = h ` {0..b - a}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
geodesic_segment_between (h ` {0..b - a}) (h 0) (h (b - a))

goal (2 subgoals):
 1. geodesic_segment_between (g ` {a..b}) (g a) (g b)
 2. geodesic_segment (g ` {a..b})
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
geodesic_segment_between (h ` {0..b - a}) (h 0) (h (b - a))

goal (2 subgoals):
 1. geodesic_segment_between (g ` {a..b}) (g a) (g b)
 2. geodesic_segment (g ` {a..b})
[PROOF STEP]
have "g`{a..b} = h`{0..b-a}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g ` {a..b} = h ` {0..b - a}
[PROOF STEP]
unfolding h_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g ` {a..b} = (\<lambda>t. g (t + a)) ` {0..b - a}
[PROOF STEP]
apply (auto simp add: image_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>a \<le> xa; xa \<le> b\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..b - a}. g xa = g (x + a)
[PROOF STEP]
by (metis add.commute atLeastAtMost_iff diff_ge_0_iff_ge diff_right_mono le_add_diff_inverse)
[PROOF STATE]
proof (state)
this:
g ` {a..b} = h ` {0..b - a}

goal (2 subgoals):
 1. geodesic_segment_between (g ` {a..b}) (g a) (g b)
 2. geodesic_segment (g ` {a..b})
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
g ` {a..b} = h ` {0..b - a}

goal (2 subgoals):
 1. geodesic_segment_between (g ` {a..b}) (g a) (g b)
 2. geodesic_segment (g ` {a..b})
[PROOF STEP]
have "h 0 = g a" "h (b-a) = g b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h 0 = g a &&& h (b - a) = g b
[PROOF STEP]
unfolding h_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g (0 + a) = g a &&& g (b - a + a) = g b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
h 0 = g a
h (b - a) = g b

goal (2 subgoals):
 1. geodesic_segment_between (g ` {a..b}) (g a) (g b)
 2. geodesic_segment (g ` {a..b})
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
geodesic_segment_between (h ` {0..b - a}) (h 0) (h (b - a))
g ` {a..b} = h ` {0..b - a}
h 0 = g a
h (b - a) = g b
[PROOF STEP]
show "geodesic_segment_between (g`{a..b}) (g a) (g b)"
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_between (h ` {0..b - a}) (h 0) (h (b - a))
g ` {a..b} = h ` {0..b - a}
h 0 = g a
h (b - a) = g b

goal (1 subgoal):
 1. geodesic_segment_between (g ` {a..b}) (g a) (g b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
geodesic_segment_between (g ` {a..b}) (g a) (g b)

goal (1 subgoal):
 1. geodesic_segment (g ` {a..b})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
geodesic_segment_between (g ` {a..b}) (g a) (g b)
[PROOF STEP]
show "geodesic_segment (g`{a..b})"
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_between (g ` {a..b}) (g a) (g b)

goal (1 subgoal):
 1. geodesic_segment (g ` {a..b})
[PROOF STEP]
unfolding geodesic_segment_def
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_between (g ` {a..b}) (g a) (g b)

goal (1 subgoal):
 1. \<exists>x. Ex (geodesic_segment_between (g ` {a..b}) x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
geodesic_segment (g ` {a..b})

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma geodesic_segmentD:
  assumes "geodesic_segment_between G x y"
  shows "\<exists>g::(real \<Rightarrow> _). (g t = x \<and> g (t + dist x y) = y \<and> isometry_on {t..t+dist x y} g \<and> G = g`{t..t+dist x y})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>g. g t = x \<and> g (t + dist x y) = y \<and> isometry_on {t..t + dist x y} g \<and> G = g ` {t..t + dist x y}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>g. g t = x \<and> g (t + dist x y) = y \<and> isometry_on {t..t + dist x y} g \<and> G = g ` {t..t + dist x y}
[PROOF STEP]
obtain h where h: "h 0 = x" "h (dist x y) = y" "isometry_on {0..dist x y} h" "G = h`{0..dist x y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>h. \<lbrakk>h 0 = x; h (dist x y) = y; isometry_on {0..dist x y} h; G = h ` {0..dist x y}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson \<open>geodesic_segment_between G x y\<close> geodesic_segment_between_def)
[PROOF STATE]
proof (state)
this:
h 0 = x
h (dist x y) = y
isometry_on {0..dist x y} h
G = h ` {0..dist x y}

goal (1 subgoal):
 1. \<exists>g. g t = x \<and> g (t + dist x y) = y \<and> isometry_on {t..t + dist x y} g \<and> G = g ` {t..t + dist x y}
[PROOF STEP]
have * [simp]: "(\<lambda>x. x - t) ` {t..t + dist x y} = {0..dist x y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. x - t) ` {t..t + dist x y} = {0..dist x y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>x. x - t) ` {t..t + dist x y} = {0..dist x y}

goal (1 subgoal):
 1. \<exists>g. g t = x \<and> g (t + dist x y) = y \<and> isometry_on {t..t + dist x y} g \<and> G = g ` {t..t + dist x y}
[PROOF STEP]
define g where "g = (\<lambda>s. h (s - t))"
[PROOF STATE]
proof (state)
this:
g = (\<lambda>s. h (s - t))

goal (1 subgoal):
 1. \<exists>g. g t = x \<and> g (t + dist x y) = y \<and> isometry_on {t..t + dist x y} g \<and> G = g ` {t..t + dist x y}
[PROOF STEP]
have "g t = x" "g (t + dist x y) = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g t = x &&& g (t + dist x y) = y
[PROOF STEP]
using h assms(1)
[PROOF STATE]
proof (prove)
using this:
h 0 = x
h (dist x y) = y
isometry_on {0..dist x y} h
G = h ` {0..dist x y}
geodesic_segment_between G x y

goal (1 subgoal):
 1. g t = x &&& g (t + dist x y) = y
[PROOF STEP]
unfolding g_def
[PROOF STATE]
proof (prove)
using this:
h 0 = x
h (dist x y) = y
isometry_on {0..dist x y} h
G = h ` {0..dist x y}
geodesic_segment_between G x y

goal (1 subgoal):
 1. h (t - t) = x &&& h (t + dist x y - t) = y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g t = x
g (t + dist x y) = y

goal (1 subgoal):
 1. \<exists>g. g t = x \<and> g (t + dist x y) = y \<and> isometry_on {t..t + dist x y} g \<and> G = g ` {t..t + dist x y}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
g t = x
g (t + dist x y) = y

goal (1 subgoal):
 1. \<exists>g. g t = x \<and> g (t + dist x y) = y \<and> isometry_on {t..t + dist x y} g \<and> G = g ` {t..t + dist x y}
[PROOF STEP]
have "isometry_on {t..t+dist x y} g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isometry_on {t..t + dist x y} g
[PROOF STEP]
unfolding g_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isometry_on {t..t + dist x y} (\<lambda>s. h (s - t))
[PROOF STEP]
apply (rule isometry_on_compose[of _ _ h])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. isometry_on {t..t + dist x y} (\<lambda>x. x - t)
 2. isometry_on ((\<lambda>x. x - t) ` {t..t + dist x y}) h
[PROOF STEP]
by (simp add: dist_real_def isometry_on_def, simp add: h(3))
[PROOF STATE]
proof (state)
this:
isometry_on {t..t + dist x y} g

goal (1 subgoal):
 1. \<exists>g. g t = x \<and> g (t + dist x y) = y \<and> isometry_on {t..t + dist x y} g \<and> G = g ` {t..t + dist x y}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
isometry_on {t..t + dist x y} g

goal (1 subgoal):
 1. \<exists>g. g t = x \<and> g (t + dist x y) = y \<and> isometry_on {t..t + dist x y} g \<and> G = g ` {t..t + dist x y}
[PROOF STEP]
have "g` {t..t + dist x y} = G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g ` {t..t + dist x y} = G
[PROOF STEP]
unfolding g_def h(4)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. h (s - t)) ` {t..t + dist x y} = h ` {0..dist x y}
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. x - t) ` {t..t + dist x y} = {0..dist x y}

goal (1 subgoal):
 1. (\<lambda>s. h (s - t)) ` {t..t + dist x y} = h ` {0..dist x y}
[PROOF STEP]
by (metis image_image)
[PROOF STATE]
proof (state)
this:
g ` {t..t + dist x y} = G

goal (1 subgoal):
 1. \<exists>g. g t = x \<and> g (t + dist x y) = y \<and> isometry_on {t..t + dist x y} g \<and> G = g ` {t..t + dist x y}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
g t = x
g (t + dist x y) = y
isometry_on {t..t + dist x y} g
g ` {t..t + dist x y} = G
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
g t = x
g (t + dist x y) = y
isometry_on {t..t + dist x y} g
g ` {t..t + dist x y} = G

goal (1 subgoal):
 1. \<exists>g. g t = x \<and> g (t + dist x y) = y \<and> isometry_on {t..t + dist x y} g \<and> G = g ` {t..t + dist x y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>g. g t = x \<and> g (t + dist x y) = y \<and> isometry_on {t..t + dist x y} g \<and> G = g ` {t..t + dist x y}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma geodesic_segment_endpoints [simp]:
  assumes "geodesic_segment_between G x y"
  shows "x \<in> G" "y \<in> G" "G \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> G &&& y \<in> G &&& G \<noteq> {}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_between G x y

goal (1 subgoal):
 1. x \<in> G &&& y \<in> G &&& G \<noteq> {}
[PROOF STEP]
unfolding geodesic_segment_between_def
[PROOF STATE]
proof (prove)
using this:
\<exists>g. g 0 = x \<and> g (dist x y) = y \<and> isometry_on {0..dist x y} g \<and> G = g ` {0..dist x y}

goal (1 subgoal):
 1. x \<in> G &&& y \<in> G &&& G \<noteq> {}
[PROOF STEP]
by (auto, metis atLeastAtMost_iff image_eqI less_eq_real_def zero_le_dist)


[STATEMENT]
lemma geodesic_segment_commute:
  assumes "geodesic_segment_between G x y"
  shows "geodesic_segment_between G y x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_between G y x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. geodesic_segment_between G y x
[PROOF STEP]
obtain g::"real\<Rightarrow>'a" where g: "g 0 = x" "g (dist x y) = y" "isometry_on {0..dist x y} g" "G = g`{0..dist x y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g 0 = x; g (dist x y) = y; isometry_on {0..dist x y} g; G = g ` {0..dist x y}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson \<open>geodesic_segment_between G x y\<close> geodesic_segment_between_def)
[PROOF STATE]
proof (state)
this:
g 0 = x
g (dist x y) = y
isometry_on {0..dist x y} g
G = g ` {0..dist x y}

goal (1 subgoal):
 1. geodesic_segment_between G y x
[PROOF STEP]
define h::"real\<Rightarrow>'a" where "h = (\<lambda>t. g(dist x y-t))"
[PROOF STATE]
proof (state)
this:
h = (\<lambda>t. g (dist x y - t))

goal (1 subgoal):
 1. geodesic_segment_between G y x
[PROOF STEP]
have "(\<lambda>t. dist x y -t)`{0..dist x y} = {0..dist x y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (-) (dist x y) ` {0..dist x y} = {0..dist x y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(-) (dist x y) ` {0..dist x y} = {0..dist x y}

goal (1 subgoal):
 1. geodesic_segment_between G y x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(-) (dist x y) ` {0..dist x y} = {0..dist x y}
[PROOF STEP]
have "h`{0..dist x y} = G"
[PROOF STATE]
proof (prove)
using this:
(-) (dist x y) ` {0..dist x y} = {0..dist x y}

goal (1 subgoal):
 1. h ` {0..dist x y} = G
[PROOF STEP]
unfolding g(4) h_def
[PROOF STATE]
proof (prove)
using this:
(-) (dist x y) ` {0..dist x y} = {0..dist x y}

goal (1 subgoal):
 1. (\<lambda>t. g (dist x y - t)) ` {0..dist x y} = g ` {0..dist x y}
[PROOF STEP]
by (metis image_image)
[PROOF STATE]
proof (state)
this:
h ` {0..dist x y} = G

goal (1 subgoal):
 1. geodesic_segment_between G y x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
h ` {0..dist x y} = G

goal (1 subgoal):
 1. geodesic_segment_between G y x
[PROOF STEP]
have "h 0 = y" "h (dist x y) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h 0 = y &&& h (dist x y) = x
[PROOF STEP]
unfolding h_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g (dist x y - 0) = y &&& g (dist x y - dist x y) = x
[PROOF STEP]
using g
[PROOF STATE]
proof (prove)
using this:
g 0 = x
g (dist x y) = y
isometry_on {0..dist x y} g
G = g ` {0..dist x y}

goal (1 subgoal):
 1. g (dist x y - 0) = y &&& g (dist x y - dist x y) = x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
h 0 = y
h (dist x y) = x

goal (1 subgoal):
 1. geodesic_segment_between G y x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
h 0 = y
h (dist x y) = x

goal (1 subgoal):
 1. geodesic_segment_between G y x
[PROOF STEP]
have "isometry_on {0..dist x y} h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isometry_on {0..dist x y} h
[PROOF STEP]
unfolding h_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isometry_on {0..dist x y} (\<lambda>t. g (dist x y - t))
[PROOF STEP]
apply (rule isometry_on_compose[of _ _ g])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. isometry_on {0..dist x y} ((-) (dist x y))
 2. isometry_on ((-) (dist x y) ` {0..dist x y}) g
[PROOF STEP]
using g(3)
[PROOF STATE]
proof (prove)
using this:
isometry_on {0..dist x y} g

goal (2 subgoals):
 1. isometry_on {0..dist x y} ((-) (dist x y))
 2. isometry_on ((-) (dist x y) ` {0..dist x y}) g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
isometry_on {0..dist x y} h

goal (1 subgoal):
 1. geodesic_segment_between G y x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
h ` {0..dist x y} = G
h 0 = y
h (dist x y) = x
isometry_on {0..dist x y} h
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
h ` {0..dist x y} = G
h 0 = y
h (dist x y) = x
isometry_on {0..dist x y} h

goal (1 subgoal):
 1. geodesic_segment_between G y x
[PROOF STEP]
unfolding geodesic_segment_between_def
[PROOF STATE]
proof (prove)
using this:
h ` {0..dist x y} = G
h 0 = y
h (dist x y) = x
isometry_on {0..dist x y} h

goal (1 subgoal):
 1. \<exists>g. g 0 = y \<and> g (dist y x) = x \<and> isometry_on {0..dist y x} g \<and> G = g ` {0..dist y x}
[PROOF STEP]
by (auto simp add: dist_commute)
[PROOF STATE]
proof (state)
this:
geodesic_segment_between G y x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma geodesic_segment_dist:
  assumes "geodesic_segment_between G x y" "a \<in> G"
  shows "dist x a + dist a y = dist x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist x a + dist a y = dist x y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist x a + dist a y = dist x y
[PROOF STEP]
obtain g where g: "g 0 = x" "g (dist x y) = y" "isometry_on {0..dist x y} g" "G = g`{0..dist x y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g 0 = x; g (dist x y) = y; isometry_on {0..dist x y} g; G = g ` {0..dist x y}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson \<open>geodesic_segment_between G x y\<close> geodesic_segment_between_def)
[PROOF STATE]
proof (state)
this:
g 0 = x
g (dist x y) = y
isometry_on {0..dist x y} g
G = g ` {0..dist x y}

goal (1 subgoal):
 1. dist x a + dist a y = dist x y
[PROOF STEP]
obtain t where t: "t \<in> {0..dist x y}" "a = g t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t. \<lbrakk>t \<in> {0..dist x y}; a = g t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using g(4) assms
[PROOF STATE]
proof (prove)
using this:
G = g ` {0..dist x y}
geodesic_segment_between G x y
a \<in> G

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>t \<in> {0..dist x y}; a = g t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t \<in> {0..dist x y}
a = g t

goal (1 subgoal):
 1. dist x a + dist a y = dist x y
[PROOF STEP]
have "dist x a = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist x a = t
[PROOF STEP]
using isometry_onD[OF g(3) _ t(1), of 0]
[PROOF STATE]
proof (prove)
using this:
0 \<in> {0..dist x y} \<Longrightarrow> dist (g 0) (g t) = dist 0 t

goal (1 subgoal):
 1. dist x a = t
[PROOF STEP]
unfolding g(1) dist_real_def t(2)
[PROOF STATE]
proof (prove)
using this:
0 \<in> {0..dist x y} \<Longrightarrow> dist x (g t) = \<bar>0 - t\<bar>

goal (1 subgoal):
 1. dist x (g t) = t
[PROOF STEP]
using t(1)
[PROOF STATE]
proof (prove)
using this:
0 \<in> {0..dist x y} \<Longrightarrow> dist x (g t) = \<bar>0 - t\<bar>
t \<in> {0..dist x y}

goal (1 subgoal):
 1. dist x (g t) = t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist x a = t

goal (1 subgoal):
 1. dist x a + dist a y = dist x y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
dist x a = t

goal (1 subgoal):
 1. dist x a + dist a y = dist x y
[PROOF STEP]
have "dist a y = dist x y - t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist a y = dist x y - t
[PROOF STEP]
using isometry_onD[OF g(3) _ t(1), of "dist x y"]
[PROOF STATE]
proof (prove)
using this:
dist x y \<in> {0..dist x y} \<Longrightarrow> dist (g (dist x y)) (g t) = dist (dist x y) t

goal (1 subgoal):
 1. dist a y = dist x y - t
[PROOF STEP]
unfolding g(2) dist_real_def t(2)
[PROOF STATE]
proof (prove)
using this:
dist x y \<in> {0..dist x y} \<Longrightarrow> dist y (g t) = \<bar>dist x y - t\<bar>

goal (1 subgoal):
 1. dist (g t) y = dist x y - t
[PROOF STEP]
using t(1)
[PROOF STATE]
proof (prove)
using this:
dist x y \<in> {0..dist x y} \<Longrightarrow> dist y (g t) = \<bar>dist x y - t\<bar>
t \<in> {0..dist x y}

goal (1 subgoal):
 1. dist (g t) y = dist x y - t
[PROOF STEP]
by (auto simp add: dist_commute)
[PROOF STATE]
proof (state)
this:
dist a y = dist x y - t

goal (1 subgoal):
 1. dist x a + dist a y = dist x y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
dist x a = t
dist a y = dist x y - t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dist x a = t
dist a y = dist x y - t

goal (1 subgoal):
 1. dist x a + dist a y = dist x y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist x a + dist a y = dist x y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma geodesic_segment_dist_unique:
  assumes "geodesic_segment_between G x y" "a \<in> G" "b \<in> G" "dist x a = dist x b"
  shows "a = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a = b
[PROOF STEP]
obtain g where g: "g 0 = x" "g (dist x y) = y" "isometry_on {0..dist x y} g" "G = g`{0..dist x y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g 0 = x; g (dist x y) = y; isometry_on {0..dist x y} g; G = g ` {0..dist x y}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson \<open>geodesic_segment_between G x y\<close> geodesic_segment_between_def)
[PROOF STATE]
proof (state)
this:
g 0 = x
g (dist x y) = y
isometry_on {0..dist x y} g
G = g ` {0..dist x y}

goal (1 subgoal):
 1. a = b
[PROOF STEP]
obtain ta where ta: "ta \<in> {0..dist x y}" "a = g ta"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ta. \<lbrakk>ta \<in> {0..dist x y}; a = g ta\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using g(4) assms
[PROOF STATE]
proof (prove)
using this:
G = g ` {0..dist x y}
geodesic_segment_between G x y
a \<in> G
b \<in> G
dist x a = dist x b

goal (1 subgoal):
 1. (\<And>ta. \<lbrakk>ta \<in> {0..dist x y}; a = g ta\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ta \<in> {0..dist x y}
a = g ta

goal (1 subgoal):
 1. a = b
[PROOF STEP]
have *: "dist x a = ta"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist x a = ta
[PROOF STEP]
unfolding g(1)[symmetric] ta(2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (g 0) (g ta) = ta
[PROOF STEP]
using isometry_onD[OF g(3), of 0 ta]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 \<in> {0..dist x y}; ta \<in> {0..dist x y}\<rbrakk> \<Longrightarrow> dist (g 0) (g ta) = dist 0 ta

goal (1 subgoal):
 1. dist (g 0) (g ta) = ta
[PROOF STEP]
unfolding dist_real_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 \<in> {0..dist x y}; ta \<in> {0..dist x y}\<rbrakk> \<Longrightarrow> dist (g 0) (g ta) = \<bar>0 - ta\<bar>

goal (1 subgoal):
 1. dist (g 0) (g ta) = ta
[PROOF STEP]
using ta(1)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 \<in> {0..dist x y}; ta \<in> {0..dist x y}\<rbrakk> \<Longrightarrow> dist (g 0) (g ta) = \<bar>0 - ta\<bar>
ta \<in> {0..dist x y}

goal (1 subgoal):
 1. dist (g 0) (g ta) = ta
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist x a = ta

goal (1 subgoal):
 1. a = b
[PROOF STEP]
obtain tb where tb: "tb \<in> {0..dist x y}" "b = g tb"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>tb. \<lbrakk>tb \<in> {0..dist x y}; b = g tb\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using g(4) assms
[PROOF STATE]
proof (prove)
using this:
G = g ` {0..dist x y}
geodesic_segment_between G x y
a \<in> G
b \<in> G
dist x a = dist x b

goal (1 subgoal):
 1. (\<And>tb. \<lbrakk>tb \<in> {0..dist x y}; b = g tb\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
tb \<in> {0..dist x y}
b = g tb

goal (1 subgoal):
 1. a = b
[PROOF STEP]
have "dist x b = tb"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist x b = tb
[PROOF STEP]
unfolding g(1)[symmetric] tb(2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (g 0) (g tb) = tb
[PROOF STEP]
using isometry_onD[OF g(3), of 0 tb]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 \<in> {0..dist x y}; tb \<in> {0..dist x y}\<rbrakk> \<Longrightarrow> dist (g 0) (g tb) = dist 0 tb

goal (1 subgoal):
 1. dist (g 0) (g tb) = tb
[PROOF STEP]
unfolding dist_real_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 \<in> {0..dist x y}; tb \<in> {0..dist x y}\<rbrakk> \<Longrightarrow> dist (g 0) (g tb) = \<bar>0 - tb\<bar>

goal (1 subgoal):
 1. dist (g 0) (g tb) = tb
[PROOF STEP]
using tb(1)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 \<in> {0..dist x y}; tb \<in> {0..dist x y}\<rbrakk> \<Longrightarrow> dist (g 0) (g tb) = \<bar>0 - tb\<bar>
tb \<in> {0..dist x y}

goal (1 subgoal):
 1. dist (g 0) (g tb) = tb
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist x b = tb

goal (1 subgoal):
 1. a = b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dist x b = tb
[PROOF STEP]
have "ta = tb"
[PROOF STATE]
proof (prove)
using this:
dist x b = tb

goal (1 subgoal):
 1. ta = tb
[PROOF STEP]
using * \<open>dist x a = dist x b\<close>
[PROOF STATE]
proof (prove)
using this:
dist x b = tb
dist x a = ta
dist x a = dist x b

goal (1 subgoal):
 1. ta = tb
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ta = tb

goal (1 subgoal):
 1. a = b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ta = tb
[PROOF STEP]
show "a = b"
[PROOF STATE]
proof (prove)
using this:
ta = tb

goal (1 subgoal):
 1. a = b
[PROOF STEP]
using ta(2) tb(2)
[PROOF STATE]
proof (prove)
using this:
ta = tb
a = g ta
b = g tb

goal (1 subgoal):
 1. a = b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a = b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma geodesic_segment_union:
  assumes "dist x z = dist x y + dist y z"
          "geodesic_segment_between G x y" "geodesic_segment_between H y z"
  shows "geodesic_segment_between (G \<union> H) x z"
        "G \<inter> H = {y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_between (G \<union> H) x z &&& G \<inter> H = {y}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. geodesic_segment_between (G \<union> H) x z
 2. G \<inter> H = {y}
[PROOF STEP]
obtain g where g: "g 0 = x" "g (dist x y) = y" "isometry_on {0..dist x y} g" "G = g`{0..dist x y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g 0 = x; g (dist x y) = y; isometry_on {0..dist x y} g; G = g ` {0..dist x y}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson \<open>geodesic_segment_between G x y\<close> geodesic_segment_between_def)
[PROOF STATE]
proof (state)
this:
g 0 = x
g (dist x y) = y
isometry_on {0..dist x y} g
G = g ` {0..dist x y}

goal (2 subgoals):
 1. geodesic_segment_between (G \<union> H) x z
 2. G \<inter> H = {y}
[PROOF STEP]
obtain h where h: "h (dist x y) = y" "h (dist x z) = z" "isometry_on {dist x y..dist x z} h" "H = h`{dist x y..dist x z}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>h. \<lbrakk>h (dist x y) = y; h (dist x z) = z; isometry_on {dist x y..dist x z} h; H = h ` {dist x y..dist x z}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding \<open>dist x z = dist x y + dist y z\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>h. \<lbrakk>h (dist x y) = y; h (dist x y + dist y z) = z; isometry_on {dist x y..dist x y + dist y z} h; H = h ` {dist x y..dist x y + dist y z}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using geodesic_segmentD[OF \<open>geodesic_segment_between H y z\<close>, of "dist x y"]
[PROOF STATE]
proof (prove)
using this:
\<exists>g. g (dist x y) = y \<and> g (dist x y + dist y z) = z \<and> isometry_on {dist x y..dist x y + dist y z} g \<and> H = g ` {dist x y..dist x y + dist y z}

goal (1 subgoal):
 1. (\<And>h. \<lbrakk>h (dist x y) = y; h (dist x y + dist y z) = z; isometry_on {dist x y..dist x y + dist y z} h; H = h ` {dist x y..dist x y + dist y z}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
h (dist x y) = y
h (dist x z) = z
isometry_on {dist x y..dist x z} h
H = h ` {dist x y..dist x z}

goal (2 subgoals):
 1. geodesic_segment_between (G \<union> H) x z
 2. G \<inter> H = {y}
[PROOF STEP]
define f where "f = (\<lambda>t. if t \<le> dist x y then g t else h t)"
[PROOF STATE]
proof (state)
this:
f = (\<lambda>t. if t \<le> dist x y then g t else h t)

goal (2 subgoals):
 1. geodesic_segment_between (G \<union> H) x z
 2. G \<inter> H = {y}
[PROOF STEP]
have fg: "f t = g t" if "t \<le> dist x y" for t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f t = g t
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if t \<le> dist x y then g t else h t) = g t
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
t \<le> dist x y

goal (1 subgoal):
 1. (if t \<le> dist x y then g t else h t) = g t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?t \<le> dist x y \<Longrightarrow> f ?t = g ?t

goal (2 subgoals):
 1. geodesic_segment_between (G \<union> H) x z
 2. G \<inter> H = {y}
[PROOF STEP]
have fh: "f t = h t" if "t \<ge> dist x y" for t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f t = h t
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if t \<le> dist x y then g t else h t) = h t
[PROOF STEP]
apply (cases "t > dist x y")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. dist x y < t \<Longrightarrow> (if t \<le> dist x y then g t else h t) = h t
 2. \<not> dist x y < t \<Longrightarrow> (if t \<le> dist x y then g t else h t) = h t
[PROOF STEP]
using that g(2) h(1)
[PROOF STATE]
proof (prove)
using this:
dist x y \<le> t
g (dist x y) = y
h (dist x y) = y

goal (2 subgoals):
 1. dist x y < t \<Longrightarrow> (if t \<le> dist x y then g t else h t) = h t
 2. \<not> dist x y < t \<Longrightarrow> (if t \<le> dist x y then g t else h t) = h t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist x y \<le> ?t \<Longrightarrow> f ?t = h ?t

goal (2 subgoals):
 1. geodesic_segment_between (G \<union> H) x z
 2. G \<inter> H = {y}
[PROOF STEP]
have "f 0 = x" "f (dist x z) = z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f 0 = x &&& f (dist x z) = z
[PROOF STEP]
using fg fh g(1) h(2) assms(1)
[PROOF STATE]
proof (prove)
using this:
?t \<le> dist x y \<Longrightarrow> f ?t = g ?t
dist x y \<le> ?t \<Longrightarrow> f ?t = h ?t
g 0 = x
h (dist x z) = z
dist x z = dist x y + dist y z

goal (1 subgoal):
 1. f 0 = x &&& f (dist x z) = z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f 0 = x
f (dist x z) = z

goal (2 subgoals):
 1. geodesic_segment_between (G \<union> H) x z
 2. G \<inter> H = {y}
[PROOF STEP]
have "f`{0..dist x z} = f`{0..dist x y} \<union> f`{dist x y..dist x z}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` {0..dist x z} = f ` {0..dist x y} \<union> f ` {dist x y..dist x z}
[PROOF STEP]
unfolding assms(1) image_Un[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` {0..dist x y + dist y z} = f ` ({0..dist x y} \<union> {dist x y..dist x y + dist y z})
[PROOF STEP]
by (simp add: ivl_disj_un_two_touch(4))
[PROOF STATE]
proof (state)
this:
f ` {0..dist x z} = f ` {0..dist x y} \<union> f ` {dist x y..dist x z}

goal (2 subgoals):
 1. geodesic_segment_between (G \<union> H) x z
 2. G \<inter> H = {y}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f ` {0..dist x z} = f ` {0..dist x y} \<union> f ` {dist x y..dist x z}

goal (2 subgoals):
 1. geodesic_segment_between (G \<union> H) x z
 2. G \<inter> H = {y}
[PROOF STEP]
have "f`{0..dist x y} = G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` {0..dist x y} = G
[PROOF STEP]
unfolding g(4)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` {0..dist x y} = g ` {0..dist x y}
[PROOF STEP]
using fg image_cong
[PROOF STATE]
proof (prove)
using this:
?t \<le> dist x y \<Longrightarrow> f ?t = g ?t
\<lbrakk>?M = ?N; \<And>x. x \<in> ?N \<Longrightarrow> ?f x = ?g x\<rbrakk> \<Longrightarrow> ?f ` ?M = ?g ` ?N

goal (1 subgoal):
 1. f ` {0..dist x y} = g ` {0..dist x y}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
f ` {0..dist x y} = G

goal (2 subgoals):
 1. geodesic_segment_between (G \<union> H) x z
 2. G \<inter> H = {y}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f ` {0..dist x y} = G

goal (2 subgoals):
 1. geodesic_segment_between (G \<union> H) x z
 2. G \<inter> H = {y}
[PROOF STEP]
have "f`{dist x y..dist x z} = H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` {dist x y..dist x z} = H
[PROOF STEP]
unfolding h(4)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` {dist x y..dist x z} = h ` {dist x y..dist x z}
[PROOF STEP]
using fh image_cong
[PROOF STATE]
proof (prove)
using this:
dist x y \<le> ?t \<Longrightarrow> f ?t = h ?t
\<lbrakk>?M = ?N; \<And>x. x \<in> ?N \<Longrightarrow> ?f x = ?g x\<rbrakk> \<Longrightarrow> ?f ` ?M = ?g ` ?N

goal (1 subgoal):
 1. f ` {dist x y..dist x z} = h ` {dist x y..dist x z}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
f ` {dist x y..dist x z} = H

goal (2 subgoals):
 1. geodesic_segment_between (G \<union> H) x z
 2. G \<inter> H = {y}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f ` {0..dist x z} = f ` {0..dist x y} \<union> f ` {dist x y..dist x z}
f ` {0..dist x y} = G
f ` {dist x y..dist x z} = H
[PROOF STEP]
have "f`{0..dist x z} = G \<union> H"
[PROOF STATE]
proof (prove)
using this:
f ` {0..dist x z} = f ` {0..dist x y} \<union> f ` {dist x y..dist x z}
f ` {0..dist x y} = G
f ` {dist x y..dist x z} = H

goal (1 subgoal):
 1. f ` {0..dist x z} = G \<union> H
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f ` {0..dist x z} = G \<union> H

goal (2 subgoals):
 1. geodesic_segment_between (G \<union> H) x z
 2. G \<inter> H = {y}
[PROOF STEP]
have Ifg: "dist (f s) (f t) = s-t" if "0 \<le> t" "t \<le> s" "s \<le> dist x y" for s t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (f s) (f t) = s - t
[PROOF STEP]
using that fg[of s] fg[of t] isometry_onD[OF g(3), of s t]
[PROOF STATE]
proof (prove)
using this:
0 \<le> t
t \<le> s
s \<le> dist x y
s \<le> dist x y \<Longrightarrow> f s = g s
t \<le> dist x y \<Longrightarrow> f t = g t
\<lbrakk>s \<in> {0..dist x y}; t \<in> {0..dist x y}\<rbrakk> \<Longrightarrow> dist (g s) (g t) = dist s t

goal (1 subgoal):
 1. dist (f s) (f t) = s - t
[PROOF STEP]
unfolding dist_real_def
[PROOF STATE]
proof (prove)
using this:
0 \<le> t
t \<le> s
s \<le> dist x y
s \<le> dist x y \<Longrightarrow> f s = g s
t \<le> dist x y \<Longrightarrow> f t = g t
\<lbrakk>s \<in> {0..dist x y}; t \<in> {0..dist x y}\<rbrakk> \<Longrightarrow> dist (g s) (g t) = \<bar>s - t\<bar>

goal (1 subgoal):
 1. dist (f s) (f t) = s - t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 \<le> ?t; ?t \<le> ?s; ?s \<le> dist x y\<rbrakk> \<Longrightarrow> dist (f ?s) (f ?t) = ?s - ?t

goal (2 subgoals):
 1. geodesic_segment_between (G \<union> H) x z
 2. G \<inter> H = {y}
[PROOF STEP]
have Ifh: "dist (f s) (f t) = s-t" if "dist x y \<le> t" "t \<le> s" "s \<le> dist x z" for s t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (f s) (f t) = s - t
[PROOF STEP]
using that fh[of s] fh[of t] isometry_onD[OF h(3), of s t]
[PROOF STATE]
proof (prove)
using this:
dist x y \<le> t
t \<le> s
s \<le> dist x z
dist x y \<le> s \<Longrightarrow> f s = h s
dist x y \<le> t \<Longrightarrow> f t = h t
\<lbrakk>s \<in> {dist x y..dist x z}; t \<in> {dist x y..dist x z}\<rbrakk> \<Longrightarrow> dist (h s) (h t) = dist s t

goal (1 subgoal):
 1. dist (f s) (f t) = s - t
[PROOF STEP]
unfolding dist_real_def
[PROOF STATE]
proof (prove)
using this:
dist x y \<le> t
t \<le> s
s \<le> dist x z
dist x y \<le> s \<Longrightarrow> f s = h s
dist x y \<le> t \<Longrightarrow> f t = h t
\<lbrakk>s \<in> {dist x y..dist x z}; t \<in> {dist x y..dist x z}\<rbrakk> \<Longrightarrow> dist (h s) (h t) = \<bar>s - t\<bar>

goal (1 subgoal):
 1. dist (f s) (f t) = s - t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>dist x y \<le> ?t; ?t \<le> ?s; ?s \<le> dist x z\<rbrakk> \<Longrightarrow> dist (f ?s) (f ?t) = ?s - ?t

goal (2 subgoals):
 1. geodesic_segment_between (G \<union> H) x z
 2. G \<inter> H = {y}
[PROOF STEP]
have I: "dist (f s) (f t) = s-t" if "0 \<le> t" "t \<le> s" "s \<le> dist x z" for s t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (f s) (f t) = s - t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist (f s) (f t) = s - t
[PROOF STEP]
consider "t \<le> dist x y \<and> s \<ge> dist x y" | "s \<le> dist x y" | "t \<ge> dist x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<le> dist x y \<and> dist x y \<le> s \<Longrightarrow> thesis; s \<le> dist x y \<Longrightarrow> thesis; dist x y \<le> t \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<lbrakk>t \<le> dist x y \<and> dist x y \<le> s \<Longrightarrow> ?thesis; s \<le> dist x y \<Longrightarrow> ?thesis; dist x y \<le> t \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. dist (f s) (f t) = s - t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>t \<le> dist x y \<and> dist x y \<le> s \<Longrightarrow> ?thesis; s \<le> dist x y \<Longrightarrow> ?thesis; dist x y \<le> t \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>t \<le> dist x y \<and> dist x y \<le> s \<Longrightarrow> ?thesis; s \<le> dist x y \<Longrightarrow> ?thesis; dist x y \<le> t \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. dist (f s) (f t) = s - t
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. t \<le> dist x y \<and> dist x y \<le> s \<Longrightarrow> dist (f s) (f t) = s - t
 2. s \<le> dist x y \<Longrightarrow> dist (f s) (f t) = s - t
 3. dist x y \<le> t \<Longrightarrow> dist (f s) (f t) = s - t
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
t \<le> dist x y \<and> dist x y \<le> s

goal (3 subgoals):
 1. t \<le> dist x y \<and> dist x y \<le> s \<Longrightarrow> dist (f s) (f t) = s - t
 2. s \<le> dist x y \<Longrightarrow> dist (f s) (f t) = s - t
 3. dist x y \<le> t \<Longrightarrow> dist (f s) (f t) = s - t
[PROOF STEP]
have "dist (f t) (f s) \<le> dist (f t) (f (dist x y)) + dist (f (dist x y)) (f s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (f t) (f s) \<le> dist (f t) (f (dist x y)) + dist (f (dist x y)) (f s)
[PROOF STEP]
using dist_triangle
[PROOF STATE]
proof (prove)
using this:
dist ?x ?z \<le> dist ?x ?y + dist ?y ?z

goal (1 subgoal):
 1. dist (f t) (f s) \<le> dist (f t) (f (dist x y)) + dist (f (dist x y)) (f s)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (f t) (f s) \<le> dist (f t) (f (dist x y)) + dist (f (dist x y)) (f s)

goal (3 subgoals):
 1. t \<le> dist x y \<and> dist x y \<le> s \<Longrightarrow> dist (f s) (f t) = s - t
 2. s \<le> dist x y \<Longrightarrow> dist (f s) (f t) = s - t
 3. dist x y \<le> t \<Longrightarrow> dist (f s) (f t) = s - t
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (f t) (f s) \<le> dist (f t) (f (dist x y)) + dist (f (dist x y)) (f s)

goal (3 subgoals):
 1. t \<le> dist x y \<and> dist x y \<le> s \<Longrightarrow> dist (f s) (f t) = s - t
 2. s \<le> dist x y \<Longrightarrow> dist (f s) (f t) = s - t
 3. dist x y \<le> t \<Longrightarrow> dist (f s) (f t) = s - t
[PROOF STEP]
have "... \<le> (dist x y - t) + (s - dist x y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (f t) (f (dist x y)) + dist (f (dist x y)) (f s) \<le> dist x y - t + (s - dist x y)
[PROOF STEP]
using that 1 Ifg[of t "dist x y"] Ifh[of "dist x y" s]
[PROOF STATE]
proof (prove)
using this:
0 \<le> t
t \<le> s
s \<le> dist x z
t \<le> dist x y \<and> dist x y \<le> s
\<lbrakk>0 \<le> t; t \<le> dist x y; dist x y \<le> dist x y\<rbrakk> \<Longrightarrow> dist (f (dist x y)) (f t) = dist x y - t
\<lbrakk>dist x y \<le> dist x y; dist x y \<le> s; s \<le> dist x z\<rbrakk> \<Longrightarrow> dist (f s) (f (dist x y)) = s - dist x y

goal (1 subgoal):
 1. dist (f t) (f (dist x y)) + dist (f (dist x y)) (f s) \<le> dist x y - t + (s - dist x y)
[PROOF STEP]
by (auto simp add: dist_commute intro: mono_intros)
[PROOF STATE]
proof (state)
this:
dist (f t) (f (dist x y)) + dist (f (dist x y)) (f s) \<le> dist x y - t + (s - dist x y)

goal (3 subgoals):
 1. t \<le> dist x y \<and> dist x y \<le> s \<Longrightarrow> dist (f s) (f t) = s - t
 2. s \<le> dist x y \<Longrightarrow> dist (f s) (f t) = s - t
 3. dist x y \<le> t \<Longrightarrow> dist (f s) (f t) = s - t
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist (f t) (f s) \<le> dist x y - t + (s - dist x y)
[PROOF STEP]
have *: "dist (f t) (f s) \<le> s - t"
[PROOF STATE]
proof (prove)
using this:
dist (f t) (f s) \<le> dist x y - t + (s - dist x y)

goal (1 subgoal):
 1. dist (f t) (f s) \<le> s - t
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dist (f t) (f s) \<le> s - t

goal (3 subgoals):
 1. t \<le> dist x y \<and> dist x y \<le> s \<Longrightarrow> dist (f s) (f t) = s - t
 2. s \<le> dist x y \<Longrightarrow> dist (f s) (f t) = s - t
 3. dist x y \<le> t \<Longrightarrow> dist (f s) (f t) = s - t
[PROOF STEP]
have "dist x z \<le> dist (f 0) (f t) + dist (f t) (f s) + dist (f s) (f (dist x z))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist x z \<le> dist (f 0) (f t) + dist (f t) (f s) + dist (f s) (f (dist x z))
[PROOF STEP]
unfolding \<open>f 0 = x\<close> \<open>f (dist x z) = z\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist x z \<le> dist x (f t) + dist (f t) (f s) + dist (f s) z
[PROOF STEP]
using dist_triangle4
[PROOF STATE]
proof (prove)
using this:
dist ?x ?t \<le> dist ?x ?y + dist ?y ?z + dist ?z ?t

goal (1 subgoal):
 1. dist x z \<le> dist x (f t) + dist (f t) (f s) + dist (f s) z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist x z \<le> dist (f 0) (f t) + dist (f t) (f s) + dist (f s) (f (dist x z))

goal (3 subgoals):
 1. t \<le> dist x y \<and> dist x y \<le> s \<Longrightarrow> dist (f s) (f t) = s - t
 2. s \<le> dist x y \<Longrightarrow> dist (f s) (f t) = s - t
 3. dist x y \<le> t \<Longrightarrow> dist (f s) (f t) = s - t
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist x z \<le> dist (f 0) (f t) + dist (f t) (f s) + dist (f s) (f (dist x z))

goal (3 subgoals):
 1. t \<le> dist x y \<and> dist x y \<le> s \<Longrightarrow> dist (f s) (f t) = s - t
 2. s \<le> dist x y \<Longrightarrow> dist (f s) (f t) = s - t
 3. dist x y \<le> t \<Longrightarrow> dist (f s) (f t) = s - t
[PROOF STEP]
have "... \<le> t + dist (f t) (f s) + (dist x z - s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (f 0) (f t) + dist (f t) (f s) + dist (f s) (f (dist x z)) \<le> t + dist (f t) (f s) + (dist x z - s)
[PROOF STEP]
using that 1 Ifg[of 0 t] Ifh[of s "dist x z"]
[PROOF STATE]
proof (prove)
using this:
0 \<le> t
t \<le> s
s \<le> dist x z
t \<le> dist x y \<and> dist x y \<le> s
\<lbrakk>0 \<le> 0; 0 \<le> t; t \<le> dist x y\<rbrakk> \<Longrightarrow> dist (f t) (f 0) = t - 0
\<lbrakk>dist x y \<le> s; s \<le> dist x z; dist x z \<le> dist x z\<rbrakk> \<Longrightarrow> dist (f (dist x z)) (f s) = dist x z - s

goal (1 subgoal):
 1. dist (f 0) (f t) + dist (f t) (f s) + dist (f s) (f (dist x z)) \<le> t + dist (f t) (f s) + (dist x z - s)
[PROOF STEP]
by (auto simp add: dist_commute intro: mono_intros)
[PROOF STATE]
proof (state)
this:
dist (f 0) (f t) + dist (f t) (f s) + dist (f s) (f (dist x z)) \<le> t + dist (f t) (f s) + (dist x z - s)

goal (3 subgoals):
 1. t \<le> dist x y \<and> dist x y \<le> s \<Longrightarrow> dist (f s) (f t) = s - t
 2. s \<le> dist x y \<Longrightarrow> dist (f s) (f t) = s - t
 3. dist x y \<le> t \<Longrightarrow> dist (f s) (f t) = s - t
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist x z \<le> t + dist (f t) (f s) + (dist x z - s)
[PROOF STEP]
have "s - t \<le> dist (f t) (f s)"
[PROOF STATE]
proof (prove)
using this:
dist x z \<le> t + dist (f t) (f s) + (dist x z - s)

goal (1 subgoal):
 1. s - t \<le> dist (f t) (f s)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s - t \<le> dist (f t) (f s)

goal (3 subgoals):
 1. t \<le> dist x y \<and> dist x y \<le> s \<Longrightarrow> dist (f s) (f t) = s - t
 2. s \<le> dist x y \<Longrightarrow> dist (f s) (f t) = s - t
 3. dist x y \<le> t \<Longrightarrow> dist (f s) (f t) = s - t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s - t \<le> dist (f t) (f s)
[PROOF STEP]
show "dist (f s) (f t) = s-t"
[PROOF STATE]
proof (prove)
using this:
s - t \<le> dist (f t) (f s)

goal (1 subgoal):
 1. dist (f s) (f t) = s - t
[PROOF STEP]
using * dist_commute
[PROOF STATE]
proof (prove)
using this:
s - t \<le> dist (f t) (f s)
dist (f t) (f s) \<le> s - t
dist ?x ?y = dist ?y ?x

goal (1 subgoal):
 1. dist (f s) (f t) = s - t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (f s) (f t) = s - t

goal (2 subgoals):
 1. s \<le> dist x y \<Longrightarrow> dist (f s) (f t) = s - t
 2. dist x y \<le> t \<Longrightarrow> dist (f s) (f t) = s - t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. s \<le> dist x y \<Longrightarrow> dist (f s) (f t) = s - t
 2. dist x y \<le> t \<Longrightarrow> dist (f s) (f t) = s - t
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
s \<le> dist x y

goal (2 subgoals):
 1. s \<le> dist x y \<Longrightarrow> dist (f s) (f t) = s - t
 2. dist x y \<le> t \<Longrightarrow> dist (f s) (f t) = s - t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<le> dist x y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s \<le> dist x y

goal (1 subgoal):
 1. dist (f s) (f t) = s - t
[PROOF STEP]
using Ifg that
[PROOF STATE]
proof (prove)
using this:
s \<le> dist x y
\<lbrakk>0 \<le> ?t; ?t \<le> ?s; ?s \<le> dist x y\<rbrakk> \<Longrightarrow> dist (f ?s) (f ?t) = ?s - ?t
0 \<le> t
t \<le> s
s \<le> dist x z

goal (1 subgoal):
 1. dist (f s) (f t) = s - t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (f s) (f t) = s - t

goal (1 subgoal):
 1. dist x y \<le> t \<Longrightarrow> dist (f s) (f t) = s - t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist x y \<le> t \<Longrightarrow> dist (f s) (f t) = s - t
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:
dist x y \<le> t

goal (1 subgoal):
 1. dist x y \<le> t \<Longrightarrow> dist (f s) (f t) = s - t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dist x y \<le> t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dist x y \<le> t

goal (1 subgoal):
 1. dist (f s) (f t) = s - t
[PROOF STEP]
using Ifh that
[PROOF STATE]
proof (prove)
using this:
dist x y \<le> t
\<lbrakk>dist x y \<le> ?t; ?t \<le> ?s; ?s \<le> dist x z\<rbrakk> \<Longrightarrow> dist (f ?s) (f ?t) = ?s - ?t
0 \<le> t
t \<le> s
s \<le> dist x z

goal (1 subgoal):
 1. dist (f s) (f t) = s - t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (f s) (f t) = s - t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
dist (f s) (f t) = s - t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 \<le> ?t; ?t \<le> ?s; ?s \<le> dist x z\<rbrakk> \<Longrightarrow> dist (f ?s) (f ?t) = ?s - ?t

goal (2 subgoals):
 1. geodesic_segment_between (G \<union> H) x z
 2. G \<inter> H = {y}
[PROOF STEP]
have "isometry_on {0..dist x z} f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isometry_on {0..dist x z} f
[PROOF STEP]
unfolding isometry_on_def dist_real_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>xa\<in>{0..dist x z}. \<forall>y\<in>{0..dist x z}. dist (f xa) (f y) = \<bar>xa - y\<bar>
[PROOF STEP]
using I
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 \<le> ?t; ?t \<le> ?s; ?s \<le> dist x z\<rbrakk> \<Longrightarrow> dist (f ?s) (f ?t) = ?s - ?t

goal (1 subgoal):
 1. \<forall>xa\<in>{0..dist x z}. \<forall>y\<in>{0..dist x z}. dist (f xa) (f y) = \<bar>xa - y\<bar>
[PROOF STEP]
by (auto, metis abs_of_nonneg dist_commute dist_real_def le_cases zero_le_dist)
[PROOF STATE]
proof (state)
this:
isometry_on {0..dist x z} f

goal (2 subgoals):
 1. geodesic_segment_between (G \<union> H) x z
 2. G \<inter> H = {y}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
isometry_on {0..dist x z} f
[PROOF STEP]
show "geodesic_segment_between (G \<union> H) x z"
[PROOF STATE]
proof (prove)
using this:
isometry_on {0..dist x z} f

goal (1 subgoal):
 1. geodesic_segment_between (G \<union> H) x z
[PROOF STEP]
unfolding geodesic_segment_between_def
[PROOF STATE]
proof (prove)
using this:
isometry_on {0..dist x z} f

goal (1 subgoal):
 1. \<exists>g. g 0 = x \<and> g (dist x z) = z \<and> isometry_on {0..dist x z} g \<and> G \<union> H = g ` {0..dist x z}
[PROOF STEP]
using \<open>f 0 = x\<close> \<open>f (dist x z) = z\<close> \<open>f`{0..dist x z} = G \<union> H\<close>
[PROOF STATE]
proof (prove)
using this:
isometry_on {0..dist x z} f
f 0 = x
f (dist x z) = z
f ` {0..dist x z} = G \<union> H

goal (1 subgoal):
 1. \<exists>g. g 0 = x \<and> g (dist x z) = z \<and> isometry_on {0..dist x z} g \<and> G \<union> H = g ` {0..dist x z}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
geodesic_segment_between (G \<union> H) x z

goal (1 subgoal):
 1. G \<inter> H = {y}
[PROOF STEP]
have "G \<inter> H \<subseteq> {y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. G \<inter> H \<subseteq> {y}
[PROOF STEP]
proof (auto)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> G; x \<in> H\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> G; x \<in> H\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
assume a: "a \<in> G" "a \<in> H"
[PROOF STATE]
proof (state)
this:
a \<in> G
a \<in> H

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> G; x \<in> H\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
obtain s where s: "s \<in> {0..dist x y}" "a = g s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s. \<lbrakk>s \<in> {0..dist x y}; a = g s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using a g(4)
[PROOF STATE]
proof (prove)
using this:
a \<in> G
a \<in> H
G = g ` {0..dist x y}

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>s \<in> {0..dist x y}; a = g s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s \<in> {0..dist x y}
a = g s

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> G; x \<in> H\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
obtain t where t: "t \<in> {dist x y..dist x z}" "a = h t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t. \<lbrakk>t \<in> {dist x y..dist x z}; a = h t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using a h(4)
[PROOF STATE]
proof (prove)
using this:
a \<in> G
a \<in> H
H = h ` {dist x y..dist x z}

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>t \<in> {dist x y..dist x z}; a = h t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t \<in> {dist x y..dist x z}
a = h t

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> G; x \<in> H\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have "a = f s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = f s
[PROOF STEP]
using fg s
[PROOF STATE]
proof (prove)
using this:
?t \<le> dist x y \<Longrightarrow> f ?t = g ?t
s \<in> {0..dist x y}
a = g s

goal (1 subgoal):
 1. a = f s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a = f s

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> G; x \<in> H\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
a = f s

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> G; x \<in> H\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have "a = f t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = f t
[PROOF STEP]
using fh t
[PROOF STATE]
proof (prove)
using this:
dist x y \<le> ?t \<Longrightarrow> f ?t = h ?t
t \<in> {dist x y..dist x z}
a = h t

goal (1 subgoal):
 1. a = f t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a = f t

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> G; x \<in> H\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
a = f s
a = f t
[PROOF STEP]
have "s = t"
[PROOF STATE]
proof (prove)
using this:
a = f s
a = f t

goal (1 subgoal):
 1. s = t
[PROOF STEP]
using isometry_onD[OF \<open>isometry_on {0..dist x z} f\<close>, of s t] s(1) t(1)
[PROOF STATE]
proof (prove)
using this:
a = f s
a = f t
\<lbrakk>s \<in> {0..dist x z}; t \<in> {0..dist x z}\<rbrakk> \<Longrightarrow> dist (f s) (f t) = dist s t
s \<in> {0..dist x y}
t \<in> {dist x y..dist x z}

goal (1 subgoal):
 1. s = t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s = t

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> G; x \<in> H\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s = t
[PROOF STEP]
have "s = dist x y"
[PROOF STATE]
proof (prove)
using this:
s = t

goal (1 subgoal):
 1. s = dist x y
[PROOF STEP]
using s t
[PROOF STATE]
proof (prove)
using this:
s = t
s \<in> {0..dist x y}
a = g s
t \<in> {dist x y..dist x z}
a = h t

goal (1 subgoal):
 1. s = dist x y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s = dist x y

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> G; x \<in> H\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s = dist x y
[PROOF STEP]
show "a = y"
[PROOF STATE]
proof (prove)
using this:
s = dist x y

goal (1 subgoal):
 1. a = y
[PROOF STEP]
using s(2) g
[PROOF STATE]
proof (prove)
using this:
s = dist x y
a = g s
g 0 = x
g (dist x y) = y
isometry_on {0..dist x y} g
G = g ` {0..dist x y}

goal (1 subgoal):
 1. a = y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a = y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
G \<inter> H \<subseteq> {y}

goal (1 subgoal):
 1. G \<inter> H = {y}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
G \<inter> H \<subseteq> {y}
[PROOF STEP]
show "G \<inter> H = {y}"
[PROOF STATE]
proof (prove)
using this:
G \<inter> H \<subseteq> {y}

goal (1 subgoal):
 1. G \<inter> H = {y}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
G \<inter> H \<subseteq> {y}
dist x z = dist x y + dist y z
geodesic_segment_between G x y
geodesic_segment_between H y z

goal (1 subgoal):
 1. G \<inter> H = {y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
G \<inter> H = {y}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma geodesic_segment_dist_le:
  assumes "geodesic_segment_between G x y" "a \<in> G" "b \<in> G"
  shows "dist a b \<le> dist x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist a b \<le> dist x y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist a b \<le> dist x y
[PROOF STEP]
obtain g where g: "g 0 = x" "g (dist x y) = y" "isometry_on {0..dist x y} g" "G = g`{0..dist x y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g 0 = x; g (dist x y) = y; isometry_on {0..dist x y} g; G = g ` {0..dist x y}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson \<open>geodesic_segment_between G x y\<close> geodesic_segment_between_def)
[PROOF STATE]
proof (state)
this:
g 0 = x
g (dist x y) = y
isometry_on {0..dist x y} g
G = g ` {0..dist x y}

goal (1 subgoal):
 1. dist a b \<le> dist x y
[PROOF STEP]
obtain s t where st: "s \<in> {0..dist x y}" "t \<in> {0..dist x y}" "a = g s" "b = g t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s t. \<lbrakk>s \<in> {0..dist x y}; t \<in> {0..dist x y}; a = g s; b = g t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using g(4) assms
[PROOF STATE]
proof (prove)
using this:
G = g ` {0..dist x y}
geodesic_segment_between G x y
a \<in> G
b \<in> G

goal (1 subgoal):
 1. (\<And>s t. \<lbrakk>s \<in> {0..dist x y}; t \<in> {0..dist x y}; a = g s; b = g t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s \<in> {0..dist x y}
t \<in> {0..dist x y}
a = g s
b = g t

goal (1 subgoal):
 1. dist a b \<le> dist x y
[PROOF STEP]
have "dist a b = abs(s-t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist a b = \<bar>s - t\<bar>
[PROOF STEP]
using isometry_onD[OF g(3) st(1) st(2)]
[PROOF STATE]
proof (prove)
using this:
dist (g s) (g t) = dist s t

goal (1 subgoal):
 1. dist a b = \<bar>s - t\<bar>
[PROOF STEP]
unfolding st(3) st(4) dist_real_def
[PROOF STATE]
proof (prove)
using this:
dist (g s) (g t) = \<bar>s - t\<bar>

goal (1 subgoal):
 1. dist (g s) (g t) = \<bar>s - t\<bar>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dist a b = \<bar>s - t\<bar>

goal (1 subgoal):
 1. dist a b \<le> dist x y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dist a b = \<bar>s - t\<bar>
[PROOF STEP]
show "dist a b \<le> dist x y"
[PROOF STATE]
proof (prove)
using this:
dist a b = \<bar>s - t\<bar>

goal (1 subgoal):
 1. dist a b \<le> dist x y
[PROOF STEP]
using st(1) st(2)
[PROOF STATE]
proof (prove)
using this:
dist a b = \<bar>s - t\<bar>
s \<in> {0..dist x y}
t \<in> {0..dist x y}

goal (1 subgoal):
 1. dist a b \<le> dist x y
[PROOF STEP]
unfolding dist_real_def
[PROOF STATE]
proof (prove)
using this:
dist a b = \<bar>s - t\<bar>
s \<in> {0..dist x y}
t \<in> {0..dist x y}

goal (1 subgoal):
 1. dist a b \<le> dist x y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist a b \<le> dist x y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma geodesic_segment_param [simp]:
  assumes "geodesic_segment_between G x y"
  shows "geodesic_segment_param G x 0 = x"
        "geodesic_segment_param G x (dist x y) = y"
        "t \<in> {0..dist x y} \<Longrightarrow> geodesic_segment_param G x t \<in> G"
        "isometry_on {0..dist x y} (geodesic_segment_param G x)"
        "(geodesic_segment_param G x)`{0..dist x y} = G"
        "t \<in> {0..dist x y} \<Longrightarrow> dist x (geodesic_segment_param G x t) = t"
        "s \<in> {0..dist x y} \<Longrightarrow> t \<in> {0..dist x y} \<Longrightarrow> dist (geodesic_segment_param G x s) (geodesic_segment_param G x t) = abs(s-t)"
        "z \<in> G \<Longrightarrow> z = geodesic_segment_param G x (dist x z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((geodesic_segment_param G x 0 = x &&& geodesic_segment_param G x (dist x y) = y) &&& (t \<in> {0..dist x y} \<Longrightarrow> geodesic_segment_param G x t \<in> G) &&& isometry_on {0..dist x y} (geodesic_segment_param G x)) &&& (geodesic_segment_param G x ` {0..dist x y} = G &&& (t \<in> {0..dist x y} \<Longrightarrow> dist x (geodesic_segment_param G x t) = t)) &&& (\<lbrakk>s \<in> {0..dist x y}; t \<in> {0..dist x y}\<rbrakk> \<Longrightarrow> dist (geodesic_segment_param G x s) (geodesic_segment_param G x t) = \<bar>s - t\<bar>) &&& (z \<in> G \<Longrightarrow> z = geodesic_segment_param G x (dist x z))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. geodesic_segment_param G x 0 = x
 2. geodesic_segment_param G x (dist x y) = y
 3. t \<in> {0..dist x y} \<Longrightarrow> geodesic_segment_param G x t \<in> G
 4. isometry_on {0..dist x y} (geodesic_segment_param G x)
 5. geodesic_segment_param G x ` {0..dist x y} = G
 6. t \<in> {0..dist x y} \<Longrightarrow> dist x (geodesic_segment_param G x t) = t
 7. \<lbrakk>s \<in> {0..dist x y}; t \<in> {0..dist x y}\<rbrakk> \<Longrightarrow> dist (geodesic_segment_param G x s) (geodesic_segment_param G x t) = \<bar>s - t\<bar>
 8. z \<in> G \<Longrightarrow> z = geodesic_segment_param G x (dist x z)
[PROOF STEP]
obtain g::"real\<Rightarrow>'a" where g: "g 0 = x" "g (dist x y) = y" "isometry_on {0..dist x y} g" "G = g`{0..dist x y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g 0 = x; g (dist x y) = y; isometry_on {0..dist x y} g; G = g ` {0..dist x y}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson \<open>geodesic_segment_between G x y\<close> geodesic_segment_between_def)
[PROOF STATE]
proof (state)
this:
g 0 = x
g (dist x y) = y
isometry_on {0..dist x y} g
G = g ` {0..dist x y}

goal (8 subgoals):
 1. geodesic_segment_param G x 0 = x
 2. geodesic_segment_param G x (dist x y) = y
 3. t \<in> {0..dist x y} \<Longrightarrow> geodesic_segment_param G x t \<in> G
 4. isometry_on {0..dist x y} (geodesic_segment_param G x)
 5. geodesic_segment_param G x ` {0..dist x y} = G
 6. t \<in> {0..dist x y} \<Longrightarrow> dist x (geodesic_segment_param G x t) = t
 7. \<lbrakk>s \<in> {0..dist x y}; t \<in> {0..dist x y}\<rbrakk> \<Longrightarrow> dist (geodesic_segment_param G x s) (geodesic_segment_param G x t) = \<bar>s - t\<bar>
 8. z \<in> G \<Longrightarrow> z = geodesic_segment_param G x (dist x z)
[PROOF STEP]
have *: "g t \<in> G \<and> dist x (g t) = t" if "t \<in> {0..dist x y}" for t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g t \<in> G \<and> dist x (g t) = t
[PROOF STEP]
using isometry_onD[OF g(3), of 0 t] that g(1) g(4)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 \<in> {0..dist x y}; t \<in> {0..dist x y}\<rbrakk> \<Longrightarrow> dist (g 0) (g t) = dist 0 t
t \<in> {0..dist x y}
g 0 = x
G = g ` {0..dist x y}

goal (1 subgoal):
 1. g t \<in> G \<and> dist x (g t) = t
[PROOF STEP]
unfolding dist_real_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 \<in> {0..dist x y}; t \<in> {0..dist x y}\<rbrakk> \<Longrightarrow> dist (g 0) (g t) = \<bar>0 - t\<bar>
t \<in> {0..dist x y}
g 0 = x
G = g ` {0..dist x y}

goal (1 subgoal):
 1. g t \<in> G \<and> dist x (g t) = t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?t \<in> {0..dist x y} \<Longrightarrow> g ?t \<in> G \<and> dist x (g ?t) = ?t

goal (8 subgoals):
 1. geodesic_segment_param G x 0 = x
 2. geodesic_segment_param G x (dist x y) = y
 3. t \<in> {0..dist x y} \<Longrightarrow> geodesic_segment_param G x t \<in> G
 4. isometry_on {0..dist x y} (geodesic_segment_param G x)
 5. geodesic_segment_param G x ` {0..dist x y} = G
 6. t \<in> {0..dist x y} \<Longrightarrow> dist x (geodesic_segment_param G x t) = t
 7. \<lbrakk>s \<in> {0..dist x y}; t \<in> {0..dist x y}\<rbrakk> \<Longrightarrow> dist (geodesic_segment_param G x s) (geodesic_segment_param G x t) = \<bar>s - t\<bar>
 8. z \<in> G \<Longrightarrow> z = geodesic_segment_param G x (dist x z)
[PROOF STEP]
have G: "geodesic_segment_param G x t = g t" if "t \<in> {0..dist x y}" for t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_param G x t = g t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. geodesic_segment_param G x t = g t
[PROOF STEP]
have A: "geodesic_segment_param G x t \<in> G \<and> dist x (geodesic_segment_param G x t) = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_param G x t \<in> G \<and> dist x (geodesic_segment_param G x t) = t
[PROOF STEP]
using *[OF that]
[PROOF STATE]
proof (prove)
using this:
g t \<in> G \<and> dist x (g t) = t

goal (1 subgoal):
 1. geodesic_segment_param G x t \<in> G \<and> dist x (geodesic_segment_param G x t) = t
[PROOF STEP]
unfolding geodesic_segment_param_def
[PROOF STATE]
proof (prove)
using this:
g t \<in> G \<and> dist x (g t) = t

goal (1 subgoal):
 1. (if \<exists>w. w \<in> G \<and> dist x w = t then SOME w. w \<in> G \<and> dist x w = t else SOME w. w \<in> G) \<in> G \<and> dist x (if \<exists>w. w \<in> G \<and> dist x w = t then SOME w. w \<in> G \<and> dist x w = t else SOME w. w \<in> G) = t
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>w. \<lbrakk>g (dist x w) \<in> G; dist x (g (dist x w)) = dist x w; w \<in> G; t = dist x w\<rbrakk> \<Longrightarrow> (SOME wa. wa \<in> G \<and> dist x wa = dist x w) \<in> G
 2. \<And>w. \<lbrakk>g (dist x w) \<in> G; dist x (g (dist x w)) = dist x w; w \<in> G; t = dist x w\<rbrakk> \<Longrightarrow> dist x (SOME wa. wa \<in> G \<and> dist x wa = dist x w) = dist x w
[PROOF STEP]
using *[OF that]
[PROOF STATE]
proof (prove)
using this:
g t \<in> G \<and> dist x (g t) = t

goal (2 subgoals):
 1. \<And>w. \<lbrakk>g (dist x w) \<in> G; dist x (g (dist x w)) = dist x w; w \<in> G; t = dist x w\<rbrakk> \<Longrightarrow> (SOME wa. wa \<in> G \<and> dist x wa = dist x w) \<in> G
 2. \<And>w. \<lbrakk>g (dist x w) \<in> G; dist x (g (dist x w)) = dist x w; w \<in> G; t = dist x w\<rbrakk> \<Longrightarrow> dist x (SOME wa. wa \<in> G \<and> dist x wa = dist x w) = dist x w
[PROOF STEP]
by (metis (mono_tags, lifting) someI)+
[PROOF STATE]
proof (state)
this:
geodesic_segment_param G x t \<in> G \<and> dist x (geodesic_segment_param G x t) = t

goal (1 subgoal):
 1. geodesic_segment_param G x t = g t
[PROOF STEP]
obtain s where s: "geodesic_segment_param G x t = g s" "s \<in> {0..dist x y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s. \<lbrakk>geodesic_segment_param G x t = g s; s \<in> {0..dist x y}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using A g(4)
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_param G x t \<in> G \<and> dist x (geodesic_segment_param G x t) = t
G = g ` {0..dist x y}

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>geodesic_segment_param G x t = g s; s \<in> {0..dist x y}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
geodesic_segment_param G x t = g s
s \<in> {0..dist x y}

goal (1 subgoal):
 1. geodesic_segment_param G x t = g t
[PROOF STEP]
have "s = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s = t
[PROOF STEP]
using *[OF \<open>s \<in> {0..dist x y}\<close>] A
[PROOF STATE]
proof (prove)
using this:
g s \<in> G \<and> dist x (g s) = s
geodesic_segment_param G x t \<in> G \<and> dist x (geodesic_segment_param G x t) = t

goal (1 subgoal):
 1. s = t
[PROOF STEP]
unfolding s(1)
[PROOF STATE]
proof (prove)
using this:
g s \<in> G \<and> dist x (g s) = s
g s \<in> G \<and> dist x (g s) = t

goal (1 subgoal):
 1. s = t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s = t

goal (1 subgoal):
 1. geodesic_segment_param G x t = g t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s = t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s = t

goal (1 subgoal):
 1. geodesic_segment_param G x t = g t
[PROOF STEP]
using s
[PROOF STATE]
proof (prove)
using this:
s = t
geodesic_segment_param G x t = g s
s \<in> {0..dist x y}

goal (1 subgoal):
 1. geodesic_segment_param G x t = g t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
geodesic_segment_param G x t = g t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?t \<in> {0..dist x y} \<Longrightarrow> geodesic_segment_param G x ?t = g ?t

goal (8 subgoals):
 1. geodesic_segment_param G x 0 = x
 2. geodesic_segment_param G x (dist x y) = y
 3. t \<in> {0..dist x y} \<Longrightarrow> geodesic_segment_param G x t \<in> G
 4. isometry_on {0..dist x y} (geodesic_segment_param G x)
 5. geodesic_segment_param G x ` {0..dist x y} = G
 6. t \<in> {0..dist x y} \<Longrightarrow> dist x (geodesic_segment_param G x t) = t
 7. \<lbrakk>s \<in> {0..dist x y}; t \<in> {0..dist x y}\<rbrakk> \<Longrightarrow> dist (geodesic_segment_param G x s) (geodesic_segment_param G x t) = \<bar>s - t\<bar>
 8. z \<in> G \<Longrightarrow> z = geodesic_segment_param G x (dist x z)
[PROOF STEP]
show "geodesic_segment_param G x 0 = x"
       "geodesic_segment_param G x (dist x y) = y"
       "t \<in> {0..dist x y} \<Longrightarrow> geodesic_segment_param G x t \<in> G"
       "isometry_on {0..dist x y} (geodesic_segment_param G x)"
       "(geodesic_segment_param G x)`{0..dist x y} = G"
       "t \<in> {0..dist x y} \<Longrightarrow> dist x (geodesic_segment_param G x t) = t"
       "s \<in> {0..dist x y} \<Longrightarrow> t \<in> {0..dist x y} \<Longrightarrow> dist (geodesic_segment_param G x s) (geodesic_segment_param G x t) = abs(s-t)"
       "z \<in> G \<Longrightarrow> z = geodesic_segment_param G x (dist x z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((geodesic_segment_param G x 0 = x &&& geodesic_segment_param G x (dist x y) = y) &&& (t \<in> {0..dist x y} \<Longrightarrow> geodesic_segment_param G x t \<in> G) &&& isometry_on {0..dist x y} (geodesic_segment_param G x)) &&& (geodesic_segment_param G x ` {0..dist x y} = G &&& (t \<in> {0..dist x y} \<Longrightarrow> dist x (geodesic_segment_param G x t) = t)) &&& (\<lbrakk>s \<in> {0..dist x y}; t \<in> {0..dist x y}\<rbrakk> \<Longrightarrow> dist (geodesic_segment_param G x s) (geodesic_segment_param G x t) = \<bar>s - t\<bar>) &&& (z \<in> G \<Longrightarrow> z = geodesic_segment_param G x (dist x z))
[PROOF STEP]
using G g
[PROOF STATE]
proof (prove)
using this:
?t \<in> {0..dist x y} \<Longrightarrow> geodesic_segment_param G x ?t = g ?t
g 0 = x
g (dist x y) = y
isometry_on {0..dist x y} g
G = g ` {0..dist x y}

goal (1 subgoal):
 1. ((geodesic_segment_param G x 0 = x &&& geodesic_segment_param G x (dist x y) = y) &&& (t \<in> {0..dist x y} \<Longrightarrow> geodesic_segment_param G x t \<in> G) &&& isometry_on {0..dist x y} (geodesic_segment_param G x)) &&& (geodesic_segment_param G x ` {0..dist x y} = G &&& (t \<in> {0..dist x y} \<Longrightarrow> dist x (geodesic_segment_param G x t) = t)) &&& (\<lbrakk>s \<in> {0..dist x y}; t \<in> {0..dist x y}\<rbrakk> \<Longrightarrow> dist (geodesic_segment_param G x s) (geodesic_segment_param G x t) = \<bar>s - t\<bar>) &&& (z \<in> G \<Longrightarrow> z = geodesic_segment_param G x (dist x z))
[PROOF STEP]
apply (auto simp add: rev_image_eqI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>\<And>t. 0 \<le> t \<and> t \<le> dist (g 0) y \<Longrightarrow> geodesic_segment_param (g ` {0..dist (g 0) y}) (g 0) t = g t; g (dist (g 0) y) = y; isometry_on {0..dist (g 0) y} g; G = g ` {0..dist (g 0) y}; x = g 0\<rbrakk> \<Longrightarrow> isometry_on {0..dist (g 0) y} (geodesic_segment_param (g ` {0..dist (g 0) y}) (g 0))
 2. \<lbrakk>\<And>t. 0 \<le> t \<and> t \<le> dist (g 0) y \<Longrightarrow> geodesic_segment_param (g ` {0..dist (g 0) y}) (g 0) t = g t; g (dist (g 0) y) = y; isometry_on {0..dist (g 0) y} g; G = g ` {0..dist (g 0) y}; x = g 0; 0 \<le> t; t \<le> dist (g 0) y\<rbrakk> \<Longrightarrow> dist (g 0) (g t) = t
 3. \<lbrakk>\<And>t. 0 \<le> t \<and> t \<le> dist (g 0) y \<Longrightarrow> geodesic_segment_param (g ` {0..dist (g 0) y}) (g 0) t = g t; g (dist (g 0) y) = y; isometry_on {0..dist (g 0) y} g; G = g ` {0..dist (g 0) y}; x = g 0; 0 \<le> s; s \<le> dist (g 0) y; 0 \<le> t; t \<le> dist (g 0) y\<rbrakk> \<Longrightarrow> dist (g s) (g t) = \<bar>s - t\<bar>
 4. \<And>xa. \<lbrakk>\<And>t. 0 \<le> t \<and> t \<le> dist (g 0) y \<Longrightarrow> geodesic_segment_param (g ` {0..dist (g 0) y}) (g 0) t = g t; g (dist (g 0) y) = y; isometry_on {0..dist (g 0) y} g; G = g ` {0..dist (g 0) y}; x = g 0; z = g xa; 0 \<le> xa; xa \<le> dist (g 0) y\<rbrakk> \<Longrightarrow> g xa = geodesic_segment_param (g ` {0..dist (g 0) y}) (g 0) (dist (g 0) (g xa))
[PROOF STEP]
using G isometry_on_cong * atLeastAtMost_iff
[PROOF STATE]
proof (prove)
using this:
?t \<in> {0..dist x y} \<Longrightarrow> geodesic_segment_param G x ?t = g ?t
\<lbrakk>isometry_on ?X ?f; \<And>x. x \<in> ?X \<Longrightarrow> ?g x = ?f x\<rbrakk> \<Longrightarrow> isometry_on ?X ?g
?t \<in> {0..dist x y} \<Longrightarrow> g ?t \<in> G \<and> dist x (g ?t) = ?t
(?i \<in> {?l..?u}) = (?l \<le> ?i \<and> ?i \<le> ?u)

goal (4 subgoals):
 1. \<lbrakk>\<And>t. 0 \<le> t \<and> t \<le> dist (g 0) y \<Longrightarrow> geodesic_segment_param (g ` {0..dist (g 0) y}) (g 0) t = g t; g (dist (g 0) y) = y; isometry_on {0..dist (g 0) y} g; G = g ` {0..dist (g 0) y}; x = g 0\<rbrakk> \<Longrightarrow> isometry_on {0..dist (g 0) y} (geodesic_segment_param (g ` {0..dist (g 0) y}) (g 0))
 2. \<lbrakk>\<And>t. 0 \<le> t \<and> t \<le> dist (g 0) y \<Longrightarrow> geodesic_segment_param (g ` {0..dist (g 0) y}) (g 0) t = g t; g (dist (g 0) y) = y; isometry_on {0..dist (g 0) y} g; G = g ` {0..dist (g 0) y}; x = g 0; 0 \<le> t; t \<le> dist (g 0) y\<rbrakk> \<Longrightarrow> dist (g 0) (g t) = t
 3. \<lbrakk>\<And>t. 0 \<le> t \<and> t \<le> dist (g 0) y \<Longrightarrow> geodesic_segment_param (g ` {0..dist (g 0) y}) (g 0) t = g t; g (dist (g 0) y) = y; isometry_on {0..dist (g 0) y} g; G = g ` {0..dist (g 0) y}; x = g 0; 0 \<le> s; s \<le> dist (g 0) y; 0 \<le> t; t \<le> dist (g 0) y\<rbrakk> \<Longrightarrow> dist (g s) (g t) = \<bar>s - t\<bar>
 4. \<And>xa. \<lbrakk>\<And>t. 0 \<le> t \<and> t \<le> dist (g 0) y \<Longrightarrow> geodesic_segment_param (g ` {0..dist (g 0) y}) (g 0) t = g t; g (dist (g 0) y) = y; isometry_on {0..dist (g 0) y} g; G = g ` {0..dist (g 0) y}; x = g 0; z = g xa; 0 \<le> xa; xa \<le> dist (g 0) y\<rbrakk> \<Longrightarrow> g xa = geodesic_segment_param (g ` {0..dist (g 0) y}) (g 0) (dist (g 0) (g xa))
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<And>t. 0 \<le> t \<and> t \<le> dist (g 0) y \<Longrightarrow> geodesic_segment_param (g ` {0..dist (g 0) y}) (g 0) t = g t; g (dist (g 0) y) = y; isometry_on {0..dist (g 0) y} g; G = g ` {0..dist (g 0) y}; x = g 0; 0 \<le> t; t \<le> dist (g 0) y\<rbrakk> \<Longrightarrow> dist (g 0) (g t) = t
 2. \<lbrakk>\<And>t. 0 \<le> t \<and> t \<le> dist (g 0) y \<Longrightarrow> geodesic_segment_param (g ` {0..dist (g 0) y}) (g 0) t = g t; g (dist (g 0) y) = y; isometry_on {0..dist (g 0) y} g; G = g ` {0..dist (g 0) y}; x = g 0; 0 \<le> s; s \<le> dist (g 0) y; 0 \<le> t; t \<le> dist (g 0) y\<rbrakk> \<Longrightarrow> dist (g s) (g t) = \<bar>s - t\<bar>
 3. \<And>xa. \<lbrakk>\<And>t. 0 \<le> t \<and> t \<le> dist (g 0) y \<Longrightarrow> geodesic_segment_param (g ` {0..dist (g 0) y}) (g 0) t = g t; g (dist (g 0) y) = y; isometry_on {0..dist (g 0) y} g; G = g ` {0..dist (g 0) y}; x = g 0; z = g xa; 0 \<le> xa; xa \<le> dist (g 0) y\<rbrakk> \<Longrightarrow> g xa = geodesic_segment_param (g ` {0..dist (g 0) y}) (g 0) (dist (g 0) (g xa))
[PROOF STEP]
using G isometry_on_cong * atLeastAtMost_iff
[PROOF STATE]
proof (prove)
using this:
?t \<in> {0..dist x y} \<Longrightarrow> geodesic_segment_param G x ?t = g ?t
\<lbrakk>isometry_on ?X ?f; \<And>x. x \<in> ?X \<Longrightarrow> ?g x = ?f x\<rbrakk> \<Longrightarrow> isometry_on ?X ?g
?t \<in> {0..dist x y} \<Longrightarrow> g ?t \<in> G \<and> dist x (g ?t) = ?t
(?i \<in> {?l..?u}) = (?l \<le> ?i \<and> ?i \<le> ?u)

goal (3 subgoals):
 1. \<lbrakk>\<And>t. 0 \<le> t \<and> t \<le> dist (g 0) y \<Longrightarrow> geodesic_segment_param (g ` {0..dist (g 0) y}) (g 0) t = g t; g (dist (g 0) y) = y; isometry_on {0..dist (g 0) y} g; G = g ` {0..dist (g 0) y}; x = g 0; 0 \<le> t; t \<le> dist (g 0) y\<rbrakk> \<Longrightarrow> dist (g 0) (g t) = t
 2. \<lbrakk>\<And>t. 0 \<le> t \<and> t \<le> dist (g 0) y \<Longrightarrow> geodesic_segment_param (g ` {0..dist (g 0) y}) (g 0) t = g t; g (dist (g 0) y) = y; isometry_on {0..dist (g 0) y} g; G = g ` {0..dist (g 0) y}; x = g 0; 0 \<le> s; s \<le> dist (g 0) y; 0 \<le> t; t \<le> dist (g 0) y\<rbrakk> \<Longrightarrow> dist (g s) (g t) = \<bar>s - t\<bar>
 3. \<And>xa. \<lbrakk>\<And>t. 0 \<le> t \<and> t \<le> dist (g 0) y \<Longrightarrow> geodesic_segment_param (g ` {0..dist (g 0) y}) (g 0) t = g t; g (dist (g 0) y) = y; isometry_on {0..dist (g 0) y} g; G = g ` {0..dist (g 0) y}; x = g 0; z = g xa; 0 \<le> xa; xa \<le> dist (g 0) y\<rbrakk> \<Longrightarrow> g xa = geodesic_segment_param (g ` {0..dist (g 0) y}) (g 0) (dist (g 0) (g xa))
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>t. 0 \<le> t \<and> t \<le> dist (g 0) y \<Longrightarrow> geodesic_segment_param (g ` {0..dist (g 0) y}) (g 0) t = g t; g (dist (g 0) y) = y; isometry_on {0..dist (g 0) y} g; G = g ` {0..dist (g 0) y}; x = g 0; 0 \<le> s; s \<le> dist (g 0) y; 0 \<le> t; t \<le> dist (g 0) y\<rbrakk> \<Longrightarrow> dist (g s) (g t) = \<bar>s - t\<bar>
 2. \<And>xa. \<lbrakk>\<And>t. 0 \<le> t \<and> t \<le> dist (g 0) y \<Longrightarrow> geodesic_segment_param (g ` {0..dist (g 0) y}) (g 0) t = g t; g (dist (g 0) y) = y; isometry_on {0..dist (g 0) y} g; G = g ` {0..dist (g 0) y}; x = g 0; z = g xa; 0 \<le> xa; xa \<le> dist (g 0) y\<rbrakk> \<Longrightarrow> g xa = geodesic_segment_param (g ` {0..dist (g 0) y}) (g 0) (dist (g 0) (g xa))
[PROOF STEP]
by (auto simp add: * dist_real_def isometry_onD)
[PROOF STATE]
proof (state)
this:
geodesic_segment_param G x 0 = x
geodesic_segment_param G x (dist x y) = y
t \<in> {0..dist x y} \<Longrightarrow> geodesic_segment_param G x t \<in> G
isometry_on {0..dist x y} (geodesic_segment_param G x)
geodesic_segment_param G x ` {0..dist x y} = G
t \<in> {0..dist x y} \<Longrightarrow> dist x (geodesic_segment_param G x t) = t
\<lbrakk>s \<in> {0..dist x y}; t \<in> {0..dist x y}\<rbrakk> \<Longrightarrow> dist (geodesic_segment_param G x s) (geodesic_segment_param G x t) = \<bar>s - t\<bar>
z \<in> G \<Longrightarrow> z = geodesic_segment_param G x (dist x z)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma geodesic_segment_param_in_segment:
  assumes "G \<noteq> {}"
  shows "geodesic_segment_param G x t \<in> G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_param G x t \<in> G
[PROOF STEP]
unfolding geodesic_segment_param_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if \<exists>w. w \<in> G \<and> dist x w = t then SOME w. w \<in> G \<and> dist x w = t else SOME w. w \<in> G) \<in> G
[PROOF STEP]
apply (auto, metis (mono_tags, lifting) someI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w. w \<in> G \<longrightarrow> dist x w \<noteq> t \<Longrightarrow> (SOME w. w \<in> G) \<in> G
[PROOF STEP]
using assms some_in_eq
[PROOF STATE]
proof (prove)
using this:
G \<noteq> {}
((SOME x. x \<in> ?A) \<in> ?A) = (?A \<noteq> {})

goal (1 subgoal):
 1. \<forall>w. w \<in> G \<longrightarrow> dist x w \<noteq> t \<Longrightarrow> (SOME w. w \<in> G) \<in> G
[PROOF STEP]
by fastforce


[STATEMENT]
lemma geodesic_segment_reverse_param:
  assumes "geodesic_segment_between G x y"
          "t \<in> {0..dist x y}"
  shows "geodesic_segment_param G y (dist x y - t) = geodesic_segment_param G x t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_param G y (dist x y - t) = geodesic_segment_param G x t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. geodesic_segment_param G y (dist x y - t) = geodesic_segment_param G x t
[PROOF STEP]
have * [simp]: "geodesic_segment_between G y x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_between G y x
[PROOF STEP]
using geodesic_segment_commute[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_between G y x

goal (1 subgoal):
 1. geodesic_segment_between G y x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
geodesic_segment_between G y x

goal (1 subgoal):
 1. geodesic_segment_param G y (dist x y - t) = geodesic_segment_param G x t
[PROOF STEP]
have "geodesic_segment_param G y (dist x y - t) \<in> G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_param G y (dist x y - t) \<in> G
[PROOF STEP]
apply (rule geodesic_segment_param(3)[of _ _ x])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. geodesic_segment_between G y x
 2. dist x y - t \<in> {0..dist y x}
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
t \<in> {0..dist x y}

goal (2 subgoals):
 1. geodesic_segment_between G y x
 2. dist x y - t \<in> {0..dist y x}
[PROOF STEP]
by (auto simp add: dist_commute)
[PROOF STATE]
proof (state)
this:
geodesic_segment_param G y (dist x y - t) \<in> G

goal (1 subgoal):
 1. geodesic_segment_param G y (dist x y - t) = geodesic_segment_param G x t
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
geodesic_segment_param G y (dist x y - t) \<in> G

goal (1 subgoal):
 1. geodesic_segment_param G y (dist x y - t) = geodesic_segment_param G x t
[PROOF STEP]
have "dist (geodesic_segment_param G y (dist x y - t)) x = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (geodesic_segment_param G y (dist x y - t)) x = t
[PROOF STEP]
using geodesic_segment_param(2)[OF *] geodesic_segment_param(7)[OF *, of "dist x y -t" "dist x y"] assms(2)
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_param G y (dist y x) = x
\<lbrakk>dist x y - t \<in> {0..dist y x}; dist x y \<in> {0..dist y x}\<rbrakk> \<Longrightarrow> dist (geodesic_segment_param G y (dist x y - t)) (geodesic_segment_param G y (dist x y)) = \<bar>dist x y - t - dist x y\<bar>
t \<in> {0..dist x y}

goal (1 subgoal):
 1. dist (geodesic_segment_param G y (dist x y - t)) x = t
[PROOF STEP]
by (auto simp add: dist_commute)
[PROOF STATE]
proof (state)
this:
dist (geodesic_segment_param G y (dist x y - t)) x = t

goal (1 subgoal):
 1. geodesic_segment_param G y (dist x y - t) = geodesic_segment_param G x t
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
dist (geodesic_segment_param G y (dist x y - t)) x = t

goal (1 subgoal):
 1. geodesic_segment_param G y (dist x y - t) = geodesic_segment_param G x t
[PROOF STEP]
have "geodesic_segment_param G x t \<in> G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_param G x t \<in> G
[PROOF STEP]
apply (rule geodesic_segment_param(3)[OF assms(1)])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> {0..dist x y}
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
t \<in> {0..dist x y}

goal (1 subgoal):
 1. t \<in> {0..dist x y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
geodesic_segment_param G x t \<in> G

goal (1 subgoal):
 1. geodesic_segment_param G y (dist x y - t) = geodesic_segment_param G x t
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
geodesic_segment_param G x t \<in> G

goal (1 subgoal):
 1. geodesic_segment_param G y (dist x y - t) = geodesic_segment_param G x t
[PROOF STEP]
have "dist (geodesic_segment_param G x t) x = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (geodesic_segment_param G x t) x = t
[PROOF STEP]
using geodesic_segment_param(6)[OF assms]
[PROOF STATE]
proof (prove)
using this:
dist x (geodesic_segment_param G x t) = t

goal (1 subgoal):
 1. dist (geodesic_segment_param G x t) x = t
[PROOF STEP]
by (simp add: dist_commute)
[PROOF STATE]
proof (state)
this:
dist (geodesic_segment_param G x t) x = t

goal (1 subgoal):
 1. geodesic_segment_param G y (dist x y - t) = geodesic_segment_param G x t
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
geodesic_segment_param G y (dist x y - t) \<in> G
dist (geodesic_segment_param G y (dist x y - t)) x = t
geodesic_segment_param G x t \<in> G
dist (geodesic_segment_param G x t) x = t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_param G y (dist x y - t) \<in> G
dist (geodesic_segment_param G y (dist x y - t)) x = t
geodesic_segment_param G x t \<in> G
dist (geodesic_segment_param G x t) x = t

goal (1 subgoal):
 1. geodesic_segment_param G y (dist x y - t) = geodesic_segment_param G x t
[PROOF STEP]
using geodesic_segment_dist_unique[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_param G y (dist x y - t) \<in> G
dist (geodesic_segment_param G y (dist x y - t)) x = t
geodesic_segment_param G x t \<in> G
dist (geodesic_segment_param G x t) x = t
\<lbrakk>?a \<in> G; ?b \<in> G; dist x ?a = dist x ?b\<rbrakk> \<Longrightarrow> ?a = ?b

goal (1 subgoal):
 1. geodesic_segment_param G y (dist x y - t) = geodesic_segment_param G x t
[PROOF STEP]
by (simp add: dist_commute)
[PROOF STATE]
proof (state)
this:
geodesic_segment_param G y (dist x y - t) = geodesic_segment_param G x t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dist_along_geodesic_wrt_endpoint:
  assumes "geodesic_segment_between G x y"
          "u \<in> G" "v \<in> G"
  shows "dist u v = abs(dist u x - dist v x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist u v = \<bar>dist u x - dist v x\<bar>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist u v = \<bar>dist u x - dist v x\<bar>
[PROOF STEP]
have *: "u = geodesic_segment_param G x (dist x u)" "v = geodesic_segment_param G x (dist x v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u = geodesic_segment_param G x (dist x u) &&& v = geodesic_segment_param G x (dist x v)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_between G x y
u \<in> G
v \<in> G

goal (1 subgoal):
 1. u = geodesic_segment_param G x (dist x u) &&& v = geodesic_segment_param G x (dist x v)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u = geodesic_segment_param G x (dist x u)
v = geodesic_segment_param G x (dist x v)

goal (1 subgoal):
 1. dist u v = \<bar>dist u x - dist v x\<bar>
[PROOF STEP]
have "dist u v = dist (geodesic_segment_param G x (dist x u)) (geodesic_segment_param G x (dist x v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist u v = dist (geodesic_segment_param G x (dist x u)) (geodesic_segment_param G x (dist x v))
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
u = geodesic_segment_param G x (dist x u)
v = geodesic_segment_param G x (dist x v)

goal (1 subgoal):
 1. dist u v = dist (geodesic_segment_param G x (dist x u)) (geodesic_segment_param G x (dist x v))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist u v = dist (geodesic_segment_param G x (dist x u)) (geodesic_segment_param G x (dist x v))

goal (1 subgoal):
 1. dist u v = \<bar>dist u x - dist v x\<bar>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist u v = dist (geodesic_segment_param G x (dist x u)) (geodesic_segment_param G x (dist x v))

goal (1 subgoal):
 1. dist u v = \<bar>dist u x - dist v x\<bar>
[PROOF STEP]
have "... = abs(dist x u - dist x v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (geodesic_segment_param G x (dist x u)) (geodesic_segment_param G x (dist x v)) = \<bar>dist x u - dist x v\<bar>
[PROOF STEP]
apply (rule geodesic_segment_param(7)[OF assms(1)])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. dist x u \<in> {0..dist x y}
 2. dist x v \<in> {0..dist x y}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_between G x y
u \<in> G
v \<in> G

goal (2 subgoals):
 1. dist x u \<in> {0..dist x y}
 2. dist x v \<in> {0..dist x y}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>geodesic_segment_between G x y; u \<in> G; v \<in> G\<rbrakk> \<Longrightarrow> dist x u \<le> dist x y
 2. \<lbrakk>geodesic_segment_between G x y; u \<in> G; v \<in> G\<rbrakk> \<Longrightarrow> dist x v \<le> dist x y
[PROOF STEP]
using geodesic_segment_dist_le geodesic_segment_endpoints(1)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>geodesic_segment_between ?G ?x ?y; ?a \<in> ?G; ?b \<in> ?G\<rbrakk> \<Longrightarrow> dist ?a ?b \<le> dist ?x ?y
geodesic_segment_between ?G ?x ?y \<Longrightarrow> ?x \<in> ?G

goal (2 subgoals):
 1. \<lbrakk>geodesic_segment_between G x y; u \<in> G; v \<in> G\<rbrakk> \<Longrightarrow> dist x u \<le> dist x y
 2. \<lbrakk>geodesic_segment_between G x y; u \<in> G; v \<in> G\<rbrakk> \<Longrightarrow> dist x v \<le> dist x y
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
dist (geodesic_segment_param G x (dist x u)) (geodesic_segment_param G x (dist x v)) = \<bar>dist x u - dist x v\<bar>

goal (1 subgoal):
 1. dist u v = \<bar>dist u x - dist v x\<bar>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist u v = \<bar>dist x u - dist x v\<bar>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dist u v = \<bar>dist x u - dist x v\<bar>

goal (1 subgoal):
 1. dist u v = \<bar>dist u x - dist v x\<bar>
[PROOF STEP]
by (simp add: dist_commute)
[PROOF STATE]
proof (state)
this:
dist u v = \<bar>dist u x - dist v x\<bar>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma geodesic_subsegment_subset:
  "geodesic_subsegment G x s t \<subseteq> G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_subsegment G x s t \<subseteq> G
[PROOF STEP]
unfolding geodesic_subsegment_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. G \<inter> {z. s \<le> dist x z \<and> dist x z \<le> t} \<subseteq> G
[PROOF STEP]
by simp