doc-src/TutorialI/Inductive/document/Star.tex

use proper context operations (for fresh names of type and term variables, and for hypothetical definitions), monomorphize theorems (instead of terms, necessary for hypothetical definitions made during lambda lifting)

%
\begin{isabellebody}%
\def\isabellecontext{Star}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isamarkupsection{The Reflexive Transitive Closure%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\label{sec:rtc}
\index{reflexive transitive closure!defining inductively|(}%
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{\isactrlsup {\isacharasterisk}} was
defined as a least fixed point because inductive definitions were not yet
available. But now they are:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{inductive{\isacharunderscore}set}\isamarkupfalse%
\isanewline
\ \ rtc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequoteclose}\ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharunderscore}{\isacharasterisk}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline
\ \ \isakeyword{for}\ r\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequoteclose}\isanewline
\isakeyword{where}\isanewline
\ \ rtc{\isacharunderscore}refl{\isacharbrackleft}iff{\isacharbrackright}{\isacharcolon}\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\isanewline
{\isacharbar}\ rtc{\isacharunderscore}step{\isacharcolon}\ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymlbrakk}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent
The function \isa{rtc} is annotated with concrete syntax: instead of
\isa{rtc\ r} we can write \isa{r{\isacharasterisk}}. The actual definition
consists of two rules. Reflexivity is obvious and is immediately given the
\isa{iff} attribute to increase automation. The
second rule, \isa{rtc{\isacharunderscore}step}, says that we can always add one more
\isa{r}-step to the left. Although we could make \isa{rtc{\isacharunderscore}step} an
introduction rule, this is dangerous: the recursion in the second premise
slows down and may even kill the automatic tactics.

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.
The rest of this section is devoted to proving that it is equivalent to
the standard definition. We start with a simple lemma:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
\ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{by}\isamarkupfalse%
{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}step{\isacharparenright}%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\begin{isamarkuptext}%
\noindent
Although the lemma itself is an unremarkable consequence of the basic rules,
it has the advantage that it can be declared an introduction rule without the
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 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
\isa{rtc{\isachardot}induct}:
\begin{isabelle}%
\ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}{\isacharquery}x{\isadigit{1}}{\isachardot}{\isadigit{0}}{\isacharcomma}\ {\isacharquery}x{\isadigit{2}}{\isachardot}{\isadigit{0}}{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ x{\isacharsemicolon}\isanewline
\isaindent{\ \ \ \ \ \ }{\isasymAnd}x\ y\ z{\isachardot}\ {\isasymlbrakk}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}{\isacharsemicolon}\ {\isacharquery}P\ y\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P\ x\ z{\isasymrbrakk}\isanewline
\isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ {\isacharquery}P\ {\isacharquery}x{\isadigit{1}}{\isachardot}{\isadigit{0}}\ {\isacharquery}x{\isadigit{2}}{\isachardot}{\isadigit{0}}%
\end{isabelle}
It says that \isa{{\isacharquery}P} holds for an arbitrary pair \isa{{\isacharparenleft}{\isacharquery}x{\isadigit{1}}{\isachardot}{\isadigit{0}}{\isacharcomma}\ {\isacharquery}x{\isadigit{2}}{\isachardot}{\isadigit{0}}{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}}
if \isa{{\isacharquery}P} is preserved by all rules of the inductive definition,
i.e.\ if \isa{{\isacharquery}P} holds for the conclusion provided it holds for the
premises. In general, rule induction for an $n$-ary inductive relation $R$
expects a premise of the form $(x@1,\dots,x@n) \in R$.

Now we turn to the inductive proof of transitivity:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
\ rtc{\isacharunderscore}trans{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlbrakk}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{apply}\isamarkupfalse%
{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}%
\begin{isamarkuptxt}%
\noindent
Unfortunately, even the base case is a problem:
\begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}%
\end{isabelle}
We have to abandon this proof attempt.
To understand what is going on, let us look again at \isa{rtc{\isachardot}induct}.
In the above application of \isa{erule}, the first premise of
\isa{rtc{\isachardot}induct} is unified with the first suitable assumption, which
is \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}} rather than \isa{{\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}}. Although that
is what we want, it is merely due to the order in which the assumptions occur
in the subgoal, which it is not good practice to rely on. As a result,
\isa{{\isacharquery}xb} becomes \isa{x}, \isa{{\isacharquery}xa} becomes
\isa{y} and \isa{{\isacharquery}P} becomes \isa{{\isasymlambda}u\ v{\isachardot}\ {\isacharparenleft}u{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}}, thus
yielding the above subgoal. So what went wrong?

