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