9993
|
1 |
%
|
|
2 |
\begin{isabellebody}%
|
|
3 |
\def\isabellecontext{simp}%
|
|
4 |
%
|
|
5 |
\isamarkupsection{Simplification}
|
|
6 |
%
|
|
7 |
\begin{isamarkuptext}%
|
|
8 |
\label{sec:simplification-II}\index{simplification|(}
|
|
9 |
This section discusses some additional nifty features not covered so far and
|
|
10 |
gives a short introduction to the simplification process itself. The latter
|
|
11 |
is helpful to understand why a particular rule does or does not apply in some
|
|
12 |
situation.%
|
|
13 |
\end{isamarkuptext}%
|
|
14 |
%
|
|
15 |
\isamarkupsubsection{Advanced features}
|
|
16 |
%
|
|
17 |
\isamarkupsubsubsection{Congruence rules}
|
|
18 |
%
|
|
19 |
\begin{isamarkuptext}%
|
|
20 |
\label{sec:simp-cong}
|
|
21 |
It is hardwired into the simplifier that while simplifying the conclusion $Q$
|
|
22 |
of $P \isasymImp Q$ it is legal to make uses of the assumptions $P$. This
|
|
23 |
kind of contextual information can also be made available for other
|
|
24 |
operators. For example, \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongrightarrow}\ xs\ {\isacharat}\ xs\ {\isacharequal}\ xs} simplifies to \isa{True} because we may use \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} when simplifying \isa{xs\ {\isacharat}\ xs\ {\isacharequal}\ xs}. The generation of contextual information during simplification is
|
|
25 |
controlled by so-called \bfindex{congruence rules}. This is the one for
|
|
26 |
\isa{{\isasymlongrightarrow}}:
|
|
27 |
\begin{isabelle}%
|
|
28 |
\ \ \ \ \ {\isasymlbrakk}P\ {\isacharequal}\ P{\isacharprime}{\isacharsemicolon}\ P{\isacharprime}\ {\isasymLongrightarrow}\ Q\ {\isacharequal}\ Q{\isacharprime}{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}P\ {\isasymlongrightarrow}\ Q{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}P{\isacharprime}\ {\isasymlongrightarrow}\ Q{\isacharprime}{\isacharparenright}%
|
|
29 |
\end{isabelle}
|
|
30 |
It should be read as follows:
|
|
31 |
In order to simplify \isa{P\ {\isasymlongrightarrow}\ Q} to \isa{P{\isacharprime}\ {\isasymlongrightarrow}\ Q{\isacharprime}},
|
|
32 |
simplify \isa{P} to \isa{P{\isacharprime}}
|
|
33 |
and assume \isa{P{\isacharprime}} when simplifying \isa{Q} to \isa{Q{\isacharprime}}.
|
|
34 |
|
|
35 |
Here are some more examples. The congruence rules for bounded
|
|
36 |
quantifiers supply contextual information about the bound variable:
|
|
37 |
\begin{isabelle}%
|
|
38 |
\ \ \ \ \ {\isasymlbrakk}A\ {\isacharequal}\ B{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ B\ {\isasymLongrightarrow}\ P\ x\ {\isacharequal}\ Q\ x{\isasymrbrakk}\isanewline
|
|
39 |
\ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymforall}x{\isasymin}A{\isachardot}\ P\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymforall}x{\isasymin}B{\isachardot}\ Q\ x{\isacharparenright}%
|
|
40 |
\end{isabelle}
|
|
41 |
The congruence rule for conditional expressions supply contextual
|
|
42 |
information for simplifying the arms:
|
|
43 |
\begin{isabelle}%
|
|
44 |
\ \ \ \ \ {\isasymlbrakk}b\ {\isacharequal}\ c{\isacharsemicolon}\ c\ {\isasymLongrightarrow}\ x\ {\isacharequal}\ u{\isacharsemicolon}\ {\isasymnot}\ c\ {\isasymLongrightarrow}\ y\ {\isacharequal}\ v{\isasymrbrakk}\isanewline
|
|
45 |
\ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}if\ b\ then\ x\ else\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ c\ then\ u\ else\ v{\isacharparenright}%
|
|
46 |
\end{isabelle}
|
|
47 |
A congruence rule can also \emph{prevent} simplification of some arguments.
|
|
48 |
Here is an alternative congruence rule for conditional expressions:
|
|
49 |
\begin{isabelle}%
|
|
50 |
\ \ \ \ \ b\ {\isacharequal}\ c\ {\isasymLongrightarrow}\ {\isacharparenleft}if\ b\ then\ x\ else\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ c\ then\ x\ else\ y{\isacharparenright}%
|
|
51 |
\end{isabelle}
|
|
52 |
Only the first argument is simplified; the others remain unchanged.
|
|
53 |
This makes simplification much faster and is faithful to the evaluation
|
|
54 |
strategy in programming languages, which is why this is the default
|
|
55 |
congruence rule for \isa{if}. Analogous rules control the evaluaton of
|
|
56 |
\isa{case} expressions.
|
|
57 |
|
|
58 |
You can delare your own congruence rules with the attribute \isa{cong},
|
|
59 |
either globally, in the usual manner,
|
|
60 |
\begin{quote}
|
|
61 |
\isacommand{declare} \textit{theorem-name} \isa{{\isacharbrackleft}cong{\isacharbrackright}}
|
|
62 |
\end{quote}
|
|
63 |
or locally in a \isa{simp} call by adding the modifier
|
|
64 |
\begin{quote}
|
|
65 |
\isa{cong{\isacharcolon}} \textit{list of theorem names}
|
|
66 |
\end{quote}
|
|
67 |
The effect is reversed by \isa{cong\ del} instead of \isa{cong}.
|
|
68 |
|
|
69 |
\begin{warn}
|
|
70 |
The congruence rule \isa{conj{\isacharunderscore}cong}
|
|
71 |
\begin{isabelle}%
|
|
72 |
\ \ \ \ \ {\isasymlbrakk}P\ {\isacharequal}\ P{\isacharprime}{\isacharsemicolon}\ P{\isacharprime}\ {\isasymLongrightarrow}\ Q\ {\isacharequal}\ Q{\isacharprime}{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}P\ {\isasymand}\ Q{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}P{\isacharprime}\ {\isasymand}\ Q{\isacharprime}{\isacharparenright}%
|
|
73 |
\end{isabelle}
|
|
74 |
is occasionally useful but not a default rule; you have to use it explicitly.
|
|
75 |
\end{warn}%
|
|
76 |
\end{isamarkuptext}%
|
|
77 |
%
|
|
78 |
\isamarkupsubsubsection{Permutative rewrite rules}
|
|
79 |
%
|
|
80 |
\begin{isamarkuptext}%
|
|
81 |
\index{rewrite rule!permutative|bold}
|
|
82 |
\index{rewriting!ordered|bold}
|
|
83 |
\index{ordered rewriting|bold}
|
|
84 |
\index{simplification!ordered|bold}
|
|
85 |
An equation is a \bfindex{permutative rewrite rule} if the left-hand
|
|
86 |
side and right-hand side are the same up to renaming of variables. The most
|
|
87 |
common permutative rule is commutativity: \isa{x\ {\isacharplus}\ y\ {\isacharequal}\ y\ {\isacharplus}\ x}. Other examples
|
|
88 |
include \isa{x\ {\isacharminus}\ y\ {\isacharminus}\ z\ {\isacharequal}\ x\ {\isacharminus}\ z\ {\isacharminus}\ y} in arithmetic and \isa{insert\ x\ {\isacharparenleft}insert\ y\ A{\isacharparenright}\ {\isacharequal}\ insert\ y\ {\isacharparenleft}insert\ x\ A{\isacharparenright}} for sets. Such rules are problematic because
|
|
89 |
once they apply, they can be used forever. The simplifier is aware of this
|
|
90 |
danger and treats permutative rules by means of a special strategy, called
|
|
91 |
\bfindex{ordered rewriting}: a permutative rewrite
|
|
92 |
rule is only applied if the term becomes ``smaller'' (w.r.t.\ some fixed
|
|
93 |
lexicographic ordering on terms). For example, commutativity rewrites
|
|
94 |
\isa{b\ {\isacharplus}\ a} to \isa{a\ {\isacharplus}\ b}, but then stops because \isa{a\ {\isacharplus}\ b} is strictly
|
|
95 |
smaller than \isa{b\ {\isacharplus}\ a}. Permutative rewrite rules can be turned into
|
|
96 |
simplification rules in the usual manner via the \isa{simp} attribute; the
|
|
97 |
simplifier recognizes their special status automatically.
|
|
98 |
|
|
99 |
Permutative rewrite rules are most effective in the case of
|
|
100 |
associative-commutative operators. (Associativity by itself is not
|
|
101 |
permutative.) When dealing with an AC-operator~$f$, keep the
|
|
102 |
following points in mind:
|
|
103 |
\begin{itemize}\index{associative-commutative operators}
|
|
104 |
|
|
105 |
\item The associative law must always be oriented from left to right,
|
|
106 |
namely $f(f(x,y),z) = f(x,f(y,z))$. The opposite orientation, if
|
|
107 |
used with commutativity, can lead to nontermination.
|
|
108 |
|
|
109 |
\item To complete your set of rewrite rules, you must add not just
|
|
110 |
associativity~(A) and commutativity~(C) but also a derived rule, {\bf
|
|
111 |
left-com\-mut\-ativ\-ity} (LC): $f(x,f(y,z)) = f(y,f(x,z))$.
|
|
112 |
\end{itemize}
|
|
113 |
Ordered rewriting with the combination of A, C, and LC sorts a term
|
|
114 |
lexicographically:
|
|
115 |
\[\def\maps#1{~\stackrel{#1}{\leadsto}~}
|
|
116 |
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)) \]
|
|
117 |
|
|
118 |
Note that ordered rewriting for \isa{{\isacharplus}} and \isa{{\isacharasterisk}} on numbers is rarely
|
|
119 |
necessary because the builtin arithmetic capabilities often take care of
|
|
120 |
this.%
|
|
121 |
\end{isamarkuptext}%
|
|
122 |
%
|
|
123 |
\isamarkupsubsection{How it works}
|
|
124 |
%
|
|
125 |
\begin{isamarkuptext}%
|
|
126 |
\label{sec:SimpHow}
|
|
127 |
Roughly speaking, the simplifier proceeds bottom-up (subterms are simplified
|
|
128 |
first) and a conditional equation is only applied if its condition could be
|
|
129 |
proved (again by simplification). Below we explain some special%
|
|
130 |
\end{isamarkuptext}%
|
|
131 |
%
|
|
132 |
\isamarkupsubsubsection{Higher-order patterns}
|
|
133 |
%
|
|
134 |
\isamarkupsubsubsection{Local assumptions}
|
|
135 |
%
|
|
136 |
\isamarkupsubsubsection{The preprocessor}
|
|
137 |
%
|
|
138 |
\begin{isamarkuptext}%
|
|
139 |
\index{simplification|)}%
|
|
140 |
\end{isamarkuptext}%
|
|
141 |
\end{isabellebody}%
|
|
142 |
%%% Local Variables:
|
|
143 |
%%% mode: latex
|
|
144 |
%%% TeX-master: "root"
|
|
145 |
%%% End:
|