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