1 (* Title: HOL/ex/meson |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1992 University of Cambridge |
|
5 |
|
6 Test data for the MESON proof procedure |
|
7 (Excludes the equality problems 51, 52, 56, 58) |
|
8 |
|
9 show_hyps:=false; |
|
10 |
|
11 by (rtac ccontr 1); |
|
12 val [prem] = gethyps 1; |
|
13 val nnf = make_nnf prem; |
|
14 val xsko = skolemize nnf; |
|
15 by (cut_facts_tac [xsko] 1 THEN REPEAT (etac exE 1)); |
|
16 val [_,sko] = gethyps 1; |
|
17 val clauses = make_clauses [sko]; |
|
18 val horns = make_horns clauses; |
|
19 val go::_ = neg_clauses clauses; |
|
20 |
|
21 goal HOL.thy "False"; |
|
22 by (rtac (make_goal go) 1); |
|
23 by (prolog_step_tac horns 1); |
|
24 by (depth_prolog_tac horns); |
|
25 by (best_prolog_tac size_of_subgoals horns); |
|
26 *) |
|
27 |
|
28 writeln"File HOL/ex/meson-test."; |
|
29 |
|
30 (**** Interactive examples ****) |
|
31 |
|
32 (*Generate nice names for Skolem functions*) |
|
33 Logic.auto_rename := true; Logic.set_rename_prefix "a"; |
|
34 |
|
35 |
|
36 writeln"Problem 25"; |
|
37 goal HOL.thy "(? x. P(x)) & \ |
|
38 \ (! x. L(x) --> ~ (M(x) & R(x))) & \ |
|
39 \ (! x. P(x) --> (M(x) & L(x))) & \ |
|
40 \ ((! x. P(x)-->Q(x)) | (? x. P(x)&R(x))) \ |
|
41 \ --> (? x. Q(x)&P(x))"; |
|
42 by (rtac ccontr 1); |
|
43 val [prem25] = gethyps 1; |
|
44 val nnf25 = make_nnf prem25; |
|
45 val xsko25 = skolemize nnf25; |
|
46 by (cut_facts_tac [xsko25] 1 THEN REPEAT (etac exE 1)); |
|
47 val [_,sko25] = gethyps 1; |
|
48 val clauses25 = make_clauses [sko25]; (*7 clauses*) |
|
49 val horns25 = make_horns clauses25; (*16 Horn clauses*) |
|
50 val go25::_ = neg_clauses clauses25; |
|
51 |
|
52 goal HOL.thy "False"; |
|
53 by (rtac (make_goal go25) 1); |
|
54 by (depth_prolog_tac horns25); |
|
55 |
|
56 |
|
57 writeln"Problem 26"; |
|
58 goal HOL.thy "((? x. p(x)) = (? x. q(x))) & \ |
|
59 \ (! x. ! y. p(x) & q(y) --> (r(x) = s(y))) \ |
|
60 \ --> ((! x. p(x)-->r(x)) = (! x. q(x)-->s(x)))"; |
|
61 by (rtac ccontr 1); |
|
62 val [prem26] = gethyps 1; |
|
63 val nnf26 = make_nnf prem26; |
|
64 val xsko26 = skolemize nnf26; |
|
65 by (cut_facts_tac [xsko26] 1 THEN REPEAT (etac exE 1)); |
|
66 val [_,sko26] = gethyps 1; |
|
67 val clauses26 = make_clauses [sko26]; (*9 clauses*) |
|
68 val horns26 = make_horns clauses26; (*24 Horn clauses*) |
|
69 val go26::_ = neg_clauses clauses26; |
|
70 |
|
71 goal HOL.thy "False"; |
|
72 by (rtac (make_goal go26) 1); |
|
73 by (depth_prolog_tac horns26); (*6 secs*) |
|
74 |
|
75 |
|
76 |
|
77 writeln"Problem 43 NOW PROVED AUTOMATICALLY!!"; |
|
78 goal HOL.thy "(! x. ! y. q(x,y) = (! z. p(z,x) = (p(z,y)::bool))) \ |
|
79 \ --> (! x. (! y. q(x,y) = (q(y,x)::bool)))"; |
|
80 by (rtac ccontr 1); |
|
81 val [prem43] = gethyps 1; |
|
82 val nnf43 = make_nnf prem43; |
|
83 val xsko43 = skolemize nnf43; |
|
84 by (cut_facts_tac [xsko43] 1 THEN REPEAT (etac exE 1)); |
|
85 val [_,sko43] = gethyps 1; |
|
86 val clauses43 = make_clauses [sko43]; (*6*) |
|
87 val horns43 = make_horns clauses43; (*16*) |
|
88 val go43::_ = neg_clauses clauses43; |
|
89 |
|
90 goal HOL.thy "False"; |
|
91 by (rtac (make_goal go43) 1); |
|
92 by (best_prolog_tac size_of_subgoals horns43); |
|
93 (*8.7 secs*) |
|
94 |
|
95 |
|
96 (*Restore variable name preservation*) |
|
97 Logic.auto_rename := false; |
|
98 |
|
99 |
|
100 (**** Batch test data ****) |
|
101 |
|
102 (*Sample problems from |
|
103 F. J. Pelletier, |
|
104 Seventy-Five Problems for Testing Automatic Theorem Provers, |
|
105 J. Automated Reasoning 2 (1986), 191-216. |
|
106 Errata, JAR 4 (1988), 236-236. |
|
107 |
|
108 The hardest problems -- judging by experience with several theorem provers, |
|
109 including matrix ones -- are 34 and 43. |
|
110 *) |
|
111 |
|
112 writeln"Pelletier's examples"; |
|
113 (*1*) |
|
114 goal HOL.thy "(P-->Q) = (~Q --> ~P)"; |
|
115 by (safe_meson_tac 1); |
|
116 result(); |
|
117 |
|
118 (*2*) |
|
119 goal HOL.thy "(~ ~ P) = P"; |
|
120 by (safe_meson_tac 1); |
|
121 result(); |
|
122 |
|
123 (*3*) |
|
124 goal HOL.thy "~(P-->Q) --> (Q-->P)"; |
|
125 by (safe_meson_tac 1); |
|
126 result(); |
|
127 |
|
128 (*4*) |
|
129 goal HOL.thy "(~P-->Q) = (~Q --> P)"; |
|
130 by (safe_meson_tac 1); |
|
131 result(); |
|
132 |
|
133 (*5*) |
|
134 goal HOL.thy "((P|Q)-->(P|R)) --> (P|(Q-->R))"; |
|
135 by (safe_meson_tac 1); |
|
136 result(); |
|
137 |
|
138 (*6*) |
|
139 goal HOL.thy "P | ~ P"; |
|
140 by (safe_meson_tac 1); |
|
141 result(); |
|
142 |
|
143 (*7*) |
|
144 goal HOL.thy "P | ~ ~ ~ P"; |
|
145 by (safe_meson_tac 1); |
|
146 result(); |
|
147 |
|
148 (*8. Peirce's law*) |
|
149 goal HOL.thy "((P-->Q) --> P) --> P"; |
|
150 by (safe_meson_tac 1); |
|
151 result(); |
|
152 |
|
153 (*9*) |
|
154 goal HOL.thy "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"; |
|
155 by (safe_meson_tac 1); |
|
156 result(); |
|
157 |
|
158 (*10*) |
|
159 goal HOL.thy "(Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P=Q)"; |
|
160 by (safe_meson_tac 1); |
|
161 result(); |
|
162 |
|
163 (*11. Proved in each direction (incorrectly, says Pelletier!!) *) |
|
164 goal HOL.thy "P=(P::bool)"; |
|
165 by (safe_meson_tac 1); |
|
166 result(); |
|
167 |
|
168 (*12. "Dijkstra's law"*) |
|
169 goal HOL.thy "((P = Q) = R) = (P = (Q = R))"; |
|
170 by (best_meson_tac size_of_subgoals 1); |
|
171 result(); |
|
172 |
|
173 (*13. Distributive law*) |
|
174 goal HOL.thy "(P | (Q & R)) = ((P | Q) & (P | R))"; |
|
175 by (safe_meson_tac 1); |
|
176 result(); |
|
177 |
|
178 (*14*) |
|
179 goal HOL.thy "(P = Q) = ((Q | ~P) & (~Q|P))"; |
|
180 by (safe_meson_tac 1); |
|
181 result(); |
|
182 |
|
183 (*15*) |
|
184 goal HOL.thy "(P --> Q) = (~P | Q)"; |
|
185 by (safe_meson_tac 1); |
|
186 result(); |
|
187 |
|
188 (*16*) |
|
189 goal HOL.thy "(P-->Q) | (Q-->P)"; |
|
190 by (safe_meson_tac 1); |
|
191 result(); |
|
192 |
|
193 (*17*) |
|
194 goal HOL.thy "((P & (Q-->R))-->S) = ((~P | Q | S) & (~P | ~R | S))"; |
|
195 by (safe_meson_tac 1); |
|
196 result(); |
|
197 |
|
198 writeln"Classical Logic: examples with quantifiers"; |
|
199 |
|
200 goal HOL.thy "(! x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))"; |
|
201 by (safe_meson_tac 1); |
|
202 result(); |
|
203 |
|
204 goal HOL.thy "(? x. P-->Q(x)) = (P --> (? x.Q(x)))"; |
|
205 by (safe_meson_tac 1); |
|
206 result(); |
|
207 |
|
208 goal HOL.thy "(? x.P(x)-->Q) = ((! x.P(x)) --> Q)"; |
|
209 by (safe_meson_tac 1); |
|
210 result(); |
|
211 |
|
212 goal HOL.thy "((! x.P(x)) | Q) = (! x. P(x) | Q)"; |
|
213 by (safe_meson_tac 1); |
|
214 result(); |
|
215 |
|
216 writeln"Testing the complete tactic"; |
|
217 |
|
218 (*Not provable by pc_tac: needs multiple instantiation of !. |
|
219 Could be proved trivially by a PROLOG interpreter*) |
|
220 goal HOL.thy "(! x. P(x)-->P(f(x))) & P(d)-->P(f(f(f(d))))"; |
|
221 by (safe_meson_tac 1); |
|
222 result(); |
|
223 |
|
224 (*Not provable by pc_tac: needs double instantiation of EXISTS*) |
|
225 goal HOL.thy "? x. P(x) --> P(a) & P(b)"; |
|
226 by (safe_meson_tac 1); |
|
227 result(); |
|
228 |
|
229 goal HOL.thy "? z. P(z) --> (! x. P(x))"; |
|
230 by (safe_meson_tac 1); |
|
231 result(); |
|
232 |
|
233 writeln"Hard examples with quantifiers"; |
|
234 |
|
235 writeln"Problem 18"; |
|
236 goal HOL.thy "? y. ! x. P(y)-->P(x)"; |
|
237 by (safe_meson_tac 1); |
|
238 result(); |
|
239 |
|
240 writeln"Problem 19"; |
|
241 goal HOL.thy "? x. ! y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))"; |
|
242 by (safe_meson_tac 1); |
|
243 result(); |
|
244 |
|
245 writeln"Problem 20"; |
|
246 goal HOL.thy "(! x y. ? z. ! w. (P(x)&Q(y)-->R(z)&S(w))) \ |
|
247 \ --> (? x y. P(x) & Q(y)) --> (? z. R(z))"; |
|
248 by (safe_meson_tac 1); |
|
249 result(); |
|
250 |
|
251 writeln"Problem 21"; |
|
252 goal HOL.thy "(? x. P-->Q(x)) & (? x. Q(x)-->P) --> (? x. P=Q(x))"; |
|
253 by (safe_meson_tac 1); |
|
254 result(); |
|
255 |
|
256 writeln"Problem 22"; |
|
257 goal HOL.thy "(! x. P = Q(x)) --> (P = (! x. Q(x)))"; |
|
258 by (safe_meson_tac 1); |
|
259 result(); |
|
260 |
|
261 writeln"Problem 23"; |
|
262 goal HOL.thy "(! x. P | Q(x)) = (P | (! x. Q(x)))"; |
|
263 by (safe_meson_tac 1); |
|
264 result(); |
|
265 |
|
266 writeln"Problem 24"; |
|
267 goal HOL.thy "~(? x. S(x)&Q(x)) & (! x. P(x) --> Q(x)|R(x)) & \ |
|
268 \ ~(? x.P(x)) --> (? x.Q(x)) & (! x. Q(x)|R(x) --> S(x)) \ |
|
269 \ --> (? x. P(x)&R(x))"; |
|
270 by (safe_meson_tac 1); |
|
271 result(); |
|
272 |
|
273 writeln"Problem 25"; |
|
274 goal HOL.thy "(? x. P(x)) & \ |
|
275 \ (! x. L(x) --> ~ (M(x) & R(x))) & \ |
|
276 \ (! x. P(x) --> (M(x) & L(x))) & \ |
|
277 \ ((! x. P(x)-->Q(x)) | (? x. P(x)&R(x))) \ |
|
278 \ --> (? x. Q(x)&P(x))"; |
|
279 by (safe_meson_tac 1); |
|
280 result(); |
|
281 |
|
282 writeln"Problem 26"; |
|
283 goal HOL.thy "((? x. p(x)) = (? x. q(x))) & \ |
|
284 \ (! x. ! y. p(x) & q(y) --> (r(x) = s(y))) \ |
|
285 \ --> ((! x. p(x)-->r(x)) = (! x. q(x)-->s(x)))"; |
|
286 by (safe_meson_tac 1); |
|
287 result(); |
|
288 |
|
289 writeln"Problem 27"; |
|
290 goal HOL.thy "(? x. P(x) & ~Q(x)) & \ |
|
291 \ (! x. P(x) --> R(x)) & \ |
|
292 \ (! x. M(x) & L(x) --> P(x)) & \ |
|
293 \ ((? x. R(x) & ~ Q(x)) --> (! x. L(x) --> ~ R(x))) \ |
|
294 \ --> (! x. M(x) --> ~L(x))"; |
|
295 by (safe_meson_tac 1); |
|
296 result(); |
|
297 |
|
298 writeln"Problem 28. AMENDED"; |
|
299 goal HOL.thy "(! x. P(x) --> (! x. Q(x))) & \ |
|
300 \ ((! x. Q(x)|R(x)) --> (? x. Q(x)&S(x))) & \ |
|
301 \ ((? x.S(x)) --> (! x. L(x) --> M(x))) \ |
|
302 \ --> (! x. P(x) & L(x) --> M(x))"; |
|
303 by (safe_meson_tac 1); |
|
304 result(); |
|
305 |
|
306 writeln"Problem 29. Essentially the same as Principia Mathematica *11.71"; |
|
307 goal HOL.thy "(? x. F(x)) & (? y. G(y)) \ |
|
308 \ --> ( ((! x. F(x)-->H(x)) & (! y. G(y)-->J(y))) = \ |
|
309 \ (! x y. F(x) & G(y) --> H(x) & J(y)))"; |
|
310 by (safe_meson_tac 1); (*5 secs*) |
|
311 result(); |
|
312 |
|
313 writeln"Problem 30"; |
|
314 goal HOL.thy "(! x. P(x) | Q(x) --> ~ R(x)) & \ |
|
315 \ (! x. (Q(x) --> ~ S(x)) --> P(x) & R(x)) \ |
|
316 \ --> (! x. S(x))"; |
|
317 by (safe_meson_tac 1); |
|
318 result(); |
|
319 |
|
320 writeln"Problem 31"; |
|
321 goal HOL.thy "~(? x.P(x) & (Q(x) | R(x))) & \ |
|
322 \ (? x. L(x) & P(x)) & \ |
|
323 \ (! x. ~ R(x) --> M(x)) \ |
|
324 \ --> (? x. L(x) & M(x))"; |
|
325 by (safe_meson_tac 1); |
|
326 result(); |
|
327 |
|
328 writeln"Problem 32"; |
|
329 goal HOL.thy "(! x. P(x) & (Q(x)|R(x))-->S(x)) & \ |
|
330 \ (! x. S(x) & R(x) --> L(x)) & \ |
|
331 \ (! x. M(x) --> R(x)) \ |
|
332 \ --> (! x. P(x) & M(x) --> L(x))"; |
|
333 by (safe_meson_tac 1); |
|
334 result(); |
|
335 |
|
336 writeln"Problem 33"; |
|
337 goal HOL.thy "(! x. P(a) & (P(x)-->P(b))-->P(c)) = \ |
|
338 \ (! x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))"; |
|
339 by (safe_meson_tac 1); (*5.6 secs*) |
|
340 result(); |
|
341 |
|
342 writeln"Problem 34 AMENDED (TWICE!!)"; |
|
343 (*Andrews's challenge*) |
|
344 goal HOL.thy "((? x. ! y. p(x) = p(y)) = \ |
|
345 \ ((? x. q(x)) = (! y. p(y)))) = \ |
|
346 \ ((? x. ! y. q(x) = q(y)) = \ |
|
347 \ ((? x. p(x)) = (! y. q(y))))"; |
|
348 by (safe_meson_tac 1); (*90 secs*) |
|
349 result(); |
|
350 |
|
351 writeln"Problem 35"; |
|
352 goal HOL.thy "? x y. P(x,y) --> (! u v. P(u,v))"; |
|
353 by (safe_meson_tac 1); |
|
354 result(); |
|
355 |
|
356 writeln"Problem 36"; |
|
357 goal HOL.thy "(! x. ? y. J(x,y)) & \ |
|
358 \ (! x. ? y. G(x,y)) & \ |
|
359 \ (! x y. J(x,y) | G(x,y) --> \ |
|
360 \ (! z. J(y,z) | G(y,z) --> H(x,z))) \ |
|
361 \ --> (! x. ? y. H(x,y))"; |
|
362 by (safe_meson_tac 1); |
|
363 result(); |
|
364 |
|
365 writeln"Problem 37"; |
|
366 goal HOL.thy "(! z. ? w. ! x. ? y. \ |
|
367 \ (P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (? u.Q(u,w)))) & \ |
|
368 \ (! x z. ~P(x,z) --> (? y. Q(y,z))) & \ |
|
369 \ ((? x y. Q(x,y)) --> (! x. R(x,x))) \ |
|
370 \ --> (! x. ? y. R(x,y))"; |
|
371 by (safe_meson_tac 1); (*causes unification tracing messages*) |
|
372 result(); |
|
373 |
|
374 writeln"Problem 38"; |
|
375 goal HOL.thy |
|
376 "(! x. p(a) & (p(x) --> (? y. p(y) & r(x,y))) --> \ |
|
377 \ (? z. ? w. p(z) & r(x,w) & r(w,z))) = \ |
|
378 \ (! x. (~p(a) | p(x) | (? z. ? w. p(z) & r(x,w) & r(w,z))) & \ |
|
379 \ (~p(a) | ~(? y. p(y) & r(x,y)) | \ |
|
380 \ (? z. ? w. p(z) & r(x,w) & r(w,z))))"; |
|
381 by (safe_meson_tac 1); (*62 secs*) |
|
382 result(); |
|
383 |
|
384 writeln"Problem 39"; |
|
385 goal HOL.thy "~ (? x. ! y. F(y,x) = (~F(y,y)))"; |
|
386 by (safe_meson_tac 1); |
|
387 result(); |
|
388 |
|
389 writeln"Problem 40. AMENDED"; |
|
390 goal HOL.thy "(? y. ! x. F(x,y) = F(x,x)) \ |
|
391 \ --> ~ (! x. ? y. ! z. F(z,y) = (~F(z,x)))"; |
|
392 by (safe_meson_tac 1); |
|
393 result(); |
|
394 |
|
395 writeln"Problem 41"; |
|
396 goal HOL.thy "(! z. (? y. (! x. f(x,y) = (f(x,z) & ~ f(x,x))))) \ |
|
397 \ --> ~ (? z. ! x. f(x,z))"; |
|
398 by (safe_meson_tac 1); |
|
399 result(); |
|
400 |
|
401 writeln"Problem 42"; |
|
402 goal HOL.thy "~ (? y. ! x. p(x,y) = (~ (? z. p(x,z) & p(z,x))))"; |
|
403 by (safe_meson_tac 1); |
|
404 result(); |
|
405 |
|
406 writeln"Problem 43 NOW PROVED AUTOMATICALLY!!"; |
|
407 goal HOL.thy "(! x. ! y. q(x,y) = (! z. p(z,x) = (p(z,y)::bool))) \ |
|
408 \ --> (! x. (! y. q(x,y) = (q(y,x)::bool)))"; |
|
409 by (safe_meson_tac 1); |
|
410 result(); |
|
411 |
|
412 writeln"Problem 44"; |
|
413 goal HOL.thy "(! x. f(x) --> \ |
|
414 \ (? y. g(y) & h(x,y) & (? y. g(y) & ~ h(x,y)))) & \ |
|
415 \ (? x. j(x) & (! y. g(y) --> h(x,y))) \ |
|
416 \ --> (? x. j(x) & ~f(x))"; |
|
417 by (safe_meson_tac 1); |
|
418 result(); |
|
419 |
|
420 writeln"Problem 45"; |
|
421 goal HOL.thy "(! x. f(x) & (! y. g(y) & h(x,y) --> j(x,y)) \ |
|
422 \ --> (! y. g(y) & h(x,y) --> k(y))) & \ |
|
423 \ ~ (? y. l(y) & k(y)) & \ |
|
424 \ (? x. f(x) & (! y. h(x,y) --> l(y)) \ |
|
425 \ & (! y. g(y) & h(x,y) --> j(x,y))) \ |
|
426 \ --> (? x. f(x) & ~ (? y. g(y) & h(x,y)))"; |
|
427 by (safe_meson_tac 1); (*11 secs*) |
|
428 result(); |
|
429 |
|
430 writeln"Problem 46"; |
|
431 goal HOL.thy |
|
432 "(! x. f(x) & (! y. f(y) & h(y,x) --> g(y)) --> g(x)) & \ |
|
433 \ ((? x.f(x) & ~g(x)) --> \ |
|
434 \ (? x. f(x) & ~g(x) & (! y. f(y) & ~g(y) --> j(x,y)))) & \ |
|
435 \ (! x y. f(x) & f(y) & h(x,y) --> ~j(y,x)) \ |
|
436 \ --> (! x. f(x) --> g(x))"; |
|
437 by (safe_meson_tac 1); (*11 secs*) |
|
438 result(); |
|
439 |
|
440 (* Example suggested by Johannes Schumann and credited to Pelletier *) |
|
441 goal HOL.thy "(!x y z. P(x,y) --> P(y,z) --> P(x,z)) --> \ |
|
442 \ (!x y z. Q(x,y) --> Q(y,z) --> Q(x,z)) --> \ |
|
443 \ (!x y.Q(x,y) --> Q(y,x)) --> (!x y. P(x,y) | Q(x,y)) --> \ |
|
444 \ (!x y.P(x,y)) | (!x y.Q(x,y))"; |
|
445 by (safe_meson_tac 1); (*32 secs*) |
|
446 result(); |
|
447 |
|
448 writeln"Problem 50"; |
|
449 (*What has this to do with equality?*) |
|
450 goal HOL.thy "(! x. P(a,x) | (! y.P(x,y))) --> (? x. ! y.P(x,y))"; |
|
451 by (safe_meson_tac 1); |
|
452 result(); |
|
453 |
|
454 writeln"Problem 55"; |
|
455 |
|
456 (*Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988). |
|
457 meson_tac cannot report who killed Agatha. *) |
|
458 goal HOL.thy "lives(agatha) & lives(butler) & lives(charles) & \ |
|
459 \ (killed(agatha,agatha) | killed(butler,agatha) | killed(charles,agatha)) & \ |
|
460 \ (!x y. killed(x,y) --> hates(x,y) & ~richer(x,y)) & \ |
|
461 \ (!x. hates(agatha,x) --> ~hates(charles,x)) & \ |
|
462 \ (hates(agatha,agatha) & hates(agatha,charles)) & \ |
|
463 \ (!x. lives(x) & ~richer(x,agatha) --> hates(butler,x)) & \ |
|
464 \ (!x. hates(agatha,x) --> hates(butler,x)) & \ |
|
465 \ (!x. ~hates(x,agatha) | ~hates(x,butler) | ~hates(x,charles)) --> \ |
|
466 \ (? x. killed(x,agatha))"; |
|
467 by (safe_meson_tac 1); |
|
468 result(); |
|
469 |
|
470 writeln"Problem 57"; |
|
471 goal HOL.thy |
|
472 "P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) & \ |
|
473 \ (! x y z. P(x,y) & P(y,z) --> P(x,z)) --> P(f(a,b), f(a,c))"; |
|
474 by (safe_meson_tac 1); |
|
475 result(); |
|
476 |
|
477 writeln"Problem 58"; |
|
478 (* Challenge found on info-hol *) |
|
479 goal HOL.thy |
|
480 "! P Q R x. ? v w. ! y z. P(x) & Q(y) --> (P(v) | R(w)) & (R(z) --> Q(v))"; |
|
481 by (safe_meson_tac 1); |
|
482 result(); |
|
483 |
|
484 writeln"Problem 59"; |
|
485 goal HOL.thy "(! x. P(x) = (~P(f(x)))) --> (? x. P(x) & ~P(f(x)))"; |
|
486 by (safe_meson_tac 1); |
|
487 result(); |
|
488 |
|
489 writeln"Problem 60"; |
|
490 goal HOL.thy "! x. P(x,f(x)) = (? y. (! z. P(z,y) --> P(z,f(x))) & P(x,y))"; |
|
491 by (safe_meson_tac 1); |
|
492 result(); |
|
493 |
|
494 writeln"Reached end of file."; |
|
495 |
|
496 (*26 August 1992: loaded in 277 secs. New Jersey v 75*) |
|