Abstract
This chapter is dedicated to the most important definition principle after recursive functions and datatypes: inductively defined sets.
We start with a simple example: the set of even numbers. A slightly more complicated example, the reflexive transitive closure, is the subject of Sect. 7.2. In particular, some standard induction heuristics are discussed. Advanced forms of inductive definitions are discussed in Sect. 7.3. To demonstrate the versatility of inductive definitions, the chapter closes with a case study from the realm of context-free grammars. The first two sections are required reading for anybody interested in mathematical modelling.
Chapter PDF
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
(2002). 7. Inductively Defined Sets. In: Nipkow, T., Wenzel, M., Paulson, L.C. (eds) Isabelle/HOL. Lecture Notes in Computer Science, vol 2283. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45949-9_7
Download citation
DOI: https://doi.org/10.1007/3-540-45949-9_7
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43376-7
Online ISBN: 978-3-540-45949-1
eBook Packages: Springer Book Archive