X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fstyle%2Fproofs.xsl;h=1d619260a2dbe6bd22fa5c64d5e14f57b4666081;hb=7e60b896247a228beea1b2a547c1f606e1834921;hp=4c207e4820e6d30f0e52a540aab890478536bc31;hpb=3aa2fd56797217a73b59e25bbe961dbc8c08bb2f;p=helm.git

diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl
index 4c207e482..1d619260a 100644
--- a/helm/style/proofs.xsl
+++ b/helm/style/proofs.xsl
@@ -186,6 +186,121 @@
  </xsl:choose>
 </xsl:template>
 
+<xsl:template mode="diseq" match="*">
+  <xsl:param name="rel" select="'eq'"/>
+  <xsl:choose>
+  <xsl:when test="name()='APPLY'">
+      <xsl:variable name="id" select="@id"/>
+   <xsl:choose>
+    <!-- ricordarsi di trattare il parametro -->
+    <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_transitive.con'] and count(child::*) = 7">
+       <xsl:apply-templates mode="diseq" select="*[6]">
+        <xsl:with-param name="rel" select="'leq'"/>
+       </xsl:apply-templates>
+       <xsl:apply-templates mode="noannot" select="*[4]"/>
+       <xsl:apply-templates mode="diseq" select="*[7]">
+        <xsl:with-param name="rel" select="'leq'"/>
+       </xsl:apply-templates>
+    </xsl:when> 
+    <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_wdl.con'] and count(child::*) = 7">
+       <m:eq/>
+       <!-- <m:ci><xsl:value-of select="'eq'"/></m:ci> -->
+       <xsl:call-template name="generate_side_proof">
+        <xsl:with-param name="proof" select="*[7]"/>
+        <xsl:with-param name="show_statement" select="0"/>
+       </xsl:call-template>
+       <xsl:apply-templates mode="noannot" select="*[3]"/>
+       <xsl:apply-templates mode="diseq" select="*[6]">
+        <xsl:with-param name="rel" select="'leq'"/>
+       </xsl:apply-templates>
+    </xsl:when> 
+    <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_less_trans.con'] and count(child::*) = 7">
+       <xsl:apply-templates mode="diseq" select="*[6]">
+        <xsl:with-param name="rel" select="'leq'"/>
+       </xsl:apply-templates>
+       <xsl:apply-templates mode="noannot" select="*[4]"/>
+       <xsl:apply-templates mode="diseq" select="*[7]">
+        <xsl:with-param name="rel" select="'lt'"/>
+       </xsl:apply-templates>
+    </xsl:when>
+    <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/less_leEq_trans.con'] and count(child::*) = 7">
+       <xsl:apply-templates mode="diseq" select="*[6]">
+        <xsl:with-param name="rel" select="'lt'"/>
+       </xsl:apply-templates>
+       <xsl:apply-templates mode="noannot" select="*[4]"/>
+       <xsl:apply-templates mode="diseq" select="*[7]">
+        <xsl:with-param name="rel" select="'leq'"/>
+       </xsl:apply-templates>
+    </xsl:when>  
+    <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_wdr.con'] and count(child::*) = 7">
+       <xsl:apply-templates mode="diseq" select="*[6]">
+        <xsl:with-param name="rel" select="'leq'"/>
+       </xsl:apply-templates>
+       <xsl:apply-templates mode="noannot" select="*[4]"/>
+       <xsl:apply-templates mode="diseq" select="*[7]">
+        <xsl:with-param name="rel" select="'eq'"/>
+       </xsl:apply-templates>
+    </xsl:when>  
+    <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_transitive_unfolded.con'] and count(child::*) = 7">
+      <xsl:apply-templates mode="diseq" select="*[6]">
+        <xsl:with-param name="rel" select="'lt'"/>
+       </xsl:apply-templates>
+       <xsl:apply-templates mode="noannot" select="*[4]"/>
+       <xsl:apply-templates mode="diseq" select="*[7]">
+        <xsl:with-param name="rel" select="'lt'"/>
+       </xsl:apply-templates>
+     </xsl:when> 
+    <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_wdr.con'] and count(child::*) = 7">
+       <xsl:apply-templates mode="diseq" select="*[6]">
+        <xsl:with-param name="rel" select="'lt'"/>
+       </xsl:apply-templates>
+       <xsl:apply-templates mode="noannot" select="*[4]"/>
+       <xsl:apply-templates mode="diseq" select="*[7]">
+        <xsl:with-param name="rel" select="'eq'"/>
+       </xsl:apply-templates>
+     </xsl:when>
+    <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_wdl.con'] and count(child::*) = 7">
+       <m:eq/>
+       <!-- <m:ci><xsl:value-of select="'eq'"/></m:ci> -->
+       <xsl:call-template name="generate_side_proof">
+        <xsl:with-param name="proof" select="*[7]"/>
+        <xsl:with-param name="show_statement" select="0"/>
+       </xsl:call-template>
+       <xsl:apply-templates mode="noannot" select="*[3]"/>
+       <xsl:apply-templates mode="diseq" select="*[6]">
+        <xsl:with-param name="rel" select="'lt'"/>
+       </xsl:apply-templates>
+    </xsl:when> 
+    <!-- 
+    <xsl:when test="CONST[attribute::uri='cic:/Algebra/CSetoids/CSetoid_basics/eq_transitive_unfolded.con'] and count(child::*) = 7">
+     <xsl:apply-templates mode="diseq" select="*[6]"/>
+     <m:eq/>
+     <xsl:apply-templates mode="noannot" select="*[4]"/>
+     <m:eq/>
+     <xsl:apply-templates mode="diseq" select="*[7]"/>
+    </xsl:when> 
+    -->
+    <xsl:otherwise>
+     <xsl:element name="{concat('m:',$rel)}"/>
+     <!-- <m:ci><xsl:value-of select="$rel"/></m:ci> -->  
+     <xsl:call-template name="generate_side_proof">
+      <xsl:with-param name="proof" select="."/>
+      <xsl:with-param name="show_statement" select="0"/>
+     </xsl:call-template> 
+    </xsl:otherwise>
+   </xsl:choose>
+  </xsl:when>
+  <xsl:otherwise>
+   <xsl:element name="{concat('m:',$rel)}"/> 
+   <!-- <m:ci><xsl:value-of select="$rel"/></m:ci> --> 
+   <xsl:call-template name="generate_side_proof">
+    <xsl:with-param name="proof" select="."/>
+    <xsl:with-param name="show_statement" select="0"/>
+   </xsl:call-template>
+  </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
 <xsl:template mode="proof_transform" match="*">
  <xsl:choose>
   <xsl:when test="name()='APPLY'">
