# Theory Bidirected_Digraph

```theory Bidirected_Digraph
imports
Digraph
"HOL-Combinatorics.Permutations"
begin

section ‹Bidirected Graphs›

locale bidirected_digraph = wf_digraph G for G +
fixes arev :: "'b ⇒ 'b"
assumes arev_dom: "⋀a. a ∈ arcs G ⟷ arev a ≠ a"
assumes arev_arev_raw: "⋀a. a ∈ arcs G ⟹ arev (arev a) = a"
assumes tail_arev[simp]: "⋀a. a ∈ arcs G ⟹ tail G (arev a) = head G a"

lemma (in wf_digraph) bidirected_digraphI:
assumes arev_eq: "⋀a. a ∉ arcs G ⟹ arev a = a"
assumes arev_neq: "⋀a. a ∈ arcs G ⟹ arev a ≠ a"
assumes arev_arev_raw: "⋀a. a ∈ arcs G ⟹ arev (arev a) = a"
assumes tail_arev: "⋀a. a ∈ arcs G ⟹ tail G (arev a) = head G a"
shows "bidirected_digraph G arev"
using assms by unfold_locales (auto simp: permutes_def)

context bidirected_digraph begin

lemma bidirected_digraph[intro!]: "bidirected_digraph G arev"
by unfold_locales

lemma arev_arev[simp]: "arev (arev a) = a"
using arev_dom by (cases "a ∈ arcs G") (auto simp: arev_arev_raw)

lemma arev_o_arev[simp]: "arev o arev = id"

lemma arev_eq: "a ∉ arcs G ⟹ arev a = a"

lemma arev_neq: "a ∈ arcs G ⟹ arev a ≠ a"

lemma arev_in_arcs[simp]: "a ∈ arcs G ⟹ arev a ∈ arcs G"
by (metis arev_arev arev_dom)

assumes "a ∈ arcs G" shows "head G (arev a) = tail G a"
proof -
from assms have "head G (arev a) = tail G (arev (arev a)) "
by (simp only: tail_arev arev_in_arcs)
then show ?thesis by simp
qed

lemma ate_arev[simp]:
assumes "a ∈ arcs G" shows "arc_to_ends G (arev a) = prod.swap (arc_to_ends G a)"
using assms by (auto simp: arc_to_ends_def)

lemma bij_arev: "bij arev"
using arev_arev by (metis bij_betw_imageI inj_on_inverseI surjI)

lemma arev_permutes_arcs: "arev permutes arcs G"
using arev_dom bij_arev by (auto simp: permutes_def bij_iff)

lemma arev_eq_iff: "⋀x y. arev x = arev y ⟷ x = y"
by (metis arev_arev)

lemma in_arcs_eq: "in_arcs G w = arev ` out_arcs G w"
by auto (metis arev_arev arev_in_arcs image_eqI in_out_arcs_conv tail_arev)

lemma inj_on_arev[intro!]: "inj_on arev S"
by (metis arev_arev inj_on_inverseI)

lemma even_card_loops:
"even (card (in_arcs G w ∩ out_arcs G w))" (is "even (card ?S)")
proof -
{ assume "¬finite ?S"
then have ?thesis by simp
}
moreover
{ assume A:"finite ?S"
have "card ?S = card (⋃{{a,arev a} | a. a ∈ ?S})" (is "_ = card (⋃ ?T)")
by (rule arg_cong[where f=card]) (auto intro!: exI[where x="{x, arev x}" for x])
also have "…= sum card ?T"
proof (rule card_Union_disjoint)
show "⋀A. A∈{{a, arev a} |a. a ∈ ?S} ⟹ finite A" by auto
show "pairwise disjnt {{a, arev a} |a. a ∈ in_arcs G w ∩ out_arcs G w}"
unfolding pairwise_def disjnt_def
qed
also have "… = sum (λa. 2) ?T"
by (intro sum.cong) (auto simp: card_insert_if dest: arev_neq)
also have "… = 2 * card ?T" by simp
finally have ?thesis by simp
}
ultimately
show ?thesis by blast
qed

end

(*XXX*)
sublocale bidirected_digraph ⊆ sym_digraph
proof (unfold_locales, unfold symmetric_def, intro symI)
fix u v assume "u →⇘G⇙ v"
then obtain a where "a ∈ arcs G" "arc_to_ends G a = (u,v)" by (auto simp: arcs_ends_def)
then have "arev a ∈ arcs G" "arc_to_ends G (arev a) = (v,u)"
by (auto simp: arc_to_ends_def)
then show "v →⇘G⇙ u" by (auto simp: arcs_ends_def intro: rev_image_eqI)
qed

end
```