X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fhelp%2FC%2Fsec_tactics.xml;h=56037dde56bf7d59f20b4efc6d6b1f848a2b643a;hb=e43d7e9c2acfa6d1c74838ba15589833cfc275fc;hp=2e1f6f36565e8a32f32c921e63badaf964e26a36;hpb=522d835109b6df16e1c082ae128c0e08677cbb1b;p=helm.git
diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml
index 2e1f6f365..56037dde5 100644
--- a/helm/software/matita/help/C/sec_tactics.xml
+++ b/helm/software/matita/help/C/sec_tactics.xml
@@ -163,27 +163,40 @@
clear
clear
- clear H
+
+ clear H1 ... Hm
+
Synopsis:
- clear &id;
+
+ clear
+ &id; [&id;â¦]
+
Pre-conditions:
- H must be an hypothesis of the
- current sequent to prove.
+
+
+ H1 ... Hm
+ must be hypotheses of the
+ current sequent to prove.
+
Action:
- It hides the hypothesis H from the
- current sequent.
+
+ It hides the hypotheses
+
+ H1 ... Hm
+ from the current sequent.
+
@@ -382,14 +395,22 @@
decompose
decompose
- decompose (T1 ... Tn) H hips
+ decompose (T1 ... Tn)
+ H as H1 ... Hm
Synopsis:
- decompose &id; [&id;]⦠&intros-spec;
+
+ decompose
+ [(
+ &id;â¦
+ )]
+ [&id;]
+ [as &id;â¦]
+
@@ -408,9 +429,13 @@
Action:
- Runs elim H hyps, clears H and tries to run
- itself recursively on each new identifier introduced by
- elim in the opened sequents.
+ Runs
+ elim H H1 ... Hm
+ , clears H and tries to run itself
+ recursively on each new identifier introduced by
+ elim in the opened sequents.
+ If H is not provided tries this operation on
+ each premise in the current context.
@@ -425,16 +450,16 @@
-
- demodulation
- demodulation
- demodulation patt
+
+ demodulate
+ demodulate
+ demodulate
Synopsis:
- demodulation &pattern;
+ demodulate
@@ -750,31 +775,48 @@ its constructor takes no arguments.
fwd
fwd
- fwd ...TODO
+ fwd H as H0 ... Hn
Synopsis:
- fwd &id; [([&id;]â¦)]
+ fwd &id; [as &id; [&id;]â¦]
Pre-conditions:
- TODO.
+
+ The type of H must be the premise of a
+ forward simplification theorem.
+
Action:
- TODO.
+
+ This tactic is under development.
+ It simplifies the current context by removing
+ H using the following methods:
+ forward application (by lapply) of a suitable
+ simplification theorem, chosen automatically, of which the type
+ of H is a premise,
+ decomposition (by decompose),
+ rewriting (by rewrite).
+ H0 ... Hn
+ are passed to the tactics fwd invokes, as
+ names for the premise they introduce.
+
New sequents to prove:
- TODO.
+
+ The ones opened by the tactics fwd invokes.
+
@@ -857,7 +899,7 @@ its constructor takes no arguments.
injection
- injection
+ injection
injection p
@@ -1019,7 +1061,7 @@ its constructor takes no arguments.
lapply
lapply
- lapply depth=d t
+ lapply linear depth=d t
to t1, ..., tn as H
@@ -1027,25 +1069,59 @@ its constructor takes no arguments.
Synopsis:
- lapply [depth=&nat;] &sterm; [to &sterm; [&sterm;]â¦] [as &id;]
+
+ lapply
+ [linear]
+ [depth=&nat;]
+ &sterm;
+ [to
+ &sterm;
+ [,&sterm;â¦]
+ ]
+ [as &id;]
+
Pre-conditions:
- TODO.
+
+ t must have at least d
+ independent premises and n must not be
+ greater than d.
+
Action:
- TODO.
+
+ Invokes letin H â (t ? ... ?)
+ with enough ?'s to reach the
+ d-th independent premise of
+ t
+ (d is maximum if unspecified).
+ Then istantiates (by apply) with
+ t1, ..., tn
+ the ?'s corresponding to the first
+ n independent premises of
+ t.
+ Usually the other ?'s preceding the
+ n-th independent premise of
+ t are istantiated as a consequence.
+ If the linear flag is specified and if
+ t, t1, ..., tn
+ are (applications of) premises in the current context, they are
+ cleared.
+
New sequents to prove:
- TODO.
+
+ The ones opened by the tactics lapply invokes.
+