helm/software/matita/contribs/procedural/CoRN/algebra/CMonoids.mma

   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 include "CoRN.ma".
  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 "algebra/CSemiGroups.ma".
  24
  25 (* Begin_SpecReals *)
  26
  27 (*#*
  28 * Monoids %\label{section:monoids}%
  29 ** Definition of monoids
  30 *)
  31
  32 inline procedural "cic:/CoRN/algebra/CMonoids/is_rht_unit.con" as definition.
  33
  34 (* End_SpecReals *)
  35
  36 inline procedural "cic:/CoRN/algebra/CMonoids/is_lft_unit.con" as definition.
  37
  38 (* UNEXPORTED
  39 Implicit Arguments is_lft_unit [S].
  40 *)
  41
  42 (* Begin_SpecReals *)
  43
  44 (* UNEXPORTED
  45 Implicit Arguments is_rht_unit [S].
  46 *)
  47
  48 inline procedural "cic:/CoRN/algebra/CMonoids/is_CMonoid.ind".
  49
  50 inline procedural "cic:/CoRN/algebra/CMonoids/CMonoid.ind".
  51
  52 (* COERCION
  53 cic:/matita/CoRN-Procedural/algebra/CMonoids/cm_crr.con
  54 *)
  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 (* NOTATION
  74 Notation Zero := (cm_unit _).
  75 *)
  76
  77 inline procedural "cic:/CoRN/algebra/CMonoids/nonZeroP.con" as definition.
  78
  79 (* End_SpecReals *)
  80
  81 (* UNEXPORTED
  82 Implicit Arguments nonZeroP [M].
  83 *)
  84
  85 (*#*
  86 ** Monoid axioms
  87 %\begin{convention}% Let [M] be a monoid.
  88 %\end{convention}%
  89 *)
  90
  91 (* UNEXPORTED
  92 Section CMonoid_axioms
  93 *)
  94
  95 (* UNEXPORTED
  96 cic:/CoRN/algebra/CMonoids/CMonoid_axioms/M.var
  97 *)
  98
  99 inline procedural "cic:/CoRN/algebra/CMonoids/CMonoid_is_CMonoid.con" as lemma.
 100
 101 inline procedural "cic:/CoRN/algebra/CMonoids/cm_rht_unit.con" as lemma.
 102
 103 inline procedural "cic:/CoRN/algebra/CMonoids/cm_lft_unit.con" as lemma.
 104
 105 (* UNEXPORTED
 106 End CMonoid_axioms
 107 *)
 108
 109 (*#*
 110 ** Monoid basics
 111 %\begin{convention}% Let [M] be a monoid.
 112 %\end{convention}%
 113 *)
 114
 115 (* UNEXPORTED
 116 Section CMonoid_basics
 117 *)
 118
 119 (* UNEXPORTED
 120 cic:/CoRN/algebra/CMonoids/CMonoid_basics/M.var
 121 *)
 122
 123 inline procedural "cic:/CoRN/algebra/CMonoids/cm_rht_unit_unfolded.con" as lemma.
 124
 125 inline procedural "cic:/CoRN/algebra/CMonoids/cm_lft_unit_unfolded.con" as lemma.
 126
 127 (* UNEXPORTED
 128 Hint Resolve cm_rht_unit_unfolded cm_lft_unit_unfolded: algebra.
 129 *)
 130
 131 inline procedural "cic:/CoRN/algebra/CMonoids/cm_unit_unique_lft.con" as lemma.
 132
 133 inline procedural "cic:/CoRN/algebra/CMonoids/cm_unit_unique_rht.con" as lemma.
 134
 135 (* Begin_SpecReals *)
 136
 137 (*#*
 138 The proof component of the monoid is irrelevant.
 139 *)
 140
 141 inline procedural "cic:/CoRN/algebra/CMonoids/is_CMonoid_proof_irr.con" as lemma.
 142
 143 (* End_SpecReals *)
 144
 145 (*#*
 146 ** Submonoids
 147 %\begin{convention}%
 148 Let [P] a predicate on [M] containing [Zero] and closed under [[+]].
 149 %\end{convention}%
 150 *)
 151
 152 (* UNEXPORTED
 153 Section SubCMonoids
 154 *)
 155
 156 (* UNEXPORTED
 157 cic:/CoRN/algebra/CMonoids/CMonoid_basics/SubCMonoids/P.var
 158 *)
 159
 160 (* UNEXPORTED
 161 cic:/CoRN/algebra/CMonoids/CMonoid_basics/SubCMonoids/Punit.var
 162 *)
 163
 164 (* UNEXPORTED
 165 cic:/CoRN/algebra/CMonoids/CMonoid_basics/SubCMonoids/op_pres_P.var
 166 *)
 167
 168 inline procedural "cic:/CoRN/algebra/CMonoids/CMonoid_basics/SubCMonoids/subcrr.con" "CMonoid_basics__SubCMonoids__" as definition.
 169
 170 inline procedural "cic:/CoRN/algebra/CMonoids/ismon_scrr.con" as lemma.
 171
 172 inline procedural "cic:/CoRN/algebra/CMonoids/Build_SubCMonoid.con" as definition.
 173
 174 (* UNEXPORTED
 175 End SubCMonoids
 176 *)
 177
 178 (* UNEXPORTED
 179 End CMonoid_basics
 180 *)
 181
 182 (* UNEXPORTED
 183 Hint Resolve cm_rht_unit_unfolded cm_lft_unit_unfolded: algebra.
 184 *)
 185