[STATEMENT]
lemma ex_perpendicular:
  assumes "is_poincare_line H" "z \<in> unit_disc"
  shows "\<exists> H'. is_poincare_line H' \<and> perpendicular H H' \<and> z \<in> circline_set H'" (is "?P' H z")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>H'. is_poincare_line H' \<and> perpendicular H H' \<and> z \<in> circline_set H'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>H'. is_poincare_line H' \<and> perpendicular H H' \<and> z \<in> circline_set H'
[PROOF STEP]
have "\<forall> z. z \<in> unit_disc \<longrightarrow> ?P' H z" (is "?P H")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>z. z \<in> unit_disc \<longrightarrow> (\<exists>H'. is_poincare_line H' \<and> perpendicular H H' \<and> z \<in> circline_set H')
[PROOF STEP]
proof (rule wlog_line_x_axis)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. is_poincare_line H
 2. \<forall>z. z \<in> unit_disc \<longrightarrow> (\<exists>H'. is_poincare_line H' \<and> perpendicular x_axis H' \<and> z \<in> circline_set H')
 3. \<And>M. \<lbrakk>unit_disc_fix M; \<forall>z. z \<in> unit_disc \<longrightarrow> (\<exists>H'. is_poincare_line H' \<and> perpendicular (moebius_circline M H) H' \<and> z \<in> circline_set H')\<rbrakk> \<Longrightarrow> \<forall>z. z \<in> unit_disc \<longrightarrow> (\<exists>H'. is_poincare_line H' \<and> perpendicular H H' \<and> z \<in> circline_set H')
[PROOF STEP]
show "?P x_axis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>z. z \<in> unit_disc \<longrightarrow> (\<exists>H'. is_poincare_line H' \<and> perpendicular x_axis H' \<and> z \<in> circline_set H')
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z. z \<in> unit_disc \<Longrightarrow> \<exists>H'. is_poincare_line H' \<and> perpendicular x_axis H' \<and> z \<in> circline_set H'
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z. z \<in> unit_disc \<Longrightarrow> \<exists>H'. is_poincare_line H' \<and> perpendicular x_axis H' \<and> z \<in> circline_set H'
[PROOF STEP]
assume "z \<in> unit_disc"
[PROOF STATE]
proof (state)
this:
z \<in> unit_disc

goal (1 subgoal):
 1. \<And>z. z \<in> unit_disc \<Longrightarrow> \<exists>H'. is_poincare_line H' \<and> perpendicular x_axis H' \<and> z \<in> circline_set H'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
z \<in> unit_disc
[PROOF STEP]
have "z \<noteq> of_complex 1" "z \<noteq> of_complex (-1)"
[PROOF STATE]
proof (prove)
using this:
z \<in> unit_disc

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

goal (1 subgoal):
 1. \<And>z. z \<in> unit_disc \<Longrightarrow> \<exists>H'. is_poincare_line H' \<and> perpendicular x_axis H' \<and> z \<in> circline_set H'
[PROOF STEP]
thus "?P' x_axis z"
[PROOF STATE]
proof (prove)
using this:
z \<noteq> of_complex 1
z \<noteq> of_complex (- 1)

goal (1 subgoal):
 1. \<exists>H'. is_poincare_line H' \<and> perpendicular x_axis H' \<and> z \<in> circline_set H'
[PROOF STEP]
using \<open>z \<in> unit_disc\<close>
[PROOF STATE]
proof (prove)
using this:
z \<noteq> of_complex 1
z \<noteq> of_complex (- 1)
z \<in> unit_disc

goal (1 subgoal):
 1. \<exists>H'. is_poincare_line H' \<and> perpendicular x_axis H' \<and> z \<in> circline_set H'
[PROOF STEP]
using calc_perpendicular_to_x_axis[of z] perpendicular_to_x_axis
[PROOF STATE]
proof (prove)
using this:
z \<noteq> of_complex 1
z \<noteq> of_complex (- 1)
z \<in> unit_disc
\<lbrakk>z \<noteq> of_complex 1; z \<noteq> of_complex (- 1)\<rbrakk> \<Longrightarrow> z \<in> circline_set (calc_perpendicular_to_x_axis z) \<and> is_poincare_line (calc_perpendicular_to_x_axis z) \<and> perpendicular_to_x_axis (calc_perpendicular_to_x_axis z)
is_poincare_line ?H \<Longrightarrow> perpendicular_to_x_axis ?H = perpendicular x_axis ?H

goal (1 subgoal):
 1. \<exists>H'. is_poincare_line H' \<and> perpendicular x_axis H' \<and> z \<in> circline_set H'
[PROOF STEP]
by (rule_tac x = "calc_perpendicular_to_x_axis z" in exI, auto)
[PROOF STATE]
proof (state)
this:
\<exists>H'. is_poincare_line H' \<and> perpendicular x_axis H' \<and> z \<in> circline_set H'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>z. z \<in> unit_disc \<longrightarrow> (\<exists>H'. is_poincare_line H' \<and> perpendicular x_axis H' \<and> z \<in> circline_set H')

goal (2 subgoals):
 1. is_poincare_line H
 2. \<And>M. \<lbrakk>unit_disc_fix M; \<forall>z. z \<in> unit_disc \<longrightarrow> (\<exists>H'. is_poincare_line H' \<and> perpendicular (moebius_circline M H) H' \<and> z \<in> circline_set H')\<rbrakk> \<Longrightarrow> \<forall>z. z \<in> unit_disc \<longrightarrow> (\<exists>H'. is_poincare_line H' \<and> perpendicular H H' \<and> z \<in> circline_set H')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_poincare_line H
 2. \<And>M. \<lbrakk>unit_disc_fix M; \<forall>z. z \<in> unit_disc \<longrightarrow> (\<exists>H'. is_poincare_line H' \<and> perpendicular (moebius_circline M H) H' \<and> z \<in> circline_set H')\<rbrakk> \<Longrightarrow> \<forall>z. z \<in> unit_disc \<longrightarrow> (\<exists>H'. is_poincare_line H' \<and> perpendicular H H' \<and> z \<in> circline_set H')
[PROOF STEP]
fix M
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_poincare_line H
 2. \<And>M. \<lbrakk>unit_disc_fix M; \<forall>z. z \<in> unit_disc \<longrightarrow> (\<exists>H'. is_poincare_line H' \<and> perpendicular (moebius_circline M H) H' \<and> z \<in> circline_set H')\<rbrakk> \<Longrightarrow> \<forall>z. z \<in> unit_disc \<longrightarrow> (\<exists>H'. is_poincare_line H' \<and> perpendicular H H' \<and> z \<in> circline_set H')
[PROOF STEP]
assume "unit_disc_fix M"
[PROOF STATE]
proof (state)
this:
unit_disc_fix M

goal (2 subgoals):
 1. is_poincare_line H
 2. \<And>M. \<lbrakk>unit_disc_fix M; \<forall>z. z \<in> unit_disc \<longrightarrow> (\<exists>H'. is_poincare_line H' \<and> perpendicular (moebius_circline M H) H' \<and> z \<in> circline_set H')\<rbrakk> \<Longrightarrow> \<forall>z. z \<in> unit_disc \<longrightarrow> (\<exists>H'. is_poincare_line H' \<and> perpendicular H H' \<and> z \<in> circline_set H')
[PROOF STEP]
assume *: "?P (moebius_circline M H)"
[PROOF STATE]
proof (state)
this:
\<forall>z. z \<in> unit_disc \<longrightarrow> (\<exists>H'. is_poincare_line H' \<and> perpendicular (moebius_circline M H) H' \<and> z \<in> circline_set H')

goal (2 subgoals):
 1. is_poincare_line H
 2. \<And>M. \<lbrakk>unit_disc_fix M; \<forall>z. z \<in> unit_disc \<longrightarrow> (\<exists>H'. is_poincare_line H' \<and> perpendicular (moebius_circline M H) H' \<and> z \<in> circline_set H')\<rbrakk> \<Longrightarrow> \<forall>z. z \<in> unit_disc \<longrightarrow> (\<exists>H'. is_poincare_line H' \<and> perpendicular H H' \<and> z \<in> circline_set H')
[PROOF STEP]
show "?P H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>z. z \<in> unit_disc \<longrightarrow> (\<exists>H'. is_poincare_line H' \<and> perpendicular H H' \<and> z \<in> circline_set H')
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z. z \<in> unit_disc \<Longrightarrow> \<exists>H'. is_poincare_line H' \<and> perpendicular H H' \<and> z \<in> circline_set H'
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z. z \<in> unit_disc \<Longrightarrow> \<exists>H'. is_poincare_line H' \<and> perpendicular H H' \<and> z \<in> circline_set H'
[PROOF STEP]
assume "z \<in> unit_disc"
[PROOF STATE]
proof (state)
this:
z \<in> unit_disc

goal (1 subgoal):
 1. \<And>z. z \<in> unit_disc \<Longrightarrow> \<exists>H'. is_poincare_line H' \<and> perpendicular H H' \<and> z \<in> circline_set H'
[PROOF STEP]
hence "moebius_pt M z \<in> unit_disc"
[PROOF STATE]
proof (prove)
using this:
z \<in> unit_disc

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

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

goal (1 subgoal):
 1. \<And>z. z \<in> unit_disc \<Longrightarrow> \<exists>H'. is_poincare_line H' \<and> perpendicular H H' \<and> z \<in> circline_set H'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
moebius_pt M z \<in> unit_disc
[PROOF STEP]
obtain H' where *: "is_poincare_line H'" "perpendicular (moebius_circline M H) H'" "moebius_pt M z \<in> circline_set H'"
[PROOF STATE]
proof (prove)
using this:
moebius_pt M z \<in> unit_disc

goal (1 subgoal):
 1. (\<And>H'. \<lbrakk>is_poincare_line H'; perpendicular (moebius_circline M H) H'; moebius_pt M z \<in> circline_set H'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
moebius_pt M z \<in> unit_disc
\<forall>z. z \<in> unit_disc \<longrightarrow> (\<exists>H'. is_poincare_line H' \<and> perpendicular (moebius_circline M H) H' \<and> z \<in> circline_set H')

goal (1 subgoal):
 1. (\<And>H'. \<lbrakk>is_poincare_line H'; perpendicular (moebius_circline M H) H'; moebius_pt M z \<in> circline_set H'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_poincare_line H'
perpendicular (moebius_circline M H) H'
moebius_pt M z \<in> circline_set H'

goal (1 subgoal):
 1. \<And>z. z \<in> unit_disc \<Longrightarrow> \<exists>H'. is_poincare_line H' \<and> perpendicular H H' \<and> z \<in> circline_set H'
[PROOF STEP]
have h: "H = moebius_circline (-M) (moebius_circline M H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H = moebius_circline (- M) (moebius_circline M H)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
H = moebius_circline (- M) (moebius_circline M H)

goal (1 subgoal):
 1. \<And>z. z \<in> unit_disc \<Longrightarrow> \<exists>H'. is_poincare_line H' \<and> perpendicular H H' \<and> z \<in> circline_set H'
[PROOF STEP]
show "?P' H z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>H'. is_poincare_line H' \<and> perpendicular H H' \<and> z \<in> circline_set H'
[PROOF STEP]
using * \<open>unit_disc_fix M\<close>
[PROOF STATE]
proof (prove)
using this:
is_poincare_line H'
perpendicular (moebius_circline M H) H'
moebius_pt M z \<in> circline_set H'
unit_disc_fix M

goal (1 subgoal):
 1. \<exists>H'. is_poincare_line H' \<and> perpendicular H H' \<and> z \<in> circline_set H'
[PROOF STEP]
apply (subst h)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_poincare_line H'; perpendicular (moebius_circline M H) H'; moebius_pt M z \<in> circline_set H'; unit_disc_fix M\<rbrakk> \<Longrightarrow> \<exists>H'. is_poincare_line H' \<and> perpendicular (moebius_circline (- M) (moebius_circline M H)) H' \<and> z \<in> circline_set H'
[PROOF STEP]
apply (rule_tac x="moebius_circline (-M) H'" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_poincare_line H'; perpendicular (moebius_circline M H) H'; moebius_pt M z \<in> circline_set H'; unit_disc_fix M\<rbrakk> \<Longrightarrow> is_poincare_line (moebius_circline (- M) H') \<and> perpendicular (moebius_circline (- M) (moebius_circline M H)) (moebius_circline (- M) H') \<and> z \<in> circline_set (moebius_circline (- M) H')
[PROOF STEP]
apply (simp del: moebius_circline_comp_inv_left)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>H'. is_poincare_line H' \<and> perpendicular H H' \<and> z \<in> circline_set H'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>z. z \<in> unit_disc \<longrightarrow> (\<exists>H'. is_poincare_line H' \<and> perpendicular H H' \<and> z \<in> circline_set H')

goal (1 subgoal):
 1. is_poincare_line H
[PROOF STEP]
qed fact
[PROOF STATE]
proof (state)
this:
\<forall>z. z \<in> unit_disc \<longrightarrow> (\<exists>H'. is_poincare_line H' \<and> perpendicular H H' \<and> z \<in> circline_set H')

goal (1 subgoal):
 1. \<exists>H'. is_poincare_line H' \<and> perpendicular H H' \<and> z \<in> circline_set H'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>z. z \<in> unit_disc \<longrightarrow> (\<exists>H'. is_poincare_line H' \<and> perpendicular H H' \<and> z \<in> circline_set H')

goal (1 subgoal):
 1. \<exists>H'. is_poincare_line H' \<and> perpendicular H H' \<and> z \<in> circline_set H'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>z. z \<in> unit_disc \<longrightarrow> (\<exists>H'. is_poincare_line H' \<and> perpendicular H H' \<and> z \<in> circline_set H')
is_poincare_line H
z \<in> unit_disc

goal (1 subgoal):
 1. \<exists>H'. is_poincare_line H' \<and> perpendicular H H' \<and> z \<in> circline_set H'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>H'. is_poincare_line H' \<and> perpendicular H H' \<and> z \<in> circline_set H'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ex_perpendicular_foot:
  assumes "is_poincare_line H" "z \<in> unit_disc"
  shows "\<exists> H'. is_poincare_line H' \<and> z \<in> circline_set H' \<and> perpendicular H H' \<and>
              (\<exists> z' \<in> unit_disc. z' \<in> circline_set H' \<inter> circline_set H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>H'. is_poincare_line H' \<and> z \<in> circline_set H' \<and> perpendicular H H' \<and> (\<exists>z'\<in>unit_disc. z' \<in> circline_set H' \<inter> circline_set H)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_poincare_line H
z \<in> unit_disc

goal (1 subgoal):
 1. \<exists>H'. is_poincare_line H' \<and> z \<in> circline_set H' \<and> perpendicular H H' \<and> (\<exists>z'\<in>unit_disc. z' \<in> circline_set H' \<inter> circline_set H)
[PROOF STEP]
using ex_perpendicular[OF assms]
[PROOF STATE]
proof (prove)
using this:
is_poincare_line H
z \<in> unit_disc
\<exists>H'. is_poincare_line H' \<and> perpendicular H H' \<and> z \<in> circline_set H'

goal (1 subgoal):
 1. \<exists>H'. is_poincare_line H' \<and> z \<in> circline_set H' \<and> perpendicular H H' \<and> (\<exists>z'\<in>unit_disc. z' \<in> circline_set H' \<inter> circline_set H)
[PROOF STEP]
using perpendicular_intersects[of H]
[PROOF STATE]
proof (prove)
using this:
is_poincare_line H
z \<in> unit_disc
\<exists>H'. is_poincare_line H' \<and> perpendicular H H' \<and> z \<in> circline_set H'
\<lbrakk>is_poincare_line H; is_poincare_line ?H2.0; perpendicular H ?H2.0\<rbrakk> \<Longrightarrow> \<exists>z. z \<in> unit_disc \<and> z \<in> circline_set H \<inter> circline_set ?H2.0

goal (1 subgoal):
 1. \<exists>H'. is_poincare_line H' \<and> z \<in> circline_set H' \<and> perpendicular H H' \<and> (\<exists>z'\<in>unit_disc. z' \<in> circline_set H' \<inter> circline_set H)
[PROOF STEP]
by blast


[STATEMENT]
lemma Pythagoras:
  assumes in_disc: "u \<in> unit_disc" "v \<in> unit_disc" "w \<in> unit_disc" "v \<noteq> w"
  assumes "distinct[u, v, w] \<longrightarrow> perpendicular (poincare_line u v) (poincare_line u w)"
  shows "cosh (poincare_distance v w) = cosh (poincare_distance u v) * cosh (poincare_distance u w)" (is "?P' u v w")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cosh_dist v w = cosh_dist u v * cosh_dist u w
[PROOF STEP]
proof (cases "distinct [u, v, w]")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. distinct [u, v, w] \<Longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
 2. \<not> distinct [u, v, w] \<Longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> distinct [u, v, w]

goal (2 subgoals):
 1. distinct [u, v, w] \<Longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
 2. \<not> distinct [u, v, w] \<Longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
[PROOF STEP]
thus "?thesis"
[PROOF STATE]
proof (prove)
using this:
\<not> distinct [u, v, w]

goal (1 subgoal):
 1. cosh_dist v w = cosh_dist u v * cosh_dist u w
[PROOF STEP]
using in_disc
[PROOF STATE]
proof (prove)
using this:
\<not> distinct [u, v, w]
u \<in> unit_disc
v \<in> unit_disc
w \<in> unit_disc
v \<noteq> w

goal (1 subgoal):
 1. cosh_dist v w = cosh_dist u v * cosh_dist u w
[PROOF STEP]
by (auto simp add: poincare_distance_sym)
[PROOF STATE]
proof (state)
this:
cosh_dist v w = cosh_dist u v * cosh_dist u w

goal (1 subgoal):
 1. distinct [u, v, w] \<Longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. distinct [u, v, w] \<Longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
distinct [u, v, w]

goal (1 subgoal):
 1. distinct [u, v, w] \<Longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
[PROOF STEP]
have "distinct [u, v, w] \<longrightarrow> ?P' u v w" (is "?P u v w")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
[PROOF STEP]
proof (rule wlog_perpendicular_axes[where P="?P"])
[PROOF STATE]
proof (state)
goal (12 subgoals):
 1. v \<in> unit_disc
 2. w \<in> unit_disc
 3. u \<in> unit_disc
 4. is_poincare_line ?H1.0
 5. is_poincare_line ?H2.0
 6. perpendicular ?H1.0 ?H2.0
 7. u \<in> circline_set ?H1.0 \<inter> circline_set ?H2.0
 8. v \<in> circline_set ?H1.0
 9. w \<in> circline_set ?H2.0
 10. \<And>x y. \<lbrakk>is_real x; 0 \<le> Re x; Re x < 1; is_imag y; 0 \<le> Im y; Im y < 1\<rbrakk> \<Longrightarrow> distinct [0\<^sub>h, of_complex x, of_complex y] \<longrightarrow> cosh_dist (of_complex x) (of_complex y) = cosh_dist 0\<^sub>h (of_complex x) * cosh_dist 0\<^sub>h (of_complex y)
A total of 12 subgoals...
[PROOF STEP]
show "is_poincare_line (poincare_line u v)" "is_poincare_line (poincare_line u w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_poincare_line (poincare_line u v) &&& is_poincare_line (poincare_line u w)
[PROOF STEP]
using \<open>distinct [u, v, w]\<close>
[PROOF STATE]
proof (prove)
using this:
distinct [u, v, w]

goal (1 subgoal):
 1. is_poincare_line (poincare_line u v) &&& is_poincare_line (poincare_line u w)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
is_poincare_line (poincare_line u v)
is_poincare_line (poincare_line u w)

goal (10 subgoals):
 1. v \<in> unit_disc
 2. w \<in> unit_disc
 3. u \<in> unit_disc
 4. perpendicular (poincare_line u v) (poincare_line u w)
 5. u \<in> circline_set (poincare_line u v) \<inter> circline_set (poincare_line u w)
 6. v \<in> circline_set (poincare_line u v)
 7. w \<in> circline_set (poincare_line u w)
 8. \<And>x y. \<lbrakk>is_real x; 0 \<le> Re x; Re x < 1; is_imag y; 0 \<le> Im y; Im y < 1\<rbrakk> \<Longrightarrow> distinct [0\<^sub>h, of_complex x, of_complex y] \<longrightarrow> cosh_dist (of_complex x) (of_complex y) = cosh_dist 0\<^sub>h (of_complex x) * cosh_dist 0\<^sub>h (of_complex y)
 9. \<And>M u v w. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; distinct [moebius_pt M u, moebius_pt M v, moebius_pt M w] \<longrightarrow> cosh_dist (moebius_pt M v) (moebius_pt M w) = cosh_dist (moebius_pt M u) (moebius_pt M v) * cosh_dist (moebius_pt M u) (moebius_pt M w)\<rbrakk> \<Longrightarrow> distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
 10. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; distinct [conjugate u, conjugate v, conjugate w] \<longrightarrow> cosh_dist (conjugate v) (conjugate w) = cosh_dist (conjugate u) (conjugate v) * cosh_dist (conjugate u) (conjugate w)\<rbrakk> \<Longrightarrow> distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. v \<in> unit_disc
 2. w \<in> unit_disc
 3. u \<in> unit_disc
 4. perpendicular (poincare_line u v) (poincare_line u w)
 5. u \<in> circline_set (poincare_line u v) \<inter> circline_set (poincare_line u w)
 6. v \<in> circline_set (poincare_line u v)
 7. w \<in> circline_set (poincare_line u w)
 8. \<And>x y. \<lbrakk>is_real x; 0 \<le> Re x; Re x < 1; is_imag y; 0 \<le> Im y; Im y < 1\<rbrakk> \<Longrightarrow> distinct [0\<^sub>h, of_complex x, of_complex y] \<longrightarrow> cosh_dist (of_complex x) (of_complex y) = cosh_dist 0\<^sub>h (of_complex x) * cosh_dist 0\<^sub>h (of_complex y)
 9. \<And>M u v w. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; distinct [moebius_pt M u, moebius_pt M v, moebius_pt M w] \<longrightarrow> cosh_dist (moebius_pt M v) (moebius_pt M w) = cosh_dist (moebius_pt M u) (moebius_pt M v) * cosh_dist (moebius_pt M u) (moebius_pt M w)\<rbrakk> \<Longrightarrow> distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
 10. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; distinct [conjugate u, conjugate v, conjugate w] \<longrightarrow> cosh_dist (conjugate v) (conjugate w) = cosh_dist (conjugate u) (conjugate v) * cosh_dist (conjugate u) (conjugate w)\<rbrakk> \<Longrightarrow> distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
[PROOF STEP]
show "perpendicular (poincare_line u v) (poincare_line u w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. perpendicular (poincare_line u v) (poincare_line u w)
[PROOF STEP]
using True assms
[PROOF STATE]
proof (prove)
using this:
distinct [u, v, w]
u \<in> unit_disc
v \<in> unit_disc
w \<in> unit_disc
v \<noteq> w
distinct [u, v, w] \<longrightarrow> perpendicular (poincare_line u v) (poincare_line u w)

goal (1 subgoal):
 1. perpendicular (poincare_line u v) (poincare_line u w)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
perpendicular (poincare_line u v) (poincare_line u w)

goal (9 subgoals):
 1. v \<in> unit_disc
 2. w \<in> unit_disc
 3. u \<in> unit_disc
 4. u \<in> circline_set (poincare_line u v) \<inter> circline_set (poincare_line u w)
 5. v \<in> circline_set (poincare_line u v)
 6. w \<in> circline_set (poincare_line u w)
 7. \<And>x y. \<lbrakk>is_real x; 0 \<le> Re x; Re x < 1; is_imag y; 0 \<le> Im y; Im y < 1\<rbrakk> \<Longrightarrow> distinct [0\<^sub>h, of_complex x, of_complex y] \<longrightarrow> cosh_dist (of_complex x) (of_complex y) = cosh_dist 0\<^sub>h (of_complex x) * cosh_dist 0\<^sub>h (of_complex y)
 8. \<And>M u v w. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; distinct [moebius_pt M u, moebius_pt M v, moebius_pt M w] \<longrightarrow> cosh_dist (moebius_pt M v) (moebius_pt M w) = cosh_dist (moebius_pt M u) (moebius_pt M v) * cosh_dist (moebius_pt M u) (moebius_pt M w)\<rbrakk> \<Longrightarrow> distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
 9. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; distinct [conjugate u, conjugate v, conjugate w] \<longrightarrow> cosh_dist (conjugate v) (conjugate w) = cosh_dist (conjugate u) (conjugate v) * cosh_dist (conjugate u) (conjugate w)\<rbrakk> \<Longrightarrow> distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. v \<in> unit_disc
 2. w \<in> unit_disc
 3. u \<in> unit_disc
 4. u \<in> circline_set (poincare_line u v) \<inter> circline_set (poincare_line u w)
 5. v \<in> circline_set (poincare_line u v)
 6. w \<in> circline_set (poincare_line u w)
 7. \<And>x y. \<lbrakk>is_real x; 0 \<le> Re x; Re x < 1; is_imag y; 0 \<le> Im y; Im y < 1\<rbrakk> \<Longrightarrow> distinct [0\<^sub>h, of_complex x, of_complex y] \<longrightarrow> cosh_dist (of_complex x) (of_complex y) = cosh_dist 0\<^sub>h (of_complex x) * cosh_dist 0\<^sub>h (of_complex y)
 8. \<And>M u v w. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; distinct [moebius_pt M u, moebius_pt M v, moebius_pt M w] \<longrightarrow> cosh_dist (moebius_pt M v) (moebius_pt M w) = cosh_dist (moebius_pt M u) (moebius_pt M v) * cosh_dist (moebius_pt M u) (moebius_pt M w)\<rbrakk> \<Longrightarrow> distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
 9. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; distinct [conjugate u, conjugate v, conjugate w] \<longrightarrow> cosh_dist (conjugate v) (conjugate w) = cosh_dist (conjugate u) (conjugate v) * cosh_dist (conjugate u) (conjugate w)\<rbrakk> \<Longrightarrow> distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
[PROOF STEP]
show "u \<in> unit_disc" "v \<in> unit_disc" "w \<in> unit_disc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<in> unit_disc &&& v \<in> unit_disc &&& w \<in> unit_disc
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
u \<in> unit_disc
v \<in> unit_disc
w \<in> unit_disc

goal (6 subgoals):
 1. u \<in> circline_set (poincare_line u v) \<inter> circline_set (poincare_line u w)
 2. v \<in> circline_set (poincare_line u v)
 3. w \<in> circline_set (poincare_line u w)
 4. \<And>x y. \<lbrakk>is_real x; 0 \<le> Re x; Re x < 1; is_imag y; 0 \<le> Im y; Im y < 1\<rbrakk> \<Longrightarrow> distinct [0\<^sub>h, of_complex x, of_complex y] \<longrightarrow> cosh_dist (of_complex x) (of_complex y) = cosh_dist 0\<^sub>h (of_complex x) * cosh_dist 0\<^sub>h (of_complex y)
 5. \<And>M u v w. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; distinct [moebius_pt M u, moebius_pt M v, moebius_pt M w] \<longrightarrow> cosh_dist (moebius_pt M v) (moebius_pt M w) = cosh_dist (moebius_pt M u) (moebius_pt M v) * cosh_dist (moebius_pt M u) (moebius_pt M w)\<rbrakk> \<Longrightarrow> distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
 6. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; distinct [conjugate u, conjugate v, conjugate w] \<longrightarrow> cosh_dist (conjugate v) (conjugate w) = cosh_dist (conjugate u) (conjugate v) * cosh_dist (conjugate u) (conjugate w)\<rbrakk> \<Longrightarrow> distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. u \<in> circline_set (poincare_line u v) \<inter> circline_set (poincare_line u w)
 2. v \<in> circline_set (poincare_line u v)
 3. w \<in> circline_set (poincare_line u w)
 4. \<And>x y. \<lbrakk>is_real x; 0 \<le> Re x; Re x < 1; is_imag y; 0 \<le> Im y; Im y < 1\<rbrakk> \<Longrightarrow> distinct [0\<^sub>h, of_complex x, of_complex y] \<longrightarrow> cosh_dist (of_complex x) (of_complex y) = cosh_dist 0\<^sub>h (of_complex x) * cosh_dist 0\<^sub>h (of_complex y)
 5. \<And>M u v w. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; distinct [moebius_pt M u, moebius_pt M v, moebius_pt M w] \<longrightarrow> cosh_dist (moebius_pt M v) (moebius_pt M w) = cosh_dist (moebius_pt M u) (moebius_pt M v) * cosh_dist (moebius_pt M u) (moebius_pt M w)\<rbrakk> \<Longrightarrow> distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
 6. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; distinct [conjugate u, conjugate v, conjugate w] \<longrightarrow> cosh_dist (conjugate v) (conjugate w) = cosh_dist (conjugate u) (conjugate v) * cosh_dist (conjugate u) (conjugate w)\<rbrakk> \<Longrightarrow> distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
[PROOF STEP]
show "v \<in> circline_set (poincare_line u v)" "w \<in> circline_set (poincare_line u w)"
         "u \<in> circline_set (poincare_line u v) \<inter> circline_set (poincare_line u w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> circline_set (poincare_line u v) &&& w \<in> circline_set (poincare_line u w) &&& u \<in> circline_set (poincare_line u v) \<inter> circline_set (poincare_line u w)
[PROOF STEP]
using \<open>distinct [u, v, w]\<close>
[PROOF STATE]
proof (prove)
using this:
distinct [u, v, w]

goal (1 subgoal):
 1. v \<in> circline_set (poincare_line u v) &&& w \<in> circline_set (poincare_line u w) &&& u \<in> circline_set (poincare_line u v) \<inter> circline_set (poincare_line u w)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v \<in> circline_set (poincare_line u v)
w \<in> circline_set (poincare_line u w)
u \<in> circline_set (poincare_line u v) \<inter> circline_set (poincare_line u w)

goal (3 subgoals):
 1. \<And>x y. \<lbrakk>is_real x; 0 \<le> Re x; Re x < 1; is_imag y; 0 \<le> Im y; Im y < 1\<rbrakk> \<Longrightarrow> distinct [0\<^sub>h, of_complex x, of_complex y] \<longrightarrow> cosh_dist (of_complex x) (of_complex y) = cosh_dist 0\<^sub>h (of_complex x) * cosh_dist 0\<^sub>h (of_complex y)
 2. \<And>M u v w. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; distinct [moebius_pt M u, moebius_pt M v, moebius_pt M w] \<longrightarrow> cosh_dist (moebius_pt M v) (moebius_pt M w) = cosh_dist (moebius_pt M u) (moebius_pt M v) * cosh_dist (moebius_pt M u) (moebius_pt M w)\<rbrakk> \<Longrightarrow> distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
 3. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; distinct [conjugate u, conjugate v, conjugate w] \<longrightarrow> cosh_dist (conjugate v) (conjugate w) = cosh_dist (conjugate u) (conjugate v) * cosh_dist (conjugate u) (conjugate w)\<rbrakk> \<Longrightarrow> distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>is_real x; 0 \<le> Re x; Re x < 1; is_imag y; 0 \<le> Im y; Im y < 1\<rbrakk> \<Longrightarrow> distinct [0\<^sub>h, of_complex x, of_complex y] \<longrightarrow> cosh_dist (of_complex x) (of_complex y) = cosh_dist 0\<^sub>h (of_complex x) * cosh_dist 0\<^sub>h (of_complex y)
 2. \<And>M u v w. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; distinct [moebius_pt M u, moebius_pt M v, moebius_pt M w] \<longrightarrow> cosh_dist (moebius_pt M v) (moebius_pt M w) = cosh_dist (moebius_pt M u) (moebius_pt M v) * cosh_dist (moebius_pt M u) (moebius_pt M w)\<rbrakk> \<Longrightarrow> distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
 3. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; distinct [conjugate u, conjugate v, conjugate w] \<longrightarrow> cosh_dist (conjugate v) (conjugate w) = cosh_dist (conjugate u) (conjugate v) * cosh_dist (conjugate u) (conjugate w)\<rbrakk> \<Longrightarrow> distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>is_real x; 0 \<le> Re x; Re x < 1; is_imag y; 0 \<le> Im y; Im y < 1\<rbrakk> \<Longrightarrow> distinct [0\<^sub>h, of_complex x, of_complex y] \<longrightarrow> cosh_dist (of_complex x) (of_complex y) = cosh_dist 0\<^sub>h (of_complex x) * cosh_dist 0\<^sub>h (of_complex y)
 2. \<And>M u v w. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; distinct [moebius_pt M u, moebius_pt M v, moebius_pt M w] \<longrightarrow> cosh_dist (moebius_pt M v) (moebius_pt M w) = cosh_dist (moebius_pt M u) (moebius_pt M v) * cosh_dist (moebius_pt M u) (moebius_pt M w)\<rbrakk> \<Longrightarrow> distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
 3. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; distinct [conjugate u, conjugate v, conjugate w] \<longrightarrow> cosh_dist (conjugate v) (conjugate w) = cosh_dist (conjugate u) (conjugate v) * cosh_dist (conjugate u) (conjugate w)\<rbrakk> \<Longrightarrow> distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
[PROOF STEP]
assume x: "is_real x" "0 \<le> Re x" "Re x < 1"
[PROOF STATE]
proof (state)
this:
is_real x
0 \<le> Re x
Re x < 1

goal (3 subgoals):
 1. \<And>x y. \<lbrakk>is_real x; 0 \<le> Re x; Re x < 1; is_imag y; 0 \<le> Im y; Im y < 1\<rbrakk> \<Longrightarrow> distinct [0\<^sub>h, of_complex x, of_complex y] \<longrightarrow> cosh_dist (of_complex x) (of_complex y) = cosh_dist 0\<^sub>h (of_complex x) * cosh_dist 0\<^sub>h (of_complex y)
 2. \<And>M u v w. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; distinct [moebius_pt M u, moebius_pt M v, moebius_pt M w] \<longrightarrow> cosh_dist (moebius_pt M v) (moebius_pt M w) = cosh_dist (moebius_pt M u) (moebius_pt M v) * cosh_dist (moebius_pt M u) (moebius_pt M w)\<rbrakk> \<Longrightarrow> distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
 3. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; distinct [conjugate u, conjugate v, conjugate w] \<longrightarrow> cosh_dist (conjugate v) (conjugate w) = cosh_dist (conjugate u) (conjugate v) * cosh_dist (conjugate u) (conjugate w)\<rbrakk> \<Longrightarrow> distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
[PROOF STEP]
assume y: "is_imag y" "0 \<le> Im y" "Im y < 1"
[PROOF STATE]
proof (state)
this:
is_imag y
0 \<le> Im y
Im y < 1

goal (3 subgoals):
 1. \<And>x y. \<lbrakk>is_real x; 0 \<le> Re x; Re x < 1; is_imag y; 0 \<le> Im y; Im y < 1\<rbrakk> \<Longrightarrow> distinct [0\<^sub>h, of_complex x, of_complex y] \<longrightarrow> cosh_dist (of_complex x) (of_complex y) = cosh_dist 0\<^sub>h (of_complex x) * cosh_dist 0\<^sub>h (of_complex y)
 2. \<And>M u v w. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; distinct [moebius_pt M u, moebius_pt M v, moebius_pt M w] \<longrightarrow> cosh_dist (moebius_pt M v) (moebius_pt M w) = cosh_dist (moebius_pt M u) (moebius_pt M v) * cosh_dist (moebius_pt M u) (moebius_pt M w)\<rbrakk> \<Longrightarrow> distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
 3. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; distinct [conjugate u, conjugate v, conjugate w] \<longrightarrow> cosh_dist (conjugate v) (conjugate w) = cosh_dist (conjugate u) (conjugate v) * cosh_dist (conjugate u) (conjugate w)\<rbrakk> \<Longrightarrow> distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
[PROOF STEP]
have "of_complex x \<in> unit_disc" "of_complex y \<in> unit_disc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_complex x \<in> unit_disc &&& of_complex y \<in> unit_disc
[PROOF STEP]
using x y
[PROOF STATE]
proof (prove)
using this:
is_real x
0 \<le> Re x
Re x < 1
is_imag y
0 \<le> Im y
Im y < 1

goal (1 subgoal):
 1. of_complex x \<in> unit_disc &&& of_complex y \<in> unit_disc
[PROOF STEP]
by (simp_all add: cmod_eq_Re cmod_eq_Im)
[PROOF STATE]
proof (state)
this:
of_complex x \<in> unit_disc
of_complex y \<in> unit_disc

goal (3 subgoals):
 1. \<And>x y. \<lbrakk>is_real x; 0 \<le> Re x; Re x < 1; is_imag y; 0 \<le> Im y; Im y < 1\<rbrakk> \<Longrightarrow> distinct [0\<^sub>h, of_complex x, of_complex y] \<longrightarrow> cosh_dist (of_complex x) (of_complex y) = cosh_dist 0\<^sub>h (of_complex x) * cosh_dist 0\<^sub>h (of_complex y)
 2. \<And>M u v w. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; distinct [moebius_pt M u, moebius_pt M v, moebius_pt M w] \<longrightarrow> cosh_dist (moebius_pt M v) (moebius_pt M w) = cosh_dist (moebius_pt M u) (moebius_pt M v) * cosh_dist (moebius_pt M u) (moebius_pt M w)\<rbrakk> \<Longrightarrow> distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
 3. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; distinct [conjugate u, conjugate v, conjugate w] \<longrightarrow> cosh_dist (conjugate v) (conjugate w) = cosh_dist (conjugate u) (conjugate v) * cosh_dist (conjugate u) (conjugate w)\<rbrakk> \<Longrightarrow> distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
[PROOF STEP]
show "?P 0\<^sub>h (of_complex x) (of_complex y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct [0\<^sub>h, of_complex x, of_complex y] \<longrightarrow> cosh_dist (of_complex x) (of_complex y) = cosh_dist 0\<^sub>h (of_complex x) * cosh_dist 0\<^sub>h (of_complex y)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. distinct [0\<^sub>h, of_complex x, of_complex y] \<Longrightarrow> cosh_dist (of_complex x) (of_complex y) = cosh_dist 0\<^sub>h (of_complex x) * cosh_dist 0\<^sub>h (of_complex y)
[PROOF STEP]
assume "distinct [0\<^sub>h, of_complex x, of_complex y]"
[PROOF STATE]
proof (state)
this:
distinct [0\<^sub>h, of_complex x, of_complex y]

goal (1 subgoal):
 1. distinct [0\<^sub>h, of_complex x, of_complex y] \<Longrightarrow> cosh_dist (of_complex x) (of_complex y) = cosh_dist 0\<^sub>h (of_complex x) * cosh_dist 0\<^sub>h (of_complex y)
[PROOF STEP]
hence "x \<noteq> 0" "y \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
distinct [0\<^sub>h, of_complex x, of_complex y]

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

goal (1 subgoal):
 1. distinct [0\<^sub>h, of_complex x, of_complex y] \<Longrightarrow> cosh_dist (of_complex x) (of_complex y) = cosh_dist 0\<^sub>h (of_complex x) * cosh_dist 0\<^sub>h (of_complex y)
[PROOF STEP]
let ?den1 = "1 - (cmod x)\<^sup>2" and ?den2 = "1 - (cmod y)\<^sup>2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. distinct [0\<^sub>h, of_complex x, of_complex y] \<Longrightarrow> cosh_dist (of_complex x) (of_complex y) = cosh_dist 0\<^sub>h (of_complex x) * cosh_dist 0\<^sub>h (of_complex y)
[PROOF STEP]
have "?den1 > 0" "?den2 > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < 1 - (cmod x)\<^sup>2 &&& 0 < 1 - (cmod y)\<^sup>2
[PROOF STEP]
using x y
[PROOF STATE]
proof (prove)
using this:
is_real x
0 \<le> Re x
Re x < 1
is_imag y
0 \<le> Im y
Im y < 1

goal (1 subgoal):
 1. 0 < 1 - (cmod x)\<^sup>2 &&& 0 < 1 - (cmod y)\<^sup>2
[PROOF STEP]
by (simp_all add: cmod_eq_Re cmod_eq_Im abs_square_less_1)
[PROOF STATE]
proof (state)
this:
0 < 1 - (cmod x)\<^sup>2
0 < 1 - (cmod y)\<^sup>2

goal (1 subgoal):
 1. distinct [0\<^sub>h, of_complex x, of_complex y] \<Longrightarrow> cosh_dist (of_complex x) (of_complex y) = cosh_dist 0\<^sub>h (of_complex x) * cosh_dist 0\<^sub>h (of_complex y)
[PROOF STEP]
let ?d1 = "1 + 2 * (cmod x)\<^sup>2 / ?den1"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. distinct [0\<^sub>h, of_complex x, of_complex y] \<Longrightarrow> cosh_dist (of_complex x) (of_complex y) = cosh_dist 0\<^sub>h (of_complex x) * cosh_dist 0\<^sub>h (of_complex y)
[PROOF STEP]
have "cosh (poincare_distance 0\<^sub>h (of_complex x)) = ?d1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cosh_dist 0\<^sub>h (of_complex x) = 1 + 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)
[PROOF STEP]
using \<open>?den1 > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < 1 - (cmod x)\<^sup>2

goal (1 subgoal):
 1. cosh_dist 0\<^sub>h (of_complex x) = 1 + 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)
[PROOF STEP]
using poincare_distance_formula[of "0\<^sub>h" "of_complex x"] \<open>of_complex x \<in> unit_disc\<close>
[PROOF STATE]
proof (prove)
using this:
0 < 1 - (cmod x)\<^sup>2
\<lbrakk>0\<^sub>h \<in> unit_disc; of_complex x \<in> unit_disc\<rbrakk> \<Longrightarrow> poincare_distance 0\<^sub>h (of_complex x) = poincare_distance_formula (to_complex 0\<^sub>h) (to_complex (of_complex x))
of_complex x \<in> unit_disc

goal (1 subgoal):
 1. cosh_dist 0\<^sub>h (of_complex x) = 1 + 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cosh_dist 0\<^sub>h (of_complex x) = 1 + 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)

goal (1 subgoal):
 1. distinct [0\<^sub>h, of_complex x, of_complex y] \<Longrightarrow> cosh_dist (of_complex x) (of_complex y) = cosh_dist 0\<^sub>h (of_complex x) * cosh_dist 0\<^sub>h (of_complex y)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cosh_dist 0\<^sub>h (of_complex x) = 1 + 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)

goal (1 subgoal):
 1. distinct [0\<^sub>h, of_complex x, of_complex y] \<Longrightarrow> cosh_dist (of_complex x) (of_complex y) = cosh_dist 0\<^sub>h (of_complex x) * cosh_dist 0\<^sub>h (of_complex y)
[PROOF STEP]
let ?d2 = "1 + 2 * (cmod y)\<^sup>2 / ?den2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. distinct [0\<^sub>h, of_complex x, of_complex y] \<Longrightarrow> cosh_dist (of_complex x) (of_complex y) = cosh_dist 0\<^sub>h (of_complex x) * cosh_dist 0\<^sub>h (of_complex y)
[PROOF STEP]
have "cosh (poincare_distance 0\<^sub>h (of_complex y)) = ?d2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cosh_dist 0\<^sub>h (of_complex y) = 1 + 2 * (cmod y)\<^sup>2 / (1 - (cmod y)\<^sup>2)
[PROOF STEP]
using \<open>?den2 > 0\<close> \<open>of_complex y \<in> unit_disc\<close>
[PROOF STATE]
proof (prove)
using this:
0 < 1 - (cmod y)\<^sup>2
of_complex y \<in> unit_disc

goal (1 subgoal):
 1. cosh_dist 0\<^sub>h (of_complex y) = 1 + 2 * (cmod y)\<^sup>2 / (1 - (cmod y)\<^sup>2)
[PROOF STEP]
using poincare_distance_formula[of "0\<^sub>h" "of_complex y"]
[PROOF STATE]
proof (prove)
using this:
0 < 1 - (cmod y)\<^sup>2
of_complex y \<in> unit_disc
\<lbrakk>0\<^sub>h \<in> unit_disc; of_complex y \<in> unit_disc\<rbrakk> \<Longrightarrow> poincare_distance 0\<^sub>h (of_complex y) = poincare_distance_formula (to_complex 0\<^sub>h) (to_complex (of_complex y))

goal (1 subgoal):
 1. cosh_dist 0\<^sub>h (of_complex y) = 1 + 2 * (cmod y)\<^sup>2 / (1 - (cmod y)\<^sup>2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cosh_dist 0\<^sub>h (of_complex y) = 1 + 2 * (cmod y)\<^sup>2 / (1 - (cmod y)\<^sup>2)

goal (1 subgoal):
 1. distinct [0\<^sub>h, of_complex x, of_complex y] \<Longrightarrow> cosh_dist (of_complex x) (of_complex y) = cosh_dist 0\<^sub>h (of_complex x) * cosh_dist 0\<^sub>h (of_complex y)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cosh_dist 0\<^sub>h (of_complex y) = 1 + 2 * (cmod y)\<^sup>2 / (1 - (cmod y)\<^sup>2)

goal (1 subgoal):
 1. distinct [0\<^sub>h, of_complex x, of_complex y] \<Longrightarrow> cosh_dist (of_complex x) (of_complex y) = cosh_dist 0\<^sub>h (of_complex x) * cosh_dist 0\<^sub>h (of_complex y)
[PROOF STEP]
let ?den = "?den1 * ?den2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. distinct [0\<^sub>h, of_complex x, of_complex y] \<Longrightarrow> cosh_dist (of_complex x) (of_complex y) = cosh_dist 0\<^sub>h (of_complex x) * cosh_dist 0\<^sub>h (of_complex y)
[PROOF STEP]
let ?d3 = "1 + 2 * (cmod (x - y))\<^sup>2 / ?den"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. distinct [0\<^sub>h, of_complex x, of_complex y] \<Longrightarrow> cosh_dist (of_complex x) (of_complex y) = cosh_dist 0\<^sub>h (of_complex x) * cosh_dist 0\<^sub>h (of_complex y)
[PROOF STEP]
have "cosh (poincare_distance (of_complex x) (of_complex y)) = ?d3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cosh_dist (of_complex x) (of_complex y) = 1 + 2 * (cmod (x - y))\<^sup>2 / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2))
[PROOF STEP]
using \<open>of_complex x \<in> unit_disc\<close> \<open>of_complex y \<in> unit_disc\<close>
[PROOF STATE]
proof (prove)
using this:
of_complex x \<in> unit_disc
of_complex y \<in> unit_disc

goal (1 subgoal):
 1. cosh_dist (of_complex x) (of_complex y) = 1 + 2 * (cmod (x - y))\<^sup>2 / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2))
[PROOF STEP]
using \<open>?den1 > 0\<close> \<open>?den2 > 0\<close>
[PROOF STATE]
proof (prove)
using this:
of_complex x \<in> unit_disc
of_complex y \<in> unit_disc
0 < 1 - (cmod x)\<^sup>2
0 < 1 - (cmod y)\<^sup>2

goal (1 subgoal):
 1. cosh_dist (of_complex x) (of_complex y) = 1 + 2 * (cmod (x - y))\<^sup>2 / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2))
