isabelle: src/HOL/ex/mesontest.ML@79c35a051196

     1 (*  Title:      HOL/ex/mesontest

     2     ID:         $Id$

     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

     4     Copyright   1992  University of Cambridge

     6 Test data for the MESON proof procedure

     7    (Excludes the equality problems 51, 52, 56, 58)

     9 Use the "mesonlog" shell script to process logs.

    11 show_hyps := false;

    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;

    24 goal HOL.thy "False";

    25 by (resolve_tac goes 1);

    26 keep_derivs := FullDeriv;

    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 *)

    34 writeln"File HOL/ex/meson-test.";

    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;

    42 (**** Interactive examples ****)

    44 (*Generate nice names for Skolem functions*)

    45 Logic.auto_rename := true; Logic.set_rename_prefix "a";

    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;

    64 goal HOL.thy "False";

    65 by (rtac go25 1);

    66 by (depth_prolog_tac horns25);

    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;

    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!!*)

    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;

   102 goal HOL.thy "False";

   103 by (rtac go43 1);

   104 by (best_prolog_tac size_of_subgoals horns43);   (*1.6 secs*)

   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

   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 *)

   142 (*Restore variable name preservation*)

   143 Logic.auto_rename := false;

   146 (**** Batch test data ****)

   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.

   154 The hardest problems -- judging by experience with several theorem provers,

   155 including matrix ones -- are 34 and 43.

   156 *)

   158 writeln"Pelletier's examples";

   159 (*1*)

   160 goal HOL.thy "(P --> Q)  =  (~Q --> ~P)";

   161 by (safe_meson_tac 1);

   162 result();

   164 (*2*)

   165 goal HOL.thy "(~ ~ P) =  P";

   166 by (safe_meson_tac 1);

   167 result();

   169 (*3*)

   170 goal HOL.thy "~(P-->Q) --> (Q-->P)";

   171 by (safe_meson_tac 1);

   172 result();

   174 (*4*)

   175 goal HOL.thy "(~P-->Q)  =  (~Q --> P)";

   176 by (safe_meson_tac 1);

   177 result();

   179 (*5*)

   180 goal HOL.thy "((P|Q)-->(P|R)) --> (P|(Q-->R))";

   181 by (safe_meson_tac 1);

   182 result();

   184 (*6*)

   185 goal HOL.thy "P | ~ P";

   186 by (safe_meson_tac 1);

   187 result();

   189 (*7*)

   190 goal HOL.thy "P | ~ ~ ~ P";

   191 by (safe_meson_tac 1);

   192 result();

   194 (*8.  Peirce's law*)

   195 goal HOL.thy "((P-->Q) --> P)  -->  P";

   196 by (safe_meson_tac 1);

   197 result();

   199 (*9*)

   200 goal HOL.thy "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";

   201 by (safe_meson_tac 1);

   202 result();

   204 (*10*)

   205 goal HOL.thy "(Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P=Q)";

   206 by (safe_meson_tac 1);

   207 result();

   209 (*11.  Proved in each direction (incorrectly, says Pelletier!!)  *)

   210 goal HOL.thy "P=(P::bool)";

   211 by (safe_meson_tac 1);

   212 result();

   214 (*12.  "Dijkstra's law"*)

   215 goal HOL.thy "((P = Q) = R) = (P = (Q = R))";

   216 by (safe_meson_tac 1);

   217 result();

   219 (*13.  Distributive law*)

   220 goal HOL.thy "(P | (Q & R)) = ((P | Q) & (P | R))";

   221 by (safe_meson_tac 1);

   222 result();

   224 (*14*)

   225 goal HOL.thy "(P = Q) = ((Q | ~P) & (~Q|P))";

   226 by (safe_meson_tac 1);

   227 result();

   229 (*15*)

   230 goal HOL.thy "(P --> Q) = (~P | Q)";

   231 by (safe_meson_tac 1);

   232 result();

   234 (*16*)

   235 goal HOL.thy "(P-->Q) | (Q-->P)";

   236 by (safe_meson_tac 1);

   237 result();

   239 (*17*)

   240 goal HOL.thy "((P & (Q-->R))-->S)  =  ((~P | Q | S) & (~P | ~R | S))";

   241 by (safe_meson_tac 1);

   242 result();

   244 writeln"Classical Logic: examples with quantifiers";

   246 goal HOL.thy "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))";

   247 by (safe_meson_tac 1);

   248 result();

   250 goal HOL.thy "(? x. P --> Q x)  =  (P --> (? x.Q x))";

   251 by (safe_meson_tac 1);

   252 result();

   254 goal HOL.thy "(? x.P x --> Q) = ((! x.P x) --> Q)";

   255 by (safe_meson_tac 1);

   256 result();

   258 goal HOL.thy "((! x.P x) | Q)  =  (! x. P x | Q)";

   259 by (safe_meson_tac 1);

   260 result();

   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();

   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();

   271 goal HOL.thy "? z. P z --> (! x. P x)";

   272 by (safe_meson_tac 1);

   273 result();

   275 writeln"Hard examples with quantifiers";

   277 writeln"Problem 18";

   278 goal HOL.thy "? y. ! x. P y --> P x";

   279 by (safe_meson_tac 1);

   280 result();

   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();

   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();

   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();

   298 writeln"Problem 22";

   299 goal HOL.thy "(! x. P = Q x)  -->  (P = (! x. Q x))";

   300 by (safe_meson_tac 1);

   301 result();

   303 writeln"Problem 23";

   304 goal HOL.thy "(! x. P | Q x)  =  (P | (! x. Q x))";

   305 by (safe_meson_tac 1);

   306 result();

   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();

   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();

   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();

   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();

   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();

   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();

   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();

   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();

   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();

   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();

   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();

   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();

   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();

   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();

   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();

   427 writeln"Problem 39";

   428 goal HOL.thy "~ (? x. ! y. F y x = (~F y y))";

   429 by (safe_meson_tac 1);

   430 result();

   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();

   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();

   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();

   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();

   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();

   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();

   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();

   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();

   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();

   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();

   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();

   532 writeln"Problem 55";

   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();

   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();

   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();

   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();

   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();

   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();

   581 (** Charles Morgan's problems **)

   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";

   588 fun axjoin ([],   q) = q

   589   | axjoin (p::ps, q) = "(" ^ p ^ ") --> (" ^ axjoin(ps,q) ^ ")";

   591 goal HOL.thy (axjoin([axa,axb,axd], "! x. T(i x x)"));

   592 by (safe_meson_tac 1);

   593 result();

   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 *)

   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 *)

   610 (*Restore original values*)

   611 Unify.trace_bound := orig_trace_bound;

   612 Unify.search_bound := orig_search_bound;

   614 writeln"Reached end of file.";

   616 (*26 August 1992: loaded in 277 secs.  New Jersey v 75*)

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--