# HG changeset patch
# User wenzelm
# Date 1351974700 -3600
# Node ID 7e491da6bcbde2f7dae1057bf3953642ba091abf
# Parent  e038198f7d080eab27cc67f9a870977ce79585e1
more on the Simplifier, based on old material;

diff -r e038198f7d08 -r 7e491da6bcbd src/Doc/IsarRef/Generic.thy
--- a/src/Doc/IsarRef/Generic.thy	Sat Nov 03 19:07:07 2012 +0100
+++ b/src/Doc/IsarRef/Generic.thy	Sat Nov 03 21:31:40 2012 +0100
@@ -377,7 +377,22 @@
 
 section {* The Simplifier \label{sec:simplifier} *}
 
-subsection {* Simplification methods *}
+text {* The Simplifier performs conditional and unconditional
+  rewriting and uses contextual information: rule declarations in the
+  background theory or local proof context are taken into account, as
+  well as chained facts and subgoal premises (``local assumptions'').
+  There are several general hooks that allow to modify the
+  simplification strategy, or incorporate other proof tools that solve
+  sub-problems, produce rewrite rules on demand etc.
+
+  The default Simplifier setup of major object logics (HOL, HOLCF,
+  FOL, ZF) makes the Simplifier ready for immediate use, without
+  engaging into the internal structures.  Thus it serves as
+  general-purpose proof tool with the main focus on equational
+  reasoning, and a bit more than that.  *}
+
+
+subsection {* Simplification methods \label{sec:simp-meth} *}
 
 text {*
   \begin{matharray}{rcl}
@@ -391,21 +406,34 @@
 
     opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use' | 'asm_lr' ) ')'
     ;
-    @{syntax_def simpmod}: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') |
-      'split' (() | 'add' | 'del')) ':' @{syntax thmrefs}
+    @{syntax_def simpmod}: ('add' | 'del' | 'only' | 'split' (() | 'add' | 'del') |
+      'cong' (() | 'add' | 'del')) ':' @{syntax thmrefs}
   "}
 
   \begin{description}
 
-  \item @{method simp} invokes the Simplifier, after declaring
-  additional rules according to the arguments given.  Note that the
-  @{text only} modifier first removes all other rewrite rules,
-  congruences, and looper tactics (including splits), and then behaves
-  like @{text add}.
+  \item @{method simp} invokes the Simplifier on the first subgoal,
+  after inserting chained facts as additional goal premises; further
+  rule declarations may be included via @{text "(simp add: facts)"}.
+  The proof method fails if the subgoal remains unchanged after
+  simplification.
 
-  \medskip The @{text cong} modifiers add or delete Simplifier
-  congruence rules (see also \secref{sec:simp-cong}), the default is
-  to add.
+  Note that the original goal premises and chained facts are subject
+  to simplification themselves, while declarations via @{text
+  "add"}/@{text "del"} merely follow the policies of the object-logic
+  to extract rewrite rules from theorems, without further
+  simplification.  This may lead to slightly different behavior in
+  either case, which might be required precisely like that in some
+  boundary situations to perform the intended simplification step!
+
+  \medskip The @{text only} modifier first removes all other rewrite
+  rules, looper tactics (including split rules), congruence rules, and
+  then behaves like @{text add}.  Implicit solvers remain, which means
+  that trivial rules like reflexivity or introduction of @{text
+  "True"} are available to solve the simplified subgoals, but also
+  non-trivial tools like linear arithmetic in HOL.  The latter may
+  lead to some surprise of the meaning of ``only'' in Isabelle/HOL
+  compared to English!
 
   \medskip The @{text split} modifiers add or delete rules for the
   Splitter (see also \cite{isabelle-ref}), the default is to add.
@@ -413,36 +441,60 @@
   include the Splitter (all major object logics such HOL, HOLCF, FOL,
   ZF do this already).
 
+  \medskip The @{text cong} modifiers add or delete Simplifier
+  congruence rules (see also \secref{sec:simp-rules}); the default is
+  to add.
+
   \item @{method simp_all} is similar to @{method simp}, but acts on
-  all goals (backwards from the last to the first one).
+  all goals, working backwards from the last to the first one as usual
+  in Isabelle.\footnote{The order is irrelevant for goals without
+  schematic variables, so simplification might actually be performed
+  in parallel here.}
+
+  Chained facts are inserted into all subgoals, before the
+  simplification process starts.  Further rule declarations are the
+  same as for @{method simp}.
+
+  The proof method fails if all subgoals remain unchanged after
+  simplification.
 
   \end{description}
 
