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 <!-- ALL this elements does not have inner type -->
45 <xsl:template match="PROD|SORT|MUTIND" 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 <m:apply helm:xref="{@id}">
63 <m:csymbol>proof</m:csymbol>
64 <xsl:apply-templates mode="proof_transform" select="."/>
65 <!-- <xsl:apply-templates mode="try_inductive" 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="@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>
90 <xsl:when test="$naturalLanguage='yes' and @sort='Prop' and $innertype_available='yes'">
91 <m:apply helm:xref="{@id}">
92 <m:csymbol>proof</m:csymbol>
93 <xsl:apply-templates mode="proof_transform" select="."/>
94 <xsl:for-each select="$InnerTypes">
95 <xsl:apply-templates mode="pure" select="key('typeid',$id)/*"/>
100 <xsl:apply-templates select="." mode="pure"/>
105 <!-- ALL these elements have inner type -->
106 <xsl:template match="LETIN|CAST|APPLY|MUTCASE|FIX|COFIX" mode="noannot">
107 <xsl:variable name="id" select="@id"/>
109 <xsl:when test="$naturalLanguage='yes' and @sort='Prop'">
110 <m:apply helm:xref="{@id}">
111 <m:csymbol>proof</m:csymbol>
112 <xsl:apply-templates mode="proof_transform" select="."/>
113 <!-- <xsl:apply-templates mode="try_inductive" 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/CSetoids/CSetoid_basics/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/COrdFields/Basic_Properties_of_leEq/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/COrdFields/Basic_Properties_of_leEq/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/COrdFields/Basic_Properties_of_leEq/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/COrdFields/Basic_Properties_of_leEq/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/COrdFields/Basic_Properties_of_leEq/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/COrdFields/COrdField_axioms/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/COrdFields/COrdField_axioms/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/COrdFields/COrdField_axioms/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/CSetoids/CSetoid_basics/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/COrdFields/Basic_Properties_of_leEq/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/COrdFields/Basic_Properties_of_leEq/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/COrdFields/Basic_Properties_of_leEq/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/COrdFields/Basic_Properties_of_leEq/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/COrdFields/Basic_Properties_of_leEq/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/COrdFields/COrdField_axioms/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/COrdFields/COrdField_axioms/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/COrdFields/COrdField_axioms/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/Equality/eq_ind.con' or
488 attribute::uri='cic:/Coq/Init/Logic/Logic_lemmas/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/Equality/eq_ind.con' or
506 attribute::uri='cic:/Coq/Init/Logic/Logic_lemmas/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/Conjunction/and_ind.con']
615 and count(child::*) = 6
616 and name(*[5])='LAMBDA'
617 and name(*[5]/target/*[1])='LAMBDA'">
618 <m:apply helm:xref="{@id}">
619 <m:csymbol>and_ind</m:csymbol>
620 <xsl:apply-templates mode="noannot" select="*[6]"/>
621 <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/target/@binder"/></xsl:with-param></xsl:call-template></m:ci>
622 <xsl:apply-templates mode="pure" select="*[5]/source/*"/>
623 <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/target/LAMBDA/target/@binder"/></xsl:with-param></xsl:call-template></m:ci>
624 <xsl:apply-templates mode="pure" select="*[5]/target/LAMBDA/source/*"/>
625 <xsl:apply-templates mode="proof_transform" select="*[5]/target/LAMBDA/target/*"/>
628 <xsl:when test="CONST[
629 attribute::uri='cic:/Coq/Init/Logic/Disjunction/or_ind.con']
630 and count(child::*) = 7">
632 <xsl:when test="name(*[5])='LAMBDA'
633 and name(*[6])='LAMBDA'">
634 <xsl:variable name="definition_url"
635 select="'cic:/Coq/Init/Logic/Disjunction/or.ind'"/>
636 <m:apply helm:xref="{@id}">
637 <m:csymbol>full_or_ind</m:csymbol>
638 <xsl:apply-templates mode="noannot" select="*[7]"/>
639 <xsl:for-each select="$InnerTypes">
640 <xsl:apply-templates mode="pure" select="key('typeid',$id)/*[1]"/>
643 <m:csymbol>left_case</m:csymbol>
646 <xsl:value-of select="*[5]/target/@binder"/>
649 <xsl:apply-templates mode="pure" select="*[5]/source/*[1]"/>
652 <xsl:apply-templates mode="noannot" select="*[5]/target/*[1]"/>
655 <m:csymbol>right_case</m:csymbol>
658 <xsl:apply-templates mode="pure" select="*[6]/target/@binder"/>
661 <xsl:apply-templates mode="pure" select="*[6]/source/*[1]"/>
664 <xsl:apply-templates mode="noannot" select="*[6]/target/*[1]"/>
669 <m:apply helm:xref="{@id}">
670 <m:csymbol>or_ind</m:csymbol>
671 <xsl:apply-templates mode="noannot" select="*[7]"/>
672 <xsl:for-each select="$InnerTypes">
673 <xsl:apply-templates mode="pure" select="key('typeid',$id)/*[1]"/>
675 <xsl:apply-templates mode="pure" select="*[5]"/>
676 <xsl:apply-templates mode="pure" select="*[6]"/>
681 <!-- ex_ind, exT_ind -->
682 <xsl:when test="(CONST[attribute::uri='cic:/Coq/Init/Logic_Type/exT_ind.con'] or
683 CONST[attribute::uri='cic:/Coq/Init/Logic/First_order_quantifiers/ex_ind.con'])
684 and count(child::*) = 6
685 and name(*[5])='LAMBDA'
686 and name(*[5]/target/*[1])='LAMBDA'">
687 <m:apply helm:xref="{@id}">
688 <m:csymbol>ex_ind</m:csymbol>
689 <xsl:apply-templates mode="noannot" select="*[6]"/>
690 <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/target/@binder"/></xsl:with-param></xsl:call-template></m:ci>
691 <xsl:apply-templates mode="pure" select="*[5]/source/*"/>
692 <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/target/LAMBDA/target/@binder"/></xsl:with-param></xsl:call-template></m:ci>
693 <xsl:apply-templates mode="pure" select="*[5]/target/LAMBDA/source/*"/>
694 <xsl:apply-templates mode="proof_transform" select="*[5]/target/LAMBDA/target/*"/>
697 <xsl:when test="name(*[1])='CONST'">
698 <xsl:apply-templates mode="try_inductive" select="."/>
700 <!-- patch temporanea per la gestione di redex -->
701 <xsl:when test="name(*[1])='LAMBDA' and count(child::*)=2
702 and *[2]/@sort='Prop'">
703 <m:apply helm:xref="{@id}">
704 <m:csymbol>letin</m:csymbol>
706 <m:csymbol>let</m:csymbol>
708 <xsl:call-template name="insert_subscript">
709 <xsl:with-param name="node_value">
710 <xsl:value-of select="*[1]/target/@binder"/>
714 <xsl:apply-templates mode="noannot" select="*[2]"/>
716 <xsl:apply-templates mode="proof_transform" select="*[1]/target/*[1]"/>
720 <xsl:apply-templates select="." mode="letin"/>
724 <xsl:when test="name()='LAMBDA'">
726 <xsl:when test="(name(target/*[1])='APPLY' and
727 name(target/*[1]/*[1])='CONST' and
728 (target/*[1]/*[1]/@uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
729 target/*[1]/*[1]/@uri='cic:/Coq/Init/Logic_Type/eqT_ind_r.con' or
730 target/*[1]/*[1]/@uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con')
731 and count(target/*[1]/*) = 8
732 and name(target/*[1]/*[8])='REL'
733 and target/@binder = target/*[1]/*[8]/@binder )">
735 <m:csymbol>rw_step</m:csymbol>
736 <xsl:apply-templates mode="noannot" select="target/*[1]/*[5]"/>
737 <xsl:apply-templates mode="pure" select="target/*[1]/*[3]"/>
738 <xsl:apply-templates mode="pure" select="target/*[1]/*[6]"/>
739 <xsl:call-template name="generate_side_proof">
740 <xsl:with-param name="proof" select="target/*[1]/*[7]"/>
742 <!-- <xsl:apply-templates mode="proof_transform" select="target/*[1]/*[7]"/> -->
746 <xsl:apply-templates mode="pure" select="."/>
751 <xsl:apply-templates select="." mode="pure"/>
756 <xsl:template name="is_simple">
757 <xsl:param name="proof" select="/.."/>
758 <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))"/>
761 <xsl:template name="generate_side_proof">
762 <xsl:param name="proof" select="/.."/>
763 <xsl:param name="show_statement" select="1"/>
765 <xsl:variable name="is_simple">
766 <xsl:call-template name="is_simple">
767 <xsl:with-param name="proof" select="$proof"/>
770 <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))"/>
772 <xsl:when test="$is_simple">
774 <xsl:when test="name($proof)='APPLY'">
775 <xsl:apply-templates select="$proof" mode="letin"/>
778 <xsl:apply-templates select="$proof" mode="pure"/>
783 <xsl:variable name="id" select="@id"/>
784 <m:apply helm:xref="{@id}">
786 <xsl:when test="$show_statement = 1">
787 <m:csymbol>proof</m:csymbol>
790 <m:csymbol>side_proof</m:csymbol>
793 <xsl:apply-templates mode="proof_transform" select="$proof"/>
794 <xsl:for-each select="$InnerTypes">
795 <xsl:apply-templates mode="pure" select="key('typeid',$proof/@id)/*"/>
798 <!-- <xsl:apply-templates select="$proof" mode="noannot"/> -->
803 <xsl:template match="APPLY" mode="letin">
804 <xsl:variable name="no_subproofs">
805 <xsl:variable name="stars">
806 <xsl:for-each select="*[@sort='Prop']">
807 <xsl:variable name="id" select="@id"/>
808 <xsl:variable name="innertype_available">
809 <xsl:for-each select="$InnerTypes">
810 <xsl:if test="key('typeid',$id)/*">
811 <xsl:text>yes</xsl:text>
815 <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')">
816 <!-- We generate one star for each subproof -->
817 <xsl:text>*</xsl:text>
821 <xsl:value-of select="string-length($stars)"/>
823 <!-- <m:cn><xsl:value-of select="$no_subproofs"/></m:cn> -->
825 <xsl:when test="$naturalLanguage='yes' and ($no_subproofs = 1)">
826 <m:apply helm:xref="{@id}">
827 <m:csymbol>letin1</m:csymbol>
828 <xsl:for-each select="*[@sort='Prop']">
829 <xsl:variable name="id" select="@id"/>
830 <xsl:variable name="innertype_available">
831 <xsl:for-each select="$InnerTypes">
832 <xsl:if test="key('typeid',$id)/*">
833 <xsl:text>yes</xsl:text>
837 <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')">
838 <xsl:apply-templates mode="noannot" select="."/>
841 <!-- now re-process the application -->
842 <m:apply helm:xref="{@id}">
843 <m:csymbol>app</m:csymbol>
844 <!-- mode previous looks for siblings:
845 call with the first child -->
846 <xsl:apply-templates mode="previous" select="*[1]"/>
850 <xsl:when test="$naturalLanguage='yes' and ($no_subproofs > 1)">
851 <m:apply helm:xref="{@id}">
852 <m:csymbol>letin</m:csymbol>
853 <!-- first process all subproofs (let-in) -->
854 <xsl:call-template name="gen_let"/>
855 <!-- now re-process the application -->
856 <m:apply helm:xref="{@id}">
857 <m:csymbol>app</m:csymbol>
858 <!-- mode flat looks for siblings: call with the first child -->
859 <xsl:apply-templates mode="flat" select="*[1]"/>
865 <xsl:when test="@sort='Prop'">
867 <m:csymbol>app</m:csymbol>
868 <xsl:apply-templates mode="erase" select="*[1]"/>
872 <xsl:apply-templates mode="pure" select="."/>
879 <xsl:template name="gen_let">
880 <xsl:param name="init_pos" select="0"/>
881 <xsl:param name="from" select="0"/>
882 <xsl:for-each select="*[position()>$from and @sort='Prop']">
883 <xsl:variable name="id" select="@id"/>
884 <xsl:variable name="innertype_available">
885 <xsl:for-each select="$InnerTypes">
886 <xsl:if test="key('typeid',$id)/*">
887 <xsl:text>yes</xsl:text>
891 <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')">
893 <m:csymbol>let</m:csymbol>
894 <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>
895 <xsl:apply-templates mode="noannot" select="."/>
901 <xsl:template match="*" mode="erase">
903 <xsl:when test="@sort='Prop' or $naturalLanguage='no'">
904 <xsl:apply-templates mode="pure" select="."/>
910 <xsl:apply-templates mode="erase" select="following-sibling::*[1]"/>
913 <xsl:template match="*" mode="previous">
914 <xsl:variable name="innertype_available">
915 <xsl:variable name="id" select="@id"/>
916 <xsl:for-each select="$InnerTypes">
917 <xsl:if test="key('typeid',$id)/*">
918 <xsl:text>yes</xsl:text>
923 <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'))">
924 <m:ci>previous</m:ci>
927 <!-- forse bisognerebbe trattare solo l'elemento di testa -->
929 <xsl:when test="@sort='Prop' or $naturalLanguage='no'">
930 <xsl:apply-templates mode="pure" select="."/>
936 <!-- <xsl:apply-templates select="." mode="pure"/> -->
939 <xsl:apply-templates mode="previous" select="following-sibling::*[1]"/>
942 <xsl:template match="*" mode="flat">
943 <xsl:param name="n" select="1"/>
944 <xsl:variable name="id" select="@id"/>
945 <xsl:variable name="innertype_available">
946 <xsl:for-each select="$InnerTypes">
947 <xsl:if test="key('typeid',$id)/*">
948 <xsl:text>yes</xsl:text>
953 <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'))">
955 <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>
957 <xsl:apply-templates mode="flat" select="following-sibling::*[1]">
958 <xsl:with-param name="n" select="$n+1"/>
959 </xsl:apply-templates>
963 <xsl:when test="name()='REL' or @sort='Prop' or $naturalLanguage='no'">
964 <xsl:apply-templates mode="pure" select="."/>
970 <!-- <xsl:apply-templates mode="pure" select="."/> -->
971 <xsl:apply-templates mode="flat" select="following-sibling::*[1]">
972 <xsl:with-param name="n" select="$n"/>
973 </xsl:apply-templates>
978 <!-- Auxiliary functions -->
979 <!-- OMDOC: now we have name_of_uri generalized on the extension that -->
980 <!-- can replace the next template -->
981 <xsl:template name="get_name">
982 <xsl:param name="uri" select="''"/>
983 <xsl:variable name="sub_after" select="substring-after($uri,'/')"/>
985 <xsl:when test="contains($sub_after,'/')">
986 <xsl:call-template name="get_name">
987 <xsl:with-param name="uri" select="$sub_after"/>
991 <xsl:value-of select="substring-before($sub_after,'_ind.con')"/>
996 <!-- <xsl:template match="APPLY[CONST[
997 attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con']]" mode="appflat">
999 <xsl:when test="count(child::*) > 4">
1000 <m:apply helm:xref="{@id}">
1001 <m:csymbol>app</m:csymbol>
1002 <xsl:apply-templates mode="pure" select="*[1]"/>
1006 <xsl:apply-templates mode="flat" select="*[5]"/>
1010 <m:apply helm:xref="{@id}">
1011 <m:csymbol>app</m:csymbol>
1012 <xsl:apply-templates mode="flat" select="*[1]"/>