section ‹ Connectivity › text ‹This theory defines concepts around the connectivity of a graph and its vertices, as well as graph properties that depend on connectivity definitions, such as shortest path, radius, diameter, and eccentricity › theory Connectivity imports Undirected_Graph_Walks begin context ulgraph begin subsection ‹Connecting Walks and Paths › definition connecting_walk :: "'a ⇒ 'a ⇒ 'a list ⇒ bool" where "connecting_walk u v xs ≡ is_walk xs ∧ hd xs= u ∧ last xs = v" lemma connecting_walk_rev: "connecting_walk u v xs ⟷ connecting_walk v u (rev xs)" unfolding connecting_walk_def using is_walk_rev by (auto simp add: hd_rev last_rev) lemma connecting_walk_wf: "connecting_walk u v xs ⟹ u ∈ V ∧ v ∈ V" using is_walk_wf_hd is_walk_wf_last by (auto simp add: connecting_walk_def) lemma connecting_walk_self: "u ∈ V ⟹ connecting_walk u u [u] = True" unfolding connecting_walk_def by (simp add: is_walk_singleton) text ‹ We define two definitions of connecting paths. The first uses the @{term "gen_path"} definition, which allows for trivial paths and cycles, the second uses the stricter definition of a path which requires it to be an open walk › definition connecting_path :: "'a ⇒ 'a ⇒ 'a list ⇒ bool" where "connecting_path u v xs ≡ is_gen_path xs ∧ hd xs = u ∧ last xs = v" definition connecting_path_str :: "'a ⇒ 'a ⇒ 'a list ⇒ bool" where "connecting_path_str u v xs ≡ is_path xs ∧ hd xs = u ∧ last xs = v" lemma connecting_path_rev: "connecting_path u v xs ⟷ connecting_path v u (rev xs)" unfolding connecting_path_def using is_gen_path_rev by (auto simp add: hd_rev last_rev) lemma connecting_path_walk: "connecting_path u v xs ⟹ connecting_walk u v xs" unfolding connecting_path_def connecting_walk_def using is_gen_path_def by auto lemma connecting_path_str_gen: "connecting_path_str u v xs ⟹ connecting_path u v xs" unfolding connecting_path_def connecting_path_str_def is_gen_path_def is_path_def by (simp add: is_open_walk_def) lemma connecting_path_gen_str: "connecting_path u v xs ⟹ (¬ is_cycle xs) ⟹ walk_length xs > 0 ⟹ connecting_path_str u v xs" unfolding connecting_path_def connecting_path_str_def using is_gen_path_path by auto lemma connecting_path_alt_def: "connecting_path u v xs ⟷ connecting_walk u v xs ∧ is_gen_path xs" proof - have "is_gen_path xs ⟹ is_walk xs" by (simp add: is_gen_path_def) then have "(is_walk xs ∧ hd xs = u ∧ last xs = v) ∧ is_gen_path xs ⟷ (hd xs = u ∧ last xs = v) ∧ is_gen_path xs" by blast thus ?thesis by (auto simp add: connecting_path_def connecting_walk_def) qed lemma connecting_path_length_bound: "u ≠ v ⟹ connecting_path u v p ⟹ walk_length p ≥ 1" using walk_length_def by (metis connecting_path_def is_gen_path_def is_walk_not_empty2 last_ConsL le_refl length_0_conv less_one list.exhaust_sel nat_less_le nat_neq_iff neq_Nil_conv walk_edges.simps(3)) lemma connecting_path_self: "u ∈ V ⟹ connecting_path u u [u] = True" unfolding connecting_path_alt_def using connecting_walk_self by (simp add: is_gen_path_def is_walk_singleton) lemma connecting_path_singleton: "connecting_path u v xs ⟹ length xs = 1 ⟹ u = v" by (metis cancel_comm_monoid_add_class.diff_cancel connecting_path_def fact_1 fact_nonzero last_rev length_0_conv neq_Nil_conv singleton_rev_conv walk_edges.simps(3) walk_length_conv walk_length_def) lemma connecting_walk_path: assumes "connecting_walk u v xs" shows "∃ ys . connecting_path u v ys ∧ walk_length ys ≤ walk_length xs" proof (cases "u = v") case True then show ?thesis using assms connecting_path_self connecting_walk_wf by (metis bot_nat_0.extremum list.size(3) walk_edges.simps(2) walk_length_def) next case False then have "walk_length xs ≠ 0" using assms connecting_walk_def is_walk_def by (metis last_ConsL length_0_conv list.distinct(1) list.exhaust_sel walk_edges.simps(3) walk_length_def) then show ?thesis using assms False proof (induct "walk_length xs" arbitrary: xs rule: less_induct) fix xs assume IH: "(⋀xsa. walk_length xsa < walk_length xs ⟹ walk_length xsa ≠ 0 ⟹ connecting_walk u v xsa ⟹ u ≠ v ⟹ ∃ys. connecting_path u v ys ∧ walk_length ys ≤ walk_length xsa)" assume assm: "connecting_walk u v xs" and ne: "u ≠ v" and n0: "walk_length xs ≠ 0" then show "∃ys. connecting_path u v ys ∧ walk_length ys ≤ walk_length xs" proof (cases "walk_length xs ≤ 1") ― ‹ Base Cases › case True then have "walk_length xs = 1" using n0 by auto then show ?thesis using ne assm cancel_comm_monoid_add_class.diff_cancel connecting_path_alt_def connecting_walk_def distinct_length_2_or_more distinct_singleton hd_Cons_tl is_gen_path_def is_walk_def last_ConsL last_ConsR length_0_conv length_tl walk_length_conv by (metis True) next case False then show ?thesis proof (cases "distinct xs") case True then show ?thesis using assm connecting_path_alt_def connecting_walk_def is_gen_path_def by auto next case False then obtain ws ys zs y where xs_decomp: "xs = ws@[y]@ys@[y]@zs" using not_distinct_decomp by blast let ?rs = "ws@[y]@zs" have hd: "hd ?rs = u" using xs_decomp assm connecting_walk_def by (metis hd_append list.distinct(1)) have lst: "last ?rs = v" using xs_decomp assm connecting_walk_def by simp have wl: "walk_length ?rs ≠ 0" using hd lst ne walk_length_conv by auto have "set ?rs ⊆ V" using assm connecting_walk_def is_walk_def xs_decomp by auto have cw: "connecting_walk u v ?rs" unfolding connecting_walk_def is_walk_decomp using assm connecting_walk_def hd is_walk_decomp lst xs_decomp by blast have "ys@[y] ≠ []"by simp then have "length ?rs < length xs" using xs_decomp length_list_decomp_lt by auto have "walk_length ?rs < walk_length xs" using walk_length_conv xs_decomp by force then show ?thesis using IH[of ?rs] using cw ne wl le_trans less_or_eq_imp_le by blast qed qed qed qed lemma connecting_walk_split: assumes "connecting_walk u v xs" assumes "connecting_walk v z ys" shows "connecting_walk u z (xs @ (tl ys))" using connecting_walk_def is_walk_append by (metis append.right_neutral assms(1) assms(2) connecting_walk_self connecting_walk_wf hd_append2 is_walk_not_empty last_appendR last_tl list.collapse) lemma connecting_path_split: assumes "connecting_path u v xs" "connecting_path v z ys" obtains p where "connecting_path u z p" and "walk_length p ≤ walk_length (xs @ (tl ys))" using connecting_walk_split connecting_walk_path connecting_path_walk assms(1) assms(2) by blast lemma connecting_path_split_length: assumes "connecting_path u v xs" "connecting_path v z ys" obtains p where "connecting_path u z p" and "walk_length p ≤ walk_length xs + walk_length ys" proof - have "connecting_walk u z (xs @ (tl ys))" using connecting_walk_split assms connecting_path_walk by blast have "walk_length (xs @ (tl ys)) ≤ walk_length xs + walk_length ys" using walk_length_app_ineq by (simp add: le_diff_conv walk_length_conv) thus ?thesis using connecting_path_split by (metis (full_types) assms(1) assms(2) dual_order.trans that) qed subsection ‹ Vertex Connectivity › text ‹Two vertices are defined to be connected if there exists a connecting path. Note that the more general version of a connecting path is again used as a vertex should be considered as connected to itself › definition vert_connected :: "'a ⇒ 'a ⇒ bool" where "vert_connected u v ≡ ∃ xs . connecting_path u v xs" lemma vert_connected_rev: "vert_connected u v ⟷ vert_connected v u" unfolding vert_connected_def using connecting_path_rev by auto lemma vert_connected_id: "u ∈ V ⟹ vert_connected u u = True" unfolding vert_connected_def using connecting_path_self by auto lemma vert_connected_trans: "vert_connected u v ⟹ vert_connected v z ⟹ vert_connected u z" unfolding vert_connected_def using connecting_path_split by meson lemma vert_connected_wf: "vert_connected u v ⟹ u ∈ V ∧ v ∈ V" using vert_connected_def connecting_path_walk connecting_walk_wf by blast definition vert_connected_n :: "'a ⇒ 'a ⇒ nat ⇒ bool" where "vert_connected_n u v n ≡ ∃ p. connecting_path u v p ∧ walk_length p = n" lemma vert_connected_n_imp: "vert_connected_n u v n ⟹ vert_connected u v" by (auto simp add: vert_connected_def vert_connected_n_def) lemma vert_connected_n_rev: "vert_connected_n u v n ⟷ vert_connected_n v u n" unfolding vert_connected_n_def using walk_length_rev by (metis connecting_path_rev) definition connecting_paths :: "'a ⇒ 'a ⇒ 'a list set" where "connecting_paths u v ≡ {xs . connecting_path u v xs}" lemma connecting_paths_self: "u ∈ V ⟹ [u] ∈ connecting_paths u u" unfolding connecting_paths_def using connecting_path_self by auto lemma connecting_paths_empty_iff: "vert_connected u v ⟷ connecting_paths u v ≠ {}" unfolding connecting_paths_def vert_connected_def by auto lemma elem_connecting_paths: "p ∈ connecting_paths u v ⟹ connecting_path u v p" using connecting_paths_def by blast lemma connecting_paths_ss_gen: "connecting_paths u v ⊆ gen_paths" unfolding connecting_paths_def gen_paths_def connecting_path_def by auto lemma connecting_paths_sym: "xs ∈ connecting_paths u v ⟷ rev xs ∈ connecting_paths v u" unfolding connecting_paths_def using connecting_path_rev by simp text ‹A set is considered to be connected, if all the vertices within that set are pairwise connected › definition is_connected_set :: "'a set ⇒ bool" where "is_connected_set V' ≡ (∀ u v . u ∈ V' ⟶ v ∈ V' ⟶ vert_connected u v)" lemma is_connected_set_empty: "is_connected_set {}" unfolding is_connected_set_def by simp lemma is_connected_set_singleton: "x ∈ V ⟹ is_connected_set {x}" unfolding is_connected_set_def by (auto simp add: vert_connected_id) lemma is_connected_set_wf: "is_connected_set V' ⟹ V' ⊆ V" unfolding is_connected_set_def by (meson connecting_path_walk connecting_walk_wf subsetI vert_connected_def) lemma is_connected_setD: "is_connected_set V' ⟹ u ∈ V' ⟹ v ∈ V' ⟹ vert_connected u v" by (simp add: is_connected_set_def) lemma not_connected_set: "¬ is_connected_set V' ⟹ u ∈ V' ⟹ ∃ v ∈ V' . ¬ vert_connected u v" using is_connected_setD by (meson is_connected_set_def vert_connected_rev vert_connected_trans) subsection ‹Graph Properties on Connectivity › text ‹The shortest path is defined to be the infinum of the set of connecting path walk lengths. Drawing inspiration from \<^cite>‹"noschinski_2012"›, we use the infinum and enats as this enables more natural reasoning in a non-finite setting, while also being useful for proofs of a more probabilistic or analysis nature› definition shortest_path :: "'a ⇒ 'a ⇒ enat" where "shortest_path u v ≡ INF p∈ connecting_paths u v. enat (walk_length p)" lemma shortest_path_walk_length: "shortest_path u v = n ⟹ p ∈ connecting_paths u v ⟹ walk_length p ≥ n" using shortest_path_def INF_lower[of p "connecting_paths u v" "λ p . enat (walk_length p)"] by auto lemma shortest_path_lte: "⋀ p . p ∈ connecting_paths u v ⟹ shortest_path u v ≤ walk_length p" unfolding shortest_path_def by (simp add: Inf_lower) lemma shortest_path_obtains: assumes "shortest_path u v = n" assumes "n ≠ top" obtains p where "p ∈ connecting_paths u v" and "walk_length p = n" using enat_in_INF shortest_path_def by (metis assms(1) assms(2) the_enat.simps) lemma shortest_path_intro: assumes "n ≠ top" assumes "(∃ p ∈ connecting_paths u v . walk_length p = n)" assumes "(⋀ p. p ∈ connecting_paths u v ⟹ n ≤ walk_length p)" shows "shortest_path u v = n" proof (rule ccontr) assume a: "shortest_path u v ≠ enat n" then have "shortest_path u v < n" by (metis antisym_conv2 assms(2) shortest_path_lte) then have "∃ p ∈ connecting_paths u v .walk_length p < n" using shortest_path_def by (simp add: INF_less_iff) thus False using assms(3) using le_antisym less_imp_le_nat by blast qed lemma shortest_path_self: assumes "u ∈ V" shows "shortest_path u u = 0" proof - have "[u] ∈ connecting_paths u u" using connecting_paths_self by (simp add: assms) then have "walk_length [u] = 0" using walk_length_def walk_edges.simps by auto thus ?thesis using shortest_path_def by (metis ‹[u] ∈ connecting_paths u u› le_zero_eq shortest_path_lte zero_enat_def) qed lemma connecting_paths_sym_length: "i ∈ connecting_paths u v ⟹ ∃j∈connecting_paths v u. (walk_length j) = (walk_length i)" using connecting_paths_sym by (metis walk_length_rev) lemma shortest_path_sym: "shortest_path u v = shortest_path v u" unfolding shortest_path_def by (intro INF_eq)(metis add.right_neutral le_iff_add connecting_paths_sym_length)+ lemma shortest_path_inf: "¬ vert_connected u v ⟹ shortest_path u v = ∞" using connecting_paths_empty_iff shortest_path_def by (simp add: top_enat_def) lemma shortest_path_not_inf: assumes "vert_connected u v" shows "shortest_path u v ≠ ∞" proof - have "⋀ p. connecting_path u v p ⟹ enat (walk_length p) ≠ ∞" using connecting_path_def is_gen_path_def by auto thus ?thesis unfolding shortest_path_def connecting_paths_def by (metis assms connecting_paths_def infinity_ileE mem_Collect_eq shortest_path_def shortest_path_lte vert_connected_def) qed lemma shortest_path_obtains2: assumes "vert_connected u v" obtains p where "p ∈ connecting_paths u v" and "walk_length p = shortest_path u v" proof - have "connecting_paths u v ≠ {}" using assms connecting_paths_empty_iff by auto have "shortest_path u v ≠ ∞" using assms shortest_path_not_inf by simp thus ?thesis using shortest_path_def enat_in_INF by (metis that top_enat_def) qed lemma shortest_path_split: "shortest_path x y ≤ shortest_path x z + shortest_path z y" proof (cases "vert_connected x y ∧ vert_connected x z") case True show ?thesis proof (rule ccontr) assume " ¬ shortest_path x y ≤ shortest_path x z + shortest_path z y" then have c: "shortest_path x y > shortest_path x z + shortest_path z y" by simp have "vert_connected z y" using True vert_connected_trans vert_connected_rev by blast then obtain p1 p2 where "connecting_path x z p1" and "connecting_path z y p2" and s1: "shortest_path x z = walk_length p1" and s2: "shortest_path z y = walk_length p2" using True shortest_path_obtains2 connecting_paths_def elem_connecting_paths by metis then obtain p3 where cp: "connecting_path x y p3" and "walk_length p1 + walk_length p2 ≥ walk_length p3" using connecting_path_split_length by blast then have "shortest_path x z + shortest_path z y ≥ walk_length p3" using s1 s2 by simp then have lt: "shortest_path x y > walk_length p3" using c by auto have "p3 ∈ connecting_paths x y" using cp connecting_paths_def by auto then show False using shortest_path_def shortest_path_obtains2 by (metis True enat_ord_simps(1) enat_ord_simps(2) le_Suc_ex lt not_add_less1 shortest_path_lte) qed next case False then show ?thesis by (metis enat_ord_code(3) plus_enat_simps(2) plus_enat_simps(3) shortest_path_inf vert_connected_trans) qed lemma shortest_path_invalid_v: "v ∉ V ∨ u ∉ V ⟹ shortest_path u v = ∞" using shortest_path_inf vert_connected_wf by blast lemma shortest_path_lb: assumes "u ≠ v" assumes "vert_connected u v" shows "shortest_path u v > 0" proof - have "⋀ p. connecting_path u v p ⟹ enat (walk_length p) > 0" using connecting_path_length_bound assms by fastforce thus ?thesis unfolding shortest_path_def by (metis elem_connecting_paths shortest_path_def shortest_path_obtains2 assms(2)) qed text ‹Eccentricity of a vertex v is the furthest distance between it and a (different) vertex › definition eccentricity :: "'a ⇒ enat" where "eccentricity v ≡ SUP u ∈ V - {v}. shortest_path v u" lemma eccentricity_empty_vertices: "V = {} ⟹ eccentricity v = 0" "V = {v} ⟹ eccentricity v = 0" unfolding eccentricity_def using bot_enat_def by simp_all lemma eccentricity_bot_iff: "eccentricity v = 0 ⟷ V = {} ∨ V = {v}" proof (intro iffI) assume a: "eccentricity v = 0" show "V = {} ∨ V = {v}" proof (rule ccontr, simp) assume a2: "V ≠ {} ∧ V ≠ {v}" have eq0: "∀ u ∈ V - {v} . shortest_path v u = 0" using SUP_bot_conv(1)[of "λ u. shortest_path v u" "V - {v}"] a eccentricity_def bot_enat_def by simp have nc: "∀ u ∈ V - {v} . ¬ vert_connected v u ⟶ shortest_path v u = ∞" using shortest_path_inf by simp have "∀ u ∈ V - {v} . vert_connected v u ⟶ shortest_path v u > 0" using shortest_path_lb by auto then show False using eq0 a2 nc by auto qed next show "V = {} ∨ V = {v} ⟹ eccentricity v = 0" using eccentricity_empty_vertices by auto qed lemma eccentricity_invalid_v: assumes "v ∉ V" assumes "V ≠ {}" shows "eccentricity v = ∞" proof - have "⋀ u. shortest_path v u = ∞" using assms shortest_path_invalid_v by blast have "V - {v} = V" using assms by simp then have "eccentricity v = (SUP u ∈ V . shortest_path v u)" by (simp add: eccentricity_def) thus ?thesis using eccentricity_def shortest_path_invalid_v assms by simp qed lemma eccentricity_gt_shortest_path: assumes "u ∈ V" shows "eccentricity v ≥ shortest_path v u" proof (cases "u ∈ V - {v}") case True then show ?thesis unfolding eccentricity_def by (simp add: SUP_upper) next case f1: False then have "u = v" using assms by auto then have "shortest_path u v = 0" using shortest_path_self assms by auto then show ?thesis by (simp add: ‹u = v›) qed lemma eccentricity_disconnected_graph: assumes "¬ is_connected_set V" assumes "v ∈ V" shows "eccentricity v = ∞" proof - obtain u where uin: "u ∈ V" and nvc: "¬ vert_connected v u" using not_connected_set assms by auto then have "u ≠ v" using vert_connected_id by auto then have "u ∈ V - {v}" using uin by simp moreover have "shortest_path v u = ∞" using nvc shortest_path_inf by auto thus ?thesis using eccentricity_gt_shortest_path by (metis enat_ord_simps(5) uin) qed text ‹The diameter is the largest distance between any two vertices › definition diameter :: "enat" where "diameter ≡ SUP v ∈ V . eccentricity v" lemma diameter_gt_eccentricity: "v ∈ V ⟹ diameter ≥ eccentricity v" using diameter_def by (simp add: SUP_upper) lemma diameter_disconnected_graph: assumes "¬ is_connected_set V" shows "diameter = ∞" unfolding diameter_def using eccentricity_disconnected_graph by (metis SUP_eq_const assms is_connected_set_empty) lemma diameter_empty: "V = {} ⟹ diameter = 0" unfolding diameter_def using Sup_empty bot_enat_def by simp lemma diameter_singleton: "V = {v} ⟹ diameter = eccentricity v" unfolding diameter_def by simp text ‹The radius is the smallest "shortest" distance between any two vertices › definition radius :: "enat" where "radius ≡ INF v ∈ V . eccentricity v" lemma radius_lt_eccentricity: "v ∈ V ⟹ radius ≤ eccentricity v" using radius_def by (simp add: INF_lower) lemma radius_disconnected_graph: "¬ is_connected_set V ⟹ radius = ∞" unfolding radius_def using eccentricity_disconnected_graph by (metis INF_eq_const is_connected_set_empty) lemma radius_empty: "V = {} ⟹ radius = ∞" unfolding radius_def using Inf_empty top_enat_def by simp lemma radius_singleton: "V = {v} ⟹ radius = eccentricity v" unfolding radius_def by simp text ‹The centre of the graph is all vertices whose eccentricity equals the radius › definition centre :: "'a set" where "centre ≡ {v ∈ V. eccentricity v = radius }" lemma centre_disconnected_graph: "¬ is_connected_set V ⟹ centre = V" unfolding centre_def using radius_disconnected_graph eccentricity_disconnected_graph by auto end lemma (in fin_ulgraph) fin_connecting_paths: "finite (connecting_paths u v)" using connecting_paths_ss_gen finite_gen_paths finite_subset by fastforce subsection ‹We define a connected graph as a non-empty graph (the empty set is not usually considered connected by convention), where the vertex set is connected › locale connected_ulgraph = ulgraph + ne_graph_system + assumes connected: "is_connected_set V" begin lemma vertices_connected: "u ∈ V ⟹ v ∈ V ⟹ vert_connected u v" using is_connected_set_def connected by auto lemma vertices_connected_path: "u ∈ V ⟹ v ∈ V ⟹ ∃ p. connecting_path u v p" using vertices_connected by (simp add: vert_connected_def) lemma connecting_paths_not_empty: "u ∈ V ⟹ v ∈ V ⟹ connecting_paths u v ≠ {}" using connected not_empty connecting_paths_empty_iff is_connected_setD by blast lemma min_shortest_path: assumes "u ∈ V" "v ∈ V" "u ≠ v" shows "shortest_path u v > 0" using shortest_path_lb assms vertices_connected by auto text ‹The eccentricity, diameter, radius, and centre definitions tend to be only used in a connected context, as otherwise they are the INF/SUP value. In these contexts, we can obtain the vertex responsible › lemma eccentricity_obtains_inf: assumes "V ≠ {v}" shows "eccentricity v = ∞ ∨ (∃ u ∈ (V - {v}) . shortest_path v u = eccentricity v)" proof (cases "finite ((λ u. shortest_path v u) ` (V - {v}))") case True then have e: "eccentricity v = Max ((λ u. shortest_path v u) ` (V - {v}))" unfolding eccentricity_def using Sup_enat_def using assms not_empty by auto have "(V - {v}) ≠ {}" using assms not_empty by auto then have "((λ u. shortest_path v u) ` (V - {v})) ≠ {}" by simp then obtain n where "n ∈ ((λ u. shortest_path v u) ` (V - {v}))" and "n = eccentricity v" using Max_in e True by auto then obtain u where "u ∈ (V - {v})" and "shortest_path v u = eccentricity v" by blast then show ?thesis by auto next case False then have "eccentricity v = ∞" unfolding eccentricity_def using Sup_enat_def by (metis (mono_tags, lifting) cSup_singleton empty_iff finite_insert insert_iff) then show ?thesis by simp qed lemma diameter_obtains: "diameter = ∞ ∨ (∃ v ∈ V . eccentricity v = diameter)" proof (cases "is_singleton V") case True then obtain v where "V = {v}" using is_singletonE by auto then show ?thesis using diameter_singleton by simp next case f1: False then show ?thesis proof (cases "finite ((λ v. eccentricity v) ` V)") case True then have "diameter = Max ((λ v. eccentricity v) ` V)" unfolding diameter_def using Sup_enat_def not_empty by simp then obtain n where "n ∈((λ v. eccentricity v) ` V)" and "diameter = n" using Max_in True using not_empty by auto then obtain u where "u ∈ V" and "eccentricity u = diameter" by fastforce then show ?thesis by auto next case False then have "diameter = ∞" unfolding diameter_def using Sup_enat_def by auto then show ?thesis by simp qed qed lemma radius_diameter_singleton_eq: assumes "card V = 1" shows "radius = diameter" proof - obtain v where "V = {v}" using assms card_1_singletonE by auto thus ?thesis unfolding radius_def diameter_def by auto qed end locale fin_connected_ulgraph = connected_ulgraph + fin_ulgraph begin text ‹ In a finite context the supremum/infinum are equivalent to the Max/Min of the sets respectively. This can make reasoning easier › lemma shortest_path_Min_alt: assumes "u ∈ V" "v ∈ V" shows "shortest_path u v = Min ((λ p. enat (walk_length p)) ` (connecting_paths u v))" (is "shortest_path u v = Min ?A") proof - have ne: "?A ≠ {}" using connecting_paths_not_empty assms by auto have "finite (connecting_paths u v)" by (simp add: fin_connecting_paths) then have fin: "finite ?A" by simp have "shortest_path u v = Inf ?A" unfolding shortest_path_def by simp thus ?thesis using Min_Inf ne by (metis fin) qed lemma eccentricity_Max_alt: assumes "v ∈ V" assumes "V ≠ {v}" shows "eccentricity v = Max ((λ u. shortest_path v u) ` (V - {v}))" unfolding eccentricity_def using assms Sup_enat_def finV not_empty by auto lemma diameter_Max_alt: "diameter = Max ((λ v. eccentricity v) ` V)" unfolding diameter_def using Sup_enat_def finV not_empty by auto lemma radius_Min_alt: "radius = Min ((λ v. eccentricity v) ` V)" unfolding radius_def using Min_Inf finV not_empty by (metis (no_types, opaque_lifting) empty_is_image finite_imageI) lemma eccentricity_obtains: assumes "v ∈ V" assumes "V ≠ {v}" obtains u where "u ∈ V" and "u ≠ v" and "shortest_path u v = eccentricity v" proof - have ni: "⋀ u. u ∈ V - {v} ⟹ u ≠ v ∧ u ∈ V" by auto have ne: "V - {v} ≠ {}" using assms not_empty by auto have "eccentricity v = Max ((λ u. shortest_path v u) ` (V - {v}))" using eccentricity_Max_alt assms by simp then obtain u where ui: "u ∈ V - {v}" and eq: "shortest_path v u = eccentricity v" using obtains_MAX assms finV ne by (metis finite_Diff) then have neq: "u ≠ v" by blast have uin: "u ∈ V" using ui by auto thus ?thesis using neq eq that[of u] shortest_path_sym by simp qed lemma radius_obtains: obtains v where "v ∈ V" and "radius = eccentricity v" proof - have "radius = Min ((λ v. eccentricity v) ` V)" using radius_Min_alt by simp then obtain v where "v ∈ V" and "radius = eccentricity v" using obtains_MIN[of V "(λ v . eccentricity v)"] not_empty finV by auto thus ?thesis by (simp add: that) qed lemma radius_obtains_path_vertices: assumes "card V ≥ 2" obtains u v where "u ∈ V" and "v ∈ V" and "u ≠ v" and "radius = shortest_path u v" proof - obtain v where vin: "v ∈ V" and e: "radius = eccentricity v" using radius_obtains by blast then have "V ≠ {v}" using assms by auto then obtain u where "u ∈ V" and "u ≠ v" and "shortest_path u v = radius" using eccentricity_obtains vin e by auto thus ?thesis using vin by (simp add: that) qed lemma diameter_obtains: obtains v where "v ∈ V" and "diameter = eccentricity v" proof - have "diameter = Max ((λ v. eccentricity v) ` V)" using diameter_Max_alt by simp then obtain v where "v ∈ V" and "diameter = eccentricity v" using obtains_MAX[of V "(λ v . eccentricity v)"] not_empty finV by auto thus ?thesis by (simp add: that) qed lemma diameter_obtains_path_vertices: assumes "card V ≥ 2" obtains u v where "u ∈ V" and "v ∈ V" and "u ≠ v" and "diameter = shortest_path u v" proof - obtain v where vin: "v ∈ V" and e: "diameter = eccentricity v" using diameter_obtains by blast then have "V ≠ {v}" using assms by auto then obtain u where "u ∈ V" and "u ≠ v" and "shortest_path u v = diameter" using eccentricity_obtains vin e by auto thus ?thesis using vin by (simp add: that) qed lemma radius_diameter_bounds: shows "radius ≤ diameter" "diameter ≤ 2 * radius" proof - show "radius ≤ diameter" unfolding radius_def diameter_def by (simp add: INF_le_SUP not_empty) next show "diameter ≤ 2 * radius" proof (cases "card V ≥ 2") case True then obtain x y where xin: "x ∈ V" and yin: "y ∈ V" and d: "shortest_path x y = diameter" using diameter_obtains_path_vertices by metis obtain z where zin: "z ∈ V" and e: "eccentricity z = radius" using radius_obtains by metis have "shortest_path x z ≤ eccentricity z" using eccentricity_gt_shortest_path xin shortest_path_sym by simp have "shortest_path x y ≤ shortest_path x z + shortest_path z y" using shortest_path_split by simp also have "... ≤ eccentricity z + eccentricity z" using eccentricity_gt_shortest_path shortest_path_sym zin xin yin by (simp add: add_mono) also have "... ≤ radius + radius" using e by simp finally show ?thesis using d by (simp add: mult_2) next case False have "card V ≠ 0" using not_empty finV by auto then have "card V = 1" using False by simp then show ?thesis using radius_diameter_singleton_eq by (simp add: mult_2) qed qed end text ‹ We define various subclasses of the general connected graph, using the functor locale pattern› locale connected_sgraph = sgraph + ne_graph_system + assumes connected: "is_connected_set V" sublocale connected_sgraph ⊆ connected_ulgraph by (unfold_locales) (simp add: connected) locale fin_connected_sgraph = connected_sgraph + fin_sgraph sublocale fin_connected_sgraph ⊆ fin_connected_ulgraph by (unfold_locales) end