Theory Dist

theory Dist
  imports Enat_Misc Vwalk
begin

section ‹Distances›

subsection ‹Distance from a vertex›

definition distance::"('v × 'v) set ⇒ 'v ⇒ 'v ⇒ enat" where
  "distance G u v = ( INF p. if Vwalk.vwalk_bet G u p v then length p - 1 else ∞)"

lemma vwalk_bet_dist:
  "Vwalk.vwalk_bet G u p v ⟹ distance G u v ≤ length p - 1"
  by (auto simp: distance_def image_def intro!: complete_lattice_class.Inf_lower enat_ile)

lemma reachable_dist:
  "reachable G u v ⟹ distance G u v < ∞"
  apply(clarsimp simp add: reachable_vwalk_bet_iff)
  by (auto simp: distance_def image_def intro!: complete_lattice_class.Inf_lower enat_ile)

lemma unreachable_dist:
  "¬reachable G u v ⟹ distance G u v = ∞"
  apply(clarsimp simp add: reachable_vwalk_bet_iff)
  by (auto simp: distance_def image_def intro!: complete_lattice_class.Inf_lower enat_ile)

lemma dist_reachable:
  "distance G u v < ∞ ⟹ reachable G u v"
  using wellorder_InfI       
  by(fastforce simp: distance_def image_def reachable_vwalk_bet_iff)    

lemma reachable_dist_2:
  assumes "reachable G u v"
  obtains p where "Vwalk.vwalk_bet G u p v" "distance G u v = length p - 1"
  using assms
  apply(clarsimp simp add: reachable_vwalk_bet_iff distance_def image_def)
  by (smt (verit, del_insts) Collect_disj_eq Inf_lower enat_ile mem_Collect_eq not_infinity_eq wellorder_InfI)

lemma triangle_ineq_reachable: 
  assumes "reachable G u v" "reachable G v w"
  shows "distance G u w ≤ distance G u v + distance G v w"
proof-
  obtain p q
    where p_q: "vwalk_bet G u p v" "distance G u v = length p - 1"
          "vwalk_bet G v q w" "distance G v w = length q - 1"
    using assms 
    by (auto elim!: reachable_dist_2)
  hence "vwalk_bet G u (p @ tl q) w"
    by(auto intro!: vwalk_bet_transitive)
  hence "distance G u w ≤ length (p @ tl q) - 1"
    by (auto dest!: vwalk_bet_dist)
  moreover have "length (p @ tl q) = length p + (length q - 1)"
    using ‹vwalk_bet G v q w›
    by (cases q; auto)
  ultimately have "distance G u w ≤ length p + (length q - 1) - 1"
    by (auto simp: eval_nat_numeral)
  thus ?thesis
    using p_q(1)
    by(cases p; auto simp add: p_q(2,4) eval_nat_numeral)
qed

lemma triangle_ineq:
  "distance G u w ≤ distance G u v + distance G v w"
proof(cases "reachable G u v")
  case reach_u_v: True
  then show ?thesis
  proof(cases "reachable G v w")
    case reach_v_w: True
    then show ?thesis
      using triangle_ineq_reachable reach_u_v reach_v_w
      by auto
  next
    case not_reach_v_w: False
    hence "distance G v w = ∞"
      by (simp add: unreachable_dist) 
    then show ?thesis
      by simp
  qed
next
  case not_reach_u_v: False
  hence "distance G u v = ∞"
    by (simp add: unreachable_dist) 
  then show ?thesis
    by simp
qed


lemma distance_split:
  "⟦distance G u v ≠ ∞; distance G u v = distance G u w + distance G w v ⟧ ⟹
       ∃w'. reachable G u w' ∧ distance G u w' = distance G u w ∧
            reachable G w' v ∧ distance G w' v = distance G w' v"
  by (metis dist_reachable enat_ord_simps(4) plus_eq_infty_iff_enat)

lemma dist_inf: "v ∉ dVs G ⟹ distance G u v = ∞"
proof(rule ccontr, goal_cases)
  case 1
  hence "reachable G u v"
    by(auto intro!: dist_reachable)
  hence "v ∈dVs G"
    by (simp add: reachable_in_dVs(2))
  then show ?case
    using 1
    by auto
qed

lemma dist_inf_2: "v ∉ dVs G ⟹ distance G v u = ∞"
proof(rule ccontr, goal_cases)
  case 1
  hence "reachable G v u"
    by(auto intro!: dist_reachable)
  hence "v ∈dVs G"
    by (simp add: reachable_in_dVs(1))
  then show ?case
    using 1
    by auto
qed

