## Introduction

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.

## Installation

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.

## Running hol

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``````

## Script files

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.

## Interaction

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.

## Types

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``````

## Parsing

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``````

## Terms

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.

### Variables

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.

``````> y = ``y:'b``;
val it = false: bool

> y = mk_var("y",alpha);
val it = true: bool``````

### Constants

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}``````

### Abstractions

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`.

Alpha-equivalence is less discriminating than equality.

``````> f1 = f3;
val it = false: bool``````

### Combinations

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.

## The lambda view

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", ``:α``): lambda

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

The other `lambda` constructors are `CONST` and `COMB`.

## Boolean connectives

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

> ``F`` = F;
val it = true: bool

> 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``````

## Some library functions

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 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``````

## Traces

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`.

## Unicode

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``;
<<HOL message: inventing new type variable names: 'a, 'b, 'c>>
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``````

## Equality

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``````

## Polymorphism

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``````

## Substitution

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.)

## First-order logic

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.

## Theorems

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 = ?: 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.

## Theories

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.00000s 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", "ind_type", "operator", "while", "pair",
"num", "relation", "prim_rec", "arithmetic", "numeral", "normalForms",
"one", "marker", "combin", "min", "bool", "sat", "sum", "option",
"basicSize", "numpair", "pred_set", "list", "rich_list", "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``````

## Finding theorems

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))]:
DB.data list

> DB.find"Tru";
val it =
[(("bool", "RES_FORALL_TRUE"), ( [] |- (∀x::P. T) ⇔ T, Thm)),
(("bool", "TRUTH"), ( [] |- T, Thm)),
(("ConseqConv", "true_imp"), ( [] |- ∀t. t ⇒ T, Thm))]: DB.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 =
(|- ∀m n. n ≠ 0 ⇒ m < m + n, Thm)),
(|- ∀m n. 0 < m + n ⇔ 0 < m ∨ 0 < n, Thm))]: DB.data list``````

The data are printed more nicely by `print_find`, which prints the data list as follows.

``````> val s = DB.data_list_to_string it; (* output elided *)
> say s;

-------------------------------------------
|- ∀m n. n ≠ 0 ⇒ m < m + n

----------------------------------------
|- ∀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))]: DB.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.

## Tags

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).

## Finding documentation

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.

## System conventions

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.

## Defining constants

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}``````