added a tabled implementation of the reflexive transitive closure
authorbulwahn
Thu Nov 12 20:38:57 2009 +0100 (2009-11-12)
changeset 33649854173fcd21c
parent 33640 0d82107dc07a
child 33650 dd3ea99d5c76
added a tabled implementation of the reflexive transitive closure
CONTRIBUTORS
NEWS
src/HOL/IsaMakefile
src/HOL/Library/Library.thy
src/HOL/Library/Transitive_Closure_Table.thy
     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 +