Theory Relation_Algebras

(* Title:      Relation Algebras
   Author:     Walter Guttmann
   Maintainer: Walter Guttmann <walter.guttmann at canterbury.ac.nz>
*)

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 * xT"
abbreviation surjective_var :: "'a ⇒ bool" where "surjective_var x ≡ 1 ≤ xT * x"
abbreviation univalent      :: "'a ⇒ bool" where "univalent x      ≡ xT * x ≤ 1"
abbreviation injective      :: "'a ⇒ bool" where "injective x      ≡ x * xT ≤ 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 (xT * top)" (* earlier name: atom *)

abbreviation symmetric      :: "'a ⇒ bool" where "symmetric x      ≡ xT = x"
abbreviation antisymmetric  :: "'a ⇒ bool" where "antisymmetric x  ≡ x ⊓ xT ≤ 1"
abbreviation asymmetric     :: "'a ⇒ bool" where "asymmetric x     ≡ x ⊓ xT = bot"
abbreviation linear         :: "'a ⇒ bool" where "linear x         ≡ x ⊔ xT = 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]: "xTT = x"
  assumes conv_dist_sup         : "(x ⊔ y)T = xT ⊔ yT"
  assumes conv_dist_comp        : "(x * y)T = yT * xT"
  assumes dedekind_1            : "x * y ⊓ z ≤ x * (y ⊓ (xT * z))"
begin

subclass bounded_distrib_allegory_signature .

text ‹
Many properties of relation algebras already follow in bounded distributive allegories.
›

lemma conv_isotone:
  "x ≤ y ⟹ xT ≤ yT"
  by (metis conv_dist_sup le_iff_sup)

lemma conv_order:
  "x ≤ y ⟷ xT ≤ yT"
  using conv_isotone by fastforce

lemma conv_bot [simp]:
  "botT = bot"
  using conv_order bot_unique by force

lemma conv_top [simp]:
  "topT = top"
  by (metis conv_involutive conv_order order.eq_iff top_greatest)

lemma conv_dist_inf:
  "(x ⊓ y)T = xT ⊓ yT"
  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 = xT ⊓ y ⟷ bot = x ⊓ yT"
  using conv_dist_inf conv_bot by fastforce

lemma conv_one [simp]:
  "1T = 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 . xT * 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 * xT)"
  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 ⟷ xT * 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 * yT ⊓ x = bot"
  by (metis comp_right_conjugate conjugate_def inf_commute)

lemma comp_additive:
  "additive (λy . x * y) ∧ additive (λy . xT * y) ∧ additive (λy . y * x) ∧ additive (λy . y * xT)"
  by (simp add: comp_left_dist_sup additive_def comp_right_dist_sup)

lemma dedekind_2:
  "y * x ⊓ z ≤ (y ⊓ (z * xT)) * 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 ⊓ xT) * z = (y ⊓ xT) * (x ⊓ z)"
proof -
  have "(y ⊓ xT) * z ≤ (y ⊓ xT) * (z ⊓ ((yT ⊓ x) * top))"
    by (metis inf_top_right dedekind_1 conv_dist_inf conv_involutive)
  also have "... ≤ (y ⊓ xT) * (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 ⊓ xT) * (x ⊓ z)"
proof -
  have "y * (x ⊓ z) ≤ (y ⊓ (top * (x ⊓ z)T)) * (x ⊓ z)"
    by (metis dedekind_2 inf_top_right)
  also have "... ≤ (y ⊓ xT) * (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 ⊓ xT) * 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 (vT)"
  by (metis conv_dist_comp conv_involutive conv_top)

lemma covector_conv_vector:
  "covector v ⟷ vector (vT)"
  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 ≤ xT * 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 * xT"
  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 * (xT ⊓ 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 "xT * (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 (xT)"
  by (metis conv_top conv_dist_comp conv_involutive)

lemma total_conv_surjective:
  "total x ⟷ surjective (xT)"
  by (simp add: surjective_conv_total)

lemma injective_conv_univalent:
  "injective x ⟷ univalent (xT)"
  by simp

lemma univalent_conv_injective:
  "univalent x ⟷ injective (xT)"
  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 ≤ yT"
    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 (xT)"
  by (simp add: surjective_conv_total)

lemma mapping_conv_bijective:
  "mapping x ⟷ bijective (xT)"
  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 (xT)"
  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 (xT)"
  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 (xT)"
  using conv_order conv_dist_comp by fastforce

lemma dense_conv_closed:
  "dense_rel x ⟹ dense_rel (xT)"
  using conv_order conv_dist_comp by fastforce

lemma idempotent_conv_closed:
  "idempotent x ⟹ idempotent (xT)"
  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 (xT)"
  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 (xT)"
  by simp

lemma one_inf_conv:
  "1 ⊓ x = 1 ⊓ xT"
  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 ⊓ xT"]) (simp_all add: conv_isotone inf.coboundedI2 inf.sup_assoc)

lemma antisymmetric_conv_closed:
  "antisymmetric x ⟹ antisymmetric (xT)"
  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 (xT)"
  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 (xT)"
  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 ⊔ xT ≤ x * y ⊔ yT * xT"
    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 (xT)"
  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 (xT)"
  by (simp add: inf_commute reflexive_conv_closed transitive_conv_closed)

lemma linear_order_conv_closed:
  "linear_order x ⟹ linear_order (xT)"
  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 ⊓ uT)T = vT ⊓ 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 * yT)) * (y ⊓ (xT * z)) ⊓ z"
