HOL4/doc/kananaskis-1.release.html

<HTML>
<HEAD>
<TITLE>Release Notes for Kananaskis-1 version of HOL 4</TITLE>
</HEAD>

<BODY bgcolor=white>
<H1>Notes on HOL 4, Kananaskis-1 release</H1>

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

<UL>
<LI> formalizing mathematics,
<LI> verifying hardware and software, and
<LI> constructing custom proof tools.
</UL>

And now the news.
<P>
<HR>

<H2>Change of Base</H2>

We have moved our base of operations to SourceForge.
<PRE>
     http://sourceforge.net/projects/hol/
</PRE>
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.
<P>
 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 <EM>not</EM> 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.

<P><HR>

<H2>Documentation Improved</H2>

 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
<PRE>
   <holdir>/help/HOLindex.html
</PRE>
gives organized access to

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

<P><HR>
<H2>New Examples</H2>


<UL>
<LI> <strong>ARM6</strong> --
     Anthony Fox has formalized version 6 of the Acorn Risc
            Machine and completed a proof of its correctness.
<P>

<LI><strong>Sugar2</strong> --
   Mike Gordon has deeply embedded Sugar 2.0, the Accellera
            standard property language.

<P>
<LI> <strong>miller</strong> --
        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.
<P>

<LI> <strong>Rijndael</strong> --
       Konrad Slind has formalized and proved the functional
            correctness of Rijndael, the new AES crypto algorithm.

<P>
<LI> <strong>root2</strong> --
      A short introductory example showing that the square root
      of 2 is irrational. Adapted from a proof of John Harrison.
</UL>


<P><HR>
<H2>New and improved proof tools</H2>

<UL>
<LI> Another complete decision procedure for full Presburger arithmetic
    over the integers and natural numbers, the <em>Omega Test</em>, 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 <kbd>intLib</kbd> as <kd>intLib.ARITH_CONV</kbd>.
<P>
<LI> Induct and Induct_on have been improved to deal with mutually
    recursive datatypes, thanks to code written by Peter Homeier.
<P>
<LI> Hol_datatype's definition of large "enumerated types" (data types
    with only nullary constructors) is now much more efficient than
    it used to be.
<P>

<LI> 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)
<PRE>
         EVAL ``FACT 6``
</PRE>
    and getting back
<PRE>
         > val it = |- FACT 6 = 720 : thm
</PRE>
    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.
<P>

<LI> 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
<PRE>
       srw_ss : unit -> simpset
</PRE>
    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
<PRE>
      |- FINITE (P UNION Q) = FINITE P /\ FINITE Q
</PRE>
    as well as the SET_SPEC_CONV conversion which does the right thing
    with
<PRE>
      x IN { ... | ... }
</PRE>
    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.
<P>

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

<LI> 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.
</UL>

<P><HR>
<H2>New libraries</H2>

<UL>
<LI> 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.
<P>

<LI> The library word32Lib comprises a functor (called "wordFunctor")
    for creating word theories. It also provides word32Theory (see below),
    plus an evaluation conversion "WORD32_CONV".
</UL>

<P><HR>
<H2>New and improved theories</H2>

<UL>
<LI> Laurent Thery's theories of divisibility, primality, and gcd are
    now part of the distribution, under the name dividesTheory,
    primeTheory and gcdTheory.
<P>

<LI> 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:

<UL>
<LI> Bit-field testing and extraction;
<LI> Arithmetic: Addition, Subtraction, Multiplication and Two's
      Complement;
<LI> Logical: One's Complement, Bitwise And, Or and Exclusive Or;
<LI> Shifts: Logical Right, Arithmetic Right, Rotate Right, and
      Rotate Right One Place with Carry Extension.
</UL>
<P>
    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).
<P>
    The functor <strong>wordFunctor</strong> can be used to create
    bespoke word theories. For example, a theory of 8-bit words can be
    obtained by the invocation
<PRE>
      structure word8Theory = wordFunctor (val bits = 8)
</PRE>

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

<LI> A small theory of set-theoretic fixpoints, due to Michael Norrish.

<P>
<LI> A small theory supporting relatively efficient definitional CNF, due
    to Joe Hurd.
<P>

<LI> A small theory of container types, offering maps between lists,
    finite sets, and multisets (bags).
<P>

<LI> relationTheory now defines the constants RTC and RC (reflexive and
    transitive closure, and reflexive closure) and proves a variety of
    properties about them.
<P>

<LI> Restricted quantification now uses predicate sets, so the meaning of
    the term
<PRE>
       !x::P. Q x
</PRE>
    is
<PRE>
       !x. x IN P ==> Q x.
