author  paulson 
Mon, 26 May 1997 12:53:45 +0200  
changeset 3347  4e7dfe8ae41b 
parent 3019  ca5a7bbbee6c 
child 3842  b55686a7b22c 
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 

1912  13 
set_current_thy "HOL"; (*Boosts efficiency by omitting redundant rules*) 
14 

969  15 
goal HOL.thy "(P > Q  R) > (P>Q)  (P>R)"; 
2891  16 
by (Blast_tac 1); 
969  17 
result(); 
18 

19 
(*If and only if*) 

20 

2997
86aaab39ebb1
Without the type constraint, the inner equality was NOT a biconditional...
paulson
parents:
2922
diff
changeset

21 
goal HOL.thy "(P=Q) = (Q = (P::bool))"; 
2891  22 
by (Blast_tac 1); 
969  23 
result(); 
24 

25 
goal HOL.thy "~ (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*) 

42 
goal HOL.thy "(P>Q) = (~Q > ~P)"; 

2891  43 
by (Blast_tac 1); 
969  44 
result(); 
45 

46 
(*2*) 

47 
goal HOL.thy "(~ ~ P) = P"; 

2891  48 
by (Blast_tac 1); 
969  49 
result(); 
50 

51 
(*3*) 

52 
goal HOL.thy "~(P>Q) > (Q>P)"; 

2891  53 
by (Blast_tac 1); 
969  54 
result(); 
55 

56 
(*4*) 

57 
goal HOL.thy "(~P>Q) = (~Q > P)"; 

2891  58 
by (Blast_tac 1); 
969  59 
result(); 
60 

61 
(*5*) 

62 
goal HOL.thy "((PQ)>(PR)) > (P(Q>R))"; 

2891  63 
by (Blast_tac 1); 
969  64 
result(); 
65 

66 
(*6*) 

67 
goal HOL.thy "P  ~ P"; 

2891  68 
by (Blast_tac 1); 
969  69 
result(); 
70 

71 
(*7*) 

72 
goal HOL.thy "P  ~ ~ ~ P"; 

2891  73 
by (Blast_tac 1); 
969  74 
result(); 
75 

