Theory Digraph_Component
theory Digraph_Component
imports
Digraph
Arc_Walk
Pair_Digraph
begin
section ‹Components of (Symmetric) Digraphs›
definition compatible :: "('a,'b) pre_digraph ⇒ ('a,'b) pre_digraph ⇒ bool" where
"compatible G H ≡ tail G = tail H ∧ head G = head H"
definition subgraph :: "('a,'b) pre_digraph ⇒ ('a,'b) pre_digraph ⇒ bool" where
"subgraph H G ≡ verts H ⊆ verts G ∧ arcs H ⊆ arcs G ∧ wf_digraph G ∧ wf_digraph H ∧ compatible G H"
definition induced_subgraph :: "('a,'b) pre_digraph ⇒ ('a,'b) pre_digraph ⇒ bool" where
"induced_subgraph H G ≡ subgraph H G ∧ arcs H = {e ∈ arcs G. tail G e ∈ verts H ∧ head G e ∈ verts H}"
definition spanning :: "('a,'b) pre_digraph ⇒ ('a,'b) pre_digraph ⇒ bool" where
"spanning H G ≡ subgraph H G ∧ verts G = verts H"
definition strongly_connected :: "('a,'b) pre_digraph ⇒ bool" where
"strongly_connected G ≡ verts G ≠ {} ∧ (∀u ∈ verts G. ∀v ∈ verts G. u →⇧*⇘G⇙ v)"
text ‹
The following function computes underlying symmetric graph of a digraph
and removes parallel arcs.
›
definition mk_symmetric :: "('a,'b) pre_digraph ⇒ 'a pair_pre_digraph" where
"mk_symmetric G ≡ ⦇ pverts = verts G, parcs = ⋃e∈arcs G. {(tail G e, head G e), (head G e, tail G e)}⦈"
definition connected :: "('a,'b) pre_digraph ⇒ bool" where
"connected G ≡ strongly_connected (mk_symmetric G)"
definition forest :: "('a,'b) pre_digraph ⇒ bool" where
"forest G ≡ ¬(∃p. pre_digraph.cycle G p)"
definition tree :: "('a,'b) pre_digraph ⇒ bool" where
"tree G ≡ connected G ∧ forest G"
definition spanning_tree :: "('a,'b) pre_digraph ⇒ ('a,'b) pre_digraph ⇒ bool" where
"spanning_tree H G ≡ tree H ∧ spanning H G"
definition (in pre_digraph)
max_subgraph :: "(('a,'b) pre_digraph ⇒ bool) ⇒ ('a,'b) pre_digraph ⇒ bool"
where
"max_subgraph P H ≡ subgraph H G ∧ P H ∧ (∀H'. H' ≠ H ∧ subgraph H H' ⟶ ¬(subgraph H' G ∧ P H'))"
definition (in pre_digraph) sccs :: "('a,'b) pre_digraph set" where
"sccs ≡ {H. induced_subgraph H G ∧ strongly_connected H ∧ ¬(∃H'. induced_subgraph H' G
∧ strongly_connected H' ∧ verts H ⊂ verts H')}"
definition (in pre_digraph) sccs_verts :: "'a set set" where
"sccs_verts = {S. S ≠ {} ∧ (∀u ∈ S. ∀v ∈ S. u →⇧*⇘G⇙ v) ∧ (∀u ∈ S. ∀v. v ∉ S ⟶ ¬u →⇧*⇘G⇙ v ∨ ¬v →⇧*⇘G⇙ u)}"
definition (in pre_digraph) scc_of :: "'a ⇒ 'a set" where
"scc_of u ≡ {v. u →⇧* v ∧ v →⇧* u}"
definition union :: "('a,'b) pre_digraph ⇒ ('a,'b) pre_digraph ⇒ ('a,'b) pre_digraph" where
"union G H ≡ ⦇ verts = verts G ∪ verts H, arcs = arcs G ∪ arcs H, tail = tail G, head = head G⦈"
definition (in pre_digraph) Union :: "('a,'b) pre_digraph set ⇒ ('a,'b) pre_digraph" where
"Union gs = ⦇ verts = (⋃G ∈ gs. verts G), arcs = (⋃G ∈ gs. arcs G),
tail = tail G , head = head G ⦈"
subsection ‹Compatible Graphs›
lemma compatible_tail:
assumes "compatible G H" shows "tail G = tail H"
using assms by (simp add: fun_eq_iff compatible_def)
lemma compatible_head:
assumes "compatible G H" shows "head G = head H"
using assms by (simp add: fun_eq_iff compatible_def)
lemma compatible_cas:
assumes "compatible G H" shows "pre_digraph.cas G = pre_digraph.cas H"
proof (unfold fun_eq_iff, intro allI)
fix u es v show "pre_digraph.cas G u es v = pre_digraph.cas H u es v"
using assms
by (induct es arbitrary: u)
(simp_all add: pre_digraph.cas.simps compatible_head compatible_tail)
qed
lemma compatible_awalk_verts:
assumes "compatible G H" shows "pre_digraph.awalk_verts G = pre_digraph.awalk_verts H"
proof (unfold fun_eq_iff, intro allI)
fix u es show "pre_digraph.awalk_verts G u es = pre_digraph.awalk_verts H u es"
using assms
by (induct es arbitrary: u)
(simp_all add: pre_digraph.awalk_verts.simps compatible_head compatible_tail)
qed
lemma compatibleI_with_proj[intro]:
shows "compatible (with_proj G) (with_proj H)"
by (auto simp: compatible_def)
subsection ‹Basic lemmas›
lemma (in sym_digraph) graph_symmetric:
shows "(u,v) ∈ arcs_ends G ⟹ (v,u) ∈ arcs_ends G"
using sym_arcs by (auto simp add: symmetric_def sym_def)
lemma strongly_connectedI[intro]:
assumes "verts G ≠ {}" "⋀u v. u ∈ verts G ⟹ v ∈ verts G ⟹ u →⇧*⇘G⇙ v"
shows "strongly_connected G"
using assms by (simp add: strongly_connected_def)
lemma strongly_connectedE[elim]:
assumes "strongly_connected G"
assumes "(⋀u v. u ∈ verts G ∧ v ∈ verts G ⟹ u →⇧*⇘G⇙ v) ⟹ P"
shows "P"
using assms by (auto simp add: strongly_connected_def)
lemma subgraph_imp_subverts:
assumes "subgraph H G"
shows "verts H ⊆ verts G"
using assms by (simp add: subgraph_def)
lemma induced_imp_subgraph:
assumes "induced_subgraph H G"
shows "subgraph H G"
using assms by (simp add: induced_subgraph_def)
lemma (in pre_digraph) in_sccs_imp_induced:
assumes "c ∈ sccs"
shows "induced_subgraph c G"
using assms by (auto simp: sccs_def)
lemma spanning_tree_imp_tree[dest]:
assumes "spanning_tree H G"
shows "tree H"
using assms by (simp add: spanning_tree_def)
lemma tree_imp_connected[dest]:
assumes "tree G"
shows "connected G"
using assms by (simp add: tree_def)
lemma spanning_treeI[intro]:
assumes "spanning H G"
assumes "tree H"
shows "spanning_tree H G"
using assms by (simp add: spanning_tree_def)
lemma spanning_treeE[elim]:
assumes "spanning_tree H G"
assumes "tree H ∧ spanning H G ⟹ P"
shows "P"
using assms by (simp add: spanning_tree_def)
lemma spanningE[elim]:
assumes "spanning H G"
assumes "subgraph H G ∧ verts G = verts H ⟹ P"
shows "P"
using assms by (simp add: spanning_def)
lemma (in pre_digraph) in_sccsI[intro]:
assumes "induced_subgraph c G"
assumes "strongly_connected c"
assumes "¬(∃c'. induced_subgraph c' G ∧ strongly_connected c' ∧
verts c ⊂ verts c')"
shows "c ∈ sccs"
using assms by (auto simp add: sccs_def)
lemma (in pre_digraph) in_sccsE[elim]:
assumes "c ∈ sccs"
assumes "induced_subgraph c G ⟹ strongly_connected c ⟹ ¬ (∃d.
induced_subgraph d G ∧ strongly_connected d ∧ verts c ⊂ verts d) ⟹ P"
shows "P"
using assms by (simp add: sccs_def)
lemma subgraphI:
assumes "verts H ⊆ verts G"
assumes "arcs H ⊆ arcs G"
assumes "compatible G H"
assumes "wf_digraph H"
assumes "wf_digraph G"
shows "subgraph H G"
using assms by (auto simp add: subgraph_def)
lemma subgraphE[elim]:
assumes "subgraph H G"
obtains "verts H ⊆ verts G" "arcs H ⊆ arcs G" "compatible G H" "wf_digraph H" "wf_digraph G"
using assms by (simp add: subgraph_def)
lemma induced_subgraphI[intro]:
assumes "subgraph H G"
assumes "arcs H = {e ∈ arcs G. tail G e ∈ verts H ∧ head G e ∈ verts H}"
shows "induced_subgraph H G"
using assms unfolding induced_subgraph_def by safe
lemma induced_subgraphE[elim]:
assumes "induced_subgraph H G"
assumes "⟦subgraph H G; arcs H = {e ∈ arcs G. tail G e ∈ verts H ∧ head G e ∈ verts H}⟧ ⟹ P"
shows "P"
using assms by (auto simp add: induced_subgraph_def)
lemma pverts_mk_symmetric[simp]: "pverts (mk_symmetric G) = verts G"
and parcs_mk_symmetric:
"parcs (mk_symmetric G) = (⋃e∈arcs G. {(tail G e, head G e), (head G e, tail G e)})"
by (auto simp: mk_symmetric_def arcs_ends_conv image_UN)
lemma arcs_ends_mono:
assumes "subgraph H G"
shows "arcs_ends H ⊆ arcs_ends G"
using assms by (auto simp add: subgraph_def arcs_ends_conv compatible_tail compatible_head)
lemma (in wf_digraph) subgraph_refl: "subgraph G G"
by (auto simp: subgraph_def compatible_def) unfold_locales
lemma (in wf_digraph) induced_subgraph_refl: "induced_subgraph G G"
by (rule induced_subgraphI) (auto simp: subgraph_refl)
subsection ‹The underlying symmetric graph of a digraph›
lemma (in wf_digraph) wellformed_mk_symmetric[intro]: "pair_wf_digraph (mk_symmetric G)"
by unfold_locales (auto simp: parcs_mk_symmetric)
lemma (in fin_digraph) pair_fin_digraph_mk_symmetric[intro]: "pair_fin_digraph (mk_symmetric G)"
proof -
have "finite ((λ(a,b). (b,a)) ` arcs_ends G)" (is "finite ?X") by (auto simp: arcs_ends_conv)
also have "?X = {(a, b). (b, a) ∈ arcs_ends G}" by auto
finally have X: "finite ..." .
then show ?thesis
by unfold_locales (auto simp: mk_symmetric_def arcs_ends_conv)
qed
lemma (in digraph) digraph_mk_symmetric[intro]: "pair_digraph (mk_symmetric G)"
proof -
have "finite ((λ(a,b). (b,a)) ` arcs_ends G)" (is "finite ?X") by (auto simp: arcs_ends_conv)
also have "?X = {(a, b). (b, a) ∈ arcs_ends G}" by auto
finally have "finite ..." .
then show ?thesis
by unfold_locales (auto simp: mk_symmetric_def arc_to_ends_def dest: no_loops)
qed
lemma (in wf_digraph) reachable_mk_symmetricI:
assumes "u →⇧* v" shows "u →⇧*⇘mk_symmetric G⇙ v"
proof -
have "arcs_ends G ⊆ parcs (mk_symmetric G)"
"(u, v) ∈ rtrancl_on (pverts (mk_symmetric G)) (arcs_ends G)"
using assms unfolding reachable_def by (auto simp: parcs_mk_symmetric)
then show ?thesis unfolding reachable_def by (auto intro: rtrancl_on_mono)
qed
lemma (in wf_digraph) adj_mk_symmetric_eq:
"symmetric G ⟹ parcs (mk_symmetric G) = arcs_ends G"
by (auto simp: parcs_mk_symmetric in_arcs_imp_in_arcs_ends arcs_ends_symmetric)
lemma (in wf_digraph) reachable_mk_symmetric_eq:
assumes "symmetric G" shows "u →⇧*⇘mk_symmetric G⇙ v ⟷ u →⇧* v" (is "?L ⟷ ?R")
using adj_mk_symmetric_eq[OF assms] unfolding reachable_def by auto
lemma (in wf_digraph) mk_symmetric_awalk_imp_awalk:
assumes sym: "symmetric G"
assumes walk: "pre_digraph.awalk (mk_symmetric G) u p v"
obtains q where "awalk u q v"
proof -
interpret S: pair_wf_digraph "mk_symmetric G" ..
from walk have "u →⇧*⇘mk_symmetric G⇙ v"
by (simp only: S.reachable_awalk) rule
then have "u →⇧* v" by (simp only: reachable_mk_symmetric_eq[OF sym])
then show ?thesis by (auto simp: reachable_awalk intro: that)
qed
lemma symmetric_mk_symmetric:
"symmetric (mk_symmetric G)"
by (auto simp: symmetric_def parcs_mk_symmetric intro: symI)
subsection ‹Subgraphs and Induced Subgraphs›
lemma subgraph_trans:
assumes "subgraph G H" "subgraph H I" shows "subgraph G I"
using assms by (auto simp: subgraph_def compatible_def)
text ‹
The @{term digraph} and @{term fin_digraph} properties are preserved under
the (inverse) subgraph relation
›
lemma (in fin_digraph) fin_digraph_subgraph:
assumes "subgraph H G" shows "fin_digraph H"
proof (intro_locales)
from assms show "wf_digraph H" by auto
have HG: "arcs H ⊆ arcs G" "verts H ⊆ verts G"
using assms by auto
then have "finite (verts H)" "finite (arcs H)"
using finite_verts finite_arcs by (blast intro: finite_subset)+
then show "fin_digraph_axioms H"
by unfold_locales
qed
lemma (in digraph) digraph_subgraph:
assumes "subgraph H G" shows "digraph H"
proof
fix e assume e: "e ∈ arcs H"
with assms show "tail H e ∈ verts H" "head H e ∈ verts H"
by (auto simp: subgraph_def intro: wf_digraph.wellformed)
from e and assms have "e ∈ arcs H ∩ arcs G" by auto
with assms show "tail H e ≠ head H e"
using no_loops by (auto simp: subgraph_def compatible_def arc_to_ends_def)
next
have "arcs H ⊆ arcs G" "verts H ⊆ verts G" using assms by auto
then show "finite (arcs H)" "finite (verts H)"
using finite_verts finite_arcs by (blast intro: finite_subset)+
next
fix e1 e2 assume "e1 ∈ arcs H" "e2 ∈ arcs H"
and eq: "arc_to_ends H e1 = arc_to_ends H e2"
with assms have "e1 ∈ arcs H ∩ arcs G" "e2 ∈ arcs H ∩ arcs G"
by auto
with eq show "e1 = e2"
using no_multi_arcs assms
by (auto simp: subgraph_def compatible_def arc_to_ends_def)
qed
lemma (in pre_digraph) adj_mono:
assumes "u →⇘H⇙ v" "subgraph H G"
shows "u → v"
using assms by (blast dest: arcs_ends_mono)
lemma (in pre_digraph) reachable_mono:
assumes walk: "u →⇧*⇘H⇙ v" and sub: "subgraph H G"
shows "u →⇧* v"
proof -
have "verts H ⊆ verts G" using sub by auto
with assms show ?thesis
unfolding reachable_def by (metis arcs_ends_mono rtrancl_on_mono)
qed
text ‹
Arc walks and paths are preserved under the subgraph relation.
›
lemma (in wf_digraph) subgraph_awalk_imp_awalk:
assumes walk: "pre_digraph.awalk H u p v"
assumes sub: "subgraph H G"
shows "awalk u p v"
using assms by (auto simp: pre_digraph.awalk_def compatible_cas)
lemma (in wf_digraph) subgraph_apath_imp_apath:
assumes path: "pre_digraph.apath H u p v"
assumes sub: "subgraph H G"
shows "apath u p v"
using assms unfolding pre_digraph.apath_def
by (auto intro: subgraph_awalk_imp_awalk simp: compatible_awalk_verts)
lemma subgraph_mk_symmetric:
assumes "subgraph H G"
shows "subgraph (mk_symmetric H) (mk_symmetric G)"
proof (rule subgraphI)
let ?wpms = "λG. mk_symmetric G"
from assms have "compatible G H" by auto
with assms
show "verts (?wpms H) ⊆ verts (?wpms G)"
and "arcs (?wpms H) ⊆ arcs (?wpms G)"
by (auto simp: parcs_mk_symmetric compatible_head compatible_tail)
show "compatible (?wpms G) (?wpms H)" by rule
interpret H: pair_wf_digraph "mk_symmetric H"
using assms by (auto intro: wf_digraph.wellformed_mk_symmetric)
interpret G: pair_wf_digraph "mk_symmetric G"
using assms by (auto intro: wf_digraph.wellformed_mk_symmetric)
show "wf_digraph (?wpms H)"
by unfold_locales
show "wf_digraph (?wpms G)" by unfold_locales
qed
lemma (in fin_digraph) subgraph_in_degree:
assumes "subgraph H G"
shows "in_degree H v ≤ in_degree G v"
proof -
have "finite (in_arcs G v)" by auto
moreover
have "in_arcs H v ⊆ in_arcs G v"
using assms by (auto simp: subgraph_def in_arcs_def compatible_head compatible_tail)
ultimately
show ?thesis unfolding in_degree_def by (rule card_mono)
qed
lemma (in wf_digraph) subgraph_cycle:
assumes "subgraph H G" "pre_digraph.cycle H p " shows "cycle p"
proof -
from assms have "compatible G H" by auto
with assms show ?thesis
by (auto simp: pre_digraph.cycle_def compatible_awalk_verts intro: subgraph_awalk_imp_awalk)
qed
lemma (in wf_digraph) subgraph_del_vert: "subgraph (del_vert u) G"
by (auto simp: subgraph_def compatible_def del_vert_simps wf_digraph_del_vert) intro_locales
lemma (in wf_digraph) subgraph_del_arc: "subgraph (del_arc a) G"
by (auto simp: subgraph_def compatible_def del_vert_simps wf_digraph_del_vert) intro_locales
subsection ‹Induced subgraphs›
lemma wf_digraphI_induced:
assumes "induced_subgraph H G"
shows "wf_digraph H"
proof -
from assms have "compatible G H" by auto
with assms show ?thesis by unfold_locales (auto simp: compatible_tail compatible_head)
qed
lemma (in digraph) digraphI_induced:
assumes "induced_subgraph H G"
shows "digraph H"
proof -
interpret W: wf_digraph H using assms by (rule wf_digraphI_induced)
from assms have "compatible G H" by auto
from assms have arcs: "arcs H ⊆ arcs G" by blast
show ?thesis
proof
from assms have "verts H ⊆ verts G" by blast
then show "finite (verts H)" using finite_verts by (rule finite_subset)
next
from arcs show "finite (arcs H)" using finite_arcs by (rule finite_subset)
next
fix e assume "e ∈ arcs H"
with arcs ‹compatible G H› show "tail H e ≠ head H e"
by (auto dest: no_loops simp: compatible_tail[symmetric] compatible_head[symmetric])
next
fix e1 e2 assume "e1 ∈ arcs H" "e2 ∈ arcs H" and ate: "arc_to_ends H e1 = arc_to_ends H e2"
with arcs ‹compatible G H› show "e1 = e2" using ate
by (auto intro: no_multi_arcs simp: compatible_tail[symmetric] compatible_head[symmetric] arc_to_ends_def)
qed
qed
text ‹Computes the subgraph of @{term G} induced by @{term vs}›
definition induce_subgraph :: "('a,'b) pre_digraph ⇒ 'a set ⇒ ('a,'b) pre_digraph" (infix "↾" 67) where
"G ↾ vs = ⦇ verts = vs, arcs = {e ∈ arcs G. tail G e ∈ vs ∧ head G e ∈ vs},
tail = tail G, head = head G ⦈"
lemma induce_subgraph_verts[simp]:
"verts (G ↾ vs) = vs"
by (auto simp add: induce_subgraph_def)
lemma induce_subgraph_arcs[simp]:
"arcs (G ↾ vs) = {e ∈ arcs G. tail G e ∈ vs ∧ head G e ∈ vs}"
by (auto simp add: induce_subgraph_def)
lemma induce_subgraph_tail[simp]:
"tail (G ↾ vs) = tail G"
by (auto simp: induce_subgraph_def)
lemma induce_subgraph_head[simp]:
"head (G ↾ vs) = head G"
by (auto simp: induce_subgraph_def)
lemma compatible_induce_subgraph: "compatible (G ↾ S) G"
by (auto simp: compatible_def)
lemma (in wf_digraph) induced_induce[intro]:
assumes "vs ⊆ verts G"
shows "induced_subgraph (G ↾ vs) G"
using assms
by (intro subgraphI induced_subgraphI)
(auto simp: arc_to_ends_def induce_subgraph_def wf_digraph_def compatible_def)
lemma (in wf_digraph) wellformed_induce_subgraph[intro]:
"wf_digraph (G ↾ vs)"
by unfold_locales auto
lemma induced_graph_imp_symmetric:
assumes "symmetric G"
assumes "induced_subgraph H G"
shows "symmetric H"
proof (unfold symmetric_conv, safe)
from assms have "compatible G H" by auto
fix e1 assume "e1 ∈ arcs H"
then obtain e2 where "tail G e1 = head G e2" "head G e1 = tail G e2" "e2 ∈ arcs G"
using assms by (auto simp add: symmetric_conv)
moreover
then have "e2 ∈ arcs H"
using assms and ‹e1 ∈ arcs H› by auto
ultimately
show "∃e2∈arcs H. tail H e1 = head H e2 ∧ head H e1 = tail H e2"
using assms ‹e1 ∈ arcs H› ‹compatible G H›
by (auto simp: compatible_head compatible_tail)
qed
lemma (in sym_digraph) induced_graph_imp_graph:
assumes "induced_subgraph H G"
shows "sym_digraph H"
proof (rule wf_digraph.sym_digraphI)
from assms show "wf_digraph H" by (rule wf_digraphI_induced)
next
show "symmetric H"
using assms sym_arcs by (auto intro: induced_graph_imp_symmetric)
qed
lemma (in wf_digraph) induce_reachable_preserves_paths:
assumes "u →⇧*⇘G⇙ v"
shows "u →⇧*⇘G ↾ {w. u →⇧*⇘G⇙ w}⇙ v"
using assms
proof induct
case base then show ?case by (auto simp: reachable_def)
next
case (step u w)
interpret iG: wf_digraph "G ↾ {w. u →⇧*⇘G⇙ w}"
by (rule wellformed_induce_subgraph)
from ‹u → w› have "u →⇘G ↾ {wa. u →⇧*⇘G⇙ wa}⇙ w"
by (auto simp: arcs_ends_conv reachable_def intro: wellformed rtrancl_on_into_rtrancl_on)
then have "u →⇧*⇘G ↾ {wa. u →⇧*⇘G⇙ wa}⇙ w"
by (rule iG.reachable_adjI)
moreover
from step have "{x. w →⇧* x} ⊆ {x. u →⇧* x}"
by (auto intro: adj_reachable_trans)
then have "subgraph (G ↾ {wa. w →⇧* wa}) (G ↾ {wa. u →⇧* wa})"
by (intro subgraphI) (auto simp: arcs_ends_conv compatible_def)
then have "w →⇧*⇘G ↾ {wa. u →⇧* wa}⇙ v"
by (rule iG.reachable_mono[rotated]) fact
ultimately show ?case by (rule iG.reachable_trans)
qed
lemma induce_subgraph_ends[simp]:
"arc_to_ends (G ↾ S) = arc_to_ends G"
by (auto simp: arc_to_ends_def)
lemma dominates_induce_subgraphD:
assumes "u →⇘G ↾ S⇙ v" shows "u →⇘G⇙ v"
using assms by (auto simp: arcs_ends_def intro: rev_image_eqI)
context wf_digraph begin
lemma reachable_induce_subgraphD:
assumes "u →⇧*⇘G ↾ S⇙ v" "S ⊆ verts G" shows "u →⇧*⇘G⇙ v"
proof -
interpret GS: wf_digraph "G ↾ S" by auto
show ?thesis
using assms by induct (auto dest: dominates_induce_subgraphD intro: adj_reachable_trans)
qed
lemma dominates_induce_ss:
assumes "u →⇘G ↾ S⇙ v" "S ⊆ T" shows "u →⇘G ↾ T⇙ v"
using assms by (auto simp: arcs_ends_def)
lemma reachable_induce_ss:
assumes "u →⇧*⇘G ↾ S⇙ v" "S ⊆ T" shows "u →⇧*⇘G ↾ T⇙ v"
using assms unfolding reachable_def
by induct (auto intro: dominates_induce_ss converse_rtrancl_on_into_rtrancl_on)
lemma awalk_verts_induce:
"pre_digraph.awalk_verts (G ↾ S) = awalk_verts"
proof (intro ext)
fix u p show "pre_digraph.awalk_verts (G ↾ S) u p = awalk_verts u p"
by (induct p arbitrary: u) (auto simp: pre_digraph.awalk_verts.simps)
qed
lemma (in -) cas_subset:
assumes "pre_digraph.cas G u p v" "subgraph G H"
shows "pre_digraph.cas H u p v"
using assms
by (induct p arbitrary: u) (auto simp: pre_digraph.cas.simps subgraph_def compatible_def)
lemma cas_induce:
assumes "cas u p v" "set (awalk_verts u p) ⊆ S"
shows "pre_digraph.cas (G ↾ S) u p v"
using assms
proof (induct p arbitrary: u S)
case Nil then show ?case by (auto simp: pre_digraph.cas.simps)
next
case (Cons a as)
have "pre_digraph.cas (G ↾ set (awalk_verts (head G a) as)) (head G a) as v"
using Cons by auto
then have "pre_digraph.cas (G ↾ S) (head G a) as v"
using ‹_ ⊆ S› by (rule_tac cas_subset) (auto simp: subgraph_def compatible_def)
then show ?case using Cons by (auto simp: pre_digraph.cas.simps)
qed
lemma awalk_induce:
assumes "awalk u p v" "set (awalk_verts u p) ⊆ S"
shows "pre_digraph.awalk (G ↾ S) u p v"
proof -
interpret GS: wf_digraph "G ↾ S" by auto
show ?thesis
using assms by (auto simp: pre_digraph.awalk_def cas_induce GS.cas_induce set_awalk_verts)
qed
lemma subgraph_induce_subgraphI:
assumes "V ⊆ verts G" shows "subgraph (G ↾ V) G"
by (metis assms induced_imp_subgraph induced_induce)
end
lemma induced_subgraphI':
assumes subg:"subgraph H G"
assumes max: "⋀H'. subgraph H' G ⟹ (verts H' ≠ verts H ∨ arcs H' ⊆ arcs H)"
shows "induced_subgraph H G"
proof -
interpret H: wf_digraph H using ‹subgraph H G› ..
define H' where "H' = G ↾ verts H"
then have H'_props: "subgraph H' G" "verts H' = verts H"
using subg by (auto intro: wf_digraph.subgraph_induce_subgraphI)
moreover
have "arcs H' = arcs H"
proof
show "arcs H' ⊆ arcs H" using max H'_props by auto
show "arcs H ⊆ arcs H'" using subg by (auto simp: H'_def compatible_def)
qed
then show "induced_subgraph H G" by (auto simp: induced_subgraph_def H'_def subg)
qed
lemma (in pre_digraph) induced_subgraph_altdef:
"induced_subgraph H G ⟷ subgraph H G ∧ (∀H'. subgraph H' G ⟶ (verts H' ≠ verts H ∨ arcs H' ⊆ arcs H))" (is "?L ⟷ ?R")
proof -
{ fix H' :: "('a,'b) pre_digraph"
assume A: "verts H' = verts H" "subgraph H' G"
interpret H': wf_digraph H' using ‹subgraph H' G› ..
from ‹subgraph H' G›
have comp: "tail G = tail H'" "head G = head H'" by (auto simp: compatible_def)
then have "⋀a. a ∈ arcs H' ⟹ tail G a ∈ verts H" "⋀a. a ∈ arcs H' ⟹ tail G a ∈ verts H"
by (auto dest: H'.wellformed simp: A)
then have "arcs H' ⊆ {e ∈ arcs G. tail G e ∈ verts H ∧ head G e ∈ verts H}"
using ‹subgraph H' G› by (auto simp: subgraph_def comp A(1)[symmetric])
}
then show ?thesis using induced_subgraphI'[of H G] by (auto simp: induced_subgraph_def)
qed
subsection ‹Unions of Graphs›
lemma
verts_union[simp]: "verts (union G H) = verts G ∪ verts H" and
arcs_union[simp]: "arcs (union G H) = arcs G ∪ arcs H" and
tail_union[simp]: "tail (union G H) = tail G" and
head_union[simp]: "head (union G H) = head G"
by (auto simp: union_def)
lemma wellformed_union:
assumes "wf_digraph G" "wf_digraph H" "compatible G H"
shows "wf_digraph (union G H)"
using assms
by unfold_locales
(auto simp: union_def compatible_tail compatible_head dest: wf_digraph.wellformed)
lemma subgraph_union_iff:
assumes "wf_digraph H1" "wf_digraph H2" "compatible H1 H2"
shows "subgraph (union H1 H2) G ⟷ subgraph H1 G ∧ subgraph H2 G"
using assms by (fastforce simp: compatible_def intro!: subgraphI wellformed_union)
lemma subgraph_union[intro]:
assumes "subgraph H1 G" "compatible H1 G"
assumes "subgraph H2 G" "compatible H2 G"
shows "subgraph (union H1 H2) G"
proof -
from assms have "wf_digraph (union H1 H2)"
by (auto intro: wellformed_union simp: compatible_def)
with assms show ?thesis
by (auto simp add: subgraph_def union_def arc_to_ends_def compatible_def)
qed
lemma union_fin_digraph:
assumes "fin_digraph G" "fin_digraph H" "compatible G H"
shows "fin_digraph (union G H)"
proof intro_locales
interpret G: fin_digraph G by (rule assms)
interpret H: fin_digraph H by (rule assms)
show "wf_digraph (union G H)" using assms
by (intro wellformed_union) intro_locales
show "fin_digraph_axioms (union G H)"
using assms by unfold_locales (auto simp: union_def)
qed
lemma subgraphs_of_union:
assumes "wf_digraph G" "wf_digraph G'" "compatible G G'"
shows "subgraph G (union G G')"
and "subgraph G' (union G G')"
using assms by (auto intro!: subgraphI wellformed_union simp: compatible_def)
subsection ‹Maximal Subgraphs›
lemma (in pre_digraph) max_subgraph_mp:
assumes "max_subgraph Q x" "⋀x. P x ⟹ Q x" "P x" shows "max_subgraph P x"
using assms by (auto simp: max_subgraph_def)
lemma (in pre_digraph) max_subgraph_prop: "max_subgraph P x ⟹ P x"
by (simp add: max_subgraph_def)
lemma (in pre_digraph) max_subgraph_subg_eq:
assumes "max_subgraph P H1" "max_subgraph P H2" "subgraph H1 H2"
shows "H1 = H2"
using assms by (auto simp: max_subgraph_def)
lemma subgraph_induce_subgraphI2:
assumes "subgraph H G" shows "subgraph H (G ↾ verts H)"
using assms by (auto simp: subgraph_def compatible_def wf_digraph.wellformed wf_digraph.wellformed_induce_subgraph)
definition arc_mono :: "(('a,'b) pre_digraph ⇒ bool) ⇒ bool" where
"arc_mono P ≡ (∀H1 H2. P H1 ∧ subgraph H1 H2 ∧ verts H1 = verts H2 ⟶ P H2)"
lemma (in pre_digraph) induced_subgraphI_arc_mono:
assumes "max_subgraph P H"
assumes "arc_mono P"
shows "induced_subgraph H G"
proof -
interpret wf_digraph G using assms by (auto simp: max_subgraph_def)
have "subgraph H (G ↾ verts H)" "subgraph (G ↾ verts H) G" "verts H = verts (G ↾ verts H)" "P H"
using assms by (auto simp: max_subgraph_def subgraph_induce_subgraphI2 subgraph_induce_subgraphI)
moreover
then have "P (G ↾ verts H)"
using assms by (auto simp: arc_mono_def)
ultimately
have "max_subgraph P (G ↾ verts H)"
using assms by (auto simp: max_subgraph_def) metis
then have "H = G ↾ verts H"
using ‹max_subgraph P H› ‹subgraph H _›
by (intro max_subgraph_subg_eq)
show ?thesis using assms by (subst ‹H = _›) (auto simp: max_subgraph_def)
qed
lemma (in pre_digraph) induced_subgraph_altdef2:
"induced_subgraph H G ⟷ max_subgraph (λH'. verts H' = verts H) H" (is "?L ⟷ ?R")
proof
assume ?L
moreover
{ fix H' assume "induced_subgraph H G" "subgraph H H'" "H ≠ H'"
then have "¬(subgraph H' G ∧ verts H' = verts H)"
by (auto simp: induced_subgraph_altdef compatible_def elim!: allE[where x=H'])
}
ultimately show "max_subgraph (λH'. verts H' = verts H) H" by (auto simp: max_subgraph_def)
next
assume ?R
moreover have "arc_mono (λH'. verts H' = verts H)" by (auto simp: arc_mono_def)
ultimately show ?L by (rule induced_subgraphI_arc_mono)
qed
lemma (in pre_digraph) max_subgraphI:
assumes "P x" "subgraph x G" "⋀y. ⟦x ≠ y; subgraph x y; subgraph y G⟧ ⟹ ¬P y"
shows "max_subgraph P x"
using assms by (auto simp: max_subgraph_def)
lemma (in pre_digraph) subgraphI_max_subgraph: "max_subgraph P x ⟹ subgraph x G"
by (simp add: max_subgraph_def)
subsection ‹Connected and Strongly Connected Graphs›
context wf_digraph begin
lemma in_sccs_verts_conv_reachable:
"S ∈ sccs_verts ⟷ S ≠ {} ∧ (∀u ∈ S. ∀v ∈ S. u →⇧*⇘G⇙ v) ∧ (∀u ∈ S. ∀v. v ∉ S ⟶ ¬u →⇧*⇘G⇙ v ∨ ¬v →⇧*⇘G⇙ u)"
by (simp add: sccs_verts_def)
lemma sccs_verts_disjoint:
assumes "S ∈ sccs_verts" "T ∈ sccs_verts" "S ≠ T" shows "S ∩ T = {}"
using assms unfolding in_sccs_verts_conv_reachable by safe meson+
lemma strongly_connected_spanning_imp_strongly_connected:
assumes "spanning H G"
assumes "strongly_connected H"
shows "strongly_connected G"
proof (unfold strongly_connected_def, intro ballI conjI)
from assms show "verts G ≠ {}" unfolding strongly_connected_def spanning_def by auto
next
fix u v assume "u ∈ verts G" and "v ∈ verts G"
then have "u →⇧*⇘H⇙ v" "subgraph H G"
using assms by (auto simp add: strongly_connected_def)
then show "u →⇧* v" by (rule reachable_mono)
qed
lemma strongly_connected_imp_induce_subgraph_strongly_connected:
assumes subg: "subgraph H G"
assumes sc: "strongly_connected H"
shows "strongly_connected (G ↾ (verts H))"
proof -
let ?is_H = "G ↾ (verts H)"
interpret H: wf_digraph H
using subg by (rule subgraphE)
interpret GrH: wf_digraph "?is_H"
by (rule wellformed_induce_subgraph)
have "verts H ⊆ verts G" using assms by auto
have "subgraph H (G ↾ verts H)"
using subg by (intro subgraphI) (auto simp: compatible_def)
then show ?thesis
using induced_induce[OF ‹verts H ⊆ verts G›]
and sc GrH.strongly_connected_spanning_imp_strongly_connected
unfolding spanning_def by auto
qed
lemma in_sccs_vertsI_sccs:
assumes "S ∈ verts ` sccs" shows "S ∈ sccs_verts"
unfolding sccs_verts_def
proof (intro CollectI conjI allI ballI impI)
show "S ≠ {}" using assms by (auto simp: sccs_verts_def sccs_def strongly_connected_def)
from assms have sc: "strongly_connected (G ↾ S)" "S ⊆ verts G"
apply (auto simp: sccs_verts_def sccs_def)
by (metis induced_imp_subgraph subgraphE wf_digraph.strongly_connected_imp_induce_subgraph_strongly_connected)
{
fix u v assume A: "u ∈ S" "v ∈ S"
with sc have "u →⇧*⇘G ↾ S⇙ v" by auto
then show "u →⇧*⇘G⇙ v" using ‹S ⊆ verts G› by (rule reachable_induce_subgraphD)
next
fix u v assume A: "u ∈ S" "v ∉ S"
{ assume B: "u →⇧*⇘G⇙ v" "v →⇧*⇘G⇙ u"
from B obtain p_uv where p_uv: "awalk u p_uv v" by (metis reachable_awalk)
from B obtain p_vu where p_vu: "awalk v p_vu u" by (metis reachable_awalk)
define T where "T = S ∪ set (awalk_verts u p_uv) ∪ set (awalk_verts v p_vu)"
have "S ⊆ T" by (auto simp: T_def)
have "v ∈ T" using p_vu by (auto simp: T_def set_awalk_verts)
then have "T ≠ S" using ‹v ∉ S› by auto
interpret T: wf_digraph "G ↾ T" by auto
from p_uv have T_p_uv: "T.awalk u p_uv v"
by (rule awalk_induce) (auto simp: T_def)
from p_vu have T_p_vu: "T.awalk v p_vu u"
by (rule awalk_induce) (auto simp: T_def)
have uv_reach: "u →⇧*⇘G ↾ T⇙ v" "v →⇧*⇘G ↾ T⇙ u"
using T_p_uv T_p_vu A by (metis T.reachable_awalk)+
{ fix x y assume "x ∈ S" "y ∈ S"
then have "x →⇧*⇘G ↾ S⇙ y" "y →⇧*⇘G ↾ S⇙ x"
using sc by auto
then have "x →⇧*⇘G ↾ T⇙ y" "y →⇧*⇘G ↾ T⇙ x"
using ‹S ⊆ T› by (auto intro: reachable_induce_ss)
} note A1 = this
{ fix x assume "x ∈ T"
moreover
{ assume "x ∈ S" then have "x →⇧*⇘G ↾ T⇙ v"
using uv_reach A1 A by (auto intro: T.reachable_trans[rotated])
} moreover
{ assume "x ∈ set (awalk_verts u p_uv)" then have "x →⇧*⇘G ↾ T⇙ v"
using T_p_uv by (auto simp: awalk_verts_induce intro: T.awalk_verts_reachable_to)
} moreover
{ assume "x ∈ set (awalk_verts v p_vu)" then have "x →⇧*⇘G ↾ T⇙ v"
using T_p_vu by (rule_tac T.reachable_trans)
(auto simp: uv_reach awalk_verts_induce dest: T.awalk_verts_reachable_to)
} ultimately
have "x →⇧*⇘G ↾ T⇙ v" by (auto simp: T_def)
} note xv_reach = this
{ fix x assume "x ∈ T"
moreover
{ assume "x ∈ S" then have "v →⇧*⇘G ↾ T⇙ x"
using uv_reach A1 A by (auto intro: T.reachable_trans)
} moreover
{ assume "x ∈ set (awalk_verts v p_vu)" then have "v →⇧*⇘G ↾ T⇙ x"
using T_p_vu by (auto simp: awalk_verts_induce intro: T.awalk_verts_reachable_from)
} moreover
{ assume "x ∈ set (awalk_verts u p_uv)" then have "v →⇧*⇘G ↾ T⇙ x"
using T_p_uv by (rule_tac T.reachable_trans[rotated])
(auto intro: T.awalk_verts_reachable_from uv_reach simp: awalk_verts_induce)
} ultimately
have "v →⇧*⇘G ↾ T⇙ x" by (auto simp: T_def)
} note vx_reach = this
{ fix x y assume "x ∈ T" "y ∈ T" then have "x →⇧*⇘G ↾ T⇙ y"
using xv_reach vx_reach by (blast intro: T.reachable_trans)
}
then have "strongly_connected (G ↾ T)"
using ‹S ≠ {}› ‹S ⊆ T› by auto
moreover have "induced_subgraph (G ↾ T) G"
using ‹S ⊆ verts G›
by (auto simp: T_def intro: awalk_verts_reachable_from p_uv p_vu reachable_in_verts(2))
ultimately
have "∃T. induced_subgraph (G ↾ T) G ∧ strongly_connected (G ↾ T) ∧ verts (G ↾ S) ⊂ verts (G ↾ T)"
using ‹S ⊆ T› ‹T ≠ S› by auto
then have "G ↾ S ∉ sccs" unfolding sccs_def by blast
then have "S ∉ verts ` sccs"
by (metis (erased, opaque_lifting) ‹S ⊆ T› ‹T ≠ S› ‹induced_subgraph (G ↾ T) G› ‹strongly_connected (G ↾ T)›
dual_order.order_iff_strict image_iff in_sccsE induce_subgraph_verts)
then have False using assms by metis
}
then show "¬u →⇧*⇘G⇙ v ∨ ¬v →⇧*⇘G⇙ u" by metis
}
qed
end
lemma arc_mono_strongly_connected[intro,simp]: "arc_mono strongly_connected"
by (auto simp: arc_mono_def) (metis spanning_def subgraphE wf_digraph.strongly_connected_spanning_imp_strongly_connected)
lemma (in pre_digraph) sccs_altdef2:
"sccs = {H. max_subgraph strongly_connected H}" (is "?L = ?R")
proof -
{ fix H H' :: "('a, 'b) pre_digraph"
assume a1: "strongly_connected H'"
assume a2: "induced_subgraph H' G"
assume a3: "max_subgraph strongly_connected H"
assume a4: "verts H ⊆ verts H'"
have sg: "subgraph H G" and ends_G: "tail G = tail H " "head G = head H"
using a3 by (auto simp: max_subgraph_def compatible_def)
then interpret H: wf_digraph H by blast
have "arcs H ⊆ arcs H'" using a2 a4 sg by (fastforce simp: ends_G)
then have "H = H'"
using a1 a2 a3 a4
by (metis (no_types) compatible_def induced_imp_subgraph max_subgraph_def subgraph_def)
} note X = this
{ fix H
assume a1: "induced_subgraph H G"
assume a2: "strongly_connected H"
assume a3: "∀H'. strongly_connected H' ⟶ induced_subgraph H' G ⟶ ¬ verts H ⊂ verts H'"
interpret G: wf_digraph G using a1 by auto
{ fix y assume "H ≠ y" and subg: "subgraph H y" "subgraph y G"
then have "verts H ⊂ verts y"
using a1 by (auto simp: induced_subgraph_altdef2 max_subgraph_def)
then have "¬strongly_connected y"
using subg a1 a2 a3[THEN spec, of "G ↾ verts y"]
by (auto simp: G.induced_induce G.strongly_connected_imp_induce_subgraph_strongly_connected)
}
then have "max_subgraph strongly_connected H"
using a1 a2 by (auto intro: max_subgraphI)
} note Y = this
show ?thesis unfolding sccs_def
by (auto dest: max_subgraph_prop X intro: induced_subgraphI_arc_mono Y)
qed
locale max_reachable_set = wf_digraph +
fixes S assumes S_in_sv: "S ∈ sccs_verts"
begin
lemma reach_in: "⋀u v. ⟦u ∈ S; v ∈ S⟧ ⟹ u →⇧*⇘G⇙ v"
and not_reach_out: "⋀u v. ⟦u ∈ S; v ∉ S⟧ ⟹ ¬u →⇧*⇘G⇙ v ∨ ¬v →⇧*⇘G⇙ u"
and not_empty: "S ≠ {}"
using S_in_sv by (auto simp: sccs_verts_def)
lemma reachable_induced:
assumes conn: "u ∈ S" "v ∈ S" "u →⇧*⇘G⇙ v"
shows "u →⇧*⇘G ↾ S⇙ v"
proof -
let ?H = "G ↾ S"
have "S ⊆ verts G" using reach_in by (auto dest: reachable_in_verts)
then have "induced_subgraph ?H G"
by (rule induced_induce)
then interpret H: wf_digraph ?H by (rule wf_digraphI_induced)
from conn obtain p where p: "awalk u p v" by (metis reachable_awalk)
show ?thesis
proof (cases "set p ⊆ arcs (G ↾ S)")
case True
with p conn have "H.awalk u p v"
by (auto simp: pre_digraph.awalk_def compatible_cas[OF compatible_induce_subgraph])
then show ?thesis by (metis H.reachable_awalk)
next
case False
then obtain a where "a ∈ set p" "a ∉ arcs (G ↾ S)" by auto
moreover
then have "tail G a ∉ S ∨ head G a ∉ S" using p by auto
ultimately
obtain w where "w ∈ set (awalk_verts u p)" "w ∉ S" using p by (auto simp: set_awalk_verts)
then have "u →⇧*⇘G⇙ w" "w →⇧*⇘G⇙ v"
using p by (auto intro: awalk_verts_reachable_from awalk_verts_reachable_to)
moreover have "v →⇧*⇘G⇙ u" using conn reach_in by auto
ultimately have "u →⇧*⇘G⇙ w" "w →⇧*⇘G⇙ u" by (auto intro: reachable_trans)
with ‹w ∉ S› conn not_reach_out have False by blast
then show ?thesis ..
qed
qed
lemma strongly_connected:
shows "strongly_connected (G ↾ S)"
using not_empty by (intro strongly_connectedI) (auto intro: reachable_induced reach_in)
lemma induced_in_sccs: "G ↾ S ∈ sccs"
proof -
let ?H = "G ↾ S"
have "S ⊆ verts G" using reach_in by (auto dest: reachable_in_verts)
then have "induced_subgraph ?H G"
by (rule induced_induce)
then interpret H: wf_digraph ?H by (rule wf_digraphI_induced)
{ fix T assume "S ⊂ T" "T ⊆ verts G" "strongly_connected (G ↾ T)"
from ‹S ⊂ T› obtain v where "v ∈ T" "v ∉ S" by auto
from not_empty obtain u where "u ∈ S" by auto
then have "u ∈ T" using ‹S ⊂ T› by auto
from ‹u ∈ S› ‹v ∉ S› have "¬u →⇧*⇘G⇙ v ∨ ¬v →⇧*⇘G⇙ u" by (rule not_reach_out)
moreover
from ‹strongly_connected _› have "u →⇧*⇘G ↾ T⇙ v" "v →⇧*⇘G ↾ T⇙ u"
using ‹v ∈ T› ‹u ∈ T› by (auto simp: strongly_connected_def)
then have "u →⇧*⇘G⇙ v" "v →⇧*⇘G⇙ u"
using ‹T ⊆ verts G› by (auto dest: reachable_induce_subgraphD)
ultimately have False by blast
} note psuper_not_sc = this
have "¬ (∃c'. induced_subgraph c' G ∧ strongly_connected c' ∧ verts (G ↾ S) ⊂ verts c')"
by (metis induce_subgraph_verts induced_imp_subgraph psuper_not_sc subgraphE
strongly_connected_imp_induce_subgraph_strongly_connected)
with ‹S ⊆ _› not_empty show "?H ∈ sccs" by (intro in_sccsI induced_induce strongly_connected)
qed
end
context wf_digraph begin
lemma in_verts_sccsD_sccs:
assumes "S ∈ sccs_verts"
shows "G ↾ S ∈ sccs"
proof -
from assms interpret max_reachable_set by unfold_locales
show ?thesis by (auto simp: sccs_verts_def intro: induced_in_sccs)
qed
lemma sccs_verts_conv: "sccs_verts = verts ` sccs"
by (auto intro: in_sccs_vertsI_sccs rev_image_eqI dest: in_verts_sccsD_sccs)
lemma induce_eq_iff_induced:
assumes "induced_subgraph H G" shows "G ↾ verts H = H"
using assms by (auto simp: induced_subgraph_def induce_subgraph_def compatible_def)
lemma sccs_conv_sccs_verts: "sccs = induce_subgraph G ` sccs_verts"
by (auto intro!: rev_image_eqI in_sccs_vertsI_sccs dest: in_verts_sccsD_sccs
simp: sccs_def induce_eq_iff_induced)
end
lemma connected_conv:
shows "connected G ⟷ verts G ≠ {} ∧ (∀u ∈ verts G. ∀v ∈ verts G. (u,v) ∈ rtrancl_on (verts G) ((arcs_ends G)⇧s))"
proof -
have "symcl (arcs_ends G) = parcs (mk_symmetric G)"
by (auto simp: parcs_mk_symmetric symcl_def arcs_ends_conv)
then show ?thesis by (auto simp: connected_def strongly_connected_def reachable_def)
qed
lemma (in wf_digraph) symmetric_connected_imp_strongly_connected:
assumes "symmetric G" "connected G"
shows "strongly_connected G"
proof
from ‹connected G› show "verts G ≠ {}" unfolding connected_def strongly_connected_def by auto
next
from ‹connected G›
have sc_mks: "strongly_connected (mk_symmetric G)"
unfolding connected_def by simp
fix u v assume "u ∈ verts G" "v ∈ verts G"
with sc_mks have "u →⇧*⇘mk_symmetric G⇙ v"
unfolding strongly_connected_def by auto
then show "u →⇧* v" using assms by (simp only: reachable_mk_symmetric_eq)
qed
lemma (in wf_digraph) connected_spanning_imp_connected:
assumes "spanning H G"
assumes "connected H"
shows "connected G"
proof (unfold connected_def strongly_connected_def, intro conjI ballI)
from assms show "verts (mk_symmetric G )≠ {}"
unfolding spanning_def connected_def strongly_connected_def by auto
next
fix u v
assume "u ∈ verts (mk_symmetric G)" and "v ∈ verts (mk_symmetric G)"
then have "u ∈ pverts (mk_symmetric H)" and "v ∈ pverts (mk_symmetric H)"
using ‹spanning H G› by (auto simp: mk_symmetric_def)
with ‹connected H›
have "u →⇧*⇘with_proj (mk_symmetric H)⇙ v" "subgraph (mk_symmetric H) (mk_symmetric G)"
using ‹spanning H G› unfolding connected_def
by (auto simp: spanning_def dest: subgraph_mk_symmetric)
then show "u →⇧*⇘mk_symmetric G⇙ v" by (rule pre_digraph.reachable_mono)
qed
lemma (in wf_digraph) spanning_tree_imp_connected:
assumes "spanning_tree H G"
shows "connected G"
using assms by (auto intro: connected_spanning_imp_connected)
term "LEAST x. P x"
lemma (in sym_digraph) induce_reachable_is_in_sccs:
assumes "u ∈ verts G"
shows "(G ↾ {v. u →⇧* v}) ∈ sccs"
proof -
let ?c = "(G ↾ {v. u →⇧* v})"
have isub_c: "induced_subgraph ?c G"
by (auto elim: reachable_in_vertsE)
then interpret c: wf_digraph ?c by (rule wf_digraphI_induced)
have sym_c: "symmetric (G ↾ {v. u →⇧* v})"
using sym_arcs isub_c by (rule induced_graph_imp_symmetric)
note ‹induced_subgraph ?c G›
moreover
have "strongly_connected ?c"
proof (rule strongly_connectedI)
show "verts ?c ≠ {}" using assms by auto
next
fix v w assume l_assms: "v ∈ verts ?c" "w ∈ verts ?c"
have "u →⇧*⇘G ↾ {v. u →⇧* v}⇙ v"
using l_assms by (intro induce_reachable_preserves_paths) auto
then have "v →⇧*⇘G ↾ {v. u →⇧* v}⇙ u" by (rule symmetric_reachable[OF sym_c])
also have "u →⇧*⇘G ↾ {v. u →⇧* v}⇙ w"
using l_assms by (intro induce_reachable_preserves_paths) auto
finally show "v →⇧*⇘G ↾ {v. u →⇧* v}⇙ w" .
qed
moreover
have "¬(∃d. induced_subgraph d G ∧ strongly_connected d ∧
verts ?c ⊂ verts d)"
proof
assume "∃d. induced_subgraph d G ∧ strongly_connected d ∧
verts ?c ⊂ verts d"
then obtain d where "induced_subgraph d G" "strongly_connected d"
"verts ?c ⊂ verts d" by auto
then obtain v where "v ∈ verts d" and "v ∉ verts ?c"
by auto
have "u ∈ verts ?c" using ‹u ∈ verts G› by auto
then have "u ∈ verts d" using ‹verts ?c ⊂ verts d› by auto
then have "u →⇧*⇘d⇙ v"
using ‹strongly_connected d› ‹u ∈ verts d› ‹v ∈ verts d› by auto
then have "u →⇧* v"
using ‹induced_subgraph d G›
by (auto intro: pre_digraph.reachable_mono)
then have "v ∈ verts ?c" by (auto simp: reachable_awalk)
then show False using ‹v ∉ verts ?c› by auto
qed
ultimately show ?thesis unfolding sccs_def by auto
qed
lemma induced_eq_verts_imp_eq:
assumes "induced_subgraph G H"
assumes "induced_subgraph G' H"
assumes "verts G = verts G'"
shows "G = G'"
using assms by (auto simp: induced_subgraph_def subgraph_def compatible_def)
lemma (in pre_digraph) in_sccs_subset_imp_eq:
assumes "c ∈ sccs"
assumes "d ∈ sccs"
assumes "verts c ⊆ verts d"
shows "c = d"
using assms by (blast intro: induced_eq_verts_imp_eq)
context wf_digraph begin
lemma connectedI:
assumes "verts G ≠ {}" "⋀u v. u ∈ verts G ⟹ v ∈ verts G ⟹ u →⇧*⇘mk_symmetric G⇙ v"
shows "connected G"
using assms by (auto simp: connected_def)
lemma connected_awalkE:
assumes "connected G" "u ∈ verts G" "v ∈ verts G"
obtains p where "pre_digraph.awalk (mk_symmetric G) u p v"
proof -
interpret sG: pair_wf_digraph "mk_symmetric G" ..
from assms have "u →⇧*⇘mk_symmetric G⇙ v" by (auto simp: connected_def)
then obtain p where "sG.awalk u p v" by (auto simp: sG.reachable_awalk)
then show ?thesis ..
qed
lemma inj_on_verts_sccs: "inj_on verts sccs"
by (rule inj_onI) (metis in_sccs_imp_induced induced_eq_verts_imp_eq)
lemma card_sccs_verts: "card sccs_verts = card sccs"
by (auto simp: sccs_verts_conv intro: inj_on_verts_sccs card_image)
end
lemma strongly_connected_non_disj:
assumes wf: "wf_digraph G" "wf_digraph H" "compatible G H"
assumes sc: "strongly_connected G" "strongly_connected H"
assumes not_disj: "verts G ∩ verts H ≠ {}"
shows "strongly_connected (union G H)"
proof
from sc show "verts (union G H) ≠ {}"
unfolding strongly_connected_def by simp
next
let ?x = "union G H"
fix u v w assume "u ∈ verts ?x" and "v ∈ verts ?x"
obtain w where w_in_both: "w ∈ verts G" "w ∈ verts H"
using not_disj by auto
interpret x: wf_digraph ?x
by (rule wellformed_union) fact+
have subg: "subgraph G ?x" "subgraph H ?x"
by (rule subgraphs_of_union[OF _ _ ], fact+)+
have reach_uw: "u →⇧*⇘?x⇙ w"
using ‹u ∈ verts ?x› subg w_in_both sc
by (auto intro: pre_digraph.reachable_mono)
also have reach_wv: "w →⇧*⇘?x⇙ v"
using ‹v ∈ verts ?x› subg w_in_both sc
by (auto intro: pre_digraph.reachable_mono)
finally (x.reachable_trans) show "u →⇧*⇘?x⇙ v" .
qed
context wf_digraph begin
lemma scc_disj:
assumes scc: "c ∈ sccs" "d ∈ sccs"
assumes "c ≠ d"
shows "verts c ∩ verts d = {}"
proof (rule ccontr)
assume contr: "¬?thesis"
let ?x = "union c d"
have comp1: "compatible G c" "compatible G d"
using scc by (auto simp: sccs_def)
then have comp: "compatible c d" by (auto simp: compatible_def)
have wf: "wf_digraph c" "wf_digraph d"
and sc: "strongly_connected c" "strongly_connected d"
using scc by (auto intro: in_sccs_imp_induced)
have "compatible c d"
using comp by (auto simp: sccs_def compatible_def)
from wf comp sc have union_conn: "strongly_connected ?x"
using contr by (rule strongly_connected_non_disj)
have sg: "subgraph ?x G"
using scc comp1 by (intro subgraph_union) (auto simp: compatible_def)
then have v_cd: "verts c ⊆ verts G" "verts d ⊆ verts G" by (auto elim!: subgraphE)
have "wf_digraph ?x" by (rule wellformed_union) fact+
with v_cd sg union_conn
have induce_subgraph_conn: "strongly_connected (G ↾ verts ?x)"
"induced_subgraph (G ↾ verts ?x) G"
by - (intro strongly_connected_imp_induce_subgraph_strongly_connected,
auto simp: subgraph_union_iff)
from assms have "¬verts c ⊆ verts d" and "¬ verts d ⊆ verts c"
by (metis in_sccs_subset_imp_eq)+
then have psub: "verts c ⊂ verts ?x"
by (auto simp: union_def)
then show False using induce_subgraph_conn
by (metis ‹c ∈ sccs› in_sccsE induce_subgraph_verts)
qed
lemma in_sccs_verts_conv:
"S ∈ sccs_verts ⟷ G ↾ S ∈ sccs"
by (auto simp: sccs_verts_conv intro: rev_image_eqI)
(metis in_sccs_imp_induced induce_subgraph_verts induced_eq_verts_imp_eq induced_imp_subgraph induced_induce subgraphE)
end
lemma (in wf_digraph) in_scc_of_self: "u ∈ verts G ⟹ u ∈ scc_of u"
by (auto simp: scc_of_def)
lemma (in wf_digraph) scc_of_empty_conv: "scc_of u = {} ⟷ u ∉ verts G"
using in_scc_of_self by (auto simp: scc_of_def reachable_in_verts)
lemma (in wf_digraph) scc_of_in_sccs_verts:
assumes "u ∈ verts G" shows "scc_of u ∈ sccs_verts"
using assms by (auto simp: in_sccs_verts_conv_reachable scc_of_def intro: reachable_trans exI[where x=u])
lemma (in wf_digraph) sccs_verts_subsets: "S ∈ sccs_verts ⟹ S ⊆ verts G"
by (auto simp: sccs_verts_conv)
lemma (in fin_digraph) finite_sccs_verts: "finite sccs_verts"
proof -
have "finite (Pow (verts G))" by auto
moreover with sccs_verts_subsets have "sccs_verts ⊆ Pow (verts G)" by auto
ultimately show ?thesis by (rule rev_finite_subset)
qed
lemma (in wf_digraph) sccs_verts_conv_scc_of:
"sccs_verts = scc_of ` verts G" (is "?L = ?R")
proof (intro set_eqI iffI)
fix S assume "S ∈ ?R" then show "S ∈ ?L"
by (auto simp: in_sccs_verts_conv_reachable scc_of_empty_conv) (auto simp: scc_of_def intro: reachable_trans)
next
fix S assume "S ∈ ?L"
moreover
then obtain u where "u ∈ S" by (auto simp: in_sccs_verts_conv_reachable)
moreover
then have "u ∈ verts G" using ‹S ∈ ?L› by (metis sccs_verts_subsets subsetCE)
then have "scc_of u ∈ sccs_verts" "u ∈ scc_of u"
by (auto intro: scc_of_in_sccs_verts in_scc_of_self)
ultimately
have "scc_of u = S" using sccs_verts_disjoint by blast
then show "S ∈ ?R" using ‹scc_of u ∈ _› ‹u ∈ verts G› by auto
qed
lemma (in sym_digraph) scc_ofI_reachable:
assumes "u →⇧* v" shows "u ∈ scc_of v"
using assms by (auto simp: scc_of_def symmetric_reachable[OF sym_arcs])
lemma (in sym_digraph) scc_ofI_reachable':
assumes "v →⇧* u" shows "u ∈ scc_of v"
using assms by (auto simp: scc_of_def symmetric_reachable[OF sym_arcs])
lemma (in sym_digraph) scc_ofI_awalk:
assumes "awalk u p v" shows "u ∈ scc_of v"
using assms by (metis reachable_awalk scc_ofI_reachable)
lemma (in sym_digraph) scc_ofI_apath:
assumes "apath u p v" shows "u ∈ scc_of v"
using assms by (metis reachable_apath scc_ofI_reachable)
lemma (in wf_digraph) scc_of_eq: "u ∈ scc_of v ⟹ scc_of u = scc_of v"
by (auto simp: scc_of_def intro: reachable_trans)
lemma (in wf_digraph) strongly_connected_eq_iff:
"strongly_connected G ⟷ sccs = {G}" (is "?L ⟷ ?R")
proof
assume ?L
then have "G ∈ sccs" by (auto simp: sccs_def induced_subgraph_refl)
moreover
{ fix H assume "H ∈ sccs" "G ≠ H"
with ‹G ∈ sccs› have "verts G ∩ verts H = {}" by (rule scc_disj)
moreover
from ‹H ∈ sccs› have "verts H ⊆ verts G" by auto
ultimately
have "verts H = {}" by auto
with ‹H ∈ sccs› have "False" by (auto simp: sccs_def strongly_connected_def)
} ultimately
show ?R by auto
qed (auto simp: sccs_def)
subsection ‹Components›
lemma (in sym_digraph) exists_scc:
assumes "verts G ≠ {}" shows "∃c. c ∈ sccs"
proof -
from assms obtain u where "u ∈ verts G" by auto
then show ?thesis by (blast dest: induce_reachable_is_in_sccs)
qed
theorem (in sym_digraph) graph_is_union_sccs:
shows "Union sccs = G"
proof -
have "(⋃c ∈ sccs. verts c) = verts G"
by (auto intro: induce_reachable_is_in_sccs)
moreover
have "(⋃c ∈ sccs. arcs c) = arcs G"
proof
show "(⋃c ∈ sccs. arcs c) ⊆ arcs G"
by safe (metis in_sccsE induced_imp_subgraph subgraphE subsetD)
show "arcs G ⊆ (⋃c ∈ sccs. arcs c)"
proof (safe)
fix e assume "e ∈ arcs G"
define a b where [simp]: "a = tail G e" and [simp]: "b = head G e"
have "e ∈ (⋃x ∈ sccs. arcs x)"
proof cases
assume "∃x∈sccs. {a,b } ⊆ verts x"
then obtain c where "c ∈ sccs" and "{a,b} ⊆ verts c"
by auto
then have "e ∈ {e ∈ arcs G. tail G e ∈ verts c
∧ head G e ∈ verts c}" using ‹e ∈ arcs G› by auto
then have "e ∈ arcs c" using ‹c ∈ sccs› by blast
then show ?thesis using ‹c ∈ sccs› by auto
next
assume l_assm: "¬(∃x∈sccs. {a,b} ⊆ verts x)"
have "a →⇧* b" using ‹e ∈ arcs G›
by (metis a_def b_def reachable_adjI in_arcs_imp_in_arcs_ends)
then have "{a,b} ⊆ verts (G ↾ {v. a →⇧* v})" "a ∈ verts G"
by (auto elim: reachable_in_vertsE)
moreover
have "(G ↾ {v. a →⇧* v}) ∈ sccs"
using ‹a ∈ verts G› by (auto intro: induce_reachable_is_in_sccs)
ultimately
have False using l_assm by blast
then show ?thesis by simp
qed
then show "e ∈ (⋃c ∈ sccs. arcs c)" by auto
qed
qed
ultimately show ?thesis
by (auto simp add: Union_def)
qed
lemma (in sym_digraph) scc_for_vert_ex:
assumes "u ∈ verts G"
shows "∃c. c∈sccs ∧ u ∈ verts c"
using assms by (auto intro: induce_reachable_is_in_sccs)
lemma (in sym_digraph) scc_decomp_unique:
assumes "S ⊆ sccs" "verts (Union S) = verts G" shows "S = sccs"
proof (rule ccontr)
assume "S ≠ sccs"
with assms obtain c where "c ∈ sccs" and "c ∉ S" by auto
with assms have "⋀d. d ∈ S ⟹ verts c ∩ verts d = {}"
by (intro scc_disj) auto
then have "verts c ∩ verts (Union S) = {}"
by (auto simp: Union_def)
with assms have "verts c ∩ verts G = {}" by auto
moreover from ‹c ∈ sccs› obtain u where "u ∈ verts c ∩ verts G"
by (auto simp: sccs_def strongly_connected_def)
ultimately show False by blast
qed
end