HOL stands for higher-order logic. HOL is also the name of a theorem prover, the HOL theorem prover. This is a guidebook for the theorem prover.

I assume you are familiar with functional programming and higher-order logic. (If you are not, don’t worry, these topics will be treated gently and are easy to pick up.) The main point of this tutorial is to show you how to build theories in the HOL theorem prover, assuming you have an idea of what you want to formalise and how to prove your theorems mathematically.

If you have trouble with anything, there is plenty of community support available including mailing lists and online chat. See the HOL website for details.

For support on or contributions to this guidebook itself, see its repository on GitHub.

Go to the HOL website. Follow the instructions there to install HOL.

Alternatively, you can follow the first part of the CakeML build instructions.

It is a good idea to set the environment variable
`$HOLDIR`

to point to the location of your HOL installation.
I will refer to this directory by `$HOLDIR`

from now on.

Now you can run `hol`

at the command line. You will be
greeted with a welcome message, and prompted with a read-eval-print loop
(REPL). This is in fact the REPL for the underlying ML system.

HOL is just a library for theorem proving in Standard ML (abbreviated as ML). Interacting with HOL, therefore, can be seen as programming in ML. If you don’t use any of the HOL-specific parts, you just have Standard ML:

```
> 3 + 4;
val it = 7: int
```

The HOL additions include new datatypes like `thm`

, which
represents a proven theorem. Some values of this type are already in
scope:

```
> SKOLEM_THM;
val it = ⊢ ∀P. (∀x. ∃y. P x y) ⇔ ∃f. ∀x. P x (f x): thm
```

Usual practice is not to program directly at the REPL. Instead, you
write a *script file* which can be processed by a tool called
`Holmake`

to build a theory. A typical script file looks like
this:

```
open HolKernel boolLib bossLib Parse;
val _ = new_theory"test";
(* SML declarations *)
(* for example: *)
val th = save_thm("SKOLEM_AGAIN",SKOLEM_THM);
val _ = export_theory();
```

The script file above should be saved as `testScript.sml`

,
because the name passed to `new_theory`

is
`"test"`

. To produce a theory from this script file, run
`Holmake`

as follows:

`$ Holmake testTheory.uo`

`Holmake`

knows to look for `testScript.sml`

when given the target `testTheory.uo`

. It will run the script
and produce the following files as output: `testTheory.sig`

,
`testTheory.sml`

, `testTheory.ui`

, and
`testTheory.uo`

.

The `testTheory.sig`

file contains a summary of the
contents of the generated theory. In this case, you will see that
`testTheory`

contains a single theorem, which is just a copy
of `SKOLEM_THM`

saved under the name
`SKOLEM_AGAIN`

.

The other generated files are the mechanism by which persistent theories are implemented on disk, and can be ignored for now.

One would like to develop a script file with the same ease as
programming at the REPL. For this, there are plugins for two text
editors, Vim and Emacs, which enable script-file writing alongside an
interactive HOL session. Both are included in your HOL installation. The
Vim plugin is documented at `$HOLDIR/tools/vim/README`

(also
here). The Emacs plugin is documented online.

The idea behind these interaction plugins is to write a script file
that will eventually be suitable for processing by `Holmake`

,
but to see, step-by-step in the REPL, what is happening at each point of
the script file as you are writing it.

As an example, let’s try the Vim plugin on the
`testScript.sml`

file from above. First, install the Vim
plugin by following the instructions in its `README`

. Next,
open `testScript.sml`

in Vim, and also start
`hol`

. I usually put these two windows (`hol`

and
`vim`

) side by side, so I can see what is happening in both
at once.

We begin processing from the top of the file. Select the first line
(the one containing `open`

). (To select a line in
`vim`

, position the cursor on the line and press
`V`

.) Tell `hol`

to load those theories and
libraries by typing `hl`

. You should see some output
like:

`HOLLoadSendQuiet HolKernel boolLib bossLib Parse completed`

Next, move down to the line containing `save_thm`

and send
it to `hol`

by typing `hs`

. You should see some
output like:

`val th = ⊢ ∀P. (∀x. ∃y. P x y) ⇔ ∃f. ∀x. P x (f x): thm`

You can, at this point, also write directly into the REPL if you want. For example, to see that this theorem has no hypotheses, try:

```
> hyp th;
val it = []: term list
```

But of course, if you want to add anything to the theory you produce, you should write it in the script file.

The syntax of higher-order logic includes types and terms. These are two of the main datatypes implemented by HOL, over and above what is provided by ML. Here is a type:

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

In fact, `bool`

is one of a handful of types that are
bound to ML variables by default. In general, you can make a type by
providing the name of a type operator and a list of arguments:

```
> mk_type("bool",[]);
val it = “:bool”: hol_type
> mk_type("list",[bool]); (* the type of a list of Booleans *)
val it = “:bool list”: hol_type
> dest_type it;
val it = ("list", [“:bool”]): string * hol_type list
```

Type variables can also be made by providing a name.

```
> mk_vartype("'test");
val it = “:'test”: hol_type
> mk_vartype("'f");
val it = “:ζ”: hol_type
> dest_vartype it;
val it = "'f": string
```

