doc-src/TutorialI/Inductive/Even.tex
author nipkow
Sun Nov 26 10:48:38 2000 +0100 (2000-11-26)
changeset 10520 bb9dfcc87951
parent 10419 1bfdd19c1d47
child 10654 458068404143
permissions -rw-r--r--
*** empty log message ***
paulson@10325
     1
\section{The set of even numbers}
paulson@10325
     2
paulson@10325
     3
The set of even numbers can be inductively defined as the least set
paulson@10325
     4
containing 0 and closed under the operation ${\cdots}+2$.  Obviously,
paulson@10325
     5
\emph{even} can also be expressed using the divides relation (\isa{dvd}). 
paulson@10325
     6
We shall prove below that the two formulations coincide.  On the way we
paulson@10325
     7
shall examine the primary means of reasoning about inductively defined
paulson@10325
     8
sets: rule induction.
paulson@10325
     9
paulson@10325
    10
\subsection{Making an inductive definition}
paulson@10325
    11
paulson@10325
    12
Using \isacommand{consts}, we declare the constant \isa{even} to be a set
paulson@10325
    13
of natural numbers. The \isacommand{inductive} declaration gives it the
paulson@10325
    14
desired properties.
paulson@10325
    15
\begin{isabelle}
paulson@10325
    16
\isacommand{consts}\ even\ ::\ "nat\ set"\isanewline
paulson@10325
    17
\isacommand{inductive}\ even\isanewline
paulson@10325
    18
\isakeyword{intros}\isanewline
paulson@10325
    19
zero[intro!]:\ "0\ \isasymin \ even"\isanewline
paulson@10325
    20
step[intro!]:\ "n\ \isasymin \ even\ \isasymLongrightarrow \ (Suc\ (Suc\
paulson@10325
    21
n))\ \isasymin \ even"
paulson@10325
    22
\end{isabelle}
paulson@10325
    23
paulson@10325
    24
An inductive definition consists of introduction rules.  The first one
paulson@10325
    25
above states that 0 is even; the second states that if $n$ is even, then so
paulson@10325
    26
is
paulson@10325
    27
$n+2$.  Given this declaration, Isabelle generates a fixed point definition
paulson@10325
    28
for \isa{even} and proves theorems about it.  These theorems include the
paulson@10325
    29
introduction rules specified in the declaration, an elimination rule for case
paulson@10325
    30
analysis and an induction rule.  We can refer to these theorems by
paulson@10325
    31
automatically-generated names.  Here are two examples:
paulson@10325
    32
%
paulson@10325
    33
\begin{isabelle}
paulson@10419
    34
0\ \isasymin \ even
paulson@10419
    35
\rulename{even.zero}
paulson@10419
    36
\par\smallskip
paulson@10325
    37
n\ \isasymin \ even\ \isasymLongrightarrow \ Suc\ (Suc\ n)\ \isasymin \
paulson@10325
    38
even%
paulson@10325
    39
\rulename{even.step}
paulson@10325
    40
\end{isabelle}
paulson@10325
    41
paulson@10325
    42
The introduction rules can be given attributes.  Here both rules are
paulson@10325
    43
specified as \isa{intro!}, directing the classical reasoner to 
paulson@10325
    44
apply them aggressively. Obviously, regarding 0 as even is safe.  The
paulson@10325
    45
\isa{step} rule is also safe because $n+2$ is even if and only if $n$ is
paulson@10325
    46
even.  We prove this equivalence later.
paulson@10325
    47
paulson@10325
    48
\subsection{Using introduction rules}
paulson@10325
    49
paulson@10325
    50
Our first lemma states that numbers of the form $2\times k$ are even.
paulson@10325
    51
Introduction rules are used to show that specific values belong to the
paulson@10325
    52
inductive set.  Such proofs typically involve 
paulson@10325
    53
induction, perhaps over some other inductive set.
paulson@10325
    54
\begin{isabelle}
paulson@10325
    55
\isacommand{lemma}\ two_times_even[intro!]:\ "\#2*k\ \isasymin \ even"
paulson@10325
    56
\isanewline
paulson@10325
    57
\isacommand{apply}\ (induct\ "k")\isanewline
paulson@10325
    58
\ \isacommand{apply}\ auto\isanewline
paulson@10325
    59
