Libraries

A library is an abstraction intended to provide a higher level of organization for HOL applications. In general, a library can contain a collection of theories, proof procedures, and supporting material, such as documentation. Some libraries simply provide proof procedures, such as simpLib, while others provide theories and proof procedures, such as intLib. Libraries can include other libraries.

In the HOL system, libraries are typically represented by SML structures named following the convention that library x will be found in the SML structure xLib. Loading this structure should load all the relevant sub-components of the library and set whatever system parameters are suitable for use of the library.

When the HOL system is invoked in its normal configuration, several useful libraries are automatically loaded. The most basic HOL library is boolLib, which supports the definitions of the HOL logic, found in the theory bool, and provides a useful suite of definition and reasoning tools.

Another pervasively used library is found in the structure Parse (the reader can see that we are not strictly faithful to our convention about library naming). The parser library provides support for parsing and ‘pretty-printing’ of HOL types, terms, and theorems.

The boss library provides a basic collection of standard theories and high-level proof procedures, and serves as a standard platform on which to work. It is preloaded and opened when the HOL system starts up. It includes boolLib and Parse. Theories provided include pair, sum, option; the arithmetic theories num, prim_rec, arithmetic, and numeral; and list. Other libraries included in bossLib are goalstackLib, which provides a proof manager for tactic proofs; simpLib, which provides a variety of simplifiers; numLib, which provides a decision procedure for arithmetic; Datatype, which provides high-level support for defining algebraic datatypes; and tflLib, which provides support for defining recursive functions.

Parsing and Prettyprinting

Every type and term in HOL is ultimately built by application of the primitive (abstract) constructors for types and terms. However, in order to accommodate a wide variety of mathematical expression, HOL provides flexible infrastructure for parsing and prettyprinting types and terms through the Parse structure.

The term parser supports type inference, overloading, binders, and various fixity declaration (infix, prefix, postfix, and combinations). There are also flags for controlling the behaviour of the parser. Further, the structure of the parser is exposed so that new parsers can be quickly constructed to support user applications.

The parser is parameterized by grammars for types and terms. The behaviour of the parser and prettyprinter is therefore usually altered by grammar manipulations. These can be of two kinds: temporary or permanent. Temporary changes should be used in library implementations, or in script files for those changes that the user does not wish to have persist in theories descended from the current one. Permanent changes are appropriate for use in script-files, and will be in force in all descendant theories. Functions making temporary changes are signified by a leading temp_ in their names.

Parsing types

The language of types is a simple one. An abstract grammar for the language is presented in Figure 8.1.1. The actual grammar (with concrete values for the infix symbols and type operators) can be inspected using the function type_grammar.

