# HG changeset patch
# User paulson
# Date 882873468 -3600
# Node ID 7ba65fe66c734f5453590aad937c6463350ac861
# Parent  7a81505067460fa8afd6d7ec52ceb1651f794517
New "obvious theorems"

diff -r 7a8150506746 -r 7ba65fe66c73 src/FOL/ex/cla.ML
--- a/src/FOL/ex/cla.ML	Mon Dec 22 12:22:06 1997 +0100
+++ b/src/FOL/ex/cla.ML	Tue Dec 23 11:37:48 1997 +0100
@@ -503,6 +503,23 @@
 by (Blast_tac 1);
 result();
 
+(*From Davis, Obvious Logical Inferences, IJCAI-81, 530-531
+  Fast_tac indeed copes!*)
+goal FOL.thy "(ALL x. F(x) & ~G(x) --> (EX y. H(x,y) & J(y))) & \
+\             (EX x. K(x) & F(x) & (ALL y. H(x,y) --> K(y))) &   \
+\             (ALL x. K(x) --> ~G(x))  -->  (EX x. K(x) & J(x))";
+by (Fast_tac 1);
+result();
+
+(*From Rudnicki, Obvious Inferences, JAR 3 (1987), 383-393.  
+  It does seem obvious!*)
+goal FOL.thy
+    "(ALL x. F(x) & ~G(x) --> (EX y. H(x,y) & J(y))) &        \
+\    (EX x. K(x) & F(x) & (ALL y. H(x,y) --> K(y)))  &        \
+\    (ALL x. K(x) --> ~G(x))   -->   (EX x. K(x) --> ~G(x))";
+by (Fast_tac 1);
+result();
+
 (*Halting problem: Formulation of Li Dafa (AAR Newsletter 27, Oct 1994.)
 	author U. Egly*)
 goal FOL.thy
@@ -566,10 +583,13 @@
 (*Wed Nov 16 1994: loaded in 138s [after addition of norm_term_skip] *)
 (*Mon Nov 21 1994: loaded in 131s [DEPTH_FIRST suppressing repetitions] *)
 
-(*Tue Mar  4 1997: loaded in 93s (on pochard, version 94-7) *)
-(*Tue Mar  4 1997: loaded in 89s (on pochard) *)
-(*Thu Apr  3 1997: loaded in 44s (on pochard)--using mostly Blast_tac*)
-(*Thu Apr  3 1997: loaded in 96s (on pochard)--addition of two Halting Probs*)
-(*Thu Apr  3 1997: loaded in 98s (on pochard)--using lim-1 for all haz rules*)
-(*Tue Dec  2 1997: loaded in 107s (on pochard)--added 46; new equalSubst*)
+(*Further runtimes on pochard*)
+(*Tue Mar  4 1997: loaded in 93s (version 94-7) *)
+(*Tue Mar  4 1997: loaded in 89s*)
+(*Thu Apr  3 1997: loaded in 44s--using mostly Blast_tac*)
+(*Thu Apr  3 1997: loaded in 96s--addition of two Halting Probs*)
+(*Thu Apr  3 1997: loaded in 98s--using lim-1 for all haz rules*)
+(*Tue Dec  2 1997: loaded in 107s--added 46; new equalSubst*)
+(*Fri Dec 12 1997: loaded in 91s--faster proof reconstruction*)
+(*Thu Dec 18 1997: loaded in 94s--two new "obvious theorems" (??)*)