author | nipkow |
Tue, 02 Jan 2001 12:04:33 +0100 | |
changeset 10762 | cd1a2bee5549 |
parent 10520 | bb9dfcc87951 |
child 10865 | 18927bcf7aed |
permissions | -rw-r--r-- |
nipkow@10219 | 1 |
\chapter{Inductively Defined Sets} |
nipkow@10242 | 2 |
\index{inductive definition|(} |
nipkow@10242 | 3 |
\index{*inductive|(} |
nipkow@10242 | 4 |
|
nipkow@10242 | 5 |
This chapter is dedicated to the most important definition principle after |
nipkow@10242 | 6 |
recursive functions and datatypes: inductively defined sets. |
nipkow@10242 | 7 |
|
paulson@10327 | 8 |
We start with a simple example: the set of even numbers. |
paulson@10327 | 9 |
A slightly more complicated example, the |
nipkow@10242 | 10 |
reflexive transitive closure, is the subject of {\S}\ref{sec:rtc}. In particular, |
nipkow@10242 | 11 |
some standard induction heuristics are discussed. To demonstrate the |
nipkow@10242 | 12 |
versatility of inductive definitions, {\S}\ref{sec:CFG} presents a case study |
nipkow@10242 | 13 |
from the realm of context-free grammars. The chapter closes with a discussion |
nipkow@10242 | 14 |
of advanced forms of inductive definitions. |
nipkow@10219 | 15 |
|
paulson@10327 | 16 |
\input{Inductive/Even} |
nipkow@10762 | 17 |
\input{Inductive/document/Mutual} |
nipkow@10225 | 18 |
\input{Inductive/document/Star} |
nipkow@10242 | 19 |
|
paulson@10371 | 20 |
\section{Advanced inductive definitions} |
paulson@10468 | 21 |
\input{Inductive/Advanced} |
paulson@10371 | 22 |
|
nipkow@10520 | 23 |
\input{Inductive/document/AB} |
nipkow@10520 | 24 |
|
nipkow@10242 | 25 |
\index{inductive definition|)} |
nipkow@10242 | 26 |
\index{*inductive|)} |