%

\begin{isabellebody}%

\def\isabellecontext{Star}%

%

\isamarkupsection{The reflexive transitive closure%

}

%

\begin{isamarkuptext}%

\label{sec:rtc}

{\bf Say something about inductive relations as opposed to sets? Or has that

been said already? If not, explain induction!}

A perfect example of an inductive definition is the reflexive transitive

closure of a relation. 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:%

\end{isamarkuptext}%

\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

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

\begin{isamarkuptext}%

\noindent

The function \isa{rtc} is annotated with concrete syntax: instead of

\isa{rtc\ r} we can read and write {term"r*"}. The actual definition

consists of two rules. Reflexivity is obvious and is immediately declared an

equivalence rule.  Thus the automatic tools will apply it automatically. 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 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 explicitly.

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

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

\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 quite 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.

Let us now turn to transitivity. It should be a consequence of the definition.%

\end{isamarkuptext}%

\isacommand{lemma}\ rtc{\isacharunderscore}trans{\isacharcolon}\isanewline

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

\begin{isamarkuptxt}%

\noindent

The proof starts canonically by rule induction:%

\end{isamarkuptxt}%

\isacommand{apply}{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}%

\begin{isamarkuptxt}%

\noindent

However, even the resulting 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}

and maybe not what you had expected. We have to abandon this proof attempt.

To understand what is going on,

let us look at the induction rule \isa{rtc{\isachardot}induct}:

\[ \frac{(x,y) \in r^* \qquad \bigwedge x.~P~x~x \quad \dots}{P~x~y} \]

When applying this rule, $x$ becomes \isa{x}, $y$ becomes

\isa{y} and $P~x~y$ becomes \isa{{\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}}, thus

yielding the above subgoal. So what went wrong?

When looking at the instantiation of $P~x~y$ we see

that $P$ 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 weak. Fortunately, it can easily be strengthened:

transfer the additional premise \isa{{\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}} into the conclusion:%

\end{isamarkuptxt}%

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

\begin{isamarkuptxt}%

\noindent

This is not an obscure trick but a generally applicable heuristic:

\begin{quote}\em

Whe 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}}. Thus in the end we obtain the original

statement of our lemma.%

\end{isamarkuptxt}%

\isacommand{apply}{\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

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

\ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}za{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}%

\end{isabelle}%

\end{isamarkuptxt}%

\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline

\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}step{\isacharparenright}\isanewline

\isacommand{done}%

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

\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

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

\begin{isamarkuptext}%

\noindent

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

inductions:%

\end{isamarkuptext}%

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

\isacommand{apply}{\isacharparenleft}erule\ rtc{\isadigit{2}}{\isachardot}induct{\isacharparenright}\isanewline

\ \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline

\ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline

\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}trans{\isacharparenright}\isanewline

\isacommand{done}\isanewline

\isanewline

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

\isacommand{apply}{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}\isanewline

\ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isadigit{2}}{\isachardot}intros{\isacharparenright}\isanewline

\isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isadigit{2}}{\isachardot}intros{\isacharparenright}\isanewline

\isacommand{done}%

\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, we should

certainly pick the simplest induction schema available for any concept.

Hence \isa{rtc} is the definition of choice.

\begin{exercise}

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

\end{isamarkuptext}%

\end{isabellebody}%

%%% Local Variables:

%%% mode: latex

%%% TeX-master: "root"

%%% End: