# 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)" by (simp add: inf.sup_monoid.add_assoc) finally have "sum (?w ⊓ g) ≤ sum (?v ⊓ g)" by simp thus "∀u . spanning_forest u g ⟶ sum (?w ⊓ g) ≤ sum (u ⊓ g)" using 2 11 minimum_spanning_forest_def by auto qed next have "?f ≤ f ⊔ 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}" by (simp add: conv_isotone inf.sup_monoid.add_assoc) also have "... ≤ (?c⇧^{T}* ?c ⊓ --g)⇧^{T}" using 11 conv_order by simp also have "... = ?c⇧^{T}* ?c ⊓ --g" using 2 14 conv_dist_comp conv_dist_inf by simp finally have 17: "?p⇧^{T}≤ ?c⇧^{T}* ?c ⊓ --g" . have "?e ≤ ?c⇧^{T}* ?c ⊓ ?g" using 5 6 11 mst_subgraph_inv by auto thus ?thesis using 16 17 by simp qed next show "?c ≤ r⇧^{T}* ?w⇧^{⋆}" proof - have "?c ≤ r⇧^{T}* w⇧^{⋆}" using 10 minimum_spanning_tree_def spanning_tree_def by simp also have "... ≤ r⇧^{T}* ?w⇧^{⋆}" using 4 7 8 10 11 12 15 by (metis mst_reachable_inv) finally show ?thesis . qed next show "regular ?w" using 15 by simp qed next have 18: "?f ⊔ ?p = ?fp" using 2 8 epm_1 by fastforce have "arc (w ⊓ --v * -v⇧^{T}⊓ top * ?e * w⇧^{T}⇧^{⋆})" using 5 6 8 9 11 12 reachable_restrict arc_edge by auto hence 19: "arc ?f" using 2 by simp hence "?f = bot ⟶ top = bot" by (metis mult_left_zero mult_right_zero) hence "?f ≠ bot" using 1 le_bot by auto hence "?f ⊓ v * -v⇧^{T}⊓ ?g ≠ bot" using 2 11 by (simp add: inf.absorb1 le_infI1) hence "g ⊓ (?f ⊓ v * -v⇧^{T}) ≠ bot" using inf_commute pp_inf_bot_iff by simp hence 20: "?f ⊓ ?vcv ≠ bot" by (simp add: inf_assoc inf_commute) hence 21: "?f ⊓ g = ?f ⊓ ?vcv" using 2 by (simp add: inf_assoc inf_commute inf_left_commute) have 22: "?e ⊓ g = minarc ?vcv ⊓ ?vcv" using 7 by (simp add: inf.absorb2 inf.assoc inf.commute) hence 23: "sum (?e ⊓ g) ≤ sum (?f ⊓ g)" using 15 19 20 21 by (simp add: minarc_min) have "?e ≠ bot" using 20 comp_inf.semiring.mult_not_zero semiring.mult_not_zero by blast hence 24: "?e ⊓ g ≠ bot" using 22 minarc_meet_bot by auto have "sum (?w ⊓ g) = sum (w ⊓ -?fp ⊓ g) + sum (?p⇧^{T}⊓ g) + sum (?e ⊓ g)" using 7 8 10 by (metis sum_disjoint_3 epm_8 epm_9 epm_10 minimum_spanning_tree_def spanning_tree_def) also have "... = sum (((w ⊓ -?fp) ⊔ ?p⇧^{T}) ⊓ g) + sum (?e ⊓ g)" using 11 by (metis epm_8 sum_disjoint) also have "... ≤ sum (((w ⊓ -?fp) ⊔ ?p⇧^{T}) ⊓ g) + sum (?f ⊓ g)" using 23 24 by (simp add: sum_plus_right_isotone) also have "... = sum (w ⊓ -?fp ⊓ g) + sum (?p⇧^{T}⊓ g) + sum (?f ⊓ g)" using 11 by (metis epm_8 sum_disjoint) also have "... = sum (w ⊓ -?fp ⊓ g) + sum (?p ⊓ g) + sum (?f ⊓ g)" using 13 sum_symmetric by auto also have "... = sum (((w ⊓ -?fp) ⊔ ?p ⊔ ?f) ⊓ g)" using 2 8 by (metis sum_disjoint_3 epm_11 epm_12 epm_13) also have "... = sum (w ⊓ g)" using 2 8 15 18 epm_2 by force finally have "sum (?w ⊓ g) ≤ sum (w ⊓ g)" . thus "∀u . spanning_tree u g r ⟶ sum (?w ⊓ g) ≤ sum (u ⊓ g)" using 10 order_lesseq_imp minimum_spanning_tree_def by auto qed next show "?t ≤ ?w" using 4 8 10 mst_extends_new_tree by simp qed qed next show "?n2 < ?n1" using 1 prim_invariant_def prim_vc_2 by auto qed next fix t v let ?g = "--g" assume 25: "prim_invariant t v g r ∧ v * -v⇧^{T}⊓ g = bot" hence 26: "regular v" by (metis prim_invariant_def prim_spanning_invariant_def spanning_tree_def prim_precondition_def regular_conv_closed regular_closed_star regular_mult_closed conv_involutive) from 25 obtain w where 27: "minimum_spanning_tree w g r ∧ t ≤ w" by (metis prim_invariant_def) have "spanning_tree t g r" using 25 prim_invariant_def prim_vc_3 by blast hence "component g r = v⇧^{T}" by (metis 25 prim_invariant_def span_tree_component prim_spanning_invariant_def spanning_tree_def) hence 28: "w ≤ v * v⇧^{T}" using 26 27 by (simp add: minimum_spanning_tree_def spanning_tree_def inf_pp_commute) have "vector r ∧ injective r ∧ forest w" using 25 27 by (simp add: prim_invariant_def prim_spanning_invariant_def prim_precondition_def minimum_spanning_tree_def spanning_tree_def) hence "w = t" using 25 27 28 prim_invariant_def prim_spanning_invariant_def mst_post by blast thus "minimum_spanning_tree t g r" using 27 by simp qed end end

