Theory Transitive-Closure.RBT_Map_Set_Extension

(*  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
  "HOL-Library.RBT"
  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 an implementation
  that generates
  sorted lists for both @{term r} and @{term s} and then linearly checks the subset condition.›

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.
›

definition RBT_is_key where "RBT_is_key a t = (RBT.lookup t a ≠ None)" 
definition RBT_from_list where "RBT_from_list as = RBT.bulkload (map (λ x. (x,())) as)" 
definition RBT_list_union where "RBT_list_union as bs = RBT.union bs (RBT_from_list as)" 
definition RBT_keys where "RBT_keys t = dom (RBT.lookup t)" 

lemma set_RBT_keys: "set (RBT.keys t) = RBT_keys t" 
  unfolding RBT_keys_def by (simp add: lookup_keys)

lemma RBT_from_list[simp]: "RBT_keys (RBT_from_list xs) = set xs" 
  "set (RBT.keys (RBT_from_list xs)) = set xs" 
proof -
  have "x ∈ set xs ⟹ map_of (map (λx. (x, ())) xs) x = Some ()" for x
    by (induct xs, auto)
  thus "RBT_keys (RBT_from_list xs) = set xs" unfolding lookup_union lookup_bulkload RBT_from_list_def RBT_keys_def
    by (auto dest: map_of_SomeD)
  thus "set (RBT.keys (RBT_from_list xs)) = set xs" by (simp add: set_RBT_keys)
qed

lemmas RBT_defs = RBT_is_key_def RBT_list_union_def RBT_keys_def

definition rs_subset :: "('a :: linorder,unit) RBT.rbt ⇒ ('a,unit) RBT.rbt ⇒ 'a option"
where
  "rs_subset as bs = sorted_list_subset (RBT.keys as) (RBT.keys bs)"

lemma rs_subset [simp]:
  "rs_subset as bs = None ⟷ RBT_keys as ⊆ RBT_keys bs"
  unfolding rs_subset_def
  apply (subst sorted_list_subset[OF RBT.sorted_keys RBT.sorted_keys]) 
  apply (unfold RBT_keys_def lookup_keys[symmetric])
  by auto
  
definition rs_Union :: "('q :: linorder, unit) RBT.rbt list ⇒ ('q,unit) RBT.rbt"
where
  "rs_Union = foldl RBT.union (RBT.empty)"

lemma rs_Union [simp]:
  "RBT_keys (rs_Union qs) = ⋃ (RBT_keys ` set qs)"
proof -
  { 
    fix start
    have "RBT_keys (foldl RBT.union start qs) = RBT_keys start ∪ ⋃ (RBT_keys ` set qs)"
      unfolding RBT_keys_def
      by (induct qs arbitrary: start, auto simp: RBT.lookup_union)
  } from this[of "RBT.empty"]
  show ?thesis unfolding rs_Union_def
    unfolding RBT_keys_def
    by auto
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) RBT.rbt "
where
  "elem_list_to_rm key [] = RBT.empty" |
  "elem_list_to_rm key (d # ds) =
    (let
      t = elem_list_to_rm key ds;
      k = key d
    in
      (case RBT.lookup t k of
        None ⇒ RBT.insert k [d] t
      | Some data ⇒ RBT.insert k (d # data) t))"

definition "rm_set_lookup rm = (λ a. (case RBT.lookup rm a of None ⇒ [] | Some rules ⇒ rules))"

locale rm_set = 
  fixes rm :: "('k :: linorder, 'd list) RBT.rbt"
    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 = "RBT.lookup rm"
    let ?M = "?rmset ` Map.dom ?rmset"
    let ?N = "((λ e. set (case e of None ⇒ [] | Some ds ⇒ ds)) ` ?M)"
    let ?K = "?N ∪ {{}}"
    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 RBT.lookup rm fn of None ⇒ []
          | Some ds ⇒ ds)" by auto
      show "ds ∈ ?K" 
      proof (cases "RBT.lookup 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
  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 "RBT.lookup (?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) = RBT.insert (key d) [d] (?el ds)"
        by simp
      from None have ndom: "key d ∉ Map.dom (RBT.lookup (?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 ((RBT.lookup (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
      {
        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: "RBT.lookup (?el ds) k = Some das" and da: "da ∈ set das" and k: "key da ≠ key d" 
            by (cases "RBT.lookup (?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: "((RBT.lookup (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 = "((RBT.lookup (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 "RBT.lookup (?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) = RBT.insert (key d) (d # das) (?el ds)"
        by simp
      from Some have dom: "key d ∈ Map.dom (RBT.lookup (?el ds))" by auto
      from dom have l: "?l k (d # ds) = 
        set (case ((RBT.lookup (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
      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: "RBT.lookup (?el ds) k = Some das'" and da: "da ∈ set das'" by (cases "RBT.lookup (?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 = "((RBT.lookup (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 "RBT.lookup (?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