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)"

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})"
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)
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' ```