wenzelm@60519

1 
(* Author: Stefan Berghofer, Lukas Bulwahn, TU Muenchen *)

bulwahn@33649

2 

wenzelm@60500

3 
section \<open>A tablebased implementation of the reflexive transitive closure\<close>

bulwahn@33649

4 

bulwahn@33649

5 
theory Transitive_Closure_Table

bulwahn@33649

6 
imports Main

bulwahn@33649

7 
begin

bulwahn@33649

8 

bulwahn@33649

9 
inductive rtrancl_path :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool"

bulwahn@33649

10 
for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"

bulwahn@33649

11 
where

bulwahn@33649

12 
base: "rtrancl_path r x [] x"

bulwahn@33649

13 
 step: "r x y \<Longrightarrow> rtrancl_path r y ys z \<Longrightarrow> rtrancl_path r x (y # ys) z"

bulwahn@33649

14 

wenzelm@60519

15 
lemma rtranclp_eq_rtrancl_path: "r\<^sup>*\<^sup>* x y \<longleftrightarrow> (\<exists>xs. rtrancl_path r x xs y)"

bulwahn@33649

16 
proof

wenzelm@60519

17 
show "\<exists>xs. rtrancl_path r x xs y" if "r\<^sup>*\<^sup>* x y"

wenzelm@60519

18 
using that

bulwahn@33649

19 
proof (induct rule: converse_rtranclp_induct)

berghofe@34912

20 
case base

bulwahn@33649

21 
have "rtrancl_path r y [] y" by (rule rtrancl_path.base)

bulwahn@33649

22 
then show ?case ..

bulwahn@33649

23 
next

berghofe@34912

24 
case (step x z)

wenzelm@60500

25 
from \<open>\<exists>xs. rtrancl_path r z xs y\<close>

bulwahn@33649

26 
obtain xs where "rtrancl_path r z xs y" ..

wenzelm@60500

27 
with \<open>r x z\<close> have "rtrancl_path r x (z # xs) y"

bulwahn@33649

28 
by (rule rtrancl_path.step)

bulwahn@33649

29 
then show ?case ..

bulwahn@33649

30 
qed

wenzelm@60519

31 
show "r\<^sup>*\<^sup>* x y" if "\<exists>xs. rtrancl_path r x xs y"

wenzelm@60519

32 
proof 

wenzelm@60519

33 
from that obtain xs where "rtrancl_path r x xs y" ..

wenzelm@60519

34 
then show ?thesis

wenzelm@60519

35 
proof induct

wenzelm@60519

36 
case (base x)

wenzelm@60519

37 
show ?case

wenzelm@60519

38 
by (rule rtranclp.rtrancl_refl)

wenzelm@60519

39 
next

wenzelm@60519

40 
case (step x y ys z)

wenzelm@60519

41 
from \<open>r x y\<close> \<open>r\<^sup>*\<^sup>* y z\<close> show ?case

wenzelm@60519

42 
by (rule converse_rtranclp_into_rtranclp)

wenzelm@60519

43 
qed

bulwahn@33649

44 
qed

bulwahn@33649

45 
qed

bulwahn@33649

46 

bulwahn@33649

47 
lemma rtrancl_path_trans:

bulwahn@33649

48 
assumes xy: "rtrancl_path r x xs y"

wenzelm@60519

49 
and yz: "rtrancl_path r y ys z"

bulwahn@33649

50 
shows "rtrancl_path r x (xs @ ys) z" using xy yz

bulwahn@33649

51 
proof (induct arbitrary: z)

bulwahn@33649

52 
case (base x)

bulwahn@33649

53 
then show ?case by simp

bulwahn@33649

54 
next

bulwahn@33649

55 
case (step x y xs)

bulwahn@33649

56 
then have "rtrancl_path r y (xs @ ys) z"

bulwahn@33649

57 
by simp

wenzelm@60500

58 
with \<open>r x y\<close> have "rtrancl_path r x (y # (xs @ ys)) z"

bulwahn@33649

59 
by (rule rtrancl_path.step)

bulwahn@33649

60 
then show ?case by simp

bulwahn@33649

61 
qed

bulwahn@33649

62 

bulwahn@33649

