doc-src/IsarRef/generic.tex
changeset 13048 8b2eb3b78cc3
parent 13042 d8a345d9e067
child 13411 181a293aa37a
     1.1 --- a/doc-src/IsarRef/generic.tex	Thu Mar 07 23:21:19 2002 +0100
     1.2 +++ b/doc-src/IsarRef/generic.tex	Fri Mar 08 15:53:15 2002 +0100
     1.3 @@ -1,5 +1,5 @@
     1.4  
     1.5 -\chapter{Generic Tools and Packages}\label{ch:gen-tools}
     1.6 +\chapter{Generic tools and packages}\label{ch:gen-tools}
     1.7  
     1.8  \section{Theory specification commands}
     1.9  
    1.10 @@ -62,6 +62,7 @@
    1.11  that are modeled after the Isar proof context commands (cf.\
    1.12  \S\ref{sec:proof-context}).
    1.13  
    1.14 +
    1.15  \subsubsection{Localized commands}
    1.16  
    1.17  Existing locales may be augmented later on by adding new facts.  Note that the
    1.18 @@ -238,10 +239,9 @@
    1.19  \end{matharray}
    1.20  
    1.21  Typically, the soundness proof is relatively straight-forward, often just by
    1.22 -canonical automated tools such as ``$\BY{simp}$'' (see \S\ref{sec:simp}) or
    1.23 -``$\BY{blast}$'' (see \S\ref{sec:classical-auto}).  Accordingly, the
    1.24 -``$that$'' reduction above is declared as simplification and introduction
    1.25 -rule.
    1.26 +canonical automated tools such as ``$\BY{simp}$'' or ``$\BY{blast}$''.
    1.27 +Accordingly, the ``$that$'' reduction above is declared as simplification and
    1.28 +introduction rule.
    1.29  
    1.30  \medskip
    1.31  
    1.32 @@ -466,9 +466,9 @@
    1.33  \item [$elim_format$] turns a destruction rule into elimination rule format,
    1.34    by resolving with the rule $\PROP A \Imp (\PROP A \Imp \PROP B) \Imp \PROP
    1.35    B$.
    1.36 -
    1.37 -  Note that the Classical Reasoner (\S\ref{sec:classical-att}) provides its
    1.38 -  own version of this operation.
    1.39 +  
    1.40 +  Note that the Classical Reasoner (\S\ref{sec:classical}) provides its own
    1.41 +  version of this operation.
    1.42  
    1.43  \item [$standard$] puts a theorem into the standard form of object-rules at
    1.44    the outermost theory level.  Note that this operation violates the local
    1.45 @@ -612,7 +612,7 @@
    1.46  
    1.47  \subsection{The Simplifier}\label{sec:simplifier}
    1.48  
    1.49 -\subsubsection{Simplification methods}\label{sec:simp}
    1.50 +\subsubsection{Simplification methods}
    1.51  
    1.52  \indexisarmeth{simp}\indexisarmeth{simp-all}
    1.53  \begin{matharray}{rcl}
    1.54 @@ -737,13 +737,12 @@
    1.55  \end{rail}
    1.56  
    1.57  \begin{descr}
    1.58 -
    1.59 +  
    1.60  \item [$simplified~\vec a$] causes a theorem to be simplified, either by
    1.61    exactly the specified rules $\vec a$, or the implicit Simplifier context if
    1.62    no arguments are given.  The result is fully simplified by default,
    1.63    including assumptions and conclusion; the options $no_asm$ etc.\ tune the
    1.64 -  Simplifier in the same way as the for the $simp$ method (see
    1.65 -  \S\ref{sec:simp}).
    1.66 +  Simplifier in the same way as the for the $simp$ method.
    1.67  
    1.68    Note that forward simplification restricts the simplifier to its most basic
    1.69    operation of term rewriting; solver and looper tactics \cite{isabelle-ref}
    1.70 @@ -753,7 +752,7 @@
    1.71  \end{descr}
    1.72  
    1.73  
    1.74 -\subsubsection{Low-level equational reasoning}\label{sec:basic-eq}
    1.75 +\subsubsection{Low-level equational reasoning}
    1.76  
    1.77  \indexisarmeth{subst}\indexisarmeth{hypsubst}\indexisarmeth{split}
    1.78  \begin{matharray}{rcl}
    1.79 @@ -787,15 +786,15 @@
    1.80  \item [$split~\vec a$] performs single-step case splitting using rules $thms$.
    1.81    By default, splitting is performed in the conclusion of a goal; the $asm$
    1.82    option indicates to operate on assumptions instead.
    1.83 -
    1.84 +  
    1.85    Note that the $simp$ method already involves repeated application of split
    1.86 -  rules as declared in the current context (see \S\ref{sec:simp}).
    1.87 +  rules as declared in the current context.
    1.88  \end{descr}
    1.89  
    1.90  
    1.91  \subsection{The Classical Reasoner}\label{sec:classical}
    1.92  
    1.93 -\subsubsection{Basic methods}\label{sec:classical-basic}
    1.94 +\subsubsection{Basic methods}
    1.95  
    1.96  \indexisarmeth{rule}\indexisarmeth{default}\indexisarmeth{contradiction}
    1.97  \indexisarmeth{intro}\indexisarmeth{elim}
    1.98 @@ -835,7 +834,7 @@
    1.99  \end{descr}
   1.100  
   1.101  
   1.102 -\subsubsection{Automated methods}\label{sec:classical-auto}
   1.103 +\subsubsection{Automated methods}
   1.104  
   1.105  \indexisarmeth{blast}\indexisarmeth{fast}\indexisarmeth{slow}
   1.106  \indexisarmeth{best}\indexisarmeth{safe}\indexisarmeth{clarify}
   1.107 @@ -908,9 +907,9 @@
   1.108    tactics.  These correspond to \texttt{auto_tac}, \texttt{force_tac},
   1.109    \texttt{clarsimp_tac}, and Classical Reasoner tactics with the Simplifier
   1.110    added as wrapper, see \cite[\S11]{isabelle-ref} for more information.  The
   1.111 -  modifier arguments correspond to those given in \S\ref{sec:simp} and
   1.112 -  \S\ref{sec:classical-auto}.  Just note that the ones related to the
   1.113 -  Simplifier are prefixed by \railtterm{simp} here.
   1.114 +  modifier arguments correspond to those given in \S\ref{sec:simplifier} and
   1.115 +  \S\ref{sec:classical}.  Just note that the ones related to the Simplifier
   1.116 +  are prefixed by \railtterm{simp} here.
   1.117  
   1.118    Facts provided by forward chaining are inserted into the goal before doing
   1.119    the search.  The ``!''~argument causes the full context of assumptions to be
   1.120 @@ -918,7 +917,7 @@
   1.121  \end{descr}
   1.122  
   1.123  
   1.124 -\subsubsection{Declaring rules}\label{sec:classical-mod}
   1.125 +\subsubsection{Declaring rules}
   1.126  
   1.127  \indexisarcmd{print-claset}
   1.128  \indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}
   1.129 @@ -969,7 +968,7 @@
   1.130  \end{descr}
   1.131  
   1.132  
   1.133 -\subsubsection{Classical operations}\label{sec:classical-att}
   1.134 +\subsubsection{Classical operations}
   1.135  
   1.136  \indexisaratt{elim-format}\indexisaratt{swapped}
   1.137  
   1.138 @@ -994,7 +993,7 @@
   1.139  
   1.140  \subsection{Proof by cases and induction}\label{sec:cases-induct}
   1.141  
   1.142 -\subsubsection{Rule contexts}\label{sec:rule-cases}
   1.143 +\subsubsection{Rule contexts}
   1.144  
   1.145  \indexisarcmd{case}\indexisarcmd{print-cases}
   1.146  \indexisaratt{case-names}\indexisaratt{params}\indexisaratt{consumes}
   1.147 @@ -1106,9 +1105,9 @@
   1.148  and induction over datatypes, inductive sets, and recursive functions.  The
   1.149  corresponding rules may be specified and instantiated in a casual manner.
   1.150  Furthermore, these methods provide named local contexts that may be invoked
   1.151 -via the $\CASENAME$ proof command within the subsequent proof text (cf.\
   1.152 -\S\ref{sec:rule-cases}).  This accommodates compact proof texts even when
   1.153 -reasoning about large specifications.
   1.154 +via the $\CASENAME$ proof command within the subsequent proof text.  This
   1.155 +accommodates compact proof texts even when reasoning about large
   1.156 +specifications.
   1.157  
   1.158  \begin{rail}
   1.159    'cases' spec
   1.160 @@ -1175,16 +1174,16 @@
   1.161  
   1.162  \end{descr}
   1.163  
   1.164 -Above methods produce named local contexts (cf.\ \S\ref{sec:rule-cases}), as
   1.165 -determined by the instantiated rule as specified in the text.  Beyond that,
   1.166 -the $induct$ method guesses further instantiations from the goal specification
   1.167 -itself.  Any persisting unresolved schematic variables of the resulting rule
   1.168 -will render the the corresponding case invalid.  The term binding
   1.169 -$\Var{case}$\indexisarvar{case} for the conclusion will be provided with each
   1.170 -case, provided that term is fully specified.
   1.171 +Above methods produce named local contexts, as determined by the instantiated
   1.172 +rule as specified in the text.  Beyond that, the $induct$ method guesses
   1.173 +further instantiations from the goal specification itself.  Any persisting
   1.174 +unresolved schematic variables of the resulting rule will render the the
   1.175 +corresponding case invalid.  The term binding $\Var{case}$\indexisarvar{case}
   1.176 +for the conclusion will be provided with each case, provided that term is
   1.177 +fully specified.
   1.178  
   1.179 -The $\isarkeyword{print_cases}$ command (\S\ref{sec:rule-cases}) prints all
   1.180 -named cases present in the current proof state.
   1.181 +The $\isarkeyword{print_cases}$ command prints all named cases present in the
   1.182 +current proof state.
   1.183  
   1.184  \medskip
   1.185  
   1.186 @@ -1242,10 +1241,10 @@
   1.187    corresponding methods of the same name.  Certain definitional packages of
   1.188    object-logics usually declare emerging cases and induction rules as
   1.189    expected, so users rarely need to intervene.
   1.190 -
   1.191 +  
   1.192    Manual rule declarations usually include the the $case_names$ and $ps$
   1.193    attributes to adjust names of cases and parameters of a rule (see
   1.194 -  \S\ref{sec:rule-cases}); the $consumes$ declaration is taken care of
   1.195 +  \S\ref{sec:cases-induct}); the $consumes$ declaration is taken care of
   1.196    automatically: $consumes~0$ is specified for ``type'' rules and $consumes~1$
   1.197    for ``set'' rules.
   1.198