src/HOL/Library/Transitive_Closure_Table.thy
 author hoelzl Tue Jul 19 14:37:49 2011 +0200 (2011-07-19) changeset 43922 c6f35921056e parent 37589 9c33d02656bc child 43973 a907e541b127 permissions -rw-r--r--
add nat => enat coercion
1 (* Author: Stefan Berghofer, Lukas Bulwahn, TU Muenchen *)
3 header {* A tabled 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_eq_rtrancl_tab_nil [code_unfold, code_inline del]
190 declare rtranclp_eq_rtrancl_tab_nil[THEN iffD2, code_pred_intro]
192 code_pred rtranclp using rtranclp_eq_rtrancl_tab_nil [THEN iffD1] by fastsimp
194 subsection {* A simple example *}
196 datatype ty = A | B | C
198 inductive test :: "ty \<Rightarrow> ty \<Rightarrow> bool"
199 where
200   "test A B"
201 | "test B A"
202 | "test B C"
204 subsubsection {* Invoking with the SML code generator *}
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"
213 ML "Test.test1"
214 ML "Test.test2"
215 ML "DSeq.list_of Test.test3"
216 ML "DSeq.list_of Test.test4"
218 subsubsection {* Invoking with the predicate compiler and the generic code generator *}
220 code_pred test .
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}"
227 value "test\<^sup>*\<^sup>* A C"
228 value "test\<^sup>*\<^sup>* C A"
230 hide_type ty
231 hide_const test A B C
233 end