1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/algebra/CMonoids".
21 (* $Id: CMonoids.v,v 1.3 2004/04/07 15:07:57 lcf Exp $ *)
23 (*#* printing Zero %\ensuremath{\mathbf0}% #0# *)
25 include "algebra/CSemiGroups.ma".
30 * Monoids %\label{section:monoids}%
31 ** Definition of monoids
34 inline "cic:/CoRN/algebra/CMonoids/is_rht_unit.con".
38 inline "cic:/CoRN/algebra/CMonoids/is_lft_unit.con".
41 Implicit Arguments is_lft_unit [S].
47 Implicit Arguments is_rht_unit [S].
50 inline "cic:/CoRN/algebra/CMonoids/is_CMonoid.ind".
52 inline "cic:/CoRN/algebra/CMonoids/CMonoid.ind".
54 coercion cic:/matita/CoRN-Decl/algebra/CMonoids/cm_crr.con 0 (* compounds *).
57 %\begin{nameconvention}%
58 In the names of lemmas, we will denote [Zero] with [zero].
59 We denote [ [#] Zero] in the names of lemmas by [ap_zero]
60 (and not, e.g.%\% [nonzero]).
61 %\end{nameconvention}%
67 The predicate "non-zero" is defined.
68 In lemmas we will continue to write [x [#] Zero], rather than
69 [(nonZeroP x)], but the predicate is useful for some high-level definitions,
70 e.g. for the setoid of non-zeros.
74 Notation Zero := (cm_unit _).
77 inline "cic:/CoRN/algebra/CMonoids/nonZeroP.con".
82 Implicit Arguments nonZeroP [M].
87 %\begin{convention}% Let [M] be a monoid.
92 Section CMonoid_axioms
95 alias id "M" = "cic:/CoRN/algebra/CMonoids/CMonoid_axioms/M.var".
97 inline "cic:/CoRN/algebra/CMonoids/CMonoid_is_CMonoid.con".
99 inline "cic:/CoRN/algebra/CMonoids/cm_rht_unit.con".
101 inline "cic:/CoRN/algebra/CMonoids/cm_lft_unit.con".
109 %\begin{convention}% Let [M] be a monoid.
114 Section CMonoid_basics
117 alias id "M" = "cic:/CoRN/algebra/CMonoids/CMonoid_basics/M.var".
119 inline "cic:/CoRN/algebra/CMonoids/cm_rht_unit_unfolded.con".
121 inline "cic:/CoRN/algebra/CMonoids/cm_lft_unit_unfolded.con".
124 Hint Resolve cm_rht_unit_unfolded cm_lft_unit_unfolded: algebra.
127 inline "cic:/CoRN/algebra/CMonoids/cm_unit_unique_lft.con".
129 inline "cic:/CoRN/algebra/CMonoids/cm_unit_unique_rht.con".
131 (* Begin_SpecReals *)
134 The proof component of the monoid is irrelevant.
137 inline "cic:/CoRN/algebra/CMonoids/is_CMonoid_proof_irr.con".
144 Let [P] a predicate on [M] containing [Zero] and closed under [[+]].
152 alias id "P" = "cic:/CoRN/algebra/CMonoids/CMonoid_basics/SubCMonoids/P.var".
154 alias id "Punit" = "cic:/CoRN/algebra/CMonoids/CMonoid_basics/SubCMonoids/Punit.var".
156 alias id "op_pres_P" = "cic:/CoRN/algebra/CMonoids/CMonoid_basics/SubCMonoids/op_pres_P.var".
158 inline "cic:/CoRN/algebra/CMonoids/CMonoid_basics/SubCMonoids/subcrr.con" "CMonoid_basics__SubCMonoids__".
160 inline "cic:/CoRN/algebra/CMonoids/ismon_scrr.con".
162 inline "cic:/CoRN/algebra/CMonoids/Build_SubCMonoid.con".
173 Hint Resolve cm_rht_unit_unfolded cm_lft_unit_unfolded: algebra.