section ‹Coherent Logic Problems›
theory Coherent
imports Main
begin
subsection ‹Equivalence of two versions of Pappus' Axiom›
no_notation
comp (infixl "o" 55) and
relcomp (infixr "O" 75)
lemma p1p2:
assumes "col a b c l ∧ col d e f m"
and "col b f g n ∧ col c e g o"
and "col b d h p ∧ col a e h q"
and "col c d i r ∧ col a f i s"
and "el n o ⟹ goal"
and "el p q ⟹ goal"
and "el s r ⟹ goal"
and "⋀A. el A A ⟹ pl g A ⟹ pl h A ⟹ pl i A ⟹ goal"
and "⋀A B C D. col A B C D ⟹ pl A D"
and "⋀A B C D. col A B C D ⟹ pl B D"
and "⋀A B C D. col A B C D ⟹ pl C D"
and "⋀A B. pl A B ⟹ ep A A"
and "⋀A B. ep A B ⟹ ep B A"
and "⋀A B C. ep A B ⟹ ep B C ⟹ ep A C"
and "⋀A B. pl A B ⟹ el B B"
and "⋀A B. el A B ⟹ el B A"
and "⋀A B C. el A B ⟹ el B C ⟹ el A C"
and "⋀A B C. ep A B ⟹ pl B C ⟹ pl A C"
and "⋀A B C. pl A B ⟹ el B C ⟹ pl A C"
and "⋀A B C D E F G H I J K L M N O P Q.
col A B C D ⟹ col E F G H ⟹ col B G I J ⟹ col C F I K ⟹
col B E L M ⟹ col A F L N ⟹ col C E O P ⟹ col A G O Q ⟹
(∃ R. col I L O R) ∨ pl A H ∨ pl B H ∨ pl C H ∨ pl E D ∨ pl F D ∨ pl G D"
and "⋀A B C D. pl A B ⟹ pl A C ⟹ pl D B ⟹ pl D C ⟹ ep A D ∨ el B C"
and "⋀A B. ep A A ⟹ ep B B ⟹ ∃C. pl A C ∧ pl B C"
shows goal using assms
by coherent
lemma p2p1:
assumes "col a b c l ∧ col d e f m"
and "col b f g n ∧ col c e g o"
and "col b d h p ∧ col a e h q"
and "col c d i r ∧ col a f i s"
and "pl a m ⟹ goal"
and "pl b m ⟹ goal"
and "pl c m ⟹ goal"
and "pl d l ⟹ goal"
and "pl e l ⟹ goal"
and "pl f l ⟹ goal"
and "⋀A. pl g A ⟹ pl h A ⟹ pl i A ⟹ goal"
and "⋀A B C D. col A B C D ⟹ pl A D"
and "⋀A B C D. col A B C D ⟹ pl B D"
and "⋀A B C D. col A B C D ⟹ pl C D"
and "⋀A B. pl A B ⟹ ep A A"
and "⋀A B. ep A B ⟹ ep B A"
and "⋀A B C. ep A B ⟹ ep B C ⟹ ep A C"
and "⋀A B. pl A B ⟹ el B B"
and "⋀A B. el A B ⟹ el B A"
and "⋀A B C. el A B ⟹ el B C ⟹ el A C"
and "⋀A B C. ep A B ⟹ pl B C ⟹ pl A C"
and "⋀A B C. pl A B ⟹ el B C ⟹ pl A C"
and "⋀A B C D E F G H I J K L M N O P Q.
col A B C J ⟹ col D E F K ⟹ col B F G L ⟹ col C E G M ⟹
col B D H N ⟹ col A E H O ⟹ col C D I P ⟹ col A F I Q ⟹
(∃ R. col G H I R) ∨ el L M ∨ el N O ∨ el P Q"
and "⋀A B C D. pl C A ⟹ pl C B ⟹ pl D A ⟹ pl D B ⟹ ep C D ∨ el A B"
and "⋀A B C. ep A A ⟹ ep B B ⟹ ∃C. pl A C ∧ pl B C"
shows goal using assms
by coherent
subsection ‹Preservation of the Diamond Property under reflexive closure›
lemma diamond:
assumes "reflexive_rewrite a b" "reflexive_rewrite a c"
and "⋀A. reflexive_rewrite b A ⟹ reflexive_rewrite c A ⟹ goal"
and "⋀A. equalish A A"
and "⋀A B. equalish A B ⟹ equalish B A"
and "⋀A B C. equalish A B ⟹ reflexive_rewrite B C ⟹ reflexive_rewrite A C"
and "⋀A B. equalish A B ⟹ reflexive_rewrite A B"
and "⋀A B. rewrite A B ⟹ reflexive_rewrite A B"
and "⋀A B. reflexive_rewrite A B ⟹ equalish A B ∨ rewrite A B"
and "⋀A B C. rewrite A B ⟹ rewrite A C ⟹ ∃D. rewrite B D ∧ rewrite C D"
shows goal using assms
by coherent
end