[PROOF STEP]
using poincare_distance_formula[of "of_complex x" "of_complex y"]
[PROOF STATE]
proof (prove)
using this:
of_complex x \<in> unit_disc
of_complex y \<in> unit_disc
0 < 1 - (cmod x)\<^sup>2
0 < 1 - (cmod y)\<^sup>2
\<lbrakk>of_complex x \<in> unit_disc; of_complex y \<in> unit_disc\<rbrakk> \<Longrightarrow> poincare_distance (of_complex x) (of_complex y) = poincare_distance_formula (to_complex (of_complex x)) (to_complex (of_complex y))

goal (1 subgoal):
 1. cosh_dist (of_complex x) (of_complex y) = 1 + 2 * (cmod (x - y))\<^sup>2 / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cosh_dist (of_complex x) (of_complex y) = 1 + 2 * (cmod (x - y))\<^sup>2 / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2))

goal (1 subgoal):
 1. distinct [0\<^sub>h, of_complex x, of_complex y] \<Longrightarrow> cosh_dist (of_complex x) (of_complex y) = cosh_dist 0\<^sub>h (of_complex x) * cosh_dist 0\<^sub>h (of_complex y)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cosh_dist (of_complex x) (of_complex y) = 1 + 2 * (cmod (x - y))\<^sup>2 / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2))

