doc-src/TutorialI/Inductive/inductive.tex
 author nipkow Sun Nov 26 10:48:38 2000 +0100 (2000-11-26) changeset 10520 bb9dfcc87951 parent 10468 87dda999deca child 10762 cd1a2bee5549 permissions -rw-r--r--
*** empty log message ***
     1 \chapter{Inductively Defined Sets}

     2 \index{inductive definition|(}

     3 \index{*inductive|(}

     4

     5 This chapter is dedicated to the most important definition principle after

     6 recursive functions and datatypes: inductively defined sets.

     7

     8 We start with a simple example: the set of even numbers.

     9 A slightly more complicated example, the

    10 reflexive transitive closure, is the subject of {\S}\ref{sec:rtc}. In particular,

    11 some standard induction heuristics are discussed. To demonstrate the

    12 versatility of inductive definitions, {\S}\ref{sec:CFG} presents a case study

    13 from the realm of context-free grammars. The chapter closes with a discussion

    14 of advanced forms of inductive definitions.

    15

    16 \input{Inductive/Even}

    17 \input{Inductive/document/Star}

    18

    19 \section{Advanced inductive definitions}

    20 \input{Inductive/Advanced}

    21

    22 \input{Inductive/document/AB}

    23

    24 \index{inductive definition|)}

    25 \index{*inductive|)}