--- 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}
*}