goal (1 subgoal):
 1. distinct [0\<^sub>h, of_complex x, of_complex y] \<Longrightarrow> cosh_dist (of_complex x) (of_complex y) = cosh_dist 0\<^sub>h (of_complex x) * cosh_dist 0\<^sub>h (of_complex y)
[PROOF STEP]
have "?d1 * ?d2 = ?d3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 + 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)) * (1 + 2 * (cmod y)\<^sup>2 / (1 - (cmod y)\<^sup>2)) = 1 + 2 * (cmod (x - y))\<^sup>2 / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (1 + 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)) * (1 + 2 * (cmod y)\<^sup>2 / (1 - (cmod y)\<^sup>2)) = 1 + 2 * (cmod (x - y))\<^sup>2 / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2))
[PROOF STEP]
have "?d3 = ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2) + 2 * (cmod (x - y))\<^sup>2) / ?den"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 + 2 * (cmod (x - y))\<^sup>2 / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2)) = ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2) + 2 * (cmod (x - y))\<^sup>2) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2))
[PROOF STEP]
using \<open>?den1 > 0\<close> \<open>?den2 > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < 1 - (cmod x)\<^sup>2
0 < 1 - (cmod y)\<^sup>2

goal (1 subgoal):
 1. 1 + 2 * (cmod (x - y))\<^sup>2 / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2)) = ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2) + 2 * (cmod (x - y))\<^sup>2) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2))
