Theory Transitive_Closure_Impl
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