src/Sequents/LK/Propositional.thy
author wenzelm
Mon, 20 Nov 2006 23:47:10 +0100
changeset 21426 87ac12bed1ab
child 35762 af3ff2ba4c54
permissions -rw-r--r--
converted legacy ML scripts;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
21426
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
     1
(*  Title:      LK/Propositional.thy
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
     4
    Copyright   1992  University of Cambridge
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
     5
*)
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
     6
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
     7
header {* Classical sequent calculus: examples with propositional connectives *}
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
     8
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
     9
theory Propositional
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    10
imports LK
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    11
begin
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    12
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    13
text "absorptive laws of & and | "
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    14
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    15
lemma "|- P & P <-> P"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    16
  by fast_prop
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    17
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    18
lemma "|- P | P <-> P"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    19
  by fast_prop
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    20
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    21
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    22
text "commutative laws of & and | "
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    23
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    24
lemma "|- P & Q  <->  Q & P"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    25
  by fast_prop
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    26
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    27
lemma "|- P | Q  <->  Q | P"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    28
  by fast_prop
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    29
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    30
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    31
text "associative laws of & and | "
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    32
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    33
lemma "|- (P & Q) & R  <->  P & (Q & R)"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    34
  by fast_prop
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    35
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    36
lemma "|- (P | Q) | R  <->  P | (Q | R)"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    37
  by fast_prop
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    38
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    39
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    40
text "distributive laws of & and | "
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    41
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    42
lemma "|- (P & Q) | R  <-> (P | R) & (Q | R)"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    43
  by fast_prop
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    44
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    45
lemma "|- (P | Q) & R  <-> (P & R) | (Q & R)"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    46
  by fast_prop
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    47
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    48
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    49
text "Laws involving implication"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    50
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    51
lemma "|- (P|Q --> R) <-> (P-->R) & (Q-->R)"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    52
  by fast_prop
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    53
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    54
lemma "|- (P & Q --> R) <-> (P--> (Q-->R))"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    55
  by fast_prop
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    56
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    57
lemma "|- (P --> Q & R) <-> (P-->Q)  &  (P-->R)"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    58
  by fast_prop
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    59
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    60
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    61
text "Classical theorems"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    62
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    63
lemma "|- P|Q --> P| ~P&Q"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    64
  by fast_prop
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    65
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    66
lemma "|- (P-->Q)&(~P-->R)  -->  (P&Q | R)"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    67
  by fast_prop
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    68
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    69
lemma "|- P&Q | ~P&R  <->  (P-->Q)&(~P-->R)"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    70
  by fast_prop
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    71
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    72
lemma "|- (P-->Q) | (P-->R)  <->  (P --> Q | R)"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    73
  by fast_prop
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    74
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    75
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    76
(*If and only if*)
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    77
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    78
lemma "|- (P<->Q) <-> (Q<->P)"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    79
  by fast_prop
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    80
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    81
lemma "|- ~ (P <-> ~P)"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    82
  by fast_prop
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    83
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    84
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    85
(*Sample problems from 
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    86
  F. J. Pelletier, 
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    87
  Seventy-Five Problems for Testing Automatic Theorem Provers,
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    88
  J. Automated Reasoning 2 (1986), 191-216.
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    89
  Errata, JAR 4 (1988), 236-236.
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    90
*)
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    91
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    92
(*1*)
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    93
lemma "|- (P-->Q)  <->  (~Q --> ~P)"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    94
  by fast_prop
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    95
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    96
(*2*)
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    97
lemma "|- ~ ~ P  <->  P"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    98
  by fast_prop
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
    99
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   100
(*3*)
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   101
lemma "|- ~(P-->Q) --> (Q-->P)"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   102
  by fast_prop
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   103
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   104
(*4*)
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   105
lemma "|- (~P-->Q)  <->  (~Q --> P)"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   106
  by fast_prop
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   107
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   108
(*5*)
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   109
lemma "|- ((P|Q)-->(P|R)) --> (P|(Q-->R))"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   110
  by fast_prop
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   111
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   112
(*6*)
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   113
lemma "|- P | ~ P"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   114
  by fast_prop
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   115
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   116
(*7*)
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   117
lemma "|- P | ~ ~ ~ P"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   118
  by fast_prop
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   119
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   120
(*8.  Peirce's law*)
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   121
lemma "|- ((P-->Q) --> P)  -->  P"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   122
  by fast_prop
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   123
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   124
(*9*)
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   125
lemma "|- ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   126
  by fast_prop
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   127
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   128
(*10*)
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   129
lemma "Q-->R, R-->P&Q, P-->(Q|R) |- P<->Q"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   130
  by fast_prop
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   131
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   132
(*11.  Proved in each direction (incorrectly, says Pelletier!!)  *)
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   133
lemma "|- P<->P"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   134
  by fast_prop
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   135
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   136
(*12.  "Dijkstra's law"*)
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   137
lemma "|- ((P <-> Q) <-> R)  <->  (P <-> (Q <-> R))"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   138
  by fast_prop
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   139
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   140
(*13.  Distributive law*)
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   141
lemma "|- P | (Q & R)  <-> (P | Q) & (P | R)"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   142
  by fast_prop
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   143
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   144
(*14*)
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   145
lemma "|- (P <-> Q) <-> ((Q | ~P) & (~Q|P))"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   146
  by fast_prop
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   147
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   148
(*15*)
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   149
lemma "|- (P --> Q) <-> (~P | Q)"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   150
  by fast_prop
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   151
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   152
(*16*)
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   153
lemma "|- (P-->Q) | (Q-->P)"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   154
  by fast_prop
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   155
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   156
(*17*)
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   157
lemma "|- ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))"
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   158
  by fast_prop
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   159
87ac12bed1ab converted legacy ML scripts;
wenzelm
parents:
diff changeset
   160
end