Theory Shortest_Path_Tree

theory Shortest_Path_Tree
  imports "Graph_Theory.Graph_Theory" "Graph_Definitions" "Graph_Theory_Batteries" "Misc"
begin

text ‹
This theory defines the notion of a partial shortest path tree in the locale @{text psp_tree}.
A partial shortest path tree contains the s nearest notes with respect to some weight function.
Since, at the time of writing, the definition of @{const forest} only guarantees acyclicity
and the definition of @{const tree} is also incorrect by extension, we develop our own definition
of a directed tree in the locale @{text directed_tree}.
›

section ‹Directed tree›

text ‹
The following locale defines the notion of a rooted directed tree. The tree property is
established by asserting a unique walk from the root to each vertex. Note that we need
@{const pre_digraph.awalk} and not @{const pre_digraph.apath} here since we want to have only one
incoming arc for each vertex. In the locale all the usual properties of trees are established, e.g.
non-existence of @{const pre_digraph.cycle}, absence of loops with @{locale loopfree_digraph} and
multi-arcs with @{locale nomulti_digraph}.
We also prove the admissibility of an induction rule for finite trees which constructs any tree
inductively by starting with a single node (the root) and consecutively adding leaves.
Finally we define the depth of a tree.
›
locale directed_tree =
    wf_digraph T for T +
fixes
  root :: 'a
assumes
  root_in_T: "root ∈ verts T" and
  unique_awalk: "v ∈ verts T ⟹ ∃!p. awalk root p v"
begin

subsection ‹General properties of trees›

lemma reachable_from_root: "v ∈ verts T ⟹ root →⇧*⇘T⇙ v"
  using unique_awalk reachable_awalkI by blast

lemma non_empty: "verts T ≠ {}"
  using root_in_T by blast

theorem cycle_free: "∄c. cycle c"
proof
  assume "∃c. cycle c"
  then obtain c where c: "cycle c" by blast
  from unique_awalk[of "awhd root c", OF awhd_in_verts[OF root_in_T, of c]]
  obtain p where p: "awalk root p (awhd root c)"
    using c[unfolded cycle_conv] unfolding awalk_conv by auto
  from c p awalk_appendI have "awalk root (p@c) (awhd root c)"
    by (metis awalkE' cycle_def awalk_verts_ne_eq)
  with unique_awalk p c show "False"
    using awalk_last_in_verts unfolding cycle_def by blast
qed

sublocale loopfree: loopfree_digraph T
proof(standard, rule ccontr)
  fix e assume arc: "e ∈ arcs T" and loop: "¬ tail T e ≠ head T e"
  then have "cycle [e]"
    unfolding cycle_conv
    using arc_implies_awalk by force
  with cycle_free show "False" by blast
qed

sublocale nomulti: nomulti_digraph T
proof(standard, rule ccontr, goal_cases)
  case (1 e1 e2)
  let ?u = "tail T e1" and ?v = "head T e1"
  from unique_awalk obtain p where "awalk root p ?u"
    using 1 tail_in_verts by blast
  with 1 have "awalk root (p@[e1]) ?v" and "awalk root (p@[e2]) ?v"
    unfolding arc_to_ends_def
    using arc_implies_awalk by (fastforce)+

  with unique_awalk show "False"
    using ‹e1 ≠ e2› by blast
qed


lemma connected': "⟦ u ∈ verts T; v ∈ verts T ⟧ ⟹ u →⇧*⇘mk_symmetric T⇙ v"
proof -
  let ?T' = "mk_symmetric T"
  fix u v assume "u ∈ verts T" and "v ∈ verts T"
  then have "∃up. awalk root up u" and "∃vp. awalk root vp v"
    using unique_awalk by blast+
  then obtain up vp where up: "awalk root up u" and vp: "awalk root vp v" by blast
  then have "u →⇧*⇘mk_symmetric T⇙ root" and "root →⇧*⇘mk_symmetric T⇙ v"
    by (meson reachable_awalkI reachable_mk_symmetricI
        symmetric_mk_symmetric symmetric_reachable)+
  then show "u →⇧*⇘mk_symmetric T⇙ v"
    by (meson wellformed_mk_symmetric wf_digraph.reachable_trans wf_digraph_wp_iff)
qed

theorem connected: "connected T"
  unfolding connected_def strongly_connected_def
  using connected' root_in_T by auto

lemma unique_awalk_All: "∃p. awalk u p v ⟹ ∃!p. awalk u p v"
proof(rule ccontr, goal_cases)
  case 1
  then have "∃p q. awalk u p v ∧ awalk u q v ∧ p ≠ q"
    by blast
  then obtain p q where
    p: "awalk u p v" and q: "awalk u q v" and "p ≠ q" by blast
  from unique_awalk obtain w where w: "awalk root w u"
    using ‹awalk u p v› by blast
  then have "awalk root (w@p) v" and "awalk root (w@q) v" and "(w@p) ≠ (w@q)"
    using ‹awalk u p v› ‹awalk u q v› ‹p ≠ q› awalk_appendI by auto
  with unique_awalk show ?case by blast
qed

lemma unique_arc:
  shows "u →⇘T⇙ v ⟹ ∃!e ∈ arcs T. tail T e = u ∧ head T e = v"
    and "(∄e. e ∈ arcs T ∧ tail T e = u ∧ head T e = v) ⟹ ¬ u →⇘T⇙ v"
  using unique_awalk_All nomulti.no_multi_arcs unfolding arc_to_ends_def
  by auto

lemma unique_arc_set:
  fixes u v
  defines "A ≡ {e ∈ arcs T. tail T e = u ∧ head T e = v}"
  shows "A = {} ∨ (∃e. A = {e})"
proof(cases "u →⇘T⇙ v")
  case True
  note unique_arc(1)[OF True]
  then show ?thesis unfolding A_def by blast
next
  case False
  then have "∄e. e ∈ arcs T ∧ tail T e = u ∧ head T e = v"
    using in_arcs_imp_in_arcs_ends arcs_ends_def by blast
  then show ?thesis unfolding A_def by auto
qed


lemma sp_eq_awalk_cost: "awalk a p b ⟹ awalk_cost w p = μ w a b"
proof -
  assume "awalk a p b"
  with unique_awalk_All have "{p. awalk a p b} = {p}"
    by blast
  then show ?thesis unfolding μ_def
    by (metis cInf_singleton image_empty image_insert)
qed

lemma sp_cost_finite: "awalk a p b ⟹ μ w a b > -∞ ∧ μ w a b < ∞"
  using sp_eq_awalk_cost[symmetric] by simp

theorem sp_append:
  "⟦ awalk a p b; awalk b q c ⟧ ⟹ μ w a c = μ w a b + μ w b c"
proof -
  assume p: "awalk a p b" and q: "awalk b q c"
  then have p_q: "awalk a (p@q) c" by auto
  then have "awalk_cost w (p@q) = awalk_cost w p + awalk_cost w q"
    using awalk_cost_append by blast

  with p q p_q show ?thesis using sp_eq_awalk_cost
    by (metis plus_ereal.simps(1))
qed

text ‹Convenience lemma which reformulates @{thm sp_append} to use reachability as assumptions.›
lemma sp_append2: "⟦ v1 →⇧*⇘T⇙ v2; v2 →⇧*⇘T⇙ v3 ⟧
  ⟹ μ w v1 v3 = μ w v1 v2 + μ w v2 v3"
  using reachable_awalk sp_append by auto

theorem connected_minimal: "e ∈ arcs T ⟹  ¬ (tail T e) →⇧*⇘(del_arc e)⇙ (head T e)"
proof
  let ?T' = "del_arc e" and ?u = "tail T e" and ?v = "head T e"
  assume "e ∈ arcs T" and "?u →⇧*⇘?T'⇙ ?v"
  note e = this
  then have T'_wf: "wf_digraph ?T'" by blast

  from e have "awalk ?u [e] ?v"
    by (simp add: arc_implies_awalk)
  moreover
  note wf_digraph.reachable_awalk[OF T'_wf, of ?u ?v]
  with e obtain p where p: "pre_digraph.awalk ?T' ?u p ?v" by blast

  from e have "e ∉ arcs ?T'" by simp
  with e p have "e ∉ set p" by (meson T'_wf subsetCE wf_digraph.awalkE')
  with p have "[e] ≠ p" and "awalk ?u p ?v"
    by (auto simp: subgraph_awalk_imp_awalk subgraph_del_arc)

  ultimately show False using unique_awalk_All by blast
qed

lemma All_arcs_in_path: "e ∈ arcs T ⟹ ∃p u v. awalk u p v ∧ e ∈ set p"
  by (meson arc_implies_awalk list.set_intros(1))

subsection ‹An induction rule for finite trees›
text ‹
In this section we develop an induction rule for finite trees. Since this induction rule works by
inductively adding trees we first need to define the notion of a leaf and prove numerous facts
about them.
›

definition (in pre_digraph) leaf :: "'a ⇒ bool" where
  "leaf v ≡ v ∈ verts G ∧ out_arcs G v = {}"

lemma in_degree_root_zero: "in_degree T root = 0"
proof(rule ccontr)
  assume "in_degree T root ≠ 0"
  then obtain e u where e: "tail T e = u" "head T e = root" "u ∈ verts T" "e ∈ arcs T"
    by (metis tail_in_verts all_not_in_conv card.empty in_degree_def in_in_arcs_conv)
  with unique_awalk obtain p where p: "awalk root p u" by blast
  with e have "awalk root (p@[e]) root"
    using awalk_appendI arc_implies_awalk by auto
  moreover
  have "awalk root [] root" by (simp add: awalk_Nil_iff root_in_T)
  ultimately show "False" using unique_awalk by blast
qed

lemma leaf_out_degree_zero: "leaf v ⟹ out_degree T v = 0"
  unfolding leaf_def out_degree_def by auto

lemma two_in_arcs_contr:
  assumes "e1 ∈ arcs T" "e2 ∈ arcs T" and "e1 ≠ e2" and "head T e1 = head T e2"
  shows "False"
proof -
  from unique_awalk assms obtain p1 p2
    where "awalk root p1 (tail T e1)" and "awalk root p2 (tail T e2)"
    by (meson tail_in_verts in_in_arcs_conv)
  with assms have "awalk root (p1@[e1]) (head T e1)" and "awalk root (p2@[e2]) (head T e1)"
    unfolding in_arcs_def
    using arc_implies_awalk by force+
  with unique_awalk ‹e1 ≠ e2› show "False" by blast
qed

lemma in_arcs_finite: "v ∈ verts T ⟹ finite (in_arcs T v)"
proof(rule ccontr)
  assume "¬ finite (in_arcs T v)"
  then obtain e1 e2
    where e1_e2: "e1 ∈ in_arcs T v" "e2 ∈ in_arcs T v" "e1 ≠ e2"
    by (metis finite.emptyI finite_insert finite_subset insertI1 subsetI)
  with two_in_arcs_contr show "False" unfolding in_arcs_def by auto
qed

lemma not_root_imp_in_deg_one: "⟦ v ∈ verts T; v ≠ root ⟧  ⟹ in_degree T v = 1"
proof(rule ccontr)
  assume "v ≠ root" and "v ∈ verts T" and "in_degree T v ≠ 1"
  then have "in_degree T v ≠ 0"
  proof -
    from unique_awalk ‹v ∈ verts T› obtain p where "awalk root p v" by blast
    with ‹v ≠ root› have "root →⇧+⇘T⇙ v" using reachable_awalkI by blast
    then have "∃u. u →⇘T⇙ v" by (meson tranclD2)
    then show ?thesis
      using in_arcs_finite[OF ‹v ∈ verts T›] unfolding in_degree_def
      using card_eq_0_iff by fastforce
  qed
  moreover
  have "¬ in_degree T v ≥ 2"
  proof
    assume in_deg_ge_2: "in_degree T v ≥ 2"
    have "∃e1 e2. e1 ∈ in_arcs T v ∧ e2 ∈ in_arcs T v ∧ e1 ≠ e2"
    proof(cases "in_arcs T v = {}")
      case True
      then show ?thesis using in_deg_ge_2[unfolded in_degree_def] by simp
    next
      case False
      then obtain e1 where "e1 ∈ in_arcs T v" by blast
      then have "card (in_arcs T v) = 1" if "∀e2 ∈ in_arcs T v. e1 = e2"
        using that by(auto simp: card_Suc_eq[where ?A="(in_arcs T v)"])
      then show ?thesis
        using in_deg_ge_2[unfolded in_degree_def] ‹e1 ∈ in_arcs T v› by force
    qed
    with two_in_arcs_contr show "False" unfolding in_arcs_def by auto
  qed
  ultimately show "False" using ‹in_degree T v ≠ 1› by linarith
qed

lemma in_deg_one_imp_not_root: "⟦ v ∈ verts T; in_degree T v = 1 ⟧  ⟹ v ≠ root"
  using in_degree_root_zero by auto

corollary in_deg_one_iff: "v ∈ verts T ⟹ v ≠ root ⟷ in_degree T v = 1"
  using not_root_imp_in_deg_one in_deg_one_imp_not_root by blast

lemma ex_in_arc: "⟦ v ≠ root; v ∈ verts T ⟧ ⟹ ∃e. in_arcs T v = {e}"
  using not_root_imp_in_deg_one unfolding in_degree_def
  by (auto simp: card_Suc_eq)

lemma ex_leaf: "finite (verts T) ⟹ ∃v ∈ verts T. leaf v"
proof(rule ccontr, simp)
  assume verts_fin: "finite (verts T)" and  no_leaves: "∀x∈verts T. ¬ leaf x"
  then have "∀x ∈ verts T. ∃e. e ∈ out_arcs T x"
    unfolding leaf_def by (simp add: out_arcs_def)
  then have "∀x ∈ verts T. ∃x' e. awalk x [e] x'"
    unfolding out_arcs_def using arc_implies_awalk by force
  then have extend: "∃p v'. awalk u (ps@[p]) v'" if "awalk u ps v" for u ps v
    using that by force
  have "∃u p v. awalk u p v ∧ length p = n" for n
  proof(induction n)
    case 0
    from root_in_T have "awalk root [] root"
      by (simp add: awalk_Nil_iff)
    then show ?case by blast
  next
    case (Suc n)
    then obtain u p v where "awalk u p v" and "length p = n" by blast
    from extend[OF this(1)] obtain e v' where "awalk u (p@[e]) v'" and "length (p@[e]) = Suc n"
      using length_append_singleton ‹length p = n› by auto
    then show ?case by blast
  qed
  with awalk_not_distinct[OF verts_fin] have "∃p. cycle p"
    using awalk_cyc_decompE' closed_w_imp_cycle by (metis order_refl)
  with cycle_free show False by blast
qed

lemma verts_finite_imp_arcs_finite: "finite (verts T) ⟹ finite (arcs T)"
proof -
  assume "finite (verts T)"
  then have "finite (verts T × verts T)" by simp
  let ?a = "λ(u,v). {e ∈ arcs T.  tail T e = u ∧ head T e = v}"
  let ?A = "⋃{?a e |e. e ∈ verts T × verts T}"
  have "arcs T ⊆ ?A"
  proof
    fix e assume e: "e ∈ arcs T"
    then have "tail T e ∈ verts T" and "head T e ∈ verts T"
      using wellformed by auto
    with e show "e ∈ ?A" by blast
  qed
  moreover
  have "finite (?a (u,v))" for u v
    using unique_arc_set[of u v] finite.simps by auto
  with finite_Union[OF ‹finite (verts T × verts T)›] have "finite ?A"
    by blast
  ultimately show "finite (arcs T)" using finite_subset by blast
qed

lemma root_leaf_iff: "leaf root ⟷ verts T = {root}"
proof
  from root_in_T show "verts T = {root} ⟹ leaf root"
    using leaf_def ex_leaf by auto
  show "leaf root ⟹ (verts T = {root})"
  proof(rule ccontr)
    assume "leaf root" and "verts T ≠ {root}"
    with non_empty obtain u where u: "u ∈ verts T" "u ≠root"
      by blast
    with unique_awalk obtain p where p: "awalk root p u" by blast
    with ‹u ≠ root› obtain e where e: "e = hd p" "tail T e = root"
      by (metis awalkE' awalk_ends pre_digraph.cas_simp)
    with u p have "e ∈ out_arcs T root" unfolding out_arcs_def
      by (simp, metis awalkE awalk_ends hd_in_set subset_iff)
    with ‹leaf root› show "False"
      unfolding leaf_def out_degree_def by auto
  qed
qed

lemma leaf_not_mem_awalk:
  "⟦ leaf x; awalk u p v; v ≠ x ⟧ ⟹ x ∉ set (awalk_verts u p)"
proof(induction p arbitrary: u)
  case Nil
  then have "u = v" unfolding awalk_conv by simp
  with Nil show ?case by auto
next
  case (Cons a p)
  then have "x ∉ set (awalk_verts (head T a) p)" by (simp add: awalk_Cons_iff)
  moreover
  from Cons.prems have "tail T a ≠ x"
    unfolding leaf_def out_arcs_def by auto
  ultimately show ?case by simp
qed

lemma tree_del_vert:
  assumes "v ≠ root" and "leaf v"
  shows "directed_tree (del_vert v) root"
proof(unfold_locales)
  from ‹v ≠ root› show "root ∈ verts (del_vert v)" using verts_del_vert root_in_T by auto

  have "u∈verts (del_vert v) ⟹ ∃!p. pre_digraph.awalk (del_vert v) root p u" for u
  proof -
    assume "u ∈ verts (del_vert v)"
    then have "u ∈ verts T" "u ≠ v" by (simp_all add: verts_del_vert)
    then obtain p where p: "awalk root p u" "∀p'. awalk root p' u ⟶ p = p'"
    using unique_awalk[OF ‹u ∈ verts T›] by auto
    then have "v ∉ set (awalk_verts root p)"
    using leaf_not_mem_awalk[OF ‹leaf v› _ ‹u ≠ v›] by blast
    with p have
      "pre_digraph.awalk (del_vert v) root p u"
      "∀p'. pre_digraph.awalk (del_vert v) root p' u ⟶ p = p'"
      using awalk_del_vert subgraph_awalk_imp_awalk subgraph_del_vert by blast+
    then show ?thesis by blast
  qed
  then show "⋀va. va ∈ verts (del_vert v)
  ⟹ ∃!p. pre_digraph.awalk (del_vert v) root p va" by blast
qed (meson wf_digraph_del_vert wf_digraph_def)+

lemma arcs_del_leaf:
  assumes e: "e ∈ arcs T" "head T e = v" and v: "leaf v"
  shows "arcs (del_vert v) = arcs T - {e}"
proof -
  from v have "out_arcs T v = {}"
    unfolding pre_digraph.leaf_def by simp
  moreover
  from e v have "v ≠ root"
    using loopfree.no_loops root_leaf_iff by fastforce
  from ex_in_arc[OF this] v have "in_arcs T v = {e}"
    unfolding pre_digraph.leaf_def using e e two_in_arcs_contr by fastforce
  ultimately show ?thesis unfolding out_arcs_def in_arcs_def
    using arcs_del_vert2 by auto
qed

lemma finite_directed_tree_induct[consumes 1, case_names single_vert add_leaf]:
  assumes "finite (verts T)"
  assumes base: "⋀t h root. P ⦇ verts = {root}, arcs = {}, tail = t, head = h ⦈"
      and add_leaf: "⋀T' V A t h u root a v. ⟦T' = ⦇ verts = V, arcs = A, tail = t, head = h ⦈; finite (verts T');
            directed_tree T' root; P T'; u ∈ V; v ∉ V; a ∉ A⟧
    ⟹ P ⦇ verts = V ∪ {v}, arcs = A ∪ {a}, tail = t(a := u), head = h(a := v) ⦈"
    shows "P T"
  using assms(1) directed_tree_axioms
proof(induction "card (verts T)" arbitrary: T root)
  case 0
  then have "verts T = {}" using card_eq_0_iff by simp
  with directed_tree.non_empty[OF ‹directed_tree T root›] show ?case by blast
next
  case (Suc n)
  then interpret tree_T: directed_tree T root by simp
  show ?case
  proof(cases "n = 0")
    case True
    with ‹Suc n = card (verts T)› have "card (verts T) = 1" by simp
    from mem_card1_singleton[OF tree_T.root_in_T this] have "verts T = {root}" .
    then have "arcs T = {}"
      using tree_T.loopfree.no_loops tree_T.tail_in_verts by fastforce
    with ‹verts T = {root}› have "T = ⦇ verts = {root}, arcs = {}, tail = tail T, head = head T ⦈"
      by simp
    with base[of root "tail T" "head T"] show ?thesis by simp
  next
    case False

    from Suc.prems(1) have "finite (verts T)"
      using finite_insert by simp
    from tree_T.ex_leaf[OF this]
    obtain v where v: "tree_T.leaf v" by blast
    with False have "v ≠ root"
      using tree_T.root_leaf_iff Suc.hyps(2) by fastforce
    note v = ‹tree_T.leaf v› ‹v ≠ root›

    let ?T' = "tree_T.del_vert v"
    have T': "?T' = ⦇ verts = verts ?T', arcs = arcs ?T', tail = tail ?T', head = head ?T' ⦈"
      by simp
    note tree_T.tree_del_vert[OF v(2,1)]
    moreover
    have "finite (verts ?T')"
      by (simp add: tree_T.verts_del_vert ‹finite (verts T)›)
    moreover
    from ‹finite (verts ?T')› Suc.hyps(2) Suc.prems(1) have "card (verts ?T') = n"
      using tree_T.verts_del_vert v(1)[unfolded tree_T.leaf_def] by auto
    moreover
    from tree_T.ex_in_arc[OF v(2)]
    obtain e where e: "in_arcs T v = {e}" "tail T e ∈ verts T"
      using v(1)[unfolded tree_T.leaf_def] by force
    then have "tail T e ∈ verts ?T'"
      unfolding in_arcs_def using tree_T.arcs_del_vert[of v]
      using tree_T.loopfree.no_loops tree_T.verts_del_vert[of v]
      using v(1)[unfolded tree_T.leaf_def] by fastforce
    moreover
    from Suc.hyps(1) have "P ?T'" using calculation by blast
    moreover
    note tree_T.verts_del_vert[of v]
    moreover
    from e have "head T e = v" unfolding in_arcs_def by blast
    then have "e ∉ arcs ?T'" unfolding tree_T.arcs_del_vert by simp

    ultimately have "P ⦇ verts = verts ?T' ∪ {v}, arcs = arcs ?T' ∪ {e},
      tail = (tail ?T')(e := (tail T e)), head = (head ?T')(e := v) ⦈"
      using add_leaf[OF T'] by blast
    moreover
    have "T = ⦇ verts = verts ?T' ∪ {v}, arcs = arcs ?T' ∪ {e},
      tail = (tail ?T')(e := (tail T e)), head = (head ?T')(e := v) ⦈"
    proof -
      have "verts T = verts ?T' ∪ {v}"
        using v(1)[unfolded tree_T.leaf_def] tree_T.verts_del_vert[of v] by fastforce
      moreover
      have "arcs ?T' = arcs T - out_arcs T v - in_arcs T v"
        using tree_T.arcs_del_vert2 by fastforce
      with e v(1)[unfolded pre_digraph.leaf_def] have "arcs T = arcs ?T' ∪ {e}" by auto
      moreover
      have "tail T = (tail ?T')(e := (tail T e))"
        by (simp add: tree_T.tail_del_vert)
      moreover
      from e[unfolded in_arcs_def] have "head T = (head ?T')(e := v)"
        using tree_T.head_del_vert ‹head T e = v› by auto
      ultimately show ?thesis by simp
    qed
    ultimately show ?thesis by simp
  qed
qed

text ‹A simple consequence of the induction rule is that a tree with n vertices has n-1 arcs.›
lemma Suc_card_arcs_eq_card_verts:
  assumes "finite (verts T)"
  shows "Suc (card (arcs T)) = card (verts T)"
using assms
proof(induction rule: finite_directed_tree_induct)
  case (single_vert)
  then show ?case by simp
next
  case (add_leaf)
  then show ?case
    using directed_tree.verts_finite_imp_arcs_finite
    by fastforce
qed

subsection ‹Depth of a tree›

definition depth where "depth w ≡ Sup {μ w root v|v. v ∈ verts T}"

context
  fixes w :: "'b weight_fun"
  assumes "∀e ∈ arcs T. w e ≥ 0"
begin

lemma sp_from_root_le: "u →⇧*⇘T⇙ v ⟹ μ w root v ≥ μ w u v"
proof -
  assume "u →⇧*⇘T⇙ v"

  have "μ w root u ≥ 0"
    using ‹∀e∈arcs T. 0 ≤ w e› sp_non_neg_if_w_non_neg by simp
  moreover
  have "root →⇧*⇘T⇙ u"
    using ‹u →⇧*⇘T⇙ v› reachable_from_root reachable_in_verts(1) by auto
  ultimately show ?thesis
    using ‹u →⇧*⇘T⇙ v› sp_append2 ereal_le_add_self2 by auto
qed

lemma depth_lowerB: "v ∈ verts T ⟹ depth w ≥ μ w root v"
proof -
  assume "v ∈ verts T"
  then have "μ w root v ∈ {μ w root v|v. v ∈ verts T}" by auto
  then show "depth w ≥ μ w root v"
    unfolding depth_def by (simp add: Sup_upper)
qed

lemma depth_upperB: "∀v ∈ verts T. μ w root v ≤ d ⟹ depth w ≤ d"
proof -
  assume "∀v ∈ verts T. μ w root v ≤ d"
  then have "∀x ∈ {μ w root v |v. v ∈ verts T}. x ≤ d"
    by auto
  then show ?thesis
    unfolding depth_def using Sup_least by fast
qed

text ‹
This relation between depth of a tree and its diameter is later used to establish the
correctness of the diameter estimate.
›
lemma depth_eq_fin_dia: "fin_digraph T ⟹ depth w = fin_diameter w"
proof -
  assume "fin_digraph T"
  have "∀v ∈ verts T. μ w root v < ∞"
    using μ_reach_conv reachable_from_root by blast
  then have "{μ w root v|v. v ∈ verts T} ⊆ fin_sp_costs w"
    unfolding fin_sp_costs_def using root_in_T by blast
  then have "depth w ≤ fin_diameter w"
    unfolding depth_def fin_diameter_def by (simp add: Sup_subset_mono)
  moreover
  have "¬ depth w < fin_diameter w"
  proof
    assume "depth w < fin_diameter w"
    obtain u v where "μ w u v = fin_diameter w" "u ∈ verts T" "v ∈ verts T"
      using fin_digraph.ex_sp_eq_fin_dia[OF ‹fin_digraph T› non_empty] by blast
    then have "u →⇧*⇘T⇙ v"
      by (metis μ_reach_conv fin_digraph.fin_diameter_finite[OF ‹fin_digraph T›])
    then have "μ w u v ≤ μ w root v" using sp_from_root_le by blast
    also have "… ≤ depth w" using depth_lowerB[OF ‹v ∈ verts T›] by simp
    finally have "fin_diameter w ≤ depth w"
      using ‹μ w u v = fin_diameter w› by simp
    with ‹depth w < fin_diameter w› show False by simp
  qed
  ultimately show ?thesis by simp
qed

end

end

section ‹Subgraph locale›

locale subgraph =
    G: wf_digraph G for T G +
assumes
  sub_G: "subgraph T G"
begin

sublocale wf_digraph T
  using sub_G unfolding subgraph_def by blast

lemma awalk_sub_imp_awalk:
  "awalk a p b ⟹ G.awalk a p b"
  using G.subgraph_awalk_imp_awalk sub_G by force

end

section ‹Partial shortest path three›

locale psp_tree =
  directed_tree T source + subgraph T G for G T w source n +
  assumes
    source_in_G: "source ∈ verts G" and
    partial: "G.n_nearest_verts w source n (verts T)" and
    sp: "u ∈ verts T ⟹ μ w source u = G.μ w source u"
begin

text ‹
Here we formalize the notion of a partial shortest path tree. This is a shortest path tree where
only the @{term n} nearest nodes in the graph @{term G} are explored.
Consequently, a partial shortest path tree is a subtree of the complete shortest path tree.
We can obtain the complete shortest path tree by choosing n to be larger than the cardinality
of the graph @{term G}.
›

sublocale fin_digraph T
proof(unfold_locales)
  show "finite (verts T)" using G.nnvs_finite[OF partial] .
  from verts_finite_imp_arcs_finite[OF this] show "finite (arcs T)" .
qed

lemma card_verts_le: "card (verts T) ≤ Suc n"
  using G.nnvs_card_le_n partial by auto

lemma reachable_subs: "{x. r →⇧*⇘T⇙ x} ⊆ {x. r →⇧*⇘G⇙ x}"
  by (simp add: Collect_mono G.reachable_mono sub_G)

text ‹The following lemma proves that we explore all nodes if we set @{term n} large enough.›
lemma sp_tree:
  assumes "fin_digraph G"
  assumes card_reachable: "Suc n ≥ card {x. source →⇧*⇘G⇙ x}"
  shows "verts T = {x. source →⇧*⇘G⇙ x}"
  using fin_digraph.nnvs_imp_all_reachable_Suc[OF ‹fin_digraph G› partial card_reachable] .

corollary sp_tree2:
  assumes "fin_digraph G"
  assumes "Suc n ≥ card (verts G)"
  shows "verts T = {x. source →⇧*⇘G⇙ x}"
proof -
  have "{x. source →⇧*⇘G⇙ x} ⊆ verts G"
    using source_in_G G.reachable_in_verts(2) by blast
  then have "Suc n ≥ card {x. source →⇧*⇘G⇙ x}"
    using ‹Suc n ≥ card (verts G)› fin_digraph.finite_verts[OF ‹fin_digraph G›]
    by (meson card_mono dual_order.trans)
  from sp_tree[OF ‹fin_digraph G› this] show ?thesis .
qed

lemma strongly_con_imp_card_verts_eq:
  assumes "fin_digraph G"
  assumes "strongly_connected G"
  assumes card_verts: "Suc n ≤ card (verts G)"
  shows "card (verts T) = Suc n"
proof -
  have verts_G: "verts G = {x. source →⇧*⇘G⇙ x}"
    using G.strongly_con_imp_reachable_eq_verts
      [OF source_in_G ‹strongly_connected G›, symmetric] .
  with card_verts have "Suc n ≤ card {x. source →⇧*⇘G⇙ x}" by simp

  from fin_digraph.nnvs_imp_reachable[OF ‹fin_digraph G› partial this]
  show ?thesis by blast
qed

lemma depth_fin_dia_lB:
  assumes "∀e ∈ arcs G. w e ≥ 0"
  shows "depth w ≤ G.fin_diameter w"
proof(rule ccontr)
  assume "¬ depth w ≤ G.fin_diameter w"
  then have "depth w > G.fin_diameter w"
    by auto
  then have "∃v ∈ verts T. μ w source v > G.fin_diameter w"
    unfolding depth_def by (auto simp: less_Sup_iff)
  then obtain v where v: "v ∈ verts T" "v ∈ verts G" "μ w source v > G.fin_diameter w"
    using sub_G by blast
  moreover
  have "μ w source v < ∞"
    using reachable_from_root μ_reach_conv v(1) by blast
  ultimately show "False"
    using source_in_G G.fin_dia_lowerB[OF source_in_G ‹v ∈ verts G›] sp v
    by (simp add: leD)
qed

end

end