3 <!--******************************************************************-->
4 <!-- Basic Set Theory -->
5 <!-- First draft: April 3 2000 -->
6 <!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena -->
7 <!--******************************************************************-->
9 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
10 xmlns:m="http://www.w3.org/1998/Math/MathML"
11 xmlns:helm="http://www.cs.unibo.it/helm">
13 <!--******************************************************************-->
14 <!-- Variable containing the absolute path of the CIC file -->
15 <!--******************************************************************-->
17 <xsl:variable name="absPath">http://localhost:8081/getciconly?uri=</xsl:variable>
19 <!-- ************************* LOGIC *********************************-->
23 <xsl:template match="*" mode="set">
25 <xsl:when test="name() = 'LAMBDA'">
29 <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="target/@binder"/></xsl:with-param></xsl:call-template>
32 <xsl:apply-templates select="source" mode="noannot"/>
36 <xsl:apply-templates select="target" mode="noannot"/>
41 <xsl:apply-templates select="." mode="noannot"/>
49 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/In.con']]" mode="pure">
50 <xsl:variable name="no_params">
51 <xsl:call-template name="get_no_params">
52 <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
53 <xsl:with-param name="second_uri" select="CONST/@uri"/>
57 <xsl:when test="(count(child::*) - number($no_params)) = 3">
58 <m:apply helm:xref="{@id}">
59 <m:in definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
60 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
61 <!-- <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/> -->
62 <xsl:apply-templates select="*[2+$no_params]" mode="set" />
73 <!-- NOT ha no parameters -->
74 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Init/Logic/not.con']
75 and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/In.con']]]" mode="pure">
76 <xsl:variable name="no_params">
77 <xsl:call-template name="get_no_params">
78 <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
79 <xsl:with-param name="second_uri" select="APPLY/CONST/@uri"/>
83 <xsl:when test="(count(APPLY/child::*) - number($no_params)) = 3">
84 <m:apply helm:xref="{@id}">
86 <xsl:apply-templates select="*[2]/*[3+$no_params]" mode="noannot"/>
87 <!-- <xsl:apply-templates select="*[2]/*[2+$no_params]" mode="noannot"/> -->
88 <xsl:apply-templates select="*[2]/*[2+$no_params]" mode="set"/>
99 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Empty_set.ind']]" 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="MUTIND/@uri"/>
107 <xsl:when test="(count(child::*) - number($no_params)) = 1">
108 <m:set definitionURL="{MUTIND/@uri}" helm:xref="{@id}">
111 <xsl:when test="(count(child::*) - number($no_params)) = 2">
112 <m:apply helm:xref="{@id}">
113 <m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
114 <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
115 <m:set definitionURL="{MUTIND/@uri}" helm:xref="{@id}">
127 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Singleton.ind']]" mode="pure">
128 <xsl:variable name="no_params">
129 <xsl:call-template name="get_no_params">
130 <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
131 <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
135 <xsl:when test="(count(child::*) - number($no_params)) = 2">
136 <m:set definitionURL="{MUTIND/@uri}" helm:xref="{@id}">
137 <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
140 <xsl:when test="(count(child::*) - number($no_params)) = 3">
141 <m:apply helm:xref="{@id}">
142 <m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
143 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
144 <m:set definitionURL="{MUTIND/@uri}">
145 <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
157 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Couple.ind']]" mode="pure">
158 <xsl:variable name="no_params">
159 <xsl:call-template name="get_no_params">
160 <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
161 <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
165 <xsl:when test="(count(child::*) - number($no_params)) = 3">
166 <m:set definitionURL="{MUTIND/@uri}" helm:xref="{@id}">
167 <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
168 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
171 <xsl:when test="(count(child::*) - number($no_params)) = 4">
172 <m:apply helm:xref="{@id}">
173 <m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
174 <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
175 <m:set definitionURL="{MUTIND/@uri}">
176 <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
177 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
189 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Triple.ind'] and (count(child::*) = 5)]" mode="pure">
190 <xsl:variable name="no_params">
191 <xsl:call-template name="get_no_params">
192 <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
193 <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
197 <xsl:when test="(count(child::*) - number($no_params)) = 4">
198 <m:set definitionURL="{MUTIND/@uri}" helm:xref="{@id}">
199 <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
200 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
201 <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
204 <xsl:when test="(count(child::*) - number($no_params)) = 5">
205 <m:apply helm:xref="{@id}">
206 <m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
207 <xsl:apply-templates select="*[5+$no_params]" mode="noannot"/>
208 <m:set definitionURL="{MUTIND/@uri}">
209 <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
210 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
211 <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
221 <!-- INTERSECTION -->
223 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Intersection.ind']]" mode="pure">
224 <xsl:variable name="no_params">
225 <xsl:call-template name="get_no_params">
226 <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
227 <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
231 <xsl:when test="(count(child::*) - number($no_params)) = 3">
232 <m:apply helm:xref="{@id}">
233 <m:intersect definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
234 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
235 <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
238 <xsl:when test="(count(child::*) - number($no_params)) = 4">
239 <m:apply helm:xref="{@id}">
241 <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
243 <m:intersect definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
244 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
245 <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
258 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Union.ind']]" mode="pure">
259 <xsl:variable name="no_params">
260 <xsl:call-template name="get_no_params">
261 <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
262 <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
266 <xsl:when test="(count(child::*) - number($no_params)) = 3">
267 <m:apply helm:xref="{@id}">
268 <m:union definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
269 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
270 <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
273 <xsl:when test="(count(child::*) - number($no_params)) = 4">
274 <m:apply helm:xref="{@id}">
276 <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
278 <m:union definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
279 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
280 <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
292 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Included.con']]" mode="pure">
293 <xsl:variable name="no_params">
294 <xsl:call-template name="get_no_params">
295 <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
296 <xsl:with-param name="second_uri" select="CONST/@uri"/>
300 <xsl:when test="(count(child::*) - number($no_params)) = 3">
301 <m:apply helm:xref="{@id}">
302 <m:subset definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
303 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
304 <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
313 <!-- STRICTLY INCLUDED -->
315 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Strict_Included.con']]" mode="pure">
316 <xsl:variable name="no_params">
317 <xsl:call-template name="get_no_params">
318 <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
319 <xsl:with-param name="second_uri" select="CONST/@uri"/>
323 <xsl:when test="(count(child::*) - number($no_params)) = 3">
324 <m:apply helm:xref="{@id}">
325 <m:prsubset definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
326 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
327 <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
338 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Setminus.con']]" mode="pure">
339 <xsl:variable name="no_params">
340 <xsl:call-template name="get_no_params">
341 <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
342 <xsl:with-param name="second_uri" select="CONST/@uri"/>
346 <xsl:when test="(count(child::*) - number($no_params)) = 3">
347 <m:apply helm:xref="{@id}">
348 <m:setdiff definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
349 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
350 <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
353 <xsl:when test="(count(child::*) - number($no_params)) = 4">
354 <m:apply helm:xref="{@id}">
356 <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
358 <m:setdiff definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
359 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
360 <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
372 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Add.con']]" mode="pure">
373 <xsl:variable name="no_params">
374 <xsl:call-template name="get_no_params">
375 <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
376 <xsl:with-param name="second_uri" select="CONST/@uri"/>
380 <xsl:when test="(count(child::*) - number($no_params)) = 3">
381 <m:apply helm:xref="{@id}">
382 <m:union definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
383 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
385 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
389 <xsl:when test="(count(child::*) - number($no_params)) = 4">
390 <m:apply helm:xref="{@id}">
392 <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
394 <m:union definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
395 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
397 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
408 <!-- SUBTRACT-ELEM -->
410 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Subtract.con']]" mode="pure">
411 <xsl:variable name="no_params">
412 <xsl:call-template name="get_no_params">
413 <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
414 <xsl:with-param name="second_uri" select="CONST/@uri"/>
418 <xsl:when test="(count(child::*) - number($no_params)) = 3">
419 <m:apply helm:xref="{@id}">
420 <m:setdiff definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
421 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
423 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
427 <xsl:when test="(count(child::*) - number($no_params)) = 4">
428 <m:apply helm:xref="{@id}">
430 <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
432 <m:setdiff definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
433 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
435 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
448 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Finite_sets/Ensembles_finis/cardinal.ind']]" mode="pure">
449 <xsl:variable name="no_params">
450 <xsl:call-template name="get_no_params">
451 <xsl:with-param name="first_uri" select="/cicxml/@uri"/>
452 <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
456 <xsl:when test="(count(child::*) - number($no_params)) = 3">
457 <m:apply helm:xref="{@id}">
460 <m:card definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
461 <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
463 <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>