author  paulson 
Thu, 16 Jul 1998 10:35:31 +0200  
changeset 5150  6e2e9b92c301 
parent 4463  76769b48bd88 
child 5278  a903b66822e2 
permissions  rwrr 
1465  1 
(* Title: HOL/ex/cla 
969  2 
ID: $Id$ 
1465  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
969  4 
Copyright 1994 University of Cambridge 
5 

6 
HigherOrder Logic: predicate calculus problems 

7 

8 
Taken from FOL/cla.ML; beware of precedence of = vs <> 

9 
*) 

10 

11 
writeln"File HOL/ex/cla."; 

12 

5150  13 
context HOL.thy; 
1912  14 

5150  15 
Goal "(P > Q  R) > (P>Q)  (P>R)"; 
2891  16 
by (Blast_tac 1); 
969  17 
result(); 
18 

19 
(*If and only if*) 

20 

5150  21 
Goal "(P=Q) = (Q = (P::bool))"; 
2891  22 
by (Blast_tac 1); 
969  23 
result(); 
24 

5150  25 
Goal "~ (P = (~P))"; 
2891  26 
by (Blast_tac 1); 
969  27 
result(); 
28 

29 

30 
(*Sample problems from 

31 
F. J. Pelletier, 

32 
SeventyFive Problems for Testing Automatic Theorem Provers, 

33 
J. Automated Reasoning 2 (1986), 191216. 

34 
Errata, JAR 4 (1988), 236236. 

35 

36 
The hardest problems  judging by experience with several theorem provers, 

37 
including matrix ones  are 34 and 43. 

38 
*) 

39 

40 
writeln"Pelletier's examples"; 

41 
(*1*) 

5150  42 
Goal "(P>Q) = (~Q > ~P)"; 
2891  43 
by (Blast_tac 1); 
969  44 
result(); 
45 

46 
(*2*) 

5150  47 
Goal "(~ ~ P) = P"; 
2891  48 
by (Blast_tac 1); 
969  49 
result(); 
50 

51 
(*3*) 

5150  52 
Goal "~(P>Q) > (Q>P)"; 
2891  53 
by (Blast_tac 1); 
969  54 
result(); 
55 

56 
(*4*) 

5150  57 
Goal "(~P>Q) = (~Q > P)"; 
2891  58 
by (Blast_tac 1); 
969  59 
result(); 
60 

61 
(*5*) 

5150  62 
Goal "((PQ)>(PR)) > (P(Q>R))"; 
2891  63 
by (Blast_tac 1); 
969  64 
result(); 
65 

66 
(*6*) 

5150  67 
Goal "P  ~ P"; 
2891  68 
by (Blast_tac 1); 
969  69 
result(); 
70 

71 
(*7*) 

5150  72 
Goal "P  ~ ~ ~ P"; 
2891  73 
by (Blast_tac 1); 
969  74 
result(); 
75 

