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