src/HOL/ex/mesontest.ML
author paulson
Tue Mar 04 10:21:16 1997 +0100 (1997-03-04)
changeset 2715 79c35a051196
parent 2615 99df9182f5a5
child 3842 b55686a7b22c
permissions -rw-r--r--
Updated reference to Pelletier erratum
     1 (*  Title:      HOL/ex/mesontest
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     5 
     6 Test data for the MESON proof procedure
     7    (Excludes the equality problems 51, 52, 56, 58)
     8 
     9 Use the "mesonlog" shell script to process logs.
    10 
    11 show_hyps := false;
    12 
    13 keep_derivs := MinDeriv;
    14 by (rtac ccontr 1);
    15 val [prem] = gethyps 1;
    16 val nnf = make_nnf prem;
    17 val xsko = skolemize nnf;
    18 by (cut_facts_tac [xsko] 1 THEN REPEAT (etac exE 1));
    19 val [_,sko] = gethyps 1;
    20 val clauses = make_clauses [sko];       
    21 val horns = make_horns clauses;
    22 val goes = gocls clauses;
    23 
    24 goal HOL.thy "False";
    25 by (resolve_tac goes 1);
    26 keep_derivs := FullDeriv;
    27 
    28 by (prolog_step_tac horns 1);
    29 by (iter_deepen_prolog_tac horns);
    30 by (depth_prolog_tac horns);
    31 by (best_prolog_tac size_of_subgoals horns);
    32 *)
    33 
    34 writeln"File HOL/ex/meson-test.";
    35 
    36 (*Deep unifications can be required, esp. during transformation to clauses*)
    37 val orig_trace_bound = !Unify.trace_bound
    38 and orig_search_bound = !Unify.search_bound;
    39 Unify.trace_bound := 20;
    40 Unify.search_bound := 40;
    41 
    42 (**** Interactive examples ****)
    43 
    44 (*Generate nice names for Skolem functions*)
    45 Logic.auto_rename := true; Logic.set_rename_prefix "a";
    46 
    47 
    48 writeln"Problem 25";
    49 goal HOL.thy "(? x. P x) &  \
    50 \       (! x. L x --> ~ (M x & R x)) &  \
    51 \       (! x. P x --> (M x & L x)) &   \
    52 \       ((! x. P x --> Q x) | (? x. P x & R x))  \
    53 \   --> (? x. Q x & P x)";
    54 by (rtac ccontr 1);
    55 val [prem25] = gethyps 1;
    56 val nnf25 = make_nnf prem25;
    57 val xsko25 = skolemize nnf25;
    58 by (cut_facts_tac [xsko25] 1 THEN REPEAT (etac exE 1));
    59 val [_,sko25] = gethyps 1;
    60 val clauses25 = make_clauses [sko25];   (*7 clauses*)
    61 val horns25 = make_horns clauses25;     (*16 Horn clauses*)
    62 val go25::_ = gocls clauses25;
    63 
    64 goal HOL.thy "False";
    65 by (rtac go25 1);
    66 by (depth_prolog_tac horns25);
    67 
    68 
    69 writeln"Problem 26";
    70 goal HOL.thy "((? x. p x) = (? x. q x)) &     \
    71 \     (! x. ! y. p x & q y --> (r x = s y)) \
    72 \ --> ((! x. p x --> r x) = (! x. q x --> s x))";
    73 by (rtac ccontr 1);
    74 val [prem26] = gethyps 1;
    75 val nnf26 = make_nnf prem26;
    76 val xsko26 = skolemize nnf26;
    77 by (cut_facts_tac [xsko26] 1 THEN REPEAT (etac exE 1));
    78 val [_,sko26] = gethyps 1;
    79 val clauses26 = make_clauses [sko26];                   (*9 clauses*)
    80 val horns26 = make_horns clauses26;                     (*24 Horn clauses*)
    81 val go26::_ = gocls clauses26;
    82 
    83 goal HOL.thy "False";
    84 by (rtac go26 1);
    85 by (depth_prolog_tac horns26);  (*1.4 secs*)
    86 (*Proof is of length 107!!*)
    87 
    88 
    89 writeln"Problem 43  NOW PROVED AUTOMATICALLY!!";  (*16 Horn clauses*)
    90 goal HOL.thy "(! x. ! y. q x y = (! z. p z x = (p z y::bool)))  \
    91 \         --> (! x. (! y. q x y = (q y x::bool)))";
    92 by (rtac ccontr 1);
    93 val [prem43] = gethyps 1;
    94 val nnf43 = make_nnf prem43;
    95 val xsko43 = skolemize nnf43;
    96 by (cut_facts_tac [xsko43] 1 THEN REPEAT (etac exE 1));
    97 val [_,sko43] = gethyps 1;
    98 val clauses43 = make_clauses [sko43];   (*6*)
    99 val horns43 = make_horns clauses43;     (*16*)
   100 val go43::_ = gocls clauses43;
   101 
   102 goal HOL.thy "False";
   103 by (rtac go43 1);
   104 by (best_prolog_tac size_of_subgoals horns43);   (*1.6 secs*)
   105 
   106 (* 
   107 #1  (q x xa ==> ~ q x xa) ==> q xa x
   108 #2  (q xa x ==> ~ q xa x) ==> q x xa
   109 #3  (~ q x xa ==> q x xa) ==> ~ q xa x
   110 #4  (~ q xa x ==> q xa x) ==> ~ q x xa
   111 #5  [| ~ q ?U ?V ==> q ?U ?V; ~ p ?W ?U ==> p ?W ?U |] ==> p ?W ?V
   112 #6  [| ~ p ?W ?U ==> p ?W ?U; p ?W ?V ==> ~ p ?W ?V |] ==> ~ q ?U ?V
   113 #7  [| p ?W ?V ==> ~ p ?W ?V; ~ q ?U ?V ==> q ?U ?V |] ==> ~ p ?W ?U
   114 #8  [| ~ q ?U ?V ==> q ?U ?V; ~ p ?W ?V ==> p ?W ?V |] ==> p ?W ?U
   115 #9  [| ~ p ?W ?V ==> p ?W ?V; p ?W ?U ==> ~ p ?W ?U |] ==> ~ q ?U ?V
   116 #10 [| p ?W ?U ==> ~ p ?W ?U; ~ q ?U ?V ==> q ?U ?V |] ==> ~ p ?W ?V
   117 #11 [| p (xb ?U ?V) ?U ==> ~ p (xb ?U ?V) ?U;
   118        p (xb ?U ?V) ?V ==> ~ p (xb ?U ?V) ?V |] ==> q ?U ?V
   119 #12 [| p (xb ?U ?V) ?V ==> ~ p (xb ?U ?V) ?V; q ?U ?V ==> ~ q ?U ?V |] ==>
   120     p (xb ?U ?V) ?U
   121 #13 [| q ?U ?V ==> ~ q ?U ?V; p (xb ?U ?V) ?U ==> ~ p (xb ?U ?V) ?U |] ==>
   122     p (xb ?U ?V) ?V
   123 #14 [| ~ p (xb ?U ?V) ?U ==> p (xb ?U ?V) ?U;
   124        ~ p (xb ?U ?V) ?V ==> p (xb ?U ?V) ?V |] ==> q ?U ?V
   125 #15 [| ~ p (xb ?U ?V) ?V ==> p (xb ?U ?V) ?V; q ?U ?V ==> ~ q ?U ?V |] ==>
   126     ~ p (xb ?U ?V) ?U
   127 #16 [| q ?U ?V ==> ~ q ?U ?V; ~ p (xb ?U ?V) ?U ==> p (xb ?U ?V) ?U |] ==>
   128     ~ p (xb ?U ?V) ?V
   129 
   130 And here is the proof!  (Unkn is the start state after use of goal clause)
   131 [Unkn, Res ([Thm "#14"], false, 1), Res ([Thm "#5"], false, 1),
   132    Res ([Thm "#1"], false, 1), Asm 1, Res ([Thm "#13"], false, 1), Asm 2,
   133    Asm 1, Res ([Thm "#13"], false, 1), Asm 1, Res ([Thm "#10"], false, 1),
   134    Res ([Thm "#16"], false, 1), Asm 2, Asm 1, Res ([Thm "#1"], false, 1),
   135    Asm 1, Res ([Thm "#14"], false, 1), Res ([Thm "#5"], false, 1),
   136    Res ([Thm "#2"], false, 1), Asm 1, Res ([Thm "#13"], false, 1), Asm 2,
   137    Asm 1, Res ([Thm "#8"], false, 1), Res ([Thm "#2"], false, 1), Asm 1,
   138    Res ([Thm "#12"], false, 1), Asm 2, Asm 1] : lderiv list
   139 *)
   140 
   141 
   142 (*Restore variable name preservation*)
   143 Logic.auto_rename := false; 
   144 
   145 
   146 (**** Batch test data ****)
   147 
   148 (*Sample problems from 
   149   F. J. Pelletier, 
   150   Seventy-Five Problems for Testing Automatic Theorem Provers,
   151   J. Automated Reasoning 2 (1986), 191-216.
   152   Errata, JAR 4 (1988), 236-236.
   153 
   154 The hardest problems -- judging by experience with several theorem provers,
   155 including matrix ones -- are 34 and 43.
   156 *)
   157 
   158 writeln"Pelletier's examples";
   159 (*1*)
   160 goal HOL.thy "(P --> Q)  =  (~Q --> ~P)";
   161 by (safe_meson_tac 1);
   162 result();
   163 
   164 (*2*)
   165 goal HOL.thy "(~ ~ P) =  P";
   166 by (safe_meson_tac 1);
   167 result();
   168 
   169 (*3*)
   170 goal HOL.thy "~(P-->Q) --> (Q-->P)";
   171 by (safe_meson_tac 1);
   172 result();
   173 
   174 (*4*)
   175 goal HOL.thy "(~P-->Q)  =  (~Q --> P)";
   176 by (safe_meson_tac 1);
   177 result();
   178 
   179 (*5*)
   180 goal HOL.thy "((P|Q)-->(P|R)) --> (P|(Q-->R))";
   181 by (safe_meson_tac 1);
   182 result();
   183 
   184 (*6*)
   185 goal HOL.thy "P | ~ P";
   186 by (safe_meson_tac 1);
   187 result();
   188 
   189 (*7*)
   190 goal HOL.thy "P | ~ ~ ~ P";
   191 by (safe_meson_tac 1);
   192 result();
   193 
   194 (*8.  Peirce's law*)
   195 goal HOL.thy "((P-->Q) --> P)  -->  P";
   196 by (safe_meson_tac 1);
   197 result();
   198 
   199 (*9*)
   200 goal HOL.thy "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
   201 by (safe_meson_tac 1);
   202 result();
   203 
   204 (*10*)
   205 goal HOL.thy "(Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P=Q)";
   206 by (safe_meson_tac 1);
   207 result();
   208 
   209 (*11.  Proved in each direction (incorrectly, says Pelletier!!)  *)
   210 goal HOL.thy "P=(P::bool)";
   211 by (safe_meson_tac 1);
   212 result();
   213 
   214 (*12.  "Dijkstra's law"*)
   215 goal HOL.thy "((P = Q) = R) = (P = (Q = R))";
   216 by (safe_meson_tac 1);
   217 result();
   218 
   219 (*13.  Distributive law*)
   220 goal HOL.thy "(P | (Q & R)) = ((P | Q) & (P | R))";
   221 by (safe_meson_tac 1);
   222 result();
   223 
   224 (*14*)
   225 goal HOL.thy "(P = Q) = ((Q | ~P) & (~Q|P))";
   226 by (safe_meson_tac 1);
   227 result();
   228 
   229 (*15*)
   230 goal HOL.thy "(P --> Q) = (~P | Q)";
   231 by (safe_meson_tac 1);
   232 result();
   233 
   234 (*16*)
   235 goal HOL.thy "(P-->Q) | (Q-->P)";
   236 by (safe_meson_tac 1);
   237 result();
   238 
   239 (*17*)
   240 goal HOL.thy "((P & (Q-->R))-->S)  =  ((~P | Q | S) & (~P | ~R | S))";
   241 by (safe_meson_tac 1);
   242 result();
   243 
   244 writeln"Classical Logic: examples with quantifiers";
   245 
   246 goal HOL.thy "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))";
   247 by (safe_meson_tac 1);
   248 result(); 
   249 
   250 goal HOL.thy "(? x. P --> Q x)  =  (P --> (? x.Q x))";
   251 by (safe_meson_tac 1);
   252 result(); 
   253 
   254 goal HOL.thy "(? x.P x --> Q) = ((! x.P x) --> Q)";
   255 by (safe_meson_tac 1);
   256 result(); 
   257 
   258 goal HOL.thy "((! x.P x) | Q)  =  (! x. P x | Q)";
   259 by (safe_meson_tac 1);
   260 result(); 
   261 
   262 goal HOL.thy "(! x. P x --> P(f x))  &  P d --> P(f(f(f d)))";
   263 by (safe_meson_tac 1);
   264 result();
   265 
   266 (*Needs double instantiation of EXISTS*)
   267 goal HOL.thy "? x. P x --> P a & P b";
   268 by (safe_meson_tac 1);
   269 result();
   270 
   271 goal HOL.thy "? z. P z --> (! x. P x)";
   272 by (safe_meson_tac 1);
   273 result();
   274 
   275 writeln"Hard examples with quantifiers";
   276 
   277 writeln"Problem 18";
   278 goal HOL.thy "? y. ! x. P y --> P x";
   279 by (safe_meson_tac 1);
   280 result(); 
   281 
   282 writeln"Problem 19";
   283 goal HOL.thy "? x. ! y z. (P y --> Q z) --> (P x --> Q x)";
   284 by (safe_meson_tac 1);
   285 result();
   286 
   287 writeln"Problem 20";
   288 goal HOL.thy "(! x y. ? z. ! w. (P x & Q y --> R z & S w))     \
   289 \   --> (? x y. P x & Q y) --> (? z. R z)";
   290 by (safe_meson_tac 1); 
   291 result();
   292 
   293 writeln"Problem 21";
   294 goal HOL.thy "(? x. P --> Q x) & (? x. Q x --> P) --> (? x. P=Q x)";
   295 by (safe_meson_tac 1); 
   296 result();
   297 
   298 writeln"Problem 22";
   299 goal HOL.thy "(! x. P = Q x)  -->  (P = (! x. Q x))";
   300 by (safe_meson_tac 1); 
   301 result();
   302 
   303 writeln"Problem 23";
   304 goal HOL.thy "(! x. P | Q x)  =  (P | (! x. Q x))";
   305 by (safe_meson_tac 1);  
   306 result();
   307 
   308 writeln"Problem 24";  (*The first goal clause is useless*)
   309 goal HOL.thy "~(? x. S x & Q x) & (! x. P x --> Q x | R x) &  \
   310 \    (~(? x.P x) --> (? x.Q x)) & (! x. Q x | R x --> S x)  \
   311 \   --> (? x. P x & R x)";
   312 by (safe_meson_tac 1); 
   313 result();
   314 
   315 writeln"Problem 25";
   316 goal HOL.thy "(? x. P x) &  \
   317 \       (! x. L x --> ~ (M x & R x)) &  \
   318 \       (! x. P x --> (M x & L x)) &   \
   319 \       ((! x. P x --> Q x) | (? x. P x & R x))  \
   320 \   --> (? x. Q x & P x)";
   321 by (safe_meson_tac 1); 
   322 result();
   323 
   324 writeln"Problem 26";  (*24 Horn clauses*)
   325 goal HOL.thy "((? x. p x) = (? x. q x)) &     \
   326 \     (! x. ! y. p x & q y --> (r x = s y)) \
   327 \ --> ((! x. p x --> r x) = (! x. q x --> s x))";
   328 by (safe_meson_tac 1); 
   329 result();
   330 
   331 writeln"Problem 27";    (*13 Horn clauses*)
   332 goal HOL.thy "(? x. P x & ~Q x) &   \
   333 \             (! x. P x --> R x) &   \
   334 \             (! x. M x & L x --> P x) &   \
   335 \             ((? x. R x & ~ Q x) --> (! x. L x --> ~ R x))  \
   336 \         --> (! x. M x --> ~L x)";
   337 by (safe_meson_tac 1); 
   338 result();
   339 
   340 writeln"Problem 28.  AMENDED";  (*14 Horn clauses*)
   341 goal HOL.thy "(! x. P x --> (! x. Q x)) &   \
   342 \       ((! x. Q x | R x) --> (? x. Q x & S x)) &  \
   343 \       ((? x.S x) --> (! x. L x --> M x))  \
   344 \   --> (! x. P x & L x --> M x)";
   345 by (safe_meson_tac 1);  
   346 result();
   347 
   348 writeln"Problem 29.  Essentially the same as Principia Mathematica *11.71";
   349         (*62 Horn clauses*)
   350 goal HOL.thy "(? x. F x) & (? y. G y)  \
   351 \   --> ( ((! x. F x --> H x) & (! y. G y --> J y))  =   \
   352 \         (! x y. F x & G y --> H x & J y))";
   353 by (safe_meson_tac 1);          (*0.7 secs*)
   354 result();
   355 
   356 writeln"Problem 30";
   357 goal HOL.thy "(! x. P x | Q x --> ~ R x) & \
   358 \       (! x. (Q x --> ~ S x) --> P x & R x)  \
   359 \   --> (! x. S x)";
   360 by (safe_meson_tac 1);  
   361 result();
   362 
   363 writeln"Problem 31";  (*10 Horn clauses; first negative clauses is useless*)
   364 goal HOL.thy "~(? x.P x & (Q x | R x)) & \
   365 \       (? x. L x & P x) & \
   366 \       (! x. ~ R x --> M x)  \
   367 \   --> (? x. L x & M x)";
   368 by (safe_meson_tac 1);
   369 result();
   370 
   371 writeln"Problem 32";
   372 goal HOL.thy "(! x. P x & (Q x | R x)-->S x) & \
   373 \       (! x. S x & R x --> L x) & \
   374 \       (! x. M x --> R x)  \
   375 \   --> (! x. P x & M x --> L x)";
   376 by (safe_meson_tac 1);
   377 result();
   378 
   379 writeln"Problem 33";  (*55 Horn clauses*)
   380 goal HOL.thy "(! x. P a & (P x --> P b)-->P c)  =    \
   381 \    (! x. (~P a | P x | P c) & (~P a | ~P b | P c))";
   382 by (safe_meson_tac 1);          (*5.6 secs*)
   383 result();
   384 
   385 writeln"Problem 34  AMENDED (TWICE!!)"; (*924 Horn clauses*)
   386 (*Andrews's challenge*)
   387 goal HOL.thy "((? x. ! y. p x = p y)  =               \
   388 \              ((? x. q x) = (! y. p y)))     =       \
   389 \             ((? x. ! y. q x = q y)  =               \
   390 \              ((? x. p x) = (! y. q y)))";
   391 by (safe_meson_tac 1);          (*13 secs*)
   392 result();
   393 
   394 writeln"Problem 35";
   395 goal HOL.thy "? x y. P x y -->  (! u v. P u v)";
   396 by (safe_meson_tac 1);
   397 result();
   398 
   399 writeln"Problem 36";  (*15 Horn clauses*)
   400 goal HOL.thy "(! x. ? y. J x y) & \
   401 \       (! x. ? y. G x y) & \
   402 \       (! x y. J x y | G x y -->       \
   403 \       (! z. J y z | G y z --> H x z))   \
   404 \   --> (! x. ? y. H x y)";
   405 by (safe_meson_tac 1);
   406 result();
   407 
   408 writeln"Problem 37";  (*10 Horn clauses*)
   409 goal HOL.thy "(! z. ? w. ! x. ? y. \
   410 \          (P x z --> P y w) & P y z & (P y w --> (? u.Q u w))) & \
   411 \       (! x z. ~P x z --> (? y. Q y z)) & \
   412 \       ((? x y. Q x y) --> (! x. R x x))  \
   413 \   --> (! x. ? y. R x y)";
   414 by (safe_meson_tac 1);   (*causes unification tracing messages*)
   415 result();
   416 
   417 writeln"Problem 38";  (*Quite hard: 422 Horn clauses!!*)
   418 goal HOL.thy
   419     "(! x. p a & (p x --> (? y. p y & r x y)) -->            \
   420 \          (? z. ? w. p z & r x w & r w z))  =                 \
   421 \    (! x. (~p a | p x | (? z. ? w. p z & r x w & r w z)) &  \
   422 \          (~p a | ~(? y. p y & r x y) |                      \
   423 \           (? z. ? w. p z & r x w & r w z)))";
   424 by (safe_best_meson_tac 1);  (*10 secs; iter. deepening is slightly slower*)
   425 result();
   426 
   427 writeln"Problem 39";
   428 goal HOL.thy "~ (? x. ! y. F y x = (~F y y))";
   429 by (safe_meson_tac 1);
   430 result();
   431 
   432 writeln"Problem 40.  AMENDED";
   433 goal HOL.thy "(? y. ! x. F x y = F x x)  \
   434 \       -->  ~ (! x. ? y. ! z. F z y = (~F z x))";
   435 by (safe_meson_tac 1);
   436 result();
   437 
   438 writeln"Problem 41";
   439 goal HOL.thy "(! z. (? y. (! x. f x y = (f x z & ~ f x x))))    \
   440 \              --> ~ (? z. ! x. f x z)";
   441 by (safe_meson_tac 1);
   442 result();
   443 
   444 writeln"Problem 42";
   445 goal HOL.thy "~ (? y. ! x. p x y = (~ (? z. p x z & p z x)))";
   446 by (safe_meson_tac 1);
   447 result();
   448 
   449 writeln"Problem 43  NOW PROVED AUTOMATICALLY!!";
   450 goal HOL.thy "(! x. ! y. q x y = (! z. p z x = (p z y::bool)))  \
   451 \         --> (! x. (! y. q x y = (q y x::bool)))";
   452 by (safe_best_meson_tac 1);     
   453 (*1.6 secs; iter. deepening is slightly slower*)
   454 result();
   455 
   456 writeln"Problem 44";  (*13 Horn clauses; 7-step proof*)
   457 goal HOL.thy "(! x. f x -->                                    \
   458 \             (? y. g y & h x y & (? y. g y & ~ h x y)))  &   \
   459 \             (? x. j x & (! y. g y --> h x y))               \
   460 \             --> (? x. j x & ~f x)";
   461 by (safe_meson_tac 1);
   462 result();
   463 
   464 writeln"Problem 45";  (*27 Horn clauses; 54-step proof*)
   465 goal HOL.thy "(! x. f x & (! y. g y & h x y --> j x y)        \
   466 \                     --> (! y. g y & h x y --> k y)) &       \
   467 \     ~ (? y. l y & k y) &                                    \
   468 \     (? x. f x & (! y. h x y --> l y)                        \
   469 \                  & (! y. g y & h x y --> j x y))             \
   470 \     --> (? x. f x & ~ (? y. g y & h x y))";
   471 by (safe_best_meson_tac 1);     
   472 (*1.6 secs; iter. deepening is slightly slower*)
   473 result();
   474 
   475 writeln"Problem 46";  (*26 Horn clauses; 21-step proof*)
   476 goal HOL.thy
   477     "(! x. f x & (! y. f y & h y x --> g y) --> g x) &      \
   478 \    ((? x.f x & ~g x) -->                                    \
   479 \     (? x. f x & ~g x & (! y. f y & ~g y --> j x y))) &    \
   480 \    (! x y. f x & f y & h x y --> ~j y x)                    \
   481 \     --> (! x. f x --> g x)";
   482 by (safe_best_meson_tac 1);     
   483 (*1.7 secs; iter. deepening is slightly slower*)
   484 result();
   485 
   486 writeln"Problem 47.  Schubert's Steamroller";
   487         (*26 clauses; 63 Horn clauses*)
   488 goal HOL.thy
   489     "(! x. P1 x --> P0 x) & (? x.P1 x) &     \
   490 \    (! x. P2 x --> P0 x) & (? x.P2 x) &     \
   491 \    (! x. P3 x --> P0 x) & (? x.P3 x) &     \
   492 \    (! x. P4 x --> P0 x) & (? x.P4 x) &     \
   493 \    (! x. P5 x --> P0 x) & (? x.P5 x) &     \
   494 \    (! x. Q1 x --> Q0 x) & (? x.Q1 x) &     \
   495 \    (! x. P0 x --> ((! y.Q0 y-->R x y) |    \
   496 \                     (! y.P0 y & S y x &     \
   497 \                          (? z.Q0 z&R y z) --> R x y))) &   \
   498 \    (! x y. P3 y & (P5 x|P4 x) --> S x y) &        \
   499 \    (! x y. P3 x & P2 y --> S x y) &        \
   500 \    (! x y. P2 x & P1 y --> S x y) &        \
   501 \    (! x y. P1 x & (P2 y|Q1 y) --> ~R x y) &       \
   502 \    (! x y. P3 x & P4 y --> R x y) &        \
   503 \    (! x y. P3 x & P5 y --> ~R x y) &       \
   504 \    (! x. (P4 x|P5 x) --> (? y.Q0 y & R x y))      \
   505 \    --> (? x y. P0 x & P0 y & (? z. Q1 z & R y z & R x y))";
   506 by (safe_meson_tac 1);   (*119 secs*)
   507 result();
   508 
   509 (*The Los problem?  Circulated by John Harrison*)
   510 goal HOL.thy "(! x y z. P x y & P y z --> P x z) &      \
   511 \      (! x y z. Q x y & Q y z --> Q x z) &             \
   512 \      (! x y. P x y --> P y x) &                       \
   513 \      (! x y. P x y | Q x y)                           \
   514 \      --> (! x y. P x y) | (! x y. Q x y)";
   515 by (safe_best_meson_tac 1);     (*2.3 secs; iter. deepening is VERY slow*)
   516 result();
   517 
   518 (*A similar example, suggested by Johannes Schumann and credited to Pelletier*)
   519 goal HOL.thy "(!x y z. P x y --> P y z --> P x z) --> \
   520 \       (!x y z. Q x y --> Q y z --> Q x z) --> \
   521 \       (!x y.Q x y --> Q y x) -->  (!x y. P x y | Q x y) --> \
   522 \       (!x y.P x y) | (!x y.Q x y)";
   523 by (safe_best_meson_tac 1);          (*2.7 secs*)
   524 result();
   525 
   526 writeln"Problem 50";  
   527 (*What has this to do with equality?*)
   528 goal HOL.thy "(! x. P a x | (! y.P x y)) --> (? x. ! y.P x y)";
   529 by (safe_meson_tac 1);
   530 result();
   531 
   532 writeln"Problem 55";
   533 
   534 (*Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988).
   535   meson_tac cannot report who killed Agatha. *)
   536 goal HOL.thy "lives agatha & lives butler & lives charles & \
   537 \  (killed agatha agatha | killed butler agatha | killed charles agatha) & \
   538 \  (!x y. killed x y --> hates x y & ~richer x y) & \
   539 \  (!x. hates agatha x --> ~hates charles x) & \
   540 \  (hates agatha agatha & hates agatha charles) & \
   541 \  (!x. lives x & ~richer x agatha --> hates butler x) & \
   542 \  (!x. hates agatha x --> hates butler x) & \
   543 \  (!x. ~hates x agatha | ~hates x butler | ~hates x charles) --> \
   544 \  (? x. killed x agatha)";
   545 by (safe_meson_tac 1);
   546 result();
   547 
   548 writeln"Problem 57";
   549 goal HOL.thy
   550     "P (f a b) (f b c) & P (f b c) (f a c) & \
   551 \    (! x y z. P x y & P y z --> P x z)    -->   P (f a b) (f a c)";
   552 by (safe_meson_tac 1);
   553 result();
   554 
   555 writeln"Problem 58";
   556 (* Challenge found on info-hol *)
   557 goal HOL.thy
   558     "! P Q R x. ? v w. ! y z. P x & Q y --> (P v | R w) & (R z --> Q v)";
   559 by (safe_meson_tac 1);
   560 result();
   561 
   562 writeln"Problem 59";
   563 goal HOL.thy "(! x. P x = (~P(f x))) --> (? x. P x & ~P(f x))";
   564 by (safe_meson_tac 1);
   565 result();
   566 
   567 writeln"Problem 60";
   568 goal HOL.thy "! x. P x (f x) = (? y. (! z. P z y --> P z (f x)) & P x y)";
   569 by (safe_meson_tac 1);
   570 result();
   571 
   572 writeln"Problem 62 as corrected in JAR 18 (1997), page 135";
   573 goal HOL.thy
   574     "(ALL x. p a & (p x --> p(f x)) --> p(f(f x)))  =   \
   575 \    (ALL x. (~ p a | p x | p(f(f x))) &                        \
   576 \            (~ p a | ~ p(f x) | p(f(f x))))";
   577 by (safe_meson_tac 1);
   578 result();
   579 
   580 
   581 (** Charles Morgan's problems **)
   582 
   583 val axa = "! x y.   T(i x(i y x))";
   584 val axb = "! x y z. T(i(i x(i y z))(i(i x y)(i x z)))";
   585 val axc = "! x y.   T(i(i(n x)(n y))(i y x))";
   586 val axd = "! x y.   T(i x y) & T x --> T y";
   587 
   588 fun axjoin ([],   q) = q
   589   | axjoin (p::ps, q) = "(" ^ p ^ ") --> (" ^ axjoin(ps,q) ^ ")";
   590 
   591 goal HOL.thy (axjoin([axa,axb,axd], "! x. T(i x x)"));
   592 by (safe_meson_tac 1);  
   593 result();
   594 
   595 writeln"Problem 66";  
   596 goal HOL.thy (axjoin([axa,axb,axc,axd], "! x. T(i x(n(n x)))"));
   597 (*TOO SLOW: more than 24 minutes!
   598 by (safe_meson_tac 1);
   599 result();
   600 *)
   601 
   602 writeln"Problem 67";  
   603 goal HOL.thy (axjoin([axa,axb,axc,axd], "! x. T(i(n(n x)) x)"));
   604 (*TOO SLOW: more than 3 minutes!
   605 by (safe_meson_tac 1);
   606 result();
   607 *)
   608 
   609 
   610 (*Restore original values*)
   611 Unify.trace_bound := orig_trace_bound;
   612 Unify.search_bound := orig_search_bound;
   613 
   614 writeln"Reached end of file.";
   615 
   616 (*26 August 1992: loaded in 277 secs.  New Jersey v 75*)