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:apply-templates mode="noannot" select="*[5]/target/*"/>
  60   </m:apply>
  61 </xsl:template>
  62
  63 <xsl:template mode="proof_transform" match="APPLY[CONST[
  64  attribute::uri='cic:/Coq/Init/Logic/or_ind.con']
  65  and count(child::*) = 7 and
  66  name(*[5])='LAMBDA' and count(*[5]/decl) = 1 and
  67  name(*[6])='LAMBDA' and count(*[6]/decl) = 1 ]">
  68  <xsl:variable name="id" select="@id"/>
  69  <xsl:variable name="definition_url"
  70    select="'cic:/Coq/Init/Logic/Disjunction/or.ind'"/>
  71  <m:apply helm:xref="{@id}">
  72   <m:csymbol>full_or_ind</m:csymbol>
  73   <xsl:apply-templates mode="noannot" select="*[7]"/>
  74   <xsl:for-each select="$InnerTypes">
  75    <xsl:apply-templates mode="pure" select="key('typeid',$id)/*[1]"/>
  76   </xsl:for-each>
  77   <m:apply>
  78    <m:csymbol>left_case</m:csymbol>
  79    <m:bvar>
  80     <m:ci>
  81      <xsl:value-of select="*[5]/*[1]/@binder"/>
  82     </m:ci>
  83     <m:type>
  84      <xsl:apply-templates mode="pure" select="*[5]/*[1]/*"/>
  85     </m:type>
  86    </m:bvar>
  87    <xsl:apply-templates mode="noannot" select="*[5]/target/*"/>
  88   </m:apply>
  89   <m:apply>
  90    <m:csymbol>right_case</m:csymbol>
  91    <m:bvar>
  92     <m:ci>
  93      <xsl:apply-templates mode="pure" select="*[6]/*[1]/@binder"/>
  94     </m:ci>
  95     <m:type>
  96      <xsl:apply-templates mode="pure" select="*[6]/*[1]/*"/>
  97     </m:type>
  98    </m:bvar>
  99    <xsl:apply-templates mode="noannot" select="*[6]/target"/>
 100   </m:apply>
 101  </m:apply>
 102
 103 <!-- da tertminare
 104   </xsl:when>
 105   <xsl:otherwise>
 106    <m:apply helm:xref="{@id}">
 107     <m:csymbol>or_ind</m:csymbol>
 108     <xsl:apply-templates mode="noannot" select="*[7]"/>
 109     <xsl:for-each select="$InnerTypes">
 110      <xsl:apply-templates mode="pure" select="key('typeid',$id)/*[1]"/>
 111     </xsl:for-each>
 112     <xsl:apply-templates mode="pure" select="*[5]"/>
 113     <xsl:apply-templates mode="pure" select="*[6]"/>
 114    </m:apply>
 115   </xsl:otherwise>
 116  </xsl:choose>
 117 -->
 118 </xsl:template>
 119
 120 <xsl:template mode="proof_transform" match="APPLY[CONST[
 121  attribute::uri='cic:/Coq/Init/Logic_Type/exT_ind.con' or
 122  attribute::uri='cic:/Coq/Init/Logic/First_order_quantifiers/ex_ind.con'] and
 123  count(child::*) = 6 and
 124  name(*[5])='LAMBDA' and count(*[5]/decl) = 2 ]">
 125   <xsl:variable name="id" select="@id"/>
 126    <m:apply helm:xref="{@id}">
 127     <m:csymbol>ex_ind</m:csymbol>
 128     <xsl:apply-templates mode="noannot" select="*[6]"/>
 129     <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>
 130     <xsl:apply-templates mode="pure" select="*[5]/*[1]/*"/>
 131     <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>
 132     <xsl:apply-templates mode="pure" select="*[5]/*[2]/*"/>
 133     <xsl:apply-templates mode="proof_transform" select="*[5]/target/*"/>
 134    </m:apply>
 135 </xsl:template>
 136
 137 </xsl:stylesheet>
 138