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