|
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 |
|
81 rule is only applied if the term becomes ``smaller'' (w.r.t.\ some fixed |
|
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 |
|
89 associative-commutative operators. (Associativity by itself is not |
|
90 permutative.) When dealing with an AC-operator~$f$, keep the |
|
91 following points in mind: |
|
92 \begin{itemize}\index{associative-commutative operators} |
|
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 |
|
117 proved (again by simplification). Below we explain some special |
|
118 *} |
|
119 |
|
120 subsubsection{*Higher-order patterns*} |
|
121 |
|
122 subsubsection{*Local assumptions*} |
|
123 |
|
124 subsubsection{*The preprocessor*} |
|
125 |
|
126 text{* |
|
127 \index{simplification|)} |
|
128 *} |
|
129 (*<*) |
|
130 end |
|
131 (*>*) |