Theory Kleene_Relation_Algebras

(* Title:      Kleene Relation Algebras
   Author:     Walter Guttmann
   Maintainer: Walter Guttmann <walter.guttmann at canterbury.ac.nz>
*)

section ‹Kleene Relation Algebras›

text ‹
This theory combines Kleene algebras with Stone relation algebras.
Relation algebras with transitive closure have been studied by \<^cite>‹"Ng1984"›.
The weakening to Stone relation algebras allows us to talk about reachability in weighted graphs, for example.

Many results in this theory are used in the correctness proof of Prim's minimum spanning tree algorithm.
In particular, they are concerned with the exchange property, preservation of parts of the invariant and with establishing parts of the postcondition.
›

theory Kleene_Relation_Algebras

imports Stone_Relation_Algebras.Relation_Algebras Kleene_Algebras

begin

text ‹
We first note that bounded distributive lattices can be expanded to Kleene algebras by reusing some of the operations.
›

sublocale bounded_distrib_lattice < comp_inf: bounded_kleene_algebra where star = "λx . top" and one = top and times = inf
  apply unfold_locales
  apply (simp add: inf.assoc)
  apply simp
  apply simp
  apply (simp add: le_infI2)
  apply (simp add: inf_sup_distrib2)
  apply simp
  apply simp
  apply simp
  apply simp
  apply simp
  apply (simp add: inf_sup_distrib1)
  apply simp
  apply simp
  by (simp add: inf_assoc)

text ‹
We add the Kleene star operation to each of bounded distributive allegories, pseudocomplemented distributive allegories and Stone relation algebras.
We start with single-object bounded distributive allegories.
›

class bounded_distrib_kleene_allegory = bounded_distrib_allegory + kleene_algebra
begin

subclass bounded_kleene_algebra ..

lemma conv_star_conv:
  "x⇧^⋆ ≤ x⇧^T⇧^⋆⇧^T"
proof -
  have "x⇧^T⇧^⋆ * x⇧^T ≤ x⇧^T⇧^⋆"
    by (simp add: star.right_plus_below_circ)
  hence 1: "x * x⇧^T⇧^⋆⇧^T ≤ x⇧^T⇧^⋆⇧^T"
    using conv_dist_comp conv_isotone by fastforce
  have "1 ≤ x⇧^T⇧^⋆⇧^T"
    by (simp add: reflexive_conv_closed star.circ_reflexive)
  hence "1 ⊔ x * x⇧^T⇧^⋆⇧^T ≤ x⇧^T⇧^⋆⇧^T"
    using 1 by simp
  thus ?thesis
    using star_left_induct by fastforce
qed

text ‹
It follows that star and converse commute.
›

lemma conv_star_commute:
  "x⇧^⋆⇧^T = x⇧^T⇧^⋆"
proof (rule order.antisym)
  show "x⇧^⋆⇧^T ≤ x⇧^T⇧^⋆"
    using conv_star_conv conv_isotone by fastforce
next
  show "x⇧^T⇧^⋆ ≤ x⇧^⋆⇧^T"
    by (metis conv_star_conv conv_involutive)
qed

lemma conv_plus_commute:
  "x⇧⁺⇧^T = x⇧^T⇧⁺"
  by (simp add: conv_dist_comp conv_star_commute star_plus)

text ‹Lemma ‹reflexive_inf_star› was contributed by Nicolas Robinson-O'Brien.›

lemma reflexive_inf_star:
  assumes "reflexive y"
    shows "y ⊓ x⇧^⋆ = 1 ⊔ (y ⊓ x⇧⁺)"
  by (simp add: assms star_left_unfold_equal sup.absorb2 sup_inf_distrib1)

text ‹
The following results are variants of a separation lemma of Kleene algebras.
›

lemma cancel_separate_2:
  assumes "x * y ≤ 1"
    shows "((w ⊓ x) ⊔ (z ⊓ y))⇧^⋆ = (z ⊓ y)⇧^⋆ * (w ⊓ x)⇧^⋆"
proof -
  have "(w ⊓ x) * (z ⊓ y) ≤ 1"
    by (meson assms comp_isotone order.trans inf.cobounded2)
  thus ?thesis
    using cancel_separate_1 sup_commute by simp
qed

lemma cancel_separate_3:
  assumes "x * y ≤ 1"
    shows "(w ⊓ x)⇧^⋆ * (z ⊓ y)⇧^⋆ = (w ⊓ x)⇧^⋆ ⊔ (z ⊓ y)⇧^⋆"
proof -
  have "(w ⊓ x) * (z ⊓ y) ≤ 1"
    by (meson assms comp_isotone order.trans inf.cobounded2)
  thus ?thesis
    by (simp add: cancel_separate_eq)
qed

lemma cancel_separate_4:
  assumes "z * y ≤ 1"
      and "w ≤ y ⊔ z"
      and "x ≤ y ⊔ z"
    shows "w⇧^⋆ * x⇧^⋆ = (w ⊓ y)⇧^⋆ * ((w ⊓ z)⇧^⋆ ⊔ (x ⊓ y)⇧^⋆) * (x ⊓ z)⇧^⋆"
proof -
  have "w⇧^⋆ * x⇧^⋆ = ((w ⊓ y) ⊔ (w ⊓ z))⇧^⋆ * ((x ⊓ y) ⊔ (x ⊓ z))⇧^⋆"
    by (metis assms(2,3) inf.orderE inf_sup_distrib1)
  also have "... = (w ⊓ y)⇧^⋆ * ((w ⊓ z)⇧^⋆ * (x ⊓ y)⇧^⋆) * (x ⊓ z)⇧^⋆"
    by (metis assms(1) cancel_separate_2 sup_commute mult_assoc)
  finally show ?thesis
    by (simp add: assms(1) cancel_separate_3)
qed

lemma cancel_separate_5:
  assumes "w * z⇧^T ≤ 1"
    shows "w ⊓ x * (y ⊓ z) ≤ y"
proof -
  have "w ⊓ x * (y ⊓ z) ≤ (x ⊓ w * (y ⊓ z)⇧^T) * (y ⊓ z)"
    by (metis dedekind_2 inf_commute)
  also have "... ≤ w * z⇧^T * (y ⊓ z)"
    by (simp add: conv_dist_inf inf.coboundedI2 mult_left_isotone mult_right_isotone)
  also have "... ≤ y ⊓ z"
    by (metis assms mult_1_left mult_left_isotone)
  finally show ?thesis
    by simp
qed

lemma cancel_separate_6:
  assumes "z * y ≤ 1"
      and "w ≤ y ⊔ z"
      and "x ≤ y ⊔ z"
      and "v * z⇧^T ≤ 1"
      and "v ⊓ y⇧^⋆ = bot"
    shows "v ⊓ w⇧^⋆ * x⇧^⋆ ≤ x ⊔ w"
proof -
  have "v ⊓ (w ⊓ y)⇧^⋆ * (x ⊓ y)⇧^⋆ ≤ v ⊓ y⇧^⋆ * (x ⊓ y)⇧^⋆"
    using comp_inf.mult_right_isotone mult_left_isotone star_isotone by simp
  also have "... ≤ v ⊓ y⇧^⋆"
    by (simp add: inf.coboundedI2 star.circ_increasing star.circ_mult_upper_bound star_right_induct_mult)
  finally have 1: "v ⊓ (w ⊓ y)⇧^⋆ * (x ⊓ y)⇧^⋆ = bot"
    using assms(5) le_bot by simp
  have "v ⊓ w⇧^⋆ * x⇧^⋆ = v ⊓ (w ⊓ y)⇧^⋆ * ((w ⊓ z)⇧^⋆ ⊔ (x ⊓ y)⇧^⋆) * (x ⊓ z)⇧^⋆"
    using assms(1-3) cancel_separate_4 by simp
  also have "... = (v ⊓ (w ⊓ y)⇧^⋆ * ((w ⊓ z)⇧^⋆ ⊔ (x ⊓ y)⇧^⋆) * (x ⊓ z)⇧^⋆ * (x ⊓ z)) ⊔ (v ⊓ (w ⊓ y)⇧^⋆ * ((w ⊓ z)⇧^⋆ ⊔ (x ⊓ y)⇧^⋆))"
    by (metis inf_sup_distrib1 star.circ_back_loop_fixpoint)
  also have "... ≤ x ⊔ (v ⊓ (w ⊓ y)⇧^⋆ * ((w ⊓ z)⇧^⋆ ⊔ (x ⊓ y)⇧^⋆))"
    using assms(4) cancel_separate_5 semiring.add_right_mono by simp
  also have "... = x ⊔ (v ⊓ (w ⊓ y)⇧^⋆ * (w ⊓ z)⇧^⋆)"
    using 1 by (simp add: inf_sup_distrib1 mult_left_dist_sup sup_monoid.add_assoc)
  also have "... = x ⊔ (v ⊓ (w ⊓ y)⇧^⋆ * (w ⊓ z)⇧^⋆ * (w ⊓ z)) ⊔ (v ⊓ (w ⊓ y)⇧^⋆)"
    by (metis comp_inf.semiring.distrib_left star.circ_back_loop_fixpoint sup_assoc)
  also have "... ≤ x ⊔ w ⊔ (v ⊓ (w ⊓ y)⇧^⋆)"
    using assms(4) cancel_separate_5 sup_left_isotone sup_right_isotone by simp
  also have "... ≤ x ⊔ w ⊔ (v ⊓ y⇧^⋆)"
    using comp_inf.mult_right_isotone star_isotone sup_right_isotone by simp
  finally show ?thesis
    using assms(5) le_bot by simp
qed

text ‹
We show several results about the interaction of vectors and the Kleene star.
›

lemma vector_star_1:
  assumes "vector x"
    shows "x⇧^T * (x * x⇧^T)⇧^⋆ ≤ x⇧^T"
proof -
  have "x⇧^T * (x * x⇧^T)⇧^⋆ = (x⇧^T * x)⇧^⋆ * x⇧^T"
    by (simp add: star_slide)
  also have "... ≤ top * x⇧^T"
    by (simp add: mult_left_isotone)
  also have "... = x⇧^T"
    using assms vector_conv_covector by auto
  finally show ?thesis
    .
qed

lemma vector_star_2:
  "vector x ⟹ x⇧^T * (x * x⇧^T)⇧^⋆ ≤ x⇧^T * bot⇧^⋆"
  by (simp add: star_absorb vector_star_1)

lemma vector_vector_star:
  "vector v ⟹ (v * v⇧^T)⇧^⋆ = 1 ⊔ v * v⇧^T"
  by (simp add: transitive_star vv_transitive)

lemma equivalence_star_closed:
  "equivalence x ⟹ equivalence (x⇧^⋆)"
  by (simp add: conv_star_commute star.circ_reflexive star.circ_transitive_equal)

lemma equivalence_plus_closed:
  "equivalence x ⟹ equivalence (x⇧⁺)"
  by (simp add: conv_star_commute star.circ_reflexive star.circ_sup_one_left_unfold star.circ_transitive_equal)

text ‹
The following equivalence relation characterises the component trees of a forest.
This is a special case of undirected reachability in a directed graph.
›

abbreviation "forest_components f ≡ f⇧^T⇧^⋆ * f⇧^⋆"

lemma forest_components_equivalence:
  "injective x ⟹ equivalence (forest_components x)"
  apply (intro conjI)
  apply (simp add: reflexive_mult_closed star.circ_reflexive)
  apply (metis cancel_separate_1 order.eq_iff star.circ_transitive_equal)
  by (simp add: conv_dist_comp conv_star_commute)

lemma forest_components_increasing:
  "x ≤ forest_components x"
  by (metis order.trans mult_left_isotone mult_left_one star.circ_increasing star.circ_reflexive)

lemma forest_components_isotone:
  "x ≤ y ⟹ forest_components x ≤ forest_components y"
  by (simp add: comp_isotone conv_isotone star_isotone)

lemma forest_components_idempotent:
  "injective x ⟹ forest_components (forest_components x) = forest_components x"
  by (metis forest_components_equivalence cancel_separate_1 star.circ_transitive_equal star_involutive)

lemma forest_components_star:
  "injective x ⟹ (forest_components x)⇧^⋆ = forest_components x"
  using forest_components_equivalence forest_components_idempotent star.circ_transitive_equal by simp

text ‹
The following lemma shows that the nodes reachable in the graph can be reached by only using edges between reachable nodes.
›

lemma reachable_restrict:
  assumes "vector r"
    shows "r⇧^T * g⇧^⋆ = r⇧^T * ((r⇧^T * g⇧^⋆)⇧^T * (r⇧^T * g⇧^⋆) ⊓ g)⇧^⋆"
proof -
  have 1: "r⇧^T ≤ r⇧^T * ((r⇧^T * g⇧^⋆)⇧^T * (r⇧^T * g⇧^⋆) ⊓ g)⇧^⋆"
    using mult_right_isotone mult_1_right star.circ_reflexive by fastforce
  have 2: "covector (r⇧^T * g⇧^⋆)"
    using assms covector_mult_closed vector_conv_covector by auto
  have "r⇧^T * ((r⇧^T * g⇧^⋆)⇧^T * (r⇧^T * g⇧^⋆) ⊓ g)⇧^⋆ * g ≤ r⇧^T * g⇧^⋆ * g"
    by (simp add: mult_left_isotone mult_right_isotone star_isotone)
  also have "... ≤ r⇧^T * g⇧^⋆"
    by (simp add: mult_assoc mult_right_isotone star.left_plus_below_circ star_plus)
  finally have "r⇧^T * ((r⇧^T * g⇧^⋆)⇧^T * (r⇧^T * g⇧^⋆) ⊓ g)⇧^⋆ * g = r⇧^T * ((r⇧^T * g⇧^⋆)⇧^T * (r⇧^T * g⇧^⋆) ⊓ g)⇧^⋆ * g ⊓ r⇧^T * g⇧^⋆"
    by (simp add: le_iff_inf)
  also have "... = r⇧^T * ((r⇧^T * g⇧^⋆)⇧^T * (r⇧^T * g⇧^⋆) ⊓ g)⇧^⋆ * (g ⊓ r⇧^T * g⇧^⋆)"
    using assms covector_comp_inf covector_mult_closed vector_conv_covector by auto
  also have "... = (r⇧^T * ((r⇧^T * g⇧^⋆)⇧^T * (r⇧^T * g⇧^⋆) ⊓ g)⇧^⋆ ⊓ r⇧^T * g⇧^⋆) * (g ⊓ r⇧^T * g⇧^⋆)"
    by (simp add: inf.absorb2 inf_commute mult_right_isotone star_isotone)
  also have "... = r⇧^T * ((r⇧^T * g⇧^⋆)⇧^T * (r⇧^T * g⇧^⋆) ⊓ g)⇧^⋆ * (g ⊓ r⇧^T * g⇧^⋆ ⊓ (r⇧^T * g⇧^⋆)⇧^T)"
    using 2 by (metis comp_inf_vector_1)
  also have "... = r⇧^T * ((r⇧^T * g⇧^⋆)⇧^T * (r⇧^T * g⇧^⋆) ⊓ g)⇧^⋆ * ((r⇧^T * g⇧^⋆)⇧^T ⊓ r⇧^T * g⇧^⋆ ⊓ g)"
    using inf_commute inf_assoc by simp
  also have "... = r⇧^T * ((r⇧^T * g⇧^⋆)⇧^T * (r⇧^T * g⇧^⋆) ⊓ g)⇧^⋆ * ((r⇧^T * g⇧^⋆)⇧^T * (r⇧^T * g⇧^⋆) ⊓ g)"
    using 2 by (metis covector_conv_vector inf_top.right_neutral vector_inf_comp)
  also have "... ≤ r⇧^T * ((r⇧^T * g⇧^⋆)⇧^T * (r⇧^T * g⇧^⋆) ⊓ g)⇧^⋆"
    by (simp add: mult_assoc mult_right_isotone star.left_plus_below_circ star_plus)
  finally have "r⇧^T * g⇧^⋆ ≤ r⇧^T * ((r⇧^T * g⇧^⋆)⇧^T * (r⇧^T * g⇧^⋆) ⊓ g)⇧^⋆"
    using 1 star_right_induct by auto
  thus ?thesis
    by (simp add: order.eq_iff mult_right_isotone star_isotone)
