Theory Coherent

(*  Title:      HOL/Examples/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"
    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