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