# 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" by (smt inf.sup_monoid.add_assoc inf.sup_monoid.add_commute inf_sup_absorb sup.idem) 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" by (simp add: comp_inf.semiring.distrib_left inf.sup_monoid.add_commute) hence "d * H * d⇧^{T}⊓ H * (1 ⊔ d * H * (d * H)⇧^{⋆}) ≤ 1" by (simp add: mult_left_dist_sup mult_assoc) thus ?thesis by (simp add: inf.sup_monoid.add_commute star_left_unfold_equal) qed qed have "?x * top * ?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}" using inf.sup_monoid.add_assoc inf.sup_monoid.add_commute by auto 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" by (smt comp_associative comp_inf_covector inf.sup_monoid.add_assoc inf.sup_monoid.add_commute) 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" by (smt comp_inf_covector inf.sup_monoid.add_assoc inf.sup_monoid.add_commute mult_assoc) 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 by (simp add: inf.sup_monoid.add_commute) qed also have "... ≤ (v ⊓ -F * (F ⊓ v)⇧^{T}⇧^{⋆}) * (F ⊓ v)⇧^{⋆}" by (metis dedekind_2 conv_star_commute inf.sup_monoid.add_commute) also have "... ≤ (v ⊓ -F * 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" by (simp add: inf.sup_monoid.add_assoc) hence x_below_a: "sum (?x ⊓ g) ≤ sum (a ⊓ g)" using 65 bf_between_arcs_def assms(7, 13) by blast have "sum (?e ⊓ g) ≤ sum (?x ⊓ g)" proof (rule sum_e_below_sum_x_when_outgoing_same_component) show "symmetric g" using assms(1) by auto next show "vector j" using assms(3) by blast next show "forest h" by (simp add: assms(4)) next show "?x ≤ - ?H ⊓ -- g" proof - have 67: "?x ≤ - ?H" using 66 assms(5) big_forest_def order_lesseq_imp by blast have "?x ≤ d" by (simp add: conv_isotone inf.sup_monoid.add_assoc) also have "... ≤ f ⊔ 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"