Theory Graph_Theory.Euler
theory Euler imports
Arc_Walk
Digraph_Component
Digraph_Isomorphism
begin
section ‹Euler Trails in Digraphs›
text ‹
In this section we prove the well-known theorem characterizing the
existence of an Euler Trail in an directed graph
›
subsection ‹Trails and Euler Trails›
definition (in pre_digraph) euler_trail :: "'a ⇒ 'b awalk ⇒ 'a ⇒ bool" where
"euler_trail u p v ≡ trail u p v ∧ set p = arcs G ∧ set (awalk_verts u p) = verts G"
context wf_digraph begin
lemma finite_distinct:
assumes "finite A" shows "finite {p. distinct p ∧ set p ⊆ A}"
proof -
have "{p. distinct p ∧ set p ⊆ A} ⊆ {p. set p ⊆ A ∧ length p ≤ card A}"
using assms by (auto simp: distinct_card[symmetric] intro: card_mono)
also have "finite ..."
using assms by (simp add: finite_lists_length_le)
finally (finite_subset) show ?thesis .
qed
lemma (in fin_digraph) trails_finite: "finite {p. ∃u v. trail u p v}"
proof -
have "{p. ∃u v. trail u p v} ⊆ {p. distinct p ∧ set p ⊆ arcs G}"
by (auto simp: trail_def)
with finite_arcs finite_distinct show ?thesis by (blast intro: finite_subset)
qed
lemma rotate_awalkE:
assumes "awalk u p u" "w ∈ set (awalk_verts u p)"
obtains q r where "p = q @ r" "awalk w (r @ q) w" "set (awalk_verts w (r @ q)) = set (awalk_verts u p)"
proof -
from assms obtain q r where A: "p = q @ r" and A': "awalk u q w" "awalk w r u"
by atomize_elim (rule awalk_decomp)
then have B: "awalk w (r @ q) w" by auto
have C: "set (awalk_verts w (r @ q)) = set (awalk_verts u p)"
using ‹awalk u p u› A A' by (auto simp: set_awalk_verts_append)
from A B C show ?thesis ..
qed
lemma rotate_trailE:
assumes "trail u p u" "w ∈ set (awalk_verts u p)"
obtains q r where "p = q @ r" "trail w (r @ q) w" "set (awalk_verts w (r @ q)) = set (awalk_verts u p)"
using assms by - (rule rotate_awalkE[where u=u and p=p and w=w], auto simp: trail_def)
lemma rotate_trailE':
assumes "trail u p u" "w ∈ set (awalk_verts u p)"
obtains q where "trail w q w" "set q = set p" "set (awalk_verts w q) = set (awalk_verts u p)"
proof -
from assms obtain q r where "p = q @ r" "trail w (r @ q) w" "set (awalk_verts w (r @ q)) = set (awalk_verts u p)"
by (rule rotate_trailE)
then have "set (r @ q) = set p" by auto
show ?thesis by (rule that) fact+
qed
lemma sym_reachableI_in_awalk:
assumes walk: "awalk u p v" and
w1: "w1 ∈ set (awalk_verts u p)" and w2: "w2 ∈ set (awalk_verts u p)"
shows "w1 →⇧*⇘mk_symmetric G⇙ w2"
proof -
from walk w1 obtain q r where "p = q @ r" "awalk u q w1" "awalk w1 r v"
by (atomize_elim) (rule awalk_decomp)
then have w2_in: "w2 ∈ set (awalk_verts u q) ∪ set (awalk_verts w1 r)"
using w2 by (auto simp: set_awalk_verts_append)
show ?thesis
proof cases
assume A: "w2 ∈ set (awalk_verts u q)"
obtain s where "awalk w2 s w1"
using awalk_decomp[OF ‹awalk u q w1› A] by blast
then have "w2 →⇧*⇘mk_symmetric G⇙ w1"
by (intro reachable_awalkI reachable_mk_symmetricI)
with symmetric_mk_symmetric show ?thesis by (rule symmetric_reachable)
next
assume "w2 ∉ set (awalk_verts u q)"
then have A: "w2 ∈ set (awalk_verts w1 r)"
using w2_in by blast
obtain s where "awalk w1 s w2"
using awalk_decomp[OF ‹awalk w1 r v› A] by blast
then show "w1 →⇧*⇘mk_symmetric G⇙ w2"
by (intro reachable_awalkI reachable_mk_symmetricI)
qed
qed
lemma euler_imp_connected:
assumes "euler_trail u p v" shows "connected G"
proof -
{ have "verts G ≠ {}" using assms unfolding euler_trail_def trail_def by auto }
moreover
{ fix w1 w2 assume "w1 ∈ verts G" "w2 ∈ verts G"
then have "awalk u p v " "w1 ∈ set (awalk_verts u p)" "w2 ∈ set (awalk_verts u p)"
using assms by (auto simp: euler_trail_def trail_def)
then have "w1 →⇧*⇘mk_symmetric G⇙ w2" by (rule sym_reachableI_in_awalk) }
ultimately show "connected G" by (rule connectedI)
qed
end
subsection ‹Arc Balance of Walks›
context pre_digraph begin
definition arc_set_balance :: "'a ⇒ 'b set ⇒ int" where
"arc_set_balance w A = int (card (in_arcs G w ∩ A)) - int (card (out_arcs G w ∩ A))"
definition arc_set_balanced :: "'a ⇒ 'b set ⇒ 'a ⇒ bool" where
"arc_set_balanced u A v ≡
if u = v then (∀w ∈ verts G. arc_set_balance w A = 0)
else (∀w ∈ verts G. (w ≠ u ∧ w ≠ v) ⟶ arc_set_balance w A = 0)
∧ arc_set_balance u A = -1
∧ arc_set_balance v A = 1"
abbreviation arc_balance :: "'a ⇒ 'b awalk ⇒ int" where
"arc_balance w p ≡ arc_set_balance w (set p)"
abbreviation arc_balanced :: "'a ⇒ 'b awalk ⇒ 'a ⇒ bool" where
"arc_balanced u p v ≡ arc_set_balanced u (set p) v"
lemma arc_set_balanced_all:
"arc_set_balanced u (arcs G) v =
(if u = v then (∀w ∈ verts G. in_degree G w = out_degree G w)
else (∀w ∈ verts G. (w ≠ u ∧ w ≠ v) ⟶ in_degree G w = out_degree G w)
∧ in_degree G u + 1 = out_degree G u
∧ out_degree G v + 1 = in_degree G v)"
unfolding arc_set_balanced_def arc_set_balance_def in_degree_def out_degree_def by auto
end
context wf_digraph begin
lemma arc_balance_Cons:
assumes "trail u (e # es) v"
shows "arc_set_balance w (insert e (set es)) = arc_set_balance w {e} + arc_balance w es"
proof -
from assms have "e ∉ set es" "e ∈ arcs G" by (auto simp: trail_def)
with ‹e ∉ set es› show ?thesis
apply (cases "w = tail G e")
apply (case_tac [!] "w = head G e")
apply (auto simp: arc_set_balance_def)
done
qed
lemma arc_balancedI_trail:
assumes "trail u p v" shows "arc_balanced u p v"
using assms
proof (induct p arbitrary: u)
case Nil then show ?case by (auto simp: arc_set_balanced_def arc_set_balance_def trail_def)
next
case (Cons e es)
then have "arc_balanced (head G e) es v" "u = tail G e" "e ∈ arcs G"
by (auto simp: awalk_Cons_iff trail_def)
moreover
have "⋀w. arc_balance w [e] = (if w = tail G e ∧ tail G e ≠ head G e then -1
else if w = head G e ∧ tail G e ≠ head G e then 1 else 0)"
using ‹e ∈ _› by (case_tac "w = tail G e") (auto simp: arc_set_balance_def)
ultimately show ?case
by (auto simp: arc_set_balanced_def arc_balance_Cons[OF ‹trail u _ _›])
qed
lemma trail_arc_balanceE:
assumes "trail u p v"
obtains "⋀w. ⟦ u = v ∨ (w ≠ u ∧ w ≠ v); w ∈ verts G ⟧
⟹ arc_balance w p = 0"
and "⟦ u ≠ v ⟧ ⟹ arc_balance u p = - 1"
and "⟦ u ≠ v ⟧ ⟹ arc_balance v p = 1"
using arc_balancedI_trail[OF assms] unfolding arc_set_balanced_def by (intro that) (metis,presburger+)
end
subsection ‹Closed Euler Trails›
lemma (in wf_digraph) awalk_vertex_props:
assumes "awalk u p v" "p ≠ []"
assumes "⋀w. w ∈ set (awalk_verts u p) ⟹ P w ∨ Q w"
assumes "P u" "Q v"
shows "∃e ∈ set p. P (tail G e) ∧ Q (head G e)"
using assms(2,1,3-)
proof (induct p arbitrary: u rule: list_nonempty_induct)
case (cons e es)
show ?case
proof (cases "P (tail G e) ∧ Q (head G e)")
case False
then have "P (head G e) ∨ Q (head G e)"
using cons.prems(1) cons.prems(2)[of "head G e"]
by (auto simp: awalk_Cons_iff set_awalk_verts)
then have "P (tail G e) ∧ P (head G e)"
using False using cons.prems(1,3) by auto
then have "∃e ∈ set es. P (tail G e) ∧ Q (head G e)"
using cons by (auto intro: cons simp: awalk_Cons_iff)
then show ?thesis by auto
qed auto
qed (simp add: awalk_simps)
lemma (in wf_digraph) connected_verts:
assumes "connected G" "arcs G ≠ {}"
shows "verts G = tail G ` arcs G ∪ head G ` arcs G"
proof -
{ assume "verts G = {}" then have ?thesis by (auto dest: tail_in_verts) }
moreover
{ assume "∃v. verts G = {v}"
then obtain v where "verts G = {v}" by (auto simp: card_Suc_eq)
moreover
with ‹arcs G ≠ {}› obtain e where "e ∈ arcs G" "tail G e = v" "head G e = v"
by (auto dest: tail_in_verts head_in_verts)
moreover have "tail G ` arcs G ∪ head G ` arcs G ⊆ verts G" by auto
ultimately have ?thesis by auto }
moreover
{ assume A: "∃u v. u ∈ verts G ∧ v ∈ verts G ∧ u ≠ v"
{ fix u assume "u ∈ verts G"
interpret S: pair_wf_digraph "mk_symmetric G" by rule
from A obtain v where "v ∈ verts G" "u ≠ v" by blast
then obtain p where "S.awalk u p v"
using ‹connected G› ‹u ∈ verts G› by (auto elim: connected_awalkE)
with ‹u ≠ v› obtain e where "e ∈ parcs (mk_symmetric G)" "fst e = u"
by (metis S.awalk_Cons_iff S.awalk_empty_ends list_exhaust2)
then obtain e' where "tail G e' = u ∨ head G e' = u" "e' ∈ arcs G"
by (force simp: parcs_mk_symmetric)
then have "u ∈ tail G ` arcs G ∪ head G `arcs G" by auto }
then have ?thesis by auto }
ultimately show ?thesis by blast
qed
lemma (in wf_digraph) connected_arcs_empty:
assumes "connected G" "arcs G = {}" "verts G ≠ {}" obtains v where "verts G = {v}"
proof (atomize_elim, rule ccontr)
assume A: "¬ (∃v. verts G = {v})"
interpret S: pair_wf_digraph "mk_symmetric G" by rule
from ‹verts G ≠ {}› obtain u where "u ∈ verts G" by auto
with A obtain v where "v ∈ verts G" "u ≠ v" by auto
from ‹connected G› ‹u ∈ verts G› ‹v ∈ verts G›
obtain p where "S.awalk u p v"
using ‹connected G› ‹u ∈ verts G› by (auto elim: connected_awalkE)
with ‹u ≠ v› obtain e where "e ∈ parcs (mk_symmetric G)"
by (metis S.awalk_Cons_iff S.awalk_empty_ends list_exhaust2)
with ‹arcs G = {}› show False
by (auto simp: parcs_mk_symmetric)
qed
lemma (in wf_digraph) euler_trail_conv_connected:
assumes "connected G"
shows "euler_trail u p v ⟷ trail u p v ∧ set p = arcs G" (is "?L ⟷ ?R")
proof
assume ?R show ?L
proof cases
assume "p = []" with assms ‹?R› show ?thesis
by (auto simp: euler_trail_def trail_def awalk_def elim: connected_arcs_empty)
next
assume "p ≠ []" then have "arcs G ≠ {}" using ‹?R› by auto
with assms ‹?R› ‹p ≠ []› show ?thesis
by (auto simp: euler_trail_def trail_def set_awalk_verts_not_Nil connected_verts)
qed
qed (simp add: euler_trail_def)
lemma (in wf_digraph) awalk_connected:
assumes "connected G" "awalk u p v" "set p ≠ arcs G"
shows "∃e. e ∈ arcs G - set p ∧ (tail G e ∈ set (awalk_verts u p) ∨ head G e ∈ set (awalk_verts u p))"
proof (rule ccontr)
assume A: "¬?thesis"
obtain e where "e ∈ arcs G - set p"
using assms by (auto simp: trail_def)
with A have "tail G e ∉ set (awalk_verts u p)" "tail G e ∈ verts G"
by auto
interpret S: pair_wf_digraph "mk_symmetric G" ..
have "u ∈ verts G" using ‹awalk u p v› by (auto simp: awalk_hd_in_verts)
with ‹tail G e ∈ _› and ‹connected G›
obtain q where q: "S.awalk u q (tail G e)"
by (auto elim: connected_awalkE)
have "u ∈ set (awalk_verts u p)"
using ‹awalk u p v› by (auto simp: set_awalk_verts)
have "q ≠ []" using ‹u ∈ set _› ‹tail G e ∉ _› q by auto
have "∃e ∈ set q. fst e ∈ set (awalk_verts u p) ∧ snd e ∉ set (awalk_verts u p)"
by (rule S.awalk_vertex_props[OF ‹S.awalk _ _ _› ‹q ≠ []›]) (auto simp: ‹u ∈ set _› ‹tail G e ∉ _›)
then obtain se' where se': "se' ∈ set q" "fst se' ∈ set (awalk_verts u p)" "snd se' ∉ set (awalk_verts u p)"
by auto
from se' have "se' ∈ parcs (mk_symmetric G)" using q by auto
then obtain e' where "e' ∈ arcs G" "(tail G e' = fst se' ∧ head G e' = snd se') ∨ (tail G e' = snd se' ∧ head G e' = fst se')"
by (auto simp: parcs_mk_symmetric)
moreover
then have "e' ∉ set p" using se' ‹awalk u p v›
by (auto dest: awalk_verts_arc2 awalk_verts_arc1)
ultimately show False using se'
using A by auto
qed
lemma (in wf_digraph) trail_connected:
assumes "connected G" "trail u p v" "set p ≠ arcs G"
shows "∃e. e ∈ arcs G - set p ∧ (tail G e ∈ set (awalk_verts u p) ∨ head G e ∈ set (awalk_verts u p))"
using assms by (intro awalk_connected) (auto simp: trail_def)
theorem (in fin_digraph) closed_euler1:
assumes con: "connected G"
assumes deg: "⋀u. u ∈ verts G ⟹ in_degree G u = out_degree G u"
shows "∃u p. euler_trail u p u"
proof -
from con obtain u where "u ∈ verts G" by (auto simp: connected_def strongly_connected_def)
then have "trail u [] u" by (auto simp: trail_def awalk_simps)
moreover
{ fix u p v assume "trail u p v"
then have "∃u' p' v'. euler_trail u' p' v'"
proof (induct "card (arcs G) - length p" arbitrary: u p v)
case 0
then have "u ∈ verts G" by (auto simp: trail_def)
have "set p ⊆ arcs G" using ‹trail u p v› by (auto simp: trail_def)
with 0 have "set p = arcs G"
by (auto simp: trail_def distinct_card[symmetric] card_seteq)
then have "euler_trail u p v"
using 0 by (simp add: euler_trail_conv_connected[OF con])
then show ?case by blast
next
case (Suc n)
then have neq: "set p ≠ arcs G" "u ∈ verts G"
by (auto simp: trail_def distinct_card[symmetric])
show ?case
proof (cases "u = v")
assume "u ≠ v"
then have "arc_balance u p = -1"
using Suc neq by (auto elim: trail_arc_balanceE)
then have "card (in_arcs G u ∩ set p) < card (out_arcs G u ∩ set p)"
unfolding arc_set_balance_def by auto
also have "… ≤ card (out_arcs G u)"
by (rule card_mono) auto
finally have "card (in_arcs G u ∩ set p) < card (in_arcs G u)"
using deg[OF ‹u ∈ _›] unfolding out_degree_def in_degree_def by simp
then have "in_arcs G u - set p ≠ {}"
by (auto dest: card_psubset[rotated 2])
then obtain a where "a ∈ arcs G" "head G a = u" "a ∉ set p"
by (auto simp: in_arcs_def)
then have *: "trail (tail G a) (a # p) v"
using Suc by (auto simp: trail_def awalk_simps)
then show ?thesis
using Suc by (intro Suc) auto
next
assume "u = v"
with neq con Suc
obtain a where a_in: "a ∈ arcs G - set p"
and a_end: "(tail G a ∈ set (awalk_verts u p) ∨ head G a ∈ set (awalk_verts u p))"
by (atomize_elim) (rule trail_connected)
have "trail u p u" using Suc ‹u = v› by simp
show ?case
proof (cases "tail G a ∈ set (awalk_verts u p)")
case True
with ‹trail u p u› obtain q where q: "set p = set q" "trail (tail G a) q (tail G a)"
by (rule rotate_trailE') blast
with True a_in have *: "trail (tail G a) (q @ [a]) (head G a)"
by (fastforce simp: trail_def awalk_simps )
moreover
from q Suc have "length q = length p"
by (simp add: trail_def distinct_card[symmetric])
ultimately
show ?thesis using Suc by (intro Suc) auto
next
case False
with a_end have "head G a ∈ set (awalk_verts u p)" by blast
with ‹trail u p u› obtain q where q: "set p = set q" "trail (head G a) q (head G a)"
by (rule rotate_trailE') blast
with False a_in have *: "trail (tail G a) (a # q) (head G a)"
by (fastforce simp: trail_def awalk_simps )
moreover
from q Suc have "length q = length p"
by (simp add: trail_def distinct_card[symmetric])
ultimately
show ?thesis using Suc by (intro Suc) auto
qed
qed
qed }
ultimately obtain u p v where et: "euler_trail u p v" by blast
moreover
have "u = v"
proof -
have "arc_balanced u p v"
using ‹euler_trail u p v› by (auto simp: euler_trail_def dest: arc_balancedI_trail)
then show ?thesis
using ‹euler_trail u p v› deg
by (auto simp add: euler_trail_def trail_def arc_set_balanced_all split: if_split_asm)
qed
ultimately show ?thesis by blast
qed
lemma (in wf_digraph) closed_euler_imp_eq_degree:
assumes "euler_trail u p u"
assumes "v ∈ verts G"
shows "in_degree G v = out_degree G v"
proof -
from assms have "arc_balanced u p u" "set p = arcs G"
unfolding euler_trail_def by (auto dest: arc_balancedI_trail)
with assms have "arc_balance v p = 0"
unfolding arc_set_balanced_def by auto
moreover
from ‹set p = _› have "in_arcs G v ∩ set p = in_arcs G v" "out_arcs G v ∩ set p = out_arcs G v"
by (auto intro: in_arcs_in_arcs out_arcs_in_arcs)
ultimately
show ?thesis unfolding arc_set_balance_def in_degree_def out_degree_def by auto
qed
theorem (in fin_digraph) closed_euler2:
assumes "euler_trail u p u"
shows "connected G"
and "⋀u. u ∈ verts G ⟹ in_degree G u = out_degree G u" (is "⋀u. _ ⟹ ?eq_deg u")
proof -
from assms show "connected G" by (rule euler_imp_connected)
next
fix v assume A: "v ∈ verts G"
with assms show "?eq_deg v" by (rule closed_euler_imp_eq_degree)
qed
corollary (in fin_digraph) closed_euler:
"(∃u p. euler_trail u p u) ⟷ connected G ∧ (∀u ∈ verts G. in_degree G u = out_degree G u)"
by (auto dest: closed_euler1 closed_euler2)
subsection ‹Open euler trails›
text ‹
Intuitively, a graph has an open euler trail if and only if it is possible to add
an arc such that the resulting graph has a closed euler trail. However, this is
not true in our formalization, as the arc type @{typ 'b} might be finite:
Consider for example the graph
@{term "⦇ verts = {0,1}, arcs = {()}, tail = λ_. 0, head = λ_. 1 ⦈"}. This graph
obviously has an open euler trail, but we cannot add another arc, as we already
exhausted the universe.
However, for each @{term "fin_digraph G"} there exist an isomorphic graph
@{term H} with arc type @{typ "'a × nat × 'a"}. Hence, we first characterize
the existence of euler trail for the infinite arc type @{typ "'a × nat × 'a"}
and transfer that result back to arbitrary arc types.
›
lemma open_euler_infinite_label:
fixes G :: "('a, 'a × nat × 'a) pre_digraph"
assumes "fin_digraph G"
assumes [simp]: "tail G = fst" "head G = snd o snd"
assumes con: "connected G"
assumes uv: "u ∈ verts G" "v ∈ verts G"
assumes deg: "⋀w. ⟦w ∈ verts G; u ≠ w; v ≠ w⟧ ⟹ in_degree G w = out_degree G w"
assumes deg_in: "in_degree G u + 1 = out_degree G u"
assumes deg_out: "out_degree G v + 1 = in_degree G v"
shows "∃p. pre_digraph.euler_trail G u p v"
proof -
define label :: "'a × nat × 'a ⇒ nat" where [simp]: "label = fst o snd"
interpret fin_digraph G by fact
have "finite (label ` arcs G)" by auto
moreover have "¬finite (UNIV :: nat set)" by blast
ultimately obtain l where "l ∉ label ` arcs G" by atomize_elim (rule ex_new_if_finite)
from deg_in deg_out have "u ≠ v" by auto
let ?e = "(v,l,u)"
have e_notin:"?e ∉ arcs G"
using ‹l ∉ _› by (auto simp: image_def)
let ?H = "add_arc ?e"
have [simp]: "verts ?H = verts G" using uv by simp
have [intro]: "⋀a. compatible (add_arc a) G" by (simp add: compatible_def)
interpret H: fin_digraph "add_arc a"
rewrites "tail (add_arc a) = tail G" and "head (add_arc a) = head G"
and "pre_digraph.cas (add_arc a) = cas"
and "pre_digraph.awalk_verts (add_arc a) = awalk_verts"
for a
by unfold_locales (auto dest: wellformed intro: compatible_cas compatible_awalk_verts
simp: verts_add_arc_conv)
have "∃u p. H.euler_trail ?e u p u"
proof (rule H.closed_euler1)
show "connected ?H"
proof (rule H.connectedI)
interpret sH: pair_fin_digraph "mk_symmetric ?H" ..
fix u v assume "u ∈ verts ?H" "v ∈ verts ?H"
with con have "u →⇧*⇘mk_symmetric G⇙ v" by (auto simp: connected_def)
moreover
have "subgraph G ?H" by (auto simp: subgraph_def) unfold_locales
ultimately show "u →⇧*⇘with_proj (mk_symmetric ?H)⇙ v"
by (blast intro: sH.reachable_mono subgraph_mk_symmetric)
qed (simp add: verts_add_arc_conv)
next
fix w assume "w ∈ verts ?H"
then show "in_degree ?H w = out_degree ?H w"
using deg deg_in deg_out e_notin
apply (cases "w = u")
apply (case_tac [!] "w = v")
by (auto simp: in_degree_add_arc_iff out_degree_add_arc_iff)
qed
then obtain w p where Het: "H.euler_trail ?e w p w" by blast
then have "?e ∈ set p" by (auto simp: pre_digraph.euler_trail_def)
then obtain q r where p_decomp: "p = q @ [?e] @ r"
by (auto simp: in_set_conv_decomp)
have "euler_trail u (r @ q) v"
proof (unfold euler_trail_conv_connected[OF con], intro conjI)
from Het have Ht': "H.trail ?e v (?e # r @ q) v"
unfolding p_decomp H.euler_trail_def H.trail_def
by (auto simp: p_decomp H.awalk_Cons_iff)
then have "H.trail ?e u (r @ q) v" "?e ∉ set (r @ q)"
by (auto simp: H.trail_def H.awalk_Cons_iff)
then show t': "trail u (r @ q) v"
by (auto simp: trail_def H.trail_def awalk_def H.awalk_def)
show "set (r @ q) = arcs G"
proof -
have "arcs G = arcs ?H - {?e}" using e_notin by auto
also have "arcs ?H = set p" using Het
by (auto simp: pre_digraph.euler_trail_def pre_digraph.trail_def)
finally show ?thesis using ‹?e ∉ set _› by (auto simp: p_decomp)
qed
qed
then show ?thesis by blast
qed
context wf_digraph begin
lemma trail_app_isoI:
assumes t: "trail u p v"
and hom: "digraph_isomorphism hom"
shows "pre_digraph.trail (app_iso hom G) (iso_verts hom u) (map (iso_arcs hom) p) (iso_verts hom v)"
proof -
interpret H: wf_digraph "app_iso hom G" using hom ..
from t hom have i: "inj_on (iso_arcs hom) (set p)"
unfolding trail_def digraph_isomorphism_def by (auto dest:subset_inj_on[where A="set p"])
then have "distinct (map (iso_arcs hom) p) = distinct p"
by (auto simp: distinct_map dest: inj_onD)
with t hom show ?thesis
by (auto simp: pre_digraph.trail_def awalk_app_isoI)
qed
lemma euler_trail_app_isoI:
assumes t: "euler_trail u p v"
and hom: "digraph_isomorphism hom"
shows "pre_digraph.euler_trail (app_iso hom G) (iso_verts hom u) (map (iso_arcs hom) p) (iso_verts hom v)"
proof -
from t have "awalk u p v" by (auto simp: euler_trail_def trail_def)
with assms show ?thesis
by (simp add: pre_digraph.euler_trail_def trail_app_isoI awalk_verts_app_iso_eq)
qed
end
context fin_digraph begin
theorem open_euler1:
assumes "connected G"
assumes "u ∈ verts G" "v ∈ verts G"
assumes "⋀w. ⟦w ∈ verts G; u ≠ w; v ≠ w⟧ ⟹ in_degree G w = out_degree G w"
assumes "in_degree G u + 1 = out_degree G u"
assumes "out_degree G v + 1 = in_degree G v"
shows "∃p. euler_trail u p v"
proof -
obtain f and n :: nat where "f ` arcs G = {i. i < n}"
and i: "inj_on f (arcs G)"
by atomize_elim (rule finite_imp_inj_to_nat_seg, auto)
define iso_f where "iso_f =
⦇ iso_verts = id, iso_arcs = (λa. (tail G a, f a, head G a)),
head = snd o snd, tail = fst ⦈"
have [simp]: "iso_verts iso_f = id" "iso_head iso_f = snd o snd" "iso_tail iso_f = fst"
unfolding iso_f_def by auto
have di_iso_f: "digraph_isomorphism iso_f" unfolding digraph_isomorphism_def iso_f_def
by (auto intro: inj_onI wf_digraph dest: inj_onD[OF i])
let ?iso_g = "inv_iso iso_f"
have [simp]: "⋀u. u ∈ verts G ⟹ iso_verts ?iso_g u = u"
by (auto simp: inv_iso_def fun_eq_iff the_inv_into_f_eq)
let ?H = "app_iso iso_f G"
interpret H: fin_digraph ?H using di_iso_f ..
have "∃p. H.euler_trail u p v"
using di_iso_f assms i
by (intro open_euler_infinite_label) (auto simp: connectedI_app_iso app_iso_eq)
then obtain p where Het: "H.euler_trail u p v" by blast
have "pre_digraph.euler_trail (app_iso ?iso_g ?H) (iso_verts ?iso_g u) (map (iso_arcs ?iso_g) p) (iso_verts ?iso_g v)"
using Het by (intro H.euler_trail_app_isoI digraph_isomorphism_invI di_iso_f)
then show ?thesis using di_iso_f ‹u ∈ _› ‹v ∈ _› by simp rule
qed
theorem open_euler2:
assumes et: "euler_trail u p v" and "u ≠ v"
shows "connected G ∧
(∀w ∈ verts G. u ≠ w ⟶ v ≠ w ⟶ in_degree G w = out_degree G w) ∧
in_degree G u + 1 = out_degree G u ∧
out_degree G v + 1 = in_degree G v"
proof -
from et have *: "trail u p v" "u ∈ verts G" "v ∈ verts G"
by (auto simp: euler_trail_def trail_def awalk_hd_in_verts)
from et have [simp]: "⋀u. card (in_arcs G u ∩ set p) = in_degree G u"
"⋀u. card (out_arcs G u ∩ set p) = out_degree G u"
by (auto simp: in_degree_def out_degree_def euler_trail_def intro: arg_cong[where f=card])
from assms * show ?thesis
by (auto simp: arc_set_balance_def elim: trail_arc_balanceE
intro: euler_imp_connected)
qed
corollary open_euler:
"(∃u p v. euler_trail u p v ∧ u ≠ v) ⟷
connected G ∧ (∃u v. u ∈ verts G ∧ v ∈ verts G ∧
(∀w ∈ verts G. u ≠ w ⟶ v ≠ w ⟶ in_degree G w = out_degree G w) ∧
in_degree G u + 1 = out_degree G u ∧
out_degree G v + 1 = in_degree G v)" (is "?L ⟷ ?R")
proof
assume ?L
then obtain u p v where *: "euler_trail u p v" "u ≠ v"
by auto
then have "u ∈ verts G" "v ∈ verts G"
by (auto simp: euler_trail_def trail_def awalk_hd_in_verts)
then show ?R using open_euler2[OF *] by blast
next
assume ?R
then obtain u v where *:
"connected G" "u ∈ verts G" "v ∈ verts G"
"⋀w. ⟦w ∈ verts G; u ≠ w; v ≠ w⟧ ⟹ in_degree G w = out_degree G w"
"in_degree G u + 1 = out_degree G u"
"out_degree G v + 1 = in_degree G v"
by blast
then have "u ≠ v" by auto
from * show ?L by (metis open_euler1 ‹u ≠ v›)
qed
end
end