# 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 = h⇧T ∧ 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 ⊔ w⇧T)"

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 = g⇧T"
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 * f⇧T⇧⋆)) ⊔ (f ⊓ top * minarc h * f⇧T⇧⋆)⇧T ⊔ minarc h) g (h ⊓ -minarc h ⊓ -minarc h⇧T)
∧ card { x . regular x ∧ x ≤ --h ∧ x ≤ -minarc h ∧ x ≤ -minarc h⇧T } < card { x . regular x ∧ x ≤ --h }) ∧
(¬ minarc h ≤ -forest_components f ⟶ kruskal_spanning_invariant f g (h ⊓ -minarc h ⊓ -minarc h⇧T)
∧ card { x . regular x ∧ x ≤ --h ∧ x ≤ -minarc h ∧ x ≤ -minarc h⇧T } < card { x . regular x ∧ x ≤ --h })"
proof -
let ?e = "minarc h"
let ?f = "(f ⊓ -(top * ?e * f⇧T⇧⋆)) ⊔ (f ⊓ top * ?e * f⇧T⇧⋆)⇧T ⊔ ?e"
let ?h = "h ⊓ -?e ⊓ -?e⇧T"
let ?F = "forest_components f"
let ?n1 = "card { x . regular x ∧ x ≤ --h }"
let ?n2 = "card { x . regular x ∧ x ≤ --h ∧ x ≤ -?e ∧ x ≤ -?e⇧T }"
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 (?e⇧T)"
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 "?e⇧T * top * ?e⇧T = ?e⇧T"
using assms(2) by (simp add: arc_top_arc minarc_arc)
hence "?e⇧T * top * ?e⇧T ≤ -?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 = ?h⇧T"
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 = ?h⇧T"
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 * f⇧T⇧⋆)) ⊔ (f ⊓ top * e * f⇧T⇧⋆)⇧T ⊔ e
ELSE
SKIP
FI;
h := h ⊓ -e ⊓ -e⇧T
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 * f⇧T⇧⋆)) ⊔ (f ⊓ top * e * f⇧T⇧⋆)⇧T ⊔ e
ELSE
SKIP
FI;
h := h ⊓ -e ⊓ -e⇧T
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 * f⇧T⇧⋆)) ⊔ (f ⊓ top * ?e * f⇧T⇧⋆)⇧T ⊔ ?e"
let ?h = "h ⊓ -?e ⊓ -?e⇧T"
let ?F = "forest_components f"
let ?n1 = "card { x . regular x ∧ x ≤ --h }"
let ?n2 = "card { x . regular x ∧ x ≤ --h ∧ x ≤ -?e ∧ x ≤ -?e⇧T }"
assume 1: "kruskal_invariant f g h ∧ h ≠ bot"
from 1 obtain w where 2: "minimum_spanning_forest w g ∧ f ≤ w ⊔ w⇧T"
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 "?e⇧T * top * ?e⇧T = ?e⇧T"
using 1 by (simp add: arc_top_arc minarc_arc)
hence "?e⇧T * top * ?e⇧T ≤ -?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 ⊔ w⇧T"
proof
let ?p = "w ⊓ top * ?e * w⇧T⇧⋆"
let ?v = "(w ⊓ -(top * ?e * w⇧T⇧⋆)) ⊔ ?p⇧T"
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 * w⇧T⇧⋆) ⊓ g) + sum (?p⇧T ⊓ 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 * w⇧T⇧⋆) ⊓ g) + sum (?p ⊓ g)"
using 1 kruskal_invariant_def kruskal_spanning_invariant_def sum_symmetric by simp
also have "... = sum (((w ⊓ -(top * ?e * w⇧T⇧⋆)) ⊔ ?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 ⊔ ?v⇧T = w ⊔ w⇧T"
proof -
have "?v ⊔ ?v⇧T = (w ⊓ -?p) ⊔ ?p⇧T ⊔ (w⇧T ⊓ -?p⇧T) ⊔ ?p"
using conv_complement conv_dist_inf conv_dist_sup inf_import_p sup_assoc by simp
also have "... = w ⊔ w⇧T"
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 * ?e⇧T = 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 * ?e⇧T * ?v⇧T⇧⋆ ⊓ ?F * ?e⇧T * 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 ⊔ f⇧T ≤ (?v ⊓ -?d ⊓ -?d⇧T) ⊔ (?v⇧T ⊓ -?d ⊓ -?d⇧T)"
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 ⊔ ?w⇧T"
proof (intro conjI)
have 18: "?e⇧T ≤ ?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) * ?e⇧T ≤ ?v * ?e⇧T"
using inf_le1 mult_left_isotone by simp
hence "(?v ⊓ -?d) * ?e⇧T = 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⇧⋆ * ?e⇧T * 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)"
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 ⊔ f⇧T ⊔ ?e"
using conv_dist_inf inf_le1 sup_left_isotone sup_mono by presburger
also have "... ≤ (?v ⊓ -?d ⊓ -?d⇧T) ⊔ (?v⇧T ⊓ -?d ⊓ -?d⇧T) ⊔ ?e"
using 17 sup_left_isotone by simp
also have "... ≤ (?v ⊓ -?d) ⊔ (?v⇧T ⊓ -?d ⊓ -?d⇧T) ⊔ ?e"
using inf.cobounded1 sup_inf_distrib2 by presburger
also have "... = ?w ⊔ (?v⇧T ⊓ -?d ⊓ -?d⇧T)"
by (simp add: sup_assoc sup_commute)
also have "... ≤ ?w ⊔ (?v⇧T ⊓ -?d⇧T)"
using inf.sup_right_isotone inf_assoc sup_right_isotone by simp
also have "... ≤ ?w ⊔ ?w⇧T"
using conv_complement conv_dist_inf conv_dist_sup sup_right_isotone by simp
finally show "?f ≤ ?w ⊔ ?w⇧T"
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 ⊔ w⇧T"
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 ⊓ f⇧T⇧⋆ * f⇧⋆"
using 29 spanning_forest_def inf.sup_right_isotone by simp
also have "... ≤ f ⊔ f⇧T"
apply (rule cancel_separate_6[where z=w and y="w⇧T"])
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 ⊔ f⇧T"
by simp
have "sum (f ⊓ g) = sum ((w ⊔ w⇧T) ⊓ (f ⊓ g))"
using 30 by (metis inf_absorb2 inf.assoc)
also have "... = sum (w ⊓ (f ⊓ g)) + sum (w⇧T ⊓ (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 ⊓ (f⇧T ⊓ g⇧T))"
by (metis conv_dist_inf conv_involutive sum_conv)
also have "... = sum (f ⊓ (w ⊓ g)) + sum (f⇧T ⊓ (w ⊓ g))"
using 28 inf.commute inf.assoc kruskal_invariant_def kruskal_spanning_invariant_def by simp
also have "... = sum ((f ⊔ f⇧T) ⊓ (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 ≡ r⇧T * (--g)⇧⋆"
definition "spanning_tree t g r ≡ forest t ∧ t ≤ (component g r)⇧T * (component g r) ⊓ --g ∧ component g r ≤ r⇧T * t⇧⋆ ∧ regular t"
definition "minimum_spanning_tree t g r ≡ spanning_tree t g r ∧ (∀u . spanning_tree u g r ⟶ sum (t ⊓ g) ≤ sum (u ⊓ g))"
definition "prim_precondition g r ≡ g = g⇧T ∧ injective r ∧ vector r ∧ regular r"
definition "prim_spanning_invariant t v g r ≡ prim_precondition g r ∧ v⇧T = r⇧T * t⇧⋆ ∧ spanning_tree t (v * v⇧T ⊓ g) r"
definition "prim_invariant t v g r ≡ prim_spanning_invariant t v g r ∧ (∃w . minimum_spanning_tree w g r ∧ t ≤ w)"

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

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

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

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

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

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

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

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

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

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

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

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

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

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

end

end



