Theory Tarjan_LowLink
section ‹Invariants for Tarjan's Algorithm›
theory Tarjan_LowLink
imports
"../DFS_Framework"
"../Invars/DFS_Invars_SCC"
begin
context param_DFS_defs begin
definition
"lowlink_path s v p w ≡ path E v p w ∧ p ≠ []
∧ (last p, w) ∈ cross_edges s ∪ back_edges s
∧ (length p > 1 ⟶
p!1 ∈ dom (finished s)
∧ (∀k < length p - 1. (p!k, p!Suc k) ∈ tree_edges s))"
definition
"lowlink_set s v ≡ {w ∈ dom (discovered s).
v = w
∨ (v,w) ∈ E⇧+ ∧ (w,v) ∈ E⇧+
∧ (∃p. lowlink_path s v p w)}"
context begin interpretation timing_syntax .
abbreviation LowLink where
"LowLink s v ≡ Min (δ s ` lowlink_set s v)"
end
end
context DFS_invar begin
lemma lowlink_setI:
assumes "lowlink_path s v p w"
and "w ∈ dom (discovered s)"
and "(v,w) ∈ E⇧*" "(w,v) ∈ E⇧*"
shows "w ∈ lowlink_set s v"
proof (cases "v = w")
case True thus ?thesis by (simp add: lowlink_set_def assms)
next
case False with assms have "(v,w) ∈ E⇧+" "(w,v) ∈ E⇧+" by (metis rtrancl_eq_or_trancl)+
with assms show ?thesis by (auto simp add: lowlink_set_def)
qed
lemma lowlink_set_discovered:
"lowlink_set s v ⊆ dom (discovered s)"
unfolding lowlink_set_def
by blast
lemma lowlink_set_finite[simp, intro!]:
"finite (lowlink_set s v)"
using lowlink_set_discovered discovered_finite
by (metis finite_subset)
lemma lowlink_set_not_empty:
assumes "v ∈ dom (discovered s)"
shows "lowlink_set s v ≠ {}"
unfolding lowlink_set_def
using assms by auto
lemma lowlink_path_single:
assumes "(v,w) ∈ cross_edges s ∪ back_edges s"
shows "lowlink_path s v [v] w"
unfolding lowlink_path_def
using assms cross_edges_ssE back_edges_ssE
by (auto simp add: path_simps)
lemma lowlink_path_Cons:
assumes "lowlink_path s v (x#xs) w"
and "xs ≠ []"
shows "∃u. lowlink_path s u xs w"
proof -
from assms have path: "path E v (x#xs) w"
and cb: "(last xs, w) ∈ cross_edges s ∪ back_edges s"
and f: "(x#xs)!1 ∈ dom (finished s)"
and t: "(∀k < length xs. ((x#xs)!k, (x#xs)!Suc k) ∈ tree_edges s)"
unfolding lowlink_path_def
by auto
from path obtain u where "path E u xs w" by (auto simp add: path_simps)
moreover note cb ‹xs ≠ []›
moreover { fix k define k' where "k' = Suc k"
assume "k < length xs - 1"
with k'_def have "k' < length xs" by simp
with t have "((x#xs)!k', (x#xs)!Suc k') ∈ tree_edges s" by simp
hence "(xs!k,xs!Suc k) ∈ tree_edges s" by (simp add: k'_def nth_Cons')
} note t' = this
moreover {
assume *: "length xs > 1"
from f have "xs!0 ∈ dom (finished s)" by auto
moreover from t'[of 0] * have "(xs!0,xs!1) ∈ tree_edges s" by simp
ultimately have "xs!1 ∈ dom (finished s)" using tree_edge_impl_parenthesis by metis
}
ultimately have "lowlink_path s u xs w" by (auto simp add: lowlink_path_def)
thus ?thesis ..
qed
lemma lowlink_path_in_tree:
assumes p: "lowlink_path s v p w"
and j: "j < length p"
and k: "k < j"
shows "(p!k, p!j) ∈ (tree_edges s)⇧+"
proof -
from p have "p ≠ []" by (auto simp add: lowlink_path_def)
thus ?thesis using p j k
proof (induction arbitrary: v j k rule: list_nonempty_induct)
case single thus ?case by auto
next
case (cons x xs)
define j' where "j' = j - 1"
with cons have j'_le: "j' < length xs" and "k ≤ j'" and j: "j = Suc j'" by auto
from cons lowlink_path_Cons obtain u where p: "lowlink_path s u xs w" by blast
show ?case
proof (cases "k=0")
case True
from cons have "⋀k. k < length (x#xs) - 1 ⟹ ((x#xs)!k,(x#xs)!Suc k) ∈ tree_edges s"
unfolding lowlink_path_def
by auto
moreover from True cons have "k < length (x#xs) - 1" by auto
ultimately have *: "((x#xs)!k,(x#xs)!Suc k) ∈ tree_edges s" by metis
show ?thesis
proof (cases "j' = 0")
case True with * j ‹k=0› show ?thesis by simp
next
case False with True have "j' > k" by simp
with cons.IH[OF p j'_le] have "(xs!k, xs!j') ∈ (tree_edges s)⇧+" .
with j have "((x#xs)!Suc k, (x#xs)!j) ∈ (tree_edges s)⇧+" by simp
with * show ?thesis by (metis trancl_into_trancl2)
qed
next
case False
define k' where "k' = k - 1"
with False ‹k ≤ j'› have "k' < j'" and k: "k = Suc k'" by simp_all
with cons.IH[OF p j'_le] have "(xs!k', xs!j') ∈ (tree_edges s)⇧+" by metis
hence "((x#xs)!Suc k', (x#xs)!Suc j') ∈ (tree_edges s)⇧+" by simp
with k j show ?thesis by simp
qed
qed
qed
lemma lowlink_path_finished:
assumes p: "lowlink_path s v p w"
and j: "j < length p" "j > 0"
shows "p!j ∈ dom (finished s)"
proof -
from j have "length p > 1" by simp
with p have f: "p!1 ∈ dom (finished s)" by (simp add: lowlink_path_def)
thus ?thesis
proof (cases "j=1")
case False with j have "j > 1" by simp
with assms lowlink_path_in_tree[where k=1] have "(p!1,p!j) ∈ (tree_edges s)⇧+" by simp
with f tree_path_impl_parenthesis show ?thesis by simp
qed simp
qed
lemma lowlink_path_tree_prepend:
assumes p: "lowlink_path s v p w"
and tree_edges: "(u,v) ∈ (tree_edges s)⇧+"
and fin: "u ∈ dom (finished s) ∨ (stack s ≠ [] ∧ u = hd (stack s))"
shows "∃p. lowlink_path s u p w"
proof -
note lowlink_path_def[simp]
from tree_edges trancl_is_path obtain tp where
tp: "path (tree_edges s) u tp v" "tp ≠ []"
by metis
from tree_path_impl_parenthesis assms hd_stack_tree_path_finished have
v_fin: "v ∈ dom (finished s)" by blast
from p have "p!0 = hd p" by (simp add: hd_conv_nth)
with p have p_0: "p!0 = v" by (auto simp add: path_hd)
let ?p = "tp @ p"
{
from tp path_mono[OF tree_edges_ssE] have "path E u tp v" by simp
also from p have "path E v p w" by simp
finally have "path E u ?p w" .
}
moreover from p have "?p ≠ []" by simp
moreover
from p have "(last ?p, w) ∈ cross_edges s ∪ back_edges s" by simp
moreover {
assume "length ?p > 1"
have "?p ! 1 ∈ dom (finished s)"
proof (cases "length tp > 1")
case True hence tp1: "?p ! 1 = tp ! 1" by (simp add: nth_append)
from tp True have "(tp ! 0, tp ! 1) ∈ (tree_edges s)⇧+"
by (auto simp add: path_nth_conv nth_append elim: allE[where x=0])
also from True have "tp ! 0 = hd tp" by (simp add: hd_conv_nth)
also from tp have "hd tp = u" by (simp add: path_hd)
finally have "tp ! 1 ∈ dom (finished s)"
using tree_path_impl_parenthesis fin hd_stack_tree_path_finished by blast
thus ?thesis by (subst tp1)
next
case False with tp have "length tp = 1" by (cases tp) auto
with p_0 have "?p ! 1 = v" by (simp add: nth_append)
thus ?thesis by (simp add: v_fin)
qed
also have "∀k < length ?p - 1. (?p!k, ?p!Suc k) ∈ tree_edges s"
proof (safe)
fix k
assume A: "k < length ?p - 1"
show "(?p!k, ?p!Suc k) ∈ tree_edges s"
proof (cases "k < length tp")
case True hence k: "?p ! k = tp ! k" by (simp add: nth_append)
show ?thesis
proof (cases "Suc k < length tp")
case True hence "?p ! Suc k = tp ! Suc k" by (simp add: nth_append)
moreover from True tp have "(tp ! k, tp ! Suc k) ∈ tree_edges s"
by (auto simp add: path_nth_conv nth_append
elim: allE[where x=k])
ultimately show ?thesis using k by simp
next
case False with True have *: "Suc k = length tp" by simp
with tp True have "(tp ! k, v) ∈ tree_edges s"
by (auto simp add: path_nth_conv nth_append
elim: allE[where x=k])
also from * p_0 have "v = ?p ! Suc k" by (simp add: nth_append)
finally show ?thesis by (simp add: k)
qed
next
case False hence *: "Suc k - length tp = Suc (k - length tp)" by simp
define k' where "k' = k - length tp"
with False * have k': "?p ! k = p ! k'" "?p ! Suc k = p ! Suc k'"
by (simp_all add: nth_append)
from k'_def False A have "k' < length p - 1" by simp
with p have "(p!k', p!Suc k') ∈ tree_edges s" by simp
with k' show ?thesis by simp
qed
qed
also (conjI) note calculation
}
ultimately have "lowlink_path s u ?p w" by simp
thus ?thesis ..
qed
lemma lowlink_path_complex:
assumes "(u,v) ∈ (tree_edges s)⇧+"
and "u ∈ dom (finished s) ∨ (stack s ≠ [] ∧ u = hd (stack s))"
and "(v,w) ∈ cross_edges s ∪ back_edges s"
shows "∃p. lowlink_path s u p w"
proof -
from assms lowlink_path_single have "lowlink_path s v [v] w" by simp
with assms lowlink_path_tree_prepend show ?thesis by simp
qed
lemma no_path_imp_no_lowlink_path:
assumes "edges s `` {v} = {}"
shows "¬lowlink_path s v p w"
proof
assume p: "lowlink_path s v p w"
hence [simp]: "p≠[]" by (simp add: lowlink_path_def)
from p have "hd p = v" by (auto simp add: lowlink_path_def path_hd)
with hd_conv_nth[OF ‹p≠[]›] have v: "p!0 = v" by simp
show False
proof (cases "length p > 1")
case True with p have "(p!0,p!1) ∈ tree_edges s" by (simp add: lowlink_path_def)
with v assms show False by auto
next
case False with ‹p≠[]› have "length p = 1" by (cases p) auto
hence "last p = v" by (simp add: last_conv_nth v)
with p have "(v,w) ∈ edges s" by (simp add: lowlink_path_def)
with assms show False by auto
qed
qed
context begin interpretation timing_syntax .
lemma LowLink_le_disc:
assumes "v ∈ dom (discovered s)"
shows "LowLink s v ≤ δ s v"
using assms
unfolding lowlink_set_def
by clarsimp
lemma LowLink_lessE:
assumes "LowLink s v < x"
and "v ∈ dom (discovered s)"
obtains w where "δ s w < x" "w ∈ lowlink_set s v"
proof -
let ?L = "δ s ` lowlink_set s v"
note assms
moreover from lowlink_set_finite have "finite ?L" by auto
moreover from lowlink_set_not_empty assms have "?L ≠ {}" by auto
ultimately show ?thesis using that by (auto simp: Min_less_iff)
qed
lemma LowLink_lessI:
assumes "y ∈ lowlink_set s v"
and "δ s y < δ s v"
shows "LowLink s v < δ s v"
proof -
let ?L = "δ s ` lowlink_set s v"
from assms have "δ s y ∈ ?L" by simp
moreover hence "?L ≠ {}" by auto
moreover from lowlink_set_finite have "finite ?L" by auto
ultimately show ?thesis
by (metis Min_less_iff assms(2))
qed
lemma LowLink_eqI:
assumes "DFS_invar G param s'"
assumes sub_m: "discovered s ⊆⇩m discovered s'"
assumes sub: "lowlink_set s w ⊆ lowlink_set s' w"
and rev_sub: "lowlink_set s' w ⊆ lowlink_set s w ∪ X"
and w_disc: "w ∈ dom (discovered s)"
and X: "⋀x. ⟦x ∈ X; x ∈ lowlink_set s' w⟧ ⟹ δ s' x ≥ LowLink s w"
shows "LowLink s w = LowLink s' w"
proof (rule ccontr)
interpret s': DFS_invar where s=s' by fact
assume A: "LowLink s w ≠ LowLink s' w"
from lowlink_set_discovered sub sub_m w_disc have
sub': "δ s ` lowlink_set s w ⊆ δ s' ` lowlink_set s' w"
and w_disc': "w ∈ dom (discovered s')"
and eq: "⋀ll. ll ∈ lowlink_set s w ⟹ δ s' ll = δ s ll"
by (force simp: map_le_def)+
from lowlink_set_not_empty[OF w_disc] A Min_antimono[OF sub'] s'.lowlink_set_finite have
"LowLink s' w < LowLink s w" by fastforce
then obtain ll where ll: "ll ∈ lowlink_set s' w" and ll_le: "δ s' ll < LowLink s w"
by (metis s'.LowLink_lessE w_disc')
with rev_sub have "ll ∈ lowlink_set s w ∨ ll ∈ X" by auto
hence "LowLink s w ≤ δ s' ll"
proof
assume "ll ∈ lowlink_set s w" with lowlink_set_finite eq show ?thesis by force
next
assume "ll ∈ X" with ll show ?thesis by (metis X)
qed
with ll_le show False by simp
qed
lemma LowLink_eq_disc_iff_scc_root:
assumes "v ∈ dom (finished s) ∨ (stack s ≠ [] ∧ v = hd (stack s) ∧ pending s `` {v} = {})"
shows "LowLink s v = δ s v ⟷ scc_root s v (scc_of E v)"
proof
let ?scc = "scc_of E v"
assume scc: "scc_root s v ?scc"
show "LowLink s v = δ s v"
proof (rule ccontr)
assume A: "LowLink s v ≠ δ s v"
from assms finished_discovered stack_discovered hd_in_set have disc: "v ∈ dom (discovered s)" by blast
with assms LowLink_le_disc A have "LowLink s v < δ s v" by force
with disc obtain w where
w: "δ s w < δ s v" "w ∈ lowlink_set s v"
by (metis LowLink_lessE)
with lowlink_set_discovered have wdisc: "w ∈ dom (discovered s)" by auto
from w have "(v,w) ∈ E⇧*" "(w,v) ∈ E⇧*" by (auto simp add: lowlink_set_def)
moreover have "is_scc E ?scc" "v ∈ ?scc" by simp_all
ultimately have "w ∈ ?scc" by (metis is_scc_closed)
with wdisc scc_root_disc_le[OF scc] have "δ s v ≤ δ s w" by simp
with w show False by auto
qed
next
assume LL: "LowLink s v = δ s v"
from assms finished_discovered stack_discovered hd_in_set have
v_disc: "v ∈ dom (discovered s)" by blast
from assms finished_no_pending have
v_no_p: "pending s `` {v} = {}" by blast
let ?scc = "scc_of E v"
have is_scc: "is_scc E ?scc" by simp
{
fix r
assume "r ≠ v"
and "r ∈ ?scc" "r ∈ dom (discovered s)"
have "v ∈ ?scc" by simp
with ‹r ∈ ?scc› is_scc have "(v,r) ∈ (Restr E ?scc)⇧*"
by (simp add: is_scc_connected')
hence "(v,r) ∈ (tree_edges s)⇧+" using ‹r≠v›
proof (induction rule: rtrancl_induct)
case (step y z) hence "(v,z) ∈ (Restr E ?scc)⇧*"
by (metis rtrancl_into_rtrancl)
hence "(v,z) ∈ E⇧*" by (metis Restr_rtrancl_mono)
from step have "(z,v) ∈ E⇧*" by (simp add: is_scc_connected[OF is_scc])
{
assume z_disc: "z ∈ dom (discovered s)"
and "∃p. lowlink_path s v p z"
with ‹(z,v)∈E⇧*› ‹(v,z)∈E⇧*› have ll: "z ∈ lowlink_set s v"
by (metis lowlink_setI)
have "δ s v < δ s z"
proof (rule ccontr)
presume "δ s v ≥ δ s z" with ‹z≠v› v_disc z_disc disc_unequal have "δ s z < δ s v" by fastforce
with ll have "LowLink s v < δ s v" by (metis LowLink_lessI)
with LL show False by simp
qed simp
} note δz = this
show ?case
proof (cases "y=v")
case True note [simp] = this
with step v_no_p v_disc no_pending_imp_succ_discovered have
z_disc: "z ∈ dom (discovered s)" by blast
from step edges_covered v_no_p v_disc have "(v,z) ∈ edges s" by auto
thus ?thesis
proof (rule edgesE_CB)
assume "(v,z) ∈ tree_edges s" thus ?thesis ..
next
assume CB: "(v,z) ∈ cross_edges s ∪ back_edges s"
hence "lowlink_path s v [v] z"
by (simp add: lowlink_path_single)
with δz[OF z_disc] no_pending_succ_impl_path_in_tree v_disc v_no_p step show ?thesis
by auto
qed
next
case False with step.IH have T: "(v,y) ∈ (tree_edges s)⇧+" .
with tree_path_impl_parenthesis assms hd_stack_tree_path_finished tree_path_disc have
y_fin: "y ∈ dom (finished s)"
and y_δ : "δ s v < δ s y" by blast+
with step have z_disc: "z ∈ dom (discovered s)"
using finished_imp_succ_discovered
by auto
from step edges_covered finished_no_pending[of y] y_fin finished_discovered have
"(y,z) ∈ edges s"
by fast
thus ?thesis
proof (rule edgesE_CB)
assume "(y,z) ∈ tree_edges s" with T show ?thesis ..
next
assume CB: "(y,z) ∈ cross_edges s ∪ back_edges s"
with lowlink_path_complex[OF T] assms have
"∃p. lowlink_path s v p z" by blast
with δz z_disc have δz: "δ s v < δ s z" by simp
show ?thesis
proof (cases "v ∈ dom (finished s)")
case True with tree_path_impl_parenthesis T have y_f: "φ s y < φ s v" by blast
from CB show ?thesis
proof
assume C: "(y,z) ∈ cross_edges s"
with cross_edges_finished_decr y_fin y_f have "φ s z < φ s v"
by force
moreover note δz
moreover from C cross_edges_target_finished have
"z ∈ dom (finished s)" by simp
ultimately show ?thesis
using parenthesis_impl_tree_path[OF True] by metis
next
assume B: "(y,z) ∈ back_edges s"
with back_edge_disc_lt_fin y_fin y_f have "δ s z < φ s v"
by force
moreover note δz z_disc
ultimately have "z ∈ dom (finished s)" "φ s z < φ s v"
using parenthesis_contained[OF True] by simp_all
with δz show ?thesis
using parenthesis_impl_tree_path[OF True] by metis
qed
next
case False
with assms have st: "stack s ≠ []" "v = hd (stack s)" "pending s `` {v} = {}" by blast+
have "z ∈ dom (finished s)"
proof (rule ccontr)
assume "z ∉ dom (finished s)"
with z_disc have "z ∈ set (stack s)" by (simp add: stack_set_def)
with ‹z≠v› st have "z ∈ set (tl (stack s))" by (cases "stack s") auto
with st tl_lt_stack_hd_discover δz show False by force
qed
with δz parenthesis_impl_tree_path_not_finished v_disc False show ?thesis by simp
qed
qed
qed
qed simp
hence "r ∈ (tree_edges s)⇧* `` {v}" by auto
}
hence "?scc ∩ dom (discovered s) ⊆ (tree_edges s)⇧* `` {v}"
by fastforce
thus "scc_root s v ?scc" by (auto intro!: scc_rootI v_disc)
qed
end end
end