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

lemma lres_add_export_vector:
  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