Theory Relation_Subalgebras

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

section ‹Subalgebras of Relation Algebras›

text ‹
In this theory we consider the algebraic structure of regular elements, coreflexives, vectors and covectors in Stone relation algebras.
These elements form important subalgebras and substructures of relation algebras.
›

theory Relation_Subalgebras

imports Stone_Algebras.Stone_Construction Relation_Algebras

begin

text ‹
The regular elements of a Stone relation algebra form a relation subalgebra.
›

instantiation regular :: (stone_relation_algebra) relation_algebra
begin

lift_definition times_regular :: "'a regular ⇒ 'a regular ⇒ 'a regular" is times
  using regular_mult_closed regular_closed_p by blast

lift_definition conv_regular :: "'a regular ⇒ 'a regular" is conv
  using conv_complement by blast

lift_definition one_regular :: "'a regular" is 1
  using regular_one_closed by blast

instance
  apply intro_classes
  apply (metis (mono_tags, lifting) times_regular.rep_eq Rep_regular_inject comp_associative)
  apply (metis (mono_tags, lifting) times_regular.rep_eq Rep_regular_inject mult_right_dist_sup sup_regular.rep_eq)
  apply (metis (mono_tags, lifting) times_regular.rep_eq Rep_regular_inject bot_regular.rep_eq semiring.mult_zero_left)
  apply (simp add: one_regular.rep_eq times_regular.rep_eq Rep_regular_inject[THEN sym])
  using Rep_regular_inject conv_regular.rep_eq apply force
  apply (metis (mono_tags, lifting) Rep_regular_inject conv_dist_sup conv_regular.rep_eq sup_regular.rep_eq)
  apply (metis (mono_tags, lifting) conv_regular.rep_eq times_regular.rep_eq Rep_regular_inject conv_dist_comp)
  by (auto simp add: conv_regular.rep_eq dedekind_1 inf_regular.rep_eq less_eq_regular.rep_eq times_regular.rep_eq)

end

text ‹
The coreflexives (tests) in an idempotent semiring form a bounded idempotent subsemiring.
›

typedef (overloaded) 'a coreflexive = "coreflexives::'a::non_associative_left_semiring set"
  by auto

lemma simp_coreflexive [simp]:
  "∃y . Rep_coreflexive x ≤ 1"
  using Rep_coreflexive by simp

setup_lifting type_definition_coreflexive

instantiation coreflexive :: (idempotent_semiring) bounded_idempotent_semiring
begin

lift_definition sup_coreflexive :: "'a coreflexive ⇒ 'a coreflexive ⇒ 'a coreflexive" is sup
  by simp

lift_definition times_coreflexive :: "'a coreflexive ⇒ 'a coreflexive ⇒ 'a coreflexive" is times
  by (simp add: coreflexive_mult_closed)

lift_definition bot_coreflexive :: "'a coreflexive" is bot
  by simp

lift_definition one_coreflexive :: "'a coreflexive" is 1
  by simp

lift_definition top_coreflexive :: "'a coreflexive" is 1
  by simp

lift_definition less_eq_coreflexive :: "'a coreflexive ⇒ 'a coreflexive ⇒ bool" is less_eq .

lift_definition less_coreflexive :: "'a coreflexive ⇒ 'a coreflexive ⇒ bool" is less .

instance
  apply intro_classes
  apply (simp_all add: less_coreflexive.rep_eq less_eq_coreflexive.rep_eq less_le_not_le)[2]
  apply (meson less_eq_coreflexive.rep_eq order_trans)
  apply (simp_all add: Rep_coreflexive_inject bot_coreflexive.rep_eq less_eq_coreflexive.rep_eq sup_coreflexive.rep_eq)[5]
  apply (simp add: semiring.distrib_left less_eq_coreflexive.rep_eq sup_coreflexive.rep_eq times_coreflexive.rep_eq)
  apply (metis (mono_tags, lifting) sup_coreflexive.rep_eq times_coreflexive.rep_eq Rep_coreflexive_inject mult_right_dist_sup)
  apply (simp add: times_coreflexive.rep_eq bot_coreflexive.rep_eq Rep_coreflexive_inject[THEN sym])
  apply (simp add: one_coreflexive.rep_eq times_coreflexive.rep_eq Rep_coreflexive_inject[THEN sym])
  apply (simp add: one_coreflexive.rep_eq less_eq_coreflexive.rep_eq times_coreflexive.rep_eq)
  apply (simp only: sup_coreflexive.rep_eq top_coreflexive.rep_eq Rep_coreflexive_inject[THEN sym], metis Abs_coreflexive_cases Abs_coreflexive_inverse mem_Collect_eq sup.absorb2)
  apply (simp add: less_eq_coreflexive.rep_eq mult.assoc times_coreflexive.rep_eq)
  apply (metis (mono_tags, lifting) times_coreflexive.rep_eq Rep_coreflexive_inject mult.assoc)
  using Rep_coreflexive_inject one_coreflexive.rep_eq times_coreflexive.rep_eq apply fastforce
  apply (metis (mono_tags, lifting) sup_coreflexive.rep_eq times_coreflexive.rep_eq Rep_coreflexive_inject mult_left_dist_sup)
  by (simp add: times_coreflexive.rep_eq bot_coreflexive.rep_eq Rep_coreflexive_inject[THEN sym])

end

text ‹
The coreflexives (tests) in a Stone relation algebra form a Stone relation algebra where the pseudocomplement is taken relative to the identity relation and converse is the identity function.
›

instantiation coreflexive :: (stone_relation_algebra) stone_relation_algebra
begin

lift_definition inf_coreflexive :: "'a coreflexive ⇒ 'a coreflexive ⇒ 'a coreflexive" is inf
  by (simp add: le_infI1)

lift_definition minus_coreflexive :: "'a coreflexive ⇒ 'a coreflexive ⇒ 'a coreflexive" is "λx y . x ⊓ -y"
  by (simp add: le_infI1)

lift_definition uminus_coreflexive :: "'a coreflexive ⇒ 'a coreflexive" is "λx . -x ⊓ 1"
  by simp

lift_definition conv_coreflexive :: "'a coreflexive ⇒ 'a coreflexive" is id
  by simp

instance
  apply intro_classes
  apply (auto simp: inf_coreflexive.rep_eq less_eq_coreflexive.rep_eq)[3]
  apply simp
  apply (metis (mono_tags, lifting) Rep_coreflexive_inject inf_coreflexive.rep_eq sup_coreflexive.rep_eq sup_inf_distrib1)
  apply (metis (mono_tags, lifting) Rep_coreflexive_inject bot_coreflexive.rep_eq top_greatest coreflexive_pseudo_complement inf_coreflexive.rep_eq less_eq_coreflexive.rep_eq one_coreflexive.rep_eq one_coreflexive_def top_coreflexive_def uminus_coreflexive.rep_eq)
  apply (metis (mono_tags, lifting) Rep_coreflexive_inject maddux_3_21_pp one_coreflexive.rep_eq one_coreflexive_def pp_dist_inf pp_one regular_closed_p sup_coreflexive.rep_eq sup_right_top top_coreflexive_def uminus_coreflexive.rep_eq)
  apply (auto simp: mult.assoc mult_right_dist_sup)[4]
  using Rep_coreflexive_inject conv_coreflexive.rep_eq apply fastforce
  apply (metis (mono_tags) Rep_coreflexive_inject conv_coreflexive.rep_eq)
  apply (metis (mono_tags, lifting) Rep_coreflexive_inject top_greatest conv_coreflexive.rep_eq coreflexive_commutative less_eq_coreflexive.rep_eq one_coreflexive.rep_eq one_coreflexive_def times_coreflexive.rep_eq top_coreflexive_def)
  apply (simp only: conv_coreflexive.rep_eq less_eq_coreflexive.rep_eq one_coreflexive.rep_eq times_coreflexive.rep_eq inf_coreflexive.rep_eq Rep_coreflexive_inject[THEN sym], metis coreflexive_dedekind Rep_coreflexive mem_Collect_eq)
  apply (metis (mono_tags, lifting) Rep_coreflexive Rep_coreflexive_inject coreflexive_pp_dist_comp mem_Collect_eq times_coreflexive.rep_eq uminus_coreflexive.rep_eq)
  by (metis (mono_tags, opaque_lifting) Rep_coreflexive_inverse inf.commute inf.idem inf_import_p one_coreflexive.rep_eq pp_one uminus_coreflexive.rep_eq)