76 
(*8. Peirce's law*) 

5150  77 
Goal "((P>Q) > P) > P"; 
2891  78 
by (Blast_tac 1); 
969  79 
result(); 
80 

81 
(*9*) 

5150  82 
Goal "((PQ) & (~PQ) & (P ~Q)) > ~ (~P  ~Q)"; 
2891  83 
by (Blast_tac 1); 
969  84 
result(); 
85 

86 
(*10*) 

5150  87 
Goal "(Q>R) & (R>P&Q) & (P>QR) > (P=Q)"; 
2891  88 
by (Blast_tac 1); 
969  89 
result(); 
90 

91 
(*11. Proved in each direction (incorrectly, says Pelletier!!) *) 

5150  92 
Goal "P=(P::bool)"; 
2891  93 
by (Blast_tac 1); 
969  94 
result(); 
95 

96 
(*12. "Dijkstra's law"*) 

5150  97 
Goal "((P = Q) = R) = (P = (Q = R))"; 
2891  98 
by (Blast_tac 1); 
969  99 
result(); 
100 

101 
(*13. Distributive law*) 

5150  102 
Goal "(P  (Q & R)) = ((P  Q) & (P  R))"; 
2891  103 
by (Blast_tac 1); 
969  104 
result(); 
105 

106 
(*14*) 

5150  107 
Goal "(P = Q) = ((Q  ~P) & (~QP))"; 
2891  108 
by (Blast_tac 1); 
969  109 
result(); 
110 

111 
(*15*) 

5150  112 
Goal "(P > Q) = (~P  Q)"; 
2891  113 
by (Blast_tac 1); 
969  114 
result(); 
115 

116 
(*16*) 

5150  117 
Goal "(P>Q)  (Q>P)"; 
2891  118 
by (Blast_tac 1); 
969  119 
result(); 
120 

121 
(*17*) 

5150  122 
Goal "((P & (Q>R))>S) = ((~P  Q  S) & (~P  ~R  S))"; 
2891  123 
by (Blast_tac 1); 
969  124 
result(); 
125 

126 
writeln"Classical Logic: examples with quantifiers"; 

127 

5150  128 
Goal "(! x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))"; 
2891  129 
by (Blast_tac 1); 
969  130 
result(); 
131 

5150  132 
Goal "(? x. P>Q(x)) = (P > (? x. Q(x)))"; 
2891  133 
by (Blast_tac 1); 
969  134 
result(); 
135 

5150  136 
Goal "(? x. P(x)>Q) = ((! x. P(x)) > Q)"; 
2891  137 
by (Blast_tac 1); 
969  138 
result(); 
139 

5150  140 
Goal "((! x. P(x))  Q) = (! x. P(x)  Q)"; 
2891  141 
by (Blast_tac 1); 
969  142 
result(); 
143 

144 
(*From Wishnu Prasetya*) 

5150  145 
Goal 
969  146 
"(!s. q(s) > r(s)) & ~r(s) & (!s. ~r(s) & ~q(s) > p(t)  q(t)) \ 
147 
\ > p(t)  r(t)"; 

2891  148 
by (Blast_tac 1); 
969  149 
result(); 
150 

151 

152 
writeln"Problems requiring quantifier duplication"; 

153 

5150  154 
(*Theorem B of Peter Andrews, Theorem Proving via General Matings, 
155 
JACM 28 (1981).*) 

156 
Goal "(EX x. ALL y. P(x) = P(y)) > ((EX x. P(x)) = (ALL y. P(y)))"; 

157 
by (Blast_tac 1); 

158 
result(); 

159 

969  160 
(*Needs multiple instantiation of the quantifier.*) 
5150  161 
Goal "(! x. P(x)>P(f(x))) & P(d)>P(f(f(f(d))))"; 
2891  162 
by (Blast_tac 1); 
969  163 
result(); 
164 

165 
(*Needs double instantiation of the quantifier*) 

5150  166 
Goal "? x. P(x) > P(a) & P(b)"; 
2891  167 
by (Blast_tac 1); 
969  168 
result(); 
169 

5150  170 
Goal "? z. P(z) > (! x. P(x))"; 
2891  171 
by (Blast_tac 1); 
969  172 
result(); 
173 

5150  174 
Goal "? x. (? y. P(y)) > P(x)"; 
2891  175 
by (Blast_tac 1); 
969  176 
result(); 
177 

178 
writeln"Hard examples with quantifiers"; 

179 

180 
writeln"Problem 18"; 

5150  181 
Goal "? y. ! x. P(y)>P(x)"; 
2891  182 
by (Blast_tac 1); 
969  183 
result(); 
184 

185 
writeln"Problem 19"; 

5150  186 
Goal "? x. ! y z. (P(y)>Q(z)) > (P(x)>Q(x))"; 
2891  187 
by (Blast_tac 1); 
969  188 
result(); 
189 

190 
writeln"Problem 20"; 

5150  191 
Goal "(! x y. ? z. ! w. (P(x)&Q(y)>R(z)&S(w))) \ 
969  192 
\ > (? x y. P(x) & Q(y)) > (? z. R(z))"; 
2891  193 
by (Blast_tac 1); 
969  194 
result(); 
195 

196 
writeln"Problem 21"; 

5150  197 
Goal "(? x. P>Q(x)) & (? x. Q(x)>P) > (? x. P=Q(x))"; 
2891  198 
by (Blast_tac 1); 
969  199 
result(); 
200 

201 
writeln"Problem 22"; 

5150  202 
Goal "(! x. P = Q(x)) > (P = (! x. Q(x)))"; 
2891  203 
by (Blast_tac 1); 
969  204 
result(); 
205 

206 
writeln"Problem 23"; 

5150  207 
Goal "(! x. P  Q(x)) = (P  (! x. Q(x)))"; 
2891  208 
by (Blast_tac 1); 
969  209 
result(); 
210 

211 
writeln"Problem 24"; 

5150  212 
Goal "~(? x. S(x)&Q(x)) & (! x. P(x) > Q(x)R(x)) & \ 
3842  213 
\ (~(? x. P(x)) > (? x. Q(x))) & (! x. Q(x)R(x) > S(x)) \ 
969  214 
\ > (? x. P(x)&R(x))"; 
2891  215 
by (Blast_tac 1); 
969  216 
result(); 
217 

218 
writeln"Problem 25"; 

5150  219 
Goal "(? x. P(x)) & \ 
969  220 
\ (! x. L(x) > ~ (M(x) & R(x))) & \ 
221 
\ (! x. P(x) > (M(x) & L(x))) & \ 

222 
\ ((! x. P(x)>Q(x))  (? x. P(x)&R(x))) \ 

223 
\ > (? x. Q(x)&P(x))"; 

2891  224 
by (Blast_tac 1); 
969  225 
result(); 
226 

227 
writeln"Problem 26"; 

5150  228 
Goal "((? x. p(x)) = (? x. q(x))) & \ 
1465  229 
\ (! x. ! y. p(x) & q(y) > (r(x) = s(y))) \ 
969  230 
\ > ((! x. p(x)>r(x)) = (! x. q(x)>s(x)))"; 
2891  231 
by (Blast_tac 1); 
969  232 
result(); 
233 

234 
writeln"Problem 27"; 

5150  235 
Goal "(? x. P(x) & ~Q(x)) & \ 
969  236 
\ (! x. P(x) > R(x)) & \ 
237 
\ (! x. M(x) & L(x) > P(x)) & \ 

238 
\ ((? x. R(x) & ~ Q(x)) > (! x. L(x) > ~ R(x))) \ 

239 
\ > (! x. M(x) > ~L(x))"; 

2891  240 
by (Blast_tac 1); 
969  241 
result(); 
242 

243 
writeln"Problem 28. AMENDED"; 

5150  244 
Goal "(! x. P(x) > (! x. Q(x))) & \ 
969  245 
\ ((! x. Q(x)R(x)) > (? x. Q(x)&S(x))) & \ 
3842  246 
\ ((? x. S(x)) > (! x. L(x) > M(x))) \ 
969  247 
\ > (! x. P(x) & L(x) > M(x))"; 
2891  248 
by (Blast_tac 1); 
969  249 
result(); 
250 

251 
writeln"Problem 29. Essentially the same as Principia Mathematica *11.71"; 

5150  252 
Goal "(? x. F(x)) & (? y. G(y)) \ 
969  253 
\ > ( ((! x. F(x)>H(x)) & (! y. G(y)>J(y))) = \ 
254 
\ (! x y. F(x) & G(y) > H(x) & J(y)))"; 

2891  255 
by (Blast_tac 1); 
969  256 
result(); 
257 

258 
writeln"Problem 30"; 

5150  259 
Goal "(! x. P(x)  Q(x) > ~ R(x)) & \ 
969  260 
\ (! x. (Q(x) > ~ S(x)) > P(x) & R(x)) \ 
261 
\ > (! x. S(x))"; 

2891  262 
by (Blast_tac 1); 
969  263 
result(); 
264 

265 
writeln"Problem 31"; 

5150  266 
Goal "~(? x. P(x) & (Q(x)  R(x))) & \ 
969  267 
\ (? x. L(x) & P(x)) & \ 
268 
\ (! x. ~ R(x) > M(x)) \ 

269 
\ > (? x. L(x) & M(x))"; 

2891  270 
by (Blast_tac 1); 
969  271 
result(); 
272 

273 
writeln"Problem 32"; 

5150  274 
Goal "(! x. P(x) & (Q(x)R(x))>S(x)) & \ 
969  275 
\ (! x. S(x) & R(x) > L(x)) & \ 
276 
\ (! x. M(x) > R(x)) \ 

277 
\ > (! x. P(x) & M(x) > L(x))"; 

2891  278 
by (Blast_tac 1); 
969  279 
result(); 
280 

281 
writeln"Problem 33"; 

5150  282 
Goal "(! x. P(a) & (P(x)>P(b))>P(c)) = \ 
969  283 
\ (! x. (~P(a)  P(x)  P(c)) & (~P(a)  ~P(b)  P(c)))"; 
2891  284 
by (Blast_tac 1); 
969  285 
result(); 
286 

1768  287 
writeln"Problem 34 AMENDED (TWICE!!)"; 
969  288 
(*Andrews's challenge*) 
5150  289 
Goal "((? x. ! y. p(x) = p(y)) = \ 
3019  290 
\ ((? x. q(x)) = (! y. p(y)))) = \ 
291 
\ ((? x. ! y. q(x) = q(y)) = \ 

292 
\ ((? x. p(x)) = (! y. q(y))))"; 

2891  293 
by (Blast_tac 1); 
969  294 
result(); 
295 

296 
writeln"Problem 35"; 

5150  297 
Goal "? x y. P x y > (! u v. P u v)"; 
2891  298 
by (Blast_tac 1); 
969  299 
result(); 
300 

301 
writeln"Problem 36"; 

5150  302 
Goal "(! x. ? y. J x y) & \ 
969  303 
\ (! x. ? y. G x y) & \ 
1465  304 
\ (! x y. J x y  G x y > \ 
969  305 
\ (! z. J y z  G y z > H x z)) \ 
306 
\ > (! x. ? y. H x y)"; 

2891  307 
by (Blast_tac 1); 
969  308 
result(); 
309 

310 
writeln"Problem 37"; 

5150  311 
Goal "(! z. ? w. ! x. ? y. \ 
3842  312 
\ (P x z >P y w) & P y z & (P y w > (? u. Q u w))) & \ 
969  313 
\ (! x z. ~(P x z) > (? y. Q y z)) & \ 
314 
\ ((? x y. Q x y) > (! x. R x x)) \ 

315 
\ > (! x. ? y. R x y)"; 

2891  316 
by (Blast_tac 1); 
969  317 
result(); 
318 

319 
writeln"Problem 38"; 

5150  320 
Goal 
1465  321 
"(! x. p(a) & (p(x) > (? y. p(y) & r x y)) > \ 
322 
\ (? z. ? w. p(z) & r x w & r w z)) = \ 

323 
\ (! x. (~p(a)  p(x)  (? z. ? w. p(z) & r x w & r w z)) & \ 

1716
8dbf9ca61ce5
Restored a proof of Pelletier #38  mysteriously deleted
paulson
parents:
1712
diff
changeset

324 
\ (~p(a)  ~(? y. p(y) & r x y)  \ 
969  325 
\ (? z. ? w. p(z) & r x w & r w z)))"; 
2891  326 
by (Blast_tac 1); (*beats fast_tac!*) 
1716
8dbf9ca61ce5
Restored a proof of Pelletier #38  mysteriously deleted
paulson
parents:
1712
diff
changeset

327 
result(); 
969  328 

329 
writeln"Problem 39"; 

5150  330 
Goal "~ (? x. ! y. F y x = (~ F y y))"; 
2891  331 
by (Blast_tac 1); 
969  332 
result(); 
333 

334 
writeln"Problem 40. AMENDED"; 

