# Theory LeftComplementedMonoid

Up to index of Isabelle/HOL/LatticeProperties/PseudoHoops

theory LeftComplementedMonoid
imports Operations Lattice_Prop
`header{* Left Complemented Monoid *}theory LeftComplementedMonoid  imports Operations "../LatticeProperties/Lattice_Prop"beginclass 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_greatestclass 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_residuatedclass left_inf = inf + times + left_imp +  assumes inf_l_def: "(a \<sqinter> b)  = (a l-> b) * a"class left_complemented_monoid = left_residuated_pordered_monoid + left_inf +  assumes right_divisibility: "(a ≤ b) = (∃ c . a = c * b)"beginlemma lcm_D: "a l-> a = 1"  apply (rule 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 \<sqinter> a = a"     by (rule 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 \<sqinter> a" by (unfold inf_l_def, simp)      also have "1 \<sqinter> a = a" by simp      finally show ?thesis .    qed  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 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 antisym, simp_all)      finally show ?thesis .    qed  endclass 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)"begin  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 .    qed  subclass order    proof      fix x y show "(x < y) = (x ≤ y ∧ ¬ y ≤ x)" by (unfold less_def, simp)    next      fix x show "x ≤ x" by (unfold left_lesseq, simp)    next      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)    next      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" .    qed  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 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)  endlemma (in left_complemented_monoid) left_complemented_monoid:     "class.left_complemented_monoid_algebra (op *) inf (op l->) (op ≤) (op <) 1"  by (unfold_locales, simp_all add: less_le_not_le lcm_A lcm_B lcm_C lcm_D)end`