equal
deleted
inserted
replaced
258 by (Int.fast_tac 1); |
258 by (Int.fast_tac 1); |
259 result(); |
259 result(); |
260 |
260 |
261 writeln"Problem 21"; |
261 writeln"Problem 21"; |
262 goal IFOL.thy "(EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> ~~(EX x. P<->Q(x))"; |
262 goal IFOL.thy "(EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> ~~(EX x. P<->Q(x))"; |
263 (*NOT PROVED*) |
263 (*NOT PROVED; needs quantifier duplication*) |
264 |
264 |
265 writeln"Problem 22"; |
265 writeln"Problem 22"; |
266 goal IFOL.thy "(ALL x. P <-> Q(x)) --> (P <-> (ALL x. Q(x)))"; |
266 goal IFOL.thy "(ALL x. P <-> Q(x)) --> (P <-> (ALL x. Q(x)))"; |
267 by (Int.fast_tac 1); |
267 by (Int.fast_tac 1); |
268 result(); |
268 result(); |
272 by (Int.best_tac 1); |
272 by (Int.best_tac 1); |
273 result(); |
273 result(); |
274 |
274 |
275 writeln"Problem 24"; |
275 writeln"Problem 24"; |
276 goal IFOL.thy "~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) & \ |
276 goal IFOL.thy "~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) & \ |
277 \ ~(EX x.P(x)) --> (EX x.Q(x)) & (ALL x. Q(x)|R(x) --> S(x)) \ |
277 \ (~(EX x.P(x)) --> (EX x.Q(x))) & (ALL x. Q(x)|R(x) --> S(x)) \ |
278 \ --> (EX x. P(x)&R(x))"; |
278 \ --> ~~(EX x. P(x)&R(x))"; |
|
279 (*Not clear why fast_tac, best_tac, ASTAR and ITER_DEEPEN all take forever*) |
|
280 by Int.safe_tac; |
|
281 by (etac impE 1); |
|
282 by (Int.fast_tac 1); |
279 by (Int.fast_tac 1); |
283 by (Int.fast_tac 1); |
280 result(); |
284 result(); |
281 |
285 |
282 writeln"Problem 25"; |
286 writeln"Problem 25"; |
283 goal IFOL.thy "(EX x. P(x)) & \ |
287 goal IFOL.thy "(EX x. P(x)) & \ |