src/HOL/ex/unsolved.ML
author paulson
Wed Nov 05 13:23:46 1997 +0100 (1997-11-05)
changeset 4153 e534c4c32d54
parent 2031 03a843f0f447
permissions -rw-r--r--
Ran expandshort, especially to introduce Safe_tac
clasohm@1465
     1
(*  Title:      HOL/ex/unsolved
clasohm@969
     2
    ID:         $Id$
clasohm@1465
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@969
     4
    Copyright   1992  University of Cambridge
clasohm@969
     5
clasohm@969
     6
Problems that currently defeat the MESON procedure as well as best_tac
clasohm@969
     7
*)
clasohm@969
     8
paulson@1586
     9
(*from Vladimir Lifschitz, What Is the Inverse Method?, JAR 5  1989.  1--23*)
paulson@2031
    10
        (*27 clauses; 81 Horn clauses*)
paulson@1586
    11
goal HOL.thy "? x x'. ! y. ? z z'. (~P y y | P x x | ~S z x) & \
paulson@1586
    12
\                                  (S x y | ~S y z | Q z' z')  & \
paulson@1586
    13
\                                  (Q x' y | ~Q y z' | S x' x')";
clasohm@969
    14
clasohm@969
    15
clasohm@969
    16
clasohm@969
    17
writeln"Problem 55";
clasohm@969
    18
paulson@1586
    19
(*Original, equational version by Len Schubert [via Pelletier] *)
clasohm@969
    20
goal HOL.thy
paulson@1586
    21
  "(? x. lives x & killed x agatha) & \
paulson@1586
    22
\  lives agatha & lives butler & lives charles & \
paulson@1586
    23
\  (! x. lives x --> x=agatha | x=butler | x=charles) & \
paulson@1586
    24
\  (! x y. killed x y --> hates x y) & \
paulson@1586
    25
\  (! x y. killed x y --> ~richer x y) & \
paulson@1586
    26
\  (! x. hates agatha x --> ~hates charles x) & \
paulson@1586
    27
\  (! x. ~ x=butler --> hates agatha x) & \
paulson@1586
    28
\  (! x. ~richer x agatha --> hates butler x) & \
paulson@1586
    29
\  (! x. hates agatha x --> hates butler x) & \
paulson@1586
    30
\  (! x. ? y. ~hates x y) & \
clasohm@969
    31
\  ~ agatha=butler --> \
paulson@1586
    32
\  killed agatha agatha";
clasohm@969
    33
paulson@1586
    34
(*Halting problem: Formulation of Li Dafa (AAR Newsletter 27, Oct 1994.)
paulson@2031
    35
        author U. Egly;  46 clauses; 264 Horn clauses*)
paulson@1586
    36
goal HOL.thy
paulson@1586
    37
 "((EX X. (a X) & (ALL Y. (c Y) --> (ALL Z. (d X Y Z)))) -->  \
paulson@1586
    38
\  (EX W. (c W) & (ALL Y. (c Y) --> (ALL Z. (d W Y Z)))))     \
paulson@1586
    39
\ &                                                          \
paulson@1586
    40
\ (ALL W. (c W) & (ALL U. (c U) --> (ALL V. (d W U V))) -->       \
paulson@1586
    41
\       (ALL Y Z.                                               \
paulson@1586
    42
\           ((c Y) & (h2 Y Z) --> (h3 W Y Z) & (oo W g)) &       \
paulson@1586
    43
\           ((c Y) & ~(h2 Y Z) --> (h3 W Y Z) & (oo W b))))  \
paulson@1586
    44
\ &                    \
paulson@1586
    45
\ (ALL W. (c W) &       \
paulson@1586
    46
\   (ALL Y Z.          \
paulson@1586
    47
\       ((c Y) & (h2 Y Z) --> (h3 W Y Z) & (oo W g)) &       \
paulson@1586
    48
\       ((c Y) & ~(h2 Y Z) --> (h3 W Y Z) & (oo W b))) -->       \
paulson@1586
    49
\   (EX V. (c V) &       \
paulson@1586
    50
\         (ALL Y. (((c Y) & (h3 W Y Y)) & (oo W g) --> ~(h2 V Y)) &       \
paulson@1586
    51
\                 (((c Y) & (h3 W Y Y)) & (oo W b) --> (h2 V Y) & (oo V b))))) \
paulson@1586
    52
\  -->                  \
paulson@1586
    53
\  ~ (EX X. (a X) & (ALL Y. (c Y) --> (ALL Z. (d X Y Z))))";
clasohm@969
    54