
Set Theory for Verification: II
Induction and Recursion
Lawrence C. Paulson
Computer Laboratory, University of Cambridge
April 26, 1995
Abstract. A theory of recursive definitions has been mechanized in Isabelle's ZermeloFraenkel (ZF) set theory. The objective is to support the formalization of particular recursive definitions for use in verification, semantics proofs and other computational reasoning.
Inductively defined sets are expressed as least fixedpoints, applying the KnasterTarski Theorem over a suitable set. Recursive functions are defined by wellfounded recursion and its derivatives, such as transfinite recursion. Recursive data structures are expressed by applying the KnasterTarski Theorem to a set, such as V! , that is closed under Cartesian product and disjoint sum.
Worked examples include the transitive closure of a relation, lists, variablebranching trees and mutually recursive trees and forests. The SchroderBernstein Theorem and the soundness of propositional logic are proved in Isabelle sessions.
Key words: Isabelle, set theory, recursive definitions, the SchroderBernstein Theorem