summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Library/Transitive_Closure_Table.thy

author | wenzelm |

Fri Jun 19 18:41:21 2015 +0200 (2015-06-19) | |

changeset 60519 | 84b8e5c2580e |

parent 60500 | 903bb1495239 |

child 61764 | ac6e5de1a50b |

permissions | -rw-r--r-- |

tuned proofs;

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

3 section \<open>A table-based implementation of the reflexive transitive closure\<close>

5 theory Transitive_Closure_Table

6 imports Main

7 begin

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

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

11 where

12 base: "rtrancl_path r x [] x"

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

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

16 proof

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

18 using that

19 proof (induct rule: converse_rtranclp_induct)

20 case base

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

22 then show ?case ..

23 next

24 case (step x z)

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

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

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

28 by (rule rtrancl_path.step)

29 then show ?case ..

30 qed

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

32 proof -

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

34 then show ?thesis

35 proof induct

36 case (base x)

37 show ?case

38 by (rule rtranclp.rtrancl_refl)

39 next

40 case (step x y ys z)

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

42 by (rule converse_rtranclp_into_rtranclp)

43 qed

44 qed

45 qed

47 lemma rtrancl_path_trans:

48 assumes xy: "rtrancl_path r x xs y"

49 and yz: "rtrancl_path r y ys z"

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

51 proof (induct arbitrary: z)

52 case (base x)

53 then show ?case by simp

54 next

55 case (step x y xs)

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

57 by simp

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

59 by (rule rtrancl_path.step)

60 then show ?case by simp

61 qed

63 lemma rtrancl_path_appendE:

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

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

66 using xz

67 proof (induct xs arbitrary: x)

68 case Nil

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

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

71 by cases auto

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

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

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

75 then show thesis using yz by (rule Nil)

76 next

77 case (Cons a as)

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

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

80 by cases auto

81 show thesis

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

83 assume "rtrancl_path r y ys z"

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

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

86 by (rule rtrancl_path.step)

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

88 by simp

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

90 by (rule Cons(2))

91 qed

92 qed

94 lemma rtrancl_path_distinct:

95 assumes xy: "rtrancl_path r x xs y"

96 obtains xs' where "rtrancl_path r x xs' y" and "distinct (x # xs')"

97 using xy

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

99 case (less xs)

100 show ?case

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

102 case True

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

104 next

105 case False

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

107 by (rule not_distinct_decomp)

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

109 by iprover

110 show ?thesis

111 proof (cases as)

112 case Nil

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

114 by auto

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

116 by (auto elim: rtrancl_path_appendE)

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

118 then show ?thesis

119 by (rule less(1)) (iprover intro: cs less(2))+

120 next

121 case (Cons d ds)

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

123 by auto

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

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

126 by (auto elim: rtrancl_path_appendE)

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

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

129 by (rule rtrancl_path_trans)

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

131 then show ?thesis

132 by (rule less(1)) (iprover intro: xy less(2))+

133 qed

134 qed

135 qed

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

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

139 where

140 base: "rtrancl_tab r xs x x"

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

143 lemma rtrancl_path_imp_rtrancl_tab:

144 assumes path: "rtrancl_path r x xs y"

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

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

147 shows "rtrancl_tab r ys x y"

148 using path x ys

149 proof (induct arbitrary: ys)

150 case base

151 show ?case

152 by (rule rtrancl_tab.base)

153 next

154 case (step x y zs z)

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

156 by auto

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

158 by simp

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

160 by auto

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

162 by (rule step)

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

164 by (rule rtrancl_tab.step)

165 qed

167 lemma rtrancl_tab_imp_rtrancl_path:

168 assumes tab: "rtrancl_tab r ys x y"

169 obtains xs where "rtrancl_path r x xs y"

170 using tab

171 proof induct

172 case base

173 from rtrancl_path.base show ?case

174 by (rule base)

175 next

176 case step

177 show ?case

178 by (iprover intro: step rtrancl_path.step)

179 qed

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

182 proof

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

184 proof -

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

186 by (auto simp add: rtranclp_eq_rtrancl_path)

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

188 by (rule rtrancl_path_distinct)

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

190 by simp

191 with xs' distinct show ?thesis

192 by (rule rtrancl_path_imp_rtrancl_tab)

193 qed

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

195 proof -

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

197 by (rule rtrancl_tab_imp_rtrancl_path)

198 then show ?thesis

199 by (auto simp add: rtranclp_eq_rtrancl_path)

200 qed

201 qed

203 declare rtranclp_rtrancl_eq [code del]

204 declare rtranclp_eq_rtrancl_tab_nil [THEN iffD2, code_pred_intro]

206 code_pred rtranclp

207 using rtranclp_eq_rtrancl_tab_nil [THEN iffD1] by fastforce

209 end