# Theory Incidence

theory Incidence imports Main begin
section‹Incidence›
text‹
D.Hilbert made a rigorous reconstruction of Euclidean geometry in Chapter 1 of \<^cite>‹"Hilbert"›.
There, five types of axioms are listed and 32 theorems are proved.
In Hilbert's axiom system, basic concepts such as points and lines are treated as undefined terms, and only their relationships are defined by axioms.
In addition, the continuity axiom stipulates that the Euclidean plane is essentially equivalent to the real plane R2, ensuring that the axiom system is categorical.
Implement each axiom and definition and prove the theorem (Coupling axioms related to space geometry axiom 4 to 8 are excluded).
›
datatype Point = "char"
datatype Segment = Se "Point" "Point"
datatype Line = Li "Point" "Point"
datatype Angle = An "Point" "Point" "Point"
datatype Triangle = Tr "Point" "Point" "Point"