Theory Prim

(* Title:      Prim's Minimum Spanning Tree Algorithm
   Author:     Walter Guttmann
   Maintainer: Walter Guttmann <walter.guttmann at canterbury.ac.nz>
*)

section ‹Prim's Minimum Spanning Tree Algorithm›

text ‹
In this theory we prove total correctness of Prim's minimum spanning tree algorithm.
The proof has the same overall structure as the total-correctness proof of Kruskal's algorithm \<^cite>‹"Guttmann2018c"›.
The partial-correctness proof of Prim's algorithm is discussed in \<^cite>‹"Guttmann2016c" and "Guttmann2018b"›.
›

theory Prim

imports "HOL-Hoare.Hoare_Logic" Aggregation_Algebras.Aggregation_Algebras

begin

context m_kleene_algebra
begin

abbreviation "component g r ≡ r⇧T * (--g)⇧⋆"
definition "spanning_tree t g r ≡ forest t ∧ t ≤ (component g r)⇧T * (component g r) ⊓ --g ∧ component g r ≤ r⇧T * t⇧⋆ ∧ regular t"
definition "minimum_spanning_tree t g r ≡ spanning_tree t g r ∧ (∀u . spanning_tree u g r ⟶ sum (t ⊓ g) ≤ sum (u ⊓ g))"
definition "prim_precondition g r ≡ g = g⇧T ∧ injective r ∧ vector r ∧ regular r"
definition "prim_spanning_invariant t v g r ≡ prim_precondition g r ∧ v⇧T = r⇧T * t⇧⋆ ∧ spanning_tree t (v * v⇧T ⊓ g) r"
definition "prim_invariant t v g r ≡ prim_spanning_invariant t v g r ∧ (∃w . minimum_spanning_tree w g r ∧ t ≤ w)"

lemma span_tree_split:
  assumes "vector r"
    shows "t ≤ (component g r)⇧T * (component g r) ⊓ --g ⟷ (t ≤ (component g r)⇧T ∧ t ≤ component g r ∧ t ≤ --g)"
proof -
  have "(component g r)⇧T * (component g r) = (component g r)⇧T ⊓ component g r"
    by (metis assms conv_involutive covector_mult_closed vector_conv_covector vector_covector)
  thus ?thesis
    by simp
qed

lemma span_tree_component:
  assumes "spanning_tree t g r"
    shows "component g r = component t r"
  using assms by (simp add: order.antisym mult_right_isotone star_isotone spanning_tree_def)

text ‹
We first show three verification conditions which are used in both correctness proofs.
›

lemma prim_vc_1:
  assumes "prim_precondition g r"
    shows "prim_spanning_invariant bot r g r"
proof (unfold prim_spanning_invariant_def, intro conjI)
  show "prim_precondition g r"
    using assms by simp
next
  show "r⇧T = r⇧T * bot⇧⋆"
    by (simp add: star_absorb)
next
  let ?ss = "r * r⇧T ⊓ g"
  show "spanning_tree bot ?ss r"
  proof (unfold spanning_tree_def, intro conjI)
    show "injective bot"
      by simp
  next
    show "acyclic bot"
      by simp
  next
    show "bot ≤ (component ?ss r)⇧T * (component ?ss r) ⊓ --?ss"
      by simp
  next
    have "component ?ss r ≤ component (r * r⇧T) r"
      by (simp add: mult_right_isotone star_isotone)
    also have "... ≤ r⇧T * 1⇧⋆"
      using assms by (metis order.eq_iff p_antitone regular_one_closed star_sub_one prim_precondition_def)
    also have "... = r⇧T * bot⇧⋆"
      by (simp add: star.circ_zero star_one)
    finally show "component ?ss r ≤ r⇧T * bot⇧⋆"
      .
  next
    show "regular bot"
      by simp
  qed
qed

lemma prim_vc_2:
  assumes "prim_spanning_invariant t v g r"
      and "v * -v⇧T ⊓ g ≠ bot"
    shows "prim_spanning_invariant (t ⊔ minarc (v * -v⇧T ⊓ g)) (v ⊔ minarc (v * -v⇧T ⊓ g)⇧T * top) g r ∧ card { x . regular x ∧ x ≤ component g r ∧ x ≤ -(v ⊔ minarc (v * -v⇧T ⊓ g)⇧T * top)⇧T } < card { x . regular x ∧ x ≤ component g r ∧ x ≤ -v⇧T }"
proof -
  let ?vcv = "v * -v⇧T ⊓ g"
  let ?e = "minarc ?vcv"
  let ?t = "t ⊔ ?e"
  let ?v = "v ⊔ ?e⇧T * top"
  let ?c = "component g r"
  let ?g = "--g"
  let ?n1 = "card { x . regular x ∧ x ≤ ?c ∧ x ≤ -v⇧T }"
  let ?n2 = "card { x . regular x ∧ x ≤ ?c ∧ x ≤ -?v⇧T }"
  have 1: "regular v ∧ regular (v * v⇧T) ∧ regular (?v * ?v⇧T) ∧ regular (top * ?e)"
    using assms(1) by (metis prim_spanning_invariant_def spanning_tree_def prim_precondition_def regular_conv_closed regular_closed_star regular_mult_closed conv_involutive regular_closed_top regular_closed_sup minarc_regular)
  hence 2: "t ≤ v * v⇧T ⊓ ?g"
    using assms(1) by (metis prim_spanning_invariant_def spanning_tree_def inf_pp_commute inf.boundedE)
  hence 3: "t ≤ v * v⇧T"
    by simp
  have 4: "t ≤ ?g"
    using 2 by simp
  have 5: "?e ≤ v * -v⇧T ⊓ ?g"
    using 1 by (metis minarc_below pp_dist_inf regular_mult_closed regular_closed_p)
  hence 6: "?e ≤ v * -v⇧T"
    by simp
  have 7: "vector v"
    using assms(1) prim_spanning_invariant_def prim_precondition_def by (simp add: covector_mult_closed vector_conv_covector)
  hence 8: "?e ≤ v"
    using 6 by (metis conv_complement inf.boundedE vector_complement_closed vector_covector)
  have 9: "?e * t = bot"
    using 3 6 7 et(1) by blast
  have 10: "?e * t⇧T = bot"
    using 3 6 7 et(2) by simp
  have 11: "arc ?e"
    using assms(2) minarc_arc by simp
  have "r⇧T ≤ r⇧T * t⇧⋆"
    by (metis mult_right_isotone order_refl semiring.mult_not_zero star.circ_separate_mult_1 star_absorb)
  hence 12: "r⇧T ≤ v⇧T"
    using assms(1) by (simp add: prim_spanning_invariant_def)
  have 13: "vector r ∧ injective r ∧ v⇧T = r⇧T * t⇧⋆"
    using assms(1) prim_spanning_invariant_def prim_precondition_def minimum_spanning_tree_def spanning_tree_def reachable_restrict by simp
  have "g = g⇧T"
    using assms(1) prim_invariant_def prim_spanning_invariant_def prim_precondition_def by simp
  hence 14: "?g⇧T = ?g"
    using conv_complement by simp
  show "prim_spanning_invariant ?t ?v g r ∧ ?n2 < ?n1"
  proof (rule conjI)
    show "prim_spanning_invariant ?t ?v g r"
    proof (unfold prim_spanning_invariant_def, intro conjI)
      show "prim_precondition g r"
        using assms(1) prim_spanning_invariant_def by simp
    next
      show "?v⇧T = r⇧T * ?t⇧⋆"
        using assms(1) 6 7 9 by (simp add: reachable_inv prim_spanning_invariant_def prim_precondition_def spanning_tree_def)
    next
      let ?G = "?v * ?v⇧T ⊓ g"
      show "spanning_tree ?t ?G r"
      proof (unfold spanning_tree_def, intro conjI)
        show "injective ?t"
          using assms(1) 10 11 by (simp add: injective_inv prim_spanning_invariant_def spanning_tree_def)
      next
        show "acyclic ?t"
          using assms(1) 3 6 7 acyclic_inv prim_spanning_invariant_def spanning_tree_def by simp
      next
        show "?t ≤ (component ?G r)⇧T * (component ?G r) ⊓ --?G"
          using 1 2 5 7 13 prim_subgraph_inv inf_pp_commute mst_subgraph_inv_2 by auto
      next
        show "component (?v * ?v⇧T ⊓ g) r ≤ r⇧T * ?t⇧⋆"
        proof -
          have 15: "r⇧T * (v * v⇧T ⊓ ?g)⇧⋆ ≤ r⇧T * t⇧⋆"
            using assms(1) 1 by (metis prim_spanning_invariant_def spanning_tree_def inf_pp_commute)
          have "component (?v * ?v⇧T ⊓ g) r = r⇧T * (?v * ?v⇧T ⊓ ?g)⇧⋆"
            using 1 by simp
          also have "... ≤ r⇧T * ?t⇧⋆"
            using 2 6 7 11 12 13 14 15 by (metis span_inv)
          finally show ?thesis
            .
        qed
      next
        show "regular ?t"
          using assms(1) by (metis prim_spanning_invariant_def spanning_tree_def regular_closed_sup minarc_regular)
      qed
    qed
  next
    have 16: "top * ?e ≤ ?c"
    proof -
      have "top * ?e = top * ?e⇧T * ?e"
        using 11 by (metis arc_top_edge mult_assoc)
      also have "... ≤ v⇧T * ?e"
        using 7 8 by (metis conv_dist_comp conv_isotone mult_left_isotone symmetric_top_closed)
      also have "... ≤ v⇧T * ?g"
        using 5 mult_right_isotone by auto
      also have "... = r⇧T * t⇧⋆ * ?g"
        using 13 by simp
      also have "... ≤ r⇧T * ?g⇧⋆ * ?g"
        using 4 by (simp add: mult_left_isotone mult_right_isotone star_isotone)
      also have "... ≤ ?c"
        by (simp add: comp_associative mult_right_isotone star.right_plus_below_circ)
      finally show ?thesis
        by simp
    qed
    have 17: "top * ?e ≤ -v⇧T"
      using 6 7 by (simp add: schroeder_4_p vTeT)
    have 18: "¬ top * ?e ≤ -(top * ?e)"
      by (metis assms(2) inf.orderE minarc_bot_iff conv_complement_sub_inf inf_p inf_top.left_neutral p_bot symmetric_top_closed vector_top_closed)
    have 19: "-?v⇧T = -v⇧T ⊓ -(top * ?e)"
      by (simp add: conv_dist_comp conv_dist_sup)
    hence 20: "¬ top * ?e ≤ -?v⇧T"
      using 18 by simp
    show "?n2 < ?n1"
      apply (rule psubset_card_mono)
      using finite_regular apply simp
      using 1 16 17 19 20 by auto
  qed
