hol90 logo   HOL90 USER MANUAL

The hol90 system is a re-implementation in SML/NJ of the Cambridge HOL system (hol88). The proof support of hol90 (term manipulation, axioms, inference rules, tactics, conversions, theories, libraries, etc.) is intended to be a replacement for that of hol88. The major difference between the two systems is that they have been implemented in two different dialects of ML; a host of minor differences are discussed throughout this document.

Note.It would be surprising if you could learn HOL only through this user manual. The Gordon and Melham book (Introduction to HOL, Cambridge University Press, 1993) provides a good place to start. Alternatively, you might consider a hol90 training course: contact Tom Melham for details.

Table of Contents

Beginning of hol90 user manual

Examples

In the following list you can find some detailed examples of the use of hol90.

Table of Contents

Common questions and problems

The following are some common questions and problems that might arise when one is dealing with hol90.
Why all these type annotations?
People new to HOL systems often ask why they have to add type annotations to their terms. This was a design decision made by Robin Milner for the original LCF system, and we have not found reason to change. hol90 performs full Hindley-Milner type inference, inferring most general types, and then fails if any type variable is still unconstrained. If this wasn't done, inference rules would have to normalize types at runtime. For example, in 
    ABS `x` (REFL `x`)
ABS would in general need to unify the types of the two xs, in order to make the types in the argument term and the occurrences in the theorem agree. In any case, those who want to experiment with type inference can write their own typechecker and use it in parsing, since the kernel of the system is independent of the particular type checker used.
My library take ages to load!
A current shortcoming of hol90 libraries is that any code loaded will be source, not object, so loading will be slower. As soon as SML/NJ's separate compilation facility settles down, this will be fixed. In the mean time, there is a function prim_load_theory of type 
    (string -> unit) -> {lib:lib, theory:string} -> unit
The first argument is a code_loader function - it is invoked on each file in the code section of a library. Two possible ways to use this are to: compile the code of a library or to intepret the code. The first option is already present in the functionality of the derived form load_library, i.e., 
    val load_library = prim_load_library Lib.compile;
Another specialization of prim_load_library would load the code quickly, but execution of that code would be slow. It would be appropriate for small memory machines and it would be defined: 
    val fast_load_library = prim_load_library Lib.interpret
This has not, however, been installed in the system. Another solution would be for users to load commonly used libraries and then dump the image with save_hol.
My theory (or library) doesn't load and fails with a strange error message!
In an improperly installed hol90 system, the following behaviour can sometimes occur: 
    - load_library {lib=set_lib, theory="foo"} handle e => Raise e;

    Loading the library "set".
      ... < many loading messages >
    Exception raised at Library.add_new_parent:
    Theory.new_parent.install_new_parent.get_file_by_key: 
       unable to get the file "HOL.holsig"
Here the problem is probably that the theory set found in the set library is out-of-date with respect to the HOL theory. The source of the problem is that hol90 uses unique ids (name + timestamp) to implement theories securely. When load_library is asked to load set_lib, it declares the theory foo and attempts to do a new_parent on the theory set. The theory set is found on disk. Its parents (name + timestamp) are used to chain back in the theory graph until the frontier of the existing theory graph is found.

When looking for the parents of a theory, first they are looked for in the internally held graph representing the loaded HOL theories. The equality test involves both the theory names and the timestamps. If not found, then the search goes to disk, using Globals.theory_path as denoting the places to look. When the parents of set, i.e., the HOL theory, is not found, that means the particular HOL theory being searched for does not exist in the internal graph structure. Since we know that a HOL theory is certainly there, the theory set and hence the library set is out-of-date with respect to the core HOL system. The typical reason for this is that the core HOL system has been made by invoking 

    make_hol  -n
but that the libraries were not subsequently remade. By the way, a simple test of whether the theory set is up-to-date, is to attempt to do a 
    load_theory "set" handle e => Raise e;
Why have both Psyntax and Rsyntax?
That is, why have two copies of the same thing? There are good arguments for and against both styles, so the hol90 implementors decided to make both syntaxes available. The argument for records? Record types often give better information about what the arguments of a function are. Compare 
   Psyntax.new_specification 
       :string->(string*string*int) list -> thm -> thm
