%

\begin{isabellebody}%

\def\isabellecontext{Star}%

\isamarkupfalse%

%

\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{consts}\ rtc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequote}\ \ \ {\isacharparenleft}{\isachardoublequote}{\isacharunderscore}{\isacharasterisk}{\isachardoublequote}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline

\isamarkupfalse%

\isacommand{inductive}\ {\isachardoublequote}r{\isacharasterisk}{\isachardoublequote}\isanewline

\isakeyword{intros}\isanewline

rtc{\isacharunderscore}refl{\isacharbrackleft}iff{\isacharbrackright}{\isacharcolon}\ \ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline

rtc{\isacharunderscore}step{\isacharcolon}\ \ \ \ \ \ \ {\isachardoublequote}{\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}{\isachardoublequote}\isamarkupfalse%

%

\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}\ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline

\isamarkupfalse%

\isamarkupfalse%

%

\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}xb{\isacharcomma}\ {\isacharquery}xa{\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}xb\ {\isacharquery}xa%

\end{isabelle}

It says that \isa{{\isacharquery}P} holds for an arbitrary pair \isa{{\isacharparenleft}{\isacharquery}xb{\isacharcomma}{\isacharquery}xa{\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}\ rtc{\isacharunderscore}trans{\isacharcolon}\ {\isachardoublequote}{\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}{\isachardoublequote}\isanewline

\isamarkupfalse%

\isamarkupfalse%

\isamarkuptrue%

\isamarkupfalse%

\isacommand{lemma}\ rtc{\isacharunderscore}trans{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline

\ \ {\isachardoublequote}{\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}{\isachardoublequote}\isamarkupfalse%

\isamarkuptrue%

\isamarkupfalse%

\isamarkuptrue%

\isamarkupfalse%

\isamarkupfalse%

\isamarkupfalse%

%

\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{consts}\ rtc{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequote}\isanewline

\isamarkupfalse%

\isacommand{inductive}\ {\isachardoublequote}rtc{\isadigit{2}}\ r{\isachardoublequote}\isanewline

\isakeyword{intros}\isanewline

{\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequote}\isanewline

{\isachardoublequote}{\isacharparenleft}x{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequote}\isanewline

{\isachardoublequote}{\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{\isachardoublequote}\isamarkupfalse%

%

\begin{isamarkuptext}%

\noindent

and the equivalence of the two definitions is easily shown by the obvious rule

inductions:%

\end{isamarkuptext}%

\isamarkuptrue%

\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline

\isamarkupfalse%

\isamarkupfalse%

\isamarkupfalse%

\isamarkupfalse%

\isamarkupfalse%

\isanewline

\isanewline

\isamarkupfalse%

\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequote}\isanewline

\isamarkupfalse%

\isamarkupfalse%

\isamarkupfalse%

\isamarkupfalse%

\isamarkupfalse%

%

\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%

\isamarkupfalse%

\isamarkupfalse%

\isamarkupfalse%

\isamarkupfalse%

\isamarkupfalse%

\isamarkupfalse%

\end{isabellebody}%

%%% Local Variables:

%%% mode: latex

%%% TeX-master: "root"

%%% End: