Session Relational_Minimum_Spanning_Trees

Theory Kruskal

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

section ‹Kruskal's Minimum Spanning Tree Algorithm›

text ‹
In this theory we prove total correctness of Kruskal's minimum spanning tree algorithm.
The proof uses the following steps \cite{Guttmann2018c}.
We first establish that the algorithm terminates and constructs a spanning tree.
This is a constructive proof of the existence of a spanning tree; any spanning tree algorithm could be used for this.
We then conclude that a minimum spanning tree exists.
This is necessary to establish the invariant for the actual correctness proof, which shows that Kruskal's algorithm produces a minimum spanning tree.
›

theory Kruskal

imports "HOL-Hoare.Hoare_Logic" Aggregation_Algebras.Aggregation_Algebras

begin

context m_kleene_algebra
begin

definition "spanning_forest f g  forest f  f  --g  components g  forest_components f  regular f"
definition "minimum_spanning_forest f g  spanning_forest f g  (u . spanning_forest u g  sum (f  g)  sum (u  g))"
definition "kruskal_spanning_invariant f g h  symmetric g  h = hT  g  --h = h  spanning_forest f (-h  g)"
definition "kruskal_invariant f g h  kruskal_spanning_invariant f g h  (w . minimum_spanning_forest w g  f  w  wT)"

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

lemma kruskal_vc_1:
  assumes "symmetric g"
    shows "kruskal_spanning_invariant bot g g"
proof (unfold kruskal_spanning_invariant_def, intro conjI)
  show "symmetric g"
    using assms by simp
next
  show "g = gT"
    using assms by simp
next
  show "g  --g = g"
    using inf.sup_monoid.add_commute selection_closed_id by simp
next
  show "spanning_forest bot (-g  g)"
    using star.circ_transitive_equal spanning_forest_def by simp
qed

lemma kruskal_vc_2:
  assumes "kruskal_spanning_invariant f g h"
      and "h  bot"
    shows "(minarc h  -forest_components f  kruskal_spanning_invariant ((f  -(top * minarc h * fT))  (f  top * minarc h * fT)T  minarc h) g (h  -minarc h  -minarc hT)
                                                card { x . regular x  x  --h  x  -minarc h  x  -minarc hT } < card { x . regular x  x  --h }) 
           (¬ minarc h  -forest_components f  kruskal_spanning_invariant f g (h  -minarc h  -minarc hT)
                                                  card { x . regular x  x  --h  x  -minarc h  x  -minarc hT } < card { x . regular x  x  --h })"
proof -
  let ?e = "minarc h"
  let ?f = "(f  -(top * ?e * fT))  (f  top * ?e * fT)T  ?e"
  let ?h = "h  -?e  -?eT"
  let ?F = "forest_components f"
  let ?n1 = "card { x . regular x  x  --h }"
  let ?n2 = "card { x . regular x  x  --h  x  -?e  x  -?eT }"
  have 1: "regular f  regular ?e"
    by (metis assms(1) kruskal_spanning_invariant_def spanning_forest_def minarc_regular)
  hence 2: "regular ?f  regular ?F  regular (?eT)"
    using regular_closed_star regular_conv_closed regular_mult_closed by simp
  have 3: "¬ ?e  -?e"
    using assms(2) inf.orderE minarc_bot_iff by fastforce
  have 4: "?n2 < ?n1"
    apply (rule psubset_card_mono)
    using finite_regular apply simp
    using 1 3 kruskal_spanning_invariant_def minarc_below by auto
  show "(?e  -?F  kruskal_spanning_invariant ?f g ?h  ?n2 < ?n1)  (¬ ?e  -?F  kruskal_spanning_invariant f g ?h  ?n2 < ?n1)"
  proof (rule conjI)
    have 5: "injective ?f"
      apply (rule kruskal_injective_inv)
      using assms(1) kruskal_spanning_invariant_def spanning_forest_def apply simp
      apply (simp add: covector_mult_closed)
      apply (simp add: comp_associative comp_isotone star.right_plus_below_circ)
      apply (meson mult_left_isotone order_lesseq_imp star_outer_increasing top.extremum)
      using assms(1,2) kruskal_spanning_invariant_def kruskal_injective_inv_2 minarc_arc spanning_forest_def apply simp
      using assms(2) arc_injective minarc_arc apply blast
      using assms(1,2) kruskal_spanning_invariant_def kruskal_injective_inv_3 minarc_arc spanning_forest_def by simp
    show "?e  -?F  kruskal_spanning_invariant ?f g ?h  ?n2 < ?n1"
    proof
      assume 6: "?e  -?F"
      have 7: "equivalence ?F"
        using assms(1) kruskal_spanning_invariant_def forest_components_equivalence spanning_forest_def by simp
      have "?eT * top * ?eT = ?eT"
        using assms(2) by (simp add: arc_top_arc minarc_arc)
      hence "?eT * top * ?eT  -?F"
        using 6 7 conv_complement conv_isotone by fastforce
      hence 8: "?e * ?F * ?e = bot"
        using le_bot triple_schroeder_p by simp
      show "kruskal_spanning_invariant ?f g ?h  ?n2 < ?n1"
      proof (unfold kruskal_spanning_invariant_def, intro conjI)
        show "symmetric g"
          using assms(1) kruskal_spanning_invariant_def by simp
      next
        show "?h = ?hT"
          using assms(1) by (simp add: conv_complement conv_dist_inf inf_commute inf_left_commute kruskal_spanning_invariant_def)
      next
        show "g  --?h = ?h"
          using 1 2 by (metis (hide_lams) assms(1) kruskal_spanning_invariant_def inf_assoc pp_dist_inf)
      next
        show "spanning_forest ?f (-?h  g)"
        proof (unfold spanning_forest_def, intro conjI)
          show "injective ?f"
            using 5 by simp
        next
          show "acyclic ?f"
            apply (rule kruskal_acyclic_inv)
            using assms(1) kruskal_spanning_invariant_def spanning_forest_def apply simp
            apply (simp add: covector_mult_closed)
            using 8 assms(1) kruskal_spanning_invariant_def spanning_forest_def kruskal_acyclic_inv_1 apply simp
            using 8 apply (metis comp_associative mult_left_sub_dist_sup_left star.circ_loop_fixpoint sup_commute le_bot)
            using 6 by (simp add: p_antitone_iff)
        next
          show "?f  --(-?h  g)"
            apply (rule kruskal_subgraph_inv)
            using assms(1) kruskal_spanning_invariant_def spanning_forest_def apply simp
            using assms(1) apply (metis kruskal_spanning_invariant_def minarc_below order.trans pp_isotone_inf)
            using assms(1) kruskal_spanning_invariant_def apply simp
            using assms(1) kruskal_spanning_invariant_def by simp
        next
          show "components (-?h  g)  forest_components ?f"
            apply (rule kruskal_spanning_inv)
            using 5 apply simp
            using 1 regular_closed_star regular_conv_closed regular_mult_closed apply simp
            using 1 apply simp
            using assms(1) kruskal_spanning_invariant_def spanning_forest_def by simp
        next
          show "regular ?f"
            using 2 by simp
        qed
      next
        show "?n2 < ?n1"
          using 4 by simp
      qed
    qed
  next
    show "¬ ?e  -?F  kruskal_spanning_invariant f g ?h  ?n2 < ?n1"
    proof
      assume "¬ ?e  -?F"
      hence 9: "?e  ?F"
        using 2 assms(2) arc_in_partition minarc_arc by fastforce
      show "kruskal_spanning_invariant f g ?h  ?n2 < ?n1"
      proof (unfold kruskal_spanning_invariant_def, intro conjI)
        show "symmetric g"
          using assms(1) kruskal_spanning_invariant_def by simp
      next
        show "?h = ?hT"
          using assms(1) by (simp add: conv_complement conv_dist_inf inf_commute inf_left_commute kruskal_spanning_invariant_def)
      next
        show "g  --?h = ?h"
          using 1 2 by (metis (hide_lams) assms(1) kruskal_spanning_invariant_def inf_assoc pp_dist_inf)
      next
        show "spanning_forest f (-?h  g)"
        proof (unfold spanning_forest_def, intro conjI)
          show "injective f"
            using assms(1) kruskal_spanning_invariant_def spanning_forest_def by simp
        next
          show "acyclic f"
            using assms(1) kruskal_spanning_invariant_def spanning_forest_def by simp
        next
          have "f  --(-h  g)"
            using assms(1) kruskal_spanning_invariant_def spanning_forest_def by simp
          also have "...  --(-?h  g)"
            using comp_inf.mult_right_isotone inf.sup_monoid.add_commute inf_left_commute p_antitone_inf pp_isotone by presburger
          finally show "f  --(-?h  g)"
            by simp
        next
          show "components (-?h  g)  ?F"
            apply (rule kruskal_spanning_inv_1)
            using 9 apply simp
            using 1 apply simp
            using assms(1) kruskal_spanning_invariant_def spanning_forest_def apply simp
            using assms(1) kruskal_spanning_invariant_def forest_components_equivalence spanning_forest_def by simp
        next
          show "regular f"
            using 1 by simp
        qed
      next
        show "?n2 < ?n1"
          using 4 by simp
      qed
    qed
  qed
qed

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

theorem kruskal_spanning:
  "VARS e f h
  [ symmetric g ]
  f := bot;
  h := g;
  WHILE h  bot
    INV { kruskal_spanning_invariant f g h }
    VAR { card { x . regular x  x  --h } }
     DO e := minarc h;
        IF e  -forest_components f THEN
          f := (f  -(top * e * fT))  (f  top * e * fT)T  e
        ELSE
          SKIP
        FI;
        h := h  -e  -eT
     OD
  [ spanning_forest f g ]"
  apply vcg_tc_simp
  using kruskal_vc_1 apply simp
  using kruskal_vc_2 apply simp
  using kruskal_spanning_invariant_def by auto

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

lemma kruskal_exists_spanning:
  "symmetric g  f . spanning_forest f g"
  using tc_extract_function kruskal_spanning by blast

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

lemma kruskal_exists_minimal_spanning:
  assumes "symmetric g"
    shows "f . minimum_spanning_forest f g"
proof -
  let ?s = "{ f . spanning_forest f g }"
  have "m?s . z?s . sum (m  g)  sum (z  g)"
    apply (rule finite_set_minimal)
    using finite_regular spanning_forest_def apply simp
    using assms kruskal_exists_spanning apply simp
    using sum_linear by simp
  thus ?thesis
    using minimum_spanning_forest_def by simp
qed

text ‹
Kruskal'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 kruskal:
  "VARS e f h
  [ symmetric g ]
  f := bot;
  h := g;
  WHILE h  bot
    INV { kruskal_invariant f g h }
    VAR { card { x . regular x  x  --h } }
     DO e := minarc h;
        IF e  -forest_components f THEN
          f := (f  -(top * e * fT))  (f  top * e * fT)T  e
        ELSE
          SKIP
        FI;
        h := h  -e  -eT
     OD
  [ minimum_spanning_forest f g ]"
proof vcg_tc_simp
  assume "symmetric g"
  thus "kruskal_invariant bot g g"
    using kruskal_vc_1 kruskal_exists_minimal_spanning kruskal_invariant_def by simp
next
  fix f h
  let ?e = "minarc h"
  let ?f = "(f  -(top * ?e * fT))  (f  top * ?e * fT)T  ?e"
  let ?h = "h  -?e  -?eT"
  let ?F = "forest_components f"
  let ?n1 = "card { x . regular x  x  --h }"
  let ?n2 = "card { x . regular x  x  --h  x  -?e  x  -?eT }"
  assume 1: "kruskal_invariant f g h  h  bot"
  from 1 obtain w where 2: "minimum_spanning_forest w g  f  w  wT"
    using kruskal_invariant_def by auto
  hence 3: "regular f  regular w  regular ?e"
    using 1 by (metis kruskal_invariant_def kruskal_spanning_invariant_def minimum_spanning_forest_def spanning_forest_def minarc_regular)
  show "(?e  -?F  kruskal_invariant ?f g ?h  ?n2 < ?n1)  (¬ ?e  -?F  kruskal_invariant f g ?h  ?n2 < ?n1)"
  proof (rule conjI)
    show "?e  -?F  kruskal_invariant ?f g ?h  ?n2 < ?n1"
    proof
      assume 4: "?e  -?F"
      have 5: "equivalence ?F"
        using 1 kruskal_invariant_def kruskal_spanning_invariant_def forest_components_equivalence spanning_forest_def by simp
      have "?eT * top * ?eT = ?eT"
        using 1 by (simp add: arc_top_arc minarc_arc)
      hence "?eT * top * ?eT  -?F"
        using 4 5 conv_complement conv_isotone by fastforce
      hence 6: "?e * ?F * ?e = bot"
        using le_bot triple_schroeder_p by simp
      show "kruskal_invariant ?f g ?h  ?n2 < ?n1"
      proof (unfold kruskal_invariant_def, intro conjI)
        show "kruskal_spanning_invariant ?f g ?h"
          using 1 4 kruskal_vc_2 kruskal_invariant_def by simp
      next
        show "w . minimum_spanning_forest w g  ?f  w  wT"
        proof
          let ?p = "w  top * ?e * wT"
          let ?v = "(w  -(top * ?e * wT))  ?pT"
          have 7: "regular ?p"
            using 3 regular_closed_star regular_conv_closed regular_mult_closed by simp
          have 8: "injective ?v"
            apply (rule kruskal_exchange_injective_inv_1)
            using 2 minimum_spanning_forest_def spanning_forest_def apply simp
            apply (simp add: covector_mult_closed)
            apply (simp add: comp_associative comp_isotone star.right_plus_below_circ)
            using 1 2 kruskal_injective_inv_3 minarc_arc minimum_spanning_forest_def spanning_forest_def by simp
          have 9: "components g  forest_components ?v"
            apply (rule kruskal_exchange_spanning_inv_1)
            using 8 apply simp
            using 7 apply simp
            using 2 minimum_spanning_forest_def spanning_forest_def by simp
          have 10: "spanning_forest ?v g"
          proof (unfold spanning_forest_def, intro conjI)
            show "injective ?v"
              using 8 by simp
          next
            show "acyclic ?v"
              apply (rule kruskal_exchange_acyclic_inv_1)
              using 2 minimum_spanning_forest_def spanning_forest_def apply simp
              by (simp add: covector_mult_closed)
          next
            show "?v  --g"
              apply (rule sup_least)
              using 2 inf.coboundedI1 minimum_spanning_forest_def spanning_forest_def apply simp
              using 1 2 by (metis kruskal_invariant_def kruskal_spanning_invariant_def conv_complement conv_dist_inf order.trans inf.absorb2 inf.cobounded1 minimum_spanning_forest_def spanning_forest_def)
          next
            show "components g  forest_components ?v"
              using 9 by simp
          next
            show "regular ?v"
              using 3 regular_closed_star regular_conv_closed regular_mult_closed by simp
          qed
          have 11: "sum (?v  g) = sum (w  g)"
          proof -
            have "sum (?v  g) = sum (w  -(top * ?e * wT)  g) + sum (?pT  g)"
              using 2 by (metis conv_complement conv_top epm_8 inf_import_p inf_top_right regular_closed_top vector_top_closed minimum_spanning_forest_def spanning_forest_def sum_disjoint)
            also have "... = sum (w  -(top * ?e * wT)  g) + sum (?p  g)"
              using 1 kruskal_invariant_def kruskal_spanning_invariant_def sum_symmetric by simp
            also have "... = sum (((w  -(top * ?e * wT))  ?p)  g)"
              using inf_commute inf_left_commute sum_disjoint by simp
            also have "... = sum (w  g)"
              using 3 7 maddux_3_11_pp by simp
            finally show ?thesis
              by simp
          qed
          have 12: "?v  ?vT = w  wT"
          proof -
            have "?v  ?vT = (w  -?p)  ?pT  (wT  -?pT)  ?p"
              using conv_complement conv_dist_inf conv_dist_sup inf_import_p sup_assoc by simp
            also have "... = w  wT"
              using 3 7 conv_complement conv_dist_inf inf_import_p maddux_3_11_pp sup_monoid.add_assoc sup_monoid.add_commute by simp
            finally show ?thesis
              by simp
          qed
          have 13: "?v * ?eT = bot"
            apply (rule kruskal_reroot_edge)
            using 1 apply (simp add: minarc_arc)
            using 2 minimum_spanning_forest_def spanning_forest_def by simp
          have "?v  ?e  ?v  top * ?e"
            using inf.sup_right_isotone top_left_mult_increasing by simp
          also have "...  ?v * (top * ?e)T"
            using covector_restrict_comp_conv covector_mult_closed vector_top_closed by simp
          finally have 14: "?v  ?e = bot"
            using 13 by (metis conv_dist_comp mult_assoc le_bot mult_left_zero)
          let ?d = "?v  top * ?eT * ?vT  ?F * ?eT * top  top * ?e * -?F"
          let ?w = "(?v  -?d)  ?e"
          have 15: "regular ?d"
            using 3 regular_closed_star regular_conv_closed regular_mult_closed by simp
          have 16: "?F  -?d"
            apply (rule kruskal_edge_between_components_1)
            using 5 apply simp
            using 1 conv_dist_comp minarc_arc mult_assoc by simp
          have 17: "f  fT  (?v  -?d  -?dT)  (?vT  -?d  -?dT)"
            apply (rule kruskal_edge_between_components_2)
            using 16 apply simp
            using 1 kruskal_invariant_def kruskal_spanning_invariant_def spanning_forest_def apply simp
            using 2 12 by (metis conv_dist_sup conv_involutive conv_isotone le_supI sup_commute)
          show "minimum_spanning_forest ?w g  ?f  ?w  ?wT"
          proof (intro conjI)
            have 18: "?eT  ?v"
              apply (rule kruskal_edge_arc_1[where g=g and h=h])
              using minarc_below apply simp
              using 1 apply (metis kruskal_invariant_def kruskal_spanning_invariant_def inf_le1)
              using 1 kruskal_invariant_def kruskal_spanning_invariant_def apply simp
              using 9 apply simp
              using 13 by simp
            have 19: "arc ?d"
              apply (rule kruskal_edge_arc)
              using 5 apply simp
              using 10 spanning_forest_def apply blast
              using 1 apply (simp add: minarc_arc)
              using 3 apply (metis conv_complement pp_dist_star regular_mult_closed)
              using 2 8 12 apply (simp add: kruskal_forest_components_inf)
              using 10 spanning_forest_def apply simp
              using 13 apply simp
              using 6 apply simp
              using 18 by simp
            show "minimum_spanning_forest ?w g"
            proof (unfold minimum_spanning_forest_def, intro conjI)
              have "(?v  -?d) * ?eT  ?v * ?eT"
                using inf_le1 mult_left_isotone by simp
              hence "(?v  -?d) * ?eT = bot"
                using 13 le_bot by simp
              hence 20: "?e * (?v  -?d)T = bot"
                using conv_dist_comp conv_involutive conv_bot by force
              have 21: "injective ?w"
                apply (rule injective_sup)
                using 8 apply (simp add: injective_inf_closed)
                using 20 apply simp
                using 1 arc_injective minarc_arc by blast
              show "spanning_forest ?w g"
              proof (unfold spanning_forest_def, intro conjI)
                show "injective ?w"
                  using 21 by simp
              next
                show "acyclic ?w"
                  apply (rule kruskal_exchange_acyclic_inv_2)
                  using 10 spanning_forest_def apply blast
                  using 8 apply simp
                  using inf.coboundedI1 apply simp
                  using 19 apply simp
                  using 1 apply (simp add: minarc_arc)
                  using inf.cobounded2 inf.coboundedI1 apply simp
                  using 13 by simp
              next
                have "?w  ?v  ?e"
                  using inf_le1 sup_left_isotone by simp
                also have "...  --g  ?e"
                  using 10 sup_left_isotone spanning_forest_def by blast
                also have "...  --g  --h"
                  by (simp add: le_supI2 minarc_below)
                also have "... = --g"
                  using 1 by (metis kruskal_invariant_def kruskal_spanning_invariant_def pp_isotone_inf sup.orderE)
                finally show "?w  --g"
                  by simp
              next
                have 22: "?d  (?v  -?d)T * ?eT * top"
                  apply (rule kruskal_exchange_spanning_inv_2)
                  using 8 apply simp
                  using 13 apply (metis semiring.mult_not_zero star_absorb star_simulation_right_equal)
                  using 17 apply simp
                  by (simp add: inf.coboundedI1)
                have "components g  forest_components ?v"
                  using 10 spanning_forest_def by auto
                also have "...  forest_components ?w"
                  apply (rule kruskal_exchange_forest_components_inv)
                  using 21 apply simp
                  using 15 apply simp
                  using 1 apply (simp add: arc_top_arc minarc_arc)
                  apply (simp add: inf.coboundedI1)
                  using 13 apply simp
                  using 8 apply simp
                  apply (simp add: le_infI1)
                  using 22 by simp
                finally show "components g  forest_components ?w"
                  by simp
              next
                show "regular ?w"
                  using 3 7 regular_conv_closed by simp
              qed
            next
              have 23: "?e  g  bot"
                using 1 by (metis kruskal_invariant_def kruskal_spanning_invariant_def comp_inf.semiring.mult_zero_right inf.sup_monoid.add_assoc inf.sup_monoid.add_commute minarc_bot_iff minarc_meet_bot)
              have "g  -h  (g  -h)"
                using star.circ_increasing by simp
              also have "...  (--(g  -h))"
                using pp_increasing star_isotone by blast
              also have "...  ?F"
                using 1 kruskal_invariant_def kruskal_spanning_invariant_def inf.sup_monoid.add_commute spanning_forest_def by simp
              finally have 24: "g  -h  ?F"
                by simp
              have "?d  --g"
                using 10 inf.coboundedI1 spanning_forest_def by blast
              hence "?d  --g  -?F"
                using 16 inf.boundedI p_antitone_iff by simp
              also have "... = --(g  -?F)"
                by simp
              also have "...  --h"
                using 24 p_shunting_swap pp_isotone by fastforce
              finally have 25: "?d  --h"
                by simp
              have "?d = bot  top = bot"
                using 19 by (metis mult_left_zero mult_right_zero)
              hence "?d  bot"
                using 1 le_bot by auto
              hence 26: "?d  h  bot"
                using 25 by (metis inf.absorb_iff2 inf_commute pseudo_complement)
              have "sum (?e  g) = sum (?e  --h  g)"
                by (simp add: inf.absorb1 minarc_below)
              also have "... = sum (?e  h)"
                using 1 by (metis kruskal_invariant_def kruskal_spanning_invariant_def inf.left_commute inf.sup_monoid.add_commute)
              also have "...  sum (?d  h)"
                using 19 26 minarc_min by simp
              also have "... = sum (?d  (--h  g))"
                using 1 kruskal_invariant_def kruskal_spanning_invariant_def inf_commute by simp
              also have "... = sum (?d  g)"
                using 25 by (simp add: inf.absorb2 inf_assoc inf_commute)
              finally have 27: "sum (?e  g)  sum (?d  g)"
                by simp
              have "?v  ?e  -?d = bot"
                using 14 by simp
              hence "sum (?w  g) = sum (?v  -?d  g) + sum (?e  g)"
                using sum_disjoint inf_commute inf_assoc by simp
              also have "...  sum (?v  -?d  g) + sum (?d  g)"
                using 23 27 sum_plus_right_isotone by simp
              also have "... = sum (((?v  -?d)  ?d)  g)"
                using sum_disjoint inf_le2 pseudo_complement by simp
              also have "... = sum ((?v  ?d)  (-?d  ?d)  g)"
                by (simp add: sup_inf_distrib2)
              also have "... = sum ((?v  ?d)  g)"
                using 15 by (metis inf_top_right stone)
              also have "... = sum (?v  g)"
                by (simp add: inf.sup_monoid.add_assoc)
              finally have "sum (?w  g)  sum (?v  g)"
                by simp
              thus "u . spanning_forest u g  sum (?w  g)  sum (u  g)"
                using 2 11 minimum_spanning_forest_def by auto
            qed
          next
            have "?f  f  fT  ?e"
              using conv_dist_inf inf_le1 sup_left_isotone sup_mono by presburger
            also have "...  (?v  -?d  -?dT)  (?vT  -?d  -?dT)  ?e"
              using 17 sup_left_isotone by simp
            also have "...  (?v  -?d)  (?vT  -?d  -?dT)  ?e"
              using inf.cobounded1 sup_inf_distrib2 by presburger
            also have "... = ?w  (?vT  -?d  -?dT)"
              by (simp add: sup_assoc sup_commute)
            also have "...  ?w  (?vT  -?dT)"
              using inf.sup_right_isotone inf_assoc sup_right_isotone by simp
            also have "...  ?w  ?wT"
              using conv_complement conv_dist_inf conv_dist_sup sup_right_isotone by simp
            finally show "?f  ?w  ?wT"
              by simp
          qed
        qed
      next
        show "?n2 < ?n1"
          using 1 kruskal_vc_2 kruskal_invariant_def by auto
      qed
    qed
  next
    show "¬ ?e  -?F  kruskal_invariant f g ?h  ?n2 < ?n1"
      using 1 kruskal_vc_2 kruskal_invariant_def by auto
  qed
next
  fix f
  assume 28: "kruskal_invariant f g bot"
  hence 29: "spanning_forest f g"
    using kruskal_invariant_def kruskal_spanning_invariant_def by auto
  from 28 obtain w where 30: "minimum_spanning_forest w g  f  w  wT"
    using kruskal_invariant_def by auto
  hence "w = w  --g"
    by (simp add: inf.absorb1 minimum_spanning_forest_def spanning_forest_def)
  also have "...  w  components g"
    by (metis inf.sup_right_isotone star.circ_increasing)
  also have "...  w  fT * f"
    using 29 spanning_forest_def inf.sup_right_isotone by simp
  also have "...  f  fT"
    apply (rule cancel_separate_6[where z=w and y="wT"])
    using 30 minimum_spanning_forest_def spanning_forest_def apply simp
    using 30 apply (metis conv_dist_inf conv_dist_sup conv_involutive inf.cobounded2 inf.orderE)
    using 30 apply (simp add: sup_commute)
    using 30 minimum_spanning_forest_def spanning_forest_def apply simp
    using 30 by (metis acyclic_star_below_complement comp_inf.mult_right_isotone inf_p le_bot minimum_spanning_forest_def spanning_forest_def)
  finally have 31: "w  f  fT"
    by simp
  have "sum (f  g) = sum ((w  wT)  (f  g))"
    using 30 by (metis inf_absorb2 inf.assoc)
  also have "... = sum (w  (f  g)) + sum (wT  (f  g))"
    using 30 inf.commute acyclic_asymmetric sum_disjoint minimum_spanning_forest_def spanning_forest_def by simp
  also have "... = sum (w  (f  g)) + sum (w  (fT  gT))"
    by (metis conv_dist_inf conv_involutive sum_conv)
  also have "... = sum (f  (w  g)) + sum (fT  (w  g))"
    using 28 inf.commute inf.assoc kruskal_invariant_def kruskal_spanning_invariant_def by simp
  also have "... = sum ((f  fT)  (w  g))"
    using 29 acyclic_asymmetric inf.sup_monoid.add_commute sum_disjoint spanning_forest_def by simp
  also have "... = sum (w  g)"
    using 31 by (metis inf_absorb2 inf.assoc)
  finally show "minimum_spanning_forest f g"
    using 29 30 minimum_spanning_forest_def by simp
qed

end

end

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,Guttmann2018b}.
›

theory Prim

imports "HOL-Hoare.Hoare_Logic" Aggregation_Algebras.Aggregation_Algebras

begin

context m_kleene_algebra
begin

abbreviation "component g r  rT * (--g)"
definition "spanning_tree t g r  forest t  t  (component g r)T * (component g r)  --g  component g r  rT * 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 = gT  injective r  vector r  regular r"
definition "prim_spanning_invariant t v g r  prim_precondition g r  vT = rT * t  spanning_tree t (v * vT  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 "rT = rT * bot"
    by (simp add: star_absorb)
next
  let ?ss = "r * rT  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 * rT) r"
      by (simp add: mult_right_isotone star_isotone)
    also have "...  rT * 1"
      using assms by (metis order.eq_iff p_antitone regular_one_closed star_sub_one prim_precondition_def)
    also have "... = rT * bot"
      by (simp add: star.circ_zero star_one)
    finally show "component ?ss r  rT * bot"
      .
  next
    show "regular bot"
      by simp
  qed
qed

lemma prim_vc_2:
  assumes "prim_spanning_invariant t v g r"
      and "v * -vT  g  bot"
    shows "prim_spanning_invariant (t  minarc (v * -vT  g)) (v  minarc (v * -vT  g)T * top) g r  card { x . regular x  x  component g r  x  -(v  minarc (v * -vT  g)T * top)T } < card { x . regular x  x  component g r  x  -vT }"
proof -
  let ?vcv = "v * -vT  g"
  let ?e = "minarc ?vcv"
  let ?t = "t  ?e"
  let ?v = "v  ?eT * top"
  let ?c = "component g r"
  let ?g = "--g"
  let ?n1 = "card { x . regular x  x  ?c  x  -vT }"
  let ?n2 = "card { x . regular x  x  ?c  x  -?vT }"
  have 1: "regular v  regular (v * vT)  regular (?v * ?vT)  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 * vT  ?g"
    using assms(1) by (metis prim_spanning_invariant_def spanning_tree_def inf_pp_commute inf.boundedE)
  hence 3: "t  v * vT"
    by simp
  have 4: "t  ?g"
    using 2 by simp
  have 5: "?e  v * -vT  ?g"
    using 1 by (metis minarc_below pp_dist_inf regular_mult_closed regular_closed_p)
  hence 6: "?e  v * -vT"
    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 * tT = bot"
    using 3 6 7 et(2) by simp
  have 11: "arc ?e"
    using assms(2) minarc_arc by simp
  have "rT  rT * t"
    by (metis mult_right_isotone order_refl semiring.mult_not_zero star.circ_separate_mult_1 star_absorb)
  hence 12: "rT  vT"
    using assms(1) by (simp add: prim_spanning_invariant_def)
  have 13: "vector r  injective r  vT = rT * t"
    using assms(1) prim_spanning_invariant_def prim_precondition_def minimum_spanning_tree_def spanning_tree_def reachable_restrict by simp
  have "g = gT"
    using assms(1) prim_invariant_def prim_spanning_invariant_def prim_precondition_def by simp
  hence 14: "?gT = ?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 "?vT = rT * ?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 * ?vT  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 * ?vT  g) r  rT * ?t"
        proof -
          have 15: "rT * (v * vT  ?g)  rT * t"
            using assms(1) 1 by (metis prim_spanning_invariant_def spanning_tree_def inf_pp_commute)
          have "component (?v * ?vT  g) r = rT * (?v * ?vT  ?g)"
            using 1 by simp
          also have "...  rT * ?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 * ?eT * ?e"
        using 11 by (metis arc_top_edge mult_assoc)
      also have "...  vT * ?e"
        using 7 8 by (metis conv_dist_comp conv_isotone mult_left_isotone symmetric_top_closed)
      also have "...  vT * ?g"
        using 5 mult_right_isotone by auto
      also have "... = rT * t * ?g"
        using 13 by simp
      also have "...  rT * ?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  -vT"
      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: "-?vT = -vT  -(top * ?e)"
      by (simp add: conv_dist_comp conv_dist_sup)
    hence 20: "¬ top * ?e  -?vT"
      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 * -vT  g = bot"
    shows "spanning_tree t g r"
