Merging of ex/cla.ML and ex/mesontest.ML to ex/Classical.thy
authorpaulson
Wed Oct 08 15:57:41 2003 +0200 (2003-10-08)
changeset 142204dc132902672
parent 14219 9fdea25f9ebb
child 14221 9276f30eaed6
Merging of ex/cla.ML and ex/mesontest.ML to ex/Classical.thy
src/HOL/IsaMakefile
src/HOL/ex/Classical.thy
src/HOL/ex/ROOT.ML
src/HOL/ex/cla.ML
src/HOL/ex/mesontest.ML
src/HOL/ex/mesontest2.ML
     1.1 --- a/src/HOL/IsaMakefile	Fri Oct 03 12:36:16 2003 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Wed Oct 08 15:57:41 2003 +0200
     1.3 @@ -592,7 +592,7 @@
     1.4    ex/NatSum.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy ex/Puzzle.thy \
     1.5    ex/Qsort.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy \
     1.6    ex/Ring.ML ex/Ring.thy ex/StringEx.thy ex/SVC_Oracle.ML ex/SVC_Oracle.thy \
     1.7 -  ex/Tarski.thy ex/Tuple.thy ex/cla.ML ex/mesontest.ML \
     1.8 +  ex/Tarski.thy ex/Tuple.thy ex/Classical.thy \
     1.9    ex/mesontest2.ML ex/mesontest2.thy ex/set.thy ex/svc_funcs.ML \
    1.10    ex/svc_test.ML ex/svc_test.thy ex/document/root.bib ex/document/root.tex
    1.11  	@$(ISATOOL) usedir $(OUT)/HOL ex
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/ex/Classical.thy	Wed Oct 08 15:57:41 2003 +0200
     2.3 @@ -0,0 +1,786 @@
     2.4 +(*  Title:      HOL/ex/Classical
     2.5 +    ID:         $Id$
     2.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 +    Copyright   1994  University of Cambridge
     2.8 +*)
     2.9 +
    2.10 +header{*Classical Predicate Calculus Problems*}
    2.11 +
    2.12 +theory Classical = Main:
    2.13 +
    2.14 +subsection{*Traditional Classical Reasoner*}
    2.15 +
    2.16 +text{*Taken from @{text "FOL/cla.ML"}. When porting examples from first-order
    2.17 +logic, beware of the precedence of @{text "="} versus @{text "\<leftrightarrow>"}.*}
    2.18 +
    2.19 +lemma "(P --> Q | R) --> (P-->Q) | (P-->R)"
    2.20 +by blast
    2.21 +
    2.22 +text{*If and only if*}
    2.23 +
    2.24 +lemma "(P=Q) = (Q = (P::bool))"
    2.25 +by blast
    2.26 +
    2.27 +lemma "~ (P = (~P))"
    2.28 +by blast
    2.29 +
    2.30 +
    2.31 +text{*Sample problems from 
    2.32 +  F. J. Pelletier, 
    2.33 +  Seventy-Five Problems for Testing Automatic Theorem Provers,
    2.34 +  J. Automated Reasoning 2 (1986), 191-216.
    2.35 +  Errata, JAR 4 (1988), 236-236.
    2.36 +
    2.37 +The hardest problems -- judging by experience with several theorem provers,
    2.38 +including matrix ones -- are 34 and 43.
    2.39 +*}
    2.40 +
    2.41 +subsubsection{*Pelletier's examples*}
    2.42 +
    2.43 +text{*1*}
    2.44 +lemma "(P-->Q)  =  (~Q --> ~P)"
    2.45 +by blast
    2.46 +
    2.47 +text{*2*}
    2.48 +lemma "(~ ~ P) =  P"
    2.49 +by blast
    2.50 +
    2.51 +text{*3*}
    2.52 +lemma "~(P-->Q) --> (Q-->P)"
    2.53 +by blast
    2.54 +
    2.55 +text{*4*}
    2.56 +lemma "(~P-->Q)  =  (~Q --> P)"
    2.57 +by blast
    2.58 +
    2.59 +text{*5*}
    2.60 +lemma "((P|Q)-->(P|R)) --> (P|(Q-->R))"
    2.61 +by blast
    2.62 +
    2.63 +text{*6*}
    2.64 +lemma "P | ~ P"
    2.65 +by blast
    2.66 +
    2.67 +text{*7*}
    2.68 +lemma "P | ~ ~ ~ P"
    2.69 +by blast
    2.70 +
    2.71 +text{*8.  Peirce's law*}
    2.72 +lemma "((P-->Q) --> P)  -->  P"
    2.73 +by blast
    2.74 +
    2.75 +text{*9*}
    2.76 +lemma "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
    2.77 +by blast
    2.78 +
    2.79 +text{*10*}
    2.80 +lemma "(Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P=Q)"
    2.81 +by blast
    2.82 +
    2.83 +text{*11.  Proved in each direction (incorrectly, says Pelletier!!)  *}
    2.84 +lemma "P=(P::bool)"
    2.85 +by blast
    2.86 +
    2.87 +text{*12.  "Dijkstra's law"*}
    2.88 +lemma "((P = Q) = R) = (P = (Q = R))"
    2.89 +by blast
    2.90 +
    2.91 +text{*13.  Distributive law*}
    2.92 +lemma "(P | (Q & R)) = ((P | Q) & (P | R))"
    2.93 +by blast
    2.94 +
    2.95 +text{*14*}
    2.96 +lemma "(P = Q) = ((Q | ~P) & (~Q|P))"
    2.97 +by blast
    2.98 +
    2.99 +text{*15*}
   2.100 +lemma "(P --> Q) = (~P | Q)"
   2.101 +by blast
   2.102 +
   2.103 +text{*16*}
   2.104 +lemma "(P-->Q) | (Q-->P)"
   2.105 +by blast
   2.106 +
   2.107 +text{*17*}
   2.108 +lemma "((P & (Q-->R))-->S)  =  ((~P | Q | S) & (~P | ~R | S))"
   2.109 +by blast
   2.110 +
   2.111 +subsubsection{*Classical Logic: examples with quantifiers*}
   2.112 +
   2.113 +lemma "(\<forall>x. P(x) & Q(x)) = ((\<forall>x. P(x)) & (\<forall>x. Q(x)))"
   2.114 +by blast
   2.115 +
   2.116 +lemma "(\<exists>x. P-->Q(x))  =  (P --> (\<exists>x. Q(x)))"
   2.117 +by blast
   2.118 +
   2.119 +lemma "(\<exists>x. P(x)-->Q) = ((\<forall>x. P(x)) --> Q)"
   2.120 +by blast
   2.121 +
   2.122 +lemma "((\<forall>x. P(x)) | Q)  =  (\<forall>x. P(x) | Q)"
   2.123 +by blast
   2.124 +
   2.125 +text{*From Wishnu Prasetya*}
   2.126 +lemma "(\<forall>s. q(s) --> r(s)) & ~r(s) & (\<forall>s. ~r(s) & ~q(s) --> p(t) | q(t))  
   2.127 +    --> p(t) | r(t)"
   2.128 +by blast
   2.129 +
   2.130 +
   2.131 +subsubsection{*Problems requiring quantifier duplication*}
   2.132 +
   2.133 +text{*Theorem B of Peter Andrews, Theorem Proving via General Matings, 
   2.134 +  JACM 28 (1981).*}
   2.135 +lemma "(\<exists>x. \<forall>y. P(x) = P(y)) --> ((\<exists>x. P(x)) = (\<forall>y. P(y)))"
   2.136 +by blast
   2.137 +
   2.138 +text{*Needs multiple instantiation of the quantifier.*}
   2.139 +lemma "(\<forall>x. P(x)-->P(f(x)))  &  P(d)-->P(f(f(f(d))))"
   2.140 +by blast
   2.141 +
   2.142 +text{*Needs double instantiation of the quantifier*}
   2.143 +lemma "\<exists>x. P(x) --> P(a) & P(b)"
   2.144 +by blast
   2.145 +
   2.146 +lemma "\<exists>z. P(z) --> (\<forall>x. P(x))"
   2.147 +by blast
   2.148 +
   2.149 +lemma "\<exists>x. (\<exists>y. P(y)) --> P(x)"
   2.150 +by blast
   2.151 +
   2.152 +subsubsection{*Hard examples with quantifiers*}
   2.153 +
   2.154 +text{*Problem 18*}
   2.155 +lemma "\<exists>y. \<forall>x. P(y)-->P(x)"
   2.156 +by blast
   2.157 +
   2.158 +text{*Problem 19*}
   2.159 +lemma "\<exists>x. \<forall>y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))"
   2.160 +by blast
   2.161 +
   2.162 +text{*Problem 20*}
   2.163 +lemma "(\<forall>x y. \<exists>z. \<forall>w. (P(x)&Q(y)-->R(z)&S(w)))      
   2.164 +    --> (\<exists>x y. P(x) & Q(y)) --> (\<exists>z. R(z))"
   2.165 +by blast
   2.166 +
   2.167 +text{*Problem 21*}
   2.168 +lemma "(\<exists>x. P-->Q(x)) & (\<exists>x. Q(x)-->P) --> (\<exists>x. P=Q(x))"
   2.169 +by blast
   2.170 +
   2.171 +text{*Problem 22*}
   2.172 +lemma "(\<forall>x. P = Q(x))  -->  (P = (\<forall>x. Q(x)))"
   2.173 +by blast
   2.174 +
   2.175 +text{*Problem 23*}
   2.176 +lemma "(\<forall>x. P | Q(x))  =  (P | (\<forall>x. Q(x)))"
   2.177 +by blast
   2.178 +
   2.179 +text{*Problem 24*}
   2.180 +lemma "~(\<exists>x. S(x)&Q(x)) & (\<forall>x. P(x) --> Q(x)|R(x)) &   
   2.181 +     (~(\<exists>x. P(x)) --> (\<exists>x. Q(x))) & (\<forall>x. Q(x)|R(x) --> S(x))   
   2.182 +    --> (\<exists>x. P(x)&R(x))"
   2.183 +by blast
   2.184 +
   2.185 +text{*Problem 25*}
   2.186 +lemma "(\<exists>x. P(x)) &   
   2.187 +        (\<forall>x. L(x) --> ~ (M(x) & R(x))) &   
   2.188 +        (\<forall>x. P(x) --> (M(x) & L(x))) &    
   2.189 +        ((\<forall>x. P(x)-->Q(x)) | (\<exists>x. P(x)&R(x)))   
   2.190 +    --> (\<exists>x. Q(x)&P(x))"
   2.191 +by blast
   2.192 +
   2.193 +text{*Problem 26*}
   2.194 +lemma "((\<exists>x. p(x)) = (\<exists>x. q(x))) &      
   2.195 +      (\<forall>x. \<forall>y. p(x) & q(y) --> (r(x) = s(y)))  
   2.196 +  --> ((\<forall>x. p(x)-->r(x)) = (\<forall>x. q(x)-->s(x)))"
   2.197 +by blast
   2.198 +
   2.199 +text{*Problem 27*}
   2.200 +lemma "(\<exists>x. P(x) & ~Q(x)) &    
   2.201 +              (\<forall>x. P(x) --> R(x)) &    
   2.202 +              (\<forall>x. M(x) & L(x) --> P(x)) &    
   2.203 +              ((\<exists>x. R(x) & ~ Q(x)) --> (\<forall>x. L(x) --> ~ R(x)))   
   2.204 +          --> (\<forall>x. M(x) --> ~L(x))"
   2.205 +by blast
   2.206 +
   2.207 +text{*Problem 28.  AMENDED*}
   2.208 +lemma "(\<forall>x. P(x) --> (\<forall>x. Q(x))) &    
   2.209 +        ((\<forall>x. Q(x)|R(x)) --> (\<exists>x. Q(x)&S(x))) &   
   2.210 +        ((\<exists>x. S(x)) --> (\<forall>x. L(x) --> M(x)))   
   2.211 +    --> (\<forall>x. P(x) & L(x) --> M(x))"
   2.212 +by blast
   2.213 +
   2.214 +text{*Problem 29.  Essentially the same as Principia Mathematica *11.71*}
   2.215 +lemma "(\<exists>x. F(x)) & (\<exists>y. G(y))   
   2.216 +    --> ( ((\<forall>x. F(x)-->H(x)) & (\<forall>y. G(y)-->J(y)))  =    
   2.217 +          (\<forall>x y. F(x) & G(y) --> H(x) & J(y)))"
   2.218 +by blast
   2.219 +
   2.220 +text{*Problem 30*}
   2.221 +lemma "(\<forall>x. P(x) | Q(x) --> ~ R(x)) &  
   2.222 +        (\<forall>x. (Q(x) --> ~ S(x)) --> P(x) & R(x))   
   2.223 +    --> (\<forall>x. S(x))"
   2.224 +by blast
   2.225 +
   2.226 +text{*Problem 31*}
   2.227 +lemma "~(\<exists>x. P(x) & (Q(x) | R(x))) &  
   2.228 +        (\<exists>x. L(x) & P(x)) &  
   2.229 +        (\<forall>x. ~ R(x) --> M(x))   
   2.230 +    --> (\<exists>x. L(x) & M(x))"
   2.231 +by blast
   2.232 +
   2.233 +text{*Problem 32*}
   2.234 +lemma "(\<forall>x. P(x) & (Q(x)|R(x))-->S(x)) &  
   2.235 +        (\<forall>x. S(x) & R(x) --> L(x)) &  
   2.236 +        (\<forall>x. M(x) --> R(x))   
   2.237 +    --> (\<forall>x. P(x) & M(x) --> L(x))"
   2.238 +by blast
   2.239 +
   2.240 +text{*Problem 33*}
   2.241 +lemma "(\<forall>x. P(a) & (P(x)-->P(b))-->P(c))  =     
   2.242 +     (\<forall>x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))"
   2.243 +by blast
   2.244 +
   2.245 +text{*Problem 34  AMENDED (TWICE!!)*}
   2.246 +text{*Andrews's challenge*}
   2.247 +lemma "((\<exists>x. \<forall>y. p(x) = p(y))  =                
   2.248 +               ((\<exists>x. q(x)) = (\<forall>y. p(y))))   =     
   2.249 +              ((\<exists>x. \<forall>y. q(x) = q(y))  =           
   2.250 +               ((\<exists>x. p(x)) = (\<forall>y. q(y))))"
   2.251 +by blast
   2.252 +
   2.253 +text{*Problem 35*}
   2.254 +lemma "\<exists>x y. P x y -->  (\<forall>u v. P u v)"
   2.255 +by blast
   2.256 +
   2.257 +text{*Problem 36*}
   2.258 +lemma "(\<forall>x. \<exists>y. J x y) &  
   2.259 +        (\<forall>x. \<exists>y. G x y) &  
   2.260 +        (\<forall>x y. J x y | G x y -->        
   2.261 +        (\<forall>z. J y z | G y z --> H x z))    
   2.262 +    --> (\<forall>x. \<exists>y. H x y)"
   2.263 +by blast
   2.264 +
   2.265 +text{*Problem 37*}
   2.266 +lemma "(\<forall>z. \<exists>w. \<forall>x. \<exists>y.  
   2.267 +           (P x z -->P y w) & P y z & (P y w --> (\<exists>u. Q u w))) &  
   2.268 +        (\<forall>x z. ~(P x z) --> (\<exists>y. Q y z)) &  
   2.269 +        ((\<exists>x y. Q x y) --> (\<forall>x. R x x))   
   2.270 +    --> (\<forall>x. \<exists>y. R x y)"
   2.271 +by blast
   2.272 +
   2.273 +text{*Problem 38*}
   2.274 +lemma "(\<forall>x. p(a) & (p(x) --> (\<exists>y. p(y) & r x y)) -->             
   2.275 +           (\<exists>z. \<exists>w. p(z) & r x w & r w z))  =                  
   2.276 +     (\<forall>x. (~p(a) | p(x) | (\<exists>z. \<exists>w. p(z) & r x w & r w z)) &   
   2.277 +           (~p(a) | ~(\<exists>y. p(y) & r x y) |                       
   2.278 +            (\<exists>z. \<exists>w. p(z) & r x w & r w z)))"
   2.279 +by blast (*beats fast!*)
   2.280 +
   2.281 +text{*Problem 39*}
   2.282 +lemma "~ (\<exists>x. \<forall>y. F y x = (~ F y y))"
   2.283 +by blast
   2.284 +
   2.285 +text{*Problem 40.  AMENDED*}
   2.286 +lemma "(\<exists>y. \<forall>x. F x y = F x x)   
   2.287 +        -->  ~ (\<forall>x. \<exists>y. \<forall>z. F z y = (~ F z x))"
   2.288 +by blast
   2.289 +
   2.290 +text{*Problem 41*}
   2.291 +lemma "(\<forall>z. \<exists>y. \<forall>x. f x y = (f x z & ~ f x x))         
   2.292 +               --> ~ (\<exists>z. \<forall>x. f x z)"
   2.293 +by blast
   2.294 +
   2.295 +text{*Problem 42*}
   2.296 +lemma "~ (\<exists>y. \<forall>x. p x y = (~ (\<exists>z. p x z & p z x)))"
   2.297 +by blast
   2.298 +
   2.299 +text{*Problem 43!!*}
   2.300 +lemma "(\<forall>x::'a. \<forall>y::'a. q x y = (\<forall>z. p z x = (p z y::bool)))    
   2.301 +  --> (\<forall>x. (\<forall>y. q x y = (q y x::bool)))"
   2.302 +by blast
   2.303 +
   2.304 +text{*Problem 44*}
   2.305 +lemma "(\<forall>x. f(x) -->                                     
   2.306 +              (\<exists>y. g(y) & h x y & (\<exists>y. g(y) & ~ h x y)))  &    
   2.307 +              (\<exists>x. j(x) & (\<forall>y. g(y) --> h x y))                
   2.308 +              --> (\<exists>x. j(x) & ~f(x))"
   2.309 +by blast
   2.310 +
   2.311 +text{*Problem 45*}
   2.312 +lemma "(\<forall>x. f(x) & (\<forall>y. g(y) & h x y --> j x y)  
   2.313 +                      --> (\<forall>y. g(y) & h x y --> k(y))) &        
   2.314 +     ~ (\<exists>y. l(y) & k(y)) &                                      
   2.315 +     (\<exists>x. f(x) & (\<forall>y. h x y --> l(y))                          
   2.316 +                & (\<forall>y. g(y) & h x y --> j x y))                 
   2.317 +      --> (\<exists>x. f(x) & ~ (\<exists>y. g(y) & h x y))"
   2.318 +by blast
   2.319 +
   2.320 +
   2.321 +subsubsection{*Problems (mainly) involving equality or functions*}
   2.322 +
   2.323 +text{*Problem 48*}
   2.324 +lemma "(a=b | c=d) & (a=c | b=d) --> a=d | b=c"
   2.325 +by blast
   2.326 +
   2.327 +text{*Problem 49  NOT PROVED AUTOMATICALLY*}
   2.328 +text{*Hard because it involves substitution for Vars
   2.329 +  the type constraint ensures that x,y,z have the same type as a,b,u. *}
   2.330 +lemma "(\<exists>x y::'a. \<forall>z. z=x | z=y) & P(a) & P(b) & (~a=b)  
   2.331 +                --> (\<forall>u::'a. P(u))"
   2.332 +apply safe
   2.333 +apply (rule_tac x = a in allE, assumption)
   2.334 +apply (rule_tac x = b in allE, assumption, fast)  --{*blast's treatment of equality can't do it*}
   2.335 +done
   2.336 +
   2.337 +text{*Problem 50.  (What has this to do with equality?) *}
   2.338 +lemma "(\<forall>x. P a x | (\<forall>y. P x y)) --> (\<exists>x. \<forall>y. P x y)"
   2.339 +by blast
   2.340 +
   2.341 +text{*Problem 51*}
   2.342 +lemma "(\<exists>z w. \<forall>x y. P x y = (x=z & y=w)) -->   
   2.343 +     (\<exists>z. \<forall>x. \<exists>w. (\<forall>y. P x y = (y=w)) = (x=z))"
   2.344 +by blast
   2.345 +
   2.346 +text{*Problem 52. Almost the same as 51. *}
   2.347 +lemma "(\<exists>z w. \<forall>x y. P x y = (x=z & y=w)) -->   
   2.348 +     (\<exists>w. \<forall>y. \<exists>z. (\<forall>x. P x y = (x=z)) = (y=w))"
   2.349 +by blast
   2.350 +
   2.351 +text{*Problem 55*}
   2.352 +
   2.353 +text{*Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988).
   2.354 +  fast DISCOVERS who killed Agatha. *}
   2.355 +lemma "lives(agatha) & lives(butler) & lives(charles) &  
   2.356 +   (killed agatha agatha | killed butler agatha | killed charles agatha) &  
   2.357 +   (\<forall>x y. killed x y --> hates x y & ~richer x y) &  
   2.358 +   (\<forall>x. hates agatha x --> ~hates charles x) &  
   2.359 +   (hates agatha agatha & hates agatha charles) &  
   2.360 +   (\<forall>x. lives(x) & ~richer x agatha --> hates butler x) &  
   2.361 +   (\<forall>x. hates agatha x --> hates butler x) &  
   2.362 +   (\<forall>x. ~hates x agatha | ~hates x butler | ~hates x charles) -->  
   2.363 +    killed ?who agatha"
   2.364 +by fast
   2.365 +
   2.366 +text{*Problem 56*}
   2.367 +lemma "(\<forall>x. (\<exists>y. P(y) & x=f(y)) --> P(x)) = (\<forall>x. P(x) --> P(f(x)))"
   2.368 +by blast
   2.369 +
   2.370 +text{*Problem 57*}
   2.371 +lemma "P (f a b) (f b c) & P (f b c) (f a c) &  
   2.372 +     (\<forall>x y z. P x y & P y z --> P x z)    -->   P (f a b) (f a c)"
   2.373 +by blast
   2.374 +
   2.375 +text{*Problem 58  NOT PROVED AUTOMATICALLY*}
   2.376 +lemma "(\<forall>x y. f(x)=g(y)) --> (\<forall>x y. f(f(x))=f(g(y)))"
   2.377 +by (fast intro: arg_cong [of concl: f])
   2.378 +
   2.379 +text{*Problem 59*}
   2.380 +lemma "(\<forall>x. P(x) = (~P(f(x)))) --> (\<exists>x. P(x) & ~P(f(x)))"
   2.381 +by blast
   2.382 +
   2.383 +text{*Problem 60*}
   2.384 +lemma "\<forall>x. P x (f x) = (\<exists>y. (\<forall>z. P z y --> P z (f x)) & P x y)"
   2.385 +by blast
   2.386 +
   2.387 +text{*Problem 62 as corrected in JAR 18 (1997), page 135*}
   2.388 +lemma "(\<forall>x. p a & (p x --> p(f x)) --> p(f(f x)))  =    
   2.389 +      (\<forall>x. (~ p a | p x | p(f(f x))) &                         
   2.390 +              (~ p a | ~ p(f x) | p(f(f x))))"
   2.391 +by blast
   2.392 +
   2.393 +text{*From Davis, Obvious Logical Inferences, IJCAI-81, 530-531
   2.394 +  fast indeed copes!*}
   2.395 +lemma "(\<forall>x. F(x) & ~G(x) --> (\<exists>y. H(x,y) & J(y))) &  
   2.396 +       (\<exists>x. K(x) & F(x) & (\<forall>y. H(x,y) --> K(y))) &    
   2.397 +       (\<forall>x. K(x) --> ~G(x))  -->  (\<exists>x. K(x) & J(x))"
   2.398 +by fast
   2.399 +
   2.400 +text{*From Rudnicki, Obvious Inferences, JAR 3 (1987), 383-393.  
   2.401 +  It does seem obvious!*}
   2.402 +lemma "(\<forall>x. F(x) & ~G(x) --> (\<exists>y. H(x,y) & J(y))) &         
   2.403 +       (\<exists>x. K(x) & F(x) & (\<forall>y. H(x,y) --> K(y)))  &         
   2.404 +       (\<forall>x. K(x) --> ~G(x))   -->   (\<exists>x. K(x) --> ~G(x))"
   2.405 +by fast
   2.406 +
   2.407 +text{*Attributed to Lewis Carroll by S. G. Pulman.  The first or last 
   2.408 +assumption can be deleted.*}
   2.409 +lemma "(\<forall>x. honest(x) & industrious(x) --> healthy(x)) &  
   2.410 +      ~ (\<exists>x. grocer(x) & healthy(x)) &  
   2.411 +      (\<forall>x. industrious(x) & grocer(x) --> honest(x)) &  
   2.412 +      (\<forall>x. cyclist(x) --> industrious(x)) &  
   2.413 +      (\<forall>x. ~healthy(x) & cyclist(x) --> ~honest(x))   
   2.414 +      --> (\<forall>x. grocer(x) --> ~cyclist(x))"
   2.415 +by blast
   2.416 +
   2.417 +lemma "(\<forall>x y. R(x,y) | R(y,x)) &                 
   2.418 +       (\<forall>x y. S(x,y) & S(y,x) --> x=y) &         
   2.419 +       (\<forall>x y. R(x,y) --> S(x,y))    -->   (\<forall>x y. S(x,y) --> R(x,y))"
   2.420 +by blast
   2.421 +
   2.422 +
   2.423 +subsection{*Model Elimination Prover*}
   2.424 +
   2.425 +text{*The "small example" from Bezem, Hendriks and de Nivelle,
   2.426 +Automatic Proof Construction in Type Theory Using Resolution,
   2.427 +JAR 29: 3-4 (2002), pages 253-275 *}
   2.428 +lemma "(\<forall>x y z. R(x,y) & R(y,z) --> R(x,z)) &
   2.429 +       (\<forall>x. \<exists>y. R(x,y)) -->
   2.430 +       ~ (\<forall>x. P x = (\<forall>y. R(x,y) --> ~ P y))"
   2.431 +by (tactic{*safe_best_meson_tac 1*})
   2.432 +    --{*In contrast, @{text meson} is SLOW: 15s on a 1.8GHz machine!*}
   2.433 +
   2.434 +
   2.435 +subsubsection{*Pelletier's examples*}
   2.436 +text{*1*}
   2.437 +lemma "(P --> Q)  =  (~Q --> ~P)"
   2.438 +by meson
   2.439 +
   2.440 +text{*2*}
   2.441 +lemma "(~ ~ P) =  P"
   2.442 +by meson
   2.443 +
   2.444 +text{*3*}
   2.445 +lemma "~(P-->Q) --> (Q-->P)"
   2.446 +by meson
   2.447 +
   2.448 +text{*4*}
   2.449 +lemma "(~P-->Q)  =  (~Q --> P)"
   2.450 +by meson
   2.451 +
   2.452 +text{*5*}
   2.453 +lemma "((P|Q)-->(P|R)) --> (P|(Q-->R))"
   2.454 +by meson
   2.455 +
   2.456 +text{*6*}
   2.457 +lemma "P | ~ P"
   2.458 +by meson
   2.459 +
   2.460 +text{*7*}
   2.461 +lemma "P | ~ ~ ~ P"
   2.462 +by meson
   2.463 +
   2.464 +text{*8.  Peirce's law*}
   2.465 +lemma "((P-->Q) --> P)  -->  P"
   2.466 +by meson
   2.467 +
   2.468 +text{*9*}
   2.469 +lemma "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
   2.470 +by meson
   2.471 +
   2.472 +text{*10*}
   2.473 +lemma "(Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P=Q)"
   2.474 +by meson
   2.475 +
   2.476 +text{*11.  Proved in each direction (incorrectly, says Pelletier!!)  *}
   2.477 +lemma "P=(P::bool)"
   2.478 +by meson
   2.479 +
   2.480 +text{*12.  "Dijkstra's law"*}
   2.481 +lemma "((P = Q) = R) = (P = (Q = R))"
   2.482 +by meson
   2.483 +
   2.484 +text{*13.  Distributive law*}
   2.485 +lemma "(P | (Q & R)) = ((P | Q) & (P | R))"
   2.486 +by meson
   2.487 +
   2.488 +text{*14*}
   2.489 +lemma "(P = Q) = ((Q | ~P) & (~Q|P))"
   2.490 +by meson
   2.491 +
   2.492 +text{*15*}
   2.493 +lemma "(P --> Q) = (~P | Q)"
   2.494 +by meson
   2.495 +
   2.496 +text{*16*}
   2.497 +lemma "(P-->Q) | (Q-->P)"
   2.498 +by meson
   2.499 +
   2.500 +text{*17*}
   2.501 +lemma "((P & (Q-->R))-->S)  =  ((~P | Q | S) & (~P | ~R | S))"
   2.502 +by meson
   2.503 +
   2.504 +subsubsection{*Classical Logic: examples with quantifiers*}
   2.505 +
   2.506 +lemma "(\<forall>x. P x & Q x) = ((\<forall>x. P x) & (\<forall>x. Q x))"
   2.507 +by meson
   2.508 +
   2.509 +lemma "(\<exists>x. P --> Q x)  =  (P --> (\<exists>x. Q x))"
   2.510 +by meson
   2.511 +
   2.512 +lemma "(\<exists>x. P x --> Q) = ((\<forall>x. P x) --> Q)"
   2.513 +by meson
   2.514 +
   2.515 +lemma "((\<forall>x. P x) | Q)  =  (\<forall>x. P x | Q)"
   2.516 +by meson
   2.517 +
   2.518 +lemma "(\<forall>x. P x --> P(f x))  &  P d --> P(f(f(f d)))"
   2.519 +by meson
   2.520 +
   2.521 +text{*Needs double instantiation of EXISTS*}
   2.522 +lemma "\<exists>x. P x --> P a & P b"
   2.523 +by meson
   2.524 +
   2.525 +lemma "\<exists>z. P z --> (\<forall>x. P x)"
   2.526 +by meson
   2.527 +
   2.528 +subsubsection{*Hard examples with quantifiers*}
   2.529 +
   2.530 +text{*Problem 18*}
   2.531 +lemma "\<exists>y. \<forall>x. P y --> P x"
   2.532 +by meson
   2.533 +
   2.534 +text{*Problem 19*}
   2.535 +lemma "\<exists>x. \<forall>y z. (P y --> Q z) --> (P x --> Q x)"
   2.536 +by meson
   2.537 +
   2.538 +text{*Problem 20*}
   2.539 +lemma "(\<forall>x y. \<exists>z. \<forall>w. (P x & Q y --> R z & S w))      
   2.540 +    --> (\<exists>x y. P x & Q y) --> (\<exists>z. R z)"
   2.541 +by meson
   2.542 +
   2.543 +text{*Problem 21*}
   2.544 +lemma "(\<exists>x. P --> Q x) & (\<exists>x. Q x --> P) --> (\<exists>x. P=Q x)"
   2.545 +by meson
   2.546 +
   2.547 +text{*Problem 22*}
   2.548 +lemma "(\<forall>x. P = Q x)  -->  (P = (\<forall>x. Q x))"
   2.549 +by meson
   2.550 +
   2.551 +text{*Problem 23*}
   2.552 +lemma "(\<forall>x. P | Q x)  =  (P | (\<forall>x. Q x))"
   2.553 +by meson
   2.554 +
   2.555 +text{*Problem 24*}  (*The first goal clause is useless*)
   2.556 +lemma "~(\<exists>x. S x & Q x) & (\<forall>x. P x --> Q x | R x) &   
   2.557 +      (~(\<exists>x. P x) --> (\<exists>x. Q x)) & (\<forall>x. Q x | R x --> S x)   
   2.558 +    --> (\<exists>x. P x & R x)"
   2.559 +by meson
   2.560 +
   2.561 +text{*Problem 25*}
   2.562 +lemma "(\<exists>x. P x) &   
   2.563 +      (\<forall>x. L x --> ~ (M x & R x)) &   
   2.564 +      (\<forall>x. P x --> (M x & L x)) &    
   2.565 +      ((\<forall>x. P x --> Q x) | (\<exists>x. P x & R x))   
   2.566 +    --> (\<exists>x. Q x & P x)"
   2.567 +by meson
   2.568 +
   2.569 +text{*Problem 26; has 24 Horn clauses*}
   2.570 +lemma "((\<exists>x. p x) = (\<exists>x. q x)) &      
   2.571 +      (\<forall>x. \<forall>y. p x & q y --> (r x = s y))  
   2.572 +  --> ((\<forall>x. p x --> r x) = (\<forall>x. q x --> s x))"
   2.573 +by meson
   2.574 +
   2.575 +text{*Problem 27; has 13 Horn clauses*}
   2.576 +lemma "(\<exists>x. P x & ~Q x) &    
   2.577 +      (\<forall>x. P x --> R x) &    
   2.578 +      (\<forall>x. M x & L x --> P x) &    
   2.579 +      ((\<exists>x. R x & ~ Q x) --> (\<forall>x. L x --> ~ R x))   
   2.580 +      --> (\<forall>x. M x --> ~L x)"
   2.581 +by meson
   2.582 +
   2.583 +text{*Problem 28.  AMENDED; has 14 Horn clauses*}
   2.584 +lemma "(\<forall>x. P x --> (\<forall>x. Q x)) &    
   2.585 +      ((\<forall>x. Q x | R x) --> (\<exists>x. Q x & S x)) &   
   2.586 +      ((\<exists>x. S x) --> (\<forall>x. L x --> M x))   
   2.587 +    --> (\<forall>x. P x & L x --> M x)"
   2.588 +by meson
   2.589 +
   2.590 +text{*Problem 29.  Essentially the same as Principia Mathematica
   2.591 +*11.71.  62 Horn clauses*}
   2.592 +lemma "(\<exists>x. F x) & (\<exists>y. G y)   
   2.593 +    --> ( ((\<forall>x. F x --> H x) & (\<forall>y. G y --> J y))  =    
   2.594 +          (\<forall>x y. F x & G y --> H x & J y))"
   2.595 +by meson
   2.596 +
   2.597 +
   2.598 +text{*Problem 30*}
   2.599 +lemma "(\<forall>x. P x | Q x --> ~ R x) & (\<forall>x. (Q x --> ~ S x) --> P x & R x)   
   2.600 +       --> (\<forall>x. S x)"
   2.601 +by meson
   2.602 +
   2.603 +text{*Problem 31; has 10 Horn clauses; first negative clauses is useless*}
   2.604 +lemma "~(\<exists>x. P x & (Q x | R x)) &  
   2.605 +      (\<exists>x. L x & P x) &  
   2.606 +      (\<forall>x. ~ R x --> M x)   
   2.607 +    --> (\<exists>x. L x & M x)"
   2.608 +by meson
   2.609 +
   2.610 +text{*Problem 32*}
   2.611 +lemma "(\<forall>x. P x & (Q x | R x)-->S x) &  
   2.612 +      (\<forall>x. S x & R x --> L x) &  
   2.613 +      (\<forall>x. M x --> R x)   
   2.614 +    --> (\<forall>x. P x & M x --> L x)"
   2.615 +by meson
   2.616 +
   2.617 +text{*Problem 33; has 55 Horn clauses*}
   2.618 +lemma "(\<forall>x. P a & (P x --> P b)-->P c)  =     
   2.619 +      (\<forall>x. (~P a | P x | P c) & (~P a | ~P b | P c))"
   2.620 +by meson
   2.621 +
   2.622 +text{*Problem 34  AMENDED (TWICE!!); has 924 Horn clauses*}
   2.623 +text{*Andrews's challenge*}
   2.624 +lemma "((\<exists>x. \<forall>y. p x = p y)  =                
   2.625 +       ((\<exists>x. q x) = (\<forall>y. p y)))     =        
   2.626 +      ((\<exists>x. \<forall>y. q x = q y)  =                
   2.627 +       ((\<exists>x. p x) = (\<forall>y. q y)))"
   2.628 +by meson
   2.629 +
   2.630 +text{*Problem 35*}
   2.631 +lemma "\<exists>x y. P x y -->  (\<forall>u v. P u v)"
   2.632 +by meson
   2.633 +
   2.634 +text{*Problem 36; has 15 Horn clauses*}
   2.635 +lemma "(\<forall>x. \<exists>y. J x y) &  
   2.636 +      (\<forall>x. \<exists>y. G x y) &  
   2.637 +      (\<forall>x y. J x y | G x y -->        
   2.638 +      (\<forall>z. J y z | G y z --> H x z))    
   2.639 +    --> (\<forall>x. \<exists>y. H x y)"
   2.640 +by meson
   2.641 +
   2.642 +text{*Problem 37; has 10 Horn clauses*}
   2.643 +lemma "(\<forall>z. \<exists>w. \<forall>x. \<exists>y.  
   2.644 +           (P x z --> P y w) & P y z & (P y w --> (\<exists>u. Q u w))) &  
   2.645 +      (\<forall>x z. ~P x z --> (\<exists>y. Q y z)) &  
   2.646 +      ((\<exists>x y. Q x y) --> (\<forall>x. R x x))   
   2.647 +    --> (\<forall>x. \<exists>y. R x y)"
   2.648 +by meson --{*causes unification tracing messages*}
   2.649 +
   2.650 +
   2.651 +text{*Problem 38*}  text{*Quite hard: 422 Horn clauses!!*}
   2.652 +lemma "(\<forall>x. p a & (p x --> (\<exists>y. p y & r x y)) -->             
   2.653 +           (\<exists>z. \<exists>w. p z & r x w & r w z))  =                  
   2.654 +      (\<forall>x. (~p a | p x | (\<exists>z. \<exists>w. p z & r x w & r w z)) &   
   2.655 +            (~p a | ~(\<exists>y. p y & r x y) |                       
   2.656 +             (\<exists>z. \<exists>w. p z & r x w & r w z)))"
   2.657 +by meson
   2.658 +
   2.659 +text{*Problem 39*}
   2.660 +lemma "~ (\<exists>x. \<forall>y. F y x = (~F y y))"
   2.661 +by meson
   2.662 +
   2.663 +text{*Problem 40.  AMENDED*}
   2.664 +lemma "(\<exists>y. \<forall>x. F x y = F x x)   
   2.665 +      -->  ~ (\<forall>x. \<exists>y. \<forall>z. F z y = (~F z x))"
   2.666 +by meson
   2.667 +
   2.668 +text{*Problem 41*}
   2.669 +lemma "(\<forall>z. (\<exists>y. (\<forall>x. f x y = (f x z & ~ f x x))))     
   2.670 +      --> ~ (\<exists>z. \<forall>x. f x z)"
   2.671 +by meson
   2.672 +
   2.673 +text{*Problem 42*}
   2.674 +lemma "~ (\<exists>y. \<forall>x. p x y = (~ (\<exists>z. p x z & p z x)))"
   2.675 +by meson
   2.676 +
   2.677 +text{*Problem 43  NOW PROVED AUTOMATICALLY!!*}
   2.678 +lemma "(\<forall>x. \<forall>y. q x y = (\<forall>z. p z x = (p z y::bool)))   
   2.679 +      --> (\<forall>x. (\<forall>y. q x y = (q y x::bool)))"
   2.680 +by meson
   2.681 +
   2.682 +text{*Problem 44: 13 Horn clauses; 7-step proof*}
   2.683 +lemma "(\<forall>x. f x -->                                     
   2.684 +            (\<exists>y. g y & h x y & (\<exists>y. g y & ~ h x y)))  &    
   2.685 +      (\<exists>x. j x & (\<forall>y. g y --> h x y))                
   2.686 +      --> (\<exists>x. j x & ~f x)"
   2.687 +by meson
   2.688 +
   2.689 +text{*Problem 45; has 27 Horn clauses; 54-step proof*}
   2.690 +lemma "(\<forall>x. f x & (\<forall>y. g y & h x y --> j x y)         
   2.691 +            --> (\<forall>y. g y & h x y --> k y)) &        
   2.692 +      ~ (\<exists>y. l y & k y) &                                     
   2.693 +      (\<exists>x. f x & (\<forall>y. h x y --> l y)                         
   2.694 +                & (\<forall>y. g y & h x y --> j x y))              
   2.695 +      --> (\<exists>x. f x & ~ (\<exists>y. g y & h x y))"
   2.696 +by meson
   2.697 +
   2.698 +text{*Problem 46; has 26 Horn clauses; 21-step proof*}
   2.699 +lemma "(\<forall>x. f x & (\<forall>y. f y & h y x --> g y) --> g x) &       
   2.700 +      ((\<exists>x. f x & ~g x) -->                                     
   2.701 +      (\<exists>x. f x & ~g x & (\<forall>y. f y & ~g y --> j x y))) &     
   2.702 +      (\<forall>x y. f x & f y & h x y --> ~j y x)                     
   2.703 +      --> (\<forall>x. f x --> g x)"
   2.704 +by meson
   2.705 +
   2.706 +text{*Problem 47.  Schubert's Steamroller*}
   2.707 +        text{*26 clauses; 63 Horn clauses
   2.708 +          87094 inferences so far.  Searching to depth 36*}
   2.709 +lemma "(\<forall>x. P1 x --> P0 x) & (\<exists>x. P1 x) &      
   2.710 +      (\<forall>x. P2 x --> P0 x) & (\<exists>x. P2 x) &      
   2.711 +      (\<forall>x. P3 x --> P0 x) & (\<exists>x. P3 x) &      
   2.712 +      (\<forall>x. P4 x --> P0 x) & (\<exists>x. P4 x) &      
   2.713 +      (\<forall>x. P5 x --> P0 x) & (\<exists>x. P5 x) &      
   2.714 +      (\<forall>x. Q1 x --> Q0 x) & (\<exists>x. Q1 x) &      
   2.715 +      (\<forall>x. P0 x --> ((\<forall>y. Q0 y-->R x y) |     
   2.716 +                       (\<forall>y. P0 y & S y x &      
   2.717 +                            (\<exists>z. Q0 z&R y z) --> R x y))) &    
   2.718 +      (\<forall>x y. P3 y & (P5 x|P4 x) --> S x y) &         
   2.719 +      (\<forall>x y. P3 x & P2 y --> S x y) &         
   2.720 +      (\<forall>x y. P2 x & P1 y --> S x y) &         
   2.721 +      (\<forall>x y. P1 x & (P2 y|Q1 y) --> ~R x y) &        
   2.722 +      (\<forall>x y. P3 x & P4 y --> R x y) &         
   2.723 +      (\<forall>x y. P3 x & P5 y --> ~R x y) &        
   2.724 +      (\<forall>x. (P4 x|P5 x) --> (\<exists>y. Q0 y & R x y))       
   2.725 +      --> (\<exists>x y. P0 x & P0 y & (\<exists>z. Q1 z & R y z & R x y))"
   2.726 +by (tactic{*safe_best_meson_tac 1*})
   2.727 +    --{*Considerably faster than @{text meson}, 
   2.728 +        which does iterative deepening rather than best-first search*}
   2.729 +
   2.730 +text{*The Los problem. Circulated by John Harrison*}
   2.731 +lemma "(\<forall>x y z. P x y & P y z --> P x z) &       
   2.732 +      (\<forall>x y z. Q x y & Q y z --> Q x z) &              
   2.733 +      (\<forall>x y. P x y --> P y x) &                        
   2.734 +      (\<forall>x y. P x y | Q x y)                            
   2.735 +      --> (\<forall>x y. P x y) | (\<forall>x y. Q x y)"
   2.736 +by meson
   2.737 +
   2.738 +text{*A similar example, suggested by Johannes Schumann and
   2.739 + credited to Pelletier*}
   2.740 +lemma "(\<forall>x y z. P x y --> P y z --> P x z) -->  
   2.741 +      (\<forall>x y z. Q x y --> Q y z --> Q x z) -->  
   2.742 +      (\<forall>x y. Q x y --> Q y x) -->  (\<forall>x y. P x y | Q x y) -->  
   2.743 +      (\<forall>x y. P x y) | (\<forall>x y. Q x y)"
   2.744 +by meson
   2.745 +
   2.746 +text{*Problem 50.  What has this to do with equality?*}
   2.747 +lemma "(\<forall>x. P a x | (\<forall>y. P x y)) --> (\<exists>x. \<forall>y. P x y)"
   2.748 +by meson
   2.749 +
   2.750 +text{*Problem 55*}
   2.751 +
   2.752 +text{*Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988).
   2.753 +  @{text meson} cannot report who killed Agatha. *}
   2.754 +lemma "lives agatha & lives butler & lives charles &  
   2.755 +      (killed agatha agatha | killed butler agatha | killed charles agatha) &  
   2.756 +      (\<forall>x y. killed x y --> hates x y & ~richer x y) &  
   2.757 +      (\<forall>x. hates agatha x --> ~hates charles x) &  
   2.758 +      (hates agatha agatha & hates agatha charles) &  
   2.759 +      (\<forall>x. lives x & ~richer x agatha --> hates butler x) &  
   2.760 +      (\<forall>x. hates agatha x --> hates butler x) &  
   2.761 +      (\<forall>x. ~hates x agatha | ~hates x butler | ~hates x charles) -->  
   2.762 +      (\<exists>x. killed x agatha)"
   2.763 +by meson
   2.764 +
   2.765 +text{*Problem 57*}
   2.766 +lemma "P (f a b) (f b c) & P (f b c) (f a c) &  
   2.767 +      (\<forall>x y z. P x y & P y z --> P x z)    -->   P (f a b) (f a c)"
   2.768 +by meson
   2.769 +
   2.770 +text{*Problem 58*}
   2.771 +text{* Challenge found on info-hol *}
   2.772 +lemma "\<forall>P Q R x. \<exists>v w. \<forall>y z. P x & Q y --> (P v | R w) & (R z --> Q v)"
   2.773 +by meson
   2.774 +
   2.775 +text{*Problem 59*}
   2.776 +lemma "(\<forall>x. P x = (~P(f x))) --> (\<exists>x. P x & ~P(f x))"
   2.777 +by meson
   2.778 +
   2.779 +text{*Problem 60*}
   2.780 +lemma "\<forall>x. P x (f x) = (\<exists>y. (\<forall>z. P z y --> P z (f x)) & P x y)"
   2.781 +by meson
   2.782 +
   2.783 +text{*Problem 62 as corrected in JAR 18 (1997), page 135*}
   2.784 +lemma "(\<forall>x. p a & (p x --> p(f x)) --> p(f(f x)))  =    
   2.785 +      (\<forall>x. (~ p a | p x | p(f(f x))) &                         
   2.786 +              (~ p a | ~ p(f x) | p(f(f x))))"
   2.787 +by meson
   2.788 +
   2.789 +end
     3.1 --- a/src/HOL/ex/ROOT.ML	Fri Oct 03 12:36:16 2003 +0200
     3.2 +++ b/src/HOL/ex/ROOT.ML	Wed Oct 08 15:57:41 2003 +0200
     3.3 @@ -20,8 +20,7 @@
     3.4  
     3.5  time_use_thy "NatSum";
     3.6  time_use_thy "Intuitionistic";
     3.7 -time_use     "cla.ML";
     3.8 -time_use     "mesontest.ML";
     3.9 +time_use_thy "Classical";
    3.10  time_use_thy "mesontest2";
    3.11  time_use_thy "PresburgerEx";
    3.12  time_use_thy "BT";
     4.1 --- a/src/HOL/ex/cla.ML	Fri Oct 03 12:36:16 2003 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,501 +0,0 @@
     4.4 -(*  Title:      HOL/ex/cla
     4.5 -    ID:         $Id$
     4.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.7 -    Copyright   1994  University of Cambridge
     4.8 -
     4.9 -Higher-Order Logic: predicate calculus problems
    4.10 -
    4.11 -Taken from FOL/cla.ML; beware of precedence of = vs <->
    4.12 -*)
    4.13 -
    4.14 -writeln"File HOL/ex/cla.";
    4.15 -
    4.16 -context HOL.thy; 
    4.17 -
    4.18 -Goal "(P --> Q | R) --> (P-->Q) | (P-->R)";
    4.19 -by (Blast_tac 1);
    4.20 -result();
    4.21 -
    4.22 -(*If and only if*)
    4.23 -
    4.24 -Goal "(P=Q) = (Q = (P::bool))";
    4.25 -by (Blast_tac 1);
    4.26 -result();
    4.27 -
    4.28 -Goal "~ (P = (~P))";
    4.29 -by (Blast_tac 1);
    4.30 -result();
    4.31 -
    4.32 -
    4.33 -(*Sample problems from 
    4.34 -  F. J. Pelletier, 
    4.35 -  Seventy-Five Problems for Testing Automatic Theorem Provers,
    4.36 -  J. Automated Reasoning 2 (1986), 191-216.
    4.37 -  Errata, JAR 4 (1988), 236-236.
    4.38 -
    4.39 -The hardest problems -- judging by experience with several theorem provers,
    4.40 -including matrix ones -- are 34 and 43.
    4.41 -*)
    4.42 -
    4.43 -writeln"Pelletier's examples";
    4.44 -(*1*)
    4.45 -Goal "(P-->Q)  =  (~Q --> ~P)";
    4.46 -by (Blast_tac 1);
    4.47 -result();
    4.48 -
    4.49 -(*2*)
    4.50 -Goal "(~ ~ P) =  P";
    4.51 -by (Blast_tac 1);
    4.52 -result();
    4.53 -
    4.54 -(*3*)
    4.55 -Goal "~(P-->Q) --> (Q-->P)";
    4.56 -by (Blast_tac 1);
    4.57 -result();
    4.58 -
    4.59 -(*4*)
    4.60 -Goal "(~P-->Q)  =  (~Q --> P)";
    4.61 -by (Blast_tac 1);
    4.62 -result();
    4.63 -
    4.64 -(*5*)
    4.65 -Goal "((P|Q)-->(P|R)) --> (P|(Q-->R))";
    4.66 -by (Blast_tac 1);
    4.67 -result();
    4.68 -
    4.69 -(*6*)
    4.70 -Goal "P | ~ P";
    4.71 -by (Blast_tac 1);
    4.72 -result();
    4.73 -
    4.74 -(*7*)
    4.75 -Goal "P | ~ ~ ~ P";
    4.76 -by (Blast_tac 1);
    4.77 -result();
    4.78 -
    4.79 -(*8.  Peirce's law*)
    4.80 -Goal "((P-->Q) --> P)  -->  P";
    4.81 -by (Blast_tac 1);
    4.82 -result();
    4.83 -
    4.84 -(*9*)
    4.85 -Goal "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
    4.86 -by (Blast_tac 1);
    4.87 -result();
    4.88 -
    4.89 -(*10*)
    4.90 -Goal "(Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P=Q)";
    4.91 -by (Blast_tac 1);
    4.92 -result();
    4.93 -
    4.94 -(*11.  Proved in each direction (incorrectly, says Pelletier!!)  *)
    4.95 -Goal "P=(P::bool)";
    4.96 -by (Blast_tac 1);
    4.97 -result();
    4.98 -
    4.99 -(*12.  "Dijkstra's law"*)
   4.100 -Goal "((P = Q) = R) = (P = (Q = R))";
   4.101 -by (Blast_tac 1);
   4.102 -result();
   4.103 -
   4.104 -(*13.  Distributive law*)
   4.105 -Goal "(P | (Q & R)) = ((P | Q) & (P | R))";
   4.106 -by (Blast_tac 1);
   4.107 -result();
   4.108 -
   4.109 -(*14*)
   4.110 -Goal "(P = Q) = ((Q | ~P) & (~Q|P))";
   4.111 -by (Blast_tac 1);
   4.112 -result();
   4.113 -
   4.114 -(*15*)
   4.115 -Goal "(P --> Q) = (~P | Q)";
   4.116 -by (Blast_tac 1);
   4.117 -result();
   4.118 -
   4.119 -(*16*)
   4.120 -Goal "(P-->Q) | (Q-->P)";
   4.121 -by (Blast_tac 1);
   4.122 -result();
   4.123 -
   4.124 -(*17*)
   4.125 -Goal "((P & (Q-->R))-->S)  =  ((~P | Q | S) & (~P | ~R | S))";
   4.126 -by (Blast_tac 1);
   4.127 -result();
   4.128 -
   4.129 -writeln"Classical Logic: examples with quantifiers";
   4.130 -
   4.131 -Goal "(! x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))";
   4.132 -by (Blast_tac 1);
   4.133 -result(); 
   4.134 -
   4.135 -Goal "(? x. P-->Q(x))  =  (P --> (? x. Q(x)))";
   4.136 -by (Blast_tac 1);
   4.137 -result(); 
   4.138 -
   4.139 -Goal "(? x. P(x)-->Q) = ((! x. P(x)) --> Q)";
   4.140 -by (Blast_tac 1);
   4.141 -result(); 
   4.142 -
   4.143 -Goal "((! x. P(x)) | Q)  =  (! x. P(x) | Q)";
   4.144 -by (Blast_tac 1);
   4.145 -result(); 
   4.146 -
   4.147 -(*From Wishnu Prasetya*)
   4.148 -Goal "(!s. q(s) --> r(s)) & ~r(s) & (!s. ~r(s) & ~q(s) --> p(t) | q(t)) \
   4.149 -\   --> p(t) | r(t)";
   4.150 -by (Blast_tac 1);
   4.151 -result(); 
   4.152 -
   4.153 -
   4.154 -writeln"Problems requiring quantifier duplication";
   4.155 -
   4.156 -(*Theorem B of Peter Andrews, Theorem Proving via General Matings, 
   4.157 -  JACM 28 (1981).*)
   4.158 -Goal "(EX x. ALL y. P(x) = P(y)) --> ((EX x. P(x)) = (ALL y. P(y)))";
   4.159 -by (Blast_tac 1);
   4.160 -result();
   4.161 -
   4.162 -(*Needs multiple instantiation of the quantifier.*)
   4.163 -Goal "(! x. P(x)-->P(f(x)))  &  P(d)-->P(f(f(f(d))))";
   4.164 -by (Blast_tac 1);
   4.165 -result();
   4.166 -
   4.167 -(*Needs double instantiation of the quantifier*)
   4.168 -Goal "? x. P(x) --> P(a) & P(b)";
   4.169 -by (Blast_tac 1);
   4.170 -result();
   4.171 -
   4.172 -Goal "? z. P(z) --> (! x. P(x))";
   4.173 -by (Blast_tac 1);
   4.174 -result();
   4.175 -
   4.176 -Goal "? x. (? y. P(y)) --> P(x)";
   4.177 -by (Blast_tac 1);
   4.178 -result();
   4.179 -
   4.180 -writeln"Hard examples with quantifiers";
   4.181 -
   4.182 -writeln"Problem 18";
   4.183 -Goal "? y. ! x. P(y)-->P(x)";
   4.184 -by (Blast_tac 1);
   4.185 -result(); 
   4.186 -
   4.187 -writeln"Problem 19";
   4.188 -Goal "? x. ! y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))";
   4.189 -by (Blast_tac 1);
   4.190 -result();
   4.191 -
   4.192 -writeln"Problem 20";
   4.193 -Goal "(! x y. ? z. ! w. (P(x)&Q(y)-->R(z)&S(w)))     \
   4.194 -\   --> (? x y. P(x) & Q(y)) --> (? z. R(z))";
   4.195 -by (Blast_tac 1); 
   4.196 -result();
   4.197 -
   4.198 -writeln"Problem 21";
   4.199 -Goal "(? x. P-->Q(x)) & (? x. Q(x)-->P) --> (? x. P=Q(x))";
   4.200 -by (Blast_tac 1); 
   4.201 -result();
   4.202 -
   4.203 -writeln"Problem 22";
   4.204 -Goal "(! x. P = Q(x))  -->  (P = (! x. Q(x)))";
   4.205 -by (Blast_tac 1); 
   4.206 -result();
   4.207 -
   4.208 -writeln"Problem 23";
   4.209 -Goal "(! x. P | Q(x))  =  (P | (! x. Q(x)))";
   4.210 -by (Blast_tac 1);  
   4.211 -result();
   4.212 -
   4.213 -writeln"Problem 24";
   4.214 -Goal "~(? x. S(x)&Q(x)) & (! x. P(x) --> Q(x)|R(x)) &  \
   4.215 -\    (~(? x. P(x)) --> (? x. Q(x))) & (! x. Q(x)|R(x) --> S(x))  \
   4.216 -\   --> (? x. P(x)&R(x))";
   4.217 -by (Blast_tac 1); 
   4.218 -result();
   4.219 -
   4.220 -writeln"Problem 25";
   4.221 -Goal "(? x. P(x)) &  \
   4.222 -\       (! x. L(x) --> ~ (M(x) & R(x))) &  \
   4.223 -\       (! x. P(x) --> (M(x) & L(x))) &   \
   4.224 -\       ((! x. P(x)-->Q(x)) | (? x. P(x)&R(x)))  \
   4.225 -\   --> (? x. Q(x)&P(x))";
   4.226 -by (Blast_tac 1); 
   4.227 -result();
   4.228 -
   4.229 -writeln"Problem 26";
   4.230 -Goal "((? x. p(x)) = (? x. q(x))) &     \
   4.231 -\     (! x. ! y. p(x) & q(y) --> (r(x) = s(y))) \
   4.232 -\ --> ((! x. p(x)-->r(x)) = (! x. q(x)-->s(x)))";
   4.233 -by (Blast_tac 1);
   4.234 -result();
   4.235 -
   4.236 -writeln"Problem 27";
   4.237 -Goal "(? x. P(x) & ~Q(x)) &   \
   4.238 -\             (! x. P(x) --> R(x)) &   \
   4.239 -\             (! x. M(x) & L(x) --> P(x)) &   \
   4.240 -\             ((? x. R(x) & ~ Q(x)) --> (! x. L(x) --> ~ R(x)))  \
   4.241 -\         --> (! x. M(x) --> ~L(x))";
   4.242 -by (Blast_tac 1); 
   4.243 -result();
   4.244 -
   4.245 -writeln"Problem 28.  AMENDED";
   4.246 -Goal "(! x. P(x) --> (! x. Q(x))) &   \
   4.247 -\       ((! x. Q(x)|R(x)) --> (? x. Q(x)&S(x))) &  \
   4.248 -\       ((? x. S(x)) --> (! x. L(x) --> M(x)))  \
   4.249 -\   --> (! x. P(x) & L(x) --> M(x))";
   4.250 -by (Blast_tac 1);  
   4.251 -result();
   4.252 -
   4.253 -writeln"Problem 29.  Essentially the same as Principia Mathematica *11.71";
   4.254 -Goal "(? x. F(x)) & (? y. G(y))  \
   4.255 -\   --> ( ((! x. F(x)-->H(x)) & (! y. G(y)-->J(y)))  =   \
   4.256 -\         (! x y. F(x) & G(y) --> H(x) & J(y)))";
   4.257 -by (Blast_tac 1); 
   4.258 -result();
   4.259 -
   4.260 -writeln"Problem 30";
   4.261 -Goal "(! x. P(x) | Q(x) --> ~ R(x)) & \
   4.262 -\       (! x. (Q(x) --> ~ S(x)) --> P(x) & R(x))  \
   4.263 -\   --> (! x. S(x))";
   4.264 -by (Blast_tac 1);  
   4.265 -result();
   4.266 -
   4.267 -writeln"Problem 31";
   4.268 -Goal "~(? x. P(x) & (Q(x) | R(x))) & \
   4.269 -\       (? x. L(x) & P(x)) & \
   4.270 -\       (! x. ~ R(x) --> M(x))  \
   4.271 -\   --> (? x. L(x) & M(x))";
   4.272 -by (Blast_tac 1);
   4.273 -result();
   4.274 -
   4.275 -writeln"Problem 32";
   4.276 -Goal "(! x. P(x) & (Q(x)|R(x))-->S(x)) & \
   4.277 -\       (! x. S(x) & R(x) --> L(x)) & \
   4.278 -\       (! x. M(x) --> R(x))  \
   4.279 -\   --> (! x. P(x) & M(x) --> L(x))";
   4.280 -by (Blast_tac 1);
   4.281 -result();
   4.282 -
   4.283 -writeln"Problem 33";
   4.284 -Goal "(! x. P(a) & (P(x)-->P(b))-->P(c))  =    \
   4.285 -\    (! x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))";
   4.286 -by (Blast_tac 1);
   4.287 -result();
   4.288 -
   4.289 -writeln"Problem 34  AMENDED (TWICE!!)";
   4.290 -(*Andrews's challenge*)
   4.291 -Goal "((? x. ! y. p(x) = p(y))  =               \
   4.292 -\              ((? x. q(x)) = (! y. p(y))))   =    \
   4.293 -\             ((? x. ! y. q(x) = q(y))  =          \
   4.294 -\              ((? x. p(x)) = (! y. q(y))))";
   4.295 -by (Blast_tac 1);
   4.296 -result();
   4.297 -
   4.298 -writeln"Problem 35";
   4.299 -Goal "? x y. P x y -->  (! u v. P u v)";
   4.300 -by (Blast_tac 1);
   4.301 -result();
   4.302 -
   4.303 -writeln"Problem 36";
   4.304 -Goal "(! x. ? y. J x y) & \
   4.305 -\       (! x. ? y. G x y) & \
   4.306 -\       (! x y. J x y | G x y -->       \
   4.307 -\       (! z. J y z | G y z --> H x z))   \
   4.308 -\   --> (! x. ? y. H x y)";
   4.309 -by (Blast_tac 1);
   4.310 -result();
   4.311 -
   4.312 -writeln"Problem 37";
   4.313 -Goal "(! z. ? w. ! x. ? y. \
   4.314 -\          (P x z -->P y w) & P y z & (P y w --> (? u. Q u w))) & \
   4.315 -\       (! x z. ~(P x z) --> (? y. Q y z)) & \
   4.316 -\       ((? x y. Q x y) --> (! x. R x x))  \
   4.317 -\   --> (! x. ? y. R x y)";
   4.318 -by (Blast_tac 1);
   4.319 -result();
   4.320 -
   4.321 -writeln"Problem 38";
   4.322 -Goal "(! x. p(a) & (p(x) --> (? y. p(y) & r x y)) -->            \
   4.323 -\          (? z. ? w. p(z) & r x w & r w z))  =                 \
   4.324 -\    (! x. (~p(a) | p(x) | (? z. ? w. p(z) & r x w & r w z)) &  \
   4.325 -\          (~p(a) | ~(? y. p(y) & r x y) |                      \
   4.326 -\           (? z. ? w. p(z) & r x w & r w z)))";
   4.327 -by (Blast_tac 1);  (*beats fast_tac!*)
   4.328 -result();
   4.329 -
   4.330 -writeln"Problem 39";
   4.331 -Goal "~ (? x. ! y. F y x = (~ F y y))";
   4.332 -by (Blast_tac 1);
   4.333 -result();
   4.334 -
   4.335 -writeln"Problem 40.  AMENDED";
   4.336 -Goal "(? y. ! x. F x y = F x x)  \
   4.337 -\       -->  ~ (! x. ? y. ! z. F z y = (~ F z x))";
   4.338 -by (Blast_tac 1);
   4.339 -result();
   4.340 -
   4.341 -writeln"Problem 41";
   4.342 -Goal "(! z. ? y. ! x. f x y = (f x z & ~ f x x))        \
   4.343 -\              --> ~ (? z. ! x. f x z)";
   4.344 -by (Blast_tac 1);
   4.345 -result();
   4.346 -
   4.347 -writeln"Problem 42";
   4.348 -Goal "~ (? y. ! x. p x y = (~ (? z. p x z & p z x)))";
   4.349 -by (Blast_tac 1);
   4.350 -result();
   4.351 -
   4.352 -writeln"Problem 43!!";
   4.353 -Goal "(! x::'a. ! y::'a. q x y = (! z. p z x = (p z y::bool)))   \
   4.354 -\ --> (! x. (! y. q x y = (q y x::bool)))";
   4.355 -by (Blast_tac 1);
   4.356 -result();
   4.357 -
   4.358 -writeln"Problem 44";
   4.359 -Goal "(! x. f(x) -->                                    \
   4.360 -\             (? y. g(y) & h x y & (? y. g(y) & ~ h x y)))  &   \
   4.361 -\             (? x. j(x) & (! y. g(y) --> h x y))               \
   4.362 -\             --> (? x. j(x) & ~f(x))";
   4.363 -by (Blast_tac 1);
   4.364 -result();
   4.365 -
   4.366 -writeln"Problem 45";
   4.367 -Goal "(! x. f(x) & (! y. g(y) & h x y --> j x y) \
   4.368 -\                     --> (! y. g(y) & h x y --> k(y))) &       \
   4.369 -\    ~ (? y. l(y) & k(y)) &                                     \
   4.370 -\    (? x. f(x) & (! y. h x y --> l(y))                         \
   4.371 -\               & (! y. g(y) & h x y --> j x y))                \
   4.372 -\     --> (? x. f(x) & ~ (? y. g(y) & h x y))";
   4.373 -by (Blast_tac 1); 
   4.374 -result();
   4.375 -
   4.376 -
   4.377 -writeln"Problems (mainly) involving equality or functions";
   4.378 -
   4.379 -writeln"Problem 48";
   4.380 -Goal "(a=b | c=d) & (a=c | b=d) --> a=d | b=c";
   4.381 -by (Blast_tac 1);
   4.382 -result();
   4.383 -
   4.384 -writeln"Problem 49  NOT PROVED AUTOMATICALLY";
   4.385 -(*Hard because it involves substitution for Vars;
   4.386 -  the type constraint ensures that x,y,z have the same type as a,b,u. *)
   4.387 -Goal "(? x y::'a. ! z. z=x | z=y) & P(a) & P(b) & (~a=b) \
   4.388 -\               --> (! u::'a. P(u))";
   4.389 -by (Classical.Safe_tac);
   4.390 -by (res_inst_tac [("x","a")] allE 1);
   4.391 -by (assume_tac 1);
   4.392 -by (res_inst_tac [("x","b")] allE 1);
   4.393 -by (assume_tac 1);
   4.394 -by (Fast_tac 1);    (*Blast_tac's treatment of equality can't do it*)
   4.395 -result();
   4.396 -
   4.397 -writeln"Problem 50";  
   4.398 -(*What has this to do with equality?*)
   4.399 -Goal "(! x. P a x | (! y. P x y)) --> (? x. ! y. P x y)";
   4.400 -by (Blast_tac 1);
   4.401 -result();
   4.402 -
   4.403 -writeln"Problem 51";
   4.404 -Goal "(? z w. ! x y. P x y = (x=z & y=w)) -->  \
   4.405 -\    (? z. ! x. ? w. (! y. P x y = (y=w)) = (x=z))";
   4.406 -by (Blast_tac 1);
   4.407 -result();
   4.408 -
   4.409 -writeln"Problem 52";
   4.410 -(*Almost the same as 51. *)
   4.411 -Goal "(? z w. ! x y. P x y = (x=z & y=w)) -->  \
   4.412 -\    (? w. ! y. ? z. (! x. P x y = (x=z)) = (y=w))";
   4.413 -by (Blast_tac 1);
   4.414 -result();
   4.415 -
   4.416 -writeln"Problem 55";
   4.417 -
   4.418 -(*Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988).
   4.419 -  fast_tac DISCOVERS who killed Agatha. *)
   4.420 -Goal "lives(agatha) & lives(butler) & lives(charles) & \
   4.421 -\  (killed agatha agatha | killed butler agatha | killed charles agatha) & \
   4.422 -\  (!x y. killed x y --> hates x y & ~richer x y) & \
   4.423 -\  (!x. hates agatha x --> ~hates charles x) & \
   4.424 -\  (hates agatha agatha & hates agatha charles) & \
   4.425 -\  (!x. lives(x) & ~richer x agatha --> hates butler x) & \
   4.426 -\  (!x. hates agatha x --> hates butler x) & \
   4.427 -\  (!x. ~hates x agatha | ~hates x butler | ~hates x charles) --> \
   4.428 -\   killed ?who agatha";
   4.429 -by (Fast_tac 1);
   4.430 -result();
   4.431 -
   4.432 -writeln"Problem 56";
   4.433 -Goal "(! x. (? y. P(y) & x=f(y)) --> P(x)) = (! x. P(x) --> P(f(x)))";
   4.434 -by (Blast_tac 1);
   4.435 -result();
   4.436 -
   4.437 -writeln"Problem 57";
   4.438 -Goal "P (f a b) (f b c) & P (f b c) (f a c) & \
   4.439 -\    (! x y z. P x y & P y z --> P x z)    -->   P (f a b) (f a c)";
   4.440 -by (Blast_tac 1);
   4.441 -result();
   4.442 -
   4.443 -writeln"Problem 58  NOT PROVED AUTOMATICALLY";
   4.444 -Goal "(! x y. f(x)=g(y)) --> (! x y. f(f(x))=f(g(y)))";
   4.445 -val f_cong = read_instantiate [("f","f")] arg_cong;
   4.446 -by (fast_tac (claset() addIs [f_cong]) 1);
   4.447 -result();
   4.448 -
   4.449 -writeln"Problem 59";
   4.450 -Goal "(! x. P(x) = (~P(f(x)))) --> (? x. P(x) & ~P(f(x)))";
   4.451 -by (Blast_tac 1);
   4.452 -result();
   4.453 -
   4.454 -writeln"Problem 60";
   4.455 -Goal "! x. P x (f x) = (? y. (! z. P z y --> P z (f x)) & P x y)";
   4.456 -by (Blast_tac 1);
   4.457 -result();
   4.458 -
   4.459 -writeln"Problem 62 as corrected in JAR 18 (1997), page 135";
   4.460 -Goal "(ALL x. p a & (p x --> p(f x)) --> p(f(f x)))  =   \
   4.461 -\     (ALL x. (~ p a | p x | p(f(f x))) &                        \
   4.462 -\             (~ p a | ~ p(f x) | p(f(f x))))";
   4.463 -by (Blast_tac 1);
   4.464 -result();
   4.465 -
   4.466 -(*From Davis, Obvious Logical Inferences, IJCAI-81, 530-531
   4.467 -  Fast_tac indeed copes!*)
   4.468 -goal (theory "Product_Type") 
   4.469 -             "(ALL x. F(x) & ~G(x) --> (EX y. H(x,y) & J(y))) & \
   4.470 -\             (EX x. K(x) & F(x) & (ALL y. H(x,y) --> K(y))) &   \
   4.471 -\             (ALL x. K(x) --> ~G(x))  -->  (EX x. K(x) & J(x))";
   4.472 -by (Fast_tac 1);
   4.473 -result();
   4.474 -
   4.475 -(*From Rudnicki, Obvious Inferences, JAR 3 (1987), 383-393.  
   4.476 -  It does seem obvious!*)
   4.477 -goal (theory "Product_Type")
   4.478 -    "(ALL x. F(x) & ~G(x) --> (EX y. H(x,y) & J(y))) &        \
   4.479 -\    (EX x. K(x) & F(x) & (ALL y. H(x,y) --> K(y)))  &        \
   4.480 -\    (ALL x. K(x) --> ~G(x))   -->   (EX x. K(x) --> ~G(x))";
   4.481 -by (Fast_tac 1);
   4.482 -result();
   4.483 -
   4.484 -(*Attributed to Lewis Carroll by S. G. Pulman.  The first or last assumption
   4.485 -can be deleted.*)
   4.486 -Goal "(ALL x. honest(x) & industrious(x) --> healthy(x)) & \
   4.487 -\     ~ (EX x. grocer(x) & healthy(x)) & \
   4.488 -\     (ALL x. industrious(x) & grocer(x) --> honest(x)) & \
   4.489 -\     (ALL x. cyclist(x) --> industrious(x)) & \
   4.490 -\     (ALL x. ~healthy(x) & cyclist(x) --> ~honest(x))  \
   4.491 -\     --> (ALL x. grocer(x) --> ~cyclist(x))";
   4.492 -by (Blast_tac 1);
   4.493 -result();
   4.494 -
   4.495 -goal (theory "Product_Type")
   4.496 -    "(ALL x y. R(x,y) | R(y,x)) &                \
   4.497 -\    (ALL x y. S(x,y) & S(y,x) --> x=y) &        \
   4.498 -\    (ALL x y. R(x,y) --> S(x,y))    -->   (ALL x y. S(x,y) --> R(x,y))";
   4.499 -by (Blast_tac 1);
   4.500 -result();
   4.501 -
   4.502 -
   4.503 -
   4.504 -writeln"Reached end of file.";
     5.1 --- a/src/HOL/ex/mesontest.ML	Fri Oct 03 12:36:16 2003 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,615 +0,0 @@
     5.4 -(*  Title:      HOL/ex/mesontest
     5.5 -    ID:         $Id$
     5.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.7 -    Copyright   1992  University of Cambridge
     5.8 -
     5.9 -Test data for the MESON proof procedure
    5.10 -   (Excludes the equality problems 51, 52, 56, 58)
    5.11 -
    5.12 -Use the "mesonlog" shell script to process logs.
    5.13 -
    5.14 -show_hyps := false;
    5.15 -
    5.16 -proofs := 0;
    5.17 -by (rtac ccontr 1);
    5.18 -val [prem] = gethyps 1;
    5.19 -val nnf = make_nnf prem;
    5.20 -val xsko = skolemize nnf;
    5.21 -by (cut_facts_tac [xsko] 1 THEN REPEAT (etac exE 1));
    5.22 -val [_,sko] = gethyps 1;
    5.23 -val clauses = make_clauses [sko];       
    5.24 -val horns = make_horns clauses;
    5.25 -val goes = gocls clauses;
    5.26 -
    5.27 -Goal "False";
    5.28 -by (resolve_tac goes 1);
    5.29 -proofs := 2;
    5.30 -
    5.31 -by (prolog_step_tac horns 1);
    5.32 -by (iter_deepen_prolog_tac horns);
    5.33 -by (depth_prolog_tac horns);
    5.34 -by (best_prolog_tac size_of_subgoals horns);
    5.35 -*)
    5.36 -
    5.37 -writeln"File HOL/ex/meson-test.";
    5.38 -
    5.39 -context Main.thy;
    5.40 -
    5.41 -(*Deep unifications can be required, esp. during transformation to clauses*)
    5.42 -val orig_trace_bound = !Unify.trace_bound
    5.43 -and orig_search_bound = !Unify.search_bound;
    5.44 -Unify.trace_bound := 20;
    5.45 -Unify.search_bound := 40;
    5.46 -
    5.47 -(**** Interactive examples ****)
    5.48 -
    5.49 -(*Generate nice names for Skolem functions*)
    5.50 -Logic.auto_rename := true; Logic.set_rename_prefix "a";
    5.51 -
    5.52 -
    5.53 -writeln"Problem 25";
    5.54 -Goal "(\\<exists>x. P x) &  \
    5.55 -\     (\\<forall>x. L x --> ~ (M x & R x)) &  \
    5.56 -\     (\\<forall>x. P x --> (M x & L x)) &   \
    5.57 -\     ((\\<forall>x. P x --> Q x) | (\\<exists>x. P x & R x))  \
    5.58 -\   --> (\\<exists>x. Q x & P x)";
    5.59 -by (rtac ccontr 1);
    5.60 -val [prem25] = gethyps 1;
    5.61 -val nnf25 = make_nnf prem25;
    5.62 -val xsko25 = skolemize nnf25;
    5.63 -by (cut_facts_tac [xsko25] 1 THEN REPEAT (etac exE 1));
    5.64 -val [_,sko25] = gethyps 1;
    5.65 -val clauses25 = make_clauses [sko25];   (*7 clauses*)
    5.66 -val horns25 = make_horns clauses25;     (*16 Horn clauses*)
    5.67 -val go25::_ = gocls clauses25;
    5.68 -
    5.69 -Goal "False";
    5.70 -by (rtac go25 1);
    5.71 -by (depth_prolog_tac horns25);
    5.72 -
    5.73 -
    5.74 -writeln"Problem 26";
    5.75 -Goal "((\\<exists>x. p x) = (\\<exists>x. q x)) &     \
    5.76 -\     (\\<forall>x. \\<forall>y. p x & q y --> (r x = s y)) \
    5.77 -\ --> ((\\<forall>x. p x --> r x) = (\\<forall>x. q x --> s x))";
    5.78 -by (rtac ccontr 1);
    5.79 -val [prem26] = gethyps 1;
    5.80 -val nnf26 = make_nnf prem26;
    5.81 -val xsko26 = skolemize nnf26;
    5.82 -by (cut_facts_tac [xsko26] 1 THEN REPEAT (etac exE 1));
    5.83 -val [_,sko26] = gethyps 1;
    5.84 -val clauses26 = make_clauses [sko26];                   (*9 clauses*)
    5.85 -val horns26 = make_horns clauses26;                     (*24 Horn clauses*)
    5.86 -val go26::_ = gocls clauses26;
    5.87 -
    5.88 -Goal "False";
    5.89 -by (rtac go26 1);
    5.90 -by (depth_prolog_tac horns26);  (*1.4 secs*)
    5.91 -(*Proof is of length 107!!*)
    5.92 -
    5.93 -
    5.94 -writeln"Problem 43  NOW PROVED AUTOMATICALLY!!";  (*16 Horn clauses*)
    5.95 -Goal "(\\<forall>x. \\<forall>y. q x y = (\\<forall>z. p z x = (p z y::bool)))  \
    5.96 -\     --> (\\<forall>x. (\\<forall>y. q x y = (q y x::bool)))";
    5.97 -by (rtac ccontr 1);
    5.98 -val [prem43] = gethyps 1;
    5.99 -val nnf43 = make_nnf prem43;
   5.100 -val xsko43 = skolemize nnf43;
   5.101 -by (cut_facts_tac [xsko43] 1 THEN REPEAT (etac exE 1));
   5.102 -val [_,sko43] = gethyps 1;
   5.103 -val clauses43 = make_clauses [sko43];   (*6*)
   5.104 -val horns43 = make_horns clauses43;     (*16*)
   5.105 -val go43::_ = gocls clauses43;
   5.106 -
   5.107 -Goal "False";
   5.108 -by (rtac go43 1);
   5.109 -by (best_prolog_tac size_of_subgoals horns43);   (*1.6 secs*)
   5.110 -
   5.111 -(* 
   5.112 -#1  (q x xa ==> ~ q x xa) ==> q xa x
   5.113 -#2  (q xa x ==> ~ q xa x) ==> q x xa
   5.114 -#3  (~ q x xa ==> q x xa) ==> ~ q xa x
   5.115 -#4  (~ q xa x ==> q xa x) ==> ~ q x xa
   5.116 -#5  [| ~ q ?U ?V ==> q ?U ?V; ~ p ?W ?U ==> p ?W ?U |] ==> p ?W ?V
   5.117 -#6  [| ~ p ?W ?U ==> p ?W ?U; p ?W ?V ==> ~ p ?W ?V |] ==> ~ q ?U ?V
   5.118 -#7  [| p ?W ?V ==> ~ p ?W ?V; ~ q ?U ?V ==> q ?U ?V |] ==> ~ p ?W ?U
   5.119 -#8  [| ~ q ?U ?V ==> q ?U ?V; ~ p ?W ?V ==> p ?W ?V |] ==> p ?W ?U
   5.120 -#9  [| ~ p ?W ?V ==> p ?W ?V; p ?W ?U ==> ~ p ?W ?U |] ==> ~ q ?U ?V
   5.121 -#10 [| p ?W ?U ==> ~ p ?W ?U; ~ q ?U ?V ==> q ?U ?V |] ==> ~ p ?W ?V
   5.122 -#11 [| p (xb ?U ?V) ?U ==> ~ p (xb ?U ?V) ?U;
   5.123 -       p (xb ?U ?V) ?V ==> ~ p (xb ?U ?V) ?V |] ==> q ?U ?V
   5.124 -#12 [| p (xb ?U ?V) ?V ==> ~ p (xb ?U ?V) ?V; q ?U ?V ==> ~ q ?U ?V |] ==>
   5.125 -    p (xb ?U ?V) ?U
   5.126 -#13 [| q ?U ?V ==> ~ q ?U ?V; p (xb ?U ?V) ?U ==> ~ p (xb ?U ?V) ?U |] ==>
   5.127 -    p (xb ?U ?V) ?V
   5.128 -#14 [| ~ p (xb ?U ?V) ?U ==> p (xb ?U ?V) ?U;
   5.129 -       ~ p (xb ?U ?V) ?V ==> p (xb ?U ?V) ?V |] ==> q ?U ?V
   5.130 -#15 [| ~ p (xb ?U ?V) ?V ==> p (xb ?U ?V) ?V; q ?U ?V ==> ~ q ?U ?V |] ==>
   5.131 -    ~ p (xb ?U ?V) ?U
   5.132 -#16 [| q ?U ?V ==> ~ q ?U ?V; ~ p (xb ?U ?V) ?U ==> p (xb ?U ?V) ?U |] ==>
   5.133 -    ~ p (xb ?U ?V) ?V
   5.134 -
   5.135 -And here is the proof\\<forall> (Unkn is the start state after use of goal clause)
   5.136 -[Unkn, Res ([Thm "#14"], false, 1), Res ([Thm "#5"], false, 1),
   5.137 -   Res ([Thm "#1"], false, 1), Asm 1, Res ([Thm "#13"], false, 1), Asm 2,
   5.138 -   Asm 1, Res ([Thm "#13"], false, 1), Asm 1, Res ([Thm "#10"], false, 1),
   5.139 -   Res ([Thm "#16"], false, 1), Asm 2, Asm 1, Res ([Thm "#1"], false, 1),
   5.140 -   Asm 1, Res ([Thm "#14"], false, 1), Res ([Thm "#5"], false, 1),
   5.141 -   Res ([Thm "#2"], false, 1), Asm 1, Res ([Thm "#13"], false, 1), Asm 2,
   5.142 -   Asm 1, Res ([Thm "#8"], false, 1), Res ([Thm "#2"], false, 1), Asm 1,
   5.143 -   Res ([Thm "#12"], false, 1), Asm 2, Asm 1] : lderiv list
   5.144 -*)
   5.145 -
   5.146 -
   5.147 -(*Restore variable name preservation*)
   5.148 -Logic.auto_rename := false; 
   5.149 -
   5.150 -
   5.151 -(**** Batch test data ****)
   5.152 -
   5.153 -(*Sample problems from 
   5.154 -  F. J. Pelletier, 
   5.155 -  Seventy-Five Problems for Testing Automatic Theorem Provers,
   5.156 -  J. Automated Reasoning 2 (1986), 191-216.
   5.157 -  Errata, JAR 4 (1988), 236-236.
   5.158 -
   5.159 -The hardest problems -- judging by experience with several theorem provers,
   5.160 -including matrix ones -- are 34 and 43.
   5.161 -*)
   5.162 -
   5.163 -writeln"Pelletier's examples";
   5.164 -(*1*)
   5.165 -Goal "(P --> Q)  =  (~Q --> ~P)";
   5.166 -by (meson_tac 1);
   5.167 -result();
   5.168 -
   5.169 -(*2*)
   5.170 -Goal "(~ ~ P) =  P";
   5.171 -by (meson_tac 1);
   5.172 -result();
   5.173 -
   5.174 -(*3*)
   5.175 -Goal "~(P-->Q) --> (Q-->P)";
   5.176 -by (meson_tac 1);
   5.177 -result();
   5.178 -
   5.179 -(*4*)
   5.180 -Goal "(~P-->Q)  =  (~Q --> P)";
   5.181 -by (meson_tac 1);
   5.182 -result();
   5.183 -
   5.184 -(*5*)
   5.185 -Goal "((P|Q)-->(P|R)) --> (P|(Q-->R))";
   5.186 -by (meson_tac 1);
   5.187 -result();
   5.188 -
   5.189 -(*6*)
   5.190 -Goal "P | ~ P";
   5.191 -by (meson_tac 1);
   5.192 -result();
   5.193 -
   5.194 -(*7*)
   5.195 -Goal "P | ~ ~ ~ P";
   5.196 -by (meson_tac 1);
   5.197 -result();
   5.198 -
   5.199 -(*8.  Peirce's law*)
   5.200 -Goal "((P-->Q) --> P)  -->  P";
   5.201 -by (meson_tac 1);
   5.202 -result();
   5.203 -
   5.204 -(*9*)
   5.205 -Goal "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
   5.206 -by (meson_tac 1);
   5.207 -result();
   5.208 -
   5.209 -(*10*)
   5.210 -Goal "(Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P=Q)";
   5.211 -by (meson_tac 1);
   5.212 -result();
   5.213 -
   5.214 -(*11.  Proved in each direction (incorrectly, says Pelletier!!)  *)
   5.215 -Goal "P=(P::bool)";
   5.216 -by (meson_tac 1);
   5.217 -result();
   5.218 -
   5.219 -(*12.  "Dijkstra's law"*)
   5.220 -Goal "((P = Q) = R) = (P = (Q = R))";
   5.221 -by (meson_tac 1);
   5.222 -result();
   5.223 -
   5.224 -(*13.  Distributive law*)
   5.225 -Goal "(P | (Q & R)) = ((P | Q) & (P | R))";
   5.226 -by (meson_tac 1);
   5.227 -result();
   5.228 -
   5.229 -(*14*)
   5.230 -Goal "(P = Q) = ((Q | ~P) & (~Q|P))";
   5.231 -by (meson_tac 1);
   5.232 -result();
   5.233 -
   5.234 -(*15*)
   5.235 -Goal "(P --> Q) = (~P | Q)";
   5.236 -by (meson_tac 1);
   5.237 -result();
   5.238 -
   5.239 -(*16*)
   5.240 -Goal "(P-->Q) | (Q-->P)";
   5.241 -by (meson_tac 1);
   5.242 -result();
   5.243 -
   5.244 -(*17*)
   5.245 -Goal "((P & (Q-->R))-->S)  =  ((~P | Q | S) & (~P | ~R | S))";
   5.246 -by (meson_tac 1);
   5.247 -result();
   5.248 -
   5.249 -writeln"Classical Logic: examples with quantifiers";
   5.250 -
   5.251 -Goal "(\\<forall>x. P x & Q x) = ((\\<forall>x. P x) & (\\<forall>x. Q x))";
   5.252 -by (meson_tac 1);
   5.253 -result(); 
   5.254 -
   5.255 -Goal "(\\<exists>x. P --> Q x)  =  (P --> (\\<exists>x. Q x))";
   5.256 -by (meson_tac 1);
   5.257 -result(); 
   5.258 -
   5.259 -Goal "(\\<exists>x. P x --> Q) = ((\\<forall>x. P x) --> Q)";
   5.260 -by (meson_tac 1);
   5.261 -result(); 
   5.262 -
   5.263 -Goal "((\\<forall>x. P x) | Q)  =  (\\<forall>x. P x | Q)";
   5.264 -by (meson_tac 1);
   5.265 -result(); 
   5.266 -
   5.267 -Goal "(\\<forall>x. P x --> P(f x))  &  P d --> P(f(f(f d)))";
   5.268 -by (meson_tac 1);
   5.269 -result();
   5.270 -
   5.271 -(*Needs double instantiation of EXISTS*)
   5.272 -Goal "\\<exists>x. P x --> P a & P b";
   5.273 -by (meson_tac 1);
   5.274 -result();
   5.275 -
   5.276 -Goal "\\<exists>z. P z --> (\\<forall>x. P x)";
   5.277 -by (meson_tac 1);
   5.278 -result();
   5.279 -
   5.280 -writeln"Hard examples with quantifiers";
   5.281 -
   5.282 -writeln"Problem 18";
   5.283 -Goal "\\<exists>y. \\<forall>x. P y --> P x";
   5.284 -by (meson_tac 1);
   5.285 -result(); 
   5.286 -
   5.287 -writeln"Problem 19";
   5.288 -Goal "\\<exists>x. \\<forall>y z. (P y --> Q z) --> (P x --> Q x)";
   5.289 -by (meson_tac 1);
   5.290 -result();
   5.291 -
   5.292 -writeln"Problem 20";
   5.293 -Goal "(\\<forall>x y. \\<exists>z. \\<forall>w. (P x & Q y --> R z & S w))     \
   5.294 -\   --> (\\<exists>x y. P x & Q y) --> (\\<exists>z. R z)";
   5.295 -by (meson_tac 1); 
   5.296 -result();
   5.297 -
   5.298 -writeln"Problem 21";
   5.299 -Goal "(\\<exists>x. P --> Q x) & (\\<exists>x. Q x --> P) --> (\\<exists>x. P=Q x)";
   5.300 -by (meson_tac 1); 
   5.301 -result();
   5.302 -
   5.303 -writeln"Problem 22";
   5.304 -Goal "(\\<forall>x. P = Q x)  -->  (P = (\\<forall>x. Q x))";
   5.305 -by (meson_tac 1); 
   5.306 -result();
   5.307 -
   5.308 -writeln"Problem 23";
   5.309 -Goal "(\\<forall>x. P | Q x)  =  (P | (\\<forall>x. Q x))";
   5.310 -by (meson_tac 1);  
   5.311 -result();
   5.312 -
   5.313 -writeln"Problem 24";  (*The first goal clause is useless*)
   5.314 -Goal "~(\\<exists>x. S x & Q x) & (\\<forall>x. P x --> Q x | R x) &  \
   5.315 -\     (~(\\<exists>x. P x) --> (\\<exists>x. Q x)) & (\\<forall>x. Q x | R x --> S x)  \
   5.316 -\   --> (\\<exists>x. P x & R x)";
   5.317 -by (meson_tac 1); 
   5.318 -result();
   5.319 -
   5.320 -writeln"Problem 25";
   5.321 -Goal "(\\<exists>x. P x) &  \
   5.322 -\     (\\<forall>x. L x --> ~ (M x & R x)) &  \
   5.323 -\     (\\<forall>x. P x --> (M x & L x)) &   \
   5.324 -\     ((\\<forall>x. P x --> Q x) | (\\<exists>x. P x & R x))  \
   5.325 -\   --> (\\<exists>x. Q x & P x)";
   5.326 -by (meson_tac 1); 
   5.327 -result();
   5.328 -
   5.329 -writeln"Problem 26";  (*24 Horn clauses*)
   5.330 -Goal "((\\<exists>x. p x) = (\\<exists>x. q x)) &     \
   5.331 -\     (\\<forall>x. \\<forall>y. p x & q y --> (r x = s y)) \
   5.332 -\ --> ((\\<forall>x. p x --> r x) = (\\<forall>x. q x --> s x))";
   5.333 -by (meson_tac 1); 
   5.334 -result();
   5.335 -
   5.336 -writeln"Problem 27";    (*13 Horn clauses*)
   5.337 -Goal "(\\<exists>x. P x & ~Q x) &   \
   5.338 -\     (\\<forall>x. P x --> R x) &   \
   5.339 -\     (\\<forall>x. M x & L x --> P x) &   \
   5.340 -\     ((\\<exists>x. R x & ~ Q x) --> (\\<forall>x. L x --> ~ R x))  \
   5.341 -\     --> (\\<forall>x. M x --> ~L x)";
   5.342 -by (meson_tac 1); 
   5.343 -result();
   5.344 -
   5.345 -writeln"Problem 28.  AMENDED";  (*14 Horn clauses*)
   5.346 -Goal "(\\<forall>x. P x --> (\\<forall>x. Q x)) &   \
   5.347 -\     ((\\<forall>x. Q x | R x) --> (\\<exists>x. Q x & S x)) &  \
   5.348 -\     ((\\<exists>x. S x) --> (\\<forall>x. L x --> M x))  \
   5.349 -\   --> (\\<forall>x. P x & L x --> M x)";
   5.350 -by (meson_tac 1);  
   5.351 -result();
   5.352 -
   5.353 -writeln"Problem 29.  Essentially the same as Principia Mathematica *11.71";
   5.354 -        (*62 Horn clauses*)
   5.355 -Goal "(\\<exists>x. F x) & (\\<exists>y. G y)  \
   5.356 -\   --> ( ((\\<forall>x. F x --> H x) & (\\<forall>y. G y --> J y))  =   \
   5.357 -\         (\\<forall>x y. F x & G y --> H x & J y))";
   5.358 -by (meson_tac 1);          (*0.7 secs*)
   5.359 -result();
   5.360 -
   5.361 -writeln"Problem 30";
   5.362 -Goal "(\\<forall>x. P x | Q x --> ~ R x) & \
   5.363 -\     (\\<forall>x. (Q x --> ~ S x) --> P x & R x)  \
   5.364 -\   --> (\\<forall>x. S x)";
   5.365 -by (meson_tac 1);  
   5.366 -result();
   5.367 -
   5.368 -writeln"Problem 31";  (*10 Horn clauses; first negative clauses is useless*)
   5.369 -Goal "~(\\<exists>x. P x & (Q x | R x)) & \
   5.370 -\     (\\<exists>x. L x & P x) & \
   5.371 -\     (\\<forall>x. ~ R x --> M x)  \
   5.372 -\   --> (\\<exists>x. L x & M x)";
   5.373 -by (meson_tac 1);
   5.374 -result();
   5.375 -
   5.376 -writeln"Problem 32";
   5.377 -Goal "(\\<forall>x. P x & (Q x | R x)-->S x) & \
   5.378 -\     (\\<forall>x. S x & R x --> L x) & \
   5.379 -\     (\\<forall>x. M x --> R x)  \
   5.380 -\   --> (\\<forall>x. P x & M x --> L x)";
   5.381 -by (meson_tac 1);
   5.382 -result();
   5.383 -
   5.384 -writeln"Problem 33";  (*55 Horn clauses*)
   5.385 -Goal "(\\<forall>x. P a & (P x --> P b)-->P c)  =    \
   5.386 -\     (\\<forall>x. (~P a | P x | P c) & (~P a | ~P b | P c))";
   5.387 -by (meson_tac 1);          (*5.6 secs*)
   5.388 -result();
   5.389 -
   5.390 -writeln"Problem 34  AMENDED (TWICE!!)"; (*924 Horn clauses*)
   5.391 -(*Andrews's challenge*)
   5.392 -Goal "((\\<exists>x. \\<forall>y. p x = p y)  =               \
   5.393 -\      ((\\<exists>x. q x) = (\\<forall>y. p y)))     =       \
   5.394 -\     ((\\<exists>x. \\<forall>y. q x = q y)  =               \
   5.395 -\      ((\\<exists>x. p x) = (\\<forall>y. q y)))";
   5.396 -by (meson_tac 1);          (*13 secs*)
   5.397 -result();
   5.398 -
   5.399 -writeln"Problem 35";
   5.400 -Goal "\\<exists>x y. P x y -->  (\\<forall>u v. P u v)";
   5.401 -by (meson_tac 1);
   5.402 -result();
   5.403 -
   5.404 -writeln"Problem 36";  (*15 Horn clauses*)
   5.405 -Goal "(\\<forall>x. \\<exists>y. J x y) & \
   5.406 -\     (\\<forall>x. \\<exists>y. G x y) & \
   5.407 -\     (\\<forall>x y. J x y | G x y -->       \
   5.408 -\     (\\<forall>z. J y z | G y z --> H x z))   \
   5.409 -\   --> (\\<forall>x. \\<exists>y. H x y)";
   5.410 -by (meson_tac 1);
   5.411 -result();
   5.412 -
   5.413 -writeln"Problem 37";  (*10 Horn clauses*)
   5.414 -Goal "(\\<forall>z. \\<exists>w. \\<forall>x. \\<exists>y. \
   5.415 -\          (P x z --> P y w) & P y z & (P y w --> (\\<exists>u. Q u w))) & \
   5.416 -\     (\\<forall>x z. ~P x z --> (\\<exists>y. Q y z)) & \
   5.417 -\     ((\\<exists>x y. Q x y) --> (\\<forall>x. R x x))  \
   5.418 -\   --> (\\<forall>x. \\<exists>y. R x y)";
   5.419 -by (meson_tac 1);   (*causes unification tracing messages*)
   5.420 -result();
   5.421 -
   5.422 -writeln"Problem 38";  (*Quite hard: 422 Horn clauses!!*)
   5.423 -Goal "(\\<forall>x. p a & (p x --> (\\<exists>y. p y & r x y)) -->            \
   5.424 -\          (\\<exists>z. \\<exists>w. p z & r x w & r w z))  =                 \
   5.425 -\     (\\<forall>x. (~p a | p x | (\\<exists>z. \\<exists>w. p z & r x w & r w z)) &  \
   5.426 -\           (~p a | ~(\\<exists>y. p y & r x y) |                      \
   5.427 -\            (\\<exists>z. \\<exists>w. p z & r x w & r w z)))";
   5.428 -by (safe_best_meson_tac 1);  (*10 secs; iter. deepening is slightly slower*)
   5.429 -result();
   5.430 -
   5.431 -writeln"Problem 39";
   5.432 -Goal "~ (\\<exists>x. \\<forall>y. F y x = (~F y y))";
   5.433 -by (meson_tac 1);
   5.434 -result();
   5.435 -
   5.436 -writeln"Problem 40.  AMENDED";
   5.437 -Goal "(\\<exists>y. \\<forall>x. F x y = F x x)  \
   5.438 -\     -->  ~ (\\<forall>x. \\<exists>y. \\<forall>z. F z y = (~F z x))";
   5.439 -by (meson_tac 1);
   5.440 -result();
   5.441 -
   5.442 -writeln"Problem 41";
   5.443 -Goal "(\\<forall>z. (\\<exists>y. (\\<forall>x. f x y = (f x z & ~ f x x))))    \
   5.444 -\     --> ~ (\\<exists>z. \\<forall>x. f x z)";
   5.445 -by (meson_tac 1);
   5.446 -result();
   5.447 -
   5.448 -writeln"Problem 42";
   5.449 -Goal "~ (\\<exists>y. \\<forall>x. p x y = (~ (\\<exists>z. p x z & p z x)))";
   5.450 -by (meson_tac 1);
   5.451 -result();
   5.452 -
   5.453 -writeln"Problem 43  NOW PROVED AUTOMATICALLY!!";
   5.454 -Goal "(\\<forall>x. \\<forall>y. q x y = (\\<forall>z. p z x = (p z y::bool)))  \
   5.455 -\     --> (\\<forall>x. (\\<forall>y. q x y = (q y x::bool)))";
   5.456 -by (safe_best_meson_tac 1);     
   5.457 -(*1.6 secs; iter. deepening is slightly slower*)
   5.458 -result();
   5.459 -
   5.460 -writeln"Problem 44";  (*13 Horn clauses; 7-step proof*)
   5.461 -Goal "(\\<forall>x. f x -->                                    \
   5.462 -\           (\\<exists>y. g y & h x y & (\\<exists>y. g y & ~ h x y)))  &   \
   5.463 -\     (\\<exists>x. j x & (\\<forall>y. g y --> h x y))               \
   5.464 -\     --> (\\<exists>x. j x & ~f x)";
   5.465 -by (meson_tac 1);
   5.466 -result();
   5.467 -
   5.468 -writeln"Problem 45";  (*27 Horn clauses; 54-step proof*)
   5.469 -Goal "(\\<forall>x. f x & (\\<forall>y. g y & h x y --> j x y)        \
   5.470 -\           --> (\\<forall>y. g y & h x y --> k y)) &       \
   5.471 -\     ~ (\\<exists>y. l y & k y) &                                    \
   5.472 -\     (\\<exists>x. f x & (\\<forall>y. h x y --> l y)                        \
   5.473 -\               & (\\<forall>y. g y & h x y --> j x y))             \
   5.474 -\     --> (\\<exists>x. f x & ~ (\\<exists>y. g y & h x y))";
   5.475 -by (safe_best_meson_tac 1);     
   5.476 -(*1.6 secs; iter. deepening is slightly slower*)
   5.477 -result();
   5.478 -
   5.479 -writeln"Problem 46";  (*26 Horn clauses; 21-step proof*)
   5.480 -Goal "(\\<forall>x. f x & (\\<forall>y. f y & h y x --> g y) --> g x) &      \
   5.481 -\     ((\\<exists>x. f x & ~g x) -->                                    \
   5.482 -\     (\\<exists>x. f x & ~g x & (\\<forall>y. f y & ~g y --> j x y))) &    \
   5.483 -\     (\\<forall>x y. f x & f y & h x y --> ~j y x)                    \
   5.484 -\     --> (\\<forall>x. f x --> g x)";
   5.485 -by (safe_best_meson_tac 1);     
   5.486 -(*1.7 secs; iter. deepening is slightly slower*)
   5.487 -result();
   5.488 -
   5.489 -writeln"Problem 47.  Schubert's Steamroller";
   5.490 -        (*26 clauses; 63 Horn clauses
   5.491 -          87094 inferences so far.  Searching to depth 36*)
   5.492 -Goal "(\\<forall>x. P1 x --> P0 x) & (\\<exists>x. P1 x) &     \
   5.493 -\     (\\<forall>x. P2 x --> P0 x) & (\\<exists>x. P2 x) &     \
   5.494 -\     (\\<forall>x. P3 x --> P0 x) & (\\<exists>x. P3 x) &     \
   5.495 -\     (\\<forall>x. P4 x --> P0 x) & (\\<exists>x. P4 x) &     \
   5.496 -\     (\\<forall>x. P5 x --> P0 x) & (\\<exists>x. P5 x) &     \
   5.497 -\     (\\<forall>x. Q1 x --> Q0 x) & (\\<exists>x. Q1 x) &     \
   5.498 -\     (\\<forall>x. P0 x --> ((\\<forall>y. Q0 y-->R x y) |    \
   5.499 -\                      (\\<forall>y. P0 y & S y x &     \
   5.500 -\                           (\\<exists>z. Q0 z&R y z) --> R x y))) &   \
   5.501 -\     (\\<forall>x y. P3 y & (P5 x|P4 x) --> S x y) &        \
   5.502 -\     (\\<forall>x y. P3 x & P2 y --> S x y) &        \
   5.503 -\     (\\<forall>x y. P2 x & P1 y --> S x y) &        \
   5.504 -\     (\\<forall>x y. P1 x & (P2 y|Q1 y) --> ~R x y) &       \
   5.505 -\     (\\<forall>x y. P3 x & P4 y --> R x y) &        \
   5.506 -\     (\\<forall>x y. P3 x & P5 y --> ~R x y) &       \
   5.507 -\     (\\<forall>x. (P4 x|P5 x) --> (\\<exists>y. Q0 y & R x y))      \
   5.508 -\     --> (\\<exists>x y. P0 x & P0 y & (\\<exists>z. Q1 z & R y z & R x y))";
   5.509 -by (safe_best_meson_tac 1);     (*MUCH faster than iterative deepening*)
   5.510 -result();
   5.511 -
   5.512 -(*The Los problem\\<exists> Circulated by John Harrison*)
   5.513 -Goal "(\\<forall>x y z. P x y & P y z --> P x z) &      \
   5.514 -\     (\\<forall>x y z. Q x y & Q y z --> Q x z) &             \
   5.515 -\     (\\<forall>x y. P x y --> P y x) &                       \
   5.516 -\     (\\<forall>x y. P x y | Q x y)                           \
   5.517 -\     --> (\\<forall>x y. P x y) | (\\<forall>x y. Q x y)";
   5.518 -by (safe_best_meson_tac 1);     (*2.3 secs; iter. deepening is VERY slow*)
   5.519 -result();
   5.520 -
   5.521 -(*A similar example, suggested by Johannes Schumann and credited to Pelletier*)
   5.522 -Goal "(!x y z. P x y --> P y z --> P x z) --> \
   5.523 -\     (!x y z. Q x y --> Q y z --> Q x z) --> \
   5.524 -\     (!x y. Q x y --> Q y x) -->  (!x y. P x y | Q x y) --> \
   5.525 -\     (!x y. P x y) | (!x y. Q x y)";
   5.526 -by (safe_best_meson_tac 1);          (*2.7 secs*)
   5.527 -result();
   5.528 -
   5.529 -writeln"Problem 50";  
   5.530 -(*What has this to do with equality?*)
   5.531 -Goal "(\\<forall>x. P a x | (\\<forall>y. P x y)) --> (\\<exists>x. \\<forall>y. P x y)";
   5.532 -by (meson_tac 1);
   5.533 -result();
   5.534 -
   5.535 -writeln"Problem 55";
   5.536 -
   5.537 -(*Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988).
   5.538 -  meson_tac cannot report who killed Agatha. *)
   5.539 -Goal "lives agatha & lives butler & lives charles & \
   5.540 -\     (killed agatha agatha | killed butler agatha | killed charles agatha) & \
   5.541 -\     (!x y. killed x y --> hates x y & ~richer x y) & \
   5.542 -\     (!x. hates agatha x --> ~hates charles x) & \
   5.543 -\     (hates agatha agatha & hates agatha charles) & \
   5.544 -\     (!x. lives x & ~richer x agatha --> hates butler x) & \
   5.545 -\     (!x. hates agatha x --> hates butler x) & \
   5.546 -\     (!x. ~hates x agatha | ~hates x butler | ~hates x charles) --> \
   5.547 -\     (\\<exists>x. killed x agatha)";
   5.548 -by (meson_tac 1);
   5.549 -result();
   5.550 -
   5.551 -writeln"Problem 57";
   5.552 -Goal "P (f a b) (f b c) & P (f b c) (f a c) & \
   5.553 -\     (\\<forall>x y z. P x y & P y z --> P x z)    -->   P (f a b) (f a c)";
   5.554 -by (meson_tac 1);
   5.555 -result();
   5.556 -
   5.557 -writeln"Problem 58";
   5.558 -(* Challenge found on info-hol *)
   5.559 -Goal "\\<forall>P Q R x. \\<exists>v w. \\<forall>y z. P x & Q y --> (P v | R w) & (R z --> Q v)";
   5.560 -by (meson_tac 1);
   5.561 -result();
   5.562 -
   5.563 -writeln"Problem 59";
   5.564 -Goal "(\\<forall>x. P x = (~P(f x))) --> (\\<exists>x. P x & ~P(f x))";
   5.565 -by (meson_tac 1);
   5.566 -result();
   5.567 -
   5.568 -writeln"Problem 60";
   5.569 -Goal "\\<forall>x. P x (f x) = (\\<exists>y. (\\<forall>z. P z y --> P z (f x)) & P x y)";
   5.570 -by (meson_tac 1);
   5.571 -result();
   5.572 -
   5.573 -writeln"Problem 62 as corrected in JAR 18 (1997), page 135";
   5.574 -Goal "(ALL x. p a & (p x --> p(f x)) --> p(f(f x)))  =   \
   5.575 -\     (ALL x. (~ p a | p x | p(f(f x))) &                        \
   5.576 -\             (~ p a | ~ p(f x) | p(f(f x))))";
   5.577 -by (meson_tac 1);
   5.578 -result();
   5.579 -
   5.580 -
   5.581 -(** Charles Morgan's problems **)
   5.582 -
   5.583 -val axa = "\\<forall>x y.   T(i x(i y x))";
   5.584 -val axb = "\\<forall>x y z. T(i(i x(i y z))(i(i x y)(i x z)))";
   5.585 -val axc = "\\<forall>x y.   T(i(i(n x)(n y))(i y x))";
   5.586 -val axd = "\\<forall>x y.   T(i x y) & T x --> T y";
   5.587 -
   5.588 -fun axjoin ([],   q) = q
   5.589 -  | axjoin (p::ps, q) = "(" ^ p ^ ") --> (" ^ axjoin(ps,q) ^ ")";
   5.590 -
   5.591 -Goal (axjoin([axa,axb,axd], "\\<forall>x. T(i x x)"));
   5.592 -by (meson_tac 1);  
   5.593 -result();
   5.594 -
   5.595 -writeln"Problem 66";  
   5.596 -Goal (axjoin([axa,axb,axc,axd], "\\<forall>x. T(i x(n(n x)))"));
   5.597 -(*TOO SLOW, several minutes\\<forall> 
   5.598 -     208346 inferences so far.  Searching to depth 23
   5.599 -by (meson_tac 1);
   5.600 -result();
   5.601 -*)
   5.602 -
   5.603 -writeln"Problem 67";  
   5.604 -Goal (axjoin([axa,axb,axc,axd], "\\<forall>x. T(i(n(n x)) x)"));
   5.605 -(*TOO SLOW: more than 3 minutes!
   5.606 -  51061 inferences so far.  Searching to depth 21
   5.607 -by (meson_tac 1);
   5.608 -result();
   5.609 -*)
   5.610 -
   5.611 -
   5.612 -(*Restore original values*)
   5.613 -Unify.trace_bound := orig_trace_bound;
   5.614 -Unify.search_bound := orig_search_bound;
   5.615 -
   5.616 -writeln"Reached end of file.";
   5.617 -
   5.618 -(*26 August 1992: loaded in 277 secs.  New Jersey v 75*)
     6.1 --- a/src/HOL/ex/mesontest2.ML	Fri Oct 03 12:36:16 2003 +0200
     6.2 +++ b/src/HOL/ex/mesontest2.ML	Wed Oct 08 15:57:41 2003 +0200
     6.3 @@ -3,7 +3,181 @@
     6.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6.5      Copyright   2000  University of Cambridge
     6.6  
     6.7 -MORE and MUCH HARDER test data for the MESON proof procedure
     6.8 +Test data for the MESON proof procedure
     6.9 +   (Excludes the equality problems 51, 52, 56, 58)
    6.10 +
    6.11 +NOTE: most of the old file "mesontest.ML" has been converted to Isar and moved
    6.12 +to Classical.thy
    6.13 +
    6.14 +Use the "mesonlog" shell script to process logs.
    6.15 +
    6.16 +show_hyps := false;
    6.17 +
    6.18 +proofs := 0;
    6.19 +by (rtac ccontr 1);
    6.20 +val [prem] = gethyps 1;
    6.21 +val nnf = make_nnf prem;
    6.22 +val xsko = skolemize nnf;
    6.23 +by (cut_facts_tac [xsko] 1 THEN REPEAT (etac exE 1));
    6.24 +val [_,sko] = gethyps 1;
    6.25 +val clauses = make_clauses [sko];       
    6.26 +val horns = make_horns clauses;
    6.27 +val goes = gocls clauses;
    6.28 +
    6.29 +Goal "False";
    6.30 +by (resolve_tac goes 1);
    6.31 +proofs := 2;
    6.32 +
    6.33 +by (prolog_step_tac horns 1);
    6.34 +by (iter_deepen_prolog_tac horns);
    6.35 +by (depth_prolog_tac horns);
    6.36 +by (best_prolog_tac size_of_subgoals horns);
    6.37 +*)
    6.38 +
    6.39 +writeln"File HOL/ex/meson-test.";
    6.40 +
    6.41 +context Main.thy;
    6.42 +
    6.43 +(*Deep unifications can be required, esp. during transformation to clauses*)
    6.44 +val orig_trace_bound = !Unify.trace_bound
    6.45 +and orig_search_bound = !Unify.search_bound;
    6.46 +Unify.trace_bound := 20;
    6.47 +Unify.search_bound := 40;
    6.48 +
    6.49 +(**** Interactive examples ****)
    6.50 +
    6.51 +(*Generate nice names for Skolem functions*)
    6.52 +Logic.auto_rename := true; Logic.set_rename_prefix "a";
    6.53 +
    6.54 +
    6.55 +writeln"Problem 25";
    6.56 +Goal "(\\<exists>x. P x) &  \
    6.57 +\     (\\<forall>x. L x --> ~ (M x & R x)) &  \
    6.58 +\     (\\<forall>x. P x --> (M x & L x)) &   \
    6.59 +\     ((\\<forall>x. P x --> Q x) | (\\<exists>x. P x & R x))  \
    6.60 +\   --> (\\<exists>x. Q x & P x)";
    6.61 +by (rtac ccontr 1);
    6.62 +val [prem25] = gethyps 1;
    6.63 +val nnf25 = make_nnf prem25;
    6.64 +val xsko25 = skolemize nnf25;
    6.65 +by (cut_facts_tac [xsko25] 1 THEN REPEAT (etac exE 1));
    6.66 +val [_,sko25] = gethyps 1;
    6.67 +val clauses25 = make_clauses [sko25];   (*7 clauses*)
    6.68 +val horns25 = make_horns clauses25;     (*16 Horn clauses*)
    6.69 +val go25::_ = gocls clauses25;
    6.70 +
    6.71 +Goal "False";
    6.72 +by (rtac go25 1);
    6.73 +by (depth_prolog_tac horns25);
    6.74 +
    6.75 +
    6.76 +writeln"Problem 26";
    6.77 +Goal "((\\<exists>x. p x) = (\\<exists>x. q x)) &     \
    6.78 +\     (\\<forall>x. \\<forall>y. p x & q y --> (r x = s y)) \
    6.79 +\ --> ((\\<forall>x. p x --> r x) = (\\<forall>x. q x --> s x))";
    6.80 +by (rtac ccontr 1);
    6.81 +val [prem26] = gethyps 1;
    6.82 +val nnf26 = make_nnf prem26;
    6.83 +val xsko26 = skolemize nnf26;
    6.84 +by (cut_facts_tac [xsko26] 1 THEN REPEAT (etac exE 1));
    6.85 +val [_,sko26] = gethyps 1;
    6.86 +val clauses26 = make_clauses [sko26];                   (*9 clauses*)
    6.87 +val horns26 = make_horns clauses26;                     (*24 Horn clauses*)
    6.88 +val go26::_ = gocls clauses26;
    6.89 +
    6.90 +Goal "False";
    6.91 +by (rtac go26 1);
    6.92 +by (depth_prolog_tac horns26);  (*1.4 secs*)
    6.93 +(*Proof is of length 107!!*)
    6.94 +
    6.95 +
    6.96 +writeln"Problem 43  NOW PROVED AUTOMATICALLY!!";  (*16 Horn clauses*)
    6.97 +Goal "(\\<forall>x. \\<forall>y. q x y = (\\<forall>z. p z x = (p z y::bool)))  \
    6.98 +\     --> (\\<forall>x. (\\<forall>y. q x y = (q y x::bool)))";
    6.99 +by (rtac ccontr 1);
   6.100 +val [prem43] = gethyps 1;
   6.101 +val nnf43 = make_nnf prem43;
   6.102 +val xsko43 = skolemize nnf43;
   6.103 +by (cut_facts_tac [xsko43] 1 THEN REPEAT (etac exE 1));
   6.104 +val [_,sko43] = gethyps 1;
   6.105 +val clauses43 = make_clauses [sko43];   (*6*)
   6.106 +val horns43 = make_horns clauses43;     (*16*)
   6.107 +val go43::_ = gocls clauses43;
   6.108 +
   6.109 +Goal "False";
   6.110 +by (rtac go43 1);
   6.111 +by (best_prolog_tac size_of_subgoals horns43);   (*1.6 secs*)
   6.112 +
   6.113 +(* 
   6.114 +#1  (q x xa ==> ~ q x xa) ==> q xa x
   6.115 +#2  (q xa x ==> ~ q xa x) ==> q x xa
   6.116 +#3  (~ q x xa ==> q x xa) ==> ~ q xa x
   6.117 +#4  (~ q xa x ==> q xa x) ==> ~ q x xa
   6.118 +#5  [| ~ q ?U ?V ==> q ?U ?V; ~ p ?W ?U ==> p ?W ?U |] ==> p ?W ?V
   6.119 +#6  [| ~ p ?W ?U ==> p ?W ?U; p ?W ?V ==> ~ p ?W ?V |] ==> ~ q ?U ?V
   6.120 +#7  [| p ?W ?V ==> ~ p ?W ?V; ~ q ?U ?V ==> q ?U ?V |] ==> ~ p ?W ?U
   6.121 +#8  [| ~ q ?U ?V ==> q ?U ?V; ~ p ?W ?V ==> p ?W ?V |] ==> p ?W ?U
   6.122 +#9  [| ~ p ?W ?V ==> p ?W ?V; p ?W ?U ==> ~ p ?W ?U |] ==> ~ q ?U ?V
   6.123 +#10 [| p ?W ?U ==> ~ p ?W ?U; ~ q ?U ?V ==> q ?U ?V |] ==> ~ p ?W ?V
   6.124 +#11 [| p (xb ?U ?V) ?U ==> ~ p (xb ?U ?V) ?U;
   6.125 +       p (xb ?U ?V) ?V ==> ~ p (xb ?U ?V) ?V |] ==> q ?U ?V
   6.126 +#12 [| p (xb ?U ?V) ?V ==> ~ p (xb ?U ?V) ?V; q ?U ?V ==> ~ q ?U ?V |] ==>
   6.127 +    p (xb ?U ?V) ?U
   6.128 +#13 [| q ?U ?V ==> ~ q ?U ?V; p (xb ?U ?V) ?U ==> ~ p (xb ?U ?V) ?U |] ==>
   6.129 +    p (xb ?U ?V) ?V
   6.130 +#14 [| ~ p (xb ?U ?V) ?U ==> p (xb ?U ?V) ?U;
   6.131 +       ~ p (xb ?U ?V) ?V ==> p (xb ?U ?V) ?V |] ==> q ?U ?V
   6.132 +#15 [| ~ p (xb ?U ?V) ?V ==> p (xb ?U ?V) ?V; q ?U ?V ==> ~ q ?U ?V |] ==>
   6.133 +    ~ p (xb ?U ?V) ?U
   6.134 +#16 [| q ?U ?V ==> ~ q ?U ?V; ~ p (xb ?U ?V) ?U ==> p (xb ?U ?V) ?U |] ==>
   6.135 +    ~ p (xb ?U ?V) ?V
   6.136 +
   6.137 +And here is the proof! (Unkn is the start state after use of goal clause)
   6.138 +[Unkn, Res ([Thm "#14"], false, 1), Res ([Thm "#5"], false, 1),
   6.139 +   Res ([Thm "#1"], false, 1), Asm 1, Res ([Thm "#13"], false, 1), Asm 2,
   6.140 +   Asm 1, Res ([Thm "#13"], false, 1), Asm 1, Res ([Thm "#10"], false, 1),
   6.141 +   Res ([Thm "#16"], false, 1), Asm 2, Asm 1, Res ([Thm "#1"], false, 1),
   6.142 +   Asm 1, Res ([Thm "#14"], false, 1), Res ([Thm "#5"], false, 1),
   6.143 +   Res ([Thm "#2"], false, 1), Asm 1, Res ([Thm "#13"], false, 1), Asm 2,
   6.144 +   Asm 1, Res ([Thm "#8"], false, 1), Res ([Thm "#2"], false, 1), Asm 1,
   6.145 +   Res ([Thm "#12"], false, 1), Asm 2, Asm 1] : lderiv list
   6.146 +*)
   6.147 +
   6.148 +
   6.149 +(*Restore variable name preservation*)
   6.150 +Logic.auto_rename := false; 
   6.151 +
   6.152 +
   6.153 +(** Charles Morgan's problems **)
   6.154 +
   6.155 +val axa = "\\<forall>x y.   T(i x(i y x))";
   6.156 +val axb = "\\<forall>x y z. T(i(i x(i y z))(i(i x y)(i x z)))";
   6.157 +val axc = "\\<forall>x y.   T(i(i(n x)(n y))(i y x))";
   6.158 +val axd = "\\<forall>x y.   T(i x y) & T x --> T y";
   6.159 +
   6.160 +fun axjoin ([],   q) = q
   6.161 +  | axjoin (p::ps, q) = "(" ^ p ^ ") --> (" ^ axjoin(ps,q) ^ ")";
   6.162 +
   6.163 +Goal (axjoin([axa,axb,axd], "\\<forall>x. T(i x x)"));
   6.164 +by (meson_tac 1);  
   6.165 +result();
   6.166 +
   6.167 +writeln"Problem 66";  
   6.168 +Goal (axjoin([axa,axb,axc,axd], "\\<forall>x. T(i x(n(n x)))"));
   6.169 +by (meson_tac 1);  
   6.170 +result();
   6.171 +(*SLOW: 37s on a 1.8MHz machine
   6.172 +     208346 inferences so far.  Searching to depth 23 *)
   6.173 +
   6.174 +writeln"Problem 67";  
   6.175 +Goal (axjoin([axa,axb,axc,axd], "\\<forall>x. T(i(n(n x)) x)"));
   6.176 +by (meson_tac 1);  
   6.177 +result();
   6.178 +(*10s on a 1.8MHz machine
   6.179 +  51061 inferences so far.  Searching to depth 21 *)
   6.180 +
   6.181 +
   6.182 +(*MORE and MUCH HARDER test data for the MESON proof procedure
   6.183  
   6.184  Courtesy John Harrison 
   6.185  
   6.186 @@ -181,7 +355,7 @@
   6.187    meson_tac 1);
   6.188  
   6.189  (*51194 inferences so far.  Searching to depth 13. 204.6 secs
   6.190 -  Strange\\<forall> The previous problem also has 51194 inferences at depth 13.  They
   6.191 +  Strange! The previous problem also has 51194 inferences at depth 13.  They
   6.192     must be very similar!*)
   6.193  val BOO004_1 = prove_hard
   6.194   ("(\\<forall>X. equal(X::'a,X)) &  \
   6.195 @@ -2948,7 +3122,7 @@
   6.196  \  (~subset(bDa::'a,bDd)) --> False",
   6.197    meson_tac 1);
   6.198  
   6.199 -(*34726 inferences so far.  Searching to depth 6.  2420 secs: 40 mins\\<forall> BIG*)
   6.200 +(*34726 inferences so far.  Searching to depth 6.  2420 secs: 40 mins! BIG*)
   6.201  val SET025_4 = prove_hard
   6.202   ("(\\<forall>X. equal(X::'a,X)) &  \
   6.203  \  (\\<forall>Y X. equal(X::'a,Y) --> equal(Y::'a,X)) & \