Theory MoreGraph

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

theory MoreGraph imports Complex_Main Dijkstra_Shortest_Path.Graph
begin
section ‹Undirected Multigraph and undirected trails›

locale valid_unMultigraph=valid_graph G for G::"('v,'w) graph"+
              assumes corres[simp]: "(v,w,u') ∈ edges G ⟷ (u',w,v) ∈ edges G"
                and   no_id[simp]:"(v,w,v) ∉ edges G"

fun (in valid_unMultigraph) is_trail :: "'v ⇒ ('v,'w) path ⇒ 'v ⇒ bool" where
      "is_trail v [] v' ⟷ v=v' ∧ v'∈ V" |
      "is_trail v ((v1,w,v2)#ps) v' ⟷ v=v1 ∧ (v1,w,v2)∈E ∧ 
                (v1,w,v2)∉set ps ∧(v2,w,v1)∉set ps ∧ is_trail v2 ps v'"

(*This section mainly includes lemmas related to degrees of nodes, especially when edges and paths 
are removed from an undirected graph*)
section ‹Degrees and related properties›

definition degree :: "'v ⇒ ('v,'w) graph ⇒ nat" where
    "degree v g≡ card({e. e∈edges g ∧ fst e=v})"

definition odd_nodes_set :: "('v,'w) graph ⇒ 'v set" where
    "odd_nodes_set g ≡ {v. v∈nodes g ∧ odd(degree v g)}"

  (*return the number of nodes with an odd degree in the current valid multigraph*)
definition num_of_odd_nodes :: "('v, 'w) graph ⇒ nat" where
    "num_of_odd_nodes g≡ card( odd_nodes_set g)"

definition num_of_even_nodes :: "('v, 'w) graph ⇒ nat" where
    "num_of_even_nodes g≡ card( {v. v∈nodes g ∧ even(degree v g)})"

definition del_unEdge where "del_unEdge v e v' g ≡ ⦇
    nodes = nodes g, edges = edges g - {(v,e,v'),(v',e,v)} ⦈"

definition rev_path :: "('v,'w) path ⇒ ('v,'w) path" where
    "rev_path ps ≡ map (λ(a,b,c).(c,b,a)) (rev ps)"

fun rem_unPath:: "('v,'w) path ⇒ ('v,'w) graph ⇒ ('v,'w) graph" where
    "rem_unPath [] g= g"|
    "rem_unPath ((v,w,v')#ps) g= 
        rem_unPath ps (del_unEdge v w v' g)" 
    
lemma del_undirected: "del_unEdge v e v' g = delete_edge v' e v (delete_edge v e v' g)"
  unfolding del_unEdge_def delete_edge_def by auto

lemma delete_edge_sym: "del_unEdge v e v' g = del_unEdge v' e v g" 
  unfolding del_unEdge_def by auto

lemma del_unEdge_valid[simp]: assumes "valid_unMultigraph g" 
    shows "valid_unMultigraph (del_unEdge v e v' g)"
proof -
  interpret valid_unMultigraph g by fact
  show ?thesis 
    unfolding del_unEdge_def
    by unfold_locales (auto dest: E_validD) 
qed

 
lemma set_compre_diff:"{x ∈ A - B. P x}={x ∈ A. P x} - {x ∈ B . P x}" by blast
lemma set_compre_subset: "B ⊆ A ⟹ {x ∈ B. P x} ⊆ {x ∈ A. P x}" by blast 

lemma del_edge_undirected_degree_plus: "finite (edges g) ⟹ (v,e,v') ∈ edges g 
    ⟹ (v',e,v) ∈ edges g  ⟹ degree v (del_unEdge v e v' g) + 1=degree v g" 
proof -
  assume assms: "finite (edges g)" "(v,e,v') ∈ edges g" "(v',e,v) ∈ edges g "
  have "degree v (del_unEdge v e v' g) + 1
          = card ({ea ∈  edges g - {(v, e, v'), (v', e, v)}. fst ea = v}) + 1"  
    unfolding del_unEdge_def degree_def by simp
  also have "...=card ({ea ∈  edges g. fst ea = v} - {ea ∈ {(v, e, v'), (v', e, v)}. 
      fst ea = v})+1" 
    by (metis set_compre_diff) 
  also have "...=card ({ea ∈  edges g. fst ea = v}) - card({ea ∈ {(v, e, v'), (v', e, v)}. 
      fst ea = v})+1" 
    proof -
      have "{(v, e, v'), (v', e, v)} ⊆ edges g" using ‹(v,e,v') ∈ edges g› ‹(v',e,v) ∈ edges g› 
        by auto
      hence "{ea ∈ {(v, e, v'), (v', e, v)}. fst ea = v} ⊆ {ea ∈  edges g. fst ea = v}" by auto
      moreover have "finite {ea ∈ {(v, e, v'), (v', e, v)}. fst ea = v}" by auto
      ultimately have "card ({ea ∈ edges g. fst ea = v} - {ea ∈ {(v, e, v'), (v', e, v)}. 
          fst ea = v})=card {ea ∈ edges g. fst ea = v} - card {ea ∈ {(v, e, v'), (v', e, v)}.
          fst ea = v}"
        using card_Diff_subset by blast
      thus ?thesis by auto 
    qed
  also have "...=card ({ea ∈  edges g. fst ea = v})" 
    proof -
      have "{ea ∈ {(v, e, v'), (v', e, v)}. fst ea = v}={(v,e,v')}" by auto
      hence "card {ea ∈ {(v, e, v'), (v', e, v)}. fst ea = v} = 1" by auto
      moreover have "card {ea ∈ edges g. fst ea = v}≠0" 
        by (metis (lifting, mono_tags) Collect_empty_eq assms(1) assms(2) 
          card_eq_0_iff fst_conv mem_Collect_eq rev_finite_subset subsetI)
      ultimately show ?thesis by arith
    qed
  finally have "degree v (del_unEdge v e v' g) + 1=card ({ea ∈  edges g. fst ea = v})" .
  thus ?thesis unfolding degree_def .
qed

lemma del_edge_undirected_degree_plus': "finite (edges g) ⟹ (v,e,v') ∈ edges g 
    ⟹ (v',e,v) ∈ edges g ⟹ degree v' (del_unEdge v e v' g) + 1=degree v' g"
  by (metis del_edge_undirected_degree_plus delete_edge_sym) 

lemma del_edge_undirected_degree_minus[simp]: "finite (edges g) ⟹ (v,e,v') ∈ edges g 
    ⟹ (v',e,v) ∈ edges g ⟹ degree v (del_unEdge v e v' g) =degree v g- (1::nat)" 
  using del_edge_undirected_degree_plus by (metis add_diff_cancel_left' add.commute)

lemma del_edge_undirected_degree_minus'[simp]: "finite (edges g) ⟹ (v,e,v') ∈ edges g 
    ⟹ (v',e,v) ∈ edges g ⟹ degree v' (del_unEdge v e v' g) =degree v' g- (1::nat)"
  by (metis del_edge_undirected_degree_minus delete_edge_sym) 


lemma del_unEdge_com: "del_unEdge v w v' (del_unEdge n e n' g)
          = del_unEdge n e n' (del_unEdge v w v' g)" 
  unfolding del_unEdge_def by auto

lemma rem_unPath_com: "rem_unPath ps (del_unEdge v w v' g) 
            = del_unEdge v w v' (rem_unPath ps g)" 
proof (induct ps arbitrary: g)
  case Nil
  thus ?case by (metis rem_unPath.simps(1))
next
  case (Cons a ps')
  thus ?case using del_unEdge_com 
    by (metis prod_cases3 rem_unPath.simps(1) rem_unPath.simps(2))
qed

lemma rem_unPath_valid[intro]: 
  "valid_unMultigraph g ⟹ valid_unMultigraph (rem_unPath ps g)"
proof (induct ps )
  case Nil
  thus ?case by simp
next
  case (Cons x xs)
  thus ?case 
    proof -
    have "valid_unMultigraph (rem_unPath (x # xs) g) = valid_unMultigraph 
         (del_unEdge (fst x) (fst (snd x)) (snd (snd x)) (rem_unPath xs g))"
      using rem_unPath_com by (metis prod.collapse rem_unPath.simps(2))
    also have "...=valid_unMultigraph (rem_unPath xs g)" 
      by (metis Cons.hyps Cons.prems del_unEdge_valid)
    also have "...=True" 
      using Cons by auto
    finally have "?case=True" .
    thus ?case by simp
    qed
qed 


lemma (in valid_unMultigraph) degree_frame:
    assumes "finite (edges G)"  "x ∉ {v, v'}" 
    shows "degree x (del_unEdge v w v' G) = degree x G" (is "?L=?R")
proof (cases "(v,w,v') ∈ edges G")
  case True
  have "?L=card({e. e∈edges G - {(v,w,v'),(v',w,v)} ∧ fst e=x})" 
    by (simp add:del_unEdge_def degree_def)
  also have "...=card({e. e∈edges G ∧ fst e=x}-{e. e∈{(v,w,v'),(v',w,v)} ∧ fst e=x})"
    by (metis  set_compre_diff)
  also have "...=card({e. e∈edges G ∧ fst e=x})" using ‹x ∉ {v, v'}› 
    proof -
      have "x≠v ∧ x≠ v'" using ‹x∉{v,v'}›by simp
      hence "{e. e∈{(v,w,v'),(v',w,v)} ∧ fst e=x}={}" by auto
      thus ?thesis by (metis Diff_empty)
    qed
  also have "...=?R" by (simp add:degree_def)
  finally show ?thesis .
next
  case False
  moreover hence "(v',w,v)∉E" using corres by auto
  ultimately have "E- {(v,w,v'),(v',w,v)}=E" by blast   
  hence "del_unEdge v w v' G=G" by (auto simp add:del_unEdge_def)
  thus ?thesis by auto
qed

lemma [simp]: "rev_path [] = []" unfolding rev_path_def by simp
lemma rev_path_append[simp]: "rev_path (xs@ys) = (rev_path ys) @ (rev_path xs)" 
  unfolding rev_path_def rev_append by auto
lemma rev_path_double[simp]: "rev_path(rev_path xs)=xs" 
  unfolding rev_path_def by (induct xs,auto)

lemma del_UnEdge_node[simp]: "v∈nodes (del_unEdge u e u' G) ⟷ v∈nodes G  " 
    by (metis del_unEdge_def select_convs(1))

lemma [intro!]: "finite (edges G) ⟹ finite (edges (del_unEdge u e u' G))"
    by (metis del_unEdge_def finite_Diff select_convs(2))

lemma [intro!]: "finite (nodes G) ⟹ finite (nodes (del_unEdge u e u' G))"
    by (metis del_unEdge_def select_convs(1))
 
lemma [intro!]: "finite (edges G) ⟹ finite (edges (rem_unPath ps G))"
proof (induct ps arbitrary:G)
  case Nil
  thus ?case by simp
next
  case (Cons x xs)
  hence "finite (edges (rem_unPath (x # xs) G)) = finite (edges (del_unEdge 
          (fst x) (fst (snd x)) (snd (snd x)) (rem_unPath xs G)))" 
    by (metis rem_unPath.simps(2) rem_unPath_com surjective_pairing)
  also have "...=finite (edges (rem_unPath xs G))" 
    using del_unEdge_def  
    by (metis  finite.emptyI finite_Diff2 finite_Diff_insert select_convs(2))
  also have "...=True" using Cons by auto
  finally have "?case = True" .
  thus ?case by simp
qed

lemma del_UnEdge_frame[intro]: 
  "x∈edges g ⟹ x≠(v,e,v') ⟹x≠(v',e,v) ⟹ x∈edges (del_unEdge v e v' g)"
  unfolding del_unEdge_def by auto

lemma [intro!]: "finite (nodes G) ⟹ finite (odd_nodes_set G)"
    by (metis (lifting) mem_Collect_eq odd_nodes_set_def rev_finite_subset subsetI)

lemma [simp]: "nodes (del_unEdge u e u' G)=nodes G" 
    by (metis del_unEdge_def select_convs(1))

lemma [simp]: "nodes (rem_unPath ps G) = nodes G" 
proof (induct ps)
  case Nil
  show ?case by simp
next 
  case (Cons x xs)
  have "nodes (rem_unPath (x # xs) G)=nodes (del_unEdge 
        (fst x) (fst (snd x)) (snd (snd x)) (rem_unPath xs G))" 
    by (metis rem_unPath.simps(2) rem_unPath_com surjective_pairing)
  also have "...=nodes (rem_unPath xs G)" by auto
  also have "...=nodes G" using Cons by auto
  finally show ?case .
qed

lemma [intro!]: "finite (nodes G) ⟹ finite (nodes (rem_unPath ps G))" by auto

lemma in_set_rev_path[simp]: "(v',w,v )∈set (rev_path ps) ⟷ (v,w,v')∈set ps " 
proof (induct ps)
  case Nil
  thus ?case unfolding rev_path_def by auto
next
  case (Cons x xs)
  obtain x1 x2 x3 where x:"x=(x1,x2,x3)" by (metis prod_cases3)
  have "set (rev_path (x # xs))=set ((rev_path xs)@[(x3,x2,x1)])" 
    unfolding rev_path_def 
    using x by auto
  also have "...=set (rev_path xs) ∪ {(x3,x2,x1)}" by auto
  finally have "set (rev_path (x # xs)) =set (rev_path xs) ∪ {(x3,x2,x1)}" .
  moreover have "set (x#xs)= set xs ∪ {(x1,x2,x3)}" 
    by (metis List.set_simps(2) insert_is_Un sup_commute x)
  ultimately show ?case using Cons by auto
qed

lemma rem_unPath_edges: 
    "edges(rem_unPath ps G) = edges G - (set ps ∪ set (rev_path ps))" 
proof (induct ps)
  case Nil
  show ?case unfolding rev_path_def by auto
next
  case (Cons x xs)
  obtain x1 x2 x3 where x: "x=(x1,x2,x3)" by (metis prod_cases3)
  hence "edges(rem_unPath (x#xs) G)= edges(del_unEdge x1 x2 x3 (rem_unPath xs G))"
    by (metis rem_unPath.simps(2) rem_unPath_com)
  also have "...=edges(rem_unPath xs G)-{(x1,x2,x3),(x3,x2,x1)}"
    by (metis del_unEdge_def select_convs(2))
  also have "...= edges G - (set xs ∪ set (rev_path xs))-{(x1,x2,x3),(x3,x2,x1)}"
    by (metis Cons.hyps)
  also have "...=edges G - (set (x#xs) ∪ set (rev_path (x#xs)))"  
    proof -
      have "set (rev_path xs) ∪ {(x3,x2,x1)}=set ((rev_path xs)@[(x3,x2,x1)])" 
        by (metis List.set_simps(2) empty_set set_append)
      also have "...=set (rev_path (x#xs))" unfolding rev_path_def using  x by auto
      finally have "set (rev_path xs) ∪ {(x3,x2,x1)}=set (rev_path (x#xs))" .
      moreover have "set xs ∪ {(x1,x2,x3)}=set (x#xs)" 
        by (metis List.set_simps(2) insert_is_Un sup_commute x)
      moreover have "edges G - (set xs ∪ set (rev_path xs))-{(x1,x2,x3),(x3,x2,x1)} =
                      edges G - ((set xs ∪ {(x1,x2,x3)}) ∪ (set (rev_path xs) ∪ {(x3,x2,x1)}))" 
        by auto 
      ultimately show ?thesis by auto
    qed
  finally show ?case .
qed  

lemma rem_unPath_graph [simp]: 
    "rem_unPath (rev_path ps) G=rem_unPath ps G"
proof -
  have "nodes(rem_unPath (rev_path ps) G)=nodes(rem_unPath ps G)" 
    by auto
  moreover have "edges(rem_unPath (rev_path ps) G)=edges(rem_unPath ps G)"  
    proof -
      have "set (rev_path ps) ∪ set (rev_path (rev_path ps)) = set ps ∪  set (rev_path ps) " 
        by auto
      thus ?thesis by (metis rem_unPath_edges)
    qed
  ultimately show ?thesis by auto
qed 

lemma distinct_rev_path[simp]: "distinct (rev_path ps) ⟷distinct ps" 
proof (induct ps)
  case Nil
  show ?case by auto
next 
  case (Cons x xs)
  obtain x1 x2 x3 where x: "x=(x1,x2,x3)" by (metis prod_cases3)
  hence "distinct (rev_path (x # xs))=distinct ((rev_path xs)@[(x3,x2,x1)])" 
    unfolding rev_path_def by auto
  also have "...= (distinct (rev_path xs) ∧ (x3,x2,x1)∉set (rev_path xs))" 
    by (metis distinct.simps(2) distinct1_rotate rotate1.simps(2))
  also have "...=distinct (x#xs)" 
    by (metis Cons.hyps distinct.simps(2) in_set_rev_path x)
  finally have "distinct (rev_path (x # xs))=distinct (x#xs)" .
  thus ?case .
qed


lemma (in valid_unMultigraph) is_path_rev: "is_path v' (rev_path ps) v ⟷ is_path v ps v'" 
proof (induct ps arbitrary: v)
  case Nil
  show ?case by auto
next
  case (Cons x xs)
  obtain x1 x2 x3 where x: "x=(x1,x2,x3)" by (metis prod_cases3)
  hence "is_path v' (rev_path (x # xs)) v=is_path v' ((rev_path xs) @[(x3,x2,x1)]) v" 
    unfolding rev_path_def by auto
  also have "...=(is_path v' (rev_path xs) x3 ∧ (x3,x2,x1)∈E ∧ is_path x1 [] v)" by auto
  also have "...=(is_path x3 xs v' ∧ (x3,x2,x1)∈E ∧ is_path x1 [] v)" using Cons.hyps by auto
  also have "...=is_path v (x#xs) v'" 
    by (metis corres is_path.simps(1) is_path.simps(2) is_path_memb x)
  finally have "is_path v' (rev_path (x # xs)) v=is_path v (x#xs) v'" .
  thus ?case .
qed


lemma (in valid_unMultigraph) singleton_distinct_path [intro]:
   "(v,w,v')∈E ⟹ is_trail v [(v,w,v')] v'" 
   by (metis E_validD(2) all_not_in_conv is_trail.simps set_empty) 
  
lemma (in valid_unMultigraph) is_trail_path: 
  "is_trail v ps v' ⟷ is_path v ps v' ∧ distinct ps ∧ (set ps ∩ set (rev_path ps) = {})"
proof (induct ps arbitrary:v)
  case Nil
  show ?case by auto
next
  case (Cons x xs)
  obtain x1 x2 x3 where x: "x=(x1,x2,x3)" by (metis prod_cases3)
  hence "is_trail v (x#xs) v'= (v=x1 ∧ (x1,x2,x3)∈E ∧ 
                (x1,x2,x3)∉set xs ∧(x3,x2,x1)∉set xs ∧ is_trail x3 xs v')" 
    by (metis is_trail.simps(2))
  also have "...=(v=x1 ∧ (x1,x2,x3)∈E ∧  (x1,x2,x3)∉set xs ∧(x3,x2,x1)∉set xs ∧ is_path x3 xs v' 
                  ∧ distinct xs ∧ (set xs ∩ set (rev_path xs)={}))" 
    using Cons.hyps by auto
  also have "...=(is_path v (x#xs) v' ∧ (x1,x2,x3) ≠ (x3,x2,x1) ∧ (x1,x2,x3)∉set xs 
                  ∧(x3,x2,x1)∉set xs ∧ distinct xs ∧ (set xs ∩ set (rev_path xs)={}))"
    by (metis append_Nil is_path.simps(1) is_path_simps(2) is_path_split' no_id x)
  also have "...=(is_path v (x#xs) v' ∧ (x1,x2,x3) ≠ (x3,x2,x1) ∧(x3,x2,x1)∉set xs 
                  ∧ distinct (x#xs) ∧ (set xs ∩ set (rev_path xs)={}))"
    by (metis (full_types) distinct.simps(2) x)
  also have "...=(is_path v (x#xs) v' ∧ (x1,x2,x3) ≠ (x3,x2,x1) ∧ distinct (x#xs) 
                  ∧ (x3,x2,x1)∉set xs ∧ set xs ∩ set (rev_path (x#xs))={})" 
    proof -
      have "set (rev_path (x#xs)) = set ((rev_path xs)@[(x3,x2,x1)])" using x by auto
      also have "... = set (rev_path xs) ∪ {(x3,x2,x1)}" by auto
      finally have "set (rev_path (x#xs))=set (rev_path xs) ∪ {(x3,x2,x1)}" .
      thus ?thesis by blast
    qed
  also have "...=(is_path v (x#xs) v'∧ distinct (x#xs) ∧ (set (x#xs) ∩ set (rev_path (x#xs))={}))"
    proof -
      have "(x3,x2,x1)∉set xs ⟷ (x1,x2,x3)∉ set (rev_path xs)" using in_set_rev_path by auto
      moreover have  "set (rev_path (x#xs))=set (rev_path xs) ∪ {(x3,x2,x1)}" 
        unfolding rev_path_def using x by auto
      ultimately have " (x1,x2,x3) ≠ (x3,x2,x1)∧ (x3,x2,x1)∉set xs 
                        ⟷ (x1,x2,x3)∉ set (rev_path (x#xs))"  by blast 
      thus ?thesis 
        by (metis (mono_tags) Int_iff Int_insert_left_if0 List.set_simps(2) empty_iff insertI1 x)
    qed
  finally have "is_trail v (x#xs) v'⟷(is_path v (x#xs) v'∧ distinct (x#xs) 
                  ∧ (set (x#xs) ∩ set (rev_path (x#xs))={}))" .
  thus ?case .
qed      
 
lemma  (in valid_unMultigraph) is_trail_rev: 
    "is_trail v' (rev_path ps) v ⟷ is_trail v ps v' " 
    using rev_path_append is_trail_path  is_path_rev distinct_rev_path
    by (metis Int_commute distinct_append)

lemma (in valid_unMultigraph) is_trail_intro[intro]:
  "is_trail v' ps v ⟹ is_path v' ps v" by (induct ps arbitrary:v',auto)   

lemma (in valid_unMultigraph) is_trail_split:
      "is_trail v (p1@p2) v' ⟹ (∃u. is_trail v p1 u ∧ is_trail u p2 v')"
apply (induct p1 arbitrary: v,auto) 
apply (metis is_trail_intro is_path_memb)
done

lemma (in valid_unMultigraph) is_trail_split':"is_trail v (p1@(u,w,u')#p2) v' 
    ⟹ is_trail v p1 u ∧ (u,w,u')∈E ∧ is_trail u' p2 v'"
  by (metis is_trail.simps(2) is_trail_split)

lemma (in valid_unMultigraph) distinct_elim[simp]:
  assumes "is_trail v ((v1,w,v2)#ps) v'" 
  shows "(v1,w,v2)∈edges(rem_unPath ps G) ⟷ (v1,w,v2)∈E" 
proof 
  assume "(v1, w, v2) ∈ edges (rem_unPath ps G)"
  thus "(v1, w, v2) ∈ E" by (metis assms is_trail.simps(2))
next
  assume "(v1, w, v2) ∈ E"
  have "(v1,w,v2)∉set ps ∧ (v2,w,v1)∉set ps" by (metis assms is_trail.simps(2))
  hence "(v1,w,v2)∉set ps ∧ (v1,w,v2)∉set (rev_path ps)" by simp
  hence "(v1,w,v2)∉set ps ∪ set (rev_path ps)" by simp
  hence "(v1,w,v2)∈edges G - (set ps ∪ set (rev_path ps))"
    using ‹(v1, w, v2) ∈ E› by auto
  thus "(v1,w,v2)∈edges(rem_unPath ps G)" 
    by (metis rem_unPath_edges)
qed

lemma distinct_path_subset:
  assumes "valid_unMultigraph G1" "valid_unMultigraph G2" "edges G1 ⊆edges G2" "nodes G1 ⊆nodes G2"
  assumes distinct_G1:"valid_unMultigraph.is_trail G1 v ps v'"
  shows "valid_unMultigraph.is_trail G2 v ps v'" using distinct_G1
proof (induct ps arbitrary:v)
  case Nil
  hence "v=v'∧v'∈nodes G1" 
    by (metis (full_types) assms(1) valid_unMultigraph.is_trail.simps(1))
  hence "v=v'∧v'∈nodes G2" using ‹nodes G1 ⊆ nodes G2› by auto
  thus ?case by (metis assms(2) valid_unMultigraph.is_trail.simps(1))
next
  case (Cons x xs)
  obtain x1 x2 x3 where x:"x=(x1,x2,x3)" by (metis prod_cases3)
  hence "valid_unMultigraph.is_trail G1 x3 xs v'"
    by (metis Cons.prems assms(1) valid_unMultigraph.is_trail.simps(2)) 
  hence "valid_unMultigraph.is_trail G2 x3 xs v'" using Cons by auto
  moreover have "x∈edges G1"
    by (metis Cons.prems assms(1) valid_unMultigraph.is_trail.simps(2) x)
  hence "x∈edges G2" using ‹edges G1 ⊆ edges G2› by auto
  moreover have "v=x1∧(x1,x2,x3)∉set xs∧(x3,x2,x1)∉set xs"
    by (metis Cons.prems assms(1) valid_unMultigraph.is_trail.simps(2) x)
  hence "v=x1" "(x1,x2,x3)∉set xs" "(x3,x2,x1)∉set xs" by auto
  ultimately show ?case by (metis assms(2) valid_unMultigraph.is_trail.simps(2) x)
qed

lemma (in valid_unMultigraph) distinct_path_intro':
  assumes "valid_unMultigraph.is_trail (rem_unPath p G) v ps v'"
  shows "is_trail  v ps v'" 
proof -
  have valid:"valid_unMultigraph (rem_unPath p G)"
    using rem_unPath_valid[OF valid_unMultigraph_axioms,of p] by auto
  moreover have "nodes (rem_unPath p G) ⊆ V" by auto
  moreover have "edges (rem_unPath p G) ⊆ E" 
    using rem_unPath_edges by auto
  ultimately show ?thesis 
    using distinct_path_subset[of "rem_unPath p G" G] valid_unMultigraph_axioms assms 
    by auto
qed

lemma (in valid_unMultigraph) distinct_path_intro:
  assumes "valid_unMultigraph.is_trail (del_unEdge x1 x2 x3 G) v ps v'"
  shows "is_trail  v ps v'" 
by (metis (full_types) assms distinct_path_intro' rem_unPath.simps(1) 
    rem_unPath.simps(2))

lemma (in valid_unMultigraph) distinct_elim_rev[simp]:
  assumes "is_trail v ((v1,w,v2)#ps) v'" 
  shows "(v2,w,v1)∈edges(rem_unPath ps G) ⟷ (v2,w,v1)∈E"
proof -
  have  "valid_unMultigraph (rem_unPath ps G)" using valid_unMultigraph_axioms by auto            
  hence "(v2,w,v1)∈edges(rem_unPath ps G)⟷(v1,w,v2)∈edges(rem_unPath ps G)"
    by (metis valid_unMultigraph.corres)
  moreover have "(v2,w,v1)∈E⟷(v1,w,v2)∈E" using corres by simp
  ultimately show ?thesis using distinct_elim by (metis assms)
qed
      
lemma (in valid_unMultigraph) del_UnEdge_even:
  assumes "(v,w,v') ∈ E" "finite E"
  shows "v∈odd_nodes_set(del_unEdge v w v' G) ⟷ even (degree v G)" 
proof -
  have "degree v (del_unEdge v w v' G) + 1=degree v G" 
    using del_edge_undirected_degree_plus corres by (metis assms)
  from this [symmetric] have "odd (degree v (del_unEdge v w v' G)) = even (degree v G)"
    by simp
  moreover have "v∈nodes (del_unEdge v w v' G)" by (metis E_validD(1) assms(1) del_UnEdge_node)
  ultimately show ?thesis unfolding odd_nodes_set_def by auto
qed

lemma (in valid_unMultigraph) del_UnEdge_even':
  assumes "(v,w,v') ∈ E" "finite E"
  shows "v'∈odd_nodes_set(del_unEdge v w v' G) ⟷ even (degree v' G)" 
proof -
  show ?thesis by (metis (full_types) assms corres del_UnEdge_even delete_edge_sym)          
qed

lemma del_UnEdge_even_even:
    assumes "valid_unMultigraph G" "finite(edges G)" "finite(nodes G)" "(v, w, v')∈edges G"
    assumes parity_assms: "even (degree v G)" "even (degree v' G)"
    shows "num_of_odd_nodes(del_unEdge v w v' G)=num_of_odd_nodes G + 2"
proof -
  interpret G:valid_unMultigraph by fact 
  have  "v∈odd_nodes_set(del_unEdge v w v' G)"  
    by (metis G.del_UnEdge_even assms(2) assms(4) parity_assms(1))
  moreover have  "v'∈odd_nodes_set(del_unEdge v w v' G)"  
    by (metis G.del_UnEdge_even' assms(2) assms(4) parity_assms(2))
  ultimately have extra_odd_nodes:"{v,v'} ⊆ odd_nodes_set(del_unEdge v w v' G)"
    unfolding odd_nodes_set_def by auto
  moreover have "v ∉odd_nodes_set G" and "v'∉odd_nodes_set G" 
    using parity_assms unfolding odd_nodes_set_def by auto 
  hence vv'_odd_disjoint: "{v,v'} ∩ odd_nodes_set G = {}" by auto
  moreover have "odd_nodes_set(del_unEdge v w v' G) -{v,v'}⊆odd_nodes_set G " 
    proof
      fix x
      assume x_odd_set: "x ∈ odd_nodes_set (del_unEdge v w v' G) - {v, v'}"
      hence "degree x (del_unEdge v w v' G) = degree x G" 
        by (metis Diff_iff G.degree_frame assms(2))
      hence "odd(degree x G)" using x_odd_set
        unfolding odd_nodes_set_def by auto
      moreover have "x ∈ nodes G" using x_odd_set unfolding odd_nodes_set_def by auto
      ultimately show "x ∈ odd_nodes_set G" unfolding odd_nodes_set_def by auto
    qed
  moreover have "odd_nodes_set G ⊆ odd_nodes_set(del_unEdge v w v' G)" 
    proof 
      fix x
      assume x_odd_set:  "x ∈ odd_nodes_set G"
      hence "x∉{v,v'} ⟹ odd(degree x (del_unEdge v w v' G))" 
        by (metis (lifting) G.degree_frame assms(2) mem_Collect_eq odd_nodes_set_def)
      hence "x∉{v,v'} ⟹ x∈odd_nodes_set(del_unEdge v w v' G)" 
        using x_odd_set del_UnEdge_node unfolding odd_nodes_set_def by auto 
      moreover have "x∈{v,v'} ⟹ x∈odd_nodes_set(del_unEdge v w v' G)" 
        using extra_odd_nodes by auto
      ultimately show "x ∈ odd_nodes_set (del_unEdge v w v' G)" by auto
    qed
  ultimately have "odd_nodes_set(del_unEdge v w v' G)=odd_nodes_set G ∪ {v,v'}" by auto
  thus "num_of_odd_nodes(del_unEdge v w v' G) = num_of_odd_nodes G + 2"
    proof -
      assume "odd_nodes_set(del_unEdge v w v' G)=odd_nodes_set G ∪ {v,v'}"
      moreover have "v≠v'" using G.no_id ‹(v,w,v')∈edges G› by auto
      hence "card{v,v'}=2" by simp
      moreover have " odd_nodes_set G ∩ {v,v'} = {}" 
        using vv'_odd_disjoint by auto
      moreover have "finite(odd_nodes_set G)" 
        by (metis (lifting) assms(3) mem_Collect_eq odd_nodes_set_def rev_finite_subset subsetI)
      moreover have "finite {v,v'}" by auto
      ultimately show ?thesis unfolding num_of_odd_nodes_def using card_Un_disjoint by metis
    qed
qed
  
lemma del_UnEdge_even_odd:
    assumes "valid_unMultigraph G" "finite(edges G)" "finite(nodes G)" "(v, w, v')∈edges G"
    assumes parity_assms: "even (degree v G)" "odd (degree v' G)"
    shows "num_of_odd_nodes(del_unEdge v w v' G)=num_of_odd_nodes G"
proof -
  interpret G : valid_unMultigraph by fact
  have odd_v:"v∈odd_nodes_set(del_unEdge v w v' G)" 
    by (metis G.del_UnEdge_even assms(2) assms(4) parity_assms(1))
  have  not_odd_v':"v'∉odd_nodes_set(del_unEdge v w v' G)"
    by (metis G.del_UnEdge_even' assms(2) assms(4) parity_assms(2))
  have "odd_nodes_set(del_unEdge v w v' G) ∪ {v'} ⊆odd_nodes_set G ∪ {v}"
    proof 
      fix x 
      assume x_prems:" x ∈ odd_nodes_set (del_unEdge v w v' G) ∪ {v'}"
      have "x=v' ⟹x∈odd_nodes_set G ∪ {v}" 
        using parity_assms
        by (metis (lifting) G.E_validD(2) Un_def assms(4) mem_Collect_eq odd_nodes_set_def )
      moreover have "x=v ⟹ x∈odd_nodes_set G ∪ {v}"  
        by (metis insertI1 insert_is_Un sup_commute)
      moreover have "x∉{v,v'} ⟹ x ∈ odd_nodes_set (del_unEdge v w v' G)" 
        using x_prems by auto
      hence "x∉{v,v'} ⟹ x ∈ odd_nodes_set G" unfolding odd_nodes_set_def
        using G.degree_frame ‹finite (edges G)› by auto
      hence "x∉{v,v'} ⟹ x∈odd_nodes_set G ∪ {v}" by simp 
      ultimately show "x ∈ odd_nodes_set G ∪ {v}" by auto
    qed
  moreover have "odd_nodes_set G ∪ {v} ⊆ odd_nodes_set(del_unEdge v w v' G) ∪ {v'}" 
    proof
      fix x
      assume x_prems: "x ∈ odd_nodes_set G ∪ {v}"
      have "x=v ⟹ x ∈ odd_nodes_set (del_unEdge v w v' G) ∪ {v'}" 
        by (metis UnI1 odd_v)
      moreover have "x=v' ⟹ x ∈ odd_nodes_set (del_unEdge v w v' G) ∪ {v'}" 
        by auto
      moreover have "x∉{v,v'} ⟹ x ∈ odd_nodes_set G ∪ {v}" using x_prems by auto
      hence "x∉{v,v'} ⟹  x∈odd_nodes_set (del_unEdge v w v' G)" unfolding odd_nodes_set_def
        using G.degree_frame ‹finite (edges G)› by auto
      hence "x∉{v,v'} ⟹ x ∈ odd_nodes_set (del_unEdge v w v' G) ∪ {v'}" by simp
        ultimately show "x ∈ odd_nodes_set (del_unEdge v w v' G) ∪ {v'}" by auto
    qed
  ultimately have "odd_nodes_set(del_unEdge v w v' G) ∪ {v'} = odd_nodes_set G ∪ {v}"
    by auto
  moreover have " odd_nodes_set G ∩ {v} = {}" 
    using parity_assms unfolding odd_nodes_set_def by auto
  moreover have " odd_nodes_set(del_unEdge v w v' G) ∩ {v'}={}" 
    by (metis Int_insert_left_if0 inf_bot_left inf_commute not_odd_v')
  moreover have "finite (odd_nodes_set(del_unEdge v w v' G))" 
     using ‹finite (nodes G)› by auto
  moreover have "finite (odd_nodes_set G)" using ‹finite (nodes G)› by auto
  ultimately have "card(odd_nodes_set G) + card {v} = 
                   card(odd_nodes_set(del_unEdge v w v' G)) + card {v'}" 
    using card_Un_disjoint[of "odd_nodes_set (del_unEdge v w v' G)" "{v'}"] 
      card_Un_disjoint[of "odd_nodes_set G" "{v}"] 
    by auto 
  thus ?thesis unfolding num_of_odd_nodes_def by simp 
qed  
  
lemma del_UnEdge_odd_even:
    assumes "valid_unMultigraph G" "finite(edges G)" "finite(nodes G)" "(v, w, v')∈edges G"
    assumes parity_assms: "odd (degree v G)" "even (degree v' G)"
    shows "num_of_odd_nodes(del_unEdge v w v' G)=num_of_odd_nodes G"  
by (metis assms del_UnEdge_even_odd delete_edge_sym parity_assms valid_unMultigraph.corres)
 
lemma del_UnEdge_odd_odd:
    assumes "valid_unMultigraph G" "finite(edges G)" "finite(nodes G)" "(v, w, v')∈edges G"
    assumes parity_assms: "odd (degree v G)" "odd (degree v' G)"
    shows "num_of_odd_nodes G=num_of_odd_nodes(del_unEdge v w v' G)+2"
proof -
  interpret G:valid_unMultigraph by fact
  have  "v∉odd_nodes_set(del_unEdge v w v' G)"  
    by (metis G.del_UnEdge_even assms(2) assms(4) parity_assms(1))
  moreover have  "v'∉odd_nodes_set(del_unEdge v w v' G)"  
    by (metis G.del_UnEdge_even' assms(2) assms(4) parity_assms(2))
  ultimately have vv'_disjoint: "{v,v'} ∩ odd_nodes_set(del_unEdge v w v' G) = {}" 
    by (metis (full_types) Int_insert_left_if0 inf_bot_left)
  moreover have extra_odd_nodes:"{v,v'} ⊆ odd_nodes_set( G)"
    unfolding odd_nodes_set_def 
    using ‹(v,w,v')∈edges G›
    by (metis (lifting) G.E_validD empty_subsetI insert_subset mem_Collect_eq parity_assms)  
  moreover have "odd_nodes_set G -{v,v'}⊆odd_nodes_set (del_unEdge v w v' G) " 
    proof
      fix x
      assume x_odd_set: "x ∈ odd_nodes_set G - {v, v'}"
      hence "degree x G = degree x (del_unEdge v w v' G)" 
        by (metis Diff_iff G.degree_frame assms(2))
      hence "odd(degree x (del_unEdge v w v' G))" using x_odd_set 
        unfolding odd_nodes_set_def by auto
      moreover have "x ∈ nodes (del_unEdge v w v' G)" 
        using x_odd_set unfolding odd_nodes_set_def by auto
      ultimately show "x ∈ odd_nodes_set (del_unEdge v w v' G)" 
        unfolding odd_nodes_set_def by auto
    qed
  moreover have "odd_nodes_set (del_unEdge v w v' G) ⊆ odd_nodes_set G" 
    proof 
      fix x
      assume x_odd_set:  "x ∈ odd_nodes_set (del_unEdge v w v' G)"
      hence "x∉{v,v'} ⟹ odd(degree x G)" 
        using assms G.degree_frame unfolding odd_nodes_set_def
        by auto
      hence "x∉{v,v'} ⟹ x∈odd_nodes_set G" 
        using x_odd_set del_UnEdge_node unfolding odd_nodes_set_def  
        by auto
      moreover have "x∈{v,v'} ⟹ x∈odd_nodes_set G" 
        using extra_odd_nodes by auto
      ultimately show "x ∈ odd_nodes_set G" by auto
    qed
  ultimately have "odd_nodes_set G=odd_nodes_set (del_unEdge v w v' G) ∪ {v,v'}" 
    by auto
  thus ?thesis
    proof -
      assume "odd_nodes_set G=odd_nodes_set (del_unEdge v w v' G) ∪ {v,v'}"
      moreover have " odd_nodes_set (del_unEdge v w v' G) ∩ {v,v'} = {}" 
        using vv'_disjoint by auto
      moreover have "finite(odd_nodes_set (del_unEdge v w v' G))" 
        using assms del_UnEdge_node finite_subset unfolding odd_nodes_set_def
        by auto
      moreover have "finite {v,v'}" by auto
      ultimately have "card(odd_nodes_set G)
                       = card(odd_nodes_set  (del_unEdge v w v' G)) + card{v,v'}"
        unfolding num_of_odd_nodes_def 
        using card_Un_disjoint 
        by metis 
      moreover have "v≠v'" using G.no_id ‹(v,w,v')∈edges G› by auto
      hence "card{v,v'}=2" by simp
      ultimately show ?thesis unfolding num_of_odd_nodes_def by simp
    qed
qed 

lemma (in valid_unMultigraph) rem_UnPath_parity_v': 
  assumes "finite E"  "is_trail v ps v'" 
  shows "v≠v' ⟷ (odd (degree v' (rem_unPath ps G)) = even(degree v' G))" using assms 
proof (induct ps arbitrary:v)
  case Nil
  thus ?case by (metis is_trail.simps(1) rem_unPath.simps(1))
next
  case (Cons x xs) print_cases
  obtain x1 x2 x3 where x: "x=(x1,x2,x3)" by (metis prod_cases3)
  hence rem_x:"odd (degree v' (rem_unPath (x#xs) G)) = odd(degree v' (del_unEdge
            x1 x2 x3 (rem_unPath xs G)))" 
    by (metis  rem_unPath.simps(2) rem_unPath_com)
  have "x3=v' ⟹ ?case" 
    proof (cases "v=v'")
      case True 
      assume "x3=v'"
      have "x1=v'" using x by (metis Cons.prems(2) True is_trail.simps(2))
      thus ?thesis using ‹x3=v'› by (metis Cons.prems(2) is_trail.simps(2) no_id x)
    next
      case False
      assume "x3=v'"
      have "odd (degree v' (rem_unPath (x # xs) G)) =odd(degree v' (
            del_unEdge x1 x2 x3 (rem_unPath xs G)))" using rem_x .
      also have "...=odd(degree v' (rem_unPath xs G) - 1)" 
        proof -
          have "finite (edges (rem_unPath xs G))" 
            by (metis (full_types) assms(1) finite_Diff rem_unPath_edges)
          moreover have "(x1,x2,x3) ∈edges( rem_unPath xs G)" 
            by (metis Cons.prems(2) distinct_elim is_trail.simps(2) x)
          moreover have "(x3,x2,x1) ∈edges( rem_unPath xs G)"
            by (metis Cons.prems(2) corres distinct_elim_rev is_trail.simps(2) x)
          ultimately show ?thesis 
            by (metis ‹x3 = v'› del_edge_undirected_degree_minus delete_edge_sym  x)
        qed
      also have "...=even(degree v' (rem_unPath xs G))"
        proof -
          have "(x1,x2,x3)∈E" by (metis Cons.prems(2) is_trail.simps(2) x)
          hence "(x3,x2,x1)∈edges (rem_unPath xs G)" 
            by (metis Cons.prems(2) corres distinct_elim_rev x)
          hence "(x3,x2,x1)∈{e ∈ edges (rem_unPath xs G). fst e = v'}" 
            using ‹x3=v'› by (metis (mono_tags) fst_conv mem_Collect_eq)
          moreover have "finite {e ∈ edges (rem_unPath xs G). fst e = v'}"
            using ‹finite E› by auto
          ultimately have "degree v' (rem_unPath xs G)≠0" 
            unfolding degree_def by auto
          thus ?thesis by auto
        qed
      also have "...=even (degree v' G)" 
        using ‹x3 = v'› assms
        by (metis (mono_tags) Cons.hyps Cons.prems(2) is_trail.simps(2) x)
      finally have "odd (degree v' (rem_unPath (x # xs) G))=even (degree v' G)" .
      thus ?thesis by (metis False)
    qed
  moreover have "x3≠v'⟹?case" 
    proof (cases "v=v'")
      case True
      assume "x3≠v'"
      have "odd (degree v' (rem_unPath (x # xs) G)) =odd(degree v' (
            del_unEdge x1 x2 x3 (rem_unPath xs G)))" using rem_x .
      also have "...=odd(degree v' (rem_unPath xs G) - 1)" 
        proof -
          have "finite (edges (rem_unPath xs G))" 
            by (metis (full_types) assms(1) finite_Diff rem_unPath_edges)
          moreover have "(x1,x2,x3) ∈edges( rem_unPath xs G)" 
            by (metis Cons.prems(2) distinct_elim is_trail.simps(2) x)
          moreover have "(x3,x2,x1) ∈edges( rem_unPath xs G)"
            by (metis Cons.prems(2) corres distinct_elim_rev is_trail.simps(2) x)
          ultimately show ?thesis 
            using True x
            by (metis Cons.prems(2) del_edge_undirected_degree_minus is_trail.simps(2))
        qed
      also have "...=even(degree v' (rem_unPath xs G))"
        proof -
          have "(x1,x2,x3)∈E" by (metis Cons.prems(2) is_trail.simps(2) x)
          hence "(x1,x2,x3)∈edges (rem_unPath xs G)" 
            by (metis Cons.prems(2) distinct_elim x)
          hence "(x1,x2,x3)∈{e ∈ edges (rem_unPath xs G). fst e = v'}" 
            using ‹v=v'› x  Cons
            by (metis (lifting, mono_tags) fst_conv is_trail.simps(2) mem_Collect_eq) 
          moreover have "finite {e ∈ edges (rem_unPath xs G). fst e = v'}"
            using ‹finite E› by auto
          ultimately have "degree v' (rem_unPath xs G)≠0" 
            unfolding degree_def by auto
          thus ?thesis by auto
        qed
      also have "...≠even (degree v' G)" 
        using ‹x3 ≠ v'› assms 
        by (metis Cons.hyps Cons.prems(2)is_trail.simps(2) x)
      finally have "odd (degree v' (rem_unPath (x # xs) G))≠even (degree v' G)" .
      thus ?thesis by (metis True)
    next 
      case False
      assume "x3≠v'"
      have "odd (degree v' (rem_unPath (x # xs) G)) =odd(degree v' (
            del_unEdge x1 x2 x3 (rem_unPath xs G)))" using rem_x .
      also have "...=odd(degree v' (rem_unPath xs G))" 
        proof -
          have "v=x1" by (metis Cons.prems(2) is_trail.simps(2) x)
          hence "v'∉{x1,x3}" by (metis (mono_tags) False ‹x3 ≠ v'› empty_iff insert_iff) 
          moreover have "valid_unMultigraph (rem_unPath xs G)" 
            using valid_unMultigraph_axioms by auto
          moreover have "finite (edges (rem_unPath xs G))" 
            by (metis (full_types) assms(1) finite_Diff rem_unPath_edges)
          ultimately have "degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G))
                            =degree v' (rem_unPath xs G)" using degree_frame 
            by (metis valid_unMultigraph.degree_frame)
          thus ?thesis by simp
        qed
      also have "...=even (degree v' G)"
        using assms x ‹x3 ≠ v'›
        by (metis Cons.hyps Cons.prems(2)  is_trail.simps(2))
      finally have "odd (degree v' (rem_unPath (x # xs) G))=even (degree v' G)" .
      thus ?thesis by (metis False)
    qed
  ultimately show ?case by auto
qed

lemma (in valid_unMultigraph) rem_UnPath_parity_v: 
  assumes "finite E"  "is_trail v ps v'" 
  shows "v≠v' ⟷ (odd (degree v (rem_unPath ps G)) = even(degree v G))" 
by (metis assms is_trail_rev rem_UnPath_parity_v' rem_unPath_graph)

lemma (in valid_unMultigraph) rem_UnPath_parity_others:
  assumes "finite E"  "is_trail v ps v'" "n∉{v,v'}"
  shows " even (degree n (rem_unPath ps G)) = even(degree n G)" using assms
proof (induct ps arbitrary: v)
  case Nil
  thus ?case by auto
next
  case (Cons x xs)
  obtain x1 x2 x3 where x:"x=(x1,x2,x3)" by (metis prod_cases3) 
  hence "even (degree n (rem_unPath (x#xs) G))= even (degree n (
          del_unEdge x1 x2 x3 (rem_unPath xs G)))" 
    by (metis rem_unPath.simps(2) rem_unPath_com)
  have "n=x3 ⟹?case" 
    proof - 
      assume "n=x3"
      have "even (degree n (rem_unPath (x#xs) G))= even (degree n (
          del_unEdge x1 x2 x3 (rem_unPath xs G)))" 
        by (metis rem_unPath.simps(2) rem_unPath_com x)
      also have "...=even(degree n (rem_unPath xs G) - 1)" 
        proof -
          have "finite (edges (rem_unPath xs G))" 
            by (metis (full_types) assms(1) finite_Diff rem_unPath_edges)
          moreover have "(x1,x2,x3) ∈edges( rem_unPath xs G)" 
            by (metis Cons.prems(2) distinct_elim is_trail.simps(2) x)
          moreover have "(x3,x2,x1) ∈edges( rem_unPath xs G)"
            by (metis Cons.prems(2) corres distinct_elim_rev is_trail.simps(2) x)
          ultimately show ?thesis 
            using ‹n = x3› del_edge_undirected_degree_minus' 
            by auto
        qed
      also have "...=odd(degree n (rem_unPath xs G))"
        proof -
          have "(x1,x2,x3)∈E" by (metis Cons.prems(2) is_trail.simps(2) x)
          hence "(x3,x2,x1)∈edges (rem_unPath xs G)" 
            by (metis Cons.prems(2) corres distinct_elim_rev x)
          hence "(x3,x2,x1)∈{e ∈ edges (rem_unPath xs G). fst e = n}" 
            using ‹n=x3› by (metis (mono_tags) fst_conv mem_Collect_eq)
          moreover have "finite {e ∈ edges (rem_unPath xs G). fst e = n}"
            using ‹finite E› by auto
          ultimately have "degree n (rem_unPath xs G)≠0" 
            unfolding degree_def by auto
          thus ?thesis by auto
        qed
      also have "...=even(degree n G)" 
        proof -
          have "x3≠v'" by (metis ‹n = x3› assms(3) insert_iff)
          hence "odd (degree x3 (rem_unPath xs G)) = even(degree x3 G)"
            using Cons assms
            by (metis is_trail.simps(2) rem_UnPath_parity_v x)
          thus ?thesis using ‹n=x3› by auto
        qed
      finally have "even (degree n (rem_unPath (x#xs) G))=even(degree n G)" .
      thus ?thesis .
    qed
  moreover have "n≠x3 ⟹?case" 
    proof -
      assume "n≠x3"
       have "even (degree n (rem_unPath (x#xs) G))= even (degree n (
          del_unEdge x1 x2 x3 (rem_unPath xs G)))" 
        by (metis rem_unPath.simps(2) rem_unPath_com x)
      also have "...=even(degree n (rem_unPath xs G))" 
        proof -
          have "v=x1" by (metis Cons.prems(2) is_trail.simps(2) x)
          hence "n∉{x1,x3}" by (metis Cons.prems(3) ‹n ≠ x3› insertE insertI1 singletonE)
          moreover have "valid_unMultigraph (rem_unPath xs G)" 
            using valid_unMultigraph_axioms by auto
          moreover have "finite (edges (rem_unPath xs G))" 
            by (metis (full_types) assms(1) finite_Diff rem_unPath_edges)
          ultimately have "degree n (del_unEdge x1 x2 x3 (rem_unPath xs G))
                            =degree n (rem_unPath xs G)" using degree_frame 
            by (metis valid_unMultigraph.degree_frame)
          thus ?thesis by simp
        qed
      also have "...=even(degree n G)" 
        using Cons assms ‹n ≠ x3› x by auto
      finally have "even (degree n (rem_unPath (x#xs) G))=even(degree n G)" .
      thus ?thesis .
    qed
  ultimately show ?case by auto
qed
    
lemma (in valid_unMultigraph) rem_UnPath_even:
  assumes "finite E" "finite V" "is_trail v ps v'" 
  assumes parity_assms:  "even (degree v' G)"
  shows "num_of_odd_nodes (rem_unPath ps G) = num_of_odd_nodes G 
          + (if even (degree v G)∧ v≠v' then 2 else 0)" using assms
proof (induct ps arbitrary:v)
  case Nil 
  thus ?case by auto
next
  case (Cons x xs)
  obtain x1 x2 x3 where x:"x=(x1,x2,x3)" by (metis prod_cases3) 
  have fin_nodes: "finite (nodes (rem_unPath xs G))" using Cons by auto
  have fin_edges: "finite (edges (rem_unPath xs G))" using Cons by auto
  have valid_rem_xs: "valid_unMultigraph (rem_unPath xs G)" using valid_unMultigraph_axioms 
    by auto
  have x_in:"(x1,x2,x3)∈edges (rem_unPath xs G)" 
    by (metis (full_types) Cons.prems(3) distinct_elim is_trail.simps(2) x)
  have "even (degree x1 (rem_unPath xs G)) 
        ⟹ even(degree x3 (rem_unPath xs G)) ⟹ ?case" 
    proof -
      assume parity_x1_x3: "even (degree x1 (rem_unPath xs G))" 
                           "even(degree x3 (rem_unPath xs G))"
      have "num_of_odd_nodes (rem_unPath (x#xs) G)= num_of_odd_nodes 
         (del_unEdge x1 x2 x3 (rem_unPath xs G))"
        by (metis rem_unPath.simps(2) rem_unPath_com x)
      also have "... =num_of_odd_nodes (rem_unPath xs G)+2" 
        using  parity_x1_x3  fin_nodes fin_edges valid_rem_xs x_in del_UnEdge_even_even 
        by metis
      also have "...=num_of_odd_nodes G+(if even(degree x3 G) ∧ x3≠v' then 2 else 0 )+2"
        using Cons.hyps[OF ‹finite E› ‹finite V›, of x3] ‹is_trail v (x # xs) v'›
          ‹even (degree v' G)› x 
        by auto
      also have "...=num_of_odd_nodes G+2" 
        proof -
          have "even(degree x3 G) ∧ x3≠v' ⟷ odd (degree x3 (rem_unPath xs G))" 
            using Cons.prems assms
            by (metis  is_trail.simps(2) parity_x1_x3(2) rem_UnPath_parity_v x)
          thus ?thesis using parity_x1_x3(2) by auto
        qed
      also have "...=num_of_odd_nodes G+(if even(degree v G) ∧ v≠v' then 2 else 0)" 
        proof -
          have "x1≠x3" by (metis valid_rem_xs valid_unMultigraph.no_id x_in)
          moreover hence "x1≠v'" 
            using Cons assms  
            by (metis is_trail.simps(2)  parity_x1_x3(1) rem_UnPath_parity_v' x)
          ultimately have "x1∉{x3,v'}" by auto
          hence  "even(degree x1 G)" 
            using Cons.prems(3) assms(1) assms(2) parity_x1_x3(1) 
            by (metis (full_types)  is_trail.simps(2) rem_UnPath_parity_others x)
          hence "even(degree x1 G) ∧ x1≠v'" using ‹x1 ≠ v'› by auto
          hence "even(degree v G) ∧ v≠v'" by (metis Cons.prems(3) is_trail.simps(2) x)
          thus ?thesis by auto
        qed
      finally have "num_of_odd_nodes (rem_unPath (x#xs) G)=
                        num_of_odd_nodes G+(if even(degree v G) ∧ v≠v' then 2 else 0)" .
      thus ?thesis .
    qed       
  moreover have "even (degree x1 (rem_unPath xs G)) ⟹ 
                    odd(degree x3 (rem_unPath xs G)) ⟹ ?case" 
    proof -
      assume parity_x1_x3: "even (degree x1 (rem_unPath xs G))" 
                           "odd (degree x3 (rem_unPath xs G))"
      have "num_of_odd_nodes (rem_unPath (x#xs) G)= num_of_odd_nodes 
         (del_unEdge x1 x2 x3 (rem_unPath xs G))"
        by (metis rem_unPath.simps(2) rem_unPath_com x)
      also have "... =num_of_odd_nodes (rem_unPath xs G)" 
        using  parity_x1_x3  fin_nodes fin_edges valid_rem_xs x_in 
        by (metis del_UnEdge_even_odd)
      also have "...=num_of_odd_nodes G+(if even(degree x3 G) ∧ x3≠v' then 2 else 0 )"
        using  Cons.hyps Cons.prems(3) assms(1) assms(2)  parity_assms x
        by auto
      also have "...=num_of_odd_nodes G+2" 
         proof -
          have "even(degree x3 G) ∧ x3≠v' ⟷ odd (degree x3 (rem_unPath xs G))" 
            using Cons.prems assms
            by (metis  is_trail.simps(2) parity_x1_x3(2) rem_UnPath_parity_v x)
          thus ?thesis using parity_x1_x3(2) by auto
        qed
      also have "...=num_of_odd_nodes G+(if even(degree v G) ∧ v≠v' then 2 else 0)"
        proof -
          have "x1≠x3" by (metis valid_rem_xs valid_unMultigraph.no_id x_in)
          moreover hence "x1≠v'" 
            using Cons assms  
            by (metis is_trail.simps(2)  parity_x1_x3(1) rem_UnPath_parity_v' x)
          ultimately have "x1∉{x3,v'}" by auto
          hence  "even(degree x1 G)" 
            using Cons.prems(3) assms(1) assms(2) parity_x1_x3(1) 
            by (metis (full_types)  is_trail.simps(2) rem_UnPath_parity_others x)
          hence "even(degree x1 G) ∧ x1≠v'" using ‹x1 ≠ v'› by auto
          hence "even(degree v G) ∧ v≠v'" by (metis Cons.prems(3) is_trail.simps(2) x)
          thus ?thesis by auto
        qed
      finally have "num_of_odd_nodes (rem_unPath (x#xs) G)=
                        num_of_odd_nodes G+(if even(degree v G) ∧ v≠v' then 2 else 0)" .
      thus ?thesis .
    qed         
  moreover have "odd (degree x1 (rem_unPath xs G)) ⟹ 
                    even(degree x3 (rem_unPath xs G)) ⟹ ?case"             
    proof -
      assume parity_x1_x3: "odd (degree x1 (rem_unPath xs G))" 
                           "even (degree x3 (rem_unPath xs G))"
      have "num_of_odd_nodes (rem_unPath (x#xs) G)= num_of_odd_nodes 
         (del_unEdge x1 x2 x3 (rem_unPath xs G))"
        by (metis rem_unPath.simps(2) rem_unPath_com x)
      also have "... =num_of_odd_nodes (rem_unPath xs G)" 
        using  parity_x1_x3  fin_nodes fin_edges valid_rem_xs x_in 
        by (metis del_UnEdge_odd_even)
      also have "...=num_of_odd_nodes G+(if even(degree x3 G) ∧ x3≠v' then 2 else 0 )"
        using  Cons.hyps Cons.prems(3) assms(1) assms(2) parity_assms x
        by auto
      also have "...=num_of_odd_nodes G" 
        proof -
          have "even(degree x3 G) ∧ x3≠v' ⟷ odd (degree x3 (rem_unPath xs G))" 
            using Cons.prems assms
            by (metis  is_trail.simps(2) parity_x1_x3(2) rem_UnPath_parity_v x)
          thus ?thesis using parity_x1_x3(2) by auto
        qed
      also have "...=num_of_odd_nodes G+(if even(degree v G) ∧ v≠v' then 2 else 0)" 
        proof (cases "v≠v'")
          case True
          have "x1≠x3" by (metis valid_rem_xs valid_unMultigraph.no_id x_in)
          moreover have "is_trail x3 xs v' " 
            by (metis Cons.prems(3) is_trail.simps(2) x)
          ultimately have  "odd (degree x1 (rem_unPath xs G)) 
                          ⟷ odd(degree x1 G)"  
            using True parity_x1_x3(1) rem_UnPath_parity_others x Cons.prems(3) assms(1) assms(2)
            by auto
          hence "odd(degree x1 G)" by (metis parity_x1_x3(1))
          thus ?thesis 
            by (metis (mono_tags) Cons.prems(3) Nat.add_0_right is_trail.simps(2) x)
        next
          case False
          then show ?thesis by auto
        qed    
      finally have "num_of_odd_nodes (rem_unPath (x#xs) G)=
                        num_of_odd_nodes G+(if even(degree v G) ∧ v≠v' then 2 else 0)" .
      thus ?thesis .
    qed         
  moreover have "odd (degree x1 (rem_unPath xs G)) ⟹ 
                    odd(degree x3 (rem_unPath xs G)) ⟹ ?case" 
    proof -
      assume parity_x1_x3: "odd (degree x1 (rem_unPath xs G))" 
                           "odd (degree x3 (rem_unPath xs G))"
      have "num_of_odd_nodes (rem_unPath (x#xs) G)= num_of_odd_nodes 
         (del_unEdge x1 x2 x3 (rem_unPath xs G))"
        by (metis rem_unPath.simps(2) rem_unPath_com x)
      also have "... =num_of_odd_nodes (rem_unPath xs G)-(2::nat)" 
        using del_UnEdge_odd_odd
        by (metis add_implies_diff  fin_edges fin_nodes parity_x1_x3 valid_rem_xs x_in)  
      also have "...=num_of_odd_nodes G+(if even(degree x3 G) ∧ x3≠v' then 2 else 0 )-(2::nat)"
        using Cons assms 
        by (metis is_trail.simps(2) x)
      also have "...=num_of_odd_nodes G" 
        proof -
          have "even(degree x3 G) ∧ x3≠v' ⟷ odd (degree x3 (rem_unPath xs G))" 
            using Cons.prems assms
            by (metis  is_trail.simps(2) parity_x1_x3(2) rem_UnPath_parity_v x)
          thus ?thesis using parity_x1_x3(2) by auto
        qed
      also have "...=num_of_odd_nodes G+(if even(degree v G) ∧ v≠v' then 2 else 0)" 
         proof (cases "v≠v'")
          case True
          have "x1≠x3" by (metis valid_rem_xs valid_unMultigraph.no_id x_in)
          moreover have "is_trail x3 xs v' " 
            by (metis Cons.prems(3) is_trail.simps(2) x)
          ultimately have  "odd (degree x1 (rem_unPath xs G)) 
                          ⟷ odd(degree x1 G)"  
            using True Cons.prems(3) assms(1) assms(2) parity_x1_x3(1) rem_UnPath_parity_others x 
            by auto
          hence "odd(degree x1 G)" by (metis parity_x1_x3(1))
          thus ?thesis 
            by (metis (mono_tags) Cons.prems(3) Nat.add_0_right is_trail.simps(2) x)
        next
          case False
          thus ?thesis by (metis (mono_tags) add_0_iff)
        qed    
      finally have "num_of_odd_nodes (rem_unPath (x#xs) G)=
                        num_of_odd_nodes G+(if even(degree v G) ∧ v≠v' then 2 else 0)" .
      thus ?thesis .
    qed       
  ultimately show ?case by metis
qed 

lemma (in valid_unMultigraph) rem_UnPath_odd:
  assumes "finite E" "finite V" "is_trail v ps v'" 
  assumes parity_assms:  "odd (degree v' G)"
  shows "num_of_odd_nodes (rem_unPath ps G) = num_of_odd_nodes G 
          + (if odd (degree v G)∧ v≠v' then -2 else 0)" using assms
proof (induct ps arbitrary:v)
  case Nil 
  thus ?case by auto
next
  case (Cons x xs)
  obtain x1 x2 x3 where x:"x=(x1,x2,x3)" by (metis prod_cases3) 
  have fin_nodes: "finite (nodes (rem_unPath xs G))" using Cons by auto
  have fin_edges: "finite (edges (rem_unPath xs G))" using Cons by auto
  have valid_rem_xs: "valid_unMultigraph (rem_unPath xs G)" using valid_unMultigraph_axioms 
    by auto
  have x_in:"(x1,x2,x3)∈edges (rem_unPath xs G)" 
    by (metis (full_types) Cons.prems(3) distinct_elim is_trail.simps(2) x)
  have "even (degree x1 (rem_unPath xs G)) 
        ⟹ even(degree x3 (rem_unPath xs G)) ⟹ ?case" 
    proof -
      assume parity_x1_x3: "even (degree x1 (rem_unPath xs G))" 
                           "even (degree x3 (rem_unPath xs G))"
      have "num_of_odd_nodes (rem_unPath (x#xs) G)= num_of_odd_nodes 
         (del_unEdge x1 x2 x3 (rem_unPath xs G))"
        by (metis rem_unPath.simps(2) rem_unPath_com x)
      also have "... =num_of_odd_nodes (rem_unPath xs G)+2" 
        using  parity_x1_x3  fin_nodes fin_edges valid_rem_xs x_in del_UnEdge_even_even 
        by metis
      also have "...=num_of_odd_nodes G+(if odd(degree x3 G) ∧ x3≠v' then - 2 else 0 )+2"
        using Cons.hyps[OF ‹finite E› ‹finite V›,of x3] ‹is_trail v (x # xs) v'›
          ‹odd (degree v' G)› x
        by auto
      also have "...=num_of_odd_nodes G" 
        proof -
          have "odd (degree x3 G) ∧ x3≠v' ⟷ even (degree x3 (rem_unPath xs G))" 
            using Cons.prems assms
            by (metis  is_trail.simps(2) parity_x1_x3(2) rem_UnPath_parity_v x)
          thus ?thesis using parity_x1_x3(2) by auto
        qed
      also have "...=num_of_odd_nodes G+(if odd(degree v G) ∧ v≠v' then -2 else 0)" 
         proof (cases "v≠v'")
          case True
          have "x1≠x3" by (metis valid_rem_xs valid_unMultigraph.no_id x_in)
          moreover have "is_trail x3 xs v' " 
            by (metis Cons.prems(3) is_trail.simps(2) x)
          ultimately have  "even (degree x1 (rem_unPath xs G)) 
                          ⟷ even (degree x1 G)"  
            using True Cons.prems(3) assms(1) assms(2) parity_x1_x3(1) 
                rem_UnPath_parity_others x
            by auto
          hence "even (degree x1 G)" by (metis parity_x1_x3(1))
          thus ?thesis 
            by (metis (opaque_lifting, mono_tags) Cons.prems(3)  is_trail.simps(2)  
                monoid_add_class.add.right_neutral x)
        next
          case False
          then show ?thesis by auto
        qed    
      finally have "num_of_odd_nodes (rem_unPath (x#xs) G)=
                        num_of_odd_nodes G+(if odd(degree v G) ∧ v≠v' then -2 else 0)" .
      thus ?thesis .
    qed       
  moreover have "even (degree x1 (rem_unPath xs G)) ⟹ 
                    odd(degree x3 (rem_unPath xs G)) ⟹ ?case" 
    proof -
      assume parity_x1_x3: "even (degree x1 (rem_unPath xs G))" 
                           "odd (degree x3 (rem_unPath xs G))"
      have "num_of_odd_nodes (rem_unPath (x#xs) G)= num_of_odd_nodes 
         (del_unEdge x1 x2 x3 (rem_unPath xs G))"
        by (metis rem_unPath.simps(2) rem_unPath_com x)
      also have "... =num_of_odd_nodes (rem_unPath xs G)" 
        using  parity_x1_x3  fin_nodes fin_edges valid_rem_xs x_in 
        by (metis del_UnEdge_even_odd)
      also have "...=num_of_odd_nodes G+(if odd(degree x3 G) ∧ x3≠v' then - 2 else 0 )"
        using  Cons.hyps[OF ‹finite E› ‹finite V›, of x3] Cons.prems(3) assms(1) assms(2) 
          parity_assms x
        by auto
      also have "...=num_of_odd_nodes G" 
         proof -
          have "odd(degree x3 G) ∧ x3≠v' ⟷ even (degree x3 (rem_unPath xs G))" 
            using Cons.prems assms
            by (metis  is_trail.simps(2) parity_x1_x3(2) rem_UnPath_parity_v x)
          thus ?thesis using parity_x1_x3(2) by auto
        qed
      also have "...= num_of_odd_nodes G+(if odd(degree v G) ∧ v≠v' then -2 else 0)"
         proof (cases "v≠v'")
          case True
          have "x1≠x3" by (metis valid_rem_xs valid_unMultigraph.no_id x_in)
          moreover have "is_trail x3 xs v' " 
            by (metis Cons.prems(3) is_trail.simps(2) x)
          ultimately have  "even (degree x1 (rem_unPath xs G)) 
                          ⟷ even (degree x1 G)"  
            using True Cons.prems(3) assms(1) assms(2) parity_x1_x3(1) 
                rem_UnPath_parity_others x
            by auto
          hence "even (degree x1 G)" by (metis parity_x1_x3(1))
          with Cons.prems(3) x show ?thesis by auto
        next
          case False
          then show ?thesis by auto
        qed   
      finally have "num_of_odd_nodes (rem_unPath (x#xs) G)=
                        num_of_odd_nodes G+(if odd(degree v G) ∧ v≠v' then -2 else 0)" .
      thus ?thesis .
    qed         
  moreover have "odd (degree x1 (rem_unPath xs G)) ⟹ 
                    even(degree x3 (rem_unPath xs G)) ⟹ ?case"             
    proof -
      assume parity_x1_x3: "odd (degree x1 (rem_unPath xs G))" 
                           "even (degree x3 (rem_unPath xs G))"
      have "num_of_odd_nodes (rem_unPath (x#xs) G)= num_of_odd_nodes 
         (del_unEdge x1 x2 x3 (rem_unPath xs G))"
        by (metis rem_unPath.simps(2) rem_unPath_com x)
      also have "... =num_of_odd_nodes (rem_unPath xs G)" 
        using  parity_x1_x3  fin_nodes fin_edges valid_rem_xs x_in 
        by (metis del_UnEdge_odd_even)
      also have "...=num_of_odd_nodes G+(if odd(degree x3 G) ∧ x3≠v' then -2 else 0 )"
        using  Cons.hyps Cons.prems(3) assms(1) assms(2) parity_assms x
        by auto
      also have "...=num_of_odd_nodes G + (- 2)" 
        proof -
          have "odd(degree x3 G) ∧ x3≠v' ⟷ even (degree x3 (rem_unPath xs G))" 
            using Cons.prems assms
            by (metis  is_trail.simps(2) parity_x1_x3(2) rem_UnPath_parity_v x)
          hence "odd(degree x3 G) ∧ x3≠v'" by (metis parity_x1_x3(2))
          thus ?thesis by auto
        qed
      also have "...=num_of_odd_nodes G+(if odd(degree v G) ∧ v≠v' then -2 else 0)" 
         proof -
          have "x1≠x3" by (metis valid_rem_xs valid_unMultigraph.no_id x_in)
          moreover hence "x1≠v'" 
            using Cons assms  
            by (metis is_trail.simps(2)  parity_x1_x3(1) rem_UnPath_parity_v' x)
          ultimately have "x1∉{x3,v'}" by auto
          hence  "odd(degree x1 G)" 
            using Cons.prems(3) assms(1) assms(2) parity_x1_x3(1) 
            by (metis (full_types)  is_trail.simps(2) rem_UnPath_parity_others x)
          hence "odd(degree x1 G) ∧ x1≠v'" using ‹x1 ≠ v'› by auto
          hence "odd(degree v G) ∧ v≠v'" by (metis Cons.prems(3) is_trail.simps(2) x)
          thus ?thesis by auto
        qed
      finally have "num_of_odd_nodes (rem_unPath (x#xs) G)=
                        num_of_odd_nodes G+(if odd(degree v G) ∧ v≠v' then -2 else 0)" .
      thus ?thesis .
    qed         
  moreover have "odd (degree x1 (rem_unPath xs G)) ⟹ 
                    odd(degree x3 (rem_unPath xs G)) ⟹ ?case" 
    proof -
      assume parity_x1_x3: "odd (degree x1 (rem_unPath xs G))" 
                           "odd (degree x3 (rem_unPath xs G))"
      have "num_of_odd_nodes (rem_unPath (x#xs) G)= num_of_odd_nodes 
         (del_unEdge x1 x2 x3 (rem_unPath xs G))"
        by (metis rem_unPath.simps(2) rem_unPath_com x)
      also have "... =num_of_odd_nodes (rem_unPath xs G)-(2::nat)" 
        using del_UnEdge_odd_odd
        by (metis add_implies_diff  fin_edges fin_nodes parity_x1_x3 valid_rem_xs x_in)  
      also have "...=num_of_odd_nodes G -(2::nat)"
        proof -
          have "odd(degree x3 G) ∧ x3≠v' ⟷ even (degree x3 (rem_unPath xs G))" 
            using Cons.prems assms
            by (metis  is_trail.simps(2) parity_x1_x3(2) rem_UnPath_parity_v x)
          hence "¬(odd(degree x3 G) ∧ x3≠v')" by (metis parity_x1_x3(2))  
          have "num_of_odd_nodes (rem_unPath xs G)= 
                  num_of_odd_nodes G+(if odd(degree x3 G) ∧ x3≠v' then -2 else 0)" 
            by (metis Cons.hyps Cons.prems(3) assms(1) assms(2) 
                is_trail.simps(2) parity_assms x)
          thus ?thesis 
            using ‹¬ (odd (degree x3 G) ∧ x3 ≠ v')› by auto 
        qed
      also have "...=num_of_odd_nodes G+(if odd(degree v G) ∧ v≠v' then -2 else 0)" 
        proof -
          have "x1≠x3" by (metis valid_rem_xs valid_unMultigraph.no_id x_in)
          moreover hence "x1≠v'" 
            using Cons assms  
            by (metis is_trail.simps(2)  parity_x1_x3(1) rem_UnPath_parity_v' x)
          ultimately have "x1∉{x3,v'}" by auto
          hence  "odd(degree x1 G)" 
            using Cons.prems(3) assms(1) assms(2) parity_x1_x3(1) 
            by (metis (full_types)  is_trail.simps(2) rem_UnPath_parity_others x)
          hence "odd(degree x1 G) ∧ x1≠v'" using ‹x1 ≠ v'› by auto
          hence "odd(degree v G) ∧ v≠v'" by (metis Cons.prems(3) is_trail.simps(2) x)
          hence "v∈odd_nodes_set G" 
            using Cons.prems(3) E_validD(1)  x unfolding odd_nodes_set_def
            by auto
          moreover have "v'∈odd_nodes_set G" 
            using  is_path_memb[OF is_trail_intro[OF assms(3)]]  parity_assms
            unfolding odd_nodes_set_def 
            by auto
          ultimately have "{v,v'}⊆odd_nodes_set G" by auto
          moreover have "v≠v'" by (metis ‹odd (degree v G) ∧ v ≠ v'›)
          hence "card{v,v'}=2" by auto 
          moreover have "finite(odd_nodes_set G)" 
            using ‹finite V› unfolding odd_nodes_set_def
            by auto
          ultimately have "num_of_odd_nodes G≥2" by (metis card_mono num_of_odd_nodes_def)  
          thus ?thesis using ‹odd (degree v G) ∧ v ≠ v'› by auto
        qed
      finally have "num_of_odd_nodes (rem_unPath (x#xs) G)=
                        num_of_odd_nodes G+(if odd(degree v G) ∧ v≠v' then -2 else 0)" .
      thus ?thesis .
    qed       
  ultimately show ?case by metis
qed 

lemma (in valid_unMultigraph) rem_UnPath_cycle:
  assumes "finite E" "finite V" "is_trail v ps v'" "v=v'"
  shows "num_of_odd_nodes (rem_unPath ps G) = num_of_odd_nodes G" (is "?L=?R")
proof  (cases "even(degree v' G)")
  case True
  hence "?L = num_of_odd_nodes G + (if even (degree v G)∧ v≠v' then 2 else 0)" 
    by (metis assms(1) assms(2) assms(3) rem_UnPath_even)
  with assms show ?thesis by auto  
next
  case False
  hence "?L = num_of_odd_nodes G + (if odd (degree v G)∧ v≠v' then -2 else 0)" 
    by (metis assms(1) assms(2) assms(3) rem_UnPath_odd)
  thus ?thesis using ‹v = v'› by auto   
qed



section‹Connectivity›

definition (in valid_unMultigraph) connected::bool where
  "connected ≡ ∀ v∈V. ∀v'∈V. v≠v' ⟶ (∃ps. is_path v ps v')"

lemma (in valid_unMultigraph) "connected ⟹ ∀v∈V. ∀v'∈V. v≠v'⟶(∃ps. is_trail v ps v')"
proof (rule,rule,rule)
  fix v v'
  assume "v∈V" "v'∈V" "v≠v'"
  assume connected
  obtain ps where "is_path v ps v'" by (metis ‹connected› ‹v ∈ V› ‹v' ∈ V› ‹v≠v'›  connected_def)
  then obtain ps' where "is_trail v ps' v'"
    proof (induct ps arbitrary:v )
      case Nil
      thus ?case by (metis is_trail.simps(1) is_path.simps(1))
    next
      case (Cons x xs)
      obtain x1 x2 x3 where x:"x=(x1,x2,x3)" by (metis prod_cases3)
      have "is_path x3 xs v'" by (metis Cons.prems(2) is_path.simps(2) x)
      moreover have "⋀ps'. is_trail x3 ps' v' ⟹ thesis" 
        proof -
          fix ps'
          assume "is_trail x3 ps' v'"
          hence "(x1,x2,x3)∉set ps' ∧ (x3,x2,x1)∉set ps' ⟹is_trail v (x#ps') v'"
            by (metis Cons.prems(2) is_trail.simps(2) is_path.simps(2) x)
          moreover have "(x1,x2,x3)∈set ps' ⟹ ∃ps1. is_trail v ps1 v'" 
            proof -
              assume "(x1,x2,x3)∈set ps'"
              then obtain ps1 ps2 where "ps'=ps1@(x1,x2,x3)#ps2" by (metis split_list)
              hence "is_trail v (x#ps2) v'" 
                using ‹is_trail x3 ps' v'› x
                by (metis Cons.prems(2) is_trail.simps(2) 
                    is_trail_split is_path.simps(2))
              thus ?thesis by rule
            qed
          moreover have "(x3,x2,x1)∈set ps' ⟹  ∃ps1. is_trail v ps1 v'" 
             proof -
              assume "(x3,x2,x1)∈set ps'"
              then obtain ps1 ps2 where "ps'=ps1@(x3,x2,x1)#ps2" by (metis split_list)
              hence "is_trail v ps2 v'" 
                using ‹is_trail x3 ps' v'› x
                by (metis Cons.prems(2) is_trail.simps(2) 
                    is_trail_split is_path.simps(2))
              thus ?thesis by rule 
            qed
          ultimately show thesis using Cons by auto
        qed
      ultimately show ?case using Cons by auto
    qed
  thus "∃ps. is_trail v ps v'" by rule
qed

lemma (in valid_unMultigraph) no_rep_length: "is_trail v ps v'⟹length ps=card(set ps)" 
  by (induct ps arbitrary:v, auto)

lemma (in valid_unMultigraph) path_in_edges:"is_trail v ps v' ⟹ set ps ⊆ E" 
proof (induct ps arbitrary:v)
  case Nil
  show ?case by auto
next
  case (Cons x xs)
  obtain x1 x2 x3 where x:"x=(x1,x2,x3)" by (metis prod_cases3)
  hence "is_trail x3 xs v'" using Cons by auto
  hence " set xs ⊆ E" using Cons by auto
  moreover have "x∈E" using Cons by (metis is_trail_intro is_path.simps(2) x)
  ultimately show ?case by auto
qed


lemma (in valid_unMultigraph) trail_bound: 
    assumes "finite E" " is_trail v ps v'"
    shows "length ps ≤card E" 
by (metis (opaque_lifting, no_types) assms(1) assms(2) card_mono no_rep_length path_in_edges)

definition (in valid_unMultigraph) exist_path_length:: "'v ⇒ nat ⇒bool" where
  "exist_path_length v l≡∃v' ps. is_trail v' ps v ∧ length ps=l"   

lemma (in valid_unMultigraph) longest_path:
  assumes "finite E" "n ∈ V"
  shows "∃v. ∃max_path. is_trail v max_path n ∧ 
        (∀v'. ∀e∈E. ¬is_trail v' (e#max_path) n)"
proof (rule ccontr)
  assume  contro:"¬ (∃v max_path. is_trail v max_path n 
           ∧ (∀v'. ∀e∈E. ¬is_trail v' (e#max_path) n))"
  hence  induct:"(∀v max_path.  is_trail v max_path n 
           ⟶ (∃v'. ∃e∈E. is_trail v' (e#max_path) n))" by auto
  have "is_trail n [] n" using ‹n ∈ V› by auto 
  hence "exist_path_length n 0" unfolding exist_path_length_def by auto
  moreover have "∀y. exist_path_length n y ⟶ y ≤ card E" 
    using trail_bound[OF ‹finite E›] unfolding exist_path_length_def 
    by auto
  hence bound:"∀y. exist_path_length n y ⟶ y ≤ card E" by auto
  ultimately have "exist_path_length n (GREATEST x. exist_path_length n x)"
    using GreatestI_nat by auto
  then obtain v max_path where 
    max_path:"is_trail v max_path n" "length max_path=(GREATEST x. exist_path_length n x)"
    by (metis exist_path_length_def)
  hence "∃ v' e. is_trail v' (e#max_path) n" using induct by metis
  hence "exist_path_length n (length max_path +1)" 
    by (metis One_nat_def exist_path_length_def list.size(4))
  hence "length max_path + 1 ≤ (GREATEST x. exist_path_length n x)"
   by (metis Greatest_le_nat bound)
  hence "length max_path + 1 ≤ length max_path" using max_path by auto
  thus False by auto
qed


lemma even_card':
  assumes "even(card A)" "x∈A"
  shows "∃y∈A. y≠x" 
proof (rule ccontr)
  assume "¬ (∃y∈A. y ≠ x)"
  hence "∀y∈A. y=x" by auto
  hence "A={x}" by (metis all_not_in_conv assms(2) insertI2 mk_disjoint_insert)
  hence "card(A)=1" by auto
  thus False using ‹even(card A)› by auto
qed

lemma odd_card: 
  assumes "finite A" "odd(card A)"
  shows "∃x. x∈A" 
by (metis all_not_in_conv assms(2) card.empty even_zero) 

lemma (in valid_unMultigraph) extend_distinct_path: 
  assumes "finite E"  "is_trail v' ps v" 
  assumes parity_assms:"(even (degree v' G)∧v'≠v)∨(odd (degree v' G)∧v'=v)"
  shows "∃e v1. is_trail v1 (e#ps) v" 
proof -
  have "(even (degree v' G)∧v'≠v) ⟹ odd(degree v' (rem_unPath  ps G))" 
    by (metis assms(1) assms(2) rem_UnPath_parity_v)
  moreover have "(odd (degree v' G)∧v'=v) ⟹ odd(degree v' (rem_unPath  ps G))" 
    by (metis assms(1) assms(2) rem_UnPath_parity_v')
  ultimately have "odd(degree v' (rem_unPath  ps G))" using parity_assms by auto
  hence "odd (card {e. fst e=v' ∧ e∈edges G - (set ps ∪ set (rev_path ps))})" 
    using  rem_unPath_edges unfolding degree_def 
    by (metis (lifting, no_types) Collect_cong)
  hence "{e. fst e=v' ∧ e∈E - (set ps ∪ set (rev_path ps))}≠{}" 
    by (metis empty_iff finite.emptyI odd_card)
  then obtain v0 w where v0w:  "(v',w,v0)∈E" "(v',w,v0)∉set ps ∪ set (rev_path ps)" by auto
  hence "is_trail v0 ((v0,w,v')#ps) v" 
    by (metis (opaque_lifting, mono_tags) Un_iff assms(2) corres in_set_rev_path is_trail.simps(2))  
  thus ?thesis by metis
qed

text‹replace an edge (or its reverse in a path) by another path (in an undirected graph)›
fun replace_by_UnPath:: "('v,'w) path ⇒ 'v ×'w ×'v ⇒ ('v,'w) path ⇒  ('v,'w) path" where
  "replace_by_UnPath [] _ _ = []" |
  "replace_by_UnPath (x#xs) (v,e,v') ps = 
    (if x=(v,e,v') then ps@replace_by_UnPath xs (v,e,v') ps
     else if x=(v',e,v) then (rev_path ps)@replace_by_UnPath xs (v,e,v') ps
     else x#replace_by_UnPath xs (v,e,v') ps)"

lemma (in valid_unMultigraph) del_unEdge_connectivity:
  assumes "connected" "∃ps. valid_graph.is_path (del_unEdge v e v' G) v ps v'"
  shows "valid_unMultigraph.connected (del_unEdge v e v' G)"
proof -
  have valid_unMulti:"valid_unMultigraph (del_unEdge v e v' G)" 
    using valid_unMultigraph_axioms by simp
  have valid_graph: "valid_graph (del_unEdge v e v' G)" 
    using valid_graph_axioms del_undirected by (metis delete_edge_valid)
  obtain ex_path where ex_path:"valid_graph.is_path (del_unEdge v e v' G) v ex_path v'" 
    by (metis assms(2))
  show ?thesis unfolding valid_unMultigraph.connected_def[OF valid_unMulti]
  proof (rule,rule,rule)
    fix n n' 
    assume  n : "n ∈nodes (del_unEdge v e v' G)" 
    assume  n': "n'∈nodes (del_unEdge v e v' G)"
    assume "n≠n'"
    obtain ps where ps:"is_path n ps n'" 
      by (metis ‹n≠n'› n n' ‹connected› connected_def del_UnEdge_node)
    hence "valid_graph.is_path (del_unEdge v e v' G) 
           n (replace_by_UnPath ps (v,e,v') ex_path) n'" 
      proof (induct ps arbitrary:n)
        case Nil
        thus ?case by (metis is_path.simps(1) n' replace_by_UnPath.simps(1) valid_graph 
          valid_graph.is_path_simps(1))
      next
        case (Cons x xs)
        obtain x1 x2 x3 where x:"x=(x1,x2,x3)" by (metis prod_cases3)
        have "x=(v,e,v') ⟹ ?case" 
          proof -
            assume "x=(v,e,v')"
            hence "valid_graph.is_path (del_unEdge v e v' G) 
                n (replace_by_UnPath (x#xs) (v,e,v') ex_path) n'
                = valid_graph.is_path (del_unEdge v e v' G) 
                n (ex_path@(replace_by_UnPath xs (v,e,v') ex_path)) n'" 
              by (metis replace_by_UnPath.simps(2))
            also have "...=True" 
              by (metis Cons.hyps Cons.prems ‹x = (v, e, v')› ex_path is_path.simps(2) valid_graph 
                  valid_graph.is_path_split)
            finally show ?thesis by simp
          qed
        moreover have "x=(v',e,v) ⟹ ?case" 
          proof -
            assume "x=(v',e,v)"
            hence "valid_graph.is_path (del_unEdge v e v' G) 
                n (replace_by_UnPath (x#xs) (v,e,v') ex_path) n'
                = valid_graph.is_path (del_unEdge v e v' G) 
                n ((rev_path ex_path)@(replace_by_UnPath xs (v,e,v') ex_path)) n'" 
              by (metis Cons.prems is_path.simps(2) no_id replace_by_UnPath.simps(2))
            also have "...=True" 
              by (metis Cons.hyps Cons.prems ‹x = (v', e, v)› is_path.simps(2) ex_path valid_graph 
                  valid_graph.is_path_split valid_unMulti valid_unMultigraph.is_path_rev)
            finally show ?thesis by simp
          qed
        moreover have "x≠(v,e,v')∧x≠(v',e,v)⟹?case" 
          by (metis Cons.hyps Cons.prems del_UnEdge_frame is_path.simps(2) replace_by_UnPath.simps(2) 
              valid_graph valid_graph.is_path.simps(2) x)
        ultimately show ?case by auto
      qed
    thus "∃ps. valid_graph.is_path (del_unEdge v e v' G) n ps n'" by auto
  qed
qed

lemma (in valid_unMultigraph) path_between_odds:
  assumes "odd(degree v G)" "odd(degree v' G)" "finite E"  "v≠v'" "num_of_odd_nodes G=2"
  shows "∃ps. is_trail v ps v'"
proof -
   have "v∈V" 
    proof (rule ccontr)
      assume "v∉V"
      hence "∀e ∈ E. fst e ≠ v" by (metis E_valid(1) imageI subsetD)
      hence "degree v G=0" unfolding degree_def using ‹finite E› 
        by force
      thus False using ‹odd(degree v G)› by auto
    qed
  have "v'∈V" 
    proof (rule ccontr)
      assume "v'∉V"
      hence "∀e ∈ E. fst e ≠ v'" by (metis E_valid(1) imageI subsetD)
      hence "degree v' G=0" unfolding degree_def using ‹finite E› 
        by force
     thus False using ‹odd(degree v' G)› by auto
    qed
  then obtain max_path v0 where max_path:
      "is_trail  v0 max_path v'" 
      "(∀n. ∀w∈E. ¬is_trail n (w#max_path) v')" 
    using longest_path[of v'] by (metis assms(3)) 
  have "even(degree v0 G)⟹v0=v' ⟹ v0=v" 
    by (metis assms(2))
  moreover have "even(degree v0 G)⟹v0≠v' ⟹ v0=v" 
    proof -
      assume"even(degree v0 G)" "v0≠v'"
      hence "∃w v1. is_trail 
            v1 (w#max_path) v'" 
        by (metis assms(3) extend_distinct_path max_path(1))
      thus ?thesis by (metis (full_types) is_trail.simps(2) max_path(2) prod.exhaust)
    qed
  moreover have "odd(degree v0 G)⟹v0=v'⟹v0=v" 
    proof -
      assume"odd(degree v0 G)" "v0=v'"
      hence "∃w v1. is_trail v1 (w#max_path) v'" 
        by (metis assms(3) extend_distinct_path max_path(1))
      thus ?thesis by (metis (full_types) List.set_simps(2) insert_subset max_path(2) path_in_edges)
    qed
  moreover have "odd(degree v0 G)⟹v0≠v'⟹v0=v"
    proof (rule ccontr)
      assume "v0 ≠ v" "odd(degree v0 G)" "v0≠v'"
      moreover have "v∈odd_nodes_set G" 
        using ‹v ∈ V› ‹ odd (degree v G)› unfolding odd_nodes_set_def
        by auto
      moreover have "v'∈odd_nodes_set G" 
        using ‹v' ∈ V› ‹odd (degree v' G)›
        unfolding odd_nodes_set_def
        by auto
      ultimately have "{v,v',v0} ⊆ odd_nodes_set G" 
        using   is_path_memb[OF is_trail_intro[OF ‹is_trail v0 max_path v'›]] max_path(1)
        unfolding odd_nodes_set_def
        by auto
      moreover have "card {v,v',v0}=3" using ‹v0≠v› ‹v≠v'› ‹v0≠v'› by auto
      moreover have "finite (odd_nodes_set G)" 
        using assms(5) card_eq_0_iff[of "odd_nodes_set G"] unfolding num_of_odd_nodes_def 
        by auto
      ultimately have "3≤card(odd_nodes_set G)" by (metis card_mono)
      thus False using ‹num_of_odd_nodes G=2› unfolding num_of_odd_nodes_def by auto
    qed
  ultimately have "v0=v" by auto
  thus ?thesis by (metis max_path(1))
qed

lemma (in valid_unMultigraph) del_unEdge_even_connectivity:
  assumes "finite E" "finite V" "connected" "∀n∈V. even(degree n G)" "(v,e,v')∈E"
  shows "valid_unMultigraph.connected (del_unEdge v e v' G)" 
proof -
  have valid_unMulti:"valid_unMultigraph (del_unEdge v e v' G)" 
    using valid_unMultigraph_axioms by simp
  have valid_graph: "valid_graph (del_unEdge v e v' G)" 
    using valid_graph_axioms del_undirected by (metis delete_edge_valid)
  have fin_E': "finite(edges (del_unEdge v e v' G))" 
    by (metis (opaque_lifting, no_types) assms(1) del_undirected delete_edge_def 
        finite_Diff select_convs(2))
  have fin_V': "finite(nodes (del_unEdge v e v' G))" 
    by (metis (mono_tags) assms(2) del_undirected delete_edge_def select_convs(1))
  have all_even: "∀n∈nodes (del_unEdge v e v' G). n∉{v,v'}
                  ⟶even(degree n (del_unEdge v e v' G))"
    by (metis (full_types) assms(1) assms(4) degree_frame del_UnEdge_node)
  have "even (degree v G)" by (metis (full_types) E_validD(1) assms(4) assms(5))
  moreover have "even (degree v' G)" by (metis (full_types) E_validD(2) assms(4) assms(5))
  moreover have "num_of_odd_nodes G = 0" 
    using ‹∀n∈V. even(degree n G)› ‹finite V›
    unfolding num_of_odd_nodes_def odd_nodes_set_def by auto
  ultimately have "num_of_odd_nodes (del_unEdge v e v' G) = 2" 
    using del_UnEdge_even_even[of G v e v',OF valid_unMultigraph_axioms] 
    by (metis assms(1) assms(2) assms(5) monoid_add_class.add.left_neutral)
  moreover have " odd (degree v (del_unEdge v e v' G))" 
    using ‹even (degree v G)› del_UnEdge_even[OF ‹(v,e,v')∈E› ‹finite E›] 
    unfolding odd_nodes_set_def 
    by auto
  moreover have "odd (degree v' (del_unEdge v e v' G))" 
    using ‹even (degree v' G)› del_UnEdge_even'[OF ‹(v,e,v')∈E› ‹finite E›] 
    unfolding odd_nodes_set_def 
    by auto  
  moreover have "finite (edges (del_unEdge v e v' G))" 
    using ‹finite E› by auto
  moreover have "v≠v'" using no_id ‹(v,e,v')∈E› by auto
  ultimately have "∃ps. valid_unMultigraph.is_trail (del_unEdge v e v' G) v ps v'"
    using valid_unMultigraph.path_between_odds[OF valid_unMulti,of v v']    
    by auto
  thus ?thesis 
    by (metis (full_types) assms(3) del_unEdge_connectivity valid_unMulti 
      valid_unMultigraph.is_trail_intro)
qed


lemma (in valid_graph) path_end:"ps≠[] ⟹ is_path v ps v' ⟹ v'=snd (snd(last ps))" 
  by (induct ps arbitrary:v,auto)

lemma (in valid_unMultigraph) connectivity_split:
  assumes "connected" "¬valid_unMultigraph.connected (del_unEdge v w v' G)" 
          "(v,w,v')∈E"
  obtains G1 G2 where
         "nodes G1={n. ∃ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}"
         and "edges G1={(n,e,n'). (n,e,n')∈edges (del_unEdge v w v' G) 
            ∧ n∈nodes G1 ∧ n'∈nodes G1}"
         and "nodes G2={n. ∃ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}"
         and "edges G2={(n,e,n'). (n,e,n')∈edges (del_unEdge v w v' G) 
            ∧ n∈nodes G2 ∧ n'∈nodes G2}" 
         and "edges G1 ∪ edges G2 = edges (del_unEdge v w v' G)" 
         and "edges G1 ∩ edges G2={}" 
         and "nodes G1 ∪ nodes G2=nodes (del_unEdge v 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"
proof -
  have valid0:"valid_graph (del_unEdge v w v' G)" using valid_graph_axioms 
    by (metis del_undirected delete_edge_valid)
  have valid0':"valid_unMultigraph (del_unEdge v w v' G)" using valid_unMultigraph_axioms 
    by (metis del_unEdge_valid)
  obtain G1_nodes where G1_nodes:"G1_nodes= 
      {n. ∃ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}" 
    by metis
  then obtain G1 where G1:"G1=
      ⦇nodes=G1_nodes, edges={(n,e,n'). (n,e,n')∈edges (del_unEdge v w v' G) 
      ∧ n∈G1_nodes ∧ n'∈G1_nodes}⦈"
    by metis
  obtain G2_nodes where G2_nodes:"G2_nodes= 
      {n. ∃ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}" 
    by metis
  then obtain G2 where G2:"G2=
      ⦇nodes=G2_nodes, edges={(n,e,n'). (n,e,n')∈edges (del_unEdge v w v' G) 
      ∧ n∈G2_nodes ∧ n'∈G2_nodes}⦈"
    by metis 
  have valid_G1:"valid_unMultigraph G1" 
    using G1 valid_unMultigraph.corres[OF valid0'] valid_unMultigraph.no_id[OF valid0']
    by (unfold_locales,auto)
  hence valid_G1':"valid_graph G1" using valid_unMultigraph_def by auto
  have valid_G2:"valid_unMultigraph G2"  
    using G2 valid_unMultigraph.corres[OF valid0'] valid_unMultigraph.no_id[OF valid0'] 
    by (unfold_locales,auto)
  hence valid_G2': "valid_graph G2" using valid_unMultigraph_def by auto
  have "nodes G1={n. ∃ps. valid_graph.is_path (del_unEdge v w v' G) n ps v}" 
    using G1_nodes G1 by auto
  moreover have "edges G1={(n,e,n'). (n,e,n')∈edges (del_unEdge v w v' G) 
                 ∧ n∈nodes G1 ∧ n'∈nodes G1}"
    using G1_nodes G1 by auto
  moreover have "nodes G2={n. ∃ps. valid_graph.is_path (del_unEdge v w v' G) n ps v'}"
    using G2_nodes G2 by auto
  moreover have "edges G2={(n,e,n'). (n,e,n')∈edges (del_unEdge v w v' G) 
                 ∧ n∈nodes G2 ∧ n'∈nodes G2}"
    using G2_nodes G2 by auto               
  moreover have "nodes G1 ∪ nodes G2=nodes (del_unEdge v w v' G)" 
    proof (rule ccontr)
      assume "nodes G1 ∪ nodes G2 ≠ nodes (del_unEdge v w v' G)"
      moreover have "nodes G1 ⊆ nodes (del_unEdge v w v' G)"
        using valid_graph.is_path_memb[OF valid0] G1 G1_nodes by auto
      moreover have "nodes G2 ⊆ nodes (del_unEdge v w v' G)"
        using valid_graph.is_path_memb[OF valid0] G2 G2_nodes by auto
      ultimately obtain n where n:
          "n∈nodes (del_unEdge v w v' G)" "n∉nodes G1" "n∉nodes G2"
        by auto
      hence n_neg_v : "¬(∃ps. valid_graph.is_path (del_unEdge v w v' G) n ps v)" and
            n_neg_v': "¬(∃ps. valid_graph.is_path (del_unEdge v w v' G) n ps v')"
        using G1 G1_nodes G2 G2_nodes by auto
      hence "n≠v" by (metis n(1) valid0 valid_graph.is_path_simps(1))
      then obtain nvs where nvs: "is_path n nvs v" using ‹connected› 
        by (metis E_validD(1) assms(3) connected_def del_UnEdge_node n(1))
      then obtain nvs' where nvs': "nvs'=takeWhile (λx. x≠(v,w,v')∧x≠(v',w,v)) nvs" by auto
      moreover have nvs_nvs':"nvs=nvs'@dropWhile (λx. x≠(v,w,v')∧x≠(v',w,v)) nvs" 
        using nvs' takeWhile_dropWhile_id by auto
      ultimately obtain n' where is_path_nvs': "is_path n nvs' n'"
          and "is_path n' (dropWhile (λx. x≠(v,w,v')∧x≠(v',w,v)) nvs) v"
        using nvs is_path_split[of n nvs' "dropWhile (λx. x≠(v,w,v')∧x≠(v',w,v)) nvs"] by auto
      have "n'=v ∨ n'=v'" 
        proof (cases "dropWhile (λx. x≠(v,w,v')∧x≠(v',w,v)) nvs")
          case Nil
          hence "nvs=nvs'" using nvs_nvs' by (metis append_Nil2)
          hence "n'=v" using  nvs is_path_nvs' path_end by (metis (mono_tags) is_path.simps(1))
          thus ?thesis  by auto
        next
          case (Cons x xs)
          hence "dropWhile (λx. x≠(v,w,v')∧x≠(v',w,v)) nvs≠[]" by auto
          hence "hd (dropWhile (λx. x≠(v,w,v')∧x≠(v',w,v)) nvs)=(v,w,v')
                 ∨ hd (dropWhile (λx. x≠(v,w,v')∧x≠(v',w,v)) nvs)=(v',w,v)" 
            by (metis (lifting, full_types) hd_dropWhile)
          hence "x=(v,w,v')∨x=(v',w,v)" using Cons by auto
          thus ?thesis
            using ‹is_path n' (dropWhile (λx. x ≠ (v, w, v') ∧ x ≠ (v', w, v)) nvs) v›
            by (metis Cons  is_path.simps(2))
        qed
      moreover have "valid_graph.is_path (del_unEdge v w v' G) n nvs' n'" 
        using is_path_nvs' nvs'
        proof (induct nvs' arbitrary:n nvs)
          case Nil
          thus ?case by (metis del_UnEdge_node is_path.simps(1) valid0 valid_graph.is_path_simps(1))
        next
          case (Cons x xs)
          obtain x1 x2 x3 where x:"x=(x1,x2,x3)" by (metis prod_cases3)
          hence "is_path x3 xs n'" using Cons by auto
          moreover have "xs = takeWhile (λx. x ≠ (v, w, v') ∧ x ≠ (v', w, v)) (tl nvs)" 
            using ‹x # xs = takeWhile (λx. x ≠ (v, w, v') ∧ x ≠ (v', w, v)) nvs› 
            by (metis (lifting, no_types) append_Cons list.distinct(1) takeWhile.simps(2) 
                takeWhile_dropWhile_id list.sel(3))
          ultimately have "valid_graph.is_path (del_unEdge v w v' G) x3 xs n'" 
            using Cons by auto
          moreover have "x≠(v,w,v') ∧ x≠(v',w,v)" 
            using Cons(3) set_takeWhileD[of x "(λx. x ≠ (v, w, v') ∧ x ≠ (v', w, v))" nvs] 
            by (metis List.set_simps(2) insertI1)
          hence "x∈edges (del_unEdge v w v' G)" 
            by (metis Cons.prems(1) del_UnEdge_frame is_path.simps(2) x)
          ultimately show ?case using x 
            by (metis Cons.prems(1) is_path.simps(2) valid0 valid_graph.is_path.simps(2))
        qed
      ultimately show False using n_neg_v n_neg_v' by auto
    qed
  moreover have "nodes G1 ∩ nodes G2={}" 
    proof (rule ccontr)
      assume "nodes G1 ∩ nodes G2 ≠ {}"
      then obtain n where n:"n∈nodes G1" "n∈nodes G2" by auto  
      then obtain nvs nv's where 
          nvs  : "valid_graph.is_path (del_unEdge v w v' G) n nvs v" and
          nv's : "valid_graph.is_path (del_unEdge v w v' G) n nv's v'"
        using G1 G2 G1_nodes G2_nodes by auto
      hence "valid_graph.is_path (del_unEdge v w v' G) v ((rev_path nvs)@nv's) v'"
        using valid_unMultigraph.is_path_rev[OF valid0'] valid_graph.is_path_split[OF valid0] 
        by auto 
      hence "valid_unMultigraph.connected (del_unEdge v w v' G)" 
        by (metis assms(1) del_unEdge_connectivity)
      thus False by (metis assms(2))  
    qed
  moreover have "edges G1 ∪ edges G2 = edges (del_unEdge v w v' G)" 
    proof (rule ccontr)
      assume "edges G1 ∪ edges G2 ≠ edges (del_unEdge v w v' G)"
      moreover have "edges G1 ⊆ edges (del_unEdge v w v' G)" using G1 by auto
      moreover have "edges G2 ⊆ edges (del_unEdge v w v' G)" using G2 by auto
      ultimately obtain n e n' where 
          nen':
          "(n,e,n')∈edges (del_unEdge v w v' G)" 
          "(n,e,n')∉edges G1" "(n,e,n')∉edges G2" 
        by auto
      moreover have "n∈nodes (del_unEdge v w v' G)" 
        by (metis nen'(1) valid0 valid_graph.E_validD(1))
      moreover have "n'∈nodes (del_unEdge v w v' G)" 
        by (metis nen'(1) valid0 valid_graph.E_validD(2))
      ultimately have "(n∈nodes G1 ∧ n'∈nodes G2)∨(n∈nodes G2∧n'∈nodes G1)" 
        using G1 G2 ‹nodes G1 ∪ nodes G2=nodes (del_unEdge v w v' G)› by auto
      moreover have "n∈nodes G1 ⟹ n'∈nodes G2 ⟹ False" 
        proof -
          assume "n∈nodes G1" "n'∈nodes G2"
          then obtain nvs nv's where 
              nvs  : "valid_graph.is_path (del_unEdge v w v' G) n nvs v" and
              nv's : "valid_graph.is_path (del_unEdge v w v' G) n' nv's v'"
            using G1 G2 G1_nodes G2_nodes by auto
          hence "valid_graph.is_path (del_unEdge v w v' G) v 
                  ((rev_path nvs)@(n,e,n')#nv's) v'"
            using valid_unMultigraph.is_path_rev[OF valid0'] valid_graph.is_path_split'[OF valid0]
                  ‹(n,e,n')∈edges (del_unEdge v w v' G)›
            by auto 
          hence "valid_unMultigraph.connected (del_unEdge v w v' G)" 
            by (metis assms(1) del_unEdge_connectivity)
          thus False by (metis assms(2))
        qed
      moreover have "n∈nodes G2 ⟹ n'∈nodes G1 ⟹ False" 
        proof -
          assume "n'∈nodes G1" "n∈nodes G2"
          then obtain n'vs nvs where 
              n'vs  : "valid_graph.is_path (del_unEdge v w v' G) n' n'vs v" and
              nvs : "valid_graph.is_path (del_unEdge v w v' G) n nvs v'"
            using G1 G2 G1_nodes G2_nodes by auto
          moreover have "(n',e,n)∈edges (del_unEdge v w v' G)" 
            by (metis nen'(1) valid0' valid_unMultigraph.corres)
          ultimately have "valid_graph.is_path (del_unEdge v w v' G) v 
                  ((rev_path n'vs)@(n',e,n)#nvs) v'"
            using valid_unMultigraph.is_path_rev[OF valid0'] valid_graph.is_path_split'[OF valid0]
            by auto 
          hence "valid_unMultigraph.connected (del_unEdge v w v' G)" 
            by (metis assms(1) del_unEdge_connectivity)
          thus False by (metis assms(2))
        qed
      ultimately show False by auto
    qed
  moreover have "edges G1 ∩ edges G2={}" 
    proof (rule ccontr)
      assume "edges G1 ∩ edges G2 ≠ {}"
      then obtain n e n' where "(n,e,n')∈edges G1" "(n,e,n')∈edges G2" by auto
      hence "n∈nodes G1" "n∈nodes G2" using G1 G2 by auto
      thus False using ‹nodes G1 ∩ nodes G2={}› by auto
    qed
  moreover have "valid_unMultigraph.connected G1" 
    unfolding valid_unMultigraph.connected_def[OF valid_G1]
    proof (rule,rule,rule)
      fix n n' 
      assume  n : "n ∈nodes G1" 
      assume  n': "n'∈nodes G1"
      assume "n≠n'"
      obtain ps where "valid_graph.is_path (del_unEdge v w v' G) n ps v" 
        using G1 G1_nodes n by auto
      hence ps:"valid_graph.is_path G1 n ps v" 
        proof (induct ps arbitrary:n)
          case Nil
          moreover have "v∈nodes G1" using G1 G1_nodes valid0 
            by (metis (lifting, no_types) calculation mem_Collect_eq select_convs(1) 
                valid_graph.is_path.simps(1))
          ultimately show ?case 
            by (metis valid0 valid_G1 valid_unMultigraph.is_trail.simps(1)
                 valid_graph.is_path.simps(1)  valid_unMultigraph.is_trail_intro)
        next
          case (Cons x xs)
          obtain x1 x2 x3 where x:"x=(x1,x2,x3)" by (metis prod_cases3)
          have "x1∈nodes G1" using G1 G1_nodes Cons.prems x 
            by (metis (lifting) mem_Collect_eq select_convs(1) valid0 valid_graph.is_path.simps(2))
          moreover have "(x1,x2,x3)∈edges (del_unEdge v w v' G)" 
            by (metis Cons.prems valid0 valid_graph.is_path.simps(2) x)
          ultimately have "(x1,x2,x3)∈edges G1" 
            using G1 G2 ‹nodes G1 ∩ nodes G2={}› ‹edges G1 ∪ edges G2=edges (del_unEdge v w v' G)›
            by (metis (full_types) IntI Un_iff  bex_empty   valid_G2' valid_graph.E_validD(1) )
          moreover have "valid_graph.is_path (del_unEdge v w v' G) x3 xs v" 
            by (metis Cons.prems valid0 valid_graph.is_path.simps(2) x)
          hence "valid_graph.is_path G1 x3 xs v" using Cons.hyps by auto
          moreover have "x1=n" by (metis Cons.prems valid0 valid_graph.is_path.simps(2) x)
          ultimately show ?case using x valid_G1' by (metis valid_graph.is_path.simps(2))   
        qed
      obtain ps' where "valid_graph.is_path (del_unEdge v w v' G) n' ps' v" 
        using G1 G1_nodes n' by auto
      hence ps':"valid_graph.is_path G1 n' ps' v" 
        proof (induct ps' arbitrary:n')
          case Nil
          moreover have "v∈nodes G1" using G1 G1_nodes valid0 
            by (metis (lifting, no_types) calculation mem_Collect_eq select_convs(1) 
                valid_graph.is_path.simps(1))
          ultimately show ?case 
            by (metis valid0 valid_G1 valid_unMultigraph.is_trail.simps(1)
                 valid_graph.is_path.simps(1)  valid_unMultigraph.is_trail_intro)
        next
          case (Cons x xs)
          obtain x1 x2 x3 where x:"x=(x1,x2,x3)" by (metis prod_cases3)
          have "x1∈nodes G1" using G1 G1_nodes Cons.prems x 
            by (metis (lifting) mem_Collect_eq select_convs(1) valid0 valid_graph.is_path.simps(2))
          moreover have "(x1,x2,x3)∈edges (del_unEdge v w v' G)" 
            by (metis Cons.prems valid0 valid_graph.is_path.simps(2) x)
          ultimately have "(x1,x2,x3)∈edges G1" 
            using G1 G2 ‹nodes G1 ∩ nodes G2={}› 
              ‹edges G1 ∪ edges G2=edges (del_unEdge v w v' G)›
            by (metis (full_types) IntI Un_iff  bex_empty  valid_G2' valid_graph.E_validD(1))
          moreover have "valid_graph.is_path (del_unEdge v w v' G) x3 xs v" 
            by (metis Cons.prems valid0 valid_graph.is_path.simps(2) x)
          hence "valid_graph.is_path G1 x3 xs v" using Cons.hyps by auto
          moreover have "x1=n'" by (metis Cons.prems valid0 valid_graph.is_path.simps(2) x)
          ultimately show ?case using x valid_G1' by (metis valid_graph.is_path.simps(2))   
        qed
      hence "valid_graph.is_path G1 v (rev_path ps') n'" 
        using valid_unMultigraph.is_path_rev[OF valid_G1]
        by auto
      hence "valid_graph.is_path G1 n (ps@(rev_path ps')) n'" 
        using ps valid_graph.is_path_split[OF valid_G1',of n ps "rev_path ps'" n']
        by auto
      thus "∃ps. valid_graph.is_path G1 n ps n'" by auto
    qed
  moreover have "valid_unMultigraph.connected G2" 
    unfolding valid_unMultigraph.connected_def[OF valid_G2]
    proof (rule,rule,rule)
      fix n n' 
      assume  n : "n ∈nodes G2" 
      assume  n': "n'∈nodes G2"
      assume "n≠n'"
      obtain ps where "valid_graph.is_path (del_unEdge v w v' G) n ps v'" 
        using G2 G2_nodes n by auto
      hence ps:"valid_graph.is_path G2 n ps v'" 
        proof (induct ps arbitrary:n)
          case Nil
          moreover have "v'∈nodes G2" using G2 G2_nodes valid0 
            by (metis (lifting, no_types) calculation mem_Collect_eq select_convs(1) 
                valid_graph.is_path.simps(1))
          ultimately show ?case 
            by (metis valid0 valid_G2 valid_unMultigraph.is_trail.simps(1)
                 valid_graph.is_path.simps(1)  valid_unMultigraph.is_trail_intro)
        next
          case (Cons x xs)
          obtain x1 x2 x3 where x:"x=(x1,x2,x3)" by (metis prod_cases3)
          have "x1∈nodes G2" using G2 G2_nodes Cons.prems x 
            by (metis (lifting) mem_Collect_eq select_convs(1) valid0 valid_graph.is_path.simps(2))
          moreover have "(x1,x2,x3)∈edges (del_unEdge v w v' G)" 
            by (metis Cons.prems valid0 valid_graph.is_path.simps(2) x)
          ultimately have "(x1,x2,x3)∈edges G2" 
            using ‹nodes G1 ∩ nodes G2={}› ‹edges G1 ∪ edges G2=edges (del_unEdge v w v' G)›
            by (metis IntI Un_iff assms(1) bex_empty connected_def del_UnEdge_node valid0 valid0'
              valid_G1' valid_graph.E_validD(1) valid_graph.E_validD(2) valid_unMultigraph.no_id)
          moreover have "valid_graph.is_path (del_unEdge v w v' G) x3 xs v'" 
            by (metis Cons.prems valid0 valid_graph.is_path.simps(2) x)
          hence "valid_graph.is_path G2 x3 xs v'" using Cons.hyps by auto
          moreover have "x1=n" by (metis Cons.prems valid0 valid_graph.is_path.simps(2) x)
          ultimately show ?case using x valid_G2' by (metis valid_graph.is_path.simps(2))   
        qed
      obtain ps' where "valid_graph.is_path (del_unEdge v w v' G) n' ps' v'" 
        using G2 G2_nodes n' by auto
      hence ps':"valid_graph.is_path G2 n' ps' v'" 
        proof (induct ps' arbitrary:n')
          case Nil
          moreover have "v'∈nodes G2" using G2 G2_nodes valid0 
            by (metis (lifting, no_types) calculation mem_Collect_eq select_convs(1) 
                valid_graph.is_path.simps(1))
          ultimately show ?case 
            by (metis valid0 valid_G2 valid_unMultigraph.is_trail.simps(1)
                 valid_graph.is_path.simps(1)  valid_unMultigraph.is_trail_intro)
        next
          case (Cons x xs)
          obtain x1 x2 x3 where x:"x=(x1,x2,x3)" by (metis prod_cases3)
          have "x1∈nodes G2" using G2 G2_nodes Cons.prems x 
            by (metis (lifting) mem_Collect_eq select_convs(1) valid0 valid_graph.is_path.simps(2))
          moreover have "(x1,x2,x3)∈edges (del_unEdge v w v' G)" 
            by (metis Cons.prems valid0 valid_graph.is_path.simps(2) x)
          ultimately have "(x1,x2,x3)∈edges G2" 
            using  ‹nodes G1 ∩ nodes G2={}› ‹edges G1 ∪ edges G2=edges (del_unEdge v w v' G)›
            by (metis IntI Un_iff assms(1) bex_empty connected_def del_UnEdge_node valid0 valid0' 
              valid_G1' valid_graph.E_validD(1) valid_graph.E_validD(2) valid_unMultigraph.no_id)
          moreover have "valid_graph.is_path (del_unEdge v w v' G) x3 xs v'" 
            by (metis Cons.prems valid0 valid_graph.is_path.simps(2) x)
          hence "valid_graph.is_path G2 x3 xs v'" using Cons.hyps by auto
          moreover have "x1=n'" by (metis Cons.prems valid0 valid_graph.is_path.simps(2) x)
          ultimately show ?case using x valid_G2' by (metis valid_graph.is_path.simps(2))   
        qed
      hence "valid_graph.is_path G2 v' (rev_path ps') n'" 
        using valid_unMultigraph.is_path_rev[OF valid_G2]
        by auto
      hence "valid_graph.is_path G2 n (ps@(rev_path ps')) n'" 
        using ps valid_graph.is_path_split[OF valid_G2',of n ps "rev_path ps'" n']
        by auto
      thus "∃ps. valid_graph.is_path G2 n ps n'" by auto
    qed
  ultimately show ?thesis using valid_G1 valid_G2 that by auto
qed


lemma sub_graph_degree_frame:
  assumes "valid_graph G2" "edges G1 ∪ edges G2 =edges G" "nodes G1 ∩ nodes G2={}" "n∈nodes G1"
  shows "degree n G=degree n G1"
proof -
  have "{e ∈ edges G. fst e = n}⊆{e ∈ edges G1. fst e = n}" 
    proof 
      fix e assume  "e ∈ {e ∈ edges G. fst e = n}"
      hence "e∈edges G" "fst e=n" by auto
      moreover have "n∉nodes G2" 
        using ‹nodes G1 ∩ nodes G2={}› ‹n∈nodes G1›
        by auto
      hence "e∉edges G2" using valid_graph.E_validD[OF ‹valid_graph G2›] ‹fst e=n› 
        by (metis prod.exhaust fst_conv)  
      ultimately have "e∈edges G1" using ‹edges G1 ∪ edges G2 =edges G› by auto
      thus "e ∈ {e ∈ edges G1. fst e = n}" using ‹fst e=n› by auto
    qed
  moreover have "{e ∈ edges G1. fst e = n}⊆{e ∈ edges G. fst e = n}" 
    by (metis (lifting) Collect_mono Un_iff assms(2))
  ultimately show ?thesis unfolding degree_def by auto
qed
      
lemma odd_nodes_no_edge[simp]: "finite (nodes g) ⟹ num_of_odd_nodes (g ⦇edges:={} ⦈) = 0" 
  unfolding  num_of_odd_nodes_def odd_nodes_set_def degree_def by simp

section ‹Adjacent nodes›
  
definition (in valid_unMultigraph) adjacent:: "'v ⇒ 'v ⇒ bool" where
    "adjacent v v' ≡ ∃w. (v,w,v')∈E"
    
lemma (in valid_unMultigraph) adjacent_sym: "adjacent v v' ⟷ adjacent v' v" 
    unfolding adjacent_def by auto
  
lemma (in valid_unMultigraph) adjacent_no_loop[simp]: "adjacent v v' ⟹ v ≠v'"
     unfolding adjacent_def by auto

lemma (in valid_unMultigraph) adjacent_V[simp]: 
    assumes "adjacent v v'"
    shows "v∈V" "v'∈V"
  using assms E_validD unfolding adjacent_def by auto


lemma (in valid_unMultigraph) adjacent_finite:
  "finite E ⟹ finite {n. adjacent v n}"
proof -
  assume "finite E"
  { fix S v 
    have "finite S ⟹ finite {n. ∃w. (v,w,n)∈S}" 
      proof (induct S rule: finite_induct)
        case empty
        thus ?case by auto
      next
        case (insert x F)
        obtain x1 x2 x3 where x: "x=(x1,x2,x3)" by (metis prod_cases3)
        have "x1=v ⟹ ?case"
          proof -
            assume "x1=v"
            hence "{n. ∃w. (v, w, n) ∈ insert x F}=insert x3 {n. ∃w. (v, w, n) ∈ F}"
              using x by auto
            thus ?thesis using insert by auto
          qed
        moreover have "x1≠v ⟹ ?case"
          proof -
            assume "x1≠v"
            hence "{n. ∃w. (v, w, n) ∈ insert x F}={n. ∃w. (v, w, n) ∈ F}" using x by auto
            thus ?thesis using insert by auto
          qed
        ultimately show ?case by auto
      qed }
  note aux=this
  show ?thesis using aux[OF ‹finite E›, of v]  unfolding adjacent_def by auto
qed

section‹Undirected simple graph›

locale valid_unSimpGraph=valid_unMultigraph G for G::"('v,'w) graph"+
              assumes no_multi[simp]: "(v,w,u) ∈ edges G ⟹ (v,w',u) ∈edges G ⟹ w = w'"

lemma (in valid_unSimpGraph) finV_to_finE[simp]: 
  assumes "finite V" 
  shows "finite E"
proof (cases "{(v1,v2). adjacent v1 v2}={}")
  case True
  hence "E={}" unfolding adjacent_def by auto
  thus "finite E" by auto
next
  case False
  have "{(v1,v2). adjacent v1 v2} ⊆ V × V" using adjacent_V by auto
  moreover have "finite (V × V)" using ‹finite V› by auto
  ultimately have "finite {(v1,v2). adjacent v1 v2}" using finite_subset by auto
  hence "card {(v1,v2). adjacent v1 v2}≠0" using False card_eq_0_iff by auto
  moreover have "card E=card {(v1,v2). adjacent v1 v2}" 
    proof -
      have "(λ(v1,w,v2). (v1,v2))`E = {(v1,v2). adjacent v1 v2}" 
        proof -
          have "⋀x. x∈(λ(v1,w,v2). (v1,v2))`E ⟹ x∈ {(v1,v2). adjacent v1 v2}" 
            unfolding adjacent_def by auto
          moreover have "⋀x. x∈{(v1,v2). adjacent v1 v2} ⟹ x∈(λ(v1,w,v2). (v1,v2))`E" 
            unfolding adjacent_def by force
          ultimately show ?thesis by force
        qed
      moreover have "inj_on (λ(v1,w,v2). (v1,v2)) E" unfolding inj_on_def by auto
      ultimately show ?thesis by (metis card_image)
    qed
  ultimately show "finite E" by (metis card.infinite)
qed


lemma del_unEdge_valid'[simp]:"valid_unSimpGraph G⟹
    valid_unSimpGraph (del_unEdge v w u G)" 
proof -
  assume "valid_unSimpGraph G"
  hence "valid_unMultigraph (del_unEdge v w u G)" 
    using valid_unSimpGraph_def[of G] del_unEdge_valid[of G] by auto
  moreover have "valid_unSimpGraph_axioms (del_unEdge v w u G)"
    using valid_unSimpGraph.no_multi[OF ‹valid_unSimpGraph G›]
    unfolding valid_unSimpGraph_axioms_def del_unEdge_def by auto
  ultimately show "valid_unSimpGraph (del_unEdge v w u G)" using valid_unSimpGraph_def
    by auto
qed

lemma (in valid_unSimpGraph) del_UnEdge_non_adj: 
    "(v,w,u)∈E ⟹ ¬valid_unMultigraph.adjacent (del_unEdge v w u G) v u"
proof
  assume "(v, w, u) ∈ E" 
      and ccontr:"valid_unMultigraph.adjacent (del_unEdge v w u G) v u"
  have valid:"valid_unMultigraph (del_unEdge v w u G)" 
    using valid_unMultigraph_axioms by auto
  then obtain w' where vw'u:"(v,w',u)∈edges (del_unEdge v w u G)"
    using ccontr unfolding valid_unMultigraph.adjacent_def[OF valid] by auto
  hence "(v,w',u)∉{(v,w,u),(u,w,v)}" unfolding del_unEdge_def by auto
  hence "w'≠w" by auto
  moreover have "(v,w',u)∈E" using vw'u unfolding del_unEdge_def by auto
  ultimately show False using no_multi[of v w u w'] ‹(v, w, u) ∈ E› by auto
qed

lemma (in valid_unSimpGraph) degree_adjacent: "finite E ⟹ degree v G=card {n. adjacent v n}"
  using valid_unSimpGraph_axioms 
proof (induct "degree v G" arbitrary: G)
  case 0
  note valid3=‹valid_unSimpGraph G›
  hence valid2: "valid_unMultigraph G" using valid_unSimpGraph_def by auto
  have "{a. valid_unMultigraph.adjacent G v a}={}" 
    proof (rule ccontr)
      assume "{a. valid_unMultigraph.adjacent G v a} ≠ {}"
      then obtain w u where "(v,w,u)∈edges G" 
        unfolding valid_unMultigraph.adjacent_def[OF valid2] by auto
      hence "degree v G≠0" using ‹finite (edges G)› unfolding degree_def by auto
      thus False using ‹0 = degree v G› by auto
    qed
  thus ?case by (metis "0.hyps" card.empty)
next
  case (Suc n)
  hence "{e ∈ edges G. fst e = v}≠{}" using card.empty unfolding degree_def  by force
  then obtain w u where "(v,w,u)∈edges G" by auto
  have valid:"valid_unMultigraph G" using ‹valid_unSimpGraph G› valid_unSimpGraph_def by auto
  hence valid':"valid_unMultigraph (del_unEdge v w u G)" by auto
  have "valid_unSimpGraph (del_unEdge v w u G)" 
    using del_unEdge_valid' ‹valid_unSimpGraph G› by auto
  moreover have "n = degree v (del_unEdge v w u G)" 
    using ‹Suc n = degree v G›‹(v, w, u) ∈ edges G›  del_edge_undirected_degree_plus[of G v w u]
    by (metis Suc.prems(1) Suc_eq_plus1 diff_Suc_1 valid valid_unMultigraph.corres)
  moreover have "finite (edges (del_unEdge v w u G))" 
    using ‹finite (edges G)› unfolding del_unEdge_def
    by auto
  ultimately have "degree v (del_unEdge v w u G) 
      = card (Collect (valid_unMultigraph.adjacent (del_unEdge v w u G) v))"
    using Suc.hyps  by auto
  moreover have "Suc(card ({n. valid_unMultigraph.adjacent (del_unEdge v w u G)  
      v n})) = card ({n. valid_unMultigraph.adjacent G v n})" 
    using valid_unMultigraph.adjacent_def[OF valid'] 
    proof -
      have "{n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n} ⊆ 
          {n. valid_unMultigraph.adjacent G v n}"
        using del_unEdge_def[of v w u G]
        unfolding valid_unMultigraph.adjacent_def[OF valid'] 
          valid_unMultigraph.adjacent_def[OF valid]
        by auto
      moreover have "u∈{n. valid_unMultigraph.adjacent G v n}" 
        using ‹(v,w,u)∈edges G› unfolding valid_unMultigraph.adjacent_def[OF valid] by auto
      ultimately have "{n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n} ∪ {u}
          ⊆ {n. valid_unMultigraph.adjacent G v n}" by auto
      moreover have "{n. valid_unMultigraph.adjacent G v n} - {u}
          ⊆ {n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n}"
        using del_unEdge_def[of v w u G]
        unfolding valid_unMultigraph.adjacent_def[OF valid'] 
          valid_unMultigraph.adjacent_def[OF valid]
        by auto
      ultimately have "{n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n} ∪ {u}
          = {n. valid_unMultigraph.adjacent G v n}" by auto
      moreover have "u∉{n. valid_unMultigraph.adjacent (del_unEdge v w u G) v n}" 
        using valid_unSimpGraph.del_UnEdge_non_adj[OF ‹valid_unSimpGraph G› ‹(v,w,u)∈edges G›]
        by auto
      moreover have "finite {n. valid_unMultigraph.adjacent G v n}" 
        using valid_unMultigraph.adjacent_finite[OF valid ‹finite (edges G)›] by simp 
      ultimately show ?thesis 
        by (metis Un_insert_right card_insert_disjoint finite_Un sup_bot_right)
    qed
  ultimately show ?case by (metis Suc.hyps(2) ‹n = degree v (del_unEdge v w u G)›)
qed 
  
end