5150  335 
Goal "(? y. ! x. F x y = F x x) \ 
969  336 
\ > ~ (! x. ? y. ! z. F z y = (~ F z x))"; 
2891  337 
by (Blast_tac 1); 
969  338 
result(); 
339 

340 
writeln"Problem 41"; 

5150  341 
Goal "(! z. ? y. ! x. f x y = (f x z & ~ f x x)) \ 
969  342 
\ > ~ (? z. ! x. f x z)"; 
2891  343 
by (Blast_tac 1); 
969  344 
result(); 
345 

346 
writeln"Problem 42"; 

5150  347 
Goal "~ (? y. ! x. p x y = (~ (? z. p x z & p z x)))"; 
2891  348 
by (Blast_tac 1); 
969  349 
result(); 
350 

2891  351 
writeln"Problem 43!!"; 
5150  352 
Goal 
1465  353 
"(! x::'a. ! y::'a. q x y = (! z. p z x = (p z y::bool))) \ 
969  354 
\ > (! x. (! y. q x y = (q y x::bool)))"; 
2891  355 
by (Blast_tac 1); 
3347  356 
result(); 
969  357 

358 
writeln"Problem 44"; 

5150  359 
Goal "(! x. f(x) > \ 
969  360 
\ (? y. g(y) & h x y & (? y. g(y) & ~ h x y))) & \ 
1465  361 
\ (? x. j(x) & (! y. g(y) > h x y)) \ 
969  362 
\ > (? x. j(x) & ~f(x))"; 
2891  363 
by (Blast_tac 1); 
969  364 
result(); 
365 

