Theory LeftComplementedMonoid

section‹Left Complemented Monoid›

theory LeftComplementedMonoid
  imports Operations LatticeProperties.Lattice_Prop

class right_pordered_monoid_mult = order + monoid_mult +
  assumes mult_right_mono: "a  b  a * c  b * c"

class one_greatest = one + ord +
  assumes one_greatest [simp]: "a  1"

class integral_right_pordered_monoid_mult = right_pordered_monoid_mult + one_greatest

class left_residuated = ord + times + left_imp +
  assumes left_residual: "(x * a  b) = (x  a l→ b)"

class left_residuated_pordered_monoid = integral_right_pordered_monoid_mult + left_residuated

class left_inf = inf + times + left_imp +
  assumes inf_l_def: "(a  b)  = (a l→ b) * a"

class left_complemented_monoid = left_residuated_pordered_monoid + left_inf +
  assumes right_divisibility: "(a  b) = ( c . a = c * b)"
lemma lcm_D: "a l→ a = 1"
  apply (rule order.antisym, simp)
  by (unfold left_residual [THEN sym], simp)

subclass semilattice_inf
    apply unfold_locales
    apply (metis inf_l_def right_divisibility)
    apply (metis inf_l_def left_residual order_refl)    
    by (metis inf_l_def left_residual mult_right_mono right_divisibility)

  lemma left_one_inf [simp]: "1  a = a" 
    by (rule order.antisym, simp_all)

  lemma left_one_impl [simp]: "1 l→ a = a"
    (*by (metis inf_l_def left_one_inf mult.right_neutral)*)
    proof -
      have "1 l→ a = 1  a" by (unfold inf_l_def, simp)
      also have "1  a = a" by simp
      finally show ?thesis .

  lemma lcm_A: "(a l→ b) * a = (b l→ a) * b"
    apply (unfold inf_l_def [THEN sym])
    by (simp add: inf_commute)

  lemma lcm_B: "((a * b) l→ c) = (a l→ (b l→ c))" 
    apply (rule order.antisym)
    apply (simp add: left_residual [THEN sym] mult.assoc)
    apply (simp add: left_residual)

    apply (simp add: left_residual [THEN sym])
    apply (rule_tac y="(b l→ c) * b" in order_trans)
    apply (simp add: mult.assoc [THEN sym]) 
    apply (rule mult_right_mono)
    by (simp_all add: left_residual)
  lemma lcm_C: "(a  b) = ((a l→ b) = 1)"
    (*by (metis eq_iff left_residual mult.left_neutral one_greatest)*)
    proof -
      have "(a  b) = (1 * a  b)" by simp
      also have " = (1  a l→ b)" by (unfold left_residual, simp)
      also have " = (a l→ b = 1)" apply safe by(rule order.antisym, simp_all)
      finally show ?thesis .


class less_def = ord +
  assumes less_def: "(a < b) = ((a  b)  ¬ (b  a))"

class one_times = one + times +
  assumes one_left [simp]: "1 * a = a" 
  and one_right [simp]: "a * 1 = a"

class left_complemented_monoid_algebra = left_imp + one_times + left_inf + less_def +
  assumes left_impl_one [simp]: "a l→ a = 1"
  and left_impl_times: "(a l→ b) * a = (b l→ a) * b"
  and left_impl_ded: "((a * b) l→ c) = (a l→ (b l→ c))"
  and left_lesseq: "(a  b) = ((a l→ b) = 1)"
  lemma A: "(1 l→ a) l→ 1 = 1"
    proof -
      have "(1 l→ a) l→ 1 = (1 l→ a) * 1 l→ 1" by simp
      also have "... = (a l→ 1) * a l→ 1" by (subst left_impl_times, simp)
      also have "... = 1" by (simp add: left_impl_ded)
      finally show ?thesis .

  subclass order
      fix x y show "(x < y) = (x  y  ¬ y  x)" by (unfold less_def, simp)
      fix x show "x  x" by (unfold left_lesseq, simp)
      fix x y z assume a: "x  y" assume b: "y  z"
      have "x l→ z = 1 * x l→ z" by simp 
      also have "... = (x l→ y) * x l→ z" by (cut_tac a, simp add: left_lesseq)
      also have "... = (y l→ x) * y l→ z" by (simp add: left_impl_times)
      also have "... = (y l→ x) l→ (y l→ z)" by (simp add: left_impl_ded)
      also have "... = (y l→ x) l→ 1" by (cut_tac b, simp add: left_lesseq)
      also have "... = (1 * y l→ x) l→ 1" by simp
      also have "... = (1 l→ (y l→ x)) l→ 1" by (subst left_impl_ded, simp)
      also have "... = 1" by (simp add: A)
      finally show "x  z"  by (simp add: left_lesseq)
      fix x y z assume a: "x  y" assume b: "y  x"
      have "x = (x l→ y) * x" by (cut_tac a, simp add: left_lesseq)
      also have "... = (y l→ x) * y" by (simp add: left_impl_times)
      also have "... = y" by (cut_tac b, simp add: left_lesseq)
      finally show "x = y" .

  lemma B: "(1 l→ a)  1"
    apply (unfold left_lesseq)
    by (rule A)

  lemma C: "a  (1 l→ a)"
    by (simp add: left_lesseq left_impl_ded [THEN sym])

  lemma D: "a  1"
    apply (rule_tac y = "1 l→ a" in order_trans)
    by (simp_all add: C B)

  lemma less_eq: "(a  b) = ( c . a = (c * b))"
    (*by (metis left_impl_ded left_impl_one left_impl_times left_lesseq one_left)*)
    apply safe
    apply (unfold left_lesseq)
    apply (rule_tac x = "b l→ a" in exI)
    apply (simp add: left_impl_times)
    apply (simp add: left_impl_ded)
    apply (case_tac "c  1")
    apply (simp add: left_lesseq)
    by (simp add: D)

  lemma F: "(a * b) * c l→ z = a * (b * c) l→ z"
    by (simp add: left_impl_ded)

  lemma associativity: "(a * b) * c = a * (b * c)"
    (*by (metis F left_impl_one left_impl_times one_left)*)
    apply (rule order.antisym)
    apply (unfold left_lesseq)
    apply (simp add: F)
    by (simp add: F [THEN sym])

  lemma H: "a * b  b"
    apply (simp add: less_eq)
    by auto

  lemma I: "a * b l→ b = 1"
    apply (case_tac "a * b  b")
    apply (simp add: left_lesseq)
    by (simp add: H)

  lemma K: "a  b  a * c  b * c"
    apply (unfold less_eq)
    apply clarify
    apply (rule_tac x = "ca" in exI)
    by (simp add: associativity) 

  lemma L: "(x * a  b) = (x  a l→ b)"
    by (simp add: left_lesseq left_impl_ded)

  subclass left_complemented_monoid 
    apply unfold_locales 
    apply (simp_all add:  less_def D associativity K)
    apply (simp add: L)
    by (simp add: less_eq)

lemma (in left_complemented_monoid) left_complemented_monoid: 
    "class.left_complemented_monoid_algebra (*) inf (l→) (≤) (<) 1"
  by (unfold_locales, simp_all add: less_le_not_le lcm_A lcm_B lcm_C lcm_D)