summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

doc-src/TutorialI/Inductive/inductive.tex

author | nipkow |

Wed Dec 06 13:22:58 2000 +0100 (2000-12-06) | |

changeset 10608 | 620647438780 |

parent 10520 | bb9dfcc87951 |

child 10762 | cd1a2bee5549 |

permissions | -rw-r--r-- |

*** empty log message ***

1 \chapter{Inductively Defined Sets}

2 \index{inductive definition|(}

3 \index{*inductive|(}

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

6 recursive functions and datatypes: inductively defined sets.

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.

16 \input{Inductive/Even}

17 \input{Inductive/document/Star}

19 \section{Advanced inductive definitions}

20 \input{Inductive/Advanced}

22 \input{Inductive/document/AB}

24 \index{inductive definition|)}

25 \index{*inductive|)}