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