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