From f757483a6beb4ed12c9959c07567e8891a2b3048 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 19 Jul 2001 16:52:13 +0000
Subject: [PATCH] First partial syncronization between the HTML and the MathML
 presentation: many csymbols added to MathML presentation.

*** NOTE! ***
The code seems to work perfectly, but I am unsure it is well implemented.
It is better to have a thorough look at it as soon as possible.
*************

The syncronization is still incomplete. The following csymbols are
missing (all of them from the Huet contrib):

subst
lift lift_with_base
beta_red1
beta_red
par_beta_red1
par_beta_red
forgetful
isomorphic
interp
---
 helm/style/content_to_html.xsl |  52 +------
 helm/style/mmlextension.xsl    | 247 ++++++++++++++++++++++++++++++---
 helm/style/proofs.xsl          |  26 ----
 3 files changed, 226 insertions(+), 99 deletions(-)

diff --git a/helm/style/content_to_html.xsl b/helm/style/content_to_html.xsl
index 85498997f..6e89d8cd9 100644
--- a/helm/style/content_to_html.xsl
+++ b/helm/style/content_to_html.xsl
@@ -1128,54 +1128,6 @@
         </xsl:otherwise>
        </xsl:choose>
       </xsl:when>
-      <!-- nat_ind -->
-      <xsl:when test="$name='nat_ind_complete'">
-       <FONT color="red">By induction on&#x00a0;</FONT>
-       <xsl:apply-templates select="*[2]"/>:
-       <br/>
-       <xsl:call-template name="make_indent">
-        <xsl:with-param name="current_indent" select="$current_indent"/> 
-       </xsl:call-template>
-       <xsl:text>0&#x00a0;</xsl:text>
-       <xsl:call-template name="mksymbol-1">
-        <xsl:with-param name="symbol" select="'RightArrow'"/>
-        <xsl:with-param name="color" select="'green'"/>
-        <xsl:with-param name="size" select="'+0'"/>
-       </xsl:call-template>
-       <xsl:apply-templates select="*[3]">
-        <xsl:with-param name="current_indent" select="$current_indent + 8"/>
-       </xsl:apply-templates>
-       <br/>
-       <xsl:call-template name="make_indent">
-        <xsl:with-param name="current_indent" select="$current_indent"/> 
-       </xsl:call-template>
-       <xsl:text>S(</xsl:text>
-       <xsl:apply-templates select="*[4]"/>
-       <xsl:text>)&#x00a0;</xsl:text>
-       <xsl:call-template name="mksymbol-1">
-        <xsl:with-param name="symbol" select="'RightArrow'"/>
-        <xsl:with-param name="color" select="'green'"/>
-        <xsl:with-param name="size" select="'+0'"/>
-       </xsl:call-template>
-       <FONT color="red">Assume by induction</FONT>
-       <br/>
-       <xsl:call-template name="make_indent">
-        <xsl:with-param name="current_indent" select="$current_indent +10"/> 
-       </xsl:call-template>
-       <xsl:text>(</xsl:text>
-       <xsl:apply-templates select="*[5]"/>
-       <xsl:text>)</xsl:text>
-       <xsl:apply-templates select="*[6]">
-        <xsl:with-param name="current_indent" select="$current_indent + 14"/>
-       </xsl:apply-templates>
-       <br/>
-       <xsl:call-template name="make_indent">
-        <xsl:with-param name="current_indent" select="$current_indent +10"/> 
-       </xsl:call-template>
-       <xsl:apply-templates select="*[7]">
-        <xsl:with-param name="current_indent" select="$current_indent + 10"/>
-       </xsl:apply-templates>
-      </xsl:when>
       <!-- false_ind -->
       <xsl:when test="$name='false_ind'">
        <xsl:apply-templates select="*[3]">
@@ -1313,7 +1265,7 @@
        <xsl:call-template name="make_indent">
         <xsl:with-param name="current_indent" select="$current_indent"/> 
        </xsl:call-template>
-       *
+       Left:&#x00a0;
        <xsl:apply-templates select="*[4]">
         <xsl:with-param name="current_indent" select="$current_indent"/> 
        </xsl:apply-templates>
@@ -1321,7 +1273,7 @@
        <xsl:call-template name="make_indent">
         <xsl:with-param name="current_indent" select="$current_indent"/> 
        </xsl:call-template>
-       *
+       Right:&#x00a0;
        <xsl:apply-templates select="*[5]">
         <xsl:with-param name="current_indent" select="$current_indent"/> 
        </xsl:apply-templates>
