1\chapter{Inductively Defined Sets} \label{chap:inductive}
2\index{inductive definitions|(}
3
4This chapter is dedicated to the most important definition principle after
5recursive functions and datatypes: inductively defined sets.
6
7We start with a simple example: the set of even numbers.  A slightly more
8complicated example, the reflexive transitive closure, is the subject of
9{\S}\ref{sec:rtc}. In particular, some standard induction heuristics are
10discussed. Advanced forms of inductive definitions are discussed in
11{\S}\ref{sec:adv-ind-def}. To demonstrate the versatility of inductive
12definitions, the chapter closes with a case study from the realm of
13context-free grammars. The first two sections are required reading for anybody
14interested in mathematical modelling.
15
16\begin{warn}
17Predicates can also be defined inductively.
18See {\S}\ref{sec:ind-predicates}.
19\end{warn}
20
21\input{Even}
22\input{Mutual}
23\input{Star}
24
25\section{Advanced Inductive Definitions}
26\label{sec:adv-ind-def}
27\input{Advanced}
28
29\input{AB}
30
31\index{inductive definitions|)}
32