proof (rule order.antisym)
  have "x * y ⊓ z ≤ x * (y ⊓ (xT * z)) ⊓ z"
    by (simp add: dedekind_1)
  also have "... ≤ (x ⊓ (z * (y ⊓ (xT * z))T)) * (y ⊓ (xT * z)) ⊓ z"
    by (simp add: dedekind_2)
  also have "... ≤ (x ⊓ (z * yT)) * (y ⊓ (xT * 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 * yT)) * (y ⊓ (xT * z)) ⊓ z"
    .
next
  show "(x ⊓ (z * yT)) * (y ⊓ (xT * z)) ⊓ z ≤ x * y ⊓ z"
    using comp_isotone inf.sup_left_isotone by auto
qed

lemma dedekind:
  "x * y ⊓ z ≤ (x ⊓ (z * yT)) * (y ⊓ (xT * 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 * xT) * 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 ⊓ xT * x) = x"
  by (metis conv_dist_comp conv_dist_inf conv_involutive conv_one ex231a)

lemma ex231c:
  "x ≤ x * xT * 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 (xT)"
  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 * tT ≤ 1"
      and "injective e"
    shows "injective (t ⊔ e)"
proof -
  have "(t ⊔ e) * (t ⊔ e)T = t * tT ⊔ t * eT ⊔ e * tT ⊔ e * eT"
    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 * tT = bot ⟹ arc e ⟹ injective (t ⊔ e)"
  using arc_injective injective_sup bot_least by blast

lemma univalent_sup:
  "univalent t ⟹ eT * t ≤ 1 ⟹ univalent e ⟹ univalent (t ⊔ e)"
  by (metis injective_sup conv_dist_sup conv_involutive)

lemma point_injective:
  "arc x ⟹ xT * top * x ≤ 1"
  by (metis conv_top comp_associative conv_dist_comp conv_involutive vector_top_closed)

lemma vv_transitive:
  "vector v ⟹ (v * vT) * (v * vT) ≤ v * vT"
  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 * eT * e"
    by (metis (no_types, lifting) inf.absorb2 top.extremum dedekind_2 inf.commute)
  also have "... ≤ w * wT * 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 * zT) * 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 * yT) * (y ⊓ xT * x * z)"
    by (metis comp_associative dedekind)
  also have "... ≤ x * (y ⊓ xT * 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 ⊓ wT = v * wT"
  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 * zT ≤ y"
proof
  assume "x ≤ y * z"
  hence "x * zT ≤ y * z * zT"
    by (simp add: mult_left_isotone)
  also have "... ≤ y"
    using assms comp_associative mult_right_isotone by fastforce
  finally show "x * zT ≤ y"
    .
next
  assume 1: "x * zT ≤ y"
  have "x = x ⊓ top * z"
    by (simp add: assms)
  also have "... ≤ x * zT * 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 ⟷ zT * 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 ≤ rT * p"
proof -
  have "p ≤ r * q ⟷ p * qT ≤ r"
    by (simp add: assms(2) shunt_bijective)
  also have "... ⟷ qT ≤ pT * r"
    by (metis assms(1) conv_dist_comp conv_involutive conv_order shunt_bijective)
  also have "... ⟷ q ≤ rT * p"
    using conv_dist_comp conv_isotone by fastforce
  finally show ?thesis
    by simp
qed

lemma arc_expanded:
  "arc x ⟷ x * top * xT ≤ 1 ∧ xT * 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 "xT * top * x = xT * x"
proof -
  have "xT = xT * top ⊓ top * xT"
    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 * xT * x"
proof -
  have "x * xT * 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 * xT * x ≤ x"
    by simp
  thus ?thesis
    by (simp add: order.antisym ex231c)
qed

lemma arc_eq_2:
  assumes "arc x"
    shows "xT = xT * x * xT"
  using arc_eq_1 assms conv_involutive by fastforce

lemma points_arc:
  "point x ⟹ point y ⟹ arc (x * yT)"
  by (metis comp_associative conv_dist_comp conv_involutive equivalence_top_closed)

lemma point_arc:
  "point x ⟹ arc (x * xT)"
  by (simp add: points_arc)

lemma arc_expanded_1:
  "arc e ⟹ e * x * eT ≤ 1"
  by (meson arc_expanded order_trans top_greatest mult_left_isotone mult_right_isotone)

lemma arc_expanded_2:
  "arc e ⟹ eT * x * e ≤ 1"
  by (meson arc_expanded order_trans top_greatest mult_left_isotone mult_right_isotone)

lemma point_conv_comp:
  "point x ⟹ xT * 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) = xT * y * (x ⊓ y)"
    by (simp add: assms(2) conv_dist_inf covector_inf_comp_3)
  also have "... = xT * (y ⊓ yT) * x"
    by (simp add: assms(2) comp_associative covector_inf_comp_3 inf.sup_monoid.add_commute)
  also have "... ≤ xT * 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:
  "xT ^ 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