Type variable names, by convention, start with a single quote, unless they are a Greek letter. The first several letters of the (Roman) alphabet are synonymous with certain Greek letters (as demonstrated above).

Every type in HOL is either a type variable or a type operator (like
`list`

) applied to type arguments. Even `bool`

is
a type operator; it has no arguments.

Logically, there are only two primitive type operators:
`bool`

, and `fun`

, the type of functions. Others,
like `list`

, are defined types, but they are already defined
by default. Function types can be manipulated as follows.

```
> val ty = bool --> alpha;
val ty = “:bool -> α”: hol_type
> dom_rng ty;
val it = (“:bool”, “:α”): hol_type * hol_type
> dest_type ty;
val it = ("fun", [“:bool”, “:α”]): string * hol_type list
```

If you try to destruct a type operator as if it were a variable, HOL will raise an exception.

```
> is_vartype bool;
val it = false: bool
> dest_vartype bool;
Exception- HOL_ERR
{message = "not a type variable", origin_function = "dest_vartype",
origin_structure = "Type"} raised
```

It is often more convenient to call the *type parser* rather
than `mk_type`

directly. Compare these alternatives for
building a certain type.

```
> mk_type("fun",[mk_type("list",[mk_type("num",[])]),mk_type("num",[])]);
val it = “:num list -> num”: hol_type
> let val num = mk_type("num",[]) in mk_type("list",[num]) --> num end;
val it = “:num list -> num”: hol_type
> ``:num list -> num``;
val it = “:num list -> num”: hol_type
```

The backticks (`) above are special syntax provided by HOL for
calling the type parser. The underlying parser function is called
`Type`

. We can call the parser more directly:

```
> Type `:num list -> num`;
val it = “:num list -> num”: hol_type
```

The single backticks represent another special syntax, this time for
a *quotation*. Removing the special syntax entirely, we can
write:

```
> Type [QUOTE":num list -> num"];
val it = “:num list -> num”: hol_type
```

The string passed to the type parser should start with a colon as above.

Types can include variables. `alpha`

is bound to a type
variable, which can also be written as `:'a`

.

```
> alpha; ``:'a``;
val it = “:α”: hol_type
val it = “:α”: hol_type
```

(In the example above, two results are printed because two declarations were provided.)

Quotations can include values that do not need to be parsed. For example:

```
> ``:^alpha list``;
val it = “:α list”: hol_type
> ``:^(mk_type("list",[alpha])) list``; (* list of lists of alphas *)
val it = “:α list list”: hol_type
```

The last input expression is syntactic sugar for:

```
> Type [QUOTE":", ANTIQUOTE (mk_type("list",[alpha])), QUOTE " list"];
val it = “:α list list”: hol_type
```

The terms of higher-order logic include: variables, constants, abstractions, and combinations (sometimes called applications). I will show examples of all these kinds of terms, made both using term-making functions directly and using the term parser.

A variable is identified by a name and a type.

```
> val x = mk_var("x",beta);
val x = “x”: term
> val x = ``x:β``; (* or ``x:'b`` *)
val x = “x”: term
```

If you don’t provide a type, HOL will invent one.

```
> val y = ``y``;
<<HOL message: inventing new type variable names: 'a>>
val y = “y”: term
```

Variables are equal if and only if both their name and type match.

```
> Term.compare (y,``y:'b``);
val it = LESS: order
> Term.compare (y, mk_var("y",alpha));
val it = EQUAL: order
```

A constant also has a name and a type.

```
> val z = mk_const("0",``:num``);
val z = “0”: term
> val z = ``0``;
val z = “0”: term
```

Unlike variables, the type of a constant is fixed.

```
> mk_const("0",bool);
Exception- HOL_ERR
{message = "not a type match", origin_function = "create_const",
origin_structure = "Term"} raised
```

So why provide a type at all? Because constants can be
*polymorphic*. More details about polymorphism below.

Furthermore, unlike variable names, constant names are scoped into
theories. More details about theories later. The
full name of a constant can be recovered with
`dest_thy_const`

.

```
> dest_thy_const z;
val it = {Name = "0", Thy = "num", Ty = “:num”}:
{Name: string, Thy: string, Ty: hol_type}
```

An abstraction represents a function. It consists of a variable and a term (body).

```
> val f = mk_abs(x,z);
val f = “λx. 0”: term
> val f = ``λx:β. 0``; (* or ``\x:'b. 0`` *)
val f = “λx. 0”: term
> dest_abs f;
val it = (“x”, “0”): term * term
```

Terms can be tested for *alpha-equivalence*, which means
equality up to a renaming of bound variables, using
`aconv`

.

```
> aconv f (mk_abs(y,z));
val it = false: bool
> val y' = mk_var("y",beta);
val y' = “y”: term
> aconv f (mk_abs(y',z));
val it = true: bool
```

To see why the first version is false, recall the type of
`y`

declared above.

```
> dest_var y;
val it = ("y", “:α”): string * hol_type
```

A more interesting example follows. The syntax `λx y. b`

is shorthand for `λx. (λy. b)`

.

```
> val f1 = ``λx y. ¬x``;
<<HOL message: inventing new type variable names: 'a>>
val f1 = “λx y. ¬x”: term
> val f2 = ``λy x. ¬x``;
<<HOL message: inventing new type variable names: 'a>>
val f2 = “λy x. ¬x”: term
> val f3 = ``λy x. ¬y``;
<<HOL message: inventing new type variable names: 'a>>
val f3 = “λy x. ¬y”: term
> aconv f1 f2;
val it = false: bool
> aconv f1 f3;
val it = true: bool
```

In `f1`

, the type of `y`

is invented, but the
type of `x`

is fixed (as `:bool`

) by *type
inference*. The Boolean negation operator (`¬`

) takes a
Boolean argument, so HOL infers that its argument must have type
`:bool`

.

A combination represents application of a function to an argument.

```
> mk_comb(f,y');
val it = “(λx. 0) y”: term
```

The syntax is simply juxtaposition of function with argument.

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

The type of the argument must match the domain of the function’s type.

```
> mk_comb(f,y);
Exception- HOL_ERR
{message = "incompatible types", origin_function = "mk_comb",
origin_structure = "Term"} raised
```

To understand why this fails, recall that `f`

requires an
argument of type `β`

, but `y`

has type
`α`

.

```
> val (v,b) = dest_abs f;
val b = “0”: term
val v = “x”: term
> dest_var v;
val it = ("x", “:β”): string * hol_type
```

When ``f y`

` was given to the term parser, it invented new
types to ensure the application was type-correct. In fact, the HOL
variables in that quotation are unrelated to the ML variables
`f`

and `y`

.

Every function in HOL takes one argument, but multiple arguments can
be implemented using higher-order functions by *currying*.

```
> val fxyz = ``f x y z``;
<<HOL message: inventing new type variable names: 'a, 'b, 'c, 'd>>
val fxyz = “f x y z”: term
> dest_comb fxyz;
val it = (“f x y”, “z”): term * term
```

All the arguments can be stripped off at once.

```
> strip_comb fxyz;
val it = (“f”, [“x”, “y”, “z”]): term * term list
```

The counterpart for creating multiple applications at once is
`list_mk_comb`

.

```
> val tm = list_mk_comb (f3,[``x:bool``,y]);
val tm = “(λy x. ¬y) x y”: term
```

There is shorthand for extracting either of the results of
`dest_comb`

:

```
> rator tm;
val it = “(λy x. ¬y) x”: term
> rand tm;
val it = “y”: term
```

These functions stand for “operator” and “operand” respectively.

Trying to destruct a variable as an abstraction, or other such mismatches, will raise exceptions.

```
> dest_abs ``f``;
Exception- <<HOL message: inventing new type variable names: 'a>>
HOL_ERR
{message = "not a lambda abstraction", origin_function = "dest_abs",
origin_structure = "Term"} raised
```

However, an arbitrary term can be destructed using
`dest_term`

.

```
> dest_term ``f``;
<<HOL message: inventing new type variable names: 'a>>
val it = VAR ("f", Tyv "'a"): lambda
> dest_term ``λx. x``;
<<HOL message: inventing new type variable names: 'a>>
val it = LAMB (Fv ("x", Tyv "'a"), Fv ("x", Tyv "'a")): lambda
```

The other `lambda`

constructors are `CONST`

and
`COMB`

.

There are two canonical values of type `:bool`

, namely
true and false. In HOL they are written as `T`

and
`F`

, and are also bound by default to ML variables.

```
> T;
val it = “T”: term
> Term.compare (``F``, F);
val it = EQUAL: order
> type_of F;
val it = “:bool”: hol_type
```

The ML function `type_of`

, used above, returns the HOL
type of a term.

```
> type_of;
val it = fn: term -> hol_type
```

The connectives of Boolean logic can be written using either ASCII or Unicode syntax. Here are examples using both styles.

```
> ``~p``;
val it = “¬p”: term
> ``p /\ q``;
val it = “p ∧ q”: term
> ``p ∨ q``;
val it = “p ∨ q”: term
> ``x ==> y``;
val it = “x ⇒ y”: term
> ``x ⇔ y``;
val it = “x ⇔ y”: term
```

In HOL, unlike in propositional logic, these connectives have no special syntactic status: they are simply higher-order functions.

```
> val imp = ``x ⇒ y``;
val imp = “x ⇒ y”: term
> rator imp;
val it = “$==> x”: term
> type_of it;
val it = “:bool -> bool”: hol_type
> type_of``$~``;
val it = “:bool -> bool”: hol_type
```

As you can see, when writing partial applications of the connectives, their ASCII names must be used. Furthermore leading dollar signs must be used, since the default grammar used by the term parser has rules for these connectives expecting them to be fully applied. Another way to escape the special parsing of infix (and other special) tokens is to use parentheses:

```
> rand ``P (~)``;
<<HOL message: inventing new type variable names: 'a>>
val it = “$¬”: term
```

HOL comes with a small selection of pre-defined ML functions that are generally useful (and not specific to theorem proving).

The `#1`

and `#2`

functions are record
selectors for elements of tuples in ML. In HOL they are also defined as
`fst`

and `snd`

.

```
> fst (0,1);
val it = 0: int
> #2 (0,1,2)
val it = 1: int
```

The `el`

function extracts elements from a list. It is the
same as `List.nth`

in ML, but indexes from `1`

rather than `0`

.

```
> el 2 [1,2,3];
val it = 2: int
```

The `|>`

combinator does function application. Thus,
`tm2 |> dest_comb`

is the same as
`dest_comb tm2`

. Its utility is in adding readabilty (and
avoiding parentheses) when applying many functions in a row.

```
> ("hi",1,"bye") |> #3 |> String.explode |> el 2;
val it = #"y": char
```

In HOL, there is a global table of configuration options called
*traces*, which affect the interactive system in various ways.
The list of traces can be found by calling the `traces`

function:

`> traces(); (* output elided *)`

Each trace has a name (a string) and a value (an integer). Usually
`0`

means off, and `1`

means on. For traces with
more values, higher numbers usually mean more of the behaviour.

Traces can be set with `set_trace`

.

If you are using Vim, the Vim plugin (see Interaction) documentation explains how to type Unicode characters using digraphs. HOL prints output back using Unicode, but you can turn this off if desired.

```
> set_trace "Unicode" 0;
val it = (): unit
> val tm1 = ``x <=> y``;
val tm1 = ``x <=> y``: term
> val tm2 = ``x ⇔ y``;
val tm2 = ``x <=> y``: term
> set_trace "Unicode" 1;
val it = (): unit
> tm1;
val it = “x ⇔ y”: term
```

Observe that `tm2`

actually contains a variable called
`⇔`

, which is printed with a leading `$`

when
Unicode is turned on to avoid conflicting with the bi-implication
constant (`<=>`

).

```
> tm2;
val it = “x ⇔ y”: term
> dest_comb tm2;
val it = (“$<=> x”, “y”): term * term
> tm2 |> dest_comb |> #1 |> dest_comb;
val it = (“$<=>”, “x”): term * term
> is_var (#2 it);
val it = true: bool
```

One important constant in HOL is the equality function, which makes
equations. Recall `f1`

and `f3`

from the section
on Abstractions. We can make an equation
between them:

```
> val eqn = mk_eq(f1,f3);
val eqn = “(λx y. ¬x) = (λy x. ¬y)”: term
> lhs eqn;
val it = “λx y. ¬x”: term
> rhs eqn;
val it = “λy x. ¬y”: term
> dest_eq eqn;
val it = (“λx y. ¬x”, “λy x. ¬y”): term * term
```

In fact, we have already seen an instance of equality in the section on Boolean connectives. On Booleans, equality is the same as bi-implication.

```
> val iff = mk_eq(``p:bool``,``q:bool``);
val iff = “p ⇔ q”: term
```

However, equality can be applied at any type. In the first equation above, we find that equality is comparing higher-order functions.

```
> rator eqn;
val it = “$= (λx y. ¬x)”: term
> rator it;
val it = “$=”: term
> eqn |> rator |> rator |> type_of;
val it = “:(bool -> α -> bool) -> (bool -> α -> bool) -> bool”: hol_type
```

Whereas in the second equation:

```
> iff |> rator |> rator |> type_of;
val it = “:bool -> bool -> bool”: hol_type
```

In general, we have the following *polymorphic* type for
equality.

```
> type_of``$=``;
<<HOL message: inventing new type variable names: 'a>>
val it = “:α -> α -> bool”: hol_type
```

Many constants are polymorphic. A polymorphic constant has a most
general type that includes type variables. Those variables can be
*instantiated* to form a type instance of the constant.

One example is the `MAP`

constant on lists.

```
> type_of``MAP``;
<<HOL message: inventing new type variable names: 'a, 'b>>
val it = “:(α -> β) -> α list -> β list”: hol_type
> val tm = ``MAP f [T;T;F]``;
<<HOL message: inventing new type variable names: 'a>>
val tm = “MAP f [T; T; F]”: term
> strip_comb tm |> #1;
val it = “MAP”: term
> type_of it;
val it = “:(bool -> α) -> bool list -> α list”: hol_type
```

The instance of `MAP`

obtained from `tm`

is
more specialised because it was applied to a list of Booleans.

To find the most general type of a constant, one can parse the
constant and HOL will invent type variables where it can. A more
principled method is to use `prim_mk_const`

, which makes a
constant without taking a type as an argument (and instead returns the
instance of the constant with most general type), but this requires the
full name of the constant (as described later under Theories).

Any term can be instantiated with a type substitution, which maps type variables to types. In the following examples, let us pretty-print terms with types on.

```
> set_trace "types" 1;
val it = (): unit
> val tm = ``MAP f``;
<<HOL message: inventing new type variable names: 'a, 'b>>
val tm = “MAP (f :α -> β)”: term
> inst [alpha |-> bool] tm;
val it = “MAP (f :bool -> β)”: term
> inst [alpha |-> bool, beta |-> alpha] tm;
val it = “MAP (f :bool -> α)”: term
```

The `inst`

function performs a simultaneous substitution
of types for type variables. The `|->`

operator constructs
a binding, and a substitution is just a list of these bindings.

```
> set_trace "types" 0;
val it = (): unit
```

The `subst`

function performs simultaneous substitution of
terms for term variables. Term substitutions are created using the same
`|->`

operator as used for type substitutions. For an
example, recall the term we made earlier, `imp`

, which
contains two free variables.

```
> imp;
val it = “x ⇒ y”: term
> val s = [``x:bool`` |-> F, ``y:bool`` |-> ``x = y``];
<<HOL message: inventing new type variable names: 'a>>
val s = [{redex = “x”, residue = “F”}, {redex = “y”, residue = “x = y”}]:
{redex: term, residue: term} list
> subst s imp;
val it = “F ⇒ x = y”: term
```

Substitution only works on free variables. Recall `tm3`

,
which has none.

```
> f3;
val it = “λy x. ¬y”: term
```

The same substitution does nothing.

```
> subst s f3;
val it = “λy x. ¬y”: term
```

However, if we add a free occurrence of `y`

, it will be
substituted.

```
> val f3y = mk_comb(f3,``y:bool``);
val f3y = “(λy x. ¬y) y”: term
> subst s f3y;
val it = “(λy x. ¬y) (x = y)”: term
```

What happens if we do the same in the body of the abstraction?

```
> val (_,f3b) = dest_abs f3;
val f3b = “λx. ¬y”: term
> subst s f3b;
val it = “λx'. x ≠ y”: term
```

Now the bound `x`

got renamed to `x'`

, since a
different `x`

appears in the body after the substitution. (In
fact, these variables don’t even have the same type.)

To the Boolean connectives of propositional logic, first-order logic adds quantifiers. In particular, there is a universal and an existential quantifier. Here are some examples.

```
> val q = ``q:bool``;
val q = “q”: term
> mk_forall(q,``^q ==> ^q``);
val it = “∀q. q ⇒ q”: term
> ``!y. ~y ==> x``;
val it = “∀y. ¬y ⇒ x”: term
> ``?y. x ==> ~y``;
val it = “∃y. x ⇒ ¬y”: term
```

Using the term-building functions directly, one must be careful to ensure all variables have the desired types.

```
> mk_exists(``q``,``q ==> q``);
<<HOL message: inventing new type variable names: 'a>>
val it = “∃q'. q ⇒ q”: term
```

Here, the quanified variable, `q'`

, is not the same as the
variable `q`

in the body of the existential. It has a
different type, namely `:'a`

, whereas `q`

must
have type `bool`

. This happened because the bound
`q'`

was parsed in a separate context from that constraining
the type of `q`

to be `:bool`

.

There is shorthand syntax for nesting the same quantifier multiple times, which HOL will print back by default.

```
> ``!x. !y. !z. x = y``;
<<HOL message: inventing new type variable names: 'a, 'b>>
val it = “∀x y z. x = y”: term
```

The corresponding term-manipulation functions are illustrated below.

```
> strip_forall it;
val it = ([“x”, “y”, “z”], “x = y”): term list * term
> list_mk_exists([x,q],q);
val it = “∃x q. q”: term
```

In HOL, the quantifiers are in fact simply higher-order functions.

```
> val tm = ``∀x. ∃y. x = y``;
<<HOL message: inventing new type variable names: 'a>>
val tm = “∀x. ∃y. x = y”: term
> val (x,ex) = dest_forall tm;
val ex = “∃y. x = y”: term
val x = “x”: term
> dest_comb it;
val it = (“$?”, “λx. ∃q. q”): term * term
```

`dest_forall`

splits the quantifier into the bound
variable and the body, but `dest_comb`

, used on the second
quantifier, reveals that `ex`

is an application of
`$?`

to a lambda term.

```
> type_of ``$!``;
<<HOL message: inventing new type variable names: 'a>>
val it = “:(α -> bool) -> bool”: hol_type
```

A predicate is a function with codomain `:bool`

.
Quantifiers are predicates on predicates.

The third (and final) datatype HOL provides on top of ML, after types
and terms, is `thm`

, the type of proven theorems. A very
simple theorem is bound by default to the ML variable
`TRUTH`

.

```
> TRUTH;
val it = ⊢ T: thm
```

Every theorem contains a set of hypotheses and a conclusion. All
these are terms of type `:bool`

.

```
> dest_thm TRUTH;
val it = ([], “T”): term list * term
> hypset TRUTH;
val it = HOLset{}: term set
> concl TRUTH;
val it = “T”: term
```

`hyp`

, like `dest_thm`

, returns the hypotheses
as a list, which is often less efficient when writing automation, but
easier to deal with interactively.

```
> hyp TRUTH;
val it = []: term list
```

Hypotheses are not printed by default, but there is a trace to show them.

```
> set_trace "assumptions" 1;
val it = (): unit
> TRUTH;
val it = [] ⊢ T: thm
```

A key feature of HOL (and all LCF-style
theorem provers) is that values of type `thm`

can only be
produced by a small number of trusted functions in a trusted module. In
HOL, the relevant structure is `Thm`

, and the functions it
exports are available by default. (See Finding documentation for how to
inspect the contents of such structures.) Any other theorem-producing
functions must ultimately build their theorems via calls to the trusted
functions, thereby ensuring that a proof (in the form of a sequence of
calls to kernel functions) exists for every theorem. There are many
theorem-producing functions (sometimes called “derived rules”) that
build on the ones in `Thm`

.

A simple kernel function is `ASSUME`

, which creates a
theorem with an assumption.

```
> val th = ASSUME ``x ≠ y``;
<<HOL message: inventing new type variable names: 'a>>
val th = [x ≠ y] ⊢ x ≠ y: thm
```

The `DISCH`

rule can move an assumption into the
conclusion.

```
> DISCH ``x ≠ y`` th;
<<HOL message: inventing new type variable names: 'a>>
val it = [] ⊢ x ≠ y ⇒ x ≠ y: thm
```

It does not have to be in the assumptions in the first place.

```
> DISCH ``y ≠ x`` th;
<<HOL message: inventing new type variable names: 'a>>
val it = [x ≠ y] ⊢ y ≠ x ⇒ x ≠ y: thm
```

To pull the antecedent of an implication into the assumptions, use
`UNDISCH`

.

```
> UNDISCH it;
val it = [x ≠ y, y ≠ x] ⊢ x ≠ y: thm
```

To discharge all assumptions, use `DISCH_ALL`

.

```
> DISCH_ALL it;
val it = [] ⊢ y ≠ x ⇒ x ≠ y ⇒ x ≠ y: thm
```

This is useful to avoid having to write which assumption you want in theorems with only one anyway.

In the HOL theorem prover, type operators, constants, and stored
theorems are organised into *theories*. Every type operator (such
as `list`

) is defined in some theory; in the case of
`list`

, it is `listTheory`

. The fully-qualified
name of the type operator is `list$list`

.

By convention, a theory `foo`

is stored in an ML structure
called `fooTheory`

which is produced by building
`fooScript.sml`

.

To find the fully-qualified name of a type operator or constant, the following functions can be used.

```
> dest_thy_type ``:'a list``;
val it = {Args = [“:α”], Thy = "list", Tyop = "list"}:
{Args: hol_type list, Thy: string, Tyop: string}
```

(Since `dest_thy_type`

takes a type, a type operator must
be applied to arguments first. These are also returned, as with
`dest_type`

.)

```
> dest_thy_const T;
val it = {Name = "T", Thy = "bool", Ty = “:bool”}:
{Name: string, Thy: string, Ty: hol_type}
> dest_thy_type ``:num``;
val it = {Args = [], Thy = "num", Tyop = "num"}:
{Args: hol_type list, Thy: string, Tyop: string}
```

Every interactive session has a “current theory”, which is where any new logical content (constants, theorems/axioms) will be stored. By default, this will be “scratch”.

```
> current_theory();
val it = "scratch": string
```

To start working in a new theory, use `new_theory`

.

```
> new_theory "test";
Exporting theory "scratch" ... done.
Theory "scratch" took 0.00018s to build
<<HOL message: Created theory "test">>
val it = (): unit
> current_theory();
val it = "test": string
```

Only one theory can be current at a time, so the call to
`new_theory`

first exported the theory “scratch”. Generally,
`new_theory`

should not be used interactively except when
editing a script file: then, it should
appear near the start of the file to avoid adding any content to a
`scratchTheory`

. To save the current theory to disk, use
`export_theory`

; this should generally only happen at the
bottom of a script file.

Every theory has a series of *ancestors*, which can be found
(in a meaningless order) as follows.

```
> ancestry "-";
val it =
["ConseqConv", "quantHeuristics", "patternMatches", "ind_type", "divides",
"while", "one", "sum", "option", "pair", "combin", "sat", "normalForms",
"relation", "min", "bool", "marker", "num", "prim_rec", "arithmetic",
"numeral", "basicSize", "numpair", "pred_set", "list", "rich_list",
"indexedLists", "scratch"]: string list
```

The argument to `ancestry`

is the name of a theory, with
“-” being interpreted as the current theory. One of the earliest
theories is `boolTheory`

.

```
> ancestry "bool";
val it = ["min"]: string list
```

The *theory hierarchy* is the tree of theories organised by
ancestry. One theory depends on another (and therefore includes the
other amongst its ancestors) if it makes use of that theory’s types,
constants, or theorems. The root of the hierarchy is
`minTheory`

, which contains some primitive types and
constants.

The contents of a theory can be seen as follows.

```
> types "min";
val it = [("ind", 0), ("fun", 2), ("bool", 0)]: (string * int) list
> constants "min";
val it = [“$@”, “$==>”, “$=”]: term list
> theorems "min";
val it = []: (string * thm) list
> axioms "min";
val it = []: (string * thm) list
```

Names in the theory hierarchy must be unique.

```
> new_theory "bool";
Exception- HOL_ERR
{message = "theory: \"bool\" already exists.", origin_function =
"new_theory", origin_structure = "Theory"} raised
```

The contents of the current theory hierarchy are stored in a database and can be searched. Stored theorems are stored with a name, and can be searched for by name as follows.

```
> DB.find"skolem";
val it =
[(("bool", "SKOLEM_THM"),
( [] ⊢ ∀P. (∀x. ∃y. P x y) ⇔ ∃f. ∀x. P x (f x), Thm)),
(("scratch", "SKOLEM_AGAIN"),
( [] ⊢ ∀P. (∀x. ∃y. P x y) ⇔ ∃f. ∀x. P x (f x), Thm))]: public_data list
> DB.find"Tru";
val it =
[(("ConseqConv", "true_imp"), ( [] ⊢ ∀t. t ⇒ T, Thm)),
(("bool", "RES_FORALL_TRUE"), ( [] ⊢ (∀x::P. T) ⇔ T, Thm)),
(("bool", "TRUTH"), ( [] ⊢ T, Thm))]: public_data list
```

The search is case-insensitive. The output format includes the theory, theorem name, and the theorem itself. Let us turn off the printing of hypotheses for now.

```
> set_trace "assumptions" 0;
val it = (): unit
```

One can also search again within the results.

```
> DB.find_in "add" (DB.find "zero");
val it =
[(("arithmetic", "LESS_ADD_NONZERO"), (⊢ ∀m n. n ≠ 0 ⇒ m < m + n, Thm)),
(("arithmetic", "ZERO_LESS_ADD"),
(⊢ ∀m n. 0 < m + n ⇔ 0 < m ∨ 0 < n, Thm))]:
DB_dtype.public_data_value named list
```

The data are printed more nicely by `print_find`

, which
prints the data list as follows.

```
> val s = Hol_pp.data_list_to_string it; (* output elided *)
> say s;
arithmeticTheory.LESS_ADD_NONZERO (THEOREM)
-------------------------------------------
⊢ ∀m n. n ≠ 0 ⇒ m < m + n
arithmeticTheory.ZERO_LESS_ADD (THEOREM)
----------------------------------------
⊢ ∀m n. 0 < m + n ⇔ 0 < m ∨ 0 < n
val it = (): unit
```

Theorems can also be searched for by matching on their conclusion.

```
> DB.apropos_in ``_ ++ _ = _`` (DB.apropos ``[x]``);
<<HOL message: inventing new type variable names: 'a>>
<<HOL message: inventing new type variable names: 'a>>
val it =
[(("list", "APPEND_EQ_APPEND_MID"),
(⊢ l1 ⧺ [e] ⧺ l2 = m1 ⧺ m2 ⇔
(∃l. m1 = l1 ⧺ [e] ⧺ l ∧ l2 = l ⧺ m2) ∨
∃l. l1 = m1 ⧺ l ∧ m2 = l ⧺ [e] ⧺ l2, Thm)),
(("list", "APPEND_EQ_SING"),
(⊢ l1 ⧺ l2 = [e] ⇔ l1 = [e] ∧ l2 = [] ∨ l1 = [] ∧ l2 = [e], Thm)),
(("list", "APPEND_FRONT_LAST"),
(⊢ ∀l. l ≠ [] ⇒ FRONT l ⧺ [LAST l] = l, Thm)),
(("list", "MEM_APPEND_lemma"),
(⊢ ∀a b c d x.
a ⧺ [x] ⧺ b = c ⧺ [x] ⧺ d ∧ ¬MEM x b ∧ ¬MEM x a ⇒ a = c ∧ b = d,
Thm)),
(("list", "UNIQUE_DEF"),
(⊢ ∀e L. UNIQUE e L ⇔ ∃L1 L2. L1 ⧺ [e] ⧺ L2 = L ∧ ¬MEM e L1 ∧ ¬MEM e L2,
Def))]: public_data list
```

Underscores are treated specially by the parser; in particular, each underscore is parsed as a variable with a distinct name from the other underscores. Matching allows substitution of any variable by any term (of the correct type), so the treatment of underscores enables their convenient use as wildcards in terms to be matched.

Theorems also contain a set of tags indicating how they were produced. These tags propagate through uses in inference applications (e.g. if a theorem has a tag, then a theorem derived from the former will inherit this tag). These tags are especially useful with axioms in case there is a suspicion the axiom may be unsound (e.g. the axiom is taken for correct while not proven, or the axiom comes from an “oracle”, or the axiom comes from an external prover but without a proof that can be replayed by HOL).

HOL contains in-built documentation available from the REPL via the
`help`

function. The same documentation is also available in
HTML format both from `$HOLDIR/help/HOLindex.html`

and online.

In some cases, some libraries have not yet provided help documentation, but there is still information available in comments in their signature files. TODO: Also, how to set up Poly/ML to show the signatures of structures.

Finally, the HOL
website has information regarding HOL’s manuals, which can also be
found under `$HOLDIR/Manual`

in your local installation.

TODO: When HOL is built, links to all the theories and libraries are
created under `$HOLDIR/sigobj`

. This can be a useful resource
for finding out where the sources corresponding to a particular
structure are kept.

To parse a fully-qualified name, use a `$`

symbol.

```
> ``bool$T``;
val it = “T”: term
```

This is useful when the bare constant name (i.e., `T`

in
this case) is overloaded and might refer to more than one constant. The
constant `0`

often falls into this category, since it is
overloaded at different numeric types.

```
> dest_thy_const ``0``;
val it = {Name = "0", Thy = "num", Ty = “:num”}:
{Name: string, Thy: string, Ty: hol_type}
```

We summarise the additions of new surface syntax that entered in recent versions of HOL4, which reduces code-smells and is closer to syntax of other theorem provers.

We have implemented new syntaxes for `store_thm`

and
`save_thm`

, which better satisfy the recommendation that
`name1`

and `name2`

below should be the same:

`val name1 = store_thm("name2", tm, tac);`

Now we can remove the “code smell” by writing

```
Theorem name: term-syntax
Proof tac
QED
```

which might look like

```
Theorem name:
∀x. P x ⇒ Q x
Proof
rpt strip_tac >> ...
QED
```

This latter form must have the `Proof`

and
`QED`

keywords in column 0 in order for the lexing machinery
to detect the end of the term and tactic respectively. Both forms map to
applications of `Q.store_thm`

underneath, with an ML binding
also made to the appropriate name. Both forms allow for theorem
attributes to be associated with the name, so that one can write

```
Theorem ADD0[simp]: ∀x. x + 0 = x
Proof tactic
QED
```

Finally, to replace

`val nm = save_thm(“nm”, thm_expr);`

one can now write

`Theorem nm = thm_expr`

These names can also be given attributes in the same way.

There is also a new `local`

attribute available for use
with `store_thm`

, `save_thm`

and the
`Theorem`

syntax above. This attribute causes a theorem to
not be exported when `export_theory`

is called, making it
local-only. Use of `Theorem`

-`local`

is thus an
alternative to using `prove`

or `Q.prove`

. In
addition, the `Theorem`

-`local`

combination can be
abbreviated with `Triviality`

; one can write
`Triviality foo[...]`

instead of
`Theorem foo[local,...]`

.

Relatedly, there is a similar syntax for making definitions. The idiom is to write

```
Definition name[attrs]:
def
End
```

Or

```
Definition name[attrs]:
def
Termination
tactic
End
```

The latter form maps to a call to `tDefine`

; the former to
`xDefine`

. In both cases, the `name`

is taken to
be the name of the theorem stored to disk (it does *not* have a
suffix such as `_def`

appended to it), and is also the name
of the local SML binding. The attributes given by `attrs`

can
be any standard attribute (such as `simp`

), and/or drawn from
`Definition`

-specific options:

- the attribute
`schematic`

alllows the definition to be schematic; - the attribute
`nocompute`

stops the definition from being added to the global compset used by`EVAL`

- the attribute
`induction=iname`

makes the induction theorem that is automatically derived for definitions with interesting termination be called`iname`

. If this is omitted, the name chosen will be derived from the`name`

of the definition: if`name`

ends with`_def`

or`_DEF`

, the induction name will replace this suffix with`_ind`

or`_IND`

respectively; otherwise the induction name will simply be`name`

with`_ind`

appended.

Whether or not the `induction=`

attribute is used, the
induction theorem is also made available as an SML binding under the
appropriate name. This means that one does not need to follow one’s
definition with a call to something like `DB.fetch`

or
`theorem`

just to make the induction theorem available at the
SML level.

Similarly, there are analogous `Inductive`

and
`CoInductive`

syntaxes for defining inductive and coinductive
relations (using `Hol_reln`

and `Hol_coreln`

underneath). The syntax is

```
Inductive stem:
quoted term material
End
```

or

```
CoInductive stem:
quoted term material
End
```

where, as above, the `Inductive`

, `CoInductive`

and `End`

keywords must be in the leftmost column of the
script file. The `stem`

part of the syntax drives the
selection of the various theorem names (*e.g.*,
`stem_rules`

, `stem_ind`

, `stem_cases`

and `stem_strongind`

for inductive definitions) for both the
SML environment and the exported theory. The actual names of new
constants in the quoted term material do not affect these bindings.

Each (co)inductive rule can be exported under a theorem name provided
in square-bracket syntax `[~name:]`

, where `~`

is
a place-holder for the relation. For example

```
Inductive RTC:
[~refl:]
(!x. RTC R x x) /\
[~induct:]
!x y z. R x y /\ RTC R y z ==> RTC R x z
End
```

additionally exports the theorems `RTC_refl`

and
`RTC_induct`

.

There are new syntaxes for `Datatype`

and
type-abbreviation. Users can replace `val _ = Datatype`...``

with

```
Datatype: ...
End
```

and `val _ = type_abbrev("name", ty)`

with

`Type name = ty`

if the abbreviation should introduce pretty-printing (which would be
done with `type_abbrev_pp`

), the syntax is

`Type name[pp] = ty`

Note that in both `Type`

forms the `ty`

is a
correct ML value, and may thus require quoting. For example, the
`set`

abbreviation is established with

`Type set = “:α -> bool”`

The special `Type`

syntax for making type abbreviations
can now map to `temp_type_abbrev`

(or
`temp_type_abbrev_pp`

) by adding the `local`

attribute to the name of the abbreviation.

For example

`Type foo[local] = “:num -> bool # num”`

or

`Type foo[local,pp] = “:num -> bool # num”`

We have added a special syntactic form `Overload`

to
replace various flavours of `overload_on`

calls. The core
syntax is exemplified by

`Overload foo = “myterm”`

Attributes can be added after the name. Possible attributes are
`local`

(for overloads that won’t be exported) and
`inferior`

to cause a call `inferior_overload_on`

(which makes the overload the pretty-printer’s last choice).