Attempt to make our markup respect the docbook specification(!), major changes

[helm.git] / helm / software / matita / help / C / sec_terms.xml

diff --git a/helm/software/matita/help/C/sec_terms.xml b/helm/software/matita/help/C/sec_terms.xml
index 45459572bfc20affb08754727e141ba99d7f8474..fbf8dd4ef9cb614c7dfb52eb4c2fa80e1ab210b2 100644 (file)
--- a/helm/software/matita/help/C/sec_terms.xml
+++ b/helm/software/matita/help/C/sec_terms.xml
@@ -5,62 +5,67 @@
   <title>Syntax</title>
   <para>To describe syntax in this manual we use the following conventions:</para>
   <orderedlist>
   <title>Syntax</title>
   <para>To describe syntax in this manual we use the following conventions:</para>
   <orderedlist>

-   <listitem>Non terminal symbols are emphasized and have a link to their definition. E.g.: &term;</listitem>
-   <listitem>Terminal symbols are in bold. E.g.: <emphasis role="bold">theorem</emphasis></listitem>
-   <listitem>Optional sequences of elements are put in square brackets.
-    E.g.: [<emphasis role="bold">in</emphasis> &term;]</listitem>
-   <listitem>Alternatives are put in square brakets and they are separated
-    by vertical bars. E.g.: [<emphasis role="bold">&lt;</emphasis>|<emphasis role="bold">&gt;</emphasis>]</listitem>
-   <listitem>Repetition of sequences of elements are given by putting the
+    <listitem><para>Non terminal symbols are emphasized and have a link to their
+       definition. E.g.: &term;</para></listitem>
+    <listitem><para>Terminal symbols are in bold. E.g.:
+       <emphasis role="bold">theorem</emphasis></para></listitem>
+    <listitem><para>Optional sequences of elements are put in square brackets.
+       E.g.: [<emphasis role="bold">in</emphasis> &term;]</para></listitem>
+    <listitem><para>Alternatives are put in square brakets and they are
+       separated by vertical bars. E.g.: [<emphasis role="bold">&lt;</emphasis>|<emphasis role="bold">&gt;</emphasis>]</para></listitem>
+    <listitem><para>Repetition of sequences of elements are given by putting the

     first sequence in square brackets, that are followed by three dots.
     first sequence in square brackets, that are followed by three dots.

-    E.g.: [<emphasis role="bold">and</emphasis> &term;]…</listitem>
+    E.g.: [<emphasis role="bold">and</emphasis> &term;]…</para></listitem>

   </orderedlist>
   <sect1 id="terms_and_co">
   <title>Terms &amp; co.</title>
   <sect2 id="lexical">
   <title>Lexical conventions</title>
   </orderedlist>
   <sect1 id="terms_and_co">
   <title>Terms &amp; co.</title>
   <sect2 id="lexical">
   <title>Lexical conventions</title>

-  <table>
-    <tgroup>
-     <thead />
-    <tbody>
-     <row>
-      <entry id="id">&id;</entry>
-      <entry>::=</entry>
-      <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
-     </row>
-    </tbody>
-   </tgroup>
-  </table>
-  <table>
-    <tgroup>
-     <thead />
-    <tbody>
-     <row>
-      <entry id="nat">&nat;</entry>
-      <entry>::=</entry>
-      <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
-     </row>
-    </tbody>
-   </tgroup>
-  </table>
-  <table>
-    <tgroup>
-     <thead />
-    <tbody>
-     <row>
-      <entry id="uri">&uri;</entry>
-      <entry>::=</entry>
-      <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
-     </row>
-    </tbody>
-   </tgroup>
-  </table>
+  <para>
+    <table frame="all" rowsep="0" colsep="0">
+      <title>id</title>
+      <tgroup cols="4">
+      <tbody>
+       <row>
+       <entry id="id">&id;</entry>
+       <entry>::=</entry>
+       <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
+       </row>
+      </tbody>
+     </tgroup>
+    </table>
+    <table frame="all" rowsep="0" colsep="0">
+      <title>nat</title>
+      <tgroup cols="4">
+      <tbody>
+       <row>
+       <entry id="nat">&nat;</entry>
+       <entry>::=</entry>
+       <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
+       </row>
+      </tbody>
+     </tgroup>
+    </table>
+    <table frame="all" rowsep="0" colsep="0">
+      <title>uri</title>
+      <tgroup cols="4">
+      <tbody>
+       <row>
+       <entry id="uri">&uri;</entry>
+       <entry>::=</entry>
+       <entry><emphasis>〈〈&TODO;〉〉</emphasis></entry>
+       </row>
+      </tbody>
+     </tgroup>
+    </table>
+  </para>

   </sect2>
   <sect2 id="terms">
   <title>Terms</title>
   </sect2>
   <sect2 id="terms">
   <title>Terms</title>

