doc-src/TutorialI/Inductive/inductive.tex
author paulson
Tue, 17 Jul 2001 13:46:21 +0200
changeset 11428 332347b9b942
parent 11411 c315dda16748
child 23843 4cd60e5d2999
permissions -rw-r--r--
tidying the index
     1 \chapter{Inductively Defined Sets} \label{chap:inductive}
     2 \index{inductive definitions|(}
     3 
     4 This chapter is dedicated to the most important definition principle after
     5 recursive functions and datatypes: inductively defined sets.
     6 
     7 We start with a simple example: the set of even numbers.  A slightly more
     8 complicated example, the reflexive transitive closure, is the subject of
     9 {\S}\ref{sec:rtc}. In particular, some standard induction heuristics are
    10 discussed. Advanced forms of inductive definitions are discussed in
    11 {\S}\ref{sec:adv-ind-def}. To demonstrate the versatility of inductive
    12 definitions, the chapter closes with a case study from the realm of
    13 context-free grammars. The first two sections are required reading for anybody
    14 interested in mathematical modelling.
    15 
    16 \input{Inductive/even-example}
    17 \input{Inductive/document/Mutual}
    18 \input{Inductive/document/Star}
    19 
    20 \section{Advanced Inductive Definitions}
    21 \label{sec:adv-ind-def}
    22 \input{Inductive/advanced-examples}
    23 
    24 \input{Inductive/document/AB}
    25 
    26 \index{inductive definitions|)}