# 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 * d⇧T ≤ 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 ∧ a⇧T * 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 ⊓ - e⇧T ⊓ - p) ⊔ (f ⊓ - e⇧T ⊓ p) ⊔ (f ⊓ - e⇧T ⊓ p)⇧T ⊔ (f ⊓ - e⇧T ⊓ - p)⇧T ⊔ e⇧T ⊔ e = f ⊔ f⇧T ⊔ e ⊔ e⇧T"
proof -
have "(f ⊓ - e⇧T ⊓ - p) ⊔ (f ⊓ - e⇧T ⊓ p) ⊔ (f ⊓ - e⇧T ⊓ p)⇧T ⊔ (f ⊓ - e⇧T ⊓ - p)⇧T ⊔ e⇧T ⊔ e
= (f ⊓ - e⇧T ⊓ - p) ⊔ (f ⊓ - e⇧T ⊓ p) ⊔ (f⇧T ⊓ - e ⊓ p⇧T) ⊔ (f⇧T ⊓ - e ⊓ - p⇧T) ⊔ e⇧T ⊔ e"
by (simp add: conv_complement conv_dist_inf)
also have "... =
((f ⊔ (f ⊓ - e⇧T ⊓ p)) ⊓ (- e⇧T ⊔ (f ⊓ - e⇧T ⊓ p)) ⊓ (- p ⊔ (f ⊓ - e⇧T ⊓ p)))
⊔ ((f⇧T ⊔ (f⇧T ⊓ - e ⊓ - p⇧T)) ⊓ (- e ⊔ (f⇧T ⊓ - e ⊓ - p⇧T)) ⊓ (p⇧T ⊔ (f⇧T ⊓ - e ⊓ - p⇧T)))
⊔ e⇧T ⊔ e"
by (metis sup_inf_distrib2 sup_assoc)
also have "... =
((f ⊔ f) ⊓ (f ⊔ - e⇧T) ⊓ (f ⊔ p) ⊓ (- e⇧T ⊔ f) ⊓ (- e⇧T ⊔ - e⇧T) ⊓ (- e⇧T ⊔ p) ⊓ (- p ⊔ f) ⊓ (- p ⊔ - e⇧T) ⊓ (- p ⊔ p))
⊔ ((f⇧T ⊔ f⇧T) ⊓ (f⇧T ⊔ - e) ⊓ (f⇧T ⊔ - p⇧T) ⊓ (- e ⊔ f⇧T) ⊓ (- e ⊔ - e) ⊓ (- e ⊔ - p⇧T) ⊓ (p⇧T ⊔ f⇧T) ⊓ (p⇧T ⊔ - e) ⊓ (p⇧T ⊔ - p⇧T))
⊔ e⇧T ⊔ e"
using sup_inf_distrib1 sup_assoc inf_assoc sup_inf_distrib1 by simp
also have "... =
((f ⊔ f) ⊓ (f ⊔ - e⇧T) ⊓ (f ⊔ p) ⊓ (f ⊔ - p) ⊓ (- e⇧T ⊔ f) ⊓ (- e⇧T ⊔ - e⇧T) ⊓ (- e⇧T ⊔ p) ⊓ (- e⇧T ⊔ - p) ⊓ (- p ⊔ p))
⊔ ((f⇧T ⊔ f⇧T) ⊓ (f⇧T ⊔ - e) ⊓ (f⇧T ⊔ - p⇧T) ⊓ (- e ⊔ f⇧T) ⊓ (f⇧T ⊔ p⇧T) ⊓ (- e ⊔ - e) ⊓ (- e ⊔ - p⇧T) ⊓ (- e ⊔ p⇧T) ⊓ (p⇧T ⊔ - p⇧T))
⊔ e⇧T ⊔ e"
by (smt abel_semigroup.commute inf.abel_semigroup_axioms inf.left_commute sup.abel_semigroup_axioms)
also have "... = (f ⊓ - e⇧T ⊓ (- p ⊔ p)) ⊔ (f⇧T ⊓ - e ⊓ (p⇧T ⊔ - p⇧T)) ⊔ e⇧T ⊔ e"
also have "... = (f ⊓ - e⇧T) ⊔ (f⇧T ⊓ - e) ⊔ e⇧T ⊔ e"
by (metis assms(1) conv_complement inf_top_right stone)
also have "... = (f ⊔ e⇧T) ⊓ (- e⇧T ⊔ e⇧T) ⊔ (f⇧T ⊔ 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 ⊓ - e⇧T ⊓ - p ⊔ (f ⊓ - e⇧T ⊓ p)⇧T ⊔ e)"
and "injective f"
shows "forest_components ((f ⊓ - e⇧T ⊓ - p) ⊔ (f ⊓ -e⇧T ⊓ p)⇧T ⊔ e) = (f ⊔ f⇧T ⊔ e ⊔ e⇧T)⇧⋆"
proof -
have "forest_components ((f ⊓ - e⇧T ⊓ - p) ⊔ (f ⊓ -e⇧T ⊓ p)⇧T ⊔ e) = wcc ((f ⊓ - e⇧T ⊓ - p) ⊔ (f ⊓ - e⇧T ⊓ p)⇧T ⊔ e)"
by (simp add: assms(3) forest_components_wcc)
also have "... = ((f ⊓ - e⇧T ⊓ - p) ⊔ (f ⊓ - e⇧T ⊓ p)⇧T ⊔ e ⊔ (f ⊓ - e⇧T ⊓ - p)⇧T ⊔ (f ⊓ - e⇧T ⊓ p) ⊔ e⇧T)⇧⋆"
using conv_dist_sup sup_assoc by auto
also have "... = ((f ⊓ - e⇧T ⊓ - p) ⊔ (f ⊓ - e⇧T ⊓ p) ⊔ (f ⊓ - e⇧T ⊓ p)⇧T ⊔ (f ⊓ - e⇧T ⊓ - p)⇧T ⊔ e⇧T ⊔ e)⇧⋆"
using sup_assoc sup_commute by auto
also have "... = (f ⊔ f⇧T ⊔ e ⊔ e⇧T)⇧⋆"
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 ⊓ - e⇧T ⊓ - p ⊔ (f ⊓ - e⇧T ⊓ p)⇧T ⊔ e)"
and "injective f"
shows "forest_components f ≤ forest_components (f ⊓ - e⇧T ⊓ - p ⊔ (f ⊓ - e⇧T ⊓ p)⇧T ⊔ e)"
proof -
have 1: "forest_components ((f ⊓ - e⇧T ⊓ - p) ⊔ (f ⊓ -e⇧T ⊓ p)⇧T ⊔ e) = (f ⊔ f⇧T ⊔ e ⊔ e⇧T)⇧⋆"
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 ⊔ f⇧T ⊔ e⇧T ⊔ 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 "d⇧T * H * d ≤ 1"
proof -
have "d⇧T * H⇧T * 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 * a⇧T ≤ 1"
by (metis assms(2) conv_dist_comp symmetric_top_closed vector_top_closed mult_assoc)
hence "a * top * a⇧T * H ≤ H"
using assms(1) comp_isotone order_trans by blast
hence "a * top * top * a⇧T * 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 "(d⇧T * H)⇧⋆ * (H * d)⇧⋆ = (d⇧T * H)⇧⋆ ⊔ (H * d)⇧⋆"
proof -
have "(H * d)⇧T * H * d ≤ 1"
using assms big_forest_def mult_assoc by auto
hence "d⇧T * 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: "d⇧T * H * d ≤ 1"
using assms(3) big_forest_def dTransHd_le_1 by blast
hence "d * - 1 * d⇧T ≤ - H"
using triple_schroeder_p by force
hence "d * - 1 * d⇧T ≤ 1 ⊔ - H"
by (simp add: le_supI2)
hence "d * d⇧T ⊔ d * - 1 * d⇧T ≤ 1 ⊔ - H"
by (metis assms(3) big_forest_def inf_commute regular_one_closed shunting_p le_supI)
hence "d * 1 * d⇧T ⊔ d * - 1 * d⇧T ≤ 1 ⊔ - H"
by simp
hence "d * (1 ⊔ - 1) * d⇧T ≤ 1 ⊔ - H"
using comp_associative mult_right_dist_sup by (simp add: mult_left_dist_sup)
hence "d * top * d⇧T ≤ 1 ⊔ - H"
using regular_complement_top by auto
hence "d * top * a⇧T ≤ 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 * top⇧T) * (top ⊓ (H * a)⇧T * d)"
by (metis dedekind inf_commute)
also have "... = d * top ⊓ H * a * a⇧T * H⇧T * d"
by (simp add: conv_dist_comp inf_vector_comp mult_assoc)
also have "... ≤ d * top ⊓ H * a * d⇧T * H⇧T * d"
using assms(2) mult_right_isotone mult_left_isotone conv_isotone inf.sup_right_isotone by auto
also have "... = d * top ⊓ H * a * d⇧T * 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: "d⇧T * 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 "... ≤ d⇧T * 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 * top⇧T * minarc(v)⇧T * e⇧T"
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) j⇧T ⊓ 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 g⇧T)⇧T⇧⋆"

