Introduction to Isabelle

Lawrence C. Paulson Computer Laboratory University of Cambridge

 lcp@cl.cam.ac.uk

With Contributions by Tobias Nipkow and Markus Wenzel

24 November 1997

Copyright \begin{matrix}c \\ ◯ \end{matrix} 1997 by Lawrence C. Paulson

Preface

Isabelle [10, 12, 13] is a generic theorem prover. It has been instantiated to support reasoning in several object-logics:

• first-order logic, constructive and classical versions

• higher-order logic, similar to that of Gordon’s hol [2]

• Zermelo-Fraenkel set theory [18]

• an extensional version of Martin-Löf’s Type Theory [9]

• the classical first-order sequent calculus, lk

• the modal logics T , S4, and S43

• the Logic for Computable Functions [11]

A logic’s syntax and inference rules are specified declaratively; this allows singlestep proof construction. Isabelle provides control structures for expressing search procedures. Isabelle also provides several generic tools, such as simplifiers and classical theorem provers, which can be applied to object-logics.

Isabelle is a large system, but beginners can get by with a small repertoire of commands and a basic knowledge of how Isabelle works. Some knowledge of Standard ml is essential, because ml is Isabelle’s user interface. Advanced Isabelle theorem proving can involve writing ml code, possibly with Isabelle’s sources at hand. My book on ml [14] covers much material connected with Isabelle, including a simple theorem prover. Users must be familiar with logic as used in computer science; there are many good texts [1, 17].

lcf, developed by Robin Milner and colleagues [3], is an ancestor of hol, Nuprl, and several other systems. Isabelle borrows ideas from lcf: formulae are ml values; theorems belong to an abstract type; tactics and tacticals support backward proof. But lcf represents object-level rules by functions, while Isabelle represents them by terms. You may find my other writings [11, 15] helpful in understanding the relationship between lcf and Isabelle.

Isabelle was first distributed in 1986. The 1987 version introduced a higherorder meta-logic with an improved treatment of quantifiers. The 1988 version added limited polymorphism and support for natural deduction. The 1989 version included a parser and pretty printer generator. The 1992 version introduced type classes, to support many-sorted and higher-order logics. The current version provides greater support for theories and is much faster. Isabelle is still under development and will continue to change.

Overview

This manual consists of three parts. Part I discusses the Isabelle’s foundations. Part II, presents simple on-line sessions, starting with forward proof. It also covers basic tactics and tacticals, and some commands for invoking them. Part III contains further examples for users with a bit of experience. It explains how to derive rules define theories, and concludes with an extended example: a Prolog interpreter.

Isabelle’s Reference Manual and Object-Logics manual contain more details. They assume familiarity with the concepts presented here.

Acknowledgements

Tobias Nipkow contributed most of the section on defining theories. Stefan Berghofer and Sara Kalvala suggested improvements.

Tobias Nipkow has made immense contributions to Isabelle, including the parser generator, type classes, and the simplifier. Carsten Clasohm and Markus Wenzel made major contributions; Sonia Mahjoub and Karin Nimmermann also helped. Isabelle was developed using Dave Matthews’s Standard ml compiler, Poly/ml. Many people have contributed to Isabelle’s standard object-logics, including Martin Coen, Philippe de Groote, Philippe Noël. The research has been funded by the EPSRC (grants GR/G53279, GR/H40570, GR/K57381, GR/K77051) and by ESPRIT (projects 3245: Logical Frameworks, and 6453: Types).

Contents

I Foundations 1

1 Formalizing logical syntax in Isabelle 1 1.1 Simple types and constants . . . . . . . . . . . . . . . . . . . . . . 1 1.2 Polymorphic types and constants . . . . . . . . . . . . . . . . . . 3 1.3 Higher types and quantifiers . . . . . . . . . . . . . . . . . . . . . 5

2 Formalizing logical rules in Isabelle 5 2.1 Expressing propositional rules . . . . . . . . . . . . . . . . . . . . 6 2.2 Quantifier rules and substitution . . . . . . . . . . . . . . . . . . . 8 2.3 Signatures and theories . . . . . . . . . . . . . . . . . . . . . . . . 9

3 Proof construction in Isabelle 9 3.1 Higher-order unification . . . . . . . . . . . . . . . . . . . . . . . 11 3.2 Joining rules by resolution . . . . . . . . . . . . . . . . . . . . . . 12

4 Lifting a rule into a context 14 4.1 Lifting over assumptions . . . . . . . . . . . . . . . . . . . . . . . 14 4.2 Lifting over parameters . . . . . . . . . . . . . . . . . . . . . . . . 15

5 Backward proof by resolution 15 5.1 Refinement by resolution . . . . . . . . . . . . . . . . . . . . . . . 16 5.2 Proof by assumption . . . . . . . . . . . . . . . . . . . . . . . . . 16 5.3 A propositional proof . . . . . . . . . . . . . . . . . . . . . . . . . 17 5.4 A quantifier proof . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 5.5 Tactics and tacticals . . . . . . . . . . . . . . . . . . . . . . . . . 19

6 Variations on resolution 20 6.1 Elim-resolution . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 6.2 Destruction rules . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 6.3 Deriving rules by resolution . . . . . . . . . . . . . . . . . . . . . 22

II Getting Started with Isabelle 24

7 Forward proof 24 7.1 Lexical matters . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 7.2 Syntax of types and terms . . . . . . . . . . . . . . . . . . . . . . 25 7.3 Basic operations on theorems . . . . . . . . . . . . . . . . . . . . 27 7.4 *Flex-flex constraints . . . . . . . . . . . . . . . . . . . . . . . . . 28 8 Backward proof 29

8.1 The basic tactics . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 8.2 Commands for backward proof . . . . . . . . . . . . . . . . . . . . 30 8.3 A trivial example in propositional logic . . . . . . . . . . . . . . . 31 8.4 Part of a distributive law . . . . . . . . . . . . . . . . . . . . . . . 32

9 Quantifier reasoning 34 9.1 Two quantifier proofs: a success and a failure . . . . . . . . . . . 34 9.2 Nested quantifiers . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 9.3 A realistic quantifier proof . . . . . . . . . . . . . . . . . . . . . . 38 9.4 The classical reasoner . . . . . . . . . . . . . . . . . . . . . . . . . 39

III Advanced Methods 41

10 Deriving rules in Isabelle 41 10.1 Deriving a rule using tactics and meta-level assumptions . . . . . 41 10.2 Definitions and derived rules . . . . . . . . . . . . . . . . . . . . . 43 10.3 Deriving the ¬ introduction rule . . . . . . . . . . . . . . . . . . . 43 10.4 Deriving the ¬ elimination rule . . . . . . . . . . . . . . . . . . . 45

11 Defining theories 47 11.1 Declaring constants, definitions and rules . . . . . . . . . . . . . . 48 11.2 Declaring type constructors . . . . . . . . . . . . . . . . . . . . . 49 11.3 Type synonyms . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 11.4 Infix and mixfix operators . . . . . . . . . . . . . . . . . . . . . . 52 11.5 Overloading . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53

12 Theory example: the natural numbers 54 12.1 Extending first-order logic with the natural numbers . . . . . . . 54 12.2 Declaring the theory to Isabelle . . . . . . . . . . . . . . . . . . . 56 12.3 Proving some recursion equations . . . . . . . . . . . . . . . . . . 56

13 Refinement with explicit instantiation 57 13.1 A simple proof by induction . . . . . . . . . . . . . . . . . . . . . 57 13.2 An example of ambiguity in resolve_tac . . . . . . . . . . . . . 58 13.3 Proving that addition is associative . . . . . . . . . . . . . . . . . 60

14 A Prolog interpreter 61 14.1 Simple executions . . . . . . . . . . . . . . . . . . . . . . . . . . . 62 14.2 Backtracking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62 14.3 Depth-first search . . . . . . . . . . . . . . . . . . . . . . . . . . . 63

You can only find truth with logic if you have already found truth without it.

G.K. Chesterton, The Man who was Orthodox vi

Part I

Foundations

The following sections discuss Isabelle’s logical foundations in detail: representing logical syntax in the typed λ-calculus; expressing inference rules in Isabelle’s meta-logic; combining rules by resolution.

If you wish to use Isabelle immediately, please turn to page 24. You can always read about foundations later, either by returning to this point or by looking up particular items in the index.

1 Formalizing logical syntax in Isabelle

Figure 1 presents intuitionistic first-order logic, including equality. Let us see how to formalize this logic in Isabelle, illustrating the main features of Isabelle’s polymorphic meta-logic.

Isabelle represents syntax using the simply typed λ-calculus. We declare a type for each syntactic category of the logic. We declare a constant for each symbol of the logic, giving each n-place operation an n-argument curried function type. Most importantly, λ-abstraction represents variable binding in quantifiers.

Isabelle has ml-style polymorphic types such as (α)list, where list is a type constructor and α is a type variable; for example, (bool)list is the type of lists of booleans. Function types have the form (σ, τ)fun or σ ⇒ τ, where σ and τ are types. Curried function types may be abbreviated:

σ_{1} ⇒ (⋯ σ_{n} ⇒ τ ⋯) as [σ_{1}, …, σ_{n}] ⇒ τ

The syntax for terms is summarised below. Note that there are two versions of function application syntax available in Isabelle: either t u, which is the usual form for higher-order languages, or t(u), trying to look more like first-order. The latter syntax is used throughout the manual.

t :: τ  type constraint, on a term or bound variable
λx . t  abstraction
λx_{1} … x_{n} . t curried abstraction, λx_{1} …. λx_{n} . t
t(u)  application
t(u_{1}, …, u_{n}) curried application, t(u_{1}) … (u_{n})

1.1 Simple types and constants

The syntactic categories of our logic (Fig. 1) are formulae and terms. Formulae denote truth values, so (following tradition) let us call their type o. To allow 0

¬P abbreviates P → ⊥
P ↔ Q abbreviates (P → Q) ∧ (Q → P)

\begin{matrix}P & Q \\ P ∧ Q \end{matrix} (∧I )  {P ∧ Q \atop P} (∧E1) {P ∧ Q \atop Q} (∧E2)

{P \atop P ∨ Q} (∨I 1) {Q \atop P ∨ Q} (∨I 2)  \begin{aligned}P ∨ Q & [P] ⋮ . R & [Q] ⋮ . R \\ & R \end{aligned}(∨E)

[P] ⋮ . Q ; P → Q (→I )  \begin{matrix}P → Q & P \\ Q \end{matrix} (→E)

{⊥ \atop P} (⊥E)

{P \atop ∀x . P} (∀I )∗  {∀x . P \atop P[t/x]} (∀E)

{P[t/x] \atop ∃x . P} (∃I )  \begin{matrix}∃x . P & [P] ⋮ . Q \\ Q \end{matrix} (∃E)∗

t = t (refl)  t = u P[t/x] P[u/x] (subst)

*Eigenvariable conditions: ∀I : provided x is not free in the assumptions ∃E: provided x is not free in Q or any assumption except P

Figure 1: Intuitionistic first-order logic and Suc(t) as terms, let us declare a type nat of natural numbers. Later, we shall see how to admit terms of other types.

After declaring the types o and nat, we may declare constants for the symbols of our logic. Since ⊥ denotes a truth value (falsity) and 0 denotes a number, we put

⊥ :: o
0 :: nat.

If a symbol requires operands, the corresponding constant must have a function type. In our logic, the successor function (Suc) is from natural numbers to natural numbers, negation (¬) is a function from truth values to truth values, and the binary connectives are curried functions taking two truth values as arguments:

Suc :: nat ⇒ nat
¬ :: o ⇒ o
∧, ∨, →, ↔ :: [o, o] ⇒ o

The binary connectives can be declared as infixes, with appropriate precedences, so that we write P ∧ Q ∨ R instead of ∨(∧(P, Q), R).

Section 11 below describes the syntax of Isabelle theory files and illustrates it by extending our logic with mathematical induction.

1.2 Polymorphic types and constants

Which type should we assign to the equality symbol? If we tried [nat, nat] ⇒ o, then equality would be restricted to the natural numbers; we should have to declare different equality symbols for each type. Isabelle’s type system is polymorphic, so we could declare

= :: [α, α] ⇒ o,

where the type variable α ranges over all types. But this is also wrong. The declaration is too polymorphic; α includes types like o and nat ⇒ nat. Thus, it admits ⊥ = ¬(⊥) and Suc = Suc as formulae, which is acceptable in higher-order logic but not in first-order logic.

Isabelle’s type classes control polymorphism [8]. Each type variable belongs to a class, which denotes a set of types. Classes are partially ordered by the subclass relation, which is essentially the subset relation on the sets of types. They closely resemble the classes of the functional language Haskell [4, 5].

Isabelle provides the built-in class logic, which consists of the logical types: the ones we want to reason about. Let us declare a class term, to consist of all legal types of terms in our logic. The subclass structure is now term ≤ logic.

We put nat in class term by declaring nat::term. We declare the equality constant by

= :: [α::term, α] ⇒ o

where α::term constrains the type variable α to class term. Such type variables resemble Standard ml’s equality type variables.

We give o and function types the class logic rather than term, since they are not legal types for terms. We may introduce new types of class term — for instance, type string or real — at any time. We can even declare type constructors such as list, and state that type (τ)list belongs to class term provided τ does; equality applies to lists of natural numbers but not to lists of formulae. We may summarize this paragraph by a set of arity declarations for type constructors:

o :: logic
fun :: (logic, logic)logic
nat, string, real :: term
list :: (term)term

(Recall that fun is the type constructor for function types.) In higher-order logic, equality does apply to truth values and functions; this requires the arity declarations o :: term and fun :: (term, term)term. The class system can also handle overloading. We could declare arith to be the subclass of term consisting of the ‘arithmetic’ types, such as nat. Then we could declare the operators

+, −, ×, / :: [α::arith, α] ⇒ α

If we declare new types real and complex of class arith, then we in effect have three sets of operators:

+, −, ×, / :: [nat, nat] ⇒ nat
+, −, ×, / :: [real, real] ⇒ real
+, −, ×, / :: [complex, complex] ⇒ complex

Isabelle will regard these as distinct constants, each of which can be defined separately. We could even introduce the type (α)vector and declare its arity as (arith)arith. Then we could declare the constant

+ :: [(α)vector, (α)vector] ⇒ (α)vector

and specify it in terms of + :: [α, α] ⇒ α.

A type variable may belong to any finite number of classes. Suppose that we had declared yet another class ord ≤ term, the class of all ‘ordered’ types, and a constant

≤ :: [α::ord, α] ⇒ o.

In this context the variable x in x ≤ (x +x) will be assigned type α::{arith, ord}, which means α belongs to both arith and ord. Semantically the set {arith, ord} should be understood as the intersection of the sets of types represented by arith and ord. Such intersections of classes are called sorts. The empty intersection of classes, {}, contains all types and is thus the universal sort.

Even with overloading, each term has a unique, most general type. For this to be possible, the class and type declarations must satisfy certain technical constraints; see Sect. Defining Theories in the Reference Manual.

1.3 Higher types and quantifiers

Quantifiers are regarded as operations upon functions. Ignoring polymorphism for the moment, consider the formula ∀x . P(x), where x ranges over type nat. This is true if P(x) is true for all x. Abstracting P(x) into a function, this is the same as saying that λx . P(x) returns true for all arguments. Thus, the universal quantifier can be represented by a constant

∀ :: (nat ⇒ o) ⇒ o,

which is essentially an infinitary truth table. The representation of ∀x . P(x) is ∀(λx . P(x)).

The existential quantifier is treated in the same way. Other binding operators are also easily handled; for instance, the summation operator Σ_{k=i}^{j}f (k) can be represented as Σ(i, j , λk . f (k)), where

Σ :: [nat, nat, nat ⇒ nat] ⇒ nat.

Quantifiers may be polymorphic. We may define ∀ and ∃ over all legal types of terms, not just the natural numbers, and allow summations over all arithmetic types:

∀, ∃ :: (α::term ⇒ o) ⇒ o
Σ :: [nat, nat, nat ⇒ α::arith] ⇒ α

Observe that the index variables still have type nat, while the values being summed may belong to any arithmetic type.

2 Formalizing logical rules in Isabelle

Object-logics are formalized by extending Isabelle’s meta-logic [12], which is intuitionistic higher-order logic. The meta-level connectives are implication, the universal quantifier, and equality.

• The implication ϕ ⟹ ψ means ‘ϕ implies ψ’, and expresses logical entailment.

• The quantification ⋀ x . ϕ means ‘ϕ is true for all x’, and expresses generality in rules and axiom schemes.

• The equality a ≡ b means ‘a equals b’, for expressing definitions (see §10.2). Equalities left over from the unification process, so called flexflex constraints, are written a ≡^{?} b. The two equality symbols have the same logical meaning.

The syntax of the meta-logic is formalized in the same manner as object-logics, using the simply typed λ-calculus. Analogous to type o above, there is a built-in type prop of meta-level truth values. Meta-level formulae will have this type. Type prop belongs to class logic; also, σ ⇒ τ belongs to logic provided σ and τ do. Here are the types of the built-in connectives:

⟹ :: [prop, prop] ⇒ prop
⋀ :: (α::logic ⇒ prop) ⇒ prop
≡ :: [α::{}, α] ⇒ prop
≡^{?} :: [α::{}, α] ⇒ prop

The polymorphism in ⋀ is restricted to class logic to exclude certain types, those used just for parsing. The type variable α::{} ranges over the universal sort.

In our formalization of first-order logic, we declared a type o of object-level truth values, rather than using prop for this purpose. If we declared the objectlevel connectives to have types such as ¬ :: prop ⇒ prop, then these connectives would be applicable to meta-level formulae. Keeping prop and o as separate types maintains the distinction between the meta-level and the object-level. To formalize the inference rules, we shall need to relate the two levels; accordingly, we declare the constant

Trueprop :: o ⇒ prop.

We may regard Trueprop as a meta-level predicate, reading Trueprop(P) as ‘P is true at the object-level.’ Put another way, Trueprop is a coercion from o to prop.

2.1 Expressing propositional rules

We shall illustrate the use of the meta-logic by formalizing the rules of Fig. 1. Each object-level rule is expressed as a meta-level axiom.

One of the simplest rules is (∧E1). Making everything explicit, its formalization in the meta-logic is

⋀ P Q . Trueprop(P ∧ Q) ⟹ Trueprop(P).  (∧E1)

This may look formidable, but it has an obvious reading: for all object-level truth values P and Q, if P ∧ Q is true then so is P. The reading is correct because the meta-logic has simple models, where types denote sets and ⋀ really means ‘for all.’

Isabelle adopts notational conventions to ease the writing of rules. We may hide the occurrences of Trueprop by making it an implicit coercion. Outer universal quantifiers may be dropped. Finally, the nested implication

ϕ_{1} ⟹ (⋯ ϕ_{n} ⟹ ψ ⋯)

may be abbreviated as [[ϕ_{1}; …; ϕ_{n}]] ⟹ ψ, which formalizes a rule of n premises.

Using these conventions, the conjunction rules become the following axioms. These fully specify the properties of ∧:

[[P; Q]] ⟹ P ∧ Q  (∧I )
P ∧ Q ⟹ P  P ∧ Q ⟹ Q  (∧E1, 2)

Next, consider the disjunction rules. The discharge of assumption in (∨E) is expressed using ⟹:

P ⟹ P ∨ Q  Q ⟹ P ∨ Q  (∨I 1, 2)
[[P ∨ Q; P ⟹ R; Q ⟹ R]] ⟹ R  (∨E)

To understand this treatment of assumptions in natural deduction, look at implication. The rule (→I ) is the classic example of natural deduction: to prove that P → Q is true, assume P is true and show that Q must then be true. More concisely, if P implies Q (at the meta-level), then P → Q is true (at the object-level). Showing the coercion explicitly, this is formalized as

(Trueprop(P) ⟹ Trueprop(Q)) ⟹ Trueprop(P → Q).

The rule (→E) is straightforward; hiding Trueprop, the axioms to specify → are

(P ⟹ Q) ⟹ P → Q  (→I )
[[P → Q; P]] ⟹ Q.  (→E)

Finally, the intuitionistic contradiction rule is formalized as the axiom

⊥ ⟹ P.  (⊥E)

! Earlier versions of Isabelle, and certain papers [12, 13], use [[P]] to mean Trueprop(P).

2.2 Quantifier rules and substitution

Isabelle expresses variable binding using λ-abstraction; for instance, ∀x . P is formalized as ∀(λx . P). Recall that F (t) is Isabelle’s syntax for application of the function F to the argument t; it is not a meta-notation for substitution. On the other hand, a substitution will take place if F has the form λx . P; Isabelle transforms (λx . P)(t) to P[t/x] by β-conversion. Thus, we can express inference rules that involve substitution for bound variables.

A logic may attach provisos to certain of its rules, especially quantifier rules. We cannot hope to formalize arbitrary provisos. Fortunately, those typical of quantifier rules always have the same form, namely ‘x not free in … (some set of formulae),’ where x is a variable (called a parameter or eigenvariable) in some premise. Isabelle treats provisos using ⋀, its inbuilt notion of ‘for all’.

The purpose of the proviso ‘x not free in … ’ is to ensure that the premise may not make assumptions about the value of x, and therefore holds for all x. We formalize (∀I ) by

(⋀ x . Trueprop(P(x))) ⟹ Trueprop(∀x . P(x)).

This means, ‘if P(x) is true for all x, then ∀x .P(x) is true.’ The ∀E rule exploits β-conversion. Hiding Trueprop, the ∀ axioms are

(⋀ x . P(x)) ⟹ ∀x . P(x)  (∀I )
(∀x . P(x)) ⟹ P(t).  (∀E)

We have defined the object-level universal quantifier (∀) using ⋀. But we do not require meta-level counterparts of all the connectives of the object-logic! Consider the existential quantifier:

P(t) ⟹ ∃x . P(x)  (∃I )
[[∃x . P(x); ⋀ x . P(x) ⟹ Q]] ⟹ Q  (∃E)

Let us verify (∃E) semantically. Suppose that the premises hold; since ∃x . P(x) is true, we may choose an a such that P(a) is true. Instantiating ⋀ x .P(x) ⟹ Q with a yields P(a) ⟹ Q, and we obtain the desired conclusion, Q.

The treatment of substitution deserves mention. The rule

\begin{matrix}t = u & P \\ P[u/t] \end{matrix}

would be hard to formalize in Isabelle. It calls for replacing t by u throughout P, which cannot be expressed using β-conversion. Our rule (subst) uses P as a template for substitution, inferring P[u/x] from P[t/x]. When we formalize this as an axiom, the template becomes a function variable:

[[t = u; P(t)]] ⟹ P(u).  (subst)

2.3 Signatures and theories

A signature contains the information necessary for type checking, parsing and pretty printing a term. It specifies type classes and their relationships, types and their arities, constants and their types, etc. It also contains grammar rules, specified using mixfix declarations.

Two signatures can be merged provided their specifications are compatible — they must not, for example, assign different types to the same constant. Under similar conditions, a signature can be extended. Signatures are managed internally by Isabelle; users seldom encounter them.

A theory consists of a signature plus a collection of axioms. The Pure theory contains only the meta-logic. Theories can be combined provided their signatures are compatible. A theory definition extends an existing theory with further signature specifications — classes, types, constants and mixfix declarations — plus lists of axioms and definitions etc., expressed as strings to be parsed. A theory can formalize a small piece of mathematics, such as lists and their operations, or an entire logic. A mathematical development typically involves many theories in a hierarchy. For example, the Pure theory could be extended to form a theory for Fig. 1; this could be extended in two separate ways to form a theory for natural numbers and a theory for lists; the union of these two could be extended into a theory defining the length of a list:

                              Pure

↓

                               FOL

↙  ↘

                       Nat             List

↘  ↙

                            Nat + List

↓

                             Length

Each Isabelle proof typically works within a single theory, which is associated with the proof state. However, many different theories may coexist at the same time, and you may work in each of these during a single session.

! Confusing problems arise if you work in the wrong theory. Each theory defines

its own syntax. An identifier may be regarded in one theory as a constant and in another as a variable, for example.

3 Proof construction in Isabelle

I have elsewhere described the meta-logic and demonstrated it by formalizing first-order logic [12]. There is a one-to-one correspondence between meta-level proofs and object-level proofs. To each use of a meta-level axiom, such as (∀I ), there is a use of the corresponding object-level rule. Object-level assumptions and parameters have meta-level counterparts. The meta-level formalization is faithful, admitting no incorrect object-level inferences, and adequate, admitting all correct object-level inferences. These properties must be demonstrated separately for each object-logic.

The meta-logic is defined by a collection of inference rules, including equational rules for the λ-calculus and logical rules. The rules for ⟹ and ⋀ resemble those for → and ∀ in Fig. 1. Proofs performed using the primitive meta-rules would be lengthy; Isabelle proofs normally use certain derived rules. Resolution, in particular, is convenient for backward proof.

Unification is central to theorem proving. It supports quantifier reasoning by allowing certain ‘unknown’ terms to be instantiated later, possibly in stages. When proving that the time required to sort n integers is proportional to n^{2}, we need not state the constant of proportionality; when proving that a hardware adder will deliver the sum of its inputs, we need not state how many clock ticks will be required. Such quantities often emerge from the proof.

Isabelle provides schematic variables, or unknowns, for unification. Logically, unknowns are free variables. But while ordinary variables remain fixed, unification may instantiate unknowns. Unknowns are written with a ? prefix and are frequently subscripted: ?a, ?a_{1}, ?a_{2}, …, ?P, ?P_{1}, ….

Recall that an inference rule of the form

\begin{aligned}ϕ_{1} & … & ϕ_{n} \\ & ϕ \end{aligned}

is formalized in Isabelle’s meta-logic as the axiom [[ϕ_{1}; …; ϕ_{n}]] ⟹ ϕ. Such axioms resemble Prolog’s Horn clauses, and can be combined by resolution — Isabelle’s principal proof method. Resolution yields both forward and backward proof. Backward proof works by unifying a goal with the conclusion of a rule, whose premises become new subgoals. Forward proof works by unifying theorems with the premises of a rule, deriving a new theorem.

Isabelle formulae require an extended notion of resolution. They differ from Horn clauses in two major respects:

• They are written in the typed λ-calculus, and therefore must be resolved using higher-order unification.

• The constituents of a clause need not be atomic formulae. Any formula of the form Trueprop(⋯) is atomic, but axioms such as →I and ∀I contain non-atomic formulae.

Isabelle has little in common with classical resolution theorem provers such as Otter [19]. At the meta-level, Isabelle proves theorems in their positive form, not by refutation. However, an object-logic that includes a contradiction rule may employ a refutation proof procedure.

3.1 Higher-order unification

Unification is equation solving. The solution of f (?x, c) ≡^{?} f (d,?y) is ?x ≡ d and ?y ≡ c. Higher-order unification is equation solving for typed λ-terms. To handle β-conversion, it must reduce (λx . t)u to t[u/x]. That is easy — in the typed λ-calculus, all reduction sequences terminate at a normal form. But it must guess the unknown function ?f in order to solve the equation

?f (t) ≡^{?} g(u_{1}, …, u_{k}).  (1)

Huet’s [6] search procedure solves equations by imitation and projection. Imitation makes ?f apply the leading symbol (if a constant) of the right-hand side. To solve equation (1), it guesses

?f ≡ λx . g(?h_{1}(x), …,?h_{k}(x)),

where ?h_{1}, …, ?h_{k} are new unknowns. Assuming there are no other occurrences of ?f , equation (1) simplifies to the set of equations

?h_{1}(t) ≡^{?} u_{1} … ?h_{k}(t) ≡^{?} u_{k}.

If the procedure solves these equations, instantiating ?h_{1}, …, ?h_{k}, then it yields an instantiation for ?f .

Projection makes ?f apply one of its arguments. To solve equation (1), if t expects m arguments and delivers a result of suitable type, it guesses

?f ≡ λx . x(?h_{1}(x), …,?h_{m}(x)),

where ?h_{1}, …, ?h_{m} are new unknowns. Assuming there are no other occurrences of ?f , equation (1) simplifies to the equation

t(?h_{1}(t), …,?h_{m}(t)) ≡^{?} g(u_{1}, …, u_{k}).

! Huet’s unification procedure is complete. Isabelle’s polymorphic version, which

solves for type unknowns as well as for term unknowns, is incomplete. The problem is that projection requires type information. In equation (1), if the type of t is unknown, then projections are possible for all m ≥ 0, and the types of the ?h_{i} will be similarly unconstrained. Therefore, Isabelle never attempts such projections, and may fail to find unifiers where a type unknown turns out to be a function type.

Given ?f (t_{1}, …, t_{n}) ≡^{?} u, Huet’s procedure could make up to n + 1 guesses. The search tree and set of unifiers may be infinite. But higher-order unification can work effectively, provided you are careful with function unknowns:

• Equations with no function unknowns are solved using first-order unification, extended to treat bound variables. For example, λx . x ≡^{?} λx .?y has no solution because ?y ≡ x would capture the free variable x.

• An occurrence of the term ?f (x, y, z), where the arguments are distinct bound variables, causes no difficulties. Its projections can only match the corresponding variables.

• Even an equation such as ?f (a) ≡^{?} a + a is all right. It has four solutions, but Isabelle evaluates them lazily, trying projection before imitation. The first solution is usually the one desired:

?f ≡ λx . x + x ?f ≡ λx . a + x ?f ≡ λx . x + a ?f ≡ λx . a + a

• Equations such as ?f (?x,?y) ≡^{?} t and ?f (?g(x)) ≡^{?} t admit vast numbers of unifiers, and must be avoided.

In problematic cases, you may have to instantiate some unknowns before invoking unification.

3.2 Joining rules by resolution

Let [[ψ_{1}; …; ψ_{m}]] ⟹ ψ and [[ϕ_{1}; …; ϕ_{n}]] ⟹ ϕ be two Isabelle theorems, representing object-level rules. Choosing some i from 1 to n, suppose that ψ and ϕ_{i} have a higher-order unifier. Writing Xs for the application of substitution s to expression X , this means there is some s such that ψs ≡ ϕ_{i}s. By resolution, we may conclude

([[ϕ_{1}; …; ϕ_{i−1}; ψ_{1}; …; ψ_{m}; ϕ_{i+1}; …; ϕ_{n}]] ⟹ ϕ)s.

The substitution s may instantiate unknowns in both rules. In short, resolution is the following rule:

\begin{matrix}[[ψ_{1}; …; ψ_{m}]] ⟹ ψ & [[ϕ_{1}; …; ϕ_{n}]] ⟹ ϕ \\ ([[ϕ_{1}; …; ϕ_{i−1}; ψ_{1}; …; ψ_{m}; ϕ_{i+1}; …; ϕ_{n}]] ⟹ ϕ)s \end{matrix} (ψs ≡ ϕ_{i}s)

It operates at the meta-level, on Isabelle theorems, and is justified by the properties of ⟹ and ⋀. It takes the number i (for 1 ≤ i ≤ n) as a parameter and may yield infinitely many conclusions, one for each unifier of ψ with ϕ_{i}. Isabelle returns these conclusions as a sequence (lazy list).

Resolution expects the rules to have no outer quantifiers (⋀). It may rename or instantiate any schematic variables, but leaves free variables unchanged. When constructing a theory, Isabelle puts the rules into a standard form with all free variables converted into schematic ones; for instance, (→E) becomes

[[?P → ?Q; ?P]] ⟹ ?Q.

When resolving two rules, the unknowns in the first rule are renamed, by subscripting, to make them distinct from the unknowns in the second rule. To resolve (→E) with itself, the first copy of the rule becomes

[[?P_{1} → ?Q_{1}; ?P_{1}]] ⟹ ?Q_{1}.

Resolving this with (→E) in the first premise, unifying ?Q_{1} with ?P → ?Q, is the meta-level inference

[[?P_{1} → ?Q_{1}; ?P_{1}]] ⟹ ?Q_{1} [[?P → ?Q; ?P]] ⟹ ?Q
[[?P_{1} → (?P → ?Q); ?P_{1}; ?P]] ⟹ ?Q.

Renaming the unknowns in the resolvent, we have derived the object-level rule

\begin{matrix}R → (P → Q) & R & P \\ Q. \end{matrix}

Joining rules in this fashion is a simple way of proving theorems. The derived rules are conservative extensions of the object-logic, and may permit simpler proofs. Let us consider another example. Suppose we have the axiom

∀x y . Suc(x) = Suc(y) → x = y.  (inject)

The standard form of (∀E) is ∀x .?P(x) ⟹ ?P(?t). Resolving (inject) with (∀E) replaces ?P by λx . ∀y . Suc(x) = Suc(y) → x = y and leaves ?t unchanged, yielding

∀y . Suc(?t) = Suc(y) → ?t = y.

Resolving this with (∀E) puts a subscript on ?t and yields

Suc(?t_{1}) = Suc(?t) → ?t_{1} = ?t.

Resolving this with (→E) increases the subscripts and yields

Suc(?t_{2}) = Suc(?t_{1}) ⟹ ?t_{2} = ?t_{1}.

We have derived the rule

Suc(m) = Suc(n) m = n,

which goes directly from Suc(m) = Suc(n) to m = n. It is handy for simplifying an equation like Suc(Suc(Suc(m))) = Suc(Suc(Suc(0))).

4 Lifting a rule into a context

The rules (→I ) and (∀I ) may seem unsuitable for resolution. They have nonatomic premises, namely P ⟹ Q and ⋀ x . P(x), while the conclusions of all the rules are atomic (they have the form Trueprop(⋯)). Isabelle gets round the problem through a meta-inference called lifting. Let us consider how to construct proofs such as

[P, Q] ; ⋮ . ; R ; Q → R (→I )

P → (Q → R) (→I )

{P(x, y) \atop ∀y . P(x, y)} (∀I )

∀x y . P(x, y) (∀I )

4.1 Lifting over assumptions

Lifting over θ ⟹ is the following meta-inference rule:

{[[ϕ_{1}; …; ϕ_{n}]] ⟹ ϕ \atop [[θ ⟹ ϕ_{1}; …; θ ⟹ ϕ_{n}]] ⟹ (θ ⟹ ϕ)}

This is clearly sound: if [[ϕ_{1}; …; ϕ_{n}]] ⟹ ϕ is true and θ ⟹ ϕ_{1}, …, θ ⟹ ϕ_{n} and θ are all true then ϕ must be true. Iterated lifting over a series of meta-formulae θ_{k}, …, θ_{1} yields an object-rule whose conclusion is [[θ_{1}; …; θ_{k}]] ⟹ ϕ. Typically the θ_{i} are the assumptions in a natural deduction proof; lifting copies them into a rule’s premises and conclusion.

When resolving two rules, Isabelle lifts the first one if necessary. The standard form of (→I ) is

(?P ⟹ ?Q) ⟹ ?P → ?Q.

To resolve this rule with itself, Isabelle modifies one copy as follows: it renames the unknowns to ?P_{1} and ?Q_{1}, then lifts the rule over ?P ⟹ to obtain

(?P ⟹ (?P_{1} ⟹ ?Q_{1})) ⟹ (?P ⟹ (?P_{1} → ?Q_{1})).

Using the [[⋯]] abbreviation, this can be written as

[[[[?P; ?P_{1}]] ⟹ ?Q_{1}; ?P]] ⟹ ?P_{1} → ?Q_{1}.

Unifying ?P ⟹ ?P_{1} → ?Q_{1} with ?P ⟹ ?Q instantiates ?Q to ?P_{1} → ?Q_{1}. Resolution yields

([[?P; ?P_{1}]] ⟹ ?Q_{1}) ⟹ ?P → (?P_{1} → ?Q_{1}).

This represents the derived rule

[P, Q] ; ⋮ . ; R ; P → (Q → R).

4.2 Lifting over parameters

An analogous form of lifting handles premises of the form ⋀ x . . .. Here, lifting prefixes an object-rule’s premises and conclusion with ⋀ x. At the same time, lifting introduces a dependence upon x. It replaces each unknown ?a in the rule by ?a′(x), where ?a′ is a new unknown (by subscripting) of suitable type — necessarily a function type. In short, lifting is the meta-inference

[[ϕ_{1}; …; ϕ_{n}]] ⟹ ϕ
[[⋀ x . ϕ_{1}^{x}; …; ⋀ x . ϕ_{n}^{x}]] ⟹ ⋀ x . ϕ^{x},

where ϕ^{x} stands for the result of lifting unknowns over x in ϕ. It is not hard to verify that this meta-inference is sound. If ϕ ⟹ ψ then ϕ^{x} ⟹ ψ^{x} for all x; so if ϕ^{x} is true for all x then so is ψ^{x}. Thus, from ϕ ⟹ ψ we conclude (⋀ x . ϕ^{x}) ⟹ (⋀ x . ψ^{x}).

For example, (∨I ) might be lifted to

(⋀ x .?P_{1}(x)) ⟹ (⋀ x .?P_{1}(x) ∨?Q_{1}(x))

and (∀I ) to

(⋀ x y .?P_{1}(x, y)) ⟹ (⋀ x . ∀y .?P_{1}(x, y)).

Isabelle has renamed a bound variable in (∀I ) from x to y, avoiding a clash. Resolving the above with (∀I ) is the meta-inference

(⋀ x y .?P_{1}(x, y)) ⟹ (⋀ x . ∀y .?P_{1}(x, y)) (⋀ x .?P(x)) ⟹ (∀x .?P(x))
⋀ x y .?P_{1}(x, y)) ⟹ ∀x y .?P_{1}(x, y))

Here, ?P is replaced by λx . ∀y .?P_{1}(x, y); the resolvent expresses the derived rule

Q(x, y) ; ∀x y . Q(x, y) provided x, y not free in the assumptions

I discuss lifting and parameters at length elsewhere [12]. Miller goes into even greater detail [7].

5 Backward proof by resolution

Resolution is convenient for deriving simple rules and for reasoning forward from facts. It can also support backward proof, where we start with a goal and refine it to progressively simpler subgoals until all have been solved. lcf and its descendants hol and Nuprl provide tactics and tacticals, which constitute a sophisticated language for expressing proof searches. Tactics refine subgoals while tacticals combine tactics.

Isabelle’s tactics and tacticals work differently from lcf’s. An Isabelle rule is bidirectional: there is no distinction between inputs and outputs. lcf has a separate tactic for each rule; Isabelle performs refinement by any rule in a uniform fashion, using resolution.

Isabelle works with meta-level theorems of the form [[ϕ_{1}; …; ϕ_{n}]] ⟹ ϕ. We have viewed this as the rule with premises ϕ_{1}, …, ϕ_{n} and conclusion ϕ. It can also be viewed as the proof state with subgoals ϕ_{1}, …, ϕ_{n} and main goal ϕ.

To prove the formula ϕ, take ϕ ⟹ ϕ as the initial proof state. This assertion is, trivially, a theorem. At a later stage in the backward proof, a typical proof state is [[ϕ_{1}; …; ϕ_{n}]] ⟹ ϕ. This proof state is a theorem, ensuring that the subgoals ϕ_{1}, …, ϕ_{n} imply ϕ. If n = 0 then we have proved ϕ outright. If ϕ contains unknowns, they may become instantiated during the proof; a proof state may be [[ϕ_{1}; …; ϕ_{n}]] ⟹ ϕ′, where ϕ′ is an instance of ϕ.

5.1 Refinement by resolution

To refine subgoal i of a proof state by a rule, perform the following resolution:

rule proof state

new proof state

Suppose the rule is [[ψ′_{1}; …; ψ′_{m}]] ⟹ ψ′ after lifting over subgoal i’s assumptions and parameters. If the proof state is [[ϕ_{1}; …; ϕ_{n}]] ⟹ ϕ, then the new proof state is (for 1 ≤ i ≤ n)

([[ϕ_{1}; …; ϕ_{i−1}; ψ′_{1}; …; ψ′_{m}; ϕ_{i+1}; …; ϕ_{n}]] ⟹ ϕ)s.

Substitution s unifies ψ′ with ϕ_{i}. In the proof state, subgoal i is replaced by m new subgoals, the rule’s instantiated premises. If some of the rule’s unknowns are left un-instantiated, they become new unknowns in the proof state. Refinement by (∃I ), namely

?P(?t) ⟹ ∃x .?P(x),

inserts a new unknown derived from ?t by subscripting and lifting. We do not have to specify an ‘existential witness’ when applying (∃I ). Further resolutions may instantiate unknowns in the proof state.

5.2 Proof by assumption

In the course of a natural deduction proof, parameters x_{1}, …, x_{l} and assumptions θ_{1}, …, θ_{k} accumulate, forming a context for each subgoal. Repeated lifting steps can lift a rule into any context. To aid readability, Isabelle puts contexts into a normal form, gathering the parameters at the front:

⋀ x_{1} … x_{l} . [[θ_{1}; …; θ_{k}]] ⟹ θ.  (2)

Under the usual reading of the connectives, this expresses that θ follows from θ_{1}, … θ_{k} for arbitrary x_{1}, …, x_{l}. It is trivially true if θ equals any of θ_{1}, … θ_{k}, or is unifiable with any of them. This models proof by assumption in natural deduction.

Isabelle automates the meta-inference for proof by assumption. Its arguments are the meta-theorem [[ϕ_{1}; …; ϕ_{n}]] ⟹ ϕ, and some i from 1 to n, where ϕ_{i} has the form (2). Its results are meta-theorems of the form

([[ϕ_{1}; …; ϕ_{i−1}; ϕ_{i+1}; ϕ_{n}]] ⟹ ϕ)s

for each s and j such that s unifies λx_{1} … x_{l} .θ_{j} with λx_{1} … x_{l} .θ. Isabelle supplies the parameters x_{1}, …, x_{l} to higher-order unification as bound variables, which regards them as unique constants with a limited scope — this enforces parameter provisos [12].

The premise represents a proof state with n subgoals, of which the ith is to be solved by assumption. Isabelle searches the subgoal’s context for an assumption θ_{j} that can solve it. For each unifier, the meta-inference returns an instantiated proof state from which the ith subgoal has been removed. Isabelle searches for a unifying assumption; for readability and robustness, proofs do not refer to assumptions by number.

Consider the proof state

([[P(a); P(b)]] ⟹ P(?x)) ⟹ Q(?x).

Proof by assumption (with i = 1, the only possibility) yields two results:

• Q(a), instantiating ?x ≡ a

• Q(b), instantiating ?x ≡ b

Here, proof by assumption affects the main goal. It could also affect other subgoals; if we also had the subgoal [[P(b); P(c)]] ⟹ P(?x), then ?x ≡ a would transform it to [[P(b); P(c)]] ⟹ P(a), which might be unprovable.

5.3 A propositional proof

Our first example avoids quantifiers. Given the main goal P ∨ P → P, Isabelle creates the initial state

(P ∨ P → P) ⟹ (P ∨ P → P).

Bear in mind that every proof state we derive will be a meta-theorem, expressing that the subgoals imply the main goal. Our aim is to reach the state P ∨ P → P; this meta-theorem is the desired result.

The first step is to refine subgoal 1 by (→I ), creating a new state where P ∨P is an assumption:

(P ∨ P ⟹ P) ⟹ (P ∨ P → P)

The next step is (∨E), which replaces subgoal 1 by three new subgoals. Because of lifting, each subgoal contains a copy of the context — the assumption P ∨ P. (In fact, this assumption is now redundant; we shall shortly see how to get rid of it!) The new proof state is the following meta-theorem, laid out for clarity:

[[ P ∨ P ⟹ ?P_{1} ∨?Q_{1};  (subgoal 1)
[[P ∨ P; ?P_{1}]] ⟹ P;  (subgoal 2)
[[P ∨ P; ?Q_{1}]] ⟹ P  (subgoal 3)
]] ⟹ (P ∨ P → P)  (main goal)

Notice the unknowns in the proof state. Because we have applied (∨E), we must prove some disjunction, ?P_{1}∨?Q_{1}. Of course, subgoal 1 is provable by assumption. This instantiates both ?P_{1} and ?Q_{1} to P throughout the proof state:

[[ [[P ∨ P; P]] ⟹ P;  (subgoal 1)
[[P ∨ P; P]] ⟹ P  (subgoal 2)
]] ⟹ (P ∨ P → P)  (main goal)

Both of the remaining subgoals can be proved by assumption. After two such steps, the proof state is P ∨ P → P.

5.4 A quantifier proof

To illustrate quantifiers and ⋀-lifting, let us prove (∃x . P(f (x))) → (∃x . P(x)). The initial proof state is the trivial meta-theorem

(∃x . P(f (x))) → (∃x . P(x)) ⟹ (∃x . P(f (x))) → (∃x . P(x)).

As above, the first step is refinement by (→I ):

(∃x . P(f (x)) ⟹ ∃x . P(x)) ⟹ (∃x . P(f (x))) → (∃x . P(x))

The next step is (∃E), which replaces subgoal 1 by two new subgoals. Both have the assumption ∃x . P(f (x)). The new proof state is the meta-theorem

[[ ∃x . P(f (x)) ⟹ ∃x .?P_{1}(x);  (subgoal 1)
⋀ x . [[∃x . P(f (x)); ?P_{1}(x)]] ⟹ ∃x . P(x)  (subgoal 2)
]] ⟹ (∃x . P(f (x))) → (∃x . P(x))  (main goal)

The unknown ?P_{1} appears in both subgoals. Because we have applied (∃E), we must prove ∃x .?P_{1}(x), where ?P_{1}(x) may become any formula possibly containing x. Proving subgoal 1 by assumption instantiates ?P_{1} to λx . P(f (x)):

(⋀ x . [[∃x . P(f (x)); P(f (x))]] ⟹ ∃x . P(x)) ⟹ (∃x . P(f (x))) → (∃x . P(x))

The next step is refinement by (∃I ). The rule is lifted into the context of the parameter x and the assumption P(f (x)). This copies the context to the subgoal and allows the existential witness to depend upon x:

(⋀ x . [[∃x . P(f (x)); P(f (x))]] ⟹ P(?x_{2}(x))) ⟹ (∃x . P(f (x))) → (∃x . P(x))

The existential witness, ?x_{2}(x), consists of an unknown applied to a parameter. Proof by assumption unifies λx . P(f (x)) with λx . P(?x_{2}(x)), instantiating ?x_{2} to f . The final proof state contains no subgoals: (∃x . P(f (x))) → (∃x . P(x)).

5.5 Tactics and tacticals

Tactics perform backward proof. Isabelle tactics differ from those of lcf, hol and Nuprl by operating on entire proof states, rather than on individual subgoals. An Isabelle tactic is a function that takes a proof state and returns a sequence (lazy list) of possible successor states. Lazy lists are coded in ML as functions, a standard technique [14]. Isabelle represents proof states by theorems.

Basic tactics execute the meta-rules described above, operating on a given subgoal. The resolution tactics take a list of rules and return next states for each combination of rule and unifier. The assumption tactic examines the subgoal’s assumptions and returns next states for each combination of assumption and unifier. Lazy lists are essential because higher-order resolution may return infinitely many unifiers. If there are no matching rules or assumptions then no next states are generated; a tactic application that returns an empty list is said to fail.

Sequences realize their full potential with tacticals — operators for combining tactics. Depth-first search, breadth-first search and best-first search (where a heuristic function selects the best state to explore) return their outcomes as a sequence. Isabelle provides such procedures in the form of tacticals. Simpler procedures can be expressed directly using the basic tacticals THEN, ORELSE and

REPEAT:

tac1 THEN tac2 is a tactic for sequential composition. Applied to a proof state, it returns all states reachable in two steps by applying tac1 followed by tac2.

tac1 ORELSE tac2 is a choice tactic. Applied to a state, it tries tac1 and returns the result if non-empty; otherwise, it uses tac2.

REPEAT tac is a repetition tactic. Applied to a state, it returns all states reachable by applying tac as long as possible — until it would fail.

For instance, this tactic repeatedly applies tac1 and tac2, giving tac1 priority:

                     REPEAT(tac1 ORELSE tac2)

6 Variations on resolution

In principle, resolution and proof by assumption suffice to prove all theorems. However, specialized forms of resolution are helpful for working with elimination rules. Elim-resolution applies an elimination rule to an assumption; destructresolution is similar, but applies a rule in a forward style.

The last part of the section shows how the techniques for proving theorems can also serve to derive rules.

6.1 Elim-resolution

Consider proving the theorem ((R ∨ R) ∨ R) ∨ R → R. By (→I ), we prove R from the assumption ((R ∨ R) ∨ R) ∨ R. Applying (∨E) to this assumption yields two subgoals, one that assumes R (and is therefore trivial) and one that assumes (R ∨ R) ∨ R. This subgoal admits another application of (∨E). Since natural deduction never discards assumptions, we eventually generate a subgoal containing much that is redundant:

[[((R ∨ R) ∨ R) ∨ R; (R ∨ R) ∨ R; R ∨ R; R]] ⟹ R.

In general, using (∨E) on the assumption P ∨ Q creates two new subgoals with the additional assumption P or Q. In these subgoals, P ∨ Q is redundant. Other elimination rules behave similarly. In first-order logic, only universally quantified assumptions are sometimes needed more than once — say, to prove P(f (f (a))) from the assumptions ∀x . P(x) → P(f (x)) and P(a).

Many logics can be formulated as sequent calculi that delete redundant assumptions after use. The rule (∨E) might become

Γ, P, Δ ⊢ Θ Γ, Q, Δ ⊢ Θ
Γ, P ∨ Q, Δ ⊢ Θ

∨-left

In backward proof, a goal containing P ∨ Q on the left of the ⊢ (that is, as an assumption) splits into two subgoals, replacing P ∨Q by P or Q. But the sequent calculus, with its explicit handling of assumptions, can be tiresome to use.

Elim-resolution is Isabelle’s way of getting sequent calculus behaviour from natural deduction rules. It lets an elimination rule consume an assumption. Elim-resolution combines two meta-theorems:

• a rule [[ψ_{1}; …; ψ_{m}]] ⟹ ψ

• a proof state [[ϕ_{1}; …; ϕ_{n}]] ⟹ ϕ

The rule must have at least one premise, thus m > 0. Write the rule’s lifted form as [[ψ′_{1}; …; ψ′_{m}]] ⟹ ψ′. Suppose we wish to change subgoal number i.

Ordinary resolution would attempt to reduce ϕ_{i}, replacing subgoal i by m new ones. Elim-resolution tries simultaneously to reduce ϕ_{i} and to solve ψ′_{1} by assumption; it returns a sequence of next states. Each of these replaces subgoal i by instances of ψ′_{2}, …, ψ′_{m} from which the selected assumption has been deleted. Suppose ϕ_{i} has the parameter x and assumptions θ_{1}, …, θ_{k}. Then ψ′_{1}, the rule’s first premise after lifting, will be ⋀ x . [[θ_{1}; …; θ_{k}]] ⟹ ψ_{1}^{x}. Elim-resolution tries to unify ψ′ ≡^{?} ϕ_{i} and λx . θ_{j} ≡^{?} λx . ψ_{1}^{x} simultaneously, for j = 1, …, k.