qed

lemma kruskal_acyclic_inv_1:
  assumes "injective f"
      and "e * forest_components f * e = bot"
    shows "(f ⊓ top * e * f⇧^T⇧^⋆)⇧^T * f⇧^⋆ * e = bot"
proof -
  let ?q = "top * e * f⇧^T⇧^⋆"
  let ?F = "forest_components f"
  have "(f ⊓ ?q)⇧^T * f⇧^⋆ * e = ?q⇧^T ⊓ f⇧^T * f⇧^⋆ * e"
    by (metis (mono_tags) comp_associative conv_dist_inf covector_conv_vector inf_vector_comp vector_top_closed)
  also have "... ≤ ?q⇧^T ⊓ ?F * e"
    using comp_inf.mult_right_isotone mult_left_isotone star.circ_increasing by simp
  also have "... = f⇧^⋆ * e⇧^T * top ⊓ ?F * e"
    by (simp add: conv_dist_comp conv_star_commute mult_assoc)
  also have "... ≤ ?F * e⇧^T * top ⊓ ?F * e"
    by (metis conv_dist_comp conv_star_commute conv_top inf.sup_left_isotone star.circ_right_top star_outer_increasing mult_assoc)
  also have "... = ?F * (e⇧^T * top ⊓ ?F * e)"
    by (metis assms(1) forest_components_equivalence equivalence_comp_dist_inf mult_assoc)
  also have "... = (?F ⊓ top * e) * ?F * e"
    by (simp add: comp_associative comp_inf_vector_1 conv_dist_comp inf_vector_comp)
  also have "... ≤ top * e * ?F * e"
    by (simp add: mult_left_isotone)
  also have "... = bot"
    using assms(2) mult_assoc by simp
  finally show ?thesis
    by (simp add: bot_unique)
qed

lemma kruskal_forest_components_inf_1:
  assumes "f ≤ w ⊔ w⇧^T"
      and "injective w"
      and "f ≤ forest_components g"
    shows "f * forest_components (forest_components g ⊓ w) ≤ forest_components (forest_components g ⊓ w)"
proof -
  let ?f = "forest_components g"
  let ?w = "forest_components (?f ⊓ w)"
  have "f * ?w = (f ⊓ (w ⊔ w⇧^T)) * ?w"
    by (simp add: assms(1) inf.absorb1)
  also have "... = (f ⊓ w) * ?w ⊔ (f ⊓ w⇧^T) * ?w"
    by (simp add: inf_sup_distrib1 semiring.distrib_right)
  also have "... ≤ (?f ⊓ w) * ?w ⊔ (f ⊓ w⇧^T) * ?w"
    using assms(3) inf.sup_left_isotone mult_left_isotone sup_left_isotone by simp
  also have "... ≤ (?f ⊓ w) * ?w ⊔ (?f ⊓ w⇧^T) * ?w"
    using assms(3) inf.sup_left_isotone mult_left_isotone sup_right_isotone by simp
  also have "... = (?f ⊓ w) * ?w ⊔ (?f ⊓ w)⇧^T * ?w"
    by (simp add: conv_dist_comp conv_dist_inf conv_star_commute)
  also have "... ≤ (?f ⊓ w) * ?w ⊔ ?w"
    by (metis star.circ_loop_fixpoint sup_ge1 sup_right_isotone)
  also have "... = ?w ⊔ (?f ⊓ w) * (?f ⊓ w)⇧^⋆ ⊔ (?f ⊓ w) * (?f ⊓ w)⇧^T⇧⁺ * (?f ⊓ w)⇧^⋆"
    by (metis comp_associative mult_left_dist_sup star.circ_loop_fixpoint sup_commute sup_assoc)
  also have "... ≤ ?w ⊔ (?f ⊓ w)⇧^⋆ ⊔ (?f ⊓ w) * (?f ⊓ w)⇧^T⇧⁺ * (?f ⊓ w)⇧^⋆"
    using star.left_plus_below_circ sup_left_isotone sup_right_isotone by auto
  also have "... = ?w ⊔ (?f ⊓ w) * (?f ⊓ w)⇧^T⇧⁺ * (?f ⊓ w)⇧^⋆"
    by (metis star.circ_loop_fixpoint sup.right_idem)
  also have "... ≤ ?w ⊔ w * w⇧^T * ?w"
    using comp_associative conv_dist_inf mult_isotone sup_right_isotone by simp
  also have "... = ?w"
    by (metis assms(2) coreflexive_comp_top_inf inf.cobounded2 sup.orderE)
  finally show ?thesis
    by simp
qed

lemma kruskal_forest_components_inf:
  assumes "f ≤ w ⊔ w⇧^T"
      and "injective w"
    shows "forest_components f ≤ forest_components (forest_components f ⊓ w)"
proof -
  let ?f = "forest_components f"
  let ?w = "forest_components (?f ⊓ w)"
  have 1: "1 ≤ ?w"
    by (simp add: reflexive_mult_closed star.circ_reflexive)
  have "f * ?w ≤ ?w"
    using assms forest_components_increasing kruskal_forest_components_inf_1 by simp
  hence 2: "f⇧^⋆ ≤ ?w"
    using 1 star_left_induct by fastforce
  have "f⇧^T * ?w ≤ ?w"
    apply (rule kruskal_forest_components_inf_1)
    apply (metis assms(1) conv_dist_sup conv_involutive conv_isotone sup_commute)
    apply (simp add: assms(2))
    by (metis le_supI2 star.circ_back_loop_fixpoint star.circ_increasing)
  thus "?f ≤ ?w"
    using 2 star_left_induct by simp
qed

end

text ‹
We next add the Kleene star to single-object pseudocomplemented distributive allegories.
›

class pd_kleene_allegory = pd_allegory + bounded_distrib_kleene_allegory
begin

