[STATEMENT]
lemma path_measure_eq_repcs''_new:
  notes in_space_UNIV[measurable]
  fixes cfg \<phi> \<psi> s
  defines "cfg' \<equiv> repcs s cfg"
  defines "\<phi>' \<equiv> absp \<phi>" and "\<psi>' \<equiv> absp \<psi>"
  assumes s: "abss s = state cfg"
  assumes valid: "cfg \<in> R_G.valid_cfg"
  assumes valid': "cfg' \<in> valid_cfg"
  assumes equiv_\<phi>: "\<And> x. pred_stream (\<lambda> s. s \<in> S) x
                    \<Longrightarrow> pred_stream (\<lambda> s. \<phi> (reps (abss s)) \<longleftrightarrow> \<phi> s) (state cfg' ## x)"
    and equiv_\<psi>: "\<And> x. pred_stream (\<lambda> s. s \<in> S) x
                    \<Longrightarrow> pred_stream (\<lambda> s. \<psi> (reps (abss s)) \<longleftrightarrow> \<psi> s) (state cfg' ## x)"
  shows
    "emeasure (R_G.T cfg)  {x\<in>space R_G.St. (holds \<phi>' suntil holds \<psi>') (state cfg  ## x)} =
     emeasure (MDP.T cfg') {x\<in>space MDP.St. (holds \<phi>  suntil holds \<psi>)  (state cfg' ## x)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure (R_G.T cfg) {x \<in> space R_G.St. (holds \<phi>' suntil holds \<psi>') (state cfg ## x)} = emeasure (MDP.T cfg') {x \<in> space MDP.St. (holds \<phi> suntil holds \<psi>) (state cfg' ## x)}
[PROOF STEP]
unfolding cfg'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure (R_G.T cfg) {x \<in> space R_G.St. (holds \<phi>' suntil holds \<psi>') (state cfg ## x)} = emeasure (MDP.T (repcs s cfg)) {x \<in> space MDP.St. (holds \<phi> suntil holds \<psi>) (state (repcs s cfg) ## x)}
[PROOF STEP]
apply (rule path_measure_eq_repcs1_new[where P = "pred_stream (\<lambda> s. s \<in> \<S>)" and Q = "pred_stream (\<lambda> s. s \<in> S)"])
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. abss s = state cfg
 2. cfg \<in> R_G.valid_cfg
 3. {x \<in> space R_G.St. (holds \<phi>' suntil holds \<psi>') (state cfg ## x)} \<in> sets R_G.St
 4. {x \<in> space MDP.St. (holds \<phi> suntil holds \<psi>) (state (repcs s cfg) ## x)} \<in> sets MDP.St
 5. almost_everywhere (R_G.T cfg) (pred_stream (\<lambda>s. s \<in> \<S>))
 6. almost_everywhere (MDP.T (repcs s cfg)) (pred_stream (\<lambda>s. s \<in> S))
 7. Measurable.pred R_G.St (pred_stream (\<lambda>s. s \<in> \<S>))
 8. Measurable.pred MDP.St (pred_stream (\<lambda>s. s \<in> S))
 9. \<And>x y. \<lbrakk>pred_stream (\<lambda>s. s \<in> \<S>) x; smap abss y = x; x \<in> {x \<in> space R_G.St. (holds \<phi>' suntil holds \<psi>') (state cfg ## x)}\<rbrakk> \<Longrightarrow> y \<in> {x \<in> space MDP.St. (holds \<phi> suntil holds \<psi>) (state (repcs s cfg) ## x)} \<and> pred_stream (\<lambda>s. s \<in> S) y
 10. \<And>x y. \<lbrakk>pred_stream (\<lambda>s. s \<in> S) y; smap abss y = x; y \<in> {x \<in> space MDP.St. (holds \<phi> suntil holds \<psi>) (state (repcs s cfg) ## x)}\<rbrakk> \<Longrightarrow> x \<in> {x \<in> space R_G.St. (holds \<phi>' suntil holds \<psi>') (state cfg ## x)} \<and> pred_stream (\<lambda>s. s \<in> \<S>) x
[PROOF STEP]
apply fact
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. cfg \<in> R_G.valid_cfg
 2. {x \<in> space R_G.St. (holds \<phi>' suntil holds \<psi>') (state cfg ## x)} \<in> sets R_G.St
 3. {x \<in> space MDP.St. (holds \<phi> suntil holds \<psi>) (state (repcs s cfg) ## x)} \<in> sets MDP.St
 4. almost_everywhere (R_G.T cfg) (pred_stream (\<lambda>s. s \<in> \<S>))
 5. almost_everywhere (MDP.T (repcs s cfg)) (pred_stream (\<lambda>s. s \<in> S))
 6. Measurable.pred R_G.St (pred_stream (\<lambda>s. s \<in> \<S>))
 7. Measurable.pred MDP.St (pred_stream (\<lambda>s. s \<in> S))
 8. \<And>x y. \<lbrakk>pred_stream (\<lambda>s. s \<in> \<S>) x; smap abss y = x; x \<in> {x \<in> space R_G.St. (holds \<phi>' suntil holds \<psi>') (state cfg ## x)}\<rbrakk> \<Longrightarrow> y \<in> {x \<in> space MDP.St. (holds \<phi> suntil holds \<psi>) (state (repcs s cfg) ## x)} \<and> pred_stream (\<lambda>s. s \<in> S) y
 9. \<And>x y. \<lbrakk>pred_stream (\<lambda>s. s \<in> S) y; smap abss y = x; y \<in> {x \<in> space MDP.St. (holds \<phi> suntil holds \<psi>) (state (repcs s cfg) ## x)}\<rbrakk> \<Longrightarrow> x \<in> {x \<in> space R_G.St. (holds \<phi>' suntil holds \<psi>') (state cfg ## x)} \<and> pred_stream (\<lambda>s. s \<in> \<S>) x
[PROOF STEP]
apply fact
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. {x \<in> space R_G.St. (holds \<phi>' suntil holds \<psi>') (state cfg ## x)} \<in> sets R_G.St
 2. {x \<in> space MDP.St. (holds \<phi> suntil holds \<psi>) (state (repcs s cfg) ## x)} \<in> sets MDP.St
 3. almost_everywhere (R_G.T cfg) (pred_stream (\<lambda>s. s \<in> \<S>))
 4. almost_everywhere (MDP.T (repcs s cfg)) (pred_stream (\<lambda>s. s \<in> S))
 5. Measurable.pred R_G.St (pred_stream (\<lambda>s. s \<in> \<S>))
 6. Measurable.pred MDP.St (pred_stream (\<lambda>s. s \<in> S))
 7. \<And>x y. \<lbrakk>pred_stream (\<lambda>s. s \<in> \<S>) x; smap abss y = x; x \<in> {x \<in> space R_G.St. (holds \<phi>' suntil holds \<psi>') (state cfg ## x)}\<rbrakk> \<Longrightarrow> y \<in> {x \<in> space MDP.St. (holds \<phi> suntil holds \<psi>) (state (repcs s cfg) ## x)} \<and> pred_stream (\<lambda>s. s \<in> S) y
 8. \<And>x y. \<lbrakk>pred_stream (\<lambda>s. s \<in> S) y; smap abss y = x; y \<in> {x \<in> space MDP.St. (holds \<phi> suntil holds \<psi>) (state (repcs s cfg) ## x)}\<rbrakk> \<Longrightarrow> x \<in> {x \<in> space R_G.St. (holds \<phi>' suntil holds \<psi>') (state cfg ## x)} \<and> pred_stream (\<lambda>s. s \<in> \<S>) x
[PROOF STEP]
apply measurable
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. almost_everywhere (R_G.T cfg) (pred_stream (\<lambda>s. s \<in> \<S>))
 2. almost_everywhere (MDP.T (repcs s cfg)) (pred_stream (\<lambda>s. s \<in> S))
 3. Measurable.pred R_G.St (pred_stream (\<lambda>s. s \<in> \<S>))
 4. Measurable.pred MDP.St (pred_stream (\<lambda>s. s \<in> S))
 5. \<And>x y. \<lbrakk>pred_stream (\<lambda>s. s \<in> \<S>) x; smap abss y = x; x \<in> {x \<in> space R_G.St. (holds \<phi>' suntil holds \<psi>') (state cfg ## x)}\<rbrakk> \<Longrightarrow> y \<in> {x \<in> space MDP.St. (holds \<phi> suntil holds \<psi>) (state (repcs s cfg) ## x)} \<and> pred_stream (\<lambda>s. s \<in> S) y
 6. \<And>x y. \<lbrakk>pred_stream (\<lambda>s. s \<in> S) y; smap abss y = x; y \<in> {x \<in> space MDP.St. (holds \<phi> suntil holds \<psi>) (state (repcs s cfg) ## x)}\<rbrakk> \<Longrightarrow> x \<in> {x \<in> space R_G.St. (holds \<phi>' suntil holds \<psi>') (state cfg ## x)} \<and> pred_stream (\<lambda>s. s \<in> \<S>) x
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. almost_everywhere (R_G.T cfg) (pred_stream (\<lambda>s. s \<in> \<S>))
[PROOF STEP]
unfolding R_G.T_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. almost_everywhere (distr (MDP.MC.T cfg) R_G.St (smap state)) (pred_stream (\<lambda>s. s \<in> \<S>))
[PROOF STEP]
apply (subst AE_distr_iff)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. MDP.MC.T.random_variable cfg R_G.St (smap state)
 2. {x \<in> space R_G.St. pred_stream (\<lambda>s. s \<in> \<S>) x} \<in> sets R_G.St
 3. AE x in MDP.MC.T cfg. pred_stream (\<lambda>s. s \<in> \<S>) (smap state x)
[PROOF STEP]
apply (auto; fail)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. {x \<in> space R_G.St. pred_stream (\<lambda>s. s \<in> \<S>) x} \<in> sets R_G.St
 2. AE x in MDP.MC.T cfg. pred_stream (\<lambda>s. s \<in> \<S>) (smap state x)
[PROOF STEP]
apply (auto simp: stream.pred_set; fail)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in MDP.MC.T cfg. pred_stream (\<lambda>s. s \<in> \<S>) (smap state x)
[PROOF STEP]
apply (rule AE_mp[OF MDP.MC.AE_T_enabled AE_I2])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> space (MDP.MC.T cfg) \<Longrightarrow> MDP.MC.enabled cfg x \<longrightarrow> pred_stream (\<lambda>s. s \<in> \<S>) (smap state x)
[PROOF STEP]
using R_G.pred_stream_cfg_on[OF valid]
[PROOF STATE]
proof (prove)
using this:
MDP.MC.enabled cfg ?xs \<Longrightarrow> pred_stream (\<lambda>cfg. state cfg \<in> \<S> \<and> cfg \<in> R_G.cfg_on (state cfg)) ?xs

goal (1 subgoal):
 1. \<And>x. x \<in> space (MDP.MC.T cfg) \<Longrightarrow> MDP.MC.enabled cfg x \<longrightarrow> pred_stream (\<lambda>s. s \<in> \<S>) (smap state x)
[PROOF STEP]
by (auto simp: stream.pred_set)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. almost_everywhere (MDP.T (repcs s cfg)) (pred_stream (\<lambda>s. s \<in> S))
 2. Measurable.pred R_G.St (pred_stream (\<lambda>s. s \<in> \<S>))
 3. Measurable.pred MDP.St (pred_stream (\<lambda>s. s \<in> S))
 4. \<And>x y. \<lbrakk>pred_stream (\<lambda>s. s \<in> \<S>) x; smap abss y = x; x \<in> {x \<in> space R_G.St. (holds \<phi>' suntil holds \<psi>') (state cfg ## x)}\<rbrakk> \<Longrightarrow> y \<in> {x \<in> space MDP.St. (holds \<phi> suntil holds \<psi>) (state (repcs s cfg) ## x)} \<and> pred_stream (\<lambda>s. s \<in> S) y
 5. \<And>x y. \<lbrakk>pred_stream (\<lambda>s. s \<in> S) y; smap abss y = x; y \<in> {x \<in> space MDP.St. (holds \<phi> suntil holds \<psi>) (state (repcs s cfg) ## x)}\<rbrakk> \<Longrightarrow> x \<in> {x \<in> space R_G.St. (holds \<phi>' suntil holds \<psi>') (state cfg ## x)} \<and> pred_stream (\<lambda>s. s \<in> \<S>) x
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. almost_everywhere (MDP.T (repcs s cfg)) (pred_stream (\<lambda>s. s \<in> S))
[PROOF STEP]
unfolding MDP.T_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. almost_everywhere (distr (MDP.MC.T (repcs s cfg)) MDP.St (smap state)) (pred_stream (\<lambda>s. s \<in> S))
[PROOF STEP]
apply (subst AE_distr_iff)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. MDP.MC.T.random_variable (repcs s cfg) MDP.St (smap state)
 2. {x \<in> space MDP.St. pred_stream (\<lambda>s. s \<in> S) x} \<in> sets MDP.St
 3. AE x in MDP.MC.T (repcs s cfg). pred_stream (\<lambda>s. s \<in> S) (smap state x)
[PROOF STEP]
apply (auto; fail)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. {x \<in> space MDP.St. pred_stream (\<lambda>s. s \<in> S) x} \<in> sets MDP.St
 2. AE x in MDP.MC.T (repcs s cfg). pred_stream (\<lambda>s. s \<in> S) (smap state x)
[PROOF STEP]
apply (auto simp: stream.pred_set; fail)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in MDP.MC.T (repcs s cfg). pred_stream (\<lambda>s. s \<in> S) (smap state x)
[PROOF STEP]
apply (rule AE_mp[OF MDP.MC.AE_T_enabled AE_I2])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> space (MDP.MC.T (repcs s cfg)) \<Longrightarrow> MDP.MC.enabled (repcs s cfg) x \<longrightarrow> pred_stream (\<lambda>s. s \<in> S) (smap state x)
[PROOF STEP]
using MDP.pred_stream_cfg_on[OF valid', unfolded cfg'_def]
[PROOF STATE]
proof (prove)
using this:
MDP.MC.enabled (repcs s cfg) ?xs \<Longrightarrow> pred_stream (\<lambda>cfg. state cfg \<in> S \<and> cfg \<in> MDP.cfg_on (state cfg)) ?xs

goal (1 subgoal):
 1. \<And>x. x \<in> space (MDP.MC.T (repcs s cfg)) \<Longrightarrow> MDP.MC.enabled (repcs s cfg) x \<longrightarrow> pred_stream (\<lambda>s. s \<in> S) (smap state x)
[PROOF STEP]
by (auto simp: stream.pred_set)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. Measurable.pred R_G.St (pred_stream (\<lambda>s. s \<in> \<S>))
 2. Measurable.pred MDP.St (pred_stream (\<lambda>s. s \<in> S))
 3. \<And>x y. \<lbrakk>pred_stream (\<lambda>s. s \<in> \<S>) x; smap abss y = x; x \<in> {x \<in> space R_G.St. (holds \<phi>' suntil holds \<psi>') (state cfg ## x)}\<rbrakk> \<Longrightarrow> y \<in> {x \<in> space MDP.St. (holds \<phi> suntil holds \<psi>) (state (repcs s cfg) ## x)} \<and> pred_stream (\<lambda>s. s \<in> S) y
 4. \<And>x y. \<lbrakk>pred_stream (\<lambda>s. s \<in> S) y; smap abss y = x; y \<in> {x \<in> space MDP.St. (holds \<phi> suntil holds \<psi>) (state (repcs s cfg) ## x)}\<rbrakk> \<Longrightarrow> x \<in> {x \<in> space R_G.St. (holds \<phi>' suntil holds \<psi>') (state cfg ## x)} \<and> pred_stream (\<lambda>s. s \<in> \<S>) x
[PROOF STEP]
apply measurable
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>pred_stream (\<lambda>s. s \<in> \<S>) x; smap abss y = x; x \<in> {x \<in> space R_G.St. (holds \<phi>' suntil holds \<psi>') (state cfg ## x)}\<rbrakk> \<Longrightarrow> y \<in> {x \<in> space MDP.St. (holds \<phi> suntil holds \<psi>) (state (repcs s cfg) ## x)} \<and> pred_stream (\<lambda>s. s \<in> S) y
 2. \<And>x y. \<lbrakk>pred_stream (\<lambda>s. s \<in> S) y; smap abss y = x; y \<in> {x \<in> space MDP.St. (holds \<phi> suntil holds \<psi>) (state (repcs s cfg) ## x)}\<rbrakk> \<Longrightarrow> x \<in> {x \<in> space R_G.St. (holds \<phi>' suntil holds \<psi>') (state cfg ## x)} \<and> pred_stream (\<lambda>s. s \<in> \<S>) x
[PROOF STEP]
subgoal premises prems for ys xs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<in> {x \<in> space MDP.St. (holds \<phi> suntil holds \<psi>) (state (repcs s cfg) ## x)} \<and> pred_stream (\<lambda>s. s \<in> S) xs
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. xs \<in> space MDP.St
 2. (holds \<phi> suntil holds \<psi>) (state (repcs s cfg) ## xs)
 3. pred_stream (\<lambda>s. s \<in> S) xs
[PROOF STEP]
apply measurable
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (holds \<phi> suntil holds \<psi>) (state (repcs s cfg) ## xs)
 2. pred_stream (\<lambda>s. s \<in> S) xs
[PROOF STEP]
unfolding \<phi>'_def \<psi>'_def absp_def
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (holds \<phi> suntil holds \<psi>) (state (repcs s cfg) ## xs)
 2. pred_stream (\<lambda>s. s \<in> S) xs
[PROOF STEP]
apply (subst region_compatible_suntil[symmetric])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. pred_stream (\<lambda>s. \<phi> (reps (abss s)) = \<phi> s) (state (repcs s cfg) ## xs)
 2. pred_stream (\<lambda>s. \<psi> (reps (abss s)) = \<psi> s) (state (repcs s cfg) ## xs)
 3. (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (smap abss (state (repcs s cfg) ## xs))
 4. pred_stream (\<lambda>s. s \<in> S) xs
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pred_stream (\<lambda>s. \<phi> (reps (abss s)) = \<phi> s) (state (repcs s cfg) ## xs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pred_stream (\<lambda>s. \<phi> (reps (abss s)) = \<phi> s) (state (repcs s cfg) ## xs)
[PROOF STEP]
from prems
[PROOF STATE]
proof (chain)
picking this:
pred_stream (\<lambda>s. s \<in> \<S>) ys
smap abss xs = ys
ys \<in> {x \<in> space R_G.St. (holds \<phi>' suntil holds \<psi>') (state cfg ## x)}
[PROOF STEP]
have "pred_stream (\<lambda>s. s \<in> S) xs"
[PROOF STATE]
proof (prove)
using this:
pred_stream (\<lambda>s. s \<in> \<S>) ys
smap abss xs = ys
ys \<in> {x \<in> space R_G.St. (holds \<phi>' suntil holds \<psi>') (state cfg ## x)}

goal (1 subgoal):
 1. pred_stream (\<lambda>s. s \<in> S) xs
[PROOF STEP]
using \<S>_abss_S
[PROOF STATE]
proof (prove)
using this:
pred_stream (\<lambda>s. s \<in> \<S>) ys
smap abss xs = ys
ys \<in> {x \<in> space R_G.St. (holds \<phi>' suntil holds \<psi>') (state cfg ## x)}
abss ?s \<in> \<S> \<Longrightarrow> ?s \<in> S

goal (1 subgoal):
 1. pred_stream (\<lambda>s. s \<in> S) xs
[PROOF STEP]
by (auto simp: stream.pred_set)
[PROOF STATE]
proof (state)
this:
pred_stream (\<lambda>s. s \<in> S) xs

goal (1 subgoal):
 1. pred_stream (\<lambda>s. \<phi> (reps (abss s)) = \<phi> s) (state (repcs s cfg) ## xs)
[PROOF STEP]
with equiv_\<phi>
[PROOF STATE]
proof (chain)
picking this:
pred_stream (\<lambda>s. s \<in> S) ?x5 \<Longrightarrow> pred_stream (\<lambda>s. \<phi> (reps (abss s)) = \<phi> s) (state cfg' ## ?x5)
pred_stream (\<lambda>s. s \<in> S) xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pred_stream (\<lambda>s. s \<in> S) ?x5 \<Longrightarrow> pred_stream (\<lambda>s. \<phi> (reps (abss s)) = \<phi> s) (state cfg' ## ?x5)
pred_stream (\<lambda>s. s \<in> S) xs

goal (1 subgoal):
 1. pred_stream (\<lambda>s. \<phi> (reps (abss s)) = \<phi> s) (state (repcs s cfg) ## xs)
[PROOF STEP]
by (simp add: cfg'_def)
[PROOF STATE]
proof (state)
this:
pred_stream (\<lambda>s. \<phi> (reps (abss s)) = \<phi> s) (state (repcs s cfg) ## xs)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. pred_stream (\<lambda>s. \<psi> (reps (abss s)) = \<psi> s) (state (repcs s cfg) ## xs)
 2. (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (smap abss (state (repcs s cfg) ## xs))
 3. pred_stream (\<lambda>s. s \<in> S) xs
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pred_stream (\<lambda>s. \<psi> (reps (abss s)) = \<psi> s) (state (repcs s cfg) ## xs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pred_stream (\<lambda>s. \<psi> (reps (abss s)) = \<psi> s) (state (repcs s cfg) ## xs)
[PROOF STEP]
from prems
[PROOF STATE]
proof (chain)
picking this:
pred_stream (\<lambda>s. s \<in> \<S>) ys
smap abss xs = ys
ys \<in> {x \<in> space R_G.St. (holds \<phi>' suntil holds \<psi>') (state cfg ## x)}
[PROOF STEP]
have "pred_stream (\<lambda>s. s \<in> S) xs"
[PROOF STATE]
proof (prove)
using this:
pred_stream (\<lambda>s. s \<in> \<S>) ys
smap abss xs = ys
ys \<in> {x \<in> space R_G.St. (holds \<phi>' suntil holds \<psi>') (state cfg ## x)}

goal (1 subgoal):
 1. pred_stream (\<lambda>s. s \<in> S) xs
[PROOF STEP]
using \<S>_abss_S
[PROOF STATE]
proof (prove)
using this:
pred_stream (\<lambda>s. s \<in> \<S>) ys
smap abss xs = ys
ys \<in> {x \<in> space R_G.St. (holds \<phi>' suntil holds \<psi>') (state cfg ## x)}
abss ?s \<in> \<S> \<Longrightarrow> ?s \<in> S

goal (1 subgoal):
 1. pred_stream (\<lambda>s. s \<in> S) xs
[PROOF STEP]
by (auto simp: stream.pred_set)
[PROOF STATE]
proof (state)
this:
pred_stream (\<lambda>s. s \<in> S) xs

goal (1 subgoal):
 1. pred_stream (\<lambda>s. \<psi> (reps (abss s)) = \<psi> s) (state (repcs s cfg) ## xs)
[PROOF STEP]
with equiv_\<psi>
[PROOF STATE]
proof (chain)
picking this:
pred_stream (\<lambda>s. s \<in> S) ?x5 \<Longrightarrow> pred_stream (\<lambda>s. \<psi> (reps (abss s)) = \<psi> s) (state cfg' ## ?x5)
pred_stream (\<lambda>s. s \<in> S) xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pred_stream (\<lambda>s. s \<in> S) ?x5 \<Longrightarrow> pred_stream (\<lambda>s. \<psi> (reps (abss s)) = \<psi> s) (state cfg' ## ?x5)
pred_stream (\<lambda>s. s \<in> S) xs

goal (1 subgoal):
 1. pred_stream (\<lambda>s. \<psi> (reps (abss s)) = \<psi> s) (state (repcs s cfg) ## xs)
[PROOF STEP]
by (simp add: cfg'_def)
[PROOF STATE]
proof (state)
this:
pred_stream (\<lambda>s. \<psi> (reps (abss s)) = \<psi> s) (state (repcs s cfg) ## xs)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (smap abss (state (repcs s cfg) ## xs))
 2. pred_stream (\<lambda>s. s \<in> S) xs
[PROOF STEP]
using valid prems
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
pred_stream (\<lambda>s. s \<in> \<S>) ys
smap abss xs = ys
ys \<in> {x \<in> space R_G.St. (holds \<phi>' suntil holds \<psi>') (state cfg ## x)}

goal (2 subgoals):
 1. (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (smap abss (state (repcs s cfg) ## xs))
 2. pred_stream (\<lambda>s. s \<in> S) xs
[PROOF STEP]
apply (auto simp: s comp_def \<phi>'_def \<psi>'_def absp_def dest: R_G.valid_cfg_state_in_S)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cfg \<in> R_G.valid_cfg; ys = smap abss xs; pred_stream (\<lambda>x. abss x \<in> \<S>) xs; smap abss xs \<in> space R_G.St; (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (state cfg ## smap abss xs)\<rbrakk> \<Longrightarrow> pred_stream (\<lambda>s. s \<in> S) xs
[PROOF STEP]
apply (auto simp: stream.pred_set intro: \<S>_abss_S dest: R_G.valid_cfg_state_in_S)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>pred_stream (\<lambda>s. s \<in> S) y; smap abss y = x; y \<in> {x \<in> space MDP.St. (holds \<phi> suntil holds \<psi>) (state (repcs s cfg) ## x)}\<rbrakk> \<Longrightarrow> x \<in> {x \<in> space R_G.St. (holds \<phi>' suntil holds \<psi>') (state cfg ## x)} \<and> pred_stream (\<lambda>s. s \<in> \<S>) x
[PROOF STEP]
subgoal premises prems for ys xs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ys \<in> {x \<in> space R_G.St. (holds \<phi>' suntil holds \<psi>') (state cfg ## x)} \<and> pred_stream (\<lambda>s. s \<in> \<S>) ys
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. ys \<in> space R_G.St
 2. (holds \<phi>' suntil holds \<psi>') (state cfg ## ys)
 3. pred_stream (\<lambda>s. s \<in> \<S>) ys
[PROOF STEP]
using prems
[PROOF STATE]
proof (prove)
using this:
pred_stream (\<lambda>s. s \<in> S) xs
smap abss xs = ys
xs \<in> {x \<in> space MDP.St. (holds \<phi> suntil holds \<psi>) (state (repcs s cfg) ## x)}

goal (3 subgoals):
 1. ys \<in> space R_G.St
 2. (holds \<phi>' suntil holds \<psi>') (state cfg ## ys)
 3. pred_stream (\<lambda>s. s \<in> \<S>) ys
[PROOF STEP]
apply (auto simp: stream.pred_set \<S>_abss_S; measurable; fail)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (holds \<phi>' suntil holds \<psi>') (state cfg ## ys)
 2. pred_stream (\<lambda>s. s \<in> \<S>) ys
[PROOF STEP]
using prems
[PROOF STATE]
proof (prove)
using this:
pred_stream (\<lambda>s. s \<in> S) xs
smap abss xs = ys
xs \<in> {x \<in> space MDP.St. (holds \<phi> suntil holds \<psi>) (state (repcs s cfg) ## x)}

goal (2 subgoals):
 1. (holds \<phi>' suntil holds \<psi>') (state cfg ## ys)
 2. pred_stream (\<lambda>s. s \<in> \<S>) ys
[PROOF STEP]
unfolding \<phi>'_def \<psi>'_def absp_def comp_def
[PROOF STATE]
proof (prove)
using this:
pred_stream (\<lambda>s. s \<in> S) xs
smap abss xs = ys
xs \<in> {x \<in> space MDP.St. (holds \<phi> suntil holds \<psi>) (state (repcs s cfg) ## x)}

goal (2 subgoals):
 1. (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (state cfg ## ys)
 2. pred_stream (\<lambda>s. s \<in> \<S>) ys
[PROOF STEP]
apply (simp add: stream.map_comp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pred_stream (\<lambda>s. s \<in> S) xs; smap abss xs = ys; xs \<in> space MDP.St \<and> (holds \<phi> suntil holds \<psi>) (s ## xs)\<rbrakk> \<Longrightarrow> (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (state cfg ## ys)
 2. pred_stream (\<lambda>s. s \<in> \<S>) ys
[PROOF STEP]
apply (subst (asm) region_compatible_suntil[symmetric])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>pred_stream (\<lambda>s. s \<in> S) xs; smap abss xs = ys\<rbrakk> \<Longrightarrow> pred_stream (\<lambda>s. \<phi> (reps (abss s)) = \<phi> s) (s ## xs)
 2. \<lbrakk>pred_stream (\<lambda>s. s \<in> S) xs; smap abss xs = ys\<rbrakk> \<Longrightarrow> pred_stream (\<lambda>s. \<psi> (reps (abss s)) = \<psi> s) (s ## xs)
 3. \<lbrakk>pred_stream (\<lambda>s. s \<in> S) xs; smap abss xs = ys; xs \<in> space MDP.St \<and> (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (smap abss (s ## xs))\<rbrakk> \<Longrightarrow> (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (state cfg ## ys)
 4. pred_stream (\<lambda>s. s \<in> \<S>) ys
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pred_stream (\<lambda>s. s \<in> S) xs; smap abss xs = ys\<rbrakk> \<Longrightarrow> pred_stream (\<lambda>s. \<phi> (reps (abss s)) = \<phi> s) (s ## xs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>pred_stream (\<lambda>s. s \<in> S) xs; smap abss xs = ys\<rbrakk> \<Longrightarrow> pred_stream (\<lambda>s. \<phi> (reps (abss s)) = \<phi> s) (s ## xs)
[PROOF STEP]
from prems
[PROOF STATE]
proof (chain)
picking this:
pred_stream (\<lambda>s. s \<in> S) xs
smap abss xs = ys
xs \<in> {x \<in> space MDP.St. (holds \<phi> suntil holds \<psi>) (state (repcs s cfg) ## x)}
[PROOF STEP]
have "pred_stream (\<lambda>s. s \<in> S) xs"
[PROOF STATE]
proof (prove)
using this:
pred_stream (\<lambda>s. s \<in> S) xs
smap abss xs = ys
xs \<in> {x \<in> space MDP.St. (holds \<phi> suntil holds \<psi>) (state (repcs s cfg) ## x)}

goal (1 subgoal):
 1. pred_stream (\<lambda>s. s \<in> S) xs
[PROOF STEP]
using \<S>_abss_S
[PROOF STATE]
proof (prove)
using this:
pred_stream (\<lambda>s. s \<in> S) xs
smap abss xs = ys
xs \<in> {x \<in> space MDP.St. (holds \<phi> suntil holds \<psi>) (state (repcs s cfg) ## x)}
abss ?s \<in> \<S> \<Longrightarrow> ?s \<in> S

goal (1 subgoal):
 1. pred_stream (\<lambda>s. s \<in> S) xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pred_stream (\<lambda>s. s \<in> S) xs

goal (1 subgoal):
 1. \<lbrakk>pred_stream (\<lambda>s. s \<in> S) xs; smap abss xs = ys\<rbrakk> \<Longrightarrow> pred_stream (\<lambda>s. \<phi> (reps (abss s)) = \<phi> s) (s ## xs)
[PROOF STEP]
with equiv_\<phi>
[PROOF STATE]
proof (chain)
picking this:
pred_stream (\<lambda>s. s \<in> S) ?x5 \<Longrightarrow> pred_stream (\<lambda>s. \<phi> (reps (abss s)) = \<phi> s) (state cfg' ## ?x5)
pred_stream (\<lambda>s. s \<in> S) xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pred_stream (\<lambda>s. s \<in> S) ?x5 \<Longrightarrow> pred_stream (\<lambda>s. \<phi> (reps (abss s)) = \<phi> s) (state cfg' ## ?x5)
pred_stream (\<lambda>s. s \<in> S) xs

goal (1 subgoal):
 1. pred_stream (\<lambda>s. \<phi> (reps (abss s)) = \<phi> s) (s ## xs)
[PROOF STEP]
using valid
[PROOF STATE]
proof (prove)
using this:
pred_stream (\<lambda>s. s \<in> S) ?x5 \<Longrightarrow> pred_stream (\<lambda>s. \<phi> (reps (abss s)) = \<phi> s) (state cfg' ## ?x5)
pred_stream (\<lambda>s. s \<in> S) xs
cfg \<in> R_G.valid_cfg

goal (1 subgoal):
 1. pred_stream (\<lambda>s. \<phi> (reps (abss s)) = \<phi> s) (s ## xs)
[PROOF STEP]
by (simp add: cfg'_def repc_def)
[PROOF STATE]
proof (state)
this:
pred_stream (\<lambda>s. \<phi> (reps (abss s)) = \<phi> s) (s ## xs)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>pred_stream (\<lambda>s. s \<in> S) xs; smap abss xs = ys\<rbrakk> \<Longrightarrow> pred_stream (\<lambda>s. \<psi> (reps (abss s)) = \<psi> s) (s ## xs)
 2. \<lbrakk>pred_stream (\<lambda>s. s \<in> S) xs; smap abss xs = ys; xs \<in> space MDP.St \<and> (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (smap abss (s ## xs))\<rbrakk> \<Longrightarrow> (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (state cfg ## ys)
 3. pred_stream (\<lambda>s. s \<in> \<S>) ys
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pred_stream (\<lambda>s. s \<in> S) xs; smap abss xs = ys\<rbrakk> \<Longrightarrow> pred_stream (\<lambda>s. \<psi> (reps (abss s)) = \<psi> s) (s ## xs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>pred_stream (\<lambda>s. s \<in> S) xs; smap abss xs = ys\<rbrakk> \<Longrightarrow> pred_stream (\<lambda>s. \<psi> (reps (abss s)) = \<psi> s) (s ## xs)
[PROOF STEP]
from prems
[PROOF STATE]
proof (chain)
picking this:
pred_stream (\<lambda>s. s \<in> S) xs
smap abss xs = ys
xs \<in> {x \<in> space MDP.St. (holds \<phi> suntil holds \<psi>) (state (repcs s cfg) ## x)}
[PROOF STEP]
have "pred_stream (\<lambda>s. s \<in> S) xs"
[PROOF STATE]
proof (prove)
using this:
pred_stream (\<lambda>s. s \<in> S) xs
smap abss xs = ys
xs \<in> {x \<in> space MDP.St. (holds \<phi> suntil holds \<psi>) (state (repcs s cfg) ## x)}

goal (1 subgoal):
 1. pred_stream (\<lambda>s. s \<in> S) xs
[PROOF STEP]
using \<S>_abss_S
[PROOF STATE]
proof (prove)
using this:
pred_stream (\<lambda>s. s \<in> S) xs
smap abss xs = ys
xs \<in> {x \<in> space MDP.St. (holds \<phi> suntil holds \<psi>) (state (repcs s cfg) ## x)}
abss ?s \<in> \<S> \<Longrightarrow> ?s \<in> S

goal (1 subgoal):
 1. pred_stream (\<lambda>s. s \<in> S) xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pred_stream (\<lambda>s. s \<in> S) xs

goal (1 subgoal):
 1. \<lbrakk>pred_stream (\<lambda>s. s \<in> S) xs; smap abss xs = ys\<rbrakk> \<Longrightarrow> pred_stream (\<lambda>s. \<psi> (reps (abss s)) = \<psi> s) (s ## xs)
[PROOF STEP]
with equiv_\<psi>
[PROOF STATE]
proof (chain)
picking this:
pred_stream (\<lambda>s. s \<in> S) ?x5 \<Longrightarrow> pred_stream (\<lambda>s. \<psi> (reps (abss s)) = \<psi> s) (state cfg' ## ?x5)
pred_stream (\<lambda>s. s \<in> S) xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pred_stream (\<lambda>s. s \<in> S) ?x5 \<Longrightarrow> pred_stream (\<lambda>s. \<psi> (reps (abss s)) = \<psi> s) (state cfg' ## ?x5)
pred_stream (\<lambda>s. s \<in> S) xs

goal (1 subgoal):
 1. pred_stream (\<lambda>s. \<psi> (reps (abss s)) = \<psi> s) (s ## xs)
[PROOF STEP]
using valid
[PROOF STATE]
proof (prove)
using this:
pred_stream (\<lambda>s. s \<in> S) ?x5 \<Longrightarrow> pred_stream (\<lambda>s. \<psi> (reps (abss s)) = \<psi> s) (state cfg' ## ?x5)
pred_stream (\<lambda>s. s \<in> S) xs
cfg \<in> R_G.valid_cfg

goal (1 subgoal):
 1. pred_stream (\<lambda>s. \<psi> (reps (abss s)) = \<psi> s) (s ## xs)
[PROOF STEP]
by (simp add: cfg'_def)
[PROOF STATE]
proof (state)
this:
pred_stream (\<lambda>s. \<psi> (reps (abss s)) = \<psi> s) (s ## xs)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pred_stream (\<lambda>s. s \<in> S) xs; smap abss xs = ys; xs \<in> space MDP.St \<and> (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (smap abss (s ## xs))\<rbrakk> \<Longrightarrow> (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (state cfg ## ys)
 2. pred_stream (\<lambda>s. s \<in> \<S>) ys
[PROOF STEP]
using valid prems
[PROOF STATE]
proof (prove)
using this:
cfg \<in> R_G.valid_cfg
pred_stream (\<lambda>s. s \<in> S) xs
smap abss xs = ys
xs \<in> {x \<in> space MDP.St. (holds \<phi> suntil holds \<psi>) (state (repcs s cfg) ## x)}

goal (2 subgoals):
 1. \<lbrakk>pred_stream (\<lambda>s. s \<in> S) xs; smap abss xs = ys; xs \<in> space MDP.St \<and> (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (smap abss (s ## xs))\<rbrakk> \<Longrightarrow> (holds (\<lambda>x. \<phi> (reps x)) suntil holds (\<lambda>x. \<psi> (reps x))) (state cfg ## ys)
 2. pred_stream (\<lambda>s. s \<in> \<S>) ys
[PROOF STEP]
by (auto simp: s S_abss_\<S> stream.pred_set dest: R_G.valid_cfg_state_in_S)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma distance_cross_ratio_real_positive:
  assumes "u \<in> unit_disc" and "v \<in> unit_disc" and "u \<noteq> v"
  shows "\<forall> i1 i2. ideal_points (poincare_line u v) = {i1, i2} \<longrightarrow>
                  cross_ratio u i1 v i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio u i1 v i2)) \<and> Re_cross_ratio u i1 v i2 > 0" (is "?P u v")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i1 i2. ideal_points (poincare_line u v) = {i1, i2} \<longrightarrow> cross_ratio u i1 v i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio u i1 v i2)) \<and> 0 < Re_cross_ratio u i1 v i2
[PROOF STEP]
proof (rule wlog_positive_x_axis[OF assms])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>i1 i2. ideal_points (poincare_line (moebius_pt M u) (moebius_pt M v)) = {i1, i2} \<longrightarrow> cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2)) \<and> 0 < Re_cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2\<rbrakk> \<Longrightarrow> \<forall>i1 i2. ideal_points (poincare_line u v) = {i1, i2} \<longrightarrow> cross_ratio u i1 v i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio u i1 v i2)) \<and> 0 < Re_cross_ratio u i1 v i2
 2. \<And>x. \<lbrakk>is_real x; 0 < Re x; Re x < 1\<rbrakk> \<Longrightarrow> \<forall>i1 i2. ideal_points (poincare_line 0\<^sub>h (of_complex x)) = {i1, i2} \<longrightarrow> cross_ratio 0\<^sub>h i1 (of_complex x) i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio 0\<^sub>h i1 (of_complex x) i2)) \<and> 0 < Re_cross_ratio 0\<^sub>h i1 (of_complex x) i2
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>i1 i2. ideal_points (poincare_line (moebius_pt M u) (moebius_pt M v)) = {i1, i2} \<longrightarrow> cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2)) \<and> 0 < Re_cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2\<rbrakk> \<Longrightarrow> \<forall>i1 i2. ideal_points (poincare_line u v) = {i1, i2} \<longrightarrow> cross_ratio u i1 v i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio u i1 v i2)) \<and> 0 < Re_cross_ratio u i1 v i2
 2. \<And>x. \<lbrakk>is_real x; 0 < Re x; Re x < 1\<rbrakk> \<Longrightarrow> \<forall>i1 i2. ideal_points (poincare_line 0\<^sub>h (of_complex x)) = {i1, i2} \<longrightarrow> cross_ratio 0\<^sub>h i1 (of_complex x) i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio 0\<^sub>h i1 (of_complex x) i2)) \<and> 0 < Re_cross_ratio 0\<^sub>h i1 (of_complex x) i2
[PROOF STEP]
assume *: "is_real x" "0 < Re x" "Re x < 1"
[PROOF STATE]
proof (state)
this:
is_real x
0 < Re x
Re x < 1

goal (2 subgoals):
 1. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>i1 i2. ideal_points (poincare_line (moebius_pt M u) (moebius_pt M v)) = {i1, i2} \<longrightarrow> cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2)) \<and> 0 < Re_cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2\<rbrakk> \<Longrightarrow> \<forall>i1 i2. ideal_points (poincare_line u v) = {i1, i2} \<longrightarrow> cross_ratio u i1 v i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio u i1 v i2)) \<and> 0 < Re_cross_ratio u i1 v i2
 2. \<And>x. \<lbrakk>is_real x; 0 < Re x; Re x < 1\<rbrakk> \<Longrightarrow> \<forall>i1 i2. ideal_points (poincare_line 0\<^sub>h (of_complex x)) = {i1, i2} \<longrightarrow> cross_ratio 0\<^sub>h i1 (of_complex x) i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio 0\<^sub>h i1 (of_complex x) i2)) \<and> 0 < Re_cross_ratio 0\<^sub>h i1 (of_complex x) i2
[PROOF STEP]
hence "x \<noteq> -1" "x \<noteq> 1"
[PROOF STATE]
proof (prove)
using this:
is_real x
0 < Re x
Re x < 1

goal (1 subgoal):
 1. x \<noteq> - 1 &&& x \<noteq> 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<noteq> - 1
x \<noteq> 1

goal (2 subgoals):
 1. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>i1 i2. ideal_points (poincare_line (moebius_pt M u) (moebius_pt M v)) = {i1, i2} \<longrightarrow> cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2)) \<and> 0 < Re_cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2\<rbrakk> \<Longrightarrow> \<forall>i1 i2. ideal_points (poincare_line u v) = {i1, i2} \<longrightarrow> cross_ratio u i1 v i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio u i1 v i2)) \<and> 0 < Re_cross_ratio u i1 v i2
 2. \<And>x. \<lbrakk>is_real x; 0 < Re x; Re x < 1\<rbrakk> \<Longrightarrow> \<forall>i1 i2. ideal_points (poincare_line 0\<^sub>h (of_complex x)) = {i1, i2} \<longrightarrow> cross_ratio 0\<^sub>h i1 (of_complex x) i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio 0\<^sub>h i1 (of_complex x) i2)) \<and> 0 < Re_cross_ratio 0\<^sub>h i1 (of_complex x) i2
[PROOF STEP]
hence **: "of_complex x \<noteq> \<infinity>\<^sub>h" "of_complex x \<noteq> 0\<^sub>h" "of_complex x \<noteq> of_complex (-1)" "of_complex 1 \<noteq> of_complex x"
        "of_complex x \<in> circline_set x_axis"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> - 1
x \<noteq> 1

goal (1 subgoal):
 1. (of_complex x \<noteq> \<infinity>\<^sub>h &&& of_complex x \<noteq> 0\<^sub>h) &&& of_complex x \<noteq> of_complex (- 1) &&& of_complex 1 \<noteq> of_complex x &&& of_complex x \<in> circline_set x_axis
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
x \<noteq> - 1
x \<noteq> 1
is_real x
0 < Re x
Re x < 1

goal (1 subgoal):
 1. (of_complex x \<noteq> \<infinity>\<^sub>h &&& of_complex x \<noteq> 0\<^sub>h) &&& of_complex x \<noteq> of_complex (- 1) &&& of_complex 1 \<noteq> of_complex x &&& of_complex x \<in> circline_set x_axis
[PROOF STEP]
unfolding circline_set_x_axis
[PROOF STATE]
proof (prove)
using this:
x \<noteq> - 1
x \<noteq> 1
is_real x
0 < Re x
Re x < 1

goal (1 subgoal):
 1. (of_complex x \<noteq> \<infinity>\<^sub>h &&& of_complex x \<noteq> 0\<^sub>h) &&& of_complex x \<noteq> of_complex (- 1) &&& of_complex 1 \<noteq> of_complex x &&& of_complex x \<in> of_complex ` {x. is_real x} \<union> {\<infinity>\<^sub>h}
[PROOF STEP]
by (auto simp add: of_complex_inj)
[PROOF STATE]
proof (state)
this:
of_complex x \<noteq> \<infinity>\<^sub>h
of_complex x \<noteq> 0\<^sub>h
of_complex x \<noteq> of_complex (- 1)
of_complex 1 \<noteq> of_complex x
of_complex x \<in> circline_set x_axis

goal (2 subgoals):
 1. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>i1 i2. ideal_points (poincare_line (moebius_pt M u) (moebius_pt M v)) = {i1, i2} \<longrightarrow> cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2)) \<and> 0 < Re_cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2\<rbrakk> \<Longrightarrow> \<forall>i1 i2. ideal_points (poincare_line u v) = {i1, i2} \<longrightarrow> cross_ratio u i1 v i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio u i1 v i2)) \<and> 0 < Re_cross_ratio u i1 v i2
 2. \<And>x. \<lbrakk>is_real x; 0 < Re x; Re x < 1\<rbrakk> \<Longrightarrow> \<forall>i1 i2. ideal_points (poincare_line 0\<^sub>h (of_complex x)) = {i1, i2} \<longrightarrow> cross_ratio 0\<^sub>h i1 (of_complex x) i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio 0\<^sub>h i1 (of_complex x) i2)) \<and> 0 < Re_cross_ratio 0\<^sub>h i1 (of_complex x) i2
[PROOF STEP]
have ***:  "0\<^sub>h \<noteq> of_complex (-1)" "0\<^sub>h \<noteq> of_complex 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0\<^sub>h \<noteq> of_complex (- 1) &&& 0\<^sub>h \<noteq> of_complex 1
[PROOF STEP]
by (metis of_complex_zero_iff zero_neq_neg_one, simp)
[PROOF STATE]
proof (state)
this:
0\<^sub>h \<noteq> of_complex (- 1)
0\<^sub>h \<noteq> of_complex 1

goal (2 subgoals):
 1. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>i1 i2. ideal_points (poincare_line (moebius_pt M u) (moebius_pt M v)) = {i1, i2} \<longrightarrow> cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2)) \<and> 0 < Re_cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2\<rbrakk> \<Longrightarrow> \<forall>i1 i2. ideal_points (poincare_line u v) = {i1, i2} \<longrightarrow> cross_ratio u i1 v i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio u i1 v i2)) \<and> 0 < Re_cross_ratio u i1 v i2
 2. \<And>x. \<lbrakk>is_real x; 0 < Re x; Re x < 1\<rbrakk> \<Longrightarrow> \<forall>i1 i2. ideal_points (poincare_line 0\<^sub>h (of_complex x)) = {i1, i2} \<longrightarrow> cross_ratio 0\<^sub>h i1 (of_complex x) i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio 0\<^sub>h i1 (of_complex x) i2)) \<and> 0 < Re_cross_ratio 0\<^sub>h i1 (of_complex x) i2
[PROOF STEP]
have ****: "- x - 1 \<noteq> 0" "x - 1 \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - x - 1 \<noteq> 0 &&& x - 1 \<noteq> 0
[PROOF STEP]
using \<open>x \<noteq> -1\<close> \<open>x \<noteq> 1\<close>
[PROOF STATE]
proof (prove)
using this:
x \<noteq> - 1
x \<noteq> 1

goal (1 subgoal):
 1. - x - 1 \<noteq> 0 &&& x - 1 \<noteq> 0
[PROOF STEP]
by (metis add.inverse_inverse eq_iff_diff_eq_0, simp)
[PROOF STATE]
proof (state)
this:
- x - 1 \<noteq> 0
x - 1 \<noteq> 0

goal (2 subgoals):
 1. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>i1 i2. ideal_points (poincare_line (moebius_pt M u) (moebius_pt M v)) = {i1, i2} \<longrightarrow> cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2)) \<and> 0 < Re_cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2\<rbrakk> \<Longrightarrow> \<forall>i1 i2. ideal_points (poincare_line u v) = {i1, i2} \<longrightarrow> cross_ratio u i1 v i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio u i1 v i2)) \<and> 0 < Re_cross_ratio u i1 v i2
 2. \<And>x. \<lbrakk>is_real x; 0 < Re x; Re x < 1\<rbrakk> \<Longrightarrow> \<forall>i1 i2. ideal_points (poincare_line 0\<^sub>h (of_complex x)) = {i1, i2} \<longrightarrow> cross_ratio 0\<^sub>h i1 (of_complex x) i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio 0\<^sub>h i1 (of_complex x) i2)) \<and> 0 < Re_cross_ratio 0\<^sub>h i1 (of_complex x) i2
[PROOF STEP]
have "poincare_line 0\<^sub>h (of_complex x) = x_axis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poincare_line 0\<^sub>h (of_complex x) = x_axis
[PROOF STEP]
using **
[PROOF STATE]
proof (prove)
using this:
of_complex x \<noteq> \<infinity>\<^sub>h
of_complex x \<noteq> 0\<^sub>h
of_complex x \<noteq> of_complex (- 1)
of_complex 1 \<noteq> of_complex x
of_complex x \<in> circline_set x_axis

goal (1 subgoal):
 1. poincare_line 0\<^sub>h (of_complex x) = x_axis
[PROOF STEP]
by (simp add: poincare_line_0_real_is_x_axis)
[PROOF STATE]
proof (state)
this:
poincare_line 0\<^sub>h (of_complex x) = x_axis

goal (2 subgoals):
 1. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>i1 i2. ideal_points (poincare_line (moebius_pt M u) (moebius_pt M v)) = {i1, i2} \<longrightarrow> cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2)) \<and> 0 < Re_cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2\<rbrakk> \<Longrightarrow> \<forall>i1 i2. ideal_points (poincare_line u v) = {i1, i2} \<longrightarrow> cross_ratio u i1 v i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio u i1 v i2)) \<and> 0 < Re_cross_ratio u i1 v i2
 2. \<And>x. \<lbrakk>is_real x; 0 < Re x; Re x < 1\<rbrakk> \<Longrightarrow> \<forall>i1 i2. ideal_points (poincare_line 0\<^sub>h (of_complex x)) = {i1, i2} \<longrightarrow> cross_ratio 0\<^sub>h i1 (of_complex x) i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio 0\<^sub>h i1 (of_complex x) i2)) \<and> 0 < Re_cross_ratio 0\<^sub>h i1 (of_complex x) i2
[PROOF STEP]
thus "?P 0\<^sub>h (of_complex x)"
[PROOF STATE]
proof (prove)
using this:
poincare_line 0\<^sub>h (of_complex x) = x_axis

goal (1 subgoal):
 1. \<forall>i1 i2. ideal_points (poincare_line 0\<^sub>h (of_complex x)) = {i1, i2} \<longrightarrow> cross_ratio 0\<^sub>h i1 (of_complex x) i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio 0\<^sub>h i1 (of_complex x) i2)) \<and> 0 < Re_cross_ratio 0\<^sub>h i1 (of_complex x) i2
[PROOF STEP]
using * ** *** ****
[PROOF STATE]
proof (prove)
using this:
poincare_line 0\<^sub>h (of_complex x) = x_axis
is_real x
0 < Re x
Re x < 1
of_complex x \<noteq> \<infinity>\<^sub>h
of_complex x \<noteq> 0\<^sub>h
of_complex x \<noteq> of_complex (- 1)
of_complex 1 \<noteq> of_complex x
of_complex x \<in> circline_set x_axis
0\<^sub>h \<noteq> of_complex (- 1)
0\<^sub>h \<noteq> of_complex 1
- x - 1 \<noteq> 0
x - 1 \<noteq> 0

goal (1 subgoal):
 1. \<forall>i1 i2. ideal_points (poincare_line 0\<^sub>h (of_complex x)) = {i1, i2} \<longrightarrow> cross_ratio 0\<^sub>h i1 (of_complex x) i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio 0\<^sub>h i1 (of_complex x) i2)) \<and> 0 < Re_cross_ratio 0\<^sub>h i1 (of_complex x) i2
[PROOF STEP]
using cross_ratio_not_inf[of "0\<^sub>h" "of_complex 1" "of_complex (-1)" "of_complex x"]
[PROOF STATE]
proof (prove)
using this:
poincare_line 0\<^sub>h (of_complex x) = x_axis
is_real x
0 < Re x
Re x < 1
of_complex x \<noteq> \<infinity>\<^sub>h
of_complex x \<noteq> 0\<^sub>h
of_complex x \<noteq> of_complex (- 1)
of_complex 1 \<noteq> of_complex x
of_complex x \<in> circline_set x_axis
0\<^sub>h \<noteq> of_complex (- 1)
0\<^sub>h \<noteq> of_complex 1
- x - 1 \<noteq> 0
x - 1 \<noteq> 0
\<lbrakk>0\<^sub>h \<noteq> of_complex 1; of_complex (- 1) \<noteq> of_complex x\<rbrakk> \<Longrightarrow> cross_ratio 0\<^sub>h (of_complex (- 1)) (of_complex x) (of_complex 1) \<noteq> \<infinity>\<^sub>h

goal (1 subgoal):
 1. \<forall>i1 i2. ideal_points (poincare_line 0\<^sub>h (of_complex x)) = {i1, i2} \<longrightarrow> cross_ratio 0\<^sub>h i1 (of_complex x) i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio 0\<^sub>h i1 (of_complex x) i2)) \<and> 0 < Re_cross_ratio 0\<^sub>h i1 (of_complex x) i2
[PROOF STEP]
using cross_ratio_not_inf[of "0\<^sub>h" "of_complex (-1)" "of_complex 1" "of_complex x"]
[PROOF STATE]
proof (prove)
using this:
poincare_line 0\<^sub>h (of_complex x) = x_axis
is_real x
0 < Re x
Re x < 1
of_complex x \<noteq> \<infinity>\<^sub>h
of_complex x \<noteq> 0\<^sub>h
of_complex x \<noteq> of_complex (- 1)
of_complex 1 \<noteq> of_complex x
of_complex x \<in> circline_set x_axis
0\<^sub>h \<noteq> of_complex (- 1)
0\<^sub>h \<noteq> of_complex 1
- x - 1 \<noteq> 0
x - 1 \<noteq> 0
\<lbrakk>0\<^sub>h \<noteq> of_complex 1; of_complex (- 1) \<noteq> of_complex x\<rbrakk> \<Longrightarrow> cross_ratio 0\<^sub>h (of_complex (- 1)) (of_complex x) (of_complex 1) \<noteq> \<infinity>\<^sub>h
\<lbrakk>0\<^sub>h \<noteq> of_complex (- 1); of_complex 1 \<noteq> of_complex x\<rbrakk> \<Longrightarrow> cross_ratio 0\<^sub>h (of_complex 1) (of_complex x) (of_complex (- 1)) \<noteq> \<infinity>\<^sub>h

goal (1 subgoal):
 1. \<forall>i1 i2. ideal_points (poincare_line 0\<^sub>h (of_complex x)) = {i1, i2} \<longrightarrow> cross_ratio 0\<^sub>h i1 (of_complex x) i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio 0\<^sub>h i1 (of_complex x) i2)) \<and> 0 < Re_cross_ratio 0\<^sub>h i1 (of_complex x) i2
[PROOF STEP]
using cross_ratio_real[of 0 "-1" x 1] cross_ratio_real[of 0 1 x "-1"]
[PROOF STATE]
proof (prove)
using this:
poincare_line 0\<^sub>h (of_complex x) = x_axis
is_real x
0 < Re x
Re x < 1
of_complex x \<noteq> \<infinity>\<^sub>h
of_complex x \<noteq> 0\<^sub>h
of_complex x \<noteq> of_complex (- 1)
of_complex 1 \<noteq> of_complex x
of_complex x \<in> circline_set x_axis
0\<^sub>h \<noteq> of_complex (- 1)
0\<^sub>h \<noteq> of_complex 1
- x - 1 \<noteq> 0
x - 1 \<noteq> 0
\<lbrakk>0\<^sub>h \<noteq> of_complex 1; of_complex (- 1) \<noteq> of_complex x\<rbrakk> \<Longrightarrow> cross_ratio 0\<^sub>h (of_complex (- 1)) (of_complex x) (of_complex 1) \<noteq> \<infinity>\<^sub>h
\<lbrakk>0\<^sub>h \<noteq> of_complex (- 1); of_complex 1 \<noteq> of_complex x\<rbrakk> \<Longrightarrow> cross_ratio 0\<^sub>h (of_complex 1) (of_complex x) (of_complex (- 1)) \<noteq> \<infinity>\<^sub>h
\<lbrakk>is_real 0; is_real (- 1); is_real x; is_real 1; 0 \<noteq> - 1 \<and> x \<noteq> 1 \<or> 0 \<noteq> 1 \<and> - 1 \<noteq> x\<rbrakk> \<Longrightarrow> is_real (to_complex (cross_ratio (of_complex 0) (of_complex (- 1)) (of_complex x) (of_complex 1)))
\<lbrakk>is_real 0; is_real 1; is_real x; is_real (- 1); 0 \<noteq> 1 \<and> x \<noteq> - 1 \<or> 0 \<noteq> - 1 \<and> 1 \<noteq> x\<rbrakk> \<Longrightarrow> is_real (to_complex (cross_ratio (of_complex 0) (of_complex 1) (of_complex x) (of_complex (- 1))))

goal (1 subgoal):
 1. \<forall>i1 i2. ideal_points (poincare_line 0\<^sub>h (of_complex x)) = {i1, i2} \<longrightarrow> cross_ratio 0\<^sub>h i1 (of_complex x) i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio 0\<^sub>h i1 (of_complex x) i2)) \<and> 0 < Re_cross_ratio 0\<^sub>h i1 (of_complex x) i2
[PROOF STEP]
apply (auto simp add: poincare_line_0_real_is_x_axis doubleton_eq_iff circline_set_x_axis)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_real x; 0 < Re x; Re x < 1; x \<noteq> 0; of_complex x \<noteq> of_complex (- 1); 1\<^sub>h \<noteq> of_complex x; 0\<^sub>h \<noteq> of_complex (- 1); - x \<noteq> 1; x \<noteq> 1; cross_ratio 0\<^sub>h (of_complex (- 1)) (of_complex x) 1\<^sub>h \<noteq> \<infinity>\<^sub>h; cross_ratio 0\<^sub>h 1\<^sub>h (of_complex x) (of_complex (- 1)) \<noteq> \<infinity>\<^sub>h; is_real (to_complex (cross_ratio 0\<^sub>h (of_complex (- 1)) (of_complex x) 1\<^sub>h)); is_real (to_complex (cross_ratio 0\<^sub>h 1\<^sub>h (of_complex x) (of_complex (- 1))))\<rbrakk> \<Longrightarrow> 0 < Re_cross_ratio 0\<^sub>h (of_complex (- 1)) (of_complex x) 1\<^sub>h
 2. \<lbrakk>is_real x; 0 < Re x; Re x < 1; x \<noteq> 0; of_complex x \<noteq> of_complex (- 1); 1\<^sub>h \<noteq> of_complex x; 0\<^sub>h \<noteq> of_complex (- 1); - x \<noteq> 1; x \<noteq> 1; cross_ratio 0\<^sub>h (of_complex (- 1)) (of_complex x) 1\<^sub>h \<noteq> \<infinity>\<^sub>h; cross_ratio 0\<^sub>h 1\<^sub>h (of_complex x) (of_complex (- 1)) \<noteq> \<infinity>\<^sub>h; is_real (to_complex (cross_ratio 0\<^sub>h (of_complex (- 1)) (of_complex x) 1\<^sub>h)); is_real (to_complex (cross_ratio 0\<^sub>h 1\<^sub>h (of_complex x) (of_complex (- 1))))\<rbrakk> \<Longrightarrow> 0 < Re_cross_ratio 0\<^sub>h 1\<^sub>h (of_complex x) (of_complex (- 1))
[PROOF STEP]
apply (subst cross_ratio, simp_all, subst Re_complex_div_gt_0, simp, subst mult_neg_neg, simp_all)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<forall>i1 i2. ideal_points (poincare_line 0\<^sub>h (of_complex x)) = {i1, i2} \<longrightarrow> cross_ratio 0\<^sub>h i1 (of_complex x) i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio 0\<^sub>h i1 (of_complex x) i2)) \<and> 0 < Re_cross_ratio 0\<^sub>h i1 (of_complex x) i2

goal (1 subgoal):
 1. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>i1 i2. ideal_points (poincare_line (moebius_pt M u) (moebius_pt M v)) = {i1, i2} \<longrightarrow> cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2)) \<and> 0 < Re_cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2\<rbrakk> \<Longrightarrow> \<forall>i1 i2. ideal_points (poincare_line u v) = {i1, i2} \<longrightarrow> cross_ratio u i1 v i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio u i1 v i2)) \<and> 0 < Re_cross_ratio u i1 v i2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>i1 i2. ideal_points (poincare_line (moebius_pt M u) (moebius_pt M v)) = {i1, i2} \<longrightarrow> cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2)) \<and> 0 < Re_cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2\<rbrakk> \<Longrightarrow> \<forall>i1 i2. ideal_points (poincare_line u v) = {i1, i2} \<longrightarrow> cross_ratio u i1 v i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio u i1 v i2)) \<and> 0 < Re_cross_ratio u i1 v i2
[PROOF STEP]
fix M u v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>i1 i2. ideal_points (poincare_line (moebius_pt M u) (moebius_pt M v)) = {i1, i2} \<longrightarrow> cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2)) \<and> 0 < Re_cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2\<rbrakk> \<Longrightarrow> \<forall>i1 i2. ideal_points (poincare_line u v) = {i1, i2} \<longrightarrow> cross_ratio u i1 v i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio u i1 v i2)) \<and> 0 < Re_cross_ratio u i1 v i2
[PROOF STEP]
let ?Mu = "moebius_pt M u" and ?Mv = "moebius_pt M v"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>i1 i2. ideal_points (poincare_line (moebius_pt M u) (moebius_pt M v)) = {i1, i2} \<longrightarrow> cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2)) \<and> 0 < Re_cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2\<rbrakk> \<Longrightarrow> \<forall>i1 i2. ideal_points (poincare_line u v) = {i1, i2} \<longrightarrow> cross_ratio u i1 v i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio u i1 v i2)) \<and> 0 < Re_cross_ratio u i1 v i2
[PROOF STEP]
assume *: "unit_disc_fix M" "u \<in> unit_disc" "v \<in> unit_disc" "u \<noteq> v"
            "?P ?Mu ?Mv"
[PROOF STATE]
proof (state)
this:
unit_disc_fix M
u \<in> unit_disc
v \<in> unit_disc
u \<noteq> v
\<forall>i1 i2. ideal_points (poincare_line (moebius_pt M u) (moebius_pt M v)) = {i1, i2} \<longrightarrow> cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2)) \<and> 0 < Re_cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2

goal (1 subgoal):
 1. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>i1 i2. ideal_points (poincare_line (moebius_pt M u) (moebius_pt M v)) = {i1, i2} \<longrightarrow> cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2)) \<and> 0 < Re_cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2\<rbrakk> \<Longrightarrow> \<forall>i1 i2. ideal_points (poincare_line u v) = {i1, i2} \<longrightarrow> cross_ratio u i1 v i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio u i1 v i2)) \<and> 0 < Re_cross_ratio u i1 v i2
[PROOF STEP]
show "?P u v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i1 i2. ideal_points (poincare_line u v) = {i1, i2} \<longrightarrow> cross_ratio u i1 v i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio u i1 v i2)) \<and> 0 < Re_cross_ratio u i1 v i2
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i1 i2. \<lbrakk>ideal_points (poincare_line u v) = {i1, i2}; cross_ratio u i1 v i2 = \<infinity>\<^sub>h\<rbrakk> \<Longrightarrow> False
 2. \<And>i1 i2. ideal_points (poincare_line u v) = {i1, i2} \<Longrightarrow> is_real (to_complex (cross_ratio u i1 v i2))
 3. \<And>i1 i2. ideal_points (poincare_line u v) = {i1, i2} \<Longrightarrow> 0 < Re_cross_ratio u i1 v i2
[PROOF STEP]
fix i1 i2
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i1 i2. \<lbrakk>ideal_points (poincare_line u v) = {i1, i2}; cross_ratio u i1 v i2 = \<infinity>\<^sub>h\<rbrakk> \<Longrightarrow> False
 2. \<And>i1 i2. ideal_points (poincare_line u v) = {i1, i2} \<Longrightarrow> is_real (to_complex (cross_ratio u i1 v i2))
 3. \<And>i1 i2. ideal_points (poincare_line u v) = {i1, i2} \<Longrightarrow> 0 < Re_cross_ratio u i1 v i2
[PROOF STEP]
let ?cr = "cross_ratio u i1 v i2"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i1 i2. \<lbrakk>ideal_points (poincare_line u v) = {i1, i2}; cross_ratio u i1 v i2 = \<infinity>\<^sub>h\<rbrakk> \<Longrightarrow> False
 2. \<And>i1 i2. ideal_points (poincare_line u v) = {i1, i2} \<Longrightarrow> is_real (to_complex (cross_ratio u i1 v i2))
 3. \<And>i1 i2. ideal_points (poincare_line u v) = {i1, i2} \<Longrightarrow> 0 < Re_cross_ratio u i1 v i2
[PROOF STEP]
assume **: "ideal_points (poincare_line u v) = {i1, i2}"
[PROOF STATE]
proof (state)
this:
ideal_points (poincare_line u v) = {i1, i2}

goal (3 subgoals):
 1. \<And>i1 i2. \<lbrakk>ideal_points (poincare_line u v) = {i1, i2}; cross_ratio u i1 v i2 = \<infinity>\<^sub>h\<rbrakk> \<Longrightarrow> False
 2. \<And>i1 i2. ideal_points (poincare_line u v) = {i1, i2} \<Longrightarrow> is_real (to_complex (cross_ratio u i1 v i2))
 3. \<And>i1 i2. ideal_points (poincare_line u v) = {i1, i2} \<Longrightarrow> 0 < Re_cross_ratio u i1 v i2
[PROOF STEP]
have "i1 \<noteq> u" "i1 \<noteq> v" "i2 \<noteq> u" "i2 \<noteq> v" "i1 \<noteq> i2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (i1 \<noteq> u &&& i1 \<noteq> v) &&& i2 \<noteq> u &&& i2 \<noteq> v &&& i1 \<noteq> i2
[PROOF STEP]
using ideal_points_different[OF *(2-3), of i1 i2] ** \<open>u \<noteq> v\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>u \<noteq> v; ideal_points (poincare_line u v) = {i1, i2}\<rbrakk> \<Longrightarrow> i1 \<noteq> i2
\<lbrakk>u \<noteq> v; ideal_points (poincare_line u v) = {i1, i2}\<rbrakk> \<Longrightarrow> u \<noteq> i1
\<lbrakk>u \<noteq> v; ideal_points (poincare_line u v) = {i1, i2}\<rbrakk> \<Longrightarrow> u \<noteq> i2
\<lbrakk>u \<noteq> v; ideal_points (poincare_line u v) = {i1, i2}\<rbrakk> \<Longrightarrow> v \<noteq> i1
\<lbrakk>u \<noteq> v; ideal_points (poincare_line u v) = {i1, i2}\<rbrakk> \<Longrightarrow> v \<noteq> i2
ideal_points (poincare_line u v) = {i1, i2}
u \<noteq> v

goal (1 subgoal):
 1. (i1 \<noteq> u &&& i1 \<noteq> v) &&& i2 \<noteq> u &&& i2 \<noteq> v &&& i1 \<noteq> i2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i1 \<noteq> u
i1 \<noteq> v
i2 \<noteq> u
i2 \<noteq> v
i1 \<noteq> i2

goal (3 subgoals):
 1. \<And>i1 i2. \<lbrakk>ideal_points (poincare_line u v) = {i1, i2}; cross_ratio u i1 v i2 = \<infinity>\<^sub>h\<rbrakk> \<Longrightarrow> False
 2. \<And>i1 i2. ideal_points (poincare_line u v) = {i1, i2} \<Longrightarrow> is_real (to_complex (cross_ratio u i1 v i2))
 3. \<And>i1 i2. ideal_points (poincare_line u v) = {i1, i2} \<Longrightarrow> 0 < Re_cross_ratio u i1 v i2
[PROOF STEP]
hence "0 < Re (to_complex ?cr) \<and> is_real (to_complex ?cr) \<and> ?cr \<noteq> \<infinity>\<^sub>h"
[PROOF STATE]
proof (prove)
using this:
i1 \<noteq> u
i1 \<noteq> v
i2 \<noteq> u
i2 \<noteq> v
i1 \<noteq> i2

goal (1 subgoal):
 1. 0 < Re_cross_ratio u i1 v i2 \<and> is_real (to_complex (cross_ratio u i1 v i2)) \<and> cross_ratio u i1 v i2 \<noteq> \<infinity>\<^sub>h
[PROOF STEP]
using * **
[PROOF STATE]
proof (prove)
using this:
i1 \<noteq> u
i1 \<noteq> v
i2 \<noteq> u
i2 \<noteq> v
i1 \<noteq> i2
unit_disc_fix M
u \<in> unit_disc
v \<in> unit_disc
u \<noteq> v
\<forall>i1 i2. ideal_points (poincare_line (moebius_pt M u) (moebius_pt M v)) = {i1, i2} \<longrightarrow> cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2)) \<and> 0 < Re_cross_ratio (moebius_pt M u) i1 (moebius_pt M v) i2
ideal_points (poincare_line u v) = {i1, i2}

goal (1 subgoal):
 1. 0 < Re_cross_ratio u i1 v i2 \<and> is_real (to_complex (cross_ratio u i1 v i2)) \<and> cross_ratio u i1 v i2 \<noteq> \<infinity>\<^sub>h
[PROOF STEP]
apply (erule_tac x="moebius_pt M i1" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i1 \<noteq> u; i1 \<noteq> v; i2 \<noteq> u; i2 \<noteq> v; i1 \<noteq> i2; unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; ideal_points (poincare_line u v) = {i1, i2}; \<forall>i2. ideal_points (poincare_line (moebius_pt M u) (moebius_pt M v)) = {moebius_pt M i1, i2} \<longrightarrow> cross_ratio (moebius_pt M u) (moebius_pt M i1) (moebius_pt M v) i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio (moebius_pt M u) (moebius_pt M i1) (moebius_pt M v) i2)) \<and> 0 < Re_cross_ratio (moebius_pt M u) (moebius_pt M i1) (moebius_pt M v) i2\<rbrakk> \<Longrightarrow> 0 < Re_cross_ratio u i1 v i2 \<and> is_real (to_complex (cross_ratio u i1 v i2)) \<and> cross_ratio u i1 v i2 \<noteq> \<infinity>\<^sub>h
[PROOF STEP]
apply (erule_tac x="moebius_pt M i2" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i1 \<noteq> u; i1 \<noteq> v; i2 \<noteq> u; i2 \<noteq> v; i1 \<noteq> i2; unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; ideal_points (poincare_line u v) = {i1, i2}; ideal_points (poincare_line (moebius_pt M u) (moebius_pt M v)) = {moebius_pt M i1, moebius_pt M i2} \<longrightarrow> cross_ratio (moebius_pt M u) (moebius_pt M i1) (moebius_pt M v) (moebius_pt M i2) \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio (moebius_pt M u) (moebius_pt M i1) (moebius_pt M v) (moebius_pt M i2))) \<and> 0 < Re_cross_ratio (moebius_pt M u) (moebius_pt M i1) (moebius_pt M v) (moebius_pt M i2)\<rbrakk> \<Longrightarrow> 0 < Re_cross_ratio u i1 v i2 \<and> is_real (to_complex (cross_ratio u i1 v i2)) \<and> cross_ratio u i1 v i2 \<noteq> \<infinity>\<^sub>h
[PROOF STEP]
apply (subst (asm) ideal_points_poincare_line_moebius[of M u v i1 i2], simp_all)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
0 < Re_cross_ratio u i1 v i2 \<and> is_real (to_complex (cross_ratio u i1 v i2)) \<and> cross_ratio u i1 v i2 \<noteq> \<infinity>\<^sub>h

goal (3 subgoals):
 1. \<And>i1 i2. \<lbrakk>ideal_points (poincare_line u v) = {i1, i2}; cross_ratio u i1 v i2 = \<infinity>\<^sub>h\<rbrakk> \<Longrightarrow> False
 2. \<And>i1 i2. ideal_points (poincare_line u v) = {i1, i2} \<Longrightarrow> is_real (to_complex (cross_ratio u i1 v i2))
 3. \<And>i1 i2. ideal_points (poincare_line u v) = {i1, i2} \<Longrightarrow> 0 < Re_cross_ratio u i1 v i2
[PROOF STEP]
thus "0 < Re (to_complex ?cr)" "is_real (to_complex ?cr)" "?cr = \<infinity>\<^sub>h \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
using this:
0 < Re_cross_ratio u i1 v i2 \<and> is_real (to_complex (cross_ratio u i1 v i2)) \<and> cross_ratio u i1 v i2 \<noteq> \<infinity>\<^sub>h

goal (1 subgoal):
 1. 0 < Re_cross_ratio u i1 v i2 &&& is_real (to_complex (cross_ratio u i1 v i2)) &&& (cross_ratio u i1 v i2 = \<infinity>\<^sub>h \<Longrightarrow> False)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
0 < Re_cross_ratio u i1 v i2
is_real (to_complex (cross_ratio u i1 v i2))
cross_ratio u i1 v i2 = \<infinity>\<^sub>h \<Longrightarrow> False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i1 i2. ideal_points (poincare_line u v) = {i1, i2} \<longrightarrow> cross_ratio u i1 v i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio u i1 v i2)) \<and> 0 < Re_cross_ratio u i1 v i2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma distance_unique:
  assumes "u \<in> unit_disc" and "v \<in> unit_disc"
  shows "\<exists>! d. poincare_distance_pred u v d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!d. poincare_distance_pred u v d
[PROOF STEP]
proof (cases "u = v")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. u = v \<Longrightarrow> \<exists>!d. poincare_distance_pred u v d
 2. u \<noteq> v \<Longrightarrow> \<exists>!d. poincare_distance_pred u v d
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
u = v

goal (2 subgoals):
 1. u = v \<Longrightarrow> \<exists>!d. poincare_distance_pred u v d
 2. u \<noteq> v \<Longrightarrow> \<exists>!d. poincare_distance_pred u v d
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
u = v

goal (1 subgoal):
 1. \<exists>!d. poincare_distance_pred u v d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>!d. poincare_distance_pred u v d

goal (1 subgoal):
 1. u \<noteq> v \<Longrightarrow> \<exists>!d. poincare_distance_pred u v d
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. u \<noteq> v \<Longrightarrow> \<exists>!d. poincare_distance_pred u v d
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
u \<noteq> v

goal (1 subgoal):
 1. u \<noteq> v \<Longrightarrow> \<exists>!d. poincare_distance_pred u v d
[PROOF STEP]
obtain i1 i2 where *: "i1 \<noteq> i2" "ideal_points (poincare_line u v) = {i1, i2}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i1 i2. \<lbrakk>i1 \<noteq> i2; ideal_points (poincare_line u v) = {i1, i2}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using obtain_ideal_points[OF is_poincare_line_poincare_line] \<open>u \<noteq> v\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?z1 \<noteq> ?w1; \<And>i1 i2. \<lbrakk>i1 \<noteq> i2; ideal_points (poincare_line ?z1 ?w1) = {i1, i2}\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
u \<noteq> v

goal (1 subgoal):
 1. (\<And>i1 i2. \<lbrakk>i1 \<noteq> i2; ideal_points (poincare_line u v) = {i1, i2}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
i1 \<noteq> i2
ideal_points (poincare_line u v) = {i1, i2}

goal (1 subgoal):
 1. u \<noteq> v \<Longrightarrow> \<exists>!d. poincare_distance_pred u v d
[PROOF STEP]
let ?d = "calc_poincare_distance u i1 v i2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. u \<noteq> v \<Longrightarrow> \<exists>!d. poincare_distance_pred u v d
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!d. poincare_distance_pred u v d
[PROOF STEP]
proof (rule ex1I)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. poincare_distance_pred u v ?a
 2. \<And>d. poincare_distance_pred u v d \<Longrightarrow> d = ?a
[PROOF STEP]
show "poincare_distance_pred u v ?d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poincare_distance_pred u v (calc_poincare_distance u i1 v i2)
[PROOF STEP]
using * \<open>u \<noteq> v\<close>
[PROOF STATE]
proof (prove)
using this:
i1 \<noteq> i2
ideal_points (poincare_line u v) = {i1, i2}
u \<noteq> v

goal (1 subgoal):
 1. poincare_distance_pred u v (calc_poincare_distance u i1 v i2)
[PROOF STEP]
proof (simp del: calc_poincare_distance_def, safe)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i1a i2a. \<lbrakk>i1 \<noteq> i2; ideal_points (poincare_line u v) = {i1, i2}; u \<noteq> v; i1 \<noteq> i2; ideal_points (poincare_line u v) = {i1, i2}; u \<noteq> v; {i1, i2} = {i1a, i2a}\<rbrakk> \<Longrightarrow> calc_poincare_distance u i1 v i2 = calc_poincare_distance u i1a v i2a
[PROOF STEP]
fix i1' i2'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i1a i2a. \<lbrakk>i1 \<noteq> i2; ideal_points (poincare_line u v) = {i1, i2}; u \<noteq> v; i1 \<noteq> i2; ideal_points (poincare_line u v) = {i1, i2}; u \<noteq> v; {i1, i2} = {i1a, i2a}\<rbrakk> \<Longrightarrow> calc_poincare_distance u i1 v i2 = calc_poincare_distance u i1a v i2a
[PROOF STEP]
assume "{i1, i2} = {i1', i2'}"
[PROOF STATE]
proof (state)
this:
{i1, i2} = {i1', i2'}

goal (1 subgoal):
 1. \<And>i1a i2a. \<lbrakk>i1 \<noteq> i2; ideal_points (poincare_line u v) = {i1, i2}; u \<noteq> v; i1 \<noteq> i2; ideal_points (poincare_line u v) = {i1, i2}; u \<noteq> v; {i1, i2} = {i1a, i2a}\<rbrakk> \<Longrightarrow> calc_poincare_distance u i1 v i2 = calc_poincare_distance u i1a v i2a
[PROOF STEP]
hence **: "(i1' = i1 \<and> i2' = i2) \<or> (i1' = i2 \<and> i2' = i1)"
[PROOF STATE]
proof (prove)
using this:
{i1, i2} = {i1', i2'}

goal (1 subgoal):
 1. i1' = i1 \<and> i2' = i2 \<or> i1' = i2 \<and> i2' = i1
[PROOF STEP]
using doubleton_eq_iff[of i1 i2 i1' i2']
[PROOF STATE]
proof (prove)
using this:
{i1, i2} = {i1', i2'}
({i1, i2} = {i1', i2'}) = (i1 = i1' \<and> i2 = i2' \<or> i1 = i2' \<and> i2 = i1')

goal (1 subgoal):
 1. i1' = i1 \<and> i2' = i2 \<or> i1' = i2 \<and> i2' = i1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
i1' = i1 \<and> i2' = i2 \<or> i1' = i2 \<and> i2' = i1

goal (1 subgoal):
 1. \<And>i1a i2a. \<lbrakk>i1 \<noteq> i2; ideal_points (poincare_line u v) = {i1, i2}; u \<noteq> v; i1 \<noteq> i2; ideal_points (poincare_line u v) = {i1, i2}; u \<noteq> v; {i1, i2} = {i1a, i2a}\<rbrakk> \<Longrightarrow> calc_poincare_distance u i1 v i2 = calc_poincare_distance u i1a v i2a
[PROOF STEP]
have all_different: "u \<noteq> i1" "u \<noteq> i2" "v \<noteq> i1" "v \<noteq> i2" "u \<noteq> i1'" "u \<noteq> i2'" "v \<noteq> i1'" "v \<noteq> i2'" "i1 \<noteq> i2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((u \<noteq> i1 &&& u \<noteq> i2) &&& v \<noteq> i1 &&& v \<noteq> i2) &&& (u \<noteq> i1' &&& u \<noteq> i2') &&& v \<noteq> i1' &&& v \<noteq> i2' &&& i1 \<noteq> i2
[PROOF STEP]
using ideal_points_different[OF assms, of i1 i2] * ** \<open>u \<noteq> v\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>u \<noteq> v; ideal_points (poincare_line u v) = {i1, i2}\<rbrakk> \<Longrightarrow> i1 \<noteq> i2
\<lbrakk>u \<noteq> v; ideal_points (poincare_line u v) = {i1, i2}\<rbrakk> \<Longrightarrow> u \<noteq> i1
\<lbrakk>u \<noteq> v; ideal_points (poincare_line u v) = {i1, i2}\<rbrakk> \<Longrightarrow> u \<noteq> i2
\<lbrakk>u \<noteq> v; ideal_points (poincare_line u v) = {i1, i2}\<rbrakk> \<Longrightarrow> v \<noteq> i1
\<lbrakk>u \<noteq> v; ideal_points (poincare_line u v) = {i1, i2}\<rbrakk> \<Longrightarrow> v \<noteq> i2
i1 \<noteq> i2
ideal_points (poincare_line u v) = {i1, i2}
i1' = i1 \<and> i2' = i2 \<or> i1' = i2 \<and> i2' = i1
u \<noteq> v

goal (1 subgoal):
 1. ((u \<noteq> i1 &&& u \<noteq> i2) &&& v \<noteq> i1 &&& v \<noteq> i2) &&& (u \<noteq> i1' &&& u \<noteq> i2') &&& v \<noteq> i1' &&& v \<noteq> i2' &&& i1 \<noteq> i2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u \<noteq> i1
u \<noteq> i2
v \<noteq> i1
v \<noteq> i2
u \<noteq> i1'
u \<noteq> i2'
v \<noteq> i1'
v \<noteq> i2'
i1 \<noteq> i2

goal (1 subgoal):
 1. \<And>i1a i2a. \<lbrakk>i1 \<noteq> i2; ideal_points (poincare_line u v) = {i1, i2}; u \<noteq> v; i1 \<noteq> i2; ideal_points (poincare_line u v) = {i1, i2}; u \<noteq> v; {i1, i2} = {i1a, i2a}\<rbrakk> \<Longrightarrow> calc_poincare_distance u i1 v i2 = calc_poincare_distance u i1a v i2a
[PROOF STEP]
show "calc_poincare_distance u i1 v i2 = calc_poincare_distance u i1' v i2'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. calc_poincare_distance u i1 v i2 = calc_poincare_distance u i1' v i2'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. calc_poincare_distance u i1 v i2 = calc_poincare_distance u i1' v i2'
[PROOF STEP]
let ?cr = "cross_ratio u i1 v i2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. calc_poincare_distance u i1 v i2 = calc_poincare_distance u i1' v i2'
[PROOF STEP]
let ?cr' = "cross_ratio u i1' v i2'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. calc_poincare_distance u i1 v i2 = calc_poincare_distance u i1' v i2'
[PROOF STEP]
have "Re (to_complex ?cr) > 0" "is_real (to_complex ?cr)"
             "Re (to_complex ?cr') > 0" "is_real (to_complex ?cr')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0 < Re_cross_ratio u i1 v i2 &&& is_real (to_complex (cross_ratio u i1 v i2))) &&& 0 < Re_cross_ratio u i1' v i2' &&& is_real (to_complex (cross_ratio u i1' v i2'))
[PROOF STEP]
using False distance_cross_ratio_real_positive[OF assms(1-2)] * **
[PROOF STATE]
proof (prove)
using this:
u \<noteq> v
u \<noteq> v \<Longrightarrow> \<forall>i1 i2. ideal_points (poincare_line u v) = {i1, i2} \<longrightarrow> cross_ratio u i1 v i2 \<noteq> \<infinity>\<^sub>h \<and> is_real (to_complex (cross_ratio u i1 v i2)) \<and> 0 < Re_cross_ratio u i1 v i2
i1 \<noteq> i2
ideal_points (poincare_line u v) = {i1, i2}
i1' = i1 \<and> i2' = i2 \<or> i1' = i2 \<and> i2' = i1

goal (1 subgoal):
 1. (0 < Re_cross_ratio u i1 v i2 &&& is_real (to_complex (cross_ratio u i1 v i2))) &&& 0 < Re_cross_ratio u i1' v i2' &&& is_real (to_complex (cross_ratio u i1' v i2'))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < Re_cross_ratio u i1 v i2
is_real (to_complex (cross_ratio u i1 v i2))
0 < Re_cross_ratio u i1' v i2'
is_real (to_complex (cross_ratio u i1' v i2'))

goal (1 subgoal):
 1. calc_poincare_distance u i1 v i2 = calc_poincare_distance u i1' v i2'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < Re_cross_ratio u i1 v i2
is_real (to_complex (cross_ratio u i1 v i2))
0 < Re_cross_ratio u i1' v i2'
is_real (to_complex (cross_ratio u i1' v i2'))

goal (1 subgoal):
 1. calc_poincare_distance u i1 v i2 = calc_poincare_distance u i1' v i2'
[PROOF STEP]
using **
[PROOF STATE]
proof (prove)
using this:
0 < Re_cross_ratio u i1 v i2
is_real (to_complex (cross_ratio u i1 v i2))
0 < Re_cross_ratio u i1' v i2'
is_real (to_complex (cross_ratio u i1' v i2'))
i1' = i1 \<and> i2' = i2 \<or> i1' = i2 \<and> i2' = i1

goal (1 subgoal):
 1. calc_poincare_distance u i1 v i2 = calc_poincare_distance u i1' v i2'
[PROOF STEP]
using cross_ratio_not_zero cross_ratio_not_inf all_different
[PROOF STATE]
proof (prove)
using this:
0 < Re_cross_ratio u i1 v i2
is_real (to_complex (cross_ratio u i1 v i2))
0 < Re_cross_ratio u i1' v i2'
is_real (to_complex (cross_ratio u i1' v i2'))
i1' = i1 \<and> i2' = i2 \<or> i1' = i2 \<and> i2' = i1
\<lbrakk>?z \<noteq> ?u; ?v \<noteq> ?w\<rbrakk> \<Longrightarrow> cross_ratio ?z ?u ?v ?w \<noteq> 0\<^sub>h
\<lbrakk>?z \<noteq> ?w; ?u \<noteq> ?v\<rbrakk> \<Longrightarrow> cross_ratio ?z ?u ?v ?w \<noteq> \<infinity>\<^sub>h
u \<noteq> i1
u \<noteq> i2
v \<noteq> i1
v \<noteq> i2
u \<noteq> i1'
u \<noteq> i2'
v \<noteq> i1'
v \<noteq> i2'
i1 \<noteq> i2

goal (1 subgoal):
 1. calc_poincare_distance u i1 v i2 = calc_poincare_distance u i1' v i2'
[PROOF STEP]
by auto (subst cross_ratio_commute_24, subst reciprocal_real, simp_all add: ln_div)
[PROOF STATE]
proof (state)
this:
calc_poincare_distance u i1 v i2 = calc_poincare_distance u i1' v i2'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
calc_poincare_distance u i1 v i2 = calc_poincare_distance u i1' v i2'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
poincare_distance_pred u v (calc_poincare_distance u i1 v i2)

goal (1 subgoal):
 1. \<And>d. poincare_distance_pred u v d \<Longrightarrow> d = calc_poincare_distance u i1 v i2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>d. poincare_distance_pred u v d \<Longrightarrow> d = calc_poincare_distance u i1 v i2
[PROOF STEP]
fix d
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>d. poincare_distance_pred u v d \<Longrightarrow> d = calc_poincare_distance u i1 v i2
[PROOF STEP]
assume "poincare_distance_pred u v d"
[PROOF STATE]
proof (state)
this:
poincare_distance_pred u v d

goal (1 subgoal):
 1. \<And>d. poincare_distance_pred u v d \<Longrightarrow> d = calc_poincare_distance u i1 v i2
[PROOF STEP]
thus "d = ?d"
[PROOF STATE]
proof (prove)
using this:
poincare_distance_pred u v d

goal (1 subgoal):
 1. d = calc_poincare_distance u i1 v i2
[PROOF STEP]
using * \<open>u \<noteq> v\<close>
[PROOF STATE]
proof (prove)
using this:
poincare_distance_pred u v d
i1 \<noteq> i2
ideal_points (poincare_line u v) = {i1, i2}
u \<noteq> v

goal (1 subgoal):
 1. d = calc_poincare_distance u i1 v i2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
d = calc_poincare_distance u i1 v i2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>!d. poincare_distance_pred u v d

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma poincare_distance_satisfies_pred [simp]:
  assumes "u \<in> unit_disc" and "v \<in> unit_disc"
  shows "poincare_distance_pred u v (poincare_distance u v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poincare_distance_pred u v (poincare_distance u v)
[PROOF STEP]
using distance_unique[OF assms] theI'[of "poincare_distance_pred u v"]
[PROOF STATE]
proof (prove)
using this:
\<exists>!d. poincare_distance_pred u v d
\<exists>!x. poincare_distance_pred u v x \<Longrightarrow> poincare_distance_pred u v (THE x. poincare_distance_pred u v x)

goal (1 subgoal):
 1. poincare_distance_pred u v (poincare_distance u v)
[PROOF STEP]
unfolding poincare_distance_def
[PROOF STATE]
proof (prove)
using this:
\<exists>!d. poincare_distance_pred u v d
\<exists>!x. poincare_distance_pred u v x \<Longrightarrow> poincare_distance_pred u v (THE x. poincare_distance_pred u v x)

goal (1 subgoal):
 1. poincare_distance_pred u v (The (poincare_distance_pred u v))
[PROOF STEP]
by blast


[STATEMENT]
lemma poincare_distance_I:
  assumes "u \<in> unit_disc" and "v \<in> unit_disc" and "u \<noteq> v" and "ideal_points (poincare_line u v) = {i1, i2}"
  shows "poincare_distance u v = calc_poincare_distance u i1 v i2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poincare_distance u v = calc_poincare_distance u i1 v i2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
u \<in> unit_disc
v \<in> unit_disc
u \<noteq> v
ideal_points (poincare_line u v) = {i1, i2}

goal (1 subgoal):
 1. poincare_distance u v = calc_poincare_distance u i1 v i2
[PROOF STEP]
using poincare_distance_satisfies_pred[OF assms(1-2)]
[PROOF STATE]
proof (prove)
using this:
u \<in> unit_disc
v \<in> unit_disc
u \<noteq> v
ideal_points (poincare_line u v) = {i1, i2}
poincare_distance_pred u v (poincare_distance u v)

goal (1 subgoal):
 1. poincare_distance u v = calc_poincare_distance u i1 v i2
[PROOF STEP]
by simp


[STATEMENT]
lemma poincare_distance_refl [simp]:
  assumes "u \<in> unit_disc"
  shows "poincare_distance u u = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poincare_distance u u = 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
u \<in> unit_disc

goal (1 subgoal):
 1. poincare_distance u u = 0
[PROOF STEP]
using poincare_distance_satisfies_pred[OF assms assms]
[PROOF STATE]
proof (prove)
using this:
u \<in> unit_disc
poincare_distance_pred u u (poincare_distance u u)

goal (1 subgoal):
 1. poincare_distance u u = 0
[PROOF STEP]
by simp


[STATEMENT]
lemma unit_disc_fix_preserve_poincare_distance [simp]:
  assumes "unit_disc_fix M" and "u \<in> unit_disc" and "v \<in> unit_disc"
  shows "poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u v
[PROOF STEP]
proof (cases "u = v")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. u = v \<Longrightarrow> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u v
 2. u \<noteq> v \<Longrightarrow> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u v
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
u = v

goal (2 subgoals):
 1. u = v \<Longrightarrow> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u v
 2. u \<noteq> v \<Longrightarrow> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u v
[PROOF STEP]
have "moebius_pt M u \<in> unit_disc" "moebius_pt M v \<in> unit_disc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. moebius_pt M u \<in> unit_disc &&& moebius_pt M v \<in> unit_disc
[PROOF STEP]
using unit_disc_fix_iff[OF assms(1), symmetric] assms
[PROOF STATE]
proof (prove)
using this:
unit_disc = moebius_pt M ` unit_disc
unit_disc_fix M
u \<in> unit_disc
v \<in> unit_disc

goal (1 subgoal):
 1. moebius_pt M u \<in> unit_disc &&& moebius_pt M v \<in> unit_disc
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
moebius_pt M u \<in> unit_disc
moebius_pt M v \<in> unit_disc

goal (2 subgoals):
 1. u = v \<Longrightarrow> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u v
 2. u \<noteq> v \<Longrightarrow> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u v
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
moebius_pt M u \<in> unit_disc
moebius_pt M v \<in> unit_disc

goal (1 subgoal):
 1. poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u v
[PROOF STEP]
using assms \<open>u = v\<close>
[PROOF STATE]
proof (prove)
using this:
moebius_pt M u \<in> unit_disc
moebius_pt M v \<in> unit_disc
unit_disc_fix M
u \<in> unit_disc
v \<in> unit_disc
u = v

goal (1 subgoal):
 1. poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u v

goal (1 subgoal):
 1. u \<noteq> v \<Longrightarrow> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. u \<noteq> v \<Longrightarrow> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u v
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
u \<noteq> v

goal (1 subgoal):
 1. u \<noteq> v \<Longrightarrow> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u v
[PROOF STEP]
obtain i1 i2 where *: "ideal_points (poincare_line u v) = {i1, i2}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i1 i2. ideal_points (poincare_line u v) = {i1, i2} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>u \<noteq> v\<close>
[PROOF STATE]
proof (prove)
using this:
u \<noteq> v

goal (1 subgoal):
 1. (\<And>i1 i2. ideal_points (poincare_line u v) = {i1, i2} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule obtain_ideal_points[OF is_poincare_line_poincare_line[of u v]])
[PROOF STATE]
proof (state)
this:
ideal_points (poincare_line u v) = {i1, i2}

goal (1 subgoal):
 1. u \<noteq> v \<Longrightarrow> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u v
[PROOF STEP]
let ?Mu = "moebius_pt M u" and ?Mv = "moebius_pt M v" and ?Mi1 = "moebius_pt M i1" and ?Mi2 = "moebius_pt M i2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. u \<noteq> v \<Longrightarrow> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u v
[PROOF STEP]
have **: "?Mu \<in> unit_disc" "?Mv \<in> unit_disc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. moebius_pt M u \<in> unit_disc &&& moebius_pt M v \<in> unit_disc
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
unit_disc_fix M
u \<in> unit_disc
v \<in> unit_disc

goal (1 subgoal):
 1. moebius_pt M u \<in> unit_disc &&& moebius_pt M v \<in> unit_disc
[PROOF STEP]
using unit_disc_fix_iff
[PROOF STATE]
proof (prove)
using this:
unit_disc_fix M
u \<in> unit_disc
v \<in> unit_disc
unit_disc_fix ?M \<Longrightarrow> moebius_pt ?M ` unit_disc = unit_disc

goal (1 subgoal):
 1. moebius_pt M u \<in> unit_disc &&& moebius_pt M v \<in> unit_disc
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
moebius_pt M u \<in> unit_disc
moebius_pt M v \<in> unit_disc

goal (1 subgoal):
 1. u \<noteq> v \<Longrightarrow> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u v
[PROOF STEP]
have ***: "?Mu \<noteq> ?Mv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. moebius_pt M u \<noteq> moebius_pt M v
[PROOF STEP]
using \<open>u \<noteq> v\<close>
[PROOF STATE]
proof (prove)
using this:
u \<noteq> v

goal (1 subgoal):
 1. moebius_pt M u \<noteq> moebius_pt M v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
moebius_pt M u \<noteq> moebius_pt M v

goal (1 subgoal):
 1. u \<noteq> v \<Longrightarrow> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u v
[PROOF STEP]
have "poincare_distance u v = calc_poincare_distance u i1 v i2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poincare_distance u v = calc_poincare_distance u i1 v i2
[PROOF STEP]
using poincare_distance_I[OF assms(2-3) \<open>u \<noteq> v\<close> *]
[PROOF STATE]
proof (prove)
using this:
poincare_distance u v = calc_poincare_distance u i1 v i2

goal (1 subgoal):
 1. poincare_distance u v = calc_poincare_distance u i1 v i2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
poincare_distance u v = calc_poincare_distance u i1 v i2

goal (1 subgoal):
 1. u \<noteq> v \<Longrightarrow> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
poincare_distance u v = calc_poincare_distance u i1 v i2

goal (1 subgoal):
 1. u \<noteq> v \<Longrightarrow> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u v
[PROOF STEP]
have "unit_circle_fix M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unit_circle_fix M
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
unit_disc_fix M
u \<in> unit_disc
v \<in> unit_disc

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

goal (1 subgoal):
 1. u \<noteq> v \<Longrightarrow> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u v
[PROOF STEP]
hence ++: "ideal_points (poincare_line ?Mu ?Mv) = {?Mi1, ?Mi2}"
[PROOF STATE]
proof (prove)
using this:
unit_circle_fix M

goal (1 subgoal):
 1. ideal_points (poincare_line (moebius_pt M u) (moebius_pt M v)) = {moebius_pt M i1, moebius_pt M i2}
[PROOF STEP]
using \<open>u \<noteq> v\<close> assms *
[PROOF STATE]
proof (prove)
using this:
unit_circle_fix M
u \<noteq> v
unit_disc_fix M
u \<in> unit_disc
v \<in> unit_disc
ideal_points (poincare_line u v) = {i1, i2}

goal (1 subgoal):
 1. ideal_points (poincare_line (moebius_pt M u) (moebius_pt M v)) = {moebius_pt M i1, moebius_pt M i2}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ideal_points (poincare_line (moebius_pt M u) (moebius_pt M v)) = {moebius_pt M i1, moebius_pt M i2}

goal (1 subgoal):
 1. u \<noteq> v \<Longrightarrow> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u v
[PROOF STEP]
have "poincare_distance ?Mu ?Mv = calc_poincare_distance ?Mu ?Mi1 ?Mv ?Mi2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poincare_distance (moebius_pt M u) (moebius_pt M v) = calc_poincare_distance (moebius_pt M u) (moebius_pt M i1) (moebius_pt M v) (moebius_pt M i2)
[PROOF STEP]
by (rule poincare_distance_I[OF ** *** ++])
[PROOF STATE]
proof (state)
this:
poincare_distance (moebius_pt M u) (moebius_pt M v) = calc_poincare_distance (moebius_pt M u) (moebius_pt M i1) (moebius_pt M v) (moebius_pt M i2)

goal (1 subgoal):
 1. u \<noteq> v \<Longrightarrow> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
poincare_distance (moebius_pt M u) (moebius_pt M v) = calc_poincare_distance (moebius_pt M u) (moebius_pt M i1) (moebius_pt M v) (moebius_pt M i2)

goal (1 subgoal):
 1. u \<noteq> v \<Longrightarrow> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u v
[PROOF STEP]
have "calc_poincare_distance ?Mu ?Mi1 ?Mv ?Mi2 = calc_poincare_distance u i1 v i2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. calc_poincare_distance (moebius_pt M u) (moebius_pt M i1) (moebius_pt M v) (moebius_pt M i2) = calc_poincare_distance u i1 v i2
[PROOF STEP]
using ideal_points_different[OF assms(2-3) \<open>u \<noteq> v\<close> *]
[PROOF STATE]
proof (prove)
using this:
i1 \<noteq> i2
u \<noteq> i1
u \<noteq> i2
v \<noteq> i1
v \<noteq> i2

goal (1 subgoal):
 1. calc_poincare_distance (moebius_pt M u) (moebius_pt M i1) (moebius_pt M v) (moebius_pt M i2) = calc_poincare_distance u i1 v i2
[PROOF STEP]
unfolding calc_poincare_distance_def
[PROOF STATE]
proof (prove)
using this:
i1 \<noteq> i2
u \<noteq> i1
u \<noteq> i2
v \<noteq> i1
v \<noteq> i2

goal (1 subgoal):
 1. \<bar>ln (Re_cross_ratio (moebius_pt M u) (moebius_pt M i1) (moebius_pt M v) (moebius_pt M i2))\<bar> = \<bar>ln (Re_cross_ratio u i1 v i2)\<bar>
[PROOF STEP]
by (subst moebius_preserve_cross_ratio[symmetric], simp_all)
[PROOF STATE]
proof (state)
this:
calc_poincare_distance (moebius_pt M u) (moebius_pt M i1) (moebius_pt M v) (moebius_pt M i2) = calc_poincare_distance u i1 v i2

goal (1 subgoal):
 1. u \<noteq> v \<Longrightarrow> poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u v
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
poincare_distance u v = calc_poincare_distance u i1 v i2
poincare_distance (moebius_pt M u) (moebius_pt M v) = calc_poincare_distance (moebius_pt M u) (moebius_pt M i1) (moebius_pt M v) (moebius_pt M i2)
calc_poincare_distance (moebius_pt M u) (moebius_pt M i1) (moebius_pt M v) (moebius_pt M i2) = calc_poincare_distance u i1 v i2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
poincare_distance u v = calc_poincare_distance u i1 v i2
poincare_distance (moebius_pt M u) (moebius_pt M v) = calc_poincare_distance (moebius_pt M u) (moebius_pt M i1) (moebius_pt M v) (moebius_pt M i2)
calc_poincare_distance (moebius_pt M u) (moebius_pt M i1) (moebius_pt M v) (moebius_pt M i2) = calc_poincare_distance u i1 v i2

goal (1 subgoal):
 1. poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
poincare_distance (moebius_pt M u) (moebius_pt M v) = poincare_distance u v

goal:
No subgoals!
[PROOF STEP]
qed