(* Title: Disjoint-Set Forests Author: Walter Guttmann Maintainer: Walter Guttmann <walter.guttmann at canterbury.ac.nz> *) theory Disjoint_Set_Forests imports "HOL-Hoare.Hoare_Logic" Stone_Kleene_Relation_Algebras.Kleene_Relation_Algebras begin no_notation minus (infixl "-" 65) and trancl ("(_⇧^{+})" [1000] 999) context p_algebra begin abbreviation minus :: "'a ⇒ 'a ⇒ 'a" (infixl "-" 65) where "x - y ≡ x ⊓ -y" end text ‹ An arc in a Stone relation algebra corresponds to an atom in a relation algebra and represents a single edge in a graph. A point represents a set of nodes. A rectangle represents the Cartesian product of two sets of nodes \<^cite>‹"BerghammerStruth2010"›. › context times_top begin abbreviation rectangle :: "'a ⇒ bool" where "rectangle x ≡ x * top * x = x" end context stone_relation_algebra begin lemma arc_rectangle: "arc x ⟹ rectangle x" using arc_top_arc by blast section ‹Relation-Algebraic Semantics of Associative Array Access› text ‹ The following two operations model updating array $x$ at index $y$ to value $z$, and reading the content of array $x$ at index $y$, respectively. The read operation uses double brackets to avoid ambiguity with list syntax. The remainder of this section shows basic properties of these operations. › abbreviation rel_update :: "'a ⇒ 'a ⇒ 'a ⇒ 'a" ("(_[_⟼_])" [70, 65, 65] 61) where "x[y⟼z] ≡ (y ⊓ z⇧^{T}) ⊔ (-y ⊓ x)" abbreviation rel_access :: "'a ⇒ 'a ⇒ 'a" ("(2_[[_]])" [70, 65] 65) where "x[[y]] ≡ x⇧^{T}* y" lemma update_univalent: assumes "univalent x" and "vector y" and "injective z" shows "univalent (x[y⟼z])" proof - have 1: "univalent (y ⊓ z⇧^{T})" using assms(3) inf_commute univalent_inf_closed by force have "(y ⊓ z⇧^{T})⇧^{T}* (-y ⊓ x) = (y⇧^{T}⊓ z) * (-y ⊓ x)" by (simp add: conv_dist_inf) also have "... = z * (y ⊓ -y ⊓ x)" by (metis assms(2) covector_inf_comp_3 inf.sup_monoid.add_assoc inf.sup_monoid.add_commute) finally have 2: "(y ⊓ z⇧^{T})⇧^{T}* (-y ⊓ x) = bot" by simp have 3: "vector (-y)" using assms(2) vector_complement_closed by simp have "(-y ⊓ x)⇧^{T}* (y ⊓ z⇧^{T}) = (-y⇧^{T}⊓ x⇧^{T}) * (y ⊓ z⇧^{T})" by (simp add: conv_complement conv_dist_inf) also have "... = x⇧^{T}* (-y ⊓ y ⊓ z⇧^{T})" using 3 by (metis (mono_tags, opaque_lifting) conv_complement covector_inf_comp_3 inf.sup_monoid.add_assoc inf.sup_monoid.add_commute) finally have 4: "(-y ⊓ x)⇧^{T}* (y ⊓ z⇧^{T}) = bot" by simp have 5: "univalent (-y ⊓ x)" using assms(1) inf_commute univalent_inf_closed by fastforce have "(x[y⟼z])⇧^{T}* (x[y⟼z]) = (y ⊓ z⇧^{T})⇧^{T}* (x[y⟼z]) ⊔ (-y ⊓ x)⇧^{T}* (x[y⟼z])" by (simp add: conv_dist_sup mult_right_dist_sup) also have "... = (y ⊓ z⇧^{T})⇧^{T}* (y ⊓ z⇧^{T}) ⊔ (y ⊓ z⇧^{T})⇧^{T}* (-y ⊓ x) ⊔ (-y ⊓ x)⇧^{T}* (y ⊓ z⇧^{T}) ⊔ (-y ⊓ x)⇧^{T}* (-y ⊓ x)" by (simp add: mult_left_dist_sup sup_assoc) finally show ?thesis using 1 2 4 5 by simp qed lemma update_total: assumes "total x" and "vector y" and "regular y" and "surjective z" shows "total (x[y⟼z])" proof - have "(x[y⟼z]) * top = x*top[y⟼top*z]" by (simp add: assms(2) semiring.distrib_right vector_complement_closed vector_inf_comp conv_dist_comp) also have "... = top[y⟼top]" using assms(1) assms(4) by simp also have "... = top" using assms(3) regular_complement_top by auto finally show ?thesis by simp qed lemma update_mapping: assumes "mapping x" and "vector y" and "regular y" and "bijective z" shows "mapping (x[y⟼z])" using assms update_univalent update_total by simp lemma read_injective: assumes "injective y" and "univalent x" shows "injective (x[[y]])" using assms injective_mult_closed univalent_conv_injective by blast lemma read_surjective: assumes "surjective y" and "total x" shows "surjective (x[[y]])" using assms surjective_mult_closed total_conv_surjective by blast lemma read_bijective: assumes "bijective y" and "mapping x" shows "bijective (x[[y]])" by (simp add: assms read_injective read_surjective) lemma read_point: assumes "point p" and "mapping x" shows "point (x[[p]])" using assms comp_associative read_injective read_surjective by auto lemma update_postcondition: assumes "point x" "point y" shows "x ⊓ p = x * y⇧^{T}⟷ p[[x]] = y" apply (rule iffI) subgoal by (metis assms comp_associative conv_dist_comp conv_involutive covector_inf_comp_3 equivalence_top_closed vector_covector) subgoal apply (rule order.antisym) subgoal by (metis assms conv_dist_comp conv_involutive inf.boundedI inf.cobounded1 vector_covector vector_restrict_comp_conv) subgoal by (smt assms comp_associative conv_dist_comp conv_involutive covector_restrict_comp_conv dense_conv_closed equivalence_top_closed inf.boundedI shunt_mapping vector_covector preorder_idempotent) done done text ‹Back and von Wright's array independence requirements \<^cite>‹"BackWright1998"›, later also lens laws \<^cite>‹"FosterGreenwaldMoorePierceSchmitt2007"›› lemma put_get_sub: assumes "vector y" "surjective u" "vector z" "u ≤ y" shows "(x[y⟼z])[[u]] = z" proof - have "(x[y⟼z])[[u]] = (y⇧^{T}⊓ z) * u ⊔ (-y⇧^{T}⊓ x⇧^{T}) * u" by (simp add: conv_complement conv_dist_inf conv_dist_sup mult_right_dist_sup) also have "... = z * u" proof - have "(-y⇧^{T}⊓ x⇧^{T}) * u ≤ (-y⇧^{T}⊓ x⇧^{T}) * y" by (simp add: assms(4) mult_right_isotone) also have "... = bot" by (metis assms(1) covector_inf_comp_3 inf_commute conv_complement mult_right_zero p_inf vector_complement_closed) finally have "(-y⇧^{T}⊓ x⇧^{T}) * u = bot" by (simp add: bot_unique) thus ?thesis using assms(1,4) covector_inf_comp_3 inf.absorb_iff1 inf_commute by auto qed also have "... = z" by (metis assms(2,3) mult_assoc) finally show ?thesis . qed lemma put_get: assumes "vector y" "surjective y" "vector z" shows "(x[y⟼z])[[y]] = z" by (simp add: assms put_get_sub) lemma put_put: "(x[y⟼z])[y⟼w] = x[y⟼w]" by (metis inf_absorb2 inf_commute inf_le1 inf_sup_distrib1 maddux_3_13 sup_inf_absorb) lemma get_put: assumes "point y" shows "x[y⟼x[[y]]] = x" proof - have "x[y⟼x[[y]]] = (y ⊓ y⇧^{T}* x) ⊔ (-y ⊓ x)" by (simp add: conv_dist_comp) also have "... = (y ⊓ x) ⊔ (-y ⊓ x)" proof - have "y ⊓ y⇧^{T}* x = y ⊓ x" proof (rule order.antisym) have "y ⊓ y⇧^{T}* x = (y ⊓ y⇧^{T}) * x" by (simp add: assms vector_inf_comp) also have "(y ⊓ y⇧^{T}) * x = y * y⇧^{T}* x" by (simp add: assms vector_covector) also have "... ≤ x" using assms comp_isotone by fastforce finally show "y ⊓ y⇧^{T}* x ≤ y ⊓ x" by simp have "y ⊓ x ≤ y⇧^{T}* x" by (simp add: assms vector_restrict_comp_conv) thus "y ⊓ x ≤ y ⊓ y⇧^{T}* x" by simp qed thus ?thesis by simp qed also have "... = x" proof - have "regular y" using assms bijective_regular by blast thus ?thesis by (metis inf.sup_monoid.add_commute maddux_3_11_pp) qed finally show ?thesis . qed lemma update_inf: "u ≤ y ⟹ (x[y⟼z]) ⊓ u = z⇧^{T}⊓ u" by (smt comp_inf.mult_right_dist_sup comp_inf.semiring.mult_zero_right inf.left_commute inf.sup_monoid.add_assoc inf_absorb2 p_inf sup_bot_right inf.sup_monoid.add_commute) lemma update_inf_same: "(x[y⟼z]) ⊓ y = z⇧^{T}⊓ y" by (simp add: update_inf) lemma update_inf_different: "u ≤ -y ⟹ (x[y⟼z]) ⊓ u = x ⊓ u" by (smt inf.right_idem inf.sup_monoid.add_commute inf.sup_relative_same_increasing inf_import_p maddux_3_13 sup.cobounded2 update_inf_same) end section ‹Relation-Algebraic Semantics of Disjoint-Set Forests› text ‹ A disjoint-set forest represents a partition of a set into equivalence classes. We take the represented equivalence relation as the semantics of a forest. It is obtained by operation ‹fc› below. Additionally, operation ‹wcc› giving the weakly connected components of a graph will be used for the semantics of the union of two disjoint sets. Finally, operation ‹root› yields the root of a component tree, that is, the representative of a set containing a given element. This section defines these operations and derives their properties. › context stone_kleene_relation_algebra begin lemma omit_redundant_points: assumes "point p" shows "p ⊓ x⇧^{⋆}= (p ⊓ 1) ⊔ (p ⊓ x) * (-p ⊓ x)⇧^{⋆}" proof (rule order.antisym) let ?p = "p ⊓ 1" have "?p * x * (-p ⊓ x)⇧^{⋆}* ?p ≤ ?p * top * ?p" by (metis comp_associative mult_left_isotone mult_right_isotone top.extremum) also have "... ≤ ?p" by (simp add: assms injective_codomain vector_inf_one_comp) finally have "?p * x * (-p ⊓ x)⇧^{⋆}* ?p * x ≤ ?p * x" using mult_left_isotone by blast hence "?p * x * (-p ⊓ x)⇧^{⋆}* (p ⊓ x) ≤ ?p * x" by (simp add: assms comp_associative vector_inf_one_comp) also have 1: "... ≤ ?p * x * (-p ⊓ x)⇧^{⋆}" using mult_right_isotone star.circ_reflexive by fastforce finally have "?p * x * (-p ⊓ x)⇧^{⋆}* (p ⊓ x) ⊔ ?p * x * (-p ⊓ x)⇧^{⋆}* (-p ⊓ x) ≤ ?p * x * (-p ⊓ x)⇧^{⋆}" by (simp add: mult_right_isotone star.circ_plus_same star.left_plus_below_circ mult_assoc) hence "?p * x * (-p ⊓ x)⇧^{⋆}* ((p ⊔ -p) ⊓ x) ≤ ?p * x * (-p ⊓ x)⇧^{⋆}" by (simp add: comp_inf.mult_right_dist_sup mult_left_dist_sup) hence "?p * x * (-p ⊓ x)⇧^{⋆}* x ≤ ?p * x * (-p ⊓ x)⇧^{⋆}" by (metis assms bijective_regular inf.absorb2 inf.cobounded1 inf.sup_monoid.add_commute shunting_p) hence "?p * x * (-p ⊓ x)⇧^{⋆}* x ⊔ ?p * x ≤ ?p * x * (-p ⊓ x)⇧^{⋆}" using 1 by simp hence "?p * (1 ⊔ x * (-p ⊓ x)⇧^{⋆}) * x ≤ ?p * x * (-p ⊓ x)⇧^{⋆}" by (simp add: comp_associative mult_left_dist_sup mult_right_dist_sup) also have "... ≤ ?p * (1 ⊔ x * (-p ⊓ x)⇧^{⋆})" by (simp add: comp_associative mult_right_isotone) finally have "?p * x⇧^{⋆}≤ ?p * (1 ⊔ x * (-p ⊓ x)⇧^{⋆})" using star_right_induct by (meson dual_order.trans le_supI mult_left_sub_dist_sup_left mult_sub_right_one) also have "... = ?p ⊔ ?p * x * (-p ⊓ x)⇧^{⋆}" by (simp add: comp_associative semiring.distrib_left) finally show "p ⊓ x⇧^{⋆}≤ ?p ⊔ (p ⊓ x) * (-p ⊓ x)⇧^{⋆}" by (simp add: assms vector_inf_one_comp) show "?p ⊔ (p ⊓ x) * (-p ⊓ x)⇧^{⋆}≤ p ⊓ x⇧^{⋆}" by (metis assms comp_isotone inf.boundedI inf.cobounded1 inf.coboundedI2 inf.sup_monoid.add_commute le_supI star.circ_increasing star.circ_transitive_equal star_isotone star_left_unfold_equal sup.cobounded1 vector_export_comp) qed text ‹Weakly connected components› abbreviation "wcc x ≡ (x ⊔ x⇧^{T})⇧^{⋆}" lemma wcc_equivalence: "equivalence (wcc x)" apply (intro conjI) subgoal by (simp add: star.circ_reflexive) subgoal by (simp add: star.circ_transitive_equal) subgoal by (simp add: conv_dist_sup conv_star_commute sup_commute) done lemma wcc_increasing: "x ≤ wcc x" by (simp add: star.circ_sub_dist_1) lemma wcc_isotone: "x ≤ y ⟹ wcc x ≤ wcc y" using conv_isotone star_isotone sup_mono by blast lemma wcc_idempotent: "wcc (wcc x) = wcc x" using star_involutive wcc_equivalence by auto lemma wcc_below_wcc: "x ≤ wcc y ⟹ wcc x ≤ wcc y" using wcc_idempotent wcc_isotone by fastforce lemma wcc_galois: "x ≤ wcc y ⟷ wcc x ≤ wcc y" using order_trans star.circ_sub_dist_1 wcc_below_wcc by blast lemma wcc_bot: "wcc bot = 1" by (simp add: star.circ_zero) lemma wcc_one: "wcc 1 = 1" by (simp add: star_one) lemma wcc_top: "wcc top = top" by (simp add: star.circ_top) lemma wcc_with_loops: "wcc x = wcc (x ⊔ 1)" by (metis conv_dist_sup star_decompose_1 star_sup_one sup_commute symmetric_one_closed) lemma wcc_without_loops: "wcc x = wcc (x - 1)" by (metis conv_star_commute star_sum reachable_without_loops) lemma forest_components_wcc: "injective x ⟹ wcc x = forest_components x" by (simp add: cancel_separate_1) lemma wcc_sup_wcc: "wcc (x ⊔ y) = wcc (x ⊔ wcc y)" by (smt (verit, ccfv_SIG) le_sup_iff order.antisym sup_right_divisibility wcc_below_wcc wcc_increasing) text ‹Components of a forest, which is represented using edges directed towards the roots› abbreviation "fc x ≡ x⇧^{⋆}* x⇧^{T}⇧^{⋆}" lemma fc_equivalence: "univalent x ⟹ equivalence (fc x)" apply (intro conjI) subgoal by (simp add: reflexive_mult_closed star.circ_reflexive) subgoal by (metis cancel_separate_1 order.eq_iff star.circ_transitive_equal) subgoal by (simp add: conv_dist_comp conv_star_commute) done lemma fc_increasing: "x ≤ fc x" by (metis le_supE mult_left_isotone star.circ_back_loop_fixpoint star.circ_increasing) lemma fc_isotone: "x ≤ y ⟹ fc x ≤ fc y" by (simp add: comp_isotone conv_isotone star_isotone) lemma fc_idempotent: "univalent x ⟹ fc (fc x) = fc x" by (metis fc_equivalence cancel_separate_1 star.circ_transitive_equal star_involutive) lemma fc_star: "univalent x ⟹ (fc x)⇧^{⋆}= fc x" using fc_equivalence fc_idempotent star.circ_transitive_equal by simp lemma fc_plus: "univalent x ⟹ (fc x)⇧^{+}= fc x" by (metis fc_star star.circ_decompose_9) lemma fc_bot: "fc bot = 1" by (simp add: star.circ_zero) lemma fc_one: "fc 1 = 1" by (simp add: star_one) lemma fc_top: "fc top = top" by (simp add: star.circ_top) lemma fc_wcc: "univalent x ⟹ wcc x = fc x" by (simp add: fc_star star_decompose_1) lemma fc_via_root: assumes "total (p⇧^{⋆}* (p ⊓ 1))" shows "fc p = p⇧^{⋆}* (p ⊓ 1) * p⇧^{T}⇧^{⋆}" proof (rule order.antisym) have "1 ≤ p⇧^{⋆}* (p ⊓ 1) * p⇧^{T}⇧^{⋆}" by (smt assms comp_associative conv_dist_comp conv_star_commute coreflexive_idempotent coreflexive_symmetric inf.cobounded2 total_var) hence "fc p ≤ p⇧^{⋆}* p⇧^{⋆}* (p ⊓ 1) * p⇧^{T}⇧^{⋆}* p⇧^{T}⇧^{⋆}" by (metis comp_right_one mult_left_isotone mult_right_isotone mult_assoc) thus "fc p ≤ p⇧^{⋆}* (p ⊓ 1) * p⇧^{T}⇧^{⋆}" by (simp add: star.circ_transitive_equal mult_assoc) show "p⇧^{⋆}* (p ⊓ 1) * p⇧^{T}⇧^{⋆}≤ fc p" by (metis comp_isotone inf.cobounded2 mult_1_right order.refl) qed lemma update_acyclic_1: assumes "acyclic (p - 1)" and "point y" and "vector w" and "w ≤ p⇧^{⋆}* y" shows "acyclic ((p[w⟼y]) - 1)" proof - let ?p = "p[w⟼y]" have "w * y⇧^{T}≤ p⇧^{⋆}" using assms(2,4) shunt_bijective by blast hence "w * y⇧^{T}≤ (p - 1)⇧^{⋆}" using reachable_without_loops by auto hence "w * y⇧^{T}- 1 ≤ (p - 1)⇧^{⋆}- 1" by (simp add: inf.coboundedI2 inf.sup_monoid.add_commute) also have "... ≤ (p - 1)⇧^{+}" by (simp add: star_plus_without_loops) finally have 1: "w ⊓ y⇧^{T}⊓ -1 ≤ (p - 1)⇧^{+}" using assms(2,3) vector_covector by auto have "?p - 1 = (w ⊓ y⇧^{T}⊓ -1) ⊔ (-w ⊓ p ⊓ -1)" by (simp add: inf_sup_distrib2) also have "... ≤ (p - 1)⇧^{+}⊔ (-w ⊓ p ⊓ -1)" using 1 sup_left_isotone by blast also have "... ≤ (p - 1)⇧^{+}⊔ (p - 1)" using comp_inf.mult_semi_associative sup_right_isotone by auto also have "... = (p - 1)⇧^{+}" by (metis star.circ_back_loop_fixpoint sup.right_idem) finally have "(?p - 1)⇧^{+}≤ (p - 1)⇧^{+}" by (metis comp_associative comp_isotone star.circ_transitive_equal star.left_plus_circ star_isotone) also have "... ≤ -1" using assms(1) by blast finally show ?thesis by simp qed lemma update_acyclic_2: assumes "acyclic (p - 1)" and "point y" and "point x" and "y ≤ p⇧^{T}⇧^{⋆}* x" and "univalent p" and "p⇧^{T}* y ≤ y" shows "acyclic ((p[p⇧^{T}⇧^{⋆}*x⟼y]) - 1)" proof - have "p⇧^{T}* p⇧^{⋆}* y = p⇧^{T}* p * p⇧^{⋆}* y ⊔ p⇧^{T}* y" by (metis comp_associative mult_left_dist_sup star.circ_loop_fixpoint) also have "... ≤ p⇧^{⋆}* y" by (metis assms(5,6) comp_right_one le_supI le_supI2 mult_left_isotone star.circ_loop_fixpoint star.circ_transitive_equal) finally have "p⇧^{T}⇧^{⋆}* x ≤ p⇧^{⋆}* y" by (simp add: assms(2-4) bijective_reverse conv_star_commute comp_associative star_left_induct) thus ?thesis by (simp add: assms(1-3) vector_mult_closed update_acyclic_1) qed lemma update_acyclic_3: assumes "acyclic (p - 1)" and "point y" and "point w" and "y ≤ p⇧^{T}⇧^{⋆}* w" shows "acyclic ((p[w⟼y]) - 1)" by (simp add: assms bijective_reverse conv_star_commute update_acyclic_1) lemma rectangle_star_rectangle: "rectangle a ⟹ a * x⇧^{⋆}* a ≤ a" by (metis mult_left_isotone mult_right_isotone top.extremum) lemma arc_star_arc: "arc a ⟹ a * x⇧^{⋆}* a ≤ a" using arc_top_arc rectangle_star_rectangle by blast lemma star_rectangle_decompose: assumes "rectangle a" shows "(a ⊔ x)⇧^{⋆}= x⇧^{⋆}⊔ x⇧^{⋆}* a * x⇧^{⋆}" proof (rule order.antisym) have 1: "1 ≤ x⇧^{⋆}⊔ x⇧^{⋆}* a * x⇧^{⋆}" by (simp add: star.circ_reflexive sup.coboundedI1) have "(a ⊔ x) * (x⇧^{⋆}⊔ x⇧^{⋆}* a * x⇧^{⋆}) = a * x⇧^{⋆}⊔ a * x⇧^{⋆}* a * x⇧^{⋆}⊔ x⇧^{+}⊔ x⇧^{+}* a * x⇧^{⋆}" by (metis comp_associative semiring.combine_common_factor semiring.distrib_left sup_commute) also have "... = a * x⇧^{⋆}⊔ x⇧^{+}⊔ x⇧^{+}* a * x⇧^{⋆}" using assms rectangle_star_rectangle by (simp add: mult_left_isotone sup_absorb1) also have "... = x⇧^{+}⊔ x⇧^{⋆}* a * x⇧^{⋆}" by (metis comp_associative star.circ_loop_fixpoint sup_assoc sup_commute) also have "... ≤ x⇧^{⋆}⊔ x⇧^{⋆}* a * x⇧^{⋆}" using star.left_plus_below_circ sup_left_isotone by auto finally show "(a ⊔ x)⇧^{⋆}≤ x⇧^{⋆}⊔ x⇧^{⋆}* a * x⇧^{⋆}" using 1 by (metis comp_right_one le_supI star_left_induct) next show "x⇧^{⋆}⊔ x⇧^{⋆}* a * x⇧^{⋆}≤ (a ⊔ x)⇧^{⋆}" by (metis comp_isotone le_supE le_supI star.circ_increasing star.circ_transitive_equal star_isotone sup_ge2) qed lemma star_arc_decompose: "arc a ⟹ (a ⊔ x)⇧^{⋆}= x⇧^{⋆}⊔ x⇧^{⋆}* a * x⇧^{⋆}" using arc_top_arc star_rectangle_decompose by blast lemma plus_rectangle_decompose: assumes "rectangle a" shows "(a ⊔ x)⇧^{+}= x⇧^{+}⊔ x⇧^{⋆}* a * x⇧^{⋆}" proof - have "(a ⊔ x)⇧^{+}= (a ⊔ x) * (x⇧^{⋆}⊔ x⇧^{⋆}* a * x⇧^{⋆})" by (simp add: assms star_rectangle_decompose) also have "... = a * x⇧^{⋆}⊔ a * x⇧^{⋆}* a * x⇧^{⋆}⊔ x⇧^{+}⊔ x⇧^{+}* a * x⇧^{⋆}" by (metis comp_associative semiring.combine_common_factor semiring.distrib_left sup_commute) also have "... = a * x⇧^{⋆}⊔ x⇧^{+}⊔ x⇧^{+}* a * x⇧^{⋆}" using assms rectangle_star_rectangle by (simp add: mult_left_isotone sup_absorb1) also have "... = x⇧^{+}⊔ x⇧^{⋆}* a * x⇧^{⋆}" by (metis comp_associative star.circ_loop_fixpoint sup_assoc sup_commute) finally show ?thesis by simp qed lemma plus_arc_decompose: "arc a ⟹ (a ⊔ x)⇧^{+}= x⇧^{+}⊔ x⇧^{⋆}* a * x⇧^{⋆}" using arc_top_arc plus_rectangle_decompose by blast lemma update_acyclic_4: assumes "acyclic (p - 1)" and "point y" and "point w" and "y ⊓ p⇧^{⋆}* w = bot" shows "acyclic ((p[w⟼y]) - 1)" proof - let ?p = "p[w⟼y]" have "y⇧^{T}* p⇧^{⋆}* w ≤ -1" using assms(4) comp_associative pseudo_complement schroeder_3_p by auto hence 1: "p⇧^{⋆}* w * y⇧^{T}* p⇧^{⋆}≤ -1" by (metis comp_associative comp_commute_below_diversity star.circ_transitive_equal) have "?p - 1 ≤ (w ⊓ y⇧^{T}) ⊔ (p - 1)" by (metis comp_inf.mult_right_dist_sup dual_order.trans inf.cobounded1 inf.coboundedI2 inf.sup_monoid.add_assoc le_supI sup.cobounded1 sup_ge2) also have "... = w * y⇧^{T}⊔ (p - 1)" using assms(2,3) by (simp add: vector_covector) finally have "(?p - 1)⇧^{+}≤ (w * y⇧^{T}⊔ (p - 1))⇧^{+}" by (simp add: comp_isotone star_isotone) also have "... = (p - 1)⇧^{+}⊔ (p - 1)⇧^{⋆}* w * y⇧^{T}* (p - 1)⇧^{⋆}" using assms(2,3) plus_arc_decompose points_arc by (simp add: comp_associative) also have "... ≤ (p - 1)⇧^{+}⊔ p⇧^{⋆}* w * y⇧^{T}* p⇧^{⋆}" using reachable_without_loops by auto also have "... ≤ -1" using 1 assms(1) by simp finally show ?thesis by simp qed lemma update_acyclic_5: assumes "acyclic (p - 1)" and "point w" shows "acyclic ((p[w⟼w]) - 1)" proof - let ?p = "p[w⟼w]" have "?p - 1 ≤ (w ⊓ w⇧^{T}⊓ -1) ⊔ (p - 1)" by (metis comp_inf.mult_right_dist_sup inf.cobounded2 inf.sup_monoid.add_assoc sup_right_isotone) also have "... = p - 1" using assms(2) by (metis comp_inf.covector_complement_closed equivalence_top_closed inf_top.right_neutral maddux_3_13 pseudo_complement regular_closed_top regular_one_closed vector_covector vector_top_closed) finally show ?thesis using assms(1) acyclic_down_closed by blast qed text ‹Root of the tree containing point $x$ in the disjoint-set forest $p$› abbreviation "roots p ≡ (p ⊓ 1) * top" abbreviation "root p x ≡ p⇧^{T}⇧^{⋆}* x ⊓ roots p" lemma root_var: "root p x = (p ⊓ 1) * p⇧^{T}⇧^{⋆}* x" by (simp add: coreflexive_comp_top_inf inf_commute mult_assoc) lemma root_successor_loop: "univalent p ⟹ root p x = p[[root p x]]" by (metis root_var injective_codomain comp_associative conv_dist_inf coreflexive_symmetric equivalence_one_closed inf.cobounded2 univalent_conv_injective) lemma root_transitive_successor_loop: "univalent p ⟹ root p x = p⇧^{T}⇧^{⋆}* (root p x)" by (metis mult_1_right star_one star_simulation_right_equal root_successor_loop) lemma roots_successor_loop: "univalent p ⟹ p[[roots p]] = roots p" by (metis conv_involutive inf_commute injective_codomain one_inf_conv mult_assoc) lemma roots_transitive_successor_loop: "univalent p ⟹ p⇧^{T}⇧^{⋆}* (roots p) = roots p" by (metis comp_associative star.circ_left_top star_simulation_right_equal roots_successor_loop) text ‹The root of a tree of a node belongs to the same component as the node.› lemma root_same_component: "injective x ⟹ root p x * x⇧^{T}≤ fc p" by (metis comp_associative coreflexive_comp_top_inf eq_refl inf.sup_left_divisibility inf.sup_monoid.add_commute mult_isotone star.circ_circ_mult star.circ_right_top star.circ_transitive_equal star_one star_outer_increasing test_preserves_equation top_greatest) lemma root_vector: "vector x ⟹ vector (root p x)" by (simp add: vector_mult_closed root_var) lemma root_vector_inf: "vector x ⟹ root p x * x⇧^{T}= root p x ⊓ x⇧^{T}" by (simp add: vector_covector root_vector) lemma root_same_component_vector: "injective x ⟹ vector x ⟹ root p x ⊓ x⇧^{T}≤ fc p" using root_same_component root_vector_inf by fastforce lemma univalent_root_successors: assumes "univalent p" shows "(p ⊓ 1) * p⇧^{⋆}= p ⊓ 1" proof (rule order.antisym) have "(p ⊓ 1) * p ≤ p ⊓ 1" by (smt assms(1) comp_inf.mult_semi_associative conv_dist_comp conv_dist_inf conv_order equivalence_one_closed inf.absorb1 inf.sup_monoid.add_assoc injective_codomain) thus "(p ⊓ 1) * p⇧^{⋆}≤ p ⊓ 1" using star_right_induct_mult by blast show "p ⊓ 1 ≤ (p ⊓ 1) * p⇧^{⋆}" by (metis coreflexive_idempotent inf_le1 inf_le2 mult_right_isotone order_trans star.circ_increasing) qed lemma same_component_same_root_sub: assumes "univalent p" and "bijective y" and "x * y⇧^{T}≤ fc p" shows "root p x ≤ root p y" proof - have "root p x * y⇧^{T}≤ (p ⊓ 1) * p⇧^{T}⇧^{⋆}" by (smt assms(1,3) mult_isotone mult_assoc root_var fc_plus fc_star order.eq_iff univalent_root_successors) thus ?thesis by (simp add: assms(2) shunt_bijective root_var) qed lemma same_component_same_root: assumes "univalent p" and "bijective x" and "bijective y" and "x * y⇧^{T}≤ fc p" shows "root p x = root p y" proof (rule order.antisym) show "root p x ≤ root p y" using assms(1,3,4) same_component_same_root_sub by blast have "y * x⇧^{T}≤ fc p" using assms(1,4) fc_equivalence conv_dist_comp conv_isotone by fastforce thus "root p y ≤ root p x" using assms(1,2) same_component_same_root_sub by blast qed lemma same_roots_sub: assumes "univalent q" and "p ⊓ 1 ≤ q ⊓ 1" and "fc p ≤ fc q" shows "p⇧^{⋆}* (p ⊓ 1) ≤ q⇧^{⋆}* (q ⊓ 1)" proof - have "p⇧^{⋆}* (p ⊓ 1) ≤ p⇧^{⋆}* (q ⊓ 1)" using assms(2) mult_right_isotone by auto also have "... ≤ fc p * (q ⊓ 1)" using mult_left_isotone mult_right_isotone star.circ_reflexive by fastforce also have "... ≤ fc q * (q ⊓ 1)" by (simp add: assms(3) mult_left_isotone) also have "... = q⇧^{⋆}* (q ⊓ 1)" by (metis assms(1) conv_dist_comp conv_dist_inf conv_star_commute inf_commute one_inf_conv symmetric_one_closed mult_assoc univalent_root_successors) finally show ?thesis . qed lemma same_roots: assumes "univalent p" and "univalent q" and "p ⊓ 1 = q ⊓ 1" and "fc p = fc q" shows "p⇧^{⋆}* (p ⊓ 1) = q⇧^{⋆}* (q ⊓ 1)" by (smt assms conv_dist_comp conv_dist_inf conv_involutive conv_star_commute inf_commute one_inf_conv symmetric_one_closed root_var univalent_root_successors) lemma same_root: assumes "univalent p" and "univalent q" and "p ⊓ 1 = q ⊓ 1" and "fc p = fc q" shows "root p x = root q x" by (metis assms mult_assoc root_var univalent_root_successors) lemma loop_root: assumes "injective x" and "x = p[[x]]" shows "x = root p x" proof (rule order.antisym) have "x ≤ p * x" by (metis assms comp_associative comp_right_one conv_order equivalence_one_closed ex231c inf.orderE inf.sup_monoid.add_commute mult_left_isotone mult_right_isotone one_inf_conv) hence "x = (p ⊓ 1) * x" by (simp add: assms(1) inf_absorb2 injective_comp_right_dist_inf) thus "x ≤ root p x" by (metis assms(2) coreflexive_comp_top_inf inf.boundedI inf.cobounded1 inf.cobounded2 mult_isotone star.circ_increasing) next show "root p x ≤ x" using assms(2) le_infI1 star_left_induct_mult by auto qed lemma one_loop: assumes "acyclic (p - 1)" and "univalent p" shows "(p ⊓ 1) * (p⇧^{T}- 1)⇧^{+}* (p ⊓ 1) = bot" proof - have "p⇧^{T}⇧^{+}⊓ (p ⊓ 1) * top * (p ⊓ 1) = (p ⊓ 1) * p⇧^{T}⇧^{+}* (p ⊓ 1)" by (simp add: test_comp_test_top) also have "... ≤ p⇧^{T}⇧^{⋆}* (p ⊓ 1)" by (simp add: inf.coboundedI2 mult_left_isotone star.circ_mult_upper_bound star.circ_reflexive star.left_plus_below_circ) also have "... = p ⊓ 1" by (metis assms(2) conv_dist_comp conv_dist_inf conv_star_commute inf_commute one_inf_conv symmetric_one_closed univalent_root_successors) also have "... ≤ 1" by simp finally have "(p ⊓ 1) * top * (p ⊓ 1) ≤ -(p⇧^{T}⇧^{+}- 1)" using p_antitone p_antitone_iff p_shunting_swap by blast hence "(p ⊓ 1)⇧^{T}* (p⇧^{T}⇧^{+}- 1) * (p ⊓ 1)⇧^{T}≤ bot" using triple_schroeder_p p_top by blast hence "(p ⊓ 1) * (p⇧^{T}⇧^{+}- 1) * (p ⊓ 1) = bot" by (simp add: coreflexive_symmetric le_bot) thus ?thesis by (smt assms(1) conv_complement conv_dist_comp conv_dist_inf conv_star_commute inf_absorb1 star.circ_plus_same symmetric_one_closed reachable_without_loops star_plus_without_loops) qed lemma root_root: "root p x = root p (root p x)" by (smt comp_associative comp_inf.mult_right_sub_dist_sup_right dual_order.eq_iff inf.cobounded1 inf.cobounded2 inf.orderE mult_right_isotone star.circ_loop_fixpoint star.circ_transitive_equal root_var) lemma loop_root_2: assumes "acyclic (p - 1)" and "univalent p" and "injective x" and "x ≤ p⇧^{T}⇧^{+}* x" shows "x = root p x" proof (rule order.antisym) have 1: "x = x - (-1 * x)" by (metis assms(3) comp_injective_below_complement inf.orderE mult_1_left regular_one_closed) have "x ≤ (p⇧^{T}- 1)⇧^{+}* x ⊔ (p ⊓ 1) * x" by (metis assms(4) inf_commute mult_right_dist_sup one_inf_conv plus_reachable_without_loops) also have "... ≤ -1 * x ⊔ (p ⊓ 1) * x" by (metis assms(1) conv_complement conv_dist_inf conv_isotone conv_plus_commute mult_left_isotone semiring.add_right_mono symmetric_one_closed) also have "... ≤ -1 * x ⊔ root p x" using comp_isotone inf.coboundedI2 star.circ_reflexive sup_right_isotone by auto finally have "x ≤ (-1 * x ⊔ root p x) - (-1 * x)" using 1 inf.boundedI inf.order_iff by blast also have "... ≤ root p x" using inf.sup_left_divisibility by auto finally show 2: "x ≤ root p x" . have "root p x = (p ⊓ 1) * x ⊔ (p ⊓ 1) * (p⇧^{T}- 1)⇧^{+}* x" by (metis comp_associative mult_left_dist_sup star.circ_loop_fixpoint sup_commute reachable_without_loops root_var) also have "... ≤ x ⊔ (p ⊓ 1) * (p⇧^{T}- 1)⇧^{+}* root p x" using 2 by (metis coreflexive_comp_top_inf inf.cobounded2 mult_right_isotone semiring.add_mono) also have "... = x" by (metis assms(1,2) one_loop root_var mult_assoc semiring.mult_not_zero sup_bot_right) finally show "root p x ≤ x" . qed lemma path_compression_invariant_simplify: assumes "point w" and "p⇧^{T}⇧^{+}* w ≤ -w" and "w ≠ y" shows "p[[w]] ≠ w" proof assume "p[[w]] = w" hence "w ≤ p⇧^{T}⇧^{+}* w" by (metis comp_isotone eq_refl star.circ_mult_increasing) also have "... ≤ -w" by (simp add: assms(2)) finally have "w = bot" using inf.orderE by fastforce thus False using assms(1,3) le_bot by force qed end context stone_relation_algebra_tarski begin text ‹lemma ‹distinct_points› has been moved to theory ‹Relation_Algebras› in entry ‹Stone_Relation_Algebras›› text ‹Back and von Wright's array independence requirements \<^cite>‹"BackWright1998"›› lemma put_get_different_vector: assumes "vector y" "w ≤ -y" shows "(x[y⟼z])[[w]] = x[[w]]" proof - have "(x[y⟼z])[[w]] = (y⇧^{T}⊓ z) * w ⊔ (-y⇧^{T}⊓ x⇧^{T}) * w" by (simp add: conv_complement conv_dist_inf conv_dist_sup mult_right_dist_sup) also have "... = z * (w ⊓ y) ⊔ x⇧^{T}* (w - y)" by (metis assms(1) conv_complement covector_inf_comp_3 inf_commute vector_complement_closed) also have "... = z * (w ⊓ y) ⊔ x⇧^{T}* w" by (simp add: assms(2) inf.absorb1) also have "... = z * bot ⊔ x⇧^{T}* w" by (metis assms(2) comp_inf.semiring.mult_zero_right inf.absorb1 inf.sup_monoid.add_assoc p_inf) also have "... = x⇧^{T}* w" by simp finally show ?thesis . qed lemma put_get_different: assumes "point y" "point w" "w ≠ y" shows "(x[y⟼z])[[w]] = x[[w]]" proof - have "w ⊓ y = bot" using assms distinct_points by simp hence "w ≤ -y" using pseudo_complement by simp thus ?thesis by (simp add: assms(1) assms(2) put_get_different_vector) qed lemma put_put_different_vector: assumes "vector y" "vector v" "v ⊓ y = bot" shows "(x[y⟼z])[v⟼w] = (x[v⟼w])[y⟼z]" proof - have "(x[y⟼z])[v⟼w] = (v ⊓ w⇧^{T}) ⊔ (-v ⊓ y ⊓ z⇧^{T}) ⊔ (-v ⊓ -y ⊓ x)" by (simp add: comp_inf.semiring.distrib_left inf_assoc sup_assoc) also have "... = (v ⊓ w⇧^{T}) ⊔ (y ⊓ z⇧^{T}) ⊔ (-v ⊓ -y ⊓ x)" by (metis assms(3) inf_commute inf_import_p p_inf selection_closed_id) also have "... = (y ⊓ z⇧^{T}) ⊔ (v ⊓ w⇧^{T}) ⊔ (-y ⊓ -v ⊓ x)" by (simp add: inf_commute sup_commute) also have "... = (y ⊓ z⇧^{T}) ⊔ (-y ⊓ v ⊓ w⇧^{T}) ⊔ (-y ⊓ -v ⊓ x)" using assms distinct_points pseudo_complement inf.absorb2 by simp also have "... = (x[v⟼w])[y⟼z]" by (simp add: comp_inf.semiring.distrib_left inf_assoc sup_assoc) finally show ?thesis . qed lemma put_put_different: assumes "point y" "point v" "v ≠ y" shows "(x[y⟼z])[v⟼w] = (x[v⟼w])[y⟼z]" using assms distinct_points put_put_different_vector by blast end section ‹Verifying Operations on Disjoint-Set Forests› text ‹ In this section we verify the make-set, find-set and union-sets operations of disjoint-set forests. We start by introducing syntax for updating arrays in programs. Updating the value at a given array index means updating the whole array. › syntax "_rel_update" :: "idt ⇒ 'a ⇒ 'a ⇒ 'b com" ("(2_[_] :=/ _)" [70, 65, 65] 61) translations "x[y] := z" => "(x := (y ⊓ z⇧^{T}) ⊔ (CONST uminus y ⊓ x))" text ‹ The finiteness requirement in the following class is used for proving that the operations terminate. › class finite_regular_p_algebra = p_algebra + assumes finite_regular: "finite { x . regular x }" begin abbreviation card_down_regular :: "'a ⇒ nat" ("_↓" [100] 100) where "x↓ ≡ card { z . regular z ∧ z ≤ x }" end class stone_kleene_relation_algebra_tarski_finite_regular = stone_kleene_relation_algebra_tarski + finite_regular_p_algebra begin subsection ‹Make-Set› text ‹ We prove two correctness results about make-set. The first shows that the forest changes only to the extent of making one node the root of a tree. The second result adds that only singleton sets are created. › definition "make_set_postcondition p x p0 ≡ x ⊓ p = x * x⇧^{T}∧ -x ⊓ p = -x ⊓ p0" theorem make_set: "VARS p [ point x ∧ p0 = p ] p[x] := x [ make_set_postcondition p x p0 ]" apply vcg_tc_simp by (simp add: make_set_postcondition_def inf_sup_distrib1 inf_assoc[THEN sym] vector_covector[THEN sym]) theorem make_set_2: "VARS p [ point x ∧ p0 = p ∧ p ≤ 1 ] p[x] := x [ make_set_postcondition p x p0 ∧ p ≤ 1 ]" proof vcg_tc fix p assume 1: "point x ∧ p0 = p ∧ p ≤ 1" show "make_set_postcondition (p[x⟼x]) x p0 ∧ p[x⟼x] ≤ 1" proof (rule conjI) show "make_set_postcondition (p[x⟼x]) x p0" using 1 by (simp add: make_set_postcondition_def inf_sup_distrib1 inf_assoc[THEN sym] vector_covector[THEN sym]) show "p[x⟼x] ≤ 1" using 1 by (metis coreflexive_sup_closed dual_order.trans inf.cobounded2 vector_covector) qed qed text ‹ The above total-correctness proof allows us to extract a function, which can be used in other implementations below. This is a technique of \<^cite>‹"Guttmann2018c"›. › lemma make_set_exists: "point x ⟹ ∃p' . make_set_postcondition p' x p" using tc_extract_function make_set by blast definition "make_set p x ≡ (SOME p' . make_set_postcondition p' x p)" lemma make_set_function: assumes "point x" and "p' = make_set p x" shows "make_set_postcondition p' x p" proof - let ?P = "λp' . make_set_postcondition p' x p" have "?P (SOME z . ?P z)" using assms(1) make_set_exists by (meson someI) thus ?thesis using assms(2) make_set_def by auto qed end subsection ‹Find-Set› text ‹ Disjoint-set forests are represented by their parent mapping. It is a forest except each root of a component tree points to itself. We prove that find-set returns the root of the component tree of the given node. › context pd_kleene_allegory begin abbreviation "disjoint_set_forest p ≡ mapping p ∧ acyclic (p - 1)" end context stone_kleene_relation_algebra_tarski begin text ‹ If two nodes are mutually reachable from each other in a disjoint-set forest, they must be equal. › lemma forest_mutually_reachable: assumes "acyclic (p - 1)" "point x" "point y" "x ≤ p⇧^{⋆}* y" "y ≤ p⇧^{⋆}* x" shows "x = y" proof (rule ccontr) assume 1: "x ≠ y" hence 2: "x ≤ -y" by (meson assms(2,3) bijective_regular dual_order.eq_iff point_in_vector_or_complement point_in_vector_or_complement_2) have "x ≤ (p - 1)⇧^{⋆}* y" using assms(4) reachable_without_loops by auto also have "... = (p - 1)⇧^{+}* y ⊔ y" by (simp add: star.circ_loop_fixpoint mult_assoc) finally have 3: "x ≤ (p - 1)⇧^{+}* y" using 2 by (metis half_shunting inf.orderE) have 4: "y ≤ -x" using 1 by (meson assms(2,3) bijective_regular dual_order.eq_iff point_in_vector_or_complement point_in_vector_or_complement_2) have "y ≤ (p - 1)⇧^{⋆}* x" using assms(5) reachable_without_loops by auto also have "... = (p - 1)⇧^{+}* x ⊔ x" by (simp add: star.circ_loop_fixpoint mult_assoc) finally have "y ≤ (p - 1)⇧^{+}* x" using 4 by (metis half_shunting inf.orderE) also have "... ≤ (p - 1)⇧^{+}* (p - 1)⇧^{+}* y" using 3 by (simp add: comp_associative mult_right_isotone) also have "... ≤ (p - 1)⇧^{+}* y" by (simp add: mult_left_isotone plus_transitive) finally have "y * y⇧^{T}≤ (p - 1)⇧^{+}" using assms(3) shunt_bijective by blast also have "... ≤ -1" by (simp add: assms(1)) finally have "y = bot" using inf.absorb_iff1 schroeder_4_p by auto thus False using 1 assms(3) bot_least top_unique by auto qed lemma forest_mutually_reachable_2: assumes "acyclic (p - 1)" "point x" "point y" "x ≤ p⇧^{T}⇧^{⋆}* y" "y ≤ p⇧^{T}⇧^{⋆}* x" shows "x = y" proof - have 1: "x ≤ p⇧^{⋆}* y" by (simp add: assms(2,3,5) bijective_reverse conv_star_commute) have "y ≤ p⇧^{⋆}* x" by (simp add: assms(2-4) bijective_reverse conv_star_commute) thus ?thesis using 1 assms(1-3) forest_mutually_reachable by blast qed end context stone_kleene_relation_algebra_tarski_finite_regular begin definition "find_set_precondition p x ≡ disjoint_set_forest p ∧ point x" definition "find_set_invariant p x y ≡ find_set_precondition p x ∧ point y ∧ y ≤ p⇧^{T}⇧^{⋆}* x" definition "find_set_postcondition p x y ≡ point y ∧ y = root p x" lemma find_set_1: "find_set_precondition p x ⟹ find_set_invariant p x x" apply (unfold find_set_invariant_def) using mult_left_isotone star.circ_reflexive find_set_precondition_def by fastforce lemma find_set_2: "find_set_invariant p x y ∧ y ≠ p[[y]] ⟹ find_set_invariant p x (p[[y]]) ∧ (p⇧^{T}⇧^{⋆}* (p[[y]]))↓ < (p⇧^{T}⇧^{⋆}* y)↓" proof - let ?s = "{ z . regular z ∧ z ≤ p⇧^{T}⇧^{⋆}* y }" let ?t = "{ z . regular z ∧ z ≤ p⇧^{T}⇧^{⋆}* (p[[y]]) }" assume 1: "find_set_invariant p x y ∧ y ≠ p[[y]]" have 2: "point (p[[y]])" using 1 read_point find_set_invariant_def find_set_precondition_def by simp show "find_set_invariant p x (p[[y]]) ∧ card ?t < card ?s" proof (unfold find_set_invariant_def, intro conjI) show "find_set_precondition p x" using 1 find_set_invariant_def by simp show "vector (p[[y]])" using 2 by simp show "injective (p[[y]])" using 2 by simp show "surjective (p[[y]])" using 2 by simp show "p[[y]] ≤ p⇧^{T}⇧^{⋆}* x" using 1 by (metis (opaque_lifting) find_set_invariant_def comp_associative comp_isotone star.circ_increasing star.circ_transitive_equal) show "card ?t < card ?s" proof - have "p[[y]] = (p⇧^{T}⊓ 1) * y ⊔ (p⇧^{T}- 1) * y" by (metis maddux_3_11_pp mult_right_dist_sup regular_one_closed) also have "... ≤ ((p[[y]]) ⊓ y) ⊔ (p⇧^{T}- 1) * y" by (metis comp_left_subdist_inf mult_1_left semiring.add_right_mono) also have "... = (p⇧^{T}- 1) * y" using 1 2 find_set_invariant_def distinct_points by auto finally have 3: "(p⇧^{T}- 1)⇧^{⋆}* (p[[y]]) ≤ (p⇧^{T}- 1)⇧^{+}* y" by (simp add: mult_right_isotone star_simulation_right_equal mult_assoc) have "p⇧^{T}⇧^{⋆}* (p[[y]]) ≤ p⇧^{T}⇧^{⋆}* y" by (metis mult_left_isotone star.right_plus_below_circ mult_assoc) hence 4: "?t ⊆ ?s" using order_trans by auto have 5: "y ∈ ?s" using 1 find_set_invariant_def bijective_regular mult_left_isotone star.circ_reflexive by fastforce have 6: "¬ y ∈ ?t" proof assume "y ∈ ?t" hence "y ≤ (p⇧^{T}- 1)⇧^{+}* y" using 3 by (metis reachable_without_loops mem_Collect_eq order_trans) hence "y * y⇧^{T}≤ (p⇧^{T}- 1)⇧^{+}" using 1 find_set_invariant_def shunt_bijective by simp also have "... ≤ -1" using 1 by (metis (mono_tags, lifting) find_set_invariant_def find_set_precondition_def conv_dist_comp conv_dist_inf conv_isotone conv_star_commute equivalence_one_closed star.circ_plus_same symmetric_complement_closed) finally have "y ≤ -y" using schroeder_4_p by auto thus False using 1 by (metis find_set_invariant_def comp_inf.coreflexive_idempotent conv_complement covector_vector_comp inf.absorb1 inf.sup_monoid.add_commute pseudo_complement surjective_conv_total top.extremum vector_top_closed regular_closed_top) qed show "card ?t < card ?s" apply (rule psubset_card_mono) subgoal using finite_regular by simp subgoal using 4 5 6 by auto done qed qed qed lemma find_set_3: "find_set_invariant p x y ∧ y = p[[y]] ⟹ find_set_postcondition p x y" proof - assume 1: "find_set_invariant p x y ∧ y = p[[y]]" show "find_set_postcondition p x y" proof (unfold find_set_postcondition_def, rule conjI) show "point y" using 1 find_set_invariant_def by simp show "y = root p x" proof (rule order.antisym) have "y * y⇧^{T}≤ p" using 1 by (metis find_set_invariant_def find_set_precondition_def shunt_bijective shunt_mapping top_right_mult_increasing) hence "y * y⇧^{T}≤ p ⊓ 1" using 1 find_set_invariant_def le_infI by blast hence "y ≤ roots p" using 1 by (metis find_set_invariant_def order_lesseq_imp shunt_bijective top_right_mult_increasing mult_assoc) thus "y ≤ root p x" using 1 find_set_invariant_def by simp next have 2: "x ≤ p⇧^{⋆}* y" using 1 find_set_invariant_def find_set_precondition_def bijective_reverse conv_star_commute by auto have "p⇧^{T}* p⇧^{⋆}* y = p⇧^{T}* p * p⇧^{⋆}* y ⊔ (p[[y]])" by (metis comp_associative mult_left_dist_sup star.circ_loop_fixpoint) also have "... ≤ p⇧^{⋆}* y ⊔ y" using 1 by (metis find_set_invariant_def find_set_precondition_def comp_isotone mult_left_sub_dist_sup semiring.add_right_mono star.circ_back_loop_fixpoint star.circ_circ_mult star.circ_top star.circ_transitive_equal star_involutive star_one) also have "... = p⇧^{⋆}* y" by (metis star.circ_loop_fixpoint sup.left_idem sup_commute) finally have 3: "p⇧^{T}⇧^{⋆}* x ≤ p⇧^{⋆}* y" using 2 by (simp add: comp_associative star_left_induct) have "p * y ⊓ roots p = (p ⊓ 1) * p * y" using comp_associative coreflexive_comp_top_inf inf_commute by auto also have "... ≤ p⇧^{T}* p * y" by (metis inf.cobounded2 inf.sup_monoid.add_commute mult_left_isotone one_inf_conv) also have "... ≤ y" using 1 find_set_invariant_def find_set_precondition_def mult_left_isotone by fastforce finally have 4: "p * y ≤ y ⊔ -roots p" using 1 by (metis find_set_invariant_def shunting_p bijective_regular) have "p * -roots p ≤ -roots p" using 1 by (metis find_set_invariant_def find_set_precondition_def conv_complement_sub_leq conv_involutive roots_successor_loop) hence "p * y ⊔ p * -roots p ≤ y ⊔ -roots p" using 4 dual_order.trans le_supI sup_ge2 by blast hence "p * (y ⊔ -roots p) ≤ y ⊔ -roots p" by (simp add: mult_left_dist_sup) hence "p⇧^{⋆}* y ≤ y ⊔ -roots p" by (simp add: star_left_induct) hence "p⇧^{T}⇧^{⋆}* x ≤ y ⊔ -roots p" using 3 dual_order.trans by blast thus "root p x ≤ y" using 1 by (metis find_set_invariant_def shunting_p bijective_regular) qed qed qed theorem find_set: "VARS y [ find_set_precondition p x ] y := x; WHILE y ≠ p[[y]] INV { find_set_invariant p x y } VAR { (p⇧^{T}⇧^{⋆}* y)↓ } DO y := p[[y]] OD [ find_set_postcondition p x y ]" apply vcg_tc_simp apply (fact find_set_1) apply (fact find_set_2) by (fact find_set_3) lemma find_set_exists: "find_set_precondition p x ⟹ ∃y . find_set_postcondition p x y" using tc_extract_function find_set by blast text ‹ The root of a component tree is a point, that is, represents a singleton set of nodes. This could be proved from the definitions using Kleene-relation algebraic calculations. But they can be avoided because the property directly follows from the postcondition of the previous correctness proof. The corresponding algorithm shows how to obtain the root. We therefore have an essentially constructive proof of the following result. › lemma root_point: "disjoint_set_forest p ⟹ point x ⟹ point (root p x)" using find_set_exists find_set_precondition_def find_set_postcondition_def by simp definition "find_set p x ≡ (SOME y . find_set_postcondition p x y)" lemma find_set_function: assumes "find_set_precondition p x" and "y = find_set p x" shows "find_set_postcondition p x y" by (metis assms find_set_def find_set_exists someI) subsection ‹Path Compression› text ‹ The path-compression technique is frequently implemented in recursive implementations of find-set modifying the tree on the way out from recursive calls. Here we implement it using a second while-loop, which iterates over the same path to the root and changes edges to point to the root of the component, which is known after the while-loop in find-set completes. We prove that path compression preserves the equivalence-relational semantics of the disjoint-set forest and also preserves the roots of the component trees. Additionally we prove the exact effect of path compression. › definition "path_compression_precondition p x y ≡ disjoint_set_forest p ∧ point x ∧ point y ∧ y = root p x" definition "path_compression_invariant p x y p0 w ≡ path_compression_precondition p x y ∧ point w ∧ p ⊓ 1 = p0 ⊓ 1 ∧ fc p = fc p0 ∧ root p w = y ∧ p0[p0⇧^{T}⇧^{⋆}* x - p0⇧^{T}⇧^{⋆}* w⟼y] = p ∧ disjoint_set_forest p0 ∧ w ≤ p0⇧^{T}⇧^{⋆}* x" definition "path_compression_postcondition p x y p0 ≡ disjoint_set_forest p ∧ y = root p x ∧ p ⊓ 1 = p0 ⊓ 1 ∧ fc p = fc p0 ∧ p0[p0⇧^{T}⇧^{⋆}* x⟼y] = p" text ‹ We first consider a variant that achieves the effect as a single update. The parents of all nodes reachable from x are simultaneously updated to the root of the component of x. › lemma path_compression_exact: assumes "path_compression_precondition p0 x y" and "p0[p0⇧^{T}⇧^{⋆}* x⟼y] = p" shows "p ⊓ 1 = p0 ⊓ 1" "fc p = fc p0" proof - have a1: "disjoint_set_forest p0" and a2: "point x" and a3: "point y" and a4: "y = root p0 x" using path_compression_precondition_def assms(1) by auto have 1: "regular (p0⇧^{T}⇧^{⋆}* x)" using a1 a2 bijective_regular mapping_regular regular_closed_star regular_conv_closed regular_mult_closed by auto have "p ⊓ 1 = (p0⇧^{T}⇧^{⋆}* x ⊓ y⇧^{T}⊓ 1) ⊔ (-(p0⇧^{T}⇧^{⋆}* x) ⊓ p0 ⊓ 1)" using assms(2) inf_sup_distrib2 by auto also have "... = (p0⇧^{T}⇧^{⋆}* x ⊓ p0 ⊓ 1) ⊔ (-(p0⇧^{T}⇧^{⋆}* x) ⊓ p0 ⊓ 1)" proof - have "p0⇧^{T}⇧^{⋆}* x ⊓ y⇧^{T}⊓ 1 = p0⇧^{T}⇧^{⋆}* x ⊓ p0 ⊓ 1" proof (rule order.antisym) have "(p0 ⊓ 1) * p0⇧^{T}⇧^{⋆}* x ⊓ 1 ≤ p0" by (smt coreflexive_comp_top_inf_one inf.absorb_iff2 inf.cobounded2 inf.sup_monoid.add_assoc root_var) hence "p0⇧^{T}⇧^{⋆}* x ⊓ y⇧^{T}⊓ 1 ≤ p0" by (metis inf_le1 a4 conv_dist_inf coreflexive_symmetric inf.absorb2 inf.cobounded2 inf.sup_monoid.add_assoc root_var symmetric_one_closed) thus "p0⇧^{T}⇧^{⋆}* x ⊓ y⇧^{T}⊓ 1 ≤ p0⇧^{T}⇧^{⋆}* x ⊓ p0 ⊓ 1" by (meson inf.le_sup_iff order.refl) have "p0⇧^{T}⇧^{⋆}* x ⊓ p0 ⊓ 1 ≤ y" by (metis a4 coreflexive_comp_top_inf_one inf.cobounded1 inf_assoc inf_le2) thus "p0⇧^{T}⇧^{⋆}* x ⊓ p0 ⊓ 1 ≤ p0⇧^{T}⇧^{⋆}* x ⊓ y⇧^{T}⊓ 1" by (smt conv_dist_inf coreflexive_symmetric inf.absorb_iff2 inf.cobounded2 inf.sup_monoid.add_assoc) qed thus ?thesis by simp qed also have "... = p0 ⊓ 1" using 1 by (metis inf.sup_monoid.add_commute inf_sup_distrib1 maddux_3_11_pp) finally show "p ⊓ 1 = p0 ⊓ 1" . show "fc p = fc p0" proof (rule order.antisym) have 2: "univalent (p0[p0⇧^{T}⇧^{⋆}* x⟼y])" by (simp add: a1 a2 a3 update_univalent mult_assoc) have 3: "-(p0⇧^{T}⇧^{⋆}* x) ⊓ p0 ≤ (p0[p0⇧^{T}⇧^{⋆}* x⟼y])⇧^{⋆}* (p0[p0⇧^{T}⇧^{⋆}* x⟼y])⇧^{T}⇧^{⋆}" using fc_increasing inf.order_trans sup.cobounded2 by blast have "p0⇧^{T}⇧^{⋆}* x ⊓ p0 ≤ (p0⇧^{T}⇧^{⋆}⊓ p0 * x⇧^{T}) * (x ⊓ p0⇧^{⋆}* p0)" by (metis conv_involutive conv_star_commute dedekind) also have "... ≤ p0⇧^{T}⇧^{⋆}* x ⊓ p0 * x⇧^{T}* p0⇧^{⋆}* p0" by (metis comp_associative inf.boundedI inf.cobounded2 inf_le1 mult_isotone) also have "... ≤ p0⇧^{T}⇧^{⋆}* x ⊓ top * x⇧^{T}* p0⇧^{⋆}" using comp_associative comp_inf.mult_right_isotone mult_isotone star.right_plus_below_circ by auto also have "... = p0⇧^{T}⇧^{⋆}* x * x⇧^{T}* p0⇧^{⋆}" by (metis a2 symmetric_top_closed vector_covector vector_inf_comp vector_mult_closed) also have "... ≤ (p0⇧^{T}⇧^{⋆}* x * y⇧^{T}) * (y * x⇧^{T}* p0⇧^{⋆})" by (metis a3 order.antisym comp_inf.top_right_mult_increasing conv_involutive dedekind_1 inf.sup_left_divisibility inf.sup_monoid.add_commute mult_right_isotone surjective_conv_total mult_assoc) also have "... = (p0⇧^{T}⇧^{⋆}* x ⊓ y⇧^{T}) * (y ⊓ x⇧^{T}* p0⇧^{⋆})" by (metis a2 a3 vector_covector vector_inf_comp vector_mult_closed) also have "... = (p0⇧^{T}⇧^{⋆}* x ⊓ y⇧^{T}) * (p0⇧^{T}⇧^{⋆}* x ⊓ y⇧^{T})⇧^{T}" by (simp add: conv_dist_comp conv_dist_inf conv_star_commute inf_commute) also have "... ≤ (p0[p0⇧^{T}⇧^{⋆}* x⟼y])⇧^{⋆}* (p0[p0⇧^{T}⇧^{⋆}* x⟼y])⇧^{T}⇧^{⋆}" by (meson conv_isotone dual_order.trans mult_isotone star.circ_increasing sup.cobounded1) finally have "p0⇧^{T}⇧^{⋆}* x ⊓ p0 ≤ (p0[p0⇧^{T}⇧^{⋆}* x⟼y])⇧^{⋆}* (p0[p0⇧^{T}⇧^{⋆}* x⟼y])⇧^{T}⇧^{⋆}" . hence "(p0⇧^{T}⇧^{⋆}* x ⊓ p0) ⊔ (-(p0⇧^{T}⇧^{⋆}* x) ⊓ p0) ≤ (p0[p0⇧^{T}⇧^{⋆}* x⟼y])⇧^{⋆}* (p0[p0⇧^{T}⇧^{⋆}* x⟼y])⇧^{T}⇧^{⋆}" using 3 le_supI by blast hence "p0 ≤ (p0[p0⇧^{T}⇧^{⋆}* x⟼y])⇧^{⋆}* (p0[p0⇧^{T}⇧^{⋆}* x⟼y])⇧^{T}⇧^{⋆}" using 1 by (metis inf_commute maddux_3_11_pp) hence "fc p0 ≤ (p0[p0⇧^{T}⇧^{⋆}* x⟼y])⇧^{⋆}* (p0[p0⇧^{T}⇧^{⋆}* x⟼y])⇧^{T}⇧^{⋆}" using 2 fc_idempotent fc_isotone by fastforce thus "fc p0 ≤ fc p" by (simp add: assms(2)) have "((p0⇧^{T}⇧^{⋆}* x ⊓ y⇧^{T}) ⊔ (-(p0⇧^{T}⇧^{⋆}* x) ⊓ p0))⇧^{⋆}= (-(p0⇧^{T}⇧^{⋆}* x) ⊓ p0)⇧^{⋆}* ((p0⇧^{T}⇧^{⋆}* x ⊓ y⇧^{T}) ⊔ 1)" proof (rule star_sup_2) have 4: "transitive (p0⇧^{T}⇧^{⋆}* x)" using a2 comp_associative mult_right_isotone rectangle_star_rectangle by auto have "transitive (y⇧^{T})" by (metis a3 conv_dist_comp inf.eq_refl mult_assoc) thus "transitive (p0⇧^{T}⇧^{⋆}* x ⊓ y⇧^{T})" using 4 transitive_inf_closed by auto have 5: "p0⇧^{T}⇧^{⋆}* x * (-(p0⇧^{T}⇧^{⋆}* x) ⊓ p0) ≤ p0⇧^{T}⇧^{⋆}* x" by (metis a2 mult_right_isotone top_greatest mult_assoc) have "(-(p0⇧^{T}⇧^{⋆}* x) ⊓ p0)⇧^{T}* y ≤ p0⇧^{T}* y" by (simp add: conv_dist_inf mult_left_isotone) also have "... ≤ y" using a1 a4 root_successor_loop by auto finally have "y⇧^{T}* (-(p0⇧^{T}⇧^{⋆}* x) ⊓ p0) ≤ y⇧^{T}" using conv_dist_comp conv_isotone by fastforce thus "(p0⇧^{T}⇧^{⋆}* x ⊓ y⇧^{T}) * (-(p0⇧^{T}⇧^{⋆}* x) ⊓ p0) ≤ p0⇧^{T}⇧^{⋆}* x ⊓ y⇧^{T}" using 5 comp_left_subdist_inf inf_mono order_trans by blast qed hence "p⇧^{⋆}= (-(p0⇧^{T}⇧^{⋆}* x) ⊓ p0)⇧^{⋆}* ((p0⇧^{T}⇧^{⋆}* x ⊓ y⇧^{T}) ⊔ 1)" by (simp add: assms(2)) also have "... ≤ p0⇧^{⋆}* ((p0⇧^{T}⇧^{⋆}* x ⊓ y⇧^{T}) ⊔ 1)" by (simp add: mult_left_isotone star_isotone) also have "... = p0⇧^{⋆}* (p0⇧^{T}⇧^{⋆}* x * y⇧^{T}⊔ 1)" by (simp add: a2 a3 vector_covector vector_mult_closed) also have "... = p0⇧^{⋆}* (p0⇧^{T}⇧^{⋆}* (x * x⇧^{T}) * p0⇧^{⋆}* (p0 ⊓ 1) ⊔ 1)" by (metis a4 coreflexive_symmetric inf.cobounded2 root_var comp_associative conv_dist_comp conv_involutive conv_star_commute) also have "... ≤ p0⇧^{⋆}* (p0⇧^{T}⇧^{⋆}* 1 * p0⇧^{⋆}* (p0 ⊓ 1) ⊔ 1)" by (metis a2 mult_left_isotone mult_right_isotone semiring.add_left_mono sup_commute) also have "... = p0⇧^{⋆}* (p0⇧^{T}⇧^{⋆}* (p0 ⊓ 1) ⊔ p0⇧^{⋆}* (p0 ⊓ 1) ⊔ 1)" by (simp add: a1 cancel_separate_eq mult_right_dist_sup) also have "... = p0⇧^{⋆}* ((p0 ⊓ 1) ⊔ p0⇧^{⋆}* (p0 ⊓ 1) ⊔ 1)" by (smt univalent_root_successors a1 conv_dist_comp conv_dist_inf coreflexive_idempotent coreflexive_symmetric inf.cobounded2 injective_codomain loop_root root_transitive_successor_loop symmetric_one_closed) also have "... = p0⇧^{⋆}* (p0⇧^{⋆}* (p0 ⊓ 1) ⊔ 1)" by (metis inf.sup_left_divisibility inf_commute sup.left_idem sup_commute sup_relative_same_increasing) also have "... ≤ p0⇧^{⋆}* p0⇧^{⋆}" by (metis inf.cobounded2 inf_commute order.refl order_lesseq_imp star.circ_mult_upper_bound star.circ_reflexive star.circ_transitive_equal sup.boundedI sup_monoid.add_commute) also have "... = p0⇧^{⋆}" by (simp add: star.circ_transitive_equal) finally show "fc p ≤ fc p0" by (metis conv_order conv_star_commute mult_isotone) qed qed lemma update_acyclic_6: assumes "disjoint_set_forest p" and "point x" shows "acyclic ((p[p⇧^{T}⇧^{⋆}*x⟼root p x]) - 1)" using assms root_point root_successor_loop update_acyclic_2 by auto theorem path_compression_assign: "VARS p [ path_compression_precondition p x y ∧ p0 = p ] p[p⇧^{T}⇧^{⋆}* x] := y [ path_compression_postcondition p x y p0 ]" apply vcg_tc_simp apply (unfold path_compression_precondition_def path_compression_postcondition_def) apply (intro conjI) subgoal using update_univalent mult_assoc by auto subgoal using bijective_regular mapping_regular regular_closed_star regular_conv_closed regular_mult_closed update_mapping mult_assoc by auto subgoal using update_acyclic_6 by blast subgoal by (smt same_root path_compression_exact path_compression_precondition_def update_univalent vector_mult_closed) subgoal using path_compression_exact(1) path_compression_precondition_def by blast subgoal using path_compression_exact(2) path_compression_precondition_def by blast by blast text ‹ We next look at implementing these updates using a loop. › lemma path_compression_1a: assumes "point x" and "disjoint_set_forest p" and "x ≠ root p x" shows "p⇧^{T}⇧^{+}* x ≤ - x" by (meson assms bijective_regular mapping_regular regular_closed_star regular_conv_closed regular_mult_closed vector_mult_closed point_in_vector_or_complement_2 loop_root_2) lemma path_compression_1b: "x ≤ p