# HG changeset patch # User paulson # Date 973525381 -3600 # Node ID cdb451206ef9d99a7fe881b9f1bd693fe3e0a805 # Parent e2d0dda41f2c4d59f6a01e200cda7b216edc9f6a minor changes diff -r e2d0dda41f2c -r cdb451206ef9 doc-src/TutorialI/Sets/sets.tex --- 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 -induction see, for example, \cite{Baader-Nipkow}. +reasoning are finite. In Isabelle, the induction rule is expressed like this: \begin{isabelle} @@ -1040,6 +1035,5 @@ two agents in a process algebra is an example of coinduction. The coinduction rule can be strengthened in various ways; see theory {\isa{Gfp}} for details. -An example using the fixed point operators appears later in this -chapter, in the section on computation tree logic -(\S\ref{sec:ctl-case-study}). +This chapter ends with a case study concerning model checking for the +temporal logic CTL\@.