1 theory ToyList = PreList:
4 HOL already has a predefined theory of lists called @{text"List"} ---
5 @{text"ToyList"} is merely a small fragment of it chosen as an example. In
6 contrast to what is recommended in \S\ref{sec:Basic:Theories},
7 @{text"ToyList"} is not based on @{text"Main"} but on @{text"PreList"}, a
8 theory that contains pretty much everything but lists, thus avoiding
9 ambiguities caused by defining lists twice.
12 datatype 'a list = Nil ("[]")
13 | Cons 'a "'a list" (infixr "#" 65);
16 The datatype\index{*datatype} \isaindexbold{list} introduces two
17 constructors \isaindexbold{Nil} and \isaindexbold{Cons}, the
18 empty~list and the operator that adds an element to the front of a list. For
19 example, the term \isa{Cons True (Cons False Nil)} is a value of
20 type @{typ"bool list"}, namely the list with the elements @{term"True"} and
21 @{term"False"}. Because this notation becomes unwieldy very quickly, the
22 datatype declaration is annotated with an alternative syntax: instead of
23 @{term[source]Nil} and \isa{Cons x xs} we can write
24 @{term"[]"}\index{$HOL2list@\texttt{[]}|bold} and
25 @{term"x # xs"}\index{$HOL2list@\texttt{\#}|bold}. In fact, this
26 alternative syntax is the standard syntax. Thus the list \isa{Cons True
27 (Cons False Nil)} becomes @{term"True # False # []"}. The annotation
28 \isacommand{infixr}\indexbold{*infixr} means that @{text"#"} associates to
29 the right, i.e.\ the term @{term"x # y # z"} is read as @{text"x # (y # z)"}
30 and not as @{text"(x # y) # z"}.
33 Syntax annotations are a powerful but completely optional feature. You
34 could drop them from theory @{text"ToyList"} and go back to the identifiers
35 @{term[source]Nil} and @{term[source]Cons}. However, lists are such a
37 that their syntax is highly customized. We recommend that novices should
38 not use syntax annotations in their own theories.
40 Next, two functions @{text"app"} and \isaindexbold{rev} are declared:
43 consts app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65)
44 rev :: "'a list \<Rightarrow> 'a list";
48 In contrast to ML, Isabelle insists on explicit declarations of all functions
49 (keyword \isacommand{consts}). (Apart from the declaration-before-use
50 restriction, the order of items in a theory file is unconstrained.) Function
51 @{term"app"} is annotated with concrete syntax too. Instead of the prefix
52 syntax \isa{app xs ys} the infix
53 @{term"xs @ ys"}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred
54 form. Both functions are defined recursively:
59 "(x # xs) @ ys = x # (xs @ ys)";
63 "rev (x # xs) = (rev xs) @ (x # [])";
67 The equations for @{term"app"} and @{term"rev"} hardly need comments:
68 @{term"app"} appends two lists and @{term"rev"} reverses a list. The keyword
69 \isacommand{primrec}\index{*primrec} indicates that the recursion is of a
70 particularly primitive kind where each recursive call peels off a datatype
71 constructor from one of the arguments. Thus the
72 recursion always terminates, i.e.\ the function is \bfindex{total}.
74 The termination requirement is absolutely essential in HOL, a logic of total
75 functions. If we were to drop it, inconsistencies would quickly arise: the
76 ``definition'' $f(n) = f(n)+1$ immediately leads to $0 = 1$ by subtracting
78 % However, this is a subtle issue that we cannot discuss here further.
81 As we have indicated, the desire for total functions is not a gratuitously
82 imposed restriction but an essential characteristic of HOL. It is only
83 because of totality that reasoning in HOL is comparatively easy. More
84 generally, the philosophy in HOL is not to allow arbitrary axioms (such as
85 function definitions whose totality has not been proved) because they
86 quickly lead to inconsistencies. Instead, fixed constructs for introducing
87 types and functions are offered (such as \isacommand{datatype} and
88 \isacommand{primrec}) which are guaranteed to preserve consistency.
91 A remark about syntax. The textual definition of a theory follows a fixed
92 syntax with keywords like \isacommand{datatype} and \isacommand{end} (see
93 Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list).
94 Embedded in this syntax are the types and formulae of HOL, whose syntax is
95 extensible, e.g.\ by new user-defined infix operators
96 (see~\ref{sec:infix-syntax}). To distinguish the two levels, everything
97 HOL-specific (terms and types) should be enclosed in
98 \texttt{"}\dots\texttt{"}.
99 To lessen this burden, quotation marks around a single identifier can be
100 dropped, unless the identifier happens to be a keyword, as in
103 consts "end" :: "'a list \<Rightarrow> 'a"
106 When Isabelle prints a syntax error message, it refers to the HOL syntax as
107 the \bfindex{inner syntax} and the enclosing theory language as the \bfindex{outer syntax}.
110 \section{An introductory proof}
111 \label{sec:intro-proof}
113 Assuming you have input the declarations and definitions of \texttt{ToyList}
114 presented so far, we are ready to prove a few simple theorems. This will
115 illustrate not just the basic proof commands but also the typical proof
118 \subsubsection*{Main goal: @{text"rev(rev xs) = xs"}}
120 Our goal is to show that reversing a list twice produces the original
124 theorem rev_rev [simp]: "rev(rev xs) = xs";
126 txt{*\index{*theorem|bold}\index{*simp (attribute)|bold}
129 establishes a new theorem to be proved, namely @{prop"rev(rev xs) = xs"},
131 gives that theorem the name @{text"rev_rev"} by which it can be
134 and tells Isabelle (via @{text"[simp]"}) to use the theorem (once it has been
135 proved) as a simplification rule, i.e.\ all future proofs involving
136 simplification will replace occurrences of @{term"rev(rev xs)"} by
139 The name and the simplification attribute are optional.
141 Isabelle's response is to print
143 proof(prove):~step~0\isanewline
145 goal~(theorem~rev\_rev):\isanewline
146 rev~(rev~xs)~=~xs\isanewline
147 ~1.~rev~(rev~xs)~=~xs
149 The first three lines tell us that we are 0 steps into the proof of
150 theorem @{text"rev_rev"}; for compactness reasons we rarely show these
151 initial lines in this tutorial. The remaining lines display the current
153 Until we have finished a proof, the proof state always looks like this:
156 ~1.~$G\sb{1}$\isanewline
157 ~~\vdots~~\isanewline
161 is the overall goal that we are trying to prove, and the numbered lines
162 contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$ that we need to prove to
163 establish $G$. At @{text"step 0"} there is only one subgoal, which is
164 identical with the overall goal. Normally $G$ is constant and only serves as
165 a reminder. Hence we rarely show it in this tutorial.
167 Let us now get back to @{prop"rev(rev xs) = xs"}. Properties of recursively
168 defined functions are best established by induction. In this case there is
169 not much choice except to induct on @{term"xs"}:
172 apply(induct_tac xs);
174 txt{*\noindent\index{*induct_tac}%
175 This tells Isabelle to perform induction on variable @{term"xs"}. The suffix
176 @{term"tac"} stands for ``tactic'', a synonym for ``theorem proving function''.
177 By default, induction acts on the first subgoal. The new proof state contains
178 two subgoals, namely the base case (@{term[source]Nil}) and the induction step
179 (@{term[source]Cons}):
181 ~1.~rev~(rev~[])~=~[]\isanewline
182 ~2.~{\isasymAnd}a~list.~rev(rev~list)~=~list~{\isasymLongrightarrow}~rev(rev(a~\#~list))~=~a~\#~list
185 The induction step is an example of the general format of a subgoal:
187 ~$i$.~{\isasymAnd}$x\sb{1}$~\dots~$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion}
188 \end{isabelle}\index{$IsaAnd@\isasymAnd|bold}
189 The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be
190 ignored most of the time, or simply treated as a list of variables local to
191 this subgoal. Their deeper significance is explained in Chapter~\ref{chap:rules}.
192 The {\it assumptions} are the local assumptions for this subgoal and {\it
193 conclusion} is the actual proposition to be proved. Typical proof steps
194 that add new assumptions are induction or case distinction. In our example
195 the only assumption is the induction hypothesis @{term"rev (rev list) =
196 list"}, where @{term"list"} is a variable name chosen by Isabelle. If there
197 are multiple assumptions, they are enclosed in the bracket pair
198 \indexboldpos{\isasymlbrakk}{$Isabrl} and
199 \indexboldpos{\isasymrbrakk}{$Isabrr} and separated by semicolons.
201 Let us try to solve both goals automatically:
207 This command tells Isabelle to apply a proof strategy called
208 @{text"auto"} to all subgoals. Essentially, @{text"auto"} tries to
209 ``simplify'' the subgoals. In our case, subgoal~1 is solved completely (thanks
210 to the equation @{prop"rev [] = []"}) and disappears; the simplified version
211 of subgoal~2 becomes the new subgoal~1:
213 ~1.~\dots~rev(rev~list)~=~list~{\isasymLongrightarrow}~rev(rev~list~@~a~\#~[])~=~a~\#~list
215 In order to simplify this subgoal further, a lemma suggests itself.
221 subsubsection{*First lemma: @{text"rev(xs @ ys) = (rev ys) @ (rev xs)"}*}
224 After abandoning the above proof attempt\indexbold{abandon
225 proof}\indexbold{proof!abandon} (at the shell level type
226 \isacommand{oops}\indexbold{*oops}) we start a new proof:
229 lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
231 txt{*\noindent The keywords \isacommand{theorem}\index{*theorem} and
232 \isacommand{lemma}\indexbold{*lemma} are interchangable and merely indicate
233 the importance we attach to a proposition. In general, we use the words
234 \emph{theorem}\index{theorem} and \emph{lemma}\index{lemma} pretty much
237 There are two variables that we could induct on: @{term"xs"} and
238 @{term"ys"}. Because @{text"@"} is defined by recursion on
239 the first argument, @{term"xs"} is the correct one:
242 apply(induct_tac xs);
245 This time not even the base case is solved automatically:
252 ~1.~rev~ys~=~rev~ys~@~[]\isanewline
255 Again, we need to abandon this proof attempt and prove another simple lemma first.
256 In the future the step of abandoning an incomplete proof before embarking on
257 the proof of a lemma usually remains implicit.
263 subsubsection{*Second lemma: @{text"xs @ [] = xs"}*}
266 This time the canonical proof procedure
269 lemma app_Nil2 [simp]: "xs @ [] = xs";
270 apply(induct_tac xs);
275 leads to the desired message @{text"No subgoals!"}:
277 xs~@~[]~=~xs\isanewline
281 We still need to confirm that the proof is now finished:
286 text{*\noindent\indexbold{done}%
287 As a result of that final \isacommand{done}, Isabelle associates the lemma just proved
288 with its name. In this tutorial, we sometimes omit to show that final \isacommand{done}
289 if it is obvious from the context that the proof is finished.
291 % Instead of \isacommand{apply} followed by a dot, you can simply write
292 % \isacommand{by}\indexbold{by}, which we do most of the time.
293 Notice that in lemma @{thm[source]app_Nil2}
294 (as printed out after the final \isacommand{done}) the free variable @{term"xs"} has been
295 replaced by the unknown @{text"?xs"}, just as explained in
296 \S\ref{sec:variables}.
298 Going back to the proof of the first lemma
301 lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
302 apply(induct_tac xs);
307 we find that this time @{text"auto"} solves the base case, but the
308 induction step merely simplifies to
310 ~1.~{\isasymAnd}a~list.\isanewline
311 ~~~~~~~rev~(list~@~ys)~=~rev~ys~@~rev~list~{\isasymLongrightarrow}\isanewline
312 ~~~~~~~(rev~ys~@~rev~list)~@~a~\#~[]~=~rev~ys~@~rev~list~@~a~\#~[]
314 Now we need to remember that @{text"@"} associates to the right, and that
315 @{text"#"} and @{text"@"} have the same priority (namely the @{text"65"}
316 in their \isacommand{infixr} annotation). Thus the conclusion really is
318 ~~~~~(rev~ys~@~rev~list)~@~(a~\#~[])~=~rev~ys~@~(rev~list~@~(a~\#~[]))
320 and the missing lemma is associativity of @{text"@"}.
324 subsubsection{*Third lemma: @{text"(xs @ ys) @ zs = xs @ (ys @ zs)"}*}
327 Abandoning the previous proof, the canonical proof procedure
330 lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)";
331 apply(induct_tac xs);
337 succeeds without further ado.
338 Now we can go back and prove the first lemma
341 lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
342 apply(induct_tac xs);
347 and then solve our main theorem:
350 theorem rev_rev [simp]: "rev(rev xs) = xs";
351 apply(induct_tac xs);
356 The final \isacommand{end} tells Isabelle to close the current theory because
357 we are finished with its development: