# HG changeset patch # User wenzelm # Date 1307133563 -7200 # Node ID c6c4f997ad876fc965f3b1161ca2baaf63ac99eb # Parent bd8d78745a7df25694ded67481f04172141b62d0 updated and re-unified material on simprocs; diff -r bd8d78745a7d -r c6c4f997ad87 doc-src/IsarRef/Thy/Generic.thy --- a/doc-src/IsarRef/Thy/Generic.thy Fri Jun 03 21:32:48 2011 +0200 +++ b/doc-src/IsarRef/Thy/Generic.thy Fri Jun 03 22:39:23 2011 +0200 @@ -468,7 +468,22 @@ subsection {* Simplification procedures *} -text {* +text {* Simplification procedures are ML functions that produce proven + rewrite rules on demand. They are associated with higher-order + patterns that approximate the left-hand sides of equations. The + Simplifier first matches the current redex against one of the LHS + patterns; if this succeeds, the corresponding ML function is + invoked, passing the Simplifier context and redex term. Thus rules + may be specifically fashioned for particular situations, resulting + in a more powerful mechanism than term rewriting by a fixed set of + rules. + + Any successful result needs to be a (possibly conditional) rewrite + rule @{text "t \ u"} that is applicable to the current redex. The + rule will be applied just as any ordinary rewrite rule. It is + expected to be already in \emph{internal form}, bypassing the + automatic preprocessing of object-level equivalences. + \begin{matharray}{rcl} @{command_def "simproc_setup"} & : & @{text "local_theory \ local_theory"} \\ simproc & : & @{text attribute} \\ @@ -512,6 +527,26 @@ *} +subsubsection {* Example *} + +text {* The following simplification procedure for @{thm + [source=false, show_types] unit_eq} in HOL performs fine-grained + control over rule application, beyond higher-order pattern matching. + Declaring @{thm unit_eq} as @{attribute simp} directly would make + the simplifier loop! Note that a version of this simplification + procedure is already active in Isabelle/HOL. *} + +simproc_setup unit ("x::unit") = {* + fn _ => fn _ => fn ct => + if HOLogic.is_unit (term_of ct) then NONE + else SOME (mk_meta_eq @{thm unit_eq}) +*} + +text {* Since the Simplifier applies simplification procedures + frequently, it is important to make the failure check in ML + reasonably fast. *} + + subsection {* Forward simplification *} text {* diff -r bd8d78745a7d -r c6c4f997ad87 doc-src/IsarRef/Thy/document/Generic.tex --- a/doc-src/IsarRef/Thy/document/Generic.tex Fri Jun 03 21:32:48 2011 +0200 +++ b/doc-src/IsarRef/Thy/document/Generic.tex Fri Jun 03 22:39:23 2011 +0200 @@ -734,7 +734,23 @@ \isamarkuptrue% % \begin{isamarkuptext}% -\begin{matharray}{rcl} +Simplification procedures are ML functions that produce proven + rewrite rules on demand. They are associated with higher-order + patterns that approximate the left-hand sides of equations. The + Simplifier first matches the current redex against one of the LHS + patterns; if this succeeds, the corresponding ML function is + invoked, passing the Simplifier context and redex term. Thus rules + may be specifically fashioned for particular situations, resulting + in a more powerful mechanism than term rewriting by a fixed set of + rules. + + Any successful result needs to be a (possibly conditional) rewrite + rule \isa{{\isaliteral{22}{\isachardoublequote}}t\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ u{\isaliteral{22}{\isachardoublequote}}} that is applicable to the current redex. The + rule will be applied just as any ordinary rewrite rule. It is + expected to be already in \emph{internal form}, bypassing the + automatic preprocessing of object-level equivalences. + + \begin{matharray}{rcl} \indexdef{}{command}{simproc\_setup}\hypertarget{command.simproc-setup}{\hyperlink{command.simproc-setup}{\mbox{\isa{\isacommand{simproc{\isaliteral{5F}{\isacharunderscore}}setup}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\ simproc & : & \isa{attribute} \\ \end{matharray} @@ -810,6 +826,48 @@ \end{isamarkuptext}% \isamarkuptrue% % +\isamarkupsubsubsection{Example% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +The following simplification procedure for \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}u{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}unit{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{29}{\isacharparenright}}} in HOL performs fine-grained + control over rule application, beyond higher-order pattern matching. + Declaring \isa{unit{\isaliteral{5F}{\isacharunderscore}}eq} as \hyperlink{attribute.simp}{\mbox{\isa{simp}}} directly would make + the simplifier loop! Note that a version of this simplification + procedure is already active in Isabelle/HOL.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimML +% +\endisadelimML +% +\isatagML +\isacommand{simproc{\isaliteral{5F}{\isacharunderscore}}setup}\isamarkupfalse% +\ unit\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}x{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}unit{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline +\ \ fn\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ fn\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ fn\ ct\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\isanewline +\ \ \ \ if\ HOLogic{\isaliteral{2E}{\isachardot}}is{\isaliteral{5F}{\isacharunderscore}}unit\ {\isaliteral{28}{\isacharparenleft}}term{\isaliteral{5F}{\isacharunderscore}}of\ ct{\isaliteral{29}{\isacharparenright}}\ then\ NONE\isanewline +\ \ \ \ else\ SOME\ {\isaliteral{28}{\isacharparenleft}}mk{\isaliteral{5F}{\isacharunderscore}}meta{\isaliteral{5F}{\isacharunderscore}}eq\ % +\isaantiq +thm\ unit{\isaliteral{5F}{\isacharunderscore}}eq{}% +\endisaantiq +{\isaliteral{29}{\isacharparenright}}\isanewline +{\isaliteral{2A7D}{\isacharverbatimclose}}% +\endisatagML +{\isafoldML}% +% +\isadelimML +% +\endisadelimML +% +\begin{isamarkuptext}% +Since the Simplifier applies simplification procedures + frequently, it is important to make the failure check in ML + reasonably fast.% +\end{isamarkuptext}% +\isamarkuptrue% +% \isamarkupsubsection{Forward simplification% } \isamarkuptrue% diff -r bd8d78745a7d -r c6c4f997ad87 doc-src/Ref/simplifier.tex --- a/doc-src/Ref/simplifier.tex Fri Jun 03 21:32:48 2011 +0200 +++ b/doc-src/Ref/simplifier.tex Fri Jun 03 22:39:23 2011 +0200 @@ -336,47 +336,6 @@ \index{rewrite rules|)} -\subsection{*Simplification procedures} -\begin{ttbox} -addsimprocs : simpset * simproc list -> simpset -delsimprocs : simpset * simproc list -> simpset -\end{ttbox} - -Simplification procedures are {\ML} objects of abstract type -\texttt{simproc}. Basically they are just functions that may produce -\emph{proven} rewrite rules on demand. They are associated with -certain patterns that conceptually represent left-hand sides of -equations; these are shown by \texttt{print_ss}. During its -operation, the simplifier may offer a simplification procedure the -current redex and ask for a suitable rewrite rule. Thus rules may be -specifically fashioned for particular situations, resulting in a more -powerful mechanism than term rewriting by a fixed set of rules. - - -\begin{ttdescription} - -\item[$ss$ \ttindexbold{addsimprocs} $procs$] adds the simplification - procedures $procs$ to the current simpset. - -\item[$ss$ \ttindexbold{delsimprocs} $procs$] deletes the simplification - procedures $procs$ from the current simpset. - -\end{ttdescription} - -For example, simplification procedures \ttindexbold{nat_cancel} of -\texttt{HOL/Arith} cancel common summands and constant factors out of -several relations of sums over natural numbers. - -Consider the following goal, which after cancelling $a$ on both sides -contains a factor of $2$. Simplifying with the simpset of -\texttt{Arith.thy} will do the cancellation automatically: -\begin{ttbox} -{\out 1. x + a + x < y + y + 2 + a + a + a + a + a} -by (Simp_tac 1); -{\out 1. x < Suc (a + (a + y))} -\end{ttbox} - - \subsection{*Congruence rules}\index{congruence rules}\label{sec:simp-congs} \begin{ttbox} addcongs : simpset * thm list -> simpset \hfill{\bf infix 4} @@ -920,82 +879,6 @@ \index{rewrite rules!permutative|)} -\section{*Coding simplification procedures} -\begin{ttbox} - val Simplifier.simproc: Sign.sg -> string -> string list - -> (Sign.sg -> simpset -> term -> thm option) -> simproc - val Simplifier.simproc_i: Sign.sg -> string -> term list - -> (Sign.sg -> simpset -> term -> thm option) -> simproc -\end{ttbox} - -\begin{ttdescription} -\item[\ttindexbold{Simplifier.simproc}~$sign$~$name$~$lhss$~$proc$] makes - $proc$ a simplification procedure for left-hand side patterns $lhss$. The - name just serves as a comment. The function $proc$ may be invoked by the - simplifier for redex positions matched by one of $lhss$ as described below - (which are be specified as strings to be read as terms). - -\item[\ttindexbold{Simplifier.simproc_i}] is similar to - \verb,Simplifier.simproc,, but takes well-typed terms as pattern argument. -\end{ttdescription} - -Simplification procedures are applied in a two-stage process as -follows: The simplifier tries to match the current redex position -against any one of the $lhs$ patterns of any simplification procedure. -If this succeeds, it invokes the corresponding {\ML} function, passing -with the current signature, local assumptions and the (potential) -redex. The result may be either \texttt{None} (indicating failure) or -\texttt{Some~$thm$}. - -Any successful result is supposed to be a (possibly conditional) -rewrite rule $t \equiv u$ that is applicable to the current redex. -The rule will be applied just as any ordinary rewrite rule. It is -expected to be already in \emph{internal form}, though, bypassing the -automatic preprocessing of object-level equivalences. - -\medskip - -As an example of how to write your own simplification procedures, -consider eta-expansion of pair abstraction (see also -\texttt{HOL/Modelcheck/MCSyn} where this is used to provide external -model checker syntax). - -The HOL theory of tuples (see \texttt{HOL/Prod}) provides an operator -\texttt{split} together with some concrete syntax supporting -$\lambda\,(x,y).b$ abstractions. Assume that we would like to offer a tactic -that rewrites any function $\lambda\,p.f\,p$ (where $p$ is of some pair type) -to $\lambda\,(x,y).f\,(x,y)$. The corresponding rule is: -\begin{ttbox} -pair_eta_expand: (f::'a*'b=>'c) = (\%(x, y). f (x, y)) -\end{ttbox} -Unfortunately, term rewriting using this rule directly would not -terminate! We now use the simplification procedure mechanism in order -to stop the simplifier from applying this rule over and over again, -making it rewrite only actual abstractions. The simplification -procedure \texttt{pair_eta_expand_proc} is defined as follows: -\begin{ttbox} -val pair_eta_expand_proc = - Simplifier.simproc (Theory.sign_of (the_context ())) - "pair_eta_expand" ["f::'a*'b=>'c"] - (fn _ => fn _ => fn t => - case t of Abs _ => Some (mk_meta_eq pair_eta_expand) - | _ => None); -\end{ttbox} -This is an example of using \texttt{pair_eta_expand_proc}: -\begin{ttbox} -{\out 1. P (\%p::'a * 'a. fst p + snd p + z)} -by (simp_tac (simpset() addsimprocs [pair_eta_expand_proc]) 1); -{\out 1. P (\%(x::'a,y::'a). x + y + z)} -\end{ttbox} - -\medskip - -In the above example the simplification procedure just did fine -grained control over rule application, beyond higher-order pattern -matching. Usually, procedures would do some more work, in particular -prove particular theorems depending on the current redex. - - \section{*Setting up the Simplifier}\label{sec:setting-up-simp} \index{simplification!setting up}