doc-src/IsarRef/generic.tex

 
-\chapter{Generic Tools and Packages}\label{ch:gen-tools}
+\chapter{Generic tools and packages}\label{ch:gen-tools}
 
 \section{Theory specification commands}
 
 \subsection{Axiomatic type classes}\label{sec:axclass}
 

 \subsection{Locales and local contexts}\label{sec:locale}
 
 Locales are named local contexts, consisting of a list of declaration elements
 that are modeled after the Isar proof context commands (cf.\
 \S\ref{sec:proof-context}).
+
 
 \subsubsection{Localized commands}
 
 Existing locales may be augmented later on by adding new facts.  Note that the
 actual context definition may not be changed!  Several theory commands that

   \quad \QED{} \\
   \quad \FIX{\vec x}~\ASSUMENAME^\ast~a\colon~\vec\phi \\
 \end{matharray}
 
 Typically, the soundness proof is relatively straight-forward, often just by
-canonical automated tools such as ``$\BY{simp}$'' (see \S\ref{sec:simp}) or
-``$\BY{blast}$'' (see \S\ref{sec:classical-auto}).  Accordingly, the
-``$that$'' reduction above is declared as simplification and introduction
-rule.
+canonical automated tools such as ``$\BY{simp}$'' or ``$\BY{blast}$''.
+Accordingly, the ``$that$'' reduction above is declared as simplification and
+introduction rule.
 
 \medskip
 
 In a sense, $\OBTAINNAME$ represents at the level of Isar proofs what would be
 meta-logical existential quantifiers and conjunctions.  This concept has a

   given meta-level definitions throughout a rule.
 
 \item [$elim_format$] turns a destruction rule into elimination rule format,
   by resolving with the rule $\PROP A \Imp (\PROP A \Imp \PROP B) \Imp \PROP
   B$.
-
-  Note that the Classical Reasoner (\S\ref{sec:classical-att}) provides its
-  own version of this operation.
+  
+  Note that the Classical Reasoner (\S\ref{sec:classical}) provides its own
+  version of this operation.
 
 \item [$standard$] puts a theorem into the standard form of object-rules at
   the outermost theory level.  Note that this operation violates the local
   proof context (including active locales).
 

 \end{descr}
 
 
 \subsection{The Simplifier}\label{sec:simplifier}
 
-\subsubsection{Simplification methods}\label{sec:simp}
+\subsubsection{Simplification methods}
 
 \indexisarmeth{simp}\indexisarmeth{simp-all}
 \begin{matharray}{rcl}
   simp & : & \isarmeth \\
   simp_all & : & \isarmeth \\

   opt: '(' (noasm | noasmsimp | noasmuse) ')'
   ;
 \end{rail}
 
 \begin{descr}
-
+  
 \item [$simplified~\vec a$] causes a theorem to be simplified, either by
   exactly the specified rules $\vec a$, or the implicit Simplifier context if
   no arguments are given.  The result is fully simplified by default,
   including assumptions and conclusion; the options $no_asm$ etc.\ tune the
-  Simplifier in the same way as the for the $simp$ method (see
-  \S\ref{sec:simp}).
+  Simplifier in the same way as the for the $simp$ method.
 
   Note that forward simplification restricts the simplifier to its most basic
   operation of term rewriting; solver and looper tactics \cite{isabelle-ref}
   are \emph{not} involved here.  The $simplified$ attribute should be only
   rarely required under normal circumstances.
 
 \end{descr}
 
 
-\subsubsection{Low-level equational reasoning}\label{sec:basic-eq}
+\subsubsection{Low-level equational reasoning}
 
 \indexisarmeth{subst}\indexisarmeth{hypsubst}\indexisarmeth{split}
 \begin{matharray}{rcl}
   subst^* & : & \isarmeth \\
   hypsubst^* & : & \isarmeth \\

   variable.
 
 \item [$split~\vec a$] performs single-step case splitting using rules $thms$.
   By default, splitting is performed in the conclusion of a goal; the $asm$
   option indicates to operate on assumptions instead.
-
+  
   Note that the $simp$ method already involves repeated application of split
-  rules as declared in the current context (see \S\ref{sec:simp}).
+  rules as declared in the current context.
 \end{descr}
 
 
 \subsection{The Classical Reasoner}\label{sec:classical}
 
-\subsubsection{Basic methods}\label{sec:classical-basic}
+\subsubsection{Basic methods}
 
 \indexisarmeth{rule}\indexisarmeth{default}\indexisarmeth{contradiction}
 \indexisarmeth{intro}\indexisarmeth{elim}
 \begin{matharray}{rcl}
   rule & : & \isarmeth \\

   decomposition of a proof problem, in contrast to common automated tools.
 
 \end{descr}
 
 
-\subsubsection{Automated methods}\label{sec:classical-auto}
+\subsubsection{Automated methods}
 
 \indexisarmeth{blast}\indexisarmeth{fast}\indexisarmeth{slow}
 \indexisarmeth{best}\indexisarmeth{safe}\indexisarmeth{clarify}
 \begin{matharray}{rcl}
   blast & : & \isarmeth \\

 \item [$auto$, $force$, $clarsimp$, $fastsimp$, $slowsimp$, and $bestsimp$]
   provide access to Isabelle's combined simplification and classical reasoning
   tactics.  These correspond to \texttt{auto_tac}, \texttt{force_tac},
   \texttt{clarsimp_tac}, and Classical Reasoner tactics 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.
+  modifier arguments correspond to those given in \S\ref{sec:simplifier} and
+  \S\ref{sec:classical}.  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
   included as well.
 \end{descr}
 
 
-\subsubsection{Declaring rules}\label{sec:classical-mod}
+\subsubsection{Declaring rules}
 
 \indexisarcmd{print-claset}
 \indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}
 \indexisaratt{iff}\indexisaratt{rule}
 \begin{matharray}{rcl}

   and omits the Simplifier declaration.
 
 \end{descr}
 
 
-\subsubsection{Classical operations}\label{sec:classical-att}
+\subsubsection{Classical operations}
 
 \indexisaratt{elim-format}\indexisaratt{swapped}
 
 \begin{matharray}{rcl}
   elim_format & : & \isaratt \\

 \end{descr}
 
 
 \subsection{Proof by cases and induction}\label{sec:cases-induct}
 
-\subsubsection{Rule contexts}\label{sec:rule-cases}
+\subsubsection{Rule contexts}
 
 \indexisarcmd{case}\indexisarcmd{print-cases}
 \indexisaratt{case-names}\indexisaratt{params}\indexisaratt{consumes}
 \begin{matharray}{rcl}
   \isarcmd{case} & : & \isartrans{proof(state)}{proof(state)} \\

 
 The $cases$ and $induct$ methods provide a uniform interface to case analysis
 and induction over datatypes, inductive sets, and recursive functions.  The
 corresponding rules may be specified and instantiated in a casual manner.
 Furthermore, these methods provide named local contexts that may be invoked
-via the $\CASENAME$ proof command within the subsequent proof text (cf.\
-\S\ref{sec:rule-cases}).  This accommodates compact proof texts even when
-reasoning about large specifications.
+via the $\CASENAME$ proof command within the subsequent proof text.  This
+accommodates compact proof texts even when reasoning about large
+specifications.
 
 \begin{rail}
   'cases' spec
   ;
   'induct' spec

 
   The ``$(open)$'' option works the same way as for $cases$.
 
 \end{descr}
 
-Above methods produce named local contexts (cf.\ \S\ref{sec:rule-cases}), as
-determined by the instantiated rule as specified in the text.  Beyond that,
-the $induct$ method guesses further instantiations from the goal specification
-itself.  Any persisting unresolved schematic variables of the resulting rule
-will render the the corresponding case invalid.  The term binding
-$\Var{case}$\indexisarvar{case} for the conclusion will be provided with each
-case, provided that term is fully specified.
-
-The $\isarkeyword{print_cases}$ command (\S\ref{sec:rule-cases}) prints all
-named cases present in the current proof state.
+Above methods produce named local contexts, as determined by the instantiated
+rule as specified in the text.  Beyond that, the $induct$ method guesses
+further instantiations from the goal specification itself.  Any persisting
+unresolved schematic variables of the resulting rule will render the the
+corresponding case invalid.  The term binding $\Var{case}$\indexisarvar{case}
+for the conclusion will be provided with each case, provided that term is
+fully specified.
+
+The $\isarkeyword{print_cases}$ command prints all named cases present in the
+current proof state.
 
 \medskip
 
 It is important to note that there is a fundamental difference of the $cases$
 and $induct$ methods in handling of non-atomic goal statements: $cases$ just

 \item [$cases$ and $induct$] (as attributes) augment the corresponding context
   of rules for reasoning about inductive sets and types, using the
   corresponding methods of the same name.  Certain definitional packages of
   object-logics usually declare emerging cases and induction rules as
   expected, so users rarely need to intervene.
-
+  
   Manual rule declarations usually include the the $case_names$ and $ps$
   attributes to adjust names of cases and parameters of a rule (see
-  \S\ref{sec:rule-cases}); the $consumes$ declaration is taken care of
+  \S\ref{sec:cases-induct}); the $consumes$ declaration is taken care of
   automatically: $consumes~0$ is specified for ``type'' rules and $consumes~1$
   for ``set'' rules.
 
 \end{descr}