summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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}

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.

10 \subsection{Making an inductive definition}

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}

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}

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.

48 \subsection{Using introduction rules}

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.

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}

82 \subsection{Rule induction}

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

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

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.

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}

159 \subsection{Generalization and rule induction}

160 \label{sec:gen-rule-induction}

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.

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}

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}

221 The even numbers example has shown how inductive definitions can be used.

222 Later examples will show that they are actually worth using.