bulwahn@33649: (* Author: Stefan Berghofer, Lukas Bulwahn, TU Muenchen *)
bulwahn@33649:
bulwahn@33649: header {* A tabled implementation of the reflexive transitive closure *}
bulwahn@33649:
bulwahn@33649: theory Transitive_Closure_Table
bulwahn@33649: imports Main
bulwahn@33649: begin
bulwahn@33649:
bulwahn@33649: inductive rtrancl_path :: "('a \ 'a \ bool) \ 'a \ 'a list \ 'a \ bool"
bulwahn@33649: for r :: "'a \ 'a \ bool"
bulwahn@33649: where
bulwahn@33649: base: "rtrancl_path r x [] x"
bulwahn@33649: | step: "r x y \ rtrancl_path r y ys z \ rtrancl_path r x (y # ys) z"
bulwahn@33649:
bulwahn@33649: lemma rtranclp_eq_rtrancl_path: "r\<^sup>*\<^sup>* x y = (\xs. rtrancl_path r x xs y)"
bulwahn@33649: proof
bulwahn@33649: assume "r\<^sup>*\<^sup>* x y"
bulwahn@33649: then show "\xs. rtrancl_path r x xs y"
bulwahn@33649: proof (induct rule: converse_rtranclp_induct)
berghofe@34912: case base
bulwahn@33649: have "rtrancl_path r y [] y" by (rule rtrancl_path.base)
bulwahn@33649: then show ?case ..
bulwahn@33649: next
berghofe@34912: case (step x z)
bulwahn@33649: from `\xs. rtrancl_path r z xs y`
bulwahn@33649: obtain xs where "rtrancl_path r z xs y" ..
bulwahn@33649: with `r x z` have "rtrancl_path r x (z # xs) y"
bulwahn@33649: by (rule rtrancl_path.step)
bulwahn@33649: then show ?case ..
bulwahn@33649: qed
bulwahn@33649: next
bulwahn@33649: assume "\xs. rtrancl_path r x xs y"
bulwahn@33649: then obtain xs where "rtrancl_path r x xs y" ..
bulwahn@33649: then show "r\<^sup>*\<^sup>* x y"
bulwahn@33649: proof induct
bulwahn@33649: case (base x)
bulwahn@33649: show ?case by (rule rtranclp.rtrancl_refl)
bulwahn@33649: next
bulwahn@33649: case (step x y ys z)
bulwahn@33649: from `r x y` `r\<^sup>*\<^sup>* y z` show ?case
bulwahn@33649: by (rule converse_rtranclp_into_rtranclp)
bulwahn@33649: qed
bulwahn@33649: qed
bulwahn@33649:
bulwahn@33649: lemma rtrancl_path_trans:
bulwahn@33649: assumes xy: "rtrancl_path r x xs y"
bulwahn@33649: and yz: "rtrancl_path r y ys z"
bulwahn@33649: shows "rtrancl_path r x (xs @ ys) z" using xy yz
bulwahn@33649: proof (induct arbitrary: z)
bulwahn@33649: case (base x)
bulwahn@33649: then show ?case by simp
bulwahn@33649: next
bulwahn@33649: case (step x y xs)
bulwahn@33649: then have "rtrancl_path r y (xs @ ys) z"
bulwahn@33649: by simp
bulwahn@33649: with `r x y` have "rtrancl_path r x (y # (xs @ ys)) z"
bulwahn@33649: by (rule rtrancl_path.step)
bulwahn@33649: then show ?case by simp
bulwahn@33649: qed
bulwahn@33649:
bulwahn@33649: lemma rtrancl_path_appendE:
bulwahn@33649: assumes xz: "rtrancl_path r x (xs @ y # ys) z"
bulwahn@33649: obtains "rtrancl_path r x (xs @ [y]) y" and "rtrancl_path r y ys z" using xz
bulwahn@33649: proof (induct xs arbitrary: x)
bulwahn@33649: case Nil
bulwahn@33649: then have "rtrancl_path r x (y # ys) z" by simp
bulwahn@33649: then obtain xy: "r x y" and yz: "rtrancl_path r y ys z"
bulwahn@33649: by cases auto
bulwahn@33649: from xy have "rtrancl_path r x [y] y"
bulwahn@33649: by (rule rtrancl_path.step [OF _ rtrancl_path.base])
bulwahn@33649: then have "rtrancl_path r x ([] @ [y]) y" by simp
bulwahn@33649: then show ?thesis using yz by (rule Nil)
bulwahn@33649: next
bulwahn@33649: case (Cons a as)
bulwahn@33649: then have "rtrancl_path r x (a # (as @ y # ys)) z" by simp
bulwahn@33649: then obtain xa: "r x a" and az: "rtrancl_path r a (as @ y # ys) z"
bulwahn@33649: by cases auto
bulwahn@33649: show ?thesis
bulwahn@33649: proof (rule Cons(1) [OF _ az])
bulwahn@33649: assume "rtrancl_path r y ys z"
bulwahn@33649: assume "rtrancl_path r a (as @ [y]) y"
bulwahn@33649: with xa have "rtrancl_path r x (a # (as @ [y])) y"
bulwahn@33649: by (rule rtrancl_path.step)
bulwahn@33649: then have "rtrancl_path r x ((a # as) @ [y]) y"
bulwahn@33649: by simp
bulwahn@33649: then show ?thesis using `rtrancl_path r y ys z`
bulwahn@33649: by (rule Cons(2))
bulwahn@33649: qed
bulwahn@33649: qed
bulwahn@33649:
bulwahn@33649: lemma rtrancl_path_distinct:
bulwahn@33649: assumes xy: "rtrancl_path r x xs y"
bulwahn@33649: obtains xs' where "rtrancl_path r x xs' y" and "distinct (x # xs')" using xy
bulwahn@33649: proof (induct xs rule: measure_induct_rule [of length])
bulwahn@33649: case (less xs)
bulwahn@33649: show ?case
bulwahn@33649: proof (cases "distinct (x # xs)")
bulwahn@33649: case True
bulwahn@33649: with `rtrancl_path r x xs y` show ?thesis by (rule less)
bulwahn@33649: next
bulwahn@33649: case False
bulwahn@33649: then have "\as bs cs a. x # xs = as @ [a] @ bs @ [a] @ cs"
bulwahn@33649: by (rule not_distinct_decomp)
bulwahn@33649: then obtain as bs cs a where xxs: "x # xs = as @ [a] @ bs @ [a] @ cs"
bulwahn@33649: by iprover
bulwahn@33649: show ?thesis
bulwahn@33649: proof (cases as)
bulwahn@33649: case Nil
bulwahn@33649: with xxs have x: "x = a" and xs: "xs = bs @ a # cs"
wenzelm@35423: by auto
bulwahn@33649: from x xs `rtrancl_path r x xs y` have cs: "rtrancl_path r x cs y"
wenzelm@35423: by (auto elim: rtrancl_path_appendE)
bulwahn@33649: from xs have "length cs < length xs" by simp
bulwahn@33649: then show ?thesis
wenzelm@35423: by (rule less(1)) (iprover intro: cs less(2))+
bulwahn@33649: next
bulwahn@33649: case (Cons d ds)
bulwahn@33649: with xxs have xs: "xs = ds @ a # (bs @ [a] @ cs)"
wenzelm@35423: by auto
bulwahn@33649: with `rtrancl_path r x xs y` obtain xa: "rtrancl_path r x (ds @ [a]) a"
bulwahn@33649: and ay: "rtrancl_path r a (bs @ a # cs) y"
wenzelm@35423: by (auto elim: rtrancl_path_appendE)
bulwahn@33649: from ay have "rtrancl_path r a cs y" by (auto elim: rtrancl_path_appendE)
bulwahn@33649: with xa have xy: "rtrancl_path r x ((ds @ [a]) @ cs) y"
wenzelm@35423: by (rule rtrancl_path_trans)
bulwahn@33649: from xs have "length ((ds @ [a]) @ cs) < length xs" by simp
bulwahn@33649: then show ?thesis
wenzelm@35423: by (rule less(1)) (iprover intro: xy less(2))+
bulwahn@33649: qed
bulwahn@33649: qed
bulwahn@33649: qed
bulwahn@33649:
bulwahn@33649: inductive rtrancl_tab :: "('a \ 'a \ bool) \ 'a list \ 'a \ 'a \ bool"
bulwahn@33649: for r :: "'a \ 'a \ bool"
bulwahn@33649: where
bulwahn@33649: base: "rtrancl_tab r xs x x"
bulwahn@33649: | step: "x \ set xs \ r x y \ rtrancl_tab r (x # xs) y z \ rtrancl_tab r xs x z"
bulwahn@33649:
bulwahn@33649: lemma rtrancl_path_imp_rtrancl_tab:
bulwahn@33649: assumes path: "rtrancl_path r x xs y"
bulwahn@33649: and x: "distinct (x # xs)"
bulwahn@33649: and ys: "({x} \ set xs) \ set ys = {}"
bulwahn@33649: shows "rtrancl_tab r ys x y" using path x ys
bulwahn@33649: proof (induct arbitrary: ys)
bulwahn@33649: case base
bulwahn@33649: show ?case by (rule rtrancl_tab.base)
bulwahn@33649: next
bulwahn@33649: case (step x y zs z)
bulwahn@33649: then have "x \ set ys" by auto
bulwahn@33649: from step have "distinct (y # zs)" by simp
bulwahn@33649: moreover from step have "({y} \ set zs) \ set (x # ys) = {}"
bulwahn@33649: by auto
bulwahn@33649: ultimately have "rtrancl_tab r (x # ys) y z"
bulwahn@33649: by (rule step)
bulwahn@33649: with `x \ set ys` `r x y`
bulwahn@33649: show ?case by (rule rtrancl_tab.step)
bulwahn@33649: qed
bulwahn@33649:
bulwahn@33649: lemma rtrancl_tab_imp_rtrancl_path:
bulwahn@33649: assumes tab: "rtrancl_tab r ys x y"
bulwahn@33649: obtains xs where "rtrancl_path r x xs y" using tab
bulwahn@33649: proof induct
bulwahn@33649: case base
bulwahn@33649: from rtrancl_path.base show ?case by (rule base)
bulwahn@33649: next
bulwahn@33649: case step show ?case by (iprover intro: step rtrancl_path.step)
bulwahn@33649: qed
bulwahn@33649:
bulwahn@33649: lemma rtranclp_eq_rtrancl_tab_nil: "r\<^sup>*\<^sup>* x y = rtrancl_tab r [] x y"
bulwahn@33649: proof
bulwahn@33649: assume "r\<^sup>*\<^sup>* x y"
bulwahn@33649: then obtain xs where "rtrancl_path r x xs y"
bulwahn@33649: by (auto simp add: rtranclp_eq_rtrancl_path)
bulwahn@33649: then obtain xs' where xs': "rtrancl_path r x xs' y"
bulwahn@33649: and distinct: "distinct (x # xs')"
bulwahn@33649: by (rule rtrancl_path_distinct)
bulwahn@33649: have "({x} \ set xs') \ set [] = {}" by simp
bulwahn@33649: with xs' distinct show "rtrancl_tab r [] x y"
bulwahn@33649: by (rule rtrancl_path_imp_rtrancl_tab)
bulwahn@33649: next
bulwahn@33649: assume "rtrancl_tab r [] x y"
bulwahn@33649: then obtain xs where "rtrancl_path r x xs y"
bulwahn@33649: by (rule rtrancl_tab_imp_rtrancl_path)
bulwahn@33649: then show "r\<^sup>*\<^sup>* x y"
bulwahn@33649: by (auto simp add: rtranclp_eq_rtrancl_path)
bulwahn@33649: qed
bulwahn@33649:
bulwahn@46359: declare rtranclp_rtrancl_eq[code del]
bulwahn@33649: declare rtranclp_eq_rtrancl_tab_nil[THEN iffD2, code_pred_intro]
bulwahn@33649:
nipkow@44890: code_pred rtranclp using rtranclp_eq_rtrancl_tab_nil [THEN iffD1] by fastforce
bulwahn@33649:
bulwahn@33649: subsection {* A simple example *}
bulwahn@33649:
bulwahn@33649: datatype ty = A | B | C
bulwahn@33649:
bulwahn@33649: inductive test :: "ty \ ty \ bool"
bulwahn@33649: where
bulwahn@33649: "test A B"
bulwahn@33649: | "test B A"
bulwahn@33649: | "test B C"
bulwahn@33649:
bulwahn@33649: subsubsection {* Invoking with the predicate compiler and the generic code generator *}
bulwahn@33649:
bulwahn@33649: code_pred test .
bulwahn@33649:
bulwahn@33649: values "{x. test\<^sup>*\<^sup>* A C}"
bulwahn@33649: values "{x. test\<^sup>*\<^sup>* C A}"
bulwahn@33649: values "{x. test\<^sup>*\<^sup>* A x}"
bulwahn@33649: values "{x. test\<^sup>*\<^sup>* x C}"
bulwahn@33649:
bulwahn@33870: value "test\<^sup>*\<^sup>* A C"
bulwahn@33870: value "test\<^sup>*\<^sup>* C A"
bulwahn@33870:
wenzelm@36176: hide_type ty
wenzelm@36176: hide_const test A B C
bulwahn@33649:
bulwahn@46359: end