Theory KoenigsbergBridge

(*
Title:KoenigsbergBridge.thy
Author:Wenda Li
*)

theory KoenigsbergBridge imports MoreGraph
begin

section‹Definition of Eulerian trails and circuits›

definition (in valid_unMultigraph) is_Eulerian_trail:: "'v⇒('v,'w) path⇒'v⇒ bool" where
  "is_Eulerian_trail v ps v'≡ is_trail v ps v' ∧ edges (rem_unPath ps G) = {}"

definition (in valid_unMultigraph) is_Eulerian_circuit:: "'v ⇒ ('v,'w) path ⇒ 'v ⇒ bool" where
  "is_Eulerian_circuit v ps v'≡ (v=v') ∧ (is_Eulerian_trail v ps v')"

section‹Necessary conditions for Eulerian trails and circuits›

lemma (in valid_unMultigraph) euclerian_rev:
  "is_Eulerian_trail v' (rev_path ps) v=is_Eulerian_trail v ps v' "
proof -
  have "is_trail v' (rev_path ps) v=is_trail v ps v'"
    by (metis is_trail_rev)
  moreover have "edges (rem_unPath (rev_path ps) G)=edges (rem_unPath ps G)"
    by (metis rem_unPath_graph)
  ultimately show ?thesis unfolding is_Eulerian_trail_def by auto
qed

(*Necessary conditions for Eulerian circuits*)
theorem (in valid_unMultigraph) euclerian_cycle_ex:
  assumes "is_Eulerian_circuit v ps v'" "finite V" "finite E"
  shows "∀v∈V. even (degree v G)"
proof -
  obtain v ps v' where cycle:"is_Eulerian_circuit v ps v'" using assms by auto
  hence "edges (rem_unPath ps G) = {}"
    unfolding is_Eulerian_circuit_def is_Eulerian_trail_def
    by simp
  moreover have "nodes (rem_unPath ps G)=nodes G" by auto
  ultimately have "rem_unPath ps G = G ⦇edges:={}⦈" by auto
  hence "num_of_odd_nodes (rem_unPath ps G) = 0" by (metis assms(2) odd_nodes_no_edge)
  moreover have "v=v'"
    by (metis ‹is_Eulerian_circuit v ps v'› is_Eulerian_circuit_def)
  hence "num_of_odd_nodes (rem_unPath ps G)=num_of_odd_nodes G"
    by (metis assms(2) assms(3) cycle is_Eulerian_circuit_def
        is_Eulerian_trail_def rem_UnPath_cycle)
  ultimately have "num_of_odd_nodes G=0" by auto
  moreover have "finite(odd_nodes_set G)"
    using ‹finite V› unfolding odd_nodes_set_def by auto
  ultimately have "odd_nodes_set G = {}" unfolding num_of_odd_nodes_def by auto
  thus ?thesis unfolding odd_nodes_set_def by auto
qed

(*Necessary conditions for Eulerian trails*)
theorem (in valid_unMultigraph) euclerian_path_ex:
  assumes "is_Eulerian_trail v ps v'" "finite V" "finite E"
  shows "(∀v∈V. even (degree v G)) ∨ (num_of_odd_nodes G =2)"
proof -
  obtain v ps v' where path:"is_Eulerian_trail v ps v'" using assms by auto
  hence "edges (rem_unPath ps G) = {}"
    unfolding  is_Eulerian_trail_def
    by simp
  moreover have "nodes (rem_unPath ps G)=nodes G" by auto
  ultimately have "rem_unPath ps G = G ⦇edges:={}⦈" by auto
  hence odd_nodes: "num_of_odd_nodes (rem_unPath ps G) = 0"
    by (metis assms(2) odd_nodes_no_edge)
  have "v≠v' ⟹ ?thesis"
    proof (cases "even(degree v' G)")
      case True
      assume "v≠v'"
      have "is_trail v ps v'" by (metis is_Eulerian_trail_def path)
      hence "num_of_odd_nodes (rem_unPath ps G) = num_of_odd_nodes G
          + (if even (degree v G) then 2 else 0)"
        using rem_UnPath_even True ‹finite V› ‹finite E› ‹v≠v'› by auto
      hence "num_of_odd_nodes G + (if even (degree v G) then 2 else 0)=0"
        using odd_nodes by auto
      hence "num_of_odd_nodes G = 0" by auto
      moreover have "finite(odd_nodes_set G)"
        using ‹finite V› unfolding odd_nodes_set_def by auto
      ultimately have "odd_nodes_set G = {}" unfolding num_of_odd_nodes_def by auto
      thus ?thesis unfolding odd_nodes_set_def by auto
    next
      case False
      assume "v≠v'"
      have "is_trail v ps v'" by (metis is_Eulerian_trail_def path)
      hence "num_of_odd_nodes (rem_unPath ps G) = num_of_odd_nodes G
          + (if odd (degree v G) then -2 else 0)"
        using rem_UnPath_odd False ‹finite V› ‹finite E› ‹v≠v'› by auto
      hence odd_nodes_if: "num_of_odd_nodes G + (if odd (degree v G) then -2 else 0)=0"
        using odd_nodes by auto
      have "odd (degree v G) ⟹ ?thesis"
        proof -
          assume "odd (degree v G)"
          hence "num_of_odd_nodes G = 2" using odd_nodes_if by auto
          thus ?thesis by simp
        qed
      moreover have "even(degree v G) ⟹ ?thesis"
        proof -
          assume "even (degree v G)"
          hence "num_of_odd_nodes G = 0" using odd_nodes_if by auto
          moreover have "finite(odd_nodes_set G)"
            using ‹finite V› unfolding odd_nodes_set_def by auto
          ultimately have "odd_nodes_set G = {}" unfolding num_of_odd_nodes_def by auto
          thus ?thesis unfolding odd_nodes_set_def by auto
        qed
      ultimately show ?thesis by auto
    qed
  moreover have "v=v'⟹ ?thesis"
    by (metis assms(2) assms(3) euclerian_cycle_ex is_Eulerian_circuit_def path)
  ultimately show ?thesis by auto
qed

section‹Specific case of the Konigsberg Bridge Problem›

(*to denote the four landmasses*)
datatype kon_node = a | b | c | d

(*to denote the seven bridges*)
datatype kon_bridge = ab1 | ab2 | ac1 | ac2 | ad1 | bd1 | cd1

definition kon_graph :: "(kon_node,kon_bridge) graph" where
  "kon_graph≡⦇nodes={a,b,c,d},
              edges={(a,ab1,b), (b,ab1,a),
                     (a,ab2,b), (b,ab2,a),
                     (a,ac1,c), (c,ac1,a),
                     (a,ac2,c), (c,ac2,a),
                     (a,ad1,d), (d,ad1,a),
                     (b,bd1,d), (d,bd1,b),
                     (c,cd1,d), (d,cd1,c)} ⦈"

instantiation kon_node :: enum
begin
definition [simp]:  "enum_class.enum =[a,b,c,d]"
definition  [simp]: "enum_class.enum_all P ⟷ P a ∧ P b ∧ P c ∧ P d"
definition   [simp]:"enum_class.enum_ex P ⟷ P a ∨ P b ∨ P c ∨ P d"
instance proof qed (auto,(case_tac x,auto)+)
end

instantiation kon_bridge :: enum
begin
definition [simp]:"enum_class.enum =[ab1,ab2,ac1,ac2,ad1,cd1,bd1]"
definition  [simp]:"enum_class.enum_all P ⟷ P ab1 ∧ P ab2 ∧ P ac1 ∧ P ac2 ∧ P ad1  ∧ P bd1
    ∧ P cd1"
definition   [simp]:"enum_class.enum_ex P ⟷  P ab1 ∨ P ab2 ∨ P ac1 ∨ P ac2 ∨ P ad1  ∨ P bd1
    ∨ P cd1"
instance proof qed (auto,(case_tac x,auto)+)
end

interpretation   kon_graph: valid_unMultigraph kon_graph
proof (unfold_locales)
  show "fst ` edges kon_graph ⊆ nodes kon_graph" by eval
next
  show "snd ` snd ` edges kon_graph ⊆ nodes kon_graph"  by eval
next
  have " ∀v w u'. ((v, w, u') ∈ edges kon_graph) = ((u', w, v) ∈ edges kon_graph)"
    by eval
  thus "⋀v w u'. ((v, w, u') ∈ edges kon_graph) = ((u', w, v) ∈ edges kon_graph)" by simp
next
  have "∀v w. (v, w, v) ∉ edges kon_graph"  by eval
  thus "⋀v w. (v, w, v) ∉ edges kon_graph" by simp
qed

(*The specific case of the Konigsberg Bridge Problem does not have a solution*)
theorem "¬kon_graph.is_Eulerian_trail v1 p v2"
proof
  assume "kon_graph.is_Eulerian_trail  v1 p v2"
  moreover have "finite (nodes kon_graph)" by (metis finite_code)
  moreover have "finite (edges kon_graph)" by (metis finite_code)
  ultimately have contra:
    "(∀v∈nodes kon_graph. even (degree v kon_graph)) ∨(num_of_odd_nodes kon_graph =2)"
    by (metis kon_graph.euclerian_path_ex)
  have "odd(degree a kon_graph)" by eval
  moreover have "odd(degree b kon_graph)" by eval
  moreover have "odd(degree c kon_graph)" by eval
  moreover have "odd(degree d kon_graph)" by eval
  ultimately have "¬(num_of_odd_nodes kon_graph =2)" by eval
  moreover have "¬(∀v∈nodes kon_graph. even (degree v kon_graph))" by eval
  ultimately show False using contra by auto
qed

section‹Sufficient conditions for Eulerian trails and circuits›

lemma (in valid_unMultigraph) eulerian_cons:
  assumes
    "valid_unMultigraph.is_Eulerian_trail (del_unEdge v0 w v1 G) v1 ps v2"
    "(v0,w,v1)∈ E"
  shows "is_Eulerian_trail v0 ((v0,w,v1)#ps) v2"
proof -
  have valid:"valid_unMultigraph (del_unEdge v0 w v1 G)"
    using  valid_unMultigraph_axioms by auto
  hence distinct:"valid_unMultigraph.is_trail (del_unEdge v0 w v1 G) v1 ps v2"
    using assms unfolding valid_unMultigraph.is_Eulerian_trail_def[OF valid]
    by auto
  hence "set ps ⊆ edges (del_unEdge v0 w v1 G)"
    using valid_unMultigraph.path_in_edges[OF valid] by auto
  moreover have "(v0,w,v1)∉edges (del_unEdge v0 w v1 G)"
    unfolding del_unEdge_def by auto
  moreover have "(v1,w,v0)∉edges (del_unEdge v0 w v1 G)"
    unfolding del_unEdge_def by auto
  ultimately have "(v0,w,v1)∉set ps" "(v1,w,v0)∉set ps"  by auto
  moreover have "is_trail v1 ps v2"
    using distinct_path_intro[OF distinct] .
  ultimately have "is_trail v0 ((v0,w,v1)#ps) v2"
    using ‹(v0,w,v1)∈ E› by auto
  moreover have "edges (rem_unPath ps (del_unEdge v0 w v1 G)) ={}"
    using assms unfolding valid_unMultigraph.is_Eulerian_trail_def[OF valid]
    by auto
  hence "edges (rem_unPath ((v0,w,v1)#ps) G)={}"
    by (metis rem_unPath.simps(2))
  ultimately show ?thesis unfolding is_Eulerian_trail_def by auto
qed

lemma (in valid_unMultigraph) eulerian_cons':
  assumes
    "valid_unMultigraph.is_Eulerian_trail (del_unEdge v2 w v3 G) v1 ps v2"
    "(v2,w,v3)∈ E"
  shows "is_Eulerian_trail v1 (ps@[(v2,w,v3)]) v3"
proof -
  have valid:"valid_unMultigraph (del_unEdge v3 w v2 G)"
    using valid_unMultigraph_axioms del_unEdge_valid by auto
  have "del_unEdge v2 w v3 G=del_unEdge v3 w v2 G"
    by (metis delete_edge_sym)
  hence "valid_unMultigraph.is_Eulerian_trail (del_unEdge v3 w v2 G) v2
        (rev_path ps) v1" using assms valid_unMultigraph.euclerian_rev[OF valid]
    by auto
  hence "is_Eulerian_trail v3 ((v3,w,v2)#(rev_path ps)) v1"
    using eulerian_cons by (metis assms(2) corres)
  hence "is_Eulerian_trail v1 (rev_path((v3,w,v2)#(rev_path ps))) v3"
    using euclerian_rev by auto
  moreover have "rev_path((v3,w,v2)#(rev_path ps)) = rev_path(rev_path ps)@[(v2,w,v3)]"
    unfolding rev_path_def by auto
  hence "rev_path((v3,w,v2)#(rev_path ps))=ps@[(v2,w,v3)]" by auto
  ultimately show ?thesis by auto
qed

lemma eulerian_split:
  assumes "nodes G1 ∩ nodes G2 = {}" "edges G1 ∩ edges G2={}"
    "valid_unMultigraph G1" "valid_unMultigraph G2"
    "valid_unMultigraph.is_Eulerian_trail  G1 v1 ps1 v1'"
    "valid_unMultigraph.is_Eulerian_trail  G2 v2 ps2 v2'"
  shows "valid_unMultigraph.is_Eulerian_trail ⦇nodes=nodes G1 ∪ nodes G2,
          edges=edges G1 ∪ edges G2 ∪ {(v1',w,v2),(v2,w,v1')}⦈ v1 (ps1@(v1',w,v2)#ps2) v2'"
proof -
  have "valid_graph G1" using ‹valid_unMultigraph G1› valid_unMultigraph_def by auto
  have "valid_graph G2" using ‹valid_unMultigraph G2› valid_unMultigraph_def by auto
  obtain G where G:"G=⦇nodes=nodes G1 ∪ nodes G2, edges=edges G1 ∪ edges G2
      ∪ {(v1',w,v2),(v2,w,v1')}⦈"
    by metis
  have "v1'∈nodes G1"
    by (metis (full_types) ‹valid_graph G1› assms(3) assms(5) valid_graph.is_path_memb
        valid_unMultigraph.is_trail_intro valid_unMultigraph.is_Eulerian_trail_def)
  moreover have "v2∈nodes G2"
    by (metis (full_types) ‹valid_graph G2› assms(4) assms(6) valid_graph.is_path_memb
        valid_unMultigraph.is_trail_intro valid_unMultigraph.is_Eulerian_trail_def)
  moreover have ‹ba ∈ nodes G1› if ‹(aa, ab, ba) ∈ edges G1›
    for aa ab ba
    using that
    by (meson ‹valid_graph G1› valid_graph.E_validD(2)) 
  ultimately have "valid_unMultigraph ⦇nodes=nodes G1 ∪ nodes G2, edges=edges G1 ∪ edges G2 ∪
                   {(v1',w,v2),(v2,w,v1')}⦈"
    using
      valid_unMultigraph.corres[OF ‹valid_unMultigraph G1›]
      valid_unMultigraph.no_id[OF ‹valid_unMultigraph G1›]
      valid_unMultigraph.corres[OF ‹valid_unMultigraph G2›]
      valid_unMultigraph.no_id[OF ‹valid_unMultigraph G2›]
      valid_graph.E_validD[OF ‹valid_graph G1›]
      valid_graph.E_validD[OF ‹valid_graph G2›]
      ‹nodes G1 ∩ nodes G2 = {}›
    by unfold_locales auto
  hence valid: "valid_unMultigraph G" using G by auto
  hence valid':"valid_graph G" using valid_unMultigraph_def by auto
  moreover have "valid_unMultigraph.is_trail G v1 (ps1@((v1',w,v2)#ps2)) v2'"
    proof -
      have ps1_G:"valid_unMultigraph.is_trail G v1 ps1 v1'"
        proof -
          have "valid_unMultigraph.is_trail G1 v1 ps1 v1'" using assms
            by (metis valid_unMultigraph.is_Eulerian_trail_def)
          moreover have "edges G1 ⊆ edges G" by (metis G UnI1 Un_assoc select_convs(2) subrelI)
          moreover have "nodes G1 ⊆ nodes G" by (metis G inf_sup_absorb le_iff_inf select_convs(1))
          ultimately show ?thesis
            using distinct_path_subset[of G1 G,OF ‹valid_unMultigraph G1› valid] by auto
        qed
      have ps2_G:"valid_unMultigraph.is_trail G v2 ps2 v2'"
        proof -
          have "valid_unMultigraph.is_trail G2 v2 ps2 v2'" using assms
            by (metis valid_unMultigraph.is_Eulerian_trail_def)
          moreover have "edges G2 ⊆ edges G" by (metis G inf_sup_ord(3) le_supE select_convs(2))
          moreover have "nodes G2 ⊆ nodes G" by (metis G inf_sup_ord(4) select_convs(1))
          ultimately show ?thesis
            using distinct_path_subset[of G2 G,OF ‹valid_unMultigraph G2› valid] by auto
        qed
      have "valid_graph.is_path G v1 (ps1@((v1',w,v2)#ps2)) v2'"
        proof -
          have "valid_graph.is_path  G v1 ps1 v1'"
            by (metis ps1_G valid valid_unMultigraph.is_trail_intro)
          moreover have "valid_graph.is_path G v2 ps2 v2'"
            by (metis ps2_G valid valid_unMultigraph.is_trail_intro)
          moreover have "(v1',w,v2) ∈ edges G"
            using G by auto
          ultimately show ?thesis
            using valid_graph.is_path_split'[OF valid',of v1 ps1 v1' w v2 ps2 v2'] by auto
        qed
      moreover have "distinct (ps1@((v1',w,v2)#ps2))"
        proof -
          have "distinct ps1" by (metis ps1_G valid valid_unMultigraph.is_trail_path)
          moreover have "distinct ps2"
            by (metis ps2_G valid valid_unMultigraph.is_trail_path)
          moreover have "set ps1 ∩ set ps2 = {}"
            proof -
              have "set ps1 ⊆edges G1"
                by (metis assms(3) assms(5) valid_unMultigraph.is_Eulerian_trail_def
                    valid_unMultigraph.path_in_edges)
              moreover have "set ps2 ⊆ edges G2"
                by (metis assms(4) assms(6) valid_unMultigraph.is_Eulerian_trail_def
                    valid_unMultigraph.path_in_edges)
              ultimately show ?thesis using ‹edges G1 ∩ edges G2={}› by auto
            qed
          moreover have "(v1',w,v2)∉edges G1"
            using ‹v2 ∈ nodes G2› ‹valid_graph G1›
            by (metis Int_iff  all_not_in_conv assms(1) valid_graph.E_validD(2))
          hence "(v1',w,v2)∉set ps1"
            by (metis (full_types) assms(3) assms(5) subsetD valid_unMultigraph.path_in_edges
                valid_unMultigraph.is_Eulerian_trail_def )
          moreover have "(v1',w,v2)∉edges G2"
            using ‹v1' ∈ nodes G1› ‹valid_graph G2›
            by (metis  assms(1) disjoint_iff_not_equal valid_graph.E_validD(1))
          hence  "(v1',w,v2)∉set ps2"
            by (metis (full_types)  assms(4) assms(6) in_mono valid_unMultigraph.path_in_edges
                valid_unMultigraph.is_Eulerian_trail_def )
          ultimately show ?thesis using distinct_append by auto
        qed
      moreover have "set (ps1@((v1',w,v2)#ps2)) ∩ set (rev_path (ps1@((v1',w,v2)#ps2))) = {}"
        proof -
          have "set ps1 ∩ set (rev_path ps1) = {}"
            by (metis ps1_G valid valid_unMultigraph.is_trail_path)
          moreover have "set (rev_path ps2) ⊆ edges G2"
            by (metis assms(4) assms(6) valid_unMultigraph.is_trail_rev
                valid_unMultigraph.is_Eulerian_trail_def valid_unMultigraph.path_in_edges)
          hence "set ps1 ∩ set (rev_path ps2) = {}"
            using assms
              valid_unMultigraph.path_in_edges[OF ‹valid_unMultigraph G1›, of v1 ps1 v1']
              valid_unMultigraph.path_in_edges[OF ‹valid_unMultigraph G2›, of v2 ps2 v2']
            unfolding valid_unMultigraph.is_Eulerian_trail_def[OF ‹valid_unMultigraph G1›]
              valid_unMultigraph.is_Eulerian_trail_def[OF ‹valid_unMultigraph G2›]
            by auto
          moreover have "set ps2 ∩ set (rev_path ps2) = {}"
            by (metis ps2_G valid valid_unMultigraph.is_trail_path)
          moreover have "set (rev_path ps1) ⊆edges G1"
            by (metis assms(3) assms(5) valid_unMultigraph.is_Eulerian_trail_def
                valid_unMultigraph.path_in_edges valid_unMultigraph.euclerian_rev)
          hence "set ps2 ∩ set (rev_path ps1) = {}"
            by (metis calculation(2) distinct_append distinct_rev_path ps1_G ps2_G rev_path_append
              rev_path_double valid valid_unMultigraph.is_trail_path)
          moreover have "(v2,w,v1')∉set (ps1@((v1',w,v2)#ps2))"
            proof -
              have "(v2,w,v1')∉edges G1"
                using ‹v2 ∈ nodes G2› ‹valid_graph G1›
                by (metis Int_iff  all_not_in_conv assms(1) valid_graph.E_validD(1))
              hence "(v2,w,v1')∉set ps1"
                by (metis assms(3) assms(5) split_list valid_unMultigraph.is_trail_split'
                    valid_unMultigraph.is_Eulerian_trail_def)
              moreover have "(v2,w,v1')∉edges G2"
                using ‹v1' ∈ nodes G1› ‹valid_graph G2›
                by (metis IntI assms(1) empty_iff valid_graph.E_validD(2))
              hence "(v2,w,v1')∉set ps2"
                by (metis (full_types) assms(4) assms(6) in_mono  valid_unMultigraph.path_in_edges
                    valid_unMultigraph.is_Eulerian_trail_def)
              moreover have "(v2,w,v1')≠(v1',w,v2)"
                using ‹v1' ∈ nodes G1› ‹v2 ∈ nodes G2›
                by (metis IntI Pair_inject  assms(1) assms(5) bex_empty)
              ultimately show ?thesis by auto
            qed
          ultimately show ?thesis using rev_path_append by auto
        qed
      ultimately show ?thesis using valid_unMultigraph.is_trail_path[OF valid]
        by auto
    qed
  moreover have "edges (rem_unPath (ps1@((v1',w,v2)#ps2)) G)= {}"
    proof -
      have "edges (rem_unPath (ps1@((v1',w,v2)#ps2)) G)=edges G -
           (set (ps1@((v1',w,v2)#ps2)) ∪ set (rev_path (ps1@((v1',w,v2)#ps2))))"
        by (metis rem_unPath_edges)
      also have "...=edges G - (set ps1 ∪ set ps2 ∪ set (rev_path ps1) ∪ set (rev_path ps2)
                 ∪ {(v1',w,v2),(v2,w,v1')})" using rev_path_append by auto
      finally have "edges (rem_unPath (ps1@((v1',w,v2)#ps2)) G) = edges G - (set ps1 ∪
                    set ps2 ∪ set (rev_path ps1) ∪ set (rev_path ps2) ∪ {(v1',w,v2),(v2,w,v1')})" .
      moreover have "edges (rem_unPath ps1 G1)={}"
        by (metis assms(3) assms(5) valid_unMultigraph.is_Eulerian_trail_def)
      hence "edges G1 - (set ps1 ∪ set (rev_path ps1))={}"
        by (metis rem_unPath_edges)
      moreover have "edges (rem_unPath ps2 G2)={}"
        by (metis assms(4) assms(6) valid_unMultigraph.is_Eulerian_trail_def)
      hence "edges G2 - (set ps2 ∪ set (rev_path ps2))={}"
        by (metis rem_unPath_edges)
      ultimately show ?thesis using G by auto
    qed
  ultimately show ?thesis by (metis G valid valid_unMultigraph.is_Eulerian_trail_def)
qed

lemma (in valid_unMultigraph) eulerian_sufficient:
  assumes "finite V" "finite E" "connected" "V≠{}"
  shows "num_of_odd_nodes G = 2 ⟹
      (∃v∈V.∃v'∈V.∃ps. odd(degree v G)∧odd(degree v' G)∧(v≠v')∧is_Eulerian_trail v ps v')"
      and "num_of_odd_nodes G=0 ⟹ (∀v∈V.∃ps. is_Eulerian_circuit v ps v)"
    using ‹finite E› ‹finite V› valid_unMultigraph_axioms  ‹V≠{}› ‹connected›
proof (induct "card E" arbitrary: G rule: less_induct)
  case less
  assume "finite (edges G)" and "finite (nodes G)" and "valid_unMultigraph G" and "nodes G≠{}"
      and "valid_unMultigraph.connected G" and "num_of_odd_nodes G = 2"
  have "valid_graph G" using ‹valid_unMultigraph G› valid_unMultigraph_def by auto
  obtain n1 n2 where
      n1: "n1∈nodes G" "odd(degree n1 G)"
      and n2: "n2∈nodes G" "odd(degree n2 G)"
      and "n1≠n2" unfolding num_of_odd_nodes_def odd_nodes_set_def
    proof -
      have "∀S. card S=2 ⟶ (∃n1 n2. n1∈S∧n2∈S∧n1≠n2)"
        by (metis card_eq_0_iff equals0I even_card' even_numeral zero_neq_numeral)
      then obtain t1 t2
          where "t1∈{v ∈ nodes G. odd (degree v G)}" "t2∈{v ∈ nodes G. odd (degree v G)}" "t1≠t2"
        using ‹num_of_odd_nodes G = 2› unfolding num_of_odd_nodes_def odd_nodes_set_def
        by force
      thus ?thesis by (metis (lifting) that mem_Collect_eq)
    qed
  have even_except_two:"⋀n. n∈nodes G⟹ n≠n1 ⟹ n≠n2 ⟹ even(degree n G)"
    proof (rule ccontr)
      fix n assume "n ∈ nodes G"  "n ≠ n1" "n ≠ n2" "odd (degree n G)"
      have "n∈ odd_nodes_set G"
        by (metis (mono_tags) ‹n ∈ nodes G› ‹odd (degree n G)› mem_Collect_eq odd_nodes_set_def)
      moreover have "n1 ∈ odd_nodes_set G"
        by (metis (mono_tags) mem_Collect_eq n1(1) n1(2) odd_nodes_set_def)
      moreover have "n2 ∈ odd_nodes_set G"
        using n2(1) n2(2) unfolding odd_nodes_set_def by auto
      ultimately have "{n,n1,n2}⊆ odd_nodes_set G" by auto
      moreover have "card{n,n1,n2} ≥3" using ‹n1≠n2› ‹n≠n1› ‹n≠n2› by auto
      moreover have "finite (odd_nodes_set G)"
        using ‹finite (nodes G)› unfolding odd_nodes_set_def by auto
      ultimately have "card (odd_nodes_set G) ≥ 3"
        using card_mono[of "odd_nodes_set G" "{n, n1, n2}"] by auto
      thus False using ‹num_of_odd_nodes G = 2› unfolding num_of_odd_nodes_def by auto
    qed
  have "{e ∈ edges G. fst e = n1}≠{}"
    using n1
    by (metis (full_types) degree_def empty_iff finite.emptyI odd_card)
  then obtain v' w where "(n1,w,v')∈edges G" by auto
  have "v'=n2 ⟹ (∃v∈nodes G. ∃v'∈nodes G.∃ps. odd (degree v G) ∧ odd (degree v' G)  ∧ v ≠ v'
      ∧ valid_unMultigraph.is_Eulerian_trail G v ps v')"
    proof (cases "valid_unMultigraph.connected (del_unEdge n1 w n2 G)")
      assume "v'=n2"
      assume conneted':"valid_unMultigraph.connected (del_unEdge n1 w n2 G)"
      moreover have "num_of_odd_nodes (del_unEdge n1 w n2 G) = 0"
        using ‹(n1, w, v') ∈ edges G› ‹finite (edges G)› ‹finite (nodes G)›  ‹v' = n2›
          ‹num_of_odd_nodes G = 2› ‹valid_unMultigraph G› del_UnEdge_odd_odd n1(2) n2(2)
        by force
      moreover have "finite (edges (del_unEdge n1 w n2 G))"
        using ‹finite (edges G)› by auto
      moreover have "finite (nodes (del_unEdge n1 w n2 G))"
        using ‹finite (nodes G)› by auto
      moreover have "edges G - {(n1,w,n2),(n2,w,n1)} ⊂ edges G"
        using Diff_iff Diff_subset ‹(n1, w, v') ∈ edges G› ‹v' = n2›
        by fast
      hence "card (edges (del_unEdge n1 w n2 G)) < card (edges G)"
        using ‹finite (edges G)› psubset_card_mono[of "edges G" "edges G - {(n1,w,n2),(n2,w,n1)}"]
        unfolding del_unEdge_def by auto
      moreover have "valid_unMultigraph (del_unEdge n1 w n2 G)"
        using ‹valid_unMultigraph G› del_unEdge_valid by auto
      moreover have "nodes (del_unEdge n1 w n2 G) ≠ {}"
        by (metis (full_types) del_UnEdge_node empty_iff n1(1))
      ultimately have "∀v∈nodes (del_unEdge n1 w n2 G). ∃ps. valid_unMultigraph.is_Eulerian_circuit
          (del_unEdge n1 w n2 G) v ps v"
        using less.hyps[of "del_unEdge n1 w n2 G"] by auto
      thus ?thesis using eulerian_cons
        by (metis ‹(n1, w, v') ∈ edges G› ‹n1 ≠ n2› ‹v' = n2›  ‹valid_unMultigraph G›
          ‹valid_unMultigraph (del_unEdge n1 w n2 G)› del_UnEdge_node n1(1) n1(2) n2(1) n2(2)
          valid_unMultigraph.eulerian_cons valid_unMultigraph.is_Eulerian_circuit_def)
    next
      assume "v'=n2"
      assume not_conneted:"¬valid_unMultigraph.connected (del_unEdge n1 w n2 G)"
      have valid0:"valid_unMultigraph (del_unEdge n1 w n2 G)"
        using ‹valid_unMultigraph G› del_unEdge_valid by auto
      hence valid0':"valid_graph (del_unEdge n1 w n2 G)"
        using valid_unMultigraph_def by auto
      have all_even:"∀n∈nodes (del_unEdge n1 w n2 G). even(degree n (del_unEdge n1 w n2 G))"
        proof -
          have "even (degree n1 (del_unEdge n1 w n2 G))"
            using ‹(n1, w, v') ∈ edges G› ‹finite (edges G)› ‹v' = n2› ‹valid_unMultigraph G› n1
            by (auto simp add: valid_unMultigraph.corres)
          moreover have "even (degree n2 (del_unEdge n1 w n2 G))"
            using  ‹(n1, w, v') ∈ edges G› ‹finite (edges G)› ‹v' = n2› ‹valid_unMultigraph G› n2
            by (auto simp add: valid_unMultigraph.corres)
          moreover have  "⋀n. n ∈ nodes (del_unEdge n1 w n2 G) ⟹ n ≠ n1 ⟹ n ≠ n2 ⟹
              even (degree n (del_unEdge n1 w n2 G))"
            using valid_unMultigraph.degree_frame[OF ‹valid_unMultigraph G›,
              of _ n1 n2 w] even_except_two
            by (metis (no_types) ‹finite (edges G)› del_unEdge_def empty_iff insert_iff
              select_convs(1))
          ultimately show ?thesis by auto
        qed
      have "(n1,w,n2)∈edges G" by (metis ‹(n1, w, v') ∈ edges G› ‹v' = n2›)
      hence "(n2,w,n1)∈edges G" by (metis ‹valid_unMultigraph G› valid_unMultigraph.corres)
      obtain G1 G2 where
          G1_nodes: "nodes G1={n. ∃ps. valid_graph.is_path (del_unEdge n1 w n2 G) n ps n1}"
          and G1_edges: "edges G1={(n,e,n'). (n,e,n')∈edges (del_unEdge n1 w n2 G)
            ∧ n∈nodes G1 ∧ n'∈nodes G1}"
          and G2_nodes:"nodes G2={n. ∃ps. valid_graph.is_path (del_unEdge n1 w n2 G) n ps n2}"
          and G2_edges:"edges G2={(n,e,n'). (n,e,n')∈edges (del_unEdge n1 w n2 G) ∧ n∈nodes G2
            ∧ n'∈nodes G2}"
          and G1_G2_edges_union:"edges G1 ∪ edges G2 = edges (del_unEdge n1 w n2 G)"
          and "edges G1 ∩ edges G2={}"
          and G1_G2_nodes_union:"nodes G1 ∪ nodes G2=nodes (del_unEdge n1 w n2 G)"
          and "nodes G1 ∩ nodes G2={}"
          and "valid_unMultigraph G1"
          and "valid_unMultigraph G2"
          and "valid_unMultigraph.connected G1"
          and "valid_unMultigraph.connected G2"
        using valid_unMultigraph.connectivity_split[OF ‹valid_unMultigraph G›
          ‹valid_unMultigraph.connected G› ‹¬ valid_unMultigraph.connected (del_unEdge n1 w n2 G)›
          ‹(n1, w, n2) ∈ edges G› ] .
      have "edges (del_unEdge n1 w n2 G) ⊂ edges G"
        unfolding del_unEdge_def using ‹(n1, w, n2)∈edges G› ‹(n2, w, n1)∈edges G› by auto
      hence "card (edges G1) < card (edges G)" using G1_G2_edges_union
        by (metis (full_types) ‹finite (edges G)› inf_sup_absorb less_infI2 psubset_card_mono)
      moreover have "finite (edges G1)"
        using G1_G2_edges_union ‹finite (edges G)›
        by (metis ‹edges (del_unEdge n1 w n2 G) ⊂ edges G› finite_Un less_imp_le rev_finite_subset)
      moreover have "nodes G1 ⊆ nodes (del_unEdge n1 w n2 G)"
        by (metis G1_G2_nodes_union Un_upper1)
      hence "finite (nodes G1)"
        using  ‹finite (nodes G)› del_UnEdge_node rev_finite_subset  by auto
      moreover have "n1 ∈ nodes G1"
        proof -
          have "n1∈nodes (del_unEdge n1 w n2 G)" using ‹n1∈nodes G› by auto
          hence "valid_graph.is_path (del_unEdge n1 w n2 G) n1 [] n1"
            using valid0' by (metis valid_graph.is_path_simps(1))
          thus ?thesis using G1_nodes by auto
        qed
      hence "nodes G1 ≠ {}" by auto
      moreover have "num_of_odd_nodes G1 = 0"
        proof -
          have "valid_graph G2" using ‹valid_unMultigraph G2› valid_unMultigraph_def by auto
          hence "∀n∈nodes G1. degree n G1 = degree n (del_unEdge n1 w n2 G)"
          using sub_graph_degree_frame[of G2 G1 "(del_unEdge n1 w n2 G)"]
            by (metis G1_G2_edges_union ‹nodes G1 ∩ nodes G2 = {}›)
          hence "∀n∈nodes G1. even(degree n G1)" using all_even
            by (metis G1_G2_nodes_union Un_iff)
          thus ?thesis
            unfolding num_of_odd_nodes_def odd_nodes_set_def
            by (metis (lifting) Collect_empty_eq card_eq_0_iff)
        qed
      ultimately have "∀v∈nodes G1. ∃ps. valid_unMultigraph.is_Eulerian_circuit G1 v ps v"
        using less.hyps[of G1] ‹valid_unMultigraph G1› ‹valid_unMultigraph.connected G1›
        by auto
      then obtain ps1 where ps1:"valid_unMultigraph.is_Eulerian_trail G1 n1 ps1 n1"
        using ‹n1∈nodes G1›
        by (metis (full_types) ‹valid_unMultigraph G1› valid_unMultigraph.is_Eulerian_circuit_def)
      have "card (edges G2) < card (edges G)"
        using G1_G2_edges_union ‹edges (del_unEdge n1 w n2 G) ⊂ edges G›
        by (metis (full_types) ‹finite (edges G)› inf_sup_ord(4) le_less_trans psubset_card_mono)
      moreover have "finite (edges G2)"
        using G1_G2_edges_union ‹finite (edges G)›
        by (metis ‹edges (del_unEdge n1 w n2 G) ⊂ edges G› finite_Un less_imp_le rev_finite_subset)
      moreover have "nodes G2 ⊆ nodes (del_unEdge n1 w n2 G)"
        by (metis G1_G2_nodes_union Un_upper2)
      hence "finite (nodes G2)"
        using  ‹finite (nodes G)›  del_UnEdge_node rev_finite_subset by auto
      moreover have "n2 ∈ nodes G2"
        proof -
          have "n2∈nodes (del_unEdge n1 w n2 G)"
            using ‹n2∈nodes G› by auto
          hence "valid_graph.is_path (del_unEdge n1 w n2 G) n2 [] n2"
            using valid0' by (metis valid_graph.is_path_simps(1))
          thus ?thesis using G2_nodes by auto
        qed
      hence "nodes G2 ≠ {}" by auto
      moreover have "num_of_odd_nodes G2 = 0"
        proof -
          have "valid_graph G1" using ‹valid_unMultigraph G1› valid_unMultigraph_def by auto
          hence "∀n∈nodes G2. degree n G2 = degree n (del_unEdge n1 w n2 G)"
            using sub_graph_degree_frame[of G1 G2 "(del_unEdge n1 w n2 G)"]
            by (metis G1_G2_edges_union ‹nodes G1 ∩ nodes G2 = {}› inf_commute sup_commute)
          hence "∀n∈nodes G2. even(degree n G2)" using all_even
            by (metis G1_G2_nodes_union Un_iff)
          thus ?thesis
            unfolding num_of_odd_nodes_def odd_nodes_set_def
            by (metis (lifting) Collect_empty_eq card_eq_0_iff)
        qed
      ultimately have "∀v∈nodes G2. ∃ps. valid_unMultigraph.is_Eulerian_circuit G2 v ps v"
        using less.hyps[of G2] ‹valid_unMultigraph G2› ‹valid_unMultigraph.connected G2›
        by auto
      then obtain ps2 where ps2:"valid_unMultigraph.is_Eulerian_trail G2 n2 ps2 n2"
        using ‹n2∈nodes G2›
        by (metis (full_types) ‹valid_unMultigraph G2› valid_unMultigraph.is_Eulerian_circuit_def)
      have "⦇nodes = nodes G1 ∪ nodes G2, edges = edges G1 ∪ edges G2 ∪ {(n1, w, n2),
          (n2, w, n1)}⦈=G"
        proof -
          have "edges (del_unEdge n1 w n2 G) ∪ {(n1, w, n2),(n2, w, n1)} =edges G"
            using ‹(n1,w,n2)∈edges G› ‹(n2,w,n1)∈edges G›
            unfolding del_unEdge_def by auto
          moreover have   "nodes (del_unEdge n1 w n2 G)=nodes G"
            unfolding del_unEdge_def by auto
          ultimately have "⦇nodes = nodes (del_unEdge n1 w n2 G), edges =
              edges (del_unEdge n1 w n2 G) ∪ {(n1, w, n2), (n2, w, n1)}⦈=G"
            by auto
          moreover have "⦇nodes = nodes G1 ∪ nodes G2, edges = edges G1 ∪ edges G2 ∪
              {(n1, w, n2),(n2, w, n1)}⦈=⦇nodes = nodes (del_unEdge n1 w n2 G),edges
              = edges (del_unEdge n1 w n2 G) ∪ {(n1, w, n2), (n2, w, n1)}⦈"
            by (metis G1_G2_edges_union G1_G2_nodes_union)
          ultimately show ?thesis by auto
        qed
      moreover have "valid_unMultigraph.is_Eulerian_trail ⦇nodes = nodes G1 ∪ nodes G2,
          edges = edges G1 ∪ edges G2 ∪ {(n1, w, n2), (n2, w, n1)}⦈ n1 (ps1 @ (n1, w, n2) # ps2) n2"
        using eulerian_split[of G1 G2 n1 ps1 n1 n2 ps2 n2 w]
        by (metis ‹edges G1 ∩ edges G2 = {}› ‹nodes G1 ∩ nodes G2 = {}› ‹valid_unMultigraph G1›
          ‹valid_unMultigraph G2› ps1 ps2)
      ultimately show ?thesis by (metis ‹n1 ≠ n2› n1(1) n1(2) n2(1) n2(2))
    qed
  moreover have "v'≠n2 ⟹ (∃v∈nodes G. ∃v'∈nodes G.∃ps. odd (degree v G) ∧ odd (degree v' G)
      ∧ v ≠ v' ∧ valid_unMultigraph.is_Eulerian_trail G v ps v')"
    proof (cases "valid_unMultigraph.connected (del_unEdge n1 w v' G)")
      case True
      assume "v' ≠ n2"
      assume connected':"valid_unMultigraph.connected (del_unEdge n1 w v' G)"
      have "n1 ∈ nodes (del_unEdge n1 w v' G)" by (metis del_UnEdge_node n1(1))
      hence even_n1:"even(degree n1 (del_unEdge n1 w v' G))"
        using valid_unMultigraph.del_UnEdge_even[OF ‹valid_unMultigraph G› ‹(n1, w, v') ∈ edges G›
          ‹finite (edges G)›] ‹odd (degree n1 G)›
        unfolding odd_nodes_set_def by auto
      moreover have odd_n2:"odd(degree n2 (del_unEdge n1 w v' G))"
        using valid_unMultigraph.degree_frame[OF ‹valid_unMultigraph G› ‹finite (edges G)›,
          of n2 n1 v' w] ‹n1 ≠ n2› ‹v' ≠ n2›
        by (metis empty_iff insert_iff n2(2))
      moreover have "even (degree v' G)"
        using even_except_two[of v']
        by (metis (full_types) ‹(n1, w, v') ∈ edges G› ‹v' ≠ n2› ‹valid_graph G›
          ‹valid_unMultigraph G› valid_graph.E_validD(2) valid_unMultigraph.no_id)
      hence odd_v':"odd(degree v' (del_unEdge n1 w v' G))"
        using valid_unMultigraph.del_UnEdge_even'[OF ‹valid_unMultigraph G› ‹(n1, w, v') ∈ edges G›
          ‹finite (edges G)›]
        unfolding odd_nodes_set_def by auto
      ultimately have two_odds:"num_of_odd_nodes (del_unEdge n1 w v' G) = 2"
        by (metis (lifting) ‹v' ≠ n2› ‹valid_graph G› ‹valid_unMultigraph G›
          ‹(n1, w, v') ∈ edges G› ‹finite (edges G)› ‹finite (nodes G)› ‹num_of_odd_nodes G = 2›
          del_UnEdge_odd_even even_except_two n1(2) valid_graph.E_validD(2))
      moreover have valid0:"valid_unMultigraph (del_unEdge n1 w v' G)"
        using del_unEdge_valid ‹valid_unMultigraph G› by auto
      moreover have " edges G - {(n1, w, v'), (v', w, n1)} ⊂ edges G"
        using ‹(n1,w,v')∈edges G› by auto
      hence "card (edges (del_unEdge n1 w v' G)) < card (edges G)"
        using ‹finite (edges G)› unfolding del_unEdge_def
        by (metis (opaque_lifting, no_types) psubset_card_mono select_convs(2))
      moreover have "finite (edges (del_unEdge n1 w v' G))"
        unfolding del_unEdge_def
        by (metis (full_types) ‹finite (edges G)› finite_Diff select_convs(2))
      moreover have "finite (nodes (del_unEdge n1 w v' G))"
        unfolding del_unEdge_def by (metis ‹finite (nodes G)› select_convs(1))
      moreover have "nodes (del_unEdge n1 w v' G) ≠ {}"
        by (metis (full_types) del_UnEdge_node empty_iff n1(1))
      ultimately obtain s t ps where
          s: "s∈nodes (del_unEdge n1 w v' G)" "odd (degree s (del_unEdge n1 w v' G))"
          and t:"t∈nodes (del_unEdge n1 w v' G)" "odd (degree t (del_unEdge n1 w v' G))"
          and "s ≠ t"
          and s_ps_t: "valid_unMultigraph.is_Eulerian_trail (del_unEdge n1 w v' G) s ps t"
        using   connected' less.hyps[of "(del_unEdge n1 w v' G)"] by auto
      hence "(s=n2∧t=v')∨(s=v'∧t=n2)"
        using odd_n2 odd_v' two_odds ‹finite (edges G)›‹valid_unMultigraph G›
        by (metis (mono_tags) del_UnEdge_node empty_iff even_except_two even_n1 insert_iff
          valid_unMultigraph.degree_frame)
      moreover have "s=n2⟹t=v'⟹?thesis"
        by (metis ‹(n1, w, v') ∈ edges G› ‹n1 ≠ n2› ‹valid_unMultigraph G› n1(1) n1(2) n2(1) n2(2)
          s_ps_t valid0 valid_unMultigraph.euclerian_rev valid_unMultigraph.eulerian_cons)
      moreover have "s=v'⟹t=n2⟹?thesis"
        by (metis ‹(n1, w, v') ∈ edges G› ‹n1 ≠ n2› ‹valid_unMultigraph G› n1(1) n1(2) n2(1) n2(2)
          s_ps_t valid_unMultigraph.eulerian_cons)
      ultimately show ?thesis by auto
    next
      case False
      assume "v'≠n2"
      assume not_conneted:"¬valid_unMultigraph.connected (del_unEdge n1 w v' G)"
      have "(v',w,n1)∈edges G" using ‹(n1,w,v')∈edges G›
        by (metis ‹valid_unMultigraph G›  valid_unMultigraph.corres)
      have valid0:"valid_unMultigraph (del_unEdge n1 w v' G)"
        using ‹valid_unMultigraph G› del_unEdge_valid by auto
      hence valid0':"valid_graph (del_unEdge n1 w v' G)"
        using valid_unMultigraph_def by auto
      have even_n1:"even(degree n1 (del_unEdge n1 w v' G))"
        using valid_unMultigraph.del_UnEdge_even[OF ‹valid_unMultigraph G› ‹(n1,w,v')∈edges G›
          ‹finite (edges G)›] n1
        unfolding odd_nodes_set_def by auto
      moreover have odd_n2:"odd(degree n2 (del_unEdge n1 w v' G))"
        using ‹n1 ≠ n2› ‹v' ≠ n2› n2 valid_unMultigraph.degree_frame[OF ‹valid_unMultigraph G›
          ‹finite (edges G)›, of n2 n1 v' w]
        by auto
      moreover have "v'≠n1"
        using valid_unMultigraph.no_id[OF ‹valid_unMultigraph G›] ‹(n1,w,v')∈edges G› by auto
      hence odd_v':"odd(degree v' (del_unEdge n1 w v' G))"
        using  ‹v' ≠ n2›   even_except_two[of v']
          valid_graph.E_validD(2)[OF ‹valid_graph G› ‹(n1, w, v') ∈ edges G›]
          valid_unMultigraph.del_UnEdge_even'[OF  ‹valid_unMultigraph G› ‹(n1, w, v') ∈ edges G›
          ‹finite (edges G)› ]
        unfolding odd_nodes_set_def by auto
      ultimately have even_except_two':"⋀n. n∈nodes (del_unEdge n1 w v' G)⟹ n≠n2
          ⟹ n≠v'⟹ even(degree n (del_unEdge n1 w v' G))"
        using del_UnEdge_node[of _ n1 w v' G] even_except_two valid_unMultigraph.degree_frame[OF
          ‹valid_unMultigraph G› ‹finite (edges G)›, of _ n1 v' w]
        by force
      obtain G1 G2 where
          G1_nodes: "nodes G1={n. ∃ps. valid_graph.is_path (del_unEdge n1 w v' G) n ps n1}"
          and G1_edges: "edges G1={(n,e,n'). (n,e,n')∈edges (del_unEdge n1 w v' G) ∧ n∈nodes G1
            ∧ n'∈nodes G1}"
          and G2_nodes:"nodes G2={n. ∃ps. valid_graph.is_path (del_unEdge n1 w v' G) n ps v'}"
          and G2_edges:"edges G2={(n,e,n'). (n,e,n')∈edges (del_unEdge n1 w v' G) ∧ n∈nodes G2
            ∧ n'∈nodes G2}"
          and G1_G2_edges_union:"edges G1 ∪ edges G2 = edges (del_unEdge n1 w v' G)"
          and "edges G1 ∩ edges G2={}"
          and G1_G2_nodes_union:"nodes G1 ∪ nodes G2=nodes (del_unEdge n1 w v' G)"
          and "nodes G1 ∩ nodes G2={}"
          and "valid_unMultigraph G1"
          and "valid_unMultigraph G2"
          and "valid_unMultigraph.connected G1"
          and "valid_unMultigraph.connected G2"
        using valid_unMultigraph.connectivity_split[OF ‹valid_unMultigraph G›
          ‹valid_unMultigraph.connected G› not_conneted ‹(n1,w,v')∈edges G›]
        .
      have "n2∈nodes G2" using extend_distinct_path
        proof -
          have "finite (edges (del_unEdge n1 w v' G))"
            unfolding del_unEdge_def using ‹finite (edges G)› by auto
          moreover have "num_of_odd_nodes (del_unEdge n1 w v' G) = 2"
            by (metis ‹(n1, w, v') ∈ edges G› ‹(v', w, n1) ∈ edges G› ‹num_of_odd_nodes G = 2›
              ‹v' ≠ n2› ‹valid_graph G› del_UnEdge_even_odd delete_edge_sym even_except_two
              ‹finite (edges G)› ‹finite (nodes G)› ‹valid_unMultigraph G›
              n1(2) valid_graph.E_validD(2) valid_unMultigraph.no_id)
          ultimately have "∃ps. valid_unMultigraph.is_trail (del_unEdge n1 w v' G) n2 ps v'"
            using valid_unMultigraph.path_between_odds[OF valid0,of n2 v',OF odd_n2 odd_v'] ‹v'≠n2›
            by auto
          hence "∃ps. valid_graph.is_path (del_unEdge n1 w v' G) n2 ps v'"
            by (metis valid0 valid_unMultigraph.is_trail_intro)
          thus ?thesis using G2_nodes by auto
        qed
      have "v'∈nodes G2"
        proof -
          have "valid_graph.is_path (del_unEdge n1 w v' G) v' [] v'"
            by (metis (full_types) ‹(n1, w, v') ∈ edges G› ‹valid_graph G› del_UnEdge_node
                valid0' valid_graph.E_validD(2) valid_graph.is_path_simps(1))
          thus ?thesis by (metis (lifting) G2_nodes mem_Collect_eq)
        qed
      have edges_subset:"edges (del_unEdge n1 w v' G) ⊂ edges G"
        using ‹(n1,w,v')∈edges G› ‹(v',w,n1)∈edges G›
        unfolding del_unEdge_def by auto
      hence "card (edges G1) < card (edges G)"
        by (metis G1_G2_edges_union inf_sup_absorb ‹finite (edges G)›  less_infI2 psubset_card_mono)
      moreover have "finite (edges G1)"
        by (metis (full_types) G1_G2_edges_union edges_subset finite_Un finite_subset
          ‹finite (edges G)›  less_imp_le)
      moreover have "finite (nodes G1)"
        using G1_G2_nodes_union  ‹finite (nodes G)›
        unfolding del_unEdge_def
        by (metis (full_types) finite_Un select_convs(1))
      moreover have "n1∈nodes G1"
        proof -
          have "valid_graph.is_path (del_unEdge n1 w v' G) n1 [] n1"
            by (metis (full_types) del_UnEdge_node n1(1) valid0' valid_graph.is_path_simps(1))
          thus ?thesis by (metis (lifting) G1_nodes mem_Collect_eq)
        qed
      moreover hence "nodes G1 ≠ {}" by auto
      moreover have "num_of_odd_nodes G1 = 0"
        proof -
          have "∀n∈nodes G1. even(degree n (del_unEdge n1 w v' G))"
            using even_except_two' odd_v' odd_n2 ‹n2∈nodes G2› ‹nodes G1 ∩ nodes G2 = {}›
              ‹v'∈nodes G2›
            by (metis (full_types) G1_G2_nodes_union Un_iff disjoint_iff_not_equal)
          moreover have "valid_graph G2"
            using ‹valid_unMultigraph G2› valid_unMultigraph_def
            by auto
          ultimately have "∀n∈nodes G1. even(degree n G1)"
            using sub_graph_degree_frame[of G2 G1 "del_unEdge n1 w v' G"]
            by (metis G1_G2_edges_union ‹nodes G1 ∩ nodes G2 = {}›)
          thus ?thesis unfolding num_of_odd_nodes_def odd_nodes_set_def
            by (metis (lifting) card_eq_0_iff empty_Collect_eq)
        qed
      ultimately obtain ps1 where ps1:"valid_unMultigraph.is_Eulerian_trail G1 n1 ps1 n1"
        using ‹valid_unMultigraph G1› ‹valid_unMultigraph.connected G1› less.hyps[of G1]
        by (metis valid_unMultigraph.is_Eulerian_circuit_def)
      have "card (edges G2) < card (edges G)"
        by (metis G1_G2_edges_union ‹finite (edges G)› edges_subset inf_sup_absorb less_infI2
          psubset_card_mono sup_commute)
      moreover have "finite (edges G2)"
        by (metis (full_types) G1_G2_edges_union edges_subset finite_Un ‹finite (edges G)› less_le
          rev_finite_subset)
      moreover have "finite (nodes G2)"
        by (metis (mono_tags) G1_G2_nodes_union del_UnEdge_node le_sup_iff ‹finite (nodes G)›
          rev_finite_subset subsetI)
      moreover have "nodes G2 ≠ {}" using ‹v'∈nodes G2› by auto
      moreover have "num_of_odd_nodes G2 = 2"
        proof -
          have "∀n∈nodes G2. n∉{n2,v'}⟶even(degree n (del_unEdge n1 w v' G))"
            using even_except_two'
            by (metis (full_types) G1_G2_nodes_union Un_iff insert_iff)
          moreover have "valid_graph G1"
            using ‹valid_unMultigraph G1› valid_unMultigraph_def by auto
          ultimately have "∀n∈nodes G2. n∉{n2,v'}⟶even(degree n G2)"
            using sub_graph_degree_frame[of G1 G2 "del_unEdge n1 w v' G"]
            by (metis G1_G2_edges_union Int_commute Un_commute ‹nodes G1 ∩ nodes G2 = {}›)
          hence "∀n∈nodes G2. n∉{n2,v'}⟶n∉{v ∈ nodes G2. odd (degree v G2)}"
            by (metis (lifting) mem_Collect_eq)
          moreover have "odd(degree n2 G2)"
            using sub_graph_degree_frame[of G1 G2 "del_unEdge n1 w v' G"]
            by (metis (opaque_lifting, no_types) G1_G2_edges_union ‹nodes G1 ∩ nodes G2 = {}›
              ‹valid_graph G1› ‹n2 ∈ nodes G2› inf_assoc inf_bot_right inf_sup_absorb
               odd_n2 sup_bot_right sup_commute)
          hence "n2∈{v ∈ nodes G2. odd (degree v G2)}"
            by (metis (lifting) ‹n2 ∈ nodes G2› mem_Collect_eq)
          moreover have "odd(degree v' G2)"
            using sub_graph_degree_frame[of G1 G2 "del_unEdge n1 w v' G"]
            by (metis G1_G2_edges_union Int_commute Un_commute ‹nodes G1 ∩ nodes G2 = {}›
              ‹v' ∈ nodes G2› ‹valid_graph G1› odd_v')
          hence "v'∈{v ∈ nodes G2. odd (degree v G2)}"
            by (metis (full_types) Collect_conj_eq Collect_mem_eq Int_Collect ‹v' ∈ nodes G2›)
          ultimately have "{v ∈ nodes G2. odd (degree v G2)}={n2,v'}"
            using ‹finite (nodes G2)› by (induct G2,auto)
          thus ?thesis using ‹v'≠n2›
            unfolding num_of_odd_nodes_def odd_nodes_set_def by auto
        qed
      ultimately obtain s t ps2 where
          s: "s∈nodes G2" "odd (degree s G2)"
          and t:"t∈nodes G2" "odd (degree t G2)"
          and "s ≠ t"
          and s_ps2_t: "valid_unMultigraph.is_Eulerian_trail G2 s ps2 t"
        using ‹valid_unMultigraph G2› ‹valid_unMultigraph.connected G2› less.hyps[of G2]
        by auto
      moreover have "valid_graph G1"
        using ‹valid_unMultigraph G1› valid_unMultigraph_def by auto
      ultimately have "(s=n2∧t=v')∨(s=v'∧t=n2)"
        using odd_n2 odd_v' even_except_two'
          sub_graph_degree_frame[of G1 G2 "(del_unEdge n1 w v' G)"]
        by (metis G1_G2_edges_union G1_G2_nodes_union UnI1 ‹nodes G1 ∩ nodes G2 = {}› inf_commute
          sup.commute)
      moreover have merge_G1_G2:"⦇nodes = nodes G1 ∪ nodes G2, edges = edges G1 ∪ edges G2 ∪
          {(n1, w,v'),(v', w, n1)}⦈=G"
        proof -
          have "edges (del_unEdge n1 w v' G) ∪ {(n1, w, v'),(v', w, n1)} =edges G"
            using  ‹(n1,w,v')∈edges G› ‹(v',w,n1)∈edges G›
            unfolding del_unEdge_def by auto
          moreover have "nodes (del_unEdge n1 w v' G)=nodes G"
            unfolding del_unEdge_def by auto
          ultimately have "⦇nodes = nodes (del_unEdge n1 w v' G), edges =
              edges (del_unEdge n1 w v' G) ∪ {(n1, w, v'), (v', w, n1)}⦈=G"
            by auto
          moreover have "⦇nodes = nodes G1 ∪ nodes G2, edges = edges G1 ∪ edges G2 ∪
              {(n1, w, v'),(v', w, n1)}⦈=⦇nodes = nodes (del_unEdge n1 w v' G),edges
              = edges (del_unEdge n1 w v' G) ∪ {(n1, w, v'), (v', w, n1)}⦈"
            by (metis G1_G2_edges_union G1_G2_nodes_union)
          ultimately show ?thesis by auto
        qed
      moreover have "s=n2⟹t=v'⟹?thesis"
        using eulerian_split[of G1 G2 n1 ps1 n1 v' "(rev_path ps2)" n2 w] merge_G1_G2
        by (metis ‹edges G1 ∩ edges G2 = {}› ‹n1 ≠ n2› ‹nodes G1 ∩ nodes G2 = {}›
            ‹valid_unMultigraph G1› ‹valid_unMultigraph G2› n1(1) n1(2) n2(1) n2(2) ps1 s_ps2_t
            valid_unMultigraph.euclerian_rev)
      moreover have "s=v'⟹t=n2⟹?thesis"
        using eulerian_split[of G1 G2 n1 ps1 n1 v' ps2 n2 w] merge_G1_G2
        by (metis ‹edges G1 ∩ edges G2 = {}› ‹n1 ≠ n2› ‹nodes G1 ∩ nodes G2 = {}›
          ‹valid_unMultigraph G1› ‹valid_unMultigraph G2› n1(1) n1(2) n2(1) n2(2) ps1 s_ps2_t)
      ultimately show ?thesis by auto
    qed
  ultimately show "∃v∈nodes G. ∃v'∈nodes G.∃ps. odd (degree v G) ∧ odd (degree v' G) ∧ v ≠ v'
      ∧ valid_unMultigraph.is_Eulerian_trail G v ps v'"
    by auto
next
  case less
  assume "finite (edges G)" and "finite (nodes G)" and "valid_unMultigraph G" and "nodes G≠{}"
      and "valid_unMultigraph.connected G" and "num_of_odd_nodes G = 0"
  show "∀v∈nodes G. ∃ps. valid_unMultigraph.is_Eulerian_circuit G v ps v"
    proof (rule,cases "card (nodes G)=1")
      fix v assume "v∈nodes G"
      assume " card (nodes G) = 1 "
      hence "nodes G={v}"
        using ‹v ∈ nodes G›  card_Suc_eq[of "nodes G" 0] empty_iff insert_iff[of _ v]
        by auto
      have "edges G={}"
        proof (rule ccontr)
          assume "edges G ≠ {}"
          then obtain e1 e2 e3 where e:"(e1,e2,e3)∈edges G" by (metis ex_in_conv prod_cases3)
          hence "e1=e3" using ‹nodes G={v}›
            by (metis (opaque_lifting, no_types) append_Nil2 valid_unMultigraph.is_trail_rev
                valid_unMultigraph.is_trail.simps(1) ‹valid_unMultigraph G› singletonE
                valid_unMultigraph.is_trail_split valid_unMultigraph.singleton_distinct_path)
          thus False by (metis e ‹valid_unMultigraph G› valid_unMultigraph.no_id)
        qed
      hence "valid_unMultigraph.is_Eulerian_circuit G v [] v"
        by (metis ‹nodes G = {v}› insert_subset ‹valid_unMultigraph G› rem_unPath.simps(1)
            subsetI valid_unMultigraph.is_trail.simps(1)
            valid_unMultigraph.is_Eulerian_circuit_def
            valid_unMultigraph.is_Eulerian_trail_def)
      thus "∃ps. valid_unMultigraph.is_Eulerian_circuit G v ps v" by auto
    next
      fix v assume "v∈nodes G"
      assume "card (nodes G) ≠ 1"
      moreover have "card (nodes G)≠0" using ‹nodes G≠{}›
        by (metis card_eq_0_iff ‹finite (nodes G)›)
      ultimately have "card (nodes G) ≥2" by auto
      then obtain n where "card (nodes G) = Suc (Suc n)"
        by (metis le_iff_add add_2_eq_Suc)
      hence "∃n∈nodes G. n≠v" by (auto dest!: card_eq_SucD)
      then obtain v' w where "(v,w,v')∈edges G"
        proof -
          assume pre:"⋀w v'. (v, w, v') ∈ edges G ⟹ thesis"
          assume "∃n∈nodes G. n ≠ v"
          then obtain ps where  ps:"∃v'. valid_graph.is_path G v ps v' ∧ ps≠Nil"
            using valid_unMultigraph_def
            by (metis (full_types) ‹v ∈ nodes G› ‹valid_unMultigraph G› valid_graph.is_path.simps(1)
              ‹valid_unMultigraph.connected G› valid_unMultigraph.connected_def)
          then obtain v0 w v' where "∃ps'. ps=Cons (v0,w,v') ps'" by (metis neq_Nil_conv prod_cases3)
          hence "v0=v"
            using valid_unMultigraph_def
            by (metis ‹valid_unMultigraph G› ps valid_graph.is_path.simps(2))
          hence "(v,w,v')∈edges G"
            using valid_unMultigraph_def
            by (metis ‹∃ps'. ps = (v0, w, v') # ps'› ‹valid_unMultigraph G› ps
              valid_graph.is_path.simps(2))
          thus ?thesis by (metis pre)
        qed
      have all_even:"∀x∈nodes G. even(degree x G)"
        using ‹finite (nodes G)› ‹num_of_odd_nodes G = 0›
        unfolding num_of_odd_nodes_def odd_nodes_set_def by auto
      have odd_v: "odd (degree v (del_unEdge v w v' G))"
        using  ‹v ∈ nodes G› all_even valid_unMultigraph.del_UnEdge_even[OF ‹valid_unMultigraph G›
          ‹(v, w, v') ∈ edges G› ‹finite (edges G)›]
        unfolding odd_nodes_set_def by auto
      have odd_v':  "odd (degree v' (del_unEdge v w v' G))"
        using valid_unMultigraph.del_UnEdge_even'[OF ‹valid_unMultigraph G› ‹(v, w, v') ∈ edges G›
          ‹finite (edges G)›]
            all_even  valid_graph.E_validD(2)[OF _ ‹(v, w, v') ∈ edges G›]
            ‹valid_unMultigraph G›
        unfolding valid_unMultigraph_def odd_nodes_set_def
        by auto
      have valid_unMulti:"valid_unMultigraph (del_unEdge v w v' G)"
        by (metis del_unEdge_valid ‹valid_unMultigraph G›)
      moreover have valid_graph: "valid_graph (del_unEdge v w v' G)"
        using valid_unMultigraph_def del_undirected
        by (metis ‹valid_unMultigraph G› delete_edge_valid)
      moreover have fin_E': "finite(edges (del_unEdge v w v' G))"
        using ‹finite(edges G)› unfolding del_unEdge_def by auto
      moreover have fin_V': "finite(nodes (del_unEdge v w v' G))"
        using ‹finite(nodes G)› unfolding del_unEdge_def by auto
      moreover have less_card:"card(edges (del_unEdge v w v' G))<card(edges G)"
        unfolding del_unEdge_def using ‹(v,w,v')∈edges G›
        by (metis Diff_insert2 card_Diff2_less ‹finite (edges G)› ‹valid_unMultigraph G›
          select_convs(2) valid_unMultigraph.corres)
      moreover have "num_of_odd_nodes (del_unEdge v w v' G) = 2"
        using ‹valid_unMultigraph G› ‹num_of_odd_nodes G = 0› ‹v ∈ nodes G› all_even
          del_UnEdge_even_even[OF ‹valid_unMultigraph G›  ‹finite (edges G)› ‹finite (nodes G)›
          ‹(v, w, v') ∈ edges G›] valid_graph.E_validD(2)[OF _ ‹(v, w, v') ∈ edges G›]
        unfolding  valid_unMultigraph_def
        by auto
      moreover have "valid_unMultigraph.connected (del_unEdge v w v' G)"
        using ‹finite (edges G)› ‹finite (nodes G)› ‹valid_unMultigraph G›
          ‹valid_unMultigraph.connected G›
        by (metis ‹(v, w, v') ∈ edges G› all_even valid_unMultigraph.del_unEdge_even_connectivity)
      moreover have "nodes(del_unEdge v w v' G)≠{}"
        by (metis ‹v ∈ nodes G› del_UnEdge_node emptyE)
      ultimately obtain n1 n2 ps where
          n1_n2:
          "n1∈nodes (del_unEdge v w v' G)"
          "n2∈nodes (del_unEdge v w v' G)"
          "odd (degree n1 (del_unEdge v w v' G))"
          "odd (degree n2 (del_unEdge v w v' G))"
          "n1≠n2"
          and
          ps_eulerian:
          "valid_unMultigraph.is_Eulerian_trail (del_unEdge v w v' G) n1 ps n2"
        by (metis ‹num_of_odd_nodes (del_unEdge v w v' G) = 2› less.hyps(1))
      have "n1=v⟹n2=v'⟹valid_unMultigraph.is_Eulerian_circuit G v (ps@[(v',w,v)]) v"
        using ps_eulerian
        by (metis ‹(v, w, v') ∈ edges G› delete_edge_sym ‹valid_unMultigraph G›
          valid_unMultigraph.corres valid_unMultigraph.eulerian_cons'
          valid_unMultigraph.is_Eulerian_circuit_def)
      moreover have "n1=v'⟹n2=v⟹∃ps. valid_unMultigraph.is_Eulerian_circuit G v ps v"
        by (metis ‹(v, w, v') ∈ edges G› ‹valid_unMultigraph G› ps_eulerian
          valid_unMultigraph.eulerian_cons valid_unMultigraph.is_Eulerian_circuit_def)
      moreover have "(n1=v∧n2=v')∨(n2=v∧n1=v')"
        by (metis (mono_tags) all_even del_UnEdge_node insert_iff ‹finite (edges G)›
          ‹valid_unMultigraph G› n1_n2(1) n1_n2(2) n1_n2(3) n1_n2(4) n1_n2(5) singletonE
          valid_unMultigraph.degree_frame)
      ultimately show "∃ps. valid_unMultigraph.is_Eulerian_circuit G v ps v" by auto
    qed
qed
end