(* Title: Digraph_Component.thy Author: Lars Noschinski, TU München *) 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" (* Require @{term "wf_digraph G"}? *) 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)}" (*XXX: "sccs_verts = verts ` sccs" *) 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 (*XXX*) 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