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.