author | haftmann |
Fri, 20 Oct 2017 20:57:55 +0200 | |
changeset 66888 | 930abfdf8727 |
parent 63054 | 1b237d147cc4 |
permissions | -rw-r--r-- |
32734 | 1 |
(* Title: HOL/ex/Coherent.thy |
28323 | 2 |
Author: Stefan Berghofer, TU Muenchen |
32734 | 3 |
Author: Marc Bezem, Institutt for Informatikk, Universitetet i Bergen |
28323 | 4 |
*) |
5 |
||
61343 | 6 |
section \<open>Coherent Logic Problems\<close> |
28323 | 7 |
|
32734 | 8 |
theory Coherent |
9 |
imports Main |
|
10 |
begin |
|
28323 | 11 |
|
61343 | 12 |
subsection \<open>Equivalence of two versions of Pappus' Axiom\<close> |
28323 | 13 |
|
14 |
no_notation |
|
15 |
comp (infixl "o" 55) and |
|
47433
07f4bf913230
renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
griff
parents:
32734
diff
changeset
|
16 |
relcomp (infixr "O" 75) |
28323 | 17 |
|
18 |
lemma p1p2: |
|
63054 | 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" |
|
28323 | 44 |
shows goal using assms |
45 |
by coherent |
|
46 |
||
47 |
lemma p2p1: |
|
63054 | 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" |
|
28323 | 76 |
shows goal using assms |
77 |
by coherent |
|
78 |
||
79 |
||
61343 | 80 |
subsection \<open>Preservation of the Diamond Property under reflexive closure\<close> |
28323 | 81 |
|
82 |
lemma diamond: |
|
63054 | 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" |
|
28323 | 92 |
shows goal using assms |
93 |
by coherent |
|
94 |
||
95 |
end |