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