(* Title: Executable Transitive Closures of Finite Relations Author: Christian Sternagel <c.sternagel@gmail.com> René Thiemann <rene.thiemann@uibk.ac.at> Maintainer: Christian Sternagel and René Thiemann License: LGPL *) 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