Theory Transitive-Closure.Transitive_Closure_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 ‹A Generic Work-List Algorithm›

theory Transitive_Closure_Impl
imports Main
begin

text ‹
  Let @{term R} be some finite relation. We start to present a standard work-list algorithm to
  compute all elements that are reachable from some initial set by at most @{term n} @{term
  R}-steps. Then, we obtain algorithms for the (reflexive) transitive closure from a given starting
  set by exploiting the fact that for finite relations we have to iterate at most @{term "card R"}
  times. The presented algorithms are generic in the sense that the underlying data structure can
  freely be chosen, you just have to provide certain operations like union, membership, etc.
›

subsection ‹Bounded Reachability›

text ‹
  We provide an algorithm relpow_impl› that computes all states that are reachable from an
  initial set of states @{term new} by at most @{term n} steps. The algorithm also stores a set of
  states that have already been visited @{term have}, and then show, do not have to be expanded a
  second time. The algorithm is parametric in the underlying data structure, it just requires
  operations for union and membership as well as a function to compute the successors of a list.
›
fun
  relpow_impl ::
    "('a list  'a list) 
      ('a list  'b  'b)  ('a  'b  bool)  'a list  'b  nat  'b"
where
  "relpow_impl succ un memb new have 0 = un new have" |
  "relpow_impl succ un memb new have (Suc m) =
    (if new = [] then have
    else
      let
        maybe = succ new;
        have' = un new have;
        new' = filter (λ n. ¬ memb n have') maybe
      in relpow_impl succ un memb new' have' m)"

text ‹
  We need to know that the provided operations behave correctly.
›

locale set_access =
  fixes un :: "'a list  'b  'b"
    and set_of :: "'b  'a set"
    and memb :: "'a  'b  bool"
    and empty :: 'b
  assumes un: "set_of (un as bs) = set as  set_of bs"
    and memb: "memb a bs  (a  set_of bs)"
    and empty: "set_of empty = {}"

locale set_access_succ = set_access un 
  for un :: "'a list  'b  'b" +
  fixes succ :: "'a list  'a list"
   and  rel :: "('a × 'a) set"
  assumes succ: "set (succ as) = {b.  a  set as. (a, b)  rel}"
begin

abbreviation "relpow_i  relpow_impl succ un memb"

text ‹
  What follows is the main technical result of the @{const relpow_impl} algorithm: what it computes
  for arbitrary values of @{term new} and @{term have}.
›

lemma relpow_impl_main: 
  "set_of (relpow_i new have n) = 
    {b | a b m. a  set new  m  n  (a, b)  (rel  {(a, b). b  set_of have}) ^^ m} 
    set_of have"
  (is "?l new have n = ?r new have n")
