[STATEMENT]
lemma (in Gromov_hyperbolic_space_geodesic) Morse_Gromov_theorem_aux2:
  fixes f::"real \<Rightarrow> 'a"
  assumes "continuous_on {a..b} f"
          "lambda C-quasi_isometry_on {a..b} f"
          "geodesic_segment_between G (f a) (f b)"
  shows "hausdorff_distance (f`{a..b}) G \<le> lambda^2 * (11/2 * C + 92 * deltaG(TYPE('a)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hausdorff_distance (f ` {a..b}) G \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
[PROOF STEP]
proof (cases "a \<le> b")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
 2. \<not> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a \<le> b

goal (2 subgoals):
 1. a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
 2. \<not> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
[PROOF STEP]
have "lambda \<ge> 1" "C \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> lambda &&& 0 \<le> C
[PROOF STEP]
using quasi_isometry_onD[OF assms(2)]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> {a..b}; ?y \<in> {a..b}\<rbrakk> \<Longrightarrow> dist (f ?x) (f ?y) \<le> lambda * dist ?x ?y + C
\<lbrakk>?x \<in> {a..b}; ?y \<in> {a..b}\<rbrakk> \<Longrightarrow> 1 / lambda * dist ?x ?y - C \<le> dist (f ?x) (f ?y)
1 \<le> lambda
0 \<le> C

goal (1 subgoal):
 1. 1 \<le> lambda &&& 0 \<le> C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 \<le> lambda
0 \<le> C

goal (2 subgoals):
 1. a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
 2. \<not> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