qed

lemma prim_vc_3:
  assumes "prim_spanning_invariant t v g r"
      and "v * -v⇧T ⊓ g = bot"
    shows "spanning_tree t g r"
proof -
  let ?g = "--g"
  have 1: "regular v ∧ regular (v * v⇧T)"
    using assms(1) by (metis prim_spanning_invariant_def spanning_tree_def prim_precondition_def regular_conv_closed regular_closed_star regular_mult_closed conv_involutive)
  have 2: "v * -v⇧T ⊓ ?g = bot"
    using assms(2) pp_inf_bot_iff pp_pp_inf_bot_iff by simp
  have 3: "v⇧T = r⇧T * t⇧⋆ ∧ vector v"
    using assms(1) by (simp add: covector_mult_closed prim_invariant_def prim_spanning_invariant_def vector_conv_covector prim_precondition_def)
  have 4: "t ≤ v * v⇧T ⊓ ?g"
    using assms(1) 1 by (metis prim_spanning_invariant_def inf_pp_commute spanning_tree_def inf.boundedE)
  have "r⇧T * (v * v⇧T ⊓ ?g)⇧⋆ ≤ r⇧T * t⇧⋆"
    using assms(1) 1 by (metis prim_spanning_invariant_def inf_pp_commute spanning_tree_def)
  hence 5: "component g r = v⇧T"
    using 1 2 3 4 by (metis span_post)
  have "regular (v * v⇧T)"
    using assms(1) by (metis prim_spanning_invariant_def spanning_tree_def prim_precondition_def regular_conv_closed regular_closed_star regular_mult_closed conv_involutive)
  hence 6: "t ≤ v * v⇧T ⊓ ?g"
    by (metis assms(1) prim_spanning_invariant_def spanning_tree_def inf_pp_commute inf.boundedE)
  show "spanning_tree t g r"
    apply (unfold spanning_tree_def, intro conjI)
    using assms(1) prim_spanning_invariant_def spanning_tree_def apply simp
    using assms(1) prim_spanning_invariant_def spanning_tree_def apply simp
    using 5 6 apply simp
    using assms(1) 5 prim_spanning_invariant_def apply simp
    using assms(1) prim_spanning_invariant_def spanning_tree_def by simp
qed

text ‹
The following result shows that Prim's algorithm terminates and constructs a spanning tree.
We cannot yet show that this is a minimum spanning tree.
›

theorem prim_spanning:
  "VARS t v e
  [ prim_precondition g r ]
  t := bot;
  v := r;
  WHILE v * -v⇧T ⊓ g ≠ bot
    INV { prim_spanning_invariant t v g r }
    VAR { card { x . regular x ∧ x ≤ component g r ⊓ -v⇧T } }
     DO e := minarc (v * -v⇧T ⊓ g);
        t := t ⊔ e;
        v := v ⊔ e⇧T * top
     OD
  [ spanning_tree t g r ]"
  apply vcg_tc_simp
  apply (simp add: prim_vc_1)
  using prim_vc_2 apply blast
  using prim_vc_3 by auto

text ‹
Because we have shown total correctness, we conclude that a spanning tree exists.
›

lemma prim_exists_spanning:
  "prim_precondition g r ⟹ ∃t . spanning_tree t g r"
  using tc_extract_function prim_spanning by blast

text ‹
This implies that a minimum spanning tree exists, which is used in the subsequent correctness proof.
›

lemma prim_exists_minimal_spanning:
  assumes "prim_precondition g r"
    shows "∃t . minimum_spanning_tree t g r"
proof -
  let ?s = "{ t . spanning_tree t g r }"
  have "∃m∈?s . ∀z∈?s . sum (m ⊓ g) ≤ sum (z ⊓ g)"
    apply (rule finite_set_minimal)
    using finite_regular spanning_tree_def apply simp
    using assms prim_exists_spanning apply simp
    using sum_linear by simp
  thus ?thesis
    using minimum_spanning_tree_def by simp
qed

text ‹
Prim's minimum spanning tree algorithm terminates and is correct.
This is the same algorithm that is used in the previous correctness proof, with the same precondition and variant, but with a different invariant and postcondition.
›

theorem prim:
  "VARS t v e
  [ prim_precondition g r ∧ (∃w . minimum_spanning_tree w g r) ]
  t := bot;
  v := r;
  WHILE v * -v⇧T ⊓ g ≠ bot
    INV { prim_invariant t v g r }
    VAR { card { x . regular x ∧ x ≤ component g r ⊓ -v⇧T } }
     DO e := minarc (v * -v⇧T ⊓ g);
        t := t ⊔ e;
        v := v ⊔ e⇧T * top
     OD
  [ minimum_spanning_tree t g r ]"
proof vcg_tc_simp
  assume "prim_precondition g r ∧ (∃w . minimum_spanning_tree w g r)"
  thus "prim_invariant bot r g r"
    using prim_invariant_def prim_vc_1 by simp
