doc-src/IsarRef/generic.tex

--- a/doc-src/IsarRef/generic.tex	Wed Mar 15 23:41:42 2000 +0100
+++ b/doc-src/IsarRef/generic.tex	Thu Mar 16 00:26:44 2000 +0100
@@ -209,6 +209,73 @@
 %calculational steps in combination with natural deduction.
 
 
+\section{Named local contexts (cases)}\label{sec:cases}
+
+\indexisarcmd{case}\indexisarcmd{print-cases}
+\indexisaratt{case-names}\indexisaratt{params}
+\begin{matharray}{rcl}
+  \isarcmd{case} & : & \isartrans{proof(state)}{proof(state)} \\
+  \isarcmd{print_cases} & : & \isarkeep{proof} \\[0.5ex]
+  case_names & : & \isaratt \\
+  params & : & \isaratt \\
+\end{matharray}
+
+Basically, Isar proof contexts are built up explicitly using commands like
+$\FIXNAME$, $\ASSUMENAME$ etc.\ (see \S\ref{sec:proof-context}).  In typical
+verification tasks this can become hard to manage, though.  In particular, a
+large number of local contexts may emerge from case analysis or induction over
+inductive sets and types.
+
+\medskip
+
+The $\CASENAME$ command provides a shorthand to refer to certain parts of
+logical context symbolically.  Proof methods may provide an environment of
+named ``cases'' of the form $c\colon \vec x, \vec \chi$.  Then the effect of
+$\CASE{c}$ is exactly the same as $\FIX{\vec x}~\ASSUME{c}{\vec\chi}$.
+
+It is important to note that $\CASENAME$ does \emph{not} provide any means to
+peek at the current goal state, which is treated as strictly non-observable in
+Isar!  Instead, the cases considered here usually emerge in a canonical way
+from certain pieces of specification that appear in the theory somewhere else
+(e.g.\ in an inductive definition, or recursive function).  See also
+\S\ref{sec:induct-method} for more details of how this works in HOL.
+
+\medskip
+
+Named cases may be exhibited in the current proof context only if both the
+proof method and the corresponding rule support this.  Case names and
+parameters of basic rules may be declared by hand as well, by using
+appropriate attributes.  Thus variant versions of rules that have been derived
+manually may be used in advanced case analysis later.
+
+\railalias{casenames}{case\_names}
+\railterm{casenames}
+
+\begin{rail}
+  'case' nameref attributes?
+  ;
+  casenames (name + )
+  ;
+  'params' ((name * ) + 'and')
+  ;
+\end{rail}
+
+\begin{descr}
+\item [$\CASE{c}$] invokes a named local context $c\colon \vec x, \vec \chi$,
+  as provided by an appropriate proof method (such as $cases$ and $induct$,
+  see \S\ref{sec:induct-method}).  The command $\CASE{c}$ abbreviates
+  $\FIX{\vec x}~\ASSUME{c}{\vec\chi}$.
+\item [$\isarkeyword{print_cases}$] prints all local contexts of the current
+  goal context, using Isar proof language notation.  This is a diagnostic
+  command; $undo$ does not apply.
+\item [$case_names~\vec c$] declares names for the local contexts of premises
+  of some theorem ($\vec c$ refers to the \emph{suffix} of the list premises).
+\item [$params~\vec p@1 \dots \vec p@n$] renames the innermost parameters of
+  premises $1, \dots, n$ of some theorem.  An empty list of names be be given
+  to skip positions, leaving the corresponding parameters unchanged.
+\end{descr}
+
+
 \section{Axiomatic Type Classes}\label{sec:axclass}
 
 \indexisarcmd{axclass}\indexisarcmd{instance}\indexisarmeth{intro-classes}
@@ -261,51 +328,69 @@
 
 \subsection{Simplification methods}\label{sec:simp}
 
-\indexisarmeth{simp}
+\indexisarmeth{simp}\indexisarmeth{simp-all}
 \begin{matharray}{rcl}
   simp & : & \isarmeth \\
+  simp_all & : & \isarmeth \\
 \end{matharray}
 
+\railalias{simpall}{simp\_all}
+\railterm{simpall}
+
 \begin{rail}
-  'simp' ('!' ?) (simpmod * )
+  ('simp' | simpall) ('!' ?) (simpmod * )
   ;
 
-  simpmod: ('add' | 'del' | 'only' | 'other') ':' thmrefs
+  simpmod: ('add' | 'del' | 'only' | 'split' (() | 'add' | 'del') | 'other') ':' thmrefs
   ;
 \end{rail}
 
 \begin{descr}
 \item [$simp$] invokes Isabelle's simplifier, after modifying the context by
   adding or deleting rules as specified.  The \railtoken{only} modifier first
-  removes all other rewrite rules and congruences, and then is like
-  \railtoken{add}.  In contrast, \railtoken{other} ignores its arguments;
-  nevertheless there may be side-effects on the context via
-  attributes.\footnote{This provides a back door for arbitrary context
-    manipulation.}
+  removes all other rewrite rules, congruences, and looper tactics (including
+  splits), and then behaves like \railtoken{add}.
   
-  The $simp$ method is based on \texttt{asm_full_simp_tac}
-  \cite[\S10]{isabelle-ref}, but is much better behaved in practice.  Just the
-  local premises of the actual goal are involved by default.  Additional facts
-  may be inserted via forward-chaining (using $\THEN$, $\FROMNAME$ etc.).  The
-  full context of assumptions is only included in the $simp!$ version, which
-  should be used with care.
+  The \railtoken{split} modifiers add or delete rules for the Splitter (see
+  also \cite{isabelle-ref}), the default is to add.  This works only if the
+  Simplifier method has been properly setup to include the Splitter (all major
+  object logics such HOL, HOLCF, FOL, ZF do this already).
+  
+  The \railtoken{other} modifier ignores its arguments.  Nevertheless there
+  may be side-effects on the context via attributes.\footnote{This provides a
+    back door for arbitrary context manipulation.}
+  
+\item [$simp_all$] is similar to $simp$, but acts on all goals.
 \end{descr}
 
-\subsection{Modifying the context}
+The $simp$ methods are based on \texttt{asm_full_simp_tac}
+\cite[\S10]{isabelle-ref}, but is much better behaved in practice.  Just the
+local premises of the actual goal are involved by default.  Additional facts
+may be inserted via forward-chaining (using $\THEN$, $\FROMNAME$ etc.).  The
+full context of assumptions is only included in the $simp!$ versions, which
+should be used with some care, though.
 
-\indexisaratt{simp}
+Note that there is no separate $split$ method.  The effect of
+\texttt{split_tac} can be simulated via $(simp~only\colon~split\colon~thms)$.
+
+
+\subsection{Declaring rules}
+
+\indexisaratt{simp}\indexisaratt{split}
 \begin{matharray}{rcl}
   simp & : & \isaratt \\
+  split & : & \isaratt \\
 \end{matharray}
 
 \begin{rail}
-  'simp' (() | 'add' | 'del')
+  ('simp' | 'split') (() | 'add' | 'del')
   ;
 \end{rail}
 
 \begin{descr}
 \item [$simp$] adds or deletes rules from the theory or proof context (the
   default is to add).
+\item [$split$] is similar to $simp$, but refers to split rules.
 \end{descr}
 
 
@@ -421,7 +506,8 @@
   ('force' | 'auto') ('!' ?) (clasimpmod * )
   ;
 
-  clasimpmod: ('simp' ('add' | 'del' | 'only') | 'other' |
+  clasimpmod: ('simp' (() | 'add' | 'del' | 'only') | 'other' |
+    ('split' (() | 'add' | 'del')) |
     (('intro' | 'elim' | 'dest') (() | '?' | '??') | 'del')) ':' thmrefs
 \end{rail}
 
@@ -439,7 +525,7 @@
 \end{descr}
 
 
-\subsection{Modifying the context}\label{sec:classical-mod}
+\subsection{Declaring rules}\label{sec:classical-mod}
 
 \indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}
 \indexisaratt{iff}\indexisaratt{delrule}