[PROOF STEP]
have *: "infdist (f z) G \<le> lambda^2 * (11/2 * C + 91 * delta)" if "z \<in> {a..b}" "delta > deltaG(TYPE('a))" for z delta
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infdist (f z) G \<le> lambda\<^sup>2 * (11 / 2 * C + 91 * delta)
[PROOF STEP]
by (rule Morse_Gromov_theorem_aux1[OF assms(1) assms(2) True assms(3) that])
[PROOF STATE]
proof (state)
this:
\<lbrakk>?z \<in> {a..b}; deltaG TYPE('a) < ?delta\<rbrakk> \<Longrightarrow> infdist (f ?z) G \<le> lambda\<^sup>2 * (11 / 2 * C + 91 * ?delta)

goal (2 subgoals):
 1. a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
 2. \<not> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
[PROOF STEP]
define D where "D = lambda^2 * (11/2 * C + 91 * deltaG(TYPE('a)))"
[PROOF STATE]
proof (state)
this:
D = lambda\<^sup>2 * (11 / 2 * C + 91 * deltaG TYPE('a))

goal (2 subgoals):
 1. a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
 2. \<not> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
[PROOF STEP]
have "D \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> D
[PROOF STEP]
unfolding D_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> lambda\<^sup>2 * (11 / 2 * C + 91 * deltaG TYPE('a))
[PROOF STEP]
using \<open>C \<ge> 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 \<le> C

goal (1 subgoal):
 1. 0 \<le> lambda\<^sup>2 * (11 / 2 * C + 91 * deltaG TYPE('a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> D

goal (2 subgoals):
 1. a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
 2. \<not> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
[PROOF STEP]
have I: "infdist (f z) G \<le> D" if "z \<in> {a..b}" for z
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infdist (f z) G \<le> D
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. infdist (f z) G \<le> D
[PROOF STEP]
have "(infdist (f z) G/ lambda^2 - 11/2 * C)/91 \<le> delta" if "delta > deltaG(TYPE('a))" for delta
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (infdist (f z) G / lambda\<^sup>2 - 11 / 2 * C) / 91 \<le> delta
[PROOF STEP]
using *[OF \<open>z \<in> {a..b}\<close> that] \<open>lambda \<ge> 1\<close>
[PROOF STATE]
proof (prove)
using this:
infdist (f z) G \<le> lambda\<^sup>2 * (11 / 2 * C + 91 * delta)
1 \<le> lambda

goal (1 subgoal):
 1. (infdist (f z) G / lambda\<^sup>2 - 11 / 2 * C) / 91 \<le> delta
[PROOF STEP]
by (auto simp add: divide_simps algebra_simps)
[PROOF STATE]
proof (state)
this:
deltaG TYPE('a) < ?delta \<Longrightarrow> (infdist (f z) G / lambda\<^sup>2 - 11 / 2 * C) / 91 \<le> ?delta

goal (1 subgoal):
 1. infdist (f z) G \<le> D
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
deltaG TYPE('a) < ?delta \<Longrightarrow> (infdist (f z) G / lambda\<^sup>2 - 11 / 2 * C) / 91 \<le> ?delta
[PROOF STEP]
have "(infdist (f z) G/ lambda^2 - 11/2 * C)/91 \<le> deltaG(TYPE('a))"
[PROOF STATE]
proof (prove)
using this:
deltaG TYPE('a) < ?delta \<Longrightarrow> (infdist (f z) G / lambda\<^sup>2 - 11 / 2 * C) / 91 \<le> ?delta

goal (1 subgoal):
 1. (infdist (f z) G / lambda\<^sup>2 - 11 / 2 * C) / 91 \<le> deltaG TYPE('a)
[PROOF STEP]
using dense_ge
[PROOF STATE]
proof (prove)
using this:
deltaG TYPE('a) < ?delta \<Longrightarrow> (infdist (f z) G / lambda\<^sup>2 - 11 / 2 * C) / 91 \<le> ?delta
(\<And>x. ?z < x \<Longrightarrow> ?y \<le> x) \<Longrightarrow> ?y \<le> ?z

goal (1 subgoal):
 1. (infdist (f z) G / lambda\<^sup>2 - 11 / 2 * C) / 91 \<le> deltaG TYPE('a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(infdist (f z) G / lambda\<^sup>2 - 11 / 2 * C) / 91 \<le> deltaG TYPE('a)

goal (1 subgoal):
 1. infdist (f z) G \<le> D
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(infdist (f z) G / lambda\<^sup>2 - 11 / 2 * C) / 91 \<le> deltaG TYPE('a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(infdist (f z) G / lambda\<^sup>2 - 11 / 2 * C) / 91 \<le> deltaG TYPE('a)

goal (1 subgoal):
 1. infdist (f z) G \<le> D
[PROOF STEP]
unfolding D_def
[PROOF STATE]
proof (prove)
using this:
(infdist (f z) G / lambda\<^sup>2 - 11 / 2 * C) / 91 \<le> deltaG TYPE('a)

goal (1 subgoal):
 1. infdist (f z) G \<le> lambda\<^sup>2 * (11 / 2 * C + 91 * deltaG TYPE('a))
[PROOF STEP]
using \<open>lambda \<ge> 1\<close>
[PROOF STATE]
proof (prove)
using this:
(infdist (f z) G / lambda\<^sup>2 - 11 / 2 * C) / 91 \<le> deltaG TYPE('a)
1 \<le> lambda

goal (1 subgoal):
 1. infdist (f z) G \<le> lambda\<^sup>2 * (11 / 2 * C + 91 * deltaG TYPE('a))
[PROOF STEP]
by (auto simp add: divide_simps algebra_simps)
[PROOF STATE]
proof (state)
this:
infdist (f z) G \<le> D

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?z \<in> {a..b} \<Longrightarrow> infdist (f ?z) G \<le> D

goal (2 subgoals):
 1. a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
 2. \<not> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hausdorff_distance (f ` {a..b}) G \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
[PROOF STEP]
proof (rule hausdorff_distanceI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. x \<in> f ` {a..b} \<Longrightarrow> infdist x G \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
 2. \<And>x. x \<in> G \<Longrightarrow> infdist x (f ` {a..b}) \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
 3. 0 \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
[PROOF STEP]
show "0 \<le> lambda\<^sup>2 * (11/2 * C + 92 * deltaG TYPE('a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
[PROOF STEP]
using \<open>C \<ge> 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 \<le> C

goal (1 subgoal):
 1. 0 \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))

goal (2 subgoals):
 1. \<And>x. x \<in> f ` {a..b} \<Longrightarrow> infdist x G \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
 2. \<And>x. x \<in> G \<Longrightarrow> infdist x (f ` {a..b}) \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> f ` {a..b} \<Longrightarrow> infdist x G \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
 2. \<And>x. x \<in> G \<Longrightarrow> infdist x (f ` {a..b}) \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
[PROOF STEP]
assume "x \<in> f`{a..b}"
[PROOF STATE]
proof (state)
this:
x \<in> f ` {a..b}

goal (2 subgoals):
 1. \<And>x. x \<in> f ` {a..b} \<Longrightarrow> infdist x G \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
 2. \<And>x. x \<in> G \<Longrightarrow> infdist x (f ` {a..b}) \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> f ` {a..b}
[PROOF STEP]
obtain z where z: "x = f z" "z \<in> {a..b}"
[PROOF STATE]
proof (prove)
using this:
x \<in> f ` {a..b}

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

goal (2 subgoals):
 1. \<And>x. x \<in> f ` {a..b} \<Longrightarrow> infdist x G \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
 2. \<And>x. x \<in> G \<Longrightarrow> infdist x (f ` {a..b}) \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
[PROOF STEP]
show "infdist x G \<le> lambda\<^sup>2 * (11/2 * C + 92 * deltaG TYPE('a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infdist x G \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
[PROOF STEP]
unfolding z(1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infdist (f z) G \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
[PROOF STEP]
by (rule order_trans[OF I[OF \<open>z \<in> {a..b}\<close>]], auto simp add: algebra_simps D_def)
[PROOF STATE]
proof (state)
this:
infdist x G \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))

goal (1 subgoal):
 1. \<And>x. x \<in> G \<Longrightarrow> infdist x (f ` {a..b}) \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> G \<Longrightarrow> infdist x (f ` {a..b}) \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> G \<Longrightarrow> infdist x (f ` {a..b}) \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
[PROOF STEP]
assume "x \<in> G"
[PROOF STATE]
proof (state)
this:
x \<in> G

goal (1 subgoal):
 1. \<And>x. x \<in> G \<Longrightarrow> infdist x (f ` {a..b}) \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
[PROOF STEP]
have "infdist x (f`{a..b}) \<le> D + 1 * deltaG TYPE('a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infdist x (f ` {a..b}) \<le> D + 1 * deltaG TYPE('a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. infdist x (f ` {a..b}) \<le> D + 1 * deltaG TYPE('a)
[PROOF STEP]
define p where "p = geodesic_segment_param G (f a)"
[PROOF STATE]
proof (state)
this:
p = geodesic_segment_param G (f a)

goal (1 subgoal):
 1. infdist x (f ` {a..b}) \<le> D + 1 * deltaG TYPE('a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = geodesic_segment_param G (f a)
[PROOF STEP]
have p: "p 0 = f a" "p (dist (f a) (f b)) = f b"
[PROOF STATE]
proof (prove)
using this:
p = geodesic_segment_param G (f a)

goal (1 subgoal):
 1. p 0 = f a &&& p (dist (f a) (f b)) = f b
[PROOF STEP]
unfolding p_def
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_param G (f a) = geodesic_segment_param G (f a)

goal (1 subgoal):
 1. geodesic_segment_param G (f a) 0 = f a &&& geodesic_segment_param G (f a) (dist (f a) (f b)) = f b
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_param G (f a) = geodesic_segment_param G (f a)
geodesic_segment_between G (f a) (f b)

goal (1 subgoal):
 1. geodesic_segment_param G (f a) 0 = f a &&& geodesic_segment_param G (f a) (dist (f a) (f b)) = f b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p 0 = f a
p (dist (f a) (f b)) = f b

goal (1 subgoal):
 1. infdist x (f ` {a..b}) \<le> D + 1 * deltaG TYPE('a)
[PROOF STEP]
obtain t where t: "x = p t" "t \<in> {0..dist (f a) (f b)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t. \<lbrakk>x = p t; t \<in> {0..dist (f a) (f b)}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding p_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t. \<lbrakk>x = geodesic_segment_param G (f a) t; t \<in> {0..dist (f a) (f b)}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>x \<in> G\<close> \<open>geodesic_segment_between G (f a) (f b)\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> G
geodesic_segment_between G (f a) (f b)

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>x = geodesic_segment_param G (f a) t; t \<in> {0..dist (f a) (f b)}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis geodesic_segment_param(5) imageE)
[PROOF STATE]
proof (state)
this:
x = p t
t \<in> {0..dist (f a) (f b)}

goal (1 subgoal):
 1. infdist x (f ` {a..b}) \<le> D + 1 * deltaG TYPE('a)
[PROOF STEP]
define Km where "Km = (\<Union>z \<in> p`{0..t}. cball z D)"
[PROOF STATE]
proof (state)
this:
Km = (\<Union>z\<in>p ` {0..t}. cball z D)

goal (1 subgoal):
 1. infdist x (f ` {a..b}) \<le> D + 1 * deltaG TYPE('a)
[PROOF STEP]
define KM where "KM = (\<Union>z \<in> p`{t..dist (f a) (f b)}. cball z D)"
[PROOF STATE]
proof (state)
this:
KM = (\<Union>z\<in>p ` {t..dist (f a) (f b)}. cball z D)

goal (1 subgoal):
 1. infdist x (f ` {a..b}) \<le> D + 1 * deltaG TYPE('a)
[PROOF STEP]
have "f`{a..b} \<subseteq> Km \<union> KM"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` {a..b} \<subseteq> Km \<union> KM
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> f ` {a..b} \<Longrightarrow> x \<in> Km \<union> KM
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> f ` {a..b} \<Longrightarrow> x \<in> Km \<union> KM
[PROOF STEP]
assume x: "x \<in> f`{a..b}"
[PROOF STATE]
proof (state)
this:
x \<in> f ` {a..b}

goal (1 subgoal):
 1. \<And>x. x \<in> f ` {a..b} \<Longrightarrow> x \<in> Km \<union> KM
[PROOF STEP]
have "\<exists>z \<in> G. infdist x G = dist x z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>z\<in>G. infdist x G = dist x z
[PROOF STEP]
apply (rule infdist_proper_attained)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. proper G
 2. G \<noteq> {}
[PROOF STEP]
using geodesic_segment_topology[OF geodesic_segmentI[OF assms(3)]]
[PROOF STATE]
proof (prove)
using this:
compact G
connected G
path_connected G
bounded G
closed G
G \<noteq> {}
proper G

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

goal (1 subgoal):
 1. \<And>x. x \<in> f ` {a..b} \<Longrightarrow> x \<in> Km \<union> KM
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>z\<in>G. infdist x G = dist x z
[PROOF STEP]
obtain z where z: "z \<in> G" "infdist x G = dist x z"
[PROOF STATE]
proof (prove)
using this:
\<exists>z\<in>G. infdist x G = dist x z

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

goal (1 subgoal):
 1. \<And>x. x \<in> f ` {a..b} \<Longrightarrow> x \<in> Km \<union> KM
[PROOF STEP]
obtain tz where tz: "z = p tz" "tz \<in> {0..dist (f a) (f b)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>tz. \<lbrakk>z = p tz; tz \<in> {0..dist (f a) (f b)}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding p_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>tz. \<lbrakk>z = geodesic_segment_param G (f a) tz; tz \<in> {0..dist (f a) (f b)}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>z \<in> G\<close> \<open>geodesic_segment_between G (f a) (f b)\<close>
[PROOF STATE]
proof (prove)
using this:
z \<in> G
geodesic_segment_between G (f a) (f b)

goal (1 subgoal):
 1. (\<And>tz. \<lbrakk>z = geodesic_segment_param G (f a) tz; tz \<in> {0..dist (f a) (f b)}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis geodesic_segment_param(5) imageE)
[PROOF STATE]
proof (state)
this:
z = p tz
tz \<in> {0..dist (f a) (f b)}

goal (1 subgoal):
 1. \<And>x. x \<in> f ` {a..b} \<Longrightarrow> x \<in> Km \<union> KM
[PROOF STEP]
have "infdist x G \<le> D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infdist x G \<le> D
[PROOF STEP]
using I \<open>x \<in> f`{a..b}\<close>
[PROOF STATE]
proof (prove)
using this:
?z \<in> {a..b} \<Longrightarrow> infdist (f ?z) G \<le> D
x \<in> f ` {a..b}

goal (1 subgoal):
 1. infdist x G \<le> D
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
infdist x G \<le> D

goal (1 subgoal):
 1. \<And>x. x \<in> f ` {a..b} \<Longrightarrow> x \<in> Km \<union> KM
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
infdist x G \<le> D
[PROOF STEP]
have "dist z x \<le> D"
[PROOF STATE]
proof (prove)
using this:
infdist x G \<le> D

goal (1 subgoal):
 1. dist z x \<le> D
[PROOF STEP]
using z(2)
[PROOF STATE]
proof (prove)
using this:
infdist x G \<le> D
infdist x G = dist x z

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

goal (1 subgoal):
 1. \<And>x. x \<in> f ` {a..b} \<Longrightarrow> x \<in> Km \<union> KM
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dist z x \<le> D
[PROOF STEP]
show "x \<in> Km \<union> KM"
[PROOF STATE]
proof (prove)
using this:
dist z x \<le> D

goal (1 subgoal):
 1. x \<in> Km \<union> KM
[PROOF STEP]
unfolding Km_def KM_def
[PROOF STATE]
proof (prove)
using this:
dist z x \<le> D

goal (1 subgoal):
 1. x \<in> (\<Union>z\<in>p ` {0..t}. cball z D) \<union> (\<Union>z\<in>p ` {t..dist (f a) (f b)}. cball z D)
[PROOF STEP]
using tz
[PROOF STATE]
proof (prove)
using this:
dist z x \<le> D
z = p tz
tz \<in> {0..dist (f a) (f b)}

goal (1 subgoal):
 1. x \<in> (\<Union>z\<in>p ` {0..t}. cball z D) \<union> (\<Union>z\<in>p ` {t..dist (f a) (f b)}. cball z D)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
x \<in> Km \<union> KM

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f ` {a..b} \<subseteq> Km \<union> KM

goal (1 subgoal):
 1. infdist x (f ` {a..b}) \<le> D + 1 * deltaG TYPE('a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f ` {a..b} \<subseteq> Km \<union> KM
[PROOF STEP]
have *: "f`{a..b} = (Km \<inter> f`{a..b}) \<union> (KM \<inter> f`{a..b})"
[PROOF STATE]
proof (prove)
using this:
f ` {a..b} \<subseteq> Km \<union> KM

goal (1 subgoal):
 1. f ` {a..b} = Km \<inter> f ` {a..b} \<union> KM \<inter> f ` {a..b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f ` {a..b} = Km \<inter> f ` {a..b} \<union> KM \<inter> f ` {a..b}

goal (1 subgoal):
 1. infdist x (f ` {a..b}) \<le> D + 1 * deltaG TYPE('a)
[PROOF STEP]
have "(Km \<inter> f`{a..b}) \<inter> (KM \<inter> f`{a..b}) \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Km \<inter> f ` {a..b} \<inter> (KM \<inter> f ` {a..b}) \<noteq> {}
[PROOF STEP]
proof (rule connected_as_closed_union[OF _ *])
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. connected (f ` {a..b})
 2. closed (Km \<inter> f ` {a..b})
 3. closed (KM \<inter> f ` {a..b})
 4. Km \<inter> f ` {a..b} \<noteq> {}
 5. KM \<inter> f ` {a..b} \<noteq> {}
[PROOF STEP]
have "closed (f ` {a..b})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed (f ` {a..b})
[PROOF STEP]
apply (intro compact_imp_closed compact_continuous_image)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. continuous_on {a..b} f
 2. compact {a..b}
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
continuous_on {a..b} f

goal (2 subgoals):
 1. continuous_on {a..b} f
 2. compact {a..b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
closed (f ` {a..b})

goal (5 subgoals):
 1. connected (f ` {a..b})
 2. closed (Km \<inter> f ` {a..b})
 3. closed (KM \<inter> f ` {a..b})
 4. Km \<inter> f ` {a..b} \<noteq> {}
 5. KM \<inter> f ` {a..b} \<noteq> {}
[PROOF STEP]
have "closed Km"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed Km
[PROOF STEP]
unfolding Km_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed (\<Union>z\<in>p ` {0..t}. cball z D)
[PROOF STEP]
apply (intro compact_has_closed_thickening compact_continuous_image)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. continuous_on {0..t} p
 2. compact {0..t}
 3. continuous_on (p ` {0..t}) (\<lambda>x. D)
[PROOF STEP]
apply (rule continuous_on_subset[of "{0..dist (f a) (f b)}" p])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. continuous_on {0..dist (f a) (f b)} p
 2. {0..t} \<subseteq> {0..dist (f a) (f b)}
 3. compact {0..t}
 4. continuous_on (p ` {0..t}) (\<lambda>x. D)
[PROOF STEP]
unfolding p_def
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. continuous_on {0..dist (f a) (f b)} (geodesic_segment_param G (f a))
 2. {0..t} \<subseteq> {0..dist (f a) (f b)}
 3. compact {0..t}
 4. continuous_on (geodesic_segment_param G (f a) ` {0..t}) (\<lambda>x. D)
[PROOF STEP]
using assms(3) \<open>t \<in> {0..dist (f a) (f b)}\<close>
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_between G (f a) (f b)
t \<in> {0..dist (f a) (f b)}

goal (4 subgoals):
 1. continuous_on {0..dist (f a) (f b)} (geodesic_segment_param G (f a))
 2. {0..t} \<subseteq> {0..dist (f a) (f b)}
 3. compact {0..t}
 4. continuous_on (geodesic_segment_param G (f a) ` {0..t}) (\<lambda>x. D)
[PROOF STEP]
by (auto simp add: isometry_on_continuous)
[PROOF STATE]
proof (state)
this:
closed Km

goal (5 subgoals):
 1. connected (f ` {a..b})
 2. closed (Km \<inter> f ` {a..b})
 3. closed (KM \<inter> f ` {a..b})
 4. Km \<inter> f ` {a..b} \<noteq> {}
 5. KM \<inter> f ` {a..b} \<noteq> {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
closed Km
[PROOF STEP]
show "closed (Km \<inter> f`{a..b})"
[PROOF STATE]
proof (prove)
using this:
closed Km

goal (1 subgoal):
 1. closed (Km \<inter> f ` {a..b})
[PROOF STEP]
by (rule topological_space_class.closed_Int) fact
[PROOF STATE]
proof (state)
this:
closed (Km \<inter> f ` {a..b})

goal (4 subgoals):
 1. connected (f ` {a..b})
 2. closed (KM \<inter> f ` {a..b})
 3. Km \<inter> f ` {a..b} \<noteq> {}
 4. KM \<inter> f ` {a..b} \<noteq> {}
[PROOF STEP]
have "closed KM"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed KM
[PROOF STEP]
unfolding KM_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed (\<Union>z\<in>p ` {t..dist (f a) (f b)}. cball z D)
[PROOF STEP]
apply (intro compact_has_closed_thickening compact_continuous_image)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. continuous_on {t..dist (f a) (f b)} p
 2. compact {t..dist (f a) (f b)}
 3. continuous_on (p ` {t..dist (f a) (f b)}) (\<lambda>x. D)
[PROOF STEP]
apply (rule continuous_on_subset[of "{0..dist (f a) (f b)}" p])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. continuous_on {0..dist (f a) (f b)} p
 2. {t..dist (f a) (f b)} \<subseteq> {0..dist (f a) (f b)}
 3. compact {t..dist (f a) (f b)}
 4. continuous_on (p ` {t..dist (f a) (f b)}) (\<lambda>x. D)
[PROOF STEP]
unfolding p_def
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. continuous_on {0..dist (f a) (f b)} (geodesic_segment_param G (f a))
 2. {t..dist (f a) (f b)} \<subseteq> {0..dist (f a) (f b)}
 3. compact {t..dist (f a) (f b)}
 4. continuous_on (geodesic_segment_param G (f a) ` {t..dist (f a) (f b)}) (\<lambda>x. D)
[PROOF STEP]
using assms(3) \<open>t \<in> {0..dist (f a) (f b)}\<close>
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_between G (f a) (f b)
t \<in> {0..dist (f a) (f b)}

goal (4 subgoals):
 1. continuous_on {0..dist (f a) (f b)} (geodesic_segment_param G (f a))
 2. {t..dist (f a) (f b)} \<subseteq> {0..dist (f a) (f b)}
 3. compact {t..dist (f a) (f b)}
 4. continuous_on (geodesic_segment_param G (f a) ` {t..dist (f a) (f b)}) (\<lambda>x. D)
[PROOF STEP]
by (auto simp add: isometry_on_continuous)
[PROOF STATE]
proof (state)
this:
closed KM

goal (4 subgoals):
 1. connected (f ` {a..b})
 2. closed (KM \<inter> f ` {a..b})
 3. Km \<inter> f ` {a..b} \<noteq> {}
 4. KM \<inter> f ` {a..b} \<noteq> {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
closed KM
[PROOF STEP]
show "closed (KM \<inter> f`{a..b})"
[PROOF STATE]
proof (prove)
using this:
closed KM

goal (1 subgoal):
 1. closed (KM \<inter> f ` {a..b})
[PROOF STEP]
by (rule topological_space_class.closed_Int) fact
[PROOF STATE]
proof (state)
this:
closed (KM \<inter> f ` {a..b})

goal (3 subgoals):
 1. connected (f ` {a..b})
 2. Km \<inter> f ` {a..b} \<noteq> {}
 3. KM \<inter> f ` {a..b} \<noteq> {}
[PROOF STEP]
show "connected (f`{a..b})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. connected (f ` {a..b})
[PROOF STEP]
apply (rule connected_continuous_image)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. continuous_on {a..b} f
 2. connected {a..b}
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
continuous_on {a..b} f

goal (2 subgoals):
 1. continuous_on {a..b} f
 2. connected {a..b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
connected (f ` {a..b})

goal (2 subgoals):
 1. Km \<inter> f ` {a..b} \<noteq> {}
 2. KM \<inter> f ` {a..b} \<noteq> {}
[PROOF STEP]
have "f a \<in> Km \<inter> f`{a..b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f a \<in> Km \<inter> f ` {a..b}
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
a \<le> b

goal (1 subgoal):
 1. f a \<in> Km \<inter> f ` {a..b}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> b \<Longrightarrow> f a \<in> Km
[PROOF STEP]
unfolding Km_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> b \<Longrightarrow> f a \<in> (\<Union>z\<in>p ` {0..t}. cball z D)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> b \<Longrightarrow> \<exists>x\<in>{0..t}. dist (p x) (f a) \<le> D
[PROOF STEP]
apply (rule bexI[of _ 0])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a \<le> b \<Longrightarrow> dist (p 0) (f a) \<le> D
 2. a \<le> b \<Longrightarrow> 0 \<in> {0..t}
[PROOF STEP]
unfolding p
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a \<le> b \<Longrightarrow> dist (f a) (f a) \<le> D
 2. a \<le> b \<Longrightarrow> 0 \<in> {0..t}
[PROOF STEP]
using \<open>D \<ge> 0\<close> t(2)
[PROOF STATE]
proof (prove)
using this:
0 \<le> D
t \<in> {0..dist (f a) (f b)}

goal (2 subgoals):
 1. a \<le> b \<Longrightarrow> dist (f a) (f a) \<le> D
 2. a \<le> b \<Longrightarrow> 0 \<in> {0..t}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f a \<in> Km \<inter> f ` {a..b}

goal (2 subgoals):
 1. Km \<inter> f ` {a..b} \<noteq> {}
 2. KM \<inter> f ` {a..b} \<noteq> {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f a \<in> Km \<inter> f ` {a..b}
[PROOF STEP]
show "Km \<inter> f`{a..b} \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
f a \<in> Km \<inter> f ` {a..b}

goal (1 subgoal):
 1. Km \<inter> f ` {a..b} \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Km \<inter> f ` {a..b} \<noteq> {}

goal (1 subgoal):
 1. KM \<inter> f ` {a..b} \<noteq> {}
[PROOF STEP]
have "f b \<in> KM \<inter> f`{a..b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f b \<in> KM \<inter> f ` {a..b}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. f b \<in> KM
 2. f b \<in> f ` {a..b}
[PROOF STEP]
unfolding KM_def
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. f b \<in> (\<Union>z\<in>p ` {t..dist (f a) (f b)}. cball z D)
 2. f b \<in> f ` {a..b}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<exists>x\<in>{t..dist (f a) (f b)}. dist (p x) (f b) \<le> D
 2. f b \<in> f ` {a..b}
[PROOF STEP]
apply (rule bexI[of _ "dist (f a) (f b)"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. dist (p (dist (f a) (f b))) (f b) \<le> D
 2. dist (f a) (f b) \<in> {t..dist (f a) (f b)}
 3. f b \<in> f ` {a..b}
[PROOF STEP]
unfolding p
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. dist (f b) (f b) \<le> D
 2. dist (f a) (f b) \<in> {t..dist (f a) (f b)}
 3. f b \<in> f ` {a..b}
[PROOF STEP]
using \<open>D \<ge> 0\<close> t(2) True
[PROOF STATE]
proof (prove)
using this:
0 \<le> D
t \<in> {0..dist (f a) (f b)}
a \<le> b

goal (3 subgoals):
 1. dist (f b) (f b) \<le> D
 2. dist (f a) (f b) \<in> {t..dist (f a) (f b)}
 3. f b \<in> f ` {a..b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f b \<in> KM \<inter> f ` {a..b}

goal (1 subgoal):
 1. KM \<inter> f ` {a..b} \<noteq> {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f b \<in> KM \<inter> f ` {a..b}
[PROOF STEP]
show "KM \<inter> f`{a..b} \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
f b \<in> KM \<inter> f ` {a..b}

goal (1 subgoal):
 1. KM \<inter> f ` {a..b} \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
KM \<inter> f ` {a..b} \<noteq> {}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Km \<inter> f ` {a..b} \<inter> (KM \<inter> f ` {a..b}) \<noteq> {}

goal (1 subgoal):
 1. infdist x (f ` {a..b}) \<le> D + 1 * deltaG TYPE('a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Km \<inter> f ` {a..b} \<inter> (KM \<inter> f ` {a..b}) \<noteq> {}
[PROOF STEP]
obtain y where y: "y \<in> f`{a..b}" "y \<in> Km" "y \<in> KM"
[PROOF STATE]
proof (prove)
using this:
Km \<inter> f ` {a..b} \<inter> (KM \<inter> f ` {a..b}) \<noteq> {}

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> f ` {a..b}; y \<in> Km; y \<in> KM\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> f ` {a..b}
y \<in> Km
y \<in> KM

goal (1 subgoal):
 1. infdist x (f ` {a..b}) \<le> D + 1 * deltaG TYPE('a)
[PROOF STEP]
obtain tm where tm: "tm \<in> {0..t}" "dist (p tm) y \<le> D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>tm. \<lbrakk>tm \<in> {0..t}; dist (p tm) y \<le> D\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using y(2)
[PROOF STATE]
proof (prove)
using this:
y \<in> Km

goal (1 subgoal):
 1. (\<And>tm. \<lbrakk>tm \<in> {0..t}; dist (p tm) y \<le> D\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding Km_def
[PROOF STATE]
proof (prove)
using this:
y \<in> (\<Union>z\<in>p ` {0..t}. cball z D)

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

goal (1 subgoal):
 1. infdist x (f ` {a..b}) \<le> D + 1 * deltaG TYPE('a)
[PROOF STEP]
obtain tM where tM: "tM \<in> {t..dist (f a) (f b)}" "dist (p tM) y \<le> D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>tM. \<lbrakk>tM \<in> {t..dist (f a) (f b)}; dist (p tM) y \<le> D\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using y(3)
[PROOF STATE]
proof (prove)
using this:
y \<in> KM

goal (1 subgoal):
 1. (\<And>tM. \<lbrakk>tM \<in> {t..dist (f a) (f b)}; dist (p tM) y \<le> D\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding KM_def
[PROOF STATE]
proof (prove)
using this:
y \<in> (\<Union>z\<in>p ` {t..dist (f a) (f b)}. cball z D)

goal (1 subgoal):
 1. (\<And>tM. \<lbrakk>tM \<in> {t..dist (f a) (f b)}; dist (p tM) y \<le> D\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
tM \<in> {t..dist (f a) (f b)}
dist (p tM) y \<le> D

goal (1 subgoal):
 1. infdist x (f ` {a..b}) \<le> D + 1 * deltaG TYPE('a)
[PROOF STEP]
define H where "H = p`{tm..tM}"
[PROOF STATE]
proof (state)
this:
H = p ` {tm..tM}

goal (1 subgoal):
 1. infdist x (f ` {a..b}) \<le> D + 1 * deltaG TYPE('a)
[PROOF STEP]
have *: "geodesic_segment_between H (p tm) (p tM)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_between H (p tm) (p tM)
[PROOF STEP]
unfolding H_def p_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geodesic_segment_between (geodesic_segment_param G (f a) ` {tm..tM}) (geodesic_segment_param G (f a) tm) (geodesic_segment_param G (f a) tM)
[PROOF STEP]
apply (rule geodesic_segmentI2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. isometry_on {tm..tM} (geodesic_segment_param G (f a))
 2. tm \<le> tM
[PROOF STEP]
using assms(3) \<open>tm \<in> {0..t}\<close> \<open>tM \<in> {t..dist (f a) (f b)}\<close> isometry_on_subset
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_between G (f a) (f b)
tm \<in> {0..t}
tM \<in> {t..dist (f a) (f b)}
\<lbrakk>isometry_on ?X ?f; ?Y \<subseteq> ?X\<rbrakk> \<Longrightarrow> isometry_on ?Y ?f

goal (2 subgoals):
 1. isometry_on {tm..tM} (geodesic_segment_param G (f a))
 2. tm \<le> tM
[PROOF STEP]
using assms(3) geodesic_segment_param(4)
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_between G (f a) (f b)
tm \<in> {0..t}
tM \<in> {t..dist (f a) (f b)}
\<lbrakk>isometry_on ?X ?f; ?Y \<subseteq> ?X\<rbrakk> \<Longrightarrow> isometry_on ?Y ?f
geodesic_segment_between G (f a) (f b)
geodesic_segment_between ?G ?x ?y \<Longrightarrow> isometry_on {0..dist ?x ?y} (geodesic_segment_param ?G ?x)

goal (2 subgoals):
 1. isometry_on {tm..tM} (geodesic_segment_param G (f a))
 2. tm \<le> tM
[PROOF STEP]
by (auto) fastforce
[PROOF STATE]
proof (state)
this:
geodesic_segment_between H (p tm) (p tM)

goal (1 subgoal):
 1. infdist x (f ` {a..b}) \<le> D + 1 * deltaG TYPE('a)
[PROOF STEP]
have "x \<in> H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> H
[PROOF STEP]
unfolding t(1) H_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p t \<in> p ` {tm..tM}
[PROOF STEP]
using \<open>tm \<in> {0..t}\<close> \<open>tM \<in> {t..dist (f a) (f b)}\<close>
[PROOF STATE]
proof (prove)
using this:
tm \<in> {0..t}
tM \<in> {t..dist (f a) (f b)}

goal (1 subgoal):
 1. p t \<in> p ` {tm..tM}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> H

goal (1 subgoal):
 1. infdist x (f ` {a..b}) \<le> D + 1 * deltaG TYPE('a)
[PROOF STEP]
have "infdist x (f ` {a..b}) \<le> dist x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infdist x (f ` {a..b}) \<le> dist x y
[PROOF STEP]
by (rule infdist_le[OF y(1)])
[PROOF STATE]
proof (state)
this:
infdist x (f ` {a..b}) \<le> dist x y

goal (1 subgoal):
 1. infdist x (f ` {a..b}) \<le> D + 1 * deltaG TYPE('a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
infdist x (f ` {a..b}) \<le> dist x y

goal (1 subgoal):
 1. infdist x (f ` {a..b}) \<le> D + 1 * deltaG TYPE('a)
[PROOF STEP]
have "... \<le> max (dist (p tm) y) (dist (p tM) y) + deltaG(TYPE('a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist x y \<le> max (dist (p tm) y) (dist (p tM) y) + deltaG TYPE('a)
[PROOF STEP]
by (rule dist_le_max_dist_triangle[OF * \<open>x \<in> H\<close>])
[PROOF STATE]
proof (state)
this:
dist x y \<le> max (dist (p tm) y) (dist (p tM) y) + deltaG TYPE('a)

goal (1 subgoal):
 1. infdist x (f ` {a..b}) \<le> D + 1 * deltaG TYPE('a)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
infdist x (f ` {a..b}) \<le> max (dist (p tm) y) (dist (p tM) y) + deltaG TYPE('a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
infdist x (f ` {a..b}) \<le> max (dist (p tm) y) (dist (p tM) y) + deltaG TYPE('a)

goal (1 subgoal):
 1. infdist x (f ` {a..b}) \<le> D + 1 * deltaG TYPE('a)
[PROOF STEP]
using tm(2) tM(2)
[PROOF STATE]
proof (prove)
using this:
infdist x (f ` {a..b}) \<le> max (dist (p tm) y) (dist (p tM) y) + deltaG TYPE('a)
dist (p tm) y \<le> D
dist (p tM) y \<le> D

goal (1 subgoal):
 1. infdist x (f ` {a..b}) \<le> D + 1 * deltaG TYPE('a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
infdist x (f ` {a..b}) \<le> D + 1 * deltaG TYPE('a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
infdist x (f ` {a..b}) \<le> D + 1 * deltaG TYPE('a)

goal (1 subgoal):
 1. \<And>x. x \<in> G \<Longrightarrow> infdist x (f ` {a..b}) \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
infdist x (f ` {a..b}) \<le> D + 1 * deltaG TYPE('a)

goal (1 subgoal):
 1. \<And>x. x \<in> G \<Longrightarrow> infdist x (f ` {a..b}) \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
[PROOF STEP]
have "... \<le> D + lambda^2 * deltaG TYPE('a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D + 1 * deltaG TYPE('a) \<le> D + lambda\<^sup>2 * deltaG TYPE('a)
[PROOF STEP]
apply (intro mono_intros)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> lambda\<^sup>2
[PROOF STEP]
using \<open>lambda \<ge> 1\<close>
[PROOF STATE]
proof (prove)
using this:
1 \<le> lambda

goal (1 subgoal):
 1. 1 \<le> lambda\<^sup>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
D + 1 * deltaG TYPE('a) \<le> D + lambda\<^sup>2 * deltaG TYPE('a)

goal (1 subgoal):
 1. \<And>x. x \<in> G \<Longrightarrow> infdist x (f ` {a..b}) \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
infdist x (f ` {a..b}) \<le> D + lambda\<^sup>2 * deltaG TYPE('a)
[PROOF STEP]
show "infdist x (f ` {a..b}) \<le> lambda\<^sup>2 * (11/2 * C + 92 * deltaG TYPE('a))"
[PROOF STATE]
proof (prove)
using this:
infdist x (f ` {a..b}) \<le> D + lambda\<^sup>2 * deltaG TYPE('a)

goal (1 subgoal):
 1. infdist x (f ` {a..b}) \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
[PROOF STEP]
unfolding D_def
[PROOF STATE]
proof (prove)
using this:
infdist x (f ` {a..b}) \<le> lambda\<^sup>2 * (11 / 2 * C + 91 * deltaG TYPE('a)) + lambda\<^sup>2 * deltaG TYPE('a)

goal (1 subgoal):
 1. infdist x (f ` {a..b}) \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
infdist x (f ` {a..b}) \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
hausdorff_distance (f ` {a..b}) G \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))

goal (1 subgoal):
 1. \<not> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> a \<le> b

goal (1 subgoal):
 1. \<not> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> a \<le> b
[PROOF STEP]
have "f`{a..b} = {}"
[PROOF STATE]
proof (prove)
using this:
\<not> a \<le> b

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

goal (1 subgoal):
 1. \<not> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f ` {a..b} = {}
[PROOF STEP]
have "hausdorff_distance (f ` {a..b}) G = 0"
[PROOF STATE]
proof (prove)
using this:
f ` {a..b} = {}

goal (1 subgoal):
 1. hausdorff_distance (f ` {a..b}) G = 0
[PROOF STEP]
unfolding hausdorff_distance_def
[PROOF STATE]
proof (prove)
using this:
f ` {a..b} = {}

goal (1 subgoal):
 1. (if f ` {a..b} = {} \<or> G = {} \<or> \<not> bounded (f ` {a..b}) \<or> \<not> bounded G then 0 else max (SUP x\<in>f ` {a..b}. infdist x G) (SUP x\<in>G. infdist x (f ` {a..b}))) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hausdorff_distance (f ` {a..b}) G = 0

goal (1 subgoal):
 1. \<not> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hausdorff_distance (f ` {a..b}) G = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
hausdorff_distance (f ` {a..b}) G = 0

goal (1 subgoal):
 1. hausdorff_distance (f ` {a..b}) G \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
[PROOF STEP]
using quasi_isometry_onD(4)[OF assms(2)]
[PROOF STATE]
proof (prove)
using this:
hausdorff_distance (f ` {a..b}) G = 0
0 \<le> C

goal (1 subgoal):
 1. hausdorff_distance (f ` {a..b}) G \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hausdorff_distance (f ` {a..b}) G \<le> lambda\<^sup>2 * (11 / 2 * C + 92 * deltaG TYPE('a))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem (in Gromov_hyperbolic_space_geodesic) Morse_Gromov_theorem:
  fixes f::"real \<Rightarrow> 'a"
  assumes "lambda C-quasi_isometry_on {a..b} f"
          "geodesic_segment_between G (f a) (f b)"
  shows "hausdorff_distance (f`{a..b}) G \<le> 92 * lambda^2 * (C + deltaG(TYPE('a)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
have C: "C \<ge> 0" "lambda \<ge> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> C &&& 1 \<le> lambda
[PROOF STEP]
using quasi_isometry_onD[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> {a..b}; ?y \<in> {a..b}\<rbrakk> \<Longrightarrow> dist (f ?x) (f ?y) \<le> lambda * dist ?x ?y + C
\<lbrakk>?x \<in> {a..b}; ?y \<in> {a..b}\<rbrakk> \<Longrightarrow> 1 / lambda * dist ?x ?y - C \<le> dist (f ?x) (f ?y)
1 \<le> lambda
0 \<le> C

goal (1 subgoal):
 1. 0 \<le> C &&& 1 \<le> lambda
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> C
1 \<le> lambda

goal (1 subgoal):
 1. hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
consider "dist (f a) (f b) \<ge> 2 * C \<and> a \<le> b" | "dist (f a) (f b) \<le> 2 * C \<and> a \<le> b" | "b < a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>2 * C \<le> dist (f a) (f b) \<and> a \<le> b \<Longrightarrow> thesis; dist (f a) (f b) \<le> 2 * C \<and> a \<le> b \<Longrightarrow> thesis; b < a \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
\<lbrakk>2 * C \<le> dist (f a) (f b) \<and> a \<le> b \<Longrightarrow> ?thesis; dist (f a) (f b) \<le> 2 * C \<and> a \<le> b \<Longrightarrow> ?thesis; b < a \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>2 * C \<le> dist (f a) (f b) \<and> a \<le> b \<Longrightarrow> ?thesis; dist (f a) (f b) \<le> 2 * C \<and> a \<le> b \<Longrightarrow> ?thesis; b < a \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>2 * C \<le> dist (f a) (f b) \<and> a \<le> b \<Longrightarrow> ?thesis; dist (f a) (f b) \<le> 2 * C \<and> a \<le> b \<Longrightarrow> ?thesis; b < a \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. 2 * C \<le> dist (f a) (f b) \<and> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 2. dist (f a) (f b) \<le> 2 * C \<and> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 3. b < a \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
2 * C \<le> dist (f a) (f b) \<and> a \<le> b

goal (3 subgoals):
 1. 2 * C \<le> dist (f a) (f b) \<and> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 2. dist (f a) (f b) \<le> 2 * C \<and> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 3. b < a \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
have "\<exists>d. continuous_on {a..b} d \<and> d a = f a \<and> d b = f b
                \<and> (\<forall>x\<in>{a..b}. dist (f x) (d x) \<le> 4 * C)
                \<and> lambda (4 * C)-quasi_isometry_on {a..b} d
                \<and> (2 * lambda)-lipschitz_on {a..b} d
                \<and> hausdorff_distance (f`{a..b}) (d`{a..b}) \<le> 2 * C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>d. continuous_on {a..b} d \<and> d a = f a \<and> d b = f b \<and> (\<forall>x\<in>{a..b}. dist (f x) (d x) \<le> 4 * C) \<and> lambda (4 * C) -quasi_isometry_on {a..b} d \<and> (2 * lambda)-lipschitz_on {a..b} d \<and> hausdorff_distance (f ` {a..b}) (d ` {a..b}) \<le> 2 * C
[PROOF STEP]
apply (rule quasi_geodesic_made_lipschitz[OF assms(1)])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * C \<le> dist (f a) (f b)
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
2 * C \<le> dist (f a) (f b) \<and> a \<le> b

goal (1 subgoal):
 1. 2 * C \<le> dist (f a) (f b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>d. continuous_on {a..b} d \<and> d a = f a \<and> d b = f b \<and> (\<forall>x\<in>{a..b}. dist (f x) (d x) \<le> 4 * C) \<and> lambda (4 * C) -quasi_isometry_on {a..b} d \<and> (2 * lambda)-lipschitz_on {a..b} d \<and> hausdorff_distance (f ` {a..b}) (d ` {a..b}) \<le> 2 * C

goal (3 subgoals):
 1. 2 * C \<le> dist (f a) (f b) \<and> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 2. dist (f a) (f b) \<le> 2 * C \<and> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 3. b < a \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>d. continuous_on {a..b} d \<and> d a = f a \<and> d b = f b \<and> (\<forall>x\<in>{a..b}. dist (f x) (d x) \<le> 4 * C) \<and> lambda (4 * C) -quasi_isometry_on {a..b} d \<and> (2 * lambda)-lipschitz_on {a..b} d \<and> hausdorff_distance (f ` {a..b}) (d ` {a..b}) \<le> 2 * C
[PROOF STEP]
obtain d where d: "d a = f a" "d b = f b"
                        "\<And>x. x \<in> {a..b} \<Longrightarrow> dist (f x) (d x) \<le> 4 * C"
                        "lambda (4 * C)-quasi_isometry_on {a..b} d"
                        "(2 * lambda)-lipschitz_on {a..b} d"
                        "hausdorff_distance (f`{a..b}) (d`{a..b}) \<le> 2 * C"
[PROOF STATE]
proof (prove)
using this:
\<exists>d. continuous_on {a..b} d \<and> d a = f a \<and> d b = f b \<and> (\<forall>x\<in>{a..b}. dist (f x) (d x) \<le> 4 * C) \<and> lambda (4 * C) -quasi_isometry_on {a..b} d \<and> (2 * lambda)-lipschitz_on {a..b} d \<and> hausdorff_distance (f ` {a..b}) (d ` {a..b}) \<le> 2 * C

goal (1 subgoal):
 1. (\<And>d. \<lbrakk>d a = f a; d b = f b; \<And>x. x \<in> {a..b} \<Longrightarrow> dist (f x) (d x) \<le> 4 * C; lambda (4 * C) -quasi_isometry_on {a..b} d; (2 * lambda)-lipschitz_on {a..b} d; hausdorff_distance (f ` {a..b}) (d ` {a..b}) \<le> 2 * C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
d a = f a
d b = f b
?x \<in> {a..b} \<Longrightarrow> dist (f ?x) (d ?x) \<le> 4 * C
lambda (4 * C) -quasi_isometry_on {a..b} d
(2 * lambda)-lipschitz_on {a..b} d
hausdorff_distance (f ` {a..b}) (d ` {a..b}) \<le> 2 * C

goal (3 subgoals):
 1. 2 * C \<le> dist (f a) (f b) \<and> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 2. dist (f a) (f b) \<le> 2 * C \<and> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 3. b < a \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
have a: "hausdorff_distance (d`{a..b}) G \<le> lambda^2 * ((11/2) * (4 * C) + 92 * deltaG(TYPE('a)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hausdorff_distance (d ` {a..b}) G \<le> lambda\<^sup>2 * (11 / 2 * (4 * C) + 92 * deltaG TYPE('a))
[PROOF STEP]
apply (rule Morse_Gromov_theorem_aux2)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. continuous_on {a..b} d
 2. lambda (4 * C) -quasi_isometry_on {a..b} d
 3. geodesic_segment_between G (d a) (d b)
[PROOF STEP]
using d assms lipschitz_on_continuous_on
[PROOF STATE]
proof (prove)
using this:
d a = f a
d b = f b
?x \<in> {a..b} \<Longrightarrow> dist (f ?x) (d ?x) \<le> 4 * C
lambda (4 * C) -quasi_isometry_on {a..b} d
(2 * lambda)-lipschitz_on {a..b} d
hausdorff_distance (f ` {a..b}) (d ` {a..b}) \<le> 2 * C
lambda C -quasi_isometry_on {a..b} f
geodesic_segment_between G (f a) (f b)
?L-lipschitz_on ?X ?f \<Longrightarrow> continuous_on ?X ?f

goal (3 subgoals):
 1. continuous_on {a..b} d
 2. lambda (4 * C) -quasi_isometry_on {a..b} d
 3. geodesic_segment_between G (d a) (d b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hausdorff_distance (d ` {a..b}) G \<le> lambda\<^sup>2 * (11 / 2 * (4 * C) + 92 * deltaG TYPE('a))

goal (3 subgoals):
 1. 2 * C \<le> dist (f a) (f b) \<and> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 2. dist (f a) (f b) \<le> 2 * C \<and> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 3. b < a \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
have "hausdorff_distance (f`{a..b}) G \<le>
          hausdorff_distance (f`{a..b}) (d`{a..b}) + hausdorff_distance (d`{a..b}) G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hausdorff_distance (f ` {a..b}) G \<le> hausdorff_distance (f ` {a..b}) (d ` {a..b}) + hausdorff_distance (d ` {a..b}) G
[PROOF STEP]
apply (rule hausdorff_distance_triangle)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. d ` {a..b} \<noteq> {}
 2. bounded (d ` {a..b})
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
2 * C \<le> dist (f a) (f b) \<and> a \<le> b

goal (2 subgoals):
 1. d ` {a..b} \<noteq> {}
 2. bounded (d ` {a..b})
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded (d ` {a..b})
[PROOF STEP]
by (rule quasi_isometry_on_bounded[OF d(4)], auto)
[PROOF STATE]
proof (state)
this:
hausdorff_distance (f ` {a..b}) G \<le> hausdorff_distance (f ` {a..b}) (d ` {a..b}) + hausdorff_distance (d ` {a..b}) G

goal (3 subgoals):
 1. 2 * C \<le> dist (f a) (f b) \<and> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 2. dist (f a) (f b) \<le> 2 * C \<and> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 3. b < a \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
hausdorff_distance (f ` {a..b}) G \<le> hausdorff_distance (f ` {a..b}) (d ` {a..b}) + hausdorff_distance (d ` {a..b}) G

goal (3 subgoals):
 1. 2 * C \<le> dist (f a) (f b) \<and> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 2. dist (f a) (f b) \<le> 2 * C \<and> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 3. b < a \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
have "... \<le> lambda^2 * ((11/2) * (4 * C) + 92 * deltaG(TYPE('a))) + 1 * 2 * C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hausdorff_distance (f ` {a..b}) (d ` {a..b}) + hausdorff_distance (d ` {a..b}) G \<le> lambda\<^sup>2 * (11 / 2 * (4 * C) + 92 * deltaG TYPE('a)) + 1 * 2 * C
[PROOF STEP]
using a d
[PROOF STATE]
proof (prove)
using this:
hausdorff_distance (d ` {a..b}) G \<le> lambda\<^sup>2 * (11 / 2 * (4 * C) + 92 * deltaG TYPE('a))
d a = f a
d b = f b
?x \<in> {a..b} \<Longrightarrow> dist (f ?x) (d ?x) \<le> 4 * C
lambda (4 * C) -quasi_isometry_on {a..b} d
(2 * lambda)-lipschitz_on {a..b} d
hausdorff_distance (f ` {a..b}) (d ` {a..b}) \<le> 2 * C

goal (1 subgoal):
 1. hausdorff_distance (f ` {a..b}) (d ` {a..b}) + hausdorff_distance (d ` {a..b}) G \<le> lambda\<^sup>2 * (11 / 2 * (4 * C) + 92 * deltaG TYPE('a)) + 1 * 2 * C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hausdorff_distance (f ` {a..b}) (d ` {a..b}) + hausdorff_distance (d ` {a..b}) G \<le> lambda\<^sup>2 * (11 / 2 * (4 * C) + 92 * deltaG TYPE('a)) + 1 * 2 * C

goal (3 subgoals):
 1. 2 * C \<le> dist (f a) (f b) \<and> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 2. dist (f a) (f b) \<le> 2 * C \<and> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 3. b < a \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
hausdorff_distance (f ` {a..b}) (d ` {a..b}) + hausdorff_distance (d ` {a..b}) G \<le> lambda\<^sup>2 * (11 / 2 * (4 * C) + 92 * deltaG TYPE('a)) + 1 * 2 * C

goal (3 subgoals):
 1. 2 * C \<le> dist (f a) (f b) \<and> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 2. dist (f a) (f b) \<le> 2 * C \<and> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 3. b < a \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
have "... \<le> lambda^2 * ((11/2) * (4 * C) + 92 * deltaG(TYPE('a))) + lambda^2 * 2 * C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lambda\<^sup>2 * (11 / 2 * (4 * C) + 92 * deltaG TYPE('a)) + 1 * 2 * C \<le> lambda\<^sup>2 * (11 / 2 * (4 * C) + 92 * deltaG TYPE('a)) + lambda\<^sup>2 * 2 * C
[PROOF STEP]
apply (intro mono_intros)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. 1 \<le> lambda\<^sup>2
 2. 0 \<le> 2
 3. 0 \<le> C
[PROOF STEP]
using \<open>lambda \<ge> 1\<close> \<open>C \<ge> 0\<close>
[PROOF STATE]
proof (prove)
using this:
1 \<le> lambda
0 \<le> C

goal (3 subgoals):
 1. 1 \<le> lambda\<^sup>2
 2. 0 \<le> 2
 3. 0 \<le> C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lambda\<^sup>2 * (11 / 2 * (4 * C) + 92 * deltaG TYPE('a)) + 1 * 2 * C \<le> lambda\<^sup>2 * (11 / 2 * (4 * C) + 92 * deltaG TYPE('a)) + lambda\<^sup>2 * 2 * C

goal (3 subgoals):
 1. 2 * C \<le> dist (f a) (f b) \<and> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 2. dist (f a) (f b) \<le> 2 * C \<and> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 3. b < a \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lambda\<^sup>2 * (11 / 2 * (4 * C) + 92 * deltaG TYPE('a)) + 1 * 2 * C \<le> lambda\<^sup>2 * (11 / 2 * (4 * C) + 92 * deltaG TYPE('a)) + lambda\<^sup>2 * 2 * C

goal (3 subgoals):
 1. 2 * C \<le> dist (f a) (f b) \<and> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 2. dist (f a) (f b) \<le> 2 * C \<and> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 3. b < a \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
have "... = lambda^2 * (24 * C + 92 * deltaG(TYPE('a)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lambda\<^sup>2 * (11 / 2 * (4 * C) + 92 * deltaG TYPE('a)) + lambda\<^sup>2 * 2 * C = lambda\<^sup>2 * (24 * C + 92 * deltaG TYPE('a))
[PROOF STEP]
by (simp add: algebra_simps divide_simps)
[PROOF STATE]
proof (state)
this:
lambda\<^sup>2 * (11 / 2 * (4 * C) + 92 * deltaG TYPE('a)) + lambda\<^sup>2 * 2 * C = lambda\<^sup>2 * (24 * C + 92 * deltaG TYPE('a))

goal (3 subgoals):
 1. 2 * C \<le> dist (f a) (f b) \<and> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 2. dist (f a) (f b) \<le> 2 * C \<and> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 3. b < a \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lambda\<^sup>2 * (11 / 2 * (4 * C) + 92 * deltaG TYPE('a)) + lambda\<^sup>2 * 2 * C = lambda\<^sup>2 * (24 * C + 92 * deltaG TYPE('a))

goal (3 subgoals):
 1. 2 * C \<le> dist (f a) (f b) \<and> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 2. dist (f a) (f b) \<le> 2 * C \<and> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 3. b < a \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
have "... \<le> lambda^2 * (92 * C + 92 * deltaG(TYPE('a)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lambda\<^sup>2 * (24 * C + 92 * deltaG TYPE('a)) \<le> lambda\<^sup>2 * (92 * C + 92 * deltaG TYPE('a))
[PROOF STEP]
apply (intro mono_intros)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. 24 \<le> 92
 2. 0 \<le> C
 3. 0 \<le> lambda\<^sup>2
[PROOF STEP]
using \<open>lambda \<ge> 1\<close> \<open>C \<ge> 0\<close>
[PROOF STATE]
proof (prove)
using this:
1 \<le> lambda
0 \<le> C

goal (3 subgoals):
 1. 24 \<le> 92
 2. 0 \<le> C
 3. 0 \<le> lambda\<^sup>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lambda\<^sup>2 * (24 * C + 92 * deltaG TYPE('a)) \<le> lambda\<^sup>2 * (92 * C + 92 * deltaG TYPE('a))

goal (3 subgoals):
 1. 2 * C \<le> dist (f a) (f b) \<and> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 2. dist (f a) (f b) \<le> 2 * C \<and> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 3. b < a \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
hausdorff_distance (f ` {a..b}) G \<le> lambda\<^sup>2 * (92 * C + 92 * deltaG TYPE('a))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
hausdorff_distance (f ` {a..b}) G \<le> lambda\<^sup>2 * (92 * C + 92 * deltaG TYPE('a))

goal (1 subgoal):
 1. hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
by (auto simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))

goal (2 subgoals):
 1. dist (f a) (f b) \<le> 2 * C \<and> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 2. b < a \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. dist (f a) (f b) \<le> 2 * C \<and> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 2. b < a \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
dist (f a) (f b) \<le> 2 * C \<and> a \<le> b

goal (2 subgoals):
 1. dist (f a) (f b) \<le> 2 * C \<and> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 2. b < a \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
have "(1/lambda) * dist a b - C \<le> dist (f a) (f b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / lambda * dist a b - C \<le> dist (f a) (f b)
[PROOF STEP]
apply (rule quasi_isometry_onD[OF assms(1)])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a \<in> {a..b}
 2. b \<in> {a..b}
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
dist (f a) (f b) \<le> 2 * C \<and> a \<le> b

goal (2 subgoals):
 1. a \<in> {a..b}
 2. b \<in> {a..b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 / lambda * dist a b - C \<le> dist (f a) (f b)

goal (2 subgoals):
 1. dist (f a) (f b) \<le> 2 * C \<and> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 2. b < a \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 / lambda * dist a b - C \<le> dist (f a) (f b)

goal (2 subgoals):
 1. dist (f a) (f b) \<le> 2 * C \<and> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 2. b < a \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
have "... \<le> 2 * C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (f a) (f b) \<le> 2 * C
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
dist (f a) (f b) \<le> 2 * C \<and> a \<le> b

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

goal (2 subgoals):
 1. dist (f a) (f b) \<le> 2 * C \<and> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 2. b < a \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
1 / lambda * dist a b - C \<le> 2 * C
[PROOF STEP]
have "dist a b \<le> 3 * lambda * C"
[PROOF STATE]
proof (prove)
using this:
1 / lambda * dist a b - C \<le> 2 * C

goal (1 subgoal):
 1. dist a b \<le> 3 * lambda * C
[PROOF STEP]
using C
[PROOF STATE]
proof (prove)
using this:
1 / lambda * dist a b - C \<le> 2 * C
0 \<le> C
1 \<le> lambda

goal (1 subgoal):
 1. dist a b \<le> 3 * lambda * C
[PROOF STEP]
by (auto simp add: algebra_simps divide_simps)
[PROOF STATE]
proof (state)
this:
dist a b \<le> 3 * lambda * C

goal (2 subgoals):
 1. dist (f a) (f b) \<le> 2 * C \<and> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 2. b < a \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dist a b \<le> 3 * lambda * C
[PROOF STEP]
have *: "b - a \<le> 3 * lambda * C"
[PROOF STATE]
proof (prove)
using this:
dist a b \<le> 3 * lambda * C

goal (1 subgoal):
 1. b - a \<le> 3 * lambda * C
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
dist a b \<le> 3 * lambda * C
dist (f a) (f b) \<le> 2 * C \<and> a \<le> b

goal (1 subgoal):
 1. b - a \<le> 3 * lambda * C
[PROOF STEP]
unfolding dist_real_def
[PROOF STATE]
proof (prove)
using this:
\<bar>a - b\<bar> \<le> 3 * lambda * C
dist (f a) (f b) \<le> 2 * C \<and> a \<le> b

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

goal (2 subgoals):
 1. dist (f a) (f b) \<le> 2 * C \<and> a \<le> b \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 2. b < a \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
proof (rule hausdorff_distanceI2)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. x \<in> f ` {a..b} \<Longrightarrow> \<exists>y\<in>G. dist x y \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 2. \<And>x. x \<in> G \<Longrightarrow> \<exists>y\<in>f ` {a..b}. dist x y \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 3. 0 \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
show "0 \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
using C
[PROOF STATE]
proof (prove)
using this:
0 \<le> C
1 \<le> lambda

goal (1 subgoal):
 1. 0 \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))

goal (2 subgoals):
 1. \<And>x. x \<in> f ` {a..b} \<Longrightarrow> \<exists>y\<in>G. dist x y \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 2. \<And>x. x \<in> G \<Longrightarrow> \<exists>y\<in>f ` {a..b}. dist x y \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> f ` {a..b} \<Longrightarrow> \<exists>y\<in>G. dist x y \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 2. \<And>x. x \<in> G \<Longrightarrow> \<exists>y\<in>f ` {a..b}. dist x y \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
assume "x \<in> f`{a..b}"
[PROOF STATE]
proof (state)
this:
x \<in> f ` {a..b}

goal (2 subgoals):
 1. \<And>x. x \<in> f ` {a..b} \<Longrightarrow> \<exists>y\<in>G. dist x y \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 2. \<And>x. x \<in> G \<Longrightarrow> \<exists>y\<in>f ` {a..b}. dist x y \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> f ` {a..b}
[PROOF STEP]
obtain t where t: "x = f t" "t \<in> {a..b}"
[PROOF STATE]
proof (prove)
using this:
x \<in> f ` {a..b}

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

goal (2 subgoals):
 1. \<And>x. x \<in> f ` {a..b} \<Longrightarrow> \<exists>y\<in>G. dist x y \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 2. \<And>x. x \<in> G \<Longrightarrow> \<exists>y\<in>f ` {a..b}. dist x y \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
have "dist x (f a) \<le> lambda * dist t a + C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist x (f a) \<le> lambda * dist t a + C
[PROOF STEP]
unfolding t(1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (f t) (f a) \<le> lambda * dist t a + C
[PROOF STEP]
using quasi_isometry_onD(1)[OF assms(1) t(2)] 2
[PROOF STATE]
proof (prove)
using this:
?y \<in> {a..b} \<Longrightarrow> dist (f t) (f ?y) \<le> lambda * dist t ?y + C
dist (f a) (f b) \<le> 2 * C \<and> a \<le> b

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

goal (2 subgoals):
 1. \<And>x. x \<in> f ` {a..b} \<Longrightarrow> \<exists>y\<in>G. dist x y \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 2. \<And>x. x \<in> G \<Longrightarrow> \<exists>y\<in>f ` {a..b}. dist x y \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist x (f a) \<le> lambda * dist t a + C

goal (2 subgoals):
 1. \<And>x. x \<in> f ` {a..b} \<Longrightarrow> \<exists>y\<in>G. dist x y \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 2. \<And>x. x \<in> G \<Longrightarrow> \<exists>y\<in>f ` {a..b}. dist x y \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
have "... \<le> lambda * (b - a) + 1 * 1 * C + 0 * 0 * deltaG(TYPE('a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lambda * dist t a + C \<le> lambda * (b - a) + 1 * 1 * C + 0 * 0 * deltaG TYPE('a)
[PROOF STEP]
using t(2) 2 C
[PROOF STATE]
proof (prove)
using this:
t \<in> {a..b}
dist (f a) (f b) \<le> 2 * C \<and> a \<le> b
0 \<le> C
1 \<le> lambda

goal (1 subgoal):
 1. lambda * dist t a + C \<le> lambda * (b - a) + 1 * 1 * C + 0 * 0 * deltaG TYPE('a)
[PROOF STEP]
unfolding dist_real_def
[PROOF STATE]
proof (prove)
using this:
t \<in> {a..b}
dist (f a) (f b) \<le> 2 * C \<and> a \<le> b
0 \<le> C
1 \<le> lambda

goal (1 subgoal):
 1. lambda * \<bar>t - a\<bar> + C \<le> lambda * (b - a) + 1 * 1 * C + 0 * 0 * deltaG TYPE('a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lambda * dist t a + C \<le> lambda * (b - a) + 1 * 1 * C + 0 * 0 * deltaG TYPE('a)

goal (2 subgoals):
 1. \<And>x. x \<in> f ` {a..b} \<Longrightarrow> \<exists>y\<in>G. dist x y \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 2. \<And>x. x \<in> G \<Longrightarrow> \<exists>y\<in>f ` {a..b}. dist x y \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lambda * dist t a + C \<le> lambda * (b - a) + 1 * 1 * C + 0 * 0 * deltaG TYPE('a)

goal (2 subgoals):
 1. \<And>x. x \<in> f ` {a..b} \<Longrightarrow> \<exists>y\<in>G. dist x y \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 2. \<And>x. x \<in> G \<Longrightarrow> \<exists>y\<in>f ` {a..b}. dist x y \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
have "... \<le> lambda * (3 * lambda * C) + lambda^2 * (92-3) * C + lambda^2 * 92 * deltaG(TYPE('a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lambda * (b - a) + 1 * 1 * C + 0 * 0 * deltaG TYPE('a) \<le> lambda * (3 * lambda * C) + lambda\<^sup>2 * (92 - 3) * C + lambda\<^sup>2 * 92 * deltaG TYPE('a)
[PROOF STEP]
apply (intro mono_intros *)
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. 0 \<le> lambda
 2. 1 \<le> lambda\<^sup>2
 3. 1 \<le> 92 - 3
 4. 0 \<le> lambda\<^sup>2
 5. 0 \<le> 1
 6. 0 \<le> C
 7. 0 \<le> lambda\<^sup>2
 8. 0 \<le> 92
 9. 0 \<le> lambda\<^sup>2
 10. 0 \<le> 0
[PROOF STEP]
using C
[PROOF STATE]
proof (prove)
using this:
0 \<le> C
1 \<le> lambda

goal (10 subgoals):
 1. 0 \<le> lambda
 2. 1 \<le> lambda\<^sup>2
 3. 1 \<le> 92 - 3
 4. 0 \<le> lambda\<^sup>2
 5. 0 \<le> 1
 6. 0 \<le> C
 7. 0 \<le> lambda\<^sup>2
 8. 0 \<le> 92
 9. 0 \<le> lambda\<^sup>2
 10. 0 \<le> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lambda * (b - a) + 1 * 1 * C + 0 * 0 * deltaG TYPE('a) \<le> lambda * (3 * lambda * C) + lambda\<^sup>2 * (92 - 3) * C + lambda\<^sup>2 * 92 * deltaG TYPE('a)

goal (2 subgoals):
 1. \<And>x. x \<in> f ` {a..b} \<Longrightarrow> \<exists>y\<in>G. dist x y \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 2. \<And>x. x \<in> G \<Longrightarrow> \<exists>y\<in>f ` {a..b}. dist x y \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist x (f a) \<le> lambda * (3 * lambda * C) + lambda\<^sup>2 * (92 - 3) * C + lambda\<^sup>2 * 92 * deltaG TYPE('a)
[PROOF STEP]
have *: "dist x (f a) \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))"
[PROOF STATE]
proof (prove)
using this:
dist x (f a) \<le> lambda * (3 * lambda * C) + lambda\<^sup>2 * (92 - 3) * C + lambda\<^sup>2 * 92 * deltaG TYPE('a)

goal (1 subgoal):
 1. dist x (f a) \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
by (simp add: algebra_simps power2_eq_square)
[PROOF STATE]
proof (state)
this:
dist x (f a) \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))

goal (2 subgoals):
 1. \<And>x. x \<in> f ` {a..b} \<Longrightarrow> \<exists>y\<in>G. dist x y \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 2. \<And>x. x \<in> G \<Longrightarrow> \<exists>y\<in>f ` {a..b}. dist x y \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
show "\<exists>y\<in>G. dist x y \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y\<in>G. dist x y \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
apply (rule bexI[of _ "f a"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. dist x (f a) \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 2. f a \<in> G
[PROOF STEP]
using * 2 assms(2)
[PROOF STATE]
proof (prove)
using this:
dist x (f a) \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
dist (f a) (f b) \<le> 2 * C \<and> a \<le> b
geodesic_segment_between G (f a) (f b)

goal (2 subgoals):
 1. dist x (f a) \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 2. f a \<in> G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>y\<in>G. dist x y \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))

goal (1 subgoal):
 1. \<And>x. x \<in> G \<Longrightarrow> \<exists>y\<in>f ` {a..b}. dist x y \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> G \<Longrightarrow> \<exists>y\<in>f ` {a..b}. dist x y \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> G \<Longrightarrow> \<exists>y\<in>f ` {a..b}. dist x y \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
assume "x \<in> G"
[PROOF STATE]
proof (state)
this:
x \<in> G

goal (1 subgoal):
 1. \<And>x. x \<in> G \<Longrightarrow> \<exists>y\<in>f ` {a..b}. dist x y \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> G
[PROOF STEP]
have "dist x (f a) \<le> dist (f a) (f b)"
[PROOF STATE]
proof (prove)
using this:
x \<in> G

goal (1 subgoal):
 1. dist x (f a) \<le> dist (f a) (f b)
[PROOF STEP]
by (meson assms geodesic_segment_dist_le geodesic_segment_endpoints(1) local.some_geodesic_is_geodesic_segment(1))
[PROOF STATE]
proof (state)
this:
dist x (f a) \<le> dist (f a) (f b)

goal (1 subgoal):
 1. \<And>x. x \<in> G \<Longrightarrow> \<exists>y\<in>f ` {a..b}. dist x y \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist x (f a) \<le> dist (f a) (f b)

goal (1 subgoal):
 1. \<And>x. x \<in> G \<Longrightarrow> \<exists>y\<in>f ` {a..b}. dist x y \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
have "... \<le> 1 * 2 * C + lambda^2 * 0 * deltaG(TYPE('a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (f a) (f b) \<le> 1 * 2 * C + lambda\<^sup>2 * 0 * deltaG TYPE('a)
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
dist (f a) (f b) \<le> 2 * C \<and> a \<le> b

goal (1 subgoal):
 1. dist (f a) (f b) \<le> 1 * 2 * C + lambda\<^sup>2 * 0 * deltaG TYPE('a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (f a) (f b) \<le> 1 * 2 * C + lambda\<^sup>2 * 0 * deltaG TYPE('a)

goal (1 subgoal):
 1. \<And>x. x \<in> G \<Longrightarrow> \<exists>y\<in>f ` {a..b}. dist x y \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (f a) (f b) \<le> 1 * 2 * C + lambda\<^sup>2 * 0 * deltaG TYPE('a)

goal (1 subgoal):
 1. \<And>x. x \<in> G \<Longrightarrow> \<exists>y\<in>f ` {a..b}. dist x y \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
have "... \<le> lambda^2 * 92 * C + lambda^2 * 92 * deltaG(TYPE('a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 * 2 * C + lambda\<^sup>2 * 0 * deltaG TYPE('a) \<le> lambda\<^sup>2 * 92 * C + lambda\<^sup>2 * 92 * deltaG TYPE('a)
[PROOF STEP]
apply (intro mono_intros)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. 1 \<le> lambda\<^sup>2
 2. 2 \<le> 92
 3. 0 \<le> lambda\<^sup>2
 4. 0 \<le> 2
 5. 0 \<le> C
 6. 0 \<le> 92
 7. 0 \<le> lambda\<^sup>2
[PROOF STEP]
using C
[PROOF STATE]
proof (prove)
using this:
0 \<le> C
1 \<le> lambda

goal (7 subgoals):
 1. 1 \<le> lambda\<^sup>2
 2. 2 \<le> 92
 3. 0 \<le> lambda\<^sup>2
 4. 0 \<le> 2
 5. 0 \<le> C
 6. 0 \<le> 92
 7. 0 \<le> lambda\<^sup>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 * 2 * C + lambda\<^sup>2 * 0 * deltaG TYPE('a) \<le> lambda\<^sup>2 * 92 * C + lambda\<^sup>2 * 92 * deltaG TYPE('a)

goal (1 subgoal):
 1. \<And>x. x \<in> G \<Longrightarrow> \<exists>y\<in>f ` {a..b}. dist x y \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist x (f a) \<le> lambda\<^sup>2 * 92 * C + lambda\<^sup>2 * 92 * deltaG TYPE('a)
[PROOF STEP]
have *: "dist x (f a) \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))"
[PROOF STATE]
proof (prove)
using this:
dist x (f a) \<le> lambda\<^sup>2 * 92 * C + lambda\<^sup>2 * 92 * deltaG TYPE('a)

goal (1 subgoal):
 1. dist x (f a) \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
dist x (f a) \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))

goal (1 subgoal):
 1. \<And>x. x \<in> G \<Longrightarrow> \<exists>y\<in>f ` {a..b}. dist x y \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
show "\<exists>y\<in>f`{a..b}. dist x y \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y\<in>f ` {a..b}. dist x y \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
apply (rule bexI[of _ "f a"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. dist x (f a) \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 2. f a \<in> f ` {a..b}
[PROOF STEP]
using * 2
[PROOF STATE]
proof (prove)
using this:
dist x (f a) \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
dist (f a) (f b) \<le> 2 * C \<and> a \<le> b

goal (2 subgoals):
 1. dist x (f a) \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 2. f a \<in> f ` {a..b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>y\<in>f ` {a..b}. dist x y \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))

goal (1 subgoal):
 1. b < a \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b < a \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:
b < a

goal (1 subgoal):
 1. b < a \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b < a
[PROOF STEP]
have "hausdorff_distance (f ` {a..b}) G = 0"
[PROOF STATE]
proof (prove)
using this:
b < a

goal (1 subgoal):
 1. hausdorff_distance (f ` {a..b}) G = 0
[PROOF STEP]
unfolding hausdorff_distance_def
[PROOF STATE]
proof (prove)
using this:
b < a

goal (1 subgoal):
 1. (if f ` {a..b} = {} \<or> G = {} \<or> \<not> bounded (f ` {a..b}) \<or> \<not> bounded G then 0 else max (SUP x\<in>f ` {a..b}. infdist x G) (SUP x\<in>G. infdist x (f ` {a..b}))) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hausdorff_distance (f ` {a..b}) G = 0

goal (1 subgoal):
 1. b < a \<Longrightarrow> hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hausdorff_distance (f ` {a..b}) G = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
hausdorff_distance (f ` {a..b}) G = 0

goal (1 subgoal):
 1. hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
using C
[PROOF STATE]
proof (prove)
using this:
hausdorff_distance (f ` {a..b}) G = 0
0 \<le> C
1 \<le> lambda

goal (1 subgoal):
 1. hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
hausdorff_distance (f ` {a..b}) G \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem (in Gromov_hyperbolic_space_geodesic) Morse_Gromov_theorem2:
  fixes c d::"real \<Rightarrow> 'a"
  assumes "lambda C-quasi_isometry_on {A..B} c"
          "lambda C-quasi_isometry_on {A..B} d"
          "c A = d A" "c B = d B"
  shows "hausdorff_distance (c`{A..B}) (d`{A..B}) \<le> 184 * lambda^2 * (C + deltaG(TYPE('a)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hausdorff_distance (c ` {A..B}) (d ` {A..B}) \<le> 184 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
proof (cases "A \<le> B")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A \<le> B \<Longrightarrow> hausdorff_distance (c ` {A..B}) (d ` {A..B}) \<le> 184 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 2. \<not> A \<le> B \<Longrightarrow> hausdorff_distance (c ` {A..B}) (d ` {A..B}) \<le> 184 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> A \<le> B

goal (2 subgoals):
 1. A \<le> B \<Longrightarrow> hausdorff_distance (c ` {A..B}) (d ` {A..B}) \<le> 184 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 2. \<not> A \<le> B \<Longrightarrow> hausdorff_distance (c ` {A..B}) (d ` {A..B}) \<le> 184 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> A \<le> B
[PROOF STEP]
have "hausdorff_distance (c`{A..B}) (d`{A..B}) = 0"
[PROOF STATE]
proof (prove)
using this:
\<not> A \<le> B

goal (1 subgoal):
 1. hausdorff_distance (c ` {A..B}) (d ` {A..B}) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hausdorff_distance (c ` {A..B}) (d ` {A..B}) = 0

goal (2 subgoals):
 1. A \<le> B \<Longrightarrow> hausdorff_distance (c ` {A..B}) (d ` {A..B}) \<le> 184 * lambda\<^sup>2 * (C + deltaG TYPE('a))
 2. \<not> A \<le> B \<Longrightarrow> hausdorff_distance (c ` {A..B}) (d ` {A..B}) \<le> 184 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hausdorff_distance (c ` {A..B}) (d ` {A..B}) = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
hausdorff_distance (c ` {A..B}) (d ` {A..B}) = 0

goal (1 subgoal):
 1. hausdorff_distance (c ` {A..B}) (d ` {A..B}) \<le> 184 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
using quasi_isometry_onD[OF assms(1)] delta_nonneg
[PROOF STATE]
proof (prove)
using this:
hausdorff_distance (c ` {A..B}) (d ` {A..B}) = 0
\<lbrakk>?x \<in> {A..B}; ?y \<in> {A..B}\<rbrakk> \<Longrightarrow> dist (c ?x) (c ?y) \<le> lambda * dist ?x ?y + C
\<lbrakk>?x \<in> {A..B}; ?y \<in> {A..B}\<rbrakk> \<Longrightarrow> 1 / lambda * dist ?x ?y - C \<le> dist (c ?x) (c ?y)
1 \<le> lambda
0 \<le> C
0 \<le> deltaG TYPE('a)

goal (1 subgoal):
 1. hausdorff_distance (c ` {A..B}) (d ` {A..B}) \<le> 184 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hausdorff_distance (c ` {A..B}) (d ` {A..B}) \<le> 184 * lambda\<^sup>2 * (C + deltaG TYPE('a))

goal (1 subgoal):
 1. A \<le> B \<Longrightarrow> hausdorff_distance (c ` {A..B}) (d ` {A..B}) \<le> 184 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A \<le> B \<Longrightarrow> hausdorff_distance (c ` {A..B}) (d ` {A..B}) \<le> 184 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
A \<le> B

goal (1 subgoal):
 1. A \<le> B \<Longrightarrow> hausdorff_distance (c ` {A..B}) (d ` {A..B}) \<le> 184 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
have "hausdorff_distance (c`{A..B}) {c A--c B} \<le> 92 * lambda^2 * (C + deltaG(TYPE('a)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hausdorff_distance (c ` {A..B}) {c A--c B} \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
by (rule Morse_Gromov_theorem[OF assms(1)], auto)
[PROOF STATE]
proof (state)
this:
hausdorff_distance (c ` {A..B}) {c A--c B} \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))

goal (1 subgoal):
 1. A \<le> B \<Longrightarrow> hausdorff_distance (c ` {A..B}) (d ` {A..B}) \<le> 184 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
hausdorff_distance (c ` {A..B}) {c A--c B} \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))

goal (1 subgoal):
 1. A \<le> B \<Longrightarrow> hausdorff_distance (c ` {A..B}) (d ` {A..B}) \<le> 184 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
have "hausdorff_distance {c A--c B} (d`{A..B}) \<le> 92 * lambda^2 * (C + deltaG(TYPE('a)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hausdorff_distance {c A--c B} (d ` {A..B}) \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
unfolding \<open>c A = d A\<close> \<open>c B = d B\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hausdorff_distance {d A--d B} (d ` {A..B}) \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
apply (subst hausdorff_distance_sym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hausdorff_distance (d ` {A..B}) {d A--d B} \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
by (rule Morse_Gromov_theorem[OF assms(2)], auto)
[PROOF STATE]
proof (state)
this:
hausdorff_distance {c A--c B} (d ` {A..B}) \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))

goal (1 subgoal):
 1. A \<le> B \<Longrightarrow> hausdorff_distance (c ` {A..B}) (d ` {A..B}) \<le> 184 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
hausdorff_distance {c A--c B} (d ` {A..B}) \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))

goal (1 subgoal):
 1. A \<le> B \<Longrightarrow> hausdorff_distance (c ` {A..B}) (d ` {A..B}) \<le> 184 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
have "hausdorff_distance (c`{A..B}) (d`{A..B}) \<le> hausdorff_distance (c`{A..B}) {c A--c B} + hausdorff_distance {c A--c B} (d`{A..B})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hausdorff_distance (c ` {A..B}) (d ` {A..B}) \<le> hausdorff_distance (c ` {A..B}) {c A--c B} + hausdorff_distance {c A--c B} (d ` {A..B})
[PROOF STEP]
apply (rule hausdorff_distance_triangle)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. {c A--c B} \<noteq> {}
 2. bounded {c A--c B}
[PROOF STEP]
using True compact_imp_bounded[OF some_geodesic_compact]
[PROOF STATE]
proof (prove)
using this:
A \<le> B
bounded {?x1--?S1--?y1}

goal (2 subgoals):
 1. {c A--c B} \<noteq> {}
 2. bounded {c A--c B}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hausdorff_distance (c ` {A..B}) (d ` {A..B}) \<le> hausdorff_distance (c ` {A..B}) {c A--c B} + hausdorff_distance {c A--c B} (d ` {A..B})

goal (1 subgoal):
 1. A \<le> B \<Longrightarrow> hausdorff_distance (c ` {A..B}) (d ` {A..B}) \<le> 184 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
hausdorff_distance (c ` {A..B}) {c A--c B} \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
hausdorff_distance {c A--c B} (d ` {A..B}) \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
hausdorff_distance (c ` {A..B}) (d ` {A..B}) \<le> hausdorff_distance (c ` {A..B}) {c A--c B} + hausdorff_distance {c A--c B} (d ` {A..B})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
hausdorff_distance (c ` {A..B}) {c A--c B} \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
hausdorff_distance {c A--c B} (d ` {A..B}) \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('a))
hausdorff_distance (c ` {A..B}) (d ` {A..B}) \<le> hausdorff_distance (c ` {A..B}) {c A--c B} + hausdorff_distance {c A--c B} (d ` {A..B})

goal (1 subgoal):
 1. hausdorff_distance (c ` {A..B}) (d ` {A..B}) \<le> 184 * lambda\<^sup>2 * (C + deltaG TYPE('a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hausdorff_distance (c ` {A..B}) (d ` {A..B}) \<le> 184 * lambda\<^sup>2 * (C + deltaG TYPE('a))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma geodesic_quasi_isometric_image:
  fixes f::"'a::metric_space \<Rightarrow> 'b::Gromov_hyperbolic_space_geodesic"
  assumes "lambda C-quasi_isometry_on UNIV f"
          "geodesic_segment_between G x y"
  shows "hausdorff_distance (f`G) {f x--f y} \<le> 92 * lambda^2 * (C + deltaG(TYPE('b)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hausdorff_distance (f ` G) {f x--f y} \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('b))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. hausdorff_distance (f ` G) {f x--f y} \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('b))
[PROOF STEP]
define c where "c = f o (geodesic_segment_param G x)"
[PROOF STATE]
proof (state)
this:
c = f \<circ> geodesic_segment_param G x

goal (1 subgoal):
 1. hausdorff_distance (f ` G) {f x--f y} \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('b))
[PROOF STEP]
have *: "(1 * lambda) (0 * lambda + C)-quasi_isometry_on {0..dist x y} c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 * lambda) (0 * lambda + C) -quasi_isometry_on {0..dist x y} c
[PROOF STEP]
unfolding c_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 * lambda) (0 * lambda + C) -quasi_isometry_on {0..dist x y} (f \<circ> geodesic_segment_param G x)
[PROOF STEP]
by (rule quasi_isometry_on_compose[where Y = UNIV], auto intro!: isometry_quasi_isometry_on simp add: assms)
[PROOF STATE]
proof (state)
this:
(1 * lambda) (0 * lambda + C) -quasi_isometry_on {0..dist x y} c

goal (1 subgoal):
 1. hausdorff_distance (f ` G) {f x--f y} \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('b))
[PROOF STEP]
have "hausdorff_distance (c`{0..dist x y}) {c 0--c (dist x y)} \<le> 92 * lambda^2 * (C + deltaG(TYPE('b)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hausdorff_distance (c ` {0..dist x y}) {c 0--c (dist x y)} \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('b))
[PROOF STEP]
apply (rule Morse_Gromov_theorem)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. lambda C -quasi_isometry_on {0..dist x y} c
 2. geodesic_segment_between {c 0--c (dist x y)} (c 0) (c (dist x y))
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
(1 * lambda) (0 * lambda + C) -quasi_isometry_on {0..dist x y} c

goal (2 subgoals):
 1. lambda C -quasi_isometry_on {0..dist x y} c
 2. geodesic_segment_between {c 0--c (dist x y)} (c 0) (c (dist x y))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hausdorff_distance (c ` {0..dist x y}) {c 0--c (dist x y)} \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('b))

goal (1 subgoal):
 1. hausdorff_distance (f ` G) {f x--f y} \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('b))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
hausdorff_distance (c ` {0..dist x y}) {c 0--c (dist x y)} \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('b))

goal (1 subgoal):
 1. hausdorff_distance (f ` G) {f x--f y} \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('b))
[PROOF STEP]
have "c`{0..dist x y} = f`G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c ` {0..dist x y} = f ` G
[PROOF STEP]
unfolding c_def image_comp[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` geodesic_segment_param G x ` {0..dist x y} = f ` G
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_between G x y

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

goal (1 subgoal):
 1. hausdorff_distance (f ` G) {f x--f y} \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('b))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
c ` {0..dist x y} = f ` G

goal (1 subgoal):
 1. hausdorff_distance (f ` G) {f x--f y} \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('b))
[PROOF STEP]
have "c 0 = f x" "c (dist x y) = f y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c 0 = f x &&& c (dist x y) = f y
[PROOF STEP]
unfolding c_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<circ> geodesic_segment_param G x) 0 = f x &&& (f \<circ> geodesic_segment_param G x) (dist x y) = f y
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
geodesic_segment_between G x y

goal (1 subgoal):
 1. (f \<circ> geodesic_segment_param G x) 0 = f x &&& (f \<circ> geodesic_segment_param G x) (dist x y) = f y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c 0 = f x
c (dist x y) = f y

goal (1 subgoal):
 1. hausdorff_distance (f ` G) {f x--f y} \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('b))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
hausdorff_distance (c ` {0..dist x y}) {c 0--c (dist x y)} \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('b))
c ` {0..dist x y} = f ` G
c 0 = f x
c (dist x y) = f y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
hausdorff_distance (c ` {0..dist x y}) {c 0--c (dist x y)} \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('b))
c ` {0..dist x y} = f ` G
c 0 = f x
c (dist x y) = f y

goal (1 subgoal):
 1. hausdorff_distance (f ` G) {f x--f y} \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('b))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hausdorff_distance (f ` G) {f x--f y} \<le> 92 * lambda\<^sup>2 * (C + deltaG TYPE('b))

goal:
No subgoals!
[PROOF STEP]
qed