proof (induction n arbitrary: "have" new)
  case (Suc n hhave nnew)
  show ?case
  proof (cases "nnew = []")
    case True
    then show ?thesis by auto
  next
    case False
    let ?have = "set_of hhave"
    let ?new = "set nnew"
    obtain "have" new where hav: "have = ?have" and new: "new = ?new" by auto
    let ?reln = "λ m. (rel  {(a, b). b  new  b  have}) ^^  m"
    let ?rel = "λ m. (rel  {(a, b). b  have}) ^^  m"
    have idl: "?l nnew hhave (Suc n) = 
      {uu. a. (aa new. (aa,a)  rel)  a  new  a  have  (m  n. (a, uu)  ?reln m)} 
      (new  have)"
      (is "_ = ?l1  (?l2  ?l3)")
      by (simp add: hav new False Let_def Suc, simp add: memb un succ)
    let ?l = "?l1  (?l2  ?l3)"
    have idr: "?r nnew hhave (Suc n) = {b.  a m. a  new  m  Suc n  (a, b)  ?rel m}  have"
      (is "_ = (?r1  ?r2)") by (simp add: hav new)
    let ?r = "?r1  ?r2"
    {
      fix b
      assume b: "b  ?l"      
      have "b  ?r" 
      proof (cases "b  new  b  have")
        case True then show ?thesis 
        proof
          assume "b  have" then show ?thesis by auto
        next
          assume b: "b  new"
          have "b  ?r1"
            by (intro CollectI, rule exI, rule exI [of _ 0], intro conjI, rule b, auto)
          then show ?thesis by auto
        qed
      next
        case False
        with b have "b  ?l1" by auto
        then obtain a2 a1 m where a2n: "a2  new" and a2h: "a2  have" and a1: "a1  new"
          and a1a2: "(a1,a2)  rel" and m: "m  n" and a2b: "(a2,b)  ?reln m" by auto
        have "b  ?r1"
          by (rule CollectI, rule exI, rule exI [of _ "Suc m"], intro conjI, rule a1, simp add: m, rule relpow_Suc_I2, rule, rule a1a2, simp add: a2h, insert a2b, induct m arbitrary: a2 b, auto)
        then show ?thesis by auto
      qed
    }     
    moreover
    { 
      fix b
      assume b: "b  ?r"
      then have "b  ?l" 
      proof (cases "b  have")
        case True then show ?thesis by auto
      next
        case False
        with b have "b  ?r1" by auto
        then obtain a m where a: "a  new" and m: "m  Suc n" and ab: "(a, b)  ?rel m" by auto
        have seq: " a  new. (a, b)  ?rel m"
          using a  ab by auto
        obtain l where l: "l = (LEAST m. ( a  new. (a, b)  ?rel m))" by auto
        have least: "( a  new. (a, b)  ?rel l)"
          by (unfold l, rule LeastI, rule seq)
        have lm: "l  m" unfolding l
          by (rule Least_le, rule seq)
        with m have ln: "l  Suc n" by auto
        from least obtain a where a: "a  new"
          and ab: "(a, b)  ?rel l" by auto
        from ab [unfolded relpow_fun_conv]
        obtain f where fa: "f 0 = a" and fb: "b = f l"
          and steps: " i. i < l  (f i, f (Suc i))  ?rel 1" by auto
        {
          fix i
          assume i: "i < l"
          have main: "f (Suc i)  new" 
          proof
            assume new: "f (Suc i)  new"
            let ?f = "λ j. f (Suc i + j)"
            have seq: "(f (Suc i), b)  ?rel (l - Suc i)"
              unfolding relpow_fun_conv
            proof (rule exI[of _ ?f], intro conjI allI impI)
              from i show "f (Suc i + (l - Suc i)) = b"
                unfolding fb by auto
            next
              fix j
              assume "j < l - Suc i"
              then have small: "Suc i + j < l" by auto
              show "(?f j, ?f (Suc j))  rel  {(a, b). b  have}" using steps [OF small] by auto
            qed simp
            from i have small: "l - Suc i < l" by auto
            from seq new have " a  new. (a, b)  ?rel (l - Suc i)"  by auto
            with not_less_Least [OF small [unfolded l]]
            show False unfolding l by auto
          qed
          then have "(f i, f (Suc i))  ?reln 1"
            using steps [OF i] by auto
        } note steps = this
        have ab: "(a, b)  ?reln l" unfolding relpow_fun_conv
          by (intro exI conjI, insert fa fb steps, auto)
        have "b  ?l1  ?l2" 
        proof (cases l)
          case 0
          with ab a show ?thesis by auto
        next
          case (Suc ll)
          from relpow_Suc_D2 [OF ab [unfolded Suc]] a ln Suc 
          show ?thesis by auto
        qed
        then show ?thesis by auto
      qed
    }
    ultimately show ?thesis
      unfolding idl idr by blast
  qed
qed (simp add: un)

text ‹
  From the previous lemma we can directly derive that @{const relpow_impl} works correctly if @{term
  have} is initially set to empty›
lemma relpow_impl:
  "set_of (relpow_i new empty n) = {b | a b m. a  set new  m  n  (a, b)  rel ^^ m}" 
proof -
  have id: "rel  {(a ,b). True} = rel" by auto
  show ?thesis unfolding relpow_impl_main empty by (simp add: id)
qed

end


subsection ‹Reflexive Transitive Closure and Transitive closure›

text ‹
  Using @{const relpow_impl} it is now easy to obtain algorithms for the reflexive transitive
  closure and the transitive closure by restricting the number of steps to the size of the finite
  relation. Note that @{const relpow_impl} will abort the computation as soon as no new states are
  detected. Hence, there is no penalty in using this large bound.
›

