author  wenzelm 
Sat, 01 Nov 2014 14:20:38 +0100  
changeset 58860  fee7cfa69c50 
parent 48985  5386df44a037 
child 67406  23307fd33906 
permissions  rwrr 
17914  1 
(*<*)theory Star imports Main begin(*>*) 
10225  2 

10898  3 
section{*The Reflexive Transitive Closure*} 
10225  4 

10242  5 
text{*\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 

11147  12 
introduced in \S\ref{sec:Relations}, where the operator @{text"\<^sup>*"} was 
10520  13 
defined as a least fixed point because inductive definitions were not yet 
14 
available. But now they are: 

10225  15 
*} 
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 

24 
text{*\noindent 

25 
The function @{term rtc} is annotated with concrete syntax: instead of 

11494  26 
@{text"rtc r"} we can write @{term"r*"}. The actual definition 
10520  27 
consists of two rules. Reflexivity is obvious and is immediately given the 
28 
@{text iff} attribute to increase automation. The 

10363  29 
second rule, @{thm[source]rtc_step}, says that we can always add one more 
30 
@{term r}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: 
10242  39 
*} 
10225  40 

11308  41 
lemma [intro]: "(x,y) \<in> r \<Longrightarrow> (x,y) \<in> r*" 
58860  42 
by(blast intro: rtc_step) 
10225  43 

10242  44 
text{*\noindent 
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 @{term"r*"} occurs only in 

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 

10898  50 
shows that @{text blast} is able to handle @{thm[source]rtc_step}. But 
10242  51 
some of the other automatic tactics are more sensitive, and even @{text 
52 
blast} can be lead astray in the presence of large numbers of rules. 

53 

10520  54 
To prove transitivity, we need rule induction, i.e.\ theorem 
55 
@{thm[source]rtc.induct}: 

56 
@{thm[display]rtc.induct} 

32891  57 
It says that @{text"?P"} holds for an arbitrary pair @{thm (prem 1) rtc.induct} 
23847
32d76edc5e5c
Refer to major premise of induction rule via "thm_style prem1".
berghofe
parents:
23733
diff
changeset

58 
if @{text"?P"} is preserved by all rules of the inductive definition, 
10520  59 
i.e.\ if @{text"?P"} holds for the conclusion provided it holds for the 
60 
premises. In general, rule induction for an $n$ary inductive relation $R$ 

61 
expects a premise of the form $(x@1,\dots,x@n) \in R$. 

62 

63 
Now we turn to the inductive proof of transitivity: 

10242  64 
*} 
65 

10520  66 
lemma rtc_trans: "\<lbrakk> (x,y) \<in> r*; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*" 
10363  67 
apply(erule rtc.induct) 
68 

69 
txt{*\noindent 

11494  70 
Unfortunately, even the base case is a problem: 
10363  71 
@{subgoals[display,indent=0,goals_limit=1]} 
11494  72 
We have to abandon this proof attempt. 
10520  73 
To understand what is going on, let us look again at @{thm[source]rtc.induct}. 
74 
In the above application of @{text erule}, the first premise of 

75 
@{thm[source]rtc.induct} is unified with the first suitable assumption, which 

76 
is @{term"(x,y) \<in> r*"} rather than @{term"(y,z) \<in> r*"}. Although that 

77 
is what we want, it is merely due to the order in which the assumptions occur 

78 
in the subgoal, which it is not good practice to rely on. As a result, 

79 
@{text"?xb"} becomes @{term x}, @{text"?xa"} becomes 

80 
@{term y} and @{text"?P"} becomes @{term"%u v. (u,z) : r*"}, thus 

10242  81 
yielding the above subgoal. So what went wrong? 
82 

10520  83 
When looking at the instantiation of @{text"?P"} we see that it does not 
84 
depend on its second parameter at all. The reason is that in our original 

85 
goal, of the pair @{term"(x,y)"} only @{term x} appears also in the 

86 
conclusion, but not @{term y}. Thus our induction statement is too 

27172  87 
general. Fortunately, it can easily be specialized: 
10363  88 
transfer the additional premise @{prop"(y,z):r*"} into the conclusion:*} 
89 
(*<*)oops(*>*) 

10242  90 
lemma rtc_trans[rule_format]: 
91 
"(x,y) \<in> r* \<Longrightarrow> (y,z) \<in> r* \<longrightarrow> (x,z) \<in> r*" 