text ‹
A relation is a permutation if and only if it has a left inverse and a right inverse.
›

lemma invertible_total:
  assumes "∃z . 1 ≤ x * z"
  shows "total x"
proof -
  from assms obtain z where "1 ≤ x * z"
    by auto
  hence "top ≤ x * z * top"
    using mult_isotone by fastforce
  also have "... ≤ x * top"
    by (simp add: mult_right_isotone mult_assoc)
  finally show ?thesis
    using top_le by auto
qed

lemma invertible_surjective:
  assumes "∃y . 1 ≤ y * x"
  shows "surjective x"
proof -
  from assms obtain y where "1 ≤ y * x"
    by auto
  hence "top ≤ top * y * x"
    using mult_right_isotone mult_assoc by fastforce
  also have "... ≤ top * x"
    by (simp add: mult_left_isotone)
  finally show ?thesis
    by (simp add: top_le)
qed

lemma invertible_univalent:
  assumes "∃y . y * x = 1"
      and "∃z . x * z = 1"
  shows "univalent x"
proof -
  from assms obtain y where 1: "y * x = 1"
    by auto
  from assms obtain z where 2: "x * z = 1"
    by auto
  have "y = y * x * z"
    using 2 comp_associative comp_right_one by force
  also have "... = z"
    using 1 by auto
  finally have 3: "y = z"
    .
  hence "total z"
    using 1 invertible_total by blast
  hence "x ≤ x * z * zT"
    using mult_right_isotone total_var mult_assoc by fastforce
  also have "... = zT"
    using 2 by auto
  finally have 4: "x ≤ zT"
    .
  have "total x"
    using 2 invertible_total by blast
  hence "z ≤ z * x * xT"
    using comp_associative mult_right_isotone total_var by fastforce
  also have "... = xT"
    using 1 3 by auto
  finally have "z ≤ xT"
    .
  hence "z = xT"
    using 4 conv_order by force
  thus ?thesis
    using 1 3 by blast
  (* this already shows permutation, but proving univalent seems to need all assumptions *)
qed

lemma invertible_injective:
  assumes "∃y . y * x = 1"
      and "∃z . x * z = 1"
    shows "injective x"
  by (metis assms invertible_univalent conv_dist_comp conv_involutive mult_left_one)

lemma invertible_mapping:
  assumes "∃y . y * x = 1"
      and "∃z . x * z = 1"
    shows "mapping x"
  using assms invertible_total invertible_univalent dual_order.eq_iff by auto

lemma invertible_bijective:
  assumes "∃y . y * x = 1"
      and "∃z . x * z = 1"
    shows "bijective x"
  using assms invertible_injective invertible_surjective by blast

text ‹
We define domain explicitly and show a few properties.
›

abbreviation domain :: "'a ⇒ 'a"
  where "domain x ≡ x * top ⊓ 1"

lemma domain_var:
  "domain x = x * xT ⊓ 1"
  by (smt (verit, del_insts) dedekind_eq inf.sup_monoid.add_commute inf_top_right mult.monoid_axioms symmetric_top_closed total_one_closed monoid.right_neutral)

lemma domain_comp:
  "domain x * x = x"
  using domain_var inf.sup_monoid.add_commute by auto

lemma domain_mult_inf:
  "domain x * domain y = domain x ⊓ domain y"
  using coreflexive_comp_inf by force

lemma domain_mult_commutative:
  "domain x * domain y = domain y * domain x"
  using coreflexive_commutative by force

lemma domain_mult_idempotent:
  "domain x * domain x = domain x"
  by (simp add: coreflexive_idempotent)

lemma domain_export:
  "domain (domain x * y) = domain x * domain y"
  by (simp add: inf_commute inf_left_commute inf_vector_comp)

lemma domain_local:
  "domain (x * domain y) = domain (x * y)"
  by (simp add: comp_associative vector_export_comp)

lemma domain_dist_sup:
  "domain (x ⊔ y) = domain x ⊔ domain y"
  by (simp add: inf_sup_distrib2 mult_right_dist_sup)

lemma domain_idempotent:
  "domain (domain x) = domain x"
  by (simp add: vector_export_comp)

lemma domain_bot:
  "domain bot = bot"
  by simp

lemma domain_one:
  "domain 1 = 1"
  by simp

lemma domain_top:
  "domain top = 1"
  by simp

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 ⊔ xT = -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 (xT * top)"

end

class pd_allegory = bounded_distrib_allegory + p_algebra
begin

subclass relation_algebra_signature .

subclass pd_algebra ..

lemma conv_complement_1:
  "-(xT) ⊔ (-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 = -(xT)"
  by (metis conv_complement_1 conv_dist_sup conv_involutive sup_commute)

lemma conv_complement_sub_inf [simp]:
  "xT * -(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:
  "xT * -(x * y) ≤ -y"
  using pseudo_complement conv_complement_sub_inf by blast

