doc-src/TutorialI/Sets/sets.tex
changeset 10374 d72638f2b78e
parent 10373 f9211fc8cd7d
child 10398 cdb451206ef9
equal deleted inserted replaced
10373:f9211fc8cd7d 10374:d72638f2b78e
   881 More general than these is induction over a well-founded relation. 
   881 More general than these is induction over a well-founded relation. 
   882 Such A relation expresses the notion of a terminating process. 
   882 Such A relation expresses the notion of a terminating process. 
   883 Intuitively, the relation~$\prec$ is \textbf{well-founded} if it admits no
   883 Intuitively, the relation~$\prec$ is \textbf{well-founded} if it admits no
   884 infinite  descending chains
   884 infinite  descending chains
   885 \[ \cdots \prec a@2 \prec a@1 \prec a@0. \]
   885 \[ \cdots \prec a@2 \prec a@1 \prec a@0. \]
   886 If $\prec$ is well-founded then it can be used with the well-founded 
   886 If $\prec$ is well-founded then it can be used with the \textbf{well-founded
   887 induction rule: 
   887 induction}\indexbold{induction!well-founded}\index{well-founded
       
   888 induction|see{induction, well-founded}} rule:
   888 \[ \infer{P(a)}{\infer*{P(x)}{[\forall y.\, y\prec x \imp P(y)]}} \]
   889 \[ \infer{P(a)}{\infer*{P(x)}{[\forall y.\, y\prec x \imp P(y)]}} \]
   889 To show $P(a)$ for a particular term~$a$, it suffices to show $P(x)$ for
   890 To show $P(a)$ for a particular term~$a$, it suffices to show $P(x)$ for
   890 arbitrary~$x$ under the assumption that $P(y)$ holds for $y\prec x$. 
   891 arbitrary~$x$ under the assumption that $P(y)$ holds for $y\prec x$. 
   891 Intuitively, the well-foundedness of $\prec$ ensures that the chains of
   892 Intuitively, the well-foundedness of $\prec$ ensures that the chains of
   892 reasoning are finite.
   893 reasoning are finite.  For a fuller account of well-founded relations and
       
   894 induction see, for example, \cite{Baader-Nipkow}.
   893 
   895 
   894 In Isabelle, the induction rule is expressed like this:
   896 In Isabelle, the induction rule is expressed like this:
   895 \begin{isabelle}
   897 \begin{isabelle}
   896 {\isasymlbrakk}wf\ r;\ 
   898 {\isasymlbrakk}wf\ r;\ 
   897   {\isasymAnd}x.\ {\isasymforall}y.\ (y,x)\ \isasymin\ r\
   899   {\isasymAnd}x.\ {\isasymforall}y.\ (y,x)\ \isasymin\ r\