HOL Guidebook

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.

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

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

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.

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", 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.

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

> 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

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

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

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)),
    (("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.

Evaluation

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

Simple proofs

Useful tactics

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.

Standard theories

Defining constants

Overloading

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}

Defining datatypes

Induction

Conversions

The simplifier

Defining relations

The type database

Defining quotients

Changing the parser

Writing more tactics

More proofs

Modern syntax

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.

Theorem

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,...].

Definition

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.

Inductive and CoInductive

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.

Datatype

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”

Overload

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