{ x + y | x < y }as the set that takes all pairs of numbers such that the first component is less than the other, and then sums them (generating the set of all non-zero numbers). The new notation allows one to specify that only the
x
should vary by writing
{ x + y | x | x < y }This denotes the set of numbers from
y
up to but not
including 2 * y
. To express the first set
in the new notation, one would write
{ x + y | x,y | x < y }The parser accepts both notations. The pretty-printer prefers the old notation unless it can not express the set being printed. Further details are in the Description. Thanks to John Harrison for discussion leading to the adoption of this syntax.
The syntax of string and character literals is now the same as
that accepted by SML. This means that escapes such as
\n
(for the linefeed character) and
\^E
(for ASCII character no. 5) can be used
inside string and character literals.
The SML syntax which allows strings to be broken over new-lines by using back-slashes is also supported. This means that one can write
``mystring = "the quick brown fox jumps over \ \the lazy dog"``
and have the actual string value generated exclude the white-space appearing between the back-slashes.
It is possible to include both ^
(caret) and
`
back-tick characters inside quotations. Usually
these characters have special meaning inside quotations: caret
is used to introduce an antiquotation, and the back-tick is used
to end a quotation (singly or doubly, depending on the sort of
quotation). The caret character can be used as is if a
sequence of them is followed by white-space. Otherwise, it
needs to be “escaped” by preceding it with another
caret character. Similarly, the backquote character can be
written by escaping it with a caret. For example, writing
``s1 ^ s2``
will result in the string s1 ^ s2
being passed
to the HOL parser. This string will then be treated in the
standard fashion. E.g., if ^
is an infix, a
function application with it as the head operator will be
created. If one wrote ``s1 ^^ s2``
this would also
pass through unchanged. However, if one wrote
``s1 ^s2``
this would be taken as an anti-quotation of SML variable
s2
. One should write
``s1 ^^s2``
to get the single caret passed to the underlying lexer.
Note that the back-quote character always needs to be escaped by a caret, and that caret-escapes need to be applied even within string literals and comments that occur inside quotations.
The XEmacs editor is now supported, in addition to Emacs,
by the tools/hol98-mode.el
file of Emacs
extensions.
Case expressions may now include literals as patterns,
in addition to constructor expressions as in the past. These
literals may be for example of types num
,
char
, or string
;
or they may be of any other type as well, even function types.
Literals need not be constants, but they must not contain
any free variables.
case n of 0 -> "none" || 1 -> "one" || 2 -> "two" || _ -> "many"
Patterns in case expressions are similar to the patterns used
in the definition of recursive functions by Define
.
Thus they may be deeply nested within larger patterns.
As before, in case of overlapping patterns, the earliest
listed pattern is matched.
If the set of patterns specified is sparse, there may be new
rows generated automatically to fill it out, and possibly some new
or renamed variables or the ARB
constant to properly
represent the case expression.
- ``case a of (1, y, z) -> y + z || (x, 2, z) -> x - z || (x, y, 3) -> x * y``; > val it = ``case a of (1,2,3) -> 2 + 3 || (1,2,z) -> 2 + z || (1,y,3) -> y + 3 || (1,y,z) -> y + z || (x,2,3) -> x - 3 || (x,2,z') -> x - z' || (x,y',3) -> x * y' || (x,y',z') -> ARB`` : term
A complex pattern with several components may include
both literals and constructor expressions as subpatterns.
However, a set of patterns specified in a case expression
may not have both literals and constructor expressions as
alternatives to each other, except insofar as a pattern
may be both a literal and a (0-ary) constructor, such as
the literal 0
. See the Description for more
information and examples of case expressions.
Inductive definitions are now made with respect to a
varying “monoset
”: a list of theorems
specifying that boolean operators are monotone in their
arguments. These are used to justify recursions that may occur
underneath new operators that users introduce.
Initially, this set includes results for the standard
boolean operators (such as existential quantification and
conjunction), and is augmented as later theories are loaded. For
example, the constant EVERY
in the theory of lists,
has a monotonicity result
|- (!x:'a. P x ==> Q x) ==> (EVERY P l ==> EVERY Q l)
and this is incorporated into the global monoset
when
the theory of lists is loaded. This then allows the easy definition
of relations that recurse under EVERY
, as in this rule
!x. EVERY newrel (somelist_of x) ==> newrel x
Theorems can be declared as monotonicity results using the
export_mono
function. See the Description for the
exact form that monotonicity theorems must take.
Types that are instances of abbreviation patterns (made with
type_abbrev
) now print in abbreviated form by
default. For example, if one writes
type_abbrev("set", ``:'a -> bool``);
Then, as before, one can write ``:num set``
and
have this understood by the type parser. Now, in addition, when
types are printed, this is reversed, so that the following
works:
- type_of ``(UNION)``; > val it = ``:'a set -> 'a set -> 'a set`` : hol_type
Unfortunately, with this particular example, one also gets
- type_of ``(/\)``; > val it = ``:bool -> bool set`` : hol_type
which is more confusing than it is illuminating. For this
reason, it is possible to turn abbreviation printing off
globally (using a trace
variable,
print_tyabbrevs
), or on an
abbreviation-by-abbreviation basis. The latter is done with the
function
disable_tyabbrev_printing : string -> unit
Calls to this function are made in the pred_set
and bag
theories so that those theories’
abbreviations (set
, bag
and
multiset
) are not printed.
There is a new polymorphic type,
``:'a itself``
containing just one value for
all possible instantiations of ``:'a``
. This value
is supported by special syntax, and can be written
(:tyname)
This type provides a convenient method for defining values
that are dependent on just the type, and not on any values
within that type. For example, within the new theory of words, the constant
dimindex
has type
:'a itself -> num
, and returns the
cardinality of the universe of the type 'a
if the
universe is finite, or one otherwise. The syntax support means
one can write terms such as
dimindex(:bool)
and
dimindex(:'a -> bool)
This type is inspired by a similar one in Isabelle/HOL.
The muddyC/muddy.c
file would not build with
gcc-4
.
The implementation of Q.EXISTS
was incorrect
(would only work with witnesses of type :bool
).
Thanks to Eunsuk Kang for the report of this bug.
The natural number and integer decision procedures were not normalising multiplicative expressions as much as they should, causing obvious goals to not get proved. Thanks to Alexey Gotsman for the report of this bug.
The theory and identifier indexes in the help pages were generated with bogus links. Thanks to Hasan Amjad for the report of this bug.
Expressions using case
-expressions with
function-types and applied to arguments failed to parse
correctly.
The implementation of Holmake
’s
--rebuild_deps
(or -r
) option was
faulty. Thanks to Tom Ridge for the report of this bug.
The implementation of stringLib.string_EQ_CONV
failed if one of the string arguments was the empty string.
Thanks to Mike Gordon for the report of this bug.
The derivation of “strong” induction principles
in the inductive definitions library has been improved to cope
with multiple (mutually recursive) inductively-defined
relations. Such relations could always be defined using
Hol_reln
, but their strong induction principles
couldn’t be derived. (See below for a change in the type
and home of this function.)
A theory of the rational numbers, thanks to Jens Brandt. This is used in the embedding of ACL2 in HOL.
A new polymorphic theory of fixed-width
words, called words
. This is now our recommended way
of using types such as word32
, word16
etc.
This builds on John Harrison’s “Finite cartesian
products” from A HOL theory of Euclidean space in
TPHOLs 2005.
There is now no need to use the word functor
approach introduced in Kananaskis-3 (though this code is still
available). Instead, when wordsTheory
is loaded, one
set of polymorphic constants is defined, and these can be used for
all the word types. Words are polymorphic in one argument (thus
there is a type ``:'a word``
) and types such as
word32
and word16
instantiate the type
parameter to different concrete type arguments. (The cardinality of
the parameter’s universe indicates the number of bits in the
word.) For more, see the Description.
sexp
of S-expressions. All 78 ACL2 axioms have been
verified in HOL. A suite of tools is available to translate HOL
datatypes into S-expressions and HOL functions to functions on
S-expressions. Scripts are provided to print S-expressions defined
inside HOL to defuns and defthms for processing by the ACL2 system,
and for slurping ACL2 defuns and defthms into HOL. This work is a
collaboration between Mike Gordon and James Reynolds at the
University of Cambridge and Warren Hunt and Matt Kaufmann at the
University of Texas. The goal is to provide a robust and scalable
link between the HOL4 and ACL2 systems suitable for use on
substantial industrial-scale verification projects. temporal_deep
contains deep embeddings of temporal logics and other formalisms related to model checking. Amongst others there are deep embeddings of
temporalLib
this allows LTL model checking. Moreover, there is a translation of a subset of the FL of the PSL example into LTL. Thus, this example allows model checking for a subset of PSL.
The std_ss
simpset has become more powerful,
picking up a set of “obvious” rewrites that used to
be in arith_ss
. Now the latter simpset adds just
the decision procedure for Presburger arithmetic.
Functions such as induction_of
in the
TypeBase
structure that used to take a string (the
name of a type operator), now take a type. Thus, instead of
TypeBase.induction_of "num"use
TypeBase.induction_of ``:num``
The normalisation of arithmetic terms performed by
the ARITH_ss
simpset fragment (and thus, the
simpset bossLib.arith_ss
) is more aggressive. This
can break proofs. The bossLib
library now exports
old_arith_ss
and old_ARITH_ss
entry-points if users wish to avoid having to adjust their
proofs.
The derive_strong_induction
function has
changed type, and location. It is now an entry-point in
IndDefLib
, and has type
thm * thm -> thm
rather than
thm list * thm -> thm
The first argument should now be the “rules”
theorem returned by a call to Hol_reln
.
In order to avoid certain misleading scenarios, the type of
mk_oracle_thm
has changed so that it takes a string
as its first argument rather than a tag
. The
implementation of mk_oracle_thm
turns the given
string into a tag value using the function
Tag.read
. There is also a new function,
Thm.add_tag
, that allows arbitrary tags to be added
to existing theorems. Thanks to Mark Adams for discussion leading
to this change.