Theory Boruvka
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
Aggregation_Algebras.M_Choose_Component
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
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 forest_modulo_equivalence_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 order.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
subsection ‹Forests modulo an equivalence›
text ‹
In the graphical interpretation, the arcs of d are directed towards the root(s) of the ‹forest_modulo_equivalence›.
›
definition "forest_modulo_equivalence x d ≡ equivalence x ∧ univalent (x * d) ∧ x ⊓ d * d⇧T ≤ 1 ∧ (x * d)⇧+ ⊓ x ≤ bot"
definition "forest_modulo_equivalence_path a b H d ≡ arc a ∧ arc b ∧ a⇧T * top ≤ (H * d)⇧⋆ * H * b * top"
lemma d_separates_forest_modulo_equivalence_1:
assumes "forest_modulo_equivalence x d"
shows "x * d ≤ -x"
proof -
have "x * d ≤ (x * d)⇧+"
using star.circ_mult_increasing by simp
also have "... ≤ -x"
using assms(1) forest_modulo_equivalence_def le_bot pseudo_complement by blast
finally show ?thesis
by simp
qed
lemma d_separates_forest_modulo_equivalence_2:
shows "forest_modulo_equivalence x d ⟹ d * x ≤ -x"
using forest_modulo_equivalence_def schroeder_6_p d_separates_forest_modulo_equivalence_1 by metis
lemma d_separates_forest_modulo_equivalence_3:
assumes "forest_modulo_equivalence x d"
shows "d ≤ -x"
proof -
have "1 ≤ x"
using assms(1) forest_modulo_equivalence_def by auto
then have "d ≤ x * d"
using mult_left_isotone by fastforce
also have "... ≤ (x * d)⇧+"
using star.circ_mult_increasing by simp
also have "... ≤ -x"
using assms(1) forest_modulo_equivalence_def le_bot pseudo_complement by blast
finally show ?thesis
by simp
qed
lemma d_separates_forest_modulo_equivalence_4:
shows "forest_modulo_equivalence x d ⟹ d⇧T ≤ -x"
using d_separates_forest_modulo_equivalence_3 forest_modulo_equivalence_def conv_isotone symmetric_complement_closed by metis
lemma d_separates_forest_modulo_equivalence_5:
shows "forest_modulo_equivalence x d ⟹ d ⊔ d⇧T ≤ -x"
using d_separates_forest_modulo_equivalence_3 d_separates_forest_modulo_equivalence_4 sup_least by blast
lemma d_separates_forest_modulo_equivalence_6:
shows "forest_modulo_equivalence x d ⟹ d * x ⊔ x * d ≤ -x"
using d_separates_forest_modulo_equivalence_1 d_separates_forest_modulo_equivalence_2 sup_least by blast
lemma d_separates_forest_modulo_equivalence_7:
shows "forest_modulo_equivalence x d ⟹ x * (d ⊔ d⇧T) * x ≤ -x"
using d_separates_forest_modulo_equivalence_5 forest_modulo_equivalence_def inf.sup_monoid.add_commute preorder_idempotent pseudo_complement triple_schroeder_p by metis
lemma d_separates_forest_modulo_equivalence_8:
shows "forest_modulo_equivalence x d ⟹ (d * x)⇧T ≤ -x"
using d_separates_forest_modulo_equivalence_2 forest_modulo_equivalence_def conv_isotone symmetric_complement_closed by metis
lemma d_separates_forest_modulo_equivalence_9:
shows "forest_modulo_equivalence x d ⟹ (x * d)⇧T ≤ -x"
by (metis d_separates_forest_modulo_equivalence_1 forest_modulo_equivalence_def conv_isotone symmetric_complement_closed)
lemma d_separates_forest_modulo_equivalence_10:
shows "forest_modulo_equivalence x d ⟹ (d * x)⇧+ ≤ -x"
using forest_modulo_equivalence_def le_bot pseudo_complement schroeder_5_p star_slide mult_assoc by metis
lemma d_separates_forest_modulo_equivalence_11:
shows "forest_modulo_equivalence x d ⟹ (x * d)⇧+ ≤ -x"
using forest_modulo_equivalence_def le_bot pseudo_complement by blast
lemma d_separates_forest_modulo_equivalence_12:
shows "forest_modulo_equivalence x d ⟹ (d * x)⇧T⇧+ ≤ -x"
using d_separates_forest_modulo_equivalence_10 forest_modulo_equivalence_def conv_isotone conv_plus_commute symmetric_complement_closed by metis
lemma d_separates_x_in_forest_13:
shows "forest_modulo_equivalence x d ⟹ (x * d)⇧T⇧+ ≤ -x"
using d_separates_forest_modulo_equivalence_11 forest_modulo_equivalence_def conv_isotone conv_plus_commute symmetric_complement_closed by metis
lemma irreflexive_d_in_forest_modulo_equivalence:
shows "forest_modulo_equivalence x d ⟹ irreflexive d"
by (metis d_separates_forest_modulo_equivalence_3 forest_modulo_equivalence_def inf.cobounded2 inf.left_commute inf.orderE pseudo_complement)
lemma univalent_d_in_forest_modulo_equivalence:
assumes "forest_modulo_equivalence x d"
shows "univalent d"
proof -
have "d⇧T * d ≤ d⇧T * x⇧T * x * d"
using assms(1) forest_modulo_equivalence_def comp_isotone comp_right_one mult_sub_right_one by metis
also have "... ≤ 1"
using assms(1) forest_modulo_equivalence_def comp_associative conv_dist_comp by auto
finally show ?thesis
by simp
qed
lemma acyclic_d_in_forest_modulo_equivalence:
assumes "forest_modulo_equivalence x d"
shows "acyclic d"
proof -
have "d⇧⋆ ≤ (x * d)⇧⋆"
using assms(1) forest_modulo_equivalence_def mult_left_isotone star.circ_circ_mult star.circ_circ_mult_1 star.circ_extra_circ star.left_plus_circ star_involutive star_isotone star_one star_slide mult_assoc by metis
then have "d * d⇧⋆ ≤ d * (x * d)⇧⋆"
using mult_right_isotone by blast
also have "... ≤ x * d * (x * d)⇧⋆"
using assms(1) forest_modulo_equivalence_def eq_refl inf.order_trans mult_isotone star.circ_circ_mult_1 star_involutive star_one star_outer_increasing mult_assoc by metis
also have "... ≤ -x"
using assms d_separates_forest_modulo_equivalence_11 by blast
also have "... ≤ -1"
using assms(1) forest_modulo_equivalence_def p_antitone by blast
finally show ?thesis
by simp
qed
lemma acyclic_dt_d_in_forest_modulo_equivalence:
shows "forest_modulo_equivalence x d ⟹ acyclic (d⇧T)"
using acyclic_d_in_forest_modulo_equivalence conv_plus_commute irreflexive_conv_closed by fastforce
lemma dt_forest_modulo_equivalence_forest:
shows "forest_modulo_equivalence x d ⟹ forest (d⇧T)"
using acyclic_dt_d_in_forest_modulo_equivalence univalent_d_in_forest_modulo_equivalence by simp
lemma var_forest_modulo_equivalence_axiom:
shows "forest_modulo_equivalence x d ⟹ d⇧T * x * d ≤ 1"
using forest_modulo_equivalence_def comp_associative conv_dist_comp preorder_idempotent by metis
lemma forest_modulo_equivalence_wcc:
assumes "forest_modulo_equivalence x d"
shows "(x * d)⇧⋆ * (x * d)⇧T⇧⋆ = ((x * d) ⊔ (x * d)⇧T)⇧⋆"
using assms(1) forest_modulo_equivalence_def fc_wcc by force
lemma forest_modulo_equivalence_direction_1:
assumes "forest_modulo_equivalence x d"
shows "(x * d)⇧⋆ ⊓ (x * d)⇧T = bot"
using assms(1) d_separates_forest_modulo_equivalence_11 forest_modulo_equivalence_def acyclic_star_below_complement_1 order_lesseq_imp p_antitone_iff by meson
lemma forest_modulo_equivalence_direction_2:
assumes "forest_modulo_equivalence x d"
shows "(x * d)⇧T⇧⋆ ⊓ (x * d) ≤ bot"
using assms(1) forest_modulo_equivalence_direction_1 comp_inf.idempotent_bot_closed conv_inf_bot_iff conv_star_commute inf.sup_left_divisibility by metis
lemma forest_modulo_equivalence_separate:
assumes "forest_modulo_equivalence x d"
shows "(x * d)⇧⋆ * (x * d)⇧T⇧⋆ ⊓ (x * d)⇧T * (x * d) ≤ 1"
proof -
have "(x * d)⇧⋆ ⊓ (x * d)⇧T * (x * d) = (1 ⊔ (x * d)⇧+) ⊓ (x * d)⇧T * (x * d)"
using star_left_unfold_equal by simp
also have "... = (1 ⊓ (x * d)⇧T * (x * d)) ⊔ ((x * d)⇧+ ⊓ (x * d)⇧T * (x * d))"
using comp_inf.semiring.distrib_right by simp
also have "... ≤ 1 ⊔ ((x * d)⇧+ ⊓ (x * d)⇧T * (x * d))"
using inf.cobounded1 semiring.add_right_mono by blast
also have "... = 1 ⊔ ((x * d)⇧⋆ ⊓ (x * d)⇧T) * (x * d)"
using assms(1) forest_modulo_equivalence_def forest_modulo_equivalence_direction_1 comp_inf.semiring.mult_zero_right inf.sup_left_divisibility le_infI2 semiring.mult_not_zero sup.orderE by metis
also have "... ≤ 1 ⊔ bot"
using assms(1) forest_modulo_equivalence_direction_1 by simp
finally have 2: "(x * d)⇧⋆ ⊓ (x * d)⇧T * (x * d) ≤ 1"
by simp
then have 3: "(x * d)⇧T⇧⋆ ⊓ (x * d)⇧T * (x * d) ≤ 1"
using assms(1) forest_modulo_equivalence_def conv_dist_comp conv_dist_inf conv_involutive conv_star_commute coreflexive_symmetric by metis
have "((x * d)⇧⋆ ⊔ (x * d)⇧T⇧⋆) ⊓ ((x * d)⇧T * (x * d)) ≤ 1"
using 2 3 inf_sup_distrib2 by simp
thus ?thesis
using assms(1) le_infI2 forest_modulo_equivalence_def by blast
qed
lemma forest_modulo_equivalence_path_trans_closure:
assumes "forest_modulo_equivalence x d"
shows "(x * d⇧T)⇧+ * x * d * x * d⇧T ≤ (x * d⇧T)⇧+"
proof -
have "(x * d⇧T)⇧+ * x * d * x * d⇧T = (x * d⇧T)⇧⋆ * x * d⇧T * x * d * x * d⇧T"
using comp_associative star.circ_plus_same by metis
also have "... ≤ (x * d⇧T)⇧⋆ * x * 1 * x * d⇧T"
using assms(1) forest_modulo_equivalence_def var_forest_modulo_equivalence_axiom comp_associative mult_left_isotone mult_right_isotone by metis
also have "... ≤ (x * d⇧T)⇧⋆ * x * d⇧T"
using assms(1) forest_modulo_equivalence_def by (simp add: preorder_idempotent mult_assoc)
finally show ?thesis
using star.circ_plus_same mult_assoc by simp
qed
text ‹
The ‹forest_modulo_equivalence› structure is preserved if d is decreased.
›
lemma forest_modulo_equivalence_decrease_d:
assumes "forest_modulo_equivalence x d"
shows "forest_modulo_equivalence x (d ⊓ c)"
proof (unfold forest_modulo_equivalence_def, intro conjI)
show "reflexive x"
using assms(1) forest_modulo_equivalence_def by blast
next
show "transitive x"
using assms(1) forest_modulo_equivalence_def by blast
next
show "symmetric x"
using assms(1) forest_modulo_equivalence_def by blast
next
show "univalent (x * (d ⊓ c))"
proof -
have "(x * (d ⊓ c))⇧T * x * (d ⊓ c) ≤ (x * d)⇧T * x * d"
using conv_order mult_isotone by auto
also have "... ≤ 1"
using assms(1) forest_modulo_equivalence_def mult_assoc by auto
finally show ?thesis
using mult_assoc by auto
qed
next
show "coreflexive (x ⊓ ((d ⊓ c) * (d ⊓ c)⇧T))"
proof -
have "x ⊓ (d ⊓ c) * (d ⊓ c)⇧T ≤ x ⊓ d * d⇧T"
using conv_dist_inf inf.sup_right_isotone mult_isotone by auto
thus ?thesis
using assms(1) forest_modulo_equivalence_def order_lesseq_imp by blast
qed
next
show "(x * (d ⊓ c))⇧+ ⊓ x ≤ bot"
proof -
have "(x * (d ⊓ c))⇧+ ≤ (x * d)⇧+"
using comp_isotone star_isotone by simp
thus ?thesis
using assms d_separates_forest_modulo_equivalence_11 dual_order.eq_iff dual_order.trans pseudo_complement by blast
qed
qed
lemma expand_forest_modulo_equivalence:
assumes "forest_modulo_equivalence H d"
shows "(d⇧T * H)⇧⋆ * (H * d)⇧⋆ = (d⇧T * H)⇧⋆ ⊔ (H * d)⇧⋆"
proof -
have "(H * d)⇧T * H * d ≤ 1"
using assms forest_modulo_equivalence_def mult_assoc by auto
hence "d⇧T * H * H * d ≤ 1"
using assms forest_modulo_equivalence_def conv_dist_comp by auto
thus ?thesis
by (simp add: cancel_separate_eq comp_associative)
qed
lemma forest_modulo_equivalence_path_bot:
assumes "arc a"
and "a ≤ d"
and "forest_modulo_equivalence H d"
shows "(d ⊓ - a)⇧T * (H * a * top) ≤ bot"
proof -
have 1: "d⇧T * H * d ≤ 1"
using assms(3) forest_modulo_equivalence_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) forest_modulo_equivalence_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 forest_modulo_equivalence_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) forest_modulo_equivalence_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 forest_modulo_equivalence_path_split_2:
assumes "arc a"
and "a ≤ d"
and "forest_modulo_equivalence 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) forest_modulo_equivalence_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) forest_modulo_equivalence_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) forest_modulo_equivalence_def star_slide mult_assoc preorder_idempotent)
also have "... = H * ((d ⊓ - a) * H)⇧⋆ * H * a * top"
using assms(3) forest_modulo_equivalence_def preorder_idempotent by fastforce
finally show ?thesis
by (metis assms(3) forest_modulo_equivalence_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 ‹
This section has been moved to theories ‹Stone_Relation_Algebras.Choose_Component› and ‹Aggregation_Algebras.M_Choose_Component›.
›
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.
›
context m_kleene_algebra_choose_component
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
∧ regular d
∧ regular j ∧ vector j
∧ regular h ∧ forest h
∧ forest_components h * j = j
∧ forest_modulo_equivalence (forest_components h) d
∧ d * top ≤ - j
∧ f ⊔ f⇧T = h ⊔ h⇧T ⊔ d ⊔ d⇧T
∧ (∀ a b . forest_modulo_equivalence_path a b (forest_components h) d ∧ a ≤ -(forest_components h) ⊓ -- g ∧ b ≤ d ⟶ sum(b ⊓ g) ≤ sum(a ⊓ g))"
lemma F_is_H_and_d:
assumes "f ⊔ f⇧T = h ⊔ h⇧T ⊔ d ⊔ d⇧T"
and "injective f"
and "injective h"
shows "forest_components f = (forest_components h * (d ⊔ d⇧T))⇧⋆ * forest_components h"
proof -
have "forest_components f = (f ⊔ f⇧T)⇧⋆"
using assms(2) cancel_separate_1 by simp
also have "... = (h ⊔ h⇧T ⊔ d ⊔ d⇧T)⇧⋆"
using assms(1) by auto
also have "... = ((h ⊔ h⇧T)⇧⋆ * (d ⊔ d⇧T))⇧⋆ * (h ⊔ h⇧T)⇧⋆"
using star.circ_sup_9 sup_assoc by metis
also have "... = (forest_components h * (d ⊔ d⇧T))⇧⋆ * forest_components h"
using assms(3) forest_components_wcc by simp
finally show ?thesis
by simp
qed
lemma H_below_F:
assumes "f ⊔ f⇧T = h ⊔ h⇧T ⊔ d ⊔ d⇧T"
and "injective f"
and "injective h"
shows "forest_components h ≤ forest_components f"
using assms(1, 2, 3) cancel_separate_1 dual_order.trans star.circ_sub_dist by metis
lemma H_below_regular_g:
assumes "f ⊔ f⇧T = h ⊔ h⇧T ⊔ d ⊔ d⇧T"
and "f ≤ --g"
and "symmetric g"
shows "h ≤ --g"
proof -
have "h ≤ f ⊔ f⇧T"
using assms(1) sup_assoc by simp
also have "... ≤ --g"
using assms(2, 3) conv_complement conv_isotone by fastforce
finally show ?thesis
using order_trans by blast
qed
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 ‹
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 forests modulo an equivalence›
text ‹
We prove a number of properties about ‹forest_modulo_equivalence› 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 ‹
There is a path in the ‹forest_modulo_equivalence› between edges $a$ and $b$ if and only if there is either a path in the ‹forest_modulo_equivalence› from $a$ to $b$ or one from $a$ to $c$ and one from $c$ to $b$.
›
lemma forest_modulo_equivalence_path_split_disj:
assumes "equivalence H"
and "arc c"
and "regular a ∧ regular b ∧ regular c ∧ regular d ∧ regular H"
shows "forest_modulo_equivalence_path a b H (d ⊔ c) ⟷ forest_modulo_equivalence_path a b H d ∨ (forest_modulo_equivalence_path a c H d ∧ forest_modulo_equivalence_path c b H d)"
proof -
have 1: "forest_modulo_equivalence_path a b H (d ⊔ c) ⟶ forest_modulo_equivalence_path a b H d ∨ (forest_modulo_equivalence_path a c H d ∧ forest_modulo_equivalence_path c b H d)"
proof (rule impI)
assume 11: "forest_modulo_equivalence_path a b H (d ⊔ c)"
hence "a⇧T * top ≤ (H * (d ⊔ c))⇧⋆ * H * b * top"
by (simp add: forest_modulo_equivalence_path_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 forest_modulo_equivalence_path_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 "forest_modulo_equivalence_path a b H d ∨ (forest_modulo_equivalence_path a c H d ∧ forest_modulo_equivalence_path 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 "forest_modulo_equivalence_path a b H d"
using 11 forest_modulo_equivalence_path_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 "forest_modulo_equivalence_path a c H d ∧ forest_modulo_equivalence_path c b H d"
using 11 15 assms(2) forest_modulo_equivalence_path_def by auto
thus ?thesis
by simp
qed
qed
have 2: "forest_modulo_equivalence_path a b H d ∨ (forest_modulo_equivalence_path a c H d ∧ forest_modulo_equivalence_path c b H d) ⟶ forest_modulo_equivalence_path a b H (d ⊔ c)"
proof -
have 21: "forest_modulo_equivalence_path a b H d ⟶ forest_modulo_equivalence_path a b H (d ⊔ c)"
proof (rule impI)
assume 22:"forest_modulo_equivalence_path a b H d"
hence "a⇧T * top ≤ (H * d)⇧⋆ * H * b * top"
using forest_modulo_equivalence_path_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 "forest_modulo_equivalence_path a b H (d ⊔ c)"
using 22 forest_modulo_equivalence_path_def by blast
qed
have "forest_modulo_equivalence_path a c H d ∧ forest_modulo_equivalence_path c b H d ⟶ forest_modulo_equivalence_path a b H (d ⊔ c)"
proof (rule impI)
assume 23: "forest_modulo_equivalence_path a c H d ∧ forest_modulo_equivalence_path c b H d"
hence "a⇧T * top ≤ (H * d)⇧⋆ * H * c * top"
using forest_modulo_equivalence_path_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: forest_modulo_equivalence_path_def)
also have "... ≤ (H * d)⇧⋆ * H * b * top ⊔ (H * d)⇧⋆ * H * c * (H * d)⇧⋆ * H * b * top"
by (simp add: forest_modulo_equivalence_path_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 "forest_modulo_equivalence_path a b H (d ⊔ c)"
using 23 forest_modulo_equivalence_path_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 forest_modulo_equivalence_d_U_e:
assumes "forest f"
and "vector j"
and "regular j"
and "forest h"
and "forest_modulo_equivalence (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 "j ≠ bot"
shows "forest_modulo_equivalence (forest_components h) (d ⊔ selected_edge h j g)"
proof (cases "selected_edge h j g = bot")
let ?e = "selected_edge h j g"
case True
assume "?e = bot"
thus ?thesis
by (simp add: True assms(5))
next
let ?H = "forest_components h"
let ?F = "forest_components f"
let ?e = "selected_edge h j g"
let ?d' = "d ⊔ ?e"
case False
assume e_not_bot: "?e ≠ bot"
have "forest_modulo_equivalence (forest_components h) (d ⊔ selected_edge h j g)"
proof (unfold forest_modulo_equivalence_def, intro conjI)
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 "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 e_not_bot 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, 6, 7, 10) 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(5) dTransHd_le_1 forest_modulo_equivalence_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(5) forest_modulo_equivalence_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(6) conv_complement conv_isotone mult_right_isotone)
also have "... ≤ j * - j⇧T"
using assms(2, 3, 10) et_below_j mult_left_isotone by auto
also have "... ≤ - ?H"
using 03 by (metis assms(2, 3, 7) 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 e_not_bot 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 ≤ bot"
proof -
have 40: "(?H * d)⇧+ ≤ -?H"
using assms(5) forest_modulo_equivalence_def bot_unique pseudo_complement by blast
have "?e ≤ - ?F"
by (simp add: assms(9))
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"
using assms(1, 4, 8) H_below_F by blast
hence 46:"?H * ?e ≤ ?F * ?e"
by (simp add: mult_left_isotone)
have "d ≤ f ⊔ f⇧T"
using assms(8) 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) e_not_bot 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 e_not_bot 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 40 44 assms(5) sup.boundedI by blast
finally show ?thesis
using pseudo_complement by force
qed
qed
thus ?thesis
by blast
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 "forest_modulo_equivalence H d"
and "forest_modulo_equivalence_path 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) forest_modulo_equivalence_path_def by auto
have 3: "e * top * e⇧T ≤ 1"
using assms(2) forest_modulo_equivalence_path_def arc_expanded by blast
have 4: "top * ?x * top = top"
proof -
have "a⇧T * top ≤ (H * d)⇧⋆ * H * e * top"
using assms(2) forest_modulo_equivalence_path_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 forest_modulo_equivalence_path_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: forest_modulo_equivalence_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) forest_modulo_equivalence_path_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) forest_modulo_equivalence_def by auto
also have "... = H * (d ⊓ top * e⇧T * H)⇧T * H * (d⇧T * H)⇧⋆ * a⇧T * top"
using assms(1) forest_modulo_equivalence_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 forest_modulo_equivalence_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) forest_modulo_equivalence_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) forest_modulo_equivalence_path_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) forest_modulo_equivalence_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) forest_modulo_equivalence_def conv_dist_comp conv_star_commute schroeder_4_p star_slide)
hence "H * (d * H)⇧⋆ ≤ - d⇧T"
using 511 by (metis assms(1) forest_modulo_equivalence_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) forest_modulo_equivalence_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) forest_modulo_equivalence_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) forest_modulo_equivalence_def dTransHd_le_1 le_supI1 by blast
hence "(- 1 ⊓ H) * d⇧T * H ≤ - d⇧T"
by (metis assms(1) forest_modulo_equivalence_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) forest_modulo_equivalence_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) forest_modulo_equivalence_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) forest_modulo_equivalence_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) forest_modulo_equivalence_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) forest_modulo_equivalence_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) forest_modulo_equivalence_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) forest_modulo_equivalence_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) forest_modulo_equivalence_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_forest_modulo_equivalence 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) forest_modulo_equivalence_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) forest_modulo_equivalence_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) forest_modulo_equivalence_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) forest_modulo_equivalence_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) forest_modulo_equivalence_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) forest_modulo_equivalence_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) forest_modulo_equivalence_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) forest_modulo_equivalence_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) forest_modulo_equivalence_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_forest_modulo_equivalence)
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) forest_modulo_equivalence_def reflexive_inf_star by blast
have "H ⊓ (d⇧T * H)⇧⋆ = 1 ⊔ H ⊓ (d⇧T * H)⇧+"
using assms(1) forest_modulo_equivalence_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) forest_modulo_equivalence_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.
For example, Theorem ‹e_leq_c_c_complement_transpose_general› is used to show that the ‹selected_edge› has its source inside and its target outside the component it is chosen for.
›
lemma e_leq_c_c_complement_transpose_general:
assumes "e = minarc (v * -(v)⇧T ⊓ g)"
and "regular v"
shows "e ≤ v * -(v)⇧T"
proof -
have "e ≤ -- (v * - v⇧T ⊓ g)"
using assms(1) minarc_below order_trans by blast
also have "... ≤ -- (v * - v⇧T)"
using order_lesseq_imp pp_isotone_inf by blast
also have "... = v * - v⇧T"
using assms(2) regular_mult_closed by auto
finally show ?thesis
by simp
qed
lemma x_leq_c_transpose_general:
assumes "vector_classes x v"
and "a⇧T * top ≤ x * e * top"
and "e ≤ v * -v⇧T"
shows "a ≤ v⇧T"
proof -
have 1: "equivalence x"
using assms(1) using vector_classes_def by blast
have "a ≤ top * a"
using top_left_mult_increasing by blast
also have "... ≤ (x * e * top)⇧T"
using assms(2) conv_dist_comp conv_isotone by fastforce
also have "... = top * e⇧T * x"
using 1 by (simp add: conv_dist_comp mult_assoc)
also have "... ≤ top * (v * - v⇧T)⇧T * x"
by (metis assms(3) conv_dist_comp conv_isotone mult_left_isotone symmetric_top_closed)
also have "... = top * (- v * v⇧T) * x"
by (simp add: conv_complement conv_dist_comp)
also have "... ≤ top * v⇧T * x"
by (metis mult_left_isotone top.extremum mult_assoc)
also have "... = v⇧T * x"
using assms(1) vector_classes_def vector_conv_covector by auto
also have "... = v⇧T"
by (metis assms(1) order.antisym conv_dist_comp conv_order dual_order.trans mult_right_isotone mult_sub_right_one vector_classes_def)
finally show ?thesis
by simp
qed
lemma x_leq_c_complement_general:
assumes "vector v"
and "v * v⇧T ≤ x"
and "a ≤ v⇧T"
and "a ≤ -x"
shows "a ≤ -v"
proof -
have "a ≤ -x ⊓ v⇧T"
using assms(3, 4) by auto
also have "... ≤ - v"
proof -
have "v ⊓ v⇧T ≤ x"
using assms(1, 2) vector_covector by auto
hence "-x ⊓ v ⊓ v⇧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
lemma sum_e_below_sum_a_when_outgoing_same_component_general:
assumes "e = minarc (v * -(v)⇧T ⊓ g)"
and "symmetric g"
and "arc a"
and "a ≤ -x ⊓ -- g"
and "a⇧T * top ≤ x * e * top"
and "unique_vector_class x v"
shows "sum (e ⊓ g) ≤ sum (a ⊓ g)"
proof -
have 1:"e ≤ v * - v⇧T"
using assms(1, 6) e_leq_c_c_complement_transpose_general unique_vector_class_def vector_classes_def by auto
have 2: "a ≤ v⇧T"
using 1 assms(5) assms(6) x_leq_c_transpose_general unique_vector_class_def by blast
hence "a ≤ -v"
using assms(4, 6) inf.boundedE unique_vector_class_def vector_classes_def x_leq_c_complement_general by meson
hence "a ≤ - v ⊓ v⇧T"
using 2 by simp
hence "a ≤ - v * v⇧T"
using assms(6) vector_complement_closed vector_covector unique_vector_class_def vector_classes_def by metis
hence "a⇧T ≤ v⇧T⇧T * - v⇧T"
using conv_complement conv_dist_comp conv_isotone by metis
hence 3: "a⇧T ≤ v * - v⇧T"
by simp
hence "a ≤ -- g"
using assms(4) by auto
hence "a⇧T ≤ -- g"
using assms(2) conv_complement conv_isotone by fastforce
hence "a⇧T ⊓ v * - v⇧T ⊓ -- g ≠ bot"
using 3 assms(3, 6) inf.orderE semiring.mult_not_zero unique_vector_class_def vector_classes_def by metis
hence "a⇧T ⊓ v * - v⇧T ⊓ g ≠ bot"
using inf.sup_monoid.add_commute pp_inf_bot_iff by auto
hence "sum (minarc (v * - v⇧T ⊓ g) ⊓ (v * - v⇧T ⊓ g)) ≤ sum (a⇧T ⊓ v * - v⇧T ⊓ g)"
using assms(3) minarc_min inf.sup_monoid.add_assoc by simp
hence "sum (e ⊓ v * - v⇧T ⊓ g) ≤ sum (a⇧T ⊓ v * - v⇧T ⊓ g)"
using assms(1, 6) inf.sup_monoid.add_assoc by simp
hence "sum (e ⊓ g) ≤ sum (a⇧T ⊓ g)"
using 1 3 by (metis inf.orderE)
hence "sum (e ⊓ g) ≤ sum (a ⊓ g)"
by (simp add: assms(2) sum_symmetric)
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 "regular 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_a_when_outgoing_same_component_general)
next
show "?e = minarc (?c * - ?c⇧T ⊓ g)"
by simp
next
show "symmetric g"
by (simp add: assms(1))
next
show "arc x"
by (simp add: assms(8))
next
show "x ≤ -?H ⊓ -- g"
using assms(5) by auto
next
show "x⇧T * top ≤ ?H * ?e * top"
by (simp add: assms(6))
next
show "unique_vector_class ?H ?c"
proof (unfold unique_vector_class_def, unfold vector_classes_def, intro conjI)
next
show "regular ?H"
by (metis assms(4) conv_complement pp_dist_star regular_mult_closed)
next
show "regular ?c"
using component_is_regular by auto
next
show "reflexive ?H"
using assms(3) forest_components_equivalence by blast
next
show "transitive ?H"
using assms(3) fch_equivalence by blast
next
show "symmetric ?H"
by (simp add: assms(3) fch_equivalence)
next
show "vector ?c"
by (simp add: assms(2, 6) component_is_vector)
next
show "?H * ?c ≤ ?c"
using component_single by auto
next
show "?c ≠ bot"
using assms(2, 6 , 7, 8) inf_bot_left le_bot minarc_bot mult_left_zero mult_right_zero by fastforce
next
show "?c * ?c⇧T ≤ ?H"
by (simp add: component_is_connected)
qed
qed
qed
text ‹
If there is a path in the ‹forest_modulo_equivalence› 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 ‹forest_modulo_equivalence_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_forest_modulo_equivalence:
assumes "symmetric g"
and "f ≤ --g"
and "vector j"
and "forest h"
and "forest_modulo_equivalence (forest_components h) d"
and "f ⊔ f⇧T = h ⊔ h⇧T ⊔ d ⊔ d⇧T"
and "(∀ a b . forest_modulo_equivalence_path 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 "forest_modulo_equivalence_path 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))
next
show "regular h"
using assms(14) by auto
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 "forest_modulo_equivalence ?H d"
by (simp add: assms(5))
next
show "forest_modulo_equivalence_path a ?e ?H d"
proof -
have 611: "forest_modulo_equivalence_path 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 forest_modulo_equivalence_path_def arc_regular by fastforce
thus ?thesis
using 616 by (smt forest_modulo_equivalence_path_split_disj assms(4, 8, 10, 12) forest_modulo_equivalence_path_def fch_equivalence minarc_regular regular_closed_star regular_conv_closed regular_mult_closed)
qed
next
show "(?H * d)⇧+ ≤ - ?H"
using assms(5) forest_modulo_equivalence_def le_bot pseudo_complement by blast
next
show "¬ a⇧T * top ≤ ?H * ?e * top"
by (simp add: False)
next
show "regular a"
using assms(12) forest_modulo_equivalence_path_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: "forest_modulo_equivalence_path a ?x ?H d"
using 61 assms(12) forest_modulo_equivalence_path_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 forest_modulo_equivalence_path_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"
proof -
have "?x ≤ d"
using 66 by blast
also have "... ≤ ?H * d"
using dual_order.trans star.circ_loop_fixpoint sup.cobounded2 mult_assoc by metis
also have "... ≤ (?H * d)⇧+"
using star.circ_mult_increasing by blast
also have "... ≤ - ?H"
using assms(5) bot_unique pseudo_complement forest_modulo_equivalence_def by blast
thus ?thesis
using calculation inf.order_trans by blast
qed
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
next
show "regular h"
using assms(14) by auto
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"
by simp
hence "i * top ≤ v⇧T⇧⋆ * e⇧T * top"
by (metis comp_associative mult_left_isotone vector_top_closed)
hence "e⇧T * top ≤ v⇧T⇧⋆⇧T * i * top"
using 2 by (metis bijective_reverse mult_assoc)
also have "... = v⇧⋆ * i * top"
by (simp add: conv_star_commute)
also have "... ≤ (v ⊓ -i ⊓ -i⇧T)⇧⋆ * i * top"
proof -
have 3: "i * top ≤ (v ⊓ -i ⊓ -i⇧T)⇧⋆ * i * top"
using star.circ_loop_fixpoint sup_right_divisibility mult_assoc by auto
have "(v ⊓ i) * (v ⊓ -i ⊓ -i⇧T)⇧⋆ * i * top ≤ i * top * i * top"
by (metis comp_isotone inf.cobounded1 inf.sup_monoid.add_commute mult_left_isotone top.extremum)
also have "... ≤ i * top"
by simp
finally have 4: "(v ⊓ i) * (v ⊓ -i ⊓ -i⇧T)⇧⋆ * i * top ≤ (v ⊓ -i ⊓ -i⇧T)⇧⋆ * i * top"
using 3 dual_order.trans by blast
have 5: "(v ⊓ -i ⊓ -i⇧T) * (v ⊓ -i ⊓ -i⇧T)⇧⋆ * i * top ≤ (v ⊓ -i ⊓ -i⇧T)⇧⋆ * i * top"
by (metis mult_left_isotone star.circ_increasing star.left_plus_circ)
have "v⇧+ ≤ -1"
by (simp add: assms(1))
hence "v * v ≤ -1"
by (metis mult_left_isotone order_trans star.circ_increasing star.circ_plus_same)
hence "v * 1 ≤ -v⇧T"
by (simp add: schroeder_5_p)
hence "v ≤ -v⇧T"
by simp
hence "v ⊓ v⇧T ≤ bot"
by (simp add: bot_unique pseudo_complement)
hence 7: "v ⊓ i⇧T ≤ bot"
by (metis assms(3) comp_inf.mult_right_isotone conv_dist_inf inf.boundedE inf.le_iff_sup le_bot)
hence "(v ⊓ i⇧T) * (v ⊓ -i ⊓ -i⇧T)⇧⋆ * i * top ≤ bot"
using le_bot semiring.mult_zero_left by fastforce
hence 6: "(v ⊓ i⇧T) * (v ⊓ -i ⊓ -i⇧T)⇧⋆ * i * top ≤ (v ⊓ -i ⊓ -i⇧T)⇧⋆ * i * top"
using bot_least le_bot by blast
have 8: "v = (v ⊓ i) ⊔ (v ⊓ i⇧T) ⊔ (v ⊓ -i ⊓ -i⇧T)"
proof -
have 81: "regular i"
by (simp add: assms(4) arc_regular)
have "(v ⊓ i⇧T) ⊔ (v ⊓ -i ⊓ -i⇧T) = (v ⊓ -i)"
using 7 by (metis comp_inf.coreflexive_comp_inf_complement inf_import_p inf_p le_bot maddux_3_11_pp top.extremum)
hence "(v ⊓ i) ⊔ (v ⊓ i⇧T) ⊔ (v ⊓ -i ⊓ -i⇧T) = (v ⊓ i) ⊔ (v ⊓ -i)"
by (simp add: sup.semigroup_axioms semigroup.assoc)
also have "... = v"
using 81 by (metis maddux_3_11_pp)
finally show ?thesis
by simp
qed
have "(v ⊓ i) * (v ⊓ -i ⊓ -i⇧T)⇧⋆ * i * top ⊔ (v ⊓ i⇧T) * (v ⊓ -i ⊓ -i⇧T)⇧⋆ * i * top ⊔ (v ⊓ -i ⊓ -i⇧T) * (v ⊓ -i ⊓ -i⇧T)⇧⋆ * i * top ≤ (v ⊓ -i ⊓ -i⇧T)⇧⋆ * i * top"
using 4 5 6 by simp
hence "((v ⊓ i) ⊔ (v ⊓ i⇧T) ⊔ (v ⊓ -i ⊓ -i⇧T)) * (v ⊓ -i ⊓ -i⇧T)⇧⋆ * i * top ≤ (v ⊓ -i ⊓ -i⇧T)⇧⋆ * i * top"
by (simp add: mult_right_dist_sup)
hence "v * (v ⊓ -i ⊓ -i⇧T)⇧⋆ * i * top ≤ (v ⊓ -i ⊓ -i⇧T)⇧⋆ * i * top"
using 8 by auto
hence "i * top ⊔ v * (v ⊓ -i ⊓ -i⇧T)⇧⋆ * i * top ≤ (v ⊓ -i ⊓ -i⇧T)⇧⋆ * i * top"
using 3 by auto
hence 9:"v⇧⋆ * (v ⊓ -i ⊓ -i⇧T)⇧⋆ * i * top ≤ (v ⊓ -i ⊓ -i⇧T)⇧⋆ * i * top"
by (simp add: star_left_induct_mult mult_assoc)
have "v⇧⋆ * i * top ≤ v⇧⋆ * (v ⊓ -i ⊓ -i⇧T)⇧⋆ * i * top"
using 3 mult_right_isotone mult_assoc by auto
thus ?thesis
using 9 order.trans by blast
qed
finally have "e⇧T * top ≤ (v ⊓ -i ⊓ -i⇧T)⇧⋆ * i * top"
by simp
hence "i * top ≤ (v ⊓ -i ⊓ -i⇧T)⇧⋆⇧T * e⇧T * top"
using 2 by (metis bijective_reverse mult_assoc)
also have "... = (v⇧T ⊓ -i ⊓ -i⇧T)⇧⋆ * e⇧T * top"
using comp_inf.inf_vector_comp conv_complement conv_dist_inf conv_star_commute inf.sup_monoid.add_commute by auto
also have "... ≤ ((v ⊓ -i ⊓ -i⇧T) ⊔ (v⇧T ⊓ -i ⊓ -i⇧T))⇧⋆ * e⇧T * top"
by (simp add: mult_left_isotone star_isotone)
finally have "i ≤ ((v⇧T ⊓ -i ⊓ -i⇧T) ⊔ (v ⊓ -i ⊓ -i⇧T))⇧⋆ * e⇧T * top"
using dual_order.trans top_right_mult_increasing sup_commute by auto
also have "... = (v⇧T ⊓ -i ⊓ -i⇧T)⇧⋆ * (v ⊓ -i ⊓ -i⇧T)⇧⋆ * e⇧T * top"
using 1 cancel_separate_1 by (simp add: sup_commute)
also have "... ≤ (v⇧T ⊓ -i ⊓ -i⇧T)⇧⋆ * v⇧⋆ * e⇧T * top"
by (simp add: inf_assoc mult_left_isotone mult_right_isotone star_isotone)
also have "... = (v⇧T ⊓ -i ⊓ -i⇧T)⇧⋆ * e⇧T * top"
using assms(2) mult_assoc by simp
also have "... ≤ (v⇧T ⊓ -i⇧T)⇧⋆ * e⇧T * top"
by (metis mult_left_isotone star_isotone inf.cobounded2 inf.left_commute inf.sup_monoid.add_commute)
also have "... = (v ⊓ -i)⇧T⇧⋆ * e⇧T * top"
using conv_complement conv_dist_inf by auto
finally show ?thesis
by simp
qed
lemma exists_a_w:
assumes "symmetric g"
and "forest f"
and "f ≤ --g"
and "regular f"
and "(∃w . minimum_spanning_forest w g ∧ f ≤ w ⊔ w⇧T)"
and "vector j"
and "regular j"
and "forest h"
and "forest_modulo_equivalence (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 "(∀ a b . forest_modulo_equivalence_path a b (forest_components h) d ∧ a ≤ -(forest_components h) ⊓ -- g ∧ b ≤ d ⟶ sum(b ⊓ g) ≤ sum(a ⊓ g))"
and "regular d"
and "selected_edge h j g ≤ - forest_components f"
and "selected_edge h j g ≠ bot"
and "j ≠ bot"
and "regular h"
and "h ≤ --g"
shows "∃w. minimum_spanning_forest w g ∧
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) ≤ w ⊔ w⇧T"
proof -
let ?p = "path f h j g"
let ?e = "selected_edge h j g"
let ?f = "(f ⊓ -?e⇧T ⊓ -?p) ⊔ (f ⊓ -?e⇧T ⊓ ?p)⇧T ⊔ ?e"
let ?F = "forest_components f"
let ?H = "forest_components h"
let ?ec = "choose_component (forest_components h) j * - choose_component (forest_components h) j⇧T ⊓ g"
from assms(4) obtain w where 2: "minimum_spanning_forest w g ∧ f ≤ w ⊔ w⇧T"
using assms(5) by blast
hence 3: "regular w ∧ regular f ∧ regular ?e"
by (metis assms(4) minarc_regular minimum_spanning_forest_def spanning_forest_def)
have 5: "equivalence ?F"
using assms(2) forest_components_equivalence by auto
have "?e⇧T * top * ?e⇧T = ?e⇧T"
by (metis arc_conv_closed arc_top_arc coreflexive_bot_closed coreflexive_symmetric minarc_arc minarc_bot_iff semiring.mult_not_zero)
hence "?e⇧T * top * ?e⇧T ≤ -?F"
using 5 assms(15) conv_complement conv_isotone by fastforce
hence 6: "?e * ?F * ?e = bot"
using assms(2) le_bot triple_schroeder_p by simp
let ?q = "w ⊓ top * ?e * w⇧T⇧⋆"
let ?v = "(w ⊓ -(top * ?e * w⇧T⇧⋆)) ⊔ ?q⇧T"
have 7: "regular ?q"
using 3 regular_closed_star regular_conv_closed regular_mult_closed by auto
have 8: "injective ?v"
proof (rule kruskal_exchange_injective_inv_1)
show "injective w"
using 2 minimum_spanning_forest_def spanning_forest_def by blast
next
show "covector (top * ?e * w⇧T⇧⋆)"
by (simp add: covector_mult_closed)
next
show "top * ?e * w⇧T⇧⋆ * w⇧T ≤ top * ?e * w⇧T⇧⋆"
by (simp add: mult_right_isotone star.right_plus_below_circ mult_assoc)
next
show "coreflexive ((top * ?e * w⇧T⇧⋆)⇧T * (top * ?e * w⇧T⇧⋆) ⊓ w⇧T * w)"
using 2 by (metis comp_inf.semiring.mult_not_zero forest_bot kruskal_injective_inv_3 minarc_arc minarc_bot_iff minimum_spanning_forest_def semiring.mult_not_zero spanning_forest_def)
qed
have 9: "components g ≤ forest_components ?v"
proof (rule kruskal_exchange_spanning_inv_1)
show "injective (w ⊓ - (top *?e * w⇧T⇧⋆) ⊔ (w ⊓ top * ?e * w⇧T⇧⋆)⇧T)"
using 8 by simp
next
show "regular (w ⊓ top * ?e * w⇧T⇧⋆)"
using 7 by simp
next
show "components g ≤ forest_components w"
using 2 minimum_spanning_forest_def spanning_forest_def by blast
qed
have 10: "spanning_forest ?v g"
proof (unfold spanning_forest_def, intro conjI)
show "injective ?v"
using 8 by auto
next
show "acyclic ?v"
proof (rule kruskal_exchange_acyclic_inv_1)
show "pd_kleene_allegory_class.acyclic w"
using 2 minimum_spanning_forest_def spanning_forest_def by blast
next
show "covector (top * ?e * w⇧T⇧⋆)"
by (simp add: covector_mult_closed)
qed
next
show "?v ≤ --g"
proof (rule sup_least)
show "w ⊓ - (top * ?e * w⇧T⇧⋆) ≤ - - g"
using 7 inf.coboundedI1 minimum_spanning_forest_def spanning_forest_def 2 by blast
next
show "(w ⊓ top * ?e * w⇧T⇧⋆)⇧T ≤ - - g"
using 2 by (metis assms(1) conv_complement conv_isotone inf.coboundedI1 minimum_spanning_forest_def spanning_forest_def)
qed
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 auto
qed
have 11: "sum (?v ⊓ g) = sum (w ⊓ g)"
proof -
have "sum (?v ⊓ g) = sum (w ⊓ -(top * ?e * w⇧T⇧⋆) ⊓ g) + sum (?q⇧T ⊓ g)"
using 2 by (smt 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 (?q ⊓ g)"
by (simp add: assms(1) sum_symmetric)
also have "... = sum (((w ⊓ -(top * ?e * w⇧T⇧⋆)) ⊔ ?q) ⊓ g)"
using inf_commute inf_left_commute sum_disjoint by simp
also have "... = sum (w ⊓ g)"
using 3 7 8 maddux_3_11_pp by auto
finally show ?thesis
by simp
qed
have 12: "?v ⊔ ?v⇧T = w ⊔ w⇧T"
proof -
have "?v ⊔ ?v⇧T = (w ⊓ -?q) ⊔ ?q⇧T ⊔ (w⇧T ⊓ -?q⇧T) ⊔ ?q"
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 auto
finally show ?thesis
by simp
qed
have 13: "?v * ?e⇧T = bot"
proof (rule kruskal_reroot_edge)
show "injective (?e⇧T * top)"
using assms(16) minarc_arc minarc_bot_iff by blast
next
show "pd_kleene_allegory_class.acyclic w"
using 2 minimum_spanning_forest_def spanning_forest_def by simp
qed
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 ?i = "?v ⊓ (- ?F) * ?e * top ⊓ top * ?e⇧T * ?F"
let ?w = "(?v ⊓ -?i) ⊔ ?e"
have 15: "regular ?i"
using 3 regular_closed_star regular_conv_closed regular_mult_closed by simp
have 16: "?F ≤ -?i"
proof -
have 161: "bijective (?e * top)"
using assms(16) minarc_arc minarc_bot_iff by auto
have "?i ≤ - ?F * ?e * top"
using inf.cobounded2 inf.coboundedI1 by blast
also have "... = - (?F * ?e * top)"
using 161 comp_bijective_complement by (simp add: mult_assoc)
finally have "?i ≤ - (?F * ?e * top)"
by blast
hence 162: "?i ⊓ ?F ≤ - (?F * ?e * top)"
using inf.coboundedI1 by blast
have "?i ⊓ ?F ≤ ?F ⊓ (top * ?e⇧T * ?F)"
by (meson inf_le1 inf_le2 le_infI order_trans)
also have "... ≤ ?F * (top * ?e⇧T * ?F)⇧T"
by (simp add: covector_mult_closed covector_restrict_comp_conv)
also have "... = ?F * ?F⇧T * ?e⇧T⇧T * top⇧T"
by (simp add: conv_dist_comp mult_assoc)
also have "... = ?F * ?F * ?e * top"
by (simp add: conv_dist_comp conv_star_commute)
also have "... = ?F * ?e * top"
by (simp add: 5 preorder_idempotent)
finally have "?i ⊓ ?F ≤ ?F * ?e * top"
by simp
hence "?i ⊓ ?F ≤ ?F * ?e * top ⊓ - (?F * ?e * top)"
using 162 inf.bounded_iff by blast
also have "... = bot"
by simp
finally show ?thesis
using le_bot p_antitone_iff pseudo_complement by blast
qed
have 17: "?i ≤ top * ?e⇧T * (?F ⊓ ?v ⊓ -?i)⇧T⇧⋆"
proof -
have "?i ≤ ?v ⊓ - ?F * ?e * top ⊓ top * ?e⇧T * (?F ⊓ ?v)⇧T⇧⋆ * (?F ⊓ ?v)⇧⋆"
using 2 8 12 by (smt inf.sup_right_isotone kruskal_forest_components_inf mult_right_isotone mult_assoc)
also have "... = ?v ⊓ - ?F * ?e * top ⊓ top * ?e⇧T * (?F ⊓ ?v)⇧T⇧⋆ * (1 ⊔ (?F ⊓ ?v)⇧⋆ * (?F ⊓ ?v))"
using star_left_unfold_equal star.circ_right_unfold_1 by auto
also have "... = ?v ⊓ - ?F * ?e * top ⊓ (top * ?e⇧T * (?F ⊓ ?v)⇧T⇧⋆ ⊔ top * ?e⇧T * (?F ⊓ ?v)⇧T⇧⋆ * (?F ⊓ ?v)⇧⋆ * (?F ⊓ ?v))"
by (simp add: mult_left_dist_sup mult_assoc)
also have "... = (?v ⊓ - ?F * ?e * top ⊓ top * ?e⇧T * (?F ⊓ ?v)⇧T⇧⋆) ⊔ (?v ⊓ - ?F * ?e * top ⊓ top * ?e⇧T * (?F ⊓ ?v)⇧T⇧⋆ * (?F ⊓ ?v)⇧⋆ * (?F ⊓ ?v))"
using comp_inf.semiring.distrib_left by blast
also have "... ≤ top * ?e⇧T * (?F ⊓ ?v)⇧T⇧⋆ ⊔ (?v ⊓ - ?F * ?e * top ⊓ top * ?e⇧T * (?F ⊓ ?v)⇧T⇧⋆ * (?F ⊓ ?v)⇧⋆ * (?F ⊓ ?v))"
using comp_inf.semiring.add_right_mono inf_le2 by blast
also have "... ≤ top * ?e⇧T * (?F ⊓ ?v)⇧T⇧⋆ ⊔ (?v ⊓ - ?F * ?e * top ⊓ top * ?e⇧T * (?F⇧T ⊓ ?v⇧T)⇧⋆ * (?F ⊓ ?v)⇧⋆ * (?F ⊓ ?v))"
by (simp add: conv_dist_inf)
also have "... ≤ top * ?e⇧T * (?F ⊓ ?v)⇧T⇧⋆ ⊔ (?v ⊓ - ?F * ?e * top ⊓ top * ?e⇧T * ?F⇧T⇧⋆ * ?F⇧⋆ * (?F ⊓ ?v))"
proof -
have "top * ?e⇧T * (?F⇧T ⊓ ?v⇧T)⇧⋆ * (?F ⊓ ?v)⇧⋆ * (?F ⊓ ?v) ≤ top * ?e⇧T * ?F⇧T⇧⋆ * ?F⇧⋆ * (?F ⊓ ?v)"
using star_isotone by (simp add: comp_isotone)
hence "?v ⊓ - ?F * ?e * top ⊓ top * ?e⇧T * (?F⇧T ⊓ ?v⇧T)⇧⋆ * (?F ⊓ ?v)⇧⋆ * (?F ⊓ ?v) ≤ ?v ⊓ - ?F * ?e * top ⊓ top * ?e⇧T * ?F⇧T⇧⋆ * ?F⇧⋆ * (?F ⊓ ?v)"
using inf.sup_right_isotone by blast
thus ?thesis
using sup_right_isotone by blast
qed
also have "... = top * ?e⇧T * (?F ⊓ ?v)⇧T⇧⋆ ⊔ (?v ⊓ - ?F * ?e * top ⊓ top * ?e⇧T * ?F⇧⋆ * ?F⇧⋆ * (?F ⊓ ?v))"
using 5 by auto
also have "... = top * ?e⇧T * (?F ⊓ ?v)⇧T⇧⋆ ⊔ (?v ⊓ - ?F * ?e * top ⊓ top * ?e⇧T * ?F * ?F * (?F ⊓ ?v))"
by (simp add: assms(2) forest_components_star)
also have "... = top * ?e⇧T * (?F ⊓ ?v)⇧T⇧⋆ ⊔ (?v ⊓ - ?F * ?e * top ⊓ top * ?e⇧T * ?F * (?F ⊓ ?v))"
using 5 mult.semigroup_axioms preorder_idempotent semigroup.assoc by fastforce
also have "... = top * ?e⇧T * (?F ⊓ ?v)⇧T⇧⋆"
proof -
have "?e * top * ?e⇧T ≤ 1"
using assms(16) arc_expanded minarc_arc minarc_bot_iff by auto
hence "?F * ?e * top * ?e⇧T ≤ ?F * 1"
by (metis comp_associative comp_isotone mult_semi_associative star.circ_transitive_equal)
hence "?v * ?v⇧T * ?F * ?e * top * ?e⇧T ≤ 1 * ?F * 1"
using 8 by (smt comp_isotone mult_assoc)
hence 171: "?v * ?v⇧T * ?F * ?e * top * ?e⇧T ≤ ?F"
by simp
hence "?v * (?F ⊓ ?v)⇧T * ?F * ?e * top * ?e⇧T ≤ ?F"
proof -
have "?v * (?F ⊓ ?v)⇧T * ?F * ?e * top * ?e⇧T ≤ ?v * ?v⇧T * ?F * ?e * top * ?e⇧T"
by (simp add: conv_dist_inf mult_left_isotone mult_right_isotone)
thus ?thesis
using 171 order_trans by blast
qed
hence 172: "-?F * ((?F ⊓ ?v)⇧T * ?F * ?e * top * ?e⇧T)⇧T ≤ -?v"
by (smt schroeder_4_p comp_associative order_lesseq_imp pp_increasing)
have "-?F * ((?F ⊓ ?v)⇧T * ?F * ?e * top * ?e⇧T)⇧T = -?F * ?e⇧T⇧T * top⇧T * ?e⇧T * ?F⇧T * (?F ⊓ ?v)⇧T⇧T"
by (simp add: comp_associative conv_dist_comp)
also have "... = -?F * ?e * top * ?e⇧T * ?F * (?F ⊓ ?v)"
using 5 by auto
also have "... = -?F * ?e * top * top * ?e⇧T * ?F * (?F ⊓ ?v)"
using comp_associative by auto
also have "... = -?F * ?e * top ⊓ top * ?e⇧T * ?F * (?F ⊓ ?v)"
by (smt comp_associative comp_inf.star.circ_decompose_9 comp_inf.star_star_absorb comp_inf_covector inf_vector_comp vector_top_closed)
finally have "-?F * ((?F ⊓ ?v)⇧T * ?F * ?e * top * ?e⇧T)⇧T = -?F * ?e * top ⊓ top * ?e⇧T * ?F * (?F ⊓ ?v)"
by simp
hence "-?F * ?e * top ⊓ top * ?e⇧T * ?F * (?F ⊓ ?v) ≤ -?v"
using 172 by auto
hence "?v ⊓ -?F * ?e * top ⊓ top * ?e⇧T * ?F * (?F ⊓ ?v) ≤ bot"
by (smt bot_unique inf.sup_monoid.add_commute p_shunting_swap pseudo_complement)
thus ?thesis
using le_bot sup_monoid.add_0_right by blast
qed
also have "... = top * ?e⇧T * (?F ⊓ ?v ⊓ -?i)⇧T⇧⋆"
using 16 by (smt comp_inf.coreflexive_comp_inf_complement inf_top_right p_bot pseudo_complement top.extremum)
finally show ?thesis
by blast
qed
have 18: "?i ≤ top * ?e⇧T * ?w⇧T⇧⋆"
proof -
have "?i ≤ top * ?e⇧T * (?F ⊓ ?v ⊓ -?i)⇧T⇧⋆"
using 17 by simp
also have "... ≤ top * ?e⇧T * (?v ⊓ -?i)⇧T⇧⋆"
using mult_right_isotone conv_isotone star_isotone inf.cobounded2 inf.sup_monoid.add_assoc by (simp add: inf.sup_monoid.add_assoc order.eq_iff inf.sup_monoid.add_commute)
also have "... ≤ top * ?e⇧T * ((?v ⊓ -?i) ⊔ ?e)⇧T⇧⋆"
using mult_right_isotone conv_isotone star_isotone sup_ge1 by simp
finally show ?thesis
by blast
qed
have 19: "?i ≤ top * ?e⇧T * ?v⇧T⇧⋆"
proof -
have "?i ≤ top * ?e⇧T * (?F ⊓ ?v ⊓ -?i)⇧T⇧⋆"
using 17 by simp
also have "... ≤ top * ?e⇧T * (?v ⊓ -?i)⇧T⇧⋆"
using mult_right_isotone conv_isotone star_isotone inf.cobounded2 inf.sup_monoid.add_assoc by (simp add: inf.sup_monoid.add_assoc order.eq_iff inf.sup_monoid.add_commute)
also have "... ≤ top * ?e⇧T * (?v)⇧T⇧⋆"
using mult_right_isotone conv_isotone star_isotone by auto
finally show ?thesis
by blast
qed
have 20: "f ⊔ f⇧T ≤ (?v ⊓ -?i ⊓ -?i⇧T) ⊔ (?v⇧T ⊓ -?i ⊓ -?i⇧T)"
proof (rule kruskal_edge_between_components_2)
show "?F ≤ - ?i"
using 16 by simp
next
show "injective f"
by (simp add: assms(2))
next
show "f ⊔ f⇧T ≤ w ⊓ - (top * ?e * w⇧T⇧⋆) ⊔ (w ⊓ top * ?e * w⇧T⇧⋆)⇧T ⊔ (w ⊓ - (top * ?e * w⇧T⇧⋆) ⊔ (w ⊓ top * ?e * w⇧T⇧⋆)⇧T)⇧T"
using 2 12 by (metis conv_dist_sup conv_involutive conv_isotone le_supI sup_commute)
qed
have "minimum_spanning_forest ?w g ∧ ?f ≤ ?w ⊔ ?w⇧T"
proof (intro conjI)
have 211: "?e⇧T ≤ ?v⇧⋆"
proof (rule kruskal_edge_arc_1[where g=g and h="?ec"])
show "?e ≤ -- ?ec"
using minarc_below by blast
next
show "?ec ≤ g"
using assms(4) inf.cobounded2 by (simp add: boruvka_inner_invariant_def boruvka_outer_invariant_def conv_dist_inf)
next
show "symmetric g"
by (meson assms(1) boruvka_inner_invariant_def boruvka_outer_invariant_def)
next
show "components g ≤ forest_components (w ⊓ - (top * ?e * w⇧T⇧⋆) ⊔ (w ⊓ top * ?e * w⇧T⇧⋆)⇧T)"
using 9 by simp
next
show "(w ⊓ - (top * ?e * w⇧T⇧⋆) ⊔ (w ⊓ top * ?e * w⇧T⇧⋆)⇧T) * ?e⇧T = bot"
using 13 by blast
qed
have 212: "arc ?i"
proof (rule boruvka_edge_arc)
show "equivalence ?F"
by (simp add: 5)
next
show "forest ?v"
using 10 spanning_forest_def by blast
next
show "arc ?e"
using assms(16) minarc_arc minarc_bot_iff by blast
next
show "regular ?F"
using 3 regular_closed_star regular_conv_closed regular_mult_closed by auto
next
show "?F ≤ forest_components (?F ⊓ ?v)"
by (simp add: 12 2 8 kruskal_forest_components_inf)
next
show "regular ?v"
using 10 spanning_forest_def by blast
next
show "?v * ?e⇧T = bot"
using 13 by auto
next
show "?e * ?F * ?e = bot"
by (simp add: 6)
next
show "?e⇧T ≤ ?v⇧⋆"
using 211 by auto
next
show "?e ≠ bot"
by (simp add: assms(16))
qed
show "minimum_spanning_forest ?w g"
proof (unfold minimum_spanning_forest_def, intro conjI)
have "(?v ⊓ -?i) * ?e⇧T ≤ ?v * ?e⇧T"
using inf_le1 mult_left_isotone by simp
hence "(?v ⊓ -?i) * ?e⇧T = bot"
using 13 le_bot by simp
hence 221: "?e * (?v ⊓ -?i)⇧T = bot"
using conv_dist_comp conv_involutive conv_bot by force
have 222: "injective ?w"
proof (rule injective_sup)
show "injective (?v ⊓ -?i)"
using 8 by (simp add: injective_inf_closed)
next
show "coreflexive (?e * (?v ⊓ -?i)⇧T)"
using 221 by simp
next
show "injective ?e"
by (metis arc_injective minarc_arc coreflexive_bot_closed coreflexive_injective minarc_bot_iff)
qed
show "spanning_forest ?w g"
proof (unfold spanning_forest_def, intro conjI)
show "injective ?w"
using 222 by simp
next
show "acyclic ?w"
proof (rule kruskal_exchange_acyclic_inv_2)
show "acyclic ?v"
using 10 spanning_forest_def by blast
next
show "injective ?v"
using 8 by simp
next
show "?i ≤?v"
using inf.coboundedI1 by simp
next
show "bijective (?i⇧T * top)"
using 212 by simp
next
show "bijective (?e * top)"
using 14 212 by (smt assms(4) comp_inf.idempotent_bot_closed conv_complement minarc_arc minarc_bot_iff p_bot regular_closed_bot semiring.mult_not_zero symmetric_top_closed)
next
show "?i ≤ top * ?e⇧T *?v⇧T⇧⋆"
using 19 by simp
next
show "?v * ?e⇧T * top = bot"
using 13 by simp
qed
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"
proof -
have 1: "--g ≤ --g ⊔ --h"
by simp
have 2: "?e ≤ --g ⊔ --h"
by (metis inf.coboundedI1 inf.sup_monoid.add_commute minarc_below order.trans p_dist_inf p_dist_sup sup.cobounded1)
thus ?thesis
using 1 2 by simp
qed
also have "... ≤ --g"
using assms(18, 19) by auto
finally show "?w ≤ --g"
by simp
next
have 223: "?i ≤ (?v ⊓ -?i)⇧T⇧⋆ * ?e⇧T * top"
proof (rule boruvka_exchange_spanning_inv)
show "forest ?v"
using 10 spanning_forest_def by blast
next
show "?v⇧⋆ * ?e⇧T = ?e⇧T"
using 13 by (smt conv_complement conv_dist_comp conv_involutive conv_star_commute dense_pp fc_top regular_closed_top star_absorb)
next
show "?i ≤ ?v ⊓ top * ?e⇧T * ?w⇧T⇧⋆"
using 18 inf.sup_monoid.add_assoc by auto
next
show "arc ?i"
using 212 by blast
next
show "arc ?e"
using assms(16) minarc_arc minarc_bot_iff by auto
next
show "?v ≤ --g"
using 10 spanning_forest_def by blast
next
show "?w ≤ --g"
proof -
have 2231: "?e ≤ --g"
by (metis inf.boundedE minarc_below pp_dist_inf)
have "?w ≤ ?v ⊔ ?e"
using inf_le1 sup_left_isotone by simp
also have "... ≤ --g"
using 2231 10 spanning_forest_def sup_least by blast
finally show ?thesis
by blast
qed
next
show "?e ≤ --g"
by (metis inf.boundedE minarc_below pp_dist_inf)
next
show "components g ≤ forest_components ?v"
by (simp add: 9)
qed
have "components g ≤ forest_components ?v"
using 10 spanning_forest_def by auto
also have "... ≤ forest_components ?w"
proof (rule kruskal_exchange_forest_components_inv)
next
show "injective ((?v ⊓ -?i) ⊔ ?e)"
using 222 by simp
next
show "regular ?i"
using 15 by simp
next
show "?e * top * ?e = ?e"
by (metis arc_top_arc minarc_arc minarc_bot_iff semiring.mult_not_zero)
next
show "?i ≤ top * ?e⇧T * ?v⇧T⇧⋆"
using 19 by blast
next
show "?v * ?e⇧T * top = bot"
using 13 by simp
next
show "injective ?v"
using 8 by simp
next
show "?i ≤ ?v"
by (simp add: le_infI1)
next
show "?i ≤ (?v ⊓ -?i)⇧T⇧⋆ * ?e⇧T * top"
using 223 by blast
qed
finally show "components g ≤ forest_components ?w"
by simp
next
show "regular ?w"
using 3 7 regular_conv_closed by simp
qed
next
have 224: "?e ⊓ g ≠ bot"
using assms(16) inf.left_commute inf_bot_right minarc_meet_bot by fastforce
have 225: "sum (?e ⊓ g) ≤ sum (?i ⊓ g)"
proof (rule a_to_e_in_forest_modulo_equivalence)
show "symmetric g"
using assms(1) boruvka_inner_invariant_def boruvka_outer_invariant_def by auto
next
show "j ≠ bot"
by (simp add: assms(17))
next
show "f ≤ -- g"
by (simp add: assms(3))
next
show "vector j"
using assms(6) boruvka_inner_invariant_def by blast
next
show "forest h"
by (simp add: assms(8))
next
show " forest_modulo_equivalence (forest_components h) d"
by (simp add: assms(9))
next
show "f ⊔ f⇧T = h ⊔ h⇧T ⊔ d ⊔ d⇧T"
by (simp add: assms(12))
next
show "∀a b. forest_modulo_equivalence_path a b (?H) d ∧ a ≤ - ?H ⊓ - - g ∧ b ≤ d ⟶ sum (b ⊓ g) ≤ sum (a ⊓ g)"
by (simp add: assms(13))
next
show "regular d"
using assms(14) by auto
next
show "?e = ?e"
by simp
next
show "arc ?i"
using 212 by blast
next
show "forest_modulo_equivalence_path ?i ?e ?H (d ⊔ ?e)"
proof -
have "d⇧T * ?H * ?e = bot"
using assms(6, 7, 10 ,11, 17) dT_He_eq_bot le_bot by blast
hence 251: "d⇧T * ?H * ?e ≤ (?H * d)⇧⋆ * ?H * ?e"
by simp
hence "d⇧T * ?H * ?H * ?e ≤ (?H * d)⇧⋆ * ?H * ?e"
by (metis assms(8) forest_components_star star.circ_decompose_9 mult_assoc)
hence "d⇧T * (?H * d)⇧⋆ * ?H * ?e ≤ (?H * d)⇧⋆ * ?H * ?e"
proof -
have "d⇧T * ?H * d ≤ 1"
using assms(9) forest_modulo_equivalence_def dTransHd_le_1 by blast
hence "d⇧T * ?H * d * (?H * d)⇧⋆ * ?H * ?e ≤ (?H * d)⇧⋆ * ?H * ?e"
by (metis mult_left_isotone star.circ_circ_mult star_involutive star_one)
hence "d⇧T * ?H * ?e ⊔ d⇧T * ?H * d * (?H * d)⇧⋆ * ?H * ?e ≤ (?H * d)⇧⋆ * ?H * ?e"
using 251 by simp
hence "d⇧T * (1 ⊔ ?H * d * (?H * d)⇧⋆) * ?H * ?e ≤ (?H * d)⇧⋆ * ?H * ?e"
by (simp add: comp_associative comp_left_dist_sup semiring.distrib_right)
thus ?thesis
by (simp add: star_left_unfold_equal)
qed
hence "?H * d⇧T * (?H * d)⇧⋆ * ?H * ?e ≤ ?H * (?H * d)⇧⋆ * ?H * ?e"
by (simp add: mult_right_isotone mult_assoc)
hence "?H * d⇧T * (?H * d)⇧⋆ * ?H * ?e ≤ ?H * ?H * (d * ?H)⇧⋆ * ?e"
by (smt star_slide mult_assoc)
hence "?H * d⇧T * (?H * d)⇧⋆ * ?H * ?e ≤ ?H * (d * ?H)⇧⋆ * ?e"
by (metis assms(8) forest_components_star star.circ_decompose_9)
hence "?H * d⇧T * (?H * d)⇧⋆ * ?H * ?e ≤ (?H * d)⇧⋆ * ?H * ?e"
using star_slide by auto
hence "?H * d * (?H * d)⇧⋆ * ?H * ?e ⊔ ?H * d⇧T * (?H * d)⇧⋆ * ?H * ?e ≤ (?H * d)⇧⋆ * ?H * ?e"
by (smt le_supI star.circ_loop_fixpoint sup.cobounded2 sup_commute mult_assoc)
hence "(?H * (d ⊔ d⇧T)) * (?H * d)⇧⋆ * ?H * ?e ≤ (?H * d)⇧⋆ * ?H * ?e"
by (simp add: semiring.distrib_left semiring.distrib_right)
hence "(?H * (d ⊔ d⇧T))⇧⋆ * (?H * d)⇧⋆ * ?H * ?e ≤ (?H * d)⇧⋆ * ?H * ?e"
by (simp add: star_left_induct_mult mult_assoc)
hence 252: "(?H * (d ⊔ d⇧T))⇧⋆ * ?H * ?e ≤ (?H * d)⇧⋆ * ?H * ?e"
by (smt mult_left_dist_sup star.circ_transitive_equal star_slide star_sup_1 mult_assoc)
have "?i ≤ top * ?e⇧T * ?F"
by auto
hence "?i⇧T ≤ ?F⇧T * ?e⇧T⇧T * top⇧T"
by (simp add: conv_dist_comp conv_dist_inf mult_assoc)
hence "?i⇧T * top ≤ ?F⇧T * ?e⇧T⇧T * top⇧T * top"
using comp_isotone by blast
also have "... = ?F⇧T * ?e⇧T⇧T * top⇧T"
by (simp add: vector_mult_closed)
also have "... = ?F * ?e⇧T⇧T * top⇧T"
by (simp add: conv_dist_comp conv_star_commute)
also have "... = ?F * ?e * top"
by simp
also have "... = (?H * (d ⊔ d⇧T))⇧⋆ * ?H * ?e * top"
using assms(2, 8, 12) F_is_H_and_d by simp
also have "... ≤ (?H * d)⇧⋆ * ?H * ?e * top"
by (simp add: 252 comp_isotone)
also have "... ≤ (?H * (d ⊔ ?e))⇧⋆ * ?H * ?e * top"
by (simp add: comp_isotone star_isotone)
finally have "?i⇧T * top ≤ (?H * (d ⊔ ?e))⇧⋆ * ?H * ?e * top"
by blast
thus ?thesis
using 212 assms(16) forest_modulo_equivalence_path_def minarc_arc minarc_bot_iff by blast
qed
next
show "?i ≤ - ?H ⊓ -- g"
proof -
have "forest_components h ≤ forest_components f"
using assms(2, 8, 12) H_below_F by blast
then have 241: "?i ≤ -?H"
using 16 assms(9) inf.order_lesseq_imp p_antitone_iff by blast
have "?i ≤ -- g"
using 10 inf.coboundedI1 spanning_forest_def by blast
thus ?thesis
using 241 inf_greatest by blast
qed
next
show "regular h"
using assms(18) by auto
qed
have "?v ⊓ ?e ⊓ -?i = bot"
using 14 by simp
hence "sum (?w ⊓ g) = sum (?v ⊓ -?i ⊓ g) + sum (?e ⊓ g)"
using sum_disjoint inf_commute inf_assoc by simp
also have "... ≤ sum (?v ⊓ -?i ⊓ g) + sum (?i ⊓ g)"
using 224 225 sum_plus_right_isotone by simp
also have "... = sum (((?v ⊓ -?i) ⊔ ?i) ⊓ g)"
using sum_disjoint inf_le2 pseudo_complement by simp
also have "... = sum ((?v ⊔ ?i) ⊓ (-?i ⊔ ?i) ⊓ g)"
by (simp add: sup_inf_distrib2)
also have "... = sum ((?v ⊔ ?i) ⊓ 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"
by (smt conv_dist_inf inf_le1 sup_left_isotone sup_mono inf.order_lesseq_imp)
also have "... ≤ (?v ⊓ -?i ⊓ -?i⇧T) ⊔ (?v⇧T ⊓ -?i ⊓ -?i⇧T) ⊔ ?e"
using 20 sup_left_isotone by simp
also have "... ≤ (?v ⊓ -?i) ⊔ (?v⇧T ⊓ -?i ⊓ -?i⇧T) ⊔ ?e"
by (metis inf.cobounded1 sup_inf_distrib2)
also have "... = ?w ⊔ (?v⇧T ⊓ -?i ⊓ -?i⇧T)"
by (simp add: sup_assoc sup_commute)
also have "... ≤ ?w ⊔ (?v⇧T ⊓ -?i⇧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
thus ?thesis by auto
qed
lemma boruvka_outer_invariant_when_e_not_bot:
assumes "boruvka_inner_invariant j f h g d"
and "j ≠ bot"
and "selected_edge h j g ≤ - forest_components f"
and "selected_edge h j g ≠ bot"
shows "boruvka_outer_invariant (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) g"
proof -
let ?c = "choose_component (forest_components h) j"
let ?p = "path f h j g"
let ?F = "forest_components f"
let ?H = "forest_components h"
let ?e = "selected_edge h j g"
let ?f' = "f ⊓ -?e⇧T ⊓ -?p ⊔ (f ⊓ -?e⇧T ⊓ ?p)⇧T ⊔ ?e"
let ?d' = "d ⊔ ?e"
let ?j' = "j ⊓ -?c"
show "boruvka_outer_invariant ?f' g"
proof (unfold boruvka_outer_invariant_def, intro conjI)
show "symmetric g"
by (meson assms(1) boruvka_inner_invariant_def boruvka_outer_invariant_def)
next
show "injective ?f'"
proof (rule kruskal_injective_inv)
show "injective (f ⊓ - ?e⇧T)"
by (meson assms(1) boruvka_inner_invariant_def boruvka_outer_invariant_def injective_inf_closed)
show "covector (?p)"
using covector_mult_closed by simp
show "?p * (f ⊓ - ?e⇧T)⇧T ≤ ?p"
by (simp add: mult_right_isotone star.left_plus_below_circ star_plus mult_assoc)
show "?e ≤ ?p"
by (meson mult_left_isotone order.trans star_outer_increasing top.extremum)
show "?p * (f ⊓ - ?e⇧T)⇧T ≤ - ?e"
proof -
have "?p * (f ⊓ - ?e⇧T)⇧T ≤ ?p * f⇧T"
by (simp add: conv_dist_inf mult_right_isotone)
also have "... ≤ top * ?e * (f)⇧T⇧⋆ * f⇧T"
using conv_dist_inf star_isotone comp_isotone by simp
also have "... ≤ - ?e"
using assms(1, 4) boruvka_inner_invariant_def boruvka_outer_invariant_def kruskal_injective_inv_2 minarc_arc minarc_bot_iff by auto
finally show ?thesis .
qed
show "injective (?e)"
by (metis arc_injective coreflexive_bot_closed minarc_arc minarc_bot_iff semiring.mult_not_zero)
show "coreflexive (?p⇧T * ?p ⊓ (f ⊓ - ?e⇧T)⇧T * (f ⊓ - ?e⇧T))"
proof -
have "(?p⇧T * ?p ⊓ (f ⊓ - ?e⇧T)⇧T * (f ⊓ - ?e⇧T)) ≤ ?p⇧T * ?p ⊓ f⇧T * f"
using conv_dist_inf inf.sup_right_isotone mult_isotone by simp
also have "... ≤ (top * ?e * f⇧T⇧⋆)⇧T * (top * ?e * f⇧T⇧⋆) ⊓ f⇧T * f"
by (metis comp_associative comp_inf.coreflexive_transitive comp_inf.mult_right_isotone comp_isotone conv_isotone inf.cobounded1 inf.idem inf.sup_monoid.add_commute star_isotone top.extremum)
also have "... ≤ 1"
using assms(1, 4) boruvka_inner_invariant_def boruvka_outer_invariant_def kruskal_injective_inv_3 minarc_arc minarc_bot_iff by auto
finally show ?thesis
by simp
qed
qed
next
show "acyclic ?f'"
proof (rule kruskal_acyclic_inv)
show "acyclic (f ⊓ - ?e⇧T)"
proof -
have f_intersect_below: "(f ⊓ - ?e⇧T) ≤ f" by simp
have "acyclic f"
by (meson assms(1) boruvka_inner_invariant_def boruvka_outer_invariant_def)
thus ?thesis
using comp_isotone dual_order.trans star_isotone f_intersect_below by blast
qed
next
show "covector ?p"
by (metis comp_associative vector_top_closed)
next
show "(f ⊓ - ?e⇧T ⊓ ?p)⇧T * (f ⊓ - ?e⇧T)⇧⋆ * ?e = bot"
proof -
have "?e ≤ - (f⇧T⇧⋆ * f⇧⋆)"
by (simp add: assms(3))
hence "?e * top * ?e ≤ - (f⇧T⇧⋆ * f⇧⋆)"
by (metis arc_top_arc minarc_arc minarc_bot_iff semiring.mult_not_zero)
hence "?e⇧T * top * ?e⇧T ≤ - (f⇧T⇧⋆ * f⇧⋆)⇧T"
by (metis comp_associative conv_complement conv_dist_comp conv_isotone symmetric_top_closed)
hence "?e⇧T * top * ?e⇧T ≤ - (f⇧T⇧⋆ * f⇧⋆)"
by (simp add: conv_dist_comp conv_star_commute)
hence "?e * (f⇧T⇧⋆ * f⇧⋆) * ?e ≤ bot"
using triple_schroeder_p by auto
hence 1: "?e * f⇧T⇧⋆ * f⇧⋆ * ?e ≤ bot"
using mult_assoc by auto
have 2: "(f ⊓ - ?e⇧T)⇧T⇧⋆ ≤ f⇧T⇧⋆"
by (simp add: conv_dist_inf star_isotone)
have "(f ⊓ - ?e⇧T ⊓ ?p)⇧T * (f ⊓ - ?e⇧T)⇧⋆ * ?e ≤ (f ⊓ ?p)⇧T * (f ⊓ - ?e⇧T)⇧⋆ * ?e"
by (simp add: comp_isotone conv_dist_inf inf.orderI inf.sup_monoid.add_assoc)
also have "... ≤ (f ⊓ ?p)⇧T * f⇧⋆ * ?e"
by (simp add: comp_isotone star_isotone)
also have "... ≤ (f ⊓ top * ?e * (f)⇧T⇧⋆)⇧T * f⇧⋆ * ?e"
using 2 by (metis comp_inf.comp_isotone comp_inf.coreflexive_transitive comp_isotone conv_isotone inf.idem top.extremum)
also have "... = (f⇧T ⊓ (top * ?e * f⇧T⇧⋆)⇧T) * f⇧⋆ * ?e"
by (simp add: conv_dist_inf)
also have "... ≤ top * (f⇧T ⊓ (top * ?e * f⇧T⇧⋆)⇧T) * f⇧⋆ * ?e"
using top_left_mult_increasing mult_assoc by auto
also have "... = (top ⊓ top * ?e * f⇧T⇧⋆) * f⇧T * f⇧⋆ * ?e"
by (smt covector_comp_inf_1 covector_mult_closed order.eq_iff inf.sup_monoid.add_commute vector_top_closed)
also have "... = top * ?e * f⇧T⇧⋆ * f⇧T * f⇧⋆ * ?e"
by simp
also have "... ≤ top * ?e * f⇧T⇧⋆ * f⇧⋆ * ?e"
by (smt conv_dist_comp conv_isotone conv_star_commute mult_left_isotone mult_right_isotone star.left_plus_below_circ mult_assoc)
also have "... ≤ bot"
using 1 covector_bot_closed le_bot mult_assoc by fastforce
finally show ?thesis
using le_bot by auto
qed
next
show "?e * (f ⊓ - ?e⇧T)⇧⋆ * ?e = bot"
proof -
have 1: "?e ≤ - ?F"
by (simp add: assms(3))
have 2: "injective f"
by (meson assms(1) boruvka_inner_invariant_def boruvka_outer_invariant_def)
have 3: "equivalence ?F"
using 2 forest_components_equivalence by simp
hence 4: "?e⇧T = ?e⇧T * top * ?e⇧T"
by (smt arc_conv_closed arc_top_arc covector_complement_closed covector_conv_vector ex231e minarc_arc minarc_bot_iff pp_surjective regular_closed_top vector_mult_closed vector_top_closed)
also have "... ≤ - ?F" using 1 3 conv_isotone conv_complement calculation by fastforce
finally have 5: "?e * ?F * ?e = bot"
using 4 by (smt triple_schroeder_p le_bot pp_total regular_closed_top vector_top_closed)
have "(f ⊓ - ?e⇧T)⇧⋆ ≤ f⇧⋆"
by (simp add: star_isotone)
hence "?e * (f ⊓ - ?e⇧T)⇧⋆ * ?e ≤ ?e * f⇧⋆ * ?e"
using mult_left_isotone mult_right_isotone by blast
also have "... ≤ ?e * ?F * ?e"
by (metis conv_star_commute forest_components_increasing mult_left_isotone mult_right_isotone star_involutive)
also have 6: "... = bot"
using 5 by simp
finally show ?thesis using 6 le_bot by blast
qed
next
show "forest_components (f ⊓ -?e⇧T) ≤ - ?e"
proof -
have 1: "?e ≤ - ?F"
by (simp add: assms(3))
have "f ⊓ - ?e⇧T ≤ f"
by simp
hence "forest_components (f ⊓ - ?e⇧T) ≤ ?F"
using forest_components_isotone by blast
thus ?thesis
using 1 order_lesseq_imp p_antitone_iff by blast
qed
qed
next
show "?f' ≤ --g"
proof -
have 1: "(f ⊓ - ?e⇧T ⊓ - ?p) ≤ --g"
by (meson assms(1) boruvka_inner_invariant_def boruvka_outer_invariant_def inf.coboundedI1)
have 2: "(f ⊓ - ?e⇧T ⊓ ?p)⇧T ≤ --g"
proof -
have "(f ⊓ - ?e⇧T ⊓ ?p)⇧T ≤ f⇧T"
by (simp add: conv_isotone inf.sup_monoid.add_assoc)
also have "... ≤ --g"
by (metis assms(1) boruvka_inner_invariant_def boruvka_outer_invariant_def conv_complement conv_isotone)
finally show ?thesis
by simp
qed
have 3: "?e ≤ --g"
by (metis inf.boundedE minarc_below pp_dist_inf)
show ?thesis using 1 2 3
by simp
qed
next
show "regular ?f'"
using assms(1) boruvka_inner_invariant_def boruvka_outer_invariant_def minarc_regular regular_closed_star regular_conv_closed regular_mult_closed by auto
next
show "∃w. minimum_spanning_forest w g ∧ ?f' ≤ w ⊔ w⇧T"
proof (rule exists_a_w)
show "symmetric g"
using assms(1) boruvka_inner_invariant_def boruvka_outer_invariant_def by auto
next
show "forest f"
using assms(1) boruvka_inner_invariant_def boruvka_outer_invariant_def by auto
next
show "f ≤ --g"
using assms(1) boruvka_inner_invariant_def boruvka_outer_invariant_def by auto
next
show "regular f"
using assms(1) boruvka_inner_invariant_def boruvka_outer_invariant_def by auto
next
show "(∃w . minimum_spanning_forest w g ∧ f ≤ w ⊔ w⇧T)"
using assms(1) boruvka_inner_invariant_def boruvka_outer_invariant_def by auto
next
show "vector j"
using assms(1) boruvka_inner_invariant_def by blast
next
show "regular j"
using assms(1) boruvka_inner_invariant_def by blast
next
show "forest h"
using assms(1) boruvka_inner_invariant_def by blast
next
show "forest_modulo_equivalence (forest_components h) d"
using assms(1) boruvka_inner_invariant_def by blast
next
show "d * top ≤ - j"
using assms(1) boruvka_inner_invariant_def by blast
next
show "forest_components h * j = j"
using assms(1) boruvka_inner_invariant_def by blast
next
show "f ⊔ f⇧T = h ⊔ h⇧T ⊔ d ⊔ d⇧T"
using assms(1) boruvka_inner_invariant_def by blast
next
show "(∀ a b . forest_modulo_equivalence_path a b (forest_components h) d ∧ a ≤ -(forest_components h) ⊓ -- g ∧ b ≤ d ⟶ sum(b ⊓ g) ≤ sum(a ⊓ g))"
using assms(1) boruvka_inner_invariant_def by blast
next
show "regular d"
using assms(1) boruvka_inner_invariant_def by blast
next
show "selected_edge h j g ≤ - forest_components f"
by (simp add: assms(3))
next
show "selected_edge h j g ≠ bot"
by (simp add: assms(4))
next
show "j ≠ bot"
by (simp add: assms(2))
next
show "regular h"
using assms(1) boruvka_inner_invariant_def boruvka_outer_invariant_def by auto
next
show "h ≤ --g"
using H_below_regular_g assms(1) boruvka_inner_invariant_def boruvka_outer_invariant_def by auto
qed
qed
qed
lemma second_inner_invariant_when_e_not_bot:
assumes "boruvka_inner_invariant j f h g d"
and "j ≠ bot"
and "selected_edge h j g ≤ - forest_components f"
and "selected_edge h j g ≠ bot"
shows "boruvka_inner_invariant
(j ⊓ - choose_component (forest_components h) j)
(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)
h g (d ⊔ selected_edge h j g)"
proof -
let ?c = "choose_component (forest_components h) j"
let ?p = "path f h j g"
let ?F = "forest_components f"
let ?H = "forest_components h"
let ?e = "selected_edge h j g"
let ?f' = "f ⊓ -?e⇧T ⊓ -?p ⊔ (f ⊓ -?e⇧T ⊓ ?p)⇧T ⊔ ?e"
let ?d' = "d ⊔ ?e"
let ?j' = "j ⊓ -?c"
show "boruvka_inner_invariant ?j' ?f' h g ?d'"
proof (unfold boruvka_inner_invariant_def, intro conjI)
show 1: "boruvka_outer_invariant ?f' g"
using assms(1, 2, 3, 4) boruvka_outer_invariant_when_e_not_bot by blast
next
show "g ≠ bot"
using assms(1) boruvka_inner_invariant_def by force
next
show "regular ?d'"
using assms(1) boruvka_inner_invariant_def minarc_regular by auto
next
show "regular ?j'"
using assms(1) boruvka_inner_invariant_def by auto
next
show "vector ?j'"
using assms(1, 2) boruvka_inner_invariant_def component_is_vector vector_complement_closed vector_inf_closed by simp
next
show "regular h"
by (meson assms(1) boruvka_inner_invariant_def)
next
show "injective h"
by (meson assms(1) boruvka_inner_invariant_def)
next
show "pd_kleene_allegory_class.acyclic h"
by (meson assms(1) boruvka_inner_invariant_def)
next
show "?H * ?j' = ?j'"
using fc_j_eq_j_inv assms(1) boruvka_inner_invariant_def by blast
next
show "forest_modulo_equivalence ?H ?d'"
using assms(1, 2, 3) forest_modulo_equivalence_d_U_e boruvka_inner_invariant_def boruvka_outer_invariant_def by auto
next
show "?d' * top ≤ -?j'"
proof -
have 31: "?d' * top = d * top ⊔ ?e * top"
by (simp add: mult_right_dist_sup)
have 32: "d * top ≤ -?j'"
by (meson assms(1) boruvka_inner_invariant_def inf.coboundedI1 p_antitone_iff)
have "regular (?c * - ?c⇧T)"
using assms(1) boruvka_inner_invariant_def boruvka_outer_invariant_def component_is_regular regular_conv_closed regular_mult_closed by presburger
then have "minarc(?c * - ?c⇧T ⊓ g) = minarc(?c ⊓ - ?c⇧T ⊓ g)"
by (metis component_is_vector covector_comp_inf inf_top.left_neutral vector_conv_compl)
also have "... ≤ -- (?c ⊓ - ?c⇧T ⊓ g)"
using minarc_below by blast
also have "... ≤ -- ?c"
by (simp add: inf.sup_monoid.add_assoc)
also have "... = ?c"
using component_is_regular by auto
finally have "?e ≤ ?c"
by simp
then have "?e * top ≤ ?c"
by (metis component_is_vector mult_left_isotone)
also have "... ≤ -j ⊔ ?c"
by simp
also have "... = - (j ⊓ - ?c)"
using component_is_regular by auto
finally have 33: "?e * top ≤ - (j ⊓ - ?c)"
by simp
show ?thesis
using 31 32 33 by auto
qed
next
show "?f' ⊔ ?f'⇧T = h ⊔ h⇧T ⊔ ?d' ⊔ ?d'⇧T"
proof -
have "?f' ⊔ ?f'⇧T = f ⊓ - ?e⇧T ⊓ - ?p ⊔ (f ⊓ - ?e⇧T ⊓ ?p)⇧T ⊔ ?e ⊔ (f ⊓ - ?e⇧T ⊓ - ?p)⇧T ⊔ (f ⊓ - ?e⇧T ⊓ ?p) ⊔ ?e⇧T"
by (simp add: conv_dist_sup sup_monoid.add_assoc)
also have "... = (f ⊓ - ?e⇧T ⊓ - ?p) ⊔ (f ⊓ - ?e⇧T ⊓ ?p) ⊔ (f ⊓ - ?e⇧T ⊓ ?p)⇧T ⊔ (f ⊓ - ?e⇧T ⊓ - ?p)⇧T ⊔ ?e⇧T ⊔ ?e"
by (simp add: sup.left_commute sup_commute)
also have "... = f ⊔ f⇧T ⊔ ?e ⊔ ?e⇧T"
proof (rule simplify_f)
show "regular ?p"
using assms(1) boruvka_inner_invariant_def boruvka_outer_invariant_def minarc_regular regular_closed_star regular_conv_closed regular_mult_closed by auto
next
show "regular ?e"
using minarc_regular by blast
qed
also have "... = h ⊔ h⇧T ⊔ d ⊔ d⇧T ⊔ ?e ⊔ ?e⇧T"
using assms(1) boruvka_inner_invariant_def by auto
finally show ?thesis
by (smt conv_dist_sup sup.left_commute sup_commute)
qed
next
show "∀ a b . forest_modulo_equivalence_path a b ?H ?d' ∧ a ≤ - ?H ⊓ -- g ∧ b ≤ ?d' ⟶ sum (b ⊓ g) ≤ sum (a ⊓ g)"
proof (intro allI, rule impI, unfold forest_modulo_equivalence_path_def)
fix a b
assume 1: "(arc a ∧ arc b ∧ a⇧T * top ≤ (?H * ?d')⇧⋆ * ?H * b * top) ∧ a ≤ - ?H ⊓ -- g ∧ b ≤ ?d'"
thus "sum (b ⊓ g) ≤ sum (a ⊓ g)"
proof (cases "b = ?e")
case b_equals_e: True
thus ?thesis
proof (cases "a = ?e")
case True
thus ?thesis
using b_equals_e by auto
next
case a_ne_e: False
have "sum (b ⊓ g) ≤ sum (a ⊓ g)"
proof (rule a_to_e_in_forest_modulo_equivalence)
show "symmetric g"
using assms(1) boruvka_inner_invariant_def boruvka_outer_invariant_def by auto
next
show "j ≠ bot"
by (simp add: assms(2))
next
show "f ≤ -- g"
using assms(1) boruvka_inner_invariant_def boruvka_outer_invariant_def by auto
next
show "vector j"
using assms(1) boruvka_inner_invariant_def by blast
next
show "forest h"
using assms(1) boruvka_inner_invariant_def by blast
next
show "forest_modulo_equivalence (forest_components h) d"
using assms(1) boruvka_inner_invariant_def by blast
next
show "f ⊔ f⇧T = h ⊔ h⇧T ⊔ d ⊔ d⇧T"
using assms(1) boruvka_inner_invariant_def by blast
next
show "∀a b. forest_modulo_equivalence_path a b (?H) d ∧ a ≤ - ?H ⊓ - - g ∧ b ≤ d ⟶ sum (b ⊓ g) ≤ sum (a ⊓ g)"
using assms(1) boruvka_inner_invariant_def by blast
next
show "regular d"
using assms(1) boruvka_inner_invariant_def by blast
next
show "b = ?e"
using b_equals_e by simp
next
show "arc a"
using 1 by simp
next
show "forest_modulo_equivalence_path a b ?H ?d'"
using 1 forest_modulo_equivalence_path_def by simp
next
show "a ≤ - ?H ⊓ -- g"
using 1 by simp
next
show "regular h"
using assms(1) boruvka_inner_invariant_def boruvka_outer_invariant_def by auto
qed
thus ?thesis
by simp
qed
next
case b_not_equal_e: False
then have b_below_d: "b ≤ d"
using 1 assms(4) different_arc_in_sup_arc minarc_arc minarc_bot_iff by metis
thus ?thesis
proof (cases "?e ≤ d")
case True
then have "forest_modulo_equivalence_path a b ?H d ∧ b ≤ d"
using 1 forest_modulo_equivalence_path_def sup.absorb1 by auto
thus ?thesis
using 1 assms(1) boruvka_inner_invariant_def by blast
next
case e_not_less_than_d: False
have 71:"equivalence ?H"
using assms(1) fch_equivalence boruvka_inner_invariant_def by auto
then have 72: "forest_modulo_equivalence_path a b ?H ?d' ⟷ forest_modulo_equivalence_path a b ?H d ∨ (forest_modulo_equivalence_path a ?e ?H d ∧ forest_modulo_equivalence_path ?e b ?H d)"
proof (rule forest_modulo_equivalence_path_split_disj)
show "arc ?e"
using assms(4) minarc_arc minarc_bot_iff by blast
next
show "regular a ∧ regular b ∧ regular ?e ∧ regular d ∧ regular ?H"
using assms(1) 1 boruvka_inner_invariant_def boruvka_outer_invariant_def arc_regular minarc_regular regular_closed_star regular_conv_closed regular_mult_closed by auto
qed
thus ?thesis
proof (cases "forest_modulo_equivalence_path a b ?H d")
case True
have "forest_modulo_equivalence_path a b ?H d ∧ b ≤ d"
using 1 True forest_modulo_equivalence_path_def sup.absorb1 by (metis assms(4) b_not_equal_e minarc_arc minarc_bot_iff different_arc_in_sup_arc)
thus ?thesis
using 1 assms(1) b_below_d boruvka_inner_invariant_def by auto
next
case False
have 73:"forest_modulo_equivalence_path a ?e ?H d ∧ forest_modulo_equivalence_path ?e b ?H d"
using 1 72 False forest_modulo_equivalence_path_def by blast
have 74: "?e ≤ --g"
by (metis inf.boundedE minarc_below pp_dist_inf)
have "?H ≤ ?F"
using assms(1) H_below_F boruvka_inner_invariant_def boruvka_outer_invariant_def by blast
then have "?e ≤ - ?H"
using assms(3) order_trans p_antitone by blast
then have "?e ≤ - ?H ⊓ --g"
using 74 by simp
then have 75: "sum (b ⊓ g) ≤ sum (?e ⊓ g)"
using assms(1) b_below_d 73 boruvka_inner_invariant_def by blast
have 76: "forest_modulo_equivalence_path a ?e ?H ?d'"
by (meson 73 forest_modulo_equivalence_path_split_disj assms(1) forest_modulo_equivalence_path_def boruvka_inner_invariant_def boruvka_outer_invariant_def fch_equivalence arc_regular regular_closed_star regular_conv_closed regular_mult_closed)
have 77: "sum (?e ⊓ g) ≤ sum (a ⊓ g)"
proof (rule a_to_e_in_forest_modulo_equivalence)
show "symmetric g"
using assms(1) boruvka_inner_invariant_def boruvka_outer_invariant_def by auto
next
show "j ≠ bot"
by (simp add: assms(2))
next
show "f ≤ -- g"
using assms(1) boruvka_inner_invariant_def boruvka_outer_invariant_def by auto
next
show "vector j"
using assms(1) boruvka_inner_invariant_def by blast
next
show "forest h"
using assms(1) boruvka_inner_invariant_def by blast
next
show "forest_modulo_equivalence (forest_components h) d"
using assms(1) boruvka_inner_invariant_def by blast
next
show "f ⊔ f⇧T = h ⊔ h⇧T ⊔ d ⊔ d⇧T"
using assms(1) boruvka_inner_invariant_def by blast
next
show "∀a b. forest_modulo_equivalence_path a b (?H) d ∧ a ≤ - ?H ⊓ - - g ∧ b ≤ d ⟶ sum (b ⊓ g) ≤ sum (a ⊓ g)"
using assms(1) boruvka_inner_invariant_def by blast
next
show "regular d"
using assms(1) boruvka_inner_invariant_def by blast
next
show "?e = ?e"
by simp
next
show "arc a"
using 1 by simp
next
show "forest_modulo_equivalence_path a ?e ?H ?d'"
by (simp add: "76")
next
show "a ≤ - ?H ⊓ --g"
using 1 by simp
next
show "regular h"
using assms(1) boruvka_inner_invariant_def boruvka_outer_invariant_def by auto
qed
thus ?thesis
using 75 order.trans by blast
qed
qed
qed
qed
qed
qed
lemma second_inner_invariant_when_e_bot:
assumes "selected_edge h j g = bot"
and "selected_edge h j g ≤ - forest_components f"
and "boruvka_inner_invariant j f h g d"
shows "boruvka_inner_invariant
(j ⊓ - choose_component (forest_components h) j)
(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)
h g (d ⊔ selected_edge h j g)"
proof -
let ?c = "choose_component (forest_components h) j"
let ?p = "path f h j g"
let ?F = "forest_components f"
let ?H = "forest_components h"
let ?e = "selected_edge h j g"
let ?f' = "f ⊓ -?e⇧T ⊓ -?p ⊔ (f ⊓ -?e⇧T ⊓ ?p)⇧T ⊔ ?e"
let ?d' = "d ⊔ ?e"
let ?j' = "j ⊓ -?c"
show "boruvka_inner_invariant ?j' ?f' h g ?d'"
proof (unfold boruvka_inner_invariant_def, intro conjI)
next
show "boruvka_outer_invariant ?f' g"
using assms(1) assms(3) boruvka_inner_invariant_def by auto
next
show "g ≠ bot"
using assms(3) boruvka_inner_invariant_def by blast
next
show "regular ?d'"
using assms(1) assms(3) boruvka_inner_invariant_def by auto
next
show "regular ?j'"
using assms(3) boruvka_inner_invariant_def by auto
next
show "vector ?j'"
by (metis assms(3) boruvka_inner_invariant_def component_is_vector vector_complement_closed vector_inf_closed)
next
show "regular h"
using assms(3) boruvka_inner_invariant_def by blast
next
show "injective h"
using assms(3) boruvka_inner_invariant_def by blast
next
show "pd_kleene_allegory_class.acyclic h"
using assms(3) boruvka_inner_invariant_def by blast
next
show "?H * ?j' = ?j'"
using assms(3) fc_j_eq_j_inv boruvka_inner_invariant_def by blast
next
show "forest_modulo_equivalence ?H ?d'"
using assms(1) assms(3) boruvka_inner_invariant_def by auto
next
show "?d' * top ≤ -?j'"
using assms(1) assms(3) boruvka_inner_invariant_def by (metis order.trans p_antitone_inf sup_monoid.add_0_right)
next
show "?f' ⊔ ?f'⇧T = h ⊔ h⇧T ⊔ ?d' ⊔ ?d'⇧T"
using assms(1, 3) boruvka_inner_invariant_def by auto
next
show "∀a b. forest_modulo_equivalence_path a b ?H ?d' ∧ a ≤ -?H ⊓ --g ∧ b ≤ ?d' ⟶ sum(b ⊓ g) ≤ sum(a ⊓ g)"
using assms(1, 3) boruvka_inner_invariant_def by auto
qed
qed
subsection ‹Formalization and correctness proof›
text ‹
The following result shows that Bor\r{u}vka's algorithm constructs a minimum spanning forest.
We have the same postcondition as the proof of Kruskal's minimum spanning tree algorithm.
We show only partial correctness.
›
theorem boruvka_mst:
"VARS f j h c e d
{ symmetric g }
f := bot;
WHILE -(forest_components f) ⊓ g ≠ bot
INV { boruvka_outer_invariant f g }
DO
j := top;
h := f;
d := bot;
WHILE j ≠ bot
INV { boruvka_inner_invariant j f h g d }
DO
c := choose_component (forest_components h) j;
e := minarc(c * -c⇧T ⊓ g);
IF e ≤ -(forest_components f) THEN
f := f ⊓ -e⇧T;
f := (f ⊓ -(top * e * f⇧T⇧⋆)) ⊔ (f ⊓ top * e * f⇧T⇧⋆)⇧T ⊔ e;
d := d ⊔ e
ELSE
SKIP
FI;
j := j ⊓ -c
OD
OD
{ minimum_spanning_forest f g }"
proof vcg_simp
assume 1: "symmetric g"
show "boruvka_outer_invariant bot g"
using 1 boruvka_outer_invariant_def kruskal_exists_minimal_spanning by auto
next
fix f
let ?F = "forest_components f"
assume 1: "boruvka_outer_invariant f g ∧ - ?F ⊓ g ≠ bot"
have 2: "equivalence ?F"
using 1 boruvka_outer_invariant_def forest_components_equivalence by auto
show "boruvka_inner_invariant top f f g bot"
proof (unfold boruvka_inner_invariant_def, intro conjI)
show "boruvka_outer_invariant f g"
by (simp add: 1)
next
show "g ≠ bot"
using 1 by auto
next
show "surjective top"
by simp
next
show "regular top"
by simp
next
show "regular bot"
by auto
next
show "regular f"
using 1 boruvka_outer_invariant_def by blast
next
show "injective f"
using 1 boruvka_outer_invariant_def by blast
next
show "pd_kleene_allegory_class.acyclic f"
using 1 boruvka_outer_invariant_def by blast
next
show "forest_modulo_equivalence ?F bot"
by (simp add: 2 forest_modulo_equivalence_def)
next
show "bot * top ≤ - top"
by simp
next
show "times_top_class.total (?F)"
by (simp add: star.circ_right_top mult_assoc)
next
show "f ⊔ f⇧T = f ⊔ f⇧T ⊔ bot ⊔ bot⇧T"
by simp
next
show "∀ a b. forest_modulo_equivalence_path a b ?F bot ∧ a ≤ - ?F ⊓ -- g ∧ b ≤ bot ⟶ sum (b ⊓ g) ≤ sum (a ⊓ g)"
by (metis (full_types) forest_modulo_equivalence_path_def bot_unique mult_left_zero mult_right_zero top.extremum)
qed
next
fix f j h d
let ?c = "choose_component (forest_components h) j"
let ?p = "path f h j g"
let ?F = "forest_components f"
let ?H = "forest_components h"
let ?e = "selected_edge h j g"
let ?f' = "f ⊓ -?e⇧T ⊓ -?p ⊔ (f ⊓ -?e⇧T ⊓ ?p)⇧T ⊔ ?e"
let ?d' = "d ⊔ ?e"
let ?j' = "j ⊓ -?c"
assume 1: "boruvka_inner_invariant j f h g d ∧ j ≠ bot"
show "(?e ≤ -?F ⟶ boruvka_inner_invariant ?j' ?f' h g ?d') ∧ (¬ ?e ≤ -?F ⟶ boruvka_inner_invariant ?j' f h g d)"
proof (intro conjI)
show "?e ≤ -?F ⟶ boruvka_inner_invariant ?j' ?f' h g ?d'"
proof (cases "?e = bot")
case True
thus ?thesis
using 1 second_inner_invariant_when_e_bot by simp
next
case False
thus ?thesis
using 1 second_inner_invariant_when_e_not_bot by simp
qed
next
show "¬ ?e ≤ -?F ⟶ boruvka_inner_invariant ?j' f h g d"
proof (rule impI, unfold boruvka_inner_invariant_def, intro conjI)
show "boruvka_outer_invariant f g"
using 1 boruvka_inner_invariant_def by blast
next
show "g ≠ bot"
using 1 boruvka_inner_invariant_def by blast
next
show "vector ?j'"
using 1 boruvka_inner_invariant_def component_is_vector vector_complement_closed vector_inf_closed by auto
next
show "regular ?j'"
using 1 boruvka_inner_invariant_def by auto
next
show "regular d"
using 1 boruvka_inner_invariant_def by blast
next
show "regular h"
using 1 boruvka_inner_invariant_def by blast
next
show "injective h"
using 1 boruvka_inner_invariant_def by blast
next
show "pd_kleene_allegory_class.acyclic h"
using 1 boruvka_inner_invariant_def by blast
next
show "forest_modulo_equivalence ?H d"
using 1 boruvka_inner_invariant_def by blast
next
show "d * top ≤ -?j'"
using 1 by (meson boruvka_inner_invariant_def dual_order.trans p_antitone_inf)
next
show "?H * ?j' = ?j'"
using 1 fc_j_eq_j_inv boruvka_inner_invariant_def by blast
next
show "f ⊔ f⇧T = h ⊔ h⇧T ⊔ d ⊔ d⇧T"
using 1 boruvka_inner_invariant_def by blast
next
show "¬ ?e ≤ -?F ⟹ ∀a b. forest_modulo_equivalence_path a b ?H d ∧ a ≤ -?H ⊓ --g ∧ b ≤ d ⟶ sum(b ⊓ g) ≤ sum(a ⊓ g)"
using 1 boruvka_inner_invariant_def by blast
qed
qed
next
fix f h d
assume "boruvka_inner_invariant bot f h g d"
thus "boruvka_outer_invariant f g"
by (meson boruvka_inner_invariant_def)
next
fix f
assume 1: "boruvka_outer_invariant f g ∧ - forest_components f ⊓ g = bot"
hence 2:"spanning_forest f g"
proof (unfold spanning_forest_def, intro conjI)
show "injective f"
using 1 boruvka_outer_invariant_def by blast
next
show "acyclic f"
using 1 boruvka_outer_invariant_def by blast
next
show "f ≤ --g"
using 1 boruvka_outer_invariant_def by blast
next
show "components g ≤ forest_components f"
proof -
let ?F = "forest_components f"
have "-?F ⊓ g ≤ bot"
by (simp add: 1)
hence "--g ≤ bot ⊔ --?F"
using 1 shunting_p p_antitone pseudo_complement by auto
hence "--g ≤ ?F"
using 1 boruvka_outer_invariant_def pp_dist_comp pp_dist_star regular_conv_closed by auto
hence "(--g)⇧⋆ ≤ ?F⇧⋆"
by (simp add: star_isotone)
thus ?thesis
using 1 boruvka_outer_invariant_def forest_components_star by auto
qed
next
show "regular f"
using 1 boruvka_outer_invariant_def by auto
qed
from 1 obtain w where 3: "minimum_spanning_forest w g ∧ f ≤ w ⊔ w⇧T"
using boruvka_outer_invariant_def by blast
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 2 spanning_forest_def inf.sup_right_isotone by simp
also have "... ≤ f ⊔ f⇧T"
proof (rule cancel_separate_6[where z=w and y="w⇧T"])
show "injective w"
using 3 minimum_spanning_forest_def spanning_forest_def by simp
next
show "f⇧T ≤ w⇧T ⊔ w"
using 3 by (metis conv_dist_inf conv_dist_sup conv_involutive inf.cobounded2 inf.orderE)
next
show "f ≤ w⇧T ⊔ w"
using 3 by (simp add: sup_commute)
next
show "injective w"
using 3 minimum_spanning_forest_def spanning_forest_def by simp
next
show "w ⊓ w⇧T⇧⋆ = bot"
using 3 by (metis acyclic_star_below_complement comp_inf.mult_right_isotone inf_p le_bot minimum_spanning_forest_def spanning_forest_def)
qed
finally have 4: "w ≤ f ⊔ f⇧T"
by simp
have "sum (f ⊓ g) = sum ((w ⊔ w⇧T) ⊓ (f ⊓ g))"
using 3 by (metis inf_absorb2 inf.assoc)
also have "... = sum (w ⊓ (f ⊓ g)) + sum (w⇧T ⊓ (f ⊓ g))"
using 3 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))"
proof -
have 51:"f⇧T ⊓ (w ⊓ g) = f⇧T ⊓ (w ⊓ g⇧T)"
using 1 boruvka_outer_invariant_def by auto
have 52:"f ⊓ (w ⊓ g) = w ⊓ (f ⊓ g)"
by (simp add: inf.left_commute)
thus ?thesis
using 51 52 abel_semigroup.left_commute inf.abel_semigroup_axioms by fastforce
qed
also have "... = sum ((f ⊔ f⇧T) ⊓ (w ⊓ g))"
using 2 acyclic_asymmetric inf.sup_monoid.add_commute sum_disjoint spanning_forest_def by simp
also have "... = sum (w ⊓ g)"
using 4 by (metis inf_absorb2 inf.assoc)
finally show "minimum_spanning_forest f g"
using 2 3 minimum_spanning_forest_def by simp
qed
end
end