doc-src/IsarRef/generic.tex
changeset 9606 1bf495402ae9
parent 9480 7afb808b6b3e
child 9614 8ca1fc75230e
     1.1 --- a/doc-src/IsarRef/generic.tex	Mon Aug 14 18:47:32 2000 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Mon Aug 14 18:49:23 2000 +0200
     1.3 @@ -53,12 +53,13 @@
     1.4  
     1.5  \indexisarcmd{also}\indexisarcmd{finally}
     1.6  \indexisarcmd{moreover}\indexisarcmd{ultimately}
     1.7 -\indexisaratt{trans}
     1.8 +\indexisarcmd{print-trans-rules}\indexisaratt{trans}
     1.9  \begin{matharray}{rcl}
    1.10    \isarcmd{also} & : & \isartrans{proof(state)}{proof(state)} \\
    1.11    \isarcmd{finally} & : & \isartrans{proof(state)}{proof(chain)} \\
    1.12    \isarcmd{moreover} & : & \isartrans{proof(state)}{proof(state)} \\
    1.13    \isarcmd{ultimately} & : & \isartrans{proof(state)}{proof(chain)} \\
    1.14 +  \isarcmd{print_trans_rules} & : & \isarkeep{theory~|~proof} \\
    1.15    trans & : & \isaratt \\
    1.16  \end{matharray}
    1.17  
    1.18 @@ -92,7 +93,7 @@
    1.19    block-structure has been suppressed.}
    1.20  \begin{matharray}{rcl}
    1.21    \ALSO@0 & \equiv & \NOTE{calculation}{this} \\
    1.22 -  \ALSO@{n+1} & \equiv & \NOTE{calculation}{trans~[OF~calculation~this]} \\
    1.23 +  \ALSO@{n+1} & \equiv & \NOTE{calculation}{trans~[OF~calculation~this]} \\[0.5ex]
    1.24    \FINALLY & \equiv & \ALSO~\FROM{calculation} \\
    1.25    \MOREOVER & \equiv & \NOTE{calculation}{calculation~this} \\
    1.26    \ULTIMATELY & \equiv & \MOREOVER~\FROM{calculation} \\
    1.27 @@ -130,7 +131,11 @@
    1.28  \item [$\MOREOVER$ and $\ULTIMATELY$] are analogous to $\ALSO$ and $\FINALLY$,
    1.29    but collect results only, without applying rules.
    1.30    
    1.31 +\item [$\isarkeyword{print_trans_rules}$] prints the list of transitivity
    1.32 +  rules declared in the current context.
    1.33 +  
    1.34  \item [$trans$] declares theorems as transitivity rules.
    1.35 + 
    1.36  \end{descr}
    1.37  
    1.38  
    1.39 @@ -233,7 +238,7 @@
    1.40    \qquad \ASSUME{that [simp, intro]}{\All{\vec x} \vec\phi \Imp thesis} \\
    1.41    \qquad \FROM{\vec b}~\HAVE{}{thesis}~~\langle proof\rangle \\
    1.42    \quad \EN \\
    1.43 -  \quad \FIX{\vec x}~\ASSUMENAME^{obtained}~{a}~{\vec\phi} \\
    1.44 +  \quad \FIX{\vec x}~\ASSUMENAME^{\ast}~{a}~{\vec\phi} \\
    1.45  \end{matharray}
    1.46  
    1.47  Typically, the soundness proof is relatively straight-forward, often just by
    1.48 @@ -254,12 +259,13 @@
    1.49  
    1.50  \section{Miscellaneous methods and attributes}
    1.51  
    1.52 -\indexisarmeth{unfold}\indexisarmeth{fold}
    1.53 +\indexisarmeth{unfold}\indexisarmeth{fold}\indexisarmeth{insert}
    1.54  \indexisarmeth{erule}\indexisarmeth{drule}\indexisarmeth{frule}
    1.55  \indexisarmeth{fail}\indexisarmeth{succeed}
    1.56  \begin{matharray}{rcl}
    1.57    unfold & : & \isarmeth \\
    1.58    fold & : & \isarmeth \\[0.5ex]
    1.59 +  insert^* & : & \isarmeth \\[0.5ex]
    1.60    erule^* & : & \isarmeth \\
    1.61    drule^* & : & \isarmeth \\
    1.62    frule^* & : & \isarmeth \\[0.5ex]
    1.63 @@ -268,7 +274,7 @@
    1.64  \end{matharray}
    1.65  
    1.66  \begin{rail}
    1.67 -  ('fold' | 'unfold' | 'erule' | 'drule' | 'frule') thmrefs
    1.68 +  ('fold' | 'unfold' | 'insert' | 'erule' | 'drule' | 'frule') thmrefs
    1.69    ;
    1.70  \end{rail}
    1.71  
    1.72 @@ -286,6 +292,8 @@
    1.73    the proof language level, rather than via implicit proof state
    1.74    manipulations.  For example, a proper single-step elimination would be done
    1.75    using the basic $rule$ method, with forward chaining of current facts.
    1.76 +\item [$insert~\vec a$] inserts theorems as facts into all goals of the proof
    1.77 +  state.  Note that current facts indicated for forward chaining are ignored.
    1.78  \item [$succeed$] yields a single (unchanged) result; it is the identity of
    1.79    the ``\texttt{,}'' method combinator (cf.\ \S\ref{sec:syn-meth}).
    1.80  \item [$fail$] yields an empty result sequence; it is the identity of the
    1.81 @@ -340,8 +348,8 @@
    1.82    process that is normally intended (cf.\ \texttt{RS} and \texttt{COMP} in
    1.83    \cite[\S5]{isabelle-ref}).
    1.84  \item [$where~\vec x = \vec t$] perform named instantiation of schematic
    1.85 -  variables occurring in a theorem.  Unlike instantiation tactics (such as
    1.86 -  \texttt{res_inst_tac}, see \cite{isabelle-ref}), actual schematic variables
    1.87 +  variables occurring in a theorem.  Unlike instantiation tactics such as
    1.88 +  $rule_tac$ (see \S\ref{sec:tactic-commands}), actual schematic variables
    1.89    have to be specified (e.g.\ $\Var{x@3}$).
    1.90    
    1.91  \item [$unfold~\vec a$ and $fold~\vec a$] expand and fold back again the given
    1.92 @@ -364,6 +372,111 @@
    1.93  \end{descr}
    1.94  
    1.95  
    1.96 +\section{Tactic emulations}\label{sec:tactics}
    1.97 +
    1.98 +The following improper proof methods emulate traditional tactics.  These admit
    1.99 +direct access to the goal state, which is normally considered harmful!  In
   1.100 +particular, this may involve both numbered goal addressing (default 1), and
   1.101 +dynamic instantiation within the scope of some subgoal.
   1.102 +
   1.103 +\begin{warn}
   1.104 +  Dynamic instantiations are read and type-checked according to a subgoal of
   1.105 +  the current dynamic goal state, rather than the static proof context!  In
   1.106 +  particular, locally fixed variables and term abbreviations may not be
   1.107 +  included in the term specifications.  Thus schematic variables are left to
   1.108 +  be solved by unification with certain parts of the subgoal involved.
   1.109 +\end{warn}
   1.110 +
   1.111 +Note that the tactic emulation proof methods in Isabelle/Isar are consistently
   1.112 +named $foo_tac$.
   1.113 +
   1.114 +\indexisarmeth{rule-tac}\indexisarmeth{erule-tac}
   1.115 +\indexisarmeth{drule-tac}\indexisarmeth{frule-tac}
   1.116 +\indexisarmeth{cut-tac}\indexisarmeth{thin-tac}
   1.117 +\indexisarmeth{subgoal-tac}\indexisarmeth{tactic}
   1.118 +\begin{matharray}{rcl}
   1.119 +  rule_tac^* & : & \isarmeth \\
   1.120 +  erule_tac^* & : & \isarmeth \\
   1.121 +  drule_tac^* & : & \isarmeth \\
   1.122 +  frule_tac^* & : & \isarmeth \\
   1.123 +  cut_tac^* & : & \isarmeth \\
   1.124 +  thin_tac^* & : & \isarmeth \\
   1.125 +  subgoal_tac^* & : & \isarmeth \\
   1.126 +  tactic^* & : & \isarmeth \\
   1.127 +\end{matharray}
   1.128 +
   1.129 +\railalias{ruletac}{rule\_tac}
   1.130 +\railterm{ruletac}
   1.131 +
   1.132 +\railalias{eruletac}{erule\_tac}
   1.133 +\railterm{eruletac}
   1.134 +
   1.135 +\railalias{druletac}{drule\_tac}
   1.136 +\railterm{druletac}
   1.137 +
   1.138 +\railalias{fruletac}{frule\_tac}
   1.139 +\railterm{fruletac}
   1.140 +
   1.141 +\railalias{cuttac}{cut\_tac}
   1.142 +\railterm{cuttac}
   1.143 +
   1.144 +\railalias{thintac}{thin\_tac}
   1.145 +\railterm{thintac}
   1.146 +
   1.147 +\railalias{subgoaltac}{subgoal\_tac}
   1.148 +\railterm{subgoaltac}
   1.149 +
   1.150 +\begin{rail}
   1.151 +  ( ruletac | eruletac | druletac | fruletac | cuttac | thintac ) goalspec?
   1.152 +  ( insts thmref | thmrefs )
   1.153 +  ;
   1.154 +  subgoaltac goalspec? (prop +)
   1.155 +  ;
   1.156 +  'tactic' text
   1.157 +  ;
   1.158 +
   1.159 +  insts: ((name '=' term) + 'and') 'in'
   1.160 +  ;
   1.161 +\end{rail}
   1.162 +
   1.163 +\begin{descr}
   1.164 +\item [$rule_tac$ etc.] do resolution of rules with explicit instantiation.
   1.165 +  This works the same way as the ML tactics \texttt{res_inst_tac} etc. (see
   1.166 +  \cite[\S3]{isabelle-ref}).
   1.167 +  
   1.168 +  Note that multiple rules may be only given there is no instantiation.  Then
   1.169 +  $rule_tac$ is the same as \texttt{resolve_tac} in ML (see
   1.170 +  \cite[\S3]{isabelle-ref}).
   1.171 +\item [$cut_tac$] inserts facts into the proof state as assumption of a
   1.172 +  subgoal, see also \texttt{cut_facts_tac} in \cite[\S3]{isabelle-ref}.  Note
   1.173 +  that the scope of schmatic variables is spread over the main goal statement.
   1.174 +  Instantiations may be given as well, see also ML tactic
   1.175 +  \texttt{cut_inst_tac} in \cite[\S3]{isabelle-ref}.
   1.176 +\item [$thin_tac~\phi$] deletes the specified assumption from a subgoal; note
   1.177 +  that $\phi$ may contain schematic variables.  See also \texttt{thin_tac} in
   1.178 +  \cite[\S3]{isabelle-ref}.
   1.179 +\item [$subgoal_tac~\phi$] adds $\phi$ as an assumption to a subgoal.  See
   1.180 +  also \texttt{subgoal_tac} and \texttt{subgoals_tac} in
   1.181 +  \cite[\S3]{isabelle-ref}.
   1.182 +\item [$tactic~text$] produces a proof method from any ML text of type
   1.183 +  \texttt{tactic}.  Apart from the usual ML environment and the current
   1.184 +  implicit theory context, the ML code may refer to the following locally
   1.185 +  bound values:
   1.186 +
   1.187 +%%FIXME ttbox produces too much trailing space (why?)
   1.188 +{\footnotesize\begin{verbatim}
   1.189 +val ctxt  : Proof.context
   1.190 +val facts : thm list
   1.191 +val thm   : string -> thm
   1.192 +val thms  : string -> thm list
   1.193 +\end{verbatim}}
   1.194 +  Here \texttt{ctxt} refers to the current proof context, \texttt{facts}
   1.195 +  indicates any current facts for forward-chaining, and
   1.196 +  \texttt{thm}~/~\texttt{thms} retrieve named facts (including global
   1.197 +  theorems) from the context.
   1.198 +\end{descr}
   1.199 +
   1.200 +
   1.201  \section{The Simplifier}
   1.202  
   1.203  \subsection{Simplification methods}\label{sec:simp}
   1.204 @@ -547,7 +660,10 @@
   1.205  \begin{descr}
   1.206  \item [$blast$] refers to the classical tableau prover (see \texttt{blast_tac}
   1.207    in \cite[\S11]{isabelle-ref}).  The optional argument specifies a
   1.208 -  user-supplied search bound (default 20).
   1.209 +  user-supplied search bound (default 20).  Note that $blast$ is the only
   1.210 +  classical proof procedure in Isabelle that can handle actual object-logic
   1.211 +  rules as local assumptions ($fast$ etc.\ would just ignore non-atomic
   1.212 +  facts).
   1.213  \item [$fast$, $best$, and $clarify$] refer to the generic classical reasoner.
   1.214    See \texttt{fast_tac}, \texttt{best_tac}, and \texttt{clarify_tac} in
   1.215    \cite[\S11]{isabelle-ref} for more information.
   1.216 @@ -565,15 +681,17 @@
   1.217  
   1.218  \subsection{Combined automated methods}
   1.219  
   1.220 -\indexisarmeth{force}\indexisarmeth{auto}\indexisarmeth{clarsimp}
   1.221 +\indexisarmeth{auto}\indexisarmeth{force}
   1.222 +\indexisarmeth{clarsimp}\indexisarmeth{fastsimp}
   1.223  \begin{matharray}{rcl}
   1.224 +  auto & : & \isarmeth \\
   1.225    force & : & \isarmeth \\
   1.226 -  auto & : & \isarmeth \\
   1.227    clarsimp & : & \isarmeth \\
   1.228 +  fastsimp & : & \isarmeth \\
   1.229  \end{matharray}
   1.230  
   1.231  \begin{rail}
   1.232 -  ('force' | 'auto' | 'clarsimp') ('!' ?) (clasimpmod * )
   1.233 +  ('auto' | 'force' | 'clarsimp' | 'fastsimp') ('!' ?) (clasimpmod * )
   1.234    ;
   1.235  
   1.236    clasimpmod: ('simp' (() | 'add' | 'del' | 'only') | 'other' |
   1.237 @@ -582,12 +700,14 @@
   1.238  \end{rail}
   1.239  
   1.240  \begin{descr}
   1.241 -\item [$force$, $auto$, and $clarsimp$] provide access to Isabelle's combined
   1.242 -  simplification and classical reasoning tactics.  See \texttt{force_tac},
   1.243 -  \texttt{auto_tac}, and \texttt{clarsimp_tac} in \cite[\S11]{isabelle-ref}
   1.244 -  for more information.  The modifier arguments correspond to those given in
   1.245 -  \S\ref{sec:simp} and \S\ref{sec:classical-auto}.  Just note that the ones
   1.246 -  related to the Simplifier are prefixed by \railtterm{simp} here.
   1.247 +\item [$auto$, $force$, $clarsimp$, $fastsimp$] provide access to Isabelle's
   1.248 +  combined simplification and classical reasoning tactics.  These correspond
   1.249 +  to \texttt{auto_tac}, \texttt{force_tac}, \texttt{clarsimp_tac}, and
   1.250 +  \texttt{fast_tac} (with the Simplifier added as wrapper), see
   1.251 +  \cite[\S11]{isabelle-ref} for more information.  The modifier arguments
   1.252 +  correspond to those given in \S\ref{sec:simp} and
   1.253 +  \S\ref{sec:classical-auto}.  Just note that the ones related to the
   1.254 +  Simplifier are prefixed by \railtterm{simp} here.
   1.255    
   1.256    Facts provided by forward chaining are inserted into the goal before doing
   1.257    the search.  The ``!''~argument causes the full context of assumptions to be