end

text ‹
Vectors in a Stone relation algebra form a Stone subalgebra.
›

typedef (overloaded) 'a vector = "vectors::'a::bounded_pre_left_semiring set"
  using surjective_top_closed by blast

lemma simp_vector [simp]:
  "∃y . Rep_vector x * top = Rep_vector x"
  using Rep_vector by simp

setup_lifting type_definition_vector

instantiation vector :: (stone_relation_algebra) stone_algebra
begin

lift_definition sup_vector :: "'a vector ⇒ 'a vector ⇒ 'a vector" is sup
  by (simp add: vector_sup_closed)

lift_definition inf_vector :: "'a vector ⇒ 'a vector ⇒ 'a vector" is inf
  by (simp add: vector_inf_closed)

lift_definition uminus_vector :: "'a vector ⇒ 'a vector" is uminus
  by (simp add: vector_complement_closed)

lift_definition bot_vector :: "'a vector" is bot
  by simp

lift_definition top_vector :: "'a vector" is top
  by simp

lift_definition less_eq_vector :: "'a vector ⇒ 'a vector ⇒ bool" is less_eq .

lift_definition less_vector :: "'a vector ⇒ 'a vector ⇒ bool" is less .

instance
  apply intro_classes
  apply (auto simp: Rep_vector_inject top_vector.rep_eq bot_vector.rep_eq less_le_not_le inf_vector.rep_eq sup_vector.rep_eq less_eq_vector.rep_eq less_vector.rep_eq)[12]
  apply (metis (mono_tags, lifting) Rep_vector_inject inf_vector.rep_eq sup_inf_distrib1 sup_vector.rep_eq)
  apply (metis (mono_tags, lifting) Rep_vector_inject bot_vector_def bot_vector.rep_eq pseudo_complement inf_vector.rep_eq less_eq_vector.rep_eq uminus_vector.rep_eq)
  by (metis (mono_tags, lifting) sup_vector.rep_eq uminus_vector.rep_eq Rep_vector_inverse stone top_vector.abs_eq)

end

text ‹
Covectors in a Stone relation algebra form a Stone subalgebra.
›

typedef (overloaded) 'a covector = "covectors::'a::bounded_pre_left_semiring set"
  using surjective_top_closed by blast

lemma simp_covector [simp]:
  "∃y . top * Rep_covector x = Rep_covector x"
  using Rep_covector by simp

setup_lifting type_definition_covector

instantiation covector :: (stone_relation_algebra) stone_algebra
begin

lift_definition sup_covector :: "'a covector ⇒ 'a covector ⇒ 'a covector" is sup
  by (simp add: covector_sup_closed)

lift_definition inf_covector :: "'a covector ⇒ 'a covector ⇒ 'a covector" is inf
  by (simp add: covector_inf_closed)

lift_definition uminus_covector :: "'a covector ⇒ 'a covector" is uminus
  by (simp add: covector_complement_closed)

lift_definition bot_covector :: "'a covector" is bot
  by simp

lift_definition top_covector :: "'a covector" is top
  by simp

lift_definition less_eq_covector :: "'a covector ⇒ 'a covector ⇒ bool" is less_eq .

lift_definition less_covector :: "'a covector ⇒ 'a covector ⇒ bool" is less .

instance
  apply intro_classes
  apply (auto simp: Rep_covector_inject less_eq_covector.rep_eq inf_covector.rep_eq bot_covector.rep_eq top_covector.rep_eq sup_covector.rep_eq less_le_not_le less_covector.rep_eq)[12]
  apply (metis (mono_tags, lifting) Rep_covector_inject inf_covector.rep_eq sup_inf_distrib1 sup_covector.rep_eq)
  apply (metis (mono_tags, lifting) Rep_covector_inject bot_covector_def bot_covector.rep_eq pseudo_complement inf_covector.rep_eq less_eq_covector.rep_eq uminus_covector.rep_eq)
  by (metis (mono_tags, lifting) sup_covector.rep_eq uminus_covector.rep_eq Rep_covector_inverse stone top_covector.abs_eq)

end

end