lemma dist_eq: "⟦⋀p. Vwalk.vwalk_bet G' u p v ⟹ Vwalk.vwalk_bet G u (map f p) v⟧ ⟹
                   distance G u v ≤ distance G' u v"
  apply(auto simp: distance_def image_def intro!: Inf_lower)
  apply (smt (verit, ccfv_threshold) Un_iff length_map mem_Collect_eq wellorder_InfI)
  by (meson vwalk_bet_nonempty')

lemma distance_subset: "G ⊆ G' ⟹ distance G' u v ≤ distance G u v"
  by (metis enat_ord_simps(3) reachable_dist_2 unreachable_dist vwalk_bet_dist vwalk_bet_subset)


lemma distance_neighbourhood:
  "⟦v ∈ neighbourhood G u⟧ ⟹ distance G u v ≤ 1"
proof(goal_cases)
  case 1
  hence "vwalk_bet G u [u,v] v"
    by auto
  moreover have "length [u,v] = 2"
    by auto
  ultimately show ?case
    by(force dest!: vwalk_bet_dist simp: one_enat_def)
qed

subsection ‹Shortest Paths›

definition shortest_path::"('v × 'v) set ⇒ 'v ⇒ 'v list ⇒ 'v ⇒ bool" where
  "shortest_path G u p v = (distance G u v = length p -1 ∧ vwalk_bet G u p v)"

lemma shortest_path_props[elim]:
  "shortest_path G u p v ⟹ (⟦distance G u v = length p -1; vwalk_bet G u p v⟧ ⟹ P) ⟹ P"
  by (auto simp: shortest_path_def)

lemma shortest_path_intro:
  "⟦distance G u v = length p -1; vwalk_bet G u p v⟧ ⟹ shortest_path G u p v"
  by (auto simp: shortest_path_def)

lemma shortest_path_vwalk: "shortest_path G u p v ⟹ vwalk_bet G u p v"
  by(auto simp: shortest_path_def)

lemma shortest_path_dist: "shortest_path G u p v ⟹ distance G u v = length p - 1"
  by(auto simp: shortest_path_def)

lemma shortest_path_split_1:
  "⟦shortest_path G u (p1 @ x # p2) v⟧ ⟹ shortest_path G x (x # p2) v"
proof(goal_cases)
  case 1
  hence "vwalk_bet G u (p1 @ [x]) x" "vwalk_bet G x (x # p2) v"
    by (auto dest!: shortest_path_vwalk simp: split_vwalk vwalk_bet_pref)

  hence "reachable G x v" "reachable G u x"
    by (auto dest: reachable_vwalk_betD) 


  have "distance G x v ≥ length (x # p2) - 1"
  proof(rule ccontr, goal_cases)
    case 1
    moreover from ‹reachable G x v›
    obtain p where "vwalk_bet G x p v" "distance G x v = enat (length p - 1)"
      by (rule reachable_dist_2)
    ultimately have "length p - 1 < length (x # p2) - 1"
      by auto 
    hence "length (p1 @ p) - 1 < length (p1 @ x # p2) - 1"
      by auto

    have "vwalk_bet G u ((p1 @ [x]) @ (tl p)) v"
      using ‹vwalk_bet G u (p1 @ [x]) x› ‹vwalk_bet G x p v› 
      by (fastforce intro: vwalk_bet_transitive)
    moreover have "p = x # (tl p)"
      using ‹vwalk_bet G x p v› 
      by (fastforce dest: hd_of_vwalk_bet)
    ultimately have "distance G u v ≤ length (p1 @ p) -1"
      using vwalk_bet_dist
      by fastforce
    moreover have "distance G u v = length (p1 @ x # p2) - 1"
      using ‹shortest_path G u (p1 @ x # p2) v›
      by (rule shortest_path_dist)
    ultimately show ?case
      using ‹length (p1 @ p) - 1 < length (p1 @ x # p2) - 1›
      by auto 
  qed
  moreover have "distance G x v ≤ length (x # p2) - 1"
    using ‹vwalk_bet G x (x # p2) v›
    by (force intro!: vwalk_bet_dist)

  ultimately show ?case
    using ‹vwalk_bet G x (x # p2) v›
    by (auto simp: shortest_path_def)
qed

lemma shortest_path_split_2:
  "⟦shortest_path G u (p1 @ x # p2) v⟧ ⟹ shortest_path G u (p1 @ [x]) x"
proof(goal_cases)
  case 1
  hence "vwalk_bet G u (p1 @ [x]) x" "vwalk_bet G x (x # p2) v"
    by (auto dest!: shortest_path_vwalk simp: split_vwalk vwalk_bet_pref)

  hence "reachable G x v" "reachable G u x"
    by (auto dest: reachable_vwalk_betD) 

  have "distance G u x ≥ length (p1 @ [x]) - 1"
  proof(rule ccontr, goal_cases)
    case 1
    moreover from ‹reachable G u x›
    obtain p where "vwalk_bet G u p x" "distance G u x = enat (length p - 1)"
      by (rule reachable_dist_2)
    ultimately have "length p - 1 < length (p1 @ [x]) - 1"
      by auto 
    hence "length (p @ p2) - 1 < length (p1 @ x # p2) - 1"
      by auto
    have "vwalk_bet G u (butlast p @ x # p2) v"
      using ‹vwalk_bet G u p x› ‹vwalk_bet G x (x # p2) v› 
      by (simp add: vwalk_bet_transitive_2)
    moreover have "p = (butlast p) @ [x]"
      using ‹vwalk_bet G u p x› 
      by (fastforce dest: last_of_vwalk_bet')
    moreover have "length p > 0"
      using ‹vwalk_bet G u p x›
      by force
    ultimately have "distance G u v ≤ length (p @ p2) -1"
      by (auto dest!: vwalk_bet_dist simp: neq_Nil_conv)
    moreover have "distance G u v = length (p1 @ x # p2) - 1"
      using ‹shortest_path G u (p1 @ x # p2) v›
      by (rule shortest_path_dist)
    ultimately show ?case
      using ‹length (p @ p2) - 1 < length (p1 @ x # p2) - 1›
      by auto 
  qed
  moreover have "distance G u x ≤ length (p1 @ [x]) - 1"
    using ‹vwalk_bet G u (p1 @ [x]) x›
    by (force intro!: vwalk_bet_dist)

  ultimately show ?case
    using ‹vwalk_bet G u (p1 @ [x]) x›
    by (auto simp: shortest_path_def)
qed

lemma shortest_path_split_distance:
  "⟦shortest_path G u (p1 @ x # p2) v⟧ ⟹ distance G u x ≤ distance G u v"
  using shortest_path_split_2[where G = G and u = u and ?p1.0 = p1 and x = x] shortest_path_dist
  by force

lemma shortest_path_split_distance':
  "⟦x ∈ set p; shortest_path G u p v⟧ ⟹ distance G u x ≤ distance G u v"
  apply(subst (asm) in_set_conv_decomp_last)
  using shortest_path_split_distance
  by auto 

lemma shortest_path_exists:
  assumes "reachable G u v"
  obtains p where "shortest_path G u p v"
  using assms 
  by (force elim!: reachable_dist_2 simp: shortest_path_def)

lemma shortest_path_exists_2:
  assumes "distance G u v < ∞"
  obtains p where "shortest_path G u p v"
  using assms 
  by (force dest!: dist_reachable elim!: shortest_path_exists simp: shortest_path_def)

lemma not_distinct_props: 
  "¬distinct xs ⟹ (⋀x1 x2 xs1 xs2 xs3. ⟦xs = xs1 @ x1# xs2 @ x2 # xs3; x1 = x2⟧ ⟹ P) ⟹ P"
  using not_distinct_decomp
  by fastforce

lemma shortest_path_distinct:
  "shortest_path G u p v ⟹ distinct p"
  apply(erule shortest_path_props)
  apply(rule ccontr)
  apply(erule not_distinct_props)
proof(goal_cases)
  case (1 x1 x2 xs1 xs2 xs3)
  hence "Vwalk.vwalk_bet G u (xs1 @ x2 # xs3) v"
    using vwalk_bet_transitive_2 closed_vwalk_bet_decompE
    by (smt (verit, best) butlast_snoc)
  hence "distance G u v ≤ length (xs1 @ x2 # xs3) - 1"
    using vwalk_bet_dist
    by force
  moreover have "length (xs1 @ x2 # xs3) < length p"
    by(auto simp: ‹ p = xs1 @ x1 # xs2 @ x2 # xs3›)
  ultimately show ?case
    using ‹distance G u v = enat (length p - 1)›
    by auto
qed

lemma diet_eq': "⟦⋀p. shortest_path G' u p v ⟹ shortest_path G u (map f p) v⟧ ⟹
                   distance G u v ≤ distance G' u v"
  apply(auto simp: shortest_path_def)
  by (metis One_nat_def Orderings.order_eq_iff order.strict_implies_order reachable_dist
            reachable_dist_2 unreachable_dist)

lemma distance_0:
  "(u = v ∧ v ∈ dVs G) ⟷ distance G u v = 0"
proof(safe, goal_cases)
  case 1
  hence "vwalk_bet G v [v] v"
    by auto
  moreover have "length [v] = 1"
    by auto
  ultimately show ?case
    using zero_enat_def
    by(auto dest!: vwalk_bet_dist simp: )
next
  case 2
  hence "distance G u v < ∞"
    by auto
  then obtain p where "shortest_path G u p v"
    by(erule shortest_path_exists_2)
  hence "length p = 1" "vwalk_bet G u p v"
    using ‹distance G u v = 0›
    apply (auto simp: shortest_path_def)
    by (metis diff_Suc_Suc diff_zero enat_0_iff(2) hd_of_vwalk_bet length_Cons)
  then obtain x where "p = [x]"
    by (auto simp: length_Suc_conv)
  then have "x = u" "x = v" "x ∈ dVs G"
    using ‹vwalk_bet G u p v› hd_of_vwalk_bet last_of_vwalk_bet
    by (fastforce simp: vwalk_bet_in_vertices)+
  then show "u = v"  "v ∈ dVs G"
    by auto
qed

lemma distance_neighbourhood':
  "⟦v ∈ neighbourhood G u⟧ ⟹ distance G x v ≤ distance G x u + 1"
  using triangle_ineq distance_neighbourhood
  by (metis add.commute add_mono_thms_linordered_semiring(3) order_trans)



lemma Suc_le_length_iff_2:
  "(Suc n ≤ length xs) = (∃x ys. xs = ys @ [x] ∧ n ≤ length ys)"
  by (metis Suc_le_D Suc_le_mono length_Suc_conv_rev)

lemma distance_parent: 
  "⟦distance G u v < ∞; u ≠ v⟧ ⟹ 
     ∃w. distance G u w + 1 = distance G u v ∧ v ∈ neighbourhood G w"
proof(goal_cases)
  case 1
  then obtain p where "shortest_path G u p v"
    by(force dest!: dist_reachable elim!: shortest_path_exists)
  hence "length p ≥ 2"
    using ‹u≠v› 
    by(auto dest!: shortest_path_vwalk simp: Suc_le_length_iff eval_nat_numeral elim: vwalk_betE)
  then obtain p' x y where "p = p' @ [x, y]"
    by(auto simp: Suc_le_length_iff_2 eval_nat_numeral)

  hence "shortest_path G u (p' @ [x]) x"
    using ‹shortest_path G u p v› 
    by (fastforce dest: shortest_path_split_2)

  hence "distance G u x + 1 = distance G u v"
    using ‹shortest_path G u p v› ‹p = p' @ [x,y]›
    by (auto dest!: shortest_path_dist simp: eSuc_plus_1)
  moreover have "y = v"
    using ‹shortest_path G u p v› ‹p = p' @ [x,y]› 
    by(force simp: ‹p = p' @ [x,y]› dest!: shortest_path_vwalk intro!: vwalk_bet_snoc[where p = "p' @ [x]"])
  moreover have "y ∈ neighbourhood G x"
    using ‹shortest_path G u p v› ‹p = p' @ [x,y]› vwalk_bet_suffix_is_vwalk_bet
    by(fastforce simp: ‹p = p' @ [x,y]› dest!: shortest_path_vwalk)
  ultimately show ?thesis
    by auto
qed

subsection ‹Distance from a set of vertices›

definition distance_set::"('v × 'v) set ⇒ 'v set ⇒ 'v ⇒ enat" where 
  "distance_set G U v = ( INF u∈U. distance G u v)"

(*TODO: intro rule*)

lemma dist_set_inf: "v ∉ dVs G ⟹ distance_set G U v = ∞"
  by(auto simp: distance_set_def INF_eqI dist_inf)

lemma dist_set_mem[intro]: "u ∈ U ⟹ distance_set G U v ≤ distance G u v"
  by (auto simp: distance_set_def wellorder_Inf_le1)

lemma dist_not_inf'': "⟦distance_set G U v ≠ ∞; u∈U; distance G u v = distance_set G U v⟧
                       ⟹ ∃p. vwalk_bet G u (u#p) v ∧ length p = distance G u v ∧
                               set p ∩ U = {}"
proof(goal_cases)
  case main: 1
  then obtain p where "vwalk_bet G u (u#p) v" "length p = distance G u v"
    by (metis dist_reachable enat_ord_simps(4) hd_of_vwalk_bet length_tl list.sel(3) reachable_dist_2)
  moreover have "set p ∩ U = {}"
  proof(rule ccontr, goal_cases)
    case 1
    then obtain p1 w p2 where "p = p1 @ w # p2" "w ∈ U"
      by (auto dest!: split_list)
    hence "length (w#p2) < length (u#p)"
      by auto
    moreover have "vwalk_bet G w (w#p2) v"
      using ‹p = p1 @ w # p2› ‹vwalk_bet G u (u # p) v›
            split_vwalk vwalk_bet_cons
      by fastforce
    hence "distance G w v ≤ length p2"
      by(auto dest!: vwalk_bet_dist) 
    ultimately have "distance_set G U v ≤ length p2"
      using ‹w ∈ U› 
      by(auto dest!: dist_set_mem dest: order.trans)
    moreover have "length p ≤ distance_set G U v"
      by (simp add: ‹enat (length p) = distance G u v› main(3))
    moreover have " enat (length p2) < eSuc (enat (length p1 + length p2))"
      by auto
    ultimately have False
      using leD
      apply -
      apply(drule dual_order.trans[where c = "enat (length p)"])
      by (fastforce simp: ‹p = p1 @ w # p2› dest: )+
    then show ?case
      by auto
  qed
  ultimately show ?thesis
    by auto
qed

lemma dist_not_inf''':
  "⟦distance_set G U v ≠ ∞; u∈U; distance G u v = distance_set G U v⟧
      ⟹ ∃p. shortest_path G u (u#p) v ∧ set p ∩ U = {}"
  apply (simp add: shortest_path_def)
  by (metis dist_not_inf'' enat.distinct(1))

(*lemma distance_set_split:
  "⟦distance_set G U v ≠ ∞; distance_set G U v = distance_set G U w + distance_set G U' v; w ∈ U' ⟧ ⟹
       ∃w'∈U'. reachable G u w' ∧ distance G u w' = distance G u w ∧
            reachable G w' v ∧ distance G w' v = distance G w' v"
proof(goal_cases)
  case 1
  hence "distance_set G U' v ≠ ∞"
    by (simp add: plus_eq_infty_iff_enat)
  then obtain w' where "w' ∈ U'" "distance_set G U' v = distance G w' v" "reachable G w' v"
    using 1
    by (metis dist_not_inf')
*)

lemma distance_set_union:
  "distance_set G (U ∪ V) v ≤ distance_set G U v"
  by (simp add: distance_set_def INF_superset_mono)   

lemma lt_lt_infnty: "x < (y::enat) ⟹ x < ∞"
  using enat_ord_code(3) order_less_le_trans
  by blast

lemma finite_dist_nempty:
  "distance_set G V v ≠ ∞ ⟹ V ≠ {}"
  by (auto simp: distance_set_def top_enat_def)

lemma distance_set_wit: 
  assumes "v ∈ V"
  obtains v' where "v' ∈ V" "distance_set G V x = distance G v' x"
  using assms wellorder_InfI[of "distance G v x" "(%v. distance G v x) ` V"]
  by (auto simp: distance_set_def image_def dest!: )

lemma distance_set_wit':
  assumes "distance_set G V v ≠ ∞"
  obtains v' where "v' ∈ V" "distance_set G V x = distance G v' x"
  using finite_dist_nempty[OF assms]
  by (auto elim: distance_set_wit)

lemma dist_set_not_inf: "distance_set G U v ≠ ∞ ⟹ ∃u∈U. distance G u v = distance_set G U v"
  using distance_set_wit'
  by metis

lemma dist_not_inf': "distance_set G U v ≠ ∞ ⟹
                        ∃u∈U. distance G u v = distance_set G U v ∧ reachable G u v"
  by (metis dist_reachable dist_set_not_inf enat_ord_simps(4))

lemma distance_on_vwalk:
  "⟦distance_set G U v = distance G u v; u ∈ U; shortest_path G u p v; w ∈ set p⟧
       ⟹ distance_set G U w = distance G u w"
proof(goal_cases)
  case assms: 1
  hence "distance_set G U w ≤ distance G u w"
    by (auto intro: dist_set_mem)
  moreover have "distance G u w ≤ distance_set G U w"
  proof(rule ccontr, goal_cases)
    case dist_gt: 1
    hence "distance_set G U w ≠ ∞"
      using lt_lt_infnty
      by (auto simp: linorder_class.not_le)
    then obtain u' where "u' ∈ U" "distance G u' w < distance G u w"
      using dist_gt 
      by (fastforce dest!: dist_set_not_inf)
    moreover then obtain p' where "shortest_path G u' p' w"
      by (fastforce dest: lt_lt_infnty elim!: shortest_path_exists_2)
    moreover obtain p1 p2 where "p = p1 @ [w] @ p2"
      using ‹w ∈ set p›              
      by(fastforce dest: iffD1[OF in_set_conv_decomp_first])
    ultimately have "vwalk_bet G u' (p' @ tl ([w] @ p2)) v"
      using ‹shortest_path G u p v› 
      apply -
      apply (rule vwalk_bet_transitive)
      by(auto dest!: shortest_path_vwalk shortest_path_split_1)+
    moreover have "shortest_path G u (p1 @[w]) w"
      using ‹shortest_path G u p v›
      by(auto dest!: shortest_path_split_2 simp: ‹p = p1 @ [w] @ p2›) 
    hence "length (p' @ tl ([w] @ p2)) - 1 < length p - 1"
      using ‹shortest_path G u' p' w› ‹distance G u' w < distance G u w›
      by(auto dest!: shortest_path_dist simp: ‹p = p1 @ [w] @ p2›)
    hence "length (p' @ tl ([w] @ p2)) - 1 < distance_set G U v"
      using assms(1,3) shortest_path_dist
      by force
    ultimately show False
      using dist_set_mem [OF ‹u' ∈ U›]
      apply -
      apply(drule vwalk_bet_dist)
      by (meson leD order_le_less_trans)
  qed
  ultimately show ?thesis
    by auto
qed

lemma diff_le_self_enat: "m - n ≤ (m::enat)"
  by (metis diff_le_self enat.exhaust enat_ord_code(1) idiff_enat_enat idiff_infinity idiff_infinity_right order_refl zero_le)

lemma shortest_path_dist_set_union:
  "⟦distance_set G U v = distance G u v; u ∈ U; shortest_path G u (p1 @ x # p2) v;
     x ∈ V; ⋀v'. v' ∈ V ⟹ distance_set G U v' = distance G u x⟧
       ⟹ distance_set G (U ∪ V) v = distance_set G U v - distance G u x"
proof(goal_cases)
  case assms: 1
  define k where "k = distance G u x"
  have "distance_set G (U ∪ V) v ≤ distance_set G U v - k"
  proof-
    have "vwalk_bet G x (x#p2) v"
      using ‹shortest_path G u (p1 @ x # p2) v›
      by(auto dest: shortest_path_vwalk split_vwalk)
    moreover have ‹x ∈ U ∪ V›
      using ‹x ∈ V›
      by auto
    ultimately have "distance_set G (U ∪ V) v ≤ length (x # p2) - 1"
      by(auto simp only: dest!: vwalk_bet_dist dist_set_mem dest: order_trans) 
    moreover have "length p1 = k"
    proof-
      have "shortest_path G u (p1 @ [x]) x"
        using ‹shortest_path G u (p1 @ x # p2) v›
        by(auto intro: shortest_path_split_2)
      moreover have "distance_set G U x = k"
        using assms
        by (auto simp: k_def)
      ultimately have "length (p1 @ [x]) - 1 = k"
        using assms(1,2,3) distance_on_vwalk shortest_path_dist
        by fastforce        
      thus ?thesis
        by auto
    qed
    hence "(distance_set G U v) - k = length (x#p2) - 1"
      using ‹shortest_path G u (p1 @ x # p2) v›
      by(auto dest!: shortest_path_dist simp: ‹distance_set G U v = distance G u v›)
    ultimately show ?thesis
      by auto
  qed
  moreover have "distance_set G (U ∪ V) v ≥ distance_set G U v - k"
  proof(rule ccontr, goal_cases)
    case dist_lt: 1
    hence "distance_set G (U ∪ V) v ≠ ∞"
      using lt_lt_infnty
      by (auto simp: linorder_class.not_le)
    then obtain u' where "u' ∈ U ∪ V" "distance G u' v < distance_set G U v - k"
      using dist_lt
      by (fastforce dest!: dist_set_not_inf)
    then consider "u' ∈ U" | "u' ∈ V"
      by auto
    then show ?case
    proof(cases)
      case 1
      moreover from ‹distance G u' v < distance_set G U v - k›
      have ‹distance G u' v < distance_set G U v›
        using diff_le_self_enat order_less_le_trans
        by blast
      ultimately show ?thesis
        by(auto simp: dist_set_mem leD)
    next
      case 2
      moreover from ‹distance G u' v < distance_set G U v - k›
      obtain p2 where "shortest_path G u' p2 v"
        by(auto elim!: shortest_path_exists_2 dest: lt_lt_infnty)
      have "distance_set G U u' = k"
        using assms 2
        by (auto simp: k_def)
      moreover have ‹k ≠ ∞›
        using assms 
        by (fastforce simp: k_def dest: shortest_path_split_2 shortest_path_dist )
      ultimately obtain u where "u ∈ U" "distance G u u' = k"
        by(fastforce dest!: dist_set_not_inf)
      moreover have "distance G u v ≤ distance G u u' + distance G u' v"
        using ‹k ≠ ∞› lt_lt_infnty[OF ‹distance G u' v < distance_set G U v - k›] ‹distance G u u' = k›
        by(auto intro!: triangle_ineq simp: dist_reachable)
      ultimately have "distance G u v ≤ k + distance G u' v"
        by auto
      hence "distance G u v < k + (distance_set G U v - k)"
        using ‹distance G u' v < distance_set G U v - k›
        by (meson ‹k ≠ ∞› dual_order.strict_trans2 enat_add_left_cancel_less)
      moreover have "k ≤ distance_set G U v"
        using assms(1,3) shortest_path_split_distance
        by (fastforce simp: k_def)
      hence "k + (distance_set G U v - k) ≤ distance_set G U v"
        by (simp add: ‹k ≠ ∞› add_diff_assoc_enat)
      ultimately have "distance G u v < distance_set G U v "
        by auto
      then show ?thesis
        using ‹u ∈ U›
        by (simp add: dist_set_mem leD)
    qed
  qed
  ultimately show ?case
    by (auto simp: k_def)
qed
                   
lemma Inf_enat_def1:
  fixes K::"enat set"
  assumes "K ≠ {}"
  shows "Inf K ∈ K"
  using assms
  by (auto simp add: Min_def Inf_enat_def) (meson LeastI)

lemma INF_plus_enat:
  "V ≠ {} ⟹ (INF v∈V. (f::'a ⇒ enat) v) + (x::enat) = (INF v∈V. f v + x)"
proof(goal_cases)
  case assms: 1
  have "(INF v∈V. (f::'a ⇒ enat) v) + (x::enat) ≤ f_v" if "f_v ∈ {f v + x | v . v∈V}" for f_v
    using that
    apply(auto simp: image_def)
    by (metis (mono_tags, lifting) Inf_lower mem_Collect_eq)
  moreover have "(INF v∈V. (f::'a ⇒ enat) v) + (x::enat) ∈ {f v + x | v . v∈V}"
  proof-
    have "Inf {f v | v. v ∈ V} ∈ {f v | v. v ∈ V}"
      apply (rule Inf_enat_def1)
      using assms
      by simp

    then obtain v where "v ∈ V" "Inf {f v | v. v ∈ V} = f v"
      using assms
      by auto
    hence "f v + 1 ∈ {f v + 1 | v. v ∈ V}"
      by auto
    hence "Inf {f v | v. v ∈ V} + x ∈ {f v + x | v. v ∈ V}"
      apply(subst ‹Inf {f v | v. v ∈ V} = f v›)
      by auto
    thus ?thesis
      by (simp add: Setcompr_eq_image)
  qed
  ultimately show ?case
    by (simp add: Inf_lower Setcompr_eq_image order_antisym wellorder_InfI)
qed

lemma distance_set_neighbourhood:
  "⟦v ∈ neighbourhood G u; Vs ≠ {}⟧ ⟹ distance_set G Vs v ≤ distance_set G Vs u + 1"
proof(goal_cases)
  case assms: 1
  hence "(INF w∈ Vs. distance G w v) ≤ (INF w∈ Vs. distance G w u + 1)"
    by (auto simp add: distance_neighbourhood' intro!: INF_mono')
  also have "... = (INF w∈ Vs. distance G w u) + (1::enat)"
    using ‹Vs ≠ {}› 
    by (auto simp: INF_plus_enat)
  finally show ?case
    by(simp only: distance_set_def)
qed

lemma distance_set_parent: 
  "⟦distance_set G Vs v < ∞; Vs ≠ {}; v ∉ Vs⟧ ⟹ 
     ∃w. distance_set G Vs w + 1 = distance_set G Vs v ∧ v ∈ neighbourhood G w"
proof(goal_cases)
  case 1
  moreover hence "distance_set G Vs v ≠ ∞"
    by auto
  ultimately obtain u where ‹u ∈ Vs› ‹distance_set G Vs v = distance G u v › ‹u ≠ v›
    by(fastforce elim!: distance_set_wit')
  then obtain w where "distance G u w + 1 = distance G u v" "v ∈ neighbourhood G w"
    using 1 distance_parent
    by fastforce
  thus ?thesis
    by (metis "1"(2) ‹distance_set G Vs v = distance G u v› ‹u ∈ Vs› 
              add_mono_thms_linordered_semiring(3) dist_set_mem
              distance_set_neighbourhood nle_le)
qed

lemma distance_set_parent':
  "⟦0 < distance_set G Vs v; distance_set G Vs v < ∞; Vs ≠ {}⟧ ⟹ 
     ∃w. distance_set G Vs w + 1 = distance_set G Vs v ∧ v ∈ neighbourhood G w"
  using distance_set_parent
  by (metis antisym_conv2 dist_set_inf distance_0 distance_set_def less_INF_D order.strict_implies_order)

lemma distance_set_0[simp]: "⟦v ∈ dVs G⟧ ⟹ distance_set G Vs v = 0 ⟷ v ∈ Vs"
proof(safe, goal_cases)
  case 2
  moreover have "distance G v v = 0"
    by (meson calculation(1) distance_0)
  ultimately show ?case
    by (metis dist_set_mem le_zero_eq)
next
  case 1
  thus ?case
    by (metis dist_set_not_inf distance_0 infinity_ne_i0)
qed

lemma dist_set_leq: 
  "⟦⋀u. u ∈ Vs ⟹ distance G u v ≤ distance G' u v⟧ ⟹ distance_set G Vs v ≤ distance_set G' Vs v"
  by(auto simp: distance_set_def INF_superset_mono)             

lemma dist_set_eq: 
  "⟦⋀u. u ∈ Vs ⟹ distance G u v = distance G' u v⟧ ⟹ distance_set G Vs v = distance_set G' Vs v"
  using dist_set_leq
  by (metis nle_le)

lemma distance_set_subset: "G ⊆ G' ⟹ distance_set G' Vs v ≤ distance_set G Vs v"
  by (simp add: dist_set_leq distance_subset)

lemma vwalk_bet_dist_set:
  "⟦Vwalk.vwalk_bet G u p v; u ∈ U⟧ ⟹ distance_set G U v ≤ length p - 1"
  apply (auto simp: distance_set_def image_def intro!:)
  by (metis (mono_tags, lifting) Inf_lower One_nat_def dual_order.trans mem_Collect_eq vwalk_bet_dist)
(*
section ‹Forests›

definition "forest G ≡ (∀u v p p'. Vwalk.vwalk_bet G u p v ∧ Vwalk.vwalk_bet G u p' v ⟶ p = p')"

lemma forest_props[elim]:
"forest G ⟹ (⟦ ⋀u v p p'. ⟦Vwalk.vwalk_bet G u p v; Vwalk.vwalk_bet G u p' v⟧ ⟹ p = p'⟧ ⟹ P) ⟹ P"
  by (auto simp: forest_def)

lemma forest_intro:
"⟦ ⋀u v p p'. ⟦Vwalk.vwalk_bet G u p v; Vwalk.vwalk_bet G u p' v⟧ ⟹ p = p'⟧ ⟹ forest G"
  by (auto simp: forest_def)

lemma forest_subset: "⟦forest G'; G ⊆ G'⟧ ⟹ forest G"
  by(auto simp: forest_def intro!: vwalk_bet_subset)

lemma distance_forest: "⟦reachable G u v; G ⊆ G'; forest G'⟧ ⟹ distance G u v = distance G' u v"
proof(goal_cases)
  case 1
  have "distance G' u v ≤ distance G u v"
    using ‹G ⊆ G'›
    by(auto simp: distance_subset)
  moreover  have "distance G u v ≤ distance G' u v"
    using 1 
    apply(auto simp: elim!: forest_props intro!: dist_eq[where f = id])
    by (metis reachable_dist_2 vwalk_bet_subset)
  ultimately show ?thesis
    by auto
qed

lemma forest_shortest_path:
  "⟦forest G; Vwalk.vwalk_bet G u p v⟧ ⟹ shortest_path G u p v"
  apply(auto elim!: forest_props intro!: shortest_path_intro)
  by (metis One_nat_def reachable_dist_2 reachable_vwalk_bet_iff)

lemma forest_insert: "⟦forest G; v ∉ dVs G⟧ ⟹ forest (insert (u,v) G)"
proof(intro forest_intro, goal_cases)
  case (1 u v p p')
  then show ?case sorry
qed

lemma forest_union: "⟦forest G⟧ ⟹ forest (G ∪ {(u,v). u ∈ dVs G ∧ v ∉ dVs G})"
  using forest_subset forest_insert
  apply auto
  sorry

section ‹Rooted Forest›



lemma distance_set_forest:
  "⟦u ∈ Vs; reachable G u v; G ⊆ G'; forest G'⟧ ⟹ distance_set G Vs v = distance_set G' Vs v"
proof(goal_cases)
  case 1
  then obtain p where "Vwalk.vwalk_bet G u p v"
    by (meson reachable_vwalk_bet_iff)
  hence "shortest_path G u p v"
    using ‹forest G'›  ‹G ⊆ G'› 
    by(auto dest: forest_subset intro!: forest_shortest_path)
  then show ?case
    by (metis (no_types, lifting) "1"(1) "1"(2) "1"(3) ‹vwalk_bet G u p v› distance_set_0 distance_set_shortest_path reachable_in_dVs(1) vwalk_bet_endpoints(2) vwalk_bet_subset)
qed*)
  
end