[PROOF STEP]
by (subst add_num_frac, simp, simp)
[PROOF STATE]
proof (state)
this:
1 + 2 * (cmod (x - y))\<^sup>2 / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2)) = ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2) + 2 * (cmod (x - y))\<^sup>2) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2))

goal (1 subgoal):
 1. (1 + 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)) * (1 + 2 * (cmod y)\<^sup>2 / (1 - (cmod y)\<^sup>2)) = 1 + 2 * (cmod (x - y))\<^sup>2 / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 + 2 * (cmod (x - y))\<^sup>2 / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2)) = ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2) + 2 * (cmod (x - y))\<^sup>2) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2))

goal (1 subgoal):
 1. (1 + 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)) * (1 + 2 * (cmod y)\<^sup>2 / (1 - (cmod y)\<^sup>2)) = 1 + 2 * (cmod (x - y))\<^sup>2 / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2))
[PROOF STEP]
have "... = (Re ((1 - x * cnj x) * (1 - y * cnj y) + 2 * (x - y)*cnj (x - y)) / ?den)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2) + 2 * (cmod (x - y))\<^sup>2) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2)) = Re ((1 - x * cnj x) * (1 - y * cnj y) + 2 * (x - y) * cnj (x - y)) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2))
[PROOF STEP]
using \<open>is_real x\<close> \<open>is_imag y\<close>
[PROOF STATE]
proof (prove)
using this:
is_real x
is_imag y

goal (1 subgoal):
 1. ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2) + 2 * (cmod (x - y))\<^sup>2) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2)) = Re ((1 - x * cnj x) * (1 - y * cnj y) + 2 * (x - y) * cnj (x - y)) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2))
[PROOF STEP]
by ((subst cmod_square)+, simp)
[PROOF STATE]
proof (state)
this:
((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2) + 2 * (cmod (x - y))\<^sup>2) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2)) = Re ((1 - x * cnj x) * (1 - y * cnj y) + 2 * (x - y) * cnj (x - y)) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2))

goal (1 subgoal):
 1. (1 + 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)) * (1 + 2 * (cmod y)\<^sup>2 / (1 - (cmod y)\<^sup>2)) = 1 + 2 * (cmod (x - y))\<^sup>2 / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2) + 2 * (cmod (x - y))\<^sup>2) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2)) = Re ((1 - x * cnj x) * (1 - y * cnj y) + 2 * (x - y) * cnj (x - y)) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2))

goal (1 subgoal):
 1. (1 + 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)) * (1 + 2 * (cmod y)\<^sup>2 / (1 - (cmod y)\<^sup>2)) = 1 + 2 * (cmod (x - y))\<^sup>2 / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2))
[PROOF STEP]
have "... = Re (1 + x * cnj x * y * cnj y
                               + x * cnj x - 2 * y * cnj x - 2 * x * cnj y + y * cnj y) / ?den"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Re ((1 - x * cnj x) * (1 - y * cnj y) + 2 * (x - y) * cnj (x - y)) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2)) = Re (1 + x * cnj x * y * cnj y + x * cnj x - 2 * y * cnj x - 2 * x * cnj y + y * cnj y) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2))
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
Re ((1 - x * cnj x) * (1 - y * cnj y) + 2 * (x - y) * cnj (x - y)) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2)) = Re (1 + x * cnj x * y * cnj y + x * cnj x - 2 * y * cnj x - 2 * x * cnj y + y * cnj y) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2))

goal (1 subgoal):
 1. (1 + 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)) * (1 + 2 * (cmod y)\<^sup>2 / (1 - (cmod y)\<^sup>2)) = 1 + 2 * (cmod (x - y))\<^sup>2 / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Re ((1 - x * cnj x) * (1 - y * cnj y) + 2 * (x - y) * cnj (x - y)) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2)) = Re (1 + x * cnj x * y * cnj y + x * cnj x - 2 * y * cnj x - 2 * x * cnj y + y * cnj y) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2))

goal (1 subgoal):
 1. (1 + 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)) * (1 + 2 * (cmod y)\<^sup>2 / (1 - (cmod y)\<^sup>2)) = 1 + 2 * (cmod (x - y))\<^sup>2 / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2))
[PROOF STEP]
have "... = Re ((1 + y * cnj y) * (1 + x * cnj x)) / ?den"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Re (1 + x * cnj x * y * cnj y + x * cnj x - 2 * y * cnj x - 2 * x * cnj y + y * cnj y) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2)) = Re ((1 + y * cnj y) * (1 + x * cnj x)) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2))
[PROOF STEP]
using \<open>is_real x\<close> \<open>is_imag y\<close>
[PROOF STATE]
proof (prove)
using this:
is_real x
is_imag y

goal (1 subgoal):
 1. Re (1 + x * cnj x * y * cnj y + x * cnj x - 2 * y * cnj x - 2 * x * cnj y + y * cnj y) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2)) = Re ((1 + y * cnj y) * (1 + x * cnj x)) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2))
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
Re (1 + x * cnj x * y * cnj y + x * cnj x - 2 * y * cnj x - 2 * x * cnj y + y * cnj y) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2)) = Re ((1 + y * cnj y) * (1 + x * cnj x)) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2))

goal (1 subgoal):
 1. (1 + 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)) * (1 + 2 * (cmod y)\<^sup>2 / (1 - (cmod y)\<^sup>2)) = 1 + 2 * (cmod (x - y))\<^sup>2 / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
1 + 2 * (cmod (x - y))\<^sup>2 / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2)) = Re ((1 + y * cnj y) * (1 + x * cnj x)) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
1 + 2 * (cmod (x - y))\<^sup>2 / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2)) = Re ((1 + y * cnj y) * (1 + x * cnj x)) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2))

goal (1 subgoal):
 1. (1 + 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)) * (1 + 2 * (cmod y)\<^sup>2 / (1 - (cmod y)\<^sup>2)) = 1 + 2 * (cmod (x - y))\<^sup>2 / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2))
[PROOF STEP]
using \<open>?den1 > 0\<close> \<open>?den2 > 0\<close>
[PROOF STATE]
proof (prove)
using this:
1 + 2 * (cmod (x - y))\<^sup>2 / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2)) = Re ((1 + y * cnj y) * (1 + x * cnj x)) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2))
0 < 1 - (cmod x)\<^sup>2
0 < 1 - (cmod y)\<^sup>2

goal (1 subgoal):
 1. (1 + 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)) * (1 + 2 * (cmod y)\<^sup>2 / (1 - (cmod y)\<^sup>2)) = 1 + 2 * (cmod (x - y))\<^sup>2 / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2))
[PROOF STEP]
apply (subst add_num_frac, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 + 2 * (cmod (x - y))\<^sup>2 / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2)) = Re ((1 + y * cnj y) * (1 + x * cnj x)) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2)); 0 < 1 - (cmod x)\<^sup>2; 0 < 1 - (cmod y)\<^sup>2\<rbrakk> \<Longrightarrow> (2 * (cmod x)\<^sup>2 + 1 * (1 - (cmod x)\<^sup>2)) / (1 - (cmod x)\<^sup>2) * (1 + 2 * (cmod y)\<^sup>2 / (1 - (cmod y)\<^sup>2)) = 1 + 2 * (cmod (x - y))\<^sup>2 / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2))
[PROOF STEP]
apply (subst add_num_frac, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 + 2 * (cmod (x - y))\<^sup>2 / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2)) = Re ((1 + y * cnj y) * (1 + x * cnj x)) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2)); 0 < 1 - (cmod x)\<^sup>2; 0 < 1 - (cmod y)\<^sup>2\<rbrakk> \<Longrightarrow> (2 * (cmod x)\<^sup>2 + 1 * (1 - (cmod x)\<^sup>2)) / (1 - (cmod x)\<^sup>2) * ((2 * (cmod y)\<^sup>2 + 1 * (1 - (cmod y)\<^sup>2)) / (1 - (cmod y)\<^sup>2)) = 1 + 2 * (cmod (x - y))\<^sup>2 / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 + 2 * (cmod (x - y))\<^sup>2 / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2)) = (1 + (Re y * Re y + Im y * Im y)) * (1 + (Re x * Re x + Im x * Im x)) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2)); (cmod x)\<^sup>2 < 1; (cmod y)\<^sup>2 < 1\<rbrakk> \<Longrightarrow> ((cmod x)\<^sup>2 + 1) * ((cmod y)\<^sup>2 + 1) = (1 + (Re y * Re y + Im y * Im y)) * (1 + (Re x * Re x + Im x * Im x))
[PROOF STEP]
apply (subst cmod_square)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>1 + 2 * (cmod (x - y))\<^sup>2 / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2)) = (1 + (Re y * Re y + Im y * Im y)) * (1 + (Re x * Re x + Im x * Im x)) / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2)); (cmod x)\<^sup>2 < 1; (cmod y)\<^sup>2 < 1\<rbrakk> \<Longrightarrow> (Re (x * cnj x) + 1) * (Re (y * cnj y) + 1) = (1 + (Re y * Re y + Im y * Im y)) * (1 + (Re x * Re x + Im x * Im x))
[PROOF STEP]
apply (simp add: field_simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(1 + 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)) * (1 + 2 * (cmod y)\<^sup>2 / (1 - (cmod y)\<^sup>2)) = 1 + 2 * (cmod (x - y))\<^sup>2 / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(1 + 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)) * (1 + 2 * (cmod y)\<^sup>2 / (1 - (cmod y)\<^sup>2)) = 1 + 2 * (cmod (x - y))\<^sup>2 / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2))

goal (1 subgoal):
 1. distinct [0\<^sub>h, of_complex x, of_complex y] \<Longrightarrow> cosh_dist (of_complex x) (of_complex y) = cosh_dist 0\<^sub>h (of_complex x) * cosh_dist 0\<^sub>h (of_complex y)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
cosh_dist 0\<^sub>h (of_complex x) = 1 + 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)
cosh_dist 0\<^sub>h (of_complex y) = 1 + 2 * (cmod y)\<^sup>2 / (1 - (cmod y)\<^sup>2)
cosh_dist (of_complex x) (of_complex y) = 1 + 2 * (cmod (x - y))\<^sup>2 / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2))
(1 + 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)) * (1 + 2 * (cmod y)\<^sup>2 / (1 - (cmod y)\<^sup>2)) = 1 + 2 * (cmod (x - y))\<^sup>2 / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2))
[PROOF STEP]
show "?P' 0\<^sub>h (of_complex x) (of_complex y)"
[PROOF STATE]
proof (prove)
using this:
cosh_dist 0\<^sub>h (of_complex x) = 1 + 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)
cosh_dist 0\<^sub>h (of_complex y) = 1 + 2 * (cmod y)\<^sup>2 / (1 - (cmod y)\<^sup>2)
cosh_dist (of_complex x) (of_complex y) = 1 + 2 * (cmod (x - y))\<^sup>2 / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2))
(1 + 2 * (cmod x)\<^sup>2 / (1 - (cmod x)\<^sup>2)) * (1 + 2 * (cmod y)\<^sup>2 / (1 - (cmod y)\<^sup>2)) = 1 + 2 * (cmod (x - y))\<^sup>2 / ((1 - (cmod x)\<^sup>2) * (1 - (cmod y)\<^sup>2))

