|
9743
|
1 |
\chapter{The Tricks of the Trade}
|
|
|
2 |
|
|
|
3 |
\section{Simplification}
|
|
9754
|
4 |
\label{sec:simplification-II}
|
|
9743
|
5 |
\index{simplification|(}
|
|
|
6 |
|
|
|
7 |
\subsection{Advanced features}
|
|
|
8 |
|
|
|
9 |
\subsubsection{Congruence rules}
|
|
|
10 |
|
|
|
11 |
|
|
|
12 |
\subsubsection{Permutative rewrite rules}
|
|
|
13 |
|
|
|
14 |
A rewrite rule is \textbf{permutative} if the left-hand side and right-hand
|
|
|
15 |
side are the same up to renaming of variables. The most common permutative
|
|
|
16 |
rule is commutativity: $x+y = y+x$. Another example is $(x-y)-z = (x-z)-y$.
|
|
|
17 |
Such rules are problematic because once they apply, they can be used forever.
|
|
|
18 |
The simplifier is aware of this danger and treats permutative rules
|
|
|
19 |
separately. For details see~\cite{isabelle-ref}.
|
|
|
20 |
|
|
|
21 |
|
|
|
22 |
|
|
|
23 |
\subsection{How it works}
|
|
|
24 |
\label{sec:SimpHow}
|
|
|
25 |
|
|
|
26 |
\subsubsection{Higher-order patterns}
|
|
|
27 |
|
|
|
28 |
\subsubsection{Local assumptions}
|
|
|
29 |
|
|
|
30 |
\subsubsection{The preprocessor}
|
|
|
31 |
|
|
|
32 |
\index{simplification|)}
|
|
|
33 |
|
|
|
34 |
|
|
|
35 |
\section{Advanced induction techniques}
|
|
|
36 |
\label{sec:advanced-ind}
|
|
|
37 |
\input{Misc/document/AdvancedInd.tex}
|