\isacommand{done}
paulson@10325
    60
\end{isabelle}
paulson@10325
    61
%
paulson@10325
    62
The first step is induction on the natural number \isa{k}, which leaves
paulson@10325
    63
two subgoals:
paulson@10325
    64
\begin{isabelle}
paulson@10325
    65
\ 1.\ \#2\ *\ 0\ \isasymin \ even\isanewline
paulson@10325
    66
\ 2.\ \isasymAnd n.\ \#2\ *\ n\ \isasymin \ even\ \isasymLongrightarrow \ \#2\ *\ Suc\ n\ \isasymin \ even
paulson@10325
    67
\end{isabelle}
paulson@10325
    68
%
paulson@10325
    69
Here \isa{auto} simplifies both subgoals so that they match the introduction
paulson@10325
    70
rules, which are then applied automatically.
paulson@10325
    71
paulson@10325
    72
Our ultimate goal is to prove the equivalence between the traditional
paulson@10325
    73
definition of \isa{even} (using the divides relation) and our inductive
paulson@10325
    74
definition.  One direction of this equivalence is immediate by the lemma
paulson@10325
    75
just proved, whose \isa{intro!} attribute ensures it will be used.
paulson@10325
    76
\begin{isabelle}
paulson@10325
    77
\isacommand{lemma}\ dvd_imp_even:\ "\#2\ dvd\ n\ \isasymLongrightarrow \ n\ \isasymin \ even"\isanewline
paulson@10325
    78
\isacommand{apply}\ (auto\ simp\ add:\ dvd_def)\isanewline
paulson@10325
    79
\isacommand{done}
paulson@10325
    80
\end{isabelle}
paulson@10325
    81
paulson@10325
    82
\subsection{Rule induction}
paulson@10325
    83
paulson@10419
    84
From the definition of the set
paulson@10419
    85
\isa{even}, Isabelle has
paulson@10419
    86
generated an induction rule:
paulson@10419
    87
\begin{isabelle}
paulson@10419
    88
\isasymlbrakk xa\ \isasymin \ even;\isanewline
paulson@10419
    89
\ P\ 0;\isanewline
paulson@10419
    90
\ \isasymAnd n.\ \isasymlbrakk n\ \isasymin \ even;\ P\ n\isasymrbrakk \
paulson@10419
    91
\isasymLongrightarrow \ P\ (Suc\ (Suc\ n))\isasymrbrakk\isanewline
paulson@10419
    92
\ \isasymLongrightarrow \ P\ xa%
paulson@10419
    93
\rulename{even.induct}
paulson@10419
    94
\end{isabelle}
paulson@10419
    95
A property \isa{P} holds for every even number provided it
paulson@10419
    96
holds for~\isa{0} and is closed under the operation
paulson@10419
    97
\isa{Suc(Suc\(\cdots\))}.  Then \isa{P} is closed under the introduction
paulson@10419
    98
rules for \isa{even}, which is the least set closed under those rules. 
paulson@10419
    99
This type of inductive argument is called \textbf{rule induction}. 
paulson@10419
   100
paulson@10419
   101
Apart from the double application of \isa{Suc}, the induction rule above
paulson@10419
   102
resembles the familiar mathematical induction, which indeed is an instance
paulson@10419
   103
of rule induction; the natural numbers can be defined inductively to be
paulson@10419
   104
the least set containing \isa{0} and closed under~\isa{Suc}.
paulson@10419
   105
paulson@10419
   106
Induction is the usual way of proving a property of the elements of an
paulson@10419
   107
inductively defined set.  Let us prove that all members of the set
paulson@10419
   108
\isa{even} are multiples of two.  
paulson@10325
   109
\begin{isabelle}
paulson@10325
   110
\isacommand{lemma}\ even_imp_dvd:\ "n\ \isasymin \ even\ \isasymLongrightarrow \ \#2\ dvd\ n"\isanewline
paulson@10325
   111
\isacommand{apply}\ (erule\ even.induct)\isanewline
paulson@10325
   112
\ \isacommand{apply}\ simp\isanewline
paulson@10325
   113
\isacommand{apply}\ (simp\ add:\ dvd_def)\isanewline
paulson@10325
   114
\isacommand{apply}\ clarify\isanewline
paulson@10325
   115
\isacommand{apply}\ (rule_tac\ x\ =\ "Suc\ k"\ \isakeyword{in}\ exI)\isanewline
paulson@10325
   116
\isacommand{apply}\ simp\isanewline
paulson@10325
   117
\isacommand{done}
paulson@10325
   118
\end{isabelle}
paulson@10325
   119
%
paulson@10325
   120
We begin by applying induction.  Note that \isa{even.induct} has the form
paulson@10325
   121
of an elimination rule, so we use the method \isa{erule}.  We get two
paulson@10325
   122
subgoals:
paulson@10325
   123
\begin{isabelle}
paulson@10325
   124
\ 1.\ \#2\ dvd\ 0\isanewline
paulson@10325
   125
\ 2.\ \isasymAnd n.\ \isasymlbrakk n\ \isasymin \ even;\ \#2\ dvd\ n\isasymrbrakk \ \isasymLongrightarrow \ \#2\ dvd\ Suc\ (Suc\ n)
paulson@10325
   126
\end{isabelle}
paulson@10325
   127
%
paulson@10325
   128
The first subgoal is trivial (by \isa{simp}).  For the second
paulson@10325
   129
subgoal, we unfold the definition of \isa{dvd}:
paulson@10325
   130
\begin{isabelle}
paulson@10325
   131
\ 1.\ \isasymAnd n.\ \isasymlbrakk n\ \isasymin \ even;\ \isasymexists k.\
paulson@10325
   132
n\ =\ \#2\ *\ k\isasymrbrakk \ \isasymLongrightarrow \ \isasymexists k.\
paulson@10325
   133
Suc\ (Suc\ n)\ =\ \#2\ *\ k
paulson@10325
   134
\end{isabelle}
paulson@10325
   135
%
paulson@10325
   136
Then we use
paulson@10325
   137
\isa{clarify} to eliminate the existential quantifier from the assumption
paulson@10325
   138
