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.

The Isabelle definition command is a safer way to define constants than the axiomatization command. The syntax is similiar:

However, there are several differences:

• Only one constant (my_const above) can be defined.
• Only one axiom can be defined, and it must be an equation of the format my_const ... = ..., describing the meaning of my_const in terms of other, already-defined constants.

If no name is given to the defining equation, the default name produced by appending _def to the name of the constant is used (e.g. my_const_def)

Given a theorem r: A = B (typically a defining equation given by the definition command), apply (unfold r) replaces every occurrence of A in the current goal with B.

If the theorem r has premises, then all of those premises must be directly satisfied by assumptions in the current goal for unfold to succeed.

We use the unfold method with the lemma generated by Definition [isa-001D] to replace nand with its definition in our goal:

The Isabelle simplifier, or simp, is one of the most powerful proof automation features in Isabelle, but it is a very simple idea. Given a set of equations, apply (simp) will (almost) blindly rewrite the goal by all of those equations (as well as any equations that are local assumptions in the goal) left-to-right. Given a sufficiently expressive set of equations, this allows the simplifier to solve many goals (including all of the theorems in Example [isa-001E]) on its own.

The default set of equations that simp uses is called the simpset. We can add theorems to the simpset by attaching the [simp] attribute to them.

We can also adjust the simpset locally when we invoke the simp method:

The datatype defines a new type (like typedecl) but also defines some special constants, called constructors, which make values of that type. Constructors may optionally take arguments, and these data types may be recursive.

These datatypes are analogous to the algebraic data types found in many functional programming languages.

The datatype command automatically proves many lemmas about these types for you, chiefly:

• Disjointness: Values made with one constructor are not equal to values made with another constructor.
• Exhaustivity: The only values of this type are those made by the listed constructors.
• Injectivity: Two values of the same constructor are equal iff their arguments are equal.

This defines a type called oot with two values, ONE : oot and TWO : oot. The print_theorems command here allows us to see all of the theorems automatically created by the datatype command, chiefly that the constants ONE and TWO are disjoint (i.e. ONE ≠ TWO) and exhaustive (i.e. that there are no other values of type oot apart from ONE and TWO)

The case_tac method splits the current goal into multiple cases. Given a term t of type \tau , apply (case_tac t) will produce a new goal for each possible case of t according to the .cases theorem for the type \tau .

This works for all types defined with datatype, as well as for natural numbers (type nat) and bools — often an easier way to do classical reasoning than using rule ccontr.

Isabelle/HOL's theory of natural numbers defines natural numbers in a different way, but they behave much as if they were defined with the datatype command.

The fun command can be used to define functions in Isabelle. Unlike definitions, functions can be defined by multiple pattern-matching equations, they may be recursive, and their equations are automatically added to the simpset.

The print_theorems command allows us to see all of the lemmas generated by this command.

In cases where the recursion and pattern matching follows exactly the structure of the datatype in one argument, primrec can be used instead of fun, which is a bit more efficient:

While it is possible to use rule or erule with the generated .induct theorem from a datatype, it is usually much simpler and more convenient to use the induct proof method. Similar to the case_tac method, apply (induct t) splits the goal into various cases, one for each constructor of the type of t. The difference is that for recursive cases of the datatype, we also get an inductive hypothesis added to our assumptions.

The above function is given another function as an input.

This type encodes a sequence of oot values. For example, the value ONEs 3 (TWOs 2 (ONEs 1 Empty)) encodes the sequence [ONE, ONE, ONE, TWO, TWO, ONE].

Methods can be combined using the ; operator:

This applies m2 to every subgoal that results from applying m1 to the current goal. It can be chained together multiple times. For example, the entire proof of Theorem [isa-001W] can be much more succinctly expressed as one line:

This function uses the prepend function to concatenate two oots sequences together.

The Isabelle/HOL theory of Lists defines lists as follows:

This is an example of a polymorphic data type, where the type variable 'a stands for a type. For example, the type nat list is the type of lists of nat, and oot list is the type of a list of oots.

The notation x#xs is syntax sugar for Cons x xs and [] is syntax sugar for Nil. Lists can also be written in square brackets, so:

is equivalent to:

which is equivalent to:

Some provided functions are useful, including replicate :: nat ⇒ 'a ⇒ 'a list, which produces a list of n copies of the given value, and append :: 'a list ⇒ 'a list ⇒ 'a list which joins two lists together into one. The append function also has special notation, so a @ b is equivalent to append a b