-  By default the Simplifier methods take local assumptions fully into
-  account, using equational assumptions in the subsequent
-  normalization process, or simplifying assumptions themselves (cf.\
-  @{ML asm_full_simp_tac} in \cite{isabelle-ref}).  In structured
-  proofs this is usually quite well behaved in practice: just the
-  local premises of the actual goal are involved, additional facts may
-  be inserted via explicit forward-chaining (via @{command "then"},
-  @{command "from"}, @{command "using"} etc.).
+  By default the Simplifier methods above take local assumptions fully
+  into account, using equational assumptions in the subsequent
+  normalization process, or simplifying assumptions themselves.
+  Further options allow to fine-tune the behavior of the Simplifier
+  in this respect, corresponding to a variety of ML tactics as
+  follows.\footnote{Unlike the corresponding Isar proof methods, the
+  ML tactics do not insist in changing the goal state.}
+
+  \begin{center}
+  \small
+  \begin{tabular}{|l|l|p{0.3\textwidth}|}
+  \hline
+  Isar method & ML tactic & behavior \\\hline
+
+  @{text "(simp (no_asm))"} & @{ML simp_tac} & assumptions are ignored
+  completely \\\hline
 
-  Additional Simplifier options may be specified to tune the behavior
-  further (mostly for unstructured scripts with many accidental local
-  facts): ``@{text "(no_asm)"}'' means assumptions are ignored
-  completely (cf.\ @{ML simp_tac}), ``@{text "(no_asm_simp)"}'' means
-  assumptions are used in the simplification of the conclusion but are
-  not themselves simplified (cf.\ @{ML asm_simp_tac}), and ``@{text
-  "(no_asm_use)"}'' means assumptions are simplified but are not used
-  in the simplification of each other or the conclusion (cf.\ @{ML
-  full_simp_tac}).  For compatibility reasons, there is also an option
-  ``@{text "(asm_lr)"}'', which means that an assumption is only used
-  for simplifying assumptions which are to the right of it (cf.\ @{ML
-  asm_lr_simp_tac}).
+  @{text "(simp (no_asm_simp))"} & @{ML asm_simp_tac} & assumptions
+  are used in the simplification of the conclusion but are not
+  themselves simplified \\\hline
+
+  @{text "(simp (no_asm_use))"} & @{ML full_simp_tac} & assumptions
+  are simplified but are not used in the simplification of each other
+  or the conclusion \\\hline
 
-  The configuration option @{text "depth_limit"} limits the number of
-  recursive invocations of the simplifier during conditional
-  rewriting.
+  @{text "(simp)"} & @{ML asm_full_simp_tac} & assumptions are used in
+  the simplification of the conclusion and to simplify other
+  assumptions \\\hline
+
+  @{text "(simp (asm_lr))"} & @{ML asm_lr_simp_tac} & compatibility
+  mode: an assumption is only used for simplifying assumptions which
+  are to the right of it \\\hline
+
+  \end{tabular}
+  \end{center}
 
   \medskip The Splitter package is usually configured to work as part
   of the Simplifier.  The effect of repeatedly applying @{ML
@@ -452,51 +504,45 @@
 *}
 
 