76 
(*8. Peirce's law*) 

77 
goal HOL.thy "((P>Q) > P) > P"; 

2891  78 
by (Blast_tac 1); 
969  79 
result(); 
80 

81 
(*9*) 

82 
goal HOL.thy "((PQ) & (~PQ) & (P ~Q)) > ~ (~P  ~Q)"; 

2891  83 
by (Blast_tac 1); 
969  84 
result(); 
85 

86 
(*10*) 

87 
goal HOL.thy "(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!!) *) 

92 
goal HOL.thy "P=P::bool"; 

2891  93 
by (Blast_tac 1); 
969  94 
result(); 
95 

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

97 
goal HOL.thy "((P = Q) = R) = (P = (Q = R))"; 

2891  98 
by (Blast_tac 1); 
969  99 
result(); 
100 

101 
(*13. Distributive law*) 

102 
goal HOL.thy "(P  (Q & R)) = ((P  Q) & (P  R))"; 

2891  103 
by (Blast_tac 1); 
969  104 
result(); 
105 

106 
(*14*) 

107 
goal HOL.thy "(P = Q) = ((Q  ~P) & (~QP))"; 

2891  108 
by (Blast_tac 1); 
969  109 
result(); 
110 

111 
(*15*) 

112 
goal HOL.thy "(P > Q) = (~P  Q)"; 

2891  113 
by (Blast_tac 1); 
969  114 
result(); 
115 

116 
(*16*) 

117 
goal HOL.thy "(P>Q)  (Q>P)"; 

2891  118 
by (Blast_tac 1); 
969  119 
result(); 
120 

121 
(*17*) 

122 
goal HOL.thy "((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 

128 
goal HOL.thy "(! x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))"; 

2891  129 
by (Blast_tac 1); 
969  130 
result(); 
131 

132 
goal HOL.thy "(? x. P>Q(x)) = (P > (? x.Q(x)))"; 

2891  133 
by (Blast_tac 1); 
969  134 
result(); 
135 

136 
goal HOL.thy "(? x.P(x)>Q) = ((! x.P(x)) > Q)"; 

2891  137 
by (Blast_tac 1); 
969  138 
result(); 
139 

140 
goal HOL.thy "((! x.P(x))  Q) = (! x. P(x)  Q)"; 

2891  141 
by (Blast_tac 1); 
969  142 
result(); 
143 

144 
(*From Wishnu Prasetya*) 

145 
goal HOL.thy 

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 

154 
(*Needs multiple instantiation of the quantifier.*) 

155 
goal HOL.thy "(! x. P(x)>P(f(x))) & P(d)>P(f(f(f(d))))"; 

2891  156 
by (Blast_tac 1); 
969  157 
result(); 
158 

159 
(*Needs double instantiation of the quantifier*) 

160 
goal HOL.thy "? x. P(x) > P(a) & P(b)"; 

2891  161 
by (Blast_tac 1); 
969  162 
result(); 
163 

164 
goal HOL.thy "? z. P(z) > (! x. P(x))"; 

2891  165 
by (Blast_tac 1); 
969  166 
result(); 
167 

168 
goal HOL.thy "? x. (? y. P(y)) > P(x)"; 

2891  169 
by (Blast_tac 1); 
969  170 
result(); 
171 

172 
writeln"Hard examples with quantifiers"; 

173 

174 
writeln"Problem 18"; 

175 
goal HOL.thy "? y. ! x. P(y)>P(x)"; 

2891  176 
by (Blast_tac 1); 
969  177 
result(); 
178 

179 
writeln"Problem 19"; 

180 
goal HOL.thy "? x. ! y z. (P(y)>Q(z)) > (P(x)>Q(x))"; 

2891  181 
by (Blast_tac 1); 
969  182 
result(); 
183 

184 
writeln"Problem 20"; 

185 
goal HOL.thy "(! x y. ? z. ! w. (P(x)&Q(y)>R(z)&S(w))) \ 

186 
\ > (? x y. P(x) & Q(y)) > (? z. R(z))"; 

2891  187 
by (Blast_tac 1); 
969  188 
result(); 
189 

190 
writeln"Problem 21"; 

191 
goal HOL.thy "(? x. P>Q(x)) & (? x. Q(x)>P) > (? x. P=Q(x))"; 

2891  192 
by (Blast_tac 1); 
969  193 
result(); 
194 

195 
writeln"Problem 22"; 

196 
goal HOL.thy "(! x. P = Q(x)) > (P = (! x. Q(x)))"; 

2891  197 
by (Blast_tac 1); 
969  198 
result(); 
199 

200 
writeln"Problem 23"; 

201 
goal HOL.thy "(! x. P  Q(x)) = (P  (! x. Q(x)))"; 

2891  202 
by (Blast_tac 1); 
969  203 
result(); 
204 

205 
writeln"Problem 24"; 

206 
goal HOL.thy "~(? x. S(x)&Q(x)) & (! x. P(x) > Q(x)R(x)) & \ 

2575  207 
\ (~(? x.P(x)) > (? x.Q(x))) & (! x. Q(x)R(x) > S(x)) \ 
969  208 
\ > (? x. P(x)&R(x))"; 
2891  209 
by (Blast_tac 1); 
969  210 
result(); 
211 

212 
writeln"Problem 25"; 

213 
goal HOL.thy "(? x. P(x)) & \ 

214 
\ (! x. L(x) > ~ (M(x) & R(x))) & \ 

215 
\ (! x. P(x) > (M(x) & L(x))) & \ 

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

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

2891  218 
by (Blast_tac 1); 
969  219 
result(); 
220 

221 
writeln"Problem 26"; 

1465  222 
goal HOL.thy "((? x. p(x)) = (? x. q(x))) & \ 
223 
\ (! x. ! y. p(x) & q(y) > (r(x) = s(y))) \ 

969  224 
\ > ((! x. p(x)>r(x)) = (! x. q(x)>s(x)))"; 
2891  225 
by (Blast_tac 1); 
969  226 
result(); 
227 

228 
writeln"Problem 27"; 

229 
goal HOL.thy "(? x. P(x) & ~Q(x)) & \ 

230 
\ (! x. P(x) > R(x)) & \ 

231 
\ (! x. M(x) & L(x) > P(x)) & \ 

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

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

2891  234 
by (Blast_tac 1); 
969  235 
result(); 
236 

237 
writeln"Problem 28. AMENDED"; 

238 
goal HOL.thy "(! x. P(x) > (! x. Q(x))) & \ 

239 
\ ((! x. Q(x)R(x)) > (? x. Q(x)&S(x))) & \ 

240 
\ ((? x.S(x)) > (! x. L(x) > M(x))) \ 

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

2891  242 
by (Blast_tac 1); 
969  243 
result(); 
244 

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

246 
goal HOL.thy "(? x. F(x)) & (? y. G(y)) \ 

247 
\ > ( ((! x. F(x)>H(x)) & (! y. G(y)>J(y))) = \ 

248 
\ (! x y. F(x) & G(y) > H(x) & J(y)))"; 

2891  249 
by (Blast_tac 1); 
969  250 
result(); 
251 

252 
writeln"Problem 30"; 

253 
goal HOL.thy "(! x. P(x)  Q(x) > ~ R(x)) & \ 

254 
\ (! x. (Q(x) > ~ S(x)) > P(x) & R(x)) \ 

255 
\ > (! x. S(x))"; 

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

259 
writeln"Problem 31"; 

260 
goal HOL.thy "~(? x.P(x) & (Q(x)  R(x))) & \ 

261 
\ (? x. L(x) & P(x)) & \ 

262 
\ (! x. ~ R(x) > M(x)) \ 

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

2891  264 
by (Blast_tac 1); 
969  265 
result(); 
266 

267 
writeln"Problem 32"; 

268 
goal HOL.thy "(! x. P(x) & (Q(x)R(x))>S(x)) & \ 

269 
\ (! x. S(x) & R(x) > L(x)) & \ 

270 
\ (! x. M(x) > R(x)) \ 

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

2891  272 
by (Blast_tac 1); 
969  273 
result(); 
274 

275 
writeln"Problem 33"; 

276 
goal HOL.thy "(! x. P(a) & (P(x)>P(b))>P(c)) = \ 

277 
\ (! x. (~P(a)  P(x)  P(c)) & (~P(a)  ~P(b)  P(c)))"; 

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

1768  281 
writeln"Problem 34 AMENDED (TWICE!!)"; 
969  282 
(*Andrews's challenge*) 
1465  283 
goal HOL.thy "((? x. ! y. p(x) = p(y)) = \ 
3019  284 
\ ((? x. q(x)) = (! y. p(y)))) = \ 
285 
\ ((? x. ! y. q(x) = q(y)) = \ 

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

2891  287 
by (Blast_tac 1); 
969  288 
result(); 
289 

290 
writeln"Problem 35"; 

291 
goal HOL.thy "? x y. P x y > (! u v. P u v)"; 

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

295 
writeln"Problem 36"; 

296 
goal HOL.thy "(! x. ? y. J x y) & \ 

297 
\ (! x. ? y. G x y) & \ 

1465  298 
\ (! x y. J x y  G x y > \ 
969  299 
\ (! z. J y z  G y z > H x z)) \ 
300 
\ > (! x. ? y. H x y)"; 

2891  301 
by (Blast_tac 1); 
969  302 
result(); 
303 

304 
writeln"Problem 37"; 

305 
goal HOL.thy "(! z. ? w. ! x. ? y. \ 

306 
\ (P x z >P y w) & P y z & (P y w > (? u.Q u w))) & \ 

307 
\ (! x z. ~(P x z) > (? y. Q y z)) & \ 

308 
\ ((? x y. Q x y) > (! x. R x x)) \ 

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

2891  310 
by (Blast_tac 1); 
969  311 
result(); 
312 

313 
writeln"Problem 38"; 

314 
goal HOL.thy 

1465  315 
"(! x. p(a) & (p(x) > (? y. p(y) & r x y)) > \ 
316 
\ (? z. ? w. p(z) & r x w & r w z)) = \ 

