author paulson Mon, 06 Nov 2000 16:43:01 +0100 changeset 10398 cdb451206ef9 parent 10397 e2d0dda41f2c child 10399 e37e123738f7
minor changes
--- a/doc-src/TutorialI/Sets/sets.tex	Mon Nov 06 16:41:39 2000 +0100
+++ b/doc-src/TutorialI/Sets/sets.tex	Mon Nov 06 16:43:01 2000 +0100
@@ -1,4 +1,3 @@
-% ID:         $Id$
\chapter{Sets, Functions and Relations}

Mathematics relies heavily on set theory: not just unions and intersections
@@ -633,7 +632,6 @@

\section{Relations}
-\label{sec:Relations}

A \textbf{relation} is a set of pairs.  As such, the set operations apply
to them.  For instance, we may form the union of two relations.  Other
@@ -728,10 +726,10 @@
\rulename{RelPow.relpow.simps}
\end{isabelle}

-The \textbf{reflexive transitive closure} of a relation is particularly
-important.  It has the postfix syntax \isa{r\isacharcircum{*}}.  The
-construction is defined   to be the least fixedpoint satisfying the
-following equation:
+The \textbf{reflexive transitive closure} of the
+relation~\isa{r} is written with the
+postfix syntax \isa{r\isacharcircum{*}}.  It is the least solution of the
+equation
\begin{isabelle}
r\isacharcircum{*}\ =\ Id\ \isasymunion\ (r\ O\ r\isacharcircum{*})
\rulename{rtrancl_unfold}
@@ -874,7 +872,6 @@

\section{Well-founded relations and induction}
-\label{sec:Well-founded}

Induction comes in many forms, including traditional mathematical
induction, structural induction on lists and induction on size.
@@ -883,15 +880,13 @@
Intuitively, the relation~$\prec$ is \textbf{well-founded} if it admits no
infinite  descending chains
$\cdots \prec a@2 \prec a@1 \prec a@0.$
-If $\prec$ is well-founded then it can be used with the \textbf{well-founded
-induction}\indexbold{induction!well-founded}\index{well-founded
-induction|see{induction, well-founded}} rule:
+If $\prec$ is well-founded then it can be used with the well-founded
+induction rule:
$\infer{P(a)}{\infer*{P(x)}{[\forall y.\, y\prec x \imp P(y)]}}$
To show $P(a)$ for a particular term~$a$, it suffices to show $P(x)$ for
arbitrary~$x$ under the assumption that $P(y)$ holds for $y\prec x$.
Intuitively, the well-foundedness of $\prec$ ensures that the chains of
-reasoning are finite.  For a fuller account of well-founded relations and
+temporal logic CTL\@.