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