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