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. eedges g  fst e=v})"

definition odd_nodes_set :: "('v,'w) graph  'v set" where
    "odd_nodes_set g  {v. vnodes 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. vnodes 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. eedges G - {(v,w,v'),(v',w,v)}  fst e=x})" 
    by (simp add:del_unEdge_def degree_def)
  also have "...=card({e. eedges G  fst e=x}-{e. e{(v,w,v'),(v',w,v)}  fst e=x})"
    by (metis  set_compre_diff)
  also have "...=card({e. eedges G  fst e=x})" using x  {v, v'} 
    proof -
      have "xv  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]: "vnodes (del_unEdge u e u' G)  vnodes 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]: 
  "xedges g  x(v,e,v') x(v',e,v)  xedges (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 "xedges G1"
    by (metis Cons.prems assms(1) valid_unMultigraph.is_trail.simps(2) x)
  hence "xedges 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 "vodd_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 "vnodes (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  "vodd_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'}  xodd_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'}  xodd_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 "vv'" 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:"vodd_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' xodd_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  xodd_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'}  xodd_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'}   xodd_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  "vodd_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'}  xodd_nodes_set G" 
        using x_odd_set del_UnEdge_node unfolding odd_nodes_set_def  
        by auto
      moreover have "x{v,v'}  xodd_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 "vv'" 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 "vv'  (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 "x3v'?case" 
    proof (cases "v=v'")
      case True
      assume "x3v'"
      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 "x3v'"
      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 "vv'  (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 "x3v'" 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 "nx3 ?case" 
    proof -
      assume "nx3"
       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) vv' 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)  x3v' 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)  x3v'  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)  vv' then 2 else 0)" 
        proof -
          have "x1x3" by (metis valid_rem_xs valid_unMultigraph.no_id x_in)
          moreover hence "x1v'" 
            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)  x1v'" using x1  v' by auto
          hence "even(degree v G)  vv'" 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)  vv' 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)  x3v' 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)  x3v'  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)  vv' then 2 else 0)"
        proof -
          have "x1x3" by (metis valid_rem_xs valid_unMultigraph.no_id x_in)
          moreover hence "x1v'" 
            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)  x1v'" using x1  v' by auto
          hence "even(degree v G)  vv'" 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)  vv' 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)  x3v' 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)  x3v'  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)  vv' then 2 else 0)" 
        proof (cases "vv'")
          case True
          have "x1x3" 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)  vv' 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)  x3v' 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)  x3v'  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)  vv' then 2 else 0)" 
         proof (cases "vv'")
          case True
          have "x1x3" 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)  vv' 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) vv' 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)  x3v' 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)  x3v'  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)  vv' then -2 else 0)" 
         proof (cases "vv'")
          case True
          have "x1x3" 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)  vv' 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)  x3v' 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)  x3v'  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)  vv' then -2 else 0)"
         proof (cases "vv'")
          case True
          have "x1x3" 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)  vv' 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)  x3v' 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)  x3v'  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)  x3v'" by (metis parity_x1_x3(2))
          thus ?thesis by auto
        qed
      also have "...=num_of_odd_nodes G+(if odd(degree v G)  vv' then -2 else 0)" 
         proof -
          have "x1x3" by (metis valid_rem_xs valid_unMultigraph.no_id x_in)
          moreover hence "x1v'" 
            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)  x1v'" using x1  v' by auto
          hence "odd(degree v G)  vv'" 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)  vv' 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))"