Theory Transitive_Closure_RBT_Impl
section ‹Closure Computation via Red Black Trees›
theory Transitive_Closure_RBT_Impl
imports
Transitive_Closure_Impl
RBT_Map_Set_Extension
begin
text ‹
We provide two algorithms to compute the reflexive transitive closure which internally work on red
black trees. Therefore, the carrier has to be linear ordered. The first one (@{term
rtrancl_rbt_impl}) computes the closure on demand for a given set of initial states. The second
one (@{term memo_rbt_rtrancl}) precomputes the closure for each individual state, stores the
results, and then only does a look-up.
For the transitive closure there are the corresponding algorithms @{term trancl_rbt_impl} and
@{term memo_rbt_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}
using red black trees. To compute the successors efficiently, all successors of a state are
collected and stored in a red black tree map by using @{const elem_list_to_rm}. Then, to lift the
successor relation for single states to lists of states, all results are united using @{const
rs_Union}. The rest is standard.
›
interpretation set_access "λ as bs. rs.union bs (rs.from_list as)" rs.α rs.memb "rs.empty ()"
by (unfold_locales, auto simp: rs.correct)
abbreviation rm_succ :: "('a :: linorder × 'a) list ⇒ 'a list ⇒ 'a list"
where
"rm_succ ≡ (λ r. let rm = elem_list_to_rm fst r in
(λ as. rs.to_list (rs_Union (map (λ a. rs.from_list (map snd (rm_set_lookup rm a))) as))))"
definition rtrancl_rbt_impl :: "('a :: linorder × 'a) list ⇒ 'a list ⇒ 'a rs"
where
"rtrancl_rbt_impl = rtrancl_impl rm_succ
(λ as bs. rs.union bs (rs.from_list as)) rs.memb (rs.empty ())"
definition trancl_rbt_impl :: "('a :: linorder × 'a) list ⇒ 'a list ⇒ 'a rs"
where
"trancl_rbt_impl = trancl_impl rm_succ
(λ as bs. rs.union bs (rs.from_list as)) rs.memb (rs.empty ())"
lemma rtrancl_rbt_impl:
"rs.α (rtrancl_rbt_impl r as) = {b. ∃ a ∈ set as. (a,b) ∈ (set r)⇧*}"
unfolding rtrancl_rbt_impl_def
by (rule set_access_gen.rtrancl_impl, unfold_locales, unfold Let_def, simp add: rs.correct elem_list_to_rm.rm_set_lookup, force)
lemma trancl_rbt_impl:
"rs.α (trancl_rbt_impl r as) = {b. ∃ a ∈ set as. (a,b) ∈ (set r)⇧+}"
unfolding trancl_rbt_impl_def
by (rule set_access_gen.trancl_impl, unfold_locales, unfold Let_def, simp add: rs.correct elem_list_to_rm.rm_set_lookup, 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. Since we assume a linear order on the carrier, for the lookup we can use maps that are
implemented as red black trees.
›
definition memo_rbt_rtrancl :: "('a :: linorder × 'a) list ⇒ ('a ⇒ 'a rs)"
where
"memo_rbt_rtrancl r =
(let
tr = rtrancl_rbt_impl r;
rm = rm.to_map (map (λ a. (a, tr [a])) ((rs.to_list ∘ rs.from_list ∘ map fst) r))
in
(λa. case rm.lookup a rm of
None ⇒ rs.from_list [a]
| Some as ⇒ as))"
lemma memo_rbt_rtrancl:
"rs.α (memo_rbt_rtrancl r a) = {b. (a, b) ∈ (set r)⇧*}" (is "?l = ?r")
proof -
let ?rm = "rm.to_map
(map (λa. (a, rtrancl_rbt_impl r [a])) ((rs.to_list ∘ rs.from_list ∘ map fst) r))"
show ?thesis
proof (cases "rm.lookup a ?rm")
case None
have one: "?l = {a}"
unfolding memo_rbt_rtrancl_def Let_def None
by (simp add: rs.correct)
from None [unfolded rm.lookup_correct [OF rm.invar], simplified rm.correct map_of_eq_None_iff]
have a: "a ∉ fst ` set r" by (simp add: rs.correct, 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 "b = a"
by (cases n, force+)
}
then have "?r = {a}" by auto
then show ?thesis unfolding one by simp
next
case (Some as)
have as: "rs.α as = {b. (a,b) ∈ (set r)⇧*}"
using map_of_SomeD [OF Some [unfolded rm.lookup_correct [OF rm.invar], simplified rm.correct]]
rtrancl_rbt_impl [of r "[a]"] by force
then show ?thesis unfolding memo_rbt_rtrancl_def Let_def Some by simp
qed
qed
definition memo_rbt_trancl :: "('a :: linorder × 'a) list ⇒ ('a ⇒ 'a rs)"
where
"memo_rbt_trancl r =
(let
tr = trancl_rbt_impl r;
rm = rm.to_map (map (λ a. (a, tr [a])) ((rs.to_list ∘ rs.from_list ∘ map fst) r))
in (λ a.
(case rm.lookup a rm of
None ⇒ rs.empty ()
| Some as ⇒ as)))"
lemma memo_rbt_trancl:
"rs.α (memo_rbt_trancl r a) = {b. (a, b) ∈ (set r)⇧+}" (is "?l = ?r")
proof -
let ?rm = "rm.to_map
(map (λ a. (a, trancl_rbt_impl r [a])) ((rs.to_list ∘ rs.from_list ∘ map fst) r))"
show ?thesis
proof (cases "rm.lookup a ?rm")
case None
have one: "?l = {}"
unfolding memo_rbt_trancl_def Let_def None
by (simp add: rs.correct)
from None [unfolded rm.lookup_correct [OF rm.invar], simplified rm.correct map_of_eq_None_iff]
have a: "a ∉ fst ` set r" by (simp add: rs.correct, 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: "rs.α as = {b. (a,b) ∈ (set r)⇧+}"
using map_of_SomeD [OF Some [unfolded rm.lookup_correct [OF rm.invar], simplified rm.correct]]
trancl_rbt_impl [of r "[a]"] by force
then show ?thesis unfolding memo_rbt_trancl_def Let_def Some by simp
qed
qed
end