author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 10212  33fe2d701ddd 
child 11025  a70b796d9af8 
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*) 

5278  145 
Goal "(!s. q(s) > r(s)) & ~r(s) & (!s. ~r(s) & ~q(s) > p(t)  q(t)) \ 
969  146 
\ > p(t)  r(t)"; 
2891  147 
by (Blast_tac 1); 
969  148 
result(); 
149 

150 

151 
writeln"Problems requiring quantifier duplication"; 

152 

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

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

156 
by (Blast_tac 1); 

157 
result(); 

158 

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

164 
(*Needs double instantiation of the quantifier*) 

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

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

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

177 
writeln"Hard examples with quantifiers"; 

178 

179 
writeln"Problem 18"; 

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

184 
writeln"Problem 19"; 

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

189 
writeln"Problem 20"; 

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

195 
writeln"Problem 21"; 

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

200 
writeln"Problem 22"; 

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

205 
writeln"Problem 23"; 

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

210 
writeln"Problem 24"; 

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

217 
writeln"Problem 25"; 

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

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

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

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

226 
writeln"Problem 26"; 

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

233 
writeln"Problem 27"; 

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

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

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

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

242 
writeln"Problem 28. AMENDED"; 

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

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

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

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

257 
writeln"Problem 30"; 

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

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

264 
writeln"Problem 31"; 

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

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

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

272 
writeln"Problem 32"; 

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

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

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

280 
writeln"Problem 33"; 

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

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

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

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

295 
writeln"Problem 35"; 

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

300 
writeln"Problem 36"; 

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

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

309 
writeln"Problem 37"; 

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

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

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

318 
writeln"Problem 38"; 

5278  319 
Goal "(! x. p(a) & (p(x) > (? y. p(y) & r x y)) > \ 
1465  320 
\ (? z. ? w. p(z) & r x w & r w z)) = \ 
321 
\ (! 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

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

325 
result(); 
969  326 

327 
writeln"Problem 39"; 

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

332 
writeln"Problem 40. AMENDED"; 

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

338 
writeln"Problem 41"; 

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

344 
writeln"Problem 42"; 

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

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

355 
writeln"Problem 44"; 

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

363 
writeln"Problem 45"; 

5278  364 
Goal "(! x. f(x) & (! y. g(y) & h x y > j x y) \ 
1465  365 
\ > (! y. g(y) & h x y > k(y))) & \ 
366 
\ ~ (? y. l(y) & k(y)) & \ 

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

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

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

373 

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

375 

376 
writeln"Problem 48"; 

5150  377 
Goal "(a=b  c=d) & (a=c  b=d) > a=d  b=c"; 
2891  378 
by (Blast_tac 1); 
969  379 
result(); 
380 

381 
writeln"Problem 49 NOT PROVED AUTOMATICALLY"; 

382 
(*Hard because it involves substitution for Vars; 

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

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

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

390 
by (assume_tac 1); 

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

391 
by (Fast_tac 1); (*Blast_tac's treatment of equality can't do it*) 
969  392 
result(); 
393 

394 
writeln"Problem 50"; 

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

5150  396 
Goal "(! x. P a x  (! y. P x y)) > (? x. ! y. P x y)"; 
2891  397 
by (Blast_tac 1); 
969  398 
result(); 
399 

400 
writeln"Problem 51"; 

5278  401 
Goal "(? z w. ! x y. P x y = (x=z & y=w)) > \ 
969  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. *) 

5278  408 
Goal "(? z w. ! x y. P x y = (x=z & y=w)) > \ 
969  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. *) 

5150  417 
Goal "lives(agatha) & lives(butler) & lives(charles) & \ 
969  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"; 

5278  430 
Goal "(! x. (? y. P(y) & x=f(y)) > P(x)) = (! x. P(x) > P(f(x)))"; 
2891  431 
by (Blast_tac 1); 
969  432 
result(); 
433 

434 
writeln"Problem 57"; 

5278  435 
Goal "P (f a b) (f b c) & P (f b c) (f a c) & \ 
969  436 
\ (! x y z. P x y & P y z > P x z) > P (f a b) (f a c)"; 
2891  437 
by (Blast_tac 1); 
969  438 
result(); 
439 

440 
writeln"Problem 58 NOT PROVED AUTOMATICALLY"; 

5150  441 
Goal "(! x y. f(x)=g(y)) > (! x y. f(f(x))=f(g(y)))"; 
969  442 
val f_cong = read_instantiate [("f","f")] arg_cong; 
4089  443 
by (fast_tac (claset() addIs [f_cong]) 1); 
969  444 
result(); 
445 

446 
writeln"Problem 59"; 

5150  447 
Goal "(! x. P(x) = (~P(f(x)))) > (? x. P(x) & ~P(f(x)))"; 
2891  448 
by (Blast_tac 1); 
969  449 
result(); 
450 

451 
writeln"Problem 60"; 

5278  452 
Goal "! x. P x (f x) = (? y. (! z. P z y > P z (f x)) & P x y)"; 
2891  453 
by (Blast_tac 1); 
969  454 
result(); 
455 

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

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

2891  460 
by (Blast_tac 1); 
1404  461 
result(); 
462 

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

10212  465 
goal Product_Type.thy "(ALL x. F(x) & ~G(x) > (EX y. H(x,y) & J(y))) & \ 
4463  466 
\ (EX x. K(x) & F(x) & (ALL y. H(x,y) > K(y))) & \ 
467 
\ (ALL x. K(x) > ~G(x)) > (EX x. K(x) & J(x))"; 

468 
by (Fast_tac 1); 

469 
result(); 

470 

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

10212  473 
goal Product_Type.thy 
1712  474 
"(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) > ~G(x))"; 

4463  477 
by (Fast_tac 1); 
1712  478 
result(); 
479 

6799
95abcc002a21
new classical example from Lewis Carroll via S G Pulman
paulson
parents:
5278
diff
changeset

480 
(*Attributed to Lewis Carroll by S. G. Pulman. The first or last assumption 
95abcc002a21
new classical example from Lewis Carroll via S G Pulman
paulson
parents:
5278
diff
changeset

481 
can be deleted.*) 
95abcc002a21
new classical example from Lewis Carroll via S G Pulman
paulson
parents:
5278
diff
changeset

482 
Goal "(ALL x. honest(x) & industrious(x) > healthy(x)) & \ 
95abcc002a21
new classical example from Lewis Carroll via S G Pulman
paulson
parents:
5278
diff
changeset

483 
\ ~ (EX x. grocer(x) & healthy(x)) & \ 
95abcc002a21
new classical example from Lewis Carroll via S G Pulman
paulson
parents:
5278
diff
changeset

484 
\ (ALL x. industrious(x) & grocer(x) > honest(x)) & \ 
95abcc002a21
new classical example from Lewis Carroll via S G Pulman
paulson
parents:
5278
diff
changeset

485 
\ (ALL x. cyclist(x) > industrious(x)) & \ 
95abcc002a21
new classical example from Lewis Carroll via S G Pulman
paulson
parents:
5278
diff
changeset

486 
\ (ALL x. ~healthy(x) & cyclist(x) > ~honest(x)) \ 
95abcc002a21
new classical example from Lewis Carroll via S G Pulman
paulson
parents:
5278
diff
changeset

487 
\ > (ALL x. grocer(x) > ~cyclist(x))"; 
95abcc002a21
new classical example from Lewis Carroll via S G Pulman
paulson
parents:
5278
diff
changeset

488 
by (Blast_tac 1); 
95abcc002a21
new classical example from Lewis Carroll via S G Pulman
paulson
parents:
5278
diff
changeset

489 
result(); 
95abcc002a21
new classical example from Lewis Carroll via S G Pulman
paulson
parents:
5278
diff
changeset

490 

10212  491 
goal Product_Type.thy 
1712  492 
"(ALL x y. R(x,y)  R(y,x)) & \ 
493 
\ (ALL x y. S(x,y) & S(y,x) > x=y) & \ 

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

2891  495 
by (Blast_tac 1); 
1712  496 
result(); 
497 

498 

499 

969  500 
writeln"Reached end of file."; 