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

69517

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

10242

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

69517

26 
\<open>rtc r\<close> we can write @{term"r*"}. The actual definition

10520

27 
consists of two rules. Reflexivity is obvious and is immediately given the

69517

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


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:

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


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

69517

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}

69517

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}.

69517

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


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


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,

69517

78 
\<open>?xb\<close> becomes @{term x}, \<open>?xa\<close> becomes


79 
@{term y} and \<open>?P\<close> becomes @{term"\<lambda>u v. (u,z) \<in> r*"}, thus

10242

80 
yielding the above subgoal. So what went wrong?


81 

69517

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


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


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

27172

86 
general. Fortunately, it can easily be specialized:

67613

87 
transfer the additional premise @{prop"(y,z)\<in>r*"} 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

69517

100 
\S\ref{sec:indvarinprems}. 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>

10242

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


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


119 
relation containing @{term r}. 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.

10242

154 
Hence @{term rtc} is the definition of choice.

11494

155 
\index{reflexive transitive closure!defining inductively)}

10242

156 

10520

157 
\begin{exercise}\label{ex:conversertcstep}

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


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


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


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 
(*>*)
