## [4b23aa]: thys / PseudoHoops / RightComplementedMonoid.thy  Maximize  Restore  History

### 89 lines (64 with data), 3.4 kB

 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 header{* 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" "op \" "op r\" 1 "op \" "op <" 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_infix by unfold_locales lemma right_semilattice_inf: "class.semilattice_inf_infix inf op \ op <" by unfold_locales lemma right_one_inf [simp]: "1 \ a = a" by (rule dual.left_one_inf) lemma right_one_impl [simp]: "1 r\ a = a" by (rule dual.left_one_impl) 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 "op r\" "op \" "op <" 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 (op \) (op <) 1 (op *) inf (op 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 "op \" "op <" 1 "op *" inf "op r\" by (unfold_locales, simp_all add: less_le_not_le rcm_A rcm_B rcm_C rcm_D) *) end