# Theory N_Relation_Algebras

(* Title:      N-Relation-Algebras
Author:     Walter Guttmann
Maintainer: Walter Guttmann <walter.guttmann at canterbury.ac.nz>
*)

section ‹N-Relation-Algebras›

theory N_Relation_Algebras

imports Stone_Relation_Algebras.Relation_Algebras N_Omega_Algebras

begin

context bounded_distrib_allegory
begin

subclass lattice_ordered_pre_left_semiring ..

end

text ‹Theorem 37›

sublocale relation_algebra < n_algebra where sup = sup and bot = bot and top = top and inf = inf and n = N and L = top
apply unfold_locales
using N_comp_top comp_inf.semiring.distrib_left inf.sup_monoid.add_commute inf_vector_comp apply simp
apply (metis N_comp compl_sup double_compl mult_assoc mult_right_dist_sup top_mult_top N_comp_N)
apply (metis brouwer.p_antitone inf.sup_monoid.add_commute inf.sup_right_isotone mult_left_isotone p_antitone_sup)
apply simp
using N_vector_top apply force
apply simp
apply (simp add: brouwer.p_antitone_iff top_right_mult_increasing)
apply simp
apply (metis N_comp_top conv_complement_sub double_compl le_supI2 le_iff_sup mult_assoc mult_left_isotone schroeder_3)
by simp

sublocale relation_algebra < n_algebra_apx where sup = sup and bot = bot and top = top and inf = inf and n = N and L = top and apx = greater_eq
apply unfold_locales
using n_less_eq_char by force

no_notation
inverse_divide (infixl "'/" 70)

notation
divide (infixl "'/" 70)

class left_residuated_relation_algebra = relation_algebra + inverse +
assumes lres_def: "x / y = -(-x * yT)"
begin

text ‹Theorem 32.1›

subclass residuated_pre_left_semiring
apply unfold_locales
by (metis compl_le_swap1 lres_def schroeder_4)

end

context left_residuated_relation_algebra
begin

text ‹Theorem 32.3›

lemma lres_mult_lres_lres:
"x / (z * y) = (x / y) / z"
by (metis conv_dist_comp double_compl lres_def mult_assoc)

text ‹Theorem 32.5›

lemma lres_dist_inf:
"(x  y) / z = (x / z)  (y / z)"
by (metis compl_inf compl_sup lres_def mult_right_dist_sup)

text ‹Theorem 32.6›

assumes "vector x"
shows "(x  y) / z = x  (y / z)"
proof -
have "(x  y) / z = -((-x  -y) * zT)"
by (simp add: lres_def)
also have "... = -(-x  (-y * zT))"
using assms vector_complement_closed vector_inf_comp by auto
also have "... = x  (y / z)"
by (simp add: lres_def)
finally show ?thesis
.
qed

text ‹Theorem 32.7›

lemma lres_top_vector:
"vector (x / top)"
using equivalence_top_closed lres_def vector_complement_closed vector_mult_closed vector_top_closed by auto

text ‹Theorem 32.10›

lemma lres_top_export_inf_mult:
"((x / top)  y) * z = (x / top)  (y * z)"
by (simp add: vector_inf_comp lres_top_vector)

lemma N_lres:
"N(x) = x / top  1"
using lres_def by auto

end

class complete_relation_algebra = relation_algebra + complete_lattice
begin

definition mu :: "('a  'a)  'a" where "mu f  Inf { y . f y  y }"
definition nu :: "('a  'a)  'a" where "nu f  Sup { y . y  f y }"

lemma mu_lower_bound:
"f x  x  mu f  x"
by (auto simp add: mu_def intro: Inf_lower)

lemma mu_greatest_lower_bound:
"(y . f y  y  x  y)  x  mu f"
using lfp_def lfp_greatest mu_def by auto

lemma mu_unfold_1:
"isotone f  f (mu f)  mu f"
by (metis mu_greatest_lower_bound order_trans mu_lower_bound isotone_def)

lemma mu_unfold_2:
"isotone f  mu f  f (mu f)"
by (simp add: mu_lower_bound mu_unfold_1 ord.isotone_def)

lemma mu_unfold:
"isotone f  mu f = f (mu f)"
by (simp add: order.antisym mu_unfold_1 mu_unfold_2)

lemma mu_const:
"mu (λx . y) = y"
by (simp add: isotone_def mu_unfold)

lemma mu_lpfp:
"isotone f  is_least_prefixpoint f (mu f)"
by (simp add: is_least_prefixpoint_def mu_lower_bound mu_unfold_1)

lemma mu_lfp:
"isotone f  is_least_fixpoint f (mu f)"
by (metis is_least_fixpoint_def mu_lower_bound mu_unfold order_refl)

lemma mu_pmu:
"isotone f   f = mu f"
using least_prefixpoint_same mu_lpfp by force

lemma mu_mu:
"isotone f  μ f = mu f"
using least_fixpoint_same mu_lfp by fastforce

end

class omega_relation_algebra = relation_algebra + star + omega +
assumes ra_star_left_unfold : "1  y * y  y"
assumes ra_star_left_induct : "z  y * x  x  y * z  x"
assumes ra_star_right_induct: "z  x * y  x  z * y  x"
assumes ra_omega_unfold: "yω = y * yω"
assumes ra_omega_induct: "x  z  y * x  x  yω  y * z"
begin

subclass bounded_omega_algebra
apply unfold_locales
using ra_star_left_unfold apply blast
using ra_star_left_induct apply blast
using ra_star_right_induct apply blast
using ra_omega_unfold apply blast
using ra_omega_induct by blast

end

text ‹Theorem 38›

sublocale omega_relation_algebra < n_omega_algebra where sup = sup and bot = bot and top = top and inf = inf and n = N and L = top and apx = greater_eq and Omega = "λx . N(xω) * top  x"
apply unfold_locales
apply simp
using n_split_omega_mult omega_vector star_mult_omega apply force
by simp

end