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