# 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)

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