src/HOL/ex/cla.ML
author paulson
Tue Mar 04 10:21:16 1997 +0100 (1997-03-04)
changeset 2715 79c35a051196
parent 2575 65abf447151b
child 2891 d8f254ad1ab9
permissions -rw-r--r--
Updated reference to Pelletier erratum
     1 (*  Title:      HOL/ex/cla
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     5 
     6 Higher-Order Logic: predicate calculus problems
     7 
     8 Taken from FOL/cla.ML; beware of precedence of = vs <->
     9 *)
    10 
    11 writeln"File HOL/ex/cla.";
    12 
    13 set_current_thy "HOL";  (*Boosts efficiency by omitting redundant rules*)
    14 
    15 goal HOL.thy "(P --> Q | R) --> (P-->Q) | (P-->R)";
    16 by (Fast_tac 1);
    17 result();
    18 
    19 (*If and only if*)
    20 
    21 goal HOL.thy "(P=Q) = (Q=P::bool)";
    22 by (Fast_tac 1);
    23 result();
    24 
    25 goal HOL.thy "~ (P = (~P))";
    26 by (Fast_tac 1);
    27 result();
    28 
    29 
    30 (*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 writeln"Pelletier's examples";
    41 (*1*)
    42 goal HOL.thy "(P-->Q)  =  (~Q --> ~P)";
    43 by (Fast_tac 1);
    44 result();
    45 
    46 (*2*)
    47 goal HOL.thy "(~ ~ P) =  P";
    48 by (Fast_tac 1);
    49 result();
    50 
    51 (*3*)
    52 goal HOL.thy "~(P-->Q) --> (Q-->P)";
    53 by (Fast_tac 1);
    54 result();
    55 
    56 (*4*)
    57 goal HOL.thy "(~P-->Q)  =  (~Q --> P)";
    58 by (Fast_tac 1);
    59 result();
    60 
    61 (*5*)
    62 goal HOL.thy "((P|Q)-->(P|R)) --> (P|(Q-->R))";
    63 by (Fast_tac 1);
    64 result();
    65 
    66 (*6*)
    67 goal HOL.thy "P | ~ P";
    68 by (Fast_tac 1);
    69 result();
    70 
    71 (*7*)
    72 goal HOL.thy "P | ~ ~ ~ P";
    73 by (Fast_tac 1);
    74 result();
    75 
    76 (*8.  Peirce's law*)
    77 goal HOL.thy "((P-->Q) --> P)  -->  P";
    78 by (Fast_tac 1);
    79 result();
    80 
    81 (*9*)
    82 goal HOL.thy "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
    83 by (Fast_tac 1);
    84 result();
    85 
    86 (*10*)
    87 goal HOL.thy "(Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P=Q)";
    88 by (Fast_tac 1);
    89 result();
    90 
    91 (*11.  Proved in each direction (incorrectly, says Pelletier!!)  *)
    92 goal HOL.thy "P=P::bool";
    93 by (Fast_tac 1);
    94 result();
    95 
    96 (*12.  "Dijkstra's law"*)
    97 goal HOL.thy "((P = Q) = R) = (P = (Q = R))";
    98 by (Fast_tac 1);
    99 result();
   100 
   101 (*13.  Distributive law*)
   102 goal HOL.thy "(P | (Q & R)) = ((P | Q) & (P | R))";
   103 by (Fast_tac 1);
   104 result();
   105 
   106 (*14*)
   107 goal HOL.thy "(P = Q) = ((Q | ~P) & (~Q|P))";
   108 by (Fast_tac 1);
   109 result();
   110 
   111 (*15*)
   112 goal HOL.thy "(P --> Q) = (~P | Q)";
   113 by (Fast_tac 1);
   114 result();
   115 
   116 (*16*)
   117 goal HOL.thy "(P-->Q) | (Q-->P)";
   118 by (Fast_tac 1);
   119 result();
   120 
   121 (*17*)
   122 goal HOL.thy "((P & (Q-->R))-->S)  =  ((~P | Q | S) & (~P | ~R | S))";
   123 by (Fast_tac 1);
   124 result();
   125 
   126 writeln"Classical Logic: examples with quantifiers";
   127 
   128 goal HOL.thy "(! x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))";
   129 by (Fast_tac 1);
   130 result(); 
   131 
   132 goal HOL.thy "(? x. P-->Q(x))  =  (P --> (? x.Q(x)))";
   133 by (Fast_tac 1);
   134 result(); 
   135 
   136 goal HOL.thy "(? x.P(x)-->Q) = ((! x.P(x)) --> Q)";
   137 by (Fast_tac 1);
   138 result(); 
   139 
   140 goal HOL.thy "((! x.P(x)) | Q)  =  (! x. P(x) | Q)";
   141 by (Fast_tac 1);
   142 result(); 
   143 
   144 (*From Wishnu Prasetya*)
   145 goal HOL.thy
   146    "(!s. q(s) --> r(s)) & ~r(s) & (!s. ~r(s) & ~q(s) --> p(t) | q(t)) \
   147 \   --> p(t) | r(t)";
   148 by (Fast_tac 1);
   149 result(); 
   150 
   151 
   152 writeln"Problems requiring quantifier duplication";
   153 
   154 (*Needs multiple instantiation of the quantifier.*)
   155 goal HOL.thy "(! x. P(x)-->P(f(x)))  &  P(d)-->P(f(f(f(d))))";
   156 by (Deepen_tac 1 1);
   157 result();
   158 
   159 (*Needs double instantiation of the quantifier*)
   160 goal HOL.thy "? x. P(x) --> P(a) & P(b)";
   161 by (Deepen_tac 1 1);
   162 result();
   163 
   164 goal HOL.thy "? z. P(z) --> (! x. P(x))";
   165 by (Deepen_tac 1 1);
   166 result();
   167 
   168 goal HOL.thy "? x. (? y. P(y)) --> P(x)";
   169 by (Deepen_tac 1 1);
   170 result();
   171 
   172 writeln"Hard examples with quantifiers";
   173 
   174 writeln"Problem 18";
   175 goal HOL.thy "? y. ! x. P(y)-->P(x)";
   176 by (Deepen_tac 1 1);
   177 result(); 
   178 
   179 writeln"Problem 19";
   180 goal HOL.thy "? x. ! y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))";
   181 by (Deepen_tac 1 1);
   182 result();
   183 
   184 writeln"Problem 20";
   185 goal HOL.thy "(! x y. ? z. ! w. (P(x)&Q(y)-->R(z)&S(w)))     \
   186 \   --> (? x y. P(x) & Q(y)) --> (? z. R(z))";
   187 by (Fast_tac 1); 
   188 result();
   189 
   190 writeln"Problem 21";
   191 goal HOL.thy "(? x. P-->Q(x)) & (? x. Q(x)-->P) --> (? x. P=Q(x))";
   192 by (Deepen_tac 1 1); 
   193 result();
   194 
   195 writeln"Problem 22";
   196 goal HOL.thy "(! x. P = Q(x))  -->  (P = (! x. Q(x)))";
   197 by (Fast_tac 1); 
   198 result();
   199 
   200 writeln"Problem 23";
   201 goal HOL.thy "(! x. P | Q(x))  =  (P | (! x. Q(x)))";
   202 by (Best_tac 1);  
   203 result();
   204 
   205 writeln"Problem 24";
   206 goal HOL.thy "~(? x. S(x)&Q(x)) & (! x. P(x) --> Q(x)|R(x)) &  \
   207 \    (~(? x.P(x)) --> (? x.Q(x))) & (! x. Q(x)|R(x) --> S(x))  \
   208 \   --> (? x. P(x)&R(x))";
   209 by (Fast_tac 1); 
   210 result();
   211 
   212 writeln"Problem 25";
   213 goal HOL.thy "(? x. P(x)) &  \
   214 \       (! x. L(x) --> ~ (M(x) & R(x))) &  \
   215 \       (! x. P(x) --> (M(x) & L(x))) &   \
   216 \       ((! x. P(x)-->Q(x)) | (? x. P(x)&R(x)))  \
   217 \   --> (? x. Q(x)&P(x))";
   218 by (Best_tac 1); 
   219 result();
   220 
   221 writeln"Problem 26";
   222 goal HOL.thy "((? x. p(x)) = (? x. q(x))) &     \
   223 \     (! x. ! y. p(x) & q(y) --> (r(x) = s(y))) \
   224 \ --> ((! x. p(x)-->r(x)) = (! x. q(x)-->s(x)))";
   225 by (Fast_tac 1);
   226 result();
   227 
   228 writeln"Problem 27";
   229 goal HOL.thy "(? x. P(x) & ~Q(x)) &   \
   230 \             (! x. P(x) --> R(x)) &   \
   231 \             (! x. M(x) & L(x) --> P(x)) &   \
   232 \             ((? x. R(x) & ~ Q(x)) --> (! x. L(x) --> ~ R(x)))  \
   233 \         --> (! x. M(x) --> ~L(x))";
   234 by (Fast_tac 1); 
   235 result();
   236 
   237 writeln"Problem 28.  AMENDED";
   238 goal HOL.thy "(! x. P(x) --> (! x. Q(x))) &   \
   239 \       ((! x. Q(x)|R(x)) --> (? x. Q(x)&S(x))) &  \
   240 \       ((? x.S(x)) --> (! x. L(x) --> M(x)))  \
   241 \   --> (! x. P(x) & L(x) --> M(x))";
   242 by (Fast_tac 1);  
   243 result();
   244 
   245 writeln"Problem 29.  Essentially the same as Principia Mathematica *11.71";
   246 goal HOL.thy "(? x. F(x)) & (? y. G(y))  \
   247 \   --> ( ((! x. F(x)-->H(x)) & (! y. G(y)-->J(y)))  =   \
   248 \         (! x y. F(x) & G(y) --> H(x) & J(y)))";
   249 by (Fast_tac 1); 
   250 result();
   251 
   252 writeln"Problem 30";
   253 goal HOL.thy "(! x. P(x) | Q(x) --> ~ R(x)) & \
   254 \       (! x. (Q(x) --> ~ S(x)) --> P(x) & R(x))  \
   255 \   --> (! x. S(x))";
   256 by (Fast_tac 1);  
   257 result();
   258 
   259 writeln"Problem 31";
   260 goal HOL.thy "~(? x.P(x) & (Q(x) | R(x))) & \
   261 \       (? x. L(x) & P(x)) & \
   262 \       (! x. ~ R(x) --> M(x))  \
   263 \   --> (? x. L(x) & M(x))";
   264 by (Fast_tac 1);
   265 result();
   266 
   267 writeln"Problem 32";
   268 goal HOL.thy "(! x. P(x) & (Q(x)|R(x))-->S(x)) & \
   269 \       (! x. S(x) & R(x) --> L(x)) & \
   270 \       (! x. M(x) --> R(x))  \
   271 \   --> (! x. P(x) & M(x) --> L(x))";
   272 by (Best_tac 1);
   273 result();
   274 
   275 writeln"Problem 33";
   276 goal HOL.thy "(! x. P(a) & (P(x)-->P(b))-->P(c))  =    \
   277 \    (! x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))";
   278 by (Best_tac 1);
   279 result();
   280 
   281 writeln"Problem 34  AMENDED (TWICE!!)";
   282 (*Andrews's challenge*)
   283 goal HOL.thy "((? x. ! y. p(x) = p(y))  =               \
   284 \                   ((? x. q(x)) = (! y. p(y))))   =    \
   285 \                  ((? x. ! y. q(x) = q(y))  =          \
   286 \                   ((? x. p(x)) = (! y. q(y))))";
   287 by (Deepen_tac 3 1);
   288 (*slower with smaller bounds*)
   289 result();
   290 
   291 writeln"Problem 35";
   292 goal HOL.thy "? x y. P x y -->  (! u v. P u v)";
   293 by (Deepen_tac 1 1);
   294 result();
   295 
   296 writeln"Problem 36";
   297 goal HOL.thy "(! x. ? y. J x y) & \
   298 \       (! x. ? y. G x y) & \
   299 \       (! x y. J x y | G x y -->       \
   300 \       (! z. J y z | G y z --> H x z))   \
   301 \   --> (! x. ? y. H x y)";
   302 by (Fast_tac 1);
   303 result();
   304 
   305 writeln"Problem 37";
   306 goal HOL.thy "(! z. ? w. ! x. ? y. \
   307 \          (P x z -->P y w) & P y z & (P y w --> (? u.Q u w))) & \
   308 \       (! x z. ~(P x z) --> (? y. Q y z)) & \
   309 \       ((? x y. Q x y) --> (! x. R x x))  \
   310 \   --> (! x. ? y. R x y)";
   311 by (Fast_tac 1);
   312 result();
   313 
   314 writeln"Problem 38";
   315 goal HOL.thy
   316     "(! x. p(a) & (p(x) --> (? y. p(y) & r x y)) -->            \
   317 \          (? z. ? w. p(z) & r x w & r w z))  =                 \
   318 \    (! x. (~p(a) | p(x) | (? z. ? w. p(z) & r x w & r w z)) &  \
   319 \          (~p(a) | ~(? y. p(y) & r x y) |                      \
   320 \           (? z. ? w. p(z) & r x w & r w z)))";
   321 by (Deepen_tac 0 1);  (*beats fast_tac!*)
   322 result();
   323 
   324 writeln"Problem 39";
   325 goal HOL.thy "~ (? x. ! y. F y x = (~ F y y))";
   326 by (Fast_tac 1);
   327 result();
   328 
   329 writeln"Problem 40.  AMENDED";
   330 goal HOL.thy "(? y. ! x. F x y = F x x)  \
   331 \       -->  ~ (! x. ? y. ! z. F z y = (~ F z x))";
   332 by (Fast_tac 1);
   333 result();
   334 
   335 writeln"Problem 41";
   336 goal HOL.thy "(! z. ? y. ! x. f x y = (f x z & ~ f x x))        \
   337 \              --> ~ (? z. ! x. f x z)";
   338 by (Best_tac 1);
   339 result();
   340 
   341 writeln"Problem 42";
   342 goal HOL.thy "~ (? y. ! x. p x y = (~ (? z. p x z & p z x)))";
   343 by (Deepen_tac 3 1);
   344 result();
   345 
   346 writeln"Problem 43  NOT PROVED AUTOMATICALLY";
   347 goal HOL.thy
   348     "(! x::'a. ! y::'a. q x y = (! z. p z x = (p z y::bool)))   \
   349 \ --> (! x. (! y. q x y = (q y x::bool)))";
   350 
   351 
   352 writeln"Problem 44";
   353 goal HOL.thy "(! x. f(x) -->                                    \
   354 \             (? y. g(y) & h x y & (? y. g(y) & ~ h x y)))  &   \
   355 \             (? x. j(x) & (! y. g(y) --> h x y))               \
   356 \             --> (? x. j(x) & ~f(x))";
   357 by (Fast_tac 1);
   358 result();
   359 
   360 writeln"Problem 45";
   361 goal HOL.thy
   362     "(! x. f(x) & (! y. g(y) & h x y --> j x y) \
   363 \                     --> (! y. g(y) & h x y --> k(y))) &       \
   364 \    ~ (? y. l(y) & k(y)) &                                     \
   365 \    (? x. f(x) & (! y. h x y --> l(y))                         \
   366 \               & (! y. g(y) & h x y --> j x y))                \
   367 \     --> (? x. f(x) & ~ (? y. g(y) & h x y))";
   368 by (Best_tac 1); 
   369 result();
   370 
   371 
   372 writeln"Problems (mainly) involving equality or functions";
   373 
   374 writeln"Problem 48";
   375 goal HOL.thy "(a=b | c=d) & (a=c | b=d) --> a=d | b=c";
   376 by (Fast_tac 1);
   377 result();
   378 
   379 writeln"Problem 49  NOT PROVED AUTOMATICALLY";
   380 (*Hard because it involves substitution for Vars;
   381   the type constraint ensures that x,y,z have the same type as a,b,u. *)
   382 goal HOL.thy "(? x y::'a. ! z. z=x | z=y) & P(a) & P(b) & (~a=b) \
   383 \               --> (! u::'a.P(u))";
   384 by (Classical.safe_tac (!claset));
   385 by (res_inst_tac [("x","a")] allE 1);
   386 by (assume_tac 1);
   387 by (res_inst_tac [("x","b")] allE 1);
   388 by (assume_tac 1);
   389 by (Fast_tac 1);
   390 result();
   391 
   392 writeln"Problem 50";  
   393 (*What has this to do with equality?*)
   394 goal HOL.thy "(! x. P a x | (! y.P x y)) --> (? x. ! y.P x y)";
   395 by (Deepen_tac 1 1);
   396 result();
   397 
   398 writeln"Problem 51";
   399 goal HOL.thy
   400     "(? z w. ! x y. P x y = (x=z & y=w)) -->  \
   401 \    (? z. ! x. ? w. (! y. P x y = (y=w)) = (x=z))";
   402 by (Best_tac 1);
   403 result();
   404 
   405 writeln"Problem 52";
   406 (*Almost the same as 51. *)
   407 goal HOL.thy
   408     "(? z w. ! x y. P x y = (x=z & y=w)) -->  \
   409 \    (? w. ! y. ? z. (! x. P x y = (x=z)) = (y=w))";
   410 by (Best_tac 1);
   411 result();
   412 
   413 writeln"Problem 55";
   414 
   415 (*Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988).
   416   fast_tac DISCOVERS who killed Agatha. *)
   417 goal HOL.thy "lives(agatha) & lives(butler) & lives(charles) & \
   418 \  (killed agatha agatha | killed butler agatha | killed charles agatha) & \
   419 \  (!x y. killed x y --> hates x y & ~richer x y) & \
   420 \  (!x. hates agatha x --> ~hates charles x) & \
   421 \  (hates agatha agatha & hates agatha charles) & \
   422 \  (!x. lives(x) & ~richer x agatha --> hates butler x) & \
   423 \  (!x. hates agatha x --> hates butler x) & \
   424 \  (!x. ~hates x agatha | ~hates x butler | ~hates x charles) --> \
   425 \   killed ?who agatha";
   426 by (Fast_tac 1);
   427 result();
   428 
   429 writeln"Problem 56";
   430 goal HOL.thy
   431     "(! x. (? y. P(y) & x=f(y)) --> P(x)) = (! x. P(x) --> P(f(x)))";
   432 by (Fast_tac 1);
   433 result();
   434 
   435 writeln"Problem 57";
   436 goal HOL.thy
   437     "P (f a b) (f b c) & P (f b c) (f a c) & \
   438 \    (! x y z. P x y & P y z --> P x z)    -->   P (f a b) (f a c)";
   439 by (Fast_tac 1);
   440 result();
   441 
   442 writeln"Problem 58  NOT PROVED AUTOMATICALLY";
   443 goal HOL.thy "(! x y. f(x)=g(y)) --> (! x y. f(f(x))=f(g(y)))";
   444 val f_cong = read_instantiate [("f","f")] arg_cong;
   445 by (fast_tac (!claset addIs [f_cong]) 1);
   446 result();
   447 
   448 writeln"Problem 59";
   449 goal HOL.thy "(! x. P(x) = (~P(f(x)))) --> (? x. P(x) & ~P(f(x)))";
   450 by (Deepen_tac 1 1);
   451 result();
   452 
   453 writeln"Problem 60";
   454 goal HOL.thy
   455     "! x. P x (f x) = (? y. (! z. P z y --> P z (f x)) & P x y)";
   456 by (Fast_tac 1);
   457 result();
   458 
   459 writeln"Problem 62 as corrected in JAR 18 (1997), page 135";
   460 goal HOL.thy
   461     "(ALL x. p a & (p x --> p(f x)) --> p(f(f x)))  =   \
   462 \    (ALL x. (~ p a | p x | p(f(f x))) &                        \
   463 \            (~ p a | ~ p(f x) | p(f(f x))))";
   464 by (Fast_tac 1);
   465 result();
   466 
   467 (*From Rudnicki, Obvious Inferences, JAR 3 (1987), 383-393.  
   468   It does seem obvious!*)
   469 goal Prod.thy
   470     "(ALL x. F(x) & ~G(x) --> (EX y. H(x,y) & J(y))) &        \
   471 \    (EX x. K(x) & F(x) & (ALL y. H(x,y) --> K(y)))  &        \
   472 \    (ALL x. K(x) --> ~G(x))   -->   (EX x. K(x) --> ~G(x))";
   473 by (Fast_tac 1);
   474 result();
   475 
   476 goal Prod.thy
   477     "(ALL x y. R(x,y) | R(y,x)) &                \
   478 \    (ALL x y. S(x,y) & S(y,x) --> x=y) &        \
   479 \    (ALL x y. R(x,y) --> S(x,y))    -->   (ALL x y. S(x,y) --> R(x,y))";
   480 by (Fast_tac 1);
   481 result();
   482 
   483 
   484 
   485 writeln"Reached end of file.";