With the inductive command, we define a predicate by specifying a collection of inference rules, and the inductive predicate is the smallest predicate closed under those rules.

In other words: An element satisfies the predicate exactly if it can be derived using the given rules.

From the given rules, Isabelle automatically generates an induction principle (.induct) which can be used with the induct method (see Proof Method [isa-0029]) and a cases theorem (.cases) for use with the case_tac method.

You’ve already seen how to use induct for structural induction. Exactly the same induct method can also be used for rule induction, when your induction is over an inductively defined predicate, not over the structure of some datatype.

When you define a predicate p with the inductive command, Isabelle automatically produces an induction rule named p.induct. This rule expresses how to perform induction over derivations of p x, one case for each introduction rule of the predicate.

Although you could apply the raw rule with rule or erule, it is almost always easier to use:

This behaves just like structural induction: The goal is split into one subgoal per introduction rule of the predicate, and recursive premises of the rules give rise to induction hypotheses, added to your assumptions.

We define well, an inductive wellformedness predicate for oots sequences, that state there are no segments of zero length, and that no two adjacent segments have the same oot value.

Some methods (like erule when there are multiple matching assumptions) are nondeterministic, producing multiple alternative proof states.

The back command interactively explores a different alternative branch produced by the previous step.

This is useful for interactive exploration, but is very brittle and considered poor style.

Instead, we can combine methods with the comma operator ,: The command apply (m1, m2) first runs m1, and then runs m2, accepting only the nondeterministic branches where the second method m2 succeeds. This avoids the need for back:

For a method m:

Repeatedly applies the m as many times as possible until it fails. It stops automatically when m can no longer make progress; and does not backtrack.

By default, structural induction induct t produces an induction hypothesis for the variables directly mentioned in t, and rule induction induct rule: p.induct produces a hypothesis for the variables directly mentioned by the eliminated p assumption.

Sometimes you need a stronger hypothesis that generalises across additional variables in the goal. The arbitrary option tells the induct method to generalise certain variables, so the induction hypothesis assumes the property holds for all values of those variables.

blast is a method for automatic classical first-order reasoning, based on a tableaux prover. apply blast attempts a thorough search using sets of intro and elim rules. Like simp, rules can be annotated with [intro] and [elim] annotations, or they can be passed locally to blast (i.e. apply (blast intro: nandI1 nandI2 elim: nandE))

The methods fast, slow, and best use a different classical proof search engine than blast, each with a different proof search strategy. fast performs a quick, depth-bounded search, and is generally faster. slow is a more exhaustive search and more backtracking, and best performs a best-first search strategy using a heuristic based on the size of the goal. In general, if fast or blast can solve your goal, it will be the most efficient at solving it, whereas slow and best are only used if no other automated technique works.

Rules such as conjI, impI, or disjE that cannot change a provable goal into unprovable goal(s) are called safe. Isabelle's automation strategies like safe rules because they can apply them without fear, or the need for backtracking. You can mark a rule as safe by marking it [intro!] or [elim!]. This can also be done locally when invoking methods like blast, fast, slow, and best.

The method safe applies only safe rules to the current goal. The method clarify is similar, but it only applies safe rules that do not split the goal into multiple subgoals. Like blast etc., rules can be added to these methods with intro!: etc.

clarsimp the combination of clarify and simp, and is very useful when doing exploratory proving. slowsimp is the combination of slow and simp. bestsimp is the combination of best and simp. The combination of fast and simp is, for inexplicable reasons, called fastforce.

force is a very thorough proof search that can often solve goals other methods can't. It can be thought of as a very thorough version of blast combined with simp. The method auto, by contrast, is a more lightweight search that attempts to simulateneously solve all goals, rather than just the first one. Unlike the other automated methods, auto will leave behind goals that it is unable to prove.

Because the behaviour of auto differs greatly between Isabelle versions and is very sensitive to what theories are loaded, it's considered bad style to use auto as anything but the final step in a proof, but it can nonetheless be useful to see what goals auto outputs to see where it's getting stuck.

Isabelle includes a feature called the sledgehammer that invokes external proof search procedures (such as SMT solvers) and provides them with lemmas that appear to be relevant. If the tools find a proof, it can often replay them in Isabelle's proof kernel, giving an Isabelle proof that matches what the external proof tool found.

To invoke this procedure on a goal, searching automatically for related lemmas, type the word try in an open subgoal.