Theory Coherent

theory Coherent
imports Main
(*  Title:      HOL/ex/Coherent.thy
    Author:     Stefan Berghofer, TU Muenchen
    Author:     Marc Bezem, Institutt for Informatikk, Universitetet i Bergen 
*)

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"
  "col b f g n ∧ col c e g o"
  "col b d h p ∧ col a e h q"
  "col c d i r ∧ col a f i s"
  "el n o ⟹ goal"
  "el p q ⟹ goal"
  "el s r ⟹ goal"
  "⋀A. el A A ⟹ pl g A ⟹ pl h A ⟹ pl i A ⟹ goal"
  "⋀A B C D. col A B C D ⟹ pl A D"
  "⋀A B C D. col A B C D ⟹ pl B D"
  "⋀A B C D. col A B C D ⟹ pl C D"
  "⋀A B. pl A B ⟹ ep A A"
  "⋀A B. ep A B ⟹ ep B A"
  "⋀A B C. ep A B ⟹ ep B C ⟹ ep A C"
  "⋀A B. pl A B ⟹ el B B"
  "⋀A B. el A B ⟹ el B A"
  "⋀A B C. el A B ⟹ el B C ⟹ el A C"
  "⋀A B C. ep A B ⟹ pl B C ⟹ pl A C"
  "⋀A B C. pl A B ⟹ el B C ⟹ pl A C"
  "⋀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"
  "⋀A B C D. pl A B ⟹ pl A C ⟹ pl D B ⟹ pl D C ⟹ ep A D ∨ el B C"
  "⋀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"
  "col b f g n ∧ col c e g o"
  "col b d h p ∧ col a e h q"
  "col c d i r ∧ col a f i s"
  "pl a m ⟹ goal"
  "pl b m ⟹ goal"
  "pl c m ⟹ goal"
  "pl d l ⟹ goal"
  "pl e l ⟹ goal"
  "pl f l ⟹ goal"
  "⋀A. pl g A ⟹ pl h A ⟹ pl i A ⟹ goal"
  "⋀A B C D. col A B C D ⟹ pl A D"
  "⋀A B C D. col A B C D ⟹ pl B D"
  "⋀A B C D. col A B C D ⟹ pl C D"
  "⋀A B. pl A B ⟹ ep A A"
  "⋀A B. ep A B ⟹ ep B A"
  "⋀A B C. ep A B ⟹ ep B C ⟹ ep A C"
  "⋀A B. pl A B ⟹ el B B"
  "⋀A B. el A B ⟹ el B A"
  "⋀A B C. el A B ⟹ el B C ⟹ el A C"
  "⋀A B C. ep A B ⟹ pl B C ⟹ pl A C"
  "⋀A B C. pl A B ⟹ el B C ⟹ pl A C"
  "⋀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"
  "⋀A B C D. pl C A ⟹ pl C B ⟹ pl D A ⟹ pl D B ⟹ ep C D ∨ el A B"
  "⋀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"
  "⋀A. reflexive_rewrite b A ⟹ reflexive_rewrite c A ⟹ goal"
  "⋀A. equalish A A" 
  "⋀A B. equalish A B ⟹ equalish B A"
  "⋀A B C. equalish A B ⟹ reflexive_rewrite B C ⟹ reflexive_rewrite A C"
  "⋀A B. equalish A B ⟹ reflexive_rewrite A B"
  "⋀A B. rewrite A B ⟹ reflexive_rewrite A B"
  "⋀A B. reflexive_rewrite A B ⟹ equalish A B ∨ rewrite A B"
  "⋀A B C. rewrite A B ⟹ rewrite A C ⟹ ∃D. rewrite B D ∧ rewrite C D"
  shows goal using assms
  by coherent

end