# ` 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.

# Examples

In the following list you can find some detailed examples of the use of hol90.
• Fermat's last theorem (n = 4)
• Verification of a hardware multiplier
• Inductive definitions
• The operational semantics of a small imperative language
• Combinatory logic
• Minimal intuitionistic logic, plus proof of Curry-Howard isomorphism with combinatory logic
• A small process algebra
• Abstract theories
• Documentation - somewhat dated, but still useful!
• Abstract theory of monoids
• Abstract theory of groups
• An instantiation of groups with xor
• Chandy and Misra's UNITY formalism
• dining philosophers
• Staunstrup and Loevengreen's 2-Arbiter example
• Window inference
• Basic examples
• A parity circuit
• Applying a database query language to theories
• Documentation
• Basic examples
• A more complex example

# 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;

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.
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.

# Surf the source!

The hol90 distribution is organized into the following directories:
• contrib - libraries contributed by users
• doc - system documentation
• examples - examples of using hol90
• src - the hol90 sources
• library - the standard libraries
• theories - the system theories
• tools - some useful tools

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.

• Sys_params - system building options.
• Globals - global flags
• Exception - HOL_ERR defined
• Lib - utility routines
• Uid - unique identifiers
• File - file operations along a path
• Help - a simple interface to system documentation
• Type - HOL types
• Term - HOL terms
• Match - matching for types and terms
• Dsyntax - derived syntax for terms
• Parse_support - interface to preterm construction
• Parse - parsing of types and terms
• Hol_pp - prettyprinting of types and terms
• Thm - the primitive rules of inference of the HOL logic
• Theory - theory operations
• Library - functions for interacting with libraries
• Install - relocating hol90 to a new directory
• Const_spec - principle of constant specification
• Type_def - principle of type definition
• Const_def - principle of constant definition
• Drule - derived rules of inference and theorems
• Conv - conversions
• Tactical - tacticals
• Net - discrimination nets for terms
• Rewrite - rewriting functions
• Thm_cont - theorem continuations
• Tactic - tactics
• Taut_thms - some tautologies
• Resolve - HOL-style resolution rules of inference
• Type_def_support - helps prove useful thms from a type definition
• Induct_then - generalized induction tactic
• Prim_rec - generalized primitive recursive definition
• Num_conv - num_CONV
• Let_conv - let_CONV and PAIRED_BETA_CONV
• Num_induct - INDUCT and INDUCT_TAC
• Rec_type_support - helps prove useful thms from a "define_type" definition
• Define_type - derived principle of definition for concrete recursive types
• Goalstack - goal-directed proof manager
• Sys_lib - descriptions of the predefined libraries of the system
• Psyntax - support for paired syntax
• Rsyntax - support for record-style syntax
Every bound identifier that is not in the pervasive environment of SML/NJ should be in one of the above structures.

# 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).

# 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.
• Interface maps and constant hiding.
• Type abbreviations (for the logic).
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!

## 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.
• hol_type - Abstract type of HOL types
• term - Abstract type of HOL terms
• thm - Abstract type of theorems
• lib - Abstract type of library descriptions
• fixity - Parsing status of constants
• subst = {redex:'a, residue:'a} list - Substitutions for types and terms
• conv = term -> thm - Equality reasoners
• goal = term list * term
• validation = thm list -> thm
• tactic = goal -> goal list * validation
• thm_tactic = thm -> tactic
• thm_tactical = thm_tactic -> thm_tactic
• rewrites - Rewrite rule databases
• 'a net - "Hash tables" indexed by terms
• preterm - Terms that haven't been typechecked yet
• goalstack - Backwards proof managers
• proofs - Collections of backwards proof managers
• arg
• parse

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

## 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;
```

## 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.

## 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.

## 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.