# HG changeset patch
# User wenzelm
# Date 1352402314 -3600
# Node ID c5cc24781cbf44bbe669b2f265e8b234c9b44898
# Parent  ceb877c315a1e19ef7500433845068c7f3b7da88
updated explanation of rewrite rules;

diff -r ceb877c315a1 -r c5cc24781cbf src/Doc/IsarRef/Generic.thy
--- 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.
 
diff -r ceb877c315a1 -r c5cc24781cbf src/Doc/Ref/document/simplifier.tex
--- 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 :