ex/unsolved.ML
author clasohm
Wed, 02 Mar 1994 12:26:55 +0100
changeset 48 21291189b51e
parent 0 7949f97df77a
permissions -rw-r--r--
changed "." to "$" and Cons to infix "#" to eliminate ambiguity
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	HOL/ex/unsolved
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1992  University of Cambridge
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     5
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     6
Problems that currently defeat the MESON procedure as well as best_tac
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     7
*)
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     8
7949f97df77a Initial revision
clasohm
parents:
diff changeset
     9
(*from Vladimir Lifschitz, What Is the Inverse Method?, JAR 5 (1989), 1--23*)
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    10
goal HOL.thy "? x x'. ! y. ? z z'. (~P(y,y) | P(x,x) | ~S(z,x)) & \
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    11
\                                       (S(x,y) | ~S(y,z) | Q(z',z'))  & \
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    12
\                                       (Q(x',y) | ~Q(y,z') | S(x',x'))";
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    13
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    14
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    15
writeln"Problem 47  Schubert's Steamroller";
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    16
goal HOL.thy
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    17
    "(! x. P1(x) --> P0(x)) & (? x.P1(x)) &	\
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    18
\    (! x. P2(x) --> P0(x)) & (? x.P2(x)) &	\
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    19
\    (! x. P3(x) --> P0(x)) & (? x.P3(x)) &	\
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    20
\    (! x. P4(x) --> P0(x)) & (? x.P4(x)) &	\
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    21
\    (! x. P5(x) --> P0(x)) & (? x.P5(x)) &	\
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    22
\    (! x. Q1(x) --> Q0(x)) & (? x.Q1(x)) &	\
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    23
\    (! x. P0(x) --> ((! y.Q0(y)-->R(x,y)) | 	\
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    24
\		      (! y.P0(y) & S(y,x) & 	\
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    25
\		           (? z.Q0(z)&R(y,z)) --> R(x,y)))) &	\
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    26
\    (! x y. P3(y) & (P5(x)|P4(x)) --> S(x,y)) &	\
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    27
\    (! x y. P3(x) & P2(y) --> S(x,y)) &	\
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    28
\    (! x y. P2(x) & P1(y) --> S(x,y)) &	\
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    29
\    (! x y. P1(x) & (P2(y)|Q1(y)) --> ~R(x,y)) &	\
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    30
\    (! x y. P3(x) & P4(y) --> R(x,y)) &	\
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    31
\    (! x y. P3(x) & P5(y) --> ~R(x,y)) &	\
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    32
\    (! x. (P4(x)|P5(x)) --> (? y.Q0(y) & R(x,y)))	\
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    33
\    --> (? x y. P0(x) & P0(y) & (? z. Q1(z) & R(y,z) & R(x,y)))";
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    34
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    35
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    36
writeln"Problem 55";
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    37
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    38
(*Original, equational version by Len Schubert, via Pelletier *)
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    39
goal HOL.thy
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    40
  "(? x. lives(x) & killed(x,agatha)) & \
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    41
\  lives(agatha) & lives(butler) & lives(charles) & \
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    42
\  (! x. lives(x) --> x=agatha | x=butler | x=charles) & \
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    43
\  (! x y. killed(x,y) --> hates(x,y)) & \
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    44
\  (! x y. killed(x,y) --> ~richer(x,y)) & \
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    45
\  (! x. hates(agatha,x) --> ~hates(charles,x)) & \
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    46
\  (! x. ~ x=butler --> hates(agatha,x)) & \
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    47
\  (! x. ~richer(x,agatha) --> hates(butler,x)) & \
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    48
\  (! x. hates(agatha,x) --> hates(butler,x)) & \
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    49
\  (! x. ? y. ~hates(x,y)) & \
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    50
\  ~ agatha=butler --> \
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    51
\  killed(agatha,agatha)";
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    52
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    53
(** Charles Morgan's problems **)
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    54
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    55
val axa = "! x y.   T(i(x, i(y,x)))";
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    56
val axb = "! x y z. T(i(i(x, i(y,z)), i(i(x,y), i(x,z))))";
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    57
val axc = "! x y.   T(i(i(n(x), n(y)), i(y,x)))";
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    58
val axd = "! x y.   T(i(x,y)) & T(x) --> T(y)";
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    59
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    60
fun axjoin ([],   q) = q
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    61
  | axjoin(p::ps, q) = "(" ^ p ^ ") --> (" ^ axjoin(ps,q) ^ ")";
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    62
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    63
goal HOL.thy (axjoin([axa,axb,axd], "! x. T(i(x,x))"));
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    64
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    65
writeln"Problem 66";
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    66
goal HOL.thy (axjoin([axa,axb,axc,axd], "! x. T(i(x, n(n(x))))"));
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    67
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    68
writeln"Problem 67";
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    69
goal HOL.thy (axjoin([axa,axb,axc,axd], "! x. T(i(n(n(x)), x))"));
7949f97df77a Initial revision
clasohm
parents:
diff changeset
    70