(* 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 ‹Accessing Values via Keys› theory RBT_Map_Set_Extension imports Collections.RBTMapImpl Collections.RBTSetImpl Matrix.Utility begin text ‹ We provide two extensions of the red black tree implementation. The first extension provides two convenience methods on sets which are represented by red black trees: a check on subsets and the big union operator. The second extension is to provide two operations @{term elem_list_to_rm} and @{term rm_set_lookup} which can be used to index a set of values via keys. More precisely, given a list of values of type @{typ "'v"} and a key function of type @{typ "'v => 'k"}, @{term elem_list_to_rm} will generate a map of type @{typ "'k => 'v set"}. Then with @{term rs_set_lookup} we can efficiently access all values which match a given key. › subsection ‹Subset and Union› text ‹ For the subset operation @{term "r ⊆ s"} we provide two implementations. The first one (@{term rs_subset}) traverses over @{term r} and then performs membership tests ‹∈ s›. Its complexity is ${\cal O}(|r| \cdot log (|s|))$. The second one (@{term rs_subset_list}) generates sorted lists for both @{term r} and @{term s} and then linearly checks the subset condition. Its complexity is ${\cal O}(|r| + |s|)$. › text ‹ As union operator we use the standard fold function. Note that the order of the union is important so that new sets are added to the big union. › (* perhaps there is a smarter way to use two iterates at the same time, however, when writing this theory this feature was not detected in the RBTSetImpl theory *) definition rs_subset :: "('a :: linorder) rs ⇒ 'a rs ⇒ 'a option" where "rs_subset as bs = rs.iteratei as (λ maybe. case maybe of None ⇒ True | Some _ ⇒ False) (λ a _. if rs.memb a bs then None else Some a) None" lemma rs_subset [simp]: "rs_subset as bs = None ⟷ rs.α as ⊆ rs.α bs" proof - let ?abort = "λ maybe. case maybe of None ⇒ True | Some _ ⇒ False" let ?I = "λ aas maybe. maybe = None ⟷ (∀ a. a ∈ rs.α as - aas ⟶ a ∈ rs.α bs)" let ?it = "rs_subset as bs" have "?I {} ?it ∨ (∃ it ⊆ rs.α as. it ≠ {} ∧ ¬ ?abort ?it ∧ ?I it ?it)" unfolding rs_subset_def by (rule rs.iteratei_rule_P [where I="?I"]) (auto simp: rs.correct) then show ?thesis by auto qed definition rs_subset_list :: "('a :: linorder) rs ⇒ 'a rs ⇒ 'a option" where "rs_subset_list as bs = sorted_list_subset (rs.to_sorted_list as) (rs.to_sorted_list bs)" lemma rs_subset_list [simp]: "rs_subset_list as bs = None ⟷ rs.α as ⊆ rs.α bs" unfolding rs_subset_list_def sorted_list_subset[OF rs.to_sorted_list_correct(3)[OF rs.invar, of as] rs.to_sorted_list_correct(3)[OF rs.invar, of bs]] by (simp add: rs.to_sorted_list_correct) definition rs_Union :: "('q :: linorder) rs list ⇒ 'q rs" where "rs_Union = foldl rs.union (rs.empty ())" lemma rs_Union [simp]: "rs.α (rs_Union qs) = ⋃ (rs.α ` set qs)" proof - { fix start have "rs.α (foldl rs.union start qs) = rs.α start ∪ ⋃ (rs.α ` set qs)" by (induct qs arbitrary: start, auto simp: rs.correct) } from this[of "rs.empty ()"] show ?thesis unfolding rs_Union_def by (auto simp: rs.correct) qed subsection ‹Grouping Values via Keys› text ‹ The functions to produce the index (@{term elem_list_to_rm}) and the lookup function (@{term rm_set_lookup}) are straight-forward, however it requires some tedious reasoning that they perform as they should. › fun elem_list_to_rm :: "('d ⇒ 'k :: linorder) ⇒ 'd list ⇒ ('k, 'd list) rm" where "elem_list_to_rm key [] = rm.empty ()" | "elem_list_to_rm key (d # ds) = (let rm = elem_list_to_rm key ds; k = key d in (case rm.α rm k of None ⇒ rm.update_dj k [d] rm | Some data ⇒ rm.update k (d # data) rm))" definition "rm_set_lookup rm = (λ a. (case rm.α rm a of None ⇒ [] | Some rules ⇒ rules))" lemma rm_to_list_empty [simp]: "rm.to_list (rm.empty ()) = []" proof - have "map_of (rm.to_list (rm.empty ())) = Map.empty" by (simp add: rm.correct) moreover have map_of_empty_iff: "⋀l. map_of l = Map.empty ⟷ l = []" by (case_tac l) auto ultimately show ?thesis by metis qed locale rm_set = fixes rm :: "('k :: linorder, 'd list) rm" and key :: "'d ⇒ 'k" and data :: "'d set" assumes rm_set_lookup: "⋀ k. set (rm_set_lookup rm k) = {d ∈ data. key d = k}" begin lemma data_lookup: "data = ⋃ {set (rm_set_lookup rm k) | k. True}" (is "_ = ?R") proof - { fix d assume d: "d ∈ data" then have d: "d ∈ {d' ∈ data. key d' = key d}" by auto have "d ∈ ?R" by (rule UnionI[OF _ d], rule CollectI, rule exI[of _ "key d"], unfold rm_set_lookup[of "key d"], simp) } moreover { fix d assume "d ∈ ?R" from this[unfolded rm_set_lookup] have "d ∈ data" by auto } ultimately show ?thesis by blast qed lemma finite_data: "finite data" unfolding data_lookup proof show "finite {set (rm_set_lookup rm k) | k. True}" (is "finite ?L") proof - let ?rmset = "rm.α rm" let ?M = "?rmset ` Map.dom ?rmset" let ?N = "((λ e. set (case e of None ⇒ [] | Some ds ⇒ ds)) ` ?M)" let ?K = "?N ∪ {{}}" from rm.finite[of rm] have fin: "finite ?K" by auto show ?thesis proof (rule finite_subset[OF _ fin], rule) fix ds assume "ds ∈ ?L" from this[unfolded rm_set_lookup_def] obtain fn where ds: "ds = set (case rm.α rm fn of None ⇒ [] | Some ds ⇒ ds)" by auto show "ds ∈ ?K" proof (cases "rm.α rm fn") case None then show ?thesis unfolding ds by auto next case (Some rules) from Some have fn: "fn ∈ Map.dom ?rmset" by auto have "ds ∈ ?N" unfolding ds by (rule, rule refl, rule, rule refl, rule fn) then show ?thesis by auto qed qed qed qed (force simp: rm_set_lookup_def) end interpretation elem_list_to_rm: rm_set "elem_list_to_rm key ds" key "set ds" proof fix k show "set (rm_set_lookup (elem_list_to_rm key ds) k) = {d ∈ set ds. key d = k}" proof (induct ds arbitrary: k) case Nil then show ?case unfolding rm_set_lookup_def by (simp add: rm.correct) next case (Cons d ds k) let ?el = "elem_list_to_rm key" let ?l = "λk ds. set (rm_set_lookup (?el ds) k)" let ?r = "λk ds. {d ∈ set ds. key d = k}" from Cons have ind: "⋀ k. ?l k ds = ?r k ds" by auto show "?l k (d # ds) = ?r k (d # ds)" proof (cases "rm.α (?el ds) (key d)") case None from None ind[of "key d"] have r: "{da ∈ set ds. key da = key d} = {}" unfolding rm_set_lookup_def by auto from None have el: "?el (d # ds) = rm.update_dj (key d) [d] (?el ds)" by simp from None have ndom: "key d ∉ Map.dom (rm.α (?el ds))" by auto have r: "?r k (d # ds) = ?r k ds ∩ {da. key da ≠ key d} ∪ {da . key da = k ∧ da = d}" (is "_ = ?r1 ∪ ?r2") using r by auto from ndom have l: "?l k (d # ds) = set (case ((rm.α (elem_list_to_rm key ds))(key d ↦ [d])) k of None ⇒ [] | Some rules ⇒ rules)" (is "_ = ?l") unfolding el rm_set_lookup_def by (simp add: rm.correct) { fix da assume "da ∈ ?r1 ∪ ?r2" then have "da ∈ ?l" proof assume "da ∈ ?r2" then have da: "da = d" and k: "key d = k" by auto show ?thesis unfolding da k by auto next assume "da ∈ ?r1" from this[unfolded ind[symmetric] rm_set_lookup_def] obtain das where rm: "rm.α (?el ds) k = Some das" and da: "da ∈ set das" and k: "key da ≠ key d" by (cases "rm.α (?el ds) k", auto) from ind[of k, unfolded rm_set_lookup_def] rm da k have k: "key d ≠ k" by auto have rm: "((rm.α (elem_list_to_rm key ds))(key d ↦ [d])) k = Some das" unfolding rm[symmetric] using k by auto show ?thesis unfolding rm using da by auto qed } moreover { fix da assume l: "da ∈ ?l" let ?rm = "((rm.α (elem_list_to_rm key ds))(key d ↦ [d])) k" from l obtain das where rm: "?rm = Some das" and da: "da ∈ set das" by (cases ?rm, auto) have "da ∈ ?r1 ∪ ?r2" proof (cases "k = key d") case True with rm da have da: "da = d" by auto then show ?thesis using True by auto next case False with rm have "rm.α (?el ds) k = Some das" by auto from ind[of k, unfolded rm_set_lookup_def this] da False show ?thesis by auto qed } ultimately have "?l = ?r1 ∪ ?r2" by blast then show ?thesis unfolding l r . next case (Some das) from Some ind[of "key d"] have das: "{da ∈ set ds. key da = key d} = set das" unfolding rm_set_lookup_def by auto from Some have el: "?el (d # ds) = rm.update (key d) (d # das) (?el ds)" by simp from Some have dom: "key d ∈ Map.dom (rm.α (?el ds))" by auto from dom have l: "?l k (d # ds) = set (case ((rm.α (elem_list_to_rm key ds))(key d ↦ (d # das))) k of None ⇒ [] | Some rules ⇒ rules)" (is "_ = ?l") unfolding el rm_set_lookup_def by (simp add: rm.correct) have r: "?r k (d # ds) = ?r k ds ∪ {da. key da = k ∧ da = d}" (is "_ = ?r1 ∪ ?r2") by auto { fix da assume "da ∈ ?r1 ∪ ?r2" then have "da ∈ ?l" proof assume "da ∈ ?r2" then have da: "da = d" and k: "key d = k" by auto show ?thesis unfolding da k by auto next assume "da ∈ ?r1" from this[unfolded ind[symmetric] rm_set_lookup_def] obtain das' where rm: "rm.α (?el ds) k = Some das'" and da: "da ∈ set das'" by (cases "rm.α (?el ds) k", auto) from ind[of k, unfolded rm_set_lookup_def rm] have das': "set das' = {d ∈ set ds. key d = k}" by auto show ?thesis proof (cases "k = key d") case True show ?thesis using das' das da unfolding True by simp next case False then show ?thesis using das' da rm by auto qed qed } moreover { fix da assume l: "da ∈ ?l" let ?rm = "((rm.α (elem_list_to_rm key ds))(key d ↦ d # das)) k" from l obtain das' where rm: "?rm = Some das'" and da: "da ∈ set das'" by (cases ?rm, auto) have "da ∈ ?r1 ∪ ?r2" proof (cases "k = key d") case True with rm da das have da: "da ∈ set (d # das)" by auto then have "da = d ∨ da ∈ set das" by auto then have k: "key da = k" proof assume "da = d" then show ?thesis using True by simp next assume "da ∈ set das" with das True show ?thesis by auto qed from da k show ?thesis using das by auto next case False with rm have "rm.α (?el ds) k = Some das'" by auto from ind[of k, unfolded rm_set_lookup_def this] da False show ?thesis by auto qed } ultimately have "?l = ?r1 ∪ ?r2" by blast then show ?thesis unfolding l r . qed qed qed end