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