section ‹Graphs› theory Graph imports Main begin text ‹ Let us now define digraphs, graphs, walks, paths, and related concepts. › text ‹@{typ 'a} is the vertex type.› type_synonym 'a Edge = "'a × 'a" type_synonym 'a Walk = "'a list" record 'a Graph = verts :: "'a set" ("Vı") arcs :: "'a Edge set" ("Eı") abbreviation is_arc :: "('a, 'b) Graph_scheme ⇒ 'a ⇒ 'a ⇒ bool" (infixl "→ı" 60) where "v →⇘G⇙ w ≡ (v,w) ∈ E⇘G⇙" text ‹ We consider directed and undirected finite graphs. Our graphs do not have multi-edges. › locale Digraph = fixes G :: "('a, 'b) Graph_scheme" (structure) assumes finite_vertex_set: "finite V" and valid_edge_set: "E ⊆ V × V" context Digraph begin lemma finite_edge_set [simp]: "finite E" using finite_vertex_set valid_edge_set by (simp add: finite_subset) lemma edges_are_in_V: assumes "v→w" shows "v ∈ V" "w ∈ V" using assms valid_edge_set by blast+ subsection ‹Walks› text ‹A walk is sequence of vertices connected by edges.› inductive walk :: "'a Walk ⇒ bool" where Nil [simp]: "walk []" | Singleton [simp]: "v ∈ V ⟹ walk [v]" | Cons: "v→w ⟹ walk (w # vs) ⟹ walk (v # w # vs)" text ‹ Show a few composition/decomposition lemmas for walks. These will greatly simplify the proofs that follow.› lemma walk_2 [simp]: "v→w ⟹ walk [v,w]" by (simp add: edges_are_in_V(2) walk.intros(3)) lemma walk_comp: "⟦ walk xs; walk ys; xs = Nil ∨ ys = Nil ∨ last xs→hd ys ⟧ ⟹ walk (xs @ ys)" by (induct rule: walk.induct, simp_all add: walk.intros(3)) (metis list.exhaust_sel walk.intros(2) walk.intros(3)) lemma walk_tl: "walk xs ⟹ walk (tl xs)" by (induct rule: walk.induct) simp_all lemma walk_drop: "walk xs ⟹ walk (drop n xs)" by (induct n, simp) (metis drop_Suc tl_drop walk_tl) lemma walk_take: "walk xs ⟹ walk (take n xs)" by (induct arbitrary: n rule: walk.induct) (simp, metis Digraph.walk.simps Digraph_axioms take_Cons' take_eq_Nil, metis Digraph.walk.simps Digraph_axioms edges_are_in_V(1) take_Cons') lemma walk_decomp: assumes "walk (xs @ ys)" shows "walk xs" "walk ys" using assms append_eq_conv_conj[of xs ys "xs @ ys"] walk_take walk_drop by metis+ lemma walk_in_V: "walk xs ⟹ set xs ⊆ V" by (induct rule: walk.induct; simp add: edges_are_in_V) lemma walk_first_edge: "walk (v # w # xs) ⟹ v→w" using walk.cases by fastforce lemma walk_first_edge': "⟦ walk (v # xs); xs ≠ Nil ⟧ ⟹ v→hd xs" using walk_first_edge by (metis list.exhaust_sel) lemma walk_middle_edge: "walk (xs @ v # w # ys) ⟹ v→w" by (induct "xs @ v # w # ys" arbitrary: xs rule: walk.induct, simp, simp) (metis list.sel(1,3) self_append_conv2 tl_append2) lemma walk_last_edge: "⟦ walk (xs @ ys); xs ≠ Nil; ys ≠ Nil ⟧ ⟹ last xs→hd ys" using walk_middle_edge[of "butlast xs" "last xs" "hd ys" "tl ys"] by (metis Cons_eq_appendI append_butlast_last_id append_eq_append_conv2 list.exhaust_sel self_append_conv) subsection ‹Paths› text ‹ A path is a walk without repeated vertices. This is simple enough, so most of the above lemmas transfer directly to paths. › abbreviation path :: "'a Walk ⇒ bool" where "path xs ≡ walk xs ∧ distinct xs" lemma path_singleton [simp]: "v ∈ V ⟹ path [v]" by simp lemma path_2 [simp]: "⟦ v→w; v ≠ w ⟧ ⟹ path [v,w]" by simp lemma path_cons: "⟦ path xs; xs ≠ Nil; v→hd xs; v ∉ set xs ⟧ ⟹ path (v # xs)" by (metis distinct.simps(2) list.exhaust_sel walk.Cons) lemma path_comp: "⟦ walk xs; walk ys; xs = Nil ∨ ys = Nil ∨ last xs→hd ys; distinct (xs @ ys) ⟧ ⟹ path (xs @ ys)" using walk_comp by blast lemma path_tl: "path xs ⟹ path (tl xs)" by (simp add: distinct_tl walk_tl) lemma path_drop: "path xs ⟹ path (drop n xs)" by (simp add: walk_drop) lemma path_take: "path xs ⟹ path (take n xs)" by (simp add: walk_take) lemma path_decomp: assumes "path (xs @ ys)" shows "path xs" "path ys" using walk_decomp assms distinct_append by blast+ lemma path_decomp': "path (xs @ x # ys) ⟹ path (xs @ [x])" by (metis Singleton distinct.simps(2) distinct1_rotate edges_are_in_V(1) list.discI list.sel(1) not_distinct_conv_prefix path_decomp(1) rotate1.simps(2) walk_comp walk_decomp(2) walk_first_edge' walk_last_edge) lemma path_in_V: "path xs ⟹ set xs ⊆ V" by (simp add: walk_in_V) lemma path_length: "path xs ⟹ length xs ≤ card V" by (metis card_mono distinct_card finite_vertex_set path_in_V) lemma path_first_edge: "path (v # w # xs) ⟹ v→w" using walk_first_edge by blast lemma path_first_edge': "⟦ path (v # xs); xs ≠ Nil ⟧ ⟹ v→hd xs" using walk_first_edge' by blast lemma path_middle_edge: "path (xs @ v # w # ys) ⟹ v → w" using walk_middle_edge by blast lemma path_first_vertex: "path (x # xs) ⟹ x ∉ set xs" by simp lemma path_disjoint: "⟦ path (xs @ ys); xs ≠ Nil; x ∈ set xs ⟧ ⟹ x ∉ set ys" by auto subsection ‹The Set of All Paths› definition all_paths where "all_paths ≡ { xs | xs. path xs }" text ‹ Because paths have no repeated vertices, every graph has at most finitely many distinct paths. This will be useful later to easily derive that any set of paths is finite. › lemma finitely_many_paths: "finite all_paths" proof- have "all_paths ⊆ {xs. set xs ⊆ V ∧ length xs ≤ card V}" unfolding all_paths_def using path_length by (simp add: Collect_mono path_in_V) thus ?thesis using finite_lists_length_le[OF finite_vertex_set] walk_in_V infinite_super by blast qed end ― ‹context Digraph› text ‹We introduce shorthand notation for a path connecting two vertices.› definition path_from_to :: "('a, 'b) Graph_scheme ⇒ 'a ⇒ 'a Walk ⇒ 'a ⇒ bool" ("_ ↝_↝ı _" [71, 71, 71] 70) where "path_from_to G v xs w ≡ Digraph.path G xs ∧ xs ≠ Nil ∧ hd xs = v ∧ last xs = w" context Digraph begin lemma path_from_toI [intro]: "⟦ path xs; xs ≠ Nil; hd xs = v; last xs = w ⟧ ⟹ v ↝xs↝ w" and path_from_toE [dest]: "v ↝xs↝ w ⟹ path xs ∧ xs ≠ Nil ∧ hd xs = v ∧ last xs = w" unfolding path_from_to_def by blast+ lemma path_from_to_ends: "v ↝(xs @ w # ys)↝ w ⟹ ys = Nil" by (metis path_from_toE distinct.simps(2) last.simps last_appendR last_in_set list.discI path_decomp(2)) lemma path_from_to_combine: assumes "v ↝(xs @ x # xs')↝ w" "v' ↝(ys @ x # ys')↝ w'" "set xs ∩ set ys' = {}" shows "v ↝(xs @ x # ys') ↝ w'" proof show "path (xs @ x # ys')" by (metis path_from_toE assms(1,2,3) disjoint_insert(1) distinct_append list.sel(1) list.set(2) list.simps(3) path_decomp(2) walk_comp walk_decomp(1) walk_last_edge) show "hd (xs @ x # ys') = v" by (metis path_from_toE assms(1) hd_append list.sel(1)) show "last (xs @ x # ys') = w'" using assms(2) by auto qed simp lemma path_from_to_first: "v ↝xs↝ w ⟹ v ∉ set (tl xs)" by (metis path_from_toE list.collapse path_first_vertex) lemma path_from_to_first': "v ↝(xs @ x # xs')↝ w ⟹ v ∉ set xs'" by (metis path_from_toE append_eq_append_conv2 distinct.simps(2) hd_append list.exhaust_sel list.sel(3) list.set_sel(1,2) list.simps(3) path_disjoint self_append_conv) lemma path_from_to_last: "v ↝xs↝ w ⟹ w ∉ set (butlast xs)" by (metis path_from_toE append_butlast_last_id distinct_append not_distinct_conv_prefix) lemma path_from_to_last': "v ↝(xs @ x # xs')↝ w ⟹ w ∉ set xs" by (metis path_from_toE bex_empty last_appendR last_in_set list.set(1) list.simps(3) path_disjoint) text ‹Every walk contains a path connecting the same vertices.› lemma walk_to_path: assumes "walk xs" "xs ≠ Nil" "hd xs = v" "last xs = w" shows "∃ys. v ↝ys↝ w ∧ set ys ⊆ set xs" proof- text ‹We prove this by removing loops from @{term xs} until @{term xs} is a path. We want to perform induction over @{term "length xs"}, but @{term xs} in @{term "set ys ⊆ set xs"} should not be part of the induction hypothesis. To accomplish this, we hide @{term "set xs"} behind a definition for this specific part of the goal.› define target_set where "target_set ≡ set xs" hence "set xs ⊆ target_set" by simp thus "∃ys. v ↝ys↝ w ∧ set ys ⊆ target_set" using assms proof (induct "length xs" arbitrary: xs rule: infinite_descent0) case (smaller n) then obtain xs where xs: "n = length xs" "walk xs" "xs ≠ Nil" "hd xs = v" "last xs = w" "set xs ⊆ target_set" and hyp: "¬(∃ys. v ↝ys↝ w ∧ set ys ⊆ target_set)" by blast text ‹If @{term xs} is not a path, then @{term xs} is not distinct and we can decompose it.› then obtain ys rest u where xs_decomp: "u ∈ set ys" "distinct ys" "xs = ys @ u # rest" using not_distinct_conv_prefix by (metis path_from_toI) text ‹@{term u} appears in @{term ys}, so we have a loop in @{term xs} starting from an occurrence of @{term u} in @{term ys} ending in the vertex @{term u} in @{term "u # rest"}. We define @{term zs} as @{term xs} without this loop.› obtain ys' ys_suffix where ys_decomp: "ys = ys' @ u # ys_suffix" by (meson split_list xs_decomp(1)) define zs where "zs ≡ ys' @ u # rest" have "walk zs" unfolding zs_def using xs(2) xs_decomp(3) ys_decomp by (metis walk_decomp list.sel(1) list.simps(3) walk_comp walk_last_edge) moreover have "length zs < n" unfolding zs_def by (simp add: xs(1) xs_decomp(3) ys_decomp) moreover have "hd zs = v" unfolding zs_def by (metis append_is_Nil_conv hd_append list.sel(1) xs(4) xs_decomp(3) ys_decomp) moreover have "last zs = w" unfolding zs_def using xs(5) xs_decomp(3) by auto moreover have "set zs ⊆ target_set" unfolding zs_def using xs(6) xs_decomp(3) ys_decomp by auto ultimately show ?case using zs_def hyp by blast qed simp qed subsection ‹Edges of Walks› text ‹The set of edges on a walk. Note that this is empty for walks of length 0 or 1.› definition edges_of_walk :: "'a Walk ⇒ 'a Edge set" where "edges_of_walk xs = { (v,w) | v w xs_pre xs_post. xs = xs_pre @ v # w # xs_post }" lemma edges_of_walkE: "(v,w) ∈ edges_of_walk xs ⟹ ∃xs_pre xs_post. xs = xs_pre @ v # w # xs_post" unfolding edges_of_walk_def by blast lemma edges_of_walk_in_E: "walk xs ⟹ edges_of_walk xs ⊆ E" unfolding edges_of_walk_def using walk_middle_edge by auto lemma edges_of_walk_finite: "walk xs ⟹ finite (edges_of_walk xs)" using edges_of_walk_in_E finite_edge_set finite_subset by blast lemma edges_of_walk_empty: "edges_of_walk [] = {}" "edges_of_walk [v] = {}" unfolding edges_of_walk_def by simp_all lemma edges_of_walk_2: "edges_of_walk [v,w] = {(v,w)}" proof { fix v' w' assume "(v', w') ∈ edges_of_walk [v,w]" then obtain xs_pre xs_post where xs_decomp: "[v,w] = xs_pre @ v' # w' # xs_post" using edges_of_walkE[of v' w' "[v,w]"] by blast then have "xs_pre = Nil" by (metis Nil_is_append_conv butlast.simps(2) butlast_append list.discI) then have "(v',w') ∈ {(v,w)}" using xs_decomp by simp } then show "edges_of_walk [v, w] ⊆ {(v, w)}" by (simp add: subrelI) show "{(v, w)} ⊆ edges_of_walk [v, w]" unfolding edges_of_walk_def by blast qed lemma edges_of_walk_edge: "⟦ walk xs; (v,w) ∈ edges_of_walk xs ⟧ ⟹ v→w" using edges_of_walkE walk_middle_edge by fastforce lemma edges_of_walk_middle [simp]: "(v,w) ∈ edges_of_walk (xs @ v # w # xs')" unfolding edges_of_walk_def by blast lemma edges_of_comp1: "edges_of_walk xs ⊆ edges_of_walk (xs @ ys)" unfolding edges_of_walk_def by force lemma edges_of_comp2: "edges_of_walk ys ⊆ edges_of_walk (xs @ ys)" proof- { fix v w assume "(v,w) ∈ edges_of_walk ys" then have "∃ys_pre ys_post. ys = ys_pre @ v # w # ys_post" by (meson edges_of_walkE) then have "(v,w) ∈ edges_of_walk (xs @ ys)" by (metis (mono_tags, lifting) append.assoc edges_of_walk_def mem_Collect_eq) } then show ?thesis by (simp add: subrelI) qed lemma walk_edges_decomp_simple: "edges_of_walk (v # w # xs) = {(v,w)} ∪ edges_of_walk (w # xs)" (is "?A = ?B") proof have "edges_of_walk (w # xs) ⊆ ?A" using edges_of_comp2[of "w # xs" "[v]"] by simp moreover have "(v,w) ∈ ?A" by (metis append_eq_Cons_conv edges_of_walk_middle) ultimately show "?B ⊆ ?A" by blast { fix v' w' assume "(v',w') ∈ ?A" then obtain xs_pre xs_post where xs_decomp: "v # w # xs = xs_pre @ v' # w' # xs_post" using edges_of_walkE by blast have "(v',w') ∈ ?B" proof (cases) assume "xs_pre = Nil" then show ?thesis using xs_decomp by auto next assume "xs_pre ≠ Nil" then show ?thesis by (metis Cons_eq_append_conv UnI2 edges_of_walk_middle xs_decomp) qed } then show "?A ⊆ ?B" by auto qed lemma walk_edges_decomp: "edges_of_walk (xs @ x # xs') = edges_of_walk (xs @ [x]) ∪ edges_of_walk (x # xs')" proof (induct xs) case (Cons v xs) show ?case proof (cases) assume "xs = Nil" then show ?thesis using edges_of_walk_2 walk_edges_decomp_simple by auto next assume "xs ≠ Nil" then obtain w xs_post where "xs = w # xs_post" using list.exhaust_sel by blast then show ?thesis using Cons.hyps walk_edges_decomp_simple by auto qed qed (simp add: edges_of_walk_empty(2)) lemma walk_edges_decomp': "edges_of_walk (xs @ v # w # xs') = edges_of_walk (xs @ [v]) ∪ {(v,w)} ∪ edges_of_walk (w # xs')" using walk_edges_decomp walk_edges_decomp_simple by (metis sup.assoc) lemma walk_edges_vertices: assumes "(v, w) ∈ edges_of_walk xs" shows "v ∈ set xs" "w ∈ set xs" using assms edges_of_walkE by force+ lemma walk_edges_subset: assumes edges_subsets: "edges_of_walk xs ⊆ edges_of_walk ys" and non_trivial: "tl xs ≠ Nil" shows "set xs ⊆ set ys" proof fix v assume "v ∈ set xs" then obtain xs_pre xs_post where xs_decomp: "xs = xs_pre @ v # xs_post" by (meson split_list) show "v ∈ set ys" proof (cases) assume "xs_pre = Nil" then have "xs_post ≠ Nil" using xs_decomp non_trivial by auto then have "xs = xs_pre @ v # hd xs_post # tl xs_post" by (simp add: xs_decomp) then have "(v, hd xs_post) ∈ edges_of_walk xs" using edges_of_walk_def by auto then show ?thesis using walk_edges_vertices(1) edges_subsets by fastforce next assume "xs_pre ≠ Nil" then have "xs = butlast xs_pre @ last xs_pre # v # xs_post" by (simp add: xs_decomp) then have "(last xs_pre, v) ∈ edges_of_walk xs" using edges_of_walk_def by auto then show ?thesis using walk_edges_vertices(2) edges_subsets by fastforce qed qed text ‹ A path has no repeated vertices, so if we split a path at an edge we find that the two pieces do not contain this edge any more. › lemma path_edges: assumes "path xs" "(v,w) ∈ edges_of_walk xs" shows "∃xs_pre xs_post. xs = xs_pre @ v # w # xs_post ∧ (v,w) ∉ edges_of_walk (xs_pre @ [v]) ∧ (v,w) ∉ edges_of_walk (w # xs_post)" proof- obtain xs_pre xs_post where xs_decomp: "xs = xs_pre @ v # w # xs_post" by (meson assms(2) edges_of_walkE) then have "(v,w) ∉ edges_of_walk (xs_pre @ [v])" using assms(1) edges_of_walkE by (metis path_from_to_ends list.discI path_decomp' path_from_toI snoc_eq_iff_butlast) moreover have "(v,w) ∉ edges_of_walk (w # xs_post)" using assms(1) by (metis edges_of_walkE in_set_conv_decomp path_decomp(2) path_first_vertex xs_decomp) ultimately show ?thesis using xs_decomp by blast qed lemma path_edges_remove_prefix: assumes "path (xs @ x # xs')" shows "edges_of_walk (xs @ [x]) = edges_of_walk (xs @ x # xs') - edges_of_walk (x # xs')" proof- { fix v w assume *: "(v,w) ∈ edges_of_walk (xs @ [x])" then have 1: "(v,w) ∈ edges_of_walk (xs @ x # xs')" using walk_edges_decomp[of xs x xs'] by force moreover have "(v,w) ∉ edges_of_walk (x # xs')" proof assume contra: "(v,w) ∈ edges_of_walk (x # xs')" then have "w ∈ set (x # xs')" by (meson walk_edges_vertices(2)) moreover have "w ≠ x" using assms contra * 1 by (metis path_decomp(2) UnE edges_of_walkE edges_of_walk_edge list.set_intros(1) path_2 path_disjoint path_first_vertex self_append_conv2 set_append walk_edges_vertices(1)) moreover have "w ∈ set (xs @ [x])" by (meson * walk_edges_vertices(2)) ultimately show False using assms by auto qed ultimately have "(v,w) ∈ edges_of_walk (xs @ x # xs') - edges_of_walk (x # xs')" by blast } then show ?thesis using walk_edges_decomp[of xs x xs'] by auto qed subsection ‹The First Edge of a Walk› text ‹ In the proof of Menger's Theorem, we will often talk about the first edge of a path. Let us define this concept. › fun first_edge_of_walk where "first_edge_of_walk (v # w # xs) = (v, w)" | "first_edge_of_walk [v] = undefined" | "first_edge_of_walk [] = undefined" lemma first_edge_in_edges: "tl xs ≠ Nil ⟹ first_edge_of_walk xs ∈ edges_of_walk xs" unfolding edges_of_walk_def by (induct rule: first_edge_of_walk.induct) auto lemma first_edge_hd_tl: "⟦ v ↝xs↝ w; tl xs ≠ Nil ⟧ ⟹ first_edge_of_walk xs = (v, hd (tl xs))" by (induct "xs" rule: first_edge_of_walk.induct) auto lemma first_edge_first: assumes "v ↝xs↝ w" "(v,w') ∈ edges_of_walk xs" shows "first_edge_of_walk xs = (v,w')" using assms proof (induct rule: first_edge_of_walk.induct) case (1 v w xs) then show ?case by (metis path_decomp(1) append_self_conv2 edges_of_walkE first_edge_of_walk.simps(1) hd_append hd_in_set not_distinct_conv_prefix path_from_toE) next case (2 v) then show ?case using path_edges by fastforce qed blast subsection ‹Distance› text ‹ The distance between two vertices is the minimum length of a path. Note that this is not a symmetric function because we are on digraphs. › definition distance :: "'a ⇒ 'a ⇒ nat" where "distance v w ≡ Min { length xs | xs. v↝xs↝w }" text ‹ The @{const Min} operator applies only to finite sets, so let us prove that this is the case. › lemma distance_lengths_finite: "finite { length xs | xs. v↝xs↝w }" proof- have "{ length xs | xs. v↝xs↝w } ⊆ { n | n. n ≤ card V }" using path_length by blast then show ?thesis using finite_Collect_le_nat by (meson finite_subset) qed text ‹ If we have a concrete path from @{term v} to @{term w}, then the length of this path bounds the distance from @{term v} to @{term w}. › lemma distance_upper_bound: "v↝xs↝w ⟹ distance v w ≤ length xs" unfolding distance_def using Min_le[OF distance_lengths_finite] by blast text ‹ Another characterization of @{const distance}: If we have a concrete minimal path from @{term v} to @{term w}, this defines the distance. › lemma distance_witness: assumes xs: "v ↝xs↝ w" and xs_min: "⋀xs'. v ↝xs'↝ w ⟹ length xs ≤ length xs'" shows "distance v w = length xs" proof- have "⋀d. d ∈ {length xs | xs. v ↝xs↝ w} ⟹ length xs ≤ d" using xs_min by blast then show ?thesis unfolding distance_def using Min_eqI by (metis (mono_tags, lifting) distance_lengths_finite xs mem_Collect_eq) qed subsection ‹Subgraphs› text ‹We only need one kind of subgraph: The subgraph obtained by removing a single vertex.› definition remove_vertex :: "'a ⇒ ('a, 'b) Graph_scheme" where "remove_vertex x ≡ G⦇ verts := V - {x}, arcs := Restr E (V - {x}) ⦈" lemma remove_vertex_V: "V⇘remove_vertex x⇙ = V - {x}" unfolding remove_vertex_def by auto lemma remove_vertex_V': "V⇘remove_vertex x⇙ ⊆ V" unfolding remove_vertex_def by auto lemma remove_vertex_E: "E⇘remove_vertex x⇙ = Restr E (V - {x})" unfolding remove_vertex_def by simp lemma remove_vertex_E': "v →⇘remove_vertex x⇙ w ⟹ v→w" by (simp add: remove_vertex_E) lemma remove_vertex_E'': "⟦ v→w; v ≠ x; w ≠ x ⟧ ⟹ v →⇘remove_vertex x⇙ w" by (simp add: edges_are_in_V remove_vertex_E) text ‹Of course, this is still a digraph.› lemma remove_vertex_Digraph: "Digraph (remove_vertex v)" proof let ?V = "V⇘remove_vertex v⇙" let ?E = "E⇘remove_vertex v⇙" show "finite ?V" unfolding remove_vertex_def using finite_vertex_set by simp show "?E ⊆ ?V × ?V" proof fix e assume "e ∈ ?E" then have "e ∈ (V - {v}) × (V - {v})" by (metis Int_iff remove_vertex_E) then show "e ∈ ?V × ?V" using remove_vertex_V by auto qed have "⋀x y. ⟦ (x,y) ∈ ?E; (x,y) ∉ E ⟧ ⟹ (y,x) ∈ ?E" unfolding remove_vertex_def by simp qed text ‹ We are also going to need a few lemmas about how walks and paths behave when we remove a vertex. First, if we remove a vertex that is not on a walk @{term xs}, then @{term xs} is still a walk after removing this vertex. › lemma remove_vertex_walk: assumes "walk xs" "x ∉ set xs" shows "Digraph.walk (remove_vertex x) xs" proof- interpret H: Digraph "remove_vertex x" using remove_vertex_Digraph by blast show ?thesis using assms proof (induct rule: walk.induct) case (Singleton v) then have "v ∈ V - {x}" by simp then show ?case using remove_vertex_V by simp next case (Cons v w vs) then have "v →⇘remove_vertex x⇙ w" using remove_vertex_E'' by auto then show ?case by (meson Cons.hyps(3) Cons.prems(1) H.Cons assms(2) list.set_intros(2)) qed simp qed text ‹The same holds for paths.› lemma remove_vertex_path_from_to: "⟦ v ↝xs↝ w; x ∈ V; x ∉ set xs ⟧ ⟹ v ↝xs↝⇘remove_vertex x⇙ w" using path_from_to_def remove_vertex_walk by fastforce text ‹ Conversely, if something was a walk or a path in the subgraph, then it is also a walk or a path in the supergraph. › lemma remove_vertex_walk_add: assumes "Digraph.walk (remove_vertex x) xs" shows "walk xs" proof- interpret H: Digraph "remove_vertex x" using remove_vertex_Digraph by blast show ?thesis using assms proof (induct rule: H.walk.induct) case (Singleton v) then show ?case by (meson Digraph.Singleton Digraph_axioms remove_vertex_V' subsetD) next case (Cons v w vs) then show ?case by (meson Digraph.Cons Digraph_axioms remove_vertex_E') qed simp qed lemma remove_vertex_path_from_to_add: "v ↝xs↝⇘remove_vertex x⇙ w ⟹ v ↝xs↝ w" using path_from_to_def remove_vertex_walk_add by fastforce end ― ‹context Digraph› subsection ‹Two Distinguished Distinct Non-adjacent Vertices.› text ‹ The setup for Menger's Theorem requires two distinguished distinct non-adjacent vertices @{term v0} and @{term v1}. Let us pin down this concept with the following locale. › locale v0_v1_Digraph = Digraph + fixes v0 v1 :: "'a" assumes v0_V: "v0 ∈ V" and v1_V: "v1 ∈ V" and v0_nonadj_v1: "¬v0→v1" and v0_neq_v1: "v0 ≠ v1" text ‹ The only lemma we need about @{locale v0_v1_Digraph} for now is that it is closed under removing a vertex that is not @{term v0} or @{term v1}. › lemma (in v0_v1_Digraph) remove_vertices_v0_v1_Digraph: assumes "v ≠ v0" "v ≠ v1" shows "v0_v1_Digraph (remove_vertex v) v0 v1" proof (rule v0_v1_Digraph.intro) show "v0_v1_Digraph_axioms (remove_vertex v) v0 v1" using assms v0_nonadj_v1 v0_neq_v1 v0_V v1_V remove_vertex_V remove_vertex_E' by unfold_locales blast+ qed (simp add: remove_vertex_Digraph) subsection ‹Undirected Graphs› text ‹ We represent undirecteded graphs as a special case of digraphs where every undirected edge is represented as an edge in both directions. We also exclude loops because loops are uncommon in undirected graphs. As we will explain in the next paragraph, all of this has no bearing on the validity of Menger's Theorem for undirected graphs. › locale Graph = Digraph + assumes undirected: "v→w = w→v" and no_loops: "¬v→v" text ‹ We observe that this makes @{locale Digraph} a sublocale of @{locale Graph}, meaning that every theorem we prove for digraphs automatically holds for undirected graphs, although it may not make sense because for example ``connectedness'' (if we were to define it) would need different definitions for directed and undirected graphs. Fortunately, the notions of ``separator'' and ``internally vertex-disjoint paths'' on directed graphs are the same for undirected graphs. So Menger's Theorem, when we eventually prove it in the @{locale Digraph} locale, will apply automatically to the @{locale Graph} locale without any additional work. For this reason we will not use the @{term Graph} locale again in this proof development and it exists merely to show that undirected graphs are covered as a special case by our definitions. › end