src/FOL/ex/prop.ML
changeset 0 a5a9c433f639
child 1459 d12da312eff4
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/FOL/ex/prop.ML	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,153 @@
     1.4 +(*  Title: 	FOL/ex/prop
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1991  University of Cambridge
     1.8 +
     1.9 +First-Order Logic: propositional examples (intuitionistic and classical)
    1.10 +Needs declarations of the theory "thy" and the tactic "tac"
    1.11 +*)
    1.12 +
    1.13 +writeln"File FOL/ex/prop.";
    1.14 +
    1.15 +
    1.16 +writeln"commutative laws of & and | ";
    1.17 +goal thy "P & Q  -->  Q & P";
    1.18 +by tac;
    1.19 +result();
    1.20 +
    1.21 +goal thy "P | Q  -->  Q | P";
    1.22 +by tac;
    1.23 +result();
    1.24 +
    1.25 +
    1.26 +writeln"associative laws of & and | ";
    1.27 +goal thy "(P & Q) & R  -->  P & (Q & R)";
    1.28 +by tac;
    1.29 +result();
    1.30 +
    1.31 +goal thy "(P | Q) | R  -->  P | (Q | R)";
    1.32 +by tac;
    1.33 +result();
    1.34 +
    1.35 +
    1.36 +
    1.37 +writeln"distributive laws of & and | ";
    1.38 +goal thy "(P & Q) | R  --> (P | R) & (Q | R)";
    1.39 +by tac;
    1.40 +result();
    1.41 +
    1.42 +goal thy "(P | R) & (Q | R)  --> (P & Q) | R";
    1.43 +by tac;
    1.44 +result();
    1.45 +
    1.46 +goal thy "(P | Q) & R  --> (P & R) | (Q & R)";
    1.47 +by tac;
    1.48 +result();
    1.49 +
    1.50 +
    1.51 +goal thy "(P & R) | (Q & R)  --> (P | Q) & R";
    1.52 +by tac;
    1.53 +result();
    1.54 +
    1.55 +
    1.56 +writeln"Laws involving implication";
    1.57 +
    1.58 +goal thy "(P-->R) & (Q-->R) <-> (P|Q --> R)";
    1.59 +by tac;
    1.60 +result();
    1.61 +
    1.62 +
    1.63 +goal thy "(P & Q --> R) <-> (P--> (Q-->R))";
    1.64 +by tac;
    1.65 +result();
    1.66 +
    1.67 +
    1.68 +goal thy "((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R";
    1.69 +by tac;
    1.70 +result();
    1.71 +
    1.72 +goal thy "~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)";
    1.73 +by tac;
    1.74 +result();
    1.75 +
    1.76 +goal thy "(P --> Q & R) <-> (P-->Q)  &  (P-->R)";
    1.77 +by tac;
    1.78 +result();
    1.79 +
    1.80 +
    1.81 +writeln"Propositions-as-types";
    1.82 +
    1.83 +(*The combinator K*)
    1.84 +goal thy "P --> (Q --> P)";
    1.85 +by tac;
    1.86 +result();
    1.87 +
    1.88 +(*The combinator S*)
    1.89 +goal thy "(P-->Q-->R)  --> (P-->Q) --> (P-->R)";
    1.90 +by tac;
    1.91 +result();
    1.92 +
    1.93 +
    1.94 +(*Converse is classical*)
    1.95 +goal thy "(P-->Q) | (P-->R)  -->  (P --> Q | R)";
    1.96 +by tac;
    1.97 +result();
    1.98 +
    1.99 +goal thy "(P-->Q)  -->  (~Q --> ~P)";
   1.100 +by tac;
   1.101 +result();
   1.102 +
   1.103 +
   1.104 +writeln"Schwichtenberg's examples (via T. Nipkow)";
   1.105 +
   1.106 +(* stab-imp *)
   1.107 +goal thy "(((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q";
   1.108 +by tac;
   1.109 +result();
   1.110 +
   1.111 +(* stab-to-peirce *)
   1.112 +goal thy "(((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q) \
   1.113 +\	      --> ((P --> Q) --> P) --> P";
   1.114 +by tac;
   1.115 +result();
   1.116 +
   1.117 +(* peirce-imp1 *)
   1.118 +goal thy "(((Q --> R) --> Q) --> Q) \
   1.119 +\	       --> (((P --> Q) --> R) --> P --> Q) --> P --> Q";
   1.120 +by tac;
   1.121 +result();
   1.122 +  
   1.123 +(* peirce-imp2 *)
   1.124 +goal thy "(((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P";
   1.125 +by tac;
   1.126 +result();
   1.127 +
   1.128 +(* mints  *)
   1.129 +goal thy "((((P --> Q) --> P) --> P) --> Q) --> Q";
   1.130 +by tac;
   1.131 +result();
   1.132 +
   1.133 +(* mints-solovev *)
   1.134 +goal thy "(P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R";
   1.135 +by tac;
   1.136 +result();
   1.137 +
   1.138 +(* tatsuta *)
   1.139 +goal thy "(((P7 --> P1) --> P10) --> P4 --> P5) \
   1.140 +\	  --> (((P8 --> P2) --> P9) --> P3 --> P10) \
   1.141 +\	  --> (P1 --> P8) --> P6 --> P7 \
   1.142 +\	  --> (((P3 --> P2) --> P9) --> P4) \
   1.143 +\	  --> (P1 --> P3) --> (((P6 --> P1) --> P2) --> P9) --> P5";
   1.144 +by tac;
   1.145 +result();
   1.146 +
   1.147 +(* tatsuta1 *)
   1.148 +goal thy "(((P8 --> P2) --> P9) --> P3 --> P10) \
   1.149 +\    --> (((P3 --> P2) --> P9) --> P4) \
   1.150 +\    --> (((P6 --> P1) --> P2) --> P9) \
   1.151 +\    --> (((P7 --> P1) --> P10) --> P4 --> P5) \
   1.152 +\    --> (P1 --> P3) --> (P1 --> P8) --> P6 --> P7 --> P5";
   1.153 +by tac;
   1.154 +result();
   1.155 +
   1.156 +writeln"Reached end of file.";