author | wenzelm |
Tue, 28 Aug 2012 14:37:57 +0200 | |
changeset 48966 | 6e15de7dd871 |
parent 38432 | 439f50a241c1 |
permissions | -rw-r--r-- |
15136 | 1 |
theory ToyList |
26729 | 2 |
imports Datatype |
15136 | 3 |
begin |
8745 | 4 |
|
48966
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
38432
diff
changeset
|
5 |
(*<*) |
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
38432
diff
changeset
|
6 |
ML {* |
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
38432
diff
changeset
|
7 |
let |
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
38432
diff
changeset
|
8 |
val texts = |
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
38432
diff
changeset
|
9 |
map (File.read o Path.append (Thy_Load.master_directory @{theory}) o Path.explode) |
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
38432
diff
changeset
|
10 |
["ToyList1", "ToyList2"]; |
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
38432
diff
changeset
|
11 |
val trs = Outer_Syntax.parse Position.start (implode texts); |
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
38432
diff
changeset
|
12 |
in @{assert} (Toplevel.is_toplevel (fold Toplevel.command trs Toplevel.toplevel)) end; |
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
38432
diff
changeset
|
13 |
*} |
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
38432
diff
changeset
|
14 |
(*>*) |
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
wenzelm
parents:
38432
diff
changeset
|
15 |
|
8745 | 16 |
text{*\noindent |
26729 | 17 |
HOL already has a predefined theory of lists called @{text List} --- |
18 |
@{text ToyList} is merely a small fragment of it chosen as an example. In |
|
8745 | 19 |
contrast to what is recommended in \S\ref{sec:Basic:Theories}, |
26729 | 20 |
@{text ToyList} is not based on @{text Main} but on @{text Datatype}, a |
8745 | 21 |
theory that contains pretty much everything but lists, thus avoiding |
22 |
ambiguities caused by defining lists twice. |
|
23 |
*} |
|
24 |
||
25 |
datatype 'a list = Nil ("[]") |
|
26 |
| Cons 'a "'a list" (infixr "#" 65); |
|
27 |
||
28 |
text{*\noindent |
|
12327 | 29 |
The datatype\index{datatype@\isacommand {datatype} (command)} |
30 |
\tydx{list} introduces two |
|
11428 | 31 |
constructors \cdx{Nil} and \cdx{Cons}, the |
9541 | 32 |
empty~list and the operator that adds an element to the front of a list. For |
9792 | 33 |
example, the term \isa{Cons True (Cons False Nil)} is a value of |
34 |
type @{typ"bool list"}, namely the list with the elements @{term"True"} and |
|
11450 | 35 |
@{term"False"}. Because this notation quickly becomes unwieldy, the |
8745 | 36 |
datatype declaration is annotated with an alternative syntax: instead of |
9792 | 37 |
@{term[source]Nil} and \isa{Cons x xs} we can write |
15364 | 38 |
@{term"[]"}\index{$HOL2list@\isa{[]}|bold} and |
39 |
@{term"x # xs"}\index{$HOL2list@\isa{\#}|bold}. In fact, this |
|
11450 | 40 |
alternative syntax is the familiar one. Thus the list \isa{Cons True |
9541 | 41 |
(Cons False Nil)} becomes @{term"True # False # []"}. The annotation |
11428 | 42 |
\isacommand{infixr}\index{infixr@\isacommand{infixr} (annotation)} |
43 |
means that @{text"#"} associates to |
|
11450 | 44 |
the right: the term @{term"x # y # z"} is read as @{text"x # (y # z)"} |
9792 | 45 |
and not as @{text"(x # y) # z"}. |
10971 | 46 |
The @{text 65} is the priority of the infix @{text"#"}. |
8745 | 47 |
|
48 |
\begin{warn} |
|
13191 | 49 |
Syntax annotations can be powerful, but they are difficult to master and |
11456 | 50 |
are never necessary. You |
9792 | 51 |
could drop them from theory @{text"ToyList"} and go back to the identifiers |
27015 | 52 |
@{term[source]Nil} and @{term[source]Cons}. Novices should avoid using |
10795 | 53 |
syntax annotations in their own theories. |
8745 | 54 |
\end{warn} |
27015 | 55 |
Next, two functions @{text"app"} and \cdx{rev} are defined recursively, |
56 |
in this order, because Isabelle insists on definition before use: |
|
8745 | 57 |
*} |
58 |
||
27015 | 59 |
primrec app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65) where |
60 |
"[] @ ys = ys" | |
|
61 |
"(x # xs) @ ys = x # (xs @ ys)" |
|
62 |
||
63 |
primrec rev :: "'a list \<Rightarrow> 'a list" where |
|
64 |
"rev [] = []" | |
|
65 |
"rev (x # xs) = (rev xs) @ (x # [])" |
|
8745 | 66 |
|
27015 | 67 |
text{*\noindent |
68 |
Each function definition is of the form |
|
69 |
\begin{center} |
|
70 |
\isacommand{primrec} \textit{name} @{text"::"} \textit{type} \textit{(optional syntax)} \isakeyword{where} \textit{equations} |
|
71 |
\end{center} |
|
72 |
The equations must be separated by @{text"|"}. |
|
73 |
% |
|
74 |
Function @{text"app"} is annotated with concrete syntax. Instead of the |
|
10790 | 75 |
prefix syntax @{text"app xs ys"} the infix |
15364 | 76 |
@{term"xs @ ys"}\index{$HOL2list@\isa{\at}|bold} becomes the preferred |
27015 | 77 |
form. |
8745 | 78 |
|
27015 | 79 |
\index{*rev (constant)|(}\index{append function|(} |
10790 | 80 |
The equations for @{text"app"} and @{term"rev"} hardly need comments: |
81 |
@{text"app"} appends two lists and @{term"rev"} reverses a list. The |
|
11428 | 82 |
keyword \commdx{primrec} indicates that the recursion is |
10790 | 83 |
of a particularly primitive kind where each recursive call peels off a datatype |
8771 | 84 |
constructor from one of the arguments. Thus the |
10654 | 85 |
recursion always terminates, i.e.\ the function is \textbf{total}. |
11428 | 86 |
\index{functions!total} |
8745 | 87 |
|
88 |
The termination requirement is absolutely essential in HOL, a logic of total |
|
89 |
functions. If we were to drop it, inconsistencies would quickly arise: the |
|
90 |
``definition'' $f(n) = f(n)+1$ immediately leads to $0 = 1$ by subtracting |
|
91 |
$f(n)$ on both sides. |
|
92 |
% However, this is a subtle issue that we cannot discuss here further. |
|
93 |
||
94 |
\begin{warn} |
|
11456 | 95 |
As we have indicated, the requirement for total functions is an essential characteristic of HOL\@. It is only |
8745 | 96 |
because of totality that reasoning in HOL is comparatively easy. More |
11456 | 97 |
generally, the philosophy in HOL is to refrain from asserting arbitrary axioms (such as |
8745 | 98 |
function definitions whose totality has not been proved) because they |
99 |
quickly lead to inconsistencies. Instead, fixed constructs for introducing |
|
100 |
types and functions are offered (such as \isacommand{datatype} and |
|
101 |
\isacommand{primrec}) which are guaranteed to preserve consistency. |
|
102 |
\end{warn} |
|
103 |
||
11456 | 104 |
\index{syntax}% |
8745 | 105 |
A remark about syntax. The textual definition of a theory follows a fixed |
10971 | 106 |
syntax with keywords like \isacommand{datatype} and \isacommand{end}. |
107 |
% (see Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list). |
|
8745 | 108 |
Embedded in this syntax are the types and formulae of HOL, whose syntax is |
12631 | 109 |
extensible (see \S\ref{sec:concrete-syntax}), e.g.\ by new user-defined infix operators. |
10971 | 110 |
To distinguish the two levels, everything |
8745 | 111 |
HOL-specific (terms and types) should be enclosed in |
112 |
\texttt{"}\dots\texttt{"}. |
|
113 |
To lessen this burden, quotation marks around a single identifier can be |
|
27015 | 114 |
dropped, unless the identifier happens to be a keyword, for example |
115 |
\isa{"end"}. |
|
8745 | 116 |
When Isabelle prints a syntax error message, it refers to the HOL syntax as |
11456 | 117 |
the \textbf{inner syntax} and the enclosing theory language as the \textbf{outer syntax}. |
8745 | 118 |
|
38430
254a021ed66e
tuned text about "value" and added note on comments.
nipkow
parents:
27015
diff
changeset
|
119 |
Comments\index{comment} must be in enclosed in \texttt{(* }and\texttt{ *)}. |
254a021ed66e
tuned text about "value" and added note on comments.
nipkow
parents:
27015
diff
changeset
|
120 |
|
25342 | 121 |
\section{Evaluation} |
122 |
\index{evaluation} |
|
123 |
||
124 |
Assuming you have processed the declarations and definitions of |
|
125 |
\texttt{ToyList} presented so far, you may want to test your |
|
126 |
functions by running them. For example, what is the value of |
|
127 |
@{term"rev(True#False#[])"}? Command |
|
128 |
*} |
|
129 |
||
130 |
value "rev (True # False # [])" |
|
131 |
||
132 |
text{* \noindent yields the correct result @{term"False # True # []"}. |
|
133 |
But we can go beyond mere functional programming and evaluate terms with |
|
134 |
variables in them, executing functions symbolically: *} |
|
135 |
||
38430
254a021ed66e
tuned text about "value" and added note on comments.
nipkow
parents:
27015
diff
changeset
|
136 |
value "rev (a # b # c # [])" |
25342 | 137 |
|
38432
439f50a241c1
Using type real does not require a separate logic now.
nipkow
parents:
38430
diff
changeset
|
138 |
text{*\noindent yields @{term"c # b # a # []"}. |
439f50a241c1
Using type real does not require a separate logic now.
nipkow
parents:
38430
diff
changeset
|
139 |
|
10885 | 140 |
\section{An Introductory Proof} |
8745 | 141 |
\label{sec:intro-proof} |
142 |
||
25342 | 143 |
Having convinced ourselves (as well as one can by testing) that our |
144 |
definitions capture our intentions, we are ready to prove a few simple |
|
16360 | 145 |
theorems. This will illustrate not just the basic proof commands but |
146 |
also the typical proof process. |
|
8745 | 147 |
|
11457 | 148 |
\subsubsection*{Main Goal.} |
8745 | 149 |
|
150 |
Our goal is to show that reversing a list twice produces the original |
|
11456 | 151 |
list. |
8745 | 152 |
*} |
153 |
||
154 |
theorem rev_rev [simp]: "rev(rev xs) = xs"; |
|
155 |
||
11428 | 156 |
txt{*\index{theorem@\isacommand {theorem} (command)|bold}% |
10795 | 157 |
\noindent |
11456 | 158 |
This \isacommand{theorem} command does several things: |
8745 | 159 |
\begin{itemize} |
160 |
\item |
|
11456 | 161 |
It establishes a new theorem to be proved, namely @{prop"rev(rev xs) = xs"}. |
8745 | 162 |
\item |
11456 | 163 |
It gives that theorem the name @{text"rev_rev"}, for later reference. |
8745 | 164 |
\item |
11456 | 165 |
It tells Isabelle (via the bracketed attribute \attrdx{simp}) to take the eventual theorem as a simplification rule: future proofs involving |
9792 | 166 |
simplification will replace occurrences of @{term"rev(rev xs)"} by |
167 |
@{term"xs"}. |
|
11457 | 168 |
\end{itemize} |
8745 | 169 |
The name and the simplification attribute are optional. |
12332 | 170 |
Isabelle's response is to print the initial proof state consisting |
171 |
of some header information (like how many subgoals there are) followed by |
|
13868 | 172 |
@{subgoals[display,indent=0]} |
12332 | 173 |
For compactness reasons we omit the header in this tutorial. |
174 |
Until we have finished a proof, the \rmindex{proof state} proper |
|
175 |
always looks like this: |
|
9723 | 176 |
\begin{isabelle} |
8745 | 177 |
~1.~$G\sb{1}$\isanewline |
178 |
~~\vdots~~\isanewline |
|
179 |
~$n$.~$G\sb{n}$ |
|
9723 | 180 |
\end{isabelle} |
13868 | 181 |
The numbered lines contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$ |
182 |
that we need to prove to establish the main goal.\index{subgoals} |
|
183 |
Initially there is only one subgoal, which is identical with the |
|
184 |
main goal. (If you always want to see the main goal as well, |
|
185 |
set the flag \isa{Proof.show_main_goal}\index{*show_main_goal (flag)} |
|
186 |
--- this flag used to be set by default.) |
|
8745 | 187 |
|
9792 | 188 |
Let us now get back to @{prop"rev(rev xs) = xs"}. Properties of recursively |
8745 | 189 |
defined functions are best established by induction. In this case there is |
11428 | 190 |
nothing obvious except induction on @{term"xs"}: |
8745 | 191 |
*} |
192 |
||
193 |
apply(induct_tac xs); |
|
194 |
||
11428 | 195 |
txt{*\noindent\index{*induct_tac (method)}% |
9792 | 196 |
This tells Isabelle to perform induction on variable @{term"xs"}. The suffix |
11428 | 197 |
@{term"tac"} stands for \textbf{tactic},\index{tactics} |
198 |
a synonym for ``theorem proving function''. |
|
8745 | 199 |
By default, induction acts on the first subgoal. The new proof state contains |
9792 | 200 |
two subgoals, namely the base case (@{term[source]Nil}) and the induction step |
201 |
(@{term[source]Cons}): |
|
10971 | 202 |
@{subgoals[display,indent=0,margin=65]} |
8745 | 203 |
|
11456 | 204 |
The induction step is an example of the general format of a subgoal:\index{subgoals} |
9723 | 205 |
\begin{isabelle} |
12327 | 206 |
~$i$.~{\isasymAnd}$x\sb{1}$~\dots$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion} |
10328 | 207 |
\end{isabelle}\index{$IsaAnd@\isasymAnd|bold} |
8745 | 208 |
The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be |
209 |
ignored most of the time, or simply treated as a list of variables local to |
|
10302 | 210 |
this subgoal. Their deeper significance is explained in Chapter~\ref{chap:rules}. |
11456 | 211 |
The {\it assumptions}\index{assumptions!of subgoal} |
212 |
are the local assumptions for this subgoal and {\it |
|
213 |
conclusion}\index{conclusion!of subgoal} is the actual proposition to be proved. |
|
214 |
Typical proof steps |
|
215 |
that add new assumptions are induction and case distinction. In our example |
|
9541 | 216 |
the only assumption is the induction hypothesis @{term"rev (rev list) = |
9792 | 217 |
list"}, where @{term"list"} is a variable name chosen by Isabelle. If there |
8745 | 218 |
are multiple assumptions, they are enclosed in the bracket pair |
219 |
\indexboldpos{\isasymlbrakk}{$Isabrl} and |
|
220 |
\indexboldpos{\isasymrbrakk}{$Isabrr} and separated by semicolons. |
|
221 |
||
222 |
Let us try to solve both goals automatically: |
|
223 |
*} |
|
224 |
||
225 |
apply(auto); |
|
226 |
||
227 |
txt{*\noindent |
|
228 |
This command tells Isabelle to apply a proof strategy called |
|
9792 | 229 |
@{text"auto"} to all subgoals. Essentially, @{text"auto"} tries to |
10978 | 230 |
simplify the subgoals. In our case, subgoal~1 is solved completely (thanks |
9792 | 231 |
to the equation @{prop"rev [] = []"}) and disappears; the simplified version |
8745 | 232 |
of subgoal~2 becomes the new subgoal~1: |
10971 | 233 |
@{subgoals[display,indent=0,margin=70]} |
8745 | 234 |
In order to simplify this subgoal further, a lemma suggests itself. |
235 |
*} |
|
236 |
(*<*) |
|
237 |
oops |
|
238 |
(*>*) |
|
239 |
||
11428 | 240 |
subsubsection{*First Lemma*} |
9723 | 241 |
|
8745 | 242 |
text{* |
11428 | 243 |
\indexbold{abandoning a proof}\indexbold{proofs!abandoning} |
244 |
After abandoning the above proof attempt (at the shell level type |
|
245 |
\commdx{oops}) we start a new proof: |
|
8745 | 246 |
*} |
247 |
||
248 |
lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)"; |
|
249 |
||
11428 | 250 |
txt{*\noindent The keywords \commdx{theorem} and |
251 |
\commdx{lemma} are interchangeable and merely indicate |
|
10971 | 252 |
the importance we attach to a proposition. Therefore we use the words |
11428 | 253 |
\emph{theorem} and \emph{lemma} pretty much interchangeably, too. |
8745 | 254 |
|
9792 | 255 |
There are two variables that we could induct on: @{term"xs"} and |
256 |
@{term"ys"}. Because @{text"@"} is defined by recursion on |
|
257 |
the first argument, @{term"xs"} is the correct one: |
|
8745 | 258 |
*} |
259 |
||
260 |
apply(induct_tac xs); |
|
261 |
||
262 |
txt{*\noindent |
|
263 |
This time not even the base case is solved automatically: |
|
264 |
*} |
|
265 |
||
266 |
apply(auto); |
|
267 |
||
268 |
txt{* |
|
10362 | 269 |
@{subgoals[display,indent=0,goals_limit=1]} |
270 |
Again, we need to abandon this proof attempt and prove another simple lemma |
|
271 |
first. In the future the step of abandoning an incomplete proof before |
|
272 |
embarking on the proof of a lemma usually remains implicit. |
|
8745 | 273 |
*} |
274 |
(*<*) |
|
275 |
oops |
|
276 |
(*>*) |
|
277 |
||
11428 | 278 |
subsubsection{*Second Lemma*} |
9723 | 279 |
|
8745 | 280 |
text{* |
11456 | 281 |
We again try the canonical proof procedure: |
8745 | 282 |
*} |
283 |
||
284 |
lemma app_Nil2 [simp]: "xs @ [] = xs"; |
|
285 |
apply(induct_tac xs); |
|
286 |
apply(auto); |
|
287 |
||
288 |
txt{* |
|
289 |
\noindent |
|
11456 | 290 |
It works, yielding the desired message @{text"No subgoals!"}: |
10362 | 291 |
@{goals[display,indent=0]} |
8745 | 292 |
We still need to confirm that the proof is now finished: |
293 |
*} |
|
294 |
||
10171 | 295 |
done |
8745 | 296 |
|
11428 | 297 |
text{*\noindent |
298 |
As a result of that final \commdx{done}, Isabelle associates the lemma just proved |
|
10171 | 299 |
with its name. In this tutorial, we sometimes omit to show that final \isacommand{done} |
300 |
if it is obvious from the context that the proof is finished. |
|
301 |
||
302 |
% Instead of \isacommand{apply} followed by a dot, you can simply write |
|
303 |
% \isacommand{by}\indexbold{by}, which we do most of the time. |
|
10971 | 304 |
Notice that in lemma @{thm[source]app_Nil2}, |
305 |
as printed out after the final \isacommand{done}, the free variable @{term"xs"} has been |
|
9792 | 306 |
replaced by the unknown @{text"?xs"}, just as explained in |
307 |
\S\ref{sec:variables}. |
|
8745 | 308 |
|
309 |
Going back to the proof of the first lemma |
|
310 |
*} |
|
311 |
||
312 |
lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)"; |
|
313 |
apply(induct_tac xs); |
|
314 |
apply(auto); |
|
315 |
||
316 |
txt{* |
|
317 |
\noindent |
|
9792 | 318 |
we find that this time @{text"auto"} solves the base case, but the |
8745 | 319 |
induction step merely simplifies to |
10362 | 320 |
@{subgoals[display,indent=0,goals_limit=1]} |
9792 | 321 |
Now we need to remember that @{text"@"} associates to the right, and that |
322 |
@{text"#"} and @{text"@"} have the same priority (namely the @{text"65"} |
|
8745 | 323 |
in their \isacommand{infixr} annotation). Thus the conclusion really is |
9723 | 324 |
\begin{isabelle} |
9792 | 325 |
~~~~~(rev~ys~@~rev~list)~@~(a~\#~[])~=~rev~ys~@~(rev~list~@~(a~\#~[])) |
9723 | 326 |
\end{isabelle} |
9792 | 327 |
and the missing lemma is associativity of @{text"@"}. |
9723 | 328 |
*} |
329 |
(*<*)oops(*>*) |
|
8745 | 330 |
|
11456 | 331 |
subsubsection{*Third Lemma*} |
8745 | 332 |
|
9723 | 333 |
text{* |
11456 | 334 |
Abandoning the previous attempt, the canonical proof procedure |
335 |
succeeds without further ado. |
|
8745 | 336 |
*} |
337 |
||
338 |
lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"; |
|
339 |
apply(induct_tac xs); |
|
10171 | 340 |
apply(auto); |
341 |
done |
|
8745 | 342 |
|
343 |
text{* |
|
344 |
\noindent |
|
11456 | 345 |
Now we can prove the first lemma: |
8745 | 346 |
*} |
347 |
||
348 |
lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)"; |
|
349 |
apply(induct_tac xs); |
|
10171 | 350 |
apply(auto); |
351 |
done |
|
8745 | 352 |
|
353 |
text{*\noindent |
|
11456 | 354 |
Finally, we prove our main theorem: |
8745 | 355 |
*} |
356 |
||
357 |
theorem rev_rev [simp]: "rev(rev xs) = xs"; |
|
358 |
apply(induct_tac xs); |
|
10171 | 359 |
apply(auto); |
360 |
done |
|
8745 | 361 |
|
362 |
text{*\noindent |
|
11456 | 363 |
The final \commdx{end} tells Isabelle to close the current theory because |
364 |
we are finished with its development:% |
|
365 |
\index{*rev (constant)|)}\index{append function|)} |
|
8745 | 366 |
*} |
367 |
||
368 |
end |