Re: [Hol-info] Theories in HOL4

[Konrad S. <sl...@cs...>]

Hi Bob,

> 	1) How does one add a new ancestor to a theory? [What is the
> analogue of new_parent in HOL90?]

In HOL4, an exported theory segment named "foo" is represented by a
compiled ML structure named "fooTheory". Thus, in HOL90, one would write 

    new_parent "foo";

and in HOL4 one writes
 
    load "fooTheory";

When this structure is loaded by the underlying ML system, all the
ancestors of "foo" are recursively loaded. The contents of "foo" are
then available by using the dot notation, e.g., fooTheory.mythm, or by
"open"ing fooTheory and directly accessing the contents, e.g., mythm.

> 	2) How does one save the theory created by new_theory [and the
> work of a session] to disk?

 There are 2 aspects to this question. 

1. If you are in the process of building up a theory segment, the
sequence of ML commands which make definitions, prove theorems,
etc. should be held in a text file (call it "foo"). This file can be
"use"d to re-build the state in a fresh invocation of HOL. This file
gives inter-session persistence, but requires all the definitions
and proofs to be re-executed, which can take awhile.  

2. Once you've got a theory segment completely developed, it should be
moved to a "script" file, named in our example, "fooScript.sml". The
"Script.sml" suffix is a requirement. You also have to add 

    val _ = export_theory();

to the end of the file. Holmake should then be invoked in the current
directory. It will load all the required context for the theory foo,
execute the ML in fooScript, creating foo and its theorems, and dump the
results to a file "fooTheory", which is then compiled. The result can be
loaded as above. 

See the template file <holdir>/examples/tempScript.sml for an example.

> 	How does one reopen the theory for further work on it in a later
> session.

  Can't. Once a theory x has been exported, it becomes "closed": it
can't be re-opened in order to stuff more things into it. One can
however extend x, by creating a new theory y and making x a parent of y.

Alternatively, you could also go back and edit xScript.sml and re-build
xTheory with Holmake. 

There's more extensive discussion of theories in the HOL description, 

   http://umn.dl.sourceforge.net/sourceforge/hol/kananaskis-1-description.pdf

from pages 56 and 124. Also section 4.5 of the tutorial may be
helpful. Finally, online documentation may be found at

   http://hol.sourceforge.net/kananaskis-1-helpdocs/help/HOLindex.html

(follow the "Theory" structure link).


Konrad.