# Theory More_Disjoint_Set_Forests

```(* 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

text ‹Theorem 6.4›

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)"
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

text ‹Theorem 2.13›

lemma update_ub:
"x[y⟼z] ≤ x ⊔ z⇧T"
by (meson dual_order.trans inf.cobounded2 le_supI sup.cobounded1 sup_ge2)

text ‹Theorem 6.7›

lemma update_square_ub:
"x[y⟼(x * x)⇧T] ≤ x ⊔ x * x"
by (metis conv_involutive update_ub)

text ‹Theorem 2.14›

lemma update_same_sub:
assumes "u ⊓ x = u ⊓ z"
and "y ≤ u"
and "regular y"
shows "x[y⟼z⇧T] = x"

text ‹Theorem 2.15›

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)

text ‹Theorem 2.11›

lemma update_bot:
"x[bot⟼z] = x"
by simp

text ‹Theorem 2.12›

lemma update_top:
"x[top⟼z] = z⇧T"
by simp

text ‹Theorem 2.6›

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)

text ‹Theorem 2.7›

lemma update_split:
assumes "regular w"
shows "x[y⟼z] = (x[y - w⟼z])[y ⊓ w⟼z]"

text ‹Theorem 2.8›

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"
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)"
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)"
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]]])"

text ‹Theorem 2.9›

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]]])"

text ‹Theorem 2.10›

lemma update_mapping_swap:
assumes "mapping x"
and "point y"
and "point z"
shows "mapping ((x[y⟼x[[z]]])[z⟼x[[y]]])"

text ‹Theorem 2.16 ‹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

text ‹Theorem 5.3›

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)

text ‹Theorem 6.1›

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)"
have "x ⊓ 1 ≤ top * (x ⊓ 1)"
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"
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"
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"
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"
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"
have "x⇧T ⊓ (x * x)⇧⋆ = (x⇧T ⊓ (x * x)⇧⋆ ⊓ 1) ⊔ (x⇧T ⊓ (x * x)⇧⋆ ⊓ -1)"
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"
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"
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⇧⋆)"
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)

text ‹Theorem 6.2›

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)"
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)"
also have "... ≤ (1 ⊓ (x - 1) * (x - 1)) ⊔ (x - 1) * (x ⊓ 1) ⊔ x"
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"
also have "... = x"
by (metis comp_isotone inf.cobounded1 inf_le2 mult_1_right sup.absorb2)
finally show "x * x ⊓ 1 ≤ x ⊓ 1"
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"
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

text ‹Theorem 6.5›

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"
also have "... = (y ⊓ y⇧T * x * x ⊓ 1) ⊔ (-y ⊓ x ⊓ 1)"
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"
finally show ?thesis
.
qed

text ‹Theorem 6.6›

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)"
also have "... ≤ x * x ⊔ x"
using 1 inf_le2 sup_mono by blast
also have "... ≤ x⇧⋆"
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"
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"
also have "... = (y ⊓ y⇧T * x * x) * x⇧T ⊓ -y⇧T"
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"
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)"
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

text ‹Theorem 6.2›

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"
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"
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)

text ‹Theorem 6.3›

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"
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)"
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

text ‹Theorem 6.3›

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

text ‹Theorem 6.8›

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

text ‹Theorem 6.9›

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"
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)"
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)"
hence "?y ≤ ?p ⊓ --((?p ⊓ x)⇧T * top)⇧T"
by (metis conv_complement conv_isotone inf.sup_right_isotone)
also have "... = ?p ⊓ --(top * (?p ⊓ x))"
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 ≡
path_compression_precondition p x y ∧ 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)"
also have "... = ?px ⊓ x⇧T * ?p2⇧⋆ * (1 - p0)"
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"
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"
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)"
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"
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"
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"
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"
show "x ≤ (p0 * p0)⇧T⇧⋆ * x"
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"
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"
also have "... = (p ⊓ -y)⇧T⇧⋆ * x"
by (simp add: conv_complement conv_dist_inf star_left_unfold_equal)
also have "... ≤ ?pyppy⇧T⇧⋆ * x"
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"
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"
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"
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"
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]"