|
1 (*<*) |
|
2 theory simp2 imports Main begin |
|
3 (*>*) |
|
4 |
|
5 section{*Simplification*} |
|
6 |
|
7 text{*\label{sec:simplification-II}\index{simplification|(} |
|
8 This section describes features not covered until now. It also |
|
9 outlines the simplification process itself, which can be helpful |
|
10 when the simplifier does not do what you expect of it. |
|
11 *} |
|
12 |
|
13 subsection{*Advanced Features*} |
|
14 |
|
15 subsubsection{*Congruence Rules*} |
|
16 |
|
17 text{*\label{sec:simp-cong} |
|
18 While simplifying the conclusion $Q$ |
|
19 of $P \Imp Q$, it is legal to use the assumption $P$. |
|
20 For $\Imp$ this policy is hardwired, but |
|
21 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 One congruence rule for conditional expressions supplies contextual |
|
37 information for simplifying the @{text then} and @{text else} cases: |
|
38 @{thm[display]if_cong[no_vars]} |
|
39 An alternative congruence rule for conditional expressions |
|
40 actually \emph{prevents} simplification of some arguments: |
|
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 evaluation of |
|
46 @{text case} expressions. |
|
47 |
|
48 You can declare your own congruence rules with the attribute \attrdx{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 \par\noindent |
|
63 is occasionally useful but is not a default rule; you have to declare it explicitly. |
|
64 \end{warn} |
|
65 *} |
|
66 |
|
67 subsubsection{*Permutative Rewrite Rules*} |
|
68 |
|
69 text{* |
|
70 \index{rewrite rules!permutative|bold}% |
|
71 An equation is a \textbf{permutative rewrite rule} if the left-hand |
|
72 side and right-hand side are the same up to renaming of variables. The most |
|
73 common permutative rule is commutativity: @{prop"x+y = y+x"}. Other examples |
|
74 include @{prop"(x-y)-z = (x-z)-y"} in arithmetic and @{prop"insert x (insert |
|
75 y A) = insert y (insert x A)"} for sets. Such rules are problematic because |
|
76 once they apply, they can be used forever. The simplifier is aware of this |
|
77 danger and treats permutative rules by means of a special strategy, called |
|
78 \bfindex{ordered rewriting}: a permutative rewrite |
|
79 rule is only applied if the term becomes smaller with respect to a fixed |
|
80 lexicographic ordering on terms. For example, commutativity rewrites |
|
81 @{term"b+a"} to @{term"a+b"}, but then stops because @{term"a+b"} is strictly |
|
82 smaller than @{term"b+a"}. Permutative rewrite rules can be turned into |
|
83 simplification rules in the usual manner via the @{text simp} attribute; the |
|
84 simplifier recognizes their special status automatically. |
|
85 |
|
86 Permutative rewrite rules are most effective in the case of |
|
87 associative-commutative functions. (Associativity by itself is not |
|
88 permutative.) When dealing with an AC-function~$f$, keep the |
|
89 following points in mind: |
|
90 \begin{itemize}\index{associative-commutative function} |
|
91 |
|
92 \item The associative law must always be oriented from left to right, |
|
93 namely $f(f(x,y),z) = f(x,f(y,z))$. The opposite orientation, if |
|
94 used with commutativity, can lead to nontermination. |
|
95 |
|
96 \item To complete your set of rewrite rules, you must add not just |
|
97 associativity~(A) and commutativity~(C) but also a derived rule, {\bf |
|
98 left-com\-mut\-ativ\-ity} (LC): $f(x,f(y,z)) = f(y,f(x,z))$. |
|
99 \end{itemize} |
|
100 Ordered rewriting with the combination of A, C, and LC sorts a term |
|
101 lexicographically: |
|
102 \[\def\maps#1{~\stackrel{#1}{\leadsto}~} |
|
103 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)) \] |
|
104 |
|
105 Note that ordered rewriting for @{text"+"} and @{text"*"} on numbers is rarely |
|
106 necessary because the built-in arithmetic prover often succeeds without |
|
107 such tricks. |
|
108 *} |
|
109 |
|
110 subsection{*How the Simplifier Works*} |
|
111 |
|
112 text{*\label{sec:SimpHow} |
|
113 Roughly speaking, the simplifier proceeds bottom-up: subterms are simplified |
|
114 first. A conditional equation is only applied if its condition can be |
|
115 proved, again by simplification. Below we explain some special features of |
|
116 the rewriting process. |
|
117 *} |
|
118 |
|
119 subsubsection{*Higher-Order Patterns*} |
|
120 |
|
121 text{*\index{simplification rule|(} |
|
122 So far we have pretended the simplifier can deal with arbitrary |
|
123 rewrite rules. This is not quite true. For reasons of feasibility, |
|
124 the simplifier expects the |
|
125 left-hand side of each rule to be a so-called \emph{higher-order |
|
126 pattern}~\cite{nipkow-patterns}\indexbold{patterns!higher-order}. |
|
127 This restricts where |
|
128 unknowns may occur. Higher-order patterns are terms in $\beta$-normal |
|
129 form. (This means there are no subterms of the form $(\lambda x. M)(N)$.) |
|
130 Each occurrence of an unknown is of the form |
|
131 $\Var{f}~x@1~\dots~x@n$, where the $x@i$ are distinct bound |
|
132 variables. Thus all ordinary rewrite rules, where all unknowns are |
|
133 of base type, for example @{thm add_assoc}, are acceptable: if an unknown is |
|
134 of base type, it cannot have any arguments. Additionally, the rule |
|
135 @{text"(\<forall>x. ?P x \<and> ?Q x) = ((\<forall>x. ?P x) \<and> (\<forall>x. ?Q x))"} is also acceptable, in |
|
136 both directions: all arguments of the unknowns @{text"?P"} and |
|
137 @{text"?Q"} are distinct bound variables. |
|
138 |
|
139 If the left-hand side is not a higher-order pattern, all is not lost. |
|
140 The simplifier will still try to apply the rule provided it |
|
141 matches directly: without much $\lambda$-calculus hocus |
|
142 pocus. For example, @{text"(?f ?x \<in> range ?f) = True"} rewrites |
|
143 @{term"g a \<in> range g"} to @{const True}, but will fail to match |
|
144 @{text"g(h b) \<in> range(\<lambda>x. g(h x))"}. However, you can |
|
145 eliminate the offending subterms --- those that are not patterns --- |
|
146 by adding new variables and conditions. |
|
147 In our example, we eliminate @{text"?f ?x"} and obtain |
|
148 @{text"?y = |
|
149 ?f ?x \<Longrightarrow> (?y \<in> range ?f) = True"}, which is fine |
|
150 as a conditional rewrite rule since conditions can be arbitrary |
|
151 terms. However, this trick is not a panacea because the newly |
|
152 introduced conditions may be hard to solve. |
|
153 |
|
154 There is no restriction on the form of the right-hand |
|
155 sides. They may not contain extraneous term or type variables, though. |
|
156 *} |
|
157 |
|
158 subsubsection{*The Preprocessor*} |
|
159 |
|
160 text{*\label{sec:simp-preprocessor} |
|
161 When a 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, @{prop"f x = |
|
164 g x & h x = k x"} becomes the two separate |
|
165 simplification 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 = \hbox{\isa{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 =\isa{True}$. |
|
178 For example, the formula |
|
179 \begin{center}@{prop"(p \<longrightarrow> t=u \<and> ~r) \<and> s"}\end{center} |
|
180 is converted into the three rules |
|
181 \begin{center} |
|
182 @{prop"p \<Longrightarrow> t = u"},\quad @{prop"p \<Longrightarrow> r = False"},\quad @{prop"s = True"}. |
|
183 \end{center} |
|
184 \index{simplification rule|)} |
|
185 \index{simplification|)} |
|
186 *} |
|
187 (*<*) |
|
188 end |
|
189 (*>*) |