'cong' modifiers;
authorwenzelm
Tue Aug 29 00:53:48 2000 +0200 (2000-08-29)
changeset 971175df6a20b0b3
parent 9710 159469a85035
child 9712 e33422a2eb9c
'cong' modifiers;
doc-src/IsarRef/generic.tex
     1.1 --- a/doc-src/IsarRef/generic.tex	Tue Aug 29 00:53:21 2000 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Tue Aug 29 00:53:48 2000 +0200
     1.3 @@ -527,7 +527,8 @@
     1.4  
     1.5    opt: '(' (noasm | noasmsimp | noasmuse) ')'
     1.6    ;
     1.7 -  simpmod: ('add' | 'del' | 'only' | 'split' (() | 'add' | 'del') | 'other') ':' thmrefs
     1.8 +  simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') |
     1.9 +    'split' (() | 'add' | 'del') | 'other') ':' thmrefs
    1.10    ;
    1.11  \end{rail}
    1.12  
    1.13 @@ -536,15 +537,18 @@
    1.14    according to the arguments given.  Note that the \railtterm{only} modifier
    1.15    first removes all other rewrite rules, congruences, and looper tactics
    1.16    (including splits), and then behaves like \railtterm{add}.
    1.17 -
    1.18 -  The \railtterm{split} modifiers add or delete rules for the Splitter (see
    1.19 -  also \cite{isabelle-ref}), the default is to add.  This works only if the
    1.20 -  Simplifier method has been properly setup to include the Splitter (all major
    1.21 -  object logics such HOL, HOLCF, FOL, ZF do this already).
    1.22 -
    1.23 -  The \railtterm{other} modifier ignores its arguments.  Nevertheless,
    1.24 -  additional kinds of rules may be declared by including appropriate
    1.25 -  attributes in the specification.
    1.26 +  
    1.27 +  \medskip The \railtterm{cong} modifiers add or delete Simplifier congruence
    1.28 +  rules (see also \cite{isabelle-ref}), the default is to add.
    1.29 +  
    1.30 +  \medskip The \railtterm{split} modifiers add or delete rules for the
    1.31 +  Splitter (see also \cite{isabelle-ref}), the default is to add.  This works
    1.32 +  only if the Simplifier method has been properly setup to include the
    1.33 +  Splitter (all major object logics such HOL, HOLCF, FOL, ZF do this already).
    1.34 +  
    1.35 +  \medskip The \railtterm{other} modifier ignores its arguments.
    1.36 +  Nevertheless, additional kinds of rules may be declared by including
    1.37 +  appropriate attributes in the specification.
    1.38  \item [$simp_all$] is similar to $simp$, but acts on all goals.
    1.39  \end{descr}
    1.40  
    1.41 @@ -568,9 +572,9 @@
    1.42  \medskip
    1.43  
    1.44  The Splitter package is usually configured to work as part of the Simplifier.
    1.45 -There is no separate $split$ method available.  The effect of repeatedly
    1.46 -applying \texttt{split_tac} can be simulated by
    1.47 -$(simp~only\colon~split\colon~\vec a)$.
    1.48 +The effect of repeatedly applying \texttt{split_tac} can be simulated by
    1.49 +$(simp~only\colon~split\colon~\vec a)$.  There is also a separate $split$
    1.50 +method available for single-step case splitting, see \S\ref{sec:basic-eq}.
    1.51  
    1.52  
    1.53  \subsection{Declaring rules}
    1.54 @@ -580,12 +584,12 @@
    1.55  \begin{matharray}{rcl}
    1.56    print_simpset & : & \isarkeep{theory~|~proof} \\
    1.57    simp & : & \isaratt \\
    1.58 +  cong & : & \isaratt \\
    1.59    split & : & \isaratt \\
    1.60 -  cong & : & \isaratt \\
    1.61  \end{matharray}
    1.62  
    1.63  \begin{rail}
    1.64 -  ('simp' | 'split' | 'cong') (() | 'add' | 'del')
    1.65 +  ('simp' | 'cong' | 'split') (() | 'add' | 'del')
    1.66    ;
    1.67  \end{rail}
    1.68  
    1.69 @@ -594,8 +598,8 @@
    1.70    Simplifier, which is also known as ``simpset'' internally
    1.71    \cite{isabelle-ref}.  This is a diagnostic command; $undo$ does not apply.
    1.72  \item [$simp$] declares simplification rules.
    1.73 -\item [$split$] declares split rules.
    1.74  \item [$cong$] declares congruence rules.
    1.75 +\item [$split$] declares case split rules.
    1.76  \end{descr}
    1.77  
    1.78  
    1.79 @@ -618,7 +622,7 @@
    1.80  information.
    1.81  
    1.82  
    1.83 -\section{Basic equational reasoning}
    1.84 +\section{Basic equational reasoning}\label{sec:basic-eq}
    1.85  
    1.86  \indexisarmeth{subst}\indexisarmeth{hypsubst}\indexisarmeth{split}\indexisaratt{symmetric}
    1.87  \begin{matharray}{rcl}
    1.88 @@ -750,8 +754,8 @@
    1.89    ('auto' | 'force' | 'clarsimp' | 'fastsimp') ('!' ?) (clasimpmod * )
    1.90    ;
    1.91  
    1.92 -  clasimpmod: ('simp' (() | 'add' | 'del' | 'only') | 'other' |
    1.93 -    ('split' (() | 'add' | 'del')) |
    1.94 +  clasimpmod: ('simp' (() | 'add' | 'del' | 'only') |
    1.95 +    'cong' (() | 'add' | 'del') | ('split' (() | 'add' | 'del')) | 'other' |
    1.96      (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' thmrefs
    1.97  \end{rail}
    1.98