These lectures introduce theorem proving using the proof assistant Isabelle. Isabelle supports many logics, but by far the most popular is Higher Order Logic, the focus of these notes. Isabelle comes pre-packaged with its HOL libraries, as well as a proof editor (based on jEdit) and various other tools.

The proof developments shown in these notes are all developed with Isabelle 2024, but Isabelle 2025 (the latest version at time of writing) is largely backwards compatible with it. I have not upgraded due to some proof automation regressions in Isabelle 2025 that do not affect the content of these notes.

An Isabelle file is called a theory, and they consist of mathematical definitions (of types and terms), lemmas and proofs. Isabelle theories start with a theory name and a declaration of all the theories on which it depends. The theory name must match the file name, so the code from this lecture should be saved into a file called HOLFromScratch.thy.

We imported the theory Pure, which contains only the very basic built-in structures that define Isabelle's logic.

Isabelle's logical framework consists of terms (t), types (\tau ) and formulae (\varphi ). Each term t must have a type \tau , written t :: \tau .

In the below code, we define a new type called bool, and we declare that terms of type bool can be used as judgments in our formulae. The details of the judgment command are not important for now.

Formulae in Isabelle are hereditary Harrop formulae, defined as:

In Isabelle's syntax, formulae, terms, and types are typically surrounded by quote marks "" or cartouches ‹› — the two are equivalent.

Consider the following rule: \dfrac {A \quad B}{A \land B}{\text {\small conjI}} This is encoded as an Isabelle formula as follows: \bigwedge A. \left (\bigwedge B. (A \implies (B \implies (A \land B)))\right )

Because \implies is right-associative, we can remove some parentheses:

We can also combine the meta-quantifiers:

Isabelle includes special syntax \llbracket A_0; A_1, \dots , A_n \rrbracket \implies C which is equivalent to A_0 \implies A_1 \implies \dots \implies A_n \implies C.

Isabelle will also automatically add quantifiers to unknown variables, so we can drop the meta-quantifiers from the outermost part of the formula:

Isabelle's basic mechanism to define new things is the axiomatization command.

This defines the constants (with their types) in the constants section, and assumes the formulae stated in the axioms section.

Terms in Isabelle are essentially terms of the (polymorphic) typed lambda calculus. When we declare a constant like:

We are introducing a new constant called conj that has type bool ⇒ bool ⇒ bool — that is, a function that takes two values of type bool and produces another bool. The infixr annotation on the right hand side lets us use familiar notation A ∧ B instead of writing conj A B, but the meaning of A ∧ B is identical to conj A B.

Given a goal \llbracket A_1 \dots A_n \rrbracket \implies G and a theorem r: \llbracket P_1 \dots P_n \rrbracket \implies G (commonly an introduction rule), apply (rule r) replaces the goal with subgoals:

• \llbracket A_1 \dots A_n \rrbracket \implies P_1
• \dots
• \llbracket A_1 \dots A_n \rrbracket \implies P_n

Given a goal \llbracket X; A_1 \dots A_n \rrbracket \implies G and a theorem r: \llbracket X; P_1 \dots P_n \rrbracket \implies Y, apply (frule r) replaces the goal with subgoals:

• \llbracket X; A_1 \dots A_n \rrbracket \implies P_1
• \dots
• \llbracket X; A_1 \dots A_n \rrbracket \implies P_n
• \llbracket X; Y; A_1 \dots A_n \rrbracket \implies G

The method drule is the same as frule except that it also deletes the assumption X from the last subgoal.

Given a goal \llbracket X; A_1 \dots A_n \rrbracket \implies G and a theorem r: \llbracket X; P_1 \dots P_n \rrbracket \implies G (typically an elimination rule where the conclusion is just a variable, easily unified with G), apply (erule r) replaces the goal with subgoals:

• \llbracket A_1 \dots A_n \rrbracket \implies P_1
• \dots
• \llbracket A_1 \dots A_n \rrbracket \implies P_n

The typical rule, erule, drule, frule methods rely entirely on unification to determine how to instantiate the variables in the provided rule. Sometimes, it is useful to state explicitly how to instantiate some variables in the rule, particularly when dealing with quantifiers, or when there are multiple possible candidates.