1.1 --- a/CONTRIBUTORS Thu Nov 12 17:21:51 2009 +0100
1.2 +++ b/CONTRIBUTORS Thu Nov 12 20:38:57 2009 +0100
1.3 @@ -6,6 +6,10 @@
1.4
1.5 Contributions to this Isabelle version
1.6 --------------------------------------
1.7 +
1.8 +* November 2009: Stefan Berghofer, Lukas Bulwahn, TUM
1.9 + A tabled implementation of the reflexive transitive closure
1.10 +
1.11 * November 2009: Lukas Bulwahn, TUM
1.12 Predicate Compiler: a compiler for inductive predicates to equational specfications
1.13
2.1 --- a/NEWS Thu Nov 12 17:21:51 2009 +0100
2.2 +++ b/NEWS Thu Nov 12 20:38:57 2009 +0100
2.3 @@ -37,6 +37,8 @@
2.4
2.5 *** HOL ***
2.6
2.7 +* A tabled implementation of the reflexive transitive closure
2.8 +
2.9 * New commands "code_pred" and "values" to invoke the predicate compiler
2.10 and to enumerate values of inductive predicates.
2.11
3.1 --- a/src/HOL/IsaMakefile Thu Nov 12 17:21:51 2009 +0100
3.2 +++ b/src/HOL/IsaMakefile Thu Nov 12 20:38:57 2009 +0100
3.3 @@ -382,8 +382,9 @@
3.4 Library/Order_Relation.thy Library/Nested_Environment.thy \
3.5 Library/Ramsey.thy Library/Zorn.thy Library/Library/ROOT.ML \
3.6 Library/Library/document/root.tex Library/Library/document/root.bib \
3.7 - Library/While_Combinator.thy Library/Product_ord.thy \
3.8 - Library/Char_nat.thy Library/Char_ord.thy Library/Option_ord.thy \
3.9 + Library/Transitive_Closure_Table.thy Library/While_Combinator.thy \
3.10 + Library/Product_ord.thy Library/Char_nat.thy \
3.11 + Library/Char_ord.thy Library/Option_ord.thy \
3.12 Library/Sublist_Order.thy Library/List_lexord.thy \
3.13 Library/Coinductive_List.thy Library/AssocList.thy \
3.14 Library/Formal_Power_Series.thy Library/Binomial.thy \
4.1 --- a/src/HOL/Library/Library.thy Thu Nov 12 17:21:51 2009 +0100
4.2 +++ b/src/HOL/Library/Library.thy Thu Nov 12 20:38:57 2009 +0100
4.3 @@ -51,6 +51,7 @@
4.4 SML_Quickcheck
4.5 State_Monad
4.6 Sum_Of_Squares
4.7 + Transitive_Closure_Table
4.8 Univ_Poly
4.9 While_Combinator
4.10 Word
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/HOL/Library/Transitive_Closure_Table.thy Thu Nov 12 20:38:57 2009 +0100
5.3 @@ -0,0 +1,230 @@
5.4 +(* Author: Stefan Berghofer, Lukas Bulwahn, TU Muenchen *)
5.5 +
5.6 +header {* A tabled implementation of the reflexive transitive closure *}
5.7 +
5.8 +theory Transitive_Closure_Table
5.9 +imports Main
5.10 +begin
5.11 +
5.12 +inductive rtrancl_path :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool"
5.13 + for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
5.14 +where
5.15 + base: "rtrancl_path r x [] x"
5.16 +| step: "r x y \<Longrightarrow> rtrancl_path r y ys z \<Longrightarrow> rtrancl_path r x (y # ys) z"
5.17 +
5.18 +lemma rtranclp_eq_rtrancl_path: "r\<^sup>*\<^sup>* x y = (\<exists>xs. rtrancl_path r x xs y)"
5.19 +proof
5.20 + assume "r\<^sup>*\<^sup>* x y"
5.21 + then show "\<exists>xs. rtrancl_path r x xs y"
5.22 + proof (induct rule: converse_rtranclp_induct)
5.23 + case 1
5.24 + have "rtrancl_path r y [] y" by (rule rtrancl_path.base)
5.25 + then show ?case ..
5.26 + next
5.27 + case (2 x z)
5.28 + from `\<exists>xs. rtrancl_path r z xs y`
5.29 + obtain xs where "rtrancl_path r z xs y" ..
5.30 + with `r x z` have "rtrancl_path r x (z # xs) y"
5.31 + by (rule rtrancl_path.step)
5.32 + then show ?case ..
5.33 + qed
5.34 +next
5.35 + assume "\<exists>xs. rtrancl_path r x xs y"
5.36 + then obtain xs where "rtrancl_path r x xs y" ..
5.37 + then show "r\<^sup>*\<^sup>* x y"
5.38 + proof induct
5.39 + case (base x)
5.40 + show ?case by (rule rtranclp.rtrancl_refl)
5.41 + next
5.42 + case (step x y ys z)
5.43 + from `r x y` `r\<^sup>*\<^sup>* y z` show ?case
5.44 + by (rule converse_rtranclp_into_rtranclp)
5.45 + qed
5.46 +qed
5.47 +
5.48 +lemma rtrancl_path_trans:
5.49 + assumes xy: "rtrancl_path r x xs y"
5.50 + and yz: "rtrancl_path r y ys z"
5.51 + shows "rtrancl_path r x (xs @ ys) z" using xy yz
5.52 +proof (induct arbitrary: z)
5.53 + case (base x)
5.54 + then show ?case by simp
5.55 +next
5.56 + case (step x y xs)
5.57 + then have "rtrancl_path r y (xs @ ys) z"
5.58 + by simp
5.59 + with `r x y` have "rtrancl_path r x (y # (xs @ ys)) z"
5.60 + by (rule rtrancl_path.step)
5.61 + then show ?case by simp
5.62 +qed
5.63 +
5.64 +lemma rtrancl_path_appendE:
5.65 + assumes xz: "rtrancl_path r x (xs @ y # ys) z"
5.66 + obtains "rtrancl_path r x (xs @ [y]) y" and "rtrancl_path r y ys z" using xz
5.67 +proof (induct xs arbitrary: x)
5.68 + case Nil
5.69 + then have "rtrancl_path r x (y # ys) z" by simp
5.70 + then obtain xy: "r x y" and yz: "rtrancl_path r y ys z"
5.71 + by cases auto
5.72 + from xy have "rtrancl_path r x [y] y"
5.73 + by (rule rtrancl_path.step [OF _ rtrancl_path.base])
5.74 + then have "rtrancl_path r x ([] @ [y]) y" by simp
5.75 + then show ?thesis using yz by (rule Nil)
5.76 +next
5.77 + case (Cons a as)
5.78 + then have "rtrancl_path r x (a # (as @ y # ys)) z" by simp
5.79 + then obtain xa: "r x a" and az: "rtrancl_path r a (as @ y # ys) z"
5.80 + by cases auto
5.81 + show ?thesis
5.82 + proof (rule Cons(1) [OF _ az])
5.83 + assume "rtrancl_path r y ys z"
5.84 + assume "rtrancl_path r a (as @ [y]) y"
5.85 + with xa have "rtrancl_path r x (a # (as @ [y])) y"
5.86 + by (rule rtrancl_path.step)
5.87 + then have "rtrancl_path r x ((a # as) @ [y]) y"
5.88 + by simp
5.89 + then show ?thesis using `rtrancl_path r y ys z`
5.90 + by (rule Cons(2))
5.91 + qed
5.92 +qed
5.93 +
5.94 +lemma rtrancl_path_distinct:
5.95 + assumes xy: "rtrancl_path r x xs y"
5.96 + obtains xs' where "rtrancl_path r x xs' y" and "distinct (x # xs')" using xy
5.97 +proof (induct xs rule: measure_induct_rule [of length])
5.98 + case (less xs)
5.99 + show ?case
5.100 + proof (cases "distinct (x # xs)")
5.101 + case True
5.102 + with `rtrancl_path r x xs y` show ?thesis by (rule less)
5.103 + next
5.104 + case False
5.105 + then have "\<exists>as bs cs a. x # xs = as @ [a] @ bs @ [a] @ cs"
5.106 + by (rule not_distinct_decomp)
5.107 + then obtain as bs cs a where xxs: "x # xs = as @ [a] @ bs @ [a] @ cs"
5.108 + by iprover
5.109 + show ?thesis
5.110 + proof (cases as)
5.111 + case Nil
5.112 + with xxs have x: "x = a" and xs: "xs = bs @ a # cs"
5.113 + by auto
5.114 + from x xs `rtrancl_path r x xs y` have cs: "rtrancl_path r x cs y"
5.115 + by (auto elim: rtrancl_path_appendE)
5.116 + from xs have "length cs < length xs" by simp
5.117 + then show ?thesis
5.118 + by (rule less(1)) (iprover intro: cs less(2))+
5.119 + next
5.120 + case (Cons d ds)
5.121 + with xxs have xs: "xs = ds @ a # (bs @ [a] @ cs)"
5.122 + by auto
5.123 + with `rtrancl_path r x xs y` obtain xa: "rtrancl_path r x (ds @ [a]) a"
5.124 + and ay: "rtrancl_path r a (bs @ a # cs) y"
5.125 + by (auto elim: rtrancl_path_appendE)
5.126 + from ay have "rtrancl_path r a cs y" by (auto elim: rtrancl_path_appendE)
5.127 + with xa have xy: "rtrancl_path r x ((ds @ [a]) @ cs) y"
5.128 + by (rule rtrancl_path_trans)
5.129 + from xs have "length ((ds @ [a]) @ cs) < length xs" by simp
5.130 + then show ?thesis
5.131 + by (rule less(1)) (iprover intro: xy less(2))+
5.132 + qed
5.133 + qed
5.134 +qed
5.135 +
5.136 +inductive rtrancl_tab :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
5.137 + for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
5.138 +where
5.139 + base: "rtrancl_tab r xs x x"
5.140 +| step: "x \<notin> set xs \<Longrightarrow> r x y \<Longrightarrow> rtrancl_tab r (x # xs) y z \<Longrightarrow> rtrancl_tab r xs x z"
5.141 +
5.142 +lemma rtrancl_path_imp_rtrancl_tab:
5.143 + assumes path: "rtrancl_path r x xs y"
5.144 + and x: "distinct (x # xs)"
5.145 + and ys: "({x} \<union> set xs) \<inter> set ys = {}"
5.146 + shows "rtrancl_tab r ys x y" using path x ys
5.147 +proof (induct arbitrary: ys)
5.148 + case base
5.149 + show ?case by (rule rtrancl_tab.base)
5.150 +next
5.151 + case (step x y zs z)
5.152 + then have "x \<notin> set ys" by auto
5.153 + from step have "distinct (y # zs)" by simp
5.154 + moreover from step have "({y} \<union> set zs) \<inter> set (x # ys) = {}"
5.155 + by auto
5.156 + ultimately have "rtrancl_tab r (x # ys) y z"
5.157 + by (rule step)
5.158 + with `x \<notin> set ys` `r x y`
5.159 + show ?case by (rule rtrancl_tab.step)
5.160 +qed
5.161 +
5.162 +lemma rtrancl_tab_imp_rtrancl_path:
5.163 + assumes tab: "rtrancl_tab r ys x y"
5.164 + obtains xs where "rtrancl_path r x xs y" using tab
5.165 +proof induct
5.166 + case base
5.167 + from rtrancl_path.base show ?case by (rule base)
5.168 +next
5.169 + case step show ?case by (iprover intro: step rtrancl_path.step)
5.170 +qed
5.171 +
5.172 +lemma rtranclp_eq_rtrancl_tab_nil: "r\<^sup>*\<^sup>* x y = rtrancl_tab r [] x y"
5.173 +proof
5.174 + assume "r\<^sup>*\<^sup>* x y"
5.175 + then obtain xs where "rtrancl_path r x xs y"
5.176 + by (auto simp add: rtranclp_eq_rtrancl_path)
5.177 + then obtain xs' where xs': "rtrancl_path r x xs' y"
5.178 + and distinct: "distinct (x # xs')"
5.179 + by (rule rtrancl_path_distinct)
5.180 + have "({x} \<union> set xs') \<inter> set [] = {}" by simp
5.181 + with xs' distinct show "rtrancl_tab r [] x y"
5.182 + by (rule rtrancl_path_imp_rtrancl_tab)
5.183 +next
5.184 + assume "rtrancl_tab r [] x y"
5.185 + then obtain xs where "rtrancl_path r x xs y"
5.186 + by (rule rtrancl_tab_imp_rtrancl_path)
5.187 + then show "r\<^sup>*\<^sup>* x y"
5.188 + by (auto simp add: rtranclp_eq_rtrancl_path)
5.189 +qed
5.190 +
5.191 +declare rtranclp_eq_rtrancl_tab_nil [code_unfold]
5.192 +
5.193 +declare rtranclp_eq_rtrancl_tab_nil[THEN iffD2, code_pred_intro]
5.194 +
5.195 +code_pred rtranclp using rtranclp_eq_rtrancl_tab_nil[THEN iffD1] by fastsimp
5.196 +
5.197 +subsection {* A simple example *}
5.198 +
5.199 +datatype ty = A | B | C
5.200 +
5.201 +inductive test :: "ty \<Rightarrow> ty \<Rightarrow> bool"
5.202 +where
5.203 + "test A B"
5.204 +| "test B A"
5.205 +| "test B C"
5.206 +
5.207 +subsubsection {* Invoking with the SML code generator *}
5.208 +
5.209 +code_module Test
5.210 +contains
5.211 +test1 = "test\<^sup>*\<^sup>* A C"
5.212 +test2 = "test\<^sup>*\<^sup>* C A"
5.213 +test3 = "test\<^sup>*\<^sup>* A _"
5.214 +test4 = "test\<^sup>*\<^sup>* _ C"
5.215 +
5.216 +ML "Test.test1"
5.217 +ML "Test.test2"
5.218 +ML "DSeq.list_of Test.test3"
5.219 +ML "DSeq.list_of Test.test4"
5.220 +
5.221 +subsubsection {* Invoking with the predicate compiler and the generic code generator *}
5.222 +
5.223 +code_pred test .
5.224 +
5.225 +values "{x. test\<^sup>*\<^sup>* A C}"
5.226 +values "{x. test\<^sup>*\<^sup>* C A}"
5.227 +values "{x. test\<^sup>*\<^sup>* A x}"
5.228 +values "{x. test\<^sup>*\<^sup>* x C}"
5.229 +
5.230 +hide const test
5.231 +
5.232 +end
5.233 +