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
 @{term is_pappus1} @{term is_pappus2}.
▪ We prove the equivalence of these two formulations @{term pappus_equiv}.
▪ We state Pappus property for a plane @{term is_pappus}. 
›

section ‹Pappus's Property›

context projective_plane
begin

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

lemma distinct6_def:
"distinct [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)"
  by auto

definition lines :: "'point ⇒ 'point ⇒ 'line 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 :: "'point ⇒ 'point ⇒ 'line" 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 :: "['point, 'point, 'point, 'point, 'point] ⇒ 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 :: 
"['point, 'point, 'point, 'point, 'point, 'point, 'point, 'point, 'point] => bool " where
"is_pappus1 A B C A' B' C' P Q R ≡ 
  distinct[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 :: "['point, 'point, 'point, 'point, 'point] ⇒ 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 ::
"['point, 'point, 'point, 'point, 'point, 'point, 'point, 'point, 'point] ⇒ bool" where
"is_pappus2 A B C A' B' C' P Q R ≡ 
  (distinct [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 "distinct [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:"distinct [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 "distinct [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'› ‹distinct [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'› ‹distinct [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'› ‹distinct [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 ‹distinct [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 ‹distinct [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 ‹distinct [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'› ‹distinct [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› 
        ‹⟦distinct [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

end