Quelle  Euler.thy

(* Title:  Euler.thy
   Author: Lars Noschinski, TU München
*)
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

(* XXX move; notused*)
lemma (in fin_digraph) trails_finite: "finite {p. ∃u v. trail u p v}"
proof -
  have "{p. ∃u v. trail u p v} ⊆ {p. set p ⊆ arcs G ∧ distinct p}"
    by (auto simp: trail_def)
  with finite_subset_distinct[OF finite_arcs] show ?thesis
    using finite_subset by blast 
qed
(* XXX: simplify apath_finite proof? *)

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 →^* _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 →^* _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 →^* _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 →^* _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

(* XXX change order of arguments? *)
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


(* XXX tune assumption? e \<notin> set es oder so? *)
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"
    ― ‹We define a graph which has an closed euler trail›

  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 →^* _G v" by (auto simp: connected_def)
      moreover
      have "subgraph G ?H" by (auto simp: subgraph_def) unfold_locales
      ultimately show "u →^* _{(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)
    ― ‹We show now that removing the additional arc of @{term ?H}
 from p yields an euler trail in G›

  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:inj_on_subset[where B="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

(* XXX: We can get rid of "u \<in> verts G" "v \<in> verts G" here and in @{thm open_euler_infinite_label} *)
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