Notes on HOL 4, Kananaskis-6 release

We are pleased to announce the Kananaskis-6 release of HOL 4.

New features
Bugs fixed
New theories
New tools
New versions
New examples
Incompatibilities

New features:

The HolSmtLib library now supports proof reconstruction for the SMT solver Z3. (Several other SMT solvers continue to be supported as oracles.)
The pretty-printer now uses colours to convey extra information about terms and types as they are printed. For example, bound term variables are printed in green, and free variables are printed in blue. This colouring will happen on colour terminals such as Unix xterm (also the standard MacOS Terminal application), as well as inside Emacs.

If you are using the Emacs mode, then the types of both sorts of variables are also available in a mouse-over tooltip. Moreover, the colours and printing-styles used in the Emacs mode for things like bound variables can be customised, using M-x customize.

Besides this automatic colored pretty-printing depending on the term structure, it is now possible to define syntax highlighting in userprinters.
Many type variables can now be parsed and printed as lower-case Greek letters. For example, you can input ``:'a``, and will get back ``:α``. You can also input type variables using the Greek letters (except for the letter λ). Underneath, the type variable still has the name with the apostrophe: this is a purely presentational change.
Bounded rewrites work better (a few bugs were fixed here), and there is now also an easy way to specify that a rewrite should only occur on the left or right side of a term. For example, to apply the theorem th twice, and on the left-hand side on an equality, use
```
         SIMP_TAC bool_ss [Ntimes th 2, SimpLHS]
```
To rewrite on the right-hand side:
```
         SIMP_TAC bool_ss [Ntimes th 2, SimpRHS]
```
It is also possible to rewrite on the left or right sides of operators other than equality. See the Description manual for details.
If the block of universally quantified variables at the head of a clause in the definition of an inductive relation contains duplicate names, Hol_reln detects this and provides an informative error message.
There are two new “document-level” modes for using HOL’s LaTeX-pretty-printing technology (originally due to Ramana Kumar and Thomas Türk). In both, terms, types and theorems become straightforward to embed in LaTeX documents. For example, one might write something like
```
        The term \HOLtm{p1 /\ q2} is a typical conjunction.
```
and have this turned into
```
        The term p₁ ∧ q₂ is a typical conjunction.
```
after LaTeX has been run. The ASCII conjunction has turned into a nice LaTeX maths symbol, and the term has been parsed, allowing variables to be printed in italic font, and with trailing digits sub-scripted.

See the Description manual for more detailed documentation.
Simplification of terms involving the EL operator (calculates the n^th element of a list) is better.
Some new syntax for various bag operations, including arithmetic symbols +, -, <, ≤ for the notions on bags that are just point-wise lifts of those operators on numbers (BAG_UNION, BAG_DIFF, PSUB_BAG, SUB_BAG).
New syntax for universal sets (in pred_setTheory). In ASCII mode, univ(:'a) is the universal set with elements drawn from type :'a. Another example: univ(:num) is the set of all natural numbers. With Unicode on, the first example prints as 𝕌(:α). The Unicode character used here (U+1D54C, a cute uppercase ‘U’) is beyond the BMP (Basic Multilingual Plane) and may not appear in many fonts. Rather than have to give up all of Unicode to get around this, there is an additional trace variable ("Unicode Univ printing") to turn off the use of this character, making the syntax use univ once more.
Of course, the old syntax (UNIV:'a -> bool, or UNIV:'a set) continues to work.
A new “vim mode” for controlling a HOL session from within the vim editor. This mimicks most of the important features of the Emacs mode. See tools/vim for a README file about this feature. Thanks to Ramana Kumar for the implementation of this tool.
If syntax that involves non-ASCII characters is added using add_rule, set_fixity or overload_on, it is only used if the Unicode flag is set. If the Unicode flag is toggled off and then on again, the Unicode syntax will disappear and reappear appropriately.
The persistent simpset (srw_ss(), also used in SRW_TAC) can now have named simpset fragments removed from it using the function diminish_srw_ss.
bin/build uses earlier (cached) options when not explicitly overridden. In particular, kernel specifications (-expk, and the new -stdknl), and build-sequence file specifications are cached in tools/lastbuildoptions so that one can subsequently do just bin/build to build again with those same options. To override a -seq foo option, you can use the -fullbuild option.
Other options (-symlink, -selftest) are not cached.
Users can configure their interactive sessions (setting output pretty-printing options with set_trace commands for example), by writing SML code into a .hol-config.sml file in their HOME directory. In fact, all of the following are acceptable names for the file: hol-config.sml, hol-config.ML, .hol-config, .hol-config.sml, and .hol-config.ML. The first of these that is found is used.
(The meaning of “the user’s home directory” is clear on Unix systems. On Windows, the environment variables HOMEPATH and APPDATA are consulted to determine where to look.)
The file, if it exists, is use-d into the interactive session, when it begins. A message is printed saying as much also.

Bugs fixed:

Type abbreviations used to be able to be applied to more type arguments than they were expecting. E.g.,
```
         type_abbrev("foo", ``:bool``)
```
followed by
```
         ``:'a foo``
```
used to work. No more!
Hol_reln now correctly accepts inductive definitions where type variables appear only in schematic variables.
Hol_reln now correctly accepts inductive definitions defining multiple (presumably multiply recursive) relations with schematic variables. Note that for a variable to be detected as schematic in this situation, it needs to be a parameter to all relations, even if it may not be used in all of them.
The syntax num$0 failed to parse. Thanks to Behzad Akbarpour for the report of this bug.
In Hol_datatype, nested recursion in record data types where the new type was also polymorphic failed. Thanks to Ramana Kumar for the report of this bug.
In Hol_datatype, nested recursion involving the itself type constructor could fail. Thanks to Ramana Kumar for the report of and fix for this bug.
The TypeNet data structure for indexing information by types could get confused if the “same” type was redefined (in the one interactive session) with different arities. Thanks to Ramana Kumar for the bug report that led to the isolation of this problem.

New theories:

A very simple theory string_numTheory demonstrating that strings and natural numbers are in bijection (with functions n2s and s2n constructively demonstrating this bijection).
A theory of trie-like trees that recurse under a finite map, fmaptreeTheory. This type can be used to represent recursive namespace-like environments.

New tools:

A new library HolQbfLib provides an interface to external Quantified Boolean Formulae (QBF) solvers. It can check certificates of invalidity generated by the QBF solver Squolem.
A bit-blasting conversion for operations on fixed-width words: BBLAST_CONV. This goes beyond the capabilities of WORD_BIT_EQ_CONV by expanding out additions and subtractions. This allows the new conversion to automatically handle small but tricky bit vector goals. For example:
```
         (x && 3w = 0w:word32) ==> ((x + 4w * y) && 3w = 0w)
```
and
```
         !a:word8. a <+ 4w /\ b <+ a /\ c <=+ 5w ==> (b + c) <=+ 7w
```
(These aren’t provable with wordsLib.WORD_DECIDE.)
Obviously bit-blasting is a brute force approach, so the new conversion should be used with care. It will only work well for smallish word sizes and when there is only and handful of additions around. It is also “eager”—additions are expanded out even when not strictly necessary. For example, in
```
         (a + b) <+ c /\ c <+ d ==> (a + b) <+ d:word32
```
the sum a + b is expanded. Users may be able to achieve speed-ups by first introducing abbreviations and then proving general forms, e.g.
```
         x <+ c /\ c <+ d ==> x <+ d:word32
```
The conversion handles most operators, however, the following are not covered or interpreted:
- Type variables for word lengths, i.e. terms of type ``:'a word``
- General multiplication, i.e. ``w1 * w2``. Multiplication by a literal is okay, although this may introduce many additions.
- Bit field selections with non-literal bounds, e.g. ``(exp1 -- exp2) w``.
- Shifting by non-literal amounts, e.g. ``w << exp``.
- ``n2w exp`` and ``w2n w``. Also w2s, s2w, w2l and l2w.
- word_div, word_sdiv, word_mod and word_log2.

New versions:

New examples:

A development of some basic computability theory:
- a development of λ-terms as computable functions, showing that things like Church-numerals are as powerful as one would like, and that λ-terms can indeed be set up to evaluate suitably encoded λ-terms (thereby providing a Universal Machine);
- a development of primitive recursive and recursive functions doing much the same;
- a demonstration that both models can emulate each other;
- definition of concepts of recursive, and recursively-enumerable sets; and
- some standard results, including: the Halting Problem, Rice's Theorem, the Recursion theorem, that recursive sets are closed under union and complementation, that r.e. sets are closed under union and intersection but not complement, and that if a set and its complement are both r.e. then they are both recursive.

Incompatibilities:

Drule.CONJUNCTS_CONV (proving equivalence of conjunctions under associativity, commutativity and idempotence) has been renamed to Drule.CONJUNCTS_AC.
Drule.CONJ_SET_CONV and Drule.FRONT_CONJ_CONV have been removed. Their functionality can easily be derived from Drule.CONJUNCTS_AC.
The overload <> on words$word_slice has been removed and replaced with ''.
The interface of userprinter (user defined pretty printers) changed. Instead of getting just two functions add_string and add_break, it now gets a record of type term_pp_types.ppstream_funs that contains these functions as well as several others.
The type of the filter field of the SSFRAG function for constructing simpset fragment values has changed from (thm -> thm list) option to (controlled_thm -> controlled_thm list) option, where a controlled theorem value is a pair of a theorem and a control indicating how many times the rewrite is allowed to be applied. See the REFERENCE and the BoundedRewrites module for details.
The Unicode structure is now a sub-structure of Parse, due to some significant code-reorganisation. This means that a line such as
```
         open Parse boolLib Unicode
```
will fail. Instead it must be
```
         open Parse boolLib
         open Unicode
```
The constant INFINITE in pred_setTheory has been replaced by an abbreviation. Thus, if one types ``INFINITE s``, the underlying term is really ¬FINITE s. All instances of this pattern will print as INFINITE s. The functions mk_infinite, dest_infinite and is_infinite in pred_setSyntax continue to work and do the “right thing”, the entrypoint infinite_tm in the same module has been removed.

Notes on HOL 4, Kananaskis-6 release

Contents

New features:

Bugs fixed:

New theories:

New tools:

New versions:

New examples:

Incompatibilities: