Theory Transitive_Closure_RBT_Impl

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