Computer Laboratory

Technical reports

Set theory for verification: II
Induction and recursion

Lawrence C. Paulson

September 1993, 46 pages

Abstract

A theory of recursive definitions has been mechanized in Isabelle’s Zermelo-Fraenkel (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 Knaster-Tarski Theorem over a suitable set. Recursive functions are defined by well-founded recursion and its derivatives, such as transfinite recursion. Recursive data structures are expressed by applying the Knaster-Tarski Theorem to a set that is closed under Cartesian product and disjoint sum.

Worked examples include the transitive closure of a relation, lists, variable-branching trees and mutually recursive trees and forests. The Schröder-Bernstein Theorem and the soundness of propositional logic are proved in Isabelle sessions.

Full text

PDF (0.3 MB)

BibTeX record

@TechReport{UCAM-CL-TR-312,
  author =	 {Paulson, Lawrence C.},
  title = 	 {{Set theory for verification: II : Induction and recursion}},
  year = 	 1993,
  month = 	 sep,
  url = 	 {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-312.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-312}
}