helm/style/logic.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: november 2002, 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 <xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Coq/Init/Logic/False_ind.con'] and count(child::*) = 3]">
  38  <xsl:variable name="id" select="@id"/>
  39  <m:apply helm:xref="{@id}">
  40   <m:csymbol>false_ind</m:csymbol>
  41   <m:ci>cic:/Coq/Init/Logic/False_ind.con</m:ci>
  42   <xsl:apply-templates mode="noannot" select="*[3]"/>
  43  </m:apply>
  44 </xsl:template>
  45
  46
  47 <xsl:template mode="proof_transform" match="APPLY[CONST[
  48  attribute::uri='cic:/Coq/Init/Logic/and_ind.con'] and
  49  count(child::*) = 6 and name(*[5])='LAMBDA' and
  50  count(*[5]/decl) >= 2]">
  51   <xsl:variable name="id" select="@id"/>
  52   <m:apply helm:xref="{@id}">
  53    <m:csymbol>and_ind</m:csymbol>
  54    <xsl:apply-templates mode="noannot" select="*[6]"/>
  55    <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/*[1]/@binder"/></xsl:with-param></xsl:call-template></m:ci>
  56    <xsl:apply-templates mode="pure" select="*[5]/*[1]/*"/>
  57    <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/*[2]/@binder"/></xsl:with-param></xsl:call-template></m:ci>
  58    <xsl:apply-templates mode="pure" select="*[5]/*[2]/*"/>
  59    <xsl:choose>
  60     <xsl:when test="count(*[5]/decl) = 2">
  61      <xsl:apply-templates mode="noannot" select="*[5]/target/*"/>
  62     </xsl:when>
  63     <xsl:otherwise>
  64      <xsl:apply-templates select="*[5]/*[3]" mode="lambda_prop"/>
  65     </xsl:otherwise>
  66    </xsl:choose>
  67   </m:apply>
  68 </xsl:template>
  69
  70 <xsl:template mode="proof_transform" match="APPLY[CONST[
  71  attribute::uri='cic:/Coq/Init/Logic/or_ind.con']
  72  and count(child::*) = 7 and
  73  name(*[5])='LAMBDA' and count(*[5]/decl) = 1 and
  74  name(*[6])='LAMBDA' and count(*[6]/decl) = 1 ]">
  75  <xsl:variable name="id" select="@id"/>
  76  <xsl:variable name="definition_url"
  77    select="'cic:/Coq/Init/Logic/Disjunction/or.ind'"/>
  78  <m:apply helm:xref="{@id}">
  79   <m:csymbol>full_or_ind</m:csymbol>
  80   <xsl:apply-templates mode="noannot" select="*[7]"/>
  81   <xsl:for-each select="$InnerTypes">
  82    <xsl:apply-templates mode="pure" select="key('typeid',$id)/*[1]"/>
  83   </xsl:for-each>
  84   <m:apply>
  85    <m:csymbol>left_case</m:csymbol>
  86    <m:bvar>
  87     <m:ci>
  88      <xsl:value-of select="*[5]/*[1]/@binder"/>
  89     </m:ci>
  90     <m:type>
  91      <xsl:apply-templates mode="pure" select="*[5]/*[1]/*"/>
  92     </m:type>
  93    </m:bvar>
  94    <xsl:apply-templates mode="noannot" select="*[5]/target/*"/>
  95   </m:apply>
  96   <m:apply>
  97    <m:csymbol>right_case</m:csymbol>
  98    <m:bvar>
  99     <m:ci>
 100      <xsl:apply-templates mode="pure" select="*[6]/*[1]/@binder"/>
 101     </m:ci>
 102     <m:type>
 103      <xsl:apply-templates mode="pure" select="*[6]/*[1]/*"/>
 104     </m:type>
 105    </m:bvar>
 106    <xsl:apply-templates mode="noannot" select="*[6]/target"/>
 107   </m:apply>
 108  </m:apply>
 109
 110 <!-- da tertminare
 111   </xsl:when>
 112   <xsl:otherwise>
 113    <m:apply helm:xref="{@id}">
 114     <m:csymbol>or_ind</m:csymbol>
 115     <xsl:apply-templates mode="noannot" select="*[7]"/>
 116     <xsl:for-each select="$InnerTypes">
 117      <xsl:apply-templates mode="pure" select="key('typeid',$id)/*[1]"/>
 118     </xsl:for-each>
 119     <xsl:apply-templates mode="pure" select="*[5]"/>
 120     <xsl:apply-templates mode="pure" select="*[6]"/>
 121    </m:apply>
 122   </xsl:otherwise>
 123  </xsl:choose>
 124 -->
 125 </xsl:template>
 126
 127
 128 <xsl:template mode="proof_transform" match="APPLY[CONST[
 129  attribute::uri='cic:/Coq/Init/Logic_Type/exT_ind.con' or
 130  attribute::uri='cic:/Coq/Init/Logic/First_order_quantifiers/ex_ind.con'] and
 131  count(child::*) = 6 and
 132  name(*[5])='LAMBDA' and count(*[5]/decl) >= 2 ]">
 133   <xsl:variable name="id" select="@id"/>
 134    <m:apply helm:xref="{@id}">
 135     <m:csymbol>ex_ind</m:csymbol>
 136     <xsl:apply-templates mode="noannot" select="*[6]"/>
 137     <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/*[1]/@binder"/></xsl:with-param></xsl:call-template></m:ci>
 138     <xsl:apply-templates mode="pure" select="*[5]/*[1]/*"/>
 139     <m:ci><xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[5]/*[2]/@binder"/></xsl:with-param></xsl:call-template></m:ci>
 140     <xsl:apply-templates mode="pure" select="*[5]/*[2]/*"/>
 141     <xsl:choose>
 142      <xsl:when test="count(*[5]/decl) > 2">
 143       <xsl:apply-templates mode="lambda_prop" select="*[5]/decl[3]"/>
 144      </xsl:when>
 145      <xsl:otherwise>
 146       <xsl:apply-templates mode="proof_transform" select="*[5]/target/*"/>
 147      </xsl:otherwise>
 148     </xsl:choose>
 149    </m:apply>
 150 </xsl:template>
 151
 152
 153 </xsl:stylesheet>
 154
 155