author  paulson 
Mon, 21 Apr 1997 10:14:31 +0200  
changeset 2997  86aaab39ebb1 
parent 2922  580647a879cf 
child 3019  ca5a7bbbee6c 
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)) = \ 
284 
\ ((? x. q(x)) = (! y. p(y)))) = \ 

285 
\ ((? x. ! y. q(x) = q(y)) = \ 

969  286 
\ ((? x. p(x)) = (! y. q(y))))"; 
2891  287 
by (Blast_tac 1); 
969  288 
(*slower with smaller bounds*) 
289 
result(); 

290 

291 
writeln"Problem 35"; 

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

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

296 
writeln"Problem 36"; 

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

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

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

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

305 
writeln"Problem 37"; 

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

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

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

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

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

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

314 
writeln"Problem 38"; 

315 
goal HOL.thy 

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

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

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

322 
result(); 
969  323 

324 
writeln"Problem 39"; 

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

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

329 
writeln"Problem 40. AMENDED"; 

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

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

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

335 
writeln"Problem 41"; 

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

341 
writeln"Problem 42"; 

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

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

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

352 

353 
writeln"Problem 44"; 

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

361 
writeln"Problem 45"; 

362 
goal HOL.thy 

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

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

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

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

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

372 

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

374 

375 
writeln"Problem 48"; 

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

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

380 
writeln"Problem 49 NOT PROVED AUTOMATICALLY"; 

381 
(*Hard because it involves substitution for Vars; 

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

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

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

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

389 
by (assume_tac 1); 

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

393 
writeln"Problem 50"; 

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

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

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

399 
writeln"Problem 51"; 

400 
goal HOL.thy 

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

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

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

406 
writeln"Problem 52"; 

407 
(*Almost the same as 51. *) 

408 
goal HOL.thy 

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

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

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

414 
writeln"Problem 55"; 

415 

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

417 
fast_tac DISCOVERS who killed Agatha. *) 

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

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

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

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

422 
\ (hates agatha agatha & hates agatha charles) & \ 

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

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

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

426 
\ killed ?who agatha"; 

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

430 
writeln"Problem 56"; 

431 
goal HOL.thy 

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

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

436 
writeln"Problem 57"; 

437 
goal HOL.thy 

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

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

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

443 
writeln"Problem 58 NOT PROVED AUTOMATICALLY"; 

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

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

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

449 
writeln"Problem 59"; 

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

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

454 
writeln"Problem 60"; 

455 
goal HOL.thy 

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

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

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

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

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

470 
goal Prod.thy 

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

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

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

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

477 
goal Prod.thy 

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

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

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

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

484 

485 

969  486 
writeln"Reached end of file."; 