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 ***
     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.