From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 16 Nov 2001 09:36:08 +0000 (+0000)
Subject: Disequalities chains for algebra. First draft.
X-Git-Tag: mlminidom_0_2_2~78
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9615625bcabfb81bda129ee14c3bf396ba761416;p=helm.git

Disequalities chains for algebra. First draft.
---

diff --git a/helm/style/arith.xsl b/helm/style/arith.xsl
index 47baf518d..0751b123c 100644
--- a/helm/style/arith.xsl
+++ b/helm/style/arith.xsl
@@ -36,6 +36,39 @@
 
 <!-- ************************** ARITHMETICS ****************************** -->
 
+<!-- S and O -->
+<xsl:template match="APPLY[*[position()=1 and name()='MUTCONSTRUCT' and @uri='cic:/Coq/Init/Datatypes/nat.ind' and @noConstr='2'] and count(*)=2]" mode="pure">
+   <xsl:apply-templates select="*[2]" mode="succ">
+    <xsl:with-param name="n" select="1"/>
+    <xsl:with-param name="iden" select="@id"/>
+   </xsl:apply-templates>
+</xsl:template>
+
+<xsl:template match="*" mode="succ">
+ <xsl:param name="n" select="0"/>
+ <xsl:param name="iden" select="''"/>
+ <xsl:choose>
+  <xsl:when test="name()='APPLY' and *[position()=1 and name()='MUTCONSTRUCT'
+and @uri='cic:/Coq/Init/Datatypes/nat.ind' and @noConstr='2']">
+   <xsl:apply-templates select="*[2]" mode="succ">
+    <xsl:with-param name="n" select="$n +1"/>
+    <xsl:with-param name="iden" select="$iden"/>
+   </xsl:apply-templates>
+  </xsl:when>
+  <xsl:when test="name()='MUTCONSTRUCT' and @uri='cic:/Coq/Init/Datatypes/nat.ind' and @noConstr='1'">
+   <m:ci helm:xref="{$iden}"><xsl:value-of select="$n"/></m:ci>
+  </xsl:when>
+  <xsl:otherwise>
+   <m:apply helm:xref="{$iden}">
+    <m:plus/>
+    <m:ci><xsl:value-of select="$n"/></m:ci>
+    <xsl:apply-templates select="." mode="pure"/>
+   </m:apply>
+  </xsl:otherwise>
+ </xsl:choose>
+</xsl:template>
+
+
 <xsl:template match="APPLY[MUTIND/@uri='cic:/Coq/Init/Peano/le.ind']" mode="pure">
    <xsl:call-template name="mk-mml-op-noannot">
       <xsl:with-param name="arity" select="2"/>
diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl
index b5c7481bf..5ffa0742a 100644
--- a/helm/style/content_to_html.xsl
+++ b/helm/style/content_to_html.xsl
@@ -1209,7 +1209,43 @@
          </xsl:apply-templates>
         </xsl:if>
        </xsl:for-each>
-      </xsl:when> 
+      </xsl:when>
+       <!-- diseq_chain -->
+      <xsl:when test="$name='diseq_chain'">
+       <FONT color="red">We have the following chain of disequalities:</FONT>
+       <xsl:for-each select="*[position() mod 3 = 2]">
+        <xsl:variable name="pos" select="position()"/>
+        <br/>
+        <xsl:call-template name="make_indent">
+         <xsl:with-param name="current_indent" select="$current_indent + 5"/>
+        </xsl:call-template>
+        <xsl:choose>
+         <xsl:when test="$pos=1">
+          <xsl:apply-templates select=".">
+           <xsl:with-param name="current_indent" select="$current_indent + 5"/>
+          </xsl:apply-templates>
+          <xsl:text>&#x00a0;</xsl:text>
+          <xsl:apply-templates mode="inline" select="../*[position()=3*$pos]"/>
+         </xsl:when>
+         <xsl:otherwise>
+          <xsl:apply-templates mode="inline" select="../*[position()=3*($pos - 1)]"/>
+          <xsl:text>&#x00a0;</xsl:text>
+          <xsl:apply-templates select=".">
+           <xsl:with-param name="current_indent" select="$current_indent + 5"/>
+          </xsl:apply-templates>
+         </xsl:otherwise>
+        </xsl:choose>
+        <xsl:if test="$pos != last()">
+         <br/>
+         <xsl:call-template name="make_indent">
+          <xsl:with-param name="current_indent" select="$current_indent + 15"/>
+         </xsl:call-template>
+         <xsl:apply-templates select="../*[position()=3*$pos +1]">
+          <xsl:with-param name="current_indent" select="$current_indent + 15"/>
+         </xsl:apply-templates>
+        </xsl:if>
+       </xsl:for-each>
+      </xsl:when>
       <!-- letin1 -->
       <xsl:when test="$name='letin1'">
        <xsl:apply-templates select="*[position()=2]">
diff --git a/helm/style/drop_coercions.xsl b/helm/style/drop_coercions.xsl
index f2bc44d0d..b31160eab 100644
--- a/helm/style/drop_coercions.xsl
+++ b/helm/style/drop_coercions.xsl
@@ -153,6 +153,25 @@
     </xsl:choose>
 </xsl:template>
 
+<xsl:template match="APPLY[CONST[position()='1' and 
+   @uri='cic:/Algebra/CRings/nat_injection/nring.con']]">
+     <xsl:variable name="no_params">
+      <xsl:call-template name="get_no_params">
+       <xsl:with-param name="first_uri" select="$CICURI"/>
+       <xsl:with-param name="second_uri" select="CONST[1]/@uri"/>
+      </xsl:call-template>
+     </xsl:variable>
+    <xsl:choose>
+     <xsl:when test="(count(child::*) - number($no_params)) = 2">
+      <xsl:apply-templates select="*[2+$no_params]"/>
+     </xsl:when>
+     <xsl:otherwise>
+      <APPLY id="{@id}" sort="{@sort}">
+       <xsl:apply-templates select="*"/>
+      </APPLY>
+     </xsl:otherwise>
+    </xsl:choose>
+</xsl:template>
 
 <xsl:template match = "/|*">
   <xsl:copy>
diff --git a/helm/style/html_init.xsl b/helm/style/html_init.xsl
index d3c9d1992..46fc61b24 100644
--- a/helm/style/html_init.xsl
+++ b/helm/style/html_init.xsl
@@ -165,6 +165,24 @@
  </xsl:choose>
 </xsl:template>
 
+<xsl:template mode="inline" match="m:eq|m:leq|m:lt|m:geq|m:gt">
+  <xsl:variable name="uri"><xsl:value-of select="*[1]/@definitionURL"/></xsl:variable>
+  <xsl:choose>
+  <xsl:when test="$uri != ''">
+   <a href="{$uri}">
+    <xsl:call-template name="mksymbol-init">
+     <xsl:with-param name="symbol" select="local-name(.)"/>
+    </xsl:call-template>
+   </a>
+  </xsl:when>
+  <xsl:otherwise>
+   <xsl:call-template name="mksymbol-init">
+     <xsl:with-param name="symbol" select="local-name(.)"/>
+   </xsl:call-template>
+  </xsl:otherwise>
+  </xsl:choose>
+</xsl:template>
+
  <xsl:template mode="inline" match="m:apply[m:and|m:or|m:eq|m:neq|m:leq|m:lt
        |m:geq|m:gt|m:plus|m:times|m:divide]">
   <xsl:variable name="uri"><xsl:value-of select="*[1]/@definitionURL"/></xsl:variable>
diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl
index 745792133..5a34d8a06 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
@@ -511,7 +749,7 @@
      </xsl:otherwise>
     </xsl:choose>
     <xsl:apply-templates mode="proof_transform" select="$proof"/>
-    <xsl:apply-templates mode="pure" select="$InnerTypes/InnerTypes/TYPE[@of=$id]/*"/>
+    <xsl:apply-templates mode="pure" select="$InnerTypes/InnerTypes/TYPE[@of=$proof/@id]/*"/>
    </m:apply>
    <!-- <xsl:apply-templates select="$proof" mode="noannot"/> -->
   </xsl:otherwise>