[Hol-info] HOL4 Kananaskis-3 Released

[Michael N. <Mic...@ni...>]

We're pleased to announce the release of the latest version of the
HOL4 theorem-proving system, Kananaskis-3.  It is available for
download from

  http://hol.sourceforge.net

A source tarball is available for all platforms (Unixes, Windows and
Mac OS 10), as well as a Windows self-extracting archive executable.

----------------------------------------------------------------------

                     Notes on HOL 4, Kananaskis-3 release

New features:

     * Configuration and installation of the system is easier. Instead =
of
       having to edit configure.sml yourself, just pipe
       tools/smart-configure into mosml as the first step of installati=
on
       (before build):

         mosml < tools/smart-configure.sml

     * The term and type parsers now report errors with an indication a=
s
       to where in the parse they have occurred. If the error is found
       during a run of Holmake, the location includes the line number i=
n
       the file where the error is. Pragma comments of the form
       (*#loc 100 5*) allow the line and column numbers to be overridde=
n,
       =E0 la C's #line directive. (Many thanks to Keith Wansbrough for=
 the
       implementation of this feature.) The lexer is also much faster
       than it used to be.

     * The system better distinguishes interactive and non-interactive
       use (the latter occurs with building things with Holmake).
       Diagnostic output is now rather different in non-interactive mod=
e.
       Holmake comes with a new -i or --interactive flag to flip the
       underlying flag back to interactive, if you want to see
       "interactive mode" output.

     * Holmake now supports the use of user-specified variables, in a
       manner analogous to that done by traditional make implementation=
s.
       For example, one can define a variable OBJS,

         OBJS =3D foo bar baz

       and then refer to this variable elsewhere by writing $(OBJS)
       Holmake also provides some functions like those in GNU make for
       manipulating text (performing pattern-based substitutions, for
       example). See the DESCRIPTION for more details.

     * Performance when defining large record types (where the number o=
f
       fields is greater than a user-adjustable reference variable), is=

       now much improved. Part of this change was to remove update
       functions as separate constants (they are now encoded using
       functional update functions), though the concrete syntax remains=
=2E
       See the DESCRIPTION for more details.

     * In addition to the traditional $-prefix for making identifiers
       ignore their status as special forms in the grammar, HOL now
       supports the Caml method of enclosing identifiers in parentheses=
=2E
       Thus, instead of

         $/\ p

       one can also write

         (/\) p

       By default, the pretty-printer continues to print using the old
       $-syntax. This can be changed by setting the trace variable
       "pp=5Fdollar=5Fescapes".

     * Pretty-printing of "list forms" (e.g., lists, sets and bags) is
       now under more user-control. See the REFERENCE (or online help)
       for add=5Flistform, whose type has changed, for more detail on t=
his.
       (Thanks to Lockwood Morris for this feature suggestion.)

     * There are two new simpset fragments in realSimps. REAL=5FREDUCE=5F=
ss
       performs calculations over ground rational values. Thus,

         SIMP=5FCONV (std=5Fss ++ REAL=5FREDUCE=5Fss) [] ``1/3 - 3/7``

       returns

         > val it =3D |- 1 / 3 - 3 / 7 =3D ~2 / 21 : thm

       When realSimps is loaded, REAL=5FREDUCE=5Fss is automatically ad=
ded to
       the stateful-rewriting simpset, and bossLib's EVAL is also
       augmented with this functionality. This code also removes common=

       factors from fractions even when there are no other arithmetic
       operations being performed.

       The second simpset fragment in realSimps is REAL=5FARITH=5Fss, w=
hich
       embodies the RealArith decision procedure for universal Presburg=
er
       arithmetic over the real numbers.

     * The simplifier now provides simpler interfaces for the addition =
of
       AC-rewriting and congruence rules. They can be added as if norma=
l
       rewrites with the functions simpLib.AC and simpLib.Cong. Thus,

         - SIMP=5FCONV bool=5Fss [AC ADD=5FCOMM ADD=5FASSOC] ``3 + x + =
y + 1``;
         > val it =3D |- 3 + x + y + 1 =3D x + (y + (1 + 3)) : thm

       Cong is used similarly. Both functions are further described in
       the REFERENCE.

     * Holmake now supports a new command-line option --logging, which
       tells it to record running times for the building of theories.
       These times are stored in a file in the current directory. See t=
