# Theory Digraph

```(* Title:  Digraph.thy
Author: Lars Noschinski, TU München
Author: René Neumann
*)

theory Digraph
imports
Main
Rtrancl_On
Stuff
begin

section ‹Digraphs›

record ('a,'b) pre_digraph =
verts :: "'a set"
arcs :: "'b set"
tail :: "'b ⇒ 'a"
head :: "'b ⇒ 'a"

definition arc_to_ends :: "('a,'b) pre_digraph ⇒ 'b ⇒ 'a × 'a" where
"arc_to_ends G e ≡ (tail G e, head G e)"

locale pre_digraph =
fixes G :: "('a, 'b) pre_digraph" (structure)

locale wf_digraph = pre_digraph +
assumes tail_in_verts[simp]: "e ∈ arcs G ⟹ tail G e ∈ verts G"
assumes head_in_verts[simp]: "e ∈ arcs G ⟹ head G e ∈ verts G"
begin

lemma wf_digraph: "wf_digraph G" by intro_locales

lemmas wellformed = tail_in_verts head_in_verts

end

definition arcs_ends :: "('a,'b) pre_digraph ⇒ ('a × 'a) set" where
"arcs_ends G ≡ arc_to_ends G ` arcs G"

definition symmetric :: "('a,'b) pre_digraph ⇒ bool" where
"symmetric G ≡ sym (arcs_ends G)"

text ‹
Matches "pseudo digraphs" from \<^cite>‹"bangjensen2009digraphs"›, except for
allowing the null graph. For a discussion of that topic,
›
locale fin_digraph = wf_digraph +
assumes finite_verts[simp]: "finite (verts G)"
and finite_arcs[simp]: "finite (arcs G)"

locale loopfree_digraph = wf_digraph +
assumes no_loops: "e ∈ arcs G ⟹ tail G e ≠ head G e"

locale nomulti_digraph = wf_digraph +
assumes no_multi_arcs: "⋀e1 e2. ⟦e1 ∈ arcs G; e2 ∈ arcs G;
arc_to_ends G e1 = arc_to_ends G e2⟧ ⟹ e1 = e2"

locale sym_digraph = wf_digraph +
assumes sym_arcs[intro]: "symmetric G"

locale digraph = fin_digraph + loopfree_digraph + nomulti_digraph

text ‹
We model graphs as symmetric digraphs. This is fine for many purposes,
but not for all. For example, the path \$a,b,a\$ is considered to be a cycle
in a digraph (and hence in a symmetric digraph), but not in an undirected
graph.
›
locale pseudo_graph = fin_digraph + sym_digraph

locale graph = digraph + pseudo_graph

lemma (in wf_digraph) fin_digraphI[intro]:
assumes "finite (verts G)"
assumes "finite (arcs G)"
shows "fin_digraph G"
using assms by unfold_locales

lemma (in wf_digraph) sym_digraphI[intro]:
assumes "symmetric G"
shows "sym_digraph G"
using assms by unfold_locales

lemma (in digraph) graphI[intro]:
assumes "symmetric G"
shows "graph G"
using assms by unfold_locales

definition (in wf_digraph) arc :: "'b ⇒ 'a × 'a ⇒ bool" where
"arc e uv ≡ e ∈ arcs G ∧ tail G e = fst uv ∧ head G e = snd uv"

lemma (in fin_digraph) fin_digraph: "fin_digraph G"
by unfold_locales

lemma (in nomulti_digraph) nomulti_digraph: "nomulti_digraph G" by unfold_locales

lemma arcs_ends_conv: "arcs_ends G = (λe. (tail G e, head G e)) ` arcs G"
by (auto simp: arc_to_ends_def arcs_ends_def)

lemma symmetric_conv: "symmetric G ⟷ (∀e1 ∈ arcs G. ∃e2 ∈ arcs G. tail G e1 = head G e2 ∧ head G e1 = tail G e2)"
unfolding symmetric_def arcs_ends_conv sym_def by auto

lemma arcs_ends_symmetric:
assumes "symmetric G"
shows "(u,v) ∈ arcs_ends G ⟹ (v,u) ∈ arcs_ends G"
using assms unfolding symmetric_def sym_def by auto

lemma (in nomulti_digraph) inj_on_arc_to_ends:
"inj_on (arc_to_ends G) (arcs G)"
by (rule inj_onI) (rule no_multi_arcs)

subsection ‹Reachability›

abbreviation dominates :: "('a,'b) pre_digraph ⇒ 'a ⇒ 'a ⇒ bool" ("_ →ı _" [100,100] 40) where
"dominates G u v ≡ (u,v) ∈ arcs_ends G"

abbreviation reachable1 :: "('a,'b) pre_digraph ⇒ 'a ⇒ 'a ⇒ bool" ("_ →⇧+ı _" [100,100] 40) where
"reachable1 G u v ≡ (u,v) ∈ (arcs_ends G)^+"

definition reachable :: "('a,'b) pre_digraph ⇒ 'a ⇒ 'a ⇒ bool" ("_ →⇧*ı _" [100,100] 40) where
"reachable G u v ≡ (u,v) ∈ rtrancl_on (verts G) (arcs_ends G)"

lemma reachableE[elim]:
assumes "u →⇘G⇙ v"
obtains e where "e ∈ arcs G" "tail G e = u" "head G e = v"
using assms by (auto simp add: arcs_ends_conv)

lemma (in loopfree_digraph) adj_not_same:
assumes "a → a" shows "False"
using assms by (rule reachableE) (auto dest: no_loops)

lemma reachable_in_vertsE:
assumes "u →⇧*⇘G⇙ v" obtains "u ∈ verts G" "v ∈ verts G"
using assms unfolding reachable_def by induct auto

lemma symmetric_reachable:
assumes "symmetric G" "v →⇧*⇘G⇙ w" shows "w →⇧*⇘G⇙ v"
proof -
have "sym (rtrancl_on (verts G) (arcs_ends G))"
using assms by (auto simp add: symmetric_def dest: rtrancl_on_sym)
then show ?thesis using assms unfolding reachable_def by (blast elim: symE)
qed

lemma reachable_rtranclI:
"u →⇧*⇘G ⇙ v ⟹ (u, v) ∈ (arcs_ends G)⇧*"
unfolding reachable_def by (rule rtrancl_on_rtranclI)

context wf_digraph begin

assumes "u →⇘G⇙ v" shows "u ∈ verts G" "v ∈ verts G"
using assms unfolding arcs_ends_conv by auto

lemma dominatesI: assumes "arc_to_ends G a = (u,v)" "a ∈ arcs G" shows "u →⇘G⇙ v"
using assms by (auto simp: arcs_ends_def intro: rev_image_eqI)

lemma reachable_refl [intro!, Pure.intro!, simp]: "v ∈ verts G ⟹ v →⇧* v"
unfolding reachable_def by auto

assumes "a →⇘G⇙ b" "b →⇧*⇘G⇙ c" shows "a →⇧*⇘G⇙ c"
using assms by (auto simp: reachable_def intro: converse_rtrancl_on_into_rtrancl_on adj_in_verts)

assumes "a →⇧*⇘G⇙ b" "b →⇘G⇙ c" shows "a →⇧*⇘G⇙ c"
using assms by (auto simp: reachable_def intro: rtrancl_on_into_rtrancl_on adj_in_verts)

lemma reachable_adjI [intro, simp]: "u → v ⟹ u →⇧* v"

lemma reachable_trans[trans]:
assumes "u →⇧*v" "v →⇧* w" shows "u →⇧* w"
using assms unfolding reachable_def by (rule rtrancl_on_trans)

lemma reachable_induct[consumes 1, case_names base step]:
assumes major: "u →⇧*⇘G⇙ v"
and cases: "u ∈ verts G ⟹ P u"
"⋀x y. ⟦u →⇧*⇘G⇙ x; x →⇘G⇙ y; P x⟧ ⟹ P y"
shows "P v"
using assms unfolding reachable_def by (rule rtrancl_on_induct) auto

lemma converse_reachable_induct[consumes 1, case_names base step, induct pred: reachable]:
assumes major: "u →⇧*⇘G⇙ v"
and cases: "v ∈ verts G ⟹ P v"
"⋀x y. ⟦x →⇘G⇙ y; y →⇧*⇘G⇙ v; P y⟧ ⟹ P x"
shows "P u"
using assms unfolding reachable_def by (rule converse_rtrancl_on_induct) auto

