Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4); Sun, 17 Jan 1993 05:24:16 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA05867; Sat, 16 Jan 93 21:14:38 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA05862; Sat, 16 Jan 93 21:14:33 -0800 Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.4) to cl; Sun, 17 Jan 1993 05:13:54 +0000 To: chou@edu.ucla.cs Cc: info-hol@edu.uidaho.cs.ted (INFO-HOL mailing list) Subject: Re: Unused assumptions In-Reply-To: Your message of Sat, 16 Jan 93 19:42:47 -0800. <9301170342.AA07383@maui.cs.ucla.edu> Date: Sun, 17 Jan 93 05:13:48 +0000 From: John Harrison Message-Id: <"swan.cl.ca.283:17.01.93.05.13.57"@cl.cam.ac.uk> Ching Tsun says: > Notice that the assumption "a" has been lost! Why? > Because it is not actually used in the proof, though > one may think ASM_REWRITE_TAC uses every assumption. > This habit of dropping unused assumptions is not limited > to rewriting tactics; many other tactics have similar > behavior. My question is: Should this be considered > a virtue or a vice? In my view it's definitely a vice. There's another related problem with alpha-equivalence, exemplified by: > #let th = PROVE > # ("!x:*. x = x", > # ACCEPT_TAC(GEN "y:*" (REFL "y:*")));; > th = |- !y. y = y I think all tactics should be fixed up so this problem doesn't arise. Alternatively one could have a tactical, say "EXACT", which would do any alpha-conversion or adding and permuting of assumptions. Maybe there are other issues involved that I haven't thought of which make this impractical. John.