We are pleased to announce the Kananaskis-7 release of HOL 4.
proof reconstruction also for goals that involve fixed-width words,
based on bit-blasting (cf.
blastLib) and other word
HolSmtLib provides a translation from HOL into
format. (Support for SMT-LIB 1.2 has been
HolQbfLib supports checking both validity and
invalidity certificates for Squolem 2.02. (Support for Squolem 1.x has
been discontinued. Incompatibility.)
wordsSyntax.mk_word_replicate computes the width
of the resulting word when applied to a numeral and a fixed-width
word. Minor incompatibility.
numLib.MOD_ss simpset fragment simplifies a number of expressions involving natural number modulus (
(7*x + 3) MOD 2 will automatically simplify to
(x + 1) MOD 2.
User pretty-printers now have to be of a different type.
This incompatibility affects the function
Users have to write their pretty-printers in a monadic style, where pretty-printing components are linked with an infix
The advantage of the new system is that it gives pretty-printers access to information about which variables are bound and free, and the ability to change this status when making recursive calls to the built-in printer.
It will also be easier to extend the system with new functionality along the same lines.
The system supports syntax for decimal fractions (e.g.,
This syntax maps to division terms of the form n / 10m.
3.012 maps to the term
3012 / 1000.
This transformation is reversed by the pretty-printer.
In the core system, this syntax is enabled for the real, rational and complex theories.
numSimps.REDUCE_ss no longer diverges on certain
There is now LaTeX notation for the operation of cross-product on sets (written A × B), and for the numeric pairing function (written n ⊗ m).
The lexer now tokenizes the input
Also handle occurrences of such strings in
Theory.sig files, which can cause them to become invalid SML.
When making definitions with
Hol_defn, and others), one can now use the boolean equivalence syntax (
⇔), not just
SimpR directives for controlling the position of simplification were only working with binary relations, not functions (such as
Thanks to Ramana Kumar for the report of the bug.
Fix type-parsing bug when array suffixes and normal suffixes (such as
list) interact. Now, both
:bool list and
:bool list parse correctly.
The theory of transcendental functions (
has been extended with a treatment of exponentiation where exponents
can be of type
:real. This is implemented by the (infix)
rpow. (The existing function
requires a natural number as the exponent.) Thanks to Umair Siddique
for the definition and theorems.
A formalisation of the complex numbers (
complexTheory) by Yong Guan, Liming Li, Minhua Wu and Zhiping Shi.
The authors referred to the HOL Light theory by John Harrison and the theory in PVS.
It includes treatments of the complex numbers in the real pair form, the polar form and the exponential form, with basic arithmetic results and some other theorems.
A theory of relations based on sets of pairs (
Most of the theorems are about orders, including Zorn’s lemma, and a lemma stating that “stream-like” partial orders can be extended to “stream-like” linear orders.
Also add a theorem to
llist that “stream-like” linear orders can be converted into lazy lists.
Thanks to Scott Owens for this development.
A few extra tools in
These can be used to simplify applications of unary/binary minus, introducing or eliminating subtractions where possible.
These must not be used simulataneously with
WORD_ss (as this will likely result in non-termination).
However, can be used to good effect afterwards.
wordsLib.WORD_SUB_CONV ``a + -1w * b`` |- a + -1w * b = a - b wordsLib.WORD_SUB_CONV ``-(a - b)`` |- -(a - b) = b - a wordsLib.WORD_SUB_CONV ``a + b * 3w : word2`` |- a + b * 3w = a - b wordsLib.WORD_SUB_CONV ``192w * a + b : word8`` |- 192w * a + b = b - 64w * a
Convert division by a power of two into a right shift. For example:
wordsLib.WORD_DIV_LSR_CONV ``(a:word8) // 8w`` |- a // 8w = a >>> 3
MOD by powers of two into application of BITS.
wordsLib.BITS_INTRO_CONV ``(a DIV 4) MOD 8``; |- (a DIV 4) MOD 8 = BITS 4 2 a wordsLib.BITS_INTRO_CONV ``(a MOD 32) DIV 8``; |- a MOD 32 DIV 8 = BITS 4 3 a wordsLib.BITS_INTRO_CONV ``a MOD 2 ** 4``; |- a MOD 2 ** 4 = BITS 3 0 a wordsLib.BITS_INTRO_CONV ``a MOD dimword (:'a)``; |- a MOD dimword (:'a) = BITS (dimindex (:'a) - 1) 0 a
Attempts to convert goals of the form
``a = b``,
``a < b`` and
``a <= b`` into goals of the form
``n2w a = n2w b``,
``n2w a <+ n2w b`` and
``n2w a <=+ n2w b``.
The integer argument denotes the required word size.
This enables some bounded problems (over the naturals) to be proved using bit-vector tactics.
For example, the goal:
`((11 >< 8) (imm12:word16) : word12) <> 0w ==> ((31 + 2 * w2n ((11 >< 8) imm12 : word12)) MOD 32 = w2n (2w * (11 >< 8) imm12 + -1w : word32))`
can be solved with
STRIP_TAC THEN n2w_INTRO_TAC 32 THEN FULL_BBLAST_TAC
A mechanisation of first-order and nominal unification done in an accumulator-passing style with
Some basic category theory (up to the Yoneda lemma), including two categories of
sets: one using HOL sets (predicates) and one using the axiomatically introduced type from
Lib.itotal removed; use
instead. Note that
handle _ is harmful:
Interrupt should never be handled without being
The ugly situation whereby we had fixities called
Prefix really encoded an absence of fixity, has been done away with.
Now the fixity
Prefix codes for what used to be
TruePrefix, and in relevant situations where a
fixity value was required, a
fixity option can be provided instead.
In this situation
NONE is used to indicate the absence of a fixity.
set_fixity takes a
fixity, not a
fixity option, so its old ability to remove fixities has disappeared.
If you wish to do this, you should use the function
HOL 4, Kananaskis-7