[STATEMENT]
lemma perpendicular_to_x_axis:
  assumes "is_poincare_line H"
  shows "perpendicular_to_x_axis H \<longleftrightarrow> perpendicular x_axis H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. perpendicular_to_x_axis H = perpendicular x_axis H
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_poincare_line H

goal (1 subgoal):
 1. perpendicular_to_x_axis H = perpendicular x_axis H
[PROOF STEP]
unfolding perpendicular_def
[PROOF STATE]
proof (prove)
using this:
is_poincare_line H

goal (1 subgoal):
 1. perpendicular_to_x_axis H = (cos_angle (of_circline x_axis) (of_circline H) = 0)
[PROOF STEP]
proof (transfer, transfer)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>H Ha. \<lbrakk>hermitean H \<and> H \<noteq> mat_zero; is_poincare_line_cmat H; is_poincare_line_clmat Ha\<rbrakk> \<Longrightarrow> perpendicular_to_x_axis_cmat H = (cos_angle_cmat (of_circline_cmat x_axis_cmat) (of_circline_cmat H) = 0)
[PROOF STEP]
fix H
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>H Ha. \<lbrakk>hermitean H \<and> H \<noteq> mat_zero; is_poincare_line_cmat H; is_poincare_line_clmat Ha\<rbrakk> \<Longrightarrow> perpendicular_to_x_axis_cmat H = (cos_angle_cmat (of_circline_cmat x_axis_cmat) (of_circline_cmat H) = 0)
[PROOF STEP]
assume hh: "hermitean H \<and> H \<noteq> mat_zero" "is_poincare_line_cmat H"
[PROOF STATE]
proof (state)
this:
hermitean H \<and> H \<noteq> mat_zero
is_poincare_line_cmat H

goal (1 subgoal):
 1. \<And>H Ha. \<lbrakk>hermitean H \<and> H \<noteq> mat_zero; is_poincare_line_cmat H; is_poincare_line_clmat Ha\<rbrakk> \<Longrightarrow> perpendicular_to_x_axis_cmat H = (cos_angle_cmat (of_circline_cmat x_axis_cmat) (of_circline_cmat H) = 0)
[PROOF STEP]
obtain A B C D where *: "H = (A, B, C, D)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A B C D. H = (A, B, C, D) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases H, auto)
[PROOF STATE]
proof (state)
this:
H = (A, B, C, D)

goal (1 subgoal):
 1. \<And>H Ha. \<lbrakk>hermitean H \<and> H \<noteq> mat_zero; is_poincare_line_cmat H; is_poincare_line_clmat Ha\<rbrakk> \<Longrightarrow> perpendicular_to_x_axis_cmat H = (cos_angle_cmat (of_circline_cmat x_axis_cmat) (of_circline_cmat H) = 0)
[PROOF STEP]
hence "is_real A" "(cmod B)\<^sup>2 > (cmod A)\<^sup>2" "H = (A, B, cnj B, A)"
[PROOF STATE]
proof (prove)
using this:
H = (A, B, C, D)

goal (1 subgoal):
 1. is_real A &&& (cmod A)\<^sup>2 < (cmod B)\<^sup>2 &&& H = (A, B, cnj B, A)
[PROOF STEP]
using hermitean_elems[of A B C D] hh
[PROOF STATE]
proof (prove)
using this:
H = (A, B, C, D)
hermitean (A, B, C, D) \<Longrightarrow> is_real A
hermitean (A, B, C, D) \<Longrightarrow> is_real D
hermitean (A, B, C, D) \<Longrightarrow> B = cnj C
hermitean (A, B, C, D) \<Longrightarrow> cnj B = C
hermitean H \<and> H \<noteq> mat_zero
is_poincare_line_cmat H

