diff --git a/thys/Projective_Geometry/Desargues_2D.thy b/thys/Projective_Geometry/Desargues_2D.thy
--- a/thys/Projective_Geometry/Desargues_2D.thy
+++ b/thys/Projective_Geometry/Desargues_2D.thy
@@ -1,1032 +1,1036 @@
 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 \<open>
 Contents:
 \<^item> 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
 \<open>\<alpha> = BC \<inter> B'C'\<close>, \<open>\<beta> = AC \<inter> A'C'\<close> and \<open>\<gamma> = AB \<inter> A'B'\<close> are collinear).
 In this file we restrict ourself to the case where the two triangles ABC and A'B'C' are coplanar. 
 \<close>
 
 section \<open>Desargues's Theorem: The Coplanar Case\<close>
 
+context higher_projective_space_rank
+begin
+
 definition desargues_config_2D :: 
-  "[Points, Points, Points, Points, Points, Points, Points, Points, Points, Points] \<Rightarrow> bool" 
+  "['point, 'point, 'point, 'point, 'point, 'point, 'point, 'point, 'point, 'point] \<Rightarrow> bool" 
   where "desargues_config_2D A B C A' B' C' P \<alpha> \<beta> \<gamma> \<equiv> rk {A, B, C} = 3 \<and> rk {A', B', C'} = 3 \<and> 
 rk {A, A', P} = 2 \<and> rk {B, B', P} = 2 \<and> rk {C, C', P} = 2 \<and> rk {A, B, \<gamma>} = 2 \<and> rk {A', B', \<gamma>} = 2 \<and>
 rk {A, C, \<beta>} = 2 \<and> rk {A', C', \<beta>} = 2 \<and> rk {B, C, \<alpha>} = 2 \<and> rk {B', C', \<alpha>} = 2 \<and> 
 rk {A, B, C, A', B', C'} = 3 \<and> 
 \<comment> \<open>We add the following non-degeneracy conditions\<close>
 rk {A, B, P} = 3 \<and> rk {A, C, P} = 3 \<and> rk {B, C, P} = 3 \<and> 
 rk {A, A'} = 2 \<and> rk {B, B'} = 2 \<and> 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'} \<le> 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}"]
     by (simp add: insert_commute)
   then have "rk {A, B, C, A', B', C', P} \<le> 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} \<le> 3" 
     using rk_triple_le by auto
   have "rk {A, B, A', B', P} \<ge> 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)
     by (simp add: insert_commute rk_singleton)
   have "rk {A, B, A', B', P} + rk {B', P} \<le> rk {A, A', B', P} + rk {B, B', P}" 
     using matroid_ax_3_alt[of "{B', P}" "{A, A', B', P}" "{B, B', P}"]
     by (simp add: insert_commute)
   then have "rk {A, A', B', P} \<ge> 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} \<le> rk {A', B', P} + rk {A, A', P}" 
     using matroid_ax_3_alt[of "{A', P}" "{A', B', P}" "{A, A', P}"]
     by (simp add: insert_commute)
   then have "rk {A', B', P} \<ge> 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 \<alpha> \<beta> \<gamma>" 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 \<alpha> \<beta> \<gamma>] 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 \<alpha> \<beta> \<gamma>] 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 \<alpha> \<beta> \<gamma>] 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} \<ge> 4"
   shows "rk {A', B', P, Q} = 4"
 proof-
   have "card {A', B', P, Q} \<le> 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} \<le> 4" 
     using matroid_ax_1b dual_order.trans by blast
   have "rk {A, B, C, A', B', C', P, Q} + rk {A', B', P} \<le> 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}"]
     by (simp add: insert_commute)
   then have "rk {A', B', P, Q} \<ge> 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} \<ge> 4" 
     using assms non_colinear_A'B'P coplanar_ABCA'B'C'P
     by (smt diff_add_inverse2 le_trans)
   from f1 and f2 show "rk {A', B', P, Q} = 4"
     by (simp add: f1 eq_iff)
 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 \<alpha> \<beta> \<gamma>" 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} \<ge> 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 \<alpha> \<beta> \<gamma>] 
       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 \<alpha> \<beta> \<gamma>] 
       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 \<alpha> \<beta> \<gamma>] 
       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} \<le> 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} \<le> 4" 
     using dual_order.trans matroid_ax_1b 
     by auto
   have f2:"rk {A', B', P, Q, R} + rk {P, R} \<le> rk {A', B', P, R} + rk {P, Q, R}" 
     using matroid_ax_3_alt[of "{P, R}" "{A', B', P, R}" "{P, Q, R}"]
     by (simp add: insert_commute)
   have f3:"rk {A', B', P, Q, R} \<ge> 4" 
     using matroid_ax_2 assms(3)
     by (metis insert_mono subset_insertI)
   from f2 and f3 have f4:"rk {A', B', P, R} \<ge> 4" 
     using assms(1) assms(2) 
     by linarith
   thus "rk {A', B', P, R} = 4" 
     using f1 f4
     by (simp add: f1 le_antisym)
 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'} \<le> rk {A, B, A'} + rk {A, A', P}" 
     using matroid_ax_3_alt[of "{A, A'}" "{A, B, A'}" "{A, A', P}"]
     by (simp add: insert_commute)
   then have "rk {A, B, A'} \<ge> 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"
     by (simp add: le_antisym rk_triple_le)
 qed
 
 lemma desargues_config_2D_non_collinear :
   assumes "desargues_config_2D A B C A' B' C' P \<alpha> \<beta> \<gamma>"
   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 \<alpha> \<beta> \<gamma>] rk_ABA' 
     by auto
   show "rk {A, B, B'} = 3" 
     using assms desargues_config_2D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>] 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 \<alpha> \<beta> \<gamma>] 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} \<ge> 4" and "rk {A, B, C, A', B', C'} \<le> 3"
   shows "rk {A, a} = 2"
 proof-
   have "rk {Q, A', A, a} + rk {a} \<le> rk {Q, A', a} + rk {A, a}" 
     using matroid_ax_3_alt[of "{a}" "{Q, A', a}" "{A, a}"]
     by (simp add: insert_commute)
   then have "rk {Q, A', A, a} \<le> rk {Q, A', a} + rk {A, a} - rk {a}"
     using add_le_imp_le_diff 
     by blast
   then have "rk {Q, A', A, a} \<le> 2" if "rk {A, a} = 1"
     using assms(4)
     by (simp add: rk_singleton that)
   then have "rk {Q, A', A} \<le> 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 
         numeral_3_eq_3 one_add_one rk_couple rk_triple_le that)
   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} \<le> 3" if "rk {A, a} = 1"
     by (metis One_nat_def Un_insert_right add.right_neutral add_Suc_right insert_commute matroid_ax_2_alt 
         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'} \<le> 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'}"]
     by (simp add: insert_commute)
   then have "rk {A, B, C, A', B', C', P, Q} \<le> 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} \<le> 3" if "rk {A, a} = 1"
     using assms(1) assms(2) assms(3) assms(6) f1 rk_ABA'
     by (smt \<open>rk {A, B, C, A', B', C', P, Q} + rk {A, B, A'} \<le> rk {A, A', B, P, Q} + rk {A, B, C, A', B', C'}\<close> 
         add_diff_cancel_right' add_leD2 le_less_trans not_le 
         ordered_cancel_comm_monoid_diff_class.add_diff_inverse 
         ordered_cancel_comm_monoid_diff_class.le_add_diff that)
   then have "\<not> (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 \<alpha> \<beta> \<gamma>" and "rk {A, B, C, A', B', C', P, Q} \<ge> 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 \<alpha> \<beta> \<gamma>] 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 \<alpha> \<beta> \<gamma>] 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 \<alpha> \<beta> \<gamma>] 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} \<ge> 4"
 proof-
   have "rk {A', B', P, R, a, A, B} \<ge> rk {A', B', P, R}" 
     using matroid_ax_2 
     by auto
   then have f1:"rk {A', B', P, R, a, A, B} \<ge> 4" 
     using rk_A'B'PR assms(3) assms(4) assms(5) 
     by auto
   have f2:"rk {A', B', A, B, P} \<le> 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} \<le> 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}"]
     by (simp add: insert_commute)
   then have "rk {A, B, P, R, a} \<ge> 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} \<ge> 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} \<ge> 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} \<ge> 4"
 proof-
   have "rk {A, B, C, A', B', C'} \<le> 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} \<ge> 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} \<le> rk {A, B, P, a} + rk {R, A, a}"
     using matroid_ax_3_alt[of "{A, a}" "{A, B, P, a}" "{R, A, a}"]
     by (simp add: insert_commute)
   thus "rk {A, B, P, a} \<ge> 4" 
     using f1 f2 assms(10) 
     by (smt add_le_imp_le_diff diff_add_inverse2 order_trans)
 qed
 
 lemma desargues_config_2D_rkABPa_rkABPb_rkABPc :
   assumes "desargues_config_2D A B C A' B' C' P \<alpha> \<beta> \<gamma>" and "rk {A, B, C, A', B', C', P, Q} \<ge> 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} \<ge> 4" and "rk {A, B, P, b} \<ge> 4" and "rk {A, B, P, c} \<ge> 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 \<alpha> \<beta> \<gamma>] 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 \<alpha> \<beta> \<gamma>] 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} \<ge> 4" 
     using f1 f2 assms(1) desargues_config_2D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>] assms(7) assms(2) assms(3) 
       assms(4) assms(8) rk_ABPa 
     by auto
   show "rk {A, B, P, b} \<ge> 4" 
     using f1 f2 assms(1) desargues_config_2D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>] 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} \<ge> 4"
   proof-
     have f3:"rk {A, B, P, R, c} \<ge> 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 \<alpha> \<beta> \<gamma>] 
         f1 assms(3) assms(4) f2
       by auto
     have "{A, B, P, R, c} \<subseteq> {A, B, C, P, R, c}" 
       by auto
     then have f4:"rk {A, B, C, P, R, c} \<ge> 4" 
       using matroid_ax_2 f3
       by (meson dual_order.trans)
     have "rk {A, B, C, P, R, c} + rk {C, c} \<le> 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}"]
       by (simp add: insert_commute)
     then have f5:"rk {A, B, C, P, c} \<ge> 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} \<le> 3" 
       using matroid_ax_2 f1
       by (smt insert_iff subsetI)
     have "rk {A, B, C, P, c} + rk {A, B, P} \<le> 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}"]
       by (simp add: insert_commute)
     then have "rk {A, B, P, c} \<ge> rk {A, B, C, P, c}" 
       using assms(1) desargues_config_2D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>] f6
       by linarith
     thus "rk {A, B, P, c} \<ge> 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} \<ge> 3"
 proof-
   have f1:"rk {A, C, A', P} \<ge> 3" 
     using assms(1) matroid_ax_2
     by (metis insert_commute subset_insertI)
   have "rk {A, C, A', P} + rk {A, A'} \<le> rk {A, A', C} + rk {A, A', P}" 
     using matroid_ax_3_alt[of "{A, A'}" "{A, A', C}" "{A, A', P}"]
     by (simp add: insert_commute)
   thus "rk {A, A', C} \<ge> 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'} \<ge> 3"
   by (smt assms(1) assms(2) assms(3) insert_commute rk_AA'C)
 
 lemma rk_AA'Ca :
   assumes "rk {A, A', C} \<ge> 3" and "rk {A, B, P, a} \<ge> 4" and "rk {A, B, C, A', B', C', P} = 3"
   shows "rk {A, A', C, a} \<ge> 4"
 proof-
   have f1:"rk {A, A', C, a, B, P} \<ge> 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'} \<le> 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} \<le> 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'}"]
     by (simp add: insert_commute)
   then have "rk {A, A', C, a} \<ge> 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} \<ge> 4" 
     using f1 assms(1) f2
     by linarith
 qed
 
 lemma rk_AA'C'a :
   assumes "rk {A, A', C'} \<ge> 3" and "rk {A, B, P, a} \<ge> 4" and "rk {A, B, C, A', B', C', P} = 3"
   shows "rk {A, A', C', a} \<ge> 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} \<ge> 4"
   shows "rk {R, a} = 2"
 proof-
   have "R = a" if "rk {R, a} = 1" 
     using rk_couple_to_singleton 
     by (simp add: that)
   then have "rk {R, Q, A'} = 2" if "rk {R, a} = 1"
     using assms(1) 
     by (simp add: insert_commute that)
   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} \<le> rk {A, A', P} + rk {P, Q, R, A'}"
     using matroid_ax_3_alt[of "{A', P}" "{A, A', P}" "{P, Q, R, A'}"]
     by (simp add: insert_commute)
   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} \<le> 3" if "rk {R, a} = 1" 
     using matroid_ax_2_alt[of "{P, Q, R, A', A}" "B"]
     by (simp add: insert_commute that)
   have f3:"rk {A, B, A', P} \<ge> 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} \<le> 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}"]
     by (simp add: insert_commute)
   then have f4:"rk {P, Q, R, A', A, B, C, B', C'} \<le> 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'} \<ge> 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)
     by (smt Suc_1 Suc_le_eq add_Suc add_Suc_right nat_1_add_1 not_le numeral_2_eq_2 numeral_3_eq_3 
         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 \<alpha> \<beta> \<gamma>" and "rk {A, B, C, A', B', C', P, Q} \<ge> 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 \<alpha> \<beta> \<gamma>] 
     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 \<alpha> \<beta> \<gamma>] 
       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 \<alpha> \<beta> \<gamma>] 
       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 \<alpha> \<beta> \<gamma>]
       assms(2) assms(3) assms(4) assms(7) assms(10)
     by (metis insert_commute)
 qed
 
 lemma rk_acAC\<beta> :
   assumes "rk {R, A, a} = 2" and "rk {R, C, c} = 2" and "rk {A, C} = 2" and "rk {A, C, \<beta>} = 2"
 and "rk {Q, A', a} = 2" and "rk {A, A', C, a} \<ge> 4"
   shows "rk {a, c, A, C, \<beta>} = 3"
 proof-
   have "rk {a, c, A, C, R} + rk {R} \<le> rk {R, A, a} + rk {R, C, c}" 
     using matroid_ax_3_alt[of "{R}" "{R, A, a}" "{R, C, c}"]
     by (simp add: insert_commute)
   then have f1:"rk {a, c, A, C, R} \<le> 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, \<beta>} + rk {A, C} \<le> rk {a, c, A, C, R} + rk {A, C, \<beta>}" 
     using matroid_ax_3_alt[of "{A, C}" "{a, c, A, C, R}" "{A, C, \<beta>}"]
     by (simp add: insert_commute)
   then have f2:"rk {a, c, A, C, R, \<beta>} \<le> 3" 
     using f1 assms(3) assms(4)
     by linarith
   have "{a, c, A, C, \<beta>} \<subseteq> {a, c, A, C, R, \<beta>}" 
     by auto
   then have f3:"rk {a, c, A, C, \<beta>} \<le> 3" 
     using matroid_ax_2 f2
     by (meson order_trans)
   have f4:"rk {A, A', C, a, c, Q} \<ge> 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} \<le> rk {a, c, A, C} + rk {Q, A', a}"
     using matroid_ax_3_alt[of "{a}" "{a, c, A, C}" "{Q, A', a}"]
     by (simp add: insert_commute)
   then have "rk {a, c, A, C} \<ge> 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} \<ge> 3" 
     using f4 assms(5)
     by (smt One_nat_def \<open>rk {A, A', C, a, c, Q} + rk {a} \<le> rk {a, c, A, C} + rk {Q, A', a}\<close> 
         ab_semigroup_add_class.add_ac(1) add_2_eq_Suc' add_diff_cancel_right' add_le_imp_le_diff 
         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, \<beta>} \<ge> 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, \<beta>} = 3" 
     using f3 le_antisym 
     by blast
 qed
 
 lemma rk_acA'C'\<beta> :
   assumes "rk {Q, A', a} = 2" and "rk {Q, C', c} = 2" and "rk {A', C'} = 2" and "rk {A', C', \<beta>} = 2"
 and "rk {R, A, a} = 2" and "rk {A', A, C', a} \<ge> 4"
   shows "rk {a, c, A', C', \<beta>} = 3" 
   using assms rk_acAC\<beta>  
   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} \<le> 4" using assms(2) matroid_ax_2_alt[of "{B, C, P}" "Q"]
     by (simp add: insert_commute)
   have "rk {A, B, C, Q, P} + rk {B, C, P} \<le> 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}"]
     by (simp add: insert_commute)
   then have "rk {P, B, C, Q} \<ge> 4" 
     using assms
     by (smt add.commute dual_order.trans insert_commute matroid_ax_2 nat_add_left_cancel_le 
         subset_insertI)
   thus "rk {P, B, C, Q} = 4"
     by (simp add: \<open>rk {P, B, C, Q} \<le> 4\<close> antisym)
 qed
 
 lemma desargues_config_2D_rkABCP :
   assumes "desargues_config_2D A B C A' B' C' P \<alpha> \<beta> \<gamma>"
   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 \<alpha> \<beta> \<gamma>] 
     by auto
   then have f1:"rk {A, B, C, P} \<ge> 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} \<subseteq> {A, B, C, A', B', C', P}" 
     by auto
   then have "rk {A, B, C, P} \<le> 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 \<alpha> \<beta> \<gamma>" and "rk {A, B, C, A', B', C', P, Q} \<ge> 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} \<ge> 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 \<alpha> \<beta> \<gamma>] 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 \<alpha> \<beta> \<gamma>] 
       assms(2) assms(7) assms(8) 
     by auto
   from f1 and f2 have f3:"rk {A, B, P, a} \<ge> 4" 
     using assms(1) desargues_config_2D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>] assms(2) assms(3) assms(4) 
       assms(5) assms(6) rk_ABPa 
     by auto
   have "{A, B, P, a} \<subseteq> {A, B, C, a, b, c, P}" 
     by auto
   then have f4:"rk {A, B, C, a, b, c, P} \<ge> 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} \<le> 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}"]
     by (simp add: insert_commute)
   thus "rk {A, B, C, a, b, c} \<ge> 4" 
     using f4 assms(1) desargues_config_2D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>] f5
     by linarith
 qed
 
 lemma rk_abc :
   assumes "desargues_config_2D A B C A' B' C' P \<alpha> \<beta> \<gamma>" and "rk {A, B, C, A', B', C', P, Q} \<ge> 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} \<le> 3"
     by (simp add: rk_triple_le)
   have "rk {A, B, C, a, b, c} \<ge> 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} \<ge> 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 \<alpha> \<beta> \<gamma>] 
     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 \<alpha> \<beta> \<gamma>] 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} \<le> 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}"]
     by (simp add: insert_commute)
   then have f5:"rk {a, b, c, R, A, B} \<ge> 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 \<alpha> \<beta> \<gamma>] 
       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} \<le> 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}"]
     by (simp add: insert_commute)
   then have f7:"rk {a, b, c, R, A} \<ge> 4"
     using f5 f6 assms(10) 
     by linarith
   have "rk {a, b, c, R, A} + rk {a} \<le> rk {a, b, c} + rk {R, A, a}"
     using matroid_ax_3_alt[of "{a}" "{a, b, c}" "{R, A, a}"]
     by (simp add: insert_commute)
   then have "rk {a, b, c} \<ge> 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 
         one_add_one rk_ax_singleton semiring_norm(2) semiring_norm(8))
   thus "rk {a, b, c} = 3"
     by (simp add: \<open>rk {a, b, c} \<le> 3\<close> le_antisym)
 qed
 
 lemma rk_ac\<beta> :
   assumes "desargues_config_2D A B C A' B' C' P \<alpha> \<beta> \<gamma>" and "rk {A, B, C, A', B', C', P, Q} \<ge> 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, \<beta>} = 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, \<beta>} \<ge> 2"
     using matroid_ax_2
     by (metis empty_subsetI insert_mono)
   have f1:"rk {a, c, A, C, A', C', \<beta>} + rk {a, c, \<beta>} \<le> rk {a, c, A, C, \<beta>} + rk {a, c, A', C', \<beta>}"
     using matroid_ax_3_alt[of "{a, c, \<beta>}" "{a, c, A, C, \<beta>}" "{a, c, A', C', \<beta>}"]
     by (simp add: insert_commute)
   have f2:"rk {A, A', C} \<ge> 3"
     using rk_AA'C assms(1) desargues_config_2D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>] 
     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 \<alpha> \<beta> \<gamma>] 
     by auto
   then have f4:"rk {A, B, P, a} \<ge> 4" 
     using rk_ABPa assms(1) desargues_config_2D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>]
     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} \<ge> 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, \<beta>} = 3"
     using rk_acAC\<beta>[of R A a C c \<beta> Q A'] assms(1) desargues_config_2D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>]
       assms(9) assms(11) assms(3) rk_triple_to_rk_couple 
     by blast
   have "rk {A', A, C', a} \<ge> 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 \<alpha> \<beta> \<gamma>]
     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', \<beta>} = 3" 
     using rk_acA'C'\<beta>[of Q A' a C' c \<beta> R A] assms(1) desargues_config_2D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>]
       assms(3) assms(5) assms(9)
     by (metis (full_types) insert_commute rk_triple_to_rk_couple)
   have "{A, A', C, a} \<subseteq> {a, c, A, C, A', C', \<beta>}" 
     by auto
   then have f7:"rk {a, c, A, C, A', C', \<beta>} \<ge> 4"
     using matroid_ax_2
     by (meson \<open>4 \<le> rk {A, A', C, a}\<close> dual_order.trans)
   then have "rk {a, c, \<beta>} \<le> 2"
     using f1 f5 f6
     by linarith
   thus "rk {a, c, \<beta>} = 2"
     using \<open>2 \<le> rk {a, c, \<beta>}\<close> le_antisym 
     by blast
 qed
 
 lemma rk_ab\<gamma> :
   assumes "desargues_config_2D A B C A' B' C' P \<alpha> \<beta> \<gamma>" and "rk {A, B, C, A', B', C', P, Q} \<ge> 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, \<gamma>} = 2"
 proof-
   have "desargues_config_2D A C B A' C' B' P \<alpha> \<gamma> \<beta>"
     using assms(1) desargues_config_2D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>] 
       desargues_config_2D_def[of A C B A' C' B' P \<alpha> \<gamma> \<beta>]
     by (metis insert_commute)
   thus "rk {a, b, \<gamma>} = 2" 
     using rk_ac\<beta>[of A C B A' C' B' P \<alpha> \<gamma> \<beta> 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\<alpha> :
   assumes "desargues_config_2D A B C A' B' C' P \<alpha> \<beta> \<gamma>" and "rk {A, B, C, A', B', C', P, Q} \<ge> 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, \<alpha>} = 2"
 proof-
   have "desargues_config_2D B A C B' A' C' P \<beta> \<alpha> \<gamma>"
     using assms(1) desargues_config_2D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>] 
       desargues_config_2D_def[of B A C B' A' C' P \<beta> \<alpha> \<gamma>]
     by (metis insert_commute)
   thus "rk {b, c, \<alpha>} = 2"
     using rk_ac\<beta>[of B A C B' A' C' P \<beta> \<alpha> \<gamma> 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\<alpha>\<beta>\<gamma> :
   assumes "desargues_config_2D A B C A' B' C' P \<alpha> \<beta> \<gamma>" and "rk {A, B, C, A', B', C', P, Q} \<ge> 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, \<alpha>, \<beta>, \<gamma>} = 3"
 proof-
   have f1:"rk {a, b, \<gamma>} = 2" 
     using rk_ab\<gamma>[of A B C A' B' C' P \<alpha> \<beta> \<gamma> Q a b c R] assms 
     by auto
   have f2:"rk {a, c, \<beta>} = 2"
     using rk_ac\<beta>[of A B C A' B' C' P \<alpha> \<beta> \<gamma> Q a b c R] assms 
     by auto
   have f3:"rk {b, c, \<alpha>} = 2"
     using rk_bc\<alpha>[of A B C A' B' C' P \<alpha> \<beta> \<gamma> Q a b c R] assms
     by auto
   have "rk {a, b, c, \<beta>, \<gamma>} + rk {a} \<le> rk {a, b, \<gamma>} + rk {a, c, \<beta>}"
     using matroid_ax_3_alt[of "{a}" "{a, b, \<gamma>}" "{a, c, \<beta>}"]
     by (simp add: insert_commute)
   then have "rk {a, b, c, \<beta>, \<gamma>} \<le> 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, \<beta>, \<gamma>} = 3"
     using matroid_ax_2 rk_abc[of A B C A' B' C' P \<alpha> \<beta> \<gamma> 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 \<alpha> \<beta> \<gamma> 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, \<alpha>, \<beta>, \<gamma>} + rk {b, c} \<le> rk {a, b, c, \<beta>, \<gamma>} + rk {b, c, \<alpha>}"
     using matroid_ax_3_alt[of "{b, c}" "{a, b, c, \<beta>, \<gamma>}" "{b, c, \<alpha>}"]
     by (simp add: insert_commute)
   then have "rk {a, b, c, \<alpha>, \<beta>, \<gamma>} \<le> 3"
     using f3 f4 f5
     by linarith
   thus "rk {a, b, c, \<alpha>, \<beta>, \<gamma>} = 3"
     using matroid_ax_2
     by (metis \<open>rk {a, b, c} = 3\<close> empty_subsetI insert_mono le_antisym)
 qed
 
 lemma rk_ABC\<alpha>\<beta>\<gamma> :
   assumes "desargues_config_2D A B C A' B' C' P \<alpha> \<beta> \<gamma>" and "rk {A, B, C, A', B', C', P, Q} \<ge> 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, \<alpha>, \<beta>, \<gamma>} = 3"
 proof-
 have f1:"rk {A, B, \<gamma>} = 2" 
     using assms(1) desargues_config_2D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>] 
     by auto
   have f2:"rk {A, C, \<beta>} = 2"
     using assms(1) desargues_config_2D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>] 
     by auto
   have f3:"rk {B, C, \<alpha>} = 2"
     using assms(1) desargues_config_2D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>] 
     by auto
   have "rk {A, B, C, \<beta>, \<gamma>} + rk {A} \<le> rk {A, B, \<gamma>} + rk {A, C, \<beta>}"
     using matroid_ax_3_alt[of "{A}" "{A, B, \<gamma>}" "{A, C, \<beta>}"]
     by (simp add: insert_commute)
   then have "rk {A, B, C, \<beta>, \<gamma>} \<le> 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 \<alpha> \<beta> \<gamma>]
     by auto
   then have f4:"rk {A, B, C, \<beta>, \<gamma>} = 3"
     using matroid_ax_2
     by (metis \<open>rk {A, B, C, \<beta>, \<gamma>} \<le> 3\<close> empty_subsetI insert_mono le_antisym)
   have f5:"rk {B, C} = 2"
     using \<open>rk {A, B, C} = 3\<close> rk_couple rk_triple_to_rk_couple 
     by force
   have "rk {A, B, C, \<alpha>, \<beta>, \<gamma>} + rk {B, C} \<le> rk {A, B, C, \<beta>, \<gamma>} + rk {B, C, \<alpha>}"
     using matroid_ax_3_alt[of "{B, C}" "{A, B, C, \<beta>, \<gamma>}" "{B, C, \<alpha>}"]
     by (simp add: insert_commute)
   then have "rk {A, B, C, \<alpha>, \<beta>, \<gamma>} \<le> 3"
     using f3 f4 f5
     by linarith
   thus "rk {A, B, C, \<alpha>, \<beta>, \<gamma>} = 3"
     using matroid_ax_2
     by (metis \<open>rk {A, B, C} = 3\<close> empty_subsetI insert_mono le_antisym)
 qed
 
 lemma rk_\<alpha>\<beta>\<gamma> :
   assumes "desargues_config_2D A B C A' B' C' P \<alpha> \<beta> \<gamma>" and "rk {A, B, C, A', B', C', P, Q} \<ge> 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 {\<alpha>, \<beta>, \<gamma>} \<le> 2"
 proof-
   have "rk {A, B, C, a, b, c} \<ge> 4"
     using desargues_config_2D_rkABCabc[of A B C A' B' C' P \<alpha> \<beta> \<gamma> Q a R b c] assms 
     by auto
   have "{A, B, C, a, b, c} \<subseteq> {A, B, C, a, b, c, \<alpha>, \<beta>, \<gamma>}" 
     by auto
   then have f1:"rk {A, B, C, a, b, c, \<alpha>, \<beta>, \<gamma>} \<ge> 4"
     using matroid_ax_2
     by (meson \<open>4 \<le> rk {A, B, C, a, b, c}\<close> dual_order.trans)
   have "rk {A, B, C, a, b, c, \<alpha>, \<beta>, \<gamma>} + rk {\<alpha>, \<beta>, \<gamma>} \<le> rk {A, B, C, \<alpha>, \<beta>, \<gamma>} + rk {a, b, c, \<alpha>, \<beta>, \<gamma>}"
     using matroid_ax_3_alt[of "{\<alpha>, \<beta>, \<gamma>}" "{A, B, C, \<alpha>, \<beta>, \<gamma>}" "{a, b, c, \<alpha>, \<beta>, \<gamma>}"]
     by (simp add: insert_commute)
   thus "rk {\<alpha>, \<beta>, \<gamma>} \<le> 2"
     using f1 rk_ABC\<alpha>\<beta>\<gamma>[of A B C A' B' C' P \<alpha> \<beta> \<gamma> Q a b c R] rk_abc\<alpha>\<beta>\<gamma>[of A B C A' B' C' P \<alpha> \<beta> \<gamma> Q a b c R]
     by (smt One_nat_def Suc_1 Suc_le_eq add_Suc_right add_le_imp_le_diff 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) diff_add_inverse2 le_antisym nat_1_add_1 not_less numeral_3_eq_3 one_plus_numeral 
         rk_triple_le semiring_norm(2) semiring_norm(4))
 qed
 
 lemma rk_\<alpha>\<beta>\<gamma>_special_case_1 :
   assumes "desargues_config_2D A B C A' B' C' P \<alpha> \<beta> \<gamma>" and "rk {A', P} = 1"
   shows "rk {\<alpha>, \<beta>, \<gamma>} \<le> 2"
 proof-
   have "A' = P"
     by (simp add: assms(2) rk_couple_to_singleton)
   then have "rk {A', C', C, \<beta>} + rk {C', A'} \<le> rk {C, C', P} + rk {A', C', \<beta>}"
     using matroid_ax_3_alt[of "{C', A'}" "{C, C', P}" "{A', C', \<beta>}"]
     by (simp add: insert_commute)
   then have "rk {A', C', C, \<beta>} \<le> rk {A', C', \<beta>}"
     using assms(1) desargues_config_2D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>]
     by (metis (full_types) add_le_cancel_right insert_commute rk_triple_to_rk_couple)
   then have f5:"rk {A', C', C, \<beta>} = 2"
     using assms(1) desargues_config_2D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>]
     by (metis insert_commute le_antisym matroid_ax_2 subset_insertI)
   have "rk {A, A', C, a, C', \<beta>} + rk {A, C, \<beta>} \<le> rk {A, A', C', C, \<beta>} + rk {a, A, C, \<beta>}" for a
     using matroid_ax_3_alt[of "{A, C, \<beta>}" "{A, A', C', C, \<beta>}" "{a, A, C, \<beta>}"]
     by (simp add: insert_commute)
   then have f6:"rk {A, A', C', C, \<beta>} \<ge> 3"
     using assms(1) desargues_config_2D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>] rk_AA'Ca rk_acAC\<beta>
     by (metis Un_insert_right Un_upper2 \<open>A' = P\<close> insert_commute matroid_ax_2 sup_bot.right_neutral)
   have "rk {A, A', C', C, \<beta>} + rk {\<beta>, C} \<le> rk {A, C, \<beta>} + rk {A', C', C, \<beta>}"
     using matroid_ax_3_alt[of "{\<beta>, C}" "{A, C, \<beta>}" "{A', C', C, \<beta>}"]
     by (simp add: insert_commute)
   then have "rk {\<beta>, C} \<le> 1" 
     using assms(1) desargues_config_2D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>] f5 f6
     by linarith
   then have "\<beta> = C"
     using rk_couple 
     by force
   have "rk {A', B', B, \<gamma>} + rk {B', A'} \<le> rk {B, B', P} + rk {A', B', \<gamma>}"
     using matroid_ax_3_alt[of "{B', A'}" "{B, B', P}" "{A', B', \<gamma>}"]
     by (simp add: \<open>A' = P\<close> insert_commute)
   then have "rk {A', B', B, \<gamma>} \<le> rk {A', B', \<gamma>}"
     using assms(1) desargues_config_2D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>]
     by (metis (full_types) add_le_cancel_right insert_commute rk_triple_to_rk_couple)
   then have f7:"rk {A', B', B, \<gamma>} = 2"
     using assms(1) desargues_config_2D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>]
     by (metis insert_commute le_antisym matroid_ax_2 subset_insertI)
   have "rk {A, A', B, a, B', \<gamma>} + rk {A, B, \<gamma>} \<le> rk {A, A', B', B, \<gamma>} + rk {a, A, B, \<gamma>}" for a
     using matroid_ax_3_alt[of "{A, B, \<gamma>}" "{A, A', B', B, \<gamma>}" "{a, A, B, \<gamma>}"]
     by (simp add: insert_commute)
   then have f8:"rk {A, A', B', B, \<gamma>} \<ge> 3"
     using assms(1) desargues_config_2D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>] rk_AA'Ca rk_acAC\<beta>
     by (metis Un_insert_right Un_upper2 \<open>A' = P\<close> insert_commute matroid_ax_2 sup_bot.right_neutral)
   have "rk {A, A', B', B, \<gamma>} + rk {\<gamma>, B} \<le> rk {A, B, \<gamma>} + rk {A', B', B, \<gamma>}"
     using matroid_ax_3_alt[of "{\<gamma>, B}" "{A, B, \<gamma>}" "{A', B', B, \<gamma>}"]
     by (simp add: insert_commute)
   then have "rk {\<gamma>, B} \<le> 1" 
     using assms(1) desargues_config_2D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>] f7 f8
     by linarith
   then have "\<gamma> = B"
     using rk_couple 
     by force
   then have "rk {\<alpha>, \<beta>, \<gamma>} = rk {\<alpha>, C, B}"
     using \<open>\<beta> = C \<close> 
     by auto
   thus "rk {\<alpha>, \<beta>, \<gamma>} \<le> 2" 
     using assms(1) desargues_config_2D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>]
     by (metis insert_commute order_refl)
 qed
 
 lemma rk_\<alpha>\<beta>\<gamma>_special_case_2 :
   assumes "desargues_config_2D A B C A' B' C' P \<alpha> \<beta> \<gamma>" and "rk {B', P} = 1"
   shows "rk {\<alpha>, \<beta>, \<gamma>} \<le> 2"
 proof-
   have "desargues_config_2D B A C B' A' C' P \<beta> \<alpha> \<gamma>"
     using assms(1) desargues_config_2D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>] 
       desargues_config_2D_def[of B A C B' A' C' P \<beta> \<alpha> \<gamma>]
     by (metis insert_commute)
   thus "rk {\<alpha>, \<beta>, \<gamma>} \<le> 2"
     using rk_\<alpha>\<beta>\<gamma>_special_case_1[of B A C B' A' C' P \<beta> \<alpha> \<gamma>] assms(2)
     by (simp add: insert_commute)
 qed
 
 lemma rk_\<alpha>\<beta>\<gamma>_special_case_3 :
   assumes "desargues_config_2D A B C A' B' C' P \<alpha> \<beta> \<gamma>" and "rk {C', P} = 1"
   shows "rk {\<alpha>, \<beta>, \<gamma>} \<le> 2"
 proof-
   have "desargues_config_2D  C B A C' B' A' P \<gamma> \<beta> \<alpha>"
     using assms(1) desargues_config_2D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>] 
       desargues_config_2D_def[of C B A C' B' A' P \<gamma> \<beta> \<alpha>]
     by (metis insert_commute)
   thus "rk {\<alpha>, \<beta>, \<gamma>} \<le> 2"
     using rk_\<alpha>\<beta>\<gamma>_special_case_1[of C B A C' B' A' P \<gamma> \<beta> \<alpha>] assms(2)
     by (simp add: insert_commute)
 qed
 
 theorem desargues_2D :
   assumes "desargues_config_2D A B C A' B' C' P \<alpha> \<beta> \<gamma>"
   shows "rk {\<alpha>, \<beta>, \<gamma>} \<le> 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 \<alpha> \<beta> \<gamma>] coplanar_ABCA'B'C'P
     by auto
   obtain Q where "rk {A, B, C, A', B', C', P, Q} \<ge> 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} \<le> rk {P, Q, R} + rk {A, A', P}"
     using matroid_ax_3_alt[of "{P}" "{P, Q, R}" "{A, A', P}"]
     by (simp add: insert_commute)
   then have "rk {Q, A', R, A, P} \<le> 3"
     using rk_singleton assms desargues_config_2D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>]
     by (metis Suc_1 Suc_eq_plus1 Suc_le_mono \<open>rk {P, Q, R} = 2\<close> add_Suc_right eval_nat_numeral(3))
   then have f2:"rk {Q, A', R, A} \<le> 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} \<le> rk {P, Q, R} + rk {B, B', P}"
     using matroid_ax_3_alt[of "{P}" "{P, Q, R}" "{B, B', P}"]
     by (simp add: insert_commute)
   then have "rk {Q, B', R, B, P} \<le> 3"
     using rk_singleton assms desargues_config_2D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>]
     by (metis Suc_1 Suc_eq_plus1 Suc_le_mono \<open>rk {P, Q, R} = 2\<close> add_Suc_right eval_nat_numeral(3))
   then have f3:"rk {Q, B', R, B} \<le> 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} \<le> rk {P, Q, R} + rk {C, C', P}"
     using matroid_ax_3_alt[of "{P}" "{P, Q, R}" "{C, C', P}"]
     by (simp add: insert_commute)
   then have "rk {Q, C', R, C, P} \<le> 3"
     using rk_singleton assms desargues_config_2D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>]
     by (metis Suc_1 Suc_eq_plus1 Suc_le_mono \<open>rk {P, Q, R} = 2\<close> add_Suc_right eval_nat_numeral(3))
   then have f4:"rk {Q, C', R, C} \<le> 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 {\<alpha>, \<beta>, \<gamma>} \<le> 2" if "rk {A', P} = 2" and "rk {B', P} = 2" and "rk {C', P} = 2"
     using rk_\<alpha>\<beta>\<gamma>[of A B C A' B' C' P \<alpha> \<beta> \<gamma> Q a b c R] \<open>4 \<le> rk {A, B, C, A', B', C', P, Q}\<close> 
       \<open>rk {P, Q, R} = 2\<close> \<open>rk {P, R} = 2\<close> \<open>rk {Q, A', a} = 2\<close> \<open>rk {Q, B', b} = 2\<close> \<open>rk {Q, R} = 2\<close> 
       \<open>rk {R, A, a} = 2\<close> \<open>rk {R, B, b} = 2\<close> assms that(1) that(2) that(3) 
     by blast
   have "rk {\<alpha>, \<beta>, \<gamma>} \<le> 2" if "rk {A', P} = 1"
     using rk_\<alpha>\<beta>\<gamma>_special_case_1 assms that 
     by auto
   have "rk {\<alpha>, \<beta>, \<gamma>} \<le> 2" if "rk {B', P} = 1"
     using rk_\<alpha>\<beta>\<gamma>_special_case_2 assms that
     by auto
   have "rk {\<alpha>, \<beta>, \<gamma>} \<le> 2" if "rk {C', P} = 1"
     using rk_\<alpha>\<beta>\<gamma>_special_case_3 assms that
     by auto
   thus "rk {\<alpha>, \<beta>, \<gamma>} \<le> 2"
     using \<open>\<lbrakk>rk {A', P} = 2; rk {B', P} = 2; rk {C', P} = 2\<rbrakk> \<Longrightarrow> rk {\<alpha>, \<beta>, \<gamma>} \<le> 2\<close> 
       \<open>rk {A', P} = 1 \<Longrightarrow> rk {\<alpha>, \<beta>, \<gamma>} \<le> 2\<close> \<open>rk {B', P} = 1 \<Longrightarrow> rk {\<alpha>, \<beta>, \<gamma>} \<le> 2\<close> 
       rk_couple rk_singleton_bis 
     by blast
 qed
+end
 
 end
diff --git a/thys/Projective_Geometry/Desargues_3D.thy b/thys/Projective_Geometry/Desargues_3D.thy
--- a/thys/Projective_Geometry/Desargues_3D.thy
+++ b/thys/Projective_Geometry/Desargues_3D.thy
@@ -1,199 +1,204 @@
 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 \<open>
 Contents:
 \<^item> 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
 \<open>\<alpha> = BC \<inter> B'C'\<close>, \<open>\<beta> = AC \<inter> A'C'\<close> and \<open>\<gamma> = AB \<inter> A'B'\<close> are collinear).
 In this file we restrict ourself to the case where the two triangles ABC and A'B'C' are not coplanar. 
 \<close>
 
 section \<open>Desargues's Theorem: The Non-coplanar Case\<close>
 
