Theory Relation_Algebras
section ‹Relation Algebras›
text ‹
The main structures introduced in this theory are Stone relation algebras.
They generalise Tarski's relation algebras \<^cite>‹"Tarski1941"› by weakening the Boolean algebra lattice structure to a Stone algebra.
Our motivation is to generalise relation-algebraic methods from unweighted graphs to weighted graphs.
Unlike unweighted graphs, weighted graphs do not form a Boolean algebra because there is no complement operation on the edge weights.
However, edge weights form a Stone algebra, and matrices over edge weights (that is, weighted graphs) form a Stone relation algebra.
The development in this theory is described in our papers \<^cite>‹"Guttmann2016c" and "Guttmann2017b"›.
Our main application there is the verification of Prim's minimum spanning tree algorithm.
Related work about fuzzy relations \<^cite>‹"Goguen1967" and "Winter2001b"›, Dedekind categories \<^cite>‹"KawaharaFurusawa2001"› and rough relations \<^cite>‹"Comer1993" and "Pawlak1996"› is also discussed in these papers.
In particular, Stone relation algebras do not assume that the underlying lattice is complete or a Heyting algebra, and they do not assume that composition has residuals.
We proceed in two steps.
First, we study the positive fragment in the form of single-object bounded distributive allegories \<^cite>‹"FreydScedrov1990"›.
Second, we extend these structures by a pseudocomplement operation with additional axioms to obtain Stone relation algebras.
Tarski's relation algebras are then obtained by a simple extension that imposes a Boolean algebra.
See, for example, \<^cite>‹"BirdMoor1997" and "HirschHodkinson2002" and "Maddux1996" and "Maddux2006" and "Schmidt2011" and "SchmidtStroehlein1993"› for further details about relations and relation algebras, and \<^cite>‹"AndrekaMikulas2011" and "BredihinSchein1978"› for algebras of relations with a smaller signature.
›
theory Relation_Algebras
imports Stone_Algebras.P_Algebras Semirings
begin
subsection ‹Single-Object Bounded Distributive Allegories›
text ‹
We start with developing bounded distributive allegories.
The following definitions concern properties of relations that require converse in addition to lattice and semiring operations.
›
class conv =
fixes conv :: "'a ⇒ 'a" ("_⇧T" [100] 100)
class bounded_distrib_allegory_signature = inf + sup + times + conv + bot + top + one + ord
begin
subclass times_one_ord .
subclass times_top .
abbreviation total_var :: "'a ⇒ bool" where "total_var x ≡ 1 ≤ x * x⇧T"
abbreviation surjective_var :: "'a ⇒ bool" where "surjective_var x ≡ 1 ≤ x⇧T * x"
abbreviation univalent :: "'a ⇒ bool" where "univalent x ≡ x⇧T * x ≤ 1"
abbreviation injective :: "'a ⇒ bool" where "injective x ≡ x * x⇧T ≤ 1"
abbreviation mapping :: "'a ⇒ bool" where "mapping x ≡ univalent x ∧ total x"
abbreviation bijective :: "'a ⇒ bool" where "bijective x ≡ injective x ∧ surjective x"
abbreviation point :: "'a ⇒ bool" where "point x ≡ vector x ∧ bijective x"
abbreviation arc :: "'a ⇒ bool" where "arc x ≡ bijective (x * top) ∧ bijective (x⇧T * top)"
abbreviation symmetric :: "'a ⇒ bool" where "symmetric x ≡ x⇧T = x"
abbreviation antisymmetric :: "'a ⇒ bool" where "antisymmetric x ≡ x ⊓ x⇧T ≤ 1"
abbreviation asymmetric :: "'a ⇒ bool" where "asymmetric x ≡ x ⊓ x⇧T = bot"
abbreviation linear :: "'a ⇒ bool" where "linear x ≡ x ⊔ x⇧T = top"
abbreviation equivalence :: "'a ⇒ bool" where "equivalence x ≡ preorder x ∧ symmetric x"
abbreviation order :: "'a ⇒ bool" where "order x ≡ preorder x ∧ antisymmetric x"
abbreviation linear_order :: "'a ⇒ bool" where "linear_order x ≡ order x ∧ linear x"
end
text ‹
We reuse the relation algebra axioms given in \<^cite>‹"Maddux1996"› except for one -- see lemma ‹conv_complement_sub› below -- which we replace with the Dedekind rule (or modular law) ‹dedekind_1›.
The Dedekind rule or variants of it are known from \<^cite>‹"BirdMoor1997" and "FreydScedrov1990" and "KawaharaFurusawaMori1999" and "SchmidtStroehlein1993"›.
We add ‹comp_left_zero›, which follows in relation algebras but not in the present setting.
The main change is that only a bounded distributive lattice is required, not a Boolean algebra.
›
class bounded_distrib_allegory = bounded_distrib_lattice + times + one + conv +
assumes comp_associative : "(x * y) * z = x * (y * z)"
assumes comp_right_dist_sup : "(x ⊔ y) * z = (x * z) ⊔ (y * z)"
assumes comp_left_zero [simp]: "bot * x = bot"
assumes comp_left_one [simp]: "1 * x = x"
assumes conv_involutive [simp]: "x⇧T⇧T = x"
assumes conv_dist_sup : "(x ⊔ y)⇧T = x⇧T ⊔ y⇧T"
assumes conv_dist_comp : "(x * y)⇧T = y⇧T * x⇧T"
assumes dedekind_1 : "x * y ⊓ z ≤ x * (y ⊓ (x⇧T * z))"
begin
subclass bounded_distrib_allegory_signature .
text ‹
Many properties of relation algebras already follow in bounded distributive allegories.
›
lemma conv_isotone:
"x ≤ y ⟹ x⇧T ≤ y⇧T"
by (metis conv_dist_sup le_iff_sup)
lemma conv_order:
"x ≤ y ⟷ x⇧T ≤ y⇧T"
using conv_isotone by fastforce
lemma conv_bot [simp]:
"bot⇧T = bot"
using conv_order bot_unique by force
lemma conv_top [simp]:
"top⇧T = top"
by (metis conv_involutive conv_order order.eq_iff top_greatest)
lemma conv_dist_inf:
"(x ⊓ y)⇧T = x⇧T ⊓ y⇧T"
apply (rule order.antisym)
using conv_order apply simp
by (metis conv_order conv_involutive inf.boundedI inf.cobounded1 inf.cobounded2)
lemma conv_inf_bot_iff:
"bot = x⇧T ⊓ y ⟷ bot = x ⊓ y⇧T"
using conv_dist_inf conv_bot by fastforce
lemma conv_one [simp]:
"1⇧T = 1"
by (metis comp_left_one conv_dist_comp conv_involutive)
lemma comp_left_dist_sup:
"(x * y) ⊔ (x * z) = x * (y ⊔ z)"
by (metis comp_right_dist_sup conv_involutive conv_dist_sup conv_dist_comp)
lemma comp_right_isotone:
"x ≤ y ⟹ z * x ≤ z * y"
by (simp add: comp_left_dist_sup sup.absorb_iff1)
lemma comp_left_isotone:
"x ≤ y ⟹ x * z ≤ y * z"
by (metis comp_right_dist_sup le_iff_sup)
lemma comp_isotone:
"x ≤ y ⟹ w ≤ z ⟹ x * w ≤ y * z"
using comp_left_isotone comp_right_isotone order.trans by blast
lemma comp_left_subdist_inf:
"(x ⊓ y) * z ≤ x * z ⊓ y * z"
by (simp add: comp_left_isotone)
lemma comp_left_increasing_sup:
"x * y ≤ (x ⊔ z) * y"
by (simp add: comp_left_isotone)
lemma comp_right_subdist_inf:
"x * (y ⊓ z) ≤ x * y ⊓ x * z"
by (simp add: comp_right_isotone)
lemma comp_right_increasing_sup:
"x * y ≤ x * (y ⊔ z)"
by (simp add: comp_right_isotone)
lemma comp_right_zero [simp]:
"x * bot = bot"
by (metis comp_left_zero conv_dist_comp conv_involutive)
lemma comp_right_one [simp]:
"x * 1 = x"
by (metis comp_left_one conv_dist_comp conv_involutive)
lemma comp_left_conjugate:
"conjugate (λy . x * y) (λy . x⇧T * y)"
apply (unfold conjugate_def, intro allI)
by (metis comp_right_zero bot.extremum_unique conv_involutive dedekind_1 inf.commute)
lemma comp_right_conjugate:
"conjugate (λy . y * x) (λy . y * x⇧T)"
apply (unfold conjugate_def, intro allI)
by (metis comp_left_conjugate[unfolded conjugate_def] conv_inf_bot_iff conv_dist_comp conv_involutive)
text ‹
We still obtain a semiring structure.
›
subclass bounded_idempotent_semiring
by (unfold_locales)
(auto simp: comp_right_isotone comp_right_dist_sup comp_associative comp_left_dist_sup)
sublocale inf: semiring_0 sup bot inf
by (unfold_locales, auto simp: inf_sup_distrib2 inf_sup_distrib1 inf_assoc)
lemma schroeder_1:
"x * y ⊓ z = bot ⟷ x⇧T * z ⊓ y = bot"
using abel_semigroup.commute comp_left_conjugate conjugate_def inf.abel_semigroup_axioms by fastforce
lemma schroeder_2:
"x * y ⊓ z = bot ⟷ z * y⇧T ⊓ x = bot"
by (metis comp_right_conjugate conjugate_def inf_commute)
lemma comp_additive:
"additive (λy . x * y) ∧ additive (λy . x⇧T * y) ∧ additive (λy . y * x) ∧ additive (λy . y * x⇧T)"
by (simp add: comp_left_dist_sup additive_def comp_right_dist_sup)
lemma dedekind_2:
"y * x ⊓ z ≤ (y ⊓ (z * x⇧T)) * x"
by (metis conv_dist_inf conv_order conv_dist_comp dedekind_1)
text ‹
The intersection with a vector can still be exported from the first argument of a composition, and many other properties of vectors and covectors continue to hold.
›
lemma vector_inf_comp:
"vector x ⟹ (x ⊓ y) * z = x ⊓ (y * z)"
apply (rule order.antisym)
apply (metis comp_left_subdist_inf comp_right_isotone inf.sup_left_isotone order_lesseq_imp top_greatest)
by (metis comp_left_isotone comp_right_isotone dedekind_2 inf_commute inf_mono order_refl order_trans top_greatest)
lemma vector_inf_closed:
"vector x ⟹ vector y ⟹ vector (x ⊓ y)"
by (simp add: vector_inf_comp)
lemma vector_inf_one_comp:
"vector x ⟹ (x ⊓ 1) * y = x ⊓ y"
by (simp add: vector_inf_comp)
lemma covector_inf_comp_1:
assumes "vector x"
shows "(y ⊓ x⇧T) * z = (y ⊓ x⇧T) * (x ⊓ z)"
proof -
have "(y ⊓ x⇧T) * z ≤ (y ⊓ x⇧T) * (z ⊓ ((y⇧T ⊓ x) * top))"
by (metis inf_top_right dedekind_1 conv_dist_inf conv_involutive)
also have "... ≤ (y ⊓ x⇧T) * (x ⊓ z)"
by (metis assms comp_left_isotone comp_right_isotone inf_le2 inf_mono order_refl inf_commute)
finally show ?thesis
by (simp add: comp_right_isotone order.antisym)
qed
lemma covector_inf_comp_2:
assumes "vector x"
shows "y * (x ⊓ z) = (y ⊓ x⇧T) * (x ⊓ z)"
proof -
have "y * (x ⊓ z) ≤ (y ⊓ (top * (x ⊓ z)⇧T)) * (x ⊓ z)"
by (metis dedekind_2 inf_top_right)
also have "... ≤ (y ⊓ x⇧T) * (x ⊓ z)"
by (metis assms comp_left_isotone conv_dist_comp conv_order conv_top eq_refl inf_le1 inf_mono)
finally show ?thesis
using comp_left_subdist_inf order.antisym by auto
qed
lemma covector_inf_comp_3:
"vector x ⟹ (y ⊓ x⇧T) * z = y * (x ⊓ z)"
by (metis covector_inf_comp_1 covector_inf_comp_2)
lemma covector_inf_closed:
"covector x ⟹ covector y ⟹ covector (x ⊓ y)"
by (metis comp_right_subdist_inf order.antisym top_left_mult_increasing)
lemma vector_conv_covector:
"vector v ⟷ covector (v⇧T)"
by (metis conv_dist_comp conv_involutive conv_top)
lemma covector_conv_vector:
"covector v ⟷ vector (v⇧T)"
by (simp add: vector_conv_covector)
lemma covector_comp_inf:
"covector z ⟹ x * (y ⊓ z) = x * y ⊓ z"
apply (rule order.antisym)
apply (metis comp_isotone comp_right_subdist_inf inf.boundedE inf.boundedI inf.cobounded2 top.extremum)
by (metis comp_left_isotone comp_right_isotone dedekind_1 inf_commute inf_mono order_refl order_trans top_greatest)
lemma vector_restrict_comp_conv:
"vector x ⟹ x ⊓ y ≤ x⇧T * y"
by (metis covector_inf_comp_3 eq_refl inf.sup_monoid.add_commute inf_top_right le_supE sup.orderE top_left_mult_increasing)
lemma covector_restrict_comp_conv:
"covector x ⟹ y ⊓ x ≤ y * x⇧T"
by (metis conv_dist_comp conv_dist_inf conv_order conv_top inf.sup_monoid.add_commute vector_restrict_comp_conv)
lemma covector_comp_inf_1:
"covector x ⟹ (y ⊓ x) * z = y * (x⇧T ⊓ z)"
using covector_conv_vector covector_inf_comp_3 by fastforce
text ‹
We still have two ways to represent surjectivity and totality.
›
lemma surjective_var:
"surjective x ⟷ surjective_var x"
proof
assume "surjective x"
thus "surjective_var x"
by (metis dedekind_2 comp_left_one inf_absorb2 top_greatest)
next
assume "surjective_var x"
hence "x⇧T * (x * top) = top"
by (metis comp_left_isotone comp_associative comp_left_one top_le)
thus "surjective x"
by (metis comp_right_isotone conv_top conv_dist_comp conv_involutive top_greatest top_le)
qed
lemma total_var:
"total x ⟷ total_var x"
by (metis conv_top conv_dist_comp conv_involutive surjective_var)
lemma surjective_conv_total:
"surjective x ⟷ total (x⇧T)"
by (metis conv_top conv_dist_comp conv_involutive)
lemma total_conv_surjective:
"total x ⟷ surjective (x⇧T)"
by (simp add: surjective_conv_total)
lemma injective_conv_univalent:
"injective x ⟷ univalent (x⇧T)"
by simp
lemma univalent_conv_injective:
"univalent x ⟷ injective (x⇧T)"
by simp
text ‹
We continue with studying further closure properties.
›
lemma univalent_bot_closed:
"univalent bot"
by simp
lemma univalent_one_closed:
"univalent 1"
by simp
lemma univalent_inf_closed:
"univalent x ⟹ univalent (x ⊓ y)"
by (metis comp_left_subdist_inf comp_right_subdist_inf conv_dist_inf inf.cobounded1 order_lesseq_imp)
lemma univalent_mult_closed:
assumes "univalent x"
and "univalent y"
shows "univalent (x * y)"
proof -
have "(x * y)⇧T * x ≤ y⇧T"
by (metis assms(1) comp_left_isotone comp_right_one conv_one conv_order comp_associative conv_dist_comp conv_involutive)
thus ?thesis
by (metis assms(2) comp_left_isotone comp_associative dual_order.trans)
qed
lemma injective_bot_closed:
"injective bot"
by simp
lemma injective_one_closed:
"injective 1"
by simp
lemma injective_inf_closed:
"injective x ⟹ injective (x ⊓ y)"
by (metis conv_dist_inf injective_conv_univalent univalent_inf_closed)
lemma injective_mult_closed:
"injective x ⟹ injective y ⟹ injective (x * y)"
by (metis injective_conv_univalent conv_dist_comp univalent_mult_closed)
lemma mapping_one_closed:
"mapping 1"
by simp
lemma mapping_mult_closed:
"mapping x ⟹ mapping y ⟹ mapping (x * y)"
by (simp add: comp_associative univalent_mult_closed)
lemma bijective_one_closed:
"bijective 1"
by simp
lemma bijective_mult_closed:
"bijective x ⟹ bijective y ⟹ bijective (x * y)"
by (metis injective_mult_closed comp_associative)
lemma bijective_conv_mapping:
"bijective x ⟷ mapping (x⇧T)"
by (simp add: surjective_conv_total)
lemma mapping_conv_bijective:
"mapping x ⟷ bijective (x⇧T)"
by (simp add: total_conv_surjective)
lemma reflexive_inf_closed:
"reflexive x ⟹ reflexive y ⟹ reflexive (x ⊓ y)"
by simp
lemma reflexive_conv_closed:
"reflexive x ⟹ reflexive (x⇧T)"
using conv_isotone by force
lemma coreflexive_inf_closed:
"coreflexive x ⟹ coreflexive (x ⊓ y)"
by (simp add: le_infI1)
lemma coreflexive_conv_closed:
"coreflexive x ⟹ coreflexive (x⇧T)"
using conv_order by force
lemma coreflexive_symmetric:
"coreflexive x ⟹ symmetric x"
by (metis comp_right_one comp_right_subdist_inf conv_dist_inf conv_dist_comp conv_involutive dedekind_1 inf.absorb1 inf_absorb2)
lemma transitive_inf_closed:
"transitive x ⟹ transitive y ⟹ transitive (x ⊓ y)"
by (meson comp_left_subdist_inf inf.cobounded1 inf.sup_mono inf_le2 mult_right_isotone order.trans)
lemma transitive_conv_closed:
"transitive x ⟹ transitive (x⇧T)"
using conv_order conv_dist_comp by fastforce
lemma dense_conv_closed:
"dense_rel x ⟹ dense_rel (x⇧T)"
using conv_order conv_dist_comp by fastforce
lemma idempotent_conv_closed:
"idempotent x ⟹ idempotent (x⇧T)"
by (metis conv_dist_comp)
lemma preorder_inf_closed:
"preorder x ⟹ preorder y ⟹ preorder (x ⊓ y)"
using transitive_inf_closed by auto
lemma preorder_conv_closed:
"preorder x ⟹ preorder (x⇧T)"
by (simp add: reflexive_conv_closed transitive_conv_closed)
lemma symmetric_bot_closed:
"symmetric bot"
by simp
lemma symmetric_one_closed:
"symmetric 1"
by simp
lemma symmetric_top_closed:
"symmetric top"
by simp
lemma symmetric_inf_closed:
"symmetric x ⟹ symmetric y ⟹ symmetric (x ⊓ y)"
by (simp add: conv_dist_inf)
lemma symmetric_sup_closed:
"symmetric x ⟹ symmetric y ⟹ symmetric (x ⊔ y)"
by (simp add: conv_dist_sup)
lemma symmetric_conv_closed:
"symmetric x ⟹ symmetric (x⇧T)"
by simp
lemma one_inf_conv:
"1 ⊓ x = 1 ⊓ x⇧T"
by (metis conv_dist_inf coreflexive_symmetric inf.cobounded1 symmetric_one_closed)
lemma antisymmetric_bot_closed:
"antisymmetric bot"
by simp
lemma antisymmetric_one_closed:
"antisymmetric 1"
by simp
lemma antisymmetric_inf_closed:
"antisymmetric x ⟹ antisymmetric (x ⊓ y)"
by (rule order_trans[where y="x ⊓ x⇧T"]) (simp_all add: conv_isotone inf.coboundedI2 inf.sup_assoc)
lemma antisymmetric_conv_closed:
"antisymmetric x ⟹ antisymmetric (x⇧T)"
by (simp add: inf_commute)
lemma asymmetric_bot_closed:
"asymmetric bot"
by simp
lemma asymmetric_inf_closed:
"asymmetric x ⟹ asymmetric (x ⊓ y)"
by (metis conv_dist_inf inf.mult_zero_left inf.left_commute inf_assoc)
lemma asymmetric_conv_closed:
"asymmetric x ⟹ asymmetric (x⇧T)"
by (simp add: inf_commute)
lemma linear_top_closed:
"linear top"
by simp
lemma linear_sup_closed:
"linear x ⟹ linear (x ⊔ y)"
by (metis conv_dist_sup sup_assoc sup_commute sup_top_right)
lemma linear_reflexive:
"linear x ⟹ reflexive x"
by (metis one_inf_conv inf.distrib_left inf.cobounded2 inf.orderE reflexive_top_closed sup.idem)
lemma linear_conv_closed:
"linear x ⟹ linear (x⇧T)"
by (simp add: sup_commute)
lemma linear_comp_closed:
assumes "linear x"
and "linear y"
shows "linear (x * y)"
proof -
have "reflexive y"
by (simp add: assms(2) linear_reflexive)
hence "x ⊔ x⇧T ≤ x * y ⊔ y⇧T * x⇧T"
by (metis case_split_left case_split_right le_supI sup.cobounded1 sup.cobounded2 sup.idem reflexive_conv_closed)
thus ?thesis
by (simp add: assms(1) conv_dist_comp top_le)
qed
lemma equivalence_one_closed:
"equivalence 1"
by simp
lemma equivalence_top_closed:
"equivalence top"
by simp
lemma equivalence_inf_closed:
"equivalence x ⟹ equivalence y ⟹ equivalence (x ⊓ y)"
using conv_dist_inf preorder_inf_closed by auto
lemma equivalence_conv_closed:
"equivalence x ⟹ equivalence (x⇧T)"
by simp
lemma order_one_closed:
"order 1"
by simp
lemma order_inf_closed:
"order x ⟹ order y ⟹ order (x ⊓ y)"
using antisymmetric_inf_closed transitive_inf_closed by auto
lemma order_conv_closed:
"order x ⟹ order (x⇧T)"
by (simp add: inf_commute reflexive_conv_closed transitive_conv_closed)
lemma linear_order_conv_closed:
"linear_order x ⟹ linear_order (x⇧T)"
using equivalence_top_closed conv_dist_sup inf_commute reflexive_conv_closed transitive_conv_closed by force
text ‹
We show a fact about equivalences.
›
lemma equivalence_comp_dist_inf:
"equivalence x ⟹ x * y ⊓ x * z = x * (y ⊓ x * z)"
by (metis order.antisym comp_right_subdist_inf dedekind_1 order.eq_iff inf.absorb1 inf.absorb2 mult_1_right mult_assoc)
text ‹
The following result generalises the fact that composition with a test amounts to intersection with the corresponding vector.
Both tests and vectors can be used to represent sets as relations.
›
lemma coreflexive_comp_top_inf:
"coreflexive x ⟹ x * top ⊓ y = x * y"
apply (rule order.antisym)
apply (metis comp_left_isotone comp_left_one coreflexive_symmetric dedekind_1 inf_top_left order_trans)
using comp_left_isotone comp_right_isotone by fastforce
lemma coreflexive_comp_top_inf_one:
"coreflexive x ⟹ x * top ⊓ 1 = x"
by (simp add: coreflexive_comp_top_inf)
lemma coreflexive_comp_inf:
"coreflexive x ⟹ coreflexive y ⟹ x * y = x ⊓ y"
by (metis (full_types) coreflexive_comp_top_inf coreflexive_comp_top_inf_one inf.mult_assoc inf.absorb2)
lemma coreflexive_comp_inf_comp:
assumes "coreflexive x"
and "coreflexive y"
shows "(x * z) ⊓ (y * z) = (x ⊓ y) * z"
proof -
have "(x * z) ⊓ (y * z) = x * top ⊓ z ⊓ y * top ⊓ z"
using assms coreflexive_comp_top_inf inf_assoc by auto
also have "... = x * top ⊓ y * top ⊓ z"
by (simp add: inf.commute inf.left_commute)
also have "... = (x ⊓ y) * top ⊓ z"
by (metis assms coreflexive_comp_inf coreflexive_comp_top_inf mult_assoc)
also have "... = (x ⊓ y) * z"
by (simp add: assms(1) coreflexive_comp_top_inf coreflexive_inf_closed)
finally show ?thesis
.
qed
lemma test_comp_test_inf:
"(x ⊓ 1) * y * (z ⊓ 1) = (x ⊓ 1) * y ⊓ y * (z ⊓ 1)"
by (smt comp_right_one comp_right_subdist_inf coreflexive_comp_top_inf inf.left_commute inf.orderE inf_le2 mult_assoc)
lemma test_comp_test_top:
"y ⊓ (x ⊓ 1) * top * (z ⊓ 1) = (x ⊓ 1) * y * (z ⊓ 1)"
proof -
have "∀u v . (v ⊓ u⇧T)⇧T = v⇧T ⊓ u"
using conv_dist_inf by auto
thus ?thesis
by (smt conv_dist_comp conv_involutive coreflexive_comp_top_inf inf.cobounded2 inf.left_commute inf.sup_monoid.add_commute symmetric_one_closed mult_assoc symmetric_top_closed)
qed
lemma coreflexive_idempotent:
"coreflexive x ⟹ idempotent x"
by (simp add: coreflexive_comp_inf)
lemma coreflexive_univalent:
"coreflexive x ⟹ univalent x"
by (simp add: coreflexive_idempotent coreflexive_symmetric)
lemma coreflexive_injective:
"coreflexive x ⟹ injective x"
by (simp add: coreflexive_idempotent coreflexive_symmetric)
lemma coreflexive_commutative:
"coreflexive x ⟹ coreflexive y ⟹ x * y = y * x"
by (simp add: coreflexive_comp_inf inf.commute)
lemma coreflexive_dedekind:
"coreflexive x ⟹ coreflexive y ⟹ coreflexive z ⟹ x * y ⊓ z ≤ x * (y ⊓ x * z)"
by (simp add: coreflexive_comp_inf inf.coboundedI1 inf.left_commute)
text ‹
Also the equational version of the Dedekind rule continues to hold.
›
lemma dedekind_eq:
"x * y ⊓ z = (x ⊓ (z * y⇧T)) * (y ⊓ (x⇧T * z)) ⊓ z"
proof (rule order.antisym)
have "x * y ⊓ z ≤ x * (y ⊓ (x⇧T * z)) ⊓ z"
by (simp add: dedekind_1)
also have "... ≤ (x ⊓ (z * (y ⊓ (x⇧T * z))⇧T)) * (y ⊓ (x⇧T * z)) ⊓ z"
by (simp add: dedekind_2)
also have "... ≤ (x ⊓ (z * y⇧T)) * (y ⊓ (x⇧T * z)) ⊓ z"
by (metis comp_left_isotone comp_right_isotone inf_mono conv_order inf.cobounded1 order_refl)
finally show "x * y ⊓ z ≤ (x ⊓ (z * y⇧T)) * (y ⊓ (x⇧T * z)) ⊓ z"
.
next
show "(x ⊓ (z * y⇧T)) * (y ⊓ (x⇧T * z)) ⊓ z ≤ x * y ⊓ z"
using comp_isotone inf.sup_left_isotone by auto
qed
lemma dedekind:
"x * y ⊓ z ≤ (x ⊓ (z * y⇧T)) * (y ⊓ (x⇧T * z))"
by (metis dedekind_eq inf.cobounded1)
lemma vector_export_comp:
"(x * top ⊓ y) * z = x * top ⊓ y * z"
proof -
have "vector (x * top)"
by (simp add: comp_associative)
thus ?thesis
by (simp add: vector_inf_comp)
qed
lemma vector_export_comp_unit:
"(x * top ⊓ 1) * y = x * top ⊓ y"
by (simp add: vector_export_comp)
text ‹
We solve a few exercises from \<^cite>‹"SchmidtStroehlein1993"›.
›
lemma ex231a [simp]:
"(1 ⊓ x * x⇧T) * x = x"
by (metis inf.cobounded1 inf.idem inf_right_idem comp_left_one conv_one coreflexive_comp_top_inf dedekind_eq)
lemma ex231b [simp]:
"x * (1 ⊓ x⇧T * x) = x"
by (metis conv_dist_comp conv_dist_inf conv_involutive conv_one ex231a)
lemma ex231c:
"x ≤ x * x⇧T * x"
by (metis comp_left_isotone ex231a inf_le2)
lemma ex231d:
"x ≤ x * top * x"
by (metis comp_left_isotone comp_right_isotone top_greatest order_trans ex231c)
lemma ex231e [simp]:
"x * top * x * top = x * top"
by (metis ex231d order.antisym comp_associative mult_right_isotone top.extremum)
lemma arc_injective:
"arc x ⟹ injective x"
by (metis conv_dist_inf conv_involutive inf.absorb2 top_right_mult_increasing univalent_inf_closed)
lemma arc_conv_closed:
"arc x ⟹ arc (x⇧T)"
by simp
lemma arc_univalent:
"arc x ⟹ univalent x"
using arc_conv_closed arc_injective univalent_conv_injective by blast
lemma injective_codomain:
assumes "injective x"
shows "x * (x ⊓ 1) = x ⊓ 1"
proof (rule order.antisym)
show "x * (x ⊓ 1) ≤ x ⊓ 1"
by (metis assms comp_right_one dual_order.trans inf.boundedI inf.cobounded1 inf.sup_monoid.add_commute mult_right_isotone one_inf_conv)
next
show "x ⊓ 1 ≤ x * (x ⊓ 1)"
by (metis coreflexive_idempotent inf.cobounded1 inf.cobounded2 mult_left_isotone)
qed
text ‹
The following result generalises \<^cite>‹‹Exercise 2› in "Oliveira2009"›.
It is used to show that the while-loop preserves injectivity of the constructed tree.
›
lemma injective_sup:
assumes "injective t"
and "e * t⇧T ≤ 1"
and "injective e"
shows "injective (t ⊔ e)"
proof -
have "(t ⊔ e) * (t ⊔ e)⇧T = t * t⇧T ⊔ t * e⇧T ⊔ e * t⇧T ⊔ e * e⇧T"
by (simp add: comp_left_dist_sup conv_dist_sup semiring.distrib_right sup.assoc)
thus ?thesis
using assms coreflexive_symmetric conv_dist_comp by fastforce
qed
lemma injective_inv:
"injective t ⟹ e * t⇧T = bot ⟹ arc e ⟹ injective (t ⊔ e)"
using arc_injective injective_sup bot_least by blast
lemma univalent_sup:
"univalent t ⟹ e⇧T * t ≤ 1 ⟹ univalent e ⟹ univalent (t ⊔ e)"
by (metis injective_sup conv_dist_sup conv_involutive)
lemma point_injective:
"arc x ⟹ x⇧T * top * x ≤ 1"
by (metis conv_top comp_associative conv_dist_comp conv_involutive vector_top_closed)
lemma vv_transitive:
"vector v ⟹ (v * v⇧T) * (v * v⇧T) ≤ v * v⇧T"
by (metis comp_associative comp_left_isotone comp_right_isotone top_greatest)
lemma epm_3:
assumes "e ≤ w"
and "injective w"
shows "e = w ⊓ top * e"
proof -
have "w ⊓ top * e ≤ w * e⇧T * e"
by (metis (no_types, lifting) inf.absorb2 top.extremum dedekind_2 inf.commute)
also have "... ≤ w * w⇧T * e"
by (simp add: assms(1) conv_isotone mult_left_isotone mult_right_isotone)
also have "... ≤ e"
using assms(2) coreflexive_comp_top_inf inf.sup_right_divisibility by blast
finally show ?thesis
by (simp add: assms(1) top_left_mult_increasing order.antisym)
qed
lemma comp_inf_vector:
"x * (y ⊓ z * top) = (x ⊓ top * z⇧T) * y"
by (metis conv_top covector_inf_comp_3 comp_associative conv_dist_comp inf.commute vector_top_closed)
lemma inf_vector_comp:
"(x ⊓ y * top) * z = y * top ⊓ x * z"
using inf.commute vector_export_comp by auto
lemma comp_inf_covector:
"x * (y ⊓ top * z) = x * y ⊓ top * z"
by (simp add: covector_comp_inf covector_mult_closed)
text ‹
Well-known distributivity properties of univalent and injective relations over meet continue to hold.
›
lemma univalent_comp_left_dist_inf:
assumes "univalent x"
shows "x * (y ⊓ z) = x * y ⊓ x * z"
proof (rule order.antisym)
show "x * (y ⊓ z) ≤ x * y ⊓ x * z"
by (simp add: comp_right_isotone)
next
have "x * y ⊓ x * z ≤ (x ⊓ x * z * y⇧T) * (y ⊓ x⇧T * x * z)"
by (metis comp_associative dedekind)
also have "... ≤ x * (y ⊓ x⇧T * x * z)"
by (simp add: comp_left_isotone)
also have "... ≤ x * (y ⊓ 1 * z)"
using assms comp_left_isotone comp_right_isotone inf.sup_right_isotone by blast
finally show "x * y ⊓ x * z ≤ x * (y ⊓ z)"
by simp
qed
lemma injective_comp_right_dist_inf:
"injective z ⟹ (x ⊓ y) * z = x * z ⊓ y * z"
by (metis univalent_comp_left_dist_inf conv_dist_comp conv_involutive conv_dist_inf)
lemma vector_covector:
"vector v ⟹ vector w ⟹ v ⊓ w⇧T = v * w⇧T"
by (metis covector_comp_inf inf_top_left vector_conv_covector)
lemma comp_inf_vector_1:
"(x ⊓ top * y) * z = x * (z ⊓ (top * y)⇧T)"
by (simp add: comp_inf_vector conv_dist_comp)
text ‹
The shunting properties for bijective relations and mappings continue to hold.
›
lemma shunt_bijective:
assumes "bijective z"
shows "x ≤ y * z ⟷ x * z⇧T ≤ y"
proof
assume "x ≤ y * z"
hence "x * z⇧T ≤ y * z * z⇧T"
by (simp add: mult_left_isotone)
also have "... ≤ y"
using assms comp_associative mult_right_isotone by fastforce
finally show "x * z⇧T ≤ y"
.
next
assume 1: "x * z⇧T ≤ y"
have "x = x ⊓ top * z"
by (simp add: assms)
also have "... ≤ x * z⇧T * z"
by (metis dedekind_2 inf_commute inf_top.right_neutral)
also have "... ≤ y * z"
using 1 by (simp add: mult_left_isotone)
finally show "x ≤ y * z"
.
qed
lemma shunt_mapping:
"mapping z ⟹ x ≤ z * y ⟷ z⇧T * x ≤ y"
by (metis shunt_bijective mapping_conv_bijective conv_order conv_dist_comp conv_involutive)
lemma bijective_reverse:
assumes "bijective p"
and "bijective q"
shows "p ≤ r * q ⟷ q ≤ r⇧T * p"
proof -
have "p ≤ r * q ⟷ p * q⇧T ≤ r"
by (simp add: assms(2) shunt_bijective)
also have "... ⟷ q⇧T ≤ p⇧T * r"
by (metis assms(1) conv_dist_comp conv_involutive conv_order shunt_bijective)
also have "... ⟷ q ≤ r⇧T * p"
using conv_dist_comp conv_isotone by fastforce
finally show ?thesis
by simp
qed
lemma arc_expanded:
"arc x ⟷ x * top * x⇧T ≤ 1 ∧ x⇧T * top * x ≤ 1 ∧ top * x * top = top"
by (metis conv_top comp_associative conv_dist_comp conv_involutive vector_top_closed)
lemma arc_top_arc:
assumes "arc x"
shows "x * top * x = x"
by (metis assms epm_3 top_right_mult_increasing vector_inf_comp vector_mult_closed vector_top_closed)
lemma arc_top_edge:
assumes "arc x"
shows "x⇧T * top * x = x⇧T * x"
proof -
have "x⇧T = x⇧T * top ⊓ top * x⇧T"
using assms epm_3 top_right_mult_increasing by simp
thus ?thesis
by (metis comp_inf_vector_1 conv_dist_comp conv_involutive conv_top inf.absorb1 top_right_mult_increasing)
qed
text ‹Lemmas ‹arc_eq_1› and ‹arc_eq_2› were contributed by Nicolas Robinson-O'Brien.›
lemma arc_eq_1:
assumes "arc x"
shows "x = x * x⇧T * x"
proof -
have "x * x⇧T * x ≤ x * top * x"
by (simp add: mult_left_isotone mult_right_isotone)
also have "... ≤ x"
by (simp add: assms arc_top_arc)
finally have "x * x⇧T * x ≤ x"
by simp
thus ?thesis
by (simp add: order.antisym ex231c)
qed
lemma arc_eq_2:
assumes "arc x"
shows "x⇧T = x⇧T * x * x⇧T"
using arc_eq_1 assms conv_involutive by fastforce
lemma points_arc:
"point x ⟹ point y ⟹ arc (x * y⇧T)"
by (metis comp_associative conv_dist_comp conv_involutive equivalence_top_closed)
lemma point_arc:
"point x ⟹ arc (x * x⇧T)"
by (simp add: points_arc)
lemma arc_expanded_1:
"arc e ⟹ e * x * e⇧T ≤ 1"
by (meson arc_expanded order_trans top_greatest mult_left_isotone mult_right_isotone)
lemma arc_expanded_2:
"arc e ⟹ e⇧T * x * e ≤ 1"
by (meson arc_expanded order_trans top_greatest mult_left_isotone mult_right_isotone)
lemma point_conv_comp:
"point x ⟹ x⇧T * x = top"
using order_eq_iff shunt_bijective top_greatest vector_conv_covector by blast
lemma point_antisymmetric:
"point x ⟹ antisymmetric x"
by (simp add: vector_covector)
lemma mapping_inf_point_arc:
assumes "mapping x"
and "point y"
shows "arc (x ⊓ y)"
proof (unfold arc_expanded, intro conjI)
show "(x ⊓ y) * top * (x ⊓ y)⇧T ≤ 1"
by (metis assms conv_dist_comp covector_conv_vector inf.orderE inf.sup_monoid.add_commute surjective_conv_total top.extremum top_right_mult_increasing vector_export_comp)
have "(x ⊓ y)⇧T * top * (x ⊓ y) = x⇧T * y * (x ⊓ y)"
by (simp add: assms(2) conv_dist_inf covector_inf_comp_3)
also have "... = x⇧T * (y ⊓ y⇧T) * x"
by (simp add: assms(2) comp_associative covector_inf_comp_3 inf.sup_monoid.add_commute)
also have "... ≤ x⇧T * x"
by (metis assms(2) comp_right_one mult_left_isotone mult_right_isotone vector_covector)
also have "... ≤ 1"
by (simp add: assms(1))
finally show "(x ⊓ y)⇧T * top * (x ⊓ y) ≤ 1"
.
show "top * (x ⊓ y) * top = top"
by (metis assms inf_top_right inf_vector_comp mult_assoc)
qed
lemma univalent_power_closed:
"univalent x ⟹ univalent (x ^ n)"
apply (rule monoid_power_closed)
using univalent_mult_closed by auto
lemma injective_power_closed:
"injective x ⟹ injective (x ^ n)"
apply (rule monoid_power_closed)
using injective_mult_closed by auto
lemma mapping_power_closed:
"mapping x ⟹ mapping (x ^ n)"
apply (rule monoid_power_closed)
using mapping_mult_closed by auto
lemma bijective_power_closed:
"bijective x ⟹ bijective (x ^ n)"
apply (rule monoid_power_closed)
using bijective_mult_closed by auto
lemma power_conv_commute:
"x⇧T ^ n = (x ^ n)⇧T"
proof (induct n)
case 0
thus ?case
by simp
next
case (Suc n)
thus ?case
using conv_dist_comp power_Suc2 by force
qed
end
subsection ‹Single-Object Pseudocomplemented Distributive Allegories›
text ‹
We extend single-object bounded distributive allegories by a pseudocomplement operation.
The following definitions concern properties of relations that require a pseudocomplement.
›
class relation_algebra_signature = bounded_distrib_allegory_signature + uminus
begin
abbreviation irreflexive :: "'a ⇒ bool" where "irreflexive x ≡ x ≤ -1"
abbreviation strict_linear :: "'a ⇒ bool" where "strict_linear x ≡ x ⊔ x⇧T = -1"
abbreviation strict_order :: "'a ⇒ bool" where "strict_order x ≡ irreflexive x ∧ transitive x"
abbreviation linear_strict_order :: "'a ⇒ bool" where "linear_strict_order x ≡ strict_order x ∧ strict_linear x"
text ‹
The following variants are useful for the graph model.
›
abbreviation pp_mapping :: "'a ⇒ bool" where "pp_mapping x ≡ univalent x ∧ total (--x)"
abbreviation pp_bijective :: "'a ⇒ bool" where "pp_bijective x ≡ injective x ∧ surjective (--x)"
abbreviation pp_point :: "'a ⇒ bool" where "pp_point x ≡ vector x ∧ pp_bijective x"
abbreviation pp_arc :: "'a ⇒ bool" where "pp_arc x ≡ pp_bijective (x * top) ∧ pp_bijective (x⇧T * top)"
end
class pd_allegory = bounded_distrib_allegory + p_algebra
begin
subclass relation_algebra_signature .
subclass pd_algebra ..
lemma conv_complement_1:
"-(x⇧T) ⊔ (-x)⇧T = (-x)⇧T"
by (metis conv_dist_inf conv_order bot_least conv_involutive pseudo_complement sup.absorb2 sup.cobounded2)
lemma conv_complement:
"(-x)⇧T = -(x⇧T)"
by (metis conv_complement_1 conv_dist_sup conv_involutive sup_commute)
lemma conv_complement_sub_inf [simp]:
"x⇧T * -(x * y) ⊓ y = bot"
by (metis comp_left_zero conv_dist_comp conv_involutive dedekind_1 inf_import_p inf_p inf_right_idem ppp pseudo_complement regular_closed_bot)
lemma conv_complement_sub_leq:
"x⇧T * -(x * y) ≤ -y"
using pseudo_complement conv_complement_sub_inf by blast
lemma conv_complement_sub [simp]:
"x⇧T * -(x * y) ⊔ -y = -y"
by (simp add: conv_complement_sub_leq sup.absorb2)
lemma complement_conv_sub:
"-(y * x) * x⇧T ≤ -y"
by (metis conv_complement conv_complement_sub_leq conv_order conv_dist_comp)
text ‹
The following so-called Schr\"oder equivalences, or De Morgan's Theorem K, hold only with a pseudocomplemented element on both right-hand sides.
›
lemma schroeder_3_p:
"x * y ≤ -z ⟷ x⇧T * z ≤ -y"
using pseudo_complement schroeder_1 by auto
lemma schroeder_4_p:
"x * y ≤ -z ⟷ z * y⇧T ≤ -x"
using pseudo_complement schroeder_2 by auto
lemma comp_pp_semi_commute:
"x * --y ≤ --(x * y)"
using conv_complement_sub_leq schroeder_3_p by fastforce
text ‹
The following result looks similar to a property of (anti)domain.
›
lemma p_comp_pp [simp]:
"-(x * --y) = -(x * y)"
using comp_pp_semi_commute comp_right_isotone order.eq_iff p_antitone pp_increasing by fastforce
lemma pp_comp_semi_commute:
"--x * y ≤ --(x * y)"
using complement_conv_sub schroeder_4_p by fastforce
lemma p_pp_comp [simp]:
"-(--x * y) = -(x * y)"
using pp_comp_semi_commute comp_left_isotone order.eq_iff p_antitone pp_increasing by fastforce
lemma pp_comp_subdist:
"--x * --y ≤ --(x * y)"
by (simp add: p_antitone_iff)
lemma theorem24xxiii:
"x * y ⊓ -(x * z) = x * (y ⊓ -z) ⊓ -(x * z)"
proof -
have "x * y ⊓ -(x * z) ≤ x * (y ⊓ (x⇧T * -(x * z)))"
by (simp add: dedekind_1)
also have "... ≤ x * (y ⊓ -z)"
using comp_right_isotone conv_complement_sub_leq inf.sup_right_isotone by auto
finally show ?thesis
using comp_right_subdist_inf order.antisym inf.coboundedI2 inf.commute by auto
qed
text ‹
Even in Stone relation algebras, we do not obtain the backward implication in the following result.
›
lemma vector_complement_closed:
"vector x ⟹ vector (-x)"
by (metis complement_conv_sub conv_top order.eq_iff top_right_mult_increasing)
lemma covector_complement_closed:
"covector x ⟹ covector (-x)"
by (metis conv_complement_sub_leq conv_top order.eq_iff top_left_mult_increasing)
lemma covector_vector_comp:
"vector v ⟹ -v⇧T * v = bot"
by (metis conv_bot conv_complement conv_complement_sub_inf conv_dist_comp conv_involutive inf_top.right_neutral)
lemma irreflexive_bot_closed:
"irreflexive bot"
by simp
lemma irreflexive_inf_closed:
"irreflexive x ⟹ irreflexive (x ⊓ y)"
by (simp add: le_infI1)
lemma irreflexive_sup_closed:
"irreflexive x ⟹ irreflexive y ⟹ irreflexive (x ⊔ y)"
by simp
lemma irreflexive_conv_closed:
"irreflexive x ⟹ irreflexive (x⇧T)"
using conv_complement conv_isotone by fastforce
lemma reflexive_complement_irreflexive:
"reflexive x ⟹ irreflexive (-x)"
by (simp add: p_antitone)
lemma irreflexive_complement_reflexive:
"irreflexive x ⟷ reflexive (-x)"
by (simp add: p_antitone_iff)
lemma symmetric_complement_closed:
"symmetric x ⟹ symmetric (-x)"
by (simp add: conv_complement)
lemma asymmetric_irreflexive:
"asymmetric x ⟹ irreflexive x"
by (metis inf.mult_not_zero inf.left_commute inf.right_idem inf.sup_monoid.add_commute pseudo_complement one_inf_conv)
lemma linear_asymmetric:
"linear x ⟹ asymmetric (-x)"
using conv_complement p_top by force
lemma strict_linear_sup_closed:
"strict_linear x ⟹ strict_linear y ⟹ strict_linear (x ⊔ y)"
by (metis (mono_tags, opaque_lifting) conv_dist_sup sup.right_idem sup_assoc sup_commute)
lemma strict_linear_irreflexive:
"strict_linear x ⟹ irreflexive x"
using sup_left_divisibility by blast
lemma strict_linear_conv_closed:
"strict_linear x ⟹ strict_linear (x⇧T)"
by (simp add: sup_commute)
lemma strict_order_var:
"strict_order x ⟷ asymmetric x ∧ transitive x"
by (metis asymmetric_irreflexive comp_right_one irreflexive_conv_closed conv_dist_comp dual_order.trans pseudo_complement schroeder_3_p)
lemma strict_order_bot_closed:
"strict_order bot"
by simp
lemma strict_order_inf_closed:
"strict_order x ⟹ strict_order y ⟹ strict_order (x ⊓ y)"
using inf.coboundedI1 transitive_inf_closed by auto
lemma strict_order_conv_closed:
"strict_order x ⟹ strict_order (x⇧T)"
using irreflexive_conv_closed transitive_conv_closed by blast
lemma order_strict_order:
assumes "order x"
shows "strict_order (x ⊓ -1)"
proof (rule conjI)
show 1: "irreflexive (x ⊓ -1)"
by simp
have "antisymmetric (x ⊓ -1)"
using antisymmetric_inf_closed assms by blast
hence "(x ⊓ -1) * (x ⊓ -1) ⊓ 1 ≤ (x ⊓ -1 ⊓ (x ⊓ -1)⇧T) * (x ⊓ -1 ⊓ (x ⊓ -1)⇧T)"
using 1 by (metis (no_types) coreflexive_symmetric irreflexive_inf_closed coreflexive_transitive dedekind_1 inf_idem mult_1_right semiring.mult_not_zero strict_order_var)
also have "... = (x ⊓ x⇧T ⊓ -1) * (x ⊓ x⇧T ⊓ -1)"
by (simp add: conv_complement conv_dist_inf inf.absorb2 inf.sup_monoid.add_assoc)
also have "... = bot"
using assms order.antisym reflexive_conv_closed by fastforce
finally have "(x ⊓ -1) * (x ⊓ -1) ≤ -1"
using le_bot pseudo_complement by blast
thus "transitive (x ⊓ -1)"
by (meson assms comp_isotone inf.boundedI inf.cobounded1 inf.order_lesseq_imp)
qed
lemma strict_order_order:
"strict_order x ⟹ order (x ⊔ 1)"
apply (unfold strict_order_var, intro conjI)
apply simp
apply (simp add: mult_left_dist_sup mult_right_dist_sup sup.absorb2)
using conv_dist_sup coreflexive_bot_closed sup.absorb2 sup_inf_distrib2 by fastforce
lemma linear_strict_order_conv_closed:
"linear_strict_order x ⟹ linear_strict_order (x⇧T)"
by (simp add: irreflexive_conv_closed sup_monoid.add_commute transitive_conv_closed)
lemma linear_order_strict_order:
"linear_order x ⟹ linear_strict_order (x ⊓ -1)"
apply (rule conjI)
using order_strict_order apply simp
by (metis conv_complement conv_dist_inf coreflexive_symmetric order.eq_iff inf.absorb2 inf.distrib_left inf.sup_monoid.add_commute top.extremum)
lemma regular_conv_closed:
"regular x ⟹ regular (x⇧T)"
by (metis conv_complement)
text ‹
We show a number of facts about equivalences.
›
lemma equivalence_comp_left_complement:
"equivalence x ⟹ x * -x = -x"
apply (rule order.antisym)
apply (metis conv_complement_sub_leq preorder_idempotent)
using mult_left_isotone by fastforce
lemma equivalence_comp_right_complement:
"equivalence x ⟹ -x * x = -x"
by (metis equivalence_comp_left_complement conv_complement conv_dist_comp)
text ‹
The pseudocomplement of tests is given by the following operation.
›
abbreviation coreflexive_complement :: "'a ⇒ 'a" ("_ ''" [80] 80)
where "x ' ≡ -x ⊓ 1"
lemma coreflexive_comp_top_coreflexive_complement:
"coreflexive x ⟹ (x * top)' = x '"
by (metis coreflexive_comp_top_inf_one inf.commute inf_import_p)
lemma coreflexive_comp_inf_complement:
"coreflexive x ⟹ (x * y) ⊓ -z = (x * y) ⊓ -(x * z)"
by (metis coreflexive_comp_top_inf inf.sup_relative_same_increasing inf_import_p inf_le1)
lemma double_coreflexive_complement:
"x '' = (-x)'"
using inf.sup_monoid.add_commute inf_import_p by auto
lemma coreflexive_pp_dist_comp:
assumes "coreflexive x"
and "coreflexive y"
shows "(x * y)'' = x '' * y ''"
proof -
have "(x * y)'' = --(x * y) ⊓ 1"
by (simp add: double_coreflexive_complement)
also have "... = --x ⊓ --y ⊓ 1"
by (simp add: assms coreflexive_comp_inf)
also have "... = (--x ⊓ 1) * (--y ⊓ 1)"
by (simp add: coreflexive_comp_inf inf.left_commute inf.sup_monoid.add_assoc)
also have "... = x '' * y ''"
by (simp add: double_coreflexive_complement)
finally show ?thesis
.
qed
lemma coreflexive_pseudo_complement:
"coreflexive x ⟹ x ⊓ y = bot ⟷ x ≤ y '"
by (simp add: pseudo_complement)
lemma pp_bijective_conv_mapping:
"pp_bijective x ⟷ pp_mapping (x⇧T)"
by (simp add: conv_complement surjective_conv_total)
lemma pp_arc_expanded:
"pp_arc x ⟷ x * top * x⇧T ≤ 1 ∧ x⇧T * top * x ≤ 1 ∧ top * --x * top = top"
proof
assume 1: "pp_arc x"
have 2: "x * top * x⇧T ≤ 1"
using 1 by (metis comp_associative conv_dist_comp equivalence_top_closed vector_top_closed)
have 3: "x⇧T * top * x ≤ 1"
using 1 by (metis conv_dist_comp conv_involutive equivalence_top_closed vector_top_closed mult_assoc)
have 4: "x⇧T ≤ x⇧T * x * x⇧T"
by (metis conv_involutive ex231c)
have "top = --(top * x) * top"
using 1 by (metis conv_complement conv_dist_comp conv_involutive equivalence_top_closed)
also have "... ≤ --(top * x⇧T * top * x) * top"
using 1 by (metis eq_refl mult_assoc p_comp_pp p_pp_comp)
also have "... = (top * --(x * top) ⊓ --(top * x⇧T * top * x)) * top"
using 1 by simp
also have "... = top * (--(x * top) ⊓ --(top * x⇧T * top * x)) * top"
by (simp add: covector_complement_closed covector_comp_inf covector_mult_closed)
also have "... = top * --(x * top ⊓ top * x⇧T * top * x) * top"
by simp
also have "... = top * --(x * top * x⇧T * top * x) * top"
by (metis comp_associative comp_inf_covector inf_top.left_neutral)
also have "... ≤ top * --(x * top * x⇧T * x * x⇧T * top * x) * top"
using 4 by (metis comp_associative comp_left_isotone comp_right_isotone pp_isotone)
also have "... ≤ top * --(x * x⇧T * top * x) * top"
using 2 by (metis comp_associative comp_left_isotone comp_right_isotone pp_isotone comp_left_one)
also have "... ≤ top * --x * top"
using 3 by (metis comp_associative comp_left_isotone comp_right_isotone pp_isotone comp_right_one)
finally show "x * top * x⇧T ≤ 1 ∧ x⇧T * top * x ≤ 1 ∧ top * --x * top = top"
using 2 3 top_le by blast
next
assume "x * top * x⇧T ≤ 1 ∧ x⇧T * top * x ≤ 1 ∧ top * --x * top = top"
thus "pp_arc x"
apply (intro conjI)
apply (metis comp_associative conv_dist_comp equivalence_top_closed vector_top_closed)
apply (metis comp_associative mult_right_isotone top_le pp_comp_semi_commute)
apply (metis conv_dist_comp coreflexive_symmetric vector_conv_covector vector_top_closed mult_assoc)
by (metis conv_complement conv_dist_comp equivalence_top_closed inf.orderE inf_top.left_neutral mult_right_isotone pp_comp_semi_commute)
qed
text ‹
The following operation represents states with infinite executions of non-strict computations.
›
abbreviation N :: "'a ⇒ 'a"
where "N x ≡ -(-x * top) ⊓ 1"
lemma N_comp:
"N x * y = -(-x * top) ⊓ y"
by (simp add: vector_mult_closed vector_complement_closed vector_inf_one_comp)
lemma N_comp_top [simp]:
"N x * top = -(-x * top)"
by (simp add: N_comp)
lemma vector_N_pp:
"vector x ⟹ N x = --x ⊓ 1"
by (simp add: vector_complement_closed)
lemma N_vector_pp [simp]:
"N (x * top) = --(x * top) ⊓ 1"
by (simp add: comp_associative vector_complement_closed)
lemma N_vector_top_pp [simp]:
"N (x * top) * top = --(x * top)"
by (metis N_comp_top comp_associative vector_top_closed vector_complement_closed)
lemma N_below_inf_one_pp:
"N x ≤ --x ⊓ 1"
using inf.sup_left_isotone p_antitone top_right_mult_increasing by auto
lemma N_below_pp:
"N x ≤ --x"
using N_below_inf_one_pp by auto
lemma N_comp_N:
"N x * N y = -(-x * top) ⊓ -(-y * top) ⊓ 1"
by (simp add: N_comp inf.mult_assoc)
lemma N_bot [simp]:
"N bot = bot"
by simp
lemma N_top [simp]:
"N top = 1"
by simp
lemma n_split_omega_mult_pp:
"xs * --xo = xo ⟹ vector xo ⟹ N top * xo = xs * N xo * top"
by (metis N_top N_vector_top_pp comp_associative comp_left_one)
text ‹
Many of the following results have been derived for verifying Prim's minimum spanning tree algorithm.
›
lemma ee:
assumes "vector v"
and "e ≤ v * -v⇧T"
shows "e * e = bot"
proof -
have "e * v ≤ bot"
by (metis assms covector_vector_comp comp_associative mult_left_isotone mult_right_zero)
thus ?thesis
by (metis assms(2) bot_unique comp_associative mult_right_isotone semiring.mult_not_zero)
qed
lemma et:
assumes "vector v"
and "e ≤ v * -v⇧T"
and "t ≤ v * v⇧T"
shows "e * t = bot"
and "e * t⇧T = bot"
proof -
have "e * t ≤ v * -v⇧T * v * v⇧T"
using assms(2-3) comp_isotone mult_assoc by fastforce
thus "e * t = bot"
by (simp add: assms(1) covector_vector_comp le_bot mult_assoc)
next
have "t⇧T ≤ v * v⇧T"
using assms(3) conv_order conv_dist_comp by fastforce
hence "e * t⇧T ≤ v * -v⇧T * v * v⇧T"
by (metis assms(2) comp_associative comp_isotone)
thus "e * t⇧T = bot"
by (simp add: assms(1) covector_vector_comp le_bot mult_assoc)
qed
lemma ve_dist:
assumes "e ≤ v * -v⇧T"
and "vector v"
and "arc e"
shows "(v ⊔ e⇧T * top) * (v ⊔ e⇧T * top)⇧T = v * v⇧T ⊔ v * v⇧T * e ⊔ e⇧T * v * v⇧T ⊔ e⇧T * e"
proof -
have "e ≤ v * top"
using assms(1) comp_right_isotone dual_order.trans top_greatest by blast
hence "v * top * e = v * top * (v * top ⊓ e)"
by (simp add: inf.absorb2)
also have "... = (v * top ⊓ top * v⇧T) * e"
using assms(2) covector_inf_comp_3 vector_conv_covector by force
also have "... = v * top * v⇧T * e"
by (metis assms(2) inf_top_right vector_inf_comp)
also have "... = v * v⇧T * e"
by (simp add: assms(2))
finally have 1: "v * top * e = v * v⇧T * e"
.
have "e⇧T * top * e ≤ e⇧T * top * e * e⇧T * e"
using ex231c comp_associative mult_right_isotone by auto
also have "... ≤ e⇧T * e"
by (metis assms(3) coreflexive_comp_top_inf le_infE mult_semi_associative point_injective)
finally have 2: "e⇧T * top * e = e⇧T * e"
by (simp add: order.antisym mult_left_isotone top_right_mult_increasing)
have "(v ⊔ e⇧T * top) * (v ⊔ e⇧T * top)⇧T = (v ⊔ e⇧T * top) * (v⇧T ⊔ top * e)"
by (simp add: conv_dist_comp conv_dist_sup)
also have "... = v * v⇧T ⊔ v * top * e ⊔ e⇧T * top * v⇧T ⊔ e⇧T * top * top * e"
by (metis semiring.distrib_left semiring.distrib_right sup_assoc mult_assoc)
also have "... = v * v⇧T ⊔ v * top * e ⊔ (v * top * e)⇧T ⊔ e⇧T * top * e"
by (simp add: comp_associative conv_dist_comp)
also have "... = v * v⇧T ⊔ v * v⇧T * e ⊔ (v * v⇧T * e)⇧T ⊔ e⇧T * e"
using 1 2 by simp
finally show ?thesis
by (simp add: comp_associative conv_dist_comp)
qed
lemma ev:
"vector v ⟹ e ≤ v * -v⇧T ⟹ e * v = bot"
by (metis covector_vector_comp order.antisym bot_least comp_associative mult_left_isotone mult_right_zero)
lemma vTeT:
"vector v ⟹ e ≤ v * -v⇧T ⟹ v⇧T * e⇧T = bot"
using conv_bot ev conv_dist_comp by fastforce
text ‹
The following result is used to show that the while-loop of Prim's algorithm preserves that the constructed tree is a subgraph of g.
›
lemma prim_subgraph_inv:
assumes "e ≤ v * -v⇧T ⊓ g"
and "t ≤ v * v⇧T ⊓ g"
shows "t ⊔ e ≤ ((v ⊔ e⇧T * top) * (v ⊔ e⇧T * top)⇧T) ⊓ g"
proof (rule sup_least)
have "t ≤ ((v ⊔ e⇧T * top) * v⇧T) ⊓ g"
using assms(2) le_supI1 mult_right_dist_sup by auto
also have "... ≤ ((v ⊔ e⇧T * top) * (v ⊔ e⇧T * top)⇧T) ⊓ g"
using comp_right_isotone conv_dist_sup inf.sup_left_isotone by auto
finally show "t ≤ ((v ⊔ e⇧T * top) * (v ⊔ e⇧T * top)⇧T) ⊓ g"
.
next
have "e ≤ v * top"
by (meson assms(1) inf.boundedE mult_right_isotone order.trans top.extremum)
hence "e ≤ v * top ⊓ top * e"
by (simp add: top_left_mult_increasing)
also have "... = v * top * e"
by (metis inf_top_right vector_export_comp)
finally have "e ≤ v * top * e ⊓ g"
using assms(1) by auto
also have "... = v * (e⇧T * top)⇧T ⊓ g"
by (simp add: comp_associative conv_dist_comp)
also have "... ≤ v * (v ⊔ e⇧T * top)⇧T ⊓ g"
by (simp add: conv_dist_sup mult_left_dist_sup sup.assoc sup.orderI)
also have "... ≤ (v ⊔ e⇧T * top) * (v ⊔ e⇧T * top)⇧T ⊓ g"
using inf.sup_left_isotone mult_right_sub_dist_sup_left by auto
finally show "e ≤ ((v ⊔ e⇧T * top) * (v ⊔ e⇧T * top)⇧T) ⊓ g"
.
qed
text ‹
The following result shows how to apply the Schr\"oder equivalence to the middle factor in a composition of three relations.
Again the elements on the right-hand side need to be pseudocomplemented.
›
lemma triple_schroeder_p:
"x * y * z ≤ -w ⟷ x⇧T * w * z⇧T ≤ -y"
using mult_assoc p_antitone_iff schroeder_3_p schroeder_4_p by auto
text ‹
The rotation versions of the Schr\"oder equivalences continue to hold, again with pseudocomplemented elements on the right-hand side.
›
lemma schroeder_5_p:
"x * y ≤ -z ⟷ y * z⇧T ≤ -x⇧T"
using schroeder_3_p schroeder_4_p by auto
lemma schroeder_6_p:
"x * y ≤ -z ⟷ z⇧T * x ≤ -y⇧T"
using schroeder_3_p schroeder_4_p by auto
lemma vector_conv_compl:
"vector v ⟹ top * -v⇧T = -v⇧T"
by (simp add: covector_complement_closed vector_conv_covector)
text ‹
Composition commutes, relative to the diversity relation.
›
lemma comp_commute_below_diversity:
"x * y ≤ -1 ⟷ y * x ≤ -1"
by (metis comp_right_one conv_dist_comp conv_one schroeder_3_p schroeder_4_p)
lemma comp_injective_below_complement:
"injective y ⟹ -x * y ≤ -(x * y)"
by (metis p_antitone_iff comp_associative comp_right_isotone comp_right_one schroeder_4_p)
lemma comp_univalent_below_complement:
"univalent x ⟹ x * -y ≤ -(x * y)"
by (metis p_inf pseudo_complement semiring.mult_zero_right univalent_comp_left_dist_inf)
text ‹
Bijective relations and mappings can be exported from a pseudocomplement.
›
lemma comp_bijective_complement:
"bijective y ⟹ -x * y = -(x * y)"
using comp_injective_below_complement complement_conv_sub order.antisym shunt_bijective by blast
lemma comp_mapping_complement:
"mapping x ⟹ x * -y = -(x * y)"
by (metis (full_types) comp_bijective_complement conv_complement conv_dist_comp conv_involutive total_conv_surjective)
text ‹
The following facts are used in the correctness proof of Kruskal's minimum spanning tree algorithm.
›
lemma kruskal_injective_inv:
assumes "injective f"
and "covector q"
and "q * f⇧T ≤ q"
and "e ≤ q"
and "q * f⇧T ≤ -e"
and "injective e"
and "q⇧T * q ⊓ f⇧T * f ≤ 1"
shows "injective ((f ⊓ -q) ⊔ (f ⊓ q)⇧T ⊔ e)"
proof -
have 1: "(f ⊓ -q) * (f ⊓ -q)⇧T ≤ 1"
by (simp add: assms(1) injective_inf_closed)
have 2: "(f ⊓ -q) * (f ⊓ q) ≤ 1"
proof -
have 21: "bot = q * f⇧T ⊓ - q"
by (metis assms(3) inf.sup_monoid.add_assoc inf.sup_right_divisibility inf_import_p inf_p)
have "(f ⊓ -q) * (f ⊓ q) ≤ -q * f ⊓ q"
by (metis assms(2) comp_inf_covector comp_isotone inf.cobounded2 inf.left_idem)
also have "... = bot"
using 21 schroeder_2 by auto
finally show ?thesis
by (simp add: bot_unique)
qed
have 3: "(f ⊓ -q) * e⇧T ≤ 1"
proof -
have "(f ⊓ -q) * e⇧T ≤ -q * e⇧T"
by (simp add: mult_left_isotone)
also have "... = bot"
by (metis assms(2,4) bot_unique conv_bot conv_complement covector_complement_closed p_antitone p_bot regular_closed_bot schroeder_5_p)
finally show ?thesis
by (simp add: bot_unique)
qed
have 4: "(f ⊓ q)⇧T * (f ⊓ -q)⇧T ≤ 1"
using 2 conv_dist_comp conv_isotone by force
have 5: "(f ⊓ q)⇧T * (f ⊓ q) ≤ 1"
proof -
have "(f ⊓ q)⇧T * (f ⊓ q) ≤ q⇧T * q ⊓ f⇧T * f"
by (simp add: conv_isotone mult_isotone)
also have "... ≤ 1"
by (simp add: assms(7))
finally show ?thesis
by simp
qed
have 6: "(f ⊓ q)⇧T * e⇧T ≤ 1"
proof -
have "f⇧T * e⇧T ≤ -q⇧T"
using assms(5) schroeder_5_p by simp
hence "(f ⊓ q)⇧T * e⇧T = bot"
by (metis assms(2,5) conv_bot conv_dist_comp covector_comp_inf inf.absorb1 inf.cobounded2 inf.sup_monoid.add_commute inf_left_commute inf_p schroeder_4_p)
thus ?thesis
by (simp add: bot_unique)
qed
have 7: "e * (f ⊓ -q)⇧T ≤ 1"
using 3 conv_dist_comp coreflexive_symmetric by fastforce
have 8: "e * (f ⊓ q) ≤ 1"
using 6 conv_dist_comp coreflexive_symmetric by fastforce
have 9: "e * e⇧T ≤ 1"
by (simp add: assms(6))
have "((f ⊓ -q) ⊔ (f ⊓ q)⇧T ⊔ e) * ((f ⊓ -q) ⊔ (f ⊓ q)⇧T ⊔ e)⇧T = (f ⊓ -q) * (f ⊓ -q)⇧T ⊔ (f ⊓ -q) * (f ⊓ q) ⊔ (f ⊓ -q) * e⇧T ⊔ (f ⊓ q)⇧T * (f ⊓ -q)⇧T ⊔ (f ⊓ q)⇧T * (f ⊓ q) ⊔ (f ⊓ q)⇧T * e⇧T ⊔ e * (f ⊓ -q)⇧T ⊔ e * (f ⊓ q) ⊔ e * e⇧T"
using comp_left_dist_sup comp_right_dist_sup conv_dist_sup sup.assoc by simp
also have "... ≤ 1"
using 1 2 3 4 5 6 7 8 9 by simp
finally show ?thesis
by simp
qed
lemma kruskal_exchange_injective_inv_1:
assumes "injective f"
and "covector q"
and "q * f⇧T ≤ q"
and "q⇧T * q ⊓ f⇧T * f ≤ 1"
shows "injective ((f ⊓ -q) ⊔ (f ⊓ q)⇧T)"
using kruskal_injective_inv[where e=bot] by (simp add: assms)
lemma kruskal_exchange_acyclic_inv_3:
assumes "injective w"
and "d ≤ w"
shows "(w ⊓ -d) * d⇧T * top = bot"
proof -
have "(w ⊓ -d) * d⇧T * top = (w ⊓ -d ⊓ (d⇧T * top)⇧T) * top"
by (simp add: comp_associative comp_inf_vector_1 conv_dist_comp)
also have "... = (w ⊓ top * d ⊓ -d) * top"
by (simp add: conv_dist_comp inf_commute inf_left_commute)
finally show ?thesis
using assms epm_3 by simp
qed
lemma kruskal_subgraph_inv:
assumes "f ≤ --(-h ⊓ g)"
and "e ≤ --g"
and "symmetric h"
and "symmetric g"
shows "(f ⊓ -q) ⊔ (f ⊓ q)⇧T ⊔ e ≤ --(-(h ⊓ -e ⊓ -e⇧T) ⊓ g)"
proof -
let ?f = "(f ⊓ -q) ⊔ (f ⊓ q)⇧T ⊔ e"
let ?h = "h ⊓ -e ⊓ -e⇧T"
have 1: "f ⊓ -q ≤ -h ⊓ --g"
using assms(1) inf.coboundedI1 by simp
have "(f ⊓ q)⇧T ≤ (-h ⊓ --g)⇧T"
using assms(1) inf.coboundedI1 conv_isotone by simp
also have "... = -h ⊓ --g"
using assms(3,4) conv_complement conv_dist_inf by simp
finally have "?f ≤ (-h ⊓ --g) ⊔ (e ⊓ --g)"
using 1 assms(2) inf.absorb1 semiring.add_right_mono by simp
also have "... ≤ (-h ⊔ --e) ⊓ --g"
by (simp add: inf.coboundedI1 le_supI2 pp_increasing)
also have "... ≤ -?h ⊓ --g"
using inf.sup_left_isotone order_trans p_antitone_inf p_supdist_inf by blast
finally show "?f ≤ --(-?h ⊓ g)"
using inf_pp_semi_commute order_lesseq_imp by blast
qed
lemma antisymmetric_inf_diversity:
"antisymmetric x ⟹ x ⊓ -1 = x ⊓ -x⇧T"
by (smt (verit, del_insts) inf.orderE inf.sup_monoid.add_assoc inf.sup_monoid.add_commute inf_import_p one_inf_conv)
end
subsection ‹Stone Relation Algebras›
text ‹
We add ‹pp_dist_comp› and ‹pp_one›, which follow in relation algebras but not in the present setting.
The main change is that only a Stone algebra is required, not a Boolean algebra.
›
class stone_relation_algebra = pd_allegory + stone_algebra +
assumes pp_dist_comp : "--(x * y) = --x * --y"
assumes pp_one [simp]: "--1 = 1"
begin
text ‹
The following property is a simple consequence of the Stone axiom.
We cannot hope to remove the double complement in it.
›
lemma conv_complement_0_p [simp]:
"(-x)⇧T ⊔ (--x)⇧T = top"
by (metis conv_top conv_dist_sup stone)
lemma theorem24xxiv_pp:
"-(x * y) ⊔ --(x * z) = -(x * (y ⊓ -z)) ⊔ --(x * z)"
by (metis p_dist_inf theorem24xxiii)
lemma asymmetric_linear:
"asymmetric x ⟷ linear (-x)"
by (metis conv_complement inf.distrib_left inf_p maddux_3_11_pp p_bot p_dist_inf)
lemma strict_linear_asymmetric:
"strict_linear x ⟹ antisymmetric (-x)"
by (metis conv_complement eq_refl p_dist_sup pp_one)
lemma regular_complement_top:
"regular x ⟹ x ⊔ -x = top"
by (metis stone)
lemma regular_mult_closed:
"regular x ⟹ regular y ⟹ regular (x * y)"
by (simp add: pp_dist_comp)
lemma regular_one_closed:
"regular 1"
by simp
text ‹
The following variants of total and surjective are useful for graphs.
›
lemma pp_total:
"total (--x) ⟷ -(x*top) = bot"
by (simp add: dense_pp pp_dist_comp)
lemma pp_surjective:
"surjective (--x) ⟷ -(top*x) = bot"
by (metis p_bot p_comp_pp p_top pp_dist_comp)
text ‹
Bijective elements and mappings are necessarily regular, that is, invariant under double-complement.
This implies that points are regular.
Moreover, also arcs are regular.
›
lemma bijective_regular:
"bijective x ⟹ regular x"
by (metis comp_bijective_complement mult_left_one regular_one_closed)
lemma mapping_regular:
"mapping x ⟹ regular x"
by (metis bijective_regular conv_complement conv_involutive total_conv_surjective)
lemma arc_regular:
assumes "arc x"
shows "regular x"
proof -
have "--x ≤ --(x * top ⊓ top * x)"
by (simp add: pp_isotone top_left_mult_increasing top_right_mult_increasing)
also have "... = --(x * top) ⊓ --(top * x)"
by simp
also have "... = x * top ⊓ top * x"
by (metis assms bijective_regular conv_top conv_dist_comp conv_involutive mapping_regular)
also have "... ≤ x * x⇧T * top * x"
by (metis comp_associative dedekind_1 inf.commute inf_top.right_neutral)
also have "... ≤ x"
by (metis assms comp_right_one conv_top comp_associative conv_dist_comp conv_involutive mult_right_isotone vector_top_closed)
finally show ?thesis
by (simp add: order.antisym pp_increasing)
qed
lemma regular_power_closed:
"regular x ⟹ regular (x ^ n)"
apply (rule monoid_power_closed)
using regular_mult_closed by auto
end
text ‹
Every Stone algebra can be expanded to a Stone relation algebra by identifying the semiring and lattice structures and taking identity as converse.
›