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; Tue, 11 Jul 1995 10:49:01 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA051814742; Tue, 11 Jul 1995 03:25:42 -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 AA051784733; Tue, 11 Jul 1995 03:25:33 -0600 From: shepherd_david/uk_bristo_br@brx001.bristol.st.com Received: by daisy id KAA15901; Tue, 11 Jul 1995 10:28:43 +0100 Received: from by brx001 with SMTP (1.37.109.11/16.2) id AA104254177; Tue, 11 Jul 1995 10:16:17 +0100 X-Openmail-Hops: 1 Date: Tue, 11 Jul 95 10:15:53 +0100 Message-Id: In-Reply-To: <199507102203.AA114043820@bobcat.cs.byu.edu> Subject: RE: [Q] manipulating assumptions Mime-Version: 1.0 To: info-hol@leopard.cs.byu.edu Cc: windley@cs.byu.edu Content-Type: text/plain; charset=US-ASCII; name="Message text" Content-Transfer-Encoding: 7bit > > Recently rahard@ee.umanitoba.ca asked about manipulating assumptions. > > Below are 8 different ways of solving the goal. The first 6 do not > manipulate the assumption list in the sense that the question asked, but do > solve the goal. The last two manipulate the assumption list using > ASSUM_LIST. > > Its interesting to note that the last two examples are not shorter than the > first 5 and are in many cases considerably more complex. Obviously this > won't always be the case, but the direct approach is not always the best. An even simpler method than any of the ones suggested here is to use the FAUST package REWRITE_TAC[] THEN FAUST_TAC solves the goal - actually the REWRITE_TAC[] is used purely to flip (p1 = T) and (p2 = F) into p1 and ~p2 and a less heavyweight tactic could do this (I have one around somewhere called BOOL_SIMP_{CONV|RULE|TAC} which does all the obvious boolean simplifications. DeS