text ‹
The following definitions and results concern acyclic graphs and forests.
›

abbreviation acyclic :: "'a ⇒ bool" where "acyclic x ≡ x⇧⁺ ≤ -1"

abbreviation forest :: "'a ⇒ bool" where "forest x ≡ injective x ∧ acyclic x"

lemma forest_bot:
  "forest bot"
  by simp

lemma acyclic_down_closed:
  "x ≤ y ⟹ acyclic y ⟹ acyclic x"
  using comp_isotone star_isotone by fastforce

lemma forest_down_closed:
  "x ≤ y ⟹ forest y ⟹ forest x"
  using conv_isotone mult_isotone star_isotone by fastforce

lemma acyclic_star_below_complement:
  "acyclic w ⟷ w⇧^T⇧^⋆ ≤ -w"
  by (simp add: conv_star_commute schroeder_4_p)

lemma acyclic_star_below_complement_1:
  "acyclic w ⟷ w⇧^⋆ ⊓ w⇧^T = bot"
  using pseudo_complement schroeder_5_p by force

lemma acyclic_star_inf_conv:
  assumes "acyclic w"
  shows "w⇧^⋆ ⊓ w⇧^T⇧^⋆ = 1"
proof -
  have "w⇧⁺ ⊓ w⇧^T⇧^⋆ ≤ (w ⊓ w⇧^T⇧^⋆) * w⇧^⋆"
    by (metis conv_star_commute dedekind_2 star.circ_transitive_equal)
  also have "... = bot"
    by (metis assms conv_star_commute p_antitone_iff pseudo_complement schroeder_4_p semiring.mult_not_zero star.circ_circ_mult star_involutive star_one)
  finally have "w⇧^⋆ ⊓ w⇧^T⇧^⋆ ≤ 1"
    by (metis order.eq_iff le_bot mult_left_zero star.circ_plus_one star.circ_zero star_left_unfold_equal sup_inf_distrib1)
  thus ?thesis
    by (simp add: order.antisym star.circ_reflexive)
qed

lemma acyclic_asymmetric:
  "acyclic w ⟹ asymmetric w"
  by (simp add: dual_order.trans pseudo_complement schroeder_5_p star.circ_increasing)

lemma forest_separate:
  assumes "forest x"
    shows "x⇧^⋆ * x⇧^T⇧^⋆ ⊓ x⇧^T * x ≤ 1"
proof -
  have "x⇧^⋆ * 1 ≤ -x⇧^T"
    using assms schroeder_5_p by force
  hence 1: "x⇧^⋆ ⊓ x⇧^T = bot"
    by (simp add: pseudo_complement)
  have "x⇧^⋆ ⊓ x⇧^T * x = (1 ⊔ x⇧^⋆ * x) ⊓ x⇧^T * x"
    using star.circ_right_unfold_1 by simp
  also have "... = (1 ⊓ x⇧^T * x) ⊔ (x⇧^⋆ * x ⊓ x⇧^T * x)"
    by (simp add: inf_sup_distrib2)
  also have "... ≤ 1 ⊔ (x⇧^⋆ * x ⊓ x⇧^T * x)"
    using sup_left_isotone by simp
  also have "... = 1 ⊔ (x⇧^⋆ ⊓ x⇧^T) * x"
    by (simp add: assms injective_comp_right_dist_inf)
  also have "... = 1"
    using 1 by simp
  finally have 2: "x⇧^⋆ ⊓ x⇧^T * x ≤ 1"
    .
  hence 3: "x⇧^T⇧^⋆ ⊓ x⇧^T * x ≤ 1"
    by (metis (mono_tags, lifting) conv_star_commute conv_dist_comp conv_dist_inf conv_involutive coreflexive_symmetric)
  have "x⇧^⋆ * x⇧^T⇧^⋆ ⊓ x⇧^T * x ≤ (x⇧^⋆ ⊔ x⇧^T⇧^⋆) ⊓ x⇧^T * x"
    using assms cancel_separate inf.sup_left_isotone by simp
  also have "... ≤ 1"
    using 2 3 by (simp add: inf_sup_distrib2)
  finally show ?thesis
    .
qed

text ‹
The following definition captures the components of undirected weighted graphs.
›

abbreviation "components g ≡ (--g)⇧^⋆"

lemma components_equivalence:
  "symmetric x ⟹ equivalence (components x)"
  by (simp add: conv_star_commute conv_complement star.circ_reflexive star.circ_transitive_equal)

lemma components_increasing:
  "x ≤ components x"
  using order_trans pp_increasing star.circ_increasing by blast

lemma components_isotone:
  "x ≤ y ⟹ components x ≤ components y"
  by (simp add: pp_isotone star_isotone)

lemma cut_reachable:
  assumes "v⇧^T = r⇧^T * t⇧^⋆"
      and "t ≤ g"
    shows "v * -v⇧^T ⊓ g ≤ (r⇧^T * g⇧^⋆)⇧^T * (r⇧^T * g⇧^⋆)"
proof -
  have "v * -v⇧^T ⊓ g ≤ v * top ⊓ g"
    using inf.sup_left_isotone mult_right_isotone top_greatest by blast
  also have "... = (r⇧^T * t⇧^⋆)⇧^T * top ⊓ g"
    by (metis assms(1) conv_involutive)
  also have "... ≤ (r⇧^T * g⇧^⋆)⇧^T * top ⊓ g"
    using assms(2) conv_isotone inf.sup_left_isotone mult_left_isotone mult_right_isotone star_isotone by auto
  also have "... ≤ (r⇧^T * g⇧^⋆)⇧^T * ((r⇧^T * g⇧^⋆) * g)"
    by (metis conv_involutive dedekind_1 inf_top.left_neutral)
  also have "... ≤ (r⇧^T * g⇧^⋆)⇧^T * (r⇧^T * g⇧^⋆)"
    by (simp add: mult_assoc mult_right_isotone star.left_plus_below_circ star_plus)
  finally show ?thesis
    .
qed

text ‹
The following lemma shows that the predecessors of visited nodes in the minimum spanning tree extending the current tree have all been visited.
›

lemma predecessors_reachable:
  assumes "vector r"
      and "injective r"
      and "v⇧^T = r⇧^T * t⇧^⋆"
      and "forest w"
      and "t ≤ w"
      and "w ≤ (r⇧^T * g⇧^⋆)⇧^T * (r⇧^T * g⇧^⋆) ⊓ g"
      and "r⇧^T * g⇧^⋆ ≤ r⇧^T * w⇧^⋆"
    shows "w * v ≤ v"
proof -
  have "w * r ≤ (r⇧^T * g⇧^⋆)⇧^T * (r⇧^T * g⇧^⋆) * r"
    using assms(6) mult_left_isotone by auto
  also have "... ≤ (r⇧^T * g⇧^⋆)⇧^T * top"
    by (simp add: mult_assoc mult_right_isotone)
  also have "... = (r⇧^T * g⇧^⋆)⇧^T"
    by (simp add: assms(1) comp_associative conv_dist_comp)
  also have "... ≤ (r⇧^T * w⇧^⋆)⇧^T"
    by (simp add: assms(7) conv_isotone)
  also have "... = w⇧^T⇧^⋆ * r"
    by (simp add: conv_dist_comp conv_star_commute)
  also have "... ≤ -w * r"
    using assms(4) by (simp add: mult_left_isotone acyclic_star_below_complement)
  also have "... ≤ -(w * r)"
    by (simp add: assms(2) comp_injective_below_complement)
  finally have 1: "w * r = bot"
    by (simp add: le_iff_inf)
  have "v = t⇧^T⇧^⋆ * r"
    by (metis assms(3) conv_dist_comp conv_involutive conv_star_commute)
  also have "... = t⇧^T * v ⊔ r"
    by (simp add: calculation star.circ_loop_fixpoint)
  also have "... ≤ w⇧^T * v ⊔ r"
    using assms(5) comp_isotone conv_isotone semiring.add_right_mono by auto
  finally have "w * v ≤ w * w⇧^T * v ⊔ w * r"
    by (simp add: comp_left_dist_sup mult_assoc mult_right_isotone)
  also have "... = w * w⇧^T * v"
    using 1 by simp
  also have "... ≤ v"
    using assms(4) by (simp add: star_left_induct_mult_iff star_sub_one)
  finally show ?thesis
    .
