HOL90 USER MANUAL
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.
Beginning of hol90 user manual
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.
(string -> unit) -> {lib:lib, theory:string} -> unitThe 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.interpretThis 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.
- 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_holbut 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-n
load_theory "set" handle e => Raise e;
Psyntax.new_specification :string->(string*string*int) list -> thm -> thmwith
Rsyntax.new_specification : {name :string, sat_thm : Thm.thm, consts:{const_name:string, fixity:Term.fixity} list} -> Thm.thmFurthermore, 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.
;;_DEFwhich 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.
$=:bool->bool->boolwill be broken up by the lexer as
$=: bool -> bool -> booland parsed as an application of the symbolic identifier "$=:" to the term argument list ["bool", "->", "bool", "->", "bool"]. But
$= :bool->bool->boolis 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.
EXISTS_TAC "x'"Often, removing the prime will enable the proof to go through.
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.
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).
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.
The special-purpose types arg and parse are used locally in the parser and might change or disappear.
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 -> 'aThe 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 "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.
theory_path : string list ref library_path : string list ref help_path : string list refThese 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 -> unitIn "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.
Globals.show_types := true;