(* Title: More on Disjoint-Set Forests Author: Walter Guttmann Maintainer: Walter Guttmann <walter.guttmann at canterbury.ac.nz> *) theory More_Disjoint_Set_Forests imports Disjoint_Set_Forests begin section ‹More on Array Access and Disjoint-Set Forests› text ‹ This section contains further results about directed acyclic graphs and relational array operations. › context stone_relation_algebra begin lemma update_square: assumes "point y" shows "x[y⟼x[[x[[y]]]]] ≤ x * x ⊔ x" proof - have "x[y⟼x[[x[[y]]]]] = (y ⊓ y⇧^{T}* x * x) ⊔ (-y ⊓ x)" by (simp add: conv_dist_comp) also have "... ≤ (y ⊓ y⇧^{T}) * x * x ⊔ x" by (smt assms inf.eq_refl inf.sup_monoid.add_commute inf_le1 sup_mono vector_inf_comp) also have "... ≤ x * x ⊔ x" by (smt (z3) assms comp_associative conv_dist_comp coreflexive_comp_top_inf inf.cobounded2 sup_left_isotone symmetric_top_closed) finally show ?thesis . qed lemma update_ub: "x[y⟼z] ≤ x ⊔ z⇧^{T}" by (meson dual_order.trans inf.cobounded2 le_supI sup.cobounded1 sup_ge2) lemma update_square_ub: "x[y⟼(x * x)⇧^{T}] ≤ x ⊔ x * x" by (metis conv_involutive update_ub) lemma update_same_sub: assumes "u ⊓ x = u ⊓ z" and "y ≤ u" and "regular y" shows "x[y⟼z⇧^{T}] = x" by (smt (z3) assms conv_involutive inf.sup_monoid.add_commute inf.sup_relative_same_increasing maddux_3_11_pp) lemma update_point_get: "point y ⟹ x[y⟼z[[y]]] = x[y⟼z⇧^{T}]" by (metis conv_involutive get_put inf_commute update_inf_same) lemma update_bot: "x[bot⟼z] = x" by simp lemma update_top: "x[top⟼z] = z⇧^{T}" by simp lemma update_same: assumes "regular u" shows "(x[y⟼z])[u⟼z] = x[y ⊔ u⟼z]" proof - have "(x[y⟼z])[u⟼z] = (u ⊓ z⇧^{T}) ⊔ (-u ⊓ y ⊓ z⇧^{T}) ⊔ (-u ⊓ -y ⊓ x)" using inf.sup_monoid.add_assoc inf_sup_distrib1 sup_assoc by force also have "... = (u ⊓ z⇧^{T}) ⊔ (y ⊓ z⇧^{T}) ⊔ (-(u ⊔ y) ⊓ x)" by (metis assms inf_sup_distrib2 maddux_3_21_pp p_dist_sup) also have "... = x[y ⊔ u⟼z]" using comp_inf.mult_right_dist_sup sup_commute by auto finally show ?thesis . qed lemma update_same_3: assumes "regular u" and "regular v" shows "((x[y⟼z])[u⟼z])[v⟼z] = x[y ⊔ u ⊔ v⟼z]" by (metis assms update_same) lemma update_split: assumes "regular w" shows "x[y⟼z] = (x[y - w⟼z])[y ⊓ w⟼z]" by (smt (z3) assms comp_inf.semiring.distrib_left inf.left_commute inf.sup_monoid.add_commute inf_import_p maddux_3_11_pp maddux_3_12 p_dist_inf sup_assoc) lemma update_injective_swap: assumes "injective x" and "point y" and "injective z" and "vector z" shows "injective ((x[y⟼x[[z]]])[z⟼x[[y]]])" proof - have 1: "(z ⊓ y⇧^{T}* x) * (z ⊓ y⇧^{T}* x)⇧^{T}≤ 1" using assms(3) injective_inf_closed by auto have "(z ⊓ y⇧^{T}* x) * (-z ⊓ y ⊓ z⇧^{T}* x)⇧^{T}≤ (z ⊓ y⇧^{T}* x) * (y⇧^{T}⊓ x⇧^{T}* z)" by (metis conv_dist_comp conv_involutive conv_order inf.boundedE inf.boundedI inf.cobounded1 inf.cobounded2 mult_right_isotone) also have "... = (z ⊓ z⇧^{T}* x) * (y⇧^{T}⊓ x⇧^{T}* y)" by (smt (z3) assms(2,4) covector_inf_comp_3 inf.left_commute inf.sup_monoid.add_commute comp_associative conv_dist_comp conv_involutive) also have "... = (z ⊓ z⇧^{T}) * x * x⇧^{T}* (y ⊓ y⇧^{T})" by (smt (z3) assms(2,4) comp_associative inf.sup_monoid.add_commute vector_covector vector_inf_comp) also have "... ≤ x * x⇧^{T}" by (metis assms(2-4) comp_associative comp_right_one coreflexive_comp_top_inf inf.coboundedI2 mult_right_isotone vector_covector) also have "... ≤ 1" by (simp add: assms(1)) finally have 2: "(z ⊓ y⇧^{T}* x) * (-z ⊓ y ⊓ z⇧^{T}* x)⇧^{T}≤ 1" . have "(z ⊓ y⇧^{T}* x) * (-z ⊓ -y ⊓ x)⇧^{T}≤ y⇧^{T}* x * (-y⇧^{T}⊓ x⇧^{T})" by (smt comp_isotone conv_complement conv_dist_inf inf.cobounded2 inf.sup_monoid.add_assoc) also have "... = y⇧^{T}* x * x⇧^{T}⊓ -y⇧^{T}" by (simp add: inf.commute assms(2) covector_comp_inf vector_conv_compl) also have "... ≤ y⇧^{T}⊓ -y⇧^{T}" by (metis assms(1) comp_associative comp_inf.mult_left_isotone comp_isotone comp_right_one mult_sub_right_one) finally have 3: "(z ⊓ y⇧^{T}* x) * (-z ⊓ -y ⊓ x)⇧^{T}≤ 1" using pseudo_complement by fastforce have 4: "(-z ⊓ y ⊓ z⇧^{T}* x) * (z ⊓ y⇧^{T}* x)⇧^{T}≤ 1" using 2 conv_dist_comp conv_order by force have 5: "(-z ⊓ y ⊓ z⇧^{T}* x) * (-z ⊓ y ⊓ z⇧^{T}* x)⇧^{T}≤ 1" by (simp add: assms(2) inf_assoc inf_left_commute injective_inf_closed) have "(-z ⊓ y ⊓ z⇧^{T}* x) * (-z ⊓ -y ⊓ x)⇧^{T}≤ z⇧^{T}* x * (-z⇧^{T}⊓ x⇧^{T})" using comp_inf.mult_left_isotone comp_isotone conv_complement conv_dist_inf inf.cobounded1 inf.cobounded2 by auto also have "... = z⇧^{T}* x * x⇧^{T}⊓ -z⇧^{T}" by (metis assms(4) covector_comp_inf inf.sup_monoid.add_commute vector_conv_compl) also have "... ≤ z⇧^{T}⊓ -z⇧^{T}" by (metis assms(1) comp_associative comp_inf.mult_left_isotone comp_isotone comp_right_one mult_sub_right_one) finally have 6: "(-z ⊓ y ⊓ z⇧^{T}* x) * (-z ⊓ -y ⊓ x)⇧^{T}≤ 1" using pseudo_complement by fastforce have 7: "(-z ⊓ -y ⊓ x) * (z ⊓ y⇧^{T}* x)⇧^{T}≤ 1" using 3 conv_dist_comp coreflexive_symmetric by fastforce have 8: "(-z ⊓ -y ⊓ x) * (-z ⊓ y ⊓ z⇧^{T}* x)⇧^{T}≤ 1" using 6 conv_dist_comp coreflexive_symmetric by fastforce have 9: "(-z ⊓ -y ⊓ x) * (-z ⊓ -y ⊓ x)⇧^{T}≤ 1" using assms(1) inf.sup_monoid.add_commute injective_inf_closed by auto have "(x[y⟼x[[z]]])[z⟼x[[y]]] = (z ⊓ y⇧^{T}* x) ⊔ (-z ⊓ y ⊓ z⇧^{T}* x) ⊔ (-z ⊓ -y ⊓ x)" by (simp add: comp_inf.comp_left_dist_sup conv_dist_comp inf_assoc sup_monoid.add_assoc) hence "((x[y⟼x[[z]]])[z⟼x[[y]]]) * ((x[y⟼x[[z]]])[z⟼x[[y]]])⇧^{T}= ((z ⊓ y⇧^{T}* x) ⊔ (-z ⊓ y ⊓ z⇧^{T}* x) ⊔ (-z ⊓ -y ⊓ x)) * ((z ⊓ y⇧^{T}* x)⇧^{T}⊔ (-z ⊓ y ⊓ z⇧^{T}* x)⇧^{T}⊔ (-z ⊓ -y ⊓ x)⇧^{T})" by (simp add: conv_dist_sup) also have "... = (z ⊓ y⇧^{T}* x) * ((z ⊓ y⇧^{T}* x)⇧^{T}⊔ (-z ⊓ y ⊓ z⇧^{T}* x)⇧^{T}⊔ (-z ⊓ -y ⊓ x)⇧^{T}) ⊔ (-z ⊓ y ⊓ z⇧^{T}* x) * ((z ⊓ y⇧^{T}* x)⇧^{T}⊔ (-z ⊓ y ⊓ z⇧^{T}* x)⇧^{T}⊔ (-z ⊓ -y ⊓ x)⇧^{T}) ⊔ (-z ⊓ -y ⊓ x) * ((z ⊓ y⇧^{T}* x)⇧^{T}⊔ (-z ⊓ y ⊓ z⇧^{T}* x)⇧^{T}⊔ (-z ⊓ -y ⊓ x)⇧^{T})" using mult_right_dist_sup by auto also have "... = (z ⊓ y⇧^{T}* x) * (z ⊓ y⇧^{T}* x)⇧^{T}⊔ (z ⊓ y⇧^{T}* x) * (-z ⊓ y ⊓ z⇧^{T}* x)⇧^{T}⊔ (z ⊓ y⇧^{T}* x) * (-z ⊓ -y ⊓ x)⇧^{T}⊔ (-z ⊓ y ⊓ z⇧^{T}* x) * (z ⊓ y⇧^{T}* x)⇧^{T}⊔ (-z ⊓ y ⊓ z⇧^{T}* x) * (-z ⊓ y ⊓ z⇧^{T}* x)⇧^{T}⊔ (-z ⊓ y ⊓ z⇧^{T}* x) * (-z ⊓ -y ⊓ x)⇧^{T}⊔ (-z ⊓ -y ⊓ x) * (z ⊓ y⇧^{T}* x)⇧^{T}⊔ (-z ⊓ -y ⊓ x) * (-z ⊓ y ⊓ z⇧^{T}* x)⇧^{T}⊔ (-z ⊓ -y ⊓ x) * (-z ⊓ -y ⊓ x)⇧^{T}" using mult_left_dist_sup sup.left_commute sup_commute by auto also have "... ≤ 1" using 1 2 3 4 5 6 7 8 9 by simp_all finally show ?thesis . qed lemma update_injective_swap_2: assumes "injective x" shows "injective ((x[y⟼x[[bot]]])[bot⟼x[[y]]])" by (simp add: assms inf.sup_monoid.add_commute injective_inf_closed) lemma update_univalent_swap: assumes "univalent x" and "injective y" and "vector y" and "injective z" and "vector z" shows "univalent ((x[y⟼x[[z]]])[z⟼x[[y]]])" by (simp add: assms read_injective update_univalent) lemma update_mapping_swap: assumes "mapping x" and "point y" and "point z" shows "mapping ((x[y⟼x[[z]]])[z⟼x[[y]]])" by (simp add: assms bijective_regular read_injective read_surjective update_total update_univalent) text ‹lemma ‹mapping_inf_point_arc› has been moved to theory ‹Relation_Algebras› in entry ‹Stone_Relation_Algebras›› end context stone_kleene_relation_algebra begin lemma omit_redundant_points_2: assumes "point p" shows "p ⊓ x⇧^{⋆}= (p ⊓ 1) ⊔ (p ⊓ x ⊓ -p⇧^{T}) * (x ⊓ -p⇧^{T})⇧^{⋆}" proof - let ?p = "p ⊓ 1" let ?np = "-p ⊓ 1" have 1: "p ⊓ x⇧^{⋆}⊓ 1 = p ⊓ 1" by (metis inf.le_iff_sup inf.left_commute inf.sup_monoid.add_commute star.circ_reflexive) have 2: "p ⊓ 1 ⊓ -p⇧^{T}= bot" by (smt (z3) inf_bot_right inf_commute inf_left_commute one_inf_conv p_inf) have "p ⊓ x⇧^{⋆}⊓ -1 = p ⊓ x⇧^{⋆}⊓ -p⇧^{T}" by (metis assms antisymmetric_inf_diversity inf.cobounded1 inf.sup_relative_same_increasing vector_covector) also have "... = (p ⊓ 1 ⊓ -p⇧^{T}) ⊔ ((p ⊓ x) * (-p ⊓ x)⇧^{⋆}⊓ -p⇧^{T})" by (simp add: assms omit_redundant_points comp_inf.semiring.distrib_right) also have "... = (p ⊓ x) * (-p ⊓ x)⇧^{⋆}⊓ -p⇧^{T}" using 2 by simp also have "... = ?p * x * (-p ⊓ x)⇧^{⋆}⊓ -p⇧^{T}" by (metis assms vector_export_comp_unit) also have "... = ?p * x * (?np * x)⇧^{⋆}⊓ -p⇧^{T}" by (metis assms vector_complement_closed vector_export_comp_unit) also have "... = ?p * x * (?np * x)⇧^{⋆}* ?np" by (metis assms conv_complement covector_comp_inf inf.sup_monoid.add_commute mult_1_right one_inf_conv vector_conv_compl) also have "... = ?p * x * ?np * (x * ?np)⇧^{⋆}" using star_slide mult_assoc by auto also have "... = (?p * x ⊓ -p⇧^{T}) * (x * ?np)⇧^{⋆}" by (metis assms conv_complement covector_comp_inf inf.sup_monoid.add_commute mult_1_right one_inf_conv vector_conv_compl) also have "... = (?p * x ⊓ -p⇧^{T}) * (x ⊓ -p⇧^{T})⇧^{⋆}" by (metis assms conv_complement covector_comp_inf inf.sup_monoid.add_commute mult_1_right one_inf_conv vector_conv_compl) also have "... = (p ⊓ x ⊓ -p⇧^{T}) * (x ⊓ -p⇧^{T})⇧^{⋆}" by (metis assms vector_export_comp_unit) finally show ?thesis using 1 by (metis maddux_3_11_pp regular_one_closed) qed lemma omit_redundant_points_3: assumes "point p" shows "p ⊓ x⇧^{⋆}= (p ⊓ 1) ⊔ (p ⊓ (x ⊓ -p⇧^{T})⇧^{+})" by (simp add: assms inf_assoc vector_inf_comp omit_redundant_points_2) lemma even_odd_root: assumes "acyclic (x - 1)" and "regular x" and "univalent x" shows "(x * x)⇧^{T}⇧^{⋆}⊓ x⇧^{T}* (x * x)⇧^{T}⇧^{⋆}= (1 ⊓ x) * ((x * x)⇧^{T}⇧^{⋆}⊓ x⇧^{T}* (x * x)⇧^{T}⇧^{⋆})" proof - have 1: "univalent (x * x)" by (simp add: assms(3) univalent_mult_closed) have "x ⊓ 1 ≤ top * (x ⊓ 1)" by (simp add: top_left_mult_increasing) hence "x ⊓ -(top * (x ⊓ 1)) ≤ x - 1" using assms(2) p_shunting_swap pp_dist_comp by auto hence "x⇧^{⋆}* (x ⊓ -(top * (x ⊓ 1))) ≤ (x - 1)⇧^{⋆}* (x - 1)" using mult_right_isotone reachable_without_loops by auto also have "... ≤ -1" by (simp add: assms(1) star_plus) finally have "(x ⊓ -(top * (x ⊓ 1)))⇧^{T}≤ -x⇧^{⋆}" using schroeder_4_p by force hence "x⇧^{T}⊓ x⇧^{⋆}≤ (top * (x ⊓ 1))⇧^{T}" by (smt (z3) assms(2) conv_complement conv_dist_inf p_shunting_swap regular_closed_inf regular_closed_top regular_mult_closed regular_one_closed) also have "... = (1 ⊓ x) * top" by (metis conv_dist_comp conv_dist_inf inf_commute one_inf_conv symmetric_one_closed symmetric_top_closed) finally have 2: "(x⇧^{T}⊓ x⇧^{⋆}) * top ≤ (1 ⊓ x) * top" by (metis inf.orderE inf.orderI inf_commute inf_vector_comp) have "1 ⊓ x⇧^{T}⇧^{+}≤ (x⇧^{T}⊓ 1 * x⇧^{⋆}) * x⇧^{T}⇧^{⋆}" by (metis conv_involutive conv_star_commute dedekind_2 inf_commute) also have "... ≤ (x⇧^{T}⊓ x⇧^{⋆}) * top" by (simp add: mult_right_isotone) also have "... ≤ (1 ⊓ x) * top" using 2 by simp finally have 3: "1 ⊓ x⇧^{T}⇧^{+}≤ (1 ⊓ x) * top" . have "x⇧^{T}⊓ (x⇧^{T}* x⇧^{T})⇧^{+}= 1 * x⇧^{T}⊓ (x⇧^{T}* x⇧^{T})⇧^{⋆}* x⇧^{T}* x⇧^{T}" using star_plus mult_assoc by auto also have "... = (1 ⊓ (x⇧^{T}* x⇧^{T})⇧^{⋆}* x⇧^{T}) * x⇧^{T}" using assms(3) injective_comp_right_dist_inf by force also have "... ≤ (1 ⊓ x⇧^{T}⇧^{⋆}* x⇧^{T}) * x⇧^{T}" by (meson comp_inf.mult_right_isotone comp_isotone inf.eq_refl star.circ_square) also have "... ≤ (1 ⊓ x) * top * x⇧^{T}" using 3 by (simp add: mult_left_isotone star_plus) also have "... ≤ (1 ⊓ x) * top" by (simp add: comp_associative mult_right_isotone) finally have 4: "x⇧^{T}⊓ (x⇧^{T}* x⇧^{T})⇧^{+}≤ (1 ⊓ x) * top" . have "x⇧^{T}⊓ (x⇧^{T}* x⇧^{T})⇧^{⋆}= (x⇧^{T}⊓ 1) ⊔ (x⇧^{T}⊓ (x⇧^{T}* x⇧^{T})⇧^{+})" by (metis inf_sup_distrib1 star_left_unfold_equal) also have "... ≤ (1 ⊓ x) * top" using 4 by (metis inf.sup_monoid.add_commute le_supI one_inf_conv top_right_mult_increasing) finally have 4: "x⇧^{T}⊓ (x⇧^{T}* x⇧^{T})⇧^{⋆}≤ (1 ⊓ x) * top" . have "x⇧^{T}⊓ (x * x)⇧^{⋆}⊓ -1 ≤ x⇧^{T}⊓ x⇧^{⋆}⊓ -1" by (simp add: inf.coboundedI2 inf.sup_monoid.add_commute star.circ_square) also have "... = (x - 1)⇧^{⋆}⊓ (x - 1)⇧^{T}" using conv_complement conv_dist_inf inf_assoc inf_left_commute reachable_without_loops symmetric_one_closed by auto also have "... = bot" using assms(1) acyclic_star_below_complement_1 by auto finally have 5: "x⇧^{T}⊓ (x * x)⇧^{⋆}⊓ -1 = bot" by (simp add: le_bot) have "x⇧^{T}⊓ (x * x)⇧^{⋆}= (x⇧^{T}⊓ (x * x)⇧^{⋆}⊓ 1) ⊔ (x⇧^{T}⊓ (x * x)⇧^{⋆}⊓ -1)" by (metis maddux_3_11_pp regular_one_closed) also have "... = x⇧^{T}⊓ (x * x)⇧^{⋆}⊓ 1" using 5 by simp also have "... = x⇧^{T}⊓ 1" by (metis calculation comp_inf.semiring.distrib_left inf.sup_monoid.add_commute star.circ_transitive_equal star_involutive star_left_unfold_equal sup_inf_absorb) finally have "(x⇧^{T}⊓ (x * x)⇧^{⋆}) ⊔ (x⇧^{T}⊓ (x⇧^{T}* x⇧^{T})⇧^{⋆}) ≤ (1 ⊓ x) * top" using 4 inf.sup_monoid.add_commute one_inf_conv top_right_mult_increasing by auto hence "x⇧^{T}⊓ ((x * x)⇧^{⋆}⊔ (x * x)⇧^{T}⇧^{⋆}) ≤ (1 ⊓ x) * top" by (simp add: comp_inf.semiring.distrib_left conv_dist_comp) hence 6: "x⇧^{T}⊓ (x * x)⇧^{T}⇧^{⋆}* (x * x)⇧^{⋆}≤ (1 ⊓ x) * top" using 1 by (simp add: cancel_separate_eq sup_commute) have "(x * x)⇧^{T}⇧^{⋆}⊓ x⇧^{T}* (x * x)⇧^{T}⇧^{⋆}≤ (x⇧^{T}⊓ (x * x)⇧^{T}⇧^{⋆}* (x * x)⇧^{⋆}) * (x * x)⇧^{T}⇧^{⋆}" by (metis conv_involutive conv_star_commute dedekind_2 inf_commute) also have "... ≤ (1 ⊓ x) * top * (x * x)⇧^{T}⇧^{⋆}" using 6 by (simp add: mult_left_isotone) also have "... = (1 ⊓ x) * top" by (simp add: comp_associative star.circ_left_top) finally have "(x * x)⇧^{T}⇧^{⋆}⊓ x⇧^{T}* (x * x)⇧^{T}⇧^{⋆}= (x * x)⇧^{T}⇧^{⋆}⊓ x⇧^{T}* (x * x)⇧^{T}⇧^{⋆}⊓ (1 ⊓ x) * top" using inf.order_iff by auto also have "... = (1 ⊓ x) * ((x * x)⇧^{T}⇧^{⋆}⊓ x⇧^{T}* (x * x)⇧^{T}⇧^{⋆})" by (metis coreflexive_comp_top_inf inf.cobounded1 inf.sup_monoid.add_commute) finally show ?thesis . qed lemma update_square_plus: "point y ⟹ x[y⟼x[[x[[y]]]]] ≤ x⇧^{+}" by (meson update_square comp_isotone dual_order.trans le_supI order_refl star.circ_increasing star.circ_mult_increasing) lemma update_square_ub_plus: "x[y⟼(x * x)⇧^{T}] ≤ x⇧^{+}" by (simp add: comp_isotone inf.coboundedI2 star.circ_increasing star.circ_mult_increasing) lemma acyclic_square: assumes "acyclic (x - 1)" shows "x * x ⊓ 1 = x ⊓ 1" proof (rule order.antisym) have "1 ⊓ x * x = 1 ⊓ ((x - 1) * x ⊔ (x ⊓ 1) * x)" by (metis maddux_3_11_pp regular_one_closed semiring.distrib_right) also have "... ≤ 1 ⊓ ((x - 1) * x ⊔ x)" by (metis inf.cobounded2 mult_1_left mult_left_isotone inf.sup_right_isotone semiring.add_left_mono) also have "... = 1 ⊓ ((x - 1) * (x - 1) ⊔ (x - 1) * (x ⊓ 1) ⊔ x)" by (metis maddux_3_11_pp mult_left_dist_sup regular_one_closed) also have "... ≤ (1 ⊓ (x - 1) * (x - 1)) ⊔ (x - 1) * (x ⊓ 1) ⊔ x" by (metis inf_le2 inf_sup_distrib1 semiring.add_left_mono sup_monoid.add_assoc) also have "... ≤ (1 ⊓ (x - 1)⇧^{+}) ⊔ (x - 1) * (x ⊓ 1) ⊔ x" by (metis comp_isotone inf.eq_refl inf.sup_right_isotone star.circ_increasing sup_monoid.add_commute sup_right_isotone) also have "... = (x - 1) * (x ⊓ 1) ⊔ x" by (metis assms inf.le_iff_sup inf.sup_monoid.add_commute inf_import_p inf_p regular_one_closed sup_inf_absorb sup_monoid.add_commute) also have "... = x" by (metis comp_isotone inf.cobounded1 inf_le2 mult_1_right sup.absorb2) finally show "x * x ⊓ 1 ≤ x ⊓ 1" by (simp add: inf.sup_monoid.add_commute) show "x ⊓ 1 ≤ x * x ⊓ 1" by (metis coreflexive_idempotent inf_le1 inf_le2 le_infI mult_isotone) qed lemma diagonal_update_square_aux: assumes "acyclic (x - 1)" and "point y" shows "1 ⊓ y ⊓ y⇧^{T}* x * x = 1 ⊓ y ⊓ x" proof - have 1: "1 ⊓ y ⊓ x ≤ y⇧^{T}* x * x" by (metis comp_isotone coreflexive_idempotent inf.boundedE inf.cobounded1 inf.cobounded2 one_inf_conv) have "1 ⊓ y ⊓ y⇧^{T}* x * x = 1 ⊓ (y ⊓ y⇧^{T}) * x * x" by (simp add: assms(2) inf.sup_monoid.add_assoc vector_inf_comp) also have "... = 1 ⊓ (y ⊓ 1) * x * x" by (metis assms(2) inf.cobounded1 inf.sup_monoid.add_commute inf.sup_same_context one_inf_conv vector_covector) also have "... ≤ 1 ⊓ x * x" by (metis comp_left_subdist_inf inf.sup_right_isotone le_infE mult_left_isotone mult_left_one) also have "... ≤ x" using assms(1) acyclic_square inf.sup_monoid.add_commute by auto finally show ?thesis using 1 by (metis inf.absorb2 inf.left_commute inf.sup_monoid.add_commute) qed lemma diagonal_update_square: assumes "acyclic (x - 1)" and "point y" shows "(x[y⟼x[[x[[y]]]]]) ⊓ 1 = x ⊓ 1" proof - let ?xy = "x[[y]]" let ?xxy = "x[[?xy]]" let ?xyxxy = "x[y⟼?xxy]" have "?xyxxy ⊓ 1 = ((y ⊓ y⇧^{T}* x * x) ⊔ (-y ⊓ x)) ⊓ 1" by (simp add: conv_dist_comp) also have "... = (y ⊓ y⇧^{T}* x * x ⊓ 1) ⊔ (-y ⊓ x ⊓ 1)" by (simp add: inf_sup_distrib2) also have "... = (y ⊓ x ⊓ 1) ⊔ (-y ⊓ x ⊓ 1)" using assms by (smt (verit, ccfv_threshold) diagonal_update_square_aux find_set_precondition_def inf_assoc inf_commute) also have "... = x ⊓ 1" by (metis assms(2) bijective_regular comp_inf.mult_right_dist_sup inf.sup_monoid.add_commute maddux_3_11_pp) finally show ?thesis . qed lemma fc_update_square: assumes "mapping x" and "point y" shows "fc (x[y⟼x[[x[[y]]]]]) = fc x" proof (rule order.antisym) let ?xy = "x[[y]]" let ?xxy = "x[[?xy]]" let ?xyxxy = "x[y⟼?xxy]" have 1: "y ⊓ y⇧^{T}* x * x ≤ x * x" by (smt (z3) assms(2) inf.cobounded2 inf.sup_monoid.add_commute inf.sup_same_context mult_1_left one_inf_conv vector_covector vector_inf_comp) have 2: "?xyxxy = (y ⊓ y⇧^{T}* x * x) ⊔ (-y ⊓ x)" by (simp add: conv_dist_comp) also have "... ≤ x * x ⊔ x" using 1 inf_le2 sup_mono by blast also have "... ≤ x⇧^{⋆}" by (simp add: star.circ_increasing star.circ_mult_upper_bound) finally show "fc ?xyxxy ≤ fc x" by (metis comp_isotone conv_order conv_star_commute star_involutive star_isotone) have 3: "y ⊓ x ⊓ 1 ≤ fc ?xyxxy" using inf.coboundedI1 inf.sup_monoid.add_commute reflexive_mult_closed star.circ_reflexive by auto have 4: "y - 1 ≤ -y⇧^{T}" using assms(2) p_shunting_swap regular_one_closed vector_covector by auto have "y ⊓ x ≤ y⇧^{T}* x" by (simp add: assms(2) vector_restrict_comp_conv) also have "... ≤ y⇧^{T}* x * x * x⇧^{T}" by (metis assms(1) comp_associative mult_1_right mult_right_isotone total_var) finally have "y ⊓ x ⊓ -1 ≤ y ⊓ -y⇧^{T}⊓ y⇧^{T}* x * x * x⇧^{T}" using 4 by (smt (z3) inf.cobounded1 inf.coboundedI2 inf.sup_monoid.add_assoc inf.sup_monoid.add_commute inf_greatest) also have "... = (y ⊓ y⇧^{T}* x * x) * x⇧^{T}⊓ -y⇧^{T}" by (metis assms(2) inf.sup_monoid.add_assoc inf.sup_monoid.add_commute vector_inf_comp) also have "... = (y ⊓ y⇧^{T}* x * x) * (x⇧^{T}⊓ -y⇧^{T})" using assms(2) covector_comp_inf vector_conv_compl by auto also have "... = (y ⊓ y⇧^{T}* x * x) * (-y ⊓ x)⇧^{T}" by (simp add: conv_complement conv_dist_inf inf_commute) also have "... ≤ ?xyxxy * (-y ⊓ x)⇧^{T}" using 2 by (simp add: comp_left_increasing_sup) also have "... ≤ ?xyxxy * ?xyxxy⇧^{T}" by (simp add: conv_isotone mult_right_isotone) also have "... ≤ fc ?xyxxy" using comp_isotone star.circ_increasing by blast finally have 5: "y ⊓ x ≤ fc ?xyxxy" using 3 by (smt (z3) comp_inf.semiring.distrib_left inf.le_iff_sup maddux_3_11_pp regular_one_closed) have "x = (y ⊓ x) ⊔ (-y ⊓ x)" by (metis assms(2) bijective_regular inf.sup_monoid.add_commute maddux_3_11_pp) also have "... ≤ fc ?xyxxy" using 5 dual_order.trans fc_increasing sup.cobounded2 sup_least by blast finally show "fc x ≤ fc ?xyxxy" by (smt (z3) assms fc_equivalence fc_isotone fc_wcc read_injective star.circ_decompose_9 star_decompose_1 update_univalent) qed lemma acyclic_plus_loop: assumes "acyclic (x - 1)" shows "x⇧^{+}⊓ 1 = x ⊓ 1" proof - let ?r = "x ⊓ 1" let ?i = "x - 1" have "x⇧^{+}⊓ 1 = (?i ⊔ ?r)⇧^{+}⊓ 1" by (metis maddux_3_11_pp regular_one_closed) also have "... = ((?i⇧^{⋆}* ?r)⇧^{⋆}* ?i⇧^{+}⊔ (?i⇧^{⋆}* ?r)⇧^{+}) ⊓ 1" using plus_sup by auto also have "... ≤ (?i⇧^{+}⊔ (?i⇧^{⋆}* ?r)⇧^{+}) ⊓ 1" by (metis comp_associative dual_order.eq_iff maddux_3_11_pp reachable_without_loops regular_one_closed star.circ_plus_same star.circ_sup_9) also have "... = (?i⇧^{⋆}* ?r)⇧^{+}⊓ 1" by (smt (z3) assms comp_inf.mult_right_dist_sup inf.absorb2 inf.sup_monoid.add_commute inf_le2 maddux_3_11_pp pseudo_complement regular_one_closed) also have "... ≤ ?i⇧^{⋆}* ?r ⊓ 1" by (metis comp_associative dual_order.eq_iff maddux_3_11_pp reachable_without_loops regular_one_closed star.circ_sup_9 star_slide) also have "... = (?r ⊔ ?i⇧^{+}* ?r) ⊓ 1" using comp_associative star.circ_loop_fixpoint sup_commute by force also have "... ≤ x ⊔ (?i⇧^{+}* ?r ⊓ 1)" by (metis comp_inf.mult_right_dist_sup inf.absorb1 inf.cobounded1 inf.cobounded2) also have "... ≤ x ⊔ (-1 * ?r ⊓ 1)" by (meson assms comp_inf.comp_isotone mult_left_isotone order.refl semiring.add_left_mono) also have "... = x" by (metis comp_inf.semiring.mult_not_zero comp_right_one inf.cobounded2 inf_sup_absorb mult_right_isotone pseudo_complement sup.idem sup_inf_distrib1) finally show ?thesis by (meson inf.sup_same_context inf_le1 order_trans star.circ_mult_increasing) qed lemma star_irreflexive_part_eq: "x⇧^{⋆}- 1 = (x - 1)⇧^{+}- 1" by (metis reachable_without_loops star_plus_without_loops) lemma star_irreflexive_part: "x⇧^{⋆}- 1 ≤ (x - 1)⇧^{+}" using star_irreflexive_part_eq by auto lemma square_irreflexive_part: "x * x - 1 ≤ (x - 1)⇧^{+}" proof - have "x * x = (x ⊓ 1) * x ⊔ (x - 1) * x" by (metis maddux_3_11_pp mult_right_dist_sup regular_one_closed) also have "... ≤ 1 * x ⊔ (x - 1) * x" using comp_isotone inf.cobounded2 semiring.add_right_mono by blast also have "... ≤ 1 ⊔ (x - 1) ⊔ (x - 1) * x" by (metis inf.cobounded2 maddux_3_11_pp mult_1_left regular_one_closed sup_left_isotone) also have "... = (x - 1) * (x ⊔ 1) ⊔ 1" by (simp add: mult_left_dist_sup sup_assoc sup_commute) finally have "x * x - 1 ≤ (x - 1) * (x ⊔ 1)" using shunting_var_p by auto also have "... = (x - 1) * (x - 1) ⊔ (x - 1)" by (metis comp_right_one inf.sup_monoid.add_commute maddux_3_21_pp mult_left_dist_sup regular_one_closed sup_commute) also have "... ≤ (x - 1)⇧^{+}" by (metis mult_left_isotone star.circ_increasing star.circ_mult_increasing star.circ_plus_same sup.bounded_iff) finally show ?thesis . qed lemma square_irreflexive_part_2: "x * x - 1 ≤ x⇧^{⋆}- 1" using comp_inf.mult_left_isotone star.circ_increasing star.circ_mult_upper_bound by blast lemma acyclic_update_square: assumes "acyclic (x - 1)" shows "acyclic ((x[y⟼(x * x)⇧^{T}]) - 1)" proof - have "((x[y⟼(x * x)⇧^{T}]) - 1)⇧^{+}≤ ((x ⊔ x * x) - 1)⇧^{+}" by (metis comp_inf.mult_right_isotone comp_isotone inf.sup_monoid.add_commute star_isotone update_square_ub) also have "... = ((x - 1) ⊔ (x * x - 1))⇧^{+}" using comp_inf.semiring.distrib_right by auto also have "... ≤ ((x - 1)⇧^{+})⇧^{+}" by (smt (verit, del_insts) comp_isotone reachable_without_loops star.circ_mult_increasing star.circ_plus_same star.circ_right_slide star.circ_separate_5 star.circ_square star.circ_transitive_equal star.left_plus_circ sup.bounded_iff sup_ge1 square_irreflexive_part) also have "... ≤ -1" using assms by (simp add: acyclic_plus) finally show ?thesis . qed lemma disjoint_set_forest_update_square: assumes "disjoint_set_forest x" and "vector y" and "regular y" shows "disjoint_set_forest (x[y⟼(x * x)⇧^{T}])" proof (intro conjI) show "univalent (x[y⟼(x * x)⇧^{T}])" using assms update_univalent mapping_mult_closed univalent_conv_injective by blast show "total (x[y⟼(x * x)⇧^{T}])" using assms update_total total_conv_surjective total_mult_closed by blast show "acyclic ((x[y⟼(x * x)⇧^{T}]) - 1)" using acyclic_update_square assms(1) by blast qed lemma disjoint_set_forest_update_square_point: assumes "disjoint_set_forest x" and "point y" shows "disjoint_set_forest (x[y⟼(x * x)⇧^{T}])" using assms disjoint_set_forest_update_square bijective_regular by blast end section ‹Verifying Further Operations on Disjoint-Set Forests› text ‹ In this section we verify the init-sets, path-halving and path-splitting operations of disjoint-set forests. › class choose_point = fixes choose_point :: "'a ⇒ 'a" text ‹ Using the ‹choose_point› operation we define a simple for-each-loop abstraction as syntactic sugar translated to a while-loop. Regular vector ‹h› describes the set of all elements that are yet to be processed. It is made explicit so that the invariant can refer to it. › syntax "_Foreach" :: "idt ⇒ idt ⇒ 'assn ⇒ 'com ⇒ 'com" ("(1FOREACH _/ USING _/ INV {_} //DO _ /OD)" [0,0,0,0] 61) translations "FOREACH x USING h INV { i } DO c OD" => "h := CONST top; WHILE h ≠ CONST bot INV { CONST regular h ∧ CONST vector h ∧ i } VAR { h↓ } DO x := CONST choose_point h; c; h[x] := CONST bot OD" class stone_kleene_relation_algebra_choose_point_finite_regular = stone_kleene_relation_algebra + finite_regular_p_algebra + choose_point + assumes choose_point_point: "vector x ⟹ x ≠ bot ⟹ point (choose_point x)" assumes choose_point_decreasing: "choose_point x ≤ --x" begin subclass stone_kleene_relation_algebra_tarski_finite_regular proof unfold_locales fix x let ?p = "choose_point (x * top)" let ?q = "choose_point ((?p ⊓ x)⇧^{T}* top)" let ?y = "?p ⊓ ?q⇧^{T}" assume 1: "regular x" "x ≠ bot" hence 2: "x * top ≠ bot" using le_bot top_right_mult_increasing by auto hence 3: "point ?p" by (simp add: choose_point_point comp_associative) hence 4: "?p ≠ bot" using 2 mult_right_zero by force have "?p ⊓ x ≠ bot" proof assume "?p ⊓ x = bot" hence 5: "x ≤ -?p" using p_antitone_iff pseudo_complement by auto have "?p ≤ --(x * top)" by (simp add: choose_point_decreasing) also have "... ≤ --(-?p * top)" using 5 by (simp add: comp_isotone pp_isotone) also have "... = -?p * top" using regular_mult_closed by auto also have "... = -?p" using 3 vector_complement_closed by auto finally have "?p = bot" using inf_absorb2 by fastforce thus False using 4 by auto qed hence "(?p ⊓ x)⇧^{T}* top ≠ bot" by (metis comp_inf.semiring.mult_zero_left comp_right_one inf.sup_monoid.add_commute inf_top.left_neutral schroeder_1) hence "point ?q" using choose_point_point vector_top_closed mult_assoc by auto hence 6: "arc ?y" using 3 by (smt bijective_conv_mapping inf.sup_monoid.add_commute mapping_inf_point_arc) have "?q ≤ --((?p ⊓ x)⇧^{T}* top)" by (simp add: choose_point_decreasing) hence "?y ≤ ?p ⊓ --((?p ⊓ x)⇧^{T}* top)⇧^{T}" by (metis conv_complement conv_isotone inf.sup_right_isotone) also have "... = ?p ⊓ --(top * (?p ⊓ x))" by (simp add: conv_dist_comp) also have "... = ?p ⊓ top * (?p ⊓ x)" using 1 3 bijective_regular pp_dist_comp by auto also have "... = ?p ⊓ ?p⇧^{T}* x" using 3 by (metis comp_inf_vector conv_dist_comp inf.sup_monoid.add_commute inf_top_right symmetric_top_closed) also have "... = (?p ⊓ ?p⇧^{T}) * x" using 3 by (simp add: vector_inf_comp) also have "... ≤ 1 * x" using 3 point_antisymmetric mult_left_isotone by blast finally have "?y ≤ x" by simp thus "top * x * top = top" using 6 by (smt (verit, ccfv_SIG) mult_assoc le_iff_sup mult_left_isotone semiring.distrib_left sup.orderE top.extremum) qed subsection ‹Init-Sets› text ‹ A disjoint-set forest is initialised by applying ‹make_set› to each node. We prove that the resulting disjoint-set forest is the identity relation. › theorem init_sets: "VARS h p x [ True ] FOREACH x USING h INV { p - h = 1 - h } DO p := make_set p x OD [ p = 1 ∧ disjoint_set_forest p ∧ h = bot ]" proof vcg_tc_simp fix h p let ?x = "choose_point h" let ?m = "make_set p ?x" assume 1: "regular h ∧ vector h ∧ p - h = 1 - h ∧ h ≠ bot" show "vector (-?x ⊓ h) ∧ ?m ⊓ (--?x ⊔ -h) = 1 ⊓ (--?x ⊔ -h) ∧ card { x . regular x ∧ x ≤ -?x ∧ x ≤ h } < h↓" proof (intro conjI) show "vector (-?x ⊓ h)" using 1 choose_point_point vector_complement_closed vector_inf_closed by blast have 2: "point ?x ∧ regular ?x" using 1 bijective_regular choose_point_point by blast have 3: "-h ≤ -?x" using choose_point_decreasing p_antitone_iff by auto have 4: "?x ⊓ ?m = ?x * ?x⇧^{T}∧ -?x ⊓ ?m = -?x ⊓ p" using 1 choose_point_point make_set_function make_set_postcondition_def by auto have "?m ⊓ (--?x ⊔ -h) = (?m ⊓ ?x) ⊔ (?m - h)" using 2 comp_inf.comp_left_dist_sup by auto also have "... = ?x * ?x⇧^{T}⊔ (?m ⊓ -?x ⊓ -h)" using 3 4 by (smt (z3) inf_absorb2 inf_assoc inf_commute) also have "... = ?x * ?x⇧^{T}⊔ (1 - h)" using 1 3 4 inf.absorb2 inf.sup_monoid.add_assoc inf_commute by auto also have "... = (1 ⊓ ?x) ⊔ (1 - h)" using 2 by (metis inf.cobounded2 inf.sup_same_context one_inf_conv vector_covector) also have "... = 1 ⊓ (--?x ⊔ -h)" using 2 comp_inf.semiring.distrib_left by auto finally show "?m ⊓ (--?x ⊔ -h) = 1 ⊓ (--?x ⊔ -h)" . have 5: "¬ ?x ≤ -?x" using 1 2 by (metis comp_commute_below_diversity conv_order inf.cobounded2 inf_absorb2 pseudo_complement strict_order_var top.extremum) have 6: "?x ≤ h" using 1 by (metis choose_point_decreasing) show "card { x . regular x ∧ x ≤ -?x ∧ x ≤ h } < h↓" apply (rule psubset_card_mono) using finite_regular apply simp using 2 5 6 by auto qed qed end subsection ‹Path Halving› text ‹ Path halving is a variant of the path compression technique. Similarly to path compression, we implement path halving independently of find-set, using a second while-loop which iterates over the same path to the root. We prove that path halving 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 halving, which is to replace every other parent pointer with a pointer to the respective grandparent. › context stone_kleene_relation_algebra_tarski_finite_regular begin definition "path_halving_invariant p x y p0 ≡ find_set_precondition p x ∧ point y ∧ y ≤ p⇧^{T}⇧^{⋆}* x ∧ y ≤ (p0 * p0)⇧^{T}⇧^{⋆}* x ∧ p0[(p0 * p0)⇧^{T}⇧^{⋆}* x - p0⇧^{T}⇧^{⋆}* y⟼(p0 * p0)⇧^{T}] = p ∧ disjoint_set_forest p0" definition "path_halving_postcondition p x y p0 ≡ disjoint_set_forest p ∧ y = root p x ∧ p ⊓ 1 = p0 ⊓ 1 ∧ fc p = fc p0 ∧ p0[(p0 * p0)⇧^{T}⇧^{⋆}* x⟼(p0 * p0)⇧^{T}] = p" lemma path_halving_invariant_aux_1: assumes "point x" and "point y" and "disjoint_set_forest p0" shows "p0 ≤ wcc (p0[(p0 * p0)⇧^{T}⇧^{⋆}* x - p0⇧^{T}⇧^{⋆}* y⟼(p0 * p0)⇧^{T}])" proof - let ?p2 = "p0 * p0" let ?p2t = "?p2⇧^{T}" let ?p2ts = "?p2t⇧^{⋆}" let ?px = "?p2ts * x" let ?py = "-(p0⇧^{T}⇧^{⋆}* y)" let ?pxy = "?px ⊓ ?py" let ?p = "p0[?pxy⟼?p2t]" have 1: "regular ?pxy" using assms(1,3) bijective_regular find_set_precondition_def mapping_regular pp_dist_comp regular_closed_star regular_conv_closed path_halving_invariant_def by auto have 2: "vector x ∧ vector ?px ∧ vector ?py" using assms(1,2) find_set_precondition_def vector_complement_closed vector_mult_closed path_halving_invariant_def by auto have 3: "?pxy ⊓ p0 ⊓ -?p2 ≤ -?px⇧^{T}" proof - have 4: "injective x ∧ univalent ?p2 ∧ regular p0" using assms(1,3) find_set_precondition_def mapping_regular univalent_mult_closed path_halving_invariant_def by auto have "?p2⇧^{⋆}* p0 ⊓ 1 ≤ p0⇧^{+}⊓ 1" using comp_inf.mult_left_isotone comp_isotone comp_right_one mult_sub_right_one star.circ_square star_slide by auto also have "... ≤ p0" using acyclic_plus_loop assms(3) path_halving_invariant_def by auto finally have 5: "?p2⇧^{⋆}* p0 ⊓ 1 ≤ p0" . hence 6: "?p2ts * (1 - p0) ≤ -p0" by (smt (verit, ccfv_SIG) conv_star_commute dual_order.trans inf.sup_monoid.add_assoc order.refl p_antitone_iff pseudo_complement schroeder_4_p schroeder_6_p) have "?p2t⇧^{+}* p0 ⊓ 1 = ?p2ts * p0⇧^{T}* (p0⇧^{T}* p0) ⊓ 1" by (metis conv_dist_comp star_plus mult_assoc) also have "... ≤ ?p2ts * p0⇧^{T}⊓ 1" by (metis assms(3) comp_inf.mult_left_isotone comp_isotone comp_right_one mult_sub_right_one) also have "... ≤ p0" using 5 by (metis conv_dist_comp conv_star_commute inf_commute one_inf_conv star_slide) finally have "?p2t⇧^{+}* p0 ≤ -1 ⊔ p0" by (metis regular_one_closed shunting_var_p sup_commute) hence 7: "?p2⇧^{+}* (1 - p0) ≤ -p0" by (smt (z3) conv_dist_comp conv_star_commute half_shunting inf.sup_monoid.add_assoc inf.sup_monoid.add_commute pseudo_complement schroeder_4_p schroeder_6_p star.circ_plus_same) have "(1 ⊓ ?px) * top * (1 ⊓ ?px ⊓ -p0) = ?px ⊓ top * (1 ⊓ ?px ⊓ -p0)" using 2 by (metis inf_commute vector_inf_one_comp mult_assoc) also have "... = ?px ⊓ ?px⇧^{T}* (1 - p0)" using 2 by (smt (verit, ccfv_threshold) covector_inf_comp_3 inf.sup_monoid.add_assoc inf.sup_monoid.add_commute inf_top.left_neutral) also have "... = ?px ⊓ x⇧^{T}* ?p2⇧^{⋆}* (1 - p0)" by (simp add: conv_dist_comp conv_star_commute) also have "... = (?px ⊓ x⇧^{T}) * ?p2⇧^{⋆}* (1 - p0)" using 2 vector_inf_comp by auto also have "... = ?p2ts * (x * x⇧^{T}) * ?p2⇧^{⋆}* (1 - p0)" using 2 vector_covector mult_assoc by auto also have "... ≤ ?p2ts * ?p2⇧^{⋆}* (1 - p0)" using 4 by (metis inf.order_lesseq_imp mult_left_isotone star.circ_mult_upper_bound star.circ_reflexive) also have "... = (?p2ts ⊔ ?p2⇧^{⋆}) * (1 - p0)" using 4 by (simp add: cancel_separate_eq) also have "... = (?p2ts ⊔ ?p2⇧^{+}) * (1 - p0)" by (metis star.circ_plus_one star_plus_loops sup_assoc sup_commute) also have "... ≤ -p0" using 6 7 by (simp add: mult_right_dist_sup) finally have "(1 ⊓ ?px)⇧^{T}* p0 * (1 ⊓ ?px ⊓ -p0)⇧^{T}≤ bot" by (smt (z3) inf.boundedI inf_p top.extremum triple_schroeder_p) hence 8: "(1 ⊓ ?px) * p0 * (1 ⊓ ?px ⊓ -p0) = bot" by (simp add: coreflexive_inf_closed coreflexive_symmetric le_bot) have "?px ⊓ p0 ⊓ ?px⇧^{T}= (1 ⊓ ?px) * p0 ⊓ ?px⇧^{T}" using 2 inf_commute vector_inf_one_comp by fastforce also have "... = (1 ⊓ ?px) * p0 * (1 ⊓ ?px)" using 2 by (metis comp_inf_vector mult_1_right vector_conv_covector) also have "... = (1 ⊓ ?px) * p0 * (1 ⊓ ?px ⊓ p0) ⊔ (1 ⊓ ?px) * p0 * (1 ⊓ ?px ⊓ -p0)" using 4 by (metis maddux_3_11_pp mult_left_dist_sup) also have "... = (1 ⊓ ?px) * p0 * (1 ⊓ ?px ⊓ p0)" using 8 by simp also have "... ≤ ?p2" by (metis comp_isotone coreflexive_comp_top_inf inf.cobounded1 inf.cobounded2) finally have "?px ⊓ p0 ⊓ -?p2 ≤ -?px⇧^{T}" using 4 p_shunting_swap regular_mult_closed by fastforce thus ?thesis by (meson comp_inf.mult_left_isotone dual_order.trans inf.cobounded1) qed have "p0 ≤ ?p2 * p0⇧^{T}" by (metis assms(3) comp_associative comp_isotone comp_right_one eq_refl total_var) hence "?pxy ⊓ p0 ⊓ -?p2 ≤ ?p2 * p0⇧^{T}" by (metis inf.coboundedI1 inf.sup_monoid.add_commute) hence "?pxy ⊓ p0 ⊓ -?p2 ≤ ?pxy ⊓ ?p2 * p0⇧^{T}⊓ -?px⇧^{T}" using 3 by (meson dual_order.trans inf.boundedI inf.cobounded1) also have "... = (?pxy ⊓ ?p2) * p0⇧^{T}⊓ -?px⇧^{T}" using 2 vector_inf_comp by auto also have "... = (?pxy ⊓ ?p2) * (-?px ⊓ p0)⇧^{T}" using 2 by (simp add: covector_comp_inf inf.sup_monoid.add_commute vector_conv_compl conv_complement conv_dist_inf) also have "... ≤ ?p * (-?px ⊓ p0)⇧^{T}" using comp_left_increasing_sup by auto also have "... ≤ ?p * ?p⇧^{T}" by (metis comp_inf.mult_right_isotone comp_isotone conv_isotone inf.eq_refl inf.sup_monoid.add_commute le_supI1 p_antitone_inf sup_commute) also have "... ≤ wcc ?p" using star.circ_sub_dist_2 by auto finally have 9: "?pxy ⊓ p0 ⊓ -?p2 ≤ wcc ?p" . have "p0 = (?pxy ⊓ p0) ⊔ (-?pxy ⊓ p0)" using 1 by (metis inf.sup_monoid.add_commute maddux_3_11_pp) also have "... ≤ (?pxy ⊓ p0) ⊔ ?p" using sup_right_isotone by auto also have "... = (?pxy ⊓ p0 ⊓ -?p2) ⊔ (?pxy ⊓ p0 ⊓ ?p2) ⊔ ?p" by (smt (z3) assms(3) maddux_3_11_pp mapping_regular pp_dist_comp path_halving_invariant_def) also have "... ≤ (?pxy ⊓ p0 ⊓ -?p2) ⊔ (?pxy ⊓ ?p2) ⊔ ?p" by (meson comp_inf.comp_left_subdist_inf inf.boundedE semiring.add_left_mono semiring.add_right_mono) also have "... = (?pxy ⊓ p0 ⊓ -?p2) ⊔ ?p" using sup_assoc by auto also have "... ≤ wcc ?p ⊔ ?p" using 9 sup_left_isotone by blast also have "... ≤ wcc ?p" by (simp add: star.circ_sub_dist_1) finally show ?thesis . qed lemma path_halving_invariant_aux: assumes "path_halving_invariant p x y p0" shows "p[[y]] = p0[[y]]" and "p[[p[[y]]]] = p0[[p0[[y]]]]" and "p[[p[[p[[y]]]]]] = p0[[p0[[p0[[y]]]]]]" and "p ⊓ 1 = p0 ⊓ 1" and "fc p = fc p0" proof - let ?p2 = "p0 * p0" let ?p2t = "?p2⇧^{T}" let ?p2ts = "?p2t⇧^{⋆}" let ?px = "?p2ts * x" let ?py = "-(p0⇧^{T}⇧^{⋆}* y)" let ?pxy = "?px ⊓ ?py" let ?p = "p0[?pxy⟼?p2t]" have "?p[[y]] = p0[[y]]" apply (rule put_get_different_vector) using assms find_set_precondition_def vector_complement_closed vector_inf_closed vector_mult_closed path_halving_invariant_def apply force by (meson inf.cobounded2 order_lesseq_imp p_antitone_iff path_compression_1b) thus 1: "p[[y]] = p0[[y]]" using assms path_halving_invariant_def by auto have "?p[[p0[[y]]]] = p0[[p0[[y]]]]" apply (rule put_get_different_vector) using assms find_set_precondition_def vector_complement_closed vector_inf_closed vector_mult_closed path_halving_invariant_def apply force by (metis comp_isotone inf.boundedE inf.coboundedI2 inf.eq_refl p_antitone_iff selection_closed_id star.circ_increasing) thus 2: "p[[p[[y]]]] = p0[[p0[[y]]]]" using 1 assms path_halving_invariant_def by auto have "?p[[p0[[p0[[y]]]]]] = p0[[p0[[p0[[y]]]]]]" apply (rule put_get_different_vector) using assms find_set_precondition_def vector_complement_closed vector_inf_closed vector_mult_closed path_halving_invariant_def apply force by (metis comp_associative comp_isotone conv_dist_comp conv_involutive conv_order inf.coboundedI2 inf.le_iff_sup mult_left_isotone p_antitone_iff p_antitone_inf star.circ_increasing star.circ_transitive_equal) thus "p[[p[[p[[y]]]]]] = p0[[p0[[p0[[y]]]]]]" using 2 assms path_halving_invariant_def by auto have 3: "regular ?pxy" using assms bijective_regular find_set_precondition_def mapping_regular pp_dist_comp regular_closed_star regular_conv_closed path_halving_invariant_def by auto have "p ⊓ 1 = ?p ⊓ 1" using assms path_halving_invariant_def by auto also have "... = (?pxy ⊓ ?p2 ⊓ 1) ⊔ (-?pxy ⊓ p0 ⊓ 1)" using comp_inf.semiring.distrib_right conv_involutive by auto also have "... = (?pxy ⊓ p0 ⊓ 1) ⊔ (-?pxy ⊓ p0 ⊓ 1)" using assms acyclic_square path_halving_invariant_def inf.sup_monoid.add_assoc by auto also have "... = (?pxy ⊔ -?pxy) ⊓ p0 ⊓ 1" using inf_sup_distrib2 by auto also have "... = p0 ⊓ 1" using 3 by (metis inf.sup_monoid.add_commute inf_sup_distrib1 maddux_3_11_pp) finally show "p ⊓ 1 = p0 ⊓ 1" . have "p ≤ p0⇧^{+}" by (metis assms path_halving_invariant_def update_square_ub_plus) hence 4: "fc p ≤ fc p0" using conv_plus_commute fc_isotone star.left_plus_circ by fastforce have "wcc p0 ≤ wcc ?p" by (meson assms wcc_below_wcc path_halving_invariant_aux_1 path_halving_invariant_def find_set_precondition_def) hence "fc p0 ≤ fc ?p" using assms find_set_precondition_def path_halving_invariant_def fc_wcc by auto thus "fc p = fc p0" using 4 assms path_halving_invariant_def by auto qed lemma path_halving_1: "find_set_precondition p0 x ⟹ path_halving_invariant p0 x x p0" proof - assume 1: "find_set_precondition p0 x" show "path_halving_invariant p0 x x p0" proof (unfold path_halving_invariant_def, intro conjI) show "find_set_precondition p0 x" using 1 by simp show "vector x" "injective x" "surjective x" using 1 find_set_precondition_def by auto show "x ≤ p0⇧^{T}⇧^{⋆}* x" by (simp add: path_compression_1b) show "x ≤ (p0 * p0)⇧^{T}⇧^{⋆}* x" by (simp add: path_compression_1b) have "(p0 * p0)⇧^{T}⇧^{⋆}* x ≤ p0⇧^{T}⇧^{⋆}* x" by (simp add: conv_dist_comp mult_left_isotone star.circ_square) thus "p0[(p0 * p0)⇧^{T}⇧^{⋆}* x - p0⇧^{T}⇧^{⋆}* x⟼(p0 * p0)⇧^{T}] = p0" by (smt (z3) inf.le_iff_sup inf_commute maddux_3_11_pp p_antitone_inf pseudo_complement) show "univalent p0" "total p0" "acyclic (p0 - 1)" using 1 find_set_precondition_def by auto qed qed lemma path_halving_2: "path_halving_invariant p x y p0 ∧ y ≠ p[[y]] ⟹ path_halving_invariant (p[y⟼p[[p[[y]]]]]) x ((p[y⟼p[[p[[y]]]]])[[y]]) p0 ∧ ((p[y⟼p[[p[[y]]]]])⇧^{T}⇧^{⋆}* ((p[y⟼p[[p[[y]]]]])[[y]]))↓ < (p⇧^{T}⇧^{⋆}* y)↓" proof - let ?py = "p[[y]]" let ?ppy = "p[[?py]]" let ?pyppy = "p[y⟼?ppy]" let ?p2 = "p0 * p0" let ?p2t = "?p2⇧^{T}" let ?p2ts = "?p2t⇧^{⋆}" let ?px = "?p2ts * x" let ?py2 = "-(p0⇧^{T}⇧^{⋆}* y)" let ?pxy = "?px ⊓ ?py2" let ?p = "p0[?pxy⟼?p2t]" let ?pty = "p0⇧^{T}* y" let ?pt2y = "p0⇧^{T}* p0⇧^{T}* y" let ?pt2sy = "p0⇧^{T}⇧^{⋆}* p0⇧^{T}* p0⇧^{T}* y" assume 1: "path_halving_invariant p x y p0 ∧ y ≠ ?py" have 2: "point ?pty ∧ point ?pt2y" using 1 by (smt (verit) comp_associative read_injective read_surjective path_halving_invariant_def) show "path_halving_invariant ?pyppy x (?pyppy[[y]]) p0 ∧ (?pyppy⇧^{T}⇧^{⋆}* (?pyppy[[y]]))↓ < (p⇧^{T}⇧^{⋆}* y)↓" proof show "path_halving_invariant ?pyppy x (?pyppy[[y]]) p0" proof (unfold path_halving_invariant_def, intro conjI) show 3: "find_set_precondition ?pyppy x" proof (unfold find_set_precondition_def, intro conjI) show "univalent ?pyppy" using 1 find_set_precondition_def read_injective update_univalent path_halving_invariant_def by auto show "total ?pyppy" using 1 bijective_regular find_set_precondition_def read_surjective update_total path_halving_invariant_def by force show "acyclic (?pyppy - 1)" apply (rule update_acyclic_3) using 1 find_set_precondition_def path_halving_invariant_def apply blast using 1 2 comp_associative path_halving_invariant_aux(2) apply force using 1 path_halving_invariant_def apply blast by (metis inf.order_lesseq_imp mult_isotone star.circ_increasing star.circ_square mult_assoc) show "vector x" "injective x" "surjective x" using 1 find_set_precondition_def path_halving_invariant_def by auto qed show "vector (?pyppy[[y]])" using 1 comp_associative path_halving_invariant_def by auto show "injective (?pyppy[[y]])" using 1 3 read_injective path_halving_invariant_def find_set_precondition_def by auto show "surjective (?pyppy[[y]])" using 1 3 read_surjective path_halving_invariant_def find_set_precondition_def by auto show "?pyppy[[y]] ≤ ?pyppy⇧^{T}⇧^{⋆}* x" proof - have "y = (y ⊓ p⇧^{T}⇧^{⋆}) * x" using 1 le_iff_inf vector_inf_comp path_halving_invariant_def by auto also have "... = ((y ⊓ 1) ⊔ (y ⊓ (p⇧^{T}⊓ -y⇧^{T})⇧^{+})) * x" using 1 omit_redundant_points_3 path_halving_invariant_def by auto also have "... ≤ (1 ⊔ (y ⊓ (p⇧^{T}⊓ -y⇧^{T})⇧^{+})) * x" using 1 sup_inf_distrib2 vector_inf_comp path_halving_invariant_def by auto also have "... ≤ (1 ⊔ (p⇧^{T}⊓ -y⇧^{T})⇧^{+}) * x" by (simp add: inf.coboundedI2 mult_left_isotone) also have "... = (p ⊓ -y)⇧^{T}⇧^{⋆}* x" by (simp add: conv_complement conv_dist_inf star_left_unfold_equal) also have "... ≤ ?pyppy⇧^{T}⇧^{⋆}* x" by (simp add: conv_isotone inf.sup_monoid.add_commute mult_left_isotone star_isotone) finally show ?thesis by (metis mult_isotone star.circ_increasing star.circ_transitive_equal mult_assoc) qed show "?pyppy[[y]] ≤ ?px" proof - have "?pyppy[[y]] = p[[?py]]" using 1 put_get vector_mult_closed path_halving_invariant_def by force also have "... = p0[[p0[[y]]]]" using 1 path_halving_invariant_aux(2) by blast also have "... = ?p2t * y" by (simp add: conv_dist_comp mult_assoc) also have "... ≤ ?p2t * ?px" using 1 path_halving_invariant_def comp_associative mult_right_isotone by force also have "... ≤ ?px" by (metis comp_associative mult_left_isotone star.left_plus_below_circ) finally show ?thesis . qed show "p0[?px - p0⇧^{T}⇧^{⋆}* (?pyppy[[y]])⟼?p2t] = ?pyppy" proof - have "?px ⊓ ?pty = ?px ⊓ p0⇧^{T}* ?px ⊓ ?pty" using 1 inf.absorb2 inf.sup_monoid.add_assoc mult_right_isotone path_halving_invariant_def by force also have "... = (?p2ts ⊓ p0⇧^{T}* ?p2ts) * x ⊓ ?pty" using 3 comp_associative find_set_precondition_def injective_comp_right_dist_inf by auto also have "... = (1 ⊓ p0) * (?p2ts ⊓ p0⇧^{T}* ?p2ts) * x ⊓ ?pty" using 1 even_odd_root mapping_regular path_halving_invariant_def by auto also have "... ≤ (1 ⊓ p0) * top ⊓ ?pty" by (metis comp_associative comp_inf.mult_left_isotone comp_inf.star.circ_sub_dist_2 comp_left_subdist_inf dual_order.trans mult_right_isotone) also have 4: "... = (1 ⊓ p0⇧^{T}) * ?pty" using coreflexive_comp_top_inf one_inf_conv by auto also have "... ≤ ?pt2y" by (simp add: mult_assoc mult_left_isotone) finally have 5: "?px ⊓ ?pty ≤ ?pt2y" . have 6: "p[?px ⊓ -?pt2sy ⊓ ?pty⟼?p2t] = p" proof (cases "?pty ≤ ?px ⊓ -?pt2sy") case True hence "?pty ≤ ?pt2y" using 5 conv_dist_comp inf.absorb2 by auto hence 7: "?pty = ?pt2y" using 2 epm_3 by fastforce have "p[?px ⊓ -?pt2sy ⊓ ?pty⟼?p2t] = p[?pty⟼?p2t]" using True inf.absorb2 by auto also have "... = p[?pty⟼?p2[[?pty]]]" using 2 update_point_get by auto also have "... = p[?pty⟼p0⇧^{T}* p0⇧^{T}* p0⇧^{T}* y]" using comp_associative conv_dist_comp by auto also have "... = p[?pty⟼?pt2y]" using 7 mult_assoc by simp also have "... = p[?pty⟼p[[?pty]]]" using 1 path_halving_invariant_aux(1,2) mult_assoc by force also have "... = p" using 2 get_put by auto finally show ?thesis . next case False have "mapping ?p2" using 1 mapping_mult_closed path_halving_invariant_def by blast hence 8: "regular (?px ⊓ -?pt2sy)" using 1 bijective_regular find_set_precondition_def mapping_regular pp_dist_comp regular_closed_star regular_conv_closed path_halving_invariant_def by auto have "vector (?px ⊓ -?pt2sy)" using 1 find_set_precondition_def vector_complement_closed vector_inf_closed vector_mult_closed path_halving_invariant_def by force hence "?pty ≤ -(?px ⊓ -?pt2sy)" using 2 8 point_in_vector_or_complement False by blast hence "?px ⊓ -?pt2sy ⊓ ?pty = bot" by (simp add: p_antitone_iff pseudo_complement) thus ?thesis by simp qed have 9: "p[?px ⊓ -?pt2sy ⊓ y⟼?p2t] = ?pyppy" proof (cases "y ≤ -?pt2sy") case True hence "p[?px ⊓ -?pt2sy ⊓ y⟼?p2t] = p[y⟼?p2t]" using 1 inf.absorb2 path_halving_invariant_def by auto also have "... = ?pyppy" using 1 by (metis comp_associative conv_dist_comp path_halving_invariant_aux(2) path_halving_invariant_def update_point_get) finally show ?thesis . next case False have "vector (-?pt2sy)" using 1 vector_complement_closed vector_mult_closed path_halving_invariant_def by blast hence 10: "y ≤ ?pt2sy" using 1 by (smt (verit, del_insts) False bijective_regular point_in_vector_or_complement regular_closed_star regular_mult_closed total_conv_surjective univalent_conv_injective path_halving_invariant_def) hence "?px ⊓ -?pt2sy ⊓ y = bot" by (simp add: inf.coboundedI2 p_antitone pseudo_complement) hence 11: "p[?px ⊓ -?pt2sy ⊓ y⟼?p2t] = p" by simp have "y ≤ p0⇧^{T}⇧^{+}* y" using 10 by (metis mult_left_isotone order_lesseq_imp star.circ_plus_same star.left_plus_below_circ) hence 12: "y = root p0 y" using 1 loop_root_2 path_halving_invariant_def by blast have "?pyppy = p[y⟼p0[[p0[[y]]]]]" using 1 path_halving_invariant_aux(2) by force also have "... = p[y⟼p0[[y]]]" using 1 12 by (metis root_successor_loop path_halving_invariant_def) also have "... = p[y⟼?py]" using 1 path_halving_invariant_aux(1) by force also have "... = p" using 1 get_put path_halving_invariant_def by blast finally show ?thesis using 11 by simp qed have 13: "-?pt2sy = -(p0⇧^{T}⇧^{⋆}* y) ⊔ (-?pt2sy ⊓ ?pty) ⊔ (-?pt2sy ⊓ y)" proof (rule order.antisym) have 14: "regular (p0⇧^{T}⇧^{⋆}* y) ∧ regular ?pt2sy" using 1 by (metis order.antisym conv_complement conv_dist_comp conv_involutive conv_star_commute forest_components_increasing mapping_regular pp_dist_star regular_mult_closed top.extremum path_halving_invariant_def) have "p0⇧^{T}⇧^{⋆}= p0⇧^{T}⇧^{⋆}* p0⇧^{T}* p0⇧^{T}⊔ p0⇧^{T}⊔ 1" using star.circ_back_loop_fixpoint star.circ_plus_same star_left_unfold_equal sup_commute by auto hence "p0⇧^{T}⇧^{⋆}* y ≤ ?pt2sy ⊔ ?pty ⊔ y" by (metis inf.eq_refl mult_1_left mult_right_dist_sup) also have "... = ?pt2sy ⊔ (-?pt2sy ⊓ ?pty) ⊔ y" using 14 by (metis maddux_3_21_pp) also have "... = ?pt2sy ⊔ (-?pt2sy ⊓ ?pty) ⊔ (-?pt2sy ⊓ y)" using 14 by (smt (z3) maddux_3_21_pp sup.left_commute sup_assoc) hence "p0⇧^{T}⇧^{⋆}* y ⊓ -?pt2sy ≤ (-?pt2sy ⊓ ?pty) ⊔ (-?pt2sy ⊓ y)" using calculation half_shunting sup_assoc sup_commute by auto thus "-?pt2sy ≤ -(p0⇧^{T}⇧^{⋆}* y) ⊔ (-?pt2sy ⊓ ?pty) ⊔ (-?pt2sy ⊓ y)" using 14 by (smt (z3) inf.sup_monoid.add_commute shunting_var_p sup.left_commute sup_commute) have "-(p0⇧^{T}⇧^{⋆}* y) ≤ -?pt2sy" by (meson mult_left_isotone order.trans p_antitone star.right_plus_below_circ) thus "-(p0⇧^{T}⇧^{⋆}* y) ⊔ (-?pt2sy ⊓ ?pty) ⊔ (-?pt2sy ⊓ y) ≤ -?pt2sy" by simp qed have "regular ?px" "regular ?pty" "regular y" using 1 bijective_regular find_set_precondition_def mapping_regular pp_dist_comp regular_closed_star regular_conv_closed path_halving_invariant_def by auto hence 15: "regular (?px ⊓ -?pt2sy ⊓ ?pty)" "regular (?px ⊓ -?pt2sy ⊓ y)" by auto have "p0[?px - p0⇧^{T}⇧^{⋆}* (?pyppy[[y]])⟼?p2t] = p0[?px - p0⇧^{T}⇧^{⋆}* (p[[?py]])⟼?p2t]" using 1 put_get vector_mult_closed path_halving_invariant_def by auto also have "... = p0[?px - ?pt2sy⟼?p2t]" using 1 comp_associative path_halving_invariant_aux(2) by force also have "... = p0[?pxy ⊔ (?px ⊓ -?pt2sy ⊓ ?pty) ⊔ (?px ⊓ -?pt2sy ⊓ y)⟼?p2t]" using 13 by (metis comp_inf.semiring.distrib_left inf.sup_monoid.add_assoc) also have "... = (?p[?px ⊓ -?pt2sy ⊓ ?pty⟼?p2t])[?px ⊓ -?pt2sy ⊓ y⟼?p2t]" using 15 by (smt (z3) update_same_3 comp_inf.semiring.mult_not_zero inf.sup_monoid.add_assoc inf.sup_monoid.add_commute) also have "... = (p[?px ⊓ -?pt2sy ⊓ ?pty⟼?p2t])[?px ⊓ -?pt2sy ⊓ y⟼?p2t]" using 1 path_halving_invariant_def by auto also have "... = p[?px ⊓ -?pt2sy ⊓ y⟼?p2t]" using 6 by simp also have "... = ?pyppy" using 9 by auto finally show ?thesis . qed show "univalent p0" "total p0" "acyclic (p0 - 1)