1.1 --- a/doc-src/Ref/classical.tex Fri May 01 11:43:38 1998 +0200
1.2 +++ b/doc-src/Ref/classical.tex Fri May 01 19:51:03 1998 +0200
1.3 @@ -329,7 +329,7 @@
1.4 The first wrapper list, which is considered to contain safe wrappers only,
1.5 affects \ttindex{safe_step_tac} and all the tactics that call it.
1.6 The second one, which may contain unsafe wrappers, affects \ttindex{step_tac},
1.7 -\ttindex{slow_step_tac} and the tactics that call them.
1.8 +\ttindex{slow_step_tac}, and the tactics that call them.
1.9 A wrapper transforms each step of the search, for example
1.10 by invoking other tactics before or alternatively to the original step tactic.
1.11 All members of a wrapper list are applied in turn to the respective step tactic.
1.12 @@ -341,63 +341,79 @@
1.13
1.14 \begin{ttbox}
1.15 type wrapper = (int -> tactic) -> (int -> tactic);
1.16 +
1.17 +addSWrapper : claset * (string * wrapper ) -> claset \hfill{\bf infix 4}
1.18 addSbefore : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
1.19 addSaltern : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
1.20 -addSWrapper : claset * (string * wrapper ) -> claset \hfill{\bf infix 4}
1.21 delSWrapper : claset * string -> claset \hfill{\bf infix 4}
1.22 +
1.23 +addWrapper : claset * (string * wrapper ) -> claset \hfill{\bf infix 4}
1.24 addbefore : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
1.25 addaltern : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4}
1.26 -addWrapper : claset * (string * wrapper ) -> claset \hfill{\bf infix 4}
1.27 delWrapper : claset * string -> claset \hfill{\bf infix 4}
1.28
1.29 +addSss : claset * simpset -> claset \hfill{\bf infix 4}
1.30 addss : claset * simpset -> claset \hfill{\bf infix 4}
1.31 \end{ttbox}
1.32 %
1.33 -\index{simplification!from classical reasoner} The wrapper tacticals
1.34 -underly the operator addss, which combines each search step by
1.35 -simplification. Strictly speaking, \texttt{addss} is not part of the
1.36 -classical reasoner. It should be defined when the simplifier is
1.37 -installed:
1.38 -\begin{ttbox}
1.39 -infix 4 addss;
1.40 -fun cs addss ss = cs addbefore asm_full_simp_tac ss;
1.41 -\end{ttbox}
1.42
1.43 \begin{ttdescription}
1.44 +\item[$cs$ addSWrapper $(name,wrapper)$] \indexbold{*addSWrapper}
1.45 +adds a new wrapper, which should yield a safe tactic,
1.46 +to modify the existing safe step tactic.
1.47 +
1.48 +\item[$cs$ addSbefore $(name,tac)$] \indexbold{*addSbefore}
1.49 +adds the given tactic as safe wrapper, such that it is
1.50 +applied {\em before} each safe step of the search.
1.51 +
1.52 +\item[$cs$ addSaltern $(name,tac)$] \indexbold{*addSaltern}
1.53 +adds the given tactic as safe wrapper, such that it is
1.54 +applied when a safe step of the search would fail.
1.55 +
1.56 +\item[$cs$ delSWrapper $name$] \indexbold{*delSWrapper}
1.57 +deletes the safe wrapper with the given name.
1.58 +
1.59 +\item[$cs$ addWrapper $(name,wrapper)$] \indexbold{*addWrapper}
1.60 +adds a new wrapper to modify the existing (unsafe) step tactic.
1.61 +
1.62 +\item[$cs$ addbefore $(name,tac)$] \indexbold{*addbefore}
1.63 +adds the given tactic as unsafe wrapper, such that it is
1.64 +applied {\em before} each step of the search.
1.65 +
1.66 +\item[$cs$ addaltern $(name,tac)$] \indexbold{*addaltern}
1.67 +adds the given tactic as unsafe wrapper, such that it is
1.68 +applied when a step of the search would fail.
1.69 +
1.70 +\item[$cs$ delWrapper $name$] \indexbold{*delWrapper}
1.71 +deletes the unsafe wrapper with the given name.
1.72 +
1.73 +\item[$cs$ addSss $ss$] \indexbold{*addss}
1.74 +adds the simpset~$ss$ to the classical set. The assumptions and goal will be
1.75 +simplified, in a rather safe way, after each safe step of the search.
1.76 +
1.77 \item[$cs$ addss $ss$] \indexbold{*addss}
1.78 adds the simpset~$ss$ to the classical set. The assumptions and goal will be
1.79 -simplified, in a safe way, after the safe steps of the search.
1.80 +simplified, before the each unsafe step of the search.
1.81
1.82 -\item[$cs$ addSbefore $tac$] \indexbold{*addSbefore}
1.83 -changes the safe wrapper tactical to apply the given tactic {\em before}
1.84 -each safe step of the search.
1.85 +\end{ttdescription}
1.86
1.87 -\item[$cs$ addSaltern $tac$] \indexbold{*addSaltern}
1.88 -changes the safe wrapper tactical to apply the given tactic when a safe step
1.89 -of the search would fail.
1.90 -
1.91 -\item[$cs$ setSWrapper $tactical$] \indexbold{*setSWrapper}
1.92 -specifies a new safe wrapper tactical.
1.93 -
1.94 -\item[$cs$ compSWrapper $tactical$] \indexbold{*compSWrapper}
1.95 -composes the $tactical$ with the existing safe wrapper tactical,
1.96 -to combine their effects.
1.97 -
1.98 -\item[$cs$ addbefore $tac$] \indexbold{*addbefore}
1.99 -changes the (unsafe) wrapper tactical to apply the given tactic, which should
1.100 -be safe, {\em before} each step of the search.
1.101 -
1.102 -\item[$cs$ addaltern $tac$] \indexbold{*addaltern}
1.103 -changes the (unsafe) wrapper tactical to apply the given tactic
1.104 -{\em alternatively} after each step of the search.
1.105 -
1.106 -\item[$cs$ setWrapper $tactical$] \indexbold{*setWrapper}
1.107 -specifies a new (unsafe) wrapper tactical.
1.108 -
1.109 -\item[$cs$ compWrapper $tactical$] \indexbold{*compWrapper}
1.110 -composes the $tactical$ with the existing (unsafe) wrapper tactical,
1.111 -to combine their effects.
1.112 -\end{ttdescription}
1.113 +\index{simplification!from classical reasoner} The wrapper tacticals
1.114 +underly the operators addss and addSss, which are used as primitives
1.115 +for the automatic tactics described in \S\label{sec:automatic-tactics}.
1.116 +Strictly speaking, both operators are not part of the classical reasoner.
1.117 +They should be defined when the simplifier is installed:
1.118 +\begin{ttbox}
1.119 +infix 4 addSss addss;
1.120 +fun cs addSss ss = cs addSaltern ("safe_asm_full_simp_tac",
1.121 + CHANGED o (safe_asm_full_simp_tac ss));
1.122 +fun cs addss ss = cs addbefore ("asm_full_simp_tac", asm_full_simp_tac ss);
1.123 +\end{ttbox}
1.124 +\begin{warn}
1.125 +Being defined as wrappers, these operators are inappropriate for adding more
1.126 +than one simpset at a time: the simpset added last overwrites any earlier ones.
1.127 +When a simpset combined with a claset is to be augmented, this should done
1.128 +{\em before} combining it with the claset.
1.129 +\end{warn}
1.130
1.131
1.132 \section{The classical tactics}
1.133 @@ -473,22 +489,36 @@
1.134 \end{ttdescription}
1.135
1.136
1.137 -\subsection{An automatic tactic}
1.138 +\subsection{Automatic tactics}\label{sec:automatic-tactics}
1.139 \begin{ttbox}
1.140 -auto_tac : claset * simpset -> tactic
1.141 -auto : unit -> unit
1.142 +type clasimpset = claset * simpset;
1.143 +auto_tac : clasimpset -> tactic
1.144 +force_tac : clasimpset -> int -> tactic
1.145 +auto : unit -> unit
1.146 +force : int -> unit
1.147 \end{ttbox}
1.148 -The auto-tactic attempts to prove all subgoals using a combination of
1.149 -simplification and classical reasoning. It is intended for situations where
1.150 -there are a lot of mostly trivial subgoals; it proves all the easy ones,
1.151 -leaving the ones it cannot prove. (Unfortunately, attempting to prove the
1.152 -hard ones may take a long time.) It must be supplied both a simpset and a
1.153 -claset; therefore it is most easily called as \texttt{Auto_tac}, which uses
1.154 -the default claset and simpset (see \S\ref{sec:current-claset} below). For
1.155 -interactive use, the shorthand \texttt{auto();} abbreviates
1.156 +The automatic tactics attempt to prove goals using a combination of
1.157 +simplification and classical reasoning.
1.158 +\begin{itemize}
1.159 +\item[\ttindexbold{auto_tac $(cs,ss)$}] is intended for situations where
1.160 +there are a lot of mostly trivial subgoals; it proves all the easy ones,
1.161 +leaving the ones it cannot prove.
1.162 +(Unfortunately, attempting to prove the hard ones may take a long time.)
1.163 +\item[\ttindexbold{force_tac} $(cs,ss)$ $i$] is intended to prove subgoal~$i$
1.164 +completely. It tries to apply all fancy tactics it knows about,
1.165 +performing a rather exhaustive search.
1.166 +\end{itemize}
1.167 +They must be supplied both a simpset and a claset; therefore
1.168 +they are most easily called as \texttt{Auto_tac} and \texttt{Force_tac}, which
1.169 +use the default claset and simpset (see \S\ref{sec:current-claset} below).
1.170 +For interactive use, the shorthand \texttt{auto();} abbreviates
1.171 \begin{ttbox}
1.172 by Auto_tac;
1.173 \end{ttbox}
1.174 +while \texttt{force 1;} abbreviates
1.175 +\begin{ttbox}
1.176 +by (Force_tac 1);
1.177 +\end{ttbox}
1.178
1.179 \subsection{Other classical tactics}
1.180 \begin{ttbox}
1.181 @@ -557,7 +587,7 @@
1.182 yourself, you can execute these procedures one step at a time.
1.183 \begin{ttdescription}
1.184 \item[\ttindexbold{safe_step_tac} $cs$ $i$] performs a safe step on
1.185 - subgoal~$i$. The safe wrapper tactical is applied to a tactic that may
1.186 + subgoal~$i$. The safe wrapper tacticals are applied to a tactic that may
1.187 include proof by assumption or Modus Ponens (taking care not to instantiate
1.188 unknowns), or substitution.
1.189
1.190 @@ -568,7 +598,7 @@
1.191 but allows unknowns to be instantiated.
1.192
1.193 \item[\ttindexbold{step_tac} $cs$ $i$] is the basic step of the proof
1.194 - procedure. The (unsafe) wrapper tactical is applied to a tactic that tries
1.195 + procedure. The (unsafe) wrapper tacticals are applied to a tactic that tries
1.196 \texttt{safe_tac}, \texttt{inst_step_tac}, or applies an unsafe rule from~$cs$.
1.197
1.198 \item[\ttindexbold{slow_step_tac}]
1.199 @@ -597,6 +627,7 @@
1.200 \begin{ttbox}
1.201 Blast_tac : int -> tactic
1.202 Auto_tac : tactic
1.203 +Force_tac : int -> tactic
1.204 Fast_tac : int -> tactic
1.205 Best_tac : int -> tactic
1.206 Deepen_tac : int -> int -> tactic
1.207 @@ -606,7 +637,7 @@
1.208 Safe_step_tac : int -> tactic
1.209 Step_tac : int -> tactic
1.210 \end{ttbox}
1.211 -\indexbold{*Blast_tac}\indexbold{*Auto_tac}
1.212 +\indexbold{*Blast_tac}\indexbold{*Auto_tac}\indexbold{*Force_tac}
1.213 \indexbold{*Best_tac}\indexbold{*Fast_tac}%
1.214 \indexbold{*Deepen_tac}
1.215 \indexbold{*Clarify_tac}\indexbold{*Clarify_step_tac}