3 <!-- Copyright (C) 2000, HELM Team -->
5 <!-- This file is part of HELM, an Hypertextual, Electronic -->
6 <!-- Library of Mathematics, developed at the Computer Science -->
7 <!-- Department, University of Bologna, Italy. -->
9 <!-- HELM is free software; you can redistribute it and/or -->
10 <!-- modify it under the terms of the GNU General Public License -->
11 <!-- as published by the Free Software Foundation; either version 2 -->
12 <!-- of the License, or (at your option) any later version. -->
14 <!-- HELM is distributed in the hope that it will be useful, -->
15 <!-- but WITHOUT ANY WARRANTY; without even the implied warranty of -->
16 <!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -->
17 <!-- GNU General Public License for more details. -->
19 <!-- You should have received a copy of the GNU General Public License -->
20 <!-- along with HELM; if not, write to the Free Software -->
21 <!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston, -->
22 <!-- MA 02111-1307, USA. -->
24 <!-- For details, see the HELM World-Wide-Web page, -->
25 <!-- http://cs.unibo.it/helm/. -->
27 <!--******************************************************************-->
28 <!-- Basic Set Theory -->
29 <!-- First draft: April 3 2000 -->
30 <!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena -->
31 <!--******************************************************************-->
33 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
34 xmlns:m="http://www.w3.org/1998/Math/MathML"
35 xmlns:helm="http://www.cs.unibo.it/helm">
38 <!-- ************************* LOGIC *********************************-->
41 <xsl:template match="*" mode="set">
43 <xsl:when test="name() = 'LAMBDA'">
47 <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[1]/@binder"/></xsl:with-param></xsl:call-template>
50 <xsl:apply-templates select="*[1]" mode="noannot"/>
54 <xsl:apply-templates select="*[2]" mode="lambda"/>
59 <xsl:apply-templates select="." mode="noannot"/>
66 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/In.con']]" mode="pure">
67 <xsl:variable name="no_params">
68 <xsl:call-template name="get_no_params">
69 <xsl:with-param name="first_uri" select="$CICURI"/>
70 <xsl:with-param name="second_uri" select="CONST/@uri"/>
74 <xsl:when test="(count(child::*) - number($no_params)) = 3">
75 <m:apply helm:xref="{@id}">
76 <m:in definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
77 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
78 <!-- <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/> -->
79 <xsl:apply-templates select="*[2+$no_params]" mode="set" />
90 <!-- NOT ha no parameters -->
91 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Init/Logic/not.con']
92 and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/In.con']]]" mode="pure">
93 <xsl:variable name="no_params">
94 <xsl:call-template name="get_no_params">
95 <xsl:with-param name="first_uri" select="$CICURI"/>
96 <xsl:with-param name="second_uri" select="APPLY/CONST/@uri"/>
100 <xsl:when test="(count(APPLY/child::*) - number($no_params)) = 3">
101 <m:apply helm:xref="{@id}">
103 <xsl:apply-templates select="*[2]/*[3+$no_params]" mode="noannot"/>
104 <!-- <xsl:apply-templates select="*[2]/*[2+$no_params]" mode="noannot"/> -->
105 <xsl:apply-templates select="*[2]/*[2+$no_params]" mode="set"/>
116 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Empty_set.ind']]" mode="pure">
117 <xsl:variable name="no_params">
118 <xsl:call-template name="get_no_params">
119 <xsl:with-param name="first_uri" select="$CICURI"/>
120 <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
124 <xsl:when test="(count(child::*) - number($no_params)) = 1">
125 <m:set definitionURL="{MUTIND/@uri}" helm:xref="{@id}">
128 <xsl:when test="(count(child::*) - number($no_params)) = 2">
129 <m:apply helm:xref="{@id}">
130 <m:in definitionURL="cic:/Coq/Sets/Ensembles/In.con"/>
131 <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
132 <m:set definitionURL="{MUTIND/@uri}" helm:xref="{@id}">
144 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Singleton.ind']]" mode="pure">
145 <xsl:variable name="no_params">
146 <xsl:call-template name="get_no_params">
147 <xsl:with-param name="first_uri" select="$CICURI"/>
148 <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
152 <xsl:when test="(count(child::*) - number($no_params)) = 2">
153 <m:set definitionURL="{MUTIND/@uri}" helm:xref="{@id}">
154 <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
157 <xsl:when test="(count(child::*) - number($no_params)) = 3">
158 <m:apply helm:xref="{@id}">
159 <m:in definitionURL="cic:/Coq/Sets/Ensembles/In.con"/>
160 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
161 <m:set definitionURL="{MUTIND/@uri}">
162 <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
174 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Couple.ind']]" mode="pure">
175 <xsl:variable name="no_params">
176 <xsl:call-template name="get_no_params">
177 <xsl:with-param name="first_uri" select="$CICURI"/>
178 <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
182 <xsl:when test="(count(child::*) - number($no_params)) = 3">
183 <m:set definitionURL="{MUTIND/@uri}" helm:xref="{@id}">
184 <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
185 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
188 <xsl:when test="(count(child::*) - number($no_params)) = 4">
189 <m:apply helm:xref="{@id}">
190 <m:in definitionURL="cic:/Coq/Sets/Ensembles/In.con"/>
191 <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
192 <m:set definitionURL="{MUTIND/@uri}">
193 <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
194 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
206 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Triple.ind'] and (count(child::*) = 5)]" mode="pure">
207 <xsl:variable name="no_params">
208 <xsl:call-template name="get_no_params">
209 <xsl:with-param name="first_uri" select="$CICURI"/>
210 <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
214 <xsl:when test="(count(child::*) - number($no_params)) = 4">
215 <m:set definitionURL="{MUTIND/@uri}" helm:xref="{@id}">
216 <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
217 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
218 <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
221 <xsl:when test="(count(child::*) - number($no_params)) = 5">
222 <m:apply helm:xref="{@id}">
223 <m:in definitionURL="cic:/Coq/Sets/Ensembles/In.con"/>
224 <xsl:apply-templates select="*[5+$no_params]" mode="noannot"/>
225 <m:set definitionURL="{MUTIND/@uri}">
226 <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
227 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
228 <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
238 <!-- INTERSECTION -->
240 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Intersection.ind']]" mode="pure">
241 <xsl:variable name="no_params">
242 <xsl:call-template name="get_no_params">
243 <xsl:with-param name="first_uri" select="$CICURI"/>
244 <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
248 <xsl:when test="(count(child::*) - number($no_params)) = 3">
249 <m:apply helm:xref="{@id}">
250 <m:intersect definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
251 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
252 <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
255 <xsl:when test="(count(child::*) - number($no_params)) = 4">
256 <m:apply helm:xref="{@id}">
258 <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
260 <m:intersect definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
261 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
262 <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
275 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Union.ind']]" mode="pure">
276 <xsl:variable name="no_params">
277 <xsl:call-template name="get_no_params">
278 <xsl:with-param name="first_uri" select="$CICURI"/>
279 <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
283 <xsl:when test="(count(child::*) - number($no_params)) = 3">
284 <m:apply helm:xref="{@id}">
285 <m:union definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
286 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
287 <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
290 <xsl:when test="(count(child::*) - number($no_params)) = 4">
291 <m:apply helm:xref="{@id}">
293 <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
295 <m:union definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
296 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
297 <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
309 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Included.con']]" mode="pure">
310 <xsl:variable name="no_params"> <xsl:call-template name="get_no_params">
311 <xsl:with-param name="first_uri" select="$CICURI"/>
312 <xsl:with-param name="second_uri" select="CONST/@uri"/>
316 <xsl:when test="(count(child::*) - number($no_params)) = 3">
317 <m:apply helm:xref="{@id}">
318 <m:subset definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
319 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
320 <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
329 <!-- STRICTLY INCLUDED -->
331 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Strict_Included.con']]" mode="pure">
332 <xsl:variable name="no_params">
333 <xsl:call-template name="get_no_params">
334 <xsl:with-param name="first_uri" select="$CICURI"/>
335 <xsl:with-param name="second_uri" select="CONST/@uri"/>
339 <xsl:when test="(count(child::*) - number($no_params)) = 3">
340 <m:apply helm:xref="{@id}">
341 <m:prsubset definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
342 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
343 <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
354 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Setminus.con']]" mode="pure">
355 <xsl:variable name="no_params">
356 <xsl:call-template name="get_no_params">
357 <xsl:with-param name="first_uri" select="$CICURI"/>
358 <xsl:with-param name="second_uri" select="CONST/@uri"/>
362 <xsl:when test="(count(child::*) - number($no_params)) = 3">
363 <m:apply helm:xref="{@id}">
364 <m:setdiff definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
365 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
366 <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
369 <xsl:when test="(count(child::*) - number($no_params)) = 4">
370 <m:apply helm:xref="{@id}">
372 <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
374 <m:setdiff definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
375 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
376 <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
388 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Add.con']]" mode="pure">
389 <xsl:variable name="no_params">
390 <xsl:call-template name="get_no_params">
391 <xsl:with-param name="first_uri" select="$CICURI"/>
392 <xsl:with-param name="second_uri" select="CONST/@uri"/>
396 <xsl:when test="(count(child::*) - number($no_params)) = 3">
397 <m:apply helm:xref="{@id}">
398 <m:union definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
399 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
401 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
405 <xsl:when test="(count(child::*) - number($no_params)) = 4">
406 <m:apply helm:xref="{@id}">
408 <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
410 <m:union definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
411 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
413 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
424 <!-- SUBTRACT-ELEM -->
426 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Subtract.con']]" mode="pure">
427 <xsl:variable name="no_params">
428 <xsl:call-template name="get_no_params">
429 <xsl:with-param name="first_uri" select="$CICURI"/>
430 <xsl:with-param name="second_uri" select="CONST/@uri"/>
434 <xsl:when test="(count(child::*) - number($no_params)) = 3">
435 <m:apply helm:xref="{@id}">
436 <m:setdiff definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
437 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
439 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
443 <xsl:when test="(count(child::*) - number($no_params)) = 4">
444 <m:apply helm:xref="{@id}">
446 <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
448 <m:setdiff definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
449 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
451 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
464 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Finite_sets/cardinal.ind']]" mode="pure">
465 <xsl:variable name="no_params">
466 <xsl:call-template name="get_no_params">
467 <xsl:with-param name="first_uri" select="$CICURI"/>
468 <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
472 <xsl:when test="(count(child::*) - number($no_params)) = 3">
473 <m:apply helm:xref="{@id}">
476 <m:card definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
477 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
479 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
488 <!-- ******************* SIGMA TYPES **************************** -->
491 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Init/Specif/sig.ind']]" mode="pure">
493 <xsl:when test="count(child::*) = 3">
495 <xsl:when test="name(*[3]) = 'LAMBDA'">
499 <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[3]/*[1]/@binder"/></xsl:with-param></xsl:call-template>
502 <xsl:apply-templates select="*[3]/*[1]/*[1]" mode="noannot"/>
506 <xsl:apply-templates select="*[3]/*[2]" mode="lambda"/>
515 <xsl:apply-templates select="*[2]" mode="noannot"/>
520 <m:csymbol>app</m:csymbol>
521 <xsl:apply-templates select="*[3]" mode="noannot"/>