helm/software/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 (* $Id: CMonoids.v,v 1.3 2004/04/07 15:07:57 lcf Exp $ *)
  20
  21 (*#* printing Zero %\ensuremath{\mathbf0}% #0# *)
  22
  23 (* INCLUDE
  24 CSemiGroups
  25 *)
  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 (*#*
  55 %\begin{nameconvention}%
  56 In the names of lemmas, we will denote [Zero] with [zero].
  57 We denote [ [#] Zero] in the names of lemmas by [ap_zero]
  58 (and not, e.g.%\% [nonzero]).
  59 %\end{nameconvention}%
  60 *)
  61
  62 (* Begin_SpecReals *)
  63
  64 (*#*
  65 The predicate "non-zero" is defined.
  66 In lemmas we will continue to write [x [#] Zero], rather than
  67 [(nonZeroP x)], but the predicate is useful for some high-level definitions,
  68 e.g. for the setoid of non-zeros.
  69 *)
  70
  71 inline cic:/CoRN/algebra/CMonoids/nonZeroP.con.
  72
  73 (* End_SpecReals *)
  74
  75 (* UNEXPORTED
  76 Implicit Arguments nonZeroP [M].
  77 *)
  78
  79 (*#*
  80 ** Monoid axioms
  81 %\begin{convention}% Let [M] be a monoid.
  82 %\end{convention}%
  83 *)
  84
  85 (* UNEXPORTED
  86 Section CMonoid_axioms.
  87 *)
  88
  89 inline cic:/CoRN/algebra/CMonoids/M.var.
  90
  91 inline cic:/CoRN/algebra/CMonoids/CMonoid_is_CMonoid.con.
  92
  93 inline cic:/CoRN/algebra/CMonoids/cm_rht_unit.con.
  94
  95 inline cic:/CoRN/algebra/CMonoids/cm_lft_unit.con.
  96
  97 (* UNEXPORTED
  98 End CMonoid_axioms.
  99 *)
 100
 101 (*#*
 102 ** Monoid basics
 103 %\begin{convention}% Let [M] be a monoid.
 104 %\end{convention}%
 105 *)
 106
 107 (* UNEXPORTED
 108 Section CMonoid_basics.
 109 *)
 110
 111 inline cic:/CoRN/algebra/CMonoids/M.var.
 112
 113 inline cic:/CoRN/algebra/CMonoids/cm_rht_unit_unfolded.con.
 114
 115 inline cic:/CoRN/algebra/CMonoids/cm_lft_unit_unfolded.con.
 116
 117 (* UNEXPORTED
 118 Hint Resolve cm_rht_unit_unfolded cm_lft_unit_unfolded: algebra.
 119 *)
 120
 121 inline cic:/CoRN/algebra/CMonoids/cm_unit_unique_lft.con.
 122
 123 inline cic:/CoRN/algebra/CMonoids/cm_unit_unique_rht.con.
 124
 125 (* Begin_SpecReals *)
 126
 127 (*#*
 128 The proof component of the monoid is irrelevant.
 129 *)
 130
 131 inline cic:/CoRN/algebra/CMonoids/is_CMonoid_proof_irr.con.
 132
 133 (* End_SpecReals *)
 134
 135 (*#*
 136 ** Submonoids
 137 %\begin{convention}%
 138 Let [P] a predicate on [M] containing [Zero] and closed under [[+]].
 139 %\end{convention}%
 140 *)
 141
 142 (* UNEXPORTED
 143 Section SubCMonoids.
 144 *)
 145
 146 inline cic:/CoRN/algebra/CMonoids/P.var.
 147
 148 inline cic:/CoRN/algebra/CMonoids/Punit.var.
 149
 150 inline cic:/CoRN/algebra/CMonoids/op_pres_P.var.
 151
 152 inline cic:/CoRN/algebra/CMonoids/subcrr.con.
 153
 154 inline cic:/CoRN/algebra/CMonoids/ismon_scrr.con.
 155
 156 inline cic:/CoRN/algebra/CMonoids/Build_SubCMonoid.con.
 157
 158 (* UNEXPORTED
 159 End SubCMonoids.
 160 *)
 161
 162 (* UNEXPORTED
 163 End CMonoid_basics.
 164 *)
 165
 166 (* UNEXPORTED
 167 Hint Resolve cm_rht_unit_unfolded cm_lft_unit_unfolded: algebra.
 168 *)
 169