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
  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"
  by (simp add: ax1 col_def)

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

lemma col_ABB: "col A B B"
  by (simp add: ax1 col_def)

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
  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"
  by (simp add: inter_def inters_comm)

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"
        by (simp add: col_A_B_ABl W_def)
      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