doc-src/TutorialI/ToyList/ToyList.thy
author nipkow
Wed Dec 13 09:39:53 2000 +0100 (2000-12-13)
changeset 10654 458068404143
parent 10362 c6b197ccf1f1
child 10790 520dd8696927
permissions -rw-r--r--
*** empty log message ***
nipkow@8745
     1
theory ToyList = PreList:
nipkow@8745
     2
nipkow@8745
     3
text{*\noindent
nipkow@9792
     4
HOL already has a predefined theory of lists called @{text"List"} ---
nipkow@9792
     5
@{text"ToyList"} is merely a small fragment of it chosen as an example. In
nipkow@8745
     6
contrast to what is recommended in \S\ref{sec:Basic:Theories},
nipkow@9792
     7
@{text"ToyList"} is not based on @{text"Main"} but on @{text"PreList"}, a
nipkow@8745
     8
theory that contains pretty much everything but lists, thus avoiding
nipkow@8745
     9
ambiguities caused by defining lists twice.
nipkow@8745
    10
*}
nipkow@8745
    11
nipkow@8745
    12
datatype 'a list = Nil                          ("[]")
nipkow@8745
    13
                 | Cons 'a "'a list"            (infixr "#" 65);
nipkow@8745
    14
nipkow@8745
    15
