(* Title: HOL/Examples/Coherent.thy
Author: Stefan Berghofer, TU Muenchen
Author: Marc Bezem, Institutt for Informatikk, Universitetet i Bergen
*)
section \<open>Coherent Logic Problems\<close>
theory Coherent
imports Main
begin
subsection \<open>Equivalence of two versions of Pappus' Axiom\<close>
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 \<Longrightarrow> col E F G H \<Longrightarrow> col B G I J \<Longrightarrow> col C F I K \<Longrightarrow>
col B E L M \<Longrightarrow> col A F L N \<Longrightarrow> col C E O P \<Longrightarrow> col A G O Q \<Longrightarrow>
(\<exists> R. col I L O R) \<or> pl A H \<or> pl B H \<or> pl C H \<or> pl E D \<or> pl F D \<or> 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 \<Longrightarrow> col D E F K \<Longrightarrow> col B F G L \<Longrightarrow> col C E G M \<Longrightarrow>
col B D H N \<Longrightarrow> col A E H O \<Longrightarrow> col C D I P \<Longrightarrow> col A F I Q \<Longrightarrow>
(\<exists> R. col G H I R) \<or> el L M \<or> el N O \<or> 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 \<open>Preservation of the Diamond Property under reflexive closure\<close>
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
¤ Dauer der Verarbeitung: 0.18 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
