
1 (*<*)theory Star imports Main begin(*>*) 

2 

3 section{*The Reflexive Transitive Closure*} 

4 

5 text{*\label{sec:rtc} 

6 \index{reflexive transitive closure!defining inductively(}% 

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 

12 introduced in \S\ref{sec:Relations}, where the operator @{text"\<^sup>*"} was 

13 defined as a least fixed point because inductive definitions were not yet 

14 available. But now they are: 

15 *} 

16 

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*" 

23 

24 text{*\noindent 

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

26 @{text"rtc r"} we can write @{term"r*"}. The actual definition 

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

28 @{text iff} attribute to increase automation. The 

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 

31 introduction rule, this is dangerous: the recursion in the second premise 

32 slows down and may even kill the automatic tactics. 

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: 

36 for a start, it does not even mention transitivity. 

37 The rest of this section is devoted to proving that it is equivalent to 

38 the standard definition. We start with a simple lemma: 

39 *} 

40 

41 lemma [intro]: "(x,y) \<in> r \<Longrightarrow> (x,y) \<in> r*" 

42 by(blast intro: rtc_step); 

43 

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 

50 shows that @{text blast} is able to handle @{thm[source]rtc_step}. But 

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 

54 To prove transitivity, we need rule induction, i.e.\ theorem 

55 @{thm[source]rtc.induct}: 

56 @{thm[display]rtc.induct} 

57 It says that @{text"?P"} holds for an arbitrary pair @{thm (prem 1) rtc.induct} 

58 if @{text"?P"} is preserved by all rules of the inductive definition, 

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: 

64 *} 

65 

66 lemma rtc_trans: "\<lbrakk> (x,y) \<in> r*; (y,z) \<in> r* \<rbrakk> \<Longrightarrow> (x,z) \<in> r*" 

67 apply(erule rtc.induct) 

68 

69 txt{*\noindent 

70 Unfortunately, even the base case is a problem: 

71 @{subgoals[display,indent=0,goals_limit=1]} 

72 We have to abandon this proof attempt. 

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 

81 yielding the above subgoal. So what went wrong? 

82 

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 

87 general. Fortunately, it can easily be specialized: 

88 transfer the additional premise @{prop"(y,z):r*"} into the conclusion:*} 

89 (*<*)oops(*>*) 

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 

96 When proving a statement by rule induction on $(x@1,\dots,x@n) \in R$, 

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 

102 @{text"\<longrightarrow>"} back into @{text"\<Longrightarrow>"}: in the end we obtain the original 

103 statement of our lemma. 

104 *} 

105 

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 

113 apply(blast); 

114 apply(blast intro: rtc_step); 

115 done 

116 

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

122 

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" 

130 

131 text{*\noindent 

132 and the equivalence of the two definitions is easily shown by the obvious rule 

133 inductions: 

134 *} 

135 

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

137 apply(erule rtc2.induct); 

138 apply(blast); 

139 apply(blast); 

140 apply(blast intro: rtc_trans); 

141 done 

142 

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

144 apply(erule rtc.induct); 

145 apply(blast intro: rtc2.intros); 

146 apply(blast intro: rtc2.intros); 

147 done 

148 

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 

153 @{thm[source]rtc2.induct}. Since inductive proofs are hard enough 

154 anyway, we should always pick the simplest induction schema available. 

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

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

157 

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

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} 

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} 

167 *} 

168 (*<*) 

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

170 apply(erule rtc.induct); 

171 apply blast; 

172 apply(blast intro: rtc_step) 

173 done 

174 

175 end 

176 (*>*) 