text‹\label{sec:simplification-II}\index{simplification|(}
section describes features not covered until now. It also
the simplification process itself, which can be helpful
the simplifier does not do what you expect of it. ›
subsection‹Advanced Features›
subsubsection‹Congruence Rules›
text‹\label{sec:simp-cong}
simplifying the conclusion $Q$
$P \Imp Q$, it is legal to use the assumption $P$.
$\Imp$ this policy is hardwired, but
information can also be made available for other
. For example, prop‹xs = [] --> xs@xs = xs› simplifies to term‹True› because we may use prop‹xs = []› when simplifying prop‹xs@xs = ›. The generation of contextual information during simplification is
by so-called \bfindex{congruence rules}. This is the one for ‹⟶›:
{thm[display]imp_cong[no_vars]}
should be read as follows:
order to simplify prop‹P-->Q› to prop‹P'-->Q'›, prop‹P› to prop‹P'›
assume prop‹P'› when simplifying prop‹Q› to prop‹Q'›.
are some more examples. The congruence rules for bounded
supply contextual information about the bound variable:
{thm[display,eta_contract=false,margin=60]ball_cong[no_vars]}
congruence rule for conditional expressions supplies contextual
for simplifying the ‹then› and ‹else› cases:
{thm[display]if_cong[no_vars]}
alternative congruence rule for conditional expressions \emph{prevents} simplification of some arguments:
{thm[display]if_weak_cong[no_vars]}
the first argument is simplified; the others remain unchanged.
makes simplification much faster and is faithful to the evaluation
in programming languages, which is why this is the default
rule for ‹if›. Analogous rules control the evaluation of ‹case› expressions.
can declare your own congruence rules with the attribute \attrdx{cong},
globally, in the usual manner,
begin{quote}
isacommand{declare} \textit{theorem-name} ‹[cong]›
end{quote}
locally in a ‹simp› call by adding the modifier
begin{quote} ‹cong:›\textit{list of theorem names}
end{quote}
effect is reversed by ‹cong del› instead of ‹cong›.
begin{warn}
congruence rule @{thm[source]conj_cong}
{thm[display]conj_cong[no_vars]}
par\noindent
occasionally useful but is not a default rule; you have to declare it explicitly.
end{warn} ›
subsubsection‹Permutative Rewrite Rules›
text‹
index{rewrite rules!permutative|bold}%
equation is a \textbf{permutative rewrite rule} if the left-hand
and right-hand side are the same up to renaming of variables. The most
permutative rule is commutativity: prop‹x+y = y+x›. Other examples prop‹(x-y)-z = (x-z)-y› in arithmetic and prop‹insert x (insert
A) = insert y (insert x A)› for sets. Such rules are problematic because
they apply, they can be used forever. The simplifier is aware of this
and treats permutative rules by means of a special strategy, called
bfindex{ordered rewriting}: a permutative rewrite
is only applied if the term becomes smaller with respect to a fixed
ordering on terms. For example, commutativity rewrites term‹b+a› to term‹a+b›, but then stops because term‹a+b› is strictly
than term‹b+a›. Permutative rewrite rules can be turned into
rules in the usual manner via the ‹simp› attribute; the
recognizes their special status automatically.
rewrite rules are most effective in the case of
-commutative functions. (Associativity by itself is not
.) When dealing with an AC-function~$f$, keep the
points in mind:
begin{itemize}\index{associative-commutative function}
item The associative law must always be oriented from left to right,
namely $f(f(x,y),z) = f(x,f(y,z))$. The opposite orientation, if
used with commutativity, can lead to nontermination.
item To complete your set of rewrite rules, you must add not just
associativity~(A) and commutativity~(C) but also a derived rule, {\bf
left-com\-mut\-ativ\-ity} (LC): $f(x,f(y,z)) = f(y,f(x,z))$.
end{itemize}
rewriting with the combination of A, C, and LC sorts a term
:
[\def\maps#1{~\stackrel{#1}{\leadsto}~}
f(f(b,c),a) \maps{A} f(b,f(c,a)) \maps{C} f(b,f(a,c)) \maps{LC} f(a,f(b,c)) \]
that ordered rewriting for ‹+› and ‹*› on numbers is rarely
because the built-in arithmetic prover often succeeds without
tricks. ›
subsection‹How the Simplifier Works›
text‹\label{sec:SimpHow}
speaking, the simplifier proceeds bottom-up: subterms are simplified
. A conditional equation is only applied if its condition can be
, again by simplification. Below we explain some special features of
rewriting process. ›
subsubsection‹Higher-Order Patterns›
text‹\index{simplification rule|(}
far we have pretended the simplifier can deal with arbitrary
rules. This is not quite true. For reasons of feasibility,
simplifier expects the
-hand side of each rule to be a so-called \emph{higher-order
}~cite‹"nipkow-patterns"›\indexbold{patterns!higher-order}.
restricts where
may occur. Higher-order patterns are terms in $\beta$-normal
. (This means there are no subterms of the form $(\lambda x. M)(N)$.)
occurrence of an unknown is of the form \Var{f}~x@1~\dots~x@n$, where the $x@i$ are distinct bound
. Thus all ordinary rewrite rules, where all unknowns are
base type, for example @{thm add.assoc}, are acceptable: if an unknown is
base type, it cannot have any arguments. Additionally, the rule ‹(∀x. ?P x ∧ ?Q x) = ((∀x. ?P x) ∧ (∀x. ?Q x))› is also acceptable, in
directions: all arguments of the unknowns ‹?P› and ‹?Q› are distinct bound variables.
the left-hand side is not a higher-order pattern, all is not lost.
simplifier will still try to apply the rule provided it
directly: without much $\lambda$-calculus hocus
. For example, ‹(?f ?x ∈ range ?f) = True› rewrites term‹g a ∈ range g› to const‹True›, but will fail to match ‹g(h b) ∈ range(λx. g(h x))›. However, you can
the offending subterms --- those that are not patterns ---
adding new variables and conditions.
our example, we eliminate ‹?f ?x› and obtain ‹?y =
f ?x ==> (?y ∈ range ?f) = True›, which is fine
a conditional rewrite rule since conditions can be arbitrary
. However, this trick is not a panacea because the newly
conditions may be hard to solve.
is no restriction on the form of the right-hand
. They may not contain extraneous term or type variables, though. ›
subsubsection‹The Preprocessor›
text‹\label{sec:simp-preprocessor}
a theorem is declared a simplification rule, it need not be a
equation already. The simplifier will turn it into a set of
equations automatically. For example, prop‹f x =
x & h x = k x› becomes the two separate
rules prop‹f x = g x› and prop‹h x = k x›. In
, the input theorem is converted as follows:
begin{eqnarray}
neg P &\mapsto& P = \hbox{\isa{False}} \nonumber\\ \longrightarrow Q &\mapsto& P \Longrightarrow Q \nonumber\\ \land Q &\mapsto& P,\ Q \nonumber\\
forall x.~P~x &\mapsto& P~\Var{x}\nonumber\\
forall x \in A.\ P~x &\mapsto& \Var{x} \in A \Longrightarrow P~\Var{x} \nonumber\\ ‹if›\ P\ ‹then›\ Q\ ‹else›\ R &\mapsto&
P \Longrightarrow Q,\ \neg P \Longrightarrow R \nonumber
end{eqnarray}
this conversion process is finished, all remaining non-equations
P$ are turned into trivial equations $P =\isa{True}$.
example, the formula
begin{center}prop‹(p ⟶ t=u ∧ ~r) ∧ s›\end{center}
converted into the three rules
begin{center} prop‹p ==> t = u›,\quadprop‹p ==> r = False›,\quadprop‹s = True›.
end{center}
index{simplification rule|)}
index{simplification|)} › (*<*) end (*>*)
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