goal (1 subgoal):
 1. is_real A &&& (cmod A)\<^sup>2 < (cmod B)\<^sup>2 &&& H = (A, B, cnj B, A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_real A
(cmod A)\<^sup>2 < (cmod B)\<^sup>2
H = (A, B, cnj B, A)

goal (1 subgoal):
 1. \<And>H Ha. \<lbrakk>hermitean H \<and> H \<noteq> mat_zero; is_poincare_line_cmat H; is_poincare_line_clmat Ha\<rbrakk> \<Longrightarrow> perpendicular_to_x_axis_cmat H = (cos_angle_cmat (of_circline_cmat x_axis_cmat) (of_circline_cmat H) = 0)
[PROOF STEP]
thus "perpendicular_to_x_axis_cmat H =
        (cos_angle_cmat (of_circline_cmat x_axis_cmat) (of_circline_cmat H) = 0)"
[PROOF STATE]
proof (prove)
using this:
is_real A
(cmod A)\<^sup>2 < (cmod B)\<^sup>2
H = (A, B, cnj B, A)

goal (1 subgoal):
 1. perpendicular_to_x_axis_cmat H = (cos_angle_cmat (of_circline_cmat x_axis_cmat) (of_circline_cmat H) = 0)
[PROOF STEP]
using cmod_square[of B] cmod_square[of A]
[PROOF STATE]
proof (prove)
using this:
is_real A
(cmod A)\<^sup>2 < (cmod B)\<^sup>2
H = (A, B, cnj B, A)
(cmod B)\<^sup>2 = Re (B * cnj B)
(cmod A)\<^sup>2 = Re (A * cnj A)

goal (1 subgoal):
 1. perpendicular_to_x_axis_cmat H = (cos_angle_cmat (of_circline_cmat x_axis_cmat) (of_circline_cmat H) = 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
perpendicular_to_x_axis_cmat H = (cos_angle_cmat (of_circline_cmat x_axis_cmat) (of_circline_cmat H) = 0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma perpendicular_to_x_axis_y_axis:
  assumes "perpendicular_to_x_axis (poincare_line 0\<^sub>h (of_complex z))" "z \<noteq> 0"
  shows "is_imag z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_imag z
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
perpendicular_to_x_axis (poincare_line 0\<^sub>h (of_complex z))
z \<noteq> 0

goal (1 subgoal):
 1. is_imag z
[PROOF STEP]
by (transfer, transfer, simp)


[STATEMENT]
lemma wlog_perpendicular_axes:
  assumes in_disc: "u \<in> unit_disc" "v \<in> unit_disc" "z \<in> unit_disc"
  assumes perpendicular: "is_poincare_line H1" "is_poincare_line H2" "perpendicular H1 H2"
  assumes "z \<in> circline_set H1 \<inter> circline_set H2" "u \<in> circline_set H1" "v \<in> circline_set H2"
  assumes axes: "\<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> P 0\<^sub>h (of_complex x) (of_complex y)"
  assumes moebius: "\<And> M u v w. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; P (moebius_pt M u) (moebius_pt M v) (moebius_pt M w) \<rbrakk> \<Longrightarrow> P u v w"
  assumes conjugate: "\<And> u v w. \<lbrakk>u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; P (conjugate u) (conjugate v) (conjugate w) \<rbrakk> \<Longrightarrow> P u v w"
  shows "P z u v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P z u v
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P z u v
[PROOF STEP]
have "\<forall> v H1 H2. is_poincare_line H1 \<and> is_poincare_line H2 \<and> perpendicular H1 H2 \<and>
                   z \<in> circline_set H1 \<inter> circline_set H2 \<and> u \<in> circline_set H1 \<and> v \<in> circline_set H2 \<and> v \<in> unit_disc \<longrightarrow> P z u v" (is "?P z u")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>v H1 H2. is_poincare_line H1 \<and> is_poincare_line H2 \<and> perpendicular H1 H2 \<and> z \<in> circline_set H1 \<inter> circline_set H2 \<and> u \<in> circline_set H1 \<and> v \<in> circline_set H2 \<and> v \<in> unit_disc \<longrightarrow> P z u v
[PROOF STEP]
proof (rule wlog_x_axis[where P="?P"])
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. z \<in> unit_disc
 2. u \<in> unit_disc
 3. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; \<forall>va H1 H2. is_poincare_line H1 \<and> is_poincare_line H2 \<and> perpendicular H1 H2 \<and> moebius_pt M u \<in> circline_set H1 \<inter> circline_set H2 \<and> moebius_pt M v \<in> circline_set H1 \<and> va \<in> circline_set H2 \<and> va \<in> unit_disc \<longrightarrow> P (moebius_pt M u) (moebius_pt M v) va\<rbrakk> \<Longrightarrow> \<forall>va H1 H2. is_poincare_line H1 \<and> is_poincare_line H2 \<and> perpendicular H1 H2 \<and> u \<in> circline_set H1 \<inter> circline_set H2 \<and> v \<in> circline_set H1 \<and> va \<in> circline_set H2 \<and> va \<in> unit_disc \<longrightarrow> P u v va
 4. \<And>x. \<lbrakk>is_real x; 0 \<le> Re x; Re x < 1\<rbrakk> \<Longrightarrow> \<forall>v H1 H2. is_poincare_line H1 \<and> is_poincare_line H2 \<and> perpendicular H1 H2 \<and> 0\<^sub>h \<in> circline_set H1 \<inter> circline_set H2 \<and> of_complex x \<in> circline_set H1 \<and> v \<in> circline_set H2 \<and> v \<in> unit_disc \<longrightarrow> P 0\<^sub>h (of_complex x) v
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. z \<in> unit_disc
 2. u \<in> unit_disc
 3. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; \<forall>va H1 H2. is_poincare_line H1 \<and> is_poincare_line H2 \<and> perpendicular H1 H2 \<and> moebius_pt M u \<in> circline_set H1 \<inter> circline_set H2 \<and> moebius_pt M v \<in> circline_set H1 \<and> va \<in> circline_set H2 \<and> va \<in> unit_disc \<longrightarrow> P (moebius_pt M u) (moebius_pt M v) va\<rbrakk> \<Longrightarrow> \<forall>va H1 H2. is_poincare_line H1 \<and> is_poincare_line H2 \<and> perpendicular H1 H2 \<and> u \<in> circline_set H1 \<inter> circline_set H2 \<and> v \<in> circline_set H1 \<and> va \<in> circline_set H2 \<and> va \<in> unit_disc \<longrightarrow> P u v va
 4. \<And>x. \<lbrakk>is_real x; 0 \<le> Re x; Re x < 1\<rbrakk> \<Longrightarrow> \<forall>v H1 H2. is_poincare_line H1 \<and> is_poincare_line H2 \<and> perpendicular H1 H2 \<and> 0\<^sub>h \<in> circline_set H1 \<inter> circline_set H2 \<and> of_complex x \<in> circline_set H1 \<and> v \<in> circline_set H2 \<and> v \<in> unit_disc \<longrightarrow> P 0\<^sub>h (of_complex x) v
[PROOF STEP]
assume x: "is_real x" "Re x \<ge> 0" "Re x < 1"
[PROOF STATE]
proof (state)
this:
is_real x
0 \<le> Re x
Re x < 1

goal (4 subgoals):
 1. z \<in> unit_disc
 2. u \<in> unit_disc
 3. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; \<forall>va H1 H2. is_poincare_line H1 \<and> is_poincare_line H2 \<and> perpendicular H1 H2 \<and> moebius_pt M u \<in> circline_set H1 \<inter> circline_set H2 \<and> moebius_pt M v \<in> circline_set H1 \<and> va \<in> circline_set H2 \<and> va \<in> unit_disc \<longrightarrow> P (moebius_pt M u) (moebius_pt M v) va\<rbrakk> \<Longrightarrow> \<forall>va H1 H2. is_poincare_line H1 \<and> is_poincare_line H2 \<and> perpendicular H1 H2 \<and> u \<in> circline_set H1 \<inter> circline_set H2 \<and> v \<in> circline_set H1 \<and> va \<in> circline_set H2 \<and> va \<in> unit_disc \<longrightarrow> P u v va
 4. \<And>x. \<lbrakk>is_real x; 0 \<le> Re x; Re x < 1\<rbrakk> \<Longrightarrow> \<forall>v H1 H2. is_poincare_line H1 \<and> is_poincare_line H2 \<and> perpendicular H1 H2 \<and> 0\<^sub>h \<in> circline_set H1 \<inter> circline_set H2 \<and> of_complex x \<in> circline_set H1 \<and> v \<in> circline_set H2 \<and> v \<in> unit_disc \<longrightarrow> P 0\<^sub>h (of_complex x) v
[PROOF STEP]
have "of_complex x \<in> unit_disc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_complex x \<in> unit_disc
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
is_real x
0 \<le> Re x
Re x < 1

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

goal (4 subgoals):
 1. z \<in> unit_disc
 2. u \<in> unit_disc
 3. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; \<forall>va H1 H2. is_poincare_line H1 \<and> is_poincare_line H2 \<and> perpendicular H1 H2 \<and> moebius_pt M u \<in> circline_set H1 \<inter> circline_set H2 \<and> moebius_pt M v \<in> circline_set H1 \<and> va \<in> circline_set H2 \<and> va \<in> unit_disc \<longrightarrow> P (moebius_pt M u) (moebius_pt M v) va\<rbrakk> \<Longrightarrow> \<forall>va H1 H2. is_poincare_line H1 \<and> is_poincare_line H2 \<and> perpendicular H1 H2 \<and> u \<in> circline_set H1 \<inter> circline_set H2 \<and> v \<in> circline_set H1 \<and> va \<in> circline_set H2 \<and> va \<in> unit_disc \<longrightarrow> P u v va
 4. \<And>x. \<lbrakk>is_real x; 0 \<le> Re x; Re x < 1\<rbrakk> \<Longrightarrow> \<forall>v H1 H2. is_poincare_line H1 \<and> is_poincare_line H2 \<and> perpendicular H1 H2 \<and> 0\<^sub>h \<in> circline_set H1 \<inter> circline_set H2 \<and> of_complex x \<in> circline_set H1 \<and> v \<in> circline_set H2 \<and> v \<in> unit_disc \<longrightarrow> P 0\<^sub>h (of_complex x) v
[PROOF STEP]
show "?P 0\<^sub>h (of_complex x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>v H1 H2. is_poincare_line H1 \<and> is_poincare_line H2 \<and> perpendicular H1 H2 \<and> 0\<^sub>h \<in> circline_set H1 \<inter> circline_set H2 \<and> of_complex x \<in> circline_set H1 \<and> v \<in> circline_set H2 \<and> v \<in> unit_disc \<longrightarrow> P 0\<^sub>h (of_complex x) v
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v H1 H2. \<lbrakk>is_poincare_line H1; is_poincare_line H2; perpendicular H1 H2; 0\<^sub>h \<in> circline_set H1; 0\<^sub>h \<in> circline_set H2; of_complex x \<in> circline_set H1; v \<in> circline_set H2; v \<in> unit_disc\<rbrakk> \<Longrightarrow> P 0\<^sub>h (of_complex x) v
[PROOF STEP]
fix v H1 H2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v H1 H2. \<lbrakk>is_poincare_line H1; is_poincare_line H2; perpendicular H1 H2; 0\<^sub>h \<in> circline_set H1; 0\<^sub>h \<in> circline_set H2; of_complex x \<in> circline_set H1; v \<in> circline_set H2; v \<in> unit_disc\<rbrakk> \<Longrightarrow> P 0\<^sub>h (of_complex x) v
[PROOF STEP]
assume "v \<in> unit_disc"
[PROOF STATE]
proof (state)
this:
v \<in> unit_disc

goal (1 subgoal):
 1. \<And>v H1 H2. \<lbrakk>is_poincare_line H1; is_poincare_line H2; perpendicular H1 H2; 0\<^sub>h \<in> circline_set H1; 0\<^sub>h \<in> circline_set H2; of_complex x \<in> circline_set H1; v \<in> circline_set H2; v \<in> unit_disc\<rbrakk> \<Longrightarrow> P 0\<^sub>h (of_complex x) v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v \<in> unit_disc
[PROOF STEP]
obtain y where y: "v = of_complex y"
[PROOF STATE]
proof (prove)
using this:
v \<in> unit_disc

goal (1 subgoal):
 1. (\<And>y. v = of_complex y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using inf_or_of_complex[of v]
[PROOF STATE]
proof (prove)
using this:
v \<in> unit_disc
v = \<infinity>\<^sub>h \<or> (\<exists>x. v = of_complex x)

goal (1 subgoal):
 1. (\<And>y. v = of_complex y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v = of_complex y

goal (1 subgoal):
 1. \<And>v H1 H2. \<lbrakk>is_poincare_line H1; is_poincare_line H2; perpendicular H1 H2; 0\<^sub>h \<in> circline_set H1; 0\<^sub>h \<in> circline_set H2; of_complex x \<in> circline_set H1; v \<in> circline_set H2; v \<in> unit_disc\<rbrakk> \<Longrightarrow> P 0\<^sub>h (of_complex x) v
[PROOF STEP]
assume 1: "is_poincare_line H1" "is_poincare_line H2" "perpendicular H1 H2"
[PROOF STATE]
proof (state)
this:
is_poincare_line H1
is_poincare_line H2
perpendicular H1 H2

goal (1 subgoal):
 1. \<And>v H1 H2. \<lbrakk>is_poincare_line H1; is_poincare_line H2; perpendicular H1 H2; 0\<^sub>h \<in> circline_set H1; 0\<^sub>h \<in> circline_set H2; of_complex x \<in> circline_set H1; v \<in> circline_set H2; v \<in> unit_disc\<rbrakk> \<Longrightarrow> P 0\<^sub>h (of_complex x) v
[PROOF STEP]
assume 2: "0\<^sub>h \<in> circline_set H1" "0\<^sub>h \<in> circline_set H2" "of_complex x \<in> circline_set H1" "v \<in> circline_set H2"
[PROOF STATE]
proof (state)
this:
0\<^sub>h \<in> circline_set H1
0\<^sub>h \<in> circline_set H2
of_complex x \<in> circline_set H1
v \<in> circline_set H2

goal (1 subgoal):
 1. \<And>v H1 H2. \<lbrakk>is_poincare_line H1; is_poincare_line H2; perpendicular H1 H2; 0\<^sub>h \<in> circline_set H1; 0\<^sub>h \<in> circline_set H2; of_complex x \<in> circline_set H1; v \<in> circline_set H2; v \<in> unit_disc\<rbrakk> \<Longrightarrow> P 0\<^sub>h (of_complex x) v
[PROOF STEP]
show "P 0\<^sub>h (of_complex x) v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P 0\<^sub>h (of_complex x) v
[PROOF STEP]
proof (cases "of_complex x = 0\<^sub>h")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. of_complex x = 0\<^sub>h \<Longrightarrow> P 0\<^sub>h (of_complex x) v
 2. of_complex x \<noteq> 0\<^sub>h \<Longrightarrow> P 0\<^sub>h (of_complex x) v
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
of_complex x = 0\<^sub>h

goal (2 subgoals):
 1. of_complex x = 0\<^sub>h \<Longrightarrow> P 0\<^sub>h (of_complex x) v
 2. of_complex x \<noteq> 0\<^sub>h \<Longrightarrow> P 0\<^sub>h (of_complex x) v
[PROOF STEP]
show "P 0\<^sub>h (of_complex x) v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P 0\<^sub>h (of_complex x) v
[PROOF STEP]
proof (cases "v = 0\<^sub>h")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. v = 0\<^sub>h \<Longrightarrow> P 0\<^sub>h (of_complex x) v
 2. v \<noteq> 0\<^sub>h \<Longrightarrow> P 0\<^sub>h (of_complex x) v
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
v = 0\<^sub>h

goal (2 subgoals):
 1. v = 0\<^sub>h \<Longrightarrow> P 0\<^sub>h (of_complex x) v
 2. v \<noteq> 0\<^sub>h \<Longrightarrow> P 0\<^sub>h (of_complex x) v
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
v = 0\<^sub>h

goal (1 subgoal):
 1. P 0\<^sub>h (of_complex x) v
[PROOF STEP]
using \<open>of_complex x = 0\<^sub>h\<close>
[PROOF STATE]
proof (prove)
using this:
v = 0\<^sub>h
of_complex x = 0\<^sub>h

goal (1 subgoal):
 1. P 0\<^sub>h (of_complex x) v
[PROOF STEP]
using axes[of 0 0]
[PROOF STATE]
proof (prove)
using this:
v = 0\<^sub>h
of_complex x = 0\<^sub>h
\<lbrakk>is_real 0; 0 \<le> Re 0; Re 0 < 1; is_imag 0; 0 \<le> Im 0; Im 0 < 1\<rbrakk> \<Longrightarrow> P 0\<^sub>h (of_complex 0) (of_complex 0)

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

goal (1 subgoal):
 1. v \<noteq> 0\<^sub>h \<Longrightarrow> P 0\<^sub>h (of_complex x) v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v \<noteq> 0\<^sub>h \<Longrightarrow> P 0\<^sub>h (of_complex x) v
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
v \<noteq> 0\<^sub>h

goal (1 subgoal):
 1. v \<noteq> 0\<^sub>h \<Longrightarrow> P 0\<^sub>h (of_complex x) v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P 0\<^sub>h (of_complex x) v
[PROOF STEP]
proof (rule wlog_rotation_to_positive_y_axis)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. v \<in> unit_disc
 2. v \<noteq> 0\<^sub>h
 3. \<And>\<phi> u. \<lbrakk>u \<in> unit_disc; u \<noteq> 0\<^sub>h; P 0\<^sub>h (of_complex x) (moebius_pt (moebius_rotation \<phi>) u)\<rbrakk> \<Longrightarrow> P 0\<^sub>h (of_complex x) u
 4. \<And>xa. \<lbrakk>is_imag xa; 0 < Im xa; Im xa < 1\<rbrakk> \<Longrightarrow> P 0\<^sub>h (of_complex x) (of_complex xa)
[PROOF STEP]
show "v \<in> unit_disc" "v \<noteq> 0\<^sub>h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> unit_disc &&& v \<noteq> 0\<^sub>h
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
v \<in> unit_disc
v \<noteq> 0\<^sub>h

goal (2 subgoals):
 1. \<And>\<phi> u. \<lbrakk>u \<in> unit_disc; u \<noteq> 0\<^sub>h; P 0\<^sub>h (of_complex x) (moebius_pt (moebius_rotation \<phi>) u)\<rbrakk> \<Longrightarrow> P 0\<^sub>h (of_complex x) u
 2. \<And>xa. \<lbrakk>is_imag xa; 0 < Im xa; Im xa < 1\<rbrakk> \<Longrightarrow> P 0\<^sub>h (of_complex x) (of_complex xa)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<phi> u. \<lbrakk>u \<in> unit_disc; u \<noteq> 0\<^sub>h; P 0\<^sub>h (of_complex x) (moebius_pt (moebius_rotation \<phi>) u)\<rbrakk> \<Longrightarrow> P 0\<^sub>h (of_complex x) u
 2. \<And>xa. \<lbrakk>is_imag xa; 0 < Im xa; Im xa < 1\<rbrakk> \<Longrightarrow> P 0\<^sub>h (of_complex x) (of_complex xa)
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<phi> u. \<lbrakk>u \<in> unit_disc; u \<noteq> 0\<^sub>h; P 0\<^sub>h (of_complex x) (moebius_pt (moebius_rotation \<phi>) u)\<rbrakk> \<Longrightarrow> P 0\<^sub>h (of_complex x) u
 2. \<And>xa. \<lbrakk>is_imag xa; 0 < Im xa; Im xa < 1\<rbrakk> \<Longrightarrow> P 0\<^sub>h (of_complex x) (of_complex xa)
[PROOF STEP]
assume "is_imag y" "0 < Im y" "Im y < 1"
[PROOF STATE]
proof (state)
this:
is_imag y
0 < Im y
Im y < 1

goal (2 subgoals):
 1. \<And>\<phi> u. \<lbrakk>u \<in> unit_disc; u \<noteq> 0\<^sub>h; P 0\<^sub>h (of_complex x) (moebius_pt (moebius_rotation \<phi>) u)\<rbrakk> \<Longrightarrow> P 0\<^sub>h (of_complex x) u
 2. \<And>xa. \<lbrakk>is_imag xa; 0 < Im xa; Im xa < 1\<rbrakk> \<Longrightarrow> P 0\<^sub>h (of_complex x) (of_complex xa)
[PROOF STEP]
thus "P 0\<^sub>h (of_complex x) (of_complex y)"
[PROOF STATE]
proof (prove)
using this:
is_imag y
0 < Im y
Im y < 1

goal (1 subgoal):
 1. P 0\<^sub>h (of_complex x) (of_complex y)
[PROOF STEP]
using x axes[of x y]
[PROOF STATE]
proof (prove)
using this:
is_imag y
0 < Im y
Im y < 1
is_real x
0 \<le> Re x
Re x < 1
\<lbrakk>is_real x; 0 \<le> Re x; Re x < 1; is_imag y; 0 \<le> Im y; Im y < 1\<rbrakk> \<Longrightarrow> P 0\<^sub>h (of_complex x) (of_complex y)

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

goal (1 subgoal):
 1. \<And>\<phi> u. \<lbrakk>u \<in> unit_disc; u \<noteq> 0\<^sub>h; P 0\<^sub>h (of_complex x) (moebius_pt (moebius_rotation \<phi>) u)\<rbrakk> \<Longrightarrow> P 0\<^sub>h (of_complex x) u
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<phi> u. \<lbrakk>u \<in> unit_disc; u \<noteq> 0\<^sub>h; P 0\<^sub>h (of_complex x) (moebius_pt (moebius_rotation \<phi>) u)\<rbrakk> \<Longrightarrow> P 0\<^sub>h (of_complex x) u
[PROOF STEP]
fix \<phi> u
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<phi> u. \<lbrakk>u \<in> unit_disc; u \<noteq> 0\<^sub>h; P 0\<^sub>h (of_complex x) (moebius_pt (moebius_rotation \<phi>) u)\<rbrakk> \<Longrightarrow> P 0\<^sub>h (of_complex x) u
[PROOF STEP]
assume "u \<in> unit_disc" "u \<noteq> 0\<^sub>h"
                   "P 0\<^sub>h (of_complex x) (moebius_pt (moebius_rotation \<phi>) u)"
[PROOF STATE]
proof (state)
this:
u \<in> unit_disc
u \<noteq> 0\<^sub>h
P 0\<^sub>h (of_complex x) (moebius_pt (moebius_rotation \<phi>) u)

goal (1 subgoal):
 1. \<And>\<phi> u. \<lbrakk>u \<in> unit_disc; u \<noteq> 0\<^sub>h; P 0\<^sub>h (of_complex x) (moebius_pt (moebius_rotation \<phi>) u)\<rbrakk> \<Longrightarrow> P 0\<^sub>h (of_complex x) u
[PROOF STEP]
thus "P 0\<^sub>h (of_complex x) u"
[PROOF STATE]
proof (prove)
using this:
u \<in> unit_disc
u \<noteq> 0\<^sub>h
P 0\<^sub>h (of_complex x) (moebius_pt (moebius_rotation \<phi>) u)

goal (1 subgoal):
 1. P 0\<^sub>h (of_complex x) u
[PROOF STEP]
using \<open>of_complex x = 0\<^sub>h\<close>
[PROOF STATE]
proof (prove)
using this:
u \<in> unit_disc
u \<noteq> 0\<^sub>h
P 0\<^sub>h (of_complex x) (moebius_pt (moebius_rotation \<phi>) u)
of_complex x = 0\<^sub>h

goal (1 subgoal):
 1. P 0\<^sub>h (of_complex x) u
[PROOF STEP]
using moebius[of "moebius_rotation \<phi>"  "0\<^sub>h" "0\<^sub>h" u]
[PROOF STATE]
proof (prove)
using this:
u \<in> unit_disc
u \<noteq> 0\<^sub>h
P 0\<^sub>h (of_complex x) (moebius_pt (moebius_rotation \<phi>) u)
of_complex x = 0\<^sub>h
\<lbrakk>unit_disc_fix (moebius_rotation \<phi>); 0\<^sub>h \<in> unit_disc; 0\<^sub>h \<in> unit_disc; u \<in> unit_disc; P (moebius_pt (moebius_rotation \<phi>) 0\<^sub>h) (moebius_pt (moebius_rotation \<phi>) 0\<^sub>h) (moebius_pt (moebius_rotation \<phi>) u)\<rbrakk> \<Longrightarrow> P 0\<^sub>h 0\<^sub>h u

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P 0\<^sub>h (of_complex x) v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P 0\<^sub>h (of_complex x) v

goal (1 subgoal):
 1. of_complex x \<noteq> 0\<^sub>h \<Longrightarrow> P 0\<^sub>h (of_complex x) v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. of_complex x \<noteq> 0\<^sub>h \<Longrightarrow> P 0\<^sub>h (of_complex x) v
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
of_complex x \<noteq> 0\<^sub>h

goal (1 subgoal):
 1. of_complex x \<noteq> 0\<^sub>h \<Longrightarrow> P 0\<^sub>h (of_complex x) v
[PROOF STEP]
hence *: "poincare_line 0\<^sub>h (of_complex x) = x_axis"
[PROOF STATE]
proof (prove)
using this:
of_complex x \<noteq> 0\<^sub>h

goal (1 subgoal):
 1. poincare_line 0\<^sub>h (of_complex x) = x_axis
[PROOF STEP]
using x poincare_line_0_real_is_x_axis[of "of_complex x"]
[PROOF STATE]
proof (prove)
using this:
of_complex x \<noteq> 0\<^sub>h
is_real x
0 \<le> Re x
Re x < 1
\<lbrakk>of_complex x \<in> circline_set x_axis; of_complex x \<noteq> 0\<^sub>h; of_complex x \<noteq> \<infinity>\<^sub>h\<rbrakk> \<Longrightarrow> poincare_line 0\<^sub>h (of_complex x) = x_axis

goal (1 subgoal):
 1. poincare_line 0\<^sub>h (of_complex x) = x_axis
[PROOF STEP]
unfolding circline_set_x_axis
[PROOF STATE]
proof (prove)
using this:
of_complex x \<noteq> 0\<^sub>h
is_real x
0 \<le> Re x
Re x < 1
\<lbrakk>of_complex x \<in> of_complex ` {x. is_real x} \<union> {\<infinity>\<^sub>h}; of_complex x \<noteq> 0\<^sub>h; of_complex x \<noteq> \<infinity>\<^sub>h\<rbrakk> \<Longrightarrow> poincare_line 0\<^sub>h (of_complex x) = x_axis

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

goal (1 subgoal):
 1. of_complex x \<noteq> 0\<^sub>h \<Longrightarrow> P 0\<^sub>h (of_complex x) v
[PROOF STEP]
hence "H1 = x_axis"
[PROOF STATE]
proof (prove)
using this:
poincare_line 0\<^sub>h (of_complex x) = x_axis

goal (1 subgoal):
 1. H1 = x_axis
[PROOF STEP]
using unique_poincare_line[of "0\<^sub>h" "of_complex x" H1] 1 2
[PROOF STATE]
proof (prove)
using this:
poincare_line 0\<^sub>h (of_complex x) = x_axis
\<lbrakk>0\<^sub>h \<noteq> of_complex x; 0\<^sub>h \<in> unit_disc; of_complex x \<in> unit_disc; 0\<^sub>h \<in> circline_set H1; of_complex x \<in> circline_set H1; is_poincare_line H1\<rbrakk> \<Longrightarrow> H1 = poincare_line 0\<^sub>h (of_complex x)
is_poincare_line H1
is_poincare_line H2
perpendicular H1 H2
0\<^sub>h \<in> circline_set H1
0\<^sub>h \<in> circline_set H2
of_complex x \<in> circline_set H1
v \<in> circline_set H2

goal (1 subgoal):
 1. H1 = x_axis
[PROOF STEP]
using \<open>of_complex x \<in> unit_disc\<close> False
[PROOF STATE]
proof (prove)
using this:
poincare_line 0\<^sub>h (of_complex x) = x_axis
\<lbrakk>0\<^sub>h \<noteq> of_complex x; 0\<^sub>h \<in> unit_disc; of_complex x \<in> unit_disc; 0\<^sub>h \<in> circline_set H1; of_complex x \<in> circline_set H1; is_poincare_line H1\<rbrakk> \<Longrightarrow> H1 = poincare_line 0\<^sub>h (of_complex x)
is_poincare_line H1
is_poincare_line H2
perpendicular H1 H2
0\<^sub>h \<in> circline_set H1
0\<^sub>h \<in> circline_set H2
of_complex x \<in> circline_set H1
v \<in> circline_set H2
of_complex x \<in> unit_disc
of_complex x \<noteq> 0\<^sub>h

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

goal (1 subgoal):
 1. of_complex x \<noteq> 0\<^sub>h \<Longrightarrow> P 0\<^sub>h (of_complex x) v
[PROOF STEP]
have "is_imag y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_imag y
[PROOF STEP]
proof (cases "y = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y = 0 \<Longrightarrow> is_imag y
 2. y \<noteq> 0 \<Longrightarrow> is_imag y
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
y = 0

goal (2 subgoals):
 1. y = 0 \<Longrightarrow> is_imag y
 2. y \<noteq> 0 \<Longrightarrow> is_imag y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
y = 0

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

goal (1 subgoal):
 1. y \<noteq> 0 \<Longrightarrow> is_imag y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y \<noteq> 0 \<Longrightarrow> is_imag y
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
y \<noteq> 0

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

goal (1 subgoal):
 1. 0\<^sub>h \<noteq> of_complex y
[PROOF STEP]
using of_complex_zero_iff[of y]
[PROOF STATE]
proof (prove)
using this:
y \<noteq> 0
(of_complex y = 0\<^sub>h) = (y = 0)

goal (1 subgoal):
 1. 0\<^sub>h \<noteq> of_complex y
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
0\<^sub>h \<noteq> of_complex y

goal (1 subgoal):
 1. y \<noteq> 0 \<Longrightarrow> is_imag y
[PROOF STEP]
hence "H2 = poincare_line 0\<^sub>h (of_complex y)"
[PROOF STATE]
proof (prove)
using this:
0\<^sub>h \<noteq> of_complex y

goal (1 subgoal):
 1. H2 = poincare_line 0\<^sub>h (of_complex y)
[PROOF STEP]
using 1 2 \<open>v \<in> unit_disc\<close>
[PROOF STATE]
proof (prove)
using this:
0\<^sub>h \<noteq> of_complex y
is_poincare_line H1
is_poincare_line H2
perpendicular H1 H2
0\<^sub>h \<in> circline_set H1
0\<^sub>h \<in> circline_set H2
of_complex x \<in> circline_set H1
v \<in> circline_set H2
v \<in> unit_disc

goal (1 subgoal):
 1. H2 = poincare_line 0\<^sub>h (of_complex y)
[PROOF STEP]
using unique_poincare_line[of "0\<^sub>h" "of_complex y" H2] y
[PROOF STATE]
proof (prove)
using this:
0\<^sub>h \<noteq> of_complex y
is_poincare_line H1
is_poincare_line H2
perpendicular H1 H2
0\<^sub>h \<in> circline_set H1
0\<^sub>h \<in> circline_set H2
of_complex x \<in> circline_set H1
v \<in> circline_set H2
v \<in> unit_disc
\<lbrakk>0\<^sub>h \<noteq> of_complex y; 0\<^sub>h \<in> unit_disc; of_complex y \<in> unit_disc; 0\<^sub>h \<in> circline_set H2; of_complex y \<in> circline_set H2; is_poincare_line H2\<rbrakk> \<Longrightarrow> H2 = poincare_line 0\<^sub>h (of_complex y)
v = of_complex y

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

goal (1 subgoal):
 1. y \<noteq> 0 \<Longrightarrow> is_imag y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
H2 = poincare_line 0\<^sub>h (of_complex y)

goal (1 subgoal):
 1. is_imag y
[PROOF STEP]
using 1 \<open>H1 = x_axis\<close>
[PROOF STATE]
proof (prove)
using this:
H2 = poincare_line 0\<^sub>h (of_complex y)
is_poincare_line H1
is_poincare_line H2
perpendicular H1 H2
H1 = x_axis

goal (1 subgoal):
 1. is_imag y
[PROOF STEP]
using perpendicular_to_x_axis_y_axis[of y] False
[PROOF STATE]
proof (prove)
using this:
H2 = poincare_line 0\<^sub>h (of_complex y)
is_poincare_line H1
is_poincare_line H2
perpendicular H1 H2
H1 = x_axis
\<lbrakk>perpendicular_to_x_axis (poincare_line 0\<^sub>h (of_complex y)); y \<noteq> 0\<rbrakk> \<Longrightarrow> is_imag y
y \<noteq> 0

goal (1 subgoal):
 1. is_imag y
[PROOF STEP]
using perpendicular_to_x_axis[of H2]
[PROOF STATE]
proof (prove)
using this:
H2 = poincare_line 0\<^sub>h (of_complex y)
is_poincare_line H1
is_poincare_line H2
perpendicular H1 H2
H1 = x_axis
\<lbrakk>perpendicular_to_x_axis (poincare_line 0\<^sub>h (of_complex y)); y \<noteq> 0\<rbrakk> \<Longrightarrow> is_imag y
y \<noteq> 0
is_poincare_line H2 \<Longrightarrow> perpendicular_to_x_axis H2 = perpendicular x_axis H2

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

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

goal (1 subgoal):
 1. of_complex x \<noteq> 0\<^sub>h \<Longrightarrow> P 0\<^sub>h (of_complex x) v
[PROOF STEP]
show "P 0\<^sub>h (of_complex x) v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P 0\<^sub>h (of_complex x) v
[PROOF STEP]
proof (cases "Im y \<ge> 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 \<le> Im y \<Longrightarrow> P 0\<^sub>h (of_complex x) v
 2. \<not> 0 \<le> Im y \<Longrightarrow> P 0\<^sub>h (of_complex x) v
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
0 \<le> Im y

goal (2 subgoals):
 1. 0 \<le> Im y \<Longrightarrow> P 0\<^sub>h (of_complex x) v
 2. \<not> 0 \<le> Im y \<Longrightarrow> P 0\<^sub>h (of_complex x) v
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
0 \<le> Im y

goal (1 subgoal):
 1. P 0\<^sub>h (of_complex x) v
[PROOF STEP]
using axes[of x y] x y \<open>is_imag y\<close> \<open>v \<in> unit_disc\<close>
[PROOF STATE]
proof (prove)
using this:
0 \<le> Im y
\<lbrakk>is_real x; 0 \<le> Re x; Re x < 1; is_imag y; 0 \<le> Im y; Im y < 1\<rbrakk> \<Longrightarrow> P 0\<^sub>h (of_complex x) (of_complex y)
is_real x
0 \<le> Re x
Re x < 1
v = of_complex y
is_imag y
v \<in> unit_disc

goal (1 subgoal):
 1. P 0\<^sub>h (of_complex x) v
[PROOF STEP]
by (simp add: cmod_eq_Im)
[PROOF STATE]
proof (state)
this:
P 0\<^sub>h (of_complex x) v

goal (1 subgoal):
 1. \<not> 0 \<le> Im y \<Longrightarrow> P 0\<^sub>h (of_complex x) v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> 0 \<le> Im y \<Longrightarrow> P 0\<^sub>h (of_complex x) v
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> 0 \<le> Im y

goal (1 subgoal):
 1. \<not> 0 \<le> Im y \<Longrightarrow> P 0\<^sub>h (of_complex x) v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P 0\<^sub>h (of_complex x) v
[PROOF STEP]
proof (rule conjugate)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. 0\<^sub>h \<in> unit_disc
 2. of_complex x \<in> unit_disc
 3. v \<in> unit_disc
 4. P (conjugate 0\<^sub>h) (conjugate (of_complex x)) (conjugate v)
[PROOF STEP]
have "Im (cnj y) < 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Im (cnj y) < 1
[PROOF STEP]
using \<open>v \<in> unit_disc\<close> y \<open>is_imag y\<close> eq_minus_cnj_iff_imag[of y]
[PROOF STATE]
proof (prove)
using this:
v \<in> unit_disc
v = of_complex y
is_imag y
(cnj y = - y) = is_imag y

goal (1 subgoal):
 1. Im (cnj y) < 1
[PROOF STEP]
by (simp add: cmod_eq_Im)
[PROOF STATE]
proof (state)
this:
Im (cnj y) < 1

goal (4 subgoals):
 1. 0\<^sub>h \<in> unit_disc
 2. of_complex x \<in> unit_disc
 3. v \<in> unit_disc
 4. P (conjugate 0\<^sub>h) (conjugate (of_complex x)) (conjugate v)
[PROOF STEP]
thus "P (conjugate 0\<^sub>h) (conjugate (of_complex x)) (conjugate v)"
[PROOF STATE]
proof (prove)
using this:
Im (cnj y) < 1

goal (1 subgoal):
 1. P (conjugate 0\<^sub>h) (conjugate (of_complex x)) (conjugate v)
[PROOF STEP]
using \<open>is_real x\<close> eq_cnj_iff_real[of x] y \<open>is_imag y\<close>
[PROOF STATE]
proof (prove)
using this:
Im (cnj y) < 1
is_real x
(cnj x = x) = is_real x
v = of_complex y
is_imag y

goal (1 subgoal):
 1. P (conjugate 0\<^sub>h) (conjugate (of_complex x)) (conjugate v)
[PROOF STEP]
using axes[OF x, of "cnj y"] False
[PROOF STATE]
proof (prove)
using this:
Im (cnj y) < 1
is_real x
(cnj x = x) = is_real x
v = of_complex y
is_imag y
\<lbrakk>is_imag (cnj y); 0 \<le> Im (cnj y); Im (cnj y) < 1\<rbrakk> \<Longrightarrow> P 0\<^sub>h (of_complex x) (of_complex (cnj y))
\<not> 0 \<le> Im y

goal (1 subgoal):
 1. P (conjugate 0\<^sub>h) (conjugate (of_complex x)) (conjugate v)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P (conjugate 0\<^sub>h) (conjugate (of_complex x)) (conjugate v)

goal (3 subgoals):
 1. 0\<^sub>h \<in> unit_disc
 2. of_complex x \<in> unit_disc
 3. v \<in> unit_disc
[PROOF STEP]
show "0\<^sub>h \<in> unit_disc" "of_complex x \<in> unit_disc" "v \<in> unit_disc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0\<^sub>h \<in> unit_disc &&& of_complex x \<in> unit_disc &&& v \<in> unit_disc
[PROOF STEP]
by (simp, fact+)
[PROOF STATE]
proof (state)
this:
0\<^sub>h \<in> unit_disc
of_complex x \<in> unit_disc
v \<in> unit_disc

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P 0\<^sub>h (of_complex x) v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P 0\<^sub>h (of_complex x) v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P 0\<^sub>h (of_complex x) v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>v H1 H2. is_poincare_line H1 \<and> is_poincare_line H2 \<and> perpendicular H1 H2 \<and> 0\<^sub>h \<in> circline_set H1 \<inter> circline_set H2 \<and> of_complex x \<in> circline_set H1 \<and> v \<in> circline_set H2 \<and> v \<in> unit_disc \<longrightarrow> P 0\<^sub>h (of_complex x) v

goal (3 subgoals):
 1. z \<in> unit_disc
 2. u \<in> unit_disc
 3. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; \<forall>va H1 H2. is_poincare_line H1 \<and> is_poincare_line H2 \<and> perpendicular H1 H2 \<and> moebius_pt M u \<in> circline_set H1 \<inter> circline_set H2 \<and> moebius_pt M v \<in> circline_set H1 \<and> va \<in> circline_set H2 \<and> va \<in> unit_disc \<longrightarrow> P (moebius_pt M u) (moebius_pt M v) va\<rbrakk> \<Longrightarrow> \<forall>va H1 H2. is_poincare_line H1 \<and> is_poincare_line H2 \<and> perpendicular H1 H2 \<and> u \<in> circline_set H1 \<inter> circline_set H2 \<and> v \<in> circline_set H1 \<and> va \<in> circline_set H2 \<and> va \<in> unit_disc \<longrightarrow> P u v va
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. z \<in> unit_disc
 2. u \<in> unit_disc
 3. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; \<forall>va H1 H2. is_poincare_line H1 \<and> is_poincare_line H2 \<and> perpendicular H1 H2 \<and> moebius_pt M u \<in> circline_set H1 \<inter> circline_set H2 \<and> moebius_pt M v \<in> circline_set H1 \<and> va \<in> circline_set H2 \<and> va \<in> unit_disc \<longrightarrow> P (moebius_pt M u) (moebius_pt M v) va\<rbrakk> \<Longrightarrow> \<forall>va H1 H2. is_poincare_line H1 \<and> is_poincare_line H2 \<and> perpendicular H1 H2 \<and> u \<in> circline_set H1 \<inter> circline_set H2 \<and> v \<in> circline_set H1 \<and> va \<in> circline_set H2 \<and> va \<in> unit_disc \<longrightarrow> P u v va
[PROOF STEP]
show "z \<in> unit_disc" "u \<in> unit_disc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<in> unit_disc &&& u \<in> unit_disc
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
z \<in> unit_disc
u \<in> unit_disc

goal (1 subgoal):
 1. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; \<forall>va H1 H2. is_poincare_line H1 \<and> is_poincare_line H2 \<and> perpendicular H1 H2 \<and> moebius_pt M u \<in> circline_set H1 \<inter> circline_set H2 \<and> moebius_pt M v \<in> circline_set H1 \<and> va \<in> circline_set H2 \<and> va \<in> unit_disc \<longrightarrow> P (moebius_pt M u) (moebius_pt M v) va\<rbrakk> \<Longrightarrow> \<forall>va H1 H2. is_poincare_line H1 \<and> is_poincare_line H2 \<and> perpendicular H1 H2 \<and> u \<in> circline_set H1 \<inter> circline_set H2 \<and> v \<in> circline_set H1 \<and> va \<in> circline_set H2 \<and> va \<in> unit_disc \<longrightarrow> P u v va
[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; \<forall>va H1 H2. is_poincare_line H1 \<and> is_poincare_line H2 \<and> perpendicular H1 H2 \<and> moebius_pt M u \<in> circline_set H1 \<inter> circline_set H2 \<and> moebius_pt M v \<in> circline_set H1 \<and> va \<in> circline_set H2 \<and> va \<in> unit_disc \<longrightarrow> P (moebius_pt M u) (moebius_pt M v) va\<rbrakk> \<Longrightarrow> \<forall>va H1 H2. is_poincare_line H1 \<and> is_poincare_line H2 \<and> perpendicular H1 H2 \<and> u \<in> circline_set H1 \<inter> circline_set H2 \<and> v \<in> circline_set H1 \<and> va \<in> circline_set H2 \<and> va \<in> unit_disc \<longrightarrow> P u v va
[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; \<forall>va H1 H2. is_poincare_line H1 \<and> is_poincare_line H2 \<and> perpendicular H1 H2 \<and> moebius_pt M u \<in> circline_set H1 \<inter> circline_set H2 \<and> moebius_pt M v \<in> circline_set H1 \<and> va \<in> circline_set H2 \<and> va \<in> unit_disc \<longrightarrow> P (moebius_pt M u) (moebius_pt M v) va\<rbrakk> \<Longrightarrow> \<forall>va H1 H2. is_poincare_line H1 \<and> is_poincare_line H2 \<and> perpendicular H1 H2 \<and> u \<in> circline_set H1 \<inter> circline_set H2 \<and> v \<in> circline_set H1 \<and> va \<in> circline_set H2 \<and> va \<in> unit_disc \<longrightarrow> P u v va
[PROOF STEP]
assume *: "unit_disc_fix M" "u \<in> unit_disc" "v \<in> unit_disc"
[PROOF STATE]
proof (state)
this:
unit_disc_fix M
u \<in> unit_disc
v \<in> unit_disc

goal (1 subgoal):
 1. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; \<forall>va H1 H2. is_poincare_line H1 \<and> is_poincare_line H2 \<and> perpendicular H1 H2 \<and> moebius_pt M u \<in> circline_set H1 \<inter> circline_set H2 \<and> moebius_pt M v \<in> circline_set H1 \<and> va \<in> circline_set H2 \<and> va \<in> unit_disc \<longrightarrow> P (moebius_pt M u) (moebius_pt M v) va\<rbrakk> \<Longrightarrow> \<forall>va H1 H2. is_poincare_line H1 \<and> is_poincare_line H2 \<and> perpendicular H1 H2 \<and> u \<in> circline_set H1 \<inter> circline_set H2 \<and> v \<in> circline_set H1 \<and> va \<in> circline_set H2 \<and> va \<in> unit_disc \<longrightarrow> P u v va
[PROOF STEP]
assume **: "?P (moebius_pt M u) (moebius_pt M v)"
[PROOF STATE]
proof (state)
this:
\<forall>v H1 H2. is_poincare_line H1 \<and> is_poincare_line H2 \<and> perpendicular H1 H2 \<and> moebius_pt M u \<in> circline_set H1 \<inter> circline_set H2 \<and> moebius_pt M v \<in> circline_set H1 \<and> v \<in> circline_set H2 \<and> v \<in> unit_disc \<longrightarrow> P (moebius_pt M u) (moebius_pt M v) v

goal (1 subgoal):
 1. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; \<forall>va H1 H2. is_poincare_line H1 \<and> is_poincare_line H2 \<and> perpendicular H1 H2 \<and> moebius_pt M u \<in> circline_set H1 \<inter> circline_set H2 \<and> moebius_pt M v \<in> circline_set H1 \<and> va \<in> circline_set H2 \<and> va \<in> unit_disc \<longrightarrow> P (moebius_pt M u) (moebius_pt M v) va\<rbrakk> \<Longrightarrow> \<forall>va H1 H2. is_poincare_line H1 \<and> is_poincare_line H2 \<and> perpendicular H1 H2 \<and> u \<in> circline_set H1 \<inter> circline_set H2 \<and> v \<in> circline_set H1 \<and> va \<in> circline_set H2 \<and> va \<in> unit_disc \<longrightarrow> P u v va
[PROOF STEP]
show "?P u v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>v H1 H2. is_poincare_line H1 \<and> is_poincare_line H2 \<and> perpendicular H1 H2 \<and> u \<in> circline_set H1 \<inter> circline_set H2 \<and> v \<in> circline_set H1 \<and> v \<in> circline_set H2 \<and> v \<in> unit_disc \<longrightarrow> P u v v
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v H1 H2. \<lbrakk>is_poincare_line H1; is_poincare_line H2; perpendicular H1 H2; u \<in> circline_set H1; u \<in> circline_set H2; v \<in> circline_set H1; v \<in> circline_set H2; v \<in> unit_disc\<rbrakk> \<Longrightarrow> P u v v
[PROOF STEP]
fix w H1 H2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v H1 H2. \<lbrakk>is_poincare_line H1; is_poincare_line H2; perpendicular H1 H2; u \<in> circline_set H1; u \<in> circline_set H2; v \<in> circline_set H1; v \<in> circline_set H2; v \<in> unit_disc\<rbrakk> \<Longrightarrow> P u v v
[PROOF STEP]
assume ***: "is_poincare_line H1" "is_poincare_line H2" "perpendicular H1 H2"
                  "u \<in> circline_set H1" "u \<in> circline_set H2"
                  "v \<in> circline_set H1" "w \<in> circline_set H2" "w \<in> unit_disc"
[PROOF STATE]
proof (state)
this:
is_poincare_line H1
is_poincare_line H2
perpendicular H1 H2
u \<in> circline_set H1
u \<in> circline_set H2
v \<in> circline_set H1
w \<in> circline_set H2
w \<in> unit_disc

goal (1 subgoal):
 1. \<And>v H1 H2. \<lbrakk>is_poincare_line H1; is_poincare_line H2; perpendicular H1 H2; u \<in> circline_set H1; u \<in> circline_set H2; v \<in> circline_set H1; v \<in> circline_set H2; v \<in> unit_disc\<rbrakk> \<Longrightarrow> P u v v
[PROOF STEP]
thus "P u v w"
[PROOF STATE]
proof (prove)
using this:
is_poincare_line H1
is_poincare_line H2
perpendicular H1 H2
u \<in> circline_set H1
u \<in> circline_set H2
v \<in> circline_set H1
w \<in> circline_set H2
w \<in> unit_disc

goal (1 subgoal):
 1. P u v w
[PROOF STEP]
using moebius[of M u v w] *
[PROOF STATE]
proof (prove)
using this:
is_poincare_line H1
is_poincare_line H2
perpendicular H1 H2
u \<in> circline_set H1
u \<in> circline_set H2
v \<in> circline_set H1
w \<in> circline_set H2
w \<in> unit_disc
\<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; P (moebius_pt M u) (moebius_pt M v) (moebius_pt M w)\<rbrakk> \<Longrightarrow> P u v w
unit_disc_fix M
u \<in> unit_disc
v \<in> unit_disc

goal (1 subgoal):
 1. P u v w
[PROOF STEP]
using **[rule_format, of "moebius_circline M H1" "moebius_circline M H2" "moebius_pt M w"]
[PROOF STATE]
proof (prove)
using this:
is_poincare_line H1
is_poincare_line H2
perpendicular H1 H2
u \<in> circline_set H1
u \<in> circline_set H2
v \<in> circline_set H1
w \<in> circline_set H2
w \<in> unit_disc
\<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; w \<in> unit_disc; P (moebius_pt M u) (moebius_pt M v) (moebius_pt M w)\<rbrakk> \<Longrightarrow> P u v w
unit_disc_fix M
u \<in> unit_disc
v \<in> unit_disc
is_poincare_line (moebius_circline M H1) \<and> is_poincare_line (moebius_circline M H2) \<and> perpendicular (moebius_circline M H1) (moebius_circline M H2) \<and> moebius_pt M u \<in> circline_set (moebius_circline M H1) \<inter> circline_set (moebius_circline M H2) \<and> moebius_pt M v \<in> circline_set (moebius_circline M H1) \<and> moebius_pt M w \<in> circline_set (moebius_circline M H2) \<and> moebius_pt M w \<in> unit_disc \<Longrightarrow> P (moebius_pt M u) (moebius_pt M v) (moebius_pt M w)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>v H1 H2. is_poincare_line H1 \<and> is_poincare_line H2 \<and> perpendicular H1 H2 \<and> u \<in> circline_set H1 \<inter> circline_set H2 \<and> v \<in> circline_set H1 \<and> v \<in> circline_set H2 \<and> v \<in> unit_disc \<longrightarrow> P u v v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>v H1 H2. is_poincare_line H1 \<and> is_poincare_line H2 \<and> perpendicular H1 H2 \<and> z \<in> circline_set H1 \<inter> circline_set H2 \<and> u \<in> circline_set H1 \<and> v \<in> circline_set H2 \<and> v \<in> unit_disc \<longrightarrow> P z u v

goal (1 subgoal):
 1. P z u v
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>v H1 H2. is_poincare_line H1 \<and> is_poincare_line H2 \<and> perpendicular H1 H2 \<and> z \<in> circline_set H1 \<inter> circline_set H2 \<and> u \<in> circline_set H1 \<and> v \<in> circline_set H2 \<and> v \<in> unit_disc \<longrightarrow> P z u v

goal (1 subgoal):
 1. P z u v
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>v H1 H2. is_poincare_line H1 \<and> is_poincare_line H2 \<and> perpendicular H1 H2 \<and> z \<in> circline_set H1 \<inter> circline_set H2 \<and> u \<in> circline_set H1 \<and> v \<in> circline_set H2 \<and> v \<in> unit_disc \<longrightarrow> P z u v
u \<in> unit_disc
v \<in> unit_disc
z \<in> unit_disc
is_poincare_line H1
is_poincare_line H2
perpendicular H1 H2
z \<in> circline_set H1 \<inter> circline_set H2
u \<in> circline_set H1
v \<in> circline_set H2
\<lbrakk>is_real ?x; 0 \<le> Re ?x; Re ?x < 1; is_imag ?y; 0 \<le> Im ?y; Im ?y < 1\<rbrakk> \<Longrightarrow> P 0\<^sub>h (of_complex ?x) (of_complex ?y)
\<lbrakk>unit_disc_fix ?M; ?u \<in> unit_disc; ?v \<in> unit_disc; ?w \<in> unit_disc; P (moebius_pt ?M ?u) (moebius_pt ?M ?v) (moebius_pt ?M ?w)\<rbrakk> \<Longrightarrow> P ?u ?v ?w
\<lbrakk>?u \<in> unit_disc; ?v \<in> unit_disc; ?w \<in> unit_disc; P (conjugate ?u) (conjugate ?v) (conjugate ?w)\<rbrakk> \<Longrightarrow> P ?u ?v ?w

goal (1 subgoal):
 1. P z u v
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P z u v

goal:
No subgoals!
[PROOF STEP]
qed