doc-src/IsarRef/generic.tex
changeset 9614 8ca1fc75230e
parent 9606 1bf495402ae9
child 9642 d8d1f70024bd
     1.1 --- a/doc-src/IsarRef/generic.tex	Thu Aug 17 10:29:50 2000 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Thu Aug 17 10:31:10 2000 +0200
     1.3 @@ -37,7 +37,7 @@
     1.4    names.  Furthermore a class introduction rule is generated, which is
     1.5    employed by method $intro_classes$ to support instantiation proofs of this
     1.6    class.
     1.7 -  
     1.8 +
     1.9  \item [$\isarkeyword{instance}~c@1 < c@2$ and $\isarkeyword{instance}~t ::
    1.10    (\vec s)c$] setup a goal stating a class relation or type arity.  The proof
    1.11    would usually proceed by $intro_classes$, and then establish the
    1.12 @@ -119,7 +119,7 @@
    1.13    applied to $calculation$ and $this$ (in that order).  Transitivity rules are
    1.14    picked from the current context plus those given as explicit arguments (the
    1.15    latter have precedence).
    1.16 -  
    1.17 +
    1.18  \item [$\FINALLY~(\vec a)$] maintaining $calculation$ in the same way as
    1.19    $\ALSO$, and concludes the current calculational thread.  The final result
    1.20    is exhibited as fact for forward chaining towards the next goal. Basically,
    1.21 @@ -127,15 +127,15 @@
    1.22    ``$\FINALLY~\SHOW{}{\Var{thesis}}~\DOT$'' and
    1.23    ``$\FINALLY~\HAVE{}{\phi}~\DOT$'' are typical idioms for concluding
    1.24    calculational proofs.
    1.25 -  
    1.26 +
    1.27  \item [$\MOREOVER$ and $\ULTIMATELY$] are analogous to $\ALSO$ and $\FINALLY$,
    1.28    but collect results only, without applying rules.
    1.29 -  
    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 +
    1.35  \item [$trans$] declares theorems as transitivity rules.
    1.36 - 
    1.37 +
    1.38  \end{descr}
    1.39  
    1.40  
    1.41 @@ -204,10 +204,13 @@
    1.42  \item [$params~\vec p@1 \dots \vec p@n$] renames the innermost parameters of
    1.43    premises $1, \dots, n$ of some theorem.  An empty list of names may be given
    1.44    to skip positions, leaving the present parameters unchanged.
    1.45 +
    1.46 +  Note that the default usage of case rules does \emph{not} directly expose
    1.47 +  parameters to the proof context (see also \S\ref{sec:induct-method-proper}).
    1.48  \end{descr}
    1.49  
    1.50  
    1.51 -\section{Generalized existence}
    1.52 +\section{Generalized existence}\label{sec:obtain}
    1.53  
    1.54  \indexisarcmd{obtain}
    1.55  \begin{matharray}{rcl}
    1.56 @@ -287,7 +290,7 @@
    1.57    elim-resolution, destruct-resolution, and forward-resolution, respectively
    1.58    \cite{isabelle-ref}.  These are improper method, mainly for experimentation
    1.59    and emulating tactic scripts.
    1.60 -  
    1.61 +
    1.62    Different modes of basic rule application are usually expressed in Isar at
    1.63    the proof language level, rather than via implicit proof state
    1.64    manipulations.  For example, a proper single-step elimination would be done
    1.65 @@ -305,7 +308,7 @@
    1.66  \indexisaratt{elimify}
    1.67  \indexisaratt{no-vars}
    1.68  
    1.69 -\indexisaratt{RS}\indexisaratt{COMP}
    1.70 +\indexisaratt{THEN}\indexisaratt{COMP}
    1.71  \indexisaratt{where}
    1.72  \indexisaratt{tag}\indexisaratt{untag}
    1.73  \indexisaratt{export}
    1.74 @@ -313,7 +316,7 @@
    1.75  \begin{matharray}{rcl}
    1.76    tag & : & \isaratt \\
    1.77    untag & : & \isaratt \\[0.5ex]
    1.78 -  RS & : & \isaratt \\
    1.79 +  THEN & : & \isaratt \\
    1.80    COMP & : & \isaratt \\[0.5ex]
    1.81    where & : & \isaratt \\[0.5ex]
    1.82    unfold & : & \isaratt \\
    1.83 @@ -329,7 +332,7 @@
    1.84    ;
    1.85    'untag' name
    1.86    ;
    1.87 -  ('RS' | 'COMP') nat? thmref
    1.88 +  ('THEN' | 'COMP') nat? thmref
    1.89    ;
    1.90    'where' (name '=' term * 'and')
    1.91    ;
    1.92 @@ -343,32 +346,32 @@
    1.93    tools (e.g.\ $\LEMMANAME$ causes the tag ``$lemma$'' to be added to the
    1.94    result).  The first string is considered the tag name, the rest its
    1.95    arguments.  Note that untag removes any tags of the same name.
    1.96 -\item [$RS~n~a$ and $COMP~n~a$] compose rules.  $RS$ resolves with the $n$-th
    1.97 -  premise of $a$; $COMP$ is a version of $RS$ that skips the automatic lifting
    1.98 +\item [$THEN~n~a$ and $COMP~n~a$] compose rules.  $THEN$ resolves with the
    1.99 +  $n$-th premise of $a$; the $COMP$ version skips the automatic lifting
   1.100    process that is normally intended (cf.\ \texttt{RS} and \texttt{COMP} in
   1.101    \cite[\S5]{isabelle-ref}).
   1.102  \item [$where~\vec x = \vec t$] perform named instantiation of schematic
   1.103    variables occurring in a theorem.  Unlike instantiation tactics such as
   1.104    $rule_tac$ (see \S\ref{sec:tactic-commands}), actual schematic variables
   1.105    have to be specified (e.g.\ $\Var{x@3}$).
   1.106 -  
   1.107 +
   1.108  \item [$unfold~\vec a$ and $fold~\vec a$] expand and fold back again the given
   1.109    meta-level definitions throughout a rule.
   1.110 - 
   1.111 +
   1.112  \item [$standard$] puts a theorem into the standard form of object-rules, just
   1.113    as the ML function \texttt{standard} (see \cite[\S5]{isabelle-ref}).
   1.114 -  
   1.115 +
   1.116  \item [$elimify$] turns an destruction rule into an elimination, just as the
   1.117    ML function \texttt{make\_elim} (see \cite{isabelle-ref}).
   1.118 -  
   1.119 +
   1.120  \item [$no_vars$] replaces schematic variables by free ones; this is mainly
   1.121    for tuning output of pretty printed theorems.
   1.122 -  
   1.123 +
   1.124  \item [$export$] lifts a local result out of the current proof context,
   1.125    generalizing all fixed variables and discharging all assumptions.  Note that
   1.126    proper incremental export is already done as part of the basic Isar
   1.127    machinery.  This attribute is mainly for experimentation.
   1.128 -  
   1.129 +
   1.130  \end{descr}
   1.131  
   1.132  
   1.133 @@ -393,7 +396,8 @@
   1.134  \indexisarmeth{rule-tac}\indexisarmeth{erule-tac}
   1.135  \indexisarmeth{drule-tac}\indexisarmeth{frule-tac}
   1.136  \indexisarmeth{cut-tac}\indexisarmeth{thin-tac}
   1.137 -\indexisarmeth{subgoal-tac}\indexisarmeth{tactic}
   1.138 +\indexisarmeth{subgoal-tac}\indexisarmeth{rename_tac}
   1.139 +\indexisarmeth{rotate-tac}\indexisarmeth{tactic}
   1.140  \begin{matharray}{rcl}
   1.141    rule_tac^* & : & \isarmeth \\
   1.142    erule_tac^* & : & \isarmeth \\
   1.143 @@ -402,6 +406,8 @@
   1.144    cut_tac^* & : & \isarmeth \\
   1.145    thin_tac^* & : & \isarmeth \\
   1.146    subgoal_tac^* & : & \isarmeth \\
   1.147 +  rename_tac^* & : & \isarmeth \\
   1.148 +  rotate_tac^* & : & \isarmeth \\
   1.149    tactic^* & : & \isarmeth \\
   1.150  \end{matharray}
   1.151  
   1.152 @@ -426,12 +432,22 @@
   1.153  \railalias{subgoaltac}{subgoal\_tac}
   1.154  \railterm{subgoaltac}
   1.155  
   1.156 +\railalias{renametac}{rename\_tac}
   1.157 +\railterm{renametac}
   1.158 +
   1.159 +\railalias{rotatetac}{rotate\_tac}
   1.160 +\railterm{rotatetac}
   1.161 +
   1.162  \begin{rail}
   1.163    ( ruletac | eruletac | druletac | fruletac | cuttac | thintac ) goalspec?
   1.164    ( insts thmref | thmrefs )
   1.165    ;
   1.166    subgoaltac goalspec? (prop +)
   1.167    ;
   1.168 +  renametac goalspec? (name +)
   1.169 +  ;
   1.170 +  rotatetac goalspec? int?
   1.171 +  ;
   1.172    'tactic' text
   1.173    ;
   1.174  
   1.175 @@ -443,7 +459,7 @@
   1.176  \item [$rule_tac$ etc.] do resolution of rules with explicit instantiation.
   1.177    This works the same way as the ML tactics \texttt{res_inst_tac} etc. (see
   1.178    \cite[\S3]{isabelle-ref}).
   1.179 -  
   1.180 +
   1.181    Note that multiple rules may be only given there is no instantiation.  Then
   1.182    $rule_tac$ is the same as \texttt{resolve_tac} in ML (see
   1.183    \cite[\S3]{isabelle-ref}).
   1.184 @@ -458,6 +474,12 @@
   1.185  \item [$subgoal_tac~\phi$] adds $\phi$ as an assumption to a subgoal.  See
   1.186    also \texttt{subgoal_tac} and \texttt{subgoals_tac} in
   1.187    \cite[\S3]{isabelle-ref}.
   1.188 +\item [$rename_tac~\vec x$] renames parameters of a goal according to the list
   1.189 +  $\vec x$, which refers to the \emph{suffix} of variables.
   1.190 +\item [$rotate_tac~n$] rotates the assumptions of a goal by $n$ positions:
   1.191 +  from right to left if $n$ is positive, and from left to right if $n$ is
   1.192 +  negative; the default value is $1$.  See also \texttt{rotate_tac} in
   1.193 +  \cite[\S3]{isabelle-ref}.
   1.194  \item [$tactic~text$] produces a proof method from any ML text of type
   1.195    \texttt{tactic}.  Apart from the usual ML environment and the current
   1.196    implicit theory context, the ML code may refer to the following locally
   1.197 @@ -477,7 +499,7 @@
   1.198  \end{descr}
   1.199  
   1.200  
   1.201 -\section{The Simplifier}
   1.202 +\section{The Simplifier}\label{sec:simplifier}
   1.203  
   1.204  \subsection{Simplification methods}\label{sec:simp}
   1.205  
   1.206 @@ -514,12 +536,12 @@
   1.207    according to the arguments given.  Note that the \railtterm{only} modifier
   1.208    first removes all other rewrite rules, congruences, and looper tactics
   1.209    (including splits), and then behaves like \railtterm{add}.
   1.210 -  
   1.211 +
   1.212    The \railtterm{split} modifiers add or delete rules for the Splitter (see
   1.213    also \cite{isabelle-ref}), the default is to add.  This works only if the
   1.214    Simplifier method has been properly setup to include the Splitter (all major
   1.215    object logics such HOL, HOLCF, FOL, ZF do this already).
   1.216 -  
   1.217 +
   1.218    The \railtterm{other} modifier ignores its arguments.  Nevertheless,
   1.219    additional kinds of rules may be declared by including appropriate
   1.220    attributes in the specification.
   1.221 @@ -536,9 +558,9 @@
   1.222  should be used with some care, though.
   1.223  
   1.224  Additional Simplifier options may be specified to tune the behavior even
   1.225 -further: $(no_asm)$ means assumptions are ignored completely (cf.\ 
   1.226 +further: $(no_asm)$ means assumptions are ignored completely (cf.\
   1.227  \texttt{simp_tac}), $(no_asm_simp)$ means assumptions are used in the
   1.228 -simplification of the conclusion but are not themselves simplified (cf.\ 
   1.229 +simplification of the conclusion but are not themselves simplified (cf.\
   1.230  \texttt{asm_simp_tac}), and $(no_asm_use)$ means assumptions are simplified
   1.231  but are not used in the simplification of each other or the conclusion (cf.
   1.232  \texttt{full_simp_tac}).
   1.233 @@ -596,6 +618,34 @@
   1.234  information.
   1.235  
   1.236  
   1.237 +\section{Basic equational reasoning}
   1.238 +
   1.239 +\indexisarmeth{subst}\indexisarmeth{hypsubst}\indexisaratt{symmetric}
   1.240 +\begin{matharray}{rcl}
   1.241 +  subst & : & \isarmeth \\
   1.242 +  hypsubst^* & : & \isarmeth \\
   1.243 +  symmetric & : & \isaratt \\
   1.244 +\end{matharray}
   1.245 +
   1.246 +\begin{rail}
   1.247 +  'subst' thmref
   1.248 +  ;
   1.249 +\end{rail}
   1.250 +
   1.251 +These methods and attributes provide basic facilities for equational reasoning
   1.252 +that are intended for specialized applications only.  Normally, single step
   1.253 +reasoning would be performed by calculation (see \S\ref{sec:calculation}),
   1.254 +while the Simplifier is the canonical tool for automated normalization (see
   1.255 +\S\ref{sec:simplifier}).
   1.256 +
   1.257 +\begin{descr}
   1.258 +\item [$subst~thm$] performs a single substitution step using rule $thm$,
   1.259 +  which may be either a meta or object equality.
   1.260 +\item [$hypsubst$] performs substitution using some assumption.
   1.261 +\item [$symmetric$] applies the symmetry rule of meta or object equality.
   1.262 +\end{descr}
   1.263 +
   1.264 +
   1.265  \section{The Classical Reasoner}
   1.266  
   1.267  \subsection{Basic methods}\label{sec:classical-basic}
   1.268 @@ -622,7 +672,7 @@
   1.269    This is made the default method for basic proof steps, such as $\PROOFNAME$
   1.270    and ``$\DDOT$'' (two dots), see also \S\ref{sec:proof-steps} and
   1.271    \S\ref{sec:pure-meth-att}.
   1.272 -  
   1.273 +
   1.274  \item [$intro$ and $elim$] repeatedly refine some goal by intro- or
   1.275    elim-resolution, after having inserted any facts.  Omitting the arguments
   1.276    refers to any suitable rules declared in the context, otherwise only the
   1.277 @@ -630,7 +680,7 @@
   1.278    of what actually happens, thus it is very appropriate as an initial method
   1.279    for $\PROOFNAME$ that splits up certain connectives of the goal, before
   1.280    entering the actual sub-proof.
   1.281 -  
   1.282 +
   1.283  \item [$contradiction$] solves some goal by contradiction, deriving any result
   1.284    from both $\neg A$ and $A$.  Facts, which are guaranteed to participate, may
   1.285    appear in either order.
   1.286 @@ -708,7 +758,7 @@
   1.287    correspond to those given in \S\ref{sec:simp} and
   1.288    \S\ref{sec:classical-auto}.  Just note that the ones related to the
   1.289    Simplifier are prefixed by \railtterm{simp} here.
   1.290 -  
   1.291 +
   1.292    Facts provided by forward chaining are inserted into the goal before doing
   1.293    the search.  The ``!''~argument causes the full context of assumptions to be
   1.294    included as well.
   1.295 @@ -745,7 +795,7 @@
   1.296    single ``!'' classifies as \emph{safe}, and ``?'' as \emph{extra} (i.e.\ not
   1.297    applied in the search-oriented automated methods, but only in single-step
   1.298    methods such as $rule$).
   1.299 -  
   1.300 +
   1.301  \item [$iff$] declares equations both as rules for the Simplifier and
   1.302    Classical Reasoner.
   1.303  
   1.304 @@ -755,7 +805,7 @@
   1.305  \end{descr}
   1.306  
   1.307  
   1.308 -%%% Local Variables: 
   1.309 +%%% Local Variables:
   1.310  %%% mode: latex
   1.311  %%% TeX-master: "isar-ref"
   1.312 -%%% End: 
   1.313 +%%% End: