tuned;
authorwenzelm
Mon Mar 04 19:08:15 2002 +0100 (2002-03-04)
changeset 130157c3726a3dbec
parent 13014 3c1c493e6d93
child 13016 c039b8ede204
tuned;
doc-src/IsarRef/generic.tex
     1.1 --- a/doc-src/IsarRef/generic.tex	Mon Mar 04 19:07:58 2002 +0100
     1.2 +++ b/doc-src/IsarRef/generic.tex	Mon Mar 04 19:08:15 2002 +0100
     1.3 @@ -583,10 +583,6 @@
     1.4  
     1.5  \subsection{The Simplifier}\label{sec:simplifier}
     1.6  
     1.7 -\subsubsection{Basic equational reasoning}
     1.8 -
     1.9 -FIXME
    1.10 -
    1.11  \subsubsection{Simplification methods}\label{sec:simp}
    1.12  
    1.13  \indexisarmeth{simp}\indexisarmeth{simp-all}
    1.14 @@ -620,6 +616,7 @@
    1.15  \end{rail}
    1.16  
    1.17  \begin{descr}
    1.18 +
    1.19  \item [$simp$] invokes Isabelle's simplifier, after declaring additional rules
    1.20    according to the arguments given.  Note that the \railtterm{only} modifier
    1.21    first removes all other rewrite rules, congruences, and looper tactics
    1.22 @@ -632,25 +629,28 @@
    1.23    Splitter (see also \cite{isabelle-ref}), the default is to add.  This works
    1.24    only if the Simplifier method has been properly setup to include the
    1.25    Splitter (all major object logics such HOL, HOLCF, FOL, ZF do this already).
    1.26 -\item [$simp_all$] is similar to $simp$, but acts on all goals.
    1.27 +  
    1.28 +\item [$simp_all$] is similar to $simp$, but acts on all goals (backwards from
    1.29 +  the last to the first one).
    1.30 +
    1.31  \end{descr}
    1.32  
    1.33 -By default, the Simplifier methods are based on \texttt{asm_full_simp_tac}
    1.34 -internally \cite[\S10]{isabelle-ref}, which means that assumptions are both
    1.35 -simplified as well as used in simplifying the conclusion.  In structured
    1.36 -proofs this is usually quite well behaved in practice: just the local premises
    1.37 -of the actual goal are involved, additional facts may inserted via explicit
    1.38 -forward-chaining (using $\THEN$, $\FROMNAME$ etc.).  The full context of
    1.39 -assumptions is only included if the ``$!$'' (bang) argument is given, which
    1.40 -should be used with some care, though.
    1.41 +By default the Simplifier methods take local assumptions fully into account,
    1.42 +using equational assumptions in the subsequent normalization process, or
    1.43 +simplifying assumptions themselvess (cf.\ \texttt{asm_full_simp_tac} in
    1.44 +\cite[\S10]{isabelle-ref}).  In structured proofs this is usually quite well
    1.45 +behaved in practice: just the local premises of the actual goal are involved,
    1.46 +additional facts may inserted via explicit forward-chaining (using $\THEN$,
    1.47 +$\FROMNAME$ etc.).  The full context of assumptions is only included if the
    1.48 +``$!$'' (bang) argument is given, which should be used with some care, though.
    1.49  
    1.50 -Additional Simplifier options may be specified to tune the behavior even
    1.51 -further: $(no_asm)$ means assumptions are ignored completely (cf.\
    1.52 -\texttt{simp_tac}), $(no_asm_simp)$ means assumptions are used in the
    1.53 -simplification of the conclusion but are not themselves simplified (cf.\
    1.54 -\texttt{asm_simp_tac}), and $(no_asm_use)$ means assumptions are simplified
    1.55 -but are not used in the simplification of each other or the conclusion (cf.
    1.56 -\texttt{full_simp_tac}).
    1.57 +Additional Simplifier options may be specified to tune the behavior further
    1.58 +(mostly for unstructured scripts with many accidental local facts): $(no_asm)$
    1.59 +means assumptions are ignored completely (cf.\ \texttt{simp_tac}),
    1.60 +$(no_asm_simp)$ means assumptions are used in the simplification of the
    1.61 +conclusion but are not themselves simplified (cf.\ \texttt{asm_simp_tac}), and
    1.62 +$(no_asm_use)$ means assumptions are simplified but are not used in the
    1.63 +simplification of each other or the conclusion (cf.  \texttt{full_simp_tac}).
    1.64  
    1.65  \medskip
    1.66  
    1.67 @@ -688,15 +688,13 @@
    1.68  
    1.69  \subsubsection{Forward simplification}
    1.70  
    1.71 -FIXME thmargs
    1.72 -
    1.73  \indexisaratt{simplified}
    1.74  \begin{matharray}{rcl}
    1.75    simplified & : & \isaratt \\
    1.76  \end{matharray}
    1.77  
    1.78  \begin{rail}
    1.79 -  'simplified' opt?
    1.80 +  'simplified' opt? thmrefs?
    1.81    ;
    1.82  
    1.83    opt: '(' (noasm | noasmsimp | noasmuse) ')'
    1.84 @@ -704,27 +702,29 @@
    1.85  \end{rail}
    1.86  
    1.87  \begin{descr}
    1.88 -\item [$simplified$] causes a theorem to be simplified according to the
    1.89 -  current Simplifier context (there are no separate arguments for declaring
    1.90 -  additional rules).  By default the result is fully simplified, including
    1.91 -  assumptions and conclusion.  The options $no_asm$ etc.\ restrict the
    1.92 +  
    1.93 +\item [$simplified~\vec a$] causes a theorem to be simplified, either by
    1.94 +  exactly the specified rules $\vec a$, or the implicit Simplifier context if
    1.95 +  no arguments are given.  The result is fully simplified by default,
    1.96 +  including assumptions and conclusion; the options $no_asm$ etc.\ tune the
    1.97    Simplifier in the same way as the for the $simp$ method (see
    1.98 -  \S\ref{sec:simp}).  FIXME args
    1.99 +  \S\ref{sec:simp}).
   1.100    
   1.101 -  The $simplified$ operation should be used only very rarely, usually for
   1.102 -  experimentation only.
   1.103 +  Note that forward simplification restricts the simplifier to its most basic
   1.104 +  operation of term rewriting; solver and looper tactics \cite{isabelle-ref}
   1.105 +  are \emph{not} involved here.  The $simplified$ attribute should be only
   1.106 +  rarely required under normal circumstances.
   1.107 +
   1.108  \end{descr}
   1.109  
   1.110  
   1.111 -\subsubsection{Basic equational reasoning}\label{sec:basic-eq}
   1.112 -
   1.113 -FIXME move?
   1.114 +\subsubsection{Low-level equational reasoning}\label{sec:basic-eq}
   1.115  
   1.116  \indexisarmeth{subst}\indexisarmeth{hypsubst}\indexisarmeth{split}
   1.117  \begin{matharray}{rcl}
   1.118 -  subst & : & \isarmeth \\
   1.119 +  subst^* & : & \isarmeth \\
   1.120    hypsubst^* & : & \isarmeth \\
   1.121 -  split & : & \isarmeth \\
   1.122 +  split^* & : & \isarmeth \\
   1.123  \end{matharray}
   1.124  
   1.125  \begin{rail}
   1.126 @@ -734,16 +734,21 @@
   1.127    ;
   1.128  \end{rail}
   1.129  
   1.130 -These methods and attributes provide basic facilities for equational reasoning
   1.131 -that are intended for specialized applications only.  Normally, single step
   1.132 -reasoning would be performed by calculation (see \S\ref{sec:calculation}),
   1.133 -while the Simplifier is the canonical tool for automated normalization (see
   1.134 -\S\ref{sec:simplifier}).
   1.135 +These methods provide low-level facilities for equational reasoning that are
   1.136 +intended for specialized applications only.  Normally, single step
   1.137 +calculations would be performed in a structured text (see also
   1.138 +\S\ref{sec:calculation}), while the Simplifier methods provide the canonical
   1.139 +way for automated normalization (see \S\ref{sec:simplifier}).
   1.140  
   1.141  \begin{descr}
   1.142 +  
   1.143  \item [$subst~thm$] performs a single substitution step using rule $thm$,
   1.144    which may be either a meta or object equality.
   1.145 -\item [$hypsubst$] performs substitution using some assumption.
   1.146 +  
   1.147 +\item [$hypsubst$] performs substitution using some assumption.  Note that
   1.148 +  this only works for equations of the form $x = t$ where $x$ is a free or
   1.149 +  bound variable!
   1.150 +  
   1.151  \item [$split~thms$] performs single-step case splitting using rules $thms$.
   1.152    By default, splitting is performed in the conclusion of a goal; the $asm$
   1.153    option indicates to operate on assumptions instead.