460 by (Blast_tac 1); |
460 by (Blast_tac 1); |
461 result(); |
461 result(); |
462 |
462 |
463 (*From Davis, Obvious Logical Inferences, IJCAI-81, 530-531 |
463 (*From Davis, Obvious Logical Inferences, IJCAI-81, 530-531 |
464 Fast_tac indeed copes!*) |
464 Fast_tac indeed copes!*) |
465 goal Product_Type.thy "(ALL x. F(x) & ~G(x) --> (EX y. H(x,y) & J(y))) & \ |
465 goal (theory "Product_Type") |
|
466 "(ALL x. F(x) & ~G(x) --> (EX y. H(x,y) & J(y))) & \ |
466 \ (EX x. K(x) & F(x) & (ALL y. H(x,y) --> K(y))) & \ |
467 \ (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 \ (ALL x. K(x) --> ~G(x)) --> (EX x. K(x) & J(x))"; |
468 by (Fast_tac 1); |
469 by (Fast_tac 1); |
469 result(); |
470 result(); |
470 |
471 |
471 (*From Rudnicki, Obvious Inferences, JAR 3 (1987), 383-393. |
472 (*From Rudnicki, Obvious Inferences, JAR 3 (1987), 383-393. |
472 It does seem obvious!*) |
473 It does seem obvious!*) |
473 goal Product_Type.thy |
474 goal (theory "Product_Type") |
474 "(ALL x. F(x) & ~G(x) --> (EX y. H(x,y) & J(y))) & \ |
475 "(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 \ (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))"; |
477 \ (ALL x. K(x) --> ~G(x)) --> (EX x. K(x) --> ~G(x))"; |
477 by (Fast_tac 1); |
478 by (Fast_tac 1); |
478 result(); |
479 result(); |
486 \ (ALL x. ~healthy(x) & cyclist(x) --> ~honest(x)) \ |
487 \ (ALL x. ~healthy(x) & cyclist(x) --> ~honest(x)) \ |
487 \ --> (ALL x. grocer(x) --> ~cyclist(x))"; |
488 \ --> (ALL x. grocer(x) --> ~cyclist(x))"; |
488 by (Blast_tac 1); |
489 by (Blast_tac 1); |
489 result(); |
490 result(); |
490 |
491 |
491 goal Product_Type.thy |
492 goal (theory "Product_Type") |
492 "(ALL x y. R(x,y) | R(y,x)) & \ |
493 "(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. 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))"; |
495 \ (ALL x y. R(x,y) --> S(x,y)) --> (ALL x y. S(x,y) --> R(x,y))"; |
495 by (Blast_tac 1); |
496 by (Blast_tac 1); |
496 result(); |
497 result(); |