partial conversion to Isar scripts
authorpaulson
Thu Oct 16 10:31:40 2003 +0200 (2003-10-16)
changeset 14236c73d62ce9d1c
parent 14235 281295a1bbaa
child 14237 a486123e24a5
partial conversion to Isar scripts
src/FOL/IFOL.thy
src/FOL/IsaMakefile
src/FOL/ex/Classical.thy
src/FOL/ex/ROOT.ML
src/FOL/ex/cla.ML
     1.1 --- a/src/FOL/IFOL.thy	Wed Oct 15 11:02:28 2003 +0200
     1.2 +++ b/src/FOL/IFOL.thy	Thu Oct 16 10:31:40 2003 +0200
     1.3 @@ -64,6 +64,13 @@
     1.4  
     1.5  local
     1.6  
     1.7 +finalconsts
     1.8 +  False All Ex
     1.9 +  "op ="
    1.10 +  "op &"
    1.11 +  "op |"
    1.12 +  "op -->"
    1.13 +
    1.14  axioms
    1.15  
    1.16    (* Equality *)
    1.17 @@ -86,18 +93,6 @@
    1.18  
    1.19    FalseE:       "False ==> P"
    1.20  
    1.21 -
    1.22 -  (* Definitions *)
    1.23 -
    1.24 -  True_def:     "True  == False-->False"
    1.25 -  not_def:      "~P    == P-->False"
    1.26 -  iff_def:      "P<->Q == (P-->Q) & (Q-->P)"
    1.27 -
    1.28 -  (* Unique existence *)
    1.29 -
    1.30 -  ex1_def:      "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
    1.31 -
    1.32 -
    1.33    (* Quantifiers *)
    1.34  
    1.35    allI:         "(!!x. P(x)) ==> (ALL x. P(x))"
    1.36 @@ -112,6 +107,17 @@
    1.37    iff_reflection: "(P<->Q) ==> (P==Q)"
    1.38  
    1.39  
    1.40 +defs
    1.41 +  (* Definitions *)
    1.42 +
    1.43 +  True_def:     "True  == False-->False"
    1.44 +  not_def:      "~P    == P-->False"
    1.45 +  iff_def:      "P<->Q == (P-->Q) & (Q-->P)"
    1.46 +
    1.47 +  (* Unique existence *)
    1.48 +
    1.49 +  ex1_def:      "Ex1(P) == EX x. P(x) & (ALL y. P(y) --> y=x)"
    1.50 +
    1.51  
    1.52  subsection {* Lemmas and proof tools *}
    1.53  
     2.1 --- a/src/FOL/IsaMakefile	Wed Oct 15 11:02:28 2003 +0200
     2.2 +++ b/src/FOL/IsaMakefile	Thu Oct 16 10:31:40 2003 +0200
     2.3 @@ -45,8 +45,8 @@
     2.4  $(LOG)/FOL-ex.gz: $(OUT)/FOL ex/First_Order_Logic.thy \
     2.5    ex/If.thy ex/IffOracle.ML ex/IffOracle.thy ex/List.ML ex/List.thy	\
     2.6    ex/Nat.ML ex/Nat.thy ex/Nat2.ML ex/Nat2.thy ex/Natural_Numbers.thy	\
     2.7 -  ex/Prolog.ML ex/Prolog.thy ex/ROOT.ML ex/cla.ML ex/document/root.tex	\
     2.8 -  ex/foundn.ML ex/int.ML ex/int.thy ex/intro.ML ex/prop.ML ex/quant.ML
     2.9 +  ex/Prolog.ML ex/Prolog.thy ex/ROOT.ML ex/Classical.thy ex/document/root.tex\
    2.10 +  ex/foundn.ML ex/Intuitionistic.thy ex/intro.ML ex/prop.ML ex/quant.ML
    2.11  	@$(ISATOOL) usedir $(OUT)/FOL ex
    2.12  
    2.13  
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/FOL/ex/Classical.thy	Thu Oct 16 10:31:40 2003 +0200
     3.3 @@ -0,0 +1,523 @@
     3.4 +(*  Title:      FOL/ex/Classical
     3.5 +    ID:         $Id$
     3.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 +    Copyright   1994  University of Cambridge
     3.8 +*)
     3.9 +
    3.10 +header{*Classical Predicate Calculus Problems*}
    3.11 +
    3.12 +theory Classical = FOL:
    3.13 +
    3.14 +lemma "(P --> Q | R) --> (P-->Q) | (P-->R)"
    3.15 +by blast
    3.16 +
    3.17 +text{*If and only if*}
    3.18 +
    3.19 +lemma "(P<->Q) <-> (Q<->P)"
    3.20 +by blast
    3.21 +
    3.22 +lemma "~ (P <-> ~P)"
    3.23 +by blast
    3.24 +
    3.25 +
    3.26 +text{*Sample problems from 
    3.27 +  F. J. Pelletier, 
    3.28 +  Seventy-Five Problems for Testing Automatic Theorem Provers,
    3.29 +  J. Automated Reasoning 2 (1986), 191-216.
    3.30 +  Errata, JAR 4 (1988), 236-236.
    3.31 +
    3.32 +The hardest problems -- judging by experience with several theorem provers,
    3.33 +including matrix ones -- are 34 and 43.
    3.34 +*}
    3.35 +
    3.36 +subsection{*Pelletier's examples*}
    3.37 +
    3.38 +text{*1*}
    3.39 +lemma "(P-->Q)  <->  (~Q --> ~P)"
    3.40 +by blast
    3.41 +
    3.42 +text{*2*}
    3.43 +lemma "~ ~ P  <->  P"
    3.44 +by blast
    3.45 +
    3.46 +text{*3*}
    3.47 +lemma "~(P-->Q) --> (Q-->P)"
    3.48 +by blast
    3.49 +
    3.50 +text{*4*}
    3.51 +lemma "(~P-->Q)  <->  (~Q --> P)"
    3.52 +by blast
    3.53 +
    3.54 +text{*5*}
    3.55 +lemma "((P|Q)-->(P|R)) --> (P|(Q-->R))"
    3.56 +by blast
    3.57 +
    3.58 +text{*6*}
    3.59 +lemma "P | ~ P"
    3.60 +by blast
    3.61 +
    3.62 +text{*7*}
    3.63 +lemma "P | ~ ~ ~ P"
    3.64 +by blast
    3.65 +
    3.66 +text{*8.  Peirce's law*}
    3.67 +lemma "((P-->Q) --> P)  -->  P"
    3.68 +by blast
    3.69 +
    3.70 +text{*9*}
    3.71 +lemma "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
    3.72 +by blast
    3.73 +
    3.74 +text{*10*}
    3.75 +lemma "(Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P<->Q)"
    3.76 +by blast
    3.77 +
    3.78 +text{*11.  Proved in each direction (incorrectly, says Pelletier!!)  *}
    3.79 +lemma "P<->P"
    3.80 +by blast
    3.81 +
    3.82 +text{*12.  "Dijkstra's law"*}
    3.83 +lemma "((P <-> Q) <-> R)  <->  (P <-> (Q <-> R))"
    3.84 +by blast
    3.85 +
    3.86 +text{*13.  Distributive law*}
    3.87 +lemma "P | (Q & R)  <-> (P | Q) & (P | R)"
    3.88 +by blast
    3.89 +
    3.90 +text{*14*}
    3.91 +lemma "(P <-> Q) <-> ((Q | ~P) & (~Q|P))"
    3.92 +by blast
    3.93 +
    3.94 +text{*15*}
    3.95 +lemma "(P --> Q) <-> (~P | Q)"
    3.96 +by blast
    3.97 +
    3.98 +text{*16*}
    3.99 +lemma "(P-->Q) | (Q-->P)"
   3.100 +by blast
   3.101 +
   3.102 +text{*17*}
   3.103 +lemma "((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))"
   3.104 +by blast
   3.105 +
   3.106 +subsection{*Classical Logic: examples with quantifiers*}
   3.107 +
   3.108 +lemma "(\<forall>x. P(x) & Q(x)) <-> (\<forall>x. P(x))  &  (\<forall>x. Q(x))"
   3.109 +by blast
   3.110 +
   3.111 +lemma "(\<exists>x. P-->Q(x))  <->  (P --> (\<exists>x. Q(x)))"
   3.112 +by blast
   3.113 +
   3.114 +lemma "(\<exists>x. P(x)-->Q)  <->  (\<forall>x. P(x)) --> Q"
   3.115 +by blast
   3.116 +
   3.117 +lemma "(\<forall>x. P(x)) | Q  <->  (\<forall>x. P(x) | Q)"
   3.118 +by blast
   3.119 +
   3.120 +text{*Discussed in Avron, Gentzen-Type Systems, Resolution and Tableaux,
   3.121 +  JAR 10 (265-281), 1993.  Proof is trivial!*}
   3.122 +lemma "~((\<exists>x.~P(x)) & ((\<exists>x. P(x)) | (\<exists>x. P(x) & Q(x))) & ~ (\<exists>x. P(x)))"
   3.123 +by blast
   3.124 +
   3.125 +subsection{*Problems requiring quantifier duplication*}
   3.126 +
   3.127 +text{*Theorem B of Peter Andrews, Theorem Proving via General Matings, 
   3.128 +  JACM 28 (1981).*}
   3.129 +lemma "(\<exists>x. \<forall>y. P(x) <-> P(y)) --> ((\<exists>x. P(x)) <-> (\<forall>y. P(y)))"
   3.130 +by blast
   3.131 +
   3.132 +text{*Needs multiple instantiation of ALL.*}
   3.133 +lemma "(\<forall>x. P(x)-->P(f(x)))  &  P(d)-->P(f(f(f(d))))"
   3.134 +by blast
   3.135 +
   3.136 +text{*Needs double instantiation of the quantifier*}
   3.137 +lemma "\<exists>x. P(x) --> P(a) & P(b)"
   3.138 +by blast
   3.139 +
   3.140 +lemma "\<exists>z. P(z) --> (\<forall>x. P(x))"
   3.141 +by blast
   3.142 +
   3.143 +lemma "\<exists>x. (\<exists>y. P(y)) --> P(x)"
   3.144 +by blast
   3.145 +
   3.146 +text{*V. Lifschitz, What Is the Inverse Method?, JAR 5 (1989), 1--23.  NOT PROVED*}
   3.147 +lemma "\<exists>x x'. \<forall>y. \<exists>z z'.  
   3.148 +                (~P(y,y) | P(x,x) | ~S(z,x)) &  
   3.149 +                (S(x,y) | ~S(y,z) | Q(z',z'))  &  
   3.150 +                (Q(x',y) | ~Q(y,z') | S(x',x'))"
   3.151 +oops
   3.152 +
   3.153 +
   3.154 +
   3.155 +subsection{*Hard examples with quantifiers*}
   3.156 +
   3.157 +text{*18*}
   3.158 +lemma "\<exists>y. \<forall>x. P(y)-->P(x)"
   3.159 +by blast
   3.160 +
   3.161 +text{*19*}
   3.162 +lemma "\<exists>x. \<forall>y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))"
   3.163 +by blast
   3.164 +
   3.165 +text{*20*}
   3.166 +lemma "(\<forall>x y. \<exists>z. \<forall>w. (P(x)&Q(y)-->R(z)&S(w)))      
   3.167 +    --> (\<exists>x y. P(x) & Q(y)) --> (\<exists>z. R(z))"
   3.168 +by blast
   3.169 +
   3.170 +text{*21*}
   3.171 +lemma "(\<exists>x. P-->Q(x)) & (\<exists>x. Q(x)-->P) --> (\<exists>x. P<->Q(x))"
   3.172 +by blast
   3.173 +
   3.174 +text{*22*}
   3.175 +lemma "(\<forall>x. P <-> Q(x))  -->  (P <-> (\<forall>x. Q(x)))"
   3.176 +by blast
   3.177 +
   3.178 +text{*23*}
   3.179 +lemma "(\<forall>x. P | Q(x))  <->  (P | (\<forall>x. Q(x)))"
   3.180 +by blast
   3.181 +
   3.182 +text{*24*}
   3.183 +lemma "~(\<exists>x. S(x)&Q(x)) & (\<forall>x. P(x) --> Q(x)|R(x)) &   
   3.184 +      (~(\<exists>x. P(x)) --> (\<exists>x. Q(x))) & (\<forall>x. Q(x)|R(x) --> S(x))   
   3.185 +    --> (\<exists>x. P(x)&R(x))"
   3.186 +by blast
   3.187 +
   3.188 +text{*25*}
   3.189 +lemma "(\<exists>x. P(x)) &   
   3.190 +      (\<forall>x. L(x) --> ~ (M(x) & R(x))) &   
   3.191 +      (\<forall>x. P(x) --> (M(x) & L(x))) &    
   3.192 +      ((\<forall>x. P(x)-->Q(x)) | (\<exists>x. P(x)&R(x)))   
   3.193 +    --> (\<exists>x. Q(x)&P(x))"
   3.194 +by blast
   3.195 +
   3.196 +text{*26*}
   3.197 +lemma "((\<exists>x. p(x)) <-> (\<exists>x. q(x))) &  
   3.198 +      (\<forall>x. \<forall>y. p(x) & q(y) --> (r(x) <-> s(y)))    
   3.199 +  --> ((\<forall>x. p(x)-->r(x)) <-> (\<forall>x. q(x)-->s(x)))"
   3.200 +by blast
   3.201 +
   3.202 +text{*27*}
   3.203 +lemma "(\<exists>x. P(x) & ~Q(x)) &    
   3.204 +      (\<forall>x. P(x) --> R(x)) &    
   3.205 +      (\<forall>x. M(x) & L(x) --> P(x)) &    
   3.206 +      ((\<exists>x. R(x) & ~ Q(x)) --> (\<forall>x. L(x) --> ~ R(x)))   
   3.207 +  --> (\<forall>x. M(x) --> ~L(x))"
   3.208 +by blast
   3.209 +
   3.210 +text{*28.  AMENDED*}
   3.211 +lemma "(\<forall>x. P(x) --> (\<forall>x. Q(x))) &    
   3.212 +        ((\<forall>x. Q(x)|R(x)) --> (\<exists>x. Q(x)&S(x))) &   
   3.213 +        ((\<exists>x. S(x)) --> (\<forall>x. L(x) --> M(x)))   
   3.214 +    --> (\<forall>x. P(x) & L(x) --> M(x))"
   3.215 +by blast
   3.216 +
   3.217 +text{*29.  Essentially the same as Principia Mathematica *11.71*}
   3.218 +lemma "(\<exists>x. P(x)) & (\<exists>y. Q(y))   
   3.219 +    --> ((\<forall>x. P(x)-->R(x)) & (\<forall>y. Q(y)-->S(y))   <->      
   3.220 +         (\<forall>x y. P(x) & Q(y) --> R(x) & S(y)))"
   3.221 +by blast
   3.222 +
   3.223 +text{*30*}
   3.224 +lemma "(\<forall>x. P(x) | Q(x) --> ~ R(x)) &  
   3.225 +      (\<forall>x. (Q(x) --> ~ S(x)) --> P(x) & R(x))   
   3.226 +    --> (\<forall>x. S(x))"
   3.227 +by blast
   3.228 +
   3.229 +text{*31*}
   3.230 +lemma "~(\<exists>x. P(x) & (Q(x) | R(x))) &  
   3.231 +        (\<exists>x. L(x) & P(x)) &  
   3.232 +        (\<forall>x. ~ R(x) --> M(x))   
   3.233 +    --> (\<exists>x. L(x) & M(x))"
   3.234 +by blast
   3.235 +
   3.236 +text{*32*}
   3.237 +lemma "(\<forall>x. P(x) & (Q(x)|R(x))-->S(x)) &  
   3.238 +      (\<forall>x. S(x) & R(x) --> L(x)) &  
   3.239 +      (\<forall>x. M(x) --> R(x))   
   3.240 +      --> (\<forall>x. P(x) & M(x) --> L(x))"
   3.241 +by blast
   3.242 +
   3.243 +text{*33*}
   3.244 +lemma "(\<forall>x. P(a) & (P(x)-->P(b))-->P(c))  <->     
   3.245 +      (\<forall>x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))"
   3.246 +by blast
   3.247 +
   3.248 +text{*34  AMENDED (TWICE!!).  Andrews's challenge*}
   3.249 +lemma "((\<exists>x. \<forall>y. p(x) <-> p(y))  <->                 
   3.250 +       ((\<exists>x. q(x)) <-> (\<forall>y. p(y))))     <->         
   3.251 +      ((\<exists>x. \<forall>y. q(x) <-> q(y))  <->                 
   3.252 +       ((\<exists>x. p(x)) <-> (\<forall>y. q(y))))"
   3.253 +by blast
   3.254 +
   3.255 +text{*35*}
   3.256 +lemma "\<exists>x y. P(x,y) -->  (\<forall>u v. P(u,v))"
   3.257 +by blast
   3.258 +
   3.259 +text{*36*}
   3.260 +lemma "(\<forall>x. \<exists>y. J(x,y)) &  
   3.261 +      (\<forall>x. \<exists>y. G(x,y)) &  
   3.262 +      (\<forall>x y. J(x,y) | G(x,y) --> (\<forall>z. J(y,z) | G(y,z) --> H(x,z)))    
   3.263 +  --> (\<forall>x. \<exists>y. H(x,y))"
   3.264 +by blast
   3.265 +
   3.266 +text{*37*}
   3.267 +lemma "(\<forall>z. \<exists>w. \<forall>x. \<exists>y.  
   3.268 +           (P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (\<exists>u. Q(u,w)))) &  
   3.269 +      (\<forall>x z. ~P(x,z) --> (\<exists>y. Q(y,z))) &  
   3.270 +      ((\<exists>x y. Q(x,y)) --> (\<forall>x. R(x,x)))   
   3.271 +      --> (\<forall>x. \<exists>y. R(x,y))"
   3.272 +by blast
   3.273 +
   3.274 +text{*38*}
   3.275 +lemma "(\<forall>x. p(a) & (p(x) --> (\<exists>y. p(y) & r(x,y))) -->         
   3.276 +             (\<exists>z. \<exists>w. p(z) & r(x,w) & r(w,z)))  <->          
   3.277 +      (\<forall>x. (~p(a) | p(x) | (\<exists>z. \<exists>w. p(z) & r(x,w) & r(w,z))) &     
   3.278 +              (~p(a) | ~(\<exists>y. p(y) & r(x,y)) |                           
   3.279 +              (\<exists>z. \<exists>w. p(z) & r(x,w) & r(w,z))))"
   3.280 +by blast
   3.281 +
   3.282 +text{*39*}
   3.283 +lemma "~ (\<exists>x. \<forall>y. F(y,x) <-> ~F(y,y))"
   3.284 +by blast
   3.285 +
   3.286 +text{*40.  AMENDED*}
   3.287 +lemma "(\<exists>y. \<forall>x. F(x,y) <-> F(x,x)) -->   
   3.288 +              ~(\<forall>x. \<exists>y. \<forall>z. F(z,y) <-> ~ F(z,x))"
   3.289 +by blast
   3.290 +
   3.291 +text{*41*}
   3.292 +lemma "(\<forall>z. \<exists>y. \<forall>x. f(x,y) <-> f(x,z) & ~ f(x,x))         
   3.293 +          --> ~ (\<exists>z. \<forall>x. f(x,z))"
   3.294 +by blast
   3.295 +
   3.296 +text{*42*}
   3.297 +lemma "~ (\<exists>y. \<forall>x. p(x,y) <-> ~ (\<exists>z. p(x,z) & p(z,x)))"
   3.298 +by blast
   3.299 +
   3.300 +text{*43*}
   3.301 +lemma "(\<forall>x. \<forall>y. q(x,y) <-> (\<forall>z. p(z,x) <-> p(z,y)))      
   3.302 +          --> (\<forall>x. \<forall>y. q(x,y) <-> q(y,x))"
   3.303 +by blast
   3.304 +
   3.305 +(*Other proofs: Can use auto, which cheats by using rewriting!  
   3.306 +  Deepen_tac alone requires 253 secs.  Or
   3.307 +  by (mini_tac 1 THEN Deepen_tac 5 1) *)
   3.308 +
   3.309 +text{*44*}
   3.310 +lemma "(\<forall>x. f(x) --> (\<exists>y. g(y) & h(x,y) & (\<exists>y. g(y) & ~ h(x,y)))) &  
   3.311 +      (\<exists>x. j(x) & (\<forall>y. g(y) --> h(x,y)))                    
   3.312 +      --> (\<exists>x. j(x) & ~f(x))"
   3.313 +by blast
   3.314 +
   3.315 +text{*45*}
   3.316 +lemma "(\<forall>x. f(x) & (\<forall>y. g(y) & h(x,y) --> j(x,y))   
   3.317 +                      --> (\<forall>y. g(y) & h(x,y) --> k(y))) &     
   3.318 +      ~ (\<exists>y. l(y) & k(y)) &                                    
   3.319 +      (\<exists>x. f(x) & (\<forall>y. h(x,y) --> l(y))                     
   3.320 +                  & (\<forall>y. g(y) & h(x,y) --> j(x,y)))           
   3.321 +      --> (\<exists>x. f(x) & ~ (\<exists>y. g(y) & h(x,y)))"
   3.322 +by blast
   3.323 +
   3.324 +
   3.325 +text{*46*}
   3.326 +lemma "(\<forall>x. f(x) & (\<forall>y. f(y) & h(y,x) --> g(y)) --> g(x)) &       
   3.327 +      ((\<exists>x. f(x) & ~g(x)) -->                                     
   3.328 +       (\<exists>x. f(x) & ~g(x) & (\<forall>y. f(y) & ~g(y) --> j(x,y)))) &     
   3.329 +      (\<forall>x y. f(x) & f(y) & h(x,y) --> ~j(y,x))                     
   3.330 +       --> (\<forall>x. f(x) --> g(x))"
   3.331 +by blast
   3.332 +
   3.333 +
   3.334 +subsection{*Problems (mainly) involving equality or functions*}
   3.335 +
   3.336 +text{*48*}
   3.337 +lemma "(a=b | c=d) & (a=c | b=d) --> a=d | b=c"
   3.338 +by blast
   3.339 +
   3.340 +text{*49  NOT PROVED AUTOMATICALLY.  Hard because it involves substitution
   3.341 +  for Vars
   3.342 +  the type constraint ensures that x,y,z have the same type as a,b,u. *}
   3.343 +lemma "(\<exists>x y::'a. \<forall>z. z=x | z=y) & P(a) & P(b) & a~=b  
   3.344 +                --> (\<forall>u::'a. P(u))"
   3.345 +apply safe
   3.346 +apply (rule_tac x = a in allE, assumption)
   3.347 +apply (rule_tac x = b in allE, assumption, fast)
   3.348 +       --{*blast's treatment of equality can't do it*}
   3.349 +done
   3.350 +
   3.351 +text{*50.  (What has this to do with equality?) *}
   3.352 +lemma "(\<forall>x. P(a,x) | (\<forall>y. P(x,y))) --> (\<exists>x. \<forall>y. P(x,y))"
   3.353 +by blast
   3.354 +
   3.355 +text{*51*}
   3.356 +lemma "(\<exists>z w. \<forall>x y. P(x,y) <->  (x=z & y=w)) -->   
   3.357 +      (\<exists>z. \<forall>x. \<exists>w. (\<forall>y. P(x,y) <-> y=w) <-> x=z)"
   3.358 +by blast
   3.359 +
   3.360 +text{*52*}
   3.361 +text{*Almost the same as 51. *}
   3.362 +lemma "(\<exists>z w. \<forall>x y. P(x,y) <->  (x=z & y=w)) -->   
   3.363 +      (\<exists>w. \<forall>y. \<exists>z. (\<forall>x. P(x,y) <-> x=z) <-> y=w)"
   3.364 +by blast
   3.365 +
   3.366 +text{*55*}
   3.367 +
   3.368 +(*Original, equational version by Len Schubert, via Pelletier *** NOT PROVED
   3.369 +Goal "(\<exists>x. lives(x) & killed(x,agatha)) &  
   3.370 +   lives(agatha) & lives(butler) & lives(charles) &  
   3.371 +   (\<forall>x. lives(x) --> x=agatha | x=butler | x=charles) &  
   3.372 +   (\<forall>x y. killed(x,y) --> hates(x,y)) &  
   3.373 +   (\<forall>x y. killed(x,y) --> ~richer(x,y)) &  
   3.374 +   (\<forall>x. hates(agatha,x) --> ~hates(charles,x)) &  
   3.375 +   (\<forall>x. ~ x=butler --> hates(agatha,x)) &  
   3.376 +   (\<forall>x. ~richer(x,agatha) --> hates(butler,x)) &  
   3.377 +   (\<forall>x. hates(agatha,x) --> hates(butler,x)) &  
   3.378 +   (\<forall>x. \<exists>y. ~hates(x,y)) &  
   3.379 +   ~ agatha=butler -->  
   3.380 +   killed(?who,agatha)"
   3.381 +by Safe_tac;
   3.382 +by (dres_inst_tac [("x1","x")] (spec RS mp) 1);
   3.383 +by (assume_tac 1);
   3.384 +by (etac (spec RS exE) 1);
   3.385 +by (REPEAT (etac allE 1));
   3.386 +by (Blast_tac 1);
   3.387 +result();
   3.388 +****)
   3.389 +
   3.390 +text{*Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988).
   3.391 +  fast DISCOVERS who killed Agatha. *}
   3.392 +lemma "lives(agatha) & lives(butler) & lives(charles) &  
   3.393 +   (killed(agatha,agatha) | killed(butler,agatha) | killed(charles,agatha)) &  
   3.394 +   (\<forall>x y. killed(x,y) --> hates(x,y) & ~richer(x,y)) &  
   3.395 +   (\<forall>x. hates(agatha,x) --> ~hates(charles,x)) &  
   3.396 +   (hates(agatha,agatha) & hates(agatha,charles)) &  
   3.397 +   (\<forall>x. lives(x) & ~richer(x,agatha) --> hates(butler,x)) &  
   3.398 +   (\<forall>x. hates(agatha,x) --> hates(butler,x)) &  
   3.399 +   (\<forall>x. ~hates(x,agatha) | ~hates(x,butler) | ~hates(x,charles)) -->  
   3.400 +    killed(?who,agatha)"
   3.401 +by fast --{*MUCH faster than blast*}
   3.402 +
   3.403 +
   3.404 +text{*56*}
   3.405 +lemma "(\<forall>x. (\<exists>y. P(y) & x=f(y)) --> P(x)) <-> (\<forall>x. P(x) --> P(f(x)))"
   3.406 +by blast
   3.407 +
   3.408 +text{*57*}
   3.409 +lemma "P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) &  
   3.410 +     (\<forall>x y z. P(x,y) & P(y,z) --> P(x,z))    -->   P(f(a,b), f(a,c))"
   3.411 +by blast
   3.412 +
   3.413 +text{*58  NOT PROVED AUTOMATICALLY*}
   3.414 +lemma "(\<forall>x y. f(x)=g(y)) --> (\<forall>x y. f(f(x))=f(g(y)))"
   3.415 +by (slow elim: subst_context)
   3.416 +
   3.417 +
   3.418 +text{*59*}
   3.419 +lemma "(\<forall>x. P(x) <-> ~P(f(x))) --> (\<exists>x. P(x) & ~P(f(x)))"
   3.420 +by blast
   3.421 +
   3.422 +text{*60*}
   3.423 +lemma "\<forall>x. P(x,f(x)) <-> (\<exists>y. (\<forall>z. P(z,y) --> P(z,f(x))) & P(x,y))"
   3.424 +by blast
   3.425 +
   3.426 +text{*62 as corrected in JAR 18 (1997), page 135*}
   3.427 +lemma "(\<forall>x. p(a) & (p(x) --> p(f(x))) --> p(f(f(x))))  <->      
   3.428 +      (\<forall>x. (~p(a) | p(x) | p(f(f(x)))) &                       
   3.429 +              (~p(a) | ~p(f(x)) | p(f(f(x)))))"
   3.430 +by blast
   3.431 +
   3.432 +text{*From Davis, Obvious Logical Inferences, IJCAI-81, 530-531
   3.433 +  fast indeed copes!*}
   3.434 +lemma "(\<forall>x. F(x) & ~G(x) --> (\<exists>y. H(x,y) & J(y))) &  
   3.435 +              (\<exists>x. K(x) & F(x) & (\<forall>y. H(x,y) --> K(y))) &    
   3.436 +              (\<forall>x. K(x) --> ~G(x))  -->  (\<exists>x. K(x) & J(x))"
   3.437 +by fast
   3.438 +
   3.439 +text{*From Rudnicki, Obvious Inferences, JAR 3 (1987), 383-393.  
   3.440 +  It does seem obvious!*}
   3.441 +lemma "(\<forall>x. F(x) & ~G(x) --> (\<exists>y. H(x,y) & J(y))) &         
   3.442 +      (\<exists>x. K(x) & F(x) & (\<forall>y. H(x,y) --> K(y)))  &         
   3.443 +      (\<forall>x. K(x) --> ~G(x))   -->   (\<exists>x. K(x) --> ~G(x))"
   3.444 +by fast
   3.445 +
   3.446 +text{*Halting problem: Formulation of Li Dafa (AAR Newsletter 27, Oct 1994.)
   3.447 +	author U. Egly*}
   3.448 +lemma "((\<exists>x. A(x) & (\<forall>y. C(y) --> (\<forall>z. D(x,y,z)))) -->                
   3.449 +   (\<exists>w. C(w) & (\<forall>y. C(y) --> (\<forall>z. D(w,y,z)))))                   
   3.450 +  &                                                                      
   3.451 +  (\<forall>w. C(w) & (\<forall>u. C(u) --> (\<forall>v. D(w,u,v))) -->                 
   3.452 +        (\<forall>y z.                                                        
   3.453 +            (C(y) &  P(y,z) --> Q(w,y,z) & OO(w,g)) &                    
   3.454 +            (C(y) & ~P(y,z) --> Q(w,y,z) & OO(w,b))))                    
   3.455 +  &                                                                      
   3.456 +  (\<forall>w. C(w) &                                                         
   3.457 +    (\<forall>y z.                                                            
   3.458 +        (C(y) & P(y,z) --> Q(w,y,z) & OO(w,g)) &                         
   3.459 +        (C(y) & ~P(y,z) --> Q(w,y,z) & OO(w,b))) -->                     
   3.460 +    (\<exists>v. C(v) &                                                        
   3.461 +          (\<forall>y. ((C(y) & Q(w,y,y)) & OO(w,g) --> ~P(v,y)) &            
   3.462 +                  ((C(y) & Q(w,y,y)) & OO(w,b) --> P(v,y) & OO(v,b)))))  
   3.463 +   -->                   
   3.464 +   ~ (\<exists>x. A(x) & (\<forall>y. C(y) --> (\<forall>z. D(x,y,z))))"
   3.465 +by (tactic{*Blast.depth_tac (claset ()) 12 1*})
   3.466 +   --{*Needed because the search for depths below 12 is very slow*}
   3.467 +
   3.468 +
   3.469 +text{*Halting problem II: credited to M. Bruschi by Li Dafa in JAR 18(1), p.105*}
   3.470 +lemma "((\<exists>x. A(x) & (\<forall>y. C(y) --> (\<forall>z. D(x,y,z)))) -->        
   3.471 +   (\<exists>w. C(w) & (\<forall>y. C(y) --> (\<forall>z. D(w,y,z)))))           
   3.472 +  &                                                              
   3.473 +  (\<forall>w. C(w) & (\<forall>u. C(u) --> (\<forall>v. D(w,u,v))) -->         
   3.474 +        (\<forall>y z.                                                
   3.475 +            (C(y) &  P(y,z) --> Q(w,y,z) & OO(w,g)) &           
   3.476 +            (C(y) & ~P(y,z) --> Q(w,y,z) & OO(w,b))))          
   3.477 +  &                                                              
   3.478 +  ((\<exists>w. C(w) & (\<forall>y. (C(y) &  P(y,y) --> Q(w,y,y) & OO(w,g)) & 
   3.479 +                         (C(y) & ~P(y,y) --> Q(w,y,y) & OO(w,b))))  
   3.480 +   -->                                                             
   3.481 +   (\<exists>v. C(v) & (\<forall>y. (C(y) &  P(y,y) --> P(v,y) & OO(v,g)) &   
   3.482 +                         (C(y) & ~P(y,y) --> P(v,y) & OO(v,b)))))  
   3.483 +  -->                                                              
   3.484 +  ((\<exists>v. C(v) & (\<forall>y. (C(y) &  P(y,y) --> P(v,y) & OO(v,g)) &   
   3.485 +                         (C(y) & ~P(y,y) --> P(v,y) & OO(v,b))))   
   3.486 +   -->                                                             
   3.487 +   (\<exists>u. C(u) & (\<forall>y. (C(y) &  P(y,y) --> ~P(u,y)) &     
   3.488 +                         (C(y) & ~P(y,y) --> P(u,y) & OO(u,b)))))  
   3.489 +   -->                                                             
   3.490 +   ~ (\<exists>x. A(x) & (\<forall>y. C(y) --> (\<forall>z. D(x,y,z))))"
   3.491 +by blast
   3.492 +
   3.493 +text{* Challenge found on info-hol *}
   3.494 +lemma "\<forall>x. \<exists>v w. \<forall>y z. P(x) & Q(y) --> (P(v) | R(w)) & (R(z) --> Q(v))"
   3.495 +by blast
   3.496 +
   3.497 +text{*Attributed to Lewis Carroll by S. G. Pulman.  The first or last assumption
   3.498 +can be deleted.*}
   3.499 +lemma "(\<forall>x. honest(x) & industrious(x) --> healthy(x)) &  
   3.500 +      ~ (\<exists>x. grocer(x) & healthy(x)) &  
   3.501 +      (\<forall>x. industrious(x) & grocer(x) --> honest(x)) &  
   3.502 +      (\<forall>x. cyclist(x) --> industrious(x)) &  
   3.503 +      (\<forall>x. ~healthy(x) & cyclist(x) --> ~honest(x))   
   3.504 +      --> (\<forall>x. grocer(x) --> ~cyclist(x))"
   3.505 +by blast
   3.506 +
   3.507 +
   3.508 +(*Runtimes for old versions of this file:
   3.509 +Thu Jul 23 1992: loaded in 467s using iffE [on SPARC2] 
   3.510 +Mon Nov 14 1994: loaded in 144s [on SPARC10, with deepen_tac] 
   3.511 +Wed Nov 16 1994: loaded in 138s [after addition of norm_term_skip] 
   3.512 +Mon Nov 21 1994: loaded in 131s [DEPTH_FIRST suppressing repetitions] 
   3.513 +
   3.514 +Further runtimes on a Sun-4
   3.515 +Tue Mar  4 1997: loaded in 93s (version 94-7) 
   3.516 +Tue Mar  4 1997: loaded in 89s
   3.517 +Thu Apr  3 1997: loaded in 44s--using mostly Blast_tac
   3.518 +Thu Apr  3 1997: loaded in 96s--addition of two Halting Probs
   3.519 +Thu Apr  3 1997: loaded in 98s--using lim-1 for all haz rules
   3.520 +Tue Dec  2 1997: loaded in 107s--added 46; new equalSubst
   3.521 +Fri Dec 12 1997: loaded in 91s--faster proof reconstruction
   3.522 +Thu Dec 18 1997: loaded in 94s--two new "obvious theorems" (??)
   3.523 +*)
   3.524 +
   3.525 +end
   3.526 +
     4.1 --- a/src/FOL/ex/ROOT.ML	Wed Oct 15 11:02:28 2003 +0200
     4.2 +++ b/src/FOL/ex/ROOT.ML	Thu Oct 16 10:31:40 2003 +0200
     4.3 @@ -14,7 +14,7 @@
     4.4  time_use_thy "Prolog";
     4.5  
     4.6  writeln"\n** Intuitionistic examples **\n";
     4.7 -time_use_thy "int";
     4.8 +time_use_thy "Intuitionistic";
     4.9  
    4.10  val thy = IFOL.thy  and  tac = IntPr.fast_tac 1;
    4.11  time_use     "prop.ML";
    4.12 @@ -22,7 +22,7 @@
    4.13  
    4.14  writeln"\n** Classical examples **\n";
    4.15  time_use     "mini.ML";
    4.16 -time_use     "cla.ML";
    4.17 +time_use_thy "Classical";
    4.18  time_use_thy "If";
    4.19  
    4.20  val thy = FOL.thy  and  tac = Cla.fast_tac FOL_cs 1;
     5.1 --- a/src/FOL/ex/cla.ML	Wed Oct 15 11:02:28 2003 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,602 +0,0 @@
     5.4 -(*  Title:      FOL/ex/cla.ML
     5.5 -    ID:         $Id$
     5.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.7 -    Copyright   1994  University of Cambridge
     5.8 -
     5.9 -Classical First-Order Logic
    5.10 -*)
    5.11 -
    5.12 -writeln"File FOL/ex/cla.ML";
    5.13 -
    5.14 -context FOL.thy;
    5.15 -
    5.16 -open Cla;    (*in case structure IntPr is open!*)
    5.17 -
    5.18 -Goal "(P --> Q | R) --> (P-->Q) | (P-->R)";
    5.19 -by (Blast_tac 1);
    5.20 -result();
    5.21 -
    5.22 -(*If and only if*)
    5.23 -
    5.24 -Goal "(P<->Q) <-> (Q<->P)";
    5.25 -by (Blast_tac 1);
    5.26 -result();
    5.27 -
    5.28 -Goal "~ (P <-> ~P)";
    5.29 -by (Blast_tac 1);
    5.30 -result();
    5.31 -
    5.32 -
    5.33 -(*Sample problems from 
    5.34 -  F. J. Pelletier, 
    5.35 -  Seventy-Five Problems for Testing Automatic Theorem Provers,
    5.36 -  J. Automated Reasoning 2 (1986), 191-216.
    5.37 -  Errata, JAR 4 (1988), 236-236.
    5.38 -
    5.39 -The hardest problems -- judging by experience with several theorem provers,
    5.40 -including matrix ones -- are 34 and 43.
    5.41 -*)
    5.42 -
    5.43 -writeln"Pelletier's examples";
    5.44 -(*1*)
    5.45 -Goal "(P-->Q)  <->  (~Q --> ~P)";
    5.46 -by (Blast_tac 1);
    5.47 -result();
    5.48 -
    5.49 -(*2*)
    5.50 -Goal "~ ~ P  <->  P";
    5.51 -by (Blast_tac 1);
    5.52 -result();
    5.53 -
    5.54 -(*3*)
    5.55 -Goal "~(P-->Q) --> (Q-->P)";
    5.56 -by (Blast_tac 1);
    5.57 -result();
    5.58 -
    5.59 -(*4*)
    5.60 -Goal "(~P-->Q)  <->  (~Q --> P)";
    5.61 -by (Blast_tac 1);
    5.62 -result();
    5.63 -
    5.64 -(*5*)
    5.65 -Goal "((P|Q)-->(P|R)) --> (P|(Q-->R))";
    5.66 -by (Blast_tac 1);
    5.67 -result();
    5.68 -
    5.69 -(*6*)
    5.70 -Goal "P | ~ P";
    5.71 -by (Blast_tac 1);
    5.72 -result();
    5.73 -
    5.74 -(*7*)
    5.75 -Goal "P | ~ ~ ~ P";
    5.76 -by (Blast_tac 1);
    5.77 -result();
    5.78 -
    5.79 -(*8.  Peirce's law*)
    5.80 -Goal "((P-->Q) --> P)  -->  P";
    5.81 -by (Blast_tac 1);
    5.82 -result();
    5.83 -
    5.84 -(*9*)
    5.85 -Goal "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
    5.86 -by (Blast_tac 1);
    5.87 -result();
    5.88 -
    5.89 -(*10*)
    5.90 -Goal "(Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P<->Q)";
    5.91 -by (Blast_tac 1);
    5.92 -result();
    5.93 -
    5.94 -(*11.  Proved in each direction (incorrectly, says Pelletier!!)  *)
    5.95 -Goal "P<->P";
    5.96 -by (Blast_tac 1);
    5.97 -result();
    5.98 -
    5.99 -(*12.  "Dijkstra's law"*)
   5.100 -Goal "((P <-> Q) <-> R)  <->  (P <-> (Q <-> R))";
   5.101 -by (Blast_tac 1);
   5.102 -result();
   5.103 -
   5.104 -(*13.  Distributive law*)
   5.105 -Goal "P | (Q & R)  <-> (P | Q) & (P | R)";
   5.106 -by (Blast_tac 1);
   5.107 -result();
   5.108 -
   5.109 -(*14*)
   5.110 -Goal "(P <-> Q) <-> ((Q | ~P) & (~Q|P))";
   5.111 -by (Blast_tac 1);
   5.112 -result();
   5.113 -
   5.114 -(*15*)
   5.115 -Goal "(P --> Q) <-> (~P | Q)";
   5.116 -by (Blast_tac 1);
   5.117 -result();
   5.118 -
   5.119 -(*16*)
   5.120 -Goal "(P-->Q) | (Q-->P)";
   5.121 -by (Blast_tac 1);
   5.122 -result();
   5.123 -
   5.124 -(*17*)
   5.125 -Goal "((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))";
   5.126 -by (Blast_tac 1);
   5.127 -result();
   5.128 -
   5.129 -writeln"Classical Logic: examples with quantifiers";
   5.130 -
   5.131 -Goal "(ALL x. P(x) & Q(x)) <-> (ALL x. P(x))  &  (ALL x. Q(x))";
   5.132 -by (Blast_tac 1);
   5.133 -result(); 
   5.134 -
   5.135 -Goal "(EX x. P-->Q(x))  <->  (P --> (EX x. Q(x)))";
   5.136 -by (Blast_tac 1);
   5.137 -result(); 
   5.138 -
   5.139 -Goal "(EX x. P(x)-->Q)  <->  (ALL x. P(x)) --> Q";
   5.140 -by (Blast_tac 1);
   5.141 -result(); 
   5.142 -
   5.143 -Goal "(ALL x. P(x)) | Q  <->  (ALL x. P(x) | Q)";
   5.144 -by (Blast_tac 1);
   5.145 -result(); 
   5.146 -
   5.147 -(*Discussed in Avron, Gentzen-Type Systems, Resolution and Tableaux,
   5.148 -  JAR 10 (265-281), 1993.  Proof is trivial!*)
   5.149 -Goal "~((EX x.~P(x)) & ((EX x. P(x)) | (EX x. P(x) & Q(x))) & ~ (EX x. P(x)))";
   5.150 -by (Blast_tac 1);
   5.151 -result();
   5.152 -
   5.153 -writeln"Problems requiring quantifier duplication";
   5.154 -
   5.155 -(*Theorem B of Peter Andrews, Theorem Proving via General Matings, 
   5.156 -  JACM 28 (1981).*)
   5.157 -Goal "(EX x. ALL y. P(x) <-> P(y)) --> ((EX x. P(x)) <-> (ALL y. P(y)))";
   5.158 -by (Blast_tac 1);
   5.159 -result();
   5.160 -
   5.161 -(*Needs multiple instantiation of ALL.*)
   5.162 -Goal "(ALL x. P(x)-->P(f(x)))  &  P(d)-->P(f(f(f(d))))";
   5.163 -by (Blast_tac 1);
   5.164 -result();
   5.165 -
   5.166 -(*Needs double instantiation of the quantifier*)
   5.167 -Goal "EX x. P(x) --> P(a) & P(b)";
   5.168 -by (Blast_tac 1);
   5.169 -result();
   5.170 -
   5.171 -Goal "EX z. P(z) --> (ALL x. P(x))";
   5.172 -by (Blast_tac 1);
   5.173 -result();
   5.174 -
   5.175 -Goal "EX x. (EX y. P(y)) --> P(x)";
   5.176 -by (Blast_tac 1);
   5.177 -result();
   5.178 -
   5.179 -(*V. Lifschitz, What Is the Inverse Method?, JAR 5 (1989), 1--23.  NOT PROVED*)
   5.180 -Goal "EX x x'. ALL y. EX z z'. \
   5.181 -\               (~P(y,y) | P(x,x) | ~S(z,x)) & \
   5.182 -\               (S(x,y) | ~S(y,z) | Q(z',z'))  & \
   5.183 -\               (Q(x',y) | ~Q(y,z') | S(x',x'))";
   5.184 -
   5.185 -
   5.186 -
   5.187 -writeln"Hard examples with quantifiers";
   5.188 -
   5.189 -writeln"Problem 18";
   5.190 -Goal "EX y. ALL x. P(y)-->P(x)";
   5.191 -by (Blast_tac 1);
   5.192 -result(); 
   5.193 -
   5.194 -writeln"Problem 19";
   5.195 -Goal "EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))";
   5.196 -by (Blast_tac 1);
   5.197 -result();
   5.198 -
   5.199 -writeln"Problem 20";
   5.200 -Goal "(ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))     \
   5.201 -\   --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))";
   5.202 -by (Blast_tac 1); 
   5.203 -result();
   5.204 -
   5.205 -writeln"Problem 21";
   5.206 -Goal "(EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))";
   5.207 -by (Blast_tac 1);
   5.208 -result();
   5.209 -
   5.210 -writeln"Problem 22";
   5.211 -Goal "(ALL x. P <-> Q(x))  -->  (P <-> (ALL x. Q(x)))";
   5.212 -by (Blast_tac 1); 
   5.213 -result();
   5.214 -
   5.215 -writeln"Problem 23";
   5.216 -Goal "(ALL x. P | Q(x))  <->  (P | (ALL x. Q(x)))";
   5.217 -by (Blast_tac 1);  
   5.218 -result();
   5.219 -
   5.220 -writeln"Problem 24";
   5.221 -Goal "~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &  \
   5.222 -\     (~(EX x. P(x)) --> (EX x. Q(x))) & (ALL x. Q(x)|R(x) --> S(x))  \
   5.223 -\   --> (EX x. P(x)&R(x))";
   5.224 -by (Blast_tac 1); 
   5.225 -result();
   5.226 -
   5.227 -writeln"Problem 25";
   5.228 -Goal "(EX x. P(x)) &  \
   5.229 -\     (ALL x. L(x) --> ~ (M(x) & R(x))) &  \
   5.230 -\     (ALL x. P(x) --> (M(x) & L(x))) &   \
   5.231 -\     ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x)))  \
   5.232 -\   --> (EX x. Q(x)&P(x))";
   5.233 -by (Blast_tac 1); 
   5.234 -result();
   5.235 -
   5.236 -writeln"Problem 26";
   5.237 -Goal "((EX x. p(x)) <-> (EX x. q(x))) & \
   5.238 -\     (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y)))   \
   5.239 -\ --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))";
   5.240 -by (Blast_tac 1);
   5.241 -result();
   5.242 -
   5.243 -writeln"Problem 27";
   5.244 -Goal "(EX x. P(x) & ~Q(x)) &   \
   5.245 -\     (ALL x. P(x) --> R(x)) &   \
   5.246 -\     (ALL x. M(x) & L(x) --> P(x)) &   \
   5.247 -\     ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x)))  \
   5.248 -\ --> (ALL x. M(x) --> ~L(x))";
   5.249 -by (Blast_tac 1); 
   5.250 -result();
   5.251 -
   5.252 -writeln"Problem 28.  AMENDED";
   5.253 -Goal "(ALL x. P(x) --> (ALL x. Q(x))) &   \
   5.254 -\       ((ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) &  \
   5.255 -\       ((EX x. S(x)) --> (ALL x. L(x) --> M(x)))  \
   5.256 -\   --> (ALL x. P(x) & L(x) --> M(x))";
   5.257 -by (Blast_tac 1);  
   5.258 -result();
   5.259 -
   5.260 -writeln"Problem 29.  Essentially the same as Principia Mathematica *11.71";
   5.261 -Goal "(EX x. P(x)) & (EX y. Q(y))  \
   5.262 -\   --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y))   <->     \
   5.263 -\        (ALL x y. P(x) & Q(y) --> R(x) & S(y)))";
   5.264 -by (Blast_tac 1); 
   5.265 -result();
   5.266 -
   5.267 -writeln"Problem 30";
   5.268 -Goal "(ALL x. P(x) | Q(x) --> ~ R(x)) & \
   5.269 -\     (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))  \
   5.270 -\   --> (ALL x. S(x))";
   5.271 -by (Blast_tac 1);  
   5.272 -result();
   5.273 -
   5.274 -writeln"Problem 31";
   5.275 -Goal "~(EX x. P(x) & (Q(x) | R(x))) & \
   5.276 -\       (EX x. L(x) & P(x)) & \
   5.277 -\       (ALL x. ~ R(x) --> M(x))  \
   5.278 -\   --> (EX x. L(x) & M(x))";
   5.279 -by (Blast_tac 1);
   5.280 -result();
   5.281 -
   5.282 -writeln"Problem 32";
   5.283 -Goal "(ALL x. P(x) & (Q(x)|R(x))-->S(x)) & \
   5.284 -\     (ALL x. S(x) & R(x) --> L(x)) & \
   5.285 -\     (ALL x. M(x) --> R(x))  \
   5.286 -\     --> (ALL x. P(x) & M(x) --> L(x))";
   5.287 -by (Blast_tac 1);
   5.288 -result();
   5.289 -
   5.290 -writeln"Problem 33";
   5.291 -Goal "(ALL x. P(a) & (P(x)-->P(b))-->P(c))  <->    \
   5.292 -\     (ALL x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))";
   5.293 -by (Blast_tac 1);
   5.294 -result();
   5.295 -
   5.296 -writeln"Problem 34  AMENDED (TWICE!!)";
   5.297 -(*Andrews's challenge*)
   5.298 -Goal "((EX x. ALL y. p(x) <-> p(y))  <->                \
   5.299 -\      ((EX x. q(x)) <-> (ALL y. p(y))))     <->        \
   5.300 -\     ((EX x. ALL y. q(x) <-> q(y))  <->                \
   5.301 -\      ((EX x. p(x)) <-> (ALL y. q(y))))";
   5.302 -by (Blast_tac 1);
   5.303 -result();
   5.304 -
   5.305 -writeln"Problem 35";
   5.306 -Goal "EX x y. P(x,y) -->  (ALL u v. P(u,v))";
   5.307 -by (Blast_tac 1);
   5.308 -result();
   5.309 -
   5.310 -writeln"Problem 36";
   5.311 -Goal "(ALL x. EX y. J(x,y)) & \
   5.312 -\     (ALL x. EX y. G(x,y)) & \
   5.313 -\     (ALL x y. J(x,y) | G(x,y) --> (ALL z. J(y,z) | G(y,z) --> H(x,z)))   \
   5.314 -\ --> (ALL x. EX y. H(x,y))";
   5.315 -by (Blast_tac 1);
   5.316 -result();
   5.317 -
   5.318 -writeln"Problem 37";
   5.319 -Goal "(ALL z. EX w. ALL x. EX y. \
   5.320 -\          (P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u. Q(u,w)))) & \
   5.321 -\     (ALL x z. ~P(x,z) --> (EX y. Q(y,z))) & \
   5.322 -\     ((EX x y. Q(x,y)) --> (ALL x. R(x,x)))  \
   5.323 -\     --> (ALL x. EX y. R(x,y))";
   5.324 -by (Blast_tac 1);
   5.325 -result();
   5.326 -
   5.327 -writeln"Problem 38";
   5.328 -Goal "(ALL x. p(a) & (p(x) --> (EX y. p(y) & r(x,y))) -->        \
   5.329 -\            (EX z. EX w. p(z) & r(x,w) & r(w,z)))  <->         \
   5.330 -\     (ALL x. (~p(a) | p(x) | (EX z. EX w. p(z) & r(x,w) & r(w,z))) &    \
   5.331 -\             (~p(a) | ~(EX y. p(y) & r(x,y)) |                          \
   5.332 -\             (EX z. EX w. p(z) & r(x,w) & r(w,z))))";
   5.333 -by (Blast_tac 1);  (*beats fast_tac!*)
   5.334 -result();
   5.335 -
   5.336 -writeln"Problem 39";
   5.337 -Goal "~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
   5.338 -by (Blast_tac 1);
   5.339 -result();
   5.340 -
   5.341 -writeln"Problem 40.  AMENDED";
   5.342 -Goal "(EX y. ALL x. F(x,y) <-> F(x,x)) -->  \
   5.343 -\             ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))";
   5.344 -by (Blast_tac 1);
   5.345 -result();
   5.346 -
   5.347 -writeln"Problem 41";
   5.348 -Goal "(ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x))        \
   5.349 -\         --> ~ (EX z. ALL x. f(x,z))";
   5.350 -by (Blast_tac 1);
   5.351 -result();
   5.352 -
   5.353 -writeln"Problem 42";
   5.354 -Goal "~ (EX y. ALL x. p(x,y) <-> ~ (EX z. p(x,z) & p(z,x)))";
   5.355 -by (Blast_tac 1);
   5.356 -result();
   5.357 -
   5.358 -writeln"Problem 43";
   5.359 -Goal "(ALL x. ALL y. q(x,y) <-> (ALL z. p(z,x) <-> p(z,y)))     \
   5.360 -\         --> (ALL x. ALL y. q(x,y) <-> q(y,x))";
   5.361 -by (Blast_tac 1);
   5.362 -(*Other proofs: Can use Auto_tac(), which cheats by using rewriting!  
   5.363 -  Deepen_tac alone requires 253 secs.  Or
   5.364 -  by (mini_tac 1 THEN Deepen_tac 5 1);
   5.365 -*)
   5.366 -result();
   5.367 -
   5.368 -writeln"Problem 44";
   5.369 -Goal "(ALL x. f(x) --> (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y)))) & \
   5.370 -\     (EX x. j(x) & (ALL y. g(y) --> h(x,y)))                   \
   5.371 -\     --> (EX x. j(x) & ~f(x))";
   5.372 -by (Blast_tac 1);
   5.373 -result();
   5.374 -
   5.375 -writeln"Problem 45";
   5.376 -Goal "(ALL x. f(x) & (ALL y. g(y) & h(x,y) --> j(x,y))  \
   5.377 -\                     --> (ALL y. g(y) & h(x,y) --> k(y))) &    \
   5.378 -\     ~ (EX y. l(y) & k(y)) &                                   \
   5.379 -\     (EX x. f(x) & (ALL y. h(x,y) --> l(y))                    \
   5.380 -\                 & (ALL y. g(y) & h(x,y) --> j(x,y)))          \
   5.381 -\     --> (EX x. f(x) & ~ (EX y. g(y) & h(x,y)))";
   5.382 -by (Blast_tac 1); 
   5.383 -result();
   5.384 -
   5.385 -
   5.386 -writeln"Problem 46";
   5.387 -Goal "(ALL x. f(x) & (ALL y. f(y) & h(y,x) --> g(y)) --> g(x)) &      \
   5.388 -\     ((EX x. f(x) & ~g(x)) -->                                    \
   5.389 -\      (EX x. f(x) & ~g(x) & (ALL y. f(y) & ~g(y) --> j(x,y)))) &    \
   5.390 -\     (ALL x y. f(x) & f(y) & h(x,y) --> ~j(y,x))                    \
   5.391 -\      --> (ALL x. f(x) --> g(x))";
   5.392 -by (Blast_tac 1); 
   5.393 -result();
   5.394 -
   5.395 -
   5.396 -writeln"Problems (mainly) involving equality or functions";
   5.397 -
   5.398 -writeln"Problem 48";
   5.399 -Goal "(a=b | c=d) & (a=c | b=d) --> a=d | b=c";
   5.400 -by (Blast_tac 1);
   5.401 -result();
   5.402 -
   5.403 -writeln"Problem 49  NOT PROVED AUTOMATICALLY";
   5.404 -(*Hard because it involves substitution for Vars;
   5.405 -  the type constraint ensures that x,y,z have the same type as a,b,u. *)
   5.406 -Goal "(EX x y::'a. ALL z. z=x | z=y) & P(a) & P(b) & a~=b \
   5.407 -\               --> (ALL u::'a. P(u))";
   5.408 -by Safe_tac;
   5.409 -by (res_inst_tac [("x","a")] allE 1);
   5.410 -by (assume_tac 1);
   5.411 -by (res_inst_tac [("x","b")] allE 1);
   5.412 -by (assume_tac 1);
   5.413 -by (Fast_tac 1);    (*Blast_tac's treatment of equality can't do it*)
   5.414 -result();
   5.415 -
   5.416 -writeln"Problem 50";  
   5.417 -(*What has this to do with equality?*)
   5.418 -Goal "(ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))";
   5.419 -by (Blast_tac 1);
   5.420 -result();
   5.421 -
   5.422 -writeln"Problem 51";
   5.423 -Goal "(EX z w. ALL x y. P(x,y) <->  (x=z & y=w)) -->  \
   5.424 -\     (EX z. ALL x. EX w. (ALL y. P(x,y) <-> y=w) <-> x=z)";
   5.425 -by (Blast_tac 1);
   5.426 -result();
   5.427 -
   5.428 -writeln"Problem 52";
   5.429 -(*Almost the same as 51. *)
   5.430 -Goal "(EX z w. ALL x y. P(x,y) <->  (x=z & y=w)) -->  \
   5.431 -\     (EX w. ALL y. EX z. (ALL x. P(x,y) <-> x=z) <-> y=w)";
   5.432 -by (Blast_tac 1);
   5.433 -result();
   5.434 -
   5.435 -writeln"Problem 55";
   5.436 -
   5.437 -(*Original, equational version by Len Schubert, via Pelletier *** NOT PROVED
   5.438 -Goal "(EX x. lives(x) & killed(x,agatha)) & \
   5.439 -\  lives(agatha) & lives(butler) & lives(charles) & \
   5.440 -\  (ALL x. lives(x) --> x=agatha | x=butler | x=charles) & \
   5.441 -\  (ALL x y. killed(x,y) --> hates(x,y)) & \
   5.442 -\  (ALL x y. killed(x,y) --> ~richer(x,y)) & \
   5.443 -\  (ALL x. hates(agatha,x) --> ~hates(charles,x)) & \
   5.444 -\  (ALL x. ~ x=butler --> hates(agatha,x)) & \
   5.445 -\  (ALL x. ~richer(x,agatha) --> hates(butler,x)) & \
   5.446 -\  (ALL x. hates(agatha,x) --> hates(butler,x)) & \
   5.447 -\  (ALL x. EX y. ~hates(x,y)) & \
   5.448 -\  ~ agatha=butler --> \
   5.449 -\  killed(?who,agatha)";
   5.450 -by Safe_tac;
   5.451 -by (dres_inst_tac [("x1","x")] (spec RS mp) 1);
   5.452 -by (assume_tac 1);
   5.453 -by (etac (spec RS exE) 1);
   5.454 -by (REPEAT (etac allE 1));
   5.455 -by (Blast_tac 1);
   5.456 -result();
   5.457 -****)
   5.458 -
   5.459 -(*Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988).
   5.460 -  fast_tac DISCOVERS who killed Agatha. *)
   5.461 -Goal "lives(agatha) & lives(butler) & lives(charles) & \
   5.462 -\  (killed(agatha,agatha) | killed(butler,agatha) | killed(charles,agatha)) & \
   5.463 -\  (ALL x y. killed(x,y) --> hates(x,y) & ~richer(x,y)) & \
   5.464 -\  (ALL x. hates(agatha,x) --> ~hates(charles,x)) & \
   5.465 -\  (hates(agatha,agatha) & hates(agatha,charles)) & \
   5.466 -\  (ALL x. lives(x) & ~richer(x,agatha) --> hates(butler,x)) & \
   5.467 -\  (ALL x. hates(agatha,x) --> hates(butler,x)) & \
   5.468 -\  (ALL x. ~hates(x,agatha) | ~hates(x,butler) | ~hates(x,charles)) --> \
   5.469 -\   killed(?who,agatha)";
   5.470 -by (Fast_tac 1);  
   5.471 -  (*MUCH faster than Blast_tac: 1.5s against ??s, mostly proof reconstruction*)
   5.472 -result();
   5.473 -
   5.474 -
   5.475 -writeln"Problem 56";
   5.476 -Goal "(ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))";
   5.477 -by (Blast_tac 1);
   5.478 -result();
   5.479 -
   5.480 -writeln"Problem 57";
   5.481 -Goal "P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) & \
   5.482 -\    (ALL x y z. P(x,y) & P(y,z) --> P(x,z))    -->   P(f(a,b), f(a,c))";
   5.483 -by (Blast_tac 1);
   5.484 -result();
   5.485 -
   5.486 -writeln"Problem 58  NOT PROVED AUTOMATICALLY";
   5.487 -Goal "(ALL x y. f(x)=g(y)) --> (ALL x y. f(f(x))=f(g(y)))";
   5.488 -by (slow_tac (claset() addEs [subst_context]) 1);
   5.489 -result();
   5.490 -
   5.491 -writeln"Problem 59";
   5.492 -Goal "(ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))";
   5.493 -by (Blast_tac 1);
   5.494 -result();
   5.495 -
   5.496 -writeln"Problem 60";
   5.497 -Goal "ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))";
   5.498 -by (Blast_tac 1);
   5.499 -result();
   5.500 -
   5.501 -writeln"Problem 62 as corrected in JAR 18 (1997), page 135";
   5.502 -Goal "(ALL x. p(a) & (p(x) --> p(f(x))) --> p(f(f(x))))  <->     \
   5.503 -\     (ALL x. (~p(a) | p(x) | p(f(f(x)))) &                      \
   5.504 -\             (~p(a) | ~p(f(x)) | p(f(f(x)))))";
   5.505 -by (Blast_tac 1);
   5.506 -result();
   5.507 -
   5.508 -(*From Davis, Obvious Logical Inferences, IJCAI-81, 530-531
   5.509 -  Fast_tac indeed copes!*)
   5.510 -Goal "(ALL x. F(x) & ~G(x) --> (EX y. H(x,y) & J(y))) & \
   5.511 -\             (EX x. K(x) & F(x) & (ALL y. H(x,y) --> K(y))) &   \
   5.512 -\             (ALL x. K(x) --> ~G(x))  -->  (EX x. K(x) & J(x))";
   5.513 -by (Fast_tac 1);
   5.514 -result();
   5.515 -
   5.516 -(*From Rudnicki, Obvious Inferences, JAR 3 (1987), 383-393.  
   5.517 -  It does seem obvious!*)
   5.518 -Goal "(ALL x. F(x) & ~G(x) --> (EX y. H(x,y) & J(y))) &        \
   5.519 -\     (EX x. K(x) & F(x) & (ALL y. H(x,y) --> K(y)))  &        \
   5.520 -\     (ALL x. K(x) --> ~G(x))   -->   (EX x. K(x) --> ~G(x))";
   5.521 -by (Fast_tac 1);
   5.522 -result();
   5.523 -
   5.524 -(*Halting problem: Formulation of Li Dafa (AAR Newsletter 27, Oct 1994.)
   5.525 -	author U. Egly*)
   5.526 -Goal "((EX x. A(x) & (ALL y. C(y) --> (ALL z. D(x,y,z)))) -->               \
   5.527 -\  (EX w. C(w) & (ALL y. C(y) --> (ALL z. D(w,y,z)))))                  \
   5.528 -\ &                                                                     \
   5.529 -\ (ALL w. C(w) & (ALL u. C(u) --> (ALL v. D(w,u,v))) -->                \
   5.530 -\       (ALL y z.                                                       \
   5.531 -\           (C(y) &  P(y,z) --> Q(w,y,z) & OO(w,g)) &                   \
   5.532 -\           (C(y) & ~P(y,z) --> Q(w,y,z) & OO(w,b))))                   \
   5.533 -\ &                                                                     \
   5.534 -\ (ALL w. C(w) &                                                        \
   5.535 -\   (ALL y z.                                                           \
   5.536 -\       (C(y) & P(y,z) --> Q(w,y,z) & OO(w,g)) &                        \
   5.537 -\       (C(y) & ~P(y,z) --> Q(w,y,z) & OO(w,b))) -->                    \
   5.538 -\   (EX v. C(v) &                                                       \
   5.539 -\         (ALL y. ((C(y) & Q(w,y,y)) & OO(w,g) --> ~P(v,y)) &           \
   5.540 -\                 ((C(y) & Q(w,y,y)) & OO(w,b) --> P(v,y) & OO(v,b))))) \
   5.541 -\  -->                  \
   5.542 -\  ~ (EX x. A(x) & (ALL y. C(y) --> (ALL z. D(x,y,z))))";
   5.543 -by (Blast.depth_tac (claset()) 12 1);
   5.544 -result();
   5.545 -
   5.546 -
   5.547 -(*Halting problem II: credited to M. Bruschi by Li Dafa in JAR 18(1), p.105*)
   5.548 -Goal "((EX x. A(x) & (ALL y. C(y) --> (ALL z. D(x,y,z)))) -->       \
   5.549 -\  (EX w. C(w) & (ALL y. C(y) --> (ALL z. D(w,y,z)))))          \
   5.550 -\ &                                                             \
   5.551 -\ (ALL w. C(w) & (ALL u. C(u) --> (ALL v. D(w,u,v))) -->        \
   5.552 -\       (ALL y z.                                               \
   5.553 -\           (C(y) &  P(y,z) --> Q(w,y,z) & OO(w,g)) &          \
   5.554 -\           (C(y) & ~P(y,z) --> Q(w,y,z) & OO(w,b))))         \
   5.555 -\ &                                                             \
   5.556 -\ ((EX w. C(w) & (ALL y. (C(y) &  P(y,y) --> Q(w,y,y) & OO(w,g)) &\
   5.557 -\                        (C(y) & ~P(y,y) --> Q(w,y,y) & OO(w,b)))) \
   5.558 -\  -->                                                            \
   5.559 -\  (EX v. C(v) & (ALL y. (C(y) &  P(y,y) --> P(v,y) & OO(v,g)) &  \
   5.560 -\                        (C(y) & ~P(y,y) --> P(v,y) & OO(v,b))))) \
   5.561 -\ -->                                                             \
   5.562 -\ ((EX v. C(v) & (ALL y. (C(y) &  P(y,y) --> P(v,y) & OO(v,g)) &  \
   5.563 -\                        (C(y) & ~P(y,y) --> P(v,y) & OO(v,b))))  \
   5.564 -\  -->                                                            \
   5.565 -\  (EX u. C(u) & (ALL y. (C(y) &  P(y,y) --> ~P(u,y)) &    \
   5.566 -\                        (C(y) & ~P(y,y) --> P(u,y) & OO(u,b))))) \
   5.567 -\  -->                                                            \
   5.568 -\  ~ (EX x. A(x) & (ALL y. C(y) --> (ALL z. D(x,y,z))))";
   5.569 -by (Blast.depth_tac(claset()) 7 1);
   5.570 -result();
   5.571 -
   5.572 -(* Challenge found on info-hol *)
   5.573 -Goal "ALL x. EX v w. ALL y z. P(x) & Q(y) --> (P(v) | R(w)) & (R(z) --> Q(v))";
   5.574 -by (Blast_tac 1);
   5.575 -result();
   5.576 -
   5.577 -(*Attributed to Lewis Carroll by S. G. Pulman.  The first or last assumption
   5.578 -can be deleted.*)
   5.579 -Goal "(ALL x. honest(x) & industrious(x) --> healthy(x)) & \
   5.580 -\     ~ (EX x. grocer(x) & healthy(x)) & \
   5.581 -\     (ALL x. industrious(x) & grocer(x) --> honest(x)) & \
   5.582 -\     (ALL x. cyclist(x) --> industrious(x)) & \
   5.583 -\     (ALL x. ~healthy(x) & cyclist(x) --> ~honest(x))  \
   5.584 -\     --> (ALL x. grocer(x) --> ~cyclist(x))";
   5.585 -by (Blast_tac 1);
   5.586 -result();
   5.587 -
   5.588 -
   5.589 -writeln"Reached end of file.";
   5.590 -
   5.591 -(*Thu Jul 23 1992: loaded in 467s using iffE [on SPARC2] *)
   5.592 -(*Mon Nov 14 1994: loaded in 144s [on SPARC10, with deepen_tac] *)
   5.593 -(*Wed Nov 16 1994: loaded in 138s [after addition of norm_term_skip] *)
   5.594 -(*Mon Nov 21 1994: loaded in 131s [DEPTH_FIRST suppressing repetitions] *)
   5.595 -
   5.596 -(*Further runtimes on pochard*)
   5.597 -(*Tue Mar  4 1997: loaded in 93s (version 94-7) *)
   5.598 -(*Tue Mar  4 1997: loaded in 89s*)
   5.599 -(*Thu Apr  3 1997: loaded in 44s--using mostly Blast_tac*)
   5.600 -(*Thu Apr  3 1997: loaded in 96s--addition of two Halting Probs*)
   5.601 -(*Thu Apr  3 1997: loaded in 98s--using lim-1 for all haz rules*)
   5.602 -(*Tue Dec  2 1997: loaded in 107s--added 46; new equalSubst*)
   5.603 -(*Fri Dec 12 1997: loaded in 91s--faster proof reconstruction*)
   5.604 -(*Thu Dec 18 1997: loaded in 94s--two new "obvious theorems" (??)*)
   5.605 -