Delivery-Date: 
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
Message-Id: <9402040810.AA19254@maui.cs.ucla.edu>
To: info-hol@cs.uidaho.edu (info-hol mailing list)
Subject: Finding a theorem whose name I know
Date: Fri, 04 Feb 94 00:10:07 PST
From: chou@cs.ucla.edu

Finding a theorem in HOL is hard.  Even if I know exactly what the
theorem is called, I still need to find out in which theory it resides
and whether it is a derived theorem, a definition, or (in rare cases)
an axiom.  In almost all cases I really couldn't care less about these
extraneous informations about a theorem.  Why can't I have an ML procedure
find_thm which can find and return a named theorem?  This is easy to do
if I know in which theory the theorem resides:

fun find_thm (thy) (lbl) =
  theorem    (thy) (lbl) handle _ =>
  definition (thy) (lbl) handle _ =>
  axiom      (thy) (lbl) handle _ =>
  raise (* ... *) ;

But what if I don't know which theory to look at?  I can search through
all theories in the ancestry of the current theory, but this is extremely
inefficient since lots of useless theories can get loaded in.
Any suggestions?  What I need is probably some sort of data structures
stored on disk via which I can find out very fast where a named theorem
is among all existing theories.  Has anyone hacked something like this?

Finally, I know autoloading helps, but I still need to know which theory
to autoload from and, if I just need a few theorems out of the hundreds
a theory may offer, it is very inefficient to load them all in.
Since I'm running out of memory in large proofs, I want to avoid
autoloading as much as possible.

- Ching Tsun