Notes on HOL 4, Kananaskis-1 release

It has been a long time since our last major release. Progress has been made on many fronts. The HOL system has become easier to use, and it has grown a lot as well. Our goal continues to be the provision of a leading-edge research platform suitable for

formalizing mathematics,
verifying hardware and software, and
constructing custom proof tools.

And now the news.

Change of Base

We have moved our base of operations to SourceForge.

     http://sourceforge.net/projects/hol/

The (very nice) facilities available at SourceForge have enabled the HOL developers, who are currently scattered over three countries, to keep reasonable control over a continually changing system. SourceForge also provides a convenient place from which to distribute the system. Ordinary users can even grab incremental updates and bugfixes, rather than waiting for upcoming releases.

HOL is an open system, and we welcome those keen to play a role in its continuing evolution. There are many ways in which one might take part in HOL development. It is not necessary to have a deep knowledge of HOL (or even logic) in order to make a contribution. If you are interested, please send us an email.

Documentation Improved

Much new documentation has been written, especially for heavily used proof tools. Existing documentation has been spruced up, and there is a new interface to it. The HOL Reference Page, located in the distribution at

   /help/HOLindex.html

gives organized access to

libraries (source)
theories (proved theorems, scripts, and theory map)
proof support (documentation and links to source)
an index of all identifiers in the system, with links to sources

New Examples

ARM6 -- Anthony Fox has formalized version 6 of the Acorn Risc Machine and completed a proof of its correctness.
Sugar2 -- Mike Gordon has deeply embedded Sugar 2.0, the Accellera standard property language.
miller -- Joe Hurd has completely formalized an argument for the correctness of the Miller-Rabin probabilistic primality test. Also included are some cute smaller examples using probability.
Rijndael -- Konrad Slind has formalized and proved the functional correctness of Rijndael, the new AES crypto algorithm.
root2 -- A short introductory example showing that the square root of 2 is irrational. Adapted from a proof of John Harrison.

New and improved proof tools

Another complete decision procedure for full Presburger arithmetic over the integers and natural numbers, the Omega Test, has been implemented. It is usually faster than Cooper's algorithm, but problems that require significant work in converting the input to DNF can cause it to take much longer. The Omega Test is available in intLib as intLib.ARITH_CONV.
Induct and Induct_on have been improved to deal with mutually recursive datatypes, thanks to code written by Peter Homeier.
Hol_datatype's definition of large "enumerated types" (data types with only nullary constructors) is now much more efficient than it used to be.
There is a new (simple) interface provided to the "call-by-value" rewriter. bossLib.EVAL and bossLib.EVAL_TAC "evaluate" terms and goals respectively using a global set of rewrite theorems. This set is updated as theories load, so that running "functional programs" in the logic should often be as simple a matter as writing (for example)
```
         EVAL ``FACT 6``
```
and getting back
```
         > val it = |- FACT 6 = 720 : thm
```
Definitions made with Define also automatically update this global set of rewrites. There is support for monitoring EVAL and its kin, and for controlling the depth of its expansions.
The system now maintains a "stateful" simpset that is updated automatically as theories and libraries load, and as new types are defined. It can be accessed in the module BasicProvers or bossLib, with the function
```
       srw_ss : unit -> simpset
```
The access to type information (constructor injectivity and disjointness) duplicates the functionality provided by RW_TAC, but use of srw_ss has the advantage that other theorems and behaviours are also available automatically. For example, when pred_setLib is loaded, the srw_ss() simpset is extended with all pred_setTheory's "obvious rewrites", things like
```
      |- FINITE (P UNION Q) = FINITE P /\ FINITE Q
```
as well as the SET_SPEC_CONV conversion which does the right thing with
```
      x IN { ... | ... }
```
terms. There is also an RW_TAC equivalent, SRW_TAC which uses this simpset and also implements RW_TAC's aggressive stripping and normalisation strategies.
Permutative rewriting now has a kinder interface. Previously the simplifier cared about the order of the submitted (A,C) theorems, and required them to be fully specialized. No longer! Permutative rewrite sets can now be easily built with simpLib.ac_ss.
Much attention has been paid to efficiency problems arising from big terms (ranging to those with hundreds of thousands or millions of connectives and bound variables). We have not solved the problem of scale, but we have been able to remedy some serious bottlenecks. These improvements have generally been backwards compatible, but have also required some new (experimental) primitives. Consult the hol-developers discussion list at SourceForge for further information.

New libraries