next
  fix t v
  let ?vcv = "v * -v⇧T ⊓ g"
  let ?vv = "v * v⇧T ⊓ g"
  let ?e = "minarc ?vcv"
  let ?t = "t ⊔ ?e"
  let ?v = "v ⊔ ?e⇧T * top"
  let ?c = "component g r"
  let ?g = "--g"
  let ?n1 = "card { x . regular x ∧ x ≤ ?c ∧ x ≤ -v⇧T }"
  let ?n2 = "card { x . regular x ∧ x ≤ ?c ∧ x ≤ -?v⇧T }"
  assume 1: "prim_invariant t v g r ∧ ?vcv ≠ bot"
  hence 2: "regular v ∧ regular (v * v⇧T)"
    by (metis (no_types, opaque_lifting) prim_invariant_def prim_spanning_invariant_def spanning_tree_def prim_precondition_def regular_conv_closed regular_closed_star regular_mult_closed conv_involutive)
  have 3: "t ≤ v * v⇧T ⊓ ?g"
    using 1 2 by (metis (no_types, opaque_lifting) prim_invariant_def prim_spanning_invariant_def spanning_tree_def inf_pp_commute inf.boundedE)
  hence 4: "t ≤ v * v⇧T"
    by simp
  have 5: "t ≤ ?g"
    using 3 by simp
  have 6: "?e ≤ v * -v⇧T ⊓ ?g"
    using 2 by (metis minarc_below pp_dist_inf regular_mult_closed regular_closed_p)
  hence 7: "?e ≤ v * -v⇧T"
    by simp
  have 8: "vector v"
    using 1 prim_invariant_def prim_spanning_invariant_def prim_precondition_def by (simp add: covector_mult_closed vector_conv_covector)
  have 9: "arc ?e"
    using 1 minarc_arc by simp
  from 1 obtain w where 10: "minimum_spanning_tree w g r ∧ t ≤ w"
    by (metis prim_invariant_def)
  hence 11: "vector r ∧ injective r ∧ v⇧T = r⇧T * t⇧⋆ ∧ forest w ∧ t ≤ w ∧ w ≤ ?c⇧T * ?c ⊓ ?g ∧ r⇧T * (?c⇧T * ?c ⊓ ?g)⇧⋆ ≤ r⇧T * w⇧⋆"
    using 1 2 prim_invariant_def prim_spanning_invariant_def prim_precondition_def minimum_spanning_tree_def spanning_tree_def reachable_restrict by simp
  hence 12: "w * v ≤ v"
    using predecessors_reachable reachable_restrict by auto
  have 13: "g = g⇧T"
    using 1 prim_invariant_def prim_spanning_invariant_def prim_precondition_def by simp
  hence 14: "?g⇧T = ?g"
    using conv_complement by simp
  show "prim_invariant ?t ?v g r ∧ ?n2 < ?n1"
  proof (unfold prim_invariant_def, intro conjI)
    show "prim_spanning_invariant ?t ?v g r"
      using 1 prim_invariant_def prim_vc_2 by blast
  next
    show "∃w . minimum_spanning_tree w g r ∧ ?t ≤ w"
    proof
      let ?f = "w ⊓ v * -v⇧T ⊓ top * ?e * w⇧T⇧⋆"
      let ?p = "w ⊓ -v * -v⇧T ⊓ top * ?e * w⇧T⇧⋆"
      let ?fp = "w ⊓ -v⇧T ⊓ top * ?e * w⇧T⇧⋆"
      let ?w = "(w ⊓ -?fp) ⊔ ?p⇧T ⊔ ?e"
      have 15: "regular ?f ∧ regular ?fp ∧ regular ?w"
        using 2 10 by (metis regular_conv_closed regular_closed_star regular_mult_closed regular_closed_top regular_closed_inf regular_closed_sup minarc_regular minimum_spanning_tree_def spanning_tree_def)
      show "minimum_spanning_tree ?w g r ∧ ?t ≤ ?w"
      proof (intro conjI)
        show "minimum_spanning_tree ?w g r"
        proof (unfold minimum_spanning_tree_def, intro conjI)
          show "spanning_tree ?w g r"
          proof (unfold spanning_tree_def, intro conjI)
            show "injective ?w"
              using 7 8 9 11 exchange_injective by blast
          next
            show "acyclic ?w"
              using 7 8 11 12 exchange_acyclic by blast
          next
            show "?w ≤ ?c⇧T * ?c ⊓ --g"
            proof -
              have 16: "w ⊓ -?fp ≤ ?c⇧T * ?c ⊓ --g"
                using 10 by (simp add: le_infI1 minimum_spanning_tree_def spanning_tree_def)
              have "?p⇧T ≤ w⇧T"
                by (simp add: conv_isotone inf.sup_monoid.add_assoc)
              also have "... ≤ (?c⇧T * ?c ⊓ --g)⇧T"
                using 11 conv_order by simp
              also have "... = ?c⇧T * ?c ⊓ --g"
                using 2 14 conv_dist_comp conv_dist_inf by simp
              finally have 17: "?p⇧T ≤ ?c⇧T * ?c ⊓ --g"
                .
              have "?e ≤ ?c⇧T * ?c ⊓ ?g"
                using 5 6 11 mst_subgraph_inv by auto
              thus ?thesis
                using 16 17 by simp
            qed
          next
            show "?c ≤ r⇧T * ?w⇧⋆"
            proof -
              have "?c ≤ r⇧T * w⇧⋆"
                using 10 minimum_spanning_tree_def spanning_tree_def by simp
              also have "... ≤ r⇧T * ?w⇧⋆"
                using 4 7 8 10 11 12 15 by (metis mst_reachable_inv)
              finally show ?thesis
                .
            qed
          next
            show "regular ?w"
              using 15 by simp
          qed
        next
          have 18: "?f ⊔ ?p = ?fp"
            using 2 8 epm_1 by fastforce
          have "arc (w ⊓ --v * -v⇧T ⊓ top * ?e * w⇧T⇧⋆)"
            using 5 6 8 9 11 12 reachable_restrict arc_edge by auto
          hence 19: "arc ?f"
            using 2 by simp
          hence "?f = bot ⟶ top = bot"
            by (metis mult_left_zero mult_right_zero)
          hence "?f ≠ bot"
            using 1 le_bot by auto
          hence "?f ⊓ v * -v⇧T ⊓ ?g ≠ bot"
            using 2 11 by (simp add: inf.absorb1 le_infI1)
          hence "g ⊓ (?f ⊓ v * -v⇧T) ≠ bot"
            using inf_commute pp_inf_bot_iff by simp
          hence 20: "?f ⊓ ?vcv ≠ bot"
            by (simp add: inf_assoc inf_commute)
          hence 21: "?f ⊓ g = ?f ⊓ ?vcv"
            using 2 by (simp add: inf_assoc inf_commute inf_left_commute)
          have 22: "?e ⊓ g = minarc ?vcv ⊓ ?vcv"
            using 7 by (simp add: inf.absorb2 inf.assoc inf.commute)
          hence 23: "sum (?e ⊓ g) ≤ sum (?f ⊓ g)"
            using 15 19 20 21 by (simp add: minarc_min)
          have "?e ≠ bot"
            using 20 comp_inf.semiring.mult_not_zero semiring.mult_not_zero by blast
          hence 24: "?e ⊓ g ≠ bot"
            using 22 minarc_meet_bot by auto
          have "sum (?w ⊓ g) = sum (w ⊓ -?fp ⊓ g) + sum (?p⇧T ⊓ g) + sum (?e ⊓ g)"
            using 7 8 10 by (metis sum_disjoint_3 epm_8 epm_9 epm_10 minimum_spanning_tree_def spanning_tree_def)
          also have "... = sum (((w ⊓ -?fp) ⊔ ?p⇧T) ⊓ g) + sum (?e ⊓ g)"
            using 11 by (metis epm_8 sum_disjoint)
          also have "... ≤ sum (((w ⊓ -?fp) ⊔ ?p⇧T) ⊓ g) + sum (?f ⊓ g)"
            using 23 24 by (simp add: sum_plus_right_isotone)
          also have "... = sum (w ⊓ -?fp ⊓ g) + sum (?p⇧T ⊓ g) + sum (?f ⊓ g)"
            using 11 by (metis epm_8 sum_disjoint)
          also have "... = sum (w ⊓ -?fp ⊓ g) + sum (?p ⊓ g) + sum (?f ⊓ g)"
            using 13 sum_symmetric by auto
          also have "... = sum (((w ⊓ -?fp) ⊔ ?p ⊔ ?f) ⊓ g)"
            using 2 8 by (metis sum_disjoint_3 epm_11 epm_12 epm_13)
          also have "... = sum (w ⊓ g)"
            using 2 8 15 18 epm_2 by force
          finally have "sum (?w ⊓ g) ≤ sum (w ⊓ g)"
            .
          thus "∀u . spanning_tree u g r ⟶ sum (?w ⊓ g) ≤ sum (u ⊓ g)"
            using 10 order_lesseq_imp minimum_spanning_tree_def by auto
        qed
      next
        show "?t ≤ ?w"
          using 4 8 10 mst_extends_new_tree by simp
      qed
    qed
  next
    show "?n2 < ?n1"
      using 1 prim_invariant_def prim_vc_2 by auto
  qed
next
  fix t v
  let ?g = "--g"
  assume 25: "prim_invariant t v g r ∧ v * -v⇧T ⊓ g = bot"
  hence 26: "regular v"
    by (metis prim_invariant_def prim_spanning_invariant_def spanning_tree_def prim_precondition_def regular_conv_closed regular_closed_star regular_mult_closed conv_involutive)
  from 25 obtain w where 27: "minimum_spanning_tree w g r ∧ t ≤ w"
    by (metis prim_invariant_def)
  have "spanning_tree t g r"
    using 25 prim_invariant_def prim_vc_3 by blast
  hence "component g r = v⇧T"
    by (metis 25 prim_invariant_def span_tree_component prim_spanning_invariant_def spanning_tree_def)
  hence 28: "w ≤ v * v⇧T"
    using 26 27 by (simp add: minimum_spanning_tree_def spanning_tree_def inf_pp_commute)
  have "vector r ∧ injective r ∧ forest w"
    using 25 27 by (simp add: prim_invariant_def prim_spanning_invariant_def prim_precondition_def minimum_spanning_tree_def spanning_tree_def)
  hence "w = t"
    using 25 27 28 prim_invariant_def prim_spanning_invariant_def mst_post by blast
  thus "minimum_spanning_tree t g r"
    using 27 by simp
qed

end

end