with 
   Rsyntax.new_specification : 
       {name :string,  sat_thm : Thm.thm,
        consts:{const_name:string, fixity:Term.fixity} list} -> Thm.thm
Furthermore, code written with records can be more readable when intensive term manipulations are being performed. Alternatively, it can be much clumsier to write such code, since the syntax of records entails more verbosity.
Autoloading failure.
Some derived principles of definition may define symbolic constants, and need to generate a name to store the definition with on a theory file. Usually this name generation is done by prepending the name of the constant being defined to "_DEF". This can give us strange names, like 
       ;;_DEF
which is half symbolic identifier and half ordinary identifier. This strangeness is not a problem when loading the theory, but such theory bindings will not be autoloadable; the system will issue a warning message when autoloading such a binding and skip over it.
Problems in parsing symbolic identifiers.
The inclusion of ":" in the "symbolics" means that some constraints may need to be separated by white space. For example 
        $=:bool->bool->bool
will be broken up by the lexer as 
        $=: bool -> bool -> bool
and parsed as an application of the symbolic identifier "$=:" to the term argument list ["bool", "->", "bool", "->", "bool"]. But 
        $= :bool->bool->bool
is OK, being parsed as the symbolic identifier "=" constrained by a type. Another example involves the comma, which is also a symbolic identifier: 
       ($+,T)
the intended pairing of the addition function with the constant "T" will fail to typecheck because the phrase will be broken up as 
        (  $+,  T  )
and interpreted as a variable "+," applied to "T". The intended parse is achieved by inserting a space before the comma.
Non-confluence in rewriting
In both hol88 and hol90, the rewriting process will occasionally encounter a term to which more than one rewrite will be applicable. The first match will be the one used to rewrite the term. It can happen (rarely) that hol90 will choose a different first match than hol88, and that the result will be different. This is an example of non-confluence. Some proofs from hol88 may break as a result.
Renaming
The basic hol90 term operations "subst" and "inst" do the least possible variable renaming within the bounds given by certain strictures (such as being able to re-parse prettyprinted terms to themselves). hol88 will sometimes rename unnecessarily, and this can, at times, cause a proof not to port. This typically occurs in the case of supplying witnesses to EXISTS_TAC. A sure tip off is a proof that won't port because there is a primed existential witness in the tactic, e.g., 
        EXISTS_TAC "x'"
Often, removing the prime will enable the proof to go through.

Table of Contents

Surf the source!

The hol90 distribution is organized into the following directories:

Table of Contents

The hol90 executable comprises a set of about 40 structures, all loaded into the SML image, plus a collection of theories. All the structures are open, so the system appears to be totally without form. However, the form is there: if you wish to browse around, or have to track down a bug, a quick reference to the structures follows.

Every bound identifier that is not in the pervasive environment of SML/NJ should be in one of the above structures.

Table of Contents

Using SML

We provide a simple guide to the local installation of SML/NJ.

For those hol88 users migrating to hol90, SML has a Core language subset that is quite close to ML Classic. A comparative reading of the hol88 and hol90 sources will go a long way towards making one "Core SML-fluent". One might start by reading the hol90 "standard prelude" (src/0/lib.sml), which provides many utility functions used in building the system.

The formal semantics of SML is found in The Definition of Standard ML (MIT Press 1990) and some discussion of the semantics can be found in Commentary on Standard ML (MIT Press 1990). These books are for reference, and are by no means introductory texts. A gentler introduction is Larry Paulson's textbook, ML for the Working Programmer (Cambridge University Press, 1991).

Table of Contents

Compatibility with hol88

As stated in the introduction to this manual, there are few differences between hol88 and hol90, at least at the level of theorem proving. However, there is a host of differences in the support for theorem proving and so a straghtforward compatibility package is not possible. We have, however, made a minor effort at supporting those who are used to hol88: in conjunction with the built-in structure Psyntax, hol88_lib gives hol90 some ability to mimic hol88. Therefore, to operate as much as possible in a hol88-like environment, one would do the following: 
    load_library{lib = hol88_lib, theory = "-"};
    open Psyntax Compat;

Warning: hol88_lib is by no means complete! If you have additions you want made, please send them to the author of this document.

Lacunae

The following hol88 facilities do not appear in hol90. As well, there are still a few libraries have not yet been ported. Finally, the contrib directory is much smaller than that of hol88.

