author | nipkow |
Thu, 07 Aug 2014 09:48:04 +0200 | |
changeset 57804 | fcf966675478 |
parent 56989 | fafcf43ded4a |
child 57817 | dfebc374bd89 |
permissions | -rw-r--r-- |
47269 | 1 |
(*<*) |
2 |
theory Types_and_funs |
|
3 |
imports Main |
|
4 |
begin |
|
5 |
(*>*) |
|
6 |
text{* |
|
7 |
\vspace{-5ex} |
|
52361 | 8 |
\section{Type and Function Definitions} |
47269 | 9 |
|
10 |
Type synonyms are abbreviations for existing types, for example |
|
11 |
*} |
|
12 |
||
13 |
type_synonym string = "char list" |
|
14 |
||
55348 | 15 |
text{*\index{string@@{text string}} |
47269 | 16 |
Type synonyms are expanded after parsing and are not present in internal representation and output. They are mere conveniences for the reader. |
17 |
||
18 |
\subsection{Datatypes} |
|
51465 | 19 |
\label{sec:datatypes} |
47269 | 20 |
|
21 |
The general form of a datatype definition looks like this: |
|
22 |
\begin{quote} |
|
23 |
\begin{tabular}{@ {}rclcll} |
|
55348 | 24 |
\indexed{\isacom{datatype}}{datatype} @{text "('a\<^sub>1,\<dots>,'a\<^sub>n)t"} |
47269 | 25 |
& = & $C_1 \ @{text"\""}\tau_{1,1}@{text"\""} \dots @{text"\""}\tau_{1,n_1}@{text"\""}$ \\ |
26 |
& $|$ & \dots \\ |
|
27 |
& $|$ & $C_k \ @{text"\""}\tau_{k,1}@{text"\""} \dots @{text"\""}\tau_{k,n_k}@{text"\""}$ |
|
28 |
\end{tabular} |
|
29 |
\end{quote} |
|
30 |
It introduces the constructors \ |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset
|
31 |
$C_i :: \tau_{i,1}\Rightarrow \cdots \Rightarrow \tau_{i,n_i} \Rightarrow$~@{text "('a\<^sub>1,\<dots>,'a\<^sub>n)t"} \ and expresses that any value of this type is built from these constructors in a unique manner. Uniqueness is implied by the following |
47269 | 32 |
properties of the constructors: |
33 |
\begin{itemize} |
|
34 |
\item \emph{Distinctness:} $C_i\ \ldots \neq C_j\ \dots$ \quad if $i \neq j$ |
|
35 |
\item \emph{Injectivity:} |
|
36 |
\begin{tabular}[t]{l} |
|
37 |
$(C_i \ x_1 \dots x_{n_i} = C_i \ y_1 \dots y_{n_i}) =$\\ |
|
38 |
$(x_1 = y_1 \land \dots \land x_{n_i} = y_{n_i})$ |
|
39 |
\end{tabular} |
|
40 |
\end{itemize} |
|
41 |
The fact that any value of the datatype is built from the constructors implies |
|
55348 | 42 |
the \concept{structural induction}\index{induction} rule: to show |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset
|
43 |
$P~x$ for all $x$ of type @{text "('a\<^sub>1,\<dots>,'a\<^sub>n)t"}, |
47269 | 44 |
one needs to show $P(C_i\ x_1 \dots x_{n_i})$ (for each $i$) assuming |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset
|
45 |
$P(x_j)$ for all $j$ where $\tau_{i,j} =$~@{text "('a\<^sub>1,\<dots>,'a\<^sub>n)t"}. |
47269 | 46 |
Distinctness and injectivity are applied automatically by @{text auto} |
47 |
and other proof methods. Induction must be applied explicitly. |
|
48 |
||
55348 | 49 |
Datatype values can be taken apart with case expressions\index{case expression}\index{case expression@@{text "case ... of"}}, for example |
47269 | 50 |
\begin{quote} |
51 |
\noquotes{@{term[source] "(case xs of [] \<Rightarrow> 0 | x # _ \<Rightarrow> Suc x)"}} |
|
52 |
\end{quote} |
|
53 |
just like in functional programming languages. Case expressions |
|
54 |
must be enclosed in parentheses. |
|
55 |
||
56 |
As an example, consider binary trees: |
|
57 |
*} |
|
58 |
||
47306 | 59 |
datatype 'a tree = Tip | Node "'a tree" 'a "'a tree" |
47269 | 60 |
|
61 |
text{* with a mirror function: *} |
|
62 |
||
63 |
fun mirror :: "'a tree \<Rightarrow> 'a tree" where |
|
64 |
"mirror Tip = Tip" | |
|
65 |
"mirror (Node l a r) = Node (mirror r) a (mirror l)" |
|
66 |
||
67 |
text{* The following lemma illustrates induction: *} |
|
68 |
||
69 |
lemma "mirror(mirror t) = t" |
|
70 |
apply(induction t) |
|
71 |
||
72 |
txt{* yields |
|
73 |
@{subgoals[display]} |
|
74 |
The induction step contains two induction hypotheses, one for each subtree. |
|
75 |
An application of @{text auto} finishes the proof. |
|
76 |
||
77 |
A very simple but also very useful datatype is the predefined |
|
55348 | 78 |
@{datatype[display] option}\index{option@@{text option}}\index{None@@{const None}}\index{Some@@{const Some}} |
47269 | 79 |
Its sole purpose is to add a new element @{const None} to an existing |
80 |
type @{typ 'a}. To make sure that @{const None} is distinct from all the |
|
81 |
elements of @{typ 'a}, you wrap them up in @{const Some} and call |
|
82 |
the new type @{typ"'a option"}. A typical application is a lookup function |
|
83 |
on a list of key-value pairs, often called an association list: |
|
84 |
*} |
|
85 |
(*<*) |
|
86 |
apply auto |
|
87 |
done |
|
88 |
(*>*) |
|
89 |
fun lookup :: "('a * 'b) list \<Rightarrow> 'a \<Rightarrow> 'b option" where |
|
47306 | 90 |
"lookup [] x = None" | |
91 |
"lookup ((a,b) # ps) x = (if a = x then Some b else lookup ps x)" |
|
47269 | 92 |
|
93 |
text{* |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset
|
94 |
Note that @{text"\<tau>\<^sub>1 * \<tau>\<^sub>2"} is the type of pairs, also written @{text"\<tau>\<^sub>1 \<times> \<tau>\<^sub>2"}. |
51393 | 95 |
Pairs can be taken apart either by pattern matching (as above) or with the |
57804 | 96 |
projection functions @{const fst} and @{const snd}: @{thm fst_conv[of x y]} and @{thm snd_conv[of x y]}. |
97 |
Tuples are simulated by pairs nested to the right: @{term"(a,b,c)"} |
|
98 |
is short for @{text"(a, (b, c))"} and @{text "\<tau>\<^sub>1 \<times> \<tau>\<^sub>2 \<times> \<tau>\<^sub>3"} is short for |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset
|
99 |
@{text "\<tau>\<^sub>1 \<times> (\<tau>\<^sub>2 \<times> \<tau>\<^sub>3)"}. |
47269 | 100 |
|
101 |
\subsection{Definitions} |
|
102 |
||
56989 | 103 |
Non-recursive functions can be defined as in the following example: |
55348 | 104 |
\index{definition@\isacom{definition}}*} |
47269 | 105 |
|
106 |
definition sq :: "nat \<Rightarrow> nat" where |
|
107 |
"sq n = n * n" |
|
108 |
||
109 |
text{* Such definitions do not allow pattern matching but only |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset
|
110 |
@{text"f x\<^sub>1 \<dots> x\<^sub>n = t"}, where @{text f} does not occur in @{text t}. |
47269 | 111 |
|
112 |
\subsection{Abbreviations} |
|
113 |
||
114 |
Abbreviations are similar to definitions: |
|
55348 | 115 |
\index{abbreviation@\isacom{abbreviation}}*} |
47269 | 116 |
|
117 |
abbreviation sq' :: "nat \<Rightarrow> nat" where |
|
52045 | 118 |
"sq' n \<equiv> n * n" |
47269 | 119 |
|
120 |
text{* The key difference is that @{const sq'} is only syntactic sugar: |
|
52045 | 121 |
after parsing, @{term"sq' t"} is replaced by \mbox{@{term"t*t"}}, and |
122 |
before printing, every occurrence of @{term"u*u"} is replaced by |
|
123 |
\mbox{@{term"sq' u"}}. Internally, @{const sq'} does not exist. |
|
124 |
This is the |
|
47269 | 125 |
advantage of abbreviations over definitions: definitions need to be expanded |
52045 | 126 |
explicitly (\autoref{sec:rewr-defs}) whereas abbreviations are already |
47269 | 127 |
expanded upon parsing. However, abbreviations should be introduced sparingly: |
128 |
if abused, they can lead to a confusing discrepancy between the internal and |
|
129 |
external view of a term. |
|
130 |
||
52045 | 131 |
The ASCII representation of @{text"\<equiv>"} is \texttt{==} or \xsymbol{equiv}. |
132 |
||
52361 | 133 |
\subsection{Recursive Functions} |
47269 | 134 |
\label{sec:recursive-funs} |
135 |
||
55348 | 136 |
Recursive functions are defined with \indexed{\isacom{fun}}{fun} by pattern matching |
56989 | 137 |
over datatype constructors. The order of equations matters, as in |
47269 | 138 |
functional programming languages. However, all HOL functions must be |
139 |
total. This simplifies the logic---terms are always defined---but means |
|
140 |
that recursive functions must terminate. Otherwise one could define a |
|
141 |
function @{prop"f n = f n + (1::nat)"} and conclude \mbox{@{prop"(0::nat) = 1"}} by |
|
142 |
subtracting @{term"f n"} on both sides. |
|
143 |
||
47711 | 144 |
Isabelle's automatic termination checker requires that the arguments of |
47269 | 145 |
recursive calls on the right-hand side must be strictly smaller than the |
146 |
arguments on the left-hand side. In the simplest case, this means that one |
|
147 |
fixed argument position decreases in size with each recursive call. The size |
|
148 |
is measured as the number of constructors (excluding 0-ary ones, e.g.\ @{text |
|
47711 | 149 |
Nil}). Lexicographic combinations are also recognized. In more complicated |
47269 | 150 |
situations, the user may have to prove termination by hand. For details |
151 |
see~\cite{Krauss}. |
|
152 |
||
153 |
Functions defined with \isacom{fun} come with their own induction schema |
|
154 |
that mirrors the recursion schema and is derived from the termination |
|
155 |
order. For example, |
|
156 |
*} |
|
157 |
||
158 |
fun div2 :: "nat \<Rightarrow> nat" where |
|
159 |
"div2 0 = 0" | |
|
54136 | 160 |
"div2 (Suc 0) = 0" | |
47269 | 161 |
"div2 (Suc(Suc n)) = Suc(div2 n)" |
162 |
||
163 |
text{* does not just define @{const div2} but also proves a |
|
47711 | 164 |
customized induction rule: |
47269 | 165 |
\[ |
166 |
\inferrule{ |
|
167 |
\mbox{@{thm (prem 1) div2.induct}}\\ |
|
168 |
\mbox{@{thm (prem 2) div2.induct}}\\ |
|
169 |
\mbox{@{thm (prem 3) div2.induct}}} |
|
170 |
{\mbox{@{thm (concl) div2.induct[of _ "m"]}}} |
|
171 |
\] |
|
47711 | 172 |
This customized induction rule can simplify inductive proofs. For example, |
47269 | 173 |
*} |
174 |
||
54571 | 175 |
lemma "div2(n) = n div 2" |
47269 | 176 |
apply(induction n rule: div2.induct) |
177 |
||
54571 | 178 |
txt{* (where the infix @{text div} is the predefined division operation) |
56989 | 179 |
yields the subgoals |
47269 | 180 |
@{subgoals[display,margin=65]} |
181 |
An application of @{text auto} finishes the proof. |
|
182 |
Had we used ordinary structural induction on @{text n}, |
|
183 |
the proof would have needed an additional |
|
47711 | 184 |
case analysis in the induction step. |
47269 | 185 |
|
54571 | 186 |
This example leads to the following induction heuristic: |
187 |
\begin{quote} |
|
188 |
\emph{Let @{text f} be a recursive function. |
|
189 |
If the definition of @{text f} is more complicated |
|
190 |
than having one equation for each constructor of some datatype, |
|
55348 | 191 |
then properties of @{text f} are best proved via @{text "f.induct"}.\index{inductionrule@@{text".induct"}}} |
54571 | 192 |
\end{quote} |
193 |
||
47269 | 194 |
The general case is often called \concept{computation induction}, |
195 |
because the induction follows the (terminating!) computation. |
|
196 |
For every defining equation |
|
197 |
\begin{quote} |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset
|
198 |
@{text "f(e) = \<dots> f(r\<^sub>1) \<dots> f(r\<^sub>k) \<dots>"} |
47269 | 199 |
\end{quote} |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset
|
200 |
where @{text"f(r\<^sub>i)"}, @{text"i=1\<dots>k"}, are all the recursive calls, |
47269 | 201 |
the induction rule @{text"f.induct"} contains one premise of the form |
202 |
\begin{quote} |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset
|
203 |
@{text"P(r\<^sub>1) \<Longrightarrow> \<dots> \<Longrightarrow> P(r\<^sub>k) \<Longrightarrow> P(e)"} |
47269 | 204 |
\end{quote} |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset
|
205 |
If @{text "f :: \<tau>\<^sub>1 \<Rightarrow> \<dots> \<Rightarrow> \<tau>\<^sub>n \<Rightarrow> \<tau>"} then @{text"f.induct"} is applied like this: |
47269 | 206 |
\begin{quote} |
55348 | 207 |
\isacom{apply}@{text"(induction x\<^sub>1 \<dots> x\<^sub>n rule: f.induct)"}\index{inductionrule@@{text"induction ... rule:"}} |
47269 | 208 |
\end{quote} |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset
|
209 |
where typically there is a call @{text"f x\<^sub>1 \<dots> x\<^sub>n"} in the goal. |
47269 | 210 |
But note that the induction rule does not mention @{text f} at all, |
211 |
except in its name, and is applicable independently of @{text f}. |
|
212 |
||
54136 | 213 |
|
54436 | 214 |
\subsection*{Exercises} |
54136 | 215 |
|
216 |
\begin{exercise} |
|
54194 | 217 |
Starting from the type @{text "'a tree"} defined in the text, define |
218 |
a function @{text "contents ::"} @{typ "'a tree \<Rightarrow> 'a list"} |
|
219 |
that collects all values in a tree in a list, in any order, |
|
220 |
without removing duplicates. |
|
221 |
Then define a function @{text "treesum ::"} @{typ "nat tree \<Rightarrow> nat"} |
|
222 |
that sums up all values in a tree of natural numbers |
|
223 |
and prove @{prop "treesum t = listsum(contents t)"}. |
|
224 |
\end{exercise} |
|
225 |
||
226 |
\begin{exercise} |
|
227 |
Define a new type @{text "'a tree2"} of binary trees where values are also |
|
228 |
stored in the leaves of the tree. Also reformulate the |
|
229 |
@{const mirror} function accordingly. Define two functions |
|
230 |
@{text "pre_order"} and @{text "post_order"} of type @{text "'a tree2 \<Rightarrow> 'a list"} |
|
231 |
that traverse a tree and collect all stored values in the respective order in |
|
232 |
a list. Prove @{prop "pre_order (mirror t) = rev (post_order t)"}. |
|
233 |
\end{exercise} |
|
234 |
||
235 |
\begin{exercise} |
|
54571 | 236 |
Define a function @{text "intersperse ::"} @{typ "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"} |
237 |
such that @{text "intersperse a [x\<^sub>1, ..., x\<^sub>n] = [x\<^sub>1, a, x\<^sub>2, a, ..., a, x\<^sub>n]"}. |
|
238 |
Now prove that @{prop "map f (intersperse a xs) = intersperse (f a) (map f xs)"}. |
|
54136 | 239 |
\end{exercise} |
240 |
||
241 |
||
55348 | 242 |
\section{Induction Heuristics}\index{induction heuristics} |
47269 | 243 |
|
244 |
We have already noted that theorems about recursive functions are proved by |
|
245 |
induction. In case the function has more than one argument, we have followed |
|
246 |
the following heuristic in the proofs about the append function: |
|
247 |
\begin{quote} |
|
248 |
\emph{Perform induction on argument number $i$\\ |
|
249 |
if the function is defined by recursion on argument number $i$.} |
|
250 |
\end{quote} |
|
251 |
The key heuristic, and the main point of this section, is to |
|
47711 | 252 |
\emph{generalize the goal before induction}. |
47269 | 253 |
The reason is simple: if the goal is |
254 |
too specific, the induction hypothesis is too weak to allow the induction |
|
255 |
step to go through. Let us illustrate the idea with an example. |
|
256 |
||
257 |
Function @{const rev} has quadratic worst-case running time |
|
258 |
because it calls append for each element of the list and |
|
259 |
append is linear in its first argument. A linear time version of |
|
260 |
@{const rev} requires an extra argument where the result is accumulated |
|
261 |
gradually, using only~@{text"#"}: |
|
262 |
*} |
|
263 |
(*<*) |
|
264 |
apply auto |
|
265 |
done |
|
266 |
(*>*) |
|
267 |
fun itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where |
|
47711 | 268 |
"itrev [] ys = ys" | |
47269 | 269 |
"itrev (x#xs) ys = itrev xs (x#ys)" |
270 |
||
271 |
text{* The behaviour of @{const itrev} is simple: it reverses |
|
272 |
its first argument by stacking its elements onto the second argument, |
|
47711 | 273 |
and it returns that second argument when the first one becomes |
47269 | 274 |
empty. Note that @{const itrev} is tail-recursive: it can be |
56989 | 275 |
compiled into a loop; no stack is necessary for executing it. |
47269 | 276 |
|
277 |
Naturally, we would like to show that @{const itrev} does indeed reverse |
|
278 |
its first argument provided the second one is empty: |
|
279 |
*} |
|
280 |
||
281 |
lemma "itrev xs [] = rev xs" |
|
282 |
||
283 |
txt{* There is no choice as to the induction variable: |
|
284 |
*} |
|
285 |
||
286 |
apply(induction xs) |
|
287 |
apply(auto) |
|
288 |
||
289 |
txt{* |
|
290 |
Unfortunately, this attempt does not prove |
|
291 |
the induction step: |
|
292 |
@{subgoals[display,margin=70]} |
|
293 |
The induction hypothesis is too weak. The fixed |
|
294 |
argument,~@{term"[]"}, prevents it from rewriting the conclusion. |
|
295 |
This example suggests a heuristic: |
|
296 |
\begin{quote} |
|
47711 | 297 |
\emph{Generalize goals for induction by replacing constants by variables.} |
47269 | 298 |
\end{quote} |
299 |
Of course one cannot do this na\"{\i}vely: @{prop"itrev xs ys = rev xs"} is |
|
47711 | 300 |
just not true. The correct generalization is |
47269 | 301 |
*}; |
302 |
(*<*)oops;(*>*) |
|
303 |
lemma "itrev xs ys = rev xs @ ys" |
|
304 |
(*<*)apply(induction xs, auto)(*>*) |
|
305 |
txt{* |
|
306 |
If @{text ys} is replaced by @{term"[]"}, the right-hand side simplifies to |
|
307 |
@{term"rev xs"}, as required. |
|
47711 | 308 |
In this instance it was easy to guess the right generalization. |
47269 | 309 |
Other situations can require a good deal of creativity. |
310 |
||
311 |
Although we now have two variables, only @{text xs} is suitable for |
|
312 |
induction, and we repeat our proof attempt. Unfortunately, we are still |
|
313 |
not there: |
|
314 |
@{subgoals[display,margin=65]} |
|
315 |
The induction hypothesis is still too weak, but this time it takes no |
|
47711 | 316 |
intuition to generalize: the problem is that the @{text ys} |
47269 | 317 |
in the induction hypothesis is fixed, |
318 |
but the induction hypothesis needs to be applied with |
|
319 |
@{term"a # ys"} instead of @{text ys}. Hence we prove the theorem |
|
320 |
for all @{text ys} instead of a fixed one. We can instruct induction |
|
55361 | 321 |
to perform this generalization for us by adding @{text "arbitrary: ys"}\index{arbitrary@@{text"arbitrary:"}}. |
47269 | 322 |
*} |
323 |
(*<*)oops |
|
324 |
lemma "itrev xs ys = rev xs @ ys" |
|
325 |
(*>*) |
|
326 |
apply(induction xs arbitrary: ys) |
|
327 |
||
328 |
txt{* The induction hypothesis in the induction step is now universally quantified over @{text ys}: |
|
329 |
@{subgoals[display,margin=65]} |
|
330 |
Thus the proof succeeds: |
|
331 |
*} |
|
332 |
||
333 |
apply auto |
|
334 |
done |
|
335 |
||
336 |
text{* |
|
47711 | 337 |
This leads to another heuristic for generalization: |
47269 | 338 |
\begin{quote} |
47711 | 339 |
\emph{Generalize induction by generalizing all free |
47269 | 340 |
variables\\ {\em(except the induction variable itself)}.} |
341 |
\end{quote} |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset
|
342 |
Generalization is best performed with @{text"arbitrary: y\<^sub>1 \<dots> y\<^sub>k"}. |
47269 | 343 |
This heuristic prevents trivial failures like the one above. |
344 |
However, it should not be applied blindly. |
|
345 |
It is not always required, and the additional quantifiers can complicate |
|
346 |
matters in some cases. The variables that need to be quantified are typically |
|
347 |
those that change in recursive calls. |
|
348 |
||
54136 | 349 |
|
54436 | 350 |
\subsection*{Exercises} |
54136 | 351 |
|
352 |
\begin{exercise} |
|
353 |
Write a tail-recursive variant of the @{text add} function on @{typ nat}: |
|
354 |
@{term "itadd :: nat \<Rightarrow> nat \<Rightarrow> nat"}. |
|
355 |
Tail-recursive means that in the recursive case, @{text itadd} needs to call |
|
356 |
itself directly: \mbox{@{term"itadd (Suc m) n"}} @{text"= itadd \<dots>"}. |
|
357 |
Prove @{prop "itadd m n = add m n"}. |
|
358 |
\end{exercise} |
|
359 |
||
360 |
||
47269 | 361 |
\section{Simplification} |
362 |
||
55317 | 363 |
So far we have talked a lot about simplifying terms without explaining the concept. |
364 |
\conceptidx{Simplification}{simplification} means |
|
47269 | 365 |
\begin{itemize} |
366 |
\item using equations $l = r$ from left to right (only), |
|
367 |
\item as long as possible. |
|
368 |
\end{itemize} |
|
47711 | 369 |
To emphasize the directionality, equations that have been given the |
55317 | 370 |
@{text"simp"} attribute are called \conceptidx{simplification rules}{simplification rule}. |
371 |
Logically, they are still symmetric, but proofs by |
|
47269 | 372 |
simplification use them only in the left-to-right direction. The proof tool |
373 |
that performs simplifications is called the \concept{simplifier}. It is the |
|
374 |
basis of @{text auto} and other related proof methods. |
|
375 |
||
376 |
The idea of simplification is best explained by an example. Given the |
|
377 |
simplification rules |
|
378 |
\[ |
|
379 |
\begin{array}{rcl@ {\quad}l} |
|
380 |
@{term"0 + n::nat"} &@{text"="}& @{text n} & (1) \\ |
|
381 |
@{term"(Suc m) + n"} &@{text"="}& @{term"Suc (m + n)"} & (2) \\ |
|
382 |
@{text"(Suc m \<le> Suc n)"} &@{text"="}& @{text"(m \<le> n)"} & (3)\\ |
|
383 |
@{text"(0 \<le> m)"} &@{text"="}& @{const True} & (4) |
|
384 |
\end{array} |
|
385 |
\] |
|
386 |
the formula @{prop"0 + Suc 0 \<le> Suc 0 + x"} is simplified to @{const True} |
|
387 |
as follows: |
|
388 |
\[ |
|
389 |
\begin{array}{r@ {}c@ {}l@ {\quad}l} |
|
390 |
@{text"(0 + Suc 0"} & \leq & @{text"Suc 0 + x)"} & \stackrel{(1)}{=} \\ |
|
391 |
@{text"(Suc 0"} & \leq & @{text"Suc 0 + x)"} & \stackrel{(2)}{=} \\ |
|
392 |
@{text"(Suc 0"} & \leq & @{text"Suc (0 + x)"} & \stackrel{(3)}{=} \\ |
|
393 |
@{text"(0"} & \leq & @{text"0 + x)"} & \stackrel{(4)}{=} \\[1ex] |
|
394 |
& @{const True} |
|
395 |
\end{array} |
|
396 |
\] |
|
397 |
Simplification is often also called \concept{rewriting} |
|
55317 | 398 |
and simplification rules \conceptidx{rewrite rules}{rewrite rule}. |
47269 | 399 |
|
52361 | 400 |
\subsection{Simplification Rules} |
47269 | 401 |
|
402 |
The attribute @{text"simp"} declares theorems to be simplification rules, |
|
403 |
which the simplifier will use automatically. In addition, |
|
404 |
\isacom{datatype} and \isacom{fun} commands implicitly declare some |
|
405 |
simplification rules: \isacom{datatype} the distinctness and injectivity |
|
406 |
rules, \isacom{fun} the defining equations. Definitions are not declared |
|
407 |
as simplification rules automatically! Nearly any theorem can become a |
|
408 |
simplification rule. The simplifier will try to transform it into an |
|
409 |
equation. For example, the theorem @{prop"\<not> P"} is turned into @{prop"P = False"}. |
|
410 |
||
411 |
Only equations that really simplify, like @{prop"rev (rev xs) = xs"} and |
|
412 |
@{prop"xs @ [] = xs"}, should be declared as simplification |
|
413 |
rules. Equations that may be counterproductive as simplification rules |
|
414 |
should only be used in specific proof steps (see \S\ref{sec:simp} below). |
|
415 |
Distributivity laws, for example, alter the structure of terms |
|
416 |
and can produce an exponential blow-up. |
|
417 |
||
52361 | 418 |
\subsection{Conditional Simplification Rules} |
47269 | 419 |
|
420 |
Simplification rules can be conditional. Before applying such a rule, the |
|
421 |
simplifier will first try to prove the preconditions, again by |
|
422 |
simplification. For example, given the simplification rules |
|
423 |
\begin{quote} |
|
424 |
@{prop"p(0::nat) = True"}\\ |
|
425 |
@{prop"p(x) \<Longrightarrow> f(x) = g(x)"}, |
|
426 |
\end{quote} |
|
427 |
the term @{term"f(0::nat)"} simplifies to @{term"g(0::nat)"} |
|
428 |
but @{term"f(1::nat)"} does not simplify because @{prop"p(1::nat)"} |
|
429 |
is not provable. |
|
430 |
||
431 |
\subsection{Termination} |
|
432 |
||
433 |
Simplification can run forever, for example if both @{prop"f x = g x"} and |
|
434 |
@{prop"g(x) = f(x)"} are simplification rules. It is the user's |
|
435 |
responsibility not to include simplification rules that can lead to |
|
436 |
nontermination, either on their own or in combination with other |
|
437 |
simplification rules. The right-hand side of a simplification rule should |
|
438 |
always be ``simpler'' than the left-hand side---in some sense. But since |
|
439 |
termination is undecidable, such a check cannot be automated completely |
|
440 |
and Isabelle makes little attempt to detect nontermination. |
|
441 |
||
442 |
When conditional simplification rules are applied, their preconditions are |
|
443 |
proved first. Hence all preconditions need to be |
|
444 |
simpler than the left-hand side of the conclusion. For example |
|
445 |
\begin{quote} |
|
446 |
@{prop "n < m \<Longrightarrow> (n < Suc m) = True"} |
|
447 |
\end{quote} |
|
448 |
is suitable as a simplification rule: both @{prop"n<m"} and @{const True} |
|
449 |
are simpler than \mbox{@{prop"n < Suc m"}}. But |
|
450 |
\begin{quote} |
|
451 |
@{prop "Suc n < m \<Longrightarrow> (n < m) = True"} |
|
452 |
\end{quote} |
|
453 |
leads to nontermination: when trying to rewrite @{prop"n<m"} to @{const True} |
|
454 |
one first has to prove \mbox{@{prop"Suc n < m"}}, which can be rewritten to @{const True} provided @{prop"Suc(Suc n) < m"}, \emph{ad infinitum}. |
|
455 |
||
55348 | 456 |
\subsection{The \indexed{@{text simp}}{simp} Proof Method} |
47269 | 457 |
\label{sec:simp} |
458 |
||
459 |
So far we have only used the proof method @{text auto}. Method @{text simp} |
|
460 |
is the key component of @{text auto}, but @{text auto} can do much more. In |
|
461 |
some cases, @{text auto} is overeager and modifies the proof state too much. |
|
462 |
In such cases the more predictable @{text simp} method should be used. |
|
463 |
Given a goal |
|
464 |
\begin{quote} |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset
|
465 |
@{text"1. \<lbrakk> P\<^sub>1; \<dots>; P\<^sub>m \<rbrakk> \<Longrightarrow> C"} |
47269 | 466 |
\end{quote} |
467 |
the command |
|
468 |
\begin{quote} |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset
|
469 |
\isacom{apply}@{text"(simp add: th\<^sub>1 \<dots> th\<^sub>n)"} |
47269 | 470 |
\end{quote} |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset
|
471 |
simplifies the assumptions @{text "P\<^sub>i"} and the conclusion @{text C} using |
47269 | 472 |
\begin{itemize} |
473 |
\item all simplification rules, including the ones coming from \isacom{datatype} and \isacom{fun}, |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset
|
474 |
\item the additional lemmas @{text"th\<^sub>1 \<dots> th\<^sub>n"}, and |
47269 | 475 |
\item the assumptions. |
476 |
\end{itemize} |
|
477 |
In addition to or instead of @{text add} there is also @{text del} for removing |
|
478 |
simplification rules temporarily. Both are optional. Method @{text auto} |
|
479 |
can be modified similarly: |
|
480 |
\begin{quote} |
|
481 |
\isacom{apply}@{text"(auto simp add: \<dots> simp del: \<dots>)"} |
|
482 |
\end{quote} |
|
483 |
Here the modifiers are @{text"simp add"} and @{text"simp del"} |
|
484 |
instead of just @{text add} and @{text del} because @{text auto} |
|
485 |
does not just perform simplification. |
|
486 |
||
487 |
Note that @{text simp} acts only on subgoal 1, @{text auto} acts on all |
|
488 |
subgoals. There is also @{text simp_all}, which applies @{text simp} to |
|
489 |
all subgoals. |
|
490 |
||
56989 | 491 |
\subsection{Rewriting with Definitions} |
47269 | 492 |
\label{sec:rewr-defs} |
493 |
||
494 |
Definitions introduced by the command \isacom{definition} |
|
495 |
can also be used as simplification rules, |
|
496 |
but by default they are not: the simplifier does not expand them |
|
497 |
automatically. Definitions are intended for introducing abstract concepts and |
|
498 |
not merely as abbreviations. Of course, we need to expand the definition |
|
499 |
initially, but once we have proved enough abstract properties of the new |
|
500 |
constant, we can forget its original definition. This style makes proofs more |
|
501 |
robust: if the definition has to be changed, only the proofs of the abstract |
|
502 |
properties will be affected. |
|
503 |
||
504 |
The definition of a function @{text f} is a theorem named @{text f_def} |
|
505 |
and can be added to a call of @{text simp} just like any other theorem: |
|
506 |
\begin{quote} |
|
507 |
\isacom{apply}@{text"(simp add: f_def)"} |
|
508 |
\end{quote} |
|
509 |
In particular, let-expressions can be unfolded by |
|
510 |
making @{thm[source] Let_def} a simplification rule. |
|
511 |
||
52361 | 512 |
\subsection{Case Splitting With @{text simp}} |
47269 | 513 |
|
514 |
Goals containing if-expressions are automatically split into two cases by |
|
515 |
@{text simp} using the rule |
|
516 |
\begin{quote} |
|
517 |
@{prop"P(if A then s else t) = ((A \<longrightarrow> P(s)) \<and> (~A \<longrightarrow> P(t)))"} |
|
518 |
\end{quote} |
|
519 |
For example, @{text simp} can prove |
|
520 |
\begin{quote} |
|
521 |
@{prop"(A \<and> B) = (if A then B else False)"} |
|
522 |
\end{quote} |
|
523 |
because both @{prop"A \<longrightarrow> (A & B) = B"} and @{prop"~A \<longrightarrow> (A & B) = False"} |
|
524 |
simplify to @{const True}. |
|
525 |
||
526 |
We can split case-expressions similarly. For @{text nat} the rule looks like this: |
|
527 |
@{prop[display,margin=65,indent=4]"P(case e of 0 \<Rightarrow> a | Suc n \<Rightarrow> b n) = ((e = 0 \<longrightarrow> P a) & (ALL n. e = Suc n \<longrightarrow> P(b n)))"} |
|
528 |
Case expressions are not split automatically by @{text simp}, but @{text simp} |
|
529 |
can be instructed to do so: |
|
530 |
\begin{quote} |
|
531 |
\isacom{apply}@{text"(simp split: nat.split)"} |
|
532 |
\end{quote} |
|
533 |
splits all case-expressions over natural numbers. For an arbitrary |
|
55348 | 534 |
datatype @{text t} it is @{text "t.split"}\index{split@@{text".split"}} instead of @{thm[source] nat.split}. |
47269 | 535 |
Method @{text auto} can be modified in exactly the same way. |
55348 | 536 |
The modifier \indexed{@{text "split:"}}{split} can be followed by multiple names. |
54605 | 537 |
Splitting if or case-expressions in the assumptions requires |
538 |
@{text "split: if_splits"} or @{text "split: t.splits"}. |
|
52593 | 539 |
|
540 |
||
54436 | 541 |
\subsection*{Exercises} |
52593 | 542 |
|
54195 | 543 |
\exercise\label{exe:tree0} |
544 |
Define a datatype @{text tree0} of binary tree skeletons which do not store |
|
545 |
any information, neither in the inner nodes nor in the leaves. |
|
54467 | 546 |
Define a function @{text "nodes :: tree0 \<Rightarrow> nat"} that counts the number of |
54195 | 547 |
all nodes (inner nodes and leaves) in such a tree. |
548 |
Consider the following recursive function: |
|
549 |
*} |
|
550 |
(*<*) |
|
551 |
datatype tree0 = Tip | Node tree0 tree0 |
|
552 |
(*>*) |
|
553 |
fun explode :: "nat \<Rightarrow> tree0 \<Rightarrow> tree0" where |
|
554 |
"explode 0 t = t" | |
|
555 |
"explode (Suc n) t = explode n (Node t t)" |
|
556 |
||
557 |
text {* |
|
558 |
Find an equation expressing the size of a tree after exploding it |
|
559 |
(\noquotes{@{term [source] "nodes (explode n t)"}}) as a function |
|
560 |
of @{term "nodes t"} and @{text n}. Prove your equation. |
|
56989 | 561 |
You may use the usual arithmetic operators, including the exponentiation |
54195 | 562 |
operator ``@{text"^"}''. For example, \noquotes{@{prop [source] "2 ^ 2 = 4"}}. |
563 |
||
564 |
Hint: simplifying with the list of theorems @{thm[source] algebra_simps} |
|
565 |
takes care of common algebraic properties of the arithmetic operators. |
|
566 |
\endexercise |
|
567 |
||
52593 | 568 |
\exercise |
569 |
Define arithmetic expressions in one variable over integers (type @{typ int}) |
|
570 |
as a data type: |
|
571 |
*} |
|
572 |
||
573 |
datatype exp = Var | Const int | Add exp exp | Mult exp exp |
|
574 |
||
575 |
text{* |
|
576 |
Define a function \noquotes{@{term [source]"eval :: exp \<Rightarrow> int \<Rightarrow> int"}} |
|
577 |
such that @{term"eval e x"} evaluates @{text e} at the value |
|
578 |
@{text x}. |
|
579 |
||
580 |
A polynomial can be represented as a list of coefficients, starting with |
|
581 |
the constant. For example, @{term "[4, 2, -1, 3::int]"} represents the |
|
582 |
polynomial $4 + 2x - x^2 + 3x^3$. |
|
583 |
Define a function \noquotes{@{term [source] "evalp :: int list \<Rightarrow> int \<Rightarrow> int"}} |
|
584 |
that evaluates a polynomial at the given value. |
|
585 |
Define a function \noquotes{@{term[source] "coeffs :: exp \<Rightarrow> int list"}} |
|
586 |
that transforms an expression into a polynomial. This may require auxiliary |
|
587 |
functions. Prove that @{text coeffs} preserves the value of the expression: |
|
588 |
\mbox{@{prop"evalp (coeffs e) x = eval e x"}.} |
|
54467 | 589 |
Hint: consider the hint in Exercise~\ref{exe:tree0}. |
52593 | 590 |
\endexercise |
47269 | 591 |
*} |
592 |
(*<*) |
|
593 |
end |
|
594 |
(*>*) |