1 (* Title: FOL/ex/prop |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1991 University of Cambridge |
|
5 |
|
6 First-Order Logic: propositional examples (intuitionistic and classical) |
|
7 Needs declarations of the theory "thy" and the tactic "tac" |
|
8 *) |
|
9 |
|
10 writeln"File FOL/ex/prop."; |
|
11 |
|
12 |
|
13 writeln"commutative laws of & and | "; |
|
14 Goal "P & Q --> Q & P"; |
|
15 by tac; |
|
16 result(); |
|
17 |
|
18 Goal "P | Q --> Q | P"; |
|
19 by tac; |
|
20 result(); |
|
21 |
|
22 |
|
23 writeln"associative laws of & and | "; |
|
24 Goal "(P & Q) & R --> P & (Q & R)"; |
|
25 by tac; |
|
26 result(); |
|
27 |
|
28 Goal "(P | Q) | R --> P | (Q | R)"; |
|
29 by tac; |
|
30 result(); |
|
31 |
|
32 |
|
33 |
|
34 writeln"distributive laws of & and | "; |
|
35 Goal "(P & Q) | R --> (P | R) & (Q | R)"; |
|
36 by tac; |
|
37 result(); |
|
38 |
|
39 Goal "(P | R) & (Q | R) --> (P & Q) | R"; |
|
40 by tac; |
|
41 result(); |
|
42 |
|
43 Goal "(P | Q) & R --> (P & R) | (Q & R)"; |
|
44 by tac; |
|
45 result(); |
|
46 |
|
47 |
|
48 Goal "(P & R) | (Q & R) --> (P | Q) & R"; |
|
49 by tac; |
|
50 result(); |
|
51 |
|
52 |
|
53 writeln"Laws involving implication"; |
|
54 |
|
55 Goal "(P-->R) & (Q-->R) <-> (P|Q --> R)"; |
|
56 by tac; |
|
57 result(); |
|
58 |
|
59 |
|
60 Goal "(P & Q --> R) <-> (P--> (Q-->R))"; |
|
61 by tac; |
|
62 result(); |
|
63 |
|
64 |
|
65 Goal "((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R"; |
|
66 by tac; |
|
67 result(); |
|
68 |
|
69 Goal "~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)"; |
|
70 by tac; |
|
71 result(); |
|
72 |
|
73 Goal "(P --> Q & R) <-> (P-->Q) & (P-->R)"; |
|
74 by tac; |
|
75 result(); |
|
76 |
|
77 |
|
78 writeln"Propositions-as-types"; |
|
79 |
|
80 (*The combinator K*) |
|
81 Goal "P --> (Q --> P)"; |
|
82 by tac; |
|
83 result(); |
|
84 |
|
85 (*The combinator S*) |
|
86 Goal "(P-->Q-->R) --> (P-->Q) --> (P-->R)"; |
|
87 by tac; |
|
88 result(); |
|
89 |
|
90 |
|
91 (*Converse is classical*) |
|
92 Goal "(P-->Q) | (P-->R) --> (P --> Q | R)"; |
|
93 by tac; |
|
94 result(); |
|
95 |
|
96 Goal "(P-->Q) --> (~Q --> ~P)"; |
|
97 by tac; |
|
98 result(); |
|
99 |
|
100 |
|
101 writeln"Schwichtenberg's examples (via T. Nipkow)"; |
|
102 |
|
103 (* stab-imp *) |
|
104 Goal "(((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q"; |
|
105 by tac; |
|
106 result(); |
|
107 |
|
108 (* stab-to-peirce *) |
|
109 Goal "(((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q) \ |
|
110 \ --> ((P --> Q) --> P) --> P"; |
|
111 by tac; |
|
112 result(); |
|
113 |
|
114 (* peirce-imp1 *) |
|
115 Goal "(((Q --> R) --> Q) --> Q) \ |
|
116 \ --> (((P --> Q) --> R) --> P --> Q) --> P --> Q"; |
|
117 by tac; |
|
118 result(); |
|
119 |
|
120 (* peirce-imp2 *) |
|
121 Goal "(((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P"; |
|
122 by tac; |
|
123 result(); |
|
124 |
|
125 (* mints *) |
|
126 Goal "((((P --> Q) --> P) --> P) --> Q) --> Q"; |
|
127 by tac; |
|
128 result(); |
|
129 |
|
130 (* mints-solovev *) |
|
131 Goal "(P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R"; |
|
132 by tac; |
|
133 result(); |
|
134 |
|
135 (* tatsuta *) |
|
136 Goal "(((P7 --> P1) --> P10) --> P4 --> P5) \ |
|
137 \ --> (((P8 --> P2) --> P9) --> P3 --> P10) \ |
|
138 \ --> (P1 --> P8) --> P6 --> P7 \ |
|
139 \ --> (((P3 --> P2) --> P9) --> P4) \ |
|
140 \ --> (P1 --> P3) --> (((P6 --> P1) --> P2) --> P9) --> P5"; |
|
141 by tac; |
|
142 result(); |
|
143 |
|
144 (* tatsuta1 *) |
|
145 Goal "(((P8 --> P2) --> P9) --> P3 --> P10) \ |
|
146 \ --> (((P3 --> P2) --> P9) --> P4) \ |
|
147 \ --> (((P6 --> P1) --> P2) --> P9) \ |
|
148 \ --> (((P7 --> P1) --> P10) --> P4 --> P5) \ |
|
149 \ --> (P1 --> P3) --> (P1 --> P8) --> P6 --> P7 --> P5"; |
|
150 by tac; |
|
151 result(); |
|
152 |
|
153 writeln"Reached end of file."; |
|