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: