# 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 \<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 {*
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}