Filter
Top Products
Appendix A
Compatibility with other
HOLs
Here is a brief list of some of the major incompatibilities with other versions of
HOL:
• CAML, the underlying ML is different from previous HOL versions, some-
where between ‘Classic ML’ and Standard ML.
• There is no theory mechanism; every theorem is just bound to an ML name.
It is possible to save and load theorems via CAML primitives, but this is
not recommended since it subverts the usual mechanisms for constructing
elements of the thm type.
• Parsing status is orthogonal to whether an identifier is a constant or a variable.
Parsing status is not indicated at the time constants are defined. To suppress
special parse status, HOL Light requires the identifier to be put in parentheses
like (+), whereas other HOL versions use $+.
• Higher order matching is applied pervasively throughout the system, and in
some cases this can lead to a different result from a first order match even
when both succeed.
• All permutative rewrite rules are automatically ordered by the rewriting func-
tions.
• Operator overloading is permitted in the surface syntax. There are however
still some limitations on overloading of polymorphic operators. The interface
map feature in previous HOLs has been abolished and operator overloading
is used instead.
• Decision procedures for linear arithmetic are available for integers and reals
as well as naturals.
• A comprehensive theory of wellfounded relations is provided, but no tools for
automating general recursive definitions.
• The resolution tactics have been removed, or more accurately replaced by
trivial ones that do not attempt multiple chaining.
• Goals have theorems as assumptions, rather than terms to be assumed. The
tactic mechanism allows the use of instantiable metavariables, and assump-
tions may be labelled with names. The internal type of tactics has changed
to reflect these changes.
103