doc-src/IsarRef/generic.tex
changeset 8483 b437907f9b26
parent 8203 2fcc6017cb72
child 8507 d22fcea34cb7
     1.1 --- a/doc-src/IsarRef/generic.tex	Wed Mar 15 23:41:42 2000 +0100
     1.2 +++ b/doc-src/IsarRef/generic.tex	Thu Mar 16 00:26:44 2000 +0100
     1.3 @@ -209,6 +209,73 @@
     1.4  %calculational steps in combination with natural deduction.
     1.5  
     1.6  
     1.7 +\section{Named local contexts (cases)}\label{sec:cases}
     1.8 +
     1.9 +\indexisarcmd{case}\indexisarcmd{print-cases}
    1.10 +\indexisaratt{case-names}\indexisaratt{params}
    1.11 +\begin{matharray}{rcl}
    1.12 +  \isarcmd{case} & : & \isartrans{proof(state)}{proof(state)} \\
    1.13 +  \isarcmd{print_cases} & : & \isarkeep{proof} \\[0.5ex]
    1.14 +  case_names & : & \isaratt \\
    1.15 +  params & : & \isaratt \\
    1.16 +\end{matharray}
    1.17 +
    1.18 +Basically, Isar proof contexts are built up explicitly using commands like
    1.19 +$\FIXNAME$, $\ASSUMENAME$ etc.\ (see \S\ref{sec:proof-context}).  In typical
    1.20 +verification tasks this can become hard to manage, though.  In particular, a
    1.21 +large number of local contexts may emerge from case analysis or induction over
    1.22 +inductive sets and types.
    1.23 +
    1.24 +\medskip
    1.25 +
    1.26 +The $\CASENAME$ command provides a shorthand to refer to certain parts of
    1.27 +logical context symbolically.  Proof methods may provide an environment of
    1.28 +named ``cases'' of the form $c\colon \vec x, \vec \chi$.  Then the effect of
    1.29 +$\CASE{c}$ is exactly the same as $\FIX{\vec x}~\ASSUME{c}{\vec\chi}$.
    1.30 +
    1.31 +It is important to note that $\CASENAME$ does \emph{not} provide any means to
    1.32 +peek at the current goal state, which is treated as strictly non-observable in
    1.33 +Isar!  Instead, the cases considered here usually emerge in a canonical way
    1.34 +from certain pieces of specification that appear in the theory somewhere else
    1.35 +(e.g.\ in an inductive definition, or recursive function).  See also
    1.36 +\S\ref{sec:induct-method} for more details of how this works in HOL.
    1.37 +
    1.38 +\medskip
    1.39 +
    1.40 +Named cases may be exhibited in the current proof context only if both the
    1.41 +proof method and the corresponding rule support this.  Case names and
    1.42 +parameters of basic rules may be declared by hand as well, by using
    1.43 +appropriate attributes.  Thus variant versions of rules that have been derived
    1.44 +manually may be used in advanced case analysis later.
    1.45 +
    1.46 +\railalias{casenames}{case\_names}
    1.47 +\railterm{casenames}
    1.48 +
    1.49 +\begin{rail}
    1.50 +  'case' nameref attributes?
    1.51 +  ;
    1.52 +  casenames (name + )
    1.53 +  ;
    1.54 +  'params' ((name * ) + 'and')
    1.55 +  ;
    1.56 +\end{rail}
    1.57 +
    1.58 +\begin{descr}
    1.59 +\item [$\CASE{c}$] invokes a named local context $c\colon \vec x, \vec \chi$,
    1.60 +  as provided by an appropriate proof method (such as $cases$ and $induct$,
    1.61 +  see \S\ref{sec:induct-method}).  The command $\CASE{c}$ abbreviates
    1.62 +  $\FIX{\vec x}~\ASSUME{c}{\vec\chi}$.
    1.63 +\item [$\isarkeyword{print_cases}$] prints all local contexts of the current
    1.64 +  goal context, using Isar proof language notation.  This is a diagnostic
    1.65 +  command; $undo$ does not apply.
    1.66 +\item [$case_names~\vec c$] declares names for the local contexts of premises
    1.67 +  of some theorem ($\vec c$ refers to the \emph{suffix} of the list premises).
    1.68 +\item [$params~\vec p@1 \dots \vec p@n$] renames the innermost parameters of
    1.69 +  premises $1, \dots, n$ of some theorem.  An empty list of names be be given
    1.70 +  to skip positions, leaving the corresponding parameters unchanged.
    1.71 +\end{descr}
    1.72 +
    1.73 +
    1.74  \section{Axiomatic Type Classes}\label{sec:axclass}
    1.75  
    1.76  \indexisarcmd{axclass}\indexisarcmd{instance}\indexisarmeth{intro-classes}
    1.77 @@ -261,51 +328,69 @@
    1.78  
    1.79  \subsection{Simplification methods}\label{sec:simp}
    1.80  
    1.81 -\indexisarmeth{simp}
    1.82 +\indexisarmeth{simp}\indexisarmeth{simp-all}
    1.83  \begin{matharray}{rcl}
    1.84    simp & : & \isarmeth \\
    1.85 +  simp_all & : & \isarmeth \\
    1.86  \end{matharray}
    1.87  
    1.88 +\railalias{simpall}{simp\_all}
    1.89 +\railterm{simpall}
    1.90 +
    1.91  \begin{rail}
    1.92 -  'simp' ('!' ?) (simpmod * )
    1.93 +  ('simp' | simpall) ('!' ?) (simpmod * )
    1.94    ;
    1.95  
    1.96 -  simpmod: ('add' | 'del' | 'only' | 'other') ':' thmrefs
    1.97 +  simpmod: ('add' | 'del' | 'only' | 'split' (() | 'add' | 'del') | 'other') ':' thmrefs
    1.98    ;
    1.99  \end{rail}
   1.100  
   1.101  \begin{descr}
   1.102  \item [$simp$] invokes Isabelle's simplifier, after modifying the context by
   1.103    adding or deleting rules as specified.  The \railtoken{only} modifier first
   1.104 -  removes all other rewrite rules and congruences, and then is like
   1.105 -  \railtoken{add}.  In contrast, \railtoken{other} ignores its arguments;
   1.106 -  nevertheless there may be side-effects on the context via
   1.107 -  attributes.\footnote{This provides a back door for arbitrary context
   1.108 -    manipulation.}
   1.109 +  removes all other rewrite rules, congruences, and looper tactics (including
   1.110 +  splits), and then behaves like \railtoken{add}.
   1.111    
   1.112 -  The $simp$ method is based on \texttt{asm_full_simp_tac}
   1.113 -  \cite[\S10]{isabelle-ref}, but is much better behaved in practice.  Just the
   1.114 -  local premises of the actual goal are involved by default.  Additional facts
   1.115 -  may be inserted via forward-chaining (using $\THEN$, $\FROMNAME$ etc.).  The
   1.116 -  full context of assumptions is only included in the $simp!$ version, which
   1.117 -  should be used with care.
   1.118 +  The \railtoken{split} modifiers add or delete rules for the Splitter (see
   1.119 +  also \cite{isabelle-ref}), the default is to add.  This works only if the
   1.120 +  Simplifier method has been properly setup to include the Splitter (all major
   1.121 +  object logics such HOL, HOLCF, FOL, ZF do this already).
   1.122 +  
   1.123 +  The \railtoken{other} modifier ignores its arguments.  Nevertheless there
   1.124 +  may be side-effects on the context via attributes.\footnote{This provides a
   1.125 +    back door for arbitrary context manipulation.}
   1.126 +  
   1.127 +\item [$simp_all$] is similar to $simp$, but acts on all goals.
   1.128  \end{descr}
   1.129  
   1.130 -\subsection{Modifying the context}
   1.131 +The $simp$ methods are based on \texttt{asm_full_simp_tac}
   1.132 +\cite[\S10]{isabelle-ref}, but is much better behaved in practice.  Just the
   1.133 +local premises of the actual goal are involved by default.  Additional facts
   1.134 +may be inserted via forward-chaining (using $\THEN$, $\FROMNAME$ etc.).  The
   1.135 +full context of assumptions is only included in the $simp!$ versions, which
   1.136 +should be used with some care, though.
   1.137  
   1.138 -\indexisaratt{simp}
   1.139 +Note that there is no separate $split$ method.  The effect of
   1.140 +\texttt{split_tac} can be simulated via $(simp~only\colon~split\colon~thms)$.
   1.141 +
   1.142 +
   1.143 +\subsection{Declaring rules}
   1.144 +
   1.145 +\indexisaratt{simp}\indexisaratt{split}
   1.146  \begin{matharray}{rcl}
   1.147    simp & : & \isaratt \\
   1.148 +  split & : & \isaratt \\
   1.149  \end{matharray}
   1.150  
   1.151  \begin{rail}
   1.152 -  'simp' (() | 'add' | 'del')
   1.153 +  ('simp' | 'split') (() | 'add' | 'del')
   1.154    ;
   1.155  \end{rail}
   1.156  
   1.157  \begin{descr}
   1.158  \item [$simp$] adds or deletes rules from the theory or proof context (the
   1.159    default is to add).
   1.160 +\item [$split$] is similar to $simp$, but refers to split rules.
   1.161  \end{descr}
   1.162  
   1.163  
   1.164 @@ -421,7 +506,8 @@
   1.165    ('force' | 'auto') ('!' ?) (clasimpmod * )
   1.166    ;
   1.167  
   1.168 -  clasimpmod: ('simp' ('add' | 'del' | 'only') | 'other' |
   1.169 +  clasimpmod: ('simp' (() | 'add' | 'del' | 'only') | 'other' |
   1.170 +    ('split' (() | 'add' | 'del')) |
   1.171      (('intro' | 'elim' | 'dest') (() | '?' | '??') | 'del')) ':' thmrefs
   1.172  \end{rail}
   1.173  
   1.174 @@ -439,7 +525,7 @@
   1.175  \end{descr}
   1.176  
   1.177  
   1.178 -\subsection{Modifying the context}\label{sec:classical-mod}
   1.179 +\subsection{Declaring rules}\label{sec:classical-mod}
   1.180  
   1.181  \indexisaratt{intro}\indexisaratt{elim}\indexisaratt{dest}
   1.182  \indexisaratt{iff}\indexisaratt{delrule}