author | paulson |
Fri, 12 Jan 2001 16:28:14 +0100 | |
changeset 10884 | 2995639c6a09 |
parent 10865 | 18927bcf7aed |
child 11147 | d848c6693185 |
permissions | -rw-r--r-- |
paulson@10865 | 1 |
\chapter{Inductively Defined Sets} \label{chap:inductive} |
nipkow@10242 | 2 |
\index{inductive definition|(} |
nipkow@10242 | 3 |
\index{*inductive|(} |
nipkow@10242 | 4 |
|
nipkow@10242 | 5 |
This chapter is dedicated to the most important definition principle after |
nipkow@10242 | 6 |
recursive functions and datatypes: inductively defined sets. |
nipkow@10242 | 7 |
|
paulson@10327 | 8 |
We start with a simple example: the set of even numbers. |
paulson@10327 | 9 |
A slightly more complicated example, the |
nipkow@10242 | 10 |
reflexive transitive closure, is the subject of {\S}\ref{sec:rtc}. In particular, |
nipkow@10242 | 11 |
some standard induction heuristics are discussed. To demonstrate the |
nipkow@10242 | 12 |
versatility of inductive definitions, {\S}\ref{sec:CFG} presents a case study |
nipkow@10242 | 13 |
from the realm of context-free grammars. The chapter closes with a discussion |
nipkow@10242 | 14 |
of advanced forms of inductive definitions. |
nipkow@10219 | 15 |
|
paulson@10884 | 16 |
\input{Inductive/even-example} |
nipkow@10762 | 17 |
\input{Inductive/document/Mutual} |
nipkow@10225 | 18 |
\input{Inductive/document/Star} |
nipkow@10242 | 19 |
|
paulson@10371 | 20 |
\section{Advanced inductive definitions} |
paulson@10884 | 21 |
\input{Inductive/advanced-examples} |
paulson@10371 | 22 |
|
nipkow@10520 | 23 |
\input{Inductive/document/AB} |
nipkow@10520 | 24 |
|
nipkow@10242 | 25 |
\index{inductive definition|)} |
nipkow@10242 | 26 |
\index{*inductive|)} |