|
1 (*<*) |
|
2 theory Bool_nat_list |
|
3 imports Main |
|
4 begin |
|
5 (*>*) |
|
6 |
|
7 text{* |
|
8 \vspace{-4ex} |
|
9 \section{\texorpdfstring{Types @{typ bool}, @{typ nat} and @{text list}}{Types bool, nat and list}} |
|
10 |
|
11 These are the most important predefined types. We go through them one by one. |
|
12 Based on examples we learn how to define (possibly recursive) functions and |
|
13 prove theorems about them by induction and simplification. |
|
14 |
|
15 \subsection{Type \indexed{@{typ bool}}{bool}} |
|
16 |
|
17 The type of boolean values is a predefined datatype |
|
18 @{datatype[display] bool} |
|
19 with the two values \indexed{@{const True}}{True} and \indexed{@{const False}}{False} and |
|
20 with many predefined functions: @{text "\<not>"}, @{text "\<and>"}, @{text "\<or>"}, @{text |
|
21 "\<longrightarrow>"} etc. Here is how conjunction could be defined by pattern matching: |
|
22 *} |
|
23 |
|
24 fun conj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where |
|
25 "conj True True = True" | |
|
26 "conj _ _ = False" |
|
27 |
|
28 text{* Both the datatype and function definitions roughly follow the syntax |
|
29 of functional programming languages. |
|
30 |
|
31 \subsection{Type \indexed{@{typ nat}}{nat}} |
|
32 |
|
33 Natural numbers are another predefined datatype: |
|
34 @{datatype[display] nat}\index{Suc@@{const Suc}} |
|
35 All values of type @{typ nat} are generated by the constructors |
|
36 @{text 0} and @{const Suc}. Thus the values of type @{typ nat} are |
|
37 @{text 0}, @{term"Suc 0"}, @{term"Suc(Suc 0)"} etc. |
|
38 There are many predefined functions: @{text "+"}, @{text "*"}, @{text |
|
39 "\<le>"}, etc. Here is how you could define your own addition: |
|
40 *} |
|
41 |
|
42 fun add :: "nat \<Rightarrow> nat \<Rightarrow> nat" where |
|
43 "add 0 n = n" | |
|
44 "add (Suc m) n = Suc(add m n)" |
|
45 |
|
46 text{* And here is a proof of the fact that @{prop"add m 0 = m"}: *} |
|
47 |
|
48 lemma add_02: "add m 0 = m" |
|
49 apply(induction m) |
|
50 apply(auto) |
|
51 done |
|
52 (*<*) |
|
53 lemma "add m 0 = m" |
|
54 apply(induction m) |
|
55 (*>*) |
|
56 txt{* The \isacom{lemma} command starts the proof and gives the lemma |
|
57 a name, @{text add_02}. Properties of recursively defined functions |
|
58 need to be established by induction in most cases. |
|
59 Command \isacom{apply}@{text"(induction m)"} instructs Isabelle to |
|
60 start a proof by induction on @{text m}. In response, it will show the |
|
61 following proof state: |
|
62 @{subgoals[display,indent=0]} |
|
63 The numbered lines are known as \emph{subgoals}. |
|
64 The first subgoal is the base case, the second one the induction step. |
|
65 The prefix @{text"\<And>m."} is Isabelle's way of saying ``for an arbitrary but fixed @{text m}''. The @{text"\<Longrightarrow>"} separates assumptions from the conclusion. |
|
66 The command \isacom{apply}@{text"(auto)"} instructs Isabelle to try |
|
67 and prove all subgoals automatically, essentially by simplifying them. |
|
68 Because both subgoals are easy, Isabelle can do it. |
|
69 The base case @{prop"add 0 0 = 0"} holds by definition of @{const add}, |
|
70 and the induction step is almost as simple: |
|
71 @{text"add\<^raw:~>(Suc m) 0 = Suc(add m 0) = Suc m"} |
|
72 using first the definition of @{const add} and then the induction hypothesis. |
|
73 In summary, both subproofs rely on simplification with function definitions and |
|
74 the induction hypothesis. |
|
75 As a result of that final \isacom{done}, Isabelle associates the lemma |
|
76 just proved with its name. You can now inspect the lemma with the command |
|
77 *} |
|
78 |
|
79 thm add_02 |
|
80 |
|
81 txt{* which displays @{thm[show_question_marks,display] add_02} The free |
|
82 variable @{text m} has been replaced by the \concept{unknown} |
|
83 @{text"?m"}. There is no logical difference between the two but an |
|
84 operational one: unknowns can be instantiated, which is what you want after |
|
85 some lemma has been proved. |
|
86 |
|
87 Note that there is also a proof method @{text induct}, which behaves almost |
|
88 like @{text induction}; the difference is explained in \autoref{ch:Isar}. |
|
89 |
|
90 \begin{warn} |
|
91 Terminology: We use \concept{lemma}, \concept{theorem} and \concept{rule} |
|
92 interchangeably for propositions that have been proved. |
|
93 \end{warn} |
|
94 \begin{warn} |
|
95 Numerals (@{text 0}, @{text 1}, @{text 2}, \dots) and most of the standard |
|
96 arithmetic operations (@{text "+"}, @{text "-"}, @{text "*"}, @{text"\<le>"}, |
|
97 @{text"<"} etc) are overloaded: they are available |
|
98 not just for natural numbers but for other types as well. |
|
99 For example, given the goal @{text"x + 0 = x"}, there is nothing to indicate |
|
100 that you are talking about natural numbers. Hence Isabelle can only infer |
|
101 that @{term x} is of some arbitrary type where @{text 0} and @{text"+"} |
|
102 exist. As a consequence, you will be unable to prove the goal. |
|
103 % To alert you to such pitfalls, Isabelle flags numerals without a |
|
104 % fixed type in its output: @ {prop"x+0 = x"}. |
|
105 In this particular example, you need to include |
|
106 an explicit type constraint, for example @{text"x+0 = (x::nat)"}. If there |
|
107 is enough contextual information this may not be necessary: @{prop"Suc x = |
|
108 x"} automatically implies @{text"x::nat"} because @{term Suc} is not |
|
109 overloaded. |
|
110 \end{warn} |
|
111 |
|
112 \subsubsection{An Informal Proof} |
|
113 |
|
114 Above we gave some terse informal explanation of the proof of |
|
115 @{prop"add m 0 = m"}. A more detailed informal exposition of the lemma |
|
116 might look like this: |
|
117 \bigskip |
|
118 |
|
119 \noindent |
|
120 \textbf{Lemma} @{prop"add m 0 = m"} |
|
121 |
|
122 \noindent |
|
123 \textbf{Proof} by induction on @{text m}. |
|
124 \begin{itemize} |
|
125 \item Case @{text 0} (the base case): @{prop"add 0 0 = 0"} |
|
126 holds by definition of @{const add}. |
|
127 \item Case @{term"Suc m"} (the induction step): |
|
128 We assume @{prop"add m 0 = m"}, the induction hypothesis (IH), |
|
129 and we need to show @{text"add (Suc m) 0 = Suc m"}. |
|
130 The proof is as follows:\smallskip |
|
131 |
|
132 \begin{tabular}{@ {}rcl@ {\quad}l@ {}} |
|
133 @{term "add (Suc m) 0"} &@{text"="}& @{term"Suc(add m 0)"} |
|
134 & by definition of @{text add}\\ |
|
135 &@{text"="}& @{term "Suc m"} & by IH |
|
136 \end{tabular} |
|
137 \end{itemize} |
|
138 Throughout this book, \concept{IH} will stand for ``induction hypothesis''. |
|
139 |
|
140 We have now seen three proofs of @{prop"add m 0 = 0"}: the Isabelle one, the |
|
141 terse four lines explaining the base case and the induction step, and just now a |
|
142 model of a traditional inductive proof. The three proofs differ in the level |
|
143 of detail given and the intended reader: the Isabelle proof is for the |
|
144 machine, the informal proofs are for humans. Although this book concentrates |
|
145 on Isabelle proofs, it is important to be able to rephrase those proofs |
|
146 as informal text comprehensible to a reader familiar with traditional |
|
147 mathematical proofs. Later on we will introduce an Isabelle proof language |
|
148 that is closer to traditional informal mathematical language and is often |
|
149 directly readable. |
|
150 |
|
151 \subsection{Type \indexed{@{text list}}{list}} |
|
152 |
|
153 Although lists are already predefined, we define our own copy just for |
|
154 demonstration purposes: |
|
155 *} |
|
156 (*<*) |
|
157 apply(auto) |
|
158 done |
|
159 declare [[names_short]] |
|
160 (*>*) |
|
161 datatype 'a list = Nil | Cons 'a "'a list" |
|
162 |
|
163 text{* |
|
164 \begin{itemize} |
|
165 \item Type @{typ "'a list"} is the type of lists over elements of type @{typ 'a}. Because @{typ 'a} is a type variable, lists are in fact \concept{polymorphic}: the elements of a list can be of arbitrary type (but must all be of the same type). |
|
166 \item Lists have two constructors: @{const Nil}, the empty list, and @{const Cons}, which puts an element (of type @{typ 'a}) in front of a list (of type @{typ "'a list"}). |
|
167 Hence all lists are of the form @{const Nil}, or @{term"Cons x Nil"}, |
|
168 or @{term"Cons x (Cons y Nil)"} etc. |
|
169 \item \isacom{datatype} requires no quotation marks on the |
|
170 left-hand side, but on the right-hand side each of the argument |
|
171 types of a constructor needs to be enclosed in quotation marks, unless |
|
172 it is just an identifier (e.g.\ @{typ nat} or @{typ 'a}). |
|
173 \end{itemize} |
|
174 We also define two standard functions, append and reverse: *} |
|
175 |
|
176 fun app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where |
|
177 "app Nil ys = ys" | |
|
178 "app (Cons x xs) ys = Cons x (app xs ys)" |
|
179 |
|
180 fun rev :: "'a list \<Rightarrow> 'a list" where |
|
181 "rev Nil = Nil" | |
|
182 "rev (Cons x xs) = app (rev xs) (Cons x Nil)" |
|
183 |
|
184 text{* By default, variables @{text xs}, @{text ys} and @{text zs} are of |
|
185 @{text list} type. |
|
186 |
|
187 Command \indexed{\isacommand{value}}{value} evaluates a term. For example, *} |
|
188 |
|
189 value "rev(Cons True (Cons False Nil))" |
|
190 |
|
191 text{* yields the result @{value "rev(Cons True (Cons False Nil))"}. This works symbolically, too: *} |
|
192 |
|
193 value "rev(Cons a (Cons b Nil))" |
|
194 |
|
195 text{* yields @{value "rev(Cons a (Cons b Nil))"}. |
|
196 \medskip |
|
197 |
|
198 Figure~\ref{fig:MyList} shows the theory created so far. |
|
199 Because @{text list}, @{const Nil}, @{const Cons} etc are already predefined, |
|
200 Isabelle prints qualified (long) names when executing this theory, for example, @{text MyList.Nil} |
|
201 instead of @{const Nil}. |
|
202 To suppress the qualified names you can insert the command |
|
203 \texttt{declare [[names\_short]]}. |
|
204 This is not recommended in general but just for this unusual example. |
|
205 % Notice where the |
|
206 %quotations marks are needed that we mostly sweep under the carpet. In |
|
207 %particular, notice that \isacom{datatype} requires no quotation marks on the |
|
208 %left-hand side, but that on the right-hand side each of the argument |
|
209 %types of a constructor needs to be enclosed in quotation marks. |
|
210 |
|
211 \begin{figure}[htbp] |
|
212 \begin{alltt} |
|
213 \input{MyList.thy}\end{alltt} |
|
214 \caption{A Theory of Lists} |
|
215 \label{fig:MyList} |
|
216 \end{figure} |
|
217 |
|
218 \subsubsection{Structural Induction for Lists} |
|
219 |
|
220 Just as for natural numbers, there is a proof principle of induction for |
|
221 lists. Induction over a list is essentially induction over the length of |
|
222 the list, although the length remains implicit. To prove that some property |
|
223 @{text P} holds for all lists @{text xs}, i.e.\ \mbox{@{prop"P(xs)"}}, |
|
224 you need to prove |
|
225 \begin{enumerate} |
|
226 \item the base case @{prop"P(Nil)"} and |
|
227 \item the inductive case @{prop"P(Cons x xs)"} under the assumption @{prop"P(xs)"}, for some arbitrary but fixed @{text x} and @{text xs}. |
|
228 \end{enumerate} |
|
229 This is often called \concept{structural induction} for lists. |
|
230 |
|
231 \subsection{The Proof Process} |
|
232 |
|
233 We will now demonstrate the typical proof process, which involves |
|
234 the formulation and proof of auxiliary lemmas. |
|
235 Our goal is to show that reversing a list twice produces the original |
|
236 list. *} |
|
237 |
|
238 theorem rev_rev [simp]: "rev(rev xs) = xs" |
|
239 |
|
240 txt{* Commands \isacom{theorem} and \isacom{lemma} are |
|
241 interchangeable and merely indicate the importance we attach to a |
|
242 proposition. Via the bracketed attribute @{text simp} we also tell Isabelle |
|
243 to make the eventual theorem a \conceptnoidx{simplification rule}: future proofs |
|
244 involving simplification will replace occurrences of @{term"rev(rev xs)"} by |
|
245 @{term"xs"}. The proof is by induction: *} |
|
246 |
|
247 apply(induction xs) |
|
248 |
|
249 txt{* |
|
250 As explained above, we obtain two subgoals, namely the base case (@{const Nil}) and the induction step (@{const Cons}): |
|
251 @{subgoals[display,indent=0,margin=65]} |
|
252 Let us try to solve both goals automatically: |
|
253 *} |
|
254 |
|
255 apply(auto) |
|
256 |
|
257 txt{*Subgoal~1 is proved, and disappears; the simplified version |
|
258 of subgoal~2 becomes the new subgoal~1: |
|
259 @{subgoals[display,indent=0,margin=70]} |
|
260 In order to simplify this subgoal further, a lemma suggests itself. |
|
261 |
|
262 \subsubsection{A First Lemma} |
|
263 |
|
264 We insert the following lemma in front of the main theorem: |
|
265 *} |
|
266 (*<*) |
|
267 oops |
|
268 (*>*) |
|
269 lemma rev_app [simp]: "rev(app xs ys) = app (rev ys) (rev xs)" |
|
270 |
|
271 txt{* There are two variables that we could induct on: @{text xs} and |
|
272 @{text ys}. Because @{const app} is defined by recursion on |
|
273 the first argument, @{text xs} is the correct one: |
|
274 *} |
|
275 |
|
276 apply(induction xs) |
|
277 |
|
278 txt{* This time not even the base case is solved automatically: *} |
|
279 apply(auto) |
|
280 txt{* |
|
281 \vspace{-5ex} |
|
282 @{subgoals[display,goals_limit=1]} |
|
283 Again, we need to abandon this proof attempt and prove another simple lemma |
|
284 first. |
|
285 |
|
286 \subsubsection{A Second Lemma} |
|
287 |
|
288 We again try the canonical proof procedure: |
|
289 *} |
|
290 (*<*) |
|
291 oops |
|
292 (*>*) |
|
293 lemma app_Nil2 [simp]: "app xs Nil = xs" |
|
294 apply(induction xs) |
|
295 apply(auto) |
|
296 done |
|
297 |
|
298 text{* |
|
299 Thankfully, this worked. |
|
300 Now we can continue with our stuck proof attempt of the first lemma: |
|
301 *} |
|
302 |
|
303 lemma rev_app [simp]: "rev(app xs ys) = app (rev ys) (rev xs)" |
|
304 apply(induction xs) |
|
305 apply(auto) |
|
306 |
|
307 txt{* |
|
308 We find that this time @{text"auto"} solves the base case, but the |
|
309 induction step merely simplifies to |
|
310 @{subgoals[display,indent=0,goals_limit=1]} |
|
311 The missing lemma is associativity of @{const app}, |
|
312 which we insert in front of the failed lemma @{text rev_app}. |
|
313 |
|
314 \subsubsection{Associativity of @{const app}} |
|
315 |
|
316 The canonical proof procedure succeeds without further ado: |
|
317 *} |
|
318 (*<*)oops(*>*) |
|
319 lemma app_assoc [simp]: "app (app xs ys) zs = app xs (app ys zs)" |
|
320 apply(induction xs) |
|
321 apply(auto) |
|
322 done |
|
323 (*<*) |
|
324 lemma rev_app [simp]: "rev(app xs ys) = app (rev ys)(rev xs)" |
|
325 apply(induction xs) |
|
326 apply(auto) |
|
327 done |
|
328 |
|
329 theorem rev_rev [simp]: "rev(rev xs) = xs" |
|
330 apply(induction xs) |
|
331 apply(auto) |
|
332 done |
|
333 (*>*) |
|
334 text{* |
|
335 Finally the proofs of @{thm[source] rev_app} and @{thm[source] rev_rev} |
|
336 succeed, too. |
|
337 |
|
338 \subsubsection{Another Informal Proof} |
|
339 |
|
340 Here is the informal proof of associativity of @{const app} |
|
341 corresponding to the Isabelle proof above. |
|
342 \bigskip |
|
343 |
|
344 \noindent |
|
345 \textbf{Lemma} @{prop"app (app xs ys) zs = app xs (app ys zs)"} |
|
346 |
|
347 \noindent |
|
348 \textbf{Proof} by induction on @{text xs}. |
|
349 \begin{itemize} |
|
350 \item Case @{text Nil}: \ @{prop"app (app Nil ys) zs = app ys zs"} @{text"="} |
|
351 \mbox{@{term"app Nil (app ys zs)"}} \ holds by definition of @{text app}. |
|
352 \item Case @{text"Cons x xs"}: We assume |
|
353 \begin{center} \hfill @{term"app (app xs ys) zs"} @{text"="} |
|
354 @{term"app xs (app ys zs)"} \hfill (IH) \end{center} |
|
355 and we need to show |
|
356 \begin{center} @{prop"app (app (Cons x xs) ys) zs = app (Cons x xs) (app ys zs)"}.\end{center} |
|
357 The proof is as follows:\smallskip |
|
358 |
|
359 \begin{tabular}{@ {}l@ {\quad}l@ {}} |
|
360 @{term"app (app (Cons x xs) ys) zs"}\\ |
|
361 @{text"= app (Cons x (app xs ys)) zs"} & by definition of @{text app}\\ |
|
362 @{text"= Cons x (app (app xs ys) zs)"} & by definition of @{text app}\\ |
|
363 @{text"= Cons x (app xs (app ys zs))"} & by IH\\ |
|
364 @{text"= app (Cons x xs) (app ys zs)"} & by definition of @{text app} |
|
365 \end{tabular} |
|
366 \end{itemize} |
|
367 \medskip |
|
368 |
|
369 \noindent Didn't we say earlier that all proofs are by simplification? But |
|
370 in both cases, going from left to right, the last equality step is not a |
|
371 simplification at all! In the base case it is @{prop"app ys zs = app Nil (app |
|
372 ys zs)"}. It appears almost mysterious because we suddenly complicate the |
|
373 term by appending @{text Nil} on the left. What is really going on is this: |
|
374 when proving some equality \mbox{@{prop"s = t"}}, both @{text s} and @{text t} are |
|
375 simplified until they ``meet in the middle''. This heuristic for equality proofs |
|
376 works well for a functional programming context like ours. In the base case |
|
377 both @{term"app (app Nil ys) zs"} and @{term"app Nil (app |
|
378 ys zs)"} are simplified to @{term"app ys zs"}, the term in the middle. |
|
379 |
|
380 \subsection{Predefined Lists} |
|
381 \label{sec:predeflists} |
|
382 |
|
383 Isabelle's predefined lists are the same as the ones above, but with |
|
384 more syntactic sugar: |
|
385 \begin{itemize} |
|
386 \item @{text "[]"} is \indexed{@{const Nil}}{Nil}, |
|
387 \item @{term"x # xs"} is @{term"Cons x xs"}\index{Cons@@{const Cons}}, |
|
388 \item @{text"[x\<^sub>1, \<dots>, x\<^sub>n]"} is @{text"x\<^sub>1 # \<dots> # x\<^sub>n # []"}, and |
|
389 \item @{term "xs @ ys"} is @{term"app xs ys"}. |
|
390 \end{itemize} |
|
391 There is also a large library of predefined functions. |
|
392 The most important ones are the length function |
|
393 @{text"length :: 'a list \<Rightarrow> nat"}\index{length@@{const length}} (with the obvious definition), |
|
394 and the \indexed{@{const map}}{map} function that applies a function to all elements of a list: |
|
395 \begin{isabelle} |
|
396 \isacom{fun} @{const map} @{text"::"} @{typ[source] "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"}\\ |
|
397 @{text"\""}@{thm list.map(1)}@{text"\" |"}\\ |
|
398 @{text"\""}@{thm list.map(2)}@{text"\""} |
|
399 \end{isabelle} |
|
400 |
|
401 \ifsem |
|
402 Also useful are the \concept{head} of a list, its first element, |
|
403 and the \concept{tail}, the rest of the list: |
|
404 \begin{isabelle}\index{hd@@{const hd}} |
|
405 \isacom{fun} @{text"hd :: 'a list \<Rightarrow> 'a"}\\ |
|
406 @{prop"hd(x#xs) = x"} |
|
407 \end{isabelle} |
|
408 \begin{isabelle}\index{tl@@{const tl}} |
|
409 \isacom{fun} @{text"tl :: 'a list \<Rightarrow> 'a list"}\\ |
|
410 @{prop"tl [] = []"} @{text"|"}\\ |
|
411 @{prop"tl(x#xs) = xs"} |
|
412 \end{isabelle} |
|
413 Note that since HOL is a logic of total functions, @{term"hd []"} is defined, |
|
414 but we do now know what the result is. That is, @{term"hd []"} is not undefined |
|
415 but underdefined. |
|
416 \fi |
|
417 % |
|
418 |
|
419 From now on lists are always the predefined lists. |
|
420 |
|
421 |
|
422 \subsection*{Exercises} |
|
423 |
|
424 \begin{exercise} |
|
425 Use the \isacom{value} command to evaluate the following expressions: |
|
426 @{term[source] "1 + (2::nat)"}, @{term[source] "1 + (2::int)"}, |
|
427 @{term[source] "1 - (2::nat)"} and @{term[source] "1 - (2::int)"}. |
|
428 \end{exercise} |
|
429 |
|
430 \begin{exercise} |
|
431 Start from the definition of @{const add} given above. |
|
432 Prove that @{const add} is associative and commutative. |
|
433 Define a recursive function @{text double} @{text"::"} @{typ"nat \<Rightarrow> nat"} |
|
434 and prove @{prop"double m = add m m"}. |
|
435 \end{exercise} |
|
436 |
|
437 \begin{exercise} |
|
438 Define a function @{text"count ::"} @{typ"'a \<Rightarrow> 'a list \<Rightarrow> nat"} |
|
439 that counts the number of occurrences of an element in a list. Prove |
|
440 @{prop"count x xs \<le> length xs"}. |
|
441 \end{exercise} |
|
442 |
|
443 \begin{exercise} |
|
444 Define a recursive function @{text "snoc ::"} @{typ"'a list \<Rightarrow> 'a \<Rightarrow> 'a list"} |
|
445 that appends an element to the end of a list. With the help of @{text snoc} |
|
446 define a recursive function @{text "reverse ::"} @{typ"'a list \<Rightarrow> 'a list"} |
|
447 that reverses a list. Prove @{prop"reverse(reverse xs) = xs"}. |
|
448 \end{exercise} |
|
449 |
|
450 \begin{exercise} |
|
451 Define a recursive function @{text "sum ::"} @{typ"nat \<Rightarrow> nat"} such that |
|
452 \mbox{@{text"sum n"}} @{text"="} @{text"0 + ... + n"} and prove |
|
453 @{prop" sum(n::nat) = n * (n+1) div 2"}. |
|
454 \end{exercise} |
|
455 *} |
|
456 (*<*) |
|
457 end |
|
458 (*>*) |