Datatypes and (Co)Inductive Definitions in Isabelle/HOL

Tobias Nipkow and Larry Paulson

1 Introduction

This document is an excerpt from the manual for Isabelle’s Higher-Order Logic (HOL). It presents those features of HOL which are not included in Paulson’s LNCS volume on Isabelle [2]: ML-like datatypes, primitive recursive function definitions over such datatypes, and (co)inductively defined sets.

2 Datatype declarations

It is often necessary to extend a theory with ml-like datatypes. This extension consists of the new type, declarations of its constructors and rules that describe the new type. The theory definition section datatype represents a compact way of doing this.

2.1 Foundations

A datatype declaration has the following general structure:

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 one of the following:

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

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

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

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)

together with unproblematic ones like

datatype t = C (t list).

1This makes it a recursive type. To ensure that the new type is not empty at least one constructor must consist of only non-recursive type components.

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:

distinct They are distinct:

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

inject 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 method is used if their number exceeds a certain value, currently 4. In that case every constructor is mapped to a natural number

t ord(C_{1}(x_{1}, …, x_{k_{1}})) = 0
⋮
t ord(C_{m}(x_{1}, …, x_{k_{m}} )) = m − 1

and distinctness of constructors is expressed by:

t ord(x) ≠ t ord(y) ⟹ x ≠ y.

In addition a structural induction axiom induct 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}, i.e. the property P can be assumed for all arguments of the recursive type.

The type also 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}

In contrast to ml, all constructors must be present, their order is fixed, and nested patterns are not supported.

2.2 Defining datatypes

A datatype is defined in a theory definition file using the keyword datatype. The definition following datatype must conform to the syntax of typedecl specified in Fig. 1 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. typedecl

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

cons

[figure: id; string; (; typ; ,; ); mixfix]

typ

[figure: typevarlist; id; tid]

typevarlist Figure 1: Syntax of datatype declarations

[figure: tid; (; tid; ,; )]

Reading the theory file produces a structure which, in addition to the usual components, contains a structure named t for each datatype t defined in the file.^{2} 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 convenience distinct contains inequalities in both directions.

! If there are five or more constructors, the t ord scheme is used for distinct. In this case the theory Arith must be contained in the current theory, if necessary by including it explicitly.

The reduction rules of the case-construct are in cases. All theorems from distinct, inject and cases are combined in simps for use with the simplifier. A call to the tactic “induct_tac var i” applies structural induction over variable var to subgoal i.

2.3 Examples

2.3.1 The datatype α list

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

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

After loading the theory (use_thy "MyList"), we can prove Cons(x, xs) ≠ xs. First we build a suitable simpset for the simplifier:

      val mylist_ss = HOL_ss addsimps MyList.list.simps;
      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 (MyList.list.induct_tac "xs" 1);
       Level 1
       ! x. Cons(x, xs) ~= xs
        1. ! x. Cons(x, Nil) ~= Nil
        2. !!a list.
              ! x. Cons(x, list) ~= list ==>
              ! x. Cons(x, Cons(a, list)) ~= Cons(a, list)

2Otherwise multiple datatypes in the same theory file would lead to name clashes.

3Of course there is a list type in HOL already. This is only an example.

The first subgoal can be proved with the simplifier and the distinctness axioms which are

part of mylist_ss.
      by (simp_tac mylist_ss 1);
       Level 2
       ! x. Cons(x, xs) ~= xs
        1. !!a list.
              ! x. Cons(x, list) ~= list ==>
              ! x. Cons(x, Cons(a, list)) ~= Cons(a, list)

Using the freeness axioms we can quickly prove the remaining goal.

      by (asm_simp_tac mylist_ss 1);
       Level 3
       ! x. Cons(x, xs) ~= xs
       No subgoals!

Because both subgoals were proved by almost the same tactic we could have done that in one step using

      by (ALLGOALS (asm_simp_tac mylist_ss));

2.3.2 The datatype α list with mixfix syntax

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

      MyList = HOL +
        datatype 'a list = "[]" ("[]")
                         | "#" ('a, 'a list) (infixr 70)
      end

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

2.3.3 A datatype for weekdays

This example shows a datatype that consists of more than four constructors:

      Days = Arith +
        datatype days = Mo | Tu | We | Th | Fr | Sa | So
      end

Because there are more than four constructors, the theory must be based on Arith. Inequality is defined via a function days_ord. Although the expression Mo ~= Tu is not directly contained in distinct, it can be proved by the simplifier if arith_ss is used:

      val days_ss = arith_ss addsimps Days.days.simps;
      goal Days.thy "Mo ~= Tu";
      by (simp_tac days_ss 1);

Note that usually it is not necessary to derive these inequalities explicitly because the simplifier will dispose of them automatically.

2.4 Primitive recursive functions

Datatypes come with a uniform way of defining functions, primitive recursion. Although it is possible to define primitive recursive functions by asserting their reduction rules as new axioms, e.g.

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

this carries with it the danger of accidentally asserting an inconsistency, for example app([],ys) = us. Therefore primitive recursive functions on datatypes can be defined with a special syntax:

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

The system will now check that the two rules app_Nil and app_Cons do indeed form a primitive recursive definition, thus ensuring that consistency is maintained. For example

      primrec app MyList.list
          app_Nil   "app([],ys) = us"

is rejected:

      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. The function must already have been declared.

• type is the name of the datatype, either as an id or in the long form Thy.t, where Thy is the name of the parent theory the datatype was declared in, and 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 named equations of the form id string, where the identifier gives the name of the rule in the result structure, and string is a reduction rule 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.

A theory file may contain any number of primrec sections which may be intermixed with other declarations.

For the consistency-sensitive user it may be reassuring to know that primrec does not assert the reduction rules as new axioms but derives them as theorems from an explicit definition of the recursive function in terms of a recursion operator on the datatype.

The primitive recursive function can also use infix or mixfix syntax:

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

The reduction rules become part of the ML structure Append and can be used to prove theorems about the function:

      val append_ss = HOL_ss addsimps [Append.app_Nil,Append.app_Cons];
      goal Append.thy "(xs @ ys) @ zs = xs @ (ys @ zs)";
      by (MyList.list.induct_tac "xs" 1);
      by (ALLGOALS(asm_simp_tac append_ss));

3 Inductive and coinductive definitions

An inductive definition specifies the least set closed under given rules. For example, a structural operational semantics is an inductive definition of an evaluation relation. Dually, a coinductive definition specifies the greatest set closed under given rules. 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,^{4} 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.

3.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.

4It appeared in CADE [1] and a longer version is distributed with Isabelle.

      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 2: The result of a (co)inductive definition

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. For a coinductive definition, it contains the rule coinduct.

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

3.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 .thy.ML file; 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 identifiers, not infix operators.

• 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.

3.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 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, such as the theory

HOL/ex/PropLog.thy and the directory HOL/IMP. The theory HOL/LList.thy contains

coinductive definitions.

References

[1] Lawrence C. Paulson. A fixedpoint approach to implementing (co)inductive definitions. In Alan Bundy, editor, Proc. 12th Int. Conf. Automated Deduction, volume 814 of Lect. Notes in Comp. Sci., pages 148–161. Springer-Verlag, 1994.

[2] Lawrence C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lect. Notes in Comp. Sci. Springer-Verlag, 1994.