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 ***
     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.  The solution is easy provided
   183 we have the necessary inverses, here subtraction:
   184 \begin{isabelle}
   185 \isacommand{lemma}\ even_imp_even_minus_2:\ "n\ \isasymin \ even\ \isasymLongrightarrow \ n-\#2\ \isasymin \ even"\isanewline
   186 \isacommand{apply}\ (erule\ even.induct)\isanewline
   187 \ \isacommand{apply}\ auto\isanewline
   188 \isacommand{done}
   189 \end{isabelle}
   190 %
   191 This lemma is trivially inductive.  Here are the subgoals:
   192 \begin{isabelle}
   193 \ 1.\ 0\ -\ \#2\ \isasymin \ even\isanewline
   194 \ 2.\ \isasymAnd n.\ \isasymlbrakk n\ \isasymin \ even;\ n\ -\ \#2\ \isasymin \ even\isasymrbrakk \ \isasymLongrightarrow \ Suc\ (Suc\ n)\ -\ \#2\ \isasymin \ even%
   195 \end{isabelle}
   196 The first is trivial because \isa{0\ -\ \#2} simplifies to \isa{0}, which is
   197 even.  The second is trivial too: \isa{Suc\ (Suc\ n)\ -\ \#2} simplifies to
   198 \isa{n}, matching the assumption.
   199 
   200 \medskip
   201 Using our lemma, we can easily prove the result we originally wanted:
   202 \begin{isabelle}
   203 \isacommand{lemma}\ Suc_Suc_even_imp_even:\ "Suc\ (Suc\ n)\ \isasymin \ even\ \isasymLongrightarrow \ n\ \isasymin \ even"\isanewline
   204 \isacommand{apply}\ (drule\ even_imp_even_minus_2)\isanewline
   205 \isacommand{apply}\ simp\isanewline
   206 \isacommand{done}
   207 \end{isabelle}
   208 
   209 We have just proved the converse of the introduction rule \isa{even.step}. 
   210 This suggests proving the following equivalence.  We give it the \isa{iff}
   211 attribute because of its obvious value for simplification.
   212 \begin{isabelle}
   213 \isacommand{lemma}\ [iff]:\ "((Suc\ (Suc\ n))\ \isasymin \ even)\ =\ (n\
   214 \isasymin \ even)"\isanewline
   215 \isacommand{apply}\ (blast\ dest:\ Suc_Suc_even_imp_even)\isanewline
   216 \isacommand{done}
   217 \end{isabelle}
   218 
   219 The even numbers example has shown how inductive definitions can be used. 
   220 Later examples will show that they are actually worth using.