1 (*<*)theory Star = Main:(*>*) |
1 (*<*)theory Star = Main:(*>*) |
2 |
2 |
3 section{*The reflexive transitive closure*} |
3 section{*The reflexive transitive closure*} |
4 |
4 |
5 text{*\label{sec:rtc} |
5 text{*\label{sec:rtc} |
6 {\bf Say something about inductive relations as opposed to sets? Or has that |
6 Many inductive definitions define proper relations rather than merely set |
7 been said already? If not, explain induction!} |
7 like @{term even}. A perfect example is the |
8 |
8 reflexive transitive closure of a relation. This concept was already |
9 A perfect example of an inductive definition is the reflexive transitive |
9 introduced in \S\ref{sec:Relations}, where the operator @{text"^*"} was |
10 closure of a relation. This concept was already introduced in |
10 defined as a least fixed point because inductive definitions were not yet |
11 \S\ref{sec:Relations}, where the operator @{text"^*"} was |
11 available. But now they are: |
12 defined as a least fixed point because |
|
13 inductive definitions were not yet available. But now they are: |
|
14 *} |
12 *} |
15 |
13 |
16 consts rtc :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set" ("_*" [1000] 999) |
14 consts rtc :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set" ("_*" [1000] 999) |
17 inductive "r*" |
15 inductive "r*" |
18 intros |
16 intros |
19 rtc_refl[iff]: "(x,x) \<in> r*" |
17 rtc_refl[iff]: "(x,x) \<in> r*" |
20 rtc_step: "\<lbrakk> (x,y) \<in> r; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*" |
18 rtc_step: "\<lbrakk> (x,y) \<in> r; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*" |
21 |
19 |
22 text{*\noindent |
20 text{*\noindent |
23 The function @{term rtc} is annotated with concrete syntax: instead of |
21 The function @{term rtc} is annotated with concrete syntax: instead of |
24 @{text"rtc r"} we can read and write {term"r*"}. The actual definition |
22 @{text"rtc r"} we can read and write @{term"r*"}. The actual definition |
25 consists of two rules. Reflexivity is obvious and is immediately declared an |
23 consists of two rules. Reflexivity is obvious and is immediately given the |
26 equivalence rule. Thus the automatic tools will apply it automatically. The |
24 @{text iff} attribute to increase automation. The |
27 second rule, @{thm[source]rtc_step}, says that we can always add one more |
25 second rule, @{thm[source]rtc_step}, says that we can always add one more |
28 @{term r}-step to the left. Although we could make @{thm[source]rtc_step} an |
26 @{term r}-step to the left. Although we could make @{thm[source]rtc_step} an |
29 introduction rule, this is dangerous: the recursion slows down and may |
27 introduction rule, this is dangerous: the recursion in the second premise |
30 even kill the automatic tactics. |
28 slows down and may even kill the automatic tactics. |
31 |
29 |
32 The above definition of the concept of reflexive transitive closure may |
30 The above definition of the concept of reflexive transitive closure may |
33 be sufficiently intuitive but it is certainly not the only possible one: |
31 be sufficiently intuitive but it is certainly not the only possible one: |
34 for a start, it does not even mention transitivity explicitly. |
32 for a start, it does not even mention transitivity explicitly. |
35 The rest of this section is devoted to proving that it is equivalent to |
33 The rest of this section is devoted to proving that it is equivalent to |
43 Although the lemma itself is an unremarkable consequence of the basic rules, |
41 Although the lemma itself is an unremarkable consequence of the basic rules, |
44 it has the advantage that it can be declared an introduction rule without the |
42 it has the advantage that it can be declared an introduction rule without the |
45 danger of killing the automatic tactics because @{term"r*"} occurs only in |
43 danger of killing the automatic tactics because @{term"r*"} occurs only in |
46 the conclusion and not in the premise. Thus some proofs that would otherwise |
44 the conclusion and not in the premise. Thus some proofs that would otherwise |
47 need @{thm[source]rtc_step} can now be found automatically. The proof also |
45 need @{thm[source]rtc_step} can now be found automatically. The proof also |
48 shows that @{term blast} is quite able to handle @{thm[source]rtc_step}. But |
46 shows that @{text blast} is quite able to handle @{thm[source]rtc_step}. But |
49 some of the other automatic tactics are more sensitive, and even @{text |
47 some of the other automatic tactics are more sensitive, and even @{text |
50 blast} can be lead astray in the presence of large numbers of rules. |
48 blast} can be lead astray in the presence of large numbers of rules. |
51 |
49 |
52 Let us now turn to transitivity. It should be a consequence of the definition. |
50 To prove transitivity, we need rule induction, i.e.\ theorem |
|
51 @{thm[source]rtc.induct}: |
|
52 @{thm[display]rtc.induct} |
|
53 It says that @{text"?P"} holds for an arbitrary pair @{text"(?xb,?xa) \<in> |
|
54 ?r*"} if @{text"?P"} is preserved by all rules of the inductive definition, |
|
55 i.e.\ if @{text"?P"} holds for the conclusion provided it holds for the |
|
56 premises. In general, rule induction for an $n$-ary inductive relation $R$ |
|
57 expects a premise of the form $(x@1,\dots,x@n) \in R$. |
|
58 |
|
59 Now we turn to the inductive proof of transitivity: |
53 *} |
60 *} |
54 |
61 |
55 lemma rtc_trans: |
62 lemma rtc_trans: "\<lbrakk> (x,y) \<in> r*; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*" |
56 "\<lbrakk> (x,y) \<in> r*; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*" |
|
57 |
|
58 txt{*\noindent |
|
59 The proof starts canonically by rule induction: |
|
60 *} |
|
61 |
|
62 apply(erule rtc.induct) |
63 apply(erule rtc.induct) |
63 |
64 |
64 txt{*\noindent |
65 txt{*\noindent |
65 However, even the resulting base case is a problem |
66 Unfortunately, even the resulting base case is a problem |
66 @{subgoals[display,indent=0,goals_limit=1]} |
67 @{subgoals[display,indent=0,goals_limit=1]} |
67 and maybe not what you had expected. We have to abandon this proof attempt. |
68 and maybe not what you had expected. We have to abandon this proof attempt. |
68 To understand what is going on, |
69 To understand what is going on, let us look again at @{thm[source]rtc.induct}. |
69 let us look at the induction rule @{thm[source]rtc.induct}: |
70 In the above application of @{text erule}, the first premise of |
70 \[ \frac{(x,y) \in r^* \qquad \bigwedge x.~P~x~x \quad \dots}{P~x~y} \] |
71 @{thm[source]rtc.induct} is unified with the first suitable assumption, which |
71 When applying this rule, $x$ becomes @{term x}, $y$ becomes |
72 is @{term"(x,y) \<in> r*"} rather than @{term"(y,z) \<in> r*"}. Although that |
72 @{term y} and $P~x~y$ becomes @{prop"(x,z) : r*"}, thus |
73 is what we want, it is merely due to the order in which the assumptions occur |
|
74 in the subgoal, which it is not good practice to rely on. As a result, |
|
75 @{text"?xb"} becomes @{term x}, @{text"?xa"} becomes |
|
76 @{term y} and @{text"?P"} becomes @{term"%u v. (u,z) : r*"}, thus |
73 yielding the above subgoal. So what went wrong? |
77 yielding the above subgoal. So what went wrong? |
74 |
78 |
75 When looking at the instantiation of $P~x~y$ we see |
79 When looking at the instantiation of @{text"?P"} we see that it does not |
76 that $P$ does not depend on its second parameter at |
80 depend on its second parameter at all. The reason is that in our original |
77 all. The reason is that in our original goal, of the pair @{term"(x,y)"} only |
81 goal, of the pair @{term"(x,y)"} only @{term x} appears also in the |
78 @{term x} appears also in the conclusion, but not @{term y}. Thus our |
82 conclusion, but not @{term y}. Thus our induction statement is too |
79 induction statement is too weak. Fortunately, it can easily be strengthened: |
83 weak. Fortunately, it can easily be strengthened: |
80 transfer the additional premise @{prop"(y,z):r*"} into the conclusion:*} |
84 transfer the additional premise @{prop"(y,z):r*"} into the conclusion:*} |
81 (*<*)oops(*>*) |
85 (*<*)oops(*>*) |
82 lemma rtc_trans[rule_format]: |
86 lemma rtc_trans[rule_format]: |
83 "(x,y) \<in> r* \<Longrightarrow> (y,z) \<in> r* \<longrightarrow> (x,z) \<in> r*" |
87 "(x,y) \<in> r* \<Longrightarrow> (y,z) \<in> r* \<longrightarrow> (x,z) \<in> r*" |
84 |
88 |
143 transitivity. As a consequence, @{thm[source]rtc.induct} is simpler than |
147 transitivity. As a consequence, @{thm[source]rtc.induct} is simpler than |
144 @{thm[source]rtc2.induct}. Since inductive proofs are hard enough, we should |
148 @{thm[source]rtc2.induct}. Since inductive proofs are hard enough, we should |
145 certainly pick the simplest induction schema available for any concept. |
149 certainly pick the simplest induction schema available for any concept. |
146 Hence @{term rtc} is the definition of choice. |
150 Hence @{term rtc} is the definition of choice. |
147 |
151 |
148 \begin{exercise} |
152 \begin{exercise}\label{ex:converse-rtc-step} |
149 Show that the converse of @{thm[source]rtc_step} also holds: |
153 Show that the converse of @{thm[source]rtc_step} also holds: |
150 @{prop[display]"[| (x,y) : r*; (y,z) : r |] ==> (x,z) : r*"} |
154 @{prop[display]"[| (x,y) : r*; (y,z) : r |] ==> (x,z) : r*"} |
|
155 \end{exercise} |
|
156 \begin{exercise} |
|
157 Repeat the development of this section, but starting with a definition of |
|
158 @{term rtc} where @{thm[source]rtc_step} is replaced by its converse as shown |
|
159 in exercise~\ref{ex:converse-rtc-step}. |
151 \end{exercise} |
160 \end{exercise} |
152 *} |
161 *} |
153 (*<*) |
162 (*<*) |
154 lemma rtc_step2[rule_format]: "(x,y) : r* \<Longrightarrow> (y,z) : r --> (x,z) : r*" |
163 lemma rtc_step2[rule_format]: "(x,y) : r* \<Longrightarrow> (y,z) : r --> (x,z) : r*" |
155 apply(erule rtc.induct); |
164 apply(erule rtc.induct); |