qed

subsection ‹Prim's Algorithm›

text ‹
The following results are used for proving the correctness of Prim's minimum spanning tree algorithm.
›

subsubsection ‹Preservation of Invariant›

text ‹
We first treat the preservation of the invariant.
The following lemma shows that the while-loop preserves that ‹v› represents the nodes of the constructed tree.
The remaining lemmas in this section show that ‹t› is a spanning tree.
The exchange property is treated in the following two sections.
›

lemma reachable_inv:
  assumes "vector v"
      and "e ≤ v * -v⇧^T"
      and "e * t = bot"
      and "v⇧^T = r⇧^T * t⇧^⋆"
    shows "(v ⊔ e⇧^T * top)⇧^T = r⇧^T * (t ⊔ e)⇧^⋆"
proof -
  have 1: "v⇧^T ≤ r⇧^T * (t ⊔ e)⇧^⋆"
    by (simp add: assms(4) mult_right_isotone star.circ_sub_dist)
  have 2: "(e⇧^T * top)⇧^T = top * e"
    by (simp add: conv_dist_comp)
  also have "... = top * (v * -v⇧^T ⊓ e)"
    by (simp add: assms(2) inf_absorb2)
  also have "... ≤ top * (v * top ⊓ e)"
    using inf.sup_left_isotone mult_right_isotone top_greatest by blast
  also have "... = top * v⇧^T * e"
    by (simp add: comp_inf_vector inf.sup_monoid.add_commute)
  also have "... = v⇧^T * e"
    using assms(1) vector_conv_covector by auto
  also have "... ≤ r⇧^T * (t ⊔ e)⇧^⋆ * e"
    using 1 by (simp add: mult_left_isotone)
  also have "... ≤ r⇧^T * (t ⊔ e)⇧^⋆ * (t ⊔ e)"
    by (simp add: mult_right_isotone)
  also have "... ≤ r⇧^T * (t ⊔ e)⇧^⋆"
    by (simp add: comp_associative mult_right_isotone star.right_plus_below_circ)
  finally have 3: "(v ⊔ e⇧^T * top)⇧^T ≤ r⇧^T * (t ⊔ e)⇧^⋆"
    using 1 by (simp add: conv_dist_sup)
  have "r⇧^T ≤ r⇧^T * t⇧^⋆"
    using sup.bounded_iff star.circ_back_loop_prefixpoint by blast
  also have "... ≤ (v ⊔ e⇧^T * top)⇧^T"
    by (metis assms(4) conv_isotone sup_ge1)
  finally have 4: "r⇧^T ≤ (v ⊔ e⇧^T * top)⇧^T"
    .
  have "(v ⊔ e⇧^T * top)⇧^T * (t ⊔ e) = (v ⊔ e⇧^T * top)⇧^T * t ⊔ (v ⊔ e⇧^T * top)⇧^T * e"
    by (simp add: mult_left_dist_sup)
  also have "... ≤ (v ⊔ e⇧^T * top)⇧^T * t ⊔ top * e"
    using comp_isotone semiring.add_left_mono by auto
  also have "... = v⇧^T * t ⊔ top * e * t ⊔ top * e"
    using 2 by (simp add: conv_dist_sup mult_right_dist_sup)
  also have "... = v⇧^T * t ⊔ top * e"
    by (simp add: assms(3) comp_associative)
  also have "... ≤ r⇧^T * t⇧^⋆ ⊔ top * e"
    by (metis assms(4) star.circ_back_loop_fixpoint sup_ge1 sup_left_isotone)
  also have "... = v⇧^T ⊔ top * e"
    by (simp add: assms(4))
  finally have 5: "(v ⊔ e⇧^T * top)⇧^T * (t ⊔ e) ≤ (v ⊔ e⇧^T * top)⇧^T"
    using 2 by (simp add: conv_dist_sup)
  have "r⇧^T * (t ⊔ e)⇧^⋆ ≤ (v ⊔ e⇧^T * top)⇧^T * (t ⊔ e)⇧^⋆"
    using 4 by (simp add: mult_left_isotone)
  also have "... ≤ (v ⊔ e⇧^T * top)⇧^T"
    using 5 by (simp add: star_right_induct_mult)
  finally show ?thesis
    using 3 by (simp add: order.eq_iff)
qed

text ‹
The next result is used to show that the while-loop preserves acyclicity of the constructed tree.
›

lemma acyclic_inv:
  assumes "acyclic t"
      and "vector v"
      and "e ≤ v * -v⇧^T"
      and "t ≤ v * v⇧^T"
    shows "acyclic (t ⊔ e)"
proof -
  have "t⇧⁺ * e ≤ t⇧⁺ * v * -v⇧^T"
    by (simp add: assms(3) comp_associative mult_right_isotone)
  also have "... ≤ v * v⇧^T * t⇧^⋆ * v * -v⇧^T"
    by (simp add: assms(4) mult_left_isotone)
  also have "... ≤ v * top * -v⇧^T"
    by (metis mult_assoc mult_left_isotone mult_right_isotone top_greatest)
  also have "... = v * -v⇧^T"
    by (simp add: assms(2))
  also have "... ≤ -1"
    by (simp add: pp_increasing schroeder_3_p)
  finally have 1: "t⇧⁺ * e ≤ -1"
    .
  have 2: "e * t⇧^⋆ = e"
    using assms(2-4) et(1) star_absorb by blast
  have "e⇧^⋆ = 1 ⊔ e ⊔ e * e * e⇧^⋆"
    by (metis star.circ_loop_fixpoint star_square_2 sup_commute)
  also have "... = 1 ⊔ e"
    using assms(2,3) ee comp_left_zero bot_least sup_absorb1 by simp
  finally have 3: "e⇧^⋆ = 1 ⊔ e"
    .
  have "e ≤ v * -v⇧^T"
    by (simp add: assms(3))
  also have "... ≤ -1"
    by (simp add: pp_increasing schroeder_3_p)
  finally have 4: "t⇧⁺ * e ⊔ e ≤ -1"
    using 1 by simp
  have "(t ⊔ e)⇧⁺ = (t ⊔ e) * t⇧^⋆ * (e * t⇧^⋆)⇧^⋆"
    using star_sup_1 mult_assoc by simp
  also have "... = (t ⊔ e) * t⇧^⋆ * (1 ⊔ e)"
    using 2 3 by simp
  also have "... = t⇧⁺ * (1 ⊔ e) ⊔ e * t⇧^⋆ * (1 ⊔ e)"
    by (simp add: comp_right_dist_sup)
  also have "... = t⇧⁺ * (1 ⊔ e) ⊔ e * (1 ⊔ e)"
    using 2 by simp
  also have "... = t⇧⁺ * (1 ⊔ e) ⊔ e"
    using 3 by (metis star_absorb assms(2,3) ee)
  also have "... = t⇧⁺ ⊔ t⇧⁺ * e ⊔ e"
    by (simp add: mult_left_dist_sup)
  also have "... ≤ -1"
    using 4 by (metis assms(1) sup.absorb1 sup.orderI sup_assoc)
  finally show ?thesis
    .