$$ \begin{array}{lcl} \tau &::=& \tau \;\odot\; \tau \;\;|\;\; \mathit{vtype} \;\;|\;\; \mathit{tyop} \;\;|\;\; \mathtt{(} \;\mathit{tylist}\;\mathtt{)} \;\mathit{tyop} \;\;|\;\; \tau \;\mathit{tyop} \;\;|\;\; \mathtt{(}\;\tau\;\mathtt{)} \;\;|\;\; \tau\mathtt{[}\tau\mathtt{]}\\ \odot &::=& \mathtt{->} \;\;|\;\; \mathtt{\#} \;\;|\;\; \mathtt{+} \;\;|\;\; \cdots\\ \mathit{vtype} &::=& \mathtt{'a} \;\;|\;\; \mathtt{'b} \;\;|\;\; \mathtt{'c} \;\;|\;\; \cdots\\ \mathit{tylist} &::=& \tau \;\;|\;\; \tau \;\mathtt{,}\;\mathit{tylist}\\ \mathit{tyop} &::=& \mathtt{bool} \;\;|\;\; \mathtt{list} \;\;|\;\; \mathtt{num} \;\;|\;\; \mathtt{fun} \;\;|\;\; \cdots \end{array} $$

Figure 8.1.1. An abstract grammar for HOL types ($\tau$). Infixes ($\odot$) always bind more weakly than type operators ($\mathit{tyop}$) (and type-subscripting $\tau\mathtt{[}\tau\mathtt{]}$), so that $\tau_1 \;\odot\; \tau_2\;\mathit{tyop}$ is always parsed as $\tau_1 \;\odot\; (\tau_2\;\mathit{tyop})$. Different infixes can have different priorities, and infixes at different priority levels can associate differently (to the left, to the right, or not at all). Users can extend the categories $\odot$ and $\mathit{tyop}$ by making new type definitions, and by directly manipulating the grammar.

Type infixes

Infixes may be introduced with the function add_infix_type. This sets up a mapping from an infix symbol (such as ->) to the name of an existing type operator (such as fun). The binary symbol needs to be given a precedence level and an associativity. See REFERENCE for more details.

Type abbreviations

Users can abbreviate common type patterns with abbreviations. This is done with the SML function type_abbrev:

   type_abbrev : string * hol_type -> unit

An abbreviation is a new type operator, of any number of arguments, that expands into an existing type. For example, one might develop a light-weight theory of numbers extended with an infinity, where the representing type was num option (NONE would represent the infinity value). One might set up an abbreviation infnum that expanded to this underlying type. Polymorphic patterns are supported as well. For example, as described in Section 5.5.1, the abbreviation set, of one argument, is such that :'a set expands into the type :'a -> bool, for any type :'a.

When types come to be printed, the expansion of abbreviations done by the parser is reversed if the type_abbrev_pp entry-point is used; otherwise the abbreviation is for input only. For more information, see type_abbrev's entry in REFERENCE.

There are special syntactic forms available for both type abbreviation entry-points. Instead of

   val _ = type_abbrev("set", “:'a -> bool”)

one can write

   Type set = “:'a -> bool”

and if an underlying call to type_abbrev_pp is desired, the [pp] “attribute” should be added to the name, thus:

   Type set[pp] = “:'a -> bool”

If a “temporary” abbreviation is required (one whose effect will not be apparent in descendent theories), then the local attribute can also be added to the Type syntax, or the SML functions temp_type_abbrev and temp_type_abbrev_pp can be used.

Parsing terms

The term parser provides a grammar-based infrastructure for supporting concrete syntax for formalizations. Usually, the HOL grammar gets extended when a new definition or constant specification is made. (The introduction of new constants is discussed in Sections 1.6.3.1 and 1.6.3.2.) However, any identifier can have a parsing status attached at any time. In the following, we explore some of the capabilities of the HOL term parser.

Parser architecture

The parser turns strings into terms. It does this in the following series of phases, all of which are influenced by the provided grammar. Usually this grammar is the default global grammar, but users can arrange to use different grammars if they desire. Strictly, parsing occurs after lexing has split the input into a series of tokens. For more on lexing, see Section 1.3.1.

Concrete Syntax: Features such as infixes, binders and mix-fix forms are translated away, creating an intermediate, “abstract syntax” form (ML type Absyn). The possible fixities are discussed in Section 8.1.2.6 below. Concrete syntax forms are added to the grammar with functions such as add_rule and set_fixity (for which, see the REFERENCE). The action of this phase of parsing is embodied in the function Absyn.

The Absyn data type is constructed using constructors AQ (an antiquote, see Section 8.1.3); IDENT (an identifier); QIDENT (a qualified identifier, given as thy$ident) ; APP (an application of one form to another); LAM (an abstraction of a variable over a body), and TYPED (a form accompanied by a type constraint¹, see Section 8.1.2.4). At this stage of the translation, there is no distinction made between constants and variables: though QIDENT forms must be constants, users are also able to refer to constants by giving their bare names.

It is possible for names that occur in the Absyn value to be different from any of the tokens that appeared in the original input. For example, the input

   “if P then Q else R”

will turn into

   APP (APP (APP (IDENT "COND", IDENT "P"), IDENT "Q"), IDENT "R")

(This is slightly simplified output: the various constructors for Absyn, including APP, also take location parameters.)

The standard grammar includes a rule that associates the special mix-fix form for if-then-else expressions with the underlying “name” COND. It is COND that will eventually be resolved as the constant bool$COND.

If the “quotation” syntax with a bare dollar is used, then this phase of the parser will not treat strings as part of a special form. For example, “$if P” turns into the Absyn form

   APP(IDENT "if", IDENT "P")

not a form involving COND.

More typically, one often writes something like “$+ x”, which generates the abstract syntax

   APP(IDENT "+", IDENT "x")

Without the dollar-sign, the concrete syntax parser would complain about the fact that the infix plus did not have a left-hand argument. When the successful result of parsing is handed to the next phase, the fact that there is a constant called + will give the input its desired meaning.

Symbols can also be “escaped” by enclosing them in parentheses. Thus, the above could be written “(+) x” for the same effect.

The user can insert intermediate transformation functions of their own design into the parsing processing at this point. This is done with the function

   add_absyn_postprocessor

The user's function will be of type Absyn -> Absyn and can perform whatever changes are appropriate. Like all other aspects of parsing, these functions are part of a grammar: if the user doesn't want to see a particular function used, they can arrange for parsing to be done with respect to a different grammar.

Name Resolution: The bare IDENT forms in the Absyn value are resolved as free variables, bound names or constants. This process results in a value of the Preterm data type, which has similar constructors to those in Absyn except with forms for constants. A string can be converted straight to a Preterm by way of the Preterm function.

A bound name is the first argument to a LAM constructor, an identifier occurring on the left-hand side of a case-expression's arrow, or an identifier occurring within a set comprehension's pattern. A constant is a string that is present in the domain of the grammar's “overload map”. Free variables are all other identifiers. Free variables of the same name in a term will all have the same type. Identifiers are tested to see if they are bound, and then to see if they are constants. Thus it is possible to write

   \SUC. SUC + 3

and have the string SUC be treated as a number in the context of the given abstraction, rather than as the successor constant.

The “overload map” is a map from strings to lists of terms. The terms are usually just constants, but can be arbitrary terms (giving rise to “syntactic macros” or “patterns”). This facility is used to allow a name such as + to map to different addition constants in theories such as arithmetic, integer, and words. In this way the “real” names of the constants can be divorced from what the user types. In the case of addition, the natural number plus actually is called + (strictly, arithmetic$+); but over the integers, it is int_add, and over words it is word_add. (Note that because each constant is from a different theory and thus a different namespace, they could all have the name +.)

When name resolution determines that an identifier should be treated as a constant, it is mapped to a preterm form that lists all of the possibilities for that string. Subsequently, because the terms in the range of the overload map will typically have different types, type inference will often eliminate possibilities from the list. If multiple possibilities remain after type inference has been performed, then a warning will be printed, and one of the possibilities will be chosen. (Users can control which terms are picked when this situation arises.)

When a term in the overload map is chosen as the best option, it is substituted into the term at appropriate position. If the term is a lambda abstraction, then as many $\beta$-reductions are done as possible, using any arguments that the term has been applied to. It is in this way that a syntactic pattern can process arguments. (See also Section 8.1.2.3 for more on syntactic patterns.)

Type Inference: All terms in the HOL logic are well-typed. The kernel enforces this through the API for the term data type. (In particular, the mk_comb function checks that the type of the first argument is a function whose domain is equal to the type of the second argument.) The parser's job is to turn user-supplied strings into terms. For convenience, it is vital that the users do not have to provide types for all of the identifiers they type. (See Section 8.1.2.5 below.)

In the presence of overloaded identifiers, type inference may not be able to assign a unique type to all constants. If multiple possibilities exist, one will be picked when the Preterm is finally converted into a genuine term.

Conversion to Term: When a Preterm has been type-checked, the final conversion from that type to the term type is mostly straightforward. The user can insert further processing at this point as well, so that a user-supplied function modifies the result before the parser returns.

Unicode characters

It is possible to have the HOL parsing and printing infrastructure use Unicode characters (written in the UTF-8 encoding). This makes it possible to write and read terms such as

   ∀x. P x ∧ Q x

rather than

   !x. P x /\ Q x

If they wish, users may simply define constants that have Unicode characters in their names, and leave it at that. The problem with this approach is that standard tools will likely then create theory files that include (illegal) SML bindings like val →_def = .... The result will be ...Theory.sig and ...Theory.sml files that fail to compile, even though the call to export_theory may succeed. This problem can be finessed through the use of functions like set_MLname, but it's probably best practice to only use alphanumerics in the names of constants, and to then use functions like overload_on and add_rule to create Unicode syntax for the underlying constant.

If users have fonts with the appropriate repertoire of characters to display their syntax, and are confident that any other users of their theories will too, then this is perfectly reasonable. However, if users wish to retain some backwards compatibility a provide a pure ASCII syntax, they can do so by defining that pure ASCII syntax first. Having done this, they can create a Unicode version of the syntax with the function Unicode.unicode_version. Then, either Unicode or ASCII characters can be used to input the syntax, and, while the trace variable "PP.avoid_unicode" is $1$, the ASCII syntax will be used for printing. If the trace is set to $0$, then again, both syntaxes can be used to write the terms, but the pretty-printer will prefer the Unicode syntax when the terms are printed by the system.

For example, in boolScript.sml, the Unicode character for logical and (∧), is set up as a Unicode alternative for /\ with the call

   val _ = unicode_version {u = UChar.conj, tmnm = "/\\"};

(In this context, the Unicode structure has been open-ed, giving access also to the structure UChar which contains bindings for the Greek alphabet, and some common mathematical symbols.)

The argument to unicode_version is a record with fields u and tmnm. Both are strings. The tmnm field can either be the name of a constant, or a token appearing in a concrete syntax rule (possibly mapping to some other name). If the tmnm is only the name of a constant, then, with the trace variable enabled, the string u will be overloaded to the same name. If the tmnm is the same as a concrete syntax rule's token, then the behaviour is to create a new rule mapping to the same name, but with the string u used as the token.

Lexing rules with Unicode characters

Roughly speaking, HOL considers characters to be divided into three classes: alphanumerics, non-aggregating symbols and symbols. This affects the behaviour of the lexer when it encounters strings of characters. Unless there is a specific “mixed” token already in the grammar, tokens split when the character class changes. Thus, in the string

   ++a

the lexer will see two tokens, ++ and a, because + is a symbol and a is an alphanumeric. The classification of the additional Unicode characters is very simplistic: all Greek letters except λ are alphanumeric; the logical negation symbol ¬ is non-aggregating; a variety of parenthetical characters (e.g., $\llparenthesis\,\rrparenthesis$) are non-aggregating, and everything else is symbolic. (The exception for λ is to allow strings like λx.x to lex into four tokens.)

Overloading and Syntactic Patterns ("macros")

As earlier alluded to, a limited amount of overloading resolution is performed by the term parser. For example, the ‘tilde’ symbol (~) denotes boolean negation in the initial theory of HOL, and it also denotes the additive inverse in the integer and real theories. If we load the integer theory and enter an ambiguous term featuring ~, the system will inform us that overloading resolution is being performed.

> load "integerTheory";
val it = (): unit

> Term `~~x`;
<<HOL message: more than one resolution of overloading was possible>>
val it = “¬¬x”: term

> type_of it;
val it = “:bool”: hol_type

A priority mechanism is used to resolve multiple possible choices. In the example, ~ could be consistently chosen to have type :bool -> bool or :int -> int, and the mechanism has chosen the former. For finer control, explicit type constraints may be used. In the following session, the ~~x in the first quotation has type :bool, while in the second, a type constraint ensures that ~~x has type :int.

> Term `~(x = ~~x)`;
<<HOL message: more than one resolution of overloading was possible>>
val it = “(x :bool) ⇎ ¬¬x”: term

> Term `~(x:int = ~~x)`;
val it = “(x :int) ≠ --x”: term

Note that the symbol ~ stands for two different constants in the second quotation; its first occurrence is boolean negation, while the other two occurrences are the additive inverse operation for integers.

The prettiest way to introduce entries into the overload map is to use the Overload syntactic form:

   Overload name[attrs] = “term/pattern”

(The name can be a bare SML alpha-numeric identifier or enclosed in string-literal quotes; names that are “symbolic” in any way must be enclosed in string-literal double quotes. For example, Overload "-@-" = “...”.) Depending on the choice of attributes, this will map into a call to one of a variety of underlying “overload-on” functions. The default (without any attributes) calls overload_on, whose effect is to make an entry in the map that will be exported with the theory. The overloading effect thus persists in descendent theories. If the local attribute is used, this export doesn't occur, and the overloading effect is only visible for the rest of the containing script file.²

The other attribute that can be used is inferior, which causes the entry to be made, but makes it the pretty-printer's last choice when matching terms are printed.

All of this functionality ultimately stems from the “overload map” mentioned earlier. This is actually a combination of maps, one for parsing, and one for printing. The parsing map is from names to lists of terms, and determines how the names that appear in a Preterm will translate into terms. In essence, bound names turn into bound variables, unbound names not in the domain of the map turn into free variables, and unbound names in the domain of the map turn into one of the elements of the set associated with the given name. Each term in the set of possibilities may have a different type, so type inference will choose from those that have types consistent with the rest of the given term. If the resulting list contains more than one element, then the term appearing earlier in the list will be chosen.

The most common use-case for the overload map is have names map to constants. In this way, for example, the various numeric theories can map the string "+" to the relevant notions of addition, each of which is a different constant. However, the system has extra flexibility because names can map to arbitrary terms. For example, it is possible to map to specific type-instances of constants. Thus, the string "<=>" maps to equality, but where the arguments are forced to be of type ":bool".

Moreover, if the term mapped to is a lambda-abstraction (i.e., of the form $\lambda x.\;M$), then the parser will perform all possible $\beta$-reductions for that term and the arguments accompanying it. For example, in boolTheory and its descendants, the string "<>" is overloaded to the term “\x y. ~(x = y)”. Additionally, "<>" is set up at the concrete syntax level as an infix. When the user inputs “x <> y”, the resulting Absyn value is

   APP(APP(IDENT "<>", IDENT "x"), IDENT "x")

The "x" and "y" identifiers will map to free variables, but the "<>" identifier maps to a list containing “\x y. ~(x = y)”. This term has type

   :'a -> 'a -> bool

and the polymorphic variables are generalisable, allowing type inference to give appropriate (identical) types to x and y. Assuming that this option is the only overloading for "<>" left after type inference, then the resulting term will be ~(x = y). Better, though this will be the underlying structure of the term in memory, it will actually print as “x <> y”.

If the term mapped to in the overload map contains any free variables, these variables will not be instantiated in any way. In particular, if these variables have polymorphic types, then the type variables in those types will be constant: not subject to instantiation by type inference.

Pretty-printing and syntactic patterns

The second part of the “overload map” is a map from terms to strings, specifying how terms should be turned back into identifiers. (Though it does not actually construct an Absyn value, this process reverses the name resolution phase of parsing, producing something that is then printed according to the concrete syntax part of the given grammar.)

Because parsing can map single names to complicated term structures, printing must be able to take a complicated term structure back to a single name. It does this by performing term matching.³

If multiple patterns match the same term, then the printer picks the most specific match (the one that requires least instantiation of the pattern's variables). If this still results in multiple, equally specific, possibilities, the most recently added pattern takes precedence. (Users can thus manipulate the printer's preferences by making otherwise redundant Overload declarations.)

In the example of the not-equal-to operator above, the pattern will be ~(?x = ?y), where the question-marks indicate instantiable pattern variables. If a pattern includes free variables (recall that the x and y in this example were bound by an abstraction), then these will not be instantiable.

There is one further nicety in the use of this facility: “bigger” matches, covering more of a term, take precedence. The difficulty this can cause is illustrated in the IS_PREFIX pattern from rich_listTheory. For the sake of backwards compatibility this identifier maps to

   \x y. isPREFIX y x

where isPREFIX is a constant from listTheory. (The issue is that IS_PREFIX expects its arguments in reverse order to that expected by isPREFIX.) Now, when this macro is set up the overload map already contains a mapping from the string "isPREFIX" to the constant isPREFIX (this happens with every constant definition). But after the call establishing the new pattern for IS_PREFIX, the isPREFIX form will no longer be printed. Nor is it enough, to repeat the call

   Overload isPREFIX = “isPREFIX”

Instead (assuming that isPREFIX is indeed the preferred printing form), the call must be

   Overload isPREFIX = “\x y. isPREFIX x y”

so that isPREFIX's pattern is as long as IS_PREFIX's.

Type constraints

A term can be constrained to be of a certain type. For example, X:bool constrains the variable X to have type bool. An attempt to constrain a term inappropriately will raise an exception: for example,

   if T then (X:ind) else (Y:bool)

will fail because both branches of a conditional must be of the same type. Type constraints can be seen as a suffix that binds more tightly than everything except function application. Thus $\term\ \ldots\ \term : \type$ is equal to $(\term\ \ldots\ \term) : \type$, but $x < y:$num is a legitimate constraint on just the variable $y$.

The inclusion of : in the symbolic identifiers means that some constraints may need to be separated by white space. For example,

   $=:bool->bool->bool

will be broken up by the HOL lexer as

   $=: bool -> bool -> bool

and parsed as an application of the symbolic identifier $=: to the argument list of terms [bool, ->, bool, ->, bool]. A well-placed space will avoid this problem:

   $= :bool->bool->bool

is parsed as the symbolic identifier "=" constrained by a type. Instead of the $, one can also use parentheses to remove special parsing behaviour from lexemes:

   (=):bool->bool->bool

Type inference

Consider the term x = T: it (and all of its subterms) has a type in the HOL logic. Now, T has type bool. This means that the constant = has type xty -> bool -> bool, for some type xty. Since the type scheme for = is 'a -> 'a -> bool, we know that xty must in fact be bool in order for the type instance to be well-formed. Knowing this, we can deduce that the type of x must be bool.

Ignoring the jargon (“scheme” and “instance”) in the previous paragraph, we have conducted a type assignment to the term structure, ending up with a well-typed term. It would be very tedious for users to conduct such argumentation by hand for each term entered to HOL. Thus, HOL uses an adaptation of Milner's type inference algorithm for SML when constructing terms via parsing. At the end of type inference, unconstrained type variables get assigned names by the system. Usually, this assignment does the right thing. However, at times, the most general type is not what is desired and the user must add type constraints to the relevant subterms. For tricky situations, the global variable show_types can be assigned. When this flag is set, the prettyprinters for terms and theorems will show how types have been assigned to subterms. If you do not want the system to assign type variables for you, the global variable guessing_tyvars can be set to false, in which case the existence of unassigned type variables at the end of type inference will raise an exception.

Fixities

In order to provide some notational flexibility, constants come in various flavours or fixities: besides being an ordinary constant (with no fixity), constants can also be binders, prefixes, suffixes, infixes, or closefixes. More generally, terms can also be represented using reasonably arbitrary mixfix specifications. The degree to which terms bind their associated arguments is known as precedence. The higher this number, the tighter the binding. For example, when introduced, + has a precedence of 500, while the tighter binding multiplication (*) has a precedence of 600.

Binders

A binder is a construct that binds a variable; for example, the universal quantifier. In HOL, this is represented using a trick that goes back to Alonzo Church: a binder is a constant that takes a lambda abstraction as its argument. The lambda binding is used to implement the binding of the construct. This is an elegant and uniform solution. Thus the concrete syntax !v. M is represented by the application of the constant ! to the abstraction (\v. M).

The most common binders are !, ?, ?!, and @. Sometimes one wants to iterate applications of the same binder, e.g.,

   !x. !y. ?p. ?q. ?r. t.

This can instead be rendered

   !x y. ?p q r. t.

Infixes

Infix constants can associate in one of three different ways: right, left or not at all. (If + were non-associative, then 3 + 4 + 5 would fail to parse; one would have to write (3 + 4) + 5 or 3 + (4 + 5) depending on the desired meaning.) The precedence ordering for the initial set of infixes is /\, \/, ==>, =, , (comma⁴). Of these, equality is non-associative, and the remainder are right associative. Thus

   X /\ Y ==> C \/ D, P = E, Q

is equal to

   ((X /\ Y) ==> (C \/ D)), ((P = E), Q).

An expression $$ \term \; \langle\mathit{infix}\rangle\; \term $$ is internally represented as $$ ((\langle\mathit{infix}\rangle\; \term)\; \term) $$

Prefixes

Where infixes appear between their arguments, prefixes appear before theirs. This might initially appear to be the same thing as happens with normal function application where the symbol on the left simply has no fixity: is $f$ in $f(x)$ not acting as a prefix? Actually though, in a term such as $f(x)$, where $f$ and $x$ do not have fixities, the syntax is treated as if there is an invisible infix function application between the two tokens: $f\cdot{}x$. This infix operator binds tightly, so that when one writes $f\,x + y$, the parse is $(f\cdot{}x) + y$.⁵ It is then useful to allow for genuine prefixes so that operators can live at different precedence levels than function application. An example of this is ~, logical negation. This is a prefix with lower precedence than function application. Normally $$ f\;x\; y\qquad \text{is parsed as}\qquad (f\; x)\; y $$ but $$ \mathtt{\sim}\; x\; y\qquad\text{is parsed as}\qquad \mathtt{\sim}\; (x\; y) $$ because the precedence of ~ is lower than that of function application. The unary negation symbol would also typically be defined as a prefix, if only to allow one to write $$ \mathit{negop}\,\mathit{negop}\,3 $$ (whatever negop happened to be) without needing extra parentheses.

On the other hand, the univ syntax for the universal set (see Section 5.5.1) is an example of a prefix operator that binds more tightly than application. This means that f univ(:'a) is parsed as f(univ(:'a)), not (f univ)(:'a) (which parse would fail to type-check).

Suffixes

Suffixes appear after their arguments. There are suffixes ^+, ^* and ^= corresponding to the transitive, the reflexive and transitive, and the “equivalence” closure used in relationTheory (Section 5.5.3). Suffixes are associated with a precedence just as infixes and prefixes are. If p is a prefix, i an infix, and s a suffix, then there are six possible orderings for the three different operators based on their precedences, giving five parses for $\mathtt{p}\; t_1\; \mathtt{i}\; t_2\; \mathtt{s}$ depending on the relative precedences:

Closefixes

Closefix terms are operators that completely enclose their arguments. An example one might use in the development of a theory of denotational semantics is semantic brackets. Thus, the HOL parsing facilities can be configured to allow one to write denotation x as [| x |]. Closefixes are not associated with precedences because they can not compete for arguments with other operators.

Parser tricks and magic

Here we describe how to achieve some useful effects with the parser in HOL.

Aliasing: If one wants a special syntax to be an “alias” for a normal HOL form, this is easy to achieve; both examples so far have effectively done this. However, if one just wants to have a normal one-for-one substitution of one string for another, one can't use the grammar/syntax phase of parsing to do this. Instead, one can use the overloading mechanism. For example, let us alias MEM for IS_EL. We need to use the function overload_on to overload the original constant for the new name:

   val _ = overload_on ("MEM", “IS_EL”);

Making addition right associative: If one has a number of old scripts that assume addition is right associative because this is how HOL used to be, it might be too much pain to convert. The trick is to remove all of the rules at the given level of the grammar, and put them back as right associative infixes. The easiest way to tell what rules are in the grammar is by inspection (use term_grammar()). With just arithmeticTheory loaded, the only infixes at level 500 are + and -. So, we remove the rules for them:

   val _ = app temp_remove_rules_for_term ["+", "-"];

And then we put them back with the appropriate associativity:

   val _ = app (fn s => temp_add_infix(s, 500, RIGHT)) ["+", "-"];

Note that we use the temp_ versions of these two functions so that other theories depending on this one won't be affected. Further note that we can't have two infixes at the same level of precedence with different associativities, so we have to remove both operators, not just addition.

Mix-fix syntax for if-then-else: The first step in bringing this about is to look at the general shape of expressions of this form. In this case, it will be: $$ \mathtt{if}\;\; \dots \;\;\mathtt{then}\;\;\dots\;\; \mathtt{else}\;\;\dots $$ Because there needs to be a “dangling” term to the right, the appropriate fixity is Prefix. Knowing that the underlying term constant is called COND, the simplest way to achieve the desired syntax is:

val _ = add_rule
   {term_name = "COND", fixity = Prefix 70,
    pp_elements = [TOK "if", BreakSpace(1,0), TM, BreakSpace(1,0),
                   TOK "then", BreakSpace(1,0), TM, BreakSpace(1,0),
                   TOK "else", BreakSpace(1,0)],
    paren_style = Always,
    block_style = (AroundEachPhrase, (PP.CONSISTENT, 0))};

The actual rule is slightly more complicated, and may be found in the sources for the theory bool.

Mix-fix syntax for term substitution: Here the desire is to be able to write something like: $$ \mathtt{[}\,t_1\,\mathtt{/}\,t_2\,\mathtt{]}\,t_3 $$ denoting the substitution of $t_1$ for $t_2$ in $t_3$, perhaps translating to SUB $t_1\;t_2\;t_3$. This looks like it should be another Prefix, but the choice of the square brackets ([ and ]) as delimiters would conflict with the concrete syntax for list literals if this was done. Given that list literals are effectively of the CloseFix class, the new syntax must be of the same class. This is easy enough to do: we set up syntax $$ \mathtt{[}\,t_1\,\mathtt{/}\,t_2\,\mathtt{]} $$ to map to SUB $t_1\;t_2$, a value of a functional type, that when applied to a third argument will look right.⁶ The rule for this is thus:

  val _ = add_rule
           {term_name = "SUB", fixity = Closefix,
            pp_elements = [TOK "[", TM, TOK "/", TM, TOK "]"],
            paren_style = OnlyIfNecessary,
            block_style = (AroundEachPhrase, (PP.INCONSISTENT, 2))};

Hiding constants

The following function can be used to hide the constant status of a name from the quotation parser.

  val hide   : string -> ({Name : string, Thy : string} list *
                          {Name : string, Thy : string} list)

Evaluating hide "$x$" makes the quotation parser treat $x$ as a variable (lexical rules permitting), even if $x$ is the name of a constant in the current theory (constants and variables can have the same name). This is useful if one wants to use variables with the same names as previously declared (or built-in) constants (e.g., o, I, S, etc.). The name $x$ is still a constant for the constructors, theories, etc.; hide affects parsing and printing by removing the given name from the “overload map” described above in Section 8.1.2.1. Note that the effect of hide is temporary; its effects do not persist in theories descended from the current one. See the REFERENCE entry for hide for more details, including an explanation of the return type.

The function

   reveal : string -> unit

undoes hiding.

The function

   hidden : string -> bool

tests whether a string is the name of a hidden constant.

Adjusting the pretty-print depth

The following SML reference can be used to adjust the maximum depth of printing

   max_print_depth : int ref

The default print depth is $-1$, which is interpreted as meaning no maximum. Subterms nested more deeply than the maximum print depth are printed as .... For example:

> arithmeticTheory.ADD_CLAUSES;
val it =
   ⊢ 0 + m = m ∧ m + 0 = m ∧ SUC m + n = SUC (m + n) ∧
     m + SUC n = SUC (m + n): thm

> max_print_depth := 3;
val it = (): unit
> arithmeticTheory.ADD_CLAUSES;
val it = ⊢ ... + ... = m ∧ ... = ... ∧ ... ∧ ...: thm

Quotations and antiquotation

Logic-related syntax in the HOL system is typically passed to the parser in special forms known as quotations. A basic quotation is delimited by single quotation characters (..., Unicode code-points U+2018 and U+2019), or single back-ticks (i.e., `, ASCII character 96). When quotation values are printed out by the ML interactive loop, they look rather ugly because of the special filtering that is done to these values before the ML interpreter even sees them:

> val q = ‘f x = 3’;
val q = [QUOTE " (*#loc 1 12*)f x = 3"]: 'a frag list

Quotations (the ML environment prints the type as 'a frag list) are the raw input form expected by the various HOL parsers. They are also polymorphic (to be explained below). Thus the function Parse.Term takes a (term) quotation and returns a term, and is of type $$ term quotation -> term $$

The term and type parsers can also be called implicitly by using double quotations (with “...”, characters U+201C and U+201D), or doubled back-ticks as delimiters. For the type parser, the first non-space character after the leading delimiter must also be a colon. Thus:

> val t1 = “\x:num. x + 3”;
val t1 = “λx. x + 3”: term
> val t2 = ``p /\ q``;
val t2 = “p ∧ q”: term

> val ty = “:'a -> bool”;
val ty = “:α -> bool”: hol_type

The expression bound to ML variable t1 above is actually expanded to an application of the function Parse.Term to the quotation argument ‘p /\ q’. Similarly, the declaration of ty’s expression expands into an application of Parse.Type to the quotation ‘:'a -> bool’.

The significant advantage of quotations over normal SML strings is that they can include new-line and backslash characters without requiring special quoting. Newlines occur whenever terms get beyond the trivial in size, while backslashes occur in not just the ASCII representation of $\lambda$, but also the syntax for conjunction and disjunction.

If a quotation is to include a back-quote character, then the single back-quote delimiters cannot be used; instead this must be done by using the ‘..’ syntax. Backquotes can also freely appear between the “...” delimiters. To include a caret in quoted material (otherwise used for antiquotations, see below), it must not be followed by an alphanumeric identifier, nor by parentheses. Thus:

> ‘f `x’;
val it = [QUOTE " (*#loc 1 4*)f `x"]: 'a frag list

> ``f ^` x``;
<<HOL message: inventing new type variable names: 'a, 'b, 'c>>
val it = “f ^` x”: term

> “f ^ x”;
<<HOL message: inventing new type variable names: 'a, 'b, 'c>>
val it = “f ^ x”: term

The main use of the caret is to introduce antiquotations (as suggested in the last example above). Within a quotation, expressions of the form ^($t$) (where $t$ is an SML expression of type term or type) are called antiquotations. An antiquotation ^($t$) evaluates to the SML value of $t$. For example, x \/ ^(mk_conj(“y:bool”, “z:bool”)) evaluates to the same term as x \/ (y /\ z).
The most common use of antiquotation is when the term $t$ is bound to an SML variable $x$. In this case ^($x$) can be abbreviated by ^$x$.

The following session illustrates antiquotation.

> load "intLib";   ... output elided ...
> val y = “x+1”;
val y = “x + 1”: term

> val z = “y = ^y”;
val z = “y = x + 1”: term

> “!x:num.?y:num.^z”;
val it = “∀x. ∃y. y = x + 1”: term

Types may be antiquoted as well:

> val pred = “:'a -> bool”;
val pred = “:α -> bool”: hol_type

> “:^pred -> bool”;
val it = “:(α -> bool) -> bool”: hol_type

Quotations are polymorphic, and the type variable of a quotation corresponds to the type of entity that can be antiquoted into that quotation. Because the term parser expects only antiquoted terms, antiquoting a type into a term quotation requires the use of ty_antiq. For example,

> “!P:^pred. P x ==> Q x”;
Exception- Type error in function application.
   Function: Parse.Term : term frag list -> term
   Argument:
      [
         QUOTE " (*#loc 1 4*)!P:",
         ANTIQUOTE pred,
         QUOTE " (*#loc 1 12*). P x ==> Q x"
         ] : hol_type frag list
   Reason:
      Can't unify term (*Created from opaque signature*) with
         hol_type (*Created from opaque signature*)
         (Different type constructors)
Fail "Static Errors" raised

> “!P:^(ty_antiq pred). P x ==> Q x”;
val it = “∀P. P x ⇒ Q x”: term

Generalised Quotation Syntax

In line with various “modern” syntaxes (e.g., Theorem and Definition), it is possible to define custom quotation tooling using the Quote keyword. There are two forms. The first is

Quote ident1 = ident2:
  ...
End

where the Quote and End keywords must occur in column 1 of the source script-file. This is translated to

val ident1 = ident2 ‘ ... ’;

The other form is a short-cut where the quotation is parsed by the provided function only for its side-effects. The surface syntax is

Quote ident:
  ...
End

which is translated to

val _ = ident ‘ ... ’;

In both forms the identifier immediately before the colon must be a valid SML identifier containing only alpha-numeric characters (but with structure-qualification and full-stops also permitted). In the first form, ident1 must be a simple (unqualified) alphanumeric identifier (e.g., foo, bar', Foo_bar, but not M.bar, nor ++).

Backwards compatibility of syntax

This section of the manual documents the (extensive) changes made to the parsing of HOL terms and types in the Taupo release (one of the HOL3 releases) and beyond from the point of view of a user who doesn't want to know how to use the new facilities, but wants to make sure that their old code continues to work cleanly.

The changes which may cause old terms to fail to parse are:

• The precedence of type annotations has completely changed. It is now a very tight suffix (though with a precedence weaker than that associated with function application), instead of a weak one. This means that (x,y:bool # bool) should now be written as (x,y):bool # bool. The previous form will now be parsed as a type annotation applying to just the y. This change brings the syntax of the logic closer to that of SML and should make it generally easier to annotate tuples, as one can now write $$ (x\,:\,\tau_1,\;y\,:\,\tau_2,\dots z\,:\,\tau_n) $$ instead of $$ (x\,:\,\tau_1, \;(y\,:\,\tau_2, \dots (z\,:\,\tau_n))) $$ where extra parentheses have had to be added just to allow one to write a frequently occurring form of constraint.

• Most arithmetic operators are now left associative instead of right associative. In particular, $+$, $-$, $*$ and DIV are all left associative. Similarly, the analogous operators in other numeric theories such as integer and real are also left associative. This brings the HOL parser in line with standard mathematical practice.

• The binding equality in let expressions is treated exactly the same way as equalities in other contexts. In previous versions of HOL, equalities in this context have a different, weak binding precedence.

• The old syntax for conditional expressions has been removed. Thus the string ‘$p$=>$q$|$r$’ must now be written ‘if $p$then$q$else$r$’ instead.

• Some lexical categories are more strictly policed. String literals (strings inside double quotes) and numerals can't be used unless the relevant theories have been loaded. Nor can these literals be used as variables inside binding scopes.

A Simple Interactive Proof Manager

The goal stack provides a simple interface to tactic-based interactive proof. When one uses tactics to decompose a proof, many intermediate states arise; the goalstack takes care of the necessary bookkeeping. The implementation of goalstacks reported here is a re-design of Larry Paulson's original conception.

The goalstack library is automatically loaded when HOL starts up. Editor modes can support the process of using the proof manager; here we describe the underlying SML interface.

The abstract types goalstack and proofs are the focus of backwards proof operations. The type proofs can be regarded as a list of independent goalstacks. Most operations act on the head of the list of goalstacks; there are also operations so that the focus can be changed.

Starting a goalstack proof

   g        : term quotation -> proofs
   set_goal : goal -> proofs

Recall that the type goal is an abbreviation for term list * term. To start on a new goal, one gives set_goal a goal. This creates a new goalstack and makes it the focus of further operations.

A shorthand for set_goal is the function g: it invokes the parser automatically, and it doesn't allow the goal to have any assumptions.

Calling set_goal, or g, adds a new proof attempt to the existing ones, i.e., rather than overwriting the current proof attempt, the new attempt is stacked on top.

Applying a tactic to a goal

   expandf : tactic -> goalstack
   expand  : tactic -> goalstack
   e       : tactic -> goalstack

How does one actually do a goalstack proof then? In most cases, the application of tactics to the current goal is done with the function expand. In the rare case that one wants to apply an invalid tactic, then expandf is used. (For an explanation of invalid tactics, see Section 4.1.) The abbreviation e may also be used to expand a tactic.

Undo

   b          : unit -> goalstack
   rd         : unit -> goalstack
   drop       : unit -> proofs
   dropn      : int  -> proofs
   backup     : unit -> goalstack
   redo       : unit -> goalstack
   restart    : unit -> goalstack
   set_backup : int  -> unit

Often (we are tempted to say usually!) one takes a wrong path in doing a proof, or makes a mistake when setting a goal. To undo a step in the goalstack, the function backup and its abbreviation b are used. This will restore the goalstack to its previous state. To redo a step in the goalstack, the redo function, abbreviated as rd, may be used.

To directly back up all the way to the original goal, the function restart may be used. Obviously, it is also important to get rid of proof attempts that are wrong; for that there is drop, which gets rid of the current proof attempt, and dropn, which eliminates the top $n$ proof attempts.

Each proof attempt has its own undo-list of previous states. The undo-list for each attempt is of fixed size (initially 12). If you wish to set this value for the current proof attempt, the function set_backup can be used. If the size of the backup list is set to be smaller than it currently is, the undo list will be immediately truncated. You can not undo a “proofs-level” operation, such as set_goal or drop.

Viewing the state of the proof manager

   p            : unit -> goalstack
   status       : unit -> proofs
   top_goal     : unit -> goal
   top_goals    : unit -> goal list
   initial_goal : unit -> goal
   top_thm      : unit -> thm

To view the state of the proof manager at any time, the functions p and status can be used. The former only shows the top subgoals in the current goalstack, while the second gives a summary of every proof attempt.

To get the top goal or goals of a proof attempt, use top_goal and top_goals. To get the original goal of a proof attempt, use initial_goal.

Once a theorem has been proved, the goalstack that was used to derive it still exists (including its undo-list): its main job now is to hold the theorem. This theorem can be retrieved with top_thm.

Switch focus to a different subgoal or proof attempt

   r             : int -> goalstack
   R             : int -> proofs
   rotate        : int -> goalstack
   rotate_proofs : int -> proofs

Often we want to switch our attention to a different goal in the current proof, or a different proof. The functions that do this are rotate and rotate_proofs, respectively. The abbreviations r and R are simpler to type in.

High Level Proof — bossLib

The library bossLib marshals some of the most widely used theorem proving tools in HOL and provides them with a convenient interface for interaction. The library currently focuses on three things: definition of datatypes and functions; high-level interactive proof operations, and composition of automated reasoners. Loading bossLib commits one to working in a context that already supplies the theories of booleans, pairs, sums, the option type, arithmetic, and lists.

Support for high-level proof steps

The following functions use information in the database to ease the application of HOL's underlying functionality:

   type_rws     : hol_type -> thm list
   Induct       : tactic
   Cases        : tactic
   Cases_on     : term quotation -> tactic
   Induct_on    : term quotation -> tactic

The function type_rws will search for the given type in the underlying TypeBase database and return useful rewrite rules for that type. The rewrite rules of the datatype are built from the injectivity and distinctness theorems, along with the case constant definition. The simplification tactics RW_TAC, SRW_TAC, and the simpset (srw_ss()) automatically include these theorems. Other tactics used with other simpsets will need these theorems to be manually added.

The Induct tactic makes it convenient to invoke induction. When it is applied to a goal, the leading universal quantifier is examined; if its type is that of a known datatype, the appropriate structural induction tactic is extracted and applied.

The Cases tactic makes it convenient to invoke case analysis. The leading universal quantifier in the goal is examined; if its type is that of a known datatype, the appropriate structural case analysis theorem is extracted and applied.

The Cases_on tactic takes a quotation, which is parsed into a term $M$, and then $M$ is searched for in the goal. If $M$ is a variable, then a variable with the same name is searched for. Once the term to split over is known, its type and the associated facts are obtained from the underlying database and used to perform the case split. If some free variables of $M$ are bound in the goal, an attempt is made to remove (universal) quantifiers so that the case split has force. Finally, $M$ need not appear in the goal, although it should at least contain some free variables already appearing in the goal. Note that the Cases_on tactic is more general than Cases, but it does require an explicit term to be given.

The Induct_on tactic takes a quotation, which is parsed into a term $M$, and then $M$ is searched for in the goal. If $M$ is a variable, then a variable with the same name is searched for. Once the term to induct on is known, its type and the associated facts are obtained from the underlying database and used to perform the induction. If $M$ is not a variable, a new variable $v$ not already occurring in the goal is created, and used to build a term $v = M$ which the goal is made conditional on before the induction is performed. First however, all terms containing free variables from $M$ are moved from the assumptions to the conclusion of the goal, and all free variables of $M$ are universally quantified. Induct_on is more general than Induct, but it does require an explicit term to be given.

Induct_on can also be used to perform rule inductions, for which see Section 7.7.1.

Three supplementary entry-points have been provided for more exotic inductions:

completeInduct_on: performs complete induction on the term denoted by the given quotation. Complete induction allows a seemingly⁷ stronger induction hypothesis than ordinary mathematical induction: to wit, when inducting on $n$, one is allowed to assume the property holds for all $m$ smaller than $n$. Formally: $\forall P.\ (\forall x.\ (\forall y.\ y < x \supset P\, y) \supset P\,x) \supset \forall x.\ P\,x$. This allows the inductive hypothesis to be used more than once, and also allows instantiating the inductive hypothesis to other than the predecessor.

measureInduct_on: takes a quotation, and breaks it apart to find a term and a measure function with which to induct. For example, if one wanted to induct on the length of a list L, the invocation measureInduct_on `LENGTH L` would be appropriate.

recInduct: takes a induction theorem generated by Define or Hol_defn and applies it to the current goal.

Automated reasoners

bossLib brings together the most powerful reasoners in HOL and tries to make it easy to compose them in a simple way. We take our basic reasoners from mesonLib, simpLib, and numLib, but the point of bossLib is to provide a layer of abstraction so the user has to know only a few entry-points.⁸ (These underlying libraries, and others providing similarly powerful tools are described in detail in sections below.)

   PROVE      : thm list -> term -> thm
   PROVE_TAC  : thm list -> tactic

   METIS_TAC  : thm list -> tactic
   METIS_PROVE: thm list -> term -> thm

   DECIDE     : term quotation -> thm
   DECIDE_TAC : tactic

The inference rule PROVE (and the corresponding tactic PROVE_TAC) takes a list of theorems and a term, and attempts to prove the term using a first order reasoner. The two METIS functions perform the same functionality but use a different underlying proof method. The PROVE entry-points refer to the meson library, which is further described in Section 8.4.1 below. The METIS system is described in Section 8.4.2. The inference rule DECIDE (and the corresponding tactic DECIDE_TAC) applies a decision procedure that (at least) handles statements of linear arithmetic.

   RW_TAC   : simpset -> thm list -> tactic
   SRW_TAC  : ssfrag list -> thm list -> tactic
   &&       : simpset * thm list -> simpset  (* infix *)
   std_ss   : simpset
   arith_ss : simpset
   list_ss  : simpset
   srw_ss   : unit -> simpset

The rewriting tactic RW_TAC works by first adding the given theorems into the given simpset; then it simplifies the goal as much as possible; then it performs case splits on any conditional expressions in the goal; then it repeatedly (1) eliminates all hypotheses of the form $v = M$ or $M = v$ where $v$ is a variable not occurring in $M$, (2) breaks down any equations between constructor terms occurring anywhere in the goal. Finally, RW_TAC lifts let-expressions within the goal so that the binding equations appear as abbreviations in the assumptions.

The tactic SRW_TAC is similar to RW_TAC, but works with respect to an underlying simpset (accessible through the function srw_ss) that is updated as new context is loaded. This simpset can be augmented through the addition of "simpset fragments" (ssfrag values) and theorems. In situations where there are many large types stored in the system, RW_TAC's performance can suffer because it repeatedly adds all of the rewrite theorems for the known types into a simpset before attacking the goal. On the other hand, SRW_TAC loads rewrites into the simpset underneath srw_ss() just once, making for faster operation in this situation.

bossLib provides a number of simplification sets. The simpset for pure logic, sums, pairs, and the option type is named std_ss. The simpset for arithmetic is named arith_ss, and the simpset for lists is named list_ss. The simpsets provided by bossLib strictly increase in strength: std_ss is contained in arith_ss, and arith_ss is contained in list_ss. The infix combinator \&\& is used to build a new simpset from a given simpset and a list of theorems. HOL's simplification technology is described further in Section 8.5 below and in the REFERENCE.

   by : term quotation * tactic -> tactic (* infix 8 *)
   SPOSE_NOT_THEN : (thm -> tactic) -> tactic

The function by is an infix operator that takes a quotation and a tactic $\mathit{tac}$. The quotation is parsed into a term $M$. When the invocation `M` by tac is applied to a goal $(A,g)$, a new subgoal $(A,M)$ is created and $\mathit{tac}$ is applied to it. If the goal is proved, the resulting theorem is broken down and added to the assumptions of the original goal; thus the proof proceeds with the goal $((M::A), g)$. (Note however, that case-splitting will happen if the breaking-down of $\vdash M$ exposes disjunctions.) Thus by allows a useful style of ‘assertional’ or ‘Mizar-like’ reasoning to be mixed with ordinary tactic proof.⁹

The SPOSE_NOT_THEN entry-point initiates a proof by contradiction by assuming the negation of the goal and driving the negation inwards through quantifiers. It provides the resulting theorem as an argument to the supplied function, which will use the theorem to build and apply a tactic.

First Order Proof — mesonLib and metisLib

First order proof is a powerful theorem-proving technique that can finish off complicated goals. Unlike tools such as the simplifier, it either proves a goal outright, or fails. It can not transform a goal into a different (and more helpful) form.

Model elimination — mesonLib

The meson library is an implementation of the model-elimination method for finding proofs of goals in first-order logic. There are three main entry-points:

   MESON_TAC     : thm list -> tactic
   ASM_MESON_TAC : thm list -> tactic
   GEN_MESON_TAC : int -> int -> int -> thm list -> tactic

Each of these tactics attempts to prove the goal. They will either succeed in doing so, or fail with a “depth exceeded” exception. If the branching factor in the search-space is high, the meson tactics may also take a very long time to reach the maximum depth.

All of the meson tactics take a list of theorems. These extra facts are used by the decision procedure to help prove the goal. MESON_TAC ignores the goal's assumptions; the other two entry-points include the assumptions as part of the sequent to be proved.

The extra parameters to GEN_MESON_TAC provide extra control of the behaviour of the iterative deepening that is at the heart of the search for a proof. In any given iteration, the algorithm searches for a proof of depth no more than a parameter $d$. The default behaviour for MESON_TAC and ASM_MESON_TAC is to start $d$ at 0, to increment it by one each time a search fails, and to fail if $d$ exceeds the value stored in the reference value mesonLib.max_depth. By way of contrast, GEN_MESON_TAC\ min\ max\ step starts $d$ at min, increments it by step, and gives up when $d$ exceeds max.

The PROVE_TAC function from bossLib performs some normalisation, before passing a goal and its assumptions to ASM_MESON_TAC. Because of this normalisation, in most circumstances, PROVE_TAC should be preferred to ASM_MESON_TAC.

Resolution — metisLib

The metis library is an implementation of the resolution method for finding proofs of goals in first-order logic. There are two main entry-points:

   METIS_TAC   : thm list -> tactic
   METIS_PROVE : thm list -> term -> thm

Both functions take a list of theorems, and these are used as lemmas in the proof. METIS_TAC is a tactic, and will either succeed in proving the goal, or if unsuccessful will either fail or loop forever. METIS_PROVE takes a term $t$ and tries to prove a theorem with conclusion $t$: if successful, the theorem $\vdash t$ is returned. As for METIS_TAC, it might fail or loop forever if the proof search is unsuccessful.

The metisLib family of proof tools implement the ordered resolution and ordered paramodulation calculus for first order logic, which usually makes them better suited to goals requiring non-trivial equality reasoning than the tactics in mesonLib.

Efficient Applicative Order Reduction — computeLib

Section 7.2 and Section 7.6 show the ability of HOL to represent many of the standard constructs of functional programming. If one then wants to ‘run’ functional programs on arguments, there are several choices. First, one could apply the simplifier, as demonstrated in Section 8.5. This allows all the power of the rewriting process to be brought to bear, including, for example, the application of decision procedures to prove constraints on conditional rewrite rules. Second, one could write the program, and all the programs it transitively depends on, out to a file in a suitable concrete syntax, and invoke a compiler or interpreter. This functionality is available in HOL via use of EmitML.exportML.

Third, computeLib can be used. This library supports call-by-value evaluation of HOL functions by deductive steps. In other words, it is quite similar to having an SML interpreter inside the HOL logic, working by forward inference. When used in this way, functional programs can be executed more quickly than by using the simplifier.

The most accessible entry-points for using the computeLib library are the conversion EVAL and its tactic counterpart EVAL_TAC. These depend on an internal database that stores function definitions. In the following example, loading sortingTheory augments this database with relevant definitions, that of Quicksort (QSORT) in particular, and then we can evaluate QSORT on a concrete list.

> load "sortingTheory";
val it = (): unit

> EVAL ``QSORT (<=) [76;34;102;3;4]``;
<<HOL message: more than one resolution of overloading was possible>>
<<HOL message: inventing new type variable names: 'a>>
val it = ⊢ QSORT $<= [76; 34; 102; 3; 4] = QSORT $<= [76; 34; 102; 3; 4]: thm

Often, the argument to a function has no variables: in that case application of EVAL ought to return a ground result, as in the above example. However, EVAL can also evaluate functions on arguments with variables — so-called symbolic evaluation — and in that case, the behaviour of EVAL depends on the structure of the recursion equations. For example, in the following session, if there is sufficient information in the input, symbolic execution can deliver an interesting result. However, if there is not enough information in the input to allow the algorithm any traction, no expansion will take place.

> EVAL ``REVERSE [u;v;w;x;y;z]``;
<<HOL message: inventing new type variable names: 'a>>
val it = ⊢ REVERSE [u; v; w; x; y; z] = [z; y; x; w; v; u]: thm

> EVAL ``REVERSE alist``;
<<HOL message: inventing new type variable names: 'a>>
val it = ⊢ REVERSE alist = REV alist []: thm

Dealing with divergence

The major difficulty with using EVAL is termination. All too often, symbolic evaluation with EVAL will diverge, or generate enormous terms. The usual cause is conditionals with variables in the test. For example, the following definition is provably equal to FACT,

> Define `fact n = if n=0 then 1 else n * fact (n-1)`;
<<HOL warning: ThmSetData.revise_data: 
  Theorems in set "compute":
    ADD<scratch$fact_def>
  invalidated by NewBinding("fact_def", {private=false,loc=Unknown,class=Thm})>>
Equations stored under "fact_def".
Induction stored under "fact_ind".
val it = ⊢ ∀n. fact n = if n = 0 then 1 else n * fact (n − 1): thm

But the two definitions evaluate completely differently.

> EVAL ``FACT n``;
val it = ⊢ FACT n = FACT n: thm

> EVAL ``fact n``;
  <.... interrupt key struck ...>
Interrupted.

The primitive-recursive definition of FACT does not expand at all, while the destructor-style recursion of fact never stops expanding. A rudimentary monitoring facility shows the behaviour, first on a ground argument, then on a symbolic argument.

> val [fact] = decls "fact";
val fact = “fact”: term
> computeLib.monitoring := SOME (same_const fact);
val it = (): unit

> EVAL ``fact 4``;
fact 4 = if 4 = 0 then 1 else 4 * fact (4 − 1)
fact 3 = if 3 = 0 then 1 else 3 * fact (3 − 1)
fact 2 = if 2 = 0 then 1 else 2 * fact (2 − 1)
fact 1 = if 1 = 0 then 1 else 1 * fact (1 − 1)
fact 0 = if 0 = 0 then 1 else 0 * fact (0 − 1)
val it = ⊢ fact 4 = 24: thm

> EVAL ``fact n``;
fact n = (if n = 0 then 1 else n * fact (n - 1))
fact (n - 1) = (if n - 1 = 0 then 1 else (n - 1) * fact (n - 1 - 1))
fact (n - 1 - 1) =
(if n - 1 - 1 = 0 then 1 else (n - 1 - 1) * fact (n - 1 - 1 - 1))
fact (n - 1 - 1 - 1) =
(if n - 1 - 1 - 1 = 0 then
   1
 else
   (n - 1 - 1 - 1) * fact (n - 1 - 1 - 1 - 1))
   .
   .
   .

In each recursive expansion, the test involves a variable, and hence cannot be reduced to either T or F. Thus, expansion never stops.

Some simple remedies can be adopted in trying to deal with non-terminating symbolic evaluation.

• RESTR_EVAL_CONV behaves like EVAL except it takes an extra list of constants. During evaluation, if one of the supplied constants is encountered, it will not be expanded. This allows evaluation down to a specified level, and can be used to cut-off some looping evaluations.

• set_skip can also be used to control evaluation. See the REFERENCE entry for CBV_CONV for discussion of set_skip.

Custom evaluators

For some problems, it is desirable to construct a customized evaluator, specialized to a fixed set of definitions. The compset type found in computeLib is the type of definition databases. The functions new_compset, bool_compset, add_funs, and add_convs provide the standard way to build up such databases. Another quite useful compset is reduceLib.num_compset, which may be used for evaluating terms with numbers and booleans. Given a compset, the function CBV_CONV generates an evaluator: it is used to implement EVAL. See REFERENCE for more details.

Dealing with Functions over Peano Numbers

Functions defined by pattern-matching over Peano-style numbers cannot be used by EVAL to compute the application of those functions to numerals. This is because numerals are represented with a binary positional notation (described in Section 5.3.3). The Peano-style presentation is important for proofs about these functions, so we encourage definitions in this style. For the sake of computation, HOL's definitional facilities will automatically use the SML function numLib.SUC_TO_NUMERAL_DEFN_CONV to derive equations over numerals from an equation over SUC.

> Definition mod3_def:
    mod3 0 = 0 /\
    mod3 (SUC n) = let m = mod3 n in
                   if m = 2 then 0 else m + 1
  End   ... output elided ...
> EVAL “mod3 11”;
val it = ⊢ mod3 11 = 2: thm

Storing and using definitions

HOL's top-level definition facilities (i.e., the Define function and the Definition syntax) automatically add definitions to the global compset used by EVAL and EVAL_TAC.

Occasionally, one does not want a definition automatically added to the global compset. The easiest way to achieve this is to use the nocompute “pseudo-attribute”:¹⁰

> Definition f_def[nocompute]: f x = x + 10
  End
Definition has been stored under "f_def"
val f_def = ⊢ ∀x. f x = x + 10: thm
> EVAL ``f 6``;
val it = ⊢ f 6 = f 6: thm

By using the nocompute attribute, or lower level tools such as Hol_defn, defining equations are not added to the global compset. Subsequently, one may want to specify theorems to be used as the basis for EVAL's computation. This can be done with the compute attribute attached to a theorem declaration. For example, one might write

> Theorem f_6[compute]: f 6 = 16
  Proof simp[f_def]
  QED
val f_6 = ⊢ f 6 = 16: thm

> EVAL “f 6 = f 7”;
val it = ⊢ f 6 = f 7 ⇔ 16 = f 7: thm

Computation with First-Order Terms — cv_computeLib and cv_transLib

The library cv_computeLib supports fast evaluation of HOL terms. It exports a single conversion, cv_compute, which accepts terms in a simple, first-order, untyped language built from a recursive datatype of pairs and natural numbers. Its accompanying theory, cvTheory, defines this type (called :cv) and its operations. When applicable, cv_computeLib will often execute several orders of magnitude faster than computeLib (Section 8.6) on similar inputs. Such performance is possible because cv_computeLib relies on an interpreter that is implemented inside the kernel, and that uses native ML datatypes and arbitrary precision integer arithmetic to execute quickly. This implementation is a Standard ML adaption of the compute facility in the Candle theorem prover, which has been proved to be sound wrt. the inference rules of higher-order logic (Abrahamsson and Myreen 2023).

The library cv_transLib provides a user-friendly interface to cv_computeLib. It exports automation which translates functional HOL definitions into equivalent functions which operate over the :cv type, and a wrapper around cv_computeLib.cv_compute called cv_eval which can be used much like computeLib.EVAL (Section 8.6). Its accompanying theories (cv_primTheory and cv_stdTheory) define and translate various common operations over primitive types.

Computing with cv_compute directly

The following example shows how to define a (very simple) function and use it in a computation with cv_compute.

NB: this example illustrates how cv_compute works, but is not the recommended workflow for using it. Instead, use cv_transLib (Section 8.7.3).

> load "cv_computeLib";
val it = (): unit
> Definition square_def:
    square x = cv_mul x x
  End
Definition has been stored under "square_def"
val square_def = ⊢ ∀x. square x = cv_mul x x: thm
> cv_computeLib.cv_compute [square_def] ``square (cv$Num 7)``;
val it = ⊢ square (cv$Num 7) = cv$Num 49: thm

To reduce a term involving the constant square, cv_compute must be given its defining equation (square_def), and both the input term and this equation must be written in a special style, using a special set of operations (such as cv_mul). We call defining equations and terms in this style code equations and compute expressions, respectively.

Compute expressions

A compute expression is a closed, first-order expression with type :cv. The :cv datatype is defined in cvTheory as follows:

  Datatype: cv = Pair cv cv
               | Num num
  End

Aside from the :cv datatype constructors, the following operations can be used to construct new compute expressions:

Arithmetic

Pairs

Miscellaneous

The following holds for the semantics of these operations:

• Arithmetic works as on HOL's natural numbers.
• Boolean-like expressions (such as cv_if) treat Num 1 as true, and all other values as false.
• All ill-typed expressions (such as cv_fst (Num 3)) are defined as Num 0.
• Function constants must have a corresponding code equation, see below.

Code equations

A theorem $\mathtt{f}\;x_1 \cdots x_n = e$ is a code equation for f, if:

• $x_1 \cdots x_n$ are variables of type :cv,
• $e$ has type :cv,
• $e$ is a compute expression, except that the variables $x_i$ may be free in $e$.

Example: computing factorial

The following example is taken from the cv_computeLib examples, available in exampleTheory in examples/cv_compute, and has been modified to showcase let-bindings:

> load "cv_computeLib";
val it = (): unit

> Definition fact_def:
   fact n =
     let one = cv$Num 1 in
     cv_if (cv_lt n one)
           one
           (cv_mul n (fact (cv_sub n one)))
  Termination
   WF_REL_TAC `measure cv_size` >>
   Cases >>
   simp [cv_size_def, CaseEq "bool", c2b_def]
  End   ... output elided ...

> time (cv_computeLib.cv_compute [fact_def]) “fact (cv$Num 1234)”;
runtime: 0.11815s,    gctime: 0.00000s,     systime: 0.00068s.
val it =
   ⊢ fact (cv$Num 1234) =
     cv$Num
       51084981466469576881306176261004598750272741624636207875758364885...
   thm

On a modern machine, the call to cv_compute finishes in less than two tenths of a second.

Thm.compute

The conversion cv_compute is built on top of a kernel primitive accessible through the function Thm.compute:

  type instantiation =
    { cval_terms : (string * term) list,
      cval_type  : hol_type,
      num_type   : hol_type,
      char_eqns  : (string * thm) list }
  val compute : instantiation -> thm list -> term -> thm

Before it can be used, Thm.compute must be instantiated with a record containing constants, types and characteristic theorems for the constants and types. The list of characteristic equations is rather large, and need only be passed to compute once (the application is cached). Indeed, this instantiation is the sole duty performed by cv_computeLib.

The reason for why this instantiation must occur is as follows. Internally, Thm.compute takes apart the HOL logic's terms and converts them into its own representation, performs computation, and converts the result back into a term. The soundness of this procedure depends on various constants and types having certain meanings; for example, that + is natural number addition, and that the following holds:

ADD
  ⊢ (∀n. 0 + n = n) ∧ ∀m n. SUC m + n = SUC (m + n)

However, natural numbers, arithmetic, and theorems like ADD are derived long after the kernel code is compiled.

Alternative instantiations

It is possible to instantiate Thm.compute differently, for example if one wants to use a different type of numbers (as long as it satisfies the same axioms). An example instantiation can be seen in the source code of cv_computeLib in the HOL sources; the list of types, constants and symbols required is too long to include here.

Further reading

For an in-depth explanation of Thm.compute, we refer the reader to the Candle theorem prover's compute primitive (Abrahamsson and Myreen 2023), on which Thm.compute is based.

Computing with cv_compute via cv_transLib

It is also possible to use cv_compute on HOL functions that are not defined using the :cv type, using cv_transLib. This library supports automatic translation of functions to equivalent versions operating over the :cv type, and maintains a database of known translations. Then, the cv_eval entrypoint can be used on a regular HOL term: it uses the database to translate the term to an equivalent :cv version, invokes cv_compute, and translates the result back from the :cv type. Note therefore that, like cv_compute, cv_eval accepts only closed terms. All constants in its input must also be found in its database of known translations. Therefore, the intended workflow for using cv_transLib is as follows:

1. Define HOL functions in the usual way.
2. Invoke cv_transLib to translate these functions to :cv versions, populating the database of known translations.
3. Use cv_transLib.cv_eval to evaluate terms composed of known constants efficiently.

Translation entrypoints

There are eight entrypoints in cv_transLib for translating HOL functions to :cv equivalents: cv_trans, cv_trans_pre, cv_trans_rec, cv_trans_rec_pre, cv_auto_trans, cv_auto_trans_pre, cv_auto_trans_rec, and cv_auto_trans_rec_pre.

All accept a theorem representing a HOL definition. Those with prefix cv_trans fail if, during translation, they encounter a constant which does not have a known translation. Those with prefix cv_auto_trans invoke themselves recursively on any such unknown constants.

Translation of some HOL functions give rise to a precondition (for example, listheory.HD requires its argument to be non-empty). All eight entrypoints will attempt to discharge simple preconditions, but the variants containing pre allow a more complex precondition to persist and return its definition to the user. Preconditions bubble up through further translations, and must be discharged for any term used with cv_eval. The other variants fail if they encounter a precondition they cannot discharge.

Translation of a recursive HOL function produces a recursive :cv function, which may require a termination proof. All eight entrypoints attempt to discharge simple termination proofs, but the variants containing rec accept an additional argument, a tactic which should discharge a more complex termination goal. The other variants will fail if they cannot prove termination.

Examples: computing squares and factorials

The following example mirrors those in Section 8.7.1, but it uses cv_transLib instead of interacting directly with the :cv type.

> load "cv_transLib";
val it = (): unit
> load "cv_stdTheory";
val it = (): unit

> Definition square'_def:
    square' (x:num) = x * x
  End
Definition has been stored under "square'_def"
val square'_def = ⊢ ∀x. square' x = x * x: thm

> cv_transLib.cv_trans square'_def;
val it = (): unit

> cv_transLib.cv_eval ``square' 7``;
val it = ⊢ square' 7 = 49: thm

> arithmeticTheory.FACT;
val it = ⊢ FACT 0 = 1 ∧ ∀n. FACT (SUC n) = SUC n * FACT n: thm

> cv_transLib.cv_trans arithmeticTheory.FACT;
Equations stored under "cv_FACT_def".
Induction stored under "cv_FACT_ind".
val it = (): unit

> time cv_transLib.cv_eval ``FACT 1234``;
runtime: 0.12709s,    gctime: 0.00000s,     systime: 0.00026s.
val it =
   ⊢ FACT 1234 =
     5108498146646957688130617626100459875027274162463620787575836488567...
   thm

Further usage examples are located in examples/cv_compute.

Arithmetic Libraries — numLib, intLib and realLib

Each of the arithmetic libraries of HOL provide a suite of definitions and theorems as well as automated inference support.

numLib

The most basic numbers in HOL are the natural numbers. The numLib library encompasses the theories numTheory, prim_recTheory, arithmeticTheory, and numeralTheory. This library also incorporates an evaluator for numeric expression from reduceLib and a decision procedure for linear arithmetic ARITH_CONV. The evaluator and the decision procedure are integrated into the simpset arith_ss used by the simplifier. As well, the linear arithmetic decision procedure can be directly invoked through DECIDE and DECIDE_TAC, both found in bossLib.

intLib

The intLib library comprises integerTheory, an extensive theory of the integers, plus two decision procedures for full Presburger arithmetic. These are available as intLib.COOPER_CONV and intLib.ARITH_CONV. These decision procedures are able to deal with linear arithmetic over the integers and the natural numbers, as well as dealing with arbitrary alternation of quantifiers. The ARITH_CONV procedure is an implementation of the Omega Test, and seems to generally perform better than Cooper's algorithm. There are problems for which this is not true however, so it is useful to have both procedures available.

In addition, the intLib.INTEGER_RULE (and its tactic version intLib.INTEGER_TAC) ported from HOL-Light can solve some simple equations about divisibility of integers, e.g. d int_divides m ==> d int_divides (m * n). As part of the procedure, multivariate polynomials of integer are expanded to their “normal forms” (with respect to certain ordering), and thus equations between equivalent such polynomials can be decided, e.g. w * y + x * z - (w * z + x * y) = (w - x) * (y - z).

realLib

The realLib library provides a foundational development of the real numbers and analysis. See Section 5.3.6 for a quick description of the theories. Also provided is a theory of polynomials, in polyTheory. A decision procedure for linear arithmetic on the real numbers is also provided by realLib, under the name REAL_ARITH_CONV and REAL_ARITH_TAC.

Bit Vector Library — wordsLib

The library wordsLib provides tool support for bit-vectors, this includes facilities for: evaluation, parsing, pretty-printing and simplification.

Evaluation

The library wordsLib should be loaded when evaluating ground bit-vector terms. This library provides a compset words_compset, which can be used in the construction of custom compsets and conversions.

> load "wordsLib";
val it = (): unit

> EVAL ``8w + 9w:word4``;
val it = ⊢ 8w + 9w = 1w: thm

Note that a type annotation is used here to designate the word size. When the word size is represented by a type variable (i.e., for arbitrary length words), evaluation may give partial or unsatisfactory results.

Parsing and pretty-printing

Words can be parsed in binary, decimal and hexadecimal. For example:

> ``0b111010w : word8``;
val it = “58w”: term

> ``0x3Aw : word8``;
val it = “58w”: term

It is possible to parse octal numbers, but this must be enabled first by setting the reference base_tokens.allow_octal_input to true. For example:

> ``072w : word8``;
val it = “72w”: term

> base_tokens.allow_octal_input:=true;
val it = (): unit

> ``072w : word8``;
val it = “58w”: term

Words can be pretty-printed using the standard number bases. For example, the function wordsLib.output_words_as_bin will select binary format:

> wordsLib.output_words_as_bin();
val it = (): unit

> EVAL ``($FCP ODD):word16``;
val it = ⊢ $FCP ODD = 0b1010101010101010w: thm

The function output_words_as is more flexible and allows the number base to vary depending on the word length and numeric value. The default pretty-printer (installed when loading wordsLib) prints small values in decimal and large values in hexadecimal. The function output_words_as_oct will automatically enable the parsing of octal numbers.

The trace variable "word printing" provides an alternative method for changing the output number base — it is particularly suited to temporarily selecting a number base, for example:

> Feedback.trace ("word printing", 1) Parse.term_to_string ``32w``;
<<HOL message: inventing new type variable names: 'a>>
val it = "0b100000w": string

The choices are as follows: 0 (default) — small numbers decimal, large numbers hexadecimal; 1 — binary; 2 — octal; 3 — decimal; and 4 — hexadecimal.

Types

You may have noticed that :word4 and :word8 have been used as convenient parsing abbreviations for :bool[4] and :bool[8] — this facility is available for many standard word sizes. Users wishing to use this notation for non-standard word sizes can use the function wordsLib.mk_word_size:

> Lib.try Parse.Type `:word15` handle _ => bool;

Exception raised at Parse.type parser: on line 1, characters 21-26:
  word15 not a known type operator
val it = “:bool”: hol_type

> wordsLib.mk_word_size 15;
val it = (): unit

> ``:word15``;
val it = “:word15”: hol_type

Operator overloading

The symbols for the standard arithmetic operations (addition, subtraction and multiplication) are overloaded with operators from other standard theories, i.e., for the natural, integer, rational and real numbers. In many cases type inference will resolve overloading, however, in some cases this is not possible. The choice of operator will then depend upon the order in which theories are loaded. To change this behaviour the functions wordsLib.deprecate_word and wordsLib.prefer_word are provided. For example, in the following session, the selection of word operators is deprecated:

> type_of ``a + b``;
<<HOL message: more than one resolution of overloading was possible>>
<<HOL message: inventing new type variable names: 'a>>
val it = “:α word”: hol_type

> wordsLib.deprecate_word();
val it = (): unit

> type_of ``a + b``;
<<HOL message: more than one resolution of overloading was possible>>
val it = “:num”: hol_type

In the above, natural number addition is chosen in preference to word addition. Conversely, words are preferred over the integers below:

> type_of ``a + b``;
<<HOL message: more than one resolution of overloading was possible>>
val it = “:num”: hol_type

> wordsLib.prefer_word();
val it = (): unit
> type_of ``a + b``;
<<HOL message: more than one resolution of overloading was possible>>
<<HOL message: inventing new type variable names: 'a>>
val it = “:α word”: hol_type

Of course, type annotations could have been added to avoid this problem entirely.

Guessing word lengths

It can be a nuisance to add type annotations when specifying the return type for operations such as: word_extract, word_concat, concat_word_list and word_replicate. This is because there is often a “standard” length that could be guessed, e.g., concatenation usually sums the constituent word lengths. A facility for word length guessing is controlled by the reference wordsLib.guessing_word_lengths, which is false by default. The guesses are made during a post-processing step that occurs after the application of Parse.Term. This is demonstrated below.

> wordsLib.guessing_word_lengths:=true;
val it = (): unit

> ``concat_word_list [(4 >< 1) (w:word32); w2; w3]``;
<<HOL message: inventing new type variable names: 'a, 'b>>
<<HOL message: assigning word length: α <- 4>>
<<HOL message: assigning word length: β <- 12>>
val it = “concat_word_list [(4 >< 1) w; w2; w3]”: term

In the example above, word length guessing is turned on. Two guesses are made: the extraction is expected to give a four bit word, and the concatenation gives a twelve bit word ($3 \times 4$). If non-standard numeric lengths are required then type annotations can be added to avoid guesses being made. With guessing turned off, the result types would remain as invented type variables, i.e., as alpha and beta above.

Simplification and conversions

The following simpset fragments are provided:

SIZES_ss: evaluates a group of functions that operate over numeric types, such as dimindex and dimword.

BIT_ss: tries to simplify occurrences of the function BIT.

WORD_LOGIC_ss: simplifies bitwise logic operations.

WORD_ARITH_ss: simplifies word arithmetic operations. Subtraction is replaced with multiplication by -1.

WORD_SHIFT_ss: simplifies shift operations.

WORD_ss: contains all of the above fragments, and also does some extra ground term evaluation. This fragment is added to srw_ss.

WORD_ARITH_EQ_ss: simplifies `a = b` to `a - b = 0w`.

WORD_BIT_EQ_ss: aggressively expands non-arithmetic bit-vector operations into Boolean expressions. (Should be used with care — it includes fcpLib.FCP_ss.)

WORD_EXTRACT_ss: simplification for a variety of operations: word-to-word conversions; concatenation; shifts and bit-field extraction. Can be used in situations where WORD_BIT_EQ_ss is unsuitable.

WORD_MUL_LSL_ss: simplifies multiplication by a word literal into a sum of partial products.

Many of these simpset fragments have corresponding conversions. For example, the conversion WORD_ARITH_CONV is based on WORD_ARITH_EQ_ss, however, it does some extra work to ensure that `a = b` and `b = a` convert into the same expression. Therefore, this conversion is suited to reasoning about the equality of arithmetic word expressions.

The behaviour of the fragments listed above are demonstrated using the following function:

> fun conv ss = SIMP_CONV (pure_ss++ss) [];
val conv = fn: ssfrag -> conv

The following session demonstrates SIZES_ss:

> conv wordsLib.SIZES_ss ``dimindex(:12)``;
val it = ⊢ dimindex (:12) = 12: thm

> conv wordsLib.SIZES_ss ``FINITE univ(:32)``;
val it = ⊢ FINITE 𝕌(:32) ⇔ T: thm

The fragment BIT_ss converts BIT into membership test over a set of (high) bit positions:

> conv wordsLib.BIT_ss ``BIT 3 5``;
val it = ⊢ BIT 3 5 ⇔ F: thm

> conv wordsLib.BIT_ss ``BIT i 123``;
val it = ⊢ BIT i 123 ⇔ i ∈ {0; 1; 3; 4; 5; 6}: thm

This simplification provides some support for reasoning about bitwise operations over arbitrary word lengths. The arithmetic, logic and shift fragments help tidy up basic word expressions:

> conv wordsLib.WORD_LOGIC_ss ``a && 12w || 11w && a``;
<<HOL message: inventing new type variable names: 'a>>
val it = ⊢ a && 12w ‖ 11w && a = 15w && a: thm

> conv wordsLib.WORD_ARITH_ss ``3w * b + a + 2w * b - a * 4w:word2``;
val it = ⊢ 3w * b + a + 2w * b − a * 4w = a + b: thm

> conv wordsLib.WORD_SHIFT_ss ``0w << 12 + a >>> 0 + b << 2 << 3``;
<<HOL message: inventing new type variable names: 'a>>
val it = ⊢ 0w ≪ 12 + a ⋙ 0 + b ≪ 2 ≪ 3 = 0w + a + b ≪ (2 + 3): thm

The remaining fragments are not included in wordsLib.WORD_ss or srw_ss. The bit equality fragment is demonstrated below.

> SIMP_CONV (std_ss++wordsLib.WORD_BIT_EQ_ss) [] ``a && b = ~0w : word2``;
val it = ⊢ a && b = ¬0w ⇔ (a ' 1 ∧ b ' 1) ∧ a ' 0 ∧ b ' 0: thm

The extract fragment is useful for reasoning about bit-field operations and is best used in combination with wordsLib.SIZES_ss or wordsLib.WORD_ss, for example:

> SIMP_CONV (std_ss++wordsLib.SIZES_ss++wordsLib.WORD_EXTRACT_ss) []
    ``(4 -- 1) ((a:word3) @@ (b:word2)) : word5``;
val it = ⊢ (4 -- 1) (a @@ b) = (2 >< 0) a ≪ 1 ‖ (1 >< 1) b: thm

Finally, the fragment WORD_MUL_LSL_ss is demonstrated below.

> conv wordsLib.WORD_MUL_LSL_ss ``5w * a : word8``;
val it = ⊢ 5w * a = a ≪ 2 + a: thm

Rewriting with the theorem wordsTheory.WORD_MUL_LSL provides an means to undo this simplification, for example:

> SIMP_CONV (std_ss++wordsLib.WORD_ARITH_ss) [wordsTheory.WORD_MUL_LSL]
    ``a << 2 + a : word8``;
val it = ⊢ a ≪ 2 + a = 5w * a: thm

Obviously, without adding safeguards, this rewrite theorem cannot be deployed when used in combination with the WORD_MUL_LSL_ss fragment.

Decision procedures

A decision procedure for words is provided in the form of blastLib.BBLAST_PROVE. This procedure uses bit-blasting — converting word expressions into propositions and then using a SAT solver to decide the goal.¹¹ This approach is reasonably general and can tackle a wide range of bit-vector problems. However, there are some limitations: the approach only works for constant word lengths, linear arithmetic (multiplication by literals) and for shifts and bit-field extractions with respect to literal values. Also note that some problems will be potentially slow to prove, e.g., when word sizes are large and/or when there are many nested additions (perhaps through multiplication).

The following examples show BBLAST_PROVE in use:

> load "blastLib";   ... output elided ...
> blastLib.BBLAST_PROVE ``a + 2w <+ 4w <=> a <+ 2w \/ 13w <+ a :word4``;
val it = ⊢ a + 2w <₊ 4w ⇔ a <₊ 2w ∨ 13w <₊ a: thm

> blastLib.BBLAST_PROVE ``w2w (a:word8) <+ 256w : word16``;
val it = ⊢ w2w a <₊ 256w: thm

The decision procedure BBLAST_PROVE is based on the conversion BBLAST_CONV. This conversion can be used to convert bit-vector problems into a propositional form; for example:

> blastLib.BBLAST_CONV ``(((a : word16) + 5w) << 3) ' 5``;
val it = ⊢ ((a + 5w) ≪ 3) ' 5 ⇔ (¬a ' 2 ⇔ ¬(a ' 1 ∧ a ' 0)): thm

There are also bit-blasting tactics: BBLAST_TAC and FULL_BBLAST_TAC; with only the latter making use of goal assumptions.

1. The types in Absyn constraints are not full HOL types, but values from another intermediate type, Pretype. ↩

2. The use of local induces a call to the temp_overload_on function. ↩

3. The matching done is first-order; contrast the higher-order matching done in the simplifier. ↩

4. When pairTheory has been loaded. ↩

5. There are tighter infix operators: the dot in field selection causes $f\,x.fld$ to parse as $f\cdot(x.fld)$. ↩

6. Note that doing the same thing for the if-then-else example in the previous example would be inappropriate, as it would allow one to write $$ \mathtt{if}\;P\;\mathtt{then}\;Q\;\mathtt{else} $$ without the trailing argument. ↩

7. Complete induction and ordinary mathematical induction are each derivable from the other. ↩

8. In the mid 1980's Graham Birtwistle advocated such an approach, calling it ‘Ten Tactic HOL’. ↩

9. Proofs in the Mizar system are readable documents, unlike most tactic-based proofs. ↩

10. The nocompute attribute does nothing when applied to Theorem declarations. ↩

11. This approach enables counter-examples to be given when a goal's negation is satisfiable. ↩