src/HOL/ex/Coherent.thy
author griff
Tue, 03 Apr 2012 17:26:30 +0900
changeset 47433 07f4bf913230
parent 32734 06c13b2e562e
child 58889 5b7a9633cfa8
permissions -rw-r--r--
renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
32734
06c13b2e562e misc tuning and modernization;
wenzelm
parents: 28323
diff changeset
     1
(*  Title:      HOL/ex/Coherent.thy
28323
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
     2
    Author:     Stefan Berghofer, TU Muenchen
32734
06c13b2e562e misc tuning and modernization;
wenzelm
parents: 28323
diff changeset
     3
    Author:     Marc Bezem, Institutt for Informatikk, Universitetet i Bergen 
28323
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
     4
*)
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
     5
32734
06c13b2e562e misc tuning and modernization;
wenzelm
parents: 28323
diff changeset
     6
header {* Coherent Logic Problems *}
28323
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
     7
32734
06c13b2e562e misc tuning and modernization;
wenzelm
parents: 28323
diff changeset
     8
theory Coherent
06c13b2e562e misc tuning and modernization;
wenzelm
parents: 28323
diff changeset
     9
imports Main
06c13b2e562e misc tuning and modernization;
wenzelm
parents: 28323
diff changeset
    10
begin
28323
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    11
32734
06c13b2e562e misc tuning and modernization;
wenzelm
parents: 28323
diff changeset
    12
subsection {* Equivalence of two versions of Pappus' Axiom *}
28323
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    13
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    14
no_notation
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    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
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    17
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    18
lemma p1p2:
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    19
  assumes
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    20
  "col a b c l \<and> col d e f m"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    21
  "col b f g n \<and> col c e g o"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    22
  "col b d h p \<and> col a e h q"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    23
  "col c d i r \<and> col a f i s"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    24
  "el n o \<Longrightarrow> goal"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    25
  "el p q \<Longrightarrow> goal"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    26
  "el s r \<Longrightarrow> goal"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    27
  "\<And>A. el A A \<Longrightarrow> pl g A \<Longrightarrow> pl h A \<Longrightarrow> pl i A \<Longrightarrow> goal"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    28
  "\<And>A B C D. col A B C D \<Longrightarrow> pl A D"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    29
  "\<And>A B C D. col A B C D \<Longrightarrow> pl B D"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    30
  "\<And>A B C D. col A B C D \<Longrightarrow> pl C D"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    31
  "\<And>A B. pl A B \<Longrightarrow> ep A A"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    32
  "\<And>A B. ep A B \<Longrightarrow> ep B A"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    33
  "\<And>A B C. ep A B \<Longrightarrow> ep B C \<Longrightarrow> ep A C"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    34
  "\<And>A B. pl A B \<Longrightarrow> el B B"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    35
  "\<And>A B. el A B \<Longrightarrow> el B A"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    36
  "\<And>A B C. el A B \<Longrightarrow> el B C \<Longrightarrow> el A C"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    37
  "\<And>A B C. ep A B \<Longrightarrow> pl B C \<Longrightarrow> pl A C"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    38
  "\<And>A B C. pl A B \<Longrightarrow> el B C \<Longrightarrow> pl A C"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    39
  "\<And>A B C D E F G H I J K L M N O P Q.
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    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>
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    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>
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    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"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    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"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    44
  "\<And>A B. ep A A \<Longrightarrow> ep B B \<Longrightarrow> \<exists>C. pl A C \<and> pl B C"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    45
  shows goal using assms
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    46
  by coherent
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    47
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    48
lemma p2p1:
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    49
  assumes
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    50
  "col a b c l \<and> col d e f m"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    51
  "col b f g n \<and> col c e g o"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    52
  "col b d h p \<and> col a e h q"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    53
  "col c d i r \<and> col a f i s"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    54
  "pl a m \<Longrightarrow> goal"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    55
  "pl b m \<Longrightarrow> goal"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    56
  "pl c m \<Longrightarrow> goal"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    57
  "pl d l \<Longrightarrow> goal"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    58
  "pl e l \<Longrightarrow> goal"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    59
  "pl f l \<Longrightarrow> goal"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    60
  "\<And>A. pl g A \<Longrightarrow> pl h A \<Longrightarrow> pl i A \<Longrightarrow> goal"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    61
  "\<And>A B C D. col A B C D \<Longrightarrow> pl A D"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    62
  "\<And>A B C D. col A B C D \<Longrightarrow> pl B D"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    63
  "\<And>A B C D. col A B C D \<Longrightarrow> pl C D"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    64
  "\<And>A B. pl A B \<Longrightarrow> ep A A"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    65
  "\<And>A B. ep A B \<Longrightarrow> ep B A"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    66
  "\<And>A B C. ep A B \<Longrightarrow> ep B C \<Longrightarrow> ep A C"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    67
  "\<And>A B. pl A B \<Longrightarrow> el B B"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    68
  "\<And>A B. el A B \<Longrightarrow> el B A"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    69
  "\<And>A B C. el A B \<Longrightarrow> el B C \<Longrightarrow> el A C"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    70
  "\<And>A B C. ep A B \<Longrightarrow> pl B C \<Longrightarrow> pl A C"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    71
  "\<And>A B C. pl A B \<Longrightarrow> el B C \<Longrightarrow> pl A C"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    72
  "\<And>A B C D E F G H I J K L M N O P Q.
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    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>
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    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>
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    75
     (\<exists> R. col G H I R) \<or> el L M \<or> el N O \<or> el P Q"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    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"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    77
  "\<And>A B C. ep A A \<Longrightarrow> ep B B \<Longrightarrow> \<exists>C. pl A C \<and> pl B C"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    78
  shows goal using assms
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    79
  by coherent
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    80
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    81
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    82
subsection {* Preservation of the Diamond Property under reflexive closure *}
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    83
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    84
lemma diamond:
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    85
  assumes
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    86
  "reflexive_rewrite a b" "reflexive_rewrite a c"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    87
  "\<And>A. reflexive_rewrite b A \<Longrightarrow> reflexive_rewrite c A \<Longrightarrow> goal"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    88
  "\<And>A. equalish A A" 
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    89
  "\<And>A B. equalish A B \<Longrightarrow> equalish B A"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    90
  "\<And>A B C. equalish A B \<Longrightarrow> reflexive_rewrite B C \<Longrightarrow> reflexive_rewrite A C"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    91
  "\<And>A B. equalish A B \<Longrightarrow> reflexive_rewrite A B"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    92
  "\<And>A B. rewrite A B \<Longrightarrow> reflexive_rewrite A B"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    93
  "\<And>A B. reflexive_rewrite A B \<Longrightarrow> equalish A B \<or> rewrite A B"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    94
  "\<And>A B C. rewrite A B \<Longrightarrow> rewrite A C \<Longrightarrow> \<exists>D. rewrite B D \<and> rewrite C D"
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    95
  shows goal using assms
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    96
  by coherent
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    97
8f12f7275637 Examples for coherent logic prover.
berghofe
parents:
diff changeset
    98
end