We are pleased to announce the Kananaskis-6 release of HOL 4.
The HolSmtLib
library now supports proof
reconstruction for the
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 nth 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.
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.
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.
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:
``:'a word``
``w1 * w2``
.
Multiplication by a literal is
okay, although this may introduce many additions.
``(exp1 -- exp2) w``
.
``w << exp``
.
``n2w exp``
and ``w2n w``
. Also w2s
, s2w
, w2l
and l2w
.
word_div
, word_sdiv
, word_mod
and word_log2
.
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.