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