--- a/src/Doc/IsarRef/Generic.thy Wed Nov 07 21:43:02 2012 +0100
+++ b/src/Doc/IsarRef/Generic.thy Thu Nov 08 20:18:34 2012 +0100
@@ -630,13 +630,65 @@
simpset and the context of the problem being simplified may lead to
unexpected results.
- \item @{attribute simp} declares simplification rules, by adding or
+ \item @{attribute simp} declares rewrite rules, by adding or
deleting them from the simpset within the theory or proof context.
+ Rewrite rules are theorems expressing some form of equality, for
+ example:
+
+ @{text "Suc ?m + ?n = ?m + Suc ?n"} \\
+ @{text "?P \<and> ?P \<longleftrightarrow> ?P"} \\
+ @{text "?A \<union> ?B \<equiv> {x. x \<in> ?A \<or> x \<in> ?B}"}
+
+ \smallskip
+ Conditional rewrites such as @{text "?m < ?n \<Longrightarrow> ?m div ?n = 0"} are
+ also permitted; the conditions can be arbitrary formulas.
+
+ \medskip Internally, all rewrite rules are translated into Pure
+ equalities, theorems with conclusion @{text "lhs \<equiv> rhs"}. The
+ simpset contains a function for extracting equalities from arbitrary
+ theorems, which is usually installed when the object-logic is
+ configured initially. For example, @{text "\<not> ?x \<in> {}"} could be
+ turned into @{text "?x \<in> {} \<equiv> False"}. Theorems that are declared as
+ @{attribute simp} and local assumptions within a goal are treated
+ uniformly in this respect.
+
+ The Simplifier accepts the following formats for the @{text "lhs"}
+ term:
+
+ \begin{enumerate}
- Internally, all rewrite rules have to be expressed as Pure
- equalities, potentially with some conditions of arbitrary form.
- Such rewrite rules in Pure are derived automatically from
- object-level equations that are supplied by the user.
+ \item First-order patterns, considering the sublanguage of
+ application of constant operators to variable operands, without
+ @{text "\<lambda>"}-abstractions or functional variables.
+ For example:
+
+ @{text "(?x + ?y) + ?z \<equiv> ?x + (?y + ?z)"} \\
+ @{text "f (f ?x ?y) ?z \<equiv> f ?x (f ?y ?z)"}
+
+ \item Higher-order patterns in the sense of \cite{nipkow-patterns}.
+ These are terms in @{text "\<beta>"}-normal form (this will always be the
+ case unless you have done something strange) where each occurrence
+ of an unknown is of the form @{text "?F x\<^sub>1 \<dots> x\<^sub>n"}, where the
+ @{text "x\<^sub>i"} are distinct bound variables.
+
+ For example, @{text "(\<forall>x. ?P x \<and> ?Q x) \<equiv> (\<forall>x. ?P x) \<and> (\<forall>x. ?Q x)"}
+ or its symmetric form, since the @{text "rhs"} is also a
+ higher-order pattern.
+
+ \item Physical first-order patterns over raw @{text "\<lambda>"}-term
+ structure without @{text "\<alpha>\<beta>\<eta>"}-equality; abstractions and bound
+ variables are treated like quasi-constant term material.
+
+ For example, the rule @{text "?f ?x \<in> range ?f = True"} rewrites the
+ term @{text "g a \<in> range g"} to @{text "True"}, but will fail to
+ match @{text "g (h b) \<in> range (\<lambda>x. g (h x))"}. However, offending
+ subterms (in our case @{text "?f ?x"}, which is not a pattern) can
+ be replaced by adding new variables and conditions like this: @{text
+ "?y = ?f ?x \<Longrightarrow> ?y \<in> range ?f = True"} is acceptable as a conditional
+ rewrite rule of the second category since conditions can be
+ arbitrary terms.
+
+ \end{enumerate}
\item @{attribute split} declares case split rules.
--- a/src/Doc/Ref/document/simplifier.tex Wed Nov 07 21:43:02 2012 +0100
+++ b/src/Doc/Ref/document/simplifier.tex Thu Nov 08 20:18:34 2012 +0100
@@ -4,73 +4,6 @@
\section{Simplification sets}\index{simplification sets}
-\subsection{Rewrite rules}
-\begin{ttbox}
-addsimps : simpset * thm list -> simpset \hfill{\bf infix 4}
-delsimps : simpset * thm list -> simpset \hfill{\bf infix 4}
-\end{ttbox}
-
-\index{rewrite rules|(} Rewrite rules are theorems expressing some
-form of equality, for example:
-\begin{eqnarray*}
- Suc(\Var{m}) + \Var{n} &=& \Var{m} + Suc(\Var{n}) \\
- \Var{P}\conj\Var{P} &\bimp& \Var{P} \\
- \Var{A} \un \Var{B} &\equiv& \{x.x\in \Var{A} \disj x\in \Var{B}\}
-\end{eqnarray*}
-Conditional rewrites such as $\Var{m}<\Var{n} \Imp \Var{m}/\Var{n} =
-0$ are also permitted; the conditions can be arbitrary formulas.
-
-Internally, all rewrite rules are translated into meta-equalities,
-theorems with conclusion $lhs \equiv rhs$. Each simpset contains a
-function for extracting equalities from arbitrary theorems. For
-example, $\neg(\Var{x}\in \{\})$ could be turned into $\Var{x}\in \{\}
-\equiv False$. This function can be installed using
-\ttindex{setmksimps} but only the definer of a logic should need to do
-this; see {\S}\ref{sec:setmksimps}. The function processes theorems
-added by \texttt{addsimps} as well as local assumptions.
-
-\begin{ttdescription}
-
-\item[$ss$ \ttindexbold{addsimps} $thms$] adds rewrite rules derived
- from $thms$ to the simpset $ss$.
-
-\item[$ss$ \ttindexbold{delsimps} $thms$] deletes rewrite rules
- derived from $thms$ from the simpset $ss$.
-
-\end{ttdescription}
-
-\begin{warn}
- The simplifier will accept all standard rewrite rules: those where
- all unknowns are of base type. Hence ${\Var{i}+(\Var{j}+\Var{k})} =
- {(\Var{i}+\Var{j})+\Var{k}}$ is OK.
-
- It will also deal gracefully with all rules whose left-hand sides
- are so-called {\em higher-order patterns}~\cite{nipkow-patterns}.
- \indexbold{higher-order pattern}\indexbold{pattern, higher-order}
- These are terms in $\beta$-normal form (this will always be the case
- unless you have done something strange) where each occurrence of an
- unknown is of the form $\Var{F}(x@1,\dots,x@n)$, where the $x@i$ are
- distinct bound variables. Hence $(\forall x.\Var{P}(x) \land
- \Var{Q}(x)) \bimp (\forall x.\Var{P}(x)) \land (\forall
- x.\Var{Q}(x))$ is also OK, in both directions.
-
- In some rare cases the rewriter will even deal with quite general
- rules: for example ${\Var{f}(\Var{x})\in range(\Var{f})} = True$
- rewrites $g(a) \in range(g)$ to $True$, but will fail to match
- $g(h(b)) \in range(\lambda x.g(h(x)))$. However, you can replace
- the offending subterms (in our case $\Var{f}(\Var{x})$, which is not
- a pattern) by adding new variables and conditions: $\Var{y} =
- \Var{f}(\Var{x}) \Imp \Var{y}\in range(\Var{f}) = True$ is
- acceptable as a conditional rewrite rule since conditions can be
- arbitrary terms.
-
- There is basically no restriction on the form of the right-hand
- sides. They may not contain extraneous term or type variables,
- though.
-\end{warn}
-\index{rewrite rules|)}
-
-
\subsection{*The subgoaler}\label{sec:simp-subgoaler}
\begin{ttbox}
setsubgoaler :