--- a/doc-src/TutorialI/Inductive/document/Star.tex Fri Jan 12 16:05:12 2001 +0100
+++ b/doc-src/TutorialI/Inductive/document/Star.tex Fri Jan 12 16:07:20 2001 +0100
@@ -2,14 +2,16 @@
\begin{isabellebody}%
\def\isabellecontext{Star}%
%
-\isamarkupsection{The reflexive transitive closure%
+\isamarkupsection{The Reflexive Transitive Closure%
}
%
\begin{isamarkuptext}%
\label{sec:rtc}
-Many inductive definitions define proper relations rather than merely set
-like \isa{even}. A perfect example is the
-reflexive transitive closure of a relation. This concept was already
+An inductive definition may accept parameters, so it can express
+functions that yield sets.
+Relations too can be defined inductively, since they are just sets of pairs.
+A perfect example is the function that maps a relation to its
+reflexive transitive closure. This concept was already
introduced in \S\ref{sec:Relations}, where the operator \isa{{\isacharcircum}{\isacharasterisk}} was
defined as a least fixed point because inductive definitions were not yet
available. But now they are:%
@@ -32,9 +34,9 @@
The above definition of the concept of reflexive transitive closure may
be sufficiently intuitive but it is certainly not the only possible one:
-for a start, it does not even mention transitivity explicitly.
+for a start, it does not even mention transitivity.
The rest of this section is devoted to proving that it is equivalent to
-the ``standard'' definition. We start with a simple lemma:%
+the standard definition. We start with a simple lemma:%
\end{isamarkuptext}%
\isacommand{lemma}\ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharcolon}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
\isacommand{by}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}step{\isacharparenright}%
@@ -45,7 +47,7 @@
danger of killing the automatic tactics because \isa{r{\isacharasterisk}} occurs only in
the conclusion and not in the premise. Thus some proofs that would otherwise
need \isa{rtc{\isacharunderscore}step} can now be found automatically. The proof also
-shows that \isa{blast} is quite able to handle \isa{rtc{\isacharunderscore}step}. But
+shows that \isa{blast} is able to handle \isa{rtc{\isacharunderscore}step}. But
some of the other automatic tactics are more sensitive, and even \isa{blast} can be lead astray in the presence of large numbers of rules.
To prove transitivity, we need rule induction, i.e.\ theorem
@@ -149,8 +151,9 @@
So why did we start with the first definition? Because it is simpler. It
contains only two rules, and the single step rule is simpler than
transitivity. As a consequence, \isa{rtc{\isachardot}induct} is simpler than
-\isa{rtc{\isadigit{2}}{\isachardot}induct}. Since inductive proofs are hard enough, we should
-certainly pick the simplest induction schema available for any concept.
+\isa{rtc{\isadigit{2}}{\isachardot}induct}. Since inductive proofs are hard enough
+anyway, we should
+certainly pick the simplest induction schema available.
Hence \isa{rtc} is the definition of choice.
\begin{exercise}\label{ex:converse-rtc-step}