Abstract
The purpose of this chapter is to deepen your understanding of the concepts encountered so far and to introduce advanced forms of datatypes and recursive functions. The first two sections give a structured presentation of theorem proving by simplification (Sect. 3.1) and discuss important heuristics for induction (Sect. 3.2). You can skip them if you are not planning to perform proofs yourself. We then present a case study: a compiler for expressions (Sect. 3.3). Advanced datatypes, including those involving function spaces, are covered in Sect. 3.4; it closes with another case study, search trees (“tries”). Finally we introduce recdef, a general form of recursive function definition that goes well beyond primrec (Sect. 3.5).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
(2002). 3. More Functional Programming. 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_3
Download citation
DOI: https://doi.org/10.1007/3-540-45949-9_3
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