src/HOL/ex/Classical.thy
author haftmann
Wed Mar 12 19:38:14 2008 +0100 (2008-03-12)
changeset 26265 4b63b9e9b10d
parent 24300 e170cee91c66
child 30607 c3d1590debd8
permissions -rw-r--r--
separated Random.thy from Quickcheck.thy
     1 (*  Title:      HOL/ex/Classical
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     5 *)
     6 
     7 header{*Classical Predicate Calculus Problems*}
     8 
     9 theory Classical imports Main begin
    10 
    11 subsection{*Traditional Classical Reasoner*}
    12 
    13 text{*The machine "griffon" mentioned below is a 2.5GHz Power Mac G5.*}
    14 
    15 text{*Taken from @{text "FOL/Classical.thy"}. When porting examples from
    16 first-order logic, beware of the precedence of @{text "="} versus @{text
    17 "\<leftrightarrow>"}.*}
    18 
    19 lemma "(P --> Q | R) --> (P-->Q) | (P-->R)"
    20 by blast
    21 
    22 text{*If and only if*}
    23 
    24 lemma "(P=Q) = (Q = (P::bool))"
    25 by blast
    26 
    27 lemma "~ (P = (~P))"
    28 by blast
    29 
    30 
    31 text{*Sample problems from
    32   F. J. Pelletier,
    33   Seventy-Five Problems for Testing Automatic Theorem Provers,
    34   J. Automated Reasoning 2 (1986), 191-216.
    35   Errata, JAR 4 (1988), 236-236.
    36 
    37 The hardest problems -- judging by experience with several theorem provers,
    38 including matrix ones -- are 34 and 43.
    39 *}
    40 
    41 subsubsection{*Pelletier's examples*}
    42 
    43 text{*1*}
    44 lemma "(P-->Q)  =  (~Q --> ~P)"
    45 by blast
    46 
    47 text{*2*}
    48 lemma "(~ ~ P) =  P"
    49 by blast
    50 
    51 text{*3*}
    52 lemma "~(P-->Q) --> (Q-->P)"
    53 by blast
    54 
    55 text{*4*}
    56 lemma "(~P-->Q)  =  (~Q --> P)"
    57 by blast
    58 
    59 text{*5*}
    60 lemma "((P|Q)-->(P|R)) --> (P|(Q-->R))"
    61 by blast
    62 
    63 text{*6*}
    64 lemma "P | ~ P"
    65 by blast
    66 
    67 text{*7*}
    68 lemma "P | ~ ~ ~ P"
    69 by blast
    70 
    71 text{*8.  Peirce's law*}
    72 lemma "((P-->Q) --> P)  -->  P"
    73 by blast
    74 
    75 text{*9*}
    76 lemma "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
    77 by blast
    78 
    79 text{*10*}
    80 lemma "(Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P=Q)"
    81 by blast
    82 
    83 text{*11.  Proved in each direction (incorrectly, says Pelletier!!)  *}
    84 lemma "P=(P::bool)"
    85 by blast
    86 
    87 text{*12.  "Dijkstra's law"*}
    88 lemma "((P = Q) = R) = (P = (Q = R))"
    89 by blast
    90 
    91 text{*13.  Distributive law*}
    92 lemma "(P | (Q & R)) = ((P | Q) & (P | R))"
    93 by blast
    94 
    95 text{*14*}
    96 lemma "(P = Q) = ((Q | ~P) & (~Q|P))"
    97 by blast
    98 
    99 text{*15*}
   100 lemma "(P --> Q) = (~P | Q)"
   101 by blast
   102 
   103 text{*16*}
   104 lemma "(P-->Q) | (Q-->P)"
   105 by blast
   106 
   107 text{*17*}
   108 lemma "((P & (Q-->R))-->S)  =  ((~P | Q | S) & (~P | ~R | S))"
   109 by blast
   110 
   111 subsubsection{*Classical Logic: examples with quantifiers*}
   112 
   113 lemma "(\<forall>x. P(x) & Q(x)) = ((\<forall>x. P(x)) & (\<forall>x. Q(x)))"
   114 by blast
   115 
   116 lemma "(\<exists>x. P-->Q(x))  =  (P --> (\<exists>x. Q(x)))"
   117 by blast
   118 
   119 lemma "(\<exists>x. P(x)-->Q) = ((\<forall>x. P(x)) --> Q)"
   120 by blast
   121 
   122 lemma "((\<forall>x. P(x)) | Q)  =  (\<forall>x. P(x) | Q)"
   123 by blast
   124 
   125 text{*From Wishnu Prasetya*}
   126 lemma "(\<forall>s. q(s) --> r(s)) & ~r(s) & (\<forall>s. ~r(s) & ~q(s) --> p(t) | q(t))
   127     --> p(t) | r(t)"
   128 by blast
   129 
   130 
   131 subsubsection{*Problems requiring quantifier duplication*}
   132 
   133 text{*Theorem B of Peter Andrews, Theorem Proving via General Matings,
   134   JACM 28 (1981).*}
   135 lemma "(\<exists>x. \<forall>y. P(x) = P(y)) --> ((\<exists>x. P(x)) = (\<forall>y. P(y)))"
   136 by blast
   137 
   138 text{*Needs multiple instantiation of the quantifier.*}
   139 lemma "(\<forall>x. P(x)-->P(f(x)))  &  P(d)-->P(f(f(f(d))))"
   140 by blast
   141 
   142 text{*Needs double instantiation of the quantifier*}
   143 lemma "\<exists>x. P(x) --> P(a) & P(b)"
   144 by blast
   145 
   146 lemma "\<exists>z. P(z) --> (\<forall>x. P(x))"
   147 by blast
   148 
   149 lemma "\<exists>x. (\<exists>y. P(y)) --> P(x)"
   150 by blast
   151 
   152 subsubsection{*Hard examples with quantifiers*}
   153 
   154 text{*Problem 18*}
   155 lemma "\<exists>y. \<forall>x. P(y)-->P(x)"
   156 by blast
   157 
   158 text{*Problem 19*}
   159 lemma "\<exists>x. \<forall>y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))"
   160 by blast
   161 
   162 text{*Problem 20*}
   163 lemma "(\<forall>x y. \<exists>z. \<forall>w. (P(x)&Q(y)-->R(z)&S(w)))
   164     --> (\<exists>x y. P(x) & Q(y)) --> (\<exists>z. R(z))"
   165 by blast
   166 
   167 text{*Problem 21*}
   168 lemma "(\<exists>x. P-->Q(x)) & (\<exists>x. Q(x)-->P) --> (\<exists>x. P=Q(x))"
   169 by blast
   170 
   171 text{*Problem 22*}
   172 lemma "(\<forall>x. P = Q(x))  -->  (P = (\<forall>x. Q(x)))"
   173 by blast
   174 
   175 text{*Problem 23*}
   176 lemma "(\<forall>x. P | Q(x))  =  (P | (\<forall>x. Q(x)))"
   177 by blast
   178 
   179 text{*Problem 24*}
   180 lemma "~(\<exists>x. S(x)&Q(x)) & (\<forall>x. P(x) --> Q(x)|R(x)) &
   181      (~(\<exists>x. P(x)) --> (\<exists>x. Q(x))) & (\<forall>x. Q(x)|R(x) --> S(x))
   182     --> (\<exists>x. P(x)&R(x))"
   183 by blast
   184 
   185 text{*Problem 25*}
   186 lemma "(\<exists>x. P(x)) &
   187         (\<forall>x. L(x) --> ~ (M(x) & R(x))) &
   188         (\<forall>x. P(x) --> (M(x) & L(x))) &
   189         ((\<forall>x. P(x)-->Q(x)) | (\<exists>x. P(x)&R(x)))
   190     --> (\<exists>x. Q(x)&P(x))"
   191 by blast
   192 
   193 text{*Problem 26*}
   194 lemma "((\<exists>x. p(x)) = (\<exists>x. q(x))) &
   195       (\<forall>x. \<forall>y. p(x) & q(y) --> (r(x) = s(y)))
   196   --> ((\<forall>x. p(x)-->r(x)) = (\<forall>x. q(x)-->s(x)))"
   197 by blast
   198 
   199 text{*Problem 27*}
   200 lemma "(\<exists>x. P(x) & ~Q(x)) &
   201               (\<forall>x. P(x) --> R(x)) &
   202               (\<forall>x. M(x) & L(x) --> P(x)) &
   203               ((\<exists>x. R(x) & ~ Q(x)) --> (\<forall>x. L(x) --> ~ R(x)))
   204           --> (\<forall>x. M(x) --> ~L(x))"
   205 by blast
   206 
   207 text{*Problem 28.  AMENDED*}
   208 lemma "(\<forall>x. P(x) --> (\<forall>x. Q(x))) &
   209         ((\<forall>x. Q(x)|R(x)) --> (\<exists>x. Q(x)&S(x))) &
   210         ((\<exists>x. S(x)) --> (\<forall>x. L(x) --> M(x)))
   211     --> (\<forall>x. P(x) & L(x) --> M(x))"
   212 by blast
   213 
   214 text{*Problem 29.  Essentially the same as Principia Mathematica *11.71*}
   215 lemma "(\<exists>x. F(x)) & (\<exists>y. G(y))
   216     --> ( ((\<forall>x. F(x)-->H(x)) & (\<forall>y. G(y)-->J(y)))  =
   217           (\<forall>x y. F(x) & G(y) --> H(x) & J(y)))"
   218 by blast
   219 
   220 text{*Problem 30*}
   221 lemma "(\<forall>x. P(x) | Q(x) --> ~ R(x)) &
   222         (\<forall>x. (Q(x) --> ~ S(x)) --> P(x) & R(x))
   223     --> (\<forall>x. S(x))"
   224 by blast
   225 
   226 text{*Problem 31*}
   227 lemma "~(\<exists>x. P(x) & (Q(x) | R(x))) &
   228         (\<exists>x. L(x) & P(x)) &
   229         (\<forall>x. ~ R(x) --> M(x))
   230     --> (\<exists>x. L(x) & M(x))"
   231 by blast
   232 
   233 text{*Problem 32*}
   234 lemma "(\<forall>x. P(x) & (Q(x)|R(x))-->S(x)) &
   235         (\<forall>x. S(x) & R(x) --> L(x)) &
   236         (\<forall>x. M(x) --> R(x))
   237     --> (\<forall>x. P(x) & M(x) --> L(x))"
   238 by blast
   239 
   240 text{*Problem 33*}
   241 lemma "(\<forall>x. P(a) & (P(x)-->P(b))-->P(c))  =
   242      (\<forall>x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))"
   243 by blast
   244 
   245 text{*Problem 34  AMENDED (TWICE!!)*}
   246 text{*Andrews's challenge*}
   247 lemma "((\<exists>x. \<forall>y. p(x) = p(y))  =
   248                ((\<exists>x. q(x)) = (\<forall>y. p(y))))   =
   249               ((\<exists>x. \<forall>y. q(x) = q(y))  =
   250                ((\<exists>x. p(x)) = (\<forall>y. q(y))))"
   251 by blast
   252 
   253 text{*Problem 35*}
   254 lemma "\<exists>x y. P x y -->  (\<forall>u v. P u v)"
   255 by blast
   256 
   257 text{*Problem 36*}
   258 lemma "(\<forall>x. \<exists>y. J x y) &
   259         (\<forall>x. \<exists>y. G x y) &
   260         (\<forall>x y. J x y | G x y -->
   261         (\<forall>z. J y z | G y z --> H x z))
   262     --> (\<forall>x. \<exists>y. H x y)"
   263 by blast
   264 
   265 text{*Problem 37*}
   266 lemma "(\<forall>z. \<exists>w. \<forall>x. \<exists>y.
   267            (P x z -->P y w) & P y z & (P y w --> (\<exists>u. Q u w))) &
   268         (\<forall>x z. ~(P x z) --> (\<exists>y. Q y z)) &
   269         ((\<exists>x y. Q x y) --> (\<forall>x. R x x))
   270     --> (\<forall>x. \<exists>y. R x y)"
   271 by blast
   272 
   273 text{*Problem 38*}
   274 lemma "(\<forall>x. p(a) & (p(x) --> (\<exists>y. p(y) & r x y)) -->
   275            (\<exists>z. \<exists>w. p(z) & r x w & r w z))  =
   276      (\<forall>x. (~p(a) | p(x) | (\<exists>z. \<exists>w. p(z) & r x w & r w z)) &
   277            (~p(a) | ~(\<exists>y. p(y) & r x y) |
   278             (\<exists>z. \<exists>w. p(z) & r x w & r w z)))"
   279 by blast (*beats fast!*)
   280 
   281 text{*Problem 39*}
   282 lemma "~ (\<exists>x. \<forall>y. F y x = (~ F y y))"
   283 by blast
   284 
   285 text{*Problem 40.  AMENDED*}
   286 lemma "(\<exists>y. \<forall>x. F x y = F x x)
   287         -->  ~ (\<forall>x. \<exists>y. \<forall>z. F z y = (~ F z x))"
   288 by blast
   289 
   290 text{*Problem 41*}
   291 lemma "(\<forall>z. \<exists>y. \<forall>x. f x y = (f x z & ~ f x x))
   292                --> ~ (\<exists>z. \<forall>x. f x z)"
   293 by blast
   294 
   295 text{*Problem 42*}
   296 lemma "~ (\<exists>y. \<forall>x. p x y = (~ (\<exists>z. p x z & p z x)))"
   297 by blast
   298 
   299 text{*Problem 43!!*}
   300 lemma "(\<forall>x::'a. \<forall>y::'a. q x y = (\<forall>z. p z x = (p z y::bool)))
   301   --> (\<forall>x. (\<forall>y. q x y = (q y x::bool)))"
   302 by blast
   303 
   304 text{*Problem 44*}
   305 lemma "(\<forall>x. f(x) -->
   306               (\<exists>y. g(y) & h x y & (\<exists>y. g(y) & ~ h x y)))  &
   307               (\<exists>x. j(x) & (\<forall>y. g(y) --> h x y))
   308               --> (\<exists>x. j(x) & ~f(x))"
   309 by blast
   310 
   311 text{*Problem 45*}
   312 lemma "(\<forall>x. f(x) & (\<forall>y. g(y) & h x y --> j x y)
   313                       --> (\<forall>y. g(y) & h x y --> k(y))) &
   314      ~ (\<exists>y. l(y) & k(y)) &
   315      (\<exists>x. f(x) & (\<forall>y. h x y --> l(y))
   316                 & (\<forall>y. g(y) & h x y --> j x y))
   317       --> (\<exists>x. f(x) & ~ (\<exists>y. g(y) & h x y))"
   318 by blast
   319 
   320 
   321 subsubsection{*Problems (mainly) involving equality or functions*}
   322 
   323 text{*Problem 48*}
   324 lemma "(a=b | c=d) & (a=c | b=d) --> a=d | b=c"
   325 by blast
   326 
   327 text{*Problem 49  NOT PROVED AUTOMATICALLY.
   328      Hard because it involves substitution for Vars
   329   the type constraint ensures that x,y,z have the same type as a,b,u. *}
   330 lemma "(\<exists>x y::'a. \<forall>z. z=x | z=y) & P(a) & P(b) & (~a=b)
   331                 --> (\<forall>u::'a. P(u))"
   332 by metis
   333 
   334 text{*Problem 50.  (What has this to do with equality?) *}
   335 lemma "(\<forall>x. P a x | (\<forall>y. P x y)) --> (\<exists>x. \<forall>y. P x y)"
   336 by blast
   337 
   338 text{*Problem 51*}
   339 lemma "(\<exists>z w. \<forall>x y. P x y = (x=z & y=w)) -->
   340      (\<exists>z. \<forall>x. \<exists>w. (\<forall>y. P x y = (y=w)) = (x=z))"
   341 by blast
   342 
   343 text{*Problem 52. Almost the same as 51. *}
   344 lemma "(\<exists>z w. \<forall>x y. P x y = (x=z & y=w)) -->
   345      (\<exists>w. \<forall>y. \<exists>z. (\<forall>x. P x y = (x=z)) = (y=w))"
   346 by blast
   347 
   348 text{*Problem 55*}
   349 
   350 text{*Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988).
   351   fast DISCOVERS who killed Agatha. *}
   352 lemma "lives(agatha) & lives(butler) & lives(charles) &
   353    (killed agatha agatha | killed butler agatha | killed charles agatha) &
   354    (\<forall>x y. killed x y --> hates x y & ~richer x y) &
   355    (\<forall>x. hates agatha x --> ~hates charles x) &
   356    (hates agatha agatha & hates agatha charles) &
   357    (\<forall>x. lives(x) & ~richer x agatha --> hates butler x) &
   358    (\<forall>x. hates agatha x --> hates butler x) &
   359    (\<forall>x. ~hates x agatha | ~hates x butler | ~hates x charles) -->
   360     killed ?who agatha"
   361 by fast
   362 
   363 text{*Problem 56*}
   364 lemma "(\<forall>x. (\<exists>y. P(y) & x=f(y)) --> P(x)) = (\<forall>x. P(x) --> P(f(x)))"
   365 by blast
   366 
   367 text{*Problem 57*}
   368 lemma "P (f a b) (f b c) & P (f b c) (f a c) &
   369      (\<forall>x y z. P x y & P y z --> P x z)    -->   P (f a b) (f a c)"
   370 by blast
   371 
   372 text{*Problem 58  NOT PROVED AUTOMATICALLY*}
   373 lemma "(\<forall>x y. f(x)=g(y)) --> (\<forall>x y. f(f(x))=f(g(y)))"
   374 by (fast intro: arg_cong [of concl: f])
   375 
   376 text{*Problem 59*}
   377 lemma "(\<forall>x. P(x) = (~P(f(x)))) --> (\<exists>x. P(x) & ~P(f(x)))"
   378 by blast
   379 
   380 text{*Problem 60*}
   381 lemma "\<forall>x. P x (f x) = (\<exists>y. (\<forall>z. P z y --> P z (f x)) & P x y)"
   382 by blast
   383 
   384 text{*Problem 62 as corrected in JAR 18 (1997), page 135*}
   385 lemma "(\<forall>x. p a & (p x --> p(f x)) --> p(f(f x)))  =
   386       (\<forall>x. (~ p a | p x | p(f(f x))) &
   387               (~ p a | ~ p(f x) | p(f(f x))))"
   388 by blast
   389 
   390 text{*From Davis, Obvious Logical Inferences, IJCAI-81, 530-531
   391   fast indeed copes!*}
   392 lemma "(\<forall>x. F(x) & ~G(x) --> (\<exists>y. H(x,y) & J(y))) &
   393        (\<exists>x. K(x) & F(x) & (\<forall>y. H(x,y) --> K(y))) &
   394        (\<forall>x. K(x) --> ~G(x))  -->  (\<exists>x. K(x) & J(x))"
   395 by fast
   396 
   397 text{*From Rudnicki, Obvious Inferences, JAR 3 (1987), 383-393.
   398   It does seem obvious!*}
   399 lemma "(\<forall>x. F(x) & ~G(x) --> (\<exists>y. H(x,y) & J(y))) &
   400        (\<exists>x. K(x) & F(x) & (\<forall>y. H(x,y) --> K(y)))  &
   401        (\<forall>x. K(x) --> ~G(x))   -->   (\<exists>x. K(x) --> ~G(x))"
   402 by fast
   403 
   404 text{*Attributed to Lewis Carroll by S. G. Pulman.  The first or last
   405 assumption can be deleted.*}
   406 lemma "(\<forall>x. honest(x) & industrious(x) --> healthy(x)) &
   407       ~ (\<exists>x. grocer(x) & healthy(x)) &
   408       (\<forall>x. industrious(x) & grocer(x) --> honest(x)) &
   409       (\<forall>x. cyclist(x) --> industrious(x)) &
   410       (\<forall>x. ~healthy(x) & cyclist(x) --> ~honest(x))
   411       --> (\<forall>x. grocer(x) --> ~cyclist(x))"
   412 by blast
   413 
   414 lemma "(\<forall>x y. R(x,y) | R(y,x)) &
   415        (\<forall>x y. S(x,y) & S(y,x) --> x=y) &
   416        (\<forall>x y. R(x,y) --> S(x,y))    -->   (\<forall>x y. S(x,y) --> R(x,y))"
   417 by blast
   418 
   419 
   420 subsection{*Model Elimination Prover*}
   421 
   422 
   423 text{*Trying out meson with arguments*}
   424 lemma "x < y & y < z --> ~ (z < (x::nat))"
   425 by (meson order_less_irrefl order_less_trans)
   426 
   427 text{*The "small example" from Bezem, Hendriks and de Nivelle,
   428 Automatic Proof Construction in Type Theory Using Resolution,
   429 JAR 29: 3-4 (2002), pages 253-275 *}
   430 lemma "(\<forall>x y z. R(x,y) & R(y,z) --> R(x,z)) &
   431        (\<forall>x. \<exists>y. R(x,y)) -->
   432        ~ (\<forall>x. P x = (\<forall>y. R(x,y) --> ~ P y))"
   433 by (tactic{*Meson.safe_best_meson_tac 1*})
   434     --{*In contrast, @{text meson} is SLOW: 7.6s on griffon*}
   435 
   436 
   437 subsubsection{*Pelletier's examples*}
   438 text{*1*}
   439 lemma "(P --> Q)  =  (~Q --> ~P)"
   440 by blast
   441 
   442 text{*2*}
   443 lemma "(~ ~ P) =  P"
   444 by blast
   445 
   446 text{*3*}
   447 lemma "~(P-->Q) --> (Q-->P)"
   448 by blast
   449 
   450 text{*4*}
   451 lemma "(~P-->Q)  =  (~Q --> P)"
   452 by blast
   453 
   454 text{*5*}
   455 lemma "((P|Q)-->(P|R)) --> (P|(Q-->R))"
   456 by blast
   457 
   458 text{*6*}
   459 lemma "P | ~ P"
   460 by blast
   461 
   462 text{*7*}
   463 lemma "P | ~ ~ ~ P"
   464 by blast
   465 
   466 text{*8.  Peirce's law*}
   467 lemma "((P-->Q) --> P)  -->  P"
   468 by blast
   469 
   470 text{*9*}
   471 lemma "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
   472 by blast
   473 
   474 text{*10*}
   475 lemma "(Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P=Q)"
   476 by blast
   477 
   478 text{*11.  Proved in each direction (incorrectly, says Pelletier!!)  *}
   479 lemma "P=(P::bool)"
   480 by blast
   481 
   482 text{*12.  "Dijkstra's law"*}
   483 lemma "((P = Q) = R) = (P = (Q = R))"
   484 by blast
   485 
   486 text{*13.  Distributive law*}
   487 lemma "(P | (Q & R)) = ((P | Q) & (P | R))"
   488 by blast
   489 
   490 text{*14*}
   491 lemma "(P = Q) = ((Q | ~P) & (~Q|P))"
   492 by blast
   493 
   494 text{*15*}
   495 lemma "(P --> Q) = (~P | Q)"
   496 by blast
   497 
   498 text{*16*}
   499 lemma "(P-->Q) | (Q-->P)"
   500 by blast
   501 
   502 text{*17*}
   503 lemma "((P & (Q-->R))-->S)  =  ((~P | Q | S) & (~P | ~R | S))"
   504 by blast
   505 
   506 subsubsection{*Classical Logic: examples with quantifiers*}
   507 
   508 lemma "(\<forall>x. P x & Q x) = ((\<forall>x. P x) & (\<forall>x. Q x))"
   509 by blast
   510 
   511 lemma "(\<exists>x. P --> Q x)  =  (P --> (\<exists>x. Q x))"
   512 by blast
   513 
   514 lemma "(\<exists>x. P x --> Q) = ((\<forall>x. P x) --> Q)"
   515 by blast
   516 
   517 lemma "((\<forall>x. P x) | Q)  =  (\<forall>x. P x | Q)"
   518 by blast
   519 
   520 lemma "(\<forall>x. P x --> P(f x))  &  P d --> P(f(f(f d)))"
   521 by blast
   522 
   523 text{*Needs double instantiation of EXISTS*}
   524 lemma "\<exists>x. P x --> P a & P b"
   525 by blast
   526 
   527 lemma "\<exists>z. P z --> (\<forall>x. P x)"
   528 by blast
   529 
   530 text{*From a paper by Claire Quigley*}
   531 lemma "\<exists>y. ((P c & Q y) | (\<exists>z. ~ Q z)) | (\<exists>x. ~ P x & Q d)"
   532 by fast
   533 
   534 subsubsection{*Hard examples with quantifiers*}
   535 
   536 text{*Problem 18*}
   537 lemma "\<exists>y. \<forall>x. P y --> P x"
   538 by blast
   539 
   540 text{*Problem 19*}
   541 lemma "\<exists>x. \<forall>y z. (P y --> Q z) --> (P x --> Q x)"
   542 by blast
   543 
   544 text{*Problem 20*}
   545 lemma "(\<forall>x y. \<exists>z. \<forall>w. (P x & Q y --> R z & S w))
   546     --> (\<exists>x y. P x & Q y) --> (\<exists>z. R z)"
   547 by blast
   548 
   549 text{*Problem 21*}
   550 lemma "(\<exists>x. P --> Q x) & (\<exists>x. Q x --> P) --> (\<exists>x. P=Q x)"
   551 by blast
   552 
   553 text{*Problem 22*}
   554 lemma "(\<forall>x. P = Q x)  -->  (P = (\<forall>x. Q x))"
   555 by blast
   556 
   557 text{*Problem 23*}
   558 lemma "(\<forall>x. P | Q x)  =  (P | (\<forall>x. Q x))"
   559 by blast
   560 
   561 text{*Problem 24*}  (*The first goal clause is useless*)
   562 lemma "~(\<exists>x. S x & Q x) & (\<forall>x. P x --> Q x | R x) &
   563       (~(\<exists>x. P x) --> (\<exists>x. Q x)) & (\<forall>x. Q x | R x --> S x)
   564     --> (\<exists>x. P x & R x)"
   565 by blast
   566 
   567 text{*Problem 25*}
   568 lemma "(\<exists>x. P x) &
   569       (\<forall>x. L x --> ~ (M x & R x)) &
   570       (\<forall>x. P x --> (M x & L x)) &
   571       ((\<forall>x. P x --> Q x) | (\<exists>x. P x & R x))
   572     --> (\<exists>x. Q x & P x)"
   573 by blast
   574 
   575 text{*Problem 26; has 24 Horn clauses*}
   576 lemma "((\<exists>x. p x) = (\<exists>x. q x)) &
   577       (\<forall>x. \<forall>y. p x & q y --> (r x = s y))
   578   --> ((\<forall>x. p x --> r x) = (\<forall>x. q x --> s x))"
   579 by blast
   580 
   581 text{*Problem 27; has 13 Horn clauses*}
   582 lemma "(\<exists>x. P x & ~Q x) &
   583       (\<forall>x. P x --> R x) &
   584       (\<forall>x. M x & L x --> P x) &
   585       ((\<exists>x. R x & ~ Q x) --> (\<forall>x. L x --> ~ R x))
   586       --> (\<forall>x. M x --> ~L x)"
   587 by blast
   588 
   589 text{*Problem 28.  AMENDED; has 14 Horn clauses*}
   590 lemma "(\<forall>x. P x --> (\<forall>x. Q x)) &
   591       ((\<forall>x. Q x | R x) --> (\<exists>x. Q x & S x)) &
   592       ((\<exists>x. S x) --> (\<forall>x. L x --> M x))
   593     --> (\<forall>x. P x & L x --> M x)"
   594 by blast
   595 
   596 text{*Problem 29.  Essentially the same as Principia Mathematica *11.71.
   597       62 Horn clauses*}
   598 lemma "(\<exists>x. F x) & (\<exists>y. G y)
   599     --> ( ((\<forall>x. F x --> H x) & (\<forall>y. G y --> J y))  =
   600           (\<forall>x y. F x & G y --> H x & J y))"
   601 by blast
   602 
   603 
   604 text{*Problem 30*}
   605 lemma "(\<forall>x. P x | Q x --> ~ R x) & (\<forall>x. (Q x --> ~ S x) --> P x & R x)
   606        --> (\<forall>x. S x)"
   607 by blast
   608 
   609 text{*Problem 31; has 10 Horn clauses; first negative clauses is useless*}
   610 lemma "~(\<exists>x. P x & (Q x | R x)) &
   611       (\<exists>x. L x & P x) &
   612       (\<forall>x. ~ R x --> M x)
   613     --> (\<exists>x. L x & M x)"
   614 by blast
   615 
   616 text{*Problem 32*}
   617 lemma "(\<forall>x. P x & (Q x | R x)-->S x) &
   618       (\<forall>x. S x & R x --> L x) &
   619       (\<forall>x. M x --> R x)
   620     --> (\<forall>x. P x & M x --> L x)"
   621 by blast
   622 
   623 text{*Problem 33; has 55 Horn clauses*}
   624 lemma "(\<forall>x. P a & (P x --> P b)-->P c)  =
   625       (\<forall>x. (~P a | P x | P c) & (~P a | ~P b | P c))"
   626 by blast
   627 
   628 text{*Problem 34: Andrews's challenge has 924 Horn clauses*}
   629 lemma "((\<exists>x. \<forall>y. p x = p y)  = ((\<exists>x. q x) = (\<forall>y. p y)))     =
   630       ((\<exists>x. \<forall>y. q x = q y)  = ((\<exists>x. p x) = (\<forall>y. q y)))"
   631 by blast
   632 
   633 text{*Problem 35*}
   634 lemma "\<exists>x y. P x y -->  (\<forall>u v. P u v)"
   635 by blast
   636 
   637 text{*Problem 36; has 15 Horn clauses*}
   638 lemma "(\<forall>x. \<exists>y. J x y) & (\<forall>x. \<exists>y. G x y) &
   639        (\<forall>x y. J x y | G x y --> (\<forall>z. J y z | G y z --> H x z))
   640        --> (\<forall>x. \<exists>y. H x y)"
   641 by blast
   642 
   643 text{*Problem 37; has 10 Horn clauses*}
   644 lemma "(\<forall>z. \<exists>w. \<forall>x. \<exists>y.
   645            (P x z --> P y w) & P y z & (P y w --> (\<exists>u. Q u w))) &
   646       (\<forall>x z. ~P x z --> (\<exists>y. Q y z)) &
   647       ((\<exists>x y. Q x y) --> (\<forall>x. R x x))
   648     --> (\<forall>x. \<exists>y. R x y)"
   649 by blast --{*causes unification tracing messages*}
   650 
   651 
   652 text{*Problem 38*}  text{*Quite hard: 422 Horn clauses!!*}
   653 lemma "(\<forall>x. p a & (p x --> (\<exists>y. p y & r x y)) -->
   654            (\<exists>z. \<exists>w. p z & r x w & r w z))  =
   655       (\<forall>x. (~p a | p x | (\<exists>z. \<exists>w. p z & r x w & r w z)) &
   656             (~p a | ~(\<exists>y. p y & r x y) |
   657              (\<exists>z. \<exists>w. p z & r x w & r w z)))"
   658 by blast
   659 
   660 text{*Problem 39*}
   661 lemma "~ (\<exists>x. \<forall>y. F y x = (~F y y))"
   662 by blast
   663 
   664 text{*Problem 40.  AMENDED*}
   665 lemma "(\<exists>y. \<forall>x. F x y = F x x)
   666       -->  ~ (\<forall>x. \<exists>y. \<forall>z. F z y = (~F z x))"
   667 by blast
   668 
   669 text{*Problem 41*}
   670 lemma "(\<forall>z. (\<exists>y. (\<forall>x. f x y = (f x z & ~ f x x))))
   671       --> ~ (\<exists>z. \<forall>x. f x z)"
   672 by blast
   673 
   674 text{*Problem 42*}
   675 lemma "~ (\<exists>y. \<forall>x. p x y = (~ (\<exists>z. p x z & p z x)))"
   676 by blast
   677 
   678 text{*Problem 43  NOW PROVED AUTOMATICALLY!!*}
   679 lemma "(\<forall>x. \<forall>y. q x y = (\<forall>z. p z x = (p z y::bool)))
   680       --> (\<forall>x. (\<forall>y. q x y = (q y x::bool)))"
   681 by blast
   682 
   683 text{*Problem 44: 13 Horn clauses; 7-step proof*}
   684 lemma "(\<forall>x. f x --> (\<exists>y. g y & h x y & (\<exists>y. g y & ~ h x y)))  &
   685        (\<exists>x. j x & (\<forall>y. g y --> h x y))
   686        --> (\<exists>x. j x & ~f x)"
   687 by blast
   688 
   689 text{*Problem 45; has 27 Horn clauses; 54-step proof*}
   690 lemma "(\<forall>x. f x & (\<forall>y. g y & h x y --> j x y)
   691             --> (\<forall>y. g y & h x y --> k y)) &
   692       ~ (\<exists>y. l y & k y) &
   693       (\<exists>x. f x & (\<forall>y. h x y --> l y)
   694                 & (\<forall>y. g y & h x y --> j x y))
   695       --> (\<exists>x. f x & ~ (\<exists>y. g y & h x y))"
   696 by blast
   697 
   698 text{*Problem 46; has 26 Horn clauses; 21-step proof*}
   699 lemma "(\<forall>x. f x & (\<forall>y. f y & h y x --> g y) --> g x) &
   700        ((\<exists>x. f x & ~g x) -->
   701        (\<exists>x. f x & ~g x & (\<forall>y. f y & ~g y --> j x y))) &
   702        (\<forall>x y. f x & f y & h x y --> ~j y x)
   703        --> (\<forall>x. f x --> g x)"
   704 by blast
   705 
   706 text{*Problem 47.  Schubert's Steamroller.
   707       26 clauses; 63 Horn clauses.
   708       87094 inferences so far.  Searching to depth 36*}
   709 lemma "(\<forall>x. wolf x \<longrightarrow> animal x) & (\<exists>x. wolf x) &
   710        (\<forall>x. fox x \<longrightarrow> animal x) & (\<exists>x. fox x) &
   711        (\<forall>x. bird x \<longrightarrow> animal x) & (\<exists>x. bird x) &
   712        (\<forall>x. caterpillar x \<longrightarrow> animal x) & (\<exists>x. caterpillar x) &
   713        (\<forall>x. snail x \<longrightarrow> animal x) & (\<exists>x. snail x) &
   714        (\<forall>x. grain x \<longrightarrow> plant x) & (\<exists>x. grain x) &
   715        (\<forall>x. animal x \<longrightarrow>
   716              ((\<forall>y. plant y \<longrightarrow> eats x y)  \<or> 
   717 	      (\<forall>y. animal y & smaller_than y x &
   718                     (\<exists>z. plant z & eats y z) \<longrightarrow> eats x y))) &
   719        (\<forall>x y. bird y & (snail x \<or> caterpillar x) \<longrightarrow> smaller_than x y) &
   720        (\<forall>x y. bird x & fox y \<longrightarrow> smaller_than x y) &
   721        (\<forall>x y. fox x & wolf y \<longrightarrow> smaller_than x y) &
   722        (\<forall>x y. wolf x & (fox y \<or> grain y) \<longrightarrow> ~eats x y) &
   723        (\<forall>x y. bird x & caterpillar y \<longrightarrow> eats x y) &
   724        (\<forall>x y. bird x & snail y \<longrightarrow> ~eats x y) &
   725        (\<forall>x. (caterpillar x \<or> snail x) \<longrightarrow> (\<exists>y. plant y & eats x y))
   726        \<longrightarrow> (\<exists>x y. animal x & animal y & (\<exists>z. grain z & eats y z & eats x y))"
   727 by (tactic{*Meson.safe_best_meson_tac 1*})
   728     --{*Nearly twice as fast as @{text meson},
   729         which performs iterative deepening rather than best-first search*}
   730 
   731 text{*The Los problem. Circulated by John Harrison*}
   732 lemma "(\<forall>x y z. P x y & P y z --> P x z) &
   733        (\<forall>x y z. Q x y & Q y z --> Q x z) &
   734        (\<forall>x y. P x y --> P y x) &
   735        (\<forall>x y. P x y | Q x y)
   736        --> (\<forall>x y. P x y) | (\<forall>x y. Q x y)"
   737 by meson
   738 
   739 text{*A similar example, suggested by Johannes Schumann and
   740  credited to Pelletier*}
   741 lemma "(\<forall>x y z. P x y --> P y z --> P x z) -->
   742        (\<forall>x y z. Q x y --> Q y z --> Q x z) -->
   743        (\<forall>x y. Q x y --> Q y x) -->  (\<forall>x y. P x y | Q x y) -->
   744        (\<forall>x y. P x y) | (\<forall>x y. Q x y)"
   745 by meson
   746 
   747 text{*Problem 50.  What has this to do with equality?*}
   748 lemma "(\<forall>x. P a x | (\<forall>y. P x y)) --> (\<exists>x. \<forall>y. P x y)"
   749 by blast
   750 
   751 text{*Problem 54: NOT PROVED*}
   752 lemma "(\<forall>y::'a. \<exists>z. \<forall>x. F x z = (x=y)) -->
   753       ~ (\<exists>w. \<forall>x. F x w = (\<forall>u. F x u --> (\<exists>y. F y u & ~ (\<exists>z. F z u & F z y))))"
   754 oops 
   755 
   756 
   757 text{*Problem 55*}
   758 
   759 text{*Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988).
   760   @{text meson} cannot report who killed Agatha. *}
   761 lemma "lives agatha & lives butler & lives charles &
   762        (killed agatha agatha | killed butler agatha | killed charles agatha) &
   763        (\<forall>x y. killed x y --> hates x y & ~richer x y) &
   764        (\<forall>x. hates agatha x --> ~hates charles x) &
   765        (hates agatha agatha & hates agatha charles) &
   766        (\<forall>x. lives x & ~richer x agatha --> hates butler x) &
   767        (\<forall>x. hates agatha x --> hates butler x) &
   768        (\<forall>x. ~hates x agatha | ~hates x butler | ~hates x charles) -->
   769        (\<exists>x. killed x agatha)"
   770 by meson
   771 
   772 text{*Problem 57*}
   773 lemma "P (f a b) (f b c) & P (f b c) (f a c) &
   774       (\<forall>x y z. P x y & P y z --> P x z)    -->   P (f a b) (f a c)"
   775 by blast
   776 
   777 text{*Problem 58: Challenge found on info-hol *}
   778 lemma "\<forall>P Q R x. \<exists>v w. \<forall>y z. P x & Q y --> (P v | R w) & (R z --> Q v)"
   779 by blast
   780 
   781 text{*Problem 59*}
   782 lemma "(\<forall>x. P x = (~P(f x))) --> (\<exists>x. P x & ~P(f x))"
   783 by blast
   784 
   785 text{*Problem 60*}
   786 lemma "\<forall>x. P x (f x) = (\<exists>y. (\<forall>z. P z y --> P z (f x)) & P x y)"
   787 by blast
   788 
   789 text{*Problem 62 as corrected in JAR 18 (1997), page 135*}
   790 lemma "(\<forall>x. p a & (p x --> p(f x)) --> p(f(f x)))  =
   791        (\<forall>x. (~ p a | p x | p(f(f x))) &
   792             (~ p a | ~ p(f x) | p(f(f x))))"
   793 by blast
   794 
   795 text{** Charles Morgan's problems **}
   796 
   797 lemma
   798   assumes a: "\<forall>x y.  T(i x(i y x))"
   799       and b: "\<forall>x y z. T(i (i x (i y z)) (i (i x y) (i x z)))"
   800       and c: "\<forall>x y.   T(i (i (n x) (n y)) (i y x))"
   801       and c': "\<forall>x y.   T(i (i y x) (i (n x) (n y)))"
   802       and d: "\<forall>x y.   T(i x y) & T x --> T y"
   803  shows True
   804 proof -
   805   from a b d have "\<forall>x. T(i x x)" by blast
   806   from a b c d have "\<forall>x. T(i x (n(n x)))" --{*Problem 66*}
   807     by metis
   808   from a b c d have "\<forall>x. T(i (n(n x)) x)" --{*Problem 67*}
   809     by meson
   810       --{*4.9s on griffon. 51061 inferences, depth 21 *}
   811   from a b c' d have "\<forall>x. T(i x (n(n x)))" 
   812       --{*Problem 68: not proved.  Listed as satisfiable in TPTP (LCL078-1)*}
   813 oops
   814 
   815 text{*Problem 71, as found in TPTP (SYN007+1.005)*}
   816 lemma "p1 = (p2 = (p3 = (p4 = (p5 = (p1 = (p2 = (p3 = (p4 = p5))))))))"
   817 by blast
   818 
   819 end