Theory RightComplementedMonoid

section‹Right Complemented Monoid›

theory RightComplementedMonoid
imports LeftComplementedMonoid
begin

class left_pordered_monoid_mult = order + monoid_mult +
  assumes mult_left_mono: "a ≤ b ⟹ c * a ≤ c * b"

class integral_left_pordered_monoid_mult = left_pordered_monoid_mult + one_greatest

class right_residuated = ord + times + right_imp +
  assumes right_residual: "(a * x ≤ b) = (x ≤ a r→ b)"

class right_residuated_pordered_monoid = integral_left_pordered_monoid_mult + right_residuated

class right_inf = inf + times + right_imp +
  assumes inf_r_def: "(a ⊓ b)  = a * (a r→ b)"

class right_complemented_monoid = right_residuated_pordered_monoid + right_inf +
  assumes left_divisibility: "(a ≤ b) = (∃ c . a = b * c)"

sublocale right_complemented_monoid < dual: left_complemented_monoid "λ a b . b * a" "(⊓)" "(r→)" 1 "(≤)" "(<)"
  apply unfold_locales
  apply (simp_all add: inf_r_def mult.assoc mult_left_mono)
  apply (simp add: right_residual)
  by (simp add: left_divisibility)

context right_complemented_monoid begin
lemma rcm_D: "a r→ a = 1"
  by (rule dual.lcm_D)

subclass semilattice_inf
    by unfold_locales

lemma right_semilattice_inf: "class.semilattice_inf inf (≤) (<)"
  by unfold_locales

  lemma right_one_inf [simp]: "1 ⊓ a = a"
    by simp

  lemma right_one_impl [simp]: "1 r→ a = a"
    by simp

  lemma rcm_A: "a * (a r→ b) = b * (b r→ a)"
    by (rule dual.lcm_A)

  lemma rcm_B: "((b * a) r→ c) = (a r→ (b r→ c))"
    by (rule dual.lcm_B)

  lemma rcm_C: "(a ≤ b) = ((a r→ b) = 1)"
    by (rule dual.lcm_C)
  end

class right_complemented_monoid_nole_algebra = right_imp + one_times + right_inf + less_def +
  assumes right_impl_one [simp]: "a r→ a = 1"
  and right_impl_times: "a * (a r→ b) = b * (b r→ a)"
  and right_impl_ded: "((a * b) r→ c) = (b r→ (a r→ c))"

class right_complemented_monoid_algebra = right_complemented_monoid_nole_algebra +
  assumes right_lesseq: "(a ≤ b) = ((a r→ b) = 1)"
begin
end

sublocale right_complemented_monoid_algebra < dual_algebra: left_complemented_monoid_algebra "λ a b . b * a" inf "(r→)" "(≤)" "(<)" 1
  apply (unfold_locales, simp_all)
  by (rule inf_r_def, rule right_impl_times, rule right_impl_ded, rule right_lesseq)

context right_complemented_monoid_algebra begin

subclass right_complemented_monoid
  apply unfold_locales
  apply simp_all
  apply (simp add: dual_algebra.mult.assoc)
  apply (simp add: dual_algebra.mult_right_mono)
  apply (simp add: dual_algebra.left_residual)
  by (simp add: dual_algebra.right_divisibility)
end

lemma (in right_complemented_monoid) right_complemented_monoid: "class.right_complemented_monoid_algebra (≤) (<) 1 (*) inf (r→)"
  by (unfold_locales, simp_all add: less_le_not_le rcm_A rcm_B rcm_C rcm_D)

(*
sublocale right_complemented_monoid < rcm: right_complemented_monoid_algebra "(≤)" "(<)" 1 "( * )" inf "(r→)"
  by (unfold_locales, simp_all add: less_le_not_le rcm_A rcm_B rcm_C rcm_D)
*)

end