summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Library/Transitive_Closure_Table.thy

changeset 33649 | 854173fcd21c |

child 33870 | 5b0d23d2c08f |

--- /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 +