author | Walther Neuper <neuper@ist.tugraz.at> |
Thu, 12 Aug 2010 15:03:34 +0200 | |
branch | isac-from-Isabelle2009-2 |
changeset 37913 | 20e3616b2d9c |
parent 25330 | 15bf0f47a87d |
child 49537 | 708278fc2dff |
permissions | -rw-r--r-- |
paulson@10865 | 1 |
\chapter{Inductively Defined Sets} \label{chap:inductive} |
paulson@11428 | 2 |
\index{inductive definitions|(} |
nipkow@10242 | 3 |
|
nipkow@10242 | 4 |
This chapter is dedicated to the most important definition principle after |
nipkow@10242 | 5 |
recursive functions and datatypes: inductively defined sets. |
nipkow@10242 | 6 |
|
nipkow@11147 | 7 |
We start with a simple example: the set of even numbers. A slightly more |
nipkow@11147 | 8 |
complicated example, the reflexive transitive closure, is the subject of |
nipkow@11147 | 9 |
{\S}\ref{sec:rtc}. In particular, some standard induction heuristics are |
nipkow@11147 | 10 |
discussed. Advanced forms of inductive definitions are discussed in |
nipkow@11147 | 11 |
{\S}\ref{sec:adv-ind-def}. To demonstrate the versatility of inductive |
nipkow@11147 | 12 |
definitions, the chapter closes with a case study from the realm of |
nipkow@11147 | 13 |
context-free grammars. The first two sections are required reading for anybody |
nipkow@11147 | 14 |
interested in mathematical modelling. |
nipkow@10219 | 15 |
|
nipkow@25330 | 16 |
\begin{warn} |
nipkow@25330 | 17 |
Predicates can also be defined inductively. |
nipkow@25330 | 18 |
See {\S}\ref{sec:ind-predicates}. |
nipkow@25330 | 19 |
\end{warn} |
nipkow@25330 | 20 |
|
berghofe@23843 | 21 |
\input{Inductive/document/Even} |
nipkow@10762 | 22 |
\input{Inductive/document/Mutual} |
nipkow@10225 | 23 |
\input{Inductive/document/Star} |
nipkow@10242 | 24 |
|
nipkow@11216 | 25 |
\section{Advanced Inductive Definitions} |
nipkow@11147 | 26 |
\label{sec:adv-ind-def} |
berghofe@23843 | 27 |
\input{Inductive/document/Advanced} |
paulson@10371 | 28 |
|
nipkow@10520 | 29 |
\input{Inductive/document/AB} |
nipkow@10520 | 30 |
|
paulson@11428 | 31 |
\index{inductive definitions|)} |