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 
*)

header {* 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