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>
-   <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.
-    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>
-  <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>
-  <table>
-    <tgroup>
-     <thead />
+  <para>
+  <table frame="all" rowsep="0" colsep="0">
+    <title>Terms</title>
+    <tgroup cols="4">
     <tbody>
      <row>
       <entry id="term">&term;</entry>
@@ -144,9 +149,9 @@
    </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>
@@ -158,8 +163,8 @@
       <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>
@@ -241,31 +246,65 @@
    </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>
-       [<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>[<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>
+     <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>
 
-  <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>
@@ -282,6 +321,7 @@
     </tbody>
    </tgroup>
   </table>
+  </para>
 
   </sect2>
   </sect1>
@@ -289,13 +329,13 @@
   <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">
-    <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>;
@@ -309,16 +349,63 @@
     <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>
-    <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">
-    <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
@@ -335,7 +422,7 @@
     <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
@@ -343,19 +430,19 @@
      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">
-    <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">
-    <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>