We are pleased to announce the Kananaskis-7 release of HOL 4.
HolSmtLib
supports Z3
proof reconstruction also for goals that involve fixed-width words,
based on bit-blasting (cf. blastLib) and other word
decision procedures.
HolSmtLib provides a translation from HOL into
SMT-LIB 2
format. (Support for SMT-LIB 1.2 has been
discontinued. Incompatibility.)
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.
The new numLib.MOD_ss simpset fragment simplifies a number of expressions involving natural number modulus (MOD).
For example, (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 add_user_printer.
Users have to write their pretty-printers in a monadic style, where pretty-printing components are linked with an infix >> connective.
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., 3.021).
This syntax maps to division terms of the form n / 10m.
Thus 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
terms.
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 ``"(*"`` correctly.
Also handle occurrences of such strings in Theory.sig files, which can cause them to become invalid SML.
When making definitions with Define (and Hol_defn, and others), one can now use the boolean equivalence syntax (<=> or ⇔), not just =.
The SimpL and SimpR directives for controlling the position of simplification were only working with binary relations, not functions (such as +, say).
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[32] list and :bool list[32] parse correctly.
The theory of transcendental functions (transcTheory)
has been extended with a treatment of exponentiation where exponents
can be of type :real. This is implemented by the (infix)
function rpow. (The existing function pow
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 (set_relationTheory).
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 wordsLib:
WORD_SUB_CONV / WORD_SUB_ss
These can be used to simplify applications of unary/binary minus, introducing or eliminating subtractions where possible.
These must not be used simulataneously with srw_ss, WORD_ARITH_ss or WORD_ss (as this will likely result in non-termination).
However, can be used to good effect afterwards.
For example:
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
WORD_DIV_LSR_CONV
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
BITS_INTRO_CONV / BITS_INTRO_ss
These convert DIV and MOD by powers of two into application of BITS.
For example:
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
n2w_INTRO_TAC <int>
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 triangular
substitutions.
In examples/unification/triangular.
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 zfsetTheory.
In examples/category.
Lib.itotal removed; use Lib.total
instead. Note that handle _ is harmful:
exception Interrupt should never be handled without being
re-raised.
Lib.gather removed;
use {Lib,List}.filter instead.
The ugly situation whereby we had fixities called Prefix and TruePrefix, but 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.
The function 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 remove_rules_for_term.