Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from dworshak.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Thu, 9 Sep 1993 09:50:26 +0100
Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA24827;
          Thu, 9 Sep 93 01:45:13 -0700
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
Received: from tuminfo2.informatik.tu-muenchen.de by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.4/16.2) id AA24823; Thu, 9 Sep 93 01:45:09 -0700
Received: from sunbroy14.informatik.tu-muenchen.de ([131.159.0.114]) 
          by tuminfo2.informatik.tu-muenchen.de with SMTP id <57668>;
          Thu, 9 Sep 1993 10:45:07 +0200
Received: by sunbroy14.informatik.tu-muenchen.de id <8081>;
          Thu, 9 Sep 1993 10:44:48 +0200
From: Tobias.Nipkow@informatik.tu-muenchen.de
To: info-hol@cs.uidaho.edu
Cc: joyce@cs.ubc.ca, Larry.Paulson@cl.cam.ac.uk
In-Reply-To: Jeffrey Joyce's message of Thu, 9 Sep 1993 02:15:00 +0200 <7637*joyce@cs.ubc.ca>
Subject: a little proof challenge
Message-Id: <93Sep9.104448met_dst.8081@sunbroy14.informatik.tu-muenchen.de>
Date: Thu, 9 Sep 1993 10:44:35 +0200

I couldn't resist trying Jeff's little challenge in Isabelle/HOL.
The standard tactics for dealing with quantified formulae, fast_tac and
best_tac, unfortunately failed and I had to pull out the big gun:

Level 0
! P Q R x. ? v w. ! y z. P(x) & Q(y) --> (P(v) | R(w)) & (R(z) --> Q(v))
 1. ! P Q R x. ? v w. ! y z. P(x) & Q(y) --> (P(v) | R(w)) & (R(z) --> Q(v))
val it = [] : thm list
> by (safe_meson_tac 1);
Level 1
! P Q R x. ? v w. ! y z. P(x) & Q(y) --> (P(v) | R(w)) & (R(z) --> Q(v))
No subgoals!
Timing  compile-0.0s (0.0s+0.0s+0.0s+0.0s+0.0s) run-1.4s

Questions about safe_meson_tac should be directed to Larry Paulson.  Let me
just tell you that it is based on a strategy (model elimination) due to Mark
Stickel.

Tobias