HOL Light Tutorial

September 26, 2026 Abstract The HOL Light theorem prover can be difficult to get started with. While the manual is fairly detailed and comprehensive, the large amount of background information that has to be absorbed before the user can do anything interesting is intimidating. Here we give an alternative ‘quick start’ guide, aimed at teaching basic use of the system quickly by means of a graded set of examples. Some readers may find it easier to absorb; those who do not are referred after all to the standard manual. Contents 1 Installation 1.1 For Windows Users: WSL and Cygwin 1.2 OCaml 1.3 HOL Light 1.3.1 Installing HOL Light from a package manager 1.3.2 Installing HOL Light from its source code 1.4 Editor 1.5 Other versions of HOL 2 OCaml toplevel basics 2.1 Compiling a HOL Light Proof 3 HOL basics 3.1 Terms 3.2 Types 3.3 Theorems 3.4 Derived rules 4 Propositional logic 4.1 Proving tautologies 4.2 Low-level logical rules 4.3 Logic design and verification 5 Equations and functions 5.1 Curried functions 5.2 Pairing 5.3 Equational reasoning 5.4 Definitions 6 Abstractions and quantifiers 6.1 Quantifiers 6.2 First-order reasoning 7 Conversions and rewriting 7.1 Conversionals 7.2 Depth conversions 7.3 Matching 7.4 Rewriting 7.5 Searching for theorems 8 Tactics and tacticals 8.1 The goalstack 8.2 Inductive proofs about summations 9 HOL’s number systems 9.1 Arithmetical decision procedures 9.2 Nonlinear reasoning 9.3 Quantifier elimination 10 Inductive definitions 10.1 The bug puzzle 10.2 Verification of concurrent programs 11 Wellfounded induction 11.1 Irrationality of 2 11.2 Wellfoundedness 12 Changing proof style 12.1 Towards more readable proofs 12.2 Example 12.3 The right style? 13 Recursive definitions 13.1 Binomial coefficients 13.2 The binomial theorem 14 Sets and functions 14.1 Choice and the select operator 14.2 Function calculus 14.3 Some cardinal arithmetic 15 Inductive datatypes 15.1 Enumerated types 15.2 Recursive types 15.3 The Fano plane 15.4 Record types 16 Semantics of programming languages 16.1 Semantics of the language 16.2 Determinism 16.3 Weakest preconditions 16.4 Axiomatic semantics 17 Shallow embedding 17.1 State and expressions 17.2 Commands 17.3 Hoare rules 17.4 Verification conditions 17.5 Refinement 18 Number theory 18.1 Congruences 18.2 Fermat’s Little Theorem 18.3 RSA encryption 19 Real analysis 19.1 Chebyshev polynomials 19.2 A trivial part of Sarkovskii’s theorem 19.3 Derivatives 20 Embedding of logics 20.1 Modal logic 20.2 Deep embedding 20.3 Modal schemas 20.4 Shallow embedding 21 HOL as a functional programming language 21.1 Normalizing if-then-else expressions 21.2 Proving properties 21.3 A theorem prover 21.4 Execution 22 Vectors 22.1 3-dimensional vectors 22.2 Cross products 23 Custom tactics 23.1 The Kochen-Specker paradox 23.2 Formalization in HOL 24 Defining new types 24.1 Nonzero 3-vectors 24.2 The projective plane again 24.3 Quotient types 25 Custom inference rules 25.1 Ordered rewriting using the LPO 25.2 Critical pairs 25.3 Examples of completion 26 Linking external tools 26.1 Maxima 26.2 Interfacing HOL and Maxima 26.3 Factoring 26.4 Antiderivatives and integrals A The evolution of HOL Light A.1 LCF A.2 HOL A.3 Development and applications A.4 hol90, ProofPower and HOL Light 1 Installation HOL Light can fairly easily be made to work on most modern computers. Since the first version (Harrison 1996a), the build process has been simplified considerably. In what follows, we will sometimes assume a Unix-like environment such as Linux. If the reader has access to a Linux machine and feels comfortable with it, its use is recommended. However, users of Windows need not despair, because all the Unix tools needed, and many more useful ones besides, are freely available as part of Cygwin. From Windows 10, you can also install Windows Subsystem for Linux (WSL) and choose a Linux distribution you prefer. Non-Windows users, or Windows users determined to work “natively”, can skip the next subsection. 1.1 For Windows Users: WSL and Cygwin If you are using Windows 10 or above, you can install Windows Subsystem for Linux which is an official feature of Microsoft Windows. Its installation instruction is available on https://learn.microsoft.com/en-us/windows/wsl/install. After its installation, you can choose which Linux distribution to add to your WSL, from Microsoft Store. If WSL is not supported on your Windows, you can try Cygwin. Cygwin is a Linux-like environment that can be run within Windows, without interfering with normal Windows usage. Among other things, it provides a traditional shell from which the usual Unix/Linux software tools are available. Cygwin can be freely downloaded from http://www.cygwin.com/. It is a large system, particularly if you select all the package installation options, so the download and installation can take some time. However it usually seems to be straightforward and unproblematic. After installing Cygwin, simply start a ’Bash shell’. On my Windows machine, for example, I follow the menu sequence Start →All Programs→ Cygwin→ Cygwin bash shell. This application is a ‘shell’ (Unix jargon for something analogous to a Windows command prompt) from which the later commands below can be invoked as if you were within Linux. We will hereinafter say ‘Linux’ when we mean Linux, some other version of Unix, or Cygwin inside Windows. 1.2 OCaml HOL Light is built on top of the functional programming language Objective CAML (‘OCaml’). To be more precise, HOL Light is written in OCaml and the OCaml read-eval-print loop is the usual means of interacting with HOL Light. So installing OCaml is a prerequisite for using HOL Light. Besides, it is a powerful modern programming language with much to recommend it for a wide range of other applications. OCaml can be installed on a wide range of architectures by following the instructions on the Web site http://caml.inria.fr/ocaml/english.en.html. I normally rebuild the system from sources, even under Cygwin (it only requires a few short commands) but precompiled binaries are available for many platforms. 1.3 HOL Light Finally we are ready to install HOL Light itself. HOL Light can be either installed using a package manager or by building it from its source code. Installing HOL Light using a package manager is easier, but you might get a bit out-of-date version. Building it from the source code is harder, but you are guaranteed to get its latest features. 1.3.1 Installing HOL Light from a package manager HOL Light is available at OPAM, an OCaml package manager. If you have OPAM installed on your computer (Its instruction can be found from https://opam.ocaml.org/doc/Install.html), you can install HOL Light by doing the following: opam install hol_light If you use a debian-based Linux distribution, then you can get HOL Light together with useful auxiliary tools by installing the hol-light package. sudo apt-get install hol-light However, if you are using Ubuntu, the HOL Light system you retrieved from apt-get will be outdated for this tutorial. Please consider using OPAM to install HOL Light in this case. 1.3.2 Installing HOL Light from its source code You can download the system by cloning the HOL Light Github repository https://github.com/jrh13/hol-light/. Cloning the Github repository can be done by doing the following in the current directory of the shell: git clone https://github.com/jrh13/hol-light.git Or, if you don’t have git available, you can download the archive file https://github.com/jrh13/hol-light/archive/refs/heads/master.zip. The web browser will download it to hol-light-master.zip. Unzip it to hol-light using the unzip command: unzip hol-light-master.zip -d hol-light Either at the shell prompt (Linux) or the command prompt, move into the appropriate directory by: cd hol-light The first step is to install OCaml libraries the HOL Light system uses. Each library can be either installed using a package manager or manually built from source codes. Instructions for building OCaml libraries from their source codes is not explained in this tutorial because it is likely that the libraries will have better instructions. For package managers, you can either choose a package manager natively supported by your operating system (homebrew for macOS, apt for Ubuntu), or OPAM, an official OCaml package manager that supports identical user interface for multiple operating systems. Which package manager should we use? There are pros and cons. For OPAM, you will need an extra step in advance to install it. However, after its setup, you can quickly install necessary packages using a Makefile command HOL Light provides. In the case of native package managers, HOL Light does not provide such convenience yet. However, you can still install the libraries by finding the package names corresponding to those of your package manager. The list of OCaml packages are described in the (_opam) file. HOL Light must be functional regardless of which package manager you choose. If you have OPAM available on your machine, simply run one of the two following commands depending on your preference of OCaml version: make switch # This will create a local setup for OCaml 4 make switch-5 # This will create a local setup for OCaml 5 This will create a local OPAM environment inside the hol-light directory and install packages in it. Then, activate the local environment setup on the terminal as the following: eval $(opam env) The next step is to create a special file used by HOL Light to handle parsing and printing within OCaml. In Linux you can just do: make Now start up an interactive OCaml session by: ./hol.sh You should now see a large amount of output as HOL Light is loaded, which in particular involves proving many theorems and giving them names. After about two minutes, depending on how fast your computer is, you should see something like the last few lines of output below and the OCaml prompt: 0..0..0..solved at 3 * HOL-Light syntax in effect *