317 
\ (! 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

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

321 
result(); 
969  322 

323 
writeln"Problem 39"; 

324 
goal HOL.thy "~ (? x. ! y. F y x = (~ F y y))"; 

2891  325 
by (Blast_tac 1); 
969  326 
result(); 
327 

328 
writeln"Problem 40. AMENDED"; 

329 
goal HOL.thy "(? y. ! x. F x y = F x x) \ 

330 
\ > ~ (! x. ? y. ! z. F z y = (~ F z x))"; 

2891  331 
by (Blast_tac 1); 
969  332 
result(); 
333 

334 
writeln"Problem 41"; 

1465  335 
goal HOL.thy "(! z. ? y. ! x. f x y = (f x z & ~ f x x)) \ 
969  336 
\ > ~ (? z. ! x. f x z)"; 
2891  337 
by (Blast_tac 1); 
969  338 
result(); 
339 

340 
writeln"Problem 42"; 

341 
goal HOL.thy "~ (? y. ! x. p x y = (~ (? z. p x z & p z x)))"; 

2891  342 
by (Blast_tac 1); 
969  343 
result(); 
344 

2891  345 
writeln"Problem 43!!"; 
969  346 
goal HOL.thy 
1465  347 
"(! x::'a. ! y::'a. q x y = (! z. p z x = (p z y::bool))) \ 
969  348 
\ > (! x. (! y. q x y = (q y x::bool)))"; 
2891  349 
by (Blast_tac 1); 
3347  350 
result(); 
969  351 

352 
writeln"Problem 44"; 

1465  353 
goal HOL.thy "(! x. f(x) > \ 
969  354 
\ (? y. g(y) & h x y & (? y. g(y) & ~ h x y))) & \ 
1465  355 
\ (? x. j(x) & (! y. g(y) > h x y)) \ 
969  356 
\ > (? x. j(x) & ~f(x))"; 
2891  357 
by (Blast_tac 1); 
969  358 
result(); 
359 

