helm/software/matita/contribs/CoRN-Procedural/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 alias id "M" = "cic:/CoRN/algebra/CMonoids/CMonoid_axioms/M.var".
  96
  97 inline procedural "cic:/CoRN/algebra/CMonoids/CMonoid_is_CMonoid.con" as lemma.
  98
  99 inline procedural "cic:/CoRN/algebra/CMonoids/cm_rht_unit.con" as lemma.
 100
 101 inline procedural "cic:/CoRN/algebra/CMonoids/cm_lft_unit.con" as lemma.
 102
 103 (* UNEXPORTED
 104 End CMonoid_axioms
 105 *)
 106
 107 (*#*
 108 ** Monoid basics
 109 %\begin{convention}% Let [M] be a monoid.
 110 %\end{convention}%
 111 *)
 112
 113 (* UNEXPORTED
 114 Section CMonoid_basics
 115 *)
 116
 117 alias id "M" = "cic:/CoRN/algebra/CMonoids/CMonoid_basics/M.var".
 118
 119 inline procedural "cic:/CoRN/algebra/CMonoids/cm_rht_unit_unfolded.con" as lemma.
 120
 121 inline procedural "cic:/CoRN/algebra/CMonoids/cm_lft_unit_unfolded.con" as lemma.
 122
 123 (* UNEXPORTED
 124 Hint Resolve cm_rht_unit_unfolded cm_lft_unit_unfolded: algebra.
 125 *)
 126
 127 inline procedural "cic:/CoRN/algebra/CMonoids/cm_unit_unique_lft.con" as lemma.
 128
 129 inline procedural "cic:/CoRN/algebra/CMonoids/cm_unit_unique_rht.con" as lemma.
 130
 131 (* Begin_SpecReals *)
 132
 133 (*#*
 134 The proof component of the monoid is irrelevant.
 135 *)
 136
 137 inline procedural "cic:/CoRN/algebra/CMonoids/is_CMonoid_proof_irr.con" as lemma.
 138
 139 (* End_SpecReals *)
 140
 141 (*#*
 142 ** Submonoids
 143 %\begin{convention}%
 144 Let [P] a predicate on [M] containing [Zero] and closed under [[+]].
 145 %\end{convention}%
 146 *)
 147
 148 (* UNEXPORTED
 149 Section SubCMonoids
 150 *)
 151
 152 alias id "P" = "cic:/CoRN/algebra/CMonoids/CMonoid_basics/SubCMonoids/P.var".
 153
 154 alias id "Punit" = "cic:/CoRN/algebra/CMonoids/CMonoid_basics/SubCMonoids/Punit.var".
 155
 156 alias id "op_pres_P" = "cic:/CoRN/algebra/CMonoids/CMonoid_basics/SubCMonoids/op_pres_P.var".
 157
 158 inline procedural "cic:/CoRN/algebra/CMonoids/CMonoid_basics/SubCMonoids/subcrr.con" "CMonoid_basics__SubCMonoids__" as definition.
 159
 160 inline procedural "cic:/CoRN/algebra/CMonoids/ismon_scrr.con" as lemma.
 161
 162 inline procedural "cic:/CoRN/algebra/CMonoids/Build_SubCMonoid.con" as definition.
 163
 164 (* UNEXPORTED
 165 End SubCMonoids
 166 *)
 167
 168 (* UNEXPORTED
 169 End CMonoid_basics
 170 *)
 171
 172 (* UNEXPORTED
 173 Hint Resolve cm_rht_unit_unfolded cm_lft_unit_unfolded: algebra.
 174 *)
 175