1 <!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -->
2 <!-- GNU General Public License for more details. -->
4 <!-- You should have received a copy of the GNU General Public License -->
5 <!-- along with HELM; if not, write to the Free Software -->
6 <!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston, -->
7 <!-- MA 02111-1307, USA. -->
9 <!-- For details, see the HELM World-Wide-Web page, -->
10 <!-- http://cs.unibo.it/helm/. -->
12 <!--******************************************************************-->
14 <!-- (completely) Revisited: february 2001, Andrea Asperti -->
15 <!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena -->
16 <!--******************************************************************-->
18 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
19 xmlns:m="http://www.w3.org/1998/Math/MathML"
20 xmlns:helm="http://www.cs.unibo.it/helm">
22 <xsl:template mode="proof_transform" match="APPLY[CONST[
23 attribute::uri='cic:/Coq/Init/Logic/eq_ind.con' or
24 attribute::uri='cic:/Coq/Init/Logic/eq_ind_r.con' or
25 attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
26 attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind_r.con' or
27 attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) = 7]">
28 <xsl:variable name="id" select="@id"/>
30 <m:csymbol>rw_step</m:csymbol>
31 <xsl:apply-templates mode="noannot" select="*[5]"/>
32 <xsl:apply-templates mode="pure" select="*[3]"/>
33 <xsl:apply-templates mode="pure" select="*[6]"/>
34 <xsl:call-template name="generate_side_proof">
35 <xsl:with-param name="proof" select="*[7]"/>
40 <xsl:template mode="proof_transform" match="APPLY[CONST[
41 attribute::uri='cic:/Coq/Init/Logic/eq_ind.con' or
42 attribute::uri='cic:/Coq/Init/Logic/eq_ind_r.con' or
43 attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind.con' or
44 attribute::uri='cic:/Coq/Init/Logic_Type/eqT_ind_r.con' or
45 attribute::uri='cic:/Coq/Zarith/auxiliary/eqT_ind_r.con'] and count(child::*) > 7]">
46 <xsl:variable name="no_extraproofs" select="count(*[position()>7 and @sort='Prop' and (name(.)='LAMBDA' or name(.)='LETIN' or name(.)='APPLY' or name(.)='MUTCASE' or name(.)='FIX' or name(.)='COFIX')])"/>
48 <xsl:when test="$no_extraproofs=0">
50 <m:csymbol>rewrite_and_apply</m:csymbol>
52 <m:csymbol>rw_step</m:csymbol>
53 <xsl:apply-templates mode="noannot" select="*[5]"/>
54 <xsl:apply-templates mode="pure" select="*[3]"/>
55 <xsl:apply-templates mode="pure" select="*[6]"/>
56 <xsl:call-template name="generate_side_proof">
57 <xsl:with-param name="proof" select="*[7]"/>
60 <xsl:apply-templates mode="noannot" select="*[position()>7]"/>
65 <xsl:when test="*[5]/@sort='Prop'">
66 <m:apply helm:xref="{@id}">
67 <m:csymbol>letin</m:csymbol>
69 <m:csymbol>let</m:csymbol>
71 <xsl:call-template name="insert_subscript">
72 <xsl:with-param name="node_value" select="'h1'"/>
75 <xsl:apply-templates mode="noannot" select="*[5]"/>
77 <xsl:call-template name="gen_let">
78 <xsl:with-param name="init_pos" select="1"/>
79 <xsl:with-param name="from" select="7"/>
82 <m:csymbol>rewrite_and_apply</m:csymbol>
84 <m:csymbol>rw_step</m:csymbol>
86 <xsl:call-template name="insert_subscript">
87 <xsl:with-param name="node_value" select="'h1'"/>
90 <xsl:apply-templates mode="pure" select="*[3]"/>
91 <xsl:apply-templates mode="pure" select="*[6]"/>
92 <xsl:call-template name="generate_side_proof">
93 <xsl:with-param name="proof" select="*[7]"/>
96 <xsl:apply-templates mode="flat" select="*[8]">
97 <xsl:with-param name="n">
98 <xsl:value-of select="2"/>
100 </xsl:apply-templates>
105 <m:apply helm:xref="{@id}">
106 <m:csymbol>letin</m:csymbol>
107 <xsl:call-template name="gen_let">
108 <xsl:with-param name="init_pos" select="0"/>
109 <xsl:with-param name="form" select="7"/>
112 <m:csymbol>rewrite_and_apply</m:csymbol>
114 <m:csymbol>rw_step</m:csymbol>
115 <xsl:apply-templates mode="pure" select="*[5]"/>
116 <xsl:apply-templates mode="pure" select="*[3]"/>
117 <xsl:apply-templates mode="pure" select="*[6]"/>
118 <xsl:call-template name="generate_side_proof">
119 <xsl:with-param name="proof" select="*[7]"/>
122 <xsl:apply-templates mode="flat" select="*[8]">
123 <xsl:with-param name="n">
124 <xsl:value-of select="1"/>
126 </xsl:apply-templates>