360 
writeln"Problem 45"; 

361 
goal HOL.thy 

1465  362 
"(! x. f(x) & (! y. g(y) & h x y > j x y) \ 
363 
\ > (! y. g(y) & h x y > k(y))) & \ 

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

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

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

969  367 
\ > (? x. f(x) & ~ (? y. g(y) & h x y))"; 
2891  368 
by (Blast_tac 1); 
969  369 
result(); 
370 

371 

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

373 

374 
writeln"Problem 48"; 

375 
goal HOL.thy "(a=b  c=d) & (a=c  b=d) > a=d  b=c"; 

2891  376 
by (Blast_tac 1); 
969  377 
result(); 
378 

379 
writeln"Problem 49 NOT PROVED AUTOMATICALLY"; 

380 
(*Hard because it involves substitution for Vars; 

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

382 
goal HOL.thy "(? x y::'a. ! z. z=x  z=y) & P(a) & P(b) & (~a=b) \ 

1465  383 
\ > (! u::'a.P(u))"; 
1820  384 
by (Classical.safe_tac (!claset)); 
969  385 
by (res_inst_tac [("x","a")] allE 1); 
386 
by (assume_tac 1); 

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

388 
by (assume_tac 1); 

2891  389 
by (Blast_tac 1); 
969  390 
result(); 
391 

392 
writeln"Problem 50"; 

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

394 
goal HOL.thy "(! x. P a x  (! y.P x y)) > (? x. ! y.P x y)"; 

2891  395 
by (Blast_tac 1); 
969  396 
result(); 
397 

398 
writeln"Problem 51"; 

399 
goal HOL.thy 

400 
"(? z w. ! x y. P x y = (x=z & y=w)) > \ 

401 
\ (? z. ! x. ? w. (! y. P x y = (y=w)) = (x=z))"; 

2891  402 
by (Blast_tac 1); 
969  403 
result(); 
404 

405 
writeln"Problem 52"; 

406 
(*Almost the same as 51. *) 

407 
goal HOL.thy 

408 
"(? z w. ! x y. P x y = (x=z & y=w)) > \ 

409 
\ (? w. ! y. ? z. (! x. P x y = (x=z)) = (y=w))"; 

2891  410 
by (Blast_tac 1); 
969  411 
result(); 
412 

413 
writeln"Problem 55"; 

414 

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

416 
fast_tac DISCOVERS who killed Agatha. *) 

417 
goal HOL.thy "lives(agatha) & lives(butler) & lives(charles) & \ 

418 
\ (killed agatha agatha  killed butler agatha  killed charles agatha) & \ 

419 
\ (!x y. killed x y > hates x y & ~richer x y) & \ 

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

421 
\ (hates agatha agatha & hates agatha charles) & \ 

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

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

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

425 
\ killed ?who agatha"; 

2922  426 
by (Fast_tac 1); 
969  427 
result(); 
428 

429 
writeln"Problem 56"; 

430 
goal HOL.thy 

431 
"(! x. (? y. P(y) & x=f(y)) > P(x)) = (! x. P(x) > P(f(x)))"; 

2891  432 
by (Blast_tac 1); 
969  433 
result(); 
434 

435 
writeln"Problem 57"; 

436 
goal HOL.thy 

437 
"P (f a b) (f b c) & P (f b c) (f a c) & \ 

438 
\ (! x y z. P x y & P y z > P x z) > P (f a b) (f a c)"; 

2891  439 
by (Blast_tac 1); 
969  440 
result(); 
441 

442 
writeln"Problem 58 NOT PROVED AUTOMATICALLY"; 

443 
goal HOL.thy "(! x y. f(x)=g(y)) > (! x y. f(f(x))=f(g(y)))"; 

444 
val f_cong = read_instantiate [("f","f")] arg_cong; 

1820  445 
by (fast_tac (!claset addIs [f_cong]) 1); 
969  446 
result(); 
447 

448 
writeln"Problem 59"; 

449 
goal HOL.thy "(! x. P(x) = (~P(f(x)))) > (? x. P(x) & ~P(f(x)))"; 

2891  450 
by (Blast_tac 1); 
969  451 
result(); 
452 

453 
writeln"Problem 60"; 

454 
goal HOL.thy 

455 
"! x. P x (f x) = (? y. (! z. P z y > P z (f x)) & P x y)"; 

2891  456 
by (Blast_tac 1); 
969  457 
result(); 
458 

2715  459 
writeln"Problem 62 as corrected in JAR 18 (1997), page 135"; 
1404  460 
goal HOL.thy 
1465  461 
"(ALL x. p a & (p x > p(f x)) > p(f(f x))) = \ 
462 
\ (ALL x. (~ p a  p x  p(f(f x))) & \ 

1404  463 
\ (~ p a  ~ p(f x)  p(f(f x))))"; 
2891  464 
by (Blast_tac 1); 
1404  465 
result(); 
466 

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

469 
goal Prod.thy 

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

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

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

2891  473 
by (Blast_tac 1); 
1712  474 
result(); 
475 

476 
goal Prod.thy 

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

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

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

2891  480 
by (Blast_tac 1); 
1712  481 
result(); 
482 

483 

484 

969  485 
writeln"Reached end of file."; 