# 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;