</PRE>
    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.
</UL>

<P><HR>
<H2>Improved support for large formalizations</H2>

<UL>
<LI> Holmake will now read and act under the supervision of make-files
    (usually named <strong>Holmakefile</strong>). 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 <strong>Holmake</strong> section of
    the <strong>DESCRIPTION</strong>.
</UL>

<P><HR>
<H2>New syntax support</H2>

<UL>
<LI> 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
<PRE>
       bool$/\
</PRE>
    is the conjunction operator in boolTheory, and
<PRE>
       :num$num
</PRE>
    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
<PRE>
        {Name:string, Thy:string, Ty:hol_type} -> term
</PRE>
    and the function <kbd>dest_thy_const</kbd> inverts this.
    <kbd>mk_const</kbd> remains in the system, but its behaviour is
    unspecified when two or more constants have the same name.
<P>

<LI> Type abbreviations can now be introduced using the function
    <kbd>Parse.type_abbrev</kbd>.  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
<PRE>
        type_abbrev("set", ``:'a -> bool``)
</PRE>
    is used in <kbd>pred_setTheory</kbd> 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.

<P>
<LI> Syntax for ML-style case expressions is now supported.  The same
    patterns supported by <kbd>Define</kbd> are allowed.  Some examples
    of the syntax:
<PRE>
        case n of 0 -> x || SUC n -> n + 1
</PRE>
    and
<PRE>
        case p of (x, []) -> x + 1
               || (y, h::t) -> y + h
</PRE>
</UL>

<P><HR>
<H2>Modified syntax support</H2>

<UL>
<LI> The system now compiles files with common HOL infix declarations
    already in scope.  This means that one need no longer write
<PRE>
       infix THEN THENL ...
</PRE>
    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.

<P>
<LI> We have rationalised the ML API.  By default, just about all
    functions use "paired" syntax, rather than "record" syntax.  So,
    mk_var has type
<PRE>
      string * hol_type -> term
</PRE>
    rather than
<PRE>
      {Name : string, Ty : hol_type} -> term
</PRE>
    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
    |-&gt; function can be used to construct such records.)

<P>
<LI> 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
<PRE>
        overload_on ("foo", ``bar``);
</PRE>
<P>

<LI> The names of record fields are not now overloaded to the accessor
    function.  This function needs to be accessed as the constant
<PRE>
      &lt;rcd-type-name&gt;_&lt;fldname&gt;
</PRE>
    E.g., "rcd_fld". If you really like the 'dot' syntax, you can
    always write
<PRE>
      \r. r.fld
</PRE>
    which eta-converts to the above.
<P>

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

<LI> 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.
</UL>

<P><HR>

<H2>"Gratuitous" and probably irritating incompatibilities</H2>

<UL>
<LI> There is no longer any module called basicHol90Lib.  Instead,
    proof scripts should open boolLib.

<P>
<LI> 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
<PRE>
      val INTER_ASSOC = GSYM INTER_ASSOC
      val UNION_ASSOC = GSYM UNION_ASSOC
</PRE>
    before the references to these theorems occur.
<P>

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

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

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

<LI> Eta-conversion used to be part of std_ss, but it has been removed.
    This may break some proofs.

<P>
<LI> 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
<PRE>
      theorems ()
</PRE>
    should thus be replaced with
<PRE>
      theorems "-"
</PRE>
</UL>

<P><HR>

<H2>Miscellaneous</H2>

<UL>
<LI> There are now four (4!) hol executables.  They are:
<PRE>
      hol, hol.bare, hol.unquote, and hol.bare.unquote
</PRE>
    all found in the bin/ directory.  We recommend hol.unquote as the
    standard starting point.
<P>
    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).

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

<P>
<LI> The installation procedure has been somewhat simplified. In
    particular, installation on Windows is easier.

<P>
<LI> 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.
</UL>

<P><HR>

<H2>A final note</H2>

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

<LI> <strong>HOL88</strong> and earlier: implementations based on a Lisp
      substrate, with Classic ML.

<LI> <strong>HOL90</strong>: implementations in Standard ML, principally
      using the SML/NJ implementation.

<LI> <strong>HOL98</strong> (Athabasca and Taupo releases):
      implementations using Moscow ML, and with a new library and theory
      mechanism.
<LI> HOL (Kananaskis releases and beyond)

</OL>
  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 <em>lake</em>-<em>number</em> naming scheme.
</BODY></HTML>
<P>
<HR>
<EM><A HREF="http://hol.sourceforge.net/">
    HOL 4, &nbsp;Kananaskis-1
</EM>
</BODY>
</HTML>