A Fixedpoint Approach to (Co)Inductive and (Co)Datatype Definitions^{∗}

Lawrence C. Paulson

              lcp@cl.cam.ac.uk

Computer Laboratory, University of Cambridge, England

1 October 2005

Abstract

This paper presents a fixedpoint approach to inductive definitions. Instead of using a syntactic test such as “strictly positive,” the approach lets definitions involve any operators that have been proved monotone. It is conceptually simple, which has allowed the easy implementation of mutual recursion and iterated definitions. It also handles coinductive definitions: simply replace the least fixedpoint by a greatest fixedpoint.

The method has been implemented in two of Isabelle’s logics, zf set theory and higher-order logic. It should be applicable to any logic in which the Knaster-Tarski theorem can be proved. Examples include lists of n elements, the accessible part of a relation and the set of primitive recursive functions. One example of a coinductive definition is bisimulations for lazy lists. Recursive datatypes are examined in detail, as well as one example of a codatatype: lazy lists.

The Isabelle package has been applied in several large case studies, including two proofs of the Church-Rosser theorem and a coinductive proof of semantic consistency. The package can be trusted because it proves theorems from definitions, instead of asserting desired properties as axioms.

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

∗J. Grundy and S. Thompson made detailed comments. Mads Tofte and the referees were also helpful. The research was funded by the SERC grants GR/G53279, GR/H40570 and by the ESPRIT Project 6453 “Types”.

Contents

1 Introduction 1

2 Fixedpoint operators 2

3 Elements of an inductive or coinductive definition 3 3.1 The form of the introduction rules . . . . . . . . . . . . . . . . 3 3.2 The fixedpoint definitions . . . . . . . . . . . . . . . . . . . . 4 3.3 Mutual recursion . . . . . . . . . . . . . . . . . . . . . . . . . 5 3.4 Proving the introduction rules . . . . . . . . . . . . . . . . . . 5 3.5 The case analysis rule . . . . . . . . . . . . . . . . . . . . . . . 6

4 Induction and coinduction rules 6 4.1 The basic induction rule . . . . . . . . . . . . . . . . . . . . . 7 4.2 Modified induction rules . . . . . . . . . . . . . . . . . . . . . 8 4.3 Coinduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8

5 Examples of inductive and coinductive definitions 9 5.1 The finite powerset operator . . . . . . . . . . . . . . . . . . . 9 5.2 Lists of n elements . . . . . . . . . . . . . . . . . . . . . . . . 10 5.3 Rule inversion: the function mk cases . . . . . . . . . . . . . 12 5.4 A coinductive definition: bisimulations on lazy lists . . . . . . 13 5.5 The accessible part of a relation . . . . . . . . . . . . . . . . . 14 5.6 The primitive recursive functions . . . . . . . . . . . . . . . . 15

6 Datatypes and codatatypes 18 6.1 Constructors and their domain . . . . . . . . . . . . . . . . . . 18 6.2 The case analysis operator . . . . . . . . . . . . . . . . . . . . 19 6.3 Example: lists and lazy lists . . . . . . . . . . . . . . . . . . . 20 6.4 Example: mutual recursion . . . . . . . . . . . . . . . . . . . . 21 6.5 Example: a four-constructor datatype . . . . . . . . . . . . . . 22 6.6 Proving freeness theorems . . . . . . . . . . . . . . . . . . . . 23

7 Related work 24

8 Conclusions and future work 25

1 Introduction

Several theorem provers provide commands for formalizing recursive data structures, like lists and trees. Robin Milner implemented one of the first of these, for Edinburgh lcf [15]. Given a description of the desired data structure, Milner’s package formulated appropriate definitions and proved the characteristic theorems. Similar is Melham’s recursive type package for the Cambridge hol system [14]. Such data structures are called datatypes below, by analogy with datatype declarations in Standard ml. Some logics take datatypes as primitive; consider Boyer and Moore’s shell principle [4] and the Coq type theory [21].

A datatype is but one example of an inductive definition. Such a definition [2] specifies the least set R closed under given rules: applying a rule to elements of R yields a result within R. Inductive definitions have many applications. The collection of theorems in a logic is inductively defined. A structural operational semantics [12] is an inductive definition of a reduction or evaluation relation on programs. A few theorem provers provide commands for formalizing inductive definitions; these include Coq [21] and again the hol system [5].

The dual notion is that of a coinductive definition. Such a 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. Important examples include using bisimulation relations to formalize equivalence of processes [16] or lazy functional programs [1]. Other examples include lazy lists and other infinite data structures; these are called codatatypes below.

Not all inductive definitions are meaningful. Monotone inductive definitions are a large, well-behaved class. Monotonicity can be enforced by syntactic conditions such as “strictly positive,” but this could lead to monotone definitions being rejected on the grounds of their syntactic form. More flexible is to formalize monotonicity within the logic and allow users to prove it.

This paper describes a package based on a fixedpoint approach. Least fixedpoints yield inductive definitions; greatest fixedpoints yield coinductive definitions. Most of the discussion below applies equally to inductive and coinductive definitions, and most of the code is shared.

The package supports mutual recursion and infinitely-branching datatypes and codatatypes. It allows use of any operators that have been proved monotone, thus accepting all provably monotone inductive definitions, including iterated definitions.

The package has been implemented in Isabelle [28, 24] using zf set theory [23, 25]; part of it has since been ported to Isabelle/hol (higher-order logic). The recursion equations are specified as introduction rules for the mutually recursive sets. The package transforms these rules into a mapping over sets, and attempts to prove that the mapping is monotonic and welltyped. If successful, the package makes fixedpoint definitions and proves the introduction, elimination and (co)induction rules. Users invoke the package by making simple declarations in Isabelle theory files.

Most datatype packages equip the new datatype with some means of expressing recursive functions. This is the main omission from my package. Its fixedpoint operators define only recursive sets. The Isabelle/zf theory provides well-founded recursion [25], which is harder to use than structural recursion but considerably more general. Slind [33] has written a package to automate the definition of well-founded recursive functions in Isabelle/hol.

Outline. Section 2 introduces the least and greatest fixedpoint operators. Section 3 discusses the form of introduction rules, mutual recursion and other points common to inductive and coinductive definitions. Section 4 discusses induction and coinduction rules separately. Section 5 presents several examples, including a coinductive definition. Section 6 describes datatype definitions. Section 7 presents related work. Section 8 draws brief conclusions. The appendices are simple user’s manuals for this Isabelle package.

Most of the definitions and theorems shown below have been generated by the package. I have renamed some variables to improve readability.

2 Fixedpoint operators

In set theory, the least and greatest fixedpoint operators are defined as follows:

lfp(D, h) ≡ ⋂{X ⊆ D . h(X ) ⊆ X }
gfp(D, h) ≡ ⋃{X ⊆ D . X ⊆ h(X )}

Let D be a set. Say that h is bounded by D if h(D) ⊆ D, and monotone below D if h(A) ⊆ h(B) for all A and B such that A ⊆ B ⊆ D. If h is bounded by D and monotone then both operators yield fixedpoints:

lfp(D, h) = h(lfp(D, h))
gfp(D, h) = h(gfp(D, h))

These equations are instances of the Knaster-Tarski theorem, which states that every monotonic function over a complete lattice has a fixedpoint [6]. It is obvious from their definitions that lfp must be the least fixedpoint, and gfp the greatest.

This fixedpoint theory is simple. The Knaster-Tarski theorem is easy to prove. Showing monotonicity of h is trivial, in typical cases. We must also exhibit a bounding set D for h. Frequently this is trivial, as when a set of theorems is (co)inductively defined over some previously existing set of formulæ. Isabelle/zf provides suitable bounding sets for infinitely-branching (co)datatype definitions; see §6.1. Bounding sets are also called domains.

The powerset operator is monotone, but by Cantor’s theorem there is no set A such that A = P(A). We cannot put A = lfp(D, P) because there is no suitable domain D. But §5.5 demonstrates that P is still useful in inductive definitions.

3 Elements of an inductive or coinductive definition

Consider a (co)inductive definition of the sets R_{1}, …, R_{n}, in mutual recursion. They will be constructed from domains D_{1}, …, D_{n}, respectively. The construction yields not R_{i} ⊆ D_{i} but R_{i} ⊆ D_{1} + ⋯ + D_{n}, where R_{i} is contained in the image of D_{i} under an injection. Reasons for this are discussed elsewhere [25, §4.5].

The definition may involve arbitrary parameters p⃗ = p_{1}, …, p_{k}. Each recursive set then has the form R_{i}(p⃗). The parameters must be identical every time they occur within a definition. This would appear to be a serious restriction compared with other systems such as Coq [21]. For instance, we cannot define the lists of n elements as the set listn(A, n) using rules where the parameter n varies. Section 5.2 describes how to express this set using the inductive definition package.

To avoid clutter below, the recursive sets are shown as simply R_{i} instead of R_{i}(p⃗).

3.1 The form of the introduction rules

The body of the definition consists of the desired introduction rules. The conclusion of each rule must have the form t ∈ R_{i}, where t is any term. Premises typically have the same form, but they can have the more general form t ∈ M (R_{i}) or express arbitrary side-conditions.

The premise t ∈ M (R_{i}) is permitted if M is a monotonic operator on sets, satisfying the rule

{A ⊆ B \atop M (A) ⊆ M (B)}

The user must supply the package with monotonicity rules for all such premises.

The ability to introduce new monotone operators makes the approach flexible. A suitable choice of M and t can express a lot. The powerset operator P is monotone, and the premise t ∈ P(R) expresses t ⊆ R; see §5.5 for an example. The list of operator is monotone, as is easily proved by induction. The premise t ∈ list(R) avoids having to encode the effect of list(R) using mutual recursion; see §5.6 and also my earlier paper [25, §4.4].

Introduction rules may also contain side-conditions. These are premises consisting of arbitrary formulæ not mentioning the recursive sets. Sideconditions typically involve type-checking. One example is the premise a ∈ A in the following rule from the definition of lists:

a ∈ A l ∈ list(A)

Cons(a, l) ∈ list(A)

3.2 The fixedpoint definitions

The package translates the list of desired introduction rules into a fixedpoint definition. Consider, as a running example, the finite powerset operator Fin(A): the set of all finite subsets of A. It can be defined as the least set closed under the rules

∅ ∈ Fin(A) \begin{matrix}a ∈ A & b ∈ Fin(A) \\ \{a\} ∪ b ∈ Fin(A) \end{matrix}

The domain in a (co)inductive definition must be some existing set closed under the rules. A suitable domain for Fin(A) is P(A), the set of all subsets of A. The package generates the definition

Fin(A) ≡ lfp(P(A), λX . {z ∈ P(A). z = ∅ ∨ (∃a b . z = {a} ∪ b ∧ a ∈ A ∧ b ∈ X )})

The contribution of each rule to the definition of Fin(A) should be obvious. A coinductive definition is similar but uses gfp instead of lfp.

The package must prove that the fixedpoint operator is applied to a monotonic function. If the introduction rules have the form described above, and if the package is supplied a monotonicity theorem for every t ∈ M (R_{i}) premise, then this proof is trivial.^{1}

The package returns its result as an ml structure, which consists of named components; we may regard it as a record. The result structure contains the definitions of the recursive sets as a theorem list called defs. It also contains some theorems; dom subset is an inclusion such as Fin(A) ⊆ P(A), while bnd mono asserts that the fixedpoint definition is monotonic.

Internally the package uses the theorem unfold, a fixedpoint equation such as

Fin(A) = {z ∈ P(A). z = ∅ ∨
(∃a b . z = {a} ∪ b ∧ a ∈ A ∧ b ∈ Fin(A))}

In order to save space, this theorem is not exported.

3.3 Mutual recursion

In a mutually recursive definition, the domain of the fixedpoint construction is the disjoint sum of the domain D_{i} of each R_{i}, for i = 1, …, n. The package uses the injections of the binary disjoint sum, typically Inl and Inr, to express injections h_{1n}, …, h_{nn} for the n-ary disjoint sum D_{1} + ⋯ + D_{n}.

As discussed elsewhere [25, §4.5], Isabelle/zf defines the operator Part to support mutual recursion. The set Part(A, h) contains those elements of A having the form h(z):

Part(A, h) ≡ {x ∈ A . ∃z . x = h(z)}.

For mutually recursive sets R_{1}, …, R_{n} with n > 1, the package makes n + 1 definitions. The first defines a set R using a fixedpoint operator. The remaining n definitions have the form

R_{i} ≡ Part(R, h_{in}), i = 1, …, n.

It follows that R = R_{1} ∪ ⋯ ∪ R_{n}, where the R_{i} are pairwise disjoint.

3.4 Proving the introduction rules

The user supplies the package with the desired form of the introduction rules. Once it has derived the theorem unfold, it attempts to prove those rules.

1Due to the presence of logical connectives in the fixedpoint’s body, the monotonicity proof requires some unusual rules. These state that the connectives ∧, ∨ and ∃ preserve monotonicity with respect to the partial ordering on unary predicates given by P ⊑ Q if and only if ∀x . P(x) → Q(x).

From the user’s point of view, this is the trickiest stage; the proofs often fail. The task is to show that the domain D_{1} + ⋯ + D_{n} of the combined set R_{1} ∪ ⋯ ∪ R_{n} is closed under all the introduction rules. This essentially involves replacing each R_{i} by D_{1} + ⋯ + D_{n} in each of the introduction rules and attempting to prove the result.

Consider the Fin(A) example. After substituting P(A) for Fin(A) in the rules, the package must prove

∅ ∈ P(A) \begin{matrix}a ∈ A & b ∈ P(A) \\ \{a\} ∪ b ∈ P(A) \end{matrix}

Such proofs can be regarded as type-checking the definition.^{2} The user supplies the package with type-checking rules to apply. Usually these are general purpose rules from the zf theory. They could however be rules specifically proved for a particular inductive definition; sometimes this is the easiest way to get the definition through!

The result structure contains the introduction rules as the theorem list

intrs.

3.5 The case analysis rule

The elimination rule, called elim, performs case analysis. It is a simple consequence of unfold. There is one case for each introduction rule. If x ∈ Fin(A) then either x = ∅ or else x = {a} ∪ b for some a ∈ A and b ∈ Fin(A). Formally, the elimination rule for Fin(A) is written

x ∈ Fin(A)

[x = ∅] ; ⋮ . ; Q

[x = {a} ∪ b a ∈ A b ∈ Fin(A)]_{a,b}

⋮ . Q

Q

The subscripted variables a and b above the third premise are eigenvariables, subject to the usual “not free in … ” proviso.

4 Induction and coinduction rules

Here we must consider inductive and coinductive definitions separately. For an inductive definition, the package returns an induction rule derived directly from the properties of least fixedpoints, as well as a modified rule for mutual recursion. For a coinductive definition, the package returns a basic coinduction rule.

2The Isabelle/hol version does not require these proofs, as hol has implicit typechecking.

4.1 The basic induction rule

The basic rule, called induct, is appropriate in most situations. For inductive definitions, it is strong rule induction [5]; for datatype definitions (see below), it is just structural induction.

The induction rule for an inductively defined set R has the form described below. For the time being, assume that R’s domain is not a Cartesian product; inductively defined relations are treated slightly differently.

The major premise is x ∈ R. There is a minor premise for each introduction rule:

• If the introduction rule concludes t ∈ R_{i}, then the minor premise is P(t).

• The minor premise’s eigenvariables are precisely the introduction rule’s free variables that are not parameters of R. For instance, the eigenvariables in the Fin(A) rule below are a and b, but not A.

• If the introduction rule has a premise t ∈ R_{i}, then the minor premise discharges the assumption t ∈ R_{i} and the induction hypothesis P(t). If the introduction rule has a premise t ∈ M (R_{i}) then the minor premise discharges the single assumption

t ∈ M ({z ∈ R_{i} . P(z)}).

Because M is monotonic, this assumption implies t ∈ M (R_{i}). The occurrence of P gives the effect of an induction hypothesis, which may be exploited by appealing to properties of M .

The induction rule for Fin(A) resembles the elimination rule shown above, but includes an induction hypothesis:

x ∈ Fin(A) P(∅)

[a ∈ A b ∈ Fin(A) P(b)]_{a,b}
⋮ .
P({a} ∪ b)

P(x)

Stronger induction rules often suggest themselves. We can derive a rule for Fin(A) whose third premise discharges the extra assumption a ∉ b. The package provides rules for mutual induction and inductive relations. The Isabelle/zf theory also supports well-founded induction and recursion over datatypes, by reasoning about the rank of a set [25, §3.4].

4.2 Modified induction rules

If the domain of R is a Cartesian product A_{1}×⋯×A_{m} (however nested), then the corresponding predicate P_{i} takes m arguments. The major premise becomes ⟨z_{1}, …, z_{m}⟩ ∈ R instead of x ∈ R; the conclusion becomes P(z_{1}, …, z_{m}). This simplifies reasoning about inductively defined relations, eliminating the need to express properties of z_{1}, …, z_{m} as properties of the tuple ⟨z_{1}, …, z_{m}⟩. Occasionally it may require you to split up the induction variable using SigmaE and dom subset, especially if the constant split appears in the rule.

The mutual induction rule is called mutual induct. It differs from the basic rule in two respects:

• Instead of a single predicate P, it uses n predicates P_{1}, …, P_{n}: one for each recursive set.

• There is no major premise such as x ∈ R_{i}. Instead, the conclusion refers to all the recursive sets:

(∀z . z ∈ R_{1} → P_{1}(z)) ∧ ⋯ ∧ (∀z . z ∈ R_{n} → P_{n}(z))

Proving the premises establishes P_{i}(z) for z ∈ R_{i} and i = 1, …, n.

If the domain of some R_{i} is a Cartesian product, then the mutual induction rule is modified accordingly. The predicates are made to take m separate arguments instead of a tuple, and the quantification in the conclusion is over the separate variables z_{1}, …, z_{m}.

4.3 Coinduction

A coinductive definition yields a primitive coinduction rule, with no refinements such as those for the induction rules. (Experience may suggest refinements later.) Consider the codatatype of lazy lists as an example. For suitable definitions of LNil and LCons, lazy lists may be defined as the greatest set consistent with the rules

           LNil ∈ llist(A) a ∈ A l ∈ llist(A) LCons(a, l) ∈ llist(A) (−)

The (−) tag stresses that this is a coinductive definition. A suitable domain for llist(A) is quniv(A); this set is closed under the variant forms of sum and product that are used to represent non-well-founded data structures (see §6.1).

The package derives an unfold theorem similar to that for Fin(A). Then it proves the theorem coinduct, which expresses that llist(A) is the greatest solution to this equation contained in quniv(A):

x ∈ X X ⊆ quniv(A)

[z ∈ X ]_{z} ; ⋮ .

z = LNil ∨ (∃a l. z = LCons(a, l) ∧ a ∈ A ∧

l ∈ X ∪ llist(A))

                         x ∈ llist(A)

This rule complements the introduction rules; it provides a means of showing x ∈ llist(A) when x is infinite. For instance, if x = LCons(0, x) then applying the rule with X = {x} proves x ∈ llist(nat). (Here nat is the set of natural numbers.)

Having X ∪ llist(A) instead of simply X in the third premise above represents a slight strengthening of the greatest fixedpoint property. I discuss several forms of coinduction rules elsewhere [26].

The clumsy form of the third premise makes the rule hard to use, especially in large definitions. Probably a constant should be declared to abbreviate the large disjunction, and rules derived to allow proving the separate disjuncts.

5 Examples of inductive and coinductive definitions

This section presents several examples from the literature: the finite powerset operator, lists of n elements, bisimulations on lazy lists, the well-founded part of a relation, and the primitive recursive functions.

5.1 The finite powerset operator

This operator has been discussed extensively above. Here is the corresponding invocation in an Isabelle theory file. Note that cons(a, b) abbreviates {a} ∪ b in Isabelle/zf.

      Finite = Arith +
      consts      Fin :: i=>i
      inductive
        domains   "Fin(A)" <= "Pow(A)"
        intrs
          emptyI  "0 : Fin(A)"
          consI   "[| a: A;  b: Fin(A) |] ==> cons(a,b) : Fin(A)"
        type_intrs  empty_subsetI, cons_subsetI, PowI
        type_elims "[make_elim PowD]"
      end

Theory Finite extends the parent theory Arith by declaring the unary function symbol Fin, which is defined inductively. Its domain is specified as P(A), where A is the parameter appearing in the introduction rules. For type-checking, we supply two introduction rules:

∅ ⊆ A \begin{matrix}a ∈ C & B ⊆ C \\ \{a\} ∪ B ⊆ C \end{matrix}

A further introduction rule and an elimination rule express both directions of the equivalence A ∈ P(B) ↔ A ⊆ B. Type-checking involves mostly introduction rules.

Like all Isabelle theory files, this one yields a structure containing the new theory as an ml value. Structure Finite also has a substructure, called Fin. After declaring open Finite; we can refer to the Fin(A) introduction rules as the list Fin.intrs or individually as Fin.emptyI and Fin.consI. The induction rule is Fin.induct.

5.2 Lists of n elements

This has become a standard example of an inductive definition. Following Paulin-Mohring [21], we could attempt to define a new datatype listn(A, n), for lists of length n, as an n-indexed family of sets. But her introduction rules

Niln ∈ listn(A, 0) \begin{matrix}n ∈ nat & a ∈ A & l ∈ listn(A, n) \\ Consn(n, a, l) ∈ listn(A, succ(n)) \end{matrix}

are not acceptable to the inductive definition package: listn occurs with three different parameter lists in the definition.

The Isabelle version of this example suggests a general treatment of varying parameters. It uses the existing datatype definition of list(A), with constructors Nil and Cons, and incorporates the parameter n into the inductive set itself. It defines listn(A) as a relation consisting of pairs ⟨n, l⟩ such that n ∈ nat and l ∈ list(A) and l has length n. In fact, listn(A) is the converse of the length function on list(A). The Isabelle/zf introduction rules are

⟨0, Nil⟩ ∈ listn(A) \begin{matrix}a ∈ A & ⟨n, l⟩ ∈ listn(A) \\ ⟨succ(n), Cons(a, l)⟩ ∈ listn(A) \end{matrix}

The Isabelle theory file takes, as parent, the theory List of lists. We declare the constant listn and supply an inductive definition, specifying the domain

as nat × list(A):
      ListN = List +
      consts  listn :: i=>i
      inductive
        domains   "listn(A)" <= "nat*list(A)"
        intrs
          NilI  "<0,Nil>: listn(A)"
          ConsI "[| a:A; <n,l>:listn(A) |] ==> <succ(n), Cons(a,l)>: listn(A)"
        type_intrs "nat_typechecks @ list.intrs"
      end

The type-checking rules include those for 0, succ, Nil and Cons. Because listn(A) is a set of pairs, type-checking requires the equivalence ⟨a, b⟩ ∈ A × B ↔ a ∈ A ∧ b ∈ B. The package always includes the rules for ordered pairs.

The package returns introduction, elimination and induction rules for listn. The basic induction rule, listn.induct, is

⟨z_{1}, z_{2}⟩ ∈ listn(A) P(0, Nil)

[a ∈ A ⟨n, l⟩ ∈ listn(A) P(n, l)]_{a,l,n}
⋮ .

P(succ(n), Cons(a, l))

P(z_{1}, z_{2})

This rule lets the induction formula to be a binary property of pairs, P(n, l). It is now a simple matter to prove theorems about listn(A), such as

∀l ∈ list(A) . ⟨length(l), l⟩ ∈ listn(A)

listn(A)“{n} = {l ∈ list(A) . length(l) = n}

This latter result — here r“X denotes the image of X under r — asserts that the inductive definition agrees with the obvious notion of n-element list.

A “list of n elements” really is a list, namely an element of list(A). It is subject to list operators such as append (concatenation). For example, a trivial induction on ⟨m, l⟩ ∈ listn(A) yields

⟨m, l⟩ ∈ listn(A) ⟨m′, l′⟩ ∈ listn(A)
⟨m + m′, l@l′⟩ ∈ listn(A)

where + denotes addition on the natural numbers and @ denotes append.

5.3 Rule inversion: the function mk cases

The elimination rule, listn.elim, is cumbersome:

     x ∈ listn(A)

[x = ⟨0, Nil⟩] ; ⋮ . ; Q

[ \begin{matrix}x = ⟨succ(n), Cons(a, l)⟩ \\ a ∈ A \\ ⟨n, l⟩ ∈ listn(A) \end{matrix} ]_{a,l,n}

⋮ . Q

Q

The ml function listn.mk cases generates simplified instances of this rule. It works by freeness reasoning on the list constructors: Cons(a, l) is injective in its two arguments and differs from Nil. If x is ⟨i, Nil⟩ or ⟨i, Cons(a, l)⟩ then listn.mk cases deduces the corresponding form of i; this is called rule inversion. Here is a sample session:

      listn.mk_cases "<i,Nil> : listn(A)";
        "[| <?i, []> : listn(?A); ?i = 0 ==> ?Q |] ==> ?Q" : thm
      listn.mk_cases "<i,Cons(a,l)> : listn(A)";
        "[| <?i, Cons(?a, ?l)> : listn(?A);
            !!n. [| ?a : ?A; <n, ?l> : listn(?A); ?i = succ(n) |] ==> ?Q
         |] ==> ?Q" : thm

Each of these rules has only two premises. In conventional notation, the second rule is

⟨i, Cons(a, l)⟩ ∈ listn(A)

[ \begin{matrix}a ∈ A \\ ⟨n, l⟩ ∈ listn(A) \\ i = succ(n) \end{matrix} ]_{n}

⋮ . Q

Q

The package also has built-in rules for freeness reasoning about 0 and succ. So if x is ⟨0, l⟩ or ⟨succ(i), l⟩, then listn.mk cases can deduce the corresponding form of l.

The function mk cases is also useful with datatype definitions. The instance from the definition of lists, namely list.mk cases, can prove that Cons(a, l) ∈ list(A) implies a ∈ A and l ∈ list(A):

Cons(a, l) ∈ list(A)

[a ∈ A l ∈ list(A)]

⋮ . Q

Q A typical use of mk cases concerns inductive definitions of evaluation relations. Then rule inversion yields case analysis on possible evaluations. For example, Isabelle/zf includes a short proof of the diamond property for parallel contraction on combinators. Ole Rasmussen used mk cases extensively in his development of the theory of residuals [31].

5.4 A coinductive definition: bisimulations on lazy lists

This example anticipates the definition of the codatatype llist(A), which consists of finite and infinite lists over A. Its constructors are LNil and LCons, satisfying the introduction rules shown in §4.3. Because llist(A) is defined as a greatest fixedpoint and uses the variant pairing and injection operators, it contains non-well-founded elements such as solutions to LCons(a, l) = l.

The next step in the development of lazy lists is to define a coinduction principle for proving equalities. This is done by showing that the equality relation on lazy lists is the greatest fixedpoint of some monotonic operation. The usual approach [30] is to define some notion of bisimulation for lazy lists, define equivalence to be the greatest bisimulation, and finally to prove that two lazy lists are equivalent if and only if they are equal. The coinduction rule for equivalence then yields a coinduction principle for equalities.

A binary relation R on lazy lists is a bisimulation provided R ⊆ R^{+}, where R^{+} is the relation

{⟨LNil, LNil⟩} ∪ {⟨LCons(a, l), LCons(a, l′)⟩ . a ∈ A ∧ ⟨l, l′⟩ ∈ R}.

A pair of lazy lists are equivalent if they belong to some bisimulation. Equivalence can be coinductively defined as the greatest fixedpoint for the introduction rules

⟨LNil, LNil⟩ ∈ lleq(A) a ∈ A ⟨l, l′⟩ ∈ lleq(A) ⟨LCons(a, l), LCons(a, l′)⟩ ∈ lleq(A) (−)

To make this coinductive definition, the theory file includes (after the declaration of llist(A)) the following lines:

   consts    lleq :: i=>i
   coinductive
     domains "lleq(A)" <= "llist(A) * llist(A)"
     intrs
       LNil  "<LNil,LNil> : lleq(A)"
       LCons "[| a:A; <l,l'>:lleq(A) |] ==> <LCons(a,l),LCons(a,l')>: lleq(A)"
     type_intrs  "llist.intrs"

The domain of lleq(A) is llist(A)×llist(A). The type-checking rules include the introduction rules for llist(A), whose declaration is discussed below (§6.3).

The package returns the introduction rules and the elimination rule, as usual. But instead of induction rules, it returns a coinduction rule. The rule is too big to display in the usual notation; its conclusion is x ∈ lleq(A) and its premises are x ∈ X , X ⊆ llist(A) × llist(A) and

[z ∈ X ]_{z} ; ⋮ .

z = ⟨LNil, LNil⟩ ∨ (∃a l l′ . z = ⟨LCons(a, l), LCons(a, l′)⟩ ∧ a ∈ A ∧ ⟨l, l′⟩ ∈ X ∪ lleq(A))

Thus if x ∈ X , where X is a bisimulation contained in the domain of lleq(A), then x ∈ lleq(A). It is easy to show that lleq(A) is reflexive: the equality relation is a bisimulation. And lleq(A) is symmetric: its converse is a bisimulation. But showing that lleq(A) coincides with the equality relation takes some work.

5.5 The accessible part of a relation

Let ≺ be a binary relation on D; in short, (≺) ⊆ D × D. The accessible or well-founded part of ≺, written acc(≺), is essentially that subset of D for which ≺ admits no infinite decreasing chains [2]. Formally, acc(≺) is inductively defined to be the least set that contains a if it contains all ≺- predecessors of a, for a ∈ D. Thus we need an introduction rule of the form

∀y . y ≺ a → y ∈ acc(≺)
a ∈ acc(≺)

Paulin-Mohring treats this example in Coq [21], but it causes difficulties for other systems. Its premise is not acceptable to the inductive definition package of the Cambridge hol system [5]. It is also unacceptable to the Isabelle package (recall §3.1), but fortunately can be transformed into the acceptable form t ∈ M (R).

The powerset operator is monotonic, and t ∈ P(R) is equivalent to t ⊆ R. This in turn is equivalent to ∀y ∈ t . y ∈ R. To express ∀y . y ≺ a → y ∈ acc(≺) we need only find a term t such that y ∈ t if and only if y ≺ a. A suitable t is the inverse image of {a} under ≺.

The definition below follows this approach. Here r is ≺ and field(r) refers to D, the domain of acc(r). (The field of a relation is the union of its domain and range.) Finally r^{−}“{a} denotes the inverse image of {a} under r. We supply the theorem Pow mono, which asserts that P is monotonic.

      consts    acc :: i=>i
      inductive
        domains "acc(r)" <= "field(r)"
        intrs
          vimage  "[| r-``{a}: Pow(acc(r)); a: field(r) |] ==> a: acc(r)"
        monos      Pow_mono

The Isabelle theory proceeds to prove facts about acc(≺). For instance, ≺ is well-founded if and only if its field is contained in acc(≺).

As mentioned in §4.1, a premise of the form t ∈ M (R) gives rise to an unusual induction hypothesis. Let us examine the induction rule, acc.induct:

x ∈ acc(r)

[ \begin{matrix}r^{−}“\{a\} & ∈ P(\{z ∈ acc(r) . P(z)\}) \\ a & ∈ field(r) \end{matrix} ]_{a}

⋮ . P(a)

P(x)

The strange induction hypothesis is equivalent to ∀y . ⟨y, a⟩ ∈ r → y ∈ acc(r) ∧ P(y). Therefore the rule expresses well-founded induction on the accessible part of ≺.

The use of inverse image is not essential. The Isabelle package can accept introduction rules with arbitrary premises of the form ∀y⃗ . P(y⃗) → f (y⃗) ∈ R. The premise can be expressed equivalently as

{z ∈ D . P(y⃗) ∧ z = f (y⃗)} ∈ P(R)

provided f (y⃗) ∈ D for all y⃗ such that P(y⃗). The following section demonstrates another use of the premise t ∈ M (R), where M = list.

5.6 The primitive recursive functions

The primitive recursive functions are traditionally defined inductively, as a subset of the functions over the natural numbers. One difficulty is that functions of all arities are taken together, but this is easily circumvented by regarding them as functions on lists. Another difficulty, the notion of composition, is less easily circumvented.

Here is a more precise definition. Letting x⃗ abbreviate x_{0}, …, x_{n−1}, we can write lists such as [x⃗], [y + 1, x⃗], etc. A function is primitive recursive if it belongs to the least set of functions in list(nat) → nat containing

• The successor function SC, such that SC[y, x⃗] = y + 1.

• All constant functions CONST(k), such that CONST(k)[x⃗] = k.

• All projection functions PROJ(i), such that PROJ(i)[x⃗] = x_{i} if 0 ≤ i < n.

• All compositions COMP(g, [f_{0}, …, f_{m−1}]), where g and f_{0}, …, f_{m−1} are primitive recursive, such that

COMP(g, [f_{0}, …, f_{m−1}])[x⃗] = g[f_{0}[x⃗], …, f_{m−1}[x⃗]].

• All recursions PREC(f , g), where f and g are primitive recursive, such that

PREC(f , g)[0, x⃗] = f [x⃗]
PREC(f , g)[y + 1, x⃗] = g[PREC(f , g)[y, x⃗], y, x⃗].

Composition is awkward because it combines not two functions, as is usual, but m + 1 functions. In her proof that Ackermann’s function is not primitive recursive, Nora Szasz was unable to formalize this definition directly [34]. So she generalized primitive recursion to tuple-valued functions. This modified the inductive definition such that each operation on primitive recursive functions combined just two functions.

Szasz was using alf, but Coq and hol would also have problems accepting this definition. Isabelle’s package accepts it easily since [f_{0}, …, f_{m−1}] is a list of primitive recursive functions and list is monotonic. There are five introduction rules, one for each of the five forms of primitive recursive function. Let us examine the one for COMP:

                 g ∈ primrec fs ∈ list(primrec)

                      COMP(g, fs) ∈ primrec

The induction rule for primrec has one case for each introduction rule. Due to the use of list as a monotone operator, the composition case has an unusual induction hypothesis:

[g ∈ primrec fs ∈ list({z ∈ primrec . P(z)})]_{fs,g}
⋮ .

P(COMP(g, fs))

The hypothesis states that fs is a list of primitive recursive functions, each satisfying the induction formula. Proving the COMP case typically requires structural induction on lists, yielding two subcases: either fs = Nil or else fs = Cons(f , fs′), where f ∈ primrec, P(f ), and fs′ is another list of primitive recursive functions satisfying P.

Primrec_defs = Main +
consts SC :: i

⋮

defs
 SC_def    "SC == lam l:list(nat).list_case(0, %x xs.succ(x), l)"

⋮

end
Primrec = Primrec_defs +
consts prim_rec :: i
inductive
 domains "primrec" <= "list(nat)->nat"
 intrs
   SC     "SC : primrec"
   CONST  "k: nat ==> CONST(k) : primrec"
   PROJ   "i: nat ==> PROJ(i) : primrec"
   COMP   "[| g: primrec; fs: list(primrec) |] ==> COMP(g,fs): primrec"
   PREC   "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec"
 monos       list_mono
 con_defs    SC_def, CONST_def, PROJ_def, COMP_def, PREC_def
 type_intrs "nat_typechecks @ list.intrs @
             [lam_type, list_case_type, drop_type, map_type,
              apply_type, rec_type]"
end

Figure 1: Inductive definition of the primitive recursive functions

Figure 1 presents the theory file. Theory Primrec defines the constants SC, CONST, etc. These are not constructors of a new datatype, but functions over lists of numbers. Their definitions, most of which are omitted, consist of routine list programming. In Isabelle/zf, the primitive recursive functions are defined as a subset of the function set list(nat) → nat.

The Isabelle theory goes on to formalize Ackermann’s function and prove that it is not primitive recursive, using the induction rule primrec.induct. The proof follows Szasz’s excellent account.

6 Datatypes and codatatypes

A (co)datatype definition is a (co)inductive definition with automatically defined constructors and a case analysis operator. The package proves that the case operator inverts the constructors and can prove freeness theorems involving any pair of constructors.

6.1 Constructors and their domain

A (co)inductive definition selects a subset of an existing set; a (co)datatype definition creates a new set. The package reduces the latter to the former. Isabelle/zf supplies sets having strong closure properties to serve as domains for (co)inductive definitions.

Isabelle/zf defines the Cartesian product A×B, containing ordered pairs ⟨a, b⟩; it also defines the disjoint sum A + B, containing injections Inl(a) ≡ ⟨0, a⟩ and Inr(b) ≡ ⟨1, b⟩. For use below, define the m-tuple ⟨x_{1}, …, x_{m}⟩ to be the empty set ∅ if m = 0, simply x_{1} if m = 1 and ⟨x_{1}, ⟨x_{2}, …, x_{m}⟩⟩ if m ≥ 2.

A datatype constructor Con(x_{1}, …, x_{m}) is defined to be h(⟨x_{1}, …, x_{m}⟩), where h is composed of Inl and Inr. In a mutually recursive definition, all constructors for the set R_{i} have the outer form h_{in}, where h_{in} is the injection described in §3.3. Further nested injections ensure that the constructors for R_{i} are pairwise distinct.

Isabelle/zf defines the set univ(A), which contains A and furthermore contains ⟨a, b⟩, Inl(a) and Inr(b) for a, b ∈ univ(A). In a typical datatype definition with set parameters A_{1}, …, A_{k}, a suitable domain for all the recursive sets is univ(A_{1}∪⋯∪A_{k}). This solves the problem for datatypes [25, §4.2].

The standard pairs and injections can only yield well-founded constructions. This eases the (manual!) definition of recursive functions over datatypes. But they are unsuitable for codatatypes, which typically contain nonwell-founded objects.

To support codatatypes, Isabelle/zf defines a variant notion of ordered pair, written ⟨a; b⟩. It also defines the corresponding variant notion of Cartesian product A ⊗ B, variant injections QInl(a) and QInr(b) and variant disjoint sum A ⊕ B. Finally it defines the set quniv(A), which contains A and furthermore contains ⟨a; b⟩, QInl(a) and QInr(b) for a, b ∈ quniv(A). In a typical codatatype definition with set parameters A_{1}, …, A_{k}, a suitable domain is quniv(A_{1} ∪ ⋯ ∪ A_{k}). Details are published elsewhere [27].

6.2 The case analysis operator

The (co)datatype package automatically defines a case analysis operator, called R case. A mutually recursive definition still has only one operator, whose name combines those of the recursive sets: it is called R_{1} ... R_{n} case. The case operator is analogous to those for products and sums.

Datatype definitions employ standard products and sums, whose operators are split and case and satisfy the equations

split(f , ⟨x, y⟩) = f (x, y)
case(f , g, Inl(x)) = f (x)
case(f , g, Inr(y)) = g(y)

Suppose the datatype has k constructors Con_{1}, …, Con_{k}. Then its case operator takes k +1 arguments and satisfies an equation for each constructor:

R case(f_{1}, …, f_{k}, Con_{i}(x⃗)) = f_{i}(x⃗), i = 1, …, k

The case operator’s definition takes advantage of Isabelle’s representation of syntax in the typed λ-calculus; it could readily be adapted to a theorem prover for higher-order logic. If f and g have meta-type i ⇒ i then so do split(f ) and case(f , g). This works because split and case operate on their last argument. They are easily combined to make complex case analysis operators. For example, case(f , case(g, h)) performs case analysis for A + (B + C ); let us verify one of the three equations:

case(f , case(g, h), Inr(Inl(b))) = case(g, h, Inl(b)) = g(b)

Codatatype definitions are treated in precisely the same way. They express case operators using those for the variant products and sums, namely qsplit

and qcase.

To see how constructors and the case analysis operator are defined, let us examine some examples. Further details are available elsewhere [25].

6.3 Example: lists and lazy lists

Here is a declaration of the datatype of lists, as it might appear in a theory file:

      consts  list :: i=>i
      datatype "list(A)" = Nil | Cons ("a:A", "l: list(A)")

And here is a declaration of the codatatype of lazy lists:

      consts  llist :: i=>i
      codatatype "llist(A)" = LNil | LCons ("a: A", "l: llist(A)")

Each form of list has two constructors, one for the empty list and one for adding an element to a list. Each takes a parameter, defining the set of lists over a given set A. Each is automatically given the appropriate domain: univ(A) for list(A) and quniv(A) for llist(A). The default can be overridden.

Since list(A) is a datatype, it has a structural induction rule, list.induct:

x ∈ list(A) P(Nil)

[a ∈ A l ∈ list(A) P(l)]_{a,l}
⋮ .
P(Cons(a, l))

P(x)

Induction and freeness yield the law l ≠ Cons(a, l). To strengthen this, Isabelle/zf defines the rank of a set and proves that the standard pairs and injections have greater rank than their components. An immediate consequence, which justifies structural recursion on lists [25, §4.3], is

                    rank(l) < rank(Cons(a, l)).

But llist(A) is a codatatype and has no induction rule. Instead it has the coinduction rule shown in §4.3. Since variant pairs and injections are monotonic and need not have greater rank than their components, fixedpoint operators can create cyclic constructions. For example, the definition

              lconst(a) ≡ lfp(univ(a), λl . LCons(a, l))

yields lconst(a) = LCons(a, lconst(a)).

It may be instructive to examine the definitions of the constructors and case operator for list(A). The definitions for llist(A) are similar. The list constructors are defined as follows:

                         Nil ≡ Inl(∅)

Cons(a, l) ≡ Inr(⟨a, l⟩)

The operator list case performs case analysis on these two alternatives:

              list case(c, h) ≡ case(λu . c, split(h))

Let us verify the two equations:

         list case(c, h, Nil) = case(λu . c, split(h), Inl(∅))

= (λu . c)(∅)
= c
list case(c, h, Cons(x, y)) = case(λu . c, split(h), Inr(⟨x, y⟩))
= split(h, ⟨x, y⟩)
= h(x, y)

6.4 Example: mutual recursion

In mutually recursive trees and forests [25, §4.5], trees have the one constructor Tcons, while forests have the two constructors Fnil and Fcons:

      consts  tree, forest, tree_forest    :: i=>i
      datatype "tree(A)"   = Tcons ("a: A",  "f: forest(A)")
      and      "forest(A)" = Fnil  |  Fcons ("t: tree(A)",  "f: forest(A)")

The three introduction rules define the mutual recursion. The distinguishing feature of this example is its two induction rules.

The basic induction rule is called tree forest.induct:

x ∈ tree forest(A)

[ \begin{matrix}a ∈ A \\ f ∈ forest(A) \\ P(f ) \end{matrix} ]_{a,f}
⋮ .

P(Tcons(a, f )) P(Fnil)

[ \begin{matrix}t ∈ tree(A) \\ P(t) \\ f ∈ forest(A) \\ P(f ) \end{matrix} ]_{t,f}

⋮ .

P(Fcons(t, f ))

P(x)

This rule establishes a single predicate for tree forest(A), the union of the recursive sets. Although such reasoning can be useful [25, §4.5], a proper mutual induction rule should establish separate predicates for tree(A) and forest(A). The package calls this rule tree forest.mutual induct. Observe the usage of P and Q in the induction hypotheses:

[ \begin{matrix}a ∈ A \\ f ∈ forest(A) \\ Q(f ) \end{matrix} ]_{a,f}
⋮ .

P(Tcons(a, f )) Q(Fnil)

[ \begin{matrix}t ∈ tree(A) \\ P(t) \\ f ∈ forest(A) \\ Q(f ) \end{matrix} ]_{t,f}

⋮ .

Q(Fcons(t, f ))

(∀z . z ∈ tree(A) → P(z)) ∧ (∀z . z ∈ forest(A) → Q(z))

Elsewhere I describe how to define mutually recursive functions over trees and forests [25, §4.5].

Both forest constructors have the form Inr(⋯), while the tree constructor has the form Inl(⋯). This pattern would hold regardless of how many tree or forest constructors there were.

Tcons(a, l) ≡ Inl(⟨a, l⟩)

                       Fnil ≡ Inr(Inl(∅))

Fcons(a, l) ≡ Inr(Inr(⟨a, l⟩))

There is only one case operator; it works on the union of the trees and forests:

   tree forest case(f , c, g) ≡ case(split(f ), case(λu . c, split(g)))

6.5 Example: a four-constructor datatype

A bigger datatype will illustrate some efficiency refinements. It has four constructors Con_{0}, …, Con_{3}, with the corresponding arities.

      consts    data :: [i,i] => i
      datatype  "data(A,B)" = Con0
                            | Con1 ("a: A")
                            | Con2 ("a: A", "b: B")
                            | Con3 ("a: A", "b: B", "d: data(A,B)")

Because this datatype has two set parameters, A and B, the package automatically supplies univ(A ∪ B) as its domain. The structural induction rule has four minor premises, one per constructor, and only the last has an induction hypothesis. (Details are left to the reader.)

The constructors are defined by the equations

                      Con_{0} ≡ Inl(Inl(∅))

Con_{1}(a) ≡ Inl(Inr(a))
Con_{2}(a, b) ≡ Inr(Inl(⟨a, b⟩))
Con_{3}(a, b, c) ≡ Inr(Inr(⟨a, b, c⟩)).

The case analysis operator is

data case(f_{0}, f_{1}, f_{2}, f_{3}) ≡ case(\begin{matrix}case(λu . f_{0}, f_{1}), \\ case(split(f_{2}), split(λv . split(f_{3}(v))))) \end{matrix}

This may look cryptic, but the case equations are trivial to verify.

In the constructor definitions, the injections are balanced. A more naive approach is to define Con_{3}(a, b, c) as Inr(Inr(Inr(⟨a, b, c⟩))); instead, each constructor has two injections. The difference here is small. But the zf examples include a 60-element enumeration type, where each constructor has 5 or 6 injections. The naive approach would require 1 to 59 injections; the definitions would be quadratic in size. It is like the advantage of binary notation over unary.

The result structure contains the case operator and constructor definitions as the theorem list con_defs. It contains the case equations, such as

data case(f_{0}, f_{1}, f_{2}, f_{3}, Con_{3}(a, b, c)) = f_{3}(a, b, c),

as the theorem list case_eqns. There is one equation per constructor.

6.6 Proving freeness theorems

There are two kinds of freeness theorems:

• injectiveness theorems, such as

Con_{2}(a, b) = Con_{2}(a′, b′) ↔ a = a′ ∧ b = b′

• distinctness theorems, such as

Con_{1}(a) ≠ Con_{2}(a′, b′)

Since the number of such theorems is quadratic in the number of constructors, the package does not attempt to prove them all. Instead it returns tools for proving desired theorems — either manually or during simplification or classical reasoning.

The theorem list free_iffs enables the simplifier to perform freeness reasoning. This works by incremental unfolding of constructors that appear in equations. The theorem list contains logical equivalences such as

Con_{0} = c ↔ c = Inl(Inl(∅))
Con_{1}(a) = c ↔ c = Inl(Inr(a))

⋮
Inl(a) = Inl(b) ↔ a = b

               Inl(a) = Inr(b) ↔ False

⟨a, b⟩ = ⟨a′, b′⟩ ↔ a = a′ ∧ b = b′

For example, these rewrite Con_{1}(a) = Con_{1}(b) to a = b in four steps.

The theorem list free_SEs enables the classical reasoner to perform similar replacements. It consists of elimination rules to replace Con_{0} = c by c = Inl(Inl(∅)) and so forth, in the assumptions.

Such incremental unfolding combines freeness reasoning with other proof steps. It has the unfortunate side-effect of unfolding definitions of constructors in contexts such as ∃x . Con_{1}(a) = x, where they should be left alone. Calling the Isabelle tactic fold tac con defs restores the defined constants.

7 Related work

The use of least fixedpoints to express inductive definitions seems obvious. Why, then, has this technique so seldom been implemented?

Most automated logics can only express inductive definitions by asserting axioms. Little would be left of Boyer and Moore’s logic [4] if their shell principle were removed. With alf the situation is more complex; earlier versions of Martin-Löf’s type theory could (using wellordering types) express datatype definitions, but the version underlying alf requires new rules for each definition [7]. With Coq the situation is subtler still; its underlying Calculus of Constructions can express inductive definitions [13], but cannot quite handle datatype definitions [21]. It seems that researchers tried hard to circumvent these problems before finally extending the Calculus with rule schemes for strictly positive operators. Recently Giménez has extended the Calculus of Constructions with inductive and coinductive types [10], with mechanized support in Coq.

Higher-order logic can express inductive definitions through quantification over unary predicates. The following formula expresses that i belongs to the least set containing 0 and closed under succ:

∀P . P(0) ∧ (∀x . P(x) → P(succ(x))) → P(i)

This technique can be used to prove the Knaster-Tarski theorem, which (in its general form) is little used in the Cambridge hol system. Melham [14] describes the development. The natural numbers are defined as shown above, but lists are defined as functions over the natural numbers. Unlabelled trees are defined using Gödel numbering; a labelled tree consists of an unlabelled tree paired with a list of labels. Melham’s datatype package expresses the user’s datatypes in terms of labelled trees. It has been highly successful, but a fixedpoint approach might have yielded greater power with less effort.

Elsa Gunter [11] reports an ongoing project to generalize the Cambridge hol system with mutual recursion and infinitely-branching trees. She retains many features of Melham’s approach.

Melham’s inductive definition package [5] also uses quantification over predicates. But instead of formalizing the notion of monotone function, it requires definitions to consist of finitary rules, a syntactic form that excludes many monotone inductive definitions.

pvs [20] is another proof assistant based on higher-order logic. It supports both inductive definitions and datatypes, apparently by asserting axioms. Datatypes may not be iterated in general, but may use recursion over the built-in list type.

The earliest use of least fixedpoints is probably Robin Milner’s. Brian Monahan extended this package considerably [18], as did I in unpublished work.^{3} lcf is a first-order logic of domain theory; the relevant fixedpoint theorem is not Knaster-Tarski but concerns fixedpoints of continuous functions over domains. lcf is too weak to express recursive predicates. The Isabelle package might be the first to be based on the Knaster-Tarski theorem.

8 Conclusions and future work

Higher-order logic and set theory are both powerful enough to express inductive definitions. A growing number of theorem provers implement one of these [8, 32]. The easiest sort of inductive definition package to write is one that asserts new axioms, not one that makes definitions and proves theorems about them. But asserting axioms could introduce unsoundness.

The fixedpoint approach makes it fairly easy to implement a package for (co)inductive definitions that does not assert axioms. It is efficient: it processes most definitions in seconds and even a 60-constructor datatype requires only a few minutes. It is also simple: The first working version took under a week to code, consisting of under 1100 lines (35K bytes) of Standard ml.

In set theory, care is needed to ensure that the inductive definition yields a set (rather than a proper class). This problem is inherent to set theory, whether or not the Knaster-Tarski theorem is employed. We must exhibit a bounding set (called a domain above). For inductive definitions, this is often trivial. For datatype definitions, I have had to formalize much set theory. To justify infinitely-branching datatype definitions, I have had to develop a theory of cardinal arithmetic [29], such as the theorem that if κ is an infinite cardinal and |X (α)| ≤ κ for all α < κ then | ⋃_{α<κ} X (α)| ≤ κ. The need for such efforts is not a drawback of the fixedpoint approach, for the alternative is to take such definitions on faith.

3The datatype package described in my lcf book [22] does not make definitions, but merely asserts axioms.

