From a094832a413d3d11cd4031b01a5119452384a7ac Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 20 Jun 2006 17:59:04 +0000
Subject: [PATCH] - fwd concrete syntax fixed - decompose, fwd, lapply
 documentation fixed

---
 components/grafite/grafiteAstPp.ml         |  2 +-
 components/grafite_parser/grafiteParser.ml |  2 +-
 matita/help/C/sec_tactics.xml              | 51 +++++++++++++++++-----
 matita/help/C/tactic_quickref.xml          |  8 +++-
 4 files changed, 49 insertions(+), 14 deletions(-)

diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml
index 9e1dffdcd..20d57ef9e 100644
--- a/components/grafite/grafiteAstPp.ml
+++ b/components/grafite/grafiteAstPp.ml
@@ -110,7 +110,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
        (lazy_term_pp term) (pp_tactic_pattern pattern)
   | FwdSimpl (_, hyp, idents) -> 
       sprintf "fwd %s%s" hyp 
-        (match idents with [] -> "" | idents -> " " ^ pp_idents idents)
+        (match idents with [] -> "" | idents -> " as " ^ pp_idents idents)
   | Generalize (_, pattern, ident) ->
      sprintf "generalize %s%s" (pp_tactic_pattern pattern)
       (match ident with None -> "" | Some id -> " as " ^ id)
diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 535e396a9..ad081d664 100644
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -178,7 +178,7 @@ EXTEND
          GrafiteAst.Fold (loc, kind, t, p)
     | IDENT "fourier" ->
         GrafiteAst.Fourier loc
-    | IDENT "fwd"; hyp = IDENT; idents = OPT ident_list0 ->
+    | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
         let idents = match idents with None -> [] | Some idents -> idents in
         GrafiteAst.FwdSimpl (loc, hyp, idents)
     | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
diff --git a/matita/help/C/sec_tactics.xml b/matita/help/C/sec_tactics.xml
index c10d2bd33..bc5095fae 100644
--- a/matita/help/C/sec_tactics.xml
+++ b/matita/help/C/sec_tactics.xml
@@ -389,7 +389,11 @@
         <varlistentry role="tactic.synopsis">
           <term>Synopsis:</term>
           <listitem>
-            <para><emphasis role="bold">decompose</emphasis> &id; [&id;]… &intros-spec;</para>
+            <para>
+	     <emphasis role="bold">decompose</emphasis>
+	     [<emphasis role="bold">(</emphasis>[&id;]…<emphasis role="bold">)</emphasis>]
+	     &id; &intros-spec;
+	    </para>
           </listitem>
         </varlistentry>
         <varlistentry>
@@ -750,13 +754,13 @@ its constructor takes no arguments.</para>
   <sect1 id="tac_fwd">
     <title>fwd</title>
     <titleabbrev>fwd</titleabbrev>
-    <para><userinput>fwd H</userinput></para>
+    <para><userinput>fwd H as H<subscript>0</subscript> ... H<subscript>n</subscript></userinput></para>
     <para>
       <variablelist>
         <varlistentry role="tactic.synopsis">
           <term>Synopsis:</term>
           <listitem>
-            <para><emphasis role="bold">fwd</emphasis> &id; [<emphasis role="bold">(</emphasis>[&id;]…<emphasis role="bold">)</emphasis>]</para>
+            <para><emphasis role="bold">fwd</emphasis> &id; [<emphasis role="bold">as</emphasis> &id; [&id;]…]</para>
           </listitem>
         </varlistentry>
         <varlistentry>
@@ -775,16 +779,23 @@ its constructor takes no arguments.</para>
 	     This tactic is under development.
              It simplifies the current context by removing
 	     <command>H</command> using the following methods:
-	     forward application of a suitable simplification theorem (chosen
-             automatically) of which the type of <command>H</command> is a
-             premise, decomposition, rewriting. 
+	     forward application (by <command>lapply</command>) of a suitable
+	     simplification theorem, chosen automatically, of which the type
+	     of <command>H</command> is a premise, 
+	     decomposition (by <command>decompose</command>),
+	     rewriting (by <command>rewrite</command>).
+	     <command>H<subscript>0</subscript> ... H<subscript>n</subscript></command>
+	     are passed to the tactics <command>fwd</command> invokes, as
+             names for the premise they introduce.
 	    </para>
           </listitem>
         </varlistentry>
         <varlistentry>
           <term>New sequents to prove:</term>
           <listitem>
-            <para>None.</para>
+            <para>
+	     The ones opened by the tactics <command>fwd</command> invokes.
+	    </para>
           </listitem>
         </varlistentry>
       </variablelist>
@@ -1043,19 +1054,39 @@ its constructor takes no arguments.</para>
         <varlistentry>
           <term>Pre-conditions:</term>
           <listitem>
-            <para>TODO.</para>
+            <para>
+	     <command>t</command> must have at least <command>d</command>
+	     independent premises and <command>n</command> must not be
+	     greater than <command>d</command>.
+	    </para>
           </listitem>
         </varlistentry>
         <varlistentry>
           <term>Action:</term>
           <listitem>
-            <para>TODO.</para>
+            <para>
+	     It invokes <command>letin H ≝ (t ? ... ?)</command>
+	     with enough <command>?</command>'s to reach the 
+	     <command>d</command>-th independent premise of
+	     <command>t</command>
+	     (<command>d</command> is maximum if unspecified).	     
+	     Then it istantiates (by <command>apply</command>) with
+	     t<subscript>1</subscript>, ..., t<subscript>n</subscript>
+	     the <command>?</command>'s corresponding to the first 
+	     <command>n</command> independent premises of
+	     <command>t</command>.
+	     Usually the other <command>?</command>'s preceding the 
+	     <command>n</command>-th independent premise of
+	     <command>t</command> are istantiated as a consequence.
+	    </para>
           </listitem>
         </varlistentry>
         <varlistentry>
           <term>New sequents to prove:</term>
           <listitem>
-            <para>TODO.</para>
+            <para>
+	     The ones opened by the tactics <command>lapply</command> invokes.
+	    </para>
           </listitem>
         </varlistentry>
       </variablelist>
diff --git a/matita/help/C/tactic_quickref.xml b/matita/help/C/tactic_quickref.xml
index e1f7eb434..6a735eee2 100644
--- a/matita/help/C/tactic_quickref.xml
+++ b/matita/help/C/tactic_quickref.xml
@@ -38,7 +38,11 @@
     <para><link linkend="tac_cut"><emphasis role="bold">cut</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>]</para>
   </listitem>
   <listitem>
-    <para><link linkend="tac_decompose"><emphasis role="bold">decompose</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis> [<emphasis><link linkend="grammar.id">id</link></emphasis>]… <emphasis><link linkend="grammar.intros-spec">intros-spec</link></emphasis></para>
+    <para>
+	     <link linkend="tac_decompose"><emphasis role="bold">decompose</emphasis></link>
+	     [<emphasis role="bold">(</emphasis>[<emphasis><link linkend="grammar.id">id</link></emphasis>]…<emphasis role="bold">)</emphasis>]
+	     <emphasis><link linkend="grammar.id">id</link></emphasis> <emphasis><link linkend="grammar.intros-spec">intros-spec</link></emphasis>
+	    </para>
   </listitem>
   <listitem>
     <para><link linkend="tac_demodulation"><emphasis role="bold">demodulation</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></para>
@@ -80,7 +84,7 @@
     </para>
   </listitem>
   <listitem>
-    <para><link linkend="tac_fwd"><emphasis role="bold">fwd</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis> [<emphasis role="bold">(</emphasis>[<emphasis><link linkend="grammar.id">id</link></emphasis>]…<emphasis role="bold">)</emphasis>]</para>
+    <para><link linkend="tac_fwd"><emphasis role="bold">fwd</emphasis></link> <emphasis><link linkend="grammar.id">id</link></emphasis> [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis> [<emphasis><link linkend="grammar.id">id</link></emphasis>]…]</para>
   </listitem>
   <listitem>
     <para><link linkend="tac_generalize"><emphasis role="bold">generalize</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis> [<emphasis role="bold">as</emphasis> <emphasis><link linkend="grammar.id">id</link></emphasis>]</para>
-- 
2.39.2