diff --git a/thys/Relational_Minimum_Spanning_Trees/Boruvka.thy b/thys/Relational_Minimum_Spanning_Trees/Boruvka.thy --- a/thys/Relational_Minimum_Spanning_Trees/Boruvka.thy +++ b/thys/Relational_Minimum_Spanning_Trees/Boruvka.thy @@ -1,3619 +1,3819 @@ (* Title: Borůvka's Minimum Spanning Tree Algorithm Author: Nicolas Robinson-O'Brien Maintainer: Walter Guttmann *) section \Bor\r{u}vka's Minimum Spanning Tree Algorithm\ text \ In this theory we prove partial correctness of Bor\r{u}vka's minimum spanning tree algorithm. \ theory Boruvka imports Relational_Disjoint_Set_Forests.Disjoint_Set_Forests Kruskal begin subsection \General results\ text \ The proof is carried out in $m$-$k$-Stone-Kleene relation algebras. In this section we give results that hold more generally. \ context stone_kleene_relation_algebra begin -definition "big_forest H d \ - equivalence H - \ d \ -H - \ univalent (H * d) - \ H \ d * d\<^sup>T \ 1 - \ (H * d)\<^sup>+ \ - H" - -definition "bf_between_points p q H d \ point p \ point q \ p \ (H * d)\<^sup>\ * H * d" - -definition "bf_between_arcs a b H d \ arc a \ arc b \ a\<^sup>T * top \ (H * d)\<^sup>\ * H * b * top" - -text \Theorem 3\ - lemma He_eq_He_THe_star: assumes "arc e" and "equivalence H" shows "H * e = H * e * (top * H * e)\<^sup>\" proof - let ?x = "H * e" have 1: "H * e \ H * e * (top * H * e)\<^sup>\" using comp_isotone star.circ_reflexive by fastforce have "H * e * (top * H * e)\<^sup>\ = H * e * (top * e)\<^sup>\" by (metis assms(2) preorder_idempotent surjective_var) also have "... \ H * e * (1 \ top * (e * top)\<^sup>\ * 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)\<^sup>\ \ 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))\<^sup>\ = (H * d)\<^sup>\ \ (H * d)\<^sup>\ * H * e * (H * d)\<^sup>\" proof - have "H * e * (H * d)\<^sup>\ * 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)\<^sup>\ * H * e \ H * e" by simp have "(H * (d \ e))\<^sup>\ = (H * d \ H * e)\<^sup>\" by (simp add: comp_left_dist_sup) also have "... = (H * d)\<^sup>\ \ (H * d)\<^sup>\ * H * e * (H * d)\<^sup>\" 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\<^sup>T \ - p) \ (f \ - e\<^sup>T \ p) \ (f \ - e\<^sup>T \ p)\<^sup>T \ (f \ - e\<^sup>T \ - p)\<^sup>T \ e\<^sup>T \ e = f \ f\<^sup>T \ e \ e\<^sup>T" proof - have "(f \ - e\<^sup>T \ - p) \ (f \ - e\<^sup>T \ p) \ (f \ - e\<^sup>T \ p)\<^sup>T \ (f \ - e\<^sup>T \ - p)\<^sup>T \ e\<^sup>T \ e = (f \ - e\<^sup>T \ - p) \ (f \ - e\<^sup>T \ p) \ (f\<^sup>T \ - e \ p\<^sup>T) \ (f\<^sup>T \ - e \ - p\<^sup>T) \ e\<^sup>T \ e" by (simp add: conv_complement conv_dist_inf) also have "... = ((f \ (f \ - e\<^sup>T \ p)) \ (- e\<^sup>T \ (f \ - e\<^sup>T \ p)) \ (- p \ (f \ - e\<^sup>T \ p))) \ ((f\<^sup>T \ (f\<^sup>T \ - e \ - p\<^sup>T)) \ (- e \ (f\<^sup>T \ - e \ - p\<^sup>T)) \ (p\<^sup>T \ (f\<^sup>T \ - e \ - p\<^sup>T))) \ e\<^sup>T \ e" by (metis sup_inf_distrib2 sup_assoc) also have "... = ((f \ f) \ (f \ - e\<^sup>T) \ (f \ p) \ (- e\<^sup>T \ f) \ (- e\<^sup>T \ - e\<^sup>T) \ (- e\<^sup>T \ p) \ (- p \ f) \ (- p \ - e\<^sup>T) \ (- p \ p)) \ ((f\<^sup>T \ f\<^sup>T) \ (f\<^sup>T \ - e) \ (f\<^sup>T \ - p\<^sup>T) \ (- e \ f\<^sup>T) \ (- e \ - e) \ (- e \ - p\<^sup>T) \ (p\<^sup>T \ f\<^sup>T) \ (p\<^sup>T \ - e) \ (p\<^sup>T \ - p\<^sup>T)) \ e\<^sup>T \ e" using sup_inf_distrib1 sup_assoc inf_assoc sup_inf_distrib1 by simp also have "... = ((f \ f) \ (f \ - e\<^sup>T) \ (f \ p) \ (f \ - p) \ (- e\<^sup>T \ f) \ (- e\<^sup>T \ - e\<^sup>T) \ (- e\<^sup>T \ p) \ (- e\<^sup>T \ - p) \ (- p \ p)) \ ((f\<^sup>T \ f\<^sup>T) \ (f\<^sup>T \ - e) \ (f\<^sup>T \ - p\<^sup>T) \ (- e \ f\<^sup>T) \ (f\<^sup>T \ p\<^sup>T) \ (- e \ - e) \ (- e \ - p\<^sup>T) \ (- e \ p\<^sup>T) \ (p\<^sup>T \ - p\<^sup>T)) \ e\<^sup>T \ e" by (smt abel_semigroup.commute inf.abel_semigroup_axioms inf.left_commute sup.abel_semigroup_axioms) also have "... = (f \ - e\<^sup>T \ (- p \ p)) \ (f\<^sup>T \ - e \ (p\<^sup>T \ - p\<^sup>T)) \ e\<^sup>T \ e" by (smt inf.sup_monoid.add_assoc inf.sup_monoid.add_commute inf_sup_absorb sup.idem) also have "... = (f \ - e\<^sup>T) \ (f\<^sup>T \ - e) \ e\<^sup>T \ e" by (metis assms(1) conv_complement inf_top_right stone) also have "... = (f \ e\<^sup>T) \ (- e\<^sup>T \ e\<^sup>T) \ (f\<^sup>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\<^sup>T \ - p \ (f \ - e\<^sup>T \ p)\<^sup>T \ e)" and "injective f" shows "forest_components ((f \ - e\<^sup>T \ - p) \ (f \ -e\<^sup>T \ p)\<^sup>T \ e) = (f \ f\<^sup>T \ e \ e\<^sup>T)\<^sup>\" proof - have "forest_components ((f \ - e\<^sup>T \ - p) \ (f \ -e\<^sup>T \ p)\<^sup>T \ e) = wcc ((f \ - e\<^sup>T \ - p) \ (f \ - e\<^sup>T \ p)\<^sup>T \ e)" by (simp add: assms(3) forest_components_wcc) also have "... = ((f \ - e\<^sup>T \ - p) \ (f \ - e\<^sup>T \ p)\<^sup>T \ e \ (f \ - e\<^sup>T \ - p)\<^sup>T \ (f \ - e\<^sup>T \ p) \ e\<^sup>T)\<^sup>\" using conv_dist_sup sup_assoc by auto also have "... = ((f \ - e\<^sup>T \ - p) \ (f \ - e\<^sup>T \ p) \ (f \ - e\<^sup>T \ p)\<^sup>T \ (f \ - e\<^sup>T \ - p)\<^sup>T \ e\<^sup>T \ e)\<^sup>\" using sup_assoc sup_commute by auto also have "... = (f \ f\<^sup>T \ e \ e\<^sup>T)\<^sup>\" 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\<^sup>T \ - p \ (f \ - e\<^sup>T \ p)\<^sup>T \ e)" and "injective f" shows "forest_components f \ forest_components (f \ - e\<^sup>T \ - p \ (f \ - e\<^sup>T \ p)\<^sup>T \ e)" proof - have 1: "forest_components ((f \ - e\<^sup>T \ - p) \ (f \ -e\<^sup>T \ p)\<^sup>T \ e) = (f \ f\<^sup>T \ e \ e\<^sup>T)\<^sup>\" 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\<^sup>T \ e\<^sup>T \ e)\<^sup>\" by (simp add: le_supI2 star_isotone sup_commute) finally show ?thesis using 1 sup.left_commute sup_commute by simp qed lemma fch_equivalence: assumes "forest h" shows "equivalence (forest_components h)" by (simp add: assms forest_components_equivalence) -lemma big_forest_path_split_1: +lemma forest_modulo_equivalence_path_split_1: assumes "arc a" and "equivalence H" shows "(H * d)\<^sup>\ * H * a * top = (H * (d \ - a))\<^sup>\ * 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\<^sup>\ * ?a \ ?x\<^sup>\ * ?a" proof - have "?x\<^sup>\ *?y * ?x\<^sup>\ * ?a \ ?x\<^sup>\ * ?a * ?a" by (smt mult_left_isotone star.circ_right_top top_right_mult_increasing mult_assoc) also have "... = ?x\<^sup>\ * ?a * a * top" by (metis ex231e mult_assoc) also have "... = ?x\<^sup>\ * ?a" by (simp add: assms(1) mult_assoc) finally have 11: "?x\<^sup>\ *?y * ?x\<^sup>\ * ?a \ ?x\<^sup>\ * ?a" by simp have "?d\<^sup>\ * ?a = (?H * (d \ a) \ ?H * (d \ -a))\<^sup>\ * ?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)\<^sup>\ * ?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)\<^sup>\ * ?a" by (simp add: sup_commute mult_assoc) also have "... = ?x\<^sup>\ * ?a \ (?x\<^sup>\ * ?y * (?x\<^sup>\ * ?y)\<^sup>\ * ?x\<^sup>\) * ?a" by (smt mult_right_dist_sup star.circ_sup_9 star.circ_unfold_sum mult_assoc) also have "... \ ?x\<^sup>\ * ?a \ (?x\<^sup>\ * ?y * (top * ?y)\<^sup>\ * ?x\<^sup>\) * ?a" proof - have "(?x\<^sup>\ * ?y)\<^sup>\ \ (top * ?y)\<^sup>\" 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\<^sup>\ * ?a \ (?x\<^sup>\ * ?y * ?x\<^sup>\) * ?a" using assms(1, 2) He_eq_He_THe_star arc_regular mult_assoc by auto finally have 13: "(?H * d)\<^sup>\ * ?a \ ?x\<^sup>\ * ?a \ ?x\<^sup>\ * ?y * ?x\<^sup>\ * ?a" by (simp add: mult_assoc) have 14: "?x\<^sup>\ * ?y * ?x\<^sup>\ * ?a \ ?x\<^sup>\ * ?a" using 11 mult_assoc by auto thus ?thesis using 13 14 sup.absorb1 by auto qed have 2: "?d\<^sup>\ * ?a \ ?x\<^sup>\ *?a" by (simp add: comp_isotone star_isotone) thus ?thesis - using 1 2 antisym mult_assoc by simp + using 1 2 order.antisym mult_assoc by simp qed lemma dTransHd_le_1: assumes "equivalence H" and "univalent (H * d)" shows "d\<^sup>T * H * d \ 1" proof - have "d\<^sup>T * H\<^sup>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\<^sup>T \ 1" by (metis assms(2) conv_dist_comp symmetric_top_closed vector_top_closed mult_assoc) hence "a * top * a\<^sup>T * H \ H" using assms(1) comp_isotone order_trans by blast hence "a * top * top * a\<^sup>T * H \ H" by (simp add: vector_mult_closed) hence "a * top * (H * a * top)\<^sup>T \ H" by (metis assms(1) conv_dist_comp symmetric_top_closed vector_top_closed mult_assoc) thus ?thesis using assms(2) comp_injective_below_complement mult_assoc by auto qed -text \Theorem 4\ +subsection \Forests modulo an equivalence\ -lemma expand_big_forest: - assumes "big_forest H d" +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\<^sup>T \ 1 \ (x * d)\<^sup>+ \ x \ bot" + +definition "forest_modulo_equivalence_path a b H d \ arc a \ arc b \ a\<^sup>T * top \ (H * d)\<^sup>\ * 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)\<^sup>+" + 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)\<^sup>+" + 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\<^sup>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\<^sup>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\<^sup>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)\<^sup>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)\<^sup>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)\<^sup>+ \ -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)\<^sup>+ \ -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)\<^sup>T\<^sup>+ \ -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)\<^sup>T\<^sup>+ \ -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\<^sup>T * d \ d\<^sup>T * x\<^sup>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\<^sup>\ \ (x * d)\<^sup>\" + 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\<^sup>\ \ d * (x * d)\<^sup>\" + using mult_right_isotone by blast + also have "... \ x * d * (x * d)\<^sup>\" + 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\<^sup>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\<^sup>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\<^sup>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)\<^sup>\ * (x * d)\<^sup>T\<^sup>\ = ((x * d) \ (x * d)\<^sup>T)\<^sup>\" + 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)\<^sup>\ \ (x * d)\<^sup>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)\<^sup>T\<^sup>\ \ (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)\<^sup>\ * (x * d)\<^sup>T\<^sup>\ \ (x * d)\<^sup>T * (x * d) \ 1" +proof - + have "(x * d)\<^sup>\ \ (x * d)\<^sup>T * (x * d) = (1 \ (x * d)\<^sup>+) \ (x * d)\<^sup>T * (x * d)" + using star_left_unfold_equal by simp + also have "... = (1 \ (x * d)\<^sup>T * (x * d)) \ ((x * d)\<^sup>+ \ (x * d)\<^sup>T * (x * d))" + using comp_inf.semiring.distrib_right by simp + also have "... \ 1 \ ((x * d)\<^sup>+ \ (x * d)\<^sup>T * (x * d))" + using inf.cobounded1 semiring.add_right_mono by blast + also have "... = 1 \ ((x * d)\<^sup>\ \ (x * d)\<^sup>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)\<^sup>\ \ (x * d)\<^sup>T * (x * d) \ 1" + by simp + then have 3: "(x * d)\<^sup>T\<^sup>\ \ (x * d)\<^sup>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)\<^sup>\ \ (x * d)\<^sup>T\<^sup>\) \ ((x * d)\<^sup>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\<^sup>T)\<^sup>+ * x * d * x * d\<^sup>T \ (x * d\<^sup>T)\<^sup>+" +proof - + have "(x * d\<^sup>T)\<^sup>+ * x * d * x * d\<^sup>T = (x * d\<^sup>T)\<^sup>\ * x * d\<^sup>T * x * d * x * d\<^sup>T" + using comp_associative star.circ_plus_same by metis + also have "... \ (x * d\<^sup>T)\<^sup>\ * x * 1 * x * d\<^sup>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\<^sup>T)\<^sup>\ * x * d\<^sup>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))\<^sup>T * x * (d \ c) \ (x * d)\<^sup>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)\<^sup>T))" + proof - + have "x \ (d \ c) * (d \ c)\<^sup>T \ x \ d * d\<^sup>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))\<^sup>+ \ x \ bot" + proof - + have "(x * (d \ c))\<^sup>+ \ (x * d)\<^sup>+" + 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\<^sup>T * H)\<^sup>\ * (H * d)\<^sup>\ = (d\<^sup>T * H)\<^sup>\ \ (H * d)\<^sup>\" proof - have "(H * d)\<^sup>T * H * d \ 1" - using assms big_forest_def mult_assoc by auto + using assms forest_modulo_equivalence_def mult_assoc by auto hence "d\<^sup>T * H * H * d \ 1" - using assms big_forest_def conv_dist_comp by auto + using assms forest_modulo_equivalence_def conv_dist_comp by auto thus ?thesis by (simp add: cancel_separate_eq comp_associative) qed - -lemma big_forest_path_bot: +lemma forest_modulo_equivalence_path_bot: assumes "arc a" and "a \ d" - and "big_forest H d" + and "forest_modulo_equivalence H d" shows "(d \ - a)\<^sup>T * (H * a * top) \ bot" proof - have 1: "d\<^sup>T * H * d \ 1" - using assms(3) big_forest_def dTransHd_le_1 by blast + using assms(3) forest_modulo_equivalence_def dTransHd_le_1 by blast hence "d * - 1 * d\<^sup>T \ - H" using triple_schroeder_p by force hence "d * - 1 * d\<^sup>T \ 1 \ - H" by (simp add: le_supI2) hence "d * d\<^sup>T \ d * - 1 * d\<^sup>T \ 1 \ - H" - by (metis assms(3) big_forest_def inf_commute regular_one_closed shunting_p le_supI) + by (metis assms(3) forest_modulo_equivalence_def inf_commute regular_one_closed shunting_p le_supI) hence "d * 1 * d\<^sup>T \ d * - 1 * d\<^sup>T \ 1 \ - H" by simp hence "d * (1 \ - 1) * d\<^sup>T \ 1 \ - H" using comp_associative mult_right_dist_sup by (simp add: mult_left_dist_sup) hence "d * top * d\<^sup>T \ 1 \ - H" using regular_complement_top by auto hence "d * top * a\<^sup>T \ 1 \ - H" using assms(2) conv_isotone dual_order.trans mult_right_isotone by blast hence "d * (a * top)\<^sup>T \ 1 \ - H" by (simp add: comp_associative conv_dist_comp) hence "d \ (1 \ - H) * (a * top)" by (simp add: assms(1) shunt_bijective) hence "d \ a * top \ - H * a * top" by (simp add: comp_associative mult_right_dist_sup) also have "... \ a * top \ - (H * a * top)" - using assms(1, 3) HcompaT_le_compHaT big_forest_def sup_right_isotone by auto + 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\<^sup>T) * (top \ (H * a)\<^sup>T * d)" by (metis dedekind inf_commute) also have "... = d * top \ H * a * a\<^sup>T * H\<^sup>T * d" by (simp add: conv_dist_comp inf_vector_comp mult_assoc) also have "... \ d * top \ H * a * d\<^sup>T * H\<^sup>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\<^sup>T * H * d" - using assms(3) big_forest_def by auto + 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 big_forest_path_split_2: +lemma forest_modulo_equivalence_path_split_2: assumes "arc a" and "a \ d" - and "big_forest H d" + and "forest_modulo_equivalence H d" shows "(H * (d \ - a))\<^sup>\ * H * a * top = (H * ((d \ - a) \ (d \ - a)\<^sup>T))\<^sup>\ * H * a * top" proof - let ?lhs = "(H * (d \ - a))\<^sup>\ * H * a * top" have 1: "d\<^sup>T * H * d \ 1" - using assms(3) big_forest_def dTransHd_le_1 by blast + 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)\<^sup>T * (H * (d \ - a))\<^sup>\ * (H * a * top) = (d \ - a)\<^sup>T * H * (d \ - a) * (H * (d \ - a))\<^sup>\ * (H * a * top)" proof - have "(d \ - a)\<^sup>T * (H * (d \ - a))\<^sup>\ * (H * a * top) = (d \ - a)\<^sup>T * (1 \ H * (d \ - a) * (H * (d \ - a))\<^sup>\) * (H * a * top)" by (simp add: star_left_unfold_equal) also have "... = (d \ - a)\<^sup>T * H * a * top \ (d \ - a)\<^sup>T * H * (d \ - a) * (H * (d \ - a))\<^sup>\ * (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)\<^sup>T * H * (d \ - a) * (H * (d \ - a))\<^sup>\ * (H * a * top)" - by (metis assms(1, 2, 3) big_forest_path_bot mult_assoc le_bot) + 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\<^sup>T * H * d * (H * (d \ - a))\<^sup>\ * (H * a * top)" using conv_isotone inf.cobounded1 mult_isotone by auto also have "... \ 1 * (H * (d \ - a))\<^sup>\ * (H * a * top)" using 1 by (metis le_iff_sup mult_right_dist_sup) finally have 3: "(d \ - a)\<^sup>T * (H * (d \ - a))\<^sup>\ * (H * a * top) \ ?lhs" using mult_assoc by auto hence 4: "H * (d \ - a)\<^sup>T * (H * (d \ - a))\<^sup>\ * (H * a * top) \ ?lhs" proof - have "H * (d \ - a)\<^sup>T * (H * (d \ - a))\<^sup>\ * (H * a * top) \ H * (H * (d \ - a))\<^sup>\ * H * a * top" using 3 mult_right_isotone mult_assoc by auto also have "... = H * H * ((d \ - a) * H)\<^sup>\ * H * a * top" - by (metis assms(3) big_forest_def star_slide mult_assoc preorder_idempotent) + by (metis assms(3) forest_modulo_equivalence_def star_slide mult_assoc preorder_idempotent) also have "... = H * ((d \ - a) * H)\<^sup>\ * H * a * top" - using assms(3) big_forest_def preorder_idempotent by fastforce + using assms(3) forest_modulo_equivalence_def preorder_idempotent by fastforce finally show ?thesis - by (metis assms(3) big_forest_def preorder_idempotent star_slide mult_assoc) + by (metis assms(3) forest_modulo_equivalence_def preorder_idempotent star_slide mult_assoc) qed have 5: "(H * (d \ - a) \ H * (d \ - a)\<^sup>T) * (H * (d \ - a))\<^sup>\ * H * a * top \ ?lhs" proof - have 51: "H * (d \ - a) * (H * (d \ - a))\<^sup>\ * H * a * top \ (H * (d \ - a))\<^sup>\ * H * a * top" using star.left_plus_below_circ mult_left_isotone by simp have 52: "(H * (d \ - a) \ H * (d \ - a)\<^sup>T) * (H * (d \ - a))\<^sup>\ * H * a * top = H * (d \ - a) * (H * (d \ - a))\<^sup>\ * H * a * top \ H * (d \ - a)\<^sup>T * (H * (d \ - a))\<^sup>\ * H * a * top" using mult_right_dist_sup by auto hence "... \ (H * (d \ - a))\<^sup>\ * H * a * top \ H * (d \ - a)\<^sup>T * (H * (d \ - a))\<^sup>\ * 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)\<^sup>T)\<^sup>\ * H * a * top \ ?lhs" proof - have "(H * (d \ - a) \ H * (d \ - a)\<^sup>T)\<^sup>\ * (H * (d \ - a))\<^sup>\ * 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)\<^sup>T))\<^sup>\ * H * a * top \ ?lhs" using mult_left_dist_sup by auto have 7: "(H * (d \ - a))\<^sup>\ * H * a * top \ (H * ((d \ - a) \ (d \ - a)\<^sup>T))\<^sup>\ * 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 +context stone_relation_algebra +begin + +text \ +A \vector_classes\ corresponds to one or more equivalence classes and a \unique_vector_class\ corresponds to a single equivalence class. +\ + +definition vector_classes :: "'a \ 'a \ bool" where "vector_classes x v \ regular x \ regular v \ equivalence x \ vector v \ x * v \ v \ v \ bot" +definition unique_vector_class :: "'a \ 'a \ bool" where "unique_vector_class x v \ vector_classes x v \ v * v\<^sup>T \ x" + +end + subsection \An operation to select components\ text \ We introduce the operation \choose_component\. \begin{itemize} -\item Axiom \component_in_v\ expresses that the result of \choose_component\ is contained in the set of vertices, $v$, we are selecting from, ignoring the weights. -\item Axiom \component_is_vector\ states that the result of \choose_component\ is a vector. -\item Axiom \component_is_regular\ states that the result of \choose_component\ is regular. -\item Axiom \component_is_connected\ states that any two vertices from the result of \choose_component\ are connected in $e$. -\item Axiom \component_single\ states that the result of \choose_component\ is closed under being connected in $e$. -\item Finally, axiom \component_not_bot_when_v_bot_bot\ expresses that the operation \choose_component\ returns a non-empty component if the input satisfies the given criteria. + \item Axiom \component_in_v\ expresses that the result of \choose_component\ is contained in the set of vertices, $v$, we are selecting from, ignoring the weights. + \item Axiom \component_is_vector\ states that the result of \choose_component\ is a vector. + \item Axiom \component_is_regular\ states that the result of \choose_component\ is regular. + \item Axiom \component_is_connected\ states that any two vertices from the result of \choose_component\ are connected in $e$. + \item Axiom \component_single\ states that the result of \choose_component\ is closed under being connected in $e$. + \item Finally, axiom \component_not_bot_when_v_bot_bot\ expresses that the operation \choose_component\ returns a non-empty component if the input satisfies the given criteria. \end{itemize} \ class choose_component = fixes choose_component :: "'a \ 'a \ 'a" class choose_component_algebra = choose_component + stone_relation_algebra + - assumes component_in_v: "choose_component e v \ --v" - assumes component_is_vector: "vector (choose_component e v)" - assumes component_is_regular: "regular (choose_component e v)" - assumes component_is_connected: "choose_component e v * (choose_component e v)\<^sup>T \ e" - assumes component_single: "choose_component e v = e * choose_component e v" - assumes component_not_bot_when_v_bot_bot: " - regular e - \ equivalence e - \ vector v - \ regular v - \ e * v = v - \ v \ bot \ choose_component e v \ bot" - -text \Theorem 1\ + assumes component_is_vector: "vector (choose_component e v)" + assumes component_is_regular: "regular (choose_component e v)" + assumes component_in_v: "choose_component e v \ --v" + assumes component_is_connected: "choose_component e v * (choose_component e v)\<^sup>T \ e" + assumes component_single: "e * choose_component e v \ choose_component e v" + assumes component_not_bot_when_v_bot_bot: "vector_classes e v \ choose_component e v \ bot" text \ Every \m_kleene_algebra\ is an instance of \choose_component_algebra\ when the \choose_component\ operation is defined as follows: \ context m_kleene_algebra begin -definition "choose_component_input_condition e v \ - regular e - \ equivalence e - \ vector v - \ regular v - \ e * v = v" - definition "m_choose_component e v \ - if choose_component_input_condition e v then + if vector_classes e v then e * minarc(v) * top else bot" sublocale m_choose_component_algebra: choose_component_algebra where choose_component = m_choose_component proof fix e v show "m_choose_component e v \ -- v" - proof (cases "choose_component_input_condition e v") + proof (cases "vector_classes e v") case True hence "m_choose_component e v = e * minarc(v) * top" by (simp add: m_choose_component_def) also have "... \ e * --v * top" by (simp add: comp_isotone minarc_below) also have "... = e * v * top" - using True choose_component_input_condition_def by auto - also have "... = v * top" - using True choose_component_input_condition_def by auto + using True vector_classes_def by auto + also have "... \ v * top" + using True vector_classes_def mult_assoc by auto finally show ?thesis - using True choose_component_input_condition_def by auto + using True vector_classes_def by auto next case False hence "m_choose_component e v = bot" using False m_choose_component_def by auto thus ?thesis by simp qed next fix e v show "vector (m_choose_component e v)" - proof (cases "choose_component_input_condition e v") + proof (cases "vector_classes e v") case True thus ?thesis by (simp add: mult_assoc m_choose_component_def) next case False thus ?thesis by (simp add: m_choose_component_def) qed next fix e v show "regular (m_choose_component e v)" - using choose_component_input_condition_def minarc_regular regular_closed_star regular_mult_closed m_choose_component_def by auto + using minarc_regular regular_mult_closed vector_classes_def m_choose_component_def by auto next fix e v show "m_choose_component e v * (m_choose_component e v)\<^sup>T \ e" - proof (cases "choose_component_input_condition e v") + proof (cases "vector_classes e v") case True - assume 1: "choose_component_input_condition e v" + assume 1: "vector_classes e v" hence "m_choose_component e v * (m_choose_component e v)\<^sup>T = e * minarc(v) * top * (e * minarc(v) * top)\<^sup>T" by (simp add: m_choose_component_def) also have "... = e * minarc(v) * top * top\<^sup>T * minarc(v)\<^sup>T * e\<^sup>T" by (metis comp_associative conv_dist_comp) also have "... = e * minarc(v) * top * top * minarc(v)\<^sup>T * e" - using 1 choose_component_input_condition_def by auto + using True vector_classes_def by auto also have "... = e * minarc(v) * top * minarc(v)\<^sup>T * e" by (simp add: comp_associative) also have "... \ e" proof (cases "v = bot") case True thus ?thesis by (simp add: True minarc_bot) next case False assume 3: "v \ bot" hence "e * minarc(v) * top * minarc(v)\<^sup>T \ e * 1" using 3 minarc_arc arc_expanded comp_associative mult_right_isotone by fastforce hence "e * minarc(v) * top * minarc(v)\<^sup>T * e \ e * 1 * e" using mult_left_isotone by auto also have "... = e" - using 1 choose_component_input_condition_def preorder_idempotent by auto + using True preorder_idempotent vector_classes_def by auto thus ?thesis using calculation by auto qed thus ?thesis by (simp add: calculation) next case False thus ?thesis by (simp add: m_choose_component_def) qed next fix e v - show "m_choose_component e v = e * m_choose_component e v" - proof (cases "choose_component_input_condition e v") + show "e * m_choose_component e v \ m_choose_component e v" + proof (cases "vector_classes e v") case True thus ?thesis - by (metis choose_component_input_condition_def preorder_idempotent m_choose_component_def mult_assoc) + using comp_right_one dual_order.eq_iff mult_isotone vector_classes_def m_choose_component_def mult_assoc by metis next case False thus ?thesis by (simp add: m_choose_component_def) qed next fix e v - show "regular e \ equivalence e \ vector v \ regular v \ e * v = v \ v \ bot \ m_choose_component e v \ bot" - proof (cases "choose_component_input_condition e v") + show "vector_classes e v \ m_choose_component e v \ bot" + proof (cases "vector_classes e v") case True hence "m_choose_component e v \ minarc(v) * top" - by (metis choose_component_input_condition_def mult_1_left mult_left_isotone m_choose_component_def) + using vector_classes_def m_choose_component_def comp_associative minarc_arc shunt_bijective by fastforce also have "... \ minarc(v)" using calculation dual_order.trans top_right_mult_increasing by blast thus ?thesis - using True bot_unique minarc_bot_iff by fastforce + using le_bot minarc_bot_iff vector_classes_def by fastforce next case False thus ?thesis - using choose_component_input_condition_def by blast + by blast qed qed end subsection \m-k-Stone-Kleene relation algebras\ text \ $m$-$k$-Stone-Kleene relation algebras are an extension of $m$-Kleene algebras where the \choose_component\ operation has been added. \ class m_kleene_algebra_choose_component = m_kleene_algebra + choose_component_algebra begin text \ A \selected_edge\ is a minimum-weight edge whose source is in a component, with respect to $h$, $j$ and $g$, and whose target is not in that component. \ abbreviation "selected_edge h j g \ minarc (choose_component (forest_components h) j * - choose_component (forest_components h) j\<^sup>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\<^sup>T)\<^sup>T\<^sup>\" definition "boruvka_outer_invariant f g \ symmetric g \ forest f \ f \ --g \ regular f \ (\w . minimum_spanning_forest w g \ f \ w \ w\<^sup>T)" definition "boruvka_inner_invariant j f h g d \ boruvka_outer_invariant f g \ g \ bot - \ vector j - \ regular j - \ boruvka_outer_invariant h g - \ forest h - \ forest_components h \ forest_components f - \ big_forest (forest_components h) d + \ 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 - \ forest_components h * j = j - \ forest_components f = (forest_components h * (d \ d\<^sup>T))\<^sup>\ * forest_components h \ f \ f\<^sup>T = h \ h\<^sup>T \ d \ d\<^sup>T - \ (\ a b . bf_between_arcs a b (forest_components h) d \ a \ -(forest_components h) \ -- g \ b \ d - \ sum(b \ g) \ sum(a \ g)) - \ regular d" + \ (\ 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\<^sup>T = h \ h\<^sup>T \ d \ d\<^sup>T" + and "injective f" + and "injective h" + shows "forest_components f = (forest_components h * (d \ d\<^sup>T))\<^sup>\ * forest_components h" +proof - + have "forest_components f = (f \ f\<^sup>T)\<^sup>\" + using assms(2) cancel_separate_1 by simp + also have "... = (h \ h\<^sup>T \ d \ d\<^sup>T)\<^sup>\" + using assms(1) by auto + also have "... = ((h \ h\<^sup>T)\<^sup>\ * (d \ d\<^sup>T))\<^sup>\ * (h \ h\<^sup>T)\<^sup>\" + using star.circ_sup_9 sup_assoc by metis + also have "... = (forest_components h * (d \ d\<^sup>T))\<^sup>\ * forest_components h" + using assms(3) forest_components_wcc by simp + finally show ?thesis + by simp +qed + +lemma H_below_F: + assumes "f \ f\<^sup>T = h \ h\<^sup>T \ d \ d\<^sup>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\<^sup>T = h \ h\<^sup>T \ d \ d\<^sup>T" + and "f \ --g" + and "symmetric g" + shows "h \ --g" +proof - + have "h \ f \ f\<^sup>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)\<^sup>T \ - (path f h j g) \ (f \ - (selected_edge h j g)\<^sup>T \ (path f h j g))\<^sup>T \ (selected_edge h j g) = f \ - (path f h j g) \ (f \ (path f h j g))\<^sup>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\<^sup>T \ ?F" by (metis conv_dist_comp conv_involutive conv_order conv_star_commute forest_components_increasing) hence "- ?F \ - f\<^sup>T" using p_antitone by auto hence "?e \ - f\<^sup>T" using 1 dual_order.trans by blast hence "f\<^sup>T \ - ?e" by (simp add: p_antitone_iff) hence "f\<^sup>T\<^sup>T \ - ?e\<^sup>T" by (metis conv_complement conv_dist_inf inf.orderE inf.orderI) hence "f \ - ?e\<^sup>T" by auto hence "f = f \ - ?e\<^sup>T" using inf.orderE by blast hence "f \ - ?e\<^sup>T \ - ?p \ (f \ - ?e\<^sup>T \ ?p)\<^sup>T \ ?e = f \ - ?p \ (f \ ?p)\<^sup>T \ ?e" by auto thus ?thesis by auto qed -text \Theorem 2\ - text \ The source of the \selected_edge\ is contained in $j$, the vector describing those vertices still to be processed in the inner loop of Bor\r{u}vka's algorithm. \ lemma et_below_j: assumes "vector j" and "regular j" and "j \ bot" shows "selected_edge h j g * top \ j" proof - let ?e = "selected_edge h j g" let ?c = "choose_component (forest_components h) j" have "?e * top \ --(?c * -?c\<^sup>T \ g) * top" using comp_isotone minarc_below by blast also have "... = (--(?c * -?c\<^sup>T) \ --g) * top" by simp also have "... = (?c * -?c\<^sup>T \ --g) * top" using component_is_regular regular_mult_closed by auto also have "... = (?c \ -?c\<^sup>T \ --g) * top" by (metis component_is_vector conv_complement vector_complement_closed vector_covector) also have "... \ ?c * top" using inf.cobounded1 mult_left_isotone order_trans by blast also have "... \ j * top" by (metis assms(2) comp_inf.star.circ_sup_2 comp_isotone component_in_v) also have "... = j" by (simp add: assms(1)) finally show ?thesis by simp qed -subsubsection \Components of forests and big forests\ +subsubsection \Components of forests and forests modulo an equivalence\ text \ -We prove a number of properties about \big_forest\ and \forest_components\. +We prove a number of properties about \forest_modulo_equivalence\ and \forest_components\. \ +lemma component_single_eq: + assumes "equivalence x" + shows "choose_component x v = x * choose_component x v" +proof - + have 1: "choose_component x v \ x * choose_component x v" + by (meson component_is_connected ex231c mult_isotone order_lesseq_imp) + thus ?thesis + by (simp add: component_single order.antisym) +qed + 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\<^sup>T * ?c \ ?c" using 1 by simp hence "?H * - ?c \ - ?c" using component_is_regular schroeder_3_p by force hence "j \ ?H * - ?c \ j \ - ?c" using inf.sup_right_isotone by auto thus ?thesis using 2 3 order.antisym by simp qed -text \Theorem 5\ - text \ -There is a path in the \big_forest\ between edges $a$ and $b$ if and only if there is either a path in the \big_forest\ from $a$ to $b$ or one from $a$ to $c$ and one from $c$ to $b$. +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 big_forest_path_split_disj: +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 "bf_between_arcs a b H (d \ c) \ bf_between_arcs a b H d \ (bf_between_arcs a c H d \ bf_between_arcs c b H d)" + 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: "bf_between_arcs a b H (d \ c) \ bf_between_arcs a b H d \ (bf_between_arcs a c H d \ bf_between_arcs c b H d)" + 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: "bf_between_arcs a b H (d \ c)" + assume 11: "forest_modulo_equivalence_path a b H (d \ c)" hence "a\<^sup>T * top \ (H * (d \ c))\<^sup>\ * H * b * top" - by (simp add: bf_between_arcs_def) + by (simp add: forest_modulo_equivalence_path_def) also have "... = ((H * d)\<^sup>\ \ (H * d)\<^sup>\ * H * c * (H * d)\<^sup>\) * H * b * top" using assms(1, 2) path_through_components by simp also have "... = (H * d)\<^sup>\ * H * b * top \ (H * d)\<^sup>\ * H * c * (H * d)\<^sup>\ * H * b * top" by (simp add: mult_right_dist_sup) finally have 12:"a\<^sup>T * top \ (H * d)\<^sup>\ * H * b * top \ (H * d)\<^sup>\ * H * c * (H * d)\<^sup>\ * H * b * top" by simp have 13: "a\<^sup>T * top \ (H * d)\<^sup>\ * H * b * top \ a\<^sup>T * top \ (H * d)\<^sup>\ * H * c * (H * d)\<^sup>\ * H * b * top" proof (rule point_in_vector_sup) show "point (a\<^sup>T * top)" - using 11 bf_between_arcs_def mult_assoc by auto + using 11 forest_modulo_equivalence_path_def mult_assoc by auto next show "vector ((H * d)\<^sup>\ * H * b * top)" using vector_mult_closed by simp next show "regular ((H * d)\<^sup>\ * H * b * top)" using assms(3) pp_dist_comp pp_dist_star by auto next show "a\<^sup>T * top \ (H * d)\<^sup>\ * H * b * top \ (H * d)\<^sup>\ * H * c * (H * d)\<^sup>\ * H * b * top" using 12 by simp qed - thus "bf_between_arcs a b H d \ (bf_between_arcs a c H d \ bf_between_arcs c b H d)" + 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\<^sup>T * top \ (H * d)\<^sup>\ * H * b * top") case True assume "a\<^sup>T * top \ (H * d)\<^sup>\ * H * b * top" - hence "bf_between_arcs a b H d" - using 11 bf_between_arcs_def by auto + 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\<^sup>T * top \ (H * d)\<^sup>\ * H * c * (H * d)\<^sup>\ * H * b * top" using 13 by (simp add: False) hence 15: "a\<^sup>T * top \ (H * d)\<^sup>\ * H * c * top" by (metis mult_right_isotone order_lesseq_imp top_greatest mult_assoc) have "c\<^sup>T * top \ (H * d)\<^sup>\ * H * b * top" proof (rule ccontr) assume "\ c\<^sup>T * top \ (H * d)\<^sup>\ * H * b * top" hence "c\<^sup>T * top \ -((H * d)\<^sup>\ * 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)\<^sup>\ * H * b * top \ bot" using schroeder_3_p mult_assoc by auto thus "False" using 13 False sup.absorb_iff1 mult_assoc by auto qed - hence "bf_between_arcs a c H d \ bf_between_arcs c b H d" - using 11 15 assms(2) bf_between_arcs_def by auto + 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: "bf_between_arcs a b H d \ (bf_between_arcs a c H d \ bf_between_arcs c b H d) \ bf_between_arcs a b H (d \ c)" + 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: "bf_between_arcs a b H d \ bf_between_arcs a b H (d \ c)" + have 21: "forest_modulo_equivalence_path a b H d \ forest_modulo_equivalence_path a b H (d \ c)" proof (rule impI) - assume 22:"bf_between_arcs a b H d" + assume 22:"forest_modulo_equivalence_path a b H d" hence "a\<^sup>T * top \ (H * d)\<^sup>\ * H * b * top" - using bf_between_arcs_def by blast + using forest_modulo_equivalence_path_def by blast hence "a\<^sup>T * top \ (H * (d \ c))\<^sup>\ * H * b * top" by (simp add: mult_left_isotone mult_right_dist_sup mult_right_isotone order.trans star_isotone star_slide) - thus "bf_between_arcs a b H (d \ c)" - using 22 bf_between_arcs_def by blast + thus "forest_modulo_equivalence_path a b H (d \ c)" + using 22 forest_modulo_equivalence_path_def by blast qed - have "bf_between_arcs a c H d \ bf_between_arcs c b H d \ bf_between_arcs a b H (d \ c)" + 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: "bf_between_arcs a c H d \ bf_between_arcs c b H d" + assume 23: "forest_modulo_equivalence_path a c H d \ forest_modulo_equivalence_path c b H d" hence "a\<^sup>T * top \ (H * d)\<^sup>\ * H * c * top" - using bf_between_arcs_def by blast + using forest_modulo_equivalence_path_def by blast also have "... \ (H * d)\<^sup>\ * H * c * c\<^sup>T * c * top" by (metis ex231c comp_inf.star.circ_sup_2 mult_isotone mult_right_isotone mult_assoc) also have "... \ (H * d)\<^sup>\ * H * c * c\<^sup>T * top" by (simp add: mult_right_isotone mult_assoc) also have "... \ (H * d)\<^sup>\ * H * c * (H * d)\<^sup>\ * H * b * top" - using 23 mult_right_isotone mult_assoc by (simp add: bf_between_arcs_def) + using 23 mult_right_isotone mult_assoc by (simp add: forest_modulo_equivalence_path_def) also have "... \ (H * d)\<^sup>\ * H * b * top \ (H * d)\<^sup>\ * H * c * (H * d)\<^sup>\ * H * b * top" - by (simp add: bf_between_arcs_def) + by (simp add: forest_modulo_equivalence_path_def) finally have "a\<^sup>T * top \ (H * (d \ c))\<^sup>\ * H * b * top" using assms(1, 2) path_through_components mult_right_dist_sup by simp - thus "bf_between_arcs a b H (d \ c)" - using 23 bf_between_arcs_def by blast + 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\<^sup>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\<^sup>T * ?H * ?e \ (d * top)\<^sup>T * ?H * (?e * top)" by (simp add: comp_isotone conv_isotone top_right_mult_increasing) also have "... \ (d * top)\<^sup>T * ?H * j" using 1 mult_right_isotone by auto also have "... \ (- j)\<^sup>T * ?H * j" by (simp add: assms(3) conv_isotone mult_left_isotone) also have "... = (- j)\<^sup>T * j" using assms(4) comp_associative by auto also have "... = bot" by (simp add: assms(1) conv_complement covector_vector_comp) finally show ?thesis using coreflexive_bot_closed le_bot by blast qed -lemma big_forest_d_U_e: +lemma forest_modulo_equivalence_d_U_e: assumes "forest f" and "vector j" and "regular j" and "forest h" - and "forest_components h \ forest_components f" - and "big_forest (forest_components h) d" + and "forest_modulo_equivalence (forest_components h) d" and "d * top \ - j" and "forest_components h * j = j" and "f \ f\<^sup>T = h \ h\<^sup>T \ d \ d\<^sup>T" and "selected_edge h j g \ - forest_components f" - and "selected_edge h j g \ bot" and "j \ bot" - shows "big_forest (forest_components h) (d \ selected_edge h j g)" -proof (unfold big_forest_def, intro conjI) + 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" - show 01: "reflexive ?H" - by (simp add: assms(4) forest_components_equivalence) - show 02: "transitive ?H" - by (simp add: assms(4) forest_components_equivalence) - show 03: "symmetric ?H" - by (simp add: assms(4) forest_components_equivalence) - have 04: "equivalence ?H" - by (simp add: 01 02 03) - show 1: "?d' \ - ?H" - proof - - have "?H \ ?F" - by (simp add: assms(5)) - hence 11: "?e \ - ?H" - using assms(10) order_lesseq_imp p_antitone by blast - have "d \ - ?H" - using assms(6) big_forest_def by auto - thus ?thesis - by (simp add: 11) - qed - show "univalent (?H * ?d')" - proof - - have "(?H * ?d')\<^sup>T * (?H * ?d') = ?d'\<^sup>T * ?H\<^sup>T * ?H * ?d'" - using conv_dist_comp mult_assoc by auto - also have "... = ?d'\<^sup>T * ?H * ?H * ?d'" - by (simp add: conv_dist_comp conv_star_commute) - also have "... = ?d'\<^sup>T * ?H * ?d'" - using 01 02 by (metis preorder_idempotent mult_assoc) - finally have 21: "univalent (?H * ?d') \ ?e\<^sup>T * ?H * d \ d\<^sup>T * ?H * ?e \ ?e\<^sup>T * ?H * ?e \ d\<^sup>T * ?H * d \ 1" - using conv_dist_sup semiring.distrib_left semiring.distrib_right by auto - have 22: "?e\<^sup>T * ?H * ?e \ 1" + 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 221: "?e\<^sup>T * ?H * ?e \ ?e\<^sup>T * top * ?e" - by (simp add: mult_left_isotone mult_right_isotone) - have "arc ?e" - using assms(11) minarc_arc minarc_bot_iff by blast - hence "?e\<^sup>T * top * ?e \ 1" - using arc_expanded by blast - thus ?thesis - using 221 dual_order.trans by blast - qed - have 24: "d\<^sup>T * ?H * ?e \ 1" - by (metis assms(2, 3, 7, 8, 12) dT_He_eq_bot coreflexive_bot_closed le_bot) - hence "(d\<^sup>T * ?H * ?e)\<^sup>T \ 1\<^sup>T" - using conv_isotone by blast - hence "?e\<^sup>T * ?H\<^sup>T * d\<^sup>T\<^sup>T \ 1" - by (simp add: conv_dist_comp mult_assoc) - hence 25: "?e\<^sup>T * ?H * d \ 1" - using assms(4) fch_equivalence by auto - have 8: "d\<^sup>T * ?H * d \ 1" - using 04 assms(6) dTransHd_le_1 big_forest_def by blast - thus ?thesis - using 21 22 24 25 by simp - qed - show "coreflexive (?H \ ?d' * ?d'\<^sup>T)" - proof - - have "coreflexive (?H \ ?d' * ?d'\<^sup>T) \ ?H \ (d \ ?e) * (d\<^sup>T \ ?e\<^sup>T) \ 1" - by (simp add: conv_dist_sup) - also have "... \ ?H \ (d * d\<^sup>T \ d * ?e\<^sup>T \ ?e * d\<^sup>T \ ?e * ?e\<^sup>T) \ 1" - by (metis mult_left_dist_sup mult_right_dist_sup sup.left_commute sup_commute) - finally have 1: "coreflexive (?H \ ?d' * ?d'\<^sup>T) \ ?H \ d * d\<^sup>T \ ?H \ d * ?e\<^sup>T \ ?H \ ?e * d\<^sup>T \ ?H \ ?e * ?e\<^sup>T \ 1" - by (simp add: inf_sup_distrib1) - have 31: "?H \ d * d\<^sup>T \ 1" - using assms(6) big_forest_def by blast - have 32: "?H \ ?e * d\<^sup>T \ 1" - proof - - have "?e * d\<^sup>T \ ?e * top * (d * top)\<^sup>T" - by (simp add: conv_isotone mult_isotone top_right_mult_increasing) - also have "... \ ?e * top * - j\<^sup>T" - by (metis assms(7) conv_complement conv_isotone mult_right_isotone) - also have "... \ j * - j\<^sup>T" - using assms(2, 3, 12) et_below_j mult_left_isotone by auto - also have "... \ - ?H" - using 03 by (metis assms(2, 3, 8) conv_complement conv_dist_comp equivalence_top_closed mult_left_isotone schroeder_3_p vector_top_closed) - finally have "?e * d\<^sup>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\<^sup>T \ 1" - proof - - have 331: "injective h" - by (simp add: assms(4)) - have "(?H \ ?e * d\<^sup>T)\<^sup>T \ 1" - using 32 coreflexive_conv_closed by auto - hence "?H \ (?e * d\<^sup>T)\<^sup>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\<^sup>T \ 1" - proof - - have 341:"arc ?e \ arc (?e\<^sup>T)" - using assms(11) minarc_arc minarc_bot_iff by auto - have "?H \ ?e * ?e\<^sup>T \ ?e * ?e\<^sup>T" - by auto + have "(?H * ?d')\<^sup>T * (?H * ?d') = ?d'\<^sup>T * ?H\<^sup>T * ?H * ?d'" + using conv_dist_comp mult_assoc by auto + also have "... = ?d'\<^sup>T * ?H * ?H * ?d'" + by (simp add: conv_dist_comp conv_star_commute) + also have "... = ?d'\<^sup>T * ?H * ?d'" + using 01 02 by (metis preorder_idempotent mult_assoc) + finally have 21: "univalent (?H * ?d') \ ?e\<^sup>T * ?H * d \ d\<^sup>T * ?H * ?e \ ?e\<^sup>T * ?H * ?e \ d\<^sup>T * ?H * d \ 1" + using conv_dist_sup semiring.distrib_left semiring.distrib_right by auto + have 22: "?e\<^sup>T * ?H * ?e \ 1" + proof - + have 221: "?e\<^sup>T * ?H * ?e \ ?e\<^sup>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\<^sup>T * top * ?e \ 1" + using arc_expanded by blast + thus ?thesis + using 221 dual_order.trans by blast + qed + have 24: "d\<^sup>T * ?H * ?e \ 1" + by (metis assms(2, 3, 6, 7, 10) dT_He_eq_bot coreflexive_bot_closed le_bot) + hence "(d\<^sup>T * ?H * ?e)\<^sup>T \ 1\<^sup>T" + using conv_isotone by blast + hence "?e\<^sup>T * ?H\<^sup>T * d\<^sup>T\<^sup>T \ 1" + by (simp add: conv_dist_comp mult_assoc) + hence 25: "?e\<^sup>T * ?H * d \ 1" + using assms(4) fch_equivalence by auto + have 8: "d\<^sup>T * ?H * d \ 1" + using 04 assms(5) dTransHd_le_1 forest_modulo_equivalence_def by blast thus ?thesis - using 341 arc_injective le_infI2 by blast + using 21 22 24 25 by simp qed - thus ?thesis - using 1 31 32 33 34 by simp - qed - show 4:"(?H * (d \ ?e))\<^sup>+ \ - ?H" - proof - - have "?e \ - ?F" - by (simp add: assms(10)) - hence "?F \ - ?e" - by (simp add: p_antitone_iff) - hence "?F\<^sup>T * ?F \ - ?e" - using assms(1) fch_equivalence by fastforce - hence "?F\<^sup>T * ?F * ?F\<^sup>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)\<^sup>\ * ?F * ?e * (?F * ?F)\<^sup>\ \ - ?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)\<^sup>\ * ?F * ?e * (?F)\<^sup>\" - by (simp add: assms(1) forest_components_star) - also have "... = (?F * ?F)\<^sup>\ * ?F * ?e * (?F * ?F)\<^sup>\" - using 43 by simp - finally show ?thesis - using 41 by simp - qed - hence 44: "(?H * d)\<^sup>\ * ?H * ?e * (?H * d)\<^sup>\ \ - ?H" + show "coreflexive (?H \ ?d' * ?d'\<^sup>T)" proof - - have 45: "?H \ ?F" - by (simp add: assms(5)) - hence 46:"?H * ?e \ ?F * ?e" - by (simp add: mult_left_isotone) - have "d \ f \ f\<^sup>T" - using assms(9) sup.left_commute sup_commute by auto - also have "... \ ?F" - by (metis forest_components_increasing le_supI2 star.circ_back_loop_fixpoint star.circ_increasing sup.bounded_iff) - finally have "d \ ?F" - by simp - hence "?H * d \ ?F * ?F" - using 45 mult_isotone by auto - hence 47: "(?H * d)\<^sup>\ \ (?F * ?F)\<^sup>\" - by (simp add: star_isotone) - hence "(?H * d)\<^sup>\ * ?H * ?e * (?H * d)\<^sup>\ \ (?H * d)\<^sup>\ * ?F * ?e * (?H * d)\<^sup>\" - using 46 by (metis mult_left_isotone mult_right_isotone mult_assoc) - also have "... \ (?F * ?F)\<^sup>\ * ?F * ?e * (?F * ?F)\<^sup>\" - 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 + have "coreflexive (?H \ ?d' * ?d'\<^sup>T) \ ?H \ (d \ ?e) * (d\<^sup>T \ ?e\<^sup>T) \ 1" + by (simp add: conv_dist_sup) + also have "... \ ?H \ (d * d\<^sup>T \ d * ?e\<^sup>T \ ?e * d\<^sup>T \ ?e * ?e\<^sup>T) \ 1" + by (metis mult_left_dist_sup mult_right_dist_sup sup.left_commute sup_commute) + finally have 1: "coreflexive (?H \ ?d' * ?d'\<^sup>T) \ ?H \ d * d\<^sup>T \ ?H \ d * ?e\<^sup>T \ ?H \ ?e * d\<^sup>T \ ?H \ ?e * ?e\<^sup>T \ 1" + by (simp add: inf_sup_distrib1) + have 31: "?H \ d * d\<^sup>T \ 1" + using assms(5) forest_modulo_equivalence_def by blast + have 32: "?H \ ?e * d\<^sup>T \ 1" + proof - + have "?e * d\<^sup>T \ ?e * top * (d * top)\<^sup>T" + by (simp add: conv_isotone mult_isotone top_right_mult_increasing) + also have "... \ ?e * top * - j\<^sup>T" + by (metis assms(6) conv_complement conv_isotone mult_right_isotone) + also have "... \ j * - j\<^sup>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\<^sup>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\<^sup>T \ 1" + proof - + have 331: "injective h" + by (simp add: assms(4)) + have "(?H \ ?e * d\<^sup>T)\<^sup>T \ 1" + using 32 coreflexive_conv_closed by auto + hence "?H \ (?e * d\<^sup>T)\<^sup>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\<^sup>T \ 1" + proof - + have 341:"arc ?e \ arc (?e\<^sup>T)" + using e_not_bot minarc_arc minarc_bot_iff by auto + have "?H \ ?e * ?e\<^sup>T \ ?e * ?e\<^sup>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 - have "(?H * (d \ ?e))\<^sup>+ = (?H * (d \ ?e))\<^sup>\ * (?H * (d \ ?e))" - using star.circ_plus_same by auto - also have "... = ((?H * d)\<^sup>\ \ (?H * d)\<^sup>\ * ?H * ?e * (?H * d)\<^sup>\) * (?H * (d \ ?e))" - using assms(4, 11) forest_components_equivalence minarc_arc minarc_bot_iff path_through_components by auto - also have "... = (?H * d)\<^sup>\ * (?H * (d \ ?e)) \ (?H * d)\<^sup>\ * ?H * ?e * (?H * d)\<^sup>\ * (?H * (d \ ?e))" - using mult_right_dist_sup by auto - also have "... = (?H * d)\<^sup>\ * (?H * d \ ?H * ?e) \ (?H * d)\<^sup>\ * ?H * ?e * (?H * d)\<^sup>\ * (?H * d \ ?H * ?e)" - by (simp add: mult_left_dist_sup) - also have "... = (?H * d)\<^sup>\ * ?H * d \ (?H * d)\<^sup>\ * ?H * ?e \ (?H * d)\<^sup>\ * ?H * ?e * (?H * d)\<^sup>\ * (?H * d \ ?H * ?e)" - using mult_left_dist_sup mult_assoc by auto - also have "... = (?H * d)\<^sup>+ \ (?H * d)\<^sup>\ * ?H * ?e \ (?H * d)\<^sup>\ * ?H * ?e * (?H * d)\<^sup>\ * (?H * d \ ?H * ?e)" - by (simp add: star.circ_plus_same mult_assoc) - also have "... = (?H * d)\<^sup>+ \ (?H * d)\<^sup>\ * ?H * ?e \ (?H * d)\<^sup>\ * ?H * ?e * (?H * d)\<^sup>\ * ?H * d \ (?H * d)\<^sup>\ * ?H * ?e * (?H * d)\<^sup>\ * ?H * ?e" - by (simp add: mult.semigroup_axioms semiring.distrib_left sup.semigroup_axioms semigroup.assoc) - also have "... \ (?H * d)\<^sup>+ \ (?H * d)\<^sup>\ * ?H * ?e \ (?H * d)\<^sup>\ * ?H * ?e * (?H * d)\<^sup>\ * ?H * d \ (?H * d)\<^sup>\ * ?H * ?e" + show 4:"(?H * (d \ ?e))\<^sup>+ \ ?H \ bot" proof - - have "?e * (?H * d)\<^sup>\ * ?H * ?e \ ?e * top * ?e" - by (metis comp_associative comp_inf.coreflexive_idempotent comp_inf.coreflexive_transitive comp_isotone top.extremum) - also have "... \ ?e" - using assms(11) arc_top_arc minarc_arc minarc_bot_iff by auto - finally have "?e * (?H * d)\<^sup>\ * ?H * ?e \ ?e" - by simp - hence "(?H * d)\<^sup>\ * ?H * ?e * (?H * d)\<^sup>\ * ?H * ?e \ (?H * d)\<^sup>\ * ?H * ?e" - by (simp add: comp_associative comp_isotone) - thus ?thesis - using sup_right_isotone by blast + have 40: "(?H * d)\<^sup>+ \ -?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\<^sup>T * ?F \ - ?e" + using assms(1) fch_equivalence by fastforce + hence "?F\<^sup>T * ?F * ?F\<^sup>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)\<^sup>\ * ?F * ?e * (?F * ?F)\<^sup>\ \ - ?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)\<^sup>\ * ?F * ?e * (?F)\<^sup>\" + by (simp add: assms(1) forest_components_star) + also have "... = (?F * ?F)\<^sup>\ * ?F * ?e * (?F * ?F)\<^sup>\" + using 43 by simp + finally show ?thesis + using 41 by simp + qed + hence 44: "(?H * d)\<^sup>\ * ?H * ?e * (?H * d)\<^sup>\ \ - ?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\<^sup>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)\<^sup>\ \ (?F * ?F)\<^sup>\" + by (simp add: star_isotone) + hence "(?H * d)\<^sup>\ * ?H * ?e * (?H * d)\<^sup>\ \ (?H * d)\<^sup>\ * ?F * ?e * (?H * d)\<^sup>\" + using 46 by (metis mult_left_isotone mult_right_isotone mult_assoc) + also have "... \ (?F * ?F)\<^sup>\ * ?F * ?e * (?F * ?F)\<^sup>\" + 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))\<^sup>+ = (?H * (d \ ?e))\<^sup>\ * (?H * (d \ ?e))" + using star.circ_plus_same by auto + also have "... = ((?H * d)\<^sup>\ \ (?H * d)\<^sup>\ * ?H * ?e * (?H * d)\<^sup>\) * (?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)\<^sup>\ * (?H * (d \ ?e)) \ (?H * d)\<^sup>\ * ?H * ?e * (?H * d)\<^sup>\ * (?H * (d \ ?e))" + using mult_right_dist_sup by auto + also have "... = (?H * d)\<^sup>\ * (?H * d \ ?H * ?e) \ (?H * d)\<^sup>\ * ?H * ?e * (?H * d)\<^sup>\ * (?H * d \ ?H * ?e)" + by (simp add: mult_left_dist_sup) + also have "... = (?H * d)\<^sup>\ * ?H * d \ (?H * d)\<^sup>\ * ?H * ?e \ (?H * d)\<^sup>\ * ?H * ?e * (?H * d)\<^sup>\ * (?H * d \ ?H * ?e)" + using mult_left_dist_sup mult_assoc by auto + also have "... = (?H * d)\<^sup>+ \ (?H * d)\<^sup>\ * ?H * ?e \ (?H * d)\<^sup>\ * ?H * ?e * (?H * d)\<^sup>\ * (?H * d \ ?H * ?e)" + by (simp add: star.circ_plus_same mult_assoc) + also have "... = (?H * d)\<^sup>+ \ (?H * d)\<^sup>\ * ?H * ?e \ (?H * d)\<^sup>\ * ?H * ?e * (?H * d)\<^sup>\ * ?H * d \ (?H * d)\<^sup>\ * ?H * ?e * (?H * d)\<^sup>\ * ?H * ?e" + by (simp add: mult.semigroup_axioms semiring.distrib_left sup.semigroup_axioms semigroup.assoc) + also have "... \ (?H * d)\<^sup>+ \ (?H * d)\<^sup>\ * ?H * ?e \ (?H * d)\<^sup>\ * ?H * ?e * (?H * d)\<^sup>\ * ?H * d \ (?H * d)\<^sup>\ * ?H * ?e" + proof - + have "?e * (?H * d)\<^sup>\ * ?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)\<^sup>\ * ?H * ?e \ ?e" + by simp + hence "(?H * d)\<^sup>\ * ?H * ?e * (?H * d)\<^sup>\ * ?H * ?e \ (?H * d)\<^sup>\ * ?H * ?e" + by (simp add: comp_associative comp_isotone) + thus ?thesis + using sup_right_isotone by blast + qed + also have "... = (?H * d)\<^sup>+ \ (?H * d)\<^sup>\ * ?H * ?e \ (?H * d)\<^sup>\ * ?H * ?e * (?H * d)\<^sup>\ * ?H * d" + by (simp add: order.eq_iff ac_simps) + also have "... = (?H * d)\<^sup>+ \ (?H * d)\<^sup>\ * ?H * ?e \ (?H * d)\<^sup>\ * ?H * ?e * (?H * d)\<^sup>+" + using star.circ_plus_same mult_assoc by auto + also have "... = (?H * d)\<^sup>+ \ (?H * d)\<^sup>\ * ?H * ?e * (1 \ (?H * d)\<^sup>+)" + by (simp add: mult_left_dist_sup sup_assoc) + also have "... = (?H * d)\<^sup>+ \ (?H * d)\<^sup>\ * ?H * ?e * (?H * d)\<^sup>\" + 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 - also have "... = (?H * d)\<^sup>+ \ (?H * d)\<^sup>\ * ?H * ?e \ (?H * d)\<^sup>\ * ?H * ?e * (?H * d)\<^sup>\ * ?H * d" - by (simp add: order.eq_iff ac_simps) - also have "... = (?H * d)\<^sup>+ \ (?H * d)\<^sup>\ * ?H * ?e \ (?H * d)\<^sup>\ * ?H * ?e * (?H * d)\<^sup>+" - using star.circ_plus_same mult_assoc by auto - also have "... = (?H * d)\<^sup>+ \ (?H * d)\<^sup>\ * ?H * ?e * (1 \ (?H * d)\<^sup>+)" - by (simp add: mult_left_dist_sup sup_assoc) - also have "... = (?H * d)\<^sup>+ \ (?H * d)\<^sup>\ * ?H * ?e * (?H * d)\<^sup>\" - by (simp add: star_left_unfold_equal) - also have "... \ - ?H" - using 44 assms(6) big_forest_def by auto - finally show ?thesis - by simp qed + 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 "big_forest H d" - and "bf_between_arcs a e H d" + assumes "forest_modulo_equivalence H d" + and "forest_modulo_equivalence_path a e H d" and "H * d * (H * d)\<^sup>\ \ - H" and "\ a\<^sup>T * top \ H * e * top" and "regular a" and "regular e" and "regular H" and "regular d" shows "arc (d \ top * e\<^sup>T * H \ (H * d\<^sup>T)\<^sup>\ * H * a\<^sup>T * top)" proof - let ?x = "d \ top * e\<^sup>T * H \ (H * d\<^sup>T)\<^sup>\ * H * a\<^sup>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\<^sup>T * top * a \ 1" - using arc_expanded assms(2) bf_between_arcs_def by auto + using arc_expanded assms(2) forest_modulo_equivalence_path_def by auto have 3: "e * top * e\<^sup>T \ 1" - using assms(2) bf_between_arcs_def arc_expanded by blast + using assms(2) forest_modulo_equivalence_path_def arc_expanded by blast have 4: "top * ?x * top = top" proof - have "a\<^sup>T * top \ (H * d)\<^sup>\ * H * e * top" - using assms(2) bf_between_arcs_def by blast + using assms(2) forest_modulo_equivalence_path_def by blast also have "... = H * e * top \ (H * d)\<^sup>\ * H * d * H * e * top" by (metis star.circ_loop_fixpoint star.circ_plus_same sup_commute mult_assoc) finally have "a\<^sup>T * top \ H * e * top \ (H * d)\<^sup>\ * H * d * H * e * top" by simp hence "a\<^sup>T * top \ H * e * top \ a\<^sup>T * top \ (H * d)\<^sup>\ * H * d * H * e * top" - using assms(2, 6, 7) point_in_vector_sup bf_between_arcs_def regular_mult_closed vector_mult_closed by auto + using assms(2, 6, 7) point_in_vector_sup forest_modulo_equivalence_path_def regular_mult_closed vector_mult_closed by auto hence "a\<^sup>T * top \ (H * d)\<^sup>\ * H * d * H * e * top" using assms(4) by blast also have "... = (H * d)\<^sup>\ * H * d * (H * e * top \ H * e * top)" by (simp add: mult_assoc) also have "... = (H * d)\<^sup>\ * H * (d \ (H * e * top)\<^sup>T) * H * e * top" by (metis comp_associative covector_inf_comp_3 star.circ_left_top star.circ_top) also have "... = (H * d)\<^sup>\ * H * (d \ top\<^sup>T * e\<^sup>T * H\<^sup>T) * H * e * top" using conv_dist_comp mult_assoc by auto also have "... = (H * d)\<^sup>\ * H * (d \ top * e\<^sup>T * H) * H * e * top" - using assms(1) by (simp add: big_forest_def) + using assms(1) by (simp add: forest_modulo_equivalence_def) finally have 2: "a\<^sup>T * top \ (H * d)\<^sup>\ * H * (d \ top * e\<^sup>T * H) * H * e * top" by simp hence "e * top \ ((H * d)\<^sup>\ * H * (d \ top * e\<^sup>T * H) * H)\<^sup>T * a\<^sup>T * top" proof - have "bijective (e * top) \ bijective (a\<^sup>T * top)" - using assms(2) bf_between_arcs_def by auto + using assms(2) forest_modulo_equivalence_path_def by auto thus ?thesis using 2 by (metis bijective_reverse mult_assoc) qed also have "... = H\<^sup>T * (d \ top * e\<^sup>T * H)\<^sup>T * H\<^sup>T * (H * d)\<^sup>\\<^sup>T * a\<^sup>T * top" by (simp add: conv_dist_comp mult_assoc) also have "... = H * (d \ top * e\<^sup>T * H)\<^sup>T * H * (H * d)\<^sup>\\<^sup>T * a\<^sup>T * top" - using assms(1) big_forest_def by auto + using assms(1) forest_modulo_equivalence_def by auto also have "... = H * (d \ top * e\<^sup>T * H)\<^sup>T * H * (d\<^sup>T * H)\<^sup>\ * a\<^sup>T * top" - using assms(1) big_forest_def conv_dist_comp conv_star_commute by auto + using assms(1) forest_modulo_equivalence_def conv_dist_comp conv_star_commute by auto also have "... = H * (d\<^sup>T \ H * e * top) * H * (d\<^sup>T * H)\<^sup>\ * a\<^sup>T * top" - using assms(1) conv_dist_comp big_forest_def comp_associative conv_dist_inf by auto + using assms(1) conv_dist_comp forest_modulo_equivalence_def comp_associative conv_dist_inf by auto also have "... = H * (d\<^sup>T \ H * e * top) * (H * d\<^sup>T)\<^sup>\ * H * a\<^sup>T * top" by (simp add: comp_associative star_slide) also have "... = H * (d\<^sup>T \ H * e * top) * ((H * d\<^sup>T)\<^sup>\ * H * a\<^sup>T * top \ (H * d\<^sup>T)\<^sup>\ * H * a\<^sup>T * top)" using mult_assoc by auto also have "... = H * (d\<^sup>T \ H * e * top \ ((H * d\<^sup>T)\<^sup>\ * H * a\<^sup>T * top)\<^sup>T) * (H * d\<^sup>T)\<^sup>\ * H * a\<^sup>T * top" by (smt comp_inf_vector covector_comp_inf vector_conv_covector vector_top_closed mult_assoc) also have "... = H * (d\<^sup>T \ (top * e\<^sup>T * H)\<^sup>T \ ((H * d\<^sup>T)\<^sup>\ * H * a\<^sup>T * top)\<^sup>T) * (H * d\<^sup>T)\<^sup>\ * H * a\<^sup>T * top" - using assms(1) big_forest_def conv_dist_comp mult_assoc by auto + using assms(1) forest_modulo_equivalence_def conv_dist_comp mult_assoc by auto also have "... = H * (d \ top * e\<^sup>T * H \ (H * d\<^sup>T)\<^sup>\ * H * a\<^sup>T * top)\<^sup>T * (H * d\<^sup>T)\<^sup>\ * H * a\<^sup>T * top" by (simp add: conv_dist_inf) finally have 3: "e * top \ H * ?x\<^sup>T * (H * d\<^sup>T)\<^sup>\ * H * a\<^sup>T * top" by auto have "?x \ bot" proof (rule ccontr) assume "\ ?x \ bot" hence "e * top = bot" using 3 le_bot by auto thus "False" - using assms(2, 4) bf_between_arcs_def mult_assoc semiring.mult_zero_right by auto + 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\<^sup>T \ 1" proof - have 51: "H * (d * H)\<^sup>\ \ d * H * d\<^sup>T \ 1" proof - have 511: "d * (H * d)\<^sup>\ \ - H" - using assms(1, 3) big_forest_def preorder_idempotent schroeder_4_p triple_schroeder_p by fastforce + using assms(1, 3) forest_modulo_equivalence_def preorder_idempotent schroeder_4_p triple_schroeder_p by fastforce hence "(d * H)\<^sup>\ * d \ - H" using star_slide by auto hence "H * (d\<^sup>T * H)\<^sup>\ \ - d" - by (smt assms(1) big_forest_def conv_dist_comp conv_star_commute schroeder_4_p star_slide) + by (smt assms(1) forest_modulo_equivalence_def conv_dist_comp conv_star_commute schroeder_4_p star_slide) hence "H * (d * H)\<^sup>\ \ - d\<^sup>T" - using 511 by (metis assms(1) big_forest_def schroeder_5_p star_slide) + using 511 by (metis assms(1) forest_modulo_equivalence_def schroeder_5_p star_slide) hence "H * (d * H)\<^sup>\ \ - (H * d\<^sup>T)" by (metis assms(3) p_antitone_iff schroeder_4_p star_slide mult_assoc) hence "H * (d * H)\<^sup>\ \ H * d\<^sup>T \ bot" by (simp add: bot_unique pseudo_complement) hence "H * d * (H * (d * H)\<^sup>\ \ H * d\<^sup>T) \ 1" by (simp add: bot_unique) hence 512: "H * d * H * (d * H)\<^sup>\ \ H * d * H * d\<^sup>T \ 1" - using univalent_comp_left_dist_inf assms(1) big_forest_def mult_assoc by fastforce + using univalent_comp_left_dist_inf assms(1) forest_modulo_equivalence_def mult_assoc by fastforce hence 513: "H * d * H * (d * H)\<^sup>\ \ d * H * d\<^sup>T \ 1" proof - have "d * H * d\<^sup>T \ H * d * H * d\<^sup>T" - by (metis assms(1) big_forest_def conv_dist_comp conv_involutive mult_1_right mult_left_isotone) + 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\<^sup>T * H * d \ 1 \ - H" - using assms(1) big_forest_def dTransHd_le_1 le_supI1 by blast + using assms(1) forest_modulo_equivalence_def dTransHd_le_1 le_supI1 by blast hence "(- 1 \ H) * d\<^sup>T * H \ - d\<^sup>T" - by (metis assms(1) big_forest_def dTransHd_le_1 inf.sup_monoid.add_commute le_infI2 p_antitone_iff regular_one_closed schroeder_4_p mult_assoc) + 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\<^sup>T \ - H" - by (metis assms(1) big_forest_def conv_dist_comp schroeder_3_p triple_schroeder_p) + by (metis assms(1) forest_modulo_equivalence_def conv_dist_comp schroeder_3_p triple_schroeder_p) hence "H \ d * (- 1 \ H) * d\<^sup>T \ 1" by (metis inf.coboundedI1 p_antitone_iff p_shunting_swap regular_one_closed) hence "H \ d * d\<^sup>T \ H \ d * (- 1 \ H) * d\<^sup>T \ 1" - using assms(1) big_forest_def le_supI by blast + using assms(1) forest_modulo_equivalence_def le_supI by blast hence "H \ (d * 1 * d\<^sup>T \ d * (- 1 \ H) * d\<^sup>T) \ 1" using comp_inf.semiring.distrib_left by auto hence "H \ (d * (1 \ (- 1 \ H)) * d\<^sup>T) \ 1" by (simp add: mult_left_dist_sup mult_right_dist_sup) hence 514: "H \ d * H * d\<^sup>T \ 1" - by (metis assms(1) big_forest_def comp_inf.semiring.distrib_left inf.le_iff_sup inf.sup_monoid.add_commute inf_top_right regular_one_closed stone) + 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\<^sup>T \ H * d * H * (d * H)\<^sup>\ \ d * H * d\<^sup>T \ 1" using 513 514 by simp hence "d * H * d\<^sup>T \ (H \ H * d * H * (d * H)\<^sup>\) \ 1" by (simp add: comp_inf.semiring.distrib_left inf.sup_monoid.add_commute) hence "d * H * d\<^sup>T \ H * (1 \ d * H * (d * H)\<^sup>\) \ 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\<^sup>T = (d \ top * e\<^sup>T * H \ (H * d\<^sup>T)\<^sup>\ * H * a\<^sup>T * top) * top * (d\<^sup>T \ H\<^sup>T * e\<^sup>T\<^sup>T * top\<^sup>T \ top\<^sup>T * a\<^sup>T\<^sup>T * H\<^sup>T * (d\<^sup>T\<^sup>T * H\<^sup>T)\<^sup>\)" by (simp add: conv_dist_comp conv_dist_inf conv_star_commute mult_assoc) also have "... = (d \ top * e\<^sup>T * H \ (H * d\<^sup>T)\<^sup>\ * H * a\<^sup>T * top) * top * (d\<^sup>T \ H * e * top \ top * a * H * (d * H)\<^sup>\)" - using assms(1) big_forest_def by auto + using assms(1) forest_modulo_equivalence_def by auto also have "... = (H * d\<^sup>T)\<^sup>\ * H * a\<^sup>T * top \ (d \ top * e\<^sup>T * H) * top * (d\<^sup>T \ H * e * top \ top * a * H * (d * H)\<^sup>\)" by (metis inf_vector_comp vector_export_comp) also have "... = (H * d\<^sup>T)\<^sup>\ * H * a\<^sup>T * top \ (d \ top * e\<^sup>T * H) * top * top * (d\<^sup>T \ H * e * top \ top * a * H * (d * H)\<^sup>\)" by (simp add: vector_mult_closed) also have "... = (H * d\<^sup>T)\<^sup>\ * H * a\<^sup>T * top \ d * ((top * e\<^sup>T * H)\<^sup>T \ top) * top * (d\<^sup>T \ H * e * top \ top * a * H * (d * H)\<^sup>\)" by (simp add: covector_comp_inf_1 covector_mult_closed) also have "... = (H * d\<^sup>T)\<^sup>\ * H * a\<^sup>T * top \ d * ((top * e\<^sup>T * H)\<^sup>T \ (H * e * top)\<^sup>T) * d\<^sup>T \ top * a * H * (d * H)\<^sup>\" 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\<^sup>T)\<^sup>\ * H * a\<^sup>T * top \ top * a * H * (d * H)\<^sup>\ \ d * ((top * e\<^sup>T * H)\<^sup>T \ (H * e * top)\<^sup>T) * d\<^sup>T" using inf.sup_monoid.add_assoc inf.sup_monoid.add_commute by auto also have "... = (H * d\<^sup>T)\<^sup>\ * H * a\<^sup>T * top * top * a * H * (d * H)\<^sup>\ \ d * ((top * e\<^sup>T * H)\<^sup>T \ (H * e * top)\<^sup>T) * d\<^sup>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\<^sup>T)\<^sup>\ * H * a\<^sup>T * top * a * H * (d * H)\<^sup>\ \ d * (H * e * top \ top * e\<^sup>T * H) * d\<^sup>T" - using assms(1) big_forest_def conv_dist_comp mult_assoc by auto + using assms(1) forest_modulo_equivalence_def conv_dist_comp mult_assoc by auto also have "... = (H * d\<^sup>T)\<^sup>\ * H * a\<^sup>T * top * a * H * (d * H)\<^sup>\ \ d * H * e * top * e\<^sup>T * H * d\<^sup>T" by (metis comp_inf_covector inf_top.left_neutral mult_assoc) also have "... \ (H * d\<^sup>T)\<^sup>\ * (H * d)\<^sup>\ * H \ d * H * e * top * e\<^sup>T * H * d\<^sup>T" proof - have "(H * d\<^sup>T)\<^sup>\ * H * a\<^sup>T * top * a * H * (d * H)\<^sup>\ \ (H * d\<^sup>T)\<^sup>\ * H * 1 * H * (d * H)\<^sup>\" using 2 by (metis comp_associative comp_isotone mult_left_isotone mult_semi_associative star.circ_transitive_equal) also have "... = (H * d\<^sup>T)\<^sup>\ * H * (d * H)\<^sup>\" - using assms(1) big_forest_def mult.semigroup_axioms preorder_idempotent semigroup.assoc by fastforce + using assms(1) forest_modulo_equivalence_def mult.semigroup_axioms preorder_idempotent semigroup.assoc by fastforce also have "... = (H * d\<^sup>T)\<^sup>\ * (H * d)\<^sup>\ * H" by (metis star_slide mult_assoc) finally show ?thesis using inf.sup_left_isotone by auto qed also have "... \ (H * d\<^sup>T)\<^sup>\ * (H * d)\<^sup>\ * H \ d * H * d\<^sup>T" proof - have "d * H * e * top * e\<^sup>T * H * d\<^sup>T \ d * H * 1 * H * d\<^sup>T" using 3 by (metis comp_isotone idempotent_one_closed mult_left_isotone mult_sub_right_one mult_assoc) also have "... \ d * H * d\<^sup>T" - by (metis assms(1) big_forest_def mult_left_isotone mult_one_associative mult_semi_associative preorder_idempotent) + 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\<^sup>T * H)\<^sup>\ * (H * d)\<^sup>\ * H \ d * H * d\<^sup>T" - by (metis assms(1) big_forest_def comp_associative preorder_idempotent star_slide) + by (metis assms(1) forest_modulo_equivalence_def comp_associative preorder_idempotent star_slide) also have "... = H * ((d\<^sup>T * H)\<^sup>\ \ (H * d)\<^sup>\) * H \ d * H * d\<^sup>T" - by (simp add: assms(1) expand_big_forest mult.semigroup_axioms semigroup.assoc) + by (simp add: assms(1) expand_forest_modulo_equivalence mult.semigroup_axioms semigroup.assoc) also have "... = (H * (d\<^sup>T * H)\<^sup>\ * H \ H * (H * d)\<^sup>\ * H) \ d * H * d\<^sup>T" by (simp add: mult_left_dist_sup mult_right_dist_sup) also have "... = (H * d\<^sup>T)\<^sup>\ * H \ d * H * d\<^sup>T \ H * (d * H)\<^sup>\ \ d * H * d\<^sup>T" - by (smt assms(1) big_forest_def inf_sup_distrib2 mult.semigroup_axioms preorder_idempotent star_slide semigroup.assoc) + by (smt assms(1) forest_modulo_equivalence_def inf_sup_distrib2 mult.semigroup_axioms preorder_idempotent star_slide semigroup.assoc) also have "... \ (H * d\<^sup>T)\<^sup>\ * H \ d * H * d\<^sup>T \ 1" using 51 comp_inf.semiring.add_left_mono by blast finally have "?x * top * ?x\<^sup>T \ 1" - using 51 by (smt assms(1) big_forest_def conv_dist_comp conv_dist_inf conv_dist_sup conv_involutive conv_star_commute equivalence_one_closed mult.semigroup_axioms sup.absorb2 semigroup.assoc conv_isotone conv_order) + 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\<^sup>T * top * ?x \ 1" proof - have "?x\<^sup>T * top * ?x = (d\<^sup>T \ H\<^sup>T * e\<^sup>T\<^sup>T * top\<^sup>T \ top\<^sup>T * a\<^sup>T\<^sup>T * H\<^sup>T * (d\<^sup>T\<^sup>T * H\<^sup>T)\<^sup>\) * top * (d \ top * e\<^sup>T * H \ (H * d\<^sup>T)\<^sup>\ * H * a\<^sup>T * top)" by (simp add: conv_dist_comp conv_dist_inf conv_star_commute mult_assoc) also have "... = (d\<^sup>T \ H * e * top \ top * a * H * (d * H)\<^sup>\) * top * (d \ top * e\<^sup>T * H \ (H * d\<^sup>T)\<^sup>\ * H * a\<^sup>T * top)" - using assms(1) big_forest_def by auto + using assms(1) forest_modulo_equivalence_def by auto also have "... = H * e * top \ (d\<^sup>T \ top * a * H * (d * H)\<^sup>\) * top * (d \ top * e\<^sup>T * H \ (H * d\<^sup>T)\<^sup>\ * H * a\<^sup>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\<^sup>T * ((top * a * H * (d * H)\<^sup>\)\<^sup>T \ top) * (d \ top * e\<^sup>T * H \ (H * d\<^sup>T)\<^sup>\ * H * a\<^sup>T * top)" by (simp add: covector_comp_inf_1 covector_mult_closed) also have "... = H * e * top \ d\<^sup>T * (d * H)\<^sup>\\<^sup>T * H * a\<^sup>T * top * (d \ top * e\<^sup>T * H \ (H * d\<^sup>T)\<^sup>\ * H * a\<^sup>T * top)" - using assms(1) big_forest_def comp_associative conv_dist_comp by auto + using assms(1) forest_modulo_equivalence_def comp_associative conv_dist_comp by auto also have "... = H * e * top \ d\<^sup>T * (d * H)\<^sup>\\<^sup>T * H * a\<^sup>T * top * (d \ (H * d\<^sup>T)\<^sup>\ * H * a\<^sup>T * top) \ top * e\<^sup>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\<^sup>T * (d * H)\<^sup>\\<^sup>T * H * a\<^sup>T * (top \ ((H * d\<^sup>T)\<^sup>\ * H * a\<^sup>T * top)\<^sup>T) * d \ top * e\<^sup>T * H" by (metis comp_associative comp_inf_vector vector_conv_covector vector_top_closed) also have "... = H * e * top \ (H * e * top)\<^sup>T \ d\<^sup>T * (d * H)\<^sup>\\<^sup>T * H * a\<^sup>T * ((H * d\<^sup>T)\<^sup>\ * H * a\<^sup>T * top)\<^sup>T * d" - by (smt assms(1) big_forest_def conv_dist_comp inf.left_commute inf.sup_monoid.add_commute symmetric_top_closed mult_assoc inf_top.left_neutral) + 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)\<^sup>T \ d\<^sup>T * (d * H)\<^sup>\\<^sup>T * H * a\<^sup>T * ((H * d\<^sup>T)\<^sup>\ * H * a\<^sup>T * top)\<^sup>T * d" using vector_covector vector_mult_closed by auto also have "... = H * e * top * top\<^sup>T * e\<^sup>T * H\<^sup>T \ d\<^sup>T * (d * H)\<^sup>\\<^sup>T * H * a\<^sup>T * top\<^sup>T * a\<^sup>T\<^sup>T * H\<^sup>T * (H * d\<^sup>T)\<^sup>\\<^sup>T * d" by (smt conv_dist_comp mult.semigroup_axioms symmetric_top_closed semigroup.assoc) also have "... = H * e * top * top * e\<^sup>T * H \ d\<^sup>T * (H * d\<^sup>T)\<^sup>\ * H * a\<^sup>T * top * a * H * (d * H)\<^sup>\ * d" - using assms(1) big_forest_def conv_dist_comp conv_star_commute by auto + using assms(1) forest_modulo_equivalence_def conv_dist_comp conv_star_commute by auto also have "... = H * e * top * e\<^sup>T * H \ d\<^sup>T * (H * d\<^sup>T)\<^sup>\ * H * a\<^sup>T * top * a * H * (d * H)\<^sup>\ * d" using vector_top_closed mult_assoc by auto also have "... \ H \ d\<^sup>T * (H * d\<^sup>T)\<^sup>\ * H * (d * H)\<^sup>\ * d" proof - have "H * e * top * e\<^sup>T * H \ H * 1 * H" using 3 by (metis comp_associative mult_left_isotone mult_right_isotone) also have "... = H" - using assms(1) big_forest_def preorder_idempotent by auto + using assms(1) forest_modulo_equivalence_def preorder_idempotent by auto finally have 611: "H * e * top * e\<^sup>T * H \ H" by simp have "d\<^sup>T * (H * d\<^sup>T)\<^sup>\ * H * a\<^sup>T * top * a * H * (d * H)\<^sup>\ * d \ d\<^sup>T * (H * d\<^sup>T)\<^sup>\ * H * 1 * H * (d * H)\<^sup>\ * d" using 2 by (metis comp_associative mult_left_isotone mult_right_isotone) also have "... = d\<^sup>T * (H * d\<^sup>T)\<^sup>\ * H * (d * H)\<^sup>\ * d" - using assms(1) big_forest_def mult.semigroup_axioms preorder_idempotent semigroup.assoc by fastforce + using assms(1) forest_modulo_equivalence_def mult.semigroup_axioms preorder_idempotent semigroup.assoc by fastforce finally have "d\<^sup>T * (H * d\<^sup>T)\<^sup>\ * H * a\<^sup>T * top * a * H * (d * H)\<^sup>\ * d \ d\<^sup>T * (H * d\<^sup>T)\<^sup>\ * H * (d * H)\<^sup>\ * d" by simp thus ?thesis using 611 comp_inf.comp_isotone by blast qed also have "... = H \ (d\<^sup>T * H)\<^sup>\ * d\<^sup>T * H * d * (H * d)\<^sup>\" using star_slide mult_assoc by auto also have "... \ H \ (d\<^sup>T * H)\<^sup>\ * (H * d)\<^sup>\" proof - have "(d\<^sup>T * H)\<^sup>\ * d\<^sup>T * H * d * (H * d)\<^sup>\ \ (d\<^sup>T * H)\<^sup>\ * 1 * (H * d)\<^sup>\" - by (smt assms(1) big_forest_def conv_dist_comp mult_left_isotone mult_right_isotone preorder_idempotent mult_assoc) + by (smt assms(1) forest_modulo_equivalence_def conv_dist_comp mult_left_isotone mult_right_isotone preorder_idempotent mult_assoc) also have "... = (d\<^sup>T * H)\<^sup>\ * (H * d)\<^sup>\" by simp finally show ?thesis using inf.sup_right_isotone by blast qed also have "... = H \ ((d\<^sup>T * H)\<^sup>\ \ (H * d)\<^sup>\)" - by (simp add: assms(1) expand_big_forest) + by (simp add: assms(1) expand_forest_modulo_equivalence) also have "... = H \ (d\<^sup>T * H)\<^sup>\ \ H \ (H * d)\<^sup>\" by (simp add: comp_inf.semiring.distrib_left) also have "... = 1 \ H \ (d\<^sup>T * H)\<^sup>+ \ H \ (H * d)\<^sup>+" proof - have 612: "H \ (H * d)\<^sup>\ = 1 \ H \ (H * d)\<^sup>+" - using assms(1) big_forest_def reflexive_inf_star by blast + using assms(1) forest_modulo_equivalence_def reflexive_inf_star by blast have "H \ (d\<^sup>T * H)\<^sup>\ = 1 \ H \ (d\<^sup>T * H)\<^sup>+" - using assms(1) big_forest_def reflexive_inf_star by auto + 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)\<^sup>+ \ 1" by (metis assms(3) inf.coboundedI1 p_antitone_iff p_shunting_swap regular_one_closed) hence "H \ (d\<^sup>T * H)\<^sup>+ \ 1" - by (metis assms(1) big_forest_def conv_dist_comp conv_dist_inf conv_plus_commute coreflexive_symmetric) + 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\<^sup>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\<^sup>T = bot" and "e * F * e = bot" and "e\<^sup>T \ v\<^sup>\" and "e \ bot" shows "arc (v \ -F * e * top \ top * e\<^sup>T * F)" proof - let ?i = "v \ -F * e * top \ top * e\<^sup>T * F" have 1: "?i\<^sup>T * top * ?i \ 1" proof - have "?i\<^sup>T * top * ?i = (v\<^sup>T \ top * e\<^sup>T * -F \ F * e * top) * top * (v \ -F * e * top \ top * e\<^sup>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\<^sup>T \ top * e\<^sup>T * -F) * top * (v \ -F * e * top) \ top * e\<^sup>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\<^sup>T \ top * e\<^sup>T * -F) * top * top * (v \ -F * e * top) \ top * e\<^sup>T * F" by (simp add: comp_associative) also have "... = F * e * top \ v\<^sup>T * (top \ (top * e\<^sup>T * -F)\<^sup>T) * top * (v \ -F * e * top) \ top * e\<^sup>T * F" using comp_associative comp_inf_vector_1 by auto also have "... = F * e * top \ v\<^sup>T * (top \ (top * e\<^sup>T * -F)\<^sup>T) * (top \ (-F * e * top)\<^sup>T) * v \ top * e\<^sup>T * F" by (smt comp_inf_vector conv_dist_comp mult.semigroup_axioms symmetric_top_closed semigroup.assoc) also have "... = F * e * top \ v\<^sup>T * (top * e\<^sup>T * -F)\<^sup>T * (-F * e * top)\<^sup>T * v \ top * e\<^sup>T * F" by simp also have "... = F * e * top \ v\<^sup>T * -F\<^sup>T * e\<^sup>T\<^sup>T * top\<^sup>T * top\<^sup>T * e\<^sup>T * -F\<^sup>T * v \ top * e\<^sup>T * F" by (metis comp_associative conv_complement conv_dist_comp) also have "... = F * e * top \ v\<^sup>T * -F * e * top * top * e\<^sup>T * -F * v \ top * e\<^sup>T * F" by (simp add: assms(1)) also have "... = F * e * top \ v\<^sup>T * -F * e * top \ top * e\<^sup>T * -F * v \ top * e\<^sup>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\<^sup>T * -F) * e * top \ top * e\<^sup>T * -F * v \ top * e\<^sup>T * F" using assms(3) injective_comp_right_dist_inf mult_assoc by auto also have "... = (F \ v\<^sup>T * -F) * e * top \ top * e\<^sup>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\<^sup>T * -F) * e * top * top * e\<^sup>T * (F \ -F * v)" by (metis comp_associative comp_inf_covector inf_top.left_neutral vector_top_closed) also have "... = (F \ v\<^sup>T * -F) * e * top * e\<^sup>T * (F \ -F * v)" by (simp add: comp_associative) also have "... \ (F \ v\<^sup>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\<^sup>T * -F) * (F \ -F * v) \ F" by (metis assms(1) inf.absorb1 inf.cobounded1 mult_isotone preorder_idempotent) also have "... \ (F \ v\<^sup>T * -F) * (F \ -F * v) \ (F \ v)\<^sup>T\<^sup>\ * (F \ v)\<^sup>\" using assms(5) comp_inf.mult_right_isotone by auto also have "... \ (-F \ v\<^sup>T) * -F * -F * (-F \ v) \ (F \ v)\<^sup>T\<^sup>\ * (F \ v)\<^sup>\" proof - have "F \ v\<^sup>T * -F \ (v\<^sup>T \ F * -F\<^sup>T) * -F" by (metis conv_complement dedekind_2 inf_commute) also have "... = (v\<^sup>T \ -F\<^sup>T) * -F" using assms(1) equivalence_comp_left_complement by simp finally have "F \ v\<^sup>T * -F \ F \ (v\<^sup>T \ -F) * -F" using assms(1) by auto hence 11: "F \ v\<^sup>T * -F = F \ (-F \ v\<^sup>T) * -F" by (metis inf.antisym_conv inf.sup_monoid.add_commute comp_left_subdist_inf inf.boundedE inf.sup_right_isotone) hence "F\<^sup>T \ -F\<^sup>T * v\<^sup>T\<^sup>T = F\<^sup>T \ -F\<^sup>T * (-F\<^sup>T \ v\<^sup>T\<^sup>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\<^sup>T * -F) * (F \ -F * v) = (F \ (-F \ v\<^sup>T) * -F) * (F \ -F * (-F \ v))" using 11 12 by auto also have "... \ (-F \ v\<^sup>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\<^sup>T) * -F * -F * (-F \ v) \ (F \ v)\<^sup>T * (F \ v)\<^sup>T\<^sup>\ * (F \ v)\<^sup>\) \ ((-F \ v\<^sup>T) * -F * -F * (-F \ v) \ (F \ v)\<^sup>\)" by (metis comp_associative inf_sup_distrib1 star.circ_loop_fixpoint) also have "... = ((-F \ v\<^sup>T) * -F * -F * (-F \ v) \ (F \ v\<^sup>T) * (F \ v)\<^sup>T\<^sup>\ * (F \ v)\<^sup>\) \ ((-F \ v\<^sup>T) * -F * -F * (-F \ v) \ (F \ v)\<^sup>\)" using assms(1) conv_dist_inf by auto also have "... = bot \ ((-F \ v\<^sup>T) * -F * -F * (-F \ v) \ (F \ v)\<^sup>\)" proof - have "(-F \ v\<^sup>T) * -F * -F * (-F \ v) \ (F \ v\<^sup>T) * (F \ v)\<^sup>T\<^sup>\ * (F \ v)\<^sup>\ \ 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\<^sup>T) * -F * -F * (-F \ v) \ (1 \ (F \ v)\<^sup>\ * (F \ v))" by (simp add: star.circ_plus_same star_left_unfold_equal) also have "... = ((-F \ v\<^sup>T) * -F * -F * (-F \ v) \ 1) \ ((-F \ v\<^sup>T) * -F * -F * (-F \ v) \ (F \ v)\<^sup>\ * (F \ v))" by (simp add: comp_inf.semiring.distrib_left) also have "... \ 1 \ ((-F \ v\<^sup>T) * -F * -F * (-F \ v) \ (F \ v)\<^sup>\ * (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\<^sup>T \ 1" proof - have "?i * top * ?i\<^sup>T = (v \ -F * e * top \ top * e\<^sup>T * F) * top * (v\<^sup>T \ (-F * e * top)\<^sup>T \ (top * e\<^sup>T * F)\<^sup>T)" by (simp add: conv_dist_inf) also have "... = (v \ -F * e * top \ top * e\<^sup>T * F) * top * (v\<^sup>T \ top\<^sup>T * e\<^sup>T * -F\<^sup>T \ F\<^sup>T * e\<^sup>T\<^sup>T * top\<^sup>T)" by (simp add: conv_complement conv_dist_comp mult_assoc) also have "... = (v \ -F * e * top \ top * e\<^sup>T * F) * top * (v\<^sup>T \ top * e\<^sup>T * -F \ F * e * top)" by (simp add: assms(1)) also have "... = -F * e * top \ (v \ top * e\<^sup>T * F) * top * (v\<^sup>T \ top * e\<^sup>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\<^sup>T * F) * top * (v\<^sup>T \ F * e * top) \ top * e\<^sup>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\<^sup>T * F) * top * top * (v\<^sup>T \ F * e * top) \ top * e\<^sup>T * -F" by (simp add: mult_assoc) also have "... = -F * e * top \ v * ((top * e\<^sup>T * F)\<^sup>T \ top) * top * (v\<^sup>T \ F * e * top) \ top * e\<^sup>T * -F" by (simp add: comp_inf_vector_1 mult.semigroup_axioms semigroup.assoc) also have "... = -F * e * top \ v * ((top * e\<^sup>T * F)\<^sup>T \ top) * (top \ (F * e * top)\<^sup>T) * v\<^sup>T \ top * e\<^sup>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\<^sup>T * F)\<^sup>T * (F * e * top)\<^sup>T * v\<^sup>T \ top * e\<^sup>T * -F" by simp also have "... = -F * e * top \ v * F\<^sup>T * e\<^sup>T\<^sup>T * top\<^sup>T * top\<^sup>T * e\<^sup>T * F\<^sup>T * v\<^sup>T \ top * e\<^sup>T * -F" by (metis comp_associative conv_dist_comp) also have "... = -F * e * top \ v * F * e * top * top * e\<^sup>T * F * v\<^sup>T \ top * e\<^sup>T * -F" using assms(1) by auto also have "... = -F * e * top \ v * F * e * top \ top * e\<^sup>T * F * v\<^sup>T \ top * e\<^sup>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\<^sup>T * F * v\<^sup>T \ top * e\<^sup>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\<^sup>T * (F * v\<^sup>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\<^sup>T * (F * v\<^sup>T \ -F)" by (metis inf_top_right vector_export_comp vector_top_closed) also have "... = (-F \ v * F) * e * top * e\<^sup>T * (F * v\<^sup>T \ -F)" by (simp add: comp_associative) also have "... \ (-F \ v * F) * (F * v\<^sup>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)\<^sup>T \ -F)" by (simp add: assms(1) conv_dist_comp) also have "... = (-F \ v * F) * (-F \ v * F)\<^sup>T" using assms(1) conv_complement conv_dist_inf by (simp add: inf.sup_monoid.add_commute) also have "... \ (-F \ v) * (F \ v)\<^sup>\ * (F \ v)\<^sup>T\<^sup>\ * (-F \ v)\<^sup>T" proof - let ?Fv = "F \ v" have "-F \ v * F \ -F \ v * (F \ v)\<^sup>T\<^sup>\ * (F \ v)\<^sup>\" using assms(5) inf.sup_right_isotone mult_right_isotone comp_associative by auto also have "... \ -F \ v * (F \ v)\<^sup>\" proof - have "v * v\<^sup>T \ 1" by (simp add: assms(2)) hence "v * v\<^sup>T * F \ F" using assms(1) dual_order.trans mult_left_isotone by blast hence "v * v\<^sup>T * F\<^sup>T\<^sup>\ * F\<^sup>\ \ 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)\<^sup>T * F\<^sup>T\<^sup>\ * F\<^sup>\ \ 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)\<^sup>T * (F \ v)\<^sup>T\<^sup>\ * (F \ v)\<^sup>\ \ 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)\<^sup>T * (F \ v)\<^sup>T\<^sup>\ * (F \ v)\<^sup>\ \ bot" using order.eq_iff p_antitone pseudo_complement by auto hence "(-F \ v * (F \ v)\<^sup>T * (F \ v)\<^sup>T\<^sup>\ * (F \ v)\<^sup>\) \ v * (v \ F)\<^sup>\ \ v * (v \ F)\<^sup>\" using bot_least le_bot by fastforce hence "(-F \ v * (v \ F)\<^sup>\) \ (v * (F \ v)\<^sup>T * (F \ v)\<^sup>T\<^sup>\ * (F \ v)\<^sup>\ \ v * (v \ F)\<^sup>\) \ v * (v \ F)\<^sup>\" by (simp add: sup_inf_distrib2) hence "(-F \ v * (v \ F)\<^sup>\) \ v * ((F \ v)\<^sup>T * (F \ v)\<^sup>T\<^sup>\ \ 1) * (v \ F)\<^sup>\ \ v * (v \ F)\<^sup>\" 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)\<^sup>\) \ v * (F \ v)\<^sup>T\<^sup>\ * (v \ F)\<^sup>\ \ v * (v \ F)\<^sup>\" by (simp add: star_left_unfold_equal sup_commute) hence "-F \ v * (F \ v)\<^sup>T\<^sup>\ * (v \ F)\<^sup>\ \ v * (v \ F)\<^sup>\" 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)\<^sup>T\<^sup>\) * (F \ v)\<^sup>\" by (metis dedekind_2 conv_star_commute inf.sup_monoid.add_commute) also have "... \ (v \ -F * F\<^sup>T\<^sup>\) * (F \ v)\<^sup>\" using conv_isotone inf.sup_right_isotone mult_left_isotone mult_right_isotone star_isotone by auto also have "... = (v \ -F * F) * (F \ v)\<^sup>\" by (metis assms(1) equivalence_comp_right_complement mult_left_one star_one star_simulation_right_equal) also have "... = (-F \ v) * (F \ v)\<^sup>\" using assms(1) equivalence_comp_right_complement inf.sup_monoid.add_commute by auto finally have "-F \ v * F \ (-F \ v) * (F \ v)\<^sup>\" by simp hence "(-F \ v * F) * (-F \ v * F)\<^sup>T \ (-F \ v) * (F \ v)\<^sup>\ * ((-F \ v) * (F \ v)\<^sup>\)\<^sup>T" by (simp add: comp_isotone conv_isotone) also have "... = (-F \ v) * (F \ v)\<^sup>\ * (F \ v)\<^sup>T\<^sup>\ * (-F \ v)\<^sup>T" by (simp add: comp_associative conv_dist_comp conv_star_commute) finally show ?thesis by simp qed also have "... \ (-F \ v) * ((F \ v\<^sup>\) \ (F \ v\<^sup>T\<^sup>\)) * (-F \ v)\<^sup>T" proof - have "(F \ v)\<^sup>\ * (F \ v)\<^sup>T\<^sup>\ \ F\<^sup>\ * F\<^sup>T\<^sup>\" 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)\<^sup>\ * (F \ v)\<^sup>T\<^sup>\ \ F" using assms(1) dual_order.trans by blast have "(F \ v)\<^sup>\ * (F \ v)\<^sup>T\<^sup>\ \ v\<^sup>\ * v\<^sup>T\<^sup>\" by (simp add: fc_isotone) hence "(F \ v)\<^sup>\ * (F \ v)\<^sup>T\<^sup>\ \ F \ v\<^sup>\ * v\<^sup>T\<^sup>\" using 21 by simp also have "... = F \ (v\<^sup>\ \ v\<^sup>T\<^sup>\)" 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\<^sup>T\<^sup>\) * (-F \ v)\<^sup>T \ (-F \ v) * (F \ v\<^sup>\) * (-F \ v)\<^sup>T" by (simp add: mult_left_dist_sup mult_right_dist_sup) also have "... \ (-F \ v) * (-F \ v)\<^sup>T \ (-F \ v) * (-F \ v)\<^sup>T" proof - have "(-F \ v) * (F \ v\<^sup>T\<^sup>\) \ (-F \ v) * ((F \ v)\<^sup>T\<^sup>\ * (F \ v)\<^sup>\ \ v\<^sup>T\<^sup>\)" by (simp add: assms(5) inf.coboundedI1 mult_right_isotone) also have "... = (-F \ v) * ((F \ v)\<^sup>T * (F \ v)\<^sup>T\<^sup>\ * (F \ v)\<^sup>\ \ v\<^sup>T\<^sup>\) \ (-F \ v) * ((F \ v)\<^sup>\ \ v\<^sup>T\<^sup>\)" by (metis comp_associative comp_inf.mult_right_dist_sup mult_left_dist_sup star.circ_loop_fixpoint) also have "... \ (-F \ v) * (F \ v)\<^sup>T * top \ (-F \ v) * ((F \ v)\<^sup>\ \ v\<^sup>T\<^sup>\)" by (simp add: comp_associative comp_isotone inf.coboundedI2 inf.sup_monoid.add_commute le_supI1) also have "... \ (-F \ v) * (F \ v)\<^sup>T * top \ (-F \ v) * (v\<^sup>\ \ v\<^sup>T\<^sup>\)" 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\<^sup>\ \ v\<^sup>T\<^sup>\)" 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\<^sup>T\<^sup>\) \ -F \ v" by simp have "((-F \ v) * (F \ v\<^sup>T\<^sup>\))\<^sup>T = (F \ v\<^sup>\) * (-F \ v)\<^sup>T" by (simp add: assms(1) conv_dist_inf conv_star_commute conv_dist_comp) hence "(F \ v\<^sup>\) * (-F \ v)\<^sup>T \ (-F \ v)\<^sup>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)\<^sup>T" by simp also have "... \ v * v\<^sup>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\<^sup>T * -F * v * F * e)" using assms(3, 4, 6) arc_regular regular_mult_closed by auto have 32: "bijective ((top * e\<^sup>T)\<^sup>T)" using assms(3) by (simp add: conv_dist_comp) have "top * ?i * top = top * (v \ -F * e * top) * ((top * e\<^sup>T * F)\<^sup>T \ top)" by (simp add: comp_associative comp_inf_vector_1) also have "... = (top \ (-F * e * top)\<^sup>T) * v * ((top * e\<^sup>T * F)\<^sup>T \ top)" using comp_inf_vector conv_dist_comp by auto also have "... = (-F * e * top)\<^sup>T * v * (top * e\<^sup>T * F)\<^sup>T" by simp also have "... = top\<^sup>T * e\<^sup>T * -F\<^sup>T * v * F\<^sup>T * e\<^sup>T\<^sup>T * top\<^sup>T" by (simp add: comp_associative conv_complement conv_dist_comp) finally have 33: "top * ?i * top = top * e\<^sup>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\<^sup>T * F) * top \ bot" hence "top * e\<^sup>T * -F * v * F * e * top = bot" using 33 by auto hence "e\<^sup>T * -F * v * F * e = bot" using 31 tarski comp_associative le_bot by fastforce hence "top * (-F * v * F * e)\<^sup>T \ -(e\<^sup>T)" by (metis comp_associative conv_complement_sub_leq conv_involutive p_bot schroeder_5_p) hence "top * e\<^sup>T * F\<^sup>T * v\<^sup>T * -F\<^sup>T \ -(e\<^sup>T)" by (simp add: comp_associative conv_complement conv_dist_comp) hence "v * F * e * top * e\<^sup>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\<^sup>T \ F" by (simp add: comp_associative) hence "v * F * e * top \ F * (top * e\<^sup>T)\<^sup>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\<^sup>\ * F * e * top \ F * e * top" using comp_associative star_left_induct_mult_iff by auto hence "e\<^sup>T * F * e * top \ F * e * top" by (meson assms(9) mult_left_isotone order_trans) hence "e\<^sup>T * F * e * top * (e * top)\<^sup>T \ F" using 32 shunt_bijective assms(3) mult_assoc by auto hence 34: "e\<^sup>T * F * e * top * top * e\<^sup>T \ F" by (metis conv_dist_comp mult.semigroup_axioms symmetric_top_closed semigroup.assoc) hence "e\<^sup>T \ F" proof - have "e\<^sup>T \ e\<^sup>T * e * e\<^sup>T" by (metis conv_involutive ex231c) also have "... \ e\<^sup>T * F * e * e\<^sup>T" using assms(1) comp_associative mult_left_isotone mult_right_isotone by fastforce also have "... \ e\<^sup>T * F * e * top * top * e\<^sup>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)\<^sup>T \ - e" using assms(8) comp_associative schroeder_4_p by auto hence "top * e\<^sup>T * F \ - e" by (simp add: assms(1) comp_associative conv_dist_comp) hence "(top * e\<^sup>T)\<^sup>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\<^sup>T * top)" using 1 2 3 arc_expanded by blast thus ?thesis by blast qed subsubsection \Comparison of edge weights\ text \ In this section we compare the weight of the \selected_edge\ with other edges of interest. -Theorems 8, 9, 10 and 11 are supporting lemmas. -For example, Theorem 8 is used to show that the \selected_edge\ has its source inside and its target outside the component it is chosen for. +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. \ -text \Theorem 8\ - lemma e_leq_c_c_complement_transpose_general: - assumes "e = minarc (c * -(c)\<^sup>T \ g)" - and "regular c" - shows "e \ c * -(c)\<^sup>T" + assumes "e = minarc (v * -(v)\<^sup>T \ g)" + and "regular v" + shows "e \ v * -(v)\<^sup>T" proof - - have "e \ -- (c * - c\<^sup>T \ g)" + have "e \ -- (v * - v\<^sup>T \ g)" using assms(1) minarc_below order_trans by blast - also have "... \ -- (c * - c\<^sup>T)" + also have "... \ -- (v * - v\<^sup>T)" using order_lesseq_imp pp_isotone_inf by blast - also have "... = c * - c\<^sup>T" + also have "... = v * - v\<^sup>T" using assms(2) regular_mult_closed by auto finally show ?thesis by simp qed -text \Theorem 9\ - lemma x_leq_c_transpose_general: - assumes "forest h" - and "vector c" - and "x\<^sup>T * top \ forest_components(h) * e * top" - and "e \ c * -c\<^sup>T" - and "c = forest_components(h) * c" - shows "x \ c\<^sup>T" + assumes "vector_classes x v" + and "a\<^sup>T * top \ x * e * top" + and "e \ v * -v\<^sup>T" + shows "a \ v\<^sup>T" proof - - let ?H = "forest_components h" - have "x \ top * x" + 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 "... \ (?H * e * top)\<^sup>T" - using assms(3) conv_dist_comp conv_order by force - also have "... = top * e\<^sup>T * ?H" - using assms(1) comp_associative conv_dist_comp forest_components_equivalence by auto - also have "... \ top * (c * - c\<^sup>T)\<^sup>T * ?H" - by (simp add: assms(4) conv_isotone mult_left_isotone mult_right_isotone) - also have "... = top * (- c * c\<^sup>T) * ?H" + also have "... \ (x * e * top)\<^sup>T" + using assms(2) conv_dist_comp conv_isotone by fastforce + also have "... = top * e\<^sup>T * x" + using 1 by (simp add: conv_dist_comp mult_assoc) + also have "... \ top * (v * - v\<^sup>T)\<^sup>T * x" + by (metis assms(3) conv_dist_comp conv_isotone mult_left_isotone symmetric_top_closed) + also have "... = top * (- v * v\<^sup>T) * x" by (simp add: conv_complement conv_dist_comp) - also have "... \ top * c\<^sup>T * ?H" + also have "... \ top * v\<^sup>T * x" by (metis mult_left_isotone top.extremum mult_assoc) - also have "... = c\<^sup>T * ?H" - using assms(1, 2) component_is_vector vector_conv_covector by auto - also have "... = c\<^sup>T" - by (metis assms(1, 5) fch_equivalence conv_dist_comp) + also have "... = v\<^sup>T * x" + using assms(1) vector_classes_def vector_conv_covector by auto + also have "... = v\<^sup>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 -text \Theorem 10\ - lemma x_leq_c_complement_general: - assumes "vector c" - and "c * c\<^sup>T \ forest_components h" - and "x \ c\<^sup>T" - and "x \ -forest_components h" - shows "x \ -c" + assumes "vector v" + and "v * v\<^sup>T \ x" + and "a \ v\<^sup>T" + and "a \ -x" + shows "a \ -v" proof - - let ?H = "forest_components h" - have "x \ - ?H \ c\<^sup>T" + have "a \ -x \ v\<^sup>T" using assms(3, 4) by auto - also have "... \ - c" + also have "... \ - v" proof - - have "c \ c\<^sup>T \ ?H" + have "v \ v\<^sup>T \ x" using assms(1, 2) vector_covector by auto - hence "-?H \ c \ c\<^sup>T \ bot" + hence "-x \ v \ v\<^sup>T \ bot" using inf.sup_monoid.add_assoc p_antitone pseudo_complement by fastforce thus ?thesis using le_bot p_shunting_swap pseudo_complement by blast qed finally show ?thesis by simp qed -text \Theorem 11\ - -lemma sum_e_below_sum_x_when_outgoing_same_component_general: - assumes "e = minarc (c * -(c)\<^sup>T \ g)" - and "regular c" - and "forest h" - and "vector c" - and "x\<^sup>T * top \ (forest_components h) * e * top" - and "c = (forest_components h) * c" - and "c * c\<^sup>T \ forest_components h" - and "x \ - forest_components h \ -- g" +lemma sum_e_below_sum_a_when_outgoing_same_component_general: + assumes "e = minarc (v * -(v)\<^sup>T \ g)" and "symmetric g" - and "arc x" - and "c \ bot" - shows "sum (e \ g) \ sum (x \ g)" + and "arc a" + and "a \ -x \ -- g" + and "a\<^sup>T * top \ x * e * top" + and "unique_vector_class x v" + shows "sum (e \ g) \ sum (a \ g)" proof - - let ?H = "forest_components h" - have 1:"e \ c * - c\<^sup>T" - using assms(1, 2) e_leq_c_c_complement_transpose_general by auto - have 2: "x \ c\<^sup>T" - using 1 assms(3, 4, 5, 6) x_leq_c_transpose_general by auto - hence "x \ -c" - using assms(4, 7, 8) x_leq_c_complement_general inf.boundedE by blast - hence "x \ - c \ c\<^sup>T" + have 1:"e \ v * - v\<^sup>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\<^sup>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\<^sup>T" using 2 by simp - hence "x \ - c * c\<^sup>T" - using assms(4) by (simp add: vector_complement_closed vector_covector) - hence "x\<^sup>T \ c\<^sup>T\<^sup>T * - c\<^sup>T" - by (metis conv_complement conv_dist_comp conv_isotone) - hence 3: "x\<^sup>T \ c * - c\<^sup>T" + hence "a \ - v * v\<^sup>T" + using assms(6) vector_complement_closed vector_covector unique_vector_class_def vector_classes_def by metis + hence "a\<^sup>T \ v\<^sup>T\<^sup>T * - v\<^sup>T" + using conv_complement conv_dist_comp conv_isotone by metis + hence 3: "a\<^sup>T \ v * - v\<^sup>T" by simp - hence "x \ -- g" - using assms(8) by auto - hence "x\<^sup>T \ -- g" - using assms(9) conv_complement conv_isotone by fastforce - hence "x\<^sup>T \ c * - c\<^sup>T \ -- g \ bot" - using 3 by (metis assms(10, 11) comp_inf.semiring.mult_not_zero conv_dist_comp - conv_involutive inf.orderE mult_right_zero top.extremum) - hence "x\<^sup>T \ c * - c\<^sup>T \ g \ bot" + hence "a \ -- g" + using assms(4) by auto + hence "a\<^sup>T \ -- g" + using assms(2) conv_complement conv_isotone by fastforce + hence "a\<^sup>T \ v * - v\<^sup>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\<^sup>T \ v * - v\<^sup>T \ g \ bot" using inf.sup_monoid.add_commute pp_inf_bot_iff by auto - hence "sum (minarc (c * - c\<^sup>T \ g) \ (c * - c\<^sup>T \ g)) \ sum (x\<^sup>T \ c * - c\<^sup>T \ g)" - using assms(10) minarc_min inf.sup_monoid.add_assoc by auto - hence "sum (e \ c * - c\<^sup>T \ g) \ sum (x\<^sup>T \ c * - c\<^sup>T \ g)" - using assms(1) inf.sup_monoid.add_assoc by auto - hence "sum (e \ g) \ sum (x\<^sup>T \ g)" + hence "sum (minarc (v * - v\<^sup>T \ g) \ (v * - v\<^sup>T \ g)) \ sum (a\<^sup>T \ v * - v\<^sup>T \ g)" + using assms(3) minarc_min inf.sup_monoid.add_assoc by simp + hence "sum (e \ v * - v\<^sup>T \ g) \ sum (a\<^sup>T \ v * - v\<^sup>T \ g)" + using assms(1, 6) inf.sup_monoid.add_assoc by simp + hence "sum (e \ g) \ sum (a\<^sup>T \ g)" using 1 3 by (metis inf.orderE) - hence "sum (e \ g) \ sum (x \ g)" - using assms(9) sum_symmetric by auto + 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\<^sup>T * top \ forest_components h * selected_edge h j g * top" and "j \ bot" and "arc x" shows "sum (selected_edge h j g \ g) \ sum (x \ g)" proof - let ?e = "selected_edge h j g" let ?c = "choose_component (forest_components h) j" let ?H = "forest_components h" show ?thesis - proof (rule sum_e_below_sum_x_when_outgoing_same_component_general) + proof (rule sum_e_below_sum_a_when_outgoing_same_component_general) next show "?e = minarc (?c * - ?c\<^sup>T \ g)" by simp next - show "regular ?c" - using component_is_regular by auto - next - show "forest h" - by (simp add: assms(3)) - next - show "vector ?c" - by (simp add: assms(2, 6) component_is_vector) - next - show "x\<^sup>T * top \ ?H * ?e * top" - by (simp add: assms(5)) - next - show "?c = ?H * ?c" - using component_single by auto - next - show "?c * ?c\<^sup>T \ ?H" - by (simp add: component_is_connected) - next - show "x \ -?H \ -- g" - using assms(4) by auto - next show "symmetric g" by (simp add: assms(1)) next show "arc x" - by (simp add: assms(7)) + by (simp add: assms(8)) next - show "?c \ bot" - using assms(2, 5 , 6, 7) inf_bot_left le_bot minarc_bot mult_left_zero mult_right_zero by fastforce + show "x \ -?H \ -- g" + using assms(5) by auto + next + show "x\<^sup>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\<^sup>T \ ?H" + by (simp add: component_is_connected) + qed qed qed text \ -If there is a path in the \big_forest\ from an edge between components, $a$, to the \selected_edge\, $e$, then the weight of $e$ is no greater than the weight of $a$. +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 \big_forest_path_split_disj\. + 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_bigforest: +lemma a_to_e_in_forest_modulo_equivalence: assumes "symmetric g" and "f \ --g" and "vector j" and "forest h" - and "big_forest (forest_components h) d" + and "forest_modulo_equivalence (forest_components h) d" and "f \ f\<^sup>T = h \ h\<^sup>T \ d \ d\<^sup>T" - and "(\ a b . bf_between_arcs a b (forest_components h) d \ a \ -(forest_components h) \ -- g \ b \ d \ sum(b \ g) \ sum(a \ g))" + and "(\ 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 "bf_between_arcs a b (forest_components h) (d \ selected_edge h j g)" + 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\<^sup>T * top \ ?H * ?e * top") case True show "a\<^sup>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\<^sup>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\<^sup>T * top \ ?H * ?e * top \ sum (b \ g) \ sum (a \ g)" proof - let ?d' = "d \ ?e" let ?x = "d \ top * ?e\<^sup>T * ?H \ (?H * d\<^sup>T)\<^sup>\ * ?H * a\<^sup>T * top" have 61: "arc (?x)" proof (rule shows_arc_x) - show "big_forest ?H d" + show "forest_modulo_equivalence ?H d" by (simp add: assms(5)) next - show "bf_between_arcs a ?e ?H d" + show "forest_modulo_equivalence_path a ?e ?H d" proof - - have 611: "bf_between_arcs a b ?H (d \ b)" + 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 bf_between_arcs_def arc_regular by fastforce + using 611 forest_modulo_equivalence_path_def arc_regular by fastforce thus ?thesis - using 616 by (smt big_forest_path_split_disj assms(4, 8, 10, 12) bf_between_arcs_def fch_equivalence minarc_regular regular_closed_star regular_conv_closed regular_mult_closed) + 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)\<^sup>+ \ - ?H" - using assms(5) big_forest_def by blast + using assms(5) forest_modulo_equivalence_def le_bot pseudo_complement by blast next show "\ a\<^sup>T * top \ ?H * ?e * top" by (simp add: False) next show "regular a" - using assms(12) bf_between_arcs_def arc_regular by auto + 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\<^sup>T * top)" by (simp add: assms(11)) have 63: "bijective (?x * top)" using 61 by simp have 64: "?x \ (?H * d\<^sup>T)\<^sup>\ * ?H * a\<^sup>T * top" by simp hence "?x * top \ (?H * d\<^sup>T)\<^sup>\ * ?H * a\<^sup>T * top" using mult_left_isotone inf_vector_comp by auto hence "a\<^sup>T * top \ ((?H * d\<^sup>T)\<^sup>\ * ?H)\<^sup>T * ?x * top" using 62 63 64 by (smt bijective_reverse mult_assoc) also have "... = ?H * (d * ?H)\<^sup>\ * ?x * top" using conv_dist_comp conv_star_commute by auto also have "... = (?H * d)\<^sup>\ * ?H * ?x * top" by (simp add: star_slide) finally have "a\<^sup>T * top \ (?H * d)\<^sup>\ * ?H * ?x * top" by simp - hence 65: "bf_between_arcs a ?x ?H d" - using 61 assms(12) bf_between_arcs_def by blast + 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 bf_between_arcs_def assms(7, 13) by blast + 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" - using 66 assms(5) big_forest_def order_lesseq_imp by blast + 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)\<^sup>+" + 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\<^sup>T" proof - have "h \ h\<^sup>T \ d \ d\<^sup>T = f \ f\<^sup>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\<^sup>T * top \ ?H * ?e * top" proof - have "?x \ top * ?e\<^sup>T * ?H" using inf.coboundedI1 by auto hence "?x\<^sup>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\<^sup>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\<^sup>\ * e\<^sup>T = e\<^sup>T" and "i \ v \ top * e\<^sup>T * w\<^sup>T\<^sup>\" 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)\<^sup>T\<^sup>\ * e\<^sup>T * top" proof - have 1: "(v \ -i \ -i\<^sup>T) * (v\<^sup>T \ -i \ -i\<^sup>T) \ 1" using assms(1) comp_isotone order.trans inf.cobounded1 by blast have 2: "bijective (i * top) \ bijective (e\<^sup>T * top)" using assms(4, 5) mult_assoc by auto have "i \ v * (top * e\<^sup>T * w\<^sup>T\<^sup>\)\<^sup>T" using assms(3) covector_mult_closed covector_restrict_comp_conv order_lesseq_imp vector_top_closed by blast also have "... \ v * w\<^sup>T\<^sup>\\<^sup>T * e\<^sup>T\<^sup>T * top\<^sup>T" by (simp add: comp_associative conv_dist_comp) also have "... \ v * w\<^sup>\ * e * top" by (simp add: conv_star_commute) also have "... = v * w\<^sup>\ * e * e\<^sup>T * e * top" using assms(5) arc_eq_1 by (simp add: comp_associative) also have "... \ v * w\<^sup>\ * e * e\<^sup>T * top" by (simp add: comp_associative mult_right_isotone) also have "... \ (--g) * (--g)\<^sup>\ * (--g) * e\<^sup>T * top" using assms(6, 7, 8) by (simp add: comp_isotone star_isotone) also have "... \ (--g)\<^sup>\ * e\<^sup>T * top" by (metis comp_isotone mult_left_isotone star.circ_increasing star.circ_transitive_equal) also have "... \ v\<^sup>T\<^sup>\ * v\<^sup>\ * e\<^sup>T * top" by (simp add: assms(9) mult_left_isotone) also have "... \ v\<^sup>T\<^sup>\ * e\<^sup>T * top" by (simp add: assms(2) comp_associative) finally have "i \ v\<^sup>T\<^sup>\ * e\<^sup>T * top" by simp hence "i * top \ v\<^sup>T\<^sup>\ * e\<^sup>T * top" by (metis comp_associative mult_left_isotone vector_top_closed) hence "e\<^sup>T * top \ v\<^sup>T\<^sup>\\<^sup>T * i * top" using 2 by (metis bijective_reverse mult_assoc) also have "... = v\<^sup>\ * i * top" by (simp add: conv_star_commute) also have "... \ (v \ -i \ -i\<^sup>T)\<^sup>\ * i * top" proof - have 3: "i * top \ (v \ -i \ -i\<^sup>T)\<^sup>\ * i * top" using star.circ_loop_fixpoint sup_right_divisibility mult_assoc by auto have "(v \ i) * (v \ -i \ -i\<^sup>T)\<^sup>\ * 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\<^sup>T)\<^sup>\ * i * top \ (v \ -i \ -i\<^sup>T)\<^sup>\ * i * top" using 3 dual_order.trans by blast have 5: "(v \ -i \ -i\<^sup>T) * (v \ -i \ -i\<^sup>T)\<^sup>\ * i * top \ (v \ -i \ -i\<^sup>T)\<^sup>\ * i * top" by (metis mult_left_isotone star.circ_increasing star.left_plus_circ) have "v\<^sup>+ \ -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\<^sup>T" by (simp add: schroeder_5_p) hence "v \ -v\<^sup>T" by simp hence "v \ v\<^sup>T \ bot" by (simp add: bot_unique pseudo_complement) hence 7: "v \ i\<^sup>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\<^sup>T) * (v \ -i \ -i\<^sup>T)\<^sup>\ * i * top \ bot" using le_bot semiring.mult_zero_left by fastforce hence 6: "(v \ i\<^sup>T) * (v \ -i \ -i\<^sup>T)\<^sup>\ * i * top \ (v \ -i \ -i\<^sup>T)\<^sup>\ * i * top" using bot_least le_bot by blast have 8: "v = (v \ i) \ (v \ i\<^sup>T) \ (v \ -i \ -i\<^sup>T)" proof - have 81: "regular i" by (simp add: assms(4) arc_regular) have "(v \ i\<^sup>T) \ (v \ -i \ -i\<^sup>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\<^sup>T) \ (v \ -i \ -i\<^sup>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\<^sup>T)\<^sup>\ * i * top \ (v \ i\<^sup>T) * (v \ -i \ -i\<^sup>T)\<^sup>\ * i * top \ (v \ -i \ -i\<^sup>T) * (v \ -i \ -i\<^sup>T)\<^sup>\ * i * top \ (v \ -i \ -i\<^sup>T)\<^sup>\ * i * top" using 4 5 6 by simp hence "((v \ i) \ (v \ i\<^sup>T) \ (v \ -i \ -i\<^sup>T)) * (v \ -i \ -i\<^sup>T)\<^sup>\ * i * top \ (v \ -i \ -i\<^sup>T)\<^sup>\ * i * top" by (simp add: mult_right_dist_sup) hence "v * (v \ -i \ -i\<^sup>T)\<^sup>\ * i * top \ (v \ -i \ -i\<^sup>T)\<^sup>\ * i * top" using 8 by auto hence "i * top \ v * (v \ -i \ -i\<^sup>T)\<^sup>\ * i * top \ (v \ -i \ -i\<^sup>T)\<^sup>\ * i * top" using 3 by auto hence 9:"v\<^sup>\ * (v \ -i \ -i\<^sup>T)\<^sup>\ * i * top \ (v \ -i \ -i\<^sup>T)\<^sup>\ * i * top" by (simp add: star_left_induct_mult mult_assoc) have "v\<^sup>\ * i * top \ v\<^sup>\ * (v \ -i \ -i\<^sup>T)\<^sup>\ * i * top" using 3 mult_right_isotone mult_assoc by auto thus ?thesis using 9 order.trans by blast qed finally have "e\<^sup>T * top \ (v \ -i \ -i\<^sup>T)\<^sup>\ * i * top" by simp hence "i * top \ (v \ -i \ -i\<^sup>T)\<^sup>\\<^sup>T * e\<^sup>T * top" using 2 by (metis bijective_reverse mult_assoc) also have "... = (v\<^sup>T \ -i \ -i\<^sup>T)\<^sup>\ * e\<^sup>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\<^sup>T) \ (v\<^sup>T \ -i \ -i\<^sup>T))\<^sup>\ * e\<^sup>T * top" by (simp add: mult_left_isotone star_isotone) finally have "i \ ((v\<^sup>T \ -i \ -i\<^sup>T) \ (v \ -i \ -i\<^sup>T))\<^sup>\ * e\<^sup>T * top" using dual_order.trans top_right_mult_increasing sup_commute by auto also have "... = (v\<^sup>T \ -i \ -i\<^sup>T)\<^sup>\ * (v \ -i \ -i\<^sup>T)\<^sup>\ * e\<^sup>T * top" using 1 cancel_separate_1 by (simp add: sup_commute) also have "... \ (v\<^sup>T \ -i \ -i\<^sup>T)\<^sup>\ * v\<^sup>\ * e\<^sup>T * top" by (simp add: inf_assoc mult_left_isotone mult_right_isotone star_isotone) also have "... = (v\<^sup>T \ -i \ -i\<^sup>T)\<^sup>\ * e\<^sup>T * top" using assms(2) mult_assoc by simp also have "... \ (v\<^sup>T \ -i\<^sup>T)\<^sup>\ * e\<^sup>T * top" by (metis mult_left_isotone star_isotone inf.cobounded2 inf.left_commute inf.sup_monoid.add_commute) also have "... = (v \ -i)\<^sup>T\<^sup>\ * e\<^sup>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\<^sup>T)" and "vector j" and "regular j" and "forest h" - and "forest_components h \ forest_components f" - and "big_forest (forest_components h) d" + and "forest_modulo_equivalence (forest_components h) d" and "d * top \ - j" and "forest_components h * j = j" - and "forest_components f = (forest_components h * (d \ d\<^sup>T))\<^sup>\ * forest_components h" and "f \ f\<^sup>T = h \ h\<^sup>T \ d \ d\<^sup>T" - and "(\ a b . bf_between_arcs a b (forest_components h) d \ a \ -(forest_components h) \ -- g \ b \ d \ sum(b \ g) \ sum(a \ g))" + and "(\ 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)\<^sup>T \ - (path f h j g) \ (f \ - (selected_edge h j g)\<^sup>T \ (path f h j g))\<^sup>T \ (selected_edge h j g) \ w \ w\<^sup>T" proof - let ?p = "path f h j g" let ?e = "selected_edge h j g" let ?f = "(f \ -?e\<^sup>T \ -?p) \ (f \ -?e\<^sup>T \ ?p)\<^sup>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\<^sup>T \ g" from assms(4) obtain w where 2: "minimum_spanning_forest w g \ f \ w \ w\<^sup>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\<^sup>T * top * ?e\<^sup>T = ?e\<^sup>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\<^sup>T * top * ?e\<^sup>T \ -?F" - using 5 assms(17) conv_complement conv_isotone by fastforce + 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\<^sup>T\<^sup>\" let ?v = "(w \ -(top * ?e * w\<^sup>T\<^sup>\)) \ ?q\<^sup>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\<^sup>T\<^sup>\)" by (simp add: covector_mult_closed) next show "top * ?e * w\<^sup>T\<^sup>\ * w\<^sup>T \ top * ?e * w\<^sup>T\<^sup>\" by (simp add: mult_right_isotone star.right_plus_below_circ mult_assoc) next show "coreflexive ((top * ?e * w\<^sup>T\<^sup>\)\<^sup>T * (top * ?e * w\<^sup>T\<^sup>\) \ w\<^sup>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\<^sup>T\<^sup>\) \ (w \ top * ?e * w\<^sup>T\<^sup>\)\<^sup>T)" using 8 by simp next show "regular (w \ top * ?e * w\<^sup>T\<^sup>\)" 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\<^sup>T\<^sup>\)" by (simp add: covector_mult_closed) qed next show "?v \ --g" proof (rule sup_least) show "w \ - (top * ?e * w\<^sup>T\<^sup>\) \ - - g" using 7 inf.coboundedI1 minimum_spanning_forest_def spanning_forest_def 2 by blast next show "(w \ top * ?e * w\<^sup>T\<^sup>\)\<^sup>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\<^sup>T\<^sup>\) \ g) + sum (?q\<^sup>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\<^sup>T\<^sup>\) \ g) + sum (?q \ g)" by (simp add: assms(1) sum_symmetric) also have "... = sum (((w \ -(top * ?e * w\<^sup>T\<^sup>\)) \ ?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\<^sup>T = w \ w\<^sup>T" proof - have "?v \ ?v\<^sup>T = (w \ -?q) \ ?q\<^sup>T \ (w\<^sup>T \ -?q\<^sup>T) \ ?q" using conv_complement conv_dist_inf conv_dist_sup inf_import_p sup_assoc by simp also have "... = w \ w\<^sup>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\<^sup>T = bot" proof (rule kruskal_reroot_edge) show "injective (?e\<^sup>T * top)" - using assms(18) minarc_arc minarc_bot_iff by blast + 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)\<^sup>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\<^sup>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(18) minarc_arc minarc_bot_iff by auto + 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\<^sup>T * ?F)" by (meson inf_le1 inf_le2 le_infI order_trans) also have "... \ ?F * (top * ?e\<^sup>T * ?F)\<^sup>T" by (simp add: covector_mult_closed covector_restrict_comp_conv) also have "... = ?F * ?F\<^sup>T * ?e\<^sup>T\<^sup>T * top\<^sup>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\<^sup>T * (?F \ ?v \ -?i)\<^sup>T\<^sup>\" proof - have "?i \ ?v \ - ?F * ?e * top \ top * ?e\<^sup>T * (?F \ ?v)\<^sup>T\<^sup>\ * (?F \ ?v)\<^sup>\" 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\<^sup>T * (?F \ ?v)\<^sup>T\<^sup>\ * (1 \ (?F \ ?v)\<^sup>\ * (?F \ ?v))" using star_left_unfold_equal star.circ_right_unfold_1 by auto also have "... = ?v \ - ?F * ?e * top \ (top * ?e\<^sup>T * (?F \ ?v)\<^sup>T\<^sup>\ \ top * ?e\<^sup>T * (?F \ ?v)\<^sup>T\<^sup>\ * (?F \ ?v)\<^sup>\ * (?F \ ?v))" by (simp add: mult_left_dist_sup mult_assoc) also have "... = (?v \ - ?F * ?e * top \ top * ?e\<^sup>T * (?F \ ?v)\<^sup>T\<^sup>\) \ (?v \ - ?F * ?e * top \ top * ?e\<^sup>T * (?F \ ?v)\<^sup>T\<^sup>\ * (?F \ ?v)\<^sup>\ * (?F \ ?v))" using comp_inf.semiring.distrib_left by blast also have "... \ top * ?e\<^sup>T * (?F \ ?v)\<^sup>T\<^sup>\ \ (?v \ - ?F * ?e * top \ top * ?e\<^sup>T * (?F \ ?v)\<^sup>T\<^sup>\ * (?F \ ?v)\<^sup>\ * (?F \ ?v))" using comp_inf.semiring.add_right_mono inf_le2 by blast also have "... \ top * ?e\<^sup>T * (?F \ ?v)\<^sup>T\<^sup>\ \ (?v \ - ?F * ?e * top \ top * ?e\<^sup>T * (?F\<^sup>T \ ?v\<^sup>T)\<^sup>\ * (?F \ ?v)\<^sup>\ * (?F \ ?v))" by (simp add: conv_dist_inf) also have "... \ top * ?e\<^sup>T * (?F \ ?v)\<^sup>T\<^sup>\ \ (?v \ - ?F * ?e * top \ top * ?e\<^sup>T * ?F\<^sup>T\<^sup>\ * ?F\<^sup>\ * (?F \ ?v))" proof - have "top * ?e\<^sup>T * (?F\<^sup>T \ ?v\<^sup>T)\<^sup>\ * (?F \ ?v)\<^sup>\ * (?F \ ?v) \ top * ?e\<^sup>T * ?F\<^sup>T\<^sup>\ * ?F\<^sup>\ * (?F \ ?v)" using star_isotone by (simp add: comp_isotone) hence "?v \ - ?F * ?e * top \ top * ?e\<^sup>T * (?F\<^sup>T \ ?v\<^sup>T)\<^sup>\ * (?F \ ?v)\<^sup>\ * (?F \ ?v) \ ?v \ - ?F * ?e * top \ top * ?e\<^sup>T * ?F\<^sup>T\<^sup>\ * ?F\<^sup>\ * (?F \ ?v)" using inf.sup_right_isotone by blast thus ?thesis using sup_right_isotone by blast qed also have "... = top * ?e\<^sup>T * (?F \ ?v)\<^sup>T\<^sup>\ \ (?v \ - ?F * ?e * top \ top * ?e\<^sup>T * ?F\<^sup>\ * ?F\<^sup>\ * (?F \ ?v))" using 5 by auto also have "... = top * ?e\<^sup>T * (?F \ ?v)\<^sup>T\<^sup>\ \ (?v \ - ?F * ?e * top \ top * ?e\<^sup>T * ?F * ?F * (?F \ ?v))" by (simp add: assms(2) forest_components_star) also have "... = top * ?e\<^sup>T * (?F \ ?v)\<^sup>T\<^sup>\ \ (?v \ - ?F * ?e * top \ top * ?e\<^sup>T * ?F * (?F \ ?v))" using 5 mult.semigroup_axioms preorder_idempotent semigroup.assoc by fastforce also have "... = top * ?e\<^sup>T * (?F \ ?v)\<^sup>T\<^sup>\" proof - have "?e * top * ?e\<^sup>T \ 1" - using assms(18) arc_expanded minarc_arc minarc_bot_iff by auto + using assms(16) arc_expanded minarc_arc minarc_bot_iff by auto hence "?F * ?e * top * ?e\<^sup>T \ ?F * 1" by (metis comp_associative comp_isotone mult_semi_associative star.circ_transitive_equal) hence "?v * ?v\<^sup>T * ?F * ?e * top * ?e\<^sup>T \ 1 * ?F * 1" using 8 by (smt comp_isotone mult_assoc) hence 171: "?v * ?v\<^sup>T * ?F * ?e * top * ?e\<^sup>T \ ?F" by simp hence "?v * (?F \ ?v)\<^sup>T * ?F * ?e * top * ?e\<^sup>T \ ?F" proof - have "?v * (?F \ ?v)\<^sup>T * ?F * ?e * top * ?e\<^sup>T \ ?v * ?v\<^sup>T * ?F * ?e * top * ?e\<^sup>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)\<^sup>T * ?F * ?e * top * ?e\<^sup>T)\<^sup>T \ -?v" by (smt schroeder_4_p comp_associative order_lesseq_imp pp_increasing) have "-?F * ((?F \ ?v)\<^sup>T * ?F * ?e * top * ?e\<^sup>T)\<^sup>T = -?F * ?e\<^sup>T\<^sup>T * top\<^sup>T * ?e\<^sup>T * ?F\<^sup>T * (?F \ ?v)\<^sup>T\<^sup>T" by (simp add: comp_associative conv_dist_comp) also have "... = -?F * ?e * top * ?e\<^sup>T * ?F * (?F \ ?v)" using 5 by auto also have "... = -?F * ?e * top * top * ?e\<^sup>T * ?F * (?F \ ?v)" using comp_associative by auto also have "... = -?F * ?e * top \ top * ?e\<^sup>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)\<^sup>T * ?F * ?e * top * ?e\<^sup>T)\<^sup>T = -?F * ?e * top \ top * ?e\<^sup>T * ?F * (?F \ ?v)" by simp hence "-?F * ?e * top \ top * ?e\<^sup>T * ?F * (?F \ ?v) \ -?v" using 172 by auto hence "?v \ -?F * ?e * top \ top * ?e\<^sup>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\<^sup>T * (?F \ ?v \ -?i)\<^sup>T\<^sup>\" 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\<^sup>T * ?w\<^sup>T\<^sup>\" proof - have "?i \ top * ?e\<^sup>T * (?F \ ?v \ -?i)\<^sup>T\<^sup>\" using 17 by simp also have "... \ top * ?e\<^sup>T * (?v \ -?i)\<^sup>T\<^sup>\" 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\<^sup>T * ((?v \ -?i) \ ?e)\<^sup>T\<^sup>\" using mult_right_isotone conv_isotone star_isotone sup_ge1 by simp finally show ?thesis by blast qed have 19: "?i \ top * ?e\<^sup>T * ?v\<^sup>T\<^sup>\" proof - have "?i \ top * ?e\<^sup>T * (?F \ ?v \ -?i)\<^sup>T\<^sup>\" using 17 by simp also have "... \ top * ?e\<^sup>T * (?v \ -?i)\<^sup>T\<^sup>\" 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\<^sup>T * (?v)\<^sup>T\<^sup>\" using mult_right_isotone conv_isotone star_isotone by auto finally show ?thesis by blast qed have 20: "f \ f\<^sup>T \ (?v \ -?i \ -?i\<^sup>T) \ (?v\<^sup>T \ -?i \ -?i\<^sup>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\<^sup>T \ w \ - (top * ?e * w\<^sup>T\<^sup>\) \ (w \ top * ?e * w\<^sup>T\<^sup>\)\<^sup>T \ (w \ - (top * ?e * w\<^sup>T\<^sup>\) \ (w \ top * ?e * w\<^sup>T\<^sup>\)\<^sup>T)\<^sup>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\<^sup>T" proof (intro conjI) have 211: "?e\<^sup>T \ ?v\<^sup>\" 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\<^sup>T\<^sup>\) \ (w \ top * ?e * w\<^sup>T\<^sup>\)\<^sup>T)" using 9 by simp next show "(w \ - (top * ?e * w\<^sup>T\<^sup>\) \ (w \ top * ?e * w\<^sup>T\<^sup>\)\<^sup>T) * ?e\<^sup>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(18) minarc_arc minarc_bot_iff by blast + 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\<^sup>T = bot" using 13 by auto next show "?e * ?F * ?e = bot" by (simp add: 6) next show "?e\<^sup>T \ ?v\<^sup>\" using 211 by auto next show "?e \ bot" - by (simp add: assms(18)) + by (simp add: assms(16)) qed show "minimum_spanning_forest ?w g" proof (unfold minimum_spanning_forest_def, intro conjI) have "(?v \ -?i) * ?e\<^sup>T \ ?v * ?e\<^sup>T" using inf_le1 mult_left_isotone by simp hence "(?v \ -?i) * ?e\<^sup>T = bot" using 13 le_bot by simp hence 221: "?e * (?v \ -?i)\<^sup>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)\<^sup>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\<^sup>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\<^sup>T *?v\<^sup>T\<^sup>\" using 19 by simp next show "?v * ?e\<^sup>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(20, 21) by auto + using assms(18, 19) by auto finally show "?w \ --g" by simp next have 223: "?i \ (?v \ -?i)\<^sup>T\<^sup>\ * ?e\<^sup>T * top" proof (rule boruvka_exchange_spanning_inv) show "forest ?v" using 10 spanning_forest_def by blast next show "?v\<^sup>\ * ?e\<^sup>T = ?e\<^sup>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\<^sup>T * ?w\<^sup>T\<^sup>\" using 18 inf.sup_monoid.add_assoc by auto next show "arc ?i" using 212 by blast next show "arc ?e" - using assms(18) minarc_arc minarc_bot_iff by auto + 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\<^sup>T * ?v\<^sup>T\<^sup>\" using 19 by blast next show "?v * ?e\<^sup>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)\<^sup>T\<^sup>\ * ?e\<^sup>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(18) inf.left_commute inf_bot_right minarc_meet_bot by fastforce + 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_bigforest) + 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(19)) + 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 " big_forest (forest_components h) d" - by (simp add: assms(10)) + show " forest_modulo_equivalence (forest_components h) d" + by (simp add: assms(9)) next show "f \ f\<^sup>T = h \ h\<^sup>T \ d \ d\<^sup>T" - by (simp add: assms(14)) + by (simp add: assms(12)) next - show "\a b. bf_between_arcs a b (?H) d \ a \ - ?H \ - - g \ b \ d \ sum (b \ g) \ sum (a \ g)" - by (simp add: assms(15)) + 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(16) by auto + using assms(14) by auto next show "?e = ?e" by simp next show "arc ?i" using 212 by blast next - show "bf_between_arcs ?i ?e ?H (d \ ?e)" + show "forest_modulo_equivalence_path ?i ?e ?H (d \ ?e)" proof - have "d\<^sup>T * ?H * ?e = bot" - using assms(6, 7, 11, 12, 19) dT_He_eq_bot le_bot by blast + using assms(6, 7, 10 ,11, 17) dT_He_eq_bot le_bot by blast hence 251: "d\<^sup>T * ?H * ?e \ (?H * d)\<^sup>\ * ?H * ?e" by simp hence "d\<^sup>T * ?H * ?H * ?e \ (?H * d)\<^sup>\ * ?H * ?e" by (metis assms(8) forest_components_star star.circ_decompose_9 mult_assoc) hence "d\<^sup>T * (?H * d)\<^sup>\ * ?H * ?e \ (?H * d)\<^sup>\ * ?H * ?e" proof - have "d\<^sup>T * ?H * d \ 1" - using assms(10) big_forest_def dTransHd_le_1 by blast + using assms(9) forest_modulo_equivalence_def dTransHd_le_1 by blast hence "d\<^sup>T * ?H * d * (?H * d)\<^sup>\ * ?H * ?e \ (?H * d)\<^sup>\ * ?H * ?e" by (metis mult_left_isotone star.circ_circ_mult star_involutive star_one) hence "d\<^sup>T * ?H * ?e \ d\<^sup>T * ?H * d * (?H * d)\<^sup>\ * ?H * ?e \ (?H * d)\<^sup>\ * ?H * ?e" using 251 by simp hence "d\<^sup>T * (1 \ ?H * d * (?H * d)\<^sup>\) * ?H * ?e \ (?H * d)\<^sup>\ * ?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\<^sup>T * (?H * d)\<^sup>\ * ?H * ?e \ ?H * (?H * d)\<^sup>\ * ?H * ?e" by (simp add: mult_right_isotone mult_assoc) hence "?H * d\<^sup>T * (?H * d)\<^sup>\ * ?H * ?e \ ?H * ?H * (d * ?H)\<^sup>\ * ?e" by (smt star_slide mult_assoc) hence "?H * d\<^sup>T * (?H * d)\<^sup>\ * ?H * ?e \ ?H * (d * ?H)\<^sup>\ * ?e" by (metis assms(8) forest_components_star star.circ_decompose_9) hence "?H * d\<^sup>T * (?H * d)\<^sup>\ * ?H * ?e \ (?H * d)\<^sup>\ * ?H * ?e" using star_slide by auto hence "?H * d * (?H * d)\<^sup>\ * ?H * ?e \ ?H * d\<^sup>T * (?H * d)\<^sup>\ * ?H * ?e \ (?H * d)\<^sup>\ * ?H * ?e" by (smt le_supI star.circ_loop_fixpoint sup.cobounded2 sup_commute mult_assoc) hence "(?H * (d \ d\<^sup>T)) * (?H * d)\<^sup>\ * ?H * ?e \ (?H * d)\<^sup>\ * ?H * ?e" by (simp add: semiring.distrib_left semiring.distrib_right) hence "(?H * (d \ d\<^sup>T))\<^sup>\ * (?H * d)\<^sup>\ * ?H * ?e \ (?H * d)\<^sup>\ * ?H * ?e" by (simp add: star_left_induct_mult mult_assoc) hence 252: "(?H * (d \ d\<^sup>T))\<^sup>\ * ?H * ?e \ (?H * d)\<^sup>\ * ?H * ?e" by (smt mult_left_dist_sup star.circ_transitive_equal star_slide star_sup_1 mult_assoc) have "?i \ top * ?e\<^sup>T * ?F" by auto hence "?i\<^sup>T \ ?F\<^sup>T * ?e\<^sup>T\<^sup>T * top\<^sup>T" by (simp add: conv_dist_comp conv_dist_inf mult_assoc) hence "?i\<^sup>T * top \ ?F\<^sup>T * ?e\<^sup>T\<^sup>T * top\<^sup>T * top" using comp_isotone by blast also have "... = ?F\<^sup>T * ?e\<^sup>T\<^sup>T * top\<^sup>T" by (simp add: vector_mult_closed) also have "... = ?F * ?e\<^sup>T\<^sup>T * top\<^sup>T" by (simp add: conv_dist_comp conv_star_commute) also have "... = ?F * ?e * top" by simp also have "... = (?H * (d \ d\<^sup>T))\<^sup>\ * ?H * ?e * top" - by (simp add: assms(13)) + using assms(2, 8, 12) F_is_H_and_d by simp also have "... \ (?H * d)\<^sup>\ * ?H * ?e * top" by (simp add: 252 comp_isotone) also have "... \ (?H * (d \ ?e))\<^sup>\ * ?H * ?e * top" by (simp add: comp_isotone star_isotone) finally have "?i\<^sup>T * top \ (?H * (d \ ?e))\<^sup>\ * ?H * ?e * top" by blast thus ?thesis - using 212 assms(18) bf_between_arcs_def minarc_arc minarc_bot_iff by blast + using 212 assms(16) forest_modulo_equivalence_path_def minarc_arc minarc_bot_iff by blast qed next show "?i \ - ?H \ -- g" proof - - have 241: "?i \ -?H" + 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(20) by auto + 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\<^sup>T \ ?e" by (smt conv_dist_inf inf_le1 sup_left_isotone sup_mono inf.order_lesseq_imp) also have "... \ (?v \ -?i \ -?i\<^sup>T) \ (?v\<^sup>T \ -?i \ -?i\<^sup>T) \ ?e" using 20 sup_left_isotone by simp also have "... \ (?v \ -?i) \ (?v\<^sup>T \ -?i \ -?i\<^sup>T) \ ?e" by (metis inf.cobounded1 sup_inf_distrib2) also have "... = ?w \ (?v\<^sup>T \ -?i \ -?i\<^sup>T)" by (simp add: sup_assoc sup_commute) also have "... \ ?w \ (?v\<^sup>T \ -?i\<^sup>T)" using inf.sup_right_isotone inf_assoc sup_right_isotone by simp also have "... \ ?w \ ?w\<^sup>T" using conv_complement conv_dist_inf conv_dist_sup sup_right_isotone by simp finally show "?f \ ?w \ ?w\<^sup>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\<^sup>T \ - path f h j g \ (f \ - selected_edge h j g\<^sup>T \ path f h j g)\<^sup>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\<^sup>T \ -?p \ (f \ -?e\<^sup>T \ ?p)\<^sup>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\<^sup>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\<^sup>T)\<^sup>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\<^sup>T)\<^sup>T \ - ?e" proof - have "?p * (f \ - ?e\<^sup>T)\<^sup>T \ ?p * f\<^sup>T" by (simp add: conv_dist_inf mult_right_isotone) also have "... \ top * ?e * (f)\<^sup>T\<^sup>\ * f\<^sup>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\<^sup>T * ?p \ (f \ - ?e\<^sup>T)\<^sup>T * (f \ - ?e\<^sup>T))" proof - have "(?p\<^sup>T * ?p \ (f \ - ?e\<^sup>T)\<^sup>T * (f \ - ?e\<^sup>T)) \ ?p\<^sup>T * ?p \ f\<^sup>T * f" using conv_dist_inf inf.sup_right_isotone mult_isotone by simp also have "... \ (top * ?e * f\<^sup>T\<^sup>\)\<^sup>T * (top * ?e * f\<^sup>T\<^sup>\) \ f\<^sup>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\<^sup>T)" proof - have f_intersect_below: "(f \ - ?e\<^sup>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\<^sup>T \ ?p)\<^sup>T * (f \ - ?e\<^sup>T)\<^sup>\ * ?e = bot" proof - have "?e \ - (f\<^sup>T\<^sup>\ * f\<^sup>\)" by (simp add: assms(3)) hence "?e * top * ?e \ - (f\<^sup>T\<^sup>\ * f\<^sup>\)" by (metis arc_top_arc minarc_arc minarc_bot_iff semiring.mult_not_zero) hence "?e\<^sup>T * top * ?e\<^sup>T \ - (f\<^sup>T\<^sup>\ * f\<^sup>\)\<^sup>T" by (metis comp_associative conv_complement conv_dist_comp conv_isotone symmetric_top_closed) hence "?e\<^sup>T * top * ?e\<^sup>T \ - (f\<^sup>T\<^sup>\ * f\<^sup>\)" by (simp add: conv_dist_comp conv_star_commute) hence "?e * (f\<^sup>T\<^sup>\ * f\<^sup>\) * ?e \ bot" using triple_schroeder_p by auto hence 1: "?e * f\<^sup>T\<^sup>\ * f\<^sup>\ * ?e \ bot" using mult_assoc by auto have 2: "(f \ - ?e\<^sup>T)\<^sup>T\<^sup>\ \ f\<^sup>T\<^sup>\" by (simp add: conv_dist_inf star_isotone) have "(f \ - ?e\<^sup>T \ ?p)\<^sup>T * (f \ - ?e\<^sup>T)\<^sup>\ * ?e \ (f \ ?p)\<^sup>T * (f \ - ?e\<^sup>T)\<^sup>\ * ?e" by (simp add: comp_isotone conv_dist_inf inf.orderI inf.sup_monoid.add_assoc) also have "... \ (f \ ?p)\<^sup>T * f\<^sup>\ * ?e" by (simp add: comp_isotone star_isotone) also have "... \ (f \ top * ?e * (f)\<^sup>T\<^sup>\)\<^sup>T * f\<^sup>\ * ?e" using 2 by (metis comp_inf.comp_isotone comp_inf.coreflexive_transitive comp_isotone conv_isotone inf.idem top.extremum) also have "... = (f\<^sup>T \ (top * ?e * f\<^sup>T\<^sup>\)\<^sup>T) * f\<^sup>\ * ?e" by (simp add: conv_dist_inf) also have "... \ top * (f\<^sup>T \ (top * ?e * f\<^sup>T\<^sup>\)\<^sup>T) * f\<^sup>\ * ?e" using top_left_mult_increasing mult_assoc by auto also have "... = (top \ top * ?e * f\<^sup>T\<^sup>\) * f\<^sup>T * f\<^sup>\ * ?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\<^sup>T\<^sup>\ * f\<^sup>T * f\<^sup>\ * ?e" by simp also have "... \ top * ?e * f\<^sup>T\<^sup>\ * f\<^sup>\ * ?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\<^sup>T)\<^sup>\ * ?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\<^sup>T = ?e\<^sup>T * top * ?e\<^sup>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\<^sup>T)\<^sup>\ \ f\<^sup>\" by (simp add: star_isotone) hence "?e * (f \ - ?e\<^sup>T)\<^sup>\ * ?e \ ?e * f\<^sup>\ * ?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\<^sup>T) \ - ?e" proof - have 1: "?e \ - ?F" by (simp add: assms(3)) have "f \ - ?e\<^sup>T \ f" by simp hence "forest_components (f \ - ?e\<^sup>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\<^sup>T \ - ?p) \ --g" by (meson assms(1) boruvka_inner_invariant_def boruvka_outer_invariant_def inf.coboundedI1) have 2: "(f \ - ?e\<^sup>T \ ?p)\<^sup>T \ --g" proof - have "(f \ - ?e\<^sup>T \ ?p)\<^sup>T \ f\<^sup>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\<^sup>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\<^sup>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_components h \ forest_components f" - using assms(1) boruvka_inner_invariant_def by blast - next - show "big_forest (forest_components h) d" + 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 "forest_components f = (forest_components h * (d \ d\<^sup>T))\<^sup>\ * forest_components h" - using assms(1) boruvka_inner_invariant_def by blast - next show "f \ f\<^sup>T = h \ h\<^sup>T \ d \ d\<^sup>T" using assms(1) boruvka_inner_invariant_def by blast next - show "(\ a b . bf_between_arcs a b (forest_components h) d \ a \ -(forest_components h) \ -- g \ b \ d \ sum(b \ g) \ sum(a \ g))" + 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 assms(1) boruvka_inner_invariant_def boruvka_outer_invariant_def by auto + 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\<^sup>T \ - path f h j g \ (f \ - selected_edge h j g\<^sup>T \ path f h j g)\<^sup>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\<^sup>T \ -?p \ (f \ -?e\<^sup>T \ ?p)\<^sup>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) - have 1: "boruvka_outer_invariant ?f' g" + show 1: "boruvka_outer_invariant ?f' g" using assms(1, 2, 3, 4) boruvka_outer_invariant_when_e_not_bot by blast - show "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 - 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 ?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 - show "boruvka_outer_invariant h g" + 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) - show "?H \ forest_components ?f'" - proof - - have 2: "?F \ forest_components ?f'" - proof (rule components_disj_increasing) - 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[1] - next - show "regular ?e" - using assms(1) boruvka_inner_invariant_def boruvka_outer_invariant_def minarc_regular regular_closed_star regular_conv_closed regular_mult_closed by auto[1] - next - show "injective ?f'" - using 1 boruvka_outer_invariant_def by blast - next - show "injective f" - using assms(1) boruvka_inner_invariant_def boruvka_outer_invariant_def by blast - qed - thus ?thesis - using assms(1) boruvka_inner_invariant_def dual_order.trans by blast - qed - show "big_forest ?H ?d'" - using assms(1, 2, 3, 4) big_forest_d_U_e boruvka_inner_invariant_def boruvka_outer_invariant_def by auto + 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\<^sup>T)" - using assms(1) boruvka_inner_invariant_def boruvka_outer_invariant_def component_is_regular regular_conv_closed regular_mult_closed by auto - hence "minarc(?c * - ?c\<^sup>T \ g) = minarc(?c \ - ?c\<^sup>T \ g)" + 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\<^sup>T \ g) = minarc(?c \ - ?c\<^sup>T \ g)" by (metis component_is_vector covector_comp_inf inf_top.left_neutral vector_conv_compl) also have "... \ -- (?c \ - ?c\<^sup>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 - hence "?e * top \ ?c" + 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 "?H * ?j' = ?j'" - using fc_j_eq_j_inv assms(1) boruvka_inner_invariant_def by blast - next - show "forest_components ?f' = (?H * (?d' \ ?d'\<^sup>T))\<^sup>\ * ?H" - proof - - have "forest_components ?f' = (f \ f\<^sup>T \ ?e \ ?e\<^sup>T)\<^sup>\" - proof (rule simplify_forest_components_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 auto - next - show "injective ?f'" - using assms(1, 2, 3, 4) boruvka_outer_invariant_def boruvka_outer_invariant_when_e_not_bot by blast - next - show "injective f" - using assms(1) boruvka_inner_invariant_def boruvka_outer_invariant_def by blast - qed - also have "... = (h \ h\<^sup>T \ d \ d\<^sup>T \ ?e \ ?e\<^sup>T)\<^sup>\" - using assms(1) boruvka_inner_invariant_def by simp - also have "... = (h \ h\<^sup>T \ ?d' \ ?d'\<^sup>T)\<^sup>\" - by (smt conv_dist_sup sup_monoid.add_assoc sup_monoid.add_commute) - also have "... = ((h \ h\<^sup>T)\<^sup>\ * (?d' \ ?d'\<^sup>T))\<^sup>\ * (h \ h\<^sup>T)\<^sup>\" - by (metis star.circ_sup_9 sup_assoc) - finally show ?thesis - using assms(1) boruvka_inner_invariant_def forest_components_wcc by simp - qed - next show "?f' \ ?f'\<^sup>T = h \ h\<^sup>T \ ?d' \ ?d'\<^sup>T" proof - have "?f' \ ?f'\<^sup>T = f \ - ?e\<^sup>T \ - ?p \ (f \ - ?e\<^sup>T \ ?p)\<^sup>T \ ?e \ (f \ - ?e\<^sup>T \ - ?p)\<^sup>T \ (f \ - ?e\<^sup>T \ ?p) \ ?e\<^sup>T" by (simp add: conv_dist_sup sup_monoid.add_assoc) also have "... = (f \ - ?e\<^sup>T \ - ?p) \ (f \ - ?e\<^sup>T \ ?p) \ (f \ - ?e\<^sup>T \ ?p)\<^sup>T \ (f \ - ?e\<^sup>T \ - ?p)\<^sup>T \ ?e\<^sup>T \ ?e" by (simp add: sup.left_commute sup_commute) also have "... = f \ f\<^sup>T \ ?e \ ?e\<^sup>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\<^sup>T \ d \ d\<^sup>T \ ?e \ ?e\<^sup>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 . bf_between_arcs a b ?H ?d' \ a \ - ?H \ -- g \ b \ ?d' \ sum (b \ g) \ sum (a \ g)" - proof (intro allI, rule impI, unfold bf_between_arcs_def) + 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\<^sup>T * top \ (?H * ?d')\<^sup>\ * ?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_bigforest) + 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 " big_forest (forest_components h) d" + show "forest_modulo_equivalence (forest_components h) d" using assms(1) boruvka_inner_invariant_def by blast next show "f \ f\<^sup>T = h \ h\<^sup>T \ d \ d\<^sup>T" using assms(1) boruvka_inner_invariant_def by blast next - show "\a b. bf_between_arcs a b (?H) d \ a \ - ?H \ - - g \ b \ d \ sum (b \ g) \ sum (a \ g)" + 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 "bf_between_arcs a b ?H ?d'" - using 1 bf_between_arcs_def by simp + 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 - hence b_below_d: "b \ d" - using 1 by (metis assms(4) different_arc_in_sup_arc minarc_arc minarc_bot_iff) + 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 - hence "bf_between_arcs a b ?H d \ b \ d" - using 1 bf_between_arcs_def sup.absorb1 by auto + 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 - hence 72: "bf_between_arcs a b ?H ?d' \ bf_between_arcs a b ?H d \ (bf_between_arcs a ?e ?H d \ bf_between_arcs ?e b ?H d)" - proof (rule big_forest_path_split_disj) + 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 "bf_between_arcs a b ?H d") + proof (cases "forest_modulo_equivalence_path a b ?H d") case True - have "bf_between_arcs a b ?H d \ b \ d" - using 1 by (metis assms(4) True b_not_equal_e minarc_arc minarc_bot_iff different_arc_in_sup_arc) + 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:"bf_between_arcs a ?e ?H d \ bf_between_arcs ?e b ?H d" - using 1 72 False bf_between_arcs_def by blast + 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 "?e \ - ?H" - by (meson assms(1, 3) boruvka_inner_invariant_def dual_order.trans p_antitone_iff) - hence "?e \ - ?H \ --g" + 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 - hence 75: "sum (b \ g) \ sum (?e \ g)" + then have 75: "sum (b \ g) \ sum (?e \ g)" using assms(1) b_below_d 73 boruvka_inner_invariant_def by blast - have 76: "bf_between_arcs a ?e ?H ?d'" - using 73 by (meson big_forest_path_split_disj assms(1) bf_between_arcs_def boruvka_inner_invariant_def boruvka_outer_invariant_def fch_equivalence arc_regular regular_closed_star regular_conv_closed regular_mult_closed) + 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_bigforest) + 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 " big_forest (forest_components h) d" + show "forest_modulo_equivalence (forest_components h) d" using assms(1) boruvka_inner_invariant_def by blast next show "f \ f\<^sup>T = h \ h\<^sup>T \ d \ d\<^sup>T" using assms(1) boruvka_inner_invariant_def by blast next - show "\a b. bf_between_arcs a b (?H) d \ a \ - ?H \ - - g \ b \ d \ sum (b \ g) \ sum (a \ g)" + 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 "bf_between_arcs a ?e ?H ?d'" - by (simp add: 76) + 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 - next - show "regular ?d'" - using assms(1) boruvka_inner_invariant_def minarc_regular by auto 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\<^sup>T \ - path f h j g \ (f \ - selected_edge h j g\<^sup>T \ path f h j g)\<^sup>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\<^sup>T \ -?p \ (f \ -?e\<^sup>T \ ?p)\<^sup>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, 3) boruvka_inner_invariant_def by auto + 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 "vector ?j'" - by (metis assms(3) boruvka_inner_invariant_def component_is_vector vector_complement_closed vector_inf_closed) + 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 "boruvka_outer_invariant h g" + 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 \ forest_components ?f'" - using assms(1, 3) boruvka_inner_invariant_def by auto - next - show " big_forest ?H ?d'" - using assms(1, 3) boruvka_inner_invariant_def by auto - next - show "?d' * top \ -?j'" - by (metis assms(1, 3) boruvka_inner_invariant_def order.trans p_antitone_inf sup_monoid.add_0_right) - next show "?H * ?j' = ?j'" using assms(3) fc_j_eq_j_inv boruvka_inner_invariant_def by blast next - show "forest_components ?f' = (?H * (?d' \ ?d'\<^sup>T))\<^sup>\ *?H" - using assms(1, 3) boruvka_inner_invariant_def by auto + 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'\<^sup>T = h \ h\<^sup>T \ ?d' \ ?d'\<^sup>T" using assms(1, 3) boruvka_inner_invariant_def by auto next - show "\a b. bf_between_arcs 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 - next - show "regular ?d'" + 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\<^sup>T \ g); IF e \ -(forest_components f) THEN f := f \ -e\<^sup>T; f := (f \ -(top * e * f\<^sup>T\<^sup>\)) \ (f \ top * e * f\<^sup>T\<^sup>\)\<^sup>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 "boruvka_outer_invariant f g" - using 1 by auto + 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 "?F \ ?F" - by simp - next - show "big_forest ?F bot" - by (simp add: 2 big_forest_def) + 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 * (bot \ bot\<^sup>T))\<^sup>\ * ?F" - by (metis mult_right_zero semiring.mult_zero_left star.circ_loop_fixpoint sup_commute sup_monoid.add_0_right symmetric_bot_closed) - next show "f \ f\<^sup>T = f \ f\<^sup>T \ bot \ bot\<^sup>T" by simp next - show "\ a b. bf_between_arcs a b ?F bot \ a \ - ?F \ -- g \ b \ bot \ sum (b \ g) \ sum (a \ g)" - by (metis (full_types) bf_between_arcs_def bot_unique mult_left_zero mult_right_zero top.extremum) - next - show "regular bot" - by auto + 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\<^sup>T \ -?p \ (f \ -?e\<^sup>T \ ?p)\<^sup>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 "boruvka_outer_invariant h g" - using 1 boruvka_inner_invariant_def by auto + 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 "?H \ ?F" - using 1 boruvka_inner_invariant_def by blast - next - show "big_forest ?H d" + 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 = (?H * (d \ d\<^sup>T))\<^sup>\ * ?H" - using 1 boruvka_inner_invariant_def by blast - next show "f \ f\<^sup>T = h \ h\<^sup>T \ d \ d\<^sup>T" using 1 boruvka_inner_invariant_def by blast next - show "\ ?e \ -?F \ \a b. bf_between_arcs a b ?H d \ a \ -?H \ --g \ b \ d \ sum(b \ g) \ sum(a \ g)" - using 1 boruvka_inner_invariant_def by blast - next - show "\ ?e \ -?F \ regular d" + 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)\<^sup>\ \ ?F\<^sup>\" 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\<^sup>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\<^sup>T\<^sup>\ * f\<^sup>\" using 2 spanning_forest_def inf.sup_right_isotone by simp also have "... \ f \ f\<^sup>T" proof (rule cancel_separate_6[where z=w and y="w\<^sup>T"]) show "injective w" using 3 minimum_spanning_forest_def spanning_forest_def by simp next show "f\<^sup>T \ w\<^sup>T \ w" using 3 by (metis conv_dist_inf conv_dist_sup conv_involutive inf.cobounded2 inf.orderE) next show "f \ w\<^sup>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\<^sup>T\<^sup>\ = 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\<^sup>T" by simp have "sum (f \ g) = sum ((w \ w\<^sup>T) \ (f \ g))" using 3 by (metis inf_absorb2 inf.assoc) also have "... = sum (w \ (f \ g)) + sum (w\<^sup>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\<^sup>T \ g\<^sup>T))" by (metis conv_dist_inf conv_involutive sum_conv) also have "... = sum (f \ (w \ g)) + sum (f\<^sup>T \ (w \ g))" proof - have 51:"f\<^sup>T \ (w \ g) = f\<^sup>T \ (w \ g\<^sup>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\<^sup>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 + diff --git a/thys/Relational_Minimum_Spanning_Trees/document/root.tex b/thys/Relational_Minimum_Spanning_Trees/document/root.tex --- a/thys/Relational_Minimum_Spanning_Trees/document/root.tex +++ b/thys/Relational_Minimum_Spanning_Trees/document/root.tex @@ -1,58 +1,57 @@ \documentclass[11pt,a4paper]{article} \usepackage[T1]{fontenc} \usepackage{isabelle,isabellesym} \usepackage{amssymb,ragged2e} \usepackage{pdfsetup} \isabellestyle{it} \renewenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}\justifying\color{blue}}{\end{isapar}} \renewcommand\labelitemi{$*$} \urlstyle{rm} \begin{document} \title{Relational Minimum Spanning Tree Algorithms} \author{Walter Guttmann and Nicolas Robinson-O'Brien} \maketitle \begin{abstract} We verify the correctness of Prim's, Kruskal's and Bor\r{u}vka's minimum spanning tree algorithms based on algebras for aggregation and minimisation. \end{abstract} \tableofcontents \section{Overview} The theories described in this document prove the correctness of Prim's, Kruskal's and Bor\r{u}vka's minimum spanning tree algorithms. Specifications and algorithms work in Stone-Kleene relation algebras extended by operations for aggregation and minimisation. The algorithms are implemented in a simple imperative language and their proof uses Hoare logic. The correctness proofs are discussed in \cite{Guttmann2016c,Guttmann2018b,Guttmann2018c,RobinsonOBrien2020}. \subsection{Prim's and Kruskal's minimum spanning tree algorithms} A framework based on Stone relation algebras and Kleene algebras and extended by operations for aggregation and minimisation was presented by the first author in \cite{Guttmann2016c,Guttmann2018b} and used to formally verify the correctness of Prim's minimum spanning tree algorithm. It was extended in \cite{Guttmann2018c} and applied to prove the correctness of Kruskal's minimum spanning tree algorithm. Two theories, one each for Prim's and Kruskal's algorithms, prove total correctness of these algorithms. As case studies for the algebraic framework, these two theories combined were originally part of another AFP entry \cite{Guttmann2018a}. \subsection{Bor\r{u}vka's minimum spanning tree algorithm} Otakar Bor\r{u}vka formalised the minimum spanning tree problem and proposed a solution to it \cite{Boruvka1926}. Bor\r{u}vka's original paper is written in Czech; translations of varying completeness can be found in \cite{GrahamHell1985,NesetrilMilkovaNesetrilova2001}. The theory for Bor\r{u}vka's minimum spanning tree algorithm proves partial correctness of this algorithm. This work is based on the same algebraic framework as the proof of Kruskal's algorithm; in particular it uses many theories from the hierarchy underlying \cite{Guttmann2018a}. The theory for Bor\r{u}vka's algorithm formally verifies results from the second author's Master's thesis \cite{RobinsonOBrien2020}. -Certain lemmas in this theory are numbered for easy correlation to theorems from the thesis. \begin{flushleft} \input{session} \end{flushleft} \bibliographystyle{abbrv} \bibliography{root} \end{document}