9958
|
1 |
(*<*)
|
|
2 |
theory simp = Main:
|
|
3 |
(*>*)
|
|
4 |
|
|
5 |
section{*Simplification*}
|
|
6 |
|
|
7 |
text{*\label{sec:simplification-II}\index{simplification|(}
|
|
8 |
This section discusses some additional nifty features not covered so far and
|
|
9 |
gives a short introduction to the simplification process itself. The latter
|
|
10 |
is helpful to understand why a particular rule does or does not apply in some
|
|
11 |
situation.
|
|
12 |
*}
|
|
13 |
|
|
14 |
subsection{*Advanced features*}
|
|
15 |
|
|
16 |
subsubsection{*Congruence rules*}
|
|
17 |
|
|
18 |
text{*\label{sec:simp-cong}
|
|
19 |
It is hardwired into the simplifier that while simplifying the conclusion $Q$
|
|
20 |
of $P \isasymImp Q$ it is legal to make uses of the assumptions $P$. This
|
|
21 |
kind of contextual information can also be made available for other
|
|
22 |
operators. For example, @{prop"xs = [] --> xs@xs = xs"} simplifies to @{term
|
|
23 |
True} because we may use @{prop"xs = []"} when simplifying @{prop"xs@xs =
|
|
24 |
xs"}. The generation of contextual information during simplification is
|
|
25 |
controlled by so-called \bfindex{congruence rules}. This is the one for
|
|
26 |
@{text"\<longrightarrow>"}:
|
|
27 |
@{thm[display]imp_cong[no_vars]}
|
|
28 |
It should be read as follows:
|
|
29 |
In order to simplify @{prop"P-->Q"} to @{prop"P'-->Q'"},
|
|
30 |
simplify @{prop P} to @{prop P'}
|
|
31 |
and assume @{prop"P'"} when simplifying @{prop Q} to @{prop"Q'"}.
|
|
32 |
|
|
33 |
Here are some more examples. The congruence rules for bounded
|
|
34 |
quantifiers supply contextual information about the bound variable:
|
|
35 |
@{thm[display,eta_contract=false,margin=60]ball_cong[no_vars]}
|
|
36 |
The congruence rule for conditional expressions supply contextual
|
|
37 |
information for simplifying the arms:
|
|
38 |
@{thm[display]if_cong[no_vars]}
|
|
39 |
A congruence rule can also \emph{prevent} simplification of some arguments.
|
|
40 |
Here is an alternative congruence rule for conditional expressions:
|
|
41 |
@{thm[display]if_weak_cong[no_vars]}
|
|
42 |
Only the first argument is simplified; the others remain unchanged.
|
|
43 |
This makes simplification much faster and is faithful to the evaluation
|
|
44 |
strategy in programming languages, which is why this is the default
|
|
45 |
congruence rule for @{text if}. Analogous rules control the evaluaton of
|
|
46 |
@{text case} expressions.
|
|
47 |
|
|
48 |
You can delare your own congruence rules with the attribute @{text cong},
|
|
49 |
either globally, in the usual manner,
|
|
50 |
\begin{quote}
|
|
51 |
\isacommand{declare} \textit{theorem-name} @{text"[cong]"}
|
|
52 |
\end{quote}
|
|
53 |
or locally in a @{text"simp"} call by adding the modifier
|
|
54 |
\begin{quote}
|
|
55 |
@{text"cong:"} \textit{list of theorem names}
|
|
56 |
\end{quote}
|
|
57 |
The effect is reversed by @{text"cong del"} instead of @{text cong}.
|
|
58 |
|
|
59 |
\begin{warn}
|
|
60 |
The congruence rule @{thm[source]conj_cong}
|
|
61 |
@{thm[display]conj_cong[no_vars]}
|
|
62 |
is occasionally useful but not a default rule; you have to use it explicitly.
|
|
63 |
\end{warn}
|
|
64 |
*}
|
|
65 |
|
|
66 |
subsubsection{*Permutative rewrite rules*}
|
|
67 |
|
|
68 |
text{*
|
|
69 |
\index{rewrite rule!permutative|bold}
|
|
70 |
\index{rewriting!ordered|bold}
|
|
71 |
\index{ordered rewriting|bold}
|
|
72 |
\index{simplification!ordered|bold}
|
|
73 |
An equation is a \bfindex{permutative rewrite rule} if the left-hand
|
|
74 |
side and right-hand side are the same up to renaming of variables. The most
|
|
75 |
common permutative rule is commutativity: @{prop"x+y = y+x"}. Other examples
|
|
76 |
include @{prop"(x-y)-z = (x-z)-y"} in arithmetic and @{prop"insert x (insert
|
|
77 |
y A) = insert y (insert x A)"} for sets. Such rules are problematic because
|
|
78 |
once they apply, they can be used forever. The simplifier is aware of this
|
|
79 |
danger and treats permutative rules by means of a special strategy, called
|
|
80 |
\bfindex{ordered rewriting}: a permutative rewrite
|
10795
|
81 |
rule is only applied if the term becomes ``smaller'' (with respect to a fixed
|
9958
|
82 |
lexicographic ordering on terms). For example, commutativity rewrites
|
|
83 |
@{term"b+a"} to @{term"a+b"}, but then stops because @{term"a+b"} is strictly
|
|
84 |
smaller than @{term"b+a"}. Permutative rewrite rules can be turned into
|
|
85 |
simplification rules in the usual manner via the @{text simp} attribute; the
|
|
86 |
simplifier recognizes their special status automatically.
|
|
87 |
|
|
88 |
Permutative rewrite rules are most effective in the case of
|
10281
|
89 |
associative-commutative functions. (Associativity by itself is not
|
|
90 |
permutative.) When dealing with an AC-function~$f$, keep the
|
9958
|
91 |
following points in mind:
|
10281
|
92 |
\begin{itemize}\index{associative-commutative function}
|
9958
|
93 |
|
|
94 |
\item The associative law must always be oriented from left to right,
|
|
95 |
namely $f(f(x,y),z) = f(x,f(y,z))$. The opposite orientation, if
|
|
96 |
used with commutativity, can lead to nontermination.
|
|
97 |
|
|
98 |
\item To complete your set of rewrite rules, you must add not just
|
|
99 |
associativity~(A) and commutativity~(C) but also a derived rule, {\bf
|
|
100 |
left-com\-mut\-ativ\-ity} (LC): $f(x,f(y,z)) = f(y,f(x,z))$.
|
|
101 |
\end{itemize}
|
|
102 |
Ordered rewriting with the combination of A, C, and LC sorts a term
|
|
103 |
lexicographically:
|
|
104 |
\[\def\maps#1{~\stackrel{#1}{\leadsto}~}
|
|
105 |
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)) \]
|
|
106 |
|
|
107 |
Note that ordered rewriting for @{text"+"} and @{text"*"} on numbers is rarely
|
|
108 |
necessary because the builtin arithmetic capabilities often take care of
|
|
109 |
this.
|
|
110 |
*}
|
|
111 |
|
|
112 |
subsection{*How it works*}
|
|
113 |
|
|
114 |
text{*\label{sec:SimpHow}
|
|
115 |
Roughly speaking, the simplifier proceeds bottom-up (subterms are simplified
|
|
116 |
first) and a conditional equation is only applied if its condition could be
|
10186
|
117 |
proved (again by simplification). Below we explain some special features of the rewriting process.
|
9958
|
118 |
*}
|
|
119 |
|
|
120 |
subsubsection{*Higher-order patterns*}
|
|
121 |
|
10186
|
122 |
text{*\index{simplification rule|(}
|
|
123 |
So far we have pretended the simplifier can deal with arbitrary
|
|
124 |
rewrite rules. This is not quite true. Due to efficiency (and
|
|
125 |
potentially also computability) reasons, the simplifier expects the
|
|
126 |
left-hand side of each rule to be a so-called \emph{higher-order
|
|
127 |
pattern}~\cite{nipkow-patterns}\indexbold{higher-order
|
|
128 |
pattern}\indexbold{pattern, higher-order}. This restricts where
|
|
129 |
unknowns may occur. Higher-order patterns are terms in $\beta$-normal
|
|
130 |
form (this will always be the case unless you have done something
|
|
131 |
strange) where each occurrence of an unknown is of the form
|
|
132 |
$\Var{f}~x@1~\dots~x@n$, where the $x@i$ are distinct bound
|
|
133 |
variables. Thus all ``standard'' rewrite rules, where all unknowns are
|
|
134 |
of base type, for example @{thm add_assoc}, are OK: if an unknown is
|
|
135 |
of base type, it cannot have any arguments. Additionally, the rule
|
|
136 |
@{text"(\<forall>x. ?P x \<and> ?Q x) = ((\<forall>x. ?P x) \<and> (\<forall>x. ?Q x))"} is also OK, in
|
|
137 |
both directions: all arguments of the unknowns @{text"?P"} and
|
|
138 |
@{text"?Q"} are distinct bound variables.
|
|
139 |
|
|
140 |
If the left-hand side is not a higher-order pattern, not all is lost
|
|
141 |
and the simplifier will still try to apply the rule, but only if it
|
|
142 |
matches ``directly'', i.e.\ without much $\lambda$-calculus hocus
|
|
143 |
pocus. For example, @{text"?f ?x \<in> range ?f = True"} rewrites
|
|
144 |
@{term"g a \<in> range g"} to @{term True}, but will fail to match
|
|
145 |
@{text"g(h b) \<in> range(\<lambda>x. g(h x))"}. However, you can
|
|
146 |
replace the offending subterms (in our case @{text"?f ?x"}, which
|
|
147 |
is not a pattern) by adding new variables and conditions: @{text"?y =
|
|
148 |
?f ?x \<Longrightarrow> ?y \<in> range ?f = True"} is fine
|
|
149 |
as a conditional rewrite rule since conditions can be arbitrary
|
|
150 |
terms. However, this trick is not a panacea because the newly
|
|
151 |
introduced conditions may be hard to prove, which has to take place
|
|
152 |
before the rule can actually be applied.
|
|
153 |
|
|
154 |
There is basically no restriction on the form of the right-hand
|
|
155 |
sides. They may not contain extraneous term or type variables, though.
|
|
156 |
*}
|
9958
|
157 |
|
|
158 |
subsubsection{*The preprocessor*}
|
|
159 |
|
|
160 |
text{*
|
10186
|
161 |
When some theorem is declared a simplification rule, it need not be a
|
|
162 |
conditional equation already. The simplifier will turn it into a set of
|
|
163 |
conditional equations automatically. For example, given @{prop"f x =
|
|
164 |
g x & h x = k x"} the simplifier will turn this into the two separate
|
|
165 |
simplifiction rules @{prop"f x = g x"} and @{prop"h x = k x"}. In
|
|
166 |
general, the input theorem is converted as follows:
|
|
167 |
\begin{eqnarray}
|
|
168 |
\neg P &\mapsto& P = False \nonumber\\
|
|
169 |
P \longrightarrow Q &\mapsto& P \Longrightarrow Q \nonumber\\
|
|
170 |
P \land Q &\mapsto& P,\ Q \nonumber\\
|
|
171 |
\forall x.~P~x &\mapsto& P~\Var{x}\nonumber\\
|
|
172 |
\forall x \in A.\ P~x &\mapsto& \Var{x} \in A \Longrightarrow P~\Var{x} \nonumber\\
|
|
173 |
@{text if}\ P\ @{text then}\ Q\ @{text else}\ R &\mapsto&
|
|
174 |
P \Longrightarrow Q,\ \neg P \Longrightarrow R \nonumber
|
|
175 |
\end{eqnarray}
|
|
176 |
Once this conversion process is finished, all remaining non-equations
|
|
177 |
$P$ are turned into trivial equations $P = True$.
|
|
178 |
For example, the formula @{prop"(p \<longrightarrow> q \<and> r) \<and> s"} is converted into the three rules
|
|
179 |
\begin{center}
|
|
180 |
@{prop"p \<Longrightarrow> q = True"},\quad @{prop"p \<Longrightarrow> r = True"},\quad @{prop"s = True"}.
|
|
181 |
\end{center}
|
|
182 |
\index{simplification rule|)}
|
9958
|
183 |
\index{simplification|)}
|
|
184 |
*}
|
|
185 |
(*<*)
|
|
186 |
end
|
|
187 |
(*>*)
|