1(* Title: HOL/ex/Coherent.thy 2 Author: Stefan Berghofer, TU Muenchen 3 Author: Marc Bezem, Institutt for Informatikk, Universitetet i Bergen 4*) 5 6section \<open>Coherent Logic Problems\<close> 7 8theory Coherent 9imports Main 10begin 11 12subsection \<open>Equivalence of two versions of Pappus' Axiom\<close> 13 14no_notation 15 comp (infixl "o" 55) and 16 relcomp (infixr "O" 75) 17 18lemma p1p2: 19 assumes "col a b c l \<and> col d e f m" 20 and "col b f g n \<and> col c e g o" 21 and "col b d h p \<and> col a e h q" 22 and "col c d i r \<and> col a f i s" 23 and "el n o \<Longrightarrow> goal" 24 and "el p q \<Longrightarrow> goal" 25 and "el s r \<Longrightarrow> goal" 26 and "\<And>A. el A A \<Longrightarrow> pl g A \<Longrightarrow> pl h A \<Longrightarrow> pl i A \<Longrightarrow> goal" 27 and "\<And>A B C D. col A B C D \<Longrightarrow> pl A D" 28 and "\<And>A B C D. col A B C D \<Longrightarrow> pl B D" 29 and "\<And>A B C D. col A B C D \<Longrightarrow> pl C D" 30 and "\<And>A B. pl A B \<Longrightarrow> ep A A" 31 and "\<And>A B. ep A B \<Longrightarrow> ep B A" 32 and "\<And>A B C. ep A B \<Longrightarrow> ep B C \<Longrightarrow> ep A C" 33 and "\<And>A B. pl A B \<Longrightarrow> el B B" 34 and "\<And>A B. el A B \<Longrightarrow> el B A" 35 and "\<And>A B C. el A B \<Longrightarrow> el B C \<Longrightarrow> el A C" 36 and "\<And>A B C. ep A B \<Longrightarrow> pl B C \<Longrightarrow> pl A C" 37 and "\<And>A B C. pl A B \<Longrightarrow> el B C \<Longrightarrow> pl A C" 38 and "\<And>A B C D E F G H I J K L M N O P Q. 39 col A B C D \<Longrightarrow> col E F G H \<Longrightarrow> col B G I J \<Longrightarrow> col C F I K \<Longrightarrow> 40 col B E L M \<Longrightarrow> col A F L N \<Longrightarrow> col C E O P \<Longrightarrow> col A G O Q \<Longrightarrow> 41 (\<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" 42 and "\<And>A B C D. pl A B \<Longrightarrow> pl A C \<Longrightarrow> pl D B \<Longrightarrow> pl D C \<Longrightarrow> ep A D \<or> el B C" 43 and "\<And>A B. ep A A \<Longrightarrow> ep B B \<Longrightarrow> \<exists>C. pl A C \<and> pl B C" 44 shows goal using assms 45 by coherent 46 47lemma p2p1: 48 assumes "col a b c l \<and> col d e f m" 49 and "col b f g n \<and> col c e g o" 50 and "col b d h p \<and> col a e h q" 51 and "col c d i r \<and> col a f i s" 52 and "pl a m \<Longrightarrow> goal" 53 and "pl b m \<Longrightarrow> goal" 54 and "pl c m \<Longrightarrow> goal" 55 and "pl d l \<Longrightarrow> goal" 56 and "pl e l \<Longrightarrow> goal" 57 and "pl f l \<Longrightarrow> goal" 58 and "\<And>A. pl g A \<Longrightarrow> pl h A \<Longrightarrow> pl i A \<Longrightarrow> goal" 59 and "\<And>A B C D. col A B C D \<Longrightarrow> pl A D" 60 and "\<And>A B C D. col A B C D \<Longrightarrow> pl B D" 61 and "\<And>A B C D. col A B C D \<Longrightarrow> pl C D" 62 and "\<And>A B. pl A B \<Longrightarrow> ep A A" 63 and "\<And>A B. ep A B \<Longrightarrow> ep B A" 64 and "\<And>A B C. ep A B \<Longrightarrow> ep B C \<Longrightarrow> ep A C" 65 and "\<And>A B. pl A B \<Longrightarrow> el B B" 66 and "\<And>A B. el A B \<Longrightarrow> el B A" 67 and "\<And>A B C. el A B \<Longrightarrow> el B C \<Longrightarrow> el A C" 68 and "\<And>A B C. ep A B \<Longrightarrow> pl B C \<Longrightarrow> pl A C" 69 and "\<And>A B C. pl A B \<Longrightarrow> el B C \<Longrightarrow> pl A C" 70 and "\<And>A B C D E F G H I J K L M N O P Q. 71 col A B C J \<Longrightarrow> col D E F K \<Longrightarrow> col B F G L \<Longrightarrow> col C E G M \<Longrightarrow> 72 col B D H N \<Longrightarrow> col A E H O \<Longrightarrow> col C D I P \<Longrightarrow> col A F I Q \<Longrightarrow> 73 (\<exists> R. col G H I R) \<or> el L M \<or> el N O \<or> el P Q" 74 and "\<And>A B C D. pl C A \<Longrightarrow> pl C B \<Longrightarrow> pl D A \<Longrightarrow> pl D B \<Longrightarrow> ep C D \<or> el A B" 75 and "\<And>A B C. ep A A \<Longrightarrow> ep B B \<Longrightarrow> \<exists>C. pl A C \<and> pl B C" 76 shows goal using assms 77 by coherent 78 79 80subsection \<open>Preservation of the Diamond Property under reflexive closure\<close> 81 82lemma diamond: 83 assumes "reflexive_rewrite a b" "reflexive_rewrite a c" 84 and "\<And>A. reflexive_rewrite b A \<Longrightarrow> reflexive_rewrite c A \<Longrightarrow> goal" 85 and "\<And>A. equalish A A" 86 and "\<And>A B. equalish A B \<Longrightarrow> equalish B A" 87 and "\<And>A B C. equalish A B \<Longrightarrow> reflexive_rewrite B C \<Longrightarrow> reflexive_rewrite A C" 88 and "\<And>A B. equalish A B \<Longrightarrow> reflexive_rewrite A B" 89 and "\<And>A B. rewrite A B \<Longrightarrow> reflexive_rewrite A B" 90 and "\<And>A B. reflexive_rewrite A B \<Longrightarrow> equalish A B \<or> rewrite A B" 91 and "\<And>A B C. rewrite A B \<Longrightarrow> rewrite A C \<Longrightarrow> \<exists>D. rewrite B D \<and> rewrite C D" 92 shows goal using assms 93 by coherent 94 95end 96