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