lemma (in pre_digraph) converse_reachable_cases:
assumes "u →⇧*⇘G⇙ v"
obtains (base) "u = v" "u ∈ verts G"
| (step) w where "u →⇘G⇙ w" "w →⇧*⇘G⇙ v"
using assms unfolding reachable_def by (cases rule: converse_rtrancl_on_cases) auto

lemma reachable_in_verts:
assumes "u →⇧* v" shows "u ∈ verts G" "v ∈ verts G"
using assms by induct (simp_all add: adj_in_verts)

lemma reachable1_in_verts:
assumes "u →⇧+ v" shows "u ∈ verts G" "v ∈ verts G"
using assms

lemma reachable1_reachable[intro]:
"v →⇧+ w ⟹ v →⇧* w"
unfolding reachable_def
by (rule rtrancl_consistent_rtrancl_on) (simp_all add: reachable1_in_verts adj_in_verts)

lemmas reachable1_reachableE[elim] = reachable1_reachable[elim_format]

lemma reachable_neq_reachable1[intro]:
assumes reach: "v →⇧* w"
and neq: "v ≠ w"
shows "v →⇧+ w"
proof -
from reach have "(v,w) ∈ (arcs_ends G)^*" by (rule reachable_rtranclI)
with neq show ?thesis by (auto dest: rtranclD)
qed

lemmas reachable_neq_reachable1E[elim] = reachable_neq_reachable1[elim_format]

lemma reachable1_reachable_trans [trans]:
"u →⇧+ v ⟹ v →⇧* w ⟹ u →⇧+ w"
by (metis trancl_trans reachable_neq_reachable1)

lemma reachable_reachable1_trans [trans]:
"u →⇧* v ⟹ v →⇧+ w ⟹ u →⇧+ w"
by (metis trancl_trans reachable_neq_reachable1)

lemma reachable_conv:
"u →⇧* v ⟷ (u,v) ∈ (arcs_ends G)^* ∩ (verts G × verts G)"
apply (auto intro: reachable_in_verts)
apply (induct rule: rtrancl_induct)
apply auto
done

lemma reachable_conv':
assumes "u ∈ verts G"
shows "u →⇧* v ⟷ (u,v) ∈ (arcs_ends G)⇧*" (is "?L = ?R")
proof
assume "?R" then show "?L" using assms  by induct auto
qed (auto simp: reachable_conv)

end

lemma (in sym_digraph) symmetric_reachable':
assumes "v →⇧*⇘G⇙ w" shows "w →⇧*⇘G⇙ v"
using sym_arcs assms by (rule symmetric_reachable)

subsection ‹Degrees of vertices›

definition in_arcs :: "('a, 'b) pre_digraph ⇒ 'a ⇒ 'b set" where
"in_arcs G v ≡ {e ∈ arcs G. head G e = v}"

definition out_arcs :: "('a, 'b) pre_digraph ⇒ 'a ⇒ 'b set" where
"out_arcs G v ≡ {e ∈ arcs G. tail G e = v}"

definition in_degree :: "('a, 'b) pre_digraph ⇒ 'a ⇒ nat" where
"in_degree G v ≡ card (in_arcs G v)"

definition out_degree :: "('a, 'b) pre_digraph ⇒ 'a ⇒ nat" where
"out_degree G v ≡ card (out_arcs G v)"

lemma (in fin_digraph) finite_in_arcs[intro]:
"finite (in_arcs G v)"
unfolding in_arcs_def by auto

lemma (in fin_digraph) finite_out_arcs[intro]:
"finite (out_arcs G v)"
unfolding out_arcs_def by auto

lemma in_in_arcs_conv[simp]:
"e ∈ in_arcs G v ⟷ e ∈ arcs G ∧ head G e = v"
unfolding in_arcs_def by auto

lemma in_out_arcs_conv[simp]:
"e ∈ out_arcs G v ⟷ e ∈ arcs G ∧ tail G e = v"
unfolding out_arcs_def by auto

lemma inout_arcs_arc_simps[simp]:
assumes "e ∈ arcs G"
shows "tail G e = u ⟹ out_arcs G u ∩ insert e E = insert e (out_arcs G u ∩ E)"
"tail G e ≠ u ⟹ out_arcs G u ∩ insert e E = out_arcs G u ∩ E"
"out_arcs G u ∩ {} = {}" (* XXX: should be unnecessary *)
"head G e = u ⟹ in_arcs G u ∩ insert e E = insert e (in_arcs G u ∩ E)"
"head G e ≠ u ⟹ in_arcs G u ∩ insert e E = in_arcs G u ∩ E"
"in_arcs G u ∩ {} = {}" (* XXX: should be unnecessary *)
using assms by auto

lemma in_arcs_int_arcs[simp]: "in_arcs G u ∩ arcs G = in_arcs G u" and
out_arcs_int_arcs[simp]: "out_arcs G u ∩ arcs G = out_arcs G u"
by auto

lemma in_arcs_in_arcs: "x ∈ in_arcs G u ⟹ x ∈ arcs G"
and out_arcs_in_arcs: "x ∈ out_arcs G u ⟹ x ∈ arcs G"
by (auto simp: in_arcs_def out_arcs_def)

subsection ‹Graph operations›

context pre_digraph begin

definition add_arc :: "'b ⇒  ('a,'b) pre_digraph" where
"add_arc a = ⦇ verts = verts G ∪ {tail G a, head G a}, arcs = insert a (arcs G), tail = tail G, head = head G ⦈"

definition  del_arc :: "'b ⇒ ('a,'b) pre_digraph" where
"del_arc a = ⦇ verts = verts G, arcs = arcs G - {a}, tail = tail G, head = head G ⦈"

definition add_vert :: "'a ⇒  ('a,'b) pre_digraph" where
"add_vert v = ⦇ verts = insert v (verts G), arcs = arcs G, tail = tail G, head = head G ⦈"

definition del_vert :: "'a ⇒  ('a,'b) pre_digraph" where
"del_vert v = ⦇ verts = verts G - {v}, arcs = {a ∈ arcs G. tail G a ≠ v ∧ head G a ≠ v}, tail = tail G, head = head G ⦈"

lemma
verts_add_arc: "⟦ tail G a ∈ verts G; head G a ∈ verts G ⟧ ⟹ verts (add_arc a) = verts G"  and
verts_add_arc_conv: "verts (add_arc a) = verts G ∪ {tail G a, head G a}" and
arcs_add_arc: "arcs (add_arc a) = insert a (arcs G)" and
tail_add_arc: "tail (add_arc a) = tail G" and
by (auto simp: add_arc_def)

lemma
verts_del_arc: "verts (del_arc a) = verts G"  and
arcs_del_arc: "arcs (del_arc a) = arcs G - {a}" and
tail_del_arc: "tail (del_arc a) = tail G" and
by (auto simp: del_arc_def)

lemmas del_arc_simps[simp] = verts_del_arc arcs_del_arc tail_del_arc head_del_arc

lemma
verts_add_vert: "verts (pre_digraph.add_vert G u) = insert u (verts G)" and
arcs_add_vert: "arcs (pre_digraph.add_vert G u) = arcs G" and
tail_add_vert: "tail (pre_digraph.add_vert G u) = tail G" and
by (auto simp: pre_digraph.add_vert_def)

lemma
verts_del_vert: "verts (pre_digraph.del_vert G u) = verts G - {u}" and
arcs_del_vert: "arcs (pre_digraph.del_vert G u) = {a ∈ arcs G. tail G a ≠ u ∧ head G a ≠ u}" and
tail_del_vert: "tail (pre_digraph.del_vert G u) = tail G" and
ends_del_vert: "arc_to_ends (pre_digraph.del_vert G u) = arc_to_ends G"
by (auto simp: pre_digraph.del_vert_def arc_to_ends_def)

lemmas del_vert_simps = verts_del_vert arcs_del_vert tail_del_vert head_del_vert

by (auto simp: pre_digraph.add_arc_def)

"⟦ tail G a ∈ verts G; head G a ∈ verts G ⟧ ⟹ pre_digraph.del_arc (add_arc a) a = del_arc a"
by (auto simp: pre_digraph.add_arc_simps pre_digraph.del_arc_simps)

lemma del_del_arc_collapse[simp]: "pre_digraph.del_arc (del_arc a) a = del_arc a"
by (auto simp: pre_digraph.add_arc_simps pre_digraph.del_arc_simps)

by (auto simp: pre_digraph.add_arc_def)

lemma del_arc_commute: "pre_digraph.del_arc (del_arc b) a = pre_digraph.del_arc (del_arc a) b"
by (auto simp: pre_digraph.del_arc_def)

lemma del_arc_in: "a ∉ arcs G ⟹ del_arc a = G"
by (rule pre_digraph.equality) (auto simp: add_arc_def)

"in_arcs (add_arc a) u = (if head G a = u then insert a (in_arcs G u) else in_arcs G u)"
by auto

"out_arcs (add_arc a) u = (if tail G a = u then insert a (out_arcs G u) else out_arcs G u)"
by auto

lemma in_arcs_del_arc_iff:
"in_arcs (del_arc a) u = (if head G a = u then in_arcs G u - {a} else in_arcs G u)"
by auto

lemma out_arcs_del_arc_iff:
"out_arcs (del_arc a) u = (if tail G a = u then out_arcs G u - {a} else out_arcs G u)"
by auto

lemma (in wf_digraph) add_arc_in: "a ∈ arcs G ⟹ add_arc a = G"
by (rule pre_digraph.equality) (auto simp: add_arc_def)

end

context wf_digraph begin

"wf_digraph (add_arc a)" by unfold_locales (auto simp: verts_add_arc_conv)

lemma wf_digraph_del_arc[intro]:
"wf_digraph (del_arc a)" by unfold_locales (auto simp: verts_add_arc_conv)

lemma wf_digraph_del_vert: "wf_digraph (del_vert u)"
by standard (auto simp: del_vert_simps)

by standard (auto simp: add_vert_simps)

assumes "u ∉ verts G"
shows "pre_digraph.del_vert (add_vert u) u = G"
using assms by (intro pre_digraph.equality) (auto simp: pre_digraph.del_vert_def add_vert_def)

end

context fin_digraph begin

"in_degree (add_arc a) u = (if head G a = u ∧ a ∉ arcs G then in_degree G u + 1 else in_degree G u)"
proof -
have "a ∉ arcs G ⟹ a ∉ in_arcs G u" by (auto simp: in_arcs_def)
with finite_in_arcs show ?thesis
unfolding in_degree_def by (auto simp: in_arcs_add_arc_iff intro: arg_cong[where f=card])
qed

"out_degree (add_arc a) u = (if tail G a = u ∧ a ∉ arcs G then out_degree G u + 1 else out_degree G u)"
proof -
have "a ∉ arcs G ⟹ a ∉ out_arcs G u" by (auto simp: out_arcs_def)
with finite_out_arcs show ?thesis
unfolding out_degree_def by (auto simp: out_arcs_add_arc_iff intro: arg_cong[where f=card])
qed

lemma in_degree_del_arc_iff:
"in_degree (del_arc a) u = (if head G a = u ∧ a ∈ arcs G then in_degree G u - 1 else in_degree G u)"
proof -
have "a ∉ arcs G ⟹ a ∉ in_arcs G u" by (auto simp: in_arcs_def)
with finite_in_arcs show ?thesis
unfolding in_degree_def by (auto simp: in_arcs_del_arc_iff intro: arg_cong[where f=card])
qed

lemma out_degree_del_arc_iff:
"out_degree (del_arc a) u = (if tail G a = u ∧ a ∈ arcs G then out_degree G u - 1 else out_degree G u)"
proof -
have "a ∉ arcs G ⟹ a ∉ out_arcs G u" by (auto simp: out_arcs_def)
with finite_out_arcs show ?thesis
unfolding out_degree_def by (auto simp: out_arcs_del_arc_iff intro: arg_cong[where f=card])
qed

lemma fin_digraph_del_vert: "fin_digraph (del_vert u)"
by standard (auto simp: del_vert_simps)

lemma fin_digraph_del_arc: "fin_digraph (del_arc a)"
by standard (auto simp: del_vert_simps)

end

end
```