qed

text ‹
The following lemma shows that the extended tree is in the component reachable from the root.
›

lemma mst_subgraph_inv_2:
  assumes "regular (v * v⇧^T)"
      and "t ≤ v * v⇧^T ⊓ --g"
      and "v⇧^T = r⇧^T * t⇧^⋆"
      and "e ≤ v * -v⇧^T ⊓ --g"
      and "vector v"
      and "regular ((v ⊔ e⇧^T * top) * (v ⊔ e⇧^T * top)⇧^T)"
    shows "t ⊔ e ≤ (r⇧^T * (--((v ⊔ e⇧^T * top) * (v ⊔ e⇧^T * top)⇧^T ⊓ g))⇧^⋆)⇧^T * (r⇧^T * (--((v ⊔ e⇧^T * top) * (v ⊔ e⇧^T * top)⇧^T ⊓ g))⇧^⋆)"
proof -
  let ?v = "v ⊔ e⇧^T * top"
  let ?G = "?v * ?v⇧^T ⊓ g"
  let ?c = "r⇧^T * (--?G)⇧^⋆"
  have "v⇧^T ≤ r⇧^T * (--(v * v⇧^T ⊓ g))⇧^⋆"
    using assms(1-3) inf_pp_commute mult_right_isotone star_isotone by auto
  also have "... ≤ ?c"
    using comp_inf.mult_right_isotone comp_isotone conv_isotone inf.commute mult_right_isotone pp_isotone star_isotone sup.cobounded1 by presburger
  finally have 2: "v⇧^T ≤ ?c ∧ v ≤ ?c⇧^T"
    by (metis conv_isotone conv_involutive)
  have "t ≤ v * v⇧^T"
    using assms(2) by auto
  hence 3: "t ≤ ?c⇧^T * ?c"
    using 2 order_trans mult_isotone by blast
  have "e ≤ v * top ⊓ --g"
    by (metis assms(4,5) inf.bounded_iff inf.sup_left_divisibility mult_right_isotone top.extremum)
  hence "e ≤ v * top ⊓ top * e ⊓ --g"
    by (simp add: top_left_mult_increasing inf.boundedI)
  hence "e ≤ v * top * e ⊓ --g"
    by (metis comp_inf_covector inf.absorb2 mult_assoc top.extremum)
  hence "t ⊔ e ≤ (v * v⇧^T ⊓ --g) ⊔ (v * top * e ⊓ --g)"
    using assms(2) sup_mono by blast
  also have "... = v * ?v⇧^T ⊓ --g"
    by (simp add: inf_sup_distrib2 mult_assoc mult_left_dist_sup conv_dist_comp conv_dist_sup)
  also have "... ≤ --?G"
    using assms(6) comp_left_increasing_sup inf.sup_left_isotone pp_dist_inf by auto
  finally have 4: "t ⊔ e ≤ --?G"
    .
  have "e ≤ e * e⇧^T * e"
    by (simp add: ex231c)
  also have "... ≤ v * -v⇧^T * -v * v⇧^T * e"
    by (metis assms(4) mult_left_isotone conv_isotone conv_dist_comp mult_assoc mult_isotone conv_involutive conv_complement inf.boundedE)
  also have "... ≤ v * top * v⇧^T * e"
    by (metis mult_assoc mult_left_isotone mult_right_isotone top.extremum)
  also have "... = v * r⇧^T * t⇧^⋆ * e"
    using assms(3,5) by (simp add: mult_assoc)
  also have "... ≤ v * r⇧^T * (t ⊔ e)⇧^⋆"
    by (simp add: comp_associative mult_right_isotone star.circ_mult_upper_bound star.circ_sub_dist_1 star_isotone sup_commute)
  also have "... ≤ v * ?c"
    using 4 by (simp add: mult_assoc mult_right_isotone star_isotone)
  also have "... ≤ ?c⇧^T * ?c"
    using 2 by (simp add: mult_left_isotone)
  finally show ?thesis
    using 3 by simp
qed

lemma span_inv:
  assumes "e ≤ v * -v⇧^T"
      and "vector v"
      and "arc e"
      and "t ≤ (v * v⇧^T) ⊓ g"
      and "g⇧^T = g"
      and "v⇧^T = r⇧^T * t⇧^⋆"
      and "injective r"
      and "r⇧^T ≤ v⇧^T"
      and "r⇧^T * ((v * v⇧^T) ⊓ g)⇧^⋆ ≤ r⇧^T * t⇧^⋆"
    shows "r⇧^T * (((v ⊔ e⇧^T * top) * (v ⊔ e⇧^T * top)⇧^T) ⊓ g)⇧^⋆ ≤ r⇧^T * (t ⊔ e)⇧^⋆"
