doc-src/TutorialI/Inductive/document/Star.tex
 author nipkow Wed Dec 06 13:22:58 2000 +0100 (2000-12-06) changeset 10608 620647438780 parent 10601 894f845c3dbf child 10617 adc0ed64a120 permissions -rw-r--r--
*** empty log message ***
 nipkow@10225  1 %  nipkow@10225  2 \begin{isabellebody}%  nipkow@10225  3 \def\isabellecontext{Star}%  nipkow@10225  4 %  wenzelm@10395  5 \isamarkupsection{The reflexive transitive closure%  wenzelm@10395  6 }  nipkow@10225  7 %  nipkow@10225  8 \begin{isamarkuptext}%  nipkow@10242  9 \label{sec:rtc}  nipkow@10520  10 Many inductive definitions define proper relations rather than merely set  nipkow@10520  11 like \isa{even}. A perfect example is the  nipkow@10520  12 reflexive transitive closure of a relation. This concept was already  nipkow@10520  13 introduced in \S\ref{sec:Relations}, where the operator \isa{{\isacharcircum}{\isacharasterisk}} was  nipkow@10520  14 defined as a least fixed point because inductive definitions were not yet  nipkow@10520  15 available. But now they are:%  nipkow@10225  16 \end{isamarkuptext}%  nipkow@10242  17 \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  nipkow@10225  18 \isacommand{inductive}\ {\isachardoublequote}r{\isacharasterisk}{\isachardoublequote}\isanewline  nipkow@10225  19 \isakeyword{intros}\isanewline  nipkow@10242  20 rtc{\isacharunderscore}refl{\isacharbrackleft}iff{\isacharbrackright}{\isacharcolon}\ \ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline  nipkow@10242  21 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}%  nipkow@10242  22 \begin{isamarkuptext}%  nipkow@10242  23 \noindent  nipkow@10242  24 The function \isa{rtc} is annotated with concrete syntax: instead of  nipkow@10520  25 \isa{rtc\ r} we can read and write \isa{r{\isacharasterisk}}. The actual definition  nipkow@10520  26 consists of two rules. Reflexivity is obvious and is immediately given the  nipkow@10520  27 \isa{iff} attribute to increase automation. The  nipkow@10363  28 second rule, \isa{rtc{\isacharunderscore}step}, says that we can always add one more  nipkow@10363  29 \isa{r}-step to the left. Although we could make \isa{rtc{\isacharunderscore}step} an  nipkow@10520  30 introduction rule, this is dangerous: the recursion in the second premise  nipkow@10520  31 slows down and may even kill the automatic tactics.  nipkow@10242  32 nipkow@10242  33 The above definition of the concept of reflexive transitive closure may  nipkow@10242  34 be sufficiently intuitive but it is certainly not the only possible one:  nipkow@10242  35 for a start, it does not even mention transitivity explicitly.  nipkow@10242  36 The rest of this section is devoted to proving that it is equivalent to  nipkow@10242  37 the standard'' definition. We start with a simple lemma:%  nipkow@10242  38 \end{isamarkuptext}%  nipkow@10225  39 \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  nipkow@10242  40 \isacommand{by}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}step{\isacharparenright}%  nipkow@10242  41 \begin{isamarkuptext}%  nipkow@10242  42 \noindent  nipkow@10242  43 Although the lemma itself is an unremarkable consequence of the basic rules,  nipkow@10242  44 it has the advantage that it can be declared an introduction rule without the  nipkow@10242  45 danger of killing the automatic tactics because \isa{r{\isacharasterisk}} occurs only in  nipkow@10242  46 the conclusion and not in the premise. Thus some proofs that would otherwise  nipkow@10242  47 need \isa{rtc{\isacharunderscore}step} can now be found automatically. The proof also  nipkow@10242  48 shows that \isa{blast} is quite able to handle \isa{rtc{\isacharunderscore}step}. But  nipkow@10242  49 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  50 nipkow@10520  51 To prove transitivity, we need rule induction, i.e.\ theorem  nipkow@10520  52 \isa{rtc{\isachardot}induct}:  nipkow@10520  53 \begin{isabelle}%  paulson@10601  54 \ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}{\isacharquery}xb{\isacharcomma}\ {\isacharquery}xa{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ x{\isacharsemicolon}\isanewline  paulson@10601  55 \ \ \ \ \ \ \ \ {\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  paulson@10601  56 \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharquery}P\ {\isacharquery}xb\ {\isacharquery}xa%  nipkow@10520  57 \end{isabelle}  nipkow@10520  58 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  59 i.e.\ if \isa{{\isacharquery}P} holds for the conclusion provided it holds for the  nipkow@10520  60 premises. In general, rule induction for an $n$-ary inductive relation $R$  nipkow@10520  61 expects a premise of the form $(x@1,\dots,x@n) \in R$.  nipkow@10520  62 nipkow@10520  63 Now we turn to the inductive proof of transitivity:%  nipkow@10242  64 \end{isamarkuptext}%  nipkow@10520  65 \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  nipkow@10242  66 \isacommand{apply}{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}%  nipkow@10363  67 \begin{isamarkuptxt}%  nipkow@10242  68 \noindent  nipkow@10520  69 Unfortunately, even the resulting base case is a problem  nipkow@10363  70 \begin{isabelle}%  nipkow@10363  71 \ {\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  72 \end{isabelle}  nipkow@10242  73 and maybe not what you had expected. We have to abandon this proof attempt.  nipkow@10520  74 To understand what is going on, let us look again at \isa{rtc{\isachardot}induct}.  nipkow@10520  75 In the above application of \isa{erule}, the first premise of  nipkow@10520  76 \isa{rtc{\isachardot}induct} is unified with the first suitable assumption, which  nipkow@10520  77 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  78 is what we want, it is merely due to the order in which the assumptions occur  nipkow@10520  79 in the subgoal, which it is not good practice to rely on. As a result,  nipkow@10520  80 \isa{{\isacharquery}xb} becomes \isa{x}, \isa{{\isacharquery}xa} becomes  nipkow@10520  81 \isa{y} and \isa{{\isacharquery}P} becomes \isa{{\isasymlambda}u\ v{\isachardot}\ {\isacharparenleft}u{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}}, thus  nipkow@10242  82 yielding the above subgoal. So what went wrong?  nipkow@10242  83 nipkow@10520  84 When looking at the instantiation of \isa{{\isacharquery}P} we see that it does not  nipkow@10520  85 depend on its second parameter at all. The reason is that in our original  nipkow@10520  86 goal, of the pair \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}} only \isa{x} appears also in the  nipkow@10520  87 conclusion, but not \isa{y}. Thus our induction statement is too  nipkow@10520  88 weak. Fortunately, it can easily be strengthened:  nipkow@10242  89 transfer the additional premise \isa{{\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}} into the conclusion:%  nipkow@10363  90 \end{isamarkuptxt}%  nipkow@10242  91 \isacommand{lemma}\ rtc{\isacharunderscore}trans{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline  nipkow@10242  92 \ \ {\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}%  nipkow@10242  93 \begin{isamarkuptxt}%  nipkow@10242  94 \noindent  nipkow@10242  95 This is not an obscure trick but a generally applicable heuristic:  nipkow@10242  96 \begin{quote}\em  nipkow@10242  97 Whe proving a statement by rule induction on $(x@1,\dots,x@n) \in R$,  nipkow@10242  98 pull all other premises containing any of the $x@i$ into the conclusion  nipkow@10242  99 using $\longrightarrow$.  nipkow@10242  100 \end{quote}  nipkow@10242  101 A similar heuristic for other kinds of inductions is formulated in  nipkow@10242  102 \S\ref{sec:ind-var-in-prems}. The \isa{rule{\isacharunderscore}format} directive turns  nipkow@10242  103 \isa{{\isasymlongrightarrow}} back into \isa{{\isasymLongrightarrow}}. Thus in the end we obtain the original  nipkow@10363  104 statement of our lemma.%  nipkow@10363  105 \end{isamarkuptxt}%  nipkow@10363  106 \isacommand{apply}{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}%  nipkow@10363  107 \begin{isamarkuptxt}%  nipkow@10363  108 \noindent  nipkow@10242  109 Now induction produces two subgoals which are both proved automatically:  nipkow@10363  110 \begin{isabelle}%  nipkow@10242  111 \ {\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  112 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}x\ y\ za{\isachardot}\isanewline  paulson@10601  113 \ \ \ \ \ \ \ {\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  paulson@10601  114 \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}za{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}%  nipkow@10242  115 \end{isabelle}%  nipkow@10242  116 \end{isamarkuptxt}%  nipkow@10225  117 \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline  nipkow@10237  118 \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}step{\isacharparenright}\isanewline  nipkow@10242  119 \isacommand{done}%  nipkow@10242  120 \begin{isamarkuptext}%  nipkow@10242  121 Let us now prove that \isa{r{\isacharasterisk}} is really the reflexive transitive closure  nipkow@10242  122 of \isa{r}, i.e.\ the least reflexive and transitive  nipkow@10242  123 relation containing \isa{r}. The latter is easily formalized%  nipkow@10242  124 \end{isamarkuptext}%  nipkow@10237  125 \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  nipkow@10237  126 \isacommand{inductive}\ {\isachardoublequote}rtc{\isadigit{2}}\ r{\isachardoublequote}\isanewline  nipkow@10225  127 \isakeyword{intros}\isanewline  nipkow@10237  128 {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequote}\isanewline  nipkow@10237  129 {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequote}\isanewline  nipkow@10237  130 {\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}%  nipkow@10237  131 \begin{isamarkuptext}%  nipkow@10242  132 \noindent  nipkow@10242  133 and the equivalence of the two definitions is easily shown by the obvious rule  nipkow@10237  134 inductions:%  nipkow@10237  135 \end{isamarkuptext}%  nipkow@10237  136 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline  nipkow@10237  137 \isacommand{apply}{\isacharparenleft}erule\ rtc{\isadigit{2}}{\isachardot}induct{\isacharparenright}\isanewline  nipkow@10237  138 \ \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline  nipkow@10237  139 \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline  nipkow@10237  140 \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}trans{\isacharparenright}\isanewline  nipkow@10237  141 \isacommand{done}\isanewline  nipkow@10225  142 \isanewline  nipkow@10237  143 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequote}\isanewline  nipkow@10237  144 \isacommand{apply}{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}\isanewline  nipkow@10237  145 \ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isadigit{2}}{\isachardot}intros{\isacharparenright}\isanewline  nipkow@10237  146 \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isadigit{2}}{\isachardot}intros{\isacharparenright}\isanewline  nipkow@10242  147 \isacommand{done}%  nipkow@10242  148 \begin{isamarkuptext}%  nipkow@10242  149 So why did we start with the first definition? Because it is simpler. It  nipkow@10242  150 contains only two rules, and the single step rule is simpler than  nipkow@10242  151 transitivity. As a consequence, \isa{rtc{\isachardot}induct} is simpler than  nipkow@10242  152 \isa{rtc{\isadigit{2}}{\isachardot}induct}. Since inductive proofs are hard enough, we should  nipkow@10242  153 certainly pick the simplest induction schema available for any concept.  nipkow@10242  154 Hence \isa{rtc} is the definition of choice.  nipkow@10242  155 nipkow@10520  156 \begin{exercise}\label{ex:converse-rtc-step}  nipkow@10242  157 Show that the converse of \isa{rtc{\isacharunderscore}step} also holds:  nipkow@10242  158 \begin{isabelle}%  paulson@10601  159 \ \ \ \ \ {\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  160 \end{isabelle}  nipkow@10520  161 \end{exercise}  nipkow@10520  162 \begin{exercise}  nipkow@10520  163 Repeat the development of this section, but starting with a definition of  nipkow@10520  164 \isa{rtc} where \isa{rtc{\isacharunderscore}step} is replaced by its converse as shown  nipkow@10520  165 in exercise~\ref{ex:converse-rtc-step}.  nipkow@10242  166 \end{exercise}%  nipkow@10242  167 \end{isamarkuptext}%  nipkow@10225  168 \end{isabellebody}%  nipkow@10225  169 %%% Local Variables:  nipkow@10225  170 %%% mode: latex  nipkow@10225  171 %%% TeX-master: "root"  nipkow@10225  172 %%% End: