Theory DFS_Invars_SCC
section ‹Invariants for SCCs›
theory DFS_Invars_SCC
imports
DFS_Invars_Basic
begin
definition scc_root' :: "('v × 'v) set ⇒ ('v,'es) state_scheme ⇒ 'v ⇒ 'v set ⇒ bool"
where
"scc_root' E s v scc ⟷ is_scc E scc
∧ v ∈ scc
∧ v ∈ dom (discovered s)
∧ scc ∩ dom (discovered s) ⊆ (tree_edges s)⇧* `` {v}"
context param_DFS_defs begin
abbreviation "scc_root ≡ scc_root' E"
lemmas scc_root_def = scc_root'_def
lemma scc_rootI:
assumes "is_scc E scc"
and "v ∈ dom (discovered s)"
and "v ∈ scc"
and "scc ∩ dom (discovered s) ⊆ (tree_edges s)⇧* `` {v}"
shows "scc_root s v scc"
using assms by (simp add: scc_root_def)
definition "scc_roots s = {v. ∃scc. scc_root s v scc}"
end
context DFS_invar begin
lemma scc_root_is_discovered:
"scc_root s v scc ⟹ v ∈ dom (discovered s)"
by (simp add: scc_root_def)
lemma scc_root_scc_tree_rtrancl:
assumes "scc_root s v scc"
and "x ∈ scc" "x ∈ dom (discovered s)"
shows "(v,x) ∈ (tree_edges s)⇧*"
using assms
by (auto simp add: scc_root_def)
lemma scc_root_scc_reach:
assumes "scc_root s r scc"
and "v ∈ scc"
shows "(r,v) ∈ E⇧*"
proof -
from assms have "is_scc E scc" "r ∈ scc" by (simp_all add: scc_root_def)
with is_scc_connected assms show ?thesis by metis
qed
lemma scc_reach_scc_root:
assumes "scc_root s r scc"
and "v ∈ scc"
shows "(v,r) ∈ E⇧*"
proof -
from assms have "is_scc E scc" "r ∈ scc" by (simp_all add: scc_root_def)
with is_scc_connected assms show ?thesis by metis
qed
lemma scc_root_scc_tree_trancl:
assumes "scc_root s v scc"
and "x ∈ scc" "x ∈ dom (discovered s)" "x ≠ v"
shows "(v,x) ∈ (tree_edges s)⇧+"
using assms scc_root_scc_tree_rtrancl
by (auto simp add: rtrancl_eq_or_trancl)
lemma scc_root_unique_scc:
"scc_root s v scc ⟹ scc_root s v scc' ⟹ scc = scc'"
unfolding scc_root_def
by (metis is_scc_unique)
lemma scc_root_unique_root:
assumes scc1: "scc_root s v scc"
and scc2: "scc_root s v' scc"
shows "v = v'"
proof (rule ccontr)
assume "v ≠ v'"
from scc1 have "v ∈ scc" "v ∈ dom (discovered s)"
by (simp_all add: scc_root_def)
with scc_root_scc_tree_trancl[OF scc2] ‹v ≠ v'› have "(v',v) ∈ (tree_edges s)⇧+"
by simp
also from scc2 have "v' ∈ scc" "v' ∈ dom (discovered s)"
by (simp_all add: scc_root_def)
with scc_root_scc_tree_trancl[OF scc1] ‹v≠v'› have "(v,v') ∈ (tree_edges s)⇧+"
by simp
finally show False using no_loop_in_tree by contradiction
qed
lemma scc_root_unique_is_scc:
assumes "scc_root s v scc"
shows "scc_root s v (scc_of E v)"
proof -
from assms have "v ∈ scc" "is_scc E scc" by (simp_all add: scc_root_def)
moreover have "v ∈ scc_of E v" "is_scc E (scc_of E v)" by simp_all
ultimately have "scc = scc_of E v" using is_scc_unique by metis
thus ?thesis using assms by simp
qed
lemma scc_root_finished_impl_scc_finished:
assumes "v ∈ dom (finished s)"
and "scc_root s v scc"
shows "scc ⊆ dom (finished s)"
proof
fix x
assume "x ∈ scc"
let ?E = "Restr E scc"
from assms have "is_scc E scc" "v ∈ scc" by (simp_all add: scc_root_def)
hence "(v,x) ∈ (Restr E scc)⇧*" using ‹x ∈ scc›
by (simp add: is_scc_connected')
with rtrancl_is_path obtain p where "path ?E v p x" by metis
thus "x ∈ dom (finished s)"
proof (induction p arbitrary: x rule: rev_induct)
case Nil hence "v = x" by simp
with assms show ?case by simp
next
case (snoc y ys) hence "path ?E v ys y" "(y,x) ∈ ?E"
by (simp_all add: path_append_conv)
with snoc.IH have "y ∈ dom (finished s)" by simp
moreover from ‹(y,x) ∈ ?E› have "(y,x) ∈ E" "x ∈ scc" by auto
ultimately have "x ∈ dom (discovered s)"
using finished_imp_succ_discovered
by blast
with ‹x ∈ scc› show ?case
using assms scc_root_scc_tree_trancl tree_path_impl_parenthesis
by blast
qed
qed
context begin interpretation timing_syntax .
lemma scc_root_disc_le:
assumes "scc_root s v scc"
and "x ∈ scc" "x ∈ dom (discovered s)"
shows "δ s v ≤ δ s x"
proof (cases "x = v")
case False with assms scc_root_scc_tree_trancl tree_path_disc have
"δ s v < δ s x"
by blast
thus ?thesis by simp
qed simp
lemma scc_root_fin_ge:
assumes "scc_root s v scc"
and "v ∈ dom (finished s)"
and "x ∈ scc"
shows "φ s v ≥ φ s x"
proof (cases "x = v")
case False
from assms scc_root_finished_impl_scc_finished have
"x ∈ dom (finished s)" by auto
hence "x ∈ dom (discovered s)" using finished_discovered by auto
with assms False have "(v,x) ∈ (tree_edges s)⇧+"
using scc_root_scc_tree_trancl by simp
with tree_path_impl_parenthesis assms False show ?thesis by force
qed simp
lemma scc_root_is_Min_disc:
assumes "scc_root s v scc"
shows "Min (δ s ` (scc ∩ dom (discovered s))) = δ s v" (is "Min ?S = _")
proof (rule Min_eqI)
from discovered_finite show "finite ?S" by auto
from scc_root_disc_le[OF assms] show "⋀y. y ∈ ?S ⟹ δ s v ≤ y" by force
from assms have "v ∈ scc" "v ∈ dom (discovered s)"
by (simp_all add: scc_root_def)
thus "δ s v ∈ ?S" by auto
qed
lemma Min_disc_is_scc_root:
assumes "v ∈ scc" "v ∈ dom (discovered s)"
and "is_scc E scc"
and min: "δ s v = Min (δ s ` (scc ∩ dom (discovered s)))"
shows "scc_root s v scc"
proof -
{
fix y
assume A: "y ∈ scc" "y ∈ dom (discovered s)" "y ≠ v"
with min have "δ s v ≤ δ s y" by auto
with assms disc_unequal A have "δ s v < δ s y" by fastforce
} note scc_disc = this
{
fix x
assume A: "x ∈ scc ∩ dom (discovered s)"
have "x ∈ (tree_edges s)⇧* `` {v}"
proof (cases "v = x")
case False with A scc_disc have δ: "δ s v < δ s x" by simp
have "(v,x) ∈ (tree_edges s)⇧+"
proof (cases "v ∈ dom (finished s)")
case False with stack_set_def assms have
v_stack: "v ∈ set (stack s)" by auto
show ?thesis
proof (cases "x ∈ dom (finished s)")
case True
with parenthesis_impl_tree_path_not_finished[of v x] assms δ False
show ?thesis by auto
next
case False with A stack_set_def have "x ∈ set (stack s)" by auto
with v_stack δ show ?thesis
using on_stack_is_tree_path
by simp
qed
next
case True note v_fin = this
let ?E = "Restr E scc"
{
fix y
assume "(v, y) ∈ ?E" and "v ≠ y"
hence *: "y ∈ succ v" "y ∈ scc" by auto
with finished_imp_succ_discovered v_fin have
"y ∈ dom (discovered s)" by simp
with scc_disc ‹v ≠ y› * have "δ s v < δ s y" by simp
with * finished_succ_impl_path_in_tree v_fin have "(v,y) ∈ (tree_edges s)⇧+" by simp
} note trancl_base = this
from A have "x ∈ scc" by simp
with assms have "(v,x) ∈ ?E⇧*"
by (simp add: is_scc_connected')
with ‹v≠x› have "(v,x) ∈ ?E⇧+" by (metis rtrancl_eq_or_trancl)
thus ?thesis using ‹v≠x›
proof (induction)
case (base y) with trancl_base show ?case .
next
case (step y z)
show ?case
proof (cases "v = y")
case True with step trancl_base show ?thesis by simp
next
case False with step have "(v,y) ∈ (tree_edges s)⇧+" by simp
with tree_path_impl_parenthesis[OF _ v_fin] have
y_fin: "y ∈ dom (finished s)"
and y_t: "δ s v < δ s y" "φ s y < φ s v"
by auto
with finished_discovered have y_disc: "y ∈ dom (discovered s)"
by auto
from step have *: "z ∈ succ y" "z ∈ scc" by auto
with finished_imp_succ_discovered y_fin have
z_disc: "z ∈ dom (discovered s)" by simp
with * ‹v≠z› have δz: "δ s v < δ s z" by (simp add: scc_disc)
from * edges_covered finished_no_pending[OF ‹y ∈ dom (finished s)›]
y_disc have "(y,z) ∈ edges s" by auto
thus ?thesis
proof safe
assume "(y,z) ∈ tree_edges s" with ‹(v,y) ∈ (tree_edges s)⇧+› show ?thesis ..
next
assume CE: "(y,z) ∈ cross_edges s"
with cross_edges_finished_decr y_fin y_t have "φ s z < φ s v"
by force
moreover note δz
moreover from CE cross_edges_target_finished have
"z ∈ dom (finished s)" by simp
ultimately show ?thesis
using parenthesis_impl_tree_path[OF v_fin] by metis
next
assume BE: "(y,z) ∈ back_edges s"
with back_edge_disc_lt_fin y_fin y_t have
"δ s z < φ s v" by force
moreover note δz
moreover note z_disc
ultimately have "z ∈ dom (finished s)" "φ s z < φ s v"
using parenthesis_contained[OF v_fin] by simp_all
with δz show ?thesis
using parenthesis_impl_tree_path[OF v_fin] by metis
qed
qed
qed
qed
thus ?thesis by auto
qed simp
}
hence "scc ∩ dom (discovered s) ⊆ (tree_edges s)⇧* `` {v}" by blast
with assms show ?thesis by (auto intro: scc_rootI)
qed
lemma scc_root_iff_Min_disc:
assumes "is_scc E scc" "r ∈ scc" "r ∈ dom (discovered s)"
shows "scc_root s r scc ⟷ Min (δ s ` (scc ∩ dom (discovered s))) = δ s r" (is "?L ⟷ ?R")
proof
assume "?L" with scc_root_is_Min_disc show "?R" .
next
assume "?R" with Min_disc_is_scc_root assms show "?L" by simp
qed
lemma scc_root_exists:
assumes "is_scc E scc"
and scc: "scc ∩ dom (discovered s) ≠ {}"
shows "∃r. scc_root s r scc"
proof -
let ?S = "scc ∩ dom (discovered s)"
from discovered_finite have "finite (δ s`?S)" by auto
moreover from scc have "δ s ` ?S ≠ {}" by auto
moreover have "⋀(x::nat) f A. x ∉ f ` A ∨ (∃y. x = f y ∧ y ∈ A)" by blast
ultimately have "∃x ∈ ?S. δ s x = Min (δ s ` ?S)" by (metis Min_in)
with Min_disc_is_scc_root ‹is_scc E scc› show ?thesis by auto
qed
lemma scc_root_of_node_exists:
assumes "v ∈ dom (discovered s)"
shows "∃r. scc_root s r (scc_of E v)"
proof -
have "is_scc E (scc_of E v)" by simp
moreover have "v ∈ scc_of E v" by simp
with assms have "scc_of E v ∩ dom (discovered s) ≠ {}" by blast
ultimately show ?thesis using scc_root_exists by metis
qed
lemma scc_root_transfer':
assumes "discovered s = discovered s'" "tree_edges s = tree_edges s'"
shows "scc_root s r scc ⟷ scc_root s' r scc"
unfolding scc_root_def
by (simp add: assms)
lemma scc_root_transfer:
assumes inv: "DFS_invar G param s'"
assumes r_d: "r ∈ dom (discovered s)"
assumes d: "dom (discovered s) ⊆ dom (discovered s')"
"∀x∈dom (discovered s). δ s x = δ s' x"
"∀x∈dom (discovered s') - dom (discovered s). δ s' x ≥ counter s"
and t: "tree_edges s ⊆ tree_edges s'"
shows "scc_root s r scc ⟷ scc_root s' r scc"
proof -
interpret s': DFS_invar where s=s' by fact
let ?sd = "scc ∩ dom (discovered s)"
let ?sd' = "scc ∩ dom (discovered s')"
let ?sdd = "scc ∩ (dom (discovered s') - dom (discovered s))"
{
assume r_s: "r ∈ scc" "is_scc E scc"
with r_d have ne: "δ s'`?sd ≠ {}" by blast
from discovered_finite have fin: "finite (δ s' ` ?sd)" by simp
from timing_less_counter d have "⋀x. x∈δ s' ` ?sd ⟹ x < counter s" by auto
hence Min: "Min (δ s' ` ?sd) < counter s"
using Min_less_iff[OF fin] ne by blast
from d have "Min (δ s ` ?sd) = Min (δ s' ` ?sd)" by (auto simp: image_def)
also from d have "?sd' = ?sd ∪ ?sdd" by auto
hence *: "δ s' ` ?sd' = δ s' ` ?sd ∪ δ s' ` ?sdd" by auto
hence "Min (δ s' ` ?sd) = Min (δ s' ` ?sd')"
proof (cases "?sdd = {}")
case False
from d have "⋀x. x ∈ δ s' ` ?sdd ⟹ x ≥ counter s" by auto
moreover from False have ne': "δ s' ` ?sdd ≠ {}" by blast
moreover from s'.discovered_finite have fin': "finite (δ s' ` ?sdd)" by blast
ultimately have "Min (δ s' ` ?sdd) ≥ counter s"
using Min_ge_iff by metis
with Min Min_Un[OF fin ne fin' ne'] * show ?thesis by simp
qed simp
finally have "Min (δ s ` ?sd) = Min (δ s' ` ?sd')" .
} note aux = this
show ?thesis
proof
assume r: "scc_root s r scc"
from r_d d have "δ s' r = δ s r" by simp
also from r scc_root_is_Min_disc have "δ s r = Min (δ s ` ?sd)" by simp
also from r aux have "Min (δ s ` ?sd) = Min (δ s' ` ?sd')" by (simp add: scc_root_def)
finally show "scc_root s' r scc"
using r_d d r[unfolded scc_root_def]
by (blast intro!: s'.Min_disc_is_scc_root)
next
assume r': "scc_root s' r scc"
from r_d d have "δ s r = δ s' r" by simp
also from r' s'.scc_root_is_Min_disc have "δ s' r = Min (δ s' ` ?sd')" by simp
also from r' aux have "Min (δ s' ` ?sd') = Min (δ s ` ?sd)" by (simp add: scc_root_def)
finally show "scc_root s r scc"
using r_d d r'[unfolded scc_root_def]
by (blast intro!: Min_disc_is_scc_root)
qed
qed
end end
end