helm/software/matita/help/C/sec_terms.xml

   1
   2 <!-- =========== Terms, declarations and definitions ============ -->
   3
   4 <chapter id="sec_terms">
   5   <title>Syntax</title>
   6   <para>To describe syntax in this manual we use the following conventions:</para>
   7   <orderedlist>
   8     <listitem><para>Non terminal symbols are emphasized and have a link to their
   9         definition. E.g.: &term;</para></listitem>
  10     <listitem><para>Terminal symbols are in bold. E.g.:
  11         <emphasis role="bold">theorem</emphasis></para></listitem>
  12     <listitem><para>Optional sequences of elements are put in square brackets.
  13         E.g.: [<emphasis role="bold">in</emphasis> &term;]</para></listitem>
  14     <listitem><para>Alternatives are put in square brakets and they are
  15         separated by vertical bars. E.g.: [<emphasis role="bold">&lt;</emphasis>|<emphasis role="bold">&gt;</emphasis>]</para></listitem>
  16     <listitem><para>Repetitions of a sequence of elements are given by putting the
  17     sequence in square brackets, that are followed by three dots. The empty
  18     sequence is a valid repetition.
  19     E.g.: [<emphasis role="bold">and</emphasis> &term;]…</para></listitem>
  20     <listitem><para>Characters belonging to a set of characters are given
  21      by listing the set elements in square brackets. Hyphens are used to
  22      specify ranges of characters in the set.
  23      E.g.: [<emphasis role="bold">a</emphasis>-<emphasis role="bold">zA</emphasis>-<emphasis role="bold">Z0</emphasis>-<emphasis role="bold">9_-</emphasis>]</para></listitem>
  24   </orderedlist>
  25   <sect1 id="terms_and_co">
  26   <title>Terms &amp; co.</title>
  27   <sect2 id="lexical">
  28   <title>Lexical conventions</title>
  29     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
  30       <title>id</title>
  31       <tgroup cols="4">
  32       <tbody>
  33        <row>
  34         <entry id="grammar.id">&id;</entry>
  35         <entry>::=</entry>
  36         <entry><emphasis>〈〈any sequence of letters, underscores or valid <ulink type="http" url="http://www.w3.org/TR/2004/REC-xml-20040204/#NT-Digit">XML digits</ulink> prefixed by a latin letter ([a-zA-Z]) and post-fixed by a possible empty sequence of decorators ([?'`])〉〉</emphasis></entry>
  37        </row>
  38       </tbody>
  39      </tgroup>
  40     </table>
  41     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
  42       <title>nat</title>
  43       <tgroup cols="4">
  44       <tbody>
  45        <row>
  46         <entry id="grammar.nat">&nat;</entry>
  47         <entry>::=</entry>
  48         <entry><emphasis>〈〈any sequence of valid <ulink type="http" url="http://www.w3.org/TR/2004/REC-xml-20040204/#NT-Digit">XML digits</ulink>〉〉</emphasis></entry>
  49        </row>
  50       </tbody>
  51      </tgroup>
  52     </table>
  53     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
  54       <title>char</title>
  55       <tgroup cols="4">
  56       <tbody>
  57        <row>
  58         <entry id="grammar.char">&char;</entry>
  59         <entry>::=</entry>
  60         <entry>[<emphasis role="bold">a</emphasis>-<emphasis role="bold">zA</emphasis>-<emphasis role="bold">Z0</emphasis>-<emphasis role="bold">9_-</emphasis>]</entry>
  61        </row>
  62       </tbody>
  63      </tgroup>
  64     </table>
  65     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
  66       <title>uri-step</title>
  67       <tgroup cols="4">
  68       <tbody>
  69        <row>
  70         <entry id="grammar.uri-step">&uri-step;</entry>
  71         <entry>::=</entry>
  72         <entry>&char;[&char;]…</entry>
  73        </row>
  74       </tbody>
  75      </tgroup>
  76     </table>
  77     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
  78       <title>uri</title>
  79       <tgroup cols="4">
  80       <tbody>
  81        <row>
  82         <entry id="grammar.uri">&uri;</entry>
  83         <entry>::=</entry>
  84         <entry>[<emphasis role="bold">cic:/</emphasis>|<emphasis role="bold">theory:/</emphasis>]&uri-step;[<emphasis role="bold">/</emphasis>&uri-step;]…<emphasis role="bold">.</emphasis>&id;[<emphasis role="bold">.</emphasis>&id;]…[<emphasis role="bold">#xpointer(</emphasis>&nat;<emphasis role="bold">/</emphasis>&nat;[<emphasis role="bold">/</emphasis>&nat;]…<emphasis role="bold">)</emphasis>]</entry>
  85        </row>
  86       </tbody>
  87      </tgroup>
  88     </table>
  89   </sect2>
  90   <sect2 id="terms">
  91   <title>Terms</title>
  92
  93   <!-- ZACK: Sample EBNF snippet, see:
  94   http://www.docbook.org/tdg/en/html/productionset.html -->
  95   <!--
  96   <productionset>
  97     <title>Terms</title>
  98     <production id="grammar.term">
  99       <lhs>&term;</lhs>
 100       <rhs>&sterm;</rhs>
 101       <lineannotation></lineannotation>
 102     </production>
 103   </productionset>
 104   -->
 105
 106   <para>
 107   <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 108     <title>Terms</title>
 109     <tgroup cols="4">
 110     <tbody>
 111      <row>
 112       <entry id="grammar.term">&term;</entry>
 113       <entry>::=</entry>
 114       <entry>&sterm;</entry>
 115       <entry>simple or delimited term</entry>
 116      </row>
 117      <row>
 118       <entry/>
 119       <entry>|</entry>
 120       <entry>&term; &term;</entry>
 121       <entry>application</entry>
 122      </row>
 123      <row>
 124       <entry/>
 125       <entry>|</entry>
 126       <entry><emphasis role="bold">λ</emphasis>&args;<emphasis role="bold">.</emphasis>&term;</entry>
 127       <entry>λ-abstraction</entry>
 128      </row>
 129      <row>
 130       <entry/>
 131       <entry>|</entry>
 132       <entry><emphasis role="bold">Π</emphasis>&args;<emphasis role="bold">.</emphasis>&term;</entry>
 133       <entry>dependent product meant to define a datatype</entry>
 134      </row>
 135      <row>
 136       <entry/>
 137       <entry>|</entry>
 138       <entry><emphasis role="bold">∀</emphasis>&args;<emphasis role="bold">.</emphasis>&term;</entry>
 139       <entry>dependent product meant to define a proposition</entry>
 140      </row>
 141      <row>
 142       <entry/>
 143       <entry>|</entry>
 144       <entry>&term; <emphasis role="bold">→</emphasis> &term;</entry>
 145       <entry>non-dependent product (logical implication or function space)</entry>
 146      </row>
 147      <row>
 148       <entry/>
 149       <entry>|</entry>
 150       <entry><emphasis role="bold">let</emphasis> [&id;|(&id;<emphasis role="bold">:</emphasis> &term;)] <emphasis role="bold">≝</emphasis> &term; <emphasis role="bold">in</emphasis> &term;</entry>
 151       <entry>local definition</entry>
 152      </row>
 153      <row>
 154       <entry/>
 155       <entry>|</entry>
 156       <entry>
 157         <emphasis role="bold">let</emphasis>
 158         [<emphasis role="bold">co</emphasis>]<emphasis role="bold">rec</emphasis>
 159         &rec_def;
 160       </entry>
 161       <entry>(co)recursive definitions</entry>
 162      </row>
 163      <row>
 164       <entry/>
 165       <entry/>
 166       <entry>
 167       [<emphasis role="bold">and</emphasis> &rec_def;]…
 168       </entry>
 169       <entry/>
 170      </row>
 171      <row>
 172       <entry/>
 173       <entry/>
 174       <entry>
 175       <emphasis role="bold">in</emphasis> &term;
 176       </entry>
 177       <entry/>
 178      </row>
 179      <row>
 180       <entry/>
 181       <entry>|</entry>
 182       <entry>…</entry>
 183       <entry>user provided notation</entry>
 184      </row>
 185       <row>
 186         <entry id="grammar.rec_def">&rec_def;</entry>
 187         <entry>::=</entry>
 188         <entry>
 189           &id; [&id;|<emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&term;]… <emphasis role="bold">:</emphasis>&term;<emphasis role="bold">)</emphasis>]…
 190         </entry>
 191         <entry />
 192       </row>
 193       <row>
 194         <entry />
 195         <entry />
 196         <entry>
 197           [<emphasis role="bold">on</emphasis> &nat;]
 198           [<emphasis role="bold">:</emphasis> &term;]
 199           <emphasis role="bold">≝</emphasis> &term;]
 200         </entry>
 201         <entry />
 202       </row>
 203     </tbody>
 204    </tgroup>
 205   </table>
 206
 207   <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 208     <title>Simple terms</title>
 209     <tgroup cols="4">
 210     <tbody>
 211      <row>
 212       <entry id="grammar.sterm">&sterm;</entry>
 213       <entry>::=</entry>
 214       <entry><emphasis role="bold">(</emphasis>&term;<emphasis role="bold">)</emphasis></entry>
 215       <entry/>
 216      </row>
 217      <row>
 218       <entry/>
 219       <entry>|</entry>
 220       <entry>&id;[<emphasis role="bold">\subst[</emphasis>
 221        &id;<emphasis role="bold">≔</emphasis>&term;
 222        [<emphasis role="bold">;</emphasis>&id;<emphasis role="bold">≔</emphasis>&term;]…
 223        <emphasis role="bold">]</emphasis>]
 224       </entry>
 225       <entry>identifier with optional explicit named substitution</entry>
 226      </row>
 227      <row>
 228       <entry/>
 229       <entry>|</entry>
 230       <entry>&uri;</entry>
 231       <entry>a qualified reference</entry>
 232      </row>
 233      <row>
 234       <entry/>
 235       <entry>|</entry>
 236       <entry><emphasis role="bold">Prop</emphasis></entry>
 237       <entry>the impredicative sort of propositions</entry>
 238      </row>
 239      <row>
 240       <entry/>
 241       <entry>|</entry>
 242       <entry><emphasis role="bold">Set</emphasis></entry>
 243       <entry>the impredicate sort of datatypes</entry>
 244      </row>
 245      <row>
 246       <entry/>
 247       <entry>|</entry>
 248       <entry><emphasis role="bold">Type</emphasis></entry>
 249       <entry>one predicative sort of datatypes</entry>
 250      </row>
 251      <row>
 252       <entry/>
 253       <entry>|</entry>
 254       <entry><emphasis role="bold">?</emphasis></entry>
 255       <entry>implicit argument</entry>
 256      </row>
 257      <row>
 258       <entry/>
 259       <entry>|</entry>
 260       <entry><emphasis role="bold">?n</emphasis>
 261       [<emphasis role="bold">[</emphasis>
 262       [<emphasis role="bold">_</emphasis>|&term;]…
 263       <emphasis role="bold">]</emphasis>]</entry>
 264       <entry>metavariable</entry>
 265      </row>
 266      <row>
 267       <entry/>
 268       <entry>|</entry>
 269         <entry><emphasis role="bold">match</emphasis> &term;
 270         [ <emphasis role="bold">in</emphasis> &term; ]
 271         [ <emphasis role="bold">return</emphasis> &term; ]
 272         <emphasis role="bold">with</emphasis>
 273       </entry>
 274       <entry>case analysis</entry>
 275      </row>
 276      <row>
 277       <entry/>
 278       <entry/>
 279       <entry>
 280        <emphasis role="bold">[</emphasis>
 281        &match_branch;[<emphasis role="bold">|</emphasis>&match_branch;]…
 282        <emphasis role="bold">]</emphasis>
 283       </entry>
 284       <entry/>
 285      </row>
 286      <row>
 287       <entry/>
 288       <entry>|</entry>
 289       <entry><emphasis role="bold">(</emphasis>&term;<emphasis role="bold">:</emphasis>&term;<emphasis role="bold">)</emphasis></entry>
 290       <entry>cast</entry>
 291      </row>
 292      <row>
 293       <entry/>
 294       <entry>|</entry>
 295       <entry>…</entry>
 296       <entry>user provided notation at precedence 90</entry>
 297      </row>
 298     </tbody>
 299    </tgroup>
 300   </table>
 301
 302   <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 303     <title>Arguments</title>
 304     <tgroup cols="4">
 305     <tbody>
 306      <row>
 307       <entry id="grammar.args">&args;</entry>
 308       <entry>::=</entry>
 309       <entry>
 310        <emphasis role="bold">_</emphasis>[<emphasis role="bold">:</emphasis> &term;]
 311       </entry>
 312       <entry>ignored argument</entry>
 313      </row>
 314      <row>
 315       <entry/>
 316       <entry>|</entry>
 317       <entry>
 318        <emphasis role="bold">(</emphasis><emphasis role="bold">_</emphasis>[<emphasis role="bold">:</emphasis> &term;]<emphasis role="bold">)</emphasis>
 319       </entry>
 320       <entry>ignored argument</entry>
 321      </row>
 322      <row>
 323       <entry/>
 324       <entry>|</entry>
 325       <entry>&id;[<emphasis role="bold">,</emphasis>&id;]…[<emphasis role="bold">:</emphasis> &term;]</entry>
 326       <entry></entry>
 327      </row>
 328      <row>
 329       <entry/>
 330       <entry>|</entry>
 331       <entry><emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&id;]…[<emphasis role="bold">:</emphasis> &term;]<emphasis role="bold">)</emphasis></entry>
 332       <entry/>
 333      </row>
 334      <row>
 335       <entry id="grammar.args2">&args2;</entry>
 336       <entry>::=</entry>
 337       <entry>&id;</entry>
 338       <entry/>
 339      </row>
 340      <row>
 341       <entry/>
 342       <entry>|</entry>
 343       <entry><emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&id;]…<emphasis role="bold">:</emphasis> &term;<emphasis role="bold">)</emphasis></entry>
 344       <entry/>
 345      </row>
 346     </tbody>
 347    </tgroup>
 348   </table>
 349
 350   <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 351     <title>Pattern matching</title>
 352     <tgroup cols="4">
 353     <tbody>
 354       <row>
 355         <entry id="grammar.match_branch">&match_branch;</entry>
 356         <entry>::=</entry>
 357         <entry>&match_pattern; <emphasis role="bold">⇒</emphasis> &term;</entry>
 358         <entry />
 359       </row>
 360      <row>
 361       <entry id="grammar.match_pattern">&match_pattern;</entry>
 362       <entry>::=</entry>
 363       <entry>&id;</entry>
 364       <entry>0-ary constructor</entry>
 365      </row>
 366      <row>
 367       <entry/>
 368       <entry>|</entry>
 369       <entry><emphasis role="bold">(</emphasis>&id; &id; [&id;]…<emphasis role="bold">)</emphasis></entry>
 370       <entry>n-ary constructor (binds the n arguments)</entry>
 371      </row>
 372     </tbody>
 373    </tgroup>
 374   </table>
 375   </para>
 376
 377   </sect2>
 378   </sect1>
 379
 380   <sect1 id="axiom_definition_declaration">
 381    <title>Definitions and declarations</title>
 382    <sect2 id="axiom">
 383     <title><emphasis role="bold">axiom</emphasis> &id;<emphasis role="bold">:</emphasis> &term;</title>
 384     <titleabbrev>axiom</titleabbrev>
 385     <para><userinput>axiom H: P</userinput></para>
 386     <para><command>H</command> is declared as an axiom that states <command>P</command></para>
 387   </sect2>
 388   <sect2 id="definition">
 389     <title><emphasis role="bold">definition</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
 390     <titleabbrev>definition</titleabbrev>
 391     <para><userinput>definition f: T ≝ t</userinput></para>
 392     <para><command>f</command> is defined as <command>t</command>;
 393      <command>T</command> is its type. An error is raised if the type of
 394      <command>t</command> is not convertible to <command>T</command>.</para>
 395     <para><command>T</command> is inferred from <command>t</command> if
 396       omitted.</para>
 397     <para><command>t</command> can be omitted only if <command>T</command> is
 398      given. In this case Matita enters in interactive mode and
 399      <command>f</command> must be defined by means of tactics.</para>
 400     <para>Notice that the command is equivalent to <command>theorem f: T ≝ t</command>.</para>
 401   </sect2>
 402   <sect2 id="inductive">
 403     <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;]…
 404 [<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;]…]…
 405 </title>
 406     <titleabbrev>(co)inductive types declaration</titleabbrev>
 407     <para><userinput>inductive i x y z: S ≝ k1:T1 | … | kn:Tn with i' : S' ≝ k1':T1' | … | km':Tm'</userinput></para>
 408     <para>Declares a family of two mutually inductive types
 409      <command>i</command> and <command>i'</command> whose types are
 410      <command>S</command> and <command>S'</command>, which must be convertible
 411      to sorts.</para>
 412     <para>The constructors <command>ki</command> of type <command>Ti</command>
 413      and <command>ki'</command> of type <command>Ti'</command> are also
 414      simultaneously declared. The declared types <command>i</command> and
 415      <command>i'</command> may occur in the types of the constructors, but
 416      only in strongly positive positions according to the rules of the
 417      calculus.</para>
 418     <para>The whole family is parameterized over the arguments <command>x,y,z</command>.</para>
 419     <para>If the keyword <command>coinductive</command> is used, the declared
 420      types are considered mutually coinductive.</para>
 421     <para>Elimination principles for the record are automatically generated
 422      by Matita, if allowed by the typing rules of the calculus according to
 423      the sort <command>S</command>. If generated,
 424      they are named <command>i_ind</command>, <command>i_rec</command> and
 425      <command>i_rect</command> according to the sort of their induction
 426      predicate.</para>
 427   </sect2>
 428   <sect2 id="record">
 429     <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>
 430     <titleabbrev>record</titleabbrev>
 431     <para><userinput>record id x y z: S ≝ { f1: T1; …; fn:Tn }</userinput></para>
 432     <para>Declares a new record family <command>id</command> parameterized over
 433      <command>x,y,z</command>.</para>
 434     <para><command>S</command> is the type of the record
 435      and it must be convertible to a sort.</para>
 436     <para>Each field <command>fi</command> is declared by giving its type
 437      <command>Ti</command>. A record without any field is admitted.</para>
 438     <para>Elimination principles for the record are automatically generated
 439      by Matita, if allowed by the typing rules of the calculus according to
 440      the sort <command>S</command>. If generated,
 441      they are named <command>i_ind</command>, <command>i_rec</command> and
 442      <command>i_rect</command> according to the sort of their induction
 443      predicate.</para>
 444     <para>For each field <command>fi</command> a record projection
 445      <command>fi</command> is also automatically generated if projection
 446      is allowed by the typing rules of the calculus according to the
 447      sort <command>S</command>, the type <command>T1</command> and
 448      the definability of depending record projections.</para>
 449     <para>If the type of a field is declared with <command>:&gt;</command>,
 450      the corresponding record projection becomes an implicit coercion.
 451      This is just syntactic sugar and it has the same effect of declaring the
 452      record projection as a coercion later on.</para>
 453   </sect2>
 454   </sect1>
 455
 456   <sect1 id="proofs">
 457    <title>Proofs</title>
 458    <sect2 id="theorem">
 459     <title><emphasis role="bold">theorem</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
 460     <titleabbrev>theorem</titleabbrev>
 461     <para><userinput>theorem f: P ≝ p</userinput></para>
 462     <para>Proves a new theorem <command>f</command> whose thesis is
 463      <command>P</command>.</para>
 464     <para>If <command>p</command> is provided, it must be a proof term for
 465      <command>P</command>. Otherwise an interactive proof is started.</para>
 466     <para><command>P</command> can be omitted only if the proof is not
 467      interactive.</para>
 468     <para>Proving a theorem already proved in the library is an error.
 469      To provide an alternative name and proof for the same theorem, use
 470      <command>variant f: P ≝ p</command>.</para>
 471     <para>A warning is raised if the name of the theorem cannot be obtained
 472       by mangling the name of the constants in its thesis.</para>
 473     <para>Notice that the command is equivalent to <command>definition f: T ≝ t</command>.</para>
 474    </sect2>
 475    <sect2 id="variant">
 476     <title><emphasis role="bold">variant</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
 477     <titleabbrev>variant</titleabbrev>
 478     <para><userinput>variant f: T ≝ t</userinput></para>
 479     <para>Same as <command>theorem f: T ≝ t</command>, but it does not
 480      complain if the theorem has already been proved. To be used to give
 481      an alternative name or proof to a theorem.</para>
 482    </sect2>
 483    <sect2 id="lemma">
 484     <title><emphasis role="bold">lemma</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
 485     <titleabbrev>lemma</titleabbrev>
 486     <para><userinput>lemma f: T ≝ t</userinput></para>
 487     <para>Same as <command>theorem f: T ≝ t</command></para>
 488    </sect2>
 489    <sect2 id="fact">
 490     <title><emphasis role="bold">fact</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
 491     <titleabbrev>fact</titleabbrev>
 492     <para><userinput>fact f: T ≝ t</userinput></para>
 493     <para>Same as <command>theorem f: T ≝ t</command></para>
 494    </sect2>
 495    <sect2 id="remark">
 496     <title><emphasis role="bold">remark</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &term;]</title>
 497     <titleabbrev>remark</titleabbrev>
 498     <para><userinput>remark f: T ≝ t</userinput></para>
 499     <para>Same as <command>theorem f: T ≝ t</command></para>
 500    </sect2>
 501   </sect1>
 502
 503   <sect1 id="tacticargs">
 504    <title>Tactic arguments</title>
 505    <para>This section documents the syntax of some recurring arguments for
 506     tactics.</para>
 507
 508     <sect2 id="introsspec">
 509     <title>intros-spec</title>
 510     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 511       <title>intros-spec</title>
 512       <tgroup cols="4">
 513       <tbody>
 514        <row>
 515         <entry id="grammar.intros-spec">&intros-spec;</entry>
 516         <entry>::=</entry>
 517         <entry>[&nat;] [<emphasis role="bold">(</emphasis>[&id;]…<emphasis role="bold">)</emphasis>]</entry>
 518        </row>
 519       </tbody>
 520      </tgroup>
 521     </table>
 522         <para>The natural number is the number of new hypotheses to be introduced. The list of identifiers gives the name for the first hypotheses.</para>
 523     </sect2>
 524
 525     <sect2 id="pattern">
 526     <title>pattern</title>
 527     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 528       <title>pattern</title>
 529       <tgroup cols="4">
 530       <tbody>
 531        <row>
 532         <entry id="grammar.pattern">&pattern;</entry>
 533         <entry>::=</entry>
 534         <entry>&TODO;</entry>
 535        </row>
 536       </tbody>
 537      </tgroup>
 538     </table>
 539         <para>&TODO;</para>
 540     </sect2>
 541
 542     <sect2 id="reduction-kind">
 543     <title>reduction-kind</title>
 544     <para>Reduction kinds are normalization functions that transform a term
 545      to a convertible but simpler one. Each reduction kind can be used both
 546      as a tactic argument and as a stand-alone tactic.</para>
 547     <table frame="topbot" rowsep="0" colsep="0" role="grammar">
 548       <title>reduction-kind</title>
 549       <tgroup cols="4">
 550       <tbody>
 551        <row>
 552         <entry id="grammar.reduction-kind">&reduction-kind;</entry>
 553         <entry>::=</entry>
 554         <entry><emphasis role="bold">demodulate</emphasis></entry>
 555        </row>
 556        <row>
 557         <entry/>
 558         <entry>|</entry>
 559         <entry><emphasis role="bold">normalize</emphasis></entry>
 560         <entry>Computes the βδιζ-normal form</entry>
 561        </row>
 562        <row>
 563         <entry/>
 564         <entry>|</entry>
 565         <entry><emphasis role="bold">reduce</emphasis></entry>
 566         <entry>Computes the βδιζ-normal form</entry>
 567        </row>
 568        <row>
 569         <entry/>
 570         <entry>|</entry>
 571         <entry><emphasis role="bold">simplify</emphasis></entry>
 572         <entry>Computes a form supposed to be simpler</entry>
 573        </row>
 574        <row>
 575         <entry/>
 576         <entry>|</entry>
 577         <entry><emphasis role="bold">unfold</emphasis> [&sterm;]</entry>
 578         <entry>δ-reduces the constant or variable if specified, or that
 579          in head position</entry>
 580        </row>
 581        <row>
 582         <entry/>
 583         <entry>|</entry>
 584         <entry><emphasis role="bold">whd</emphasis></entry>
 585         <entry>Computes the βδιζ-weak-head normal form</entry>
 586        </row>
 587       </tbody>
 588      </tgroup>
 589     </table>
 590     </sect2>
 591   </sect1>
 592
 593 </chapter>
 594