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

src/HOL/Library/Transitive_Closure_Table.thy

author | blanchet |

Wed Sep 24 15:45:55 2014 +0200 (2014-09-24) | |

changeset 58425 | 246985c6b20b |

parent 56922 | d411a81b8356 |

child 58881 | b9556a055632 |

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

simpler proof

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

3 header {* A table-based implementation of the reflexive transitive closure *}

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 = (\<exists>xs. rtrancl_path r x xs y)"

16 proof

17 assume "r\<^sup>*\<^sup>* x y"

18 then show "\<exists>xs. rtrancl_path r x xs y"

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 `\<exists>xs. rtrancl_path r z xs y`

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

27 with `r x z` have "rtrancl_path r x (z # xs) y"

28 by (rule rtrancl_path.step)

29 then show ?case ..

30 qed

31 next

32 assume "\<exists>xs. rtrancl_path r x xs y"

33 then obtain xs where "rtrancl_path r x xs y" ..

34 then show "r\<^sup>*\<^sup>* x y"

35 proof induct

36 case (base x)

37 show ?case by (rule rtranclp.rtrancl_refl)

38 next

39 case (step x y ys z)

40 from `r x y` `r\<^sup>*\<^sup>* y z` show ?case

41 by (rule converse_rtranclp_into_rtranclp)

42 qed

43 qed

45 lemma rtrancl_path_trans:

46 assumes xy: "rtrancl_path r x xs y"

47 and yz: "rtrancl_path r y ys z"

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

49 proof (induct arbitrary: z)

50 case (base x)

51 then show ?case by simp

52 next

53 case (step x y xs)

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

55 by simp

56 with `r x y` have "rtrancl_path r x (y # (xs @ ys)) z"

57 by (rule rtrancl_path.step)

58 then show ?case by simp

59 qed

61 lemma rtrancl_path_appendE:

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

63 obtains "rtrancl_path r x (xs @ [y]) y" and "rtrancl_path r y ys z" using xz

64 proof (induct xs arbitrary: x)

65 case Nil

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

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

68 by cases auto

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

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

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

72 then show ?thesis using yz by (rule Nil)

73 next

74 case (Cons a as)

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

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

77 by cases auto

78 show ?thesis

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

80 assume "rtrancl_path r y ys z"

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

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

83 by (rule rtrancl_path.step)

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

85 by simp

86 then show ?thesis using `rtrancl_path r y ys z`

87 by (rule Cons(2))

88 qed

89 qed

91 lemma rtrancl_path_distinct:

92 assumes xy: "rtrancl_path r x xs y"

93 obtains xs' where "rtrancl_path r x xs' y" and "distinct (x # xs')" using xy

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

95 case (less xs)

96 show ?case

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

98 case True

99 with `rtrancl_path r x xs y` show ?thesis by (rule less)

100 next

101 case False

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

103 by (rule not_distinct_decomp)

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

105 by iprover

106 show ?thesis

107 proof (cases as)

108 case Nil

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

110 by auto

111 from x xs `rtrancl_path r x xs y` have cs: "rtrancl_path r x cs y"

112 by (auto elim: rtrancl_path_appendE)

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

114 then show ?thesis

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

116 next

117 case (Cons d ds)

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

119 by auto

120 with `rtrancl_path r x xs y` obtain xa: "rtrancl_path r x (ds @ [a]) a"

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

122 by (auto elim: rtrancl_path_appendE)

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

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

125 by (rule rtrancl_path_trans)

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

127 then show ?thesis

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

129 qed

130 qed

131 qed

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

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

135 where

136 base: "rtrancl_tab r xs x x"

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

139 lemma rtrancl_path_imp_rtrancl_tab:

140 assumes path: "rtrancl_path r x xs y"

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

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

143 shows "rtrancl_tab r ys x y" using path x ys

144 proof (induct arbitrary: ys)

145 case base

146 show ?case by (rule rtrancl_tab.base)

147 next

148 case (step x y zs z)

149 then have "x \<notin> set ys" by auto

150 from step have "distinct (y # zs)" by simp

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

152 by auto

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

154 by (rule step)

155 with `x \<notin> set ys` `r x y`

156 show ?case by (rule rtrancl_tab.step)

157 qed

159 lemma rtrancl_tab_imp_rtrancl_path:

160 assumes tab: "rtrancl_tab r ys x y"

161 obtains xs where "rtrancl_path r x xs y" using tab

162 proof induct

163 case base

164 from rtrancl_path.base show ?case by (rule base)

165 next

166 case step show ?case by (iprover intro: step rtrancl_path.step)

167 qed

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

170 proof

171 assume "r\<^sup>*\<^sup>* x y"

172 then obtain xs where "rtrancl_path r x xs y"

173 by (auto simp add: rtranclp_eq_rtrancl_path)

174 then obtain xs' where xs': "rtrancl_path r x xs' y"

175 and distinct: "distinct (x # xs')"

176 by (rule rtrancl_path_distinct)

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

178 with xs' distinct show "rtrancl_tab r [] x y"

179 by (rule rtrancl_path_imp_rtrancl_tab)

180 next

181 assume "rtrancl_tab r [] x y"

182 then obtain xs where "rtrancl_path r x xs y"

183 by (rule rtrancl_tab_imp_rtrancl_path)

184 then show "r\<^sup>*\<^sup>* x y"

185 by (auto simp add: rtranclp_eq_rtrancl_path)

186 qed

188 declare rtranclp_rtrancl_eq[code del]

189 declare rtranclp_eq_rtrancl_tab_nil[THEN iffD2, code_pred_intro]

191 code_pred rtranclp using rtranclp_eq_rtrancl_tab_nil [THEN iffD1] by fastforce

193 end