doc-src/TutorialI/Inductive/Even.tex
 author nipkow Wed Dec 06 13:22:58 2000 +0100 (2000-12-06) changeset 10608 620647438780 parent 10520 bb9dfcc87951 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.