text{*\noindent
nipkow@8745
    16
The datatype\index{*datatype} \isaindexbold{list} introduces two
nipkow@8745
    17
constructors \isaindexbold{Nil} and \isaindexbold{Cons}, the
nipkow@9541
    18
empty~list and the operator that adds an element to the front of a list. For
nipkow@9792
    19
example, the term \isa{Cons True (Cons False Nil)} is a value of
nipkow@9792
    20
type @{typ"bool list"}, namely the list with the elements @{term"True"} and
nipkow@9792
    21
@{term"False"}. Because this notation becomes unwieldy very quickly, the
nipkow@8745
    22
datatype declaration is annotated with an alternative syntax: instead of
nipkow@9792
    23
@{term[source]Nil} and \isa{Cons x xs} we can write
nipkow@9792
    24
@{term"[]"}\index{$HOL2list@\texttt{[]}|bold} and
nipkow@9541
    25
@{term"x # xs"}\index{$HOL2list@\texttt{\#}|bold}. In fact, this
nipkow@8745
    26
alternative syntax is the standard syntax. Thus the list \isa{Cons True
nipkow@9541
    27
(Cons False Nil)} becomes @{term"True # False # []"}. The annotation
nipkow@9792
    28
\isacommand{infixr}\indexbold{*infixr} means that @{text"#"} associates to
nipkow@9792
    29
the right, i.e.\ the term @{term"x # y # z"} is read as @{text"x # (y # z)"}
nipkow@9792
    30
and not as @{text"(x # y) # z"}.
nipkow@8745
    31
nipkow@8745
    32
\begin{warn}
nipkow@8745
    33
  Syntax annotations are a powerful but completely optional feature. You
nipkow@9792
    34
  could drop them from theory @{text"ToyList"} and go back to the identifiers
nipkow@9792
    35
  @{term[source]Nil} and @{term[source]Cons}. However, lists are such a
nipkow@9792
    36
  central datatype
nipkow@8745
    37
  that their syntax is highly customized. We recommend that novices should
nipkow@8745
    38
  not use syntax annotations in their own theories.
nipkow@8745
    39
\end{warn}
nipkow@9792
    40
Next, two functions @{text"app"} and \isaindexbold{rev} are declared:
nipkow@8745
    41
*}
nipkow@8745
    42
nipkow@10236
    43
consts app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"   (infixr "@" 65)
nipkow@10236
    44
       rev :: "'a list \<Rightarrow> 'a list";
nipkow@8745
    45
nipkow@8745
    46
text{*
nipkow@8745
    47
\noindent
nipkow@8745
    48
In contrast to ML, Isabelle insists on explicit declarations of all functions
nipkow@8745
    49
(keyword \isacommand{consts}).  (Apart from the declaration-before-use
nipkow@8745
    50
restriction, the order of items in a theory file is unconstrained.) Function
nipkow@9792
    51
@{term"app"} is annotated with concrete syntax too. Instead of the prefix
nipkow@9541
    52
syntax \isa{app xs ys} the infix
nipkow@9541
    53
@{term"xs @ ys"}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred
nipkow@8745
    54
form. Both functions are defined recursively:
nipkow@8745
    55
*}
nipkow@8745
    56
nipkow@8745
    57
primrec
nipkow@8745
    58
"[] @ ys       = ys"
nipkow@8745
    59
"(x # xs) @ ys = x # (xs @ ys)";
nipkow@8745
    60
nipkow@8745
    61
primrec
nipkow@8745
    62
"rev []        = []"
nipkow@8745
    63
"rev (x # xs)  = (rev xs) @ (x # [])";
nipkow@8745
    64
nipkow@8745
    65
text{*
nipkow@8745
    66
\noindent
nipkow@9792
    67
The equations for @{term"app"} and @{term"rev"} hardly need comments:
nipkow@9792
    68
@{term"app"} appends two lists and @{term"rev"} reverses a list.  The keyword
nipkow@8745
    69
\isacommand{primrec}\index{*primrec} indicates that the recursion is of a
nipkow@8745
    70
particularly primitive kind where each recursive call peels off a datatype
nipkow@8771
    71
constructor from one of the arguments.  Thus the
nipkow@10654
    72
recursion always terminates, i.e.\ the function is \textbf{total}.
nipkow@10654
    73
\index{total function}
nipkow@8745
    74
nipkow@8745
    75
The termination requirement is absolutely essential in HOL, a logic of total
nipkow@8745
    76
functions. If we were to drop it, inconsistencies would quickly arise: the
nipkow@8745
    77
``definition'' $f(n) = f(n)+1$ immediately leads to $0 = 1$ by subtracting
nipkow@8745
    78
$f(n)$ on both sides.
nipkow@8745
    79
% However, this is a subtle issue that we cannot discuss here further.
nipkow@8745
    80
nipkow@8745
    81
\begin{warn}
nipkow@8745
    82
  As we have indicated, the desire for total functions is not a gratuitously
nipkow@8745
    83
  imposed restriction but an essential characteristic of HOL. It is only
nipkow@8745
    84
  because of totality that reasoning in HOL is comparatively easy.  More
nipkow@8745
    85
  generally, the philosophy in HOL is not to allow arbitrary axioms (such as
nipkow@8745
    86
  function definitions whose totality has not been proved) because they
nipkow@8745
    87
  quickly lead to inconsistencies. Instead, fixed constructs for introducing
nipkow@8745
    88
  types and functions are offered (such as \isacommand{datatype} and
nipkow@8745
    89
  \isacommand{primrec}) which are guaranteed to preserve consistency.
nipkow@8745
    90
\end{warn}
nipkow@8745
    91
nipkow@8745
    92
A remark about syntax.  The textual definition of a theory follows a fixed
nipkow@8745
    93
syntax with keywords like \isacommand{datatype} and \isacommand{end} (see
nipkow@8745
    94
Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list).
nipkow@8745
    95
Embedded in this syntax are the types and formulae of HOL, whose syntax is
nipkow@8745
    96
extensible, e.g.\ by new user-defined infix operators
nipkow@8745
    97
(see~\ref{sec:infix-syntax}). To distinguish the two levels, everything
nipkow@8745
    98
HOL-specific (terms and types) should be enclosed in
nipkow@8745
    99
\texttt{"}\dots\texttt{"}. 
nipkow@8745
   100
To lessen this burden, quotation marks around a single identifier can be
nipkow@8745
   101
dropped, unless the identifier happens to be a keyword, as in
nipkow@8745
   102
*}
nipkow@8745
   103
nipkow@10236
   104
consts "end" :: "'a list \<Rightarrow> 'a"
nipkow@8745
   105
nipkow@8745
   106
text{*\noindent
nipkow@8745
   107
When Isabelle prints a syntax error message, it refers to the HOL syntax as
nipkow@8771
   108
the \bfindex{inner syntax} and the enclosing theory language as the \bfindex{outer syntax}.
nipkow@8745
   109
nipkow@8745
   110
nipkow@8745
   111
\section{An introductory proof}
nipkow@8745
   112
\label{sec:intro-proof}
nipkow@8745
   113
nipkow@8745
   114
Assuming you have input the declarations and definitions of \texttt{ToyList}
nipkow@8745
   115
presented so far, we are ready to prove a few simple theorems. This will
nipkow@8745
   116
illustrate not just the basic proof commands but also the typical proof
nipkow@8745
   117
process.
nipkow@8745
   118
nipkow@9792
   119
\subsubsection*{Main goal: @{text"rev(rev xs) = xs"}}
nipkow@8745
   120
nipkow@8745
   121
Our goal is to show that reversing a list twice produces the original
nipkow@8745
   122
list. The input line
nipkow@8745
   123
*}
nipkow@8745
   124
nipkow@8745
   125
theorem rev_rev [simp]: "rev(rev xs) = xs";
nipkow@8745
   126
nipkow@8771
   127
txt{*\index{*theorem|bold}\index{*simp (attribute)|bold}
nipkow@8745
   128
\begin{itemize}
nipkow@8745
   129
\item
nipkow@9792
   130
establishes a new theorem to be proved, namely @{prop"rev(rev xs) = xs"},
nipkow@8745
   131
\item
nipkow@9792
   132
gives that theorem the name @{text"rev_rev"} by which it can be
nipkow@9792
   133
referred to,
nipkow@8745
   134
\item
nipkow@9792
   135
and tells Isabelle (via @{text"[simp]"}) to use the theorem (once it has been
nipkow@8745
   136
proved) as a simplification rule, i.e.\ all future proofs involving
nipkow@9792
   137
simplification will replace occurrences of @{term"rev(rev xs)"} by
nipkow@9792
   138
@{term"xs"}.
nipkow@8745
   139
nipkow@8745
   140
The name and the simplification attribute are optional.
nipkow@8745
   141
\end{itemize}
nipkow@8745
   142
Isabelle's response is to print
nipkow@9723
   143
\begin{isabelle}
nipkow@8745
   144
proof(prove):~step~0\isanewline
nipkow@8745
   145
\isanewline
nipkow@8745
   146
goal~(theorem~rev\_rev):\isanewline
nipkow@8745
   147
rev~(rev~xs)~=~xs\isanewline
nipkow@8745
   148
~1.~rev~(rev~xs)~=~xs
nipkow@9723
   149
\end{isabelle}
nipkow@8745
   150
The first three lines tell us that we are 0 steps into the proof of
nipkow@9792
   151
theorem @{text"rev_rev"}; for compactness reasons we rarely show these
nipkow@8745
   152
initial lines in this tutorial. The remaining lines display the current
nipkow@8745
   153
proof state.
nipkow@8745
   154
Until we have finished a proof, the proof state always looks like this:
nipkow@9723
   155
\begin{isabelle}
nipkow@8745
   156
$G$\isanewline
nipkow@8745
   157
~1.~$G\sb{1}$\isanewline
nipkow@8745
   158
~~\vdots~~\isanewline
nipkow@8745
   159
~$n$.~$G\sb{n}$
nipkow@9723
   160
\end{isabelle}
nipkow@8745
   161
where $G$
nipkow@8745
   162
is the overall goal that we are trying to prove, and the numbered lines
nipkow@8745
   163
contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$ that we need to prove to
nipkow@9792
   164
establish $G$. At @{text"step 0"} there is only one subgoal, which is
nipkow@8745
   165
identical with the overall goal.  Normally $G$ is constant and only serves as
nipkow@8745
   166
a reminder. Hence we rarely show it in this tutorial.
nipkow@8745
   167
nipkow@9792
   168
Let us now get back to @{prop"rev(rev xs) = xs"}. Properties of recursively
nipkow@8745
   169
defined functions are best established by induction. In this case there is
nipkow@9792
   170
not much choice except to induct on @{term"xs"}:
nipkow@8745
   171
*}
nipkow@8745
   172
nipkow@8745
   173
apply(induct_tac xs);
nipkow@8745
   174
nipkow@8745
   175
txt{*\noindent\index{*induct_tac}%
nipkow@9792
   176
This tells Isabelle to perform induction on variable @{term"xs"}. The suffix
nipkow@9792
   177
@{term"tac"} stands for ``tactic'', a synonym for ``theorem proving function''.
nipkow@8745
   178
By default, induction acts on the first subgoal. The new proof state contains
nipkow@9792
   179
two subgoals, namely the base case (@{term[source]Nil}) and the induction step
nipkow@9792
   180
(@{term[source]Cons}):
nipkow@9723
   181
\begin{isabelle}
nipkow@8745
   182
~1.~rev~(rev~[])~=~[]\isanewline
nipkow@9792
   183
~2.~{\isasymAnd}a~list.~rev(rev~list)~=~list~{\isasymLongrightarrow}~rev(rev(a~\#~list))~=~a~\#~list
nipkow@9723
   184
\end{isabelle}
nipkow@8745
   185
nipkow@8745
   186
The induction step is an example of the general format of a subgoal:
nipkow@9723
   187
\begin{isabelle}
nipkow@10328
   188
~$i$.~{\isasymAnd}$x\sb{1}$~\dots~$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion}
nipkow@10328
   189
\end{isabelle}\index{$IsaAnd@\isasymAnd|bold}
nipkow@8745
   190
The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be
nipkow@8745
   191
ignored most of the time, or simply treated as a list of variables local to
paulson@10302
   192
this subgoal. Their deeper significance is explained in Chapter~\ref{chap:rules}.
nipkow@8745
   193
The {\it assumptions} are the local assumptions for this subgoal and {\it
nipkow@8745
   194
  conclusion} is the actual proposition to be proved. Typical proof steps
nipkow@8745
   195
that add new assumptions are induction or case distinction. In our example
nipkow@9541
   196
the only assumption is the induction hypothesis @{term"rev (rev list) =
nipkow@9792
   197
  list"}, where @{term"list"} is a variable name chosen by Isabelle. If there
nipkow@8745
   198
are multiple assumptions, they are enclosed in the bracket pair
nipkow@8745
   199
\indexboldpos{\isasymlbrakk}{$Isabrl} and
nipkow@8745
   200
\indexboldpos{\isasymrbrakk}{$Isabrr} and separated by semicolons.
nipkow@8745
   201
nipkow@8745
   202
Let us try to solve both goals automatically:
nipkow@8745
   203
*}
nipkow@8745
   204
nipkow@8745
   205
apply(auto);
nipkow@8745
   206
nipkow@8745
   207
txt{*\noindent
nipkow@8745
   208
This command tells Isabelle to apply a proof strategy called
nipkow@9792
   209
@{text"auto"} to all subgoals. Essentially, @{text"auto"} tries to
nipkow@8745
   210
``simplify'' the subgoals.  In our case, subgoal~1 is solved completely (thanks
nipkow@9792
   211
to the equation @{prop"rev [] = []"}) and disappears; the simplified version
nipkow@8745
   212
of subgoal~2 becomes the new subgoal~1:
nipkow@9723
   213
\begin{isabelle}
nipkow@8745
   214
~1.~\dots~rev(rev~list)~=~list~{\isasymLongrightarrow}~rev(rev~list~@~a~\#~[])~=~a~\#~list
nipkow@9723
   215
\end{isabelle}
nipkow@8745
   216
In order to simplify this subgoal further, a lemma suggests itself.
nipkow@8745
   217
*}
nipkow@8745
   218
(*<*)
nipkow@8745
   219
oops
nipkow@8745
   220
(*>*)
nipkow@8745
   221
nipkow@9792
   222
subsubsection{*First lemma: @{text"rev(xs @ ys) = (rev ys) @ (rev xs)"}*}
nipkow@9723
   223
nipkow@8745
   224
text{*
nipkow@9494
   225
After abandoning the above proof attempt\indexbold{abandon
nipkow@9494
   226
proof}\indexbold{proof!abandon} (at the shell level type
nipkow@9494
   227
\isacommand{oops}\indexbold{*oops}) we start a new proof:
nipkow@8745
   228
*}
nipkow@8745
   229
nipkow@8745
   230
lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
nipkow@8745
   231
nipkow@8745
   232
txt{*\noindent The keywords \isacommand{theorem}\index{*theorem} and
nipkow@8745
   233
\isacommand{lemma}\indexbold{*lemma} are interchangable and merely indicate
nipkow@8745
   234
the importance we attach to a proposition. In general, we use the words
nipkow@8745
   235
\emph{theorem}\index{theorem} and \emph{lemma}\index{lemma} pretty much
nipkow@8745
   236
interchangeably.
nipkow@8745
   237
nipkow@9792
   238
There are two variables that we could induct on: @{term"xs"} and
nipkow@9792
   239
@{term"ys"}. Because @{text"@"} is defined by recursion on
nipkow@9792
   240
the first argument, @{term"xs"} is the correct one:
nipkow@8745
   241
*}
nipkow@8745
   242
nipkow@8745
   243
apply(induct_tac xs);
nipkow@8745
   244
nipkow@8745
   245
txt{*\noindent
nipkow@8745
   246
This time not even the base case is solved automatically:
nipkow@8745
   247
*}
nipkow@8745
   248
nipkow@8745
   249
apply(auto);
nipkow@8745
   250
nipkow@8745
   251
txt{*
nipkow@10362
   252
@{subgoals[display,indent=0,goals_limit=1]}
nipkow@10362
   253
Again, we need to abandon this proof attempt and prove another simple lemma
nipkow@10362
   254
first. In the future the step of abandoning an incomplete proof before
nipkow@10362
   255
embarking on the proof of a lemma usually remains implicit.
nipkow@8745
   256
*}
nipkow@8745
   257
(*<*)
nipkow@8745
   258
oops
nipkow@8745
   259
(*>*)
nipkow@8745
   260
nipkow@9792
   261
subsubsection{*Second lemma: @{text"xs @ [] = xs"}*}
nipkow@9723
   262
nipkow@8745
   263
text{*
nipkow@8745
   264
This time the canonical proof procedure
nipkow@8745
   265
*}
nipkow@8745
   266
nipkow@8745
   267
lemma app_Nil2 [simp]: "xs @ [] = xs";
nipkow@8745
   268
apply(induct_tac xs);
nipkow@8745
   269
apply(auto);
nipkow@8745
   270
nipkow@8745
   271
txt{*
nipkow@8745
   272
\noindent
nipkow@9792
   273
leads to the desired message @{text"No subgoals!"}:
nipkow@10362
   274
@{goals[display,indent=0]}
nipkow@8745
   275
We still need to confirm that the proof is now finished:
nipkow@8745
   276
*}
nipkow@8745
   277
nipkow@10171
   278
done
nipkow@8745
   279
nipkow@10171
   280
text{*\noindent\indexbold{done}%
nipkow@10171
   281
As a result of that final \isacommand{done}, Isabelle associates the lemma just proved
nipkow@10171
   282
with its name. In this tutorial, we sometimes omit to show that final \isacommand{done}
nipkow@10171
   283
if it is obvious from the context that the proof is finished.
nipkow@10171
   284
nipkow@10171
   285
% Instead of \isacommand{apply} followed by a dot, you can simply write
nipkow@10171
   286
% \isacommand{by}\indexbold{by}, which we do most of the time.
nipkow@10171
   287
Notice that in lemma @{thm[source]app_Nil2}
nipkow@10171
   288
(as printed out after the final \isacommand{done}) the free variable @{term"xs"} has been
nipkow@9792
   289
replaced by the unknown @{text"?xs"}, just as explained in
nipkow@9792
   290
\S\ref{sec:variables}.
nipkow@8745
   291
nipkow@8745
   292
Going back to the proof of the first lemma
nipkow@8745
   293
*}
nipkow@8745
   294
nipkow@8745
   295
lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
nipkow@8745
   296
apply(induct_tac xs);
nipkow@8745
   297
apply(auto);
nipkow@8745
   298
nipkow@8745
   299
txt{*
nipkow@8745
   300
\noindent
nipkow@9792
   301
we find that this time @{text"auto"} solves the base case, but the
nipkow@8745
   302
induction step merely simplifies to
nipkow@10362
   303
@{subgoals[display,indent=0,goals_limit=1]}
nipkow@9792
   304
Now we need to remember that @{text"@"} associates to the right, and that
nipkow@9792
   305
@{text"#"} and @{text"@"} have the same priority (namely the @{text"65"}
nipkow@8745
   306
in their \isacommand{infixr} annotation). Thus the conclusion really is
nipkow@9723
   307
\begin{isabelle}
nipkow@9792
   308
~~~~~(rev~ys~@~rev~list)~@~(a~\#~[])~=~rev~ys~@~(rev~list~@~(a~\#~[]))
nipkow@9723
   309
\end{isabelle}
nipkow@9792
   310
and the missing lemma is associativity of @{text"@"}.
nipkow@9723
   311
*}
nipkow@9723
   312
(*<*)oops(*>*)
nipkow@8745
   313
nipkow@9792
   314
subsubsection{*Third lemma: @{text"(xs @ ys) @ zs = xs @ (ys @ zs)"}*}
nipkow@8745
   315
nipkow@9723
   316
text{*
nipkow@8745
   317
Abandoning the previous proof, the canonical proof procedure
nipkow@8745
   318
*}
nipkow@8745
   319
nipkow@8745
   320
lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)";
nipkow@8745
   321
apply(induct_tac xs);
nipkow@10171
   322
apply(auto);
nipkow@10171
   323
done
nipkow@8745
   324
nipkow@8745
   325
text{*
nipkow@8745
   326
\noindent
nipkow@8745
   327
succeeds without further ado.
nipkow@8745
   328
Now we can go back and prove the first lemma
nipkow@8745
   329
*}
nipkow@8745
   330
nipkow@8745
   331
lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
nipkow@8745
   332
apply(induct_tac xs);
nipkow@10171
   333
apply(auto);
nipkow@10171
   334
done
nipkow@8745
   335
nipkow@8745
   336
text{*\noindent
nipkow@8745
   337
and then solve our main theorem:
nipkow@8745
   338
*}
nipkow@8745
   339
nipkow@8745
   340
theorem rev_rev [simp]: "rev(rev xs) = xs";
nipkow@8745
   341
apply(induct_tac xs);
nipkow@10171
   342
apply(auto);
nipkow@10171
   343
done
nipkow@8745
   344
nipkow@8745
   345
text{*\noindent
nipkow@9792
   346
The final \isacommand{end} tells Isabelle to close the current theory because
nipkow@8745
   347
we are finished with its development:
nipkow@8745
   348
*}
nipkow@8745
   349
nipkow@8745
   350
end