helm/software/matita/contribs/CoRN-Decl/algebra/CSemiGroups.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/CSemiGroups".
  18
  19 include "CoRN.ma".
  20
  21 (* $Id: CSemiGroups.v,v 1.8 2004/04/22 14:49:43 lcf Exp $ *)
  22
  23 (*#* printing [+] %\ensuremath+% #+# *)
  24
  25 (*#* printing {+} %\ensuremath+% #+# *)
  26
  27 include "algebra/CSetoidInc.ma".
  28
  29 (* Begin_SpecReals *)
  30
  31 (*#* *Semigroups
  32
  33 **Definition of the notion of semigroup
  34 *)
  35
  36 inline "cic:/CoRN/algebra/CSemiGroups/is_CSemiGroup.con".
  37
  38 inline "cic:/CoRN/algebra/CSemiGroups/CSemiGroup.ind".
  39
  40 coercion "cic:/matita/CoRN-Decl/algebra/CSemiGroups/csg_crr.con" 0 (* compounds *).
  41
  42 (*#*
  43 %\begin{nameconvention}%
  44 In the %{\em %names%}% of lemmas, we will denote [[+]] with [plus].
  45 %\end{nameconvention}%
  46 *)
  47
  48 (* UNEXPORTED
  49 Implicit Arguments csg_op [c].
  50 *)
  51
  52 (* End_SpecReals *)
  53
  54 (*#* **Semigroup axioms
  55 The axiomatic properties of a semi group.
  56
  57 %\begin{convention}% Let [G] be a semi-group.
  58 %\end{convention}%
  59 *)
  60
  61 (* UNEXPORTED
  62 Section CSemiGroup_axioms.
  63 *)
  64
  65 inline "cic:/CoRN/algebra/CSemiGroups/G.var".
  66
  67 inline "cic:/CoRN/algebra/CSemiGroups/CSemiGroup_is_CSemiGroup.con".
  68
  69 inline "cic:/CoRN/algebra/CSemiGroups/plus_assoc.con".
  70
  71 (* UNEXPORTED
  72 End CSemiGroup_axioms.
  73 *)
  74
  75 (* Begin_SpecReals *)
  76
  77 (*#* **Semigroup basics
  78
  79 %\begin{convention}%
  80 Let [G] be a semi-group.
  81 %\end{convention}%
  82 *)
  83
  84 (* UNEXPORTED
  85 Section CSemiGroup_basics.
  86 *)
  87
  88 inline "cic:/CoRN/algebra/CSemiGroups/G.var".
  89
  90 (* End_SpecReals *)
  91
  92 inline "cic:/CoRN/algebra/CSemiGroups/plus_assoc_unfolded.con".
  93
  94 (* UNEXPORTED
  95 End CSemiGroup_basics.
  96 *)
  97
  98 (* End_SpecReals *)
  99
 100 (* UNEXPORTED
 101 Hint Resolve plus_assoc_unfolded: algebra.
 102 *)
 103
 104 (*#* **Functional operations
 105 We can also define a similar addition operator, which will be denoted by [{+}], on partial functions.
 106
 107 %\begin{convention}% Whenever possible, we will denote the functional construction corresponding to an algebraic operation by the same symbol enclosed in curly braces.
 108 %\end{convention}%
 109
 110 At this stage, we will always consider automorphisms; we %{\em %could%}% treat this in a more general setting, but we feel that it wouldn't really be a useful effort.
 111
 112 %\begin{convention}% Let [G:CSemiGroup] and [F,F':(PartFunct G)] and denote by [P] and [Q], respectively, the predicates characterizing their domains.
 113 %\end{convention}%
 114 *)
 115
 116 (* UNEXPORTED
 117 Section Part_Function_Plus.
 118 *)
 119
 120 inline "cic:/CoRN/algebra/CSemiGroups/G.var".
 121
 122 inline "cic:/CoRN/algebra/CSemiGroups/F.var".
 123
 124 inline "cic:/CoRN/algebra/CSemiGroups/F'.var".
 125
 126 (* begin hide *)
 127
 128 inline "cic:/CoRN/algebra/CSemiGroups/P.con".
 129
 130 inline "cic:/CoRN/algebra/CSemiGroups/Q.con".
 131
 132 (* end hide *)
 133
 134 inline "cic:/CoRN/algebra/CSemiGroups/part_function_plus_strext.con".
 135
 136 inline "cic:/CoRN/algebra/CSemiGroups/Fplus.con".
 137
 138 (*#*
 139 %\begin{convention}% Let [R:G->CProp].
 140 %\end{convention}%
 141 *)
 142
 143 inline "cic:/CoRN/algebra/CSemiGroups/R.var".
 144
 145 inline "cic:/CoRN/algebra/CSemiGroups/included_FPlus.con".
 146
 147 inline "cic:/CoRN/algebra/CSemiGroups/included_FPlus'.con".
 148
 149 inline "cic:/CoRN/algebra/CSemiGroups/included_FPlus''.con".
 150
 151 (* UNEXPORTED
 152 End Part_Function_Plus.
 153 *)
 154
 155 (* UNEXPORTED
 156 Implicit Arguments Fplus [G].
 157 *)
 158
 159 (* UNEXPORTED
 160 Hint Resolve included_FPlus : included.
 161 *)
 162
 163 (* UNEXPORTED
 164 Hint Immediate included_FPlus' included_FPlus'' : included.
 165 *)
 166
 167 (*#* **Subsemigroups
 168 %\begin{convention}%
 169 Let [csg] a semi-group and [P] a non-empty
 170 predicate on the semi-group which is preserved by [[+]].
 171 %\end{convention}%
 172 *)
 173
 174 (* UNEXPORTED
 175 Section SubCSemiGroups.
 176 *)
 177
 178 inline "cic:/CoRN/algebra/CSemiGroups/csg.var".
 179
 180 inline "cic:/CoRN/algebra/CSemiGroups/P.var".
 181
 182 inline "cic:/CoRN/algebra/CSemiGroups/op_pres_P.var".
 183
 184 inline "cic:/CoRN/algebra/CSemiGroups/subcrr.con".
 185
 186 inline "cic:/CoRN/algebra/CSemiGroups/Build_SubCSemiGroup.con".
 187
 188 (* UNEXPORTED
 189 End SubCSemiGroups.
 190 *)
 191