helm/style/diseq.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 <!-- Disequalities                                                    -->
  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 <!-- ************************* LOGIC *********************************-->
  38
  39 <xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/CSetoids/CSetoid_basics/eq_transitive_unfolded.con'] and count(child::*) = 7]">
  40  <xsl:variable name="id" select="@id"/>
  41  <m:apply>
  42   <m:csymbol>diseq_chain</m:csymbol>
  43   <xsl:apply-templates mode="noannot" select="*[3]"/>
  44   <xsl:apply-templates mode="diseq" select="*[6]">
  45    <xsl:with-param name="rel" select="'eq'"/>
  46   </xsl:apply-templates>
  47   <xsl:apply-templates mode="noannot" select="*[4]"/>
  48   <xsl:apply-templates mode="diseq" select="*[7]">
  49    <xsl:with-param name="rel" select="'eq'"/>
  50   </xsl:apply-templates>
  51   <xsl:apply-templates mode="noannot" select="*[5]"/>
  52  </m:apply>
  53 </xsl:template>
  54
  55 <xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/Basic_Properties_of_leEq/leEq_transitive.con'] and count(child::*) = 7]">
  56  <xsl:variable name="id" select="@id"/>
  57  <m:apply>
  58   <m:csymbol>diseq_chain</m:csymbol>
  59   <xsl:apply-templates mode="noannot" select="*[3]"/>
  60   <xsl:apply-templates mode="diseq" select="*[6]">
  61    <xsl:with-param name="rel" select="'leq'"/>
  62   </xsl:apply-templates>
  63   <xsl:apply-templates mode="noannot" select="*[4]"/>
  64   <xsl:apply-templates mode="diseq" select="*[7]">
  65    <xsl:with-param name="rel" select="'leq'"/>
  66   </xsl:apply-templates>
  67   <xsl:apply-templates mode="noannot" select="*[5]"/>
  68  </m:apply>
  69 </xsl:template>
  70
  71 <xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/Basic_Properties_of_leEq/leEq_wdl.con'] and count(child::*) = 7]">
  72  <xsl:variable name="id" select="@id"/>
  73  <m:apply>
  74   <m:csymbol>diseq_chain</m:csymbol>
  75   <xsl:apply-templates mode="noannot" select="*[5]"/>
  76   <xsl:apply-templates mode="diseq" select="*[7]">
  77    <xsl:with-param name="rel" select="'eq'"/>
  78   </xsl:apply-templates>
  79   <xsl:apply-templates mode="noannot" select="*[3]"/>
  80   <xsl:apply-templates mode="diseq" select="*[6]">
  81    <xsl:with-param name="rel" select="'leq'"/>
  82   </xsl:apply-templates>
  83   <xsl:apply-templates mode="noannot" select="*[4]"/>
  84  </m:apply>
  85 </xsl:template>
  86
  87 <xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/Basic_Properties_of_leEq/leEq_less_trans.con'] and count(child::*) = 7]">
  88  <xsl:variable name="id" select="@id"/>
  89  <m:apply>
  90   <m:csymbol>diseq_chain</m:csymbol>
  91   <xsl:apply-templates mode="noannot" select="*[3]"/>
  92   <xsl:apply-templates mode="diseq" select="*[6]">
  93    <xsl:with-param name="rel" select="'leq'"/>
  94   </xsl:apply-templates>
  95   <xsl:apply-templates mode="noannot" select="*[4]"/>
  96   <xsl:apply-templates mode="diseq" select="*[7]">
  97    <xsl:with-param name="rel" select="'lt'"/>
  98   </xsl:apply-templates>
  99   <xsl:apply-templates mode="noannot" select="*[5]"/>
 100  </m:apply>
 101 </xsl:template>
 102
 103 <xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/Basic_Properties_of_leEq/less_leEq_trans.con'] and count(child::*) = 7]">
 104  <xsl:variable name="id" select="@id"/>
 105  <m:apply>
 106   <m:csymbol>diseq_chain</m:csymbol>
 107   <xsl:apply-templates mode="noannot" select="*[3]"/>
 108   <xsl:apply-templates mode="diseq" select="*[6]">
 109    <xsl:with-param name="rel" select="'lt'"/>
 110   </xsl:apply-templates>
 111   <xsl:apply-templates mode="noannot" select="*[4]"/>
 112   <xsl:apply-templates mode="diseq" select="*[7]">
 113    <xsl:with-param name="rel" select="'leq'"/>
 114   </xsl:apply-templates>
 115   <xsl:apply-templates mode="noannot" select="*[5]"/>
 116  </m:apply>
 117 </xsl:template>
 118
 119 <xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/Basic_Properties_of_leEq/leEq_wdr.con'] and count(child::*) = 7]">
 120  <xsl:variable name="id" select="@id"/>
 121  <m:apply>
 122   <m:csymbol>diseq_chain</m:csymbol>
 123   <xsl:apply-templates mode="noannot" select="*[3]"/>
 124   <xsl:apply-templates mode="diseq" select="*[6]">
 125    <xsl:with-param name="rel" select="'leq'"/>
 126   </xsl:apply-templates>
 127   <xsl:apply-templates mode="noannot" select="*[4]"/>
 128   <xsl:apply-templates mode="diseq" select="*[7]">
 129    <xsl:with-param name="rel" select="'eq'"/>
 130   </xsl:apply-templates>
 131   <xsl:apply-templates mode="noannot" select="*[5]"/>
 132  </m:apply>
 133 </xsl:template>
 134
 135 <xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/COrdField_axioms/less_transitive_unfolded.con'] and count(child::*) = 7]">
 136  <xsl:variable name="id" select="@id"/>
 137  <m:apply>
 138   <m:csymbol>diseq_chain</m:csymbol>
 139   <xsl:apply-templates mode="noannot" select="*[3]"/>
 140   <xsl:apply-templates mode="diseq" select="*[6]">
 141    <xsl:with-param name="rel" select="'lt'"/>
 142   </xsl:apply-templates>
 143   <xsl:apply-templates mode="noannot" select="*[4]"/>
 144   <xsl:apply-templates mode="diseq" select="*[7]">
 145    <xsl:with-param name="rel" select="'lt'"/>
 146   </xsl:apply-templates>
 147   <xsl:apply-templates mode="noannot" select="*[5]"/>
 148  </m:apply>
 149 </xsl:template>
 150
 151 <xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/COrdField_axioms/less_wdr.con'] and count(child::*) = 7]">
 152  <xsl:variable name="id" select="@id"/>
 153  <m:apply>
 154   <m:csymbol>diseq_chain</m:csymbol>
 155   <xsl:apply-templates mode="noannot" select="*[3]"/>
 156   <xsl:apply-templates mode="diseq" select="*[6]">
 157    <xsl:with-param name="rel" select="'lt'"/>
 158   </xsl:apply-templates>
 159   <xsl:apply-templates mode="noannot" select="*[4]"/>
 160   <xsl:apply-templates mode="diseq" select="*[7]">
 161    <xsl:with-param name="rel" select="'eq'"/>
 162   </xsl:apply-templates>
 163   <xsl:apply-templates mode="noannot" select="*[5]"/>
 164  </m:apply>
 165 </xsl:template>
 166
 167 <xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Algebra/algebra/COrdFields/COrdField_axioms/less_wdl.con'] and count(child::*) = 7]">
 168  <xsl:variable name="id" select="@id"/>
 169  <m:apply>
 170   <m:csymbol>diseq_chain</m:csymbol>
 171   <xsl:apply-templates mode="noannot" select="*[5]"/>
 172   <xsl:apply-templates mode="diseq" select="*[7]">
 173    <xsl:with-param name="rel" select="'eq'"/>
 174   </xsl:apply-templates>
 175   <xsl:apply-templates mode="noannot" select="*[3]"/>
 176   <xsl:apply-templates mode="diseq" select="*[6]">
 177    <xsl:with-param name="rel" select="'lt'"/>
 178   </xsl:apply-templates>
 179   <xsl:apply-templates mode="noannot" select="*[4]"/>
 180  </m:apply>
 181 </xsl:template>
 182
 183 <xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Coq/Reals/Rbase/Rle_lt_trans.con'] and count(child::*) = 6]">
 184  <xsl:variable name="id" select="@id"/>
 185  <m:apply>
 186   <m:csymbol>diseq_chain</m:csymbol>
 187   <xsl:apply-templates mode="noannot" select="*[2]"/>
 188   <xsl:apply-templates mode="diseq" select="*[5]">
 189    <xsl:with-param name="rel" select="'leq'"/>
 190   </xsl:apply-templates>
 191   <xsl:apply-templates mode="noannot" select="*[3]"/>
 192   <xsl:apply-templates mode="diseq" select="*[6]">
 193    <xsl:with-param name="rel" select="'lt'"/>
 194   </xsl:apply-templates>
 195   <xsl:apply-templates mode="noannot" select="*[4]"/>
 196  </m:apply>
 197 </xsl:template>
 198
 199 <xsl:template mode="proof_transform" match="APPLY[CONST[attribute::uri='cic:/Coq/Reals/Rbase/Rlt_le_trans.con'] and count(child::*) = 6]">
 200  <xsl:variable name="id" select="@id"/>
 201  <m:apply>
 202   <m:csymbol>diseq_chain</m:csymbol>
 203   <xsl:apply-templates mode="noannot" select="*[2]"/>
 204   <xsl:apply-templates mode="diseq" select="*[5]">
 205    <xsl:with-param name="rel" select="'lt'"/>
 206   </xsl:apply-templates>
 207   <xsl:apply-templates mode="noannot" select="*[3]"/>
 208   <xsl:apply-templates mode="diseq" select="*[6]">
 209    <xsl:with-param name="rel" select="'leq'"/>
 210   </xsl:apply-templates>
 211   <xsl:apply-templates mode="noannot" select="*[4]"/>
 212  </m:apply>
 213 </xsl:template>
 214
 215 <xsl:template mode="diseq" match="*">
 216  <xsl:param name="rel" select="'eq'"/>
 217   <xsl:choose>
 218    <xsl:when test="name()='APPLY'">
 219     <xsl:variable name="id" select="@id"/>
 220     <xsl:choose>
 221      <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_transitive.con'] and count(child::*) = 7">
 222        <xsl:apply-templates mode="diseq" select="*[6]">
 223         <xsl:with-param name="rel" select="'leq'"/>
 224        </xsl:apply-templates>
 225        <xsl:apply-templates mode="noannot" select="*[4]"/>
 226        <xsl:apply-templates mode="diseq" select="*[7]">
 227         <xsl:with-param name="rel" select="'leq'"/>
 228        </xsl:apply-templates>
 229      </xsl:when>
 230      <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_wdl.con'] and count(child::*) = 7">
 231        <xsl:call-template name="generate_side_proof">
 232         <xsl:with-param name="proof" select="*[7]"/>
 233         <xsl:with-param name="show_statement" select="0"/>
 234        </xsl:call-template>
 235        <xsl:apply-templates mode="diseq" select="*[7]">
 236         <xsl:with-param name="rel" select="'eq'"/>
 237        </xsl:apply-templates>
 238        <xsl:apply-templates mode="noannot" select="*[3]"/>
 239        <xsl:apply-templates mode="diseq" select="*[6]">
 240         <xsl:with-param name="rel" select="'leq'"/>
 241        </xsl:apply-templates>
 242      </xsl:when>
 243      <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_less_trans.con'] and count(child::*) = 7">
 244        <xsl:apply-templates mode="diseq" select="*[6]">
 245         <xsl:with-param name="rel" select="'leq'"/>
 246        </xsl:apply-templates>
 247        <xsl:apply-templates mode="noannot" select="*[4]"/>
 248        <xsl:apply-templates mode="diseq" select="*[7]">
 249         <xsl:with-param name="rel" select="'lt'"/>
 250        </xsl:apply-templates>
 251      </xsl:when>
 252      <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/less_leEq_trans.con'] and count(child::*) = 7">
 253        <xsl:apply-templates mode="diseq" select="*[6]">
 254         <xsl:with-param name="rel" select="'lt'"/>
 255        </xsl:apply-templates>
 256        <xsl:apply-templates mode="noannot" select="*[4]"/>
 257        <xsl:apply-templates mode="diseq" select="*[7]">
 258         <xsl:with-param name="rel" select="'leq'"/>
 259        </xsl:apply-templates>
 260      </xsl:when>
 261      <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_wdr.con'] and count(child::*) = 7">
 262        <xsl:apply-templates mode="diseq" select="*[6]">
 263         <xsl:with-param name="rel" select="'leq'"/>
 264        </xsl:apply-templates>
 265        <xsl:apply-templates mode="noannot" select="*[4]"/>
 266        <xsl:apply-templates mode="diseq" select="*[7]">
 267         <xsl:with-param name="rel" select="'eq'"/>
 268        </xsl:apply-templates>
 269      </xsl:when>
 270      <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_transitive_unfolded.con'] and count(child::*) = 7">
 271       <xsl:apply-templates mode="diseq" select="*[6]">
 272         <xsl:with-param name="rel" select="'lt'"/>
 273        </xsl:apply-templates>
 274        <xsl:apply-templates mode="noannot" select="*[4]"/>
 275        <xsl:apply-templates mode="diseq" select="*[7]">
 276         <xsl:with-param name="rel" select="'lt'"/>
 277        </xsl:apply-templates>
 278      </xsl:when>
 279      <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_wdr.con'] and count(child::*) = 7">
 280        <xsl:apply-templates mode="diseq" select="*[6]">
 281         <xsl:with-param name="rel" select="'lt'"/>
 282        </xsl:apply-templates>
 283        <xsl:apply-templates mode="noannot" select="*[4]"/>
 284        <xsl:apply-templates mode="diseq" select="*[7]">
 285         <xsl:with-param name="rel" select="'eq'"/>
 286        </xsl:apply-templates>
 287      </xsl:when>
 288      <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_wdl.con'] and count(child::*) = 7">
 289        <xsl:apply-templates mode="diseq" select="*[7]">
 290         <xsl:with-param name="rel" select="'eq'"/>
 291        </xsl:apply-templates>
 292        <xsl:apply-templates mode="noannot" select="*[3]"/>
 293        <xsl:apply-templates mode="diseq" select="*[6]">
 294         <xsl:with-param name="rel" select="'lt'"/>
 295        </xsl:apply-templates>
 296      </xsl:when>
 297      <!-- REALS -->
 298      <xsl:when test="CONST[attribute::uri='cic:/Coq/Reals/Rbase/Rlt_le_trans.con'] and count(child::*) = 6">
 299        <xsl:apply-templates mode="diseq" select="*[5]">
 300         <xsl:with-param name="rel" select="'lt'"/>
 301        </xsl:apply-templates>
 302        <xsl:apply-templates mode="noannot" select="*[3]"/>
 303        <xsl:apply-templates mode="diseq" select="*[6]">
 304         <xsl:with-param name="rel" select="'leq'"/>
 305        </xsl:apply-templates>
 306      </xsl:when>
 307      <xsl:when test="CONST[attribute::uri='cic:/Coq/Reals/Rbase/Rle_lt_trans.con'] and count(child::*) = 6">
 308        <xsl:apply-templates mode="diseq" select="*[5]">
 309         <xsl:with-param name="rel" select="'leq'"/>
 310        </xsl:apply-templates>
 311        <xsl:apply-templates mode="noannot" select="*[3]"/>
 312        <xsl:apply-templates mode="diseq" select="*[6]">
 313         <xsl:with-param name="rel" select="'lt'"/>
 314        </xsl:apply-templates>
 315      </xsl:when>
 316      <xsl:otherwise>
 317       <xsl:element name="{concat('m:',$rel)}"/>
 318       <xsl:call-template name="generate_side_proof">
 319        <xsl:with-param name="proof" select="."/>
 320        <xsl:with-param name="show_statement" select="0"/>
 321       </xsl:call-template>
 322      </xsl:otherwise>
 323     </xsl:choose>
 324    </xsl:when>
 325    <xsl:otherwise>
 326     <xsl:element name="{concat('m:',$rel)}"/>
 327     <xsl:call-template name="generate_side_proof">
 328      <xsl:with-param name="proof" select="."/>
 329      <xsl:with-param name="show_statement" select="0"/>
 330     </xsl:call-template>
 331    </xsl:otherwise>
 332   </xsl:choose>
 333 </xsl:template>
 334
 335
 336 </xsl:stylesheet>