src/HOL/Library/Transitive_Closure_Table.thy
author wenzelm
Mon Mar 01 21:41:35 2010 +0100 (2010-03-01)
changeset 35423 6ef9525a5727
parent 34912 c04747153bcf
child 36176 3fe7e97ccca8
permissions -rw-r--r--
eliminated hard tabs;
     1 (* Author: Stefan Berghofer, Lukas Bulwahn, TU Muenchen *)
     2 
     3 header {* A tabled implementation of the reflexive transitive closure *}
     4 
     5 theory Transitive_Closure_Table
     6 imports Main
     7 begin
     8 
     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"
    14 
    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
    44 
    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
    60 
    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
    90 
    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
   132 
   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"
   138 
   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
   158 
   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
   168 
   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
   187 
   188 declare rtranclp_eq_rtrancl_tab_nil [code_unfold, code_inline del]
   189 
   190 declare rtranclp_eq_rtrancl_tab_nil[THEN iffD2, code_pred_intro]
   191 
   192 code_pred rtranclp using rtranclp_eq_rtrancl_tab_nil[THEN iffD1] by fastsimp
   193 
   194 subsection {* A simple example *}
   195 
   196 datatype ty = A | B | C
   197 
   198 inductive test :: "ty \<Rightarrow> ty \<Rightarrow> bool"
   199 where
   200   "test A B"
   201 | "test B A"
   202 | "test B C"
   203 
   204 subsubsection {* Invoking with the SML code generator *}
   205 
   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"
   212 
   213 ML "Test.test1"
   214 ML "Test.test2"
   215 ML "DSeq.list_of Test.test3"
   216 ML "DSeq.list_of Test.test4"
   217 
   218 subsubsection {* Invoking with the predicate compiler and the generic code generator *}
   219 
   220 code_pred test .
   221 
   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}"
   226 
   227 value "test\<^sup>*\<^sup>* A C"
   228 value "test\<^sup>*\<^sup>* C A"
   229 
   230 hide type ty
   231 hide const test A B C
   232 
   233 end
   234