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 \index{datatype@\isacommand {datatype} (command)}
17 The datatype \tydx{list} introduces two
18 constructors \cdx{Nil} and \cdx{Cons}, the
19 empty~list and the operator that adds an element to the front of a list. For
20 example, the term \isa{Cons True (Cons False Nil)} is a value of
21 type @{typ"bool list"}, namely the list with the elements @{term"True"} and
22 @{term"False"}. Because this notation quickly becomes unwieldy, the
23 datatype declaration is annotated with an alternative syntax: instead of
24 @{term[source]Nil} and \isa{Cons x xs} we can write
25 @{term"[]"}\index{$HOL2list@\texttt{[]}|bold} and
26 @{term"x # xs"}\index{$HOL2list@\texttt{\#}|bold}. In fact, this
27 alternative syntax is the familiar one. Thus the list \isa{Cons True
28 (Cons False Nil)} becomes @{term"True # False # []"}. The annotation
29 \isacommand{infixr}\index{infixr@\isacommand{infixr} (annotation)}
30 means that @{text"#"} associates to
31 the right: the term @{term"x # y # z"} is read as @{text"x # (y # z)"}
32 and not as @{text"(x # y) # z"}.
33 The @{text 65} is the priority of the infix @{text"#"}.
36 Syntax annotations are a powerful but optional feature. You
37 could drop them from theory @{text"ToyList"} and go back to the identifiers
38 @{term[source]Nil} and @{term[source]Cons}.
39 We recommend that novices avoid using
40 syntax annotations in their own theories.
42 Next, two functions @{text"app"} and \cdx{rev} are declared:
45 consts app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65)
46 rev :: "'a list \<Rightarrow> 'a list";
50 In contrast to many functional programming languages,
51 Isabelle insists on explicit declarations of all functions
52 (keyword \isacommand{consts}). Apart from the declaration-before-use
53 restriction, the order of items in a theory file is unconstrained. Function
54 @{text"app"} is annotated with concrete syntax too. Instead of the
55 prefix syntax @{text"app xs ys"} the infix
56 @{term"xs @ ys"}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred
57 form. Both functions are defined recursively:
62 "(x # xs) @ ys = x # (xs @ ys)";
66 "rev (x # xs) = (rev xs) @ (x # [])";
70 The equations for @{text"app"} and @{term"rev"} hardly need comments:
71 @{text"app"} appends two lists and @{term"rev"} reverses a list. The
72 keyword \commdx{primrec} indicates that the recursion is
73 of a particularly primitive kind where each recursive call peels off a datatype
74 constructor from one of the arguments. Thus the
75 recursion always terminates, i.e.\ the function is \textbf{total}.
76 \index{functions!total}
78 The termination requirement is absolutely essential in HOL, a logic of total
79 functions. If we were to drop it, inconsistencies would quickly arise: the
80 ``definition'' $f(n) = f(n)+1$ immediately leads to $0 = 1$ by subtracting
82 % However, this is a subtle issue that we cannot discuss here further.
85 As we have indicated, the requirement for total functions is not a gratuitous
86 restriction but an essential characteristic of HOL\@. It is only
87 because of totality that reasoning in HOL is comparatively easy. More
88 generally, the philosophy in HOL is not to allow arbitrary axioms (such as
89 function definitions whose totality has not been proved) because they
90 quickly lead to inconsistencies. Instead, fixed constructs for introducing
91 types and functions are offered (such as \isacommand{datatype} and
92 \isacommand{primrec}) which are guaranteed to preserve consistency.
95 A remark about syntax. The textual definition of a theory follows a fixed
96 syntax with keywords like \isacommand{datatype} and \isacommand{end}.
97 % (see Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list).
98 Embedded in this syntax are the types and formulae of HOL, whose syntax is
99 extensible (see \S\ref{sec:syntax-anno}), e.g.\ by new user-defined infix operators.
100 To distinguish the two levels, everything
101 HOL-specific (terms and types) should be enclosed in
102 \texttt{"}\dots\texttt{"}.
103 To lessen this burden, quotation marks around a single identifier can be
104 dropped, unless the identifier happens to be a keyword, as in
107 consts "end" :: "'a list \<Rightarrow> 'a"
110 When Isabelle prints a syntax error message, it refers to the HOL syntax as
111 the \bfindex{inner syntax} and the enclosing theory language as the \bfindex{outer syntax}.
114 \section{An Introductory Proof}
115 \label{sec:intro-proof}
117 Assuming you have input the declarations and definitions of \texttt{ToyList}
118 presented so far, we are ready to prove a few simple theorems. This will
119 illustrate not just the basic proof commands but also the typical proof
122 \subsubsection*{Main Goal: @{text"rev(rev xs) = xs"}.}
124 Our goal is to show that reversing a list twice produces the original
128 theorem rev_rev [simp]: "rev(rev xs) = xs";
130 txt{*\index{theorem@\isacommand {theorem} (command)|bold}%
131 \index{*simp (attribute)|bold}
133 does several things. It
136 establishes a new theorem to be proved, namely @{prop"rev(rev xs) = xs"},
138 gives that theorem the name @{text"rev_rev"} by which it can be
141 and tells Isabelle (via @{text"[simp]"}) to use the theorem (once it has been
142 proved) as a simplification rule, i.e.\ all future proofs involving
143 simplification will replace occurrences of @{term"rev(rev xs)"} by
146 The name and the simplification attribute are optional.
148 Isabelle's response is to print
150 proof(prove):~step~0\isanewline
152 goal~(theorem~rev\_rev):\isanewline
153 rev~(rev~xs)~=~xs\isanewline
154 ~1.~rev~(rev~xs)~=~xs
156 The first three lines tell us that we are 0 steps into the proof of
157 theorem @{text"rev_rev"}; for compactness reasons we rarely show these
158 initial lines in this tutorial. The remaining lines display the current
160 Until we have finished a proof, the proof state always looks like this:
163 ~1.~$G\sb{1}$\isanewline
164 ~~\vdots~~\isanewline
168 is the overall goal that we are trying to prove, and the numbered lines
169 contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$ that we need to prove to
170 establish $G$. At @{text"step 0"} there is only one subgoal, which is
171 identical with the overall goal. Normally $G$ is constant and only serves as
172 a reminder. Hence we rarely show it in this tutorial.
174 Let us now get back to @{prop"rev(rev xs) = xs"}. Properties of recursively
175 defined functions are best established by induction. In this case there is
176 nothing obvious except induction on @{term"xs"}:
179 apply(induct_tac xs);
181 txt{*\noindent\index{*induct_tac (method)}%
182 This tells Isabelle to perform induction on variable @{term"xs"}. The suffix
183 @{term"tac"} stands for \textbf{tactic},\index{tactics}
184 a synonym for ``theorem proving function''.
185 By default, induction acts on the first subgoal. The new proof state contains
186 two subgoals, namely the base case (@{term[source]Nil}) and the induction step
187 (@{term[source]Cons}):
188 @{subgoals[display,indent=0,margin=65]}
190 The induction step is an example of the general format of a subgoal:
192 ~$i$.~{\isasymAnd}$x\sb{1}$~\dots~$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion}
193 \end{isabelle}\index{$IsaAnd@\isasymAnd|bold}
194 The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be
195 ignored most of the time, or simply treated as a list of variables local to
196 this subgoal. Their deeper significance is explained in Chapter~\ref{chap:rules}.
197 The {\it assumptions} are the local assumptions for this subgoal and {\it
198 conclusion} is the actual proposition to be proved. Typical proof steps
199 that add new assumptions are induction or case distinction. In our example
200 the only assumption is the induction hypothesis @{term"rev (rev list) =
201 list"}, where @{term"list"} is a variable name chosen by Isabelle. If there
202 are multiple assumptions, they are enclosed in the bracket pair
203 \indexboldpos{\isasymlbrakk}{$Isabrl} and
204 \indexboldpos{\isasymrbrakk}{$Isabrr} and separated by semicolons.
206 Let us try to solve both goals automatically:
212 This command tells Isabelle to apply a proof strategy called
213 @{text"auto"} to all subgoals. Essentially, @{text"auto"} tries to
214 simplify the subgoals. In our case, subgoal~1 is solved completely (thanks
215 to the equation @{prop"rev [] = []"}) and disappears; the simplified version
216 of subgoal~2 becomes the new subgoal~1:
217 @{subgoals[display,indent=0,margin=70]}
218 In order to simplify this subgoal further, a lemma suggests itself.
224 subsubsection{*First Lemma*}
227 \indexbold{abandoning a proof}\indexbold{proofs!abandoning}
228 After abandoning the above proof attempt (at the shell level type
229 \commdx{oops}) we start a new proof:
232 lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
234 txt{*\noindent The keywords \commdx{theorem} and
235 \commdx{lemma} are interchangeable and merely indicate
236 the importance we attach to a proposition. Therefore we use the words
237 \emph{theorem} and \emph{lemma} pretty much interchangeably, too.
239 There are two variables that we could induct on: @{term"xs"} and
240 @{term"ys"}. Because @{text"@"} is defined by recursion on
241 the first argument, @{term"xs"} is the correct one:
244 apply(induct_tac xs);
247 This time not even the base case is solved automatically:
253 @{subgoals[display,indent=0,goals_limit=1]}
254 Again, we need to abandon this proof attempt and prove another simple lemma
255 first. In the future the step of abandoning an incomplete proof before
256 embarking on the proof of a lemma usually remains implicit.
262 subsubsection{*Second Lemma*}
265 This time the canonical proof procedure
268 lemma app_Nil2 [simp]: "xs @ [] = xs";
269 apply(induct_tac xs);
274 leads to the desired message @{text"No subgoals!"}:
275 @{goals[display,indent=0]}
276 We still need to confirm that the proof is now finished:
282 As a result of that final \commdx{done}, Isabelle associates the lemma just proved
283 with its name. In this tutorial, we sometimes omit to show that final \isacommand{done}
284 if it is obvious from the context that the proof is finished.
286 % Instead of \isacommand{apply} followed by a dot, you can simply write
287 % \isacommand{by}\indexbold{by}, which we do most of the time.
288 Notice that in lemma @{thm[source]app_Nil2},
289 as printed out after the final \isacommand{done}, the free variable @{term"xs"} has been
290 replaced by the unknown @{text"?xs"}, just as explained in
291 \S\ref{sec:variables}.
293 Going back to the proof of the first lemma
296 lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
297 apply(induct_tac xs);
302 we find that this time @{text"auto"} solves the base case, but the
303 induction step merely simplifies to
304 @{subgoals[display,indent=0,goals_limit=1]}
305 Now we need to remember that @{text"@"} associates to the right, and that
306 @{text"#"} and @{text"@"} have the same priority (namely the @{text"65"}
307 in their \isacommand{infixr} annotation). Thus the conclusion really is
309 ~~~~~(rev~ys~@~rev~list)~@~(a~\#~[])~=~rev~ys~@~(rev~list~@~(a~\#~[]))
311 and the missing lemma is associativity of @{text"@"}.
315 subsubsection{*Third Lemma: @{text"(xs @ ys) @ zs = xs @ (ys @ zs)"}*}
318 Abandoning the previous proof, the canonical proof procedure
321 lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)";
322 apply(induct_tac xs);
328 succeeds without further ado.
329 Now we can prove the first lemma
332 lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
333 apply(induct_tac xs);
338 and then prove our main theorem:
341 theorem rev_rev [simp]: "rev(rev xs) = xs";
342 apply(induct_tac xs);
347 The final \isacommand{end} tells Isabelle to close the current theory because
348 we are finished with its development: