36 *) |
36 *) |
37 |
37 |
38 writeln"Pelletier's examples"; |
38 writeln"Pelletier's examples"; |
39 (*1*) |
39 (*1*) |
40 goal HOL.thy "(P-->Q) = (~Q --> ~P)"; |
40 goal HOL.thy "(P-->Q) = (~Q --> ~P)"; |
41 by (fast_tac HOL_cs 1); |
41 by (Fast_tac 1); |
42 result(); |
42 result(); |
43 |
43 |
44 (*2*) |
44 (*2*) |
45 goal HOL.thy "(~ ~ P) = P"; |
45 goal HOL.thy "(~ ~ P) = P"; |
46 by (fast_tac HOL_cs 1); |
46 by (Fast_tac 1); |
47 result(); |
47 result(); |
48 |
48 |
49 (*3*) |
49 (*3*) |
50 goal HOL.thy "~(P-->Q) --> (Q-->P)"; |
50 goal HOL.thy "~(P-->Q) --> (Q-->P)"; |
51 by (fast_tac HOL_cs 1); |
51 by (Fast_tac 1); |
52 result(); |
52 result(); |
53 |
53 |
54 (*4*) |
54 (*4*) |
55 goal HOL.thy "(~P-->Q) = (~Q --> P)"; |
55 goal HOL.thy "(~P-->Q) = (~Q --> P)"; |
56 by (fast_tac HOL_cs 1); |
56 by (Fast_tac 1); |
57 result(); |
57 result(); |
58 |
58 |
59 (*5*) |
59 (*5*) |
60 goal HOL.thy "((P|Q)-->(P|R)) --> (P|(Q-->R))"; |
60 goal HOL.thy "((P|Q)-->(P|R)) --> (P|(Q-->R))"; |
61 by (fast_tac HOL_cs 1); |
61 by (Fast_tac 1); |
62 result(); |
62 result(); |
63 |
63 |
64 (*6*) |
64 (*6*) |
65 goal HOL.thy "P | ~ P"; |
65 goal HOL.thy "P | ~ P"; |
66 by (fast_tac HOL_cs 1); |
66 by (Fast_tac 1); |
67 result(); |
67 result(); |
68 |
68 |
69 (*7*) |
69 (*7*) |
70 goal HOL.thy "P | ~ ~ ~ P"; |
70 goal HOL.thy "P | ~ ~ ~ P"; |
71 by (fast_tac HOL_cs 1); |
71 by (Fast_tac 1); |
72 result(); |
72 result(); |
73 |
73 |
74 (*8. Peirce's law*) |
74 (*8. Peirce's law*) |
75 goal HOL.thy "((P-->Q) --> P) --> P"; |
75 goal HOL.thy "((P-->Q) --> P) --> P"; |
76 by (fast_tac HOL_cs 1); |
76 by (Fast_tac 1); |
77 result(); |
77 result(); |
78 |
78 |
79 (*9*) |
79 (*9*) |
80 goal HOL.thy "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"; |
80 goal HOL.thy "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"; |
81 by (fast_tac HOL_cs 1); |
81 by (Fast_tac 1); |
82 result(); |
82 result(); |
83 |
83 |
84 (*10*) |
84 (*10*) |
85 goal HOL.thy "(Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P=Q)"; |
85 goal HOL.thy "(Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P=Q)"; |
86 by (fast_tac HOL_cs 1); |
86 by (Fast_tac 1); |
87 result(); |
87 result(); |
88 |
88 |
89 (*11. Proved in each direction (incorrectly, says Pelletier!!) *) |
89 (*11. Proved in each direction (incorrectly, says Pelletier!!) *) |
90 goal HOL.thy "P=P::bool"; |
90 goal HOL.thy "P=P::bool"; |
91 by (fast_tac HOL_cs 1); |
91 by (Fast_tac 1); |
92 result(); |
92 result(); |
93 |
93 |
94 (*12. "Dijkstra's law"*) |
94 (*12. "Dijkstra's law"*) |
95 goal HOL.thy "((P = Q) = R) = (P = (Q = R))"; |
95 goal HOL.thy "((P = Q) = R) = (P = (Q = R))"; |
96 by (fast_tac HOL_cs 1); |
96 by (Fast_tac 1); |
97 result(); |
97 result(); |
98 |
98 |
99 (*13. Distributive law*) |
99 (*13. Distributive law*) |
100 goal HOL.thy "(P | (Q & R)) = ((P | Q) & (P | R))"; |
100 goal HOL.thy "(P | (Q & R)) = ((P | Q) & (P | R))"; |
101 by (fast_tac HOL_cs 1); |
101 by (Fast_tac 1); |
102 result(); |
102 result(); |
103 |
103 |
104 (*14*) |
104 (*14*) |
105 goal HOL.thy "(P = Q) = ((Q | ~P) & (~Q|P))"; |
105 goal HOL.thy "(P = Q) = ((Q | ~P) & (~Q|P))"; |
106 by (fast_tac HOL_cs 1); |
106 by (Fast_tac 1); |
107 result(); |
107 result(); |
108 |
108 |
109 (*15*) |
109 (*15*) |
110 goal HOL.thy "(P --> Q) = (~P | Q)"; |
110 goal HOL.thy "(P --> Q) = (~P | Q)"; |
111 by (fast_tac HOL_cs 1); |
111 by (Fast_tac 1); |
112 result(); |
112 result(); |
113 |
113 |
114 (*16*) |
114 (*16*) |
115 goal HOL.thy "(P-->Q) | (Q-->P)"; |
115 goal HOL.thy "(P-->Q) | (Q-->P)"; |
116 by (fast_tac HOL_cs 1); |
116 by (Fast_tac 1); |
117 result(); |
117 result(); |
118 |
118 |
119 (*17*) |
119 (*17*) |
120 goal HOL.thy "((P & (Q-->R))-->S) = ((~P | Q | S) & (~P | ~R | S))"; |
120 goal HOL.thy "((P & (Q-->R))-->S) = ((~P | Q | S) & (~P | ~R | S))"; |
121 by (fast_tac HOL_cs 1); |
121 by (Fast_tac 1); |
122 result(); |
122 result(); |
123 |
123 |
124 writeln"Classical Logic: examples with quantifiers"; |
124 writeln"Classical Logic: examples with quantifiers"; |
125 |
125 |
126 goal HOL.thy "(! x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))"; |
126 goal HOL.thy "(! x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))"; |
127 by (fast_tac HOL_cs 1); |
127 by (Fast_tac 1); |
128 result(); |
128 result(); |
129 |
129 |
130 goal HOL.thy "(? x. P-->Q(x)) = (P --> (? x.Q(x)))"; |
130 goal HOL.thy "(? x. P-->Q(x)) = (P --> (? x.Q(x)))"; |
131 by (fast_tac HOL_cs 1); |
131 by (Fast_tac 1); |
132 result(); |
132 result(); |
133 |
133 |
134 goal HOL.thy "(? x.P(x)-->Q) = ((! x.P(x)) --> Q)"; |
134 goal HOL.thy "(? x.P(x)-->Q) = ((! x.P(x)) --> Q)"; |
135 by (fast_tac HOL_cs 1); |
135 by (Fast_tac 1); |
136 result(); |
136 result(); |
137 |
137 |
138 goal HOL.thy "((! x.P(x)) | Q) = (! x. P(x) | Q)"; |
138 goal HOL.thy "((! x.P(x)) | Q) = (! x. P(x) | Q)"; |
139 by (fast_tac HOL_cs 1); |
139 by (Fast_tac 1); |
140 result(); |
140 result(); |
141 |
141 |
142 (*From Wishnu Prasetya*) |
142 (*From Wishnu Prasetya*) |
143 goal HOL.thy |
143 goal HOL.thy |
144 "(!s. q(s) --> r(s)) & ~r(s) & (!s. ~r(s) & ~q(s) --> p(t) | q(t)) \ |
144 "(!s. q(s) --> r(s)) & ~r(s) & (!s. ~r(s) & ~q(s) --> p(t) | q(t)) \ |
145 \ --> p(t) | r(t)"; |
145 \ --> p(t) | r(t)"; |
146 by (fast_tac HOL_cs 1); |
146 by (Fast_tac 1); |
147 result(); |
147 result(); |
148 |
148 |
149 |
149 |
150 writeln"Problems requiring quantifier duplication"; |
150 writeln"Problems requiring quantifier duplication"; |
151 |
151 |
152 (*Needs multiple instantiation of the quantifier.*) |
152 (*Needs multiple instantiation of the quantifier.*) |
153 goal HOL.thy "(! x. P(x)-->P(f(x))) & P(d)-->P(f(f(f(d))))"; |
153 goal HOL.thy "(! x. P(x)-->P(f(x))) & P(d)-->P(f(f(f(d))))"; |
154 by (deepen_tac HOL_cs 1 1); |
154 by (deepen_tac (!claset) 1 1); |
155 result(); |
155 result(); |
156 |
156 |
157 (*Needs double instantiation of the quantifier*) |
157 (*Needs double instantiation of the quantifier*) |
158 goal HOL.thy "? x. P(x) --> P(a) & P(b)"; |
158 goal HOL.thy "? x. P(x) --> P(a) & P(b)"; |
159 by (deepen_tac HOL_cs 1 1); |
159 by (deepen_tac (!claset) 1 1); |
160 result(); |
160 result(); |
161 |
161 |
162 goal HOL.thy "? z. P(z) --> (! x. P(x))"; |
162 goal HOL.thy "? z. P(z) --> (! x. P(x))"; |
163 by (deepen_tac HOL_cs 1 1); |
163 by (deepen_tac (!claset) 1 1); |
164 result(); |
164 result(); |
165 |
165 |
166 goal HOL.thy "? x. (? y. P(y)) --> P(x)"; |
166 goal HOL.thy "? x. (? y. P(y)) --> P(x)"; |
167 by (deepen_tac HOL_cs 1 1); |
167 by (deepen_tac (!claset) 1 1); |
168 result(); |
168 result(); |
169 |
169 |
170 writeln"Hard examples with quantifiers"; |
170 writeln"Hard examples with quantifiers"; |
171 |
171 |
172 writeln"Problem 18"; |
172 writeln"Problem 18"; |
173 goal HOL.thy "? y. ! x. P(y)-->P(x)"; |
173 goal HOL.thy "? y. ! x. P(y)-->P(x)"; |
174 by (deepen_tac HOL_cs 1 1); |
174 by (deepen_tac (!claset) 1 1); |
175 result(); |
175 result(); |
176 |
176 |
177 writeln"Problem 19"; |
177 writeln"Problem 19"; |
178 goal HOL.thy "? x. ! y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))"; |
178 goal HOL.thy "? x. ! y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))"; |
179 by (deepen_tac HOL_cs 1 1); |
179 by (deepen_tac (!claset) 1 1); |
180 result(); |
180 result(); |
181 |
181 |
182 writeln"Problem 20"; |
182 writeln"Problem 20"; |
183 goal HOL.thy "(! x y. ? z. ! w. (P(x)&Q(y)-->R(z)&S(w))) \ |
183 goal HOL.thy "(! x y. ? z. ! w. (P(x)&Q(y)-->R(z)&S(w))) \ |
184 \ --> (? x y. P(x) & Q(y)) --> (? z. R(z))"; |
184 \ --> (? x y. P(x) & Q(y)) --> (? z. R(z))"; |
185 by (fast_tac HOL_cs 1); |
185 by (Fast_tac 1); |
186 result(); |
186 result(); |
187 |
187 |
188 writeln"Problem 21"; |
188 writeln"Problem 21"; |
189 goal HOL.thy "(? x. P-->Q(x)) & (? x. Q(x)-->P) --> (? x. P=Q(x))"; |
189 goal HOL.thy "(? x. P-->Q(x)) & (? x. Q(x)-->P) --> (? x. P=Q(x))"; |
190 by (deepen_tac HOL_cs 1 1); |
190 by (deepen_tac (!claset) 1 1); |
191 result(); |
191 result(); |
192 |
192 |
193 writeln"Problem 22"; |
193 writeln"Problem 22"; |
194 goal HOL.thy "(! x. P = Q(x)) --> (P = (! x. Q(x)))"; |
194 goal HOL.thy "(! x. P = Q(x)) --> (P = (! x. Q(x)))"; |
195 by (fast_tac HOL_cs 1); |
195 by (Fast_tac 1); |
196 result(); |
196 result(); |
197 |
197 |
198 writeln"Problem 23"; |
198 writeln"Problem 23"; |
199 goal HOL.thy "(! x. P | Q(x)) = (P | (! x. Q(x)))"; |
199 goal HOL.thy "(! x. P | Q(x)) = (P | (! x. Q(x)))"; |
200 by (best_tac HOL_cs 1); |
200 by (best_tac (!claset) 1); |
201 result(); |
201 result(); |
202 |
202 |
203 writeln"Problem 24"; |
203 writeln"Problem 24"; |
204 goal HOL.thy "~(? x. S(x)&Q(x)) & (! x. P(x) --> Q(x)|R(x)) & \ |
204 goal HOL.thy "~(? x. S(x)&Q(x)) & (! x. P(x) --> Q(x)|R(x)) & \ |
205 \ ~(? x.P(x)) --> (? x.Q(x)) & (! x. Q(x)|R(x) --> S(x)) \ |
205 \ ~(? x.P(x)) --> (? x.Q(x)) & (! x. Q(x)|R(x) --> S(x)) \ |
206 \ --> (? x. P(x)&R(x))"; |
206 \ --> (? x. P(x)&R(x))"; |
207 by (fast_tac HOL_cs 1); |
207 by (Fast_tac 1); |
208 result(); |
208 result(); |
209 |
209 |
210 writeln"Problem 25"; |
210 writeln"Problem 25"; |
211 goal HOL.thy "(? x. P(x)) & \ |
211 goal HOL.thy "(? x. P(x)) & \ |
212 \ (! x. L(x) --> ~ (M(x) & R(x))) & \ |
212 \ (! x. L(x) --> ~ (M(x) & R(x))) & \ |
213 \ (! x. P(x) --> (M(x) & L(x))) & \ |
213 \ (! x. P(x) --> (M(x) & L(x))) & \ |
214 \ ((! x. P(x)-->Q(x)) | (? x. P(x)&R(x))) \ |
214 \ ((! x. P(x)-->Q(x)) | (? x. P(x)&R(x))) \ |
215 \ --> (? x. Q(x)&P(x))"; |
215 \ --> (? x. Q(x)&P(x))"; |
216 by (best_tac HOL_cs 1); |
216 by (best_tac (!claset) 1); |
217 result(); |
217 result(); |
218 |
218 |
219 writeln"Problem 26"; |
219 writeln"Problem 26"; |
220 goal HOL.thy "((? x. p(x)) = (? x. q(x))) & \ |
220 goal HOL.thy "((? x. p(x)) = (? x. q(x))) & \ |
221 \ (! x. ! y. p(x) & q(y) --> (r(x) = s(y))) \ |
221 \ (! x. ! y. p(x) & q(y) --> (r(x) = s(y))) \ |
222 \ --> ((! x. p(x)-->r(x)) = (! x. q(x)-->s(x)))"; |
222 \ --> ((! x. p(x)-->r(x)) = (! x. q(x)-->s(x)))"; |
223 by (fast_tac HOL_cs 1); |
223 by (Fast_tac 1); |
224 result(); |
224 result(); |
225 |
225 |
226 writeln"Problem 27"; |
226 writeln"Problem 27"; |
227 goal HOL.thy "(? x. P(x) & ~Q(x)) & \ |
227 goal HOL.thy "(? x. P(x) & ~Q(x)) & \ |
228 \ (! x. P(x) --> R(x)) & \ |
228 \ (! x. P(x) --> R(x)) & \ |
229 \ (! x. M(x) & L(x) --> P(x)) & \ |
229 \ (! x. M(x) & L(x) --> P(x)) & \ |
230 \ ((? x. R(x) & ~ Q(x)) --> (! x. L(x) --> ~ R(x))) \ |
230 \ ((? x. R(x) & ~ Q(x)) --> (! x. L(x) --> ~ R(x))) \ |
231 \ --> (! x. M(x) --> ~L(x))"; |
231 \ --> (! x. M(x) --> ~L(x))"; |
232 by (fast_tac HOL_cs 1); |
232 by (Fast_tac 1); |
233 result(); |
233 result(); |
234 |
234 |
235 writeln"Problem 28. AMENDED"; |
235 writeln"Problem 28. AMENDED"; |
236 goal HOL.thy "(! x. P(x) --> (! x. Q(x))) & \ |
236 goal HOL.thy "(! x. P(x) --> (! x. Q(x))) & \ |
237 \ ((! x. Q(x)|R(x)) --> (? x. Q(x)&S(x))) & \ |
237 \ ((! x. Q(x)|R(x)) --> (? x. Q(x)&S(x))) & \ |
238 \ ((? x.S(x)) --> (! x. L(x) --> M(x))) \ |
238 \ ((? x.S(x)) --> (! x. L(x) --> M(x))) \ |
239 \ --> (! x. P(x) & L(x) --> M(x))"; |
239 \ --> (! x. P(x) & L(x) --> M(x))"; |
240 by (fast_tac HOL_cs 1); |
240 by (Fast_tac 1); |
241 result(); |
241 result(); |
242 |
242 |
243 writeln"Problem 29. Essentially the same as Principia Mathematica *11.71"; |
243 writeln"Problem 29. Essentially the same as Principia Mathematica *11.71"; |
244 goal HOL.thy "(? x. F(x)) & (? y. G(y)) \ |
244 goal HOL.thy "(? x. F(x)) & (? y. G(y)) \ |
245 \ --> ( ((! x. F(x)-->H(x)) & (! y. G(y)-->J(y))) = \ |
245 \ --> ( ((! x. F(x)-->H(x)) & (! y. G(y)-->J(y))) = \ |
246 \ (! x y. F(x) & G(y) --> H(x) & J(y)))"; |
246 \ (! x y. F(x) & G(y) --> H(x) & J(y)))"; |
247 by (fast_tac HOL_cs 1); |
247 by (Fast_tac 1); |
248 result(); |
248 result(); |
249 |
249 |
250 writeln"Problem 30"; |
250 writeln"Problem 30"; |
251 goal HOL.thy "(! x. P(x) | Q(x) --> ~ R(x)) & \ |
251 goal HOL.thy "(! x. P(x) | Q(x) --> ~ R(x)) & \ |
252 \ (! x. (Q(x) --> ~ S(x)) --> P(x) & R(x)) \ |
252 \ (! x. (Q(x) --> ~ S(x)) --> P(x) & R(x)) \ |
253 \ --> (! x. S(x))"; |
253 \ --> (! x. S(x))"; |
254 by (fast_tac HOL_cs 1); |
254 by (Fast_tac 1); |
255 result(); |
255 result(); |
256 |
256 |
257 writeln"Problem 31"; |
257 writeln"Problem 31"; |
258 goal HOL.thy "~(? x.P(x) & (Q(x) | R(x))) & \ |
258 goal HOL.thy "~(? x.P(x) & (Q(x) | R(x))) & \ |
259 \ (? x. L(x) & P(x)) & \ |
259 \ (? x. L(x) & P(x)) & \ |
260 \ (! x. ~ R(x) --> M(x)) \ |
260 \ (! x. ~ R(x) --> M(x)) \ |
261 \ --> (? x. L(x) & M(x))"; |
261 \ --> (? x. L(x) & M(x))"; |
262 by (fast_tac HOL_cs 1); |
262 by (Fast_tac 1); |
263 result(); |
263 result(); |
264 |
264 |
265 writeln"Problem 32"; |
265 writeln"Problem 32"; |
266 goal HOL.thy "(! x. P(x) & (Q(x)|R(x))-->S(x)) & \ |
266 goal HOL.thy "(! x. P(x) & (Q(x)|R(x))-->S(x)) & \ |
267 \ (! x. S(x) & R(x) --> L(x)) & \ |
267 \ (! x. S(x) & R(x) --> L(x)) & \ |
268 \ (! x. M(x) --> R(x)) \ |
268 \ (! x. M(x) --> R(x)) \ |
269 \ --> (! x. P(x) & M(x) --> L(x))"; |
269 \ --> (! x. P(x) & M(x) --> L(x))"; |
270 by (best_tac HOL_cs 1); |
270 by (best_tac (!claset) 1); |
271 result(); |
271 result(); |
272 |
272 |
273 writeln"Problem 33"; |
273 writeln"Problem 33"; |
274 goal HOL.thy "(! x. P(a) & (P(x)-->P(b))-->P(c)) = \ |
274 goal HOL.thy "(! x. P(a) & (P(x)-->P(b))-->P(c)) = \ |
275 \ (! x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))"; |
275 \ (! x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))"; |
276 by (best_tac HOL_cs 1); |
276 by (best_tac (!claset) 1); |
277 result(); |
277 result(); |
278 |
278 |
279 writeln"Problem 34 AMENDED (TWICE!!)"; |
279 writeln"Problem 34 AMENDED (TWICE!!)"; |
280 (*Andrews's challenge*) |
280 (*Andrews's challenge*) |
281 goal HOL.thy "((? x. ! y. p(x) = p(y)) = \ |
281 goal HOL.thy "((? x. ! y. p(x) = p(y)) = \ |
282 \ ((? x. q(x)) = (! y. p(y)))) = \ |
282 \ ((? x. q(x)) = (! y. p(y)))) = \ |
283 \ ((? x. ! y. q(x) = q(y)) = \ |
283 \ ((? x. ! y. q(x) = q(y)) = \ |
284 \ ((? x. p(x)) = (! y. q(y))))"; |
284 \ ((? x. p(x)) = (! y. q(y))))"; |
285 by (deepen_tac HOL_cs 3 1); |
285 by (deepen_tac (!claset) 3 1); |
286 (*slower with smaller bounds*) |
286 (*slower with smaller bounds*) |
287 result(); |
287 result(); |
288 |
288 |
289 writeln"Problem 35"; |
289 writeln"Problem 35"; |
290 goal HOL.thy "? x y. P x y --> (! u v. P u v)"; |
290 goal HOL.thy "? x y. P x y --> (! u v. P u v)"; |
291 by (deepen_tac HOL_cs 1 1); |
291 by (deepen_tac (!claset) 1 1); |
292 result(); |
292 result(); |
293 |
293 |
294 writeln"Problem 36"; |
294 writeln"Problem 36"; |
295 goal HOL.thy "(! x. ? y. J x y) & \ |
295 goal HOL.thy "(! x. ? y. J x y) & \ |
296 \ (! x. ? y. G x y) & \ |
296 \ (! x. ? y. G x y) & \ |
297 \ (! x y. J x y | G x y --> \ |
297 \ (! x y. J x y | G x y --> \ |
298 \ (! z. J y z | G y z --> H x z)) \ |
298 \ (! z. J y z | G y z --> H x z)) \ |
299 \ --> (! x. ? y. H x y)"; |
299 \ --> (! x. ? y. H x y)"; |
300 by (fast_tac HOL_cs 1); |
300 by (Fast_tac 1); |
301 result(); |
301 result(); |
302 |
302 |
303 writeln"Problem 37"; |
303 writeln"Problem 37"; |
304 goal HOL.thy "(! z. ? w. ! x. ? y. \ |
304 goal HOL.thy "(! z. ? w. ! x. ? y. \ |
305 \ (P x z -->P y w) & P y z & (P y w --> (? u.Q u w))) & \ |
305 \ (P x z -->P y w) & P y z & (P y w --> (? u.Q u w))) & \ |
306 \ (! x z. ~(P x z) --> (? y. Q y z)) & \ |
306 \ (! x z. ~(P x z) --> (? y. Q y z)) & \ |
307 \ ((? x y. Q x y) --> (! x. R x x)) \ |
307 \ ((? x y. Q x y) --> (! x. R x x)) \ |
308 \ --> (! x. ? y. R x y)"; |
308 \ --> (! x. ? y. R x y)"; |
309 by (fast_tac HOL_cs 1); |
309 by (Fast_tac 1); |
310 result(); |
310 result(); |
311 |
311 |
312 writeln"Problem 38"; |
312 writeln"Problem 38"; |
313 goal HOL.thy |
313 goal HOL.thy |
314 "(! x. p(a) & (p(x) --> (? y. p(y) & r x y)) --> \ |
314 "(! x. p(a) & (p(x) --> (? y. p(y) & r x y)) --> \ |
315 \ (? z. ? w. p(z) & r x w & r w z)) = \ |
315 \ (? z. ? w. p(z) & r x w & r w z)) = \ |
316 \ (! x. (~p(a) | p(x) | (? z. ? w. p(z) & r x w & r w z)) & \ |
316 \ (! x. (~p(a) | p(x) | (? z. ? w. p(z) & r x w & r w z)) & \ |
317 \ (~p(a) | ~(? y. p(y) & r x y) | \ |
317 \ (~p(a) | ~(? y. p(y) & r x y) | \ |
318 \ (? z. ? w. p(z) & r x w & r w z)))"; |
318 \ (? z. ? w. p(z) & r x w & r w z)))"; |
319 by (deepen_tac HOL_cs 0 1); (*beats fast_tac!*) |
319 by (deepen_tac (!claset) 0 1); (*beats fast_tac!*) |
320 result(); |
320 result(); |
321 |
321 |
322 writeln"Problem 39"; |
322 writeln"Problem 39"; |
323 goal HOL.thy "~ (? x. ! y. F y x = (~ F y y))"; |
323 goal HOL.thy "~ (? x. ! y. F y x = (~ F y y))"; |
324 by (fast_tac HOL_cs 1); |
324 by (Fast_tac 1); |
325 result(); |
325 result(); |
326 |
326 |
327 writeln"Problem 40. AMENDED"; |
327 writeln"Problem 40. AMENDED"; |
328 goal HOL.thy "(? y. ! x. F x y = F x x) \ |
328 goal HOL.thy "(? y. ! x. F x y = F x x) \ |
329 \ --> ~ (! x. ? y. ! z. F z y = (~ F z x))"; |
329 \ --> ~ (! x. ? y. ! z. F z y = (~ F z x))"; |
330 by (fast_tac HOL_cs 1); |
330 by (Fast_tac 1); |
331 result(); |
331 result(); |
332 |
332 |
333 writeln"Problem 41"; |
333 writeln"Problem 41"; |
334 goal HOL.thy "(! z. ? y. ! x. f x y = (f x z & ~ f x x)) \ |
334 goal HOL.thy "(! z. ? y. ! x. f x y = (f x z & ~ f x x)) \ |
335 \ --> ~ (? z. ! x. f x z)"; |
335 \ --> ~ (? z. ! x. f x z)"; |
336 by (best_tac HOL_cs 1); |
336 by (best_tac (!claset) 1); |
337 result(); |
337 result(); |
338 |
338 |
339 writeln"Problem 42"; |
339 writeln"Problem 42"; |
340 goal HOL.thy "~ (? y. ! x. p x y = (~ (? z. p x z & p z x)))"; |
340 goal HOL.thy "~ (? y. ! x. p x y = (~ (? z. p x z & p z x)))"; |
341 by (deepen_tac HOL_cs 3 1); |
341 by (deepen_tac (!claset) 3 1); |
342 result(); |
342 result(); |
343 |
343 |
344 writeln"Problem 43 NOT PROVED AUTOMATICALLY"; |
344 writeln"Problem 43 NOT PROVED AUTOMATICALLY"; |
345 goal HOL.thy |
345 goal HOL.thy |
346 "(! x::'a. ! y::'a. q x y = (! z. p z x = (p z y::bool))) \ |
346 "(! x::'a. ! y::'a. q x y = (! z. p z x = (p z y::bool))) \ |
350 writeln"Problem 44"; |
350 writeln"Problem 44"; |
351 goal HOL.thy "(! x. f(x) --> \ |
351 goal HOL.thy "(! x. f(x) --> \ |
352 \ (? y. g(y) & h x y & (? y. g(y) & ~ h x y))) & \ |
352 \ (? y. g(y) & h x y & (? y. g(y) & ~ h x y))) & \ |
353 \ (? x. j(x) & (! y. g(y) --> h x y)) \ |
353 \ (? x. j(x) & (! y. g(y) --> h x y)) \ |
354 \ --> (? x. j(x) & ~f(x))"; |
354 \ --> (? x. j(x) & ~f(x))"; |
355 by (fast_tac HOL_cs 1); |
355 by (Fast_tac 1); |
356 result(); |
356 result(); |
357 |
357 |
358 writeln"Problem 45"; |
358 writeln"Problem 45"; |
359 goal HOL.thy |
359 goal HOL.thy |
360 "(! x. f(x) & (! y. g(y) & h x y --> j x y) \ |
360 "(! x. f(x) & (! y. g(y) & h x y --> j x y) \ |
361 \ --> (! y. g(y) & h x y --> k(y))) & \ |
361 \ --> (! y. g(y) & h x y --> k(y))) & \ |
362 \ ~ (? y. l(y) & k(y)) & \ |
362 \ ~ (? y. l(y) & k(y)) & \ |
363 \ (? x. f(x) & (! y. h x y --> l(y)) \ |
363 \ (? x. f(x) & (! y. h x y --> l(y)) \ |
364 \ & (! y. g(y) & h x y --> j x y)) \ |
364 \ & (! y. g(y) & h x y --> j x y)) \ |
365 \ --> (? x. f(x) & ~ (? y. g(y) & h x y))"; |
365 \ --> (? x. f(x) & ~ (? y. g(y) & h x y))"; |
366 by (best_tac HOL_cs 1); |
366 by (best_tac (!claset) 1); |
367 result(); |
367 result(); |
368 |
368 |
369 |
369 |
370 writeln"Problems (mainly) involving equality or functions"; |
370 writeln"Problems (mainly) involving equality or functions"; |
371 |
371 |
372 writeln"Problem 48"; |
372 writeln"Problem 48"; |
373 goal HOL.thy "(a=b | c=d) & (a=c | b=d) --> a=d | b=c"; |
373 goal HOL.thy "(a=b | c=d) & (a=c | b=d) --> a=d | b=c"; |
374 by (fast_tac HOL_cs 1); |
374 by (Fast_tac 1); |
375 result(); |
375 result(); |
376 |
376 |
377 writeln"Problem 49 NOT PROVED AUTOMATICALLY"; |
377 writeln"Problem 49 NOT PROVED AUTOMATICALLY"; |
378 (*Hard because it involves substitution for Vars; |
378 (*Hard because it involves substitution for Vars; |
379 the type constraint ensures that x,y,z have the same type as a,b,u. *) |
379 the type constraint ensures that x,y,z have the same type as a,b,u. *) |
380 goal HOL.thy "(? x y::'a. ! z. z=x | z=y) & P(a) & P(b) & (~a=b) \ |
380 goal HOL.thy "(? x y::'a. ! z. z=x | z=y) & P(a) & P(b) & (~a=b) \ |
381 \ --> (! u::'a.P(u))"; |
381 \ --> (! u::'a.P(u))"; |
382 by (Classical.safe_tac HOL_cs); |
382 by (Classical.safe_tac (!claset)); |
383 by (res_inst_tac [("x","a")] allE 1); |
383 by (res_inst_tac [("x","a")] allE 1); |
384 by (assume_tac 1); |
384 by (assume_tac 1); |
385 by (res_inst_tac [("x","b")] allE 1); |
385 by (res_inst_tac [("x","b")] allE 1); |
386 by (assume_tac 1); |
386 by (assume_tac 1); |
387 by (fast_tac HOL_cs 1); |
387 by (Fast_tac 1); |
388 result(); |
388 result(); |
389 |
389 |
390 writeln"Problem 50"; |
390 writeln"Problem 50"; |
391 (*What has this to do with equality?*) |
391 (*What has this to do with equality?*) |
392 goal HOL.thy "(! x. P a x | (! y.P x y)) --> (? x. ! y.P x y)"; |
392 goal HOL.thy "(! x. P a x | (! y.P x y)) --> (? x. ! y.P x y)"; |
393 by (deepen_tac HOL_cs 1 1); |
393 by (deepen_tac (!claset) 1 1); |
394 result(); |
394 result(); |
395 |
395 |
396 writeln"Problem 51"; |
396 writeln"Problem 51"; |
397 goal HOL.thy |
397 goal HOL.thy |
398 "(? z w. ! x y. P x y = (x=z & y=w)) --> \ |
398 "(? z w. ! x y. P x y = (x=z & y=w)) --> \ |
399 \ (? z. ! x. ? w. (! y. P x y = (y=w)) = (x=z))"; |
399 \ (? z. ! x. ? w. (! y. P x y = (y=w)) = (x=z))"; |
400 by (best_tac HOL_cs 1); |
400 by (best_tac (!claset) 1); |
401 result(); |
401 result(); |
402 |
402 |
403 writeln"Problem 52"; |
403 writeln"Problem 52"; |
404 (*Almost the same as 51. *) |
404 (*Almost the same as 51. *) |
405 goal HOL.thy |
405 goal HOL.thy |
406 "(? z w. ! x y. P x y = (x=z & y=w)) --> \ |
406 "(? z w. ! x y. P x y = (x=z & y=w)) --> \ |
407 \ (? w. ! y. ? z. (! x. P x y = (x=z)) = (y=w))"; |
407 \ (? w. ! y. ? z. (! x. P x y = (x=z)) = (y=w))"; |
408 by (best_tac HOL_cs 1); |
408 by (best_tac (!claset) 1); |
409 result(); |
409 result(); |
410 |
410 |
411 writeln"Problem 55"; |
411 writeln"Problem 55"; |
412 |
412 |
413 (*Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988). |
413 (*Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988). |
419 \ (hates agatha agatha & hates agatha charles) & \ |
419 \ (hates agatha agatha & hates agatha charles) & \ |
420 \ (!x. lives(x) & ~richer x agatha --> hates butler x) & \ |
420 \ (!x. lives(x) & ~richer x agatha --> hates butler x) & \ |
421 \ (!x. hates agatha x --> hates butler x) & \ |
421 \ (!x. hates agatha x --> hates butler x) & \ |
422 \ (!x. ~hates x agatha | ~hates x butler | ~hates x charles) --> \ |
422 \ (!x. ~hates x agatha | ~hates x butler | ~hates x charles) --> \ |
423 \ killed ?who agatha"; |
423 \ killed ?who agatha"; |
424 by (fast_tac HOL_cs 1); |
424 by (Fast_tac 1); |
425 result(); |
425 result(); |
426 |
426 |
427 writeln"Problem 56"; |
427 writeln"Problem 56"; |
428 goal HOL.thy |
428 goal HOL.thy |
429 "(! x. (? y. P(y) & x=f(y)) --> P(x)) = (! x. P(x) --> P(f(x)))"; |
429 "(! x. (? y. P(y) & x=f(y)) --> P(x)) = (! x. P(x) --> P(f(x)))"; |
430 by (fast_tac HOL_cs 1); |
430 by (Fast_tac 1); |
431 result(); |
431 result(); |
432 |
432 |
433 writeln"Problem 57"; |
433 writeln"Problem 57"; |
434 goal HOL.thy |
434 goal HOL.thy |
435 "P (f a b) (f b c) & P (f b c) (f a c) & \ |
435 "P (f a b) (f b c) & P (f b c) (f a c) & \ |
436 \ (! x y z. P x y & P y z --> P x z) --> P (f a b) (f a c)"; |
436 \ (! x y z. P x y & P y z --> P x z) --> P (f a b) (f a c)"; |
437 by (fast_tac HOL_cs 1); |
437 by (Fast_tac 1); |
438 result(); |
438 result(); |
439 |
439 |
440 writeln"Problem 58 NOT PROVED AUTOMATICALLY"; |
440 writeln"Problem 58 NOT PROVED AUTOMATICALLY"; |
441 goal HOL.thy "(! x y. f(x)=g(y)) --> (! x y. f(f(x))=f(g(y)))"; |
441 goal HOL.thy "(! x y. f(x)=g(y)) --> (! x y. f(f(x))=f(g(y)))"; |
442 val f_cong = read_instantiate [("f","f")] arg_cong; |
442 val f_cong = read_instantiate [("f","f")] arg_cong; |
443 by (fast_tac (HOL_cs addIs [f_cong]) 1); |
443 by (fast_tac (!claset addIs [f_cong]) 1); |
444 result(); |
444 result(); |
445 |
445 |
446 writeln"Problem 59"; |
446 writeln"Problem 59"; |
447 goal HOL.thy "(! x. P(x) = (~P(f(x)))) --> (? x. P(x) & ~P(f(x)))"; |
447 goal HOL.thy "(! x. P(x) = (~P(f(x)))) --> (? x. P(x) & ~P(f(x)))"; |
448 by (deepen_tac HOL_cs 1 1); |
448 by (deepen_tac (!claset) 1 1); |
449 result(); |
449 result(); |
450 |
450 |
451 writeln"Problem 60"; |
451 writeln"Problem 60"; |
452 goal HOL.thy |
452 goal HOL.thy |
453 "! x. P x (f x) = (? y. (! z. P z y --> P z (f x)) & P x y)"; |
453 "! x. P x (f x) = (? y. (! z. P z y --> P z (f x)) & P x y)"; |
454 by (fast_tac HOL_cs 1); |
454 by (Fast_tac 1); |
455 result(); |
455 result(); |
456 |
456 |
457 writeln"Problem 62 as corrected in AAR newletter #31"; |
457 writeln"Problem 62 as corrected in AAR newletter #31"; |
458 goal HOL.thy |
458 goal HOL.thy |
459 "(ALL x. p a & (p x --> p(f x)) --> p(f(f x))) = \ |
459 "(ALL x. p a & (p x --> p(f x)) --> p(f(f x))) = \ |
460 \ (ALL x. (~ p a | p x | p(f(f x))) & \ |
460 \ (ALL x. (~ p a | p x | p(f(f x))) & \ |
461 \ (~ p a | ~ p(f x) | p(f(f x))))"; |
461 \ (~ p a | ~ p(f x) | p(f(f x))))"; |
462 by (fast_tac HOL_cs 1); |
462 by (Fast_tac 1); |
463 result(); |
463 result(); |
464 |
464 |
465 (*From Rudnicki, Obvious Inferences, JAR 3 (1987), 383-393. |
465 (*From Rudnicki, Obvious Inferences, JAR 3 (1987), 383-393. |
466 It does seem obvious!*) |
466 It does seem obvious!*) |
467 goal Prod.thy |
467 goal Prod.thy |
468 "(ALL x. F(x) & ~G(x) --> (EX y. H(x,y) & J(y))) & \ |
468 "(ALL x. F(x) & ~G(x) --> (EX y. H(x,y) & J(y))) & \ |
469 \ (EX x. K(x) & F(x) & (ALL y. H(x,y) --> K(y))) & \ |
469 \ (EX x. K(x) & F(x) & (ALL y. H(x,y) --> K(y))) & \ |
470 \ (ALL x. K(x) --> ~G(x)) --> (EX x. K(x) --> ~G(x))"; |
470 \ (ALL x. K(x) --> ~G(x)) --> (EX x. K(x) --> ~G(x))"; |
471 by (fast_tac HOL_cs 1); |
471 by (Fast_tac 1); |
472 result(); |
472 result(); |
473 |
473 |
474 goal Prod.thy |
474 goal Prod.thy |
475 "(ALL x y. R(x,y) | R(y,x)) & \ |
475 "(ALL x y. R(x,y) | R(y,x)) & \ |
476 \ (ALL x y. S(x,y) & S(y,x) --> x=y) & \ |
476 \ (ALL x y. S(x,y) & S(y,x) --> x=y) & \ |
477 \ (ALL x y. R(x,y) --> S(x,y)) --> (ALL x y. S(x,y) --> R(x,y))"; |
477 \ (ALL x y. R(x,y) --> S(x,y)) --> (ALL x y. S(x,y) --> R(x,y))"; |
478 by (fast_tac HOL_cs 1); |
478 by (Fast_tac 1); |
479 result(); |
479 result(); |
480 |
480 |
481 |
481 |
482 |
482 |
483 writeln"Reached end of file."; |
483 writeln"Reached end of file."; |