Let us redo the example from §5.3. The elimination rule is (∨E),

[[?P ∨?Q; ?P ⟹ ?R; ?Q ⟹ ?R]] ⟹ ?R

and the proof state is (P ∨ P ⟹ P) ⟹ (P ∨ P → P). The lifted rule is

[[ P ∨ P ⟹ ?P_{1} ∨?Q_{1};
[[P ∨ P; ?P_{1}]] ⟹ ?R_{1};
[[P ∨ P; ?Q_{1}]] ⟹ ?R_{1}
]] ⟹ (P ∨ P ⟹ ?R_{1})

Unification takes the simultaneous equations P ∨ P ≡^{?} ?P_{1} ∨ ?Q_{1} and ?R_{1} ≡^{?} P, yielding ?P_{1} ≡ ?Q_{1} ≡ ?R_{1} ≡ P. The new proof state is simply

[[P ⟹ P; P ⟹ P]] ⟹ (P ∨ P → P).

Elim-resolution’s simultaneous unification gives better control than ordinary resolution. Recall the substitution rule:

[[?t = ?u; ?P(?t)]] ⟹ ?P(?u)  (subst)

Unsuitable for ordinary resolution because ?P(?u) admits many unifiers, (subst) works well with elim-resolution. It deletes some assumption of the form x = y and replaces every y by x in the subgoal formula. The simultaneous unification instantiates ?u to y; if y is not an unknown, then ?P(y) can easily be unified with another formula.

In logical parlance, the premise containing the connective to be eliminated is called the major premise. Elim-resolution expects the major premise to come first. The order of the premises is significant in Isabelle.

6.2 Destruction rules

Looking back to Fig. 1, notice that there are two kinds of elimination rule. The rules (∧E1), (∧E2), (→E) and (∀E) extract the conclusion from the major premise. In Isabelle parlance, such rules are called destruction rules; they are readable and easy to use in forward proof. The rules (∨E), (⊥E) and (∃E) work by discharging assumptions; they support backward proof in a style reminiscent of the sequent calculus.

The latter style is the most general form of elimination rule. In natural deduction, there is no way to recast (∨E), (⊥E) or (∃E) as destruction rules. But we can write general elimination rules for ∧, → and ∀:

\begin{matrix}P ∧ Q & [P, Q] ; ⋮ . ; R \\ R \end{matrix} \begin{aligned}P → Q & & P & [Q] ⋮ . R \\ & R \end{aligned} \begin{matrix}∀x . P & [P[t/x]] ; ⋮ . ; Q \\ Q \end{matrix}

Because they are concise, destruction rules are simpler to derive than the corresponding elimination rules. To facilitate their use in backward proof, Isabelle provides a means of transforming a destruction rule such as

\begin{aligned}P_{1} & … & P_{m} \\ & Q \end{aligned} to the elimination rule \begin{aligned}P_{1} & … & P_{m} & [Q] ⋮ . R \\ & & R. \end{aligned}

Destruct-resolution combines this transformation with elim-resolution. It applies a destruction rule to some assumption of a subgoal. Given the rule above, it replaces the assumption P_{1} by Q, with new subgoals of showing instances of P_{2}, …, P_{m}. Destruct-resolution works forward from a subgoal’s assumptions. Ordinary resolution performs forward reasoning from theorems, as illustrated in §3.2.

6.3 Deriving rules by resolution

The meta-logic, itself a form of the predicate calculus, is defined by a system of natural deduction rules. Each theorem may depend upon meta-assumptions. The theorem that ϕ follows from the assumptions ϕ_{1}, …, ϕ_{n} is written

ϕ [ϕ_{1}, …, ϕ_{n}].

A more conventional notation might be ϕ_{1}, …, ϕ_{n} ⊢ ϕ, but Isabelle’s notation is more readable with large formulae.

Meta-level natural deduction provides a convenient mechanism for deriving new object-level rules. To derive the rule

\begin{aligned}θ_{1} & … & θ_{k} \\ & ϕ, \end{aligned}

assume the premises θ_{1}, …, θ_{k} at the meta-level. Then prove ϕ, possibly using these assumptions. Starting with a proof state ϕ ⟹ ϕ, assumptions may accumulate, reaching a final state such as

ϕ [θ_{1}, …, θ_{k}].

The meta-rule for ⟹ introduction discharges an assumption. Discharging them in the order θ_{k}, …, θ_{1} yields the meta-theorem [[θ_{1}; …; θ_{k}]] ⟹ ϕ, with no assumptions. This represents the desired rule. Let us derive the general ∧ elimination rule:

\begin{matrix}P ∧ Q & [P, Q] ; ⋮ . ; R \\ R \end{matrix}  (∧E)

We assume P ∧ Q and [[P; Q]] ⟹ R, and commence backward proof in the state R ⟹ R. Resolving this with the second assumption yields the state

[[P; Q]] ⟹ R [ [[P; Q]] ⟹ R ].

Resolving subgoals 1 and 2 with (∧E1) and (∧E2), respectively, yields the state

[[P ∧?Q_{1}; ?P_{2} ∧ Q]] ⟹ R [ [[P; Q]] ⟹ R ].

The unknowns ?Q_{1} and ?P_{2} arise from unconstrained subformulae in the premises of (∧E1) and (∧E2). Resolving both subgoals with the assumption P ∧ Q instantiates the unknowns to yield

R [ [[P; Q]] ⟹ R, P ∧ Q ].

The proof may use the meta-assumptions in any order, and as often as necessary; when finished, we discharge them in the correct order to obtain the desired form:

[[P ∧ Q; [[P; Q]] ⟹ R]] ⟹ R

We have derived the rule using free variables, which prevents their premature instantiation during the proof; we may now replace them by schematic variables.

! Schematic variables are not allowed in meta-assumptions, for a variety of reasons. Meta-assumptions remain fixed throughout a proof.

Part II

Getting Started with Isabelle

Let us consider how to perform simple proofs using Isabelle. At present, Isabelle’s user interface is ml. Proofs are conducted by applying certain ml functions, which update a stored proof state. Basically, all syntax must be expressed using plain ascii characters. There are also mechanisms built into Isabelle that support alternative syntaxes, for example using mathematical symbols from a special screen font. The meta-logic and major object-logics already provide such fancy output as an option.

Object-logics are built upon Pure Isabelle, which implements the meta-logic and provides certain fundamental data structures: types, terms, signatures, theorems and theories, tactics and tacticals. These data structures have the corresponding ml types typ, term, Sign.sg, thm, theory and tactic; tacticals have function types such as tactic->tactic. Isabelle users can operate on these data structures by writing ml programs.

7 Forward proof

This section describes the concrete syntax for types, terms and theorems, and demonstrates forward proof.

7.1 Lexical matters

An identifier is a string of letters, digits, underscores (_) and single quotes ('), beginning with a letter. Single quotes are regarded as primes; for instance x' is read as x′. Identifiers are separated by white space and special characters. Reserved words are identifiers that appear in Isabelle syntax definitions.

An Isabelle theory can declare symbols composed of special characters, such as =, ==, => and ==>. (The latter three are part of the syntax of the meta-logic.) Such symbols may be run together; thus if } and { are used for set brackets then {{a},{a,b}} is valid notation for a set of sets — but only if }} and {{ have not been declared as symbols! The parser resolves any ambiguity by taking the longest possible symbol that has been declared. Thus the string ==> is read as a single symbol. But = => is read as two symbols.

Identifiers that are not reserved words may serve as free variables or constants. A type identifier consists of an identifier prefixed by a prime, for example 'a and 'hello. Type identifiers stand for (free) type variables, which remain fixed during a proof.

An unknown (or type unknown) consists of a question mark, an identifier (or type identifier), and a subscript. The subscript, a non-negative integer, allows the renaming of unknowns prior to unification.^{1}

7.2 Syntax of types and terms

Classes are denoted by identifiers; the built-in class logic contains the ‘logical’ types. Sorts are lists of classes enclosed in braces } and {; singleton sorts may be abbreviated by dropping the braces.

Types are written with a syntax like ml’s. The built-in type prop is the type of propositions. Type variables can be constrained to particular classes or sorts,

for example 'a::term and ?'b::{ord, arith}.

ASCII Notation for Types

α::C α :: C class constraint
α::{C_{1}, …,C_{n}} α :: {C_{1}, …, C_{n}} sort constraint
σ => τ σ ⇒ τ function type
[σ_{1}, …,σ_{n}] => τ [σ_{1}, …, σ_{n}] ⇒ τ curried function type
(τ_{1}, …,τ_{n})tycon (τ_{1}, …, τ_{n})tycon type construction

Terms are those of the typed λ-calculus.

ASCII Notation for Terms

t::σ  t :: σ  type constraint
%x.t  λx . t  abstraction
%x_{1} … x_{n}.t  λx_{1} … x_{n} . t curried abstraction
t(u_{1}, …,u_{n}) t(u_{1}, …, u_{n}) curried application

The theorems and rules of an object-logic are represented by theorems in the meta-logic, which are expressed using meta-formulae. Since the meta-logic is higher-order, meta-formulae ϕ, ψ, θ, … are just terms of type prop.

ASCII Notation for Meta-Formulae

a == b  a ≡ b  meta-equality
a =?= b  a ≡^{?} b  flex-flex constraint
ϕ ==> ψ  ϕ ⟹ ψ  meta-implication
[|ϕ_{1}; …;ϕ_{n}|] ==> ψ [[ϕ_{1}; …; ϕ_{n}]] ⟹ ψ nested implication
!!x.ϕ  ⋀ x . ϕ  meta-quantification
!!x_{1} … x_{n}.ϕ  ⋀ x_{1} …. x_{n} . ϕ  nested quantification

Flex-flex constraints are meta-equalities arising from unification; they require special treatment. See §7.4.

1The subscript may appear after the identifier, separated by a dot; this prevents ambiguity when the identifier ends with a digit. Thus ?z6.0 has identifier "z6" and subscript 0, while ?a0.5 has identifier "a0" and subscript 5. If the identifier does not end with a digit, then no dot appears and a subscript of 0 is omitted; for example, ?hello has identifier "hello" and subscript zero, while ?z6 has identifier "z" and subscript 6. The same conventions apply to type unknowns. The question mark is not part of the identifier!

Most logics define the implicit coercion Trueprop from object-formulae to propositions. This could cause an ambiguity: in P ⟹ Q, do the variables P and Q stand for meta-formulae or object-formulae? If the latter, P ⟹ Q really abbreviates Trueprop(P) ⟹ Trueprop(Q). To prevent such ambiguities, Isabelle’s syntax does not allow a meta-formula to consist of a variable. Variables of type prop are seldom useful, but you can make a variable stand for a metaformula by prefixing it with the symbol PROP:

      PROP ?psi ==> PROP ?theta

Symbols of object-logics are typically rendered into ascii as follows:

True  ⊤  true
False  ⊥  false
P & Q  P ∧ Q  conjunction
P | Q  P ∨ Q  disjunction
~ P  ¬P  negation
P --> Q  P → Q implication
P <-> Q  P ↔ Q bi-implication
ALL x y z . P ∀x y z . P for all
EX x y z . P ∃x y z . P there exists

To illustrate the notation, consider two axioms for first-order logic:

[[P; Q]] ⟹ P ∧ Q  (∧I )
[[∃x . P(x); ⋀ x . P(x) → Q]] ⟹ Q  (∃E)

(∧I ) translates into ascii characters as

      [| ?P; ?Q |] ==> ?P & ?Q

The schematic variables let unification instantiate the rule. To avoid cluttering logic definitions with question marks, Isabelle converts any free variables in a rule to schematic variables; we normally declare (∧I ) as

      [| P; Q |] ==> P & Q

This variables convention agrees with the treatment of variables in goals. Free variables in a goal remain fixed throughout the proof. After the proof is finished, Isabelle converts them to scheme variables in the resulting theorem. Scheme variables in a goal may be replaced by terms during the proof, supporting answer extraction, program synthesis, and so forth.

For a final example, the rule (∃E) is rendered in ascii as

      [| EX x.P(x);  !!x. P(x) ==> Q |] ==> Q

7.3 Basic operations on theorems

Meta-level theorems have the ml type thm. They represent the theorems and inference rules of object-logics. Isabelle’s meta-logic is implemented using the lcf approach: each meta-level inference rule is represented by a function from theorems to theorems. Object-level rules are taken as axioms.

The main theorem printing commands are prth, prths and prthq. Of the other operations on theorems, most useful are RS and RSN, which perform resolution.

prth thm; pretty-prints thm at the terminal.

prths thms; pretty-prints thms, a list of theorems.

prthq thmq; pretty-prints thmq, a sequence of theorems; this is useful for inspecting the output of a tactic.

thm1 RS thm2 resolves the conclusion of thm1 with the first premise of thm2.

thm1 RSN (i, thm2) resolves the conclusion of thm1 with the ith premise of thm2.

standard thm puts thm into a standard format. It also renames schematic variables to have subscript zero, improving readability and reducing subscript growth.

The rules of a theory are normally bound to ml identifiers. Suppose we are running an Isabelle session containing theory FOL, natural deduction first-order logic.^{2} Let us try an example given in §3.2. We first print mp, which is the rule (→E), then resolve it with itself.

      prth mp;
        [| ?P --> ?Q; ?P |] ==> ?Q
        val it = "[| ?P --> ?Q; ?P |] ==> ?Q" : thm
      prth (mp RS mp);
        [| ?P1 --> ?P --> ?Q; ?P1; ?P |] ==> ?Q
        val it = "[| ?P1 --> ?P --> ?Q; ?P1; ?P |] ==> ?Q" : thm

User input appears in typewriter characters, and output appears in slanted typewriter characters. ml’s response val … is compiler-dependent and will sometimes be suppressed. This session illustrates two formats for the display of theorems. Isabelle’s top-level displays theorems as ml values, enclosed in quotes. Printing commands like prth omit the quotes and the surrounding val ...: thm. Ignoring their side-effects, the commands are identity functions.

2For a listing of the FOL rules and their ml names, turn to Isabelle’s Object-Logics.

To contrast RS with RSN, we resolve conjunct1, which stands for (∧E1), with mp.

      conjunct1 RS mp;
        val it = "[| (?P --> ?Q) & ?Q1; ?P |] ==> ?Q" : thm
      conjunct1 RSN (2,mp);
        val it = "[| ?P --> ?Q; ?P & ?Q1 |] ==> ?Q" : thm

These correspond to the following proofs:

{(P → Q) ∧ Q_{1} \atop P → Q} (∧E1) P Q (→E)

P → Q {P ∧ Q_{1} \atop P} (∧E1) Q

(→E)

Rules can be derived by pasting other rules together. Let us join spec, which stands for (∀E), with mp and conjunct1. In ml, the identifier it denotes the value just printed.

      spec;
        val it = "ALL x. ?P(x) ==> ?P(?x)" : thm
      it RS mp;
        val it = "[| ALL x. ?P3(x) --> ?Q2(x); ?P3(?x1) |] ==>
                  ?Q2(?x1)" : thm
      it RS conjunct1;
        val it = "[| ALL x. ?P4(x) --> ?P6(x) & ?Q5(x); ?P4(?x2) |] ==>
                  ?P6(?x2)" : thm
      standard it;
        val it = "[| ALL x. ?P(x) --> ?Pa(x) & ?Q(x); ?P(?x) |] ==>
                  ?Pa(?x)" : thm

By resolving (∀E) with (→E) and (∧E1), we have derived a destruction rule for formulae of the form ∀x . P(x) → (Q(x) ∧ R(x)). Used with destruct-resolution, such specialized rules provide a way of referring to particular assumptions.

7.4 *Flex-flex constraints

In higher-order unification, flex-flex equations are those where both sides begin with a function unknown, such as ?f (0) ≡^{?} ?g(0). They admit a trivial unifier, here ?f ≡ λx .?a and ?g ≡ λy .?a, where ?a is a new unknown. They admit many other unifiers, such as ?f ≡ λx . ?g(0) and {?f ≡ λx . x, ?g ≡ λx . 0}. Huet’s procedure does not enumerate the unifiers; instead, it retains flex-flex equations as constraints on future unifications. Flex-flex constraints occasionally become attached to a proof state; more frequently, they appear during use of RS and RSN:

      refl;
        val it = "?a = ?a" : thm
      exI;
        val it = "?P(?x) ==> EX x. ?P(x)" : thm
      refl RS exI;
        val it = "?a3(?x) =?= ?a2(?x) ==> EX x. ?a3(x) = ?a2(x)" : thm

Renaming variables, this is ∃x .?f (x) = ?g(x) with the constraint ?f (?u) ≡^{?} ?g(?u). Instances satisfying the constraint include ∃x . ?f (x) = ?f (x) and ∃x . x = ?u. Calling flexflex_rule removes all constraints by applying the trivial unifier:

      prthq (flexflex_rule it);
        EX x. ?a4 = ?a4

Isabelle simplifies flex-flex equations to eliminate redundant bound variables. In λx y .?f (k(y), x) ≡^{?} λx y .?g(y), there is no bound occurrence of x on the right side; thus, there will be none on the left in a common instance of these terms. Choosing a new variable ?h, Isabelle assigns ?f ≡ λu v.?h(u), simplifying the left side to λx y .?h(k(y)). Dropping x from the equation leaves λy .?h(k(y)) ≡^{?} λy .?g(y). By η-conversion, this simplifies to the assignment ?g ≡ λy.?h(k(y)).

! RS and RSN fail (by raising exception THM) unless the resolution delivers exactly

one resolvent. For multiple results, use RL and RLN, which operate on theorem lists. The following example uses read_instantiate to create an instance of refl containing no schematic variables.

      val reflk = read_instantiate [("a","k")] refl;
        val reflk = "k = k" : thm

A flex-flex constraint is no longer possible; resolution does not find a unique unifier:

      reflk RS exI;
        uncaught exception THM

Using RL this time, we discover that there are four unifiers, and four resolvents:

      [reflk] RL [exI];
        val it = ["EX x. x = x", "EX x. k = x",
                  "EX x. x = k", "EX x. k = k"] : thm list

8 Backward proof

Although RS and RSN are fine for simple forward reasoning, large proofs require tactics. Isabelle provides a suite of commands for conducting a backward proof using tactics.

8.1 The basic tactics

The tactics assume_tac, resolve_tac, eresolve_tac, and dresolve_tac suf-

fice for most single-step proofs. Although eresolve_tac and dresolve_tac are not strictly necessary, they simplify proofs involving elimination and destruction rules. All the tactics act on a subgoal designated by a positive integer i, failing if i is out of range. The resolution tactics try their list of theorems in left-to-right order.

assume_tac i is the tactic that attempts to solve subgoal i by assumption. Proof by assumption is not a trivial step; it can falsify other subgoals by instantiating shared variables. There may be several ways of solving the subgoal by assumption.

resolve_tac thms i is the basic resolution tactic, used for most proof steps. The thms represent object-rules, which are resolved against subgoal i of the proof state. For each rule, resolution forms next states by unifying the conclusion with the subgoal and inserting instantiated premises in its place. A rule can admit many higher-order unifiers. The tactic fails if none of the rules generates next states.

eresolve_tac thms i performs elim-resolution. Like resolve_tac thms i followed by assume_tac i, it applies a rule then solves its first premise by assumption. But eresolve_tac additionally deletes that assumption from any subgoals arising from the resolution.

dresolve_tac thms i performs destruct-resolution with the thms, as described in §6.2. It is useful for forward reasoning from the assumptions.

8.2 Commands for backward proof

Tactics are normally applied using the subgoal module, which maintains a proof state and manages the proof construction. It allows interactive backtracking through the proof space, going away to prove lemmas, etc.; of its many commands, most important are the following:

goal theory formula; begins a new proof, where theory is usually an ml identifier and the formula is written as an ml string.

by tactic; applies the tactic to the current proof state, raising an exception if the tactic fails.

undo(); reverts to the previous proof state. Undo can be repeated but cannot be undone. Do not omit the parentheses; typing undo; merely causes ml to echo the value of that function. result(); returns the theorem just proved, in a standard format. It fails if

unproved subgoals are left, etc.

qed name; is the usual way of ending a proof. It gets the theorem using result, stores it in Isabelle’s theorem database and binds it to an ml identifier.

The commands and tactics given above are cumbersome for interactive use. Although our examples will use the full commands, you may prefer Isabelle’s shortcuts:

       ba i;  abbreviates by (assume_tac i);
       br thm i;  abbreviates by (resolve_tac [thm] i);
       be thm i;  abbreviates by (eresolve_tac [thm] i);
       bd thm i;  abbreviates by (dresolve_tac [thm] i);

8.3 A trivial example in propositional logic

Directory FOL of the Isabelle distribution defines the theory of first-order logic. Let us try the example from §5.3, entering the goal P ∨ P → P in that theory.^{3}

      goal FOL.thy "P|P --> P";
        Level 0
        P | P --> P
        1. P | P --> P

Isabelle responds by printing the initial proof state, which has P ∨ P → P as the main goal and the only subgoal. The level of the state is the number of by commands that have been applied to reach it. We now use resolve_tac to apply the rule impI, or (→I ), to subgoal 1:

      by (resolve_tac [impI] 1);
        Level 1
        P | P --> P
        1. P | P ==> P

In the new proof state, subgoal 1 is P under the assumption P ∨ P. (The meta-implication ==> indicates assumptions.) We apply disjE, or (∨E), to that subgoal:

      by (resolve_tac [disjE] 1);
        Level 2
        P | P --> P
        1. P | P ==> ?P1 | ?Q1
        2. [| P | P; ?P1 |] ==> P
        3. [| P | P; ?Q1 |] ==> P

3To run these examples, see the file FOL/ex/intro.ML. The files README and Makefile on the directories Pure and FOL explain how to build first-order logic.

At Level 2 there are three subgoals, each provable by assumption. We deviate from §5.3 by tackling subgoal 3 first, using assume_tac. This affects subgoal 1, updating ?Q1 to P.

      by (assume_tac 3);
        Level 3
        P | P --> P
        1. P | P ==> ?P1 | P
        2. [| P | P; ?P1 |] ==> P

Next we tackle subgoal 2, instantiating ?P1 to P in subgoal 1.

      by (assume_tac 2);
        Level 4
        P | P --> P
        1. P | P ==> P | P

Lastly we prove the remaining subgoal by assumption:

      by (assume_tac 1);
        Level 5
        P | P --> P
        No subgoals!

Isabelle tells us that there are no longer any subgoals: the proof is complete. Calling qed stores the theorem.

      qed "mythm";
        val mythm = "?P | ?P --> ?P" : thm

Isabelle has replaced the free variable P by the scheme variable ?P. Free variables in the proof state remain fixed throughout the proof. Isabelle finally converts them to scheme variables so that the resulting theorem can be instantiated with any formula.

As an exercise, try doing the proof as in §5.3, observing how instantiations affect the proof state.

8.4 Part of a distributive law

To demonstrate the tactics eresolve_tac, dresolve_tac and the tactical REPEAT, let us prove part of the distributive law

(P ∧ Q) ∨ R ↔ (P ∨ R) ∧ (Q ∨ R).

We begin by stating the goal to Isabelle and applying (→I ) to it:

      goal FOL.thy "(P & Q) | R  --> (P | R)";
        Level 0
        P & Q | R --> P | R
         1. P & Q | R --> P | R

      by (resolve_tac [impI] 1);
        Level 1
        P & Q | R --> P | R
         1. P & Q | R ==> P | R

Previously we applied (∨E) using resolve_tac, but eresolve_tac deletes the assumption after use. The resulting proof state is simpler.

      by (eresolve_tac [disjE] 1);
        Level 2
        P & Q | R --> P | R
         1. P & Q ==> P | R
         2. R ==> P | R

Using dresolve_tac, we can apply (∧E1) to subgoal 1, replacing the assumption P ∧ Q by P. Normally we should apply the rule (∧E), given in §6.2. That is an elimination rule and requires eresolve_tac; it would replace P ∧ Q by the two assumptions P and Q. Because the present example does not need Q, we may

try out dresolve_tac.
      by (dresolve_tac [conjunct1] 1);
        Level 3
        P & Q | R --> P | R
         1. P ==> P | R
         2. R ==> P | R

The next two steps apply (∨I 1) and (∨I 2) in an obvious manner.

      by (resolve_tac [disjI1] 1);
        Level 4
        P & Q | R --> P | R
         1. P ==> P
         2. R ==> P | R
      by (resolve_tac [disjI2] 2);
        Level 5
        P & Q | R --> P | R
         1. P ==> P
         2. R ==> R

Two calls of assume_tac can finish the proof. The tactical REPEAT here expresses a tactic that calls assume_tac 1 as many times as possible. We can restrict attention to subgoal 1 because the other subgoals move up after subgoal 1 disappears.

      by (REPEAT (assume_tac 1));
        Level 6
        P & Q | R --> P | R
        No subgoals!

9 Quantifier reasoning

This section illustrates how Isabelle enforces quantifier provisos. Suppose that x, y and z are parameters of a subgoal. Quantifier rules create terms such as ?f (x, z), where ?f is a function unknown. Instantiating ?f to λx z . t has the effect of replacing ?f (x, z) by t, where the term t may contain free occurrences of x and z. On the other hand, no instantiation of ?f can replace ?f (x, z) by a term containing free occurrences of y, since parameters are bound variables.

9.1 Two quantifier proofs: a success and a failure

Let us contrast a proof of the theorem ∀x . ∃y . x = y with an attempted proof of the non-theorem ∃y . ∀x . x = y. The former proof succeeds, and the latter fails, because of the scope of quantified variables [12]. Unification helps even in these trivial proofs. In ∀x . ∃y . x = y the y that ‘exists’ is simply x, but we need never say so. This choice is forced by the reflexive law for equality, and happens automatically.

The successful proof. The proof of ∀x . ∃y . x = y demonstrates the introduction rules (∀I ) and (∃I ). We state the goal and apply (∀I ):

      goal FOL.thy "ALL x. EX y. x=y";
        Level 0
        ALL x. EX y. x = y
         1. ALL x. EX y. x = y
      by (resolve_tac [allI] 1);
        Level 1
        ALL x. EX y. x = y
         1. !!x. EX y. x = y

The variable x is no longer universally quantified, but is a parameter in the subgoal; thus, it is universally quantified at the meta-level. The subgoal must be proved for all possible values of x.

To remove the existential quantifier, we apply the rule (∃I ):

      by (resolve_tac [exI] 1);
        Level 2
        ALL x. EX y. x = y
         1. !!x. x = ?y1(x)

The bound variable y has become ?y1(x). This term consists of the function unknown ?y1 applied to the parameter x. Instances of ?y1(x) may or may not contain x. We resolve the subgoal with the reflexivity axiom.

      by (resolve_tac [refl] 1);
        Level 3
        ALL x. EX y. x = y
        No subgoals!

Let us consider what has happened in detail. The reflexivity axiom is lifted over x to become ⋀ x .?f (x) = ?f (x), which is unified with ⋀ x . x = ?y_{1}(x). The function unknowns ?f and ?y_{1} are both instantiated to the identity function, and x = ?y_{1}(x) collapses to x = x by β-reduction.

The unsuccessful proof. We state the goal ∃y . ∀x . x = y, which is not a theorem, and try (∃I ):

      goal FOL.thy "EX y. ALL x. x=y";
        Level 0
        EX y. ALL x. x = y
         1. EX y. ALL x. x = y
      by (resolve_tac [exI] 1);
        Level 1
        EX y. ALL x. x = y
         1. ALL x. x = ?y

The unknown ?y may be replaced by any term, but this can never introduce another bound occurrence of x. We now apply (∀I ):

      by (resolve_tac [allI] 1);
        Level 2
        EX y. ALL x. x = y
         1. !!x. x = ?y

Compare our position with the previous Level 2. Instead of ?y1(x) we have ?y, whose instances may not contain the bound variable x. The reflexivity axiom does not unify with subgoal 1.

      by (resolve_tac [refl] 1);
        by: tactic failed

There can be no proof of ∃y .∀x .x = y by the soundness of first-order logic. I have elsewhere proved the faithfulness of Isabelle’s encoding of first-order logic [12]; there could, of course, be faults in the implementation.

9.2 Nested quantifiers

Multiple quantifiers create complex terms. Proving

(∀x y . P(x, y)) → (∀z w . P(w, z))

9 QUANTIFIER REASONING 36

will demonstrate how parameters and unknowns develop. If they appear in the wrong order, the proof will fail.

This section concludes with a demonstration of REPEAT and ORELSE.

goal FOL.thy "(ALL x y.P(x,y))  -->  (ALL z w.P(w,z))";
Level 0
(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
 1. (ALL x y. P(x,y)) --> (ALL z w. P(w,z))
by (resolve_tac [impI] 1);
Level 1
(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
 1. ALL x y. P(x,y) ==> ALL z w. P(w,z)

The wrong approach. Using dresolve_tac, we apply the rule (∀E), bound to the ml identifier spec. Then we apply (∀I ).

by (dresolve_tac [spec] 1);
Level 2
(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
 1. ALL y. P(?x1,y) ==> ALL z w. P(w,z)
by (resolve_tac [allI] 1);
Level 3
(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
 1. !!z. ALL y. P(?x1,y) ==> ALL w. P(w,z)

The unknown ?x1 and the parameter z have appeared. We again apply (∀E) and (∀I ).

by (dresolve_tac [spec] 1);
Level 4
(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
 1. !!z. P(?x1,?y3(z)) ==> ALL w. P(w,z)
by (resolve_tac [allI] 1);
Level 5
(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
 1. !!z w. P(?x1,?y3(z)) ==> P(w,z)

The unknown ?y3 and the parameter w have appeared. Each unknown is applied to the parameters existing at the time of its creation; instances of ?x1 cannot contain z or w, while instances of ?y3(z) can only contain z. Due to the restriction on ?x1, proof by assumption will fail.

by (assume_tac 1);
by: tactic failed
uncaught exception ERROR

The right approach. To do this proof, the rules must be applied in the correct order. Parameters should be created before unknowns. The choplev command returns to an earlier stage of the proof; let us return to the result of applying (→I ):

      choplev 1;
        Level 1
        (ALL x y. P(x,y)) --> (ALL z w. P(w,z))
         1. ALL x y. P(x,y) ==> ALL z w. P(w,z)

Previously we made the mistake of applying (∀E) before (∀I ).

      by (resolve_tac [allI] 1);
        Level 2
        (ALL x y. P(x,y)) --> (ALL z w. P(w,z))
         1. !!z. ALL x y. P(x,y) ==> ALL w. P(w,z)
      by (resolve_tac [allI] 1);
        Level 3
        (ALL x y. P(x,y)) --> (ALL z w. P(w,z))
         1. !!z w. ALL x y. P(x,y) ==> P(w,z)

The parameters z and w have appeared. We now create the unknowns:

      by (dresolve_tac [spec] 1);
        Level 4
        (ALL x y. P(x,y)) --> (ALL z w. P(w,z))
         1. !!z w. ALL y. P(?x3(z,w),y) ==> P(w,z)
      by (dresolve_tac [spec] 1);
        Level 5
        (ALL x y. P(x,y)) --> (ALL z w. P(w,z))
         1. !!z w. P(?x3(z,w),?y4(z,w)) ==> P(w,z)

Both ?x3(z,w) and ?y4(z,w) could become any terms containing z and w:

      by (assume_tac 1);
        Level 6
        (ALL x y. P(x,y)) --> (ALL z w. P(w,z))
        No subgoals!

A one-step proof using tacticals. Repeated application of rules can be effective, but the rules should be attempted in the correct order. Let us return to the original goal using choplev:

      choplev 0;
        Level 0
        (ALL x y. P(x,y)) --> (ALL z w. P(w,z))
         1. (ALL x y. P(x,y)) --> (ALL z w. P(w,z))

As we have just seen, allI should be attempted before spec, while assume_tac generally can be attempted first. Such priorities can easily be expressed using ORELSE, and repeated using REPEAT.

      by (REPEAT (assume_tac 1 ORELSE resolve_tac [impI,allI] 1
           ORELSE dresolve_tac [spec] 1));
        Level 1
        (ALL x y. P(x,y)) --> (ALL z w. P(w,z))
        No subgoals!

9.3 A realistic quantifier proof

To see the practical use of parameters and unknowns, let us prove half of the equivalence

(∀x . P(x) → Q) ↔ ((∃x . P(x)) → Q).

We state the left-to-right half to Isabelle in the normal way. Since → is nested to the right, (→I ) can be applied twice; we use REPEAT:

      goal FOL.thy "(ALL x.P(x) --> Q) --> (EX x.P(x)) --> Q";
        Level 0
        (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q
         1. (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q
      by (REPEAT (resolve_tac [impI] 1));
        Level 1
        (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q
         1. [| ALL x. P(x) --> Q; EX x. P(x) |] ==> Q

We can eliminate the universal or the existential quantifier. The existential quantifier should be eliminated first, since this creates a parameter. The rule (∃E) is bound to the identifier exE.

      by (eresolve_tac [exE] 1);
        Level 2
        (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q
         1. !!x. [| ALL x. P(x) --> Q; P(x) |] ==> Q

The only possibility now is (∀E), a destruction rule. We use dresolve_tac, which discards the quantified assumption; it is only needed once.

      by (dresolve_tac [spec] 1);
        Level 3
        (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q
         1. !!x. [| P(x); P(?x3(x)) --> Q |] ==> Q

Because we applied (∃E) before (∀E), the unknown term ?x3(x) may depend upon the parameter x.

Although (→E) is a destruction rule, it works with eresolve_tac to perform backward chaining. This technique is frequently useful.

      by (eresolve_tac [mp] 1);
        Level 4
        (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q
         1. !!x. P(x) ==> P(?x3(x))

The tactic has reduced Q to P(?x3(x)), deleting the implication. The final step is trivial, thanks to the occurrence of x.

      by (assume_tac 1);
        Level 5
        (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q
        No subgoals!

9.4 The classical reasoner

Although Isabelle cannot compete with fully automatic theorem provers, it provides enough automation to tackle substantial examples. The classical reasoner can be set up for any classical natural deduction logic; see the Reference Manual.

Rules are packaged into classical sets. The classical reasoner provides several tactics, which apply rules using naive algorithms. Unification handles quantifiers as shown above. The most useful tactic is Blast_tac.

Let us solve problems 40 and 60 of Pelletier [16]. (The backslashes \… \ are an ml string escape sequence, to break the long string over two lines.)

      goal FOL.thy "(EX y. ALL x. J(y,x) <-> ~J(x,x))  \
      \       -->  ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))";
        Level 0
        (EX y. ALL x. J(y,x) <-> ~J(x,x)) -->
        ~(ALL x. EX y. ALL z. J(z,y) <-> ~J(z,x))
         1. (EX y. ALL x. J(y,x) <-> ~J(x,x)) -->
            ~(ALL x. EX y. ALL z. J(z,y) <-> ~J(z,x))

Blast_tac proves subgoal 1 at a stroke.

      by (Blast_tac 1);
        Depth = 0
        Depth = 1
        Level 1
        (EX y. ALL x. J(y,x) <-> ~J(x,x)) -->
        ~(ALL x. EX y. ALL z. J(z,y) <-> ~J(z,x))
        No subgoals!

Sceptics may examine the proof by calling the package’s single-step tactics, such as step_tac. This would take up much space, however, so let us proceed to the next example:

      goal FOL.thy "ALL x. P(x,f(x)) <-> \
      \       (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))";
        Level 0
        ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))
         1. ALL x. P(x,f(x)) <->
            (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))

Again, subgoal 1 succumbs immediately.

      by (Blast_tac 1);
        Depth = 0
        Depth = 1
        Level 1
        ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))
        No subgoals!

The classical reasoner is not restricted to the usual logical connectives. The natural deduction rules for unions and intersections resemble those for disjunction and conjunction. The rules for infinite unions and intersections resemble those for quantifiers. Given such rules, the classical reasoner is effective for reasoning in set theory.

Part III

Advanced Methods

Before continuing, it might be wise to try some of your own examples in Isabelle, reinforcing your knowledge of the basic functions.

Look through Isabelle’s Object-Logics and try proving some simple theorems. You probably should begin with first-order logic (FOL or LK). Try working some of the examples provided, and others from the literature. Set theory (ZF) and Constructive Type Theory (CTT) form a richer world for mathematical reasoning and, again, many examples are in the literature. Higher-order logic (HOL) is Isabelle’s most elaborate logic. Its types and functions are identified with those of the meta-logic.

Choose a logic that you already understand. Isabelle is a proof tool, not a teaching tool; if you do not know how to do a particular proof on paper, then you certainly will not be able to do it on the machine. Even experienced users plan large proofs on paper.

We have covered only the bare essentials of Isabelle, but enough to perform substantial proofs. By occasionally dipping into the Reference Manual, you can learn additional tactics, subgoal commands and tacticals.

10 Deriving rules in Isabelle

A mathematical development goes through a progression of stages. Each stage defines some concepts and derives rules about them. We shall see how to derive rules, perhaps involving definitions, using Isabelle. The following section will explain how to declare types, constants, rules and definitions.

10.1 Deriving a rule using tactics and meta-level assumptions

The subgoal module supports the derivation of rules, as discussed in §6.3. The goal command, when supplied a goal of the form [[θ_{1}; …; θ_{k}]] ⟹ ϕ, creates ϕ ⟹ ϕ as the initial proof state and returns a list consisting of the theorems θ_{i} [θ_{i}], for i = 1, …, k. These meta-assumptions are also recorded internally, allowing result (which is called by qed) to discharge them in the original order.

Let us derive ∧ elimination using Isabelle. Until now, calling goal has returned an empty list, which we have thrown away. In this example, the list contains the two premises of the rule. We bind them to the ml identifiers major 10 DERIVING RULES IN ISABELLE 42

and minor:^{4}
val [major,minor] = goal FOL.thy
  "[| P&Q;  [| P; Q |] ==> R |] ==> R";
Level 0
R
 1. R
val major = "P & Q  [P & Q]" : thm
val minor = "[| P; Q |] ==> R  [[| P; Q |] ==> R]" : thm

Look at the minor premise, recalling that meta-level assumptions are shown in brackets. Using minor, we reduce R to the subgoals P and Q:

by (resolve_tac [minor] 1);
Level 1
R
 1. P
 2. Q

Deviating from §6.3, we apply (∧E1) forwards from the assumption P ∧ Q to obtain the theorem P [P ∧ Q].

major RS conjunct1;
val it = "P  [P & Q]" : thm
by (resolve_tac [major RS conjunct1] 1);
Level 2
R
 1. Q

Similarly, we solve the subgoal involving Q.

major RS conjunct2;
val it = "Q  [P & Q]" : thm
by (resolve_tac [major RS conjunct2] 1);
Level 3
R
No subgoals!

Calling topthm returns the current proof state as a theorem. Note that it contains assumptions. Calling qed discharges the assumptions — both occurrences of P ∧ Q are discharged as one — and makes the variables schematic.

topthm();
val it = "R  [P & Q, P & Q, [| P; Q |] ==> R]" : thm
qed "conjE";
val conjE = "[| ?P & ?Q; [| ?P; ?Q |] ==> ?R |] ==> ?R" : thm

4Some ML compilers will print a message such as binding not exhaustive. This warns that goal must return a 2-element list. Otherwise, the pattern-match will fail; ML will raise excep-

tion Match.

10.2 Definitions and derived rules

Definitions are expressed as meta-level equalities. Let us define negation and the if-and-only-if connective:

¬?P ≡ ?P → ⊥
?P ↔ ?Q ≡ (?P → ?Q) ∧ (?Q → ?P)

Isabelle permits meta-level rewriting using definitions such as these. Unfolding replaces every instance of ¬?P by the corresponding instance of ?P → ⊥. For example, ∀x . ¬(P(x) ∧ ¬R(x, 0)) unfolds to

∀x . (P(x) ∧ R(x, 0) → ⊥) → ⊥.

Folding a definition replaces occurrences of the right-hand side by the left. The occurrences need not be free in the entire formula.

When you define new concepts, you should derive rules asserting their abstract properties, and then forget their definitions. This supports modularity: if you later change the definitions without affecting their abstract properties, then most of your proofs will carry through without change. Indiscriminate unfolding makes a subgoal grow exponentially, becoming unreadable.

Taking this point of view, Isabelle does not unfold definitions automatically during proofs. Rewriting must be explicit and selective. Isabelle provides tactics and meta-rules for rewriting, and a version of the goal command that unfolds the conclusion and premises of the rule being derived.

For example, the intuitionistic definition of negation given above may seem peculiar. Using Isabelle, we shall derive pleasanter negation rules:

[P] ⋮ . ; ⊥ ; ¬P (¬I ) \begin{matrix}¬P & P \\ Q \end{matrix} (¬E)

This requires proving the following meta-formulae:

(P ⟹ ⊥) ⟹ ¬P  (¬I )
[[¬P; P]] ⟹ Q.  (¬E)

10.3 Deriving the ¬ introduction rule

To derive (¬I ), we may call goal with the appropriate formula. Again, goal returns a list consisting of the rule’s premises. We bind this one-element list to 10 DERIVING RULES IN ISABELLE 44

the ml identifier prems.

val prems = goal FOL.thy "(P ==> False) ==> ~P";
Level 0
~P
 1. ~P
val prems = ["P ==> False  [P ==> False]"] : thm list

Calling rewrite_goals_tac with not_def, which is the definition of negation, unfolds that definition in the subgoals. It leaves the main goal alone.

not_def;
val it = "~?P == ?P --> False" : thm
by (rewrite_goals_tac [not_def]);
Level 1
~P
 1. P --> False

Using impI and the premise, we reduce subgoal 1 to a triviality:

by (resolve_tac [impI] 1);
Level 2
~P
 1. P ==> False
by (resolve_tac prems 1);
Level 3
~P
 1. P ==> P

The rest of the proof is routine. Note the form of the final result.

by (assume_tac 1);
Level 4
~P
No subgoals!
qed "notI";
val notI = "(?P ==> False) ==> ~?P" : thm

There is a simpler way of conducting this proof. The goalw command starts a backward proof, as does goal, but it also unfolds definitions. Thus there is no

need to call rewrite_goals_tac:
val prems = goalw FOL.thy [not_def]
  "(P ==> False) ==> ~P";
Level 0
~P
 1. P --> False
val prems = ["P ==> False  [P ==> False]"] : thm list

10.4 Deriving the ¬ elimination rule

Let us derive the rule (¬E). The proof follows that of conjE above, with an additional step to unfold negation in the major premise. Although the goalw command is best for this, let us try goal to see another way of unfolding definitions. After binding the premises to ml identifiers, we apply FalseE:

      val [major,minor] = goal FOL.thy "[| ~P;  P |] ==> R";
        Level 0
        R
         1. R
        val major = "~ P  [~ P]" : thm
        val minor = "P  [P]" : thm
      by (resolve_tac [FalseE] 1);
        Level 1
        R
         1. False

Everything follows from falsity. And we can prove falsity using the premises and Modus Ponens:

      by (resolve_tac [mp] 1);
        Level 2
        R
         1. ?P1 --> False
         2. ?P1

For subgoal 1, we transform the major premise from ¬P to P → ⊥. The function rewrite_rule, given a list of definitions, unfolds them in a theorem. Rewriting does not affect the theorem’s hypothesis, which remains ¬P:

      rewrite_rule [not_def] major;
        val it = "P --> False  [~P]" : thm
      by (resolve_tac [it] 1);
        Level 3
        R
         1. P

The subgoal ?P1 has been instantiated to P, which we can prove using the minor premise:

      by (resolve_tac [minor] 1);
        Level 4
        R
        No subgoals!
      qed "notE";
        val notE = "[| ~?P; ?P |] ==> ?R" : thm

Again, there is a simpler way of conducting this proof. Recall that the goalw command unfolds definitions the conclusion; it also unfolds definitions in the premises:

      val [major,minor] = goalw FOL.thy [not_def]
          "[| ~P;  P |] ==> R";
        val major = "P --> False  [~ P]" : thm
        val minor = "P  [P]" : thm

Observe the difference in major; the premises are unfolded without calling rewrite_rule. Incidentally, the four calls to resolve_tac above can be collapsed to one, with the help of RS; this is a typical example of forward reasoning from a complex premise.

      minor RS (major RS mp RS FalseE);
        val it = "?P  [P, ~P]" : thm
      by (resolve_tac [it] 1);
        Level 1
        R
        No subgoals!

Finally, here is a trick that is sometimes useful. If the goal has an outermost meta-quantifier, then goal and goalw do not return the rule’s premises in the list of theorems; instead, the premises become assumptions in subgoal 1.

      goalw FOL.thy [not_def] "!!P R. [| ~P;  P |] ==> R";
        Level 0
        !!P R. [| ~ P; P |] ==> R
         1. !!P R. [| P --> False; P |] ==> R
      val it = [] : thm list

The proof continues as before. But instead of referring to ml identifiers, we refer

to assumptions using eresolve_tac or assume_tac:
      by (resolve_tac [FalseE] 1);
        Level 1
        !!P R. [| ~ P; P |] ==> R
         1. !!P R. [| P --> False; P |] ==> False
      by (eresolve_tac [mp] 1);
        Level 2
        !!P R. [| ~ P; P |] ==> R
         1. !!P R. P ==> P
      by (assume_tac 1);
        Level 3
        !!P R. [| ~ P; P |] ==> R
        No subgoals!

Calling qed strips the meta-quantifiers, so the resulting theorem is the same as before.

      qed "notE";
        val notE = "[| ~?P; ?P |] ==> ?R" : thm

Do not use the !! trick if the premises contain meta-level connectives, because eresolve_tac and assume_tac would not be able to handle the resulting assumptions. The trick is not suitable for deriving the introduction rule (¬I ).

11 Defining theories

Isabelle makes no distinction between simple extensions of a logic — like specifying a type bool with constants true and false — and defining an entire logic. A theory definition has a form like

T = S_{1} + ⋯ + S_{n} +

classes class declarations

      default  sort

types type declarations and synonyms arities type arity declarations consts constant declarations syntax syntactic constant declarations translations ast translation rules defs meta-logical definitions rules rule declarations

      end

ML ML code

This declares the theory T to extend the existing theories S_{1}, …, S_{n}. It may introduce new classes, types, arities (of existing types), constants and rules; it can specify the default sort for type variables. A constant declaration can specify an associated concrete syntax. The translations section specifies rewrite rules on abstract syntax trees, handling notations and abbreviations. The ML section may contain code to perform arbitrary syntactic transformations. The main declaration forms are discussed below. There are some more sections not presented here, the full syntax can be found in an appendix of the Reference Manual. Also note that object-logics may add further theory sections, for example typedef,

datatype in HOL.

All the declaration parts can be omitted or repeated and may appear in any order, except that the ml section must be last (after the end keyword). In the simplest case, T is just the union of S_{1}, …, S_{n}. New theories always extend one or more other theories, inheriting their types, constants, syntax, etc. The theory Pure contains nothing but Isabelle’s meta-logic. The variant CPure offers the more usual higher-order function application syntax t u_{1} … u_{n} instead of t(u_{1}, …, u_{n}) in Pure.

Each theory definition must reside in a separate file, whose name is the theory’s with .thy appended. Calling use_thy"T " reads the definition from T.thy, writes a corresponding file of ml code .T.thy.ML, reads the latter file, and deletes it if no errors occurred. This declares the ml structure T , which contains a component thy denoting the new theory, a component for each rule, and everything declared in ML code.

Errors may arise during the translation to ml (say, a misspelled keyword) or during creation of the new theory (say, a type error in a rule). But if all goes well, use_thy will finally read the file T.ML (if it exists). This file typically contains proofs that refer to the components of T . The structure is automatically opened, so its components may be referred to by unqualified names, e.g. just thy instead

of T .thy.

use_thy automatically loads a theory’s parents before loading the theory itself. When a theory file is modified, many theories may have to be reloaded. Isabelle records the modification times and dependencies of theory files. See the Reference Manual for more details.

11.1 Declaring constants, definitions and rules

Most theories simply declare constants, definitions and rules. The constant declaration part has the form

      consts c_{1} :: τ_{1}

⋮
c_{n} :: τ_{n}

where c_{1}, …, c_{n} are constants and τ_{1}, …, τ_{n} are types. The types must be enclosed in quotation marks if they contain user-declared infix type constructors like *. Each constant must be enclosed in quotation marks unless it is a valid identifier. To declare c_{1}, …, c_{n} as constants of type τ, the n declarations may be abbreviated to a single line:

              c_{1}, ..., c_{n} :: τ

The rule declaration part has the form

rules id_{1} "rule_{1}"

⋮

id_{n} "rule_{n}"

where id_{1}, …, id_{n} are ml identifiers and rule_{1}, …, rule_{n} are expressions of type prop. Each rule must be enclosed in quotation marks.

The definition part is similar, but with the keyword defs instead of rules. Definitions are rules of the form s ≡ t, and should serve only as abbreviations. The simplest form of a definition is f ≡ t, where f is a constant. Also allowed are η-equivalent forms of this, where the arguments of f appear applied on the left-hand side of the equation instead of abstracted on the right-hand side.

Isabelle checks for common errors in definitions, such as extra variables on the right-hand side, but currently does not a complete test of well-formedness. Thus determined users can write non-conservative ‘definitions’ by using mutual recursion, for example; the consequences of such actions are their responsibility.

This example theory extends first-order logic by declaring and defining two constants, nand and xor:

      Gate = FOL +
      consts  nand,xor :: [o,o] => o
      defs    nand_def "nand(P,Q) == ~(P & Q)"
              xor_def  "xor(P,Q)  == P & ~Q | ~P & Q"
      end

Declaring and defining constants can be combined:

      Gate = FOL +
      constdefs  nand :: [o,o] => o
                 "nand(P,Q) == ~(P & Q)"
                 xor  :: [o,o] => o
                 "xor(P,Q)  == P & ~Q | ~P & Q"
      end

constdefs generates the names nand_def and xor_def automatically, which is why it is restricted to alphanumeric identifiers. In general it has the form

      constdefs id_{1} :: τ_{1}

"id_{1} ≡ …"
⋮
id_{n} :: τ_{n}
"id_{n} ≡ …"

! A common mistake when writing definitions is to introduce extra free variables on the right-hand side as in the following fictitious definition:

      defs  prime_def "prime(p) == (m divides p) --> (m=1 | m=p)"

Isabelle rejects this “definition” because of the extra m on the right-hand side, which would introduce an inconsistency. What you should have written is

      defs  prime_def "prime(p) == ALL m. (m divides p) --> (m=1 | m=p)"

11.2 Declaring type constructors

Types are composed of type variables and type constructors. Each type constructor takes a fixed number of arguments. They are declared with an ml-like syntax. If list takes one type argument, tree takes two arguments and nat takes no arguments, then these type constructors can be declared by

      types 'a list
            ('a,'b) tree
            nat

The type declaration part has the general form

types tids_{1} id_{1} ⋮ tids_{n} id_{n}

where id_{1}, …, id_{n} are identifiers and tids_{1}, …, tids_{n} are type argument lists as shown in the example above. It declares each id_{i} as a type constructor with the specified number of argument places.

The arity declaration part has the form

arities tycon_{1} :: arity_{1} ⋮ tycon_{n} :: arity_{n}

where tycon_{1}, …, tycon_{n} are identifiers and arity_{1}, …, arity_{n} are arities. Arity declarations add arities to existing types; they do not declare the types themselves. In the simplest case, for an 0-place type constructor, an arity is simply the type’s class. Let us declare a type bool of class term, with constants tt and ff . (In first-order logic, booleans are distinct from formulae, which have type o :: logic.)

      Bool = FOL +
      types   bool
      arities bool    :: term
      consts  tt,ff   :: bool
      end

A k-place type constructor may have arities of the form (s_{1}, …, s_{k})c, where s_{1}, …, s_{n} are sorts and c is a class. Each sort specifies a type argument; it has the form {c_{1}, …, c_{m}}, where c_{1}, …, c_{m} are classes. Mostly we deal with singleton sorts, and may abbreviate them by dropping the braces. The arity (term)term is short for ({term})term. Recall the discussion in §1.2.

A type constructor may be overloaded (subject to certain conditions) by appearing in several arity declarations. For instance, the function type constructor fun has the arity (logic, logic)logic; in higher-order logic, it is declared also to have arity (term, term)term.

Theory List declares the 1-place type constructor list, gives it arity (term)term, and declares constants Nil and Cons with polymorphic types:^{5}

      List = FOL +
      types   'a list
      arities list    :: (term)term
      consts  Nil     :: 'a list
              Cons    :: ['a, 'a list] => 'a list
      end

Multiple arity declarations may be abbreviated to a single line:

arities tycon_{1}, ..., tycon_{n} :: arity

11.3 Type synonyms

Isabelle supports type synonyms (abbreviations) which are similar to those found in ml. Such synonyms are defined in the type declaration part and are fairly self explanatory:

      types gate       = [o,o] => o
            'a pred    = 'a => o
            ('a,'b)nuf = 'b => 'a

Type declarations and synonyms can be mixed arbitrarily:

      types nat
            'a stream = nat => 'a
            signal    = nat stream
            'a list

A synonym is merely an abbreviation for some existing type expression. Hence synonyms may not be recursive! Internally all synonyms are fully expanded. As a consequence Isabelle output never contains synonyms. Their main purpose is to improve the readability of theory definitions. Synonyms can be used just like any other type:

      consts and,or :: gate
             negate :: signal => signal

5In the consts part, type variable 'a has the default sort, which is term. See the Reference Manual for more information.

11.4 Infix and mixfix operators

Infix or mixfix syntax may be attached to constants. Consider the following theory:

      Gate2 = FOL +
      consts  "~&"     :: [o,o] => o         (infixl 35)
              "#"      :: [o,o] => o         (infixl 30)
      defs    nand_def "P ~& Q == ~(P & Q)"
              xor_def  "P # Q  == P & ~Q | ~P & Q"
      end

The constant declaration part declares two left-associating infix operators with their priorities, or precedences; they are ¬& of priority 35 and # of priority 30. Hence P # Q # R is parsed as (P # Q) # R and P # Q ¬& R as P # (Q ¬& R). Note the quotation marks in "~&" and "#".

The constants op ~& and op # are declared automatically, just as in ml. Hence you may write propositions like op #(True) == op ~&(True), which asserts that the functions λQ . True # Q and λQ . True ¬& Q are identical.

Infix syntax and constant names may be also specified independently. For example, consider this version of ¬&:

      consts  nand     :: [o,o] => o         (infixl "~&" 35)

Mixfix operators may have arbitrary context-free syntaxes. Let us add a line to the constant declaration part:

              If :: [o,o,o] => o       ("if _then _else _")

This declares a constant If of type [o, o, o] ⇒ o with concrete syntax if P then Q else R as well as If(P,Q,R). Underscores denote argument positions.

The declaration above does not allow the if-then-else construct to be printed split across several lines, even if it is too long to fit on one line. Pretty-printing information can be added to specify the layout of mixfix operators. For details, see the Reference Manual, chapter ‘Defining Logics’.

Mixfix declarations can be annotated with priorities, just like infixes. The example above is just a shorthand for

              If :: [o,o,o] => o       ("if _then _else _" [0,0,0] 1000)

The numeric components determine priorities. The list of integers defines, for each argument position, the minimal priority an expression at that position must have. The final integer is the priority of the construct itself. In the example above, any argument expression is acceptable because priorities are non-negative, and conditionals may appear everywhere because 1000 is the highest priority. On the other hand, the declaration

              If :: [o,o,o] => o       ("if _then _else _" [100,0,0] 99)

defines concrete syntax for a conditional whose first argument cannot have the form if P then Q else R because it must have a priority of at least 100. We may of course write

     if (if P then Q else R) then S else T

because expressions in parentheses have maximal priority.

Binary type constructors, like products and sums, may also be declared as infixes. The type declaration below introduces a type constructor ∗ with infix notation α ∗ β, together with the mixfix notation < , > for pairs. We also see a rule declaration part.

      Prod = FOL +
      types   ('a,'b) "*"                           (infixl 20)
      arities "*"     :: (term,term)term
      consts  fst     :: "'a * 'b => 'a"
              snd     :: "'a * 'b => 'b"
              Pair    :: "['a,'b] => 'a * 'b"       ("(1<_,/_>)")
      rules   fst     "fst(<a,b>) = a"
              snd     "snd(<a,b>) = b"
      end

! The name of the type constructor is * and not op *, as it would be in the case

of an infix constant. Only infix type constructors can have symbolic names like *. General mixfix syntax for types may be introduced via appropriate syntax declarations.

11.5 Overloading

The class declaration part has the form

      classes id_{1} < c_{1}

⋮

id_{n} < c_{n}

where id_{1}, …, id_{n} are identifiers and c_{1}, …, c_{n} are existing classes. It declares each id_{i} as a new class, a subclass of c_{i}. In the general case, an identifier may be declared to be a subclass of k existing classes:

              id < c_{1}, ..., c_{k}

Type classes allow constants to be overloaded. As suggested in §1.2, let us define the class arith of arithmetic types with the constants + :: [α, α] ⇒ α and 0, 1::α, for α::arith. We introduce arith as a subclass of term and add the three polymorphic constants of this class.

      Arith = FOL +
      classes arith < term
      consts  "0"     :: 'a::arith                  ("0")
              "1"     :: 'a::arith                  ("1")
              "+"     :: ['a::arith,'a] => 'a       (infixl 60)
      end

No rules are declared for these constants: we merely introduce their names without specifying properties. On the other hand, classes with rules make it possible to prove generic theorems. Such theorems hold for all instances, all types in that class.

We can now obtain distinct versions of the constants of arith by declaring certain types to be of class arith. For example, let us declare the 0-place type constructors bool and nat:

      BoolNat = Arith +
      types   bool  nat
      arities bool, nat   :: arith
      consts  Suc         :: nat=>nat
      rules   add0        "0 + n = n::nat"
              addS        "Suc(m)+n = Suc(m+n)"
              nat1        "1 = Suc(0)"
              or0l        "0 + x = x::bool"
              or0r        "x + 0 = x::bool"
              or1l        "1 + x = 1::bool"
              or1r        "x + 1 = 1::bool"
      end

Because nat and bool have class arith, we can use 0, 1 and + at either type. The type constraints in the axioms are vital. Without constraints, the x in 1 + x = x would have type α::arith and the axiom would hold for any type of class arith. This would collapse nat to a trivial type:

Suc(1) = Suc(0 + 1) = Suc(0) + 1 = 1 + 1 = 1!

12 Theory example: the natural numbers

We shall now work through a small example of formalized mathematics demonstrating many of the theory extension features.

12.1 Extending first-order logic with the natural numbers

Section 1 has formalized a first-order logic, including a type nat and the constants 0 :: nat and Suc :: nat ⇒ nat. Let us introduce the Peano axioms for mathematical induction and the freeness of 0 and Suc:

P[0/x] [P] ⋮ . ; P[Suc(x)/x] P[n/x] (induct)

provided x is not free in any assumption except P

Suc(m) = Suc(n) m = n (Suc inject) {Suc(m) = 0 \atop R} (Suc neq 0)

Mathematical induction asserts that P(n) is true, for any n :: nat, provided P(0) holds and that P(x) implies P(Suc(x)) for all x. Some authors express the induction step as ∀x . P(x) → P(Suc(x)). To avoid making induction require the presence of other connectives, we formalize mathematical induction as

[[P(0); ⋀ x . P(x) ⟹ P(Suc(x))]] ⟹ P(n).  (induct)

Similarly, to avoid expressing the other rules using ∀, → and ¬, we take advantage of the meta-logic;^{6} (Suc neq 0) is an elimination rule for Suc(m) = 0:

Suc(m) = Suc(n) ⟹ m = n  (Suc inject)
Suc(m) = 0 ⟹ R  (Suc neq 0)

We shall also define a primitive recursion operator, rec. Traditionally, primitive recursion takes a natural number a and a 2-place function f , and obeys the equations

rec(0, a, f ) = a
rec(Suc(m), a, f ) = f (m, rec(m, a, f ))

Addition, defined by m + n ≡ rec(m, n, λx y . Suc(y)), should satisfy

0 + n = n
Suc(m) + n = Suc(m + n)

Primitive recursion appears to pose difficulties: first-order logic has no functionvalued expressions. We again take advantage of the meta-logic, which does have functions. We also generalise primitive recursion to be polymorphic over any type of class term, and declare the addition function:

rec :: [nat, α::term, [nat, α] ⇒ α] ⇒ α
+ :: [nat, nat] ⇒ nat

6On the other hand, the axioms Suc(m) = Suc(n) ↔ m = n and ¬(Suc(m) = 0) are logically equivalent to those given, and work better with Isabelle’s simplifier.

12.2 Declaring the theory to Isabelle

Let us create the theory Nat starting from theory FOL, which contains only classical logic with no natural numbers. We declare the 0-place type constructor nat and the associated constants. Note that the constant 0 requires a mixfix annotation because 0 is not a legal identifier, and could not otherwise be written in terms:

      Nat = FOL +
      types   nat
      arities nat         :: term
      consts  "0"         :: nat                              ("0")
              Suc         :: nat=>nat
              rec         :: [nat, 'a, [nat,'a]=>'a] => 'a
              "+"         :: [nat, nat] => nat                (infixl 60)
      rules   Suc_inject  "Suc(m)=Suc(n) ==> m=n"
              Suc_neq_0   "Suc(m)=0      ==> R"
              induct      "[| P(0);  !!x. P(x) ==> P(Suc(x)) |]  ==> P(n)"
              rec_0       "rec(0,a,f) = a"
              rec_Suc     "rec(Suc(m), a, f) = f(m, rec(m,a,f))"
              add_def     "m+n == rec(m, n, %x y. Suc(y))"
      end

In axiom add_def, recall that % stands for λ. Loading this theory file creates the ml structure Nat, which contains the theory and axioms.

12.3 Proving some recursion equations

File FOL/ex/Nat.ML contains proofs involving this theory of the natural numbers. As a trivial example, let us derive recursion equations for +. Here is the zero case:

      goalw Nat.thy [add_def] "0+n = n";
        Level 0
        0 + n = n
         1. rec(0,n,%x y. Suc(y)) = n
      by (resolve_tac [rec_0] 1);
        Level 1
        0 + n = n
        No subgoals!
      qed "add_0";

And here is the successor case:

      goalw Nat.thy [add_def] "Suc(m)+n = Suc(m+n)";
        Level 0
        Suc(m) + n = Suc(m + n)
         1. rec(Suc(m),n,%x y. Suc(y)) = Suc(rec(m,n,%x y. Suc(y)))

      by (resolve_tac [rec_Suc] 1);
        Level 1
        Suc(m) + n = Suc(m + n)
        No subgoals!
      qed "add_Suc";

The induction rule raises some complications, which are discussed next.

13 Refinement with explicit instantiation

In order to employ mathematical induction, we need to refine a subgoal by the rule (induct). The conclusion of this rule is ?P(?n), which is highly ambiguous in higher-order unification. It matches every way that a formula can be regarded as depending on a subterm of type nat. To get round this problem, we could make the induction rule conclude ∀n . ?P(n) — but putting a subgoal into this form requires refinement by (∀E), which is equally hard!

The tactic res_inst_tac, like resolve_tac, refines a subgoal by a rule. But it also accepts explicit instantiations for the rule’s schematic variables.

res_inst_tac insts thm i instantiates the rule thm with the instantiations insts, and then performs resolution on subgoal i.

eres_inst_tac and dres_inst_tac are similar, but perform elim-resolution and destruct-resolution, respectively.

The list insts consists of pairs [(v_{1}, e_{1}), …, (v_{n}, e_{n})], where v_{1}, …, v_{n} are names of schematic variables in the rule — with no leading question marks! — and e_{1}, …, e_{n} are expressions giving their instantiations. The expressions are typechecked in the context of a particular subgoal: free variables receive the same types as they have in the subgoal, and parameters may appear. Type variable instantiations may appear in insts, but they are seldom required: res_inst_tac instantiates type variables automatically whenever the type of e_{i} is an instance of the type of ?v_{i}.

13.1 A simple proof by induction

Let us prove that no natural number k equals its own successor. To use (induct), we instantiate ?n to k; Isabelle finds a good instantiation for ?P.

      goal Nat.thy "~ (Suc(k) = k)";
        Level 0
        Suc(k) ~= k
         1. Suc(k) ~= k

      by (res_inst_tac [("n","k")] induct 1);
        Level 1
        Suc(k) ~= k
         1. Suc(0) ~= 0
         2. !!x. Suc(x) ~= x ==> Suc(Suc(x)) ~= Suc(x)

We should check that Isabelle has correctly applied induction. Subgoal 1 is the base case, with k replaced by 0. Subgoal 2 is the inductive step, with k replaced by Suc(x) and with an induction hypothesis for x. The rest of the proof demonstrates notI, notE and the other rules of theory Nat. The base case holds

by Suc_neq_0:
      by (resolve_tac [notI] 1);
        Level 2
        Suc(k) ~= k
         1. Suc(0) = 0 ==> False
         2. !!x. Suc(x) ~= x ==> Suc(Suc(x)) ~= Suc(x)
      by (eresolve_tac [Suc_neq_0] 1);
        Level 3
        Suc(k) ~= k
         1. !!x. Suc(x) ~= x ==> Suc(Suc(x)) ~= Suc(x)

The inductive step holds by the contrapositive of Suc_inject. Negation rules transform the subgoal into that of proving Suc(x) = x from Suc(Suc(x)) = Suc(x):

      by (resolve_tac [notI] 1);
        Level 4
        Suc(k) ~= k
         1. !!x. [| Suc(x) ~= x; Suc(Suc(x)) = Suc(x) |] ==> False
      by (eresolve_tac [notE] 1);
        Level 5
        Suc(k) ~= k
         1. !!x. Suc(Suc(x)) = Suc(x) ==> Suc(x) = x
      by (eresolve_tac [Suc_inject] 1);
        Level 6
        Suc(k) ~= k
        No subgoals!

13.2 An example of ambiguity in resolve_tac

If you try the example above, you may observe that res_inst_tac is not actually needed. Almost by chance, resolve_tac finds the right instantiation for (induct) to yield the desired next state. With more complex formulae, our luck fails.

      goal Nat.thy "(k+m)+n = k+(m+n)";
        Level 0
        k + m + n = k + (m + n)
         1. k + m + n = k + (m + n)
      by (resolve_tac [induct] 1);
        Level 1
        k + m + n = k + (m + n)
         1. k + m + n = 0
         2. !!x. k + m + n = x ==> k + m + n = Suc(x)

This proof requires induction on k. The occurrence of 0 in subgoal 1 indicates that induction has been applied to the term k +(m +n); this application is sound but will not lead to a proof here. Fortunately, Isabelle can (lazily!) generate all the valid applications of induction. The back command causes backtracking to an alternative outcome of the tactic.

      back();
        Level 1
        k + m + n = k + (m + n)
         1. k + m + n = k + 0
         2. !!x. k + m + n = k + x ==> k + m + n = k + Suc(x)

Now induction has been applied to m + n. This is equally useless. Let us call back again.

      back();
        Level 1
        k + m + n = k + (m + n)
         1. k + m + 0 = k + (m + 0)
         2. !!x. k + m + x = k + (m + x) ==>
                 k + m + Suc(x) = k + (m + Suc(x))

Now induction has been applied to n. What is the next alternative?

      back();
        Level 1
        k + m + n = k + (m + n)
         1. k + m + n = k + (m + 0)
         2. !!x. k + m + n = k + (m + x) ==> k + m + n = k + (m + Suc(x))

Inspecting subgoal 1 reveals that induction has been applied to just the second occurrence of n. This perfectly legitimate induction is useless here.

The main goal admits fourteen different applications of induction. The number is exponential in the size of the formula.

13.3 Proving that addition is associative

Let us invoke the induction rule properly, using res_inst_tac. At the same time, we shall have a glimpse at Isabelle’s simplification tactics, which are described in the Reference Manual.

Isabelle’s simplification tactics repeatedly apply equations to a subgoal, perhaps proving it. For efficiency, the rewrite rules must be packaged into a simplification set, or simpset. We augment the implicit simpset of FOL with the equations proved in the previous section, namely 0 + n = n and Suc(m) + n = Suc(m + n):

      Addsimps [add_0, add_Suc];

We state the goal for associativity of addition, and use res_inst_tac to invoke induction on k:

      goal Nat.thy "(k+m)+n = k+(m+n)";
        Level 0
        k + m + n = k + (m + n)
         1. k + m + n = k + (m + n)
      by (res_inst_tac [("n","k")] induct 1);
        Level 1
        k + m + n = k + (m + n)
         1. 0 + m + n = 0 + (m + n)
         2. !!x. x + m + n = x + (m + n) ==>
                 Suc(x) + m + n = Suc(x) + (m + n)

The base case holds easily; both sides reduce to m + n. The tactic Simp_tac rewrites with respect to the current simplification set, applying the rewrite rules for addition:

      by (Simp_tac 1);
        Level 2
        k + m + n = k + (m + n)
         1. !!x. x + m + n = x + (m + n) ==>
                 Suc(x) + m + n = Suc(x) + (m + n)

The inductive step requires rewriting by the equations for addition together the induction hypothesis, which is also an equation. The tactic Asm_simp_tac rewrites using the implicit simplification set and any useful assumptions:

      by (Asm_simp_tac 1);
        Level 3
        k + m + n = k + (m + n)
        No subgoals!

14 A Prolog interpreter

To demonstrate the power of tacticals, let us construct a Prolog interpreter and execute programs involving lists.^{7} The Prolog program consists of a theory. We declare a type constructor for lists, with an arity declaration to say that (τ)list is of class term provided τ is:

list :: (term)term

We declare four constants: the empty list Nil; the infix list constructor :; the list concatenation predicate app; the list reverse predicate rev. (In Prolog, functions on lists are expressed as predicates.)

Nil :: αlist
: :: [α, αlist] ⇒ αlist
app :: [αlist, αlist, αlist] ⇒ o
rev :: [αlist, αlist] ⇒ o

The predicate app should satisfy the Prolog-style rules

app(Nil, ys, ys)  \frac{app(xs, ys, zs)}{app(x : xs, ys, x : zs)}

We define the naive version of rev, which calls app:

rev(Nil, Nil)  \frac{rev(xs, ys) app(ys, x : Nil, zs)}{rev(x : xs, zs)}

Theory Prolog extends first-order logic in order to make use of the class term and the type o. The interpreter does not use the rules of FOL.

      Prolog = FOL +
      types   'a list
      arities list    :: (term)term
      consts  Nil     :: 'a list
              ":"     :: ['a, 'a list]=> 'a list            (infixr 60)
              app     :: ['a list, 'a list, 'a list] => o
              rev     :: ['a list, 'a list] => o
      rules   appNil  "app(Nil,ys,ys)"
              appCons "app(xs,ys,zs) ==> app(x:xs, ys, x:zs)"
              revNil  "rev(Nil,Nil)"
              revCons "[| rev(xs,ys); app(ys,x:Nil,zs) |] ==> rev(x:xs,zs)"
      end

7To run these examples, see the file FOL/ex/Prolog.ML.

14 A PROLOG INTERPRETER 62

14.1 Simple executions

Repeated application of the rules solves Prolog goals. Let us append the lists [a, b, c] and [d, e]. As the rules are applied, the answer builds up in ?x.

goal Prolog.thy "app(a:b:c:Nil, d:e:Nil, ?x)";
Level 0
app(a : b : c : Nil, d : e : Nil, ?x)
 1. app(a : b : c : Nil, d : e : Nil, ?x)
by (resolve_tac [appNil,appCons] 1);
Level 1
app(a : b : c : Nil, d : e : Nil, a : ?zs1)
 1. app(b : c : Nil, d : e : Nil, ?zs1)
by (resolve_tac [appNil,appCons] 1);
Level 2
app(a : b : c : Nil, d : e : Nil, a : b : ?zs2)
 1. app(c : Nil, d : e : Nil, ?zs2)

At this point, the first two elements of the result are a and b.

by (resolve_tac [appNil,appCons] 1);
Level 3
app(a : b : c : Nil, d : e : Nil, a : b : c : ?zs3)
 1. app(Nil, d : e : Nil, ?zs3)
by (resolve_tac [appNil,appCons] 1);
Level 4
app(a : b : c : Nil, d : e : Nil, a : b : c : d : e : Nil)
No subgoals!

Prolog can run functions backwards. Which list can be appended with [c, d] to produce [a, b, c, d]? Using REPEAT, we find the answer at once, [a, b]:

goal Prolog.thy "app(?x, c:d:Nil, a:b:c:d:Nil)";
Level 0
app(?x, c : d : Nil, a : b : c : d : Nil)
 1. app(?x, c : d : Nil, a : b : c : d : Nil)
by (REPEAT (resolve_tac [appNil,appCons] 1));
Level 1
app(a : b : Nil, c : d : Nil, a : b : c : d : Nil)
No subgoals!

14.2 Backtracking

Prolog backtracking can answer questions that have multiple solutions. Which lists x and y can be appended to form the list [a, b, c, d]? This question has five solutions. Using REPEAT to apply the rules, we quickly find the first solution, namely x = [] and y = [a, b, c, d]:

goal Prolog.thy "app(?x, ?y, a:b:c:d:Nil)";
Level 0
app(?x, ?y, a : b : c : d : Nil)
 1. app(?x, ?y, a : b : c : d : Nil)
by (REPEAT (resolve_tac [appNil,appCons] 1));
Level 1
app(Nil, a : b : c : d : Nil, a : b : c : d : Nil)
No subgoals!

Isabelle can lazily generate all the possibilities. The back command returns the tactic’s next outcome, namely x = [a] and y = [b, c, d]:

back();
Level 1
app(a : Nil, b : c : d : Nil, a : b : c : d : Nil)
No subgoals!

The other solutions are generated similarly.

back();
Level 1
app(a : b : Nil, c : d : Nil, a : b : c : d : Nil)
No subgoals!
back();
Level 1
app(a : b : c : Nil, d : Nil, a : b : c : d : Nil)
No subgoals!
back();
Level 1
app(a : b : c : d : Nil, Nil, a : b : c : d : Nil)
No subgoals!

14.3 Depth-first search

Now let us try rev, reversing a list. Bundle the rules together as the ml identifier rules. Naive reverse requires 120 inferences for this 14-element list, but the tactic terminates in a few seconds.

goal Prolog.thy "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)";
Level 0
rev(a : b : c : d : e : f : g : h : i : j : k : l : m : n : Nil, ?w)
 1. rev(a : b : c : d : e : f : g : h : i : j : k : l : m : n : Nil,
        ?w)
val rules = [appNil,appCons,revNil,revCons];

      by (REPEAT (resolve_tac rules 1));
        Level 1
        rev(a : b : c : d : e : f : g : h : i : j : k : l : m : n : Nil,
            n : m : l : k : j : i : h : g : f : e : d : c : b : a : Nil)
        No subgoals!

We may execute rev backwards. This, too, should reverse a list. What is the reverse of [a, b, c]?

      goal Prolog.thy "rev(?x, a:b:c:Nil)";
        Level 0
        rev(?x, a : b : c : Nil)
         1. rev(?x, a : b : c : Nil)
      by (REPEAT (resolve_tac rules 1));
        Level 1
        rev(?x1 : Nil, a : b : c : Nil)
         1. app(Nil, ?x1 : Nil, a : b : c : Nil)

The tactic has failed to find a solution! It reached a dead end at subgoal 1: there is no ?x_{1} such that [] appended with [?x_{1}] equals [a, b, c]. Backtracking explores other outcomes.

      back();
        Level 1
        rev(?x1 : a : Nil, a : b : c : Nil)
         1. app(Nil, ?x1 : Nil, b : c : Nil)

This too is a dead end, but the next outcome is successful.

      back();
        Level 1
        rev(c : b : a : Nil, a : b : c : Nil)
        No subgoals!

REPEAT goes wrong because it is only a repetition tactical, not a search tactical. REPEAT stops when it cannot continue, regardless of which state is reached. The tactical DEPTH_FIRST searches for a satisfactory state, as specified by an ml predicate. Below, has_fewer_prems specifies that the proof state should have no subgoals.

      val prolog_tac = DEPTH_FIRST (has_fewer_prems 1)
                                   (resolve_tac rules 1);

Since Prolog uses depth-first search, this tactic is a (slow!) Prolog interpreter. We return to the start of the proof using choplev, and apply prolog_tac:

choplev 0;
Level 0
rev(?x, a : b : c : Nil)
 1. rev(?x, a : b : c : Nil)
by (DEPTH_FIRST (has_fewer_prems 1) (resolve_tac rules 1));
Level 1
rev(c : b : a : Nil, a : b : c : Nil)
No subgoals!

Let us try prolog_tac on one more example, containing four unknowns:

goal Prolog.thy "rev(a:?x:c:?y:Nil, d:?z:b:?u)";
Level 0
rev(a : ?x : c : ?y : Nil, d : ?z : b : ?u)
 1. rev(a : ?x : c : ?y : Nil, d : ?z : b : ?u)
by prolog_tac;
Level 1
rev(a : b : c : d : Nil, d : c : b : a : Nil)
No subgoals!

Although Isabelle is much slower than a Prolog system, Isabelle tactics can exploit logic programming techniques.

REFERENCES 66

References

[1] Antony Galton. Logic for Information Technology. Wiley, 1990.

[2] M. J. C. Gordon and T. F. Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993.

[3] Michael J. C. Gordon, Robin Milner, and Christopher P. Wadsworth. Edinburgh LCF: A Mechanised Logic of Computation. LNCS 78. Springer, 1979.

[4] Paul Hudak and Joseph H. Fasel. A gentle introduction to Haskell. SIGPLAN Notices, 27(5), May 1992.

[5] Paul Hudak, Simon Peyton Jones, and Philip Wadler. Report on the programming language Haskell: A non-strict, purely functional language. SIGPLAN Notices, 27(5), May 1992. Version 1.2.

[6] G. P. Huet. A unification algorithm for typed λ-calculus. Theoretical Computer Science, 1:27–57, 1975.

[7] Dale Miller. Unification under a mixed prefix. Journal of Symbolic Computation, 14(4):321–358, 1992.

[8] Tobias Nipkow and Christian Prehofer. Type reconstruction for type classes. Journal of Functional Programming, 5(2):201–224, 1995.

[9] Bengt Nordström, Kent Petersson, and Jan Smith. Programming in Martin-Löf’s Type Theory. An Introduction. Oxford University Press, 1990.

[10] Lawrence C. Paulson. Natural deduction as higher-order resolution. Journal of Logic Programming, 3:237–258, 1986.

[11] Lawrence C. Paulson. Logic and Computation: Interactive proof with Cambridge LCF. Cambridge University Press, 1987.

[12] Lawrence C. Paulson. The foundation of a generic theorem prover. Journal of Automated Reasoning, 5(3):363–397, 1989.

[13] Lawrence C. Paulson. Isabelle: The next 700 theorem provers. In P. Odifreddi, editor, Logic and Computer Science, pages 361–386. Academic Press, 1990.

[14] Lawrence C. Paulson. ML for the Working Programmer. Cambridge University Press, 1991.

[15] Lawrence C. Paulson. Designing a theorem prover. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, pages 415–475. Oxford University Press, 1992.

[16] F. J. Pelletier. Seventy-five problems for testing automatic theorem provers. Journal of Automated Reasoning, 2:191–216, 1986. Errata, JAR 4 (1988), 235–236 and JAR 18 (1997), 135.

REFERENCES 67

[17] Steve Reeves and Michael Clarke. Logic for Computer Science. Addison-Wesley, 1990.

[18] Patrick Suppes. Axiomatic Set Theory. Dover, 1972.

[19] Larry Wos. Automated reasoning and Bledsoe’s dream for the field. In Robert S. Boyer, editor, Automated Reasoning: Essays in Honor of Woody Bledsoe, pages 297–342. Kluwer Academic Publishers, 1991.

Index

!! symbol, 25

in main goal, 46 % symbol, 25 :: symbol, 25 == symbol, 25 ==> symbol, 25 => symbol, 25 =?= symbol, 25 [ symbol, 25 [| symbol, 25 ] symbol, 25 { symbol, 25 } symbol, 25 |] symbol, 25

allI theorem, 37 arities

declaring, 4, 49

Asm_simp_tac, 60

assume_tac, 30, 32, 37, 47 assumptions

deleting, 20 discharge of, 7 lifting over, 14 of main goal, 41 use of, 16, 28

axioms Peano, 55

ba, 31 back, 59, 63 backtracking

Prolog style, 62 bd, 31 be, 31

Blast_tac, 39

br, 31 by, 30

choplev, 37, 65

classes, 3

built-in, 25 classical reasoner, 39 conjunct1 theorem, 28 constants, 3

clashes with variables, 9

declaring, 48 overloaded, 54 polymorphic, 3

CPure theory, 47

definitions, 6, 48

and derived rules, 43–46

                                       DEPTH_FIRST, 64

destruct-resolution, 22, 30

disjE theorem, 31

                                       dres_inst_tac, 57
                                       dresolve_tac, 30, 32, 33, 38

eigenvariables, see parameters elim-resolution, 20, 30 equality

polymorphic, 3

                                       eres_inst_tac, 57

eresolve_tac, 30, 32, 33, 39, 47 examples

of deriving rules, 41 of induction, 57, 58 of simplification, 60 of tacticals, 37 of theories, 48, 50–54, 56, 61 propositional, 17, 31, 32 with quantifiers, 18, 34, 35, 38

exE theorem, 38

FalseE theorem, 45 first-order logic, 1 flex-flex constraints, 6, 25, 28

                                       flexflex_rule, 29

forward proof, 21, 24–30

fun type, 1, 4

function applications, 1, 8

goal, 30, 41, 46 goalw, 44–46

                                       has_fewer_prems, 64

higher-order logic, 4

identifiers, 24 impI theorem, 31, 44 infixes, 52 instantiation, 57–60 Isabelle

object-logics supported, i overview, i release history, i

λ-abstractions, 1, 8, 25 λ-calculus, 1 LCF, i LCF system, 15, 27 level of a proof, 31 lifting, 14 logic class, 3, 6, 25

major premise, 21 Match exception, 42 meta-assumptions

syntax of, 22 meta-equality, 5, 25 meta-implication, 5, 7, 25 meta-quantifiers, 5, 8, 25 meta-rewriting, 43 mixfix declarations, 52, 53, 56 ML, i ML section, 47 mp theorem, 27, 28

Nat theory, 56 nat type, 3 not_def theorem, 44 notE theorem, 45, 58 notI theorem, 44, 58

o type, 3, 4

ORELSE, 38

overloading, 4, 53

parameters, 8, 34

lifting over, 15 Prolog theory, 61 Prolog interpreter, 61 proof state, 16 proofs

commands for, 30 PROP symbol, 26 prop type, 25, 26 prop type, 6

                                       prth, 27

prthq, 27, 29

                                       prths, 27

Pure theory, 47

qed, 31, 42, 46 quantifiers, 5, 8, 34

                                       read_instantiate, 29

refl theorem, 29 REPEAT, 33, 38, 62, 64

                                       res_inst_tac, 57, 60

reserved words, 24 resolution, 10, 12

in backward proof, 15 with instantiation, 57 resolve_tac, 30, 31, 46, 58

                                       result, 31
                                       rewrite_goals_tac, 44
                                       rewrite_rule, 45, 46

RL, 29

                                       RLN, 29

RS, 27, 29, 46 RSN, 27, 29 rules

declaring, 48

derived, 13, 22, 41, 43 destruction, 21 elimination, 21 propositional, 6 quantifier, 8

search

depth-first, 63 signatures, 9

                                       Simp_tac, 60

simplification, 60 simplification sets, 60 sort constraints, 25 sorts, 5 spec theorem, 28, 36, 37

standard, 27

substitution, 8

Suc_inject, 58
Suc_neq_0, 58

syntax of types and terms, 25

tacticals, 19, 37 tactics, 19

assumption, 30 resolution, 30

term class, 3 terms

syntax of, 1, 25 theorems

basic operations on, 27 printing of, 27

theories, 9

defining, 47–57 thm ML type, 27

topthm, 42

Trueprop constant, 6, 7, 25 type constraints, 25 type constructors, 1 type identifiers, 24 type synonyms, 51 types

declaring, 49 function, 1 higher, 5 polymorphic, 3 simple, 1 syntax of, 1, 25

undo, 30

unification higher-order, 11, 58 incompleteness of, 11

unknowns, 10, 24, 34

function, 11, 28, 34

use_thy, 47, 48

variables bound, 8