lemma conv_complement_sub [simp]:
  "xT * -(x * y) ⊔ -y = -y"
  by (simp add: conv_complement_sub_leq sup.absorb2)

lemma complement_conv_sub:
  "-(y * x) * xT ≤ -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 ⟷ xT * z ≤ -y"
  using pseudo_complement schroeder_1 by auto

lemma schroeder_4_p:
  "x * y ≤ -z ⟷ z * yT ≤ -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 ⊓ (xT * -(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 ⟹ -vT * 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 (xT)"
  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 (xT)"
  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 (xT)"
  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 ⊓ xT ⊓ -1) * (x ⊓ xT ⊓ -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 (xT)"
  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 (xT)"
  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 (xT)"
  by (simp add: conv_complement surjective_conv_total)

lemma pp_arc_expanded:
  "pp_arc x ⟷ x * top * xT ≤ 1 ∧ xT * top * x ≤ 1 ∧ top * --x * top = top"
proof
  assume 1: "pp_arc x"
  have 2: "x * top * xT ≤ 1"
    using 1 by (metis comp_associative conv_dist_comp equivalence_top_closed vector_top_closed)
  have 3: "xT * top * x ≤ 1"
    using 1 by (metis conv_dist_comp conv_involutive equivalence_top_closed vector_top_closed mult_assoc)
  have 4: "xT ≤ xT * x * xT"
    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 * xT * top * x) * top"
    using 1 by (metis eq_refl mult_assoc p_comp_pp p_pp_comp)
  also have "... = (top * --(x * top) ⊓ --(top * xT * top * x)) * top"
    using 1 by simp
  also have "... = top * (--(x * top) ⊓ --(top * xT * top * x)) * top"
    by (simp add: covector_complement_closed covector_comp_inf covector_mult_closed)
  also have "... = top * --(x * top ⊓ top * xT * top * x) * top"
    by simp
  also have "... = top * --(x * top * xT * top * x) * top"
    by (metis comp_associative comp_inf_covector inf_top.left_neutral)
  also have "... ≤ top * --(x * top * xT * x * xT * top * x) * top"
    using 4 by (metis comp_associative comp_left_isotone comp_right_isotone pp_isotone)
  also have "... ≤ top * --(x * xT * 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 * xT ≤ 1 ∧ xT * top * x ≤ 1 ∧ top * --x * top = top"
    using 2 3 top_le by blast
next
  assume "x * top * xT ≤ 1 ∧ xT * 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 * -vT"
    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 * -vT"
      and "t ≤ v * vT"
    shows "e * t = bot"
      and "e * tT = bot"
proof -
  have "e * t ≤ v * -vT * v * vT"
    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 "tT ≤ v * vT"
    using assms(3) conv_order conv_dist_comp by fastforce
  hence "e * tT ≤ v * -vT * v * vT"
    by (metis assms(2) comp_associative comp_isotone)
  thus "e * tT = bot"
    by (simp add: assms(1) covector_vector_comp le_bot mult_assoc)
qed

lemma ve_dist:
  assumes "e ≤ v * -vT"
      and "vector v"
      and "arc e"
    shows "(v ⊔ eT * top) * (v ⊔ eT * top)T = v * vT ⊔ v * vT * e ⊔ eT * v * vT ⊔ eT * 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 * vT) * e"
    using assms(2) covector_inf_comp_3 vector_conv_covector by force
  also have "... = v * top * vT * e"
    by (metis assms(2) inf_top_right vector_inf_comp)
  also have "... = v * vT * e"
    by (simp add: assms(2))
  finally have 1: "v * top * e = v * vT * e"
    .
  have "eT * top * e ≤ eT * top * e * eT * e"
    using ex231c comp_associative mult_right_isotone by auto
  also have "... ≤ eT * e"
    by (metis assms(3) coreflexive_comp_top_inf le_infE mult_semi_associative point_injective)
  finally have 2: "eT * top * e = eT * e"
    by (simp add: order.antisym mult_left_isotone top_right_mult_increasing)
  have "(v ⊔ eT * top) * (v ⊔ eT * top)T = (v ⊔ eT * top) * (vT ⊔ top * e)"
    by (simp add: conv_dist_comp conv_dist_sup)
  also have "... = v * vT ⊔ v * top * e ⊔ eT * top * vT ⊔ eT * top * top * e"
    by (metis semiring.distrib_left semiring.distrib_right sup_assoc mult_assoc)
  also have "... = v * vT ⊔ v * top * e ⊔ (v * top * e)T ⊔ eT * top * e"
    by (simp add: comp_associative conv_dist_comp)
  also have "... = v * vT ⊔ v * vT * e ⊔ (v * vT * e)T ⊔ eT * e"
    using 1 2 by simp
  finally show ?thesis
    by (simp add: comp_associative conv_dist_comp)
qed

lemma ev:
  "vector v ⟹ e ≤ v * -vT ⟹ 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 * -vT ⟹ vT * eT = 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 * -vT ⊓ g"
      and "t ≤ v * vT ⊓ g"
    shows "t ⊔ e ≤ ((v ⊔ eT * top) * (v ⊔ eT * top)T) ⊓ g"
