src/FOL/ex/cla.ML

 
 goal FOL.thy "(ALL x.P(x)) | Q  <->  (ALL x. P(x) | Q)";
 by (fast_tac FOL_cs 1);
 result(); 
 
+(*Discussed in Avron, Gentzen-Type Systems, Resolution and Tableaux,
+  JAR 10 (265-281), 1993.  Proof is trivial!*)
+goal FOL.thy
+    "~ ((EX x.~P(x)) & ((EX x.P(x)) | (EX x.P(x) & Q(x))) & ~ (EX x.P(x)))";
+by (fast_tac FOL_cs 1);
+result();
+
 writeln"Problems requiring quantifier duplication";
 
 (*Needs multiple instantiation of ALL.*)
 goal FOL.thy "(ALL x. P(x)-->P(f(x)))  &  P(d)-->P(f(f(f(d))))";
 by (best_tac FOL_dup_cs 1);

 writeln"Problem 24";
 goal FOL.thy "~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &  \
 \    ~(EX x.P(x)) --> (EX x.Q(x)) & (ALL x. Q(x)|R(x) --> S(x))  \
 \   --> (EX x. P(x)&R(x))";
 by (fast_tac FOL_cs 1); 
-(*slow*)
 result();
 
 writeln"Problem 25";
 goal FOL.thy "(EX x. P(x)) &  \
 \       (ALL x. L(x) --> ~ (M(x) & R(x))) &  \

 writeln"Problem 26";
 goal FOL.thy "((EX x. p(x)) <-> (EX x. q(x))) &	\
 \     (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y)))	\
 \ --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))";
 by (fast_tac FOL_cs 1);
-(*slow*)
 result();
 
 writeln"Problem 27";
 goal FOL.thy "(EX x. P(x) & ~Q(x)) &   \
 \             (ALL x. P(x) --> R(x)) &   \
 \             (ALL x. M(x) & L(x) --> P(x)) &   \
 \             ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x)))  \
 \         --> (ALL x. M(x) --> ~L(x))";
 by (fast_tac FOL_cs 1); 
-(*slow*)
 result();
 
 writeln"Problem 28.  AMENDED";
 goal FOL.thy "(ALL x. P(x) --> (ALL x. Q(x))) &   \
 \       ((ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) &  \
 \       ((EX x.S(x)) --> (ALL x. L(x) --> M(x)))  \
 \   --> (ALL x. P(x) & L(x) --> M(x))";
 by (fast_tac FOL_cs 1);  
-(*slow*)
 result();
 
 writeln"Problem 29.  Essentially the same as Principia Mathematica *11.71";
 goal FOL.thy "(EX x. P(x)) & (EX y. Q(y))  \
 \   --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y))   <->     \