# Theory Connectivity

```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

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

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

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

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 ›
"radius ≡ INF v ∈ V . eccentricity v"

by (metis INF_eq_const is_connected_set_empty)

unfolding radius_def using Inf_empty top_enat_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

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

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

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
qed

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

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