Theory Graph_Definitions

theory Graph_Definitions
  imports "Graph_Theory.Digraph_Component" "Graph_Theory.Shortest_Path"
    "Misc" "Graph_Theory_Batteries"
begin

context wf_digraph
begin

section ‹K-neighborhood definition›
definition k_neighborhood :: "'b weight_fun ⇒ 'a ⇒ real ⇒ 'a set" where
  "k_neighborhood w v k = {u ∈ verts G. μ w v u ≤ k } - {v}"

lemma k_nh_reachable: "u ∈ k_neighborhood w v k ⟹ v →⇧* u"
  unfolding k_neighborhood_def
  using shortest_path_inf by fastforce

lemma source_nmem_k_nh: "v ∉ k_neighborhood w v k"
  unfolding k_neighborhood_def by simp

section ‹Diameter and finite diameter›
text ‹
The diameter is defined as the longest shortest path in the corresponding graph. If there is no path
between any two vertices in the graph, then the diameter is infinite.
We also make use of the notion of a @{text fin_diameter} which only considers the shortest path
between connected nodes.
›

definition sp_costs :: "'b weight_fun ⇒ ereal set" where
  "sp_costs f = {c | u v c. u ∈ verts G ∧ v ∈ verts G ∧ μ f u v = c}"

definition diameter :: "'b weight_fun ⇒ ereal" where
  "diameter f = Sup (sp_costs f)"

definition fin_sp_costs :: "'b weight_fun ⇒ ereal set" where
  "fin_sp_costs f = {c | u v c. u ∈ verts G ∧ v ∈ verts G ∧ μ f u v = c ∧ c < ∞}"

definition fin_diameter :: "'b weight_fun ⇒ ereal" where
  "fin_diameter f = Sup (fin_sp_costs f)"


subsection ‹In general graphs›

lemma empty_imp_dia_minf: "verts G = {} ⟹ diameter w = -∞"
  unfolding diameter_def sp_costs_def
  by (simp add: bot_ereal_def)

lemma empty_imp_fin_dia_minf: "verts G = {} ⟹ fin_diameter w = -∞"
  unfolding fin_diameter_def fin_sp_costs_def
  by (simp add: bot_ereal_def)

lemma dia_eq_fin_dia_if_finite: "diameter f < ∞ ⟹ diameter f = fin_diameter f"
proof -
  assume "diameter f < ∞"
  then have "∞ ∉ sp_costs f"
    unfolding diameter_def using Sup_eq_PInfty by auto
  then have "sp_costs f = fin_sp_costs f"
    unfolding sp_costs_def fin_sp_costs_def by auto
  then show ?thesis
    unfolding diameter_def fin_diameter_def by simp
qed

lemma fin_dia_lowerB: "⟦ u ∈ verts G; v ∈ verts G; μ w u v < ∞⟧
  ⟹ fin_diameter w ≥ μ w u v"
  unfolding fin_diameter_def fin_sp_costs_def
  by (metis (mono_tags, lifting) Sup_upper mem_Collect_eq)

lemma dia_lowerB: "⟦ u ∈ verts G; v ∈ verts G ⟧
  ⟹ diameter w ≥ μ w u v"
  unfolding diameter_def sp_costs_def
  by (metis (mono_tags, lifting) Sup_upper mem_Collect_eq)


subsection ‹In finite graphs›

lemma (in fin_digraph) sp_costs_finite: "finite (sp_costs f)"
  unfolding sp_costs_def by auto

lemma (in fin_digraph) fin_sp_costs_finite: "finite (fin_sp_costs f)"
  unfolding fin_sp_costs_def by auto

lemma (in fin_digraph) ex_sp_eq_dia:
  "verts G ≠ {} ⟹ ∃u ∈ verts G. ∃v ∈ verts G. μ f u v = diameter f"
proof -
  assume "verts G ≠ {}"
  then have "sp_costs f ≠ {}"
    unfolding sp_costs_def using μ_reach_conv by fastforce

  with sp_costs_finite have "∃c ∈ sp_costs f. c = diameter f"
    by (simp add: Sup_in_set diameter_def)
  then show "?thesis" unfolding diameter_def
    unfolding sp_costs_def by auto
qed

