Quelle  Coherent.thy   Sprache: Isabelle

(*  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)
unbundle no relcomp_syntax

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