changeset 50076 c5cc24781cbf
parent 50075 ceb877c315a1
child 50077 1edd0db7b6c4
--- 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.