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: "x⋅y ⊳ 1 = (y ⊳ 1)⋅(x ⊳ 1)"
  by (metis local.conv1 local.conv2 local.jonsson1b local.jonsson2c)

lemma conv_res: "(x ⊳ 1)⋅- (x⋅y) ≤ - 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 ⊲ x⋅y = (1 ⊲ y)⋅(1 ⊲ x)"
  by (metis local.conv_contrav local.conv_invol local.jonsson3c)

lemma conv_res': "(1 ⊲ x)⋅- (x⋅y) ≤ - 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 "x⋅y⋅z = x⋅(y⋅z)"
    by (metis local.mult_assoc)
  show "x⋅1 = x"
    by (metis local.mult_onel)
  show "(x ⊔ y)⋅z = x⋅z ⊔ y⋅z"
    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 "x⋅y ⊳ 1 = (y ⊳ 1)⋅(x ⊳ 1)"
    by (metis local.conv_contrav)
  show "(x ⊳ 1)⋅- (x⋅y) ≤ - y"
    by (metis local.conv_res)
qed

end (* residuated_ra *)

end