src/HOL/ex/Coherent.thy
author wenzelm
Wed Jun 22 10:09:20 2016 +0200 (2016-06-22)
changeset 63343 fb5d8a50c641
parent 63054 1b237d147cc4
permissions -rw-r--r--
bundle lifting_syntax;
     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 section \<open>Coherent Logic Problems\<close>
     7 
     8 theory Coherent
     9 imports Main
    10 begin
    11 
    12 subsection \<open>Equivalence of two versions of Pappus' Axiom\<close>
    13 
    14 no_notation
    15   comp (infixl "o" 55) and
    16   relcomp (infixr "O" 75)
    17 
    18 lemma 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 
    47 lemma 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 
    80 subsection \<open>Preservation of the Diamond Property under reflexive closure\<close>
    81 
    82 lemma 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 
    95 end