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 @{term 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›

context projective_plane
begin 

definition inters :: "'line ⇒ 'line ⇒ 'point 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 :: "'line ⇒ 'line ⇒ 'point" 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 :: "['point, 'point, 'point, 'point, 'point, 'point] ⇒ bool" where
"is_pascal A B C D E F ≡ distinct [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 "distinct [A,B,C,D,E,F]"
  shows "distinct [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 "distinct [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 :: "'line ⇒ 'point 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 "distinct [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 "distinct [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 "distinct [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 ‹distinct [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 ‹distinct [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› ‹distinct [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 ‹distinct [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› ‹distinct [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› ‹distinct [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› ‹distinct [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› ‹distinct [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› ‹distinct [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 "distinct [P,Q,R,A,C,W]"
        using assms(1) is_pappus_def is_pappus2_def ‹distinct [P,Q,R,A,C,W]› ‹col P Q R›
          ‹col A C W› inter_is_a_intersec inter_line_line_comm 
        by presburger
      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› ‹distinct [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 "distinct [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 ‹distinct [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 "distinct [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 ‹distinct [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 "distinct [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 "distinct [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› 
            ‹inter (line B C) (line E F) = 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› ‹⟦distinct [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); inter (line B C) (line E F) ≠ inter (line A C) (line E F)⟧ ⟹ col (inter (line A C) (line E F)) (inter (line C D) (line B F)) (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 ‹⟦distinct [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› 
         ‹⟦distinct [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› 
         ‹⟦distinct [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 "distinct [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 = distinct [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

end