summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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