# Theory Projective_Plane_Axioms

theory Projective_Plane_Axioms
imports Main
begin

(* Author: Anthony Bordg, University of Cambridge, apdb3@cam.ac.uk .*)

text ‹
Contents:
▪ We introduce the types of points and lines and an incidence relation between them.
▪ A set of axioms for the projective plane (the models of these axioms are
n-dimensional with n ‹≥› 2).
›

section ‹The Axioms of the Projective Plane›

(* One has a type of points *)
typedecl "Points"

(* One has a type of lines *)
typedecl "Lines"

(* One has an incidence relation between points and lines *)
consts incid :: "Points ⇒ Lines ⇒ bool"

(* Ax1: Any two (distinct) points lie on a (unique) line *)
axiomatization where
ax1: "∃l. incid P l ∧ incid Q l"

(* Ax2: Any two (distinct) lines meet in a (unique) point *)
axiomatization where
ax2: "∃P. incid P l ∧ incid P m"

(* The uniqueness part *)
axiomatization where
ax_uniqueness: "incid P l ⟶ incid Q l ⟶ incid P m ⟶ incid Q m ⟶ P = Q ∨ l = m"

definition distinct4 :: "Points ⇒ Points ⇒ Points ⇒ Points ⇒ bool" where
"distinct4 A B C D ≡ (A ≠ B) ∧ (A ≠ C) ∧ (A ≠ D) ∧ (B ≠ C) ∧ (B ≠ D) ∧ (C ≠ D)"

(* Ax3: There exists four points such that no three of them are collinear *)
axiomatization where
ax3: "∃A B C D. distinct4 A B C D ∧ (∀l.
(incid A l ∧ incid B l ⟶ ¬(incid C l) ∧ ¬(incid D l)) ∧
(incid A l ∧ incid C l ⟶ ¬(incid B l) ∧ ¬(incid D l)) ∧
(incid A l ∧ incid D l ⟶ ¬(incid B l) ∧ ¬(incid C l)) ∧
(incid B l ∧ incid C l ⟶ ¬(incid A l) ∧ ¬(incid D l)) ∧
(incid B l ∧ incid D l ⟶ ¬(incid A l) ∧ ¬(incid C l)) ∧
(incid C l ∧ incid D l ⟶ ¬(incid A l) ∧ ¬(incid B l)))"

end

# Theory Pappus_Property

theory Pappus_Property
imports Main Projective_Plane_Axioms
begin

(* Author: Anthony Bordg, University of Cambridge, apdb3@cam.ac.uk .*)

text ‹
Contents:
▪ We give two formulations of Pappus's property for a configuration of nine points
[‹is_pappus1›] [‹is_pappus2›].
▪ We prove the equivalence of these two formulations [‹pappus_equiv›].
▪ We state Pappus property for a plane [‹is_pappus›].
›

section ‹Pappus's Property›

definition col :: "[Points, Points, Points] ⇒ bool" where
"col A B C ≡ ∃l. incid A l ∧ incid B l ∧ incid C l"

definition distinct6 ::
"[Points, Points, Points, Points, Points, Points] ⇒ bool" where
"distinct6 A B C D E F ≡ (A ≠ B) ∧ (A ≠ C) ∧ (A ≠ D) ∧ (A ≠ E) ∧ (A ≠ F) ∧
(B ≠ C) ∧ (B ≠ D) ∧ (B ≠ E) ∧ (B ≠ F) ∧
(C ≠ D) ∧ (C ≠ E) ∧ (C ≠ F) ∧
(D ≠ E) ∧ (D ≠ F) ∧
(E ≠ F)"

definition lines :: "Points ⇒ Points ⇒ Lines set" where
"lines P Q ≡ {l. incid P l ∧ incid Q l}"

lemma uniq_line:
assumes "P ≠ Q" and "l ∈ lines P Q" and "m ∈ lines P Q"
shows "l = m"
using assms lines_def ax_uniqueness
by blast

definition line :: "Points ⇒ Points ⇒ Lines" where
"line P Q ≡ @l. incid P l ∧ incid Q l"

(* The point P is the intersection of the lines AB and CD. For P to be well-defined,
A and B should be distinct, C and D should be distinct, and the lines AB and CD should
be distinct *)
definition is_a_proper_intersec :: "[Points, Points, Points, Points, Points] ⇒ bool" where
"is_a_proper_intersec P A B C D ≡ (A ≠ B) ∧ (C ≠ D) ∧ (line A B ≠ line C D)
∧ col P A B ∧ col P C D"

