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 <!--******************************************************************-->
29 <!-- (completely) Revisited: february 2001, Andrea Asperti -->
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 <!-- ************************* LOGIC *********************************-->
39 <!-- Proof objects -->
41 <!-- <xsl:key name="typeid" use="@of" match="TYPE"/> -->
42 <xsl:key name="typeid" use="@of" match="TYPE"/>
44 <!-- These elements do not have inner type -->
45 <xsl:template match="PROD|SORT|MUTIND|instantiate" mode="noannot">
46 <xsl:apply-templates select="." mode="pure"/>
49 <!-- Atomic elements that have an inner type iff the expected type -->
50 <!-- is different from the synthesized type. -->
51 <xsl:template match="REL|VAR|META|CONST|MUTCONSTRUCT" mode="noannot">
52 <xsl:variable name="id" select="@id"/>
53 <xsl:variable name="innertype_available">
54 <xsl:for-each select="$InnerTypes">
55 <xsl:if test="key('typeid',$id)/*">
56 <xsl:text>yes</xsl:text>
61 <xsl:when test="$naturalLanguage='yes' and @sort='Prop' and $innertype_available='yes'">
62 <!--xsl:when test="@sort='Prop'"-->
63 <m:apply helm:xref="{@id}">
64 <m:csymbol>proof</m:csymbol>
65 <xsl:apply-templates mode="proof_transform" select="."/>
66 <xsl:for-each select="$InnerTypes">
67 <xsl:apply-templates mode="pure" select="key('typeid',$id)/*"/>
72 <xsl:apply-templates select="." mode="pure"/>
77 <!-- ALL ELEMENTS WITH A TYPE ARE TRANSLATED AS A PROOF-ELEMENT -->
79 <!-- LAMBDA has inner type only if it is not nested inside another lambda -->
80 <xsl:template match="LAMBDA" mode="noannot">
81 <xsl:variable name="id" select="decl/@id"/>
82 <xsl:variable name="innertype_available">
83 <xsl:for-each select="$InnerTypes">
84 <xsl:if test="key('typeid',$id)/*">
85 <xsl:text>yes</xsl:text>
89 <!--xsl:value-of select="concat('NL: ',$naturalLanguage,' IA: ',$innertype_available)"/-->
91 <xsl:when test="$naturalLanguage='yes' and @sort='Prop' and $innertype_available='yes'">
92 <m:apply helm:xref="{decl/@id}">
93 <m:csymbol>proof</m:csymbol>
94 <xsl:apply-templates mode="proof_transform" select="."/>
95 <xsl:for-each select="$InnerTypes">
96 <xsl:apply-templates mode="pure" select="key('typeid',$id)/*"/>
101 <xsl:apply-templates select="." mode="pure"/>
106 <!-- ALL these elements have inner type -->
107 <xsl:template match="LETIN|CAST|APPLY|MUTCASE|FIX|COFIX" mode="noannot">
108 <xsl:variable name="id" select="@id"/>
110 <xsl:when test="$naturalLanguage='yes' and @sort='Prop'">
111 <m:apply helm:xref="{@id}">
112 <m:csymbol>proof</m:csymbol>
113 <xsl:apply-templates mode="proof_transform" select="."/>
114 <xsl:for-each select="$InnerTypes">
115 <xsl:apply-templates mode="pure" select="key('typeid',$id)/*"/>
121 <xsl:when test="name()='APPLY'">
122 <!-- This is the case of an applicative expression wich is not
123 a proof but could contains proofs...
124 MODE LETIN OR MODE PURE ??? Big question -->
125 <xsl:apply-templates select="." mode="pure"/>
128 <xsl:apply-templates select="." mode="pure"/>
135 <!-- si presuppone che il tipo induttivo non sia mutuamente
136 induttivo. Bisognerebbe andare a vedere l'ultimo parametro
137 del presunto "principio di induzione", tirare fuori il tipo induttivo
138 e vedere se il suo nome coincide con il prefisso di _ind.
139 Ad esempio nat_double_ind e' definito dall'utente. L'ultimo
140 parametro di nat_double_ind e' di tipo nat, e nat e' diverso
141 da nat_double. Per ora, verifico solo l'esistenza di nat_double,
142 ma questo, benche' non porti ad errore, non copre tutti i
143 casi per quelli mutuamente induttivi -->
145 <xsl:template mode="try_inductive" match="APPLY">
146 <xsl:variable name="id" select="@id"/>
148 <xsl:when test="CONST[1]">
149 <xsl:variable name="uri" select="CONST[1]/@uri"/>
151 <xsl:when test="contains($uri,'_ind.con')">
152 <xsl:variable name="ind_uri"
153 select="concat(substring-before($uri,'_ind.con'),'.ind')"/>
154 <xsl:variable name="InductiveTypeUrl"><xsl:call-template name="URLofURI4getter"><xsl:with-param name="uri" select="$ind_uri"/></xsl:call-template></xsl:variable>
155 <xsl:variable name="inductive_def"
156 select="document($InductiveTypeUrl)/InductiveDefinition"/>
157 <!-- check if the corresponding inductive definition actually
160 <xsl:when test="$inductive_def">
161 <xsl:variable name="ind_name">
162 <xsl:call-template name="get_name">
163 <xsl:with-param name="uri" select="$uri"/>
166 <xsl:variable name="no_params">
167 <xsl:call-template name="get_no_params">
168 <xsl:with-param name="first_uri" select="$CICURI"/>
169 <xsl:with-param name="second_uri" select="$uri"/>
172 <xsl:apply-templates mode="inductive" select=".">
173 <xsl:with-param name="inductive_def_uri"
175 <xsl:with-param name="inductive_def"
176 select="$inductive_def"/>
177 <xsl:with-param name="section_params" select="$no_params"/>
178 <xsl:with-param name="inductive_def_index" select="1"/>
179 <xsl:with-param name="inductive_def_name" select="$ind_name"/>
180 </xsl:apply-templates>
183 <xsl:apply-templates mode="letin" select="."/>
188 <xsl:apply-templates mode="letin" select="."/>
193 <xsl:apply-templates mode="letin" select="."/>
198 <xsl:template mode="eq_transitive" match="*">
199 <!-- <m:ci>eccomi-1: <xsl:value-of select="name()"/></m:ci> -->
201 <xsl:when test="name()='APPLY'">
202 <!-- <m:ci>eccomi-2: <xsl:value-of select="CONST[1]/@uri"/></m:ci> -->
203 <xsl:variable name="id" select="@id"/>
205 <!-- ricordarsi di trattare il parametro -->
206 <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/CSetoids/eq_transitive_unfolded.con'] and count(child::*) = 7">
207 <!-- <m:ci>eccomi-3</m:ci> -->
208 <xsl:apply-templates mode="eq_transitive" select="*[6]"/>
209 <xsl:apply-templates mode="noannot" select="*[4]"/>
210 <xsl:apply-templates mode="eq_transitive" select="*[7]"/>
213 <xsl:call-template name="generate_side_proof">
214 <xsl:with-param name="proof" select="."/>
215 <xsl:with-param name="show_statement" select="0"/>
221 <xsl:call-template name="generate_side_proof">
222 <xsl:with-param name="proof" select="."/>
223 <xsl:with-param name="show_statement" select="0"/>
229 <xsl:template mode="diseq" match="*">
230 <xsl:param name="rel" select="'eq'"/>
232 <xsl:when test="name()='APPLY'">
233 <xsl:variable name="id" select="@id"/>
235 <!-- ricordarsi di trattare il parametro -->
236 <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/leEq_transitive.con'] and count(child::*) = 7">
237 <xsl:apply-templates mode="diseq" select="*[6]">
238 <xsl:with-param name="rel" select="'leq'"/>
239 </xsl:apply-templates>
240 <xsl:apply-templates mode="noannot" select="*[4]"/>
241 <xsl:apply-templates mode="diseq" select="*[7]">
242 <xsl:with-param name="rel" select="'leq'"/>
243 </xsl:apply-templates>
245 <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/leEq_wdl.con'] and count(child::*) = 7">
247 <!-- <m:ci><xsl:value-of select="'eq'"/></m:ci> -->
248 <xsl:call-template name="generate_side_proof">
249 <xsl:with-param name="proof" select="*[7]"/>
250 <xsl:with-param name="show_statement" select="0"/>
252 <xsl:apply-templates mode="noannot" select="*[3]"/>
253 <xsl:apply-templates mode="diseq" select="*[6]">
254 <xsl:with-param name="rel" select="'leq'"/>
255 </xsl:apply-templates>
257 <xsl:when test="CONST[attribute::uri='cic:/Algebra/algerba/COrdFields/leEq_less_trans.con'] and count(child::*) = 7">
258 <xsl:apply-templates mode="diseq" select="*[6]">
259 <xsl:with-param name="rel" select="'leq'"/>
260 </xsl:apply-templates>
261 <xsl:apply-templates mode="noannot" select="*[4]"/>
262 <xsl:apply-templates mode="diseq" select="*[7]">
263 <xsl:with-param name="rel" select="'lt'"/>
264 </xsl:apply-templates>
266 <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/less_leEq_trans.con'] and count(child::*) = 7">
267 <xsl:apply-templates mode="diseq" select="*[6]">
268 <xsl:with-param name="rel" select="'lt'"/>
269 </xsl:apply-templates>
270 <xsl:apply-templates mode="noannot" select="*[4]"/>
271 <xsl:apply-templates mode="diseq" select="*[7]">
272 <xsl:with-param name="rel" select="'leq'"/>
273 </xsl:apply-templates>
275 <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/leEq_wdr.con'] and count(child::*) = 7">
276 <xsl:apply-templates mode="diseq" select="*[6]">
277 <xsl:with-param name="rel" select="'leq'"/>
278 </xsl:apply-templates>
279 <xsl:apply-templates mode="noannot" select="*[4]"/>
280 <xsl:apply-templates mode="diseq" select="*[7]">
281 <xsl:with-param name="rel" select="'eq'"/>
282 </xsl:apply-templates>
284 <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/less_transitive_unfolded.con'] and count(child::*) = 7">
285 <xsl:apply-templates mode="diseq" select="*[6]">
286 <xsl:with-param name="rel" select="'lt'"/>
287 </xsl:apply-templates>
288 <xsl:apply-templates mode="noannot" select="*[4]"/>
289 <xsl:apply-templates mode="diseq" select="*[7]">
290 <xsl:with-param name="rel" select="'lt'"/>
291 </xsl:apply-templates>
293 <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/less_wdr.con'] and count(child::*) = 7">
294 <xsl:apply-templates mode="diseq" select="*[6]">
295 <xsl:with-param name="rel" select="'lt'"/>
296 </xsl:apply-templates>
297 <xsl:apply-templates mode="noannot" select="*[4]"/>
298 <xsl:apply-templates mode="diseq" select="*[7]">
299 <xsl:with-param name="rel" select="'eq'"/>
300 </xsl:apply-templates>
302 <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/less_wdl.con'] and count(child::*) = 7">
304 <!-- <m:ci><xsl:value-of select="'eq'"/></m:ci> -->
305 <xsl:call-template name="generate_side_proof">
306 <xsl:with-param name="proof" select="*[7]"/>
307 <xsl:with-param name="show_statement" select="0"/>
309 <xsl:apply-templates mode="noannot" select="*[3]"/>
310 <xsl:apply-templates mode="diseq" select="*[6]">
311 <xsl:with-param name="rel" select="'lt'"/>
312 </xsl:apply-templates>
315 <xsl:when test="CONST[attribute::uri='cic:/Algebra/CSetoids/CSetoid_basics/eq_transitive_unfolded.con'] and count(child::*) = 7">
316 <xsl:apply-templates mode="diseq" select="*[6]"/>
318 <xsl:apply-templates mode="noannot" select="*[4]"/>
320 <xsl:apply-templates mode="diseq" select="*[7]"/>
324 <xsl:element name="{concat('m:',$rel)}"/>
325 <!-- <m:ci><xsl:value-of select="$rel"/></m:ci> -->
326 <xsl:call-template name="generate_side_proof">
327 <xsl:with-param name="proof" select="."/>
328 <xsl:with-param name="show_statement" select="0"/>
334 <xsl:element name="{concat('m:',$rel)}"/>
335 <!-- <m:ci><xsl:value-of select="$rel"/></m:ci> -->
336 <xsl:call-template name="generate_side_proof">
337 <xsl:with-param name="proof" select="."/>
338 <xsl:with-param name="show_statement" select="0"/>
344 <xsl:template mode="proof_transform" match="*">
346 <xsl:when test="name()='APPLY'">
347 <xsl:variable name="id" select="@id"/>
349 <!-- Algebra equality (eq_transitive_unfolded) -->
350 <!-- It requires a special mode "eq_transitive"-->
351 <!-- togliere il parametro -->
352 <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/CSetoids/eq_transitive_unfolded.con'] and count(child::*) = 7">
354 <m:csymbol>eq_chain</m:csymbol>
355 <xsl:apply-templates mode="noannot" select="*[3]"/>
356 <xsl:apply-templates mode="eq_transitive" select="*[6]"/>
357 <xsl:apply-templates mode="noannot" select="*[4]"/>
358 <xsl:apply-templates mode="eq_transitive" select="*[7]"/>
359 <xsl:apply-templates mode="noannot" select="*[5]"/>
362 <!-- Algebra disequalities -->
363 <!-- It requires a special mode "diseq"-->
364 <!-- togliere il parametro -->
365 <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/leEq_transitive.con'] and count(child::*) = 7">
367 <m:csymbol>diseq_chain</m:csymbol>
368 <xsl:apply-templates mode="noannot" select="*[3]"/>
369 <xsl:apply-templates mode="diseq" select="*[6]">
370 <xsl:with-param name="rel" select="'leq'"/>
371 </xsl:apply-templates>
372 <xsl:apply-templates mode="noannot" select="*[4]"/>
373 <xsl:apply-templates mode="diseq" select="*[7]">
374 <xsl:with-param name="rel" select="'leq'"/>
375 </xsl:apply-templates>
376 <xsl:apply-templates mode="noannot" select="*[5]"/>
379 <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/leEq_wdl.con'] and count(child::*) = 7">
381 <m:csymbol>diseq_chain</m:csymbol>
382 <xsl:apply-templates mode="noannot" select="*[5]"/>
384 <!-- <m:ci><xsl:value-of select="'eq'"/></m:ci> -->
385 <xsl:call-template name="generate_side_proof">
386 <xsl:with-param name="proof" select="*[7]"/>
387 <xsl:with-param name="show_statement" select="0"/>
389 <xsl:apply-templates mode="noannot" select="*[3]"/>
390 <xsl:apply-templates mode="diseq" select="*[6]">
391 <xsl:with-param name="rel" select="'leq'"/>
392 </xsl:apply-templates>
393 <xsl:apply-templates mode="noannot" select="*[4]"/>
396 <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/leEq_less_trans.con'] and count(child::*) = 7">
398 <m:csymbol>diseq_chain</m:csymbol>
399 <xsl:apply-templates mode="noannot" select="*[3]"/>
400 <xsl:apply-templates mode="diseq" select="*[6]">
401 <xsl:with-param name="rel" select="'leq'"/>
402 </xsl:apply-templates>
403 <xsl:apply-templates mode="noannot" select="*[4]"/>
404 <xsl:apply-templates mode="diseq" select="*[7]">
405 <xsl:with-param name="rel" select="'lt'"/>
406 </xsl:apply-templates>
407 <xsl:apply-templates mode="noannot" select="*[5]"/>
410 <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/less_leEq_trans.con'] and count(child::*) = 7">
412 <m:csymbol>diseq_chain</m:csymbol>
413 <xsl:apply-templates mode="noannot" select="*[3]"/>
414 <xsl:apply-templates mode="diseq" select="*[6]">
415 <xsl:with-param name="rel" select="'lt'"/>
416 </xsl:apply-templates>
417 <xsl:apply-templates mode="noannot" select="*[4]"/>
418 <xsl:apply-templates mode="diseq" select="*[7]">
419 <xsl:with-param name="rel" select="'leq'"/>
420 </xsl:apply-templates>
421 <xsl:apply-templates mode="noannot" select="*[5]"/>
424 <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/leEq_wdr.con'] and count(child::*) = 7">
426 <m:csymbol>diseq_chain</m:csymbol>
427 <xsl:apply-templates mode="noannot" select="*[3]"/>
428 <xsl:apply-templates mode="diseq" select="*[6]">
429 <xsl:with-param name="rel" select="'leq'"/>
430 </xsl:apply-templates>
431 <xsl:apply-templates mode="noannot" select="*[4]"/>
432 <xsl:apply-templates mode="diseq" select="*[7]">
433 <xsl:with-param name="rel" select="'eq'"/>
434 </xsl:apply-templates>
435 <xsl:apply-templates mode="noannot" select="*[5]"/>
438 <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/less_transitive_unfolded.con'] and count(child::*) = 7">
440 <m:csymbol>diseq_chain</m:csymbol>
441 <xsl:apply-templates mode="noannot" select="*[3]"/>
442 <xsl:apply-templates mode="diseq" select="*[6]">
443 <xsl:with-param name="rel" select="'lt'"/>
444 </xsl:apply-templates>
445 <xsl:apply-templates mode="noannot" select="*[4]"/>
446 <xsl:apply-templates mode="diseq" select="*[7]">
447 <xsl:with-param name="rel" select="'lt'"/>
448 </xsl:apply-templates>
449 <xsl:apply-templates mode="noannot" select="*[5]"/>
452 <!-- togliere il parametro -->
453 <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/less_wdr.con'] and count(child::*) = 7">
455 <m:csymbol>diseq_chain</m:csymbol>
456 <xsl:apply-templates mode="noannot" select="*[3]"/>
457 <xsl:apply-templates mode="diseq" select="*[6]">
458 <xsl:with-param name="rel" select="'lt'"/>
459 </xsl:apply-templates>
460 <xsl:apply-templates mode="noannot" select="*[4]"/>
461 <xsl:apply-templates mode="diseq" select="*[7]">
462 <xsl:with-param name="rel" select="'eq'"/>
463 </xsl:apply-templates>
464 <xsl:apply-templates mode="noannot" select="*[5]"/>
467 <!-- togliere il parametro -->
468 <xsl:when test="CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/less_wdl.con'] and count(child::*) = 7">
470 <m:csymbol>diseq_chain</m:csymbol>
471 <xsl:apply-templates mode="noannot" select="*[5]"/>
473 <!-- <m:ci><xsl:value-of select="'eq'"/></m:ci> -->
474 <xsl:call-template name="generate_side_proof">
475 <xsl:with-param name="proof" select="*[7]"/>
476 <xsl:with-param name="show_statement" select="0"/>
478 <xsl:apply-templates mode="noannot" select="*[3]"/>
479 <xsl:apply-templates mode="diseq" select="*[6]">
480 <xsl:with-param name="rel" select="'lt'"/>
481 </xsl:apply-templates>
482 <xsl:apply-templates mode="noannot" select="*[4]"/>
486 <xsl:when test="CONST[
487 attribute::uri='cic:/Coq/Init/Logic/eq_ind.con' or
488 attribute::uri='cic:/Coq/Init/Logic/eq_ind_r.con' or
489 attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
490 attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind_r.con' or
491 attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) = 7">
493 <m:csymbol>rw_step</m:csymbol>
494 <xsl:apply-templates mode="noannot" select="*[5]"/>
495 <xsl:apply-templates mode="pure" select="*[3]"/>
496 <xsl:apply-templates mode="pure" select="*[6]"/>
497 <xsl:call-template name="generate_side_proof">
498 <xsl:with-param name="proof" select="*[7]"/>
500 <!-- <xsl:apply-templates mode="proof_transform" select="*[7]"/> -->
503 <!-- EQUALITY with extra-parameters -->
504 <xsl:when test="CONST[
505 attribute::uri='cic:/Coq/Init/Logic/eq_ind.con' or
506 attribute::uri='cic:/Coq/Init/Logic/eq_ind_r.con' or
507 attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
508 attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind_r.con' or
509 attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) > 7">
510 <xsl:variable name="no_extraproofs" select="count(*[position()>7 and @sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')])"/>
512 <xsl:when test="$no_extraproofs=0">
514 <m:csymbol>rewrite_and_apply</m:csymbol>
516 <m:csymbol>rw_step</m:csymbol>
517 <xsl:apply-templates mode="noannot" select="*[5]"/>
518 <xsl:apply-templates mode="pure" select="*[3]"/>
519 <xsl:apply-templates mode="pure" select="*[6]"/>
520 <xsl:call-template name="generate_side_proof">
521 <xsl:with-param name="proof" select="*[7]"/>
523 <!-- <xsl:apply-templates mode="pure" select="*[7]"/> -->
525 <xsl:apply-templates mode="noannot" select="*[position()>7]"/>
530 <xsl:when test="*[5]/@sort='Prop'">
531 <m:apply helm:xref="{@id}">
532 <m:csymbol>letin</m:csymbol>
534 <m:csymbol>let</m:csymbol>
536 <xsl:call-template name="insert_subscript">
537 <xsl:with-param name="node_value" select="'h1'"/>
540 <xsl:apply-templates mode="noannot" select="*[5]"/>
542 <xsl:call-template name="gen_let">
543 <xsl:with-param name="init_pos" select="1"/>
544 <xsl:with-param name="from" select="7"/>
547 <m:csymbol>rewrite_and_apply</m:csymbol>
549 <m:csymbol>rw_step</m:csymbol>
551 <xsl:call-template name="insert_subscript">
552 <xsl:with-param name="node_value" select="'h1'"/>
555 <xsl:apply-templates mode="pure" select="*[3]"/>
556 <xsl:apply-templates mode="pure" select="*[6]"/>
557 <xsl:call-template name="generate_side_proof">
558 <xsl:with-param name="proof" select="*[7]"/>
560 <!-- <xsl:apply-templates mode="pure" select="*[7]"/> -->
562 <xsl:apply-templates mode="flat" select="*[8]">
563 <xsl:with-param name="n">
564 <xsl:value-of select="2"/>
566 </xsl:apply-templates>
571 <m:apply helm:xref="{@id}">
572 <m:csymbol>letin</m:csymbol>
573 <xsl:call-template name="gen_let">
574 <xsl:with-param name="init_pos" select="0"/>
575 <xsl:with-param name="form" select="7"/>
578 <m:csymbol>rewrite_and_apply</m:csymbol>
580 <m:csymbol>rw_step</m:csymbol>
581 <xsl:apply-templates mode="pure" select="*[5]"/>
582 <xsl:apply-templates mode="pure" select="*[3]"/>
583 <xsl:apply-templates mode="pure" select="*[6]"/>
584 <xsl:call-template name="generate_side_proof">
585 <xsl:with-param name="proof" select="*[7]"/>
587 <!-- <xsl:apply-templates mode="pure" select="*[7]"/> -->
589 <xsl:apply-templates mode="flat" select="*[8]">
590 <xsl:with-param name="n">
591 <xsl:value-of select="1"/>
593 </xsl:apply-templates>
602 <xsl:when test="CONST[
603 attribute::uri='cic:/Coq/Init/Logic/False_ind.con'] and
604 count(child::*) = 3">
605 <m:apply helm:xref="{@id}">
606 <m:csymbol>false_ind</m:csymbol>
607 <m:ci>cic:/Coq/Init/Logic/False_ind.con</m:ci>
608 <xsl:apply-templates mode="noannot" select="*[3]"/>
611 <!-- gestire meglio il caso di and_ind quando la prova
612 non e' della forma \x.\y.M -->
613 <xsl:when test="CONST[
614 attribute::uri='cic:/Coq/Init/Logic/and_ind.con']
615 and count(child::*) = 6
616 and name(*[5])='LAMBDA'">
617 <m:apply helm:xref="{@id}">
618 <m:csymbol>and_ind</m:csymbol>
619 <xsl:apply-templates mode="noannot" select="*[6]"/>
620 <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/*[1]/@binder"/></xsl:with-param></xsl:call-template></m:ci>
621 <xsl:apply-templates mode="pure" select="*[5]/*[1]/*"/>
622 <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/*[2]/@binder"/></xsl:with-param></xsl:call-template></m:ci>
623 <xsl:apply-templates mode="pure" select="*[5]/*[2]/*"/>
624 <xsl:apply-templates mode="proof_transform" select="*[5]/target/*"/>
627 <xsl:when test="CONST[
628 attribute::uri='cic:/Coq/Init/Logic/or_ind.con']
629 and count(child::*) = 7">
631 <xsl:when test="name(*[5])='LAMBDA'
632 and name(*[6])='LAMBDA'">
633 <xsl:variable name="definition_url"
634 select="'cic:/Coq/Init/Logic/or.ind'"/>
635 <m:apply helm:xref="{@id}">
636 <m:csymbol>full_or_ind</m:csymbol>
637 <xsl:apply-templates mode="noannot" select="*[7]"/>
638 <xsl:for-each select="$InnerTypes">
639 <xsl:apply-templates mode="pure" select="key('typeid',$id)/*[1]"/>
642 <m:csymbol>left_case</m:csymbol>
645 <xsl:value-of select="*[5]/*[1]/@binder"/>
648 <xsl:apply-templates mode="pure" select="*[5]/*[1]/*[1]"/>
651 <xsl:apply-templates mode="noannot" select="*[5]/target/*[1]"/>
654 <m:csymbol>right_case</m:csymbol>
657 <xsl:apply-templates mode="pure" select="*[6]/*[1]/@binder"/>
660 <xsl:apply-templates mode="pure" select="*[6]/*[1]/*[1]"/>
663 <xsl:apply-templates mode="noannot" select="*[6]/target/*[1]"/>
668 <m:apply helm:xref="{@id}">
669 <m:csymbol>or_ind</m:csymbol>
670 <xsl:apply-templates mode="noannot" select="*[7]"/>
671 <xsl:for-each select="$InnerTypes">
672 <xsl:apply-templates mode="pure" select="key('typeid',$id)/*[1]"/>
674 <xsl:apply-templates mode="pure" select="*[5]"/>
675 <xsl:apply-templates mode="pure" select="*[6]"/>
680 <!-- ex_ind, exT_ind -->
681 <xsl:when test="(CONST[attribute::uri='cic:/Coq/Init/Logic_Type/exT_ind.con'] or
682 CONST[attribute::uri='cic:/Coq/Init/Logic/ex_ind.con'])
683 and count(child::*) = 6
684 and name(*[5])='LAMBDA'
685 and name(*[5]/*[2])='decl'">
686 <m:apply helm:xref="{@id}">
687 <m:csymbol>ex_ind</m:csymbol>
688 <xsl:apply-templates mode="noannot" select="*[6]"/>
689 <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/*[1]/@binder"/></xsl:with-param></xsl:call-template></m:ci>
690 <xsl:apply-templates mode="pure" select="*[5]/*[1]/*"/>
691 <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/*[2]/@binder"/></xsl:with-param></xsl:call-template></m:ci>
692 <xsl:apply-templates mode="pure" select="*[5]/*[2]/*"/>
693 <xsl:apply-templates mode="proof_transform" select="*[5]/target/*"/>
696 <xsl:when test="name(*[1])='CONST'">
697 <xsl:apply-templates mode="try_inductive" select="."/>
699 <!-- patch temporanea per la gestione di redex -->
700 <xsl:when test="name(*[1])='LAMBDA' and count(child::*)=2
701 and *[2]/@sort='Prop'">
702 <m:apply helm:xref="{@id}">
703 <m:csymbol>letin</m:csymbol>
705 <m:csymbol>let</m:csymbol>
707 <xsl:call-template name="insert_subscript">
708 <xsl:with-param name="node_value">
709 <xsl:value-of select="*[1]/*[1]/@binder"/>
713 <xsl:apply-templates mode="noannot" select="*[2]"/>
715 <xsl:apply-templates mode="proof_transform" select="*[1]/target/*[1]"/>
719 <xsl:apply-templates select="." mode="letin"/>
723 <xsl:when test="name()='LAMBDA'">
725 <xsl:when test="(name(target/*[1])='APPLY' and
726 name(target/*[1]/*[1])='CONST' and
727 (target/*[1]/*[1]/@uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
728 target/*[1]/*[1]/@uri='cic:/Coq/Init/Logic_Type/eqT_ind_r.con' or
729 target/*[1]/*[1]/@uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con')
730 and count(target/*[1]/*) = 8
731 and name(target/*[1]/*[8])='REL'
732 and target/@binder = target/*[1]/*[8]/@binder )">
734 <m:csymbol>rw_step</m:csymbol>
735 <xsl:apply-templates mode="noannot" select="target/*[1]/*[5]"/>
736 <xsl:apply-templates mode="pure" select="target/*[1]/*[3]"/>
737 <xsl:apply-templates mode="pure" select="target/*[1]/*[6]"/>
738 <xsl:call-template name="generate_side_proof">
739 <xsl:with-param name="proof" select="target/*[1]/*[7]"/>
741 <!-- <xsl:apply-templates mode="proof_transform" select="target/*[1]/*[7]"/> -->
745 <xsl:apply-templates mode="pure" select="."/>
750 <xsl:apply-templates select="." mode="pure"/>
755 <xsl:template name="is_simple">
756 <xsl:param name="proof" select="/.."/>
757 <xsl:value-of select="(count($proof/*)=0) or ((name($proof)='APPLY') and (count($proof/*[@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')]) = 0))"/>
760 <xsl:template name="generate_side_proof">
761 <xsl:param name="proof" select="/.."/>
762 <xsl:param name="show_statement" select="1"/>
764 <xsl:variable name="is_simple">
765 <xsl:call-template name="is_simple">
766 <xsl:with-param name="proof" select="$proof"/>
769 <xsl:variable name="is_simple" select="(count($proof/*)=0) or ((name($proof)='APPLY') and (count($proof/*[@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')]) = 0))"/>
771 <xsl:when test="$is_simple">
773 <xsl:when test="name($proof)='APPLY'">
774 <xsl:apply-templates select="$proof" mode="letin"/>
777 <xsl:apply-templates select="$proof" mode="pure"/>
782 <xsl:variable name="id" select="@id"/>
783 <m:apply helm:xref="{@id}">
785 <xsl:when test="$show_statement = 1">
786 <m:csymbol>proof</m:csymbol>
789 <m:csymbol>side_proof</m:csymbol>
792 <xsl:apply-templates mode="proof_transform" select="$proof"/>
793 <xsl:for-each select="$InnerTypes">
794 <xsl:apply-templates mode="pure" select="key('typeid',$proof/@id)/*"/>
797 <!-- <xsl:apply-templates select="$proof" mode="noannot"/> -->
802 <xsl:template match="APPLY" mode="letin">
803 <xsl:variable name="no_subproofs">
804 <xsl:variable name="stars">
805 <xsl:for-each select="*[@sort='Prop']">
806 <xsl:variable name="id" select="@id"/>
807 <xsl:variable name="innertype_available">
808 <xsl:for-each select="$InnerTypes">
809 <xsl:if test="key('typeid',$id)/*">
810 <xsl:text>yes</xsl:text>
814 <xsl:if test="name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX' or ((name(.)='REL' or name(.)='VAR' or name(.)='META' or name(.)='CONST' or name(.)='MUTCONSTRUCT') and $innertype_available='yes')">
815 <!-- We generate one star for each subproof -->
816 <xsl:text>*</xsl:text>
820 <xsl:value-of select="string-length($stars)"/>
822 <!-- <m:cn><xsl:value-of select="$no_subproofs"/></m:cn> -->
824 <xsl:when test="$naturalLanguage='yes' and ($no_subproofs = 1)">
825 <m:apply helm:xref="{@id}">
826 <m:csymbol>letin1</m:csymbol>
827 <xsl:for-each select="*[@sort='Prop']">
828 <xsl:variable name="id" select="@id"/>
829 <xsl:variable name="innertype_available">
830 <xsl:for-each select="$InnerTypes">
831 <xsl:if test="key('typeid',$id)/*">
832 <xsl:text>yes</xsl:text>
836 <xsl:if test="name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX' or ((name(.)='REL' or name(.)='VAR' or name(.)='META' or name(.)='CONST' or name(.)='MUTCONSTRUCT') and $innertype_available='yes')">
837 <xsl:apply-templates mode="noannot" select="."/>
840 <!-- now re-process the application -->
841 <m:apply helm:xref="{@id}">
842 <m:csymbol>app</m:csymbol>
843 <!-- mode previous looks for siblings:
844 call with the first child -->
845 <xsl:apply-templates mode="previous" select="*[1]"/>
849 <xsl:when test="$naturalLanguage='yes' and ($no_subproofs > 1)">
850 <m:apply helm:xref="{@id}">
851 <m:csymbol>letin</m:csymbol>
852 <!-- first process all subproofs (let-in) -->
853 <xsl:call-template name="gen_let"/>
854 <!-- now re-process the application -->
855 <m:apply helm:xref="{@id}">
856 <m:csymbol>app</m:csymbol>
857 <!-- mode flat looks for siblings: call with the first child -->
858 <xsl:apply-templates mode="flat" select="*[1]"/>
864 <xsl:when test="@sort='Prop'">
866 <m:csymbol>app</m:csymbol>
867 <xsl:apply-templates mode="erase" select="*[1]"/>
871 <xsl:apply-templates mode="pure" select="."/>
878 <xsl:template name="gen_let">
879 <xsl:param name="init_pos" select="0"/>
880 <xsl:param name="from" select="0"/>
881 <xsl:for-each select="*[position()>$from and @sort='Prop']">
882 <xsl:variable name="id" select="@id"/>
883 <xsl:variable name="innertype_available">
884 <xsl:for-each select="$InnerTypes">
885 <xsl:if test="key('typeid',$id)/*">
886 <xsl:text>yes</xsl:text>
890 <xsl:if test="name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX' or ((name(.)='REL' or name(.)='VAR' or name(.)='META' or name(.)='CONST' or name(.)='MUTCONSTRUCT') and $innertype_available='yes')">
892 <m:csymbol>let</m:csymbol>
893 <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="concat('h',position()+$init_pos)"/></xsl:with-param></xsl:call-template></m:ci>
894 <xsl:apply-templates mode="noannot" select="."/>
900 <xsl:template match="*" mode="erase">
902 <xsl:when test="@sort='Prop' or $naturalLanguage='no'">
903 <xsl:apply-templates mode="pure" select="."/>
909 <xsl:apply-templates mode="erase" select="following-sibling::*[1]"/>
912 <xsl:template match="*" mode="previous">
913 <xsl:variable name="innertype_available">
914 <xsl:variable name="id" select="@id"/>
915 <xsl:for-each select="$InnerTypes">
916 <xsl:if test="key('typeid',$id)/*">
917 <xsl:text>yes</xsl:text>
922 <xsl:when test="@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX' or ((name(.)='REL' or name(.)='VAR' or name(.)='META' or name(.)='CONST' or name(.)='MUTCONSTRUCT') and $innertype_available='yes'))">
923 <m:ci>previous</m:ci>
926 <!-- forse bisognerebbe trattare solo l'elemento di testa -->
928 <xsl:when test="@sort='Prop' or $naturalLanguage='no'">
929 <xsl:apply-templates mode="pure" select="."/>
935 <!-- <xsl:apply-templates select="." mode="pure"/> -->
938 <xsl:apply-templates mode="previous" select="following-sibling::*[1]"/>
941 <xsl:template match="*" mode="flat">
942 <xsl:param name="n" select="1"/>
943 <xsl:variable name="id" select="@id"/>
944 <xsl:variable name="innertype_available">
945 <xsl:for-each select="$InnerTypes">
946 <xsl:if test="key('typeid',$id)/*">
947 <xsl:text>yes</xsl:text>
952 <xsl:when test="$naturalLanguage='yes' and @sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX' or ((name(.)='REL' or name(.)='VAR' or name(.)='META' or name(.)='CONST' or name(.)='MUTCONSTRUCT') and $innertype_available='yes'))">
954 <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="concat('h',$n)"/></xsl:with-param></xsl:call-template>
956 <xsl:apply-templates mode="flat" select="following-sibling::*[1]">
957 <xsl:with-param name="n" select="$n+1"/>
958 </xsl:apply-templates>
962 <xsl:when test="name()='REL' or @sort='Prop' or $naturalLanguage='no'">
963 <xsl:apply-templates mode="pure" select="."/>
969 <!-- <xsl:apply-templates mode="pure" select="."/> -->
970 <xsl:apply-templates mode="flat" select="following-sibling::*[1]">
971 <xsl:with-param name="n" select="$n"/>
972 </xsl:apply-templates>
977 <!-- Auxiliary functions -->
978 <!-- OMDOC: now we have name_of_uri generalized on the extension that -->
979 <!-- can replace the next template -->
980 <xsl:template name="get_name">
981 <xsl:param name="uri" select="''"/>
982 <xsl:variable name="sub_after" select="substring-after($uri,'/')"/>
984 <xsl:when test="contains($sub_after,'/')">
985 <xsl:call-template name="get_name">
986 <xsl:with-param name="uri" select="$sub_after"/>
990 <xsl:value-of select="substring-before($sub_after,'_ind.con')"/>
995 <!-- <xsl:template match="APPLY[CONST[
996 attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con']]" mode="appflat">
998 <xsl:when test="count(child::*) > 4">
999 <m:apply helm:xref="{@id}">
1000 <m:csymbol>app</m:csymbol>
1001 <xsl:apply-templates mode="pure" select="*[1]"/>
1005 <xsl:apply-templates mode="flat" select="*[5]"/>
1009 <m:apply helm:xref="{@id}">
1010 <m:csymbol>app</m:csymbol>
1011 <xsl:apply-templates mode="flat" select="*[1]"/>