[STATEMENT]
lemma some_geodesic_segment_description:
  "(\<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S) \<Longrightarrow> geodesic_segment_between {x--S--y} x y"
  "(\<not>(\<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S)) \<Longrightarrow> {x--S--y} = {x, y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S \<Longrightarrow> geodesic_segment_between {x--S--y} x y) &&& (\<nexists>G. geodesic_segment_between G x y \<and> G \<subseteq> S \<Longrightarrow> {x--S--y} = {x, y})
[PROOF STEP]
unfolding some_geodesic_segment_between_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S \<Longrightarrow> geodesic_segment_between ((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) x y) &&& (\<nexists>G. geodesic_segment_between G x y \<and> G \<subseteq> S \<Longrightarrow> (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 = {x, y})
[PROOF STEP]
by (simp add: someI_ex[OF some_geodesic_segment_between_exists])+


[STATEMENT]
lemma some_geodesic_compact [simp]:
  "compact {x--S--y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. compact {x--S--y}
[PROOF STEP]
apply (cases "\<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S \<Longrightarrow> compact {x--S--y}
 2. \<nexists>G. geodesic_segment_between G x y \<and> G \<subseteq> S \<Longrightarrow> compact {x--S--y}
[PROOF STEP]
using some_geodesic_segment_description[of x y] geodesic_segment_topology[of "{x--S--y}"] geodesic_segment_def
[PROOF STATE]
proof (prove)
using this:
\<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> ?S \<Longrightarrow> geodesic_segment_between {x--?S--y} x y
\<nexists>G. geodesic_segment_between G x y \<and> G \<subseteq> ?S \<Longrightarrow> {x--?S--y} = {x, y}
geodesic_segment {x--S--y} \<Longrightarrow> compact {x--S--y}
geodesic_segment {x--S--y} \<Longrightarrow> connected {x--S--y}
geodesic_segment {x--S--y} \<Longrightarrow> path_connected {x--S--y}
geodesic_segment {x--S--y} \<Longrightarrow> bounded {x--S--y}
geodesic_segment {x--S--y} \<Longrightarrow> closed {x--S--y}
geodesic_segment {x--S--y} \<Longrightarrow> {x--S--y} \<noteq> {}
geodesic_segment {x--S--y} \<Longrightarrow> proper {x--S--y}
geodesic_segment ?G = (\<exists>x y. geodesic_segment_between ?G x y)

goal (2 subgoals):
 1. \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S \<Longrightarrow> compact {x--S--y}
 2. \<nexists>G. geodesic_segment_between G x y \<and> G \<subseteq> S \<Longrightarrow> compact {x--S--y}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>G. \<lbrakk>\<And>S. \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S \<Longrightarrow> geodesic_segment_between {x--S--y} x y; \<And>S. \<forall>G. geodesic_segment_between G x y \<longrightarrow> \<not> G \<subseteq> S \<Longrightarrow> {x--S--y} = {x, y}; geodesic_segment {x--S--y} \<Longrightarrow> compact {x--S--y}; geodesic_segment {x--S--y} \<Longrightarrow> connected {x--S--y}; geodesic_segment {x--S--y} \<Longrightarrow> path_connected {x--S--y}; geodesic_segment {x--S--y} \<Longrightarrow> bounded {x--S--y}; geodesic_segment {x--S--y} \<Longrightarrow> closed {x--S--y}; geodesic_segment {x--S--y} \<Longrightarrow> {x--S--y} \<noteq> {}; geodesic_segment {x--S--y} \<Longrightarrow> proper {x--S--y}; \<And>G. geodesic_segment G = (\<exists>x y. geodesic_segment_between G x y); geodesic_segment_between G x y; G \<subseteq> S\<rbrakk> \<Longrightarrow> compact {x--S--y}
[PROOF STEP]
by blast


[STATEMENT]
lemma some_geodesic_closed [simp]:
  "closed {x--S--y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed {x--S--y}
[PROOF STEP]
by (rule compact_imp_closed[OF some_geodesic_compact[of x S y]])


[STATEMENT]
lemma some_geodesic_bounded [simp]:
  "bounded {x--S--y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded {x--S--y}
[PROOF STEP]
by (rule compact_imp_bounded[OF some_geodesic_compact[of x S y]])


[STATEMENT]
lemma some_geodesic_endpoints [simp]:
  "x \<in> {x--S--y}" "y \<in> {x--S--y}" "{x--S--y} \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> {x--S--y} &&& y \<in> {x--S--y} &&& {x--S--y} \<noteq> {}
[PROOF STEP]
apply (cases "\<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S \<Longrightarrow> x \<in> {x--S--y}
 2. \<nexists>G. geodesic_segment_between G x y \<and> G \<subseteq> S \<Longrightarrow> x \<in> {x--S--y}
 3. y \<in> {x--S--y}
 4. {x--S--y} \<noteq> {}
[PROOF STEP]
using some_geodesic_segment_description[of x y S]
[PROOF STATE]
proof (prove)
using this:
\<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S \<Longrightarrow> geodesic_segment_between {x--S--y} x y
\<nexists>G. geodesic_segment_between G x y \<and> G \<subseteq> S \<Longrightarrow> {x--S--y} = {x, y}

goal (4 subgoals):
 1. \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S \<Longrightarrow> x \<in> {x--S--y}
 2. \<nexists>G. geodesic_segment_between G x y \<and> G \<subseteq> S \<Longrightarrow> x \<in> {x--S--y}
 3. y \<in> {x--S--y}
 4. {x--S--y} \<noteq> {}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S \<Longrightarrow> geodesic_segment_between {x--S--y} x y; \<forall>G. geodesic_segment_between G x y \<longrightarrow> \<not> G \<subseteq> S \<Longrightarrow> {x--S--y} = {x, y}\<rbrakk> \<Longrightarrow> y \<in> {x--S--y}
 2. \<lbrakk>\<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S \<Longrightarrow> geodesic_segment_between {} x y; \<forall>G. geodesic_segment_between G x y \<longrightarrow> \<not> G \<subseteq> S \<Longrightarrow> False; {x--S--y} = {}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (cases "\<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S \<Longrightarrow> geodesic_segment_between {x--S--y} x y; \<forall>G. geodesic_segment_between G x y \<longrightarrow> \<not> G \<subseteq> S \<Longrightarrow> {x--S--y} = {x, y}; \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S\<rbrakk> \<Longrightarrow> y \<in> {x--S--y}
 2. \<lbrakk>\<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S \<Longrightarrow> geodesic_segment_between {x--S--y} x y; \<forall>G. geodesic_segment_between G x y \<longrightarrow> \<not> G \<subseteq> S \<Longrightarrow> {x--S--y} = {x, y}; \<nexists>G. geodesic_segment_between G x y \<and> G \<subseteq> S\<rbrakk> \<Longrightarrow> y \<in> {x--S--y}
 3. \<lbrakk>\<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S \<Longrightarrow> geodesic_segment_between {} x y; \<forall>G. geodesic_segment_between G x y \<longrightarrow> \<not> G \<subseteq> S \<Longrightarrow> False; {x--S--y} = {}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using some_geodesic_segment_description[of x y S]
[PROOF STATE]
proof (prove)
using this:
\<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S \<Longrightarrow> geodesic_segment_between {x--S--y} x y
\<nexists>G. geodesic_segment_between G x y \<and> G \<subseteq> S \<Longrightarrow> {x--S--y} = {x, y}

goal (3 subgoals):
 1. \<lbrakk>\<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S \<Longrightarrow> geodesic_segment_between {x--S--y} x y; \<forall>G. geodesic_segment_between G x y \<longrightarrow> \<not> G \<subseteq> S \<Longrightarrow> {x--S--y} = {x, y}; \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S\<rbrakk> \<Longrightarrow> y \<in> {x--S--y}
 2. \<lbrakk>\<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S \<Longrightarrow> geodesic_segment_between {x--S--y} x y; \<forall>G. geodesic_segment_between G x y \<longrightarrow> \<not> G \<subseteq> S \<Longrightarrow> {x--S--y} = {x, y}; \<nexists>G. geodesic_segment_between G x y \<and> G \<subseteq> S\<rbrakk> \<Longrightarrow> y \<in> {x--S--y}
 3. \<lbrakk>\<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S \<Longrightarrow> geodesic_segment_between {} x y; \<forall>G. geodesic_segment_between G x y \<longrightarrow> \<not> G \<subseteq> S \<Longrightarrow> False; {x--S--y} = {}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S \<Longrightarrow> geodesic_segment_between {} x y; \<forall>G. geodesic_segment_between G x y \<longrightarrow> \<not> G \<subseteq> S \<Longrightarrow> False; {x--S--y} = {}; \<forall>G. geodesic_segment_between G x y \<longrightarrow> \<not> G \<subseteq> S \<Longrightarrow> False\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (cases "\<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S \<Longrightarrow> geodesic_segment_between {} x y; \<forall>G. geodesic_segment_between G x y \<longrightarrow> \<not> G \<subseteq> S \<Longrightarrow> False; {x--S--y} = {}; \<forall>G. geodesic_segment_between G x y \<longrightarrow> \<not> G \<subseteq> S \<Longrightarrow> False; \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>\<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S \<Longrightarrow> geodesic_segment_between {} x y; \<forall>G. geodesic_segment_between G x y \<longrightarrow> \<not> G \<subseteq> S \<Longrightarrow> False; {x--S--y} = {}; \<forall>G. geodesic_segment_between G x y \<longrightarrow> \<not> G \<subseteq> S \<Longrightarrow> False; \<nexists>G. geodesic_segment_between G x y \<and> G \<subseteq> S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using geodesic_segment_endpoints(3)
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_between ?G ?x ?y \<Longrightarrow> ?G \<noteq> {}

goal (2 subgoals):
 1. \<lbrakk>\<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S \<Longrightarrow> geodesic_segment_between {} x y; \<forall>G. geodesic_segment_between G x y \<longrightarrow> \<not> G \<subseteq> S \<Longrightarrow> False; {x--S--y} = {}; \<forall>G. geodesic_segment_between G x y \<longrightarrow> \<not> G \<subseteq> S \<Longrightarrow> False; \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>\<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S \<Longrightarrow> geodesic_segment_between {} x y; \<forall>G. geodesic_segment_between G x y \<longrightarrow> \<not> G \<subseteq> S \<Longrightarrow> False; {x--S--y} = {}; \<forall>G. geodesic_segment_between G x y \<longrightarrow> \<not> G \<subseteq> S \<Longrightarrow> False; \<nexists>G. geodesic_segment_between G x y \<and> G \<subseteq> S\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (auto, blast)


[STATEMENT]
lemma some_geodesic_subsegment:
  assumes "H \<subseteq> {x--S--y}" "compact H" "connected H" "H \<noteq> {}"
  shows "geodesic_segment H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment H
[PROOF STEP]
apply (cases "\<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S \<Longrightarrow> geodesic_segment H
 2. \<nexists>G. geodesic_segment_between G x y \<and> G \<subseteq> S \<Longrightarrow> geodesic_segment H
[PROOF STEP]
using some_geodesic_segment_description[of x y] geodesic_segment_subsegment[OF _ assms] geodesic_segment_def
[PROOF STATE]
proof (prove)
using this:
\<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> ?S \<Longrightarrow> geodesic_segment_between {x--?S--y} x y
\<nexists>G. geodesic_segment_between G x y \<and> G \<subseteq> ?S \<Longrightarrow> {x--?S--y} = {x, y}
geodesic_segment {x--S--y} \<Longrightarrow> geodesic_segment H
geodesic_segment ?G = (\<exists>x y. geodesic_segment_between ?G x y)

goal (2 subgoals):
 1. \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S \<Longrightarrow> geodesic_segment H
 2. \<nexists>G. geodesic_segment_between G x y \<and> G \<subseteq> S \<Longrightarrow> geodesic_segment H
[PROOF STEP]
apply auto[1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>G. geodesic_segment_between G x y \<and> G \<subseteq> S \<Longrightarrow> geodesic_segment H
[PROOF STEP]
using some_geodesic_segment_description[of x y] assms
[PROOF STATE]
proof (prove)
using this:
\<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> ?S \<Longrightarrow> geodesic_segment_between {x--?S--y} x y
\<nexists>G. geodesic_segment_between G x y \<and> G \<subseteq> ?S \<Longrightarrow> {x--?S--y} = {x, y}
H \<subseteq> {x--S--y}
compact H
connected H
H \<noteq> {}

goal (1 subgoal):
 1. \<nexists>G. geodesic_segment_between G x y \<and> G \<subseteq> S \<Longrightarrow> geodesic_segment H
[PROOF STEP]
by (metis connected_finite_iff_sing finite.emptyI finite.insertI finite_subset geodesic_segment_between_x_x(2))


[STATEMENT]
lemma some_geodesic_in_subset:
  assumes "x \<in> S" "y \<in> S"
  shows "{x--S--y} \<subseteq> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x--S--y} \<subseteq> S
[PROOF STEP]
apply (cases "\<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S \<Longrightarrow> {x--S--y} \<subseteq> S
 2. \<nexists>G. geodesic_segment_between G x y \<and> G \<subseteq> S \<Longrightarrow> {x--S--y} \<subseteq> S
[PROOF STEP]
unfolding some_geodesic_segment_between_def
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S \<Longrightarrow> (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 \<subseteq> S
 2. \<nexists>G. geodesic_segment_between G x y \<and> G \<subseteq> S \<Longrightarrow> (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 \<subseteq> S
[PROOF STEP]
by (simp add: assms someI_ex[OF some_geodesic_segment_between_exists])+


[STATEMENT]
lemma some_geodesic_same_endpoints [simp]:
  "{x--S--x} = {x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x--S--x} = {x}
[PROOF STEP]
apply (cases "\<exists>G. geodesic_segment_between G x x \<and> G \<subseteq> S")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<exists>G. geodesic_segment_between G x x \<and> G \<subseteq> S \<Longrightarrow> {x--S--x} = {x}
 2. \<nexists>G. geodesic_segment_between G x x \<and> G \<subseteq> S \<Longrightarrow> {x--S--x} = {x}
[PROOF STEP]
apply (meson geodesic_segment_between_x_x(3) some_geodesic_segment_description(1))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>G. geodesic_segment_between G x x \<and> G \<subseteq> S \<Longrightarrow> {x--S--x} = {x}
[PROOF STEP]
by (simp add: some_geodesic_segment_description(2))


[STATEMENT]
lemma geodesic_subsetD:
  assumes "geodesic_subset S" "x \<in> S" "y \<in> S"
  shows "geodesic_segment_between {x--S--y} x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_between {x--S--y} x y
[PROOF STEP]
using assms some_geodesic_segment_description(1)
[PROOF STATE]
proof (prove)
using this:
geodesic_subset S
x \<in> S
y \<in> S
\<exists>G. geodesic_segment_between G ?x ?y \<and> G \<subseteq> ?S \<Longrightarrow> geodesic_segment_between {?x--?S--?y} ?x ?y

goal (1 subgoal):
 1. geodesic_segment_between {x--S--y} x y
[PROOF STEP]
unfolding geodesic_subset_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>S. \<forall>y\<in>S. \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S
x \<in> S
y \<in> S
\<exists>G. geodesic_segment_between G ?x ?y \<and> G \<subseteq> ?S \<Longrightarrow> geodesic_segment_between {?x--?S--?y} ?x ?y

goal (1 subgoal):
 1. geodesic_segment_between {x--S--y} x y
[PROOF STEP]
by blast


[STATEMENT]
lemma geodesic_subsetI:
  assumes "\<And>x y. x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S"
  shows "geodesic_subset S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_subset S
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> S; ?y \<in> S\<rbrakk> \<Longrightarrow> \<exists>G. geodesic_segment_between G ?x ?y \<and> G \<subseteq> S

goal (1 subgoal):
 1. geodesic_subset S
[PROOF STEP]
unfolding geodesic_subset_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> S; ?y \<in> S\<rbrakk> \<Longrightarrow> \<exists>G. geodesic_segment_between G ?x ?y \<and> G \<subseteq> S

goal (1 subgoal):
 1. \<forall>x\<in>S. \<forall>y\<in>S. \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> S
[PROOF STEP]
by auto


[STATEMENT]
lemma geodesic_subset_empty:
  "geodesic_subset {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_subset {}
[PROOF STEP]
using geodesic_subsetI
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. \<lbrakk>x \<in> ?S; y \<in> ?S\<rbrakk> \<Longrightarrow> \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> ?S) \<Longrightarrow> geodesic_subset ?S

goal (1 subgoal):
 1. geodesic_subset {}
[PROOF STEP]
by auto


[STATEMENT]
lemma geodesic_subset_singleton:
  "geodesic_subset {x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_subset {x}
[PROOF STEP]
by (auto intro!: geodesic_subsetI geodesic_segment_between_x_x(1))


[STATEMENT]
lemma geodesic_subset_path_connected:
  assumes "geodesic_subset S"
  shows "path_connected S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path_connected S
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. path_connected S
[PROOF STEP]
have "\<exists>g. path g \<and> path_image g \<subseteq> S \<and> pathstart g = x \<and> pathfinish g = y" if "x \<in> S" "y \<in> S" for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>g. path g \<and> path_image g \<subseteq> S \<and> pathstart g = x \<and> pathfinish g = y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>g. path g \<and> path_image g \<subseteq> S \<and> pathstart g = x \<and> pathfinish g = y
[PROOF STEP]
define G where "G = {x--S--y}"
[PROOF STATE]
proof (state)
this:
G = {x--S--y}

goal (1 subgoal):
 1. \<exists>g. path g \<and> path_image g \<subseteq> S \<and> pathstart g = x \<and> pathfinish g = y
[PROOF STEP]
have *: "geodesic_segment_between G x y" "G \<subseteq> S" "x \<in> G" "y \<in> G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (geodesic_segment_between G x y &&& G \<subseteq> S) &&& x \<in> G &&& y \<in> G
[PROOF STEP]
using assms that
[PROOF STATE]
proof (prove)
using this:
geodesic_subset S
x \<in> S
y \<in> S

goal (1 subgoal):
 1. (geodesic_segment_between G x y &&& G \<subseteq> S) &&& x \<in> G &&& y \<in> G
[PROOF STEP]
by (auto simp add: G_def geodesic_subsetD some_geodesic_in_subset that(1) that(2))
[PROOF STATE]
proof (state)
this:
geodesic_segment_between G x y
G \<subseteq> S
x \<in> G
y \<in> G

goal (1 subgoal):
 1. \<exists>g. path g \<and> path_image g \<subseteq> S \<and> pathstart g = x \<and> pathfinish g = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
geodesic_segment_between G x y
G \<subseteq> S
x \<in> G
y \<in> G
[PROOF STEP]
have "path_connected G"
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_between G x y
G \<subseteq> S
x \<in> G
y \<in> G

goal (1 subgoal):
 1. path_connected G
[PROOF STEP]
using geodesic_segment_topology(3)
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_between G x y
G \<subseteq> S
x \<in> G
y \<in> G
geodesic_segment ?G \<Longrightarrow> path_connected ?G

goal (1 subgoal):
 1. path_connected G
[PROOF STEP]
unfolding geodesic_segment_def
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_between G x y
G \<subseteq> S
x \<in> G
y \<in> G
\<exists>x. Ex (geodesic_segment_between ?G x) \<Longrightarrow> path_connected ?G

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

goal (1 subgoal):
 1. \<exists>g. path g \<and> path_image g \<subseteq> S \<and> pathstart g = x \<and> pathfinish g = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path_connected G
[PROOF STEP]
have "\<exists>g. path g \<and> path_image g \<subseteq> G \<and> pathstart g = x \<and> pathfinish g = y"
[PROOF STATE]
proof (prove)
using this:
path_connected G

goal (1 subgoal):
 1. \<exists>g. path g \<and> path_image g \<subseteq> G \<and> pathstart g = x \<and> pathfinish g = y
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
path_connected G
geodesic_segment_between G x y
G \<subseteq> S
x \<in> G
y \<in> G

goal (1 subgoal):
 1. \<exists>g. path g \<and> path_image g \<subseteq> G \<and> pathstart g = x \<and> pathfinish g = y
[PROOF STEP]
unfolding path_connected_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>G. \<forall>y\<in>G. \<exists>g. path g \<and> path_image g \<subseteq> G \<and> pathstart g = x \<and> pathfinish g = y
geodesic_segment_between G x y
G \<subseteq> S
x \<in> G
y \<in> G

goal (1 subgoal):
 1. \<exists>g. path g \<and> path_image g \<subseteq> G \<and> pathstart g = x \<and> pathfinish g = y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>g. path g \<and> path_image g \<subseteq> G \<and> pathstart g = x \<and> pathfinish g = y

goal (1 subgoal):
 1. \<exists>g. path g \<and> path_image g \<subseteq> S \<and> pathstart g = x \<and> pathfinish g = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>g. path g \<and> path_image g \<subseteq> G \<and> pathstart g = x \<and> pathfinish g = y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>g. path g \<and> path_image g \<subseteq> G \<and> pathstart g = x \<and> pathfinish g = y

goal (1 subgoal):
 1. \<exists>g. path g \<and> path_image g \<subseteq> S \<and> pathstart g = x \<and> pathfinish g = y
[PROOF STEP]
using \<open>G \<subseteq> S\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>g. path g \<and> path_image g \<subseteq> G \<and> pathstart g = x \<and> pathfinish g = y
G \<subseteq> S

goal (1 subgoal):
 1. \<exists>g. path g \<and> path_image g \<subseteq> S \<and> pathstart g = x \<and> pathfinish g = y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>g. path g \<and> path_image g \<subseteq> S \<and> pathstart g = x \<and> pathfinish g = y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x \<in> S; ?y \<in> S\<rbrakk> \<Longrightarrow> \<exists>g. path g \<and> path_image g \<subseteq> S \<and> pathstart g = ?x \<and> pathfinish g = ?y

goal (1 subgoal):
 1. path_connected S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x \<in> S; ?y \<in> S\<rbrakk> \<Longrightarrow> \<exists>g. path g \<and> path_image g \<subseteq> S \<and> pathstart g = ?x \<and> pathfinish g = ?y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> S; ?y \<in> S\<rbrakk> \<Longrightarrow> \<exists>g. path g \<and> path_image g \<subseteq> S \<and> pathstart g = ?x \<and> pathfinish g = ?y

goal (1 subgoal):
 1. path_connected S
[PROOF STEP]
unfolding path_connected_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> S; ?y \<in> S\<rbrakk> \<Longrightarrow> \<exists>g. path g \<and> path_image g \<subseteq> S \<and> pathstart g = ?x \<and> pathfinish g = ?y

goal (1 subgoal):
 1. \<forall>x\<in>S. \<forall>y\<in>S. \<exists>g. path g \<and> path_image g \<subseteq> S \<and> pathstart g = x \<and> pathfinish g = y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path_connected S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma closed_segment_as_isometric_image:
  "((\<lambda>t. x + (t/dist x y) *\<^sub>R (y - x))`{0..dist x y}) = closed_segment x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>t. x + (t / dist x y) *\<^sub>R (y - x)) ` {0..dist x y} = closed_segment x y
[PROOF STEP]
proof (auto simp add: closed_segment_def image_iff)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t. \<lbrakk>0 \<le> t; t \<le> dist x y\<rbrakk> \<Longrightarrow> \<exists>u. x + (t / dist x y) *\<^sub>R (y - x) = (1 - u) *\<^sub>R x + u *\<^sub>R y \<and> 0 \<le> u \<and> u \<le> 1
 2. \<And>u. \<lbrakk>0 \<le> u; u \<le> 1\<rbrakk> \<Longrightarrow> \<exists>xa\<in>{0..dist x y}. (1 - u) *\<^sub>R x + u *\<^sub>R y = x + (xa / dist x y) *\<^sub>R (y - x)
[PROOF STEP]
fix t
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t. \<lbrakk>0 \<le> t; t \<le> dist x y\<rbrakk> \<Longrightarrow> \<exists>u. x + (t / dist x y) *\<^sub>R (y - x) = (1 - u) *\<^sub>R x + u *\<^sub>R y \<and> 0 \<le> u \<and> u \<le> 1
 2. \<And>u. \<lbrakk>0 \<le> u; u \<le> 1\<rbrakk> \<Longrightarrow> \<exists>xa\<in>{0..dist x y}. (1 - u) *\<^sub>R x + u *\<^sub>R y = x + (xa / dist x y) *\<^sub>R (y - x)
[PROOF STEP]
assume H: "0 \<le> t" "t \<le> dist x y"
[PROOF STATE]
proof (state)
this:
0 \<le> t
t \<le> dist x y

goal (2 subgoals):
 1. \<And>t. \<lbrakk>0 \<le> t; t \<le> dist x y\<rbrakk> \<Longrightarrow> \<exists>u. x + (t / dist x y) *\<^sub>R (y - x) = (1 - u) *\<^sub>R x + u *\<^sub>R y \<and> 0 \<le> u \<and> u \<le> 1
 2. \<And>u. \<lbrakk>0 \<le> u; u \<le> 1\<rbrakk> \<Longrightarrow> \<exists>xa\<in>{0..dist x y}. (1 - u) *\<^sub>R x + u *\<^sub>R y = x + (xa / dist x y) *\<^sub>R (y - x)
[PROOF STEP]
show "\<exists>u. x + (t / dist x y) *\<^sub>R (y - x) = (1 - u) *\<^sub>R x + u *\<^sub>R y \<and> 0 \<le> u \<and> u \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>u. x + (t / dist x y) *\<^sub>R (y - x) = (1 - u) *\<^sub>R x + u *\<^sub>R y \<and> 0 \<le> u \<and> u \<le> 1
[PROOF STEP]
apply (rule exI[of _ "t/dist x y"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x + (t / dist x y) *\<^sub>R (y - x) = (1 - t / dist x y) *\<^sub>R x + (t / dist x y) *\<^sub>R y \<and> 0 \<le> t / dist x y \<and> t / dist x y \<le> 1
[PROOF STEP]
using H
[PROOF STATE]
proof (prove)
using this:
0 \<le> t
t \<le> dist x y

goal (1 subgoal):
 1. x + (t / dist x y) *\<^sub>R (y - x) = (1 - t / dist x y) *\<^sub>R x + (t / dist x y) *\<^sub>R y \<and> 0 \<le> t / dist x y \<and> t / dist x y \<le> 1
[PROOF STEP]
apply (auto simp add: algebra_simps divide_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> t; t \<le> dist x y; x \<noteq> y\<rbrakk> \<Longrightarrow> x = (t / dist x y) *\<^sub>R x + ((dist x y - t) / dist x y) *\<^sub>R x
[PROOF STEP]
apply (metis add_diff_cancel_left' add_diff_eq add_divide_distrib dist_eq_0_iff scaleR_add_left vector_fraction_eq_iff)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>u. x + (t / dist x y) *\<^sub>R (y - x) = (1 - u) *\<^sub>R x + u *\<^sub>R y \<and> 0 \<le> u \<and> u \<le> 1

goal (1 subgoal):
 1. \<And>u. \<lbrakk>0 \<le> u; u \<le> 1\<rbrakk> \<Longrightarrow> \<exists>xa\<in>{0..dist x y}. (1 - u) *\<^sub>R x + u *\<^sub>R y = x + (xa / dist x y) *\<^sub>R (y - x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u. \<lbrakk>0 \<le> u; u \<le> 1\<rbrakk> \<Longrightarrow> \<exists>xa\<in>{0..dist x y}. (1 - u) *\<^sub>R x + u *\<^sub>R y = x + (xa / dist x y) *\<^sub>R (y - x)
[PROOF STEP]
fix u::real
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u. \<lbrakk>0 \<le> u; u \<le> 1\<rbrakk> \<Longrightarrow> \<exists>xa\<in>{0..dist x y}. (1 - u) *\<^sub>R x + u *\<^sub>R y = x + (xa / dist x y) *\<^sub>R (y - x)
[PROOF STEP]
assume H: "0 \<le> u" "u \<le> 1"
[PROOF STATE]
proof (state)
this:
0 \<le> u
u \<le> 1

goal (1 subgoal):
 1. \<And>u. \<lbrakk>0 \<le> u; u \<le> 1\<rbrakk> \<Longrightarrow> \<exists>xa\<in>{0..dist x y}. (1 - u) *\<^sub>R x + u *\<^sub>R y = x + (xa / dist x y) *\<^sub>R (y - x)
[PROOF STEP]
show "\<exists>t\<in>{0..dist x y}. (1 - u) *\<^sub>R x + u *\<^sub>R y = x + (t / dist x y) *\<^sub>R (y - x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t\<in>{0..dist x y}. (1 - u) *\<^sub>R x + u *\<^sub>R y = x + (t / dist x y) *\<^sub>R (y - x)
[PROOF STEP]
apply (rule bexI[of _ "u * dist x y"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (1 - u) *\<^sub>R x + u *\<^sub>R y = x + (u * dist x y / dist x y) *\<^sub>R (y - x)
 2. u * dist x y \<in> {0..dist x y}
[PROOF STEP]
using H
[PROOF STATE]
proof (prove)
using this:
0 \<le> u
u \<le> 1

goal (2 subgoals):
 1. (1 - u) *\<^sub>R x + u *\<^sub>R y = x + (u * dist x y / dist x y) *\<^sub>R (y - x)
 2. u * dist x y \<in> {0..dist x y}
[PROOF STEP]
by (auto simp add: algebra_simps mult_left_le_one_le)
[PROOF STATE]
proof (state)
this:
\<exists>t\<in>{0..dist x y}. (1 - u) *\<^sub>R x + u *\<^sub>R y = x + (t / dist x y) *\<^sub>R (y - x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in geodesic_space) some_geodesic_is_geodesic_segment [simp]:
  "geodesic_segment_between {x--y} x (y::'a)"
  "geodesic_segment {x--y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_between {x--y} x y &&& geodesic_segment {x--y}
[PROOF STEP]
using some_geodesic_segment_description(1)[of x y] geodesic_subsetD[OF geodesic]
[PROOF STATE]
proof (prove)
using this:
\<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> ?S \<Longrightarrow> geodesic_segment_between {x--?S--y} x y
\<lbrakk>?x \<in> UNIV; ?y \<in> UNIV\<rbrakk> \<Longrightarrow> geodesic_segment_between {?x--?y} ?x ?y

goal (1 subgoal):
 1. geodesic_segment_between {x--y} x y &&& geodesic_segment {x--y}
[PROOF STEP]
by (auto, blast)


[STATEMENT]
lemma (in geodesic_space) some_geodesic_connected [simp]:
  "connected {x--y}" "path_connected {x--y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. connected {x--y} &&& path_connected {x--y}
[PROOF STEP]
by (auto intro!: geodesic_segment_topology)


[STATEMENT]
lemma (in geodesic_space) geodesic_segment_param_in_geodesic_spaces [simp]:
  "geodesic_segment_param {x--y} x 0 = x"
  "geodesic_segment_param {x--y} x (dist x y) = y"
  "t \<in> {0..dist x y} \<Longrightarrow> geodesic_segment_param {x--y} x t \<in> {x--y}"
  "isometry_on {0..dist x y} (geodesic_segment_param {x--y} x)"
  "(geodesic_segment_param {x--y} x)`{0..dist x y} = {x--y}"
  "t \<in> {0..dist x y} \<Longrightarrow> dist x (geodesic_segment_param {x--y} x t) = t"
  "s \<in> {0..dist x y} \<Longrightarrow> t \<in> {0..dist x y} \<Longrightarrow> dist (geodesic_segment_param {x--y} x s) (geodesic_segment_param {x--y} x t) = abs(s-t)"
  "z \<in> {x--y} \<Longrightarrow> z = geodesic_segment_param {x--y} x (dist x z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((geodesic_segment_param {x--y} x 0 = x &&& geodesic_segment_param {x--y} x (dist x y) = y) &&& (t \<in> {0..dist x y} \<Longrightarrow> geodesic_segment_param {x--y} x t \<in> {x--y}) &&& isometry_on {0..dist x y} (geodesic_segment_param {x--y} x)) &&& (geodesic_segment_param {x--y} x ` {0..dist x y} = {x--y} &&& (t \<in> {0..dist x y} \<Longrightarrow> dist x (geodesic_segment_param {x--y} x t) = t)) &&& (\<lbrakk>s \<in> {0..dist x y}; t \<in> {0..dist x y}\<rbrakk> \<Longrightarrow> dist (geodesic_segment_param {x--y} x s) (geodesic_segment_param {x--y} x t) = \<bar>s - t\<bar>) &&& (z \<in> {x--y} \<Longrightarrow> z = geodesic_segment_param {x--y} x (dist x z))
[PROOF STEP]
using geodesic_segment_param[OF some_geodesic_is_geodesic_segment(1)[of x y]]
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_param {x--y} x 0 = x
geodesic_segment_param {x--y} x (dist x y) = y
?t \<in> {0..dist x y} \<Longrightarrow> geodesic_segment_param {x--y} x ?t \<in> {x--y}
isometry_on {0..dist x y} (geodesic_segment_param {x--y} x)
geodesic_segment_param {x--y} x ` {0..dist x y} = {x--y}
?t \<in> {0..dist x y} \<Longrightarrow> dist x (geodesic_segment_param {x--y} x ?t) = ?t
\<lbrakk>?s \<in> {0..dist x y}; ?t \<in> {0..dist x y}\<rbrakk> \<Longrightarrow> dist (geodesic_segment_param {x--y} x ?s) (geodesic_segment_param {x--y} x ?t) = \<bar>?s - ?t\<bar>
?z \<in> {x--y} \<Longrightarrow> ?z = geodesic_segment_param {x--y} x (dist x ?z)

goal (1 subgoal):
 1. ((geodesic_segment_param {x--y} x 0 = x &&& geodesic_segment_param {x--y} x (dist x y) = y) &&& (t \<in> {0..dist x y} \<Longrightarrow> geodesic_segment_param {x--y} x t \<in> {x--y}) &&& isometry_on {0..dist x y} (geodesic_segment_param {x--y} x)) &&& (geodesic_segment_param {x--y} x ` {0..dist x y} = {x--y} &&& (t \<in> {0..dist x y} \<Longrightarrow> dist x (geodesic_segment_param {x--y} x t) = t)) &&& (\<lbrakk>s \<in> {0..dist x y}; t \<in> {0..dist x y}\<rbrakk> \<Longrightarrow> dist (geodesic_segment_param {x--y} x s) (geodesic_segment_param {x--y} x t) = \<bar>s - t\<bar>) &&& (z \<in> {x--y} \<Longrightarrow> z = geodesic_segment_param {x--y} x (dist x z))
[PROOF STEP]
by auto


[STATEMENT]
lemma (in geodesic_space) uniquely_geodesic_spaceI:
  assumes "\<And>G H x (y::'a). geodesic_segment_between G x y \<Longrightarrow> geodesic_segment_between H x y \<Longrightarrow> G \<inter> H = {x, y} \<Longrightarrow> x = y"
          "geodesic_segment_between G x y" "geodesic_segment_between H x (y::'a)"
  shows "G = H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. G = H
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. G = 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. G = H
[PROOF STEP]
obtain h where h: "h 0 = x" "h (dist x y) = y" "isometry_on {0..dist x y} h" "H = h`{0..dist x y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>h. \<lbrakk>h 0 = x; h (dist x y) = y; isometry_on {0..dist x y} h; H = h ` {0..dist x y}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson \<open>geodesic_segment_between H x y\<close> geodesic_segment_between_def)
[PROOF STATE]
proof (state)
this:
h 0 = x
h (dist x y) = y
isometry_on {0..dist x y} h
H = h ` {0..dist x y}

goal (1 subgoal):
 1. G = H
[PROOF STEP]
have "g t = h t" if "t \<in> {0..dist x y}" for t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g t = h t
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g t \<noteq> h t \<Longrightarrow> False
[PROOF STEP]
assume "g t \<noteq> h t"
[PROOF STATE]
proof (state)
this:
g t \<noteq> h t

goal (1 subgoal):
 1. g t \<noteq> h t \<Longrightarrow> False
[PROOF STEP]
define Z where "Z = {s \<in> {0..dist x y}. g s = h s}"
[PROOF STATE]
proof (state)
this:
Z = {s \<in> {0..dist x y}. g s = h s}

goal (1 subgoal):
 1. g t \<noteq> h t \<Longrightarrow> False
[PROOF STEP]
have "0 \<in> Z" "dist x y \<in> Z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<in> Z &&& dist x y \<in> Z
[PROOF STEP]
unfolding Z_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<in> {s \<in> {0..dist x y}. g s = h s} &&& dist x y \<in> {s \<in> {0..dist x y}. g s = h s}
[PROOF STEP]
using g h
[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}
h 0 = x
h (dist x y) = y
isometry_on {0..dist x y} h
H = h ` {0..dist x y}

goal (1 subgoal):
 1. 0 \<in> {s \<in> {0..dist x y}. g s = h s} &&& dist x y \<in> {s \<in> {0..dist x y}. g s = h s}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<in> Z
dist x y \<in> Z

goal (1 subgoal):
 1. g t \<noteq> h t \<Longrightarrow> False
[PROOF STEP]
have "t \<notin> Z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<notin> Z
[PROOF STEP]
unfolding Z_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<notin> {s \<in> {0..dist x y}. g s = h s}
[PROOF STEP]
using \<open>g t \<noteq> h t\<close>
[PROOF STATE]
proof (prove)
using this:
g t \<noteq> h t

goal (1 subgoal):
 1. t \<notin> {s \<in> {0..dist x y}. g s = h s}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t \<notin> Z

goal (1 subgoal):
 1. g t \<noteq> h t \<Longrightarrow> False
[PROOF STEP]
have [simp]: "closed Z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed Z
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. closed Z
[PROOF STEP]
have *: "Z = (\<lambda>s. dist (g s) (h s))-`{0} \<inter> {0..dist x y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Z = (\<lambda>s. dist (g s) (h s)) -` {0} \<inter> {0..dist x y}
[PROOF STEP]
unfolding Z_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {s \<in> {0..dist x y}. g s = h s} = (\<lambda>s. dist (g s) (h s)) -` {0} \<inter> {0..dist x y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Z = (\<lambda>s. dist (g s) (h s)) -` {0} \<inter> {0..dist x y}

goal (1 subgoal):
 1. closed Z
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed Z
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed ((\<lambda>s. dist (g s) (h s)) -` {0} \<inter> {0..dist x y})
[PROOF STEP]
apply (rule closed_vimage_Int)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. closed {0}
 2. continuous_on {0..dist x y} (\<lambda>s. dist (g s) (h s))
 3. closed {0..dist x y}
[PROOF STEP]
using isometry_on_continuous[OF g(3)] isometry_on_continuous[OF h(3)] continuous_on_dist
[PROOF STATE]
proof (prove)
using this:
continuous_on {0..dist x y} g
continuous_on {0..dist x y} h
\<lbrakk>continuous_on ?s ?f; continuous_on ?s ?g\<rbrakk> \<Longrightarrow> continuous_on ?s (\<lambda>x. dist (?f x) (?g x))

goal (3 subgoals):
 1. closed {0}
 2. continuous_on {0..dist x y} (\<lambda>s. dist (g s) (h s))
 3. closed {0..dist x y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
closed Z

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
closed Z

goal (1 subgoal):
 1. g t \<noteq> h t \<Longrightarrow> False
[PROOF STEP]
define a where "a = Sup (Z \<inter> {0..t})"
[PROOF STATE]
proof (state)
this:
a = Sup (Z \<inter> {0..t})

goal (1 subgoal):
 1. g t \<noteq> h t \<Longrightarrow> False
[PROOF STEP]
have a: "a \<in> Z \<inter> {0..t}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> Z \<inter> {0..t}
[PROOF STEP]
unfolding a_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sup (Z \<inter> {0..t}) \<in> Z \<inter> {0..t}
[PROOF STEP]
apply (rule closed_contains_Sup, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Z \<inter> {0..t} = {} \<Longrightarrow> False
[PROOF STEP]
using \<open>0 \<in> Z\<close> that
[PROOF STATE]
proof (prove)
using this:
0 \<in> Z
t \<in> {0..dist x y}

goal (1 subgoal):
 1. Z \<inter> {0..t} = {} \<Longrightarrow> False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<in> Z \<inter> {0..t}

goal (1 subgoal):
 1. g t \<noteq> h t \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> Z \<inter> {0..t}
[PROOF STEP]
have "h a = g a"
[PROOF STATE]
proof (prove)
using this:
a \<in> Z \<inter> {0..t}

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

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

goal (1 subgoal):
 1. g t \<noteq> h t \<Longrightarrow> False
[PROOF STEP]
define b where "b = Inf (Z \<inter> {t..dist x y})"
[PROOF STATE]
proof (state)
this:
b = Inf (Z \<inter> {t..dist x y})

goal (1 subgoal):
 1. g t \<noteq> h t \<Longrightarrow> False
[PROOF STEP]
have b: "b \<in> Z \<inter> {t..dist x y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<in> Z \<inter> {t..dist x y}
[PROOF STEP]
unfolding b_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Inf (Z \<inter> {t..dist x y}) \<in> Z \<inter> {t..dist x y}
[PROOF STEP]
apply (rule closed_contains_Inf, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Z \<inter> {t..dist x y} = {} \<Longrightarrow> False
[PROOF STEP]
using \<open>dist x y \<in> Z\<close> that
[PROOF STATE]
proof (prove)
using this:
dist x y \<in> Z
t \<in> {0..dist x y}

goal (1 subgoal):
 1. Z \<inter> {t..dist x y} = {} \<Longrightarrow> False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b \<in> Z \<inter> {t..dist x y}

goal (1 subgoal):
 1. g t \<noteq> h t \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b \<in> Z \<inter> {t..dist x y}
[PROOF STEP]
have "h b = g b"
[PROOF STATE]
proof (prove)
using this:
b \<in> Z \<inter> {t..dist x y}

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

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

goal (1 subgoal):
 1. g t \<noteq> h t \<Longrightarrow> False
[PROOF STEP]
have notZ: "s \<notin> Z" if "s \<in> {a<..<b}" for s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<notin> Z
[PROOF STEP]
proof (rule ccontr, auto, cases "s \<le> t")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>s \<in> Z; s \<le> t\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>s \<in> Z; \<not> s \<le> t\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
s \<le> t

goal (2 subgoals):
 1. \<lbrakk>s \<in> Z; s \<le> t\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>s \<in> Z; \<not> s \<le> t\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "s \<in> Z"
[PROOF STATE]
proof (state)
this:
s \<in> Z

goal (2 subgoals):
 1. \<lbrakk>s \<in> Z; s \<le> t\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>s \<in> Z; \<not> s \<le> t\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<in> Z
[PROOF STEP]
have *: "s \<in> Z \<inter> {0..t}"
[PROOF STATE]
proof (prove)
using this:
s \<in> Z

goal (1 subgoal):
 1. s \<in> Z \<inter> {0..t}
[PROOF STEP]
using that a True
[PROOF STATE]
proof (prove)
using this:
s \<in> Z
s \<in> {a<..<b}
a \<in> Z \<inter> {0..t}
s \<le> t

goal (1 subgoal):
 1. s \<in> Z \<inter> {0..t}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s \<in> Z \<inter> {0..t}

goal (2 subgoals):
 1. \<lbrakk>s \<in> Z; s \<le> t\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>s \<in> Z; \<not> s \<le> t\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "s \<le> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<le> a
[PROOF STEP]
unfolding a_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<le> Sup (Z \<inter> {0..t})
[PROOF STEP]
apply (rule cSup_upper)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. s \<in> Z \<inter> {0..t}
 2. bdd_above (Z \<inter> {0..t})
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
s \<in> Z \<inter> {0..t}

goal (2 subgoals):
 1. s \<in> Z \<inter> {0..t}
 2. bdd_above (Z \<inter> {0..t})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s \<le> a

goal (2 subgoals):
 1. \<lbrakk>s \<in> Z; s \<le> t\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>s \<in> Z; \<not> s \<le> t\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<le> a
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
s \<le> a

goal (1 subgoal):
 1. False
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
s \<le> a
s \<in> {a<..<b}

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

goal (1 subgoal):
 1. \<lbrakk>s \<in> Z; \<not> s \<le> t\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>s \<in> Z; \<not> s \<le> t\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> s \<le> t

goal (1 subgoal):
 1. \<lbrakk>s \<in> Z; \<not> s \<le> t\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "s \<in> Z"
[PROOF STATE]
proof (state)
this:
s \<in> Z

goal (1 subgoal):
 1. \<lbrakk>s \<in> Z; \<not> s \<le> t\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<in> Z
[PROOF STEP]
have *: "s \<in> Z \<inter> {t..dist x y}"
[PROOF STATE]
proof (prove)
using this:
s \<in> Z

goal (1 subgoal):
 1. s \<in> Z \<inter> {t..dist x y}
[PROOF STEP]
using that b False
[PROOF STATE]
proof (prove)
using this:
s \<in> Z
s \<in> {a<..<b}
b \<in> Z \<inter> {t..dist x y}
\<not> s \<le> t

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

goal (1 subgoal):
 1. \<lbrakk>s \<in> Z; \<not> s \<le> t\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "s \<ge> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<le> s
[PROOF STEP]
unfolding b_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Inf (Z \<inter> {t..dist x y}) \<le> s
[PROOF STEP]
apply (rule cInf_lower)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. s \<in> Z \<inter> {t..dist x y}
 2. bdd_below (Z \<inter> {t..dist x y})
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
s \<in> Z \<inter> {t..dist x y}

goal (2 subgoals):
 1. s \<in> Z \<inter> {t..dist x y}
 2. bdd_below (Z \<inter> {t..dist x y})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b \<le> s

goal (1 subgoal):
 1. \<lbrakk>s \<in> Z; \<not> s \<le> t\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b \<le> s
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
b \<le> s

goal (1 subgoal):
 1. False
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
b \<le> s
s \<in> {a<..<b}

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?s \<in> {a<..<b} \<Longrightarrow> ?s \<notin> Z

goal (1 subgoal):
 1. g t \<noteq> h t \<Longrightarrow> False
[PROOF STEP]
have "t \<in> {a<..<b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> {a<..<b}
[PROOF STEP]
using a b \<open>t \<notin> Z\<close> less_eq_real_def
[PROOF STATE]
proof (prove)
using this:
a \<in> Z \<inter> {0..t}
b \<in> Z \<inter> {t..dist x y}
t \<notin> Z
(?x \<le> ?y) = (?x < ?y \<or> ?x = ?y)

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

goal (1 subgoal):
 1. g t \<noteq> h t \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t \<in> {a<..<b}
[PROOF STEP]
have "a \<le> b"
[PROOF STATE]
proof (prove)
using this:
t \<in> {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. g t \<noteq> h t \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<le> b
[PROOF STEP]
have "dist (h a) (h b) = b-a"
[PROOF STATE]
proof (prove)
using this:
a \<le> b

goal (1 subgoal):
 1. dist (h a) (h b) = b - a
[PROOF STEP]
using isometry_onD[OF h(3), of a b] a b that
[PROOF STATE]
proof (prove)
using this:
a \<le> b
\<lbrakk>a \<in> {0..dist x y}; b \<in> {0..dist x y}\<rbrakk> \<Longrightarrow> dist (h a) (h b) = dist a b
a \<in> Z \<inter> {0..t}
b \<in> Z \<inter> {t..dist x y}
t \<in> {0..dist x y}

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

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

goal (1 subgoal):
 1. g t \<noteq> h t \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dist (h a) (h b) = b - a
[PROOF STEP]
have "dist (h a) (h b) > 0"
[PROOF STATE]
proof (prove)
using this:
dist (h a) (h b) = b - a

goal (1 subgoal):
 1. 0 < dist (h a) (h b)
[PROOF STEP]
using \<open>t \<in> {a<..<b}\<close>
[PROOF STATE]
proof (prove)
using this:
dist (h a) (h b) = b - a
t \<in> {a<..<b}

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

goal (1 subgoal):
 1. g t \<noteq> h t \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < dist (h a) (h b)
[PROOF STEP]
have "h a \<noteq> h b"
[PROOF STATE]
proof (prove)
using this:
0 < dist (h a) (h b)

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

goal (1 subgoal):
 1. g t \<noteq> h t \<Longrightarrow> False
[PROOF STEP]
define G2 where "G2 = g`{a..b}"
[PROOF STATE]
proof (state)
this:
G2 = g ` {a..b}

goal (1 subgoal):
 1. g t \<noteq> h t \<Longrightarrow> False
[PROOF STEP]
define H2 where "H2 = h`{a..b}"
[PROOF STATE]
proof (state)
this:
H2 = h ` {a..b}

goal (1 subgoal):
 1. g t \<noteq> h t \<Longrightarrow> False
[PROOF STEP]
have "G2 \<inter> H2 \<subseteq> {h a, h b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. G2 \<inter> H2 \<subseteq> {h a, h b}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> G2 \<inter> H2 \<Longrightarrow> x \<in> {h a, h b}
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> G2 \<inter> H2 \<Longrightarrow> x \<in> {h a, h b}
[PROOF STEP]
assume z: "z \<in> G2 \<inter> H2"
[PROOF STATE]
proof (state)
this:
z \<in> G2 \<inter> H2

goal (1 subgoal):
 1. \<And>x. x \<in> G2 \<inter> H2 \<Longrightarrow> x \<in> {h a, h b}
[PROOF STEP]
obtain sg where sg: "z = g sg" "sg \<in> {a..b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>sg. \<lbrakk>z = g sg; sg \<in> {a..b}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using z
[PROOF STATE]
proof (prove)
using this:
z \<in> G2 \<inter> H2

goal (1 subgoal):
 1. (\<And>sg. \<lbrakk>z = g sg; sg \<in> {a..b}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding G2_def
[PROOF STATE]
proof (prove)
using this:
z \<in> g ` {a..b} \<inter> H2

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

goal (1 subgoal):
 1. \<And>x. x \<in> G2 \<inter> H2 \<Longrightarrow> x \<in> {h a, h b}
[PROOF STEP]
obtain sh where sh: "z = h sh" "sh \<in> {a..b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>sh. \<lbrakk>z = h sh; sh \<in> {a..b}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using z
[PROOF STATE]
proof (prove)
using this:
z \<in> G2 \<inter> H2

goal (1 subgoal):
 1. (\<And>sh. \<lbrakk>z = h sh; sh \<in> {a..b}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding H2_def
[PROOF STATE]
proof (prove)
using this:
z \<in> G2 \<inter> h ` {a..b}

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

goal (1 subgoal):
 1. \<And>x. x \<in> G2 \<inter> H2 \<Longrightarrow> x \<in> {h a, h b}
[PROOF STEP]
have "sg = dist x z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sg = dist x z
[PROOF STEP]
using isometry_onD[OF g(3), of 0 sg] a b sg(2)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 \<in> {0..dist x y}; sg \<in> {0..dist x y}\<rbrakk> \<Longrightarrow> dist (g 0) (g sg) = dist 0 sg
a \<in> Z \<inter> {0..t}
b \<in> Z \<inter> {t..dist x y}
sg \<in> {a..b}

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> G2 \<inter> H2 \<Longrightarrow> x \<in> {h a, h b}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sg = dist x z

goal (1 subgoal):
 1. \<And>x. x \<in> G2 \<inter> H2 \<Longrightarrow> x \<in> {h a, h b}
[PROOF STEP]
have "sh = dist x z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sh = dist x z
[PROOF STEP]
using isometry_onD[OF h(3), of 0 sh] a b sh(2)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 \<in> {0..dist x y}; sh \<in> {0..dist x y}\<rbrakk> \<Longrightarrow> dist (h 0) (h sh) = dist 0 sh
a \<in> Z \<inter> {0..t}
b \<in> Z \<inter> {t..dist x y}
sh \<in> {a..b}

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> G2 \<inter> H2 \<Longrightarrow> x \<in> {h a, h b}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sg = dist x z
sh = dist x z
[PROOF STEP]
have "sg = sh"
[PROOF STATE]
proof (prove)
using this:
sg = dist x z
sh = dist x z

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

goal (1 subgoal):
 1. \<And>x. x \<in> G2 \<inter> H2 \<Longrightarrow> x \<in> {h a, h b}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sg = sh
[PROOF STEP]
have "sh \<in> Z"
[PROOF STATE]
proof (prove)
using this:
sg = sh

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

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

goal (1 subgoal):
 1. sh \<in> {s \<in> {0..dist x y}. g s = h s}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sh \<in> Z

goal (1 subgoal):
 1. \<And>x. x \<in> G2 \<inter> H2 \<Longrightarrow> x \<in> {h a, h b}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sh \<in> Z
[PROOF STEP]
have "sh \<in> {a, b}"
[PROOF STATE]
proof (prove)
using this:
sh \<in> Z

goal (1 subgoal):
 1. sh \<in> {a, b}
[PROOF STEP]
using notZ sh(2)
[PROOF STATE]
proof (prove)
using this:
sh \<in> Z
?s \<in> {a<..<b} \<Longrightarrow> ?s \<notin> Z
sh \<in> {a..b}

goal (1 subgoal):
 1. sh \<in> {a, b}
[PROOF STEP]
by (metis IntD2 atLeastAtMost_iff atLeastAtMost_singleton greaterThanLessThan_iff inf_bot_left insertI2 insert_inter_insert not_le)
[PROOF STATE]
proof (state)
this:
sh \<in> {a, b}

goal (1 subgoal):
 1. \<And>x. x \<in> G2 \<inter> H2 \<Longrightarrow> x \<in> {h a, h b}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sh \<in> {a, b}
[PROOF STEP]
show "z \<in> {h a, h b}"
[PROOF STATE]
proof (prove)
using this:
sh \<in> {a, b}

goal (1 subgoal):
 1. z \<in> {h a, h b}
[PROOF STEP]
using sh(1)
[PROOF STATE]
proof (prove)
using this:
sh \<in> {a, b}
z = h sh

goal (1 subgoal):
 1. z \<in> {h a, h b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<in> {h a, h b}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
G2 \<inter> H2 \<subseteq> {h a, h b}

goal (1 subgoal):
 1. g t \<noteq> h t \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
G2 \<inter> H2 \<subseteq> {h a, h b}
[PROOF STEP]
have "G2 \<inter> H2 = {h a, h b}"
[PROOF STATE]
proof (prove)
using this:
G2 \<inter> H2 \<subseteq> {h a, h b}

goal (1 subgoal):
 1. G2 \<inter> H2 = {h a, h b}
[PROOF STEP]
using \<open>h a = g a\<close> \<open>h b = g b\<close> \<open>a \<le> b\<close>
[PROOF STATE]
proof (prove)
using this:
G2 \<inter> H2 \<subseteq> {h a, h b}
h a = g a
h b = g b
a \<le> b

goal (1 subgoal):
 1. G2 \<inter> H2 = {h a, h b}
[PROOF STEP]
unfolding H2_def G2_def
[PROOF STATE]
proof (prove)
using this:
g ` {a..b} \<inter> h ` {a..b} \<subseteq> {h a, h b}
h a = g a
h b = g b
a \<le> b

goal (1 subgoal):
 1. g ` {a..b} \<inter> h ` {a..b} = {h a, h b}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>g ` {a..b} \<inter> h ` {a..b} \<subseteq> {g a, g b}; h a = g a; h b = g b; a \<le> b\<rbrakk> \<Longrightarrow> g a \<in> h ` {a..b}
 2. \<lbrakk>g ` {a..b} \<inter> h ` {a..b} \<subseteq> {g a, g b}; h a = g a; h b = g b; a \<le> b\<rbrakk> \<Longrightarrow> g b \<in> h ` {a..b}
[PROOF STEP]
unfolding \<open>h a = g a\<close>[symmetric] \<open>h b = g b\<close>[symmetric]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>g ` {a..b} \<inter> h ` {a..b} \<subseteq> {h a, h b}; h a = h a; h b = h b; a \<le> b\<rbrakk> \<Longrightarrow> h a \<in> h ` {a..b}
 2. \<lbrakk>g ` {a..b} \<inter> h ` {a..b} \<subseteq> {h a, h b}; h a = h a; h b = h b; a \<le> b\<rbrakk> \<Longrightarrow> h b \<in> h ` {a..b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
G2 \<inter> H2 = {h a, h b}

goal (1 subgoal):
 1. g t \<noteq> h t \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
G2 \<inter> H2 = {h a, h b}

goal (1 subgoal):
 1. g t \<noteq> h t \<Longrightarrow> False
[PROOF STEP]
have "geodesic_segment_between G2 (h a) (h b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_between G2 (h a) (h b)
[PROOF STEP]
unfolding G2_def \<open>h a = g a\<close> \<open>h b = g b\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_between (g ` {a..b}) (g a) (g b)
[PROOF STEP]
apply (rule geodesic_segmentI2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. isometry_on {a..b} g
 2. a \<le> b
[PROOF STEP]
apply (rule isometry_on_subset[OF g(3)])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. {a..b} \<subseteq> {0..dist x y}
 2. a \<le> b
[PROOF STEP]
using a b that
[PROOF STATE]
proof (prove)
using this:
a \<in> Z \<inter> {0..t}
b \<in> Z \<inter> {t..dist x y}
t \<in> {0..dist x y}

goal (2 subgoals):
 1. {a..b} \<subseteq> {0..dist x y}
 2. a \<le> b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
geodesic_segment_between G2 (h a) (h b)

goal (1 subgoal):
 1. g t \<noteq> h t \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
geodesic_segment_between G2 (h a) (h b)

goal (1 subgoal):
 1. g t \<noteq> h t \<Longrightarrow> False
[PROOF STEP]
have "geodesic_segment_between H2 (h a) (h b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_between H2 (h a) (h b)
[PROOF STEP]
unfolding H2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_between (h ` {a..b}) (h a) (h b)
[PROOF STEP]
apply (rule geodesic_segmentI2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. isometry_on {a..b} h
 2. a \<le> b
[PROOF STEP]
apply (rule isometry_on_subset[OF h(3)])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. {a..b} \<subseteq> {0..dist x y}
 2. a \<le> b
[PROOF STEP]
using a b that
[PROOF STATE]
proof (prove)
using this:
a \<in> Z \<inter> {0..t}
b \<in> Z \<inter> {t..dist x y}
t \<in> {0..dist x y}

goal (2 subgoals):
 1. {a..b} \<subseteq> {0..dist x y}
 2. a \<le> b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
geodesic_segment_between H2 (h a) (h b)

goal (1 subgoal):
 1. g t \<noteq> h t \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
G2 \<inter> H2 = {h a, h b}
geodesic_segment_between G2 (h a) (h b)
geodesic_segment_between H2 (h a) (h b)
[PROOF STEP]
have "h a = h b"
[PROOF STATE]
proof (prove)
using this:
G2 \<inter> H2 = {h a, h b}
geodesic_segment_between G2 (h a) (h b)
geodesic_segment_between H2 (h a) (h b)

goal (1 subgoal):
 1. h a = h b
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
G2 \<inter> H2 = {h a, h b}
geodesic_segment_between G2 (h a) (h b)
geodesic_segment_between H2 (h a) (h b)
\<lbrakk>geodesic_segment_between ?G ?x ?y; geodesic_segment_between ?H ?x ?y; ?G \<inter> ?H = {?x, ?y}\<rbrakk> \<Longrightarrow> ?x = ?y

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

goal (1 subgoal):
 1. g t \<noteq> h t \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
h a = h b
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
h a = h b

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>h a \<noteq> h b\<close>
[PROOF STATE]
proof (prove)
using this:
h a = h b
h a \<noteq> h b

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

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

goal (1 subgoal):
 1. G = H
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?t \<in> {0..dist x y} \<Longrightarrow> g ?t = h ?t
[PROOF STEP]
show "G = H"
[PROOF STATE]
proof (prove)
using this:
?t \<in> {0..dist x y} \<Longrightarrow> g ?t = h ?t

goal (1 subgoal):
 1. G = H
[PROOF STEP]
using g(4) h(4)
[PROOF STATE]
proof (prove)
using this:
?t \<in> {0..dist x y} \<Longrightarrow> g ?t = h ?t
G = g ` {0..dist x y}
H = h ` {0..dist x y}

goal (1 subgoal):
 1. G = H
[PROOF STEP]
by (simp add: image_def)
[PROOF STATE]
proof (state)
this:
G = H

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma geodesic_segment_unique:
  "geodesic_segment_between G x y = (G = {x--(y::'a)})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_between G x y = (G = {x--y})
[PROOF STEP]
using uniquely_geodesic[of _ x y]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>geodesic_segment_between ?G x y; geodesic_segment_between ?H x y\<rbrakk> \<Longrightarrow> ?G = ?H

goal (1 subgoal):
 1. geodesic_segment_between G x y = (G = {x--y})
[PROOF STEP]
by (meson some_geodesic_is_geodesic_segment)


[STATEMENT]
lemma geodesic_segment_dist':
  assumes "dist x z = dist x y + dist y z"
  shows "y \<in> {x--z}" "{x--z} = {x--y} \<union> {y--z}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> {x--z} &&& {x--z} = {x--y} \<union> {y--z}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y \<in> {x--z}
 2. {x--z} = {x--y} \<union> {y--z}
[PROOF STEP]
have "geodesic_segment_between ({x--y} \<union> {y--z}) x z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_between ({x--y} \<union> {y--z}) x z
[PROOF STEP]
using geodesic_segment_union[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>geodesic_segment_between ?G x y; geodesic_segment_between ?H y z\<rbrakk> \<Longrightarrow> geodesic_segment_between (?G \<union> ?H) x z
\<lbrakk>geodesic_segment_between ?G x y; geodesic_segment_between ?H y z\<rbrakk> \<Longrightarrow> ?G \<inter> ?H = {y}

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

goal (2 subgoals):
 1. y \<in> {x--z}
 2. {x--z} = {x--y} \<union> {y--z}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
geodesic_segment_between ({x--y} \<union> {y--z}) x z
[PROOF STEP]
show "{x--z} = {x--y} \<union> {y--z}"
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_between ({x--y} \<union> {y--z}) x z

goal (1 subgoal):
 1. {x--z} = {x--y} \<union> {y--z}
[PROOF STEP]
using geodesic_segment_unique
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_between ({x--y} \<union> {y--z}) x z
geodesic_segment_between ?G ?x ?y = (?G = {?x--?y})

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

goal (1 subgoal):
 1. y \<in> {x--z}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{x--z} = {x--y} \<union> {y--z}
[PROOF STEP]
show "y \<in> {x--z}"
[PROOF STATE]
proof (prove)
using this:
{x--z} = {x--y} \<union> {y--z}

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma geodesic_segment_expression:
  "{x--z} = {y. dist x z = dist x y + dist y z}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x--z} = {y. dist x z = dist x y + dist y z}
[PROOF STEP]
using geodesic_segment_dist'(1) geodesic_segment_dist[OF some_geodesic_is_geodesic_segment(1)]
[PROOF STATE]
proof (prove)
using this:
dist ?x ?z = dist ?x ?y + dist ?y ?z \<Longrightarrow> ?y \<in> {?x--?z}
?a \<in> {?x--?y} \<Longrightarrow> dist ?x ?a + dist ?a ?y = dist ?x ?y

goal (1 subgoal):
 1. {x--z} = {y. dist x z = dist x y + dist y z}
[PROOF STEP]
by auto


[STATEMENT]
lemma geodesic_segment_split:
  assumes "(y::'a) \<in> {x--z}"
  shows "{x--z} = {x--y} \<union> {y--z}"
        "{x--y} \<inter> {y--z} = {y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x--z} = {x--y} \<union> {y--z} &&& {x--y} \<inter> {y--z} = {y}
[PROOF STEP]
apply (metis assms geodesic_segment_dist geodesic_segment_dist'(2) some_geodesic_is_geodesic_segment(1))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x--y} \<inter> {y--z} = {y}
[PROOF STEP]
apply (rule geodesic_segment_union(2)[of x z], auto simp add: assms)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist x z = dist x y + dist y z
[PROOF STEP]
using assms geodesic_segment_expression
[PROOF STATE]
proof (prove)
using this:
y \<in> {x--z}
{?x--?z} = {y. dist ?x ?z = dist ?x y + dist y ?z}

goal (1 subgoal):
 1. dist x z = dist x y + dist y z
[PROOF STEP]
by blast


[STATEMENT]
lemma geodesic_segment_subparam':
  assumes "y \<in> {x--z}" "t \<in> {0..dist x y}"
  shows "geodesic_segment_param {x--z} x t = geodesic_segment_param {x--y} x t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_param {x--z} x t = geodesic_segment_param {x--y} x t
[PROOF STEP]
apply (rule geodesic_segment_subparam[of _ _ z _ y])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. geodesic_segment_between {x--z} x z
 2. geodesic_segment_between {x--y} x y
 3. {x--y} \<subseteq> {x--z}
 4. t \<in> {0..dist x y}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
y \<in> {x--z}
t \<in> {0..dist x y}

goal (4 subgoals):
 1. geodesic_segment_between {x--z} x z
 2. geodesic_segment_between {x--y} x y
 3. {x--y} \<subseteq> {x--z}
 4. t \<in> {0..dist x y}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>y \<in> {x--z}; xa \<in> {x--y}; 0 \<le> t; t \<le> dist x y\<rbrakk> \<Longrightarrow> xa \<in> {x--z}
[PROOF STEP]
using geodesic_segment_split(1)[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
{x--z} = {x--y} \<union> {y--z}

goal (1 subgoal):
 1. \<And>xa. \<lbrakk>y \<in> {x--z}; xa \<in> {x--y}; 0 \<le> t; t \<le> dist x y\<rbrakk> \<Longrightarrow> xa \<in> {x--z}
[PROOF STEP]
by auto


[STATEMENT]
lemma middle:
  "dist x (middle x y) = (dist x y)/2"
  "dist (middle x y) y = (dist x y)/2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist x (middle x y) = dist x y / 2 &&& dist (middle x y) y = dist x y / 2
[PROOF STEP]
unfolding middle_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist x (SOME z. dist x z = dist x y / 2 \<and> dist z y = dist x y / 2) = dist x y / 2 &&& dist (SOME z. dist x z = dist x y / 2 \<and> dist z y = dist x y / 2) y = dist x y / 2
[PROOF STEP]
using middles[of x y]
[PROOF STATE]
proof (prove)
using this:
\<exists>z. dist x z = dist x y / 2 \<and> dist z y = dist x y / 2

goal (1 subgoal):
 1. dist x (SOME z. dist x z = dist x y / 2 \<and> dist z y = dist x y / 2) = dist x y / 2 &&& dist (SOME z. dist x z = dist x y / 2 \<and> dist z y = dist x y / 2) y = dist x y / 2
[PROOF STEP]
by (metis (mono_tags, lifting) someI_ex)+


[STATEMENT]
lemma geod_distance_successor:
  "\<forall>a < 2^n. dist (geod n a) (geod n (Suc a)) = dist x0 y0 / 2^n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a<2 ^ n. dist (geod n a) (geod n (Suc a)) = dist x0 y0 / 2 ^ n
[PROOF STEP]
proof (induction n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>a<2 ^ 0. dist (geod 0 a) (geod 0 (Suc a)) = dist x0 y0 / 2 ^ 0
 2. \<And>n. \<forall>a<2 ^ n. dist (geod n a) (geod n (Suc a)) = dist x0 y0 / 2 ^ n \<Longrightarrow> \<forall>a<2 ^ Suc n. dist (geod (Suc n) a) (geod (Suc n) (Suc a)) = dist x0 y0 / 2 ^ Suc n
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<forall>a<2 ^ 0. dist (geod 0 a) (geod 0 (Suc a)) = dist x0 y0 / 2 ^ 0
 2. \<And>n. \<forall>a<2 ^ n. dist (geod n a) (geod n (Suc a)) = dist x0 y0 / 2 ^ n \<Longrightarrow> \<forall>a<2 ^ Suc n. dist (geod (Suc n) a) (geod (Suc n) (Suc a)) = dist x0 y0 / 2 ^ Suc n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a<2 ^ 0. dist (geod 0 a) (geod 0 (Suc a)) = dist x0 y0 / 2 ^ 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>a<2 ^ 0. dist (geod 0 a) (geod 0 (Suc a)) = dist x0 y0 / 2 ^ 0

goal (1 subgoal):
 1. \<And>n. \<forall>a<2 ^ n. dist (geod n a) (geod n (Suc a)) = dist x0 y0 / 2 ^ n \<Longrightarrow> \<forall>a<2 ^ Suc n. dist (geod (Suc n) a) (geod (Suc n) (Suc a)) = dist x0 y0 / 2 ^ Suc n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<forall>a<2 ^ n. dist (geod n a) (geod n (Suc a)) = dist x0 y0 / 2 ^ n \<Longrightarrow> \<forall>a<2 ^ Suc n. dist (geod (Suc n) a) (geod (Suc n) (Suc a)) = dist x0 y0 / 2 ^ Suc n
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
\<forall>a<2 ^ n. dist (geod n a) (geod n (Suc a)) = dist x0 y0 / 2 ^ n

goal (1 subgoal):
 1. \<And>n. \<forall>a<2 ^ n. dist (geod n a) (geod n (Suc a)) = dist x0 y0 / 2 ^ n \<Longrightarrow> \<forall>a<2 ^ Suc n. dist (geod (Suc n) a) (geod (Suc n) (Suc a)) = dist x0 y0 / 2 ^ Suc n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a<2 ^ Suc n. dist (geod (Suc n) a) (geod (Suc n) (Suc a)) = dist x0 y0 / 2 ^ Suc n
[PROOF STEP]
proof (auto)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. a < 2 * 2 ^ n \<Longrightarrow> dist (geod (Suc n) a) (geod (Suc n) (Suc a)) = dist x0 y0 / (2 * 2 ^ n)
[PROOF STEP]
fix a::nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. a < 2 * 2 ^ n \<Longrightarrow> dist (geod (Suc n) a) (geod (Suc n) (Suc a)) = dist x0 y0 / (2 * 2 ^ n)
[PROOF STEP]
assume a: "a < 2 * 2^n"
[PROOF STATE]
proof (state)
this:
a < 2 * 2 ^ n

goal (1 subgoal):
 1. \<And>a. a < 2 * 2 ^ n \<Longrightarrow> dist (geod (Suc n) a) (geod (Suc n) (Suc a)) = dist x0 y0 / (2 * 2 ^ n)
[PROOF STEP]
obtain m where m: "a = 2 * m \<or> a = Suc (2 * m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>m. a = 2 * m \<or> a = Suc (2 * m) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis geod.elims)
[PROOF STATE]
proof (state)
this:
a = 2 * m \<or> a = Suc (2 * m)

goal (1 subgoal):
 1. \<And>a. a < 2 * 2 ^ n \<Longrightarrow> dist (geod (Suc n) a) (geod (Suc n) (Suc a)) = dist x0 y0 / (2 * 2 ^ n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = 2 * m \<or> a = Suc (2 * m)
[PROOF STEP]
have "m < 2^n"
[PROOF STATE]
proof (prove)
using this:
a = 2 * m \<or> a = Suc (2 * m)

goal (1 subgoal):
 1. m < 2 ^ n
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
a = 2 * m \<or> a = Suc (2 * m)
a < 2 * 2 ^ n

goal (1 subgoal):
 1. m < 2 ^ n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m < 2 ^ n

goal (1 subgoal):
 1. \<And>a. a < 2 * 2 ^ n \<Longrightarrow> dist (geod (Suc n) a) (geod (Suc n) (Suc a)) = dist x0 y0 / (2 * 2 ^ n)
[PROOF STEP]
consider "a = 2 * m" | "a = Suc(2*m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a = 2 * m \<Longrightarrow> thesis; a = Suc (2 * m) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using m
[PROOF STATE]
proof (prove)
using this:
a = 2 * m \<or> a = Suc (2 * m)

goal (1 subgoal):
 1. \<lbrakk>a = 2 * m \<Longrightarrow> thesis; a = Suc (2 * m) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>a = 2 * m \<Longrightarrow> ?thesis; a = Suc (2 * m) \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. \<And>a. a < 2 * 2 ^ n \<Longrightarrow> dist (geod (Suc n) a) (geod (Suc n) (Suc a)) = dist x0 y0 / (2 * 2 ^ n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>a = 2 * m \<Longrightarrow> ?thesis; a = Suc (2 * m) \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show "dist (geod (Suc n) a) (geod (Suc n) (Suc a)) = dist x0 y0 / (2 * 2 ^ n)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a = 2 * m \<Longrightarrow> ?thesis; a = Suc (2 * m) \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. dist (geod (Suc n) a) (geod (Suc n) (Suc a)) = dist x0 y0 / (2 * 2 ^ n)
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a = 2 * m \<Longrightarrow> dist (geod (Suc n) a) (geod (Suc n) (Suc a)) = dist x0 y0 / (2 * 2 ^ n)
 2. a = Suc (2 * m) \<Longrightarrow> dist (geod (Suc n) a) (geod (Suc n) (Suc a)) = dist x0 y0 / (2 * 2 ^ n)
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
a = 2 * m

goal (2 subgoals):
 1. a = 2 * m \<Longrightarrow> dist (geod (Suc n) a) (geod (Suc n) (Suc a)) = dist x0 y0 / (2 * 2 ^ n)
 2. a = Suc (2 * m) \<Longrightarrow> dist (geod (Suc n) a) (geod (Suc n) (Suc a)) = dist x0 y0 / (2 * 2 ^ n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (geod (Suc n) a) (geod (Suc n) (Suc a)) = dist x0 y0 / (2 * 2 ^ n)
[PROOF STEP]
unfolding 1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (geod (Suc n) (2 * m)) (geod (Suc n) (Suc (2 * m))) = dist x0 y0 / (2 * 2 ^ n)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (geod n m) (middle (geod n m) (geod n (Suc m))) = dist x0 y0 / (2 * 2 ^ n)
[PROOF STEP]
unfolding middle
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (geod n m) (geod n (Suc m)) / 2 = dist x0 y0 / (2 * 2 ^ n)
[PROOF STEP]
using Suc.IH \<open>m < 2^n\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>a<2 ^ n. dist (geod n a) (geod n (Suc a)) = dist x0 y0 / 2 ^ n
m < 2 ^ n

goal (1 subgoal):
 1. dist (geod n m) (geod n (Suc m)) / 2 = dist x0 y0 / (2 * 2 ^ n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (geod (Suc n) a) (geod (Suc n) (Suc a)) = dist x0 y0 / (2 * 2 ^ n)

goal (1 subgoal):
 1. a = Suc (2 * m) \<Longrightarrow> dist (geod (Suc n) a) (geod (Suc n) (Suc a)) = dist x0 y0 / (2 * 2 ^ n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a = Suc (2 * m) \<Longrightarrow> dist (geod (Suc n) a) (geod (Suc n) (Suc a)) = dist x0 y0 / (2 * 2 ^ n)
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
a = Suc (2 * m)

goal (1 subgoal):
 1. a = Suc (2 * m) \<Longrightarrow> dist (geod (Suc n) a) (geod (Suc n) (Suc a)) = dist x0 y0 / (2 * 2 ^ n)
[PROOF STEP]
have *: "Suc (Suc (2 * m)) = 2 * (Suc m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (Suc (2 * m)) = 2 * Suc m
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc (Suc (2 * m)) = 2 * Suc m

goal (1 subgoal):
 1. a = Suc (2 * m) \<Longrightarrow> dist (geod (Suc n) a) (geod (Suc n) (Suc a)) = dist x0 y0 / (2 * 2 ^ n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (geod (Suc n) a) (geod (Suc n) (Suc a)) = dist x0 y0 / (2 * 2 ^ n)
[PROOF STEP]
unfolding 2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (geod (Suc n) (Suc (2 * m))) (geod (Suc n) (Suc (Suc (2 * m)))) = dist x0 y0 / (2 * 2 ^ n)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (middle (geod n m) (geod n (Suc m))) (geod (Suc n) (Suc (Suc (2 * m)))) = dist x0 y0 / (2 * 2 ^ n)
[PROOF STEP]
unfolding * geod.simps(3) middle
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (geod n m) (geod n (Suc m)) / 2 = dist x0 y0 / (2 * 2 ^ n)
[PROOF STEP]
using Suc.IH \<open>m < 2^n\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>a<2 ^ n. dist (geod n a) (geod n (Suc a)) = dist x0 y0 / 2 ^ n
m < 2 ^ n

goal (1 subgoal):
 1. dist (geod n m) (geod n (Suc m)) / 2 = dist x0 y0 / (2 * 2 ^ n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (geod (Suc n) a) (geod (Suc n) (Suc a)) = dist x0 y0 / (2 * 2 ^ n)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
dist (geod (Suc n) a) (geod (Suc n) (Suc a)) = dist x0 y0 / (2 * 2 ^ n)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>a<2 ^ Suc n. dist (geod (Suc n) a) (geod (Suc n) (Suc a)) = dist x0 y0 / 2 ^ Suc n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma geod_mult:
  "geod n a = geod (n + k) (a * 2^k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geod n a = geod (n + k) (a * 2 ^ k)
[PROOF STEP]
apply (induction k, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. geod n a = geod (n + k) (a * 2 ^ k) \<Longrightarrow> geod (n + k) (a * 2 ^ k) = geod (Suc (n + k)) (a * (2 * 2 ^ k))
[PROOF STEP]
using geod.simps(3)
[PROOF STATE]
proof (prove)
using this:
geod (Suc ?n) (2 * ?m) = geod ?n ?m

goal (1 subgoal):
 1. \<And>k. geod n a = geod (n + k) (a * 2 ^ k) \<Longrightarrow> geod (n + k) (a * 2 ^ k) = geod (Suc (n + k)) (a * (2 * 2 ^ k))
[PROOF STEP]
by (metis mult.left_commute)


[STATEMENT]
lemma geod_0:
  "geod n 0 = x0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geod n 0 = x0
[PROOF STEP]
by (induction n, auto, metis geod.simps(3) semiring_normalization_rules(10))


[STATEMENT]
lemma geod_end:
  "geod n (2^n) = y0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geod n (2 ^ n) = y0
[PROOF STEP]
by (induction n, auto)


[STATEMENT]
lemma geod_upper:
  assumes "a \<le> b" "b \<le> 2^n"
  shows "dist (geod n a) (geod n b) \<le> (b-a) * dist x0 y0 / 2^n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (geod n a) (geod n b) \<le> (real b - real a) * dist x0 y0 / 2 ^ n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist (geod n a) (geod n b) \<le> (real b - real a) * dist x0 y0 / 2 ^ n
[PROOF STEP]
have *: "a+k > 2^n \<or> dist (geod n a) (geod n (a+k)) \<le> k * dist x0 y0 / 2^n" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ n < a + k \<or> dist (geod n a) (geod n (a + k)) \<le> real k * dist x0 y0 / 2 ^ n
[PROOF STEP]
proof (induction k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 2 ^ n < a + 0 \<or> dist (geod n a) (geod n (a + 0)) \<le> real 0 * dist x0 y0 / 2 ^ n
 2. \<And>k. 2 ^ n < a + k \<or> dist (geod n a) (geod n (a + k)) \<le> real k * dist x0 y0 / 2 ^ n \<Longrightarrow> 2 ^ n < a + Suc k \<or> dist (geod n a) (geod n (a + Suc k)) \<le> real (Suc k) * dist x0 y0 / 2 ^ n
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. 2 ^ n < a + 0 \<or> dist (geod n a) (geod n (a + 0)) \<le> real 0 * dist x0 y0 / 2 ^ n
 2. \<And>k. 2 ^ n < a + k \<or> dist (geod n a) (geod n (a + k)) \<le> real k * dist x0 y0 / 2 ^ n \<Longrightarrow> 2 ^ n < a + Suc k \<or> dist (geod n a) (geod n (a + Suc k)) \<le> real (Suc k) * dist x0 y0 / 2 ^ n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ n < a + 0 \<or> dist (geod n a) (geod n (a + 0)) \<le> real 0 * dist x0 y0 / 2 ^ n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
2 ^ n < a + 0 \<or> dist (geod n a) (geod n (a + 0)) \<le> real 0 * dist x0 y0 / 2 ^ n

goal (1 subgoal):
 1. \<And>k. 2 ^ n < a + k \<or> dist (geod n a) (geod n (a + k)) \<le> real k * dist x0 y0 / 2 ^ n \<Longrightarrow> 2 ^ n < a + Suc k \<or> dist (geod n a) (geod n (a + Suc k)) \<le> real (Suc k) * dist x0 y0 / 2 ^ n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. 2 ^ n < a + k \<or> dist (geod n a) (geod n (a + k)) \<le> real k * dist x0 y0 / 2 ^ n \<Longrightarrow> 2 ^ n < a + Suc k \<or> dist (geod n a) (geod n (a + Suc k)) \<le> real (Suc k) * dist x0 y0 / 2 ^ n
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
2 ^ n < a + k \<or> dist (geod n a) (geod n (a + k)) \<le> real k * dist x0 y0 / 2 ^ n

goal (1 subgoal):
 1. \<And>k. 2 ^ n < a + k \<or> dist (geod n a) (geod n (a + k)) \<le> real k * dist x0 y0 / 2 ^ n \<Longrightarrow> 2 ^ n < a + Suc k \<or> dist (geod n a) (geod n (a + Suc k)) \<le> real (Suc k) * dist x0 y0 / 2 ^ n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ n < a + Suc k \<or> dist (geod n a) (geod n (a + Suc k)) \<le> real (Suc k) * dist x0 y0 / 2 ^ n
[PROOF STEP]
proof (cases "2 ^ n < a + Suc k")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 2 ^ n < a + Suc k \<Longrightarrow> 2 ^ n < a + Suc k \<or> dist (geod n a) (geod n (a + Suc k)) \<le> real (Suc k) * dist x0 y0 / 2 ^ n
 2. \<not> 2 ^ n < a + Suc k \<Longrightarrow> 2 ^ n < a + Suc k \<or> dist (geod n a) (geod n (a + Suc k)) \<le> real (Suc k) * dist x0 y0 / 2 ^ n
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
2 ^ n < a + Suc k

goal (2 subgoals):
 1. 2 ^ n < a + Suc k \<Longrightarrow> 2 ^ n < a + Suc k \<or> dist (geod n a) (geod n (a + Suc k)) \<le> real (Suc k) * dist x0 y0 / 2 ^ n
 2. \<not> 2 ^ n < a + Suc k \<Longrightarrow> 2 ^ n < a + Suc k \<or> dist (geod n a) (geod n (a + Suc k)) \<le> real (Suc k) * dist x0 y0 / 2 ^ n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 ^ n < a + Suc k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
2 ^ n < a + Suc k

goal (1 subgoal):
 1. 2 ^ n < a + Suc k \<or> dist (geod n a) (geod n (a + Suc k)) \<le> real (Suc k) * dist x0 y0 / 2 ^ n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
2 ^ n < a + Suc k \<or> dist (geod n a) (geod n (a + Suc k)) \<le> real (Suc k) * dist x0 y0 / 2 ^ n

goal (1 subgoal):
 1. \<not> 2 ^ n < a + Suc k \<Longrightarrow> 2 ^ n < a + Suc k \<or> dist (geod n a) (geod n (a + Suc k)) \<le> real (Suc k) * dist x0 y0 / 2 ^ n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> 2 ^ n < a + Suc k \<Longrightarrow> 2 ^ n < a + Suc k \<or> dist (geod n a) (geod n (a + Suc k)) \<le> real (Suc k) * dist x0 y0 / 2 ^ n
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> 2 ^ n < a + Suc k

goal (1 subgoal):
 1. \<not> 2 ^ n < a + Suc k \<Longrightarrow> 2 ^ n < a + Suc k \<or> dist (geod n a) (geod n (a + Suc k)) \<le> real (Suc k) * dist x0 y0 / 2 ^ n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> 2 ^ n < a + Suc k
[PROOF STEP]
have *: "a + k < 2 ^ n"
[PROOF STATE]
proof (prove)
using this:
\<not> 2 ^ n < a + Suc k

goal (1 subgoal):
 1. a + k < 2 ^ n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a + k < 2 ^ n

goal (1 subgoal):
 1. \<not> 2 ^ n < a + Suc k \<Longrightarrow> 2 ^ n < a + Suc k \<or> dist (geod n a) (geod n (a + Suc k)) \<le> real (Suc k) * dist x0 y0 / 2 ^ n
[PROOF STEP]
have "dist (geod n a) (geod n (a + Suc k)) \<le> dist (geod n a) (geod n (a+k)) + dist (geod n (a+k)) (geod n (a+Suc k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (geod n a) (geod n (a + Suc k)) \<le> dist (geod n a) (geod n (a + k)) + dist (geod n (a + k)) (geod n (a + Suc k))
[PROOF STEP]
using dist_triangle
[PROOF STATE]
proof (prove)
using this:
dist ?x ?z \<le> dist ?x ?y + dist ?y ?z

goal (1 subgoal):
 1. dist (geod n a) (geod n (a + Suc k)) \<le> dist (geod n a) (geod n (a + k)) + dist (geod n (a + k)) (geod n (a + Suc k))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (geod n a) (geod n (a + Suc k)) \<le> dist (geod n a) (geod n (a + k)) + dist (geod n (a + k)) (geod n (a + Suc k))

goal (1 subgoal):
 1. \<not> 2 ^ n < a + Suc k \<Longrightarrow> 2 ^ n < a + Suc k \<or> dist (geod n a) (geod n (a + Suc k)) \<le> real (Suc k) * dist x0 y0 / 2 ^ n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (geod n a) (geod n (a + Suc k)) \<le> dist (geod n a) (geod n (a + k)) + dist (geod n (a + k)) (geod n (a + Suc k))

goal (1 subgoal):
 1. \<not> 2 ^ n < a + Suc k \<Longrightarrow> 2 ^ n < a + Suc k \<or> dist (geod n a) (geod n (a + Suc k)) \<le> real (Suc k) * dist x0 y0 / 2 ^ n
[PROOF STEP]
have "... \<le> k * dist x0 y0 / 2^n + dist x0 y0 / 2^n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (geod n a) (geod n (a + k)) + dist (geod n (a + k)) (geod n (a + Suc k)) \<le> real k * dist x0 y0 / 2 ^ n + dist x0 y0 / 2 ^ n
[PROOF STEP]
using Suc.IH * geod_distance_successor
[PROOF STATE]
proof (prove)
using this:
2 ^ n < a + k \<or> dist (geod n a) (geod n (a + k)) \<le> real k * dist x0 y0 / 2 ^ n
a + k < 2 ^ n
\<forall>a<2 ^ ?n. dist (geod ?n a) (geod ?n (Suc a)) = dist x0 y0 / 2 ^ ?n

goal (1 subgoal):
 1. dist (geod n a) (geod n (a + k)) + dist (geod n (a + k)) (geod n (a + Suc k)) \<le> real k * dist x0 y0 / 2 ^ n + dist x0 y0 / 2 ^ n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (geod n a) (geod n (a + k)) + dist (geod n (a + k)) (geod n (a + Suc k)) \<le> real k * dist x0 y0 / 2 ^ n + dist x0 y0 / 2 ^ n

goal (1 subgoal):
 1. \<not> 2 ^ n < a + Suc k \<Longrightarrow> 2 ^ n < a + Suc k \<or> dist (geod n a) (geod n (a + Suc k)) \<le> real (Suc k) * dist x0 y0 / 2 ^ n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist (geod n a) (geod n (a + Suc k)) \<le> real k * dist x0 y0 / 2 ^ n + dist x0 y0 / 2 ^ n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dist (geod n a) (geod n (a + Suc k)) \<le> real k * dist x0 y0 / 2 ^ n + dist x0 y0 / 2 ^ n

goal (1 subgoal):
 1. 2 ^ n < a + Suc k \<or> dist (geod n a) (geod n (a + Suc k)) \<le> real (Suc k) * dist x0 y0 / 2 ^ n
[PROOF STEP]
by (simp add: add_divide_distrib distrib_left mult.commute)
[PROOF STATE]
proof (state)
this:
2 ^ n < a + Suc k \<or> dist (geod n a) (geod n (a + Suc k)) \<le> real (Suc k) * dist x0 y0 / 2 ^ n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
2 ^ n < a + Suc k \<or> dist (geod n a) (geod n (a + Suc k)) \<le> real (Suc k) * dist x0 y0 / 2 ^ n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
2 ^ n < a + ?k \<or> dist (geod n a) (geod n (a + ?k)) \<le> real ?k * dist x0 y0 / 2 ^ n

goal (1 subgoal):
 1. dist (geod n a) (geod n b) \<le> (real b - real a) * dist x0 y0 / 2 ^ n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (geod n a) (geod n b) \<le> (real b - real a) * dist x0 y0 / 2 ^ n
[PROOF STEP]
using *[of "b-a"] assms
[PROOF STATE]
proof (prove)
using this:
2 ^ n < a + (b - a) \<or> dist (geod n a) (geod n (a + (b - a))) \<le> real (b - a) * dist x0 y0 / 2 ^ n
a \<le> b
b \<le> 2 ^ n

goal (1 subgoal):
 1. dist (geod n a) (geod n b) \<le> (real b - real a) * dist x0 y0 / 2 ^ n
[PROOF STEP]
by (simp add: of_nat_diff)
[PROOF STATE]
proof (state)
this:
dist (geod n a) (geod n b) \<le> (real b - real a) * dist x0 y0 / 2 ^ n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma geod_dist:
  assumes "a \<le> b" "b \<le> 2^n"
  shows "dist (geod n a) (geod n b) = (b-a) * dist x0 y0 / 2^n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (geod n a) (geod n b) = (real b - real a) * dist x0 y0 / 2 ^ n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist (geod n a) (geod n b) = (real b - real a) * dist x0 y0 / 2 ^ n
[PROOF STEP]
have "dist (geod n a) (geod n b) \<le> (real b-a) * dist x0 y0 / 2^n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (geod n a) (geod n b) \<le> (real b - real a) * dist x0 y0 / 2 ^ n
[PROOF STEP]
using geod_upper[of a b n] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a \<le> b; b \<le> 2 ^ n\<rbrakk> \<Longrightarrow> dist (geod n a) (geod n b) \<le> (real b - real a) * dist x0 y0 / 2 ^ n
a \<le> b
b \<le> 2 ^ n

goal (1 subgoal):
 1. dist (geod n a) (geod n b) \<le> (real b - real a) * dist x0 y0 / 2 ^ n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (geod n a) (geod n b) \<le> (real b - real a) * dist x0 y0 / 2 ^ n

goal (1 subgoal):
 1. dist (geod n a) (geod n b) = (real b - real a) * dist x0 y0 / 2 ^ n
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
dist (geod n a) (geod n b) \<le> (real b - real a) * dist x0 y0 / 2 ^ n

goal (1 subgoal):
 1. dist (geod n a) (geod n b) = (real b - real a) * dist x0 y0 / 2 ^ n
[PROOF STEP]
have "\<not> (dist (geod n a) (geod n b) < (real b-a) * dist x0 y0 / 2^n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> dist (geod n a) (geod n b) < (real b - real a) * dist x0 y0 / 2 ^ n
[PROOF STEP]
proof (rule ccontr, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist (geod n a) (geod n b) < (real b - real a) * dist x0 y0 / 2 ^ n \<Longrightarrow> False
[PROOF STEP]
assume *: "dist (geod n a) (geod n b) < (real b-a) * dist x0 y0 / 2^n"
[PROOF STATE]
proof (state)
this:
dist (geod n a) (geod n b) < (real b - real a) * dist x0 y0 / 2 ^ n

goal (1 subgoal):
 1. dist (geod n a) (geod n b) < (real b - real a) * dist x0 y0 / 2 ^ n \<Longrightarrow> False
[PROOF STEP]
have "dist x0 y0 = dist (geod n 0) (geod n (2^n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist x0 y0 = dist (geod n 0) (geod n (2 ^ n))
[PROOF STEP]
using geod_0 geod_end
[PROOF STATE]
proof (prove)
using this:
geod ?n 0 = x0
geod ?n (2 ^ ?n) = y0

goal (1 subgoal):
 1. dist x0 y0 = dist (geod n 0) (geod n (2 ^ n))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist x0 y0 = dist (geod n 0) (geod n (2 ^ n))

goal (1 subgoal):
 1. dist (geod n a) (geod n b) < (real b - real a) * dist x0 y0 / 2 ^ n \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist x0 y0 = dist (geod n 0) (geod n (2 ^ n))

goal (1 subgoal):
 1. dist (geod n a) (geod n b) < (real b - real a) * dist x0 y0 / 2 ^ n \<Longrightarrow> False
[PROOF STEP]
have "... \<le> dist (geod n 0) (geod n a) + dist (geod n a) (geod n b) + dist (geod n b) (geod n (2^n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (geod n 0) (geod n (2 ^ n)) \<le> dist (geod n 0) (geod n a) + dist (geod n a) (geod n b) + dist (geod n b) (geod n (2 ^ n))
[PROOF STEP]
using dist_triangle4
[PROOF STATE]
proof (prove)
using this:
dist ?x ?t \<le> dist ?x ?y + dist ?y ?z + dist ?z ?t

goal (1 subgoal):
 1. dist (geod n 0) (geod n (2 ^ n)) \<le> dist (geod n 0) (geod n a) + dist (geod n a) (geod n b) + dist (geod n b) (geod n (2 ^ n))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (geod n 0) (geod n (2 ^ n)) \<le> dist (geod n 0) (geod n a) + dist (geod n a) (geod n b) + dist (geod n b) (geod n (2 ^ n))

goal (1 subgoal):
 1. dist (geod n a) (geod n b) < (real b - real a) * dist x0 y0 / 2 ^ n \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (geod n 0) (geod n (2 ^ n)) \<le> dist (geod n 0) (geod n a) + dist (geod n a) (geod n b) + dist (geod n b) (geod n (2 ^ n))

goal (1 subgoal):
 1. dist (geod n a) (geod n b) < (real b - real a) * dist x0 y0 / 2 ^ n \<Longrightarrow> False
[PROOF STEP]
have "... < a * dist x0 y0 / 2^n + (real b-a) * dist x0 y0 / 2^n + (2^n - real b) * dist x0 y0 / 2^n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (geod n 0) (geod n a) + dist (geod n a) (geod n b) + dist (geod n b) (geod n (2 ^ n)) < real a * dist x0 y0 / 2 ^ n + (real b - real a) * dist x0 y0 / 2 ^ n + (2 ^ n - real b) * dist x0 y0 / 2 ^ n
[PROOF STEP]
using * assms geod_upper[of 0 a n] geod_upper[of b "2^n" n]
[PROOF STATE]
proof (prove)
using this:
dist (geod n a) (geod n b) < (real b - real a) * dist x0 y0 / 2 ^ n
a \<le> b
b \<le> 2 ^ n
\<lbrakk>0 \<le> a; a \<le> 2 ^ n\<rbrakk> \<Longrightarrow> dist (geod n 0) (geod n a) \<le> (real a - real 0) * dist x0 y0 / 2 ^ n
\<lbrakk>b \<le> 2 ^ n; 2 ^ n \<le> 2 ^ n\<rbrakk> \<Longrightarrow> dist (geod n b) (geod n (2 ^ n)) \<le> (real (2 ^ n) - real b) * dist x0 y0 / 2 ^ n

goal (1 subgoal):
 1. dist (geod n 0) (geod n a) + dist (geod n a) (geod n b) + dist (geod n b) (geod n (2 ^ n)) < real a * dist x0 y0 / 2 ^ n + (real b - real a) * dist x0 y0 / 2 ^ n + (2 ^ n - real b) * dist x0 y0 / 2 ^ n
[PROOF STEP]
by (auto intro: mono_intros)
[PROOF STATE]
proof (state)
this:
dist (geod n 0) (geod n a) + dist (geod n a) (geod n b) + dist (geod n b) (geod n (2 ^ n)) < real a * dist x0 y0 / 2 ^ n + (real b - real a) * dist x0 y0 / 2 ^ n + (2 ^ n - real b) * dist x0 y0 / 2 ^ n

goal (1 subgoal):
 1. dist (geod n a) (geod n b) < (real b - real a) * dist x0 y0 / 2 ^ n \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (geod n 0) (geod n a) + dist (geod n a) (geod n b) + dist (geod n b) (geod n (2 ^ n)) < real a * dist x0 y0 / 2 ^ n + (real b - real a) * dist x0 y0 / 2 ^ n + (2 ^ n - real b) * dist x0 y0 / 2 ^ n

goal (1 subgoal):
 1. dist (geod n a) (geod n b) < (real b - real a) * dist x0 y0 / 2 ^ n \<Longrightarrow> False
[PROOF STEP]
have "... = dist x0 y0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real a * dist x0 y0 / 2 ^ n + (real b - real a) * dist x0 y0 / 2 ^ n + (2 ^ n - real b) * dist x0 y0 / 2 ^ n = dist x0 y0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<le> b
b \<le> 2 ^ n

goal (1 subgoal):
 1. real a * dist x0 y0 / 2 ^ n + (real b - real a) * dist x0 y0 / 2 ^ n + (2 ^ n - real b) * dist x0 y0 / 2 ^ n = dist x0 y0
[PROOF STEP]
by (auto simp add: algebra_simps divide_simps)
[PROOF STATE]
proof (state)
this:
real a * dist x0 y0 / 2 ^ n + (real b - real a) * dist x0 y0 / 2 ^ n + (2 ^ n - real b) * dist x0 y0 / 2 ^ n = dist x0 y0

goal (1 subgoal):
 1. dist (geod n a) (geod n b) < (real b - real a) * dist x0 y0 / 2 ^ n \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist x0 y0 < dist x0 y0
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
dist x0 y0 < dist x0 y0

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> dist (geod n a) (geod n b) < (real b - real a) * dist x0 y0 / 2 ^ n

goal (1 subgoal):
 1. dist (geod n a) (geod n b) = (real b - real a) * dist x0 y0 / 2 ^ n
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
dist (geod n a) (geod n b) \<le> (real b - real a) * dist x0 y0 / 2 ^ n
\<not> dist (geod n a) (geod n b) < (real b - real a) * dist x0 y0 / 2 ^ n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dist (geod n a) (geod n b) \<le> (real b - real a) * dist x0 y0 / 2 ^ n
\<not> dist (geod n a) (geod n b) < (real b - real a) * dist x0 y0 / 2 ^ n

goal (1 subgoal):
 1. dist (geod n a) (geod n b) = (real b - real a) * dist x0 y0 / 2 ^ n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (geod n a) (geod n b) = (real b - real a) * dist x0 y0 / 2 ^ n

goal:
No subgoals!
[PROOF STEP]
qed