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