Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Coherent.thy Sprache: Isabelle

Original von: Isabelle^©

(*  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.1 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.