# HG changeset patch
# User bulwahn
# Date 1258054737 -3600
# Node ID 854173fcd21c36095d1f0bd3bc36cf9b94181e7c
# Parent  0d82107dc07a939ebd972665cf3fcb34b6ff1d93
added a tabled implementation of the reflexive transitive closure

diff -r 0d82107dc07a -r 854173fcd21c CONTRIBUTORS
--- a/CONTRIBUTORS	Thu Nov 12 17:21:51 2009 +0100
+++ b/CONTRIBUTORS	Thu Nov 12 20:38:57 2009 +0100
@@ -6,6 +6,10 @@
 
 Contributions to this Isabelle version
 --------------------------------------
+
+* November 2009: Stefan Berghofer, Lukas Bulwahn, TUM
+  A tabled implementation of the reflexive transitive closure
+
 * November 2009: Lukas Bulwahn, TUM
   Predicate Compiler: a compiler for inductive predicates to equational specfications
  
diff -r 0d82107dc07a -r 854173fcd21c NEWS
--- a/NEWS	Thu Nov 12 17:21:51 2009 +0100
+++ b/NEWS	Thu Nov 12 20:38:57 2009 +0100
@@ -37,6 +37,8 @@
 
 *** HOL ***
 
+* A tabled implementation of the reflexive transitive closure
+
 * New commands "code_pred" and "values" to invoke the predicate compiler
 and to enumerate values of inductive predicates.
 
diff -r 0d82107dc07a -r 854173fcd21c src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Nov 12 17:21:51 2009 +0100
+++ b/src/HOL/IsaMakefile	Thu Nov 12 20:38:57 2009 +0100
@@ -382,8 +382,9 @@
   Library/Order_Relation.thy Library/Nested_Environment.thy		\
   Library/Ramsey.thy Library/Zorn.thy Library/Library/ROOT.ML		\
   Library/Library/document/root.tex Library/Library/document/root.bib	\
-  Library/While_Combinator.thy Library/Product_ord.thy			\
-  Library/Char_nat.thy Library/Char_ord.thy Library/Option_ord.thy	\
+  Library/Transitive_Closure_Table.thy Library/While_Combinator.thy \
+  Library/Product_ord.thy	Library/Char_nat.thy \
+  Library/Char_ord.thy Library/Option_ord.thy	\
   Library/Sublist_Order.thy Library/List_lexord.thy			\
   Library/Coinductive_List.thy Library/AssocList.thy			\
   Library/Formal_Power_Series.thy Library/Binomial.thy			\
diff -r 0d82107dc07a -r 854173fcd21c src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Thu Nov 12 17:21:51 2009 +0100
+++ b/src/HOL/Library/Library.thy	Thu Nov 12 20:38:57 2009 +0100
@@ -51,6 +51,7 @@
   SML_Quickcheck
   State_Monad
   Sum_Of_Squares
+  Transitive_Closure_Table
   Univ_Poly
   While_Combinator
   Word
