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