|
1 (*<*)theory Even imports Main begin |
|
2 ML_file "../../antiquote_setup.ML" |
|
3 setup Antiquote_Setup.setup |
|
4 (*>*) |
|
5 |
|
6 section{* The Set of Even Numbers *} |
|
7 |
|
8 text {* |
|
9 \index{even numbers!defining inductively|(}% |
|
10 The set of even numbers can be inductively defined as the least set |
|
11 containing 0 and closed under the operation $+2$. Obviously, |
|
12 \emph{even} can also be expressed using the divides relation (@{text dvd}). |
|
13 We shall prove below that the two formulations coincide. On the way we |
|
14 shall examine the primary means of reasoning about inductively defined |
|
15 sets: rule induction. |
|
16 *} |
|
17 |
|
18 subsection{* Making an Inductive Definition *} |
|
19 |
|
20 text {* |
|
21 Using \commdx{inductive\protect\_set}, we declare the constant @{text even} to be |
|
22 a set of natural numbers with the desired properties. |
|
23 *} |
|
24 |
|
25 inductive_set even :: "nat set" where |
|
26 zero[intro!]: "0 \<in> even" | |
|
27 step[intro!]: "n \<in> even \<Longrightarrow> (Suc (Suc n)) \<in> even" |
|
28 |
|
29 text {* |
|
30 An inductive definition consists of introduction rules. The first one |
|
31 above states that 0 is even; the second states that if $n$ is even, then so |
|
32 is~$n+2$. Given this declaration, Isabelle generates a fixed point |
|
33 definition for @{term even} and proves theorems about it, |
|
34 thus following the definitional approach (see {\S}\ref{sec:definitional}). |
|
35 These theorems |
|
36 include the introduction rules specified in the declaration, an elimination |
|
37 rule for case analysis and an induction rule. We can refer to these |
|
38 theorems by automatically-generated names. Here are two examples: |
|
39 @{named_thms[display,indent=0] even.zero[no_vars] (even.zero) even.step[no_vars] (even.step)} |
|
40 |
|
41 The introduction rules can be given attributes. Here |
|
42 both rules are specified as \isa{intro!},% |
|
43 \index{intro"!@\isa {intro"!} (attribute)} |
|
44 directing the classical reasoner to |
|
45 apply them aggressively. Obviously, regarding 0 as even is safe. The |
|
46 @{text step} rule is also safe because $n+2$ is even if and only if $n$ is |
|
47 even. We prove this equivalence later. |
|
48 *} |
|
49 |
|
50 subsection{*Using Introduction Rules*} |
|
51 |
|
52 text {* |
|
53 Our first lemma states that numbers of the form $2\times k$ are even. |
|
54 Introduction rules are used to show that specific values belong to the |
|
55 inductive set. Such proofs typically involve |
|
56 induction, perhaps over some other inductive set. |
|
57 *} |
|
58 |
|
59 lemma two_times_even[intro!]: "2*k \<in> even" |
|
60 apply (induct_tac k) |
|
61 apply auto |
|
62 done |
|
63 (*<*) |
|
64 lemma "2*k \<in> even" |
|
65 apply (induct_tac k) |
|
66 (*>*) |
|
67 txt {* |
|
68 \noindent |
|
69 The first step is induction on the natural number @{text k}, which leaves |
|
70 two subgoals: |
|
71 @{subgoals[display,indent=0,margin=65]} |
|
72 Here @{text auto} simplifies both subgoals so that they match the introduction |
|
73 rules, which are then applied automatically. |
|
74 |
|
75 Our ultimate goal is to prove the equivalence between the traditional |
|
76 definition of @{text even} (using the divides relation) and our inductive |
|
77 definition. One direction of this equivalence is immediate by the lemma |
|
78 just proved, whose @{text "intro!"} attribute ensures it is applied automatically. |
|
79 *} |
|
80 (*<*)oops(*>*) |
|
81 lemma dvd_imp_even: "2 dvd n \<Longrightarrow> n \<in> even" |
|
82 by (auto simp add: dvd_def) |
|
83 |
|
84 subsection{* Rule Induction \label{sec:rule-induction} *} |
|
85 |
|
86 text {* |
|
87 \index{rule induction|(}% |
|
88 From the definition of the set |
|
89 @{term even}, Isabelle has |
|
90 generated an induction rule: |
|
91 @{named_thms [display,indent=0,margin=40] even.induct [no_vars] (even.induct)} |
|
92 A property @{term P} holds for every even number provided it |
|
93 holds for~@{text 0} and is closed under the operation |
|
94 \isa{Suc(Suc \(\cdot\))}. Then @{term P} is closed under the introduction |
|
95 rules for @{term even}, which is the least set closed under those rules. |
|
96 This type of inductive argument is called \textbf{rule induction}. |
|
97 |
|
98 Apart from the double application of @{term Suc}, the induction rule above |
|
99 resembles the familiar mathematical induction, which indeed is an instance |
|
100 of rule induction; the natural numbers can be defined inductively to be |
|
101 the least set containing @{text 0} and closed under~@{term Suc}. |
|
102 |
|
103 Induction is the usual way of proving a property of the elements of an |
|
104 inductively defined set. Let us prove that all members of the set |
|
105 @{term even} are multiples of two. |
|
106 *} |
|
107 |
|
108 lemma even_imp_dvd: "n \<in> even \<Longrightarrow> 2 dvd n" |
|
109 txt {* |
|
110 We begin by applying induction. Note that @{text even.induct} has the form |
|
111 of an elimination rule, so we use the method @{text erule}. We get two |
|
112 subgoals: |
|
113 *} |
|
114 apply (erule even.induct) |
|
115 txt {* |
|
116 @{subgoals[display,indent=0]} |
|
117 We unfold the definition of @{text dvd} in both subgoals, proving the first |
|
118 one and simplifying the second: |
|
119 *} |
|
120 apply (simp_all add: dvd_def) |
|
121 txt {* |
|
122 @{subgoals[display,indent=0]} |
|
123 The next command eliminates the existential quantifier from the assumption |
|
124 and replaces @{text n} by @{text "2 * k"}. |
|
125 *} |
|
126 apply clarify |
|
127 txt {* |
|
128 @{subgoals[display,indent=0]} |
|
129 To conclude, we tell Isabelle that the desired value is |
|
130 @{term "Suc k"}. With this hint, the subgoal falls to @{text simp}. |
|
131 *} |
|
132 apply (rule_tac x = "Suc k" in exI, simp) |
|
133 (*<*)done(*>*) |
|
134 |
|
135 text {* |
|
136 Combining the previous two results yields our objective, the |
|
137 equivalence relating @{term even} and @{text dvd}. |
|
138 % |
|
139 %we don't want [iff]: discuss? |
|
140 *} |
|
141 |
|
142 theorem even_iff_dvd: "(n \<in> even) = (2 dvd n)" |
|
143 by (blast intro: dvd_imp_even even_imp_dvd) |
|
144 |
|
145 |
|
146 subsection{* Generalization and Rule Induction \label{sec:gen-rule-induction} *} |
|
147 |
|
148 text {* |
|
149 \index{generalizing for induction}% |
|
150 Before applying induction, we typically must generalize |
|
151 the induction formula. With rule induction, the required generalization |
|
152 can be hard to find and sometimes requires a complete reformulation of the |
|
153 problem. In this example, our first attempt uses the obvious statement of |
|
154 the result. It fails: |
|
155 *} |
|
156 |
|
157 lemma "Suc (Suc n) \<in> even \<Longrightarrow> n \<in> even" |
|
158 apply (erule even.induct) |
|
159 oops |
|
160 (*<*) |
|
161 lemma "Suc (Suc n) \<in> even \<Longrightarrow> n \<in> even" |
|
162 apply (erule even.induct) |
|
163 (*>*) |
|
164 txt {* |
|
165 Rule induction finds no occurrences of @{term "Suc(Suc n)"} in the |
|
166 conclusion, which it therefore leaves unchanged. (Look at |
|
167 @{text even.induct} to see why this happens.) We have these subgoals: |
|
168 @{subgoals[display,indent=0]} |
|
169 The first one is hopeless. Rule induction on |
|
170 a non-variable term discards information, and usually fails. |
|
171 How to deal with such situations |
|
172 in general is described in {\S}\ref{sec:ind-var-in-prems} below. |
|
173 In the current case the solution is easy because |
|
174 we have the necessary inverse, subtraction: |
|
175 *} |
|
176 (*<*)oops(*>*) |
|
177 lemma even_imp_even_minus_2: "n \<in> even \<Longrightarrow> n - 2 \<in> even" |
|
178 apply (erule even.induct) |
|
179 apply auto |
|
180 done |
|
181 (*<*) |
|
182 lemma "n \<in> even \<Longrightarrow> n - 2 \<in> even" |
|
183 apply (erule even.induct) |
|
184 (*>*) |
|
185 txt {* |
|
186 This lemma is trivially inductive. Here are the subgoals: |
|
187 @{subgoals[display,indent=0]} |
|
188 The first is trivial because @{text "0 - 2"} simplifies to @{text 0}, which is |
|
189 even. The second is trivial too: @{term "Suc (Suc n) - 2"} simplifies to |
|
190 @{term n}, matching the assumption.% |
|
191 \index{rule induction|)} %the sequel isn't really about induction |
|
192 |
|
193 \medskip |
|
194 Using our lemma, we can easily prove the result we originally wanted: |
|
195 *} |
|
196 (*<*)oops(*>*) |
|
197 lemma Suc_Suc_even_imp_even: "Suc (Suc n) \<in> even \<Longrightarrow> n \<in> even" |
|
198 by (drule even_imp_even_minus_2, simp) |
|
199 |
|
200 text {* |
|
201 We have just proved the converse of the introduction rule @{text even.step}. |
|
202 This suggests proving the following equivalence. We give it the |
|
203 \attrdx{iff} attribute because of its obvious value for simplification. |
|
204 *} |
|
205 |
|
206 lemma [iff]: "((Suc (Suc n)) \<in> even) = (n \<in> even)" |
|
207 by (blast dest: Suc_Suc_even_imp_even) |
|
208 |
|
209 |
|
210 subsection{* Rule Inversion \label{sec:rule-inversion} *} |
|
211 |
|
212 text {* |
|
213 \index{rule inversion|(}% |
|
214 Case analysis on an inductive definition is called \textbf{rule |
|
215 inversion}. It is frequently used in proofs about operational |
|
216 semantics. It can be highly effective when it is applied |
|
217 automatically. Let us look at how rule inversion is done in |
|
218 Isabelle/HOL\@. |
|
219 |
|
220 Recall that @{term even} is the minimal set closed under these two rules: |
|
221 @{thm [display,indent=0] even.intros [no_vars]} |
|
222 Minimality means that @{term even} contains only the elements that these |
|
223 rules force it to contain. If we are told that @{term a} |
|
224 belongs to |
|
225 @{term even} then there are only two possibilities. Either @{term a} is @{text 0} |
|
226 or else @{term a} has the form @{term "Suc(Suc n)"}, for some suitable @{term n} |
|
227 that belongs to |
|
228 @{term even}. That is the gist of the @{term cases} rule, which Isabelle proves |
|
229 for us when it accepts an inductive definition: |
|
230 @{named_thms [display,indent=0,margin=40] even.cases [no_vars] (even.cases)} |
|
231 This general rule is less useful than instances of it for |
|
232 specific patterns. For example, if @{term a} has the form |
|
233 @{term "Suc(Suc n)"} then the first case becomes irrelevant, while the second |
|
234 case tells us that @{term n} belongs to @{term even}. Isabelle will generate |
|
235 this instance for us: |
|
236 *} |
|
237 |
|
238 inductive_cases Suc_Suc_cases [elim!]: "Suc(Suc n) \<in> even" |
|
239 |
|
240 text {* |
|
241 The \commdx{inductive\protect\_cases} command generates an instance of |
|
242 the @{text cases} rule for the supplied pattern and gives it the supplied name: |
|
243 @{named_thms [display,indent=0] Suc_Suc_cases [no_vars] (Suc_Suc_cases)} |
|
244 Applying this as an elimination rule yields one case where @{text even.cases} |
|
245 would yield two. Rule inversion works well when the conclusions of the |
|
246 introduction rules involve datatype constructors like @{term Suc} and @{text "#"} |
|
247 (list ``cons''); freeness reasoning discards all but one or two cases. |
|
248 |
|
249 In the \isacommand{inductive\_cases} command we supplied an |
|
250 attribute, @{text "elim!"}, |
|
251 \index{elim"!@\isa {elim"!} (attribute)}% |
|
252 indicating that this elimination rule can be |
|
253 applied aggressively. The original |
|
254 @{term cases} rule would loop if used in that manner because the |
|
255 pattern~@{term a} matches everything. |
|
256 |
|
257 The rule @{text Suc_Suc_cases} is equivalent to the following implication: |
|
258 @{term [display,indent=0] "Suc (Suc n) \<in> even \<Longrightarrow> n \<in> even"} |
|
259 Just above we devoted some effort to reaching precisely |
|
260 this result. Yet we could have obtained it by a one-line declaration, |
|
261 dispensing with the lemma @{text even_imp_even_minus_2}. |
|
262 This example also justifies the terminology |
|
263 \textbf{rule inversion}: the new rule inverts the introduction rule |
|
264 @{text even.step}. In general, a rule can be inverted when the set of elements |
|
265 it introduces is disjoint from those of the other introduction rules. |
|
266 |
|
267 For one-off applications of rule inversion, use the \methdx{ind_cases} method. |
|
268 Here is an example: |
|
269 *} |
|
270 |
|
271 (*<*)lemma "Suc(Suc n) \<in> even \<Longrightarrow> P"(*>*) |
|
272 apply (ind_cases "Suc(Suc n) \<in> even") |
|
273 (*<*)oops(*>*) |
|
274 |
|
275 text {* |
|
276 The specified instance of the @{text cases} rule is generated, then applied |
|
277 as an elimination rule. |
|
278 |
|
279 To summarize, every inductive definition produces a @{text cases} rule. The |
|
280 \commdx{inductive\protect\_cases} command stores an instance of the |
|
281 @{text cases} rule for a given pattern. Within a proof, the |
|
282 @{text ind_cases} method applies an instance of the @{text cases} |
|
283 rule. |
|
284 |
|
285 The even numbers example has shown how inductive definitions can be |
|
286 used. Later examples will show that they are actually worth using.% |
|
287 \index{rule inversion|)}% |
|
288 \index{even numbers!defining inductively|)} |
|
289 *} |
|
290 |
|
291 (*<*)end(*>*) |