author | bulwahn |

Thu Nov 12 20:38:57 2009 +0100 (2009-11-12) | |

changeset 33649 | 854173fcd21c |

parent 33640 | 0d82107dc07a |

child 33650 | dd3ea99d5c76 |

added a tabled implementation of the reflexive transitive closure

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 +