[STATEMENT]
lemma geod_dist2:
  assumes "a \<le> 2^n" "b \<le> 2^p" "a/2^n \<le> b / 2^p"
  shows "dist (geod n a) (geod p b) = (b/2^p - a/2^n) * dist x0 y0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (geod n a) (geod p b) = (real b / 2 ^ p - real a / 2 ^ n) * dist x0 y0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist (geod n a) (geod p b) = (real b / 2 ^ p - real a / 2 ^ n) * dist x0 y0
[PROOF STEP]
define r where "r = max n p"
[PROOF STATE]
proof (state)
this:
r = max n p

goal (1 subgoal):
 1. dist (geod n a) (geod p b) = (real b / 2 ^ p - real a / 2 ^ n) * dist x0 y0
[PROOF STEP]
define ar where "ar = a * 2^(r - n)"
[PROOF STATE]
proof (state)
this:
ar = a * 2 ^ (r - n)

goal (1 subgoal):
 1. dist (geod n a) (geod p b) = (real b / 2 ^ p - real a / 2 ^ n) * dist x0 y0
[PROOF STEP]
have a: "ar / 2^r = a / 2^n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real ar / 2 ^ r = real a / 2 ^ n
[PROOF STEP]
unfolding ar_def r_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (a * 2 ^ (max n p - n)) / 2 ^ max n p = real a / 2 ^ n
[PROOF STEP]
by (auto simp add: divide_simps semiring_normalization_rules(26))
[PROOF STATE]
proof (state)
this:
real ar / 2 ^ r = real a / 2 ^ n

goal (1 subgoal):
 1. dist (geod n a) (geod p b) = (real b / 2 ^ p - real a / 2 ^ n) * dist x0 y0
[PROOF STEP]
have A: "geod r ar = geod n a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geod r ar = geod n a
[PROOF STEP]
unfolding ar_def r_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geod (max n p) (a * 2 ^ (max n p - n)) = geod n a
[PROOF STEP]
using geod_mult[of n a "max n p - n"]
[PROOF STATE]
proof (prove)
using this:
geod n a = geod (n + (max n p - n)) (a * 2 ^ (max n p - n))

goal (1 subgoal):
 1. geod (max n p) (a * 2 ^ (max n p - n)) = geod n a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
geod r ar = geod n a

goal (1 subgoal):
 1. dist (geod n a) (geod p b) = (real b / 2 ^ p - real a / 2 ^ n) * dist x0 y0
[PROOF STEP]
define br where "br = b * 2^(r - p)"
[PROOF STATE]
proof (state)
this:
br = b * 2 ^ (r - p)

goal (1 subgoal):
 1. dist (geod n a) (geod p b) = (real b / 2 ^ p - real a / 2 ^ n) * dist x0 y0
[PROOF STEP]
have b: "br / 2^r = b / 2^p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real br / 2 ^ r = real b / 2 ^ p
[PROOF STEP]
unfolding br_def r_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (b * 2 ^ (max n p - p)) / 2 ^ max n p = real b / 2 ^ p
[PROOF STEP]
by (auto simp add: divide_simps semiring_normalization_rules(26))
[PROOF STATE]
proof (state)
this:
real br / 2 ^ r = real b / 2 ^ p

goal (1 subgoal):
 1. dist (geod n a) (geod p b) = (real b / 2 ^ p - real a / 2 ^ n) * dist x0 y0
[PROOF STEP]
have B: "geod r br = geod p b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geod r br = geod p b
[PROOF STEP]
unfolding br_def r_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. geod (max n p) (b * 2 ^ (max n p - p)) = geod p b
[PROOF STEP]
using geod_mult[of p b "max n p - p"]
[PROOF STATE]
proof (prove)
using this:
geod p b = geod (p + (max n p - p)) (b * 2 ^ (max n p - p))

goal (1 subgoal):
 1. geod (max n p) (b * 2 ^ (max n p - p)) = geod p b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
geod r br = geod p b

goal (1 subgoal):
 1. dist (geod n a) (geod p b) = (real b / 2 ^ p - real a / 2 ^ n) * dist x0 y0
[PROOF STEP]
have "dist (geod n a) (geod p b) = dist (geod r ar) (geod r br)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (geod n a) (geod p b) = dist (geod r ar) (geod r br)
[PROOF STEP]
using A B
[PROOF STATE]
proof (prove)
using this:
geod r ar = geod n a
geod r br = geod p b

goal (1 subgoal):
 1. dist (geod n a) (geod p b) = dist (geod r ar) (geod r br)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (geod n a) (geod p b) = dist (geod r ar) (geod r br)

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

goal (1 subgoal):
 1. dist (geod n a) (geod p b) = (real b / 2 ^ p - real a / 2 ^ n) * dist x0 y0
[PROOF STEP]
have "... = (real br - ar) * dist x0 y0 / 2 ^r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (geod r ar) (geod r br) = (real br - real ar) * dist x0 y0 / 2 ^ r
[PROOF STEP]
apply (rule geod_dist)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ar \<le> br
 2. br \<le> 2 ^ r
[PROOF STEP]
using \<open>a/2^n \<le> b / 2^p\<close>
[PROOF STATE]
proof (prove)
using this:
real a / 2 ^ n \<le> real b / 2 ^ p

goal (2 subgoals):
 1. ar \<le> br
 2. br \<le> 2 ^ r
[PROOF STEP]
unfolding a[symmetric] b[symmetric]
[PROOF STATE]
proof (prove)
using this:
real ar / 2 ^ r \<le> real br / 2 ^ r

goal (2 subgoals):
 1. ar \<le> br
 2. br \<le> 2 ^ r
[PROOF STEP]
apply (auto simp add: divide_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ar \<le> br \<Longrightarrow> br \<le> 2 ^ r
[PROOF STEP]
using \<open>b \<le> 2^p\<close> b
[PROOF STATE]
proof (prove)
using this:
b \<le> 2 ^ p
real br / 2 ^ r = real b / 2 ^ p

goal (1 subgoal):
 1. ar \<le> br \<Longrightarrow> br \<le> 2 ^ r
[PROOF STEP]
apply (auto simp add: divide_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ar \<le> br; b \<le> 2 ^ p; real br * 2 ^ p = real b * 2 ^ r\<rbrakk> \<Longrightarrow> br \<le> 2 ^ r
[PROOF STEP]
by (metis br_def le_add_diff_inverse2 max.cobounded2 mult.commute mult_le_mono2 r_def semiring_normalization_rules(26))
[PROOF STATE]
proof (state)
this:
dist (geod r ar) (geod r br) = (real br - real ar) * dist x0 y0 / 2 ^ r

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

goal (1 subgoal):
 1. dist (geod n a) (geod p b) = (real b / 2 ^ p - real a / 2 ^ n) * dist x0 y0
[PROOF STEP]
have "... = (real br / 2^r - real ar / 2^r) * dist x0 y0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (real br - real ar) * dist x0 y0 / 2 ^ r = (real br / 2 ^ r - real ar / 2 ^ r) * dist x0 y0
[PROOF STEP]
by (auto simp add: algebra_simps divide_simps)
[PROOF STATE]
proof (state)
this:
(real br - real ar) * dist x0 y0 / 2 ^ r = (real br / 2 ^ r - real ar / 2 ^ r) * dist x0 y0

goal (1 subgoal):
 1. dist (geod n a) (geod p b) = (real b / 2 ^ p - real a / 2 ^ n) * dist x0 y0
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist (geod n a) (geod p b) = (real br / 2 ^ r - real ar / 2 ^ r) * dist x0 y0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dist (geod n a) (geod p b) = (real br / 2 ^ r - real ar / 2 ^ r) * dist x0 y0

goal (1 subgoal):
 1. dist (geod n a) (geod p b) = (real b / 2 ^ p - real a / 2 ^ n) * dist x0 y0
[PROOF STEP]
using a b
[PROOF STATE]
proof (prove)
using this:
dist (geod n a) (geod p b) = (real br / 2 ^ r - real ar / 2 ^ r) * dist x0 y0
real ar / 2 ^ r = real a / 2 ^ n
real br / 2 ^ r = real b / 2 ^ p

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma geod_dist3:
  assumes "a \<le> 2^n" "b \<le> 2^p"
  shows "dist (geod n a) (geod p b) = abs(b/2^p - a/2^n) * dist x0 y0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (geod n a) (geod p b) = \<bar>real b / 2 ^ p - real a / 2 ^ n\<bar> * dist x0 y0
[PROOF STEP]
apply (cases "a /2^n \<le> b/2^p", auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. real a / 2 ^ n \<le> real b / 2 ^ p \<Longrightarrow> dist (geod n a) (geod p b) = (real b / 2 ^ p - real a / 2 ^ n) * dist x0 y0
 2. \<not> real a / 2 ^ n \<le> real b / 2 ^ p \<Longrightarrow> dist (geod n a) (geod p b) = (real a / 2 ^ n - real b / 2 ^ p) * dist x0 y0
[PROOF STEP]
apply (rule geod_dist2[OF assms], auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> real a / 2 ^ n \<le> real b / 2 ^ p \<Longrightarrow> dist (geod n a) (geod p b) = (real a / 2 ^ n - real b / 2 ^ p) * dist x0 y0
[PROOF STEP]
apply (subst dist_commute, rule geod_dist2[OF assms(2) assms(1)], auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma geod:
  shows "\<exists>g. isometry_on {0..dist x0 y0} g \<and> g 0 = x0 \<and> g (dist x0 y0) = y0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>g. isometry_on {0..dist x0 y0} g \<and> g 0 = x0 \<and> g (dist x0 y0) = y0
[PROOF STEP]
proof (cases "x0 = y0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x0 = y0 \<Longrightarrow> \<exists>g. isometry_on {0..dist x0 y0} g \<and> g 0 = x0 \<and> g (dist x0 y0) = y0
 2. x0 \<noteq> y0 \<Longrightarrow> \<exists>g. isometry_on {0..dist x0 y0} g \<and> g 0 = x0 \<and> g (dist x0 y0) = y0
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x0 = y0

goal (2 subgoals):
 1. x0 = y0 \<Longrightarrow> \<exists>g. isometry_on {0..dist x0 y0} g \<and> g 0 = x0 \<and> g (dist x0 y0) = y0
 2. x0 \<noteq> y0 \<Longrightarrow> \<exists>g. isometry_on {0..dist x0 y0} g \<and> g 0 = x0 \<and> g (dist x0 y0) = y0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>g. isometry_on {0..dist x0 y0} g \<and> g 0 = x0 \<and> g (dist x0 y0) = y0
[PROOF STEP]
apply (rule exI[of _ "\<lambda>_. x0"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isometry_on {0..dist x0 y0} (\<lambda>_. x0) \<and> x0 = x0 \<and> x0 = y0
[PROOF STEP]
unfolding isometry_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>{0..dist x0 y0}. \<forall>y\<in>{0..dist x0 y0}. dist x0 x0 = dist x y) \<and> x0 = x0 \<and> x0 = y0
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
x0 = y0

goal (1 subgoal):
 1. (\<forall>x\<in>{0..dist x0 y0}. \<forall>y\<in>{0..dist x0 y0}. dist x0 x0 = dist x y) \<and> x0 = x0 \<and> x0 = y0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>g. isometry_on {0..dist x0 y0} g \<and> g 0 = x0 \<and> g (dist x0 y0) = y0

goal (1 subgoal):
 1. x0 \<noteq> y0 \<Longrightarrow> \<exists>g. isometry_on {0..dist x0 y0} g \<and> g 0 = x0 \<and> g (dist x0 y0) = y0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x0 \<noteq> y0 \<Longrightarrow> \<exists>g. isometry_on {0..dist x0 y0} g \<and> g 0 = x0 \<and> g (dist x0 y0) = y0
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x0 \<noteq> y0

goal (1 subgoal):
 1. x0 \<noteq> y0 \<Longrightarrow> \<exists>g. isometry_on {0..dist x0 y0} g \<and> g 0 = x0 \<and> g (dist x0 y0) = y0
[PROOF STEP]
define A where "A = {(real k/2^n) * dist x0 y0 |k n. k \<le> 2^n}"
[PROOF STATE]
proof (state)
this:
A = {real k / 2 ^ n * dist x0 y0 |k n. k \<le> 2 ^ n}

goal (1 subgoal):
 1. x0 \<noteq> y0 \<Longrightarrow> \<exists>g. isometry_on {0..dist x0 y0} g \<and> g 0 = x0 \<and> g (dist x0 y0) = y0
[PROOF STEP]
have "{0..dist x0 y0} \<subseteq> closure A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {0..dist x0 y0} \<subseteq> closure A
[PROOF STEP]
proof (auto simp add: closure_approachable dist_real_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x e. \<lbrakk>0 \<le> x; x \<le> dist x0 y0; 0 < e\<rbrakk> \<Longrightarrow> \<exists>y\<in>A. \<bar>y - x\<bar> < e
[PROOF STEP]
fix t::real
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x e. \<lbrakk>0 \<le> x; x \<le> dist x0 y0; 0 < e\<rbrakk> \<Longrightarrow> \<exists>y\<in>A. \<bar>y - x\<bar> < e
[PROOF STEP]
assume t: "0 \<le> t" "t \<le> dist x0 y0"
[PROOF STATE]
proof (state)
this:
0 \<le> t
t \<le> dist x0 y0

goal (1 subgoal):
 1. \<And>x e. \<lbrakk>0 \<le> x; x \<le> dist x0 y0; 0 < e\<rbrakk> \<Longrightarrow> \<exists>y\<in>A. \<bar>y - x\<bar> < e
[PROOF STEP]
fix e:: real
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x e. \<lbrakk>0 \<le> x; x \<le> dist x0 y0; 0 < e\<rbrakk> \<Longrightarrow> \<exists>y\<in>A. \<bar>y - x\<bar> < e
[PROOF STEP]
assume "e > 0"
[PROOF STATE]
proof (state)
this:
0 < e

goal (1 subgoal):
 1. \<And>x e. \<lbrakk>0 \<le> x; x \<le> dist x0 y0; 0 < e\<rbrakk> \<Longrightarrow> \<exists>y\<in>A. \<bar>y - x\<bar> < e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < e
[PROOF STEP]
obtain n::nat where n: "dist x0 y0/e < 2^n"
[PROOF STATE]
proof (prove)
using this:
0 < e

goal (1 subgoal):
 1. (\<And>n. dist x0 y0 / e < 2 ^ n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using one_less_numeral_iff real_arch_pow semiring_norm(76)
[PROOF STATE]
proof (prove)
using this:
0 < e
((1::?'a) < numeral ?n) = (num.One < ?n)
1 < ?x \<Longrightarrow> \<exists>n. ?y < ?x ^ n
(num.One < num.Bit0 ?n) = True

goal (1 subgoal):
 1. (\<And>n. dist x0 y0 / e < 2 ^ n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
dist x0 y0 / e < 2 ^ n

goal (1 subgoal):
 1. \<And>x e. \<lbrakk>0 \<le> x; x \<le> dist x0 y0; 0 < e\<rbrakk> \<Longrightarrow> \<exists>y\<in>A. \<bar>y - x\<bar> < e
[PROOF STEP]
define k where "k = floor (2^n * t/ dist x0 y0)"
[PROOF STATE]
proof (state)
this:
k = \<lfloor>2 ^ n * t / dist x0 y0\<rfloor>

goal (1 subgoal):
 1. \<And>x e. \<lbrakk>0 \<le> x; x \<le> dist x0 y0; 0 < e\<rbrakk> \<Longrightarrow> \<exists>y\<in>A. \<bar>y - x\<bar> < e
[PROOF STEP]
have "k \<le> 2^n * t/ dist x0 y0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int k \<le> 2 ^ n * t / dist x0 y0
[PROOF STEP]
unfolding k_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int \<lfloor>2 ^ n * t / dist x0 y0\<rfloor> \<le> 2 ^ n * t / dist x0 y0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real_of_int k \<le> 2 ^ n * t / dist x0 y0

goal (1 subgoal):
 1. \<And>x e. \<lbrakk>0 \<le> x; x \<le> dist x0 y0; 0 < e\<rbrakk> \<Longrightarrow> \<exists>y\<in>A. \<bar>y - x\<bar> < e
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real_of_int k \<le> 2 ^ n * t / dist x0 y0

goal (1 subgoal):
 1. \<And>x e. \<lbrakk>0 \<le> x; x \<le> dist x0 y0; 0 < e\<rbrakk> \<Longrightarrow> \<exists>y\<in>A. \<bar>y - x\<bar> < e
[PROOF STEP]
have "... \<le> 2^n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ n * t / dist x0 y0 \<le> 2 ^ n
[PROOF STEP]
using t False
[PROOF STATE]
proof (prove)
using this:
0 \<le> t
t \<le> dist x0 y0
x0 \<noteq> y0

goal (1 subgoal):
 1. 2 ^ n * t / dist x0 y0 \<le> 2 ^ n
[PROOF STEP]
by (auto simp add: algebra_simps divide_simps)
[PROOF STATE]
proof (state)
this:
2 ^ n * t / dist x0 y0 \<le> 2 ^ n

goal (1 subgoal):
 1. \<And>x e. \<lbrakk>0 \<le> x; x \<le> dist x0 y0; 0 < e\<rbrakk> \<Longrightarrow> \<exists>y\<in>A. \<bar>y - x\<bar> < e
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
real_of_int k \<le> 2 ^ n
[PROOF STEP]
have "k \<le> 2^n"
[PROOF STATE]
proof (prove)
using this:
real_of_int k \<le> 2 ^ n

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

goal (1 subgoal):
 1. \<And>x e. \<lbrakk>0 \<le> x; x \<le> dist x0 y0; 0 < e\<rbrakk> \<Longrightarrow> \<exists>y\<in>A. \<bar>y - x\<bar> < e
[PROOF STEP]
have "k \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> k
[PROOF STEP]
using t False
[PROOF STATE]
proof (prove)
using this:
0 \<le> t
t \<le> dist x0 y0
x0 \<noteq> y0

goal (1 subgoal):
 1. 0 \<le> k
[PROOF STEP]
unfolding k_def
[PROOF STATE]
proof (prove)
using this:
0 \<le> t
t \<le> dist x0 y0
x0 \<noteq> y0

goal (1 subgoal):
 1. 0 \<le> \<lfloor>2 ^ n * t / dist x0 y0\<rfloor>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> k

goal (1 subgoal):
 1. \<And>x e. \<lbrakk>0 \<le> x; x \<le> dist x0 y0; 0 < e\<rbrakk> \<Longrightarrow> \<exists>y\<in>A. \<bar>y - x\<bar> < e
[PROOF STEP]
define l where "l = nat k"
[PROOF STATE]
proof (state)
this:
l = nat k

goal (1 subgoal):
 1. \<And>x e. \<lbrakk>0 \<le> x; x \<le> dist x0 y0; 0 < e\<rbrakk> \<Longrightarrow> \<exists>y\<in>A. \<bar>y - x\<bar> < e
[PROOF STEP]
have "k = int l" "l \<le> 2^n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k = int l &&& l \<le> 2 ^ n
[PROOF STEP]
using \<open>k \<ge> 0\<close> \<open>k \<le> 2^n\<close> nat_le_iff
[PROOF STATE]
proof (prove)
using this:
0 \<le> k
k \<le> 2 ^ n
(nat ?x \<le> ?n) = (?x \<le> int ?n)

goal (1 subgoal):
 1. k = int l &&& l \<le> 2 ^ n
[PROOF STEP]
unfolding l_def
[PROOF STATE]
proof (prove)
using this:
0 \<le> k
k \<le> 2 ^ n
(nat ?x \<le> ?n) = (?x \<le> int ?n)

goal (1 subgoal):
 1. k = int (nat k) &&& nat k \<le> 2 ^ n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k = int l
l \<le> 2 ^ n

goal (1 subgoal):
 1. \<And>x e. \<lbrakk>0 \<le> x; x \<le> dist x0 y0; 0 < e\<rbrakk> \<Longrightarrow> \<exists>y\<in>A. \<bar>y - x\<bar> < e
[PROOF STEP]
have "abs (2^n * t/dist x0 y0 - k) \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>2 ^ n * t / dist x0 y0 - real_of_int k\<bar> \<le> 1
[PROOF STEP]
unfolding k_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>2 ^ n * t / dist x0 y0 - real_of_int \<lfloor>2 ^ n * t / dist x0 y0\<rfloor>\<bar> \<le> 1
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
\<bar>2 ^ n * t / dist x0 y0 - real_of_int k\<bar> \<le> 1

goal (1 subgoal):
 1. \<And>x e. \<lbrakk>0 \<le> x; x \<le> dist x0 y0; 0 < e\<rbrakk> \<Longrightarrow> \<exists>y\<in>A. \<bar>y - x\<bar> < e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<bar>2 ^ n * t / dist x0 y0 - real_of_int k\<bar> \<le> 1
[PROOF STEP]
have "abs(t - k/2^n * dist x0 y0) \<le> dist x0 y0 / 2^n"
[PROOF STATE]
proof (prove)
using this:
\<bar>2 ^ n * t / dist x0 y0 - real_of_int k\<bar> \<le> 1

goal (1 subgoal):
 1. \<bar>t - real_of_int k / 2 ^ n * dist x0 y0\<bar> \<le> dist x0 y0 / 2 ^ n
[PROOF STEP]
by (auto simp add: algebra_simps divide_simps False)
[PROOF STATE]
proof (state)
this:
\<bar>t - real_of_int k / 2 ^ n * dist x0 y0\<bar> \<le> dist x0 y0 / 2 ^ n

goal (1 subgoal):
 1. \<And>x e. \<lbrakk>0 \<le> x; x \<le> dist x0 y0; 0 < e\<rbrakk> \<Longrightarrow> \<exists>y\<in>A. \<bar>y - x\<bar> < e
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>t - real_of_int k / 2 ^ n * dist x0 y0\<bar> \<le> dist x0 y0 / 2 ^ n

goal (1 subgoal):
 1. \<And>x e. \<lbrakk>0 \<le> x; x \<le> dist x0 y0; 0 < e\<rbrakk> \<Longrightarrow> \<exists>y\<in>A. \<bar>y - x\<bar> < e
[PROOF STEP]
have "... < e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist x0 y0 / 2 ^ n < e
[PROOF STEP]
using n \<open>e > 0\<close>
[PROOF STATE]
proof (prove)
using this:
dist x0 y0 / e < 2 ^ n
0 < e

goal (1 subgoal):
 1. dist x0 y0 / 2 ^ n < e
[PROOF STEP]
by (auto simp add: algebra_simps divide_simps)
[PROOF STATE]
proof (state)
this:
dist x0 y0 / 2 ^ n < e

goal (1 subgoal):
 1. \<And>x e. \<lbrakk>0 \<le> x; x \<le> dist x0 y0; 0 < e\<rbrakk> \<Longrightarrow> \<exists>y\<in>A. \<bar>y - x\<bar> < e
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<bar>t - real_of_int k / 2 ^ n * dist x0 y0\<bar> < e
[PROOF STEP]
have "abs(t - k/2^n * dist x0 y0) < e"
[PROOF STATE]
proof (prove)
using this:
\<bar>t - real_of_int k / 2 ^ n * dist x0 y0\<bar> < e

goal (1 subgoal):
 1. \<bar>t - real_of_int k / 2 ^ n * dist x0 y0\<bar> < e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<bar>t - real_of_int k / 2 ^ n * dist x0 y0\<bar> < e

goal (1 subgoal):
 1. \<And>x e. \<lbrakk>0 \<le> x; x \<le> dist x0 y0; 0 < e\<rbrakk> \<Longrightarrow> \<exists>y\<in>A. \<bar>y - x\<bar> < e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<bar>t - real_of_int k / 2 ^ n * dist x0 y0\<bar> < e
[PROOF STEP]
have "abs(t - l/2^n * dist x0 y0) < e"
[PROOF STATE]
proof (prove)
using this:
\<bar>t - real_of_int k / 2 ^ n * dist x0 y0\<bar> < e

goal (1 subgoal):
 1. \<bar>t - real l / 2 ^ n * dist x0 y0\<bar> < e
[PROOF STEP]
using \<open>k = int l\<close>
[PROOF STATE]
proof (prove)
using this:
\<bar>t - real_of_int k / 2 ^ n * dist x0 y0\<bar> < e
k = int l

goal (1 subgoal):
 1. \<bar>t - real l / 2 ^ n * dist x0 y0\<bar> < e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<bar>t - real l / 2 ^ n * dist x0 y0\<bar> < e

goal (1 subgoal):
 1. \<And>x e. \<lbrakk>0 \<le> x; x \<le> dist x0 y0; 0 < e\<rbrakk> \<Longrightarrow> \<exists>y\<in>A. \<bar>y - x\<bar> < e
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<bar>t - real l / 2 ^ n * dist x0 y0\<bar> < e

goal (1 subgoal):
 1. \<And>x e. \<lbrakk>0 \<le> x; x \<le> dist x0 y0; 0 < e\<rbrakk> \<Longrightarrow> \<exists>y\<in>A. \<bar>y - x\<bar> < e
[PROOF STEP]
have "l/2^n * dist x0 y0 \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real l / 2 ^ n * dist x0 y0 \<in> A
[PROOF STEP]
unfolding A_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real l / 2 ^ n * dist x0 y0 \<in> {real k / 2 ^ n * dist x0 y0 |k n. k \<le> 2 ^ n}
[PROOF STEP]
using \<open>l \<le> 2^n\<close>
[PROOF STATE]
proof (prove)
using this:
l \<le> 2 ^ n

goal (1 subgoal):
 1. real l / 2 ^ n * dist x0 y0 \<in> {real k / 2 ^ n * dist x0 y0 |k n. k \<le> 2 ^ n}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real l / 2 ^ n * dist x0 y0 \<in> A

goal (1 subgoal):
 1. \<And>x e. \<lbrakk>0 \<le> x; x \<le> dist x0 y0; 0 < e\<rbrakk> \<Longrightarrow> \<exists>y\<in>A. \<bar>y - x\<bar> < e
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<bar>t - real l / 2 ^ n * dist x0 y0\<bar> < e
real l / 2 ^ n * dist x0 y0 \<in> A
[PROOF STEP]
show "\<exists>u\<in>A. abs(u - t) < e"
[PROOF STATE]
proof (prove)
using this:
\<bar>t - real l / 2 ^ n * dist x0 y0\<bar> < e
real l / 2 ^ n * dist x0 y0 \<in> A

goal (1 subgoal):
 1. \<exists>u\<in>A. \<bar>u - t\<bar> < e
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<exists>u\<in>A. \<bar>u - t\<bar> < e

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{0..dist x0 y0} \<subseteq> closure A

goal (1 subgoal):
 1. x0 \<noteq> y0 \<Longrightarrow> \<exists>g. isometry_on {0..dist x0 y0} g \<and> g 0 = x0 \<and> g (dist x0 y0) = y0
[PROOF STEP]
text \<open>For each dyadic point, we choose one representation of the form $K/2^N$, it is not important
  for us that it is the minimal one.\<close>
[PROOF STATE]
proof (state)
this:
{0..dist x0 y0} \<subseteq> closure A

goal (1 subgoal):
 1. x0 \<noteq> y0 \<Longrightarrow> \<exists>g. isometry_on {0..dist x0 y0} g \<and> g 0 = x0 \<and> g (dist x0 y0) = y0
[PROOF STEP]
define index where "index = (\<lambda>t. SOME i. t = real (fst i)/2^(snd i) * dist x0 y0 \<and> (fst i) \<le> 2^(snd i))"
[PROOF STATE]
proof (state)
this:
index = (\<lambda>t. SOME i. t = real (fst i) / 2 ^ snd i * dist x0 y0 \<and> fst i \<le> 2 ^ snd i)

goal (1 subgoal):
 1. x0 \<noteq> y0 \<Longrightarrow> \<exists>g. isometry_on {0..dist x0 y0} g \<and> g 0 = x0 \<and> g (dist x0 y0) = y0
[PROOF STEP]
define K where "K = (\<lambda>t. fst (index t))"
[PROOF STATE]
proof (state)
this:
K = (\<lambda>t. fst (index t))

goal (1 subgoal):
 1. x0 \<noteq> y0 \<Longrightarrow> \<exists>g. isometry_on {0..dist x0 y0} g \<and> g 0 = x0 \<and> g (dist x0 y0) = y0
[PROOF STEP]
define N where "N = (\<lambda>t. snd (index t))"
[PROOF STATE]
proof (state)
this:
N = (\<lambda>t. snd (index t))

goal (1 subgoal):
 1. x0 \<noteq> y0 \<Longrightarrow> \<exists>g. isometry_on {0..dist x0 y0} g \<and> g 0 = x0 \<and> g (dist x0 y0) = y0
[PROOF STEP]
have t: "t = K t/ 2^(N t) * dist x0 y0 \<and> K t \<le> 2^(N t)" if "t \<in> A" for t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t = real (K t) / 2 ^ N t * dist x0 y0 \<and> K t \<le> 2 ^ N t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t = real (K t) / 2 ^ N t * dist x0 y0 \<and> K t \<le> 2 ^ N t
[PROOF STEP]
obtain n k::nat where "t = k/2^n * dist x0 y0" "k \<le> 2^n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k n. \<lbrakk>t = real k / 2 ^ n * dist x0 y0; k \<le> 2 ^ n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>t\<in> A\<close>
[PROOF STATE]
proof (prove)
using this:
t \<in> A

goal (1 subgoal):
 1. (\<And>k n. \<lbrakk>t = real k / 2 ^ n * dist x0 y0; k \<le> 2 ^ n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding A_def
[PROOF STATE]
proof (prove)
using this:
t \<in> {real k / 2 ^ n * dist x0 y0 |k n. k \<le> 2 ^ n}

goal (1 subgoal):
 1. (\<And>k n. \<lbrakk>t = real k / 2 ^ n * dist x0 y0; k \<le> 2 ^ n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t = real k / 2 ^ n * dist x0 y0
k \<le> 2 ^ n

goal (1 subgoal):
 1. t = real (K t) / 2 ^ N t * dist x0 y0 \<and> K t \<le> 2 ^ N t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t = real k / 2 ^ n * dist x0 y0
k \<le> 2 ^ n
[PROOF STEP]
have *: "\<exists>i. t = real (fst i)/2^(snd i) * dist x0 y0 \<and> (fst i) \<le> 2^(snd i)"
[PROOF STATE]
proof (prove)
using this:
t = real k / 2 ^ n * dist x0 y0
k \<le> 2 ^ n

goal (1 subgoal):
 1. \<exists>i. t = real (fst i) / 2 ^ snd i * dist x0 y0 \<and> fst i \<le> 2 ^ snd i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>i. t = real (fst i) / 2 ^ snd i * dist x0 y0 \<and> fst i \<le> 2 ^ snd i

goal (1 subgoal):
 1. t = real (K t) / 2 ^ N t * dist x0 y0 \<and> K t \<le> 2 ^ N t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t = real (K t) / 2 ^ N t * dist x0 y0 \<and> K t \<le> 2 ^ N t
[PROOF STEP]
unfolding K_def N_def index_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t = real (fst (SOME i. t = real (fst i) / 2 ^ snd i * dist x0 y0 \<and> fst i \<le> 2 ^ snd i)) / 2 ^ snd (SOME i. t = real (fst i) / 2 ^ snd i * dist x0 y0 \<and> fst i \<le> 2 ^ snd i) * dist x0 y0 \<and> fst (SOME i. t = real (fst i) / 2 ^ snd i * dist x0 y0 \<and> fst i \<le> 2 ^ snd i) \<le> 2 ^ snd (SOME i. t = real (fst i) / 2 ^ snd i * dist x0 y0 \<and> fst i \<le> 2 ^ snd i)
[PROOF STEP]
using someI_ex[OF *]
[PROOF STATE]
proof (prove)
using this:
t = real (fst (SOME x. t = real (fst x) / 2 ^ snd x * dist x0 y0 \<and> fst x \<le> 2 ^ snd x)) / 2 ^ snd (SOME x. t = real (fst x) / 2 ^ snd x * dist x0 y0 \<and> fst x \<le> 2 ^ snd x) * dist x0 y0 \<and> fst (SOME x. t = real (fst x) / 2 ^ snd x * dist x0 y0 \<and> fst x \<le> 2 ^ snd x) \<le> 2 ^ snd (SOME x. t = real (fst x) / 2 ^ snd x * dist x0 y0 \<and> fst x \<le> 2 ^ snd x)

goal (1 subgoal):
 1. t = real (fst (SOME i. t = real (fst i) / 2 ^ snd i * dist x0 y0 \<and> fst i \<le> 2 ^ snd i)) / 2 ^ snd (SOME i. t = real (fst i) / 2 ^ snd i * dist x0 y0 \<and> fst i \<le> 2 ^ snd i) * dist x0 y0 \<and> fst (SOME i. t = real (fst i) / 2 ^ snd i * dist x0 y0 \<and> fst i \<le> 2 ^ snd i) \<le> 2 ^ snd (SOME i. t = real (fst i) / 2 ^ snd i * dist x0 y0 \<and> fst i \<le> 2 ^ snd i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t = real (K t) / 2 ^ N t * dist x0 y0 \<and> K t \<le> 2 ^ N t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?t \<in> A \<Longrightarrow> ?t = real (K ?t) / 2 ^ N ?t * dist x0 y0 \<and> K ?t \<le> 2 ^ N ?t

goal (1 subgoal):
 1. x0 \<noteq> y0 \<Longrightarrow> \<exists>g. isometry_on {0..dist x0 y0} g \<and> g 0 = x0 \<and> g (dist x0 y0) = y0
[PROOF STEP]
text \<open>We can now define our function on dyadic points.\<close>
[PROOF STATE]
proof (state)
this:
?t \<in> A \<Longrightarrow> ?t = real (K ?t) / 2 ^ N ?t * dist x0 y0 \<and> K ?t \<le> 2 ^ N ?t

goal (1 subgoal):
 1. x0 \<noteq> y0 \<Longrightarrow> \<exists>g. isometry_on {0..dist x0 y0} g \<and> g 0 = x0 \<and> g (dist x0 y0) = y0
[PROOF STEP]
define f where "f = (\<lambda>t. geod (N t) (K t))"
[PROOF STATE]
proof (state)
this:
f = (\<lambda>t. geod (N t) (K t))

goal (1 subgoal):
 1. x0 \<noteq> y0 \<Longrightarrow> \<exists>g. isometry_on {0..dist x0 y0} g \<and> g 0 = x0 \<and> g (dist x0 y0) = y0
[PROOF STEP]
have "0 \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<in> A
[PROOF STEP]
unfolding A_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<in> {real k / 2 ^ n * dist x0 y0 |k n. k \<le> 2 ^ n}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<in> A

goal (1 subgoal):
 1. x0 \<noteq> y0 \<Longrightarrow> \<exists>g. isometry_on {0..dist x0 y0} g \<and> g 0 = x0 \<and> g (dist x0 y0) = y0
[PROOF STEP]
have "f 0 = x0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f 0 = x0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f 0 = x0
[PROOF STEP]
have "0 = K 0 /2^(N 0) * dist x0 y0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 = real (K 0) / 2 ^ N 0 * dist x0 y0
[PROOF STEP]
using t \<open>0 \<in> A\<close>
[PROOF STATE]
proof (prove)
using this:
?t \<in> A \<Longrightarrow> ?t = real (K ?t) / 2 ^ N ?t * dist x0 y0 \<and> K ?t \<le> 2 ^ N ?t
0 \<in> A

goal (1 subgoal):
 1. 0 = real (K 0) / 2 ^ N 0 * dist x0 y0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 = real (K 0) / 2 ^ N 0 * dist x0 y0

goal (1 subgoal):
 1. f 0 = x0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 = real (K 0) / 2 ^ N 0 * dist x0 y0
[PROOF STEP]
have "K 0 = 0"
[PROOF STATE]
proof (prove)
using this:
0 = real (K 0) / 2 ^ N 0 * dist x0 y0

goal (1 subgoal):
 1. K 0 = 0
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
0 = real (K 0) / 2 ^ N 0 * dist x0 y0
x0 \<noteq> y0

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

goal (1 subgoal):
 1. f 0 = x0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
K 0 = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
K 0 = 0

goal (1 subgoal):
 1. f 0 = x0
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
using this:
K 0 = 0

goal (1 subgoal):
 1. geod (N 0) (K 0) = x0
[PROOF STEP]
using geod_0
[PROOF STATE]
proof (prove)
using this:
K 0 = 0
geod ?n 0 = x0

goal (1 subgoal):
 1. geod (N 0) (K 0) = x0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f 0 = x0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f 0 = x0

goal (1 subgoal):
 1. x0 \<noteq> y0 \<Longrightarrow> \<exists>g. isometry_on {0..dist x0 y0} g \<and> g 0 = x0 \<and> g (dist x0 y0) = y0
[PROOF STEP]
have "dist x0 y0 = (real 1/2^0) * dist x0 y0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist x0 y0 = real 1 / 2 ^ 0 * dist x0 y0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist x0 y0 = real 1 / 2 ^ 0 * dist x0 y0

goal (1 subgoal):
 1. x0 \<noteq> y0 \<Longrightarrow> \<exists>g. isometry_on {0..dist x0 y0} g \<and> g 0 = x0 \<and> g (dist x0 y0) = y0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dist x0 y0 = real 1 / 2 ^ 0 * dist x0 y0
[PROOF STEP]
have "dist x0 y0 \<in> A"
[PROOF STATE]
proof (prove)
using this:
dist x0 y0 = real 1 / 2 ^ 0 * dist x0 y0

goal (1 subgoal):
 1. dist x0 y0 \<in> A
[PROOF STEP]
unfolding A_def
[PROOF STATE]
proof (prove)
using this:
dist x0 y0 = real 1 / 2 ^ 0 * dist x0 y0

goal (1 subgoal):
 1. dist x0 y0 \<in> {real k / 2 ^ n * dist x0 y0 |k n. k \<le> 2 ^ n}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
dist x0 y0 \<in> A

goal (1 subgoal):
 1. x0 \<noteq> y0 \<Longrightarrow> \<exists>g. isometry_on {0..dist x0 y0} g \<and> g 0 = x0 \<and> g (dist x0 y0) = y0
[PROOF STEP]
have "f (dist x0 y0) = y0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (dist x0 y0) = y0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f (dist x0 y0) = y0
[PROOF STEP]
have "dist x0 y0 = K (dist x0 y0) / 2^(N (dist x0 y0)) * dist x0 y0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist x0 y0 = real (K (dist x0 y0)) / 2 ^ N (dist x0 y0) * dist x0 y0
[PROOF STEP]
using t \<open>dist x0 y0 \<in> A\<close>
[PROOF STATE]
proof (prove)
using this:
?t \<in> A \<Longrightarrow> ?t = real (K ?t) / 2 ^ N ?t * dist x0 y0 \<and> K ?t \<le> 2 ^ N ?t
dist x0 y0 \<in> A

goal (1 subgoal):
 1. dist x0 y0 = real (K (dist x0 y0)) / 2 ^ N (dist x0 y0) * dist x0 y0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist x0 y0 = real (K (dist x0 y0)) / 2 ^ N (dist x0 y0) * dist x0 y0

goal (1 subgoal):
 1. f (dist x0 y0) = y0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dist x0 y0 = real (K (dist x0 y0)) / 2 ^ N (dist x0 y0) * dist x0 y0
[PROOF STEP]
have "K (dist x0 y0) = 2^(N(dist x0 y0))"
[PROOF STATE]
proof (prove)
using this:
dist x0 y0 = real (K (dist x0 y0)) / 2 ^ N (dist x0 y0) * dist x0 y0

goal (1 subgoal):
 1. K (dist x0 y0) = 2 ^ N (dist x0 y0)
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
dist x0 y0 = real (K (dist x0 y0)) / 2 ^ N (dist x0 y0) * dist x0 y0
x0 \<noteq> y0

goal (1 subgoal):
 1. K (dist x0 y0) = 2 ^ N (dist x0 y0)
[PROOF STEP]
by (auto simp add: divide_simps)
[PROOF STATE]
proof (state)
this:
K (dist x0 y0) = 2 ^ N (dist x0 y0)

goal (1 subgoal):
 1. f (dist x0 y0) = y0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
K (dist x0 y0) = 2 ^ N (dist x0 y0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
K (dist x0 y0) = 2 ^ N (dist x0 y0)

goal (1 subgoal):
 1. f (dist x0 y0) = y0
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
using this:
K (dist x0 y0) = 2 ^ N (dist x0 y0)

goal (1 subgoal):
 1. geod (N (dist x0 y0)) (K (dist x0 y0)) = y0
[PROOF STEP]
using geod_end
[PROOF STATE]
proof (prove)
using this:
K (dist x0 y0) = 2 ^ N (dist x0 y0)
geod ?n (2 ^ ?n) = y0

goal (1 subgoal):
 1. geod (N (dist x0 y0)) (K (dist x0 y0)) = y0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f (dist x0 y0) = y0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f (dist x0 y0) = y0

goal (1 subgoal):
 1. x0 \<noteq> y0 \<Longrightarrow> \<exists>g. isometry_on {0..dist x0 y0} g \<and> g 0 = x0 \<and> g (dist x0 y0) = y0
[PROOF STEP]
text \<open>By construction, it is an isometry on dyadic points.\<close>
[PROOF STATE]
proof (state)
this:
f (dist x0 y0) = y0

goal (1 subgoal):
 1. x0 \<noteq> y0 \<Longrightarrow> \<exists>g. isometry_on {0..dist x0 y0} g \<and> g 0 = x0 \<and> g (dist x0 y0) = y0
[PROOF STEP]
have "isometry_on A f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isometry_on A f
[PROOF STEP]
proof (rule isometry_onI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> dist (f x) (f y) = dist x y
[PROOF STEP]
fix s t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> dist (f x) (f y) = dist x y
[PROOF STEP]
assume inA: "s \<in> A" "t \<in> A"
[PROOF STATE]
proof (state)
this:
s \<in> A
t \<in> A

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> dist (f x) (f y) = dist x y
[PROOF STEP]
have "dist (f s) (f t) = abs (K t/2^(N t) - K s/2^(N s)) * dist x0 y0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (f s) (f t) = \<bar>real (K t) / 2 ^ N t - real (K s) / 2 ^ N s\<bar> * dist x0 y0
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (geod (N s) (K s)) (geod (N t) (K t)) = \<bar>real (K t) / 2 ^ N t - real (K s) / 2 ^ N s\<bar> * dist x0 y0
[PROOF STEP]
apply (rule geod_dist3)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. K s \<le> 2 ^ N s
 2. K t \<le> 2 ^ N t
[PROOF STEP]
using t inA
[PROOF STATE]
proof (prove)
using this:
?t \<in> A \<Longrightarrow> ?t = real (K ?t) / 2 ^ N ?t * dist x0 y0 \<and> K ?t \<le> 2 ^ N ?t
s \<in> A
t \<in> A

goal (2 subgoals):
 1. K s \<le> 2 ^ N s
 2. K t \<le> 2 ^ N t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (f s) (f t) = \<bar>real (K t) / 2 ^ N t - real (K s) / 2 ^ N s\<bar> * dist x0 y0

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> dist (f x) (f y) = dist x y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (f s) (f t) = \<bar>real (K t) / 2 ^ N t - real (K s) / 2 ^ N s\<bar> * dist x0 y0

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> dist (f x) (f y) = dist x y
[PROOF STEP]
have "... = abs(K t/2^(N t) * dist x0 y0 - K s/2^(N s) * dist x0 y0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>real (K t) / 2 ^ N t - real (K s) / 2 ^ N s\<bar> * dist x0 y0 = \<bar>real (K t) / 2 ^ N t * dist x0 y0 - real (K s) / 2 ^ N s * dist x0 y0\<bar>
[PROOF STEP]
by (auto simp add: abs_mult_pos left_diff_distrib)
[PROOF STATE]
proof (state)
this:
\<bar>real (K t) / 2 ^ N t - real (K s) / 2 ^ N s\<bar> * dist x0 y0 = \<bar>real (K t) / 2 ^ N t * dist x0 y0 - real (K s) / 2 ^ N s * dist x0 y0\<bar>

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> dist (f x) (f y) = dist x y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>real (K t) / 2 ^ N t - real (K s) / 2 ^ N s\<bar> * dist x0 y0 = \<bar>real (K t) / 2 ^ N t * dist x0 y0 - real (K s) / 2 ^ N s * dist x0 y0\<bar>

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> dist (f x) (f y) = dist x y
[PROOF STEP]
have "... = abs(t - s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>real (K t) / 2 ^ N t * dist x0 y0 - real (K s) / 2 ^ N s * dist x0 y0\<bar> = \<bar>t - s\<bar>
[PROOF STEP]
using t inA
[PROOF STATE]
proof (prove)
using this:
?t \<in> A \<Longrightarrow> ?t = real (K ?t) / 2 ^ N ?t * dist x0 y0 \<and> K ?t \<le> 2 ^ N ?t
s \<in> A
t \<in> A

goal (1 subgoal):
 1. \<bar>real (K t) / 2 ^ N t * dist x0 y0 - real (K s) / 2 ^ N s * dist x0 y0\<bar> = \<bar>t - s\<bar>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<bar>real (K t) / 2 ^ N t * dist x0 y0 - real (K s) / 2 ^ N s * dist x0 y0\<bar> = \<bar>t - s\<bar>

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> dist (f x) (f y) = dist x y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist (f s) (f t) = \<bar>t - s\<bar>
[PROOF STEP]
show "dist (f s) (f t) = dist s t"
[PROOF STATE]
proof (prove)
using this:
dist (f s) (f t) = \<bar>t - s\<bar>

goal (1 subgoal):
 1. dist (f s) (f t) = dist s t
[PROOF STEP]
unfolding dist_real_def
[PROOF STATE]
proof (prove)
using this:
dist (f s) (f t) = \<bar>t - s\<bar>

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
isometry_on A f

goal (1 subgoal):
 1. x0 \<noteq> y0 \<Longrightarrow> \<exists>g. isometry_on {0..dist x0 y0} g \<and> g 0 = x0 \<and> g (dist x0 y0) = y0
[PROOF STEP]
text \<open>We can thus extend it to an isometry on the closure of dyadic points.
  It is the desired geodesic.\<close>
[PROOF STATE]
proof (state)
this:
isometry_on A f

goal (1 subgoal):
 1. x0 \<noteq> y0 \<Longrightarrow> \<exists>g. isometry_on {0..dist x0 y0} g \<and> g 0 = x0 \<and> g (dist x0 y0) = y0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
isometry_on A f
[PROOF STEP]
obtain g where g: "isometry_on (closure A) g" "\<And>t. t \<in> A \<Longrightarrow> g t = f t"
[PROOF STATE]
proof (prove)
using this:
isometry_on A f

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>isometry_on (closure A) g; \<And>t. t \<in> A \<Longrightarrow> g t = f t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using isometry_extend_closure
[PROOF STATE]
proof (prove)
using this:
isometry_on A f
isometry_on ?X ?f \<Longrightarrow> \<exists>g. isometry_on (closure ?X) g \<and> (\<forall>x\<in>?X. g x = ?f x)

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>isometry_on (closure A) g; \<And>t. t \<in> A \<Longrightarrow> g t = f t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
isometry_on (closure A) g
?t \<in> A \<Longrightarrow> g ?t = f ?t

goal (1 subgoal):
 1. x0 \<noteq> y0 \<Longrightarrow> \<exists>g. isometry_on {0..dist x0 y0} g \<and> g 0 = x0 \<and> g (dist x0 y0) = y0
[PROOF STEP]
have "isometry_on {0..dist x0 y0} g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isometry_on {0..dist x0 y0} g
[PROOF STEP]
by (rule isometry_on_subset[OF \<open>isometry_on (closure A) g\<close> \<open>{0..dist x0 y0} \<subseteq> closure A\<close>])
[PROOF STATE]
proof (state)
this:
isometry_on {0..dist x0 y0} g

goal (1 subgoal):
 1. x0 \<noteq> y0 \<Longrightarrow> \<exists>g. isometry_on {0..dist x0 y0} g \<and> g 0 = x0 \<and> g (dist x0 y0) = y0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
isometry_on {0..dist x0 y0} g

goal (1 subgoal):
 1. x0 \<noteq> y0 \<Longrightarrow> \<exists>g. isometry_on {0..dist x0 y0} g \<and> g 0 = x0 \<and> g (dist x0 y0) = y0
[PROOF STEP]
have "g 0 = x0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g 0 = x0
[PROOF STEP]
using g(2)[OF \<open>0 \<in> A\<close>] \<open>f 0 = x0\<close>
[PROOF STATE]
proof (prove)
using this:
g 0 = f 0
f 0 = x0

goal (1 subgoal):
 1. g 0 = x0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
g 0 = x0

goal (1 subgoal):
 1. x0 \<noteq> y0 \<Longrightarrow> \<exists>g. isometry_on {0..dist x0 y0} g \<and> g 0 = x0 \<and> g (dist x0 y0) = y0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
g 0 = x0

goal (1 subgoal):
 1. x0 \<noteq> y0 \<Longrightarrow> \<exists>g. isometry_on {0..dist x0 y0} g \<and> g 0 = x0 \<and> g (dist x0 y0) = y0
[PROOF STEP]
have "g (dist x0 y0) = y0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g (dist x0 y0) = y0
[PROOF STEP]
using g(2)[OF \<open>dist x0 y0 \<in> A\<close>] \<open>f (dist x0 y0) = y0\<close>
[PROOF STATE]
proof (prove)
using this:
g (dist x0 y0) = f (dist x0 y0)
f (dist x0 y0) = y0

goal (1 subgoal):
 1. g (dist x0 y0) = y0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
g (dist x0 y0) = y0

goal (1 subgoal):
 1. x0 \<noteq> y0 \<Longrightarrow> \<exists>g. isometry_on {0..dist x0 y0} g \<and> g 0 = x0 \<and> g (dist x0 y0) = y0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
isometry_on {0..dist x0 y0} g
g 0 = x0
g (dist x0 y0) = y0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
isometry_on {0..dist x0 y0} g
g 0 = x0
g (dist x0 y0) = y0

goal (1 subgoal):
 1. \<exists>g. isometry_on {0..dist x0 y0} g \<and> g 0 = x0 \<and> g (dist x0 y0) = y0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>g. isometry_on {0..dist x0 y0} g \<and> g 0 = x0 \<and> g (dist x0 y0) = y0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem complete_with_middles_imp_geodesic:
  assumes "\<And>x y::('a::complete_space). \<exists>m. dist x m = dist x y /2 \<and> dist m y = dist x y /2"
  shows "OFCLASS('a, geodesic_space_class)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OFCLASS('a, geodesic_space_class)
[PROOF STEP]
proof (standard, rule geodesic_subsetI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> UNIV; y \<in> UNIV\<rbrakk> \<Longrightarrow> \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> UNIV
[PROOF STEP]
fix x0 y0::'a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> UNIV; y \<in> UNIV\<rbrakk> \<Longrightarrow> \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> UNIV
[PROOF STEP]
interpret complete_space_with_middle x0 y0
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. complete_space_with_middle TYPE('a)
[PROOF STEP]
apply standard
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<exists>z. dist x z = dist x y / 2 \<and> dist z y = dist x y / 2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<exists>m. dist ?x m = dist ?x ?y / 2 \<and> dist m ?y = dist ?x ?y / 2

goal (1 subgoal):
 1. \<And>x y. \<exists>z. dist x z = dist x y / 2 \<and> dist z y = dist x y / 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> UNIV; y \<in> UNIV\<rbrakk> \<Longrightarrow> \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> UNIV
[PROOF STEP]
have "\<exists>g. g 0 = x0 \<and> g (dist x0 y0) = y0 \<and> isometry_on {0..dist x0 y0} g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>g. g 0 = x0 \<and> g (dist x0 y0) = y0 \<and> isometry_on {0..dist x0 y0} g
[PROOF STEP]
using geod
[PROOF STATE]
proof (prove)
using this:
\<exists>g. isometry_on {0..dist x0 y0} g \<and> g 0 = x0 \<and> g (dist x0 y0) = y0

goal (1 subgoal):
 1. \<exists>g. g 0 = x0 \<and> g (dist x0 y0) = y0 \<and> isometry_on {0..dist x0 y0} g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>g. g 0 = x0 \<and> g (dist x0 y0) = y0 \<and> isometry_on {0..dist x0 y0} g

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> UNIV; y \<in> UNIV\<rbrakk> \<Longrightarrow> \<exists>G. geodesic_segment_between G x y \<and> G \<subseteq> UNIV
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>g. g 0 = x0 \<and> g (dist x0 y0) = y0 \<and> isometry_on {0..dist x0 y0} g
[PROOF STEP]
show "\<exists>G. geodesic_segment_between G x0 y0 \<and> G \<subseteq> UNIV"
[PROOF STATE]
proof (prove)
using this:
\<exists>g. g 0 = x0 \<and> g (dist x0 y0) = y0 \<and> isometry_on {0..dist x0 y0} g

goal (1 subgoal):
 1. \<exists>G. geodesic_segment_between G x0 y0 \<and> G \<subseteq> UNIV
[PROOF STEP]
unfolding geodesic_segment_between_def
[PROOF STATE]
proof (prove)
using this:
\<exists>g. g 0 = x0 \<and> g (dist x0 y0) = y0 \<and> isometry_on {0..dist x0 y0} g

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma quasi_isometry_onD:
  assumes "lambda C-quasi_isometry_on X f"
  shows "\<And>x y. x \<in> X \<Longrightarrow> y \<in> X \<Longrightarrow> dist (f x) (f y) \<le> lambda * dist x y + C"
        "\<And>x y. x \<in> X \<Longrightarrow> y \<in> X \<Longrightarrow> dist (f x) (f y) \<ge> (1/lambda) * dist x y - C"
        "lambda \<ge> 1" "C \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> dist (f x) (f y) \<le> lambda * dist x y + C) &&& (\<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> 1 / lambda * dist x y - C \<le> dist (f x) (f y))) &&& 1 \<le> lambda &&& 0 \<le> C
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
lambda C -quasi_isometry_on X f

goal (1 subgoal):
 1. ((\<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> dist (f x) (f y) \<le> lambda * dist x y + C) &&& (\<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> 1 / lambda * dist x y - C \<le> dist (f x) (f y))) &&& 1 \<le> lambda &&& 0 \<le> C
[PROOF STEP]
unfolding quasi_isometry_on_def
[PROOF STATE]
proof (prove)
using this:
1 \<le> lambda \<and> 0 \<le> C \<and> (\<forall>x\<in>X. \<forall>y\<in>X. dist (f x) (f y) \<le> lambda * dist x y + C \<and> 1 / lambda * dist x y - C \<le> dist (f x) (f y))

goal (1 subgoal):
 1. ((\<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> dist (f x) (f y) \<le> lambda * dist x y + C) &&& (\<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> 1 / lambda * dist x y - C \<le> dist (f x) (f y))) &&& 1 \<le> lambda &&& 0 \<le> C
[PROOF STEP]
by auto


[STATEMENT]
lemma quasi_isometry_onI [intro]:
  assumes "\<And>x y. x \<in> X \<Longrightarrow> y \<in> X \<Longrightarrow> dist (f x) (f y) \<le> lambda * dist x y + C"
          "\<And>x y. x \<in> X \<Longrightarrow> y \<in> X \<Longrightarrow> dist (f x) (f y) \<ge> (1/lambda) * dist x y - C"
          "lambda \<ge> 1" "C \<ge> 0"
  shows "lambda C-quasi_isometry_on X f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lambda C -quasi_isometry_on X f
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> X; ?y \<in> X\<rbrakk> \<Longrightarrow> dist (f ?x) (f ?y) \<le> lambda * dist ?x ?y + C
\<lbrakk>?x \<in> X; ?y \<in> X\<rbrakk> \<Longrightarrow> 1 / lambda * dist ?x ?y - C \<le> dist (f ?x) (f ?y)
1 \<le> lambda
0 \<le> C

goal (1 subgoal):
 1. lambda C -quasi_isometry_on X f
[PROOF STEP]
unfolding quasi_isometry_on_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> X; ?y \<in> X\<rbrakk> \<Longrightarrow> dist (f ?x) (f ?y) \<le> lambda * dist ?x ?y + C
\<lbrakk>?x \<in> X; ?y \<in> X\<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 \<and> 0 \<le> C \<and> (\<forall>x\<in>X. \<forall>y\<in>X. dist (f x) (f y) \<le> lambda * dist x y + C \<and> 1 / lambda * dist x y - C \<le> dist (f x) (f y))
[PROOF STEP]
by auto


[STATEMENT]
lemma isometry_quasi_isometry_on:
  assumes "isometry_on X f"
  shows "1 0-quasi_isometry_on X f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 0 -quasi_isometry_on X f
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
isometry_on X f

goal (1 subgoal):
 1. 1 0 -quasi_isometry_on X f
[PROOF STEP]
unfolding isometry_on_def quasi_isometry_on_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>X. \<forall>y\<in>X. dist (f x) (f y) = dist x y

goal (1 subgoal):
 1. 1 \<le> 1 \<and> 0 \<le> 0 \<and> (\<forall>x\<in>X. \<forall>y\<in>X. dist (f x) (f y) \<le> 1 * dist x y + 0 \<and> 1 / 1 * dist x y - 0 \<le> dist (f x) (f y))
[PROOF STEP]
by auto


[STATEMENT]
lemma quasi_isometry_on_change_params:
  assumes "lambda C-quasi_isometry_on X f" "mu \<ge> lambda" "D \<ge> C"
  shows "mu D-quasi_isometry_on X f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mu D -quasi_isometry_on X f
[PROOF STEP]
proof (rule quasi_isometry_onI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> dist (f x) (f y) \<le> mu * dist x y + D
 2. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> 1 / mu * dist x y - D \<le> dist (f x) (f y)
 3. 1 \<le> mu
 4. 0 \<le> D
[PROOF STEP]
have P1: "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(1)]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> X; ?y \<in> X\<rbrakk> \<Longrightarrow> dist (f ?x) (f ?y) \<le> lambda * dist ?x ?y + C
\<lbrakk>?x \<in> X; ?y \<in> X\<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 (4 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> dist (f x) (f y) \<le> mu * dist x y + D
 2. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> 1 / mu * dist x y - D \<le> dist (f x) (f y)
 3. 1 \<le> mu
 4. 0 \<le> D
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
1 \<le> lambda
0 \<le> C
[PROOF STEP]
show P2: "mu \<ge> 1" "D \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
1 \<le> lambda
0 \<le> C

goal (1 subgoal):
 1. 1 \<le> mu &&& 0 \<le> D
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
1 \<le> lambda
0 \<le> C
lambda C -quasi_isometry_on X f
lambda \<le> mu
C \<le> D

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

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> dist (f x) (f y) \<le> mu * dist x y + D
 2. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> 1 / mu * dist x y - D \<le> dist (f x) (f y)
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> dist (f x) (f y) \<le> mu * dist x y + D
 2. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> 1 / mu * dist x y - D \<le> dist (f x) (f y)
[PROOF STEP]
assume inX: "x \<in> X" "y \<in> X"
[PROOF STATE]
proof (state)
this:
x \<in> X
y \<in> X

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> dist (f x) (f y) \<le> mu * dist x y + D
 2. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> 1 / mu * dist x y - D \<le> dist (f x) (f y)
[PROOF STEP]
have "dist (f x) (f y) \<le> lambda * dist x y + C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (f x) (f y) \<le> lambda * dist x y + C
[PROOF STEP]
using quasi_isometry_onD[OF assms(1)] inX
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> X; ?y \<in> X\<rbrakk> \<Longrightarrow> dist (f ?x) (f ?y) \<le> lambda * dist ?x ?y + C
\<lbrakk>?x \<in> X; ?y \<in> X\<rbrakk> \<Longrightarrow> 1 / lambda * dist ?x ?y - C \<le> dist (f ?x) (f ?y)
1 \<le> lambda
0 \<le> C
x \<in> X
y \<in> X

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

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> dist (f x) (f y) \<le> mu * dist x y + D
 2. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> 1 / mu * dist x y - D \<le> dist (f x) (f y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (f x) (f y) \<le> lambda * dist x y + C

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> dist (f x) (f y) \<le> mu * dist x y + D
 2. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> 1 / mu * dist x y - D \<le> dist (f x) (f y)
[PROOF STEP]
have "... \<le> mu * dist x y + D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lambda * dist x y + C \<le> mu * dist x y + D
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
lambda C -quasi_isometry_on X f
lambda \<le> mu
C \<le> D

goal (1 subgoal):
 1. lambda * dist x y + C \<le> mu * dist x y + D
[PROOF STEP]
by (auto intro!: mono_intros)
[PROOF STATE]
proof (state)
this:
lambda * dist x y + C \<le> mu * dist x y + D

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> dist (f x) (f y) \<le> mu * dist x y + D
 2. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> 1 / mu * dist x y - D \<le> dist (f x) (f y)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist (f x) (f y) \<le> mu * dist x y + D
[PROOF STEP]
show "dist (f x) (f y) \<le> mu * dist x y + D"
[PROOF STATE]
proof (prove)
using this:
dist (f x) (f y) \<le> mu * dist x y + D

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

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> 1 / mu * dist x y - D \<le> dist (f x) (f y)
[PROOF STEP]
have "dist (f x) (f y) \<ge> (1/lambda) * dist x y - C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / lambda * dist x y - C \<le> dist (f x) (f y)
[PROOF STEP]
using quasi_isometry_onD[OF assms(1)] inX
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> X; ?y \<in> X\<rbrakk> \<Longrightarrow> dist (f ?x) (f ?y) \<le> lambda * dist ?x ?y + C
\<lbrakk>?x \<in> X; ?y \<in> X\<rbrakk> \<Longrightarrow> 1 / lambda * dist ?x ?y - C \<le> dist (f ?x) (f ?y)
1 \<le> lambda
0 \<le> C
x \<in> X
y \<in> X

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

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> 1 / mu * dist x y - D \<le> dist (f x) (f y)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
1 / lambda * dist x y - C \<le> dist (f x) (f y)

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> 1 / mu * dist x y - D \<le> dist (f x) (f y)
[PROOF STEP]
have "(1/lambda) * dist x y + (- C) \<ge> (1/mu) * dist x y + (- D)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / mu * dist x y + - D \<le> 1 / lambda * dist x y + - C
[PROOF STEP]
apply (intro mono_intros)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. 1 / mu \<le> 1 / lambda
 2. 0 \<le> dist x y
 3. C \<le> D
[PROOF STEP]
using P1 P2 assms
[PROOF STATE]
proof (prove)
using this:
1 \<le> lambda
0 \<le> C
1 \<le> mu
0 \<le> D
lambda C -quasi_isometry_on X f
lambda \<le> mu
C \<le> D

goal (3 subgoals):
 1. 1 / mu \<le> 1 / lambda
 2. 0 \<le> dist x y
 3. C \<le> D
[PROOF STEP]
by (auto simp add: divide_simps)
[PROOF STATE]
proof (state)
this:
1 / mu * dist x y + - D \<le> 1 / lambda * dist x y + - C

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> 1 / mu * dist x y - D \<le> dist (f x) (f y)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
1 / lambda * dist x y - C \<le> dist (f x) (f y)
1 / mu * dist x y + - D \<le> 1 / lambda * dist x y + - C
[PROOF STEP]
show "dist (f x) (f y) \<ge> (1/mu) * dist x y - D"
[PROOF STATE]
proof (prove)
using this:
1 / lambda * dist x y - C \<le> dist (f x) (f y)
1 / mu * dist x y + - D \<le> 1 / lambda * dist x y + - C

goal (1 subgoal):
 1. 1 / mu * dist x y - D \<le> dist (f x) (f y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 / mu * dist x y - D \<le> dist (f x) (f y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma quasi_isometry_on_perturb:
  assumes "lambda C-quasi_isometry_on X f"
          "D \<ge> 0"
          "\<And>x. x \<in> X \<Longrightarrow> dist (f x) (g x) \<le> D"
  shows "lambda (C + 2 * D)-quasi_isometry_on X g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lambda (C + 2 * D) -quasi_isometry_on X g
[PROOF STEP]
proof (rule quasi_isometry_onI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> dist (g x) (g y) \<le> lambda * dist x y + (C + 2 * D)
 2. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> 1 / lambda * dist x y - (C + 2 * D) \<le> dist (g x) (g y)
 3. 1 \<le> lambda
 4. 0 \<le> C + 2 * D
[PROOF STEP]
show "lambda \<ge> 1" "C + 2 * D \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> lambda &&& 0 \<le> C + 2 * D
[PROOF STEP]
using \<open>D \<ge> 0\<close> quasi_isometry_onD[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
0 \<le> D
\<lbrakk>?x \<in> X; ?y \<in> X\<rbrakk> \<Longrightarrow> dist (f ?x) (f ?y) \<le> lambda * dist ?x ?y + C
\<lbrakk>?x \<in> X; ?y \<in> X\<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 + 2 * D
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 \<le> lambda
0 \<le> C + 2 * D

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> dist (g x) (g y) \<le> lambda * dist x y + (C + 2 * D)
 2. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> 1 / lambda * dist x y - (C + 2 * D) \<le> dist (g x) (g y)
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> dist (g x) (g y) \<le> lambda * dist x y + (C + 2 * D)
 2. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> 1 / lambda * dist x y - (C + 2 * D) \<le> dist (g x) (g y)
[PROOF STEP]
assume *: "x \<in> X" "y \<in> X"
[PROOF STATE]
proof (state)
this:
x \<in> X
y \<in> X

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> dist (g x) (g y) \<le> lambda * dist x y + (C + 2 * D)
 2. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> 1 / lambda * dist x y - (C + 2 * D) \<le> dist (g x) (g y)
[PROOF STEP]
have "dist (g x) (g y) \<le> dist (f x) (f y) + 2 * D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (g x) (g y) \<le> dist (f x) (f y) + 2 * D
[PROOF STEP]
using assms(3)[OF *(1)] assms(3)[OF *(2)] dist_triangle4[of "g x" "g y" "f x" "f y"]
[PROOF STATE]
proof (prove)
using this:
dist (f x) (g x) \<le> D
dist (f y) (g y) \<le> D
dist (g x) (g y) \<le> dist (g x) (f x) + dist (f x) (f y) + dist (f y) (g y)

goal (1 subgoal):
 1. dist (g x) (g y) \<le> dist (f x) (f y) + 2 * D
[PROOF STEP]
by (simp add: dist_commute)
[PROOF STATE]
proof (state)
this:
dist (g x) (g y) \<le> dist (f x) (f y) + 2 * D

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> dist (g x) (g y) \<le> lambda * dist x y + (C + 2 * D)
 2. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> 1 / lambda * dist x y - (C + 2 * D) \<le> dist (g x) (g y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dist (g x) (g y) \<le> dist (f x) (f y) + 2 * D
[PROOF STEP]
show "dist (g x) (g y) \<le> lambda * dist x y + (C + 2 * D)"
[PROOF STATE]
proof (prove)
using this:
dist (g x) (g y) \<le> dist (f x) (f y) + 2 * D

goal (1 subgoal):
 1. dist (g x) (g y) \<le> lambda * dist x y + (C + 2 * D)
[PROOF STEP]
using quasi_isometry_onD(1)[OF assms(1) *]
[PROOF STATE]
proof (prove)
using this:
dist (g x) (g y) \<le> dist (f x) (f y) + 2 * D
dist (f x) (f y) \<le> lambda * dist x y + C

goal (1 subgoal):
 1. dist (g x) (g y) \<le> lambda * dist x y + (C + 2 * D)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (g x) (g y) \<le> lambda * dist x y + (C + 2 * D)

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> 1 / lambda * dist x y - (C + 2 * D) \<le> dist (g x) (g y)
[PROOF STEP]
have "dist (g x) (g y) \<ge> dist (f x) (f y) - 2 * D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (f x) (f y) - 2 * D \<le> dist (g x) (g y)
[PROOF STEP]
using assms(3)[OF *(1)] assms(3)[OF *(2)] dist_triangle4[of "f x" "f y" "g x" "g y"]
[PROOF STATE]
proof (prove)
using this:
dist (f x) (g x) \<le> D
dist (f y) (g y) \<le> D
dist (f x) (f y) \<le> dist (f x) (g x) + dist (g x) (g y) + dist (g y) (f y)

goal (1 subgoal):
 1. dist (f x) (f y) - 2 * D \<le> dist (g x) (g y)
[PROOF STEP]
by (simp add: dist_commute)
[PROOF STATE]
proof (state)
this:
dist (f x) (f y) - 2 * D \<le> dist (g x) (g y)

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> 1 / lambda * dist x y - (C + 2 * D) \<le> dist (g x) (g y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dist (f x) (f y) - 2 * D \<le> dist (g x) (g y)
[PROOF STEP]
show "dist (g x) (g y) \<ge> (1/lambda) * dist x y - (C + 2 * D)"
[PROOF STATE]
proof (prove)
using this:
dist (f x) (f y) - 2 * D \<le> dist (g x) (g y)

goal (1 subgoal):
 1. 1 / lambda * dist x y - (C + 2 * D) \<le> dist (g x) (g y)
[PROOF STEP]
using quasi_isometry_onD(2)[OF assms(1) *]
[PROOF STATE]
proof (prove)
using this:
dist (f x) (f y) - 2 * D \<le> dist (g x) (g y)
1 / lambda * dist x y - C \<le> dist (f x) (f y)

goal (1 subgoal):
 1. 1 / lambda * dist x y - (C + 2 * D) \<le> dist (g x) (g y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 / lambda * dist x y - (C + 2 * D) \<le> dist (g x) (g y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma quasi_isometry_on_compose:
  assumes "lambda C-quasi_isometry_on X f"
          "mu D-quasi_isometry_on Y g"
          "f`X \<subseteq> Y"
  shows "(lambda * mu) (C * mu + D)-quasi_isometry_on X (g o f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (lambda * mu) (C * mu + D) -quasi_isometry_on X (g \<circ> f)
[PROOF STEP]
proof (rule quasi_isometry_onI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> dist ((g \<circ> f) x) ((g \<circ> f) y) \<le> lambda * mu * dist x y + (C * mu + D)
 2. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> 1 / (lambda * mu) * dist x y - (C * mu + D) \<le> dist ((g \<circ> f) x) ((g \<circ> f) y)
 3. 1 \<le> lambda * mu
 4. 0 \<le> C * mu + D
[PROOF STEP]
have I: "lambda \<ge> 1" "C \<ge> 0" "mu \<ge> 1" "D \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 \<le> lambda &&& 0 \<le> C) &&& 1 \<le> mu &&& 0 \<le> D
[PROOF STEP]
using quasi_isometry_onD[OF assms(1)] quasi_isometry_onD[OF assms(2)]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> X; ?y \<in> X\<rbrakk> \<Longrightarrow> dist (f ?x) (f ?y) \<le> lambda * dist ?x ?y + C
\<lbrakk>?x \<in> X; ?y \<in> X\<rbrakk> \<Longrightarrow> 1 / lambda * dist ?x ?y - C \<le> dist (f ?x) (f ?y)
1 \<le> lambda
0 \<le> C
\<lbrakk>?x \<in> Y; ?y \<in> Y\<rbrakk> \<Longrightarrow> dist (g ?x) (g ?y) \<le> mu * dist ?x ?y + D
\<lbrakk>?x \<in> Y; ?y \<in> Y\<rbrakk> \<Longrightarrow> 1 / mu * dist ?x ?y - D \<le> dist (g ?x) (g ?y)
1 \<le> mu
0 \<le> D

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

goal (4 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> dist ((g \<circ> f) x) ((g \<circ> f) y) \<le> lambda * mu * dist x y + (C * mu + D)
 2. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> 1 / (lambda * mu) * dist x y - (C * mu + D) \<le> dist ((g \<circ> f) x) ((g \<circ> f) y)
 3. 1 \<le> lambda * mu
 4. 0 \<le> C * mu + D
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
1 \<le> lambda
0 \<le> C
1 \<le> mu
0 \<le> D
[PROOF STEP]
show "lambda * mu \<ge> 1" "C * mu + D \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
1 \<le> lambda
0 \<le> C
1 \<le> mu
0 \<le> D

goal (1 subgoal):
 1. 1 \<le> lambda * mu &&& 0 \<le> C * mu + D
[PROOF STEP]
by (auto, metis dual_order.order_iff_strict le_numeral_extra(2) mult_le_cancel_right1 order.strict_trans1)
[PROOF STATE]
proof (state)
this:
1 \<le> lambda * mu
0 \<le> C * mu + D

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> dist ((g \<circ> f) x) ((g \<circ> f) y) \<le> lambda * mu * dist x y + (C * mu + D)
 2. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> 1 / (lambda * mu) * dist x y - (C * mu + D) \<le> dist ((g \<circ> f) x) ((g \<circ> f) y)
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> dist ((g \<circ> f) x) ((g \<circ> f) y) \<le> lambda * mu * dist x y + (C * mu + D)
 2. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> 1 / (lambda * mu) * dist x y - (C * mu + D) \<le> dist ((g \<circ> f) x) ((g \<circ> f) y)
[PROOF STEP]
assume inX: "x \<in> X" "y \<in> X"
[PROOF STATE]
proof (state)
this:
x \<in> X
y \<in> X

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> dist ((g \<circ> f) x) ((g \<circ> f) y) \<le> lambda * mu * dist x y + (C * mu + D)
 2. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> 1 / (lambda * mu) * dist x y - (C * mu + D) \<le> dist ((g \<circ> f) x) ((g \<circ> f) y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> X
y \<in> X
[PROOF STEP]
have inY: "f x \<in> Y" "f y \<in> Y"
[PROOF STATE]
proof (prove)
using this:
x \<in> X
y \<in> X

goal (1 subgoal):
 1. f x \<in> Y &&& f y \<in> Y
[PROOF STEP]
using \<open>f`X \<subseteq> Y\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> X
y \<in> X
f ` X \<subseteq> Y

goal (1 subgoal):
 1. f x \<in> Y &&& f y \<in> Y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f x \<in> Y
f y \<in> Y

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> dist ((g \<circ> f) x) ((g \<circ> f) y) \<le> lambda * mu * dist x y + (C * mu + D)
 2. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> 1 / (lambda * mu) * dist x y - (C * mu + D) \<le> dist ((g \<circ> f) x) ((g \<circ> f) y)
[PROOF STEP]
have "dist ((g o f) x) ((g o f) y) \<le> mu * dist (f x) (f y) + D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist ((g \<circ> f) x) ((g \<circ> f) y) \<le> mu * dist (f x) (f y) + D
[PROOF STEP]
using quasi_isometry_onD(1)[OF assms(2) inY]
[PROOF STATE]
proof (prove)
using this:
dist (g (f x)) (g (f y)) \<le> mu * dist (f x) (f y) + D

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

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> dist ((g \<circ> f) x) ((g \<circ> f) y) \<le> lambda * mu * dist x y + (C * mu + D)
 2. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> 1 / (lambda * mu) * dist x y - (C * mu + D) \<le> dist ((g \<circ> f) x) ((g \<circ> f) y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist ((g \<circ> f) x) ((g \<circ> f) y) \<le> mu * dist (f x) (f y) + D

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> dist ((g \<circ> f) x) ((g \<circ> f) y) \<le> lambda * mu * dist x y + (C * mu + D)
 2. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> 1 / (lambda * mu) * dist x y - (C * mu + D) \<le> dist ((g \<circ> f) x) ((g \<circ> f) y)
[PROOF STEP]
have "... \<le> mu * (lambda * dist x y + C) + D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mu * dist (f x) (f y) + D \<le> mu * (lambda * dist x y + C) + D
[PROOF STEP]
using \<open>mu \<ge> 1\<close> quasi_isometry_onD(1)[OF assms(1) inX]
[PROOF STATE]
proof (prove)
using this:
1 \<le> mu
dist (f x) (f y) \<le> lambda * dist x y + C

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

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> dist ((g \<circ> f) x) ((g \<circ> f) y) \<le> lambda * mu * dist x y + (C * mu + D)
 2. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> 1 / (lambda * mu) * dist x y - (C * mu + D) \<le> dist ((g \<circ> f) x) ((g \<circ> f) y)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist ((g \<circ> f) x) ((g \<circ> f) y) \<le> mu * (lambda * dist x y + C) + D
[PROOF STEP]
show "dist ((g o f) x) ((g o f) y) \<le> (lambda * mu) * dist x y + (C * mu + D)"
[PROOF STATE]
proof (prove)
using this:
dist ((g \<circ> f) x) ((g \<circ> f) y) \<le> mu * (lambda * dist x y + C) + D

goal (1 subgoal):
 1. dist ((g \<circ> f) x) ((g \<circ> f) y) \<le> lambda * mu * dist x y + (C * mu + D)
[PROOF STEP]
by (auto simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
dist ((g \<circ> f) x) ((g \<circ> f) y) \<le> lambda * mu * dist x y + (C * mu + D)

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> 1 / (lambda * mu) * dist x y - (C * mu + D) \<le> dist ((g \<circ> f) x) ((g \<circ> f) y)
[PROOF STEP]
have "(1/(lambda * mu)) * dist x y - (C * mu + D) \<le> (1/(lambda * mu)) * dist x y - (C/mu + D)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / (lambda * mu) * dist x y - (C * mu + D) \<le> 1 / (lambda * mu) * dist x y - (C / mu + D)
[PROOF STEP]
using \<open>mu \<ge> 1\<close> \<open>C \<ge> 0\<close>
[PROOF STATE]
proof (prove)
using this:
1 \<le> mu
0 \<le> C

goal (1 subgoal):
 1. 1 / (lambda * mu) * dist x y - (C * mu + D) \<le> 1 / (lambda * mu) * dist x y - (C / mu + D)
[PROOF STEP]
apply (auto, auto simp add: divide_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 \<le> mu; 0 \<le> C\<rbrakk> \<Longrightarrow> C \<le> C * mu * mu
[PROOF STEP]
by (metis eq_iff less_eq_real_def mult.commute mult_eq_0_iff mult_le_cancel_right1 order.trans)
[PROOF STATE]
proof (state)
this:
1 / (lambda * mu) * dist x y - (C * mu + D) \<le> 1 / (lambda * mu) * dist x y - (C / mu + D)

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> 1 / (lambda * mu) * dist x y - (C * mu + D) \<le> dist ((g \<circ> f) x) ((g \<circ> f) y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 / (lambda * mu) * dist x y - (C * mu + D) \<le> 1 / (lambda * mu) * dist x y - (C / mu + D)

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> 1 / (lambda * mu) * dist x y - (C * mu + D) \<le> dist ((g \<circ> f) x) ((g \<circ> f) y)
[PROOF STEP]
have "... = (1/mu) * ((1/lambda) * dist x y - C) - D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / (lambda * mu) * dist x y - (C / mu + D) = 1 / mu * (1 / lambda * dist x y - C) - D
[PROOF STEP]
by (auto simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
1 / (lambda * mu) * dist x y - (C / mu + D) = 1 / mu * (1 / lambda * dist x y - C) - D

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> 1 / (lambda * mu) * dist x y - (C * mu + D) \<le> dist ((g \<circ> f) x) ((g \<circ> f) y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 / (lambda * mu) * dist x y - (C / mu + D) = 1 / mu * (1 / lambda * dist x y - C) - D

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> 1 / (lambda * mu) * dist x y - (C * mu + D) \<le> dist ((g \<circ> f) x) ((g \<circ> f) y)
[PROOF STEP]
have "... \<le> (1/mu) * dist (f x) (f y) - D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / mu * (1 / lambda * dist x y - C) - D \<le> 1 / mu * dist (f x) (f y) - D
[PROOF STEP]
using \<open>mu \<ge> 1\<close> quasi_isometry_onD(2)[OF assms(1) inX]
[PROOF STATE]
proof (prove)
using this:
1 \<le> mu
1 / lambda * dist x y - C \<le> dist (f x) (f y)

goal (1 subgoal):
 1. 1 / mu * (1 / lambda * dist x y - C) - D \<le> 1 / mu * dist (f x) (f y) - D
[PROOF STEP]
by (auto simp add: divide_simps)
[PROOF STATE]
proof (state)
this:
1 / mu * (1 / lambda * dist x y - C) - D \<le> 1 / mu * dist (f x) (f y) - D

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> 1 / (lambda * mu) * dist x y - (C * mu + D) \<le> dist ((g \<circ> f) x) ((g \<circ> f) y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 / mu * (1 / lambda * dist x y - C) - D \<le> 1 / mu * dist (f x) (f y) - D

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> 1 / (lambda * mu) * dist x y - (C * mu + D) \<le> dist ((g \<circ> f) x) ((g \<circ> f) y)
[PROOF STEP]
have "... \<le> dist ((g o f) x) ((g o f) y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / mu * dist (f x) (f y) - D \<le> dist ((g \<circ> f) x) ((g \<circ> f) y)
[PROOF STEP]
using quasi_isometry_onD(2)[OF assms(2) inY]
[PROOF STATE]
proof (prove)
using this:
1 / mu * dist (f x) (f y) - D \<le> dist (g (f x)) (g (f y))

goal (1 subgoal):
 1. 1 / mu * dist (f x) (f y) - D \<le> dist ((g \<circ> f) x) ((g \<circ> f) y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 / mu * dist (f x) (f y) - D \<le> dist ((g \<circ> f) x) ((g \<circ> f) y)

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> 1 / (lambda * mu) * dist x y - (C * mu + D) \<le> dist ((g \<circ> f) x) ((g \<circ> f) y)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
1 / (lambda * mu) * dist x y - (C * mu + D) \<le> dist ((g \<circ> f) x) ((g \<circ> f) y)
[PROOF STEP]
show "1 / (lambda * mu) * dist x y - (C * mu + D) \<le> dist ((g \<circ> f) x) ((g \<circ> f) y)"
[PROOF STATE]
proof (prove)
using this:
1 / (lambda * mu) * dist x y - (C * mu + D) \<le> dist ((g \<circ> f) x) ((g \<circ> f) y)

goal (1 subgoal):
 1. 1 / (lambda * mu) * dist x y - (C * mu + D) \<le> dist ((g \<circ> f) x) ((g \<circ> f) y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 / (lambda * mu) * dist x y - (C * mu + D) \<le> dist ((g \<circ> f) x) ((g \<circ> f) y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma quasi_isometry_on_bounded:
  assumes "lambda C-quasi_isometry_on X f"
          "bounded X"
  shows "bounded (f`X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded (f ` X)
[PROOF STEP]
proof (cases "X = {}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. X = {} \<Longrightarrow> bounded (f ` X)
 2. X \<noteq> {} \<Longrightarrow> bounded (f ` X)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
X = {}

goal (2 subgoals):
 1. X = {} \<Longrightarrow> bounded (f ` X)
 2. X \<noteq> {} \<Longrightarrow> bounded (f ` X)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
X = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
X = {}

goal (1 subgoal):
 1. bounded (f ` X)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bounded (f ` X)

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> bounded (f ` X)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> bounded (f ` X)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
X \<noteq> {}

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> bounded (f ` X)
[PROOF STEP]
obtain x where "x \<in> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. x \<in> X \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
X \<noteq> {}

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

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> bounded (f ` X)
[PROOF STEP]
obtain e where e: "\<And>z. z \<in> X \<Longrightarrow> dist x z \<le> e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>e. (\<And>z. z \<in> X \<Longrightarrow> dist x z \<le> e) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using bounded_any_center assms(2)
[PROOF STATE]
proof (prove)
using this:
bounded ?S = (\<exists>e. \<forall>y\<in>?S. dist ?a y \<le> e)
bounded X

goal (1 subgoal):
 1. (\<And>e. (\<And>z. z \<in> X \<Longrightarrow> dist x z \<le> e) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
?z \<in> X \<Longrightarrow> dist x ?z \<le> e

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> bounded (f ` X)
[PROOF STEP]
have "dist (f x) y \<le> C + lambda * e" if "y \<in> f`X" for y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (f x) y \<le> C + lambda * e
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist (f x) y \<le> C + lambda * e
[PROOF STEP]
obtain z where *: "z \<in> X" "y = f z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>z. \<lbrakk>z \<in> X; y = f z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>y \<in> f`X\<close>
[PROOF STATE]
proof (prove)
using this:
y \<in> f ` X

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

goal (1 subgoal):
 1. dist (f x) y \<le> C + lambda * e
[PROOF STEP]
have "dist (f x) y \<le> lambda * dist x z + C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (f x) y \<le> lambda * dist x z + C
[PROOF STEP]
unfolding \<open>y = f z\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (f x) (f z) \<le> lambda * dist x z + C
[PROOF STEP]
using * quasi_isometry_onD(1)[OF assms(1) \<open>x \<in> X\<close> \<open>z \<in> X\<close>]
[PROOF STATE]
proof (prove)
using this:
z \<in> X
y = f z
dist (f x) (f z) \<le> lambda * dist x z + C

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

goal (1 subgoal):
 1. dist (f x) y \<le> C + lambda * e
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (f x) y \<le> lambda * dist x z + C

goal (1 subgoal):
 1. dist (f x) y \<le> C + lambda * e
[PROOF STEP]
have "... \<le> C + lambda * e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lambda * dist x z + C \<le> C + lambda * e
[PROOF STEP]
using e[OF \<open>z \<in> X\<close>] quasi_isometry_onD(3)[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
dist x z \<le> e
1 \<le> lambda

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?y \<in> f ` X \<Longrightarrow> dist (f x) ?y \<le> C + lambda * e

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> bounded (f ` X)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?y \<in> f ` X \<Longrightarrow> dist (f x) ?y \<le> C + lambda * e
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?y \<in> f ` X \<Longrightarrow> dist (f x) ?y \<le> C + lambda * e

goal (1 subgoal):
 1. bounded (f ` X)
[PROOF STEP]
unfolding bounded_def
[PROOF STATE]
proof (prove)
using this:
?y \<in> f ` X \<Longrightarrow> dist (f x) ?y \<le> C + lambda * e

goal (1 subgoal):
 1. \<exists>x e. \<forall>y\<in>f ` X. dist x y \<le> e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bounded (f ` X)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma quasi_isometry_on_empty:
  assumes "C \<ge> 0" "lambda \<ge> 1"
  shows "lambda C-quasi_isometry_on {} f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lambda C -quasi_isometry_on {} f
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 \<le> C
1 \<le> lambda

goal (1 subgoal):
 1. lambda C -quasi_isometry_on {} f
[PROOF STEP]
unfolding quasi_isometry_on_def
[PROOF STATE]
proof (prove)
using this:
0 \<le> C
1 \<le> lambda

goal (1 subgoal):
 1. 1 \<le> lambda \<and> 0 \<le> C \<and> (\<forall>x\<in>{}. \<forall>y\<in>{}. dist (f x) (f y) \<le> lambda * dist x y + C \<and> 1 / lambda * dist x y - C \<le> dist (f x) (f y))
[PROOF STEP]
by auto


[STATEMENT]
lemma quasi_isometry_on_infdist:
  assumes "lambda C-quasi_isometry_on X f"
          "w \<in> X"
          "S \<subseteq> X"
  shows "infdist (f w) (f`S) \<le> lambda * infdist w S + C"
        "infdist (f w) (f`S) \<ge> (1/lambda) * infdist w S - C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infdist (f w) (f ` S) \<le> lambda * infdist w S + C &&& 1 / lambda * infdist w S - C \<le> infdist (f w) (f ` S)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. infdist (f w) (f ` S) \<le> lambda * infdist w S + C
 2. 1 / lambda * infdist w S - C \<le> infdist (f w) (f ` S)
[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(1)]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> X; ?y \<in> X\<rbrakk> \<Longrightarrow> dist (f ?x) (f ?y) \<le> lambda * dist ?x ?y + C
\<lbrakk>?x \<in> X; ?y \<in> X\<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. infdist (f w) (f ` S) \<le> lambda * infdist w S + C
 2. 1 / lambda * infdist w S - C \<le> infdist (f w) (f ` S)
[PROOF STEP]
show "infdist (f w) (f`S) \<le> lambda * infdist w S + C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infdist (f w) (f ` S) \<le> lambda * infdist w S + C
[PROOF STEP]
proof (cases "S = {}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. S = {} \<Longrightarrow> infdist (f w) (f ` S) \<le> lambda * infdist w S + C
 2. S \<noteq> {} \<Longrightarrow> infdist (f w) (f ` S) \<le> lambda * infdist w S + C
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
S = {}

goal (2 subgoals):
 1. S = {} \<Longrightarrow> infdist (f w) (f ` S) \<le> lambda * infdist w S + C
 2. S \<noteq> {} \<Longrightarrow> infdist (f w) (f ` S) \<le> lambda * infdist w S + C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
S = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
S = {}

goal (1 subgoal):
 1. infdist (f w) (f ` S) \<le> lambda * infdist w S + C
[PROOF STEP]
using \<open>C \<ge> 0\<close>
[PROOF STATE]
proof (prove)
using this:
S = {}
0 \<le> C

goal (1 subgoal):
 1. infdist (f w) (f ` S) \<le> lambda * infdist w S + C
[PROOF STEP]
unfolding infdist_def
[PROOF STATE]
proof (prove)
using this:
S = {}
0 \<le> C

goal (1 subgoal):
 1. (if f ` S = {} then 0 else Inf (dist (f w) ` f ` S)) \<le> lambda * (if S = {} then 0 else Inf (dist w ` S)) + C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
infdist (f w) (f ` S) \<le> lambda * infdist w S + C

goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> infdist (f w) (f ` S) \<le> lambda * infdist w S + C
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> infdist (f w) (f ` S) \<le> lambda * infdist w S + C
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
S \<noteq> {}

goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> infdist (f w) (f ` S) \<le> lambda * infdist w S + C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
S \<noteq> {}
[PROOF STEP]
have "(INF x\<in>S. dist (f w) (f x)) \<le> (INF x\<in>S. lambda * dist w x + C)"
[PROOF STATE]
proof (prove)
using this:
S \<noteq> {}

goal (1 subgoal):
 1. (INF x\<in>S. dist (f w) (f x)) \<le> (INF x\<in>S. lambda * dist w x + C)
[PROOF STEP]
apply (rule cINF_superset_mono)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. bdd_below ((\<lambda>x. dist (f w) (f x)) ` S)
 2. S \<subseteq> S
 3. \<And>x. x \<in> S \<Longrightarrow> dist (f w) (f x) \<le> lambda * dist w x + C
[PROOF STEP]
apply (meson bdd_belowI2 zero_le_dist)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. S \<subseteq> S
 2. \<And>x. x \<in> S \<Longrightarrow> dist (f w) (f x) \<le> lambda * dist w x + C
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
lambda C -quasi_isometry_on X f
w \<in> X
S \<subseteq> X

goal (2 subgoals):
 1. S \<subseteq> S
 2. \<And>x. x \<in> S \<Longrightarrow> dist (f w) (f x) \<le> lambda * dist w x + C
[PROOF STEP]
by (auto intro!: quasi_isometry_onD(1)[OF assms(1)])
[PROOF STATE]
proof (state)
this:
(INF x\<in>S. dist (f w) (f x)) \<le> (INF x\<in>S. lambda * dist w x + C)

goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> infdist (f w) (f ` S) \<le> lambda * infdist w S + C
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(INF x\<in>S. dist (f w) (f x)) \<le> (INF x\<in>S. lambda * dist w x + C)

goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> infdist (f w) (f ` S) \<le> lambda * infdist w S + C
[PROOF STEP]
have "... = (INF t\<in>(dist w)`S. lambda * t + C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (INF x\<in>S. lambda * dist w x + C) = (INF t\<in>dist w ` S. lambda * t + C)
[PROOF STEP]
by (auto simp add: image_comp)
[PROOF STATE]
proof (state)
this:
(INF x\<in>S. lambda * dist w x + C) = (INF t\<in>dist w ` S. lambda * t + C)

goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> infdist (f w) (f ` S) \<le> lambda * infdist w S + C
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(INF x\<in>S. lambda * dist w x + C) = (INF t\<in>dist w ` S. lambda * t + C)

goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> infdist (f w) (f ` S) \<le> lambda * infdist w S + C
[PROOF STEP]
have "... = lambda * Inf ((dist w)`S) + C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (INF t\<in>dist w ` S. lambda * t + C) = lambda * Inf (dist w ` S) + C
[PROOF STEP]
apply (rule continuous_at_Inf_mono[symmetric])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. mono (\<lambda>s. lambda * s + C)
 2. continuous (at_right (Inf (dist w ` S))) (\<lambda>s. lambda * s + C)
 3. dist w ` S \<noteq> {}
 4. bdd_below (dist w ` S)
[PROOF STEP]
unfolding mono_def
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<forall>x y. x \<le> y \<longrightarrow> lambda * x + C \<le> lambda * y + C
 2. continuous (at_right (Inf (dist w ` S))) (\<lambda>s. lambda * s + C)
 3. dist w ` S \<noteq> {}
 4. bdd_below (dist w ` S)
[PROOF STEP]
using \<open>lambda \<ge> 1\<close> False
[PROOF STATE]
proof (prove)
using this:
1 \<le> lambda
S \<noteq> {}

goal (4 subgoals):
 1. \<forall>x y. x \<le> y \<longrightarrow> lambda * x + C \<le> lambda * y + C
 2. continuous (at_right (Inf (dist w ` S))) (\<lambda>s. lambda * s + C)
 3. dist w ` S \<noteq> {}
 4. bdd_below (dist w ` S)
[PROOF STEP]
by (auto intro!: continuous_intros)
[PROOF STATE]
proof (state)
this:
(INF t\<in>dist w ` S. lambda * t + C) = lambda * Inf (dist w ` S) + C

goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> infdist (f w) (f ` S) \<le> lambda * infdist w S + C
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(INF x\<in>S. dist (f w) (f x)) \<le> lambda * Inf (dist w ` S) + C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(INF x\<in>S. dist (f w) (f x)) \<le> lambda * Inf (dist w ` S) + C

goal (1 subgoal):
 1. infdist (f w) (f ` S) \<le> lambda * infdist w S + C
[PROOF STEP]
unfolding infdist_def
[PROOF STATE]
proof (prove)
using this:
(INF x\<in>S. dist (f w) (f x)) \<le> lambda * Inf (dist w ` S) + C

goal (1 subgoal):
 1. (if f ` S = {} then 0 else Inf (dist (f w) ` f ` S)) \<le> lambda * (if S = {} then 0 else Inf (dist w ` S)) + C
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
(INF x\<in>S. dist (f w) (f x)) \<le> lambda * Inf (dist w ` S) + C
S \<noteq> {}

goal (1 subgoal):
 1. (if f ` S = {} then 0 else Inf (dist (f w) ` f ` S)) \<le> lambda * (if S = {} then 0 else Inf (dist w ` S)) + C
[PROOF STEP]
by (auto simp add: image_comp)
[PROOF STATE]
proof (state)
this:
infdist (f w) (f ` S) \<le> lambda * infdist w S + C

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
infdist (f w) (f ` S) \<le> lambda * infdist w S + C

goal (1 subgoal):
 1. 1 / lambda * infdist w S - C \<le> infdist (f w) (f ` S)
[PROOF STEP]
show "1 / lambda * infdist w S - C \<le> infdist (f w) (f ` S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / lambda * infdist w S - C \<le> infdist (f w) (f ` S)
[PROOF STEP]
proof (cases "S = {}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. S = {} \<Longrightarrow> 1 / lambda * infdist w S - C \<le> infdist (f w) (f ` S)
 2. S \<noteq> {} \<Longrightarrow> 1 / lambda * infdist w S - C \<le> infdist (f w) (f ` S)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
S = {}

goal (2 subgoals):
 1. S = {} \<Longrightarrow> 1 / lambda * infdist w S - C \<le> infdist (f w) (f ` S)
 2. S \<noteq> {} \<Longrightarrow> 1 / lambda * infdist w S - C \<le> infdist (f w) (f ` S)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
S = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
S = {}

goal (1 subgoal):
 1. 1 / lambda * infdist w S - C \<le> infdist (f w) (f ` S)
[PROOF STEP]
using \<open>C \<ge> 0\<close>
[PROOF STATE]
proof (prove)
using this:
S = {}
0 \<le> C

goal (1 subgoal):
 1. 1 / lambda * infdist w S - C \<le> infdist (f w) (f ` S)
[PROOF STEP]
unfolding infdist_def
[PROOF STATE]
proof (prove)
using this:
S = {}
0 \<le> C

goal (1 subgoal):
 1. 1 / lambda * (if S = {} then 0 else Inf (dist w ` S)) - C \<le> (if f ` S = {} then 0 else Inf (dist (f w) ` f ` S))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 / lambda * infdist w S - C \<le> infdist (f w) (f ` S)

goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> 1 / lambda * infdist w S - C \<le> infdist (f w) (f ` S)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> 1 / lambda * infdist w S - C \<le> infdist (f w) (f ` S)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
S \<noteq> {}

goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> 1 / lambda * infdist w S - C \<le> infdist (f w) (f ` S)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
S \<noteq> {}
[PROOF STEP]
have "(1/lambda) * infdist w S - C = (1/lambda) * Inf ((dist w)`S) - C"
[PROOF STATE]
proof (prove)
using this:
S \<noteq> {}

goal (1 subgoal):
 1. 1 / lambda * infdist w S - C = 1 / lambda * Inf (dist w ` S) - C
[PROOF STEP]
unfolding infdist_def
[PROOF STATE]
proof (prove)
using this:
S \<noteq> {}

goal (1 subgoal):
 1. 1 / lambda * (if S = {} then 0 else Inf (dist w ` S)) - C = 1 / lambda * Inf (dist w ` S) - C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 / lambda * infdist w S - C = 1 / lambda * Inf (dist w ` S) - C

goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> 1 / lambda * infdist w S - C \<le> infdist (f w) (f ` S)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 / lambda * infdist w S - C = 1 / lambda * Inf (dist w ` S) - C

goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> 1 / lambda * infdist w S - C \<le> infdist (f w) (f ` S)
[PROOF STEP]
have "... = (INF t\<in>(dist w)`S. (1/lambda) * t - C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / lambda * Inf (dist w ` S) - C = (INF t\<in>dist w ` S. 1 / lambda * t - C)
[PROOF STEP]
apply (rule continuous_at_Inf_mono)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. mono (\<lambda>s. 1 / lambda * s - C)
 2. continuous (at_right (Inf (dist w ` S))) (\<lambda>s. 1 / lambda * s - C)
 3. dist w ` S \<noteq> {}
 4. bdd_below (dist w ` S)
[PROOF STEP]
unfolding mono_def
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<forall>x y. x \<le> y \<longrightarrow> 1 / lambda * x - C \<le> 1 / lambda * y - C
 2. continuous (at_right (Inf (dist w ` S))) (\<lambda>s. 1 / lambda * s - C)
 3. dist w ` S \<noteq> {}
 4. bdd_below (dist w ` S)
[PROOF STEP]
using \<open>lambda \<ge> 1\<close> False
[PROOF STATE]
proof (prove)
using this:
1 \<le> lambda
S \<noteq> {}

goal (4 subgoals):
 1. \<forall>x y. x \<le> y \<longrightarrow> 1 / lambda * x - C \<le> 1 / lambda * y - C
 2. continuous (at_right (Inf (dist w ` S))) (\<lambda>s. 1 / lambda * s - C)
 3. dist w ` S \<noteq> {}
 4. bdd_below (dist w ` S)
[PROOF STEP]
by (auto simp add: divide_simps intro!: continuous_intros)
[PROOF STATE]
proof (state)
this:
1 / lambda * Inf (dist w ` S) - C = (INF t\<in>dist w ` S. 1 / lambda * t - C)

goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> 1 / lambda * infdist w S - C \<le> infdist (f w) (f ` S)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 / lambda * Inf (dist w ` S) - C = (INF t\<in>dist w ` S. 1 / lambda * t - C)

goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> 1 / lambda * infdist w S - C \<le> infdist (f w) (f ` S)
[PROOF STEP]
have "... = (INF x\<in>S. (1/lambda) * dist w x - C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (INF t\<in>dist w ` S. 1 / lambda * t - C) = (INF x\<in>S. 1 / lambda * dist w x - C)
[PROOF STEP]
by (auto simp add: image_comp)
[PROOF STATE]
proof (state)
this:
(INF t\<in>dist w ` S. 1 / lambda * t - C) = (INF x\<in>S. 1 / lambda * dist w x - C)

goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> 1 / lambda * infdist w S - C \<le> infdist (f w) (f ` S)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(INF t\<in>dist w ` S. 1 / lambda * t - C) = (INF x\<in>S. 1 / lambda * dist w x - C)

goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> 1 / lambda * infdist w S - C \<le> infdist (f w) (f ` S)
[PROOF STEP]
have "... \<le> (INF x\<in>S. dist (f w) (f x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (INF x\<in>S. 1 / lambda * dist w x - C) \<le> (INF x\<in>S. dist (f w) (f x))
[PROOF STEP]
apply (rule cINF_superset_mono[OF False])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. bdd_below ((\<lambda>x. 1 / lambda * dist w x - C) ` S)
 2. S \<subseteq> S
 3. \<And>x. x \<in> S \<Longrightarrow> 1 / lambda * dist w x - C \<le> dist (f w) (f x)
[PROOF STEP]
apply (rule bdd_belowI2[of _ "-C"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. x \<in> S \<Longrightarrow> - C \<le> 1 / lambda * dist w x - C
 2. S \<subseteq> S
 3. \<And>x. x \<in> S \<Longrightarrow> 1 / lambda * dist w x - C \<le> dist (f w) (f x)
[PROOF STEP]
using assms \<open>lambda \<ge> 1\<close>
[PROOF STATE]
proof (prove)
using this:
lambda C -quasi_isometry_on X f
w \<in> X
S \<subseteq> X
1 \<le> lambda

goal (3 subgoals):
 1. \<And>x. x \<in> S \<Longrightarrow> - C \<le> 1 / lambda * dist w x - C
 2. S \<subseteq> S
 3. \<And>x. x \<in> S \<Longrightarrow> 1 / lambda * dist w x - C \<le> dist (f w) (f x)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. S \<subseteq> S
 2. \<And>x. x \<in> S \<Longrightarrow> 1 / lambda * dist w x - C \<le> dist (f w) (f x)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> S \<Longrightarrow> 1 / lambda * dist w x - C \<le> dist (f w) (f x)
[PROOF STEP]
apply (rule quasi_isometry_onD(2)[OF assms(1)])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> S \<Longrightarrow> w \<in> X
 2. \<And>x. x \<in> S \<Longrightarrow> x \<in> X
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
lambda C -quasi_isometry_on X f
w \<in> X
S \<subseteq> X

goal (2 subgoals):
 1. \<And>x. x \<in> S \<Longrightarrow> w \<in> X
 2. \<And>x. x \<in> S \<Longrightarrow> x \<in> X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(INF x\<in>S. 1 / lambda * dist w x - C) \<le> (INF x\<in>S. dist (f w) (f x))

goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> 1 / lambda * infdist w S - C \<le> infdist (f w) (f ` S)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
1 / lambda * infdist w S - C \<le> (INF x\<in>S. dist (f w) (f x))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
1 / lambda * infdist w S - C \<le> (INF x\<in>S. dist (f w) (f x))

goal (1 subgoal):
 1. 1 / lambda * infdist w S - C \<le> infdist (f w) (f ` S)
[PROOF STEP]
unfolding infdist_def
[PROOF STATE]
proof (prove)
using this:
1 / lambda * (if S = {} then 0 else Inf (dist w ` S)) - C \<le> (INF x\<in>S. dist (f w) (f x))

goal (1 subgoal):
 1. 1 / lambda * (if S = {} then 0 else Inf (dist w ` S)) - C \<le> (if f ` S = {} then 0 else Inf (dist (f w) ` f ` S))
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
1 / lambda * (if S = {} then 0 else Inf (dist w ` S)) - C \<le> (INF x\<in>S. dist (f w) (f x))
S \<noteq> {}

goal (1 subgoal):
 1. 1 / lambda * (if S = {} then 0 else Inf (dist w ` S)) - C \<le> (if f ` S = {} then 0 else Inf (dist (f w) ` f ` S))
[PROOF STEP]
by (auto simp add: image_comp)
[PROOF STATE]
proof (state)
this:
1 / lambda * infdist w S - C \<le> infdist (f w) (f ` S)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
1 / lambda * infdist w S - C \<le> infdist (f w) (f ` S)

goal:
No subgoals!
[PROOF STEP]
qed