Theory Transitive-Closure.Transitive_Closure_List_Impl
section ‹Closure Computation using Lists›
theory Transitive_Closure_List_Impl
imports Transitive_Closure_Impl
begin
text ‹
We provide two algorithms for the computation of the reflexive transitive closure which internally
work on lists. The first one (@{term rtrancl_list_impl}) computes the closure on demand for a
given set of initial states. The second one (@{term memo_list_rtrancl}) precomputes the closure
for each individual state, stores the result, and then only does a look-up.
For the transitive closure there are the corresponding algorithms @{term trancl_list_impl} and
@{term memo_list_trancl}.
›
subsection ‹Computing Closures from Sets On-The-Fly›
text ‹
The algorithms are based on the generic algorithms @{const rtrancl_impl} and @{const trancl_impl}
instantiated by list operations. Here, after computing the successors in a straightforward way,
we use @{const remdups} to not have duplicates in the results. Moreover, also in the union
operation we filter to those elements that have not yet been seen. The use of @{const filter} in
the union operation is preferred over @{const remdups} since by construction the latter set will
not contain duplicates.
›
definition rtrancl_list_impl :: "('a × 'a) list ⇒ 'a list ⇒ 'a list"
where
"rtrancl_list_impl = rtrancl_impl
(λ r as. remdups (map snd (filter (λ (a, b). a ∈ set as) r)))
(λ xs ys. (filter (λ x. x ∉ set ys) xs) @ ys)
(λ x xs. x ∈ set xs)
[]"
definition trancl_list_impl :: "('a × 'a) list ⇒ 'a list ⇒ 'a list"
where
"trancl_list_impl = trancl_impl
(λ r as. remdups (map snd (filter (λ (a, b). a ∈ set as) r)))
(λ xs ys. (filter (λ x. x ∉ set ys) xs) @ ys)
(λ x xs. x ∈ set xs)
[]"
lemma rtrancl_list_impl:
"set (rtrancl_list_impl r as) = {b. ∃ a ∈ set as. (a, b) ∈ (set r)⇧*}"
unfolding rtrancl_list_impl_def
by (rule set_access_gen.rtrancl_impl, unfold_locales, force+)
lemma trancl_list_impl:
"set (trancl_list_impl r as) = {b. ∃ a ∈ set as. (a, b) ∈ (set r)⇧+}"
unfolding trancl_list_impl_def
by (rule set_access_gen.trancl_impl, unfold_locales, force+)
subsection ‹Precomputing Closures for Single States›
text ‹
Storing all relevant entries is done by mapping all left-hand sides of the relation to their
closure. To avoid redundant entries, @{const remdups} is used.
›
definition memo_list_rtrancl :: "('a × 'a) list ⇒ ('a ⇒ 'a list)"
where
"memo_list_rtrancl r =
(let
tr = rtrancl_list_impl r;
rm = map (λa. (a, tr [a])) ((remdups ∘ map fst) r)
in
(λa. case map_of rm a of
None ⇒ [a]
| Some as ⇒ as))"
lemma memo_list_rtrancl:
"set (memo_list_rtrancl r a) = {b. (a, b) ∈ (set r)⇧*}" (is "?l = ?r")
proof -
let ?rm = "map (λ a. (a, rtrancl_list_impl r [a])) ((remdups ∘ map fst) r)"
show ?thesis
proof (cases "map_of ?rm a")
case None
have one: "?l = {a}"
unfolding memo_list_rtrancl_def Let_def None
by auto
from None [unfolded map_of_eq_None_iff]
have a: "a ∉ fst ` set r" by force
{
fix b
assume "b ∈ ?r"
from this [unfolded rtrancl_power relpow_fun_conv] obtain n f where
ab: "f 0 = a ∧ f n = b" and steps: "⋀ i. i < n ⟹ (f i, f (Suc i)) ∈ set r" by auto
from ab steps [of 0] a have "a = b"
by (cases n, force+)
}
then have "?r = {a}" by auto
then show ?thesis unfolding one by simp
next
case (Some as)
have as: "set as = {b. (a, b) ∈ (set r)^*}"
using map_of_SomeD [OF Some]
rtrancl_list_impl [of r "[a]"] by force
then show ?thesis unfolding memo_list_rtrancl_def Let_def Some by simp
qed
qed
definition memo_list_trancl :: "('a × 'a) list ⇒ ('a ⇒ 'a list)"
where
"memo_list_trancl r =
(let
tr = trancl_list_impl r;
rm = map (λa. (a, tr [a])) ((remdups ∘ map fst) r)
in
(λa. case map_of rm a of
None ⇒ []
| Some as ⇒ as))"
lemma memo_list_trancl:
"set (memo_list_trancl r a) = {b. (a, b) ∈ (set r)⇧+}" (is "?l = ?r")
proof -
let ?rm = "map (λ a. (a, trancl_list_impl r [a])) ((remdups ∘ map fst) r)"
show ?thesis
proof (cases "map_of ?rm a")
case None
have one: "?l = {}"
unfolding memo_list_trancl_def Let_def None
by auto
from None [unfolded map_of_eq_None_iff]
have a: "a ∉ fst ` set r" by force
{
fix b
assume "b ∈ ?r"
from this [unfolded trancl_unfold_left] a have False by force
}
then have "?r = {}" by auto
then show ?thesis unfolding one by simp
next
case (Some as)
have as: "set as = {b. (a, b) ∈ (set r)⇧+}"
using map_of_SomeD [OF Some]
trancl_list_impl[of r "[a]"] by force
then show ?thesis unfolding memo_list_trancl_def Let_def Some by simp
qed
qed
end