and replace \isa{n} by \isa{\#2\ *\ k}.
paulson@10325
   139
\begin{isabelle}
paulson@10325
   140
\ 1.\ \isasymAnd n\ k.\ \#2\ *\ k\ \isasymin \ even\ \isasymLongrightarrow \ \isasymexists ka.\ Suc\ (Suc\ (\#2\ *\ k))\ =\ \#2\ *\ ka%
paulson@10325
   141
\end{isabelle}
paulson@10325
   142
%
paulson@10325
   143
The \isa{rule_tac\ldots exI} tells Isabelle that the desired
paulson@10325
   144
\isa{ka} is
paulson@10325
   145
\isa{Suc\ k}.  With this hint, the subgoal becomes trivial, and \isa{simp}
paulson@10325
   146
concludes the proof.
paulson@10325
   147
paulson@10325
   148
\medskip
paulson@10325
   149
Combining the previous two results yields our objective, the
paulson@10325
   150
equivalence relating \isa{even} and \isa{dvd}. 
paulson@10325
   151
%
paulson@10325
   152
%we don't want [iff]: discuss?
paulson@10325
   153
\begin{isabelle}
paulson@10325
   154
\isacommand{theorem}\ even_iff_dvd:\ "(n\ \isasymin \ even)\ =\ (\#2\ dvd\ n)"\isanewline
paulson@10325
   155
\isacommand{apply}\ (blast\ intro:\ dvd_imp_even\ even_imp_dvd)\isanewline
paulson@10325
   156
\isacommand{done}
paulson@10325
   157
\end{isabelle}
paulson@10325
   158
paulson@10325
   159
\subsection{Generalization and rule induction}
nipkow@10520
   160
\label{sec:gen-rule-induction}
paulson@10325
   161
paulson@10325
   162
Everybody knows that when before applying induction we often must generalize
paulson@10325
   163
the induction formula.  This step is just as important with rule induction,
paulson@10325
   164
and the required generalizations can be complicated.  In this 
paulson@10325
   165
example, the obvious statement of the result is not inductive:
paulson@10325
   166
%
paulson@10325
   167
\begin{isabelle}
paulson@10325
   168
\isacommand{lemma}\ "Suc\ (Suc\ n)\ \isasymin \ even\
paulson@10325
   169
\isasymLongrightarrow \ n\ \isasymin \ even"\isanewline
paulson@10325
   170
\isacommand{apply}\ (erule\ even.induct)\isanewline
paulson@10325
   171
\isacommand{oops}
paulson@10325
   172
\end{isabelle}
paulson@10325
   173
%
paulson@10325
   174
Rule induction finds no occurrences of \isa{Suc\ (Suc\ n)} in the
paulson@10325
   175
conclusion, which it therefore leaves unchanged.  (Look at
paulson@10325
   176
\isa{even.induct} to see why this happens.)  We get these subgoals:
paulson@10325
   177
\begin{isabelle}
paulson@10325
   178
\ 1.\ n\ \isasymin \ even\isanewline
paulson@10325
   179
\ 2.\ \isasymAnd na.\ \isasymlbrakk na\ \isasymin \ even;\ n\ \isasymin \ even\isasymrbrakk \ \isasymLongrightarrow \ n\ \isasymin \ even%
paulson@10325
   180
\end{isabelle}
paulson@10325
   181
The first one is hopeless.  In general, rule inductions involving
paulson@10325
   182
non-trivial terms will probably go wrong.  The solution is easy provided
paulson@10325
   183
we have the necessary inverses, here subtraction:
paulson@10325
   184
\begin{isabelle}
paulson@10325
   185
\isacommand{lemma}\ even_imp_even_minus_2:\ "n\ \isasymin \ even\ \isasymLongrightarrow \ n-\#2\ \isasymin \ even"\isanewline
paulson@10325
   186
\isacommand{apply}\ (erule\ even.induct)\isanewline
paulson@10325
   187
\ \isacommand{apply}\ auto\isanewline
paulson@10325
   188
\isacommand{done}
paulson@10325
   189
\end{isabelle}
paulson@10325
   190
%
paulson@10325
   191
This lemma is trivially inductive.  Here are the subgoals:
paulson@10325
   192
\begin{isabelle}
paulson@10325
   193
\ 1.\ 0\ -\ \#2\ \isasymin \ even\isanewline
paulson@10325
   194
\ 2.\ \isasymAnd n.\ \isasymlbrakk n\ \isasymin \ even;\ n\ -\ \#2\ \isasymin \ even\isasymrbrakk \ \isasymLongrightarrow \ Suc\ (Suc\ n)\ -\ \#2\ \isasymin \ even%
paulson@10325
   195
\end{isabelle}
paulson@10325
   196
The first is trivial because \isa{0\ -\ \#2} simplifies to \isa{0}, which is
paulson@10325
   197
even.  The second is trivial too: \isa{Suc\ (Suc\ n)\ -\ \#2} simplifies to
paulson@10325
   198
\isa{n}, matching the assumption.
paulson@10325
   199
paulson@10325
   200
\medskip
paulson@10325
   201
Using our lemma, we can easily prove the result we originally wanted:
paulson@10325
   202
\begin{isabelle}
paulson@10325
   203
\isacommand{lemma}\ Suc_Suc_even_imp_even:\ "Suc\ (Suc\ n)\ \isasymin \ even\ \isasymLongrightarrow \ n\ \isasymin \ even"\isanewline
paulson@10325
   204
\isacommand{apply}\ (drule\ even_imp_even_minus_2)\isanewline
paulson@10325
   205
\isacommand{apply}\ simp\isanewline
paulson@10325
   206
\isacommand{done}
paulson@10325
   207
\end{isabelle}
paulson@10325
   208
paulson@10325
   209
We have just proved the converse of the introduction rule \isa{even.step}. 
paulson@10325
   210
This suggests proving the following equivalence.  We give it the \isa{iff}
paulson@10325
   211
attribute because of its obvious value for simplification.
paulson@10325
   212
\begin{isabelle}
paulson@10325
   213
\isacommand{lemma}\ [iff]:\ "((Suc\ (Suc\ n))\ \isasymin \ even)\ =\ (n\
paulson@10325
   214
\isasymin \ even)"\isanewline
paulson@10325
   215
\isacommand{apply}\ (blast\ dest:\ Suc_Suc_even_imp_even)\isanewline
paulson@10419
   216
\isacommand{done}
paulson@10325
   217
\end{isabelle}
paulson@10419
   218
paulson@10419
   219
The even numbers example has shown how inductive definitions can be used. 
paulson@10419
   220
Later examples will show that they are actually worth using.