63 
lemma rtrancl_path_appendE:

bulwahn@33649

64 
assumes xz: "rtrancl_path r x (xs @ y # ys) z"

wenzelm@60519

65 
obtains "rtrancl_path r x (xs @ [y]) y" and "rtrancl_path r y ys z"

wenzelm@60519

66 
using xz

bulwahn@33649

67 
proof (induct xs arbitrary: x)

bulwahn@33649

68 
case Nil

bulwahn@33649

69 
then have "rtrancl_path r x (y # ys) z" by simp

bulwahn@33649

70 
then obtain xy: "r x y" and yz: "rtrancl_path r y ys z"

bulwahn@33649

71 
by cases auto

bulwahn@33649

72 
from xy have "rtrancl_path r x [y] y"

bulwahn@33649

73 
by (rule rtrancl_path.step [OF _ rtrancl_path.base])

bulwahn@33649

74 
then have "rtrancl_path r x ([] @ [y]) y" by simp

wenzelm@60519

75 
then show thesis using yz by (rule Nil)

bulwahn@33649

76 
next

bulwahn@33649

77 
case (Cons a as)

bulwahn@33649

78 
then have "rtrancl_path r x (a # (as @ y # ys)) z" by simp

bulwahn@33649

79 
then obtain xa: "r x a" and az: "rtrancl_path r a (as @ y # ys) z"

bulwahn@33649

80 
by cases auto

wenzelm@60519

81 
show thesis

bulwahn@33649

82 
proof (rule Cons(1) [OF _ az])

bulwahn@33649

83 
assume "rtrancl_path r y ys z"

bulwahn@33649

84 
assume "rtrancl_path r a (as @ [y]) y"

bulwahn@33649

85 
with xa have "rtrancl_path r x (a # (as @ [y])) y"

bulwahn@33649

86 
by (rule rtrancl_path.step)

bulwahn@33649

87 
then have "rtrancl_path r x ((a # as) @ [y]) y"

bulwahn@33649

88 
by simp

wenzelm@60519

89 
then show thesis using \<open>rtrancl_path r y ys z\<close>

bulwahn@33649

90 
by (rule Cons(2))

bulwahn@33649

91 
qed

bulwahn@33649

92 
qed

bulwahn@33649

93 

bulwahn@33649

94 
lemma rtrancl_path_distinct:

bulwahn@33649

95 
assumes xy: "rtrancl_path r x xs y"

Andreas@61764

