author | nipkow |
Fri, 07 Sep 2018 13:27:41 +0200 | |
changeset 68921 | 35ea237696cf |
parent 68919 | 027219002f32 |
child 69505 | cc2d676d5395 |
permissions | -rw-r--r-- |
47269 | 1 |
(*<*) |
2 |
theory Types_and_funs |
|
3 |
imports Main |
|
4 |
begin |
|
5 |
(*>*) |
|
67406 | 6 |
text\<open> |
47269 | 7 |
\vspace{-5ex} |
52361 | 8 |
\section{Type and Function Definitions} |
47269 | 9 |
|
10 |
Type synonyms are abbreviations for existing types, for example |
|
67406 | 11 |
\index{string@@{text string}}\<close> |
47269 | 12 |
|
13 |
type_synonym string = "char list" |
|
14 |
||
67406 | 15 |
text\<open> |
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 |
||
58605 | 49 |
Like in functional programming languages, datatype values can be taken apart |
50 |
with case expressions\index{case expression}\index{case expression@@{text "case ... of"}}, for example |
|
47269 | 51 |
\begin{quote} |
52 |
\noquotes{@{term[source] "(case xs of [] \<Rightarrow> 0 | x # _ \<Rightarrow> Suc x)"}} |
|
53 |
\end{quote} |
|
58605 | 54 |
Case expressions must be enclosed in parentheses. |
47269 | 55 |
|
58605 | 56 |
As an example of a datatype beyond @{typ nat} and @{text list}, consider binary trees: |
67406 | 57 |
\<close> |
47269 | 58 |
|
47306 | 59 |
datatype 'a tree = Tip | Node "'a tree" 'a "'a tree" |
47269 | 60 |
|
67406 | 61 |
text\<open>with a mirror function:\<close> |
47269 | 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 |
||
67406 | 67 |
text\<open>The following lemma illustrates induction:\<close> |
47269 | 68 |
|
69 |
lemma "mirror(mirror t) = t" |
|
70 |
apply(induction t) |
|
71 |
||
67406 | 72 |
txt\<open>yields |
47269 | 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: |
|
67406 | 84 |
\<close> |
47269 | 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 |
|
67406 | 93 |
text\<open> |
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: |
67406 | 104 |
\index{definition@\isacom{definition}}\<close> |
47269 | 105 |
|
106 |
definition sq :: "nat \<Rightarrow> nat" where |
|
107 |
"sq n = n * n" |
|
108 |
||
67406 | 109 |
text\<open>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: |
|
67406 | 115 |
\index{abbreviation@\isacom{abbreviation}}\<close> |
47269 | 116 |
|
117 |
abbreviation sq' :: "nat \<Rightarrow> nat" where |
|
52045 | 118 |
"sq' n \<equiv> n * n" |
47269 | 119 |
|
67406 | 120 |
text\<open>The key difference is that @{const sq'} is only syntactic sugar: |
58521 | 121 |
after parsing, @{term"sq' t"} is replaced by \mbox{@{term"t*t"}}; |
52045 | 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 |
58602 | 139 |
total. This simplifies the logic --- terms are always defined --- but means |
47269 | 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 |
|
58504 | 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 |
58620 | 151 |
see~@{cite Krauss}. |
47269 | 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, |
|
67406 | 156 |
\<close> |
47269 | 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 |
||
67406 | 163 |
text\<open>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, |
67406 | 173 |
\<close> |
47269 | 174 |
|
54571 | 175 |
lemma "div2(n) = n div 2" |
47269 | 176 |
apply(induction n rule: div2.induct) |
177 |
||
67406 | 178 |
txt\<open>(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. |
|
64862 | 221 |
Then define a function @{text "sum_tree ::"} @{typ "nat tree \<Rightarrow> nat"} |
54194 | 222 |
that sums up all values in a tree of natural numbers |
64862 | 223 |
and prove @{prop "sum_tree t = sum_list(contents t)"} |
224 |
(where @{const sum_list} is predefined). |
|
54194 | 225 |
\end{exercise} |
226 |
||
227 |
\begin{exercise} |
|
228 |
Define a new type @{text "'a tree2"} of binary trees where values are also |
|
229 |
stored in the leaves of the tree. Also reformulate the |
|
230 |
@{const mirror} function accordingly. Define two functions |
|
231 |
@{text "pre_order"} and @{text "post_order"} of type @{text "'a tree2 \<Rightarrow> 'a list"} |
|
232 |
that traverse a tree and collect all stored values in the respective order in |
|
233 |
a list. Prove @{prop "pre_order (mirror t) = rev (post_order t)"}. |
|
234 |
\end{exercise} |
|
235 |
||
236 |
\begin{exercise} |
|
54571 | 237 |
Define a function @{text "intersperse ::"} @{typ "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"} |
238 |
such that @{text "intersperse a [x\<^sub>1, ..., x\<^sub>n] = [x\<^sub>1, a, x\<^sub>2, a, ..., a, x\<^sub>n]"}. |
|
239 |
Now prove that @{prop "map f (intersperse a xs) = intersperse (f a) (map f xs)"}. |
|
54136 | 240 |
\end{exercise} |
241 |
||
242 |
||
55348 | 243 |
\section{Induction Heuristics}\index{induction heuristics} |
47269 | 244 |
|
245 |
We have already noted that theorems about recursive functions are proved by |
|
246 |
induction. In case the function has more than one argument, we have followed |
|
247 |
the following heuristic in the proofs about the append function: |
|
248 |
\begin{quote} |
|
249 |
\emph{Perform induction on argument number $i$\\ |
|
250 |
if the function is defined by recursion on argument number $i$.} |
|
251 |
\end{quote} |
|
252 |
The key heuristic, and the main point of this section, is to |
|
58502 | 253 |
\emph{generalize the goal before induction}. |
47269 | 254 |
The reason is simple: if the goal is |
255 |
too specific, the induction hypothesis is too weak to allow the induction |
|
256 |
step to go through. Let us illustrate the idea with an example. |
|
257 |
||
258 |
Function @{const rev} has quadratic worst-case running time |
|
259 |
because it calls append for each element of the list and |
|
260 |
append is linear in its first argument. A linear time version of |
|
261 |
@{const rev} requires an extra argument where the result is accumulated |
|
262 |
gradually, using only~@{text"#"}: |
|
67406 | 263 |
\<close> |
47269 | 264 |
(*<*) |
265 |
apply auto |
|
266 |
done |
|
267 |
(*>*) |
|
268 |
fun itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where |
|
47711 | 269 |
"itrev [] ys = ys" | |
47269 | 270 |
"itrev (x#xs) ys = itrev xs (x#ys)" |
271 |
||
67406 | 272 |
text\<open>The behaviour of @{const itrev} is simple: it reverses |
47269 | 273 |
its first argument by stacking its elements onto the second argument, |
47711 | 274 |
and it returns that second argument when the first one becomes |
47269 | 275 |
empty. Note that @{const itrev} is tail-recursive: it can be |
56989 | 276 |
compiled into a loop; no stack is necessary for executing it. |
47269 | 277 |
|
278 |
Naturally, we would like to show that @{const itrev} does indeed reverse |
|
279 |
its first argument provided the second one is empty: |
|
67406 | 280 |
\<close> |
47269 | 281 |
|
282 |
lemma "itrev xs [] = rev xs" |
|
283 |
||
67406 | 284 |
txt\<open>There is no choice as to the induction variable: |
285 |
\<close> |
|
47269 | 286 |
|
287 |
apply(induction xs) |
|
288 |
apply(auto) |
|
289 |
||
67406 | 290 |
txt\<open> |
47269 | 291 |
Unfortunately, this attempt does not prove |
292 |
the induction step: |
|
293 |
@{subgoals[display,margin=70]} |
|
294 |
The induction hypothesis is too weak. The fixed |
|
295 |
argument,~@{term"[]"}, prevents it from rewriting the conclusion. |
|
296 |
This example suggests a heuristic: |
|
297 |
\begin{quote} |
|
58502 | 298 |
\emph{Generalize goals for induction by replacing constants by variables.} |
47269 | 299 |
\end{quote} |
58519 | 300 |
Of course one cannot do this naively: @{prop"itrev xs ys = rev xs"} is |
58502 | 301 |
just not true. The correct generalization is |
67406 | 302 |
\<close> |
58860 | 303 |
(*<*)oops(*>*) |
47269 | 304 |
lemma "itrev xs ys = rev xs @ ys" |
305 |
(*<*)apply(induction xs, auto)(*>*) |
|
67406 | 306 |
txt\<open> |
47269 | 307 |
If @{text ys} is replaced by @{term"[]"}, the right-hand side simplifies to |
308 |
@{term"rev xs"}, as required. |
|
58502 | 309 |
In this instance it was easy to guess the right generalization. |
47269 | 310 |
Other situations can require a good deal of creativity. |
311 |
||
312 |
Although we now have two variables, only @{text xs} is suitable for |
|
313 |
induction, and we repeat our proof attempt. Unfortunately, we are still |
|
314 |
not there: |
|
315 |
@{subgoals[display,margin=65]} |
|
316 |
The induction hypothesis is still too weak, but this time it takes no |
|
58502 | 317 |
intuition to generalize: the problem is that the @{text ys} |
47269 | 318 |
in the induction hypothesis is fixed, |
319 |
but the induction hypothesis needs to be applied with |
|
320 |
@{term"a # ys"} instead of @{text ys}. Hence we prove the theorem |
|
321 |
for all @{text ys} instead of a fixed one. We can instruct induction |
|
58502 | 322 |
to perform this generalization for us by adding @{text "arbitrary: ys"}\index{arbitrary@@{text"arbitrary:"}}. |
67406 | 323 |
\<close> |
47269 | 324 |
(*<*)oops |
325 |
lemma "itrev xs ys = rev xs @ ys" |
|
326 |
(*>*) |
|
327 |
apply(induction xs arbitrary: ys) |
|
328 |
||
67406 | 329 |
txt\<open>The induction hypothesis in the induction step is now universally quantified over @{text ys}: |
47269 | 330 |
@{subgoals[display,margin=65]} |
331 |
Thus the proof succeeds: |
|
67406 | 332 |
\<close> |
47269 | 333 |
|
334 |
apply auto |
|
335 |
done |
|
336 |
||
67406 | 337 |
text\<open> |
58502 | 338 |
This leads to another heuristic for generalization: |
47269 | 339 |
\begin{quote} |
58502 | 340 |
\emph{Generalize induction by generalizing all free |
47269 | 341 |
variables\\ {\em(except the induction variable itself)}.} |
342 |
\end{quote} |
|
58502 | 343 |
Generalization is best performed with @{text"arbitrary: y\<^sub>1 \<dots> y\<^sub>k"}. |
47269 | 344 |
This heuristic prevents trivial failures like the one above. |
345 |
However, it should not be applied blindly. |
|
346 |
It is not always required, and the additional quantifiers can complicate |
|
347 |
matters in some cases. The variables that need to be quantified are typically |
|
348 |
those that change in recursive calls. |
|
349 |
||
54136 | 350 |
|
54436 | 351 |
\subsection*{Exercises} |
54136 | 352 |
|
353 |
\begin{exercise} |
|
354 |
Write a tail-recursive variant of the @{text add} function on @{typ nat}: |
|
355 |
@{term "itadd :: nat \<Rightarrow> nat \<Rightarrow> nat"}. |
|
356 |
Tail-recursive means that in the recursive case, @{text itadd} needs to call |
|
357 |
itself directly: \mbox{@{term"itadd (Suc m) n"}} @{text"= itadd \<dots>"}. |
|
358 |
Prove @{prop "itadd m n = add m n"}. |
|
359 |
\end{exercise} |
|
360 |
||
361 |
||
47269 | 362 |
\section{Simplification} |
363 |
||
55317 | 364 |
So far we have talked a lot about simplifying terms without explaining the concept. |
365 |
\conceptidx{Simplification}{simplification} means |
|
47269 | 366 |
\begin{itemize} |
367 |
\item using equations $l = r$ from left to right (only), |
|
368 |
\item as long as possible. |
|
369 |
\end{itemize} |
|
47711 | 370 |
To emphasize the directionality, equations that have been given the |
55317 | 371 |
@{text"simp"} attribute are called \conceptidx{simplification rules}{simplification rule}. |
372 |
Logically, they are still symmetric, but proofs by |
|
47269 | 373 |
simplification use them only in the left-to-right direction. The proof tool |
374 |
that performs simplifications is called the \concept{simplifier}. It is the |
|
375 |
basis of @{text auto} and other related proof methods. |
|
376 |
||
377 |
The idea of simplification is best explained by an example. Given the |
|
378 |
simplification rules |
|
379 |
\[ |
|
380 |
\begin{array}{rcl@ {\quad}l} |
|
381 |
@{term"0 + n::nat"} &@{text"="}& @{text n} & (1) \\ |
|
382 |
@{term"(Suc m) + n"} &@{text"="}& @{term"Suc (m + n)"} & (2) \\ |
|
383 |
@{text"(Suc m \<le> Suc n)"} &@{text"="}& @{text"(m \<le> n)"} & (3)\\ |
|
384 |
@{text"(0 \<le> m)"} &@{text"="}& @{const True} & (4) |
|
385 |
\end{array} |
|
386 |
\] |
|
387 |
the formula @{prop"0 + Suc 0 \<le> Suc 0 + x"} is simplified to @{const True} |
|
388 |
as follows: |
|
389 |
\[ |
|
390 |
\begin{array}{r@ {}c@ {}l@ {\quad}l} |
|
391 |
@{text"(0 + Suc 0"} & \leq & @{text"Suc 0 + x)"} & \stackrel{(1)}{=} \\ |
|
392 |
@{text"(Suc 0"} & \leq & @{text"Suc 0 + x)"} & \stackrel{(2)}{=} \\ |
|
57817 | 393 |
@{text"(Suc 0"} & \leq & @{text"Suc (0 + x))"} & \stackrel{(3)}{=} \\ |
47269 | 394 |
@{text"(0"} & \leq & @{text"0 + x)"} & \stackrel{(4)}{=} \\[1ex] |
395 |
& @{const True} |
|
396 |
\end{array} |
|
397 |
\] |
|
398 |
Simplification is often also called \concept{rewriting} |
|
55317 | 399 |
and simplification rules \conceptidx{rewrite rules}{rewrite rule}. |
47269 | 400 |
|
52361 | 401 |
\subsection{Simplification Rules} |
47269 | 402 |
|
403 |
The attribute @{text"simp"} declares theorems to be simplification rules, |
|
404 |
which the simplifier will use automatically. In addition, |
|
405 |
\isacom{datatype} and \isacom{fun} commands implicitly declare some |
|
406 |
simplification rules: \isacom{datatype} the distinctness and injectivity |
|
407 |
rules, \isacom{fun} the defining equations. Definitions are not declared |
|
408 |
as simplification rules automatically! Nearly any theorem can become a |
|
409 |
simplification rule. The simplifier will try to transform it into an |
|
410 |
equation. For example, the theorem @{prop"\<not> P"} is turned into @{prop"P = False"}. |
|
411 |
||
412 |
Only equations that really simplify, like @{prop"rev (rev xs) = xs"} and |
|
413 |
@{prop"xs @ [] = xs"}, should be declared as simplification |
|
414 |
rules. Equations that may be counterproductive as simplification rules |
|
58521 | 415 |
should only be used in specific proof steps (see \autoref{sec:simp} below). |
47269 | 416 |
Distributivity laws, for example, alter the structure of terms |
417 |
and can produce an exponential blow-up. |
|
418 |
||
52361 | 419 |
\subsection{Conditional Simplification Rules} |
47269 | 420 |
|
421 |
Simplification rules can be conditional. Before applying such a rule, the |
|
422 |
simplifier will first try to prove the preconditions, again by |
|
423 |
simplification. For example, given the simplification rules |
|
424 |
\begin{quote} |
|
425 |
@{prop"p(0::nat) = True"}\\ |
|
426 |
@{prop"p(x) \<Longrightarrow> f(x) = g(x)"}, |
|
427 |
\end{quote} |
|
428 |
the term @{term"f(0::nat)"} simplifies to @{term"g(0::nat)"} |
|
429 |
but @{term"f(1::nat)"} does not simplify because @{prop"p(1::nat)"} |
|
430 |
is not provable. |
|
431 |
||
432 |
\subsection{Termination} |
|
433 |
||
434 |
Simplification can run forever, for example if both @{prop"f x = g x"} and |
|
435 |
@{prop"g(x) = f(x)"} are simplification rules. It is the user's |
|
436 |
responsibility not to include simplification rules that can lead to |
|
437 |
nontermination, either on their own or in combination with other |
|
438 |
simplification rules. The right-hand side of a simplification rule should |
|
58602 | 439 |
always be ``simpler'' than the left-hand side --- in some sense. But since |
47269 | 440 |
termination is undecidable, such a check cannot be automated completely |
441 |
and Isabelle makes little attempt to detect nontermination. |
|
442 |
||
443 |
When conditional simplification rules are applied, their preconditions are |
|
444 |
proved first. Hence all preconditions need to be |
|
445 |
simpler than the left-hand side of the conclusion. For example |
|
446 |
\begin{quote} |
|
447 |
@{prop "n < m \<Longrightarrow> (n < Suc m) = True"} |
|
448 |
\end{quote} |
|
449 |
is suitable as a simplification rule: both @{prop"n<m"} and @{const True} |
|
450 |
are simpler than \mbox{@{prop"n < Suc m"}}. But |
|
451 |
\begin{quote} |
|
452 |
@{prop "Suc n < m \<Longrightarrow> (n < m) = True"} |
|
453 |
\end{quote} |
|
454 |
leads to nontermination: when trying to rewrite @{prop"n<m"} to @{const True} |
|
455 |
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}. |
|
456 |
||
55348 | 457 |
\subsection{The \indexed{@{text simp}}{simp} Proof Method} |
47269 | 458 |
\label{sec:simp} |
459 |
||
460 |
So far we have only used the proof method @{text auto}. Method @{text simp} |
|
461 |
is the key component of @{text auto}, but @{text auto} can do much more. In |
|
462 |
some cases, @{text auto} is overeager and modifies the proof state too much. |
|
463 |
In such cases the more predictable @{text simp} method should be used. |
|
464 |
Given a goal |
|
465 |
\begin{quote} |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset
|
466 |
@{text"1. \<lbrakk> P\<^sub>1; \<dots>; P\<^sub>m \<rbrakk> \<Longrightarrow> C"} |
47269 | 467 |
\end{quote} |
468 |
the command |
|
469 |
\begin{quote} |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset
|
470 |
\isacom{apply}@{text"(simp add: th\<^sub>1 \<dots> th\<^sub>n)"} |
47269 | 471 |
\end{quote} |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset
|
472 |
simplifies the assumptions @{text "P\<^sub>i"} and the conclusion @{text C} using |
47269 | 473 |
\begin{itemize} |
474 |
\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
|
475 |
\item the additional lemmas @{text"th\<^sub>1 \<dots> th\<^sub>n"}, and |
47269 | 476 |
\item the assumptions. |
477 |
\end{itemize} |
|
478 |
In addition to or instead of @{text add} there is also @{text del} for removing |
|
479 |
simplification rules temporarily. Both are optional. Method @{text auto} |
|
480 |
can be modified similarly: |
|
481 |
\begin{quote} |
|
482 |
\isacom{apply}@{text"(auto simp add: \<dots> simp del: \<dots>)"} |
|
483 |
\end{quote} |
|
484 |
Here the modifiers are @{text"simp add"} and @{text"simp del"} |
|
485 |
instead of just @{text add} and @{text del} because @{text auto} |
|
486 |
does not just perform simplification. |
|
487 |
||
488 |
Note that @{text simp} acts only on subgoal 1, @{text auto} acts on all |
|
489 |
subgoals. There is also @{text simp_all}, which applies @{text simp} to |
|
490 |
all subgoals. |
|
491 |
||
56989 | 492 |
\subsection{Rewriting with Definitions} |
47269 | 493 |
\label{sec:rewr-defs} |
494 |
||
495 |
Definitions introduced by the command \isacom{definition} |
|
496 |
can also be used as simplification rules, |
|
497 |
but by default they are not: the simplifier does not expand them |
|
498 |
automatically. Definitions are intended for introducing abstract concepts and |
|
499 |
not merely as abbreviations. Of course, we need to expand the definition |
|
500 |
initially, but once we have proved enough abstract properties of the new |
|
501 |
constant, we can forget its original definition. This style makes proofs more |
|
502 |
robust: if the definition has to be changed, only the proofs of the abstract |
|
503 |
properties will be affected. |
|
504 |
||
505 |
The definition of a function @{text f} is a theorem named @{text f_def} |
|
58605 | 506 |
and can be added to a call of @{text simp} like any other theorem: |
47269 | 507 |
\begin{quote} |
508 |
\isacom{apply}@{text"(simp add: f_def)"} |
|
509 |
\end{quote} |
|
510 |
In particular, let-expressions can be unfolded by |
|
511 |
making @{thm[source] Let_def} a simplification rule. |
|
512 |
||
52361 | 513 |
\subsection{Case Splitting With @{text simp}} |
47269 | 514 |
|
515 |
Goals containing if-expressions are automatically split into two cases by |
|
516 |
@{text simp} using the rule |
|
517 |
\begin{quote} |
|
518 |
@{prop"P(if A then s else t) = ((A \<longrightarrow> P(s)) \<and> (~A \<longrightarrow> P(t)))"} |
|
519 |
\end{quote} |
|
520 |
For example, @{text simp} can prove |
|
521 |
\begin{quote} |
|
522 |
@{prop"(A \<and> B) = (if A then B else False)"} |
|
523 |
\end{quote} |
|
524 |
because both @{prop"A \<longrightarrow> (A & B) = B"} and @{prop"~A \<longrightarrow> (A & B) = False"} |
|
525 |
simplify to @{const True}. |
|
526 |
||
527 |
We can split case-expressions similarly. For @{text nat} the rule looks like this: |
|
67613 | 528 |
@{prop[display,margin=65,indent=4]"P(case e of 0 \<Rightarrow> a | Suc n \<Rightarrow> b n) = ((e = 0 \<longrightarrow> P a) \<and> (\<forall>n. e = Suc n \<longrightarrow> P(b n)))"} |
47269 | 529 |
Case expressions are not split automatically by @{text simp}, but @{text simp} |
530 |
can be instructed to do so: |
|
531 |
\begin{quote} |
|
532 |
\isacom{apply}@{text"(simp split: nat.split)"} |
|
533 |
\end{quote} |
|
534 |
splits all case-expressions over natural numbers. For an arbitrary |
|
55348 | 535 |
datatype @{text t} it is @{text "t.split"}\index{split@@{text".split"}} instead of @{thm[source] nat.split}. |
47269 | 536 |
Method @{text auto} can be modified in exactly the same way. |
55348 | 537 |
The modifier \indexed{@{text "split:"}}{split} can be followed by multiple names. |
54605 | 538 |
Splitting if or case-expressions in the assumptions requires |
539 |
@{text "split: if_splits"} or @{text "split: t.splits"}. |
|
52593 | 540 |
|
68919 | 541 |
\ifsem\else |
68921 | 542 |
\subsection{Rewriting \<open>let\<close> and Numerals} |
543 |
||
544 |
Let-expressions (@{term "let x = s in t"}) can be expanded explicitly with the simplification rule |
|
545 |
@{thm[source] Let_def}. The simplifier will not expand \<open>let\<close>s automatically in many cases. |
|
68919 | 546 |
|
68921 | 547 |
Numerals of type @{typ nat} can be converted to @{const Suc} terms with the simplification rule |
548 |
@{thm[source] numeral_eq_Suc}. This is required, for example, when a function that is defined |
|
549 |
by pattern matching with @{const Suc} is applied to a numeral: if \<open>f\<close> is defined by |
|
550 |
@{text "f 0 = ..."} and @{text "f (Suc n) = ..."}, the simplifier cannot simplify \<open>f 2\<close> unless |
|
551 |
\<open>2\<close> is converted to @{term "Suc(Suc 0)"} (via @{thm[source] numeral_eq_Suc}). |
|
68919 | 552 |
\fi |
52593 | 553 |
|
54436 | 554 |
\subsection*{Exercises} |
52593 | 555 |
|
54195 | 556 |
\exercise\label{exe:tree0} |
557 |
Define a datatype @{text tree0} of binary tree skeletons which do not store |
|
558 |
any information, neither in the inner nodes nor in the leaves. |
|
54467 | 559 |
Define a function @{text "nodes :: tree0 \<Rightarrow> nat"} that counts the number of |
54195 | 560 |
all nodes (inner nodes and leaves) in such a tree. |
561 |
Consider the following recursive function: |
|
67406 | 562 |
\<close> |
54195 | 563 |
(*<*) |
564 |
datatype tree0 = Tip | Node tree0 tree0 |
|
565 |
(*>*) |
|
566 |
fun explode :: "nat \<Rightarrow> tree0 \<Rightarrow> tree0" where |
|
567 |
"explode 0 t = t" | |
|
568 |
"explode (Suc n) t = explode n (Node t t)" |
|
569 |
||
67406 | 570 |
text \<open> |
54195 | 571 |
Find an equation expressing the size of a tree after exploding it |
572 |
(\noquotes{@{term [source] "nodes (explode n t)"}}) as a function |
|
573 |
of @{term "nodes t"} and @{text n}. Prove your equation. |
|
56989 | 574 |
You may use the usual arithmetic operators, including the exponentiation |
54195 | 575 |
operator ``@{text"^"}''. For example, \noquotes{@{prop [source] "2 ^ 2 = 4"}}. |
576 |
||
577 |
Hint: simplifying with the list of theorems @{thm[source] algebra_simps} |
|
578 |
takes care of common algebraic properties of the arithmetic operators. |
|
579 |
\endexercise |
|
580 |
||
52593 | 581 |
\exercise |
582 |
Define arithmetic expressions in one variable over integers (type @{typ int}) |
|
583 |
as a data type: |
|
67406 | 584 |
\<close> |
52593 | 585 |
|
586 |
datatype exp = Var | Const int | Add exp exp | Mult exp exp |
|
587 |
||
67406 | 588 |
text\<open> |
52593 | 589 |
Define a function \noquotes{@{term [source]"eval :: exp \<Rightarrow> int \<Rightarrow> int"}} |
590 |
such that @{term"eval e x"} evaluates @{text e} at the value |
|
591 |
@{text x}. |
|
592 |
||
593 |
A polynomial can be represented as a list of coefficients, starting with |
|
594 |
the constant. For example, @{term "[4, 2, -1, 3::int]"} represents the |
|
595 |
polynomial $4 + 2x - x^2 + 3x^3$. |
|
596 |
Define a function \noquotes{@{term [source] "evalp :: int list \<Rightarrow> int \<Rightarrow> int"}} |
|
597 |
that evaluates a polynomial at the given value. |
|
598 |
Define a function \noquotes{@{term[source] "coeffs :: exp \<Rightarrow> int list"}} |
|
599 |
that transforms an expression into a polynomial. This may require auxiliary |
|
600 |
functions. Prove that @{text coeffs} preserves the value of the expression: |
|
601 |
\mbox{@{prop"evalp (coeffs e) x = eval e x"}.} |
|
54467 | 602 |
Hint: consider the hint in Exercise~\ref{exe:tree0}. |
52593 | 603 |
\endexercise |
67406 | 604 |
\<close> |
47269 | 605 |
(*<*) |
606 |
end |
|
607 |
(*>*) |