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