src/Sequents/LK/prop.ML
changeset 17481 75166ebb619b
parent 6252 935f183bf406
     1.1 --- a/src/Sequents/LK/prop.ML	Sun Sep 18 14:25:48 2005 +0200
     1.2 +++ b/src/Sequents/LK/prop.ML	Sun Sep 18 15:20:08 2005 +0200
     1.3 @@ -7,93 +7,91 @@
     1.4  Can be read to test the LK system.
     1.5  *)
     1.6  
     1.7 -writeln"LK/ex/prop: propositional examples";
     1.8 -
     1.9  writeln"absorptive laws of & and | ";
    1.10  
    1.11 -goal LK.thy "|- P & P <-> P";
    1.12 +goal (theory "LK") "|- P & P <-> P";
    1.13  by (fast_tac prop_pack 1);
    1.14  result();
    1.15  
    1.16 -goal LK.thy "|- P | P <-> P";
    1.17 +goal (theory "LK") "|- P | P <-> P";
    1.18  by (fast_tac prop_pack 1);
    1.19  result();
    1.20  
    1.21  writeln"commutative laws of & and | ";
    1.22  
    1.23 -goal LK.thy "|- P & Q  <->  Q & P";
    1.24 +goal (theory "LK") "|- P & Q  <->  Q & P";
    1.25  by (fast_tac prop_pack 1);
    1.26  result();
    1.27  
    1.28 -goal LK.thy "|- P | Q  <->  Q | P";
    1.29 +goal (theory "LK") "|- P | Q  <->  Q | P";
    1.30  by (fast_tac prop_pack 1);
    1.31  result();
    1.32  
    1.33  
    1.34  writeln"associative laws of & and | ";
    1.35  
    1.36 -goal LK.thy "|- (P & Q) & R  <->  P & (Q & R)";
    1.37 +goal (theory "LK") "|- (P & Q) & R  <->  P & (Q & R)";
    1.38  by (fast_tac prop_pack 1);
    1.39  result();
    1.40  
    1.41 -goal LK.thy "|- (P | Q) | R  <->  P | (Q | R)";
    1.42 +goal (theory "LK") "|- (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 +goal (theory "LK") "|- (P & Q) | R  <-> (P | R) & (Q | R)";
    1.49  by (fast_tac prop_pack 1);
    1.50  result();
    1.51  
    1.52 -goal LK.thy "|- (P | Q) & R  <-> (P & R) | (Q & R)";
    1.53 +goal (theory "LK") "|- (P | Q) & R  <-> (P & R) | (Q & R)";
    1.54  by (fast_tac prop_pack 1);
    1.55  result();
    1.56  
    1.57  writeln"Laws involving implication";
    1.58  
    1.59 -goal LK.thy "|- (P|Q --> R) <-> (P-->R) & (Q-->R)";
    1.60 +goal (theory "LK") "|- (P|Q --> R) <-> (P-->R) & (Q-->R)";
    1.61  by (fast_tac prop_pack 1);
    1.62  result(); 
    1.63  
    1.64 -goal LK.thy "|- (P & Q --> R) <-> (P--> (Q-->R))";
    1.65 +goal (theory "LK") "|- (P & Q --> R) <-> (P--> (Q-->R))";
    1.66  by (fast_tac prop_pack 1);
    1.67  result(); 
    1.68  
    1.69  
    1.70 -goal LK.thy "|- (P --> Q & R) <-> (P-->Q)  &  (P-->R)";
    1.71 +goal (theory "LK") "|- (P --> Q & R) <-> (P-->Q)  &  (P-->R)";
    1.72  by (fast_tac prop_pack 1);
    1.73  result();
    1.74  
    1.75  
    1.76  writeln"Classical theorems";
    1.77  
    1.78 -goal LK.thy "|- P|Q --> P| ~P&Q";
    1.79 +goal (theory "LK") "|- P|Q --> P| ~P&Q";
    1.80  by (fast_tac prop_pack 1);
    1.81  result();
    1.82  
    1.83  
    1.84 -goal LK.thy "|- (P-->Q)&(~P-->R)  -->  (P&Q | R)";
    1.85 +goal (theory "LK") "|- (P-->Q)&(~P-->R)  -->  (P&Q | R)";
    1.86  by (fast_tac prop_pack 1);
    1.87  result();
    1.88  
    1.89  
    1.90 -goal LK.thy "|- P&Q | ~P&R  <->  (P-->Q)&(~P-->R)";
    1.91 +goal (theory "LK") "|- P&Q | ~P&R  <->  (P-->Q)&(~P-->R)";
    1.92  by (fast_tac prop_pack 1);
    1.93  result();
    1.94  
    1.95  
    1.96 -goal LK.thy "|- (P-->Q) | (P-->R)  <->  (P --> Q | R)";
    1.97 +goal (theory "LK") "|- (P-->Q) | (P-->R)  <->  (P --> Q | R)";
    1.98  by (fast_tac prop_pack 1);
    1.99  result();
   1.100  
   1.101  
   1.102  (*If and only if*)
   1.103  
   1.104 -goal LK.thy "|- (P<->Q) <-> (Q<->P)";
   1.105 +goal (theory "LK") "|- (P<->Q) <-> (Q<->P)";
   1.106  by (fast_tac prop_pack 1);
   1.107  result();
   1.108  
   1.109 -goal LK.thy "|- ~ (P <-> ~P)";
   1.110 +goal (theory "LK") "|- ~ (P <-> ~P)";
   1.111  by (fast_tac prop_pack 1);
   1.112  result();
   1.113  
   1.114 @@ -106,89 +104,87 @@
   1.115  *)
   1.116  
   1.117  (*1*)
   1.118 -goal LK.thy "|- (P-->Q)  <->  (~Q --> ~P)";
   1.119 +goal (theory "LK") "|- (P-->Q)  <->  (~Q --> ~P)";
   1.120  by (fast_tac prop_pack 1);
   1.121  result();
   1.122  
   1.123  (*2*)
   1.124 -goal LK.thy "|- ~ ~ P  <->  P";
   1.125 +goal (theory "LK") "|- ~ ~ P  <->  P";
   1.126  by (fast_tac prop_pack 1);
   1.127  result();
   1.128  
   1.129  (*3*)
   1.130 -goal LK.thy "|- ~(P-->Q) --> (Q-->P)";
   1.131 +goal (theory "LK") "|- ~(P-->Q) --> (Q-->P)";
   1.132  by (fast_tac prop_pack 1);
   1.133  result();
   1.134  
   1.135  (*4*)
   1.136 -goal LK.thy "|- (~P-->Q)  <->  (~Q --> P)";
   1.137 +goal (theory "LK") "|- (~P-->Q)  <->  (~Q --> P)";
   1.138  by (fast_tac prop_pack 1);
   1.139  result();
   1.140  
   1.141  (*5*)
   1.142 -goal LK.thy "|- ((P|Q)-->(P|R)) --> (P|(Q-->R))";
   1.143 +goal (theory "LK") "|- ((P|Q)-->(P|R)) --> (P|(Q-->R))";
   1.144  by (fast_tac prop_pack 1);
   1.145  result();
   1.146  
   1.147  (*6*)
   1.148 -goal LK.thy "|- P | ~ P";
   1.149 +goal (theory "LK") "|- P | ~ P";
   1.150  by (fast_tac prop_pack 1);
   1.151  result();
   1.152  
   1.153  (*7*)
   1.154 -goal LK.thy "|- P | ~ ~ ~ P";
   1.155 +goal (theory "LK") "|- P | ~ ~ ~ P";
   1.156  by (fast_tac prop_pack 1);
   1.157  result();
   1.158  
   1.159  (*8.  Peirce's law*)
   1.160 -goal LK.thy "|- ((P-->Q) --> P)  -->  P";
   1.161 +goal (theory "LK") "|- ((P-->Q) --> P)  -->  P";
   1.162  by (fast_tac prop_pack 1);
   1.163  result();
   1.164  
   1.165  (*9*)
   1.166 -goal LK.thy "|- ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
   1.167 +goal (theory "LK") "|- ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
   1.168  by (fast_tac prop_pack 1);
   1.169  result();
   1.170  
   1.171  (*10*)
   1.172 -goal LK.thy "Q-->R, R-->P&Q, P-->(Q|R) |- P<->Q";
   1.173 +goal (theory "LK") "Q-->R, R-->P&Q, P-->(Q|R) |- P<->Q";
   1.174  by (fast_tac prop_pack 1);
   1.175  result();
   1.176  
   1.177  (*11.  Proved in each direction (incorrectly, says Pelletier!!)  *)
   1.178 -goal LK.thy "|- P<->P";
   1.179 +goal (theory "LK") "|- P<->P";
   1.180  by (fast_tac prop_pack 1);
   1.181  result();
   1.182  
   1.183  (*12.  "Dijkstra's law"*)
   1.184 -goal LK.thy "|- ((P <-> Q) <-> R)  <->  (P <-> (Q <-> R))";
   1.185 +goal (theory "LK") "|- ((P <-> Q) <-> R)  <->  (P <-> (Q <-> R))";
   1.186  by (fast_tac prop_pack 1);
   1.187  result();
   1.188  
   1.189  (*13.  Distributive law*)
   1.190 -goal LK.thy "|- P | (Q & R)  <-> (P | Q) & (P | R)";
   1.191 +goal (theory "LK") "|- P | (Q & R)  <-> (P | Q) & (P | R)";
   1.192  by (fast_tac prop_pack 1);
   1.193  result();
   1.194  
   1.195  (*14*)
   1.196 -goal LK.thy "|- (P <-> Q) <-> ((Q | ~P) & (~Q|P))";
   1.197 +goal (theory "LK") "|- (P <-> Q) <-> ((Q | ~P) & (~Q|P))";
   1.198  by (fast_tac prop_pack 1);
   1.199  result();
   1.200  
   1.201  
   1.202  (*15*)
   1.203 -goal LK.thy "|- (P --> Q) <-> (~P | Q)";
   1.204 +goal (theory "LK") "|- (P --> Q) <-> (~P | Q)";
   1.205  by (fast_tac prop_pack 1);
   1.206  result();
   1.207  
   1.208  (*16*)
   1.209 -goal LK.thy "|- (P-->Q) | (Q-->P)";
   1.210 +goal (theory "LK") "|- (P-->Q) | (Q-->P)";
   1.211  by (fast_tac prop_pack 1);
   1.212  result();
   1.213  
   1.214  (*17*)
   1.215 -goal LK.thy "|- ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))";
   1.216 +goal (theory "LK") "|- ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))";
   1.217  by (fast_tac prop_pack 1);
   1.218  result();
   1.219 -
   1.220 -writeln"Reached end of file.";