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