http://sourceforge.net/projects/hol/The (very nice) facilities available at SourceForge have enabled the HOL developers, who are currently scattered over three countries, to keep reasonable control over a continually changing system. SourceForge also provides a convenient place from which to distribute the system. Ordinary users can even grab incremental updates and bugfixes, rather than waiting for upcoming releases.
HOL is an open system, and we welcome those keen to play a role in its continuing evolution. There are many ways in which one might take part in HOL development. It is not necessary to have a deep knowledge of HOL (or even logic) in order to make a contribution. If you are interested, please send us an email.
gives organized access to/help/HOLindex.html
EVAL ``FACT 6``and getting back
> val it = |- FACT 6 = 720 : thmDefinitions made with Define also automatically update this global set of rewrites. There is support for monitoring EVAL and its kin, and for controlling the depth of its expansions.
srw_ss : unit -> simpsetThe access to type information (constructor injectivity and disjointness) duplicates the functionality provided by RW_TAC, but use of srw_ss has the advantage that other theorems and behaviours are also available automatically. For example, when pred_setLib is loaded, the srw_ss() simpset is extended with all pred_setTheory's "obvious rewrites", things like
|- FINITE (P UNION Q) = FINITE P /\ FINITE Qas well as the SET_SPEC_CONV conversion which does the right thing with
x IN { ... | ... }terms. There is also an RW_TAC equivalent, SRW_TAC which uses this simpset and also implements RW_TAC's aggressive stripping and normalisation strategies.
Theorems are provided for reasoning about bit-fields, as well as arithmetic (Commutative Ring properties) and the logical operations (Boolean Algebra properties). A number of rewrite rules are also provided, and these support fairly efficient term evaluation using WORD32_CONV (or EVAL).
The functor wordFunctor can be used to create bespoke word theories. For example, a theory of 8-bit words can be obtained by the invocation
structure word8Theory = wordFunctor (val bits = 8)
!x::P. Q xis
!x. x IN P ==> Q x.The restricted quantification library has been updated to reflect this change, and also shrunk down: in the course of use it was found that more powerful proof tools like the simplifier have removed the need for many of the lower-level tactics.
bool$/\is the conjunction operator in boolTheory, and
:num$numis the num type from numTheory. There are also new functions in the kernel's ML API for building and pulling apart constants with theory information included. For example, the function mk_thy_const has the following type
{Name:string, Thy:string, Ty:hol_type} -> termand the function dest_thy_const inverts this. mk_const remains in the system, but its behaviour is unspecified when two or more constants have the same name.
type_abbrev("set", ``:'a -> bool``)is used in pred_setTheory to establish ``:'a set`` as an abbreviation for functions of type ``'a -> bool``. After issuing this command, one can write ``NS:num set`` and ``:'b set``. When printed, types do not include abbreviations.
case n of 0 -> x || SUC n -> n + 1and
case p of (x, []) -> x + 1 || (y, h::t) -> y + h
infix THEN THENL ...at the top of one's files. Doing so is not an error however. If this behaviour leads to problems, recall that ML infix declarations can be cancelled with the "nonfix" directive.
string * hol_type -> termrather than
{Name : string, Ty : hol_type} -> termA consistently "record-ised" view of the world is still available by opening the structure Rsyntax. Even in the default view of the world, some functions still take records. These exceptions are for functions where we feel that the order of arguments of the same type is not always obvious. This is exemplified by the universal adoption of the {redex,residue} datatype for substitutions and instantiations. (Remember also that the infix |-> function can be used to construct such records.)
overload_on ("foo", ``bar``);
<rcd-type-name>_<fldname>E.g., "rcd_fld". If you really like the 'dot' syntax, you can always write
\r. r.fldwhich eta-converts to the above.
val INTER_ASSOC = GSYM INTER_ASSOC val UNION_ASSOC = GSYM UNION_ASSOCbefore the references to these theorems occur.
theorems ()should thus be replaced with
theorems "-"
hol, hol.bare, hol.unquote, and hol.bare.unquoteall found in the bin/ directory. We recommend hol.unquote as the standard starting point.
In more detail, the ".unquote" suffix means that the ``...`` preprocessor is enabled. The ".bare" indicates that the executable starts up with a minimal logical context (just boolTheory, the goal-stack and the 'standard' tactics and conversions loaded). This is like the old behaviour of the hol and hol.unquote executables. The absence of the ".bare" indicates an executable that loads "bossLib" as it starts. This provides a much richer logical environment (lists, natural numbers, pairs, options, disjoint sums), with additional tools too (arithmetic decision procedure, high-level definition principles).