summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Sat, 10 Nov 2012 20:16:16 +0100 | |

changeset 50079 | 5c36db9db335 |

parent 50078 | 02aa7f6e530d |

child 50080 | 200f749c96db |

updated subgoaler/solver/looper;

src/Doc/IsarRef/Generic.thy | file | annotate | diff | comparison | revisions | |

src/Doc/Ref/document/simplifier.tex | file | annotate | diff | comparison | revisions |

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