helm/meta_style/set.xml

   1 <!DOCTYPE OpList SYSTEM "operator.dtd">
   2
   3 <OpList xmlns:m="http://www.w3.org/1998/Math/MathML">
   4
   5 <import href="modeset.xsl"/>
   6
   7 <Operator
   8  name  = "IN"
   9  uri   = "cic:/Coq/Sets/Ensembles/Ensembles/In.con"
  10  cook  = "true"
  11  arity = "2">
  12         <mapp>
  13                 <mop tag="in"/>
  14                 <param id="2"/>
  15                 <param id="1" mode="set"/>
  16         </mapp>
  17 </Operator>
  18
  19 <NotOperator
  20  name  = "NOT IN"
  21  uri   = "cic:/Coq/Sets/Ensembles/Ensembles/In.con"
  22  cook  = "true"
  23  arity = "2">
  24         <mapp>
  25                 <m:notin/>
  26                 <param id="2"/>
  27                 <param id="1" mode="set"/>
  28         </mapp>
  29 </NotOperator>
  30
  31 <OpSet
  32  name  = "EMPTY SET"
  33  uri   = "cic:/Coq/Sets/Ensembles/Ensembles/Empty_set.ind"
  34  cook  = "true">
  35
  36         <Case arity="0">
  37                 <mop tag="set" helm:xref="$APP-ID"/>
  38         </Case>
  39
  40         <Case arity="1">
  41                 <mapp>
  42                         <m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
  43                         <param id="1"/>
  44                         <mop tag="set" helm:xref="$APP-ID"/>
  45                 </mapp>
  46         </Case>
  47 </OpSet>
  48
  49 <OpSet
  50  name  = "SINGLETON"
  51  uri   = "cic:/Coq/Sets/Ensembles/Ensembles/Singleton.ind"
  52  cook  = "true">
  53
  54         <Case arity="1">
  55                 <mop tag="set" helm:xref="$APP-ID">
  56                         <param id="1"/>
  57                 </mop>
  58         </Case>
  59
  60         <Case arity="2">
  61                 <mapp>
  62                         <m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
  63                         <param id="2"/>
  64                         <m:set definitionURL="$OP-URI">
  65                                 <param id="1"/>
  66                         </m:set>
  67                 </mapp>
  68         </Case>
  69 </OpSet>
  70
  71 <OpSet
  72  name  = "COUPLE"
  73  uri   = "cic:/Coq/Sets/Ensembles/Ensembles/Couple.ind"
  74  cook  = "true">
  75
  76         <Case arity="2">
  77                 <mop tag="set" helm:xref="$APP-ID">
  78                         <param id="1"/>
  79                         <param id="2"/>
  80                 </mop>
  81         </Case>
  82
  83         <Case arity="3">
  84                 <mapp>
  85                         <m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
  86                         <param id="3"/>
  87                         <m:set definitionURL="$OP-URI">
  88                                 <param id="1"/>
  89                                 <param id="2"/>
  90                         </m:set>
  91                 </mapp>
  92         </Case>
  93 </OpSet>
  94
  95 <OpSet
  96  name  = "TRIPLE"
  97  uri   = "cic:/Coq/Sets/Ensembles/Ensembles/Triple.ind"
  98  cook  = "true">
  99
 100         <Case arity="3">
 101                 <mop tag="set">
 102                         <param id="1"/>
 103                         <param id="2"/>
 104                         <param id="3"/>
 105                 </mop>
 106         </Case>
 107
 108         <Case arity="4">
 109                 <mapp>
 110                         <m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
 111                         <param id="4"/>
 112                         <m:set definitionURL="$OP-URI">
 113                                 <param id="1"/>
 114                                 <param id="2"/>
 115                                 <param id="3"/>
 116                         </m:set>
 117                 </mapp>
 118         </Case>
 119 </OpSet>
 120
 121 <OpSet
 122  name  = "INTERSECTION"
 123  uri   = "cic:/Coq/Sets/Ensembles/Ensembles/Intersection.ind"
 124  cook  = "true">
 125
 126         <Case arity="2">
 127                 <mapp>
 128                         <mop tag="intersect"/>
 129                         <param id="1" mode="set"/>
 130                         <param id="2" mode="set"/>
 131                 </mapp>
 132         </Case>
 133
 134         <Case arity="3">
 135                 <mapp>
 136                         <m:in/>
 137                         <param id="3"/>
 138                         <m:apply>
 139                                 <mop tag="intersect"/>
 140                                 <param id="1" mode="set"/>
 141                                 <param id="2" mode="set"/>
 142                         </m:apply>
 143                 </mapp>
 144         </Case>
 145 </OpSet>
 146
 147 <OpSet
 148  name  = "UNION"
 149  uri   = "cic:/Coq/Sets/Ensembles/Ensembles/Union.ind"
 150  cook  = "true">
 151
 152         <Case arity="2">
 153                 <mapp>
 154                         <mop tag="union"/>
 155                         <param id="1" mode="set"/>
 156                         <param id="2" mode="set"/>
 157                 </mapp>
 158         </Case>
 159
 160         <Case arity="3">
 161                 <mapp>
 162                         <m:in/>
 163                         <param id="3"/>
 164                         <m:apply>
 165                                 <mop tag="union"/>
 166                                 <param id="1" mode="set"/>
 167                                 <param id="2" mode="set"/>
 168                         </m:apply>
 169                 </mapp>
 170         </Case>
 171 </OpSet>
 172
 173 <Operator
 174  name  = "INCLUDED"
 175  uri   = "cic:/Coq/Sets/Ensembles/Ensembles/Included.con"
 176  cook  = "true"
 177  arity = "2">
 178         <mapp>
 179                 <mop tag="subset"/>
 180                 <param id="1" mode="set"/>
 181                 <param id="2" mode="set"/>
 182         </mapp>
 183 </Operator>
 184
 185 <Operator
 186  name  = "STRICTLY INCLUDED"
 187  uri   = "cic:/Coq/Sets/Ensembles/Ensembles/Strict_Included.con"
 188  cook  = "true"
 189  arity = "2">
 190         <mapp>
 191                 <mop tag="prsubset"/>
 192                 <param id="1" mode="set"/>
 193                 <param id="2" mode="set"/>
 194         </mapp>
 195 </Operator>
 196
 197 <OpSet
 198  name  = "SET-DIFF"
 199  uri   = "cic:/Coq/Sets/Ensembles/Ensembles/Setminus.con"
 200  cook  = "true">
 201
 202         <Case arity="2">
 203                 <mapp>
 204                         <mop tag="setdiff"/>
 205                         <param id="1" mode="set"/>
 206                         <param id="2" mode="set"/>
 207                 </mapp>
 208         </Case>
 209
 210         <Case arity="3">
 211                 <mapp>
 212                         <m:in/>
 213                         <param id="3"/>
 214                         <m:apply>
 215                                 <mop tag="setdiff"/>
 216                                 <param id="1" mode="set"/>
 217                                 <param id="2" mode="set"/>
 218                         </m:apply>
 219                 </mapp>
 220         </Case>
 221 </OpSet>
 222
 223 <OpSet
 224  name  = "ADD-ELEM"
 225  uri   = "cic:/Coq/Sets/Ensembles/Ensembles/Add.con"
 226  cook  = "true">
 227
 228         <Case arity="2">
 229                 <mapp>
 230                         <mop tag="union"/>
 231                         <param id="1" mode="set"/>
 232                         <m:set>
 233                                 <param id="2" mode="set"/>
 234                         </m:set>
 235                 </mapp>
 236         </Case>
 237
 238         <Case arity="3">
 239                 <mapp>
 240                         <m:in/>
 241                         <param id="3"/>
 242                         <m:apply>
 243                                 <mop tag="union"/>
 244                                 <param id="1" mode="set"/>
 245                                 <m:set>
 246                                         <param id="2"/>
 247                                 </m:set>
 248                         </m:apply>
 249                 </mapp>
 250         </Case>
 251 </OpSet>
 252
 253 <OpSet
 254  name  = "SUBTRACT-ELEM"
 255  uri   = "cic:/Coq/Sets/Ensembles/Ensembles/Subtract.con"
 256  cook  = "true">
 257
 258         <Case arity="2">
 259                 <mapp>
 260                         <mop tag="setdiff"/>
 261                         <param id="1" mode="set"/>
 262                         <m:set>
 263                                 <param id="2"/>
 264                         </m:set>
 265                 </mapp>
 266         </Case>
 267
 268         <Case arity="3">
 269                 <mapp>
 270                         <m:in/>
 271                         <param id="3"/>
 272                         <m:apply>
 273                                 <mop tag="setdiff"/>
 274                                 <param id="1" mode="set"/>
 275                                 <m:set>
 276                                         <param id="2"/>
 277                                 </m:set>
 278                         </m:apply>
 279                 </mapp>
 280         </Case>
 281 </OpSet>
 282
 283 <Operator
 284  name  = "CARD"
 285  uri   = "cic:/Coq/Sets/Finite_sets/Ensembles_finis/cardinal.ind"
 286  cook  = "true"
 287  arity = "2">
 288         <mapp>
 289                 <m:eq/>
 290                 <m:apply>
 291                         <mop tag="card"/>
 292                         <param id="1" mode="set"/>
 293                 </m:apply>
 294                 <param id="2"/>
 295         </mapp>
 296 </Operator>
 297
 298 <Operator
 299  name  = "SIGMA"
 300  uri   = "cic:/Coq/Init/Specif/Subsets/sig.ind"
 301  arity = "2">
 302         <m:set>
 303                 <mbvar name="x">
 304                         <m:type>
 305                                 <param id="1"/>
 306                         </m:type>
 307                 </mbvar>
 308                 <m:condition>
 309                         <param id="2" bvar="x"/>
 310                 </m:condition>
 311         </m:set>
 312 </Operator>
 313
 314 </OpList>