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