helm/style/proofs.xsl

   1 <?xml version="1.0"?>
   2
   3 <!-- Copyright (C) 2000, HELM Team                                     -->
   4 <!--                                                                   -->
   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.                         -->
   8 <!--                                                                   -->
   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.            -->
  13 <!--                                                                   -->
  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.                      -->
  18 <!--                                                                   -->
  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.                                              -->
  23 <!--                                                                   -->
  24 <!-- For details, see the HELM World-Wide-Web page,                    -->
  25 <!-- http://cs.unibo.it/helm/.                                         -->
  26
  27 <!--******************************************************************-->
  28 <!-- Basic Logic                                                      -->
  29 <!-- (completely) Revisited: february 2001, Andrea Asperti            -->
  30 <!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena                 -->
  31 <!--******************************************************************-->
  32
  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">
  36
  37 <!-- ************************* LOGIC *********************************-->
  38
  39 <!-- Proof objects -->
  40
  41 <!-- <xsl:key name="typeid" use="@of" match="TYPE"/> -->
  42
  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"/>
  46 </xsl:template>
  47
  48 <!-- ALL ELEMENTS WITH A TYPE ARE TRANSLATED AS A PROOF-ELEMENT -->
  49
  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"/>
  53  <xsl:choose>
  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]/*"/>
  59    </m:apply>
  60   </xsl:when>
  61   <xsl:otherwise>
  62    <xsl:apply-templates select="." mode="pure"/>
  63   </xsl:otherwise>
  64  </xsl:choose>
  65 </xsl:template>
  66
  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"/>
  70  <xsl:choose>
  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]/*"/>
  77    </m:apply>
  78   </xsl:when>
  79   <xsl:otherwise>
  80    <xsl:choose>
  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"/>
  86     </xsl:when>
  87     <xsl:otherwise>
  88      <xsl:apply-templates select="." mode="pure"/>
  89     </xsl:otherwise>
  90    </xsl:choose>
  91   </xsl:otherwise>
  92  </xsl:choose>
  93 </xsl:template>
  94
  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 -->
 104
 105 <xsl:template mode="try_inductive" match="APPLY">
 106    <xsl:variable name="id" select="@id"/>
 107    <xsl:choose>
 108     <xsl:when test="CONST[1]">
 109      <xsl:variable name="uri" select="CONST[1]/@uri"/>
 110      <xsl:choose>
 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
 118             exists -->
 119        <xsl:choose>
 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"/>
 124           </xsl:call-template>
 125          </xsl:variable>
 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"/>
 130           </xsl:call-template>
 131          </xsl:variable>
 132          <xsl:apply-templates mode="inductive" select=".">
 133           <xsl:with-param name="inductive_def_uri"
 134            select="$ind_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>
 141         </xsl:when>
 142         <xsl:otherwise>
 143          <xsl:apply-templates mode="letin" select="."/>
 144         </xsl:otherwise>
 145        </xsl:choose>
 146       </xsl:when>
 147       <xsl:otherwise>
 148        <xsl:apply-templates mode="letin" select="."/>
 149       </xsl:otherwise>
 150      </xsl:choose>
 151     </xsl:when>
 152     <xsl:otherwise>
 153      <xsl:apply-templates mode="letin" select="."/>
 154     </xsl:otherwise>
 155    </xsl:choose>
 156 </xsl:template>
 157
 158 <xsl:template mode="eq_transitive" match="*">
 159  <!-- <m:ci>eccomi-1: <xsl:value-of select="name()"/></m:ci> -->
 160  <xsl:choose>
 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"/>
 164    <xsl:choose>
 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]"/>
 171     </xsl:when>
 172     <xsl:otherwise>
 173      <xsl:call-template name="generate_side_proof">
 174       <xsl:with-param name="proof" select="."/>
 175       <xsl:with-param name="show_statement" select="0"/>
 176      </xsl:call-template>
 177     </xsl:otherwise>
 178    </xsl:choose>
 179   </xsl:when>
 180   <xsl:otherwise>
 181    <xsl:call-template name="generate_side_proof">
 182     <xsl:with-param name="proof" select="."/>
 183     <xsl:with-param name="show_statement" select="0"/>
 184    </xsl:call-template>
 185   </xsl:otherwise>
 186  </xsl:choose>
 187 </xsl:template>
 188
 189 <xsl:template mode="proof_transform" match="*">
 190  <xsl:choose>
 191   <xsl:when test="name()='APPLY'">
 192    <xsl:variable name="id" select="@id"/>
 193    <xsl:choose>
 194     <!-- Algebra equality (eq_transitive_unfolded) -->
 195     <!-- It requires a special mode "eq_transitive"-->
 196     <!-- togliere il parametro -->
 197     <xsl:when test="CONST[attribute::uri='cic:/Algebra/CSetoids/CSetoid_basics/eq_transitive_unfolded.con'] and count(child::*) = 7">
 198      <m:apply>
 199        <m:csymbol>eq_chain</m:csymbol>
 200        <xsl:apply-templates mode="noannot" select="*[3]"/>
 201        <xsl:apply-templates mode="eq_transitive" select="*[6]"/>
 202        <xsl:apply-templates mode="noannot" select="*[4]"/>
 203        <xsl:apply-templates mode="eq_transitive" select="*[7]"/>
 204        <xsl:apply-templates mode="noannot" select="*[5]"/>
 205      </m:apply>
 206     </xsl:when>
 207     <!-- EQUALITY -->
 208     <xsl:when test="CONST[
 209  attribute::uri='cic:/Coq/Init/Logic/Equality/eq_ind.con' or
 210  attribute::uri='cic:/Coq/Init/Logic/Logic_lemmas/eq_ind_r.con' or
 211  attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
 212  attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind_r.con' or
 213  attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) = 7">
 214       <m:apply>
 215        <m:csymbol>rw_step</m:csymbol>
 216        <xsl:apply-templates mode="noannot" select="*[5]"/>
 217        <xsl:apply-templates mode="pure" select="*[3]"/>
 218        <xsl:apply-templates mode="pure" select="*[6]"/>
 219        <xsl:call-template name="generate_side_proof">
 220         <xsl:with-param name="proof" select="*[7]"/>
 221        </xsl:call-template>
 222        <!-- <xsl:apply-templates mode="proof_transform" select="*[7]"/> -->
 223       </m:apply>
 224     </xsl:when>
 225     <!-- EQUALITY with extra-parameters -->
 226     <xsl:when test="CONST[
 227  attribute::uri='cic:/Coq/Init/Logic/Equality/eq_ind.con' or
 228  attribute::uri='cic:/Coq/Init/Logic/Logic_lemmas/eq_ind_r.con' or
 229  attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
 230  attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind_r.con' or
 231  attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) > 7">
 232       <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')])"/>
 233       <xsl:choose>
 234        <xsl:when test="$no_extraproofs=0">
 235         <m:apply>
 236          <m:csymbol>rewrite_and_apply</m:csymbol>
 237          <m:apply>
 238           <m:csymbol>rw_step</m:csymbol>
 239           <xsl:apply-templates mode="noannot" select="*[5]"/>
 240           <xsl:apply-templates mode="pure" select="*[3]"/>
 241           <xsl:apply-templates mode="pure" select="*[6]"/>
 242           <xsl:call-template name="generate_side_proof">
 243            <xsl:with-param name="proof" select="*[7]"/>
 244            </xsl:call-template>
 245           <!-- <xsl:apply-templates mode="pure" select="*[7]"/> -->
 246          </m:apply>
 247          <xsl:apply-templates mode="noannot" select="*[position()>7]"/>
 248         </m:apply>
 249        </xsl:when>
 250        <xsl:otherwise>
 251         <xsl:choose>
 252          <xsl:when test="*[5]/@sort='Prop'">
 253           <m:apply helm:xref="{@id}">
 254            <m:csymbol>letin</m:csymbol>
 255            <m:apply>
 256             <m:csymbol>let</m:csymbol>
 257             <m:ci>
 258              <xsl:call-template name="insert_subscript">
 259               <xsl:with-param name="node_value" select="'h1'"/>
 260              </xsl:call-template>
 261             </m:ci>
 262             <xsl:apply-templates mode="noannot" select="*[5]"/>
 263            </m:apply>
 264            <xsl:call-template name="gen_let">
 265             <xsl:with-param name="init_pos" select="1"/>
 266             <xsl:with-param name="from" select="7"/>
 267            </xsl:call-template>
 268            <m:apply>
 269             <m:csymbol>rewrite_and_apply</m:csymbol>
 270             <m:apply>
 271              <m:csymbol>rw_step</m:csymbol>
 272              <m:ci>
 273               <xsl:call-template name="insert_subscript">
 274                <xsl:with-param name="node_value" select="'h1'"/>
 275               </xsl:call-template>
 276              </m:ci>
 277              <xsl:apply-templates mode="pure" select="*[3]"/>
 278              <xsl:apply-templates mode="pure" select="*[6]"/>
 279              <xsl:call-template name="generate_side_proof">
 280               <xsl:with-param name="proof" select="*[7]"/>
 281              </xsl:call-template>
 282              <!-- <xsl:apply-templates mode="pure" select="*[7]"/> -->
 283             </m:apply>
 284             <xsl:apply-templates mode="flat" select="*[8]">
 285              <xsl:with-param name="n">
 286               <xsl:value-of select="2"/>
 287              </xsl:with-param>
 288             </xsl:apply-templates>
 289            </m:apply>
 290           </m:apply>
 291          </xsl:when>
 292          <xsl:otherwise>
 293           <m:apply helm:xref="{@id}">
 294            <m:csymbol>letin</m:csymbol>
 295            <xsl:call-template name="gen_let">
 296             <xsl:with-param name="init_pos" select="0"/>
 297             <xsl:with-param name="form" select="7"/>
 298            </xsl:call-template>
 299            <m:apply>
 300             <m:csymbol>rewrite_and_apply</m:csymbol>
 301             <m:apply>
 302              <m:csymbol>rw_step</m:csymbol>
 303              <xsl:apply-templates mode="pure" select="*[5]"/>
 304              <xsl:apply-templates mode="pure" select="*[3]"/>
 305              <xsl:apply-templates mode="pure" select="*[6]"/>
 306              <xsl:call-template name="generate_side_proof">
 307               <xsl:with-param name="proof" select="*[7]"/>
 308              </xsl:call-template>
 309              <!-- <xsl:apply-templates mode="pure" select="*[7]"/> -->
 310             </m:apply>
 311             <xsl:apply-templates mode="flat" select="*[8]">
 312              <xsl:with-param name="n">
 313               <xsl:value-of select="1"/>
 314              </xsl:with-param>
 315             </xsl:apply-templates>
 316            </m:apply>
 317           </m:apply>
 318          </xsl:otherwise>
 319         </xsl:choose>
 320        </xsl:otherwise>
 321       </xsl:choose>
 322     </xsl:when>
 323     <!-- False_ind -->
 324     <xsl:when test="CONST[
 325      attribute::uri='cic:/Coq/Init/Logic/False_ind.con'] and
 326      count(child::*) = 3">
 327      <m:apply helm:xref="{@id}">
 328        <m:csymbol>false_ind</m:csymbol>
 329        <m:ci>cic:/Coq/Init/Logic/False_ind.con</m:ci>
 330        <xsl:apply-templates mode="noannot" select="*[3]"/>
 331      </m:apply>
 332     </xsl:when>
 333     <!-- gestire meglio il caso di and_ind quando la prova
 334          non e' della forma \x.\y.M -->
 335     <xsl:when test="CONST[
 336  attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con']
 337  and count(child::*) = 6
 338  and name(*[5])='LAMBDA'
 339  and name(*[5]/target/*[1])='LAMBDA'">
 340       <m:apply helm:xref="{@id}">
 341        <m:csymbol>and_ind</m:csymbol>
 342        <xsl:apply-templates mode="noannot" select="*[6]"/>
 343        <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>
 344        <xsl:apply-templates mode="pure" select="*[5]/source/*"/>
 345        <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>
 346        <xsl:apply-templates mode="pure" select="*[5]/target/LAMBDA/source/*"/>
 347        <xsl:apply-templates mode="proof_transform" select="*[5]/target/LAMBDA/target/*"/>
 348       </m:apply>
 349     </xsl:when>
 350     <xsl:when test="CONST[
 351  attribute::uri='cic:/Coq/Init/Logic/Disjunction/or_ind.con']
 352  and count(child::*) = 7">
 353       <xsl:choose>
 354        <xsl:when test="name(*[5])='LAMBDA'
 355                  and name(*[6])='LAMBDA'">
 356         <xsl:variable name="definition_url"
 357             select="'cic:/Coq/Init/Logic/Disjunction/or.ind'"/>
 358         <m:apply helm:xref="{@id}">
 359          <m:csymbol>full_or_ind</m:csymbol>
 360          <xsl:apply-templates mode="noannot" select="*[7]"/>
 361          <xsl:apply-templates mode="pure"
 362               select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
 363          <m:apply>
 364           <m:csymbol>left_case</m:csymbol>
 365           <m:bvar>
 366            <m:ci>
 367             <xsl:value-of select="*[5]/target/@binder"/>
 368            </m:ci>
 369            <m:type>
 370             <xsl:apply-templates mode="pure" select="*[5]/source/*[1]"/>
 371            </m:type>
 372           </m:bvar>
 373           <xsl:apply-templates mode="noannot" select="*[5]/target/*[1]"/>
 374          </m:apply>
 375          <m:apply>
 376           <m:csymbol>right_case</m:csymbol>
 377           <m:bvar>
 378            <m:ci>
 379             <xsl:apply-templates mode="pure" select="*[6]/target/@binder"/>
 380            </m:ci>
 381            <m:type>
 382             <xsl:apply-templates mode="pure" select="*[6]/source/*[1]"/>
 383            </m:type>
 384           </m:bvar>
 385           <xsl:apply-templates mode="noannot" select="*[6]/target/*[1]"/>
 386          </m:apply>
 387         </m:apply>
 388        </xsl:when>
 389        <xsl:otherwise>
 390         <m:apply helm:xref="{@id}">
 391          <m:csymbol>or_ind</m:csymbol>
 392          <xsl:apply-templates mode="noannot" select="*[7]"/>
 393          <xsl:apply-templates mode="pure"
 394               select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
 395          <xsl:apply-templates mode="pure" select="*[5]"/>
 396          <xsl:apply-templates mode="pure" select="*[6]"/>
 397         </m:apply>
 398        </xsl:otherwise>
 399       </xsl:choose>
 400     </xsl:when>
 401     <!-- ex_ind, exT_ind -->
 402       <xsl:when test="(CONST[attribute::uri='cic:/Coq/Init/Logic_Type/exT_ind.con'] or
 403       CONST[attribute::uri='cic:/Coq/Init/Logic/First_order_quantifiers/ex_ind.con'])
 404  and count(child::*) = 6
 405  and name(*[5])='LAMBDA'
 406  and name(*[5]/target/*[1])='LAMBDA'">
 407       <m:apply helm:xref="{@id}">
 408        <m:csymbol>ex_ind</m:csymbol>
 409        <xsl:apply-templates mode="noannot" select="*[6]"/>
 410        <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>
 411        <xsl:apply-templates mode="pure" select="*[5]/source/*"/>
 412        <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>
 413        <xsl:apply-templates mode="pure" select="*[5]/target/LAMBDA/source/*"/>
 414        <xsl:apply-templates mode="proof_transform" select="*[5]/target/LAMBDA/target/*"/>
 415       </m:apply>
 416     </xsl:when>
 417     <xsl:when test="name(*[1])='CONST'">
 418      <xsl:apply-templates mode="try_inductive" select="."/>
 419     </xsl:when>
 420     <!-- patch temporanea per la gestione di redex -->
 421     <xsl:when test="name(*[1])='LAMBDA' and count(child::*)=2
 422          and *[2]/@sort='Prop'">
 423      <m:apply helm:xref="{@id}">
 424       <m:csymbol>letin</m:csymbol>
 425       <m:apply>
 426        <m:csymbol>let</m:csymbol>
 427        <m:ci>
 428         <xsl:call-template name="insert_subscript">
 429          <xsl:with-param name="node_value">
 430           <xsl:value-of select="*[1]/target/@binder"/>
 431          </xsl:with-param>
 432         </xsl:call-template>
 433        </m:ci>
 434        <xsl:apply-templates mode="noannot" select="*[2]"/>
 435       </m:apply>
 436       <xsl:apply-templates mode="proof_transform" select="*[1]/target/*[1]"/>
 437      </m:apply>
 438     </xsl:when>
 439     <xsl:otherwise>
 440      <xsl:apply-templates select="." mode="letin"/>
 441     </xsl:otherwise>
 442    </xsl:choose>
 443   </xsl:when>
 444   <xsl:when test="name()='LAMBDA'">
 445    <xsl:choose>
 446      <xsl:when test="(name(target/*[1])='APPLY'  and
 447       name(target/*[1]/*[1])='CONST' and
 448       (target/*[1]/*[1]/@uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
 449        target/*[1]/*[1]/@uri='cic:/Coq/Init/Logic_Type/eqT_ind_r.con' or
 450        target/*[1]/*[1]/@uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con')
 451       and count(target/*[1]/*) = 8
 452       and name(target/*[1]/*[8])='REL'
 453       and target/@binder = target/*[1]/*[8]/@binder )">
 454       <m:apply>
 455        <m:csymbol>rw_step</m:csymbol>
 456        <xsl:apply-templates mode="noannot" select="target/*[1]/*[5]"/>
 457        <xsl:apply-templates mode="pure" select="target/*[1]/*[3]"/>
 458        <xsl:apply-templates mode="pure" select="target/*[1]/*[6]"/>
 459        <xsl:call-template name="generate_side_proof">
 460         <xsl:with-param name="proof" select="target/*[1]/*[7]"/>
 461        </xsl:call-template>
 462        <!-- <xsl:apply-templates mode="proof_transform" select="target/*[1]/*[7]"/> -->
 463       </m:apply>
 464      </xsl:when>
 465      <xsl:otherwise>
 466       <xsl:apply-templates mode="pure" select="."/>
 467      </xsl:otherwise>
 468     </xsl:choose>
 469    </xsl:when>
 470   <xsl:otherwise>
 471    <xsl:apply-templates select="." mode="pure"/>
 472   </xsl:otherwise>
 473  </xsl:choose>
 474 </xsl:template>
 475
 476 <xsl:template name="is_simple">
 477  <xsl:param name="proof" select="/.."/>
 478  <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))"/>
 479 </xsl:template>
 480
 481 <xsl:template name="generate_side_proof">
 482  <xsl:param name="proof" select="/.."/>
 483  <xsl:param name="show_statement" select="1"/>
 484 <!--
 485  <xsl:variable name="is_simple">
 486   <xsl:call-template name="is_simple">
 487    <xsl:with-param name="proof" select="$proof"/>
 488   </xsl:call-template>
 489  </xsl:variable> -->
 490 <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))"/>
 491  <xsl:choose>
 492   <xsl:when test="$is_simple">
 493    <xsl:choose>
 494     <xsl:when test="name($proof)='APPLY'">
 495      <xsl:apply-templates select="$proof" mode="letin"/>
 496     </xsl:when>
 497     <xsl:otherwise>
 498      <xsl:apply-templates select="$proof" mode="pure"/>
 499     </xsl:otherwise>
 500    </xsl:choose>
 501   </xsl:when>
 502   <xsl:otherwise>
 503    <xsl:variable name="id" select="@id"/>
 504    <m:apply helm:xref="{@id}">
 505     <xsl:choose>
 506      <xsl:when test="$show_statement = 1">
 507       <m:csymbol>proof</m:csymbol>
 508      </xsl:when>
 509      <xsl:otherwise>
 510       <m:csymbol>side_proof</m:csymbol>
 511      </xsl:otherwise>
 512     </xsl:choose>
 513     <xsl:apply-templates mode="proof_transform" select="$proof"/>
 514     <xsl:apply-templates mode="pure" select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
 515    </m:apply>
 516    <!-- <xsl:apply-templates select="$proof" mode="noannot"/> -->
 517   </xsl:otherwise>
 518  </xsl:choose>
 519 </xsl:template>
 520
 521 <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')])"/>
 522
 523 <xsl:template match="APPLY" mode="letin">
 524    <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')])"/>
 525    <!-- <m:cn><xsl:value-of select="$no_subproofs"/></m:cn> -->
 526    <xsl:choose>
 527     <xsl:when test="$naturalLanguage='yes' and ($no_subproofs = 1)">
 528      <m:apply helm:xref="{@id}">
 529       <m:csymbol>letin1</m:csymbol>
 530       <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')]"/>
 531       <!-- now re-process the application -->
 532       <m:apply helm:xref="{@id}">
 533        <m:csymbol>app</m:csymbol>
 534        <!-- mode previous looks for siblings:
 535             call with the first child -->
 536        <xsl:apply-templates mode="previous" select="*[1]"/>
 537       </m:apply>
 538      </m:apply>
 539     </xsl:when>
 540     <xsl:when test="$naturalLanguage='yes' and ($no_subproofs > 1)">
 541      <m:apply helm:xref="{@id}">
 542       <m:csymbol>letin</m:csymbol>
 543       <!-- first process all subproofs (let-in) -->
 544       <xsl:call-template name="gen_let"/>
 545       <!-- now re-process the application  -->
 546       <m:apply helm:xref="{@id}">
 547        <m:csymbol>app</m:csymbol>
 548        <!-- mode flat looks for siblings: call with the first child -->
 549        <xsl:apply-templates mode="flat" select="*[1]"/>
 550       </m:apply>
 551      </m:apply>
 552     </xsl:when>
 553     <xsl:otherwise>
 554      <xsl:choose>
 555      <xsl:when test="@sort='Prop'">
 556       <m:apply>
 557        <m:csymbol>app</m:csymbol>
 558        <xsl:apply-templates mode="erase" select="*[1]"/>
 559       </m:apply>
 560      </xsl:when>
 561      <xsl:otherwise>
 562       <xsl:apply-templates mode="pure" select="."/>
 563      </xsl:otherwise>
 564      </xsl:choose>
 565     </xsl:otherwise>
 566    </xsl:choose>
 567 </xsl:template>
 568
 569 <xsl:template name="gen_let">
 570  <xsl:param name="init_pos" select="0"/>
 571  <xsl:param name="from" select="0"/>
 572       <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')]">
 573        <m:apply>
 574         <m:csymbol>let</m:csymbol>
 575         <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>
 576         <xsl:apply-templates mode="noannot" select="."/>
 577        </m:apply>
 578       </xsl:for-each>
 579 </xsl:template>
 580
 581 <xsl:template match="*" mode="erase">
 582   <xsl:choose>
 583    <xsl:when test="@sort='Prop' or $naturalLanguage='no'">
 584     <xsl:apply-templates mode="pure" select="."/>
 585    </xsl:when>
 586    <xsl:otherwise>
 587     <m:ci>.</m:ci>
 588    </xsl:otherwise>
 589    </xsl:choose>
 590  <xsl:apply-templates mode="erase" select="following-sibling::*[1]"/>
 591 </xsl:template>
 592
 593 <xsl:template match="*" mode="previous">
 594  <xsl:choose>
 595   <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')">
 596    <m:ci>previous</m:ci>
 597   </xsl:when>
 598   <xsl:otherwise>
 599    <!-- forse bisognerebbe trattare solo l'elemento di testa -->
 600    <xsl:choose>
 601    <xsl:when test="@sort='Prop' or $naturalLanguage='no'">
 602     <xsl:apply-templates mode="pure" select="."/>
 603    </xsl:when>
 604    <xsl:otherwise>
 605     <m:ci>.</m:ci>
 606    </xsl:otherwise>
 607    </xsl:choose>
 608    <!-- <xsl:apply-templates select="." mode="pure"/> -->
 609   </xsl:otherwise>
 610  </xsl:choose>
 611  <xsl:apply-templates mode="previous" select="following-sibling::*[1]"/>
 612 </xsl:template>
 613
 614 <xsl:template match="*" mode="flat">
 615  <xsl:param name="n" select="1"/>
 616  <xsl:variable name="id" select="@id"/>
 617  <xsl:choose>
 618   <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')">
 619    <m:ci>
 620     <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>
 621    </m:ci>
 622    <xsl:apply-templates mode="flat" select="following-sibling::*[1]">
 623     <xsl:with-param name="n" select="$n+1"/>
 624    </xsl:apply-templates>
 625   </xsl:when>
 626   <xsl:otherwise>
 627    <xsl:choose>
 628     <xsl:when test="name()='REL' or @sort='Prop' or $naturalLanguage='no'">
 629      <xsl:apply-templates mode="pure" select="."/>
 630     </xsl:when>
 631     <xsl:otherwise>
 632      <m:ci>.</m:ci>
 633     </xsl:otherwise>
 634    </xsl:choose>
 635    <!-- <xsl:apply-templates mode="pure" select="."/> -->
 636    <xsl:apply-templates mode="flat" select="following-sibling::*[1]">
 637     <xsl:with-param name="n" select="$n"/>
 638    </xsl:apply-templates>
 639   </xsl:otherwise>
 640  </xsl:choose>
 641 </xsl:template>
 642
 643 <!-- Auxiliary functions -->
 644 <!-- OMDOC: now we have name_of_uri generalized on the extension that -->
 645 <!-- can replace the next template                                    -->
 646 <xsl:template name="get_name">
 647  <xsl:param name="uri" select="''"/>
 648  <xsl:variable name="sub_after" select="substring-after($uri,'/')"/>
 649  <xsl:choose>
 650   <xsl:when test="contains($sub_after,'/')">
 651    <xsl:call-template name="get_name">
 652     <xsl:with-param name="uri" select="$sub_after"/>
 653    </xsl:call-template>
 654   </xsl:when>
 655   <xsl:otherwise>
 656    <xsl:value-of select="substring-before($sub_after,'_ind.con')"/>
 657   </xsl:otherwise>
 658  </xsl:choose>
 659 </xsl:template>
 660
 661 <!-- <xsl:template match="APPLY[CONST[
 662  attribute::uri='cic:/Coq/Init/Logic/Conjunction/and_ind.con']]" mode="appflat">
 663     <xsl:choose>
 664      <xsl:when test="count(child::*) > 4">
 665       <m:apply helm:xref="{@id}">
 666        <m:csymbol>app</m:csymbol>
 667        <xsl:apply-templates mode="pure" select="*[1]"/>
 668        <m:ci>*</m:ci>
 669        <m:ci>*</m:ci>
 670        <m:ci>*</m:ci>
 671        <xsl:apply-templates mode="flat" select="*[5]"/>
 672       </m:apply>
 673      </xsl:when>
 674      <xsl:otherwise>
 675       <m:apply helm:xref="{@id}">
 676        <m:csymbol>app</m:csymbol>
 677        <xsl:apply-templates mode="flat" select="*[1]"/>
 678       </m:apply>
 679      </xsl:otherwise>
 680     </xsl:choose>
 681 </xsl:template>  -->
 682
 683
 684 </xsl:stylesheet>