Conversion between the two systems

Currently, there are no good tools for converting between the two systems. A set of gnuemacs functions for doing elementary conversions between Classic ML and SML files is provided with the release, in the "tools" directory. They work best on files that are mainly proofs; files of general ML code really need a more comprehensive solution. In spite of that, any gmacs hackers who want to expand the capabilities of these functions are warmly encouraged!

Table of Contents

Introduced types

Here we give a listing of all types defined by hol90 on top of SML. The definitions of type abbreviations are given. Most of the other types are abstract, and have specially installed prettyprinters so that users can "see" values of these opaque types.

The special-purpose types arg and parse are used locally in the parser and might change or disappear.

Table of Contents

Exceptions

The multitude of exceptions that hol90 can raise have been shepherded into one: 
    exception HOL_ERR of {origin_structure : string,
                          origin_function : string,
                          message :string}
The three fields are, in order: the name of the structure that the raising routine inhabits; the name of the raising routine; and the message. Any exception that propagates to the top level should either be HOL_ERR or defined in the SML/NJ pervasive environment.

Unfortunately, SML/NJ does not automatically print the values of exceptions that propagate to the top level. To help in this, the structure Exception (where HOL_ERR is defined) provides the routines 

    print_HOL_ERR: exn -> unit
    Raise : exn -> 'a
The first prints out HOL_ERR in a fashion prescribed by the (assignable) function Globals.output_HOL_ERR. The second does the same (provided Globals.print_exceptions is set to true), but also raises the exception again. This feature is handy for debugging and also for reporting HOL_ERR, since it saves on finding a value of the proper type to return: 
    el 3 ["foo","bar"] handle e => (print_HOL_ERR e; "blag");
    el 3 ["foo","bar"] handle e => Raise e;

Table of Contents

Help

A primitive on-line help system exists: an invocation of "help" on the subject of interest, e.g., 

    help "X"
follows the help_path until it finds a file X.doc. Then it makes a system call to process the file and print the results to std_out. An assignable string interpreted as an operating system function is used for printing: it is the variable 

       Globals.output_help : string ref

which is initially set to "/bin/cat". If you find that "help" fails because the system call fails, you should try the auxiliary help function "help1", which produces TeX-annotated, but still readable, output.

Unhappily, hol90 is not as yet self-sufficient in the area of help files: it relies primarily on the hol88 documentation. This is not that bad, since most of the functionality in the two systems is identical, particularly in the area of proof functions. However, at times the help is deficient or downright unhelpful!

It can happen that you will able to get help for a function that doesn't exist in the system, e.g., "dest_pred". To ease your puzzlement, there is "meta-help" for this: do 

    help "hol88_extras";
which will return a complete listing of all entry points of hol88 that aren't also in hol90. Each entry has a one-line explanation; often the entry point, if it is useful, has a different name in hol90. Many entries in the list are not useful and should in fact be deleted from hol88.

Table of Contents

Paths

The following paths exist in the structure Globals: 
    theory_path : string list ref
    library_path : string list ref
    help_path : string list ref
These are used to find theories, libraries, and help. The three paths are independent. Each path begins with an empty path (""), so that help, theories and libraries can be designated by absolute pathnames. The paths are used primarily to find files to read, load, or print; however, the theory and library paths are also used to determine where to write a theory or library, respectively. In this case, the first member of the list is taken as the prefix of the pathname of the file to be written. If the write fails, no further attempts are made using other members of the list.

There are some functions for manipulating paths: 

    Lib.cons_path : string -> string list ref -> unit
    Lib.append_path : string -> string list ref -> unit
In "cons_path", an attempt is made to keep the empty path first in the path list. This is helpful for developing local versions of system theories, help, and libraries.

Table of Contents

Flags

All assignable variables in the system are held in the structure Globals. Most of them are directly assignable, for example 
    Globals.show_types := true;

HOL start-up files

When hol90 is invoked, it looks for a file called "hol-init.sml", first in the current directory, then in the user's home directory. A "use" is performed on the first hol-init.sml found. This support is extended to all binaries resulting from an invocation of "save_hol". This service can be disabled by assigning Globals.use_init_file to false.
Table of Contents
Konrad Slind, slind@informatik.tu-muenchen.de