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