3 \def\isabellecontext{Star}%
5 \isamarkupsection{The reflexive transitive closure}
10 {\bf Say something about inductive relations as opposed to sets? Or has that
11 been said already? If not, explain induction!}
13 A perfect example of an inductive definition is the reflexive transitive
14 closure of a relation. This concept was already introduced in
15 \S\ref{sec:rtrancl}, but it was not shown how it is defined. In fact,
16 the operator \isa{{\isacharcircum}{\isacharasterisk}} is not defined inductively but via a least
17 fixpoint because at that point in the theory hierarchy
18 inductive definitions are not yet 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 read and write {term"r*"}. The actual definition
29 consists of two rules. Reflexivity is obvious and is immediately declared an
30 equivalence. Thus the automatic tools will apply it automatically. The second
31 rule, \isa{rtc{\isacharunderscore}step}, says that we can always add one more \isa{r}-step to the left. Although we could make \isa{rtc{\isacharunderscore}step} an
32 introduction rule, this is dangerous: the recursion slows down and may
33 even kill the automatic tactics.
35 The above definition of the concept of reflexive transitive closure may
36 be sufficiently intuitive but it is certainly not the only possible one:
37 for a start, it does not even mention transitivity explicitly.
38 The rest of this section is devoted to proving that it is equivalent to
39 the ``standard'' definition. We start with a simple lemma:%
41 \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
42 \isacommand{by}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}step{\isacharparenright}%
43 \begin{isamarkuptext}%
45 Although the lemma itself is an unremarkable consequence of the basic rules,
46 it has the advantage that it can be declared an introduction rule without the
47 danger of killing the automatic tactics because \isa{r{\isacharasterisk}} occurs only in
48 the conclusion and not in the premise. Thus some proofs that would otherwise
49 need \isa{rtc{\isacharunderscore}step} can now be found automatically. The proof also
50 shows that \isa{blast} is quite able to handle \isa{rtc{\isacharunderscore}step}. But
51 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.
53 Let us now turn to transitivity. It should be a consequence of the definition.%
55 \isacommand{lemma}\ rtc{\isacharunderscore}trans{\isacharcolon}\isanewline
56 \ \ {\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}%
59 The proof starts canonically by rule induction:%
61 \isacommand{apply}{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}%
62 \begin{isamarkuptext}%
64 However, even the resulting base case is a problem
66 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}
68 and maybe not what you had expected. We have to abandon this proof attempt.
69 To understand what is going on,
70 let us look at the induction rule \isa{rtc{\isachardot}induct}:
71 \[ \frac{(x,y) \in r^* \qquad \bigwedge x.~P~x~x \quad \dots}{P~x~y} \]
72 When applying this rule, $x$ becomes \isa{x}, $y$ becomes
73 \isa{y} and $P~x~y$ becomes \isa{{\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}}, thus
74 yielding the above subgoal. So what went wrong?
76 When looking at the instantiation of $P~x~y$ we see
77 that $P$ does not depend on its second parameter at
78 all. The reason is that in our original goal, of the pair \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}} only
79 \isa{x} appears also in the conclusion, but not \isa{y}. Thus our
80 induction statement is too weak. Fortunately, it can easily be strengthened:
81 transfer the additional premise \isa{{\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}} into the conclusion:%
83 \isacommand{lemma}\ rtc{\isacharunderscore}trans{\isacharbrackleft}rule{\isacharunderscore}format{\isacharbrackright}{\isacharcolon}\isanewline
84 \ \ {\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}%
87 This is not an obscure trick but a generally applicable heuristic:
89 Whe proving a statement by rule induction on $(x@1,\dots,x@n) \in R$,
90 pull all other premises containing any of the $x@i$ into the conclusion
91 using $\longrightarrow$.
93 A similar heuristic for other kinds of inductions is formulated in
94 \S\ref{sec:ind-var-in-prems}. The \isa{rule{\isacharunderscore}format} directive turns
95 \isa{{\isasymlongrightarrow}} back into \isa{{\isasymLongrightarrow}}. Thus in the end we obtain the original
96 statement of our lemma.
98 Now induction produces two subgoals which are both proved automatically:
100 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\isanewline
101 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}x\ y\ za{\isachardot}\isanewline
102 \ \ \ \ \ \ \ {\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
103 \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}za{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymlongrightarrow}\ {\isacharparenleft}x{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}
106 \isacommand{apply}{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}\isanewline
107 \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
108 \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}step{\isacharparenright}\isanewline
110 \begin{isamarkuptext}%
111 Let us now prove that \isa{r{\isacharasterisk}} is really the reflexive transitive closure
112 of \isa{r}, i.e.\ the least reflexive and transitive
113 relation containing \isa{r}. The latter is easily formalized%
115 \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
116 \isacommand{inductive}\ {\isachardoublequote}rtc{\isadigit{2}}\ r{\isachardoublequote}\isanewline
117 \isakeyword{intros}\isanewline
118 {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequote}\isanewline
119 {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequote}\isanewline
120 {\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}%
121 \begin{isamarkuptext}%
123 and the equivalence of the two definitions is easily shown by the obvious rule
126 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
127 \isacommand{apply}{\isacharparenleft}erule\ rtc{\isadigit{2}}{\isachardot}induct{\isacharparenright}\isanewline
128 \ \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
129 \ \isacommand{apply}{\isacharparenleft}blast{\isacharparenright}\isanewline
130 \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isacharunderscore}trans{\isacharparenright}\isanewline
131 \isacommand{done}\isanewline
133 \isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequote}\isanewline
134 \isacommand{apply}{\isacharparenleft}erule\ rtc{\isachardot}induct{\isacharparenright}\isanewline
135 \ \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isadigit{2}}{\isachardot}intros{\isacharparenright}\isanewline
136 \isacommand{apply}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isadigit{2}}{\isachardot}intros{\isacharparenright}\isanewline
138 \begin{isamarkuptext}%
139 So why did we start with the first definition? Because it is simpler. It
140 contains only two rules, and the single step rule is simpler than
141 transitivity. As a consequence, \isa{rtc{\isachardot}induct} is simpler than
142 \isa{rtc{\isadigit{2}}{\isachardot}induct}. Since inductive proofs are hard enough, we should
143 certainly pick the simplest induction schema available for any concept.
144 Hence \isa{rtc} is the definition of choice.
147 Show that the converse of \isa{rtc{\isacharunderscore}step} also holds:
149 \ \ \ \ \ {\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}%
156 %%% TeX-master: "root"