Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2); Thu, 3 Dec 1992 16:19:42 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA20656; Thu, 3 Dec 92 07:56:05 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from nene.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA20649; Thu, 3 Dec 92 07:55:48 -0800 Received: from guillemot.cl.cam.ac.uk (user tfm (rfc931)) by nene.cl.cam.ac.uk with SMTP (PP-6.3) to cl; Thu, 3 Dec 1992 15:54:39 +0000 To: Wishnu Prasetya Cc: info-hol@edu.uidaho.cs.ted (hol mailing list), Tom.Melham@uk.ac.cam.cl Subject: Re: HELP: RES_TAC In-Reply-To: Your message of Thu, 03 Dec 92 13:41:45 +0700. <199212031241.AA01381@infix.cs.ruu.nl> Date: Thu, 03 Dec 92 15:54:30 +0000 From: Tom Melham Message-Id: <"nene.cl.ca.354:03.12.92.15.54.51"@cl.cam.ac.uk> To the replies of David Shepherd and John Harrison, I would add the following general observation. Canonicalization for the HOL "resolution" tactics is based on the idea that the assumptions of a goal are most likely to be in a vaguely "standard" form. This means conjunctions and disjunctions split, and existential quantifiers stripped off --- e.g. what the very commonly-used tactics STRIP_TAC and STRIP_ASSUME_TAC do by default. In the current case > "WELL_FOUNDED(R 0)" > [ "0 < n \/ (0 = n) ==> WELL_FOUNDED(R 0)" ] > [ "0 < n \/ (0 = n)" ] is in "non-standard" form because of the disjunction on the assumption list. But the canonicalization of the implication is ["0 < n ==> WELL_FOUNDED(R 0)"; "0 = n ==> WELL_FOUNDED(R 0)"] reflecting the fact that most often we expect disjunctions to be split into cases. Hence RES_TAC doesn't work here. Both David and John's solutions work, but I would suggest another one --- try not to get yourself into such a non-standard situation, unless really necessary. Tom