Abstract
We describe formalization of the Poincaré disc model of hyperbolic
geometry within the Isabelle/HOL proof assistant. The model is defined
within the extended complex plane (one dimensional complex projectives
space ℂP1), formalized in the AFP entry “Complex Geometry”.
Points, lines, congruence of pairs of points, betweenness of triples
of points, circles, and isometries are defined within the model. It is
shown that the model satisfies all Tarski's axioms except the
Euclid's axiom. It is shown that it satisfies its negation and
the limiting parallels axiom (which proves it to be a model of
hyperbolic geometry).
License
Topics
Session Poincare_Disc
- Hyperbolic_Functions
- Tarski
- Poincare_Lines
- Poincare_Lines_Ideal_Points
- Poincare_Distance
- Poincare_Circles
- Poincare_Between
- Poincare_Lines_Axis_Intersections
- Poincare_Perpendicular
- Poincare
- Poincare_Tarski