(* We state a first form of Pappus's property *)
definition is_pappus1 ::
"[Points, Points, Points, Points, Points, Points, Points, Points, Points] => bool " where
"is_pappus1 A B C A' B' C' P Q R ≡
distinct6 A B C A' B' C' ⟶ col A B C ⟶ col A' B' C'
⟶ is_a_proper_intersec P A B' A' B ⟶ is_a_proper_intersec Q B C' B' C
⟶ is_a_proper_intersec R A C' A' C
⟶ col P Q R"

definition is_a_intersec :: "[Points, Points, Points, Points, Points] ⇒ bool" where
"is_a_intersec P A B C D ≡ col P A B ∧ col P C D"

(* We state a second form of Pappus's property *)
definition is_pappus2 ::
"[Points, Points, Points, Points, Points, Points, Points, Points, Points] ⇒ bool" where
"is_pappus2 A B C A' B' C' P Q R ≡
(distinct6 A B C A' B' C' ∨ (A ≠ B' ∧ A'≠ B ∧ line A B' ≠ line A' B ∧
B ≠ C' ∧ B' ≠ C ∧ line B C' ≠ line B' C ∧
A ≠ C' ∧ A' ≠ C ∧ line A C' ≠ line A' C))
⟶ col A B C ⟶ col A' B' C' ⟶ is_a_intersec P A B' A' B
⟶ is_a_intersec Q B C' B' C ⟶ is_a_intersec R A C' A' C
⟶ col P Q R"

lemma is_a_proper_intersec_is_a_intersec:
assumes "is_a_proper_intersec P A B C D"
shows "is_a_intersec P A B C D"
using assms is_a_intersec_def is_a_proper_intersec_def
by auto

(* The first and the second forms of Pappus's property are equivalent *)
lemma pappus21:
assumes "is_pappus2 A B C A' B' C' P Q R"
shows "is_pappus1 A B C A' B' C' P Q R"
using assms is_pappus2_def is_pappus1_def is_a_proper_intersec_is_a_intersec
by auto

lemma col_AAB: "col A A B"

lemma col_ABA: "col A B A"
using ax1 col_def
by blast

lemma col_ABB: "col A B B"

lemma incidA_lAB: "incid A (line A B)"
by (metis (no_types, lifting) ax1 line_def someI_ex)

lemma incidB_lAB: "incid B (line A B)"
by (metis (no_types, lifting) ax1 line_def someI_ex)

lemma degenerate_hexagon_is_pappus:
assumes "distinct6 A B C A' B' C'" and "col A B C" and "col A' B' C'" and
"is_a_intersec P A B' A' B" and "is_a_intersec Q B C' B' C" and "is_a_intersec R A C' A' C"
and "line A B' = line A' B ∨ line B C' = line B' C ∨ line A C' = line A' C"
shows "col P Q R"
proof -
have "col P Q R" if "line A B' = line A' B"
by (smt assms(1) assms(3) assms(4) assms(5) assms(6) ax_uniqueness col_def distinct6_def
incidA_lAB incidB_lAB is_a_intersec_def that)
have "col P Q R" if "line B C' = line B' C"
by (smt ‹line A B' = line A' B ⟹ col P Q R› assms(1) assms(2) assms(3) ax_uniqueness col_def
distinct6_def incidA_lAB incidB_lAB that)
have "col P Q R" if "line A C' = line A' C"
by (smt ‹line B C' = line B' C ⟹ col P Q R› assms(1) assms(2) assms(3) assms(7) ax_uniqueness
col_def distinct6_def incidA_lAB incidB_lAB)
show "col P Q R"
using ‹line A B' = line A' B ⟹ col P Q R› ‹line A C' = line A' C ⟹ col P Q R›
‹line B C' = line B' C ⟹ col P Q R› assms(7)
by blast
qed

lemma pappus12:
assumes "is_pappus1 A B C A' B' C' P Q R"
shows "is_pappus2 A B C A' B' C' P Q R"
proof -
have "col P Q R" if "(A ≠ B' ∧ A'≠ B ∧ line A B' ≠ line A' B ∧
B ≠ C' ∧ B' ≠ C ∧ line B C' ≠ line B' C ∧
A ≠ C' ∧ A' ≠ C ∧ line A C' ≠ line A' C)" and h1:"col A B C" and h2:"col A' B' C'"
and "is_a_intersec P A B' A' B" and "is_a_intersec Q B C' B' C"
and "is_a_intersec R A C' A' C"
proof -
have "col P Q R" if "A = B" (* in this case P = A = B and P, Q, R lie on AC' *)
proof -
have "P = A"
by (metis ‹A ≠ B' ∧ A' ≠ B ∧ line A B' ≠ line A' B ∧ B ≠ C' ∧ B' ≠ C ∧ line B C' ≠ line B' C
∧ A ≠ C' ∧ A' ≠ C ∧ line A C' ≠ line A' C› ‹is_a_intersec P A B' A' B› ax_uniqueness col_def
incidA_lAB incidB_lAB is_a_intersec_def that)
have "col P A C' ∧ col Q A C' ∧ col R A C'"
using ‹P = A› ‹is_a_intersec Q B C' B' C› ‹is_a_intersec R A C' A' C› col_AAB
is_a_intersec_def that
by auto
then show "col P Q R"
by (smt ‹A ≠ B' ∧ A' ≠ B ∧ line A B' ≠ line A' B ∧ B ≠ C' ∧ B' ≠ C ∧ line B C' ≠ line B' C
∧ A ≠ C' ∧ A' ≠ C ∧ line A C' ≠ line A' C› ax_uniqueness col_def)
qed
have "col P Q R" if "A = C" (* case where P = A = C = Q and P,Q,R belong to AB' *)
proof -
have "R = A"
by (metis ‹A ≠ B' ∧ A' ≠ B ∧ line A B' ≠ line A' B ∧ B ≠ C' ∧ B' ≠ C ∧ line B C' ≠ line B' C
∧ A ≠ C' ∧ A' ≠ C ∧ line A C' ≠ line A' C› ‹is_a_intersec R A C' A' C› ax_uniqueness col_def incidA_lAB incidB_lAB is_a_intersec_def that)
have "col P A B' ∧ col Q A B' ∧ col R A B'"
using ‹R = A› ‹is_a_intersec P A B' A' B› ‹is_a_intersec Q B C' B' C› col_def
is_a_intersec_def that
by auto
then show "col P Q R"
by (smt ‹A ≠ B' ∧ A' ≠ B ∧ line A B' ≠ line A' B ∧ B ≠ C' ∧ B' ≠ C ∧ line B C' ≠ line B' C
∧ A ≠ C' ∧ A' ≠ C ∧ line A C' ≠ line A' C› ax_uniqueness col_def)
qed
have "col P Q R" if "A = A'" (* very degenerate case, all the 9 points are collinear*)
by (smt ‹A ≠ B' ∧ A' ≠ B ∧ line A B' ≠ line A' B ∧ B ≠ C' ∧ B' ≠ C ∧ line B C' ≠ line B' C ∧
A ≠ C' ∧ A' ≠ C ∧ line A C' ≠ line A' C› ‹is_a_intersec P A B' A' B› ‹is_a_intersec R A C' A' C›
ax_uniqueness col_ABA col_def incidA_lAB incidB_lAB is_a_intersec_def that)
have "col P Q R" if "B = C" (* case where B = C = Q and P,Q,R belong to A'B *)
by (smt ‹A ≠ B' ∧ A' ≠ B ∧ line A B' ≠ line A' B ∧ B ≠ C' ∧ B' ≠ C ∧ line B C' ≠ line B' C ∧
A ≠ C' ∧ A' ≠ C ∧ line A C' ≠ line A' C› ‹is_a_intersec P A B' A' B› ‹is_a_intersec Q B C' B' C›
‹is_a_intersec R A C' A' C› ax_uniqueness col_def incidA_lAB incidB_lAB is_a_intersec_def that)
have "col P Q R" if "B = B'" (* very degenerate case, the 9 points are collinear *)
by (smt ‹A ≠ B' ∧ A' ≠ B ∧ line A B' ≠ line A' B ∧ B ≠ C' ∧ B' ≠ C ∧ line B C' ≠ line B' C ∧
A ≠ C' ∧ A' ≠ C ∧ line A C' ≠ line A' C› ‹is_a_intersec P A B' A' B› ‹is_a_intersec Q B C' B' C›
ax_uniqueness col_AAB col_def incidA_lAB incidB_lAB is_a_intersec_def that)
have "col P Q R" if "C = C'" (* again, very degenerate case, the 9 points are collinear *)
by (smt ‹A ≠ B' ∧ A' ≠ B ∧ line A B' ≠ line A' B ∧ B ≠ C' ∧ B' ≠ C ∧ line B C' ≠ line B' C ∧
A ≠ C' ∧ A' ≠ C ∧ line A C' ≠ line A' C› ‹is_a_intersec Q B C' B' C› ‹is_a_intersec R A C' A' C›
ax_uniqueness col_ABB col_def incidA_lAB incidB_lAB is_a_intersec_def that)
have "col P Q R" if "A' = B'" (* case where P = A' = B', and P,Q,R belong to A'C *)
by (smt ‹A ≠ B' ∧ A' ≠ B ∧ line A B' ≠ line A' B ∧ B ≠ C' ∧ B' ≠ C ∧ line B C' ≠ line B' C ∧
A ≠ C' ∧ A' ≠ C ∧ line A C' ≠ line A' C› ‹is_a_intersec P A B' A' B› ‹is_a_intersec Q B C' B' C›
‹is_a_intersec R A C' A' C› ax_uniqueness col_def incidA_lAB incidB_lAB is_a_intersec_def that)
have "col P Q R" if "A' = C'" (* case where R = A' = B', the points P,Q,R belong to A'B *)
by (smt ‹A ≠ B' ∧ A' ≠ B ∧ line A B' ≠ line A' B ∧ B ≠ C' ∧ B' ≠ C ∧ line B C' ≠ line B' C ∧
A ≠ C' ∧ A' ≠ C ∧ line A C' ≠ line A' C› ‹is_a_intersec P A B' A' B› ‹is_a_intersec Q B C' B' C›
‹is_a_intersec R A C' A' C› ax_uniqueness col_def incidA_lAB incidB_lAB is_a_intersec_def that)
have "col P Q R" if "B' = C'" (* case where Q = B' = C', the points P,Q,R belong to AB' *)
by (smt ‹A ≠ B' ∧ A' ≠ B ∧ line A B' ≠ line A' B ∧ B ≠ C' ∧ B' ≠ C ∧ line B C' ≠ line B' C ∧
A ≠ C' ∧ A' ≠ C ∧ line A C' ≠ line A' C› ‹is_a_intersec P A B' A' B› ‹is_a_intersec Q B C' B' C›
‹is_a_intersec R A C' A' C› ax_uniqueness col_def incidA_lAB incidB_lAB is_a_intersec_def that)
have "col P Q R" if "A ≠ B ∧ A ≠ C ∧ A ≠ A' ∧ B ≠ C ∧ B ≠ B' ∧ C ≠ C' ∧ A'≠ B'
∧ A' ≠ C' ∧ B' ≠ C'"
proof -
have a1:"distinct6 A B C A' B' C'"
using ‹A ≠ B' ∧ A' ≠ B ∧ line A B' ≠ line A' B ∧ B ≠ C' ∧ B' ≠ C ∧ line B C' ≠ line B' C ∧
A ≠ C' ∧ A' ≠ C ∧ line A C' ≠ line A' C› distinct6_def that
by auto
have "is_a_proper_intersec P A B' A' B"
using ‹A ≠ B' ∧ A' ≠ B ∧ line A B' ≠ line A' B ∧ B ≠ C' ∧ B' ≠ C ∧ line B C' ≠ line B' C ∧
A ≠ C' ∧ A' ≠ C ∧ line A C' ≠ line A' C› ‹is_a_intersec P A B' A' B› is_a_intersec_def
is_a_proper_intersec_def
by auto
have "is_a_proper_intersec Q B C' B' C"
using ‹A ≠ B' ∧ A' ≠ B ∧ line A B' ≠ line A' B ∧ B ≠ C' ∧ B' ≠ C ∧ line B C' ≠ line B' C ∧
A ≠ C' ∧ A' ≠ C ∧ line A C' ≠ line A' C› ‹is_a_intersec Q B C' B' C› is_a_intersec_def
is_a_proper_intersec_def
by auto
have "is_a_proper_intersec R A C' A' C"
using ‹A ≠ B' ∧ A' ≠ B ∧ line A B' ≠ line A' B ∧ B ≠ C' ∧ B' ≠ C ∧ line B C' ≠ line B' C ∧
A ≠ C' ∧ A' ≠ C ∧ line A C' ≠ line A' C› ‹is_a_intersec R A C' A' C› is_a_intersec_def
is_a_proper_intersec_def
by auto
show "col P Q R"
using ‹is_a_proper_intersec P A B' A' B› ‹is_a_proper_intersec Q B C' B' C›
‹is_a_proper_intersec R A C' A' C› a1 assms h1 h2 is_pappus1_def
by blast
qed
show "col P Q R"
using ‹A = A' ⟹ col P Q R› ‹A = B ⟹ col P Q R› ‹A = C ⟹ col P Q R›
‹A ≠ B ∧ A ≠ C ∧ A ≠ A' ∧ B ≠ C ∧ B ≠ B' ∧ C ≠ C' ∧ A' ≠ B' ∧ A' ≠ C' ∧ B' ≠ C' ⟹ col P Q R›
‹A' = B' ⟹ col P Q R› ‹A' = C' ⟹ col P Q R› ‹B = B' ⟹ col P Q R› ‹B = C ⟹ col P Q R›
‹B' = C' ⟹ col P Q R› ‹C = C' ⟹ col P Q R›
by blast
qed
have "col P Q R" if "distinct6 A B C A' B' C'" and "col A B C" and "col A' B' C'"
and "is_a_intersec P A B' A' B" and "is_a_intersec Q B C' B' C" and "is_a_intersec R A C' A' C"
proof -
have "col P Q R" if "line A B' = line A' B"
using ‹col A B C› ‹col A' B' C'› ‹distinct6 A B C A' B' C'› ‹is_a_intersec P A B' A' B›
‹is_a_intersec Q B C' B' C› ‹is_a_intersec R A C' A' C› degenerate_hexagon_is_pappus that
by blast
have "col P Q R" if "line B C' = line B' C"
using ‹col A B C› ‹col A' B' C'› ‹distinct6 A B C A' B' C'› ‹is_a_intersec P A B' A' B›
‹is_a_intersec Q B C' B' C› ‹is_a_intersec R A C' A' C› degenerate_hexagon_is_pappus that
by blast
have "col P Q R" if "line A' C = line A C'"
using ‹col A B C› ‹col A' B' C'› ‹distinct6 A B C A' B' C'› ‹is_a_intersec P A B' A' B›
‹is_a_intersec Q B C' B' C› ‹is_a_intersec R A C' A' C› degenerate_hexagon_is_pappus that
by auto
have "col P Q R" if "line A B' ≠ line A' B" and "line B C' ≠ line B' C" and
"line A C' ≠ line A' C"
proof -
have "is_a_proper_intersec P A B' A' B"
using ‹distinct6 A B C A' B' C'› ‹is_a_intersec P A B' A' B› distinct6_def is_a_intersec_def
is_a_proper_intersec_def that(1)
by auto
have "is_a_proper_intersec Q B C' B' C"
using ‹distinct6 A B C A' B' C'› ‹is_a_intersec Q B C' B' C› distinct6_def is_a_intersec_def
is_a_proper_intersec_def that(2)
by auto
have "is_a_proper_intersec R A C' A' C"
using ‹distinct6 A B C A' B' C'› ‹is_a_intersec R A C' A' C› distinct6_def is_a_intersec_def
is_a_proper_intersec_def that(3)
by auto
show "col P Q R"
using ‹col A B C› ‹col A' B' C'› ‹distinct6 A B C A' B' C'› ‹is_a_proper_intersec P A B' A' B›
‹is_a_proper_intersec Q B C' B' C› ‹is_a_proper_intersec R A C' A' C› assms is_pappus1_def
by blast
qed
show "col P Q R"
using ‹⟦line A B' ≠ line A' B; line B C' ≠ line B' C; line A C' ≠ line A' C⟧ ⟹ col P Q R›
‹line A B' = line A' B ⟹ col P Q R› ‹line A' C = line A C' ⟹ col P Q R›
‹line B C' = line B' C ⟹ col P Q R›
by fastforce
qed
show "is_pappus2 A B C A' B' C' P Q R"
by (simp add: ‹⟦A ≠ B' ∧ A' ≠ B ∧ line A B' ≠ line A' B ∧ B ≠ C' ∧ B' ≠ C ∧ line B C' ≠ line B' C
∧ A ≠ C' ∧ A' ≠ C ∧ line A C' ≠ line A' C; col A B C; col A' B' C'; is_a_intersec P A B' A' B; is_a_intersec Q B C' B' C; is_a_intersec R A C' A' C⟧ ⟹ col P Q R›
‹⟦distinct6 A B C A' B' C'; col A B C; col A' B' C'; is_a_intersec P A B' A' B; is_a_intersec Q B C' B' C; is_a_intersec R A C' A' C⟧ ⟹ col P Q R›
is_pappus2_def)
qed

lemma pappus_equiv: "is_pappus1 A B C A' B' C' P Q R = is_pappus2 A B C A' B' C' P Q R"
using pappus12 pappus21
by blast

(* Finally, we give Pappus's property for a plane stating that the diagonal points
of any hexagon of that plane, whose vertices lie alternately on two lines, are collinear *)

definition is_pappus :: "bool" where
"is_pappus ≡ ∀A B C D E F P Q R. is_pappus2 A B C D E F P Q R"

end


# Theory Pascal_Property

theory Pascal_Property
imports Main Projective_Plane_Axioms Pappus_Property
begin

(* Author: Anthony Bordg, University of Cambridge, apdb3@cam.ac.uk .*)

text ‹
Contents:
▪ A hexagon is pascal if its three opposite sides meet in collinear points [‹is_pascal›].
▪ A plane is pascal, or has Pascal's property, if for every hexagon of that plane
Pascal property is stable under any permutation of that hexagon.
›

section ‹Pascal's Property›

definition inters :: "Lines ⇒ Lines ⇒ Points set" where
"inters l m ≡ {P. incid P l ∧ incid P m}"

lemma inters_is_singleton:
assumes "l ≠ m" and "P ∈ inters l m" and "Q ∈ inters l m"
shows "P = Q"
using assms ax_uniqueness inters_def
by blast

definition inter :: "Lines ⇒ Lines ⇒ Points" where
"inter l m ≡ @P. P ∈ inters l m"

lemma uniq_inter:
assumes "l ≠ m" and "incid P l" and "incid P m"
shows "inter l m = P"
proof -
have "P ∈ inters l m"
by (simp add: assms(2) assms(3) inters_def)
have "∀Q. Q ∈ inters l m ⟶ Q = P"
using ‹P ∈ inters l m› assms(1) inters_is_singleton
by blast
show "inter l m = P"
using ‹P ∈ inters l m› assms(1) inter_def inters_is_singleton
by auto
qed

(* The configuration of a hexagon where the three pairs of opposite sides meet in
collinear points *)
definition is_pascal :: "[Points, Points, Points, Points, Points, Points] ⇒ bool" where
"is_pascal A B C D E F ≡ distinct6 A B C D E F ⟶ line B C ≠ line E F ⟶ line C D ≠ line A F
⟶ line A B ≠ line D E ⟶
(let P = inter (line B C) (line E F) in
let Q = inter (line C D) (line A F) in
let R = inter (line A B) (line D E) in
col P Q R)"

lemma col_rot_CW:
assumes "col P Q R"
shows "col R P Q"
using assms col_def
by auto

lemma col_2cycle:
assumes "col P Q R"
shows "col P R Q"
using assms col_def
by auto

lemma distinct6_rot_CW:
assumes "distinct6 A B C D E F"
shows "distinct6 F A B C D E"
using assms distinct6_def
by auto

lemma lines_comm: "lines P Q = lines Q P"
using lines_def
by auto

lemma line_comm:
assumes "P ≠ Q"
shows "line P Q = line Q P"
by (metis ax_uniqueness incidA_lAB incidB_lAB)

lemma inters_comm: "inters l m = inters m l"
using inters_def
by auto

lemma inter_comm: "inter l m = inter m l"

lemma inter_line_line_comm:
assumes "C ≠ D"
shows "inter (line A B) (line C D) = inter (line A B) (line D C)"
using assms line_comm
by auto

lemma inter_line_comm_line:
assumes "A ≠ B"
shows "inter (line A B) (line C D) = inter (line B A) (line C D)"
using assms line_comm
by auto

lemma inter_comm_line_line_comm:
assumes "C ≠ D" and "line A B ≠ line C D"
shows "inter (line A B) (line C D) = inter (line D C) (line A B)"
by (metis inter_comm line_comm)

(* Pascal's property is stable under the 6-cycle [A B C D E F] *)
lemma is_pascal_rot_CW:
assumes "is_pascal A B C D E F"
shows "is_pascal F A B C D E"
proof -
define P Q R where "P = inter (line A B) (line D E)" and "Q = inter (line B C) (line E F)" and
"R = inter (line F A) (line C D)"
have "col P Q R" if "distinct6 F A B C D E" and "line A B ≠ line D E" and "line B C ≠ line E F"
and "line F A ≠ line C D"
using P_def Q_def R_def assms col_rot_CW distinct6_def inter_comm is_pascal_def line_comm
that(1) that(2) that(3) that(4)
by auto
then show "is_pascal F A B C D E"
by (metis P_def Q_def R_def is_pascal_def line_comm)
qed

(* We recall that the group of permutations S_6 is generated by the 2-cycle [1 2]
and the 6-cycle [1 2 3 4 5 6] *)

(* Assuming Pappus's property, Pascal's property is stable under the 2-cycle [A B] *)

lemma incid_C_AB:
assumes "A ≠ B" and "incid A l" and "incid B l" and "incid C l"
shows "incid C (line A B)"
using assms ax_uniqueness incidA_lAB incidB_lAB
by blast

lemma incid_inters_left:
assumes "P ∈ inters l m"
shows "incid P l"
using assms inters_def
by auto

lemma incid_inters_right:
assumes "P ∈ inters l m"
shows "incid P m"
using assms incid_inters_left inters_comm
by blast

lemma inter_in_inters: "inter l m ∈ inters l m"
proof -
have "∃P. P ∈ inters l m"
using inters_def ax2
by auto
show "inter l m ∈ inters l m"
by (metis ‹∃P. P ∈ inters l m› inter_def some_eq_ex)
qed

lemma incid_inter_left: "incid (inter l m) l"
using incid_inters_left inter_in_inters
by blast

lemma incid_inter_right: "incid (inter l m) m"
using incid_inter_left inter_comm
by fastforce

lemma col_A_B_ABl: "col A B (inter (line A B) l)"
using col_def incidA_lAB incidB_lAB incid_inter_left
by blast

lemma col_A_B_lAB: "col A B (inter l (line A B))"
using col_A_B_ABl inter_comm
by auto

lemma inter_is_a_intersec: "is_a_intersec (inter (line A B) (line C D)) A B C D"
by (simp add: col_A_B_ABl col_A_B_lAB col_rot_CW is_a_intersec_def)

definition line_ext :: "Lines ⇒ Points set" where
"line_ext l ≡ {P. incid P l}"

lemma line_left_inter_1:
assumes "P ∈ line_ext l" and "P ∉ line_ext m"
shows "line (inter l m) P = l"
by (metis CollectD CollectI assms(1) assms(2) incidA_lAB incidB_lAB incid_inter_left
incid_inter_right line_ext_def uniq_inter)

lemma line_left_inter_2:
assumes "P ∈ line_ext m" and "P ∉ line_ext l"
shows "line (inter l m) P = m"
using assms inter_comm line_left_inter_1
by fastforce

lemma line_right_inter_1:
assumes "P ∈ line_ext l" and "P ∉ line_ext m"
shows "line P (inter l m) = l"
by (metis assms line_comm line_left_inter_1)

lemma line_right_inter_2:
assumes "P ∈ line_ext m" and "P ∉ line_ext l"
shows "line P (inter l m) = m"
by (metis assms inter_comm line_comm line_left_inter_1)

lemma inter_ABC_1:
assumes "line A B ≠ line C A"
shows "inter (line A B) (line C A) = A"
using assms ax_uniqueness incidA_lAB incidB_lAB incid_inter_left incid_inter_right
by blast

lemma line_inter_2:
assumes "inter l m ≠ inter l' m"
shows "line (inter l m) (inter l' m) = m"
using assms ax_uniqueness incidA_lAB incidB_lAB incid_inter_right
by blast

lemma col_line_ext_1:
assumes "col A B C" and "A ≠ C"
shows "B ∈ line_ext (line A C)"
by (metis CollectI assms ax_uniqueness col_def incidA_lAB incidB_lAB line_ext_def)

lemma inter_line_ext_1:
assumes "inter l m ∈ line_ext n" and "l ≠ m" and "l ≠ n"
shows "inter l m = inter l n"
using assms(1) assms(3) ax_uniqueness incid_inter_left incid_inter_right line_ext_def
by blast

lemma inter_line_ext_2:
assumes "inter l m ∈ line_ext n" and "l ≠ m" and "m ≠ n"
shows "inter l m = inter m n"
by (metis assms inter_comm inter_line_ext_1)

definition pascal_prop :: "bool" where
"pascal_prop ≡ ∀A B C D E F. is_pascal A B C D E F ⟶ is_pascal B A C D E F"

lemma pappus_pascal:
assumes "is_pappus"
shows "pascal_prop"
proof-
have "is_pascal B A C D E F" if "is_pascal A B C D E F" for A B C D E F
proof-
define X Y Z where "X = inter (line A C) (line E F)" and "Y = inter (line C D) (line B F)"
and "Z = inter (line B A) (line D E)"
have "col X Y Z" if "distinct6 B A C D E F" and "line A C ≠ line E F" and "line C D ≠ line B F"
and "line B A ≠ line D E" and "line B C = line E F"
by (smt X_def Y_def ax_uniqueness col_ABA col_rot_CW distinct6_def incidB_lAB incid_inter_left
incid_inter_right line_comm that(1) that(2) that(3) that(5))
have "col X Y Z" if "distinct6 B A C D E F" and "line A C ≠ line E F" and "line C D ≠ line B F"
and "line B A ≠ line D E" and "line C D = line A F"
by (metis X_def Y_def col_ABA col_rot_CW distinct6_def inter_ABC_1 line_comm that(1) that(2)
that(3) that(5))
have "col X Y Z" if "distinct6 B A C D E F" and "line A C ≠ line E F" and "line C D ≠ line B F"
and "line B A ≠ line D E" and "line B C ≠ line E F" and "line C D ≠ line A F"
proof-
define W where "W = inter (line A C) (line E F)"
have "col A C W"
define P Q R where "P = inter (line B C) (line E F)"
and "Q = inter (line A B) (line D E)"
and "R = inter (line C D) (line A F)"
have "col P Q R"
using P_def Q_def R_def ‹is_pascal A B C D E F› col_2cycle distinct6_def is_pascal_def
line_comm that(1) that(4) that(5) that(6)
by auto
(* Below we take care of a few degenerate cases *)
have "col X Y Z" if "P = Q"
by (smt P_def Q_def X_def Y_def Z_def ‹distinct6 B A C D E F› ax_uniqueness col_ABA col_def
distinct6_def incidA_lAB incidB_lAB incid_inter_left inter_comm that)
have "col X Y Z" if "P = R"
by (smt P_def R_def X_def Y_def Z_def ‹distinct6 B A C D E F› ‹line A C ≠ line E F›
‹line C D ≠ line B F› col_2cycle col_A_B_ABl col_rot_CW distinct6_def incidA_lAB
incidB_lAB incid_inter_left incid_inter_right that uniq_inter)
have "col X Y Z" if "P = A"
by (smt P_def Q_def R_def X_def Y_def Z_def ‹P = Q ⟹ col X Y Z› ‹P = R ⟹ col X Y Z›
‹col P Q R› ‹line B C ≠ line E F› ax_uniqueness col_def incidA_lAB incid_inter_left
incid_inter_right line_comm that)
have "col X Y Z" if "P = C"
by (smt P_def Q_def R_def X_def Y_def Z_def ‹P = R ⟹ col X Y Z› ‹col P Q R›
‹line A C ≠ line E F› ax_uniqueness col_def incidA_lAB incid_inter_left
incid_inter_right line_comm that)
have "col X Y Z" if "P = W"
by (smt P_def Q_def R_def W_def X_def Y_def Z_def ‹P = C ⟹ col X Y Z› ‹P = Q ⟹ col X Y Z›
‹col P Q R› ‹distinct6 B A C D E F› ax_uniqueness col_def distinct6_def incidB_lAB
incid_inter_left incid_inter_right line_comm that)
have "col X Y Z" if "Q = R"
by (smt Q_def R_def X_def Y_def Z_def ‹distinct6 B A C D E F› ax_uniqueness col_A_B_lAB
col_rot_CW distinct6_def incidB_lAB incid_inter_right inter_comm line_comm that)
have "col X Y Z" if "Q = A"
by (smt P_def Q_def R_def X_def Y_def Z_def ‹col P Q R› ‹distinct6 B A C D E F›
‹line C D ≠ line B F› ax_uniqueness col_ABA col_def distinct6_def incidA_lAB incidB_lAB
incid_inter_left incid_inter_right that)
have "col X Y Z" if "Q = C"
by (metis P_def Q_def W_def ‹P = W ⟹ col X Y Z› ‹distinct6 B A C D E F› ax_uniqueness
distinct6_def incidA_lAB incid_inter_left line_comm that)
have "col X Y Z" if "Q = W"
by (metis Q_def W_def X_def Z_def col_ABA line_comm that)
have "col X Y Z" if "R = A"
by (smt P_def Q_def R_def W_def X_def Y_def ‹P = W ⟹ col X Y Z› ‹Q = A ⟹ col X Y Z›
‹col P Q R› ‹distinct6 B A C D E F› ax_uniqueness col_ABA col_def col_rot_CW distinct6_def
incidA_lAB incidB_lAB incid_inter_right inter_comm that)
have "col X Y Z" if "R = C"
by (smt P_def Q_def R_def X_def Y_def Z_def ‹col P Q R› ‹distinct6 B A C D E F›
‹line A C ≠ line E F› ax_uniqueness col_def distinct6_def incidA_lAB incidB_lAB
incid_inter_left inter_comm that)
have "col X Y Z" if "R = W"
by (metis R_def W_def ‹R = A ⟹ col X Y Z› ‹R = C ⟹ col X Y Z› ‹line C D ≠ line A F›
ax_uniqueness incidA_lAB incidB_lAB incid_inter_left incid_inter_right that)
have "col X Y Z" if "A = W"
by (smt P_def Q_def R_def W_def X_def Y_def Z_def ‹P = R ⟹ col X Y Z› ‹Q = A ⟹ col X Y Z›
‹col P Q R› ‹distinct6 B A C D E F› ax_uniqueness col_def distinct6_def incidA_lAB
incidB_lAB incid_inter_left incid_inter_right that)
have "col X Y Z" if "C = W"
by (metis P_def W_def ‹P = C ⟹ col X Y Z› ‹line B C ≠ line E F› ax_uniqueness incidB_lAB
incid_inter_left incid_inter_right that)
have f1:"col (inter (line P C) (line A Q)) (inter (line Q W) (line C R))
(inter (line P W) (line A R))" if "distinct6 P Q R A C W"
using assms(1) is_pappus_def is_pappus2_def ‹distinct6 P Q R A C W› ‹col P Q R›
‹col A C W› inter_is_a_intersec inter_line_line_comm
by metis
have "col X Y Z" if "C ∈ line_ext (line E F)"
using P_def ‹P = C ⟹ col X Y Z› ‹line B C ≠ line E F› incidB_lAB line_ext_def that uniq_inter
by auto
have "col X Y Z" if "A ∈ line_ext (line D E)"
by (metis Q_def ‹Q = A ⟹ col X Y Z› ‹line B A ≠ line D E› ax_uniqueness incidA_lAB
incid_inter_left incid_inter_right line_comm line_ext_def mem_Collect_eq that)
have "col X Y Z" if "line B C = line A B"
by (metis P_def W_def ‹P = W ⟹ col X Y Z› ‹distinct6 B A C D E F› ax_uniqueness
distinct6_def incidA_lAB incidB_lAB that)
(* We can resume our proof with the non-degenerate case *)
have f2:"inter (line P C) (line A Q) = B" if
"C ∉ line_ext (line E F)" and "A ∉ line_ext (line D E)" and "line B C ≠ line A B"
by (smt CollectI P_def Q_def ax_uniqueness incidA_lAB incidB_lAB incid_inter_left
incid_inter_right line_ext_def that(1) that(2) that(3))
(* Again, we need to take care of a few particular cases *)
have "col X Y Z" if "line E F = line A F"
by (metis W_def ‹A = W ⟹ col X Y Z› ‹line A C ≠ line E F› inter_ABC_1 inter_comm that)
have "col X Y Z" if "A ∈ line_ext (line C D)"
using R_def ‹R = A ⟹ col X Y Z› ‹line C D ≠ line A F› ax_uniqueness incidA_lAB
incid_inter_left incid_inter_right line_ext_def that
by blast
have "col X Y Z" if "inter (line B C) (line E F) = inter (line A C) (line E F)"
by (simp add: P_def W_def ‹P = W ⟹ col X Y Z› that)
(* We resume the general case *)
have f3:"inter (line P W) (line A R) = F" if "line E F ≠ line A F" and "A ∉ line_ext (line C D)"
and "inter (line B C) (line E F) ≠ inter (line A C) (line E F)"
by (smt CollectI P_def R_def W_def ax_uniqueness incidA_lAB incidB_lAB incid_inter_left
incid_inter_right line_ext_def that(1) that(2) that(3))
(* Once again, first we need to handle a particular case, namely C ∈ AF, then
we resume the general case *)
have "col X Y Z" if "C ∈ line_ext (line A F)"
using R_def ‹R = C ⟹ col X Y Z› ‹line C D ≠ line A F› ax_uniqueness incidA_lAB
incid_inter_left incid_inter_right line_ext_def that
by blast
have f4:"inter (line Q W) (line C R) = inter (line Q W) (line C D)" if "C ∉ line_ext (line A F)"
using R_def incidA_lAB line_ext_def line_right_inter_1 that
by auto
then have "inter (line Q W) (line C D) ∈ line_ext (line B F)" if "distinct6 P Q R A C W"
and  "C ∉ line_ext (line E F)" and "A ∉ line_ext (line D E)" and "line B C ≠ line A B"
and "line E F ≠ line A F" and "A ∉ line_ext (line C D)"
and "inter (line B C) (line E F) ≠ inter (line A C) (line E F)"
by (smt R_def ‹distinct6 B A C D E F› ax_uniqueness col_line_ext_1 distinct6_def f1 f2 f3
incidA_lAB incidB_lAB incid_inter_left that(1) that(2) that(3) that(5) that(6) that(7))
then have "inter (line Q W) (line C D) = inter (line C D) (line B F)" if "distinct6 P Q R A C W"
and  "C ∉ line_ext (line E F)" and "A ∉ line_ext (line D E)" and "line B C ≠ line A B"
and "line E F ≠ line A F" and "A ∉ line_ext (line C D)"
and "inter (line B C) (line E F) ≠ inter (line A C) (line E F)"
by (smt W_def ‹distinct6 B A C D E F› ‹line C D ≠ line B F› ax_uniqueness distinct6_def f2
incidA_lAB incidB_lAB incid_inter_left incid_inter_right inter_line_ext_2 that(1) that(2)
that(3) that(5) that(6) that(7))
moreover have "inter (line C D) (line B F) ∈ line_ext (line Q W)" if "distinct6 P Q R A C W"
and  "C ∉ line_ext (line E F)" and "A ∉ line_ext (line D E)" and "line B C ≠ line A B"
and "line E F ≠ line A F" and "A ∉ line_ext (line C D)"
and "inter (line B C) (line E F) ≠ inter (line A C) (line E F)"
by (metis calculation col_2cycle col_A_B_ABl col_line_ext_1 distinct6_def that(1) that(2)
that(3) that(4) that(5) that(6) that(7))
ultimately have "col (inter (line A C) (line E F)) (inter (line C D) (line B F))
(inter (line A B) (line D E))" if "distinct6 P Q R A C W"
and  "C ∉ line_ext (line E F)" and "A ∉ line_ext (line D E)" and "line B C ≠ line A B"
and "line E F ≠ line A F" and "A ∉ line_ext (line C D)"
and "inter (line B C) (line E F) ≠ inter (line A C) (line E F)"
by (metis Q_def W_def col_A_B_ABl col_rot_CW that(1) that(2) that(3) that(4) that(5) that(6)
that(7))
show "col X Y Z"
by (metis P_def W_def X_def Y_def Z_def ‹A = W ⟹ col X Y Z› ‹A ∈ line_ext (line C D) ⟹ col X Y Z›
‹A ∈ line_ext (line D E) ⟹ col X Y Z› ‹C = W ⟹ col X Y Z› ‹C ∈ line_ext (line E F) ⟹ col X Y Z›
‹P = A ⟹ col X Y Z› ‹P = C ⟹ col X Y Z› ‹P = Q ⟹ col X Y Z› ‹P = R ⟹ col X Y Z›
‹Pascal_Property.inter (line B C) (line E F) = Pascal_Property.inter (line A C) (line E F) ⟹ col X Y Z›
‹Q = A ⟹ col X Y Z› ‹Q = C ⟹ col X Y Z› ‹Q = R ⟹ col X Y Z› ‹Q = W ⟹ col X Y Z› ‹R = A ⟹ col X Y Z›
‹R = C ⟹ col X Y Z› ‹R = W ⟹ col X Y Z› ‹⟦distinct6 P Q R A C W; C ∉ line_ext (line E F); A ∉ line_ext (line D E); line B C ≠ line A B; line E F ≠ line A F; A ∉ line_ext (line C D); Pascal_Property.inter (line B C) (line E F) ≠ Pascal_Property.inter (line A C) (line E F)⟧ ⟹ col (Pascal_Property.inter (line A C) (line E F)) (Pascal_Property.inter (line C D) (line B F)) (Pascal_Property.inter (line A B) (line D E))›
‹line B C = line A B ⟹ col X Y Z› ‹line E F = line A F ⟹ col X Y Z› distinct6_def line_comm)
qed
show "is_pascal B A C D E F"
using X_def Y_def Z_def ‹⟦distinct6 B A C D E F; line A C ≠ line E F; line C D ≠ line B F; line B A ≠ line D E; line B C = line E F⟧ ⟹ col X Y Z›
‹⟦distinct6 B A C D E F; line A C ≠ line E F; line C D ≠ line B F; line B A ≠ line D E; line B C ≠ line E F; line C D ≠ line A F⟧ ⟹ col X Y Z›
‹⟦distinct6 B A C D E F; line A C ≠ line E F; line C D ≠ line B F; line B A ≠ line D E; line C D = line A F⟧ ⟹ col X Y Z›
is_pascal_def
by force
qed
thus "pascal_prop" using pascal_prop_def
by auto
qed

lemma is_pascal_under_alternate_vertices:
assumes "pascal_prop" and "is_pascal A B C A' B' C'"
shows "is_pascal A B' C A' B C'"
using assms pascal_prop_def is_pascal_rot_CW
by presburger

lemma col_inter:
assumes "distinct6 A B C D E F" and "col A B C" and "col D E F"
shows "inter (line B C) (line E F) = inter (line A B) (line D E)"
by (smt assms ax_uniqueness col_def distinct6_def incidA_lAB incidB_lAB)

lemma pascal_pappus1:
assumes "pascal_prop"
shows "is_pappus1 A B C A' B' C' P Q R"
proof-
define a1 a2 a3 a4 a5 a6 where "a1 = distinct6 A B C A' B' C'"  and "a2 = col A B C" and
"a3 = col A' B' C'" and "a4 = is_a_proper_intersec P A B' A' B" and "a5 = is_a_proper_intersec Q B C' B' C"
and "a6 = is_a_proper_intersec R A C' A' C"
(* i.e. we have assumed a Pappus configuration *)
have "inter (line B C) (line B' C') = inter (line A B) (line A' B')" if a1 a2 a3 a4 a5 a6
using a1_def a2_def a3_def col_inter that(1) that(2) that(3)
by blast
then have "is_pascal A B C A' B' C'" if a1 a2 a3 a4 a5 a6
using a1_def col_ABA is_pascal_def that(1) that(2) that(3) that(4) that(5) that(6)
by auto
then have "is_pascal A B' C A' B C'" if a1 a2 a3 a4 a5 a6
using assms is_pascal_under_alternate_vertices that(1) that(2) that(3) that(4) that(5) that(6)
by blast
then have "col P Q R" if a1 a2 a3 a4 a5 a6
by (smt a1_def a4_def a5_def a6_def ax_uniqueness col_def distinct6_def incidB_lAB incid_inter_left
incid_inter_right is_a_proper_intersec_def is_pascal_def line_comm that(1) that(2) that(3)
that(4) that(5) that(6))
show "is_pappus1 A B C A' B' C' P Q R"
by (simp add: ‹⟦a1; a2; a3; a4; a5; a6⟧ ⟹ col P Q R› a1_def a2_def a3_def a4_def a5_def a6_def
is_pappus1_def)
qed

lemma pascal_pappus:
assumes "pascal_prop"
shows "is_pappus"
by (simp add: assms is_pappus_def pappus12 pascal_pappus1)

theorem pappus_iff_pascal: "is_pappus = pascal_prop"
using pappus_pascal pascal_pappus
by blast

end



# Theory Desargues_Property

theory Desargues_Property
imports Main Projective_Plane_Axioms Pappus_Property Pascal_Property
begin

(* Author: Anthony Bordg, University of Cambridge, apdb3@cam.ac.uk .*)

text ‹
Contents:
▪ We formalize Desargues's property, [‹desargues_prop›], that states that if two triangles are perspective
from a point, then they are perspective from a line.
Note that some planes satisfy that property and some others don't, hence Desargues's property is
not a theorem though it is a theorem in projective space geometry.
›

section ‹Desargues's Property›

definition distinct3 :: "[Points, Points, Points] ⇒ bool" where
"distinct3 A B C ≡ A ≠ B ∧ A ≠ C ∧ B ≠ C"

definition triangle :: "[Points, Points, Points] ⇒ bool" where
"triangle A B C ≡ distinct3 A B C ∧ (line A B ≠ line A C)"

definition meet_in :: "Lines ⇒ Lines => Points => bool " where
"meet_in l m P ≡ incid P l ∧ incid P m"

lemma meet_col_1:
assumes "meet_in (line A B) (line C D) P"
shows "col A B P"
using assms col_def incidA_lAB incidB_lAB meet_in_def
by blast

lemma meet_col_2:
assumes "meet_in (line A B) (line C D) P"
shows "col C D P"
using assms meet_col_1 meet_in_def
by auto

definition meet_3_in :: "[Lines, Lines, Lines, Points] ⇒ bool" where
"meet_3_in l m n P ≡ meet_in l m P ∧ meet_in l n P"

lemma meet_all_3:
assumes "meet_3_in l m n P"
shows "meet_in m n P"
using assms meet_3_in_def meet_in_def
by auto

lemma meet_comm:
assumes "meet_in l m P"
shows "meet_in m l P"
using assms meet_in_def
by auto

lemma meet_3_col_1:
assumes "meet_3_in (line A B) m n P"
shows "col A B P"
using assms meet_3_in_def meet_col_2 meet_in_def
by auto

lemma meet_3_col_2:
assumes "meet_3_in l (line A B) n P"
shows "col A B P"
using assms col_def incidA_lAB incidB_lAB meet_3_in_def meet_in_def
by blast

lemma meet_3_col_3:
assumes "meet_3_in l m (line A B) P"
shows "col A B P"
using assms meet_3_col_2 meet_3_in_def
by auto

definition distinct7 ::
"[Points, Points, Points, Points, Points, Points, Points] ⇒ bool" where
"distinct7 A B C D E F G ≡ (A ≠ B) ∧ (A ≠ C) ∧ (A ≠ D) ∧ (A ≠ E) ∧ (A ≠ F) ∧ (A ≠ G) ∧
(B ≠ C) ∧ (B ≠ D) ∧ (B ≠ E) ∧ (B ≠ F) ∧ (B ≠ G) ∧
(C ≠ D) ∧ (C ≠ E) ∧ (C ≠ F) ∧ (C ≠ G) ∧
(D ≠ E) ∧ (D ≠ F) ∧ (D ≠ G) ∧
(E ≠ F) ∧ (E ≠ G) ∧
(F ≠ G)"

definition distinct3l :: "[Lines, Lines, Lines] ⇒ bool" where
"distinct3l l m n ≡ l ≠ m ∧ l ≠ n ∧ m ≠ n"

(* From now on we give less general statements on purpose to avoid a lot of uninteresting
degenerate cases, since we can hardly think of any interesting application where one would need
to instantiate a statement on such degenerate case, hence our statements and proofs will be more
textbook-like. For the working mathematician the only thing that probably matters is the main
theorem without considering all the degenerate cases for which the statement might still hold. *)

definition desargues_config ::
"[Points, Points, Points, Points, Points, Points, Points, Points, Points, Points] => bool" where
"desargues_config A B C A' B' C' M N P R ≡ distinct7 A B C A' B' C' R ∧ ¬ col A B C
∧ ¬ col A' B' C' ∧ distinct3l (line A A') (line B B') (line C C') ∧
meet_3_in (line A A') (line B B') (line C C') R ∧ (line A B) ≠ (line A' B') ∧
(line B C) ≠ (line B' C') ∧ (line A C) ≠ (line A' C') ∧ meet_in (line B C) (line B' C') M ∧
meet_in (line A C) (line A' C') N ∧ meet_in (line A B) (line A' B') P"

lemma distinct7_rot_CW:
assumes "distinct7 A B C D E F G"
shows "distinct7 C A B F D E G"
using assms distinct7_def
by auto

(* Desargues configurations are stable under any rotation (i,j,k) of {1,2,3} *)
lemma desargues_config_rot_CW:
assumes "desargues_config A B C A' B' C' M N P R"
shows "desargues_config C A B C' A' B' P M N R"
by (smt assms col_rot_CW desargues_config_def distinct3l_def distinct7_rot_CW line_comm
meet_3_in_def meet_all_3 meet_comm)

lemma desargues_config_rot_CCW:
assumes "desargues_config A B C A' B' C' M N P R"
shows "desargues_config B C A B' C' A' N P M R"

(* With the two following definitions we repackage the definition of a Desargues configuration in a
"high-level", i.e. textbook-like, way. *)

definition are_perspective_from_point ::
"[Points, Points, Points, Points, Points, Points, Points] ⇒ bool" where
"are_perspective_from_point A B C A' B' C' R ≡ distinct7 A B C A' B' C' R ∧ triangle A B C ∧
triangle A' B' C' ∧ distinct3l (line A A') (line B B') (line C C') ∧
meet_3_in (line A A') (line B B') (line C C') R"

definition are_perspective_from_line ::
"[Points, Points, Points, Points, Points, Points] ⇒ bool" where
"are_perspective_from_line A B C A' B' C' ≡ distinct6 A B C A' B' C' ⟶ triangle A B C ⟶
triangle A' B' C' ⟶ line A B ≠ line A' B' ⟶ line A C ≠ line A' C' ⟶ line B C ≠ line B' C' ⟶
col (inter (line A B) (line A' B')) (inter (line A C) (line A' C')) (inter (line B C) (line B' C'))"

lemma meet_in_inter:
assumes "l ≠ m"
shows "meet_in l m (inter l m)"
by (simp add: incid_inter_left incid_inter_right meet_in_def)

lemma perspective_from_point_desargues_config:
assumes "are_perspective_from_point A B C A' B' C' R" and "line A B ≠ line A' B'" and
"line A C ≠ line A' C'" and "line B C ≠ line B' C'"
shows "desargues_config A B C A' B' C' (inter (line B C) (line B' C')) (inter (line A C) (line A' C'))
(inter (line A B) (line A' B')) R"
by (smt are_perspective_from_point_def assms(1) assms(2) assms(3) assms(4) col_line_ext_1
desargues_config_def distinct3_def incidB_lAB inter_line_ext_2 line_comm meet_in_inter
triangle_def uniq_inter)

(* Now, we state Desargues's property in a textbook-like form *)
definition desargues_prop :: "bool" where
"desargues_prop ≡
∀A B C A' B' C' P.
are_perspective_from_point A B C A' B' C' P ⟶ are_perspective_from_line A B C A' B' C'"

end



# Theory Pappus_Desargues

theory Pappus_Desargues
imports Main Projective_Plane_Axioms Pappus_Property Pascal_Property Desargues_Property
begin

(* Author: Anthony Bordg, University of Cambridge, apdb3@cam.ac.uk .*)

text ‹
Contents:
▪ We prove Hessenberg's theorem ([‹hessenberg_theorem›]): Pappus's property implies Desargues's
property in a projective plane.
›

section ‹Hessenberg's Theorem›

lemma col_ABC_ABD_1:
assumes "A ≠ B" and "col A B C" and "col A B D"
shows "col B C D"
by (metis assms ax_uniqueness col_def)

lemma col_ABC_ABD_2:
assumes "A ≠ B" and "col A B C" and "col A B D"
shows "col A C D"
by (metis assms ax_uniqueness col_def)

lemma col_line_eq_1:
assumes "A ≠ B" and "B ≠ C"and "col A B C"
shows "line A B = line B C"
by (metis assms ax_uniqueness col_def incidA_lAB incidB_lAB)

lemma col_line_eq_2:
assumes "A ≠ B" and "A ≠ C" and "col A B C"
shows "line A B = line A C"
by (metis assms col_line_eq_1 col_rot_CW line_comm)

lemma desargues_config_not_col_1:
assumes "desargues_config A B C A' B' C' M N P R"
shows "¬ col A A' B'"
proof
assume a1:"col A A' B'"
have f1:"A ≠ A'"
using assms desargues_config_def distinct7_def
by blast
have f2:"col A A' R"
using assms desargues_config_def meet_3_col_1
by blast
from f1 and f2 and a1 have f3:"col A' B' R"
using col_ABC_ABD_1
by blast
from a1 have f4:"line A A' = line A' B'"
by (metis assms ax_uniqueness col_def desargues_config_def f1 incidA_lAB incidB_lAB)
have f5:"A' ≠ B'"
using assms desargues_config_def distinct7_def
by blast
have f6:"B' ≠ R"
using assms desargues_config_def distinct7_def
by blast
from f3 and f5 and f6 have f7:"line A' B' = line B' R"
using col_line_eq_1
by blast
have "line B' R = line B B'"
by (metis a1 assms col_2cycle col_AAB col_line_eq_1 desargues_config_def f6 meet_3_col_2)
have "line A A' = line B B'"
by (simp add: ‹line B' R = line B B'› f4 f7)
then have "False"
using assms desargues_config_def distinct3l_def
by auto
then show f8:"col A A' B' ⟹ False"
by simp
qed

lemma desargues_config_not_col_2:
assumes "desargues_config A B C A' B' C' M N P R"
shows "¬ col B B' C'"
using assms desargues_config_not_col_1 desargues_config_rot_CCW
by blast

lemma desargues_config_not_col_3:
assumes "desargues_config A B C A' B' C' M N P R"
shows "¬ col C C' B'"
by (smt assms col_line_eq_1 col_rot_CW desargues_config_def desargues_config_not_col_2
desargues_config_rot_CW distinct3l_def meet_3_in_def meet_col_1 meet_col_2)

lemma desargues_config_not_col_4:
assumes "desargues_config A B C A' B' C' M N P R"
shows "¬ col A A' C'"
using assms desargues_config_not_col_3 desargues_config_rot_CCW
by blast

lemma desargues_config_not_col_5:
assumes "desargues_config A B C A' B' C' M N P R"
shows "¬ col B B' A'"
using assms desargues_config_not_col_3 desargues_config_rot_CW
by blast

lemma desargues_config_not_col_6:
assumes "desargues_config A B C A' B' C' M N P R"
shows "¬ col C C' A'"
using assms desargues_config_not_col_1 desargues_config_rot_CW
by blast

lemma desargues_config_not_col_7:
assumes "desargues_config A B C A' B' C' M N P R"
shows "¬ col A B B'"
proof
assume a1:"col A B B'"
have f1:"col A B R"
by (metis a1 assms col_ABB col_ABC_ABD_2 col_rot_CW desargues_config_def desargues_config_not_col_5
meet_3_col_2)
have f2:"col A A' R"
using assms desargues_config_def meet_3_col_1
by blast
have f3:"A ≠ A'"
using assms col_AAB desargues_config_not_col_4
by blast
have f4:"A ≠ R" using assms desargues_config_def distinct7_def
by auto
from f2 and f3 and f4 have f5:"line A A' = line A R"
using col_line_eq_2
by blast
from f1 have f6:"line A R = line B R"
by (metis a1 assms col_2cycle col_ABC_ABD_2 desargues_config_not_col_1 f2 f4)
have f7:"line B R = line B B'"
by (metis ‹line A R = line B R› a1 assms col_AAB col_line_eq_1 desargues_config_def
desargues_config_not_col_2 f1)
from f5 and f6 and f7 have "line A A' = line B B'"
by simp
then have "False"
using assms desargues_config_def distinct3l_def
by auto
thus "col A B B' ⟹ False"
by simp
qed

lemma desargues_config_not_col_8:
assumes "desargues_config A B C A' B' C' M N P R"
shows "¬ col A C C'"
by (metis assms col_ABA col_line_eq_1 col_rot_CW desargues_config_def desargues_config_not_col_3
desargues_config_not_col_7 distinct3l_def meet_3_col_1 meet_3_col_2 meet_3_col_3)

lemma desargues_config_not_col_9:
assumes "desargues_config A B C A' B' C' M N P R"
shows "¬ col B A A'"
using assms desargues_config_not_col_8 desargues_config_rot_CCW
by blast

lemma desargues_config_not_col_10:
assumes "desargues_config A B C A' B' C' M N P R"
shows "¬ col B C C'"
using assms desargues_config_not_col_7 desargues_config_rot_CCW
by blast

lemma desargues_config_not_col_11:
assumes "desargues_config A B C A' B' C' M N P R"
shows "¬ col C A A'"
using assms desargues_config_not_col_7 desargues_config_rot_CW
by blast

lemma desargues_config_not_col_12:
assumes "desargues_config A B C A' B' C' M N P R"
shows "¬ col C B B'"
using assms desargues_config_not_col_8 desargues_config_rot_CW
by blast

lemma col_inter:
assumes "A ≠ C" and "B ≠ C" and "col A B C"
shows "inter l (line B C) = inter l (line A C)"
by (metis assms col_line_eq_1 col_line_eq_2)

lemma lemma_1:
assumes "desargues_config A B C A' B' C' M N P R" and "is_pappus"
shows "col M N P ∨ incid A (line B' C') ∨ incid C' (line A B)"
proof-
have "?thesis" if "incid A (line B' C') ∨ incid C' (line A B)"
(* The proof consists in three successive applications of Pappus property *)
define Q E X F where "Q = inter (line A B) (line B' C')" and "E = inter (line A C) (line R Q)"
and "X = inter (line A C') (line R B)" and "F = inter (line A' C') (line R Q)"
have "col X E M" if "¬ incid A (line B' C')" and "¬ incid C' (line A B)"
proof-
have f1:"distinct6 C C' R Q B A"
by (smt Q_def ‹¬ incid A (line B' C')› ‹¬ incid C' (line A B)› assms(1) col_ABB col_A_B_ABl
col_A_B_lAB col_line_eq_2 col_rot_CW desargues_config_def desargues_config_not_col_12
desargues_config_not_col_2 desargues_config_not_col_3 desargues_config_not_col_7
desargues_config_not_col_9 distinct6_def incidA_lAB line_comm meet_3_col_1 meet_3_col_2)
have f2: "col C C' R"
using assms(1) desargues_config_def meet_3_col_3
by blast
have f3: "col Q B A"
using Q_def col_2cycle col_A_B_ABl col_rot_CW
by blast
have f4: "is_a_intersec E C A Q R"
using E_def col_2cycle inter_is_a_intersec is_a_intersec_def
by auto
have f5:"is_a_intersec M C B Q C'"
by (metis Q_def assms(1) col_2cycle col_ABB col_ABC_ABD_1 col_A_B_lAB col_rot_CW
desargues_config_def is_a_intersec_def meet_col_1 meet_col_2)
have f6:"is_a_intersec X C' A B R"
using X_def col_2cycle inter_is_a_intersec is_a_intersec_def
by auto
from f1 and f2 and f3 and f4 and f5 and f6 have "col M X E"
using assms(2) is_pappus2_def is_pappus_def
by blast
then show "col X E M"
using col_def
by auto
qed
have "col P X F" if "¬ incid A (line B' C')" and "¬ incid C' (line A B)"
proof-
have f1:"distinct6 A' A R Q B' C'"
by (smt Q_def ‹¬ incid A (line B' C')› ‹¬ incid C' (line A B)› assms(1) col_AAB col_A_B_ABl
col_A_B_lAB col_line_eq_1 col_rot_CW desargues_config_def desargues_config_not_col_2
desargues_config_not_col_3 desargues_config_not_col_4 desargues_config_not_col_6
desargues_config_not_col_7 distinct6_def incidB_lAB meet_3_col_2 meet_3_col_3)
have f2:"col A' A R"
by (metis assms(1) col_ABA col_line_eq_1 desargues_config_def meet_3_col_1)
have f3:"col Q B' C'"
by (simp add: Q_def col_A_B_lAB col_rot_CW)
have "is_a_intersec (inter (line A B) (line A' B')) A' B' Q A"
by (metis Q_def col_def incidA_lAB incid_inter_left inter_is_a_intersec is_a_intersec_def)
then have f4:"is_a_intersec P A' B' Q A"
using assms(1) desargues_config_def meet_in_def uniq_inter
by auto
have f5:"is_a_intersec X A C' B' R"
by (metis X_def assms(1) col_def col_line_eq_2 desargues_config_def desargues_config_not_col_9
f2 inter_is_a_intersec is_a_intersec_def line_comm meet_3_col_2)
have f6:"is_a_intersec F A' C' Q R"
by (metis F_def inter_is_a_intersec inter_line_line_comm)
from f1 and f2 and f3 and f4 and f5 and f6 and assms(2)
show "col P X F"
using is_pappus2_def is_pappus_def
by blast
qed
have "col M N P" if "¬ incid A (line B' C')" and "¬ incid C' (line A B)"
proof-
have f1:"Q ≠ C' ∧ X ≠ E ∧ line Q C' ≠ line X E"
by (smt E_def Q_def X_def ‹¬ incid A (line B' C')› ‹¬ incid C' (line A B)› assms(1) col_ABB
col_A_B_ABl col_A_B_lAB col_line_eq_2 col_rot_CW desargues_config_def
desargues_config_not_col_10 desargues_config_not_col_2 desargues_config_not_col_8
incidB_lAB incid_C_AB line_comm meet_3_col_1 meet_3_col_2 meet_3_col_3)
have f2:"E ≠ A ∧ C' ≠ F ∧ line E A ≠ line C' F"
by (smt E_def F_def Q_def X_def ‹⟦¬ incid A (line B' C'); ¬ incid C' (line A B)⟧ ⟹ col X E M›
assms(1) ax_uniqueness col_def desargues_config_def desargues_config_not_col_10
desargues_config_not_col_3 f1 incidA_lAB incidB_lAB incid_inter_left incid_inter_right
meet_in_def that(1))
have f3:"Q ≠ A ∧ X ≠ F ∧ line Q A ≠ line X F"
by (smt F_def Q_def X_def ‹¬ incid A (line B' C')› ‹¬ incid C' (line A B)› assms(1)
ax_uniqueness col_def desargues_config_def desargues_config_not_col_10
desargues_config_not_col_2 desargues_config_not_col_7 incidA_lAB incidB_lAB incid_inter_left
incid_inter_right meet_3_col_2 meet_3_col_3)
have f4:"col Q E F"
using E_def F_def col_def incidB_lAB incid_inter_right
by blast
have f5:"col X C' A"
using X_def col_2cycle col_A_B_ABl col_rot_CW
by blast
have f6:"is_a_intersec M Q C' X E"
by (metis Q_def ‹⟦¬ incid A (line B' C'); ¬ incid C' (line A B)⟧ ⟹ col X E M› assms(1)
col_ABB col_A_B_lAB col_def col_line_eq_1 desargues_config_def incidB_lAB is_a_intersec_def
meet_in_def that(1) that(2))
have f7:"is_a_intersec N E A C' F"
by (metis E_def F_def assms(1) ax_uniqueness col_rot_CW desargues_config_def f2 incidA_lAB
incidB_lAB incid_inter_left is_a_intersec_def meet_col_1 meet_col_2)
have f8:"is_a_intersec P Q A X F"
by (metis Q_def ‹⟦¬ incid A (line B' C'); ¬ incid C' (line A B)⟧ ⟹ col P X F› assms(1)
ax_uniqueness col_rot_CW desargues_config_def f3 incidA_lAB incidB_lAB incid_inter_left
is_a_intersec_def meet_col_2 meet_comm that(1) that(2))
from f1 and f2 and f3 and f4 and f5 and f6 and f7 and f8 and assms(2) show "col M N P"
using is_pappus2_def is_pappus_def
by blast
qed
show "col M N P ∨ incid A (line B' C') ∨ incid C' (line A B)"
using ‹⟦¬ incid A (line B' C'); ¬ incid C' (line A B)⟧ ⟹ col M N P›
by auto
qed

corollary corollary_1:
assumes "desargues_config A B C A' B' C' M N P R" and "is_pappus"
shows "col M N P ∨ ((incid A (line B' C') ∨ incid C' (line A B)) ∧
(incid C (line A' B') ∨ incid B' (line A C)) ∧ (incid B (line A' C') ∨ incid A' (line B C)))"
by (metis assms(1) assms(2) col_rot_CW desargues_config_rot_CCW lemma_1 line_comm)

definition triangle_circumscribes_triangle ::
"[Points, Points, Points, Points, Points, Points] ⇒ bool" where
"triangle_circumscribes_triangle A' B' C' A B C ≡ incid A (line B' C') ∧ incid C (line A' B') ∧
incid B (line A' C')"

lemma lemma_2:
assumes "desargues_config A B C A' B' C' M N P R" and "incid A (line B' C') ∨ incid C' (line A B)"
and "incid C (line A' B') ∨ incid B' (line A C)" and "incid B (line A' C') ∨ incid A' (line B C)"
shows "col M N P ∨ triangle_circumscribes_triangle A B C A' B' C' ∨ triangle_circumscribes_triangle A' B' C' A B C"
by (smt assms ax_uniqueness col_def desargues_config_not_col_1
desargues_config_not_col_11 desargues_config_not_col_12 desargues_config_not_col_2
desargues_config_not_col_3 desargues_config_not_col_9 incidA_lAB incidB_lAB
triangle_circumscribes_triangle_def)

lemma lemma_3:
assumes "is_pappus" and "desargues_config A B C A' B' C' M N P R" and
"triangle_circumscribes_triangle A' B' C' A B C"
shows "col M N P"
proof-
define S T where "S = inter (line C' P) (line R A)" and "T = inter (line C' P) (line R B)"
(* The collinearity of M N P follows from three applications of Pappus property *)
have "col N S B'"
proof-
have f1:"distinct6 R C C' P B A"
by (smt assms(2) col_AAB col_line_eq_2 col_rot_CW desargues_config_def
desargues_config_not_col_1 desargues_config_not_col_12 desargues_config_not_col_2
desargues_config_not_col_5 desargues_config_not_col_7 desargues_config_not_col_8
desargues_config_not_col_9 distinct6_def line_comm meet_3_col_1 meet_3_col_2 meet_col_1
meet_col_2)
have f2:"col R C C'"
using assms(2) col_rot_CW desargues_config_def meet_3_col_3
by blast
have f3:"col P B A"
by (metis assms(2) col_rot_CW desargues_config_def line_comm meet_col_1)
have f4:"is_a_intersec B' R B P C"
by (metis assms(2) assms(3) col_def desargues_config_def incidB_lAB is_a_intersec_def
meet_3_col_2 meet_in_def triangle_circumscribes_triangle_def)
have f5:"is_a_intersec S R A P C'"
using S_def col_2cycle inter_is_a_intersec is_a_intersec_def
by auto
have "line B C' = line A' C'"
by (metis ‹distinct6 R C C' P B A› assms(3) ax_uniqueness distinct6_def incidA_lAB incidB_lAB
triangle_circumscribes_triangle_def)
then have f6:"is_a_intersec N C A B C'"
by (metis assms(2) desargues_config_def inter_is_a_intersec line_comm meet_in_def uniq_inter)
from f1 and f2 and f3 and f4 and f5 and f6 and assms(1) have "col B' N S"
using is_pappus2_def is_pappus_def
by blast
then show "col N S B'"
qed
have "col M T A'"
proof-
have f1:"distinct6 R C C' P A B"
by (smt assms(2) col_ABA col_line_eq_2 col_rot_CW desargues_config_def desargues_config_not_col_1
desargues_config_not_col_12 desargues_config_not_col_2 desargues_config_not_col_5
desargues_config_not_col_7 desargues_config_not_col_8 desargues_config_not_col_9 distinct6_def
line_comm meet_3_col_1 meet_3_col_2 meet_col_1 meet_col_2)
have f2:"col R C C'"
using assms(2) col_rot_CW desargues_config_def meet_3_col_3
by blast
have f3:"col P A B"
using assms(2) col_rot_CW desargues_config_def meet_col_1
by blast
have f4:"line P C = line A' B'"
by (metis ‹distinct6 R C C' P A B› assms(2) assms(3) ax_uniqueness desargues_config_def
distinct6_def incidA_lAB incidB_lAB meet_in_def triangle_circumscribes_triangle_def)
have f5:"line R A = line A A'"
by (metis ‹distinct6 R C C' P A B› assms(2) col_AAB col_line_eq_2 desargues_config_def
desargues_config_not_col_1 distinct6_def line_comm meet_3_col_1)
from f4 and f5 have f6:"is_a_intersec A' R A P C"
by (metis col_def incidA_lAB incidB_lAB is_a_intersec_def)
have "line A C' = line B' C'"
by (metis assms(3) ax_uniqueness distinct6_def f1 incidA_lAB incidB_lAB
triangle_circumscribes_triangle_def)
then have f7:"is_a_intersec M C B A C'"
by (metis assms(2) col_rot_CW desargues_config_def is_a_intersec_def line_comm meet_col_1
meet_col_2)
have f8:"is_a_intersec T R B P C'"
by (metis T_def distinct6_def f1 inter_comm_line_line_comm inter_is_a_intersec line_comm)
from f1 and f2 and f3 and f6 and f7 and f8 and assms(1) have "col A' M T"
using is_pappus2_def is_pappus_def
by blast
thus "col M T A'"
qed
then show "col M N P"
proof-
have f1:"S ≠ T ∧ B ≠ A ∧ line S T ≠ line B A"
by (smt T_def ‹col N S B'› assms(2) assms(3) ax_uniqueness col_AAB col_line_eq_2 col_rot_CW
desargues_config_def desargues_config_not_col_10 desargues_config_not_col_7
desargues_config_not_col_9 incidB_lAB incid_inter_left incid_inter_right
line_comm meet_3_col_2 meet_3_col_3 meet_col_1 meet_col_2 triangle_circumscribes_triangle_def)
have f2:"A ≠ B' ∧ T ≠ A' ∧ line A B' ≠ line T A'"
by (smt T_def assms(2) col_def desargues_config_def desargues_config_not_col_1
desargues_config_not_col_9 incidB_lAB incid_C_AB incid_inter_left line_comm meet_in_def)
have f3:"S ≠ B' ∧ B ≠ A'"
by (smt S_def assms(2) assms(3) ax_uniqueness col_A_B_ABl col_line_eq_2 col_rot_CW
desargues_config_def desargues_config_not_col_2 desargues_config_not_col_5
desargues_config_not_col_7 incidA_lAB incidB_lAB incid_inter_right inter_comm line_comm
meet_3_col_2 meet_in_def triangle_circumscribes_triangle_def)
then have f4:"line S B' ≠ line B A'"
by (metis assms(2) col_def desargues_config_not_col_5 incidA_lAB incidB_lAB)
have f5:"col S A A'"
by (metis S_def assms(2) col_ABC_ABD_1 col_A_B_lAB col_rot_CW desargues_config_def
desargues_config_not_col_8 meet_3_col_1 meet_3_col_3)
have f6:"col B T B'"
by (metis T_def assms(2) col_def col_line_eq_2 desargues_config_def desargues_config_not_col_10
incidB_lAB incid_inter_right line_comm meet_3_col_2 meet_3_col_3)
have f7:"is_a_intersec P S T B A"
by (metis S_def T_def assms(2) col_ABC_ABD_1 col_A_B_ABl col_def desargues_config_def incidA_lAB
incidB_lAB is_a_intersec_def meet_in_def)
have f8:"is_a_intersec M A B' T A'"
by (metis ‹col M T A'› assms(2) assms(3) col_rot_CW desargues_config_def f2 incidA_lAB incidB_lAB
is_a_intersec_def meet_col_2 triangle_circumscribes_triangle_def uniq_inter)
have f9:"is_a_intersec N S B' B A'"
using ‹col N S B'› assms(2) assms(3) col_def desargues_config_def incidA_lAB is_a_intersec_def
meet_in_def triangle_circumscribes_triangle_def
by auto
from f1 and f2 and f3 and f4 and f5 and f6 and f7 and f8 and f9 and assms(1) have "col P M N"
using is_pappus2_def is_pappus_def
by blast
thus "col M N P"
qed
qed

theorem pappus_desargues:
assumes "is_pappus" and "desargues_config A B C A' B' C' M N P R"
shows "col M N P"
proof-
have f1:"col M N P ∨ ((incid A (line B' C') ∨ incid C' (line A B)) ∧
(incid C (line A' B') ∨ incid B' (line A C)) ∧ (incid B (line A' C') ∨ incid A' (line B C)))"
using assms corollary_1
by auto
have f2:"col M N P ∨ triangle_circumscribes_triangle A B C A' B' C' ∨ triangle_circumscribes_triangle A' B' C' A B C"
if "(incid A (line B' C') ∨ incid C' (line A B)) ∧ (incid C (line A' B') ∨ incid B' (line A C))
∧ (incid B (line A' C') ∨ incid A' (line B C))"
using assms(2) lemma_2 that
by auto
have f3:"col M N P" if "triangle_circumscribes_triangle A' B' C' A B C"
using assms lemma_3 that
by auto
have f4:"col M N P" if "triangle_circumscribes_triangle A B C A' B' C'"
proof-
have "desargues_config A' B' C' A B C M N P R"
proof-
have f1:"distinct7 A' B' C' A B C R"
using assms(2) desargues_config_def distinct7_def
by auto
have f2:"¬ col A' B' C'"
using assms(2) desargues_config_def
by blast
have f3:"¬ col A B C"
using assms(2) desargues_config_def
by blast
have f4:"distinct3l (line A' A) (line B' B) (line C' C)"
by (metis assms(2) desargues_config_def line_comm)
have f5:"meet_3_in (line A' A) (line B' B) (line C' C) R"
by (metis assms(2) desargues_config_def line_comm)
have f6:"(line A' B') ≠ (line A B) ∧ (line B' C') ≠ (line B C) ∧ (line A' C') ≠ (line A C)"
using assms(2) desargues_config_def
by auto
have f7:"meet_in (line B' C') (line B C) M ∧ meet_in (line A' C') (line A C) N ∧
meet_in (line A' B') (line A B) P"
using assms(2) desargues_config_def meet_comm
by blast
from f1 and f2 and f3 and f4 and f5 and f6 and f7 show "desargues_config A' B' C' A B C M N P R"
qed
then show "col M N P"
using assms(1) lemma_3 that
by blast
qed
from f1 and f2 and f3 and f4 show "col M N P"
by blast
qed

theorem hessenberg_thereom:
assumes "is_pappus"
shows "desargues_prop"
by (smt are_perspective_from_line_def assms col_def desargues_prop_def pappus_desargues
perspective_from_point_desargues_config)

corollary pascal_desargues:
assumes "pascal_prop"
shows "desargues_prop"
by (simp add: assms hessenberg_thereom pascal_pappus)

end



# Theory Higher_Projective_Space_Rank_Axioms

theory Higher_Projective_Space_Rank_Axioms
imports Main
begin

(* Author: Anthony Bordg, University of Cambridge, apdb3@cam.ac.uk .*)

text ‹
Contents:
▪ Following @{cite Magaud_2012} we introduce a set of axioms for projective space geometry based on
the notions of matroid and rank.
›

section ‹A Based-rank Set of Axioms for Projective Space Geometry›

(* We have a type of points *)
typedecl "Points"

(* We have a rank function "rk" on the sets of points *)
consts rk :: "Points set ⇒ nat"

(* The function rk satisfies the following axioms *)
axiomatization where
matroid_ax_1a: "rk X ≥ 0" (* Useless if rk is defined with values in ℕ, not ℤ *) and
matroid_ax_1b: "rk X ≤ card X" and
matroid_ax_2: "X ⊆ Y ⟶ rk X ≤ rk Y" and
matroid_ax_3: "rk (X ∪ Y) + rk (X ∩ Y) ≤ rk X + rk Y"

(* To capture higher projective geometry, we need to introduce the following additional axioms *)
axiomatization where
rk_ax_singleton: "rk {P} ≥ 1" and
rk_ax_couple: "P ≠ Q ⟶ rk {P,Q} ≥ 2" and
rk_ax_pasch: "rk {A,B,C,D} ≤ 3 ⟶ (∃J. rk {A,B,J} = 2 ∧ rk {C,D,J} = 2)" and
rk_ax_3_pts: "∃C. rk {A,B,C} = 2 ∧ rk {B,C} = 2 ∧ rk {A,C} = 2" and
rk_ax_dim: "∃A B C D. rk {A,B,C,D} ≥ 4"

(* Note that the rank-based axioms system above deals only with points.
Projective geometry developped this way is dimension-independent and it can be scaled to any dimension
without adding any entity to the theory or modifying the language of the theory *)

end



# Theory Matroid_Rank_Properties

theory Matroid_Rank_Properties
imports Main Higher_Projective_Space_Rank_Axioms
begin

(* Author: Anthony Bordg, University of Cambridge, apdb3@cam.ac.uk .*)

text ‹
Contents:
▪ In this file we introduce the basic lemmas and properties derived from our based-rank axioms
that will allow us to simplify our future proofs.
›

section ‹Proof Techniques Using Ranks›

lemma matroid_ax_3_alt:
assumes "I ⊆ X ∩ Y"
shows "rk (X ∪ Y) + rk I ≤ rk X + rk Y"

lemma rk_uniqueness:
assumes "rk {A,B} = 2" and "rk {C,D} = 2" and "rk {A,B,M} ≤ 2" and "rk {C,D,M} ≤ 2" and
"rk {A,B,P} ≤ 2" and "rk {C,D,P} ≤ 2" and "rk {A,B,C,D} ≥ 3"
shows "rk {M,P} = 1"
proof-
have "{A,B,M} ∪ {A,B,P} = {A,B,M,P}"
by auto
have "rk {A,B,M,P} + rk {A,B} ≤ rk {A,B,M} + rk {A,B,P}"
by (metis (full_types) ‹{A, B, M} ∪ {A, B, P} = {A, B, M, P}› insert_commute le_inf_iff
matroid_ax_3_alt subset_insertI)
then have "rk {A,B,M,P} = 2"
by (smt Un_upper1 Un_upper2 ‹{A, B, M} ∪ {A, B, P} = {A, B, M, P}› add_diff_cancel_left'
have "{C,D,M} ∪ {C,D,P} = {C,D,M,P}"
by auto
have "rk {C,D,M,P} + rk {C,D} ≤ rk {C,D,M} + rk {C,D,P}"
by (metis Un_insert_left Un_upper1 ‹{C, D, M} ∪ {C, D, P} = {C, D, M, P}› insert_is_Un le_inf_iff
matroid_ax_3_alt)
then have i1:"rk {C,D,M,P} + 2 ≤ 4"
using assms(2) assms(4) assms(6)
by linarith
moreover have i2:"rk {C,D,M,P} ≥ 2"
by (metis assms(2) insertI1 insert_subset matroid_ax_2 subset_insertI)
from i1 and i2 have "rk {C,D,M,P} = 2"
by linarith
have "rk {A,B,C,D,M,P} ≥ 3"
by (metis Un_insert_right Un_upper2 assms(7) matroid_ax_2 order_trans sup_bot.right_neutral)
have "{A,B,M,P} ∪ {C,D,M,P} = {A,B,C,D,M,P}"
by auto
then have "rk {A,B,C,D,M,P} + rk {M,P} ≤ rk {A,B,M,P} + rk {C,D,M,P}"
by (smt le_inf_iff matroid_ax_3_alt order_trans subset_insertI)
then have i3:"rk {A,B,C,D,M,P} + rk {M,P} ≤ 4"
using ‹rk {A, B, M, P} = 2› ‹rk {C, D, M, P} = 2›
by linarith
have i4:"rk {A,B,C,D,M,P} + rk {M,P} ≥ 3 + rk{M,P}"
by (simp add: ‹3 ≤ rk {A, B, C, D, M, P}›)
from i3 and i4 show "rk {M,P} = 1"
by (metis (no_types, lifting) ‹rk {A, B, C, D, M, P} + rk {M, P} ≤ rk {A, B, M, P} + rk {C, D, M, P}›
‹rk {A, B, M, P} = 2› ‹rk {C, D, M, P} = 2› add_le_cancel_left add_numeral_left antisym
insert_absorb2 numeral_Bit1 numeral_One numeral_plus_one one_add_one one_le_numeral
order_trans rk_ax_couple rk_ax_singleton)
qed

(* The following lemma allows to derive that there exists two lines that do not meet, i.e that belong
to two different planes *)
lemma rk_ax_dim_alt: "∃A B C D. ∀M. rk {A,B,M} ≠ 2 ∨ rk {C,D,M} ≠ 2"
proof-
obtain A B C D where f1:"rk {A,B,C,D} ≥ 4"
using rk_ax_dim
by auto
have "∀M. rk {A,B,M} ≠ 2 ∨ rk {C,D,M} ≠ 2"
proof
fix M
have "{A,B,C,D,M} = {A,B,M} ∪ {C,D,M}"
by auto
then have "rk {A,B,C,D,M} + rk {M} ≤ rk {A,B,M} + rk {C,D,M}"
by (smt le_inf_iff matroid_ax_3_alt order_trans subset_insertI)
then have "rk {A,B,C,D,M} ≤ 3" if "rk {A,B,M} = 2" and "rk {C,D,M} = 2"
not_le numeral_3_eq_3 numeral_One numeral_plus_one one_add_one rk_ax_singleton that(1)
that(2))
then have "rk {A,B,C,D} ≤ 3" if "rk {A,B,M} = 2" and "rk {C,D,M} = 2"
by (smt insert_commute matroid_ax_2 order_trans subset_insertI that(1) that(2))
thus "rk {A, B, M} ≠ 2 ∨ rk {C, D, M} ≠ 2 "
using ‹4 ≤ rk {A, B, C, D}›
by linarith
qed
thus "∃A B C D. ∀M. rk {A, B, M} ≠ 2 ∨ rk {C, D, M} ≠ 2"
by blast
qed

lemma rk_empty: "rk {} = 0"
proof-
have "rk {} ≥ 0"
by simp
have "rk {} ≤ 0"
by (metis card.empty matroid_ax_1b)
thus "rk {} = 0"
by blast
qed

lemma matroid_ax_2_alt: "rk X ≤ rk (X ∪ {x}) ∧ rk (X ∪ {x}) ≤ rk X + 1"
proof
have "X ⊆ X ∪ {x}"
by auto
thus "rk X ≤ rk (X ∪ {x})"
have "rk {x} ≤ 1"
by (metis One_nat_def card.empty card_Suc_eq insert_absorb insert_not_empty matroid_ax_1b)
thus "rk (X ∪ {x}) ≤ rk X + 1"
by (metis add_leD1 le_antisym matroid_ax_3 rk_ax_singleton)
qed

lemma matroid_ax_3_alt': "rk (X ∪ {y}) = rk (X ∪ {z}) ⟶ rk (X ∪ {z}) = rk X ⟶ rk X = rk (X ∪ {y,z})"
proof-
have i1:"rk X ≤ rk (X ∪ {y,z})"
using matroid_ax_2
by blast
have i2:"rk X ≥ rk (X ∪ {y,z})" if "rk (X ∪ {y}) = rk (X ∪ {z})" and "rk (X ∪ {z}) = rk X"
proof-
have "(X ∪ {y}) ∪ (X ∪ {z}) = X ∪ {y,z}"
by blast
then have "rk (X ∪ {y,z}) + rk X ≤ rk X + rk X"
by (metis ‹rk (X ∪ {y}) = rk (X ∪ {z})› ‹rk (X ∪ {z}) = rk X› inf_sup_ord(3) le_inf_iff
matroid_ax_3_alt)
thus "rk (X ∪ {y,z}) ≤ rk X"
by simp
qed
thus "rk (X ∪ {y}) = rk (X ∪ {z}) ⟶ rk (X ∪ {z}) = rk X ⟶ rk X = rk (X ∪ {y, z})"
using antisym i1
by blast
qed

lemma rk_ext:
assumes "rk X ≤ 3"
shows "∃P. rk(X ∪ {P}) = rk X + 1"
proof-
obtain A B C D where "rk {A,B,C,D} ≥ 4"
using rk_ax_dim
by auto
have f1:"rk (X ∪ {A, B, C, D}) ≥ 4"
by (metis Un_upper2 ‹4 ≤ rk {A, B, C, D}› matroid_ax_2 sup.coboundedI2 sup.orderE)
have "rk (X ∪ {A, B, C, D}) = rk X" if "rk(X ∪ {A}) = rk(X ∪ {B})" and "rk(X ∪ {B}) = rk(X ∪ {C})"
and "rk(X ∪ {C}) = rk(X ∪ {D})" and "rk(X ∪ {D}) = rk X"
using matroid_ax_3_alt' that(1) that(2) that(3) that(4)
by auto
then have f2:"rk (X ∪ {A, B, C, D}) ≤ 3" if "rk(X ∪ {A}) = rk(X ∪ {B})" and "rk(X ∪ {B}) = rk(X ∪ {C})"
and "rk(X ∪ {C}) = rk(X ∪ {D})" and "rk(X ∪ {D}) = rk X"
using assms that(1) that(2) that(3) that(4)
by linarith
from f1 and f2 have "False" if "rk(X ∪ {A}) = rk(X ∪ {B})" and "rk(X ∪ {B}) = rk(X ∪ {C})"
and "rk(X ∪ {C}) = rk(X ∪ {D})" and "rk(X ∪ {D}) = rk X"
using that(1) that(2) that(3) that(4)
by linarith
then have "rk (X ∪ {A}) = rk X + 1 ∨ rk (X ∪ {B}) = rk X + 1 ∨ rk (X ∪ {C}) = rk X + 1 ∨
rk (X ∪ {D}) = rk X + 1"
by (smt One_nat_def Suc_le_eq Suc_numeral Un_upper2 ‹4 ≤ rk {A, B, C, D}›
‹⟦rk (X ∪ {A}) = rk (X ∪ {B}); rk (X ∪ {B}) = rk (X ∪ {C}); rk (X ∪ {C}) = rk (X ∪ {D}); rk (X ∪ {D}) = rk X⟧ ⟹ rk (X ∪ {A, B, C, D}) = rk X›
not_less semiring_norm(2) semiring_norm(8) sup.coboundedI2 sup.orderE)
thus "∃P . rk (X ∪ {P}) = rk X + 1"
by blast
qed

lemma rk_singleton : "∀P. rk {P} = 1"
proof
fix P
have f1:"rk {P} ≤ 1"
by (metis One_nat_def card.empty card_Suc_eq insert_absorb insert_not_empty matroid_ax_1b)
have f2:"rk {P} ≥ 1"
using rk_ax_singleton
by auto
from f1 and f2 show "rk {P} = 1"
using antisym
by blast
qed

lemma rk_singleton_bis :
assumes "A = B"
shows "rk {A, B} = 1"

lemma rk_couple :
assumes "A ≠ B"
shows "rk {A, B} = 2"
proof-
have f1:"rk {A, B} ≤ 2"
by (metis insert_is_Un matroid_ax_2_alt one_add_one rk_singleton)
have f2:"rk {A, B} ≥ 2"
from f1 and f2 show "?thesis"
qed

lemma rk_triple_le : "rk {A, B, C} ≤ 3"
by (metis Suc_numeral Un_commute insert_absorb2 insert_is_Un linear matroid_ax_2_alt numeral_2_eq_2
numeral_3_eq_3 numeral_le_one_iff numeral_plus_one rk_couple rk_singleton semiring_norm(70))

lemma rk_couple_to_singleton :
assumes "rk {A, B} = 1"
shows "A = B"
proof-
have "rk {A, B} = 2" if "A ≠ B"
using rk_couple
thus "A = B"
using assms
by auto
qed

lemma rk_triple_to_rk_couple :
assumes "rk {A, B, C} = 3"
shows "rk {A, B} = 2"
proof-
have "rk {A, B} ≤ 2"
using matroid_ax_1b
by (metis one_le_numeral rk_ax_couple rk_couple rk_singleton_bis)
have "rk {A, B, C} ≤ 2" if "rk {A, B} = 1"
using matroid_ax_2_alt[of "{A, B}" C]
then have "rk {A, B} ≥ 2"
using assms rk_ax_couple rk_singleton_bis
by force
thus "rk {A, B} = 2"
by (simp add: ‹rk {A, B} ≤ 2› le_antisym)
qed

end



# Theory Desargues_2D

theory Desargues_2D
imports Main Higher_Projective_Space_Rank_Axioms Matroid_Rank_Properties
begin

(* Author: Anthony Bordg, University of Cambridge, apdb3@cam.ac.uk .*)

text ‹
Contents:
▪ We prove Desargues's theorem: if two triangles ABC and A'B'C' are perspective from a point P (ie.
the lines AA', BB' and CC' are concurrent in P), then they are perspective from a line (ie. the points
‹α = BC ∩ B'C'›, ‹β = AC ∩ A'C'› and ‹γ = AB ∩ A'B'› are collinear).
In this file we restrict ourself to the case where the two triangles ABC and A'B'C' are coplanar.
›

section ‹Desargues's Theorem: The Coplanar Case›

definition desargues_config_2D ::
"[Points, Points, Points, Points, Points, Points, Points, Points, Points, Points] ⇒ bool"
where "desargues_config_2D A B C A' B' C' P α β γ ≡ rk {A, B, C} = 3 ∧ rk {A', B', C'} = 3 ∧
rk {A, A', P} = 2 ∧ rk {B, B', P} = 2 ∧ rk {C, C', P} = 2 ∧ rk {A, B, γ} = 2 ∧ rk {A', B', γ} = 2 ∧
rk {A, C, β} = 2 ∧ rk {A', C', β} = 2 ∧ rk {B, C, α} = 2 ∧ rk {B', C', α} = 2 ∧
rk {A, B, C, A', B', C'} = 3 ∧
― ‹We add the following non-degeneracy conditions›
rk {A, B, P} = 3 ∧ rk {A, C, P} = 3 ∧ rk {B, C, P} = 3 ∧
rk {A, A'} = 2 ∧ rk {B, B'} = 2 ∧ rk {C, C'} = 2"

lemma coplanar_ABCA'B'C'P :
assumes "rk {A, A'} = 2" and "rk {A, B, C, A', B', C'} = 3" and "rk {A, A', P} = 2"
shows "rk {A, B, C, A', B', C', P} = 3"
proof-
have "rk {A, B, C, A', B', C', P} + rk {A, A'} ≤ rk {A, B, C, A', B', C'} + rk {A, A', P}"
using matroid_ax_3_alt[of "{A, A'}" "{A, B, C, A', B', C'}" "{A, A', P}"]
then have "rk {A, B, C, A', B', C', P} ≤ 3"
using assms(1) assms(2) assms(3)
by linarith
then show "rk {A, B, C, A', B', C', P} = 3"
using assms(2) matroid_ax_2
by (metis Un_insert_right Un_upper2 le_antisym sup_bot.right_neutral)
qed

lemma non_colinear_A'B'P :
assumes "rk {A, B, P} = 3" and "rk {A, A', P} = 2" and "rk {B, B', P} = 2" and "rk {A', P} = 2"
and "rk {B', P} = 2"
shows "rk {A', B', P} = 3"
proof-
have f1:"rk {A', B', P} ≤ 3"
using rk_triple_le by auto
have "rk {A, B, A', B', P} ≥ 3"
using assms(1) matroid_ax_2
by (metis insert_mono insert_subset subset_insertI)
then have f2:"rk {A, B, A', B', P} = 3"
using matroid_ax_3_alt[of "{P}" "{A, A', P}" "{B, B', P}"] assms(2) assms(3)
have "rk {A, B, A', B', P} + rk {B', P} ≤ rk {A, A', B', P} + rk {B, B', P}"
using matroid_ax_3_alt[of "{B', P}" "{A, A', B', P}" "{B, B', P}"]
then have "rk {A, A', B', P} ≥ 3"
using f2 assms(3) assms(5) by linarith
then have f3:"rk {A, A', B', P} = 3"
using f2 matroid_ax_2
by (metis eq_iff insert_commute subset_insertI)
have "rk {A, A', B', P} + rk {A', P} ≤ rk {A', B', P} + rk {A, A', P}"
using matroid_ax_3_alt[of "{A', P}" "{A', B', P}" "{A, A', P}"]
then have "rk {A', B', P} ≥ 3"
using f3 assms(2) assms(4) by linarith
thus "rk {A', B', P} = 3"
using f1 by auto
qed

lemma desargues_config_2D_non_collinear_P :
assumes "desargues_config_2D A B C A' B' C' P α β γ" and "rk {A', P} = 2" and "rk {B', P} = 2"
and "rk {C', P} = 2"
shows "rk {A', B', P} = 3" and "rk {A', C', P} = 3" and "rk {B', C', P} = 3"
proof-
show "rk {A', B', P} = 3"
using non_colinear_A'B'P assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ] assms(2)
assms(3)
by blast
show "rk {A', C', P} = 3"
using non_colinear_A'B'P assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ] assms(2)
assms(4)
by blast
show "rk {B', C', P} = 3"
using non_colinear_A'B'P assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ] assms(3)
assms(4)
by blast
qed

lemma rk_A'B'PQ :
assumes "rk {A, A'} = 2" and "rk {A, B, C, A', B', C'} = 3" and "rk {A, A', P} = 2" and
"rk {A, B, P} = 3" and "rk {B, B', P} = 2" and "rk {A', P} = 2" and "rk {B', P} = 2" and
"rk {A, B, C, A', B', C', P, Q} ≥ 4"
shows "rk {A', B', P, Q} = 4"
proof-
have "card {A', B', P, Q} ≤ 4"
by (smt One_nat_def Suc_numeral card.insert card.empty finite.emptyI finite_insert insert_absorb
insert_not_empty linear nat_add_left_cancel_le numeral_3_eq_3 numeral_Bit0 numeral_code(3)
numeral_le_one_iff numerals(1) one_plus_numeral semiring_norm(4) semiring_norm(69)
semiring_norm(70) semiring_norm(8))
then have f1:"rk {A', B', P, Q} ≤ 4"
using matroid_ax_1b dual_order.trans by blast
have "rk {A, B, C, A', B', C', P, Q} + rk {A', B', P} ≤ rk {A', B', P, Q} + rk {A, B, C, A', B', C', P}"
using matroid_ax_3_alt[of "{A', B', P}" "{A', B', P, Q}" "{A, B, C, A', B', C', P}"]
then have "rk {A', B', P, Q} ≥ rk {A, B, C, A', B', C', P, Q} + rk {A', B', P} - rk {A, B, C, A', B', C', P}"
using le_diff_conv
by blast
then have f2:"rk {A', B', P, Q} ≥ 4"
using assms non_colinear_A'B'P coplanar_ABCA'B'C'P
from f1 and f2 show "rk {A', B', P, Q} = 4"
qed

lemma desargues_config_2D_rkA'B'PQ_rkA'C'PQ_rkB'C'PQ :
assumes "desargues_config_2D A B C A' B' C' P α β γ" and "rk {A', P} = 2" and "rk {B', P} = 2"
and "rk {C', P} = 2" and "rk {A, B, C, A', B', C', P, Q} ≥ 4"
shows "rk {A', B', P, Q} = 4" and "rk {A', C', P, Q} = 4" and "rk {B', C', P, Q} = 4"
proof-
show "rk {A', B', P, Q} = 4"
using rk_A'B'PQ[of "A" "A'" "B" "C" "B'" "C'" "P" "Q"] assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ]
assms(2) assms(3) assms(5)
by blast
show "rk {A', C', P, Q} = 4"
using rk_A'B'PQ[of "A" "A'" "C" "B" "C'" "B'" "P" "Q"] assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ]
assms(2) assms(4) assms(5)
by (metis insert_commute)
show "rk {B', C', P, Q} = 4"
using rk_A'B'PQ[of "B" "B'" "C" "A" "C'" "A'" "P" "Q"] assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ]
assms(3) assms(4) assms(5)
by (metis insert_commute)
qed

lemma rk_A'B'PR :
assumes "rk {P, Q, R} = 2" and "rk {P, R} = 2" and "rk {A', B', P, Q} = 4"
shows "rk {A', B', P, R} = 4"
proof-
have "card {A', B', P, R} ≤ 4"
by (smt Suc_numeral assms(2) card.empty card_insert_disjoint dual_order.trans finite.emptyI
finite_insert insert_absorb linear nat_add_left_cancel_le numeral_2_eq_2 numeral_3_eq_3
numeral_Bit0 numeral_code(3) numeral_le_one_iff rk_singleton rk_triple_le semiring_norm(2)
semiring_norm(69) semiring_norm(8))
then have f1:"rk {A', B', P, R} ≤ 4"
using dual_order.trans matroid_ax_1b
by auto
have f2:"rk {A', B', P, Q, R} + rk {P, R} ≤ rk {A', B', P, R} + rk {P, Q, R}"
using matroid_ax_3_alt[of "{P, R}" "{A', B', P, R}" "{P, Q, R}"]
have f3:"rk {A', B', P, Q, R} ≥ 4"
using matroid_ax_2 assms(3)
by (metis insert_mono subset_insertI)
from f2 and f3 have f4:"rk {A', B', P, R} ≥ 4"
using assms(1) assms(2)
by linarith
thus "rk {A', B', P, R} = 4"
using f1 f4
qed

lemma rk_A'C'PR :
assumes "rk {P, Q, R} = 2" and "rk {P, R} = 2" and "rk {A', C', P, Q} = 4"
shows "rk {A', C', P, R} = 4"
using assms(1) assms(2) assms(3) rk_A'B'PR
by blast

lemma rk_B'C'PR :
assumes "rk {P, Q, R} = 2" and "rk {P, R} = 2" and "rk {B', C', P, Q} = 4"
shows "rk {B', C', P, R} = 4"
using assms(1) assms(2) assms(3) rk_A'C'PR
by blast

lemma rk_ABA' :
assumes "rk {A, B, P} = 3" and "rk {A, A'} = 2" and "rk {A, A', P} = 2"
shows "rk {A, B, A'} = 3"
proof-
have "rk {A, B, A', P} + rk {A, A'} ≤ rk {A, B, A'} + rk {A, A', P}"
using matroid_ax_3_alt[of "{A, A'}" "{A, B, A'}" "{A, A', P}"]
then have "rk {A, B, A'} ≥ 3"
using assms matroid_ax_2
by (smt eq_iff insert_absorb2 insert_commute non_colinear_A'B'P rk_couple)
thus "rk {A, B, A'} = 3"
qed

lemma desargues_config_2D_non_collinear :
assumes "desargues_config_2D A B C A' B' C' P α β γ"
shows "rk {A, B, A'} = 3" and "rk {A, B, B'} = 3" and "rk {A, C, C'} = 3"
proof-
show "rk {A, B, A'} = 3"
using assms desargues_config_2D_def[of A B C A' B' C' P α β γ] rk_ABA'
by auto
show "rk {A, B, B'} = 3"
using assms desargues_config_2D_def[of A B C A' B' C' P α β γ] rk_ABA'
by (smt insert_commute)
show "rk {A, C, C'} = 3"
using assms desargues_config_2D_def[of A B C A' B' C' P α β γ] rk_ABA'
by (smt insert_commute)
qed

lemma rk_Aa :
assumes "rk {A, B, P} = 3" and "rk {A, A'} = 2" and "rk {A, A', P} = 2" and "rk {Q, A', a} = 2"
and "rk {A, B, C, A', B', C', P, Q} ≥ 4" and "rk {A, B, C, A', B', C'} ≤ 3"
shows "rk {A, a} = 2"
proof-
have "rk {Q, A', A, a} + rk {a} ≤ rk {Q, A', a} + rk {A, a}"
using matroid_ax_3_alt[of "{a}" "{Q, A', a}" "{A, a}"]
then have "rk {Q, A', A, a} ≤ rk {Q, A', a} + rk {A, a} - rk {a}"
by blast
then have "rk {Q, A', A, a} ≤ 2" if "rk {A, a} = 1"
using assms(4)
then have "rk {Q, A', A} ≤ 2" if "rk {A, a} = 1"
using matroid_ax_2
by (metis One_nat_def assms(4) le_numeral_extra(4) nat_add_left_cancel_le numeral_2_eq_2
then have "rk {Q, A', A} = 2" if "rk {A, a} = 1"
using assms(2) matroid_ax_2
by (metis assms(4) numeral_eq_one_iff rk_couple semiring_norm(85) that)
then have "rk {A, A', P, Q} = 2" if "rk {A, a} = 1"
using assms(3) matroid_ax_3_alt'[of "{A, A'}" "P" "Q"]
by (simp add: assms(2) insert_commute that)
then have f1:"rk {A, A', B, P, Q} ≤ 3" if "rk {A, a} = 1"
numeral_2_eq_2 numeral_3_eq_3 sup_bot.right_neutral that)
have "rk {A, B, C, A', B', C', P, Q} + rk {A, B, A'} ≤ rk {A, A', B, P, Q} + rk {A, B, C, A', B', C'}"
using matroid_ax_3_alt[of "{A, B, A'}" "{A, A', B, P, Q}" "{A, B, C, A', B', C'}"]
then have "rk {A, B, C, A', B', C', P, Q} ≤ rk {A, A', B, P, Q} + rk {A, B, C, A', B', C'} - rk {A, B, A'}"
by linarith
then have "rk {A, B, C, A', B', C', P, Q} ≤ 3" if "rk {A, a} = 1"
using assms(1) assms(2) assms(3) assms(6) f1 rk_ABA'
by (smt ‹rk {A, B, C, A', B', C', P, Q} + rk {A, B, A'} ≤ rk {A, A', B, P, Q} + rk {A, B, C, A', B', C'}›
then have "¬ (rk {A, a} = 1)"
using assms(5)
by linarith
thus "rk {A, a} = 2"
using rk_couple rk_singleton_bis
by blast
qed

lemma desargues_config_2D_rkAa_rkBb_rkCc :
assumes "desargues_config_2D A B C A' B' C' P α β γ" and "rk {A, B, C, A', B', C', P, Q} ≥ 4"
and "rk {Q, A', a} = 2" and "rk {Q, B', b} = 2" and "rk {Q, C', c} = 2"
shows "rk {A, a} = 2" and "rk {B, b} = 2" and "rk {C, c} = 2"
proof-
show "rk {A, a} = 2"
using rk_Aa assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ] assms(2) assms(3)
by (metis rk_triple_le)
show "rk {B, b} = 2"
using rk_Aa assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ] assms(2) assms(4)
by (smt insert_commute rk_triple_le)
show "rk {C, c} = 2"
using rk_Aa[of "C" "A" "P" "C'" "Q" "c" "B" "B'" "A'"] assms(1)
desargues_config_2D_def[of A B C A' B' C' P α β γ] assms(2) assms(5)
by (metis insert_commute rk_triple_le)
qed

lemma rk_ABPRa :
assumes "rk {A, B, P} = 3" and "rk {A, B, C, A', B', C', P} = 3" and "rk {P, Q, R} = 2"
and "rk {P, R} = 2" and "rk {A', B', P, Q} = 4"
shows "rk {A, B, P, R, a} ≥ 4"
proof-
have "rk {A', B', P, R, a, A, B} ≥ rk {A', B', P, R}"
using matroid_ax_2
by auto
then have f1:"rk {A', B', P, R, a, A, B} ≥ 4"
using rk_A'B'PR assms(3) assms(4) assms(5)
by auto
have f2:"rk {A', B', A, B, P} ≤ 3"
using matroid_ax_2 assms(2)
by (smt insertI1 insert_subset subset_insertI)
have "rk {A', B', P, R, a, A, B} + rk {A, B, P} ≤ rk {A, B, P, R, a} + rk {A', B', A, B, P}"
using matroid_ax_3_alt[of "{A, B, P}" "{A, B, P, R, a}" "{A', B', A, B, P}"]
then have "rk {A, B, P, R, a} ≥ rk {A', B', P, R, a, A, B} + rk {A, B, P} - rk {A', B', A, B, P}"
by linarith
thus "rk {A, B, P, R, a} ≥ 4"
using f1 assms(1) f2
by linarith
qed

lemma rk_ABPa :
assumes "rk {A, B, P} = 3" and "rk {A, A'} = 2" and "rk {A, A', P} = 2" and "rk {Q, A', a} = 2"
and "rk {A, B, C, A', B', C', P, Q} ≥ 4" and "rk {A, B, C, A', B', C', P} = 3" and "rk {P, Q, R} = 2"
and "rk {P, R} = 2" and "rk {A', B', P, Q} = 4" and "rk {R, A, a} = 2"
shows "rk {A, B, P, a} ≥ 4"
proof-
have "rk {A, B, C, A', B', C'} ≤ 3"
using matroid_ax_2 assms(6)
by (smt insert_iff subsetI)
then have f1:"rk {A, a} = 2"
using assms(1) assms(2) assms(3) assms(4) assms(5) rk_Aa
by blast
have f2:"rk {A, B, P, R, a} ≥ 4"
using assms(1) assms(6) assms(7) assms(8) assms(9) rk_ABPRa
by blast
have "rk {A, B, P, R, a} + rk {A, a} ≤ rk {A, B, P, a} + rk {R, A, a}"
using matroid_ax_3_alt[of "{A, a}" "{A, B, P, a}" "{R, A, a}"]
thus "rk {A, B, P, a} ≥ 4"
using f1 f2 assms(10)
qed

lemma desargues_config_2D_rkABPa_rkABPb_rkABPc :
assumes "desargues_config_2D A B C A' B' C' P α β γ" and "rk {A, B, C, A', B', C', P, Q} ≥ 4"
and "rk {P, Q, R} = 2" and "rk {P, R} = 2" and "rk {A', P} = 2" and "rk {B', P} = 2" and
"rk {Q, A', a} = 2" and "rk {R, A, a} = 2" and "rk {Q, B', b} = 2" and "rk {R, B, b} = 2" and
"rk {Q, C', c} = 2" and "rk {R, C, c} = 2"
shows "rk {A, B, P, a} ≥ 4" and "rk {A, B, P, b} ≥ 4" and "rk {A, B, P, c} ≥ 4"
proof-
have f1:"rk {A, B, C, A', B', C', P} = 3"
using assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ] coplanar_ABCA'B'C'P
by auto
have f2:"rk {A', B', P, Q} = 4"
using assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ] assms(2) assms(5) assms(6)
rk_A'B'PQ[of "A" "A'" "B" "C" "B'" "C'" "P" "Q"]
by auto
show "rk {A, B, P, a} ≥ 4"
using f1 f2 assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ] assms(7) assms(2) assms(3)
assms(4) assms(8) rk_ABPa
by auto
show "rk {A, B, P, b} ≥ 4"
using f1 f2 assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ] assms(9) assms(2) assms(3)
assms(4) assms(10) rk_ABPa[of "B" "A" "P" "B'" "Q" "b" "C" "A'" "C'" "R"]
by (metis insert_commute)
show "rk {A, B, P, c} ≥ 4"
proof-
have f3:"rk {A, B, P, R, c} ≥ 4"
using rk_ABPRa[of A B P C A' B' C' Q R c] assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ]
f1 assms(3) assms(4) f2
by auto
have "{A, B, P, R, c} ⊆ {A, B, C, P, R, c}"
by auto
then have f4:"rk {A, B, C, P, R, c} ≥ 4"
using matroid_ax_2 f3
by (meson dual_order.trans)
have "rk {A, B, C, P, R, c} + rk {C, c} ≤ rk {A, B, C, P, c} + rk {R, C, c}"
using matroid_ax_3_alt[of "{C,c}" "{A, B, C, P, c}" "{R, C, c}"]
then have f5:"rk {A, B, C, P, c} ≥ 4"
using f4 assms(12) desargues_config_2D_rkAa_rkBb_rkCc assms(1) assms(9) assms(11) assms(2) assms(7)
by auto
have f6:"rk {A, B, C, P} ≤ 3"
using matroid_ax_2 f1
by (smt insert_iff subsetI)
have "rk {A, B, C, P, c} + rk {A, B, P} ≤ rk {A, B, P, c} + rk {A, B, C, P}"
using matroid_ax_3_alt[of "{A, B, P}" "{A, B, P, c}" "{A, B, C, P}"]
then have "rk {A, B, P, c} ≥ rk {A, B, C, P, c}"
using assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ] f6
by linarith
thus "rk {A, B, P, c} ≥ 4"
using f5
by linarith
qed
qed

lemma rk_AA'C :
assumes "rk {A, C, P} = 3" and "rk {A, A'} = 2" and "rk {A, A', P} = 2"
shows "rk {A, A', C} ≥ 3"
proof-
have f1:"rk {A, C, A', P} ≥ 3"
using assms(1) matroid_ax_2
by (metis insert_commute subset_insertI)
have "rk {A, C, A', P} + rk {A, A'} ≤ rk {A, A', C} + rk {A, A', P}"
using matroid_ax_3_alt[of "{A, A'}" "{A, A', C}" "{A, A', P}"]
thus "rk {A, A', C} ≥ 3"
using f1 assms(2) assms(3)
by linarith
qed

lemma rk_AA'C' :
assumes "rk {A', C', P} = 3" and "rk {A, A'} = 2" and "rk {A, A', P} = 2"
shows "rk {A, A', C'} ≥ 3"
by (smt assms(1) assms(2) assms(3) insert_commute rk_AA'C)

lemma rk_AA'Ca :
assumes "rk {A, A', C} ≥ 3" and "rk {A, B, P, a} ≥ 4" and "rk {A, B, C, A', B', C', P} = 3"
shows "rk {A, A', C, a} ≥ 4"
proof-
have f1:"rk {A, A', C, a, B, P} ≥ 4"
using assms(2) matroid_ax_2
by (smt dual_order.trans insert_commute insert_mono insert_subset subset_insertI)
have f2:"rk {A, B, C, P, A'} ≤ 3"
using assms(3) matroid_ax_2
by (smt empty_subsetI insert_commute insert_mono semiring_norm(3))
have "rk {A, A', C, a, B, P} + rk {A, A', C} ≤ rk {A, A', C, a} + rk {A, B, C, P, A'}"
using matroid_ax_3_alt[of "{A, A', C}" "{A, A', C, a}" "{A, B, C, P, A'}"]
then have "rk {A, A', C, a} ≥ rk {A, A', C, a, B, P} + rk {A, A', C} - rk {A, B, C, P, A'}"
using le_diff_conv
by blast
thus "rk {A, A', C, a} ≥ 4"
using f1 assms(1) f2
by linarith
qed

lemma rk_AA'C'a :
assumes "rk {A, A', C'} ≥ 3" and "rk {A, B, P, a} ≥ 4" and "rk {A, B, C, A', B', C', P} = 3"
shows "rk {A, A', C', a} ≥ 4"
by (smt assms(1) assms(2) assms(3) insert_commute rk_AA'Ca)

lemma rk_Ra :
assumes "rk {Q, A', a} = 2" and "rk {P, Q, R} = 2" and "rk {R, Q} = 2" and "rk {A, A', P} = 2"
and "rk {A', P} = 2" and "rk {A, B, C, A', B', C', P} = 3" and "rk {A, B, A'} = 3" and
"rk {A, B, C, A', B', C', P, Q} ≥ 4"
shows "rk {R, a} = 2"
proof-
have "R = a" if "rk {R, a} = 1"
using rk_couple_to_singleton
then have "rk {R, Q, A'} = 2" if "rk {R, a} = 1"
using assms(1)
then have f1:"rk {P, Q, R, A'} = 2" if "rk {R, a} = 1"
using assms(2) assms(3) matroid_ax_3_alt'
by (metis Un_empty_right Un_insert_right insert_commute that)
have "rk {P, Q, R, A', A} + rk {A', P} ≤ rk {A, A', P} + rk {P, Q, R, A'}"
using matroid_ax_3_alt[of "{A', P}" "{A, A', P}" "{P, Q, R, A'}"]
then have "rk {P, Q, R, A', A} = 2" if "rk {R, a} = 1"
using assms(4) f1 assms(5)
by (metis Un_insert_right add_le_cancel_right insert_is_Un le_antisym matroid_ax_2 subset_insertI that)
then have f2:"rk {P, Q, R, A', A, B} ≤ 3" if "rk {R, a} = 1"
using matroid_ax_2_alt[of "{P, Q, R, A', A}" "B"]
have f3:"rk {A, B, A', P} ≥ 3"
using assms(7) matroid_ax_2
by (metis insert_commute subset_insertI)
have "rk {P, Q, R, A', A, B, C, B', C'} + rk {A, B, A', P} ≤ rk {P, Q, R, A', A, B} + rk {A, B, C, A', B', C', P}"
using matroid_ax_3_alt[of "{A, B, A', P}" "{P, Q, R, A', A, B}" "{A, B, C, A', B', C', P}"]
then have f4:"rk {P, Q, R, A', A, B, C, B', C'} ≤ 3" if "rk {R, a} = 1"
using f2 f3 assms(6) that
by linarith
have f5:"rk {P, Q, R, A', A, B, C, B', C'} ≥ rk {A, B, C, A', B', C', P, Q}"
using matroid_ax_2
by auto
thus "rk {R, a} = 2" using f4 f5 assms(8)
numeral_Bit0 order.trans rk_couple rk_singleton_bis)
qed

lemma desargues_config_2D_rkRa_rkRb_rkRc :
assumes "desargues_config_2D A B C A' B' C' P α β γ" and "rk {A, B, C, A', B', C', P, Q} ≥ 4"
and "rk {P, Q, R} = 2" and "rk {Q, R} = 2" and "rk {Q, A', a} = 2" and "rk {Q, B', b} = 2" and
"rk {Q, C', c} = 2" and "rk {A', P} = 2" and "rk {B', P} = 2" and "rk {C', P} = 2"
shows "rk {R, a} = 2" and "rk {R, b} = 2" and "rk {R, c} = 2"
proof-
have f1:"rk {A, B, C, A', B', C', P} = 3"
using coplanar_ABCA'B'C'P assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ]
by blast
have f2:"rk {A, B, A'} = 3"
using desargues_config_2D_non_collinear assms(1)
by auto
have f3:"rk {A, B, B'} = 3"
using desargues_config_2D_non_collinear assms(1)
by auto
have f4:"rk {A, C, C'} = 3"
using desargues_config_2D_non_collinear assms(1)
by auto
show "rk {R, a} = 2"
using f1 f2 rk_Ra[of Q A' a P R A B C B' C'] assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ]
assms(2) assms(3) assms(4) assms(5) assms(8)
by (metis insert_commute)
show "rk {R, b} = 2"
using f1 f3 rk_Ra[of Q B' b P R B A C A' C'] assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ]
assms(2) assms(3) assms(4) assms(6) assms(9)
by (metis insert_commute)
show "rk {R, c} = 2"
using f1 f4 rk_Ra[of Q C' c P R C A B A' B'] assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ]
assms(2) assms(3) assms(4) assms(7) assms(10)
by (metis insert_commute)
qed

lemma rk_acACβ :
assumes "rk {R, A, a} = 2" and "rk {R, C, c} = 2" and "rk {A, C} = 2" and "rk {A, C, β} = 2"
and "rk {Q, A', a} = 2" and "rk {A, A', C, a} ≥ 4"
shows "rk {a, c, A, C, β} = 3"
proof-
have "rk {a, c, A, C, R} + rk {R} ≤ rk {R, A, a} + rk {R, C, c}"
using matroid_ax_3_alt[of "{R}" "{R, A, a}" "{R, C, c}"]
then have f1:"rk {a, c, A, C, R} ≤ 3"
using assms(1) assms(2)
by (metis Suc_1 Suc_eq_plus1 Suc_le_mono add_Suc_right numeral_3_eq_3 numeral_nat(1) numerals(1)
rk_singleton)
have "rk {a, c, A, C, R, β} + rk {A, C} ≤ rk {a, c, A, C, R} + rk {A, C, β}"
using matroid_ax_3_alt[of "{A, C}" "{a, c, A, C, R}" "{A, C, β}"]
then have f2:"rk {a, c, A, C, R, β} ≤ 3"
using f1 assms(3) assms(4)
by linarith
have "{a, c, A, C, β} ⊆ {a, c, A, C, R, β}"
by auto
then have f3:"rk {a, c, A, C, β} ≤ 3"
using matroid_ax_2 f2
by (meson order_trans)
have f4:"rk {A, A', C, a, c, Q} ≥ 4"
using matroid_ax_2 assms(6)
by (smt dual_order.trans insert_commute insert_mono insert_subset subset_insertI)
have "rk {A, A', C, a, c, Q} + rk {a} ≤ rk {a, c, A, C} + rk {Q, A', a}"
using matroid_ax_3_alt[of "{a}" "{a, c, A, C}" "{Q, A', a}"]
then have "rk {a, c, A, C} ≥ rk {A, A', C, a, c, Q} + rk {a} - rk {Q, A', a}"
using le_diff_conv
by blast
then have "rk {a, c, A, C} ≥ 3"
using f4 assms(5)
by (smt One_nat_def ‹rk {A, A', C, a, c, Q} + rk {a} ≤ rk {a, c, A, C} + rk {Q, A', a}›
card.empty card.insert dual_order.antisym finite.intros(1) insert_absorb insert_not_empty
matroid_ax_1b nat_1_add_1 numeral_3_eq_3 numeral_Bit0 order.trans rk_ax_singleton)
then have "rk {a, c, A, C, β} ≥ 3"
using matroid_ax_2
by (metis Un_insert_right Un_upper2 dual_order.trans sup_bot.comm_neutral)
thus "rk {a, c, A, C, β} = 3"
using f3 le_antisym
by blast
qed

lemma rk_acA'C'β :
assumes "rk {Q, A', a} = 2" and "rk {Q, C', c} = 2" and "rk {A', C'} = 2" and "rk {A', C', β} = 2"
and "rk {R, A, a} = 2" and "rk {A', A, C', a} ≥ 4"
shows "rk {a, c, A', C', β} = 3"
using assms rk_acACβ
by blast

lemma plane_representation_change :
assumes "rk {A, B, C, P} = 3" and "rk {B, C, P} = 3" and "rk {A, B, C, Q} = 4"
shows "rk {P, B, C, Q} = 4"
proof-
have "rk {P, B, C, Q} ≤ 4" using assms(2) matroid_ax_2_alt[of "{B, C, P}" "Q"]
have "rk {A, B, C, Q, P} + rk {B, C, P} ≤ rk {P, B, C, Q} + rk {A, B, C, P}"
using matroid_ax_3_alt[of "{B, C, P}" "{P, B, C, Q}" "{A, B, C, P}"]
then have "rk {P, B, C, Q} ≥ 4"
using assms
subset_insertI)
thus "rk {P, B, C, Q} = 4"
by (simp add: ‹rk {P, B, C, Q} ≤ 4› antisym)
qed

lemma desargues_config_2D_rkABCP :
assumes "desargues_config_2D A B C A' B' C' P α β γ"
shows "rk {A, B, C, P} = 3"
proof-
have "rk {A, B, C} = 3"
using assms desargues_config_2D_def[of A B C A' B' C' P α β γ]
by auto
then have f1:"rk {A, B, C, P} ≥ 3"
using matroid_ax_2
by (metis empty_subsetI insert_mono)
have f2:"rk {A, B, C, A', B', C', P} = 3"
using assms desargues_config_2D_def[of A B C A' B' C' P] coplanar_ABCA'B'C'P
by auto
have "{A, B, C, P} ⊆ {A, B, C, A', B', C', P}"
by auto
then have "rk {A, B, C, P} ≤ 3"
using matroid_ax_2 f2
by metis
thus "rk {A, B, C, P} = 3"
using f1 antisym
by blast
qed

lemma desargues_config_2D_rkABCabc :
assumes "desargues_config_2D A B C A' B' C' P α β γ" and "rk {A, B, C, A', B', C', P, Q} ≥ 4"
and "rk {Q, A', a} = 2" and "rk {P, Q, R} = 2" and "rk {P, R} = 2" and "rk {R, A, a} = 2" and
"rk {A', P} = 2" and "rk {B', P} = 2"
shows "rk {A, B, C, a, b, c} ≥ 4"
proof-
have f1:"rk {A, B, C, A', B', C', P} = 3"
using assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ] coplanar_ABCA'B'C'P
by auto
have f2:"rk {A', B', P, Q} = 4"
using rk_A'B'PQ[of A A' B C B' C' P Q] assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ]
assms(2) assms(7) assms(8)
by auto
from f1 and f2 have f3:"rk {A, B, P, a} ≥ 4"
using assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ] assms(2) assms(3) assms(4)
assms(5) assms(6) rk_ABPa
by auto
have "{A, B, P, a} ⊆ {A, B, C, a, b, c, P}"
by auto
then have f4:"rk {A, B, C, a, b, c, P} ≥ 4"
using matroid_ax_2 f3
by (meson dual_order.trans)
have f5:"rk {A, B, C, P} = 3"
using assms(1) desargues_config_2D_rkABCP
by auto
have "rk {A, B, C, a, b, c, P} + rk {A, B, C} ≤ rk {A, B, C, a, b, c} + rk {A, B, C, P}"
using matroid_ax_3_alt[of "{A, B, C}" "{A, B, C, a, b, c}" "{A, B, C, P}"]
thus "rk {A, B, C, a, b, c} ≥ 4"
using f4 assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ] f5
by linarith
qed

lemma rk_abc :
assumes "desargues_config_2D A B C A' B' C' P α β γ" and "rk {A, B, C, A', B', C', P, Q} ≥ 4"
and "rk {Q, A', a} = 2" and "rk {Q, B', b} = 2" and "rk {Q, C', c} = 2" and "rk {P, Q, R} = 2" and
"rk {P, R} = 2" and "rk {Q, R} = 2" and "rk {R, A, a} = 2" and "rk {R, B, b} = 2" and
"rk {R, C, c} = 2" and "rk {A', P} = 2" and "rk {B', P} = 2" and "rk {C', P} = 2"
shows "rk {a, b, c} = 3"
proof-
have "rk {a, b, c} ≤ 3"
have "rk {A, B, C, a, b, c} ≥ 4"
using desargues_config_2D_rkABCabc assms(1) assms(13) assms(2) assms(3) assms(6) assms(7) assms(9)
assms(12)
by auto
then have f1:"rk {A, B, C, R, a, b, c} ≥ 4"
using matroid_ax_2
by (smt dual_order.trans insert_commute subset_insertI)
have f2:"rk {A, B, C, A', B', C', P} = 3"
using coplanar_ABCA'B'C'P assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ]
by auto
have f3:"rk {A, C, C'} = 3"
using assms(1) desargues_config_2D_non_collinear(3)
by auto
from f2 and f3 have f4:"rk {R, c} = 2"
using assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ] assms(2) assms(5) assms(6)
assms(8) assms(14) rk_Ra[of Q C' c P R C A B A' B']
by (metis insert_commute)
have "rk {A, B, C, R, a, b, c} + rk {R, c} ≤ rk {a, b, c, R, A, B} + rk {R, C, c}"
using matroid_ax_3_alt[of "{R, c}" "{a, b, c, R, A, B}" "{R, C, c}"]
then have f5:"rk {a, b, c, R, A, B} ≥ 4"
using f1 f4 assms(11)
by linarith
have "rk {A, B, B'} = 3"
using assms(1) desargues_config_2D_non_collinear(2)
by auto
then have f6:"rk {R, b} = 2"
using f2 assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ]
rk_Ra[of Q B' b P R B A C A' C'] assms(2) assms(4) assms(6) assms(8) assms(13)
by (metis insert_commute)
have "rk {a, b, c, R, A, B} + rk {R, b} ≤ rk {a, b, c, R, A} + rk {R, B, b}"
using matroid_ax_3_alt[of "{R, b}" "{a, b, c, R, A}" "{R, B, b}"]
then have f7:"rk {a, b, c, R, A} ≥ 4"
using f5 f6 assms(10)
by linarith
have "rk {a, b, c, R, A} + rk {a} ≤ rk {a, b, c} + rk {R, A, a}"
using matroid_ax_3_alt[of "{a}" "{a, b, c}" "{R, A, a}"]
then have "rk {a, b, c} ≥ 3"
using f7 assms(9)
by (smt One_nat_def Suc_eq_plus1 Suc_le_mono Suc_numeral add.assoc card.empty card.insert
dual_order.trans finite.intros(1) insert_absorb insert_not_empty le_antisym matroid_ax_1b
thus "rk {a, b, c} = 3"
by (simp add: ‹rk {a, b, c} ≤ 3› le_antisym)
qed

lemma rk_acβ :
assumes "desargues_config_2D A B C A' B' C' P α β γ" and "rk {A, B, C, A', B', C', P, Q} ≥ 4"
and "rk {Q, A', a} = 2" and "rk {Q, B', b} = 2" and "rk {Q, C', c} = 2" and "rk {P, Q, R} = 2" and
"rk {P, R} = 2" and "rk {Q, R} = 2" and "rk {R, A, a} = 2" and "rk {R, B, b} = 2" and
"rk {R, C, c} = 2" and "rk {A', P} = 2" and "rk {B', P} = 2" and "rk {C', P} = 2"
shows "rk {a, c, β} = 2"
proof-
have "rk {a, b, c} = 3"
using rk_abc assms
by auto
then have "rk {a, c} = 2"
by (metis insert_commute rk_triple_to_rk_couple)
then have "rk {a, c, β} ≥ 2"
using matroid_ax_2
by (metis empty_subsetI insert_mono)
have f1:"rk {a, c, A, C, A', C', β} + rk {a, c, β} ≤ rk {a, c, A, C, β} + rk {a, c, A', C', β}"
using matroid_ax_3_alt[of "{a, c, β}" "{a, c, A, C, β}" "{a, c, A', C', β}"]
have f2:"rk {A, A', C} ≥ 3"
using rk_AA'C assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ]
by auto
have f3:"rk {A, B, C, A', B', C', P} = 3"
using coplanar_ABCA'B'C'P assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ]
by auto
then have f4:"rk {A, B, P, a} ≥ 4"
using rk_ABPa assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ]
by (meson assms(12) assms(13) assms(14) assms(2) assms(3) assms(6) assms(7) assms(9)
desargues_config_2D_rkA'B'PQ_rkA'C'PQ_rkB'C'PQ(1))
have "rk {A, A', C, a} ≥ 4"
using f2 f3 f4 rk_AA'Ca[of A A' C B P a B' C']
by auto
then have f5:"rk {a, c, A, C, β} = 3"
using rk_acACβ[of R A a C c β Q A'] assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ]
assms(9) assms(11) assms(3) rk_triple_to_rk_couple
by blast
have "rk {A', A, C', a} ≥ 4"
using rk_AA'C'a[of A A' C' B P a C B'] assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ]
by (smt assms(12) assms(13) assms(14) desargues_config_2D_non_collinear_P(2) f3 f4 insert_commute
rk_AA'C)
then have f6:"rk {a, c, A', C', β} = 3"
using rk_acA'C'β[of Q A' a C' c β R A] assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ]
assms(3) assms(5) assms(9)
by (metis (full_types) insert_commute rk_triple_to_rk_couple)
have "{A, A', C, a} ⊆ {a, c, A, C, A', C', β}"
by auto
then have f7:"rk {a, c, A, C, A', C', β} ≥ 4"
using matroid_ax_2
by (meson ‹4 ≤ rk {A, A', C, a}› dual_order.trans)
then have "rk {a, c, β} ≤ 2"
using f1 f5 f6
by linarith
thus "rk {a, c, β} = 2"
using ‹2 ≤ rk {a, c, β}› le_antisym
by blast
qed

lemma rk_abγ :
assumes "desargues_config_2D A B C A' B' C' P α β γ" and "rk {A, B, C, A', B', C', P, Q} ≥ 4"
and "rk {Q, A', a} = 2" and "rk {Q, B', b} = 2" and "rk {Q, C', c} = 2" and "rk {P, Q, R} = 2" and
"rk {P, R} = 2" and "rk {Q, R} = 2" and "rk {R, A, a} = 2" and "rk {R, B, b} = 2" and
"rk {R, C, c} = 2" and "rk {A', P} = 2" and "rk {B', P} = 2" and "rk {C', P} = 2"
shows "rk {a, b, γ} = 2"
proof-
have "desargues_config_2D A C B A' C' B' P α γ β"
using assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ]
desargues_config_2D_def[of A C B A' C' B' P α γ β]
by (metis insert_commute)
thus "rk {a, b, γ} = 2"
using rk_acβ[of A C B A' C' B' P α γ β Q a c b R]
by (metis assms(10) assms(11) assms(12) assms(13) assms(14) assms(2) assms(3) assms(4) assms(5)
assms(6) assms(7) assms(8) assms(9) insert_commute)
qed

lemma rk_bcα :
assumes "desargues_config_2D A B C A' B' C' P α β γ" and "rk {A, B, C, A', B', C', P, Q} ≥ 4"
and "rk {Q, A', a} = 2" and "rk {Q, B', b} = 2" and "rk {Q, C', c} = 2" and "rk {P, Q, R} = 2" and
"rk {P, R} = 2" and "rk {Q, R} = 2" and "rk {R, A, a} = 2" and "rk {R, B, b} = 2" and
"rk {R, C, c} = 2" and "rk {A', P} = 2" and "rk {B', P} = 2" and "rk {C', P} = 2"
shows "rk {b, c, α} = 2"
proof-
have "desargues_config_2D B A C B' A' C' P β α γ"
using assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ]
desargues_config_2D_def[of B A C B' A' C' P β α γ]
by (metis insert_commute)
thus "rk {b, c, α} = 2"
using rk_acβ[of B A C B' A' C' P β α γ Q b a c R]
by (metis assms(10) assms(11) assms(12) assms(13) assms(14) assms(2) assms(3) assms(4) assms(5)
assms(6) assms(7) assms(8) assms(9) insert_commute)
qed

lemma rk_abcαβγ :
assumes "desargues_config_2D A B C A' B' C' P α β γ" and "rk {A, B, C, A', B', C', P, Q} ≥ 4"
and "rk {Q, A', a} = 2" and "rk {Q, B', b} = 2" and "rk {Q, C', c} = 2" and "rk {P, Q, R} = 2" and
"rk {P, R} = 2" and "rk {Q, R} = 2" and "rk {R, A, a} = 2" and "rk {R, B, b} = 2" and
"rk {R, C, c} = 2" and "rk {A', P} = 2" and "rk {B', P} = 2" and "rk {C', P} = 2"
shows "rk {a, b, c, α, β, γ} = 3"
proof-
have f1:"rk {a, b, γ} = 2"
using rk_abγ[of A B C A' B' C' P α β γ Q a b c R] assms
by auto
have f2:"rk {a, c, β} = 2"
using rk_acβ[of A B C A' B' C' P α β γ Q a b c R] assms
by auto
have f3:"rk {b, c, α} = 2"
using rk_bcα[of A B C A' B' C' P α β γ Q a b c R] assms
by auto
have "rk {a, b, c, β, γ} + rk {a} ≤ rk {a, b, γ} + rk {a, c, β}"
using matroid_ax_3_alt[of "{a}" "{a, b, γ}" "{a, c, β}"]
then have "rk {a, b, c, β, γ} ≤ 3"
using f1 f2
by (metis Suc_1 Suc_eq_plus1 Suc_le_mono add_Suc_right numeral_3_eq_3 numeral_nat(1) numerals(1)
rk_singleton)
then have f4:"rk {a, b, c, β, γ} = 3"
using matroid_ax_2 rk_abc[of A B C A' B' C' P α β γ Q a b c R]
by (metis Un_upper2 assms(1) assms(10) assms(11) assms(12) assms(13) assms(14) assms(2) assms(3)
assms(4) assms(5) assms(6) assms(7) assms(8) assms(9) insert_mono le_antisym sup_bot.comm_neutral)
have "rk {a, b, c} = 3"
using rk_abc[of A B C A' B' C' P α β γ Q a b c R] assms(1) assms(10) assms(11) assms(12) assms(13)
assms(14) assms(2) assms(3) assms(4) assms(5) assms(6) assms(7) assms(8) assms(9)
by blast
then have f5:"rk {b, c} = 2"
using rk_triple_to_rk_couple rk_couple
by force
have "rk {a, b, c, α, β, γ} + rk {b, c} ≤ rk {a, b, c, β, γ} + rk {b, c, α}"
using matroid_ax_3_alt[of "{b, c}" "{a, b, c, β, γ}" "{b, c, α}"]
then have "rk {a, b, c, α, β, γ} ≤ 3"
using f3 f4 f5
by linarith
thus "rk {a, b, c, α, β, γ} = 3"
using matroid_ax_2
by (metis ‹rk {a, b, c} = 3› empty_subsetI insert_mono le_antisym)
qed

lemma rk_ABCαβγ :
assumes "desargues_config_2D A B C A' B' C' P α β γ" and "rk {A, B, C, A', B', C', P, Q} ≥ 4"
and "rk {Q, A', a} = 2" and "rk {Q, B', b} = 2" and "rk {Q, C', c} = 2" and "rk {P, Q, R} = 2" and
"rk {P, R} = 2" and "rk {Q, R} = 2" and "rk {R, A, a} = 2" and "rk {R, B, b} = 2" and
"rk {R, C, c} = 2" and "rk {A', P} = 2" and "rk {B', P} = 2" and "rk {C', P} = 2"
shows "rk {A, B, C, α, β, γ} = 3"
proof-
have f1:"rk {A, B, γ} = 2"
using assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ]
by auto
have f2:"rk {A, C, β} = 2"
using assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ]
by auto
have f3:"rk {B, C, α} = 2"
using assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ]
by auto
have "rk {A, B, C, β, γ} + rk {A} ≤ rk {A, B, γ} + rk {A, C, β}"
using matroid_ax_3_alt[of "{A}" "{A, B, γ}" "{A, C, β}"]
then have "rk {A, B, C, β, γ} ≤ 3"
using f1 f2
by (metis Suc_1 Suc_eq_plus1 Suc_le_mono add_Suc_right numeral_3_eq_3 numeral_nat(1) numerals(1)
rk_singleton)
have "rk {A, B, C} = 3"
using assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ]
by auto
then have f4:"rk {A, B, C, β, γ} = 3"
using matroid_ax_2
by (metis ‹rk {A, B, C, β, γ} ≤ 3› empty_subsetI insert_mono le_antisym)
have f5:"rk {B, C} = 2"
using ‹rk {A, B, C} = 3› rk_couple rk_triple_to_rk_couple
by force
have "rk {A, B, C, α, β, γ} + rk {B, C} ≤ rk {A, B, C, β, γ} + rk {B, C, α}"
using matroid_ax_3_alt[of "{B, C}" "{A, B, C, β, γ}" "{B, C, α}"]
then have "rk {A, B, C, α, β, γ} ≤ 3"
using f3 f4 f5
by linarith
thus "rk {A, B, C, α, β, γ} = 3"
using matroid_ax_2
by (metis ‹rk {A, B, C} = 3› empty_subsetI insert_mono le_antisym)
qed

lemma rk_αβγ :
assumes "desargues_config_2D A B C A' B' C' P α β γ" and "rk {A, B, C, A', B', C', P, Q} ≥ 4"
and "rk {Q, A', a} = 2" and "rk {Q, B', b} = 2" and "rk {Q, C', c} = 2" and "rk {P, Q, R} = 2" and
"rk {P, R} = 2" and "rk {Q, R} = 2" and "rk {R, A, a} = 2" and "rk {R, B, b} = 2" and
"rk {R, C, c} = 2" and "rk {A', P} = 2" and "rk {B', P} = 2" and "rk {C', P} = 2"
shows "rk {α, β, γ} ≤ 2"
proof-
have "rk {A, B, C, a, b, c} ≥ 4"
using desargues_config_2D_rkABCabc[of A B C A' B' C' P α β γ Q a R b c] assms
by auto
have "{A, B, C, a, b, c} ⊆ {A, B, C, a, b, c, α, β, γ}"
by auto
then have f1:"rk {A, B, C, a, b, c, α, β, γ} ≥ 4"
using matroid_ax_2
by (meson ‹4 ≤ rk {A, B, C, a, b, c}› dual_order.trans)
have "rk {A, B, C, a, b, c, α, β, γ} + rk {α, β, γ} ≤ rk {A, B, C, α, β, γ} + rk {a, b, c, α, β, γ}"
using matroid_ax_3_alt[of "{α, β, γ}" "{A, B, C, α, β, γ}" "{a, b, c, α, β, γ}"]
thus "rk {α, β, γ} ≤ 2"
using f1 rk_ABCαβγ[of A B C A' B' C' P α β γ Q a b c R] rk_abcαβγ[of A B C A' B' C' P α β γ Q a b c R]
assms(12) assms(13) assms(14) assms(2) assms(3) assms(4) assms(5) assms(6) assms(7) assms(8)
rk_triple_le semiring_norm(2) semiring_norm(4))
qed

lemma rk_αβγ_special_case_1 :
assumes "desargues_config_2D A B C A' B' C' P α β γ" and "rk {A', P} = 1"
shows "rk {α, β, γ} ≤ 2"
proof-
have "A' = P"
then have "rk {A', C', C, β} + rk {C', A'} ≤ rk {C, C', P} + rk {A', C', β}"
using matroid_ax_3_alt[of "{C', A'}" "{C, C', P}" "{A', C', β}"]
then have "rk {A', C', C, β} ≤ rk {A', C', β}"
using assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ]
by (metis (full_types) add_le_cancel_right insert_commute rk_triple_to_rk_couple)
then have f5:"rk {A', C', C, β} = 2"
using assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ]
by (metis insert_commute le_antisym matroid_ax_2 subset_insertI)
have "rk {A, A', C, a, C', β} + rk {A, C, β} ≤ rk {A, A', C', C, β} + rk {a, A, C, β}" for a
using matroid_ax_3_alt[of "{A, C, β}" "{A, A', C', C, β}" "{a, A, C, β}"]
then have f6:"rk {A, A', C', C, β} ≥ 3"
using assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ] rk_AA'Ca rk_acACβ
by (metis Un_insert_right Un_upper2 ‹A' = P› insert_commute matroid_ax_2 sup_bot.right_neutral)
have "rk {A, A', C', C, β} + rk {β, C} ≤ rk {A, C, β} + rk {A', C', C, β}"
using matroid_ax_3_alt[of "{β, C}" "{A, C, β}" "{A', C', C, β}"]
then have "rk {β, C} ≤ 1"
using assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ] f5 f6
by linarith
then have "β = C"
using rk_couple
by force
have "rk {A', B', B, γ} + rk {B', A'} ≤ rk {B, B', P} + rk {A', B', γ}"
using matroid_ax_3_alt[of "{B', A'}" "{B, B', P}" "{A', B', γ}"]
by (simp add: ‹A' = P› insert_commute)
then have "rk {A', B', B, γ} ≤ rk {A', B', γ}"
using assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ]
by (metis (full_types) add_le_cancel_right insert_commute rk_triple_to_rk_couple)
then have f7:"rk {A', B', B, γ} = 2"
using assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ]
by (metis insert_commute le_antisym matroid_ax_2 subset_insertI)
have "rk {A, A', B, a, B', γ} + rk {A, B, γ} ≤ rk {A, A', B', B, γ} + rk {a, A, B, γ}" for a
using matroid_ax_3_alt[of "{A, B, γ}" "{A, A', B', B, γ}" "{a, A, B, γ}"]
then have f8:"rk {A, A', B', B, γ} ≥ 3"
using assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ] rk_AA'Ca rk_acACβ
by (metis Un_insert_right Un_upper2 ‹A' = P› insert_commute matroid_ax_2 sup_bot.right_neutral)
have "rk {A, A', B', B, γ} + rk {γ, B} ≤ rk {A, B, γ} + rk {A', B', B, γ}"
using matroid_ax_3_alt[of "{γ, B}" "{A, B, γ}" "{A', B', B, γ}"]
then have "rk {γ, B} ≤ 1"
using assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ] f7 f8
by linarith
then have "γ = B"
using rk_couple
by force
then have "rk {α, β, γ} = rk {α, C, B}"
using ‹β = C ›
by auto
thus "rk {α, β, γ} ≤ 2"
using assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ]
by (metis insert_commute order_refl)
qed

lemma rk_αβγ_special_case_2 :
assumes "desargues_config_2D A B C A' B' C' P α β γ" and "rk {B', P} = 1"
shows "rk {α, β, γ} ≤ 2"
proof-
have "desargues_config_2D B A C B' A' C' P β α γ"
using assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ]
desargues_config_2D_def[of B A C B' A' C' P β α γ]
by (metis insert_commute)
thus "rk {α, β, γ} ≤ 2"
using rk_αβγ_special_case_1[of B A C B' A' C' P β α γ] assms(2)
qed

lemma rk_αβγ_special_case_3 :
assumes "desargues_config_2D A B C A' B' C' P α β γ" and "rk {C', P} = 1"
shows "rk {α, β, γ} ≤ 2"
proof-
have "desargues_config_2D  C B A C' B' A' P γ β α"
using assms(1) desargues_config_2D_def[of A B C A' B' C' P α β γ]
desargues_config_2D_def[of C B A C' B' A' P γ β α]
by (metis insert_commute)
thus "rk {α, β, γ} ≤ 2"
using rk_αβγ_special_case_1[of C B A C' B' A' P γ β α] assms(2)
qed

theorem desargues_2D :
assumes "desargues_config_2D A B C A' B' C' P α β γ"
shows "rk {α, β, γ} ≤ 2"
proof-
have f1:"rk {A, B, C, A', B', C', P} = 3"
using assms desargues_config_2D_def[of A B C A' B' C' P α β γ] coplanar_ABCA'B'C'P
by auto
obtain Q where "rk {A, B, C, A', B', C', P, Q} ≥ 4"
using f1 rk_ext[of "{A, B, C, A', B', C', P}"]
by (metis Un_insert_left add.commute one_plus_numeral order_refl semiring_norm(2) semiring_norm(4)
sup_bot.left_neutral)
obtain R where "rk {P, Q, R} = 2" and "rk {P, R} = 2" and "rk {Q, R} = 2"
using rk_ax_3_pts
by auto
have "rk {Q, A', R, A, P} + rk {P} ≤ rk {P, Q, R} + rk {A, A', P}"
using matroid_ax_3_alt[of "{P}" "{P, Q, R}" "{A, A', P}"]
then have "rk {Q, A', R, A, P} ≤ 3"
using rk_singleton assms desargues_config_2D_def[of A B C A' B' C' P α β γ]
by (metis Suc_1 Suc_eq_plus1 Suc_le_mono ‹rk {P, Q, R} = 2› add_Suc_right eval_nat_numeral(3))
then have f2:"rk {Q, A', R, A} ≤ 3"
using matroid_ax_2
by (metis (no_types, hide_lams) dual_order.trans insert_commute subset_insertI)
obtain a where "rk {Q, A', a} = 2" and "rk {R, A, a} = 2"
using f2 rk_ax_pasch
by blast
have "rk {Q, B', R, B, P} + rk {P} ≤ rk {P, Q, R} + rk {B, B', P}"
using matroid_ax_3_alt[of "{P}" "{P, Q, R}" "{B, B', P}"]
then have "rk {Q, B', R, B, P} ≤ 3"
using rk_singleton assms desargues_config_2D_def[of A B C A' B' C' P α β γ]
by (metis Suc_1 Suc_eq_plus1 Suc_le_mono ‹rk {P, Q, R} = 2› add_Suc_right eval_nat_numeral(3))
then have f3:"rk {Q, B', R, B} ≤ 3"
using matroid_ax_2
by (metis (no_types, hide_lams) dual_order.trans insert_commute subset_insertI)
obtain b where "rk {Q, B', b} = 2" and "rk {R, B, b} = 2"
using f3 rk_ax_pasch
by blast
have "rk {Q, C', R, C, P} + rk {P} ≤ rk {P, Q, R} + rk {C, C', P}"
using matroid_ax_3_alt[of "{P}" "{P, Q, R}" "{C, C', P}"]
then have "rk {Q, C', R, C, P} ≤ 3"
using rk_singleton assms desargues_config_2D_def[of A B C A' B' C' P α β γ]
by (metis Suc_1 Suc_eq_plus1 Suc_le_mono ‹rk {P, Q, R} = 2› add_Suc_right eval_nat_numeral(3))
then have f4:"rk {Q, C', R, C} ≤ 3"
using matroid_ax_2
by (metis (no_types, hide_lams) dual_order.trans insert_commute subset_insertI)
obtain c where "rk {Q, C', c} = 2" and "rk {R, C, c} = 2"
using f4 rk_ax_pasch
by blast
then have "rk {α, β, γ} ≤ 2" if "rk {A', P} = 2" and "rk {B', P} = 2" and "rk {C', P} = 2"
using rk_αβγ[of A B C A' B' C' P α β γ Q a b c R] ‹4 ≤ rk {A, B, C, A', B', C', P, Q}›
‹rk {P, Q, R} = 2› ‹rk {P, R} = 2› ‹rk {Q, A', a} = 2› ‹rk {Q, B', b} = 2› ‹rk {Q, R} = 2›
‹rk {R, A, a} = 2› ‹rk {R, B, b} = 2› assms that(1) that(2) that(3)
by blast
have "rk {α, β, γ} ≤ 2" if "rk {A', P} = 1"
using rk_αβγ_special_case_1 assms that
by auto
have "rk {α, β, γ} ≤ 2" if "rk {B', P} = 1"
using rk_αβγ_special_case_2 assms that
by auto
have "rk {α, β, γ} ≤ 2" if "rk {C', P} = 1"
using rk_αβγ_special_case_3 assms that
by auto
thus "rk {α, β, γ} ≤ 2"
using ‹⟦rk {A', P} = 2; rk {B', P} = 2; rk {C', P} = 2⟧ ⟹ rk {α, β, γ} ≤ 2›
‹rk {A', P} = 1 ⟹ rk {α, β, γ} ≤ 2› ‹rk {B', P} = 1 ⟹ rk {α, β, γ} ≤ 2›
rk_couple rk_singleton_bis
by blast
qed

end


# Theory Desargues_3D

theory Desargues_3D
imports Main Higher_Projective_Space_Rank_Axioms Matroid_Rank_Properties
begin

(* Author: Anthony Bordg, University of Cambridge, apdb3@cam.ac.uk .*)

text ‹
Contents:
▪ We prove Desargues's theorem: if two triangles ABC and A'B'C' are perspective from a point P (ie.
the lines AA', BB' and CC' are concurrent in P), then they are perspective from a line (ie. the points
‹α = BC ∩ B'C'›, ‹β = AC ∩ A'C'› and ‹γ = AB ∩ A'B'› are collinear).
In this file we restrict ourself to the case where the two triangles ABC and A'B'C' are not coplanar.
›

section ‹Desargues's Theorem: The Non-coplanar Case›

definition desargues_config_3D ::
"[Points, Points, Points, Points, Points, Points, Points, Points, Points, Points] => bool"
where "desargues_config_3D A B C A' B' C' P α β γ ≡ rk {A, B, C} = 3 ∧ rk {A', B', C'} = 3 ∧
rk {A, A', P} = 2 ∧ rk {B, B', P} = 2 ∧ rk {C, C', P} = 2 ∧ rk {A, B, C, A', B', C'} ≥ 4 ∧
rk {B, C, α} = 2 ∧ rk {B', C', α} = 2 ∧ rk {A, C, β} = 2 ∧ rk {A', C', β} = 2 ∧ rk {A, B, γ} = 2 ∧
rk {A', B', γ} = 2"

lemma coplanar_4 :
assumes "rk {A, B, C} = 3" and "rk {B, C, α} = 2"
shows "rk {A, B, C, α} = 3"
proof-
have f1:"rk {A, B, C, α} ≥ 3"
using matroid_ax_2
by (metis assms(1) empty_subsetI insert_mono)
have "rk {A, B, C, α} + rk {B, C} ≤ rk {A, B, C} + rk {B, C, α}"
using matroid_ax_3_alt
then have f2:"rk {A, B, C, α} ≤ 3"
by (metis Un_insert_right add_One_commute assms(2) matroid_ax_2_alt numeral_plus_one
semiring_norm(3) sup_bot.right_neutral)
from f1 and f2 show "rk {A, B, C, α} = 3"
by auto
qed

lemma desargues_config_3D_coplanar_4 :
assumes "desargues_config_3D A B C A' B' C' P α β γ"
shows "rk {A, B, C, α} = 3" and "rk {A', B', C', α} = 3"
proof-
show "rk {A, B, C, α} = 3"
using assms desargues_config_3D_def[of A B C A' B' C' P α β γ] coplanar_4
by blast
show "rk {A', B', C', α} = 3"
using assms desargues_config_3D_def[of A B C A' B' C' P α β γ] coplanar_4
by blast
qed

lemma coplanar_4_bis :
assumes "rk {A, B, C} = 3" and "rk {A, C, β} = 2"
shows "rk {A, B, C, β} = 3"
by (smt assms(1) assms(2) coplanar_4 insert_commute)

lemma desargues_config_3D_coplanar_4_bis :
assumes "desargues_config_3D A B C A' B' C' P α β γ"
shows "rk {A, B, C, β} = 3" and "rk {A', B', C', β} = 3"
proof-
show "rk {A, B, C, β} = 3"
using assms desargues_config_3D_def[of A B C A' B' C' P α β γ] coplanar_4_bis
by auto
show "rk {A', B', C', β} = 3"
using assms desargues_config_3D_def[of A B C A' B' C' P α β γ] coplanar_4_bis
by auto
qed

lemma coplanar_4_ter :
assumes "rk {A, B, C} = 3" and "rk {A, B, γ} = 2"
shows "rk {A, B, C, γ} = 3"
by (smt assms(1) assms(2) coplanar_4 insert_commute)

lemma desargues_config_3D_coplanar_4_ter :
assumes "desargues_config_3D A B C A' B' C' P α β γ"
shows "rk {A, B, C, γ} = 3" and "rk {A', B', C', γ} = 3"
proof-
show "rk {A, B, C, γ} = 3"
using assms desargues_config_3D_def[of A B C A' B' C' P α β γ] coplanar_4_ter
by auto
show "rk {A', B', C', γ} = 3"
using assms desargues_config_3D_def[of A B C A' B' C' P α β γ] coplanar_4_ter
by auto
qed

lemma coplanar_5 :
assumes "rk {A, B, C} = 3" and "rk {B, C, α} = 2" and "rk {A, C, β} = 2"
shows "rk {A, B, C, α, β} = 3"
proof-
have f1:"rk {A, B, C, α} = 3"
using coplanar_4
have f2:"rk {A, B, C, β} = 3"
using coplanar_4_bis
from f1 and f2 show "rk {A, B, C, α, β} = 3"
using matroid_ax_3_alt'
by (metis Un_assoc assms(1) insert_is_Un)
qed

lemma desargues_config_3D_coplanar_5 :
assumes "desargues_config_3D A B C A' B' C' P α β γ"
shows "rk {A, B, C, α, β} = 3" and "rk {A', B', C', α, β} = 3"
proof-
show "rk {A, B, C, α, β} = 3"
using assms desargues_config_3D_def coplanar_5
by auto
show "rk {A', B', C', α, β} = 3"
using assms desargues_config_3D_def coplanar_5
by auto
qed

lemma coplanar_5_bis :
assumes "rk {A, B, C} = 3" and "rk {B, C, α} = 2" and "rk {A, B, γ} = 2"
shows "rk {A, B, C, α, γ} = 3"
by (smt assms coplanar_5 insert_commute)

lemma desargues_config_3D_coplanar_5_bis :
assumes "desargues_config_3D A B C A' B' C' P α β γ"
shows "rk {A, B, C, α, γ} = 3" and "rk {A', B', C', α, γ} = 3"
proof-
show "rk {A, B, C, α, γ} = 3"
using assms desargues_config_3D_def[of A B C A' B' C' P α β γ] coplanar_5_bis
by auto
show "rk {A', B', C', α, γ} = 3"
using assms desargues_config_3D_def[of A B C A' B' C' P α β γ] coplanar_5_bis
by auto
qed

lemma coplanar_6 :
assumes "rk {A, B, C} = 3" and "rk {B, C, α} = 2" and "rk {A, B, γ} = 2" and "rk {A, C, β} = 2"
shows "rk {A, B, C, α, β, γ} = 3"
proof-
have f1:"rk {A, B, C, α, γ} = 3"
using coplanar_5_bis assms(1) assms(2) assms(3)
by auto
have f2:"rk {A, B, C, α, β} = 3"
using coplanar_5 assms(1) assms(2) assms(4)
by auto
have f3:"rk {A, B, C, α} = 3"
using coplanar_4 assms(1) assms(2)
by auto
from f1 and f2 and f3 show "rk {A, B, C, α, β, γ} = 3"
using matroid_ax_3_alt'[of "{A, B, C, α}" "β" "γ"]
by (metis Un_insert_left sup_bot.left_neutral)
qed

lemma desargues_config_3D_coplanar_6 :
assumes "desargues_config_3D A B C A' B' C' P α β γ"
shows "rk {A, B, C, α, β, γ} = 3" and "rk {A', B', C', α, β, γ} = 3"
proof-
show "rk {A, B, C, α, β, γ} = 3"
using assms desargues_config_3D_def[of A B C A' B' C' P α β γ] coplanar_6
by auto
show "rk {A', B', C', α, β, γ} = 3"
using assms desargues_config_3D_def[of A B C A' B' C' P α β γ] coplanar_6
by auto
qed

lemma desargues_config_3D_non_coplanar :
assumes "desargues_config_3D A B C A' B' C' P α β γ"
shows "rk {A, B, C, A', B', C', α, β, γ} ≥ 4"
proof-
have "rk {A, B, C, A', B', C'} ≤ rk {A, B, C, A', B', C', α, β, γ}"
using matroid_ax_2
by auto
thus "4 ≤ rk {A, B, C, A', B', C', α, β, γ}"
using matroid_ax_2 assms desargues_config_3D_def[of A B C A' B' C' P α β γ]
by linarith
qed

theorem desargues_3D :
assumes "desargues_config_3D A B C A' B' C' P α β γ"
shows "rk {α, β, γ} ≤ 2"
proof-
have "rk {A, B, C, A', B', C', α, β, γ} + rk {α, β, γ} ≤ rk {A, B, C, α, β, γ} + rk {A', B', C', α, β, γ}"
using matroid_ax_3_alt[of "{α, β, γ}" "{A, B, C, α, β, γ}" "{A', B', C', α, β, γ}"]
then have "rk {α, β, γ} ≤ rk {A, B, C, α, β, γ} + rk {A', B', C', α, β, γ} - rk {A, B, C, A', B', C', α, β, γ}"
by linarith
thus "rk {α, β, γ} ≤ 2"
using assms desargues_config_3D_coplanar_6 desargues_config_3D_non_coplanar
by fastforce
qed

end



# Theory Projective_Space_Axioms

theory Projective_Space_Axioms
imports Main
begin

(* Author: Anthony Bordg, University of Cambridge, apdb3@cam.ac.uk .*)

text ‹
Contents:
▪ We introduce the types of points and lines and an incidence relation between them.
▪ A set of axioms for the (3-dimensional) projective space.
An alternative set of axioms could use planes as basic objects in addition to points and lines
›

section ‹The axioms of the Projective Space›

(* One has a type of points *)
typedecl "points"
(* We don't need an axiom for the existence of at least one point,
since we know that the type "points" is not empty *)

(* One has a type of lines *)
typedecl "lines"
(* idem *)

(* There is a relation of incidence between points and lines *)
consts incid :: "points ⇒ lines ⇒ bool"

axiomatization where
(* The relation of incidence is decidable *)
incid_dec: "(incid P l) ∨ ¬(incid P l)"

axiomatization where
(* Ax1: Any two distinct points are incident with just one line *)
ax1_existence: "∃l. (incid P l) ∧ (incid M l)"
axiomatization where
ax1_uniqueness: "(incid P k) ⟶ (incid M k) ⟶ (incid P l) ⟶ (incid M l) ⟶ (P = M) ∨ (k = l)"

definition distinct4 :: "points ⇒ points ⇒ points ⇒ points ⇒ bool" where
"distinct4 A B C D ≡ (A ≠ B) ∧ (A ≠ C) ∧ (A ≠ D)∧ (B ≠ C) ∧ (B ≠ D) ∧ (C ≠ D)"

(* Ax2: If A B C D are four distinct points such that AB meets CD then AC meets BD.
Sometimes this is called Pasch's axiom, but according to Wikipedia it is misleading
since Pasch's axiom refers to something else. *)
axiomatization where
ax2: "distinct4 A B C D ⟶ (incid A lAB ∧ incid B lAB)
⟶ (incid C lCD ∧ incid D lCD) ⟶ (incid A lAC ∧ incid C lAC) ⟶
(incid B lBD ∧ incid D lBD) ⟶ (∃I.(incid I lAB ∧ incid I lCD)) ⟶
(∃J.(incid J lAC ∧ incid J lBD))"

definition distinct3 :: "points => points => points => bool" where
"distinct3 A B C ≡ (A ≠ B) ∧ (A ≠ C) ∧ (B ≠ C)"

(** Dimension-related axioms **)
(* Ax3: Every line is incident with at least three points.
As I understand it, this axiom makes sure that lines are not degenerated into points
and since it asks for three distinct points, not only 2, it captures the idea that
lines are continuous, i.e. there is always a point between two distinct points. *)
axiomatization where
ax3: "∃A B C. distinct3 A B C ∧ (incid A l) ∧ (incid B l) ∧ (incid C l)"

(* Ax4: There exists two lines that do not meet,
hence the geometry is at least 3-dimensional *)
axiomatization where
ax4: "∃l m.∀P. ¬(incid P l ∧ incid P m)"

definition meet :: "lines ⇒ lines ⇒ bool" where
"meet l m ≡ ∃P. (incid P l ∧ incid P m)"

definition meet_in :: "lines ⇒ lines ⇒ points ⇒ bool" where
"meet_in l m P ≡ incid P l ∧ incid P m"

definition distinct3_line :: "lines ⇒ lines ⇒ lines ⇒ bool" where
"distinct3_line l m n ≡ (l ≠ m) ∧ (l ≠ n) ∧ (m ≠ n)"

(* Ax5: The geometry is not 4-dimensional, hence it is exactly 3-dimensional *)
axiomatization where
ax5: "distinct3_line l1 l2 l3 ⟶ (∃l4 J1 J2 J3. distinct3 J1 J2 J3 ∧
meet_in l1 l4 J1 ∧ meet_in l2 l4 J2 ∧ meet_in l3 l4 J3)"

end

# Theory Higher_Projective_Space_Axioms

theory Higher_Projective_Space_Axioms
imports Main
begin

(* Author: Anthony Bordg, University of Cambridge, apdb3@cam.ac.uk .*)

text ‹
Contents:
▪ We introduce the types of points and lines and an incidence relation between them.
▪ A set of axioms for higher projective spaces, i.e. we allow models of dimension ‹>› 3.
›

section ‹The axioms for Higher Projective Geometry›

(* One has a type of points *)
typedecl "points"

(* One has a type of lines *)
typedecl "lines"

(* One has a relation of incidence between points and lines *)
consts incid :: "points ⇒ lines ⇒ bool"

(* We have the following axioms *)

axiomatization where
(* Ax1: Any two distinct points are incident with just one line *)
ax1_existence: "∃l. (incid P l) ∧ (incid M l)"
axiomatization where
ax1_uniqueness: "(incid P k) ⟶ (incid M k) ⟶ (incid P l) ⟶ (incid M l) ⟶ (P = M) ∨ (k = l)"

definition distinct4 :: "points ⇒ points ⇒ points ⇒ points ⇒ bool" where
"distinct4 A B C D ≡ (A ≠ B) ∧ (A ≠ C) ∧ (A ≠