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

src/HOL/Library/Transitive_Closure_Table.thy

author | paulson <lp15@cam.ac.uk> |

Mon Feb 22 14:37:56 2016 +0000 (2016-02-22) | |

changeset 62379 | 340738057c8c |

parent 61765 | 13ca8f4f6907 |

child 62390 | 842917225d56 |

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

An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!

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')" and "set xs' \<subseteq> set 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) simp

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" "set cs \<subseteq> set xs"

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))(blast intro: cs less(2) order_trans del: subsetI)+

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 set: "set ((ds @ [a]) @ cs) \<subseteq> set xs" by auto

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

132 then show ?thesis

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

134 qed

135 qed

136 qed

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

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

140 where

141 base: "rtrancl_tab r xs x x"

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"

144 lemma rtrancl_path_imp_rtrancl_tab:

145 assumes path: "rtrancl_path r x xs y"

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

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

148 shows "rtrancl_tab r ys x y"

149 using path x ys

150 proof (induct arbitrary: ys)

151 case base

152 show ?case

153 by (rule rtrancl_tab.base)

154 next

155 case (step x y zs z)

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

157 by auto

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

159 by simp

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

161 by auto

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

163 by (rule step)

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

165 by (rule rtrancl_tab.step)

166 qed

168 lemma rtrancl_tab_imp_rtrancl_path:

169 assumes tab: "rtrancl_tab r ys x y"

170 obtains xs where "rtrancl_path r x xs y"

171 using tab

172 proof induct

173 case base

174 from rtrancl_path.base show ?case

175 by (rule base)

176 next

177 case step

178 show ?case

179 by (iprover intro: step rtrancl_path.step)

180 qed

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

183 proof

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

185 proof -

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

187 by (auto simp add: rtranclp_eq_rtrancl_path)

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

189 by (rule rtrancl_path_distinct)

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

191 by simp

192 with xs' distinct show ?thesis

193 by (rule rtrancl_path_imp_rtrancl_tab)

194 qed

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

196 proof -

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

198 by (rule rtrancl_tab_imp_rtrancl_path)

199 then show ?thesis

200 by (auto simp add: rtranclp_eq_rtrancl_path)

201 qed

202 qed

204 declare rtranclp_rtrancl_eq [code del]

205 declare rtranclp_eq_rtrancl_tab_nil [THEN iffD2, code_pred_intro]

207 code_pred rtranclp

208 using rtranclp_eq_rtrancl_tab_nil [THEN iffD1] by fastforce

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

211 by(induction rule: rtrancl_path.induct) auto

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

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

216 lemma rtrancl_path_nth:

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

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

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

220 qed simp

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

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

225 lemma rtrancl_path_mono:

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"

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

229 end