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 *********************************-->
42 <xsl:template match="*" mode="set">
44 <xsl:when test="name() = 'LAMBDA'">
48 <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="target/@binder"/></xsl:with-param></xsl:call-template>
51 <xsl:apply-templates select="source" mode="noannot"/>
55 <xsl:apply-templates select="target" mode="noannot"/>
60 <xsl:apply-templates select="." mode="noannot"/>
68 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/In.con']]" mode="pure">
69 <xsl:variable name="no_params">
70 <xsl:call-template name="get_no_params">
71 <xsl:with-param name="first_uri" select="$CICURI"/>
72 <xsl:with-param name="second_uri" select="CONST/@uri"/>
76 <xsl:when test="(count(child::*) - number($no_params)) = 3">
77 <m:apply helm:xref="{@id}">
78 <m:in definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
79 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
80 <!-- <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/> -->
81 <xsl:apply-templates select="*[2+$no_params]" mode="set" />
92 <!-- NOT ha no parameters -->
93 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Init/Logic/not.con']
94 and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/In.con']]]" mode="pure">
95 <xsl:variable name="no_params">
96 <xsl:call-template name="get_no_params">
97 <xsl:with-param name="first_uri" select="$CICURI"/>
98 <xsl:with-param name="second_uri" select="APPLY/CONST/@uri"/>
102 <xsl:when test="(count(APPLY/child::*) - number($no_params)) = 3">
103 <m:apply helm:xref="{@id}">
105 <xsl:apply-templates select="*[2]/*[3+$no_params]" mode="noannot"/>
106 <!-- <xsl:apply-templates select="*[2]/*[2+$no_params]" mode="noannot"/> -->
107 <xsl:apply-templates select="*[2]/*[2+$no_params]" mode="set"/>
118 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Empty_set.ind']]" mode="pure">
119 <xsl:variable name="no_params">
120 <xsl:call-template name="get_no_params">
121 <xsl:with-param name="first_uri" select="$CICURI"/>
122 <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
126 <xsl:when test="(count(child::*) - number($no_params)) = 1">
127 <m:set definitionURL="{MUTIND/@uri}" helm:xref="{@id}">
130 <xsl:when test="(count(child::*) - number($no_params)) = 2">
131 <m:apply helm:xref="{@id}">
132 <m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
133 <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
134 <m:set definitionURL="{MUTIND/@uri}" helm:xref="{@id}">
146 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Singleton.ind']]" mode="pure">
147 <xsl:variable name="no_params">
148 <xsl:call-template name="get_no_params">
149 <xsl:with-param name="first_uri" select="$CICURI"/>
150 <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
154 <xsl:when test="(count(child::*) - number($no_params)) = 2">
155 <m:set definitionURL="{MUTIND/@uri}" helm:xref="{@id}">
156 <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
159 <xsl:when test="(count(child::*) - number($no_params)) = 3">
160 <m:apply helm:xref="{@id}">
161 <m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
162 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
163 <m:set definitionURL="{MUTIND/@uri}">
164 <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
176 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Couple.ind']]" mode="pure">
177 <xsl:variable name="no_params">
178 <xsl:call-template name="get_no_params">
179 <xsl:with-param name="first_uri" select="$CICURI"/>
180 <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
184 <xsl:when test="(count(child::*) - number($no_params)) = 3">
185 <m:set definitionURL="{MUTIND/@uri}" helm:xref="{@id}">
186 <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
187 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
190 <xsl:when test="(count(child::*) - number($no_params)) = 4">
191 <m:apply helm:xref="{@id}">
192 <m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
193 <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
194 <m:set definitionURL="{MUTIND/@uri}">
195 <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
196 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
208 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Triple.ind'] and (count(child::*) = 5)]" mode="pure">
209 <xsl:variable name="no_params">
210 <xsl:call-template name="get_no_params">
211 <xsl:with-param name="first_uri" select="$CICURI"/>
212 <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
216 <xsl:when test="(count(child::*) - number($no_params)) = 4">
217 <m:set definitionURL="{MUTIND/@uri}" helm:xref="{@id}">
218 <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
219 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
220 <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
223 <xsl:when test="(count(child::*) - number($no_params)) = 5">
224 <m:apply helm:xref="{@id}">
225 <m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
226 <xsl:apply-templates select="*[5+$no_params]" mode="noannot"/>
227 <m:set definitionURL="{MUTIND/@uri}">
228 <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
229 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
230 <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
240 <!-- INTERSECTION -->
242 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Intersection.ind']]" mode="pure">
243 <xsl:variable name="no_params">
244 <xsl:call-template name="get_no_params">
245 <xsl:with-param name="first_uri" select="$CICURI"/>
246 <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
250 <xsl:when test="(count(child::*) - number($no_params)) = 3">
251 <m:apply helm:xref="{@id}">
252 <m:intersect definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
253 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
254 <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
257 <xsl:when test="(count(child::*) - number($no_params)) = 4">
258 <m:apply helm:xref="{@id}">
260 <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
262 <m:intersect definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
263 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
264 <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
277 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Union.ind']]" mode="pure">
278 <xsl:variable name="no_params">
279 <xsl:call-template name="get_no_params">
280 <xsl:with-param name="first_uri" select="$CICURI"/>
281 <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
285 <xsl:when test="(count(child::*) - number($no_params)) = 3">
286 <m:apply helm:xref="{@id}">
287 <m:union definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
288 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
289 <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
292 <xsl:when test="(count(child::*) - number($no_params)) = 4">
293 <m:apply helm:xref="{@id}">
295 <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
297 <m:union definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
298 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
299 <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
311 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Included.con']]" mode="pure">
312 <xsl:variable name="no_params">
313 <xsl:call-template name="get_no_params">
314 <xsl:with-param name="first_uri" select="$CICURI"/>
315 <xsl:with-param name="second_uri" select="CONST/@uri"/>
319 <xsl:when test="(count(child::*) - number($no_params)) = 3">
320 <m:apply helm:xref="{@id}">
321 <m:subset definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
322 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
323 <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
332 <!-- STRICTLY INCLUDED -->
334 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Strict_Included.con']]" mode="pure">
335 <xsl:variable name="no_params">
336 <xsl:call-template name="get_no_params">
337 <xsl:with-param name="first_uri" select="$CICURI"/>
338 <xsl:with-param name="second_uri" select="CONST/@uri"/>
342 <xsl:when test="(count(child::*) - number($no_params)) = 3">
343 <m:apply helm:xref="{@id}">
344 <m:prsubset definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
345 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
346 <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
357 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Setminus.con']]" mode="pure">
358 <xsl:variable name="no_params">
359 <xsl:call-template name="get_no_params">
360 <xsl:with-param name="first_uri" select="$CICURI"/>
361 <xsl:with-param name="second_uri" select="CONST/@uri"/>
365 <xsl:when test="(count(child::*) - number($no_params)) = 3">
366 <m:apply helm:xref="{@id}">
367 <m:setdiff definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
368 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
369 <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
372 <xsl:when test="(count(child::*) - number($no_params)) = 4">
373 <m:apply helm:xref="{@id}">
375 <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
377 <m:setdiff definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
378 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
379 <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
391 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Add.con']]" mode="pure">
392 <xsl:variable name="no_params">
393 <xsl:call-template name="get_no_params">
394 <xsl:with-param name="first_uri" select="$CICURI"/>
395 <xsl:with-param name="second_uri" select="CONST/@uri"/>
399 <xsl:when test="(count(child::*) - number($no_params)) = 3">
400 <m:apply helm:xref="{@id}">
401 <m:union definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
402 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
404 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
408 <xsl:when test="(count(child::*) - number($no_params)) = 4">
409 <m:apply helm:xref="{@id}">
411 <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
413 <m:union definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
414 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
416 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
427 <!-- SUBTRACT-ELEM -->
429 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Subtract.con']]" mode="pure">
430 <xsl:variable name="no_params">
431 <xsl:call-template name="get_no_params">
432 <xsl:with-param name="first_uri" select="$CICURI"/>
433 <xsl:with-param name="second_uri" select="CONST/@uri"/>
437 <xsl:when test="(count(child::*) - number($no_params)) = 3">
438 <m:apply helm:xref="{@id}">
439 <m:setdiff definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
440 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
442 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
446 <xsl:when test="(count(child::*) - number($no_params)) = 4">
447 <m:apply helm:xref="{@id}">
449 <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
451 <m:setdiff definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
452 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
454 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
467 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Finite_sets/Ensembles_finis/cardinal.ind']]" mode="pure">
468 <xsl:variable name="no_params">
469 <xsl:call-template name="get_no_params">
470 <xsl:with-param name="first_uri" select="$CICURI"/>
471 <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
475 <xsl:when test="(count(child::*) - number($no_params)) = 3">
476 <m:apply helm:xref="{@id}">
479 <m:card definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
480 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
482 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
491 <!-- ******************* SIGMA TYPES **************************** -->
493 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Init/Specif/Subsets/sig.ind']]" mode="pure">
495 <xsl:when test="count(child::*) = 3">
497 <xsl:when test="name(*[3]) = 'LAMBDA'">
501 <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[3]/target/@binder"/></xsl:with-param></xsl:call-template>
504 <xsl:apply-templates select="*[3]/source/*[1]" mode="noannot"/>
508 <xsl:apply-templates select="*[3]/target/*[1]" mode="noannot"/>
517 <xsl:apply-templates select="*[2]" mode="noannot"/>
522 <m:csymbol>app</m:csymbol>
523 <xsl:apply-templates select="*[3]" mode="noannot"/>