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">
37 <!--******************************************************************-->
38 <!-- Variable containing the absolute path of the CIC file -->
39 <!--******************************************************************-->
41 <xsl:variable name="absPath">http://localhost:8081/getciconly?uri=</xsl:variable>
43 <!-- ************************* LOGIC *********************************-->
47 <xsl:template match="*" mode="set">
49 <xsl:when test="name() = 'LAMBDA'">
53 <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="target/@binder"/></xsl:with-param></xsl:call-template>
56 <xsl:apply-templates select="source" mode="noannot"/>
60 <xsl:apply-templates select="target" mode="noannot"/>
65 <xsl:apply-templates select="." mode="noannot"/>
73 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/In.con']]" mode="pure">
74 <xsl:variable name="no_params">
75 <xsl:call-template name="get_no_params">
76 <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
77 <xsl:with-param name="second_uri" select="CONST/@uri"/>
81 <xsl:when test="(count(child::*) - number($no_params)) = 3">
82 <m:apply helm:xref="{@id}">
83 <m:in definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
84 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
85 <!-- <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/> -->
86 <xsl:apply-templates select="*[2+$no_params]" mode="set" />
97 <!-- NOT ha no parameters -->
98 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Init/Logic/not.con']
99 and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/In.con']]]" mode="pure">
100 <xsl:variable name="no_params">
101 <xsl:call-template name="get_no_params">
102 <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
103 <xsl:with-param name="second_uri" select="APPLY/CONST/@uri"/>
107 <xsl:when test="(count(APPLY/child::*) - number($no_params)) = 3">
108 <m:apply helm:xref="{@id}">
110 <xsl:apply-templates select="*[2]/*[3+$no_params]" mode="noannot"/>
111 <!-- <xsl:apply-templates select="*[2]/*[2+$no_params]" mode="noannot"/> -->
112 <xsl:apply-templates select="*[2]/*[2+$no_params]" mode="set"/>
123 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Empty_set.ind']]" mode="pure">
124 <xsl:variable name="no_params">
125 <xsl:call-template name="get_no_params">
126 <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
127 <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
131 <xsl:when test="(count(child::*) - number($no_params)) = 1">
132 <m:set definitionURL="{MUTIND/@uri}" helm:xref="{@id}">
135 <xsl:when test="(count(child::*) - number($no_params)) = 2">
136 <m:apply helm:xref="{@id}">
137 <m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
138 <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
139 <m:set definitionURL="{MUTIND/@uri}" helm:xref="{@id}">
151 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Singleton.ind']]" mode="pure">
152 <xsl:variable name="no_params">
153 <xsl:call-template name="get_no_params">
154 <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
155 <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
159 <xsl:when test="(count(child::*) - number($no_params)) = 2">
160 <m:set definitionURL="{MUTIND/@uri}" helm:xref="{@id}">
161 <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
164 <xsl:when test="(count(child::*) - number($no_params)) = 3">
165 <m:apply helm:xref="{@id}">
166 <m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
167 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
168 <m:set definitionURL="{MUTIND/@uri}">
169 <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
181 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Couple.ind']]" mode="pure">
182 <xsl:variable name="no_params">
183 <xsl:call-template name="get_no_params">
184 <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
185 <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
189 <xsl:when test="(count(child::*) - number($no_params)) = 3">
190 <m:set definitionURL="{MUTIND/@uri}" helm:xref="{@id}">
191 <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
192 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
195 <xsl:when test="(count(child::*) - number($no_params)) = 4">
196 <m:apply helm:xref="{@id}">
197 <m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
198 <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
199 <m:set definitionURL="{MUTIND/@uri}">
200 <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
201 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
213 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Triple.ind'] and (count(child::*) = 5)]" mode="pure">
214 <xsl:variable name="no_params">
215 <xsl:call-template name="get_no_params">
216 <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
217 <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
221 <xsl:when test="(count(child::*) - number($no_params)) = 4">
222 <m:set definitionURL="{MUTIND/@uri}" helm:xref="{@id}">
223 <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
224 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
225 <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
228 <xsl:when test="(count(child::*) - number($no_params)) = 5">
229 <m:apply helm:xref="{@id}">
230 <m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
231 <xsl:apply-templates select="*[5+$no_params]" mode="noannot"/>
232 <m:set definitionURL="{MUTIND/@uri}">
233 <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
234 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
235 <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
245 <!-- INTERSECTION -->
247 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Intersection.ind']]" mode="pure">
248 <xsl:variable name="no_params">
249 <xsl:call-template name="get_no_params">
250 <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
251 <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
255 <xsl:when test="(count(child::*) - number($no_params)) = 3">
256 <m:apply helm:xref="{@id}">
257 <m:intersect definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
258 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
259 <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
262 <xsl:when test="(count(child::*) - number($no_params)) = 4">
263 <m:apply helm:xref="{@id}">
265 <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
267 <m:intersect definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
268 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
269 <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
282 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Union.ind']]" mode="pure">
283 <xsl:variable name="no_params">
284 <xsl:call-template name="get_no_params">
285 <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
286 <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
290 <xsl:when test="(count(child::*) - number($no_params)) = 3">
291 <m:apply helm:xref="{@id}">
292 <m:union definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
293 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
294 <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
297 <xsl:when test="(count(child::*) - number($no_params)) = 4">
298 <m:apply helm:xref="{@id}">
300 <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
302 <m:union definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
303 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
304 <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
316 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Included.con']]" mode="pure">
317 <xsl:variable name="no_params">
318 <xsl:call-template name="get_no_params">
319 <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
320 <xsl:with-param name="second_uri" select="CONST/@uri"/>
324 <xsl:when test="(count(child::*) - number($no_params)) = 3">
325 <m:apply helm:xref="{@id}">
326 <m:subset definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
327 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
328 <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
337 <!-- STRICTLY INCLUDED -->
339 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Strict_Included.con']]" mode="pure">
340 <xsl:variable name="no_params">
341 <xsl:call-template name="get_no_params">
342 <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
343 <xsl:with-param name="second_uri" select="CONST/@uri"/>
347 <xsl:when test="(count(child::*) - number($no_params)) = 3">
348 <m:apply helm:xref="{@id}">
349 <m:prsubset definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
350 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
351 <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
362 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Setminus.con']]" mode="pure">
363 <xsl:variable name="no_params">
364 <xsl:call-template name="get_no_params">
365 <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
366 <xsl:with-param name="second_uri" select="CONST/@uri"/>
370 <xsl:when test="(count(child::*) - number($no_params)) = 3">
371 <m:apply helm:xref="{@id}">
372 <m:setdiff definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
373 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
374 <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
377 <xsl:when test="(count(child::*) - number($no_params)) = 4">
378 <m:apply helm:xref="{@id}">
380 <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
382 <m:setdiff definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
383 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
384 <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
396 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Add.con']]" mode="pure">
397 <xsl:variable name="no_params">
398 <xsl:call-template name="get_no_params">
399 <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
400 <xsl:with-param name="second_uri" select="CONST/@uri"/>
404 <xsl:when test="(count(child::*) - number($no_params)) = 3">
405 <m:apply helm:xref="{@id}">
406 <m:union definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
407 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
409 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
413 <xsl:when test="(count(child::*) - number($no_params)) = 4">
414 <m:apply helm:xref="{@id}">
416 <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
418 <m:union definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
419 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
421 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
432 <!-- SUBTRACT-ELEM -->
434 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Subtract.con']]" mode="pure">
435 <xsl:variable name="no_params">
436 <xsl:call-template name="get_no_params">
437 <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
438 <xsl:with-param name="second_uri" select="CONST/@uri"/>
442 <xsl:when test="(count(child::*) - number($no_params)) = 3">
443 <m:apply helm:xref="{@id}">
444 <m:setdiff definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
445 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
447 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
451 <xsl:when test="(count(child::*) - number($no_params)) = 4">
452 <m:apply helm:xref="{@id}">
454 <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
456 <m:setdiff definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
457 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
459 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
472 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Finite_sets/Ensembles_finis/cardinal.ind']]" mode="pure">
473 <xsl:variable name="no_params">
474 <xsl:call-template name="get_no_params">
475 <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
476 <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
480 <xsl:when test="(count(child::*) - number($no_params)) = 3">
481 <m:apply helm:xref="{@id}">
484 <m:card definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
485 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
487 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>