When looking at the instantiation of \isa{{\isacharquery}P} we see that it does not
depend on its second parameter at all. The reason is that in our original
goal, of the pair \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}} only \isa{x} appears also in the
conclusion, but not \isa{y}. Thus our induction statement is too
general. Fortunately, it can easily be specialized:
transfer the additional premise \isa{{\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}} into the conclusion:%
\end{isamarkuptxt}%
\isamarkuptrue%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
\isacommand{lemma}\isamarkupfalse%
\ rtc{\isacharunderscore}trans{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
%
\begin{isamarkuptxt}%
\noindent
This is not an obscure trick but a generally applicable heuristic:
\begin{quote}\em
When proving a statement by rule induction on $(x@1,\dots,x@n) \in R$,
pull all other premises containing any of the $x@i$ into the conclusion
using $\longrightarrow$.
\end{quote}
A similar heuristic for other kinds of inductions is formulated in
\S\ref{sec:ind-var-in-prems}. The \isa{rule{\isacharunderscore}format} directive turns
\isa{{\isasymlongrightarrow}} back into \isa{{\isasymLongrightarrow}}: in the end we obtain the original
statement of our lemma.%
\end{isamarkuptxt}%
\isamarkuptrue%
\isacommand{apply}\isamarkupfalse%
{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}%
\begin{isamarkuptxt}%
\noindent
Now induction produces two subgoals which are both proved automatically:
\begin{isabelle}%
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\isanewline
\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}x\ y\ za{\isachardot}\isanewline
\isaindent{\ {\isadigit{2}}{\isachardot}\ \ \ \ }{\isasymlbrakk}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}\ za{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isacharsemicolon}\ {\isacharparenleft}za{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isasymrbrakk}\isanewline
\isaindent{\ {\isadigit{2}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ {\isacharparenleft}za{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}%
\end{isabelle}%
\end{isamarkuptxt}%
\isamarkuptrue%
\ \isacommand{apply}\isamarkupfalse%
{\isacharparenleft}blast{\isacharparenright}\isanewline
\isacommand{apply}\isamarkupfalse%
{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}step{\isacharparenright}\isanewline
\isacommand{done}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\begin{isamarkuptext}%
Let us now prove that \isa{r{\isacharasterisk}} is really the reflexive transitive closure
of \isa{r}, i.e.\ the least reflexive and transitive
relation containing \isa{r}. The latter is easily formalized%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{inductive{\isacharunderscore}set}\isamarkupfalse%
\isanewline
\ \ rtc{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{for}\ r\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequoteclose}\isanewline
\isakeyword{where}\isanewline
\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequoteclose}\isanewline
{\isacharbar}\ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequoteclose}\isanewline
{\isacharbar}\ {\isachardoublequoteopen}{\isasymlbrakk}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent
and the equivalence of the two definitions is easily shown by the obvious rule
inductions:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{apply}\isamarkupfalse%
{\isacharparenleft}erule\ rtc{\isadigit{2}}{\isachardot}induct{\isacharparenright}\isanewline
\ \ \isacommand{apply}\isamarkupfalse%
{\isacharparenleft}blast{\isacharparenright}\isanewline
\ \isacommand{apply}\isamarkupfalse%
{\isacharparenleft}blast{\isacharparenright}\isanewline
\isacommand{apply}\isamarkupfalse%
{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}trans{\isacharparenright}\isanewline
\isacommand{done}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
\isanewline
%
\endisadelimproof
\isanewline
\isacommand{lemma}\isamarkupfalse%
\ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
\isacommand{apply}\isamarkupfalse%
{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}\isanewline
\ \isacommand{apply}\isamarkupfalse%
{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isadigit{2}}{\isachardot}intros{\isacharparenright}\isanewline
\isacommand{apply}\isamarkupfalse%
{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isadigit{2}}{\isachardot}intros{\isacharparenright}\isanewline
\isacommand{done}\isamarkupfalse%
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\begin{isamarkuptext}%
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
anyway, we should always pick the simplest induction schema available.
Hence \isa{rtc} is the definition of choice.
\index{reflexive transitive closure!defining inductively|)}

\begin{exercise}\label{ex:converse-rtc-step}
Show that the converse of \isa{rtc{\isacharunderscore}step} also holds:
\begin{isabelle}%
\ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}%
\end{isabelle}
\end{exercise}
\begin{exercise}
Repeat the development of this section, but starting with a definition of
\isa{rtc} where \isa{rtc{\isacharunderscore}step} is replaced by its converse as shown
in exercise~\ref{ex:converse-rtc-step}.
\end{exercise}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimproof
%
\endisadelimproof
%
\isatagproof
%
\endisatagproof
{\isafoldproof}%
%
\isadelimproof
%
\endisadelimproof
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: