# HG changeset patch
# User paulson
# Date 1065621461 -7200
# Node ID 4dc1329026729120b8f79ed172fb8dadbd5ddf2e
# Parent  9fdea25f9ebb6d7805710ca134d275866802a1e5
Merging of ex/cla.ML and ex/mesontest.ML to ex/Classical.thy

diff -r 9fdea25f9ebb -r 4dc132902672 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Oct 03 12:36:16 2003 +0200
+++ b/src/HOL/IsaMakefile	Wed Oct 08 15:57:41 2003 +0200
@@ -592,7 +592,7 @@
   ex/NatSum.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy ex/Puzzle.thy \
   ex/Qsort.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy \
   ex/Ring.ML ex/Ring.thy ex/StringEx.thy ex/SVC_Oracle.ML ex/SVC_Oracle.thy \
-  ex/Tarski.thy ex/Tuple.thy ex/cla.ML ex/mesontest.ML \
+  ex/Tarski.thy ex/Tuple.thy ex/Classical.thy \
   ex/mesontest2.ML ex/mesontest2.thy ex/set.thy ex/svc_funcs.ML \
   ex/svc_test.ML ex/svc_test.thy ex/document/root.bib ex/document/root.tex
 	@$(ISATOOL) usedir $(OUT)/HOL ex
diff -r 9fdea25f9ebb -r 4dc132902672 src/HOL/ex/Classical.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Classical.thy	Wed Oct 08 15:57:41 2003 +0200
@@ -0,0 +1,786 @@
+(*  Title:      HOL/ex/Classical
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994  University of Cambridge
+*)
+
+header{*Classical Predicate Calculus Problems*}
+
+theory Classical = Main:
+
+subsection{*Traditional Classical Reasoner*}
+
+text{*Taken from @{text "FOL/cla.ML"}. When porting examples from first-order
+logic, beware of the precedence of @{text "="} versus @{text "\<leftrightarrow>"}.*}
+
+lemma "(P --> Q | R) --> (P-->Q) | (P-->R)"
+by blast
+
+text{*If and only if*}
+
+lemma "(P=Q) = (Q = (P::bool))"
+by blast
+
+lemma "~ (P = (~P))"
+by blast
+
+
+text{*Sample problems from 
+  F. J. Pelletier, 
+  Seventy-Five Problems for Testing Automatic Theorem Provers,
+  J. Automated Reasoning 2 (1986), 191-216.
+  Errata, JAR 4 (1988), 236-236.
+
+The hardest problems -- judging by experience with several theorem provers,
+including matrix ones -- are 34 and 43.
+*}
+
+subsubsection{*Pelletier's examples*}
+
+text{*1*}
+lemma "(P-->Q)  =  (~Q --> ~P)"
+by blast
+
+text{*2*}
+lemma "(~ ~ P) =  P"
+by blast
+
+text{*3*}
+lemma "~(P-->Q) --> (Q-->P)"
+by blast
+
+text{*4*}
+lemma "(~P-->Q)  =  (~Q --> P)"
+by blast
+
+text{*5*}
+lemma "((P|Q)-->(P|R)) --> (P|(Q-->R))"
+by blast
+
+text{*6*}
+lemma "P | ~ P"
+by blast
+
+text{*7*}
+lemma "P | ~ ~ ~ P"
+by blast
+
+text{*8.  Peirce's law*}
+lemma "((P-->Q) --> P)  -->  P"
+by blast
+
+text{*9*}
+lemma "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
+by blast
+
+text{*10*}
+lemma "(Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P=Q)"
+by blast
+
+text{*11.  Proved in each direction (incorrectly, says Pelletier!!)  *}
+lemma "P=(P::bool)"
+by blast
+
+text{*12.  "Dijkstra's law"*}
+lemma "((P = Q) = R) = (P = (Q = R))"
+by blast
+
+text{*13.  Distributive law*}
+lemma "(P | (Q & R)) = ((P | Q) & (P | R))"
+by blast
+
+text{*14*}
+lemma "(P = Q) = ((Q | ~P) & (~Q|P))"
+by blast
+
+text{*15*}
+lemma "(P --> Q) = (~P | Q)"
+by blast
+
+text{*16*}
+lemma "(P-->Q) | (Q-->P)"
+by blast
+
+text{*17*}
+lemma "((P & (Q-->R))-->S)  =  ((~P | Q | S) & (~P | ~R | S))"
+by blast
+
+subsubsection{*Classical Logic: examples with quantifiers*}
+
+lemma "(\<forall>x. P(x) & Q(x)) = ((\<forall>x. P(x)) & (\<forall>x. Q(x)))"
+by blast
+
+lemma "(\<exists>x. P-->Q(x))  =  (P --> (\<exists>x. Q(x)))"
+by blast
+
+lemma "(\<exists>x. P(x)-->Q) = ((\<forall>x. P(x)) --> Q)"
+by blast
+
+lemma "((\<forall>x. P(x)) | Q)  =  (\<forall>x. P(x) | Q)"
+by blast
+
+text{*From Wishnu Prasetya*}
+lemma "(\<forall>s. q(s) --> r(s)) & ~r(s) & (\<forall>s. ~r(s) & ~q(s) --> p(t) | q(t))  
+    --> p(t) | r(t)"
+by blast
+
+
+subsubsection{*Problems requiring quantifier duplication*}
+
+text{*Theorem B of Peter Andrews, Theorem Proving via General Matings, 
+  JACM 28 (1981).*}
+lemma "(\<exists>x. \<forall>y. P(x) = P(y)) --> ((\<exists>x. P(x)) = (\<forall>y. P(y)))"
+by blast
+
+text{*Needs multiple instantiation of the quantifier.*}
+lemma "(\<forall>x. P(x)-->P(f(x)))  &  P(d)-->P(f(f(f(d))))"
+by blast
+
+text{*Needs double instantiation of the quantifier*}
+lemma "\<exists>x. P(x) --> P(a) & P(b)"
+by blast
+
+lemma "\<exists>z. P(z) --> (\<forall>x. P(x))"
+by blast
+
+lemma "\<exists>x. (\<exists>y. P(y)) --> P(x)"
+by blast
+
+subsubsection{*Hard examples with quantifiers*}
+
+text{*Problem 18*}
+lemma "\<exists>y. \<forall>x. P(y)-->P(x)"
+by blast
+
+text{*Problem 19*}
+lemma "\<exists>x. \<forall>y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))"
+by blast
+
+text{*Problem 20*}
+lemma "(\<forall>x y. \<exists>z. \<forall>w. (P(x)&Q(y)-->R(z)&S(w)))      
+    --> (\<exists>x y. P(x) & Q(y)) --> (\<exists>z. R(z))"
+by blast
+
+text{*Problem 21*}
+lemma "(\<exists>x. P-->Q(x)) & (\<exists>x. Q(x)-->P) --> (\<exists>x. P=Q(x))"
+by blast
+
+text{*Problem 22*}
+lemma "(\<forall>x. P = Q(x))  -->  (P = (\<forall>x. Q(x)))"
+by blast
+
+text{*Problem 23*}
+lemma "(\<forall>x. P | Q(x))  =  (P | (\<forall>x. Q(x)))"
+by blast
+
+text{*Problem 24*}
+lemma "~(\<exists>x. S(x)&Q(x)) & (\<forall>x. P(x) --> Q(x)|R(x)) &   
+     (~(\<exists>x. P(x)) --> (\<exists>x. Q(x))) & (\<forall>x. Q(x)|R(x) --> S(x))   
+    --> (\<exists>x. P(x)&R(x))"
+by blast
+
+text{*Problem 25*}
+lemma "(\<exists>x. P(x)) &   
+        (\<forall>x. L(x) --> ~ (M(x) & R(x))) &   
+        (\<forall>x. P(x) --> (M(x) & L(x))) &    
+        ((\<forall>x. P(x)-->Q(x)) | (\<exists>x. P(x)&R(x)))   
+    --> (\<exists>x. Q(x)&P(x))"
+by blast
+
+text{*Problem 26*}
+lemma "((\<exists>x. p(x)) = (\<exists>x. q(x))) &      
+      (\<forall>x. \<forall>y. p(x) & q(y) --> (r(x) = s(y)))  
+  --> ((\<forall>x. p(x)-->r(x)) = (\<forall>x. q(x)-->s(x)))"
+by blast
+
+text{*Problem 27*}
+lemma "(\<exists>x. P(x) & ~Q(x)) &    
+              (\<forall>x. P(x) --> R(x)) &    
+              (\<forall>x. M(x) & L(x) --> P(x)) &    
+              ((\<exists>x. R(x) & ~ Q(x)) --> (\<forall>x. L(x) --> ~ R(x)))   
+          --> (\<forall>x. M(x) --> ~L(x))"
+by blast
+
+text{*Problem 28.  AMENDED*}
+lemma "(\<forall>x. P(x) --> (\<forall>x. Q(x))) &    
+        ((\<forall>x. Q(x)|R(x)) --> (\<exists>x. Q(x)&S(x))) &   
+        ((\<exists>x. S(x)) --> (\<forall>x. L(x) --> M(x)))   
+    --> (\<forall>x. P(x) & L(x) --> M(x))"
+by blast
+
+text{*Problem 29.  Essentially the same as Principia Mathematica *11.71*}
+lemma "(\<exists>x. F(x)) & (\<exists>y. G(y))   
+    --> ( ((\<forall>x. F(x)-->H(x)) & (\<forall>y. G(y)-->J(y)))  =    
+          (\<forall>x y. F(x) & G(y) --> H(x) & J(y)))"
+by blast
+
+text{*Problem 30*}
+lemma "(\<forall>x. P(x) | Q(x) --> ~ R(x)) &  
+        (\<forall>x. (Q(x) --> ~ S(x)) --> P(x) & R(x))   
+    --> (\<forall>x. S(x))"
+by blast
+
+text{*Problem 31*}
+lemma "~(\<exists>x. P(x) & (Q(x) | R(x))) &  
+        (\<exists>x. L(x) & P(x)) &  
+        (\<forall>x. ~ R(x) --> M(x))   
+    --> (\<exists>x. L(x) & M(x))"
+by blast
+
+text{*Problem 32*}
+lemma "(\<forall>x. P(x) & (Q(x)|R(x))-->S(x)) &  
+        (\<forall>x. S(x) & R(x) --> L(x)) &  
+        (\<forall>x. M(x) --> R(x))   
+    --> (\<forall>x. P(x) & M(x) --> L(x))"
+by blast
+
+text{*Problem 33*}
+lemma "(\<forall>x. P(a) & (P(x)-->P(b))-->P(c))  =     
+     (\<forall>x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))"
+by blast
+
+text{*Problem 34  AMENDED (TWICE!!)*}
+text{*Andrews's challenge*}
+lemma "((\<exists>x. \<forall>y. p(x) = p(y))  =                
+               ((\<exists>x. q(x)) = (\<forall>y. p(y))))   =     
+              ((\<exists>x. \<forall>y. q(x) = q(y))  =           
+               ((\<exists>x. p(x)) = (\<forall>y. q(y))))"
+by blast
+
+text{*Problem 35*}
+lemma "\<exists>x y. P x y -->  (\<forall>u v. P u v)"
+by blast
+
+text{*Problem 36*}
+lemma "(\<forall>x. \<exists>y. J x y) &  
+        (\<forall>x. \<exists>y. G x y) &  
+        (\<forall>x y. J x y | G x y -->        
+        (\<forall>z. J y z | G y z --> H x z))    
+    --> (\<forall>x. \<exists>y. H x y)"
+by blast
+
+text{*Problem 37*}
+lemma "(\<forall>z. \<exists>w. \<forall>x. \<exists>y.  
+           (P x z -->P y w) & P y z & (P y w --> (\<exists>u. Q u w))) &  
+        (\<forall>x z. ~(P x z) --> (\<exists>y. Q y z)) &  
+        ((\<exists>x y. Q x y) --> (\<forall>x. R x x))   
+    --> (\<forall>x. \<exists>y. R x y)"
+by blast
+
+text{*Problem 38*}
+lemma "(\<forall>x. p(a) & (p(x) --> (\<exists>y. p(y) & r x y)) -->             
+           (\<exists>z. \<exists>w. p(z) & r x w & r w z))  =                  
+     (\<forall>x. (~p(a) | p(x) | (\<exists>z. \<exists>w. p(z) & r x w & r w z)) &   
+           (~p(a) | ~(\<exists>y. p(y) & r x y) |                       
+            (\<exists>z. \<exists>w. p(z) & r x w & r w z)))"
+by blast (*beats fast!*)
+
+text{*Problem 39*}
+lemma "~ (\<exists>x. \<forall>y. F y x = (~ F y y))"
+by blast
+
+text{*Problem 40.  AMENDED*}
+lemma "(\<exists>y. \<forall>x. F x y = F x x)   
+        -->  ~ (\<forall>x. \<exists>y. \<forall>z. F z y = (~ F z x))"
+by blast
+
+text{*Problem 41*}
+lemma "(\<forall>z. \<exists>y. \<forall>x. f x y = (f x z & ~ f x x))         
+               --> ~ (\<exists>z. \<forall>x. f x z)"
+by blast
+
+text{*Problem 42*}
+lemma "~ (\<exists>y. \<forall>x. p x y = (~ (\<exists>z. p x z & p z x)))"
+by blast
+
+text{*Problem 43!!*}
+lemma "(\<forall>x::'a. \<forall>y::'a. q x y = (\<forall>z. p z x = (p z y::bool)))    
+  --> (\<forall>x. (\<forall>y. q x y = (q y x::bool)))"
+by blast
+
+text{*Problem 44*}
+lemma "(\<forall>x. f(x) -->                                     
+              (\<exists>y. g(y) & h x y & (\<exists>y. g(y) & ~ h x y)))  &    
+              (\<exists>x. j(x) & (\<forall>y. g(y) --> h x y))                
+              --> (\<exists>x. j(x) & ~f(x))"
+by blast
+
+text{*Problem 45*}
+lemma "(\<forall>x. f(x) & (\<forall>y. g(y) & h x y --> j x y)  
+                      --> (\<forall>y. g(y) & h x y --> k(y))) &        
+     ~ (\<exists>y. l(y) & k(y)) &                                      
+     (\<exists>x. f(x) & (\<forall>y. h x y --> l(y))                          
+                & (\<forall>y. g(y) & h x y --> j x y))                 
+      --> (\<exists>x. f(x) & ~ (\<exists>y. g(y) & h x y))"
+by blast
+
+
+subsubsection{*Problems (mainly) involving equality or functions*}
+
+text{*Problem 48*}
+lemma "(a=b | c=d) & (a=c | b=d) --> a=d | b=c"
+by blast
+
+text{*Problem 49  NOT PROVED AUTOMATICALLY*}
+text{*Hard because it involves substitution for Vars
+  the type constraint ensures that x,y,z have the same type as a,b,u. *}
+lemma "(\<exists>x y::'a. \<forall>z. z=x | z=y) & P(a) & P(b) & (~a=b)  
+                --> (\<forall>u::'a. P(u))"
+apply safe
+apply (rule_tac x = a in allE, assumption)
+apply (rule_tac x = b in allE, assumption, fast)  --{*blast's treatment of equality can't do it*}
+done
+
+text{*Problem 50.  (What has this to do with equality?) *}
+lemma "(\<forall>x. P a x | (\<forall>y. P x y)) --> (\<exists>x. \<forall>y. P x y)"
+by blast
+
+text{*Problem 51*}
+lemma "(\<exists>z w. \<forall>x y. P x y = (x=z & y=w)) -->   
+     (\<exists>z. \<forall>x. \<exists>w. (\<forall>y. P x y = (y=w)) = (x=z))"
+by blast
+
+text{*Problem 52. Almost the same as 51. *}
+lemma "(\<exists>z w. \<forall>x y. P x y = (x=z & y=w)) -->   
+     (\<exists>w. \<forall>y. \<exists>z. (\<forall>x. P x y = (x=z)) = (y=w))"
+by blast
+
+text{*Problem 55*}
+
+text{*Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988).
+  fast DISCOVERS who killed Agatha. *}
+lemma "lives(agatha) & lives(butler) & lives(charles) &  
+   (killed agatha agatha | killed butler agatha | killed charles agatha) &  
+   (\<forall>x y. killed x y --> hates x y & ~richer x y) &  
+   (\<forall>x. hates agatha x --> ~hates charles x) &  
+   (hates agatha agatha & hates agatha charles) &  
+   (\<forall>x. lives(x) & ~richer x agatha --> hates butler x) &  
+   (\<forall>x. hates agatha x --> hates butler x) &  
+   (\<forall>x. ~hates x agatha | ~hates x butler | ~hates x charles) -->  
+    killed ?who agatha"
+by fast
+
+text{*Problem 56*}
+lemma "(\<forall>x. (\<exists>y. P(y) & x=f(y)) --> P(x)) = (\<forall>x. P(x) --> P(f(x)))"
+by blast
+
+text{*Problem 57*}
+lemma "P (f a b) (f b c) & P (f b c) (f a c) &  
+     (\<forall>x y z. P x y & P y z --> P x z)    -->   P (f a b) (f a c)"
+by blast
+
+text{*Problem 58  NOT PROVED AUTOMATICALLY*}
+lemma "(\<forall>x y. f(x)=g(y)) --> (\<forall>x y. f(f(x))=f(g(y)))"
+by (fast intro: arg_cong [of concl: f])
+
+text{*Problem 59*}
+lemma "(\<forall>x. P(x) = (~P(f(x)))) --> (\<exists>x. P(x) & ~P(f(x)))"
+by blast
+
+text{*Problem 60*}
+lemma "\<forall>x. P x (f x) = (\<exists>y. (\<forall>z. P z y --> P z (f x)) & P x y)"
+by blast
+
+text{*Problem 62 as corrected in JAR 18 (1997), page 135*}
+lemma "(\<forall>x. p a & (p x --> p(f x)) --> p(f(f x)))  =    
+      (\<forall>x. (~ p a | p x | p(f(f x))) &                         
+              (~ p a | ~ p(f x) | p(f(f x))))"
+by blast
+
+text{*From Davis, Obvious Logical Inferences, IJCAI-81, 530-531
+  fast indeed copes!*}
+lemma "(\<forall>x. F(x) & ~G(x) --> (\<exists>y. H(x,y) & J(y))) &  
+       (\<exists>x. K(x) & F(x) & (\<forall>y. H(x,y) --> K(y))) &    
+       (\<forall>x. K(x) --> ~G(x))  -->  (\<exists>x. K(x) & J(x))"
+by fast
+
+text{*From Rudnicki, Obvious Inferences, JAR 3 (1987), 383-393.  
+  It does seem obvious!*}
+lemma "(\<forall>x. F(x) & ~G(x) --> (\<exists>y. H(x,y) & J(y))) &         
+       (\<exists>x. K(x) & F(x) & (\<forall>y. H(x,y) --> K(y)))  &         
+       (\<forall>x. K(x) --> ~G(x))   -->   (\<exists>x. K(x) --> ~G(x))"
+by fast
+
+text{*Attributed to Lewis Carroll by S. G. Pulman.  The first or last 
+assumption can be deleted.*}
+lemma "(\<forall>x. honest(x) & industrious(x) --> healthy(x)) &  
+      ~ (\<exists>x. grocer(x) & healthy(x)) &  
+      (\<forall>x. industrious(x) & grocer(x) --> honest(x)) &  
+      (\<forall>x. cyclist(x) --> industrious(x)) &  
+      (\<forall>x. ~healthy(x) & cyclist(x) --> ~honest(x))   
+      --> (\<forall>x. grocer(x) --> ~cyclist(x))"
+by blast
+
+lemma "(\<forall>x y. R(x,y) | R(y,x)) &                 
+       (\<forall>x y. S(x,y) & S(y,x) --> x=y) &         
+       (\<forall>x y. R(x,y) --> S(x,y))    -->   (\<forall>x y. S(x,y) --> R(x,y))"
+by blast
+
+
+subsection{*Model Elimination Prover*}
+
+text{*The "small example" from Bezem, Hendriks and de Nivelle,
+Automatic Proof Construction in Type Theory Using Resolution,
+JAR 29: 3-4 (2002), pages 253-275 *}
+lemma "(\<forall>x y z. R(x,y) & R(y,z) --> R(x,z)) &
+       (\<forall>x. \<exists>y. R(x,y)) -->
+       ~ (\<forall>x. P x = (\<forall>y. R(x,y) --> ~ P y))"
+by (tactic{*safe_best_meson_tac 1*})
+    --{*In contrast, @{text meson} is SLOW: 15s on a 1.8GHz machine!*}
+
+
+subsubsection{*Pelletier's examples*}
+text{*1*}
+lemma "(P --> Q)  =  (~Q --> ~P)"
+by meson
+
+text{*2*}
+lemma "(~ ~ P) =  P"
+by meson
+
+text{*3*}
+lemma "~(P-->Q) --> (Q-->P)"
+by meson
+
+text{*4*}
+lemma "(~P-->Q)  =  (~Q --> P)"
+by meson
+
+text{*5*}
+lemma "((P|Q)-->(P|R)) --> (P|(Q-->R))"
+by meson
+
+text{*6*}
+lemma "P | ~ P"
+by meson
+
+text{*7*}
+lemma "P | ~ ~ ~ P"
+by meson
+
+text{*8.  Peirce's law*}
+lemma "((P-->Q) --> P)  -->  P"
+by meson
+
+text{*9*}
+lemma "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
+by meson
+
+text{*10*}
+lemma "(Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P=Q)"
+by meson
+
+text{*11.  Proved in each direction (incorrectly, says Pelletier!!)  *}
+lemma "P=(P::bool)"
+by meson
+
+text{*12.  "Dijkstra's law"*}
+lemma "((P = Q) = R) = (P = (Q = R))"
+by meson
+
+text{*13.  Distributive law*}
+lemma "(P | (Q & R)) = ((P | Q) & (P | R))"
+by meson
+
+text{*14*}
+lemma "(P = Q) = ((Q | ~P) & (~Q|P))"
+by meson
+
+text{*15*}
+lemma "(P --> Q) = (~P | Q)"
+by meson
+
+text{*16*}
+lemma "(P-->Q) | (Q-->P)"
+by meson
+
+text{*17*}
+lemma "((P & (Q-->R))-->S)  =  ((~P | Q | S) & (~P | ~R | S))"
+by meson
+
+subsubsection{*Classical Logic: examples with quantifiers*}
+
+lemma "(\<forall>x. P x & Q x) = ((\<forall>x. P x) & (\<forall>x. Q x))"
+by meson
+
+lemma "(\<exists>x. P --> Q x)  =  (P --> (\<exists>x. Q x))"
+by meson
+
+lemma "(\<exists>x. P x --> Q) = ((\<forall>x. P x) --> Q)"
+by meson
+
+lemma "((\<forall>x. P x) | Q)  =  (\<forall>x. P x | Q)"
+by meson
+
+lemma "(\<forall>x. P x --> P(f x))  &  P d --> P(f(f(f d)))"
+by meson
+
+text{*Needs double instantiation of EXISTS*}
+lemma "\<exists>x. P x --> P a & P b"
+by meson
+
+lemma "\<exists>z. P z --> (\<forall>x. P x)"
+by meson
+
+subsubsection{*Hard examples with quantifiers*}
+
+text{*Problem 18*}
+lemma "\<exists>y. \<forall>x. P y --> P x"
+by meson
+
+text{*Problem 19*}
+lemma "\<exists>x. \<forall>y z. (P y --> Q z) --> (P x --> Q x)"
+by meson
+
+text{*Problem 20*}
+lemma "(\<forall>x y. \<exists>z. \<forall>w. (P x & Q y --> R z & S w))      
+    --> (\<exists>x y. P x & Q y) --> (\<exists>z. R z)"
+by meson
+
+text{*Problem 21*}
+lemma "(\<exists>x. P --> Q x) & (\<exists>x. Q x --> P) --> (\<exists>x. P=Q x)"
+by meson
+
+text{*Problem 22*}
+lemma "(\<forall>x. P = Q x)  -->  (P = (\<forall>x. Q x))"
+by meson
+
+text{*Problem 23*}
+lemma "(\<forall>x. P | Q x)  =  (P | (\<forall>x. Q x))"
+by meson
+
+text{*Problem 24*}  (*The first goal clause is useless*)
+lemma "~(\<exists>x. S x & Q x) & (\<forall>x. P x --> Q x | R x) &   
+      (~(\<exists>x. P x) --> (\<exists>x. Q x)) & (\<forall>x. Q x | R x --> S x)   
+    --> (\<exists>x. P x & R x)"
+by meson
+
+text{*Problem 25*}
+lemma "(\<exists>x. P x) &   
+      (\<forall>x. L x --> ~ (M x & R x)) &   
+      (\<forall>x. P x --> (M x & L x)) &    
+      ((\<forall>x. P x --> Q x) | (\<exists>x. P x & R x))   
+    --> (\<exists>x. Q x & P x)"
+by meson
+
+text{*Problem 26; has 24 Horn clauses*}
+lemma "((\<exists>x. p x) = (\<exists>x. q x)) &      
+      (\<forall>x. \<forall>y. p x & q y --> (r x = s y))  
+  --> ((\<forall>x. p x --> r x) = (\<forall>x. q x --> s x))"
+by meson
+
+text{*Problem 27; has 13 Horn clauses*}
+lemma "(\<exists>x. P x & ~Q x) &    
+      (\<forall>x. P x --> R x) &    
+      (\<forall>x. M x & L x --> P x) &    
+      ((\<exists>x. R x & ~ Q x) --> (\<forall>x. L x --> ~ R x))   
+      --> (\<forall>x. M x --> ~L x)"
+by meson
+
+text{*Problem 28.  AMENDED; has 14 Horn clauses*}
+lemma "(\<forall>x. P x --> (\<forall>x. Q x)) &    
+      ((\<forall>x. Q x | R x) --> (\<exists>x. Q x & S x)) &   
+      ((\<exists>x. S x) --> (\<forall>x. L x --> M x))   
+    --> (\<forall>x. P x & L x --> M x)"
+by meson
+
+text{*Problem 29.  Essentially the same as Principia Mathematica
+*11.71.  62 Horn clauses*}
+lemma "(\<exists>x. F x) & (\<exists>y. G y)   
+    --> ( ((\<forall>x. F x --> H x) & (\<forall>y. G y --> J y))  =    
+          (\<forall>x y. F x & G y --> H x & J y))"
+by meson
+
+
+text{*Problem 30*}
+lemma "(\<forall>x. P x | Q x --> ~ R x) & (\<forall>x. (Q x --> ~ S x) --> P x & R x)   
+       --> (\<forall>x. S x)"
+by meson
+
+text{*Problem 31; has 10 Horn clauses; first negative clauses is useless*}
+lemma "~(\<exists>x. P x & (Q x | R x)) &  
+      (\<exists>x. L x & P x) &  
+      (\<forall>x. ~ R x --> M x)   
+    --> (\<exists>x. L x & M x)"
+by meson
+
+text{*Problem 32*}
+lemma "(\<forall>x. P x & (Q x | R x)-->S x) &  
+      (\<forall>x. S x & R x --> L x) &  
+      (\<forall>x. M x --> R x)   
+    --> (\<forall>x. P x & M x --> L x)"
+by meson
+
+text{*Problem 33; has 55 Horn clauses*}
+lemma "(\<forall>x. P a & (P x --> P b)-->P c)  =     
+      (\<forall>x. (~P a | P x | P c) & (~P a | ~P b | P c))"
+by meson
+
+text{*Problem 34  AMENDED (TWICE!!); has 924 Horn clauses*}
+text{*Andrews's challenge*}
+lemma "((\<exists>x. \<forall>y. p x = p y)  =                
+       ((\<exists>x. q x) = (\<forall>y. p y)))     =        
+      ((\<exists>x. \<forall>y. q x = q y)  =                
+       ((\<exists>x. p x) = (\<forall>y. q y)))"
+by meson
+
+text{*Problem 35*}
+lemma "\<exists>x y. P x y -->  (\<forall>u v. P u v)"
+by meson
+
+text{*Problem 36; has 15 Horn clauses*}
+lemma "(\<forall>x. \<exists>y. J x y) &  
+      (\<forall>x. \<exists>y. G x y) &  
+      (\<forall>x y. J x y | G x y -->        
+      (\<forall>z. J y z | G y z --> H x z))    
+    --> (\<forall>x. \<exists>y. H x y)"
+by meson
+
+text{*Problem 37; has 10 Horn clauses*}
+lemma "(\<forall>z. \<exists>w. \<forall>x. \<exists>y.  
+           (P x z --> P y w) & P y z & (P y w --> (\<exists>u. Q u w))) &  
+      (\<forall>x z. ~P x z --> (\<exists>y. Q y z)) &  
+      ((\<exists>x y. Q x y) --> (\<forall>x. R x x))   
+    --> (\<forall>x. \<exists>y. R x y)"
+by meson --{*causes unification tracing messages*}
+
+
+text{*Problem 38*}  text{*Quite hard: 422 Horn clauses!!*}
+lemma "(\<forall>x. p a & (p x --> (\<exists>y. p y & r x y)) -->             
+           (\<exists>z. \<exists>w. p z & r x w & r w z))  =                  
+      (\<forall>x. (~p a | p x | (\<exists>z. \<exists>w. p z & r x w & r w z)) &   
+            (~p a | ~(\<exists>y. p y & r x y) |                       
+             (\<exists>z. \<exists>w. p z & r x w & r w z)))"
+by meson
+
+text{*Problem 39*}
+lemma "~ (\<exists>x. \<forall>y. F y x = (~F y y))"
+by meson
+
+text{*Problem 40.  AMENDED*}
+lemma "(\<exists>y. \<forall>x. F x y = F x x)   
+      -->  ~ (\<forall>x. \<exists>y. \<forall>z. F z y = (~F z x))"
+by meson
+
+text{*Problem 41*}
+lemma "(\<forall>z. (\<exists>y. (\<forall>x. f x y = (f x z & ~ f x x))))     
+      --> ~ (\<exists>z. \<forall>x. f x z)"
+by meson
+
+text{*Problem 42*}
+lemma "~ (\<exists>y. \<forall>x. p x y = (~ (\<exists>z. p x z & p z x)))"
+by meson
+
+text{*Problem 43  NOW PROVED AUTOMATICALLY!!*}
+lemma "(\<forall>x. \<forall>y. q x y = (\<forall>z. p z x = (p z y::bool)))   
+      --> (\<forall>x. (\<forall>y. q x y = (q y x::bool)))"
+by meson
+
+text{*Problem 44: 13 Horn clauses; 7-step proof*}
+lemma "(\<forall>x. f x -->                                     
+            (\<exists>y. g y & h x y & (\<exists>y. g y & ~ h x y)))  &    
+      (\<exists>x. j x & (\<forall>y. g y --> h x y))                
+      --> (\<exists>x. j x & ~f x)"
+by meson
+
+text{*Problem 45; has 27 Horn clauses; 54-step proof*}
+lemma "(\<forall>x. f x & (\<forall>y. g y & h x y --> j x y)         
+            --> (\<forall>y. g y & h x y --> k y)) &        
+      ~ (\<exists>y. l y & k y) &                                     
+      (\<exists>x. f x & (\<forall>y. h x y --> l y)                         
+                & (\<forall>y. g y & h x y --> j x y))              
+      --> (\<exists>x. f x & ~ (\<exists>y. g y & h x y))"
+by meson
+
+text{*Problem 46; has 26 Horn clauses; 21-step proof*}
+lemma "(\<forall>x. f x & (\<forall>y. f y & h y x --> g y) --> g x) &       
+      ((\<exists>x. f x & ~g x) -->                                     
+      (\<exists>x. f x & ~g x & (\<forall>y. f y & ~g y --> j x y))) &     
+      (\<forall>x y. f x & f y & h x y --> ~j y x)                     
+      --> (\<forall>x. f x --> g x)"
+by meson
+
+text{*Problem 47.  Schubert's Steamroller*}
+        text{*26 clauses; 63 Horn clauses
+          87094 inferences so far.  Searching to depth 36*}
+lemma "(\<forall>x. P1 x --> P0 x) & (\<exists>x. P1 x) &      
+      (\<forall>x. P2 x --> P0 x) & (\<exists>x. P2 x) &      
+      (\<forall>x. P3 x --> P0 x) & (\<exists>x. P3 x) &      
+      (\<forall>x. P4 x --> P0 x) & (\<exists>x. P4 x) &      
+      (\<forall>x. P5 x --> P0 x) & (\<exists>x. P5 x) &      
+      (\<forall>x. Q1 x --> Q0 x) & (\<exists>x. Q1 x) &      
+      (\<forall>x. P0 x --> ((\<forall>y. Q0 y-->R x y) |     
+                       (\<forall>y. P0 y & S y x &      
+                            (\<exists>z. Q0 z&R y z) --> R x y))) &    
+      (\<forall>x y. P3 y & (P5 x|P4 x) --> S x y) &         
+      (\<forall>x y. P3 x & P2 y --> S x y) &         
+      (\<forall>x y. P2 x & P1 y --> S x y) &         
+      (\<forall>x y. P1 x & (P2 y|Q1 y) --> ~R x y) &        
+      (\<forall>x y. P3 x & P4 y --> R x y) &         
+      (\<forall>x y. P3 x & P5 y --> ~R x y) &        
+      (\<forall>x. (P4 x|P5 x) --> (\<exists>y. Q0 y & R x y))       
+      --> (\<exists>x y. P0 x & P0 y & (\<exists>z. Q1 z & R y z & R x y))"
+by (tactic{*safe_best_meson_tac 1*})
+    --{*Considerably faster than @{text meson}, 
+        which does iterative deepening rather than best-first search*}
+
+text{*The Los problem. Circulated by John Harrison*}
+lemma "(\<forall>x y z. P x y & P y z --> P x z) &       
+      (\<forall>x y z. Q x y & Q y z --> Q x z) &              
+      (\<forall>x y. P x y --> P y x) &                        
+      (\<forall>x y. P x y | Q x y)                            
+      --> (\<forall>x y. P x y) | (\<forall>x y. Q x y)"
+by meson
+
+text{*A similar example, suggested by Johannes Schumann and
+ credited to Pelletier*}
+lemma "(\<forall>x y z. P x y --> P y z --> P x z) -->  
+      (\<forall>x y z. Q x y --> Q y z --> Q x z) -->  
+      (\<forall>x y. Q x y --> Q y x) -->  (\<forall>x y. P x y | Q x y) -->  
+      (\<forall>x y. P x y) | (\<forall>x y. Q x y)"
+by meson
+
+text{*Problem 50.  What has this to do with equality?*}
+lemma "(\<forall>x. P a x | (\<forall>y. P x y)) --> (\<exists>x. \<forall>y. P x y)"
+by meson
+
+text{*Problem 55*}
+
+text{*Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988).
+  @{text meson} cannot report who killed Agatha. *}
+lemma "lives agatha & lives butler & lives charles &  
+      (killed agatha agatha | killed butler agatha | killed charles agatha) &  
+      (\<forall>x y. killed x y --> hates x y & ~richer x y) &  
+      (\<forall>x. hates agatha x --> ~hates charles x) &  
+      (hates agatha agatha & hates agatha charles) &  
+      (\<forall>x. lives x & ~richer x agatha --> hates butler x) &  
+      (\<forall>x. hates agatha x --> hates butler x) &  
+      (\<forall>x. ~hates x agatha | ~hates x butler | ~hates x charles) -->  
+      (\<exists>x. killed x agatha)"
+by meson
+
+text{*Problem 57*}
+lemma "P (f a b) (f b c) & P (f b c) (f a c) &  
+      (\<forall>x y z. P x y & P y z --> P x z)    -->   P (f a b) (f a c)"
+by meson
+
+text{*Problem 58*}
+text{* Challenge found on info-hol *}
+lemma "\<forall>P Q R x. \<exists>v w. \<forall>y z. P x & Q y --> (P v | R w) & (R z --> Q v)"
+by meson
+
+text{*Problem 59*}
+lemma "(\<forall>x. P x = (~P(f x))) --> (\<exists>x. P x & ~P(f x))"
+by meson
+
+text{*Problem 60*}
+lemma "\<forall>x. P x (f x) = (\<exists>y. (\<forall>z. P z y --> P z (f x)) & P x y)"
+by meson
+
+text{*Problem 62 as corrected in JAR 18 (1997), page 135*}
+lemma "(\<forall>x. p a & (p x --> p(f x)) --> p(f(f x)))  =    
+      (\<forall>x. (~ p a | p x | p(f(f x))) &                         
+              (~ p a | ~ p(f x) | p(f(f x))))"
+by meson
+
+end
diff -r 9fdea25f9ebb -r 4dc132902672 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Fri Oct 03 12:36:16 2003 +0200
+++ b/src/HOL/ex/ROOT.ML	Wed Oct 08 15:57:41 2003 +0200
@@ -20,8 +20,7 @@
 
 time_use_thy "NatSum";
 time_use_thy "Intuitionistic";
-time_use     "cla.ML";
-time_use     "mesontest.ML";
+time_use_thy "Classical";
 time_use_thy "mesontest2";
 time_use_thy "PresburgerEx";
 time_use_thy "BT";
diff -r 9fdea25f9ebb -r 4dc132902672 src/HOL/ex/cla.ML
--- a/src/HOL/ex/cla.ML	Fri Oct 03 12:36:16 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,501 +0,0 @@
-(*  Title:      HOL/ex/cla
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1994  University of Cambridge
-
-Higher-Order Logic: predicate calculus problems
-
-Taken from FOL/cla.ML; beware of precedence of = vs <->
-*)
-
-writeln"File HOL/ex/cla.";
-
-context HOL.thy; 
-
-Goal "(P --> Q | R) --> (P-->Q) | (P-->R)";
-by (Blast_tac 1);
-result();
-
-(*If and only if*)
-
-Goal "(P=Q) = (Q = (P::bool))";
-by (Blast_tac 1);
-result();
-
-Goal "~ (P = (~P))";
-by (Blast_tac 1);
-result();
-
-
-(*Sample problems from 
-  F. J. Pelletier, 
-  Seventy-Five Problems for Testing Automatic Theorem Provers,
-  J. Automated Reasoning 2 (1986), 191-216.
-  Errata, JAR 4 (1988), 236-236.
-
-The hardest problems -- judging by experience with several theorem provers,
-including matrix ones -- are 34 and 43.
-*)
-
-writeln"Pelletier's examples";
-(*1*)
-Goal "(P-->Q)  =  (~Q --> ~P)";
-by (Blast_tac 1);
-result();
-
-(*2*)
-Goal "(~ ~ P) =  P";
-by (Blast_tac 1);
-result();
-
-(*3*)
-Goal "~(P-->Q) --> (Q-->P)";
-by (Blast_tac 1);
-result();
-
-(*4*)
-Goal "(~P-->Q)  =  (~Q --> P)";
-by (Blast_tac 1);
-result();
-
-(*5*)
-Goal "((P|Q)-->(P|R)) --> (P|(Q-->R))";
-by (Blast_tac 1);
-result();
-
-(*6*)
-Goal "P | ~ P";
-by (Blast_tac 1);
-result();
-
-(*7*)
-Goal "P | ~ ~ ~ P";
-by (Blast_tac 1);
-result();
-
-(*8.  Peirce's law*)
-Goal "((P-->Q) --> P)  -->  P";
-by (Blast_tac 1);
-result();
-
-(*9*)
-Goal "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
-by (Blast_tac 1);
-result();
-
-(*10*)
-Goal "(Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P=Q)";
-by (Blast_tac 1);
-result();
-
-(*11.  Proved in each direction (incorrectly, says Pelletier!!)  *)
-Goal "P=(P::bool)";
-by (Blast_tac 1);
-result();
-
-(*12.  "Dijkstra's law"*)
-Goal "((P = Q) = R) = (P = (Q = R))";
-by (Blast_tac 1);
-result();
-
-(*13.  Distributive law*)
-Goal "(P | (Q & R)) = ((P | Q) & (P | R))";
-by (Blast_tac 1);
-result();
-
-(*14*)
-Goal "(P = Q) = ((Q | ~P) & (~Q|P))";
-by (Blast_tac 1);
-result();
-
-(*15*)
-Goal "(P --> Q) = (~P | Q)";
-by (Blast_tac 1);
-result();
-
-(*16*)
-Goal "(P-->Q) | (Q-->P)";
-by (Blast_tac 1);
-result();
-
-(*17*)
-Goal "((P & (Q-->R))-->S)  =  ((~P | Q | S) & (~P | ~R | S))";
-by (Blast_tac 1);
-result();
-
-writeln"Classical Logic: examples with quantifiers";
-
-Goal "(! x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))";
-by (Blast_tac 1);
-result(); 
-
-Goal "(? x. P-->Q(x))  =  (P --> (? x. Q(x)))";
-by (Blast_tac 1);
-result(); 
-
-Goal "(? x. P(x)-->Q) = ((! x. P(x)) --> Q)";
-by (Blast_tac 1);
-result(); 
-
-Goal "((! x. P(x)) | Q)  =  (! x. P(x) | Q)";
-by (Blast_tac 1);
-result(); 
-
-(*From Wishnu Prasetya*)
-Goal "(!s. q(s) --> r(s)) & ~r(s) & (!s. ~r(s) & ~q(s) --> p(t) | q(t)) \
-\   --> p(t) | r(t)";
-by (Blast_tac 1);
-result(); 
-
-
-writeln"Problems requiring quantifier duplication";
-
-(*Theorem B of Peter Andrews, Theorem Proving via General Matings, 
-  JACM 28 (1981).*)
-Goal "(EX x. ALL y. P(x) = P(y)) --> ((EX x. P(x)) = (ALL y. P(y)))";
-by (Blast_tac 1);
-result();
-
-(*Needs multiple instantiation of the quantifier.*)
-Goal "(! x. P(x)-->P(f(x)))  &  P(d)-->P(f(f(f(d))))";
-by (Blast_tac 1);
-result();
-
-(*Needs double instantiation of the quantifier*)
-Goal "? x. P(x) --> P(a) & P(b)";
-by (Blast_tac 1);
-result();
-
-Goal "? z. P(z) --> (! x. P(x))";
-by (Blast_tac 1);
-result();
-
-Goal "? x. (? y. P(y)) --> P(x)";
-by (Blast_tac 1);
-result();
-
-writeln"Hard examples with quantifiers";
-
-writeln"Problem 18";
-Goal "? y. ! x. P(y)-->P(x)";
-by (Blast_tac 1);
-result(); 
-
-writeln"Problem 19";
-Goal "? x. ! y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))";
-by (Blast_tac 1);
-result();
-
-writeln"Problem 20";
-Goal "(! x y. ? z. ! w. (P(x)&Q(y)-->R(z)&S(w)))     \
-\   --> (? x y. P(x) & Q(y)) --> (? z. R(z))";
-by (Blast_tac 1); 
-result();
-
-writeln"Problem 21";
-Goal "(? x. P-->Q(x)) & (? x. Q(x)-->P) --> (? x. P=Q(x))";
-by (Blast_tac 1); 
-result();
-
-writeln"Problem 22";
-Goal "(! x. P = Q(x))  -->  (P = (! x. Q(x)))";
-by (Blast_tac 1); 
-result();
-
-writeln"Problem 23";
-Goal "(! x. P | Q(x))  =  (P | (! x. Q(x)))";
-by (Blast_tac 1);  
-result();
-
-writeln"Problem 24";
-Goal "~(? x. S(x)&Q(x)) & (! x. P(x) --> Q(x)|R(x)) &  \
-\    (~(? x. P(x)) --> (? x. Q(x))) & (! x. Q(x)|R(x) --> S(x))  \
-\   --> (? x. P(x)&R(x))";
-by (Blast_tac 1); 
-result();
-
-writeln"Problem 25";
-Goal "(? x. P(x)) &  \
-\       (! x. L(x) --> ~ (M(x) & R(x))) &  \
-\       (! x. P(x) --> (M(x) & L(x))) &   \
-\       ((! x. P(x)-->Q(x)) | (? x. P(x)&R(x)))  \
-\   --> (? x. Q(x)&P(x))";
-by (Blast_tac 1); 
-result();
-
-writeln"Problem 26";
-Goal "((? x. p(x)) = (? x. q(x))) &     \
-\     (! x. ! y. p(x) & q(y) --> (r(x) = s(y))) \
-\ --> ((! x. p(x)-->r(x)) = (! x. q(x)-->s(x)))";
-by (Blast_tac 1);
-result();
-
-writeln"Problem 27";
-Goal "(? x. P(x) & ~Q(x)) &   \
-\             (! x. P(x) --> R(x)) &   \
-\             (! x. M(x) & L(x) --> P(x)) &   \
-\             ((? x. R(x) & ~ Q(x)) --> (! x. L(x) --> ~ R(x)))  \
-\         --> (! x. M(x) --> ~L(x))";
-by (Blast_tac 1); 
-result();
-
-writeln"Problem 28.  AMENDED";
-Goal "(! x. P(x) --> (! x. Q(x))) &   \
-\       ((! x. Q(x)|R(x)) --> (? x. Q(x)&S(x))) &  \
-\       ((? x. S(x)) --> (! x. L(x) --> M(x)))  \
-\   --> (! x. P(x) & L(x) --> M(x))";
-by (Blast_tac 1);  
-result();
-
-writeln"Problem 29.  Essentially the same as Principia Mathematica *11.71";
-Goal "(? x. F(x)) & (? y. G(y))  \
-\   --> ( ((! x. F(x)-->H(x)) & (! y. G(y)-->J(y)))  =   \
-\         (! x y. F(x) & G(y) --> H(x) & J(y)))";
-by (Blast_tac 1); 
-result();
-
-writeln"Problem 30";
-Goal "(! x. P(x) | Q(x) --> ~ R(x)) & \
-\       (! x. (Q(x) --> ~ S(x)) --> P(x) & R(x))  \
-\   --> (! x. S(x))";
-by (Blast_tac 1);  
-result();
-
-writeln"Problem 31";
-Goal "~(? x. P(x) & (Q(x) | R(x))) & \
-\       (? x. L(x) & P(x)) & \
-\       (! x. ~ R(x) --> M(x))  \
-\   --> (? x. L(x) & M(x))";
-by (Blast_tac 1);
-result();
-
-writeln"Problem 32";
-Goal "(! x. P(x) & (Q(x)|R(x))-->S(x)) & \
-\       (! x. S(x) & R(x) --> L(x)) & \
-\       (! x. M(x) --> R(x))  \
-\   --> (! x. P(x) & M(x) --> L(x))";
-by (Blast_tac 1);
-result();
-
-writeln"Problem 33";
-Goal "(! x. P(a) & (P(x)-->P(b))-->P(c))  =    \
-\    (! x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))";
-by (Blast_tac 1);
-result();
-
-writeln"Problem 34  AMENDED (TWICE!!)";
-(*Andrews's challenge*)
-Goal "((? x. ! y. p(x) = p(y))  =               \
-\              ((? x. q(x)) = (! y. p(y))))   =    \
-\             ((? x. ! y. q(x) = q(y))  =          \
-\              ((? x. p(x)) = (! y. q(y))))";
-by (Blast_tac 1);
-result();
-
-writeln"Problem 35";
-Goal "? x y. P x y -->  (! u v. P u v)";
-by (Blast_tac 1);
-result();
-
-writeln"Problem 36";
-Goal "(! x. ? y. J x y) & \
-\       (! x. ? y. G x y) & \
-\       (! x y. J x y | G x y -->       \
-\       (! z. J y z | G y z --> H x z))   \
-\   --> (! x. ? y. H x y)";
-by (Blast_tac 1);
-result();
-
-writeln"Problem 37";
-Goal "(! z. ? w. ! x. ? y. \
-\          (P x z -->P y w) & P y z & (P y w --> (? u. Q u w))) & \
-\       (! x z. ~(P x z) --> (? y. Q y z)) & \
-\       ((? x y. Q x y) --> (! x. R x x))  \
-\   --> (! x. ? y. R x y)";
-by (Blast_tac 1);
-result();
-
-writeln"Problem 38";
-Goal "(! x. p(a) & (p(x) --> (? y. p(y) & r x y)) -->            \
-\          (? z. ? w. p(z) & r x w & r w z))  =                 \
-\    (! x. (~p(a) | p(x) | (? z. ? w. p(z) & r x w & r w z)) &  \
-\          (~p(a) | ~(? y. p(y) & r x y) |                      \
-\           (? z. ? w. p(z) & r x w & r w z)))";
-by (Blast_tac 1);  (*beats fast_tac!*)
-result();
-
-writeln"Problem 39";
-Goal "~ (? x. ! y. F y x = (~ F y y))";
-by (Blast_tac 1);
-result();
-
-writeln"Problem 40.  AMENDED";
-Goal "(? y. ! x. F x y = F x x)  \
-\       -->  ~ (! x. ? y. ! z. F z y = (~ F z x))";
-by (Blast_tac 1);
-result();
-
-writeln"Problem 41";
-Goal "(! z. ? y. ! x. f x y = (f x z & ~ f x x))        \
-\              --> ~ (? z. ! x. f x z)";
-by (Blast_tac 1);
-result();
-
-writeln"Problem 42";
-Goal "~ (? y. ! x. p x y = (~ (? z. p x z & p z x)))";
-by (Blast_tac 1);
-result();
-
-writeln"Problem 43!!";
-Goal "(! x::'a. ! y::'a. q x y = (! z. p z x = (p z y::bool)))   \
-\ --> (! x. (! y. q x y = (q y x::bool)))";
-by (Blast_tac 1);
-result();
-
-writeln"Problem 44";
-Goal "(! x. f(x) -->                                    \
-\             (? y. g(y) & h x y & (? y. g(y) & ~ h x y)))  &   \
-\             (? x. j(x) & (! y. g(y) --> h x y))               \
-\             --> (? x. j(x) & ~f(x))";
-by (Blast_tac 1);
-result();
-
-writeln"Problem 45";
-Goal "(! x. f(x) & (! y. g(y) & h x y --> j x y) \
-\                     --> (! y. g(y) & h x y --> k(y))) &       \
-\    ~ (? y. l(y) & k(y)) &                                     \
-\    (? x. f(x) & (! y. h x y --> l(y))                         \
-\               & (! y. g(y) & h x y --> j x y))                \
-\     --> (? x. f(x) & ~ (? y. g(y) & h x y))";
-by (Blast_tac 1); 
-result();
-
-
-writeln"Problems (mainly) involving equality or functions";
-
-writeln"Problem 48";
-Goal "(a=b | c=d) & (a=c | b=d) --> a=d | b=c";
-by (Blast_tac 1);
-result();
-
-writeln"Problem 49  NOT PROVED AUTOMATICALLY";
-(*Hard because it involves substitution for Vars;
-  the type constraint ensures that x,y,z have the same type as a,b,u. *)
-Goal "(? x y::'a. ! z. z=x | z=y) & P(a) & P(b) & (~a=b) \
-\               --> (! u::'a. P(u))";
-by (Classical.Safe_tac);
-by (res_inst_tac [("x","a")] allE 1);
-by (assume_tac 1);
-by (res_inst_tac [("x","b")] allE 1);
-by (assume_tac 1);
-by (Fast_tac 1);    (*Blast_tac's treatment of equality can't do it*)
-result();
-
-writeln"Problem 50";  
-(*What has this to do with equality?*)
-Goal "(! x. P a x | (! y. P x y)) --> (? x. ! y. P x y)";
-by (Blast_tac 1);
-result();
-
-writeln"Problem 51";
-Goal "(? z w. ! x y. P x y = (x=z & y=w)) -->  \
-\    (? z. ! x. ? w. (! y. P x y = (y=w)) = (x=z))";
-by (Blast_tac 1);
-result();
-
-writeln"Problem 52";
-(*Almost the same as 51. *)
-Goal "(? z w. ! x y. P x y = (x=z & y=w)) -->  \
-\    (? w. ! y. ? z. (! x. P x y = (x=z)) = (y=w))";
-by (Blast_tac 1);
-result();
-
-writeln"Problem 55";
-
-(*Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988).
-  fast_tac DISCOVERS who killed Agatha. *)
-Goal "lives(agatha) & lives(butler) & lives(charles) & \
-\  (killed agatha agatha | killed butler agatha | killed charles agatha) & \
-\  (!x y. killed x y --> hates x y & ~richer x y) & \
-\  (!x. hates agatha x --> ~hates charles x) & \
-\  (hates agatha agatha & hates agatha charles) & \
-\  (!x. lives(x) & ~richer x agatha --> hates butler x) & \
-\  (!x. hates agatha x --> hates butler x) & \
-\  (!x. ~hates x agatha | ~hates x butler | ~hates x charles) --> \
-\   killed ?who agatha";
-by (Fast_tac 1);
-result();
-
-writeln"Problem 56";
-Goal "(! x. (? y. P(y) & x=f(y)) --> P(x)) = (! x. P(x) --> P(f(x)))";
-by (Blast_tac 1);
-result();
-
-writeln"Problem 57";
-Goal "P (f a b) (f b c) & P (f b c) (f a c) & \
-\    (! x y z. P x y & P y z --> P x z)    -->   P (f a b) (f a c)";
-by (Blast_tac 1);
-result();
-
-writeln"Problem 58  NOT PROVED AUTOMATICALLY";
-Goal "(! x y. f(x)=g(y)) --> (! x y. f(f(x))=f(g(y)))";
-val f_cong = read_instantiate [("f","f")] arg_cong;
-by (fast_tac (claset() addIs [f_cong]) 1);
-result();
-
-writeln"Problem 59";
-Goal "(! x. P(x) = (~P(f(x)))) --> (? x. P(x) & ~P(f(x)))";
-by (Blast_tac 1);
-result();
-
-writeln"Problem 60";
-Goal "! x. P x (f x) = (? y. (! z. P z y --> P z (f x)) & P x y)";
-by (Blast_tac 1);
-result();
-
-writeln"Problem 62 as corrected in JAR 18 (1997), page 135";
-Goal "(ALL x. p a & (p x --> p(f x)) --> p(f(f x)))  =   \
-\     (ALL x. (~ p a | p x | p(f(f x))) &                        \
-\             (~ p a | ~ p(f x) | p(f(f x))))";
-by (Blast_tac 1);
-result();
-
-(*From Davis, Obvious Logical Inferences, IJCAI-81, 530-531
-  Fast_tac indeed copes!*)
-goal (theory "Product_Type") 
-             "(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 (theory "Product_Type")
-    "(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();
-
-(*Attributed to Lewis Carroll by S. G. Pulman.  The first or last assumption
-can be deleted.*)
-Goal "(ALL x. honest(x) & industrious(x) --> healthy(x)) & \
-\     ~ (EX x. grocer(x) & healthy(x)) & \
-\     (ALL x. industrious(x) & grocer(x) --> honest(x)) & \
-\     (ALL x. cyclist(x) --> industrious(x)) & \
-\     (ALL x. ~healthy(x) & cyclist(x) --> ~honest(x))  \
-\     --> (ALL x. grocer(x) --> ~cyclist(x))";
-by (Blast_tac 1);
-result();
-
-goal (theory "Product_Type")
-    "(ALL x y. R(x,y) | R(y,x)) &                \
-\    (ALL x y. S(x,y) & S(y,x) --> x=y) &        \
-\    (ALL x y. R(x,y) --> S(x,y))    -->   (ALL x y. S(x,y) --> R(x,y))";
-by (Blast_tac 1);
-result();
-
-
-
-writeln"Reached end of file.";
diff -r 9fdea25f9ebb -r 4dc132902672 src/HOL/ex/mesontest.ML
--- a/src/HOL/ex/mesontest.ML	Fri Oct 03 12:36:16 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,615 +0,0 @@
-(*  Title:      HOL/ex/mesontest
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1992  University of Cambridge
-
-Test data for the MESON proof procedure
-   (Excludes the equality problems 51, 52, 56, 58)
-
-Use the "mesonlog" shell script to process logs.
-
-show_hyps := false;
-
-proofs := 0;
-by (rtac ccontr 1);
-val [prem] = gethyps 1;
-val nnf = make_nnf prem;
-val xsko = skolemize nnf;
-by (cut_facts_tac [xsko] 1 THEN REPEAT (etac exE 1));
-val [_,sko] = gethyps 1;
-val clauses = make_clauses [sko];       
-val horns = make_horns clauses;
-val goes = gocls clauses;
-
-Goal "False";
-by (resolve_tac goes 1);
-proofs := 2;
-
-by (prolog_step_tac horns 1);
-by (iter_deepen_prolog_tac horns);
-by (depth_prolog_tac horns);
-by (best_prolog_tac size_of_subgoals horns);
-*)
-
-writeln"File HOL/ex/meson-test.";
-
-context Main.thy;
-
-(*Deep unifications can be required, esp. during transformation to clauses*)
-val orig_trace_bound = !Unify.trace_bound
-and orig_search_bound = !Unify.search_bound;
-Unify.trace_bound := 20;
-Unify.search_bound := 40;
-
-(**** Interactive examples ****)
-
-(*Generate nice names for Skolem functions*)
-Logic.auto_rename := true; Logic.set_rename_prefix "a";
-
-
-writeln"Problem 25";
-Goal "(\\<exists>x. P x) &  \
-\     (\\<forall>x. L x --> ~ (M x & R x)) &  \
-\     (\\<forall>x. P x --> (M x & L x)) &   \
-\     ((\\<forall>x. P x --> Q x) | (\\<exists>x. P x & R x))  \
-\   --> (\\<exists>x. Q x & P x)";
-by (rtac ccontr 1);
-val [prem25] = gethyps 1;
-val nnf25 = make_nnf prem25;
-val xsko25 = skolemize nnf25;
-by (cut_facts_tac [xsko25] 1 THEN REPEAT (etac exE 1));
-val [_,sko25] = gethyps 1;
-val clauses25 = make_clauses [sko25];   (*7 clauses*)
-val horns25 = make_horns clauses25;     (*16 Horn clauses*)
-val go25::_ = gocls clauses25;
-
-Goal "False";
-by (rtac go25 1);
-by (depth_prolog_tac horns25);
-
-
-writeln"Problem 26";
-Goal "((\\<exists>x. p x) = (\\<exists>x. q x)) &     \
-\     (\\<forall>x. \\<forall>y. p x & q y --> (r x = s y)) \
-\ --> ((\\<forall>x. p x --> r x) = (\\<forall>x. q x --> s x))";
-by (rtac ccontr 1);
-val [prem26] = gethyps 1;
-val nnf26 = make_nnf prem26;
-val xsko26 = skolemize nnf26;
-by (cut_facts_tac [xsko26] 1 THEN REPEAT (etac exE 1));
-val [_,sko26] = gethyps 1;
-val clauses26 = make_clauses [sko26];                   (*9 clauses*)
-val horns26 = make_horns clauses26;                     (*24 Horn clauses*)
-val go26::_ = gocls clauses26;
-
-Goal "False";
-by (rtac go26 1);
-by (depth_prolog_tac horns26);  (*1.4 secs*)
-(*Proof is of length 107!!*)
-
-
-writeln"Problem 43  NOW PROVED AUTOMATICALLY!!";  (*16 Horn clauses*)
-Goal "(\\<forall>x. \\<forall>y. q x y = (\\<forall>z. p z x = (p z y::bool)))  \
-\     --> (\\<forall>x. (\\<forall>y. q x y = (q y x::bool)))";
-by (rtac ccontr 1);
-val [prem43] = gethyps 1;
-val nnf43 = make_nnf prem43;
-val xsko43 = skolemize nnf43;
-by (cut_facts_tac [xsko43] 1 THEN REPEAT (etac exE 1));
-val [_,sko43] = gethyps 1;
-val clauses43 = make_clauses [sko43];   (*6*)
-val horns43 = make_horns clauses43;     (*16*)
-val go43::_ = gocls clauses43;
-
-Goal "False";
-by (rtac go43 1);
-by (best_prolog_tac size_of_subgoals horns43);   (*1.6 secs*)
-
-(* 
-#1  (q x xa ==> ~ q x xa) ==> q xa x
-#2  (q xa x ==> ~ q xa x) ==> q x xa
-#3  (~ q x xa ==> q x xa) ==> ~ q xa x
-#4  (~ q xa x ==> q xa x) ==> ~ q x xa
-#5  [| ~ q ?U ?V ==> q ?U ?V; ~ p ?W ?U ==> p ?W ?U |] ==> p ?W ?V
-#6  [| ~ p ?W ?U ==> p ?W ?U; p ?W ?V ==> ~ p ?W ?V |] ==> ~ q ?U ?V
-#7  [| p ?W ?V ==> ~ p ?W ?V; ~ q ?U ?V ==> q ?U ?V |] ==> ~ p ?W ?U
-#8  [| ~ q ?U ?V ==> q ?U ?V; ~ p ?W ?V ==> p ?W ?V |] ==> p ?W ?U
-#9  [| ~ p ?W ?V ==> p ?W ?V; p ?W ?U ==> ~ p ?W ?U |] ==> ~ q ?U ?V
-#10 [| p ?W ?U ==> ~ p ?W ?U; ~ q ?U ?V ==> q ?U ?V |] ==> ~ p ?W ?V
-#11 [| p (xb ?U ?V) ?U ==> ~ p (xb ?U ?V) ?U;
-       p (xb ?U ?V) ?V ==> ~ p (xb ?U ?V) ?V |] ==> q ?U ?V
-#12 [| p (xb ?U ?V) ?V ==> ~ p (xb ?U ?V) ?V; q ?U ?V ==> ~ q ?U ?V |] ==>
-    p (xb ?U ?V) ?U
-#13 [| q ?U ?V ==> ~ q ?U ?V; p (xb ?U ?V) ?U ==> ~ p (xb ?U ?V) ?U |] ==>
-    p (xb ?U ?V) ?V
-#14 [| ~ p (xb ?U ?V) ?U ==> p (xb ?U ?V) ?U;
-       ~ p (xb ?U ?V) ?V ==> p (xb ?U ?V) ?V |] ==> q ?U ?V
-#15 [| ~ p (xb ?U ?V) ?V ==> p (xb ?U ?V) ?V; q ?U ?V ==> ~ q ?U ?V |] ==>
-    ~ p (xb ?U ?V) ?U
-#16 [| q ?U ?V ==> ~ q ?U ?V; ~ p (xb ?U ?V) ?U ==> p (xb ?U ?V) ?U |] ==>
-    ~ p (xb ?U ?V) ?V
-
-And here is the proof\\<forall> (Unkn is the start state after use of goal clause)
-[Unkn, Res ([Thm "#14"], false, 1), Res ([Thm "#5"], false, 1),
-   Res ([Thm "#1"], false, 1), Asm 1, Res ([Thm "#13"], false, 1), Asm 2,
-   Asm 1, Res ([Thm "#13"], false, 1), Asm 1, Res ([Thm "#10"], false, 1),
-   Res ([Thm "#16"], false, 1), Asm 2, Asm 1, Res ([Thm "#1"], false, 1),
-   Asm 1, Res ([Thm "#14"], false, 1), Res ([Thm "#5"], false, 1),
-   Res ([Thm "#2"], false, 1), Asm 1, Res ([Thm "#13"], false, 1), Asm 2,
-   Asm 1, Res ([Thm "#8"], false, 1), Res ([Thm "#2"], false, 1), Asm 1,
-   Res ([Thm "#12"], false, 1), Asm 2, Asm 1] : lderiv list
-*)
-
-
-(*Restore variable name preservation*)
-Logic.auto_rename := false; 
-
-
-(**** Batch test data ****)
-
-(*Sample problems from 
-  F. J. Pelletier, 
-  Seventy-Five Problems for Testing Automatic Theorem Provers,
-  J. Automated Reasoning 2 (1986), 191-216.
-  Errata, JAR 4 (1988), 236-236.
-
-The hardest problems -- judging by experience with several theorem provers,
-including matrix ones -- are 34 and 43.
-*)
-
-writeln"Pelletier's examples";
-(*1*)
-Goal "(P --> Q)  =  (~Q --> ~P)";
-by (meson_tac 1);
-result();
-
-(*2*)
-Goal "(~ ~ P) =  P";
-by (meson_tac 1);
-result();
-
-(*3*)
-Goal "~(P-->Q) --> (Q-->P)";
-by (meson_tac 1);
-result();
-
-(*4*)
-Goal "(~P-->Q)  =  (~Q --> P)";
-by (meson_tac 1);
-result();
-
-(*5*)
-Goal "((P|Q)-->(P|R)) --> (P|(Q-->R))";
-by (meson_tac 1);
-result();
-
-(*6*)
-Goal "P | ~ P";
-by (meson_tac 1);
-result();
-
-(*7*)
-Goal "P | ~ ~ ~ P";
-by (meson_tac 1);
-result();
-
-(*8.  Peirce's law*)
-Goal "((P-->Q) --> P)  -->  P";
-by (meson_tac 1);
-result();
-
-(*9*)
-Goal "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
-by (meson_tac 1);
-result();
-
-(*10*)
-Goal "(Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P=Q)";
-by (meson_tac 1);
-result();
-
-(*11.  Proved in each direction (incorrectly, says Pelletier!!)  *)
-Goal "P=(P::bool)";
-by (meson_tac 1);
-result();
-
-(*12.  "Dijkstra's law"*)
-Goal "((P = Q) = R) = (P = (Q = R))";
-by (meson_tac 1);
-result();
-
-(*13.  Distributive law*)
-Goal "(P | (Q & R)) = ((P | Q) & (P | R))";
-by (meson_tac 1);
-result();
-
-(*14*)
-Goal "(P = Q) = ((Q | ~P) & (~Q|P))";
-by (meson_tac 1);
-result();
-
-(*15*)
-Goal "(P --> Q) = (~P | Q)";
-by (meson_tac 1);
-result();
-
-(*16*)
-Goal "(P-->Q) | (Q-->P)";
-by (meson_tac 1);
-result();
-
-(*17*)
-Goal "((P & (Q-->R))-->S)  =  ((~P | Q | S) & (~P | ~R | S))";
-by (meson_tac 1);
-result();
-
-writeln"Classical Logic: examples with quantifiers";
-
-Goal "(\\<forall>x. P x & Q x) = ((\\<forall>x. P x) & (\\<forall>x. Q x))";
-by (meson_tac 1);
-result(); 
-
-Goal "(\\<exists>x. P --> Q x)  =  (P --> (\\<exists>x. Q x))";
-by (meson_tac 1);
-result(); 
-
-Goal "(\\<exists>x. P x --> Q) = ((\\<forall>x. P x) --> Q)";
-by (meson_tac 1);
-result(); 
-
-Goal "((\\<forall>x. P x) | Q)  =  (\\<forall>x. P x | Q)";
-by (meson_tac 1);
-result(); 
-
-Goal "(\\<forall>x. P x --> P(f x))  &  P d --> P(f(f(f d)))";
-by (meson_tac 1);
-result();
-
-(*Needs double instantiation of EXISTS*)
-Goal "\\<exists>x. P x --> P a & P b";
-by (meson_tac 1);
-result();
-
-Goal "\\<exists>z. P z --> (\\<forall>x. P x)";
-by (meson_tac 1);
-result();
-
-writeln"Hard examples with quantifiers";
-
-writeln"Problem 18";
-Goal "\\<exists>y. \\<forall>x. P y --> P x";
-by (meson_tac 1);
-result(); 
-
-writeln"Problem 19";
-Goal "\\<exists>x. \\<forall>y z. (P y --> Q z) --> (P x --> Q x)";
-by (meson_tac 1);
-result();
-
-writeln"Problem 20";
-Goal "(\\<forall>x y. \\<exists>z. \\<forall>w. (P x & Q y --> R z & S w))     \
-\   --> (\\<exists>x y. P x & Q y) --> (\\<exists>z. R z)";
-by (meson_tac 1); 
-result();
-
-writeln"Problem 21";
-Goal "(\\<exists>x. P --> Q x) & (\\<exists>x. Q x --> P) --> (\\<exists>x. P=Q x)";
-by (meson_tac 1); 
-result();
-
-writeln"Problem 22";
-Goal "(\\<forall>x. P = Q x)  -->  (P = (\\<forall>x. Q x))";
-by (meson_tac 1); 
-result();
-
-writeln"Problem 23";
-Goal "(\\<forall>x. P | Q x)  =  (P | (\\<forall>x. Q x))";
-by (meson_tac 1);  
-result();
-
-writeln"Problem 24";  (*The first goal clause is useless*)
-Goal "~(\\<exists>x. S x & Q x) & (\\<forall>x. P x --> Q x | R x) &  \
-\     (~(\\<exists>x. P x) --> (\\<exists>x. Q x)) & (\\<forall>x. Q x | R x --> S x)  \
-\   --> (\\<exists>x. P x & R x)";
-by (meson_tac 1); 
-result();
-
-writeln"Problem 25";
-Goal "(\\<exists>x. P x) &  \
-\     (\\<forall>x. L x --> ~ (M x & R x)) &  \
-\     (\\<forall>x. P x --> (M x & L x)) &   \
-\     ((\\<forall>x. P x --> Q x) | (\\<exists>x. P x & R x))  \
-\   --> (\\<exists>x. Q x & P x)";
-by (meson_tac 1); 
-result();
-
-writeln"Problem 26";  (*24 Horn clauses*)
-Goal "((\\<exists>x. p x) = (\\<exists>x. q x)) &     \
-\     (\\<forall>x. \\<forall>y. p x & q y --> (r x = s y)) \
-\ --> ((\\<forall>x. p x --> r x) = (\\<forall>x. q x --> s x))";
-by (meson_tac 1); 
-result();
-
-writeln"Problem 27";    (*13 Horn clauses*)
-Goal "(\\<exists>x. P x & ~Q x) &   \
-\     (\\<forall>x. P x --> R x) &   \
-\     (\\<forall>x. M x & L x --> P x) &   \
-\     ((\\<exists>x. R x & ~ Q x) --> (\\<forall>x. L x --> ~ R x))  \
-\     --> (\\<forall>x. M x --> ~L x)";
-by (meson_tac 1); 
-result();
-
-writeln"Problem 28.  AMENDED";  (*14 Horn clauses*)
-Goal "(\\<forall>x. P x --> (\\<forall>x. Q x)) &   \
-\     ((\\<forall>x. Q x | R x) --> (\\<exists>x. Q x & S x)) &  \
-\     ((\\<exists>x. S x) --> (\\<forall>x. L x --> M x))  \
-\   --> (\\<forall>x. P x & L x --> M x)";
-by (meson_tac 1);  
-result();
-
-writeln"Problem 29.  Essentially the same as Principia Mathematica *11.71";
-        (*62 Horn clauses*)
-Goal "(\\<exists>x. F x) & (\\<exists>y. G y)  \
-\   --> ( ((\\<forall>x. F x --> H x) & (\\<forall>y. G y --> J y))  =   \
-\         (\\<forall>x y. F x & G y --> H x & J y))";
-by (meson_tac 1);          (*0.7 secs*)
-result();
-
-writeln"Problem 30";
-Goal "(\\<forall>x. P x | Q x --> ~ R x) & \
-\     (\\<forall>x. (Q x --> ~ S x) --> P x & R x)  \
-\   --> (\\<forall>x. S x)";
-by (meson_tac 1);  
-result();
-
-writeln"Problem 31";  (*10 Horn clauses; first negative clauses is useless*)
-Goal "~(\\<exists>x. P x & (Q x | R x)) & \
-\     (\\<exists>x. L x & P x) & \
-\     (\\<forall>x. ~ R x --> M x)  \
-\   --> (\\<exists>x. L x & M x)";
-by (meson_tac 1);
-result();
-
-writeln"Problem 32";
-Goal "(\\<forall>x. P x & (Q x | R x)-->S x) & \
-\     (\\<forall>x. S x & R x --> L x) & \
-\     (\\<forall>x. M x --> R x)  \
-\   --> (\\<forall>x. P x & M x --> L x)";
-by (meson_tac 1);
-result();
-
-writeln"Problem 33";  (*55 Horn clauses*)
-Goal "(\\<forall>x. P a & (P x --> P b)-->P c)  =    \
-\     (\\<forall>x. (~P a | P x | P c) & (~P a | ~P b | P c))";
-by (meson_tac 1);          (*5.6 secs*)
-result();
-
-writeln"Problem 34  AMENDED (TWICE!!)"; (*924 Horn clauses*)
-(*Andrews's challenge*)
-Goal "((\\<exists>x. \\<forall>y. p x = p y)  =               \
-\      ((\\<exists>x. q x) = (\\<forall>y. p y)))     =       \
-\     ((\\<exists>x. \\<forall>y. q x = q y)  =               \
-\      ((\\<exists>x. p x) = (\\<forall>y. q y)))";
-by (meson_tac 1);          (*13 secs*)
-result();
-
-writeln"Problem 35";
-Goal "\\<exists>x y. P x y -->  (\\<forall>u v. P u v)";
-by (meson_tac 1);
-result();
-
-writeln"Problem 36";  (*15 Horn clauses*)
-Goal "(\\<forall>x. \\<exists>y. J x y) & \
-\     (\\<forall>x. \\<exists>y. G x y) & \
-\     (\\<forall>x y. J x y | G x y -->       \
-\     (\\<forall>z. J y z | G y z --> H x z))   \
-\   --> (\\<forall>x. \\<exists>y. H x y)";
-by (meson_tac 1);
-result();
-
-writeln"Problem 37";  (*10 Horn clauses*)
-Goal "(\\<forall>z. \\<exists>w. \\<forall>x. \\<exists>y. \
-\          (P x z --> P y w) & P y z & (P y w --> (\\<exists>u. Q u w))) & \
-\     (\\<forall>x z. ~P x z --> (\\<exists>y. Q y z)) & \
-\     ((\\<exists>x y. Q x y) --> (\\<forall>x. R x x))  \
-\   --> (\\<forall>x. \\<exists>y. R x y)";
-by (meson_tac 1);   (*causes unification tracing messages*)
-result();
-
-writeln"Problem 38";  (*Quite hard: 422 Horn clauses!!*)
-Goal "(\\<forall>x. p a & (p x --> (\\<exists>y. p y & r x y)) -->            \
-\          (\\<exists>z. \\<exists>w. p z & r x w & r w z))  =                 \
-\     (\\<forall>x. (~p a | p x | (\\<exists>z. \\<exists>w. p z & r x w & r w z)) &  \
-\           (~p a | ~(\\<exists>y. p y & r x y) |                      \
-\            (\\<exists>z. \\<exists>w. p z & r x w & r w z)))";
-by (safe_best_meson_tac 1);  (*10 secs; iter. deepening is slightly slower*)
-result();
-
-writeln"Problem 39";
-Goal "~ (\\<exists>x. \\<forall>y. F y x = (~F y y))";
-by (meson_tac 1);
-result();
-
-writeln"Problem 40.  AMENDED";
-Goal "(\\<exists>y. \\<forall>x. F x y = F x x)  \
-\     -->  ~ (\\<forall>x. \\<exists>y. \\<forall>z. F z y = (~F z x))";
-by (meson_tac 1);
-result();
-
-writeln"Problem 41";
-Goal "(\\<forall>z. (\\<exists>y. (\\<forall>x. f x y = (f x z & ~ f x x))))    \
-\     --> ~ (\\<exists>z. \\<forall>x. f x z)";
-by (meson_tac 1);
-result();
-
-writeln"Problem 42";
-Goal "~ (\\<exists>y. \\<forall>x. p x y = (~ (\\<exists>z. p x z & p z x)))";
-by (meson_tac 1);
-result();
-
-writeln"Problem 43  NOW PROVED AUTOMATICALLY!!";
-Goal "(\\<forall>x. \\<forall>y. q x y = (\\<forall>z. p z x = (p z y::bool)))  \
-\     --> (\\<forall>x. (\\<forall>y. q x y = (q y x::bool)))";
-by (safe_best_meson_tac 1);     
-(*1.6 secs; iter. deepening is slightly slower*)
-result();
-
-writeln"Problem 44";  (*13 Horn clauses; 7-step proof*)
-Goal "(\\<forall>x. f x -->                                    \
-\           (\\<exists>y. g y & h x y & (\\<exists>y. g y & ~ h x y)))  &   \
-\     (\\<exists>x. j x & (\\<forall>y. g y --> h x y))               \
-\     --> (\\<exists>x. j x & ~f x)";
-by (meson_tac 1);
-result();
-
-writeln"Problem 45";  (*27 Horn clauses; 54-step proof*)
-Goal "(\\<forall>x. f x & (\\<forall>y. g y & h x y --> j x y)        \
-\           --> (\\<forall>y. g y & h x y --> k y)) &       \
-\     ~ (\\<exists>y. l y & k y) &                                    \
-\     (\\<exists>x. f x & (\\<forall>y. h x y --> l y)                        \
-\               & (\\<forall>y. g y & h x y --> j x y))             \
-\     --> (\\<exists>x. f x & ~ (\\<exists>y. g y & h x y))";
-by (safe_best_meson_tac 1);     
-(*1.6 secs; iter. deepening is slightly slower*)
-result();
-
-writeln"Problem 46";  (*26 Horn clauses; 21-step proof*)
-Goal "(\\<forall>x. f x & (\\<forall>y. f y & h y x --> g y) --> g x) &      \
-\     ((\\<exists>x. f x & ~g x) -->                                    \
-\     (\\<exists>x. f x & ~g x & (\\<forall>y. f y & ~g y --> j x y))) &    \
-\     (\\<forall>x y. f x & f y & h x y --> ~j y x)                    \
-\     --> (\\<forall>x. f x --> g x)";
-by (safe_best_meson_tac 1);     
-(*1.7 secs; iter. deepening is slightly slower*)
-result();
-
-writeln"Problem 47.  Schubert's Steamroller";
-        (*26 clauses; 63 Horn clauses
-          87094 inferences so far.  Searching to depth 36*)
-Goal "(\\<forall>x. P1 x --> P0 x) & (\\<exists>x. P1 x) &     \
-\     (\\<forall>x. P2 x --> P0 x) & (\\<exists>x. P2 x) &     \
-\     (\\<forall>x. P3 x --> P0 x) & (\\<exists>x. P3 x) &     \
-\     (\\<forall>x. P4 x --> P0 x) & (\\<exists>x. P4 x) &     \
-\     (\\<forall>x. P5 x --> P0 x) & (\\<exists>x. P5 x) &     \
-\     (\\<forall>x. Q1 x --> Q0 x) & (\\<exists>x. Q1 x) &     \
-\     (\\<forall>x. P0 x --> ((\\<forall>y. Q0 y-->R x y) |    \
-\                      (\\<forall>y. P0 y & S y x &     \
-\                           (\\<exists>z. Q0 z&R y z) --> R x y))) &   \
-\     (\\<forall>x y. P3 y & (P5 x|P4 x) --> S x y) &        \
-\     (\\<forall>x y. P3 x & P2 y --> S x y) &        \
-\     (\\<forall>x y. P2 x & P1 y --> S x y) &        \
-\     (\\<forall>x y. P1 x & (P2 y|Q1 y) --> ~R x y) &       \
-\     (\\<forall>x y. P3 x & P4 y --> R x y) &        \
-\     (\\<forall>x y. P3 x & P5 y --> ~R x y) &       \
-\     (\\<forall>x. (P4 x|P5 x) --> (\\<exists>y. Q0 y & R x y))      \
-\     --> (\\<exists>x y. P0 x & P0 y & (\\<exists>z. Q1 z & R y z & R x y))";
-by (safe_best_meson_tac 1);     (*MUCH faster than iterative deepening*)
-result();
-
-(*The Los problem\\<exists> Circulated by John Harrison*)
-Goal "(\\<forall>x y z. P x y & P y z --> P x z) &      \
-\     (\\<forall>x y z. Q x y & Q y z --> Q x z) &             \
-\     (\\<forall>x y. P x y --> P y x) &                       \
-\     (\\<forall>x y. P x y | Q x y)                           \
-\     --> (\\<forall>x y. P x y) | (\\<forall>x y. Q x y)";
-by (safe_best_meson_tac 1);     (*2.3 secs; iter. deepening is VERY slow*)
-result();
-
-(*A similar example, suggested by Johannes Schumann and credited to Pelletier*)
-Goal "(!x y z. P x y --> P y z --> P x z) --> \
-\     (!x y z. Q x y --> Q y z --> Q x z) --> \
-\     (!x y. Q x y --> Q y x) -->  (!x y. P x y | Q x y) --> \
-\     (!x y. P x y) | (!x y. Q x y)";
-by (safe_best_meson_tac 1);          (*2.7 secs*)
-result();
-
-writeln"Problem 50";  
-(*What has this to do with equality?*)
-Goal "(\\<forall>x. P a x | (\\<forall>y. P x y)) --> (\\<exists>x. \\<forall>y. P x y)";
-by (meson_tac 1);
-result();
-
-writeln"Problem 55";
-
-(*Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988).
-  meson_tac cannot report who killed Agatha. *)
-Goal "lives agatha & lives butler & lives charles & \
-\     (killed agatha agatha | killed butler agatha | killed charles agatha) & \
-\     (!x y. killed x y --> hates x y & ~richer x y) & \
-\     (!x. hates agatha x --> ~hates charles x) & \
-\     (hates agatha agatha & hates agatha charles) & \
-\     (!x. lives x & ~richer x agatha --> hates butler x) & \
-\     (!x. hates agatha x --> hates butler x) & \
-\     (!x. ~hates x agatha | ~hates x butler | ~hates x charles) --> \
-\     (\\<exists>x. killed x agatha)";
-by (meson_tac 1);
-result();
-
-writeln"Problem 57";
-Goal "P (f a b) (f b c) & P (f b c) (f a c) & \
-\     (\\<forall>x y z. P x y & P y z --> P x z)    -->   P (f a b) (f a c)";
-by (meson_tac 1);
-result();
-
-writeln"Problem 58";
-(* Challenge found on info-hol *)
-Goal "\\<forall>P Q R x. \\<exists>v w. \\<forall>y z. P x & Q y --> (P v | R w) & (R z --> Q v)";
-by (meson_tac 1);
-result();
-
-writeln"Problem 59";
-Goal "(\\<forall>x. P x = (~P(f x))) --> (\\<exists>x. P x & ~P(f x))";
-by (meson_tac 1);
-result();
-
-writeln"Problem 60";
-Goal "\\<forall>x. P x (f x) = (\\<exists>y. (\\<forall>z. P z y --> P z (f x)) & P x y)";
-by (meson_tac 1);
-result();
-
-writeln"Problem 62 as corrected in JAR 18 (1997), page 135";
-Goal "(ALL x. p a & (p x --> p(f x)) --> p(f(f x)))  =   \
-\     (ALL x. (~ p a | p x | p(f(f x))) &                        \
-\             (~ p a | ~ p(f x) | p(f(f x))))";
-by (meson_tac 1);
-result();
-
-
-(** Charles Morgan's problems **)
-
-val axa = "\\<forall>x y.   T(i x(i y x))";
-val axb = "\\<forall>x y z. T(i(i x(i y z))(i(i x y)(i x z)))";
-val axc = "\\<forall>x y.   T(i(i(n x)(n y))(i y x))";
-val axd = "\\<forall>x y.   T(i x y) & T x --> T y";
-
-fun axjoin ([],   q) = q
-  | axjoin (p::ps, q) = "(" ^ p ^ ") --> (" ^ axjoin(ps,q) ^ ")";
-
-Goal (axjoin([axa,axb,axd], "\\<forall>x. T(i x x)"));
-by (meson_tac 1);  
-result();
-
-writeln"Problem 66";  
-Goal (axjoin([axa,axb,axc,axd], "\\<forall>x. T(i x(n(n x)))"));
-(*TOO SLOW, several minutes\\<forall> 
-     208346 inferences so far.  Searching to depth 23
-by (meson_tac 1);
-result();
-*)
-
-writeln"Problem 67";  
-Goal (axjoin([axa,axb,axc,axd], "\\<forall>x. T(i(n(n x)) x)"));
-(*TOO SLOW: more than 3 minutes!
-  51061 inferences so far.  Searching to depth 21
-by (meson_tac 1);
-result();
-*)
-
-
-(*Restore original values*)
-Unify.trace_bound := orig_trace_bound;
-Unify.search_bound := orig_search_bound;
-
-writeln"Reached end of file.";
-
-(*26 August 1992: loaded in 277 secs.  New Jersey v 75*)
diff -r 9fdea25f9ebb -r 4dc132902672 src/HOL/ex/mesontest2.ML
--- a/src/HOL/ex/mesontest2.ML	Fri Oct 03 12:36:16 2003 +0200
+++ b/src/HOL/ex/mesontest2.ML	Wed Oct 08 15:57:41 2003 +0200
@@ -3,7 +3,181 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   2000  University of Cambridge
 
-MORE and MUCH HARDER test data for the MESON proof procedure
+Test data for the MESON proof procedure
+   (Excludes the equality problems 51, 52, 56, 58)
+
+NOTE: most of the old file "mesontest.ML" has been converted to Isar and moved
+to Classical.thy
+
+Use the "mesonlog" shell script to process logs.
+
+show_hyps := false;
+
+proofs := 0;
+by (rtac ccontr 1);
+val [prem] = gethyps 1;
+val nnf = make_nnf prem;
+val xsko = skolemize nnf;
+by (cut_facts_tac [xsko] 1 THEN REPEAT (etac exE 1));
+val [_,sko] = gethyps 1;
+val clauses = make_clauses [sko];       
+val horns = make_horns clauses;
+val goes = gocls clauses;
+
+Goal "False";
+by (resolve_tac goes 1);
+proofs := 2;
+
+by (prolog_step_tac horns 1);
+by (iter_deepen_prolog_tac horns);
+by (depth_prolog_tac horns);
+by (best_prolog_tac size_of_subgoals horns);
+*)
+
+writeln"File HOL/ex/meson-test.";
+
+context Main.thy;
+
+(*Deep unifications can be required, esp. during transformation to clauses*)
+val orig_trace_bound = !Unify.trace_bound
+and orig_search_bound = !Unify.search_bound;
+Unify.trace_bound := 20;
+Unify.search_bound := 40;
+
+(**** Interactive examples ****)
+
+(*Generate nice names for Skolem functions*)
+Logic.auto_rename := true; Logic.set_rename_prefix "a";
+
+
+writeln"Problem 25";
+Goal "(\\<exists>x. P x) &  \
+\     (\\<forall>x. L x --> ~ (M x & R x)) &  \
+\     (\\<forall>x. P x --> (M x & L x)) &   \
+\     ((\\<forall>x. P x --> Q x) | (\\<exists>x. P x & R x))  \
+\   --> (\\<exists>x. Q x & P x)";
+by (rtac ccontr 1);
+val [prem25] = gethyps 1;
+val nnf25 = make_nnf prem25;
+val xsko25 = skolemize nnf25;
+by (cut_facts_tac [xsko25] 1 THEN REPEAT (etac exE 1));
+val [_,sko25] = gethyps 1;
+val clauses25 = make_clauses [sko25];   (*7 clauses*)
+val horns25 = make_horns clauses25;     (*16 Horn clauses*)
+val go25::_ = gocls clauses25;
+
+Goal "False";
+by (rtac go25 1);
+by (depth_prolog_tac horns25);
+
+
+writeln"Problem 26";
+Goal "((\\<exists>x. p x) = (\\<exists>x. q x)) &     \
+\     (\\<forall>x. \\<forall>y. p x & q y --> (r x = s y)) \
+\ --> ((\\<forall>x. p x --> r x) = (\\<forall>x. q x --> s x))";
+by (rtac ccontr 1);
+val [prem26] = gethyps 1;
+val nnf26 = make_nnf prem26;
+val xsko26 = skolemize nnf26;
+by (cut_facts_tac [xsko26] 1 THEN REPEAT (etac exE 1));
+val [_,sko26] = gethyps 1;
+val clauses26 = make_clauses [sko26];                   (*9 clauses*)
+val horns26 = make_horns clauses26;                     (*24 Horn clauses*)
+val go26::_ = gocls clauses26;
+
+Goal "False";
+by (rtac go26 1);
+by (depth_prolog_tac horns26);  (*1.4 secs*)
+(*Proof is of length 107!!*)
+
+
+writeln"Problem 43  NOW PROVED AUTOMATICALLY!!";  (*16 Horn clauses*)
+Goal "(\\<forall>x. \\<forall>y. q x y = (\\<forall>z. p z x = (p z y::bool)))  \
+\     --> (\\<forall>x. (\\<forall>y. q x y = (q y x::bool)))";
+by (rtac ccontr 1);
+val [prem43] = gethyps 1;
+val nnf43 = make_nnf prem43;
+val xsko43 = skolemize nnf43;
+by (cut_facts_tac [xsko43] 1 THEN REPEAT (etac exE 1));
+val [_,sko43] = gethyps 1;
+val clauses43 = make_clauses [sko43];   (*6*)
+val horns43 = make_horns clauses43;     (*16*)
+val go43::_ = gocls clauses43;
+
+Goal "False";
+by (rtac go43 1);
+by (best_prolog_tac size_of_subgoals horns43);   (*1.6 secs*)
+
+(* 
+#1  (q x xa ==> ~ q x xa) ==> q xa x
+#2  (q xa x ==> ~ q xa x) ==> q x xa
+#3  (~ q x xa ==> q x xa) ==> ~ q xa x
+#4  (~ q xa x ==> q xa x) ==> ~ q x xa
+#5  [| ~ q ?U ?V ==> q ?U ?V; ~ p ?W ?U ==> p ?W ?U |] ==> p ?W ?V
+#6  [| ~ p ?W ?U ==> p ?W ?U; p ?W ?V ==> ~ p ?W ?V |] ==> ~ q ?U ?V
+#7  [| p ?W ?V ==> ~ p ?W ?V; ~ q ?U ?V ==> q ?U ?V |] ==> ~ p ?W ?U
+#8  [| ~ q ?U ?V ==> q ?U ?V; ~ p ?W ?V ==> p ?W ?V |] ==> p ?W ?U
+#9  [| ~ p ?W ?V ==> p ?W ?V; p ?W ?U ==> ~ p ?W ?U |] ==> ~ q ?U ?V
+#10 [| p ?W ?U ==> ~ p ?W ?U; ~ q ?U ?V ==> q ?U ?V |] ==> ~ p ?W ?V
+#11 [| p (xb ?U ?V) ?U ==> ~ p (xb ?U ?V) ?U;
+       p (xb ?U ?V) ?V ==> ~ p (xb ?U ?V) ?V |] ==> q ?U ?V
+#12 [| p (xb ?U ?V) ?V ==> ~ p (xb ?U ?V) ?V; q ?U ?V ==> ~ q ?U ?V |] ==>
+    p (xb ?U ?V) ?U
+#13 [| q ?U ?V ==> ~ q ?U ?V; p (xb ?U ?V) ?U ==> ~ p (xb ?U ?V) ?U |] ==>
+    p (xb ?U ?V) ?V
+#14 [| ~ p (xb ?U ?V) ?U ==> p (xb ?U ?V) ?U;
+       ~ p (xb ?U ?V) ?V ==> p (xb ?U ?V) ?V |] ==> q ?U ?V
+#15 [| ~ p (xb ?U ?V) ?V ==> p (xb ?U ?V) ?V; q ?U ?V ==> ~ q ?U ?V |] ==>
+    ~ p (xb ?U ?V) ?U
+#16 [| q ?U ?V ==> ~ q ?U ?V; ~ p (xb ?U ?V) ?U ==> p (xb ?U ?V) ?U |] ==>
+    ~ p (xb ?U ?V) ?V
+
+And here is the proof! (Unkn is the start state after use of goal clause)
+[Unkn, Res ([Thm "#14"], false, 1), Res ([Thm "#5"], false, 1),
+   Res ([Thm "#1"], false, 1), Asm 1, Res ([Thm "#13"], false, 1), Asm 2,
+   Asm 1, Res ([Thm "#13"], false, 1), Asm 1, Res ([Thm "#10"], false, 1),
+   Res ([Thm "#16"], false, 1), Asm 2, Asm 1, Res ([Thm "#1"], false, 1),
+   Asm 1, Res ([Thm "#14"], false, 1), Res ([Thm "#5"], false, 1),
+   Res ([Thm "#2"], false, 1), Asm 1, Res ([Thm "#13"], false, 1), Asm 2,
+   Asm 1, Res ([Thm "#8"], false, 1), Res ([Thm "#2"], false, 1), Asm 1,
+   Res ([Thm "#12"], false, 1), Asm 2, Asm 1] : lderiv list
+*)
+
+
+(*Restore variable name preservation*)
+Logic.auto_rename := false; 
+
+
+(** Charles Morgan's problems **)
+
+val axa = "\\<forall>x y.   T(i x(i y x))";
+val axb = "\\<forall>x y z. T(i(i x(i y z))(i(i x y)(i x z)))";
+val axc = "\\<forall>x y.   T(i(i(n x)(n y))(i y x))";
+val axd = "\\<forall>x y.   T(i x y) & T x --> T y";
+
+fun axjoin ([],   q) = q
+  | axjoin (p::ps, q) = "(" ^ p ^ ") --> (" ^ axjoin(ps,q) ^ ")";
+
+Goal (axjoin([axa,axb,axd], "\\<forall>x. T(i x x)"));
+by (meson_tac 1);  
+result();
+
+writeln"Problem 66";  
+Goal (axjoin([axa,axb,axc,axd], "\\<forall>x. T(i x(n(n x)))"));
+by (meson_tac 1);  
+result();
+(*SLOW: 37s on a 1.8MHz machine
+     208346 inferences so far.  Searching to depth 23 *)
+
+writeln"Problem 67";  
+Goal (axjoin([axa,axb,axc,axd], "\\<forall>x. T(i(n(n x)) x)"));
+by (meson_tac 1);  
+result();
+(*10s on a 1.8MHz machine
+  51061 inferences so far.  Searching to depth 21 *)
+
+
+(*MORE and MUCH HARDER test data for the MESON proof procedure
 
 Courtesy John Harrison 
 
@@ -181,7 +355,7 @@
   meson_tac 1);
 
 (*51194 inferences so far.  Searching to depth 13. 204.6 secs
-  Strange\\<forall> The previous problem also has 51194 inferences at depth 13.  They
+  Strange! The previous problem also has 51194 inferences at depth 13.  They
    must be very similar!*)
 val BOO004_1 = prove_hard
  ("(\\<forall>X. equal(X::'a,X)) &  \
@@ -2948,7 +3122,7 @@
 \  (~subset(bDa::'a,bDd)) --> False",
   meson_tac 1);
 
-(*34726 inferences so far.  Searching to depth 6.  2420 secs: 40 mins\\<forall> BIG*)
+(*34726 inferences so far.  Searching to depth 6.  2420 secs: 40 mins! BIG*)
 val SET025_4 = prove_hard
  ("(\\<forall>X. equal(X::'a,X)) &  \
 \  (\\<forall>Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \