# HG changeset patch
# User oheimb
# Date 936634689 -7200
# Node ID 95a4af0e10a7f0bc82deca827b1b1c6cff1a0ffd
# Parent  9a74b57740d10b3ca9d419119c2a22f1893610a6
added ftac, eatac, datac, fatac

diff -r 9a74b57740d1 -r 95a4af0e10a7 doc-src/Ref/tactic.tex
--- a/doc-src/Ref/tactic.tex	Mon Sep 06 18:17:48 1999 +0200
+++ b/doc-src/Ref/tactic.tex	Mon Sep 06 18:18:09 1999 +0200
@@ -48,7 +48,7 @@
   elimination rules.  It resolves with a rule, proves its first premise by
   assumption, and finally \emph{deletes} that assumption from any new
   subgoals.  (To rotate a rule's premises,
-  see \texttt{rotate_prems} in~\S\ref{MiscellaneousForwardRules}.)
+  see \texttt{rotate_prems} in~{\S}\ref{MiscellaneousForwardRules}.)
 
 \item[\ttindexbold{dresolve_tac} {\it thms} {\it i}] 
   \index{forward proof}\index{destruct-resolution}
@@ -170,12 +170,16 @@
 \index{tactics!resolution}\index{tactics!assumption}
 \index{tactics!meta-rewriting}
 \begin{ttbox} 
-rtac     :      thm -> int -> tactic
-etac     :      thm -> int -> tactic
-dtac     :      thm -> int -> tactic
-atac     :             int -> tactic
-ares_tac : thm list -> int -> tactic
-rewtac   :      thm ->        tactic
+rtac     :      thm ->        int -> tactic
+etac     :      thm ->        int -> tactic
+dtac     :      thm ->        int -> tactic
+ftac     :      thm ->        int -> tactic
+atac     :                    int -> tactic
+eatac    :      thm -> int -> int -> tactic
+datac    :      thm -> int -> int -> tactic
+fatac    :      thm -> int -> int -> tactic
+ares_tac :      thm list   -> int -> tactic
+rewtac   :      thm ->               tactic
 \end{ttbox}
 These abbreviate common uses of tactics.
 \begin{ttdescription}
@@ -189,9 +193,25 @@
 abbreviates \hbox{\tt dresolve_tac [{\it thm}] {\it i}}, doing
 destruct-resolution.
 
+\item[\ttindexbold{ftac} {\it thm} {\it i}] 
+abbreviates \hbox{\tt forward_tac [{\it thm}] {\it i}}, doing
+destruct-resolution without deleting the assumption.
+
 \item[\ttindexbold{atac} {\it i}] 
 abbreviates \hbox{\tt assume_tac {\it i}}, doing proof by assumption.
 
+\item[\ttindexbold{eatac} {\it thm} {\it j} {\it i}] 
+performs \hbox{\tt etac {\it thm}} and then {\it j} times \texttt{atac}, 
+solving additionally {\it j}~premises of the rule {\it thm} by assumption.
+
+\item[\ttindexbold{datac} {\it thm} {\it j} {\it i}] 
+performs \hbox{\tt dtac {\it thm}} and then {\it j} times \texttt{atac}, 
+solving additionally {\it j}~premises of the rule {\it thm} by assumption.
+
+\item[\ttindexbold{fatac} {\it thm} {\it j} {\it i}] 
+performs \hbox{\tt ftac {\it thm}} and then {\it j} times \texttt{atac}, 
+solving additionally {\it j}~premises of the rule {\it thm} by assumption.
+
 \item[\ttindexbold{ares_tac} {\it thms} {\it i}] 
 tries proof by assumption and resolution; it abbreviates
 \begin{ttbox}
@@ -224,7 +244,7 @@
 
 \item[\ttindexbold{cut_inst_tac} {\it insts} {\it thm} {\it i}]
   instantiates the {\it thm} with the instantiations {\it insts}, as
-  described in \S\ref{res_inst_tac}.  It adds the resulting theorem as a
+  described in {\S}\ref{res_inst_tac}.  It adds the resulting theorem as a
   new assumption to subgoal~$i$. 
 
 \item[\ttindexbold{subgoal_tac} {\it formula} {\it i}] 
@@ -419,7 +439,7 @@
 
   Flex-flex constraints arise from difficult cases of higher-order
   unification.  To prevent this, use \ttindex{res_inst_tac} to instantiate