proof -
  let ?g = "--g"
  have 1: "regular v  regular (v * vT)"
    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 * -vT  ?g = bot"
    using assms(2) pp_inf_bot_iff pp_pp_inf_bot_iff by simp
  have 3: "vT = rT * 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 * vT  ?g"
    using assms(1) 1 by (metis prim_spanning_invariant_def inf_pp_commute spanning_tree_def inf.boundedE)
  have "rT * (v * vT  ?g)  rT * t"
    using assms(1) 1 by (metis prim_spanning_invariant_def inf_pp_commute spanning_tree_def)
  hence 5: "component g r = vT"
    using 1 2 3 4 by (metis span_post)
  have "regular (v * vT)"
    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 * vT  ?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 * -vT  g  bot
    INV { prim_spanning_invariant t v g r }
    VAR { card { x . regular x  x  component g r  -vT } }
     DO e := minarc (v * -vT  g);
        t := t  e;
        v := v  eT * 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 * -vT  g  bot
    INV { prim_invariant t v g r }
    VAR { card { x . regular x  x  component g r  -vT } }
     DO e := minarc (v * -vT  g);
        t := t  e;
        v := v  eT * 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 * -vT  g"
  let ?vv = "v * vT  g"
  let ?e = "minarc ?vcv"
  let ?t = "t  ?e"
  let ?v = "v  ?eT * top"
  let ?c = "component g r"
  let ?g = "--g"
  let ?n1 = "card { x . regular x  x  ?c  x  -vT }"
  let ?n2 = "card { x . regular x  x  ?c  x  -?vT }"
  assume 1: "prim_invariant t v g r  ?vcv  bot"
  hence 2: "regular v  regular (v * vT)"
    by (metis (no_types, hide_lams) 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 * vT  ?g"
    using 1 2 by (metis (no_types, hide_lams) prim_invariant_def prim_spanning_invariant_def spanning_tree_def inf_pp_commute inf.boundedE)
  hence 4: "t  v * vT"
    by simp
  have 5: "t  ?g"
    using 3 by simp
  have 6: "?e  v * -vT  ?g"
    using 2 by (metis minarc_below pp_dist_inf regular_mult_closed regular_closed_p)
  hence 7: "?e  v * -vT"
    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  vT = rT * t  forest w  t  w  w  ?cT * ?c  ?g  rT * (?cT * ?c  ?g)  rT * 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 = gT"
    using 1 prim_invariant_def prim_spanning_invariant_def prim_precondition_def by simp
  hence 14: "?gT = ?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 * -vT  top * ?e * wT"
      let ?p = "w  -v * -vT  top * ?e * wT"
      let ?fp = "w  -vT  top * ?e * wT"
      let ?w = "(w  -?fp)  ?pT  ?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  ?cT * ?c  --g"
            proof -
              have 16: "w  -?fp  ?cT * ?c  --g"
                using 10 by (simp add: le_infI1 minimum_spanning_tree_def spanning_tree_def)
              have "?pT  wT"
                by (simp add: conv_isotone inf.sup_monoid.add_assoc)
              also have "...  (?cT * ?c  --g)T"
                using 11 conv_order by simp
              also have "... = ?cT * ?c  --g"
                using 2 14 conv_dist_comp conv_dist_inf by simp
              finally have 17: "?pT  ?cT * ?c  --g"
                .
              have "?e  ?cT * ?c  ?g"
                using 5 6 11 mst_subgraph_inv by auto
              thus ?thesis
                using 16 17 by simp
            qed
          next
            show "?c  rT * ?w"
            proof -
              have "?c  rT * w"
                using 10 minimum_spanning_tree_def spanning_tree_def by simp
              also have "...  rT * ?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 * -vT  top * ?e * wT)"
            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 * -vT  ?g  bot"
            using 2 11 by (simp add: inf.absorb1 le_infI1)
          hence "g  (?f  v * -vT)  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 (?pT  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)  ?pT)  g) + sum (?e  g)"
            using 11 by (metis epm_8 sum_disjoint)
          also have "...  sum (((w  -?fp)  ?pT)  g) + sum (?f  g)"
            using 23 24 by (simp add: sum_plus_right_isotone)
          also have "... = sum (w  -?fp  g) + sum (?pT  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 * -vT  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 = vT"
    by (metis 25 prim_invariant_def span_tree_component prim_spanning_invariant_def spanning_tree_def)
  hence 28: "w  v * vT"
    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

Theory Boruvka

(* Title:      Borůvka's Minimum Spanning Tree Algorithm
   Author:     Nicolas Robinson-O'Brien
   Maintainer: Walter Guttmann <walter.guttmann at canterbury.ac.nz>
*)

section ‹Bor\r{u}vka's Minimum Spanning Tree Algorithm›

text ‹
In this theory we prove partial correctness of Bor\r{u}vka's minimum spanning tree algorithm.
›

theory Boruvka

imports
  Relational_Disjoint_Set_Forests.Disjoint_Set_Forests
  Kruskal

begin

subsection ‹General results›

text ‹
The proof is carried out in $m$-$k$-Stone-Kleene relation algebras.
In this section we give results that hold more generally.
›

context stone_kleene_relation_algebra
begin

definition "big_forest H d 
    equivalence H
   d  -H
   univalent (H * d)
   H  d * dT  1
   (H * d)+  - H"

definition "bf_between_points p q H d  point p  point q  p  (H * d) * H * d"

definition "bf_between_arcs a b H d  arc a  arc b  aT * top  (H * d) * H * b * top"

text ‹Theorem 3›

lemma He_eq_He_THe_star:
  assumes "arc e"
    and "equivalence H"
  shows "H * e = H * e * (top * H * e)"
proof -
  let ?x = "H * e"
  have 1: "H * e  H * e * (top * H * e)"
    using comp_isotone star.circ_reflexive by fastforce
  have "H * e * (top * H * e) = H * e * (top * e)"
    by (metis assms(2) preorder_idempotent surjective_var)
  also have "...  H * e * (1  top * (e * top) * e)"
    by (metis eq_refl star.circ_mult_1)
  also have "...  H * e * (1  top * top * e)"
    by (simp add: star.circ_left_top)
  also have "... = H * e  H * e * top * e"
    by (simp add: mult.semigroup_axioms semiring.distrib_left semigroup.assoc)
  finally have 2: "H * e * (top * H * e)  H * e"
    using assms arc_top_arc mult_assoc by auto
  thus ?thesis
    using 1 2 by simp
qed

lemma path_through_components:
  assumes "equivalence H"
    and "arc e"
  shows "(H * (d  e)) = (H * d)  (H * d) * H * e * (H * d)"
proof -
  have "H * e * (H * d) * H * e  H * e * top * H * e"
    by (simp add: comp_isotone)
  also have "... = H * e * top * e"
    by (metis assms(1) preorder_idempotent surjective_var mult_assoc)
  also have "... = H * e"
    using assms(2) arc_top_arc mult_assoc by auto
  finally have 1: "H * e * (H * d) * H * e  H * e"
    by simp
  have "(H * (d  e)) = (H * d  H * e)"
    by (simp add: comp_left_dist_sup)
  also have "... = (H * d)  (H * d) * H * e * (H * d)"
    using 1 star_separate_3 by (simp add: mult_assoc)
  finally show ?thesis
    by simp
qed

lemma simplify_f:
  assumes "regular p"
    and "regular e"
  shows "(f  - eT  - p)  (f  - eT  p)  (f  - eT  p)T  (f  - eT  - p)T  eT  e = f  fT  e  eT"
proof -
  have "(f  - eT  - p)  (f  - eT  p)  (f  - eT  p)T  (f  - eT  - p)T  eT  e
    = (f  - eT  - p)  (f  - eT  p)  (fT  - e  pT)  (fT  - e  - pT)  eT  e"
    by (simp add: conv_complement conv_dist_inf)
  also have "... =
      ((f  (f  - eT  p))  (- eT  (f  - eT  p))  (- p  (f  - eT  p)))
     ((fT  (fT  - e  - pT))  (- e  (fT  - e  - pT))  (pT  (fT  - e  - pT)))
     eT  e"
    by (metis sup_inf_distrib2 sup_assoc)
  also have "... =
      ((f  f)  (f  - eT)  (f  p)  (- eT  f)  (- eT  - eT)  (- eT  p)  (- p  f)  (- p  - eT)  (- p  p))
     ((fT  fT)  (fT  - e)  (fT  - pT)  (- e  fT)  (- e  - e)  (- e  - pT)  (pT  fT)  (pT  - e)  (pT  - pT))
     eT  e"
    using sup_inf_distrib1 sup_assoc inf_assoc sup_inf_distrib1 by simp
  also have "... =
      ((f  f)  (f  - eT)  (f  p)  (f  - p)  (- eT  f)  (- eT  - eT)  (- eT  p)  (- eT  - p)  (- p  p))
     ((fT  fT)  (fT  - e)  (fT  - pT)  (- e  fT)  (fT  pT)  (- e  - e)  (- e  - pT)  (- e  pT)  (pT  - pT))
     eT  e"
    by (smt abel_semigroup.commute inf.abel_semigroup_axioms inf.left_commute sup.abel_semigroup_axioms)
  also have "... = (f  - eT  (- p  p))  (fT  - e  (pT  - pT))  eT  e"
    by (smt inf.sup_monoid.add_assoc inf.sup_monoid.add_commute inf_sup_absorb sup.idem)
  also have "... = (f  - eT)  (fT  - e)  eT  e"
    by (metis assms(1) conv_complement inf_top_right stone)
  also have "... = (f  eT)  (- eT  eT)  (fT  e)  (- e  e)"
    by (metis sup.left_commute sup_assoc sup_inf_distrib2)
  finally show ?thesis
    by (metis abel_semigroup.commute assms(2) conv_complement inf_top_right stone sup.abel_semigroup_axioms sup_assoc)
qed

lemma simplify_forest_components_f:
  assumes "regular p"
    and "regular e"
    and "injective (f  - eT  - p  (f  - eT  p)T  e)"
    and "injective f"
  shows "forest_components ((f  - eT  - p)  (f  -eT  p)T  e) = (f  fT  e  eT)"
proof -
  have "forest_components ((f  - eT  - p)  (f  -eT  p)T  e) = wcc ((f  - eT  - p)  (f  - eT  p)T  e)"
    by (simp add: assms(3) forest_components_wcc)
  also have "... = ((f  - eT  - p)  (f  - eT  p)T  e  (f  - eT  - p)T  (f  - eT  p)  eT)"
    using conv_dist_sup sup_assoc by auto
  also have "... = ((f  - eT  - p)  (f  - eT  p)  (f  - eT  p)T  (f  - eT  - p)T  eT  e)"
    using sup_assoc sup_commute by auto
  also have "... = (f  fT  e  eT)"
    using assms(1, 2, 3, 4) simplify_f by auto
  finally show ?thesis
    by simp
qed

lemma components_disj_increasing:
  assumes "regular p"
    and "regular e"
    and "injective (f  - eT  - p  (f  - eT  p)T  e)"
    and "injective f"
  shows "forest_components f  forest_components (f  - eT  - p  (f  - eT  p)T  e)"
proof -
  have 1: "forest_components ((f  - eT  - p)  (f  -eT  p)T  e) = (f  fT  e  eT)"
    using simplify_forest_components_f assms(1, 2, 3, 4) by blast
  have "forest_components f = wcc f"
    by (simp add: assms(4) forest_components_wcc)
  also have "...  (f  fT  eT  e)"
    by (simp add: le_supI2 star_isotone sup_commute)
  finally show ?thesis
    using 1 sup.left_commute sup_commute by simp
qed

lemma fch_equivalence:
  assumes "forest h"
  shows "equivalence (forest_components h)"
  by (simp add: assms forest_components_equivalence)

lemma big_forest_path_split_1:
  assumes "arc a"
    and "equivalence H"
  shows "(H * d) * H * a * top = (H * (d  - a)) * H * a * top"
proof -
  let ?H = "H"
  let ?x = "?H * (d  -a)"
  let ?y = "?H * a"
  let ?a = "?H * a * top"
  let ?d = "?H * d"
  have 1: "?d * ?a  ?x * ?a"
  proof -
    have "?x *?y * ?x * ?a  ?x * ?a * ?a"
      by (smt mult_left_isotone star.circ_right_top top_right_mult_increasing mult_assoc)
    also have "... = ?x * ?a * a * top"
      by (metis ex231e mult_assoc)
    also have "... = ?x * ?a"
      by (simp add: assms(1) mult_assoc)
    finally have 11: "?x *?y * ?x * ?a  ?x * ?a"
      by simp
    have "?d * ?a = (?H * (d  a)  ?H * (d  -a)) * ?a"
    proof -
      have 12: "regular a"
        using assms(1) arc_regular by simp
      have "?H * ((d  a)  (d  - a)) = ?H * (d  top)"
        using 12 by (metis inf_top_right maddux_3_11_pp)
      thus ?thesis
        using mult_left_dist_sup by auto
    qed
    also have "...  (?y  ?x) * ?a"
      by (metis comp_inf.coreflexive_idempotent comp_isotone inf.cobounded1 inf.sup_monoid.add_commute semiring.add_mono star_isotone top.extremum)
    also have "... = (?x  ?y) * ?a"
      by (simp add: sup_commute mult_assoc)
    also have "... = ?x * ?a  (?x * ?y * (?x * ?y) * ?x) * ?a"
      by (smt mult_right_dist_sup star.circ_sup_9 star.circ_unfold_sum mult_assoc)
    also have "...  ?x * ?a  (?x * ?y * (top * ?y) * ?x) * ?a"
    proof -
      have "(?x * ?y)  (top * ?y)"
        by (simp add: mult_left_isotone star_isotone)
      thus ?thesis
        by (metis comp_inf.coreflexive_idempotent comp_inf.transitive_star eq_refl mult_left_dist_sup top.extremum mult_assoc)
    qed
    also have "... = ?x * ?a  (?x * ?y * ?x) * ?a"
      using assms(1, 2) He_eq_He_THe_star arc_regular mult_assoc by auto
    finally have 13: "(?H * d) * ?a  ?x * ?a  ?x * ?y * ?x * ?a"
      by (simp add: mult_assoc)
    have 14: "?x * ?y * ?x * ?a  ?x * ?a"
      using 11 mult_assoc by auto
    thus ?thesis
      using 13 14 sup.absorb1 by auto
  qed
  have 2: "?d * ?a  ?x *?a"
    by (simp add: comp_isotone star_isotone)
  thus ?thesis
    using 1 2 antisym mult_assoc by simp
qed

lemma dTransHd_le_1:
  assumes "equivalence H"
    and "univalent (H * d)"
  shows "dT * H * d  1"
proof -
  have "dT * HT * H * d  1"
    using assms(2) conv_dist_comp mult_assoc by auto
  thus ?thesis
    using assms(1) mult_assoc by (simp add: preorder_idempotent)
qed

lemma HcompaT_le_compHaT:
  assumes "equivalence H"
    and "injective (a * top)"
  shows "-H * a * top  - (H * a * top)"
proof -
  have "a * top * aT  1"
    by (metis assms(2) conv_dist_comp symmetric_top_closed vector_top_closed mult_assoc)
  hence "a * top * aT * H  H"
    using assms(1) comp_isotone order_trans by blast
  hence "a * top * top * aT * H  H"
    by (simp add: vector_mult_closed)
  hence "a * top * (H * a * top)T  H"
    by (metis assms(1) conv_dist_comp symmetric_top_closed vector_top_closed mult_assoc)
  thus ?thesis
    using assms(2) comp_injective_below_complement mult_assoc by auto
qed

text ‹Theorem 4›

lemma expand_big_forest:
  assumes "big_forest H d"
  shows "(dT * H) * (H * d) = (dT * H)  (H * d)"
proof -
  have "(H * d)T * H * d  1"
    using assms big_forest_def mult_assoc by auto
  hence "dT * H * H * d  1"
    using assms big_forest_def conv_dist_comp by auto
  thus ?thesis
    by (simp add: cancel_separate_eq comp_associative)
qed


lemma big_forest_path_bot:
  assumes "arc a"
    and "a  d"
    and "big_forest H d"
  shows "(d  - a)T * (H * a * top)  bot"
proof -
  have 1: "dT * H * d  1"
    using assms(3) big_forest_def dTransHd_le_1 by blast
  hence "d * - 1 * dT  - H"
    using triple_schroeder_p by force
  hence "d * - 1 * dT  1  - H"
    by (simp add: le_supI2)
  hence "d * dT  d * - 1 * dT  1  - H"
    by (metis assms(3) big_forest_def inf_commute regular_one_closed shunting_p le_supI)
  hence "d * 1 * dT  d * - 1 * dT  1  - H"
    by simp
  hence "d * (1  - 1) * dT  1  - H"
    using comp_associative mult_right_dist_sup by (simp add: mult_left_dist_sup)
  hence "d * top * dT  1  - H"
    using regular_complement_top by auto
  hence "d * top * aT  1  - H"
    using assms(2) conv_isotone dual_order.trans mult_right_isotone by blast
  hence "d * (a * top)T  1  - H"
    by (simp add: comp_associative conv_dist_comp)
  hence "d  (1  - H) * (a * top)"
    by (simp add: assms(1) shunt_bijective)
  hence "d  a * top  - H * a * top"
    by (simp add: comp_associative mult_right_dist_sup)
  also have "...  a * top  - (H * a * top)"
    using assms(1, 3) HcompaT_le_compHaT big_forest_def sup_right_isotone by auto
  finally have "d  a * top  - (H * a * top)"
    by simp
  hence "d  --( H * a * top)  a * top"
    using shunting_var_p by auto
  hence 2:"d  H * a * top  a * top"
    using inf.sup_right_isotone order.trans pp_increasing by blast
  have 3:"d  H * a * top  top * a"
  proof -
    have "d  H * a * top  (H * a  d * topT) * (top  (H * a)T * d)"
      by (metis dedekind inf_commute)
    also have "... = d * top  H * a * aT * HT * d"
      by (simp add: conv_dist_comp inf_vector_comp mult_assoc)
    also have "...  d * top  H * a * dT * HT * d"
      using assms(2) mult_right_isotone mult_left_isotone conv_isotone inf.sup_right_isotone by auto
    also have "... = d * top  H * a * dT * H * d"
      using assms(3) big_forest_def by auto
    also have "...  d * top  H * a * 1"
      using 1 by (metis inf.sup_right_isotone mult_right_isotone mult_assoc)
    also have "...  H * a"
      by simp
    also have "...  top * a"
      by (simp add: mult_left_isotone)
    finally have "d  H * a * top  top * a"
      by simp
    thus ?thesis
      by simp
  qed
  have "d  H * a * top  a * top  top * a"
    using 2 3 by simp
  also have "... = a * top * top * a"
    by (metis comp_associative comp_inf.star.circ_decompose_9 comp_inf.star_star_absorb comp_inf_covector vector_inf_comp vector_top_closed)
  also have "... = a * top * a"
    by (simp add: vector_mult_closed)
  finally have 4:"d  H * a * top  a"
    by (simp add: assms(1) arc_top_arc)
  hence "d  - a  -(H * a * top)"
    using assms(1) arc_regular p_shunting_swap by fastforce
  hence "(d  - a) * top  -(H * a * top)"
    using mult.semigroup_axioms p_antitone_iff schroeder_4_p semigroup.assoc by fastforce
  thus ?thesis
    by (simp add: schroeder_3_p)
qed

lemma big_forest_path_split_2:
  assumes "arc a"
    and "a  d"
    and "big_forest H d"
  shows "(H * (d  - a)) * H * a * top = (H * ((d  - a)  (d  - a)T)) * H * a * top"
proof -
  let ?lhs = "(H * (d  - a)) * H * a * top"
  have 1: "dT * H * d  1"
    using assms(3) big_forest_def dTransHd_le_1 by blast
  have 2: "H * a * top  ?lhs"
    by (metis le_iff_sup star.circ_loop_fixpoint star.circ_transitive_equal star_involutive sup_commute mult_assoc)
  have "(d  - a)T * (H * (d  - a)) * (H * a * top) = (d  - a)T * H * (d  - a) * (H * (d  - a)) * (H * a * top)"
  proof -
    have "(d  - a)T * (H * (d  - a)) * (H * a * top) = (d  - a)T * (1  H * (d  - a) * (H * (d  - a))) * (H * a * top)"
      by (simp add: star_left_unfold_equal)
    also have "... = (d  - a)T * H * a * top  (d  - a)T * H * (d  - a) * (H * (d  - a)) * (H * a * top)"
      by (smt mult_left_dist_sup star.circ_loop_fixpoint star.circ_mult_1 star_slide sup_commute mult_assoc)
    also have "... = bot  (d  - a)T * H * (d  - a) * (H * (d  - a)) * (H * a * top)"
      by (metis assms(1, 2, 3) big_forest_path_bot mult_assoc le_bot)
    thus ?thesis
      by (simp add: calculation)
  qed
  also have "...  dT * H * d * (H * (d  - a)) * (H * a * top)"
    using conv_isotone inf.cobounded1 mult_isotone by auto
  also have "...  1 * (H * (d  - a)) * (H * a * top)"
    using 1 by (metis le_iff_sup mult_right_dist_sup)
  finally have 3: "(d  - a)T * (H * (d  - a)) * (H * a * top)  ?lhs"
    using mult_assoc by auto
  hence 4: "H * (d  - a)T * (H * (d  - a)) * (H * a * top)  ?lhs"
  proof -
    have "H * (d  - a)T * (H * (d  - a)) * (H * a * top)  H * (H * (d  - a)) * H * a * top"
      using 3 mult_right_isotone mult_assoc by auto
    also have "... = H * H * ((d  - a) * H) * H * a * top"
      by (metis assms(3) big_forest_def star_slide mult_assoc preorder_idempotent)
    also have "... = H * ((d  - a) * H) * H * a * top"
      using assms(3) big_forest_def preorder_idempotent by fastforce
    finally show ?thesis
      by (metis assms(3) big_forest_def preorder_idempotent star_slide mult_assoc)
  qed
  have 5: "(H * (d  - a)  H * (d  - a)T) * (H * (d  - a)) * H * a * top  ?lhs"
  proof -
    have 51: "H * (d  - a) * (H * (d  - a)) * H * a * top  (H * (d  - a)) * H * a * top"
      using star.left_plus_below_circ mult_left_isotone by simp
    have 52: "(H * (d  - a)  H * (d  - a)T) * (H * (d  - a)) * H * a * top = H * (d  - a) * (H * (d  - a)) * H * a * top  H * (d  - a)T * (H * (d  - a)) * H * a * top"
      using mult_right_dist_sup by auto
    hence "...  (H * (d  - a)) * H * a * top  H * (d  - a)T * (H * (d  - a)) * H * a * top"
      using star.left_plus_below_circ mult_left_isotone sup_left_isotone by auto
    thus ?thesis
      using 4 51 52 mult_assoc by auto
  qed
  hence "(H * (d  - a)  H * (d  - a)T) * H * a * top  ?lhs"
  proof -
    have "(H * (d  - a)  H * (d  - a)T) * (H * (d  - a)) * H * a * top  ?lhs"
      using 5 star_left_induct_mult_iff mult_assoc by auto
    thus ?thesis
      using star.circ_decompose_11 star_decompose_1 by auto
  qed
  hence 6: "(H * ((d  - a)  (d  - a)T)) * H * a * top  ?lhs"
    using mult_left_dist_sup by auto
  have 7: "(H * (d  - a)) * H * a * top  (H * ((d  - a)  (d  - a)T)) * H * a * top"
    by (simp add: mult_left_isotone semiring.distrib_left star_isotone)
  thus ?thesis
    using 6 7 by (simp add: mult_assoc)
qed

end

subsection ‹An operation to select components›

text ‹
We introduce the operation choose_component›.
\begin{itemize}
\item Axiom component_in_v› expresses that the result of choose_component› is contained in the set of vertices, $v$, we are selecting from, ignoring the weights.
\item Axiom component_is_vector› states that the result of choose_component› is a vector.
\item Axiom component_is_regular› states that the result of choose_component› is regular.
\item Axiom component_is_connected› states that any two vertices from the result of choose_component› are connected in $e$.
\item Axiom component_single› states that the result of choose_component› is closed under being connected in $e$.
\item Finally, axiom component_not_bot_when_v_bot_bot› expresses that the operation choose_component› returns a non-empty component if the input satisfies the given criteria.
\end{itemize}
›

class choose_component =
  fixes choose_component :: "'a  'a  'a"

class choose_component_algebra = choose_component + stone_relation_algebra +
  assumes component_in_v: "choose_component e v  --v"
  assumes component_is_vector: "vector (choose_component e v)"
  assumes component_is_regular: "regular (choose_component e v)"
  assumes component_is_connected: "choose_component e v * (choose_component e v)T  e"
  assumes component_single: "choose_component e v = e * choose_component e v"
  assumes component_not_bot_when_v_bot_bot: "
      regular e
     equivalence e
     vector v
     regular v
     e * v = v
     v  bot  choose_component e v  bot"

text ‹Theorem 1›

text ‹
Every m_kleene_algebra› is an instance of choose_component_algebra› when the choose_component› operation is defined as follows:
›

context m_kleene_algebra
begin

definition "choose_component_input_condition e v 
    regular e
   equivalence e
   vector v
   regular v
   e * v = v"

definition "m_choose_component e v 
  if choose_component_input_condition e v then
    e * minarc(v) * top
  else
    bot"

sublocale m_choose_component_algebra: choose_component_algebra where choose_component = m_choose_component
proof
  fix e v
  show "m_choose_component e v  -- v"
  proof (cases "choose_component_input_condition e v")
    case True
    hence "m_choose_component e v = e * minarc(v) * top"
      by (simp add: m_choose_component_def)
    also have "...  e * --v * top"
      by (simp add: comp_isotone minarc_below)
    also have "... = e * v * top"
      using True choose_component_input_condition_def by auto
    also have "... = v * top"
      using True choose_component_input_condition_def by auto
    finally show ?thesis
      using True choose_component_input_condition_def by auto
  next
    case False
    hence "m_choose_component e v = bot"
      using False m_choose_component_def by auto
    thus ?thesis
      by simp
  qed
next
  fix e v
  show "vector (m_choose_component e v)"
  proof (cases "choose_component_input_condition e v")
    case True
    thus ?thesis
      by (simp add: mult_assoc m_choose_component_def)
  next
    case False
    thus ?thesis
      by (simp add: m_choose_component_def)
  qed
next
  fix e v
  show "regular (m_choose_component e v)"
    using choose_component_input_condition_def minarc_regular regular_closed_star regular_mult_closed m_choose_component_def by auto
next
  fix e v
  show "m_choose_component e v * (m_choose_component e v)T  e"
  proof (cases "choose_component_input_condition e v")
    case True
    assume 1: "choose_component_input_condition e v"
    hence "m_choose_component e v * (m_choose_component e v)T = e * minarc(v) * top * (e * minarc(v) * top)T"
      by (simp add: m_choose_component_def)
    also have "... = e * minarc(v) * top * topT * minarc(v)T * eT"
      by (metis comp_associative conv_dist_comp)
    also have "... = e * minarc(v) * top * top * minarc(v)T * e"
      using 1 choose_component_input_condition_def by auto
    also have "... = e * minarc(v) * top * minarc(v)T * e"
      by (simp add: comp_associative)
    also have "...  e"
    proof (cases "v = bot")
      case True
      thus ?thesis
        by (simp add: True minarc_bot)
    next
      case False
      assume 3: "v  bot"
      hence "e * minarc(v) * top * minarc(v)T  e * 1"
        using 3 minarc_arc arc_expanded comp_associative mult_right_isotone by fastforce
      hence "e * minarc(v) * top * minarc(v)T * e  e * 1 * e"
        using mult_left_isotone by auto
      also have "... = e"
        using 1 choose_component_input_condition_def preorder_idempotent by auto
      thus ?thesis
        using calculation by auto
    qed
    thus ?thesis
      by (simp add: calculation)
  next
    case False
    thus ?thesis
      by (simp add: m_choose_component_def)
  qed
next
  fix e v
  show "m_choose_component e v = e * m_choose_component e v"
  proof (cases "choose_component_input_condition e v")
    case True
    thus ?thesis
      by (metis choose_component_input_condition_def preorder_idempotent m_choose_component_def mult_assoc)
  next
    case False
    thus ?thesis
      by (simp add: m_choose_component_def)
  qed
next
  fix e v
  show "regular e  equivalence e  vector v  regular v  e * v = v  v  bot  m_choose_component e v  bot"
  proof (cases "choose_component_input_condition e v")
    case True
    hence "m_choose_component e v  minarc(v) * top"
      by (metis choose_component_input_condition_def mult_1_left mult_left_isotone m_choose_component_def)
    also have "...  minarc(v)"
      using calculation dual_order.trans top_right_mult_increasing by blast
    thus ?thesis
      using True bot_unique minarc_bot_iff by fastforce
  next
    case False
    thus ?thesis
      using choose_component_input_condition_def by blast
  qed
qed

end

subsection ‹m-k-Stone-Kleene relation algebras›

text ‹
$m$-$k$-Stone-Kleene relation algebras are an extension of $m$-Kleene algebras where the choose_component› operation has been added.
›

class m_kleene_algebra_choose_component =
  m_kleene_algebra
  + choose_component_algebra
begin

text ‹
A selected_edge› is a minimum-weight edge whose source is in a component, with respect to $h$, $j$ and $g$, and whose target is not in that component.
›

abbreviation "selected_edge h j g  minarc (choose_component (forest_components h) j * - choose_component (forest_components h) jT  g)"

text ‹
A path› is any sequence of edges in the forest, $f$, of the graph, $g$, backwards from the target of the selected_edge› to a root in $f$.
›

abbreviation "path f h j g  top * selected_edge h j g * (f  - selected_edge h j gT)T"

definition "boruvka_outer_invariant f g 
    symmetric g
   forest f
   f  --g
   regular f
   (w . minimum_spanning_forest w g  f  w  wT)"

definition "boruvka_inner_invariant j f h g d 
    boruvka_outer_invariant f g
   g  bot
   vector j
   regular j
   boruvka_outer_invariant h g
   forest h
   forest_components h  forest_components f
   big_forest (forest_components h) d
   d * top  - j
   forest_components h * j = j
   forest_components f = (forest_components h * (d  dT)) * forest_components h
   f  fT = h  hT  d  dT
   ( a b . bf_between_arcs a b (forest_components h) d  a  -(forest_components h)  -- g  b  d
     sum(b  g)  sum(a  g))
   regular d"

lemma expression_equivalent_without_e_complement:
  assumes "selected_edge h j g  - forest_components f"
  shows "f  - (selected_edge h j g)T  - (path f h j g)  (f  - (selected_edge h j g)T  (path f h j g))T  (selected_edge h j g)
         = f  - (path f h j g)  (f  (path f h j g))T  (selected_edge h j g)"
proof -
  let ?p = "path f h j g"
  let ?e = "selected_edge h j g"
  let ?F = "forest_components f"
  have 1: "?e  - ?F"
    by (simp add: assms)
  have "fT  ?F"
    by (metis conv_dist_comp conv_involutive conv_order conv_star_commute forest_components_increasing)
  hence "- ?F  - fT"
    using p_antitone by auto
  hence "?e  - fT"
    using 1 dual_order.trans by blast
  hence "fT  - ?e"
    by (simp add: p_antitone_iff)
  hence "fTT  - ?eT"
    by (metis conv_complement conv_dist_inf inf.orderE inf.orderI)
  hence "f  - ?eT"
    by auto
  hence "f = f  - ?eT"
    using inf.orderE by blast
  hence "f  - ?eT  - ?p  (f  - ?eT  ?p)T  ?e = f  - ?p  (f  ?p)T  ?e"
    by auto
  thus ?thesis by auto
qed

text ‹Theorem 2›

text ‹
The source of the selected_edge› is contained in $j$, the vector describing those vertices still to be processed in the inner loop of Bor\r{u}vka's algorithm.
›

lemma et_below_j:
  assumes "vector j"
    and "regular j"
    and "j  bot"
  shows "selected_edge h j g * top  j"
proof -
  let ?e = "selected_edge h j g"
  let ?c = "choose_component (forest_components h) j"
  have "?e * top  --(?c * -?cT  g) * top"
    using comp_isotone minarc_below by blast
  also have "... = (--(?c * -?cT)  --g) * top"
    by simp
  also have "... = (?c * -?cT  --g) * top"
    using component_is_regular regular_mult_closed by auto
  also have "... = (?c  -?cT  --g) * top"
    by (metis component_is_vector conv_complement vector_complement_closed vector_covector)
  also have "...  ?c * top"
    using inf.cobounded1 mult_left_isotone order_trans by blast
  also have "...  j * top"
    by (metis assms(2) comp_inf.star.circ_sup_2 comp_isotone component_in_v)
  also have "... = j"
    by (simp add: assms(1))
  finally show ?thesis
    by simp
qed

subsubsection ‹Components of forests and big forests›

text ‹
We prove a number of properties about big_forest› and forest_components›.
›

lemma fc_j_eq_j_inv:
  assumes "forest h"
    and "forest_components h * j = j"
  shows "forest_components h * (j  - choose_component (forest_components h) j) = j  - choose_component (forest_components h) j"
proof -
  let ?c = "choose_component (forest_components h) j"
  let ?H = "forest_components h"
  have 1:"equivalence ?H"
    by (simp add: assms(1) forest_components_equivalence)
  have "?H * (j  - ?c) = ?H * j  ?H * - ?c"
    using 1 by (metis assms(2) equivalence_comp_dist_inf inf.sup_monoid.add_commute)
  hence 2: "?H * (j  - ?c) = j  ?H * - ?c"
    by (simp add: assms(2))
  have 3: "j  - ?c  ?H * - ?c"
    using 1 by (metis assms(2) dedekind_1 dual_order.trans equivalence_comp_dist_inf inf.cobounded2)
  have "?H * ?c  ?c"
    using component_single by auto
  hence "?HT * ?c  ?c"
    using 1 by simp
  hence "?H * - ?c  - ?c"
    using component_is_regular schroeder_3_p by force
  hence "j  ?H * - ?c  j  - ?c"
    using inf.sup_right_isotone by auto
  thus ?thesis
    using 2 3 order.antisym by simp
qed

text ‹Theorem 5›

text ‹
There is a path in the big_forest› between edges $a$ and $b$ if and only if there is either a path in the big_forest› from $a$ to $b$ or one from $a$ to $c$ and one from $c$ to $b$.
›

lemma big_forest_path_split_disj:
  assumes "equivalence H"
    and "arc c"
    and "regular a  regular b  regular c  regular d  regular H"
  shows "bf_between_arcs a b H (d  c)  bf_between_arcs a b H d  (bf_between_arcs a c H d  bf_between_arcs c b H d)"
proof -
  have 1: "bf_between_arcs a b H (d  c)  bf_between_arcs a b H d  (bf_between_arcs a c H d  bf_between_arcs c b H d)"
  proof (rule impI)
    assume 11: "bf_between_arcs a b H (d  c)"
    hence "aT * top  (H * (d  c)) * H * b * top"
      by (simp add: bf_between_arcs_def)
    also have "... = ((H * d)  (H * d) * H * c * (H * d)) * H * b * top"
      using assms(1, 2) path_through_components by simp
    also have "... = (H * d) * H * b * top  (H * d) * H * c * (H * d) * H * b * top"
      by (simp add: mult_right_dist_sup)
    finally have 12:"aT * top  (H * d) * H * b * top  (H * d) * H * c * (H * d) * H * b * top"
      by simp
    have 13: "aT * top  (H * d) * H * b * top  aT * top  (H * d) * H * c * (H * d) * H * b * top"
    proof (rule point_in_vector_sup)
      show "point (aT * top)"
        using 11 bf_between_arcs_def mult_assoc by auto
    next
      show "vector ((H * d) * H * b * top)"
        using vector_mult_closed by simp
    next
      show "regular ((H * d) * H * b * top)"
        using assms(3) pp_dist_comp pp_dist_star by auto
    next
      show "aT * top  (H * d) * H * b * top  (H * d) * H * c * (H * d) * H * b * top"
        using 12 by simp
    qed
    thus "bf_between_arcs a b H d  (bf_between_arcs a c H d  bf_between_arcs c b H d)"
    proof (cases "aT * top  (H * d) * H * b * top")
      case True
      assume "aT * top  (H * d) * H * b * top"
      hence "bf_between_arcs a b H d"
        using 11 bf_between_arcs_def by auto
      thus ?thesis
        by simp
    next
      case False
      have 14: "aT * top  (H * d) * H * c * (H * d) * H * b * top"
        using 13 by (simp add: False)
      hence 15: "aT * top  (H * d) * H * c * top"
        by (metis mult_right_isotone order_lesseq_imp top_greatest mult_assoc)
      have "cT * top  (H * d) * H * b * top"
      proof (rule ccontr)
        assume "¬ cT * top  (H * d) * H * b * top"
        hence "cT * top  -((H * d) * H * b * top)"
          by (meson assms(2, 3) point_in_vector_or_complement regular_closed_star regular_closed_top regular_mult_closed vector_mult_closed vector_top_closed)
        hence "c * (H * d) * H * b * top  bot"
          using schroeder_3_p mult_assoc by auto
        thus "False"
          using 13 False sup.absorb_iff1 mult_assoc by auto
      qed
      hence "bf_between_arcs a c H d  bf_between_arcs c b H d"
        using 11 15 assms(2) bf_between_arcs_def by auto
      thus ?thesis
        by simp
    qed
  qed
  have 2: "bf_between_arcs a b H d  (bf_between_arcs a c H d  bf_between_arcs c b H d)  bf_between_arcs a b H (d  c)"
  proof -
    have 21: "bf_between_arcs a b H d  bf_between_arcs a b H (d  c)"
    proof (rule impI)
      assume 22:"bf_between_arcs a b H d"
      hence "aT * top  (H * d) * H * b * top"
        using bf_between_arcs_def by blast
      hence "aT * top  (H * (d  c)) * H * b * top"
        by (simp add: mult_left_isotone mult_right_dist_sup mult_right_isotone order.trans star_isotone star_slide)
      thus "bf_between_arcs a b H (d  c)"
        using 22 bf_between_arcs_def by blast
    qed
    have "bf_between_arcs a c H d  bf_between_arcs c b H d  bf_between_arcs a b H (d  c)"
    proof (rule impI)
      assume 23: "bf_between_arcs a c H d  bf_between_arcs c b H d"
      hence "aT * top  (H * d) * H * c * top"
        using bf_between_arcs_def by blast
      also have "...  (H * d) * H * c * cT * c * top"
        by (metis ex231c comp_inf.star.circ_sup_2 mult_isotone mult_right_isotone mult_assoc)
      also have "...  (H * d) * H * c * cT * top"
        by (simp add: mult_right_isotone mult_assoc)
      also have "...  (H * d) * H * c * (H * d) * H * b * top"
        using 23 mult_right_isotone mult_assoc by (simp add: bf_between_arcs_def)
      also have "...  (H * d) * H * b * top  (H * d) * H * c * (H * d) * H * b * top"
        by (simp add: bf_between_arcs_def)
      finally have "aT * top  (H * (d  c)) * H * b * top"
        using assms(1, 2) path_through_components mult_right_dist_sup by simp
      thus "bf_between_arcs a b H (d  c)"
        using 23 bf_between_arcs_def by blast
    qed
    thus ?thesis
      using 21 by auto
  qed
  thus ?thesis
    using 1 2 by blast
qed

lemma dT_He_eq_bot:
  assumes "vector j"
    and "regular j"
    and "d * top  - j"
    and "forest_components h * j = j"
    and "j  bot"
  shows "dT * forest_components h * selected_edge h j g  bot"
proof -
  let ?e = "selected_edge h j g"
  let ?H = "forest_components h"
  have 1: "?e * top  j"
    using assms(1, 2, 5) et_below_j by auto
  have "dT * ?H * ?e  (d * top)T * ?H * (?e * top)"
    by (simp add: comp_isotone conv_isotone top_right_mult_increasing)
  also have "...  (d * top)T * ?H * j"
    using 1 mult_right_isotone by auto
  also have "...  (- j)T * ?H * j"
    by (simp add: assms(3) conv_isotone mult_left_isotone)
  also have "... = (- j)T * j"
    using assms(4) comp_associative by auto
  also have "... = bot"
    by (simp add: assms(1) conv_complement covector_vector_comp)
  finally show ?thesis
    using coreflexive_bot_closed le_bot by blast
qed

lemma big_forest_d_U_e:
  assumes "forest f"
    and "vector j"
    and "regular j"
    and "forest h"
    and "forest_components h  forest_components f"
    and "big_forest (forest_components h) d"
    and "d * top  - j"
    and "forest_components h * j = j"
    and "f  fT = h  hT  d  dT"
    and "selected_edge h j g  - forest_components f"
    and "selected_edge h j g  bot"
    and "j  bot"
  shows "big_forest (forest_components h) (d  selected_edge h j g)"
proof (unfold big_forest_def, intro conjI)
  let ?H = "forest_components h"
  let ?F = "forest_components f"
  let ?e = "selected_edge h j g"
  let ?d' = "d  ?e"
  show 01: "reflexive ?H"
    by (simp add: assms(4) forest_components_equivalence)
  show 02: "transitive ?H"
    by (simp add: assms(4) forest_components_equivalence)
  show 03: "symmetric ?H"
    by (simp add: assms(4) forest_components_equivalence)
  have 04: "equivalence ?H"
    by (simp add: 01 02 03)
  show 1: "?d'  - ?H"
  proof -
    have "?H  ?F"
      by (simp add: assms(5))
    hence 11: "?e  - ?H"
      using assms(10) order_lesseq_imp p_antitone by blast
    have "d  - ?H"
      using assms(6) big_forest_def by auto
    thus ?thesis
      by (simp add: 11)
  qed
  show "univalent (?H * ?d')"
  proof -
    have "(?H * ?d')T * (?H * ?d') = ?d'T * ?HT * ?H * ?d'"
      using conv_dist_comp mult_assoc by auto
    also have "... = ?d'T * ?H * ?H * ?d'"
      by (simp add: conv_dist_comp conv_star_commute)
    also have "... = ?d'T * ?H * ?d'"
      using 01 02 by (metis preorder_idempotent mult_assoc)
    finally have 21: "univalent (?H * ?d')  ?eT * ?H * d  dT * ?H * ?e  ?eT * ?H * ?e  dT * ?H * d  1"
      using conv_dist_sup semiring.distrib_left semiring.distrib_right by auto
    have 22: "?eT * ?H * ?e  1"
    proof -
      have 221: "?eT * ?H * ?e  ?eT * top * ?e"
        by (simp add: mult_left_isotone mult_right_isotone)
      have "arc ?e"
        using assms(11) minarc_arc minarc_bot_iff by blast
      hence "?eT * top * ?e  1"
        using arc_expanded by blast
      thus ?thesis
        using 221 dual_order.trans by blast
    qed
    have 24: "dT * ?H * ?e  1"
      by (metis assms(2, 3, 7, 8, 12) dT_He_eq_bot coreflexive_bot_closed le_bot)
    hence "(dT * ?H * ?e)T  1T"
      using conv_isotone by blast
    hence "?eT * ?HT * dTT  1"
      by (simp add: conv_dist_comp mult_assoc)
    hence 25: "?eT * ?H * d  1"
      using assms(4) fch_equivalence by auto
    have 8: "dT * ?H * d  1"
      using 04 assms(6) dTransHd_le_1 big_forest_def by blast
    thus ?thesis
      using 21 22 24 25 by simp
  qed
  show "coreflexive (?H  ?d' * ?d'T)"
  proof -
    have "coreflexive (?H  ?d' * ?d'T)  ?H  (d  ?e) * (dT  ?eT)  1"
      by (simp add: conv_dist_sup)
    also have "...  ?H  (d * dT  d * ?eT  ?e * dT  ?e * ?eT)  1"
      by (metis mult_left_dist_sup mult_right_dist_sup sup.left_commute sup_commute)
    finally have 1: "coreflexive (?H  ?d' * ?d'T)  ?H  d * dT  ?H  d * ?eT  ?H  ?e * dT  ?H  ?e * ?eT  1"
      by (simp add: inf_sup_distrib1)
    have 31: "?H  d * dT  1"
      using assms(6) big_forest_def by blast
    have 32: "?H  ?e * dT  1"
    proof -
      have "?e * dT  ?e * top * (d * top)T"
        by (simp add: conv_isotone mult_isotone top_right_mult_increasing)
      also have "...  ?e * top * - jT"
        by (metis assms(7) conv_complement conv_isotone mult_right_isotone)
      also have "...  j * - jT"
        using assms(2, 3, 12) et_below_j mult_left_isotone by auto
      also have "...  - ?H"
        using 03 by (metis assms(2, 3, 8) conv_complement conv_dist_comp equivalence_top_closed mult_left_isotone schroeder_3_p vector_top_closed)
      finally have "?e * dT  - ?H"
        by simp
      thus ?thesis
        by (metis inf.coboundedI1 p_antitone_iff p_shunting_swap regular_one_closed)
    qed
    have 33: "?H  d * ?eT  1"
    proof -
      have 331: "injective h"
        by (simp add: assms(4))
      have "(?H  ?e * dT)T  1"
        using 32 coreflexive_conv_closed by auto
      hence "?H  (?e * dT)T  1"
        using 331 conv_dist_inf forest_components_equivalence by auto
      thus ?thesis
        using conv_dist_comp by auto
    qed
    have 34: "?H  ?e * ?eT  1"
    proof -
      have 341:"arc ?e  arc (?eT)"
        using assms(11) minarc_arc minarc_bot_iff by auto
      have "?H  ?e * ?eT  ?e * ?eT"
        by auto
      thus ?thesis
        using 341 arc_injective le_infI2 by blast
    qed
    thus ?thesis
      using 1 31 32 33 34 by simp
  qed
  show 4:"(?H * (d  ?e))+  - ?H"
  proof -
    have "?e  - ?F"
      by (simp add: assms(10))
    hence "?F  - ?e"
      by (simp add: p_antitone_iff)
    hence "?FT * ?F  - ?e"
      using assms(1) fch_equivalence by fastforce
    hence "?FT * ?F * ?FT  - ?e"
      by (metis assms(1) fch_equivalence forest_components_star star.circ_decompose_9)
    hence 41: "?F * ?e * ?F  - ?F"
      using triple_schroeder_p by blast
    hence 42:"(?F * ?F) * ?F * ?e * (?F * ?F)  - ?F"
    proof -
      have 43: "?F * ?F = ?F"
        using assms(1) forest_components_equivalence preorder_idempotent by auto
      hence "?F * ?e * ?F = ?F * ?F * ?e * ?F"
        by simp
      also have "... = (?F) * ?F * ?e * (?F)"
        by (simp add: assms(1) forest_components_star)
      also have "... = (?F * ?F) * ?F * ?e * (?F * ?F)"
        using 43 by simp
      finally show ?thesis
        using 41 by simp
    qed
    hence 44: "(?H * d) * ?H * ?e * (?H * d)  - ?H"
    proof -
      have 45: "?H  ?F"
        by (simp add: assms(5))
      hence 46:"?H * ?e  ?F * ?e"
        by (simp add: mult_left_isotone)
      have "d  f  fT"
        using assms(9) sup.left_commute sup_commute by auto
      also have "...  ?F"
        by (metis forest_components_increasing le_supI2 star.circ_back_loop_fixpoint star.circ_increasing sup.bounded_iff)
      finally have "d  ?F"
        by simp
      hence "?H * d  ?F * ?F"
        using 45 mult_isotone by auto
      hence 47: "(?H * d)  (?F * ?F)"
        by (simp add: star_isotone)
      hence "(?H * d) * ?H * ?e * (?H * d)  (?H * d) * ?F * ?e * (?H * d)"
        using 46 by (metis mult_left_isotone mult_right_isotone mult_assoc)
      also have "...  (?F * ?F) * ?F * ?e * (?F * ?F)"
        using 47 mult_left_isotone mult_right_isotone by (simp add: comp_isotone)
      also have "...  - ?F"
        using 42 by simp
      also have "...  - ?H"
        using 45 by (simp add: p_antitone)
      finally show ?thesis
        by simp
    qed
    have "(?H * (d  ?e))+ = (?H * (d  ?e)) * (?H * (d  ?e))"
      using star.circ_plus_same by auto
    also have "... = ((?H * d)  (?H * d) * ?H * ?e * (?H * d)) * (?H * (d  ?e))"
      using assms(4, 11) forest_components_equivalence minarc_arc minarc_bot_iff path_through_components by auto
    also have "... = (?H * d) * (?H * (d  ?e))  (?H * d) * ?H * ?e * (?H * d) * (?H * (d  ?e))"
      using mult_right_dist_sup by auto
    also have "... = (?H * d) * (?H * d  ?H * ?e)  (?H * d) * ?H * ?e * (?H * d) * (?H * d  ?H * ?e)"
      by (simp add: mult_left_dist_sup)
    also have "... = (?H * d) * ?H * d  (?H * d) * ?H * ?e  (?H * d) * ?H * ?e * (?H * d) * (?H * d  ?H * ?e)"
      using mult_left_dist_sup mult_assoc by auto
    also have "... = (?H * d)+  (?H * d) * ?H * ?e  (?H * d) * ?H * ?e * (?H * d) * (?H * d  ?H * ?e)"
      by (simp add: star.circ_plus_same mult_assoc)
    also have "... = (?H * d)+  (?H * d) * ?H * ?e  (?H * d) * ?H * ?e * (?H * d) * ?H * d  (?H * d) * ?H * ?e * (?H * d) * ?H * ?e"
      by (simp add: mult.semigroup_axioms semiring.distrib_left sup.semigroup_axioms semigroup.assoc)
    also have "...  (?H * d)+  (?H * d) * ?H * ?e  (?H * d) * ?H * ?e * (?H * d) * ?H * d  (?H * d) * ?H * ?e"
    proof -
      have "?e * (?H * d) * ?H * ?e  ?e * top * ?e"
        by (metis comp_associative comp_inf.coreflexive_idempotent comp_inf.coreflexive_transitive comp_isotone top.extremum)
      also have "...  ?e"
        using assms(11) arc_top_arc minarc_arc minarc_bot_iff by auto
      finally have "?e * (?H * d) * ?H * ?e  ?e"
        by simp
      hence "(?H * d) * ?H * ?e * (?H * d) * ?H * ?e  (?H * d) * ?H * ?e"
        by (simp add: comp_associative comp_isotone)
      thus ?thesis
        using sup_right_isotone by blast
    qed
    also have "... = (?H * d)+  (?H * d) * ?H * ?e  (?H * d) * ?H * ?e * (?H * d) * ?H * d"
      by (simp add: order.eq_iff ac_simps)
    also have "... = (?H * d)+  (?H * d) * ?H * ?e  (?H * d) * ?H * ?e * (?H * d)+"
      using star.circ_plus_same mult_assoc by auto
    also have "... = (?H * d)+  (?H * d) * ?H * ?e * (1  (?H * d)+)"
      by (simp add: mult_left_dist_sup sup_assoc)
    also have "... = (?H * d)+  (?H * d) * ?H * ?e * (?H * d)"
      by (simp add: star_left_unfold_equal)
    also have "...  - ?H"
      using 44 assms(6) big_forest_def by auto
    finally show ?thesis
      by simp
  qed
qed

subsubsection ‹Identifying arcs›

text ‹
The expression $d \sqcap \top e^\top H \sqcap (H d^\top)^* H a^\top \top$ identifies the edge incoming to the component that the selected_edge›, $e$, is outgoing from and which is on the path from edge $a$ to $e$.
Here, we prove this expression is an arc›.
›

lemma shows_arc_x:
  assumes "big_forest H d"
    and "bf_between_arcs a e H d"
    and "H * d * (H * d)  - H"
    and "¬ aT * top  H * e * top"
    and "regular a"
    and "regular e"
    and "regular H"
    and "regular d"
  shows "arc (d  top * eT * H  (H * dT) * H * aT * top)"
proof -
  let ?x = "d  top * eT * H  (H * dT) * H * aT * top"
  have 1:"regular ?x"
    using assms(5, 6, 7, 8) regular_closed_star regular_conv_closed regular_mult_closed by auto
  have 2: "aT * top * a  1"
    using arc_expanded assms(2) bf_between_arcs_def by auto
  have 3: "e * top * eT  1"
    using assms(2) bf_between_arcs_def arc_expanded by blast
  have 4: "top * ?x * top = top"
  proof -
    have "aT * top  (H * d) * H * e * top"
      using assms(2) bf_between_arcs_def by blast
    also have "... = H * e * top  (H * d) * H * d * H * e * top"
      by (metis star.circ_loop_fixpoint star.circ_plus_same sup_commute mult_assoc)
    finally have "aT * top  H * e * top  (H * d) * H * d * H * e * top"
      by simp
    hence "aT * top  H * e * top  aT * top  (H * d) * H * d * H * e * top"
      using assms(2, 6, 7) point_in_vector_sup bf_between_arcs_def regular_mult_closed vector_mult_closed by auto
    hence "aT * top  (H * d) * H * d * H * e * top"
      using assms(4) by blast
    also have "... = (H * d) * H * d * (H * e * top  H * e * top)"
      by (simp add: mult_assoc)
    also have "... = (H * d) * H * (d  (H * e * top)T) * H * e * top"
      by (metis comp_associative covector_inf_comp_3 star.circ_left_top star.circ_top)
    also have "... = (H * d) * H * (d  topT * eT * HT) * H * e * top"
      using conv_dist_comp mult_assoc by auto
    also have "... = (H * d) * H * (d  top * eT * H) * H * e * top"
      using assms(1) by (simp add: big_forest_def)
    finally have 2: "aT * top  (H * d) * H * (d  top * eT * H) * H * e * top"
      by simp
    hence "e * top  ((H * d) * H * (d  top * eT * H) * H)T * aT * top"
    proof -
      have "bijective (e * top)  bijective (aT * top)"
        using assms(2) bf_between_arcs_def by auto
      thus ?thesis
        using 2 by (metis bijective_reverse mult_assoc)
    qed
    also have "... = HT * (d  top * eT * H)T * HT * (H * d)T * aT * top"
      by (simp add: conv_dist_comp mult_assoc)
    also have "... = H * (d  top * eT * H)T * H * (H * d)T * aT * top"
      using assms(1) big_forest_def by auto
    also have "... = H * (d  top * eT * H)T * H * (dT * H) * aT * top"
      using assms(1) big_forest_def conv_dist_comp conv_star_commute by auto
    also have "... = H * (dT  H * e * top) * H * (dT * H) * aT * top"
      using assms(1) conv_dist_comp big_forest_def comp_associative conv_dist_inf by auto
    also have "... = H * (dT  H * e * top) * (H * dT) * H * aT * top"
      by (simp add: comp_associative star_slide)
    also have "... = H * (dT  H * e * top) * ((H * dT) * H * aT * top  (H * dT) * H * aT * top)"
      using mult_assoc by auto
    also have "... = H * (dT  H * e * top  ((H * dT) * H * aT * top)T) * (H * dT) * H * aT * top"
      by (smt comp_inf_vector covector_comp_inf vector_conv_covector vector_top_closed mult_assoc)
    also have "... = H * (dT  (top * eT * H)T  ((H * dT) * H * aT * top)T) * (H * dT) * H * aT * top"
      using assms(1) big_forest_def conv_dist_comp mult_assoc by auto
    also have "... = H * (d  top * eT * H  (H * dT) * H * aT * top)T * (H * dT) * H * aT * top"
      by (simp add: conv_dist_inf)
    finally have 3: "e * top  H * ?xT * (H * dT) * H * aT * top"
      by auto
    have "?x  bot"
    proof (rule ccontr)
      assume "¬ ?x  bot"
      hence "e * top = bot"
        using 3 le_bot by auto
      thus "False"
        using assms(2, 4) bf_between_arcs_def mult_assoc semiring.mult_zero_right by auto
    qed
    thus ?thesis
      using 1 using tarski by blast
  qed
  have 5: "?x * top * ?xT  1"
  proof -
    have 51: "H * (d * H)  d * H * dT  1"
    proof -
      have 511: "d * (H * d)  - H"
        using assms(1, 3) big_forest_def preorder_idempotent schroeder_4_p triple_schroeder_p by fastforce
      hence "(d * H) * d  - H"
        using star_slide by auto
      hence "H * (dT * H)  - d"
        by (smt assms(1) big_forest_def conv_dist_comp conv_star_commute schroeder_4_p star_slide)
      hence "H * (d * H)  - dT"
        using 511 by (metis assms(1) big_forest_def schroeder_5_p star_slide)
      hence "H * (d * H)  - (H * dT)"
        by (metis assms(3) p_antitone_iff schroeder_4_p star_slide mult_assoc)
      hence "H * (d * H)  H * dT  bot"
        by (simp add: bot_unique pseudo_complement)
      hence "H * d * (H * (d * H)  H * dT)  1"
        by (simp add: bot_unique)
      hence 512: "H * d * H * (d * H)  H * d * H * dT  1"
        using univalent_comp_left_dist_inf assms(1) big_forest_def mult_assoc by fastforce
      hence 513: "H * d * H * (d * H)  d * H * dT  1"
      proof -
        have "d * H * dT  H * d * H * dT"
          by (metis assms(1) big_forest_def conv_dist_comp conv_involutive mult_1_right mult_left_isotone)
        thus ?thesis
          using 512 by (smt dual_order.trans p_antitone p_shunting_swap regular_one_closed)
      qed
      have "dT * H * d  1  - H"
        using assms(1) big_forest_def dTransHd_le_1 le_supI1 by blast
      hence "(- 1  H) * dT * H  - dT"
        by (metis assms(1) big_forest_def dTransHd_le_1 inf.sup_monoid.add_commute le_infI2 p_antitone_iff regular_one_closed schroeder_4_p mult_assoc)
      hence "d * (- 1  H) * dT  - H"
        by (metis assms(1) big_forest_def conv_dist_comp schroeder_3_p triple_schroeder_p)
      hence "H  d * (- 1  H) * dT  1"
        by (metis inf.coboundedI1 p_antitone_iff p_shunting_swap regular_one_closed)
      hence "H  d * dT  H  d * (- 1  H) * dT  1"
        using assms(1) big_forest_def le_supI by blast
      hence "H  (d * 1 * dT  d * (- 1  H) * dT)  1"
        using comp_inf.semiring.distrib_left by auto
      hence "H  (d * (1  (- 1  H)) * dT)  1"
        by (simp add: mult_left_dist_sup mult_right_dist_sup)
      hence 514: "H  d * H * dT  1"
        by (metis assms(1) big_forest_def comp_inf.semiring.distrib_left inf.le_iff_sup inf.sup_monoid.add_commute inf_top_right regular_one_closed stone)
      thus ?thesis
      proof -
        have "H  d * H * dT  H * d * H * (d * H)  d * H * dT  1"
          using 513 514 by simp
        hence "d * H * dT  (H  H * d * H * (d * H))  1"
          by (simp add: comp_inf.semiring.distrib_left inf.sup_monoid.add_commute)
        hence "d * H * dT  H * (1  d * H * (d * H))  1"
          by (simp add: mult_left_dist_sup mult_assoc)
        thus ?thesis
          by (simp add: inf.sup_monoid.add_commute star_left_unfold_equal)
      qed
    qed
    have "?x * top * ?xT = (d  top * eT * H  (H * dT) * H * aT * top) * top * (dT  HT * eTT * topT  topT * aTT * HT * (dTT * HT))"
      by (simp add: conv_dist_comp conv_dist_inf conv_star_commute mult_assoc)
    also have "... = (d  top * eT * H  (H * dT) * H * aT * top) * top * (dT  H * e * top  top * a * H * (d * H))"
      using assms(1) big_forest_def by auto
    also have "... = (H * dT) * H * aT * top  (d  top * eT * H) * top * (dT  H * e * top  top * a * H * (d * H))"
      by (metis inf_vector_comp vector_export_comp)
    also have "... = (H * dT) * H * aT * top  (d  top * eT * H) * top * top * (dT  H * e * top  top * a * H * (d * H))"
      by (simp add: vector_mult_closed)
    also have "... = (H * dT) * H * aT * top  d * ((top * eT * H)T  top) * top * (dT  H * e * top  top * a * H * (d * H))"
      by (simp add: covector_comp_inf_1 covector_mult_closed)
    also have "... = (H * dT) * H * aT * top  d * ((top * eT * H)T  (H * e * top)T) * dT  top * a * H * (d * H)"
      by (smt comp_associative comp_inf.star_star_absorb comp_inf_vector conv_star_commute covector_comp_inf covector_conv_vector fc_top star.circ_top total_conv_surjective vector_conv_covector vector_inf_comp)
    also have "... = (H * dT) * H * aT * top  top * a * H * (d * H)  d * ((top * eT * H)T  (H * e * top)T) * dT"
      using inf.sup_monoid.add_assoc inf.sup_monoid.add_commute by auto
    also have "... = (H * dT) * H * aT * top * top * a * H * (d * H)  d * ((top * eT * H)T  (H * e * top)T) * dT"
      by (smt comp_inf.star.circ_decompose_9 comp_inf.star_star_absorb comp_inf_covector fc_top star.circ_decompose_11 star.circ_top vector_export_comp)
    also have "... = (H * dT) * H * aT * top * a * H * (d * H)  d * (H * e * top  top * eT * H) * dT"
      using assms(1) big_forest_def conv_dist_comp mult_assoc by auto
    also have "... = (H * dT) * H * aT * top * a * H * (d * H)  d * H * e * top * eT * H * dT"
      by (metis comp_inf_covector inf_top.left_neutral mult_assoc)
    also have "...  (H * dT) * (H * d) * H  d * H * e * top * eT * H * dT"
    proof -
      have "(H * dT) * H * aT * top * a * H * (d * H)  (H * dT) * H * 1 * H * (d * H)"
        using 2 by (metis comp_associative comp_isotone mult_left_isotone mult_semi_associative star.circ_transitive_equal)
      also have "... = (H * dT) * H * (d * H)"
        using assms(1) big_forest_def mult.semigroup_axioms preorder_idempotent semigroup.assoc by fastforce
      also have "... = (H * dT) * (H * d) * H"
        by (metis star_slide mult_assoc)
      finally show ?thesis
        using inf.sup_left_isotone by auto
    qed
    also have "...  (H * dT) * (H * d) * H  d * H * dT"
    proof -
      have "d * H * e * top * eT * H * dT  d * H * 1 * H * dT"
        using 3 by (metis comp_isotone idempotent_one_closed mult_left_isotone mult_sub_right_one mult_assoc)
      also have "...  d * H * dT"
        by (metis assms(1) big_forest_def mult_left_isotone mult_one_associative mult_semi_associative preorder_idempotent)
      finally show ?thesis
        using inf.sup_right_isotone by auto
    qed
    also have "... = H * (dT * H) * (H * d) * H  d * H * dT"
      by (metis assms(1) big_forest_def comp_associative preorder_idempotent star_slide)
    also have "... = H * ((dT * H)  (H * d)) * H  d * H * dT"
      by (simp add: assms(1) expand_big_forest mult.semigroup_axioms semigroup.assoc)
    also have "... = (H * (dT * H) * H  H * (H * d) * H)  d * H * dT"
      by (simp add: mult_left_dist_sup mult_right_dist_sup)
    also have "... = (H * dT) * H  d * H * dT  H * (d * H)  d * H * dT"
      by (smt assms(1) big_forest_def inf_sup_distrib2 mult.semigroup_axioms preorder_idempotent star_slide semigroup.assoc)
    also have "...  (H * dT) * H  d * H * dT  1"
      using 51 comp_inf.semiring.add_left_mono by blast
    finally have "?x * top * ?xT  1"
      using 51 by (smt assms(1) big_forest_def conv_dist_comp conv_dist_inf conv_dist_sup conv_involutive conv_star_commute equivalence_one_closed mult.semigroup_axioms sup.absorb2 semigroup.assoc conv_isotone conv_order)
    thus ?thesis
      by simp
  qed
  have 6: "?xT * top * ?x  1"
  proof -
    have "?xT * top * ?x = (dT  HT * eTT * topT  topT * aTT * HT * (dTT * HT)) * top * (d  top * eT * H  (H * dT) * H * aT * top)"
      by (simp add: conv_dist_comp conv_dist_inf conv_star_commute mult_assoc)
    also have "... = (dT  H * e * top  top * a * H * (d * H)) * top * (d  top * eT * H  (H * dT) * H * aT * top)"
      using assms(1) big_forest_def by auto
    also have "... = H * e * top  (dT  top * a * H * (d * H)) * top * (d  top * eT * H  (H * dT) * H * aT * top)"
      by (smt comp_associative inf.sup_monoid.add_assoc inf.sup_monoid.add_commute star.circ_left_top star.circ_top vector_inf_comp)
    also have "... = H * e * top  dT * ((top * a * H * (d * H))T  top) * (d  top * eT * H  (H * dT) * H * aT * top)"
      by (simp add: covector_comp_inf_1 covector_mult_closed)
    also have "... = H * e * top  dT * (d * H)T * H * aT * top * (d  top * eT * H  (H * dT) * H * aT * top)"
      using assms(1) big_forest_def comp_associative conv_dist_comp by auto
    also have "... = H * e * top  dT * (d * H)T * H * aT * top * (d  (H * dT) * H * aT * top)  top * eT * H"
      by (smt comp_associative comp_inf_covector inf.sup_monoid.add_assoc inf.sup_monoid.add_commute)
    also have "... = H * e * top  dT * (d * H)T * H * aT * (top  ((H * dT) * H * aT * top)T) * d  top * eT * H"
      by (metis comp_associative comp_inf_vector vector_conv_covector vector_top_closed)
    also have "... = H * e * top  (H * e * top)T  dT * (d * H)T * H * aT * ((H * dT) * H * aT * top)T * d"
      by (smt assms(1) big_forest_def conv_dist_comp inf.left_commute inf.sup_monoid.add_commute symmetric_top_closed mult_assoc inf_top.left_neutral)
    also have "... = H * e * top * (H * e * top)T  dT * (d * H)T * H * aT * ((H * dT) * H * aT * top)T * d"
      using vector_covector vector_mult_closed by auto
    also have "... = H * e * top * topT * eT * HT  dT * (d * H)T * H * aT * topT * aTT * HT * (H * dT)T * d"
      by (smt conv_dist_comp mult.semigroup_axioms symmetric_top_closed semigroup.assoc)
    also have "... = H * e * top * top * eT * H  dT * (H * dT) * H * aT * top * a * H * (d * H) * d"
      using assms(1) big_forest_def conv_dist_comp conv_star_commute by auto
    also have "... = H * e * top * eT * H  dT * (H * dT) * H * aT * top * a * H * (d * H) * d"
      using vector_top_closed mult_assoc by auto
    also have "...  H  dT * (H * dT) * H * (d * H) * d"
    proof -
      have "H * e * top * eT * H  H * 1 * H"
        using 3 by (metis comp_associative mult_left_isotone mult_right_isotone)
      also have "... = H"
        using assms(1) big_forest_def preorder_idempotent by auto
      finally have 611: "H * e * top * eT * H  H"
        by simp
      have "dT * (H * dT) * H * aT * top * a * H * (d * H) * d  dT * (H * dT) * H * 1 * H * (d * H) * d"
        using 2 by (metis comp_associative mult_left_isotone mult_right_isotone)
      also have "... = dT * (H * dT) * H * (d * H) * d"
        using assms(1) big_forest_def mult.semigroup_axioms preorder_idempotent semigroup.assoc by fastforce
      finally have "dT * (H * dT) * H * aT * top * a * H * (d * H) * d  dT * (H * dT) * H * (d * H) * d"
        by simp
      thus ?thesis
        using 611 comp_inf.comp_isotone by blast
    qed
    also have "... = H  (dT * H) * dT * H * d * (H * d)"
      using star_slide mult_assoc by auto
    also have "...  H  (dT * H) * (H * d)"
    proof -
      have "(dT * H) * dT * H * d * (H * d)  (dT * H) * 1 * (H * d)"
        by (smt assms(1) big_forest_def conv_dist_comp mult_left_isotone mult_right_isotone preorder_idempotent mult_assoc)
      also have "... = (dT * H) * (H * d)"
        by simp
      finally show ?thesis
        using inf.sup_right_isotone by blast
    qed
    also have "... = H  ((dT * H)  (H * d))"
      by (simp add: assms(1) expand_big_forest)
    also have "... = H  (dT * H)  H  (H * d)"
      by (simp add: comp_inf.semiring.distrib_left)
    also have "... = 1  H  (dT * H)+  H  (H * d)+"
    proof -
      have 612: "H  (H * d) = 1  H  (H * d)+"
        using assms(1) big_forest_def reflexive_inf_star by blast
      have "H  (dT * H) = 1  H  (dT * H)+"
        using assms(1) big_forest_def reflexive_inf_star by auto
      thus ?thesis
        using 612 sup_assoc sup_commute by auto
    qed
    also have "...  1"
    proof -
      have 613: "H  (H * d)+  1"
        by (metis assms(3) inf.coboundedI1 p_antitone_iff p_shunting_swap regular_one_closed)
      hence "H  (dT * H)+  1"
        by (metis assms(1) big_forest_def conv_dist_comp conv_dist_inf conv_plus_commute coreflexive_symmetric)
      thus ?thesis
        by (simp add: 613)
    qed
    finally show ?thesis
      by simp
  qed
  have 7:"bijective (?x * top)"
    using 4 5 6 arc_expanded by blast
  have "bijective (?xT * top)"
    using 4 5 6 arc_expanded by blast
  thus ?thesis
    using 7 by simp
qed

text ‹
To maintain that $f$ can be extended to a minimum spanning forest we identify an edge, $i = v \sqcap \overline{F}e\top \sqcap \top e^\top F$, that may be exchanged with the selected_edge›, $e$.
Here, we show that $i$ is an arc›.
›

lemma boruvka_edge_arc:
  assumes "equivalence F"
    and "forest v"
    and "arc e"
    and "regular F"
    and "F  forest_components (F  v)"
    and "regular v"
    and "v * eT = bot"
    and "e * F * e = bot"
    and "eT  v"
    and "e  bot"
  shows "arc (v  -F * e * top  top * eT * F)"
proof -
  let ?i = "v  -F * e * top  top * eT * F"
  have 1: "?iT * top * ?i  1"
  proof -
    have "?iT * top * ?i = (vT  top * eT * -F  F * e * top) * top * (v  -F * e * top  top * eT * F)"
      using assms(1) conv_complement conv_dist_comp conv_dist_inf mult.semigroup_axioms semigroup.assoc by fastforce
    also have "... = F * e * top  (vT  top * eT * -F) * top * (v  -F * e * top)  top * eT * F"
      by (smt covector_comp_inf covector_mult_closed inf_vector_comp vector_export_comp vector_top_closed)
    also have "... = F * e * top  (vT  top * eT * -F) * top * top * (v  -F * e * top)  top * eT * F"
      by (simp add: comp_associative)
    also have "... = F * e * top  vT * (top  (top * eT * -F)T) * top * (v  -F * e * top)  top * eT * F"
      using comp_associative comp_inf_vector_1 by auto
    also have "... = F * e * top  vT * (top  (top * eT * -F)T) * (top  (-F * e * top)T) * v  top * eT * F"
      by (smt comp_inf_vector conv_dist_comp mult.semigroup_axioms symmetric_top_closed semigroup.assoc)
    also have "... = F * e * top  vT * (top * eT * -F)T * (-F * e * top)T * v  top * eT * F"
      by simp
    also have "... = F * e * top  vT * -FT * eTT * topT * topT * eT * -FT * v  top * eT * F"
      by (metis comp_associative conv_complement conv_dist_comp)
    also have "... = F * e * top  vT * -F * e * top * top * eT * -F * v  top * eT * F"
      by (simp add: assms(1))
    also have "... = F * e * top  vT * -F * e * top  top * eT * -F * v  top * eT * F"
      by (metis comp_associative comp_inf_covector inf.sup_monoid.add_assoc inf_top.left_neutral vector_top_closed)
    also have "... = (F  vT * -F) * e * top  top * eT * -F * v  top * eT * F"
      using assms(3) injective_comp_right_dist_inf mult_assoc by auto
    also have "... = (F  vT * -F) * e * top  top * eT * (F  -F * v)"
      using assms(3) conv_dist_comp inf.sup_monoid.add_assoc inf.sup_monoid.add_commute mult.semigroup_axioms univalent_comp_left_dist_inf semigroup.assoc by fastforce
    also have "... = (F  vT * -F) * e * top * top * eT * (F  -F * v)"
      by (metis comp_associative comp_inf_covector inf_top.left_neutral vector_top_closed)
    also have "... = (F  vT * -F) * e * top * eT * (F  -F * v)"
      by (simp add: comp_associative)
    also have "...  (F  vT * -F) * (F  -F * v)"
      by (smt assms(3) conv_dist_comp mult_left_isotone shunt_bijective symmetric_top_closed top_right_mult_increasing mult_assoc)
    also have "...  (F  vT * -F) * (F  -F * v)  F"
      by (metis assms(1) inf.absorb1 inf.cobounded1 mult_isotone preorder_idempotent)
    also have "...  (F  vT * -F) * (F  -F * v)  (F  v)T * (F  v)"
      using assms(5) comp_inf.mult_right_isotone by auto
    also have "...  (-F  vT) * -F * -F * (-F  v)  (F  v)T * (F  v)"
    proof -
      have "F  vT * -F  (vT  F * -FT) * -F"
        by (metis conv_complement dedekind_2 inf_commute)
      also have "... = (vT  -FT) * -F"
        using assms(1) equivalence_comp_left_complement by simp
      finally have "F  vT * -F  F  (vT  -F) * -F"
        using assms(1) by auto
      hence 11: "F  vT * -F = F  (-F  vT) * -F"
        by (metis inf.antisym_conv inf.sup_monoid.add_commute comp_left_subdist_inf inf.boundedE inf.sup_right_isotone)
      hence "FT  -FT * vTT = FT  -FT * (-FT  vTT)"
        by (metis (full_types) assms(1) conv_complement conv_dist_comp conv_dist_inf)
      hence 12: "F  -F * v = F  -F * (-F  v)"
        using assms(1) by (simp add: abel_semigroup.commute inf.abel_semigroup_axioms)
      have "(F  vT * -F) * (F  -F * v) = (F  (-F  vT) * -F) * (F  -F * (-F  v))"
        using 11 12 by auto
      also have "...  (-F  vT) * -F * -F * (-F  v)"
        by (metis comp_associative comp_isotone inf.cobounded2)
      finally show ?thesis
        using comp_inf.mult_left_isotone by blast
    qed
    also have "... = ((-F  vT) * -F * -F * (-F  v)  (F  v)T * (F  v)T * (F  v))  ((-F  vT) * -F * -F * (-F  v)  (F  v))"
      by (metis comp_associative inf_sup_distrib1 star.circ_loop_fixpoint)
    also have "... = ((-F  vT) * -F * -F * (-F  v)  (F  vT) * (F  v)T * (F  v))  ((-F  vT) * -F * -F * (-F  v)  (F  v))"
      using assms(1) conv_dist_inf by auto
    also have "... = bot  ((-F  vT) * -F * -F * (-F  v)  (F  v))"
    proof -
      have "(-F  vT) * -F * -F * (-F  v)  (F  vT) * (F  v)T * (F  v)  bot"
        using assms(1, 2) forests_bot_2 by (simp add: comp_associative)
      thus ?thesis
        using le_bot by blast
    qed
    also have "... = (-F  vT) * -F * -F * (-F  v)  (1  (F  v) * (F  v))"
      by (simp add: star.circ_plus_same star_left_unfold_equal)
    also have "... = ((-F  vT) * -F * -F * (-F  v)  1)  ((-F  vT) * -F * -F * (-F  v)  (F  v) * (F  v))"
      by (simp add: comp_inf.semiring.distrib_left)
    also have "...  1  ((-F  vT) * -F * -F * (-F  v)  (F  v) * (F  v))"
      using sup_left_isotone by auto
    also have "...  1  bot"
      using assms(1, 2) forests_bot_3 comp_inf.semiring.add_left_mono by simp
    finally show ?thesis
      by simp
  qed
  have 2: "?i * top * ?iT  1"
  proof -
    have "?i * top * ?iT = (v  -F * e * top  top * eT * F) * top * (vT  (-F * e * top)T  (top * eT * F)T)"
      by (simp add: conv_dist_inf)
    also have "... = (v  -F * e * top  top * eT * F) * top * (vT  topT * eT * -FT  FT * eTT * topT)"
      by (simp add: conv_complement conv_dist_comp mult_assoc)
    also have "... = (v  -F * e * top  top * eT * F) * top * (vT  top * eT * -F  F * e * top)"
      by (simp add: assms(1))
    also have "... = -F * e * top  (v  top * eT * F) * top * (vT  top * eT * -F  F * e * top)"
      by (smt inf.left_commute inf.sup_monoid.add_assoc vector_export_comp)
    also have "... = -F * e * top  (v  top * eT * F) * top * (vT  F * e * top)  top * eT * -F"
      by (smt comp_inf_covector inf.sup_monoid.add_assoc inf.sup_monoid.add_commute mult_assoc)
    also have "... = -F * e * top  (v  top * eT * F) * top * top * (vT  F * e * top)  top * eT * -F"
      by (simp add: mult_assoc)
    also have "... = -F * e * top  v * ((top * eT * F)T  top) * top * (vT  F * e * top)  top * eT * -F"
      by (simp add: comp_inf_vector_1 mult.semigroup_axioms semigroup.assoc)
    also have "... = -F * e * top  v * ((top * eT * F)T  top) * (top  (F * e * top)T) * vT  top * eT * -F"
      by (smt comp_inf_vector covector_comp_inf vector_conv_covector vector_mult_closed vector_top_closed)
    also have "... = -F * e * top  v * (top * eT * F)T * (F * e * top)T * vT  top * eT * -F"
      by simp
    also have "... = -F * e * top  v * FT * eTT * topT * topT * eT * FT * vT  top * eT * -F"
      by (metis comp_associative conv_dist_comp)
    also have "... = -F * e * top  v * F * e * top * top * eT * F * vT  top * eT * -F"
      using assms(1) by auto
    also have "... = -F * e * top  v * F * e * top  top * eT * F * vT  top * eT * -F"
      by (smt comp_associative comp_inf_covector inf.sup_monoid.add_assoc inf_top.left_neutral vector_top_closed)
    also have "... = (-F  v * F) * e * top  top * eT * F * vT  top * eT * -F"
      using injective_comp_right_dist_inf assms(3) mult.semigroup_axioms semigroup.assoc by fastforce
    also have "... = (-F  v * F) * e * top  top * eT * (F * vT  -F)"
      using injective_comp_right_dist_inf assms(3) conv_dist_comp inf.sup_monoid.add_assoc mult.semigroup_axioms univalent_comp_left_dist_inf semigroup.assoc by fastforce
    also have "... = (-F  v * F) * e * top * top * eT * (F * vT  -F)"
      by (metis inf_top_right vector_export_comp vector_top_closed)
    also have "... = (-F  v * F) * e * top * eT * (F * vT  -F)"
      by (simp add: comp_associative)
    also have "...  (-F  v * F) * (F * vT  -F)"
      by (smt assms(3) conv_dist_comp mult.semigroup_axioms mult_left_isotone shunt_bijective symmetric_top_closed top_right_mult_increasing semigroup.assoc)
    also have "... = (-F  v * F) * ((v * F)T  -F)"
      by (simp add: assms(1) conv_dist_comp)
    also have "... = (-F  v * F) * (-F  v * F)T"
      using assms(1) conv_complement conv_dist_inf by (simp add: inf.sup_monoid.add_commute)
    also have "...  (-F  v) * (F  v) * (F  v)T * (-F  v)T"
    proof -
      let ?Fv = "F  v"
      have "-F  v * F  -F  v * (F  v)T * (F  v)"
        using assms(5) inf.sup_right_isotone mult_right_isotone comp_associative by auto
      also have "...  -F  v * (F  v)"
      proof -
        have "v * vT  1"
          by (simp add: assms(2))
        hence "v * vT * F  F"
          using assms(1) dual_order.trans mult_left_isotone by blast
        hence "v * vT * FT * F  F"
          by (metis assms(1) mult_1_right preorder_idempotent star.circ_sup_one_right_unfold star.circ_transitive_equal star_one star_simulation_right_equal mult_assoc)
        hence "v * (F  v)T * FT * F  F"
          by (meson conv_isotone dual_order.trans inf.cobounded2 inf.sup_monoid.add_commute mult_left_isotone mult_right_isotone)
        hence "v * (F  v)T * (F  v)T * (F  v)  F"
          by (meson conv_isotone dual_order.trans inf.cobounded2 inf.sup_monoid.add_commute mult_left_isotone mult_right_isotone comp_isotone conv_dist_inf inf.cobounded1 star_isotone)
        hence "-F  v * (F  v)T * (F  v)T * (F  v)  bot"
          using order.eq_iff p_antitone pseudo_complement by auto
        hence "(-F  v * (F  v)T * (F  v)T * (F  v))  v * (v  F)  v * (v  F)"
          using bot_least le_bot by fastforce
        hence "(-F  v * (v  F))  (v * (F  v)T * (F  v)T * (F  v)  v * (v  F))  v * (v  F)"
          by (simp add: sup_inf_distrib2)
        hence "(-F  v * (v  F))  v * ((F  v)T * (F  v)T  1) * (v  F)  v * (v  F)"
          by (simp add: inf.sup_monoid.add_commute mult.semigroup_axioms mult_left_dist_sup mult_right_dist_sup semigroup.assoc)
        hence "(-F  v * (v  F))  v * (F  v)T * (v  F)  v * (v  F)"
          by (simp add: star_left_unfold_equal sup_commute)
        hence "-F  v * (F  v)T * (v  F)  v * (v  F)"
          using comp_inf.mult_right_sub_dist_sup_left inf.order_lesseq_imp by blast
        thus ?thesis
          by (simp add: inf.sup_monoid.add_commute)
      qed
      also have "...  (v  -F * (F  v)T) * (F  v)"
        by (metis dedekind_2 conv_star_commute inf.sup_monoid.add_commute)
      also have "...  (v  -F * FT) * (F  v)"
        using conv_isotone inf.sup_right_isotone mult_left_isotone mult_right_isotone star_isotone by auto
      also have "... = (v  -F * F) * (F  v)"
        by (metis assms(1) equivalence_comp_right_complement mult_left_one star_one star_simulation_right_equal)
      also have "... = (-F  v) * (F  v)"
        using assms(1) equivalence_comp_right_complement inf.sup_monoid.add_commute by auto
      finally have "-F  v * F  (-F  v) * (F  v)"
        by simp
      hence "(-F  v * F) * (-F  v * F)T  (-F  v) * (F  v) * ((-F  v) * (F  v))T"
        by (simp add: comp_isotone conv_isotone)
      also have "... = (-F  v) * (F  v) * (F  v)T * (-F  v)T"
        by (simp add: comp_associative conv_dist_comp conv_star_commute)
      finally show ?thesis
        by simp
    qed
    also have "...  (-F  v) * ((F  v)  (F  vT)) * (-F  v)T"
    proof -
      have "(F  v) * (F  v)T  F * FT"
        using fc_isotone by auto
      also have "...  F * F"
        by (metis assms(1) preorder_idempotent star.circ_sup_one_left_unfold star.circ_transitive_equal star_right_induct_mult)
      finally have 21: "(F  v) * (F  v)T  F"
        using assms(1) dual_order.trans by blast
      have "(F  v) * (F  v)T  v * vT"
        by (simp add: fc_isotone)
      hence "(F  v) * (F  v)T  F  v * vT"
        using 21 by simp
      also have "... = F  (v  vT)"
        by (simp add: assms(2) cancel_separate_eq)
      finally show ?thesis
        by (metis assms(4, 6) comp_associative comp_inf.semiring.distrib_left comp_isotone inf_pp_semi_commute mult_left_isotone regular_closed_inf)
    qed
    also have "...  (-F  v) * (F  vT) * (-F  v)T  (-F  v) * (F  v) * (-F  v)T"
      by (simp add: mult_left_dist_sup mult_right_dist_sup)
    also have "...  (-F  v) * (-F  v)T  (-F  v) * (-F  v)T"
    proof -
      have "(-F  v) * (F  vT)  (-F  v) * ((F  v)T * (F  v)  vT)"
        by (simp add: assms(5) inf.coboundedI1 mult_right_isotone)
      also have "... = (-F  v) * ((F  v)T * (F  v)T * (F  v)  vT)  (-F  v) * ((F  v)  vT)"
        by (metis comp_associative comp_inf.mult_right_dist_sup mult_left_dist_sup star.circ_loop_fixpoint)
      also have "...  (-F  v) * (F  v)T * top  (-F  v) * ((F  v)  vT)"
        by (simp add: comp_associative comp_isotone inf.coboundedI2 inf.sup_monoid.add_commute le_supI1)
      also have "...  (-F  v) * (F  v)T * top  (-F  v) * (v  vT)"
        by (smt comp_inf.mult_right_isotone comp_inf.semiring.add_mono order.eq_iff inf.cobounded2 inf.sup_monoid.add_commute mult_right_isotone star_isotone)
      also have "...  bot  (-F  v) * (v  vT)"
        by (metis assms(1, 2) forests_bot_1 comp_associative comp_inf.semiring.add_right_mono mult_semi_associative vector_bot_closed)
      also have "...  -F  v"
        by (simp add: assms(2) acyclic_star_inf_conv)
      finally have 22: "(-F  v) * (F  vT)  -F  v"
        by simp
      have "((-F  v) * (F  vT))T = (F  v) * (-F  v)T"
        by (simp add: assms(1) conv_dist_inf conv_star_commute conv_dist_comp)
      hence "(F  v) * (-F  v)T  (-F  v)T"
        using 22 conv_isotone by fastforce
      thus ?thesis
        using 22 by (metis assms(4, 6) comp_associative comp_inf.pp_comp_semi_commute comp_inf.semiring.add_mono comp_isotone inf_pp_commute mult_left_isotone)
    qed
    also have "... = (-F  v) * (-F  v)T"
      by simp
    also have "...  v * vT"
      by (simp add: comp_isotone conv_isotone)
    also have "...  1"
      by (simp add: assms(2))
    thus ?thesis
      using calculation dual_order.trans by blast
  qed
  have 3: "top * ?i * top = top"
  proof -
    have 31: "regular (eT * -F * v * F * e)"
      using assms(3, 4, 6) arc_regular regular_mult_closed by auto
    have 32: "bijective ((top * eT)T)"
      using assms(3) by (simp add: conv_dist_comp)
    have "top * ?i * top = top * (v  -F * e * top) * ((top * eT * F)T  top)"
      by (simp add: comp_associative comp_inf_vector_1)
    also have "... = (top  (-F * e * top)T) * v * ((top * eT * F)T  top)"
      using comp_inf_vector conv_dist_comp by auto
    also have "... = (-F * e * top)T * v * (top * eT * F)T"
      by simp
    also have "... = topT * eT * -FT * v * FT * eTT * topT"
      by (simp add: comp_associative conv_complement conv_dist_comp)
    finally have 33: "top * ?i * top = top * eT * -F * v * F * e * top"
      by (simp add: assms(1))
    have "top * ?i * top  bot"
    proof (rule ccontr)
      assume "¬ top * (v  - F * e * top  top * eT * F) * top  bot"
      hence "top * eT * -F * v * F * e * top = bot"
        using 33 by auto
      hence "eT * -F * v * F * e = bot"
        using 31 tarski comp_associative le_bot by fastforce
      hence "top * (-F * v * F * e)T  -(eT)"
        by (metis comp_associative conv_complement_sub_leq conv_involutive p_bot schroeder_5_p)
      hence "top * eT * FT * vT * -FT  -(eT)"
        by (simp add: comp_associative conv_complement conv_dist_comp)
      hence "v * F * e * top * eT  F"
        by (metis assms(1, 4) comp_associative conv_dist_comp schroeder_3_p symmetric_top_closed)
      hence "v * F * e * top * top * eT  F"
        by (simp add: comp_associative)
      hence "v * F * e * top  F * (top * eT)T"
        using 32 by (metis shunt_bijective comp_associative conv_involutive)
      hence "v * F * e * top  F * e * top"
        using comp_associative conv_dist_comp by auto
      hence "v * F * e * top  F * e * top"
        using comp_associative star_left_induct_mult_iff by auto
      hence "eT * F * e * top  F * e * top"
        by (meson assms(9) mult_left_isotone order_trans)
      hence "eT * F * e * top * (e * top)T  F"
        using 32 shunt_bijective assms(3) mult_assoc by auto
      hence 34: "eT * F * e * top * top * eT  F"
        by (metis conv_dist_comp mult.semigroup_axioms symmetric_top_closed semigroup.assoc)
      hence "eT  F"
      proof -
        have "eT  eT * e * eT"
          by (metis conv_involutive ex231c)
        also have "...  eT * F * e * eT"
          using assms(1) comp_associative mult_left_isotone mult_right_isotone by fastforce
        also have "...  eT * F * e * top * top * eT"
          by (simp add: mult_left_isotone top_right_mult_increasing vector_mult_closed)
        finally show ?thesis
          using 34 by simp
      qed
      hence 35: "e  F"
        using assms(1) conv_order by fastforce
      have "top * (F * e)T  - e"
        using assms(8) comp_associative schroeder_4_p by auto
      hence "top * eT * F  - e"
        by (simp add: assms(1) comp_associative conv_dist_comp)
      hence "(top * eT)T * e  - F"
        using schroeder_3_p by auto
      hence "e * top * e  - F"
        by (simp add: conv_dist_comp)
      hence "e  - F"
        by (simp add: assms(3) arc_top_arc)
      hence "e  F  - F"
        using 35 inf.boundedI by blast
      hence "e = bot"
        using bot_unique by auto
      thus "False"
        using assms(10) by auto
    qed
    thus ?thesis
      by (metis assms(3, 4, 6) arc_regular regular_closed_inf regular_closed_top regular_conv_closed regular_mult_closed semiring.mult_not_zero tarski)
  qed
  have "bijective (?i * top)  bijective (?iT * top)"
    using 1 2 3 arc_expanded by blast
  thus ?thesis
    by blast
qed

subsubsection ‹Comparison of edge weights›

text ‹
In this section we compare the weight of the selected_edge› with other edges of interest.
Theorems 8, 9, 10 and 11 are supporting lemmas.
For example, Theorem 8 is used to show that the selected_edge› has its source inside and its target outside the component it is chosen for.
›

text ‹Theorem 8›

lemma e_leq_c_c_complement_transpose_general:
  assumes "e = minarc (c * -(c)T  g)"
    and "regular c"
  shows "e  c * -(c)T"
proof -
  have "e  -- (c * - cT  g)"
    using assms(1) minarc_below order_trans by blast
  also have "...  -- (c * - cT)"
    using order_lesseq_imp pp_isotone_inf by blast
  also have "... = c * - cT"
    using assms(2) regular_mult_closed by auto
  finally show ?thesis
    by simp
qed

text ‹Theorem 9›

lemma x_leq_c_transpose_general:
  assumes "forest h"
    and "vector c"
    and "xT * top  forest_components(h) * e * top"
    and "e  c * -cT"
    and "c = forest_components(h) * c"
  shows "x  cT"
proof -
  let ?H = "forest_components h"
  have "x  top * x"
    using top_left_mult_increasing by blast
  also have "...  (?H * e * top)T"
    using assms(3) conv_dist_comp conv_order by force
  also have "... = top * eT * ?H"
    using assms(1) comp_associative conv_dist_comp forest_components_equivalence by auto
  also have "...  top * (c * - cT)T * ?H"
    by (simp add: assms(4) conv_isotone mult_left_isotone mult_right_isotone)
  also have "... = top * (- c * cT) * ?H"
    by (simp add: conv_complement conv_dist_comp)
  also have "...  top * cT * ?H"
    by (metis mult_left_isotone top.extremum mult_assoc)
  also have "... = cT * ?H"
    using assms(1, 2) component_is_vector vector_conv_covector by auto
  also have "... = cT"
    by (metis assms(1, 5) fch_equivalence conv_dist_comp)
  finally show ?thesis
    by simp
qed

text ‹Theorem 10›

lemma x_leq_c_complement_general:
  assumes "vector c"
    and "c * cT  forest_components h"
    and "x  cT"
    and "x  -forest_components h"
  shows "x  -c"
proof -
  let ?H = "forest_components h"
  have "x  - ?H  cT"
    using assms(3, 4) by auto
  also have "...  - c"
  proof -
    have "c  cT  ?H"
      using assms(1, 2) vector_covector by auto
    hence "-?H  c  cT  bot"
      using inf.sup_monoid.add_assoc p_antitone pseudo_complement by fastforce
    thus ?thesis
      using le_bot p_shunting_swap pseudo_complement by blast
  qed
  finally show ?thesis
    by simp
qed

text ‹Theorem 11›

lemma sum_e_below_sum_x_when_outgoing_same_component_general:
  assumes "e = minarc (c * -(c)T  g)"
    and "regular c"
    and "forest h"
    and "vector c"
    and "xT * top  (forest_components h) * e * top"
    and "c = (forest_components h) * c"
    and "c * cT  forest_components h"
    and "x  - forest_components h  -- g"
    and "symmetric g"
    and "arc x"
    and "c  bot"
  shows "sum (e  g)  sum (x  g)"
proof -
  let ?H = "forest_components h"
  have 1:"e  c * - cT"
    using assms(1, 2) e_leq_c_c_complement_transpose_general by auto
  have 2: "x  cT"
    using 1 assms(3, 4, 5, 6) x_leq_c_transpose_general by auto
  hence "x  -c"
    using assms(4, 7, 8) x_leq_c_complement_general inf.boundedE by blast
  hence "x  - c  cT"
    using 2 by simp
  hence "x  - c * cT"
    using assms(4) by (simp add: vector_complement_closed vector_covector)
  hence "xT  cTT * - cT"
    by (metis conv_complement conv_dist_comp conv_isotone)
  hence 3: "xT  c * - cT"
    by simp
  hence "x  -- g"
    using assms(8) by auto
  hence "xT  -- g"
    using assms(9) conv_complement conv_isotone by fastforce
  hence "xT  c * - cT  -- g  bot"
    using 3 by (metis assms(10, 11) comp_inf.semiring.mult_not_zero conv_dist_comp
          conv_involutive inf.orderE mult_right_zero top.extremum)
  hence "xT  c * - cT  g  bot"
    using inf.sup_monoid.add_commute pp_inf_bot_iff by auto
  hence "sum (minarc (c * - cT  g)  (c * - cT  g))  sum (xT  c * - cT  g)"
    using assms(10) minarc_min inf.sup_monoid.add_assoc by auto
  hence "sum (e  c * - cT  g)  sum (xT  c * - cT  g)"
    using assms(1) inf.sup_monoid.add_assoc by auto
  hence "sum (e  g)  sum (xT  g)"
    using 1 3 by (metis inf.orderE)
  hence "sum (e  g)  sum (x  g)"
    using assms(9) sum_symmetric by auto
  thus ?thesis
    by simp
qed

lemma sum_e_below_sum_x_when_outgoing_same_component:
  assumes "symmetric g"
    and "vector j"
    and "forest h"
    and "x  - forest_components h  -- g"
    and "xT * top  forest_components h * selected_edge h j g * top"
    and "j  bot"
    and "arc x"
  shows "sum (selected_edge h j g  g)  sum (x  g)"
proof -
  let ?e = "selected_edge h j g"
  let ?c = "choose_component (forest_components h) j"
  let ?H = "forest_components h"
  show ?thesis
  proof (rule sum_e_below_sum_x_when_outgoing_same_component_general)
  next
    show "?e = minarc (?c * - ?cT  g)"
      by simp
  next
    show "regular ?c"
      using component_is_regular by auto
  next
    show "forest h"
      by (simp add: assms(3))
  next
    show "vector ?c"
      by (simp add: assms(2, 6) component_is_vector)
  next
    show "xT * top  ?H * ?e * top"
      by (simp add: assms(5))
  next
    show "?c = ?H * ?c"
      using component_single by auto
  next
    show "?c * ?cT  ?H"
      by (simp add: component_is_connected)
  next
    show "x  -?H  -- g"
      using assms(4) by auto
  next
    show "symmetric g"
      by (simp add: assms(1))
  next
    show "arc x"
      by (simp add: assms(7))
  next
    show "?c  bot"
      using assms(2, 5 , 6, 7) inf_bot_left le_bot minarc_bot mult_left_zero mult_right_zero by fastforce
  qed
qed

text ‹
If there is a path in the big_forest› from an edge between components, $a$, to the selected_edge›, $e$, then the weight of $e$ is no greater than the weight of $a$.
This is because either,
\begin{itemize}
\item the edges $a$ and $e$ are adjacent the same component so that we can use sum_e_below_sum_x_when_outgoing_same_component›, or
\item there is at least one edge between $a$ and $e$, namely $x$, the edge incoming to the component that $e$ is outgoing from.
      The path from $a$ to $e$ is split on $x$ using big_forest_path_split_disj›.
      We show that the weight of $e$ is no greater than the weight of $x$ by making use of lemma sum_e_below_sum_x_when_outgoing_same_component›.
      We define $x$ in a way that we can show that the weight of $x$ is no greater than the weight of $a$ using the invariant.
      Then, it follows that the weight of $e$ is no greater than the weight of $a$ owing to transitivity.
\end{itemize}
›

lemma a_to_e_in_bigforest:
  assumes "symmetric g"
    and "f  --g"
    and "vector j"
    and "forest h"
    and "big_forest (forest_components h) d"
    and "f  fT = h  hT  d  dT"
    and "( a b . bf_between_arcs a b (forest_components h) d  a  -(forest_components h)  -- g  b  d  sum(b  g)  sum(a  g))"
    and "regular d"
    and "j  bot"
    and "b = selected_edge h j g"
    and "arc a"
    and "bf_between_arcs a b (forest_components h) (d  selected_edge h j g)"
    and "a  - forest_components h  -- g"
    and "regular h"
  shows "sum (b  g)  sum (a  g)"
proof -
  let ?p = "path f h j g"
  let ?e = "selected_edge h j g"
  let ?F = "forest_components f"
  let ?H = "forest_components h"
  have "sum (b  g)  sum (a  g)"
  proof (cases "aT * top  ?H * ?e * top")
    case True
    show "aT * top  ?H * ?e * top  sum (b  g)  sum (a  g)"
    proof-
      have "sum (?e  g)  sum (a  g)"
      proof (rule sum_e_below_sum_x_when_outgoing_same_component)
        show "symmetric g"
          using assms(1) by auto
      next
        show "vector j"
          using assms(3) by blast
      next
        show "forest h"
          by (simp add: assms(4))
      next
        show "a  - ?H  -- g"
          using assms(13) by auto
      next
        show "aT * top  ?H * ?e * top"
          using True by auto
      next
        show "j  bot"
          by (simp add: assms(9))
      next
        show "arc a"
          by (simp add: assms(11))
      qed
      thus ?thesis
        using assms(10) by auto
    qed
  next
    case False
    show "¬ aT * top  ?H * ?e * top  sum (b  g)  sum (a  g)"
    proof -
      let ?d' = "d  ?e"
      let ?x = "d  top * ?eT * ?H  (?H * dT) * ?H * aT * top"
      have 61: "arc (?x)"
      proof (rule shows_arc_x)
        show "big_forest ?H d"
          by (simp add: assms(5))
      next
        show "bf_between_arcs a ?e ?H d"
        proof -
          have 611: "bf_between_arcs a b ?H (d  b)"
            using assms(10, 12) by auto
          have 616: "regular h"
            using assms(14) by auto
          have "regular a"
            using 611 bf_between_arcs_def arc_regular by fastforce
          thus ?thesis
            using 616 by (smt big_forest_path_split_disj assms(4, 8, 10, 12) bf_between_arcs_def fch_equivalence minarc_regular regular_closed_star regular_conv_closed regular_mult_closed)
        qed
      next
        show "(?H * d)+  - ?H"
          using assms(5) big_forest_def by blast
      next
        show "¬ aT * top  ?H * ?e * top"
          by (simp add: False)
      next
        show "regular a"
          using assms(12) bf_between_arcs_def arc_regular by auto
      next
        show "regular ?e"
          using minarc_regular by auto
      next
        show "regular ?H"
          using assms(14) pp_dist_star regular_conv_closed regular_mult_closed by auto
      next
        show "regular d"
          using assms(8) by auto
      qed
      have 62: "bijective (aT * top)"
        by (simp add: assms(11))
      have 63: "bijective (?x * top)"
        using 61 by simp
      have 64: "?x  (?H * dT) * ?H * aT * top"
        by simp
      hence "?x * top  (?H * dT) * ?H * aT * top"
        using mult_left_isotone inf_vector_comp by auto
      hence "aT * top  ((?H * dT) * ?H)T * ?x * top"
        using 62 63 64 by (smt bijective_reverse mult_assoc)
      also have "... = ?H * (d * ?H) * ?x * top"
        using conv_dist_comp conv_star_commute by auto
      also have "... = (?H * d) * ?H * ?x * top"
        by (simp add: star_slide)
      finally have "aT * top  (?H * d) * ?H * ?x * top"
        by simp
      hence 65: "bf_between_arcs a ?x ?H d"
        using 61 assms(12) bf_between_arcs_def by blast
      have 66: "?x  d"
        by (simp add: inf.sup_monoid.add_assoc)
      hence x_below_a: "sum (?x  g)  sum (a  g)"
        using 65 bf_between_arcs_def assms(7, 13) by blast
      have "sum (?e  g)  sum (?x  g)"
      proof (rule sum_e_below_sum_x_when_outgoing_same_component)
        show "symmetric g"
          using assms(1) by auto
      next
        show "vector j"
          using assms(3) by blast
      next
        show "forest h"
          by (simp add: assms(4))
      next
        show "?x  - ?H  -- g"
        proof -
          have 67: "?x  - ?H"
            using 66 assms(5) big_forest_def order_lesseq_imp by blast
          have "?x  d"
            by (simp add: conv_isotone inf.sup_monoid.add_assoc)
          also have "...  f  fT"
          proof -
            have "h  hT  d  dT = f  fT"
              by (simp add: assms(6))
            thus ?thesis
              by (metis (no_types) le_supE sup.absorb_iff2 sup.idem)
          qed
          also have "...  -- g"
            using assms(1, 2) conv_complement conv_isotone by fastforce
          finally have "?x  -- g"
            by simp
          thus ?thesis
            by (simp add: 67)
        qed
      next
        show "?xT * top  ?H * ?e * top"
        proof -
          have "?x  top * ?eT * ?H"
            using inf.coboundedI1 by auto
          hence "?xT  ?H * ?e * top"
            using conv_dist_comp conv_dist_inf conv_star_commute inf.orderI inf.sup_monoid.add_assoc inf.sup_monoid.add_commute mult_assoc by auto
          hence "?xT * top  ?H * ?e * top * top"
            by (simp add: mult_left_isotone)
          thus ?thesis
            by (simp add: mult_assoc)
        qed
      next
        show "j  bot"
          by (simp add: assms(9))
      next
        show "arc (?x)"
          using 61 by blast
      qed
      hence "sum (?e  g)  sum (a  g)"
        using x_below_a order.trans by blast
      thus ?thesis
        by (simp add: assms(10))
    qed
  qed
  thus ?thesis
    by simp
qed

subsubsection ‹Maintenance of algorithm invariants›

text ‹
In this section, most of the work is done to maintain the invariants of the inner and outer loops of the algorithm.
In particular, we use exists_a_w› to maintain that $f$ can be extended to a minimum spanning forest.
›

lemma boruvka_exchange_spanning_inv:
  assumes "forest v"
    and "v * eT = eT"
    and "i  v  top * eT * wT"
    and "arc i"
    and "arc e"
    and "v  --g"
    and "w  --g"
    and "e  --g"
    and "components g  forest_components v"
  shows "i  (v  -i)T * eT * top"
proof -
  have 1: "(v  -i  -iT) * (vT  -i  -iT)  1"
    using assms(1) comp_isotone order.trans inf.cobounded1 by blast
  have 2: "bijective (i * top)  bijective (eT * top)"
    using assms(4, 5) mult_assoc by auto
  have "i  v * (top * eT * wT)T"
    using assms(3) covector_mult_closed covector_restrict_comp_conv order_lesseq_imp vector_top_closed by blast
  also have "...  v * wTT * eTT * topT"
    by (simp add: comp_associative conv_dist_comp)
  also have "...  v * w * e * top"
    by (simp add: conv_star_commute)
  also have "... = v * w * e * eT * e * top"
    using assms(5) arc_eq_1 by (simp add: comp_associative)
  also have "...  v * w * e * eT * top"
    by (simp add: comp_associative mult_right_isotone)
  also have "...  (--g) * (--g) * (--g) * eT * top"
    using assms(6, 7, 8) by (simp add: comp_isotone star_isotone)
  also have "...  (--g) * eT * top"
    by (metis comp_isotone mult_left_isotone star.circ_increasing star.circ_transitive_equal)
  also have "...  vT * v * eT * top"
    by (simp add: assms(9) mult_left_isotone)
  also have "...  vT * eT * top"
    by (simp add: assms(2) comp_associative)
  finally have "i  vT * eT * top"