definition
  rtrancl_impl ::
    "(('a × 'a) list  'a list  'a list) 
      ('a list  'b  'b)  ('a  'b  bool)  'b  ('a × 'a) list  'a list  'b"
where
  "rtrancl_impl gen_succ un memb emp rel =
    (let
      succ = gen_succ rel;
      n = length rel
    in (λ as. relpow_impl succ un memb as emp n))"

definition
  trancl_impl ::
    "(('a × 'a) list  'a list  'a list) 
      ('a list  'b  'b)  ('a  'b  bool)  'b  ('a × 'a) list  'a list  'b"
where
  "trancl_impl gen_succ un memb emp rel =
    (let
      succ = gen_succ rel;
      n = length rel
    in (λ as. relpow_impl succ un memb (succ as) emp n))"

text ‹
  The soundness of both @{const rtrancl_impl} and @{const trancl_impl} follows from the soundness of
  @{const relpow_impl} and the fact that for finite relations, we can limit the number of steps to
  explore all elements in the reflexive transitive closure.
›

lemma rtrancl_finite_relpow:
  "(a, b)  (set rel)*  ( n  length rel. (a, b)  set rel ^^ n)" (is "?l = ?r")
proof
  assume ?r
  then show ?l
    unfolding rtrancl_power by auto
next
  assume ?l
  from this [unfolded rtrancl_power]
    obtain n where ab: "(a,b)  set rel ^^ n" ..
  obtain l where l: "l = (LEAST n. (a,b)  set rel ^^ n)" by auto
  have ab: "(a, b)  set rel ^^ l" unfolding l
    by (intro LeastI, rule ab)
  from this [unfolded relpow_fun_conv]
  obtain f where a: "f 0 = a" and b: "f l = b"
    and steps: " i. i < l  (f i, f (Suc i))  set rel" by auto
  let ?hits = "map (λ i. f (Suc i)) [0 ..< l]"
  from steps have subset: "set ?hits  snd ` set rel" by force
  have "l  length rel"
  proof (cases "distinct ?hits")
    case True
    have "l = length ?hits" by simp
    also have "... = card (set ?hits)" unfolding distinct_card [OF True] ..
    also have "...  card (snd ` set rel)" by (rule card_mono [OF _ subset], auto)
    also have "... = card (set (map snd rel))" by auto
    also have "...  length (map snd rel)" by (rule card_length)
    finally  show ?thesis by simp
  next
    case False
    from this [unfolded distinct_conv_nth]
    obtain i j where i: "i < l" and j: "j < l" and ij: "i  j" and fij: "f (Suc i) = f (Suc j)" by auto
    let ?i = "min i j"
    let ?j = "max i j"
    have i: "?i < l" and j: "?j < l" and fij: "f (Suc ?i) = f (Suc ?j)" 
      and ij: "?i < ?j"
      using i j ij fij unfolding min_def max_def by (cases "i  j", auto)
    from i j fij ij obtain i j where i: "i < l" and j: "j < l" and ij: "i < j" and fij: "f (Suc i) = f (Suc j)" by blast
    let ?g = "λ n. if n  i then f n else f (n + (j - i))"
    let ?l = "l - (j - i)"
    have abl: "(a,b)  set rel ^^ ?l"
      unfolding relpow_fun_conv
    proof (rule exI [of _ ?g], intro conjI impI allI)
      show "?g ?l = b" unfolding b [symmetric] using j ij by auto
    next
      fix k
      assume k: "k < ?l"
      show "(?g k, ?g (Suc k))  set rel" 
      proof (cases "k < i")
        case True
        with i have "k < l" by auto
        from steps [OF this] show ?thesis using True by simp
      next
        case False
        then have ik: "i  k" by auto
        show ?thesis
        proof (cases "k = i")
          case True
          then show ?thesis using ij fij steps [OF i] by simp
        next
          case False
          with ik have ik: "i < k" by auto
          then have small: "k + (j - i) < l" using k by auto
          show ?thesis using steps[OF small] ik by auto
        qed
      qed
    qed (simp add: a)
    from ij i have ll: "?l < l" by auto
    have "l  ?l" unfolding l
      by (rule Least_le, rule abl [unfolded l])
    with ll have False by simp
    then show ?thesis by simp
  qed
  with ab show ?r by auto
qed

locale set_access_gen = set_access un
  for un :: "'a list  'b  'b" +
  fixes gen_succ :: "('a × 'a) list  'a list  'a list"
  assumes gen_succ: "set (gen_succ rel as) = {b.  a  set as. (a, b)  set rel}"
begin

abbreviation "rtrancl_i  rtrancl_impl gen_succ un memb empty"
abbreviation "trancl_i  trancl_impl gen_succ un memb empty"

lemma rtrancl_impl:
  "set_of (rtrancl_i rel as) = {b. ( a  set as. (a, b)  (set rel)*)}"
proof -
  interpret set_access_succ set_of memb empty un "gen_succ rel" "set rel"
    by (unfold_locales, insert gen_succ, auto)
  show ?thesis unfolding rtrancl_impl_def Let_def relpow_impl
    by (auto simp: rtrancl_finite_relpow)
qed

lemma trancl_impl:
  "set_of (trancl_i rel as) = {b. ( a  set as. (a, b)  (set rel)+)}"
proof -
  interpret set_access_succ set_of memb empty un "gen_succ rel" "set rel"
    by (unfold_locales, insert gen_succ, auto)
  show ?thesis
    unfolding trancl_impl_def Let_def relpow_impl trancl_unfold_left relcomp_unfold rtrancl_finite_relpow succ by auto
qed

end

end