Return-Path: Delivery-Date: Received: from dworshak.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Fri, 10 Sep 1993 07:25:58 +0100 Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA26977; Thu, 9 Sep 93 23:18:42 -0700 Sender: info-hol-request@cs.uidaho.edu Errors-To: info-hol-request@cs.uidaho.edu Precedence: bulk Received: from wasa.shh.fi by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA26973; Thu, 9 Sep 93 23:18:34 -0700 Received: from charon.wasa.shh.fi by wasa.shh.fi (4.1/291091(up)) id AA22306; Fri, 10 Sep 93 09:18:31 +0300 Received: From PAMIR/WORKQUEUE by charon.wasa.shh.fi via Charon-4.0A-VROOM with IPX id 100.930910091827.416; 10 Sep 93 09:23:37 +0500 Message-Id: To: info-hol@cs.uidaho.edu From: jwright@wasa.shh.fi Organization: Swedish School of Econ. Vasa Date: 10 Sep 1993 9:16:38 EET Subject: Re: a little proof challenge Priority: normal X-Mailer: Pegasus Mail/Mac v2.02 Like many others, I spent most of the time looking at the goal "!P Q R. !x:*. ?v. ?w. !y. !z:**. ((P x /\ Q y) ==> ((P v \/ R w) /\ (R z ==> Q v)))" and figuring out that what made it look weird was that most quantifiers were too far out. Recalling that I've encountered this situation before, I dug into my files and found suitable tactics. The goal is solved by e(QUANT_IN_TAC THEN REPEAT STRIP_TAC THEN ASM_CASES_TAC "?w.(R:**->bool)w" THEN ASM_REWRITE_TAC[] THEN AUTO_EXISTS_TAC);; where QUANT_IN_TAC is a crude thing which repeatedly uses conversions that push in quantifiers (FORALL_AND_CONV, EXISTS_IMP_CONV etc.) and AUTO_EXISTS_TAC is a (likewise simple-minded) tactic which tries to instantiate existential goals using the assumption list. Time used: 10 minutes figuring out the quantifier business 10 minutes looking for old stuff in various files 2 minutes interacting with HOL Joakim