text ‹Analogous to the proof of @{thm fin_digraph.ex_sp_eq_dia}.›
lemma (in fin_digraph) ex_sp_eq_fin_dia:
  "verts G ≠ {} ⟹ ∃u ∈ verts G. ∃v ∈ verts G. μ f u v = fin_diameter f"
proof -
  assume "verts G ≠ {}"
  then have "fin_sp_costs f ≠ {}"
    unfolding fin_sp_costs_def using μ_reach_conv by fastforce

  with fin_sp_costs_finite have "∃c ∈ fin_sp_costs f. c = fin_diameter f"
    by (simp add: Sup_in_set fin_diameter_def)
  then show "?thesis" unfolding fin_diameter_def
    unfolding fin_sp_costs_def by auto
qed


lemma (in fin_digraph) fin_diameter_finite: "fin_diameter f < ∞"
proof(rule ccontr)
  fix f assume dia_infty: "¬ fin_diameter f < ∞"

  then have infty_cont: "∞ ∈ fin_sp_costs f" if *: "fin_sp_costs f ≠ {}"
    unfolding fin_diameter_def using *
    by (metis ereal_infty_less(1) fin_sp_costs_finite infinite_growing less_Sup_iff)

  then show "False"
  proof(cases "fin_sp_costs f = {}")
    case True
    then have "fin_diameter f = -∞"
      unfolding fin_diameter_def by (simp add: bot_ereal_def)
    with dia_infty show ?thesis by simp
  next
    case False
    from infty_cont[OF this] dia_infty show ?thesis
      unfolding fin_diameter_def fin_sp_costs_def by auto
  qed
qed

lemma (in fin_digraph) ex_min_apath_eq_fin_dia:
  "⟦ verts G ≠ {}; ∀e ∈ arcs G. f e ≥ 0 ⟧
  ⟹ ∃u ∈ verts G. ∃v ∈ verts G. ∃p. apath u p v ∧ awalk_cost f p = fin_diameter f"
proof -
  assume "verts G ≠ {}" and w_non_neg: "∀e ∈ arcs G. f e ≥ 0"
  from ex_sp_eq_fin_dia[OF this(1)] obtain u v
    where u_v: "u ∈ verts G" "v ∈ verts G" and sp_eq_dia: "μ f u v = fin_diameter f"
    by blast
  from sp_eq_dia have "μ f u v < ∞" using fin_diameter_finite by auto
  then have "u →⇧* v" using μ_reach_conv by blast
  from min_cost_awalk[OF this] w_non_neg obtain p
    where "apath u p v" "μ f u v = awalk_cost f p"
    by auto
  with u_v sp_eq_dia show ?thesis by auto
qed

subsection ‹Relation between diameter and finite diameter›

theorem dia_eq_fin_dia_if_strongly_con: "strongly_connected G ⟹ diameter = fin_diameter"
proof
  fix f assume strongly_con: "strongly_connected G"
  then have "∞ ∉ sp_costs f"
    unfolding sp_costs_def using μ_reach_conv by auto
  then have "sp_costs f = fin_sp_costs f"
    unfolding fin_sp_costs_def sp_costs_def by auto
  then show "diameter f = fin_diameter f"
    unfolding diameter_def fin_diameter_def by auto
qed

end

section ‹N-nearest vertices›
text ‹
The definition of @{text n_nearest_verts} is used to formalize the abstract behaviour of the
Dijkstra algorithm which iteratively visits the nearest undiscovered vertex until all
vertices are discovered.
›
context wf_digraph begin

definition unvisited_verts :: "'a ⇒ 'a set ⇒ 'a set" where
"unvisited_verts u U = {x. x ∈ verts G - U ∧ u →⇧* x}"

definition nearest_vert :: "'b weight_fun ⇒ 'a ⇒ 'a set ⇒ 'a" where
"nearest_vert w u U =
  (SOME x. x ∈ unvisited_verts u U ∧ (∀y ∈ unvisited_verts u U. μ w u y ≥ μ w u x))"

inductive n_nearest_verts :: "'b weight_fun ⇒ 'a ⇒ nat ⇒ 'a set ⇒ bool"
  where
zero_nnvs: "u ∈ verts G ⟹ n_nearest_verts _ u 0 {u}" |
n_nnvs_unvis: "⟦ n_nearest_verts w u n U; unvisited_verts u U ≠ {}⟧
   ⟹ n_nearest_verts w u (Suc n) (insert (nearest_vert w u U) U)" |
