Theory Relation_Algebra.Relation_Algebra
section ‹Relation Algebra›
theory Relation_Algebra
imports More_Boolean_Algebra Kleene_Algebra.Kleene_Algebra
begin
text ‹We follow Tarski's original article and Maddux's book, in particular we
use their notation. In contrast to Schmidt and Str\"ohlein we do not assume
that the Boolean algebra is complete and we do not consider the Tarski rule in
this development.
A main reason for using complete Boolean algebras seems to be that the
Knaster-Tarski fixpoint theorem becomes available for defining notions of
iteration. In fact, several chapters of Schmidt and Str\"ohlein's book deal
with iteration.
We capture iteration in an alternative way by linking relation algebras with
Kleene algebras (cf.~\emph{relation-algebra-rtc}).›
class relation_algebra = boolean_algebra +
fixes composition :: "'a ⇒ 'a ⇒ 'a" (infixl ‹;› 75)
and converse :: "'a ⇒ 'a" (‹(_⇧⌣)› [1000] 999)
and unit :: "'a" (‹1''›)
assumes comp_assoc: "(x ; y) ; z = x ; (y ; z)"
and comp_unitr [simp]: "x ; 1' = x"
and comp_distr: "(x + y) ; z = x ; z + y ; z"
and conv_invol [simp]: "(x⇧⌣)⇧⌣ = x"
and conv_add [simp]: "(x + y)⇧⌣ = x⇧⌣ + y⇧⌣"
and conv_contrav [simp]: "(x ; y)⇧⌣ = y⇧⌣ ; x⇧⌣"
and comp_res: "x⇧⌣ ; -(x ; y) ≤ -y"
text ‹We first show that every relation algebra is a dioid. We do not yet
treat the zero (the minimal element of the boolean reduct) since the proof of
the annihilation laws is rather tricky to automate. Following Maddux we derive
them from properties of Boolean algebras with operators.›
sublocale relation_algebra ⊆ dioid_one "(+)" "(;)" "(≤) " "(<)" "1'"
proof
fix x y z :: 'a
show "x ; y ; z = x ; (y ; z)"
by (fact comp_assoc)
show "x + y + z = x + (y + z)"
by (metis sup.commute sup.left_commute)
show "x + y = y + x"
by (fact sup.commute)
show "(x + y) ; z = x ; z + y ; z"
by (fact comp_distr)
show "x + x = x"
by (fact sup.idem)
show "x ; (y + z) = x ; y + x ; z"
by (metis conv_invol conv_add conv_contrav comp_distr)
show "x ; 1' = x"
by (fact comp_unitr)
show "1' ; x = x"
by (metis comp_unitr conv_contrav conv_invol)
show "x ≤ y ⟷ x + y = y"
by (metis sup.commute sup_absorb1 sup_ge1)
show "x < y ⟷ x ≤ y ∧ x ≠ y"
by (fact less_le)
qed
context relation_algebra
begin
text ‹First we prove some basic facts about joins and meets.›
lemma meet_interchange: "(w ⋅ x) ; (y ⋅ z) ≤ w ; y ⋅ x ; z"
by (metis inf_le1 inf_le2 le_infI mult_isol_var)
lemma join_interchange: "w ; x + y ; z ≤ (w + y) ; (x + z)"
using local.mult_isol_var local.sup.bounded_iff local.sup.cobounded2 local.sup_ge1 by presburger
text ‹We now prove some simple facts about conversion.›
lemma conv_iso: "x ≤ y ⟷ x⇧⌣ ≤ y⇧⌣"
by (metis conv_add conv_invol le_iff_sup)
lemma conv_zero [simp]: "0⇧⌣ = 0"
by (metis conv_add conv_invol sup_bot_right sup_eq_bot_iff)
lemma conv_one [simp]: "1⇧⌣ = 1"
by (metis conv_add conv_invol sup_top_left sup_top_right)
lemma conv_compl_aux: "(-x)⇧⌣ = (-x)⇧⌣ + (-x⇧⌣)"
by (metis aux9 conv_add conv_one double_compl galois_aux4 inf.commute less_eq_def sup.commute sup_top_left)
lemma conv_compl: "(-x)⇧⌣ = -(x⇧⌣)"
by (metis add_commute conv_add conv_compl_aux conv_invol)
lemma comp_res_aux [simp]: "x⇧⌣ ; -(x ; y) ⋅ y = 0"
by (metis comp_res galois_aux)
lemma conv_e [simp]: "1'⇧⌣ = 1'"
by (metis comp_unitr conv_contrav conv_invol)
lemma conv_times [simp]: "(x ⋅ y)⇧⌣ = x⇧⌣ ⋅ y⇧⌣"
by (metis compl_inf double_compl conv_add conv_compl)
text ‹The next lemmas show that conversion is self-conjugate in the sense of
Boolean algebra with operators.›
lemma conv_self_conjugate: "x⇧⌣ ⋅ y = 0 ⟷ x ⋅ y⇧⌣ = 0"
by (metis conv_invol conv_times conv_zero)
lemma conv_self_conjugate_var: "is_conjugation converse converse"
by (metis conv_self_conjugate is_conjugation_def)
text ‹The following lemmas link the relative product and meet.›
lemma one_idem_mult [simp]: "1 ; 1 = 1"
by (metis compl_eq_compl_iff galois_aux2 inf.commute inf_top_right mult_1_left mult_isor top_greatest)
lemma mult_subdistl: "x ; (y ⋅ z) ≤ x ; y"
by (metis inf_le1 mult_isol)
lemma mult_subdistr: "(x ⋅ y) ; z ≤ x ; z"
by (metis inf_le1 mult_isor)
lemma mult_subdistr_var: "(x ⋅ y) ; z ≤ x ; z ⋅ y ; z"
by (metis inf.commute le_inf_iff mult_subdistr)
text ‹The following lemmas deal with variants of the Peirce law, the
Schr\"oder laws and the Dedekind law. Some of them are obtained from Boolean
algebras with operators by instantiation, using conjugation properties.
However, Isabelle does not always pick up this relationship.›
lemma peirce_1: "x ; y ⋅ z⇧⌣ = 0 ⟹ y ; z ⋅ x⇧⌣ = 0"
by (metis compl_le_swap1 conv_contrav conv_self_conjugate galois_aux comp_res conv_invol galois_aux mult_isol order_trans)
lemma peirce: "x ; y ⋅ z⇧⌣ = 0 ⟷ y ; z ⋅ x⇧⌣ = 0"
by (metis peirce_1)
lemma schroeder_1: "x ; y ⋅ z = 0 ⟷ y ⋅ x⇧⌣ ; z = 0"
by (metis conv_invol peirce conv_contrav conv_invol conv_self_conjugate inf.commute)
lemma schroeder_2: "y ; x ⋅ z = 0 ⟷ y ⋅ z ; x⇧⌣ = 0"
by (metis conv_invol peirce schroeder_1)
text ‹The following two conjugation properties between multiplication with
elements and their converses are used for deriving modular laws of relation
algebra from those of Boolean algebras with operators.›
lemma schroeder_1_var: "is_conjugation (composition x) (composition (x⇧⌣))"
by (metis schroeder_1 is_conjugation_def)
lemma schroeder_2_var: "is_conjugation (λx. x ; y) (λx. x ; y⇧⌣)"
by (unfold is_conjugation_def, metis schroeder_2)
text ‹The following Galois connections define residuals. They link relation
algebras with action algebras. This could be further explored and formalised.
›
lemma conv_galois_1: "x ; y ≤ z ⟷ y ≤ -(x⇧⌣ ; -z)"
by (metis galois_aux galois_aux2 schroeder_1)
lemma conv_galois_2: "y ; x ≤ z ⟷ y ≤ -(-z ; x⇧⌣)"
by (metis galois_aux galois_aux2 schroeder_2)
text ‹Variants of the modular law for relation algebras can now be
instantiated from Boolean algebras with operators.›
lemma modular_1_aux': "x ; (y ⋅ -(x⇧⌣ ; z)) ⋅ z = 0"
by (metis schroeder_1_var modular_1_aux)
lemma modular_2_aux': "(y ⋅ -(z ; x⇧⌣)) ; x ⋅ z = 0"
by (metis modular_1_aux schroeder_2_var)
lemma modular_1': "x ; y ⋅ z = x ; (y ⋅ x⇧⌣ ; z) ⋅ z"
by (metis schroeder_1_var modular_1)
lemma modular_2': "y ; x ⋅ z = (y ⋅ z ; x⇧⌣) ; x ⋅ z"
proof -
have "y ; x ⋅ z = (y ⋅ z ; x⇧⌣) ; x ⋅ z + (y ⋅ -(z ; x⇧⌣)) ; x ⋅ z"
by (metis aux4 distrib_right inf.commute inf_sup_distrib1)
thus ?thesis
by (metis sup_bot_right modular_2_aux')
qed
lemma modular_1_var: "x ; y ⋅ z ≤ x ; (y ⋅ x⇧⌣ ; z)"
by (metis inf.commute inf_le2 modular_1')
lemma modular_2_var: "x ; y ⋅ z ≤ (x ⋅ z ; y⇧⌣) ; y"
by (metis inf.commute inf_le2 modular_2')
lemma modular_var_2: "x ; y ≤ x ; (y ⋅ x⇧⌣ ; 1)"
by (metis inf_top_right modular_1_var)
lemma modular_var_3: "x ; y ≤ (x ⋅ 1 ; y⇧⌣) ; y"
by (metis inf_top_right modular_2_var)
text ‹The modular laws are used to prove the Dedekind rule.›
lemma dedekind: "x ; y ⋅ z ≤ (x ⋅ z ; y⇧⌣) ; (y ⋅ x⇧⌣ ; z)"
proof -
have "x ; y ⋅ z ≤ (x ⋅ z ; y⇧⌣) ; (y ⋅ ((x ⋅ z ; y⇧⌣)⇧⌣ ; z))"
by (metis modular_2' modular_1_var)
also have "… ≤ (x ⋅ z ; y⇧⌣) ; (y ⋅ x⇧⌣ ; z)"
by (metis conv_iso inf_le1 inf_mono mult_isol mult_isor order_refl)
thus ?thesis
by (metis calculation order_trans)
qed
lemma dedekind_var_1: "x ; y ≤ (x ⋅ 1 ; y⇧⌣) ; (y ⋅ x⇧⌣ ; 1)"
by (metis dedekind inf.commute inf_top_left)
end
text ‹The Schr\"oder laws allow us, finally, to prove the annihilation laws
for zero. We formalise this by proving that relation algebras form dioids with
zero.›