-  <table>
-    <tgroup>
-     <thead />
+  <para>
+  <table frame="all" rowsep="0" colsep="0">
+    <title>Terms</title>
+    <tgroup cols="4">

     <tbody>
      <row>
       <entry id="term">&term;</entry>
     <tbody>
      <row>
       <entry id="term">&term;</entry>


@@ -144,9 +149,9 @@
    </tgroup>
   </table>
 
    </tgroup>
   </table>
 

-  <table>
-    <tgroup>
-     <thead />
+  <table frame="all" rowsep="0" colsep="0">
+    <title>Simple terms</title>
+    <tgroup cols="4">

     <tbody>
      <row>
       <entry id="sterm">&sterm;</entry>
     <tbody>
      <row>
       <entry id="sterm">&sterm;</entry>


@@ -158,8 +163,8 @@
       <entry/>
       <entry>|</entry>
       <entry>&id;[<emphasis role="bold">\subst[</emphasis>
       <entry/>
       <entry>|</entry>
       <entry>&id;[<emphasis role="bold">\subst[</emphasis>

-       &id;<emphasis role="bold">â\89\9d</emphasis>&term;
-       [<emphasis role="bold">;</emphasis>&id;<emphasis role="bold">â\89\9d</emphasis>&term;]…
+       &id;<emphasis role="bold">â\89\94</emphasis>&term;
+       [<emphasis role="bold">;</emphasis>&id;<emphasis role="bold">â\89\94</emphasis>&term;]…

        <emphasis role="bold">]</emphasis>]
       </entry>
       <entry>identifier with optional explicit named substitution</entry>
        <emphasis role="bold">]</emphasis>]
       </entry>
       <entry>identifier with optional explicit named substitution</entry>


@@ -241,31 +246,65 @@
    </tgroup>
   </table>
 
    </tgroup>
   </table>
 

-  <table>
-    <tgroup>
-     <thead />
+  <table frame="all" rowsep="0" colsep="0">
+    <title>Arguments</title>
+    <tgroup cols="4">

     <tbody>
      <row>
       <entry id="args">&args;</entry>
       <entry>::=</entry>
       <entry>
     <tbody>
      <row>
       <entry id="args">&args;</entry>
       <entry>::=</entry>
       <entry>

-       [<emphasis role="bold">(</emphasis>]<emphasis role="bold">_</emphasis>[<emphasis role="bold">:</emphasis> &term;][<emphasis role="bold">)</emphasis>]
+       <emphasis role="bold">_</emphasis>[<emphasis role="bold">:</emphasis> &term;]

       </entry>
       <entry>ignored argument</entry>
      </row>
      <row>
       <entry/>
       <entry>|</entry>
       </entry>
       <entry>ignored argument</entry>
      </row>
      <row>
       <entry/>
       <entry>|</entry>

-      <entry>[<emphasis role="bold">(</emphasis>]&id;[<emphasis role="bold">,</emphasis>&id;]…[<emphasis role="bold">:</emphasis> &term;][<emphasis role="bold">)</emphasis>]</entry>
+      <entry>
+       <emphasis role="bold">(</emphasis><emphasis role="bold">_</emphasis>[<emphasis role="bold">:</emphasis> &term;]<emphasis role="bold">)</emphasis>
+      </entry>
+      <entry>ignored argument</entry>
+     </row>
+     <row>
+      <entry/>
+      <entry>|</entry>
+      <entry>&id;[<emphasis role="bold">,</emphasis>&id;]…[<emphasis role="bold">:</emphasis> &term;]</entry>

       <entry></entry>
      </row>
       <entry></entry>
      </row>

+     <row>
+      <entry/>
+      <entry>|</entry>
+      <entry><emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&id;]…[<emphasis role="bold">:</emphasis> &term;]<emphasis role="bold">)</emphasis></entry>
+      <entry/>
+     </row>
+    </tbody>
+   </tgroup>
+  </table>
+
+  <table frame="all" rowsep="0" colsep="0">
+    <title>Miscellaneous arguments</title>
+    <tgroup cols="4">
+    <tbody>
+     <row>
+      <entry id="args2">&args2;</entry>
+      <entry>::=</entry>
+      <entry>&id;</entry>
+      <entry/>
+     </row>
+     <row>
+      <entry/>
+      <entry>|</entry>
+      <entry><emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&id;]…<emphasis role="bold">:</emphasis> &term;<emphasis role="bold">)</emphasis></entry>
+      <entry/>
+     </row>

     </tbody>
    </tgroup>
   </table>
 
     </tbody>
    </tgroup>
   </table>
 

-  <table>
-    <tgroup>
-     <thead />
+  <table frame="all" rowsep="0" colsep="0">
+    <title>Pattern matching</title>
+    <tgroup cols="4">

     <tbody>
      <row>
       <entry id="match_pattern">&match_pattern;</entry>
     <tbody>
      <row>
       <entry id="match_pattern">&match_pattern;</entry>