proof -
  let ?d = "(v * v⇧^T) ⊓ g"
  have 1: "(v ⊔ e⇧^T * top) * (v ⊔ e⇧^T * top)⇧^T = v * v⇧^T ⊔ v * v⇧^T * e ⊔ e⇧^T * v * v⇧^T ⊔ e⇧^T * e"
    using assms(1-3) ve_dist by simp
  have "t⇧^T ≤ ?d⇧^T"
    using assms(4) conv_isotone by simp
  also have "... = (v * v⇧^T) ⊓ g⇧^T"
    by (simp add: conv_dist_comp conv_dist_inf)
  also have "... = ?d"
    by (simp add: assms(5))
  finally have 2: "t⇧^T ≤ ?d"
    .
  have "v * v⇧^T = (r⇧^T * t⇧^⋆)⇧^T * (r⇧^T * t⇧^⋆)"
    by (metis assms(6) conv_involutive)
  also have "... = t⇧^T⇧^⋆ * (r * r⇧^T) * t⇧^⋆"
    by (simp add: comp_associative conv_dist_comp conv_star_commute)
  also have "... ≤ t⇧^T⇧^⋆ * 1 * t⇧^⋆"
    by (simp add: assms(7) mult_left_isotone star_right_induct_mult_iff star_sub_one)
  also have "... = t⇧^T⇧^⋆ * t⇧^⋆"
    by simp
  also have "... ≤ ?d⇧^⋆ * t⇧^⋆"
    using 2 by (simp add: comp_left_isotone star.circ_isotone)
  also have "... ≤ ?d⇧^⋆ * ?d⇧^⋆"
    using assms(4) mult_right_isotone star_isotone by simp
  also have 3: "... = ?d⇧^⋆"
    by (simp add: star.circ_transitive_equal)
  finally have 4: "v * v⇧^T ≤ ?d⇧^⋆"
    .
  have 5: "r⇧^T * ?d⇧^⋆ * (v * v⇧^T ⊓ g) ≤ r⇧^T * ?d⇧^⋆"
    by (simp add: comp_associative mult_right_isotone star.circ_plus_same star.left_plus_below_circ)
  have "r⇧^T * ?d⇧^⋆ * (v * v⇧^T * e ⊓ g) ≤ r⇧^T * ?d⇧^⋆ * v * v⇧^T * e"
    by (simp add: comp_associative comp_right_isotone)
  also have "... ≤ r⇧^T * ?d⇧^⋆ * e"
    using 3 4 by (metis comp_associative comp_isotone eq_refl)
  finally have 6: "r⇧^T * ?d⇧^⋆ * (v * v⇧^T * e ⊓ g) ≤ r⇧^T * ?d⇧^⋆ * e"
    .
  have 7: "∀x . r⇧^T * (1 ⊔ v * v⇧^T) * e⇧^T * x = bot"
  proof
    fix x
    have "r⇧^T * (1 ⊔ v * v⇧^T) * e⇧^T * x ≤ r⇧^T * (1 ⊔ v * v⇧^T) * e⇧^T * top"
      by (simp add: mult_right_isotone)
    also have "... = r⇧^T * e⇧^T * top ⊔ r⇧^T * v * v⇧^T * e⇧^T * top"
      by (simp add: comp_associative mult_left_dist_sup mult_right_dist_sup)
    also have "... = r⇧^T * e⇧^T * top"
      by (metis assms(1,2) mult_assoc mult_right_dist_sup mult_right_zero sup_bot_right vTeT)
    also have "... ≤ v⇧^T * e⇧^T * top"
      by (simp add: assms(8) comp_isotone)
    also have "... = bot"
      using vTeT assms(1,2) by simp
    finally show "r⇧^T * (1 ⊔ v * v⇧^T) * e⇧^T * x = bot"
      by (simp add: le_bot)
  qed
  have "r⇧^T * ?d⇧^⋆ * (e⇧^T * v * v⇧^T ⊓ g) ≤ r⇧^T * ?d⇧^⋆ * e⇧^T * v * v⇧^T"
    by (simp add: comp_associative comp_right_isotone)
  also have "... ≤ r⇧^T * (1 ⊔ v * v⇧^T) * e⇧^T * v * v⇧^T"
    by (metis assms(2) star.circ_isotone vector_vector_star inf_le1 comp_associative comp_right_isotone comp_left_isotone)
  also have "... = bot"
    using 7 by simp
  finally have 8: "r⇧^T * ?d⇧^⋆ * (e⇧^T * v * v⇧^T ⊓ g) = bot"
    by (simp add: le_bot)
  have "r⇧^T * ?d⇧^⋆ * (e⇧^T * e ⊓ g) ≤ r⇧^T * ?d⇧^⋆ * e⇧^T * e"
    by (simp add: comp_associative comp_right_isotone)
  also have "... ≤ r⇧^T * (1 ⊔ v * v⇧^T) * e⇧^T * e"
    by (metis assms(2) star.circ_isotone vector_vector_star inf_le1 comp_associative comp_right_isotone comp_left_isotone)
  also have "... = bot"
    using 7 by simp
  finally have 9: "r⇧^T * ?d⇧^⋆ * (e⇧^T * e ⊓ g) = bot"
    by (simp add: le_bot)
  have "r⇧^T * ?d⇧^⋆ * ((v ⊔ e⇧^T * top) * (v ⊔ e⇧^T * top)⇧^T ⊓ g) = r⇧^T * ?d⇧^⋆ * ((v * v⇧^T ⊔ v * v⇧^T * e ⊔ e⇧^T * v * v⇧^T ⊔ e⇧^T * e) ⊓ g)"
    using 1 by simp
  also have "... = r⇧^T * ?d⇧^⋆ * ((v * v⇧^T ⊓ g) ⊔ (v * v⇧^T * e ⊓ g) ⊔ (e⇧^T * v * v⇧^T ⊓ g) ⊔ (e⇧^T * e ⊓ g))"
    by (simp add: inf_sup_distrib2)
  also have "... = r⇧^T * ?d⇧^⋆ * (v * v⇧^T ⊓ g) ⊔ r⇧^T * ?d⇧^⋆ * (v * v⇧^T * e ⊓ g) ⊔ r⇧^T * ?d⇧^⋆ * (e⇧^T * v * v⇧^T ⊓ g) ⊔ r⇧^T * ?d⇧^⋆ * (e⇧^T * e ⊓ g)"
    by (simp add: comp_left_dist_sup)
  also have "... = r⇧^T * ?d⇧^⋆ * (v * v⇧^T ⊓ g) ⊔ r⇧^T * ?d⇧^⋆ * (v * v⇧^T * e ⊓ g)"
    using 8 9 by simp
  also have "... ≤ r⇧^T * ?d⇧^⋆ ⊔ r⇧^T * ?d⇧^⋆ * e"
    using 5 6 sup.mono by simp
  also have "... = r⇧^T * ?d⇧^⋆ * (1 ⊔ e)"
    by (simp add: mult_left_dist_sup)
  finally have 10: "r⇧^T * ?d⇧^⋆ * ((v ⊔ e⇧^T * top) * (v ⊔ e⇧^T * top)⇧^T ⊓ g) ≤ r⇧^T * ?d⇧^⋆ * (1 ⊔ e)"
    by simp
  have "r⇧^T * ?d⇧^⋆ * e * (v * v⇧^T ⊓ g) ≤ r⇧^T * ?d⇧^⋆ * e * v * v⇧^T"
    by (simp add: comp_associative comp_right_isotone)
  also have "... = bot"
    by (metis assms(1,2) comp_associative comp_right_zero ev comp_left_zero)
  finally have 11: "r⇧^T * ?d⇧^⋆ * e * (v * v⇧^T ⊓ g) = bot"
    by (simp add: le_bot)
  have "r⇧^T * ?d⇧^⋆ * e * (v * v⇧^T * e ⊓ g) ≤ r⇧^T * ?d⇧^⋆ * e * v * v⇧^T * e"
    by (simp add: comp_associative comp_right_isotone)
  also have "... = bot"
    by (metis assms(1,2) comp_associative comp_right_zero ev comp_left_zero)
  finally have 12: "r⇧^T * ?d⇧^⋆ * e * (v * v⇧^T * e ⊓ g) = bot"
    by (simp add: le_bot)
  have "r⇧^T * ?d⇧^⋆ * e * (e⇧^T * v * v⇧^T ⊓ g) ≤ r⇧^T * ?d⇧^⋆ * e * e⇧^T * v * v⇧^T"
    by (simp add: comp_associative comp_right_isotone)
  also have "... ≤ r⇧^T * ?d⇧^⋆ * 1 * v * v⇧^T"
    by (metis assms(3) arc_injective comp_associative comp_left_isotone comp_right_isotone)
  also have "... = r⇧^T * ?d⇧^⋆ * v * v⇧^T"
    by simp
  also have "... ≤ r⇧^T * ?d⇧^⋆ * ?d⇧^⋆"
    using 4 by (simp add: mult_right_isotone mult_assoc)
  also have "... = r⇧^T * ?d⇧^⋆"
    by (simp add: star.circ_transitive_equal comp_associative)
  finally have 13: "r⇧^T * ?d⇧^⋆ * e * (e⇧^T * v * v⇧^T ⊓ g) ≤ r⇧^T * ?d⇧^⋆"
    .
  have "r⇧^T * ?d⇧^⋆ * e * (e⇧^T * e ⊓ g) ≤ r⇧^T * ?d⇧^⋆ * e * e⇧^T * e"
    by (simp add: comp_associative comp_right_isotone)
  also have "... ≤ r⇧^T * ?d⇧^⋆ * 1 * e"
    by (metis assms(3) arc_injective comp_associative comp_left_isotone comp_right_isotone)
  also have "... = r⇧^T * ?d⇧^⋆ * e"
    by simp
  finally have 14: "r⇧^T * ?d⇧^⋆ * e * (e⇧^T * e ⊓ g) ≤ r⇧^T * ?d⇧^⋆ * e"
    .
  have "r⇧^T * ?d⇧^⋆ * e * ((v ⊔ e⇧^T * top) * (v ⊔ e⇧^T * top)⇧^T ⊓ g) = r⇧^T * ?d⇧^⋆ * e * ((v * v⇧^T ⊔ v * v⇧^T * e ⊔ e⇧^T * v * v⇧^T ⊔ e⇧^T * e) ⊓ g)"
    using 1 by simp
  also have "... = r⇧^T * ?d⇧^⋆ * e * ((v * v⇧^T ⊓ g) ⊔ (v * v⇧^T * e ⊓ g) ⊔ (e⇧^T * v * v⇧^T ⊓ g) ⊔ (e⇧^T * e ⊓ g))"
    by (simp add: inf_sup_distrib2)
  also have "... = r⇧^T * ?d⇧^⋆ * e * (v * v⇧^T ⊓ g) ⊔ r⇧^T * ?d⇧^⋆ * e * (v * v⇧^T * e ⊓ g) ⊔ r⇧^T * ?d⇧^⋆ * e * (e⇧^T * v * v⇧^T ⊓ g) ⊔ r⇧^T * ?d⇧^⋆ * e * (e⇧^T * e ⊓ g)"
    by (simp add: comp_left_dist_sup)
  also have "... = r⇧^T * ?d⇧^⋆ * e * (e⇧^T * v * v⇧^T ⊓ g) ⊔ r⇧^T * ?d⇧^⋆ * e * (e⇧^T * e ⊓ g)"
    using 11 12 by simp
  also have "... ≤ r⇧^T * ?d⇧^⋆ ⊔ r⇧^T * ?d⇧^⋆ * e"
    using 13 14 sup_mono by simp
  also have "... = r⇧^T * ?d⇧^⋆ * (1 ⊔ e)"
    by (simp add: mult_left_dist_sup)
  finally have 15: "r⇧^T * ?d⇧^⋆ * e * ((v ⊔ e⇧^T * top) * (v ⊔ e⇧^T * top)⇧^T ⊓ g) ≤ r⇧^T * ?d⇧^⋆ * (1 ⊔ e)"
    by simp
  have "r⇧^T ≤ r⇧^T * ?d⇧^⋆"
    using mult_right_isotone star.circ_reflexive by fastforce
  also have "... ≤ r⇧^T * ?d⇧^⋆ * (1 ⊔ e)"
    by (simp add: semiring.distrib_left)
  finally have 16: "r⇧^T ≤ r⇧^T * ?d⇧^⋆ * (1 ⊔ e)"
    .
  have "r⇧^T * ?d⇧^⋆ * (1 ⊔ e) * ((v ⊔ e⇧^T * top) * (v ⊔ e⇧^T * top)⇧^T ⊓ g) = r⇧^T * ?d⇧^⋆ * ((v ⊔ e⇧^T * top) * (v ⊔ e⇧^T * top)⇧^T ⊓ g) ⊔ r⇧^T * ?d⇧^⋆ * e * ((v ⊔ e⇧^T * top) * (v ⊔ e⇧^T * top)⇧^T ⊓ g)"
    by (simp add: semiring.distrib_left semiring.distrib_right)
  also have "... ≤ r⇧^T * ?d⇧^⋆ * (1 ⊔ e)"
    using 10 15 le_supI by simp
  finally have "r⇧^T * ?d⇧^⋆ * (1 ⊔ e) * ((v ⊔ e⇧^T * top) * (v ⊔ e⇧^T * top)⇧^T ⊓ g) ≤ r⇧^T * ?d⇧^⋆ * (1 ⊔ e)"
    .
  hence "r⇧^T ⊔ r⇧^T * ?d⇧^⋆ * (1 ⊔ e) * ((v ⊔ e⇧^T * top) * (v ⊔ e⇧^T * top)⇧^T ⊓ g) ≤ r⇧^T * ?d⇧^⋆ * (1 ⊔ e)"
    using 16 sup_least by simp
  hence "r⇧^T * ((v ⊔ e⇧^T * top) * (v ⊔ e⇧^T * top)⇧^T ⊓ g)⇧^⋆ ≤ r⇧^T * ?d⇧^⋆ * (1 ⊔ e)"
    by (simp add: star_right_induct)
  also have "... ≤ r⇧^T * t⇧^⋆ * (1 ⊔ e)"
    by (simp add: assms(9) mult_left_isotone)
  also have "... ≤ r⇧^T * (t ⊔ e)⇧^⋆"
    by (simp add: star_one_sup_below)
  finally show ?thesis
    .
