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,3620 +1,3620 @@ (* 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: 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 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\ lemma expand_big_forest: assumes "big_forest 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 hence "d\<^sup>T * H * H * d \ 1" using assms big_forest_def conv_dist_comp by auto thus ?thesis by (simp add: cancel_separate_eq comp_associative) qed lemma big_forest_path_bot: assumes "arc a" and "a \ d" and "big_forest H d" shows "(d \ - a)\<^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 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) 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 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 also have "... \ d * top \ H * a * 1" using 1 by (metis inf.sup_right_isotone mult_right_isotone mult_assoc) also have "... \ H * a" by simp also have "... \ top * a" by (simp add: mult_left_isotone) finally have "d \ H * a * top \ top * a" by simp thus ?thesis by simp qed have "d \ H * a * top \ a * top \ top * a" using 2 3 by simp also have "... = a * top * top * a" by (metis comp_associative comp_inf.star.circ_decompose_9 comp_inf.star_star_absorb comp_inf_covector vector_inf_comp vector_top_closed) also have "... = a * top * a" by (simp add: vector_mult_closed) finally have 4:"d \ H * a * top \ a" by (simp add: assms(1) arc_top_arc) hence "d \ - a \ -(H * a * top)" using assms(1) arc_regular p_shunting_swap by fastforce hence "(d \ - a) * top \ -(H * a * top)" using mult.semigroup_axioms p_antitone_iff schroeder_4_p semigroup.assoc by fastforce thus ?thesis by (simp add: schroeder_3_p) qed lemma big_forest_path_split_2: assumes "arc a" and "a \ d" and "big_forest H d" shows "(H * (d \ - a))\<^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 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) 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) also have "... = H * ((d \ - a) * H)\<^sup>\ * H * a * top" using assms(3) big_forest_def preorder_idempotent by fastforce finally show ?thesis by (metis assms(3) big_forest_def preorder_idempotent star_slide mult_assoc) qed have 5: "(H * (d \ - a) \ H * (d \ - a)\<^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 subsection \An operation to select components\ text \ We introduce the operation \choose_component\. \begin{itemize} \item Axiom \component_in_v\ expresses that the result of \choose_component\ is contained in the set of vertices, $v$, we are selecting from, ignoring the weights. \item Axiom \component_is_vector\ states that the result of \choose_component\ is a vector. \item Axiom \component_is_regular\ states that the result of \choose_component\ is regular. \item Axiom \component_is_connected\ states that any two vertices from the result of \choose_component\ are connected in $e$. \item Axiom \component_single\ states that the result of \choose_component\ is closed under being connected in $e$. \item Finally, axiom \component_not_bot_when_v_bot_bot\ expresses that the operation \choose_component\ returns a non-empty component if the input satisfies the given criteria. \end{itemize} \ class choose_component = fixes choose_component :: "'a \ 'a \ 'a" class choose_component_algebra = choose_component + stone_relation_algebra + assumes component_in_v: "choose_component e v \ --v" assumes component_is_vector: "vector (choose_component e v)" assumes component_is_regular: "regular (choose_component e v)" assumes component_is_connected: "choose_component e v * (choose_component e v)\<^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\ text \ Every \m_kleene_algebra\ is an instance of \choose_component_algebra\ when the \choose_component\ operation is defined as follows: \ context m_kleene_algebra begin definition "choose_component_input_condition e v \ regular e \ equivalence e \ vector v \ regular v \ e * v = v" definition "m_choose_component e v \ if choose_component_input_condition e v then e * minarc(v) * top else bot" sublocale m_choose_component_algebra: choose_component_algebra where choose_component = m_choose_component proof fix e v show "m_choose_component e v \ -- v" proof (cases "choose_component_input_condition e v") case True hence "m_choose_component e v = e * minarc(v) * top" by (simp add: m_choose_component_def) also have "... \ e * --v * top" by (simp add: comp_isotone minarc_below) also have "... = e * v * top" using True choose_component_input_condition_def by auto also have "... = v * top" using True choose_component_input_condition_def by auto finally show ?thesis using True choose_component_input_condition_def by auto next case False hence "m_choose_component e v = bot" using False m_choose_component_def by auto thus ?thesis by simp qed next fix e v show "vector (m_choose_component e v)" proof (cases "choose_component_input_condition e v") case True thus ?thesis by (simp add: mult_assoc m_choose_component_def) next case False thus ?thesis by (simp add: m_choose_component_def) qed next fix e v show "regular (m_choose_component e v)" using choose_component_input_condition_def minarc_regular regular_closed_star regular_mult_closed m_choose_component_def by auto next fix e v show "m_choose_component e v * (m_choose_component e v)\<^sup>T \ e" proof (cases "choose_component_input_condition e v") case True assume 1: "choose_component_input_condition e v" hence "m_choose_component e v * (m_choose_component e v)\<^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 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 thus ?thesis using calculation by auto qed thus ?thesis by (simp add: calculation) next case False thus ?thesis by (simp add: m_choose_component_def) qed next fix e v show "m_choose_component e v = e * m_choose_component e v" proof (cases "choose_component_input_condition e v") case True thus ?thesis by (metis choose_component_input_condition_def preorder_idempotent m_choose_component_def mult_assoc) next case False thus ?thesis by (simp add: m_choose_component_def) qed next fix e v show "regular e \ equivalence e \ vector v \ regular v \ e * v = v \ v \ bot \ m_choose_component e v \ bot" proof (cases "choose_component_input_condition e v") case True hence "m_choose_component e v \ minarc(v) * top" by (metis choose_component_input_condition_def mult_1_left mult_left_isotone m_choose_component_def) also have "... \ minarc(v)" using calculation dual_order.trans top_right_mult_increasing by blast thus ?thesis using True bot_unique minarc_bot_iff by fastforce next case False thus ?thesis using choose_component_input_condition_def by blast qed qed end subsection \m-k-Stone-Kleene relation algebras\ text \ $m$-$k$-Stone-Kleene relation algebras are an extension of $m$-Kleene algebras where the \choose_component\ operation has been added. \ class m_kleene_algebra_choose_component = m_kleene_algebra + choose_component_algebra begin text \ A \selected_edge\ is a minimum-weight edge whose source is in a component, with respect to $h$, $j$ and $g$, and whose target is not in that component. \ abbreviation "selected_edge h j g \ minarc (choose_component (forest_components h) j * - choose_component (forest_components h) j\<^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 \ 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" 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\ text \ We prove a number of properties about \big_forest\ and \forest_components\. \ lemma fc_j_eq_j_inv: assumes "forest h" and "forest_components h * j = j" shows "forest_components h * (j \ - choose_component (forest_components h) j) = j \ - choose_component (forest_components h) j" proof - let ?c = "choose_component (forest_components h) j" let ?H = "forest_components h" have 1:"equivalence ?H" by (simp add: assms(1) forest_components_equivalence) have "?H * (j \ - ?c) = ?H * j \ ?H * - ?c" using 1 by (metis assms(2) equivalence_comp_dist_inf inf.sup_monoid.add_commute) hence 2: "?H * (j \ - ?c) = j \ ?H * - ?c" by (simp add: assms(2)) have 3: "j \ - ?c \ ?H * - ?c" using 1 by (metis assms(2) dedekind_1 dual_order.trans equivalence_comp_dist_inf inf.cobounded2) have "?H * ?c \ ?c" using component_single by auto hence "?H\<^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 antisym by simp qed text \Theorem 5\ text \ There is a path in the \big_forest\ between edges $a$ and $b$ if and only if there is either a path in the \big_forest\ from $a$ to $b$ or one from $a$ to $c$ and one from $c$ to $b$. \ lemma big_forest_path_split_disj: assumes "equivalence H" and "arc c" and "regular a \ regular b \ regular c \ regular d \ regular H" shows "bf_between_arcs a b H (d \ c) \ bf_between_arcs a b H d \ (bf_between_arcs a c H d \ bf_between_arcs c b H d)" proof - have 1: "bf_between_arcs a b H (d \ c) \ bf_between_arcs a b H d \ (bf_between_arcs a c H d \ bf_between_arcs c b H d)" proof (rule impI) assume 11: "bf_between_arcs a b H (d \ c)" hence "a\<^sup>T * top \ (H * (d \ c))\<^sup>\ * H * b * top" by (simp add: bf_between_arcs_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 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)" 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 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 thus ?thesis by simp qed qed have 2: "bf_between_arcs a b H d \ (bf_between_arcs a c H d \ bf_between_arcs c b H d) \ bf_between_arcs a b H (d \ c)" proof - have 21: "bf_between_arcs a b H d \ bf_between_arcs a b H (d \ c)" proof (rule impI) assume 22:"bf_between_arcs a b H d" hence "a\<^sup>T * top \ (H * d)\<^sup>\ * H * b * top" using bf_between_arcs_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 qed have "bf_between_arcs a c H d \ bf_between_arcs c b H d \ bf_between_arcs a b H (d \ c)" proof (rule impI) assume 23: "bf_between_arcs a c H d \ bf_between_arcs c b H d" hence "a\<^sup>T * top \ (H * d)\<^sup>\ * H * c * top" using bf_between_arcs_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) 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) 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 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: assumes "forest f" and "vector j" and "regular j" and "forest h" and "forest_components h \ forest_components f" and "big_forest (forest_components h) d" and "d * top \ - j" and "forest_components h * j = j" and "f \ f\<^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) 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" 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 thus ?thesis using 341 arc_injective le_infI2 by blast qed thus ?thesis using 1 31 32 33 34 by simp qed show 4:"(?H * (d \ ?e))\<^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" 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 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" 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 qed also have "... = (?H * d)\<^sup>+ \ (?H * d)\<^sup>\ * ?H * ?e \ (?H * d)\<^sup>\ * ?H * ?e * (?H * d)\<^sup>\ * ?H * d" by (smt eq_iff sup.left_commute sup.orderE sup_commute) 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 qed subsubsection \Identifying arcs\ text \ The expression $d \sqcap \top e^\top H \sqcap (H d^\top)^* H a^\top \top$ identifies the edge incoming to the component that the \selected_edge\, $e$, is outgoing from and which is on the path from edge $a$ to $e$. Here, we prove this expression is an \arc\. \ lemma shows_arc_x: assumes "big_forest H d" and "bf_between_arcs a e H d" and "H * d * (H * d)\<^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 have 3: "e * top * e\<^sup>T \ 1" using assms(2) bf_between_arcs_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 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 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) 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 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 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 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 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 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 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 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) hence "H * (d * H)\<^sup>\ \ - d\<^sup>T" using 511 by (metis assms(1) big_forest_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 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) 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 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) hence "d * (- 1 \ H) * d\<^sup>T \ - H" by (metis assms(1) big_forest_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 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) 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 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 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 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) 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) 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) 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) 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) 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 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 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) 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 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 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 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) 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) 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 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 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) 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 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 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. \ 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" proof - have "e \ -- (c * - c\<^sup>T \ g)" using assms(1) minarc_below order_trans by blast also have "... \ -- (c * - c\<^sup>T)" using order_lesseq_imp pp_isotone_inf by blast also have "... = c * - c\<^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" proof - let ?H = "forest_components h" have "x \ top * x" 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" by (simp add: conv_complement conv_dist_comp) also have "... \ top * c\<^sup>T * ?H" 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) 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" proof - let ?H = "forest_components h" have "x \ - ?H \ c\<^sup>T" using assms(3, 4) by auto also have "... \ - c" proof - have "c \ c\<^sup>T \ ?H" using assms(1, 2) vector_covector by auto hence "-?H \ c \ c\<^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" and "symmetric g" and "arc x" and "c \ bot" shows "sum (e \ g) \ sum (x \ g)" proof - let ?H = "forest_components h" have 1:"e \ c * - c\<^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" 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" 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" 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)" using 1 3 by (metis inf.orderE) hence "sum (e \ g) \ sum (x \ g)" using assms(9) sum_symmetric by auto thus ?thesis by simp qed lemma sum_e_below_sum_x_when_outgoing_same_component: assumes "symmetric g" and "vector j" and "forest h" and "x \ - forest_components h \ -- g" and "x\<^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) 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)) next show "?c \ bot" using assms(2, 5 , 6, 7) inf_bot_left le_bot minarc_bot mult_left_zero mult_right_zero by fastforce qed qed text \ If there is a path in the \big_forest\ from an edge between components, $a$, to the \selected_edge\, $e$, then the weight of $e$ is no greater than the weight of $a$. This is because either, \begin{itemize} \item the edges $a$ and $e$ are adjacent the same component so that we can use \sum_e_below_sum_x_when_outgoing_same_component\, or \item there is at least one edge between $a$ and $e$, namely $x$, the edge incoming to the component that $e$ is outgoing from. The path from $a$ to $e$ is split on $x$ using \big_forest_path_split_disj\. We show that the weight of $e$ is no greater than the weight of $x$ by making use of lemma \sum_e_below_sum_x_when_outgoing_same_component\. We define $x$ in a way that we can show that the weight of $x$ is no greater than the weight of $a$ using the invariant. Then, it follows that the weight of $e$ is no greater than the weight of $a$ owing to transitivity. \end{itemize} \ lemma a_to_e_in_bigforest: assumes "symmetric g" and "f \ --g" and "vector j" and "forest h" and "big_forest (forest_components h) d" and "f \ f\<^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 "regular d" and "j \ bot" and "b = selected_edge h j g" and "arc a" and "bf_between_arcs a b (forest_components h) (d \ selected_edge h j g)" and "a \ - forest_components h \ -- g" and "regular h" shows "sum (b \ g) \ sum (a \ g)" proof - let ?p = "path f h j g" let ?e = "selected_edge h j g" let ?F = "forest_components f" let ?H = "forest_components h" have "sum (b \ g) \ sum (a \ g)" proof (cases "a\<^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)) 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" by (simp add: assms(5)) next show "bf_between_arcs a ?e ?H d" proof - have 611: "bf_between_arcs a b ?H (d \ b)" using assms(10, 12) by auto have 616: "regular h" using assms(14) by auto have "regular a" using 611 bf_between_arcs_def arc_regular by fastforce thus ?thesis using 616 by (smt big_forest_path_split_disj assms(4, 8, 10, 12) bf_between_arcs_def fch_equivalence minarc_regular regular_closed_star regular_conv_closed regular_mult_closed) qed next show "(?H * d)\<^sup>+ \ - ?H" using assms(5) big_forest_def 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 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 have 66: "?x \ d" by (simp add: inf.sup_monoid.add_assoc) hence x_below_a: "sum (?x \ g) \ sum (a \ g)" using 65 bf_between_arcs_def assms(7, 13) by blast have "sum (?e \ g) \ sum (?x \ g)" proof (rule sum_e_below_sum_x_when_outgoing_same_component) show "symmetric g" using assms(1) by auto next show "vector j" using assms(3) by blast next show "forest h" by (simp add: assms(4)) next show "?x \ - ?H \ -- g" proof - have 67: "?x \ - ?H" using 66 assms(5) big_forest_def order_lesseq_imp by blast have "?x \ d" by (simp add: conv_isotone inf.sup_monoid.add_assoc) also have "... \ f \ f\<^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 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 "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 "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 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 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 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 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 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 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 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)) 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 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 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 have 225: "sum (?e \ g) \ sum (?i \ g)" proof (rule a_to_e_in_bigforest) 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)) 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)) next show "f \ f\<^sup>T = h \ h\<^sup>T \ d \ d\<^sup>T" by (simp add: assms(14)) 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)) next show "regular d" using assms(16) 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)" proof - have "d\<^sup>T * ?H * ?e = bot" using assms(6, 7, 11, 12, 19) 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 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)) 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 qed next show "?i \ - ?H \ -- g" proof - 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 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 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" 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))" 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 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" 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 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 show "regular ?j'" using assms(1) boruvka_inner_invariant_def by auto show "boruvka_outer_invariant h g" by (meson assms(1) boruvka_inner_invariant_def) show "injective h" by (meson assms(1) boruvka_inner_invariant_def) 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 "?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)" 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" 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) 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) 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" 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)" 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 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) 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 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) 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") 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) 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 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" using 74 by simp hence 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 77: "sum (?e \ g) \ sum (a \ g)" proof (rule a_to_e_in_bigforest) 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" 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)" 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) 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 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) next show "regular ?j'" using assms(3) boruvka_inner_invariant_def by auto next show "boruvka_outer_invariant h g" 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 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'" 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 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) 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 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 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" 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" using 1 boruvka_inner_invariant_def by blast qed qed next - fix f h d j - assume "boruvka_inner_invariant j f h g d \ j = bot" + 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/Kruskal.thy b/thys/Relational_Minimum_Spanning_Trees/Kruskal.thy --- a/thys/Relational_Minimum_Spanning_Trees/Kruskal.thy +++ b/thys/Relational_Minimum_Spanning_Trees/Kruskal.thy @@ -1,597 +1,595 @@ (* Title: Kruskal's Minimum Spanning Tree Algorithm Author: Walter Guttmann Maintainer: Walter Guttmann *) section \Kruskal's Minimum Spanning Tree Algorithm\ text \ In this theory we prove total correctness of Kruskal's minimum spanning tree algorithm. The proof uses the following steps \cite{Guttmann2018c}. We first establish that the algorithm terminates and constructs a spanning tree. This is a constructive proof of the existence of a spanning tree; any spanning tree algorithm could be used for this. We then conclude that a minimum spanning tree exists. This is necessary to establish the invariant for the actual correctness proof, which shows that Kruskal's algorithm produces a minimum spanning tree. \ theory Kruskal imports Aggregation_Algebras.Hoare_Logic Aggregation_Algebras.Aggregation_Algebras begin context m_kleene_algebra begin definition "spanning_forest f g \ forest f \ f \ --g \ components g \ forest_components f \ regular f" definition "minimum_spanning_forest f g \ spanning_forest f g \ (\u . spanning_forest u g \ sum (f \ g) \ sum (u \ g))" definition "kruskal_spanning_invariant f g h \ symmetric g \ h = h\<^sup>T \ g \ --h = h \ spanning_forest f (-h \ g)" definition "kruskal_invariant f g h \ kruskal_spanning_invariant f g h \ (\w . minimum_spanning_forest w g \ f \ w \ w\<^sup>T)" text \ We first show two verification conditions which are used in both correctness proofs. \ lemma kruskal_vc_1: assumes "symmetric g" shows "kruskal_spanning_invariant bot g g" proof (unfold kruskal_spanning_invariant_def, intro conjI) show "symmetric g" using assms by simp next show "g = g\<^sup>T" using assms by simp next show "g \ --g = g" using inf.sup_monoid.add_commute selection_closed_id by simp next show "spanning_forest bot (-g \ g)" using star.circ_transitive_equal spanning_forest_def by simp qed lemma kruskal_vc_2: assumes "kruskal_spanning_invariant f g h" and "h \ bot" shows "(minarc h \ -forest_components f \ kruskal_spanning_invariant ((f \ -(top * minarc h * f\<^sup>T\<^sup>\)) \ (f \ top * minarc h * f\<^sup>T\<^sup>\)\<^sup>T \ minarc h) g (h \ -minarc h \ -minarc h\<^sup>T) \ card { x . regular x \ x \ --h \ x \ -minarc h \ x \ -minarc h\<^sup>T } < card { x . regular x \ x \ --h }) \ (\ minarc h \ -forest_components f \ kruskal_spanning_invariant f g (h \ -minarc h \ -minarc h\<^sup>T) \ card { x . regular x \ x \ --h \ x \ -minarc h \ x \ -minarc h\<^sup>T } < card { x . regular x \ x \ --h })" proof - let ?e = "minarc h" let ?f = "(f \ -(top * ?e * f\<^sup>T\<^sup>\)) \ (f \ top * ?e * f\<^sup>T\<^sup>\)\<^sup>T \ ?e" let ?h = "h \ -?e \ -?e\<^sup>T" let ?F = "forest_components f" let ?n1 = "card { x . regular x \ x \ --h }" let ?n2 = "card { x . regular x \ x \ --h \ x \ -?e \ x \ -?e\<^sup>T }" have 1: "regular f \ regular ?e" by (metis assms(1) kruskal_spanning_invariant_def spanning_forest_def minarc_regular) hence 2: "regular ?f \ regular ?F \ regular (?e\<^sup>T)" using regular_closed_star regular_conv_closed regular_mult_closed by simp have 3: "\ ?e \ -?e" using assms(2) inf.orderE minarc_bot_iff by fastforce have 4: "?n2 < ?n1" apply (rule psubset_card_mono) using finite_regular apply simp using 1 3 kruskal_spanning_invariant_def minarc_below by auto show "(?e \ -?F \ kruskal_spanning_invariant ?f g ?h \ ?n2 < ?n1) \ (\ ?e \ -?F \ kruskal_spanning_invariant f g ?h \ ?n2 < ?n1)" proof (rule conjI) have 5: "injective ?f" apply (rule kruskal_injective_inv) using assms(1) kruskal_spanning_invariant_def spanning_forest_def apply simp apply (simp add: covector_mult_closed) apply (simp add: comp_associative comp_isotone star.right_plus_below_circ) apply (meson mult_left_isotone order_lesseq_imp star_outer_increasing top.extremum) using assms(1,2) kruskal_spanning_invariant_def kruskal_injective_inv_2 minarc_arc spanning_forest_def apply simp using assms(2) arc_injective minarc_arc apply blast using assms(1,2) kruskal_spanning_invariant_def kruskal_injective_inv_3 minarc_arc spanning_forest_def by simp show "?e \ -?F \ kruskal_spanning_invariant ?f g ?h \ ?n2 < ?n1" proof assume 6: "?e \ -?F" have 7: "equivalence ?F" using assms(1) kruskal_spanning_invariant_def forest_components_equivalence spanning_forest_def by simp have "?e\<^sup>T * top * ?e\<^sup>T = ?e\<^sup>T" using assms(2) by (simp add: arc_top_arc minarc_arc) hence "?e\<^sup>T * top * ?e\<^sup>T \ -?F" using 6 7 conv_complement conv_isotone by fastforce hence 8: "?e * ?F * ?e = bot" using le_bot triple_schroeder_p by simp show "kruskal_spanning_invariant ?f g ?h \ ?n2 < ?n1" proof (unfold kruskal_spanning_invariant_def, intro conjI) show "symmetric g" using assms(1) kruskal_spanning_invariant_def by simp next show "?h = ?h\<^sup>T" using assms(1) by (simp add: conv_complement conv_dist_inf inf_commute inf_left_commute kruskal_spanning_invariant_def) next show "g \ --?h = ?h" using 1 2 by (metis (hide_lams) assms(1) kruskal_spanning_invariant_def inf_assoc pp_dist_inf) next show "spanning_forest ?f (-?h \ g)" proof (unfold spanning_forest_def, intro conjI) show "injective ?f" using 5 by simp next show "acyclic ?f" apply (rule kruskal_acyclic_inv) using assms(1) kruskal_spanning_invariant_def spanning_forest_def apply simp apply (simp add: covector_mult_closed) using 8 assms(1) kruskal_spanning_invariant_def spanning_forest_def kruskal_acyclic_inv_1 apply simp using 8 apply (metis comp_associative mult_left_sub_dist_sup_left star.circ_loop_fixpoint sup_commute le_bot) using 6 by (simp add: p_antitone_iff) next show "?f \ --(-?h \ g)" apply (rule kruskal_subgraph_inv) using assms(1) kruskal_spanning_invariant_def spanning_forest_def apply simp using assms(1) apply (metis kruskal_spanning_invariant_def minarc_below order.trans pp_isotone_inf) using assms(1) kruskal_spanning_invariant_def apply simp using assms(1) kruskal_spanning_invariant_def by simp next show "components (-?h \ g) \ forest_components ?f" apply (rule kruskal_spanning_inv) using 5 apply simp using 1 regular_closed_star regular_conv_closed regular_mult_closed apply simp using 1 apply simp using assms(1) kruskal_spanning_invariant_def spanning_forest_def by simp next show "regular ?f" using 2 by simp qed next show "?n2 < ?n1" using 4 by simp qed qed next show "\ ?e \ -?F \ kruskal_spanning_invariant f g ?h \ ?n2 < ?n1" proof assume "\ ?e \ -?F" hence 9: "?e \ ?F" using 2 assms(2) arc_in_partition minarc_arc by fastforce show "kruskal_spanning_invariant f g ?h \ ?n2 < ?n1" proof (unfold kruskal_spanning_invariant_def, intro conjI) show "symmetric g" using assms(1) kruskal_spanning_invariant_def by simp next show "?h = ?h\<^sup>T" using assms(1) by (simp add: conv_complement conv_dist_inf inf_commute inf_left_commute kruskal_spanning_invariant_def) next show "g \ --?h = ?h" using 1 2 by (metis (hide_lams) assms(1) kruskal_spanning_invariant_def inf_assoc pp_dist_inf) next show "spanning_forest f (-?h \ g)" proof (unfold spanning_forest_def, intro conjI) show "injective f" using assms(1) kruskal_spanning_invariant_def spanning_forest_def by simp next show "acyclic f" using assms(1) kruskal_spanning_invariant_def spanning_forest_def by simp next have "f \ --(-h \ g)" using assms(1) kruskal_spanning_invariant_def spanning_forest_def by simp also have "... \ --(-?h \ g)" using comp_inf.mult_right_isotone inf.sup_monoid.add_commute inf_left_commute p_antitone_inf pp_isotone by presburger finally show "f \ --(-?h \ g)" by simp next show "components (-?h \ g) \ ?F" apply (rule kruskal_spanning_inv_1) using 9 apply simp using 1 apply simp using assms(1) kruskal_spanning_invariant_def spanning_forest_def apply simp using assms(1) kruskal_spanning_invariant_def forest_components_equivalence spanning_forest_def by simp next show "regular f" using 1 by simp qed next show "?n2 < ?n1" using 4 by simp qed qed qed qed text \ The following result shows that Kruskal's algorithm terminates and constructs a spanning tree. We cannot yet show that this is a minimum spanning tree. \ theorem kruskal_spanning: "VARS e f h [ symmetric g ] f := bot; h := g; WHILE h \ bot INV { kruskal_spanning_invariant f g h } VAR { card { x . regular x \ x \ --h } } DO e := minarc h; IF e \ -forest_components f THEN f := (f \ -(top * e * f\<^sup>T\<^sup>\)) \ (f \ top * e * f\<^sup>T\<^sup>\)\<^sup>T \ e ELSE SKIP FI; h := h \ -e \ -e\<^sup>T OD [ spanning_forest f g ]" apply vcg_tc_simp using kruskal_vc_1 apply simp using kruskal_vc_2 apply simp using kruskal_spanning_invariant_def by auto text \ Because we have shown total correctness, we conclude that a spanning tree exists. \ lemma kruskal_exists_spanning: "symmetric g \ \f . spanning_forest f g" using tc_extract_function kruskal_spanning by blast text \ This implies that a minimum spanning tree exists, which is used in the subsequent correctness proof. \ lemma kruskal_exists_minimal_spanning: assumes "symmetric g" shows "\f . minimum_spanning_forest f g" proof - let ?s = "{ f . spanning_forest f g }" have "\m\?s . \z\?s . sum (m \ g) \ sum (z \ g)" apply (rule finite_set_minimal) using finite_regular spanning_forest_def apply simp using assms kruskal_exists_spanning apply simp using sum_linear by simp thus ?thesis using minimum_spanning_forest_def by simp qed text \ Kruskal's minimum spanning tree algorithm terminates and is correct. This is the same algorithm that is used in the previous correctness proof, with the same precondition and variant, but with a different invariant and postcondition. \ theorem kruskal: "VARS e f h [ symmetric g ] f := bot; h := g; WHILE h \ bot INV { kruskal_invariant f g h } VAR { card { x . regular x \ x \ --h } } DO e := minarc h; IF e \ -forest_components f THEN f := (f \ -(top * e * f\<^sup>T\<^sup>\)) \ (f \ top * e * f\<^sup>T\<^sup>\)\<^sup>T \ e ELSE SKIP FI; h := h \ -e \ -e\<^sup>T OD [ minimum_spanning_forest f g ]" proof vcg_tc_simp assume "symmetric g" thus "kruskal_invariant bot g g" using kruskal_vc_1 kruskal_exists_minimal_spanning kruskal_invariant_def by simp next - fix f h n + fix f h let ?e = "minarc h" let ?f = "(f \ -(top * ?e * f\<^sup>T\<^sup>\)) \ (f \ top * ?e * f\<^sup>T\<^sup>\)\<^sup>T \ ?e" let ?h = "h \ -?e \ -?e\<^sup>T" let ?F = "forest_components f" let ?n1 = "card { x . regular x \ x \ --h }" let ?n2 = "card { x . regular x \ x \ --h \ x \ -?e \ x \ -?e\<^sup>T }" - assume 1: "kruskal_invariant f g h \ h \ bot \ ?n1 = n" + assume 1: "kruskal_invariant f g h \ h \ bot" from 1 obtain w where 2: "minimum_spanning_forest w g \ f \ w \ w\<^sup>T" using kruskal_invariant_def by auto hence 3: "regular f \ regular w \ regular ?e" using 1 by (metis kruskal_invariant_def kruskal_spanning_invariant_def minimum_spanning_forest_def spanning_forest_def minarc_regular) - have "(?e \ -?F \ kruskal_invariant ?f g ?h \ ?n2 < ?n1) \ (\ ?e \ -?F \ kruskal_invariant f g ?h \ ?n2 < ?n1)" + show "(?e \ -?F \ kruskal_invariant ?f g ?h \ ?n2 < ?n1) \ (\ ?e \ -?F \ kruskal_invariant f g ?h \ ?n2 < ?n1)" proof (rule conjI) show "?e \ -?F \ kruskal_invariant ?f g ?h \ ?n2 < ?n1" proof assume 4: "?e \ -?F" have 5: "equivalence ?F" using 1 kruskal_invariant_def kruskal_spanning_invariant_def forest_components_equivalence spanning_forest_def by simp have "?e\<^sup>T * top * ?e\<^sup>T = ?e\<^sup>T" using 1 by (simp add: arc_top_arc minarc_arc) hence "?e\<^sup>T * top * ?e\<^sup>T \ -?F" using 4 5 conv_complement conv_isotone by fastforce hence 6: "?e * ?F * ?e = bot" using le_bot triple_schroeder_p by simp show "kruskal_invariant ?f g ?h \ ?n2 < ?n1" proof (unfold kruskal_invariant_def, intro conjI) show "kruskal_spanning_invariant ?f g ?h" using 1 4 kruskal_vc_2 kruskal_invariant_def by simp next show "\w . minimum_spanning_forest w g \ ?f \ w \ w\<^sup>T" proof let ?p = "w \ top * ?e * w\<^sup>T\<^sup>\" let ?v = "(w \ -(top * ?e * w\<^sup>T\<^sup>\)) \ ?p\<^sup>T" have 7: "regular ?p" using 3 regular_closed_star regular_conv_closed regular_mult_closed by simp have 8: "injective ?v" apply (rule kruskal_exchange_injective_inv_1) using 2 minimum_spanning_forest_def spanning_forest_def apply simp apply (simp add: covector_mult_closed) apply (simp add: comp_associative comp_isotone star.right_plus_below_circ) using 1 2 kruskal_injective_inv_3 minarc_arc minimum_spanning_forest_def spanning_forest_def by simp have 9: "components g \ forest_components ?v" apply (rule kruskal_exchange_spanning_inv_1) using 8 apply simp using 7 apply simp using 2 minimum_spanning_forest_def spanning_forest_def by simp have 10: "spanning_forest ?v g" proof (unfold spanning_forest_def, intro conjI) show "injective ?v" using 8 by simp next show "acyclic ?v" apply (rule kruskal_exchange_acyclic_inv_1) using 2 minimum_spanning_forest_def spanning_forest_def apply simp by (simp add: covector_mult_closed) next show "?v \ --g" apply (rule sup_least) using 2 inf.coboundedI1 minimum_spanning_forest_def spanning_forest_def apply simp using 1 2 by (metis kruskal_invariant_def kruskal_spanning_invariant_def conv_complement conv_dist_inf order.trans inf.absorb2 inf.cobounded1 minimum_spanning_forest_def spanning_forest_def) next show "components g \ forest_components ?v" using 9 by simp next show "regular ?v" using 3 regular_closed_star regular_conv_closed regular_mult_closed by simp qed have 11: "sum (?v \ g) = sum (w \ g)" proof - have "sum (?v \ g) = sum (w \ -(top * ?e * w\<^sup>T\<^sup>\) \ g) + sum (?p\<^sup>T \ g)" using 2 by (metis conv_complement conv_top epm_8 inf_import_p inf_top_right regular_closed_top vector_top_closed minimum_spanning_forest_def spanning_forest_def sum_disjoint) also have "... = sum (w \ -(top * ?e * w\<^sup>T\<^sup>\) \ g) + sum (?p \ g)" using 1 kruskal_invariant_def kruskal_spanning_invariant_def sum_symmetric by simp also have "... = sum (((w \ -(top * ?e * w\<^sup>T\<^sup>\)) \ ?p) \ g)" using inf_commute inf_left_commute sum_disjoint by simp also have "... = sum (w \ g)" using 3 7 maddux_3_11_pp by simp finally show ?thesis by simp qed have 12: "?v \ ?v\<^sup>T = w \ w\<^sup>T" proof - have "?v \ ?v\<^sup>T = (w \ -?p) \ ?p\<^sup>T \ (w\<^sup>T \ -?p\<^sup>T) \ ?p" 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 simp finally show ?thesis by simp qed have 13: "?v * ?e\<^sup>T = bot" apply (rule kruskal_reroot_edge) using 1 apply (simp add: minarc_arc) using 2 minimum_spanning_forest_def spanning_forest_def by simp have "?v \ ?e \ ?v \ top * ?e" using inf.sup_right_isotone top_left_mult_increasing by simp also have "... \ ?v * (top * ?e)\<^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 ?d = "?v \ top * ?e\<^sup>T * ?v\<^sup>T\<^sup>\ \ ?F * ?e\<^sup>T * top \ top * ?e * -?F" let ?w = "(?v \ -?d) \ ?e" have 15: "regular ?d" using 3 regular_closed_star regular_conv_closed regular_mult_closed by simp have 16: "?F \ -?d" apply (rule kruskal_edge_between_components_1) using 5 apply simp using 1 conv_dist_comp minarc_arc mult_assoc by simp have 17: "f \ f\<^sup>T \ (?v \ -?d \ -?d\<^sup>T) \ (?v\<^sup>T \ -?d \ -?d\<^sup>T)" apply (rule kruskal_edge_between_components_2) using 16 apply simp using 1 kruskal_invariant_def kruskal_spanning_invariant_def spanning_forest_def apply simp using 2 12 by (metis conv_dist_sup conv_involutive conv_isotone le_supI sup_commute) show "minimum_spanning_forest ?w g \ ?f \ ?w \ ?w\<^sup>T" proof (intro conjI) have 18: "?e\<^sup>T \ ?v\<^sup>\" apply (rule kruskal_edge_arc_1[where g=g and h=h]) using minarc_below apply simp using 1 apply (metis kruskal_invariant_def kruskal_spanning_invariant_def inf_le1) using 1 kruskal_invariant_def kruskal_spanning_invariant_def apply simp using 9 apply simp using 13 by simp have 19: "arc ?d" apply (rule kruskal_edge_arc) using 5 apply simp using 10 spanning_forest_def apply blast using 1 apply (simp add: minarc_arc) using 3 apply (metis conv_complement pp_dist_star regular_mult_closed) using 2 8 12 apply (simp add: kruskal_forest_components_inf) using 10 spanning_forest_def apply simp using 13 apply simp using 6 apply simp using 18 by simp show "minimum_spanning_forest ?w g" proof (unfold minimum_spanning_forest_def, intro conjI) have "(?v \ -?d) * ?e\<^sup>T \ ?v * ?e\<^sup>T" using inf_le1 mult_left_isotone by simp hence "(?v \ -?d) * ?e\<^sup>T = bot" using 13 le_bot by simp hence 20: "?e * (?v \ -?d)\<^sup>T = bot" using conv_dist_comp conv_involutive conv_bot by force have 21: "injective ?w" apply (rule injective_sup) using 8 apply (simp add: injective_inf_closed) using 20 apply simp using 1 arc_injective minarc_arc by blast show "spanning_forest ?w g" proof (unfold spanning_forest_def, intro conjI) show "injective ?w" using 21 by simp next show "acyclic ?w" apply (rule kruskal_exchange_acyclic_inv_2) using 10 spanning_forest_def apply blast using 8 apply simp using inf.coboundedI1 apply simp using 19 apply simp using 1 apply (simp add: minarc_arc) using inf.cobounded2 inf.coboundedI1 apply simp using 13 by simp next have "?w \ ?v \ ?e" using inf_le1 sup_left_isotone by simp also have "... \ --g \ ?e" using 10 sup_left_isotone spanning_forest_def by blast also have "... \ --g \ --h" by (simp add: le_supI2 minarc_below) also have "... = --g" using 1 by (metis kruskal_invariant_def kruskal_spanning_invariant_def pp_isotone_inf sup.orderE) finally show "?w \ --g" by simp next have 22: "?d \ (?v \ -?d)\<^sup>T\<^sup>\ * ?e\<^sup>T * top" apply (rule kruskal_exchange_spanning_inv_2) using 8 apply simp using 13 apply (metis semiring.mult_not_zero star_absorb star_simulation_right_equal) using 17 apply simp by (simp add: inf.coboundedI1) have "components g \ forest_components ?v" using 10 spanning_forest_def by auto also have "... \ forest_components ?w" apply (rule kruskal_exchange_forest_components_inv) using 21 apply simp using 15 apply simp using 1 apply (simp add: arc_top_arc minarc_arc) apply (simp add: inf.coboundedI1) using 13 apply simp using 8 apply simp apply (simp add: le_infI1) using 22 by simp finally show "components g \ forest_components ?w" by simp next show "regular ?w" using 3 7 regular_conv_closed by simp qed next have 23: "?e \ g \ bot" using 1 by (metis kruskal_invariant_def kruskal_spanning_invariant_def comp_inf.semiring.mult_zero_right inf.sup_monoid.add_assoc inf.sup_monoid.add_commute minarc_bot_iff minarc_meet_bot) have "g \ -h \ (g \ -h)\<^sup>\" using star.circ_increasing by simp also have "... \ (--(g \ -h))\<^sup>\" using pp_increasing star_isotone by blast also have "... \ ?F" using 1 kruskal_invariant_def kruskal_spanning_invariant_def inf.sup_monoid.add_commute spanning_forest_def by simp finally have 24: "g \ -h \ ?F" by simp have "?d \ --g" using 10 inf.coboundedI1 spanning_forest_def by blast hence "?d \ --g \ -?F" using 16 inf.boundedI p_antitone_iff by simp also have "... = --(g \ -?F)" by simp also have "... \ --h" using 24 p_shunting_swap pp_isotone by fastforce finally have 25: "?d \ --h" by simp have "?d = bot \ top = bot" using 19 by (metis mult_left_zero mult_right_zero) hence "?d \ bot" using 1 le_bot by auto hence 26: "?d \ h \ bot" using 25 by (metis inf.absorb_iff2 inf_commute pseudo_complement) have "sum (?e \ g) = sum (?e \ --h \ g)" by (simp add: inf.absorb1 minarc_below) also have "... = sum (?e \ h)" using 1 by (metis kruskal_invariant_def kruskal_spanning_invariant_def inf.left_commute inf.sup_monoid.add_commute) also have "... \ sum (?d \ h)" using 19 26 minarc_min by simp also have "... = sum (?d \ (--h \ g))" using 1 kruskal_invariant_def kruskal_spanning_invariant_def inf_commute by simp also have "... = sum (?d \ g)" using 25 by (simp add: inf.absorb2 inf_assoc inf_commute) finally have 27: "sum (?e \ g) \ sum (?d \ g)" by simp have "?v \ ?e \ -?d = bot" using 14 by simp hence "sum (?w \ g) = sum (?v \ -?d \ g) + sum (?e \ g)" using sum_disjoint inf_commute inf_assoc by simp also have "... \ sum (?v \ -?d \ g) + sum (?d \ g)" using 23 27 sum_plus_right_isotone by simp also have "... = sum (((?v \ -?d) \ ?d) \ g)" using sum_disjoint inf_le2 pseudo_complement by simp also have "... = sum ((?v \ ?d) \ (-?d \ ?d) \ g)" by (simp add: sup_inf_distrib2) also have "... = sum ((?v \ ?d) \ g)" using 15 by (metis inf_top_right stone) also have "... = sum (?v \ g)" by (simp add: inf.sup_monoid.add_assoc) finally have "sum (?w \ g) \ sum (?v \ g)" by simp thus "\u . spanning_forest u g \ sum (?w \ g) \ sum (u \ g)" using 2 11 minimum_spanning_forest_def by auto qed next have "?f \ f \ f\<^sup>T \ ?e" using conv_dist_inf inf_le1 sup_left_isotone sup_mono by presburger also have "... \ (?v \ -?d \ -?d\<^sup>T) \ (?v\<^sup>T \ -?d \ -?d\<^sup>T) \ ?e" using 17 sup_left_isotone by simp also have "... \ (?v \ -?d) \ (?v\<^sup>T \ -?d \ -?d\<^sup>T) \ ?e" using inf.cobounded1 sup_inf_distrib2 by presburger also have "... = ?w \ (?v\<^sup>T \ -?d \ -?d\<^sup>T)" by (simp add: sup_assoc sup_commute) also have "... \ ?w \ (?v\<^sup>T \ -?d\<^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 qed next show "?n2 < ?n1" using 1 kruskal_vc_2 kruskal_invariant_def by auto qed qed next show "\ ?e \ -?F \ kruskal_invariant f g ?h \ ?n2 < ?n1" using 1 kruskal_vc_2 kruskal_invariant_def by auto qed - thus "(?e \ -?F \ kruskal_invariant ?f g ?h \ ?n2 < n) \ (\ ?e \ -?F \ kruskal_invariant f g ?h \ ?n2 < n)" - using 1 by blast next - fix f h - assume 28: "kruskal_invariant f g h \ h = bot" + fix f + assume 28: "kruskal_invariant f g bot" hence 29: "spanning_forest f g" using kruskal_invariant_def kruskal_spanning_invariant_def by auto from 28 obtain w where 30: "minimum_spanning_forest w g \ f \ w \ w\<^sup>T" using kruskal_invariant_def by auto hence "w = w \ --g" by (simp add: inf.absorb1 minimum_spanning_forest_def spanning_forest_def) also have "... \ w \ components g" by (metis inf.sup_right_isotone star.circ_increasing) also have "... \ w \ f\<^sup>T\<^sup>\ * f\<^sup>\" using 29 spanning_forest_def inf.sup_right_isotone by simp also have "... \ f \ f\<^sup>T" apply (rule cancel_separate_6[where z=w and y="w\<^sup>T"]) using 30 minimum_spanning_forest_def spanning_forest_def apply simp using 30 apply (metis conv_dist_inf conv_dist_sup conv_involutive inf.cobounded2 inf.orderE) using 30 apply (simp add: sup_commute) using 30 minimum_spanning_forest_def spanning_forest_def apply simp using 30 by (metis acyclic_star_below_complement comp_inf.mult_right_isotone inf_p le_bot minimum_spanning_forest_def spanning_forest_def) finally have 31: "w \ f \ f\<^sup>T" by simp have "sum (f \ g) = sum ((w \ w\<^sup>T) \ (f \ g))" using 30 by (metis inf_absorb2 inf.assoc) also have "... = sum (w \ (f \ g)) + sum (w\<^sup>T \ (f \ g))" using 30 inf.commute acyclic_asymmetric sum_disjoint minimum_spanning_forest_def spanning_forest_def by simp also have "... = sum (w \ (f \ g)) + sum (w \ (f\<^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))" using 28 inf.commute inf.assoc kruskal_invariant_def kruskal_spanning_invariant_def by simp also have "... = sum ((f \ f\<^sup>T) \ (w \ g))" using 29 acyclic_asymmetric inf.sup_monoid.add_commute sum_disjoint spanning_forest_def by simp also have "... = sum (w \ g)" using 31 by (metis inf_absorb2 inf.assoc) finally show "minimum_spanning_forest f g" using 29 30 minimum_spanning_forest_def by simp qed end end diff --git a/thys/Relational_Minimum_Spanning_Trees/Prim.thy b/thys/Relational_Minimum_Spanning_Trees/Prim.thy --- a/thys/Relational_Minimum_Spanning_Trees/Prim.thy +++ b/thys/Relational_Minimum_Spanning_Trees/Prim.thy @@ -1,479 +1,477 @@ (* Title: Prim's Minimum Spanning Tree Algorithm Author: Walter Guttmann Maintainer: Walter Guttmann *) section \Prim's Minimum Spanning Tree Algorithm\ text \ In this theory we prove total correctness of Prim's minimum spanning tree algorithm. The proof has the same overall structure as the total-correctness proof of Kruskal's algorithm \cite{Guttmann2018c}. The partial-correctness proof of Prim's algorithm is discussed in \cite{Guttmann2016c,Guttmann2018b}. \ theory Prim imports Aggregation_Algebras.Hoare_Logic Aggregation_Algebras.Aggregation_Algebras begin context m_kleene_algebra begin abbreviation "component g r \ r\<^sup>T * (--g)\<^sup>\" definition "spanning_tree t g r \ forest t \ t \ (component g r)\<^sup>T * (component g r) \ --g \ component g r \ r\<^sup>T * t\<^sup>\ \ regular t" definition "minimum_spanning_tree t g r \ spanning_tree t g r \ (\u . spanning_tree u g r \ sum (t \ g) \ sum (u \ g))" definition "prim_precondition g r \ g = g\<^sup>T \ injective r \ vector r \ regular r" definition "prim_spanning_invariant t v g r \ prim_precondition g r \ v\<^sup>T = r\<^sup>T * t\<^sup>\ \ spanning_tree t (v * v\<^sup>T \ g) r" definition "prim_invariant t v g r \ prim_spanning_invariant t v g r \ (\w . minimum_spanning_tree w g r \ t \ w)" lemma span_tree_split: assumes "vector r" shows "t \ (component g r)\<^sup>T * (component g r) \ --g \ (t \ (component g r)\<^sup>T \ t \ component g r \ t \ --g)" proof - have "(component g r)\<^sup>T * (component g r) = (component g r)\<^sup>T \ component g r" by (metis assms conv_involutive covector_mult_closed vector_conv_covector vector_covector) thus ?thesis by simp qed lemma span_tree_component: assumes "spanning_tree t g r" shows "component g r = component t r" using assms by (simp add: antisym mult_right_isotone star_isotone spanning_tree_def) text \ We first show three verification conditions which are used in both correctness proofs. \ lemma prim_vc_1: assumes "prim_precondition g r" shows "prim_spanning_invariant bot r g r" proof (unfold prim_spanning_invariant_def, intro conjI) show "prim_precondition g r" using assms by simp next show "r\<^sup>T = r\<^sup>T * bot\<^sup>\" by (simp add: star_absorb) next let ?ss = "r * r\<^sup>T \ g" show "spanning_tree bot ?ss r" proof (unfold spanning_tree_def, intro conjI) show "injective bot" by simp next show "acyclic bot" by simp next show "bot \ (component ?ss r)\<^sup>T * (component ?ss r) \ --?ss" by simp next have "component ?ss r \ component (r * r\<^sup>T) r" by (simp add: mult_right_isotone star_isotone) also have "... \ r\<^sup>T * 1\<^sup>\" using assms by (metis inf.eq_iff p_antitone regular_one_closed star_sub_one prim_precondition_def) also have "... = r\<^sup>T * bot\<^sup>\" by (simp add: star.circ_zero star_one) finally show "component ?ss r \ r\<^sup>T * bot\<^sup>\" . next show "regular bot" by simp qed qed lemma prim_vc_2: assumes "prim_spanning_invariant t v g r" and "v * -v\<^sup>T \ g \ bot" shows "prim_spanning_invariant (t \ minarc (v * -v\<^sup>T \ g)) (v \ minarc (v * -v\<^sup>T \ g)\<^sup>T * top) g r \ card { x . regular x \ x \ component g r \ x \ -(v \ minarc (v * -v\<^sup>T \ g)\<^sup>T * top)\<^sup>T } < card { x . regular x \ x \ component g r \ x \ -v\<^sup>T }" proof - let ?vcv = "v * -v\<^sup>T \ g" let ?e = "minarc ?vcv" let ?t = "t \ ?e" let ?v = "v \ ?e\<^sup>T * top" let ?c = "component g r" let ?g = "--g" let ?n1 = "card { x . regular x \ x \ ?c \ x \ -v\<^sup>T }" let ?n2 = "card { x . regular x \ x \ ?c \ x \ -?v\<^sup>T }" have 1: "regular v \ regular (v * v\<^sup>T) \ regular (?v * ?v\<^sup>T) \ regular (top * ?e)" using assms(1) by (metis prim_spanning_invariant_def spanning_tree_def prim_precondition_def regular_conv_closed regular_closed_star regular_mult_closed conv_involutive regular_closed_top regular_closed_sup minarc_regular) hence 2: "t \ v * v\<^sup>T \ ?g" using assms(1) by (metis prim_spanning_invariant_def spanning_tree_def inf_pp_commute inf.boundedE) hence 3: "t \ v * v\<^sup>T" by simp have 4: "t \ ?g" using 2 by simp have 5: "?e \ v * -v\<^sup>T \ ?g" using 1 by (metis minarc_below pp_dist_inf regular_mult_closed regular_closed_p) hence 6: "?e \ v * -v\<^sup>T" by simp have 7: "vector v" using assms(1) prim_spanning_invariant_def prim_precondition_def by (simp add: covector_mult_closed vector_conv_covector) hence 8: "?e \ v" using 6 by (metis conv_complement inf.boundedE vector_complement_closed vector_covector) have 9: "?e * t = bot" using 3 6 7 et(1) by blast have 10: "?e * t\<^sup>T = bot" using 3 6 7 et(2) by simp have 11: "arc ?e" using assms(2) minarc_arc by simp have "r\<^sup>T \ r\<^sup>T * t\<^sup>\" by (metis mult_right_isotone order_refl semiring.mult_not_zero star.circ_separate_mult_1 star_absorb) hence 12: "r\<^sup>T \ v\<^sup>T" using assms(1) by (simp add: prim_spanning_invariant_def) have 13: "vector r \ injective r \ v\<^sup>T = r\<^sup>T * t\<^sup>\" using assms(1) prim_spanning_invariant_def prim_precondition_def minimum_spanning_tree_def spanning_tree_def reachable_restrict by simp have "g = g\<^sup>T" using assms(1) prim_invariant_def prim_spanning_invariant_def prim_precondition_def by simp hence 14: "?g\<^sup>T = ?g" using conv_complement by simp show "prim_spanning_invariant ?t ?v g r \ ?n2 < ?n1" proof (rule conjI) show "prim_spanning_invariant ?t ?v g r" proof (unfold prim_spanning_invariant_def, intro conjI) show "prim_precondition g r" using assms(1) prim_spanning_invariant_def by simp next show "?v\<^sup>T = r\<^sup>T * ?t\<^sup>\" using assms(1) 6 7 9 by (simp add: reachable_inv prim_spanning_invariant_def prim_precondition_def spanning_tree_def) next let ?G = "?v * ?v\<^sup>T \ g" show "spanning_tree ?t ?G r" proof (unfold spanning_tree_def, intro conjI) show "injective ?t" using assms(1) 10 11 by (simp add: injective_inv prim_spanning_invariant_def spanning_tree_def) next show "acyclic ?t" using assms(1) 3 6 7 acyclic_inv prim_spanning_invariant_def spanning_tree_def by simp next show "?t \ (component ?G r)\<^sup>T * (component ?G r) \ --?G" using 1 2 5 7 13 prim_subgraph_inv inf_pp_commute mst_subgraph_inv_2 by auto next show "component (?v * ?v\<^sup>T \ g) r \ r\<^sup>T * ?t\<^sup>\" proof - have 15: "r\<^sup>T * (v * v\<^sup>T \ ?g)\<^sup>\ \ r\<^sup>T * t\<^sup>\" using assms(1) 1 by (metis prim_spanning_invariant_def spanning_tree_def inf_pp_commute) have "component (?v * ?v\<^sup>T \ g) r = r\<^sup>T * (?v * ?v\<^sup>T \ ?g)\<^sup>\" using 1 by simp also have "... \ r\<^sup>T * ?t\<^sup>\" using 2 6 7 11 12 13 14 15 by (metis span_inv) finally show ?thesis . qed next show "regular ?t" using assms(1) by (metis prim_spanning_invariant_def spanning_tree_def regular_closed_sup minarc_regular) qed qed next have 16: "top * ?e \ ?c" proof - have "top * ?e = top * ?e\<^sup>T * ?e" using 11 by (metis arc_top_edge mult_assoc) also have "... \ v\<^sup>T * ?e" using 7 8 by (metis conv_dist_comp conv_isotone mult_left_isotone symmetric_top_closed) also have "... \ v\<^sup>T * ?g" using 5 mult_right_isotone by auto also have "... = r\<^sup>T * t\<^sup>\ * ?g" using 13 by simp also have "... \ r\<^sup>T * ?g\<^sup>\ * ?g" using 4 by (simp add: mult_left_isotone mult_right_isotone star_isotone) also have "... \ ?c" by (simp add: comp_associative mult_right_isotone star.right_plus_below_circ) finally show ?thesis by simp qed have 17: "top * ?e \ -v\<^sup>T" using 6 7 by (simp add: schroeder_4_p vTeT) have 18: "\ top * ?e \ -(top * ?e)" by (metis assms(2) inf.orderE minarc_bot_iff conv_complement_sub_inf inf_p inf_top.left_neutral p_bot symmetric_top_closed vector_top_closed) have 19: "-?v\<^sup>T = -v\<^sup>T \ -(top * ?e)" by (simp add: conv_dist_comp conv_dist_sup) hence 20: "\ top * ?e \ -?v\<^sup>T" using 18 by simp show "?n2 < ?n1" apply (rule psubset_card_mono) using finite_regular apply simp using 1 16 17 19 20 by auto qed qed lemma prim_vc_3: assumes "prim_spanning_invariant t v g r" and "v * -v\<^sup>T \ g = bot" shows "spanning_tree t g r" proof - let ?g = "--g" have 1: "regular v \ regular (v * v\<^sup>T)" using assms(1) by (metis prim_spanning_invariant_def spanning_tree_def prim_precondition_def regular_conv_closed regular_closed_star regular_mult_closed conv_involutive) have 2: "v * -v\<^sup>T \ ?g = bot" using assms(2) pp_inf_bot_iff pp_pp_inf_bot_iff by simp have 3: "v\<^sup>T = r\<^sup>T * t\<^sup>\ \ vector v" using assms(1) by (simp add: covector_mult_closed prim_invariant_def prim_spanning_invariant_def vector_conv_covector prim_precondition_def) have 4: "t \ v * v\<^sup>T \ ?g" using assms(1) 1 by (metis prim_spanning_invariant_def inf_pp_commute spanning_tree_def inf.boundedE) have "r\<^sup>T * (v * v\<^sup>T \ ?g)\<^sup>\ \ r\<^sup>T * t\<^sup>\" using assms(1) 1 by (metis prim_spanning_invariant_def inf_pp_commute spanning_tree_def) hence 5: "component g r = v\<^sup>T" using 1 2 3 4 by (metis span_post) have "regular (v * v\<^sup>T)" using assms(1) by (metis prim_spanning_invariant_def spanning_tree_def prim_precondition_def regular_conv_closed regular_closed_star regular_mult_closed conv_involutive) hence 6: "t \ v * v\<^sup>T \ ?g" by (metis assms(1) prim_spanning_invariant_def spanning_tree_def inf_pp_commute inf.boundedE) show "spanning_tree t g r" apply (unfold spanning_tree_def, intro conjI) using assms(1) prim_spanning_invariant_def spanning_tree_def apply simp using assms(1) prim_spanning_invariant_def spanning_tree_def apply simp using 5 6 apply simp using assms(1) 5 prim_spanning_invariant_def apply simp using assms(1) prim_spanning_invariant_def spanning_tree_def by simp qed text \ The following result shows that Prim's algorithm terminates and constructs a spanning tree. We cannot yet show that this is a minimum spanning tree. \ theorem prim_spanning: "VARS t v e [ prim_precondition g r ] t := bot; v := r; WHILE v * -v\<^sup>T \ g \ bot INV { prim_spanning_invariant t v g r } VAR { card { x . regular x \ x \ component g r \ -v\<^sup>T } } DO e := minarc (v * -v\<^sup>T \ g); t := t \ e; v := v \ e\<^sup>T * top OD [ spanning_tree t g r ]" apply vcg_tc_simp apply (simp add: prim_vc_1) using prim_vc_2 apply blast using prim_vc_3 by auto text \ Because we have shown total correctness, we conclude that a spanning tree exists. \ lemma prim_exists_spanning: "prim_precondition g r \ \t . spanning_tree t g r" using tc_extract_function prim_spanning by blast text \ This implies that a minimum spanning tree exists, which is used in the subsequent correctness proof. \ lemma prim_exists_minimal_spanning: assumes "prim_precondition g r" shows "\t . minimum_spanning_tree t g r" proof - let ?s = "{ t . spanning_tree t g r }" have "\m\?s . \z\?s . sum (m \ g) \ sum (z \ g)" apply (rule finite_set_minimal) using finite_regular spanning_tree_def apply simp using assms prim_exists_spanning apply simp using sum_linear by simp thus ?thesis using minimum_spanning_tree_def by simp qed text \ Prim's minimum spanning tree algorithm terminates and is correct. This is the same algorithm that is used in the previous correctness proof, with the same precondition and variant, but with a different invariant and postcondition. \ theorem prim: "VARS t v e [ prim_precondition g r \ (\w . minimum_spanning_tree w g r) ] t := bot; v := r; WHILE v * -v\<^sup>T \ g \ bot INV { prim_invariant t v g r } VAR { card { x . regular x \ x \ component g r \ -v\<^sup>T } } DO e := minarc (v * -v\<^sup>T \ g); t := t \ e; v := v \ e\<^sup>T * top OD [ minimum_spanning_tree t g r ]" proof vcg_tc_simp assume "prim_precondition g r \ (\w . minimum_spanning_tree w g r)" thus "prim_invariant bot r g r" using prim_invariant_def prim_vc_1 by simp next - fix t v n + fix t v let ?vcv = "v * -v\<^sup>T \ g" let ?vv = "v * v\<^sup>T \ g" let ?e = "minarc ?vcv" let ?t = "t \ ?e" let ?v = "v \ ?e\<^sup>T * top" let ?c = "component g r" let ?g = "--g" let ?n1 = "card { x . regular x \ x \ ?c \ x \ -v\<^sup>T }" let ?n2 = "card { x . regular x \ x \ ?c \ x \ -?v\<^sup>T }" - assume 1: "prim_invariant t v g r \ ?vcv \ bot \ ?n1 = n" + assume 1: "prim_invariant t v g r \ ?vcv \ bot" hence 2: "regular v \ regular (v * v\<^sup>T)" by (metis (no_types, hide_lams) prim_invariant_def prim_spanning_invariant_def spanning_tree_def prim_precondition_def regular_conv_closed regular_closed_star regular_mult_closed conv_involutive) have 3: "t \ v * v\<^sup>T \ ?g" using 1 2 by (metis (no_types, hide_lams) prim_invariant_def prim_spanning_invariant_def spanning_tree_def inf_pp_commute inf.boundedE) hence 4: "t \ v * v\<^sup>T" by simp have 5: "t \ ?g" using 3 by simp have 6: "?e \ v * -v\<^sup>T \ ?g" using 2 by (metis minarc_below pp_dist_inf regular_mult_closed regular_closed_p) hence 7: "?e \ v * -v\<^sup>T" by simp have 8: "vector v" using 1 prim_invariant_def prim_spanning_invariant_def prim_precondition_def by (simp add: covector_mult_closed vector_conv_covector) have 9: "arc ?e" using 1 minarc_arc by simp from 1 obtain w where 10: "minimum_spanning_tree w g r \ t \ w" by (metis prim_invariant_def) hence 11: "vector r \ injective r \ v\<^sup>T = r\<^sup>T * t\<^sup>\ \ forest w \ t \ w \ w \ ?c\<^sup>T * ?c \ ?g \ r\<^sup>T * (?c\<^sup>T * ?c \ ?g)\<^sup>\ \ r\<^sup>T * w\<^sup>\" using 1 2 prim_invariant_def prim_spanning_invariant_def prim_precondition_def minimum_spanning_tree_def spanning_tree_def reachable_restrict by simp hence 12: "w * v \ v" using predecessors_reachable reachable_restrict by auto have 13: "g = g\<^sup>T" using 1 prim_invariant_def prim_spanning_invariant_def prim_precondition_def by simp hence 14: "?g\<^sup>T = ?g" using conv_complement by simp - have "prim_invariant ?t ?v g r \ ?n2 < ?n1" + show "prim_invariant ?t ?v g r \ ?n2 < ?n1" proof (unfold prim_invariant_def, intro conjI) show "prim_spanning_invariant ?t ?v g r" using 1 prim_invariant_def prim_vc_2 by blast next show "\w . minimum_spanning_tree w g r \ ?t \ w" proof let ?f = "w \ v * -v\<^sup>T \ top * ?e * w\<^sup>T\<^sup>\" let ?p = "w \ -v * -v\<^sup>T \ top * ?e * w\<^sup>T\<^sup>\" let ?fp = "w \ -v\<^sup>T \ top * ?e * w\<^sup>T\<^sup>\" let ?w = "(w \ -?fp) \ ?p\<^sup>T \ ?e" have 15: "regular ?f \ regular ?fp \ regular ?w" using 2 10 by (metis regular_conv_closed regular_closed_star regular_mult_closed regular_closed_top regular_closed_inf regular_closed_sup minarc_regular minimum_spanning_tree_def spanning_tree_def) show "minimum_spanning_tree ?w g r \ ?t \ ?w" proof (intro conjI) show "minimum_spanning_tree ?w g r" proof (unfold minimum_spanning_tree_def, intro conjI) show "spanning_tree ?w g r" proof (unfold spanning_tree_def, intro conjI) show "injective ?w" using 7 8 9 11 exchange_injective by blast next show "acyclic ?w" using 7 8 11 12 exchange_acyclic by blast next show "?w \ ?c\<^sup>T * ?c \ --g" proof - have 16: "w \ -?fp \ ?c\<^sup>T * ?c \ --g" using 10 by (simp add: le_infI1 minimum_spanning_tree_def spanning_tree_def) have "?p\<^sup>T \ w\<^sup>T" by (simp add: conv_isotone inf.sup_monoid.add_assoc) also have "... \ (?c\<^sup>T * ?c \ --g)\<^sup>T" using 11 conv_order by simp also have "... = ?c\<^sup>T * ?c \ --g" using 2 14 conv_dist_comp conv_dist_inf by simp finally have 17: "?p\<^sup>T \ ?c\<^sup>T * ?c \ --g" . have "?e \ ?c\<^sup>T * ?c \ ?g" using 5 6 11 mst_subgraph_inv by auto thus ?thesis using 16 17 by simp qed next show "?c \ r\<^sup>T * ?w\<^sup>\" proof - have "?c \ r\<^sup>T * w\<^sup>\" using 10 minimum_spanning_tree_def spanning_tree_def by simp also have "... \ r\<^sup>T * ?w\<^sup>\" using 4 7 8 10 11 12 15 by (metis mst_reachable_inv) finally show ?thesis . qed next show "regular ?w" using 15 by simp qed next have 18: "?f \ ?p = ?fp" using 2 8 epm_1 by fastforce have "arc (w \ --v * -v\<^sup>T \ top * ?e * w\<^sup>T\<^sup>\)" using 5 6 8 9 11 12 reachable_restrict arc_edge by auto hence 19: "arc ?f" using 2 by simp hence "?f = bot \ top = bot" by (metis mult_left_zero mult_right_zero) hence "?f \ bot" using 1 le_bot by auto hence "?f \ v * -v\<^sup>T \ ?g \ bot" using 2 11 by (simp add: inf.absorb1 le_infI1) hence "g \ (?f \ v * -v\<^sup>T) \ bot" using inf_commute pp_inf_bot_iff by simp hence 20: "?f \ ?vcv \ bot" by (simp add: inf_assoc inf_commute) hence 21: "?f \ g = ?f \ ?vcv" using 2 by (simp add: inf_assoc inf_commute inf_left_commute) have 22: "?e \ g = minarc ?vcv \ ?vcv" using 7 by (simp add: inf.absorb2 inf.assoc inf.commute) hence 23: "sum (?e \ g) \ sum (?f \ g)" using 15 19 20 21 by (simp add: minarc_min) have "?e \ bot" using 20 comp_inf.semiring.mult_not_zero semiring.mult_not_zero by blast hence 24: "?e \ g \ bot" using 22 minarc_meet_bot by auto have "sum (?w \ g) = sum (w \ -?fp \ g) + sum (?p\<^sup>T \ g) + sum (?e \ g)" using 7 8 10 by (metis sum_disjoint_3 epm_8 epm_9 epm_10 minimum_spanning_tree_def spanning_tree_def) also have "... = sum (((w \ -?fp) \ ?p\<^sup>T) \ g) + sum (?e \ g)" using 11 by (metis epm_8 sum_disjoint) also have "... \ sum (((w \ -?fp) \ ?p\<^sup>T) \ g) + sum (?f \ g)" using 23 24 by (simp add: sum_plus_right_isotone) also have "... = sum (w \ -?fp \ g) + sum (?p\<^sup>T \ g) + sum (?f \ g)" using 11 by (metis epm_8 sum_disjoint) also have "... = sum (w \ -?fp \ g) + sum (?p \ g) + sum (?f \ g)" using 13 sum_symmetric by auto also have "... = sum (((w \ -?fp) \ ?p \ ?f) \ g)" using 2 8 by (metis sum_disjoint_3 epm_11 epm_12 epm_13) also have "... = sum (w \ g)" using 2 8 15 18 epm_2 by force finally have "sum (?w \ g) \ sum (w \ g)" . thus "\u . spanning_tree u g r \ sum (?w \ g) \ sum (u \ g)" using 10 order_lesseq_imp minimum_spanning_tree_def by auto qed next show "?t \ ?w" using 4 8 10 mst_extends_new_tree by simp qed qed next show "?n2 < ?n1" using 1 prim_invariant_def prim_vc_2 by auto qed - thus "prim_invariant ?t ?v g r \ ?n2 < n" - using 1 by blast next fix t v let ?g = "--g" assume 25: "prim_invariant t v g r \ v * -v\<^sup>T \ g = bot" hence 26: "regular v" by (metis prim_invariant_def prim_spanning_invariant_def spanning_tree_def prim_precondition_def regular_conv_closed regular_closed_star regular_mult_closed conv_involutive) from 25 obtain w where 27: "minimum_spanning_tree w g r \ t \ w" by (metis prim_invariant_def) have "spanning_tree t g r" using 25 prim_invariant_def prim_vc_3 by blast hence "component g r = v\<^sup>T" by (metis 25 prim_invariant_def span_tree_component prim_spanning_invariant_def spanning_tree_def) hence 28: "w \ v * v\<^sup>T" using 26 27 by (simp add: minimum_spanning_tree_def spanning_tree_def inf_pp_commute) have "vector r \ injective r \ forest w" using 25 27 by (simp add: prim_invariant_def prim_spanning_invariant_def prim_precondition_def minimum_spanning_tree_def spanning_tree_def) hence "w = t" using 25 27 28 prim_invariant_def prim_spanning_invariant_def mst_post by blast thus "minimum_spanning_tree t g r" using 27 by simp qed end end