@@ -282,6 +321,7 @@
     </tbody>
    </tgroup>
   </table>
     </tbody>
    </tgroup>
   </table>

+  </para>

 
   </sect2>
   </sect1>
 
   </sect2>
   </sect1>


@@ -289,13 +329,13 @@
   <sect1 id="axiom_definition_declaration">
    <title>Definitions and declarations</title>
    <sect2 id="axiom">
   <sect1 id="axiom_definition_declaration">
    <title>Definitions and declarations</title>
    <sect2 id="axiom">

-    <title>axiom &id;: &term;</title>
+    <title><emphasis role="bold">axiom</emphasis> &id;<emphasis role="bold">:</emphasis> &term;</title>

     <titleabbrev>axiom</titleabbrev>
     <para><userinput>axiom H: P</userinput></para>
     <para><command>H</command> is declared as an axiom that states <command>P</command></para>
   </sect2>
   <sect2 id="definition">
     <titleabbrev>axiom</titleabbrev>
     <para><userinput>axiom H: P</userinput></para>
     <para><command>H</command> is declared as an axiom that states <command>P</command></para>
   </sect2>
   <sect2 id="definition">

-    <title>definition &id;[: &term;] [≝ &term;]</title>
+    <title><emphasis role="bold">definition</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>

     <titleabbrev>definition</titleabbrev>
     <para><userinput>definition f: T ≝ t</userinput></para>
     <para><command>f</command> is defined as <command>t</command>;
     <titleabbrev>definition</titleabbrev>
     <para><userinput>definition f: T ≝ t</userinput></para>
     <para><command>f</command> is defined as <command>t</command>;


@@ -309,16 +349,63 @@
     <para>Notice that the command is equivalent to <command>theorem f: T ≝ t</command>.</para>
   </sect2>
   <sect2 id="inductive">
     <para>Notice that the command is equivalent to <command>theorem f: T ≝ t</command>.</para>
   </sect2>
   <sect2 id="inductive">

-    <title>[co]inductive &id; (of inductive types)</title>
+    <title>[<emphasis role="bold">inductive</emphasis>|<emphasis role="bold">coinductive</emphasis>] &id; [&args2;]… <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">≝</emphasis> [<emphasis role="bold">|</emphasis>] [&id;<emphasis role="bold">:</emphasis>&term;] [<emphasis role="bold">|</emphasis> &id;<emphasis role="bold">:</emphasis>&term;]…
+[<emphasis role="bold">with</emphasis> &id; <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">≝</emphasis> [<emphasis role="bold">|</emphasis>] [&id;<emphasis role="bold">:</emphasis>&term;] [<emphasis role="bold">|</emphasis> &id;<emphasis role="bold">:</emphasis>&term;]…]…
+</title>

     <titleabbrev>(co)inductive types declaration</titleabbrev>
     <titleabbrev>(co)inductive types declaration</titleabbrev>

-    <para> &TODO; </para>
+    <para><userinput>inductive i x y z: S ≝ k1:T1 | … | kn:Tn with i' : S' ≝ k1':T1' | … | km':Tm'</userinput></para>
+    <para>Declares a family of two mutually inductive types
+     <command>i</command> and <command>i'</command> whose types are
+     <command>S</command> and <command>S'</command>, which must be convertible
+     to sorts.</para>
+    <para>The constructors <command>ki</command> of type <command>Ti</command>
+     and <command>ki'</command> of type <command>Ti'</command> are also
+     simultaneously declared. The declared types <command>i</command> and
+     <command>i'</command> may occur in the types of the constructors, but
+     only in strongly positive positions according to the rules of the
+     calculus.</para>
+    <para>The whole family is parameterized over the arguments <command>x,y,z</command>.</para>
+    <para>If the keyword <command>coinductive</command> is used, the declared
+     types are considered mutually coinductive.</para>
+    <para>Elimination principles for the record are automatically generated
+     by Matita, if allowed by the typing rules of the calculus according to
+     the sort <command>S</command>. If generated,
+     they are named <command>i_ind</command>, <command>i_rec</command> and
+     <command>i_rect</command> according to the sort of their induction
+     predicate.</para> 
+  </sect2>
+  <sect2 id="record">
+    <title><emphasis role="bold">record</emphasis> &id; [&args2;]… <emphasis role="bold">:</emphasis> &term; <emphasis role="bold">≝</emphasis><emphasis role="bold">{</emphasis>[&id; [<emphasis role="bold">:</emphasis>|<emphasis role="bold">:&gt;</emphasis>] &term;] [<emphasis role="bold">;</emphasis>&id; [<emphasis role="bold">:</emphasis>|<emphasis role="bold">:&gt;</emphasis>] &term;]…<emphasis role="bold">}</emphasis></title>
+    <titleabbrev>record</titleabbrev>
+    <para><userinput>record id x y z: S ≝ { f1: T1; …; fn:Tn }</userinput></para>
+    <para>Declares a new record family <command>id</command> parameterized over
+     <command>x,y,z</command>.</para>
+    <para><command>S</command> is the type of the record
+     and it must be convertible to a sort.</para>
+    <para>Each field <command>fi</command> is declared by giving its type
+     <command>Ti</command>. A record without any field is admitted.</para>
+    <para>Elimination principles for the record are automatically generated
+     by Matita, if allowed by the typing rules of the calculus according to
+     the sort <command>S</command>. If generated,
+     they are named <command>i_ind</command>, <command>i_rec</command> and
+     <command>i_rect</command> according to the sort of their induction
+     predicate.</para> 
+    <para>For each field <command>fi</command> a record projection
+     <command>fi</command> is also automatically generated if projection
+     is allowed by the typing rules of the calculus according to the
+     sort <command>S</command>, the type <command>T1</command> and
+     the definability of depending record projections.</para>
+    <para>If the type of a field is declared with <command>:&gt;</command>,
+     the corresponding record projection becomes an implicit coercion.
+     This is just syntactic sugar and it has the same effect of declaring the
+     record projection as a coercion later on.</para>

   </sect2>
   </sect1>
 
   <sect1 id="proofs">
    <title>Proofs</title>
    <sect2 id="theorem">
   </sect2>
   </sect1>
 
   <sect1 id="proofs">
    <title>Proofs</title>
    <sect2 id="theorem">

-    <title>theorem &id;[: &term;] [≝ &term;]</title>
+    <title><emphasis role="bold">theorem</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>

     <titleabbrev>theorem</titleabbrev>
     <para><userinput>theorem f: P ≝ p</userinput></para>
     <para>Proves a new theorem <command>f</command> whose thesis is
     <titleabbrev>theorem</titleabbrev>
     <para><userinput>theorem f: P ≝ p</userinput></para>
     <para>Proves a new theorem <command>f</command> whose thesis is


@@ -335,7 +422,7 @@
     <para>Notice that the command is equivalent to <command>definition f: T ≝ t</command>.</para>
    </sect2>
    <sect2 id="variant">
     <para>Notice that the command is equivalent to <command>definition f: T ≝ t</command>.</para>
    </sect2>
    <sect2 id="variant">

-    <title>variant &id;[: &term;] [≝ &term;]</title>
+    <title><emphasis role="bold">variant</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>

     <titleabbrev>variant</titleabbrev>
     <para><userinput>variant f: T ≝ t</userinput></para>
     <para>Same as <command>theorem f: T ≝ t</command>, but it does not
     <titleabbrev>variant</titleabbrev>
     <para><userinput>variant f: T ≝ t</userinput></para>
     <para>Same as <command>theorem f: T ≝ t</command>, but it does not


@@ -343,19 +430,19 @@
      an alternative name or proof to a theorem.</para>
    </sect2>
    <sect2 id="lemma">
      an alternative name or proof to a theorem.</para>
    </sect2>
    <sect2 id="lemma">

-    <title>lemma &id;[: &term;] [≝ &term;]</title>
+    <title><emphasis role="bold">lemma</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>

     <titleabbrev>lemma</titleabbrev>
     <para><userinput>lemma f: T ≝ t</userinput></para>
     <para>Same as <command>theorem f: T ≝ t</command></para>
    </sect2>
    <sect2 id="fact">
     <titleabbrev>lemma</titleabbrev>
     <para><userinput>lemma f: T ≝ t</userinput></para>
     <para>Same as <command>theorem f: T ≝ t</command></para>
    </sect2>
    <sect2 id="fact">

-    <title>fact &id;[: &term;] [≝ &term;]</title>
+    <title><emphasis role="bold">fact</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>

     <titleabbrev>fact</titleabbrev>
     <para><userinput>fact f: T ≝ t</userinput></para>
     <para>Same as <command>theorem f: T ≝ t</command></para>
    </sect2>
    <sect2 id="remark">
     <titleabbrev>fact</titleabbrev>
     <para><userinput>fact f: T ≝ t</userinput></para>
     <para>Same as <command>theorem f: T ≝ t</command></para>
    </sect2>
    <sect2 id="remark">

-    <title>remark &id;[: &term;] [≝ &term;]</title>
+    <title><emphasis role="bold">remark</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>

     <titleabbrev>remark</titleabbrev>
     <para><userinput>remark f: T ≝ t</userinput></para>
     <para>Same as <command>theorem f: T ≝ t</command></para>
     <titleabbrev>remark</titleabbrev>
     <para><userinput>remark f: T ≝ t</userinput></para>
     <para>Same as <command>theorem f: T ≝ t</command></para>