@@ -204,6 +319,129 @@
        <xsl:apply-templates mode="noannot" select="*[5]"/>
      </m:apply>
     </xsl:when>
+    <!-- Algebra disequalities -->
+    <!-- It requires a special mode "diseq"-->
+    <!-- togliere il parametro -->
+    <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_transitive.con'] and count(child::*) = 7">
+     <m:apply>
+       <m:csymbol>diseq_chain</m:csymbol>
+       <xsl:apply-templates mode="noannot" select="*[3]"/>
+       <xsl:apply-templates mode="diseq" select="*[6]">
+        <xsl:with-param name="rel" select="'leq'"/>
+       </xsl:apply-templates>
+       <xsl:apply-templates mode="noannot" select="*[4]"/>
+       <xsl:apply-templates mode="diseq" select="*[7]">
+        <xsl:with-param name="rel" select="'leq'"/>
+       </xsl:apply-templates>
+       <xsl:apply-templates mode="noannot" select="*[5]"/>
+     </m:apply>
+    </xsl:when> 
+     <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_wdl.con'] and count(child::*) = 7">
+     <m:apply>
+       <m:csymbol>diseq_chain</m:csymbol>
+       <xsl:apply-templates mode="noannot" select="*[5]"/>
+       <m:eq/>
+       <!-- <m:ci><xsl:value-of select="'eq'"/></m:ci> -->
+       <xsl:call-template name="generate_side_proof">
+        <xsl:with-param name="proof" select="*[7]"/>
+        <xsl:with-param name="show_statement" select="0"/>
+       </xsl:call-template>
+       <xsl:apply-templates mode="noannot" select="*[3]"/>
+       <xsl:apply-templates mode="diseq" select="*[6]">
+        <xsl:with-param name="rel" select="'leq'"/>
+       </xsl:apply-templates>
+       <xsl:apply-templates mode="noannot" select="*[4]"/>
+     </m:apply>
+    </xsl:when>
+    <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_less_trans.con'] and count(child::*) = 7">
+     <m:apply>
+       <m:csymbol>diseq_chain</m:csymbol>
+       <xsl:apply-templates mode="noannot" select="*[3]"/>
+       <xsl:apply-templates mode="diseq" select="*[6]">
+        <xsl:with-param name="rel" select="'leq'"/>
+       </xsl:apply-templates>
+       <xsl:apply-templates mode="noannot" select="*[4]"/>
+       <xsl:apply-templates mode="diseq" select="*[7]">
+        <xsl:with-param name="rel" select="'lt'"/>
+       </xsl:apply-templates>
+       <xsl:apply-templates mode="noannot" select="*[5]"/>
+     </m:apply>
+    </xsl:when> 
+    <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/less_leEq_trans.con'] and count(child::*) = 7">
+     <m:apply>
+       <m:csymbol>diseq_chain</m:csymbol>
+       <xsl:apply-templates mode="noannot" select="*[3]"/>
+       <xsl:apply-templates mode="diseq" select="*[6]">
+        <xsl:with-param name="rel" select="'lt'"/>
+       </xsl:apply-templates>
+       <xsl:apply-templates mode="noannot" select="*[4]"/>
+       <xsl:apply-templates mode="diseq" select="*[7]">
+        <xsl:with-param name="rel" select="'leq'"/>
+       </xsl:apply-templates>
+       <xsl:apply-templates mode="noannot" select="*[5]"/>
+     </m:apply>
+    </xsl:when>  
+    <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/Basic_Properties_of_leEq/leEq_wdr.con'] and count(child::*) = 7">
+     <m:apply>
+       <m:csymbol>diseq_chain</m:csymbol>
+       <xsl:apply-templates mode="noannot" select="*[3]"/>
+       <xsl:apply-templates mode="diseq" select="*[6]">
+        <xsl:with-param name="rel" select="'leq'"/>
+       </xsl:apply-templates>
+       <xsl:apply-templates mode="noannot" select="*[4]"/>
+       <xsl:apply-templates mode="diseq" select="*[7]">
+        <xsl:with-param name="rel" select="'eq'"/>
+       </xsl:apply-templates>
+       <xsl:apply-templates mode="noannot" select="*[5]"/>
+     </m:apply>
+    </xsl:when>  
+    <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_transitive_unfolded.con'] and count(child::*) = 7">
+     <m:apply>
+       <m:csymbol>diseq_chain</m:csymbol>
+       <xsl:apply-templates mode="noannot" select="*[3]"/>
+       <xsl:apply-templates mode="diseq" select="*[6]">
+        <xsl:with-param name="rel" select="'lt'"/>
+       </xsl:apply-templates>
+       <xsl:apply-templates mode="noannot" select="*[4]"/>
+       <xsl:apply-templates mode="diseq" select="*[7]">
+        <xsl:with-param name="rel" select="'lt'"/>
+       </xsl:apply-templates>
+       <xsl:apply-templates mode="noannot" select="*[5]"/>
+     </m:apply>
+    </xsl:when>  
+    <!-- togliere il parametro -->
+    <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_wdr.con'] and count(child::*) = 7">
+     <m:apply>
+       <m:csymbol>diseq_chain</m:csymbol>
+       <xsl:apply-templates mode="noannot" select="*[3]"/>
+       <xsl:apply-templates mode="diseq" select="*[6]">
+        <xsl:with-param name="rel" select="'lt'"/>
+       </xsl:apply-templates>
+       <xsl:apply-templates mode="noannot" select="*[4]"/>
+       <xsl:apply-templates mode="diseq" select="*[7]">
+        <xsl:with-param name="rel" select="'eq'"/>
+       </xsl:apply-templates>
+       <xsl:apply-templates mode="noannot" select="*[5]"/>
+     </m:apply>
+    </xsl:when>
+    <!-- togliere il parametro -->
+    <xsl:when test="CONST[attribute::uri='cic:/Algebra/COrdFields/COrdField_axioms/less_wdl.con'] and count(child::*) = 7">
+     <m:apply>
+       <m:csymbol>diseq_chain</m:csymbol>
+       <xsl:apply-templates mode="noannot" select="*[5]"/>
+       <m:eq/>
+       <!-- <m:ci><xsl:value-of select="'eq'"/></m:ci> -->
+       <xsl:call-template name="generate_side_proof">
+        <xsl:with-param name="proof" select="*[7]"/>
+        <xsl:with-param name="show_statement" select="0"/>
+       </xsl:call-template>
+       <xsl:apply-templates mode="noannot" select="*[3]"/>
+       <xsl:apply-templates mode="diseq" select="*[6]">
+        <xsl:with-param name="rel" select="'lt'"/>
+       </xsl:apply-templates>
+       <xsl:apply-templates mode="noannot" select="*[4]"/>
+     </m:apply>
+    </xsl:when> 
     <!-- EQUALITY -->
     <xsl:when test="CONST[
  attribute::uri='cic:/Coq/Init/Logic/Equality/eq_ind.con' or
@@ -359,7 +597,7 @@
          <m:csymbol>full_or_ind</m:csymbol>
          <xsl:apply-templates mode="noannot" select="*[7]"/>
          <xsl:apply-templates mode="pure" 
-              select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
+              select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*[1]"/>
          <m:apply>
           <m:csymbol>left_case</m:csymbol>
           <m:bvar>
@@ -391,7 +629,7 @@
          <m:csymbol>or_ind</m:csymbol>
          <xsl:apply-templates mode="noannot" select="*[7]"/>
          <xsl:apply-templates mode="pure" 
-              select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
+              select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*[1]"/>
          <xsl:apply-templates mode="pure" select="*[5]"/>
          <xsl:apply-templates mode="pure" select="*[6]"/>
         </m:apply>
@@ -510,8 +748,8 @@
       <m:csymbol>side_proof</m:csymbol>
      </xsl:otherwise>
     </xsl:choose>
-    <xsl:apply-templates mode="proof_transform" select="."/>
-    <xsl:apply-templates mode="pure" select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
+    <xsl:apply-templates mode="proof_transform" select="$proof"/>
+    <xsl:apply-templates mode="pure" select="$InnerTypes/InnerTypes/TYPE[@of=$proof/@id]/*"/>
    </m:apply>
    <!-- <xsl:apply-templates select="$proof" mode="noannot"/> -->
   </xsl:otherwise>