# HG changeset patch # User wenzelm # Date 966271763 -7200 # Node ID 1bf495402ae95f4f557b02a47f395e39a2aada77 # Parent 60d8c954390fcd18bfd1998449bd3cc412b9308b moved tactic emulation methods here; added print_trans_rules; renamed "res_inst_tac' etc. to 'rule_tac' etc.; added 'fastsimp'; diff -r 60d8c954390f -r 1bf495402ae9 doc-src/IsarRef/generic.tex --- a/doc-src/IsarRef/generic.tex Mon Aug 14 18:47:32 2000 +0200 +++ b/doc-src/IsarRef/generic.tex Mon Aug 14 18:49:23 2000 +0200 @@ -53,12 +53,13 @@ \indexisarcmd{also}\indexisarcmd{finally} \indexisarcmd{moreover}\indexisarcmd{ultimately} -\indexisaratt{trans} +\indexisarcmd{print-trans-rules}\indexisaratt{trans} \begin{matharray}{rcl} \isarcmd{also} & : & \isartrans{proof(state)}{proof(state)} \\ \isarcmd{finally} & : & \isartrans{proof(state)}{proof(chain)} \\ \isarcmd{moreover} & : & \isartrans{proof(state)}{proof(state)} \\ \isarcmd{ultimately} & : & \isartrans{proof(state)}{proof(chain)} \\ + \isarcmd{print_trans_rules} & : & \isarkeep{theory~|~proof} \\ trans & : & \isaratt \\ \end{matharray} @@ -92,7 +93,7 @@ block-structure has been suppressed.} \begin{matharray}{rcl} \ALSO@0 & \equiv & \NOTE{calculation}{this} \\ - \ALSO@{n+1} & \equiv & \NOTE{calculation}{trans~[OF~calculation~this]} \\ + \ALSO@{n+1} & \equiv & \NOTE{calculation}{trans~[OF~calculation~this]} \\[0.5ex] \FINALLY & \equiv & \ALSO~\FROM{calculation} \\ \MOREOVER & \equiv & \NOTE{calculation}{calculation~this} \\ \ULTIMATELY & \equiv & \MOREOVER~\FROM{calculation} \\ @@ -130,7 +131,11 @@ \item [$\MOREOVER$ and $\ULTIMATELY$] are analogous to $\ALSO$ and $\FINALLY$, but collect results only, without applying rules. +\item [$\isarkeyword{print_trans_rules}$] prints the list of transitivity + rules declared in the current context. + \item [$trans$] declares theorems as transitivity rules. + \end{descr} @@ -233,7 +238,7 @@ \qquad \ASSUME{that [simp, intro]}{\All{\vec x} \vec\phi \Imp thesis} \\ \qquad \FROM{\vec b}~\HAVE{}{thesis}~~\langle proof\rangle \\ \quad \EN \\ - \quad \FIX{\vec x}~\ASSUMENAME^{obtained}~{a}~{\vec\phi} \\ + \quad \FIX{\vec x}~\ASSUMENAME^{\ast}~{a}~{\vec\phi} \\ \end{matharray} Typically, the soundness proof is relatively straight-forward, often just by @@ -254,12 +259,13 @@ \section{Miscellaneous methods and attributes} -\indexisarmeth{unfold}\indexisarmeth{fold} +\indexisarmeth{unfold}\indexisarmeth{fold}\indexisarmeth{insert} \indexisarmeth{erule}\indexisarmeth{drule}\indexisarmeth{frule} \indexisarmeth{fail}\indexisarmeth{succeed} \begin{matharray}{rcl} unfold & : & \isarmeth \\ fold & : & \isarmeth \\[0.5ex] + insert^* & : & \isarmeth \\[0.5ex] erule^* & : & \isarmeth \\ drule^* & : & \isarmeth \\ frule^* & : & \isarmeth \\[0.5ex] @@ -268,7 +274,7 @@ \end{matharray} \begin{rail} - ('fold' | 'unfold' | 'erule' | 'drule' | 'frule') thmrefs + ('fold' | 'unfold' | 'insert' | 'erule' | 'drule' | 'frule') thmrefs ; \end{rail} @@ -286,6 +292,8 @@ the proof language level, rather than via implicit proof state manipulations. For example, a proper single-step elimination would be done using the basic $rule$ method, with forward chaining of current facts. +\item [$insert~\vec a$] inserts theorems as facts into all goals of the proof + state. Note that current facts indicated for forward chaining are ignored. \item [$succeed$] yields a single (unchanged) result; it is the identity of the ``\texttt{,}'' method combinator (cf.\ \S\ref{sec:syn-meth}). \item [$fail$] yields an empty result sequence; it is the identity of the @@ -340,8 +348,8 @@ process that is normally intended (cf.\ \texttt{RS} and \texttt{COMP} in \cite[\S5]{isabelle-ref}). \item [$where~\vec x = \vec t$] perform named instantiation of schematic - variables occurring in a theorem. Unlike instantiation tactics (such as - \texttt{res_inst_tac}, see \cite{isabelle-ref}), actual schematic variables + variables occurring in a theorem. Unlike instantiation tactics such as + $rule_tac$ (see \S\ref{sec:tactic-commands}), actual schematic variables have to be specified (e.g.\ $\Var{x@3}$). \item [$unfold~\vec a$ and $fold~\vec a$] expand and fold back again the given @@ -364,6 +372,111 @@ \end{descr} +\section{Tactic emulations}\label{sec:tactics} + +The following improper proof methods emulate traditional tactics. These admit +direct access to the goal state, which is normally considered harmful! In +particular, this may involve both numbered goal addressing (default 1), and +dynamic instantiation within the scope of some subgoal. + +\begin{warn} + Dynamic instantiations are read and type-checked according to a subgoal of + the current dynamic goal state, rather than the static proof context! In + particular, locally fixed variables and term abbreviations may not be + included in the term specifications. Thus schematic variables are left to + be solved by unification with certain parts of the subgoal involved. +\end{warn} + +Note that the tactic emulation proof methods in Isabelle/Isar are consistently +named $foo_tac$. + +\indexisarmeth{rule-tac}\indexisarmeth{erule-tac} +\indexisarmeth{drule-tac}\indexisarmeth{frule-tac} +\indexisarmeth{cut-tac}\indexisarmeth{thin-tac} +\indexisarmeth{subgoal-tac}\indexisarmeth{tactic} +\begin{matharray}{rcl} + rule_tac^* & : & \isarmeth \\ + erule_tac^* & : & \isarmeth \\ + drule_tac^* & : & \isarmeth \\ + frule_tac^* & : & \isarmeth \\ + cut_tac^* & : & \isarmeth \\ + thin_tac^* & : & \isarmeth \\ + subgoal_tac^* & : & \isarmeth \\ + tactic^* & : & \isarmeth \\ +\end{matharray} + +\railalias{ruletac}{rule\_tac} +\railterm{ruletac} + +\railalias{eruletac}{erule\_tac} +\railterm{eruletac} + +\railalias{druletac}{drule\_tac} +\railterm{druletac} + +\railalias{fruletac}{frule\_tac} +\railterm{fruletac} + +\railalias{cuttac}{cut\_tac} +\railterm{cuttac} + +\railalias{thintac}{thin\_tac} +\railterm{thintac} + +\railalias{subgoaltac}{subgoal\_tac} +\railterm{subgoaltac} + +\begin{rail} + ( ruletac | eruletac | druletac | fruletac | cuttac | thintac ) goalspec? + ( insts thmref | thmrefs ) + ; + subgoaltac goalspec? (prop +) + ; + 'tactic' text + ; + + insts: ((name '=' term) + 'and') 'in' + ; +\end{rail} + +\begin{descr} +\item [$rule_tac$ etc.] do resolution of rules with explicit instantiation. + This works the same way as the ML tactics \texttt{res_inst_tac} etc. (see + \cite[\S3]{isabelle-ref}). + + Note that multiple rules may be only given there is no instantiation. Then + $rule_tac$ is the same as \texttt{resolve_tac} in ML (see + \cite[\S3]{isabelle-ref}). +\item [$cut_tac$] inserts facts into the proof state as assumption of a + subgoal, see also \texttt{cut_facts_tac} in \cite[\S3]{isabelle-ref}. Note + that the scope of schmatic variables is spread over the main goal statement. + Instantiations may be given as well, see also ML tactic + \texttt{cut_inst_tac} in \cite[\S3]{isabelle-ref}. +\item [$thin_tac~\phi$] deletes the specified assumption from a subgoal; note + that $\phi$ may contain schematic variables. See also \texttt{thin_tac} in + \cite[\S3]{isabelle-ref}. +\item [$subgoal_tac~\phi$] adds $\phi$ as an assumption to a subgoal. See + also \texttt{subgoal_tac} and \texttt{subgoals_tac} in + \cite[\S3]{isabelle-ref}. +\item [$tactic~text$] produces a proof method from any ML text of type + \texttt{tactic}. Apart from the usual ML environment and the current + implicit theory context, the ML code may refer to the following locally + bound values: + +%%FIXME ttbox produces too much trailing space (why?) +{\footnotesize\begin{verbatim} +val ctxt : Proof.context +val facts : thm list +val thm : string -> thm +val thms : string -> thm list +\end{verbatim}} + Here \texttt{ctxt} refers to the current proof context, \texttt{facts} + indicates any current facts for forward-chaining, and + \texttt{thm}~/~\texttt{thms} retrieve named facts (including global + theorems) from the context. +\end{descr} + + \section{The Simplifier} \subsection{Simplification methods}\label{sec:simp} @@ -547,7 +660,10 @@ \begin{descr} \item [$blast$] refers to the classical tableau prover (see \texttt{blast_tac} in \cite[\S11]{isabelle-ref}). The optional argument specifies a - user-supplied search bound (default 20). + user-supplied search bound (default 20). Note that $blast$ is the only + classical proof procedure in Isabelle that can handle actual object-logic + rules as local assumptions ($fast$ etc.\ would just ignore non-atomic + facts). \item [$fast$, $best$, and $clarify$] refer to the generic classical reasoner. See \texttt{fast_tac}, \texttt{best_tac}, and \texttt{clarify_tac} in \cite[\S11]{isabelle-ref} for more information. @@ -565,15 +681,17 @@ \subsection{Combined automated methods} -\indexisarmeth{force}\indexisarmeth{auto}\indexisarmeth{clarsimp} +\indexisarmeth{auto}\indexisarmeth{force} +\indexisarmeth{clarsimp}\indexisarmeth{fastsimp} \begin{matharray}{rcl} + auto & : & \isarmeth \\ force & : & \isarmeth \\ - auto & : & \isarmeth \\ clarsimp & : & \isarmeth \\ + fastsimp & : & \isarmeth \\ \end{matharray} \begin{rail} - ('force' | 'auto' | 'clarsimp') ('!' ?) (clasimpmod * ) + ('auto' | 'force' | 'clarsimp' | 'fastsimp') ('!' ?) (clasimpmod * ) ; clasimpmod: ('simp' (() | 'add' | 'del' | 'only') | 'other' | @@ -582,12 +700,14 @@ \end{rail} \begin{descr} -\item [$force$, $auto$, and $clarsimp$] provide access to Isabelle's combined - simplification and classical reasoning tactics. See \texttt{force_tac}, - \texttt{auto_tac}, and \texttt{clarsimp_tac} in \cite[\S11]{isabelle-ref} - for more information. The modifier arguments correspond to those given in - \S\ref{sec:simp} and \S\ref{sec:classical-auto}. Just note that the ones - related to the Simplifier are prefixed by \railtterm{simp} here. +\item [$auto$, $force$, $clarsimp$, $fastsimp$] provide access to Isabelle's + combined simplification and classical reasoning tactics. These correspond + to \texttt{auto_tac}, \texttt{force_tac}, \texttt{clarsimp_tac}, and + \texttt{fast_tac} (with the Simplifier added as wrapper), see + \cite[\S11]{isabelle-ref} for more information. The modifier arguments + correspond to those given in \S\ref{sec:simp} and + \S\ref{sec:classical-auto}. Just note that the ones related to the + Simplifier are prefixed by \railtterm{simp} here. Facts provided by forward chaining are inserted into the goal before doing the search. The ``!''~argument causes the full context of assumptions to be