src/LK/ex/prop.ML
changeset 0 a5a9c433f639
child 1461 6bcb44e4d6e5
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/LK/ex/prop.ML	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,194 @@
     1.4 +(*  Title: 	LK/ex/prop
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1992  University of Cambridge
     1.8 +
     1.9 +Classical sequent calculus: examples with propositional connectives
    1.10 +Can be read to test the LK system.
    1.11 +*)
    1.12 +
    1.13 +writeln"LK/ex/prop: propositional examples";
    1.14 +
    1.15 +writeln"absorptive laws of & and | ";
    1.16 +
    1.17 +goal LK.thy "|- P & P <-> P";
    1.18 +by (fast_tac prop_pack 1);
    1.19 +result();
    1.20 +
    1.21 +goal LK.thy "|- P | P <-> P";
    1.22 +by (fast_tac prop_pack 1);
    1.23 +result();
    1.24 +
    1.25 +writeln"commutative laws of & and | ";
    1.26 +
    1.27 +goal LK.thy "|- P & Q  <->  Q & P";
    1.28 +by (fast_tac prop_pack 1);
    1.29 +result();
    1.30 +
    1.31 +goal LK.thy "|- P | Q  <->  Q | P";
    1.32 +by (fast_tac prop_pack 1);
    1.33 +result();
    1.34 +
    1.35 +
    1.36 +writeln"associative laws of & and | ";
    1.37 +
    1.38 +goal LK.thy "|- (P & Q) & R  <->  P & (Q & R)";
    1.39 +by (fast_tac prop_pack 1);
    1.40 +result();
    1.41 +
    1.42 +goal LK.thy "|- (P | Q) | R  <->  P | (Q | R)";
    1.43 +by (fast_tac prop_pack 1);
    1.44 +result();
    1.45 +
    1.46 +writeln"distributive laws of & and | ";
    1.47 +goal LK.thy "|- (P & Q) | R  <-> (P | R) & (Q | R)";
    1.48 +by (fast_tac prop_pack 1);
    1.49 +result();
    1.50 +
    1.51 +goal LK.thy "|- (P | Q) & R  <-> (P & R) | (Q & R)";
    1.52 +by (fast_tac prop_pack 1);
    1.53 +result();
    1.54 +
    1.55 +writeln"Laws involving implication";
    1.56 +
    1.57 +goal LK.thy "|- (P|Q --> R) <-> (P-->R) & (Q-->R)";
    1.58 +by (fast_tac prop_pack 1);
    1.59 +result(); 
    1.60 +
    1.61 +goal LK.thy "|- (P & Q --> R) <-> (P--> (Q-->R))";
    1.62 +by (fast_tac prop_pack 1);
    1.63 +result(); 
    1.64 +
    1.65 +
    1.66 +goal LK.thy "|- (P --> Q & R) <-> (P-->Q)  &  (P-->R)";
    1.67 +by (fast_tac prop_pack 1);
    1.68 +result();
    1.69 +
    1.70 +
    1.71 +writeln"Classical theorems";
    1.72 +
    1.73 +goal LK.thy "|- P|Q --> P| ~P&Q";
    1.74 +by (fast_tac prop_pack 1);
    1.75 +result();
    1.76 +
    1.77 +
    1.78 +goal LK.thy "|- (P-->Q)&(~P-->R)  -->  (P&Q | R)";
    1.79 +by (fast_tac prop_pack 1);
    1.80 +result();
    1.81 +
    1.82 +
    1.83 +goal LK.thy "|- P&Q | ~P&R  <->  (P-->Q)&(~P-->R)";
    1.84 +by (fast_tac prop_pack 1);
    1.85 +result();
    1.86 +
    1.87 +
    1.88 +goal LK.thy "|- (P-->Q) | (P-->R)  <->  (P --> Q | R)";
    1.89 +by (fast_tac prop_pack 1);
    1.90 +result();
    1.91 +
    1.92 +
    1.93 +(*If and only if*)
    1.94 +
    1.95 +goal LK.thy "|- (P<->Q) <-> (Q<->P)";
    1.96 +by (fast_tac prop_pack 1);
    1.97 +result();
    1.98 +
    1.99 +goal LK.thy "|- ~ (P <-> ~P)";
   1.100 +by (fast_tac prop_pack 1);
   1.101 +result();
   1.102 +
   1.103 +
   1.104 +(*Sample problems from 
   1.105 +  F. J. Pelletier, 
   1.106 +  Seventy-Five Problems for Testing Automatic Theorem Provers,
   1.107 +  J. Automated Reasoning 2 (1986), 191-216.
   1.108 +  Errata, JAR 4 (1988), 236-236.
   1.109 +*)
   1.110 +
   1.111 +(*1*)
   1.112 +goal LK.thy "|- (P-->Q)  <->  (~Q --> ~P)";
   1.113 +by (fast_tac prop_pack 1);
   1.114 +result();
   1.115 +
   1.116 +(*2*)
   1.117 +goal LK.thy "|- ~ ~ P  <->  P";
   1.118 +by (fast_tac prop_pack 1);
   1.119 +result();
   1.120 +
   1.121 +(*3*)
   1.122 +goal LK.thy "|- ~(P-->Q) --> (Q-->P)";
   1.123 +by (fast_tac prop_pack 1);
   1.124 +result();
   1.125 +
   1.126 +(*4*)
   1.127 +goal LK.thy "|- (~P-->Q)  <->  (~Q --> P)";
   1.128 +by (fast_tac prop_pack 1);
   1.129 +result();
   1.130 +
   1.131 +(*5*)
   1.132 +goal LK.thy "|- ((P|Q)-->(P|R)) --> (P|(Q-->R))";
   1.133 +by (fast_tac prop_pack 1);
   1.134 +result();
   1.135 +
   1.136 +(*6*)
   1.137 +goal LK.thy "|- P | ~ P";
   1.138 +by (fast_tac prop_pack 1);
   1.139 +result();
   1.140 +
   1.141 +(*7*)
   1.142 +goal LK.thy "|- P | ~ ~ ~ P";
   1.143 +by (fast_tac prop_pack 1);
   1.144 +result();
   1.145 +
   1.146 +(*8.  Peirce's law*)
   1.147 +goal LK.thy "|- ((P-->Q) --> P)  -->  P";
   1.148 +by (fast_tac prop_pack 1);
   1.149 +result();
   1.150 +
   1.151 +(*9*)
   1.152 +goal LK.thy "|- ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
   1.153 +by (fast_tac prop_pack 1);
   1.154 +result();
   1.155 +
   1.156 +(*10*)
   1.157 +goal LK.thy "Q-->R, R-->P&Q, P-->(Q|R) |- P<->Q";
   1.158 +by (fast_tac prop_pack 1);
   1.159 +result();
   1.160 +
   1.161 +(*11.  Proved in each direction (incorrectly, says Pelletier!!)  *)
   1.162 +goal LK.thy "|- P<->P";
   1.163 +by (fast_tac prop_pack 1);
   1.164 +result();
   1.165 +
   1.166 +(*12.  "Dijkstra's law"*)
   1.167 +goal LK.thy "|- ((P <-> Q) <-> R)  <->  (P <-> (Q <-> R))";
   1.168 +by (fast_tac prop_pack 1);
   1.169 +result();
   1.170 +
   1.171 +(*13.  Distributive law*)
   1.172 +goal LK.thy "|- P | (Q & R)  <-> (P | Q) & (P | R)";
   1.173 +by (fast_tac prop_pack 1);
   1.174 +result();
   1.175 +
   1.176 +(*14*)
   1.177 +goal LK.thy "|- (P <-> Q) <-> ((Q | ~P) & (~Q|P))";
   1.178 +by (fast_tac prop_pack 1);
   1.179 +result();
   1.180 +
   1.181 +
   1.182 +(*15*)
   1.183 +goal LK.thy "|- (P --> Q) <-> (~P | Q)";
   1.184 +by (fast_tac prop_pack 1);
   1.185 +result();
   1.186 +
   1.187 +(*16*)
   1.188 +goal LK.thy "|- (P-->Q) | (Q-->P)";
   1.189 +by (fast_tac prop_pack 1);
   1.190 +result();
   1.191 +
   1.192 +(*17*)
   1.193 +goal LK.thy "|- ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))";
   1.194 +by (fast_tac prop_pack 1);
   1.195 +result();
   1.196 +
   1.197 +writeln"Reached end of file.";