-  some variables in a rule~(\S\ref{res_inst_tac}).  Normally flex-flex
+  some variables in a rule~({\S}\ref{res_inst_tac}).  Normally flex-flex
   constraints can be ignored; they often disappear as unknowns get
   instantiated.
 \end{ttdescription}
@@ -473,7 +493,7 @@
 
 \item[\ttindexbold{bimatch_tac}] 
 is like {\tt biresolve_tac}, but performs matching: unknowns in the
-proof state are never updated (see~\S\ref{match_tac}).
+proof state are never updated (see~{\S}\ref{match_tac}).
 
 \item[\ttindexbold{subgoals_of_brl}({\it flag},{\it rule})] 
 returns the number of new subgoals that bi-res\-o\-lu\-tion would yield for the
diff -r 9a74b57740d1 -r 95a4af0e10a7 lib/scripts/expandshort.pl
--- a/lib/scripts/expandshort.pl	Mon Sep 06 18:17:48 1999 +0200
+++ b/lib/scripts/expandshort.pl	Mon Sep 06 18:18:09 1999 +0200
@@ -33,6 +33,7 @@
     s/\bauto *\(\)/by Auto_tac/sg;
     s/dresolve_tac *\[(\w+)\] */dtac $1 /sg;
     s/eresolve_tac *\[(\w+)\] */etac $1 /sg;
+    s/forward_tac *\[(\w+)\] */ftac $1 /sg;
     s/resolve_tac *\[(\w+)\] */rtac $1 /sg;
     s/rewrite_goals_tac *\[(\w+)\]( *)/rewtac $1$2/sg;
     s/rtac *\((\w+)\s+RS\s+ssubst\)\s+/stac $1 /sg;
diff -r 9a74b57740d1 -r 95a4af0e10a7 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Mon Sep 06 18:17:48 1999 +0200
+++ b/src/Pure/tactic.ML	Mon Sep 06 18:18:09 1999 +0200
@@ -30,17 +30,20 @@
   val compose_tac	: (bool * thm * int) -> int -> tactic 
   val cut_facts_tac	: thm list -> int -> tactic
   val cut_inst_tac	: (string*string)list -> thm -> int -> tactic   
+  val datac             : thm -> int -> int -> tactic
   val defer_tac 	: int -> tactic
   val distinct_subgoals_tac	: tactic
   val dmatch_tac	: thm list -> int -> tactic
   val dresolve_tac	: thm list -> int -> tactic
   val dres_inst_tac	: (string*string)list -> thm -> int -> tactic   
   val dtac		: thm -> int ->tactic
+  val eatac             : thm -> int -> int -> tactic
   val etac		: thm -> int ->tactic
   val eq_assume_tac	: int -> tactic   
   val ematch_tac	: thm list -> int -> tactic
   val eresolve_tac	: thm list -> int -> tactic
   val eres_inst_tac	: (string*string)list -> thm -> int -> tactic
+  val fatac             : thm -> int -> int -> tactic
   val filter_prems_tac  : (term -> bool) -> int -> tactic  
   val filter_thms	: (term*term->bool) -> int*term*thm list -> thm list
   val filt_resolve_tac	: thm list -> int -> int -> tactic
@@ -49,6 +52,7 @@
   val fold_tac		: thm list -> tactic
   val forward_tac	: thm list -> int -> tactic   
   val forw_inst_tac	: (string*string)list -> thm -> int -> tactic
+  val ftac		: thm -> int ->tactic
   val insert_tagged_brl : ('a*(bool*thm)) * 
                           (('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net) ->
                           ('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net
@@ -156,10 +160,14 @@
 fun dresolve_tac rls = eresolve_tac (map make_elim rls);
 
 (*Shorthand versions: for resolution with a single theorem*)
-fun rtac rl = resolve_tac [rl];
+val atac    =   assume_tac;
+fun rtac rl =  resolve_tac [rl];
+fun dtac rl = dresolve_tac [rl];
 fun etac rl = eresolve_tac [rl];
-fun dtac rl = dresolve_tac [rl];
-val atac = assume_tac;
+fun ftac rl =  forward_tac [rl];
+fun datac thm j = EVERY' (dtac thm::replicate j atac);
+fun eatac thm j = EVERY' (etac thm::replicate j atac);
+fun fatac thm j = EVERY' (ftac thm::replicate j atac);
 
 (*Use an assumption or some rules ... A popular combination!*)
 fun ares_tac rules = assume_tac  ORELSE'  resolve_tac rules;