+context higher_projective_space_rank
+begin
+
 definition desargues_config_3D :: 
-  "[Points, Points, Points, Points, Points, Points, Points, Points, Points, Points] => bool" 
+  "['point, 'point, 'point, 'point, 'point, 'point, 'point, 'point, 'point, 'point] => bool" 
   where "desargues_config_3D A B C A' B' C' P \<alpha> \<beta> \<gamma> \<equiv> rk {A, B, C} = 3 \<and> rk {A', B', C'} = 3 \<and> 
 rk {A, A', P} = 2 \<and> rk {B, B', P} = 2 \<and> rk {C, C', P} = 2 \<and> rk {A, B, C, A', B', C'} \<ge> 4 \<and> 
 rk {B, C, \<alpha>} = 2 \<and> rk {B', C', \<alpha>} = 2 \<and> rk {A, C, \<beta>} = 2 \<and> rk {A', C', \<beta>} = 2 \<and> rk {A, B, \<gamma>} = 2 \<and>
 rk {A', B', \<gamma>} = 2"
 
 lemma coplanar_4 :
   assumes "rk {A, B, C} = 3" and "rk {B, C, \<alpha>} = 2" 
   shows "rk {A, B, C, \<alpha>} = 3"
 proof-
   have f1:"rk {A, B, C, \<alpha>} \<ge> 3" 
     using matroid_ax_2
     by (metis assms(1) empty_subsetI insert_mono)
   have "rk {A, B, C, \<alpha>} + rk {B, C} \<le> rk {A, B, C} + rk {B, C, \<alpha>}" 
     using matroid_ax_3_alt
     by (metis Un_insert_right add_One_commute add_mono assms(1) assms(2) matroid_ax_2_alt 
         nat_1_add_1 numeral_plus_one rk_singleton semiring_norm(3) sup_bot.right_neutral)
   then have f2:"rk {A, B, C, \<alpha>} \<le> 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, \<alpha>} = 3" 
     by auto
 qed
 
 lemma desargues_config_3D_coplanar_4 :
   assumes "desargues_config_3D A B C A' B' C' P \<alpha> \<beta> \<gamma>"
   shows "rk {A, B, C, \<alpha>} = 3" and "rk {A', B', C', \<alpha>} = 3"
 proof-
   show "rk {A, B, C, \<alpha>} = 3"
     using assms desargues_config_3D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>] coplanar_4 
     by blast
   show "rk {A', B', C', \<alpha>} = 3"
     using assms desargues_config_3D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>] coplanar_4 
     by blast
 qed
 
 lemma coplanar_4_bis :
   assumes "rk {A, B, C} = 3" and "rk {A, C, \<beta>} = 2"
   shows "rk {A, B, C, \<beta>} = 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 \<alpha> \<beta> \<gamma>"
   shows "rk {A, B, C, \<beta>} = 3" and "rk {A', B', C', \<beta>} = 3"
 proof-
   show "rk {A, B, C, \<beta>} = 3"
     using assms desargues_config_3D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>] coplanar_4_bis 
     by auto
   show "rk {A', B', C', \<beta>} = 3"
     using assms desargues_config_3D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>] coplanar_4_bis 
     by auto
 qed
 
 lemma coplanar_4_ter :
   assumes "rk {A, B, C} = 3" and "rk {A, B, \<gamma>} = 2"
   shows "rk {A, B, C, \<gamma>} = 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 \<alpha> \<beta> \<gamma>"
   shows "rk {A, B, C, \<gamma>} = 3" and "rk {A', B', C', \<gamma>} = 3"
 proof-
   show "rk {A, B, C, \<gamma>} = 3"
     using assms desargues_config_3D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>] coplanar_4_ter 
     by auto
   show "rk {A', B', C', \<gamma>} = 3"
     using assms desargues_config_3D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>] coplanar_4_ter 
     by auto
 qed
 
 lemma coplanar_5 :
   assumes "rk {A, B, C} = 3" and "rk {B, C, \<alpha>} = 2" and "rk {A, C, \<beta>} = 2"
   shows "rk {A, B, C, \<alpha>, \<beta>} = 3"
 proof-
   have f1:"rk {A, B, C, \<alpha>} = 3" 
     using coplanar_4
     by (smt One_nat_def Un_assoc Un_commute add.commute add_Suc_right assms(1) assms(2) insert_is_Un 
         le_antisym matroid_ax_2_alt numeral_2_eq_2 numeral_3_eq_3 one_add_one)
   have f2:"rk {A, B, C, \<beta>} = 3" 
     using coplanar_4_bis
     by (smt One_nat_def Un_assoc Un_commute add.commute add_Suc_right assms(1) assms(3) insert_is_Un 
         le_antisym matroid_ax_2_alt numeral_2_eq_2 numeral_3_eq_3 one_add_one)
   from f1 and f2 show "rk {A, B, C, \<alpha>, \<beta>} = 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 \<alpha> \<beta> \<gamma>"
   shows "rk {A, B, C, \<alpha>, \<beta>} = 3" and "rk {A', B', C', \<alpha>, \<beta>} = 3"
 proof-
   show "rk {A, B, C, \<alpha>, \<beta>} = 3"
     using assms desargues_config_3D_def coplanar_5 
     by auto
   show "rk {A', B', C', \<alpha>, \<beta>} = 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, \<alpha>} = 2" and "rk {A, B, \<gamma>} = 2"
   shows "rk {A, B, C, \<alpha>, \<gamma>} = 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 \<alpha> \<beta> \<gamma>"
   shows "rk {A, B, C, \<alpha>, \<gamma>} = 3" and "rk {A', B', C', \<alpha>, \<gamma>} = 3"
 proof-
   show "rk {A, B, C, \<alpha>, \<gamma>} = 3"
     using assms desargues_config_3D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>] coplanar_5_bis 
     by auto
   show "rk {A', B', C', \<alpha>, \<gamma>} = 3"
     using assms desargues_config_3D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>] coplanar_5_bis 
     by auto
 qed
 
 lemma coplanar_6 :
   assumes "rk {A, B, C} = 3" and "rk {B, C, \<alpha>} = 2" and "rk {A, B, \<gamma>} = 2" and "rk {A, C, \<beta>} = 2"
   shows "rk {A, B, C, \<alpha>, \<beta>, \<gamma>} = 3"
 proof-
   have f1:"rk {A, B, C, \<alpha>, \<gamma>} = 3" 
     using coplanar_5_bis assms(1) assms(2) assms(3) 
     by auto
   have f2:"rk {A, B, C, \<alpha>, \<beta>} = 3"
     using coplanar_5 assms(1) assms(2) assms(4) 
     by auto
   have f3:"rk {A, B, C, \<alpha>} = 3" 
     using coplanar_4 assms(1) assms(2) 
     by auto
   from f1 and f2 and f3 show "rk {A, B, C, \<alpha>, \<beta>, \<gamma>} = 3" 
     using matroid_ax_3_alt'[of "{A, B, C, \<alpha>}" "\<beta>" "\<gamma>"]
     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 \<alpha> \<beta> \<gamma>"
   shows "rk {A, B, C, \<alpha>, \<beta>, \<gamma>} = 3" and "rk {A', B', C', \<alpha>, \<beta>, \<gamma>} = 3"
 proof-
   show "rk {A, B, C, \<alpha>, \<beta>, \<gamma>} = 3"
     using assms desargues_config_3D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>] coplanar_6 
     by auto
   show "rk {A', B', C', \<alpha>, \<beta>, \<gamma>} = 3"
     using assms desargues_config_3D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>] coplanar_6 
     by auto
 qed
 
 lemma desargues_config_3D_non_coplanar :
   assumes "desargues_config_3D A B C A' B' C' P \<alpha> \<beta> \<gamma>"
   shows "rk {A, B, C, A', B', C', \<alpha>, \<beta>, \<gamma>} \<ge> 4" 
 proof-
   have "rk {A, B, C, A', B', C'} \<le> rk {A, B, C, A', B', C', \<alpha>, \<beta>, \<gamma>}" 
     using matroid_ax_2 
     by auto
   thus "4 \<le> rk {A, B, C, A', B', C', \<alpha>, \<beta>, \<gamma>}" 
     using matroid_ax_2 assms desargues_config_3D_def[of A B C A' B' C' P \<alpha> \<beta> \<gamma>] 
     by linarith
 qed
 
 theorem desargues_3D :
   assumes "desargues_config_3D A B C A' B' C' P \<alpha> \<beta> \<gamma>"
   shows "rk {\<alpha>, \<beta>, \<gamma>} \<le> 2"
 proof-
   have "rk {A, B, C, A', B', C', \<alpha>, \<beta>, \<gamma>} + rk {\<alpha>, \<beta>, \<gamma>} \<le> rk {A, B, C, \<alpha>, \<beta>, \<gamma>} + rk {A', B', C', \<alpha>, \<beta>, \<gamma>}"
     using matroid_ax_3_alt[of "{\<alpha>, \<beta>, \<gamma>}" "{A, B, C, \<alpha>, \<beta>, \<gamma>}" "{A', B', C', \<alpha>, \<beta>, \<gamma>}"]
     by (simp add: insert_commute)
   then have "rk {\<alpha>, \<beta>, \<gamma>} \<le> rk {A, B, C, \<alpha>, \<beta>, \<gamma>} + rk {A', B', C', \<alpha>, \<beta>, \<gamma>} - rk {A, B, C, A', B', C', \<alpha>, \<beta>, \<gamma>}"
     by linarith
   thus "rk {\<alpha>, \<beta>, \<gamma>} \<le> 2" 
     using assms desargues_config_3D_coplanar_6 desargues_config_3D_non_coplanar
     by fastforce
 qed
 
 end
 
+end
 
 
 
 
 
 
 
+
diff --git a/thys/Projective_Geometry/Desargues_Property.thy b/thys/Projective_Geometry/Desargues_Property.thy
--- a/thys/Projective_Geometry/Desargues_Property.thy
+++ b/thys/Projective_Geometry/Desargues_Property.thy
@@ -1,156 +1,163 @@
 theory Desargues_Property
   imports Main Projective_Plane_Axioms Pappus_Property Pascal_Property
 begin
 
 (* Author: Anthony Bordg, University of Cambridge, apdb3@cam.ac.uk .*)
 
 text \<open>
 Contents:
-\<^item> We formalize Desargues's property, [\<open>desargues_prop\<close>], that states that if two triangles are perspective 
+\<^item> We formalize Desargues's property, @{term "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. 
 \<close>
 
 section \<open>Desargues's Property\<close>
 
-definition distinct3 :: "[Points, Points, Points] \<Rightarrow> bool" where
-"distinct3 A B C \<equiv> A \<noteq> B \<and> A \<noteq> C \<and> B \<noteq> C"
+context projective_plane
+begin
 
-definition triangle :: "[Points, Points, Points] \<Rightarrow> bool" where
-"triangle A B C \<equiv> distinct3 A B C \<and> (line A B \<noteq> line A C)"
+lemma distinct3_def:
+  "distinct [A, B, C] = (A \<noteq> B \<and> A \<noteq> C \<and> B \<noteq> C)"
+  by auto
 
-definition meet_in :: "Lines \<Rightarrow> Lines => Points => bool " where
+definition triangle :: "['point, 'point, 'point] \<Rightarrow> bool" where
+"triangle A B C \<equiv> distinct [A,B,C] \<and> (line A B \<noteq> line A C)"
+
+definition meet_in :: "'line \<Rightarrow> 'line => 'point => bool " where
 "meet_in l m P \<equiv> incid P l \<and> 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] \<Rightarrow> bool" where
+definition meet_3_in :: "['line, 'line, 'line, 'point] \<Rightarrow> bool" where
 "meet_3_in l m n P \<equiv> meet_in l m P \<and> 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] \<Rightarrow> bool" where
-"distinct7 A B C D E F G \<equiv> (A \<noteq> B) \<and> (A \<noteq> C) \<and> (A \<noteq> D) \<and> (A \<noteq> E) \<and> (A \<noteq> F) \<and> (A \<noteq> G) \<and>
+lemma distinct7_def: "distinct [A,B,C,D,E,F,G] = ((A \<noteq> B) \<and> (A \<noteq> C) \<and> (A \<noteq> D) \<and> (A \<noteq> E) \<and> (A \<noteq> F) \<and> (A \<noteq> G) \<and>
 (B \<noteq> C) \<and> (B \<noteq> D) \<and> (B \<noteq> E) \<and> (B \<noteq> F) \<and> (B \<noteq> G) \<and>
 (C \<noteq> D) \<and> (C \<noteq> E) \<and> (C \<noteq> F) \<and> (C \<noteq> G) \<and>
 (D \<noteq> E) \<and> (D \<noteq> F) \<and> (D \<noteq> G) \<and>
 (E \<noteq> F) \<and> (E \<noteq> G) \<and>
-(F \<noteq> G)"
+(F \<noteq> G))"
+  by auto
 
-definition distinct3l :: "[Lines, Lines, Lines] \<Rightarrow> bool" where
-"distinct3l l m n \<equiv> l \<noteq> m \<and> l \<noteq> n \<and> m \<noteq> 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 \<equiv> distinct7 A B C A' B' C' R \<and> \<not> col A B C 
-\<and> \<not> col A' B' C' \<and> distinct3l (line A A') (line B B') (line C C') \<and> 
+  "['point, 'point, 'point, 'point, 'point, 'point, 'point, 'point, 'point, 'point] => bool" where
+"desargues_config A B C A' B' C' M N P R \<equiv> distinct [A,B,C,A',B',C',R] \<and> \<not> col A B C 
+\<and> \<not> col A' B' C' \<and> distinct [(line A A'),(line B B'),(line C C')] \<and> 
 meet_3_in (line A A') (line B B') (line C C') R \<and> (line A B) \<noteq> (line A' B') \<and> 
 (line B C) \<noteq> (line B' C') \<and> (line A C) \<noteq> (line A' C') \<and> meet_in (line B C) (line B' C') M \<and>
 meet_in (line A C) (line A' C') N \<and> 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"
+  assumes "distinct [A,B,C,D,E,F,G]"
+  shows "distinct [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 
+  by (smt assms col_rot_CW desargues_config_def distinct3_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"
   by (simp add: assms desargues_config_rot_CW)
 
 (* 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] \<Rightarrow> bool" where
-"are_perspective_from_point A B C A' B' C' R \<equiv> distinct7 A B C A' B' C' R \<and> triangle A B C \<and>
-triangle A' B' C' \<and> distinct3l (line A A') (line B B') (line C C') \<and> 
+  "['point, 'point, 'point, 'point, 'point, 'point, 'point] \<Rightarrow> bool" where
+"are_perspective_from_point A B C A' B' C' R \<equiv> distinct [A,B,C,A',B',C',R] \<and> triangle A B C \<and>
+triangle A' B' C' \<and> distinct [(line A A'),(line B B'),(line C C')] \<and> 
 meet_3_in (line A A') (line B B') (line C C') R"
 
 definition are_perspective_from_line ::
-  "[Points, Points, Points, Points, Points, Points] \<Rightarrow> bool" where
-"are_perspective_from_line A B C A' B' C' \<equiv> distinct6 A B C A' B' C' \<longrightarrow> triangle A B C \<longrightarrow>
+  "['point, 'point, 'point, 'point, 'point, 'point] \<Rightarrow> bool" where
+"are_perspective_from_line A B C A' B' C' \<equiv> distinct [A,B,C,A',B',C'] \<longrightarrow> triangle A B C \<longrightarrow>
 triangle A' B' C' \<longrightarrow> line A B \<noteq> line A' B' \<longrightarrow> line A C \<noteq> line A' C' \<longrightarrow> line B C \<noteq> line B' C' \<longrightarrow>
 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 \<noteq> 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 \<noteq> line A' B'" and 
     "line A C \<noteq> line A' C'" and "line B C \<noteq> 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)
+  unfolding desargues_config_def distinct7_def distinct3_def
+
+  using assms are_perspective_from_point_def  apply auto
+      apply (smt (z3) ax_uniqueness col_2cycle col_line_ext_1 incidB_lAB line_ext_def mem_Collect_eq triangle_def)
+  apply (smt (z3) ax_uniqueness col_def incidA_lAB line_comm triangle_def)
+  using meet_in_inter apply presburger+
+  done
 
 (* Now, we state Desargues's property in a textbook-like form *)
 definition desargues_prop :: "bool" where
 "desargues_prop \<equiv> 
 \<forall>A B C A' B' C' P. 
   are_perspective_from_point A B C A' B' C' P \<longrightarrow> are_perspective_from_line A B C A' B' C'"
 
 end
 
+end
 
 
 
 
 
+
diff --git a/thys/Projective_Geometry/Higher_Projective_Space_Axioms.thy b/thys/Projective_Geometry/Higher_Projective_Space_Axioms.thy
--- a/thys/Projective_Geometry/Higher_Projective_Space_Axioms.thy
+++ b/thys/Projective_Geometry/Higher_Projective_Space_Axioms.thy
@@ -1,60 +1,57 @@
 theory Higher_Projective_Space_Axioms
   imports Main
 begin
 
 (* Author: Anthony Bordg, University of Cambridge, apdb3@cam.ac.uk .*)
 
 text \<open>
 Contents:
-\<^item> We introduce the types of points and lines and an incidence relation between them.
+\<^item> We introduce the types of 'point and 'line and an incidence relation between them.
 \<^item> A set of axioms for higher projective spaces, i.e. we allow models of dimension \<open>>\<close> 3. 
 \<close>
 
 section \<open>The axioms for Higher Projective Geometry\<close>
 
-(* One has a type of points *)
-typedecl "points"
+lemma distinct4_def:
+  "distinct [A,B,C,D] = ((A \<noteq> B) \<and> (A \<noteq> C) \<and> (A \<noteq> D) \<and> (B \<noteq> C) \<and> (B \<noteq> D) \<and> (C \<noteq> D))"
+  by auto
 
-(* One has a type of lines *)
-typedecl "lines"
+lemma distinct3_def:
+  "distinct [A,B,C] = ((A \<noteq> B) \<and> (A \<noteq> C) \<and> (B \<noteq> C))"
+  by auto
 
-(* One has a relation of incidence between points and lines *)
-consts incid :: "points \<Rightarrow> lines \<Rightarrow> bool"
+locale higher_projective_space =
+(* One has a type of 'point *)
+(* One has a type of 'line *)
+(* One has a relation of incidence between 'point and 'line *)
+  fixes incid :: "'point \<Rightarrow> 'line \<Rightarrow> bool"
 
 (* We have the following axioms *)
 
-axiomatization where
-(* Ax1: Any two distinct points are incident with just one line *)
-ax1_existence: "\<exists>l. (incid P l) \<and> (incid M l)"
-axiomatization where
-ax1_uniqueness: "(incid P k) \<longrightarrow> (incid M k) \<longrightarrow> (incid P l) \<longrightarrow> (incid M l) \<longrightarrow> (P = M) \<or> (k = l)"
+(* Ax1: Any two distinct 'point are incident with just one line *)
+  assumes ax1_existence: "\<exists>l. (incid P l) \<and> (incid M l)"
+  assumes ax1_uniqueness: "(incid P k) \<longrightarrow> (incid M k) \<longrightarrow> (incid P l) \<longrightarrow> (incid M l) \<longrightarrow> (P = M) \<or> (k = l)"
 
-definition distinct4 :: "points \<Rightarrow> points \<Rightarrow> points \<Rightarrow> points \<Rightarrow> bool" where
-"distinct4 A B C D \<equiv> (A \<noteq> B) \<and> (A \<noteq> C) \<and> (A \<noteq> D) \<and> (B \<noteq> C) \<and> (B \<noteq> D) \<and> (C \<noteq> D)"
 
-(* Ax2: If A B C D are four distinct points such that AB meets CD, then AC meets BD.
+(* Ax2: If A B C D are four distinct 'point 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 \<longrightarrow> (incid A lAB \<and> incid B lAB) 
+assumes ax2: "distinct [A,B,C,D] \<longrightarrow> (incid A lAB \<and> incid B lAB) 
 \<longrightarrow> (incid C lCD \<and> incid D lCD) \<longrightarrow> (incid A lAC \<and> incid C lAC) \<longrightarrow> 
 (incid B lBD \<and> incid D lBD) \<longrightarrow> (\<exists>I.(incid I lAB \<and> incid I lCD)) \<longrightarrow> 
 (\<exists>J.(incid J lAC \<and> incid J lBD))"
 
-definition distinct3 :: "points => points => points => bool" where
-"distinct3 A B C \<equiv> (A \<noteq> B) \<and> (A \<noteq> C) \<and> (B \<noteq> 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 have unlimited extent, i.e. there is always a point between two distinct points. *)
-axiomatization where
-ax3: "\<exists>A B C. distinct3 A B C \<and> (incid A l) \<and> (incid B l) \<and> (incid C l)"
+(* Ax3: Every line is incident with at least three 'point.
+As I understand it, this axiom makes sure that 'line are not degenerated into 'point
+and since it asks for three distinct 'point, not only 2, it captures the idea that
+'line have unlimited extent, i.e. there is always a point between two distinct 'point. *)
+assumes ax3: "\<exists>A B C. distinct [A,B,C] \<and> (incid A l) \<and> (incid B l) \<and> (incid C l)"
 
-(* Ax4: There exists two lines that do not meet, hence the geometry is at least 3-dimensional *)
-axiomatization where
-ax4: "\<exists>l m.\<forall>P. \<not>(incid P l \<and> incid P m)"
+(* Ax4: There exists two 'line that do not meet, hence the geometry is at least 3-dimensional *)
+assumes ax4: "\<exists>l m.\<forall>P. \<not>(incid P l \<and> incid P m)"
 
 
 end
diff --git a/thys/Projective_Geometry/Higher_Projective_Space_Rank_Axioms.thy b/thys/Projective_Geometry/Higher_Projective_Space_Rank_Axioms.thy
--- a/thys/Projective_Geometry/Higher_Projective_Space_Rank_Axioms.thy
+++ b/thys/Projective_Geometry/Higher_Projective_Space_Rank_Axioms.thy
@@ -1,45 +1,46 @@
 theory Higher_Projective_Space_Rank_Axioms
   imports Main
 begin
 
 (* Author: Anthony Bordg, University of Cambridge, apdb3@cam.ac.uk .*)
 
 text \<open>
 Contents:
 \<^item> Following @{cite Magaud_2012} we introduce a set of axioms for projective space geometry based on
 the notions of matroid and rank.
 \<close>
 
 section \<open>A Based-rank Set of Axioms for Projective Space Geometry\<close>
 
 (* We have a type of points *)
-typedecl "Points"
+locale higher_projective_space_rank =
 
 (* We have a rank function "rk" on the sets of points *)
-consts rk :: "Points set \<Rightarrow> nat"
+fixes rk :: "'point set \<Rightarrow> nat"
+
 
 (* The function rk satisfies the following axioms *)
-axiomatization where
+assumes
 matroid_ax_1a: "rk X \<ge> 0" (* Useless if rk is defined with values in \<nat>, not \<int> *) and
 matroid_ax_1b: "rk X \<le> card X" and
 matroid_ax_2: "X \<subseteq> Y \<longrightarrow> rk X \<le> rk Y" and
 matroid_ax_3: "rk (X \<union> Y) + rk (X \<inter> Y) \<le> rk X + rk Y"
 
 (* To capture higher projective geometry, we need to introduce the following additional axioms *)
-axiomatization where
+assumes
 rk_ax_singleton: "rk {P} \<ge> 1" and
 rk_ax_couple: "P \<noteq> Q \<longrightarrow> rk {P,Q} \<ge> 2" and
 rk_ax_pasch: "rk {A,B,C,D} \<le> 3 \<longrightarrow> (\<exists>J. rk {A,B,J} = 2 \<and> rk {C,D,J} = 2)" and
 rk_ax_3_pts: "\<exists>C. rk {A,B,C} = 2 \<and> rk {B,C} = 2 \<and> rk {A,C} = 2" and
 rk_ax_dim: "\<exists>A B C D. rk {A,B,C,D} \<ge> 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
 
 
 
 
 
diff --git a/thys/Projective_Geometry/Matroid_Rank_Properties.thy b/thys/Projective_Geometry/Matroid_Rank_Properties.thy
--- a/thys/Projective_Geometry/Matroid_Rank_Properties.thy
+++ b/thys/Projective_Geometry/Matroid_Rank_Properties.thy
@@ -1,248 +1,249 @@
 theory Matroid_Rank_Properties
   imports Main Higher_Projective_Space_Rank_Axioms
 begin
 
 (* Author: Anthony Bordg, University of Cambridge, apdb3@cam.ac.uk .*)
 
 text \<open>
 Contents:
 \<^item> 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.
 \<close>
 
 section \<open>Proof Techniques Using Ranks\<close>
 
+context higher_projective_space_rank
+begin
+
 lemma matroid_ax_3_alt:
   assumes "I \<subseteq> X \<inter> Y"
   shows "rk (X \<union> Y) + rk I \<le> rk X + rk Y"
   by (metis add.commute add_le_cancel_right assms matroid_ax_2 matroid_ax_3 order_trans)
 
 lemma rk_uniqueness:
   assumes "rk {A,B} = 2" and "rk {C,D} = 2" and "rk {A,B,M} \<le> 2" and "rk {C,D,M} \<le> 2" and
   "rk {A,B,P} \<le> 2" and "rk {C,D,P} \<le> 2" and "rk {A,B,C,D} \<ge> 3"
   shows "rk {M,P} = 1"
 proof-
   have "{A,B,M} \<union> {A,B,P} = {A,B,M,P}"
     by auto
   have "rk {A,B,M,P} + rk {A,B} \<le> rk {A,B,M} + rk {A,B,P}"
     by (metis (full_types) \<open>{A, B, M} \<union> {A, B, P} = {A, B, M, P}\<close> 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 \<open>{A, B, M} \<union> {A, B, P} = {A, B, M, P}\<close> add_diff_cancel_left' 
-        add_diff_cancel_right' add_mono antisym assms(1) assms(3) assms(5) le_diff_conv matroid_ax_2)
+    by (metis add_diff_cancel_right' antisym assms(1) assms(3) assms(5) insert_commute le_diff_conv matroid_ax_2 subset_insertI)
   have "{C,D,M} \<union> {C,D,P} = {C,D,M,P}"
     by auto
   have "rk {C,D,M,P} + rk {C,D} \<le> rk {C,D,M} + rk {C,D,P}"
     by (metis Un_insert_left Un_upper1 \<open>{C, D, M} \<union> {C, D, P} = {C, D, M, P}\<close> insert_is_Un le_inf_iff 
         matroid_ax_3_alt)
   then have i1:"rk {C,D,M,P} + 2 \<le> 4"
     using assms(2) assms(4) assms(6) 
     by linarith
   moreover have i2:"rk {C,D,M,P} \<ge> 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} \<ge> 3"
     by (metis Un_insert_right Un_upper2 assms(7) matroid_ax_2 order_trans sup_bot.right_neutral)
   have "{A,B,M,P} \<union> {C,D,M,P} = {A,B,C,D,M,P}"
     by auto 
   then have "rk {A,B,C,D,M,P} + rk {M,P} \<le> 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} \<le> 4"
     using \<open>rk {A, B, M, P} = 2\<close> \<open>rk {C, D, M, P} = 2\<close> 
     by linarith
   have i4:"rk {A,B,C,D,M,P} + rk {M,P} \<ge> 3 + rk{M,P}"
     by (simp add: \<open>3 \<le> rk {A, B, C, D, M, P}\<close>)
   from i3 and i4 show "rk {M,P} = 1"
     by (metis (no_types, lifting) \<open>rk {A, B, C, D, M, P} + rk {M, P} \<le> rk {A, B, M, P} + rk {C, D, M, P}\<close> 
         \<open>rk {A, B, M, P} = 2\<close> \<open>rk {C, D, M, P} = 2\<close> 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: "\<exists>A B C D. \<forall>M. rk {A,B,M} \<noteq> 2 \<or> rk {C,D,M} \<noteq> 2"
 proof-
   obtain A B C D where f1:"rk {A,B,C,D} \<ge> 4"
     using rk_ax_dim 
     by auto
   have "\<forall>M. rk {A,B,M} \<noteq> 2 \<or> rk {C,D,M} \<noteq> 2"
   proof
     fix M
     have "{A,B,C,D,M} = {A,B,M} \<union> {C,D,M}"
       by auto
     then have "rk {A,B,C,D,M} + rk {M} \<le> 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} \<le> 3" if "rk {A,B,M} = 2" and "rk {C,D,M} = 2"
-      by (smt One_nat_def Suc_leI Suc_le_mono Suc_numeral add_Suc_right add_leD1 add_mono le_antisym 
-          not_le numeral_3_eq_3 numeral_One numeral_plus_one one_add_one rk_ax_singleton that(1) 
-          that(2))
+      by (smt (z3) One_nat_def Suc_le_eq Suc_numeral add_Suc_right add_le_same_cancel1 nat_1_add_1 not_less numeral_Bit1 numerals(1) order_trans rk_ax_singleton semiring_norm(2) that(1) that(2))
     then have "rk {A,B,C,D} \<le> 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} \<noteq> 2 \<or> rk {C, D, M} \<noteq> 2 "
       using \<open>4 \<le> rk {A, B, C, D}\<close> 
       by linarith
   qed
   thus "\<exists>A B C D. \<forall>M. rk {A, B, M} \<noteq> 2 \<or> rk {C, D, M} \<noteq> 2"
     by blast
 qed
 
 lemma rk_empty: "rk {} = 0"
 proof-
   have "rk {} \<ge> 0" 
     by simp
   have "rk {} \<le> 0"
     by (metis card.empty matroid_ax_1b)
   thus "rk {} = 0" 
     by blast
 qed
 
 lemma matroid_ax_2_alt: "rk X \<le> rk (X \<union> {x}) \<and> rk (X \<union> {x}) \<le> rk X + 1"
 proof
   have "X \<subseteq> X \<union> {x}" 
     by auto
   thus "rk X \<le> rk (X \<union> {x})"
     by (simp add: matroid_ax_2)
   have "rk {x} \<le> 1"
     by (metis One_nat_def card.empty card_Suc_eq insert_absorb insert_not_empty matroid_ax_1b)
   thus "rk (X \<union> {x}) \<le> rk X + 1"
     by (metis add_leD1 le_antisym matroid_ax_3 rk_ax_singleton)
 qed
 
 lemma matroid_ax_3_alt': "rk (X \<union> {y}) = rk (X \<union> {z}) \<longrightarrow> rk (X \<union> {z}) = rk X \<longrightarrow> rk X = rk (X \<union> {y,z})"
 proof-
   have i1:"rk X \<le> rk (X \<union> {y,z})"
     using matroid_ax_2 
     by blast
   have i2:"rk X \<ge> rk (X \<union> {y,z})" if "rk (X \<union> {y}) = rk (X \<union> {z})" and "rk (X \<union> {z}) = rk X"
   proof-
     have "(X \<union> {y}) \<union> (X \<union> {z}) = X \<union> {y,z}" 
       by blast
     then have "rk (X \<union> {y,z}) + rk X \<le> rk X + rk X"
       by (metis \<open>rk (X \<union> {y}) = rk (X \<union> {z})\<close> \<open>rk (X \<union> {z}) = rk X\<close> inf_sup_ord(3) le_inf_iff 
           matroid_ax_3_alt)
     thus "rk (X \<union> {y,z}) \<le> rk X" 
       by simp
   qed
   thus "rk (X \<union> {y}) = rk (X \<union> {z}) \<longrightarrow> rk (X \<union> {z}) = rk X \<longrightarrow> rk X = rk (X \<union> {y, z})"
     using antisym i1 
     by blast
 qed
 
 lemma rk_ext:
   assumes "rk X \<le> 3"
   shows "\<exists>P. rk(X \<union> {P}) = rk X + 1"
 proof-
   obtain A B C D where "rk {A,B,C,D} \<ge> 4"
     using rk_ax_dim 
     by auto
   have f1:"rk (X \<union> {A, B, C, D}) \<ge> 4"
     by (metis Un_upper2 \<open>4 \<le> rk {A, B, C, D}\<close> matroid_ax_2 sup.coboundedI2 sup.orderE)
   have "rk (X \<union> {A, B, C, D}) = rk X" if "rk(X \<union> {A}) = rk(X \<union> {B})" and "rk(X \<union> {B}) = rk(X \<union> {C})" 
     and "rk(X \<union> {C}) = rk(X \<union> {D})" and "rk(X \<union> {D}) = rk X"
     using matroid_ax_3_alt' that(1) that(2) that(3) that(4) 
     by auto
   then have f2:"rk (X \<union> {A, B, C, D}) \<le> 3" if "rk(X \<union> {A}) = rk(X \<union> {B})" and "rk(X \<union> {B}) = rk(X \<union> {C})" 
     and "rk(X \<union> {C}) = rk(X \<union> {D})" and "rk(X \<union> {D}) = rk X"
     using assms that(1) that(2) that(3) that(4) 
     by linarith
   from f1 and f2 have "False" if "rk(X \<union> {A}) = rk(X \<union> {B})" and "rk(X \<union> {B}) = rk(X \<union> {C})" 
     and "rk(X \<union> {C}) = rk(X \<union> {D})" and "rk(X \<union> {D}) = rk X"
     using that(1) that(2) that(3) that(4) 
     by linarith
   then have "rk (X \<union> {A}) = rk X + 1 \<or> rk (X \<union> {B}) = rk X + 1 \<or> rk (X \<union> {C}) = rk X + 1 \<or> 
     rk (X \<union> {D}) = rk X + 1"
     by (smt One_nat_def Suc_le_eq Suc_numeral Un_upper2 \<open>4 \<le> rk {A, B, C, D}\<close> 
         \<open>\<lbrakk>rk (X \<union> {A}) = rk (X \<union> {B}); rk (X \<union> {B}) = rk (X \<union> {C}); rk (X \<union> {C}) = rk (X \<union> {D}); rk (X \<union> {D}) = rk X\<rbrakk> \<Longrightarrow> rk (X \<union> {A, B, C, D}) = rk X\<close> 
         add.right_neutral add_Suc_right assms antisym_conv1 matroid_ax_2 matroid_ax_2_alt 
         not_less semiring_norm(2) semiring_norm(8) sup.coboundedI2 sup.orderE)
   thus "\<exists>P . rk (X \<union> {P}) = rk X + 1" 
     by blast
 qed
 
 lemma rk_singleton : "\<forall>P. rk {P} = 1"
 proof
   fix P
   have f1:"rk {P} \<le> 1"
     by (metis One_nat_def card.empty card_Suc_eq insert_absorb insert_not_empty matroid_ax_1b)
   have f2:"rk {P} \<ge> 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"
   by (simp add: assms rk_singleton)
 
 lemma rk_couple :
   assumes "A \<noteq> B"
   shows "rk {A, B} = 2"
 proof-
   have f1:"rk {A, B} \<le> 2"
     by (metis insert_is_Un matroid_ax_2_alt one_add_one rk_singleton)
   have f2:"rk {A, B} \<ge> 2"
     by (simp add: assms rk_ax_couple)
   from f1 and f2 show "?thesis"
     by (simp add: f1 le_antisym)
 qed
 
 lemma rk_triple_le : "rk {A, B, C} \<le> 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 \<noteq> B"
     using rk_couple 
     by (simp add: that)
   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} \<le> 2" 
     using matroid_ax_1b
     by (metis one_le_numeral rk_ax_couple rk_couple rk_singleton_bis)
   have "rk {A, B, C} \<le> 2" if "rk {A, B} = 1"
     using matroid_ax_2_alt[of "{A, B}" C]
     by (simp add: insert_commute that)
   then have "rk {A, B} \<ge> 2"
     using assms rk_ax_couple rk_singleton_bis 
     by force
   thus "rk {A, B} = 2"
     by (simp add: \<open>rk {A, B} \<le> 2\<close> le_antisym)
 qed
 
 
 end
 
+end
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
     
 
 
 
diff --git a/thys/Projective_Geometry/Pappus_Desargues.thy b/thys/Projective_Geometry/Pappus_Desargues.thy
--- a/thys/Projective_Geometry/Pappus_Desargues.thy
+++ b/thys/Projective_Geometry/Pappus_Desargues.thy
@@ -1,487 +1,488 @@
 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 \<open> 
 Contents:
-\<^item> We prove Hessenberg's theorem ([\<open>hessenberg_theorem\<close>]): Pappus's property implies Desargues's 
-property in a projective plane. 
+\<^item> We prove Hessenberg's theorem @{term "hessenberg_theorem"}: Pappus's property implies Desargues's 
+property in a projective plane.  
 \<close>
 
 section \<open>Hessenberg's Theorem\<close>
 
+context projective_plane
+begin
+
 lemma col_ABC_ABD_1:
   assumes "A \<noteq> 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 \<noteq> 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 \<noteq> B" and "B \<noteq> 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 \<noteq> B" and "A \<noteq> 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 "\<not> col A A' B'"
 proof
   assume a1:"col A A' B'"
   have f1:"A \<noteq> A'" 
     using assms desargues_config_def distinct7_def 
-    by blast
+    by force
   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' \<noteq> B'" 
     using assms desargues_config_def distinct7_def 
-    by blast
+    by force
   have f6:"B' \<noteq> R" 
     using assms desargues_config_def distinct7_def 
-    by blast
+    by force
   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: \<open>line B' R = line B B'\<close> f4 f7)
   then have "False"
-    using assms desargues_config_def distinct3l_def 
+    using assms desargues_config_def distinct3_def 
     by auto
   then show f8:"col A A' B' \<Longrightarrow> False"
     by simp
 qed
 
 lemma desargues_config_not_col_2:
   assumes "desargues_config A B C A' B' C' M N P R"
   shows "\<not> 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 "\<not> 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)
+      desargues_config_rot_CW distinct3_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 "\<not> 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 "\<not> 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 "\<not> 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 "\<not> 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 \<noteq> A'"
     using assms col_AAB desargues_config_not_col_4 
     by blast
   have f4:"A \<noteq> 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 \<open>line A R = line B R\<close> 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 
+    using assms desargues_config_def distinct3_def 
     by auto
   thus "col A B B' \<Longrightarrow> False"
     by simp
 qed
 
 lemma desargues_config_not_col_8:
   assumes "desargues_config A B C A' B' C' M N P R"
   shows "\<not> 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)
+  
+  by (smt (z3) assms col_ABA col_line_eq_1 col_rot_CW desargues_config_def desargues_config_not_col_6 desargues_config_not_col_7 distinct3_def meet_3_col_1 meet_3_col_3 projective_plane.meet_all_3 projective_plane.meet_col_1 projective_plane_axioms)
+  (*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 distinct3_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 "\<not> 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 "\<not> 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 "\<not> 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 "\<not> col C B B'"
   using assms desargues_config_not_col_8 desargues_config_rot_CW 
   by blast
 
 lemma col_inter:
   assumes "A \<noteq> C" and "B \<noteq> 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 \<or> incid A (line B' C') \<or> incid C' (line A B)"
 proof-
   have "?thesis" if "incid A (line B' C') \<or> incid C' (line A B)"
     by (simp add: that)
 (* 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 "\<not> incid A (line B' C')" and "\<not> incid C' (line A B)"
   proof-
-    have f1:"distinct6 C C' R Q B A"
+    have f1:"distinct [C,C',R,Q,B,A]"
       by (smt Q_def \<open>\<not> incid A (line B' C')\<close> \<open>\<not> incid C' (line A B)\<close> 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 "\<not> incid A (line B' C')" and "\<not> incid C' (line A B)"
   proof-
-    have f1:"distinct6 A' A R Q B' C'"
+    have f1:"distinct [A',A,R,Q,B',C']"
       by (smt Q_def \<open>\<not> incid A (line B' C')\<close> \<open>\<not> incid C' (line A B)\<close> 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 "\<not> incid A (line B' C')" and "\<not> incid C' (line A B)"
     proof-
       have f1:"Q \<noteq> C' \<and> X \<noteq> E \<and> line Q C' \<noteq> line X E"
         by (smt E_def Q_def X_def \<open>\<not> incid A (line B' C')\<close> \<open>\<not> incid C' (line A B)\<close> 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 \<noteq> A \<and> C' \<noteq> F \<and> line E A \<noteq> line C' F"
         by (smt E_def F_def Q_def X_def \<open>\<lbrakk>\<not> incid A (line B' C'); \<not> incid C' (line A B)\<rbrakk> \<Longrightarrow> col X E M\<close> 
             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 \<noteq> A \<and> X \<noteq> F \<and> line Q A \<noteq> line X F"
         by (smt F_def Q_def X_def \<open>\<not> incid A (line B' C')\<close> \<open>\<not> incid C' (line A B)\<close> 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 \<open>\<lbrakk>\<not> incid A (line B' C'); \<not> incid C' (line A B)\<rbrakk> \<Longrightarrow> col X E M\<close> 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 \<open>\<lbrakk>\<not> incid A (line B' C'); \<not> incid C' (line A B)\<rbrakk> \<Longrightarrow> col P X F\<close> 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))
+        by (metis Q_def \<open>\<lbrakk>\<not> incid A (line B' C'); \<not> incid C' (line A B)\<rbrakk> \<Longrightarrow> col P X F\<close> assms(1) col_AAB col_A_B_ABl col_line_eq_2 col_rot_CW desargues_config_def is_a_intersec_def meet_col_1 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 \<or> incid A (line B' C') \<or> incid C' (line A B)"
       using \<open>\<lbrakk>\<not> incid A (line B' C'); \<not> incid C' (line A B)\<rbrakk> \<Longrightarrow> col M N P\<close> 
       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 \<or> ((incid A (line B' C') \<or> incid C' (line A B)) \<and> 
   (incid C (line A' B') \<or> incid B' (line A C)) \<and> (incid B (line A' C') \<or> 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] \<Rightarrow> bool" where
+  "['point, 'point, 'point, 'point, 'point, 'point] \<Rightarrow> bool" where
 "triangle_circumscribes_triangle A' B' C' A B C \<equiv> incid A (line B' C') \<and> incid C (line A' B') \<and>
 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') \<or> incid C' (line A B)" 
     and "incid C (line A' B') \<or> incid B' (line A C)" and "incid B (line A' C') \<or> incid A' (line B C)"
   shows "col M N P \<or> triangle_circumscribes_triangle A B C A' B' C' \<or> 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"
+    have f1:"distinct [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 \<open>distinct6 R C C' P B A\<close> assms(3) ax_uniqueness distinct6_def incidA_lAB incidB_lAB 
+      by (metis \<open>distinct [R,C,C',P,B,A]\<close> 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'"
       by (simp add: col_rot_CW)
   qed
   have "col M T A'"
   proof-
-    have f1:"distinct6 R C C' P A B"
+    have f1:"distinct [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 \<open>distinct6 R C C' P A B\<close> assms(2) assms(3) ax_uniqueness desargues_config_def 
+      by (metis \<open>distinct [R,C,C',P,A,B]\<close> 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 \<open>distinct6 R C C' P A B\<close> assms(2) col_AAB col_line_eq_2 desargues_config_def 
+      by (metis \<open>distinct [R,C,C',P,A,B]\<close> 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'"
       by (simp add: col_rot_CW)
   qed
   then show "col M N P"
   proof-
     have f1:"S \<noteq> T \<and> B \<noteq> A \<and> line S T \<noteq> line B A"
       by (smt T_def \<open>col N S B'\<close> 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 \<noteq> B' \<and> T \<noteq> A' \<and> line A B' \<noteq> 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)
+      by (smt (verit) S_def T_def assms(2) assms(3) col_A_B_ABl col_line_eq_2 desargues_config_def desargues_config_not_col_1 desargues_config_not_col_9 f1 incidA_lAB inter_comm line_comm meet_3_col_1 meet_col_2 projective_plane.col_def projective_plane_axioms triangle_circumscribes_triangle_def)
     have f3:"S \<noteq> B' \<and> B \<noteq> 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' \<noteq> 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 \<open>col M T A'\<close> 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)
+      by (smt (verit, del_insts) \<open>col M T A'\<close> assms(2) assms(3) col_rot_CW desargues_config_def f2 incidA_lAB incidB_lAB is_a_intersec_def meet_col_2 projective_plane.ax_uniqueness projective_plane_axioms triangle_circumscribes_triangle_def)
     have f9:"is_a_intersec N S B' B A'"
       using \<open>col N S B'\<close> 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"
       by (simp add: col_rot_CW)
   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 \<or> ((incid A (line B' C') \<or> incid C' (line A B)) \<and> 
   (incid C (line A' B') \<or> incid B' (line A C)) \<and> (incid B (line A' C') \<or> incid A' (line B C)))"
     using assms corollary_1 
     by auto
   have f2:"col M N P \<or> triangle_circumscribes_triangle A B C A' B' C' \<or> triangle_circumscribes_triangle A' B' C' A B C"
     if "(incid A (line B' C') \<or> incid C' (line A B)) \<and> (incid C (line A' B') \<or> incid B' (line A C)) 
     \<and> (incid B (line A' C') \<or> 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" 
+      have f1:"distinct [A',B',C',A,B,C,R]" 
         using assms(2) desargues_config_def distinct7_def 
         by auto
       have f2:"\<not> col A' B' C'"
         using assms(2) desargues_config_def 
         by blast
       have f3:"\<not> col A B C"
         using assms(2) desargues_config_def 
         by blast
-      have f4:"distinct3l (line A' A) (line B' B) (line C' C)"
+      have f4:"distinct [(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') \<noteq> (line A B) \<and> (line B' C') \<noteq> (line B C) \<and> (line A' C') \<noteq> (line A C)"
         using assms(2) desargues_config_def 
         by auto
       have f7:"meet_in (line B' C') (line B C) M \<and> meet_in (line A' C') (line A C) N \<and> 
       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"
         by (simp add: desargues_config_def)
     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
 
-
+end
     
 
 
 
 
 
 
 
 
 
 
 
 
 
diff --git a/thys/Projective_Geometry/Pappus_Property.thy b/thys/Projective_Geometry/Pappus_Property.thy
--- a/thys/Projective_Geometry/Pappus_Property.thy
+++ b/thys/Projective_Geometry/Pappus_Property.thy
@@ -1,278 +1,283 @@
 theory Pappus_Property
   imports Main Projective_Plane_Axioms
 begin
 
 (* Author: Anthony Bordg, University of Cambridge, apdb3@cam.ac.uk .*)
  
 text \<open>
 Contents:
 \<^item> We give two formulations of Pappus's property for a configuration of nine points
- [\<open>is_pappus1\<close>] [\<open>is_pappus2\<close>].
-\<^item> We prove the equivalence of these two formulations [\<open>pappus_equiv\<close>].
-\<^item> We state Pappus property for a plane [\<open>is_pappus\<close>]. 
+ @{term is_pappus1} @{term is_pappus2}.
+\<^item> We prove the equivalence of these two formulations @{term pappus_equiv}.
+\<^item> We state Pappus property for a plane @{term is_pappus}. 
 \<close>
 
 section \<open>Pappus's Property\<close>
 
-definition col :: "[Points, Points, Points] \<Rightarrow> bool" where
+context projective_plane
+begin
+
+definition col :: "['point, 'point, 'point] \<Rightarrow> bool" where
 "col A B C \<equiv> \<exists>l. incid A l \<and> incid B l \<and> incid C l"
 
-definition distinct6 ::
-  "[Points, Points, Points, Points, Points, Points] \<Rightarrow> bool" where
-"distinct6 A B C D E F \<equiv> (A \<noteq> B) \<and> (A \<noteq> C) \<and> (A \<noteq> D) \<and> (A \<noteq> E) \<and> (A \<noteq> F) \<and>
+lemma distinct6_def:
+"distinct [A,B,C,D,E,F] \<equiv> (A \<noteq> B) \<and> (A \<noteq> C) \<and> (A \<noteq> D) \<and> (A \<noteq> E) \<and> (A \<noteq> F) \<and>
 (B \<noteq> C) \<and> (B \<noteq> D) \<and> (B \<noteq> E) \<and> (B \<noteq> F) \<and>
 (C \<noteq> D) \<and> (C \<noteq> E) \<and> (C \<noteq> F) \<and>
 (D \<noteq> E) \<and> (D \<noteq> F) \<and>
 (E \<noteq> F)"
+  by auto
 
-definition lines :: "Points \<Rightarrow> Points \<Rightarrow> Lines set" where
+definition lines :: "'point \<Rightarrow> 'point \<Rightarrow> 'line set" where
 "lines P Q \<equiv> {l. incid P l \<and> incid Q l}"
 
 lemma uniq_line:
   assumes "P \<noteq> Q" and "l \<in> lines P Q" and "m \<in> lines P Q"
   shows "l = m"
   using assms lines_def ax_uniqueness 
   by blast
 
-definition line :: "Points \<Rightarrow> Points \<Rightarrow> Lines" where
+definition line :: "'point \<Rightarrow> 'point \<Rightarrow> 'line" where
 "line P Q \<equiv> @l. incid P l \<and> 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] \<Rightarrow> bool" where
+definition is_a_proper_intersec :: "['point, 'point, 'point, 'point, 'point] \<Rightarrow> bool" where
 "is_a_proper_intersec P A B C D \<equiv> (A \<noteq> B) \<and> (C \<noteq> D) \<and> (line A B \<noteq> line C D)
 \<and> col P A B \<and> 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
+"['point, 'point, 'point, 'point, 'point, 'point, 'point, 'point, 'point] => bool " where
 "is_pappus1 A B C A' B' C' P Q R \<equiv> 
-  distinct6 A B C A' B' C' \<longrightarrow> col A B C \<longrightarrow> col A' B' C'
+  distinct[A,B,C,A',B',C'] \<longrightarrow> col A B C \<longrightarrow> col A' B' C'
   \<longrightarrow> is_a_proper_intersec P A B' A' B \<longrightarrow> is_a_proper_intersec Q B C' B' C
   \<longrightarrow> is_a_proper_intersec R A C' A' C 
   \<longrightarrow> col P Q R"
 
-definition is_a_intersec :: "[Points, Points, Points, Points, Points] \<Rightarrow> bool" where
+definition is_a_intersec :: "['point, 'point, 'point, 'point, 'point] \<Rightarrow> bool" where
 "is_a_intersec P A B C D \<equiv> col P A B \<and> 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] \<Rightarrow> bool" where
+"['point, 'point, 'point, 'point, 'point, 'point, 'point, 'point, 'point] \<Rightarrow> bool" where
 "is_pappus2 A B C A' B' C' P Q R \<equiv> 
-  (distinct6 A B C A' B' C' \<or> (A \<noteq> B' \<and> A'\<noteq> B \<and> line A B' \<noteq> line A' B \<and> 
+  (distinct [A,B,C,A',B',C'] \<or> (A \<noteq> B' \<and> A'\<noteq> B \<and> line A B' \<noteq> line A' B \<and> 
   B \<noteq> C' \<and> B' \<noteq> C \<and> line B C' \<noteq> line B' C \<and> 
   A \<noteq> C' \<and> A' \<noteq> C \<and> line A C' \<noteq> line A' C)) 
   \<longrightarrow> col A B C \<longrightarrow> col A' B' C' \<longrightarrow> is_a_intersec P A B' A' B 
   \<longrightarrow> is_a_intersec Q B C' B' C \<longrightarrow> is_a_intersec R A C' A' C 
   \<longrightarrow> 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
+  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 \<or> line B C' = line B' C \<or> 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 \<open>line A B' = line A' B \<Longrightarrow> col P Q R\<close> 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 \<open>line B C' = line B' C \<Longrightarrow> col P Q R\<close> assms(1) assms(2) assms(3) assms(7) ax_uniqueness 
         col_def distinct6_def incidA_lAB incidB_lAB)
   show "col P Q R"
     using \<open>line A B' = line A' B \<Longrightarrow> col P Q R\<close> \<open>line A C' = line A' C \<Longrightarrow> col P Q R\<close> 
       \<open>line B C' = line B' C \<Longrightarrow> col P Q R\<close> 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 \<noteq> B' \<and> A'\<noteq> B \<and> line A B' \<noteq> line A' B \<and> 
   B \<noteq> C' \<and> B' \<noteq> C \<and> line B C' \<noteq> line B' C \<and> 
   A \<noteq> C' \<and> A' \<noteq> C \<and> line A C' \<noteq> 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 \<open>A \<noteq> B' \<and> A' \<noteq> B \<and> line A B' \<noteq> line A' B \<and> B \<noteq> C' \<and> B' \<noteq> C \<and> line B C' \<noteq> line B' C 
   \<and> A \<noteq> C' \<and> A' \<noteq> C \<and> line A C' \<noteq> line A' C\<close> \<open>is_a_intersec P A B' A' B\<close> ax_uniqueness col_def 
             incidA_lAB incidB_lAB is_a_intersec_def that)
       have "col P A C' \<and> col Q A C' \<and> col R A C'"
         using \<open>P = A\<close> \<open>is_a_intersec Q B C' B' C\<close> \<open>is_a_intersec R A C' A' C\<close> col_AAB 
           is_a_intersec_def that 
         by auto
       then show "col P Q R"
         by (smt \<open>A \<noteq> B' \<and> A' \<noteq> B \<and> line A B' \<noteq> line A' B \<and> B \<noteq> C' \<and> B' \<noteq> C \<and> line B C' \<noteq> line B' C 
           \<and> A \<noteq> C' \<and> A' \<noteq> C \<and> line A C' \<noteq> line A' C\<close> 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 \<open>A \<noteq> B' \<and> A' \<noteq> B \<and> line A B' \<noteq> line A' B \<and> B \<noteq> C' \<and> B' \<noteq> C \<and> line B C' \<noteq> line B' C 
         \<and> A \<noteq> C' \<and> A' \<noteq> C \<and> line A C' \<noteq> line A' C\<close> \<open>is_a_intersec R A C' A' C\<close> ax_uniqueness col_def incidA_lAB incidB_lAB is_a_intersec_def that)
     have "col P A B' \<and> col Q A B' \<and> col R A B'"
       using \<open>R = A\<close> \<open>is_a_intersec P A B' A' B\<close> \<open>is_a_intersec Q B C' B' C\<close> col_def 
         is_a_intersec_def that 
       by auto
     then show "col P Q R"
       by (smt \<open>A \<noteq> B' \<and> A' \<noteq> B \<and> line A B' \<noteq> line A' B \<and> B \<noteq> C' \<and> B' \<noteq> C \<and> line B C' \<noteq> line B' C 
         \<and> A \<noteq> C' \<and> A' \<noteq> C \<and> line A C' \<noteq> line A' C\<close> ax_uniqueness col_def)
   qed
   have "col P Q R" if "A = A'" (* very degenerate case, all the 9 points are collinear*)
     by (smt \<open>A \<noteq> B' \<and> A' \<noteq> B \<and> line A B' \<noteq> line A' B \<and> B \<noteq> C' \<and> B' \<noteq> C \<and> line B C' \<noteq> line B' C \<and> 
       A \<noteq> C' \<and> A' \<noteq> C \<and> line A C' \<noteq> line A' C\<close> \<open>is_a_intersec P A B' A' B\<close> \<open>is_a_intersec R A C' A' C\<close> 
         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 \<open>A \<noteq> B' \<and> A' \<noteq> B \<and> line A B' \<noteq> line A' B \<and> B \<noteq> C' \<and> B' \<noteq> C \<and> line B C' \<noteq> line B' C \<and> 
       A \<noteq> C' \<and> A' \<noteq> C \<and> line A C' \<noteq> line A' C\<close> \<open>is_a_intersec P A B' A' B\<close> \<open>is_a_intersec Q B C' B' C\<close> 
         \<open>is_a_intersec R A C' A' C\<close> 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 \<open>A \<noteq> B' \<and> A' \<noteq> B \<and> line A B' \<noteq> line A' B \<and> B \<noteq> C' \<and> B' \<noteq> C \<and> line B C' \<noteq> line B' C \<and> 
       A \<noteq> C' \<and> A' \<noteq> C \<and> line A C' \<noteq> line A' C\<close> \<open>is_a_intersec P A B' A' B\<close> \<open>is_a_intersec Q B C' B' C\<close> 
         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 \<open>A \<noteq> B' \<and> A' \<noteq> B \<and> line A B' \<noteq> line A' B \<and> B \<noteq> C' \<and> B' \<noteq> C \<and> line B C' \<noteq> line B' C \<and> 
       A \<noteq> C' \<and> A' \<noteq> C \<and> line A C' \<noteq> line A' C\<close> \<open>is_a_intersec Q B C' B' C\<close> \<open>is_a_intersec R A C' A' C\<close> 
         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 \<open>A \<noteq> B' \<and> A' \<noteq> B \<and> line A B' \<noteq> line A' B \<and> B \<noteq> C' \<and> B' \<noteq> C \<and> line B C' \<noteq> line B' C \<and> 
       A \<noteq> C' \<and> A' \<noteq> C \<and> line A C' \<noteq> line A' C\<close> \<open>is_a_intersec P A B' A' B\<close> \<open>is_a_intersec Q B C' B' C\<close> 
         \<open>is_a_intersec R A C' A' C\<close> 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 \<open>A \<noteq> B' \<and> A' \<noteq> B \<and> line A B' \<noteq> line A' B \<and> B \<noteq> C' \<and> B' \<noteq> C \<and> line B C' \<noteq> line B' C \<and> 
       A \<noteq> C' \<and> A' \<noteq> C \<and> line A C' \<noteq> line A' C\<close> \<open>is_a_intersec P A B' A' B\<close> \<open>is_a_intersec Q B C' B' C\<close> 
         \<open>is_a_intersec R A C' A' C\<close> 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 \<open>A \<noteq> B' \<and> A' \<noteq> B \<and> line A B' \<noteq> line A' B \<and> B \<noteq> C' \<and> B' \<noteq> C \<and> line B C' \<noteq> line B' C \<and> 
       A \<noteq> C' \<and> A' \<noteq> C \<and> line A C' \<noteq> line A' C\<close> \<open>is_a_intersec P A B' A' B\<close> \<open>is_a_intersec Q B C' B' C\<close> 
         \<open>is_a_intersec R A C' A' C\<close> ax_uniqueness col_def incidA_lAB incidB_lAB is_a_intersec_def that)
   have "col P Q R" if "A \<noteq> B \<and> A \<noteq> C \<and> A \<noteq> A' \<and> B \<noteq> C \<and> B \<noteq> B' \<and> C \<noteq> C' \<and> A'\<noteq> B'
     \<and> A' \<noteq> C' \<and> B' \<noteq> C'"
   proof -
-    have a1:"distinct6 A B C A' B' C'"
+    have a1:"distinct [A,B,C,A',B',C']"
       using \<open>A \<noteq> B' \<and> A' \<noteq> B \<and> line A B' \<noteq> line A' B \<and> B \<noteq> C' \<and> B' \<noteq> C \<and> line B C' \<noteq> line B' C \<and> 
         A \<noteq> C' \<and> A' \<noteq> C \<and> line A C' \<noteq> line A' C\<close> distinct6_def that 
       by auto
     have "is_a_proper_intersec P A B' A' B"
       using \<open>A \<noteq> B' \<and> A' \<noteq> B \<and> line A B' \<noteq> line A' B \<and> B \<noteq> C' \<and> B' \<noteq> C \<and> line B C' \<noteq> line B' C \<and> 
         A \<noteq> C' \<and> A' \<noteq> C \<and> line A C' \<noteq> line A' C\<close> \<open>is_a_intersec P A B' A' B\<close> is_a_intersec_def 
         is_a_proper_intersec_def 
       by auto
     have "is_a_proper_intersec Q B C' B' C"
       using \<open>A \<noteq> B' \<and> A' \<noteq> B \<and> line A B' \<noteq> line A' B \<and> B \<noteq> C' \<and> B' \<noteq> C \<and> line B C' \<noteq> line B' C \<and> 
         A \<noteq> C' \<and> A' \<noteq> C \<and> line A C' \<noteq> line A' C\<close> \<open>is_a_intersec Q B C' B' C\<close> is_a_intersec_def 
         is_a_proper_intersec_def 
       by auto
     have "is_a_proper_intersec R A C' A' C"
       using \<open>A \<noteq> B' \<and> A' \<noteq> B \<and> line A B' \<noteq> line A' B \<and> B \<noteq> C' \<and> B' \<noteq> C \<and> line B C' \<noteq> line B' C \<and> 
         A \<noteq> C' \<and> A' \<noteq> C \<and> line A C' \<noteq> line A' C\<close> \<open>is_a_intersec R A C' A' C\<close> is_a_intersec_def 
         is_a_proper_intersec_def 
       by auto
     show "col P Q R"
       using \<open>is_a_proper_intersec P A B' A' B\<close> \<open>is_a_proper_intersec Q B C' B' C\<close> 
         \<open>is_a_proper_intersec R A C' A' C\<close> a1 assms h1 h2 is_pappus1_def 
       by blast
   qed
     show "col P Q R"
       using \<open>A = A' \<Longrightarrow> col P Q R\<close> \<open>A = B \<Longrightarrow> col P Q R\<close> \<open>A = C \<Longrightarrow> col P Q R\<close> 
         \<open>A \<noteq> B \<and> A \<noteq> C \<and> A \<noteq> A' \<and> B \<noteq> C \<and> B \<noteq> B' \<and> C \<noteq> C' \<and> A' \<noteq> B' \<and> A' \<noteq> C' \<and> B' \<noteq> C' \<Longrightarrow> col P Q R\<close> 
         \<open>A' = B' \<Longrightarrow> col P Q R\<close> \<open>A' = C' \<Longrightarrow> col P Q R\<close> \<open>B = B' \<Longrightarrow> col P Q R\<close> \<open>B = C \<Longrightarrow> col P Q R\<close> 
         \<open>B' = C' \<Longrightarrow> col P Q R\<close> \<open>C = C' \<Longrightarrow> col P Q R\<close> 
       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'"
+  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 \<open>col A B C\<close> \<open>col A' B' C'\<close> \<open>distinct6 A B C A' B' C'\<close> \<open>is_a_intersec P A B' A' B\<close> 
+      using \<open>col A B C\<close> \<open>col A' B' C'\<close> \<open>distinct [A,B,C,A',B',C']\<close> \<open>is_a_intersec P A B' A' B\<close> 
         \<open>is_a_intersec Q B C' B' C\<close> \<open>is_a_intersec R A C' A' C\<close> degenerate_hexagon_is_pappus that 
       by blast
     have "col P Q R" if "line B C' = line B' C"
-      using \<open>col A B C\<close> \<open>col A' B' C'\<close> \<open>distinct6 A B C A' B' C'\<close> \<open>is_a_intersec P A B' A' B\<close> 
+      using \<open>col A B C\<close> \<open>col A' B' C'\<close> \<open>distinct [A,B,C,A',B',C']\<close> \<open>is_a_intersec P A B' A' B\<close> 
         \<open>is_a_intersec Q B C' B' C\<close> \<open>is_a_intersec R A C' A' C\<close> degenerate_hexagon_is_pappus that 
       by blast
     have "col P Q R" if "line A' C = line A C'"
-      using \<open>col A B C\<close> \<open>col A' B' C'\<close> \<open>distinct6 A B C A' B' C'\<close> \<open>is_a_intersec P A B' A' B\<close> 
+      using \<open>col A B C\<close> \<open>col A' B' C'\<close> \<open>distinct [A,B,C,A',B',C']\<close> \<open>is_a_intersec P A B' A' B\<close> 
         \<open>is_a_intersec Q B C' B' C\<close> \<open>is_a_intersec R A C' A' C\<close> degenerate_hexagon_is_pappus that 
       by auto
     have "col P Q R" if "line A B' \<noteq> line A' B" and "line B C' \<noteq> line B' C" and
       "line A C' \<noteq> line A' C"
     proof -
       have "is_a_proper_intersec P A B' A' B"
-        using \<open>distinct6 A B C A' B' C'\<close> \<open>is_a_intersec P A B' A' B\<close> distinct6_def is_a_intersec_def 
+        using \<open>distinct [A,B,C,A',B',C']\<close> \<open>is_a_intersec P A B' A' B\<close> 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 \<open>distinct6 A B C A' B' C'\<close> \<open>is_a_intersec Q B C' B' C\<close> distinct6_def is_a_intersec_def 
+        using \<open>distinct [A,B,C,A',B',C']\<close> \<open>is_a_intersec Q B C' B' C\<close> 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 \<open>distinct6 A B C A' B' C'\<close> \<open>is_a_intersec R A C' A' C\<close> distinct6_def is_a_intersec_def 
+        using \<open>distinct [A,B,C,A',B',C']\<close> \<open>is_a_intersec R A C' A' C\<close> distinct6_def is_a_intersec_def 
           is_a_proper_intersec_def that(3) 
         by auto
       show "col P Q R"
-        using \<open>col A B C\<close> \<open>col A' B' C'\<close> \<open>distinct6 A B C A' B' C'\<close> \<open>is_a_proper_intersec P A B' A' B\<close> 
+        using \<open>col A B C\<close> \<open>col A' B' C'\<close> \<open>distinct [A,B,C,A',B',C']\<close> \<open>is_a_proper_intersec P A B' A' B\<close> 
           \<open>is_a_proper_intersec Q B C' B' C\<close> \<open>is_a_proper_intersec R A C' A' C\<close> assms is_pappus1_def 
         by blast
     qed
     show "col P Q R"
       using \<open>\<lbrakk>line A B' \<noteq> line A' B; line B C' \<noteq> line B' C; line A C' \<noteq> line A' C\<rbrakk> \<Longrightarrow> col P Q R\<close> 
         \<open>line A B' = line A' B \<Longrightarrow> col P Q R\<close> \<open>line A' C = line A C' \<Longrightarrow> col P Q R\<close> 
         \<open>line B C' = line B' C \<Longrightarrow> col P Q R\<close> 
       by fastforce
   qed
   show "is_pappus2 A B C A' B' C' P Q R"
     by (simp add: \<open>\<lbrakk>A \<noteq> B' \<and> A' \<noteq> B \<and> line A B' \<noteq> line A' B \<and> B \<noteq> C' \<and> B' \<noteq> C \<and> line B C' \<noteq> line B' C 
       \<and> A \<noteq> C' \<and> A' \<noteq> C \<and> line A C' \<noteq> 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\<rbrakk> \<Longrightarrow> col P Q R\<close> 
-        \<open>\<lbrakk>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\<rbrakk> \<Longrightarrow> col P Q R\<close> 
+        \<open>\<lbrakk>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\<rbrakk> \<Longrightarrow> col P Q R\<close> 
         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 \<equiv> \<forall>A B C D E F P Q R. is_pappus2 A B C D E F P Q R"
 
 end
+
+end
\ No newline at end of file
diff --git a/thys/Projective_Geometry/Pascal_Property.thy b/thys/Projective_Geometry/Pascal_Property.thy
--- a/thys/Projective_Geometry/Pascal_Property.thy
+++ b/thys/Projective_Geometry/Pascal_Property.thy
@@ -1,444 +1,449 @@
 theory Pascal_Property
   imports Main Projective_Plane_Axioms Pappus_Property
 begin
 
 (* Author: Anthony Bordg, University of Cambridge, apdb3@cam.ac.uk .*)
 
 text \<open>
 Contents:
-\<^item> A hexagon is pascal if its three opposite sides meet in collinear points [\<open>is_pascal\<close>].
+\<^item> A hexagon is pascal if its three opposite sides meet in collinear points @{term is_pascal}.
 \<^item> 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. 
 \<close>
 
 section \<open>Pascal's Property\<close>
 
-definition inters :: "Lines \<Rightarrow> Lines \<Rightarrow> Points set" where
+context projective_plane
+begin 
+
+definition inters :: "'line \<Rightarrow> 'line \<Rightarrow> 'point set" where
 "inters l m \<equiv> {P. incid P l \<and> incid P m}"
 
 lemma inters_is_singleton:
   assumes "l \<noteq> m" and "P \<in> inters l m" and "Q \<in> inters l m"
   shows "P = Q"
   using assms ax_uniqueness inters_def 
   by blast
 
-definition inter :: "Lines \<Rightarrow> Lines \<Rightarrow> Points" where
+definition inter :: "'line \<Rightarrow> 'line \<Rightarrow> 'point" where
 "inter l m \<equiv> @P. P \<in> inters l m"
 
 lemma uniq_inter:
   assumes "l \<noteq> m" and "incid P l" and "incid P m"
   shows "inter l m = P"
 proof -
   have "P \<in> inters l m"
     by (simp add: assms(2) assms(3) inters_def)
   have "\<forall>Q. Q \<in> inters l m \<longrightarrow> Q = P"
     using \<open>P \<in> inters l m\<close> assms(1) inters_is_singleton 
     by blast
   show "inter l m = P"
     using \<open>P \<in> inters l m\<close> 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] \<Rightarrow> bool" where
-"is_pascal A B C D E F \<equiv> distinct6 A B C D E F \<longrightarrow> line B C \<noteq> line E F \<longrightarrow> line C D \<noteq> line A F
+definition is_pascal :: "['point, 'point, 'point, 'point, 'point, 'point] \<Rightarrow> bool" where
+"is_pascal A B C D E F \<equiv> distinct [A,B,C,D,E,F] \<longrightarrow> line B C \<noteq> line E F \<longrightarrow> line C D \<noteq> line A F
 \<longrightarrow> line A B \<noteq> line D E \<longrightarrow> 
 (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"
+  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 \<noteq> 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 \<noteq> 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 \<noteq> 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 \<noteq> D" and "line A B \<noteq> 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 \<noteq> line D E" and "line B C \<noteq> line E F" 
+  have "col P Q R" if "distinct [F,A,B,C,D,E]" and "line A B \<noteq> line D E" and "line B C \<noteq> line E F" 
     and "line F A \<noteq> 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 \<noteq> 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 \<in> inters l m"
   shows "incid P l"
   using assms inters_def 
   by auto
 
 lemma incid_inters_right:
   assumes "P \<in> inters l m"
   shows "incid P m"
   using assms incid_inters_left inters_comm 
   by blast
 
 lemma inter_in_inters: "inter l m \<in> inters l m"
 proof -
   have "\<exists>P. P \<in> inters l m"
     using inters_def ax2 
     by auto
   show "inter l m \<in> inters l m"
     by (metis \<open>\<exists>P. P \<in> inters l m\<close> 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 \<Rightarrow> Points set" where
+definition line_ext :: "'line \<Rightarrow> 'point set" where
 "line_ext l \<equiv> {P. incid P l}"
 
 lemma line_left_inter_1: 
   assumes "P \<in> line_ext l" and "P \<notin> 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 \<in> line_ext m" and "P \<notin> 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 \<in> line_ext l" and "P \<notin> 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 \<in> line_ext m" and "P \<notin> 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 \<noteq> 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 \<noteq> 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 \<noteq> C"
   shows "B \<in> 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 \<in> line_ext n" and "l \<noteq> m" and "l \<noteq> 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 \<in> line_ext n" and "l \<noteq> m" and "m \<noteq> n"
   shows "inter l m = inter m n"
   by (metis assms inter_comm inter_line_ext_1)
 
 definition pascal_prop :: "bool" where
 "pascal_prop \<equiv> \<forall>A B C D E F. is_pascal A B C D E F \<longrightarrow> 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 \<noteq> line E F" and "line C D \<noteq> line B F" 
+    have "col X Y Z" if "distinct [B,A,C,D,E,F]" and "line A C \<noteq> line E F" and "line C D \<noteq> line B F" 
       and "line B A \<noteq> 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 \<noteq> line E F" and "line C D \<noteq> line B F" 
+    have "col X Y Z" if "distinct [B,A,C,D,E,F]" and "line A C \<noteq> line E F" and "line C D \<noteq> line B F" 
       and "line B A \<noteq> 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 \<noteq> line E F" and "line C D \<noteq> line B F" 
+    have "col X Y Z" if "distinct [B,A,C,D,E,F]" and "line A C \<noteq> line E F" and "line C D \<noteq> line B F" 
       and "line B A \<noteq> line D E" and "line B C \<noteq> line E F" and "line C D \<noteq> 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 \<open>is_pascal A B C D E F\<close> 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 \<open>distinct6 B A C D E F\<close> ax_uniqueness col_ABA col_def 
+        by (smt P_def Q_def X_def Y_def Z_def \<open>distinct [B,A,C,D,E,F]\<close> 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 \<open>distinct6 B A C D E F\<close> \<open>line A C \<noteq> line E F\<close> 
+        by (smt P_def R_def X_def Y_def Z_def \<open>distinct [B,A,C,D,E,F]\<close> \<open>line A C \<noteq> line E F\<close> 
             \<open>line C D \<noteq> line B F\<close> 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 \<open>P = Q \<Longrightarrow> col X Y Z\<close> \<open>P = R \<Longrightarrow> col X Y Z\<close> 
             \<open>col P Q R\<close> \<open>line B C \<noteq> line E F\<close> 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 \<open>P = R \<Longrightarrow> col X Y Z\<close> \<open>col P Q R\<close> 
             \<open>line A C \<noteq> line E F\<close> 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 \<open>P = C \<Longrightarrow> col X Y Z\<close> \<open>P = Q \<Longrightarrow> col X Y Z\<close> 
-            \<open>col P Q R\<close> \<open>distinct6 B A C D E F\<close> ax_uniqueness col_def distinct6_def incidB_lAB 
+            \<open>col P Q R\<close> \<open>distinct [B,A,C,D,E,F]\<close> 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 \<open>distinct6 B A C D E F\<close> ax_uniqueness col_A_B_lAB 
+        by (smt Q_def R_def X_def Y_def Z_def \<open>distinct [B,A,C,D,E,F]\<close> 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 \<open>col P Q R\<close> \<open>distinct6 B A C D E F\<close> 
+        by (smt P_def Q_def R_def X_def Y_def Z_def \<open>col P Q R\<close> \<open>distinct [B,A,C,D,E,F]\<close> 
             \<open>line C D \<noteq> line B F\<close> 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 \<open>P = W \<Longrightarrow> col X Y Z\<close> \<open>distinct6 B A C D E F\<close> ax_uniqueness 
+        by (metis P_def Q_def W_def \<open>P = W \<Longrightarrow> col X Y Z\<close> \<open>distinct [B,A,C,D,E,F]\<close> 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 \<open>P = W \<Longrightarrow> col X Y Z\<close> \<open>Q = A \<Longrightarrow> col X Y Z\<close> 
-            \<open>col P Q R\<close> \<open>distinct6 B A C D E F\<close> ax_uniqueness col_ABA col_def col_rot_CW distinct6_def 
+            \<open>col P Q R\<close> \<open>distinct [B,A,C,D,E,F]\<close> 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 \<open>col P Q R\<close> \<open>distinct6 B A C D E F\<close> 
+        by (smt P_def Q_def R_def X_def Y_def Z_def \<open>col P Q R\<close> \<open>distinct [B,A,C,D,E,F]\<close> 
             \<open>line A C \<noteq> line E F\<close> 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 \<open>R = A \<Longrightarrow> col X Y Z\<close> \<open>R = C \<Longrightarrow> col X Y Z\<close> \<open>line C D \<noteq> line A F\<close> 
             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 \<open>P = R \<Longrightarrow> col X Y Z\<close> \<open>Q = A \<Longrightarrow> col X Y Z\<close> 
-            \<open>col P Q R\<close> \<open>distinct6 B A C D E F\<close> ax_uniqueness col_def distinct6_def incidA_lAB 
+            \<open>col P Q R\<close> \<open>distinct [B,A,C,D,E,F]\<close> 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 \<open>P = C \<Longrightarrow> col X Y Z\<close> \<open>line B C \<noteq> line E F\<close> 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 \<open>distinct6 P Q R A C W\<close> \<open>col P Q R\<close>
+      (inter (line P W) (line A R))" if "distinct [P,Q,R,A,C,W]"
+        using assms(1) is_pappus_def is_pappus2_def \<open>distinct [P,Q,R,A,C,W]\<close> \<open>col P Q R\<close>
           \<open>col A C W\<close> inter_is_a_intersec inter_line_line_comm 
-        by metis
+        by presburger
       have "col X Y Z" if "C \<in> line_ext (line E F)"
         using P_def \<open>P = C \<Longrightarrow> col X Y Z\<close> \<open>line B C \<noteq> line E F\<close> incidB_lAB line_ext_def that uniq_inter 
         by auto 
       have "col X Y Z" if "A \<in> line_ext (line D E)"
         by (metis Q_def \<open>Q = A \<Longrightarrow> col X Y Z\<close> \<open>line B A \<noteq> line D E\<close> 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 \<open>P = W \<Longrightarrow> col X Y Z\<close> \<open>distinct6 B A C D E F\<close> ax_uniqueness 
+        by (metis P_def W_def \<open>P = W \<Longrightarrow> col X Y Z\<close> \<open>distinct [B,A,C,D,E,F]\<close> 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 \<notin> line_ext (line E F)" and "A \<notin> line_ext (line D E)" and "line B C \<noteq> 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 \<open>A = W \<Longrightarrow> col X Y Z\<close> \<open>line A C \<noteq> line E F\<close> inter_ABC_1 inter_comm that)
       have "col X Y Z" if "A \<in> line_ext (line C D)"
         using R_def \<open>R = A \<Longrightarrow> col X Y Z\<close> \<open>line C D \<noteq> line A F\<close> 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 \<open>P = W \<Longrightarrow> col X Y Z\<close> that)
           (* We resume the general case *)
       have f3:"inter (line P W) (line A R) = F" if "line E F \<noteq> line A F" and "A \<notin> line_ext (line C D)"
         and "inter (line B C) (line E F) \<noteq> 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 \<in> AF, then 
             we resume the general case *)
       have "col X Y Z" if "C \<in> line_ext (line A F)"
         using R_def \<open>R = C \<Longrightarrow> col X Y Z\<close> \<open>line C D \<noteq> line A F\<close> 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 \<notin> 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) \<in> line_ext (line B F)" if "distinct6 P Q R A C W"
+      then have "inter (line Q W) (line C D) \<in> line_ext (line B F)" if "distinct [P,Q,R,A,C,W]"
         and  "C \<notin> line_ext (line E F)" and "A \<notin> line_ext (line D E)" and "line B C \<noteq> line A B"
         and "line E F \<noteq> line A F" and "A \<notin> line_ext (line C D)"
         and "inter (line B C) (line E F) \<noteq> inter (line A C) (line E F)"
-        by (smt R_def \<open>distinct6 B A C D E F\<close> ax_uniqueness col_line_ext_1 distinct6_def f1 f2 f3 
+        by (smt R_def \<open>distinct [B,A,C,D,E,F]\<close> 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"
+      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 \<notin> line_ext (line E F)" and "A \<notin> line_ext (line D E)" and "line B C \<noteq> line A B"
         and "line E F \<noteq> line A F" and "A \<notin> line_ext (line C D)"
         and "inter (line B C) (line E F) \<noteq> inter (line A C) (line E F)"
-        by (smt W_def \<open>distinct6 B A C D E F\<close> \<open>line C D \<noteq> line B F\<close> ax_uniqueness distinct6_def f2 
+        by (smt W_def \<open>distinct [B,A,C,D,E,F]\<close> \<open>line C D \<noteq> line B F\<close> 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) \<in> line_ext (line Q W)" if "distinct6 P Q R A C W"
+      moreover have "inter (line C D) (line B F) \<in> line_ext (line Q W)" if "distinct [P,Q,R,A,C,W]"
         and  "C \<notin> line_ext (line E F)" and "A \<notin> line_ext (line D E)" and "line B C \<noteq> line A B"
         and "line E F \<noteq> line A F" and "A \<notin> line_ext (line C D)"
         and "inter (line B C) (line E F) \<noteq> 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"
+      (inter (line A B) (line D E))" if "distinct [P,Q,R,A,C,W]"
         and  "C \<notin> line_ext (line E F)" and "A \<notin> line_ext (line D E)" and "line B C \<noteq> line A B"
         and "line E F \<noteq> line A F" and "A \<notin> line_ext (line C D)"
         and "inter (line B C) (line E F) \<noteq> 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 \<open>A = W \<Longrightarrow> col X Y Z\<close> \<open>A \<in> line_ext (line C D) \<Longrightarrow> col X Y Z\<close> 
             \<open>A \<in> line_ext (line D E) \<Longrightarrow> col X Y Z\<close> \<open>C = W \<Longrightarrow> col X Y Z\<close> \<open>C \<in> line_ext (line E F) \<Longrightarrow> col X Y Z\<close> 
             \<open>P = A \<Longrightarrow> col X Y Z\<close> \<open>P = C \<Longrightarrow> col X Y Z\<close> \<open>P = Q \<Longrightarrow> col X Y Z\<close> \<open>P = R \<Longrightarrow> col X Y Z\<close> 
-            \<open>Pascal_Property.inter (line B C) (line E F) = Pascal_Property.inter (line A C) (line E F) \<Longrightarrow> col X Y Z\<close> 
+            \<open>inter (line B C) (line E F) = inter (line A C) (line E F) \<Longrightarrow> col X Y Z\<close> 
             \<open>Q = A \<Longrightarrow> col X Y Z\<close> \<open>Q = C \<Longrightarrow> col X Y Z\<close> \<open>Q = R \<Longrightarrow> col X Y Z\<close> \<open>Q = W \<Longrightarrow> col X Y Z\<close> \<open>R = A \<Longrightarrow> col X Y Z\<close> 
-            \<open>R = C \<Longrightarrow> col X Y Z\<close> \<open>R = W \<Longrightarrow> col X Y Z\<close> \<open>\<lbrakk>distinct6 P Q R A C W; C \<notin> line_ext (line E F); A \<notin> line_ext (line D E); line B C \<noteq> line A B; line E F \<noteq> line A F; A \<notin> line_ext (line C D); Pascal_Property.inter (line B C) (line E F) \<noteq> Pascal_Property.inter (line A C) (line E F)\<rbrakk> \<Longrightarrow> 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))\<close> 
+            \<open>R = C \<Longrightarrow> col X Y Z\<close> \<open>R = W \<Longrightarrow> col X Y Z\<close> \<open>\<lbrakk>distinct [P,Q,R,A,C,W]; C \<notin> line_ext (line E F); A \<notin> line_ext (line D E); line B C \<noteq> line A B; line E F \<noteq> line A F; A \<notin> line_ext (line C D); inter (line B C) (line E F) \<noteq> inter (line A C) (line E F)\<rbrakk> \<Longrightarrow> col (inter (line A C) (line E F)) (inter (line C D) (line B F)) (inter (line A B) (line D E))\<close> 
             \<open>line B C = line A B \<Longrightarrow> col X Y Z\<close> \<open>line E F = line A F \<Longrightarrow> col X Y Z\<close> distinct6_def line_comm)
      qed
      show "is_pascal B A C D E F"
-       using X_def Y_def Z_def \<open>\<lbrakk>distinct6 B A C D E F; line A C \<noteq> line E F; line C D \<noteq> line B F; line B A \<noteq> line D E; line B C = line E F\<rbrakk> \<Longrightarrow> col X Y Z\<close> 
-         \<open>\<lbrakk>distinct6 B A C D E F; line A C \<noteq> line E F; line C D \<noteq> line B F; line B A \<noteq> line D E; line B C \<noteq> line E F; line C D \<noteq> line A F\<rbrakk> \<Longrightarrow> col X Y Z\<close> 
-         \<open>\<lbrakk>distinct6 B A C D E F; line A C \<noteq> line E F; line C D \<noteq> line B F; line B A \<noteq> line D E; line C D = line A F\<rbrakk> \<Longrightarrow> col X Y Z\<close> 
+       using X_def Y_def Z_def \<open>\<lbrakk>distinct [B,A,C,D,E,F]; line A C \<noteq> line E F; line C D \<noteq> line B F; line B A \<noteq> line D E; line B C = line E F\<rbrakk> \<Longrightarrow> col X Y Z\<close> 
+         \<open>\<lbrakk>distinct [B,A,C,D,E,F]; line A C \<noteq> line E F; line C D \<noteq> line B F; line B A \<noteq> line D E; line B C \<noteq> line E F; line C D \<noteq> line A F\<rbrakk> \<Longrightarrow> col X Y Z\<close> 
+         \<open>\<lbrakk>distinct [B,A,C,D,E,F]; line A C \<noteq> line E F; line C D \<noteq> line B F; line B A \<noteq> line D E; line C D = line A F\<rbrakk> \<Longrightarrow> col X Y Z\<close> 
          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"
+  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 = distinct6 A B C A' B' C'"  and "a2 = col A B C" and 
+  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: \<open>\<lbrakk>a1; a2; a3; a4; a5; a6\<rbrakk> \<Longrightarrow> col P Q R\<close> 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"
+  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
 
 
 
 
+
diff --git a/thys/Projective_Geometry/Projective_Plane_Axioms.thy b/thys/Projective_Geometry/Projective_Plane_Axioms.thy
--- a/thys/Projective_Geometry/Projective_Plane_Axioms.thy
+++ b/thys/Projective_Geometry/Projective_Plane_Axioms.thy
@@ -1,51 +1,48 @@
 theory Projective_Plane_Axioms
   imports Main
 begin
 
-(* Author: Anthony Bordg, University of Cambridge, apdb3@cam.ac.uk .*)
+(* Author: Anthony Bordg, University of Cambridge, apdb3@cam.ac.uk. *) 
+
+(* Update: In 2021, Niels Mündler, from the Technical University of Munich, kindly updated the formalization
+to replace axiomatizations by locales. *)
 
 text \<open>
 Contents:
-\<^item> We introduce the types of points and lines and an incidence relation between them.
-\<^item> A set of axioms for the projective plane (the models of these axioms are 
-n-dimensional with n \<open>\<ge>\<close> 2). 
+\begin{itemize}
+\item We introduce the types of points and lines and an incidence relation between them.
+\item A set of axioms for the projective plane (the models of these axioms are
+n-dimensional with $n\ge 2$).
+\end{itemize}
 \<close>
 
 section \<open>The Axioms of the Projective Plane\<close>
 
-(* 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 \<Rightarrow> Lines \<Rightarrow> bool"
-
-(* Ax1: Any two (distinct) points lie on a (unique) line *)
-axiomatization where
-ax1: "\<exists>l. incid P l \<and> incid Q l"
 
-(* Ax2: Any two (distinct) lines meet in a (unique) point *)
-axiomatization where
-ax2: "\<exists>P. incid P l \<and> incid P m"
-
-(* The uniqueness part *)
-axiomatization where
-ax_uniqueness: "incid P l \<longrightarrow> incid Q l \<longrightarrow> incid P m \<longrightarrow> incid Q m \<longrightarrow> P = Q \<or> l = m"
+locale projective_plane =
+  (* One has a type of points *)
+  (* One has a type of lines *)
+  (* One has an incidence relation between points and lines *)
+  (* which is all expressed in the following line *)
+  fixes incid :: "'point \<Rightarrow> 'line \<Rightarrow> bool"
 
-definition distinct4 :: "Points \<Rightarrow> Points \<Rightarrow> Points \<Rightarrow> Points \<Rightarrow> bool" where
-"distinct4 A B C D \<equiv> (A \<noteq> B) \<and> (A \<noteq> C) \<and> (A \<noteq> D) \<and> (B \<noteq> C) \<and> (B \<noteq> D) \<and> (C \<noteq> D)"
+  (* Ax1: Any two (distinct) points lie on a (unique) line *)
+  assumes ax1: "\<exists>l. incid P l \<and> incid Q l"
 
-(* Ax3: There exists four points such that no three of them are collinear *)
-axiomatization where 
-ax3: "\<exists>A B C D. distinct4 A B C D \<and> (\<forall>l. 
-(incid A l \<and> incid B l \<longrightarrow> \<not>(incid C l) \<and> \<not>(incid D l)) \<and>
-(incid A l \<and> incid C l \<longrightarrow> \<not>(incid B l) \<and> \<not>(incid D l)) \<and>
-(incid A l \<and> incid D l \<longrightarrow> \<not>(incid B l) \<and> \<not>(incid C l)) \<and>
-(incid B l \<and> incid C l \<longrightarrow> \<not>(incid A l) \<and> \<not>(incid D l)) \<and>
-(incid B l \<and> incid D l \<longrightarrow> \<not>(incid A l) \<and> \<not>(incid C l)) \<and>
-(incid C l \<and> incid D l \<longrightarrow> \<not>(incid A l) \<and> \<not>(incid B l)))"
+  (* Ax2: Any two (distinct) lines meet in a (unique) point *)
+  assumes ax2: "\<exists>P. incid P l \<and> incid P m"
+
+  (* The uniqueness part *)
+  assumes ax_uniqueness: "\<lbrakk>incid P l; incid Q l; incid P m; incid Q m\<rbrakk> \<Longrightarrow>  P = Q \<or> l = m"
+
+  (* Ax3: There exists four points such that no three of them are collinear *)
+  assumes ax3: "\<exists>A B C D. distinct [A,B,C,D] \<and> (\<forall>l.
+              (incid A l \<and> incid B l \<longrightarrow> \<not>(incid C l) \<and> \<not>(incid D l)) \<and>
+              (incid A l \<and> incid C l \<longrightarrow> \<not>(incid B l) \<and> \<not>(incid D l)) \<and>
+              (incid A l \<and> incid D l \<longrightarrow> \<not>(incid B l) \<and> \<not>(incid C l)) \<and>
+              (incid B l \<and> incid C l \<longrightarrow> \<not>(incid A l) \<and> \<not>(incid D l)) \<and>
+              (incid B l \<and> incid D l \<longrightarrow> \<not>(incid A l) \<and> \<not>(incid C l)) \<and>
+              (incid C l \<and> incid D l \<longrightarrow> \<not>(incid A l) \<and> \<not>(incid B l)))"
 
 
-end
\ No newline at end of file
+end
diff --git a/thys/Projective_Geometry/Projective_Space_Axioms.thy b/thys/Projective_Geometry/Projective_Space_Axioms.thy
--- a/thys/Projective_Geometry/Projective_Space_Axioms.thy
+++ b/thys/Projective_Geometry/Projective_Space_Axioms.thy
@@ -1,81 +1,71 @@
 theory Projective_Space_Axioms
   imports Main
 begin
 
-(* Author: Anthony Bordg, University of Cambridge, apdb3@cam.ac.uk .*)
+(* Author: Anthony Bordg, University of Cambridge, apdb3@cam.ac.uk *)
 
 text \<open>
 Contents:
-\<^item> We introduce the types of points and lines and an incidence relation between them.
+\<^item> We introduce the types @{typ 'point} of points and @{typ 'line} of lines and an incidence relation 
+between them.
 \<^item> 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  
 \<close>
 
 section \<open>The axioms of the Projective Space\<close>
 
-(* 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 \<Rightarrow> lines \<Rightarrow> bool"
-
-axiomatization where
-(* The relation of incidence is decidable *)
-incid_dec: "(incid P l) \<or> \<not>(incid P l)"
-
-axiomatization where
-(* Ax1: Any two distinct points are incident with just one line *)
-ax1_existence: "\<exists>l. (incid P l) \<and> (incid M l)"
-axiomatization where
-ax1_uniqueness: "(incid P k) \<longrightarrow> (incid M k) \<longrightarrow> (incid P l) \<longrightarrow> (incid M l) \<longrightarrow> (P = M) \<or> (k = l)"
-
-definition distinct4 :: "points \<Rightarrow> points \<Rightarrow> points \<Rightarrow> points \<Rightarrow> bool" where
-"distinct4 A B C D \<equiv> (A \<noteq> B) \<and> (A \<noteq> C) \<and> (A \<noteq> D)\<and> (B \<noteq> C) \<and> (B \<noteq> D) \<and> (C \<noteq> D)"
+lemma distinct4_def:
+"distinct [A,B,C,D] = ((A \<noteq> B) \<and> (A \<noteq> C) \<and> (A \<noteq> D)\<and> (B \<noteq> C) \<and> (B \<noteq> D) \<and> (C \<noteq> D))"
+  by auto
 
-(* 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 \<longrightarrow> (incid A lAB \<and> incid B lAB) 
-\<longrightarrow> (incid C lCD \<and> incid D lCD) \<longrightarrow> (incid A lAC \<and> incid C lAC) \<longrightarrow> 
-(incid B lBD \<and> incid D lBD) \<longrightarrow> (\<exists>I.(incid I lAB \<and> incid I lCD)) \<longrightarrow> 
-(\<exists>J.(incid J lAC \<and> incid J lBD))"
-
-definition distinct3 :: "points => points => points => bool" where
-"distinct3 A B C \<equiv> (A \<noteq> B) \<and> (A \<noteq> C) \<and> (B \<noteq> C)"
+lemma distinct3_def:
+  "distinct [A, B, C] = (A \<noteq> B \<and> A \<noteq> C \<and> B \<noteq> C)"
+  by auto
 
-(** 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: "\<exists>A B C. distinct3 A B C \<and> (incid A l) \<and> (incid B l) \<and> (incid C l)"
-
-(* Ax4: There exists two lines that do not meet, 
-hence the geometry is at least 3-dimensional *)
-axiomatization where
-ax4: "\<exists>l m.\<forall>P. \<not>(incid P l \<and> incid P m)"
+locale projective_space =
+  (* One has a type of 'point *)
+  (* We don't need an axiom for the existence of at least one point, 
+  since we know that the type "'point" is not empty  
+  TODO: why would that be true? *)
+  (* One has a type of 'line *)
+  (* There is a relation of incidence between 'point and 'line *)
+  fixes incid :: "'point \<Rightarrow> 'line \<Rightarrow> bool"
+  fixes meet :: "'line \<Rightarrow> 'line \<Rightarrow> 'point"
+  assumes meet_def:  "(incid (meet l m) l \<and> incid (meet l m) m)"
 
-definition meet :: "lines \<Rightarrow> lines \<Rightarrow> bool" where
-"meet l m \<equiv> \<exists>P. (incid P l \<and> incid P m)"
-
-definition meet_in :: "lines \<Rightarrow> lines \<Rightarrow> points \<Rightarrow> bool" where
-"meet_in l m P \<equiv> incid P l \<and> incid P m"
+  (* The relation of incidence is decidable *)
+  assumes incid_dec: "(incid P l) \<or> \<not>(incid P l)"
 
-definition distinct3_line :: "lines \<Rightarrow> lines \<Rightarrow> lines \<Rightarrow> bool" where
-"distinct3_line l m n \<equiv> (l \<noteq> m) \<and> (l \<noteq> n) \<and> (m \<noteq> n)"
+  (* Ax1: Any two distinct 'point are incident with just one line *)
+  assumes ax1_existence: "\<exists>l. (incid P l) \<and> (incid M l)"
+  assumes ax1_uniqueness: "(incid P k) \<longrightarrow> (incid M k) \<longrightarrow> (incid P l) \<longrightarrow> (incid M l) \<longrightarrow> (P = M) \<or> (k = l)"
 
-(* Ax5: The geometry is not 4-dimensional, hence it is exactly 3-dimensional *)
-axiomatization where
-ax5: "distinct3_line l1 l2 l3 \<longrightarrow> (\<exists>l4 J1 J2 J3. distinct3 J1 J2 J3 \<and> 
-meet_in l1 l4 J1 \<and> meet_in l2 l4 J2 \<and> meet_in l3 l4 J3)"
+
+  (* Ax2: If A B C D are four distinct 'point 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. *)
+  assumes ax2: "distinct [A,B,C,D] \<longrightarrow> (incid A lAB \<and> incid B lAB) 
+  \<longrightarrow> (incid C lCD \<and> incid D lCD) \<longrightarrow> (incid A lAC \<and> incid C lAC) \<longrightarrow> 
+  (incid B lBD \<and> incid D lBD) \<longrightarrow> (\<exists>I.(incid I lAB \<and> incid I lCD)) \<longrightarrow> 
+  (\<exists>J.(incid J lAC \<and> incid J lBD))"
+
+
+
+  (** 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 'point
+  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. *)
+  assumes ax3: "\<exists>A B C. distinct3 A B C \<and> (incid A l) \<and> (incid B l) \<and> (incid C l)"
+
+  (* Ax4: There exists two Lines that do not meet, 
+  hence the geometry is at least 3-dimensional *)
+  assumes ax4: "\<exists>l m.\<forall>P. \<not>(incid P l \<and> incid P m)"
+
+
+  (* Ax5: The geometry is not 4-dimensional, hence it is exactly 3-dimensional *)
+  assumes ax5: "distinct [l1,l2,l3] \<longrightarrow> (\<exists>l4 J1 J2 J3. distinct [J1,J2,J3] \<and> 
+  meet l1 l4 = J1 \<and> meet l2 l4 = J2 \<and> meet l3 l4 = J3)"
 
 
 end
\ No newline at end of file