The library HolSatLib (http://www.cl.cam.ac.uk/~mjcg/HolSatLib/) provides a very simple harness for invoking SAT solvers on HOL terms. Currently SATO, GRASP and ZCHAFF are supported. HolSatLib has only been tested under Linux, though it should be possible to run it under Windows.
The library word32Lib comprises a functor (called "wordFunctor") for creating word theories. It also provides word32Theory (see below), plus an evaluation conversion "WORD32_CONV".

New and improved theories

Laurent Thery's theories of divisibility, primality, and gcd are now part of the distribution, under the name dividesTheory, primeTheory and gcdTheory.
A theory of 32-bit machine arithmetic, due to Anthony Fox, available under the name word32Theory. The theory defines many of the `integer' operations found in computer architectures. It was developed in modelling the ARM instruction set. The operations can be grouped as follows:
- Bit-field testing and extraction;
- Arithmetic: Addition, Subtraction, Multiplication and Two's Complement;
- Logical: One's Complement, Bitwise And, Or and Exclusive Or;
- Shifts: Logical Right, Arithmetic Right, Rotate Right, and Rotate Right One Place with Carry Extension.
Theorems are provided for reasoning about bit-fields, as well as arithmetic (Commutative Ring properties) and the logical operations (Boolean Algebra properties). A number of rewrite rules are also provided, and these support fairly efficient term evaluation using WORD32_CONV (or EVAL).
The functor wordFunctor can be used to create bespoke word theories. For example, a theory of 8-bit words can be obtained by the invocation
```
      structure word8Theory = wordFunctor (val bits = 8)
```
A replacement theory of strings over an alphabet of 256 characters has been provided. String literals are no longer implemented as an infinite set of constants, given meaning by mk_thm; instead, they are constructed terms. This removes the last use of mk_thm in the HOL system. Note however, that this new theory is not backwards compatible: it will break code that treats string literals as constants.
A small theory of set-theoretic fixpoints, due to Michael Norrish.
A small theory supporting relatively efficient definitional CNF, due to Joe Hurd.
A small theory of container types, offering maps between lists, finite sets, and multisets (bags).
relationTheory now defines the constants RTC and RC (reflexive and transitive closure, and reflexive closure) and proves a variety of properties about them.
Restricted quantification now uses predicate sets, so the meaning of the term
```
       !x::P. Q x
```
is
```
       !x. x IN P ==> Q x.
```
The restricted quantification library has been updated to reflect this change, and also shrunk down: in the course of use it was found that more powerful proof tools like the simplifier have removed the need for many of the lower-level tactics.

Improved support for large formalizations

Holmake will now read and act under the supervision of make-files (usually named Holmakefile). These files can be used to control construction of object files in languages other than SML, and also have a number of other convenient functions. The basic format of the make-files read by Holmake is very much like that of standard make-files, but there is no support for patterns. For more documentation, see the Holmake section of the DESCRIPTION.

New syntax support

Term and type constants in the logic now enjoy per-theory name-spaces. This means that multiple theories can share constants with the same names. If two term constants of the same name are part of the logical context, the parser treats that name as if it were overloaded to both constants. Constants can be unambigously specified by prepending the theory name and "$". Thus
```
       bool$/\
```
is the conjunction operator in boolTheory, and
```
       :num$num
```
is the num type from numTheory. There are also new functions in the kernel's ML API for building and pulling apart constants with theory information included. For example, the function mk_thy_const has the following type
```
        {Name:string, Thy:string, Ty:hol_type} -> term
```
and the function dest_thy_const inverts this. mk_const remains in the system, but its behaviour is unspecified when two or more constants have the same name.
Type abbreviations can now be introduced using the function Parse.type_abbrev. When a type abbreviation is made, both the abbreviation and the abbreviation's RHS can be used to specify types. Variables that occur in the RHS become parameters of the "new" type operator. Thus
```
        type_abbrev("set", ``:'a -> bool``)
```
is used in pred_setTheory to establish ``:'a set`` as an abbreviation for functions of type ``'a -> bool``. After issuing this command, one can write ``NS:num set`` and ``:'b set``. When printed, types do not include abbreviations.
Syntax for ML-style case expressions is now supported. The same patterns supported by Define are allowed. Some examples of the syntax:
```
        case n of 0 -> x || SUC n -> n + 1
```
and
```
        case p of (x, []) -> x + 1
               || (y, h::t) -> y + h
```

Modified syntax support

The system now compiles files with common HOL infix declarations already in scope. This means that one need no longer write
```
       infix THEN THENL ...
```
at the top of one's files. Doing so is not an error however. If this behaviour leads to problems, recall that ML infix declarations can be cancelled with the "nonfix" directive.
We have rationalised the ML API. By default, just about all functions use "paired" syntax, rather than "record" syntax. So, mk_var has type
```
      string * hol_type -> term
```
rather than
```
      {Name : string, Ty : hol_type} -> term
```
A consistently "record-ised" view of the world is still available by opening the structure Rsyntax. Even in the default view of the world, some functions still take records. These exceptions are for functions where we feel that the order of arguments of the same type is not always obvious. This is exemplified by the universal adoption of the {redex,residue} datatype for substitutions and instantiations. (Remember also that the infix |-> function can be used to construct such records.)
Overloading now works slightly differently. Constants are automatically overloaded to "themselves". Thus, if you define a constant called "foo", and then another called "bar", and want to have "bar" overload to "foo", then you need only call
```
        overload_on ("foo", ``bar``);
```
The names of record fields are not now overloaded to the accessor function. This function needs to be accessed as the constant
```
      <rcd-type-name>_<fldname>
```
E.g., "rcd_fld". If you really like the 'dot' syntax, you can always write
```
      \r. r.fld
```
which eta-converts to the above.
An easier way of augmenting the built-in pretty-printer is now possible. Previously we allowed for the built-in printer to be completely replaced by a new function. Now, users can also specify new functions to augment the existing code, with the new functions called on terms of specified types. For more details, see the documentation for Parse.add_user_printer in the REFERENCE.
The parser now lets you create an ambiguous grammar. In doing so, it will issue a warning, but will otherwise attempt to do its best to parse inputs. The system's parsing and printing behaviour may become unpredictable, but generous uses of parentheses should allow most reasonable uses of the parser.

"Gratuitous" and probably irritating incompatibilities

There is no longer any module called basicHol90Lib. Instead, proof scripts should open boolLib.
The orientation of the theorems INTER_ASSOC and UNION_ASSOC from pred_setTheory has been flipped. This brings these theorems into line with all of the other associativity theorems in the system, which are of the form "right-associated" = "left associated", (e.g. x + (y + z) = (x + y) + z). This form is that expected by the AC_CONV procedure. If you want to flip them back to make a now-broken proof go through, use something like
```
      val INTER_ASSOC = GSYM INTER_ASSOC
      val UNION_ASSOC = GSYM UNION_ASSOC
```
before the references to these theorems occur.
Quotations vs. terms. New tactics from bossLib and definitional principles take quotations (i.e., use `...`). This allows tactics to parse the quotations in the context of the current goal, and allows definitional principles to cope with the fact that you may be redefining a new version of an existing constant with the same name. Other functions take terms, or types (i.e., use ``...``, or (Term`...`)). For example, this means that bossLib.DECIDE now takes a term, not a quotation.
We have removed setLib (including set_Theory) from the core distribution, though the source code is still present in the src/retired/set directory. With the "set" type abbreviation, pred_setLib (including pred_setTheory) should be a "drop-in" replacement for set.
Similarly, the inductive definition packages from Melham and Harrison have been merged into one. Please consult the examples/ind_def directory to see what syntactic changes are necessary.
Eta-conversion used to be part of std_ss, but it has been removed. This may break some proofs.
The functions "theorems", "definitions" and "axioms" have gained a theory-segment parameter. These functions take the name of the theory segment from which the theorems/definitions/axioms are to be retrieved. A call to
```
      theorems ()
```
should thus be replaced with
```
      theorems "-"
```

Miscellaneous

There are now four (4!) hol executables. They are:
```
      hol, hol.bare, hol.unquote, and hol.bare.unquote
```
all found in the bin/ directory. We recommend hol.unquote as the standard starting point.
In more detail, the ".unquote" suffix means that the ``...`` preprocessor is enabled. The ".bare" indicates that the executable starts up with a minimal logical context (just boolTheory, the goal-stack and the 'standard' tactics and conversions loaded). This is like the old behaviour of the hol and hol.unquote executables. The absence of the ".bare" indicates an executable that loads "bossLib" as it starts. This provides a much richer logical environment (lists, natural numbers, pairs, options, disjoint sums), with additional tools too (arithmetic decision procedure, high-level definition principles).
The unquote filter is also better at handling Control-C interruptions. If in the middle of entering a input line that includes a delimiter (such as parentheses, various quotes etc), control-C causes the filter to completely forget that this has happened. This mimics the behaviour of Moscow ML's "native" interactive loop.
The installation procedure has been somewhat simplified. In particular, installation on Windows is easier.
Muddy wouldn't build on Linux if the binary distribution of Moscow ML was being used because of a lack of header files in an expected place. Thanks to Hasan Amjad for reporting this bug, which has been fixed.

A final note

We have retroactively decided to number HOL implementations in the following way:

HOL88 and earlier: implementations based on a Lisp substrate, with Classic ML.
HOL90: implementations in Standard ML, principally using the SML/NJ implementation.
HOL98 (Athabasca and Taupo releases): implementations using Moscow ML, and with a new library and theory mechanism.
HOL (Kananaskis releases and beyond)

With HOL 4, we do away with the habit of associating implementations with their year of origin. Individual releases within HOL 4 will retain the lake-number naming scheme.

HOL 4, Kananaskis-1