doc-src/TutorialI/ToyList/ToyList.thy
 author nipkow Tue Mar 18 17:54:27 2003 +0100 (2003-03-18) changeset 13868 01b516b64233 parent 13191 05a9929ee10e child 15136 1275417e3930 permissions -rw-r--r--
*** empty log message ***
1 theory ToyList = PreList:
3 text{*\noindent
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.
10 *}
12 datatype 'a list = Nil                          ("[]")
13                  | Cons 'a "'a list"            (infixr "#" 65);
15 text{*\noindent
16 The datatype\index{datatype@\isacommand {datatype} (command)}
17 \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"#"}.
35 \begin{warn}
36   Syntax annotations can be powerful, but they are difficult to master and
37   are never necessary.  You
38   could drop them from theory @{text"ToyList"} and go back to the identifiers
39   @{term[source]Nil} and @{term[source]Cons}.
40   Novices should avoid using
41   syntax annotations in their own theories.
42 \end{warn}
43 Next, two functions @{text"app"} and \cdx{rev} are declared:
44 *}
46 consts app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"   (infixr "@" 65)
47        rev :: "'a list \<Rightarrow> 'a list";
49 text{*
50 \noindent
51 In contrast to many functional programming languages,
52 Isabelle insists on explicit declarations of all functions
53 (keyword \commdx{consts}).  Apart from the declaration-before-use
54 restriction, the order of items in a theory file is unconstrained. Function
55 @{text"app"} is annotated with concrete syntax too. Instead of the
56 prefix syntax @{text"app xs ys"} the infix
57 @{term"xs @ ys"}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred 58 form. Both functions are defined recursively: 59 *} 61 primrec 62 "[] @ ys = ys" 63 "(x # xs) @ ys = x # (xs @ ys)"; 65 primrec 66 "rev [] = []" 67 "rev (x # xs) = (rev xs) @ (x # [])"; 69 text{* 70 \noindent\index{*rev (constant)|(}\index{append function|(} 71 The equations for @{text"app"} and @{term"rev"} hardly need comments: 72 @{text"app"} appends two lists and @{term"rev"} reverses a list. The 73 keyword \commdx{primrec} indicates that the recursion is 74 of a particularly primitive kind where each recursive call peels off a datatype 75 constructor from one of the arguments. Thus the 76 recursion always terminates, i.e.\ the function is \textbf{total}. 77 \index{functions!total} 79 The termination requirement is absolutely essential in HOL, a logic of total 80 functions. If we were to drop it, inconsistencies would quickly arise: the 81 definition''$f(n) = f(n)+1$immediately leads to$0 = 1$by subtracting 82$f(n)$on both sides. 83 % However, this is a subtle issue that we cannot discuss here further. 85 \begin{warn} 86 As we have indicated, the requirement for total functions is 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 to refrain from asserting 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. 93 \end{warn} 95 \index{syntax}% 96 A remark about syntax. The textual definition of a theory follows a fixed 97 syntax with keywords like \isacommand{datatype} and \isacommand{end}. 98 % (see Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list). 99 Embedded in this syntax are the types and formulae of HOL, whose syntax is 100 extensible (see \S\ref{sec:concrete-syntax}), e.g.\ by new user-defined infix operators. 101 To distinguish the two levels, everything 102 HOL-specific (terms and types) should be enclosed in 103 \texttt{"}\dots\texttt{"}. 104 To lessen this burden, quotation marks around a single identifier can be 105 dropped, unless the identifier happens to be a keyword, as in 106 *} 108 consts "end" :: "'a list \<Rightarrow> 'a" 110 text{*\noindent 111 When Isabelle prints a syntax error message, it refers to the HOL syntax as 112 the \textbf{inner syntax} and the enclosing theory language as the \textbf{outer syntax}. 115 \section{An Introductory Proof} 116 \label{sec:intro-proof} 118 Assuming you have input the declarations and definitions of \texttt{ToyList} 119 presented so far, we are ready to prove a few simple theorems. This will 120 illustrate not just the basic proof commands but also the typical proof 121 process. 123 \subsubsection*{Main Goal.} 125 Our goal is to show that reversing a list twice produces the original 126 list. 127 *} 129 theorem rev_rev [simp]: "rev(rev xs) = xs"; 131 txt{*\index{theorem@\isacommand {theorem} (command)|bold}% 132 \noindent 133 This \isacommand{theorem} command does several things: 134 \begin{itemize} 135 \item 136 It establishes a new theorem to be proved, namely @{prop"rev(rev xs) = xs"}. 137 \item 138 It gives that theorem the name @{text"rev_rev"}, for later reference. 139 \item 140 It tells Isabelle (via the bracketed attribute \attrdx{simp}) to take the eventual theorem as a simplification rule: future proofs involving 141 simplification will replace occurrences of @{term"rev(rev xs)"} by 142 @{term"xs"}. 143 \end{itemize} 144 The name and the simplification attribute are optional. 145 Isabelle's response is to print the initial proof state consisting 146 of some header information (like how many subgoals there are) followed by 147 @{subgoals[display,indent=0]} 148 For compactness reasons we omit the header in this tutorial. 149 Until we have finished a proof, the \rmindex{proof state} proper 150 always looks like this: 151 \begin{isabelle} 152 ~1.~$G\sb{1}$\isanewline 153 ~~\vdots~~\isanewline 154 ~$n$.~$G\sb{n}$155 \end{isabelle} 156 The numbered lines contain the subgoals$G\sb{1}$, \dots,$G\sb{n}$157 that we need to prove to establish the main goal.\index{subgoals} 158 Initially there is only one subgoal, which is identical with the 159 main goal. (If you always want to see the main goal as well, 160 set the flag \isa{Proof.show_main_goal}\index{*show_main_goal (flag)} 161 --- this flag used to be set by default.) 163 Let us now get back to @{prop"rev(rev xs) = xs"}. Properties of recursively 164 defined functions are best established by induction. In this case there is 165 nothing obvious except induction on @{term"xs"}: 166 *} 168 apply(induct_tac xs); 170 txt{*\noindent\index{*induct_tac (method)}% 171 This tells Isabelle to perform induction on variable @{term"xs"}. The suffix 172 @{term"tac"} stands for \textbf{tactic},\index{tactics} 173 a synonym for theorem proving function''. 174 By default, induction acts on the first subgoal. The new proof state contains 175 two subgoals, namely the base case (@{term[source]Nil}) and the induction step 176 (@{term[source]Cons}): 177 @{subgoals[display,indent=0,margin=65]} 179 The induction step is an example of the general format of a subgoal:\index{subgoals} 180 \begin{isabelle} 181 ~$i$.~{\isasymAnd}$x\sb{1}$~\dots$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion} 182 \end{isabelle}\index{$IsaAnd@\isasymAnd|bold}
183 The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be
184 ignored most of the time, or simply treated as a list of variables local to
185 this subgoal. Their deeper significance is explained in Chapter~\ref{chap:rules}.
186 The {\it assumptions}\index{assumptions!of subgoal}
187 are the local assumptions for this subgoal and {\it
188   conclusion}\index{conclusion!of subgoal} is the actual proposition to be proved.
189 Typical proof steps
190 that add new assumptions are induction and case distinction. In our example
191 the only assumption is the induction hypothesis @{term"rev (rev list) =
192   list"}, where @{term"list"} is a variable name chosen by Isabelle. If there
193 are multiple assumptions, they are enclosed in the bracket pair
194 \indexboldpos{\isasymlbrakk}{$Isabrl} and 195 \indexboldpos{\isasymrbrakk}{$Isabrr} and separated by semicolons.
197 Let us try to solve both goals automatically:
198 *}
200 apply(auto);
202 txt{*\noindent
203 This command tells Isabelle to apply a proof strategy called
204 @{text"auto"} to all subgoals. Essentially, @{text"auto"} tries to
205 simplify the subgoals.  In our case, subgoal~1 is solved completely (thanks
206 to the equation @{prop"rev [] = []"}) and disappears; the simplified version
207 of subgoal~2 becomes the new subgoal~1:
208 @{subgoals[display,indent=0,margin=70]}
209 In order to simplify this subgoal further, a lemma suggests itself.
210 *}
211 (*<*)
212 oops
213 (*>*)
215 subsubsection{*First Lemma*}
217 text{*
218 \indexbold{abandoning a proof}\indexbold{proofs!abandoning}
219 After abandoning the above proof attempt (at the shell level type
220 \commdx{oops}) we start a new proof:
221 *}
223 lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
225 txt{*\noindent The keywords \commdx{theorem} and
226 \commdx{lemma} are interchangeable and merely indicate
227 the importance we attach to a proposition.  Therefore we use the words
228 \emph{theorem} and \emph{lemma} pretty much interchangeably, too.
230 There are two variables that we could induct on: @{term"xs"} and
231 @{term"ys"}. Because @{text"@"} is defined by recursion on
232 the first argument, @{term"xs"} is the correct one:
233 *}
235 apply(induct_tac xs);
237 txt{*\noindent
238 This time not even the base case is solved automatically:
239 *}
241 apply(auto);
243 txt{*
244 @{subgoals[display,indent=0,goals_limit=1]}
245 Again, we need to abandon this proof attempt and prove another simple lemma
246 first. In the future the step of abandoning an incomplete proof before
247 embarking on the proof of a lemma usually remains implicit.
248 *}
249 (*<*)
250 oops
251 (*>*)
253 subsubsection{*Second Lemma*}
255 text{*
256 We again try the canonical proof procedure:
257 *}
259 lemma app_Nil2 [simp]: "xs @ [] = xs";
260 apply(induct_tac xs);
261 apply(auto);
263 txt{*
264 \noindent
265 It works, yielding the desired message @{text"No subgoals!"}:
266 @{goals[display,indent=0]}
267 We still need to confirm that the proof is now finished:
268 *}
270 done
272 text{*\noindent
273 As a result of that final \commdx{done}, Isabelle associates the lemma just proved
274 with its name. In this tutorial, we sometimes omit to show that final \isacommand{done}
275 if it is obvious from the context that the proof is finished.
277 % Instead of \isacommand{apply} followed by a dot, you can simply write
278 % \isacommand{by}\indexbold{by}, which we do most of the time.
279 Notice that in lemma @{thm[source]app_Nil2},
280 as printed out after the final \isacommand{done}, the free variable @{term"xs"} has been
281 replaced by the unknown @{text"?xs"}, just as explained in
282 \S\ref{sec:variables}.
284 Going back to the proof of the first lemma
285 *}
287 lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
288 apply(induct_tac xs);
289 apply(auto);
291 txt{*
292 \noindent
293 we find that this time @{text"auto"} solves the base case, but the
294 induction step merely simplifies to
295 @{subgoals[display,indent=0,goals_limit=1]}
296 Now we need to remember that @{text"@"} associates to the right, and that
297 @{text"#"} and @{text"@"} have the same priority (namely the @{text"65"}
298 in their \isacommand{infixr} annotation). Thus the conclusion really is
299 \begin{isabelle}
300 ~~~~~(rev~ys~@~rev~list)~@~(a~\#~[])~=~rev~ys~@~(rev~list~@~(a~\#~[]))
301 \end{isabelle}
302 and the missing lemma is associativity of @{text"@"}.
303 *}
304 (*<*)oops(*>*)
306 subsubsection{*Third Lemma*}
308 text{*
309 Abandoning the previous attempt, the canonical proof procedure
310 succeeds without further ado.
311 *}
313 lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)";
314 apply(induct_tac xs);
315 apply(auto);
316 done
318 text{*
319 \noindent
320 Now we can prove the first lemma:
321 *}
323 lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
324 apply(induct_tac xs);
325 apply(auto);
326 done
328 text{*\noindent
329 Finally, we prove our main theorem:
330 *}
332 theorem rev_rev [simp]: "rev(rev xs) = xs";
333 apply(induct_tac xs);
334 apply(auto);
335 done
337 text{*\noindent
338 The final \commdx{end} tells Isabelle to close the current theory because
339 we are finished with its development:%
340 \index{*rev (constant)|)}\index{append function|)}
341 *}
343 end