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