[STATEMENT]
lemma geodesic_subsegment:
  assumes "geodesic_segment_between G x y"
          "0 \<le> s" "s \<le> t" "t \<le> dist x y"
  shows "geodesic_subsegment G x s t = (geodesic_segment_param G x)`{s..t}"
        "geodesic_segment_between (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (geodesic_segment_param G x t)"
        "\<And>u. s \<le> u \<Longrightarrow> u \<le> t \<Longrightarrow> geodesic_segment_param (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (u - s) = geodesic_segment_param G x u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_subsegment G x s t = geodesic_segment_param G x ` {s..t} &&& geodesic_segment_between (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (geodesic_segment_param G x t) &&& (\<And>u. \<lbrakk>s \<le> u; u \<le> t\<rbrakk> \<Longrightarrow> geodesic_segment_param (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (u - s) = geodesic_segment_param G x u)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. geodesic_subsegment G x s t = geodesic_segment_param G x ` {s..t}
 2. geodesic_segment_between (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (geodesic_segment_param G x t)
 3. \<And>u. \<lbrakk>s \<le> u; u \<le> t\<rbrakk> \<Longrightarrow> geodesic_segment_param (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (u - s) = geodesic_segment_param G x u
[PROOF STEP]
show A: "geodesic_subsegment G x s t = (geodesic_segment_param G x)`{s..t}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_subsegment G x s t = geodesic_segment_param G x ` {s..t}
[PROOF STEP]
proof (auto)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xa. xa \<in> geodesic_subsegment G x s t \<Longrightarrow> xa \<in> geodesic_segment_param G x ` {s..t}
 2. \<And>xa. \<lbrakk>s \<le> xa; xa \<le> t\<rbrakk> \<Longrightarrow> geodesic_segment_param G x xa \<in> geodesic_subsegment G x s t
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xa. xa \<in> geodesic_subsegment G x s t \<Longrightarrow> xa \<in> geodesic_segment_param G x ` {s..t}
 2. \<And>xa. \<lbrakk>s \<le> xa; xa \<le> t\<rbrakk> \<Longrightarrow> geodesic_segment_param G x xa \<in> geodesic_subsegment G x s t
[PROOF STEP]
assume y: "y \<in> geodesic_subsegment G x s t"
[PROOF STATE]
proof (state)
this:
y \<in> geodesic_subsegment G x s t

goal (2 subgoals):
 1. \<And>xa. xa \<in> geodesic_subsegment G x s t \<Longrightarrow> xa \<in> geodesic_segment_param G x ` {s..t}
 2. \<And>xa. \<lbrakk>s \<le> xa; xa \<le> t\<rbrakk> \<Longrightarrow> geodesic_segment_param G x xa \<in> geodesic_subsegment G x s t
[PROOF STEP]
have "y = geodesic_segment_param G x (dist x y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y = geodesic_segment_param G x (dist x y)
[PROOF STEP]
apply (rule geodesic_segment_param(8)[OF assms(1)])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> G
[PROOF STEP]
using y geodesic_subsegment_subset
[PROOF STATE]
proof (prove)
using this:
y \<in> geodesic_subsegment G x s t
geodesic_subsegment ?G ?x ?s ?t \<subseteq> ?G

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

goal (2 subgoals):
 1. \<And>xa. xa \<in> geodesic_subsegment G x s t \<Longrightarrow> xa \<in> geodesic_segment_param G x ` {s..t}
 2. \<And>xa. \<lbrakk>s \<le> xa; xa \<le> t\<rbrakk> \<Longrightarrow> geodesic_segment_param G x xa \<in> geodesic_subsegment G x s t
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
y = geodesic_segment_param G x (dist x y)

goal (2 subgoals):
 1. \<And>xa. xa \<in> geodesic_subsegment G x s t \<Longrightarrow> xa \<in> geodesic_segment_param G x ` {s..t}
 2. \<And>xa. \<lbrakk>s \<le> xa; xa \<le> t\<rbrakk> \<Longrightarrow> geodesic_segment_param G x xa \<in> geodesic_subsegment G x s t
[PROOF STEP]
have "dist x y \<ge> s \<and> dist x y \<le> t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<le> dist x y \<and> dist x y \<le> t
[PROOF STEP]
using y
[PROOF STATE]
proof (prove)
using this:
y \<in> geodesic_subsegment G x s t

goal (1 subgoal):
 1. s \<le> dist x y \<and> dist x y \<le> t
[PROOF STEP]
unfolding geodesic_subsegment_def
[PROOF STATE]
proof (prove)
using this:
y \<in> G \<inter> {z. s \<le> dist x z \<and> dist x z \<le> t}

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

goal (2 subgoals):
 1. \<And>xa. xa \<in> geodesic_subsegment G x s t \<Longrightarrow> xa \<in> geodesic_segment_param G x ` {s..t}
 2. \<And>xa. \<lbrakk>s \<le> xa; xa \<le> t\<rbrakk> \<Longrightarrow> geodesic_segment_param G x xa \<in> geodesic_subsegment G x s t
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
y = geodesic_segment_param G x (dist x y)
s \<le> dist x y \<and> dist x y \<le> t
[PROOF STEP]
show "y \<in> geodesic_segment_param G x ` {s..t}"
[PROOF STATE]
proof (prove)
using this:
y = geodesic_segment_param G x (dist x y)
s \<le> dist x y \<and> dist x y \<le> t

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

goal (1 subgoal):
 1. \<And>xa. \<lbrakk>s \<le> xa; xa \<le> t\<rbrakk> \<Longrightarrow> geodesic_segment_param G x xa \<in> geodesic_subsegment G x s t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>s \<le> xa; xa \<le> t\<rbrakk> \<Longrightarrow> geodesic_segment_param G x xa \<in> geodesic_subsegment G x s t
[PROOF STEP]
fix u
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>s \<le> xa; xa \<le> t\<rbrakk> \<Longrightarrow> geodesic_segment_param G x xa \<in> geodesic_subsegment G x s t
[PROOF STEP]
assume H: "s \<le> u" "u \<le> t"
[PROOF STATE]
proof (state)
this:
s \<le> u
u \<le> t

goal (1 subgoal):
 1. \<And>xa. \<lbrakk>s \<le> xa; xa \<le> t\<rbrakk> \<Longrightarrow> geodesic_segment_param G x xa \<in> geodesic_subsegment G x s t
[PROOF STEP]
have *: "dist x (geodesic_segment_param G x u) = u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist x (geodesic_segment_param G x u) = u
[PROOF STEP]
apply (rule geodesic_segment_param(6)[OF assms(1)])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<in> {0..dist x y}
[PROOF STEP]
using H assms
[PROOF STATE]
proof (prove)
using this:
s \<le> u
u \<le> t
geodesic_segment_between G x y
0 \<le> s
s \<le> t
t \<le> dist x y

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

goal (1 subgoal):
 1. \<And>xa. \<lbrakk>s \<le> xa; xa \<le> t\<rbrakk> \<Longrightarrow> geodesic_segment_param G x xa \<in> geodesic_subsegment G x s t
[PROOF STEP]
show "geodesic_segment_param G x u \<in> geodesic_subsegment G x s t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_param G x u \<in> geodesic_subsegment G x s t
[PROOF STEP]
unfolding geodesic_subsegment_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_param G x u \<in> G \<inter> {z. s \<le> dist x z \<and> dist x z \<le> t}
[PROOF STEP]
using geodesic_segment_param_in_segment[OF geodesic_segment_endpoints(3)[OF assms(1)]]
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_param G ?x ?t \<in> G

goal (1 subgoal):
 1. geodesic_segment_param G x u \<in> G \<inter> {z. s \<le> dist x z \<and> dist x z \<le> t}
[PROOF STEP]
by (auto simp add: * H)
[PROOF STATE]
proof (state)
this:
geodesic_segment_param G x u \<in> geodesic_subsegment G x s t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
geodesic_subsegment G x s t = geodesic_segment_param G x ` {s..t}

goal (2 subgoals):
 1. geodesic_segment_between (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (geodesic_segment_param G x t)
 2. \<And>u. \<lbrakk>s \<le> u; u \<le> t\<rbrakk> \<Longrightarrow> geodesic_segment_param (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (u - s) = geodesic_segment_param G x u
[PROOF STEP]
have *: "isometry_on {s..t} (geodesic_segment_param G x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isometry_on {s..t} (geodesic_segment_param G x)
[PROOF STEP]
by (rule isometry_on_subset[of "{0..dist x y}"]) (auto simp add: assms)
[PROOF STATE]
proof (state)
this:
isometry_on {s..t} (geodesic_segment_param G x)

goal (2 subgoals):
 1. geodesic_segment_between (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (geodesic_segment_param G x t)
 2. \<And>u. \<lbrakk>s \<le> u; u \<le> t\<rbrakk> \<Longrightarrow> geodesic_segment_param (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (u - s) = geodesic_segment_param G x u
[PROOF STEP]
show B: "geodesic_segment_between (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (geodesic_segment_param G x t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_between (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (geodesic_segment_param G x t)
[PROOF STEP]
unfolding A
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_between (geodesic_segment_param G x ` {s..t}) (geodesic_segment_param G x s) (geodesic_segment_param G x t)
[PROOF STEP]
apply (rule geodesic_segmentI2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. isometry_on {s..t} (geodesic_segment_param G x)
 2. s \<le> t
[PROOF STEP]
using * assms
[PROOF STATE]
proof (prove)
using this:
isometry_on {s..t} (geodesic_segment_param G x)
geodesic_segment_between G x y
0 \<le> s
s \<le> t
t \<le> dist x y

goal (2 subgoals):
 1. isometry_on {s..t} (geodesic_segment_param G x)
 2. s \<le> t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
geodesic_segment_between (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (geodesic_segment_param G x t)

goal (1 subgoal):
 1. \<And>u. \<lbrakk>s \<le> u; u \<le> t\<rbrakk> \<Longrightarrow> geodesic_segment_param (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (u - s) = geodesic_segment_param G x u
[PROOF STEP]
fix u
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u. \<lbrakk>s \<le> u; u \<le> t\<rbrakk> \<Longrightarrow> geodesic_segment_param (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (u - s) = geodesic_segment_param G x u
[PROOF STEP]
assume u: "s \<le> u" "u \<le> t"
[PROOF STATE]
proof (state)
this:
s \<le> u
u \<le> t

goal (1 subgoal):
 1. \<And>u. \<lbrakk>s \<le> u; u \<le> t\<rbrakk> \<Longrightarrow> geodesic_segment_param (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (u - s) = geodesic_segment_param G x u
[PROOF STEP]
show "geodesic_segment_param (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (u - s) = geodesic_segment_param G x u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_param (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (u - s) = geodesic_segment_param G x u
[PROOF STEP]
proof (rule geodesic_segment_dist_unique[OF B])
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. geodesic_segment_param (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (u - s) \<in> geodesic_subsegment G x s t
 2. geodesic_segment_param G x u \<in> geodesic_subsegment G x s t
 3. dist (geodesic_segment_param G x s) (geodesic_segment_param (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (u - s)) = dist (geodesic_segment_param G x s) (geodesic_segment_param G x u)
[PROOF STEP]
show "geodesic_segment_param (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (u - s) \<in> geodesic_subsegment G x s t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_param (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (u - s) \<in> geodesic_subsegment G x s t
[PROOF STEP]
by (rule geodesic_segment_param_in_segment[OF geodesic_segment_endpoints(3)[OF B]])
[PROOF STATE]
proof (state)
this:
geodesic_segment_param (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (u - s) \<in> geodesic_subsegment G x s t

goal (2 subgoals):
 1. geodesic_segment_param G x u \<in> geodesic_subsegment G x s t
 2. dist (geodesic_segment_param G x s) (geodesic_segment_param (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (u - s)) = dist (geodesic_segment_param G x s) (geodesic_segment_param G x u)
[PROOF STEP]
show "geodesic_segment_param G x u \<in> geodesic_subsegment G x s t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_param G x u \<in> geodesic_subsegment G x s t
[PROOF STEP]
unfolding A
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_param G x u \<in> geodesic_segment_param G x ` {s..t}
[PROOF STEP]
using u
[PROOF STATE]
proof (prove)
using this:
s \<le> u
u \<le> t

goal (1 subgoal):
 1. geodesic_segment_param G x u \<in> geodesic_segment_param G x ` {s..t}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
geodesic_segment_param G x u \<in> geodesic_subsegment G x s t

goal (1 subgoal):
 1. dist (geodesic_segment_param G x s) (geodesic_segment_param (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (u - s)) = dist (geodesic_segment_param G x s) (geodesic_segment_param G x u)
[PROOF STEP]
have "dist (geodesic_segment_param G x s) (geodesic_segment_param (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (u - s)) = u - s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (geodesic_segment_param G x s) (geodesic_segment_param (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (u - s)) = u - s
[PROOF STEP]
using B assms u
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_between (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (geodesic_segment_param G x t)
geodesic_segment_between G x y
0 \<le> s
s \<le> t
t \<le> dist x y
s \<le> u
u \<le> t

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

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

goal (1 subgoal):
 1. dist (geodesic_segment_param G x s) (geodesic_segment_param (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (u - s)) = dist (geodesic_segment_param G x s) (geodesic_segment_param G x u)
[PROOF STEP]
have "dist (geodesic_segment_param G x s) (geodesic_segment_param G x u) = u -s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (geodesic_segment_param G x s) (geodesic_segment_param G x u) = u - s
[PROOF STEP]
using assms u
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_between G x y
0 \<le> s
s \<le> t
t \<le> dist x y
s \<le> u
u \<le> t

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

goal (1 subgoal):
 1. dist (geodesic_segment_param G x s) (geodesic_segment_param (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (u - s)) = dist (geodesic_segment_param G x s) (geodesic_segment_param G x u)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
dist (geodesic_segment_param G x s) (geodesic_segment_param (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (u - s)) = u - s
dist (geodesic_segment_param G x s) (geodesic_segment_param G x u) = u - s
[PROOF STEP]
show "dist (geodesic_segment_param G x s) (geodesic_segment_param (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (u - s)) =
        dist (geodesic_segment_param G x s) (geodesic_segment_param G x u)"
[PROOF STATE]
proof (prove)
using this:
dist (geodesic_segment_param G x s) (geodesic_segment_param (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (u - s)) = u - s
dist (geodesic_segment_param G x s) (geodesic_segment_param G x u) = u - s

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
geodesic_segment_param (geodesic_subsegment G x s t) (geodesic_segment_param G x s) (u - s) = geodesic_segment_param G x u

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma geodesic_segment_subparam:
  assumes "geodesic_segment_between G x z" "geodesic_segment_between H x y" "H \<subseteq> G" "t \<in> {0..dist x y}"
  shows "geodesic_segment_param G x t = geodesic_segment_param H x t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_param G x t = geodesic_segment_param H x t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. geodesic_segment_param G x t = geodesic_segment_param H x t
[PROOF STEP]
have "geodesic_segment_param H x t \<in> G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_param H x t \<in> G
[PROOF STEP]
using assms(3) geodesic_segment_param(3)[OF assms(2) assms(4)]
[PROOF STATE]
proof (prove)
using this:
H \<subseteq> G
geodesic_segment_param H x t \<in> H

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

goal (1 subgoal):
 1. geodesic_segment_param G x t = geodesic_segment_param H x t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
geodesic_segment_param H x t \<in> G
[PROOF STEP]
have "geodesic_segment_param H x t = geodesic_segment_param G x (dist x (geodesic_segment_param H x t))"
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_param H x t \<in> G

goal (1 subgoal):
 1. geodesic_segment_param H x t = geodesic_segment_param G x (dist x (geodesic_segment_param H x t))
[PROOF STEP]
using geodesic_segment_param(8)[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_param H x t \<in> G
?z \<in> G \<Longrightarrow> ?z = geodesic_segment_param G x (dist x ?z)

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

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

goal (1 subgoal):
 1. geodesic_segment_param G x t = geodesic_segment_param H x t
[PROOF STEP]
using geodesic_segment_param(6)[OF assms(2) assms(4)]
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_param H x t = geodesic_segment_param G x (dist x (geodesic_segment_param H x t))
dist x (geodesic_segment_param H x t) = t

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma geodesic_subsegment_exists:
  assumes "geodesic_segment G" "x \<in> G" "y \<in> G"
  shows "\<exists>H. H \<subseteq> G \<and> geodesic_segment_between H x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>H\<subseteq>G. geodesic_segment_between H x y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>H\<subseteq>G. geodesic_segment_between H x y
[PROOF STEP]
obtain a0 b0 where Ga0b0: "geodesic_segment_between G a0 b0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a0 b0. geodesic_segment_between G a0 b0 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
geodesic_segment G

goal (1 subgoal):
 1. (\<And>a0 b0. geodesic_segment_between G a0 b0 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding geodesic_segment_def
[PROOF STATE]
proof (prove)
using this:
\<exists>x. Ex (geodesic_segment_between G x)

goal (1 subgoal):
 1. (\<And>a0 b0. geodesic_segment_between G a0 b0 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
geodesic_segment_between G a0 b0

goal (1 subgoal):
 1. \<exists>H\<subseteq>G. geodesic_segment_between H x y
[PROOF STEP]
text \<open>Permuting the endpoints if necessary, we can ensure that the first endpoint $a$ is closer
  to $x$ than $y$.\<close>
[PROOF STATE]
proof (state)
this:
geodesic_segment_between G a0 b0

goal (1 subgoal):
 1. \<exists>H\<subseteq>G. geodesic_segment_between H x y
[PROOF STEP]
have "\<exists> a b. geodesic_segment_between G a b \<and> dist x a \<le> dist y a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a b. geodesic_segment_between G a b \<and> dist x a \<le> dist y a
[PROOF STEP]
proof (cases "dist x a0 \<le> dist y a0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. dist x a0 \<le> dist y a0 \<Longrightarrow> \<exists>a b. geodesic_segment_between G a b \<and> dist x a \<le> dist y a
 2. \<not> dist x a0 \<le> dist y a0 \<Longrightarrow> \<exists>a b. geodesic_segment_between G a b \<and> dist x a \<le> dist y a
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
dist x a0 \<le> dist y a0

goal (2 subgoals):
 1. dist x a0 \<le> dist y a0 \<Longrightarrow> \<exists>a b. geodesic_segment_between G a b \<and> dist x a \<le> dist y a
 2. \<not> dist x a0 \<le> dist y a0 \<Longrightarrow> \<exists>a b. geodesic_segment_between G a b \<and> dist x a \<le> dist y a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a b. geodesic_segment_between G a b \<and> dist x a \<le> dist y a
[PROOF STEP]
apply (rule exI[of _ a0], rule exI[of _ b0])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_between G a0 b0 \<and> dist x a0 \<le> dist y a0
[PROOF STEP]
using True Ga0b0
[PROOF STATE]
proof (prove)
using this:
dist x a0 \<le> dist y a0
geodesic_segment_between G a0 b0

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

goal (1 subgoal):
 1. \<not> dist x a0 \<le> dist y a0 \<Longrightarrow> \<exists>a b. geodesic_segment_between G a b \<and> dist x a \<le> dist y a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> dist x a0 \<le> dist y a0 \<Longrightarrow> \<exists>a b. geodesic_segment_between G a b \<and> dist x a \<le> dist y a
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> dist x a0 \<le> dist y a0

goal (1 subgoal):
 1. \<not> dist x a0 \<le> dist y a0 \<Longrightarrow> \<exists>a b. geodesic_segment_between G a b \<and> dist x a \<le> dist y a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a b. geodesic_segment_between G a b \<and> dist x a \<le> dist y a
[PROOF STEP]
apply (rule exI[of _ b0], rule exI[of _ a0])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_between G b0 a0 \<and> dist x b0 \<le> dist y b0
[PROOF STEP]
using Ga0b0 geodesic_segment_commute geodesic_segment_dist[OF Ga0b0 \<open>x \<in> G\<close>] geodesic_segment_dist[OF Ga0b0 \<open>y \<in> G\<close>] False
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_between G a0 b0
geodesic_segment_between ?G ?x ?y \<Longrightarrow> geodesic_segment_between ?G ?y ?x
dist a0 x + dist x b0 = dist a0 b0
dist a0 y + dist y b0 = dist a0 b0
\<not> dist x a0 \<le> dist y a0

goal (1 subgoal):
 1. geodesic_segment_between G b0 a0 \<and> dist x b0 \<le> dist y b0
[PROOF STEP]
by (auto simp add: dist_commute)
[PROOF STATE]
proof (state)
this:
\<exists>a b. geodesic_segment_between G a b \<and> dist x a \<le> dist y a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>a b. geodesic_segment_between G a b \<and> dist x a \<le> dist y a

goal (1 subgoal):
 1. \<exists>H\<subseteq>G. geodesic_segment_between H x y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>a b. geodesic_segment_between G a b \<and> dist x a \<le> dist y a
[PROOF STEP]
obtain a b where Gab: "geodesic_segment_between G a b" "dist x a \<le> dist y a"
[PROOF STATE]
proof (prove)
using this:
\<exists>a b. geodesic_segment_between G a b \<and> dist x a \<le> dist y a

goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>geodesic_segment_between G a b; dist x a \<le> dist y a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
geodesic_segment_between G a b
dist x a \<le> dist y a

goal (1 subgoal):
 1. \<exists>H\<subseteq>G. geodesic_segment_between H x y
[PROOF STEP]
have *: "0 \<le> dist x a" "dist x a \<le> dist y a" "dist y a \<le> dist a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> dist x a &&& dist x a \<le> dist y a &&& dist y a \<le> dist a b
[PROOF STEP]
using Gab assms
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_between G a b
dist x a \<le> dist y a
geodesic_segment G
x \<in> G
y \<in> G

goal (1 subgoal):
 1. 0 \<le> dist x a &&& dist x a \<le> dist y a &&& dist y a \<le> dist a b
[PROOF STEP]
by (meson geodesic_segment_dist_le geodesic_segment_endpoints(1) zero_le_dist)+
[PROOF STATE]
proof (state)
this:
0 \<le> dist x a
dist x a \<le> dist y a
dist y a \<le> dist a b

goal (1 subgoal):
 1. \<exists>H\<subseteq>G. geodesic_segment_between H x y
[PROOF STEP]
have **: "x = geodesic_segment_param G a (dist x a)" "y = geodesic_segment_param G a (dist y a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = geodesic_segment_param G a (dist x a) &&& y = geodesic_segment_param G a (dist y a)
[PROOF STEP]
using Gab \<open>x \<in> G\<close> \<open>y \<in> G\<close>
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_between G a b
dist x a \<le> dist y a
x \<in> G
y \<in> G

goal (1 subgoal):
 1. x = geodesic_segment_param G a (dist x a) &&& y = geodesic_segment_param G a (dist y a)
[PROOF STEP]
by (metis dist_commute geodesic_segment_param(8))+
[PROOF STATE]
proof (state)
this:
x = geodesic_segment_param G a (dist x a)
y = geodesic_segment_param G a (dist y a)

goal (1 subgoal):
 1. \<exists>H\<subseteq>G. geodesic_segment_between H x y
[PROOF STEP]
define H where "H = geodesic_subsegment G a (dist x a) (dist y a)"
[PROOF STATE]
proof (state)
this:
H = geodesic_subsegment G a (dist x a) (dist y a)

goal (1 subgoal):
 1. \<exists>H\<subseteq>G. geodesic_segment_between H x y
[PROOF STEP]
have "H \<subseteq> G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<subseteq> G
[PROOF STEP]
unfolding H_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_subsegment G a (dist x a) (dist y a) \<subseteq> G
[PROOF STEP]
by (rule geodesic_subsegment_subset)
[PROOF STATE]
proof (state)
this:
H \<subseteq> G

goal (1 subgoal):
 1. \<exists>H\<subseteq>G. geodesic_segment_between H x y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
H \<subseteq> G

goal (1 subgoal):
 1. \<exists>H\<subseteq>G. geodesic_segment_between H x y
[PROOF STEP]
have "geodesic_segment_between H x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_between H x y
[PROOF STEP]
unfolding H_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_between (geodesic_subsegment G a (dist x a) (dist y a)) x y
[PROOF STEP]
using geodesic_subsegment(2)[OF Gab(1) *] **
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_between (geodesic_subsegment G a (dist x a) (dist y a)) (geodesic_segment_param G a (dist x a)) (geodesic_segment_param G a (dist y a))
x = geodesic_segment_param G a (dist x a)
y = geodesic_segment_param G a (dist y a)

goal (1 subgoal):
 1. geodesic_segment_between (geodesic_subsegment G a (dist x a) (dist y a)) x y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
geodesic_segment_between H x y

goal (1 subgoal):
 1. \<exists>H\<subseteq>G. geodesic_segment_between H x y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
H \<subseteq> G
geodesic_segment_between H x y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
H \<subseteq> G
geodesic_segment_between H x y

goal (1 subgoal):
 1. \<exists>H\<subseteq>G. geodesic_segment_between H x y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>H\<subseteq>G. geodesic_segment_between H x y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma geodesic_segment_homeo_interval:
  assumes "geodesic_segment_between G x y"
  shows "{0..dist x y} homeomorphic G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {0..dist x y} homeomorphic G
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {0..dist x y} homeomorphic G
[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. {0..dist x y} homeomorphic G
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {0..dist x y} homeomorphic G
[PROOF STEP]
using isometry_on_homeomorphism(3)[OF g(3)]
[PROOF STATE]
proof (prove)
using this:
{0..dist x y} homeomorphic g ` {0..dist x y}

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma geodesic_segment_topology:
  assumes "geodesic_segment G"
  shows "compact G" "connected G" "path_connected G" "bounded G" "closed G" "G \<noteq> {}" "proper G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (compact G &&& connected G &&& path_connected G) &&& (bounded G &&& closed G) &&& G \<noteq> {} &&& proper G
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. compact G
 2. connected G
 3. path_connected G
 4. bounded G
 5. closed G
 6. G \<noteq> {}
 7. proper G
[PROOF STEP]
show "compact G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. compact G
[PROOF STEP]
using assms geodesic_segment_homeo_interval homeomorphic_compactness
[PROOF STATE]
proof (prove)
using this:
geodesic_segment G
geodesic_segment_between ?G ?x ?y \<Longrightarrow> {0..dist ?x ?y} homeomorphic ?G
?s homeomorphic ?t \<Longrightarrow> compact ?s = compact ?t

goal (1 subgoal):
 1. compact G
[PROOF STEP]
unfolding geodesic_segment_def
[PROOF STATE]
proof (prove)
using this:
\<exists>x. Ex (geodesic_segment_between G x)
geodesic_segment_between ?G ?x ?y \<Longrightarrow> {0..dist ?x ?y} homeomorphic ?G
?s homeomorphic ?t \<Longrightarrow> compact ?s = compact ?t

goal (1 subgoal):
 1. compact G
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
compact G

goal (6 subgoals):
 1. connected G
 2. path_connected G
 3. bounded G
 4. closed G
 5. G \<noteq> {}
 6. proper G
[PROOF STEP]
show "path_connected G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path_connected G
[PROOF STEP]
using assms is_interval_path_connected geodesic_segment_homeo_interval homeomorphic_path_connectedness
[PROOF STATE]
proof (prove)
using this:
geodesic_segment G
is_interval ?S \<Longrightarrow> path_connected ?S
geodesic_segment_between ?G ?x ?y \<Longrightarrow> {0..dist ?x ?y} homeomorphic ?G
?S homeomorphic ?T \<Longrightarrow> path_connected ?S = path_connected ?T

goal (1 subgoal):
 1. path_connected G
[PROOF STEP]
unfolding geodesic_segment_def
[PROOF STATE]
proof (prove)
using this:
\<exists>x. Ex (geodesic_segment_between G x)
is_interval ?S \<Longrightarrow> path_connected ?S
geodesic_segment_between ?G ?x ?y \<Longrightarrow> {0..dist ?x ?y} homeomorphic ?G
?S homeomorphic ?T \<Longrightarrow> path_connected ?S = path_connected ?T

goal (1 subgoal):
 1. path_connected G
[PROOF STEP]
by (metis is_interval_cc)
[PROOF STATE]
proof (state)
this:
path_connected G

goal (5 subgoals):
 1. connected G
 2. bounded G
 3. closed G
 4. G \<noteq> {}
 5. proper G
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path_connected G
[PROOF STEP]
show "connected G"
[PROOF STATE]
proof (prove)
using this:
path_connected G

goal (1 subgoal):
 1. connected G
[PROOF STEP]
using path_connected_imp_connected
[PROOF STATE]
proof (prove)
using this:
path_connected G
path_connected ?S \<Longrightarrow> connected ?S

goal (1 subgoal):
 1. connected G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
connected G

goal (4 subgoals):
 1. bounded G
 2. closed G
 3. G \<noteq> {}
 4. proper G
[PROOF STEP]
show "bounded G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded G
[PROOF STEP]
by (rule compact_imp_bounded, fact)
[PROOF STATE]
proof (state)
this:
bounded G

goal (3 subgoals):
 1. closed G
 2. G \<noteq> {}
 3. proper G
[PROOF STEP]
show "closed G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed G
[PROOF STEP]
by (rule compact_imp_closed, fact)
[PROOF STATE]
proof (state)
this:
closed G

goal (2 subgoals):
 1. G \<noteq> {}
 2. proper G
[PROOF STEP]
show "G \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. G \<noteq> {}
[PROOF STEP]
using assms geodesic_segment_def geodesic_segment_endpoints(3)
[PROOF STATE]
proof (prove)
using this:
geodesic_segment G
geodesic_segment ?G = (\<exists>x y. geodesic_segment_between ?G x y)
geodesic_segment_between ?G ?x ?y \<Longrightarrow> ?G \<noteq> {}

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

goal (1 subgoal):
 1. proper G
[PROOF STEP]
show "proper G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper G
[PROOF STEP]
using proper_of_compact \<open>compact G\<close>
[PROOF STATE]
proof (prove)
using this:
compact ?S \<Longrightarrow> proper ?S
compact G

goal (1 subgoal):
 1. proper G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
proper G

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma geodesic_segment_between_x_x [simp]:
  "geodesic_segment_between {x} x x"
  "geodesic_segment {x}"
  "geodesic_segment_between G x x \<longleftrightarrow> G = {x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_between {x} x x &&& geodesic_segment {x} &&& geodesic_segment_between G x x = (G = {x})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. geodesic_segment_between {x} x x
 2. geodesic_segment {x}
 3. geodesic_segment_between G x x = (G = {x})
[PROOF STEP]
show *: "geodesic_segment_between {x} x x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_between {x} x x
[PROOF STEP]
unfolding geodesic_segment_between_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>g. g 0 = x \<and> g (dist x x) = x \<and> isometry_on {0..dist x x} g \<and> {x} = g ` {0..dist x x}
[PROOF STEP]
apply (rule exI[of _ "\<lambda>_. x"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = x \<and> x = x \<and> isometry_on {0..dist x x} (\<lambda>_. x) \<and> {x} = (\<lambda>_. x) ` {0..dist x x}
[PROOF STEP]
unfolding isometry_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = x \<and> x = x \<and> (\<forall>xa\<in>{0..dist x x}. \<forall>y\<in>{0..dist x x}. dist x x = dist xa y) \<and> {x} = (\<lambda>_. x) ` {0..dist x x}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
geodesic_segment_between {x} x x

goal (2 subgoals):
 1. geodesic_segment {x}
 2. geodesic_segment_between G x x = (G = {x})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
geodesic_segment_between {x} x x
[PROOF STEP]
show "geodesic_segment {x}"
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_between {x} x x

goal (1 subgoal):
 1. geodesic_segment {x}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
geodesic_segment {x}

goal (1 subgoal):
 1. geodesic_segment_between G x x = (G = {x})
[PROOF STEP]
show "geodesic_segment_between G x x \<longleftrightarrow> G = {x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_between G x x = (G = {x})
[PROOF STEP]
using geodesic_segment_dist_le geodesic_segment_endpoints(2) *
[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> ?y \<in> ?G
geodesic_segment_between {x} x x

goal (1 subgoal):
 1. geodesic_segment_between G x x = (G = {x})
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
geodesic_segment_between G x x = (G = {x})

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma geodesic_segment_disconnection:
  assumes "geodesic_segment_between G x y" "z \<in> G"
  shows "(connected (G - {z})) = (z = x \<or> z = y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. connected (G - {z}) = (z = x \<or> z = y)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. connected (G - {z}) = (z = x \<or> z = 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. connected (G - {z}) = (z = x \<or> z = y)
[PROOF STEP]
obtain t where t: "t \<in> {0..dist x y}" "z = g t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t. \<lbrakk>t \<in> {0..dist x y}; z = g t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>z \<in> G\<close> g(4)
[PROOF STATE]
proof (prove)
using this:
z \<in> G
G = g ` {0..dist x y}

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

goal (1 subgoal):
 1. connected (G - {z}) = (z = x \<or> z = y)
[PROOF STEP]
have "({0..dist x y} - {t}) homeomorphic (G - {g t})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {0..dist x y} - {t} homeomorphic G - {g t}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {0..dist x y} - {t} homeomorphic G - {g t}
[PROOF STEP]
have *: "isometry_on ({0..dist x y} - {t}) g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isometry_on ({0..dist x y} - {t}) g
[PROOF STEP]
apply (rule isometry_on_subset[OF g(3)])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {0..dist x y} - {t} \<subseteq> {0..dist x y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
isometry_on ({0..dist x y} - {t}) g

goal (1 subgoal):
 1. {0..dist x y} - {t} homeomorphic G - {g t}
[PROOF STEP]
have "({0..dist x y} - {t}) homeomorphic g`({0..dist x y} - {t})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {0..dist x y} - {t} homeomorphic g ` ({0..dist x y} - {t})
[PROOF STEP]
by (rule isometry_on_homeomorphism(3)[OF *])
[PROOF STATE]
proof (state)
this:
{0..dist x y} - {t} homeomorphic g ` ({0..dist x y} - {t})

goal (1 subgoal):
 1. {0..dist x y} - {t} homeomorphic G - {g t}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{0..dist x y} - {t} homeomorphic g ` ({0..dist x y} - {t})

goal (1 subgoal):
 1. {0..dist x y} - {t} homeomorphic G - {g t}
[PROOF STEP]
have "g`({0..dist x y} - {t}) = G - {g t}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g ` ({0..dist x y} - {t}) = G - {g t}
[PROOF STEP]
unfolding g(4)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g ` ({0..dist x y} - {t}) = g ` {0..dist x y} - {g t}
[PROOF STEP]
using isometry_on_injective[OF g(3)] t
[PROOF STATE]
proof (prove)
using this:
inj_on g {0..dist x y}
t \<in> {0..dist x y}
z = g t

goal (1 subgoal):
 1. g ` ({0..dist x y} - {t}) = g ` {0..dist x y} - {g t}
[PROOF STEP]
by (auto simp add: inj_onD)
[PROOF STATE]
proof (state)
this:
g ` ({0..dist x y} - {t}) = G - {g t}

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

goal (1 subgoal):
 1. {0..dist x y} - {t} homeomorphic G - {g t}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{0..dist x y} - {t} homeomorphic G - {g t}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{0..dist x y} - {t} homeomorphic G - {g t}

goal (1 subgoal):
 1. connected (G - {z}) = (z = x \<or> z = y)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{0..dist x y} - {t} homeomorphic G - {g t}

goal (1 subgoal):
 1. connected (G - {z}) = (z = x \<or> z = y)
[PROOF STEP]
have "connected({0..dist x y} - {t}) = (t = 0 \<or> t = dist x y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. connected ({0..dist x y} - {t}) = (t = 0 \<or> t = dist x y)
[PROOF STEP]
using t(1)
[PROOF STATE]
proof (prove)
using this:
t \<in> {0..dist x y}

goal (1 subgoal):
 1. connected ({0..dist x y} - {t}) = (t = 0 \<or> t = dist x y)
[PROOF STEP]
by (auto simp add: connected_iff_interval, fastforce)
[PROOF STATE]
proof (state)
this:
connected ({0..dist x y} - {t}) = (t = 0 \<or> t = dist x y)

goal (1 subgoal):
 1. connected (G - {z}) = (z = x \<or> z = y)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{0..dist x y} - {t} homeomorphic G - {g t}
connected ({0..dist x y} - {t}) = (t = 0 \<or> t = dist x y)
[PROOF STEP]
have "connected (G - {z}) = (t = 0 \<or> t = dist x y)"
[PROOF STATE]
proof (prove)
using this:
{0..dist x y} - {t} homeomorphic G - {g t}
connected ({0..dist x y} - {t}) = (t = 0 \<or> t = dist x y)

goal (1 subgoal):
 1. connected (G - {z}) = (t = 0 \<or> t = dist x y)
[PROOF STEP]
unfolding \<open>z = g t\<close>[symmetric]
[PROOF STATE]
proof (prove)
using this:
{0..dist x y} - {t} homeomorphic G - {z}
connected ({0..dist x y} - {t}) = (t = 0 \<or> t = dist x y)

goal (1 subgoal):
 1. connected (G - {z}) = (t = 0 \<or> t = dist x y)
[PROOF STEP]
using homeomorphic_connectedness
[PROOF STATE]
proof (prove)
using this:
{0..dist x y} - {t} homeomorphic G - {z}
connected ({0..dist x y} - {t}) = (t = 0 \<or> t = dist x y)
?s homeomorphic ?t \<Longrightarrow> connected ?s = connected ?t

goal (1 subgoal):
 1. connected (G - {z}) = (t = 0 \<or> t = dist x y)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
connected (G - {z}) = (t = 0 \<or> t = dist x y)

goal (1 subgoal):
 1. connected (G - {z}) = (z = x \<or> z = y)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
connected (G - {z}) = (t = 0 \<or> t = dist x y)

goal (1 subgoal):
 1. connected (G - {z}) = (z = x \<or> z = y)
[PROOF STEP]
have "(t = 0 \<or> t = dist x y) = (z = x \<or> z = y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (t = 0 \<or> t = dist x y) = (z = x \<or> z = y)
[PROOF STEP]
using t g
[PROOF STATE]
proof (prove)
using this:
t \<in> {0..dist x y}
z = 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. (t = 0 \<or> t = dist x y) = (z = x \<or> z = y)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>z = g 0; 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; t \<noteq> dist (g 0) y; g t = g 0\<rbrakk> \<Longrightarrow> t = 0
 2. \<lbrakk>z = g t; g (dist (g 0) (g t)) = g t; isometry_on {0..dist (g 0) (g t)} g; G = g ` {0..dist (g 0) (g t)}; x = g 0; 0 \<le> t; t \<le> dist (g 0) (g t); t \<noteq> dist (g 0) (g t); y = g t\<rbrakk> \<Longrightarrow> t = 0
[PROOF STEP]
by (metis atLeastAtMost_iff isometry_on_inverse(2) order_refl zero_le_dist)+
[PROOF STATE]
proof (state)
this:
(t = 0 \<or> t = dist x y) = (z = x \<or> z = y)

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

goal (1 subgoal):
 1. connected (G - {z}) = (z = x \<or> z = y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
connected (G - {z}) = (z = x \<or> z = y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma geodesic_segment_unique_endpoints:
  assumes "geodesic_segment_between G x y"
          "geodesic_segment_between G a b"
  shows "{x, y} = {a, b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x, y} = {a, b}
[PROOF STEP]
by (metis geodesic_segment_disconnection assms(1) assms(2) doubleton_eq_iff geodesic_segment_endpoints(1) geodesic_segment_endpoints(2))


[STATEMENT]
lemma geodesic_segment_subsegment:
  assumes "geodesic_segment G" "H \<subseteq> G" "compact H" "connected H" "H \<noteq> {}"
  shows "geodesic_segment H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment H
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. geodesic_segment H
[PROOF STEP]
obtain x y where "geodesic_segment_between G x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. geodesic_segment_between G x y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
geodesic_segment G
H \<subseteq> G
compact H
connected H
H \<noteq> {}

goal (1 subgoal):
 1. (\<And>x y. geodesic_segment_between G x y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding geodesic_segment_def
[PROOF STATE]
proof (prove)
using this:
\<exists>x. Ex (geodesic_segment_between G x)
H \<subseteq> G
compact H
connected H
H \<noteq> {}

goal (1 subgoal):
 1. (\<And>x y. geodesic_segment_between G x y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
geodesic_segment_between G x y

goal (1 subgoal):
 1. geodesic_segment H
[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. geodesic_segment H
[PROOF STEP]
define L where "L = (inv_into {0..dist x y} g)`H"
[PROOF STATE]
proof (state)
this:
L = inv_into {0..dist x y} g ` H

goal (1 subgoal):
 1. geodesic_segment H
[PROOF STEP]
have "L \<subseteq> {0..dist x y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L \<subseteq> {0..dist x y}
[PROOF STEP]
unfolding L_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_into {0..dist x y} g ` H \<subseteq> {0..dist x y}
[PROOF STEP]
using isometry_on_inverse[OF \<open>isometry_on {0..dist x y} g\<close>] assms(2) g(4)
[PROOF STATE]
proof (prove)
using this:
isometry_on (g ` {0..dist x y}) (inv_into {0..dist x y} g)
?x \<in> {0..dist x y} \<Longrightarrow> inv_into {0..dist x y} g (g ?x) = ?x
?y \<in> g ` {0..dist x y} \<Longrightarrow> g (inv_into {0..dist x y} g ?y) = ?y
bij_betw g {0..dist x y} (g ` {0..dist x y})
H \<subseteq> G
G = g ` {0..dist x y}

goal (1 subgoal):
 1. inv_into {0..dist x y} g ` H \<subseteq> {0..dist x y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
L \<subseteq> {0..dist x y}

goal (1 subgoal):
 1. geodesic_segment H
[PROOF STEP]
have "isometry_on G (inv_into {0..dist x y} g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isometry_on G (inv_into {0..dist x y} g)
[PROOF STEP]
using isometry_on_inverse[OF \<open>isometry_on {0..dist x y} g\<close>] g(4)
[PROOF STATE]
proof (prove)
using this:
isometry_on (g ` {0..dist x y}) (inv_into {0..dist x y} g)
?x \<in> {0..dist x y} \<Longrightarrow> inv_into {0..dist x y} g (g ?x) = ?x
?y \<in> g ` {0..dist x y} \<Longrightarrow> g (inv_into {0..dist x y} g ?y) = ?y
bij_betw g {0..dist x y} (g ` {0..dist x y})
G = g ` {0..dist x y}

goal (1 subgoal):
 1. isometry_on G (inv_into {0..dist x y} g)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
isometry_on G (inv_into {0..dist x y} g)

goal (1 subgoal):
 1. geodesic_segment H
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
isometry_on G (inv_into {0..dist x y} g)
[PROOF STEP]
have "isometry_on H (inv_into {0..dist x y} g)"
[PROOF STATE]
proof (prove)
using this:
isometry_on G (inv_into {0..dist x y} g)

goal (1 subgoal):
 1. isometry_on H (inv_into {0..dist x y} g)
[PROOF STEP]
using \<open>H \<subseteq> G\<close> isometry_on_subset
[PROOF STATE]
proof (prove)
using this:
isometry_on G (inv_into {0..dist x y} g)
H \<subseteq> G
\<lbrakk>isometry_on ?X ?f; ?Y \<subseteq> ?X\<rbrakk> \<Longrightarrow> isometry_on ?Y ?f

goal (1 subgoal):
 1. isometry_on H (inv_into {0..dist x y} g)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
isometry_on H (inv_into {0..dist x y} g)

goal (1 subgoal):
 1. geodesic_segment H
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
isometry_on H (inv_into {0..dist x y} g)
[PROOF STEP]
have "H homeomorphic L"
[PROOF STATE]
proof (prove)
using this:
isometry_on H (inv_into {0..dist x y} g)

goal (1 subgoal):
 1. H homeomorphic L
[PROOF STEP]
unfolding L_def
[PROOF STATE]
proof (prove)
using this:
isometry_on H (inv_into {0..dist x y} g)

goal (1 subgoal):
 1. H homeomorphic inv_into {0..dist x y} g ` H
[PROOF STEP]
using isometry_on_homeomorphism(3)
[PROOF STATE]
proof (prove)
using this:
isometry_on H (inv_into {0..dist x y} g)
isometry_on ?X ?f \<Longrightarrow> ?X homeomorphic ?f ` ?X

goal (1 subgoal):
 1. H homeomorphic inv_into {0..dist x y} g ` H
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
H homeomorphic L

goal (1 subgoal):
 1. geodesic_segment H
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
H homeomorphic L
[PROOF STEP]
have "compact L \<and> connected L"
[PROOF STATE]
proof (prove)
using this:
H homeomorphic L

goal (1 subgoal):
 1. compact L \<and> connected L
[PROOF STEP]
using assms homeomorphic_compactness homeomorphic_connectedness
[PROOF STATE]
proof (prove)
using this:
H homeomorphic L
geodesic_segment G
H \<subseteq> G
compact H
connected H
H \<noteq> {}
?s homeomorphic ?t \<Longrightarrow> compact ?s = compact ?t
?s homeomorphic ?t \<Longrightarrow> connected ?s = connected ?t

goal (1 subgoal):
 1. compact L \<and> connected L
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
compact L \<and> connected L

goal (1 subgoal):
 1. geodesic_segment H
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
compact L \<and> connected L
[PROOF STEP]
obtain a b where "L = {a..b}"
[PROOF STATE]
proof (prove)
using this:
compact L \<and> connected L

goal (1 subgoal):
 1. (\<And>a b. L = {a..b} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using connected_compact_interval_1[of L]
[PROOF STATE]
proof (prove)
using this:
compact L \<and> connected L
(connected L \<and> compact L) = (\<exists>a b. L = {a..b})

goal (1 subgoal):
 1. (\<And>a b. L = {a..b} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
L = {a..b}

goal (1 subgoal):
 1. geodesic_segment H
[PROOF STEP]
have "a \<le> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> b
[PROOF STEP]
using \<open>H \<noteq> {}\<close> \<open>L = {a..b}\<close>
[PROOF STATE]
proof (prove)
using this:
H \<noteq> {}
L = {a..b}

goal (1 subgoal):
 1. a \<le> b
[PROOF STEP]
unfolding L_def
[PROOF STATE]
proof (prove)
using this:
H \<noteq> {}
inv_into {0..dist x y} g ` H = {a..b}

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

goal (1 subgoal):
 1. geodesic_segment H
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<le> b
[PROOF STEP]
have "0 \<le> a" "b \<le> dist x y"
[PROOF STATE]
proof (prove)
using this:
a \<le> b

goal (1 subgoal):
 1. 0 \<le> a &&& b \<le> dist x y
[PROOF STEP]
using \<open>L \<subseteq> {0..dist x y}\<close> \<open>L = {a..b}\<close>
[PROOF STATE]
proof (prove)
using this:
a \<le> b
L \<subseteq> {0..dist x y}
L = {a..b}

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

goal (1 subgoal):
 1. geodesic_segment H
[PROOF STEP]
have *: "H = g`{a..b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H = g ` {a..b}
[PROOF STEP]
by (metis L_def \<open>L = {a..b}\<close> assms(2) g(4) image_inv_into_cancel)
[PROOF STATE]
proof (state)
this:
H = g ` {a..b}

goal (1 subgoal):
 1. geodesic_segment H
[PROOF STEP]
show "geodesic_segment H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment H
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment (g ` {a..b})
[PROOF STEP]
apply (rule geodesic_segmentI2[OF _ \<open>a \<le> b\<close>])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isometry_on {a..b} g
[PROOF STEP]
apply (rule isometry_on_subset[OF g(3)])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {a..b} \<subseteq> {0..dist x y}
[PROOF STEP]
using \<open>0 \<le> a\<close> \<open>b \<le> dist x y\<close>
[PROOF STATE]
proof (prove)
using this:
0 \<le> a
b \<le> dist x y

goal (1 subgoal):
 1. {a..b} \<subseteq> {0..dist x y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
geodesic_segment H

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma isometry_preserves_geodesic_segment_between:
  assumes "isometry_on X f"
          "G \<subseteq> X" "geodesic_segment_between G x y"
  shows "geodesic_segment_between (f`G) (f x) (f y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_between (f ` G) (f x) (f y)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. geodesic_segment_between (f ` G) (f x) (f 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. geodesic_segment_between (f ` G) (f x) (f y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
g 0 = x
g (dist x y) = y
isometry_on {0..dist x y} g
G = g ` {0..dist x y}
[PROOF STEP]
have *: "f`G = (f o g) `{0..dist x y}" "f x = (f o g) 0" "f y = (f o g) (dist x y)"
[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. f ` G = (f \<circ> g) ` {0..dist x y} &&& f x = (f \<circ> g) 0 &&& f y = (f \<circ> g) (dist x y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f ` G = (f \<circ> g) ` {0..dist x y}
f x = (f \<circ> g) 0
f y = (f \<circ> g) (dist x y)

goal (1 subgoal):
 1. geodesic_segment_between (f ` G) (f x) (f y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_between (f ` G) (f x) (f y)
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_between ((f \<circ> g) ` {0..dist x y}) ((f \<circ> g) 0) ((f \<circ> g) (dist x y))
[PROOF STEP]
apply (intro geodesic_segmentI2(1))
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. isometry_on {0..dist x y} (f \<circ> g)
 2. 0 \<le> dist x y
[PROOF STEP]
unfolding comp_def
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. isometry_on {0..dist x y} (\<lambda>x. f (g x))
 2. 0 \<le> dist x y
[PROOF STEP]
apply (rule isometry_on_compose[of _ g])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. isometry_on {0..dist x y} g
 2. isometry_on (g ` {0..dist x y}) f
 3. 0 \<le> dist x y
[PROOF STEP]
using g(3) g(4) assms
[PROOF STATE]
proof (prove)
using this:
isometry_on {0..dist x y} g
G = g ` {0..dist x y}
isometry_on X f
G \<subseteq> X
geodesic_segment_between G x y

goal (3 subgoals):
 1. isometry_on {0..dist x y} g
 2. isometry_on (g ` {0..dist x y}) f
 3. 0 \<le> dist x y
[PROOF STEP]
by (auto intro: isometry_on_subset)
[PROOF STATE]
proof (state)
this:
geodesic_segment_between (f ` G) (f x) (f y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma geodesic_segment_distance:
  assumes "geodesic_segment_between G x y"
  shows "dist w x + dist w y \<le> dist x y + 2 * infdist w G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist w x + dist w y \<le> dist x y + 2 * infdist w G
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist w x + dist w y \<le> dist x y + 2 * infdist w G
[PROOF STEP]
have "\<exists>z \<in> G. infdist w G = dist w z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>z\<in>G. infdist w G = dist w z
[PROOF STEP]
apply (rule infdist_proper_attained)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. proper G
 2. G \<noteq> {}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_between G x y

goal (2 subgoals):
 1. proper G
 2. G \<noteq> {}
[PROOF STEP]
by (auto simp add: geodesic_segment_topology)
[PROOF STATE]
proof (state)
this:
\<exists>z\<in>G. infdist w G = dist w z

goal (1 subgoal):
 1. dist w x + dist w y \<le> dist x y + 2 * infdist w G
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>z\<in>G. infdist w G = dist w z
[PROOF STEP]
obtain z where z: "z \<in> G" "infdist w G = dist w z"
[PROOF STATE]
proof (prove)
using this:
\<exists>z\<in>G. infdist w G = dist w z

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>z \<in> G; infdist w G = dist w z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<in> G
infdist w G = dist w z

goal (1 subgoal):
 1. dist w x + dist w y \<le> dist x y + 2 * infdist w G
[PROOF STEP]
have "dist w x + dist w y \<le> (dist w z + dist z x) + (dist w z + dist z y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist w x + dist w y \<le> dist w z + dist z x + (dist w z + dist z y)
[PROOF STEP]
by (intro mono_intros)
[PROOF STATE]
proof (state)
this:
dist w x + dist w y \<le> dist w z + dist z x + (dist w z + dist z y)

goal (1 subgoal):
 1. dist w x + dist w y \<le> dist x y + 2 * infdist w G
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist w x + dist w y \<le> dist w z + dist z x + (dist w z + dist z y)

goal (1 subgoal):
 1. dist w x + dist w y \<le> dist x y + 2 * infdist w G
[PROOF STEP]
have "... = dist x z + dist z y + 2 * dist w z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist w z + dist z x + (dist w z + dist z y) = dist x z + dist z y + 2 * dist w z
[PROOF STEP]
by (auto simp add: dist_commute)
[PROOF STATE]
proof (state)
this:
dist w z + dist z x + (dist w z + dist z y) = dist x z + dist z y + 2 * dist w z

goal (1 subgoal):
 1. dist w x + dist w y \<le> dist x y + 2 * infdist w G
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist w z + dist z x + (dist w z + dist z y) = dist x z + dist z y + 2 * dist w z

goal (1 subgoal):
 1. dist w x + dist w y \<le> dist x y + 2 * infdist w G
[PROOF STEP]
have "... = dist x y + 2 * infdist w G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist x z + dist z y + 2 * dist w z = dist x y + 2 * infdist w G
[PROOF STEP]
using z(1) assms geodesic_segment_dist
[PROOF STATE]
proof (prove)
using this:
z \<in> G
geodesic_segment_between G x y
\<lbrakk>geodesic_segment_between ?G ?x ?y; ?a \<in> ?G\<rbrakk> \<Longrightarrow> dist ?x ?a + dist ?a ?y = dist ?x ?y

goal (1 subgoal):
 1. dist x z + dist z y + 2 * dist w z = dist x y + 2 * infdist w G
[PROOF STEP]
unfolding z(2)
[PROOF STATE]
proof (prove)
using this:
z \<in> G
geodesic_segment_between G x y
\<lbrakk>geodesic_segment_between ?G ?x ?y; ?a \<in> ?G\<rbrakk> \<Longrightarrow> dist ?x ?a + dist ?a ?y = dist ?x ?y

goal (1 subgoal):
 1. dist x z + dist z y + 2 * dist w z = dist x y + 2 * dist w z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist x z + dist z y + 2 * dist w z = dist x y + 2 * infdist w G

goal (1 subgoal):
 1. dist w x + dist w y \<le> dist x y + 2 * infdist w G
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist w x + dist w y \<le> dist x y + 2 * infdist w G
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dist w x + dist w y \<le> dist x y + 2 * infdist w G

goal (1 subgoal):
 1. dist w x + dist w y \<le> dist x y + 2 * infdist w G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist w x + dist w y \<le> dist x y + 2 * infdist w G

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proj_set_geodesic_same_basepoint:
  assumes "p \<in> proj_set x A" "geodesic_segment_between G p x" "y \<in> G"
  shows "p \<in> proj_set y A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> proj_set y A
[PROOF STEP]
proof (rule proj_setI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p \<in> A
 2. dist y p \<le> infdist y A
[PROOF STEP]
show "p \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> A
[PROOF STEP]
using assms proj_setD
[PROOF STATE]
proof (prove)
using this:
p \<in> proj_set x A
geodesic_segment_between G p x
y \<in> G
?y \<in> proj_set ?x ?A \<Longrightarrow> ?y \<in> ?A
?y \<in> proj_set ?x ?A \<Longrightarrow> dist ?x ?y = infdist ?x ?A

goal (1 subgoal):
 1. p \<in> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p \<in> A

goal (1 subgoal):
 1. dist y p \<le> infdist y A
[PROOF STEP]
have *: "dist y p \<le> dist y q" if "q \<in> A" for q
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist y p \<le> dist y q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist y p \<le> dist y q
[PROOF STEP]
have "dist p y + dist y x = dist p x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist p y + dist y x = dist p x
[PROOF STEP]
using assms geodesic_segment_dist
[PROOF STATE]
proof (prove)
using this:
p \<in> proj_set x A
geodesic_segment_between G p x
y \<in> G
\<lbrakk>geodesic_segment_between ?G ?x ?y; ?a \<in> ?G\<rbrakk> \<Longrightarrow> dist ?x ?a + dist ?a ?y = dist ?x ?y

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

goal (1 subgoal):
 1. dist y p \<le> dist y q
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist p y + dist y x = dist p x

goal (1 subgoal):
 1. dist y p \<le> dist y q
[PROOF STEP]
have "... \<le> dist q x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist p x \<le> dist q x
[PROOF STEP]
using proj_set_dist_le[OF \<open>q \<in> A\<close> assms(1)]
[PROOF STATE]
proof (prove)
using this:
dist x p \<le> dist x q

goal (1 subgoal):
 1. dist p x \<le> dist q x
[PROOF STEP]
by (simp add: dist_commute)
[PROOF STATE]
proof (state)
this:
dist p x \<le> dist q x

goal (1 subgoal):
 1. dist y p \<le> dist y q
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist p x \<le> dist q x

goal (1 subgoal):
 1. dist y p \<le> dist y q
[PROOF STEP]
have "... \<le> dist q y + dist y x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist q x \<le> dist q y + dist y x
[PROOF STEP]
by (intro mono_intros)
[PROOF STATE]
proof (state)
this:
dist q x \<le> dist q y + dist y x

goal (1 subgoal):
 1. dist y p \<le> dist y q
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist p y + dist y x \<le> dist q y + dist y x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dist p y + dist y x \<le> dist q y + dist y x

goal (1 subgoal):
 1. dist y p \<le> dist y q
[PROOF STEP]
by (simp add: dist_commute)
[PROOF STATE]
proof (state)
this:
dist y p \<le> dist y q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?q \<in> A \<Longrightarrow> dist y p \<le> dist y ?q

goal (1 subgoal):
 1. dist y p \<le> infdist y A
[PROOF STEP]
have "dist y p \<le> Inf (dist y ` A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist y p \<le> Inf (dist y ` A)
[PROOF STEP]
apply (rule cINF_greatest)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. A \<noteq> {}
 2. \<And>x. x \<in> A \<Longrightarrow> dist y p \<le> dist y x
[PROOF STEP]
using \<open>p \<in> A\<close> *
[PROOF STATE]
proof (prove)
using this:
p \<in> A
?q \<in> A \<Longrightarrow> dist y p \<le> dist y ?q

goal (2 subgoals):
 1. A \<noteq> {}
 2. \<And>x. x \<in> A \<Longrightarrow> dist y p \<le> dist y x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist y p \<le> Inf (dist y ` A)

goal (1 subgoal):
 1. dist y p \<le> infdist y A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dist y p \<le> Inf (dist y ` A)
[PROOF STEP]
show "dist y p \<le> infdist y A"
[PROOF STATE]
proof (prove)
using this:
dist y p \<le> Inf (dist y ` A)

goal (1 subgoal):
 1. dist y p \<le> infdist y A
[PROOF STEP]
unfolding infdist_def
[PROOF STATE]
proof (prove)
using this:
dist y p \<le> Inf (dist y ` A)

goal (1 subgoal):
 1. dist y p \<le> (if A = {} then 0 else Inf (dist y ` A))
[PROOF STEP]
using \<open>p \<in> A\<close>
[PROOF STATE]
proof (prove)
using this:
dist y p \<le> Inf (dist y ` A)
p \<in> A

goal (1 subgoal):
 1. dist y p \<le> (if A = {} then 0 else Inf (dist y ` A))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist y p \<le> infdist y A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proj_set_subset:
  assumes "p \<in> proj_set x A" "geodesic_segment_between G p x" "y \<in> G"
  shows "proj_set y A \<subseteq> proj_set x A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proj_set y A \<subseteq> proj_set x A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. proj_set y A \<subseteq> proj_set x A
[PROOF STEP]
have "z \<in> proj_set x A" if "z \<in> proj_set y A" for z
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<in> proj_set x A
[PROOF STEP]
proof (rule proj_setI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. z \<in> A
 2. dist x z \<le> infdist x A
[PROOF STEP]
show "z \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<in> A
[PROOF STEP]
using that proj_setD
[PROOF STATE]
proof (prove)
using this:
z \<in> proj_set y A
?y \<in> proj_set ?x ?A \<Longrightarrow> ?y \<in> ?A
?y \<in> proj_set ?x ?A \<Longrightarrow> dist ?x ?y = infdist ?x ?A

goal (1 subgoal):
 1. z \<in> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<in> A

goal (1 subgoal):
 1. dist x z \<le> infdist x A
[PROOF STEP]
have "dist x z \<le> dist x y + dist y z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist x z \<le> dist x y + dist y z
[PROOF STEP]
by (intro mono_intros)
[PROOF STATE]
proof (state)
this:
dist x z \<le> dist x y + dist y z

goal (1 subgoal):
 1. dist x z \<le> infdist x A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist x z \<le> dist x y + dist y z

goal (1 subgoal):
 1. dist x z \<le> infdist x A
[PROOF STEP]
have "... \<le> dist x y + dist y p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist x y + dist y z \<le> dist x y + dist y p
[PROOF STEP]
using proj_set_dist_le[OF proj_setD(1)[OF \<open>p \<in> proj_set x A\<close>] that]
[PROOF STATE]
proof (prove)
using this:
dist y z \<le> dist y p

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

goal (1 subgoal):
 1. dist x z \<le> infdist x A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist x y + dist y z \<le> dist x y + dist y p

goal (1 subgoal):
 1. dist x z \<le> infdist x A
[PROOF STEP]
have "... = dist x p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist x y + dist y p = dist x p
[PROOF STEP]
using assms geodesic_segment_commute geodesic_segment_dist
[PROOF STATE]
proof (prove)
using this:
p \<in> proj_set x A
geodesic_segment_between G p x
y \<in> G
geodesic_segment_between ?G ?x ?y \<Longrightarrow> geodesic_segment_between ?G ?y ?x
\<lbrakk>geodesic_segment_between ?G ?x ?y; ?a \<in> ?G\<rbrakk> \<Longrightarrow> dist ?x ?a + dist ?a ?y = dist ?x ?y

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

goal (1 subgoal):
 1. dist x z \<le> infdist x A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist x y + dist y p = dist x p

goal (1 subgoal):
 1. dist x z \<le> infdist x A
[PROOF STEP]
have "... = infdist x A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist x p = infdist x A
[PROOF STEP]
using proj_setD(2)[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
dist x p = infdist x A

goal (1 subgoal):
 1. dist x p = infdist x A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dist x p = infdist x A

goal (1 subgoal):
 1. dist x z \<le> infdist x A
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist x z \<le> infdist x A
[PROOF STEP]
show "dist x z \<le> infdist x A"
[PROOF STATE]
proof (prove)
using this:
dist x z \<le> infdist x A

goal (1 subgoal):
 1. dist x z \<le> infdist x A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dist x z \<le> infdist x A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?z \<in> proj_set y A \<Longrightarrow> ?z \<in> proj_set x A

goal (1 subgoal):
 1. proj_set y A \<subseteq> proj_set x A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?z \<in> proj_set y A \<Longrightarrow> ?z \<in> proj_set x A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?z \<in> proj_set y A \<Longrightarrow> ?z \<in> proj_set x A

goal (1 subgoal):
 1. proj_set y A \<subseteq> proj_set x A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
proj_set y A \<subseteq> proj_set x A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proj_set_thickening:
  assumes "p \<in> proj_set x Z"
          "0 \<le> D"
          "D \<le> dist p x"
          "geodesic_segment_between G p x"
  shows "geodesic_segment_param G p D \<in> proj_set x (\<Union>z\<in>Z. cball z D)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_param G p D \<in> proj_set x (\<Union>z\<in>Z. cball z D)
[PROOF STEP]
proof (rule proj_setI')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. geodesic_segment_param G p D \<in> (\<Union>z\<in>Z. cball z D)
 2. \<And>z. z \<in> (\<Union>z\<in>Z. cball z D) \<Longrightarrow> dist x (geodesic_segment_param G p D) \<le> dist x z
[PROOF STEP]
have "dist p (geodesic_segment_param G p D) = D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist p (geodesic_segment_param G p D) = D
[PROOF STEP]
using geodesic_segment_param(7)[OF assms(4), of 0 D]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 \<in> {0..dist p x}; D \<in> {0..dist p x}\<rbrakk> \<Longrightarrow> dist (geodesic_segment_param G p 0) (geodesic_segment_param G p D) = \<bar>0 - D\<bar>

goal (1 subgoal):
 1. dist p (geodesic_segment_param G p D) = D
[PROOF STEP]
unfolding geodesic_segment_param(1)[OF assms(4)]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 \<in> {0..dist p x}; D \<in> {0..dist p x}\<rbrakk> \<Longrightarrow> dist p (geodesic_segment_param G p D) = \<bar>0 - D\<bar>

goal (1 subgoal):
 1. dist p (geodesic_segment_param G p D) = D
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 \<in> {0..dist p x}; D \<in> {0..dist p x}\<rbrakk> \<Longrightarrow> dist p (geodesic_segment_param G p D) = \<bar>0 - D\<bar>
p \<in> proj_set x Z
0 \<le> D
D \<le> dist p x
geodesic_segment_between G p x

goal (1 subgoal):
 1. dist p (geodesic_segment_param G p D) = D
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dist p (geodesic_segment_param G p D) = D

goal (2 subgoals):
 1. geodesic_segment_param G p D \<in> (\<Union>z\<in>Z. cball z D)
 2. \<And>z. z \<in> (\<Union>z\<in>Z. cball z D) \<Longrightarrow> dist x (geodesic_segment_param G p D) \<le> dist x z
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dist p (geodesic_segment_param G p D) = D
[PROOF STEP]
show "geodesic_segment_param G p D \<in> (\<Union>z\<in>Z. cball z D)"
[PROOF STATE]
proof (prove)
using this:
dist p (geodesic_segment_param G p D) = D

goal (1 subgoal):
 1. geodesic_segment_param G p D \<in> (\<Union>z\<in>Z. cball z D)
[PROOF STEP]
using proj_setD(1)[OF \<open>p \<in> proj_set x Z\<close>]
[PROOF STATE]
proof (prove)
using this:
dist p (geodesic_segment_param G p D) = D
p \<in> Z

goal (1 subgoal):
 1. geodesic_segment_param G p D \<in> (\<Union>z\<in>Z. cball z D)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
geodesic_segment_param G p D \<in> (\<Union>z\<in>Z. cball z D)

goal (1 subgoal):
 1. \<And>z. z \<in> (\<Union>z\<in>Z. cball z D) \<Longrightarrow> dist x (geodesic_segment_param G p D) \<le> dist x z
[PROOF STEP]
show "dist x (geodesic_segment_param G p D) \<le> dist x y" if "y \<in> (\<Union>z\<in>Z. cball z D)" for y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist x (geodesic_segment_param G p D) \<le> dist x y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist x (geodesic_segment_param G p D) \<le> dist x y
[PROOF STEP]
obtain z where y: "y \<in> cball z D" "z \<in> Z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>z. \<lbrakk>y \<in> cball z D; z \<in> Z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>y \<in> (\<Union>z\<in>Z. cball z D)\<close>
[PROOF STATE]
proof (prove)
using this:
y \<in> (\<Union>z\<in>Z. cball z D)

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>y \<in> cball z D; z \<in> Z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> cball z D
z \<in> Z

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

goal (1 subgoal):
 1. dist (geodesic_segment_param G p D) x + D = dist p x
[PROOF STEP]
unfolding geodesic_segment_param(2)[OF assms(4)]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>D \<in> {0..dist p x}; dist p x \<in> {0..dist p x}\<rbrakk> \<Longrightarrow> dist (geodesic_segment_param G p D) x = \<bar>D - dist p x\<bar>

goal (1 subgoal):
 1. dist (geodesic_segment_param G p D) x + D = dist p x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>D \<in> {0..dist p x}; dist p x \<in> {0..dist p x}\<rbrakk> \<Longrightarrow> dist (geodesic_segment_param G p D) x = \<bar>D - dist p x\<bar>
p \<in> proj_set x Z
0 \<le> D
D \<le> dist p x
geodesic_segment_between G p x

goal (1 subgoal):
 1. dist (geodesic_segment_param G p D) x + D = dist p x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dist (geodesic_segment_param G p D) x + D = dist p x

goal (1 subgoal):
 1. dist x (geodesic_segment_param G p D) \<le> dist x y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (geodesic_segment_param G p D) x + D = dist p x

goal (1 subgoal):
 1. dist x (geodesic_segment_param G p D) \<le> dist x y
[PROOF STEP]
have "... \<le> dist z x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist p x \<le> dist z x
[PROOF STEP]
using proj_setD(2)[OF \<open>p \<in> proj_set x Z\<close>] infdist_le[OF \<open>z \<in> Z\<close>, of x]
[PROOF STATE]
proof (prove)
using this:
dist x p = infdist x Z
infdist x Z \<le> dist x z

goal (1 subgoal):
 1. dist p x \<le> dist z x
[PROOF STEP]
by (simp add: dist_commute)
[PROOF STATE]
proof (state)
this:
dist p x \<le> dist z x

goal (1 subgoal):
 1. dist x (geodesic_segment_param G p D) \<le> dist x y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist p x \<le> dist z x

goal (1 subgoal):
 1. dist x (geodesic_segment_param G p D) \<le> dist x y
[PROOF STEP]
have "... \<le> dist z y + dist y x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist z x \<le> dist z y + dist y x
[PROOF STEP]
by (intro mono_intros)
[PROOF STATE]
proof (state)
this:
dist z x \<le> dist z y + dist y x

goal (1 subgoal):
 1. dist x (geodesic_segment_param G p D) \<le> dist x y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist z x \<le> dist z y + dist y x

goal (1 subgoal):
 1. dist x (geodesic_segment_param G p D) \<le> dist x y
[PROOF STEP]
have "... \<le> D + dist y x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist z y + dist y x \<le> D + dist y x
[PROOF STEP]
using y
[PROOF STATE]
proof (prove)
using this:
y \<in> cball z D
z \<in> Z

goal (1 subgoal):
 1. dist z y + dist y x \<le> D + dist y x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dist z y + dist y x \<le> D + dist y x

goal (1 subgoal):
 1. dist x (geodesic_segment_param G p D) \<le> dist x y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist (geodesic_segment_param G p D) x + D \<le> D + dist y x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dist (geodesic_segment_param G p D) x + D \<le> D + dist y x

goal (1 subgoal):
 1. dist x (geodesic_segment_param G p D) \<le> dist x y
[PROOF STEP]
by (simp add: dist_commute)
[PROOF STATE]
proof (state)
this:
dist x (geodesic_segment_param G p D) \<le> dist x y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?y \<in> (\<Union>z\<in>Z. cball z D) \<Longrightarrow> dist x (geodesic_segment_param G p D) \<le> dist x ?y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma proj_set_thickening':
  assumes "p \<in> proj_set x Z"
          "0 \<le> D"
          "D \<le> E"
          "E \<le> dist p x"
          "geodesic_segment_between G p x"
  shows "geodesic_segment_param G p D \<in> proj_set (geodesic_segment_param G p E) (\<Union>z\<in>Z. cball z D)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_param G p D \<in> proj_set (geodesic_segment_param G p E) (\<Union>z\<in>Z. cball z D)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. geodesic_segment_param G p D \<in> proj_set (geodesic_segment_param G p E) (\<Union>z\<in>Z. cball z D)
[PROOF STEP]
define H where "H = geodesic_subsegment G p D (dist p x)"
[PROOF STATE]
proof (state)
this:
H = geodesic_subsegment G p D (dist p x)

goal (1 subgoal):
 1. geodesic_segment_param G p D \<in> proj_set (geodesic_segment_param G p E) (\<Union>z\<in>Z. cball z D)
[PROOF STEP]
have H1: "geodesic_segment_between H (geodesic_segment_param G p D) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_between H (geodesic_segment_param G p D) x
[PROOF STEP]
apply (subst geodesic_segment_param(2)[OF \<open>geodesic_segment_between G p x\<close>, symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_between H (geodesic_segment_param G p D) (geodesic_segment_param G p (dist p x))
[PROOF STEP]
unfolding H_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_between (geodesic_subsegment G p D (dist p x)) (geodesic_segment_param G p D) (geodesic_segment_param G p (dist p x))
[PROOF STEP]
apply (rule geodesic_subsegment(2))
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. geodesic_segment_between G p ?y
 2. 0 \<le> D
 3. D \<le> dist p x
 4. dist p x \<le> dist p ?y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
p \<in> proj_set x Z
0 \<le> D
D \<le> E
E \<le> dist p x
geodesic_segment_between G p x

goal (4 subgoals):
 1. geodesic_segment_between G p ?y
 2. 0 \<le> D
 3. D \<le> dist p x
 4. dist p x \<le> dist p ?y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
geodesic_segment_between H (geodesic_segment_param G p D) x

goal (1 subgoal):
 1. geodesic_segment_param G p D \<in> proj_set (geodesic_segment_param G p E) (\<Union>z\<in>Z. cball z D)
[PROOF STEP]
have H2: "geodesic_segment_param G p E \<in> H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_param G p E \<in> H
[PROOF STEP]
unfolding H_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_param G p E \<in> geodesic_subsegment G p D (dist p x)
[PROOF STEP]
using assms geodesic_subsegment(1)
[PROOF STATE]
proof (prove)
using this:
p \<in> proj_set x Z
0 \<le> D
D \<le> E
E \<le> dist p x
geodesic_segment_between G p x
\<lbrakk>geodesic_segment_between ?G ?x ?y; 0 \<le> ?s; ?s \<le> ?t; ?t \<le> dist ?x ?y\<rbrakk> \<Longrightarrow> geodesic_subsegment ?G ?x ?s ?t = geodesic_segment_param ?G ?x ` {?s..?t}

goal (1 subgoal):
 1. geodesic_segment_param G p E \<in> geodesic_subsegment G p D (dist p x)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
geodesic_segment_param G p E \<in> H

goal (1 subgoal):
 1. geodesic_segment_param G p D \<in> proj_set (geodesic_segment_param G p E) (\<Union>z\<in>Z. cball z D)
[PROOF STEP]
have "geodesic_segment_param G p D \<in> proj_set x (\<Union>z\<in>Z. cball z D)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_param G p D \<in> proj_set x (\<Union>z\<in>Z. cball z D)
[PROOF STEP]
apply (rule proj_set_thickening)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. p \<in> proj_set x Z
 2. 0 \<le> D
 3. D \<le> dist p x
 4. geodesic_segment_between G p x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
p \<in> proj_set x Z
0 \<le> D
D \<le> E
E \<le> dist p x
geodesic_segment_between G p x

goal (4 subgoals):
 1. p \<in> proj_set x Z
 2. 0 \<le> D
 3. D \<le> dist p x
 4. geodesic_segment_between G p x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
geodesic_segment_param G p D \<in> proj_set x (\<Union>z\<in>Z. cball z D)

goal (1 subgoal):
 1. geodesic_segment_param G p D \<in> proj_set (geodesic_segment_param G p E) (\<Union>z\<in>Z. cball z D)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
geodesic_segment_param G p D \<in> proj_set x (\<Union>z\<in>Z. cball z D)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_param G p D \<in> proj_set x (\<Union>z\<in>Z. cball z D)

goal (1 subgoal):
 1. geodesic_segment_param G p D \<in> proj_set (geodesic_segment_param G p E) (\<Union>z\<in>Z. cball z D)
[PROOF STEP]
by (rule proj_set_geodesic_same_basepoint[OF _ H1 H2])
[PROOF STATE]
proof (state)
this:
geodesic_segment_param G p D \<in> proj_set (geodesic_segment_param G p E) (\<Union>z\<in>Z. cball z D)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma some_geodesic_segment_between_exists:
  "\<exists>f. \<forall> x y S. f x S y = f y S x
    \<and> (if (\<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S) then (geodesic_segment_between (f x S y) x y \<and> (f x S y \<subseteq> S))
        else f x S y = {x, y})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f. \<forall>x y S. f x S y = f y S x \<and> (if \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S then geodesic_segment_between (f x S y) x y \<and> f x S y \<subseteq> S else f x S y = {x, y})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>f. \<forall>x y S. f x S y = f y S x \<and> (if \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S then geodesic_segment_between (f x S y) x y \<and> f x S y \<subseteq> S else f x S y = {x, y})
[PROOF STEP]
define g::"'a \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'a set" where
    "g = (\<lambda>x S y. if (\<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S) then (SOME G. geodesic_segment_between G x y \<and> G \<subseteq> S) else {x, y})"
[PROOF STATE]
proof (state)
this:
g = (\<lambda>x S y. if \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S then SOME G. geodesic_segment_between G x y \<and> G \<subseteq> S else {x, y})

goal (1 subgoal):
 1. \<exists>f. \<forall>x y S. f x S y = f y S x \<and> (if \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S then geodesic_segment_between (f x S y) x y \<and> f x S y \<subseteq> S else f x S y = {x, y})
[PROOF STEP]
have g1: "geodesic_segment_between (g x S y) x y \<and> (g x S y \<subseteq> S)" if "\<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S" for x y S
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_between (g x S y) x y \<and> g x S y \<subseteq> S
[PROOF STEP]
unfolding g_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_between (if \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S then SOME G. geodesic_segment_between G x y \<and> G \<subseteq> S else {x, y}) x y \<and> (if \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S then SOME G. geodesic_segment_between G x y \<and> G \<subseteq> S else {x, y}) \<subseteq> S
[PROOF STEP]
using someI_ex[OF that]
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_between (SOME xa. geodesic_segment_between xa x y \<and> xa \<subseteq> S) x y \<and> (SOME xa. geodesic_segment_between xa x y \<and> xa \<subseteq> S) \<subseteq> S

goal (1 subgoal):
 1. geodesic_segment_between (if \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S then SOME G. geodesic_segment_between G x y \<and> G \<subseteq> S else {x, y}) x y \<and> (if \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S then SOME G. geodesic_segment_between G x y \<and> G \<subseteq> S else {x, y}) \<subseteq> S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>G. geodesic_segment_between G ?x ?y \<and> G \<subseteq> ?S \<Longrightarrow> geodesic_segment_between (g ?x ?S ?y) ?x ?y \<and> g ?x ?S ?y \<subseteq> ?S

goal (1 subgoal):
 1. \<exists>f. \<forall>x y S. f x S y = f y S x \<and> (if \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S then geodesic_segment_between (f x S y) x y \<and> f x S y \<subseteq> S else f x S y = {x, y})
[PROOF STEP]
have g2: "g x S y = {x, y}" if "\<not>(\<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S)" for x y S
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g x S y = {x, y}
[PROOF STEP]
unfolding g_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S then SOME G. geodesic_segment_between G x y \<and> G \<subseteq> S else {x, y}) = {x, y}
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<nexists>G. geodesic_segment_between G x y \<and> G \<subseteq> S

goal (1 subgoal):
 1. (if \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S then SOME G. geodesic_segment_between G x y \<and> G \<subseteq> S else {x, y}) = {x, y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<nexists>G. geodesic_segment_between G ?x ?y \<and> G \<subseteq> ?S \<Longrightarrow> g ?x ?S ?y = {?x, ?y}

goal (1 subgoal):
 1. \<exists>f. \<forall>x y S. f x S y = f y S x \<and> (if \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S then geodesic_segment_between (f x S y) x y \<and> f x S y \<subseteq> S else f x S y = {x, y})
[PROOF STEP]
obtain r::"'a rel" where r: "well_order_on UNIV r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>r. well_order r \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using well_order_on
[PROOF STATE]
proof (prove)
using this:
\<exists>r. well_order_on ?A r

goal (1 subgoal):
 1. (\<And>r. well_order r \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
well_order r

goal (1 subgoal):
 1. \<exists>f. \<forall>x y S. f x S y = f y S x \<and> (if \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S then geodesic_segment_between (f x S y) x y \<and> f x S y \<subseteq> S else f x S y = {x, y})
[PROOF STEP]
have A: "x = y" if "(x, y) \<in> r" "(y, x) \<in> r" for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
using r that
[PROOF STATE]
proof (prove)
using this:
well_order r
(x, y) \<in> r
(y, x) \<in> r

goal (1 subgoal):
 1. x = y
[PROOF STEP]
unfolding well_order_on_def linear_order_on_def partial_order_on_def antisym_def
[PROOF STATE]
proof (prove)
using this:
((preorder_on UNIV r \<and> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r \<longrightarrow> x = y)) \<and> total r) \<and> wf (r - Id)
(x, y) \<in> r
(y, x) \<in> r

goal (1 subgoal):
 1. x = y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?x, ?y) \<in> r; (?y, ?x) \<in> r\<rbrakk> \<Longrightarrow> ?x = ?y

goal (1 subgoal):
 1. \<exists>f. \<forall>x y S. f x S y = f y S x \<and> (if \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S then geodesic_segment_between (f x S y) x y \<and> f x S y \<subseteq> S else f x S y = {x, y})
[PROOF STEP]
have B: "(x, y) \<in> r \<or> (y, x) \<in> r" for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> r \<or> (y, x) \<in> r
[PROOF STEP]
using r
[PROOF STATE]
proof (prove)
using this:
well_order r

goal (1 subgoal):
 1. (x, y) \<in> r \<or> (y, x) \<in> r
[PROOF STEP]
unfolding well_order_on_def linear_order_on_def total_on_def partial_order_on_def preorder_on_def refl_on_def
[PROOF STATE]
proof (prove)
using this:
((((r \<subseteq> UNIV \<times> UNIV \<and> (\<forall>x\<in>UNIV. (x, x) \<in> r)) \<and> trans r) \<and> antisym r) \<and> (\<forall>x\<in>UNIV. \<forall>y\<in>UNIV. x \<noteq> y \<longrightarrow> (x, y) \<in> r \<or> (y, x) \<in> r)) \<and> wf (r - Id)

goal (1 subgoal):
 1. (x, y) \<in> r \<or> (y, x) \<in> r
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(?x, ?y) \<in> r \<or> (?y, ?x) \<in> r

goal (1 subgoal):
 1. \<exists>f. \<forall>x y S. f x S y = f y S x \<and> (if \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S then geodesic_segment_between (f x S y) x y \<and> f x S y \<subseteq> S else f x S y = {x, y})
[PROOF STEP]
define f where "f = (\<lambda>x S y. if (x, y) \<in> r then g x S y else g y S x)"
[PROOF STATE]
proof (state)
this:
f = (\<lambda>x S y. if (x, y) \<in> r then g x S y else g y S x)

goal (1 subgoal):
 1. \<exists>f. \<forall>x y S. f x S y = f y S x \<and> (if \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S then geodesic_segment_between (f x S y) x y \<and> f x S y \<subseteq> S else f x S y = {x, y})
[PROOF STEP]
have "f x S y = f y S x" for x y S
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f x S y = f y S x
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if (x, y) \<in> r then g x S y else g y S x) = (if (y, x) \<in> r then g y S x else g x S y)
[PROOF STEP]
using r A B
[PROOF STATE]
proof (prove)
using this:
well_order r
\<lbrakk>(?x, ?y) \<in> r; (?y, ?x) \<in> r\<rbrakk> \<Longrightarrow> ?x = ?y
(?x, ?y) \<in> r \<or> (?y, ?x) \<in> r

goal (1 subgoal):
 1. (if (x, y) \<in> r then g x S y else g y S x) = (if (y, x) \<in> r then g y S x else g x S y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f ?x ?S ?y = f ?y ?S ?x

goal (1 subgoal):
 1. \<exists>f. \<forall>x y S. f x S y = f y S x \<and> (if \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S then geodesic_segment_between (f x S y) x y \<and> f x S y \<subseteq> S else f x S y = {x, y})
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f ?x ?S ?y = f ?y ?S ?x

goal (1 subgoal):
 1. \<exists>f. \<forall>x y S. f x S y = f y S x \<and> (if \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S then geodesic_segment_between (f x S y) x y \<and> f x S y \<subseteq> S else f x S y = {x, y})
[PROOF STEP]
have "geodesic_segment_between (f x S y) x y \<and> (f x S y \<subseteq> S)" if "\<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S" for x y S
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_between (f x S y) x y \<and> f x S y \<subseteq> S
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_between (if (x, y) \<in> r then g x S y else g y S x) x y \<and> (if (x, y) \<in> r then g x S y else g y S x) \<subseteq> S
[PROOF STEP]
using g1 geodesic_segment_commute that
[PROOF STATE]
proof (prove)
using this:
\<exists>G. geodesic_segment_between G ?x ?y \<and> G \<subseteq> ?S \<Longrightarrow> geodesic_segment_between (g ?x ?S ?y) ?x ?y \<and> g ?x ?S ?y \<subseteq> ?S
geodesic_segment_between ?G ?x ?y \<Longrightarrow> geodesic_segment_between ?G ?y ?x
\<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S

goal (1 subgoal):
 1. geodesic_segment_between (if (x, y) \<in> r then g x S y else g y S x) x y \<and> (if (x, y) \<in> r then g x S y else g y S x) \<subseteq> S
[PROOF STEP]
by smt
[PROOF STATE]
proof (state)
this:
\<exists>G. geodesic_segment_between G ?x ?y \<and> G \<subseteq> ?S \<Longrightarrow> geodesic_segment_between (f ?x ?S ?y) ?x ?y \<and> f ?x ?S ?y \<subseteq> ?S

goal (1 subgoal):
 1. \<exists>f. \<forall>x y S. f x S y = f y S x \<and> (if \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S then geodesic_segment_between (f x S y) x y \<and> f x S y \<subseteq> S else f x S y = {x, y})
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>G. geodesic_segment_between G ?x ?y \<and> G \<subseteq> ?S \<Longrightarrow> geodesic_segment_between (f ?x ?S ?y) ?x ?y \<and> f ?x ?S ?y \<subseteq> ?S

goal (1 subgoal):
 1. \<exists>f. \<forall>x y S. f x S y = f y S x \<and> (if \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S then geodesic_segment_between (f x S y) x y \<and> f x S y \<subseteq> S else f x S y = {x, y})
[PROOF STEP]
have "f x S y = {x, y}" if "\<not>(\<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S)" for x y S
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f x S y = {x, y}
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if (x, y) \<in> r then g x S y else g y S x) = {x, y}
[PROOF STEP]
using g2 that geodesic_segment_commute doubleton_eq_iff
[PROOF STATE]
proof (prove)
using this:
\<nexists>G. geodesic_segment_between G ?x ?y \<and> G \<subseteq> ?S \<Longrightarrow> g ?x ?S ?y = {?x, ?y}
\<nexists>G. geodesic_segment_between G x y \<and> G \<subseteq> S
geodesic_segment_between ?G ?x ?y \<Longrightarrow> geodesic_segment_between ?G ?y ?x
({?a, ?b} = {?c, ?d}) = (?a = ?c \<and> ?b = ?d \<or> ?a = ?d \<and> ?b = ?c)

goal (1 subgoal):
 1. (if (x, y) \<in> r then g x S y else g y S x) = {x, y}
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<nexists>G. geodesic_segment_between G ?x ?y \<and> G \<subseteq> ?S \<Longrightarrow> f ?x ?S ?y = {?x, ?y}

goal (1 subgoal):
 1. \<exists>f. \<forall>x y S. f x S y = f y S x \<and> (if \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S then geodesic_segment_between (f x S y) x y \<and> f x S y \<subseteq> S else f x S y = {x, y})
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f ?x ?S ?y = f ?y ?S ?x
\<exists>G. geodesic_segment_between G ?x ?y \<and> G \<subseteq> ?S \<Longrightarrow> geodesic_segment_between (f ?x ?S ?y) ?x ?y \<and> f ?x ?S ?y \<subseteq> ?S
\<nexists>G. geodesic_segment_between G ?x ?y \<and> G \<subseteq> ?S \<Longrightarrow> f ?x ?S ?y = {?x, ?y}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f ?x ?S ?y = f ?y ?S ?x
\<exists>G. geodesic_segment_between G ?x ?y \<and> G \<subseteq> ?S \<Longrightarrow> geodesic_segment_between (f ?x ?S ?y) ?x ?y \<and> f ?x ?S ?y \<subseteq> ?S
\<nexists>G. geodesic_segment_between G ?x ?y \<and> G \<subseteq> ?S \<Longrightarrow> f ?x ?S ?y = {?x, ?y}

goal (1 subgoal):
 1. \<exists>f. \<forall>x y S. f x S y = f y S x \<and> (if \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S then geodesic_segment_between (f x S y) x y \<and> f x S y \<subseteq> S else f x S y = {x, y})
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>f. \<forall>x y S. f x S y = f y S x \<and> (if \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S then geodesic_segment_between (f x S y) x y \<and> f x S y \<subseteq> S else f x S y = {x, y})

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma some_geodesic_commute:
  "{x--S--y} = {y--S--x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x--S--y} = {y--S--x}
[PROOF STEP]
unfolding some_geodesic_segment_between_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SOME f. \<forall>x y S. f x S y = f y S x \<and> (if \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S then geodesic_segment_between (f x S y) x y \<and> f x S y \<subseteq> S else f x S y = {x, y})) x S y = (SOME f. \<forall>x y S. f x S y = f y S x \<and> (if \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S then geodesic_segment_between (f x S y) x y \<and> f x S y \<subseteq> S else f x S y = {x, y})) y S x
[PROOF STEP]
by (auto simp add: someI_ex[OF some_geodesic_segment_between_exists])