proof (rule sup_least)
  have "t ≤ ((v ⊔ eT * top) * vT) ⊓ g"
    using assms(2) le_supI1 mult_right_dist_sup by auto
  also have "... ≤ ((v ⊔ eT * top) * (v ⊔ eT * top)T) ⊓ g"
    using comp_right_isotone conv_dist_sup inf.sup_left_isotone by auto
  finally show "t ≤ ((v ⊔ eT * top) * (v ⊔ eT * 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 * (eT * top)T ⊓ g"
    by (simp add: comp_associative conv_dist_comp)
  also have "... ≤ v * (v ⊔ eT * top)T ⊓ g"
    by (simp add: conv_dist_sup mult_left_dist_sup sup.assoc sup.orderI)
  also have "... ≤ (v ⊔ eT * top) * (v ⊔ eT * top)T ⊓ g"
    using inf.sup_left_isotone mult_right_sub_dist_sup_left by auto
  finally show "e ≤ ((v ⊔ eT * top) * (v ⊔ eT * 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 ⟷ xT * w * zT ≤ -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 * zT ≤ -xT"
  using schroeder_3_p schroeder_4_p by auto

lemma schroeder_6_p:
  "x * y ≤ -z ⟷ zT * x ≤ -yT"
  using schroeder_3_p schroeder_4_p by auto

lemma vector_conv_compl:
  "vector v ⟹ top * -vT = -vT"
  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 * fT ≤ q"
      and "e ≤ q"
      and "q * fT ≤ -e"
      and "injective e"
      and "qT * q ⊓ fT * 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 * fT ⊓ - 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) * eT ≤ 1"
  proof -
    have "(f ⊓ -q) * eT ≤ -q * eT"
      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) ≤ qT * q ⊓ fT * 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 * eT ≤ 1"
  proof -
    have "fT * eT ≤ -qT"
      using assms(5) schroeder_5_p by simp
    hence "(f ⊓ q)T * eT = 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 * eT ≤ 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) * eT ⊔ (f ⊓ q)T * (f ⊓ -q)T ⊔ (f ⊓ q)T * (f ⊓ q) ⊔ (f ⊓ q)T * eT ⊔ e * (f ⊓ -q)T ⊔ e * (f ⊓ q) ⊔ e * eT"
    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 * fT ≤ q"
      and "qT * q ⊓ fT * 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) * dT * top = bot"
proof -
  have "(w ⊓ -d) * dT * top = (w ⊓ -d ⊓ (dT * 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 ⊓ -eT) ⊓ g)"
proof -
  let ?f = "(f ⊓ -q) ⊔ (f ⊓ q)T ⊔ e"
  let ?h = "h ⊓ -e ⊓ -eT"
  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 ⊓ -xT"
  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 * xT * 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

(*
lemma conv_complement_0 [simp]: "xT ⊔ (-x)T = top" nitpick [expect=genuine] oops
lemma schroeder_3: "x * y ≤ z ⟷ xT * -z ≤ -y" nitpick [expect=genuine] oops
lemma schroeder_4: "x * y ≤ z ⟷ -z * yT ≤ -x" nitpick [expect=genuine] oops
lemma theorem24xxiv: "-(x * y) ⊔ (x * z) = -(x * (y ⊓ -z)) ⊔ (x * z)" nitpick [expect=genuine] oops
lemma vector_N: "x = x * top ⟶ N(x) = x ⊓ 1" nitpick [expect=genuine] oops
lemma N_vector [simp]: "N(x * top) = x * top ⊓ 1" nitpick [expect=genuine] oops
lemma N_vector_top [simp]: "N(x * top) * top = x * top" nitpick [expect=genuine] oops
lemma N_below_inf_one: "N(x) ≤ x ⊓ 1" nitpick [expect=genuine] oops
lemma N_below: "N(x) ≤ x" nitpick [expect=genuine] oops
lemma n_split_omega_mult: "xs * xo = xo ∧ xo * top = xo ⟶ N(top) * xo = xs * N(xo) * top" nitpick [expect=genuine] oops
lemma complement_vector: "vector v ⟷ vector (-v)" nitpick [expect=genuine] oops
lemma complement_covector: "covector v ⟷ covector (-v)" nitpick [expect=genuine] oops
lemma triple_schroeder: "x * y * z ≤ w ⟷ xT * -w * zT ≤ -y" nitpick [expect=genuine] oops
lemma schroeder_5: "x * y ≤ z ⟷ y * -zT ≤ -xT" nitpick [expect=genuine] oops
lemma schroeder_6: "x * y ≤ z ⟷ -zT * x ≤ -yT" nitpick [expect=genuine] oops
*)

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.
›

sublocale stone_algebra < comp_inf: stone_relation_algebra where one = top and times = inf and conv = id
proof (unfold_locales, goal_cases)
  case 7
  show ?case by (simp add: inf_commute)
qed (auto simp: inf.assoc inf_sup_distrib2 inf_left_commute)

text ‹
Every bounded linear order can be expanded to a Stone algebra, which can be expanded to a Stone relation algebra by reusing some of the operations.
In particular, composition is meet, its identity is ‹top› and converse is the identity function.
›

class linorder_stone_relation_algebra_expansion = linorder_stone_algebra_expansion + times + conv + one +
  assumes times_def [simp]: "x * y = min x y"
  assumes conv_def [simp]: "xT = x"
  assumes one_def [simp]: "1 = top"
begin

lemma times_inf [simp]:
  "x * y = x ⊓ y"
  by simp

subclass stone_relation_algebra
  apply unfold_locales
  using comp_inf.mult_right_dist_sup inf_commute inf_assoc inf_left_commute pp_dist_inf min_def by simp_all

lemma times_dense:
  "x ≠ bot ⟹ y ≠ bot ⟹ x * y ≠ bot"
  using inf_dense min_inf times_def by presburger

end

subsection ‹Relation Algebras›

text ‹
For a relation algebra, we only require that the underlying lattice is a Boolean algebra.
In fact, the only missing axiom is that double-complement is the identity.
›

class relation_algebra = boolean_algebra + stone_relation_algebra
begin

lemma conv_complement_0 [simp]:
  "xT ⊔ (-x)T = top"
  by (simp add: conv_complement)

text ‹
We now obtain the original formulations of the Schr\"oder equivalences.
›

lemma schroeder_3:
  "x * y ≤ z ⟷ xT * -z ≤ -y"
  by (simp add: schroeder_3_p)

lemma schroeder_4:
  "x * y ≤ z ⟷ -z * yT ≤ -x"
  by (simp add: schroeder_4_p)

lemma theorem24xxiv:
  "-(x * y) ⊔ (x * z) = -(x * (y ⊓ -z)) ⊔ (x * z)"
  using theorem24xxiv_pp by auto

lemma vector_N:
  "vector x ⟹ N(x) = x ⊓ 1"
  by (simp add: vector_N_pp)

lemma N_vector [simp]:
  "N(x * top) = x * top ⊓ 1"
  by simp

lemma N_vector_top [simp]:
  "N(x * top) * top = x * top"
  using N_vector_top_pp by simp

lemma N_below_inf_one:
  "N(x) ≤ x ⊓ 1"
  using N_below_inf_one_pp by simp

lemma N_below:
  "N(x) ≤ x"
  using N_below_pp by simp

lemma n_split_omega_mult:
  "xs * xo = xo ⟹ xo * top = xo ⟹ N(top) * xo = xs * N(xo) * top"
  using n_split_omega_mult_pp by simp

lemma complement_vector:
  "vector v ⟷ vector (-v)"
  using vector_complement_closed by fastforce

lemma complement_covector:
  "covector v ⟷ covector (-v)"
  using covector_complement_closed by force

lemma triple_schroeder:
  "x * y * z ≤ w ⟷ xT * -w * zT ≤ -y"
  by (simp add: triple_schroeder_p)

lemma schroeder_5:
  "x * y ≤ z ⟷ y * -zT ≤ -xT"
  by (simp add: conv_complement schroeder_5_p)

lemma schroeder_6:
  "x * y ≤ z ⟷ -zT * x ≤ -yT"
  by (simp add: conv_complement schroeder_5_p)

text ‹
We define and study the univalent part and the multivalent part of a relation.
›

abbreviation univalent_part :: "'a ⇒ 'a" (‹up›)
  where "up x ≡ x ⊓ -(x * -1)"

abbreviation multivalent_part :: "'a ⇒ 'a" (‹mp›)
  where "mp x ≡ x ⊓ x * -1"

lemma up_mp_disjoint:
 "up x ⊓ mp x = bot"
  using comp_inf.univalent_comp_left_dist_inf by auto

lemma up_mp_partition:
  "up x ⊔ mp x = x"
  by simp

lemma mp_conv_up_bot:
  "(mp x)T * up x = bot"
proof -
  have "(mp x)T * up x ≤ xT * -(x * -1)"
    by (simp add: conv_dist_inf mult_isotone)
  also have "... ≤ 1"
    by (metis conv_complement_sub_leq pp_one)
  finally have 1: "(mp x)T * up x ≤ 1"
    .
  have "(mp x)T * up x ≤ (x * -1)T * -(x * -1)"
    by (simp add: conv_isotone mult_isotone)
  also have "... ≤ -1"
    by (simp add: schroeder_3)
  finally have "(mp x)T * up x ≤ -1"
    .
  thus ?thesis
    using 1 by (metis le_iff_inf pseudo_complement)
qed

lemma up_conv_up:
  "xT * up x = (up x)T * up x"
proof -
  have "xT * up x = (up x)T * up x ⊔ (mp x)T * up x"
    by (metis conv_dist_sup mult_right_dist_sup up_mp_partition)
  thus ?thesis
    by (simp add: mp_conv_up_bot)
qed

lemma up_univalent:
  "univalent (up x)"
  by (metis inf_compl_bot_right schroeder_1 shunting_1 up_conv_up)

lemma up_mp_bot:
  "up (mp x) = bot"
  by (metis dedekind_2 equivalence_one_closed inf.sup_monoid.add_commute shunting_1 symmetric_complement_closed)

lemma mp_up_bot:
  "mp (up x) = bot"
  by (metis comp_right_one comp_univalent_below_complement double_compl shunting_1 up_univalent)

lemma up_idempotent:
  "up (up x) = up x"
  by (metis comp_right_one comp_univalent_below_complement inf.absorb1 regular_one_closed up_univalent)

lemma mp_idempotent:
  "mp (mp x) = mp x"
  using inf.absorb1 shunting_1 up_mp_bot by blast

lemma mp_conv_mp:
  "xT * mp x = (mp x)T * mp x"
  by (smt (verit, ccfv_threshold) conv_dist_comp conv_dist_sup conv_involutive inf.absorb1 mult_right_dist_sup shunting_1 mp_conv_up_bot up_mp_bot up_mp_partition)

lemma up_mp_top:
  "-(x * top) ⊔ up x * top ⊔ mp x * top = top"
  using semiring.combine_common_factor sup_monoid.add_commute by auto

lemma domain_mp:
  "domain (mp x) = x * -1 * xT ⊓ 1"
  by (smt (verit, del_insts) comp_right_one conv_dist_comp conv_dist_inf conv_involutive dedekind_eq equivalence_one_closed inf.sup_monoid.add_commute inf_top.left_neutral)

lemma domain_mp_bot:
  "domain (mp x) * x ⊓ -(x * -1) = bot"
  by (metis conv_complement_sub_inf conv_involutive inf.sup_monoid.add_assoc p_bot vector_export_comp_unit mp_conv_up_bot)

lemma domain_mp_mp:
  "domain (mp x) * x = mp x"
  by (smt (verit, ccfv_threshold) conv_complement_sub_inf conv_involutive inf.absorb1 inf.absorb_iff2 inf_sup_distrib1 p_bot shunting_1 top_right_mult_increasing vector_export_comp_unit mp_conv_up_bot up_mp_bot up_mp_partition)

lemma mp_var:
  "mp x = x ⊓ (x * -1 * xT ⊓ 1) * top"
  by (metis domain_mp domain_mp_mp inf.sup_monoid.add_commute inf_top_right vector_export_comp_unit)

end

text ‹
We briefly look at the so-called Tarski rule.
In some models of Stone relation algebras it only holds for regular elements, so we add this as an assumption.
›

class stone_relation_algebra_tarski = stone_relation_algebra +
  assumes tarski: "regular x ⟹ x ≠ bot ⟹ top * x * top = top"
begin

text ‹
We can then show, for example, that every arc is contained in a pseudocomplemented relation or its pseudocomplement.
›

lemma arc_in_partition:
  assumes "arc x"
    shows "x ≤ -y ∨ x ≤ --y"
proof -
  have 1: "x * top * xT ≤ 1 ∧ xT * top * x ≤ 1"
    using assms arc_expanded by auto
  have "¬ x ≤ --y ⟶ x ≤ -y"
  proof
    assume "¬ x ≤ --y"
    hence "x ⊓ -y ≠ bot"
      using pseudo_complement by simp
    hence "top * (x ⊓ -y) * top = top"
      using assms arc_regular tarski by auto
    hence "x = x ⊓ top * (x ⊓ -y) * top"
      by simp
    also have "... ≤ x ⊓ x * ((x ⊓ -y) * top)T * (x ⊓ -y) * top"
      by (metis dedekind_2 inf.cobounded1 inf.boundedI inf_commute mult_assoc inf.absorb2 top.extremum)
    also have "... = x ⊓ x * top * (xT ⊓ -yT) * (x ⊓ -y) * top"
      by (simp add: comp_associative conv_complement conv_dist_comp conv_dist_inf)
    also have "... ≤ x ⊓ x * top * xT * (x ⊓ -y) * top"
      using inf.sup_right_isotone mult_left_isotone mult_right_isotone by auto
    also have "... ≤ x ⊓ 1 * (x ⊓ -y) * top"
      using 1 by (metis comp_associative comp_isotone inf.sup_right_isotone mult_1_left mult_semi_associative)
    also have "... = x ⊓ (x ⊓ -y) * top"
      by simp
    also have "... ≤ (x ⊓ -y) * ((x ⊓ -y)T * x)"
      by (metis dedekind_1 inf_commute inf_top_right)
    also have "... ≤ (x ⊓ -y) * (xT * x)"
      by (simp add: conv_dist_inf mult_left_isotone mult_right_isotone)
    also have "... ≤ (x ⊓ -y) * (xT * top * x)"
      by (simp add: mult_assoc mult_right_isotone top_left_mult_increasing)
    also have "... ≤ x ⊓ -y"
      using 1 by (metis mult_right_isotone mult_1_right)
    finally show "x ≤ -y"
      by simp
  qed
  thus ?thesis
    by auto
qed

lemma non_bot_arc_in_partition_xor:
  assumes "arc x"
      and "x ≠ bot"
    shows "(x ≤ -y ∧ ¬ x ≤ --y) ∨ (¬ x ≤ -y ∧ x ≤ --y)"
proof -
  have "x ≤ -y ∧ x ≤ --y ⟶ False"
    by (simp add: assms(2) inf_absorb1 shunting_1_pp)
  thus ?thesis
    using assms(1) arc_in_partition by auto
