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