diff --git a/helm/style/mmlextension.xsl b/helm/style/mmlextension.xsl
index a4dfc5f01..8566c9726 100644
--- a/helm/style/mmlextension.xsl
+++ b/helm/style/mmlextension.xsl
@@ -407,6 +407,7 @@ which generates the toplevel element (see for instance xlink) -->
       <xsl:attribute name="m:xref"><xsl:value-of select="@id"/></xsl:attribute>
      </xsl:if>
      <xsl:choose>
+      <!-- FORALL -->
       <xsl:when test="$name='forall'">
        <xsl:choose>
        <xsl:when test="$charlength >= $framewidth">
@@ -439,6 +440,7 @@ which generates the toplevel element (see for instance xlink) -->
        </xsl:otherwise>
        </xsl:choose> 
       </xsl:when>
+      <!-- LET-IN -->
       <xsl:when test="$name='let_in'">
        <xsl:choose>
        <xsl:when test="$charlength >= $framewidth">
@@ -484,6 +486,7 @@ which generates the toplevel element (see for instance xlink) -->
        </xsl:otherwise>
        </xsl:choose>
       </xsl:when> 
+      <!-- PROD -->
       <xsl:when test="$name='prod'">
        <xsl:choose>
        <xsl:when test="$charlength >= $framewidth">
@@ -516,6 +519,7 @@ which generates the toplevel element (see for instance xlink) -->
        </xsl:otherwise>
        </xsl:choose> 
       </xsl:when>
+      <!-- ARROW -->
       <xsl:when test="$name='arrow'">
        <xsl:choose>
        <xsl:when test="$charlength >= $framewidth">
@@ -592,6 +596,7 @@ which generates the toplevel element (see for instance xlink) -->
        </xsl:otherwise>
        </xsl:choose>
       </xsl:when>
+      <!-- APP -->
       <xsl:when test="$name='app'">
        <xsl:choose>
        <xsl:when test="$charlength >= $framewidth">
@@ -634,6 +639,7 @@ which generates the toplevel element (see for instance xlink) -->
        </xsl:otherwise>
        </xsl:choose>
       </xsl:when>
+      <!-- CAST -->
       <xsl:when test="$name='cast'">
        <xsl:choose>
        <xsl:when test="$charlength >= $framewidth">
@@ -672,15 +678,19 @@ which generates the toplevel element (see for instance xlink) -->
        </xsl:otherwise>
        </xsl:choose>
       </xsl:when>
+      <!-- PROP -->
       <xsl:when test="$name='Prop'">
        <m:mo>Prop</m:mo>
       </xsl:when>
+      <!-- SET -->
       <xsl:when test="$name='Set'">
        <m:mo>Set</m:mo>
       </xsl:when>
+      <!-- TYPE -->
       <xsl:when test="$name='Type'">
        <m:mo>Type</m:mo>
       </xsl:when>
+      <!-- MUTCASE -->
       <xsl:when test="$name='mutcase'">
        <xsl:choose>
        <xsl:when test="$charlength >= $framewidth">
@@ -784,6 +794,7 @@ which generates the toplevel element (see for instance xlink) -->
        </xsl:otherwise>
        </xsl:choose>
       </xsl:when>
+      <!-- FIX -->
       <xsl:when test="$name='fix'">
        <xsl:choose>
        <xsl:when test="$charlength >= $framewidth">
@@ -873,6 +884,7 @@ which generates the toplevel element (see for instance xlink) -->
        </xsl:otherwise>
        </xsl:choose>
       </xsl:when>
+      <!-- COFIX -->
       <xsl:when test="$name='cofix'">
        <xsl:choose>
        <xsl:when test="$charlength >= $framewidth">
@@ -965,6 +977,7 @@ which generates the toplevel element (see for instance xlink) -->
       <!-- ***************************************** -->
       <!-- *********** PROOF ELEMENTS ************** -->
       <!-- ***************************************** -->
+      <!-- PROOF -->
       <xsl:when test="$name='proof'">
         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
          <m:mtr>
@@ -985,6 +998,7 @@ which generates the toplevel element (see for instance xlink) -->
          </m:mtr>
         </m:mtable>
       </xsl:when>
+      <!-- LETIN1 -->
       <xsl:when test="$name='letin1'">
         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
          <m:mtr>
@@ -1003,6 +1017,139 @@ which generates the toplevel element (see for instance xlink) -->
          </m:mtr>
         </m:mtable>
       </xsl:when>
