src/Sequents/LK/prop.ML
author wenzelm
Sun Sep 18 15:20:08 2005 +0200 (2005-09-18)
changeset 17481 75166ebb619b
parent 6252 935f183bf406
permissions -rw-r--r--
converted to Isar theory format;
wenzelm@6252
     1
(*  Title:      LK/ex/prop
wenzelm@6252
     2
    ID:         $Id$
wenzelm@6252
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
wenzelm@6252
     4
    Copyright   1992  University of Cambridge
wenzelm@6252
     5
wenzelm@6252
     6
Classical sequent calculus: examples with propositional connectives
wenzelm@6252
     7
Can be read to test the LK system.
wenzelm@6252
     8
*)
wenzelm@6252
     9
wenzelm@6252
    10
writeln"absorptive laws of & and | ";
wenzelm@6252
    11
wenzelm@17481
    12
goal (theory "LK") "|- P & P <-> P";
wenzelm@6252
    13
by (fast_tac prop_pack 1);
wenzelm@6252
    14
result();
wenzelm@6252
    15
wenzelm@17481
    16
goal (theory "LK") "|- P | P <-> P";
wenzelm@6252
    17
by (fast_tac prop_pack 1);
wenzelm@6252
    18
result();
wenzelm@6252
    19
wenzelm@6252
    20
writeln"commutative laws of & and | ";
wenzelm@6252
    21
wenzelm@17481
    22
goal (theory "LK") "|- P & Q  <->  Q & P";
wenzelm@6252
    23
by (fast_tac prop_pack 1);
wenzelm@6252
    24
result();
wenzelm@6252
    25
wenzelm@17481
    26
goal (theory "LK") "|- P | Q  <->  Q | P";
wenzelm@6252
    27
by (fast_tac prop_pack 1);
wenzelm@6252
    28
result();
wenzelm@6252
    29
wenzelm@6252
    30
wenzelm@6252
    31
writeln"associative laws of & and | ";
wenzelm@6252
    32
wenzelm@17481
    33
goal (theory "LK") "|- (P & Q) & R  <->  P & (Q & R)";
wenzelm@6252
    34
by (fast_tac prop_pack 1);
wenzelm@6252
    35
result();
wenzelm@6252
    36
wenzelm@17481
    37
goal (theory "LK") "|- (P | Q) | R  <->  P | (Q | R)";
wenzelm@6252
    38
by (fast_tac prop_pack 1);
wenzelm@6252
    39
result();
wenzelm@6252
    40
wenzelm@6252
    41
writeln"distributive laws of & and | ";
wenzelm@17481
    42
goal (theory "LK") "|- (P & Q) | R  <-> (P | R) & (Q | R)";
wenzelm@6252
    43
by (fast_tac prop_pack 1);
wenzelm@6252
    44
result();
wenzelm@6252
    45
wenzelm@17481
    46
goal (theory "LK") "|- (P | Q) & R  <-> (P & R) | (Q & R)";
wenzelm@6252
    47
by (fast_tac prop_pack 1);
wenzelm@6252
    48
result();
wenzelm@6252
    49
wenzelm@6252
    50
writeln"Laws involving implication";
wenzelm@6252
    51
wenzelm@17481
    52
goal (theory "LK") "|- (P|Q --> R) <-> (P-->R) & (Q-->R)";
wenzelm@6252
    53
by (fast_tac prop_pack 1);
wenzelm@6252
    54
result(); 
wenzelm@6252
    55
wenzelm@17481
    56
goal (theory "LK") "|- (P & Q --> R) <-> (P--> (Q-->R))";
wenzelm@6252
    57
by (fast_tac prop_pack 1);
wenzelm@6252
    58
result(); 
wenzelm@6252
    59
wenzelm@6252
    60
wenzelm@17481
    61
goal (theory "LK") "|- (P --> Q & R) <-> (P-->Q)  &  (P-->R)";
wenzelm@6252
    62
by (fast_tac prop_pack 1);
wenzelm@6252
    63
result();
wenzelm@6252
    64
wenzelm@6252
    65
wenzelm@6252
    66
writeln"Classical theorems";
wenzelm@6252
    67
wenzelm@17481
    68
goal (theory "LK") "|- P|Q --> P| ~P&Q";
wenzelm@6252
    69
by (fast_tac prop_pack 1);
wenzelm@6252
    70
result();
wenzelm@6252
    71
wenzelm@6252
    72
wenzelm@17481
    73
goal (theory "LK") "|- (P-->Q)&(~P-->R)  -->  (P&Q | R)";
wenzelm@6252
    74
by (fast_tac prop_pack 1);
wenzelm@6252
    75
result();
wenzelm@6252
    76
wenzelm@6252
    77
wenzelm@17481
    78
goal (theory "LK") "|- P&Q | ~P&R  <->  (P-->Q)&(~P-->R)";
wenzelm@6252
    79
by (fast_tac prop_pack 1);
wenzelm@6252
    80
result();
wenzelm@6252
    81
wenzelm@6252
    82
wenzelm@17481
    83
goal (theory "LK") "|- (P-->Q) | (P-->R)  <->  (P --> Q | R)";
wenzelm@6252
    84
by (fast_tac prop_pack 1);
wenzelm@6252
    85
result();
wenzelm@6252
    86
wenzelm@6252
    87
wenzelm@6252
    88
(*If and only if*)
wenzelm@6252
    89
wenzelm@17481
    90
goal (theory "LK") "|- (P<->Q) <-> (Q<->P)";
wenzelm@6252
    91
by (fast_tac prop_pack 1);
wenzelm@6252
    92
result();
wenzelm@6252
    93
wenzelm@17481
    94
