# Theory Residuated_Relation_Algebra

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