Theory More_Graph_Theory
section ‹Additions to Lars Noschinski's Graph Library›
theory More_Graph_Theory
imports Graph_Theory.Graph_Theory
begin
lemma vwalkE2:
assumes "vwalk p G"
obtains u where "p = [u]" "u ∈ verts G"
| u v es where "p = u # v # es" "(u,v) ∈ arcs_ends G" "vwalk (v # es) G"
by (metis assms list.sel(1) vwalkE vwalk_consE vwalk_singleton vwalk_to_vpath.cases)
lemma (in wf_digraph) reachable_vwalk_conv2:
"u →⇧*⇘G⇙ v ⟷ (u = v ∧ u ∈ verts G ∨ (∃vs. vwalk (u # vs @ [v]) G))"
unfolding reachable_vwalk_conv
apply (rule iffI)
subgoal
apply (elim exE conjE)
apply (erule vwalkE2)
apply (simp; fail)
by (metis append_butlast_last_id last_ConsR list.distinct(1) list.sel(1) vwalk_Cons_Cons)
apply force
done
context pre_digraph
begin
definition
"scc_graph = ⦇
verts = sccs_verts,
arcs = {(x, y). ∃a ∈ x. ∃b ∈ y. x ≠ y ∧ x ∈ sccs_verts ∧ y ∈ sccs_verts ∧ a → b},
tail = fst,
head = snd
⦈"
interpretation scc_digraph: loopfree_digraph scc_graph
by standard (auto simp: scc_graph_def)
lemmas scc_digraphI = scc_digraph.loopfree_digraph_axioms
end
context wf_digraph
begin
interpretation scc_digraph: loopfree_digraph scc_graph
by (rule scc_digraphI)
lemma scc_graph_edgeE:
assumes ‹x →⇘scc_graph⇙ y› obtains a b where
"a ∈ x" "b ∈ y" "a → b" "x ∈ sccs_verts" "y ∈ sccs_verts" "x ≠ y"
using assms by (force simp: scc_graph_def dest!: in_arcs_imp_in_arcs_ends)
lemma same_sccI:
assumes "S ∈ sccs_verts" "x ∈ S" "x →⇧* y" "y →⇧* x"
shows "y ∈ S"
using assms by (auto simp: in_sccs_verts_conv_reachable)
lemma scc_graph_reachable1E:
assumes ‹x →⇧+⇘scc_graph⇙ y› obtains a b where
"x ∈ sccs_verts " "y ∈ sccs_verts " "x ≠ y" "a ∈ x" "b ∈ y" "a →⇧+ b"
using assms
proof (atomize_elim, induction)
case (base y)
then show ?case
by (auto elim!: scc_graph_edgeE)
next
case (step y z)
then obtain a b where IH: "x ∈ sccs_verts" "y ∈ sccs_verts" "a ∈ x" "b ∈ y" "a →⇧+ b" "x ≠ y"
by auto
from ‹y →⇘scc_graph⇙ z› obtain b' c where *:
"b' ∈ y" "c ∈ z" "b' → c" "y ∈ sccs_verts" "z ∈ sccs_verts"
by (elim scc_graph_edgeE)
with ‹b ∈ y› have "b →⇧* b'"
by (simp add: in_sccs_verts_conv_reachable)
with ‹b' → c› ‹a →⇧+ b› have "a →⇧+ c"
using reachable1_reachable_trans by blast
moreover have "x ≠ z"
proof (rule ccontr, unfold not_not)
assume "x = z"
with ‹a ∈ x› ‹c ∈ z› ‹x ∈ _› have "c →⇧* a"
by (simp add: in_sccs_verts_conv_reachable)
with ‹b →⇧* b'› ‹b' → c› have "b →⇧* a"
by (meson reachable_adj_trans reachable_trans)
with IH have "b ∈ x"
by - (rule same_sccI, auto)
with sccs_verts_disjoint IH show False
by auto
qed
ultimately show ?case
using IH * by auto
qed
end
locale dag = wf_digraph +
assumes acyclic: "x →⇧+ x ⟹ False"
locale fin_dag = fin_digraph + dag
context wf_digraph
begin
interpretation scc_digraph: loopfree_digraph scc_graph
by (rule scc_digraphI)
interpretation scc_digraph: dag scc_graph
by standard (auto elim: scc_graph_reachable1E)
lemmas scc_digraphI = scc_digraph.dag_axioms
end
context fin_digraph
begin
interpretation scc_digraph: dag scc_graph
by (rule scc_digraphI)
interpretation scc_digraph: fin_dag scc_graph
apply standard
unfolding scc_graph_def
subgoal finite_verts
by (simp add: finite_sccs_verts)
subgoal finite_arcs
using finite_sccs_verts
by - (rule finite_subset[where B = "{(x, y). x ∈ sccs_verts ∧ y ∈ sccs_verts}"], auto)
done
lemmas scc_digraphI = scc_digraph.fin_dag_axioms
end
end