goal (theory "LK") "|- ~ (P <-> ~P)";
wenzelm@6252
    95
by (fast_tac prop_pack 1);
wenzelm@6252
    96
result();
wenzelm@6252
    97
wenzelm@6252
    98
wenzelm@6252
    99
(*Sample problems from 
wenzelm@6252
   100
  F. J. Pelletier, 
wenzelm@6252
   101
  Seventy-Five Problems for Testing Automatic Theorem Provers,
wenzelm@6252
   102
  J. Automated Reasoning 2 (1986), 191-216.
wenzelm@6252
   103
  Errata, JAR 4 (1988), 236-236.
wenzelm@6252
   104
*)
wenzelm@6252
   105
wenzelm@6252
   106
(*1*)
wenzelm@17481
   107
goal (theory "LK") "|- (P-->Q)  <->  (~Q --> ~P)";
wenzelm@6252
   108
by (fast_tac prop_pack 1);
wenzelm@6252
   109
result();
wenzelm@6252
   110
wenzelm@6252
   111
(*2*)
wenzelm@17481
   112
goal (theory "LK") "|- ~ ~ P  <->  P";
wenzelm@6252
   113
by (fast_tac prop_pack 1);
wenzelm@6252
   114
result();
wenzelm@6252
   115
wenzelm@6252
   116
(*3*)
wenzelm@17481
   117
goal (theory "LK") "|- ~(P-->Q) --> (Q-->P)";
wenzelm@6252
   118
by (fast_tac prop_pack 1);
wenzelm@6252
   119
result();
wenzelm@6252
   120
wenzelm@6252
   121
(*4*)
wenzelm@17481
   122
goal (theory "LK") "|- (~P-->Q)  <->  (~Q --> P)";
wenzelm@6252
   123
by (fast_tac prop_pack 1);
wenzelm@6252
   124
result();
wenzelm@6252
   125
wenzelm@6252
   126
(*5*)
wenzelm@17481
   127
goal (theory "LK") "|- ((P|Q)-->(P|R)) --> (P|(Q-->R))";
wenzelm@6252
   128
by (fast_tac prop_pack 1);
wenzelm@6252
   129
result();
wenzelm@6252
   130
wenzelm@6252
   131
(*6*)
wenzelm@17481
   132
goal (theory "LK") "|- P | ~ P";
wenzelm@6252
   133
by (fast_tac prop_pack 1);
wenzelm@6252
   134
result();
wenzelm@6252
   135
wenzelm@6252
   136
(*7*)
wenzelm@17481
   137
goal (theory "LK") "|- P | ~ ~ ~ P";
wenzelm@6252
   138
by (fast_tac prop_pack 1);
wenzelm@6252
   139
result();
wenzelm@6252
   140
wenzelm@6252
   141
(*8.  Peirce's law*)
wenzelm@17481
   142
goal (theory "LK") "|- ((P-->Q) --> P)  -->  P";
wenzelm@6252
   143
by (fast_tac prop_pack 1);
wenzelm@6252
   144
result();
wenzelm@6252
   145
wenzelm@6252
   146
(*9*)
wenzelm@17481
   147
goal (theory "LK") "|- ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
wenzelm@6252
   148
by (fast_tac prop_pack 1);
wenzelm@6252
   149
result();
wenzelm@6252
   150
wenzelm@6252
   151
(*10*)
wenzelm@17481
   152
goal (theory "LK") "Q-->R, R-->P&Q, P-->(Q|R) |- P<->Q";
wenzelm@6252
   153
by (fast_tac prop_pack 1);
wenzelm@6252
   154
result();
wenzelm@6252
   155
wenzelm@6252
   156
(*11.  Proved in each direction (incorrectly, says Pelletier!!)  *)
wenzelm@17481
   157
goal (theory "LK") "|- P<->P";
wenzelm@6252
   158
by (fast_tac prop_pack 1);
wenzelm@6252
   159
result();
wenzelm@6252
   160
wenzelm@6252
   161
(*12.  "Dijkstra's law"*)
wenzelm@17481
   162
goal (theory "LK") "|- ((P <-> Q) <-> R)  <->  (P <-> (Q <-> R))";
wenzelm@6252
   163
by (fast_tac prop_pack 1);
wenzelm@6252
   164
result();
wenzelm@6252
   165
wenzelm@6252
   166
(*13.  Distributive law*)
wenzelm@17481
   167
goal (theory "LK") "|- P | (Q & R)  <-> (P | Q) & (P | R)";
wenzelm@6252
   168
by (fast_tac prop_pack 1);
wenzelm@6252
   169
result();
wenzelm@6252
   170
wenzelm@6252
   171
(*14*)
wenzelm@17481
   172
goal (theory "LK") "|- (P <-> Q) <-> ((Q | ~P) & (~Q|P))";
wenzelm@6252
   173
by (fast_tac prop_pack 1);
wenzelm@6252
   174
result();
wenzelm@6252
   175
wenzelm@6252
   176
wenzelm@6252
   177
(*15*)
wenzelm@17481
   178
goal (theory "LK") "|- (P --> Q) <-> (~P | Q)";
wenzelm@6252
   179
by (fast_tac prop_pack 1);
wenzelm@6252
   180
result();
wenzelm@6252
   181
wenzelm@6252
   182
(*16*)
wenzelm@17481
   183
goal (theory "LK") "|- (P-->Q) | (Q-->P)";
wenzelm@6252
   184
by (fast_tac prop_pack 1);
wenzelm@6252
   185
result();
wenzelm@6252
   186
wenzelm@6252
   187
(*17*)
wenzelm@17481
   188
goal (theory "LK") "|- ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))";
wenzelm@6252
   189
by (fast_tac prop_pack 1);
wenzelm@6252
   190
result();