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

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}

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

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}

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}

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

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