366 
writeln"Problem 45"; 

5150  367 
Goal 
1465  368 
"(! x. f(x) & (! y. g(y) & h x y > j x y) \ 
369 
\ > (! y. g(y) & h x y > k(y))) & \ 

370 
\ ~ (? y. l(y) & k(y)) & \ 

371 
\ (? x. f(x) & (! y. h x y > l(y)) \ 

372 
\ & (! y. g(y) & h x y > j x y)) \ 

969  373 
\ > (? x. f(x) & ~ (? y. g(y) & h x y))"; 
2891  374 
by (Blast_tac 1); 
969  375 
result(); 
376 

377 

378 
writeln"Problems (mainly) involving equality or functions"; 

379 

380 
writeln"Problem 48"; 

5150  381 
Goal "(a=b  c=d) & (a=c  b=d) > a=d  b=c"; 
2891  382 
by (Blast_tac 1); 
969  383 
result(); 
384 

385 
writeln"Problem 49 NOT PROVED AUTOMATICALLY"; 

386 
(*Hard because it involves substitution for Vars; 

387 
the type constraint ensures that x,y,z have the same type as a,b,u. *) 

5150  388 
Goal "(? x y::'a. ! z. z=x  z=y) & P(a) & P(b) & (~a=b) \ 
3842  389 
\ > (! u::'a. P(u))"; 
4153  390 
by (Classical.Safe_tac); 
969  391 
by (res_inst_tac [("x","a")] allE 1); 
392 
by (assume_tac 1); 

393 
by (res_inst_tac [("x","b")] allE 1); 

394 
by (assume_tac 1); 

4353
d565d2197a5f
updated for latest Blast_tac, which treats equality differently
paulson
parents:
4153
diff
changeset

395 
by (Fast_tac 1); (*Blast_tac's treatment of equality can't do it*) 
969  396 
result(); 
397 

398 
writeln"Problem 50"; 

399 
(*What has this to do with equality?*) 

5150  400 
Goal "(! x. P a x  (! y. P x y)) > (? x. ! y. P x y)"; 
2891  401 
by (Blast_tac 1); 
969  402 
result(); 
403 

404 
writeln"Problem 51"; 

5150  405 
Goal 
969  406 
"(? z w. ! x y. P x y = (x=z & y=w)) > \ 
407 
\ (? z. ! x. ? w. (! y. P x y = (y=w)) = (x=z))"; 

2891  408 
by (Blast_tac 1); 
969  409 
result(); 
410 

411 
writeln"Problem 52"; 

412 
(*Almost the same as 51. *) 

5150  413 
Goal 
969  414 
"(? z w. ! x y. P x y = (x=z & y=w)) > \ 
415 
\ (? w. ! y. ? z. (! x. P x y = (x=z)) = (y=w))"; 

2891  416 
by (Blast_tac 1); 
969  417 
result(); 
418 

419 
writeln"Problem 55"; 

420 

421 
(*Nonequational version, from Manthey and Bry, CADE9 (Springer, 1988). 

422 
fast_tac DISCOVERS who killed Agatha. *) 

5150  423 
Goal "lives(agatha) & lives(butler) & lives(charles) & \ 
969  424 
\ (killed agatha agatha  killed butler agatha  killed charles agatha) & \ 
425 
\ (!x y. killed x y > hates x y & ~richer x y) & \ 

426 
\ (!x. hates agatha x > ~hates charles x) & \ 

427 
\ (hates agatha agatha & hates agatha charles) & \ 

428 
\ (!x. lives(x) & ~richer x agatha > hates butler x) & \ 

429 
\ (!x. hates agatha x > hates butler x) & \ 

430 
\ (!x. ~hates x agatha  ~hates x butler  ~hates x charles) > \ 

431 
\ killed ?who agatha"; 

2922  432 
by (Fast_tac 1); 
969  433 
result(); 
434 

435 
writeln"Problem 56"; 

5150  436 
Goal 
969  437 
"(! x. (? y. P(y) & x=f(y)) > P(x)) = (! x. P(x) > P(f(x)))"; 
2891  438 
by (Blast_tac 1); 
969  439 
result(); 
440 

441 
writeln"Problem 57"; 

5150  442 
Goal 
969  443 
"P (f a b) (f b c) & P (f b c) (f a c) & \ 
444 
\ (! x y z. P x y & P y z > P x z) > P (f a b) (f a c)"; 

2891  445 
by (Blast_tac 1); 
969  446 
result(); 
447 

448 
writeln"Problem 58 NOT PROVED AUTOMATICALLY"; 

5150  449 
Goal "(! x y. f(x)=g(y)) > (! x y. f(f(x))=f(g(y)))"; 
969  450 
val f_cong = read_instantiate [("f","f")] arg_cong; 
4089  451 
by (fast_tac (claset() addIs [f_cong]) 1); 
969  452 
result(); 
453 

454 
writeln"Problem 59"; 

5150  455 
Goal "(! x. P(x) = (~P(f(x)))) > (? x. P(x) & ~P(f(x)))"; 
2891  456 
by (Blast_tac 1); 
969  457 
result(); 
458 

459 
writeln"Problem 60"; 

5150  460 
Goal 
969  461 
"! x. P x (f x) = (? y. (! z. P z y > P z (f x)) & P x y)"; 
2891  462 
by (Blast_tac 1); 
969  463 
result(); 
464 

2715  465 
writeln"Problem 62 as corrected in JAR 18 (1997), page 135"; 
5150  466 
Goal "(ALL x. p a & (p x > p(f x)) > p(f(f x))) = \ 
467 
\ (ALL x. (~ p a  p x  p(f(f x))) & \ 

468 
\ (~ p a  ~ p(f x)  p(f(f x))))"; 

2891  469 
by (Blast_tac 1); 
1404  470 
result(); 
471 

4463  472 
(*From Davis, Obvious Logical Inferences, IJCAI81, 530531 
473 
Fast_tac indeed copes!*) 

474 
goal Prod.thy "(ALL x. F(x) & ~G(x) > (EX y. H(x,y) & J(y))) & \ 

475 
\ (EX x. K(x) & F(x) & (ALL y. H(x,y) > K(y))) & \ 

476 
\ (ALL x. K(x) > ~G(x)) > (EX x. K(x) & J(x))"; 

477 
by (Fast_tac 1); 

478 
result(); 

479 

1712  480 
(*From Rudnicki, Obvious Inferences, JAR 3 (1987), 383393. 
481 
It does seem obvious!*) 

482 
goal Prod.thy 

483 
"(ALL x. F(x) & ~G(x) > (EX y. H(x,y) & J(y))) & \ 

484 
\ (EX x. K(x) & F(x) & (ALL y. H(x,y) > K(y))) & \ 

485 
\ (ALL x. K(x) > ~G(x)) > (EX x. K(x) > ~G(x))"; 

4463  486 
by (Fast_tac 1); 
1712  487 
result(); 
488 

489 
goal Prod.thy 

490 
"(ALL x y. R(x,y)  R(y,x)) & \ 

491 
\ (ALL x y. S(x,y) & S(y,x) > x=y) & \ 

492 
\ (ALL x y. R(x,y) > S(x,y)) > (ALL x y. S(x,y) > R(x,y))"; 

2891  493 
by (Blast_tac 1); 
1712  494 
result(); 
495 

496 

497 

969  498 
writeln"Reached end of file."; 