(* 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 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