Theory Graph_Theory.Euler

(* 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 *mk_symmetric Gw2"
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 Gw1" 
      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 Gw2" 
      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 Gw2" 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 ∉ 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 *mk_symmetric Gv" 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)
    ― ‹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: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

(* XXX: We can get rid of "u ∈ verts G" "v ∈ 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