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