Chapter 4

Higher-Order Logic

The theory HOL implements higher-order logic. It is based on Gordon’s hol system [16], which itself is based on Church’s original paper [6]. Andrews’s book [2] is a full description of the original Church-style higher-order logic. Experience with the hol system has demonstrated that higher-order logic is widely applicable in many areas of mathematics and computer science, not just hardware verification, hol’s original raison d’être. It is weaker than ZF set theory but for most applications this does not matter. If you prefer ml to Lisp, you will probably prefer HOL to ZF.

The syntax of HOL^{1} follows λ-calculus and functional programming. Function application is curried. To apply the function f of type τ_{1} ⇒ τ_{2} ⇒ τ_{3} to the arguments a and b in HOL, you simply write f a b. There is no ‘apply’ operator as in ZF. Note that f (a, b) means “f applied to the pair (a, b)” in HOL. We write ordered pairs as (a, b), not ⟨a, b⟩ as in ZF.

HOL has a distinct feel, compared with ZF and CTT. It identifies object-level types with meta-level types, taking advantage of Isabelle’s built-in type checker. It identifies object-level functions with meta-level functions, so it uses Isabelle’s operations for abstraction and application.

These identifications allow Isabelle to support HOL particularly nicely, but they also mean that HOL requires more sophistication from the user — in particular, an understanding of Isabelle’s type system. Beginners should work with show_types

(or even show_sorts) set to true.

4.1 Syntax

Figure 4.1 lists the constants (including infixes and binders), while Fig. 4.2 presents the grammar of higher-order logic. Note that a~=b is translated to ¬(a = b).

! HOL has no if-and-only-if connective; logical equivalence is expressed using equality. But equality has a high priority, as befitting a relation, while if-and-only-if typically

1Earlier versions of Isabelle’s HOL used a different syntax. Ancient releases of Isabelle included still another version of HOL, with explicit type inference rules [39]. This version no longer exists, but ZF supports a similar style of reasoning.

CHAPTER 4. HIGHER-ORDER LOGIC 60

name  meta-type  description
Trueprop  bool ⇒ prop coercion to prop
Not  bool ⇒ bool  negation (¬)
True  bool  tautology (⊤)
False  bool  absurdity (⊥)
If [bool, α, α] ⇒ α  conditional
Let [α, α ⇒ β] ⇒ β  let binder

Constants

symbol name  meta-type  description
@    Eps  (α ⇒ bool) ⇒ α Hilbert description (ε)
! or ALL    All  (α ⇒ bool) ⇒ bool universal quantifier (∀)
? or EX     Ex  (α ⇒ bool) ⇒ bool existential quantifier (∃)
?! or EX! Ex1 (α ⇒ bool) ⇒ bool unique existence (∃!)
LEAST  Least (α :: ord ⇒ bool) ⇒ α  least element

Binders

symbol  meta-type priority  description
o [β ⇒ γ, α ⇒ β] ⇒ (α ⇒ γ) Left 55  composition (∘)
=  [α, α] ⇒ bool Left 50  equality (=)
<  [α :: ord, α] ⇒ bool Left 50  less than (<)
<=  [α :: ord, α] ⇒ bool Left 50 less than or equals (≤)
&  [bool, bool] ⇒ bool Right 35  conjunction (∧)
|  [bool, bool] ⇒ bool Right 30  disjunction (∨)
-->  [bool, bool] ⇒ bool Right 25  implication (→)

Infixes Figure 4.1: Syntax of HOL

term = expression of class term
| @ id . formula
| let id = term; …; id = term in term
| if formula then term else term
| LEAST id . formula
formula = expression of type bool
| term = term
| term ~= term
| term < term
| term <= term
| ~ formula
| formula & formula
| formula | formula
| formula --> formula
| ! id id^{∗} . formula | ALL id id^{∗} . formula
| ? id id^{∗} . formula | EX id id^{∗} . formula
| ?! id id^{∗} . formula | EX! id id^{∗} . formula

Figure 4.2: Full grammar for HOL

has the lowest priority. Thus, ¬¬P = P abbreviates ¬¬(P = P) and not (¬¬P) = P. When using = to mean logical equivalence, enclose both operands in parentheses.

4.1.1 Types and classes

The universal type class of higher-order terms is called term. By default, explicit type variables have class term. In particular the equality symbol and quantifiers are polymorphic over class term.

The type of formulae, bool, belongs to class term; thus, formulae are terms. The built-in type fun, which constructs function types, is overloaded with arity (term,term)term. Thus, σ ⇒ τ belongs to class term if σ and τ do, allowing quantification over functions.

HOL offers various methods for introducing new types. See §4.5 and §4.6. Theory Ord defines the syntactic class ord of order signatures; the relations

< and ≤ are polymorphic over this class, as are the functions mono, min and max, and the LEAST operator. Ord also defines a subclass order of ord which axiomatizes partially ordered types (w.r.t. ≤).

Three other syntactic type classes — plus, minus and times — permit overloading of the operators +, - and *. In particular, - is instantiated for set difference and subtraction on natural numbers.

If you state a goal containing overloaded functions, you may need to include type constraints. Type inference may otherwise make the goal more polymorphic than you intended, with confusing results. For example, the variables i, j and k in the goal i ≤ j ⟹ i ≤ j + k have type α :: {ord, plus}, although you may have expected them to have some numeric type, e.g. nat. Instead you should have stated the goal as (i :: nat) ≤ j ⟹ i ≤ j + k, which causes all three variables to have type nat.

! If resolution fails for no obvious reason, try setting show_types to true, causing

Isabelle to display types of terms. Possibly set show_sorts to true as well, causing Isabelle to display type classes and sorts.

Where function types are involved, Isabelle’s unification code does not guarantee to find instantiations for type variables automatically. Be prepared to use res_inst_tac instead of resolve_tac, possibly instantiating type variables. Setting Unify.trace_types to true causes Isabelle to report omitted search paths during unification.

4.1.2 Binders

Hilbert’s description operator εx . P[x] stands for some x satisfying P, if such exists. Since all terms in HOL denote something, a description is always meaningful, but we do not know its value unless P defines it uniquely. We may write descriptions as Eps(λx . P[x]) or use the syntax @x.P[x].

Existential quantification is defined by

∃x . P x ≡ P(εx . P x).

The unique existence quantifier, ∃!x .P, is defined in terms of ∃ and ∀. An Isabelle binder, it admits nested quantifications. For instance, ∃!x y . P x y abbreviates ∃!x .∃!y .P x y; note that this does not mean that there exists a unique pair (x, y) satisfying P x y.

Quantifiers have two notations. As in Gordon’s hol system, HOL uses ! and ? to stand for ∀ and ∃. The existential quantifier must be followed by a space; thus ?x is an unknown, while ? x.f x=y is a quantification. Isabelle’s usual notation for quantifiers, ALL and EX, is also available. Both notations are accepted for input. The ml reference HOL_quantifiers governs the output notation. If set to true, then ! and ? are displayed; this is the default. If set to false, then ALL and EX are displayed.

If τ is a type of class ord, P a formula and x a variable of type τ, then the term LEAST x . P[x] is defined to be the least (w.r.t. ≤) x such that P x holds (see Fig. 4.4). The definition uses Hilbert’s ε choice operator, so Least is always meaningful, but may yield nothing useful in case there is not a unique

      refl           t = (t::'a)
      subst          [| s = t; P s |] ==> P (t::'a)
      ext            (!!x::'a. (f x :: 'b) = g x) ==> (%x.f x) = (%x.g x)
      impI           (P ==> Q) ==> P-->Q
      mp             [| P-->Q;  P |] ==> Q
      iff            (P-->Q) --> (Q-->P) --> (P=Q)
      selectI        P(x::'a) ==> P(@x.P x)
      True_or_False  (P=True) | (P=False)

Figure 4.3: The HOL rules

least element satisfying P.^{2}

All these binders have priority 10.

! The low priority of binders means that they need to be enclosed in parenthesis when

they occur in the context of other operations. For example, instead of P ∧ ∀x . Q you need to write P ∧ (∀x . Q).

4.1.3 The let and case constructions

Local abbreviations can be introduced by a let construct whose syntax appears in Fig. 4.2. Internally it is translated into the constant Let. It can be expanded by rewriting with its definition, Let_def.

HOL also defines the basic syntax

                   case e of c_{1} => e_{1} | . . . | c_{n} => e_{n}

as a uniform means of expressing case constructs. Therefore case and of are reserved words. Initially, this is mere syntax and has no logical meaning. By declaring translations, you can cause instances of the case construct to denote applications of particular case operators. This is what happens automatically for each datatype definition (see §4.6).

! Both if and case constructs have as low a priority as quantifiers, which re-

quires additional enclosing parentheses in the context of most other operations. For example, instead of f x = if … then … else … you need to write f x = (if … then … else …).

4.2 Rules of inference

Figure 4.3 shows the primitive inference rules of HOL, with their ml names. Some of the rules deserve additional comments:

2Class ord does not require much of its instances, so ≤ need not be a well-ordering, not even an order at all!

      True_def   True     == ((%x::bool.x)=(%x.x))
      All_def    All      == (%P. P = (%x.True))
      Ex_def     Ex       == (%P. P(@x.P x))
      False_def  False    == (!P.P)
      not_def    not      == (%P. P-->False)
      and_def    op &     == (%P Q. !R. (P-->Q-->R) --> R)
      or_def     op |     == (%P Q. !R. (P-->R) --> (Q-->R) --> R)
      Ex1_def    Ex1      == (%P. ? x. P x & (! y. P y --> y=x))
      o_def      op o     == (%(f::'b=>'c) g x::'a. f(g x))
      if_def     If P x y ==
                    (%P x y. @z::'a.(P=True --> z=x) & (P=False --> z=y))
      Let_def    Let s f  == f s
      Least_def  Least P  == @x. P(x) & (ALL y. P(y) --> x <= y)"

Figure 4.4: The HOL definitions

ext expresses extensionality of functions.

iff asserts that logically equivalent formulae are equal.

selectI gives the defining property of the Hilbert ε-operator. It is a form of the Axiom of Choice. The derived rule select_equality (see below) is often easier to use.

True_or_False makes the logic classical.^{3}

HOL follows standard practice in higher-order logic: only a few connectives are taken as primitive, with the remainder defined obscurely (Fig. 4.4). Gordon’s hol system expresses the corresponding definitions [16, page 270] using objectequality (=), which is possible because equality in higher-order logic may equate formulae and even functions over formulae. But theory HOL, like all other Isabelle theories, uses meta-equality (==) for definitions.

! The definitions above should never be expanded and are shown for completeness

only. Instead users should reason in terms of the derived rules shown below or, better still, using high-level tactics (see §4.4).

Some of the rules mention type variables; for example, refl mentions the type variable 'a. This allows you to instantiate type variables explicitly by

calling res_inst_tac.

Some derived rules are shown in Figures 4.5 and 4.6, with their ml names. These include natural rules for the logical connectives, as well as sequent-style elimination rules for conjunctions, implications, and universal quantifiers.

3In fact, the ε-operator already makes the logic classical, as shown by Diaconescu; see Paulson [39] for details.

sym         s=t ==> t=s
trans       [| r=s; s=t |] ==> r=t
ssubst      [| t=s; P s |] ==> P t
box_equals  [| a=b;  a=c;  b=d |] ==> c=d
arg_cong    x = y ==> f x = f y
fun_cong    f = g ==> f x = g x
cong        [| f = g; x = y |] ==> f x = g y
not_sym     t ~= s ==> s ~= t

Equality

TrueI       True
FalseE      False ==> P
conjI       [| P; Q |] ==> P&Q
conjunct1   [| P&Q |] ==> P
conjunct2   [| P&Q |] ==> Q
conjE       [| P&Q;  [| P; Q |] ==> R |] ==> R
disjI1      P ==> P|Q
disjI2      Q ==> P|Q
disjE       [| P | Q; P ==> R; Q ==> R |] ==> R
notI        (P ==> False) ==> ~ P
notE        [| ~ P;  P |] ==> R
impE        [| P-->Q;  P;  Q ==> R |] ==> R

Propositional logic

iffI        [| P ==> Q;  Q ==> P |] ==> P=Q
iffD1       [| P=Q; P |] ==> Q
iffD2       [| P=Q; Q |] ==> P
iffE        [| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R

Logical equivalence

Figure 4.5: Derived rules for HOL

allI      (!!x. P x) ==> !x. P x
spec      !x.P x ==> P x
allE      [| !x.P x;  P x ==> R |] ==> R
all_dupE  [| !x.P x;  [| P x; !x.P x |] ==> R |] ==> R
exI       P x ==> ? x. P x
exE       [| ? x. P x; !!x. P x ==> Q |] ==> Q
ex1I      [| P a;  !!x. P x ==> x=a |] ==> ?! x. P x
ex1E      [| ?! x.P x;  !!x. [| P x;  ! y. P y --> y=x |] ==> R
          |] ==> R
select_equality [| P a;  !!x. P x ==> x=a |] ==> (@x.P x) = a

Quantifiers and descriptions

ccontr          (~P ==> False) ==> P
classical       (~P ==> P) ==> P
excluded_middle ~P | P
disjCI          (~Q ==> P) ==> P|Q
exCI            (! x. ~ P x ==> P a) ==> ? x.P x
impCE           [| P-->Q; ~ P ==> R; Q ==> R |] ==> R
iffCE           [| P=Q;  [| P;Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R
notnotD         ~~P ==> P
swap            ~P ==> (~Q ==> P) ==> Q

Classical logic

if_P            P ==> (if P then x else y) = x
if_not_P        ~ P ==> (if P then x else y) = y
expand_if       P(if Q then x else y) = ((Q --> P x) & (~Q --> P y))

Conditionals

Figure 4.6: More derived rules

Note the equality rules: ssubst performs substitution in backward proofs, while box_equals supports reasoning by simplifying both sides of an equation.

The following simple tactics are occasionally useful:

strip_tac i applies allI and impI repeatedly to remove all outermost universal quantifiers and implications from subgoal i.

case_tac "P" i performs case distinction on P for subgoal i: the latter is replaced by two identical subgoals with the added assumptions P and ¬P, respectively.

4.3 A formulation of set theory

Historically, higher-order logic gives a foundation for Russell and Whitehead’s theory of classes. Let us use modern terminology and call them sets, but note that these sets are distinct from those of ZF set theory, and behave more like ZF classes.

• Sets are given by predicates over some type σ. Types serve to define universes for sets, but type checking is still significant.

• There is a universal set (for each type). Thus, sets have complements, and may be defined by absolute comprehension.

• Although sets may contain other sets as elements, the containing set must have a more complex type.

Finite unions and intersections have the same behaviour in HOL as they do in ZF. In HOL the intersection of the empty set is well-defined, denoting the universal set for the given type.

4.3.1 Syntax of set theory

HOL’s set theory is called Set. The type α set is essentially the same as α ⇒ bool. The new type is defined for clarity and to avoid complications involving function types in unification. The isomorphisms between the two types are declared explicitly. They are very natural: Collect maps α ⇒ bool to α set, while op : maps in the other direction (ignoring argument order).

Figure 4.7 lists the constants, infixes, and syntax translations. Figure 4.8 presents the grammar of the new constructs. Infix operators include union and intersection (A ∪ B and A ∩ B), the subset and membership relations, and the image operator ``. Note that a~:b is translated to ¬(a ∈ b).

name  meta-type  description
{}  α set  the empty set
insert  [α, α set] ⇒ α set  insertion of element
Collect  (α ⇒ bool) ⇒ α set  comprehension
Compl  α set ⇒ α set  complement
INTER [α set, α ⇒ β set] ⇒ β set intersection over a set
UNION [α set, α ⇒ β set] ⇒ β set  union over a set
Inter  (α set)set ⇒ α set set of sets intersection
Union  (α set)set ⇒ α set  set of sets union
Pow  α set ⇒ (α set)set  powerset
range  (α ⇒ β) ⇒ β set  range of a function
Ball Bex [α set, α ⇒ bool] ⇒ bool  bounded quantifiers

Constants

symbol name meta-type priority description
INT    INTER1 (α ⇒ β set) ⇒ β set  10 intersection over a type
UN UNION1 (α ⇒ β set) ⇒ β set 10 union over a type

Binders

symbol meta-type priority description
`` [α ⇒ β, α set] ⇒ β set Left 90  image
Int [α set, α set] ⇒ α set Left 70 intersection (∩)
Un [α set, α set] ⇒ α set Left 65  union (∪)
:  [α, α set] ⇒ bool Left 50 membership (∈)
<= [α set, α set] ⇒ bool Left 50 subset (⊆)

Infixes Figure 4.7: Syntax of the theory Set

external  internal  description
a ~: b  ~(a : b) non-membership
{a_{1}, …}   insert a_{1} … {}  finite set
{x.P[x]}  Collect(λx . P[x]) comprehension
INT x:A.B[x] INTER A λx . B[x]  intersection
UN x:A.B[x] UNION A λx . B[x]  union
! x:A.P[x] or ALL x:A.P[x] Ball A λx . P[x]  bounded ∀
? x:A.P[x] or EX x:A.P[x] Bex A λx . P[x] bounded ∃

Translations

term = other terms…

| {}

| { term (,term)^{∗} }
| { id . formula }
| term `` term
| term Int term
| term Un term
| INT id:term . term
| UN id:term . term
| INT id id^{∗} . term
| UN id id^{∗} . term
formula = other formulae…
| term : term
| term ~: term
| term <= term
| ! id:term . formula | ALL id:term . formula
| ? id:term . formula | EX id:term . formula

Full Grammar

Figure 4.8: Syntax of the theory Set (continued)

The {a_{1}, …} notation abbreviates finite sets constructed in the obvious manner using insert and {}:

             {a, b, c} ≡ insert a (insert b (insert c {}))

The set {x.P[x]} consists of all x (of suitable type) that satisfy P[x], where P[x] is a formula that may contain free occurrences of x. This syntax expands to Collect(λx .P[x]). It defines sets by absolute comprehension, which is impossible in ZF; the type of x implicitly restricts the comprehension.

The set theory defines two bounded quantifiers:

∀x ∈ A . P[x] abbreviates ∀x . x ∈ A → P[x]
∃x ∈ A . P[x] abbreviates ∃x . x ∈ A ∧ P[x]

The constants Ball and Bex are defined accordingly. Instead of Ball A P and Bex A P we may write ! x:A.P[x] and ? x:A.P[x]. Isabelle’s usual quantifier symbols, ALL and EX, are also accepted for input. As with the primitive quantifiers, the ml reference HOL_quantifiers specifies which notation to use for output.

Unions and intersections over sets, namely ⋃_{x∈A} B[x] and ⋂_{x∈A} B[x], are written UN x:A.B[x] and INT x:A.B[x].

Unions and intersections over types, namely ⋃_{x} B[x] and ⋂_{x} B[x], are written UN x.B[x] and INT x.B[x]. They are equivalent to the previous union and intersection operators when A is the universal set.

The operators ⋃ A and ⋂ A act upon sets of sets. They are not binders, but are equal to ⋃_{x∈A} x and ⋂_{x∈A} x, respectively.

4.3.2 Axioms and rules of set theory

Figure 4.9 presents the rules of theory Set. The axioms mem_Collect_eq and Collect_mem_eq assert that the functions Collect and op : are isomorphisms. Of course, op : also serves as the membership relation.

All the other axioms are definitions. They include the empty set, bounded quantifiers, unions, intersections, complements and the subset relation. They also include straightforward constructions on functions: image (``) and range.

Figures 4.10 and 4.11 present derived rules. Most are obvious and resemble rules of Isabelle’s ZF set theory. Certain rules, such as subsetCE, bexCI and UnCI, are designed for classical reasoning; the rules subsetD, bexI, Un1 and Un2 are not strictly necessary but yield more natural proofs. Similarly, equalityCE supports classical reasoning about extensionality, after the fashion of iffCE. See the file HOL/Set.ML for proofs pertaining to set theory.

Figure 4.12 presents lattice properties of the subset relation. Unions form least upper bounds; non-empty intersections form greatest lower bounds. Reasoning directly about subsets often yields clearer proofs than reasoning about the membership relation. See the file HOL/subset.ML.

      mem_Collect_eq    (a : {x.P x}) = P a
      Collect_mem_eq    {x.x:A} = A
      empty_def         {}          == {x.False}
      insert_def        insert a B  == {x.x=a} Un B
      Ball_def          Ball A P    == ! x. x:A --> P x
      Bex_def           Bex A P     == ? x. x:A & P x
      subset_def        A <= B      == ! x:A. x:B
      Un_def            A Un B      == {x.x:A | x:B}
      Int_def           A Int B     == {x.x:A & x:B}
      set_diff_def      A - B       == {x.x:A & x~:B}
      Compl_def         Compl A     == {x. ~ x:A}
      INTER_def         INTER A B   == {y. ! x:A. y: B x}
      UNION_def         UNION A B   == {y. ? x:A. y: B x}
      INTER1_def        INTER1 B    == INTER {x.True} B
      UNION1_def        UNION1 B    == UNION {x.True} B
      Inter_def         Inter S     == (INT x:S. x)
      Union_def         Union S     == (UN  x:S. x)
      Pow_def           Pow A       == {B. B <= A}
      image_def         f``A        == {y. ? x:A. y=f x}
      range_def         range f     == {y. ? x. y=f x}

Figure 4.9: Rules of the theory Set

Figure 4.13 presents many common set equalities. They include commutative, associative and distributive laws involving unions, intersections and complements. For a complete listing see the file HOL/equalities.ML.

! Blast_tac proves many set-theoretic theorems automatically. Hence you seldom need to refer to the theorems above.

4.3.3 Properties of functions

Figure 4.14 presents a theory of simple properties of functions. Note that inv f uses Hilbert’s ε to yield an inverse of f . See the file HOL/Fun.ML for a complete listing of the derived rules. Reasoning about function composition (the operator o) and the predicate surj is done simply by expanding the definitions.

There is also a large collection of monotonicity theorems for constructions on sets in the file HOL/mono.ML.

4.4 Generic packages

HOL instantiates most of Isabelle’s generic packages, making available the simplifier and the classical reasoner.

CollectI        [| P a |] ==> a : {x.P x}
CollectD        [| a : {x.P x} |] ==> P a
CollectE        [| a : {x.P x};  P a ==> W |] ==> W
ballI           [| !!x. x:A ==> P x |] ==> ! x:A. P x
bspec           [| ! x:A. P x;  x:A |] ==> P x
ballE           [| ! x:A. P x;  P x ==> Q;  ~ x:A ==> Q |] ==> Q
bexI            [| P x;  x:A |] ==> ? x:A. P x
bexCI           [| ! x:A. ~ P x ==> P a;  a:A |] ==> ? x:A.P x
bexE            [| ? x:A. P x;  !!x. [| x:A; P x |] ==> Q  |] ==> Q

Comprehension and Bounded quantifiers

subsetI         (!!x.x:A ==> x:B) ==> A <= B
subsetD         [| A <= B;  c:A |] ==> c:B
subsetCE        [| A <= B;  ~ (c:A) ==> P;  c:B ==> P |] ==> P
subset_refl     A <= A
subset_trans    [| A<=B;  B<=C |] ==> A<=C
equalityI       [| A <= B;  B <= A |] ==> A = B
equalityD1      A = B ==> A<=B
equalityD2      A = B ==> B<=A
equalityE       [| A = B;  [| A<=B; B<=A |] ==> P |]  ==>  P
equalityCE      [| A = B;  [| c:A; c:B |] ==> P;
                           [| ~ c:A; ~ c:B |] ==> P
                |]  ==>  P

The subset and equality relations

Figure 4.10: Derived rules for set theory

emptyE   a : {} ==> P
insertI1 a : insert a B
insertI2 a : B ==> a : insert b B
insertE  [| a : insert b A;  a=b ==> P;  a:A ==> P |] ==> P
ComplI   [| c:A ==> False |] ==> c : Compl A
ComplD   [| c : Compl A |] ==> ~ c:A
UnI1     c:A ==> c : A Un B
UnI2     c:B ==> c : A Un B
UnCI     (~c:B ==> c:A) ==> c : A Un B
UnE      [| c : A Un B;  c:A ==> P;  c:B ==> P |] ==> P
IntI     [| c:A;  c:B |] ==> c : A Int B
IntD1    c : A Int B ==> c:A
IntD2    c : A Int B ==> c:B
IntE     [| c : A Int B;  [| c:A; c:B |] ==> P |] ==> P
UN_I     [| a:A;  b: B a |] ==> b: (UN x:A. B x)
UN_E     [| b: (UN x:A. B x);  !!x.[| x:A;  b:B x |] ==> R |] ==> R
INT_I    (!!x. x:A ==> b: B x) ==> b : (INT x:A. B x)
INT_D    [| b: (INT x:A. B x);  a:A |] ==> b: B a
INT_E    [| b: (INT x:A. B x);  b: B a ==> R;  ~ a:A ==> R |] ==> R
UnionI   [| X:C;  A:X |] ==> A : Union C
UnionE   [| A : Union C;  !!X.[| A:X;  X:C |] ==> R |] ==> R
InterI   [| !!X. X:C ==> A:X |] ==> A : Inter C
InterD   [| A : Inter C;  X:C |] ==> A:X
InterE   [| A : Inter C;  A:X ==> R;  ~ X:C ==> R |] ==> R
PowI     A<=B ==> A: Pow B
PowD     A: Pow B ==> A<=B
imageI   [| x:A |] ==> f x : f``A
imageE   [| b : f``A;  !!x.[| b=f x;  x:A |] ==> P |] ==> P
rangeI   f x : range f
rangeE   [| b : range f;  !!x.[| b=f x |] ==> P |] ==> P

Figure 4.11: Further derived rules for set theory

Union_upper     B:A ==> B <= Union A
Union_least     [| !!X. X:A ==> X<=C |] ==> Union A <= C
Inter_lower     B:A ==> Inter A <= B
Inter_greatest  [| !!X. X:A ==> C<=X |] ==> C <= Inter A
Un_upper1       A <= A Un B
Un_upper2       B <= A Un B
Un_least        [| A<=C;  B<=C |] ==> A Un B <= C
Int_lower1      A Int B <= A
Int_lower2      A Int B <= B
Int_greatest    [| C<=A;  C<=B |] ==> C <= A Int B

Figure 4.12: Derived rules involving subsets

Int_absorb        A Int A = A
Int_commute       A Int B = B Int A
Int_assoc         (A Int B) Int C  =  A Int (B Int C)
Int_Un_distrib    (A Un B)  Int C  =  (A Int C) Un (B Int C)
Un_absorb         A Un A = A
Un_commute        A Un B = B Un A
Un_assoc          (A Un B)  Un C  =  A Un (B Un C)
Un_Int_distrib    (A Int B) Un C  =  (A Un C) Int (B Un C)
Compl_disjoint    A Int (Compl A) = {x.False}
Compl_partition   A Un  (Compl A) = {x.True}
double_complement Compl(Compl A) = A
Compl_Un          Compl(A Un B)  = (Compl A) Int (Compl B)
Compl_Int         Compl(A Int B) = (Compl A) Un (Compl B)
Union_Un_distrib  Union(A Un B) = (Union A) Un (Union B)
Int_Union         A Int (Union B) = (UN C:B. A Int C)
Un_Union_image    (UN x:C.(A x) Un (B x)) = Union(A``C) Un Union(B``C)
Inter_Un_distrib  Inter(A Un B) = (Inter A) Int (Inter B)
Un_Inter          A Un (Inter B) = (INT C:B. A Un C)
Int_Inter_image   (INT x:C.(A x) Int (B x)) = Inter(A``C) Int Inter(B``C)

Figure 4.13: Set equalities

name  meta-type  description
inj surj  (α ⇒ β) ⇒ bool injective/surjective
inj_onto [α ⇒ β, α set] ⇒ bool injective over subset
inv (α ⇒ β) ⇒ (β ⇒ α)  inverse function

      inj_def           inj f        == ! x y. f x=f y --> x=y
      surj_def          surj f       == ! y. ? x. y=f x
      inj_onto_def      inj_onto f A == !x:A. !y:A. f x=f y --> x=y
      inv_def           inv f        == (%y. @x. f(x)=y)

Figure 4.14: Theory Fun

4.4.1 Simplification and substitution

The simplifier is available in HOL. Tactics such as Asm_simp_tac and Full_simp_tac use the default simpset (!simpset), which works for most purposes. A quite minimal simplification set for higher-order logic is HOL_ss, even more frugal is HOL_basic_ss. Equality (=), which also expresses logical equivalence, may be used for rewriting. See the file HOL/simpdata.ML for a complete listing of the basic simplification rules.

See the Reference Manual for details of substitution and simplification.

! Reducing a = b ∧ P(a) to a = b ∧ P(b) is sometimes advantageous. The left part

of a conjunction helps in simplifying the right part. This effect is not available by default: it can be slow. It can be obtained by including conj_cong in a simpset,

addcongs [conj_cong].

If the simplifier cannot use a certain rewrite rule — either because of nontermination or because its left-hand side is too flexible — then you might try

stac:

stac thm i, where thm is of the form lhs = rhs, replaces in subgoal i instances of lhs by corresponding instances of rhs. In case of multiple instances of lhs in subgoal i, backtracking may be necessary to select the desired ones.

If thm is a conditional equality, the instantiated condition becomes an additional (first) subgoal.

HOL provides the tactic hyp_subst_tac, which substitutes for an equality throughout a subgoal and its hypotheses. This tactic uses HOL’s general substitution rule.

Case splitting

HOL also provides convenient means for case splitting during rewriting. Goals containing a subterm of the form if b then...else... often require a case distinction on b. This is expressed by the theorem expand_if:

?P(if ?b then ?x else ?y) = ((?b → ?P(?x)) ∧ (¬?b → ?P(?y)))  (∗)

For example, a simple instance of (∗) is

x ∈ (if x ∈ A then A else {x}) = ((x ∈ A → x ∈ A) ∧ (x ∉ A → x ∈ {x}))

Because (∗) is too general as a rewrite rule for the simplifier (the left-hand side is not a higher-order pattern in the sense of the Reference Manual), there is a special infix function addsplits (analogous to addsimps) of type simpset * thm list -> simpset that adds rules such as (∗) to a simpset, as in

      by(simp_tac (!simpset addsplits [expand_if]) 1);

The effect is that after each round of simplification, one occurrence of if is split acording to expand_if, until all occurences of if have been eliminated.

In general, addsplits accepts rules of the form

?P(c ?x_{1} … ?x_{n}) = rhs

where c is a constant and rhs is arbitrary. Note that (∗) is of the right form because internally the left-hand side is ?P(If ?b ?x ?y). Important further examples are splitting rules for case expressions (see §4.5.3 and §4.6.1).

4.4.2 Classical reasoning

HOL derives classical introduction rules for ∨ and ∃, as well as classical elimination rules for → and ↔, and the swap rule; recall Fig. 4.6 above.

The classical reasoner is installed. Tactics such as Blast_tac and Best_tac use the default claset (!claset), which works for most purposes. Named clasets include prop_cs, which includes the propositional rules, and HOL_cs, which also includes quantifier rules. See the file HOL/cladata.ML for lists of the classical rules, and the Reference Manual for more discussion of classical proof methods.

4.5 Types

This section describes HOL’s basic predefined types (α × β, α + β, nat and α list) and ways for introducing new types in general. The most important type construction, the datatype, is treated separately in §4.6.

4.5.1 Product and sum types

Theory Prod (Fig. 4.15) defines the product type α × β, with the ordered pair syntax (a, b). General tuples are simulated by pairs nested to the right:

symbol  meta-type  description
Pair  [α, β] ⇒ α × β  ordered pairs (a, b)
fst  α × β ⇒ α  first projection
snd  α × β ⇒ β  second projection
split  [[α, β] ⇒ γ, α × β] ⇒ γ  generalized projection
Sigma [α set, α ⇒ β set] ⇒ (α × β)set  general sum of sets

Sigma_def    Sigma A B == UN x:A. UN y:B x. {(x,y)}
Pair_eq      ((a,b) = (a',b')) = (a=a' & b=b')
Pair_inject  [| (a, b) = (a',b');  [| a=a';  b=b' |] ==> R |] ==> R
PairE        [| !!x y. p = (x,y) ==> Q |] ==> Q
fst_conv     fst (a,b) = a
snd_conv     snd (a,b) = b
surjective_pairing  p = (fst p,snd p)
split        split c (a,b) = c a b
expand_split R(split c p) = (! x y. p = (x,y) --> R(c x y))
SigmaI    [| a:A;  b:B a |] ==> (a,b) : Sigma A B
SigmaE    [| c:Sigma A B; !!x y.[| x:A; y:B x; c=(x,y) |] ==> P |] ==> P

Figure 4.15: Type α × β

external  internal
τ_{1} × … × τ_{n} τ_{1} × (… (τ_{n−1} × τ_{n}) …)
(t_{1}, …, t_{n}) (t_{1}, (…, (t_{n−1}, t_{n}) …)

In addition, it is possible to use tuples as patterns in abstractions:

%(x,y).t stands for split(%x y.t)

Nested patterns are also supported. They are translated stepwise: %(x,y,z).t

⇝ %(x,(y,z)).t ⇝ split(%x.%(y,z).t) ⇝ split(%x.split(%y z.t)). The

reverse translation is performed upon printing.

! The translation between patterns and split is performed automatically by the

parser and printer. Thus the internal and external form of a term may differ, which can affects proofs. For example the term (%(x,y).(y,x))(a,b) requires the theorem split (which is in the default simpset) to rewrite to (b,a).

In addition to explicit λ-abstractions, patterns can be used in any variable binding construct which is internally described by a λ-abstraction. Some important examples are

Let: let pattern = t in u

Quantifiers: ! pattern:A. P

Choice: @ pattern . P

Set operations: UN pattern:A. B

Sets: { pattern . P }

There is a simple tactic which supports reasoning about patterns:

split_all_tac i replaces in subgoal i all !!-quantified variables of product type by individual variables for each component. A simple example:

        1. !!p. (%(x,y,z). (x, y, z)) p = p
      by(split_all_tac 1);
        1. !!x xa ya. (%(x,y,z). (x, y, z)) (x, xa, ya) = (x, xa, ya)

Theory Prod also introduces the degenerate product type unit which contains only a single element named () with the property

      unit_eq       u = ()

Theory Sum (Fig. 4.16) defines the sum type α + β which associates to the right and has a lower priority than ∗: τ_{1} + τ_{2} + τ_{3} ∗ τ_{4} means τ_{1} + (τ_{2} + (τ_{3} ∗ τ_{4})).

The definition of products and sums in terms of existing types is not shown. The constructions are fairly standard and can be found in the respective theory files.

symbol  meta-type  description
Inl  α ⇒ α + β  first injection
Inr  β ⇒ α + β  second injection
sum_case [α ⇒ γ, β ⇒ γ, α + β] ⇒ γ  conditional

Inl_not_Inr    Inl a ~= Inr b
inj_Inl        inj Inl
inj_Inr        inj Inr
sumE           [| !!x. P(Inl x);  !!y. P(Inr y) |] ==> P s
sum_case_Inl   sum_case f g (Inl x) = f x
sum_case_Inr   sum_case f g (Inr x) = g x
surjective_sum sum_case (%x. f(Inl x)) (%y. f(Inr y)) s = f s
expand_sum_case R(sum_case f g s) = ((! x. s = Inl(x) --> R(f(x))) &
                                     (! y. s = Inr(y) --> R(g(y))))

Figure 4.16: Type α + β

symbol  meta-type priority  description
0  nat  zero
Suc  nat ⇒ nat  successor function
* [nat, nat] ⇒ nat Left 70  multiplication
div [nat, nat] ⇒ nat Left 70  division
mod [nat, nat] ⇒ nat Left 70  modulus
+ [nat, nat] ⇒ nat Left 65  addition
- [nat, nat] ⇒ nat Left 65  subtraction

Constants and infixes

nat_induct     [| P 0; !!n. P n ==> P(Suc n) |]  ==> P n
Suc_not_Zero   Suc m ~= 0
inj_Suc        inj Suc
n_not_Suc_n    n~=Suc n

Basic properties

Figure 4.17: The type of natural numbers, nat

                    0+n           = n
                    (Suc m)+n     = Suc(m+n)
                    m-0           = m
                    0-n           = n
                    Suc(m)-Suc(n) = m-n
                    0*n           = 0
                    Suc(m)*n      = n + m*n
      mod_less      m<n ==> m mod n = m
      mod_geq       [| 0<n;  ~m<n |] ==> m mod n = (m-n) mod n
      div_less      m<n ==> m div n = 0
      div_geq       [| 0<n;  ~m<n |] ==> m div n = Suc((m-n) div n)

Figure 4.18: Recursion equations for the arithmetic operators

4.5.2 The type of natural numbers, nat

The theory NatDef defines the natural numbers in a roundabout but traditional way. The axiom of infinity postulates a type ind of individuals, which is nonempty and closed under an injective operation. The natural numbers are inductively generated by choosing an arbitrary individual for 0 and using the injective operation to take successors. This is a least fixedpoint construction. For details

see the file NatDef.thy.

Type nat is an instance of class ord, which makes the overloaded functions of this class (esp. < and <=, but also min, max and LEAST) available on nat. Theory Nat builds on NatDef and shows that <= is a partial order, so nat is also an instance of class order.

Theory Arith develops arithmetic on the natural numbers. It defines addition, multiplication and subtraction. Theory Divides defines division, remainder and the “divides” relation. The numerous theorems proved include commutative, associative, distributive, identity and cancellation laws. See Figs. 4.17 and 4.18. The recursion equations for the operators +, - and * on nat are part of the default simpset.

Functions on nat can be defined by primitive or well-founded recursion; see §4.7. A simple example is addition. Here, op + is the name of the infix operator +, following the standard convention.

      primrec "op +" nat
        "    0 + n = n"
        "Suc m + n = Suc(m + n)"

There is also a case-construct of the form

      case e of 0 => a | Suc m => b

Note that Isabelle insists on precisely this format; you may not even change the order of the two cases. Both primrec and case are realized by a recursion operator nat_rec, the details of which can be found in theory NatDef.

Tactic induct_tac "n" i performs induction on variable n in subgoal i using theorem nat_induct. There is also the derived theorem less_induct:

      [| !!n. [| ! m. m<n --> P m |] ==> P n |]  ==>  P n

Reasoning about arithmetic inequalities can be tedious. A minimal amount of automation is provided by the tactic trans_tac of type int -> tactic that deals with simple inequalities. Note that it only knows about 0, Suc, < and <=. The following goals are all solved by trans_tac 1:

         1. ... ==> m <= Suc(Suc m)
         1. [| ... i <= j ... Suc j <= k ... |] ==> i < k
         1. [| ... Suc m <= n ... ~ m < n ... |] ==> ...

For a complete description of the limitations of the tactic and how to avoid some of them, see the comments at the start of the file Provers/nat_transitive.ML.

If trans_tac fails you, try to find relevant arithmetic results in the library. The theory NatDef contains theorems about < and <=, the theory Arith contains theorems about +, - and *, and theory Divides contains theorems about div and mod. Use the find-functions to locate them (see the Reference Manual).

4.5.3 The type constructor for lists, list

Figure 4.19 presents the theory List: the basic list operations with their types and syntax. Type α list is defined as a datatype with the constructors [] and #. As a result the generic structural induction and case analysis tactics induct tac and exhaust tac also become available for lists. A case construct of the form

                  case e of [] => a | x#xs => b

is defined by translation. For details see §4.6. There is also a case splitting rule

split_list_case
           P(case e of [] => a | x#xs => f x xs) =

((e = [] → P(a)) ∧ (∀x xs . e = x#xs → P(f x xs)))

which can be fed to addsplits just like expand_if (see §4.4.1).

List provides a basic library of list processing functions defined by primitive recursion (see §4.7.1). The recursion equations are shown in Fig. 4.20.

4.5.4 Introducing new types

The HOL-methodology dictates that all extensions to a theory should be definitional. The type definition mechanism that meets this criterion is typedef.

symbol  meta-type priority  description
[]  α list  empty list
#  [α, α list] ⇒ α list Right 65  list constructor
null  α list ⇒ bool  emptiness test
hd  α list ⇒ α  head
tl  α list ⇒ α list  tail
last  α list ⇒ α  last element
butlast  α list ⇒ α list  drop last element
@  [α list, α list] ⇒ α list Left 65  append
map  (α ⇒ β) ⇒ (α list ⇒ β list)  apply to all
filter (α ⇒ bool) ⇒ (α list ⇒ α list)  filter functional
set  α list ⇒ α set  elements
mem  α ⇒ α list ⇒ bool Left 55  membership
foldl (β ⇒ α ⇒ β) ⇒ β ⇒ α list ⇒ β  iteration
concat  (α list)list ⇒ α list  concatenation
rev  α list ⇒ α list  reverse
length  α list ⇒ nat  length
!  α list ⇒ nat ⇒ α Left 100  indexing
take, drop  nat ⇒ α list ⇒ α list  take or drop a prefix

takeWhile,

dropWhile  (α ⇒ bool) ⇒ α list ⇒ α list  take or drop a prefix

Constants and infixes

external internal description
[x_{1}, …, x_{n}] x_{1} # ⋯ # x_{n} # []  finite list
[x:l. P]    filter (λx.P) l list comprehension

Translations Figure 4.19: The theory List

null [] = True
null (x#xs) = False
hd (x#xs) = x
tl (x#xs) = xs
tl [] = []
[] @ ys = ys
(x#xs) @ ys = x # xs @ ys
map f [] = []
map f (x#xs) = f x # map f xs
filter P [] = []
filter P (x#xs) = (if P x then x#filter P xs else filter P xs)
set [] = {}
set (x#xs) = insert x (set xs)
x mem [] = False
x mem (y#ys) = (if y=x then True else x mem ys)
foldl f a [] = a
foldl f a (x#xs) = foldl f (f a x) xs
concat([]) = []
concat(x#xs) = x @ concat(xs)
rev([]) = []
rev(x#xs) = rev(xs) @ [x]
length([]) = 0
length(x#xs) = Suc(length(xs))
xs!0 = hd xs
xs!(Suc n) = (tl xs)!n
take n [] = []
take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)
drop n [] = []
drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)
takeWhile P [] = []
takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])
dropWhile P [] = []
dropWhile P (x#xs) = (if P x then dropWhile P xs else xs)

Figure 4.20: Recursions equations for list processing functions Note that type synonyms, which are inherited from Pure and described elsewhere, are just syntactic abbreviations that have no logical meaning.

! Types in HOL must be non-empty; otherwise the quantifier rules would be unsound, because ∃x . x = x is a theorem [39, §7].

A type definition identifies the new type with a subset of an existing type. More precisely, the new type is defined by exhibiting an existing type τ, a set A :: τ set, and a theorem of the form x : A. Thus A is a non-empty subset of τ, and the new type denotes this subset. New functions are defined that establish an isomorphism between the new type and the subset. If type τ involves type variables α_{1}, …, α_{n}, then the type definition creates a type constructor (α_{1}, …, α_{n})ty rather than a particular type.

typedef

[figure: typedef; (; name; ); type; =; set; witness]

type

[figure: typevarlist; name; (; infix; )]

set string

witness

           [figure: (; id; )]

Figure 4.21: Syntax of type definitions

The syntax for type definitions is shown in Fig. 4.21. For the definition of ‘typevarlist’ and ‘infix’ see the appendix of the Reference Manual. The remaining nonterminals have the following meaning:

type: the new type constructor (α_{1}, …, α_{n})ty with optional infix annotation.

name: an alphanumeric name T for the type constructor ty, in case ty is a symbolic name. Defaults to ty. set: the representing subset A.

witness: name of a theorem of the form a : A proving non-emptiness. It can be omitted in case Isabelle manages to prove non-emptiness automatically.

If all context conditions are met (no duplicate type variables in ‘typevarlist’, no extra type variables in ‘set’, and no free term variables in ‘set’), the following components are added to the theory:

• a type ty :: (term, …, term)term

• constants

T :: τ set
Rep T :: (α_{1}, …, α_{n})ty ⇒ τ
Abs T :: τ ⇒ (α_{1}, …, α_{n})ty

• a definition and three axioms

T def  T ≡ A
Rep T  Rep T x ∈ T
Rep T inverse Abs T (Rep T x) = x
Abs T inverse y ∈ T ⟹ Rep T (Abs T y) = y

stating that (α_{1}, …, α_{n})ty is isomorphic to A by Rep T and its inverse Abs T .

Below are two simple examples of HOL type definitions. Non-emptiness is proved automatically here.

      typedef unit = "{True}"
      typedef (prod)
        ('a, 'b) "*"    (infixr 20)
            = "{f . EX (a::'a) (b::'b). f = (%x y. x = a & y = b)}"

Type definitions permit the introduction of abstract data types in a safe way, namely by providing models based on already existing types. Given some abstract axiomatic description P of a type, this involves two steps:

1. Find an appropriate type τ and subset A which has the desired properties P, and make a type definition based on this representation.

2. Prove that P holds for ty by lifting P from the representation.

You can now forget about the representation and work solely in terms of the abstract properties P.

! If you introduce a new type (constructor) ty axiomatically, i.e. by declaring the

type and its operations and by stating the desired axioms, you should make sure the type has a non-empty model. You must also have a clause

      arities ty :: (term, . . .,term)term

in your theory file to tell Isabelle that ty is in class term, the class of all HOL types.

4.6 Datatype declarations

Inductive datatypes, similar to those of ml, frequently appear in non-trivial applications of HOL. In principle, such types could be defined by hand via typedef (see §4.5.4), but this would be far too tedious. The datatype definition package of HOL automates such chores. It generates freeness theorems and induction rules from a very simple description of the new type provided by the user.

4.6.1 Basics

The general HOL datatype definition is of the following form:

datatype (α_{1}, …, α_{n}) t = C_{1} τ_{11} … τ_{1k_{1}} | … | C_{m} τ_{m1} … τ_{mk_{m}}

where α_{i} are type variables, C_{i} are distinct constructor names and τ_{ij} are types. The latter may be one of the following:

• type variables α_{1}, …, α_{n},

• types (β_{1}, …, β_{l}) t′ where t′ is a previously declared type constructor or type synonym and {β_{1}, …, β_{l}} ⊆ {α_{1}, …, α_{n}},

• the newly defined type (α_{1}, …, α_{n}) t.

Recursive occurences of (α_{1}, …, α_{n}) t are quite restricted. To ensure that the new type is non-empty, at least one constructor must consist of only non-recursive type components. If you would like one of the τ_{ij} to be a complex type expression τ you need to declare a new type synonym syn = τ first and use syn in place of τ. Of course this does not work if τ mentions the recursive type itself, thus ruling out problematic cases like datatype t = C (t ⇒ t), but also unproblematic ones like datatype t = C (t list).

The constructors are automatically defined as functions of their respective type:

C_{j} :: [τ_{j 1}, …, τ_{jk_{j}} ] ⇒ (α_{1}, …, α_{n})t

These functions have certain freeness properties — they are distinct:

C_{i} x_{1} … x_{k_{i}} ≠ C_{j} y_{1} … y_{k_{j}} for all i ≠ j .

and they are injective:

(C_{j} x_{1} … x_{k_{j}} = C_{j} y_{1} … y_{k_{j}} ) = (x_{1} = y_{1} ∧ … ∧ x_{k_{j}} = y_{k_{j}} )

Because the number of inequalities is quadratic in the number of constructors, a different representation is used if there are 7 or more of them. In that case every constructor term is mapped to a natural number:

t ord (C_{i} x_{1} … x_{k_{i}}) = i − 1

Then distinctness of constructor terms is expressed by:

t ord x ≠ t ord y ⟹ x ≠ y.

Generally, the following structural induction rule is provided:

⋀ x_{1} … x_{k_{1}} . [[P x_{r_{11}}; …; P x_{r_{1l_{1}}}]] ⟹ P (C_{1} x_{1} … x_{k_{1}})
⋮
⋀ x_{1} … x_{k_{m}} . [[P x_{r_{m1}}; …; P x_{r_{mlm}} ]] ⟹ P (C_{m} x_{1} … x_{k_{m}})

P x

where {r_{j 1}, …, r_{jl_{j}} } = {i ∈ {1, … k_{j} } | τ_{ji} = (α_{1}, …, α_{n})t} =: Rec_{j} , i.e. the property P can be assumed for all arguments of the recursive type.

For convenience, the following additional constructions are predefined for each datatype.

The case construct

The type comes with an ml-like case-construct:

case e of C_{1} x_{11} … x_{1k_{1}} ⇒ e_{1}
⋮
| C_{m} x_{m1} … x_{mk_{m}} ⇒ e_{m}

where the x_{ij} are either identifiers or nested tuple patterns as in §4.5.1.

! In contrast to ml, all constructors must be present, their order is fixed, and nested

patterns are not supported (with the exception of tuples). Violating this restriction results in strange error messages.

To perform case distinction on a goal containing a case-construct, the theorem

split_t_casesplit_t_case is provided:

P(t case f_{1} … f_{m} e) = ((∀x_{1} … x_{k_{1}} . e = C_{1} x_{1} … x_{k_{1}} → P(f_{1} x_{1} … x_{k_{1}}))
∧ … ∧

(∀x_{1} … x_{k_{m}} . e = C_{m} x_{1} … x_{k_{m}} → P(f_{m} x_{1} … x_{k_{m}})))

where t_case is the internal name of the case-construct. This theorem can be added to a simpset via addsplits (see §4.4.1). typedecl

[figure: typevarlist; id; =; cons; |]

cons

[figure: name; typ; mixfix]

typ

[figure: id; tid; (; typevarlist; id; )]

Figure 4.22: Syntax of datatype declarations

The function size

Theory Arith declares an overloaded function size of type α ⇒ nat. Each datatype defines a particular instance of size according to the following scheme:

size(C_{j} x_{j 1} … x_{jk_{1}}) = \{ \begin{matrix}0 & if Rec_{j} = ∅ \\ size(x_{r_{j 1}}) + ⋯ + size(x_{r_{jl_{j}}} ) + 1 & if Rec_{j} = \{r_{j 1}, …, r_{jl_{j}} \} \end{matrix}

where Rec_{j} is defined above. Viewing datatypes as generalized trees, the size of a leaf is 0 and the size of a node is the sum of the sizes of its subtrees +1.

4.6.2 Defining datatypes

A datatype is defined in a theory definition file using the keyword datatype. The definition following this must conform to the syntax of typedecl specified in Fig. 4.22 and must obey the rules in the previous section. As a result the theory is extended with the new type, the constructors, and the theorems listed in the previous section.

! Every theory containing a datatype declaration must be based, directly or indirectly, on the theory Arith, if necessary by including it explicitly as a parent.

Most of the theorems about the datatype become part of the default simpset and you never need to see them again because the simplifier applies them automatically. Only induction is invoked by hand:

induct_tac "x" i applies structural induction on variable x to subgoal i, provided the type of x is a datatype or type nat.

In some cases, induction is overkill and a case distinction over all constructors of the datatype suffices:

exhaust_tac "u" i performs an exhaustive case analysis for the term u whose type must be a datatype or type nat. If the datatype has n constructors C_{1}, … C_{n}, subgoal i is replaced by n new subgoals which contain the additional assumption u = C_{j} x_{1} … x_{k_{j}} for j = 1, …, n.

! Induction is only allowed on a free variable that should not occur among the premises of the subgoal. Exhaustion works for arbitrary terms.

For the technically minded, we give a more detailed description. Reading the theory file produces an ml structure which, in addition to the usual components, contains a structure named t for each datatype t defined in the file. Each structure t contains the following elements:

      val distinct : thm list
      val inject : thm list
      val induct : thm
      val cases : thm list
      val simps : thm list
      val induct_tac : string -> int -> tactic

distinct, inject and induct contain the theorems described above. For user convenience, distinct contains inequalities in both directions. The reduction rules of the case-construct are in cases. All theorems from distinct, inject and cases are combined in simps.

4.6.3 Examples

The datatype α mylist

We want to define the type α mylist.^{4} To do this we have to build a new theory that contains the type definition. We start from the basic HOL theory.

      MyList = HOL +
        datatype 'a mylist = Nil | Cons 'a ('a mylist)
      end

4This is just an example, there is already a list type in HOL, of course.

After loading the theory (with use_thy "MyList"), we can prove Cons x xs ≠ xs. To ease the induction applied below, we state the goal with x quantified at the object-level. This will be stripped later using qed_spec_mp.

      goal MyList.thy "!x. Cons x xs ~= xs";
        Level 0
        ! x. Cons x xs ~= xs
         1. ! x. Cons x xs ~= xs

This can be proved by the structural induction tactic:

      by (induct_tac "xs" 1);
        Level 1
        ! x. Cons x xs ~= xs
         1. ! x. Cons x Nil ~= Nil
         2. !!a mylist.
               ! x. Cons x mylist ~= mylist ==>
               ! x. Cons x (Cons a mylist) ~= Cons a mylist

The first subgoal can be proved using the simplifier. Isabelle has already added the freeness properties of lists to the default simplification set.

      by (Simp_tac 1);
        Level 2
        ! x. Cons x xs ~= xs
         1. !!a mylist.
               ! x. Cons x mylist ~= mylist ==>
               ! x. Cons x (Cons a mylist) ~= Cons a mylist

Similarly, we prove the remaining goal.

      by (Asm_simp_tac 1);
        Level 3
        ! x. Cons x xs ~= xs
        No subgoals!
      qed_spec_mp "not_Cons_self";
        val not_Cons_self = "Cons x xs ~= xs";

Because both subgoals could have been proved by Asm_simp_tac we could have done that in one step:

      by (ALLGOALS Asm_simp_tac);

The datatype α mylist with mixfix syntax

In this example we define the type α mylist again but this time we want to write [] for Nil and we want to use infix notation # for Cons. To do this we simply add mixfix annotations after the constructor declarations as follows:

      MyList = HOL +
        datatype 'a mylist =
          Nil ("[]")  |
          Cons 'a ('a mylist)  (infixr "#" 70)
      end

Now the theorem in the previous example can be written x#xs ~= xs. The proof is the same.

A datatype for weekdays

This example shows a datatype that consists of 7 constructors:

      Days = Arith +
        datatype days = Mon | Tue | Wed | Thu | Fri | Sat | Sun
      end

Because there are more than 6 constructors, the theory must be based on Arith. Inequality is expressed via a function days_ord. The theorem Mon ~= Tue is not directly contained among the distinctness theorems, but the simplifier can prove it thanks to rewrite rules inherited from theory Arith:

      goal Days.thy "Mon ~= Tue";
      by (Simp_tac 1);

You need not derive such inequalities explicitly: the simplifier will dispose of them automatically.

4.7 Recursive function definitions

Isabelle/HOL provides two means of declaring recursive functions.

• Primitive recursion is available only for datatypes, and it is highly restrictive. Recursive calls are only allowed on the argument’s immediate constituents. On the other hand, it is the form of recursion most often wanted, and it is easy to use.

• Well-founded recursion requires that you supply a well-founded relation that governs the recursion. Recursive calls are only allowed if they make the argument decrease under the relation. Complicated recursion forms, such as nested recursion, can be dealt with. Termination can even be proved at a later time, though having unsolved termination conditions around can make work difficult.^{5}

5This facility is based on Konrad Slind’s TFL package [44]. Thanks are due to Konrad for implementing TFL and assisting with its installation.

A theory file may contain any number of recursive function definitions, which may be intermixed with other declarations. Every recursive function must already have been declared as a constant.

These declarations do not assert new axioms. Instead, they define the function using a recursion operator. Both HOL and ZF derive the theory of well-founded recursion from first principles [35]. Primitive recursion over some datatype relies on the recursion operator provided by the datatype package. With either form of function definition, Isabelle proves the desired recursion equations as theorems.

4.7.1 Primitive recursive functions

Datatypes come with a uniform way of defining functions, primitive recursion. In principle, one can define primitive recursive functions by asserting their reduction rules as new axioms. Here is an example:

      Append = MyList +
      consts app :: ['a mylist, 'a mylist] => 'a mylist
      rules
         app_Nil   "app [] ys = ys"
         app_Cons  "app (x#xs) ys = x#app xs ys"
      end

But asserting axioms brings the danger of accidentally asserting an inconsistency,

as in app [] ys = us.

The primrec declaration is a safe means of defining primitive recursive functions on datatypes:

      Append = MyList +
      consts app :: ['a mylist, 'a mylist] => 'a mylist
      primrec app MyList.mylist
         "app [] ys = ys"
         "app (x#xs) ys = x#app xs ys"
      end

Isabelle will now check that the two rules do indeed form a primitive recursive definition, preserving consistency. For example

      primrec app MyList.mylist
          "app [] ys = us"

is rejected with an error message Extra variables on rhs.

The general form of a primitive recursive definition is

primrec function type reduction rules

where

• function is the name of the function, either as an id or a string.

• type is the name of the datatype, either as an id or in the long form T .t (T is the name of the theory where the datatype has been declared, t the name of the datatype). The long form is required if the datatype and the primrec sections are in different theories.

• reduction rules specify one or more equations of the form

f x_{1} … x_{m} (C y_{1} … y_{k}) z_{1} … z_{n} = r

such that C is a constructor of the datatype, r contains only the free variables on the left-hand side, and all recursive calls in r are of the form f … y_{i} … for some i. There must be exactly one reduction rule for each constructor. The order is immaterial. Also note that all reduction rules are added to the default simpset!

If you would like to refer to some rule by name, then you must prefix each rule with an identifier. These identifiers, like those in the rules section of a theory, will be visible at the ml level.

The primitive recursive function can have infix or mixfix syntax:

Append = MyList +
consts "@"  :: ['a mylist, 'a mylist] => 'a mylist  (infixr 60)
primrec "op @" MyList.mylist
   "[] @ ys = ys"
   "(x#xs) @ ys = x#(xs @ ys)"
end

The reduction rules for @ become part of the default simpset, which leads to short proofs:

goal Append.thy "(xs @ ys) @ zs = xs @ (ys @ zs)";
by (induct tac "xs" 1);
by (ALLGOALS Asm simp tac);

4.7.2 Well-founded recursive functions

Well-founded recursion can express any function whose termination can be proved by showing that each recursive call makes the argument smaller in a suitable sense. The recursion need not involve datatypes and there are few syntactic restrictions. Nested recursion and pattern-matching are allowed.

Here is a simple example, the Fibonacci function. The first line declares fib to be a constant. The well-founded relation is simply < (on the natural numbers).

Pattern-matching is used here: 1 is a macro for Suc 0.

      consts fib  :: "nat => nat"
      recdef fib "less_than"
          "fib 0 = 0"
          "fib 1 = 1"
          "fib (Suc(Suc x)) = (fib x + fib (Suc x))"

The well-founded relation defines a notion of “smaller” for the function’s argument type. The relation ≺ is well-founded provided it admits no infinitely decreasing chains

⋯ ≺ x_{n} ≺ ⋯ ≺ x_{1}.

If the function’s argument has type τ, then ≺ should be a relation over τ: it must have type (τ × τ)set.

Proving well-foundedness can be tricky, so HOL provides a collection of operators for building well-founded relations. The package recognizes these operators and automatically proves that the constructed relation is well-founded. Here are those operators, in order of importance:

• less_than is “less than” on the natural numbers. (It has type (nat × nat)set, while < has type [nat, nat] ⇒ bool.

• measure f , where f has type τ ⇒ nat, is the relation ≺ on type τ such that x ≺ y iff f (x) < f (y). Typically, f takes the recursive function’s arguments (as a tuple) and returns a result expressed in terms of the function size. It is called a measure function. Recall that size is overloaded and is defined on all datatypes (see §4.6.1).

• inv image f R is a generalization of measure. It specifies a relation such that x ≺ y iff f (x) is less than f (y) according to R, which must itself be a well-founded relation.

• R_{1}**R_{2} is the lexicographic product of two relations. It is a relation on pairs and satisfies (x_{1}, x_{2}) ≺ (y_{1}, y_{2}) iff x_{1} is less than y_{1} according to R_{1} or x_{1} = y_{1} and x_{2} is less than y_{2} according to R_{2}.

• finite_psubset is the proper subset relation on finite sets.

We can use measure to declare Euclid’s algorithm for the greatest common divisor. The measure function, λ(m, n).n, specifies that the recursion terminates because argument n decreases.

      recdef gcd "measure ((%(m,n).n) ::nat*nat=>nat)"
          "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"

The general form of a primitive recursive definition is

recdef function rel congs congruence rules (optional) simpset simplification set (optional) reduction rules

where

• function is the name of the function, either as an id or a string.

• rel is a HOL expression for the well-founded termination relation.

• congruence rules are required only in highly exceptional circumstances.

• the simplification set is used to prove that the supplied relation is wellfounded. It is also used to prove the termination conditions: assertions that arguments of recursive calls decrease under rel. By default, simplification uses !simpset, which is sufficient to prove well-foundedness for the built-in relations listed above.

• reduction rules specify one or more recursion equations. Each left-hand side must have the form f t, where f is the function and t is a tuple of distinct variables. If more than one equation is present then f is defined by pattern-matching on components of its argument whose type is a datatype. The patterns must be exhaustive and non-overlapping.

Unlike with primrec, the reduction rules are not added to the default simpset, and individual rules may not be labelled with identifiers. However, the identifier f .rules is visible at the ml level as a list of theorems.

With the definition of gcd shown above, Isabelle is unable to prove one termination condition. It remains as a precondition of the recursion theorems.

gcd.rules;
  ["! m n. n ~= 0 --> m mod n < n
    ==> gcd (?m, ?n) = (if ?n = 0 then ?m else gcd (?n, ?m mod ?n))"]
  : thm list

The theory Primes (on the examples directory HOL/ex) illustrates how to prove termination conditions afterwards. The function Tfl.tgoalw is like the standard function goalw, which sets up a goal to prove, but its argument should be the identifier f .rules and its effect is to set up a proof of the termination conditions:

Tfl.tgoalw thy [] gcd.rules;
  Level 0
  ! m n. n ~= 0 --> m mod n < n
   1. ! m n. n ~= 0 --> m mod n < n

This subgoal has a one-step proof using simp_tac. Once the theorem is proved, it can be used to eliminate the termination conditions from elements of gcd.rules. Theory Unify on directory HOL/Subst is a much more complicated example of this process, where the termination conditions can only be proved by complicated reasoning involving the recursive function itself.

Isabelle can prove the gcd function’s termination condition automatically if supplied with the right simpset.

      recdef gcd "measure ((%(m,n).n) ::nat*nat=>nat)"
        simpset "!simpset addsimps [mod_less_divisor, zero_less_eq]"
          "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"

A recdef definition also returns an induction rule specialized for the recursive function. For the gcd function above, the induction rule is

      gcd.induct;
        "(!!m n. n ~= 0 --> ?P n (m mod n) ==> ?P m n) ==> ?P ?u ?v" : thm

This rule should be used to reason inductively about the gcd function. It usually makes the induction hypothesis available at all recursive calls, leading to very direct proofs. If any termination conditions remain unproved, they will be additional premises of this rule.

4.8 Inductive and coinductive definitions

An inductive definition specifies the least set R closed under given rules. (Applying a rule to elements of R yields a result within R.) For example, a structural operational semantics is an inductive definition of an evaluation relation. Dually, a coinductive definition specifies the greatest set R consistent with given rules. (Every element of R can be seen as arising by applying a rule to elements of R.) An important example is using bisimulation relations to formalize equivalence of processes and infinite data structures.

A theory file may contain any number of inductive and coinductive definitions. They may be intermixed with other declarations; in particular, the (co)inductive sets must be declared separately as constants, and may have mixfix syntax or be subject to syntax translations.

Each (co)inductive definition adds definitions to the theory and also proves some theorems. Each definition creates an ml structure, which is a substructure of the main theory structure.

This package is derived from the ZF one, described in a separate paper,^{6} which you should refer to in case of difficulties. The package is simpler than ZF’s thanks to HOL’s automatic type-checking. The type of the (co)inductive determines the domain of the fixedpoint definition, and the package does not use inference rules for type-checking.

6It appeared in CADE [34]; a longer version is distributed with Isabelle.

4.8.1 The result structure

Many of the result structure’s components have been discussed in the paper; others are self-explanatory.

thy is the new theory containing the recursive sets.

defs is the list of definitions of the recursive sets.

mono is a monotonicity theorem for the fixedpoint operator.

unfold is a fixedpoint equation for the recursive set (the union of the recursive sets, in the case of mutual recursion).

intrs is the list of introduction rules, now proved as theorems, for the recursive sets. The rules are also available individually, using the names given them in the theory file.

elim is the elimination rule.

mk_cases is a function to create simplified instances of elim, using freeness reasoning on some underlying datatype.

For an inductive definition, the result structure contains two induction rules, induct and mutual_induct. (To save storage, the latter rule is just True unless more than one set is being defined.) For a coinductive definition, it contains the

rule coinduct.

Figure 4.23 summarizes the two result signatures, specifying the types of all these components.

4.8.2 The syntax of a (co)inductive definition

An inductive definition has the form

      inductive    inductive sets
        intrs      introduction rules
        monos      monotonicity theorems
        con_defs   constructor definitions

A coinductive definition is identical, except that it starts with the keyword

coinductive.

The monos and con_defs sections are optional. If present, each is specified as a string, which must be a valid ml expression of type thm list. It is simply inserted into the generated ml file that is generated from the theory definition;

  sig
  val thy          : theory
  val defs         : thm list
  val mono         : thm
  val unfold       : thm
  val intrs        : thm list
  val elim         : thm
  val mk_cases     : thm list -> string -> thm

(Inductive definitions only)

  val induct       : thm
  val mutual_induct: thm

(Coinductive definitions only)

  val coinduct    : thm
  end

Figure 4.23: The result of a (co)inductive definition

if it is ill-formed, it will trigger ML error messages. You can then inspect the file on your directory.

• The inductive sets are specified by one or more strings.

• The introduction rules specify one or more introduction rules in the form ident string, where the identifier gives the name of the rule in the result structure.

• The monotonicity theorems are required for each operator applied to a recursive set in the introduction rules. There must be a theorem of the form A ⊆ B ⟹ M (A) ⊆ M (B), for each premise t ∈ M (R_{i}) in an introduction rule!

• The constructor definitions contain definitions of constants appearing in the introduction rules. In most cases it can be omitted.

The package has a few notable restrictions:

• The theory must separately declare the recursive sets as constants.

• The names of the recursive sets must be alphanumeric identifiers.

• Side-conditions must not be conjunctions. However, an introduction rule may contain any number of side-conditions.

• Side-conditions of the form x = t, where the variable x does not occur in t, will be substituted through the rule mutual_induct.

4.8.3 Example of an inductive definition

Two declarations, included in a theory file, define the finite powerset operator. First we declare the constant Fin. Then we declare it inductively, with two introduction rules:

      consts Fin :: 'a set => 'a set set
      inductive "Fin A"
        intrs
          emptyI  "{} : Fin A"
          insertI "[| a: A;  b: Fin A |] ==> insert a b : Fin A"

The resulting theory structure contains a substructure, called Fin. It contains the Fin A introduction rules as the list Fin.intrs, and also individually as

Fin.emptyI and Fin.consI. The induction rule is Fin.induct.

For another example, here is a theory file defining the accessible part of a relation. The main thing to note is the use of Pow in the sole introduction rule, and the corresponding mention of the rule Pow_mono in the monos list. The paper [34] discusses a ZF version of this example in more detail.

      Acc = WF +
      consts pred :: "['b, ('a * 'b)set] => 'a set"   (*Set of predecessors*)
             acc  :: "('a * 'a)set => 'a set"         (*Accessible part*)
      defs   pred_def  "pred x r == y. (y,x):r"
      inductive "acc r"
        intrs
           pred "pred a r: Pow(acc r) ==> a: acc r"
        monos   "[Pow_mono]"
      end

The HOL distribution contains many other inductive definitions. Simple examples are collected on subdirectory Induct. The theory HOL/Induct/LList.thy contains coinductive definitions. Larger examples may be found on other subdirectories, such as IMP, Lambda and Auth.

4.9 The examples directories

Directory HOL/Auth contains theories for proving the correctness of cryptographic protocols. The approach is based upon operational semantics [38] rather than the more usual belief logics. On the same directory are proofs for some standard examples, such as the Needham-Schroeder public-key authentication protocol [36] and the Otway-Rees protocol.

Directory HOL/IMP contains a formalization of various denotational, operational and axiomatic semantics of a simple while-language, the necessary equivalence proofs, soundness and completeness of the Hoare rules with respect to the denotational semantics, and soundness and completeness of a verification condition generator. Much of development is taken from Winskel [50]. For details see [27].

Directory HOL/Hoare contains a user friendly surface syntax for Hoare logic, including a tactic for generating verification-conditions.

Directory HOL/MiniML contains a formalization of the type system of the core functional language Mini-ML and a correctness proof for its type inference algorithm W [23, 25].

Directory HOL/Lambda contains a formalization of untyped λ-calculus in de Bruijn notation and Church-Rosser proofs for β and η reduction [26].

Directory HOL/Subst contains Martin Coen’s mechanization of a theory of substitutions and unifiers. It is based on Paulson’s previous mechanisation in LCF [31] of Manna and Waldinger’s theory [21]. It demonstrates a complicated use of recdef, with nested recursion.

Directory HOL/Induct presents simple examples of (co)inductive definitions.

• Theory PropLog proves the soundness and completeness of classical propositional logic, given a truth table semantics. The only connective is →. A Hilbert-style axiom system is specified, and its set of theorems defined inductively. A similar proof in ZF is described elsewhere [35].

• Theory Term develops an experimental recursive type definition; the recursion goes through the type constructor list.

• Theory Simult constructs mutually recursive sets of trees and forests, including induction and recursion rules.

• The definition of lazy lists demonstrates methods for handling infinite data structures and coinduction in higher-order logic [37].^{7} Theory LList defines an operator for corecursion on lazy lists, which is used to define a few simple functions such as map and append. A coinduction principle is defined for proving equations on lazy lists.

• Theory LFilter defines the filter functional for lazy lists. This functional is notoriously difficult to define because finding the next element meeting the predicate requires possibly unlimited search. It is not computable, but can be expressed using a combination of induction and corecursion.

• Theory Exp illustrates the use of iterated inductive definitions to express a programming language semantics that appears to require mutual induction. Iterated induction allows greater modularity.

Directory HOL/ex contains other examples and experimental proofs in HOL.

• Theory Recdef presents many examples of using recdef to define recursive functions. Another example is Fib, which defines the Fibonacci function.

7To be precise, these lists are potentially infinite rather than lazy. Lazy implies a particular operational semantics.

• Theory Primes defines the Greatest Common Divisor of two natural numbers and proves a key lemma of the Fundamental Theorem of Arithmetic: if p is prime and p divides m × n then p divides m or p divides n.

• Theory Primrec develops some computation theory. It inductively defines the set of primitive recursive functions and presents a proof that Ackermann’s function is not primitive recursive.

• File cla.ML demonstrates the classical reasoner on over sixty predicate calculus theorems, ranging from simple tautologies to moderately difficult problems involving equality and quantifiers.

• File meson.ML contains an experimental implementation of the meson proof procedure, inspired by Plaisted [42]. It is much more powerful than Isabelle’s classical reasoner. But it is less useful in practice because it works only for pure logic; it does not accept derived rules for the set theory primitives, for example.

• File mesontest.ML contains test data for the meson proof procedure. These are mostly taken from Pelletier [41].

• File set.ML proves Cantor’s Theorem, which is presented in §4.10 below, and the Schröder-Bernstein Theorem.

• Theory MT contains Jacob Frost’s formalization [14] of Milner and Tofte’s coinduction example [24]. This substantial proof concerns the soundness of a type system for a simple functional language. The semantics of recursion is given by a cyclic environment, which makes a coinductive argument appropriate.

4.10 Example: Cantor’s Theorem

Cantor’s Theorem states that every set has more subsets than it has elements. It has become a favourite example in higher-order logic since it is so easily expressed:

∀f :: α ⇒ α ⇒ bool . ∃S :: α ⇒ bool . ∀x :: α . f x ≠ S

Viewing types as sets, α ⇒ bool represents the powerset of α. This version states that for every function from α to its powerset, some subset is outside its range.

The Isabelle proof uses HOL’s set theory, with the type α set and the operator range. The set S is given as an unknown instead of a quantified variable so that we may inspect the subset found by the proof.

      goal Set.thy "?S ~: range(f :: 'a=>'a set)";
        Level 0
        ?S ~: range f
         1. ?S ~: range f

The first two steps are routine. The rule rangeE replaces ?S ∈ range f by ?S = f x for some x.

      by (resolve_tac [notI] 1);
        Level 1
        ?S ~: range f
         1. ?S : range f ==> False
      by (eresolve_tac [rangeE] 1);
        Level 2
        ?S ~: range f
         1. !!x. ?S = f x ==> False

Next, we apply equalityCE, reasoning that since ?S = f x, we have ?c ∈ ?S if and only if ?c ∈ f x for any ?c.

      by (eresolve_tac [equalityCE] 1);
        Level 3
        ?S ~: range f
         1. !!x. [| ?c3 x : ?S; ?c3 x : f x |] ==> False
         2. !!x. [| ?c3 x ~: ?S; ?c3 x ~: f x |] ==> False

Now we use a bit of creativity. Suppose that ?S has the form of a comprehension. Then ?c ∈ {x . ?P x} implies ?P ?c. Destruct-resolution using CollectD instantiates ?S and creates the new assumption.

      by (dresolve_tac [CollectD] 1);
        Level 4
        {x. ?P7 x} ~: range f
         1. !!x. [| ?c3 x : f x; ?P7(?c3 x) |] ==> False
         2. !!x. [| ?c3 x ~: {x. ?P7 x}; ?c3 x ~: f x |] ==> False

Forcing a contradiction between the two assumptions of subgoal 1 completes the instantiation of S. It is now the set {x . x ∉ f x}, which is the standard diagonal construction.

      by (contr_tac 1);
        Level 5
        {x. x ~: f x} ~: range f
         1. !!x. [| x ~: {x. x ~: f x}; x ~: f x |] ==> False

The rest should be easy. To apply CollectI to the negated assumption, we

employ swap_res_tac:
      by (swap_res_tac [CollectI] 1);
        Level 6
        {x. x ~: f x} ~: range f
         1. !!x. [| x ~: f x; ~ False |] ==> x ~: f x
      by (assume_tac 1);
        Level 7
        {x. x ~: f x} ~: range f
        No subgoals!

How much creativity is required? As it happens, Isabelle can prove this theorem automatically. The default classical set !claset contains rules for most of the constructs of HOL’s set theory. We must augment it with equalityCE to break up set equalities, and then apply best-first search. Depth-first search would diverge, but best-first search successfully navigates through the large search space.

      choplev 0;
        Level 0
        ?S ~: range f
         1. ?S ~: range f
      by (best_tac (!claset addSEs [equalityCE]) 1);
        Level 1
        {x. x ~: f x} ~: range f
        No subgoals!

If you run this example interactively, make sure your current theory contains theory Set, for example by executing set_current_thy "Set". Otherwise the default claset may not contain the rules for set theory.