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"/> -->
43 <!-- ALL this elements does not have inner type -->
44 <xsl:template match="LETIN|PROD|REL|SORT|VAR|META|CONST|MUTIND|MUTCONSTRUCT" mode="noannot">
45 <xsl:apply-templates select="." mode="pure"/>
48 <!-- ALL ELEMENTS WITH A TYPE ARE TRANSLATED AS A PROOF-ELEMENT -->
50 <!-- LAMBDA has inner type only if it is not nested inside another lambda -->
51 <xsl:template match="LAMBDA" mode="noannot">
52 <xsl:variable name="id" select="@id"/>
54 <xsl:when test="$naturalLanguage='yes' and @sort='Prop' and name(../..) != 'LAMBDA'">
55 <m:apply helm:xref="{@id}">
56 <m:csymbol>proof</m:csymbol>
57 <xsl:apply-templates mode="proof_transform" select="."/>
58 <xsl:apply-templates mode="pure" select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
62 <xsl:apply-templates select="." mode="pure"/>
67 <!-- ALL these elements have inner type -->
68 <xsl:template match="CAST|APPLY|MUTCASE|FIX|COFIX" mode="noannot">
69 <xsl:variable name="id" select="@id"/>
71 <xsl:when test="$naturalLanguage='yes' and @sort='Prop'">
72 <m:apply helm:xref="{@id}">
73 <m:csymbol>proof</m:csymbol>
74 <xsl:apply-templates mode="proof_transform" select="."/>
75 <!-- <xsl:apply-templates mode="try_inductive" select="."/> -->
76 <xsl:apply-templates mode="pure" select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
81 <xsl:when test="name()='APPLY'">
82 <!-- This is the case of an applicative expression wich is not
83 a proof but could contains proofs...
84 MODE LETIN OR MODE PURE ??? Big question -->
85 <xsl:apply-templates select="." mode="pure"/>
88 <xsl:apply-templates select="." mode="pure"/>
95 <!-- si presuppone che il tipo induttivo non sia mutuamente
96 induttivo. Bisognerebbe andare a vedere l'utlimo parametro
97 del presunto "principio di induzione", tirare fuori il tipo induttivo
98 e vedere se il suo nome coincide con il prefisso di _ind.
99 Ad esempio nat_double_ind e' definito dall'utente. L'ultimo
100 parametro di nat_double_ind e' di tipo nat, e nat e' diverso
101 da nat_double. Per ora, verifico solo l'esistenza di nat_double,
102 ma questo, benche' non porti ad errore, non copre tutti i
103 casi per quelli mutuamente induttivi -->
105 <xsl:template mode="try_inductive" match="APPLY">
106 <xsl:variable name="id" select="@id"/>
108 <xsl:when test="CONST[1]">
109 <xsl:variable name="uri" select="CONST[1]/@uri"/>
111 <xsl:when test="contains($uri,'_ind.con')">
112 <xsl:variable name="ind_uri"
113 select="concat(substring-before($uri,'_ind.con'),'.ind')"/>
114 <xsl:variable name="InductiveTypeUrl"><xsl:call-template name="URLofURI4getter"><xsl:with-param name="uri" select="$ind_uri"/></xsl:call-template></xsl:variable>
115 <xsl:variable name="inductive_def"
116 select="document($InductiveTypeUrl)/InductiveDefinition"/>
117 <!-- check if the corresponding inductive definition actually
120 <xsl:when test="$inductive_def">
121 <xsl:variable name="ind_name">
122 <xsl:call-template name="get_name">
123 <xsl:with-param name="uri" select="$uri"/>
126 <xsl:variable name="no_params">
127 <xsl:call-template name="get_no_params">
128 <xsl:with-param name="first_uri" select="$CICURI"/>
129 <xsl:with-param name="second_uri" select="$uri"/>
132 <xsl:apply-templates mode="inductive" select=".">
133 <xsl:with-param name="inductive_def_uri"
135 <xsl:with-param name="inductive_def"
136 select="$inductive_def"/>
137 <xsl:with-param name="section_params" select="$no_params"/>
138 <xsl:with-param name="inductive_def_index" select="1"/>
139 <xsl:with-param name="inductive_def_name" select="$ind_name"/>
140 </xsl:apply-templates>
143 <xsl:apply-templates mode="letin" select="."/>
148 <xsl:apply-templates mode="letin" select="."/>
153 <xsl:apply-templates mode="letin" select="."/>
158 <xsl:template mode="eq_transitive" match="*">
159 <!-- <m:ci>eccomi-1: <xsl:value-of select="name()"/></m:ci> -->
161 <xsl:when test="name()='APPLY'">
162 <!-- <m:ci>eccomi-2: <xsl:value-of select="CONST[1]/@uri"/></m:ci> -->
163 <xsl:variable name="id" select="@id"/>
165 <!-- ricordarsi di trattare il parametro -->
166 <xsl:when test="CONST[attribute::uri='cic:/Algebra/CSetoids/CSetoid_basics/eq_transitive_unfolded.con'] and count(child::*) = 7">
167 <!-- <m:ci>eccomi-3</m:ci> -->
168 <xsl:apply-templates mode="eq_transitive" select="*[6]"/>
169 <xsl:apply-templates mode="noannot" select="*[4]"/>
170 <xsl:apply-templates mode="eq_transitive" select="*[7]"/>
173 <xsl:call-template name="generate_side_proof">
174 <xsl:with-param name="proof" select="."/>
175 <xsl:with-param name="show_statement" select="0"/>
181 <xsl:call-template name="generate_side_proof">
182 <xsl:with-param name="proof" select="."/>
183 <xsl:with-param name="show_statement" select="0"/>
189 <xsl:template mode="diseq" match="*">
190 <xsl:param name="rel" select="'eq'"/>
192 <xsl:when test="name()='APPLY'">
193 <xsl:variable name="id" select="@id"/>
195 <!-- ricordarsi di trattare il parametro -->
196 <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_transitive.con'] and count(child::*) = 7">
197 <xsl:apply-templates mode="diseq" select="*[6]">
198 <xsl:with-param name="rel" select="'leq'"/>
199 </xsl:apply-templates>
200 <xsl:apply-templates mode="noannot" select="*[4]"/>
201 <xsl:apply-templates mode="diseq" select="*[7]">
202 <xsl:with-param name="rel" select="'leq'"/>
203 </xsl:apply-templates>
205 <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_wdl.con'] and count(child::*) = 7">
207 <!-- <m:ci><xsl:value-of select="'eq'"/></m:ci> -->
208 <xsl:call-template name="generate_side_proof">
209 <xsl:with-param name="proof" select="*[7]"/>
210 <xsl:with-param name="show_statement" select="0"/>
212 <xsl:apply-templates mode="noannot" select="*[3]"/>
213 <xsl:apply-templates mode="diseq" select="*[6]">
214 <xsl:with-param name="rel" select="'leq'"/>
215 </xsl:apply-templates>
217 <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_less_trans.con'] and count(child::*) = 7">
218 <xsl:apply-templates mode="diseq" select="*[6]">
219 <xsl:with-param name="rel" select="'leq'"/>
220 </xsl:apply-templates>
221 <xsl:apply-templates mode="noannot" select="*[4]"/>
222 <xsl:apply-templates mode="diseq" select="*[7]">
223 <xsl:with-param name="rel" select="'lt'"/>
224 </xsl:apply-templates>
226 <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/less_leEq_trans.con'] and count(child::*) = 7">
227 <xsl:apply-templates mode="diseq" select="*[6]">
228 <xsl:with-param name="rel" select="'lt'"/>
229 </xsl:apply-templates>
230 <xsl:apply-templates mode="noannot" select="*[4]"/>
231 <xsl:apply-templates mode="diseq" select="*[7]">
232 <xsl:with-param name="rel" select="'leq'"/>
233 </xsl:apply-templates>
235 <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_wdr.con'] and count(child::*) = 7">
236 <xsl:apply-templates mode="diseq" select="*[6]">
237 <xsl:with-param name="rel" select="'leq'"/>
238 </xsl:apply-templates>
239 <xsl:apply-templates mode="noannot" select="*[4]"/>
240 <xsl:apply-templates mode="diseq" select="*[7]">
241 <xsl:with-param name="rel" select="'eq'"/>
242 </xsl:apply-templates>
244 <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_transitive_unfolded.con'] and count(child::*) = 7">
245 <xsl:apply-templates mode="diseq" select="*[6]">
246 <xsl:with-param name="rel" select="'lt'"/>
247 </xsl:apply-templates>
248 <xsl:apply-templates mode="noannot" select="*[4]"/>
249 <xsl:apply-templates mode="diseq" select="*[7]">
250 <xsl:with-param name="rel" select="'lt'"/>
251 </xsl:apply-templates>
253 <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_wdr.con'] and count(child::*) = 7">
254 <xsl:apply-templates mode="diseq" select="*[6]">
255 <xsl:with-param name="rel" select="'lt'"/>
256 </xsl:apply-templates>
257 <xsl:apply-templates mode="noannot" select="*[4]"/>
258 <xsl:apply-templates mode="diseq" select="*[7]">
259 <xsl:with-param name="rel" select="'eq'"/>
260 </xsl:apply-templates>
262 <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_wdl.con'] and count(child::*) = 7">
264 <!-- <m:ci><xsl:value-of select="'eq'"/></m:ci> -->
265 <xsl:call-template name="generate_side_proof">
266 <xsl:with-param name="proof" select="*[7]"/>
267 <xsl:with-param name="show_statement" select="0"/>
269 <xsl:apply-templates mode="noannot" select="*[3]"/>
270 <xsl:apply-templates mode="diseq" select="*[6]">
271 <xsl:with-param name="rel" select="'lt'"/>
272 </xsl:apply-templates>
275 <xsl:when test="CONST[attribute::uri='cic:/Algebra/CSetoids/CSetoid_basics/eq_transitive_unfolded.con'] and count(child::*) = 7">
276 <xsl:apply-templates mode="diseq" select="*[6]"/>
278 <xsl:apply-templates mode="noannot" select="*[4]"/>
280 <xsl:apply-templates mode="diseq" select="*[7]"/>
284 <xsl:element name="{concat('m:',$rel)}"/>
285 <!-- <m:ci><xsl:value-of select="$rel"/></m:ci> -->
286 <xsl:call-template name="generate_side_proof">
287 <xsl:with-param name="proof" select="."/>
288 <xsl:with-param name="show_statement" select="0"/>
294 <xsl:element name="{concat('m:',$rel)}"/>
295 <!-- <m:ci><xsl:value-of select="$rel"/></m:ci> -->
296 <xsl:call-template name="generate_side_proof">
297 <xsl:with-param name="proof" select="."/>
298 <xsl:with-param name="show_statement" select="0"/>
304 <xsl:template mode="proof_transform" match="*">
306 <xsl:when test="name()='APPLY'">
307 <xsl:variable name="id" select="@id"/>
309 <!-- Algebra equality (eq_transitive_unfolded) -->
310 <!-- It requires a special mode "eq_transitive"-->
311 <!-- togliere il parametro -->
312 <xsl:when test="CONST[attribute::uri='cic:/Algebra/CSetoids/CSetoid_basics/eq_transitive_unfolded.con'] and count(child::*) = 7">
314 <m:csymbol>eq_chain</m:csymbol>
315 <xsl:apply-templates mode="noannot" select="*[3]"/>
316 <xsl:apply-templates mode="eq_transitive" select="*[6]"/>
317 <xsl:apply-templates mode="noannot" select="*[4]"/>
318 <xsl:apply-templates mode="eq_transitive" select="*[7]"/>
319 <xsl:apply-templates mode="noannot" select="*[5]"/>
322 <!-- Algebra disequalities -->
323 <!-- It requires a special mode "diseq"-->
324 <!-- togliere il parametro -->
325 <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_transitive.con'] and count(child::*) = 7">
327 <m:csymbol>diseq_chain</m:csymbol>
328 <xsl:apply-templates mode="noannot" select="*[3]"/>
329 <xsl:apply-templates mode="diseq" select="*[6]">
330 <xsl:with-param name="rel" select="'leq'"/>
331 </xsl:apply-templates>
332 <xsl:apply-templates mode="noannot" select="*[4]"/>
333 <xsl:apply-templates mode="diseq" select="*[7]">
334 <xsl:with-param name="rel" select="'leq'"/>
335 </xsl:apply-templates>
336 <xsl:apply-templates mode="noannot" select="*[5]"/>
339 <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_wdl.con'] and count(child::*) = 7">
341 <m:csymbol>diseq_chain</m:csymbol>
342 <xsl:apply-templates mode="noannot" select="*[5]"/>
344 <!-- <m:ci><xsl:value-of select="'eq'"/></m:ci> -->
345 <xsl:call-template name="generate_side_proof">
346 <xsl:with-param name="proof" select="*[7]"/>
347 <xsl:with-param name="show_statement" select="0"/>
349 <xsl:apply-templates mode="noannot" select="*[3]"/>
350 <xsl:apply-templates mode="diseq" select="*[6]">
351 <xsl:with-param name="rel" select="'leq'"/>
352 </xsl:apply-templates>
353 <xsl:apply-templates mode="noannot" select="*[4]"/>
356 <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_less_trans.con'] and count(child::*) = 7">
358 <m:csymbol>diseq_chain</m:csymbol>
359 <xsl:apply-templates mode="noannot" select="*[3]"/>
360 <xsl:apply-templates mode="diseq" select="*[6]">
361 <xsl:with-param name="rel" select="'leq'"/>
362 </xsl:apply-templates>
363 <xsl:apply-templates mode="noannot" select="*[4]"/>
364 <xsl:apply-templates mode="diseq" select="*[7]">
365 <xsl:with-param name="rel" select="'lt'"/>
366 </xsl:apply-templates>
367 <xsl:apply-templates mode="noannot" select="*[5]"/>
370 <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/less_leEq_trans.con'] and count(child::*) = 7">
372 <m:csymbol>diseq_chain</m:csymbol>
373 <xsl:apply-templates mode="noannot" select="*[3]"/>
374 <xsl:apply-templates mode="diseq" select="*[6]">
375 <xsl:with-param name="rel" select="'lt'"/>
376 </xsl:apply-templates>
377 <xsl:apply-templates mode="noannot" select="*[4]"/>
378 <xsl:apply-templates mode="diseq" select="*[7]">
379 <xsl:with-param name="rel" select="'leq'"/>
380 </xsl:apply-templates>
381 <xsl:apply-templates mode="noannot" select="*[5]"/>
384 <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_wdr.con'] and count(child::*) = 7">
386 <m:csymbol>diseq_chain</m:csymbol>
387 <xsl:apply-templates mode="noannot" select="*[3]"/>
388 <xsl:apply-templates mode="diseq" select="*[6]">
389 <xsl:with-param name="rel" select="'leq'"/>
390 </xsl:apply-templates>
391 <xsl:apply-templates mode="noannot" select="*[4]"/>
392 <xsl:apply-templates mode="diseq" select="*[7]">
393 <xsl:with-param name="rel" select="'eq'"/>
394 </xsl:apply-templates>
395 <xsl:apply-templates mode="noannot" select="*[5]"/>
398 <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_transitive_unfolded.con'] and count(child::*) = 7">
400 <m:csymbol>diseq_chain</m:csymbol>
401 <xsl:apply-templates mode="noannot" select="*[3]"/>
402 <xsl:apply-templates mode="diseq" select="*[6]">
403 <xsl:with-param name="rel" select="'lt'"/>
404 </xsl:apply-templates>
405 <xsl:apply-templates mode="noannot" select="*[4]"/>
406 <xsl:apply-templates mode="diseq" select="*[7]">
407 <xsl:with-param name="rel" select="'lt'"/>
408 </xsl:apply-templates>
409 <xsl:apply-templates mode="noannot" select="*[5]"/>
412 <!-- togliere il parametro -->
413 <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_wdr.con'] and count(child::*) = 7">
415 <m:csymbol>diseq_chain</m:csymbol>
416 <xsl:apply-templates mode="noannot" select="*[3]"/>
417 <xsl:apply-templates mode="diseq" select="*[6]">
418 <xsl:with-param name="rel" select="'lt'"/>
419 </xsl:apply-templates>
420 <xsl:apply-templates mode="noannot" select="*[4]"/>
421 <xsl:apply-templates mode="diseq" select="*[7]">
422 <xsl:with-param name="rel" select="'eq'"/>
423 </xsl:apply-templates>
424 <xsl:apply-templates mode="noannot" select="*[5]"/>
427 <!-- togliere il parametro -->
428 <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_wdl.con'] and count(child::*) = 7">
430 <m:csymbol>diseq_chain</m:csymbol>
431 <xsl:apply-templates mode="noannot" select="*[5]"/>
433 <!-- <m:ci><xsl:value-of select="'eq'"/></m:ci> -->
434 <xsl:call-template name="generate_side_proof">
435 <xsl:with-param name="proof" select="*[7]"/>
436 <xsl:with-param name="show_statement" select="0"/>
438 <xsl:apply-templates mode="noannot" select="*[3]"/>
439 <xsl:apply-templates mode="diseq" select="*[6]">
440 <xsl:with-param name="rel" select="'lt'"/>
441 </xsl:apply-templates>
442 <xsl:apply-templates mode="noannot" select="*[4]"/>
446 <xsl:when test="CONST[
447 attribute::uri='cic:/Coq/Init/Logic/Equality/eq_ind.con' or
448 attribute::uri='cic:/Coq/Init/Logic/Logic_lemmas/eq_ind_r.con' or
449 attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
450 attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind_r.con' or
451 attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) = 7">
453 <m:csymbol>rw_step</m:csymbol>
454 <xsl:apply-templates mode="noannot" select="*[5]"/>
455 <xsl:apply-templates mode="pure" select="*[3]"/>
456 <xsl:apply-templates mode="pure" select="*[6]"/>
457 <xsl:call-template name="generate_side_proof">
458 <xsl:with-param name="proof" select="*[7]"/>
460 <!-- <xsl:apply-templates mode="proof_transform" select="*[7]"/> -->
463 <!-- EQUALITY with extra-parameters -->
464 <xsl:when test="CONST[
465 attribute::uri='cic:/Coq/Init/Logic/Equality/eq_ind.con' or
466 attribute::uri='cic:/Coq/Init/Logic/Logic_lemmas/eq_ind_r.con' or
467 attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
468 attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind_r.con' or
469 attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) > 7">
470 <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')])"/>
472 <xsl:when test="$no_extraproofs=0">
474 <m:csymbol>rewrite_and_apply</m:csymbol>
476 <m:csymbol>rw_step</m:csymbol>
477 <xsl:apply-templates mode="noannot" select="*[5]"/>
478 <xsl:apply-templates mode="pure" select="*[3]"/>
479 <xsl:apply-templates mode="pure" select="*[6]"/>
480 <xsl:call-template name="generate_side_proof">
481 <xsl:with-param name="proof" select="*[7]"/>
483 <!-- <xsl:apply-templates mode="pure" select="*[7]"/> -->
485 <xsl:apply-templates mode="noannot" select="*[position()>7]"/>
490 <xsl:when test="*[5]/@sort='Prop'">
491 <m:apply helm:xref="{@id}">
492 <m:csymbol>letin</m:csymbol>
494 <m:csymbol>let</m:csymbol>
496 <xsl:call-template name="insert_subscript">
497 <xsl:with-param name="node_value" select="'h1'"/>
500 <xsl:apply-templates mode="noannot" select="*[5]"/>
502 <xsl:call-template name="gen_let">
503 <xsl:with-param name="init_pos" select="1"/>
504 <xsl:with-param name="from" select="7"/>
507 <m:csymbol>rewrite_and_apply</m:csymbol>
509 <m:csymbol>rw_step</m:csymbol>
511 <xsl:call-template name="insert_subscript">
512 <xsl:with-param name="node_value" select="'h1'"/>
515 <xsl:apply-templates mode="pure" select="*[3]"/>
516 <xsl:apply-templates mode="pure" select="*[6]"/>
517 <xsl:call-template name="generate_side_proof">
518 <xsl:with-param name="proof" select="*[7]"/>
520 <!-- <xsl:apply-templates mode="pure" select="*[7]"/> -->
522 <xsl:apply-templates mode="flat" select="*[8]">
523 <xsl:with-param name="n">
524 <xsl:value-of select="2"/>
526 </xsl:apply-templates>
531 <m:apply helm:xref="{@id}">
532 <m:csymbol>letin</m:csymbol>
533 <xsl:call-template name="gen_let">
534 <xsl:with-param name="init_pos" select="0"/>
535 <xsl:with-param name="form" select="7"/>
538 <m:csymbol>rewrite_and_apply</m:csymbol>
540 <m:csymbol>rw_step</m:csymbol>
541 <xsl:apply-templates mode="pure" select="*[5]"/>
542 <xsl:apply-templates mode="pure" select="*[3]"/>
543 <xsl:apply-templates mode="pure" select="*[6]"/>
544 <xsl:call-template name="generate_side_proof">
545 <xsl:with-param name="proof" select="*[7]"/>
547 <!-- <xsl:apply-templates mode="pure" select="*[7]"/> -->
549 <xsl:apply-templates mode="flat" select="*[8]">
550 <xsl:with-param name="n">
551 <xsl:value-of select="1"/>
553 </xsl:apply-templates>
562 <xsl:when test="CONST[
563 attribute::uri='cic:/Coq/Init/Logic/False_ind.con'] and
564 count(child::*) = 3">
565 <m:apply helm:xref="{@id}">
566 <m:csymbol>false_ind</m:csymbol>
567 <m:ci>cic:/Coq/Init/Logic/False_ind.con</m:ci>
568 <xsl:apply-templates mode="noannot" select="*[3]"/>
571 <!-- gestire meglio il caso di and_ind quando la prova
572 non e' della forma \x.\y.M -->
573 <xsl:when test="CONST[
574 attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con']
575 and count(child::*) = 6
576 and name(*[5])='LAMBDA'
577 and name(*[5]/target/*[1])='LAMBDA'">
578 <m:apply helm:xref="{@id}">
579 <m:csymbol>and_ind</m:csymbol>
580 <xsl:apply-templates mode="noannot" select="*[6]"/>
581 <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>
582 <xsl:apply-templates mode="pure" select="*[5]/source/*"/>
583 <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>
584 <xsl:apply-templates mode="pure" select="*[5]/target/LAMBDA/source/*"/>
585 <xsl:apply-templates mode="proof_transform" select="*[5]/target/LAMBDA/target/*"/>
588 <xsl:when test="CONST[
589 attribute::uri='cic:/Coq/Init/Logic/Disjunction/or_ind.con']
590 and count(child::*) = 7">
592 <xsl:when test="name(*[5])='LAMBDA'
593 and name(*[6])='LAMBDA'">
594 <xsl:variable name="definition_url"
595 select="'cic:/Coq/Init/Logic/Disjunction/or.ind'"/>
596 <m:apply helm:xref="{@id}">
597 <m:csymbol>full_or_ind</m:csymbol>
598 <xsl:apply-templates mode="noannot" select="*[7]"/>
599 <xsl:apply-templates mode="pure"
600 select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
602 <m:csymbol>left_case</m:csymbol>
605 <xsl:value-of select="*[5]/target/@binder"/>
608 <xsl:apply-templates mode="pure" select="*[5]/source/*[1]"/>
611 <xsl:apply-templates mode="noannot" select="*[5]/target/*[1]"/>
614 <m:csymbol>right_case</m:csymbol>
617 <xsl:apply-templates mode="pure" select="*[6]/target/@binder"/>
620 <xsl:apply-templates mode="pure" select="*[6]/source/*[1]"/>
623 <xsl:apply-templates mode="noannot" select="*[6]/target/*[1]"/>
628 <m:apply helm:xref="{@id}">
629 <m:csymbol>or_ind</m:csymbol>
630 <xsl:apply-templates mode="noannot" select="*[7]"/>
631 <xsl:apply-templates mode="pure"
632 select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
633 <xsl:apply-templates mode="pure" select="*[5]"/>
634 <xsl:apply-templates mode="pure" select="*[6]"/>
639 <!-- ex_ind, exT_ind -->
640 <xsl:when test="(CONST[attribute::uri='cic:/Coq/Init/Logic_Type/exT_ind.con'] or
641 CONST[attribute::uri='cic:/Coq/Init/Logic/First_order_quantifiers/ex_ind.con'])
642 and count(child::*) = 6
643 and name(*[5])='LAMBDA'
644 and name(*[5]/target/*[1])='LAMBDA'">
645 <m:apply helm:xref="{@id}">
646 <m:csymbol>ex_ind</m:csymbol>
647 <xsl:apply-templates mode="noannot" select="*[6]"/>
648 <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>
649 <xsl:apply-templates mode="pure" select="*[5]/source/*"/>
650 <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>
651 <xsl:apply-templates mode="pure" select="*[5]/target/LAMBDA/source/*"/>
652 <xsl:apply-templates mode="proof_transform" select="*[5]/target/LAMBDA/target/*"/>
655 <xsl:when test="name(*[1])='CONST'">
656 <xsl:apply-templates mode="try_inductive" select="."/>
658 <!-- patch temporanea per la gestione di redex -->
659 <xsl:when test="name(*[1])='LAMBDA' and count(child::*)=2
660 and *[2]/@sort='Prop'">
661 <m:apply helm:xref="{@id}">
662 <m:csymbol>letin</m:csymbol>
664 <m:csymbol>let</m:csymbol>
666 <xsl:call-template name="insert_subscript">
667 <xsl:with-param name="node_value">
668 <xsl:value-of select="*[1]/target/@binder"/>
672 <xsl:apply-templates mode="noannot" select="*[2]"/>
674 <xsl:apply-templates mode="proof_transform" select="*[1]/target/*[1]"/>
678 <xsl:apply-templates select="." mode="letin"/>
682 <xsl:when test="name()='LAMBDA'">
684 <xsl:when test="(name(target/*[1])='APPLY' and
685 name(target/*[1]/*[1])='CONST' and
686 (target/*[1]/*[1]/@uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
687 target/*[1]/*[1]/@uri='cic:/Coq/Init/Logic_Type/eqT_ind_r.con' or
688 target/*[1]/*[1]/@uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con')
689 and count(target/*[1]/*) = 8
690 and name(target/*[1]/*[8])='REL'
691 and target/@binder = target/*[1]/*[8]/@binder )">
693 <m:csymbol>rw_step</m:csymbol>
694 <xsl:apply-templates mode="noannot" select="target/*[1]/*[5]"/>
695 <xsl:apply-templates mode="pure" select="target/*[1]/*[3]"/>
696 <xsl:apply-templates mode="pure" select="target/*[1]/*[6]"/>
697 <xsl:call-template name="generate_side_proof">
698 <xsl:with-param name="proof" select="target/*[1]/*[7]"/>
700 <!-- <xsl:apply-templates mode="proof_transform" select="target/*[1]/*[7]"/> -->
704 <xsl:apply-templates mode="pure" select="."/>
709 <xsl:apply-templates select="." mode="pure"/>
714 <xsl:template name="is_simple">
715 <xsl:param name="proof" select="/.."/>
716 <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))"/>
719 <xsl:template name="generate_side_proof">
720 <xsl:param name="proof" select="/.."/>
721 <xsl:param name="show_statement" select="1"/>
723 <xsl:variable name="is_simple">
724 <xsl:call-template name="is_simple">
725 <xsl:with-param name="proof" select="$proof"/>
728 <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))"/>
730 <xsl:when test="$is_simple">
732 <xsl:when test="name($proof)='APPLY'">
733 <xsl:apply-templates select="$proof" mode="letin"/>
736 <xsl:apply-templates select="$proof" mode="pure"/>
741 <xsl:variable name="id" select="@id"/>
742 <m:apply helm:xref="{@id}">
744 <xsl:when test="$show_statement = 1">
745 <m:csymbol>proof</m:csymbol>
748 <m:csymbol>side_proof</m:csymbol>
751 <xsl:apply-templates mode="proof_transform" select="$proof"/>
752 <xsl:apply-templates mode="pure" select="$InnerTypes/InnerTypes/TYPE[@of=$proof/@id]/*"/>
754 <!-- <xsl:apply-templates select="$proof" mode="noannot"/> -->
759 <xsl:variable name="no_subproofs" select="count(*[@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')])"/>
761 <xsl:template match="APPLY" mode="letin">
762 <xsl:variable name="no_subproofs" select="count(*[@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')])"/>
763 <!-- <m:cn><xsl:value-of select="$no_subproofs"/></m:cn> -->
765 <xsl:when test="$naturalLanguage='yes' and ($no_subproofs = 1)">
766 <m:apply helm:xref="{@id}">
767 <m:csymbol>letin1</m:csymbol>
768 <xsl:apply-templates mode="noannot" select="*[@sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')]"/>
769 <!-- now re-process the application -->
770 <m:apply helm:xref="{@id}">
771 <m:csymbol>app</m:csymbol>
772 <!-- mode previous looks for siblings:
773 call with the first child -->
774 <xsl:apply-templates mode="previous" select="*[1]"/>
778 <xsl:when test="$naturalLanguage='yes' and ($no_subproofs > 1)">
779 <m:apply helm:xref="{@id}">
780 <m:csymbol>letin</m:csymbol>
781 <!-- first process all subproofs (let-in) -->
782 <xsl:call-template name="gen_let"/>
783 <!-- now re-process the application -->
784 <m:apply helm:xref="{@id}">
785 <m:csymbol>app</m:csymbol>
786 <!-- mode flat looks for siblings: call with the first child -->
787 <xsl:apply-templates mode="flat" select="*[1]"/>
793 <xsl:when test="@sort='Prop'">
795 <m:csymbol>app</m:csymbol>
796 <xsl:apply-templates mode="erase" select="*[1]"/>
800 <xsl:apply-templates mode="pure" select="."/>
807 <xsl:template name="gen_let">
808 <xsl:param name="init_pos" select="0"/>
809 <xsl:param name="from" select="0"/>
810 <xsl:for-each select="*[position()>$from and @sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')]">
812 <m:csymbol>let</m:csymbol>
813 <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>
814 <xsl:apply-templates mode="noannot" select="."/>
819 <xsl:template match="*" mode="erase">
821 <xsl:when test="@sort='Prop' or $naturalLanguage='no'">
822 <xsl:apply-templates mode="pure" select="."/>
828 <xsl:apply-templates mode="erase" select="following-sibling::*[1]"/>
831 <xsl:template match="*" mode="previous">
833 <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')">
834 <m:ci>previous</m:ci>
837 <!-- forse bisognerebbe trattare solo l'elemento di testa -->
839 <xsl:when test="@sort='Prop' or $naturalLanguage='no'">
840 <xsl:apply-templates mode="pure" select="."/>
846 <!-- <xsl:apply-templates select="." mode="pure"/> -->
849 <xsl:apply-templates mode="previous" select="following-sibling::*[1]"/>
852 <xsl:template match="*" mode="flat">
853 <xsl:param name="n" select="1"/>
854 <xsl:variable name="id" select="@id"/>
856 <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')">
858 <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>
860 <xsl:apply-templates mode="flat" select="following-sibling::*[1]">
861 <xsl:with-param name="n" select="$n+1"/>
862 </xsl:apply-templates>
866 <xsl:when test="name()='REL' or @sort='Prop' or $naturalLanguage='no'">
867 <xsl:apply-templates mode="pure" select="."/>
873 <!-- <xsl:apply-templates mode="pure" select="."/> -->
874 <xsl:apply-templates mode="flat" select="following-sibling::*[1]">
875 <xsl:with-param name="n" select="$n"/>
876 </xsl:apply-templates>
881 <!-- Auxiliary functions -->
882 <!-- OMDOC: now we have name_of_uri generalized on the extension that -->
883 <!-- can replace the next template -->
884 <xsl:template name="get_name">
885 <xsl:param name="uri" select="''"/>
886 <xsl:variable name="sub_after" select="substring-after($uri,'/')"/>
888 <xsl:when test="contains($sub_after,'/')">
889 <xsl:call-template name="get_name">
890 <xsl:with-param name="uri" select="$sub_after"/>
894 <xsl:value-of select="substring-before($sub_after,'_ind.con')"/>
899 <!-- <xsl:template match="APPLY[CONST[
900 attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con']]" mode="appflat">
902 <xsl:when test="count(child::*) > 4">
903 <m:apply helm:xref="{@id}">
904 <m:csymbol>app</m:csymbol>
905 <xsl:apply-templates mode="pure" select="*[1]"/>
909 <xsl:apply-templates mode="flat" select="*[5]"/>
913 <m:apply helm:xref="{@id}">
914 <m:csymbol>app</m:csymbol>
915 <xsl:apply-templates mode="flat" select="*[1]"/>