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