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 \label{sec:rule-induction} |
|
84 |
|
85 From the definition of the set |
|
86 \isa{even}, Isabelle has |
|
87 generated an induction rule: |
|
88 \begin{isabelle} |
|
89 \isasymlbrakk xa\ \isasymin \ even;\isanewline |
|
90 \ P\ 0;\isanewline |
|
91 \ \isasymAnd n.\ \isasymlbrakk n\ \isasymin \ even;\ P\ n\isasymrbrakk \ |
|
92 \isasymLongrightarrow \ P\ (Suc\ (Suc\ n))\isasymrbrakk\isanewline |
|
93 \ \isasymLongrightarrow \ P\ xa% |
|
94 \rulename{even.induct} |
|
95 \end{isabelle} |
|
96 A property \isa{P} holds for every even number provided it |
|
97 holds for~\isa{0} and is closed under the operation |
|
98 \isa{Suc(Suc\(\cdots\))}. Then \isa{P} is closed under the introduction |
|
99 rules for \isa{even}, which is the least set closed under those rules. |
|
100 This type of inductive argument is called \textbf{rule induction}. |
|
101 |
|
102 Apart from the double application of \isa{Suc}, the induction rule above |
|
103 resembles the familiar mathematical induction, which indeed is an instance |
|
104 of rule induction; the natural numbers can be defined inductively to be |
|
105 the least set containing \isa{0} and closed under~\isa{Suc}. |
|
106 |
|
107 Induction is the usual way of proving a property of the elements of an |
|
108 inductively defined set. Let us prove that all members of the set |
|
109 \isa{even} are multiples of two. |
|
110 \begin{isabelle} |
|
111 \isacommand{lemma}\ even_imp_dvd:\ "n\ \isasymin \ even\ \isasymLongrightarrow \ \#2\ dvd\ n"\isanewline |
|
112 \isacommand{apply}\ (erule\ even.induct)\isanewline |
|
113 \ \isacommand{apply}\ simp\isanewline |
|
114 \isacommand{apply}\ (simp\ add:\ dvd_def)\isanewline |
|
115 \isacommand{apply}\ clarify\isanewline |
|
116 \isacommand{apply}\ (rule_tac\ x\ =\ "Suc\ k"\ \isakeyword{in}\ exI)\isanewline |
|
117 \isacommand{apply}\ simp\isanewline |
|
118 \isacommand{done} |
|
119 \end{isabelle} |
|
120 % |
|
121 We begin by applying induction. Note that \isa{even.induct} has the form |
|
122 of an elimination rule, so we use the method \isa{erule}. We get two |
|
123 subgoals: |
|
124 \begin{isabelle} |
|
125 \ 1.\ \#2\ dvd\ 0\isanewline |
|
126 \ 2.\ \isasymAnd n.\ \isasymlbrakk n\ \isasymin \ even;\ \#2\ dvd\ n\isasymrbrakk \ \isasymLongrightarrow \ \#2\ dvd\ Suc\ (Suc\ n) |
|
127 \end{isabelle} |
|
128 % |
|
129 The first subgoal is trivial (by \isa{simp}). For the second |
|
130 subgoal, we unfold the definition of \isa{dvd}: |
|
131 \begin{isabelle} |
|
132 \ 1.\ \isasymAnd n.\ \isasymlbrakk n\ \isasymin \ even;\ \isasymexists k.\ |
|
133 n\ =\ \#2\ *\ k\isasymrbrakk \ \isasymLongrightarrow \ \isasymexists k.\ |
|
134 Suc\ (Suc\ n)\ =\ \#2\ *\ k |
|
135 \end{isabelle} |
|
136 % |
|
137 Then we use |
|
138 \isa{clarify} to eliminate the existential quantifier from the assumption |
|
139 and replace \isa{n} by \isa{\#2\ *\ k}. |
|
140 \begin{isabelle} |
|
141 \ 1.\ \isasymAnd n\ k.\ \#2\ *\ k\ \isasymin \ even\ \isasymLongrightarrow \ \isasymexists ka.\ Suc\ (Suc\ (\#2\ *\ k))\ =\ \#2\ *\ ka% |
|
142 \end{isabelle} |
|
143 % |
|
144 The \isa{rule_tac\ldots exI} tells Isabelle that the desired |
|
145 \isa{ka} is |
|
146 \isa{Suc\ k}. With this hint, the subgoal becomes trivial, and \isa{simp} |
|
147 concludes the proof. |
|
148 |
|
149 \medskip |
|
150 Combining the previous two results yields our objective, the |
|
151 equivalence relating \isa{even} and \isa{dvd}. |
|
152 % |
|
153 %we don't want [iff]: discuss? |
|
154 \begin{isabelle} |
|
155 \isacommand{theorem}\ even_iff_dvd:\ "(n\ \isasymin \ even)\ =\ (\#2\ dvd\ n)"\isanewline |
|
156 \isacommand{apply}\ (blast\ intro:\ dvd_imp_even\ even_imp_dvd)\isanewline |
|
157 \isacommand{done} |
|
158 \end{isabelle} |
|
159 |
|
160 \subsection{Generalization and rule induction} |
|
161 \label{sec:gen-rule-induction} |
|
162 |
|
163 Everybody knows that when before applying induction we often must generalize |
|
164 the induction formula. This step is just as important with rule induction, |
|
165 and the required generalizations can be complicated. In this |
|
166 example, the obvious statement of the result is not inductive: |
|
167 % |
|
168 \begin{isabelle} |
|
169 \isacommand{lemma}\ "Suc\ (Suc\ n)\ \isasymin \ even\ |
|
170 \isasymLongrightarrow \ n\ \isasymin \ even"\isanewline |
|
171 \isacommand{apply}\ (erule\ even.induct)\isanewline |
|
172 \isacommand{oops} |
|
173 \end{isabelle} |
|
174 % |
|
175 Rule induction finds no occurrences of \isa{Suc\ (Suc\ n)} in the |
|
176 conclusion, which it therefore leaves unchanged. (Look at |
|
177 \isa{even.induct} to see why this happens.) We get these subgoals: |
|
178 \begin{isabelle} |
|
179 \ 1.\ n\ \isasymin \ even\isanewline |
|
180 \ 2.\ \isasymAnd na.\ \isasymlbrakk na\ \isasymin \ even;\ n\ \isasymin \ even\isasymrbrakk \ \isasymLongrightarrow \ n\ \isasymin \ even% |
|
181 \end{isabelle} |
|
182 The first one is hopeless. In general, rule inductions involving |
|
183 non-trivial terms will probably go wrong. How to deal with such situations |
|
184 in general is described in {\S}\ref{sec:ind-var-in-prems} below. |
|
185 In the current case the solution is easy because |
|
186 we have the necessary inverse, subtraction: |
|
187 \begin{isabelle} |
|
188 \isacommand{lemma}\ even_imp_even_minus_2:\ "n\ \isasymin \ even\ \isasymLongrightarrow \ n-\#2\ \isasymin \ even"\isanewline |
|
189 \isacommand{apply}\ (erule\ even.induct)\isanewline |
|
190 \ \isacommand{apply}\ auto\isanewline |
|
191 \isacommand{done} |
|
192 \end{isabelle} |
|
193 % |
|
194 This lemma is trivially inductive. Here are the subgoals: |
|
195 \begin{isabelle} |
|
196 \ 1.\ 0\ -\ \#2\ \isasymin \ even\isanewline |
|
197 \ 2.\ \isasymAnd n.\ \isasymlbrakk n\ \isasymin \ even;\ n\ -\ \#2\ \isasymin \ even\isasymrbrakk \ \isasymLongrightarrow \ Suc\ (Suc\ n)\ -\ \#2\ \isasymin \ even% |
|
198 \end{isabelle} |
|
199 The first is trivial because \isa{0\ -\ \#2} simplifies to \isa{0}, which is |
|
200 even. The second is trivial too: \isa{Suc\ (Suc\ n)\ -\ \#2} simplifies to |
|
201 \isa{n}, matching the assumption. |
|
202 |
|
203 \medskip |
|
204 Using our lemma, we can easily prove the result we originally wanted: |
|
205 \begin{isabelle} |
|
206 \isacommand{lemma}\ Suc_Suc_even_imp_even:\ "Suc\ (Suc\ n)\ \isasymin \ even\ \isasymLongrightarrow \ n\ \isasymin \ even"\isanewline |
|
207 \isacommand{apply}\ (drule\ even_imp_even_minus_2)\isanewline |
|
208 \isacommand{apply}\ simp\isanewline |
|
209 \isacommand{done} |
|
210 \end{isabelle} |
|
211 |
|
212 We have just proved the converse of the introduction rule \isa{even.step}. |
|
213 This suggests proving the following equivalence. We give it the \isa{iff} |
|
214 attribute because of its obvious value for simplification. |
|
215 \begin{isabelle} |
|
216 \isacommand{lemma}\ [iff]:\ "((Suc\ (Suc\ n))\ \isasymin \ even)\ =\ (n\ |
|
217 \isasymin \ even)"\isanewline |
|
218 \isacommand{apply}\ (blast\ dest:\ Suc_Suc_even_imp_even)\isanewline |
|
219 \isacommand{done} |
|
220 \end{isabelle} |
|
221 |
|
222 The even numbers example has shown how inductive definitions can be used. |
|
223 Later examples will show that they are actually worth using. |
|