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