(* Title: MoreGraph.thy Author:Wenda Li *) theory MoreGraph imports Complex_Main Dijkstra_Shortest_Path.Graph begin section ‹Undirected Multigraph and undirected trails› locale valid_unMultigraph=valid_graph G for G::"('v,'w) graph"+ assumes corres[simp]: "(v,w,u') ∈ edges G ⟷ (u',w,v) ∈ edges G" and no_id[simp]:"(v,w,v) ∉ edges G" fun (in valid_unMultigraph) is_trail :: "'v ⇒ ('v,'w) path ⇒ 'v ⇒ bool" where "is_trail v [] v' ⟷ v=v' ∧ v'∈ V" | "is_trail v ((v1,w,v2)#ps) v' ⟷ v=v1 ∧ (v1,w,v2)∈E ∧ (v1,w,v2)∉set ps ∧(v2,w,v1)∉set ps ∧ is_trail v2 ps v'" (*This section mainly includes lemmas related to degrees of nodes, especially when edges and paths are removed from an undirected graph*) section ‹Degrees and related properties› definition degree :: "'v ⇒ ('v,'w) graph ⇒ nat" where "degree v g≡ card({e. e∈edges g ∧ fst e=v})" definition odd_nodes_set :: "('v,'w) graph ⇒ 'v set" where "odd_nodes_set g ≡ {v. v∈nodes g ∧ odd(degree v g)}" (*return the number of nodes with an odd degree in the current valid multigraph*) definition num_of_odd_nodes :: "('v, 'w) graph ⇒ nat" where "num_of_odd_nodes g≡ card( odd_nodes_set g)" definition num_of_even_nodes :: "('v, 'w) graph ⇒ nat" where "num_of_even_nodes g≡ card( {v. v∈nodes g ∧ even(degree v g)})" definition del_unEdge where "del_unEdge v e v' g ≡ ⦇ nodes = nodes g, edges = edges g - {(v,e,v'),(v',e,v)} ⦈" definition rev_path :: "('v,'w) path ⇒ ('v,'w) path" where "rev_path ps ≡ map (λ(a,b,c).(c,b,a)) (rev ps)" fun rem_unPath:: "('v,'w) path ⇒ ('v,'w) graph ⇒ ('v,'w) graph" where "rem_unPath [] g= g"| "rem_unPath ((v,w,v')#ps) g= rem_unPath ps (del_unEdge v w v' g)" lemma del_undirected: "del_unEdge v e v' g = delete_edge v' e v (delete_edge v e v' g)" unfolding del_unEdge_def delete_edge_def by auto lemma delete_edge_sym: "del_unEdge v e v' g = del_unEdge v' e v g" unfolding del_unEdge_def by auto lemma del_unEdge_valid[simp]: assumes "valid_unMultigraph g" shows "valid_unMultigraph (del_unEdge v e v' g)" proof - interpret valid_unMultigraph g by fact show ?thesis unfolding del_unEdge_def by unfold_locales (auto dest: E_validD) qed lemma set_compre_diff:"{x ∈ A - B. P x}={x ∈ A. P x} - {x ∈ B . P x}" by blast lemma set_compre_subset: "B ⊆ A ⟹ {x ∈ B. P x} ⊆ {x ∈ A. P x}" by blast lemma del_edge_undirected_degree_plus: "finite (edges g) ⟹ (v,e,v') ∈ edges g ⟹ (v',e,v) ∈ edges g ⟹ degree v (del_unEdge v e v' g) + 1=degree v g" proof - assume assms: "finite (edges g)" "(v,e,v') ∈ edges g" "(v',e,v) ∈ edges g " have "degree v (del_unEdge v e v' g) + 1 = card ({ea ∈ edges g - {(v, e, v'), (v', e, v)}. fst ea = v}) + 1" unfolding del_unEdge_def degree_def by simp also have "...=card ({ea ∈ edges g. fst ea = v} - {ea ∈ {(v, e, v'), (v', e, v)}. fst ea = v})+1" by (metis set_compre_diff) also have "...=card ({ea ∈ edges g. fst ea = v}) - card({ea ∈ {(v, e, v'), (v', e, v)}. fst ea = v})+1" proof - have "{(v, e, v'), (v', e, v)} ⊆ edges g" using ‹(v,e,v') ∈ edges g› ‹(v',e,v) ∈ edges g› by auto hence "{ea ∈ {(v, e, v'), (v', e, v)}. fst ea = v} ⊆ {ea ∈ edges g. fst ea = v}" by auto moreover have "finite {ea ∈ {(v, e, v'), (v', e, v)}. fst ea = v}" by auto ultimately have "card ({ea ∈ edges g. fst ea = v} - {ea ∈ {(v, e, v'), (v', e, v)}. fst ea = v})=card {ea ∈ edges g. fst ea = v} - card {ea ∈ {(v, e, v'), (v', e, v)}. fst ea = v}" using card_Diff_subset by blast thus ?thesis by auto qed also have "...=card ({ea ∈ edges g. fst ea = v})" proof - have "{ea ∈ {(v, e, v'), (v', e, v)}. fst ea = v}={(v,e,v')}" by auto hence "card {ea ∈ {(v, e, v'), (v', e, v)}. fst ea = v} = 1" by auto moreover have "card {ea ∈ edges g. fst ea = v}≠0" by (metis (lifting, mono_tags) Collect_empty_eq assms(1) assms(2) card_eq_0_iff fst_conv mem_Collect_eq rev_finite_subset subsetI) ultimately show ?thesis by arith qed finally have "degree v (del_unEdge v e v' g) + 1=card ({ea ∈ edges g. fst ea = v})" . thus ?thesis unfolding degree_def . qed lemma del_edge_undirected_degree_plus': "finite (edges g) ⟹ (v,e,v') ∈ edges g ⟹ (v',e,v) ∈ edges g ⟹ degree v' (del_unEdge v e v' g) + 1=degree v' g" by (metis del_edge_undirected_degree_plus delete_edge_sym) lemma del_edge_undirected_degree_minus[simp]: "finite (edges g) ⟹ (v,e,v') ∈ edges g ⟹ (v',e,v) ∈ edges g ⟹ degree v (del_unEdge v e v' g) =degree v g- (1::nat)" using del_edge_undirected_degree_plus by (metis add_diff_cancel_left' add.commute) lemma del_edge_undirected_degree_minus'[simp]: "finite (edges g) ⟹ (v,e,v') ∈ edges g ⟹ (v',e,v) ∈ edges g ⟹ degree v' (del_unEdge v e v' g) =degree v' g- (1::nat)" by (metis del_edge_undirected_degree_minus delete_edge_sym) lemma del_unEdge_com: "del_unEdge v w v' (del_unEdge n e n' g) = del_unEdge n e n' (del_unEdge v w v' g)" unfolding del_unEdge_def by auto lemma rem_unPath_com: "rem_unPath ps (del_unEdge v w v' g) = del_unEdge v w v' (rem_unPath ps g)" proof (induct ps arbitrary: g) case Nil thus ?case by (metis rem_unPath.simps(1)) next case (Cons a ps') thus ?case using del_unEdge_com by (metis prod_cases3 rem_unPath.simps(1) rem_unPath.simps(2)) qed lemma rem_unPath_valid[intro]: "valid_unMultigraph g ⟹ valid_unMultigraph (rem_unPath ps g)" proof (induct ps ) case Nil thus ?case by simp next case (Cons x xs) thus ?case proof - have "valid_unMultigraph (rem_unPath (x # xs) g) = valid_unMultigraph (del_unEdge (fst x) (fst (snd x)) (snd (snd x)) (rem_unPath xs g))" using rem_unPath_com by (metis prod.collapse rem_unPath.simps(2)) also have "...=valid_unMultigraph (rem_unPath xs g)" by (metis Cons.hyps Cons.prems del_unEdge_valid) also have "...=True" using Cons by auto finally have "?case=True" . thus ?case by simp qed qed lemma (in valid_unMultigraph) degree_frame: assumes "finite (edges G)" "x ∉ {v, v'}" shows "degree x (del_unEdge v w v' G) = degree x G" (is "?L=?R") proof (cases "(v,w,v') ∈ edges G") case True have "?L=card({e. e∈edges G - {(v,w,v'),(v',w,v)} ∧ fst e=x})" by (simp add:del_unEdge_def degree_def) also have "...=card({e. e∈edges G ∧ fst e=x}-{e. e∈{(v,w,v'),(v',w,v)} ∧ fst e=x})" by (metis set_compre_diff) also have "...=card({e. e∈edges G ∧ fst e=x})" using ‹x ∉ {v, v'}› proof - have "x≠v ∧ x≠ v'" using ‹x∉{v,v'}›by simp hence "{e. e∈{(v,w,v'),(v',w,v)} ∧ fst e=x}={}" by auto thus ?thesis by (metis Diff_empty) qed also have "...=?R" by (simp add:degree_def) finally show ?thesis . next case False moreover hence "(v',w,v)∉E" using corres by auto ultimately have "E- {(v,w,v'),(v',w,v)}=E" by blast hence "del_unEdge v w v' G=G" by (auto simp add:del_unEdge_def) thus ?thesis by auto qed lemma [simp]: "rev_path [] = []" unfolding rev_path_def by simp lemma rev_path_append[simp]: "rev_path (xs@ys) = (rev_path ys) @ (rev_path xs)" unfolding rev_path_def rev_append by auto lemma rev_path_double[simp]: "rev_path(rev_path xs)=xs" unfolding rev_path_def by (induct xs,auto) lemma del_UnEdge_node[simp]: "v∈nodes (del_unEdge u e u' G) ⟷ v∈nodes G " by (metis del_unEdge_def select_convs(1)) lemma [intro!]: "finite (edges G) ⟹ finite (edges (del_unEdge u e u' G))" by (metis del_unEdge_def finite_Diff select_convs(2)) lemma [intro!]: "finite (nodes G) ⟹ finite (nodes (del_unEdge u e u' G))" by (metis del_unEdge_def select_convs(1)) lemma [intro!]: "finite (edges G) ⟹ finite (edges (rem_unPath ps G))" proof (induct ps arbitrary:G) case Nil thus ?case by simp next case (Cons x xs) hence "finite (edges (rem_unPath (x # xs) G)) = finite (edges (del_unEdge (fst x) (fst (snd x)) (snd (snd x)) (rem_unPath xs G)))" by (metis rem_unPath.simps(2) rem_unPath_com surjective_pairing) also have "...=finite (edges (rem_unPath xs G))" using del_unEdge_def by (metis finite.emptyI finite_Diff2 finite_Diff_insert select_convs(2)) also have "...=True" using Cons by auto finally have "?case = True" . thus ?case by simp qed lemma del_UnEdge_frame[intro]: "x∈edges g ⟹ x≠(v,e,v') ⟹x≠(v',e,v) ⟹ x∈edges (del_unEdge v e v' g)" unfolding del_unEdge_def by auto lemma [intro!]: "finite (nodes G) ⟹ finite (odd_nodes_set G)" by (metis (lifting) mem_Collect_eq odd_nodes_set_def rev_finite_subset subsetI) lemma [simp]: "nodes (del_unEdge u e u' G)=nodes G" by (metis del_unEdge_def select_convs(1)) lemma [simp]: "nodes (rem_unPath ps G) = nodes G" proof (induct ps) case Nil show ?case by simp next case (Cons x xs) have "nodes (rem_unPath (x # xs) G)=nodes (del_unEdge (fst x) (fst (snd x)) (snd (snd x)) (rem_unPath xs G))" by (metis rem_unPath.simps(2) rem_unPath_com surjective_pairing) also have "...=nodes (rem_unPath xs G)" by auto also have "...=nodes G" using Cons by auto finally show ?case . qed lemma [intro!]: "finite (nodes G) ⟹ finite (nodes (rem_unPath ps G))" by auto lemma in_set_rev_path[simp]: "(v',w,v )∈set (rev_path ps) ⟷ (v,w,v')∈set ps " proof (induct ps) case Nil thus ?case unfolding rev_path_def by auto next case (Cons x xs) obtain x1 x2 x3 where x:"x=(x1,x2,x3)" by (metis prod_cases3) have "set (rev_path (x # xs))=set ((rev_path xs)@[(x3,x2,x1)])" unfolding rev_path_def using x by auto also have "...=set (rev_path xs) ∪ {(x3,x2,x1)}" by auto finally have "set (rev_path (x # xs)) =set (rev_path xs) ∪ {(x3,x2,x1)}" . moreover have "set (x#xs)= set xs ∪ {(x1,x2,x3)}" by (metis List.set_simps(2) insert_is_Un sup_commute x) ultimately show ?case using Cons by auto qed lemma rem_unPath_edges: "edges(rem_unPath ps G) = edges G - (set ps ∪ set (rev_path ps))" proof (induct ps) case Nil show ?case unfolding rev_path_def by auto next case (Cons x xs) obtain x1 x2 x3 where x: "x=(x1,x2,x3)" by (metis prod_cases3) hence "edges(rem_unPath (x#xs) G)= edges(del_unEdge x1 x2 x3 (rem_unPath xs G))" by (metis rem_unPath.simps(2) rem_unPath_com) also have "...=edges(rem_unPath xs G)-{(x1,x2,x3),(x3,x2,x1)}" by (metis del_unEdge_def select_convs(2)) also have "...= edges G - (set xs ∪ set (rev_path xs))-{(x1,x2,x3),(x3,x2,x1)}" by (metis Cons.hyps) also have "...=edges G - (set (x#xs) ∪ set (rev_path (x#xs)))" proof - have "set (rev_path xs) ∪ {(x3,x2,x1)}=set ((rev_path xs)@[(x3,x2,x1)])" by (metis List.set_simps(2) empty_set set_append) also have "...=set (rev_path (x#xs))" unfolding rev_path_def using x by auto finally have "set (rev_path xs) ∪ {(x3,x2,x1)}=set (rev_path (x#xs))" . moreover have "set xs ∪ {(x1,x2,x3)}=set (x#xs)" by (metis List.set_simps(2) insert_is_Un sup_commute x) moreover have "edges G - (set xs ∪ set (rev_path xs))-{(x1,x2,x3),(x3,x2,x1)} = edges G - ((set xs ∪ {(x1,x2,x3)}) ∪ (set (rev_path xs) ∪ {(x3,x2,x1)}))" by auto ultimately show ?thesis by auto qed finally show ?case . qed lemma rem_unPath_graph [simp]: "rem_unPath (rev_path ps) G=rem_unPath ps G" proof - have "nodes(rem_unPath (rev_path ps) G)=nodes(rem_unPath ps G)" by auto moreover have "edges(rem_unPath (rev_path ps) G)=edges(rem_unPath ps G)" proof - have "set (rev_path ps) ∪ set (rev_path (rev_path ps)) = set ps ∪ set (rev_path ps) " by auto thus ?thesis by (metis rem_unPath_edges) qed ultimately show ?thesis by auto qed lemma distinct_rev_path[simp]: "distinct (rev_path ps) ⟷distinct ps" proof (induct ps) case Nil show ?case by auto next case (Cons x xs) obtain x1 x2 x3 where x: "x=(x1,x2,x3)" by (metis prod_cases3) hence "distinct (rev_path (x # xs))=distinct ((rev_path xs)@[(x3,x2,x1)])" unfolding rev_path_def by auto also have "...= (distinct (rev_path xs) ∧ (x3,x2,x1)∉set (rev_path xs))" by (metis distinct.simps(2) distinct1_rotate rotate1.simps(2)) also have "...=distinct (x#xs)" by (metis Cons.hyps distinct.simps(2) in_set_rev_path x) finally have "distinct (rev_path (x # xs))=distinct (x#xs)" . thus ?case . qed lemma (in valid_unMultigraph) is_path_rev: "is_path v' (rev_path ps) v ⟷ is_path v ps v'" proof (induct ps arbitrary: v) case Nil show ?case by auto next case (Cons x xs) obtain x1 x2 x3 where x: "x=(x1,x2,x3)" by (metis prod_cases3) hence "is_path v' (rev_path (x # xs)) v=is_path v' ((rev_path xs) @[(x3,x2,x1)]) v" unfolding rev_path_def by auto also have "...=(is_path v' (rev_path xs) x3 ∧ (x3,x2,x1)∈E ∧ is_path x1 [] v)" by auto also have "...=(is_path x3 xs v' ∧ (x3,x2,x1)∈E ∧ is_path x1 [] v)" using Cons.hyps by auto also have "...=is_path v (x#xs) v'" by (metis corres is_path.simps(1) is_path.simps(2) is_path_memb x) finally have "is_path v' (rev_path (x # xs)) v=is_path v (x#xs) v'" . thus ?case . qed lemma (in valid_unMultigraph) singleton_distinct_path [intro]: "(v,w,v')∈E ⟹ is_trail v [(v,w,v')] v'" by (metis E_validD(2) all_not_in_conv is_trail.simps set_empty) lemma (in valid_unMultigraph) is_trail_path: "is_trail v ps v' ⟷ is_path v ps v' ∧ distinct ps ∧ (set ps ∩ set (rev_path ps) = {})" proof (induct ps arbitrary:v) case Nil show ?case by auto next case (Cons x xs) obtain x1 x2 x3 where x: "x=(x1,x2,x3)" by (metis prod_cases3) hence "is_trail v (x#xs) v'= (v=x1 ∧ (x1,x2,x3)∈E ∧ (x1,x2,x3)∉set xs ∧(x3,x2,x1)∉set xs ∧ is_trail x3 xs v')" by (metis is_trail.simps(2)) also have "...=(v=x1 ∧ (x1,x2,x3)∈E ∧ (x1,x2,x3)∉set xs ∧(x3,x2,x1)∉set xs ∧ is_path x3 xs v' ∧ distinct xs ∧ (set xs ∩ set (rev_path xs)={}))" using Cons.hyps by auto also have "...=(is_path v (x#xs) v' ∧ (x1,x2,x3) ≠ (x3,x2,x1) ∧ (x1,x2,x3)∉set xs ∧(x3,x2,x1)∉set xs ∧ distinct xs ∧ (set xs ∩ set (rev_path xs)={}))" by (metis append_Nil is_path.simps(1) is_path_simps(2) is_path_split' no_id x) also have "...=(is_path v (x#xs) v' ∧ (x1,x2,x3) ≠ (x3,x2,x1) ∧(x3,x2,x1)∉set xs ∧ distinct (x#xs) ∧ (set xs ∩ set (rev_path xs)={}))" by (metis (full_types) distinct.simps(2) x) also have "...=(is_path v (x#xs) v' ∧ (x1,x2,x3) ≠ (x3,x2,x1) ∧ distinct (x#xs) ∧ (x3,x2,x1)∉set xs ∧ set xs ∩ set (rev_path (x#xs))={})" proof - have "set (rev_path (x#xs)) = set ((rev_path xs)@[(x3,x2,x1)])" using x by auto also have "... = set (rev_path xs) ∪ {(x3,x2,x1)}" by auto finally have "set (rev_path (x#xs))=set (rev_path xs) ∪ {(x3,x2,x1)}" . thus ?thesis by blast qed also have "...=(is_path v (x#xs) v'∧ distinct (x#xs) ∧ (set (x#xs) ∩ set (rev_path (x#xs))={}))" proof - have "(x3,x2,x1)∉set xs ⟷ (x1,x2,x3)∉ set (rev_path xs)" using in_set_rev_path by auto moreover have "set (rev_path (x#xs))=set (rev_path xs) ∪ {(x3,x2,x1)}" unfolding rev_path_def using x by auto ultimately have " (x1,x2,x3) ≠ (x3,x2,x1)∧ (x3,x2,x1)∉set xs ⟷ (x1,x2,x3)∉ set (rev_path (x#xs))" by blast thus ?thesis by (metis (mono_tags) Int_iff Int_insert_left_if0 List.set_simps(2) empty_iff insertI1 x) qed finally have "is_trail v (x#xs) v'⟷(is_path v (x#xs) v'∧ distinct (x#xs) ∧ (set (x#xs) ∩ set (rev_path (x#xs))={}))" . thus ?case . qed lemma (in valid_unMultigraph) is_trail_rev: "is_trail v' (rev_path ps) v ⟷ is_trail v ps v' " using rev_path_append is_trail_path is_path_rev distinct_rev_path by (metis Int_commute distinct_append) lemma (in valid_unMultigraph) is_trail_intro[intro]: "is_trail v' ps v ⟹ is_path v' ps v" by (induct ps arbitrary:v',auto) lemma (in valid_unMultigraph) is_trail_split: "is_trail v (p1@p2) v' ⟹ (∃u. is_trail v p1 u ∧ is_trail u p2 v')" apply (induct p1 arbitrary: v,auto) apply (metis is_trail_intro is_path_memb) done lemma (in valid_unMultigraph) is_trail_split':"is_trail v (p1@(u,w,u')#p2) v' ⟹ is_trail v p1 u ∧ (u,w,u')∈E ∧ is_trail u' p2 v'" by (metis is_trail.simps(2) is_trail_split) lemma (in valid_unMultigraph) distinct_elim[simp]: assumes "is_trail v ((v1,w,v2)#ps) v'" shows "(v1,w,v2)∈edges(rem_unPath ps G) ⟷ (v1,w,v2)∈E" proof assume "(v1, w, v2) ∈ edges (rem_unPath ps G)" thus "(v1, w, v2) ∈ E" by (metis assms is_trail.simps(2)) next assume "(v1, w, v2) ∈ E" have "(v1,w,v2)∉set ps ∧ (v2,w,v1)∉set ps" by (metis assms is_trail.simps(2)) hence "(v1,w,v2)∉set ps ∧ (v1,w,v2)∉set (rev_path ps)" by simp hence "(v1,w,v2)∉set ps ∪ set (rev_path ps)" by simp hence "(v1,w,v2)∈edges G - (set ps ∪ set (rev_path ps))" using ‹(v1, w, v2) ∈ E› by auto thus "(v1,w,v2)∈edges(rem_unPath ps G)" by (metis rem_unPath_edges) qed lemma distinct_path_subset: assumes "valid_unMultigraph G1" "valid_unMultigraph G2" "edges G1 ⊆edges G2" "nodes G1 ⊆nodes G2" assumes distinct_G1:"valid_unMultigraph.is_trail G1 v ps v'" shows "valid_unMultigraph.is_trail G2 v ps v'" using distinct_G1 proof (induct ps arbitrary:v) case Nil hence "v=v'∧v'∈nodes G1" by (metis (full_types) assms(1) valid_unMultigraph.is_trail.simps(1)) hence "v=v'∧v'∈nodes G2" using ‹nodes G1 ⊆ nodes G2› by auto thus ?case by (metis assms(2) valid_unMultigraph.is_trail.simps(1)) next case (Cons x xs) obtain x1 x2 x3 where x:"x=(x1,x2,x3)" by (metis prod_cases3) hence "valid_unMultigraph.is_trail G1 x3 xs v'" by (metis Cons.prems assms(1) valid_unMultigraph.is_trail.simps(2)) hence "valid_unMultigraph.is_trail G2 x3 xs v'" using Cons by auto moreover have "x∈edges G1" by (metis Cons.prems assms(1) valid_unMultigraph.is_trail.simps(2) x) hence "x∈edges G2" using ‹edges G1 ⊆ edges G2› by auto moreover have "v=x1∧(x1,x2,x3)∉set xs∧(x3,x2,x1)∉set xs" by (metis Cons.prems assms(1) valid_unMultigraph.is_trail.simps(2) x) hence "v=x1" "(x1,x2,x3)∉set xs" "(x3,x2,x1)∉set xs" by auto ultimately show ?case by (metis assms(2) valid_unMultigraph.is_trail.simps(2) x) qed lemma (in valid_unMultigraph) distinct_path_intro': assumes "valid_unMultigraph.is_trail (rem_unPath p G) v ps v'" shows "is_trail v ps v'" proof - have valid:"valid_unMultigraph (rem_unPath p G)" using rem_unPath_valid[OF valid_unMultigraph_axioms,of p] by auto moreover have "nodes (rem_unPath p G) ⊆ V" by auto moreover have "edges (rem_unPath p G) ⊆ E" using rem_unPath_edges by auto ultimately show ?thesis using distinct_path_subset[of "rem_unPath p G" G] valid_unMultigraph_axioms assms by auto qed lemma (in valid_unMultigraph) distinct_path_intro: assumes "valid_unMultigraph.is_trail (del_unEdge x1 x2 x3 G) v ps v'" shows "is_trail v ps v'" by (metis (full_types) assms distinct_path_intro' rem_unPath.simps(1) rem_unPath.simps(2)) lemma (in valid_unMultigraph) distinct_elim_rev[simp]: assumes "is_trail v ((v1,w,v2)#ps) v'" shows "(v2,w,v1)∈edges(rem_unPath ps G) ⟷ (v2,w,v1)∈E" proof - have "valid_unMultigraph (rem_unPath ps G)" using valid_unMultigraph_axioms by auto hence "(v2,w,v1)∈edges(rem_unPath ps G)⟷(v1,w,v2)∈edges(rem_unPath ps G)" by (metis valid_unMultigraph.corres) moreover have "(v2,w,v1)∈E⟷(v1,w,v2)∈E" using corres by simp ultimately show ?thesis using distinct_elim by (metis assms) qed lemma (in valid_unMultigraph) del_UnEdge_even: assumes "(v,w,v') ∈ E" "finite E" shows "v∈odd_nodes_set(del_unEdge v w v' G) ⟷ even (degree v G)" proof - have "degree v (del_unEdge v w v' G) + 1=degree v G" using del_edge_undirected_degree_plus corres by (metis assms) from this [symmetric] have "odd (degree v (del_unEdge v w v' G)) = even (degree v G)" by simp moreover have "v∈nodes (del_unEdge v w v' G)" by (metis E_validD(1) assms(1) del_UnEdge_node) ultimately show ?thesis unfolding odd_nodes_set_def by auto qed lemma (in valid_unMultigraph) del_UnEdge_even': assumes "(v,w,v') ∈ E" "finite E" shows "v'∈odd_nodes_set(del_unEdge v w v' G) ⟷ even (degree v' G)" proof - show ?thesis by (metis (full_types) assms corres del_UnEdge_even delete_edge_sym) qed lemma del_UnEdge_even_even: assumes "valid_unMultigraph G" "finite(edges G)" "finite(nodes G)" "(v, w, v')∈edges G" assumes parity_assms: "even (degree v G)" "even (degree v' G)" shows "num_of_odd_nodes(del_unEdge v w v' G)=num_of_odd_nodes G + 2" proof - interpret G:valid_unMultigraph by fact have "v∈odd_nodes_set(del_unEdge v w v' G)" by (metis G.del_UnEdge_even assms(2) assms(4) parity_assms(1)) moreover have "v'∈odd_nodes_set(del_unEdge v w v' G)" by (metis G.del_UnEdge_even' assms(2) assms(4) parity_assms(2)) ultimately have extra_odd_nodes:"{v,v'} ⊆ odd_nodes_set(del_unEdge v w v' G)" unfolding odd_nodes_set_def by auto moreover have "v ∉odd_nodes_set G" and "v'∉odd_nodes_set G" using parity_assms unfolding odd_nodes_set_def by auto hence vv'_odd_disjoint: "{v,v'} ∩ odd_nodes_set G = {}" by auto moreover have "odd_nodes_set(del_unEdge v w v' G) -{v,v'}⊆odd_nodes_set G " proof fix x assume x_odd_set: "x ∈ odd_nodes_set (del_unEdge v w v' G) - {v, v'}" hence "degree x (del_unEdge v w v' G) = degree x G" by (metis Diff_iff G.degree_frame assms(2)) hence "odd(degree x G)" using x_odd_set unfolding odd_nodes_set_def by auto moreover have "x ∈ nodes G" using x_odd_set unfolding odd_nodes_set_def by auto ultimately show "x ∈ odd_nodes_set G" unfolding odd_nodes_set_def by auto qed moreover have "odd_nodes_set G ⊆ odd_nodes_set(del_unEdge v w v' G)" proof fix x assume x_odd_set: "x ∈ odd_nodes_set G" hence "x∉{v,v'} ⟹ odd(degree x (del_unEdge v w v' G))" by (metis (lifting) G.degree_frame assms(2) mem_Collect_eq odd_nodes_set_def) hence "x∉{v,v'} ⟹ x∈odd_nodes_set(del_unEdge v w v' G)" using x_odd_set del_UnEdge_node unfolding odd_nodes_set_def by auto moreover have "x∈{v,v'} ⟹ x∈odd_nodes_set(del_unEdge v w v' G)" using extra_odd_nodes by auto ultimately show "x ∈ odd_nodes_set (del_unEdge v w v' G)" by auto qed ultimately have "odd_nodes_set(del_unEdge v w v' G)=odd_nodes_set G ∪ {v,v'}" by auto thus "num_of_odd_nodes(del_unEdge v w v' G) = num_of_odd_nodes G + 2" proof - assume "odd_nodes_set(del_unEdge v w v' G)=odd_nodes_set G ∪ {v,v'}" moreover have "v≠v'" using G.no_id ‹(v,w,v')∈edges G› by auto hence "card{v,v'}=2" by simp moreover have " odd_nodes_set G ∩ {v,v'} = {}" using vv'_odd_disjoint by auto moreover have "finite(odd_nodes_set G)" by (metis (lifting) assms(3) mem_Collect_eq odd_nodes_set_def rev_finite_subset subsetI) moreover have "finite {v,v'}" by auto ultimately show ?thesis unfolding num_of_odd_nodes_def using card_Un_disjoint by metis qed qed lemma del_UnEdge_even_odd: assumes "valid_unMultigraph G" "finite(edges G)" "finite(nodes G)" "(v, w, v')∈edges G" assumes parity_assms: "even (degree v G)" "odd (degree v' G)" shows "num_of_odd_nodes(del_unEdge v w v' G)=num_of_odd_nodes G" proof - interpret G : valid_unMultigraph by fact have odd_v:"v∈odd_nodes_set(del_unEdge v w v' G)" by (metis G.del_UnEdge_even assms(2) assms(4) parity_assms(1)) have not_odd_v':"v'∉odd_nodes_set(del_unEdge v w v' G)" by (metis G.del_UnEdge_even' assms(2) assms(4) parity_assms(2)) have "odd_nodes_set(del_unEdge v w v' G) ∪ {v'} ⊆odd_nodes_set G ∪ {v}" proof fix x assume x_prems:" x ∈ odd_nodes_set (del_unEdge v w v' G) ∪ {v'}" have "x=v' ⟹x∈odd_nodes_set G ∪ {v}" using parity_assms by (metis (lifting) G.E_validD(2) Un_def assms(4) mem_Collect_eq odd_nodes_set_def ) moreover have "x=v ⟹ x∈odd_nodes_set G ∪ {v}" by (metis insertI1 insert_is_Un sup_commute) moreover have "x∉{v,v'} ⟹ x ∈ odd_nodes_set (del_unEdge v w v' G)" using x_prems by auto hence "x∉{v,v'} ⟹ x ∈ odd_nodes_set G" unfolding odd_nodes_set_def using G.degree_frame ‹finite (edges G)› by auto hence "x∉{v,v'} ⟹ x∈odd_nodes_set G ∪ {v}" by simp ultimately show "x ∈ odd_nodes_set G ∪ {v}" by auto qed moreover have "odd_nodes_set G ∪ {v} ⊆ odd_nodes_set(del_unEdge v w v' G) ∪ {v'}" proof fix x assume x_prems: "x ∈ odd_nodes_set G ∪ {v}" have "x=v ⟹ x ∈ odd_nodes_set (del_unEdge v w v' G) ∪ {v'}" by (metis UnI1 odd_v) moreover have "x=v' ⟹ x ∈ odd_nodes_set (del_unEdge v w v' G) ∪ {v'}" by auto moreover have "x∉{v,v'} ⟹ x ∈ odd_nodes_set G ∪ {v}" using x_prems by auto hence "x∉{v,v'} ⟹ x∈odd_nodes_set (del_unEdge v w v' G)" unfolding odd_nodes_set_def using G.degree_frame ‹finite (edges G)› by auto hence "x∉{v,v'} ⟹ x ∈ odd_nodes_set (del_unEdge v w v' G) ∪ {v'}" by simp ultimately show "x ∈ odd_nodes_set (del_unEdge v w v' G) ∪ {v'}" by auto qed ultimately have "odd_nodes_set(del_unEdge v w v' G) ∪ {v'} = odd_nodes_set G ∪ {v}" by auto moreover have " odd_nodes_set G ∩ {v} = {}" using parity_assms unfolding odd_nodes_set_def by auto moreover have " odd_nodes_set(del_unEdge v w v' G) ∩ {v'}={}" by (metis Int_insert_left_if0 inf_bot_left inf_commute not_odd_v') moreover have "finite (odd_nodes_set(del_unEdge v w v' G))" using ‹finite (nodes G)› by auto moreover have "finite (odd_nodes_set G)" using ‹finite (nodes G)› by auto ultimately have "card(odd_nodes_set G) + card {v} = card(odd_nodes_set(del_unEdge v w v' G)) + card {v'}" using card_Un_disjoint[of "odd_nodes_set (del_unEdge v w v' G)" "{v'}"] card_Un_disjoint[of "odd_nodes_set G" "{v}"] by auto thus ?thesis unfolding num_of_odd_nodes_def by simp qed lemma del_UnEdge_odd_even: assumes "valid_unMultigraph G" "finite(edges G)" "finite(nodes G)" "(v, w, v')∈edges G" assumes parity_assms: "odd (degree v G)" "even (degree v' G)" shows "num_of_odd_nodes(del_unEdge v w v' G)=num_of_odd_nodes G" by (metis assms del_UnEdge_even_odd delete_edge_sym parity_assms valid_unMultigraph.corres) lemma del_UnEdge_odd_odd: assumes "valid_unMultigraph G" "finite(edges G)" "finite(nodes G)" "(v, w, v')∈edges G" assumes parity_assms: "odd (degree v G)" "odd (degree v' G)" shows "num_of_odd_nodes G=num_of_odd_nodes(del_unEdge v w v' G)+2" proof - interpret G:valid_unMultigraph by fact have "v∉odd_nodes_set(del_unEdge v w v' G)" by (metis G.del_UnEdge_even assms(2) assms(4) parity_assms(1)) moreover have "v'∉odd_nodes_set(del_unEdge v w v' G)" by (metis G.del_UnEdge_even' assms(2) assms(4) parity_assms(2)) ultimately have vv'_disjoint: "{v,v'} ∩ odd_nodes_set(del_unEdge v w v' G) = {}" by (metis (full_types) Int_insert_left_if0 inf_bot_left) moreover have extra_odd_nodes:"{v,v'} ⊆ odd_nodes_set( G)" unfolding odd_nodes_set_def using ‹(v,w,v')∈edges G› by (metis (lifting) G.E_validD empty_subsetI insert_subset mem_Collect_eq parity_assms) moreover have "odd_nodes_set G -{v,v'}⊆odd_nodes_set (del_unEdge v w v' G) " proof fix x assume x_odd_set: "x ∈ odd_nodes_set G - {v, v'}" hence "degree x G = degree x (del_unEdge v w v' G)" by (metis Diff_iff G.degree_frame assms(2)) hence "odd(degree x (del_unEdge v w v' G))" using x_odd_set unfolding odd_nodes_set_def by auto moreover have "x ∈ nodes (del_unEdge v w v' G)" using x_odd_set unfolding odd_nodes_set_def by auto ultimately show "x ∈ odd_nodes_set (del_unEdge v w v' G)" unfolding odd_nodes_set_def by auto qed moreover have "odd_nodes_set (del_unEdge v w v' G) ⊆ odd_nodes_set G" proof fix x assume x_odd_set: "x ∈ odd_nodes_set (del_unEdge v w v' G)" hence "x∉{v,v'} ⟹ odd(degree x G)" using assms G.degree_frame unfolding odd_nodes_set_def by auto hence "x∉{v,v'} ⟹ x∈odd_nodes_set G" using x_odd_set del_UnEdge_node unfolding odd_nodes_set_def by auto moreover have "x∈{v,v'} ⟹ x∈odd_nodes_set G" using extra_odd_nodes by auto ultimately show "x ∈ odd_nodes_set G" by auto qed ultimately have "odd_nodes_set G=odd_nodes_set (del_unEdge v w v' G) ∪ {v,v'}" by auto thus ?thesis proof - assume "odd_nodes_set G=odd_nodes_set (del_unEdge v w v' G) ∪ {v,v'}" moreover have " odd_nodes_set (del_unEdge v w v' G) ∩ {v,v'} = {}" using vv'_disjoint by auto moreover have "finite(odd_nodes_set (del_unEdge v w v' G))" using assms del_UnEdge_node finite_subset unfolding odd_nodes_set_def by auto moreover have "finite {v,v'}" by auto ultimately have "card(odd_nodes_set G) = card(odd_nodes_set (del_unEdge v w v' G)) + card{v,v'}" unfolding num_of_odd_nodes_def using card_Un_disjoint by metis moreover have "v≠v'" using G.no_id ‹(v,w,v')∈edges G› by auto hence "card{v,v'}=2" by simp ultimately show ?thesis unfolding num_of_odd_nodes_def by simp qed qed lemma (in valid_unMultigraph) rem_UnPath_parity_v': assumes "finite E" "is_trail v ps v'" shows "v≠v' ⟷ (odd (degree v' (rem_unPath ps G)) = even(degree v' G))" using assms proof (induct ps arbitrary:v) case Nil thus ?case by (metis is_trail.simps(1) rem_unPath.simps(1)) next case (Cons x xs) print_cases obtain x1 x2 x3 where x: "x=(x1,x2,x3)" by (metis prod_cases3) hence rem_x:"odd (degree v' (rem_unPath (x#xs) G)) = odd(degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G)))" by (metis rem_unPath.simps(2) rem_unPath_com) have "x3=v' ⟹ ?case" proof (cases "v=v'") case True assume "x3=v'" have "x1=v'" using x by (metis Cons.prems(2) True is_trail.simps(2)) thus ?thesis using ‹x3=v'› by (metis Cons.prems(2) is_trail.simps(2) no_id x) next case False assume "x3=v'" have "odd (degree v' (rem_unPath (x # xs) G)) =odd(degree v' ( del_unEdge x1 x2 x3 (rem_unPath xs G)))" using rem_x . also have "...=odd(degree v' (rem_unPath xs G) - 1)" proof - have "finite (edges (rem_unPath xs G))" by (metis (full_types) assms(1) finite_Diff rem_unPath_edges) moreover have "(x1,x2,x3) ∈edges( rem_unPath xs G)" by (metis Cons.prems(2) distinct_elim is_trail.simps(2) x) moreover have "(x3,x2,x1) ∈edges( rem_unPath xs G)" by (metis Cons.prems(2) corres distinct_elim_rev is_trail.simps(2) x) ultimately show ?thesis by (metis ‹x3 = v'› del_edge_undirected_degree_minus delete_edge_sym x) qed also have "...=even(degree v' (rem_unPath xs G))" proof - have "(x1,x2,x3)∈E" by (metis Cons.prems(2) is_trail.simps(2) x) hence "(x3,x2,x1)∈edges (rem_unPath xs G)" by (metis Cons.prems(2) corres distinct_elim_rev x) hence "(x3,x2,x1)∈{e ∈ edges (rem_unPath xs G). fst e = v'}" using ‹x3=v'› by (metis (mono_tags) fst_conv mem_Collect_eq) moreover have "finite {e ∈ edges (rem_unPath xs G). fst e = v'}" using ‹finite E› by auto ultimately have "degree v' (rem_unPath xs G)≠0" unfolding degree_def by auto thus ?thesis by auto qed also have "...=even (degree v' G)" using ‹x3 = v'› assms by (metis (mono_tags) Cons.hyps Cons.prems(2) is_trail.simps(2) x) finally have "odd (degree v' (rem_unPath (x # xs) G))=even (degree v' G)" . thus ?thesis by (metis False) qed moreover have "x3≠v'⟹?case" proof (cases "v=v'") case True assume "x3≠v'" have "odd (degree v' (rem_unPath (x # xs) G)) =odd(degree v' ( del_unEdge x1 x2 x3 (rem_unPath xs G)))" using rem_x . also have "...=odd(degree v' (rem_unPath xs G) - 1)" proof - have "finite (edges (rem_unPath xs G))" by (metis (full_types) assms(1) finite_Diff rem_unPath_edges) moreover have "(x1,x2,x3) ∈edges( rem_unPath xs G)" by (metis Cons.prems(2) distinct_elim is_trail.simps(2) x) moreover have "(x3,x2,x1) ∈edges( rem_unPath xs G)" by (metis Cons.prems(2) corres distinct_elim_rev is_trail.simps(2) x) ultimately show ?thesis using True x by (metis Cons.prems(2) del_edge_undirected_degree_minus is_trail.simps(2)) qed also have "...=even(degree v' (rem_unPath xs G))" proof - have "(x1,x2,x3)∈E" by (metis Cons.prems(2) is_trail.simps(2) x) hence "(x1,x2,x3)∈edges (rem_unPath xs G)" by (metis Cons.prems(2) distinct_elim x) hence "(x1,x2,x3)∈{e ∈ edges (rem_unPath xs G). fst e = v'}" using ‹v=v'› x Cons by (metis (lifting, mono_tags) fst_conv is_trail.simps(2) mem_Collect_eq) moreover have "finite {e ∈ edges (rem_unPath xs G). fst e = v'}" using ‹finite E› by auto ultimately have "degree v' (rem_unPath xs G)≠0" unfolding degree_def by auto thus ?thesis by auto qed also have "...≠even (degree v' G)" using ‹x3 ≠ v'› assms by (metis Cons.hyps Cons.prems(2)is_trail.simps(2) x) finally have "odd (degree v' (rem_unPath (x # xs) G))≠even (degree v' G)" . thus ?thesis by (metis True) next case False assume "x3≠v'" have "odd (degree v' (rem_unPath (x # xs) G)) =odd(degree v' ( del_unEdge x1 x2 x3 (rem_unPath xs G)))" using rem_x . also have "...=odd(degree v' (rem_unPath xs G))" proof - have "v=x1" by (metis Cons.prems(2) is_trail.simps(2) x) hence "v'∉{x1,x3}" by (metis (mono_tags) False ‹x3 ≠ v'› empty_iff insert_iff) moreover have "valid_unMultigraph (rem_unPath xs G)" using valid_unMultigraph_axioms by auto moreover have "finite (edges (rem_unPath xs G))" by (metis (full_types) assms(1) finite_Diff rem_unPath_edges) ultimately have "degree v' (del_unEdge x1 x2 x3 (rem_unPath xs G)) =degree v' (rem_unPath xs G)" using degree_frame by (metis valid_unMultigraph.degree_frame) thus ?thesis by simp qed also have "...=even (degree v' G)" using assms x ‹x3 ≠ v'› by (metis Cons.hyps Cons.prems(2) is_trail.simps(2)) finally have "odd (degree v' (rem_unPath (x # xs) G))=even (degree v' G)" . thus ?thesis by (metis False) qed ultimately show ?case by auto qed lemma (in valid_unMultigraph) rem_UnPath_parity_v: assumes "finite E" "is_trail v ps v'" shows "v≠v' ⟷ (odd (degree v (rem_unPath ps G)) = even(degree v G))" by (metis assms is_trail_rev rem_UnPath_parity_v' rem_unPath_graph) lemma (in valid_unMultigraph) rem_UnPath_parity_others: assumes "finite E" "is_trail v ps v'" "n∉{v,v'}" shows " even (degree n (rem_unPath ps G)) = even(degree n G)" using assms proof (induct ps arbitrary: v) case Nil thus ?case by auto next case (Cons x xs) obtain x1 x2 x3 where x:"x=(x1,x2,x3)" by (metis prod_cases3) hence "even (degree n (rem_unPath (x#xs) G))= even (degree n ( del_unEdge x1 x2 x3 (rem_unPath xs G)))" by (metis rem_unPath.simps(2) rem_unPath_com) have "n=x3 ⟹?case" proof - assume "n=x3" have "even (degree n (rem_unPath (x#xs) G))= even (degree n ( del_unEdge x1 x2 x3 (rem_unPath xs G)))" by (metis rem_unPath.simps(2) rem_unPath_com x) also have "...=even(degree n (rem_unPath xs G) - 1)" proof - have "finite (edges (rem_unPath xs G))" by (metis (full_types) assms(1) finite_Diff rem_unPath_edges) moreover have "(x1,x2,x3) ∈edges( rem_unPath xs G)" by (metis Cons.prems(2) distinct_elim is_trail.simps(2) x) moreover have "(x3,x2,x1) ∈edges( rem_unPath xs G)" by (metis Cons.prems(2) corres distinct_elim_rev is_trail.simps(2) x) ultimately show ?thesis using ‹n = x3› del_edge_undirected_degree_minus' by auto qed also have "...=odd(degree n (rem_unPath xs G))" proof - have "(x1,x2,x3)∈E" by (metis Cons.prems(2) is_trail.simps(2) x) hence "(x3,x2,x1)∈edges (rem_unPath xs G)" by (metis Cons.prems(2) corres distinct_elim_rev x) hence "(x3,x2,x1)∈{e ∈ edges (rem_unPath xs G). fst e = n}" using ‹n=x3› by (metis (mono_tags) fst_conv mem_Collect_eq) moreover have "finite {e ∈ edges (rem_unPath xs G). fst e = n}" using ‹finite E› by auto ultimately have "degree n (rem_unPath xs G)≠0" unfolding degree_def by auto thus ?thesis by auto qed also have "...=even(degree n G)" proof - have "x3≠v'" by (metis ‹n = x3› assms(3) insert_iff) hence "odd (degree x3 (rem_unPath xs G)) = even(degree x3 G)" using Cons assms by (metis is_trail.simps(2) rem_UnPath_parity_v x) thus ?thesis using ‹n=x3› by auto qed finally have "even (degree n (rem_unPath (x#xs) G))=even(degree n G)" . thus ?thesis . qed moreover have "n≠x3 ⟹?case" proof - assume "n≠x3" have "even (degree n (rem_unPath (x#xs) G))= even (degree n ( del_unEdge x1 x2 x3 (rem_unPath xs G)))" by (metis rem_unPath.simps(2) rem_unPath_com x) also have "...=even(degree n (rem_unPath xs G))" proof - have "v=x1" by (metis Cons.prems(2) is_trail.simps(2) x) hence "n∉{x1,x3}" by (metis Cons.prems(3) ‹n ≠ x3› insertE insertI1 singletonE) moreover have "valid_unMultigraph (rem_unPath xs G)" using valid_unMultigraph_axioms by auto moreover have "finite (edges (rem_unPath xs G))" by (metis (full_types) assms(1) finite_Diff rem_unPath_edges) ultimately have "degree n (del_unEdge x1 x2 x3 (rem_unPath xs G)) =degree n (rem_unPath xs G)" using degree_frame by (metis valid_unMultigraph.degree_frame) thus ?thesis by simp qed also have "...=even(degree n G)" using Cons assms ‹n ≠ x3› x by auto finally have "even (degree n (rem_unPath (x#xs) G))=even(degree n G)" . thus ?thesis . qed ultimately show ?case by auto qed lemma (in valid_unMultigraph) rem_UnPath_even: assumes "finite E" "finite V" "is_trail v ps v'" assumes parity_assms: "even (degree v' G)" shows "num_of_odd_nodes (rem_unPath ps G) = num_of_odd_nodes G + (if even (degree v G)∧ v≠v' then 2 else 0)" using assms proof (induct ps arbitrary:v) case Nil thus ?case by auto next case (Cons x xs) obtain x1 x2 x3 where x:"x=(x1,x2,x3)" by (metis prod_cases3) have fin_nodes: "finite (nodes (rem_unPath xs G))" using Cons by auto have fin_edges: "finite (edges (rem_unPath xs G))" using Cons by auto have valid_rem_xs: "valid_unMultigraph (rem_unPath xs G)" using valid_unMultigraph_axioms by auto have x_in:"(x1,x2,x3)∈edges (rem_unPath xs G)" by (metis (full_types) Cons.prems(3) distinct_elim is_trail.simps(2) x) have "even (degree x1 (rem_unPath xs G)) ⟹ even(degree x3 (rem_unPath xs G)) ⟹ ?case" proof - assume parity_x1_x3: "even (degree x1 (rem_unPath xs G))" "even(degree x3 (rem_unPath xs G))" have "num_of_odd_nodes (rem_unPath (x#xs) G)= num_of_odd_nodes (del_unEdge x1 x2 x3 (rem_unPath xs G))" by (metis rem_unPath.simps(2) rem_unPath_com x) also have "... =num_of_odd_nodes (rem_unPath xs G)+2" using parity_x1_x3 fin_nodes fin_edges valid_rem_xs x_in del_UnEdge_even_even by metis also have "...=num_of_odd_nodes G+(if even(degree x3 G) ∧ x3≠v' then 2 else 0 )+2" using Cons.hyps[OF ‹finite E› ‹finite V›, of x3] ‹is_trail v (x # xs) v'› ‹even (degree v' G)› x by auto also have "...=num_of_odd_nodes G+2" proof - have "even(degree x3 G) ∧ x3≠v' ⟷ odd (degree x3 (rem_unPath xs G))" using Cons.prems assms by (metis is_trail.simps(2) parity_x1_x3(2) rem_UnPath_parity_v x) thus ?thesis using parity_x1_x3(2) by auto qed also have "...=num_of_odd_nodes G+(if even(degree v G) ∧ v≠v' then 2 else 0)" proof - have "x1≠x3" by (metis valid_rem_xs valid_unMultigraph.no_id x_in) moreover hence "x1≠v'" using Cons assms by (metis is_trail.simps(2) parity_x1_x3(1) rem_UnPath_parity_v' x) ultimately have "x1∉{x3,v'}" by auto hence "even(degree x1 G)" using Cons.prems(3) assms(1) assms(2) parity_x1_x3(1) by (metis (full_types) is_trail.simps(2) rem_UnPath_parity_others x) hence "even(degree x1 G) ∧ x1≠v'" using ‹x1 ≠ v'› by auto hence "even(degree v G) ∧ v≠v'" by (metis Cons.prems(3) is_trail.simps(2) x) thus ?thesis by auto qed finally have "num_of_odd_nodes (rem_unPath (x#xs) G)= num_of_odd_nodes G+(if even(degree v G) ∧ v≠v' then 2 else 0)" . thus ?thesis . qed moreover have "even (degree x1 (rem_unPath xs G)) ⟹ odd(degree x3 (rem_unPath xs G)) ⟹ ?case" proof - assume parity_x1_x3: "even (degree x1 (rem_unPath xs G))" "odd (degree x3 (rem_unPath xs G))" have "num_of_odd_nodes (rem_unPath (x#xs) G)= num_of_odd_nodes (del_unEdge x1 x2 x3 (rem_unPath xs G))" by (metis rem_unPath.simps(2) rem_unPath_com x) also have "... =num_of_odd_nodes (rem_unPath xs G)" using parity_x1_x3 fin_nodes fin_edges valid_rem_xs x_in by (metis del_UnEdge_even_odd) also have "...=num_of_odd_nodes G+(if even(degree x3 G) ∧ x3≠v' then 2 else 0 )" using Cons.hyps Cons.prems(3) assms(1) assms(2) parity_assms x by auto also have "...=num_of_odd_nodes G+2" proof - have "even(degree x3 G) ∧ x3≠v' ⟷ odd (degree x3 (rem_unPath xs G))" using Cons.prems assms by (metis is_trail.simps(2) parity_x1_x3(2) rem_UnPath_parity_v x) thus ?thesis using parity_x1_x3(2) by auto qed also have "...=num_of_odd_nodes G+(if even(degree v G) ∧ v≠v' then 2 else 0)" proof - have "x1≠x3" by (metis valid_rem_xs valid_unMultigraph.no_id x_in) moreover hence "x1≠v'" using Cons assms by (metis is_trail.simps(2) parity_x1_x3(1) rem_UnPath_parity_v' x) ultimately have "x1∉{x3,v'}" by auto hence "even(degree x1 G)" using Cons.prems(3) assms(1) assms(2) parity_x1_x3(1) by (metis (full_types) is_trail.simps(2) rem_UnPath_parity_others x) hence "even(degree x1 G) ∧ x1≠v'" using ‹x1 ≠ v'› by auto hence "even(degree v G) ∧ v≠v'" by (metis Cons.prems(3) is_trail.simps(2) x) thus ?thesis by auto qed finally have "num_of_odd_nodes (rem_unPath (x#xs) G)= num_of_odd_nodes G+(if even(degree v G) ∧ v≠v' then 2 else 0)" . thus ?thesis . qed moreover have "odd (degree x1 (rem_unPath xs G)) ⟹ even(degree x3 (rem_unPath xs G)) ⟹ ?case" proof - assume parity_x1_x3: "odd (degree x1 (rem_unPath xs G))" "even (degree x3 (rem_unPath xs G))" have "num_of_odd_nodes (rem_unPath (x#xs) G)= num_of_odd_nodes (del_unEdge x1 x2 x3 (rem_unPath xs G))" by (metis rem_unPath.simps(2) rem_unPath_com x) also have "... =num_of_odd_nodes (rem_unPath xs G)" using parity_x1_x3 fin_nodes fin_edges valid_rem_xs x_in by (metis del_UnEdge_odd_even) also have "...=num_of_odd_nodes G+(if even(degree x3 G) ∧ x3≠v' then 2 else 0 )" using Cons.hyps Cons.prems(3) assms(1) assms(2) parity_assms x by auto also have "...=num_of_odd_nodes G" proof - have "even(degree x3 G) ∧ x3≠v' ⟷ odd (degree x3 (rem_unPath xs G))" using Cons.prems assms by (metis is_trail.simps(2) parity_x1_x3(2) rem_UnPath_parity_v x) thus ?thesis using parity_x1_x3(2) by auto qed also have "...=num_of_odd_nodes G+(if even(degree v G) ∧ v≠v' then 2 else 0)" proof (cases "v≠v'") case True have "x1≠x3" by (metis valid_rem_xs valid_unMultigraph.no_id x_in) moreover have "is_trail x3 xs v' " by (metis Cons.prems(3) is_trail.simps(2) x) ultimately have "odd (degree x1 (rem_unPath xs G)) ⟷ odd(degree x1 G)" using True parity_x1_x3(1) rem_UnPath_parity_others x Cons.prems(3) assms(1) assms(2) by auto hence "odd(degree x1 G)" by (metis parity_x1_x3(1)) thus ?thesis by (metis (mono_tags) Cons.prems(3) Nat.add_0_right is_trail.simps(2) x) next case False then show ?thesis by auto qed finally have "num_of_odd_nodes (rem_unPath (x#xs) G)= num_of_odd_nodes G+(if even(degree v G) ∧ v≠v' then 2 else 0)" . thus ?thesis . qed moreover have "odd (degree x1 (rem_unPath xs G)) ⟹ odd(degree x3 (rem_unPath xs G)) ⟹ ?case" proof - assume parity_x1_x3: "odd (degree x1 (rem_unPath xs G))" "odd (degree x3 (rem_unPath xs G))" have "num_of_odd_nodes (rem_unPath (x#xs) G)= num_of_odd_nodes (del_unEdge x1 x2 x3 (rem_unPath xs G))" by (metis rem_unPath.simps(2) rem_unPath_com x) also have "... =num_of_odd_nodes (rem_unPath xs G)-(2::nat)" using del_UnEdge_odd_odd by (metis add_implies_diff fin_edges fin_nodes parity_x1_x3 valid_rem_xs x_in) also have "...=num_of_odd_nodes G+(if even(degree x3 G) ∧ x3≠v' then 2 else 0 )-(2::nat)" using Cons assms by (metis is_trail.simps(2) x) also have "...=num_of_odd_nodes G" proof - have "even(degree x3 G) ∧ x3≠v' ⟷ odd (degree x3 (rem_unPath xs G))" using Cons.prems assms by (metis is_trail.simps(2) parity_x1_x3(2) rem_UnPath_parity_v x) thus ?thesis using parity_x1_x3(2) by auto qed also have "...=num_of_odd_nodes G+(if even(degree v G) ∧ v≠v' then 2 else 0)" proof (cases "v≠v'") case True have "x1≠x3" by (metis valid_rem_xs valid_unMultigraph.no_id x_in) moreover have "is_trail x3 xs v' " by (metis Cons.prems(3) is_trail.simps(2) x) ultimately have "odd (degree x1 (rem_unPath xs G)) ⟷ odd(degree x1 G)" using True Cons.prems(3) assms(1) assms(2) parity_x1_x3(1) rem_UnPath_parity_others x by auto hence "odd(degree x1 G)" by (metis parity_x1_x3(1)) thus ?thesis by (metis (mono_tags) Cons.prems(3) Nat.add_0_right is_trail.simps(2) x) next case False thus ?thesis by (metis (mono_tags) add_0_iff) qed finally have "num_of_odd_nodes (rem_unPath (x#xs) G)= num_of_odd_nodes G+(if even(degree v G) ∧ v≠v' then 2 else 0)" . thus ?thesis . qed ultimately show ?case by metis qed lemma (in valid_unMultigraph) rem_UnPath_odd: assumes "finite E" "finite V" "is_trail v ps v'" assumes parity_assms: "odd (degree v' G)" shows "num_of_odd_nodes (rem_unPath ps G) = num_of_odd_nodes G + (if odd (degree v G)∧ v≠v' then -2 else 0)" using assms proof (induct ps arbitrary:v) case Nil thus ?case by auto next case (Cons x xs) obtain x1 x2 x3 where x:"x=(x1,x2,x3)" by (metis prod_cases3) have fin_nodes: "finite (nodes (rem_unPath xs G))" using Cons by auto have fin_edges: "finite (edges (rem_unPath xs G))" using Cons by auto have valid_rem_xs: "valid_unMultigraph (rem_unPath xs G)" using valid_unMultigraph_axioms by auto have x_in:"(x1,x2,x3)∈edges (rem_unPath xs G)" by (metis (full_types) Cons.prems(3) distinct_elim is_trail.simps(2) x) have "even (degree x1 (rem_unPath xs G)) ⟹ even(degree x3 (rem_unPath xs G)) ⟹ ?case" proof - assume parity_x1_x3: "even (degree x1 (rem_unPath xs G))" "even (degree x3 (rem_unPath xs G))" have "num_of_odd_nodes (rem_unPath (x#xs) G)= num_of_odd_nodes (del_unEdge x1 x2 x3 (rem_unPath xs G))" by (metis rem_unPath.simps(2) rem_unPath_com x) also have "... =num_of_odd_nodes (rem_unPath xs G)+2" using parity_x1_x3 fin_nodes fin_edges valid_rem_xs x_in del_UnEdge_even_even by metis also have "...=num_of_odd_nodes G+(if odd(degree x3 G) ∧ x3≠v' then - 2 else 0 )+2" using Cons.hyps[OF ‹finite E› ‹finite V›,of x3] ‹is_trail v (x # xs) v'› ‹odd (degree v' G)› x by auto also have "...=num_of_odd_nodes G" proof - have "odd (degree x3 G) ∧ x3≠v' ⟷ even (degree x3 (rem_unPath xs G))" using Cons.prems assms by (metis is_trail.simps(2) parity_x1_x3(2) rem_UnPath_parity_v x) thus ?thesis using parity_x1_x3(2) by auto qed also have "...=num_of_odd_nodes G+(if odd(degree v G) ∧ v≠v' then -2 else 0)" proof (cases "v≠v'") case True have "x1≠x3" by (metis valid_rem_xs valid_unMultigraph.no_id x_in) moreover have "is_trail x3 xs v' " by (metis Cons.prems(3) is_trail.simps(2) x) ultimately have "even (degree x1 (rem_unPath xs G)) ⟷ even (degree x1 G)" using True Cons.prems(3) assms(1) assms(2) parity_x1_x3(1) rem_UnPath_parity_others x by auto hence "even (degree x1 G)" by (metis parity_x1_x3(1)) thus ?thesis by (metis (opaque_lifting, mono_tags) Cons.prems(3) is_trail.simps(2) monoid_add_class.add.right_neutral x) next case False then show ?thesis by auto qed finally have "num_of_odd_nodes (rem_unPath (x#xs) G)= num_of_odd_nodes G+(if odd(degree v G) ∧ v≠v' then -2 else 0)" . thus ?thesis . qed moreover have "even (degree x1 (rem_unPath xs G)) ⟹ odd(degree x3 (rem_unPath xs G)) ⟹ ?case" proof - assume parity_x1_x3: "even (degree x1 (rem_unPath xs G))" "odd (degree x3 (rem_unPath xs G))" have "num_of_odd_nodes (rem_unPath (x#xs) G)= num_of_odd_nodes (del_unEdge x1 x2 x3 (rem_unPath xs G))" by (metis rem_unPath.simps(2) rem_unPath_com x) also have "... =num_of_odd_nodes (rem_unPath xs G)" using parity_x1_x3 fin_nodes fin_edges valid_rem_xs x_in by (metis del_UnEdge_even_odd) also have "...=num_of_odd_nodes G+(if odd(degree x3 G) ∧ x3≠v' then - 2 else 0 )" using Cons.hyps[OF ‹finite E› ‹finite V›, of x3] Cons.prems(3) assms(1) assms(2) parity_assms x by auto also have "...=num_of_odd_nodes G" proof - have "odd(degree x3 G) ∧ x3≠v' ⟷ even (degree x3 (rem_unPath xs G))" using Cons.prems assms by (metis is_trail.simps(2) parity_x1_x3(2) rem_UnPath_parity_v x) thus ?thesis using parity_x1_x3(2) by auto qed also have "...= num_of_odd_nodes G+(if odd(degree v G) ∧ v≠v' then -2 else 0)" proof (cases "v≠v'") case True have "x1≠x3" by (metis valid_rem_xs valid_unMultigraph.no_id x_in) moreover have "is_trail x3 xs v' " by (metis Cons.prems(3) is_trail.simps(2) x) ultimately have "even (degree x1 (rem_unPath xs G)) ⟷ even (degree x1 G)" using True Cons.prems(3) assms(1) assms(2) parity_x1_x3(1) rem_UnPath_parity_others x by auto hence "even (degree x1 G)" by (metis parity_x1_x3(1)) with Cons.prems(3) x show ?thesis by auto next case False then show ?thesis by auto qed finally have "num_of_odd_nodes (rem_unPath (x#xs) G)= num_of_odd_nodes G+(if odd(degree v G) ∧ v≠v' then -2 else 0)" . thus ?thesis . qed moreover have "odd (degree x1 (rem_unPath xs G)) ⟹ even(degree x3 (rem_unPath xs G)) ⟹ ?case" proof - assume parity_x1_x3: "odd (degree x1 (rem_unPath xs G))" "even (degree x3 (rem_unPath xs G))" have "num_of_odd_nodes (rem_unPath (x#xs) G)= num_of_odd_nodes (del_unEdge x1 x2 x3 (rem_unPath xs G))" by (metis rem_unPath.simps(2) rem_unPath_com x) also have "... =num_of_odd_nodes (rem_unPath xs G)" using parity_x1_x3 fin_nodes fin_edges valid_rem_xs x_in by (metis del_UnEdge_odd_even) also have "...=num_of_odd_nodes G+(if odd(degree x3 G) ∧ x3≠v' then -2 else 0 )" using Cons.hyps Cons.prems(3) assms(1) assms(2) parity_assms x by auto also have "...=num_of_odd_nodes G + (- 2)" proof - have "odd(degree x3 G) ∧ x3≠v' ⟷ even (degree x3 (rem_unPath xs G))" using Cons.prems assms by (metis is_trail.simps(2) parity_x1_x3(2) rem_UnPath_parity_v x) hence "odd(degree x3 G) ∧ x3≠v'" by (metis parity_x1_x3(2)) thus ?thesis by auto qed also have "...=num_of_odd_nodes G+(if odd(degree v G) ∧ v≠v' then -2 else 0)" proof - have "x1≠x3" by (metis valid_rem_xs valid_unMultigraph.no_id x_in) moreover hence "x1≠v'" using Cons assms by (metis is_trail.simps(2) parity_x1_x3(1) rem_UnPath_parity_v' x) ultimately have "x1∉{x3,v'}" by auto hence "odd(degree x1 G)" using Cons.prems(3) assms(1) assms(2) parity_x1_x3(1) by (metis (full_types) is_trail.simps(2) rem_UnPath_parity_others x) hence "odd(degree x1 G) ∧ x1≠v'" using ‹x1 ≠ v'› by auto hence "odd(degree v G) ∧ v≠v'" by (metis Cons.prems(3) is_trail.simps(2) x) thus ?thesis by auto qed finally have "num_of_odd_nodes (rem_unPath (x#xs) G)= num_of_odd_nodes G+(if odd(degree v G) ∧ v≠v' then -2 else 0)" . thus ?thesis . qed moreover have "odd (degree x1 (rem_unPath xs G)) ⟹ odd(degree x3 (rem_unPath xs G)) ⟹ ?case" proof - assume parity_x1_x3: "odd (degree x1 (rem_unPath xs G))" "odd (degree x3 (rem_unPath xs G))" have "num_of_odd_nodes (rem_unPath (x#xs) G)= num_of_odd_nodes (del_unEdge x1 x2 x3 (rem_unPath xs G))" by (metis rem_unPath.simps(2) rem_unPath_com x) also have "... =num_of_odd_nodes (rem_unPath xs G)-(2::nat)" using del_UnEdge_odd_odd by (metis add_implies_diff fin_edges fin_nodes parity_x1_x3 valid_rem_xs x_in) also have "...=num_of_odd_nodes G -(2::nat)" proof - have "odd(degree x3 G) ∧ x3≠v' ⟷ even (degree x3 (rem_unPath xs G))" using Cons.prems assms by (metis is_trail.simps(2) parity_x1_x3(2) rem_UnPath_parity_v x) hence "¬(odd(degree x3 G) ∧ x3≠v')" by (metis parity_x1_x3(2)) have "num_of_odd_nodes (rem_unPath xs G)= num_of_odd_nodes G+(if odd(degree x3 G) ∧ x3≠v' then -2 else 0)" by (metis Cons.hyps Cons.prems(3) assms(1) assms(2) is_trail.simps(2) parity_assms x) thus ?thesis using ‹¬ (odd (degree x3 G) ∧ x3 ≠ v')› by auto qed also have "...=num_of_odd_nodes G+(if odd(degree v G) ∧ v≠v' then -2 else 0)" proof - have "x1≠x3" by (metis valid_rem_xs valid_unMultigraph.no_id x_in) moreover hence "x1≠v'" using Cons assms by (metis is_trail.simps(2) parity_x1_x3(1) rem_UnPath_parity_v' x) ultimately have "x1∉{x3,v'}" by auto hence "odd(degree x1 G)" using Cons.prems(3) assms(1) assms(2) parity_x1_x3(1) by (metis (full_types) is_trail.simps(2) rem_UnPath_parity_others x) hence "odd(degree x1 G) ∧ x1≠v'" using ‹x1 ≠ v'› by auto hence "odd(degree v G) ∧ v≠v'" by (metis Cons.prems(3) is_trail.simps(2) x) hence "v∈odd_nodes_set G" using Cons.prems(3) E_validD(1) x unfolding odd_nodes_set_def by auto moreover have "v'∈odd_nodes_set G" using is_path_memb[OF is_trail_intro[OF assms(3)]] parity_assms unfolding odd_nodes_set_def by auto ultimately have "{v,v'}⊆odd_nodes_set G" by auto moreover have "v≠v'" by (metis ‹odd (degree v G) ∧ v ≠ v'›) hence "card{v,v'}=2" by auto moreover have "finite(odd_nodes_set G)" using ‹finite V› unfolding odd_nodes_set_def by auto ultimately have "num_of_odd_nodes G≥2" by (metis card_mono num_of_odd_nodes_def) thus ?thesis using ‹odd (degree v G) ∧ v ≠ v'› by auto qed finally have "num_of_odd_nodes (rem_unPath (x#xs) G)= num_of_odd_nodes G+(if odd(degree v G) ∧ v≠v' then -2 else 0)" . thus ?thesis . qed ultimately show ?case by metis qed lemma (in valid_unMultigraph) rem_UnPath_cycle: assumes "finite E" "finite V" "is_trail v ps v'" "v=v'" shows "num_of_odd_nodes (rem_unPath ps G) = num_of_odd_nodes G" (is "?L=?R") proof (cases "even(degree v' G)") case True hence "?L = num_of_odd_nodes G + (if even (degree v G)∧ v≠v' then 2 else 0)" by (metis assms(1) assms(2) assms(3) rem_UnPath_even) with assms show ?thesis by auto next case False hence "?L = num_of_odd_nodes G + (if odd (degree v G)∧ v≠v'