n_nnvs_vis: "⟦ n_nearest_verts w u n U; unvisited_verts u U = {} ⟧
   ⟹ n_nearest_verts w u (Suc n) U"

inductive_cases nnvs_ind_cases: "n_nearest_verts w u n U"
thm nnvs_ind_cases


subsection ‹In general graphs›

lemma source_mem_nnvs: "n_nearest_verts w u n U ⟹ u ∈ verts G"
  by (induction rule: n_nearest_verts.induct) auto

lemma unvis_insert: "unvisited_verts u (insert x U) = (unvisited_verts u U) - {x}"
  unfolding unvisited_verts_def by auto

lemma disj_unvis_vis: "unvisited_verts u U ∩ U = {}"
  unfolding unvisited_verts_def by auto

lemma nnvs_finite: "n_nearest_verts w u n U ⟹ finite U"
  by (induction rule: n_nearest_verts.induct) auto

lemma nnvs_card_le_n: "n_nearest_verts w u n U ⟹ card U ≤ Suc n"
  by (induction rule: n_nearest_verts.induct) (auto simp: card_insert_le_m1)

lemma nnvs_mem: "n_nearest_verts w u n U ⟹ u ∈ U"
  by (induction rule: n_nearest_verts.induct) auto

lemma unvis_empty: "unvisited_verts u {a. u →⇧* a} = {}"
  unfolding unvisited_verts_def by auto

end

subsection ‹In finite graphs›
context fin_digraph begin

lemma k_nh_finite: "finite (k_neighborhood w v k)"
  unfolding k_neighborhood_def using finite_verts by force

lemma unvis_finite: "finite (unvisited_verts u U)"
  unfolding unvisited_verts_def using finite_verts by auto

lemma ex_unvis_vert:"⟦ unvisited_verts u U ≠ {} ⟧ ⟹
   ∃x ∈ unvisited_verts u U. (∀y ∈ unvisited_verts u U. μ w u y ≥ μ w u x)"
  unfolding nearest_vert_def using unvis_finite
proof(induction "unvisited_verts u U" arbitrary: u U rule: finite_induct)
  case (insert x F)
  then have "F = unvisited_verts u U - {x}"
    by auto
  then have F: "F = unvisited_verts u (insert x U)"
    using unvis_insert[symmetric] by simp

  show ?case
  proof(cases "unvisited_verts u (insert x U) = {}")
    case True
    with insert.prems show ?thesis using unvis_insert by auto
  next
    case False
    from insert(3)[OF F this] obtain x' where "x' ∈ unvisited_verts u (insert x U)"
      and "∀y∈unvisited_verts u (insert x U). μ w u x' ≤ μ w u y" by blast
    note x' = this

    show ?thesis
    proof(cases "μ w u x' ≤ μ w u x")
      case True
      from x' F insert.hyps(4) have "x' ∈ unvisited_verts u U" by blast
      moreover
      have "∀y ∈ unvisited_verts u U. μ w u x' ≤ μ w u y"
        using F True insert.hyps(4) x' by auto
      ultimately show ?thesis by blast
    next
      case False
      with x' have "∀y ∈ unvisited_verts u (insert x U). μ w u x ≤ μ w u y"
        by fastforce
      with F insert.hyps(4) have "∀y ∈ unvisited_verts u U. μ w u x ≤ μ w u y"
        by fastforce
      with insert.hyps(4) show ?thesis by blast
    qed
  qed
qed blast

lemma some_unvis_vert:
  fixes x
  assumes "unvisited_verts u U ≠ {}" and "x = nearest_vert w u U"
  shows "x ∈ unvisited_verts u U"
    and "∀y ∈ unvisited_verts u U. μ w u y ≥ μ w u x"
proof -
  define nv where "nv ≡ λx. x ∈ unvisited_verts u U
    ∧ (∀y∈unvisited_verts u U. μ w u x ≤ μ w u y)"

  from ex_unvis_vert[OF assms(1)]
  obtain x' where "nv x'" unfolding nv_def
    by blast
  then have "nv (SOME x. nv x)" using some_eq_ex by blast
  with assms(2) have "nv x" unfolding nearest_vert_def nv_def by blast
  then show
    "x ∈ unvisited_verts u U" and
    "∀y ∈ unvisited_verts u U. μ w u y ≥ μ w u x"
    unfolding nv_def by blast+
qed

lemma nearest_vert_unvis: "unvisited_verts u U ≠ {}
  ⟹ nearest_vert w u U ∈ unvisited_verts u U"
  using some_unvis_vert by simp

lemma nearest_vert_not_mem: "unvisited_verts u U ≠ {}
  ⟹ nearest_vert w u U ∉ U"
  using disj_unvis_vis some_unvis_vert(1) by fastforce

lemma nearest_vert_reachable: "unvisited_verts u U ≠ {}
  ⟹ u →⇧* nearest_vert w u U"
  using some_unvis_vert(1) unvisited_verts_def by auto

lemma nnvs_card_ge_n: "⟦ n_nearest_verts w u n U; unvisited_verts u U ≠ {} ⟧
  ⟹ card U ≥ Suc n"
proof(induction rule: n_nearest_verts.induct)
  case (n_nnvs_unvis w u n U)
  have "nearest_vert w u U ∉ U"
    using nearest_vert_unvis[OF n_nnvs_unvis.hyps(2)] disj_unvis_vis by auto
  then have "card (insert (nearest_vert w u U) U) = Suc (card U)"
    using n_nnvs_unvis.hyps(1) nnvs_finite by auto
  with n_nnvs_unvis.IH[OF n_nnvs_unvis.hyps(2)] show ?case by simp
qed simp_all

corollary nnvs_card_eq_n: "⟦ n_nearest_verts w u n U; unvisited_verts u U ≠ {} ⟧
  ⟹ card U = Suc n"
  using nnvs_card_le_n nnvs_card_ge_n le_antisym by blast


subsubsection ‹Reachability and n-nearest vertices›

lemma reachable_subs_nnvs: "⟦ u ∈ verts G; Suc n ≤ card {x. u →⇧* x} ⟧
 ⟹ ∃A ⊆ {x. u →⇧* x}. card A = Suc n ∧ n_nearest_verts w u n A"
proof(induction n)
  case 0
  then have "{u} ⊆ {x. u →⇧* x}" by simp
  with zero_nnvs[OF ‹u ∈ verts G›] show ?case
    by (metis card_Suc_eq card.empty empty_iff)
next
  case (Suc n)
  from Suc.IH[OF Suc.prems(1)] obtain A
    where "A ⊆ {a. u →⇧* a}" and "card A = Suc n" and "n_nearest_verts w u n A"
    using Suc.prems(2) Suc_leD by blast
  note A = this

  show ?case
  proof(cases "Suc n = card {a. u →⇧* a}")
    case True
    with A Suc.prems(2) show ?thesis by linarith
  next
    case False
    with Suc.prems(2) have "Suc n < card {a. u →⇧* a}" by simp
    with A have "∃x ∈ {a. u →⇧* a}. x ∉ A"
      using subset_antisym by fastforce
    then have unvis_non_empty: "unvisited_verts u A ≠ {}"
      unfolding unvisited_verts_def using reachable_in_verts(2) by auto

    let ?A' = "insert (nearest_vert w u A) A"

    note n_nnvs_unvis[OF A(3) unvis_non_empty]
    moreover
    from A(1) have "?A' ⊆ {a. u →⇧* a}"
      using some_unvis_vert[OF unvis_non_empty]
      by (simp add: unvisited_verts_def)
    moreover
    note nearest_vert_not_mem[OF unvis_non_empty]
    with A(2) card.insert[OF nnvs_finite[OF A(3)]] nnvs_finite
    have "card ?A' = Suc (Suc n)" by auto

    ultimately show ?thesis by blast
  qed
qed

corollary all_reachable_eq_nnvs: "⟦ U = {x. u →⇧* x}; card U = Suc n ⟧
 ⟹ n_nearest_verts w u n U"
  using reachable_subs_nnvs reachable_verts_finite reachable_in_verts(1)
  by (metis card_Suc_eq card_subset_eq insertI1 le_Suc_eq mem_Collect_eq)

lemma all_reachable_eq_nnvs_Suc:
  assumes "u ∈ verts G" and "U = {x. u →⇧* x}" and "Suc n ≥ card U"
  shows "n_nearest_verts w u n U"
proof -
  note * = all_reachable_eq_nnvs le_Suc_eq
  show ?thesis using assms
  proof(induction n)
    case 0
    then show ?case using * reachable_verts_finite by auto
  next
    case (Suc n)
    then show ?case using  * n_nnvs_vis unvis_empty by auto
  qed
qed


lemma nnvs_imp_reachable:"⟦ n_nearest_verts w u n A; Suc n ≤ card {x. u →⇧* x} ⟧
 ⟹ A ⊆ {x. u →⇧* x} ∧ card A = Suc n"
proof(induction rule: n_nearest_verts.induct)
  case (zero_nnvs u)
  then show ?case using nearest_vert_reachable by simp
next
  case (n_nnvs_unvis w u n U)
  then show ?case using nearest_vert_reachable
    by (simp add: nearest_vert_not_mem nnvs_finite)
next
  case (n_nnvs_vis w u n U)
  from n_nnvs_vis.hyps(2) have "{a. u →⇧* a} ⊆ U"
    unfolding unvisited_verts_def using reachable_in_verts(2) by auto
  moreover
  from n_nnvs_vis have "U ⊆ {a. u →⇧* a}"
    using Suc_leD by blast
  ultimately show ?case
    using n_nnvs_vis by auto
qed

corollary nnvs_imp_all_reachable:
  "⟦ n_nearest_verts w u n U; Suc n = card {x. u →⇧* x} ⟧
  ⟹ U = {x. u →⇧* x}"
  using nnvs_imp_reachable
  by (simp add: card_subset_eq reachable_verts_finite)

lemma nnvs_imp_all_reachable_Suc:
  assumes "n_nearest_verts w u n U"  "Suc n ≥ card {x. u →⇧* x}"
  shows "U = {x. u →⇧* x}"
  using assms
proof(induction rule: n_nearest_verts.induct)
  case (zero_nnvs u)
  have u_mem: "u ∈ {a. u →⇧* a}" by (simp add: zero_nnvs.hyps)
  moreover
  from u_mem have "card {a. u →⇧* a} = 1"
    using le_Suc_eq reachable_verts_finite zero_nnvs.prems by force
  ultimately show ?case by (metis card_1_singletonE singletonD)
next
  case (n_nnvs_unvis w u n U)
  then show ?case
    by (metis le_Suc_eq n_nearest_verts.n_nnvs_unvis
        nnvs_imp_all_reachable unvis_empty)
next
  case (n_nnvs_vis w u n U)
  then show ?case
    by (metis le_Suc_eq n_nearest_verts.n_nnvs_vis
        nnvs_imp_all_reachable)
qed

lemma nnvs_subs_verts: "n_nearest_verts w u n U ⟹ U ⊆ verts G"
proof(induction rule: n_nearest_verts.induct)
  case (n_nnvs_unvis w u n U)
  then have "nearest_vert w u U ∈ unvisited_verts u U"
    by (simp add: nearest_vert_unvis)
  then have "nearest_vert w u U ∈ verts G"
    unfolding unvisited_verts_def by simp
  with n_nnvs_unvis show ?case by blast
qed auto

subsubsection ‹Relation between n-nearest vertices and k-neighborhood›


lemma unvis_nearest_vert_contr:
  "⟦ n_nearest_verts w u n U; x ∈ U; x ≠ u; y ∈ unvisited_verts u U; μ w u y < μ w u x ⟧
  ⟹ False"
proof(induction rule: n_nearest_verts.induct)
  case (n_nnvs_unvis w u n U)
  then obtain x where x: "x ∈ insert (nearest_vert w u U) U - {u}"
    "∃y∈unvisited_verts u (insert (nearest_vert w u U) U). μ w u y < μ w u x" by blast
  then show ?case
  proof(cases "x = nearest_vert w u U")
    case True
    with n_nnvs_unvis x show ?thesis
      using some_unvis_vert unvis_insert by (metis DiffD1 not_le)
  next
    case False
    with n_nnvs_unvis x show ?thesis
      using unvis_insert by (auto, metis not_le some_unvis_vert(2))
  qed
qed blast

lemma nnvs_subs_k_nh:
  assumes nnvs: "n_nearest_verts w u n U"
      and card_N: "card (k_neighborhood w u k) ≥ n"
    shows "U - {u} ⊆ k_neighborhood w u k"
