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