Theory Poincare
section‹Poincar\'e disc model types›
text ‹In this section we introduce datatypes that represent objects in the Poincar\'e disc model.
The types are defined as subtypes (e.g., the h-points are defined as elements of $\mathbb{C}P^1$
that lie within the unit disc). The functions on those types are defined by lifting the functions
defined on the carrier type (e.g., h-distance is defined by lifting the distance function defined
for elements of $\mathbb{C}P^1$).›
theory Poincare
imports Poincare_Lines Poincare_Between Poincare_Distance Poincare_Circles
begin
subsection ‹H-points›
typedef p_point = "{z. z ∈ unit_disc}"
using zero_in_unit_disc
by (rule_tac x="0⇩h" in exI, simp)
setup_lifting type_definition_p_point
text ‹Point zero›
lift_definition p_zero :: "p_point" is "0⇩h"
by (rule zero_in_unit_disc)
text ‹Constructing h-points from complex numbers›
lift_definition p_of_complex :: "complex ⇒ p_point" is "λ z. if cmod z < 1 then of_complex z else 0⇩h"
by auto
subsection ‹H-lines›
typedef p_line = "{H. is_poincare_line H}"
by (rule_tac x="x_axis" in exI, simp)
setup_lifting type_definition_p_line
lift_definition p_incident :: "p_line ⇒ p_point ⇒ bool" is on_circline
done
text ‹Set of h-points on an h-line›
definition p_points :: "p_line ⇒ p_point set" where
"p_points l = {p. p_incident l p}"
text ‹x-axis is an example of an h-line›
lift_definition p_x_axis :: "p_line" is x_axis
by simp
text ‹Constructing the unique h-line from two h-points›
lift_definition p_line :: "p_point ⇒ p_point ⇒ p_line" is poincare_line
proof-
fix u v
show "is_poincare_line (poincare_line u v)"
proof (cases "u ≠ v")
case True
thus ?thesis
by simp
next
text‹This branch must work only for formal reasons.›
case False
thus ?thesis
by (transfer, transfer, auto simp add: hermitean_def mat_adj_def mat_cnj_def split: if_split_asm)
qed
qed
text ‹Next we show how to lift some lemmas. This could be done for all the lemmas that we have
proved earlier, but we do not do that.›
text ‹If points are different then the constructed line contains the starting points›
lemma p_on_line:
assumes "z ≠ w"
shows "p_incident (p_line z w) z"
"p_incident (p_line z w) w"
using assms
by (transfer, simp)+
text ‹There is a unique h-line passing trough the two different given h-points›
lemma
assumes "u ≠ v"
shows "∃! l. {u, v} ⊆ p_points l"
using assms
apply (rule_tac a="p_line u v" in ex1I, auto simp add: p_points_def p_on_line)
apply (transfer, simp add: unique_poincare_line)
done
text ‹The unique h-line trough zero and a non-zero h-point on the x-axis is the x-axis›
lemma
assumes "p_zero ∈ p_points l" "u ∈ p_points l" "u ≠ p_zero" "u ∈ p_points p_x_axis"
shows "l = p_x_axis"
using assms
unfolding p_points_def
apply simp
apply transfer
using is_poincare_line_0_real_is_x_axis inf_notin_unit_disc
unfolding circline_set_def
by blast
subsection ‹H-collinearity›
lift_definition p_collinear :: "p_point set ⇒ bool" is poincare_collinear
done
subsection ‹H-isometries›
text ‹H-isometries are functions that map the unit disc onto itself›
typedef p_isometry = "{f. unit_disc_fix_f f}"
by (rule_tac x="id" in exI, simp add: unit_disc_fix_f_def, rule_tac x="id_moebius" in exI, simp)
setup_lifting type_definition_p_isometry
text ‹Action of an h-isometry on an h-point›
lift_definition p_isometry_pt :: "p_isometry ⇒ p_point ⇒ p_point" is "λ f p. f p"
using unit_disc_fix_f_unit_disc
by auto
text ‹Action of an h-isometry on an h-line›
lift_definition p_isometry_line :: "p_isometry ⇒ p_line ⇒ p_line" is "λ f l. unit_disc_fix_f_circline f l"
proof-
fix f H
assume "unit_disc_fix_f f" "is_poincare_line H"
then obtain M where "unit_disc_fix M" and *: "f = moebius_pt M ∨ f = moebius_pt M ∘ conjugate"
unfolding unit_disc_fix_f_def
by auto
show "is_poincare_line (unit_disc_fix_f_circline f H)"
using *
proof
assume "f = moebius_pt M"
thus ?thesis
using ‹unit_disc_fix M› ‹is_poincare_line H›
using unit_disc_fix_f_circline_direct[of M f H]
by auto
next
assume "f = moebius_pt M ∘ conjugate"
thus ?thesis
using ‹unit_disc_fix M› ‹is_poincare_line H›
using unit_disc_fix_f_circline_indirect[of M f H]
by auto
qed
qed
text ‹An example lemma about h-isometries.›
text ‹H-isometries preserve h-collinearity›
lemma p_collinear_p_isometry_pt [simp]:
shows "p_collinear (p_isometry_pt M ` A) ⟷ p_collinear A"
proof-
have *: "∀ M A. ((λx. moebius_pt M (conjugate x)) ` A = moebius_pt M ` (conjugate ` A))"
by auto
show ?thesis
by transfer (auto simp add: unit_disc_fix_f_def *)
qed
subsection ‹H-distance and h-congruence›
lift_definition p_dist :: "p_point ⇒ p_point ⇒ real" is poincare_distance
done
definition p_congruent :: "p_point ⇒ p_point ⇒ p_point ⇒ p_point ⇒ bool" where
[simp]: "p_congruent u v u' v' ⟷ p_dist u v = p_dist u' v'"
lemma
assumes "p_dist u v = p_dist u' v'"
assumes "p_dist v w = p_dist v' w'"
assumes "p_dist u w = p_dist u' w'"
shows "∃ f. p_isometry_pt f u = u' ∧ p_isometry_pt f v = v' ∧ p_isometry_pt f w = w'"
using assms
apply transfer
using unit_disc_fix_f_congruent_triangles
by auto
text‹We prove that unit disc equipped with Poincar\'e distance is a metric space, i.e. an
instantiation of @{term metric_space} locale.›
instantiation p_point :: metric_space
begin
definition "dist_p_point = p_dist"
definition "(uniformity_p_point :: (p_point × p_point) filter) = (INF e∈{0<..}. principal {(x, y). dist_class.dist x y < e})"
definition "open_p_point (U :: p_point set) = (∀ x ∈ U. eventually (λ(x', y). x' = x ⟶ y ∈ U) uniformity)"
instance
proof
fix x y :: p_point
show "(dist_class.dist x y = 0) = (x = y)"
unfolding dist_p_point_def
by (transfer, simp add: poincare_distance_eq_0_iff)
next
fix x y z :: p_point
show "dist_class.dist x y ≤ dist_class.dist x z + dist_class.dist y z"
unfolding dist_p_point_def
apply transfer
using poincare_distance_triangle_inequality poincare_distance_sym
by metis
qed (simp_all add: open_p_point_def uniformity_p_point_def)
end
subsection ‹H-betweennes›
lift_definition p_between :: "p_point ⇒ p_point ⇒ p_point ⇒ bool" is poincare_between
done
end