Theory Relation_Algebras

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

section Relation Algebras

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,Guttmann2017b}.
Our main application there is the verification of Prim's minimum spanning tree algorithm.
Related work about fuzzy relations \cite{Goguen1967,Winter2001b}, Dedekind categories \cite{KawaharaFurusawa2001} and rough relations \cite{Comer1993,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,HirschHodkinson2002,Maddux1996,Maddux2006,Schmidt2011,SchmidtStroehlein1993} for further details about relations and relation algebras, and \cite{AndrekaMikulas2011,BredihinSchein1978} for algebras of relations with a smaller signature.

theory Relation_Algebras

imports Stone_Algebras.P_Algebras Semirings


subsection Single-Object Bounded Distributive Allegories

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

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"


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,FreydScedrov1990,KawaharaFurusawaMori1999,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))"

subclass bounded_distrib_allegory_signature .

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)

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)

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)

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

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

We still have two ways to represent surjectivity and totality.

lemma surjective_var:
  "surjective x  surjective_var x"
  assume "surjective x"
  thus "surjective_var x"
    by (metis dedekind_2 comp_left_one inf_absorb2 top_greatest)
  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)

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

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)

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)

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

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)

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

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)

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)

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"
  show "(x  (z * yT)) * (y  (xT * z))  z  x * y  z"
    using comp_isotone inf.sup_left_isotone by auto

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)

lemma vector_export_comp_unit:
  "(x * top  1) * y = x * top  y"
  by (simp add: vector_export_comp)

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)
  show "x  1  x * (x  1)"
    by (metis coreflexive_idempotent inf.cobounded1 inf.cobounded2 mult_left_isotone)

The following result generalises \cite[Exercise 2]{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

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)

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)

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

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)

The shunting properties for bijective relations and mappings continue to hold.

lemma shunt_bijective:
  assumes "bijective z"
    shows "x  y * z  x * zT  y"
  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"
  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"

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

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)

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)

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)


subsection Single-Object Pseudocomplemented Distributive Allegories

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

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"

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


class pd_allegory = bounded_distrib_allegory + p_algebra

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)

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

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

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)

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)

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)

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

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

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)

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)

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

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)

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

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

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

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)

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)

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)

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

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

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

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)


subsection Stone Relation Algebras

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]: