17914
|
1 |
(*<*)theory Star imports Main begin(*>*)
|
10225
|
2 |
|
67406
|
3 |
section\<open>The Reflexive Transitive Closure\<close>
|
10225
|
4 |
|
67406
|
5 |
text\<open>\label{sec:rtc}
|
11494
|
6 |
\index{reflexive transitive closure!defining inductively|(}%
|
10898
|
7 |
An inductive definition may accept parameters, so it can express
|
|
8 |
functions that yield sets.
|
|
9 |
Relations too can be defined inductively, since they are just sets of pairs.
|
|
10 |
A perfect example is the function that maps a relation to its
|
|
11 |
reflexive transitive closure. This concept was already
|
69505
|
12 |
introduced in \S\ref{sec:Relations}, where the operator \<open>\<^sup>*\<close> was
|
10520
|
13 |
defined as a least fixed point because inductive definitions were not yet
|
|
14 |
available. But now they are:
|
67406
|
15 |
\<close>
|
10225
|
16 |
|
23733
|
17 |
inductive_set
|
|
18 |
rtc :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set" ("_*" [1000] 999)
|
|
19 |
for r :: "('a \<times> 'a)set"
|
|
20 |
where
|
|
21 |
rtc_refl[iff]: "(x,x) \<in> r*"
|
|
22 |
| rtc_step: "\<lbrakk> (x,y) \<in> r; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*"
|
10242
|
23 |
|
67406
|
24 |
text\<open>\noindent
|
69597
|
25 |
The function \<^term>\<open>rtc\<close> is annotated with concrete syntax: instead of
|
|
26 |
\<open>rtc r\<close> we can write \<^term>\<open>r*\<close>. The actual definition
|
10520
|
27 |
consists of two rules. Reflexivity is obvious and is immediately given the
|
69505
|
28 |
\<open>iff\<close> attribute to increase automation. The
|
10363
|
29 |
second rule, @{thm[source]rtc_step}, says that we can always add one more
|
69597
|
30 |
\<^term>\<open>r\<close>-step to the left. Although we could make @{thm[source]rtc_step} an
|
10520
|
31 |
introduction rule, this is dangerous: the recursion in the second premise
|
|
32 |
slows down and may even kill the automatic tactics.
|
10242
|
33 |
|
|
34 |
The above definition of the concept of reflexive transitive closure may
|
|
35 |
be sufficiently intuitive but it is certainly not the only possible one:
|
10898
|
36 |
for a start, it does not even mention transitivity.
|
10242
|
37 |
The rest of this section is devoted to proving that it is equivalent to
|
10898
|
38 |
the standard definition. We start with a simple lemma:
|
67406
|
39 |
\<close>
|
10225
|
40 |
|
11308
|
41 |
lemma [intro]: "(x,y) \<in> r \<Longrightarrow> (x,y) \<in> r*"
|
58860
|
42 |
by(blast intro: rtc_step)
|
10225
|
43 |
|
67406
|
44 |
text\<open>\noindent
|
10242
|
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
|
69597
|
47 |
danger of killing the automatic tactics because \<^term>\<open>r*\<close> occurs only in
|
10242
|
48 |
the conclusion and not in the premise. Thus some proofs that would otherwise
|
|
49 |
need @{thm[source]rtc_step} can now be found automatically. The proof also
|
69505
|
50 |
shows that \<open>blast\<close> is able to handle @{thm[source]rtc_step}. But
|
|
51 |
some of the other automatic tactics are more sensitive, and even \<open>blast\<close> can be lead astray in the presence of large numbers of rules.
|
10242
|
52 |
|
10520
|
53 |
To prove transitivity, we need rule induction, i.e.\ theorem
|
|
54 |
@{thm[source]rtc.induct}:
|
|
55 |
@{thm[display]rtc.induct}
|
69505
|
56 |
It says that \<open>?P\<close> holds for an arbitrary pair @{thm (prem 1) rtc.induct}
|
|
57 |
if \<open>?P\<close> is preserved by all rules of the inductive definition,
|
|
58 |
i.e.\ if \<open>?P\<close> holds for the conclusion provided it holds for the
|
10520
|
59 |
premises. In general, rule induction for an $n$-ary inductive relation $R$
|
|
60 |
expects a premise of the form $(x@1,\dots,x@n) \in R$.
|
|
61 |
|
|
62 |
Now we turn to the inductive proof of transitivity:
|
67406
|
63 |
\<close>
|
10242
|
64 |
|
10520
|
65 |
lemma rtc_trans: "\<lbrakk> (x,y) \<in> r*; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*"
|
10363
|
66 |
apply(erule rtc.induct)
|
|
67 |
|
67406
|
68 |
txt\<open>\noindent
|
11494
|
69 |
Unfortunately, even the base case is a problem:
|
10363
|
70 |
@{subgoals[display,indent=0,goals_limit=1]}
|
11494
|
71 |
We have to abandon this proof attempt.
|
10520
|
72 |
To understand what is going on, let us look again at @{thm[source]rtc.induct}.
|
69505
|
73 |
In the above application of \<open>erule\<close>, the first premise of
|
10520
|
74 |
@{thm[source]rtc.induct} is unified with the first suitable assumption, which
|
69597
|
75 |
is \<^term>\<open>(x,y) \<in> r*\<close> rather than \<^term>\<open>(y,z) \<in> r*\<close>. Although that
|
10520
|
76 |
is what we want, it is merely due to the order in which the assumptions occur
|
|
77 |
in the subgoal, which it is not good practice to rely on. As a result,
|
69597
|
78 |
\<open>?xb\<close> becomes \<^term>\<open>x\<close>, \<open>?xa\<close> becomes
|
|
79 |
\<^term>\<open>y\<close> and \<open>?P\<close> becomes \<^term>\<open>\<lambda>u v. (u,z) \<in> r*\<close>, thus
|
10242
|
80 |
yielding the above subgoal. So what went wrong?
|
|
81 |
|
69505
|
82 |
When looking at the instantiation of \<open>?P\<close> we see that it does not
|
10520
|
83 |
depend on its second parameter at all. The reason is that in our original
|
69597
|
84 |
goal, of the pair \<^term>\<open>(x,y)\<close> only \<^term>\<open>x\<close> appears also in the
|
|
85 |
conclusion, but not \<^term>\<open>y\<close>. Thus our induction statement is too
|
27172
|
86 |
general. Fortunately, it can easily be specialized:
|
69597
|
87 |
transfer the additional premise \<^prop>\<open>(y,z)\<in>r*\<close> into the conclusion:\<close>
|
10363
|
88 |
(*<*)oops(*>*)
|
10242
|
89 |
lemma rtc_trans[rule_format]:
|
|
90 |
"(x,y) \<in> r* \<Longrightarrow> (y,z) \<in> r* \<longrightarrow> (x,z) \<in> r*"
|
|
91 |
|
67406
|
92 |
txt\<open>\noindent
|
10242
|
93 |
This is not an obscure trick but a generally applicable heuristic:
|
|
94 |
\begin{quote}\em
|
11257
|
95 |
When proving a statement by rule induction on $(x@1,\dots,x@n) \in R$,
|
10242
|
96 |
pull all other premises containing any of the $x@i$ into the conclusion
|
|
97 |
using $\longrightarrow$.
|
|
98 |
\end{quote}
|
|
99 |
A similar heuristic for other kinds of inductions is formulated in
|
69505
|
100 |
\S\ref{sec:ind-var-in-prems}. The \<open>rule_format\<close> directive turns
|
|
101 |
\<open>\<longrightarrow>\<close> back into \<open>\<Longrightarrow>\<close>: in the end we obtain the original
|
10242
|
102 |
statement of our lemma.
|
67406
|
103 |
\<close>
|
10242
|
104 |
|
10363
|
105 |
apply(erule rtc.induct)
|
|
106 |
|
67406
|
107 |
txt\<open>\noindent
|
10363
|
108 |
Now induction produces two subgoals which are both proved automatically:
|
|
109 |
@{subgoals[display,indent=0]}
|
67406
|
110 |
\<close>
|
10363
|
111 |
|
58860
|
112 |
apply(blast)
|
|
113 |
apply(blast intro: rtc_step)
|
10225
|
114 |
done
|
|
115 |
|
67406
|
116 |
text\<open>
|
69597
|
117 |
Let us now prove that \<^term>\<open>r*\<close> is really the reflexive transitive closure
|
|
118 |
of \<^term>\<open>r\<close>, i.e.\ the least reflexive and transitive
|
|
119 |
relation containing \<^term>\<open>r\<close>. The latter is easily formalized
|
67406
|
120 |
\<close>
|
10225
|
121 |
|
23733
|
122 |
inductive_set
|
|
123 |
rtc2 :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set"
|
|
124 |
for r :: "('a \<times> 'a)set"
|
|
125 |
where
|
|
126 |
"(x,y) \<in> r \<Longrightarrow> (x,y) \<in> rtc2 r"
|
|
127 |
| "(x,x) \<in> rtc2 r"
|
|
128 |
| "\<lbrakk> (x,y) \<in> rtc2 r; (y,z) \<in> rtc2 r \<rbrakk> \<Longrightarrow> (x,z) \<in> rtc2 r"
|
10225
|
129 |
|
67406
|
130 |
text\<open>\noindent
|
10242
|
131 |
and the equivalence of the two definitions is easily shown by the obvious rule
|
10237
|
132 |
inductions:
|
67406
|
133 |
\<close>
|
10225
|
134 |
|
10237
|
135 |
lemma "(x,y) \<in> rtc2 r \<Longrightarrow> (x,y) \<in> r*"
|
58860
|
136 |
apply(erule rtc2.induct)
|
|
137 |
apply(blast)
|
|
138 |
apply(blast)
|
|
139 |
apply(blast intro: rtc_trans)
|
10237
|
140 |
done
|
|
141 |
|
|
142 |
lemma "(x,y) \<in> r* \<Longrightarrow> (x,y) \<in> rtc2 r"
|
58860
|
143 |
apply(erule rtc.induct)
|
|
144 |
apply(blast intro: rtc2.intros)
|
|
145 |
apply(blast intro: rtc2.intros)
|
10225
|
146 |
done
|
|
147 |
|
67406
|
148 |
text\<open>
|
10242
|
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, @{thm[source]rtc.induct} is simpler than
|
10898
|
152 |
@{thm[source]rtc2.induct}. Since inductive proofs are hard enough
|
11147
|
153 |
anyway, we should always pick the simplest induction schema available.
|
69597
|
154 |
Hence \<^term>\<open>rtc\<close> is the definition of choice.
|
11494
|
155 |
\index{reflexive transitive closure!defining inductively|)}
|
10242
|
156 |
|
10520
|
157 |
\begin{exercise}\label{ex:converse-rtc-step}
|
10242
|
158 |
Show that the converse of @{thm[source]rtc_step} also holds:
|
67613
|
159 |
@{prop[display]"[| (x,y) \<in> r*; (y,z) \<in> r |] ==> (x,z) \<in> r*"}
|
10242
|
160 |
\end{exercise}
|
10520
|
161 |
\begin{exercise}
|
|
162 |
Repeat the development of this section, but starting with a definition of
|
69597
|
163 |
\<^term>\<open>rtc\<close> where @{thm[source]rtc_step} is replaced by its converse as shown
|
10520
|
164 |
in exercise~\ref{ex:converse-rtc-step}.
|
|
165 |
\end{exercise}
|
67406
|
166 |
\<close>
|
10242
|
167 |
(*<*)
|
67613
|
168 |
lemma rtc_step2[rule_format]: "(x,y) \<in> r* \<Longrightarrow> (y,z) \<in> r \<longrightarrow> (x,z) \<in> r*"
|
58860
|
169 |
apply(erule rtc.induct)
|
|
170 |
apply blast
|
12815
|
171 |
apply(blast intro: rtc_step)
|
10242
|
172 |
done
|
|
173 |
|
|
174 |
end
|
|
175 |
(*>*)
|