A special final coalgebra theorem, in the style of Aczel (1988), is proved within standard
Zermelo–Fraenkel set theory. Aczel's Anti-Foundation Axiom is replaced by a variant
definition of function that admits non-well-founded constructions. Variant ordered pairs and
tuples, of possibly infinite length, are special cases of variant functions. Analogues of Aczel's
solution and substitution lemmas are proved in the style of Rutten and Turi (1993). The
approach is less general than Aczel's, but the treatment of non-well-founded objects is
simple and concrete. The final coalgebra of a functor is its greatest fixedpoint.Compared with previous work (Paulson, 1995a), iterated substitutions and solutions are
considered, as well as final coalgebras defined with respect to parameters. The disjoint sum
construction is replaced by a smoother treatment of urelements that simplifies many of the
derivations.The theory facilitates machine implementation of recursive definitions by letting both
inductive and coinductive definitions be represented as fixed points. It has already been
applied to the theorem prover Isabelle (Paulson, 1994).
A practical mode system for recursive definitions