qed

lemma point_in_vector_or_pseudo_complement:
  assumes "point p"
      and "vector v"
    shows "p ≤ --v ∨ p ≤ -v"
proof (rule disjCI)
  assume "¬(p ≤ -v)"
  hence "top * (p ⊓ --v) = top"
    by (smt assms bijective_regular regular_closed_inf regular_closed_p shunting_1_pp tarski vector_complement_closed vector_inf_closed vector_mult_closed)
  thus "p ≤ --v"
    by (metis assms(1) epm_3 inf.absorb_iff1 inf.cobounded1 inf_top.right_neutral)
qed

lemma distinct_points:
  assumes "point x"
    and "point y"
    and "x ≠ y"
  shows "x ⊓ y = bot"
  by (metis assms order.antisym comp_bijective_complement inf.sup_monoid.add_commute mult_left_one pseudo_complement regular_one_closed point_in_vector_or_pseudo_complement)

lemma point_in_vector_or_complement:
  assumes "point p"
      and "vector v"
      and "regular v"
    shows "p ≤ v ∨ p ≤ -v"
  using assms point_in_vector_or_pseudo_complement by fastforce

lemma point_in_vector_sup:
  assumes "point p"
      and "vector v"
      and "regular v"
      and "p ≤ v ⊔ w"
    shows "p ≤ v ∨ p ≤ w"
  by (metis assms inf.absorb1 shunting_var_p sup_commute point_in_vector_or_complement)

lemma point_atomic_vector:
  assumes "point x"
    and "vector y"
    and "regular y"
    and "y ≤ x"
  shows "y = x ∨ y = bot"
proof (cases "x ≤ -y")
  case True
  thus ?thesis
    using assms(4) inf.absorb2 pseudo_complement by force
next
  case False
  thus ?thesis
    using assms point_in_vector_or_pseudo_complement by fastforce
qed

lemma point_in_vector_or_complement_2:
  assumes "point x"
    and "vector y"
    and "regular y"
    and "¬ y ≤ -x"
  shows "x ≤ y"
  using assms point_in_vector_or_pseudo_complement p_antitone_iff by fastforce

text ‹
The next three lemmas ‹arc_in_arc_or_complement›, ‹arc_in_sup_arc› and ‹different_arc_in_sup_arc› were contributed by Nicolas Robinson-O'Brien.
›

lemma arc_in_arc_or_complement:
  assumes "arc x"
      and "arc y"
      and "¬ x ≤ y"
    shows "x ≤ -y"
  using assms arc_in_partition arc_regular by force

lemma arc_in_sup_arc:
  assumes "arc x"
      and "arc y"
      and "x ≤ z ⊔ y"
    shows "x ≤ z ∨ x ≤ y"
proof (cases "x ≤ y")
  case True
  thus ?thesis
    by simp
next
  case False
  hence "x ≤ -y"
    using assms(1,2) arc_in_arc_or_complement by blast
  hence "x ≤ -y ⊓ (z ⊔ y)"
    using assms(3) by simp
  hence "x ≤ z"
    by (metis inf.boundedE inf.sup_monoid.add_commute maddux_3_13 sup_commute)
  thus ?thesis
    by simp
qed

lemma different_arc_in_sup_arc:
  assumes "arc x"
      and "arc y"
      and "x ≤ z ⊔ y"
      and "x ≠ y"
    shows "x ≤ z"
proof -
  have "x ≤ -y"
    using arc_in_arc_or_complement assms(1,2,4) order.eq_iff p_antitone_iff by blast
  hence "x ≤ -y ⊓ (z ⊔ y)"
    using assms arc_in_sup_arc by simp
  thus ?thesis
    by (metis order_lesseq_imp p_inf_sup_below sup_commute)
qed

end

class relation_algebra_tarski = relation_algebra + stone_relation_algebra_tarski

text ‹
Finally, the above axioms of relation algebras do not imply that they contain at least two elements.
This is necessary, for example, to show that arcs are not empty.
›

class stone_relation_algebra_consistent = stone_relation_algebra +
  assumes consistent: "bot ≠ top"
begin

lemma arc_not_bot:
  "arc x ⟹ x ≠ bot"
  using consistent mult_right_zero by auto

lemma point_not_bot:
  "point p ⟹ p ≠ bot"
  using consistent by force

end

class relation_algebra_consistent = relation_algebra + stone_relation_algebra_consistent

class stone_relation_algebra_tarski_consistent = stone_relation_algebra_tarski + stone_relation_algebra_consistent
begin

lemma arc_in_partition_xor:
  "arc x ⟹ (x ≤ -y ∧ ¬ x ≤ --y) ∨ (¬ x ≤ -y ∧ x ≤ --y)"
  by (simp add: non_bot_arc_in_partition_xor arc_not_bot)

lemma regular_injective_vector_point_xor_bot:
  assumes "regular x"
      and "vector x"
      and "injective x"
    shows "point x ⟷ x ≠ bot"
  using assms comp_associative consistent tarski by fastforce

end

class relation_algebra_tarski_consistent = relation_algebra + stone_relation_algebra_tarski_consistent

end