92 

93 
txt{*\noindent 

94 
This is not an obscure trick but a generally applicable heuristic: 

95 
\begin{quote}\em 

11257  96 
When proving a statement by rule induction on $(x@1,\dots,x@n) \in R$, 
10242  97 
pull all other premises containing any of the $x@i$ into the conclusion 
98 
using $\longrightarrow$. 

99 
\end{quote} 

100 
A similar heuristic for other kinds of inductions is formulated in 

101 
\S\ref{sec:indvarinprems}. The @{text rule_format} directive turns 

11147  102 
@{text"\<longrightarrow>"} back into @{text"\<Longrightarrow>"}: in the end we obtain the original 
10242  103 
statement of our lemma. 
104 
*} 

105 

10363  106 
apply(erule rtc.induct) 
107 

108 
txt{*\noindent 

109 
Now induction produces two subgoals which are both proved automatically: 

110 
@{subgoals[display,indent=0]} 

111 
*} 

112 

58860  113 
apply(blast) 
114 
apply(blast intro: rtc_step) 

10225  115 
done 
116 

10242  117 
text{* 
118 
Let us now prove that @{term"r*"} is really the reflexive transitive closure 

119 
of @{term r}, i.e.\ the least reflexive and transitive 

120 
relation containing @{term r}. The latter is easily formalized 

121 
*} 

10225  122 

23733  123 
inductive_set 
124 
rtc2 :: "('a \<times> 'a)set \<Rightarrow> ('a \<times> 'a)set" 

125 
for r :: "('a \<times> 'a)set" 

126 
where 

127 
"(x,y) \<in> r \<Longrightarrow> (x,y) \<in> rtc2 r" 

128 
 "(x,x) \<in> rtc2 r" 

129 
 "\<lbrakk> (x,y) \<in> rtc2 r; (y,z) \<in> rtc2 r \<rbrakk> \<Longrightarrow> (x,z) \<in> rtc2 r" 

10225  130 

10242  131 
text{*\noindent 
132 
and the equivalence of the two definitions is easily shown by the obvious rule 

10237  133 
inductions: 
134 
*} 

10225  135 

10237  136 
lemma "(x,y) \<in> rtc2 r \<Longrightarrow> (x,y) \<in> r*" 
58860  137 
apply(erule rtc2.induct) 
138 
apply(blast) 

139 
apply(blast) 

140 
apply(blast intro: rtc_trans) 

10237  141 
done 
142 

143 
lemma "(x,y) \<in> r* \<Longrightarrow> (x,y) \<in> rtc2 r" 

58860  144 
apply(erule rtc.induct) 
145 
apply(blast intro: rtc2.intros) 

146 
apply(blast intro: rtc2.intros) 

10225  147 
done 
148 

10242  149 
text{* 
150 
So why did we start with the first definition? Because it is simpler. It 

151 
contains only two rules, and the single step rule is simpler than 

152 
transitivity. As a consequence, @{thm[source]rtc.induct} is simpler than 

10898  153 
@{thm[source]rtc2.induct}. Since inductive proofs are hard enough 
11147  154 
anyway, we should always pick the simplest induction schema available. 
10242  155 
Hence @{term rtc} is the definition of choice. 
11494  156 
\index{reflexive transitive closure!defining inductively)} 
10242  157 

10520  158 
\begin{exercise}\label{ex:conversertcstep} 
10242  159 
Show that the converse of @{thm[source]rtc_step} also holds: 
160 
@{prop[display]"[ (x,y) : r*; (y,z) : r ] ==> (x,z) : r*"} 

161 
\end{exercise} 

10520  162 
\begin{exercise} 
163 
Repeat the development of this section, but starting with a definition of 

164 
@{term rtc} where @{thm[source]rtc_step} is replaced by its converse as shown 

165 
in exercise~\ref{ex:conversertcstep}. 

166 
\end{exercise} 

10242  167 
*} 
168 
(*<*) 

169 
lemma rtc_step2[rule_format]: "(x,y) : r* \<Longrightarrow> (y,z) : r > (x,z) : r*" 

58860  170 
apply(erule rtc.induct) 
171 
apply blast 

12815  172 
apply(blast intro: rtc_step) 
10242  173 
done 
174 

175 
end 

176 
(*>*) 