nipkow@10225: % nipkow@10225: \begin{isabellebody}% nipkow@10225: \def\isabellecontext{Star}% wenzelm@11866: \isamarkupfalse% nipkow@10225: % paulson@10878: \isamarkupsection{The Reflexive Transitive Closure% wenzelm@10395: } wenzelm@11866: \isamarkuptrue% nipkow@10225: % nipkow@10225: \begin{isamarkuptext}% nipkow@10242: \label{sec:rtc} paulson@11494: \index{reflexive transitive closure!defining inductively|(}% paulson@10878: An inductive definition may accept parameters, so it can express paulson@10878: functions that yield sets. paulson@10878: Relations too can be defined inductively, since they are just sets of pairs. paulson@10878: A perfect example is the function that maps a relation to its paulson@10878: reflexive transitive closure. This concept was already nipkow@11147: introduced in \S\ref{sec:Relations}, where the operator \isa{\isactrlsup {\isacharasterisk}} was nipkow@10520: defined as a least fixed point because inductive definitions were not yet nipkow@10520: available. But now they are:% nipkow@10225: \end{isamarkuptext}% wenzelm@11866: \isamarkuptrue% nipkow@10242: \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 wenzelm@11866: \isamarkupfalse% nipkow@10225: \isacommand{inductive}\ {\isachardoublequote}r{\isacharasterisk}{\isachardoublequote}\isanewline nipkow@10225: \isakeyword{intros}\isanewline nipkow@10242: rtc{\isacharunderscore}refl{\isacharbrackleft}iff{\isacharbrackright}{\isacharcolon}\ \ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline wenzelm@11866: 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% wenzelm@11866: % nipkow@10242: \begin{isamarkuptext}% nipkow@10242: \noindent nipkow@10242: The function \isa{rtc} is annotated with concrete syntax: instead of paulson@11494: \isa{rtc\ r} we can write \isa{r{\isacharasterisk}}. The actual definition nipkow@10520: consists of two rules. Reflexivity is obvious and is immediately given the nipkow@10520: \isa{iff} attribute to increase automation. The nipkow@10363: second rule, \isa{rtc{\isacharunderscore}step}, says that we can always add one more nipkow@10363: \isa{r}-step to the left. Although we could make \isa{rtc{\isacharunderscore}step} an nipkow@10520: introduction rule, this is dangerous: the recursion in the second premise nipkow@10520: slows down and may even kill the automatic tactics. nipkow@10242: nipkow@10242: The above definition of the concept of reflexive transitive closure may nipkow@10242: be sufficiently intuitive but it is certainly not the only possible one: paulson@10878: for a start, it does not even mention transitivity. nipkow@10242: The rest of this section is devoted to proving that it is equivalent to paulson@10878: the standard definition. We start with a simple lemma:% nipkow@10242: \end{isamarkuptext}% wenzelm@11866: \isamarkuptrue% nipkow@11308: \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 wenzelm@11866: \isamarkupfalse% wenzelm@11866: \isacommand{by}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}step{\isacharparenright}\isamarkupfalse% wenzelm@11866: % nipkow@10242: \begin{isamarkuptext}% nipkow@10242: \noindent nipkow@10242: Although the lemma itself is an unremarkable consequence of the basic rules, nipkow@10242: it has the advantage that it can be declared an introduction rule without the nipkow@10242: danger of killing the automatic tactics because \isa{r{\isacharasterisk}} occurs only in nipkow@10242: the conclusion and not in the premise. Thus some proofs that would otherwise nipkow@10242: need \isa{rtc{\isacharunderscore}step} can now be found automatically. The proof also paulson@10878: shows that \isa{blast} is able to handle \isa{rtc{\isacharunderscore}step}. But nipkow@10242: 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. nipkow@10242: nipkow@10520: To prove transitivity, we need rule induction, i.e.\ theorem nipkow@10520: \isa{rtc{\isachardot}induct}: nipkow@10520: \begin{isabelle}% nipkow@10696: \ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}{\isacharquery}xb{\isacharcomma}\ {\isacharquery}xa{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ x{\isacharsemicolon}\isanewline paulson@14379: \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 wenzelm@10950: \isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ {\isacharquery}P\ {\isacharquery}xb\ {\isacharquery}xa% nipkow@10520: \end{isabelle} nipkow@10520: 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, nipkow@10520: i.e.\ if \isa{{\isacharquery}P} holds for the conclusion provided it holds for the nipkow@10520: premises. In general, rule induction for an $n$-ary inductive relation $R$ nipkow@10520: expects a premise of the form $(x@1,\dots,x@n) \in R$. nipkow@10520: nipkow@10520: Now we turn to the inductive proof of transitivity:% nipkow@10242: \end{isamarkuptext}% wenzelm@11866: \isamarkuptrue% nipkow@10520: \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 wenzelm@11866: \isamarkupfalse% wenzelm@11866: \isacommand{apply}{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}\isamarkupfalse% wenzelm@11866: % nipkow@10363: \begin{isamarkuptxt}% nipkow@10242: \noindent paulson@11494: Unfortunately, even the base case is a problem: nipkow@10363: \begin{isabelle}% nipkow@10363: \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}% nipkow@10242: \end{isabelle} paulson@11494: We have to abandon this proof attempt. nipkow@10520: To understand what is going on, let us look again at \isa{rtc{\isachardot}induct}. nipkow@10520: In the above application of \isa{erule}, the first premise of nipkow@10520: \isa{rtc{\isachardot}induct} is unified with the first suitable assumption, which nipkow@10520: is \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}} rather than \isa{{\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}}. Although that nipkow@10520: is what we want, it is merely due to the order in which the assumptions occur nipkow@10520: in the subgoal, which it is not good practice to rely on. As a result, nipkow@10520: \isa{{\isacharquery}xb} becomes \isa{x}, \isa{{\isacharquery}xa} becomes nipkow@10520: \isa{y} and \isa{{\isacharquery}P} becomes \isa{{\isasymlambda}u\ v{\isachardot}\ {\isacharparenleft}u{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}}, thus nipkow@10242: yielding the above subgoal. So what went wrong? nipkow@10242: nipkow@10520: When looking at the instantiation of \isa{{\isacharquery}P} we see that it does not nipkow@10520: depend on its second parameter at all. The reason is that in our original nipkow@10520: goal, of the pair \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}} only \isa{x} appears also in the nipkow@10520: conclusion, but not \isa{y}. Thus our induction statement is too nipkow@10520: weak. Fortunately, it can easily be strengthened: nipkow@10242: transfer the additional premise \isa{{\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}} into the conclusion:% nipkow@10363: \end{isamarkuptxt}% wenzelm@11866: \isamarkuptrue% wenzelm@11866: \isamarkupfalse% nipkow@10242: \isacommand{lemma}\ rtc{\isacharunderscore}trans{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline wenzelm@11866: \ \ {\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% wenzelm@11866: % nipkow@10242: \begin{isamarkuptxt}% nipkow@10242: \noindent nipkow@10242: This is not an obscure trick but a generally applicable heuristic: nipkow@10242: \begin{quote}\em nipkow@11257: When proving a statement by rule induction on $(x@1,\dots,x@n) \in R$, nipkow@10242: pull all other premises containing any of the $x@i$ into the conclusion nipkow@10242: using $\longrightarrow$. nipkow@10242: \end{quote} nipkow@10242: A similar heuristic for other kinds of inductions is formulated in nipkow@10242: \S\ref{sec:ind-var-in-prems}. The \isa{rule{\isacharunderscore}format} directive turns nipkow@11147: \isa{{\isasymlongrightarrow}} back into \isa{{\isasymLongrightarrow}}: in the end we obtain the original nipkow@10363: statement of our lemma.% nipkow@10363: \end{isamarkuptxt}% wenzelm@11866: \isamarkuptrue% wenzelm@11866: \isacommand{apply}{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}\isamarkupfalse% wenzelm@11866: % nipkow@10363: \begin{isamarkuptxt}% nipkow@10363: \noindent nipkow@10242: Now induction produces two subgoals which are both proved automatically: nipkow@10363: \begin{isabelle}% nipkow@10242: \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\isanewline nipkow@10242: \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}x\ y\ za{\isachardot}\isanewline wenzelm@10950: \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 wenzelm@10950: \isaindent{\ {\isadigit{2}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ {\isacharparenleft}za{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}% nipkow@10242: \end{isabelle}% nipkow@10242: \end{isamarkuptxt}% wenzelm@11866: \ \isamarkuptrue% wenzelm@11866: \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline wenzelm@11866: \isamarkupfalse% nipkow@10237: \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}step{\isacharparenright}\isanewline wenzelm@11866: \isamarkupfalse% wenzelm@11866: \isacommand{done}\isamarkupfalse% wenzelm@11866: % nipkow@10242: \begin{isamarkuptext}% nipkow@10242: Let us now prove that \isa{r{\isacharasterisk}} is really the reflexive transitive closure nipkow@10242: of \isa{r}, i.e.\ the least reflexive and transitive nipkow@10242: relation containing \isa{r}. The latter is easily formalized% nipkow@10242: \end{isamarkuptext}% wenzelm@11866: \isamarkuptrue% nipkow@10237: \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 wenzelm@11866: \isamarkupfalse% nipkow@10237: \isacommand{inductive}\ {\isachardoublequote}rtc{\isadigit{2}}\ r{\isachardoublequote}\isanewline nipkow@10225: \isakeyword{intros}\isanewline nipkow@10237: {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequote}\isanewline nipkow@10237: {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequote}\isanewline wenzelm@11866: {\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% wenzelm@11866: % nipkow@10237: \begin{isamarkuptext}% nipkow@10242: \noindent nipkow@10242: and the equivalence of the two definitions is easily shown by the obvious rule nipkow@10237: inductions:% nipkow@10237: \end{isamarkuptext}% wenzelm@11866: \isamarkuptrue% nipkow@10237: \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline wenzelm@11866: \isamarkupfalse% nipkow@10237: \isacommand{apply}{\isacharparenleft}erule\ rtc{\isadigit{2}}{\isachardot}induct{\isacharparenright}\isanewline wenzelm@11866: \ \ \isamarkupfalse% wenzelm@11866: \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline wenzelm@11866: \ \isamarkupfalse% wenzelm@11866: \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline wenzelm@11866: \isamarkupfalse% nipkow@10237: \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}trans{\isacharparenright}\isanewline wenzelm@11866: \isamarkupfalse% nipkow@10237: \isacommand{done}\isanewline nipkow@10225: \isanewline wenzelm@11866: \isamarkupfalse% nipkow@10237: \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequote}\isanewline wenzelm@11866: \isamarkupfalse% nipkow@10237: \isacommand{apply}{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}\isanewline wenzelm@11866: \ \isamarkupfalse% nipkow@10237: \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isadigit{2}}{\isachardot}intros{\isacharparenright}\isanewline wenzelm@11866: \isamarkupfalse% wenzelm@11866: \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isadigit{2}}{\isachardot}intros{\isacharparenright}\isanewline wenzelm@11866: \isamarkupfalse% wenzelm@11866: \isacommand{done}\isamarkupfalse% wenzelm@11866: % nipkow@10242: \begin{isamarkuptext}% nipkow@10242: So why did we start with the first definition? Because it is simpler. It nipkow@10242: contains only two rules, and the single step rule is simpler than nipkow@10242: transitivity. As a consequence, \isa{rtc{\isachardot}induct} is simpler than paulson@10878: \isa{rtc{\isadigit{2}}{\isachardot}induct}. Since inductive proofs are hard enough nipkow@11147: anyway, we should always pick the simplest induction schema available. nipkow@10242: Hence \isa{rtc} is the definition of choice. paulson@11494: \index{reflexive transitive closure!defining inductively|)} nipkow@10242: nipkow@10520: \begin{exercise}\label{ex:converse-rtc-step} nipkow@10242: Show that the converse of \isa{rtc{\isacharunderscore}step} also holds: nipkow@10242: \begin{isabelle}% nipkow@10696: \ \ \ \ \ {\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}% nipkow@10242: \end{isabelle} nipkow@10520: \end{exercise} nipkow@10520: \begin{exercise} nipkow@10520: Repeat the development of this section, but starting with a definition of nipkow@10520: \isa{rtc} where \isa{rtc{\isacharunderscore}step} is replaced by its converse as shown nipkow@10520: in exercise~\ref{ex:converse-rtc-step}. nipkow@10242: \end{exercise}% nipkow@10242: \end{isamarkuptext}% wenzelm@11866: \isamarkuptrue% wenzelm@11866: \isamarkupfalse% wenzelm@11866: \isamarkupfalse% wenzelm@11866: \isamarkupfalse% wenzelm@11866: \isamarkupfalse% wenzelm@11866: \isamarkupfalse% wenzelm@11866: \isamarkupfalse% nipkow@10225: \end{isabellebody}% nipkow@10225: %%% Local Variables: nipkow@10225: %%% mode: latex nipkow@10225: %%% TeX-master: "root" nipkow@10225: %%% End: