X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_terms.xml;h=945a43837bcfb79db57081fbb359579a1ec12be3;hb=8752fac73a864c821b6954f0572bce2052924183;hp=ab26aae4872f133d42ef74fcb32f3e389f9b32eb;hpb=ce3086647682ebfa15e9e8abaacd6e817449cea2;p=helm.git

diff --git a/helm/software/matita/help/C/sec_terms.xml b/helm/software/matita/help/C/sec_terms.xml
index ab26aae48..945a43837 100644
--- a/helm/software/matita/help/C/sec_terms.xml
+++ b/helm/software/matita/help/C/sec_terms.xml
@@ -188,6 +188,7 @@
 	<entry>
 	  &id; [&id;|<emphasis role="bold">(</emphasis>&id;[<emphasis role="bold">,</emphasis>&term;]… <emphasis role="bold">:</emphasis>&term;<emphasis role="bold">)</emphasis>]…
 	</entry>
+	<entry />
       </row>
       <row>
 	<entry />
@@ -197,6 +198,7 @@
 	  [<emphasis role="bold">:</emphasis> &term;]
 	  <emphasis role="bold">≝</emphasis> &term;]
 	</entry>
+	<entry />
       </row>
     </tbody>
    </tgroup>
@@ -240,6 +242,12 @@
       <entry><emphasis role="bold">Set</emphasis></entry>
       <entry>the impredicate sort of datatypes</entry>
      </row>
+     <row>
+      <entry/>
+      <entry>|</entry>
+      <entry><emphasis role="bold">CProp</emphasis></entry>
+      <entry>one fixed predicative sort of constructive propositions</entry>
+     </row>
      <row>
       <entry/>
       <entry>|</entry>
@@ -353,6 +361,7 @@
 	<entry id="grammar.match_branch">&match_branch;</entry>
 	<entry>::=</entry>
 	<entry>&match_pattern; <emphasis role="bold">⇒</emphasis> &term;</entry>
+	<entry />
       </row>
      <row>
       <entry id="grammar.match_pattern">&match_pattern;</entry>
@@ -470,7 +479,7 @@
     <para>Notice that the command is equivalent to <command>definition f: T ≝ t</command>.</para>
    </sect2>
    <sect2 id="variant">
-    <title><emphasis role="bold">variant</emphasis> &id;[<emphasis role="bold">:</emphasis> &term;] [<emphasis role="bold">≝</emphasis> &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
@@ -528,12 +537,98 @@
        <row>
 	<entry id="grammar.pattern">&pattern;</entry>
 	<entry>::=</entry>
-        <entry>&TODO;</entry>
+        <entry><emphasis role="bold">in</emphasis>
+          [&id;[<emphasis role="bold">:</emphasis> &path;]]…
+          [<emphasis role="bold">⊢</emphasis> &path;]]</entry>
+        <entry>simple pattern</entry>
+       </row>
+       <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><emphasis role="bold">in match</emphasis> &term;
+          [<emphasis role="bold">in</emphasis>
+          [&id;[<emphasis role="bold">:</emphasis> &path;]]…
+          [<emphasis role="bold">⊢</emphasis> &path;]]</entry>
+        <entry>full pattern</entry>
+       </row>
+      </tbody>
+     </tgroup>
+    </table>
+    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+      <title>path</title>
+      <tgroup cols="4">
+      <tbody>
+       <row>
+	<entry id="grammar.path">&path;</entry>
+	<entry>::=</entry>
+        <entry><emphasis>〈〈any &sterm; whithout occurrences of <emphasis role="bold">Set</emphasis>, <emphasis role="bold">Prop</emphasis>, <emphasis role="bold">CProp</emphasis>, <emphasis role="bold">Type</emphasis>, &id;, &uri; and user provided notation; however, <emphasis role="bold">%</emphasis> is now an additional production for &sterm;〉〉</emphasis></entry>
        </row>
       </tbody>
      </tgroup>
     </table>
-        <para>&TODO;</para>
+    <para>A <emphasis>path</emphasis> locates zero or more subterms of a given term by mimicking the term structure up to:</para>
+    <orderedlist>
+      <listitem><para>Occurrences of the subterms to locate that are
+       represented by <emphasis role="bold">%</emphasis>.</para></listitem>
+      <listitem><para>Subterms without any occurrence of subterms to locate
+       that can be represented by <emphasis role="bold">?</emphasis>.
+       </para></listitem>
+    </orderedlist>
+    <para>For instance, the path
+      <userinput>∀_,_:?.(? ? % ?)→(? ? ? %)</userinput>
+       locates at once the subterms
+      <userinput>x+y</userinput> and <userinput>x*y</userinput> in the
+      term <userinput>∀x,y:nat.x+y=1→0=x*y</userinput>
+      (where the notation <userinput>A=B</userinput> hides the term
+      <userinput>(eq T A B)</userinput> for some type <userinput>T</userinput>).
+    </para>
+    <para>A <emphasis>simple pattern</emphasis> extends paths to locate
+     subterms in a whole sequent. In particular, the pattern
+     <userinput>in H: p  K: q ⊢ r</userinput> locates at once all the subterms
+     located by the pattern <userinput>r</userinput> in the conclusion of the
+     sequent and by the patterns <userinput>p</userinput> and
+     <userinput>q</userinput> in the hypotheses <userinput>H</userinput>
+     and <userinput>K</userinput> of the sequent.
+    </para>
+    <para>If no list of hypotheses is provided in a simple pattern, no subterm
+     is selected in the hypothesis. If the <userinput>⊢ p</userinput>
+     part of the pattern is not provided, no subterm will be matched in the
+     conclusion if at least one hypothesis is provided; otherwise the whole
+     conclusion is selected.
+    </para>
+    <para>Finally, a <emphasis>full pattern</emphasis> is interpreted in three
+     steps. In the first step the <userinput>match T in</userinput>
+     part is ignored and a set <emphasis>S</emphasis> of subterms is
+     located as for the case of
+     simple patterns. In the second step the term <userinput>T</userinput>
+     is parsed and interpreted in the context of each subterm
+     <emphasis>s ∈ S</emphasis>. In the last term for each
+     <emphasis>s ∈ S</emphasis> the interpreted term <userinput>T</userinput>
+     computed in the previous step is looked for. The final set of subterms
+     located by the full pattern is the set of occurrences of
+     the interpreted <userinput>T</userinput> in the subterms <emphasis>s</emphasis>.
+    </para>
+    <para>A full pattern can always be replaced by a simple pattern,
+      often at the cost of increased verbosity or decreased readability.</para>
+    <para>Example: the pattern
+      <userinput>⊢ in match x+y in ∀_,_:?.(? ? % ?)</userinput>
+      locates only the first occurrence of <userinput>x+y</userinput>
+      in the sequent <userinput>x,y: nat ⊢ ∀z,w:nat. (x+y) * (z+w) =
+      z * (x+y) + w * (x+y)</userinput>. The corresponding simple pattern
+      is <userinput>⊢ ∀_,_:?.(? ? (? % ?) ?)</userinput>.
+    </para>
+    <para>Every tactic that acts on subterms of the selected sequents have
+     a pattern argument for uniformity. To automatically generate a simple
+     pattern:</para>
+    <orderedlist>
+     <listitem><para>Select in the current goal the subterms to pass to the
+      tactic by using the mouse. In order to perform a multiple selection of
+      subterms, hold the Ctrl key while selecting every subterm after the
+      first one.</para></listitem>
+     <listitem><para>From the contextual menu select &quot;Copy&quot;.</para></listitem>
+     <listitem><para>From the &quot;Edit&quot; or the contextual menu select
+      &quot;Paste as pattern&quot;</para></listitem>
+    </orderedlist>
     </sect2>
 
     <sect2 id="reduction-kind">
@@ -548,11 +643,6 @@
        <row>
 	<entry id="grammar.reduction-kind">&reduction-kind;</entry>
 	<entry>::=</entry>
-        <entry><emphasis role="bold">demodulate</emphasis></entry>
-       </row>
-       <row>
-        <entry/>
-        <entry>|</entry>
         <entry><emphasis role="bold">normalize</emphasis></entry>
         <entry>Computes the βδιζ-normal form</entry>
        </row>