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.104 +writeln"Schwichtenberg's examples (via T. Nipkow)";
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.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.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.123 +(* peirce-imp2 *)
1.124 +goal thy "(((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P";
1.125 +by tac;
1.126 +result();
1.128 +(* mints  *)
1.129 +goal thy "((((P --> Q) --> P) --> P) --> Q) --> Q";
1.130 +by tac;
1.131 +result();
1.133 +(* mints-solovev *)
1.134 +goal thy "(P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R";
1.135 +by tac;
1.136 +result();
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.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.156 +writeln"Reached end of file.";