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 ***
     1 %

     2 \begin{isabellebody}%

     3 \def\isabellecontext{Star}%

     4 %

     5 \isamarkupsection{The reflexive transitive closure%

     6 }

     7 %

     8 \begin{isamarkuptext}%

     9 \label{sec:rtc}

    10 Many inductive definitions define proper relations rather than merely set

    11 like \isa{even}. A perfect example is the

    12 reflexive transitive closure of a relation. This concept was already

    13 introduced in \S\ref{sec:Relations}, where the operator \isa{{\isacharcircum}{\isacharasterisk}} was

    14 defined as a least fixed point because inductive definitions were not yet

    15 available. But now they are:%

    16 \end{isamarkuptext}%

    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

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

    19 \isakeyword{intros}\isanewline

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

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

    22 \begin{isamarkuptext}%

    23 \noindent

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

    25 \isa{rtc\ r} we can read and write \isa{r{\isacharasterisk}}. The actual definition

    26 consists of two rules. Reflexivity is obvious and is immediately given the

    27 \isa{iff} attribute to increase automation. The

    28 second rule, \isa{rtc{\isacharunderscore}step}, says that we can always add one more

    29 \isa{r}-step to the left. Although we could make \isa{rtc{\isacharunderscore}step} an

    30 introduction rule, this is dangerous: the recursion in the second premise

    31 slows down and may even kill the automatic tactics.

    32

    33 The above definition of the concept of reflexive transitive closure may

    34 be sufficiently intuitive but it is certainly not the only possible one:

    35 for a start, it does not even mention transitivity explicitly.

    36 The rest of this section is devoted to proving that it is equivalent to

    37 the standard'' definition. We start with a simple lemma:%

    38 \end{isamarkuptext}%

    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

    40 \isacommand{by}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}step{\isacharparenright}%

    41 \begin{isamarkuptext}%

    42 \noindent

    43 Although the lemma itself is an unremarkable consequence of the basic rules,

    44 it has the advantage that it can be declared an introduction rule without the

    45 danger of killing the automatic tactics because \isa{r{\isacharasterisk}} occurs only in

    46 the conclusion and not in the premise. Thus some proofs that would otherwise

    47 need \isa{rtc{\isacharunderscore}step} can now be found automatically. The proof also

    48 shows that \isa{blast} is quite able to handle \isa{rtc{\isacharunderscore}step}. But

    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.

    50

    51 To prove transitivity, we need rule induction, i.e.\ theorem

    52 \isa{rtc{\isachardot}induct}:

    53 \begin{isabelle}%

    54 \ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}{\isacharquery}xb{\isacharcomma}\ {\isacharquery}xa{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ x{\isacharsemicolon}\isanewline

    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

    56 \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharquery}P\ {\isacharquery}xb\ {\isacharquery}xa%

    57 \end{isabelle}

    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,

    59 i.e.\ if \isa{{\isacharquery}P} holds for the conclusion provided it holds for the

    60 premises. In general, rule induction for an $n$-ary inductive relation $R$

    61 expects a premise of the form $(x@1,\dots,x@n) \in R$.

    62

    63 Now we turn to the inductive proof of transitivity:%

    64 \end{isamarkuptext}%

    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

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

    67 \begin{isamarkuptxt}%

    68 \noindent

    69 Unfortunately, even the resulting base case is a problem

    70 \begin{isabelle}%

    71 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}%

    72 \end{isabelle}

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

    74 To understand what is going on, let us look again at \isa{rtc{\isachardot}induct}.

    75 In the above application of \isa{erule}, the first premise of

    76 \isa{rtc{\isachardot}induct} is unified with the first suitable assumption, which

    77 is \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}} rather than \isa{{\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}}. Although that

    78 is what we want, it is merely due to the order in which the assumptions occur

    79 in the subgoal, which it is not good practice to rely on. As a result,

    80 \isa{{\isacharquery}xb} becomes \isa{x}, \isa{{\isacharquery}xa} becomes

    81 \isa{y} and \isa{{\isacharquery}P} becomes \isa{{\isasymlambda}u\ v{\isachardot}\ {\isacharparenleft}u{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}}, thus

    82 yielding the above subgoal. So what went wrong?

    83

    84 When looking at the instantiation of \isa{{\isacharquery}P} we see that it does not

    85 depend on its second parameter at all. The reason is that in our original

    86 goal, of the pair \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}} only \isa{x} appears also in the

    87 conclusion, but not \isa{y}. Thus our induction statement is too

    88 weak. Fortunately, it can easily be strengthened:

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

    90 \end{isamarkuptxt}%

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

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

    93 \begin{isamarkuptxt}%

    94 \noindent

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

    96 \begin{quote}\em

    97 Whe proving a statement by rule induction on $(x@1,\dots,x@n) \in R$,

    98 pull all other premises containing any of the $x@i$ into the conclusion

    99 using $\longrightarrow$.

   100 \end{quote}

   101 A similar heuristic for other kinds of inductions is formulated in

   102 \S\ref{sec:ind-var-in-prems}. The \isa{rule{\isacharunderscore}format} directive turns

   103 \isa{{\isasymlongrightarrow}} back into \isa{{\isasymLongrightarrow}}. Thus in the end we obtain the original

   104 statement of our lemma.%

   105 \end{isamarkuptxt}%

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

   107 \begin{isamarkuptxt}%

   108 \noindent

   109 Now induction produces two subgoals which are both proved automatically:

   110 \begin{isabelle}%

   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

   112 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}x\ y\ za{\isachardot}\isanewline

   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

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

   115 \end{isabelle}%

   116 \end{isamarkuptxt}%

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

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

   119 \isacommand{done}%

   120 \begin{isamarkuptext}%

   121 Let us now prove that \isa{r{\isacharasterisk}} is really the reflexive transitive closure

   122 of \isa{r}, i.e.\ the least reflexive and transitive

   123 relation containing \isa{r}. The latter is easily formalized%

   124 \end{isamarkuptext}%

   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

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

   127 \isakeyword{intros}\isanewline

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

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

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

   131 \begin{isamarkuptext}%

   132 \noindent

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

   134 inductions:%

   135 \end{isamarkuptext}%

   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

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

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

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

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

   141 \isacommand{done}\isanewline

   142 \isanewline

   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

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

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

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

   147 \isacommand{done}%

   148 \begin{isamarkuptext}%

   149 So why did we start with the first definition? Because it is simpler. It

   150 contains only two rules, and the single step rule is simpler than

   151 transitivity.  As a consequence, \isa{rtc{\isachardot}induct} is simpler than

   152 \isa{rtc{\isadigit{2}}{\isachardot}induct}. Since inductive proofs are hard enough, we should

   153 certainly pick the simplest induction schema available for any concept.

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

   155

   156 \begin{exercise}\label{ex:converse-rtc-step}

   157 Show that the converse of \isa{rtc{\isacharunderscore}step} also holds:

   158 \begin{isabelle}%

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

   160 \end{isabelle}

   161 \end{exercise}

   162 \begin{exercise}

   163 Repeat the development of this section, but starting with a definition of

   164 \isa{rtc} where \isa{rtc{\isacharunderscore}step} is replaced by its converse as shown

   165 in exercise~\ref{ex:converse-rtc-step}.

   166 \end{exercise}%

   167 \end{isamarkuptext}%

   168 \end{isabellebody}%

   169 %%% Local Variables:

   170 %%% mode: latex

   171 %%% TeX-master: "root"

   172 %%% End: