author  wenzelm 
Sat, 05 Apr 2014 15:03:40 +0200  
changeset 56421  1ffd7eaa778b 
parent 55465  0d31c0546286 
permissions  rwrr 
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 
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 

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 

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"+"} 

54508  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 

47269  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 

52361  112 
\subsubsection{An Informal Proof} 
47269  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 

47711  141 
terse four lines explaining the base case and the induction step, and just now a 
47269  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 

47711  145 
on Isabelle proofs, it is important to be able to rephrase those proofs 
47269  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 

55317  151 
\subsection{Type \indexed{@{text list}}{list}} 
47269  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 
(*>*) 

47302  161 
datatype 'a list = Nil  Cons 'a "'a list" 
47269  162 

47302  163 
text{* 
164 
\begin{itemize} 

47711  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). 
47302  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"}, 

47269  168 
or @{term"Cons x (Cons y Nil)"} etc. 
47302  169 
\item \isacom{datatype} requires no quotation marks on the 
170 
lefthand side, but on the righthand 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} 

47269  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 

55320  187 
Command \indexed{\isacommand{value}}{value} evaluates a term. For example, *} 
47269  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 

47302  198 
Figure~\ref{fig:MyList} shows the theory created so far. 
47719
8aac84627b84
the perennial doc problem of how to define lists a second time
nipkow
parents:
47711
diff
changeset

199 
Because @{text list}, @{const Nil}, @{const Cons} etc are already predefined, 
8aac84627b84
the perennial doc problem of how to define lists a second time
nipkow
parents:
47711
diff
changeset

200 
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

201 
instead of @{const Nil}. 
8aac84627b84
the perennial doc problem of how to define lists a second time
nipkow
parents:
47711
diff
changeset

202 
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

203 
\texttt{declare [[names\_short]]}. 
8aac84627b84
the perennial doc problem of how to define lists a second time
nipkow
parents:
47711
diff
changeset

204 
This is not recommended in general but just for this unusual example. 
47302  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 
%lefthand side, but that on the righthand side each of the argument 

209 
%types of a constructor needs to be enclosed in quotation marks. 

47269  210 

211 
\begin{figure}[htbp] 

212 
\begin{alltt} 

48947
7eee8b2d2099
more standard document preparation within session context;
wenzelm
parents:
47719
diff
changeset

213 
\input{MyList.thy}\end{alltt} 
47269  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 

47711  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}. 
47269  228 
\end{enumerate} 
55318  229 
This is often called \concept{structural induction} for lists. 
47269  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 

55317  243 
to make the eventual theorem a \conceptnoidx{simplification rule}: future proofs 
47269  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]} 

47711  311 
The missing lemma is associativity of @{const app}, 
47269  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 

52361  338 
\subsubsection{Another Informal Proof} 
47269  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 

54467  375 
simplified until they ``meet in the middle''. This heuristic for equality proofs 
47269  376 
works well for a functional programming context like ours. In the base case 
54467  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. 

47269  379 

52361  380 
\subsection{Predefined Lists} 
47269  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} 

55317  386 
\item @{text "[]"} is \indexed{@{const Nil}}{Nil}, 
387 
\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

388 
\item @{text"[x\<^sub>1, \<dots>, x\<^sub>n]"} is @{text"x\<^sub>1 # \<dots> # x\<^sub>n # []"}, and 
47269  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 

55317  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: 

47269  395 
\begin{isabelle} 
47306  396 
\isacom{fun} @{const map} @{text"::"} @{typ[source] "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"}\\ 
55465  397 
@{text"\""}@{thm list.map(1)}@{text"\" "}\\ 
398 
@{text"\""}@{thm list.map(2)}@{text"\""} 

47269  399 
\end{isabelle} 
52782  400 

401 
\ifsem 

47269  402 
Also useful are the \concept{head} of a list, its first element, 
403 
and the \concept{tail}, the rest of the list: 

55317  404 
\begin{isabelle}\index{hd@@{const hd}} 
47269  405 
\isacom{fun} @{text"hd :: 'a list \<Rightarrow> 'a"}\\ 
406 
@{prop"hd(x#xs) = x"} 

407 
\end{isabelle} 

55317  408 
\begin{isabelle}\index{tl@@{const tl}} 
47269  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. 

52782  416 
\fi 
47306  417 
% 
52593  418 

52842  419 
From now on lists are always the predefined lists. 
420 

421 

54436  422 
\subsection*{Exercises} 
52593  423 

424 
\begin{exercise} 

54121  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} 

52842  431 
Start from the definition of @{const add} given above. 
54467  432 
Prove that @{const add} is associative and commutative. 
54121  433 
Define a recursive function @{text double} @{text"::"} @{typ"nat \<Rightarrow> nat"} 
434 
and prove @{prop"double m = add m m"}. 

52593  435 
\end{exercise} 
52718  436 

52593  437 
\begin{exercise} 
52842  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"} 

54121  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"}. 

52593  454 
\end{exercise} 
47269  455 
*} 
456 
(*<*) 

457 
end 

458 
(*>*) 