Proof Obligation Generation and Discharging for Recursive Definitions in VDM

2010 ◽  
pp. 40-55 ◽  
Author(s):  
Augusto Ribeiro ◽  
Peter Gorm Larsen
Keyword(s):  
Proof Obligation ◽  
Recursive Definitions

scholarly journals Final coalgebras as greatest fixed points in ZF set theory

1999 ◽  
Vol 9 (5) ◽  
pp. 545-567 ◽  
Author(s):  
LAWRENCE C. PAULSON
Keyword(s):  
Fixed Points ◽  
Set Theory ◽  
Theorem Prover ◽  
Infinite Length ◽  
Special Cases ◽  
Definition Of ◽  
Recursive Definitions ◽  
Ordered Pairs

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

Sign in / Sign up

Export Citation Format

Share Document