(* Author: Stefan Berghofer, Lukas Bulwahn, TU Muenchen *)
section \A table-based implementation of the reflexive transitive closure\
theory Transitive_Closure_Table
imports Main
begin
inductive rtrancl_path :: "('a \ 'a \ bool) \ 'a \ 'a list \ 'a \ bool"
for r :: "'a \ 'a \ bool"
where
base: "rtrancl_path r x [] x"
| step: "r x y \ rtrancl_path r y ys z \ rtrancl_path r x (y # ys) z"
lemma rtranclp_eq_rtrancl_path: "r\<^sup>*\<^sup>* x y \ (\xs. rtrancl_path r x xs y)"
proof
show "\xs. rtrancl_path r x xs y" if "r\<^sup>*\<^sup>* x y"
using that
proof (induct rule: converse_rtranclp_induct)
case base
have "rtrancl_path r y [] y" by (rule rtrancl_path.base)
then show ?case ..
next
case (step x z)
from \\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
show "r\<^sup>*\<^sup>* x y" if "\xs. rtrancl_path r x xs y"
proof -
from that obtain xs where "rtrancl_path r x xs y" ..
then show ?thesis
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
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 "\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 \ 'a \ bool) \ 'a list \ 'a \ 'a \ bool"
for r :: "'a \ 'a \ bool"
where
base: "rtrancl_tab r xs x x"
| step: "x \ set xs \ r x y \ rtrancl_tab r (x # xs) y z \ 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} \ set xs) \ 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 \ set ys"
by auto
from step have "distinct (y # zs)"
by simp
moreover from step have "({y} \ set zs) \ set (x # ys) = {}"
by auto
ultimately have "rtrancl_tab r (x # ys) y z"
by (rule step)
with \x \ 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
show "rtrancl_tab r [] x y" if "r\<^sup>*\<^sup>* x y"
proof -
from that 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} \ set xs') \ set [] = {}"
by simp
with xs' distinct show ?thesis
by (rule rtrancl_path_imp_rtrancl_tab)
qed
show "r\<^sup>*\<^sup>* x y" if "rtrancl_tab r [] x y"
proof -
from that obtain xs where "rtrancl_path r x xs y"
by (rule rtrancl_tab_imp_rtrancl_path)
then show ?thesis
by (auto simp add: rtranclp_eq_rtrancl_path)
qed
qed
declare rtranclp_rtrancl_eq [code del]
declare rtranclp_eq_rtrancl_tab_nil [THEN iffD2, code_pred_intro]
code_pred rtranclp
using rtranclp_eq_rtrancl_tab_nil [THEN iffD1] by fastforce
end