--- 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 \<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}, bypassing the
+ automatic preprocessing of object-level equivalences.
+
\begin{matharray}{rcl}
@{command_def "simproc_setup"} & : & @{text "local_theory \<rightarrow> 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 {*
--- 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%
--- 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}