diff -r 0d82107dc07a -r 854173fcd21c src/HOL/Library/Transitive_Closure_Table.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Transitive_Closure_Table.thy	Thu Nov 12 20:38:57 2009 +0100
@@ -0,0 +1,230 @@
+(* Author: Stefan Berghofer, Lukas Bulwahn, TU Muenchen *)
+
+header {* A tabled implementation of the reflexive transitive closure *}
+
+theory Transitive_Closure_Table
+imports Main
+begin
+
+inductive rtrancl_path :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool"
+  for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+where
+  base: "rtrancl_path r x [] x"
+| step: "r x y \<Longrightarrow> rtrancl_path r y ys z \<Longrightarrow> rtrancl_path r x (y # ys) z"
+
+lemma rtranclp_eq_rtrancl_path: "r\<^sup>*\<^sup>* x y = (\<exists>xs. rtrancl_path r x xs y)"
+proof
+  assume "r\<^sup>*\<^sup>* x y"
+  then show "\<exists>xs. rtrancl_path r x xs y"
+  proof (induct rule: converse_rtranclp_induct)
+    case 1
+    have "rtrancl_path r y [] y" by (rule rtrancl_path.base)
+    then show ?case ..
+  next
+    case (2 x z)
+    from `\<exists>xs. rtrancl_path r z xs y`
+    obtain xs where "rtrancl_path r z xs y" ..
+    with `r x z` have "rtrancl_path r x (z # xs) y"
+      by (rule rtrancl_path.step)
+    then show ?case ..
+  qed
+next
+  assume "\<exists>xs. rtrancl_path r x xs y"
+  then obtain xs where "rtrancl_path r x xs y" ..
+  then show "r\<^sup>*\<^sup>* x y"
+  proof induct
+    case (base x)
+    show ?case by (rule rtranclp.rtrancl_refl)
+  next
+    case (step x y ys z)
+    from `r x y` `r\<^sup>*\<^sup>* y z` show ?case
+      by (rule converse_rtranclp_into_rtranclp)
+  qed
+qed
+
+lemma rtrancl_path_trans:
+  assumes xy: "rtrancl_path r x xs y"
+  and yz: "rtrancl_path r y ys z"
+  shows "rtrancl_path r x (xs @ ys) z" using xy yz
+proof (induct arbitrary: z)
+  case (base x)
+  then show ?case by simp
+next
+  case (step x y xs)
+  then have "rtrancl_path r y (xs @ ys) z"
+    by simp
+  with `r x y` have "rtrancl_path r x (y # (xs @ ys)) z"
+    by (rule rtrancl_path.step)
+  then show ?case by simp
+qed
+
+lemma rtrancl_path_appendE:
+  assumes xz: "rtrancl_path r x (xs @ y # ys) z"
+  obtains "rtrancl_path r x (xs @ [y]) y" and "rtrancl_path r y ys z" using xz
+proof (induct xs arbitrary: x)
+  case Nil
+  then have "rtrancl_path r x (y # ys) z" by simp
+  then obtain xy: "r x y" and yz: "rtrancl_path r y ys z"
+    by cases auto
+  from xy have "rtrancl_path r x [y] y"
+    by (rule rtrancl_path.step [OF _ rtrancl_path.base])
+  then have "rtrancl_path r x ([] @ [y]) y" by simp
+  then show ?thesis using yz by (rule Nil)
+next
+  case (Cons a as)
+  then have "rtrancl_path r x (a # (as @ y # ys)) z" by simp
+  then obtain xa: "r x a" and az: "rtrancl_path r a (as @ y # ys) z"
+    by cases auto
+  show ?thesis
+  proof (rule Cons(1) [OF _ az])
+    assume "rtrancl_path r y ys z"
+    assume "rtrancl_path r a (as @ [y]) y"
+    with xa have "rtrancl_path r x (a # (as @ [y])) y"
+      by (rule rtrancl_path.step)
+    then have "rtrancl_path r x ((a # as) @ [y]) y"
+      by simp
+    then show ?thesis using `rtrancl_path r y ys z`
+      by (rule Cons(2))
+  qed
+qed
+
+lemma rtrancl_path_distinct:
+  assumes xy: "rtrancl_path r x xs y"
+  obtains xs' where "rtrancl_path r x xs' y" and "distinct (x # xs')" using xy
+proof (induct xs rule: measure_induct_rule [of length])
+  case (less xs)
+  show ?case
+  proof (cases "distinct (x # xs)")
+    case True
+    with `rtrancl_path r x xs y` show ?thesis by (rule less)
+  next
+    case False
+    then have "\<exists>as bs cs a. x # xs = as @ [a] @ bs @ [a] @ cs"
+      by (rule not_distinct_decomp)
+    then obtain as bs cs a where xxs: "x # xs = as @ [a] @ bs @ [a] @ cs"
+      by iprover
+    show ?thesis
+    proof (cases as)
+      case Nil
+      with xxs have x: "x = a" and xs: "xs = bs @ a # cs"
+	by auto
+      from x xs `rtrancl_path r x xs y` have cs: "rtrancl_path r x cs y"
+	by (auto elim: rtrancl_path_appendE)
+      from xs have "length cs < length xs" by simp
+      then show ?thesis
+	by (rule less(1)) (iprover intro: cs less(2))+
+    next
+      case (Cons d ds)
+      with xxs have xs: "xs = ds @ a # (bs @ [a] @ cs)"
+	by auto
+      with `rtrancl_path r x xs y` obtain xa: "rtrancl_path r x (ds @ [a]) a"
+        and ay: "rtrancl_path r a (bs @ a # cs) y"
+	by (auto elim: rtrancl_path_appendE)
+      from ay have "rtrancl_path r a cs y" by (auto elim: rtrancl_path_appendE)
+      with xa have xy: "rtrancl_path r x ((ds @ [a]) @ cs) y"
+	by (rule rtrancl_path_trans)
+      from xs have "length ((ds @ [a]) @ cs) < length xs" by simp
+      then show ?thesis
+	by (rule less(1)) (iprover intro: xy less(2))+
+    qed
+  qed
+qed
+
+inductive rtrancl_tab :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+  for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+where
+  base: "rtrancl_tab r xs x x"
+| step: "x \<notin> set xs \<Longrightarrow> r x y \<Longrightarrow> rtrancl_tab r (x # xs) y z \<Longrightarrow> rtrancl_tab r xs x z"
+
+lemma rtrancl_path_imp_rtrancl_tab:
+  assumes path: "rtrancl_path r x xs y"
+  and x: "distinct (x # xs)"
+  and ys: "({x} \<union> set xs) \<inter> set ys = {}"
+  shows "rtrancl_tab r ys x y" using path x ys
+proof (induct arbitrary: ys)
+  case base
+  show ?case by (rule rtrancl_tab.base)
+next
+  case (step x y zs z)
+  then have "x \<notin> set ys" by auto
+  from step have "distinct (y # zs)" by simp
+  moreover from step have "({y} \<union> set zs) \<inter> set (x # ys) = {}"
+    by auto
+  ultimately have "rtrancl_tab r (x # ys) y z"
+    by (rule step)
+  with `x \<notin> set ys` `r x y`
+  show ?case by (rule rtrancl_tab.step)
+qed
+
+lemma rtrancl_tab_imp_rtrancl_path:
+  assumes tab: "rtrancl_tab r ys x y"
+  obtains xs where "rtrancl_path r x xs y" using tab
+proof induct
+  case base
+  from rtrancl_path.base show ?case by (rule base)
+next
+  case step show ?case by (iprover intro: step rtrancl_path.step)
+qed
+
+lemma rtranclp_eq_rtrancl_tab_nil: "r\<^sup>*\<^sup>* x y = rtrancl_tab r [] x y"
+proof
+  assume "r\<^sup>*\<^sup>* x y"
+  then obtain xs where "rtrancl_path r x xs y"
+    by (auto simp add: rtranclp_eq_rtrancl_path)
+  then obtain xs' where xs': "rtrancl_path r x xs' y"
+    and distinct: "distinct (x # xs')"
+    by (rule rtrancl_path_distinct)
+  have "({x} \<union> set xs') \<inter> set [] = {}" by simp
+  with xs' distinct show "rtrancl_tab r [] x y"
+    by (rule rtrancl_path_imp_rtrancl_tab)
+next
+  assume "rtrancl_tab r [] x y"
+  then obtain xs where "rtrancl_path r x xs y"
+    by (rule rtrancl_tab_imp_rtrancl_path)
+  then show "r\<^sup>*\<^sup>* x y"
+    by (auto simp add: rtranclp_eq_rtrancl_path)
+qed
+
+declare rtranclp_eq_rtrancl_tab_nil [code_unfold]
+
+declare rtranclp_eq_rtrancl_tab_nil[THEN iffD2, code_pred_intro]
+
+code_pred rtranclp using rtranclp_eq_rtrancl_tab_nil[THEN iffD1] by fastsimp
+
+subsection {* A simple example *}
+
+datatype ty = A | B | C
+
+inductive test :: "ty \<Rightarrow> ty \<Rightarrow> bool"
+where
+  "test A B"
+| "test B A"
+| "test B C"
+
+subsubsection {* Invoking with the SML code generator *}
+
+code_module Test
+contains
+test1 = "test\<^sup>*\<^sup>* A C"
+test2 = "test\<^sup>*\<^sup>* C A"
+test3 = "test\<^sup>*\<^sup>* A _"
+test4 = "test\<^sup>*\<^sup>* _ C"
+
+ML "Test.test1"
+ML "Test.test2"
+ML "DSeq.list_of Test.test3"
+ML "DSeq.list_of Test.test4"
+
+subsubsection {* Invoking with the predicate compiler and the generic code generator *}
+
+code_pred test .
+
+values "{x. test\<^sup>*\<^sup>* A C}"
+values "{x. test\<^sup>*\<^sup>* C A}"
+values "{x. test\<^sup>*\<^sup>* A x}"
+values "{x. test\<^sup>*\<^sup>* x C}"
+
+hide const test
+
+end
+