author | wenzelm |
Sun, 06 Dec 2020 13:44:07 +0100 | |
changeset 72834 | a025f845fd41 |
parent 72656 | a17c17ab931c |
child 73511 | 2cdbb6a2f2a7 |
permissions | -rw-r--r-- |
47269 | 1 |
(*<*) |
2 |
theory Bool_nat_list |
|
68919 | 3 |
imports Complex_Main |
47269 | 4 |
begin |
5 |
(*>*) |
|
6 |
||
67406 | 7 |
text\<open> |
47269 | 8 |
\vspace{-4ex} |
69597 | 9 |
\section{\texorpdfstring{Types \<^typ>\<open>bool\<close>, \<^typ>\<open>nat\<close> and \<open>list\<close>}{Types bool, nat and list}} |
47269 | 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 |
||
69597 | 15 |
\subsection{Type \indexed{\<^typ>\<open>bool\<close>}{bool}} |
47269 | 16 |
|
17 |
The type of boolean values is a predefined datatype |
|
18 |
@{datatype[display] bool} |
|
69597 | 19 |
with the two values \indexed{\<^const>\<open>True\<close>}{True} and \indexed{\<^const>\<open>False\<close>}{False} and |
69505 | 20 |
with many predefined functions: \<open>\<not>\<close>, \<open>\<and>\<close>, \<open>\<or>\<close>, \<open>\<longrightarrow>\<close>, etc. Here is how conjunction could be defined by pattern matching: |
67406 | 21 |
\<close> |
47269 | 22 |
|
23 |
fun conj :: "bool \<Rightarrow> bool \<Rightarrow> bool" where |
|
24 |
"conj True True = True" | |
|
25 |
"conj _ _ = False" |
|
26 |
||
67406 | 27 |
text\<open>Both the datatype and function definitions roughly follow the syntax |
47269 | 28 |
of functional programming languages. |
29 |
||
69597 | 30 |
\subsection{Type \indexed{\<^typ>\<open>nat\<close>}{nat}} |
47269 | 31 |
|
32 |
Natural numbers are another predefined datatype: |
|
69597 | 33 |
@{datatype[display] nat}\index{Suc@\<^const>\<open>Suc\<close>} |
34 |
All values of type \<^typ>\<open>nat\<close> are generated by the constructors |
|
35 |
\<open>0\<close> and \<^const>\<open>Suc\<close>. Thus the values of type \<^typ>\<open>nat\<close> are |
|
36 |
\<open>0\<close>, \<^term>\<open>Suc 0\<close>, \<^term>\<open>Suc(Suc 0)\<close>, etc. |
|
69505 | 37 |
There are many predefined functions: \<open>+\<close>, \<open>*\<close>, \<open>\<le>\<close>, etc. Here is how you could define your own addition: |
67406 | 38 |
\<close> |
47269 | 39 |
|
40 |
fun add :: "nat \<Rightarrow> nat \<Rightarrow> nat" where |
|
41 |
"add 0 n = n" | |
|
42 |
"add (Suc m) n = Suc(add m n)" |
|
43 |
||
69597 | 44 |
text\<open>And here is a proof of the fact that \<^prop>\<open>add m 0 = m\<close>:\<close> |
47269 | 45 |
|
46 |
lemma add_02: "add m 0 = m" |
|
47 |
apply(induction m) |
|
48 |
apply(auto) |
|
49 |
done |
|
50 |
(*<*) |
|
51 |
lemma "add m 0 = m" |
|
52 |
apply(induction m) |
|
53 |
(*>*) |
|
67406 | 54 |
txt\<open>The \isacom{lemma} command starts the proof and gives the lemma |
69505 | 55 |
a name, \<open>add_02\<close>. Properties of recursively defined functions |
47269 | 56 |
need to be established by induction in most cases. |
69505 | 57 |
Command \isacom{apply}\<open>(induction m)\<close> instructs Isabelle to |
58 |
start a proof by induction on \<open>m\<close>. In response, it will show the |
|
62222 | 59 |
following proof state\ifsem\footnote{See page \pageref{proof-state} for how to |
62223 | 60 |
display the proof state.}\fi: |
47269 | 61 |
@{subgoals[display,indent=0]} |
62 |
The numbered lines are known as \emph{subgoals}. |
|
63 |
The first subgoal is the base case, the second one the induction step. |
|
69505 | 64 |
The prefix \<open>\<And>m.\<close> is Isabelle's way of saying ``for an arbitrary but fixed \<open>m\<close>''. The \<open>\<Longrightarrow>\<close> separates assumptions from the conclusion. |
65 |
The command \isacom{apply}\<open>(auto)\<close> instructs Isabelle to try |
|
47269 | 66 |
and prove all subgoals automatically, essentially by simplifying them. |
67 |
Because both subgoals are easy, Isabelle can do it. |
|
69597 | 68 |
The base case \<^prop>\<open>add 0 0 = 0\<close> holds by definition of \<^const>\<open>add\<close>, |
47269 | 69 |
and the induction step is almost as simple: |
69505 | 70 |
\<open>add\<^latex>\<open>~\<close>(Suc m) 0 = Suc(add m 0) = Suc m\<close> |
69597 | 71 |
using first the definition of \<^const>\<open>add\<close> and then the induction hypothesis. |
47269 | 72 |
In summary, both subproofs rely on simplification with function definitions and |
73 |
the induction hypothesis. |
|
74 |
As a result of that final \isacom{done}, Isabelle associates the lemma |
|
75 |
just proved with its name. You can now inspect the lemma with the command |
|
67406 | 76 |
\<close> |
47269 | 77 |
|
78 |
thm add_02 |
|
79 |
||
67406 | 80 |
txt\<open>which displays @{thm[show_question_marks,display] add_02} The free |
69505 | 81 |
variable \<open>m\<close> has been replaced by the \concept{unknown} |
82 |
\<open>?m\<close>. There is no logical difference between the two but there is an |
|
47269 | 83 |
operational one: unknowns can be instantiated, which is what you want after |
84 |
some lemma has been proved. |
|
85 |
||
69505 | 86 |
Note that there is also a proof method \<open>induct\<close>, which behaves almost |
87 |
like \<open>induction\<close>; the difference is explained in \autoref{ch:Isar}. |
|
47269 | 88 |
|
89 |
\begin{warn} |
|
90 |
Terminology: We use \concept{lemma}, \concept{theorem} and \concept{rule} |
|
91 |
interchangeably for propositions that have been proved. |
|
92 |
\end{warn} |
|
93 |
\begin{warn} |
|
69505 | 94 |
Numerals (\<open>0\<close>, \<open>1\<close>, \<open>2\<close>, \dots) and most of the standard |
95 |
arithmetic operations (\<open>+\<close>, \<open>-\<close>, \<open>*\<close>, \<open>\<le>\<close>, |
|
96 |
\<open><\<close>, etc.) are overloaded: they are available |
|
47269 | 97 |
not just for natural numbers but for other types as well. |
69505 | 98 |
For example, given the goal \<open>x + 0 = x\<close>, there is nothing to indicate |
47269 | 99 |
that you are talking about natural numbers. Hence Isabelle can only infer |
69597 | 100 |
that \<^term>\<open>x\<close> is of some arbitrary type where \<open>0\<close> and \<open>+\<close> |
54508 | 101 |
exist. As a consequence, you will be unable to prove the goal. |
102 |
% To alert you to such pitfalls, Isabelle flags numerals without a |
|
103 |
% fixed type in its output: @ {prop"x+0 = x"}. |
|
104 |
In this particular example, you need to include |
|
69505 | 105 |
an explicit type constraint, for example \<open>x+0 = (x::nat)\<close>. If there |
69597 | 106 |
is enough contextual information this may not be necessary: \<^prop>\<open>Suc x = |
107 |
x\<close> automatically implies \<open>x::nat\<close> because \<^term>\<open>Suc\<close> is not |
|
47269 | 108 |
overloaded. |
109 |
\end{warn} |
|
110 |
||
52361 | 111 |
\subsubsection{An Informal Proof} |
47269 | 112 |
|
113 |
Above we gave some terse informal explanation of the proof of |
|
69597 | 114 |
\<^prop>\<open>add m 0 = m\<close>. A more detailed informal exposition of the lemma |
47269 | 115 |
might look like this: |
116 |
\bigskip |
|
117 |
||
118 |
\noindent |
|
69597 | 119 |
\textbf{Lemma} \<^prop>\<open>add m 0 = m\<close> |
47269 | 120 |
|
121 |
\noindent |
|
69505 | 122 |
\textbf{Proof} by induction on \<open>m\<close>. |
47269 | 123 |
\begin{itemize} |
69597 | 124 |
\item Case \<open>0\<close> (the base case): \<^prop>\<open>add 0 0 = 0\<close> |
125 |
holds by definition of \<^const>\<open>add\<close>. |
|
126 |
\item Case \<^term>\<open>Suc m\<close> (the induction step): |
|
127 |
We assume \<^prop>\<open>add m 0 = m\<close>, the induction hypothesis (IH), |
|
69505 | 128 |
and we need to show \<open>add (Suc m) 0 = Suc m\<close>. |
47269 | 129 |
The proof is as follows:\smallskip |
130 |
||
131 |
\begin{tabular}{@ {}rcl@ {\quad}l@ {}} |
|
69597 | 132 |
\<^term>\<open>add (Suc m) 0\<close> &\<open>=\<close>& \<^term>\<open>Suc(add m 0)\<close> |
69505 | 133 |
& by definition of \<open>add\<close>\\ |
69597 | 134 |
&\<open>=\<close>& \<^term>\<open>Suc m\<close> & by IH |
47269 | 135 |
\end{tabular} |
136 |
\end{itemize} |
|
137 |
Throughout this book, \concept{IH} will stand for ``induction hypothesis''. |
|
138 |
||
69597 | 139 |
We have now seen three proofs of \<^prop>\<open>add m 0 = 0\<close>: the Isabelle one, the |
47711 | 140 |
terse four lines explaining the base case and the induction step, and just now a |
47269 | 141 |
model of a traditional inductive proof. The three proofs differ in the level |
142 |
of detail given and the intended reader: the Isabelle proof is for the |
|
143 |
machine, the informal proofs are for humans. Although this book concentrates |
|
47711 | 144 |
on Isabelle proofs, it is important to be able to rephrase those proofs |
47269 | 145 |
as informal text comprehensible to a reader familiar with traditional |
146 |
mathematical proofs. Later on we will introduce an Isabelle proof language |
|
147 |
that is closer to traditional informal mathematical language and is often |
|
148 |
directly readable. |
|
149 |
||
69505 | 150 |
\subsection{Type \indexed{\<open>list\<close>}{list}} |
47269 | 151 |
|
58521 | 152 |
Although lists are already predefined, we define our own copy for |
47269 | 153 |
demonstration purposes: |
67406 | 154 |
\<close> |
47269 | 155 |
(*<*) |
156 |
apply(auto) |
|
157 |
done |
|
158 |
declare [[names_short]] |
|
159 |
(*>*) |
|
47302 | 160 |
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
|
161 |
(*<*) |
0cbe0a56d3fa
update map definition in Prog_Prove for new datatype package
kleing
parents:
58521
diff
changeset
|
162 |
for map: map |
0cbe0a56d3fa
update map definition in Prog_Prove for new datatype package
kleing
parents:
58521
diff
changeset
|
163 |
(*>*) |
47269 | 164 |
|
67406 | 165 |
text\<open> |
47302 | 166 |
\begin{itemize} |
69597 | 167 |
\item Type \<^typ>\<open>'a list\<close> is the type of lists over elements of type \<^typ>\<open>'a\<close>. Because \<^typ>\<open>'a\<close> 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). |
168 |
\item Lists have two constructors: \<^const>\<open>Nil\<close>, the empty list, and \<^const>\<open>Cons\<close>, which puts an element (of type \<^typ>\<open>'a\<close>) in front of a list (of type \<^typ>\<open>'a list\<close>). |
|
169 |
Hence all lists are of the form \<^const>\<open>Nil\<close>, or \<^term>\<open>Cons x Nil\<close>, |
|
170 |
or \<^term>\<open>Cons x (Cons y Nil)\<close>, etc. |
|
47302 | 171 |
\item \isacom{datatype} requires no quotation marks on the |
172 |
left-hand side, but on the right-hand side each of the argument |
|
173 |
types of a constructor needs to be enclosed in quotation marks, unless |
|
69597 | 174 |
it is just an identifier (e.g., \<^typ>\<open>nat\<close> or \<^typ>\<open>'a\<close>). |
47302 | 175 |
\end{itemize} |
67406 | 176 |
We also define two standard functions, append and reverse:\<close> |
47269 | 177 |
|
178 |
fun app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where |
|
179 |
"app Nil ys = ys" | |
|
180 |
"app (Cons x xs) ys = Cons x (app xs ys)" |
|
181 |
||
182 |
fun rev :: "'a list \<Rightarrow> 'a list" where |
|
183 |
"rev Nil = Nil" | |
|
184 |
"rev (Cons x xs) = app (rev xs) (Cons x Nil)" |
|
185 |
||
69505 | 186 |
text\<open>By default, variables \<open>xs\<close>, \<open>ys\<close> and \<open>zs\<close> are of |
187 |
\<open>list\<close> type. |
|
47269 | 188 |
|
67406 | 189 |
Command \indexed{\isacommand{value}}{value} evaluates a term. For example,\<close> |
47269 | 190 |
|
191 |
value "rev(Cons True (Cons False Nil))" |
|
192 |
||
69597 | 193 |
text\<open>yields the result \<^value>\<open>rev(Cons True (Cons False Nil))\<close>. This works symbolically, too:\<close> |
47269 | 194 |
|
195 |
value "rev(Cons a (Cons b Nil))" |
|
196 |
||
69597 | 197 |
text\<open>yields \<^value>\<open>rev(Cons a (Cons b Nil))\<close>. |
47269 | 198 |
\medskip |
199 |
||
47302 | 200 |
Figure~\ref{fig:MyList} shows the theory created so far. |
69597 | 201 |
Because \<open>list\<close>, \<^const>\<open>Nil\<close>, \<^const>\<open>Cons\<close>, etc.\ are already predefined, |
69505 | 202 |
Isabelle prints qualified (long) names when executing this theory, for example, \<open>MyList.Nil\<close> |
69597 | 203 |
instead of \<^const>\<open>Nil\<close>. |
47719
8aac84627b84
the perennial doc problem of how to define lists a second time
nipkow
parents:
47711
diff
changeset
|
204 |
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
|
205 |
\texttt{declare [[names\_short]]}. |
56989 | 206 |
This is not recommended in general but is convenient for this unusual example. |
47302 | 207 |
% Notice where the |
208 |
%quotations marks are needed that we mostly sweep under the carpet. In |
|
209 |
%particular, notice that \isacom{datatype} requires no quotation marks on the |
|
210 |
%left-hand side, but that on the right-hand side each of the argument |
|
211 |
%types of a constructor needs to be enclosed in quotation marks. |
|
47269 | 212 |
|
213 |
\begin{figure}[htbp] |
|
214 |
\begin{alltt} |
|
48947
7eee8b2d2099
more standard document preparation within session context;
wenzelm
parents:
47719
diff
changeset
|
215 |
\input{MyList.thy}\end{alltt} |
58521 | 216 |
\caption{A theory of lists} |
47269 | 217 |
\label{fig:MyList} |
57805 | 218 |
\index{comment} |
47269 | 219 |
\end{figure} |
220 |
||
221 |
\subsubsection{Structural Induction for Lists} |
|
222 |
||
223 |
Just as for natural numbers, there is a proof principle of induction for |
|
224 |
lists. Induction over a list is essentially induction over the length of |
|
225 |
the list, although the length remains implicit. To prove that some property |
|
69597 | 226 |
\<open>P\<close> holds for all lists \<open>xs\<close>, i.e., \mbox{\<^prop>\<open>P(xs)\<close>}, |
47269 | 227 |
you need to prove |
228 |
\begin{enumerate} |
|
69597 | 229 |
\item the base case \<^prop>\<open>P(Nil)\<close> and |
230 |
\item the inductive case \<^prop>\<open>P(Cons x xs)\<close> under the assumption \<^prop>\<open>P(xs)\<close>, for some arbitrary but fixed \<open>x\<close> and \<open>xs\<close>. |
|
47269 | 231 |
\end{enumerate} |
55318 | 232 |
This is often called \concept{structural induction} for lists. |
47269 | 233 |
|
234 |
\subsection{The Proof Process} |
|
235 |
||
236 |
We will now demonstrate the typical proof process, which involves |
|
237 |
the formulation and proof of auxiliary lemmas. |
|
238 |
Our goal is to show that reversing a list twice produces the original |
|
67406 | 239 |
list.\<close> |
47269 | 240 |
|
241 |
theorem rev_rev [simp]: "rev(rev xs) = xs" |
|
242 |
||
67406 | 243 |
txt\<open>Commands \isacom{theorem} and \isacom{lemma} are |
47269 | 244 |
interchangeable and merely indicate the importance we attach to a |
69505 | 245 |
proposition. Via the bracketed attribute \<open>simp\<close> we also tell Isabelle |
55317 | 246 |
to make the eventual theorem a \conceptnoidx{simplification rule}: future proofs |
69597 | 247 |
involving simplification will replace occurrences of \<^term>\<open>rev(rev xs)\<close> by |
248 |
\<^term>\<open>xs\<close>. The proof is by induction:\<close> |
|
47269 | 249 |
|
250 |
apply(induction xs) |
|
251 |
||
67406 | 252 |
txt\<open> |
69597 | 253 |
As explained above, we obtain two subgoals, namely the base case (\<^const>\<open>Nil\<close>) and the induction step (\<^const>\<open>Cons\<close>): |
47269 | 254 |
@{subgoals[display,indent=0,margin=65]} |
255 |
Let us try to solve both goals automatically: |
|
67406 | 256 |
\<close> |
47269 | 257 |
|
258 |
apply(auto) |
|
259 |
||
67406 | 260 |
txt\<open>Subgoal~1 is proved, and disappears; the simplified version |
47269 | 261 |
of subgoal~2 becomes the new subgoal~1: |
262 |
@{subgoals[display,indent=0,margin=70]} |
|
263 |
In order to simplify this subgoal further, a lemma suggests itself. |
|
264 |
||
265 |
\subsubsection{A First Lemma} |
|
266 |
||
267 |
We insert the following lemma in front of the main theorem: |
|
67406 | 268 |
\<close> |
47269 | 269 |
(*<*) |
270 |
oops |
|
271 |
(*>*) |
|
272 |
lemma rev_app [simp]: "rev(app xs ys) = app (rev ys) (rev xs)" |
|
273 |
||
69505 | 274 |
txt\<open>There are two variables that we could induct on: \<open>xs\<close> and |
69597 | 275 |
\<open>ys\<close>. Because \<^const>\<open>app\<close> is defined by recursion on |
69505 | 276 |
the first argument, \<open>xs\<close> is the correct one: |
67406 | 277 |
\<close> |
47269 | 278 |
|
279 |
apply(induction xs) |
|
280 |
||
67406 | 281 |
txt\<open>This time not even the base case is solved automatically:\<close> |
47269 | 282 |
apply(auto) |
67406 | 283 |
txt\<open> |
47269 | 284 |
\vspace{-5ex} |
285 |
@{subgoals[display,goals_limit=1]} |
|
286 |
Again, we need to abandon this proof attempt and prove another simple lemma |
|
287 |
first. |
|
288 |
||
289 |
\subsubsection{A Second Lemma} |
|
290 |
||
291 |
We again try the canonical proof procedure: |
|
67406 | 292 |
\<close> |
47269 | 293 |
(*<*) |
294 |
oops |
|
295 |
(*>*) |
|
296 |
lemma app_Nil2 [simp]: "app xs Nil = xs" |
|
297 |
apply(induction xs) |
|
298 |
apply(auto) |
|
299 |
done |
|
300 |
||
67406 | 301 |
text\<open> |
47269 | 302 |
Thankfully, this worked. |
303 |
Now we can continue with our stuck proof attempt of the first lemma: |
|
67406 | 304 |
\<close> |
47269 | 305 |
|
306 |
lemma rev_app [simp]: "rev(app xs ys) = app (rev ys) (rev xs)" |
|
307 |
apply(induction xs) |
|
308 |
apply(auto) |
|
309 |
||
67406 | 310 |
txt\<open> |
69505 | 311 |
We find that this time \<open>auto\<close> solves the base case, but the |
47269 | 312 |
induction step merely simplifies to |
313 |
@{subgoals[display,indent=0,goals_limit=1]} |
|