Theory Undirected_Graph_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
  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