proof -
  from nnvs_card_le_n[OF nnvs] have card_U: "card (U - {u}) ≤ n"
    using nnvs_mem[OF nnvs] nnvs_finite[OF nnvs] by auto
  show ?thesis
  proof(rule ccontr, auto, rule ccontr)
    fix x assume x: "x ∈ U" "x ∉ k_neighborhood w u k" "x ≠ u"
    then have "{x, u} ⊆ U" using nnvs_mem[OF nnvs] by auto
    from card_mono[OF nnvs_finite[OF nnvs], OF this] have "card U ≥ 2"
      using x(3) by auto
    then have "card (U - {u} - {x}) < card (U - {u})"
      using nnvs nnvs_finite nnvs_mem x(1,3) by auto
    also have "… ≤ card (k_neighborhood w u k)"
      using card_N card_U by linarith
    finally have "card (U - {u} - {x}) < card (k_neighborhood w u k)" .
    then obtain y where y: "y ∈ k_neighborhood w u k" "y ∉ U - {u} - {x}"
      using nnvs_finite[OF nnvs] by (meson card_mono finite_Diff not_le subset_iff)
    from k_nh_reachable[OF y(1)] y x(2) have y_unvis: "y ∈ unvisited_verts u U"
      unfolding unvisited_verts_def k_neighborhood_def by blast

    from y have "μ w u y ≤ k" unfolding k_neighborhood_def by simp
    moreover
    from x have "μ w u x > k" unfolding k_neighborhood_def
      using nnvs_subs_verts[OF nnvs] by fastforce
    ultimately have "μ w u y < μ w u x" by simp
    from unvis_nearest_vert_contr[OF nnvs ‹x ∈ U› ‹x ≠ u› y_unvis this] show "False" .
  qed
qed

lemma k_nh_subs_nnvs:
  assumes nnvs: "n_nearest_verts w u n U"
      and card_nh: "card (k_neighborhood w u k) < card U"
    shows "k_neighborhood w u k ⊆ U"
proof(rule ccontr)
  assume "¬ k_neighborhood w u k ⊆ U"
  then obtain v where v: "v ∈ verts G" "v ≠ u" "μ w u v ≤ k" "v ∉ U"
    unfolding k_neighborhood_def by auto
  then have v_unvis: "v ∈ unvisited_verts u U"
    unfolding unvisited_verts_def
    using μ_reach_conv[of w u v] PInfty_neq_ereal(1)[of k] by force

  let ?close_verts = "{v ∈ verts G. μ w u v ≤ k} - {u}"
  let ?far_verts = "{v ∈ verts G. μ w u v > k} - {u}"

  have vert_part: "verts G - {u} = ?close_verts ∪ ?far_verts"
    "?close_verts ∩ ?far_verts = {}" by auto
  with finite_verts have "finite ?close_verts" and "finite ?far_verts"
    by auto

  have "card (k_neighborhood w u k) ≤ card (U - {u})"
    using card_nh nnvs nnvs_finite nnvs_mem by auto
  then have "card ?close_verts ≤ card (U - {u})"
    unfolding k_neighborhood_def
    by (cases "μ w u u ≤ k") (auto simp: insert_absorb source_mem_nnvs[OF nnvs])

  have "?far_verts ∩ (U - {u}) ≠ {}"
  proof(rule ccontr, simp)
    assume "?far_verts ∩ (U - {u}) = {}"
    then have "U - {u} ⊆ ?close_verts"
      using nnvs_subs_verts[OF nnvs] by auto
    then have "card (U - {u}) ≤ card ?close_verts"
      by (simp add: card_mono)
    with ‹card ?close_verts ≤ card (U - {u})› have "?close_verts = U - {u}"
      using card_seteq[OF ‹finite ?close_verts› ‹U - {u} ⊆ ?close_verts›]
      by blast
    then show "False" using v by auto
  qed
  then obtain x where x: "x ∈ ?far_verts" "x ∈ U" "x ≠ u"
    by auto
  then have "μ w u v < μ w u x" using ‹μ w u v ≤ k› by auto
  from unvis_nearest_vert_contr[OF nnvs x(2,3) v_unvis this]
  show "False" .
qed

end

end