Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
From: jimaf@edu.uidaho.cs.leopard (Jim Alves-Foss)
Message-Id: <9205071739.AA19108@leopard.cs.uidaho.edu>
Subject: Labeling assumptions in the asl
To: info-hol@edu.uidaho.cs.ted
Date: Thu, 7 May 92 10:39:07 PDT
Mailer: Elm [revision: 66.33]

I am trying to find a way to intuitively do proofs without using "el" for
explicit assumption numbers. I recall the thread here earlier discussing 
several ways of doing that.  I have another idea that I don't recall seeing 
and wonder if anyone has worked on it. The idea is as follows:

1. When you add assumptions to the asl give them a label ("name"):
   ASSUME_TAC term label
   ASSUME_CASES_TAC term label1 label2
   ...
2. When trying to explicitly use an assumption, use the label.
   ASM_LABEL_REWRITE_TAC [label1,label2] thm_lst

We can already do this when using lemmas (or other theorems), but for 
assumptions I haven't found a way.  This is a basic premise I have learned
from mathematicians, when you want to use something, give it a name.

Any comments would be appreciated.


-Jim Alves-Foss
 Assistant Professor
 Computer Science Department                (208) 885-7232
 University of Idaho                        (jimaf@ted.cs.uidaho.edu)