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