he
       DESCRIPTION for more details.

     * Support for abbreviations in goals, via tactics such as
       Q.ABBREV=5FTAC, is now a deal richer. Abbbreviations are now
       specially marked as such in a goal's assumptions, protecting the=
m
       against being removed by tactics such as RW=5FTAC or SRW=5FTAC. =
There
       are also new tactics for establishing abbreviations, such as
       MATCH=5FABBREV=5FTAC and PAT=5FABBREV=5FTAC. For more on these a=
nd other
       new tactics, see the REFERENCE (or the online help).

       To support old code, the old implementations of these tactics ar=
e
       available in a structure OldAbbrevTactics. Thus, it is possible =
to
       restore a file to its old behaviour by including:
         structure Q =3D struct open Q open OldAbbrevTactics end;
       at the top of an affected file.

Bugs fixed:

     * Hol=5Fdatatype would fail if called on to define a type with a
       single nullary constructor.

     * pred=5FsetLib.UNION=5FCONV (and other functions in this library)=

       failed to work as advertised. (Thanks to Lockwood Morris for the=

       report of this bug.)

     * It was too easy to do significant parser things before a
       new=5Ftheory declaration, causing these effects not to persist w=
ith
       the export of the theory. Now, attempting to do this causes a
       strong warning to be issued.

     * let terms with bodies that were abstractions didn't print
       correctly.

     * The type grammar didn't print stored type abbreviations correctl=
y.

     * Adding a user-supplied pretty-printer caused polymorphic terms t=
o
       fail to print. (The interface for adding pretty-printers is also=

       now slightly richer, see the REFERENCE manual for details.)

     * DECIDE=5FTAC didn't pay attention to goal assumptions.

     * A bug in ARITH=5FCONV's handling of conditional expressions caus=
ed
       some quantified goals to fail to be proved.

     * The lexer got confused if a token made up of non-aggregating
       characters (e.g., including ";") was used, but not as part of
       special concrete syntax. I.e., ;; was OK as an infix, but not as=
 a
       normal constant. (Thanks to Klaus Schneider for the report of th=
is
       bug.)

     * SPEC=5FVAR and theory export caused bound variables with the sam=
e
       name as constants to get changed. (Thanks to Lockwood Morris for=

       the report of this bug.)

     * Many, many documentation typos and bugs were fixed. (Thanks to
       Carl Witty for the report of most of these.)

     * Two fixes for the simplifier's implementation of congruence rule=
s.
       With deep nesting, congruence rules could lead to an exponential=

       increase in time taken. Also, terms that included variables used=

       in a rule's statement could cause the rule to fail to fire.

     * The simplifier's AC-rewriting could cause it to go into an
       infinite loop. While the new behaviour does AC-normalise
       everywhere (we hope!), it is not necessarily the same as the old=

       behaviour on examples which used to work. (Thanks to Tobias Nipk=
ow
       for useful discussion about this bug.)

     * pairLib.PAIRED=5FETA=5FCONV was broken. Thanks to Viktor Sabelfe=
ld for
       the bug report.

     * Q.UNDISCH=5FTHEN was behaving more as if it were Q.PAT=5FUNDISCH=
=5FTHEN;
       it was finding matches in the assumptions rather than equal term=
s.
       Thanks to Lockwood Morris for the bug report.

     * The order in which type arguments appeared as arguments to
       polymorphic type operators defined by Hol=5Fdatatype was previou=
sly
       undefined. For example, if one wrote:

         Hol=5Fdatatype `sum =3D left of 'a | right of 'b`;

       it was not specified that ('a,'b)sum was the type which associat=
ed
       the variable 'a with the left constructor. Now, the type picks u=
p
       the type variable arguments in Hol=5Fdatatype in alphabetical or=
der.
       This may break code that relied on what was an unspecified
       behaviour.

     * The quotation filter didn't recognise text of the form

         ``:
             foo
         ``

       with a newline immediately following the colon as a type
       quotation. (Thanks to Steve Brackin for the report of this bug.)=


New theories:

     * A theory of co-inductive (possibly infinite) labelled transition=

       paths in pathTheory.
     * A theory of sorting and list permutations in sortingTheory.

New tools:

     * A new first-order proof tactic (called METIS=5FTAC) that uses
       ordered resolution and paramodulation, specifically tailored for=

       subgoals that require equality reasoning.

     * A `boolification' tool that automatically defines functions that=

       map datatypes to boolean vectors. These kind of functions are
       needed for sending HOL subgoals to a model-checker or SAT solver=
=2E

New examples:

     * An extension of the existing lambda calculus example
       (examples/lambda) to include mechanisations of chapters 2 & 3 of=

       Hankin's lambda calculus text, and the standardisation theorem
       from Barendregt's chapter 11.

     * A formalization of the probabilistic guarded command language
       (pGCL) in higher-order logic, including a tool for deriving
       sufficient verification conditions for partial correctness.

Incompatibilities:

     * The four HOL executables have had their names adjusted. We now
       think that using HOL with the quotation filter is the appropriat=
e
       default for all users. To reflect this, the executable hol now
       includes the quotation filter. (This executable used to be calle=
d
       hol.unquote.) To avoid using the quotation filter, use
       hol.noquote. Analogous changes have been made to hol.bare; i.e.,=

       hol.bare now includes the filter, and hol.bare.noquote does not.=


     * The rewrite theorem for LET,

         LET f v =3D f v

       has been removed from std=5Fss and later simplification sets.
       (Simpsets arith=5Fss, list=5Fss and srw=5Fss() are all affected.=
)
       Old behaviours can be restored with code such as

         val std=5Fss =3D std=5Fss ++ simpLib.rewrites [LET=5FTHM]

     * Rewrite rules for arithmeticTheory's MIN and MAX constants have
       been made more general; they will now match more often. For
       example, MIN=5FLE has changed from

         m <=3D MIN m n =3D m <=3D n

       to

         p <=3D MIN m n =3D p <=3D m /\ p <=3D n

     * For reasons of efficiency, all conversions in the system may now=

       potentially raise the special exception Conv.UNCHANGED to indica=
te
       that they haven't changed the input term, and that they should b=
e
       treated as if they had returned the theorem |- t =3D t, for inpu=
t t.
       Conversion connectives (such as THENC, ORELSEC and TRY=5FCONV) a=
ll
       do the appropriate thing in the presence of this exception.

       Previously, sub-systems such as the simplifier, rewriter and
       arithmetic decision procedures have used this idea to make them
       work faster, but couldn't share information about unchangedness.=


       For interactive use, CONV=5FRULE and CONV=5FTAC handle the excep=
tion
       appropriately, and the new function QCONV (of type : conv -> con=
v)
       can make any conversion handle UNCHANGED. QCONV's implementation=

       is

         fun QCONV c t =3D c t handle UNCHANGED =3D> REFL t

       If you have code implementing conversions of your own, you may
       need to fix code if it uses the following idiom:

         fun myconv t =3D
           let val th =3D someconv t
               val ..  =3D <fiddle with th>
           in
               <resulting theorem>
           end

       If someconv raises UNCHANGED, then myconv will too, causing
       expressions such as

         myconv THENC <something else>

       to treat myconv as if it hadn't done anything (because the
       <fiddle with th> code never got called).
       This can be relatively difficult to track down, but the fix is
       simple enough: change someconv t to QCONV someconv t.

     * The constant LIST=5FTO=5FSET is now defined in listTheory.

     * The word32 theory is not built by default. Instead, a general
       wordn-theory creating executable, mkword.exe is available in the=

       hol/bin/ directory. This can be invoked to create word theories =
of
       various sizes. For example,

         $ mkword.exe 32

       will create a word32Theory in the current directory. These new
       theories don't have corresponding Script files, so Holmake doesn=
't
       automatically update these theories. If this is a concern, the
       Holmakefile in hol/src/n=5Fbit/help/Holmakefile.example-32
       demonstrates how to ensure word theories are rebuilt.

     * The type simpLib.ssdata is now called simpLib.ssfrag and the
       constructor for this type that used to be called SIMPSET is now
       called SSFRAG.
     =5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=
=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=
=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F=5F