qed

subsubsection ‹Exchange gives Spanning Trees›

text ‹
The following abbreviations are used in the spanning tree application using Prim's algorithm to construct the new tree for the exchange property.
It is obtained by replacing an edge with one that has minimal weight and reversing the path connecting these edges.
Here, w represents a weighted graph, v represents a set of nodes and e represents an edge.
›

abbreviation prim_E :: "'a ⇒ 'a ⇒ 'a ⇒ 'a" where "prim_E w v e ≡ w ⊓ --v * -v⇧^T ⊓ top * e * w⇧^T⇧^⋆"
abbreviation prim_P :: "'a ⇒ 'a ⇒ 'a ⇒ 'a" where "prim_P w v e ≡ w ⊓ -v * -v⇧^T ⊓ top * e * w⇧^T⇧^⋆"
abbreviation prim_EP :: "'a ⇒ 'a ⇒ 'a ⇒ 'a" where "prim_EP w v e ≡ w ⊓ -v⇧^T ⊓ top * e * w⇧^T⇧^⋆"
abbreviation prim_W :: "'a ⇒ 'a ⇒ 'a ⇒ 'a" where "prim_W w v e ≡ (w ⊓ -(prim_EP w v e)) ⊔ (prim_P w v e)⇧^T ⊔ e"

text ‹
The lemmas in this section are used to show that the relation after exchange represents a spanning tree.
The results in the next section are used to show that it is a minimum spanning tree.
›

lemma exchange_injective_3:
  assumes "e ≤ v * -v⇧^T"
      and "vector v"
    shows "(w ⊓ -(prim_EP w v e)) * e⇧^T = bot"
proof -
  have 1: "top * e ≤ -v⇧^T"
    by (simp add: assms schroeder_4_p vTeT)
  have "top * e ≤ top * e * w⇧^T⇧^⋆"
    using sup_right_divisibility star.circ_back_loop_fixpoint by blast
  hence "top * e ≤ -v⇧^T ⊓ top * e * w⇧^T⇧^⋆"
    using 1 by simp
  hence "top * e ≤ -(w ⊓ -prim_EP w v e)"
    by (metis inf.assoc inf_import_p le_infI2 p_antitone p_antitone_iff)
  hence "(w ⊓ -(prim_EP w v e)) * e⇧^T ≤ bot"
    using p_top schroeder_4_p by blast
  thus ?thesis
    using le_bot by simp
qed

lemma exchange_injective_6:
  assumes "arc e"
      and "forest w"
    shows "(prim_P w v e)⇧^T * e⇧^T = bot"
proof -
  have "e