Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Mon, 10 Jul 1995 11:33:51 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA280940912; Mon, 10 Jul 1995 04:08:32 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from daisy (daisy.inmos.co.uk) by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA280790688; Mon, 10 Jul 1995 04:04:48 -0600 From: shepherd_david/uk_bristo_br@brx001.bristol.st.com Received: by daisy id LAA03037; Mon, 10 Jul 1995 11:07:25 +0100 Received: from by brx001 with SMTP (1.37.109.11/16.2) id AA087510098; Mon, 10 Jul 1995 10:54:58 +0100 X-Openmail-Hops: 1 Date: Mon, 10 Jul 95 10:54:07 +0100 Message-Id: In-Reply-To: <95Jul9.215733met_dst.8082@sunbroy14.informatik.tu-muenchen.d> Subject: Re: [Q] manipulating assumptions Mime-Version: 1.0 To: info-hol@leopard.cs.byu.edu Cc: rahard@ee.umanitoba.ca Content-Type: text/plain; charset=US-ASCII; name="Message text" Content-Transfer-Encoding: 7bit > > > Question from a newbie: How do I manipulate assumptions? ... I was > > trying to prove: > > > "!inp out. > > (?p1 p2. > > (p1 = T) /\ > > (~inp ==> (p1 = out)) /\ > > (inp ==> (p2 = out)) /\ > > (p2 = F)) ==> > > (out = ~inp)" > > Often the key to using assumptions is to never let them be assumptions, > since then one loses fine-grain control. The answer lies in a special > class of tactics called `theorem continuations'. These perform an > operation on the current goal and pass the result of that to another > function (often a tactic). However, if you get into a situation where the things you want to manipulate are assumptions and it is impractical/you can't be bothered to go back and do it properly with continuations then you can make copious use of ASSUME to handle this. In the case here I think you could do ASSUME_TAC(REWRITE_RULE[ASSUME(--`p2 = F`--)](ASSUME(--`inp ==> (p2 = out)`--))) etc. This would add the asssumption --`inp ==> ~out`--. Note as ASSUME(--`...`--) becomes a standard item in these contexts I seem to recall defining two new operators along the lines of -- and == so that |-`...`-| could be used for ASSUME(--`...`--) with the |- being used to indicate that it was a theorem that was being constructed. So the you would can ASSUME_TAC(REWRITE_RULE[|-`p2 = F`-|](|-`inp ==> (p2 = out)`-|)) N.b., doing it with theorem continuations is probably the "proper" way to do it but sometimes can be a bit faster to do it the quick'n'dirty way!