definition "boruvka_outer_invariant f g ≡
symmetric g
∧ forest f
∧ f ≤ --g
∧ regular f
∧ (∃w . minimum_spanning_forest w g ∧ f ≤ w ⊔ w⇧T)"

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 ⊔ d⇧T))⇧⋆ * forest_components h
∧ f ⊔ f⇧T = h ⊔ h⇧T ⊔ d ⊔ d⇧T
∧ (∀ 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 "f⇧T ≤ ?F"
by (metis conv_dist_comp conv_involutive conv_order conv_star_commute forest_components_increasing)
hence "- ?F ≤ - f⇧T"
using p_antitone by auto
hence "?e ≤ - f⇧T"
using 1 dual_order.trans by blast
hence "f⇧T ≤ - ?e"
by (simp add: p_antitone_iff)
hence "f⇧T⇧T ≤ - ?e⇧T"
by (metis conv_complement conv_dist_inf inf.orderE inf.orderI)
hence "f ≤ - ?e⇧T"
by auto
hence "f = f ⊓ - ?e⇧T"
using inf.orderE by blast
hence "f ⊓ - ?e⇧T ⊓ - ?p ⊔ (f ⊓ - ?e⇧T ⊓ ?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 * -?c⇧T ⊓ g) * top"
using comp_isotone minarc_below by blast
also have "... = (--(?c * -?c⇧T) ⊓ --g) * top"
by simp
also have "... = (?c * -?c⇧T ⊓ --g) * top"
using component_is_regular regular_mult_closed by auto
also have "... = (?c ⊓ -?c⇧T ⊓ --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 "?H⇧T * ?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 "a⇧T * 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:"a⇧T * top ≤ (H * d)⇧⋆ * H * b * top ⊔ (H * d)⇧⋆ * H * c * (H * d)⇧⋆ * H * b * top"
by simp
have 13: "a⇧T * top ≤ (H * d)⇧⋆ * H * b * top ∨ a⇧T * top ≤ (H * d)⇧⋆ * H * c * (H * d)⇧⋆ * H * b * top"
proof (rule point_in_vector_sup)
show "point (a⇧T * 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 "a⇧T * 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 "a⇧T * top ≤ (H * d)⇧⋆ * H * b * top")
case True
assume "a⇧T * 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: "a⇧T * top ≤ (H * d)⇧⋆ * H * c * (H * d)⇧⋆ * H * b * top"
using 13 by (simp add: False)
hence 15: "a⇧T * top ≤ (H * d)⇧⋆ * H * c * top"
by (metis mult_right_isotone order_lesseq_imp top_greatest mult_assoc)
have "c⇧T * top ≤ (H * d)⇧⋆ * H * b * top"
proof (rule ccontr)
assume "¬ c⇧T * top ≤ (H * d)⇧⋆ * H * b * top"
hence "c⇧T * 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 "a⇧T * top ≤ (H * d)⇧⋆ * H * b * top"
using bf_between_arcs_def by blast
hence "a⇧T * 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 "a⇧T * top ≤ (H * d)⇧⋆ * H * c * top"
using bf_between_arcs_def by blast
also have "... ≤ (H * d)⇧⋆ * H * c * c⇧T * c * top"
by (metis ex231c comp_inf.star.circ_sup_2 mult_isotone mult_right_isotone mult_assoc)
also have "... ≤ (H * d)⇧⋆ * H * c * c⇧T * 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 "a⇧T * 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 "d⇧T * 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 "d⇧T * ?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 ⊔ f⇧T = h ⊔ h⇧T ⊔ d ⊔ d⇧T"
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 * ?H⇧T * ?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') ⟷ ?e⇧T * ?H * d ⊔ d⇧T * ?H * ?e ⊔ ?e⇧T * ?H * ?e ⊔ d⇧T * ?H * d ≤ 1"
using conv_dist_sup semiring.distrib_left semiring.distrib_right by auto
have 22: "?e⇧T * ?H * ?e ≤ 1"
proof -
have 221: "?e⇧T * ?H * ?e ≤ ?e⇧T * 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 "?e⇧T * top * ?e ≤ 1"
using arc_expanded by blast
thus ?thesis
using 221 dual_order.trans by blast
qed
have 24: "d⇧T * ?H * ?e ≤ 1"
by (metis assms(2, 3, 7, 8, 12) dT_He_eq_bot coreflexive_bot_closed le_bot)
hence "(d⇧T * ?H * ?e)⇧T ≤ 1⇧T"
using conv_isotone by blast
hence "?e⇧T * ?H⇧T * d⇧T⇧T ≤ 1"
by (simp add: conv_dist_comp mult_assoc)
hence 25: "?e⇧T * ?H * d ≤ 1"
using assms(4) fch_equivalence by auto
have 8: "d⇧T * ?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) * (d⇧T ⊔ ?e⇧T) ≤ 1"
by (simp add: conv_dist_sup)
also have "... ⟷ ?H ⊓ (d * d⇧T ⊔ d * ?e⇧T ⊔ ?e * d⇧T ⊔ ?e * ?e⇧T) ≤ 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 * d⇧T ⊔ ?H ⊓ d * ?e⇧T ⊔ ?H ⊓ ?e * d⇧T ⊔ ?H ⊓ ?e * ?e⇧T ≤ 1"
by (simp add: inf_sup_distrib1)
have 31: "?H ⊓ d * d⇧T ≤ 1"
using assms(6) big_forest_def by blast
have 32: "?H ⊓ ?e * d⇧T ≤ 1"
proof -
have "?e * d⇧T ≤ ?e * top * (d * top)⇧T"
by (simp add: conv_isotone mult_isotone top_right_mult_increasing)
also have "... ≤ ?e * top * - j⇧T"
by (metis assms(7) conv_complement conv_isotone mult_right_isotone)
also have "... ≤ j * - j⇧T"
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 * d⇧T ≤ - ?H"
by simp
thus ?thesis
by (metis inf.coboundedI1 p_antitone_iff p_shunting_swap regular_one_closed)
qed
have 33: "?H ⊓ d * ?e⇧T ≤ 1"
proof -
have 331: "injective h"
by (simp add: assms(4))
have "(?H ⊓ ?e * d⇧T)⇧T ≤ 1"
using 32 coreflexive_conv_closed by auto
hence "?H ⊓ (?e * d⇧T)⇧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 * ?e⇧T ≤ 1"
proof -
have 341:"arc ?e ∧ arc (?e⇧T)"
using assms(11) minarc_arc minarc_bot_iff by auto
have "?H ⊓ ?e * ?e⇧T ≤ ?e * ?e⇧T"
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 "?F⇧T * ?F ≤ - ?e"
using assms(1) fch_equivalence by fastforce
hence "?F⇧T * ?F * ?F⇧T ≤ - ?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 ⊔ f⇧T"
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 "¬ a⇧T * top ≤ H * e * top"
and "regular a"
and "regular e"
and "regular H"
and "regular d"
shows "arc (d ⊓ top * e⇧T * H ⊓ (H * d⇧T)⇧⋆ * H * a⇧T * top)"
proof -
let ?x = "d ⊓ top * e⇧T * H ⊓ (H * d⇧T)⇧⋆ * H * a⇧T * top"
have 1:"regular ?x"
using assms(5, 6, 7, 8) regular_closed_star regular_conv_closed regular_mult_closed by auto
have 2: "a⇧T * top * a ≤ 1"
using arc_expanded assms(2) bf_between_arcs_def by auto
have 3: "e * top * e⇧T ≤ 1"
using assms(2) bf_between_arcs_def arc_expanded by blast
have 4: "top * ?x * top = top"
proof -
have "a⇧T * 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 "a⇧T * top ≤ H * e * top ⊔ (H * d)⇧⋆ * H * d * H * e * top"
by simp
hence "a⇧T * top ≤ H * e * top ∨ a⇧T * 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 "a⇧T * 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 ⊓ top⇧T * e⇧T * H⇧T) * H * e * top"
using conv_dist_comp mult_assoc by auto
also have "... = (H * d)⇧⋆ * H * (d ⊓ top * e⇧T * H) * H * e * top"
using assms(1) by (simp add: big_forest_def)
finally have 2: "a⇧T * top ≤ (H * d)⇧⋆ * H * (d ⊓ top * e⇧T * H) * H * e * top"
by simp
hence "e * top ≤ ((H * d)⇧⋆ * H * (d ⊓ top * e⇧T * H) * H)⇧T * a⇧T * top"
proof -
have "bijective (e * top) ∧ bijective (a⇧T * top)"
using assms(2) bf_between_arcs_def by auto
thus ?thesis
using 2 by (metis bijective_reverse mult_assoc)
qed
also have "... = H⇧T * (d ⊓ top * e⇧T * H)⇧T * H⇧T * (H * d)⇧⋆⇧T * a⇧T * top"
by (simp add: conv_dist_comp mult_assoc)
also have "... = H * (d ⊓ top * e⇧T * H)⇧T * H * (H * d)⇧⋆⇧T * a⇧T * top"
using assms(1) big_forest_def by auto
also have "... = H * (d ⊓ top * e⇧T * H)⇧T * H * (d⇧T * H)⇧⋆ * a⇧T * top"
using assms(1) big_forest_def conv_dist_comp conv_star_commute by auto
also have "... = H * (d⇧T ⊓ H * e * top) * H * (d⇧T * H)⇧⋆ * a⇧T * top"
using assms(1) conv_dist_comp big_forest_def comp_associative conv_dist_inf by auto
also have "... = H * (d⇧T ⊓ H * e * top) * (H * d⇧T)⇧⋆ * H * a⇧T * top"
by (simp add: comp_associative star_slide)
also have "... = H * (d⇧T ⊓ H * e * top) * ((H * d⇧T)⇧⋆ * H * a⇧T * top ⊓ (H * d⇧T)⇧⋆ * H * a⇧T * top)"
using mult_assoc by auto
also have "... = H * (d⇧T ⊓ H * e * top ⊓ ((H * d⇧T)⇧⋆ * H * a⇧T * top)⇧T) * (H * d⇧T)⇧⋆ * H * a⇧T * top"
by (smt comp_inf_vector covector_comp_inf vector_conv_covector vector_top_closed mult_assoc)
also have "... = H * (d⇧T ⊓ (top * e⇧T * H)⇧T ⊓ ((H * d⇧T)⇧⋆ * H * a⇧T * top)⇧T) * (H * d⇧T)⇧⋆ * H * a⇧T * top"
using assms(1) big_forest_def conv_dist_comp mult_assoc by auto
also have "... = H * (d ⊓ top * e⇧T * H ⊓ (H * d⇧T)⇧⋆ * H * a⇧T * top)⇧T * (H * d⇧T)⇧⋆ * H * a⇧T * top"
by (simp add: conv_dist_inf)
finally have 3: "e * top ≤ H * ?x⇧T * (H * d⇧T)⇧⋆ * H * a⇧T * 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 * ?x⇧T ≤ 1"
proof -
have 51: "H * (d * H)⇧⋆ ⊓ d * H * d⇧T ≤ 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 * (d⇧T * H)⇧⋆ ≤ - d"
by (smt assms(1) big_forest_def conv_dist_comp conv_star_commute schroeder_4_p star_slide)
hence "H * (d * H)⇧⋆ ≤ - d⇧T"
using 511 by (metis assms(1) big_forest_def schroeder_5_p star_slide)
hence "H * (d * H)⇧⋆ ≤ - (H * d⇧T)"
by (metis assms(3) p_antitone_iff schroeder_4_p star_slide mult_assoc)
hence "H * (d * H)⇧⋆ ⊓ H * d⇧T ≤ bot"
by (simp add: bot_unique pseudo_complement)
hence "H * d * (H * (d * H)⇧⋆ ⊓ H * d⇧T) ≤ 1"
by (simp add: bot_unique)
hence 512: "H * d * H * (d * H)⇧⋆ ⊓ H * d * H * d⇧T ≤ 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 * d⇧T ≤ 1"
proof -
have "d * H * d⇧T ≤ H * d * H * d⇧T"
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 "d⇧T * H * d ≤ 1 ⊔ - H"
using assms(1) big_forest_def dTransHd_le_1 le_supI1 by blast
hence "(- 1 ⊓ H) * d⇧T * H ≤ - d⇧T"
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) * d⇧T ≤ - H"
by (metis assms(1) big_forest_def conv_dist_comp schroeder_3_p triple_schroeder_p)
hence "H ⊓ d * (- 1 ⊓ H) * d⇧T ≤ 1"
by (metis inf.coboundedI1 p_antitone_iff p_shunting_swap regular_one_closed)
hence "H ⊓ d * d⇧T ⊔ H ⊓ d * (- 1 ⊓ H) * d⇧T ≤ 1"
using assms(1) big_forest_def le_supI by blast
hence "H ⊓ (d * 1 * d⇧T ⊔ d * (- 1 ⊓ H) * d⇧T) ≤ 1"
using comp_inf.semiring.distrib_left by auto
hence "H ⊓ (d * (1 ⊔ (- 1 ⊓ H)) * d⇧T) ≤ 1"
by (simp add: mult_left_dist_sup mult_right_dist_sup)
hence 514: "H ⊓ d * H * d⇧T ≤ 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 * d⇧T ⊔ H * d * H * (d * H)⇧⋆ ⊓ d * H * d⇧T ≤ 1"
using 513 514 by simp
hence "d * H * d⇧T ⊓ (H ⊔ H * d * H * (d * H)⇧⋆) ≤ 1"
hence "d * H * d⇧T ⊓ H * (1 ⊔ d * H * (d * H)⇧⋆) ≤ 1"
by (simp add: mult_left_dist_sup mult_assoc)
thus ?thesis
qed
qed
have "?x * top * ?x⇧T = (d ⊓ top * e⇧T * H ⊓ (H * d⇧T)⇧⋆ * H * a⇧T * top) * top * (d⇧T ⊓ H⇧T * e⇧T⇧T * top⇧T ⊓ top⇧T * a⇧T⇧T * H⇧T * (d⇧T⇧T * H⇧T)⇧⋆)"
by (simp add: conv_dist_comp conv_dist_inf conv_star_commute mult_assoc)
also have "... = (d ⊓ top * e⇧T * H ⊓ (H * d⇧T)⇧⋆ * H * a⇧T * top) * top * (d⇧T ⊓ H * e * top ⊓ top * a * H * (d * H)⇧⋆)"
using assms(1) big_forest_def by auto
also have "... = (H * d⇧T)⇧⋆ * H * a⇧T * top ⊓ (d ⊓ top * e⇧T * H) * top * (d⇧T ⊓ H * e * top ⊓ top * a * H * (d * H)⇧⋆)"
by (metis inf_vector_comp vector_export_comp)
also have "... = (H * d⇧T)⇧⋆ * H * a⇧T * top ⊓ (d ⊓ top * e⇧T * H) * top * top * (d⇧T ⊓ H * e * top ⊓ top * a * H * (d * H)⇧⋆)"
by (simp add: vector_mult_closed)
also have "... = (H * d⇧T)⇧⋆ * H * a⇧T * top ⊓ d * ((top * e⇧T * H)⇧T ⊓ top) * top * (d⇧T ⊓ H * e * top ⊓ top * a * H * (d * H)⇧⋆)"
by (simp add: covector_comp_inf_1 covector_mult_closed)
also have "... = (H * d⇧T)⇧⋆ * H * a⇧T * top ⊓ d * ((top * e⇧T * H)⇧T ⊓ (H * e * top)⇧T) * d⇧T ⊓ 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 * d⇧T)⇧⋆ * H * a⇧T * top ⊓ top * a * H * (d * H)⇧⋆ ⊓ d * ((top * e⇧T * H)⇧T ⊓ (H * e * top)⇧T) * d⇧T"
also have "... = (H * d⇧T)⇧⋆ * H * a⇧T * top * top * a * H * (d * H)⇧⋆ ⊓ d * ((top * e⇧T * H)⇧T ⊓ (H * e * top)⇧T) * d⇧T"
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 * d⇧T)⇧⋆ * H * a⇧T * top * a * H * (d * H)⇧⋆ ⊓ d * (H * e * top ⊓ top * e⇧T * H) * d⇧T"
using assms(1) big_forest_def conv_dist_comp mult_assoc by auto
also have "... = (H * d⇧T)⇧⋆ * H * a⇧T * top * a * H * (d * H)⇧⋆ ⊓ d * H * e * top * e⇧T * H * d⇧T"
by (metis comp_inf_covector inf_top.left_neutral mult_assoc)
also have "... ≤ (H * d⇧T)⇧⋆ * (H * d)⇧⋆ * H ⊓ d * H * e * top * e⇧T * H * d⇧T"
proof -
have "(H * d⇧T)⇧⋆ * H * a⇧T * top * a * H * (d * H)⇧⋆ ≤ (H * d⇧T)⇧⋆ * 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 * d⇧T)⇧⋆ * H * (d * H)⇧⋆"
using assms(1) big_forest_def mult.semigroup_axioms preorder_idempotent semigroup.assoc by fastforce
also have "... = (H * d⇧T)⇧⋆ * (H * d)⇧⋆ * H"
by (metis star_slide mult_assoc)
finally show ?thesis
using inf.sup_left_isotone by auto
qed
also have "... ≤ (H * d⇧T)⇧⋆ * (H * d)⇧⋆ * H ⊓ d * H * d⇧T"
proof -
have "d * H * e * top * e⇧T * H * d⇧T ≤ d * H * 1 * H * d⇧T"
using 3 by (metis comp_isotone idempotent_one_closed mult_left_isotone mult_sub_right_one mult_assoc)
also have "... ≤ d * H * d⇧T"
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 * (d⇧T * H)⇧⋆ * (H * d)⇧⋆ * H ⊓ d * H * d⇧T"
by (metis assms(1) big_forest_def comp_associative preorder_idempotent star_slide)
also have "... = H * ((d⇧T * H)⇧⋆ ⊔ (H * d)⇧⋆) * H ⊓ d * H * d⇧T"
by (simp add: assms(1) expand_big_forest mult.semigroup_axioms semigroup.assoc)
also have "... = (H * (d⇧T * H)⇧⋆ * H ⊔ H * (H * d)⇧⋆ * H) ⊓ d * H * d⇧T"
by (simp add: mult_left_dist_sup mult_right_dist_sup)
also have "... = (H * d⇧T)⇧⋆ * H ⊓ d * H * d⇧T ⊔ H * (d * H)⇧⋆ ⊓ d * H * d⇧T"
by (smt assms(1) big_forest_def inf_sup_distrib2 mult.semigroup_axioms preorder_idempotent star_slide semigroup.assoc)
also have "... ≤ (H * d⇧T)⇧⋆ * H ⊓ d * H * d⇧T ⊔ 1"
using 51 comp_inf.semiring.add_left_mono by blast
finally have "?x * top * ?x⇧T ≤ 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: "?x⇧T * top * ?x ≤ 1"
proof -
have "?x⇧T * top * ?x = (d⇧T ⊓ H⇧T * e⇧T⇧T * top⇧T ⊓ top⇧T * a⇧T⇧T * H⇧T * (d⇧T⇧T * H⇧T)⇧⋆) * top * (d ⊓ top * e⇧T * H ⊓ (H * d⇧T)⇧⋆ * H * a⇧T * top)"
by (simp add: conv_dist_comp conv_dist_inf conv_star_commute mult_assoc)
also have "... = (d⇧T ⊓ H * e * top ⊓ top * a * H * (d * H)⇧⋆) * top * (d ⊓ top * e⇧T * H ⊓ (H * d⇧T)⇧⋆ * H * a⇧T * top)"
using assms(1) big_forest_def by auto
also have "... = H * e * top ⊓ (d⇧T ⊓ top * a * H * (d * H)⇧⋆) * top * (d ⊓ top * e⇧T * H ⊓ (H * d⇧T)⇧⋆ * H * a⇧T * 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 ⊓ d⇧T * ((top * a * H * (d * H)⇧⋆)⇧T ⊓ top) * (d ⊓ top * e⇧T * H ⊓ (H * d⇧T)⇧⋆ * H * a⇧T * top)"
by (simp add: covector_comp_inf_1 covector_mult_closed)
also have "... = H * e * top ⊓ d⇧T * (d * H)⇧⋆⇧T * H * a⇧T * top * (d ⊓ top * e⇧T * H ⊓ (H * d⇧T)⇧⋆ * H * a⇧T * top)"
using assms(1) big_forest_def comp_associative conv_dist_comp by auto
also have "... = H * e * top ⊓ d⇧T * (d * H)⇧⋆⇧T * H * a⇧T * top * (d ⊓ (H * d⇧T)⇧⋆ * H * a⇧T * top) ⊓ top * e⇧T * H"
also have "... = H * e * top ⊓ d⇧T * (d * H)⇧⋆⇧T * H * a⇧T * (top ⊓ ((H * d⇧T)⇧⋆ * H * a⇧T * top)⇧T) * d ⊓ top * e⇧T * H"
by (metis comp_associative comp_inf_vector vector_conv_covector vector_top_closed)
also have "... = H * e * top ⊓ (H * e * top)⇧T ⊓ d⇧T * (d * H)⇧⋆⇧T * H * a⇧T * ((H * d⇧T)⇧⋆ * H * a⇧T * 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 ⊓ d⇧T * (d * H)⇧⋆⇧T * H * a⇧T * ((H * d⇧T)⇧⋆ * H * a⇧T * top)⇧T * d"
using vector_covector vector_mult_closed by auto
also have "... = H * e * top * top⇧T * e⇧T * H⇧T ⊓ d⇧T * (d * H)⇧⋆⇧T * H * a⇧T * top⇧T * a⇧T⇧T * H⇧T * (H * d⇧T)⇧⋆⇧T * d"
by (smt conv_dist_comp mult.semigroup_axioms symmetric_top_closed semigroup.assoc)
also have "... = H * e * top * top * e⇧T * H ⊓ d⇧T * (H * d⇧T)⇧⋆ * H * a⇧T * 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 * e⇧T * H ⊓ d⇧T * (H * d⇧T)⇧⋆ * H * a⇧T * top * a * H * (d * H)⇧⋆ * d"
using vector_top_closed mult_assoc by auto
also have "... ≤ H ⊓ d⇧T * (H * d⇧T)⇧⋆ * H * (d * H)⇧⋆ * d"
proof -
have "H * e * top * e⇧T * 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 * e⇧T * H ≤ H"
by simp
have "d⇧T * (H * d⇧T)⇧⋆ * H * a⇧T * top * a * H * (d * H)⇧⋆ * d ≤ d⇧T * (H * d⇧T)⇧⋆ * H * 1 * H * (d * H)⇧⋆ * d"
using 2 by (metis comp_associative mult_left_isotone mult_right_isotone)
also have "... = d⇧T * (H * d⇧T)⇧⋆ * H * (d * H)⇧⋆ * d"
using assms(1) big_forest_def mult.semigroup_axioms preorder_idempotent semigroup.assoc by fastforce
finally have "d⇧T * (H * d⇧T)⇧⋆ * H * a⇧T * top * a * H * (d * H)⇧⋆ * d ≤ d⇧T * (H * d⇧T)⇧⋆ * H * (d * H)⇧⋆ * d"
by simp
thus ?thesis
using 611 comp_inf.comp_isotone by blast
qed
also have "... = H ⊓ (d⇧T * H)⇧⋆ * d⇧T * H * d * (H * d)⇧⋆"
using star_slide mult_assoc by auto
also have "... ≤ H ⊓ (d⇧T * H)⇧⋆ * (H * d)⇧⋆"
proof -
have "(d⇧T * H)⇧⋆ * d⇧T * H * d * (H * d)⇧⋆ ≤ (d⇧T * 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 "... = (d⇧T * H)⇧⋆ * (H * d)⇧⋆"
by simp
finally show ?thesis
using inf.sup_right_isotone by blast
qed
also have "... = H ⊓ ((d⇧T * H)⇧⋆ ⊔ (H * d)⇧⋆)"
by (simp add: assms(1) expand_big_forest)
also have "... = H ⊓ (d⇧T * H)⇧⋆ ⊔ H ⊓ (H * d)⇧⋆"
by (simp add: comp_inf.semiring.distrib_left)
also have "... = 1 ⊔ H ⊓ (d⇧T * 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 ⊓ (d⇧T * H)⇧⋆ = 1 ⊔ H ⊓ (d⇧T * 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 ⊓ (d⇧T * 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 (?x⇧T * 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 * e⇧T = bot"
and "e * F * e = bot"
and "e⇧T ≤ v⇧⋆"
and "e ≠ bot"
shows "arc (v ⊓ -F * e * top ⊓ top * e⇧T * F)"
proof -
let ?i = "v ⊓ -F * e * top ⊓ top * e⇧T * F"
have 1: "?i⇧T * top * ?i ≤ 1"
proof -
have "?i⇧T * top * ?i = (v⇧T ⊓ top * e⇧T * -F ⊓ F * e * top) * top * (v ⊓ -F * e * top ⊓ top * e⇧T * F)"
using assms(1) conv_complement conv_dist_comp conv_dist_inf mult.semigroup_axioms semigroup.assoc by fastforce
also have "... = F * e * top ⊓ (v⇧T ⊓ top * e⇧T * -F) * top * (v ⊓ -F * e * top) ⊓ top * e⇧T * F"
by (smt covector_comp_inf covector_mult_closed inf_vector_comp vector_export_comp vector_top_closed)
also have "... = F * e * top ⊓ (v⇧T ⊓ top * e⇧T * -F) * top * top * (v ⊓ -F * e * top) ⊓ top * e⇧T * F"
by (simp add: comp_associative)
also have "... = F * e * top ⊓ v⇧T * (top ⊓ (top * e⇧T * -F)⇧T) * top * (v ⊓ -F * e * top) ⊓ top * e⇧T * F"
using comp_associative comp_inf_vector_1 by auto
also have "... = F * e * top ⊓ v⇧T * (top ⊓ (top * e⇧T * -F)⇧T) * (top ⊓ (-F * e * top)⇧T) * v ⊓ top * e⇧T * F"
by (smt comp_inf_vector conv_dist_comp mult.semigroup_axioms symmetric_top_closed semigroup.assoc)
also have "... = F * e * top ⊓ v⇧T * (top * e⇧T * -F)⇧T * (-F * e * top)⇧T * v ⊓ top * e⇧T * F"
by simp
also have "... = F * e * top ⊓ v⇧T * -F⇧T * e⇧T⇧T * top⇧T * top⇧T * e⇧T * -F⇧T * v ⊓ top * e⇧T * F"
by (metis comp_associative conv_complement conv_dist_comp)
also have "... = F * e * top ⊓ v⇧T * -F * e * top * top * e⇧T * -F * v ⊓ top * e⇧T * F"
by (simp add: assms(1))
also have "... = F * e * top ⊓ v⇧T * -F * e * top ⊓ top * e⇧T * -F * v ⊓ top * e⇧T * F"
by (metis comp_associative comp_inf_covector inf.sup_monoid.add_assoc inf_top.left_neutral vector_top_closed)
also have "... = (F ⊓ v⇧T * -F) * e * top ⊓ top * e⇧T * -F * v ⊓ top * e⇧T * F"
using assms(3) injective_comp_right_dist_inf mult_assoc by auto
also have "... = (F ⊓ v⇧T * -F) * e * top ⊓ top * e⇧T * (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 ⊓ v⇧T * -F) * e * top * top * e⇧T * (F ⊓ -F * v)"
by (metis comp_associative comp_inf_covector inf_top.left_neutral vector_top_closed)
also have "... = (F ⊓ v⇧T * -F) * e * top * e⇧T * (F ⊓ -F * v)"
by (simp add: comp_associative)
also have "... ≤ (F ⊓ v⇧T * -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 ⊓ v⇧T * -F) * (F ⊓ -F * v) ⊓ F"
by (metis assms(1) inf.absorb1 inf.cobounded1 mult_isotone preorder_idempotent)
also have "... ≤ (F ⊓ v⇧T * -F) * (F ⊓ -F * v) ⊓ (F ⊓ v)⇧T⇧⋆ * (F ⊓ v)⇧⋆"
using assms(5) comp_inf.mult_right_isotone by auto
also have "... ≤ (-F ⊓ v⇧T) * -F * -F * (-F ⊓ v) ⊓ (F ⊓ v)⇧T⇧⋆ * (F ⊓ v)⇧⋆"
proof -
have "F ⊓ v⇧T * -F ≤ (v⇧T ⊓ F * -F⇧T) * -F"
by (metis conv_complement dedekind_2 inf_commute)
also have "... = (v⇧T ⊓ -F⇧T) * -F"
using assms(1) equivalence_comp_left_complement by simp
finally have "F ⊓ v⇧T * -F ≤ F ⊓ (v⇧T ⊓ -F) * -F"
using assms(1) by auto
hence 11: "F ⊓ v⇧T * -F = F ⊓ (-F ⊓ v⇧T) * -F"
by (metis inf.antisym_conv inf.sup_monoid.add_commute comp_left_subdist_inf inf.boundedE inf.sup_right_isotone)
hence "F⇧T ⊓ -F⇧T * v⇧T⇧T = F⇧T ⊓ -F⇧T * (-F⇧T ⊓ v⇧T⇧T)"
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 ⊓ v⇧T * -F) * (F ⊓ -F * v) = (F ⊓ (-F ⊓ v⇧T) * -F) * (F ⊓ -F * (-F ⊓ v))"
using 11 12 by auto
also have "... ≤ (-F ⊓ v⇧T) * -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 ⊓ v⇧T) * -F * -F * (-F ⊓ v) ⊓ (F ⊓ v)⇧T * (F ⊓ v)⇧T⇧⋆ * (F ⊓ v)⇧⋆) ⊔ ((-F ⊓ v⇧T) * -F * -F * (-F ⊓ v) ⊓ (F ⊓ v)⇧⋆)"
by (metis comp_associative inf_sup_distrib1 star.circ_loop_fixpoint)
also have "... = ((-F ⊓ v⇧T) * -F * -F * (-F ⊓ v) ⊓ (F ⊓ v⇧T) * (F ⊓ v)⇧T⇧⋆ * (F ⊓ v)⇧⋆) ⊔ ((-F ⊓ v⇧T) * -F * -F * (-F ⊓ v) ⊓ (F ⊓ v)⇧⋆)"
using assms(1) conv_dist_inf by auto
also have "... = bot ⊔ ((-F ⊓ v⇧T) * -F * -F * (-F ⊓ v) ⊓ (F ⊓ v)⇧⋆)"
proof -
have "(-F ⊓ v⇧T) * -F * -F * (-F ⊓ v) ⊓ (F ⊓ v⇧T) * (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 ⊓ v⇧T) * -F * -F * (-F ⊓ v) ⊓ (1 ⊔ (F ⊓ v)⇧⋆ * (F ⊓ v))"
by (simp add: star.circ_plus_same star_left_unfold_equal)
also have "... = ((-F ⊓ v⇧T) * -F * -F * (-F ⊓ v) ⊓ 1) ⊔ ((-F ⊓ v⇧T) * -F * -F * (-F ⊓ v) ⊓ (F ⊓ v)⇧⋆ * (F ⊓ v))"
by (simp add: comp_inf.semiring.distrib_left)
also have "... ≤ 1 ⊔ ((-F ⊓ v⇧T) * -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 * ?i⇧T ≤ 1"
proof -
have "?i * top * ?i⇧T = (v ⊓ -F * e * top ⊓ top * e⇧T * F) * top * (v⇧T ⊓ (-F * e * top)⇧T ⊓ (top * e⇧T * F)⇧T)"
by (simp add: conv_dist_inf)
also have "... = (v ⊓ -F * e * top ⊓ top * e⇧T * F) * top * (v⇧T ⊓ top⇧T * e⇧T * -F⇧T ⊓ F⇧T * e⇧T⇧T * top⇧T)"
by (simp add: conv_complement conv_dist_comp mult_assoc)
also have "... = (v ⊓ -F * e * top ⊓ top * e⇧T * F) * top * (v⇧T ⊓ top * e⇧T * -F ⊓ F * e * top)"
by (simp add: assms(1))
also have "... = -F * e * top ⊓ (v ⊓ top * e⇧T * F) * top * (v⇧T ⊓ top * e⇧T * -F ⊓ F * e * top)"
by (smt inf.left_commute inf.sup_monoid.add_assoc vector_export_comp)
also have "... = -F * e * top ⊓ (v ⊓ top * e⇧T * F) * top * (v⇧T ⊓ F * e * top) ⊓ top * e⇧T * -F"
also have "... = -F * e * top ⊓ (v ⊓ top * e⇧T * F) * top * top * (v⇧T ⊓ F * e * top) ⊓ top * e⇧T * -F"
by (simp add: mult_assoc)
also have "... = -F * e * top ⊓ v * ((top * e⇧T * F)⇧T ⊓ top) * top * (v⇧T ⊓ F * e * top) ⊓ top * e⇧T * -F"
by (simp add: comp_inf_vector_1 mult.semigroup_axioms semigroup.assoc)
also have "... = -F * e * top ⊓ v * ((top * e⇧T * F)⇧T ⊓ top) * (top ⊓ (F * e * top)⇧T) * v⇧T ⊓ top * e⇧T * -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 * e⇧T * F)⇧T * (F * e * top)⇧T * v⇧T ⊓ top * e⇧T * -F"
by simp
also have "... = -F * e * top ⊓ v * F⇧T * e⇧T⇧T * top⇧T * top⇧T * e⇧T * F⇧T * v⇧T ⊓ top * e⇧T * -F"
by (metis comp_associative conv_dist_comp)
also have "... = -F * e * top ⊓ v * F * e * top * top * e⇧T * F * v⇧T ⊓ top * e⇧T * -F"
using assms(1) by auto
also have "... = -F * e * top ⊓ v * F * e * top ⊓ top * e⇧T * F * v⇧T ⊓ top * e⇧T * -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 * e⇧T * F * v⇧T ⊓ top * e⇧T * -F"
using injective_comp_right_dist_inf assms(3) mult.semigroup_axioms semigroup.assoc by fastforce
also have "... = (-F ⊓ v * F) * e * top ⊓ top * e⇧T * (F * v⇧T ⊓ -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 * e⇧T * (F * v⇧T ⊓ -F)"
by (metis inf_top_right vector_export_comp vector_top_closed)
also have "... = (-F ⊓ v * F) * e * top * e⇧T * (F * v⇧T ⊓ -F)"
by (simp add: comp_associative)
also have "... ≤ (-F ⊓ v * F) * (F * v⇧T ⊓ -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 * v⇧T ≤ 1"
by (simp add: assms(2))
hence "v * v⇧T * F ≤ F"
using assms(1) dual_order.trans mult_left_isotone by blast
hence "v * v⇧T * F⇧T⇧⋆ * 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 * F⇧T⇧⋆ * 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
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 * F⇧T⇧⋆) * (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 ⊓ v⇧T⇧⋆)) * (-F ⊓ v)⇧T"
proof -
have "(F ⊓ v)⇧⋆ * (F ⊓ v)⇧T⇧⋆ ≤ F⇧⋆ * F⇧T⇧⋆"
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⇧⋆ * v⇧T⇧⋆"
by (simp add: fc_isotone)
hence "(F ⊓ v)⇧⋆ * (F ⊓ v)⇧T⇧⋆ ≤ F ⊓ v⇧⋆ * v⇧T⇧⋆"
using 21 by simp
also have "... = F ⊓ (v⇧⋆ ⊔ v⇧T⇧⋆)"
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 ⊓ v⇧T⇧⋆) * (-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 ⊓ v⇧T⇧⋆) ≤ (-F ⊓ v) * ((F ⊓ v)⇧T⇧⋆ * (F ⊓ v)⇧⋆ ⊓ v⇧T⇧⋆)"
by (simp add: assms(5) inf.coboundedI1 mult_right_isotone)
also have "... = (-F ⊓ v) * ((F ⊓ v)⇧T * (F ⊓ v)⇧T⇧⋆ * (F ⊓ v)⇧⋆ ⊓ v⇧T⇧⋆) ⊔ (-F ⊓ v) * ((F ⊓ v)⇧⋆ ⊓ v⇧T⇧⋆)"
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)⇧⋆ ⊓ v⇧T⇧⋆)"
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⇧⋆ ⊓ v⇧T⇧⋆)"
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⇧⋆ ⊓ v⇧T⇧⋆)"
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 ⊓ v⇧T⇧⋆) ≤ -F ⊓ v"
by simp
have "((-F ⊓ v) * (F ⊓ v⇧T⇧⋆))⇧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 * v⇧T"
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 (e⇧T * -F * v * F * e)"
using assms(3, 4, 6) arc_regular regular_mult_closed by auto
have 32: "bijective ((top * e⇧T)⇧T)"
using assms(3) by (simp add: conv_dist_comp)
have "top * ?i * top = top * (v ⊓ -F * e * top) * ((top * e⇧T * F)⇧T ⊓ top)"
by (simp add: comp_associative comp_inf_vector_1)
also have "... = (top ⊓ (-F * e * top)⇧T) * v * ((top * e⇧T * F)⇧T ⊓ top)"
using comp_inf_vector conv_dist_comp by auto
also have "... = (-F * e * top)⇧T * v * (top * e⇧T * F)⇧T"
by simp
also have "... = top⇧T * e⇧T * -F⇧T * v * F⇧T * e⇧T⇧T * top⇧T"
by (simp add: comp_associative conv_complement conv_dist_comp)
finally have 33: "top * ?i * top = top * e⇧T * -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 * e⇧T * F) * top ≠ bot"
hence "top * e⇧T * -F * v * F * e * top = bot"
using 33 by auto
hence "e⇧T * -F * v * F * e = bot"
using 31 tarski comp_associative le_bot by fastforce
hence "top * (-F * v * F * e)⇧T ≤ -(e⇧T)"
by (metis comp_associative conv_complement_sub_leq conv_involutive p_bot schroeder_5_p)
hence "top * e⇧T * F⇧T * v⇧T * -F⇧T ≤ -(e⇧T)"
by (simp add: comp_associative conv_complement conv_dist_comp)
hence "v * F * e * top * e⇧T ≤ F"
by (metis assms(1, 4) comp_associative conv_dist_comp schroeder_3_p symmetric_top_closed)
hence "v * F * e * top * top * e⇧T ≤ F"
by (simp add: comp_associative)
hence "v * F * e * top ≤ F * (top * e⇧T)⇧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 "e⇧T * F * e * top ≤ F * e * top"
by (meson assms(9) mult_left_isotone order_trans)
hence "e⇧T * F * e * top * (e * top)⇧T ≤ F"
using 32 shunt_bijective assms(3) mult_assoc by auto
hence 34: "e⇧T * F * e * top * top * e⇧T ≤ F"
by (metis conv_dist_comp mult.semigroup_axioms symmetric_top_closed semigroup.assoc)
hence "e⇧T ≤ F"
proof -
have "e⇧T ≤ e⇧T * e * e⇧T"
by (metis conv_involutive ex231c)
also have "... ≤ e⇧T * F * e * e⇧T"
using assms(1) comp_associative mult_left_isotone mult_right_isotone by fastforce
also have "... ≤ e⇧T * F * e * top * top * e⇧T"
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 * e⇧T * F ≤ - e"
by (simp add: assms(1) comp_associative conv_dist_comp)
hence "(top * e⇧T)⇧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 (?i⇧T * 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 * - c⇧T ⊓ g)"
using assms(1) minarc_below order_trans by blast
also have "... ≤ -- (c * - c⇧T)"
using order_lesseq_imp pp_isotone_inf by blast
also have "... = c * - c⇧T"
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 "x⇧T * top ≤ forest_components(h) * e * top"
and "e ≤ c * -c⇧T"
and "c = forest_components(h) * c"
shows "x ≤ c⇧T"
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 * e⇧T * ?H"
using assms(1) comp_associative conv_dist_comp forest_components_equivalence by auto
also have "... ≤ top * (c * - c⇧T)⇧T * ?H"
by (simp add: assms(4) conv_isotone mult_left_isotone mult_right_isotone)
also have "... = top * (- c * c⇧T) * ?H"
by (simp add: conv_complement conv_dist_comp)
also have "... ≤ top * c⇧T * ?H"
by (metis mult_left_isotone top.extremum mult_assoc)
also have "... = c⇧T * ?H"
using assms(1, 2) component_is_vector vector_conv_covector by auto
also have "... = c⇧T"
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 * c⇧T ≤ forest_components h"
and "x ≤ c⇧T"
and "x ≤ -forest_components h"
shows "x ≤ -c"
proof -
let ?H = "forest_components h"
have "x ≤ - ?H ⊓ c⇧T"
using assms(3, 4) by auto
also have "... ≤ - c"
proof -
have "c ⊓ c⇧T ≤ ?H"
using assms(1, 2) vector_covector by auto
hence "-?H ⊓ c ⊓ c⇧T ≤ 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 "x⇧T * top ≤ (forest_components h) * e * top"
and "c = (forest_components h) * c"
and "c * c⇧T ≤ 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 * - c⇧T"
using assms(1, 2) e_leq_c_c_complement_transpose_general by auto
have 2: "x ≤ c⇧T"
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 ⊓ c⇧T"
using 2 by simp
hence "x ≤ - c * c⇧T"
using assms(4) by (simp add: vector_complement_closed vector_covector)
hence "x⇧T ≤ c⇧T⇧T * - c⇧T"
by (metis conv_complement conv_dist_comp conv_isotone)
hence 3: "x⇧T ≤ c * - c⇧T"
by simp
hence "x ≤ -- g"
using assms(8) by auto
hence "x⇧T ≤ -- g"
using assms(9) conv_complement conv_isotone by fastforce
hence "x⇧T ⊓ c * - c⇧T ⊓ -- 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 "x⇧T ⊓ c * - c⇧T ⊓ g ≠ bot"
using inf.sup_monoid.add_commute pp_inf_bot_iff by auto
hence "sum (minarc (c * - c⇧T ⊓ g) ⊓ (c * - c⇧T ⊓ g)) ≤ sum (x⇧T ⊓ c * - c⇧T ⊓ g)"
using assms(10) minarc_min inf.sup_monoid.add_assoc by auto
hence "sum (e ⊓ c * - c⇧T ⊓ g) ≤ sum (x⇧T ⊓ c * - c⇧T ⊓ g)"
using assms(1) inf.sup_monoid.add_assoc by auto
hence "sum (e ⊓ g) ≤ sum (x⇧T ⊓ 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 "x⇧T * 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 * - ?c⇧T ⊓ 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 "x⇧T * top ≤ ?H * ?e * top"
by (simp add: assms(5))
next
show "?c = ?H * ?c"
using component_single by auto
next
show "?c * ?c⇧T ≤ ?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 ⊔ f⇧T = h ⊔ h⇧T ⊔ d ⊔ d⇧T"
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 "a⇧T * top ≤ ?H * ?e * top")
case True
show "a⇧T * 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 "a⇧T * 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 "¬ a⇧T * top ≤ ?H * ?e * top ⟹ sum (b ⊓ g) ≤ sum (a ⊓ g)"
proof -
let ?d' = "d ⊔ ?e"
let ?x = "d ⊓ top * ?e⇧T * ?H ⊓ (?H * d⇧T)⇧⋆ * ?H * a⇧T * 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 "¬ a⇧T * 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 (a⇧T * top)"
by (simp add: assms(11))
have 63: "bijective (?x * top)"
using 61 by simp
have 64: "?x ≤ (?H * d⇧T)⇧⋆ * ?H * a⇧T * top"
by simp
hence "?x * top ≤ (?H * d⇧T)⇧⋆ * ?H * a⇧T * top"
using mult_left_isotone inf_vector_comp by auto
hence "a⇧T * top ≤ ((?H * d⇧T)⇧⋆ * ?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 "a⇧T * 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"
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"
also have "... ≤ f ⊔ f⇧T"
proof -
have "h ⊔ h⇧T ⊔ d ⊔ d⇧T = f ⊔ f⇧T"
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 "?x⇧T * top ≤ ?H * ?e * top"
proof -
have "?x ≤ top * ?e⇧T * ?H"
using inf.coboundedI1 by auto
hence "?x⇧T ≤ ?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 "?x⇧T * 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⇧⋆ * e⇧T = e⇧T"
and "i ≤ v ⊓ top * e⇧T * w⇧T⇧⋆"
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⇧⋆ * e⇧T * top"
proof -
have 1: "(v ⊓ -i ⊓ -i⇧T) * (v⇧T ⊓ -i ⊓ -i⇧T) ≤ 1"
using assms(1) comp_isotone order.trans inf.cobounded1 by blast
have 2: "bijective (i * top) ∧ bijective (e⇧T * top)"
using assms(4, 5) mult_assoc by auto
have "i ≤ v * (top * e⇧T * w⇧T⇧⋆)⇧T"
using assms(3) covector_mult_closed covector_restrict_comp_conv order_lesseq_imp vector_top_closed by blast
also have "... ≤ v * w⇧T⇧⋆⇧T * e⇧T⇧T * top⇧T"
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 * e⇧T * e * top"
using assms(5) arc_eq_1 by (simp add: comp_associative)
also have "... ≤ v * w⇧⋆ * e * e⇧T * top"
by (simp add: comp_associative mult_right_isotone)
also have "... ≤ (--g) * (--g)⇧⋆ * (--g) * e⇧T * top"
using assms(6, 7, 8) by (simp add: comp_isotone star_isotone)
also have "... ≤ (--g)⇧⋆ * e⇧T * top"
by (metis comp_isotone mult_left_isotone star.circ_increasing star.circ_transitive_equal)
also have "... ≤ v⇧T⇧⋆ * v⇧⋆ * e⇧T * top"
by (simp add: assms(9) mult_left_isotone)
also have "... ≤ v⇧T⇧⋆ * e⇧T * top"
by (simp add: assms(2) comp_associative)
finally have "i ≤ v⇧T⇧⋆ * e⇧T * top"