goal (1 subgoal):
 1. cosh_dist (of_complex x) (of_complex y) = cosh_dist 0\<^sub>h (of_complex x) * cosh_dist 0\<^sub>h (of_complex y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cosh_dist (of_complex x) (of_complex y) = cosh_dist 0\<^sub>h (of_complex x) * cosh_dist 0\<^sub>h (of_complex y)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
distinct [0\<^sub>h, of_complex x, of_complex y] \<longrightarrow> cosh_dist (of_complex x) (of_complex y) = cosh_dist 0\<^sub>h (of_complex x) * cosh_dist 0\<^sub>h (of_complex y)

goal (2 subgoals):
 1. \<And>M u v w. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; distinct [moebius_pt M u, moebius_pt M v, moebius_pt M w] \<longrightarrow> cosh_dist (moebius_pt M v) (moebius_pt M w) = cosh_dist (moebius_pt M u) (moebius_pt M v) * cosh_dist (moebius_pt M u) (moebius_pt M w)\<rbrakk> \<Longrightarrow> distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
 2. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; distinct [conjugate u, conjugate v, conjugate w] \<longrightarrow> cosh_dist (conjugate v) (conjugate w) = cosh_dist (conjugate u) (conjugate v) * cosh_dist (conjugate u) (conjugate w)\<rbrakk> \<Longrightarrow> distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>M u v w. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; distinct [moebius_pt M u, moebius_pt M v, moebius_pt M w] \<longrightarrow> cosh_dist (moebius_pt M v) (moebius_pt M w) = cosh_dist (moebius_pt M u) (moebius_pt M v) * cosh_dist (moebius_pt M u) (moebius_pt M w)\<rbrakk> \<Longrightarrow> distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
 2. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; distinct [conjugate u, conjugate v, conjugate w] \<longrightarrow> cosh_dist (conjugate v) (conjugate w) = cosh_dist (conjugate u) (conjugate v) * cosh_dist (conjugate u) (conjugate w)\<rbrakk> \<Longrightarrow> distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
[PROOF STEP]
fix M u v w
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>M u v w. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; distinct [moebius_pt M u, moebius_pt M v, moebius_pt M w] \<longrightarrow> cosh_dist (moebius_pt M v) (moebius_pt M w) = cosh_dist (moebius_pt M u) (moebius_pt M v) * cosh_dist (moebius_pt M u) (moebius_pt M w)\<rbrakk> \<Longrightarrow> distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
 2. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; distinct [conjugate u, conjugate v, conjugate w] \<longrightarrow> cosh_dist (conjugate v) (conjugate w) = cosh_dist (conjugate u) (conjugate v) * cosh_dist (conjugate u) (conjugate w)\<rbrakk> \<Longrightarrow> distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
[PROOF STEP]
assume 1: "unit_disc_fix M" "u \<in> unit_disc" "v \<in> unit_disc" "w \<in> unit_disc"
[PROOF STATE]
proof (state)
this:
unit_disc_fix M
u \<in> unit_disc
v \<in> unit_disc
w \<in> unit_disc

goal (2 subgoals):
 1. \<And>M u v w. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; distinct [moebius_pt M u, moebius_pt M v, moebius_pt M w] \<longrightarrow> cosh_dist (moebius_pt M v) (moebius_pt M w) = cosh_dist (moebius_pt M u) (moebius_pt M v) * cosh_dist (moebius_pt M u) (moebius_pt M w)\<rbrakk> \<Longrightarrow> distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
 2. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; distinct [conjugate u, conjugate v, conjugate w] \<longrightarrow> cosh_dist (conjugate v) (conjugate w) = cosh_dist (conjugate u) (conjugate v) * cosh_dist (conjugate u) (conjugate w)\<rbrakk> \<Longrightarrow> distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
[PROOF STEP]
assume 2: "?P (moebius_pt M u) (moebius_pt M v) (moebius_pt M w)"
[PROOF STATE]
proof (state)
this:
distinct [moebius_pt M u, moebius_pt M v, moebius_pt M w] \<longrightarrow> cosh_dist (moebius_pt M v) (moebius_pt M w) = cosh_dist (moebius_pt M u) (moebius_pt M v) * cosh_dist (moebius_pt M u) (moebius_pt M w)

goal (2 subgoals):
 1. \<And>M u v w. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; distinct [moebius_pt M u, moebius_pt M v, moebius_pt M w] \<longrightarrow> cosh_dist (moebius_pt M v) (moebius_pt M w) = cosh_dist (moebius_pt M u) (moebius_pt M v) * cosh_dist (moebius_pt M u) (moebius_pt M w)\<rbrakk> \<Longrightarrow> distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
 2. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; distinct [conjugate u, conjugate v, conjugate w] \<longrightarrow> cosh_dist (conjugate v) (conjugate w) = cosh_dist (conjugate u) (conjugate v) * cosh_dist (conjugate u) (conjugate w)\<rbrakk> \<Longrightarrow> distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
[PROOF STEP]
show "?P u v w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
[PROOF STEP]
using 1 2
[PROOF STATE]
proof (prove)
using this:
unit_disc_fix M
u \<in> unit_disc
v \<in> unit_disc
w \<in> unit_disc
distinct [moebius_pt M u, moebius_pt M v, moebius_pt M w] \<longrightarrow> cosh_dist (moebius_pt M v) (moebius_pt M w) = cosh_dist (moebius_pt M u) (moebius_pt M v) * cosh_dist (moebius_pt M u) (moebius_pt M w)

goal (1 subgoal):
 1. distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w

goal (1 subgoal):
 1. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; distinct [conjugate u, conjugate v, conjugate w] \<longrightarrow> cosh_dist (conjugate v) (conjugate w) = cosh_dist (conjugate u) (conjugate v) * cosh_dist (conjugate u) (conjugate w)\<rbrakk> \<Longrightarrow> distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; distinct [conjugate u, conjugate v, conjugate w] \<longrightarrow> cosh_dist (conjugate v) (conjugate w) = cosh_dist (conjugate u) (conjugate v) * cosh_dist (conjugate u) (conjugate w)\<rbrakk> \<Longrightarrow> distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
[PROOF STEP]
fix u v w
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; distinct [conjugate u, conjugate v, conjugate w] \<longrightarrow> cosh_dist (conjugate v) (conjugate w) = cosh_dist (conjugate u) (conjugate v) * cosh_dist (conjugate u) (conjugate w)\<rbrakk> \<Longrightarrow> distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
[PROOF STEP]
assume 1:  "u \<in> unit_disc" "v \<in> unit_disc" "w \<in> unit_disc"
[PROOF STATE]
proof (state)
this:
u \<in> unit_disc
v \<in> unit_disc
w \<in> unit_disc

goal (1 subgoal):
 1. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; distinct [conjugate u, conjugate v, conjugate w] \<longrightarrow> cosh_dist (conjugate v) (conjugate w) = cosh_dist (conjugate u) (conjugate v) * cosh_dist (conjugate u) (conjugate w)\<rbrakk> \<Longrightarrow> distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
[PROOF STEP]
assume 2: "?P (conjugate u) (conjugate v) (conjugate w)"
[PROOF STATE]
proof (state)
this:
distinct [conjugate u, conjugate v, conjugate w] \<longrightarrow> cosh_dist (conjugate v) (conjugate w) = cosh_dist (conjugate u) (conjugate v) * cosh_dist (conjugate u) (conjugate w)

goal (1 subgoal):
 1. \<And>u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; distinct [conjugate u, conjugate v, conjugate w] \<longrightarrow> cosh_dist (conjugate v) (conjugate w) = cosh_dist (conjugate u) (conjugate v) * cosh_dist (conjugate u) (conjugate w)\<rbrakk> \<Longrightarrow> distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
[PROOF STEP]
show "?P u v w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
[PROOF STEP]
using 1 2
[PROOF STATE]
proof (prove)
using this:
u \<in> unit_disc
v \<in> unit_disc
w \<in> unit_disc
distinct [conjugate u, conjugate v, conjugate w] \<longrightarrow> cosh_dist (conjugate v) (conjugate w) = cosh_dist (conjugate u) (conjugate v) * cosh_dist (conjugate u) (conjugate w)

goal (1 subgoal):
 1. distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
[PROOF STEP]
by (auto simp add: conjugate_inj)
[PROOF STATE]
proof (state)
this:
distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w

goal (1 subgoal):
 1. distinct [u, v, w] \<Longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w

goal (1 subgoal):
 1. cosh_dist v w = cosh_dist u v * cosh_dist u w
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
distinct [u, v, w] \<longrightarrow> cosh_dist v w = cosh_dist u v * cosh_dist u w
distinct [u, v, w]

goal (1 subgoal):
 1. cosh_dist v w = cosh_dist u v * cosh_dist u w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cosh_dist v w = cosh_dist u v * cosh_dist u w

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma upper_bound:
  fixes b::nat
    and c::int
  assumes "b > 0"
      and "c < 2^(b-1)"
    shows "c + 2^(b-1) < 2^b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c + 2 ^ (b - 1) < 2 ^ b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c + 2 ^ (b - 1) < 2 ^ b
[PROOF STEP]
have a1: "\<And>P. (\<forall>b::nat. P b) \<Longrightarrow> (\<forall>b>0. P ((b-1)::nat))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P. \<forall>b. P b \<Longrightarrow> \<forall>b>0. P (b - 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>b. ?P b \<Longrightarrow> \<forall>b>0. ?P (b - 1)

goal (1 subgoal):
 1. c + 2 ^ (b - 1) < 2 ^ b
[PROOF STEP]
have b2: "\<forall>b::nat. (\<forall>(c::int)<2^b. (c + 2^b) < 2^(Suc b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>b c. c < 2 ^ b \<longrightarrow> c + 2 ^ b < 2 ^ Suc b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>b c. c < 2 ^ b \<longrightarrow> c + 2 ^ b < 2 ^ Suc b

goal (1 subgoal):
 1. c + 2 ^ (b - 1) < 2 ^ b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c + 2 ^ (b - 1) < 2 ^ b
[PROOF STEP]
using a1[OF b2] assms
[PROOF STATE]
proof (prove)
using this:
\<forall>b>0. \<forall>c<2 ^ (b - 1). c + 2 ^ (b - 1) < 2 ^ Suc (b - 1)
0 < b
c < 2 ^ (b - 1)

goal (1 subgoal):
 1. c + 2 ^ (b - 1) < 2 ^ b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
c + 2 ^ (b - 1) < 2 ^ b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma upper_bound2:
  fixes b::nat
      and c::int
    assumes "b > 0"
      and "c < 2^b"
      and "c \<ge> 0"
    shows "c - (2^(b-1)) < 2^(b-1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c - 2 ^ (b - 1) < 2 ^ (b - 1)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c - 2 ^ (b - 1) < 2 ^ (b - 1)
[PROOF STEP]
have a1: "\<And>P. (\<forall>b::nat. P b) \<Longrightarrow> (\<forall>b>0. P ((b-1)::nat))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P. \<forall>b. P b \<Longrightarrow> \<forall>b>0. P (b - 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>b. ?P b \<Longrightarrow> \<forall>b>0. ?P (b - 1)

goal (1 subgoal):
 1. c - 2 ^ (b - 1) < 2 ^ (b - 1)
[PROOF STEP]
have b2: "\<forall>b::nat. (\<forall>(c::int)<2^(Suc b). c\<ge>0 \<longrightarrow> (c - 2^b) < 2^b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>b c. c < 2 ^ Suc b \<longrightarrow> 0 \<le> c \<longrightarrow> c - 2 ^ b < 2 ^ b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>b c. c < 2 ^ Suc b \<longrightarrow> 0 \<le> c \<longrightarrow> c - 2 ^ b < 2 ^ b

goal (1 subgoal):
 1. c - 2 ^ (b - 1) < 2 ^ (b - 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c - 2 ^ (b - 1) < 2 ^ (b - 1)
[PROOF STEP]
using a1[OF b2] assms
[PROOF STATE]
proof (prove)
using this:
\<forall>b>0. \<forall>c<2 ^ Suc (b - 1). 0 \<le> c \<longrightarrow> c - 2 ^ (b - 1) < 2 ^ (b - 1)
0 < b
c < 2 ^ b
0 \<le> c

goal (1 subgoal):
 1. c - 2 ^ (b - 1) < 2 ^ (b - 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
c - 2 ^ (b - 1) < 2 ^ (b - 1)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma upper_bound3:
  fixes b::nat
    and v::int
      defines "x \<equiv> - (2 ^ (b - 1)) + (v + 2 ^ (b - 1)) mod 2 ^ b"
    assumes "b>0"
    shows "x < 2^(b-1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < 2 ^ (b - 1)
[PROOF STEP]
using upper_bound2 assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < ?b; ?c < 2 ^ ?b; 0 \<le> ?c\<rbrakk> \<Longrightarrow> ?c - 2 ^ (?b - 1) < 2 ^ (?b - 1)
x \<equiv> - (2 ^ (b - 1)) + (v + 2 ^ (b - 1)) mod 2 ^ b
0 < b

goal (1 subgoal):
 1. x < 2 ^ (b - 1)
[PROOF STEP]
by auto


[STATEMENT]
lemma lower_bound:
    fixes b::nat
  assumes "b>0"
    shows "\<forall>(c::int) \<ge> -(2^(b-1)). (-c + 2^(b-1) - 1 < 2^b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c\<ge>- (2 ^ (b - 1)). - c + 2 ^ (b - 1) - 1 < 2 ^ b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>c\<ge>- (2 ^ (b - 1)). - c + 2 ^ (b - 1) - 1 < 2 ^ b
[PROOF STEP]
have a1: "\<And>P. (\<forall>b::nat. P b) \<Longrightarrow> (\<forall>b>0. P ((b-1)::nat))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P. \<forall>b. P b \<Longrightarrow> \<forall>b>0. P (b - 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>b. ?P b \<Longrightarrow> \<forall>b>0. ?P (b - 1)

goal (1 subgoal):
 1. \<forall>c\<ge>- (2 ^ (b - 1)). - c + 2 ^ (b - 1) - 1 < 2 ^ b
[PROOF STEP]
have b2: "\<forall>b::nat. \<forall>(c::int) \<ge> -(2^b). (-c + (2^b) - 1) < 2^(Suc b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>b c. - (2 ^ b) \<le> c \<longrightarrow> - c + 2 ^ b - 1 < 2 ^ Suc b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>b c. - (2 ^ b) \<le> c \<longrightarrow> - c + 2 ^ b - 1 < 2 ^ Suc b

goal (1 subgoal):
 1. \<forall>c\<ge>- (2 ^ (b - 1)). - c + 2 ^ (b - 1) - 1 < 2 ^ b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c\<ge>- (2 ^ (b - 1)). - c + 2 ^ (b - 1) - 1 < 2 ^ b
[PROOF STEP]
using a1[OF b2] assms
[PROOF STATE]
proof (prove)
using this:
\<forall>b>0. \<forall>c\<ge>- (2 ^ (b - 1)). - c + 2 ^ (b - 1) - 1 < 2 ^ Suc (b - 1)
0 < b

goal (1 subgoal):
 1. \<forall>c\<ge>- (2 ^ (b - 1)). - c + 2 ^ (b - 1) - 1 < 2 ^ b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>c\<ge>- (2 ^ (b - 1)). - c + 2 ^ (b - 1) - 1 < 2 ^ b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lower_bound2:
  fixes b::nat
    and v::int
      defines "x \<equiv> 2^(b - 1) - (-v+2^(b-1)-1) mod 2^b - 1"
    assumes "b>0"
    shows "x \<ge> - (2 ^ (b - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - (2 ^ (b - 1)) \<le> x
[PROOF STEP]
using upper_bound2 assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < ?b; ?c < 2 ^ ?b; 0 \<le> ?c\<rbrakk> \<Longrightarrow> ?c - 2 ^ (?b - 1) < 2 ^ (?b - 1)
x \<equiv> 2 ^ (b - 1) - (- v + 2 ^ (b - 1) - 1) mod 2 ^ b - 1
0 < b

goal (1 subgoal):
 1. - (2 ^ (b - 1)) \<le> x
[PROOF STEP]
by auto


[STATEMENT]
lemma createSInt_id_g0:
    fixes b::nat
      and v::int
  assumes "v \<ge> 0"
      and "v < 2^(b-1)"
      and "b > 0"
    shows "createSInt b v = ShowL\<^sub>i\<^sub>n\<^sub>t v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. createSInt b v = \<lfloor>v\<rfloor>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. createSInt b v = \<lfloor>v\<rfloor>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
0 \<le> v
v < 2 ^ (b - 1)
0 < b
[PROOF STEP]
have "v + 2^(b-1) \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
0 \<le> v
v < 2 ^ (b - 1)
0 < b

goal (1 subgoal):
 1. 0 \<le> v + 2 ^ (b - 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> v + 2 ^ (b - 1)

goal (1 subgoal):
 1. createSInt b v = \<lfloor>v\<rfloor>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 \<le> v + 2 ^ (b - 1)

goal (1 subgoal):
 1. createSInt b v = \<lfloor>v\<rfloor>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
0 \<le> v
v < 2 ^ (b - 1)
0 < b
[PROOF STEP]
have "v + (2^(b-1)) < 2^b"
[PROOF STATE]
proof (prove)
using this:
0 \<le> v
v < 2 ^ (b - 1)
0 < b

goal (1 subgoal):
 1. v + 2 ^ (b - 1) < 2 ^ b
[PROOF STEP]
using upper_bound[of b]
[PROOF STATE]
proof (prove)
using this:
0 \<le> v
v < 2 ^ (b - 1)
0 < b
\<lbrakk>0 < b; ?c < 2 ^ (b - 1)\<rbrakk> \<Longrightarrow> ?c + 2 ^ (b - 1) < 2 ^ b

goal (1 subgoal):
 1. v + 2 ^ (b - 1) < 2 ^ b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v + 2 ^ (b - 1) < 2 ^ b

goal (1 subgoal):
 1. createSInt b v = \<lfloor>v\<rfloor>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
0 \<le> v + 2 ^ (b - 1)
v + 2 ^ (b - 1) < 2 ^ b
[PROOF STEP]
have "(v + 2^(b-1)) mod (2^b) = v + 2^(b-1)"
[PROOF STATE]
proof (prove)
using this:
0 \<le> v + 2 ^ (b - 1)
v + 2 ^ (b - 1) < 2 ^ b

goal (1 subgoal):
 1. (v + 2 ^ (b - 1)) mod 2 ^ b = v + 2 ^ (b - 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(v + 2 ^ (b - 1)) mod 2 ^ b = v + 2 ^ (b - 1)

goal (1 subgoal):
 1. createSInt b v = \<lfloor>v\<rfloor>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(v + 2 ^ (b - 1)) mod 2 ^ b = v + 2 ^ (b - 1)

goal (1 subgoal):
 1. createSInt b v = \<lfloor>v\<rfloor>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
0 \<le> v
v < 2 ^ (b - 1)
0 < b
[PROOF STEP]
have "createSInt b v=ShowL\<^sub>i\<^sub>n\<^sub>t (-(2^(b-1)) + (v+2^(b-1)) mod (2^b))"
[PROOF STATE]
proof (prove)
using this:
0 \<le> v
v < 2 ^ (b - 1)
0 < b

goal (1 subgoal):
 1. createSInt b v = \<lfloor>- (2 ^ (b - 1)) + (v + 2 ^ (b - 1)) mod 2 ^ b\<rfloor>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
createSInt b v = \<lfloor>- (2 ^ (b - 1)) + (v + 2 ^ (b - 1)) mod 2 ^ b\<rfloor>

goal (1 subgoal):
 1. createSInt b v = \<lfloor>v\<rfloor>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(v + 2 ^ (b - 1)) mod 2 ^ b = v + 2 ^ (b - 1)
createSInt b v = \<lfloor>- (2 ^ (b - 1)) + (v + 2 ^ (b - 1)) mod 2 ^ b\<rfloor>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(v + 2 ^ (b - 1)) mod 2 ^ b = v + 2 ^ (b - 1)
createSInt b v = \<lfloor>- (2 ^ (b - 1)) + (v + 2 ^ (b - 1)) mod 2 ^ b\<rfloor>

goal (1 subgoal):
 1. createSInt b v = \<lfloor>v\<rfloor>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
createSInt b v = \<lfloor>v\<rfloor>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma createSInt_id_l0:
    fixes b::nat
      and v::int
  assumes "v < 0"
      and "v \<ge> -(2^(b-1))"
      and "b > 0"
    shows "createSInt b v = ShowL\<^sub>i\<^sub>n\<^sub>t v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. createSInt b v = \<lfloor>v\<rfloor>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. createSInt b v = \<lfloor>v\<rfloor>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
v < 0
- (2 ^ (b - 1)) \<le> v
0 < b
[PROOF STEP]
have "-v + 2^(b-1) - 1 \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
v < 0
- (2 ^ (b - 1)) \<le> v
0 < b

goal (1 subgoal):
 1. 0 \<le> - v + 2 ^ (b - 1) - 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> - v + 2 ^ (b - 1) - 1

goal (1 subgoal):
 1. createSInt b v = \<lfloor>v\<rfloor>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 \<le> - v + 2 ^ (b - 1) - 1

goal (1 subgoal):
 1. createSInt b v = \<lfloor>v\<rfloor>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
v < 0
- (2 ^ (b - 1)) \<le> v
0 < b
[PROOF STEP]
have "-v + 2^(b-1) - 1 < 2^b"
[PROOF STATE]
proof (prove)
using this:
v < 0
- (2 ^ (b - 1)) \<le> v
0 < b

goal (1 subgoal):
 1. - v + 2 ^ (b - 1) - 1 < 2 ^ b
[PROOF STEP]
using lower_bound[of b]
[PROOF STATE]
proof (prove)
using this:
v < 0
- (2 ^ (b - 1)) \<le> v
0 < b
0 < b \<Longrightarrow> \<forall>c\<ge>- (2 ^ (b - 1)). - c + 2 ^ (b - 1) - 1 < 2 ^ b

goal (1 subgoal):
 1. - v + 2 ^ (b - 1) - 1 < 2 ^ b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
- v + 2 ^ (b - 1) - 1 < 2 ^ b

goal (1 subgoal):
 1. createSInt b v = \<lfloor>v\<rfloor>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
0 \<le> - v + 2 ^ (b - 1) - 1
- v + 2 ^ (b - 1) - 1 < 2 ^ b
[PROOF STEP]
have "(-v + 2^(b-1) - 1) mod (2^b) = (-v + 2^(b-1) - 1)"
[PROOF STATE]
proof (prove)
using this:
0 \<le> - v + 2 ^ (b - 1) - 1
- v + 2 ^ (b - 1) - 1 < 2 ^ b

goal (1 subgoal):
 1. (- v + 2 ^ (b - 1) - 1) mod 2 ^ b = - v + 2 ^ (b - 1) - 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(- v + 2 ^ (b - 1) - 1) mod 2 ^ b = - v + 2 ^ (b - 1) - 1

goal (1 subgoal):
 1. createSInt b v = \<lfloor>v\<rfloor>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(- v + 2 ^ (b - 1) - 1) mod 2 ^ b = - v + 2 ^ (b - 1) - 1

goal (1 subgoal):
 1. createSInt b v = \<lfloor>v\<rfloor>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
v < 0
- (2 ^ (b - 1)) \<le> v
0 < b
[PROOF STEP]
have "createSInt b v= ShowL\<^sub>i\<^sub>n\<^sub>t (2^(b-1) - (-v+2^(b-1)-1) mod (2^b) - 1)"
[PROOF STATE]
proof (prove)
using this:
v < 0
- (2 ^ (b - 1)) \<le> v
0 < b

goal (1 subgoal):
 1. createSInt b v = \<lfloor>2 ^ (b - 1) - (- v + 2 ^ (b - 1) - 1) mod 2 ^ b - 1\<rfloor>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
createSInt b v = \<lfloor>2 ^ (b - 1) - (- v + 2 ^ (b - 1) - 1) mod 2 ^ b - 1\<rfloor>

goal (1 subgoal):
 1. createSInt b v = \<lfloor>v\<rfloor>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(- v + 2 ^ (b - 1) - 1) mod 2 ^ b = - v + 2 ^ (b - 1) - 1
createSInt b v = \<lfloor>2 ^ (b - 1) - (- v + 2 ^ (b - 1) - 1) mod 2 ^ b - 1\<rfloor>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(- v + 2 ^ (b - 1) - 1) mod 2 ^ b = - v + 2 ^ (b - 1) - 1
createSInt b v = \<lfloor>2 ^ (b - 1) - (- v + 2 ^ (b - 1) - 1) mod 2 ^ b - 1\<rfloor>

goal (1 subgoal):
 1. createSInt b v = \<lfloor>v\<rfloor>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
createSInt b v = \<lfloor>v\<rfloor>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma createSInt_id:
    fixes b::nat
      and v::int
  assumes "v < 2^(b-1)"
      and "v \<ge> -(2^(b-1))"
      and "b > 0"
    shows "createSInt b v = ShowL\<^sub>i\<^sub>n\<^sub>t v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. createSInt b v = \<lfloor>v\<rfloor>
[PROOF STEP]
using createSInt_id_g0 createSInt_id_l0 assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 \<le> ?v; ?v < 2 ^ (?b - 1); 0 < ?b\<rbrakk> \<Longrightarrow> createSInt ?b ?v = \<lfloor>?v\<rfloor>
\<lbrakk>?v < 0; - (2 ^ (?b - 1)) \<le> ?v; 0 < ?b\<rbrakk> \<Longrightarrow> createSInt ?b ?v = \<lfloor>?v\<rfloor>
v < 2 ^ (b - 1)
- (2 ^ (b - 1)) \<le> v
0 < b

goal (1 subgoal):
 1. createSInt b v = \<lfloor>v\<rfloor>
[PROOF STEP]
by simp


[STATEMENT]
lemma createUInt_id:
  assumes "v \<ge> 0"
      and "v < 2^b"
    shows "createUInt b v =  ShowL\<^sub>i\<^sub>n\<^sub>t v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. createUInt b v = \<lfloor>v\<rfloor>
[PROOF STEP]
by (simp add: assms(1) assms(2))


[STATEMENT]
lemma convert_id[simp]:
  "convert tp tp kv = Some (kv, tp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convert tp tp kv = Some (kv, tp)
[PROOF STEP]
by (metis Types.exhaust convert.simps(1) convert.simps(2) convert.simps(4) convert.simps(5) order_refl)