-subsection {* Declaring rules *}
+subsection {* Declaring rules \label{sec:simp-rules} *}
 
 text {*
   \begin{matharray}{rcl}
     @{command_def "print_simpset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{attribute_def simp} & : & @{text attribute} \\
     @{attribute_def split} & : & @{text attribute} \\
+    @{attribute_def cong} & : & @{text attribute} \\
   \end{matharray}
 
   @{rail "
-    (@@{attribute simp} | @@{attribute split}) (() | 'add' | 'del')
+    (@@{attribute simp} | @@{attribute split} | @@{attribute cong})
+      (() | 'add' | 'del')
   "}
 
   \begin{description}
 
   \item @{command "print_simpset"} prints the collection of rules
   declared to the Simplifier, which is also known as ``simpset''
-  internally \cite{isabelle-ref}.
+  internally.
+
+  For historical reasons, simpsets may occur independently from the
+  current context, but are conceptually dependent on it.  When the
+  Simplifier is invoked via one of its main entry points in the Isar
+  source language (as proof method \secref{sec:simp-meth} or rule
+  attribute \secref{sec:simp-meth}), its simpset is derived from the
+  current proof context, and carries a back-reference to that for
+  other tools that might get invoked internally (e.g.\ simplification
+  procedures \secref{sec:simproc}).  A mismatch of the context of the
+  simpset and the context of the problem being simplified may lead to
+  unexpected results.
 
   \item @{attribute simp} declares simplification rules.
 
   \item @{attribute split} declares case split rules.
 
-  \end{description}
-*}
-
-
-subsection {* Congruence rules\label{sec:simp-cong} *}
-
-text {*
-  \begin{matharray}{rcl}
-    @{attribute_def cong} & : & @{text attribute} \\
-  \end{matharray}
-
-  @{rail "
-    @@{attribute cong} (() | 'add' | 'del')
-  "}
-
-  \begin{description}
-
   \item @{attribute cong} declares congruence rules to the Simplifier
   context.
 
-  \end{description}
-
   Congruence rules are equalities of the form @{text [display]
   "\<dots> \<Longrightarrow> f ?x\<^sub>1 \<dots> ?x\<^sub>n = f ?y\<^sub>1 \<dots> ?y\<^sub>n"}
 
@@ -532,10 +578,47 @@
   Only the first argument is simplified; the others remain unchanged.
   This can make simplification much faster, but may require an extra
   case split over the condition @{text "?q"} to prove the goal.
+
+  \end{description}
 *}
 
 
-subsection {* Simplification procedures *}
+subsection {* Configuration options \label{sec:simp-config} *}
+
+text {*
+  \begin{tabular}{rcll}
+    @{attribute_def simp_depth_limit} & : & @{text attribute} & default @{text 100} \\
+    @{attribute_def simp_trace} & : & @{text attribute} & default @{text false} \\
+    @{attribute_def simp_trace_depth_limit} & : & @{text attribute} & default @{text 1} \\
+    @{attribute_def simp_debug} & : & @{text attribute} & default @{text false} \\
+  \end{tabular}
+  \medskip
+
+  These configurations options control further aspects of the Simplifier.
+  See also \secref{sec:config}.
+
+  \begin{description}
+
+  \item @{attribute simp_depth_limit} limits the number of recursive
+  invocations of the Simplifier during conditional rewriting.
+
+  \item @{attribute simp_trace} makes the Simplifier output internal
+  operations.  This includes rewrite steps, but also bookkeeping like
+  modifications of the simpset.
+
+  \item @{attribute simp_trace_depth_limit} limits the effect of
+  @{attribute simp_trace} to the given depth of recursive Simplifier
+  invocations (when solving conditions of rewrite rules).
+
+  \item @{attribute simp_debug} makes the Simplifier output some extra
+  information about internal operations.  This includes any attempted
+  invocation of simplification procedures.
+
+  \end{description}
+*}
+
+
+subsection {* Simplification procedures \label{sec:simproc} *}
 
 text {* Simplification procedures are ML functions that produce proven
   rewrite rules on demand.  They are associated with higher-order
@@ -616,7 +699,7 @@
   reasonably fast. *}
 
 
-subsection {* Forward simplification *}
+subsection {* Forward simplification \label{sec:simp-forward} *}
 
 text {*
   \begin{matharray}{rcl}
diff -r e038198f7d08 -r 7e491da6bcbd src/Doc/Ref/document/simplifier.tex
--- a/src/Doc/Ref/document/simplifier.tex	Sat Nov 03 19:07:07 2012 +0100
+++ b/src/Doc/Ref/document/simplifier.tex	Sat Nov 03 21:31:40 2012 +0100
@@ -3,42 +3,16 @@
 \label{chap:simplification}
 \index{simplification|(}
 
-This chapter describes Isabelle's generic simplification package.  It performs
-conditional and unconditional rewriting and uses contextual information
-(`local assumptions').  It provides several general hooks, which can provide
-automatic case splits during rewriting, for example.  The simplifier is
-already set up for many of Isabelle's logics: FOL, ZF, HOL, HOLCF.
-
-The first section is a quick introduction to the simplifier that
-should be sufficient to get started.  The later sections explain more
-advanced features.
-
 
 \section{Simplification for dummies}
 \label{sec:simp-for-dummies}
 
-Basic use of the simplifier is particularly easy because each theory
-is equipped with sensible default information controlling the rewrite
-process --- namely the implicit {\em current
-  simpset}\index{simpset!current}.  A suite of simple commands is
-provided that refer to the implicit simpset of the current theory
-context.
-
-\begin{warn}
-  Make sure that you are working within the correct theory context.
-  Executing proofs interactively, or loading them from ML files
-  without associated theories may require setting the current theory
-  manually via the \ttindex{context} command.
-\end{warn}
-
 \subsection{Simplification tactics} \label{sec:simp-for-dummies-tacs}
 \begin{ttbox}
 Simp_tac          : int -> tactic
 Asm_simp_tac      : int -> tactic
 Full_simp_tac     : int -> tactic
 Asm_full_simp_tac : int -> tactic
-trace_simp        : bool ref \hfill{\bf initially false}
-debug_simp        : bool ref \hfill{\bf initially false}
 \end{ttbox}
 
 \begin{ttdescription}
@@ -60,12 +34,6 @@
 \footnote{\texttt{Asm_full_simp_tac} used to process the assumptions from
   left to right. For backwards compatibilty reasons only there is now
   \texttt{Asm_lr_simp_tac} that behaves like the old \texttt{Asm_full_simp_tac}.}
-\item[set \ttindexbold{trace_simp};] makes the simplifier output internal
-  operations.  This includes rewrite steps, but also bookkeeping like
-  modifications of the simpset.
-\item[set \ttindexbold{debug_simp};] makes the simplifier output some extra
-  information about internal operations.  This includes any attempted
-  invocation of simplification procedures.
 \end{ttdescription}
 
 \medskip
@@ -122,14 +90,6 @@
 \end{ttbox}
 terminates.
 
-\medskip
-
-Using the simplifier effectively may take a bit of experimentation.
-Set the \verb$trace_simp$\index{tracing!of simplification} flag to get
-a better idea of what is going on.  The resulting output can be
-enormous, especially since invocations of the simplifier are often
-nested (e.g.\ when solving conditions of rewrite rules).
-
 
 \subsection{Modifying the current simpset}
 \begin{ttbox}