+
+      <!-- CSC: Il caso che segue e' stato buttato li' giusto per vedere -->
+      <!-- qualche cosa. Irene, appena puoi, risistemalo.                -->
+      <xsl:when test="$name='by_induction'">
+       <m:mtable align="baseline 1" equalrows="false" columnalign="left">
+        <m:mtr>
+         <m:mtd>
+          <m:mrow>
+           <m:mtext mathcolor="red">We prove </m:mtext>
+           <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+           <xsl:apply-templates select="../*[3]"/>
+          </m:mrow>
+         </m:mtd>
+        </m:mtr>
+        <m:mtr>
+         <m:mtd>
+          <m:mrow>
+           <m:mtext mathcolor="red">by induction on </m:mtext>
+           <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+           <xsl:apply-templates
+            select="*[position()=last()]/*[position()=last()]"/>
+          </m:mrow>
+         </m:mtd>
+        </m:mtr>
+        <m:mtr>
+         <m:mtd>
+          <m:mrow>
+           <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+           <m:mtable align="baseline 1" equalrows="false" columnalign="left">
+            <xsl:for-each select="*[position()>3 and not(position()=last())]">
+             <m:mtr>
+              <m:mtd>
+               <xsl:apply-templates select="."/>
+              </m:mtd>
+             </m:mtr>
+            </xsl:for-each>
+           </m:mtable>
+          </m:mrow>
+         </m:mtd>
+        </m:mtr>
+       </m:mtable>
+      </xsl:when>
+      <!-- inductive_case -->
+      <xsl:when test="$name='inductive_case'">
+       <m:mtable align="baseline 1" equalrows="false" columnalign="left">
+        <m:mtr>
+         <m:mtd>
+          <m:mrow>
+           <m:mtext mathcolor="red">Case </m:mtext>
+           <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+           <xsl:apply-templates select="*[2]"/>
+          </m:mrow>
+         </m:mtd>
+        </m:mtr>
+        <m:mtr>
+         <m:mtd>
+          <m:mrow>
+           <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+           <m:mtable align="baseline 1" equalrows="false" columnalign="left">
+            <xsl:if test="*[3]/*[position()>1]">
+             <m:mtr>
+              <m:mtd>
+               <m:mtext mathcolor="red">By induction hypothesis, we have:</m:mtext>
+              </m:mtd>
+             </m:mtr>
+             <m:mtr>
+              <m:mtd>
+               <m:mrow>
+                <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+                <xsl:for-each select="*[3]/*[position()>1]">
+                 <m:mo stretchy="false">(</m:mo>
+                 <xsl:apply-templates select="m:ci"/>
+                 <m:mo stretchy="false">) </m:mo>
+                 <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+                 <xsl:apply-templates select="m:type"/>
+                </xsl:for-each>
+               </m:mrow>
+              </m:mtd>
+             </m:mtr>
+            </xsl:if>
+            <m:mtr>
+             <m:mtd>
+              <xsl:apply-templates select="*[4]"/>
+             </m:mtd>
+            </m:mtr>
+           </m:mtable>
+          </m:mrow>
+         </m:mtd>
+        </m:mtr>
+       </m:mtable>
+      </xsl:when>
+      <!-- case_lhs  -->
+      <xsl:when test="$name='case_lhs'">
+       <m:mrow>
+        <xsl:choose>
+         <xsl:when test="count(*)=2">
+          <xsl:apply-templates select="*[2]"/>
+         </xsl:when>
+         <xsl:otherwise>
+          <m:mo stretchy="false">(</m:mo>
+          <xsl:apply-templates select="*[2]"/>
+          <xsl:for-each select="m:bvar">
+           <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+           <xsl:apply-templates select="*[1]"/>
+           <m:mtext>:</m:mtext>
+           <xsl:apply-templates select="m:type/*[1]"/>
+          </xsl:for-each>
+          <m:mo stretchy="false">)</m:mo>
+         </xsl:otherwise>
+        </xsl:choose>
+       </m:mrow>
+      </xsl:when>
+      <xsl:when test="$name='false_ind'">
+       <m:mtable align="baseline 1" equalrows="false" columnalign="left">
+        <m:mtr>
+         <m:mtd>
+          <m:mrow>
+           <xsl:apply-templates select="*[3]"/>
+          </m:mrow>
+         </m:mtd>
+        </m:mtr>
+        <m:mtr>
+         <m:mtd>
+          <m:mrow>
+           <m:mtext mathcolor="Red">Contradiction.</m:mtext>
+          </m:mrow>
+         </m:mtd>
+        </m:mtr>
+       </m:mtable>
+      </xsl:when>
+      <!--CSC fine della parte da risistemare -->
+
+      <!-- LET-IN -->
       <xsl:when test="$name='letin'">
         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
          <!-- <xsl:for-each select="APPLY[m:csymbol and (string(m:csymbol)='let')]"> -->
@@ -1024,12 +1171,14 @@ which generates the toplevel element (see for instance xlink) -->
          </m:mtr>
         </m:mtable>
       </xsl:when>
+      <!-- LET -->
       <xsl:when test="$name='let'">
        <m:mtext>(</m:mtext>
        <xsl:apply-templates select="m:ci"/>
        <m:mtext>) </m:mtext>
        <xsl:apply-templates select="*[3]"/>
       </xsl:when>
+      <!-- RW_STEP -->
       <xsl:when test="$name='rw_step'">
         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
          <m:mtr>
@@ -1090,6 +1239,7 @@ which generates the toplevel element (see for instance xlink) -->
         </m:mtable>
       </xsl:when>
       --> 
+      <!-- REWRITE_AND_APPLY -->
       <xsl:when test="$name='rewrite_and_apply'">
         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
          <m:mtr>
@@ -1110,34 +1260,67 @@ which generates the toplevel element (see for instance xlink) -->
          </m:mtr>
        </m:mtable>
       </xsl:when>
-      <!-- NAT_IND -->
-      <xsl:when test="$name='nat_ind'">
+      <!-- AND_IND -->
+      <xsl:when test="$name='and_ind'">
         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
          <m:mtr>
           <m:mtd>
-           <m:mtext>By induction</m:mtext>
+           <m:mrow>
+            <xsl:choose>
+             <xsl:when test="name(*[2])='m:apply'">
+              <xsl:apply-templates select="*[2]"/>
+             </xsl:when>
+             <xsl:otherwise>
+              <m:mtext>Consider</m:mtext>
+              <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+              <xsl:apply-templates select="*[2]"/>
+             </xsl:otherwise>
+            </xsl:choose>
+           </m:mrow>
           </m:mtd>
          </m:mtr>
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext>base case:</m:mtext>
-            <xsl:apply-templates select="*[2]"/>
+            <m:mtext>In particular, we have</m:mtext>
            </m:mrow>
           </m:mtd>
          </m:mtr>
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext>inductive case:</m:mtext>
+            <m:mtext>(</m:mtext>
             <xsl:apply-templates select="*[3]"/>
+            <m:mtext>)</m:mtext>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+            <xsl:apply-templates select="*[4]"/>
+            </m:mrow>
+          </m:mtd>
+         </m:mtr>
+         <m:mtr>
+          <m:mtd>
+           <m:mrow>
+            <m:mtext>(</m:mtext>
+            <xsl:apply-templates select="*[5]"/>
+            <m:mtext>)</m:mtext>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+            <xsl:apply-templates select="*[6]"/>
+            </m:mrow>
+          </m:mtd>
+         </m:mtr>
+         <m:mtr>
+          <m:mtd>
+           <m:mrow>
+            <xsl:apply-templates select="*[7]"/>
            </m:mrow>
           </m:mtd>
          </m:mtr>
         </m:mtable>
       </xsl:when>
-      <!-- AND_IND -->
-      <xsl:when test="$name='and_ind'">
+      <!-- CSC: Il caso che segue e' stato buttato li' giusto per vedere -->
+      <!-- qualche cosa. Irene, appena puoi, risistemalo.                -->
+      <!-- full_or_ind -->
+      <xsl:when test="$name='full_or_ind'">
         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
          <m:mtr>
           <m:mtd>
@@ -1158,41 +1341,57 @@ which generates the toplevel element (see for instance xlink) -->
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext>In particular, we have</m:mtext>
+            <m:mtext>We proceed by cases to prove</m:mtext>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+            <xsl:apply-templates select="*[3]"/>
            </m:mrow>
           </m:mtd>
          </m:mtr>
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext>(</m:mtext>
-            <xsl:apply-templates select="*[3]"/>
-            <m:mtext>)</m:mtext>
+            <m:mtext>Left: suppose</m:mtext>
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-            <xsl:apply-templates select="*[4]"/>
-            </m:mrow>
+            <m:mo stretchy="false">(</m:mo>
+            <xsl:apply-templates select="*[4]/m:bvar/m:ci"/>
+            <m:mo stretchy="false">)</m:mo>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+            <xsl:apply-templates select="*[4]/m:bvar/m:type/*[1]"/>
+           </m:mrow>
           </m:mtd>
          </m:mtr>
          <m:mtr>
           <m:mtd>
+           <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
            <m:mrow>
-            <m:mtext>(</m:mtext>
-            <xsl:apply-templates select="*[5]"/>
-            <m:mtext>)</m:mtext>
+            <xsl:apply-templates select="*[4]/*[3]"/>
+           </m:mrow>
+          </m:mtd>
+         </m:mtr>
+         <m:mtr>
+          <m:mtd>
+           <m:mrow>
+            <m:mtext>Right: suppose</m:mtext>
             <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
-            <xsl:apply-templates select="*[6]"/>
-            </m:mrow>
+            <m:mo stretchy="false">(</m:mo>
+            <xsl:apply-templates select="*[5]/m:bvar/m:ci"/>
+            <m:mo stretchy="false">)</m:mo>
+            <m:mphantom><m:mtext>_</m:mtext></m:mphantom>
+            <xsl:apply-templates select="*[5]/m:bvar/m:type/*[1]"/>
+           </m:mrow>
           </m:mtd>
          </m:mtr>
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <xsl:apply-templates select="*[7]"/>
+            <xsl:apply-templates select="*[5]/*[3]"/>
            </m:mrow>
           </m:mtd>
          </m:mtr>
         </m:mtable>
       </xsl:when>
+      <!--CSC fine della parte da risistemare -->
+      <!-- OR_IND -->
       <xsl:when test="$name='or_ind'">
         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
          <m:mtr>
@@ -1225,7 +1424,7 @@ which generates the toplevel element (see for instance xlink) -->
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext>*</m:mtext>
+            <m:mtext>Left</m:mtext>
             <xsl:apply-templates select="*[4]"/>
            </m:mrow>
           </m:mtd>
@@ -1233,13 +1432,14 @@ which generates the toplevel element (see for instance xlink) -->
          <m:mtr>
           <m:mtd>
            <m:mrow>
-            <m:mtext>*</m:mtext>
+            <m:mtext>Right</m:mtext>
             <xsl:apply-templates select="*[5]"/>
            </m:mrow>
           </m:mtd>
          </m:mtr>
         </m:mtable>
       </xsl:when>
+      <!-- EX_IND -->
       <xsl:when test="$name='ex_ind'">
         <m:mtable align="baseline 1" equalrows="false" columnalign="left">
          <m:mtr>
@@ -1286,8 +1486,9 @@ which generates the toplevel element (see for instance xlink) -->
          </m:mtr>
         </m:mtable>
       </xsl:when>
+      <!-- ERROR -->
       <xsl:otherwise>
-       <m:ci>ERROR</m:ci>
+       <m:mi>ERROR</m:mi>
       </xsl:otherwise>
      </xsl:choose>
     </m:mrow>
diff --git a/helm/style/proofs.xsl b/helm/style/proofs.xsl
index a0302bde6..6ed01233d 100644
--- a/helm/style/proofs.xsl
+++ b/helm/style/proofs.xsl
@@ -157,32 +157,6 @@
   <xsl:when test="name()='APPLY'">
    <xsl:variable name="id" select="@id"/>
    <xsl:choose>
-    <!-- NATIND 3 parametri -->
-    <xsl:when test="CONST[attribute::uri='cic:/Coq/Init/Datatypes/nat_ind.con']              and count(child::*) = 4">
-     <m:apply>
-      <m:csymbol>nat_ind</m:csymbol>
-      <xsl:apply-templates mode="noannot" select="*[3]"/>
-      <xsl:apply-templates mode="noannot" select="*[4]"/>
-     </m:apply>
-    </xsl:when>
-    <!-- NATIND 4 parametri (nuova versione) -->
-    <!-- 
-    <xsl:when test="CONST[
- attribute::uri='cic:/Coq/Init/Datatypes/nat_ind.con'] 
- and count(child::*) = 5
- and name(*[4])='LAMBDA' 
- and name(*[4]/target/*[1])='LAMBDA'"> 
-     <m:apply>
-      <m:csymbol>nat_ind_complete</m:csymbol>
-      <xsl:apply-templates mode="noannot" select="*[5]"/>
-      <xsl:apply-templates mode="noannot" select="*[3]"/>
-      <m:ci><xsl:value-of select="*[4]/target/@binder"/></m:ci>
-      <m:ci><xsl:value-of select="*[4]/target/*[1]/target/@binder"/></m:ci>
-      <xsl:apply-templates mode="noannot" select="*[4]/target/*[1]/source/*"/>
-      <xsl:apply-templates mode="noannot" select="*[4]/target/*[1]/target/*"/>
-     </m:apply>
-    </xsl:when> 
-    -->
     <!-- EQUALITY -->
     <xsl:when test="CONST[
  attribute::uri='cic:/Coq/Init/Logic/Equality/eq_ind.con' or
-- 
2.39.2