Theory Residuated_Relation_Algebra

(* Title:      Residuated Relation Algebras
   Author:     Victor Gomes <vborgesferreiragomes1 at sheffield.ac.uk>
   Maintainer: Georg Struth <g.struth@sheffield.ac.uk> 
*)

section ‹Residuated Relation Algebras›

theory Residuated_Relation_Algebra
  imports Residuated_Boolean_Algebras Relation_Algebra.Relation_Algebra
begin

context boolean_algebra begin

text ‹
  The notation used in the relation algebra AFP entry differs a little from ours.
›

notation
  times (infixl "" 70)
  and plus (infixl "+" 65)
  and Groups.zero_class.zero ("0")
  and Groups.one_class.one ("1")

no_notation
  inf (infixl "" 70)
  and sup (infixl "+" 65)
  and bot ("0")
  and top ("1")

end

text ‹
  We prove that a unital residuated boolean algebra enriched with two simple
  equalities form a non-associative relation algebra, that is, a relation
  algebra where the associativity law does not hold.
›

class nra = unital_residuated_boolean +
  assumes conv1: "x  y = (x  1)y"
  and conv2: "x  y = x(1  y)"
begin

text ‹
  When the converse operation is set to be $\lambda x.\  x \rhd 1$,
  a unital residuated boolean algebra forms a non associative relation algebra.
›
  
lemma conv_invol: "x  1  1 = x"
  by (metis local.conv1 local.jonsson1b local.mult_onel)

lemma conv_add: "x  y  1 = (x  1)  (y  1)"
  by (metis local.conjr2_sup)

lemma conv_contrav: "xy  1 = (y  1)(x  1)"
  by (metis local.conv1 local.conv2 local.jonsson1b local.jonsson2c)

lemma conv_res: "(x  1)- (xy)  - y"
  by (metis local.comp_anti local.conjugate_r_def local.conv1 local.double_compl local.res_rc1)

text ‹
  Similarly, for $x^\smile = 1 \lhd x$, since $x \rhd 1 = 1 \lhd x$ when
  $x \rhd 1 \rhd 1 = x$ holds.
›

lemma conv_invol': "1  (1  x) = x"
  by (metis local.conv_invol local.jonsson3c)

lemma conv_add': "1  (x  y) = (1  x)  (1  y)"
  by (metis local.conjl1_sup)

lemma conv_contrav': "1  xy = (1  y)(1  x)"
  by (metis local.conv_contrav local.conv_invol local.jonsson3c)

lemma conv_res': "(1  x)- (xy)  - y"
  by (metis conv_res local.conv_invol local.jonsson3c)
  
end (* nra *)

text ‹
  Since the previous axioms are equivalent when multiplication is associative
  in a residuated boolean monoid, one of them are sufficient to
  derive a relation algebra.
›

class residuated_ra = residuated_boolean_monoid +
  assumes conv: "x  y = (x  1)y"
begin

subclass nra
proof (standard, fact conv)
  fix x y show "x  y = x(1  y)"
    by (metis conv jonsson4)
qed

sublocale relation_algebra where
  composition = "(⋅)" and unit = 1 and
  converse = "λx. x  1"
proof
  fix x y z
  show "xyz = x(yz)"
    by (metis local.mult_assoc)
  show "x1 = x"
    by (metis local.mult_onel)
  show "(x  y)z = xz  yz"
    by (metis local.distr)
  show "x  1  1 = x"
    by (metis local.conv_invol)
  show "x  y  1 = (x  1)  (y  1)"
    by (metis local.conv_add)
  show "xy  1 = (y  1)(x  1)"
    by (metis local.conv_contrav)
  show "(x  1)- (xy)  - y"
    by (metis local.conv_res)
qed

end (* residuated_ra *)

end