Theory Transitive-Closure.Transitive_Closure_List_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 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