# HG changeset patch
# User wenzelm
# Date 1352574976 -3600
# Node ID 5c36db9db335bb2ae05426abd6230894480925a0
# Parent  02aa7f6e530d09e235cfb4497439cfb0116bb8ed
updated subgoaler/solver/looper;

diff -r 02aa7f6e530d -r 5c36db9db335 src/Doc/IsarRef/Generic.thy
--- a/src/Doc/IsarRef/Generic.thy	Thu Nov 08 20:25:48 2012 +0100
+++ b/src/Doc/IsarRef/Generic.thy	Sat Nov 10 20:16:16 2012 +0100
@@ -442,7 +442,7 @@
   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.
+  Splitter (see also \secref{sec:simp-strategies} on the looper).
   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).
@@ -882,6 +882,253 @@
   reasonably fast. *}
 
 
+subsection {* Configurable Simplifier strategies \label{sec:simp-strategies} *}
+
+text {* The core term-rewriting engine of the Simplifier is normally
+  used in combination with some add-on components that modify the
+  strategy and allow to integrate other non-Simplifier proof tools.
+  These may be reconfigured in ML as explained below.  Even if the
+  default strategies of object-logics like Isabelle/HOL are used
+  unchanged, it helps to understand how the standard Simplifier
+  strategies work. *}
+
+
+subsubsection {* The subgoaler *}
+
+text {*
+  \begin{mldecls}
+  @{index_ML Simplifier.set_subgoaler: "(simpset -> int -> tactic) ->
+  simpset -> simpset"} \\
+  @{index_ML Simplifier.prems_of: "simpset -> thm list"} \\
+  \end{mldecls}
+
+  The subgoaler is the tactic used to solve subgoals arising out of
+  conditional rewrite rules or congruence rules.  The default should
+  be simplification itself.  In rare situations, this strategy may
+  need to be changed.  For example, if the premise of a conditional
+  rule is an instance of its conclusion, as in @{text "Suc ?m < ?n \<Longrightarrow>
+  ?m < ?n"}, the default strategy could loop.  % FIXME !??
+
+  \begin{description}
+
+  \item @{ML Simplifier.set_subgoaler}~@{text "ss tac"} sets the
+  subgoaler of simpset @{text "ss"} to @{text "tac"}.  The tactic will
+  be applied to the context of the running Simplifier instance,
+  expressed as a simpset.
+
+  \item @{ML Simplifier.prems_of}~@{text "ss"} retrieves the current
+  set of premises from simpset @{text "ss"} that represents the
+  context of the running Simplifier.  This may be non-empty only if
+  the Simplifier has been told to utilize local assumptions in the
+  first place (cf.\ the options in \secref{sec:simp-meth}).
+
+  \end{description}
+
+  As an example, consider the following alternative subgoaler:
+*}
+
+ML {*
+  fun subgoaler_tac ss =
+    assume_tac ORELSE'
+    resolve_tac (Simplifier.prems_of ss) ORELSE'
+    asm_simp_tac ss
+*}
+
+text {* This tactic first tries to solve the subgoal by assumption or
+  by resolving with with one of the premises, calling simplification
+  only if that fails. *}
+
+
+subsubsection {* The solver *}
+
+text {*
+  \begin{mldecls}
+  @{index_ML_type solver} \\
+  @{index_ML Simplifier.mk_solver: "string -> (simpset -> int -> tactic) ->
+  solver"} \\
+  @{index_ML_op setSolver: "simpset * solver -> simpset"} \\
+  @{index_ML_op addSolver: "simpset * solver -> simpset"} \\
+  @{index_ML_op setSSolver: "simpset * solver -> simpset"} \\
+  @{index_ML_op addSSolver: "simpset * solver -> simpset"} \\
+  \end{mldecls}
+
+  A solver is a tactic that attempts to solve a subgoal after
+  simplification.  Its core functionality is to prove trivial subgoals
+  such as @{prop "True"} and @{text "t = t"}, but object-logics might
+  be more ambitious.  For example, Isabelle/HOL performs a restricted
+  version of linear arithmetic here.
+
+  Solvers are packaged up in abstract type @{ML_type solver}, with
+  @{ML Simplifier.mk_solver} as the only operation to create a solver.
+
+  \medskip Rewriting does not instantiate unknowns.  For example,
+  rewriting alone cannot prove @{text "a \<in> ?A"} since this requires
+  instantiating @{text "?A"}.  The solver, however, is an arbitrary
+  tactic and may instantiate unknowns as it pleases.  This is the only
+  way the Simplifier can handle a conditional rewrite rule whose
+  condition contains extra variables.  When a simplification tactic is
+  to be combined with other provers, especially with the Classical
+  Reasoner, it is important whether it can be considered safe or not.
+  For this reason a simpset contains two solvers: safe and unsafe.
+
+  The standard simplification strategy solely uses the unsafe solver,
+  which is appropriate in most cases.  For special applications where
+  the simplification process is not allowed to instantiate unknowns
+  within the goal, simplification starts with the safe solver, but may
+  still apply the ordinary unsafe one in nested simplifications for
+  conditional rules or congruences. Note that in this way the overall
+  tactic is not totally safe: it may instantiate unknowns that appear
+  also in other subgoals.
+
+  \begin{description}
+
+  \item @{ML Simplifier.mk_solver}~@{text "name tac"} turns @{text
+  "tac"} into a solver; the @{text "name"} is only attached as a
+  comment and has no further significance.
+
+  \item @{text "ss setSSolver solver"} installs @{text "solver"} as
+  the safe solver of @{text "ss"}.
+
+  \item @{text "ss addSSolver solver"} adds @{text "solver"} as an
+  additional safe solver; it will be tried after the solvers which had
+  already been present in @{text "ss"}.
+
+  \item @{text "ss setSolver solver"} installs @{text "solver"} as the
+  unsafe solver of @{text "ss"}.
+
+  \item @{text "ss addSolver solver"} adds @{text "solver"} as an
+  additional unsafe solver; it will be tried after the solvers which
+  had already been present in @{text "ss"}.
+
+  \end{description}
+
+  \medskip The solver tactic is invoked with a simpset that represents
+  the context of the running Simplifier.  Further simpset operations
+  may be used to retrieve relevant information, such as the list of
+  local Simplifier premises via @{ML Simplifier.prems_of} --- this
+  list may be non-empty only if the Simplifier runs in a mode that
+  utilizes local assumptions (see also \secref{sec:simp-meth}).  The
+  solver is also presented the full goal including its assumptions in
+  any case.  Thus it can use these (e.g.\ by calling @{ML
+  assume_tac}), even if the Simplifier proper happens to ignore local
+  premises at the moment.
+
+  \medskip As explained before, the subgoaler is also used to solve
+  the premises of congruence rules.  These are usually of the form
+  @{text "s = ?x"}, where @{text "s"} needs to be simplified and
+  @{text "?x"} needs to be instantiated with the result.  Typically,
+  the subgoaler will invoke the Simplifier at some point, which will
+  eventually call the solver.  For this reason, solver tactics must be
+  prepared to solve goals of the form @{text "t = ?x"}, usually by
+  reflexivity.  In particular, reflexivity should be tried before any
+  of the fancy automated proof tools.
+
+  It may even happen that due to simplification the subgoal is no
+  longer an equality.  For example, @{text "False \<longleftrightarrow> ?Q"} could be
+  rewritten to @{text "\<not> ?Q"}.  To cover this case, the solver could
+  try resolving with the theorem @{text "\<not> False"} of the
+  object-logic.
+
+  \medskip
+
+  \begin{warn}
+  If a premise of a congruence rule cannot be proved, then the
+  congruence is ignored.  This should only happen if the rule is
+  \emph{conditional} --- that is, contains premises not of the form
+  @{text "t = ?x"}.  Otherwise it indicates that some congruence rule,
+  or possibly the subgoaler or solver, is faulty.
+  \end{warn}
+*}
+
+
+subsubsection {* The looper *}
+
+text {*
+  \begin{mldecls}
+  @{index_ML_op setloop: "simpset * (int -> tactic) -> simpset"} \\
+  @{index_ML_op setloop': "simpset * (simpset -> int -> tactic) -> simpset"} \\
+  @{index_ML_op addloop: "simpset * (string * (int -> tactic)) -> simpset"} \\
+  @{index_ML_op addloop': "simpset * (string * (simpset -> int -> tactic))
+  -> simpset"} \\
+  @{index_ML_op delloop: "simpset * string -> simpset"} \\
+  @{index_ML_op Splitter.add_split: "thm -> simpset -> simpset"} \\
+  @{index_ML_op Splitter.del_split: "thm -> simpset -> simpset"} \\
+  \end{mldecls}
+
+  The looper is a list of tactics that are applied after
+  simplification, in case the solver failed to solve the simplified
+  goal.  If the looper succeeds, the simplification process is started
+  all over again.  Each of the subgoals generated by the looper is
+  attacked in turn, in reverse order.
+
+  A typical looper is \emph{case splitting}: the expansion of a
+  conditional.  Another possibility is to apply an elimination rule on
+  the assumptions.  More adventurous loopers could start an induction.
+
+  \begin{description}
+
+  \item @{text "ss setloop tac"} installs @{text "tac"} as the only
+  looper tactic of @{text "ss"}.  The variant @{text "setloop'"}
+  allows the tactic to depend on the running Simplifier context, which
+  is represented as simpset.
+
+  \item @{text "ss addloop (name, tac)"} adds @{text "tac"} as an
+  additional looper tactic with name @{text "name"}, which is
+  significant for managing the collection of loopers.  The tactic will
+  be tried after the looper tactics that had already been present in
+  @{text "ss"}.  The variant @{text "addloop'"} allows the tactic to
+  depend on the running Simplifier context, which is represented as
+  simpset.
+
+  \item @{text "ss delloop name"} deletes the looper tactic that was
+  associated with @{text "name"} from @{text "ss"}.
+
+  \item @{ML Splitter.add_split}~@{text "thm ss"} adds split tactics
+  for @{text "thm"} as additional looper tactics of @{text "ss"}.
+
+  \item @{ML Splitter.del_split}~@{text "thm ss"} deletes the split
+  tactic corresponding to @{text thm} from the looper tactics of
+  @{text "ss"}.
+
+  \end{description}
+
+  The splitter replaces applications of a given function; the
+  right-hand side of the replacement can be anything.  For example,
+  here is a splitting rule for conditional expressions:
+
+  @{text [display] "?P (if ?Q ?x ?y) \<longleftrightarrow> (?Q \<longrightarrow> ?P ?x) \<and> (\<not> ?Q \<longrightarrow> ?P ?y)"}
+
+  Another example is the elimination operator for Cartesian products
+  (which happens to be called @{text split} in Isabelle/HOL:
+
+  @{text [display] "?P (split ?f ?p) \<longleftrightarrow> (\<forall>a b. ?p = (a, b) \<longrightarrow> ?P (f a b))"}
+
+  For technical reasons, there is a distinction between case splitting
+  in the conclusion and in the premises of a subgoal.  The former is
+  done by @{ML Splitter.split_tac} with rules like @{thm [source]
+  split_if} or @{thm [source] option.split}, which do not split the
+  subgoal, while the latter is done by @{ML Splitter.split_asm_tac}
+  with rules like @{thm [source] split_if_asm} or @{thm [source]
+  option.split_asm}, which split the subgoal.  The function @{ML
+  Splitter.add_split} automatically takes care of which tactic to
+  call, analyzing the form of the rules given as argument; it is the
+  same operation behind @{text "split"} attribute or method modifier
+  syntax in the Isar source language.
+
+  Case splits should be allowed only when necessary; they are
+  expensive and hard to control.  Case-splitting on if-expressions in
+  the conclusion is usually beneficial, so it is enabled by default in
+  Isabelle/HOL and Isabelle/FOL/ZF.
+
+  \begin{warn}
+  With @{ML Splitter.split_asm_tac} as looper component, the
+  Simplifier may split subgoals!  This might cause unexpected problems
+  in tactic expressions that silently assume 0 or 1 subgoals after
+  simplification.
+  \end{warn}
+*}
+
+
 subsection {* Forward simplification \label{sec:simp-forward} *}
 
 text {*
@@ -907,9 +1154,9 @@
 
   Note that forward simplification restricts the simplifier to its
   most basic operation of term rewriting; solver and looper tactics
-  \cite{isabelle-ref} are \emph{not} involved here.  The @{attribute
-  simplified} attribute should be only rarely required under normal
-  circumstances.
+  (\secref{sec:simp-strategies}) are \emph{not} involved here.  The
+  @{attribute simplified} attribute should be only rarely required
+  under normal circumstances.
 
   \end{description}
 *}
diff -r 02aa7f6e530d -r 5c36db9db335 src/Doc/Ref/document/simplifier.tex
--- a/src/Doc/Ref/document/simplifier.tex	Thu Nov 08 20:25:48 2012 +0100
+++ b/src/Doc/Ref/document/simplifier.tex	Sat Nov 10 20:16:16 2012 +0100
@@ -2,219 +2,6 @@
 \chapter{Simplification}
 \label{chap:simplification}
 
-\section{Configurable Simplifier components}
-
-\subsection{*The subgoaler}\label{sec:simp-subgoaler}
-\begin{ttbox}
-setsubgoaler :
-  simpset *  (simpset -> int -> tactic) -> simpset \hfill{\bf infix 4}
-prems_of_ss  : simpset -> thm list
-\end{ttbox}
-
-The subgoaler is the tactic used to solve subgoals arising out of
-conditional rewrite rules or congruence rules.  The default should be
-simplification itself.  Occasionally this strategy needs to be
-changed.  For example, if the premise of a conditional rule is an
-instance of its conclusion, as in $Suc(\Var{m}) < \Var{n} \Imp \Var{m}
-< \Var{n}$, the default strategy could loop.
-
-\begin{ttdescription}
-  
-\item[$ss$ \ttindexbold{setsubgoaler} $tacf$] sets the subgoaler of
-  $ss$ to $tacf$.  The function $tacf$ will be applied to the current
-  simplifier context expressed as a simpset.
-  
-\item[\ttindexbold{prems_of_ss} $ss$] retrieves the current set of
-  premises from simplifier context $ss$.  This may be non-empty only
-  if the simplifier has been told to utilize local assumptions in the
-  first place, e.g.\ if invoked via \texttt{asm_simp_tac}.
-
-\end{ttdescription}
-
-As an example, consider the following subgoaler:
-\begin{ttbox}
-fun subgoaler ss =
-    assume_tac ORELSE'
-    resolve_tac (prems_of_ss ss) ORELSE'
-    asm_simp_tac ss;
-\end{ttbox}
-This tactic first tries to solve the subgoal by assumption or by
-resolving with with one of the premises, calling simplification only
-if that fails.
-
-
-\subsection{*The solver}\label{sec:simp-solver}
-\begin{ttbox}
-mk_solver  : string -> (thm list -> int -> tactic) -> solver
-setSolver  : simpset * solver -> simpset \hfill{\bf infix 4}
-addSolver  : simpset * solver -> simpset \hfill{\bf infix 4}
-setSSolver : simpset * solver -> simpset \hfill{\bf infix 4}
-addSSolver : simpset * solver -> simpset \hfill{\bf infix 4}
-\end{ttbox}
-
-A solver is a tactic that attempts to solve a subgoal after
-simplification.  Typically it just proves trivial subgoals such as
-\texttt{True} and $t=t$.  It could use sophisticated means such as {\tt
-  blast_tac}, though that could make simplification expensive.
-To keep things more abstract, solvers are packaged up in type
-\texttt{solver}. The only way to create a solver is via \texttt{mk_solver}.
-
-Rewriting does not instantiate unknowns.  For example, rewriting
-cannot prove $a\in \Var{A}$ since this requires
-instantiating~$\Var{A}$.  The solver, however, is an arbitrary tactic
-and may instantiate unknowns as it pleases.  This is the only way the
-simplifier can handle a conditional rewrite rule whose condition
-contains extra variables.  When a simplification tactic is to be
-combined with other provers, especially with the classical reasoner,
-it is important whether it can be considered safe or not.  For this
-reason a simpset contains two solvers, a safe and an unsafe one.
-
-The standard simplification strategy solely uses the unsafe solver,
-which is appropriate in most cases.  For special applications where
-the simplification process is not allowed to instantiate unknowns
-within the goal, simplification starts with the safe solver, but may
-still apply the ordinary unsafe one in nested simplifications for
-conditional rules or congruences. Note that in this way the overall
-tactic is not totally safe:  it may instantiate unknowns that appear also 
-in other subgoals.
-
-\begin{ttdescription}
-\item[\ttindexbold{mk_solver} $s$ $tacf$] converts $tacf$ into a new solver;
-  the string $s$ is only attached as a comment and has no other significance.
-
-\item[$ss$ \ttindexbold{setSSolver} $tacf$] installs $tacf$ as the
-  \emph{safe} solver of $ss$.
-  
-\item[$ss$ \ttindexbold{addSSolver} $tacf$] adds $tacf$ as an
-  additional \emph{safe} solver; it will be tried after the solvers
-  which had already been present in $ss$.
-  
-\item[$ss$ \ttindexbold{setSolver} $tacf$] installs $tacf$ as the
-  unsafe solver of $ss$.
-  
-\item[$ss$ \ttindexbold{addSolver} $tacf$] adds $tacf$ as an
-  additional unsafe solver; it will be tried after the solvers which
-  had already been present in $ss$.
-
-\end{ttdescription}
-
-\medskip
-
-\index{assumptions!in simplification} The solver tactic is invoked
-with a list of theorems, namely assumptions that hold in the local
-context.  This may be non-empty only if the simplifier has been told
-to utilize local assumptions in the first place, e.g.\ if invoked via
-\texttt{asm_simp_tac}.  The solver is also presented the full goal
-including its assumptions in any case.  Thus it can use these (e.g.\ 
-by calling \texttt{assume_tac}), even if the list of premises is not
-passed.
-
-\medskip
-
-As explained in {\S}\ref{sec:simp-subgoaler}, the subgoaler is also used
-to solve the premises of congruence rules.  These are usually of the
-form $s = \Var{x}$, where $s$ needs to be simplified and $\Var{x}$
-needs to be instantiated with the result.  Typically, the subgoaler
-will invoke the simplifier at some point, which will eventually call
-the solver.  For this reason, solver tactics must be prepared to solve
-goals of the form $t = \Var{x}$, usually by reflexivity.  In
-particular, reflexivity should be tried before any of the fancy
-tactics like \texttt{blast_tac}.
-
-It may even happen that due to simplification the subgoal is no longer
-an equality.  For example $False \bimp \Var{Q}$ could be rewritten to
-$\neg\Var{Q}$.  To cover this case, the solver could try resolving
-with the theorem $\neg False$.
-
-\medskip
-
-\begin{warn}
-  If a premise of a congruence rule cannot be proved, then the
-  congruence is ignored.  This should only happen if the rule is
-  \emph{conditional} --- that is, contains premises not of the form $t
-  = \Var{x}$; otherwise it indicates that some congruence rule, or
-  possibly the subgoaler or solver, is faulty.
-\end{warn}
-
-
-\subsection{*The looper}\label{sec:simp-looper}
-\begin{ttbox}
-setloop   : simpset *           (int -> tactic)  -> simpset \hfill{\bf infix 4}
-addloop   : simpset * (string * (int -> tactic)) -> simpset \hfill{\bf infix 4}
-delloop   : simpset *  string                    -> simpset \hfill{\bf infix 4}
-addsplits : simpset * thm list -> simpset \hfill{\bf infix 4}
-delsplits : simpset * thm list -> simpset \hfill{\bf infix 4}
-\end{ttbox}
-
-The looper is a list of tactics that are applied after simplification, in case
-the solver failed to solve the simplified goal.  If the looper
-succeeds, the simplification process is started all over again.  Each
-of the subgoals generated by the looper is attacked in turn, in
-reverse order.
-
-A typical looper is \index{case splitting}: the expansion of a conditional.
-Another possibility is to apply an elimination rule on the
-assumptions.  More adventurous loopers could start an induction.
-
-\begin{ttdescription}
-  
-\item[$ss$ \ttindexbold{setloop} $tacf$] installs $tacf$ as the only looper
-  tactic of $ss$.
-  
-\item[$ss$ \ttindexbold{addloop} $(name,tacf)$] adds $tacf$ as an additional
-  looper tactic with name $name$; it will be tried after the looper tactics
-  that had already been present in $ss$.
-  
-\item[$ss$ \ttindexbold{delloop} $name$] deletes the looper tactic $name$
-  from $ss$.
-  
-\item[$ss$ \ttindexbold{addsplits} $thms$] adds
-  split tactics for $thms$ as additional looper tactics of $ss$.
-
-\item[$ss$ \ttindexbold{addsplits} $thms$] deletes the
-  split tactics for $thms$ from the looper tactics of $ss$.
-
-\end{ttdescription}
-
-The splitter replaces applications of a given function; the right-hand side
-of the replacement can be anything.  For example, here is a splitting rule
-for conditional expressions:
-\[ \Var{P}(if(\Var{Q},\Var{x},\Var{y})) \bimp (\Var{Q} \imp \Var{P}(\Var{x}))
-\conj (\neg\Var{Q} \imp \Var{P}(\Var{y})) 
-\] 
-Another example is the elimination operator for Cartesian products (which
-happens to be called~$split$):  
-\[ \Var{P}(split(\Var{f},\Var{p})) \bimp (\forall a~b. \Var{p} =
-\langle a,b\rangle \imp \Var{P}(\Var{f}(a,b))) 
-\] 
-
-For technical reasons, there is a distinction between case splitting in the 
-conclusion and in the premises of a subgoal. The former is done by
-\texttt{split_tac} with rules like \texttt{split_if} or \texttt{option.split}, 
-which do not split the subgoal, while the latter is done by 
-\texttt{split_asm_tac} with rules like \texttt{split_if_asm} or 
-\texttt{option.split_asm}, which split the subgoal.
-The operator \texttt{addsplits} automatically takes care of which tactic to
-call, analyzing the form of the rules given as argument.
-\begin{warn}
-Due to \texttt{split_asm_tac}, the simplifier may split subgoals!
-\end{warn}
-
-Case splits should be allowed only when necessary; they are expensive
-and hard to control.  Here is an example of use, where \texttt{split_if}
-is the first rule above:
-\begin{ttbox}
-by (simp_tac (simpset() 
-                 addloop ("split if", split_tac [split_if])) 1);
-\end{ttbox}
-Users would usually prefer the following shortcut using \texttt{addsplits}:
-\begin{ttbox}
-by (simp_tac (simpset() addsplits [split_if]) 1);
-\end{ttbox}
-Case-splitting on conditional expressions is usually beneficial, so it is
-enabled by default in the object-logics \texttt{HOL} and \texttt{FOL}.
-
-
 \section{Permutative rewrite rules}
 \index{rewrite rules!permutative|(}