|
1 (* Author: Stefan Berghofer, Lukas Bulwahn, TU Muenchen *) |
|
2 |
|
3 header {* A tabled implementation of the reflexive transitive closure *} |
|
4 |
|
5 theory Transitive_Closure_Table |
|
6 imports Main |
|
7 begin |
|
8 |
|
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" |
|
14 |
|
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 1 |
|
21 have "rtrancl_path r y [] y" by (rule rtrancl_path.base) |
|
22 then show ?case .. |
|
23 next |
|
24 case (2 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 |
|
44 |
|
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 |
|
60 |
|
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 |
|
90 |
|
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 |
|
132 |
|
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" |
|
138 |
|
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 |
|
158 |
|
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 |
|
168 |
|
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 |
|
187 |
|
188 declare rtranclp_eq_rtrancl_tab_nil [code_unfold] |
|
189 |
|
190 declare rtranclp_eq_rtrancl_tab_nil[THEN iffD2, code_pred_intro] |
|
191 |
|
192 code_pred rtranclp using rtranclp_eq_rtrancl_tab_nil[THEN iffD1] by fastsimp |
|
193 |
|
194 subsection {* A simple example *} |
|
195 |
|
196 datatype ty = A | B | C |
|
197 |
|
198 inductive test :: "ty \<Rightarrow> ty \<Rightarrow> bool" |
|
199 where |
|
200 "test A B" |
|
201 | "test B A" |
|
202 | "test B C" |
|
203 |
|
204 subsubsection {* Invoking with the SML code generator *} |
|
205 |
|
206 code_module Test |
|
207 contains |
|
208 test1 = "test\<^sup>*\<^sup>* A C" |
|
209 test2 = "test\<^sup>*\<^sup>* C A" |
|
210 test3 = "test\<^sup>*\<^sup>* A _" |
|
211 test4 = "test\<^sup>*\<^sup>* _ C" |
|
212 |
|
213 ML "Test.test1" |
|
214 ML "Test.test2" |
|
215 ML "DSeq.list_of Test.test3" |
|
216 ML "DSeq.list_of Test.test4" |
|
217 |
|
218 subsubsection {* Invoking with the predicate compiler and the generic code generator *} |
|
219 |
|
220 code_pred test . |
|
221 |
|
222 values "{x. test\<^sup>*\<^sup>* A C}" |
|
223 values "{x. test\<^sup>*\<^sup>* C A}" |
|
224 values "{x. test\<^sup>*\<^sup>* A x}" |
|
225 values "{x. test\<^sup>*\<^sup>* x C}" |
|
226 |
|
227 hide const test |
|
228 |
|
229 end |
|
230 |