Care is also needed to ensure that the greatest fixedpoint really yields a coinductive definition. In set theory, standard pairs admit only well-founded constructions. Aczel’s anti-foundation axiom [3] could be used to get nonwell-founded objects, but it does not seem easy to mechanize. Isabelle/zf instead uses a variant notion of ordered pairing, which can be generalized to a variant notion of function. Elsewhere I have proved that this simple approach works (yielding final coalgebras) for a broad class of definitions [27].

Several large studies make heavy use of inductive definitions. Lötzbeyer and Sandner have formalized two chapters of a semantics book [35], proving the equivalence between the operational and denotational semantics of a simple imperative language. A single theory file contains three datatype definitions (of arithmetic expressions, boolean expressions and commands) and three inductive definitions (the corresponding operational rules). Using different techniques, Nipkow [19] and Rasmussen [31] have both proved the Church-Rosser theorem; inductive definitions specify several reduction relations on λ-terms. Recently, I have applied inductive definitions to the analysis of cryptographic protocols [28].

To demonstrate coinductive definitions, Frost [9] has proved the consistency of the dynamic and static semantics for a small functional language. The example is due to Milner and Tofte [17]. It concerns an extended correspondence relation, which is defined coinductively. A codatatype definition specifies values and value environments in mutual recursion. Non-well-founded values represent recursive functions. Value environments are variant functions from variables into values. This one key definition uses most of the package’s novel features.

The approach is not restricted to set theory. It should be suitable for any logic that has some notion of set and the Knaster-Tarski theorem. I have ported the (co)inductive definition package from Isabelle/zf to Isabelle/hol (higher-order logic).

References

[1] Samson Abramsky. The lazy lambda calculus. In David A. Turner, editor, Research Topics in Functional Programming, pages 65–116. Addison-Wesley, 1990.

[2] Peter Aczel. An introduction to inductive definitions. In J. Barwise, editor, Handbook of Mathematical Logic, pages 739–782. North-Holland, 1977.

[3] Peter Aczel. Non-Well-Founded Sets. CSLI, 1988.

[4] Robert S. Boyer and J Strother Moore. A Computational Logic. Academic Press, 1979.

[5] J. Camilleri and T. F. Melham. Reasoning with inductively defined relations in the HOL theorem prover. Technical Report 265, Computer Laboratory, University of Cambridge, August 1992.

[6] B. A. Davey and H. A. Priestley. Introduction to Lattices and Order. Cambridge University Press, 1990.

[7] Peter Dybjer. Inductive sets and families in Martin-Löf’s type theory and their settheoretic semantics. In Gérard Huet and Gordon Plotkin, editors, Logical Frameworks, pages 280–306. Cambridge University Press, 1991.

[8] William M. Farmer, Joshua D. Guttman, and F. Javier Thayer. IMPS: An interactive mathematical proof system. Journal of Automated Reasoning, 11(2):213–248, 1993.

[9] Jacob Frost. A case study of co-induction in Isabelle. Technical Report 359, Computer Laboratory, University of Cambridge, February 1995.

[10] Eduardo Giménez. Codifying guarded definitions with recursive schemes. In Peter Dybjer, Bengt Nordström, and Jan Smith, editors, Types for Proofs and Programs: International Workshop TYPES ’94, LNCS 996, pages 39–59. Springer, 1995.

[11] Elsa L. Gunter. A broader class of trees for recursive type definitions for HOL. In J. Joyce and C. Seger, editors, Higher Order Logic Theorem Proving and Its Applications: HUG ’93, LNCS 780, pages 141–154. Springer, Published 1994.

[12] Matthew Hennessy. The Semantics of Programming Languages: An Elementary Introduction Using Structural Operational Semantics. Wiley, 1990.

[13] Gérard Huet. Induction principles formalized in the Calculus of Constructions. In K. Fuchi and M. Nivat, editors, Programming of Future Generation Computers, pages 205–216. Elsevier, 1988.

[14] Thomas F. Melham. Automating recursive type definitions in higher order logic. In Graham Birtwistle and P. A. Subrahmanyam, editors, Current Trends in Hardware Verification and Automated Theorem Proving, pages 341–386. Springer, 1989.

[15] Robin Milner. How to derive inductions in LCF. note, Department of Computer Science, University of Edinburgh, 1980.

[16] Robin Milner. Communication and Concurrency. Prentice-Hall, 1989.

[17] Robin Milner and Mads Tofte. Co-induction in relational semantics. Theoretical Computer Science, 87:209–220, 1991.

[18] Brian Q. Monahan. Data Type Proofs using Edinburgh LCF. PhD thesis, University of Edinburgh, 1984.

[19] Tobias Nipkow. More Church-Rosser proofs (in Isabelle/HOL). In M. McRobbie and J.K. Slaney, editors, Automated Deduction — CADE-13, volume 1104 of Lecture Notes in Computer Science, pages 733–747. Springer-Verlag, 1996.

[20] S. Owre, N. Shankar, and J. M. Rushby. The PVS specification language. Computer Science Laboratory, SRI International, Menlo Park, CA, April 1993. Beta release.

[21] Christine Paulin-Mohring. Inductive definitions in the system Coq: Rules and properties. In M. Bezem and J.F. Groote, editors, Typed Lambda Calculi and Applications, LNCS 664, pages 328–345. Springer, 1993.

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

[23] Lawrence C. Paulson. Set theory for verification: I. From foundations to functions. Journal of Automated Reasoning, 11(3):353–389, 1993.

[24] Lawrence C. Paulson. Isabelle: A Generic Theorem Prover. Springer, 1994. LNCS 828.

[25] Lawrence C. Paulson. Set theory for verification: II. Induction and recursion. Journal of Automated Reasoning, 15(2):167–215, 1995.

[26] Lawrence C. Paulson. Mechanizing coinduction and corecursion in higher-order logic. Journal of Logic and Computation, 7(2):175–204, March 1997.

[27] Lawrence C. Paulson. Final coalgebras as greatest fixed points in ZF set theory. Mathematical Structures in Computer Science, 9, 1999. in press.

[28] Lawrence C. Paulson. Tool support for logics of programs. In Manfred Broy, editor, Mathematical Methods in Program Development: Summer School Marktoberdorf 1996, NATO ASI Series F, pages 461–498. Springer, Published 1997.

[29] Lawrence C. Paulson and Krzysztof Gra̧bczewski. Mechanizing set theory: Cardinal arithmetic and the axiom of choice. Journal of Automated Reasoning, 17(3):291–323, December 1996.

[30] Andrew M. Pitts. A co-induction principle for recursively defined domains. Theoretical Computer Science, 124:195–219, 1994.

[31] Ole Rasmussen. The Church-Rosser theorem in Isabelle: A proof porting experiment. Technical Report 364, Computer Laboratory, University of Cambridge, May 1995.

[32] Mark Saaltink, Sentot Kromodimoeljo, Bill Pase, Dan Craigen, and Irwin Meisels. An EVES data abstraction example. In J. C. P. Woodcock and P. G. Larsen, editors, FME ’93: Industrial-Strength Formal Methods, volume 670 of Lecture Notes in Computer Science, pages 578–596. Springer-Verlag, 1993.

[33] Konrad Slind. Function definition in higher order logic. In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem Proving in Higher Order Logics, volume 1125 of Lecture Notes in Computer Science, pages 381–397. Springer-Verlag, 1996.

[34] Nora Szasz. A machine checked proof that Ackermann’s function is not primitive recursive. In Gérard Huet and Gordon Plotkin, editors, Logical Environments, pages 317–338. Cambridge University Press, 1993.

[35] Glynn Winskel. The Formal Semantics of Programming Languages. MIT Press, 1993.