summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Thu, 08 Nov 2012 20:18:34 +0100 | |

changeset 50076 | c5cc24781cbf |

parent 50075 | ceb877c315a1 |

child 50077 | 1edd0db7b6c4 |

updated explanation of rewrite rules;

src/Doc/IsarRef/Generic.thy | file | annotate | diff | comparison | revisions | |

src/Doc/Ref/document/simplifier.tex | file | annotate | diff | comparison | revisions |

--- 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 :