matita/contribs/CoRN-Decl/algebra/CMonoids.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 set "baseuri" "cic:/matita/CoRN-Decl/algebra/CMonoids".
  18
  19 include "CoRN.ma".
  20
  21 (* $Id: CMonoids.v,v 1.3 2004/04/07 15:07:57 lcf Exp $ *)
  22
  23 (*#* printing Zero %\ensuremath{\mathbf0}% #0# *)
  24
  25 include "algebra/CSemiGroups.ma".
  26
  27 (* Begin_SpecReals *)
  28
  29 (*#*
  30 * Monoids %\label{section:monoids}%
  31 ** Definition of monoids
  32 *)
  33
  34 inline "cic:/CoRN/algebra/CMonoids/is_rht_unit.con".
  35
  36 (* End_SpecReals *)
  37
  38 inline "cic:/CoRN/algebra/CMonoids/is_lft_unit.con".
  39
  40 (* UNEXPORTED
  41 Implicit Arguments is_lft_unit [S].
  42 *)
  43
  44 (* Begin_SpecReals *)
  45
  46 (* UNEXPORTED
  47 Implicit Arguments is_rht_unit [S].
  48 *)
  49
  50 inline "cic:/CoRN/algebra/CMonoids/is_CMonoid.ind".
  51
  52 inline "cic:/CoRN/algebra/CMonoids/CMonoid.ind".
  53
  54 coercion "cic:/matita/CoRN-Decl/algebra/CMonoids/cm_crr.con" 0 (* compounds *).
  55
  56 (*#*
  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}%
  62 *)
  63
  64 (* Begin_SpecReals *)
  65
  66 (*#*
  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.
  71 *)
  72
  73 inline "cic:/CoRN/algebra/CMonoids/nonZeroP.con".
  74
  75 (* End_SpecReals *)
  76
  77 (* UNEXPORTED
  78 Implicit Arguments nonZeroP [M].
  79 *)
  80
  81 (*#*
  82 ** Monoid axioms
  83 %\begin{convention}% Let [M] be a monoid.
  84 %\end{convention}%
  85 *)
  86
  87 (* UNEXPORTED
  88 Section CMonoid_axioms.
  89 *)
  90
  91 inline "cic:/CoRN/algebra/CMonoids/M.var".
  92
  93 inline "cic:/CoRN/algebra/CMonoids/CMonoid_is_CMonoid.con".
  94
  95 inline "cic:/CoRN/algebra/CMonoids/cm_rht_unit.con".
  96
  97 inline "cic:/CoRN/algebra/CMonoids/cm_lft_unit.con".
  98
  99 (* UNEXPORTED
 100 End CMonoid_axioms.
 101 *)
 102
 103 (*#*
 104 ** Monoid basics
 105 %\begin{convention}% Let [M] be a monoid.
 106 %\end{convention}%
 107 *)
 108
 109 (* UNEXPORTED
 110 Section CMonoid_basics.
 111 *)
 112
 113 inline "cic:/CoRN/algebra/CMonoids/M.var".
 114
 115 inline "cic:/CoRN/algebra/CMonoids/cm_rht_unit_unfolded.con".
 116
 117 inline "cic:/CoRN/algebra/CMonoids/cm_lft_unit_unfolded.con".
 118
 119 (* UNEXPORTED
 120 Hint Resolve cm_rht_unit_unfolded cm_lft_unit_unfolded: algebra.
 121 *)
 122
 123 inline "cic:/CoRN/algebra/CMonoids/cm_unit_unique_lft.con".
 124
 125 inline "cic:/CoRN/algebra/CMonoids/cm_unit_unique_rht.con".
 126
 127 (* Begin_SpecReals *)
 128
 129 (*#*
 130 The proof component of the monoid is irrelevant.
 131 *)
 132
 133 inline "cic:/CoRN/algebra/CMonoids/is_CMonoid_proof_irr.con".
 134
 135 (* End_SpecReals *)
 136
 137 (*#*
 138 ** Submonoids
 139 %\begin{convention}%
 140 Let [P] a predicate on [M] containing [Zero] and closed under [[+]].
 141 %\end{convention}%
 142 *)
 143
 144 (* UNEXPORTED
 145 Section SubCMonoids.
 146 *)
 147
 148 inline "cic:/CoRN/algebra/CMonoids/P.var".
 149
 150 inline "cic:/CoRN/algebra/CMonoids/Punit.var".
 151
 152 inline "cic:/CoRN/algebra/CMonoids/op_pres_P.var".
 153
 154 inline "cic:/CoRN/algebra/CMonoids/subcrr.con".
 155
 156 inline "cic:/CoRN/algebra/CMonoids/ismon_scrr.con".
 157
 158 inline "cic:/CoRN/algebra/CMonoids/Build_SubCMonoid.con".
 159
 160 (* UNEXPORTED
 161 End SubCMonoids.
 162 *)
 163
 164 (* UNEXPORTED
 165 End CMonoid_basics.
 166 *)
 167
 168 (* UNEXPORTED
 169 Hint Resolve cm_rht_unit_unfolded cm_lft_unit_unfolded: algebra.
 170 *)
 171