96 
obtains xs' where "rtrancl_path r x xs' y" and "distinct (x # xs')" and "set xs' \<subseteq> set xs"

wenzelm@60519

97 
using xy

bulwahn@33649

98 
proof (induct xs rule: measure_induct_rule [of length])

bulwahn@33649

99 
case (less xs)

bulwahn@33649

100 
show ?case

bulwahn@33649

101 
proof (cases "distinct (x # xs)")

bulwahn@33649

102 
case True

Andreas@61764

103 
with \<open>rtrancl_path r x xs y\<close> show ?thesis by (rule less) simp

bulwahn@33649

104 
next

bulwahn@33649

105 
case False

bulwahn@33649

106 
then have "\<exists>as bs cs a. x # xs = as @ [a] @ bs @ [a] @ cs"

bulwahn@33649

107 
by (rule not_distinct_decomp)

bulwahn@33649

108 
then obtain as bs cs a where xxs: "x # xs = as @ [a] @ bs @ [a] @ cs"

bulwahn@33649

109 
by iprover

bulwahn@33649

110 
show ?thesis

bulwahn@33649

111 
proof (cases as)

bulwahn@33649

112 
case Nil

bulwahn@33649

113 
with xxs have x: "x = a" and xs: "xs = bs @ a # cs"

wenzelm@35423

114 
by auto

Andreas@61764

115 
from x xs \<open>rtrancl_path r x xs y\<close> have cs: "rtrancl_path r x cs y" "set cs \<subseteq> set xs"

wenzelm@35423

116 
by (auto elim: rtrancl_path_appendE)

bulwahn@33649

117 
from xs have "length cs < length xs" by simp

bulwahn@33649

118 
then show ?thesis

Andreas@61764

119 
by (rule less(1))(blast intro: cs less(2) order_trans del: subsetI)+

bulwahn@33649

120 
next

bulwahn@33649

121 
case (Cons d ds)

bulwahn@33649

122 
with xxs have xs: "xs = ds @ a # (bs @ [a] @ cs)"

wenzelm@35423

123 
by auto

wenzelm@60500

124 
with \<open>rtrancl_path r x xs y\<close> obtain xa: "rtrancl_path r x (ds @ [a]) a"

bulwahn@33649

125 
and ay: "rtrancl_path r a (bs @ a # cs) y"

wenzelm@35423

126 
by (auto elim: rtrancl_path_appendE)

bulwahn@33649

127 
from ay have "rtrancl_path r a cs y" by (auto elim: rtrancl_path_appendE)

bulwahn@33649

128 
with xa have xy: "rtrancl_path r x ((ds @ [a]) @ cs) y"

wenzelm@35423

129 
by (rule rtrancl_path_trans)

Andreas@61764

130 
from xs have set: "set ((ds @ [a]) @ cs) \<subseteq> set xs" by auto

bulwahn@33649

131 
from xs have "length ((ds @ [a]) @ cs) < length xs" by simp

bulwahn@33649

132 
then show ?thesis

Andreas@61764

133 
by (rule less(1))(blast intro: xy less(2) set[THEN subsetD])+

bulwahn@33649

134 
qed

bulwahn@33649

135 
qed

bulwahn@33649

136 
qed

bulwahn@33649

137 

bulwahn@33649

138 
inductive rtrancl_tab :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"

bulwahn@33649

139 
for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"

bulwahn@33649

140 
where

bulwahn@33649

141 
base: "rtrancl_tab r xs x x"

bulwahn@33649

142 
 step: "x \<notin> set xs \<Longrightarrow> r x y \<Longrightarrow> rtrancl_tab r (x # xs) y z \<Longrightarrow> rtrancl_tab r xs x z"

bulwahn@33649

143 

bulwahn@33649

144 
lemma rtrancl_path_imp_rtrancl_tab:

bulwahn@33649

145 
assumes path: "rtrancl_path r x xs y"

wenzelm@60519

146 
and x: "distinct (x # xs)"

wenzelm@60519

147 
and ys: "({x} \<union> set xs) \<inter> set ys = {}"

wenzelm@60519

148 
shows "rtrancl_tab r ys x y"

wenzelm@60519

149 
using path x ys

bulwahn@33649

150 
proof (induct arbitrary: ys)

bulwahn@33649

151 
case base

wenzelm@60519

152 
show ?case

wenzelm@60519

153 
by (rule rtrancl_tab.base)

bulwahn@33649

154 
next

bulwahn@33649

155 
case (step x y zs z)

wenzelm@60519

156 
then have "x \<notin> set ys"

wenzelm@60519

157 
by auto

wenzelm@60519

158 
from step have "distinct (y # zs)"

wenzelm@60519

159 
by simp

bulwahn@33649

160 
moreover from step have "({y} \<union> set zs) \<inter> set (x # ys) = {}"

bulwahn@33649

161 
by auto

bulwahn@33649

162 
ultimately have "rtrancl_tab r (x # ys) y z"

bulwahn@33649

163 
by (rule step)

wenzelm@60519

164 
with \<open>x \<notin> set ys\<close> \<open>r x y\<close> show ?case

wenzelm@60519

165 
by (rule rtrancl_tab.step)

bulwahn@33649

166 
qed

bulwahn@33649

167 

bulwahn@33649

168 
lemma rtrancl_tab_imp_rtrancl_path:

bulwahn@33649

169 
assumes tab: "rtrancl_tab r ys x y"

wenzelm@60519

170 
obtains xs where "rtrancl_path r x xs y"

wenzelm@60519

171 
using tab

bulwahn@33649

172 
proof induct

bulwahn@33649

173 
case base

wenzelm@60519

174 
from rtrancl_path.base show ?case

wenzelm@60519

175 
by (rule base)

bulwahn@33649

176 
next

wenzelm@60519

177 
case step

wenzelm@60519

178 
show ?case

wenzelm@60519

179 
by (iprover intro: step rtrancl_path.step)

bulwahn@33649

180 
qed

bulwahn@33649

181 

wenzelm@60519

182 
lemma rtranclp_eq_rtrancl_tab_nil: "r\<^sup>*\<^sup>* x y \<longleftrightarrow> rtrancl_tab r [] x y"

bulwahn@33649

183 
proof

wenzelm@60519

184 
show "rtrancl_tab r [] x y" if "r\<^sup>*\<^sup>* x y"

wenzelm@60519

185 
proof 

wenzelm@60519

186 
from that obtain xs where "rtrancl_path r x xs y"

wenzelm@60519

187 
by (auto simp add: rtranclp_eq_rtrancl_path)

wenzelm@60519

188 
then obtain xs' where xs': "rtrancl_path r x xs' y" and distinct: "distinct (x # xs')"

wenzelm@60519

189 
by (rule rtrancl_path_distinct)

wenzelm@60519

190 
have "({x} \<union> set xs') \<inter> set [] = {}"

wenzelm@60519

191 
by simp

wenzelm@60519

192 
with xs' distinct show ?thesis

wenzelm@60519

193 
by (rule rtrancl_path_imp_rtrancl_tab)

wenzelm@60519

194 
qed

wenzelm@60519

195 
show "r\<^sup>*\<^sup>* x y" if "rtrancl_tab r [] x y"

wenzelm@60519

196 
proof 

wenzelm@60519

197 
from that obtain xs where "rtrancl_path r x xs y"

wenzelm@60519

198 
by (rule rtrancl_tab_imp_rtrancl_path)

wenzelm@60519

199 
then show ?thesis

wenzelm@60519

200 
by (auto simp add: rtranclp_eq_rtrancl_path)

wenzelm@60519

201 
qed

bulwahn@33649

202 
qed

bulwahn@33649

203 

wenzelm@60519

204 
declare rtranclp_rtrancl_eq [code del]

wenzelm@60519

205 
declare rtranclp_eq_rtrancl_tab_nil [THEN iffD2, code_pred_intro]

bulwahn@33649

206 

wenzelm@60519

207 
code_pred rtranclp

wenzelm@60519

208 
using rtranclp_eq_rtrancl_tab_nil [THEN iffD1] by fastforce

bulwahn@33649

209 

Andreas@61765

210 
lemma rtrancl_path_Range: "\<lbrakk> rtrancl_path R x xs y; z \<in> set xs \<rbrakk> \<Longrightarrow> RangeP R z"

Andreas@61765

211 
by(induction rule: rtrancl_path.induct) auto

Andreas@61765

212 

Andreas@61765

213 
lemma rtrancl_path_Range_end: "\<lbrakk> rtrancl_path R x xs y; xs \<noteq> [] \<rbrakk> \<Longrightarrow> RangeP R y"

Andreas@61765

214 
by(induction rule: rtrancl_path.induct)(auto elim: rtrancl_path.cases)

Andreas@61765

215 

Andreas@61765

216 
lemma rtrancl_path_nth:

Andreas@61765

217 
"\<lbrakk> rtrancl_path R x xs y; i < length xs \<rbrakk> \<Longrightarrow> R ((x # xs) ! i) (xs ! i)"

Andreas@61765

218 
proof(induction arbitrary: i rule: rtrancl_path.induct)

Andreas@61765

219 
case step thus ?case by(cases i) simp_all

Andreas@61765

220 
qed simp

Andreas@61765

221 

Andreas@61765

222 
lemma rtrancl_path_last: "\<lbrakk> rtrancl_path R x xs y; xs \<noteq> [] \<rbrakk> \<Longrightarrow> last xs = y"

Andreas@61765

223 
by(induction rule: rtrancl_path.induct)(auto elim: rtrancl_path.cases)

Andreas@61765

224 

Andreas@61765

225 
lemma rtrancl_path_mono:

Andreas@61765

226 
"\<lbrakk> rtrancl_path R x p y; \<And>x y. R x y \<Longrightarrow> S x y \<rbrakk> \<Longrightarrow> rtrancl_path S x p y"

Andreas@61765

227 
by(induction rule: rtrancl_path.induct)(auto intro: rtrancl_path.intros)

Andreas@61765

228 

bulwahn@46359

229 
end 