Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <06997-0@swan.cl.cam.ac.uk>; Mon, 11 May 1992 01:23:26 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA23973; Sun, 10 May 92 16:58:30 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from toadflax.cs.ucdavis.edu by ted.cs.uidaho.edu (16.6/1.34) id AA23969; Sun, 10 May 92 16:58:24 -0700 Received: from localhost.cs.ucdavis.edu by toadflax.cs.ucdavis.edu (4.1/UCD.CS.1.1) id AA29794; Sun, 10 May 92 16:58:41 PDT Message-Id: <9205102358.AA29794@toadflax.cs.ucdavis.edu> To: jimaf@edu.uidaho.cs.leopard (Jim Alves-Foss) Cc: info-hol@edu.uidaho.cs.ted Subject: Re: Labeling assumptions in the asl In-Reply-To: Your message of Thu, 07 May 92 10:39:07 -0800 Date: Sun, 10 May 92 16:58:40 -0700 From: sara kalvala Jim Alves-Foss says: > 1. When you add assumptions to the asl give them a label ("name"): > 2. When trying to explicitly use an assumption, use the label. A trivial way to do this is by using ASSUME: 1 subgoal: b /\ a (--`a`--) (--`b`--) - val name = ASSUME (--`b:bool`--); - e (REWRITE_TAC [name]); OK.. 1 subgoal: a (--`a`--) (--`b`--) I will refrain from suggesting the use of HOL88's ML_eval to automate this further... > This is a basic premise I have learned from mathematicians, when you > want to use something, give it a name. I am currently working on an extension of the term structure in HOL, so that any node in the term structure can be augmented by an arbitrary ML datatype, which could be, say, a label. Goals are then created using extended terms, and each assumption--or any subterm-- can then have a label attached. The modified subgoal package has hooks for functions which actually process the new information available, and one function which can be hooked on could be the processing of these labels. This extended term/proof structure should be completed sometime this summer... - Sara