3 begin |
3 begin |
4 |
4 |
5 section{* Examples of Inductive Definitions \label{sec:ind-examples} *} |
5 section{* Examples of Inductive Definitions \label{sec:ind-examples} *} |
6 |
6 |
7 text {* |
7 text {* |
8 Let us first give three examples showing how to define inductive predicates |
8 Let us first give three examples showing how to define by hand inductive |
9 by hand and then how to prove characteristic properties about them, such as |
9 predicates and then also how to prove by hand characteristic properties |
10 introduction rules and an induction principle. From these examples, we will |
10 about them, such as introduction rules and induction principles. From |
11 figure out a |
11 these examples, we will figure out a general method for defining inductive |
12 general method for defining inductive predicates. The aim in this section is |
12 predicates. The aim in this section is \emph{not} to write proofs that are as |
13 not to write proofs that are as beautiful as possible, but as close as |
13 beautiful as possible, but as close as possible to the ML-code we will |
14 possible to the ML-code producing the proofs that we will develop later. |
14 develop later. |
|
15 |
15 |
16 |
16 As a first example, let us consider the transitive closure of a relation @{text |
17 As a first example, let us consider the transitive closure of a relation @{text |
17 R}. It is an inductive predicate characterized by the two introduction rules |
18 R}. It is an inductive predicate characterised by the two introduction rules: |
18 |
19 |
19 \begin{center} |
20 \begin{center} |
20 @{term[mode=Axiom] "trcl R x x"} \hspace{5mm} |
21 @{prop[mode=Axiom] "trcl R x x"} \hspace{5mm} |
21 @{term[mode=Rule] "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"} |
22 @{prop[mode=Rule] "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"} |
22 \end{center} |
23 \end{center} |
23 |
|
24 (FIXME first rule should be an ``axiom'') |
|
25 |
24 |
26 Note that the @{text trcl} predicate has two different kinds of parameters: the |
25 Note that the @{text trcl} predicate has two different kinds of parameters: the |
27 first parameter @{text R} stays \emph{fixed} throughout the definition, whereas |
26 first parameter @{text R} stays \emph{fixed} throughout the definition, whereas |
28 the second and third parameter changes in the ``recursive call''. |
27 the second and third parameter changes in the ``recursive call''. This will |
|
28 become important later on when we deal with fixed parameters and locales. |
29 |
29 |
30 Since an inductively defined predicate is the least predicate closed under |
30 Since an inductively defined predicate is the least predicate closed under |
31 a collection of introduction rules, we define the predicate @{text "trcl R x y"} in |
31 a collection of introduction rules, we define the predicate @{text "trcl R x y"} in |
32 such a way that it holds if and only if @{text "P x y"} holds for every predicate |
32 such a way that it holds if and only if @{text "P x y"} holds for every predicate |
33 @{text P} closed under the rules above. This gives rise to the definition |
33 @{text P} closed under the rules above. This gives rise to the definition |
36 definition "trcl R x y \<equiv> |
36 definition "trcl R x y \<equiv> |
37 \<forall>P. (\<forall>x. P x x) \<longrightarrow> (\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z) \<longrightarrow> P x y" |
37 \<forall>P. (\<forall>x. P x x) \<longrightarrow> (\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z) \<longrightarrow> P x y" |
38 |
38 |
39 text {* |
39 text {* |
40 where we quantify over the predicate @{text P}. Note that we have to use the |
40 where we quantify over the predicate @{text P}. Note that we have to use the |
41 object implication @{text "\<longrightarrow>"} and object quantification @{text "\<forall>"} for stating |
41 object implication @{text "\<longrightarrow>"} and object quantification @{text "\<forall>"} for |
42 this definition. The introduction rules and induction principles derived later |
42 stating this definition (there is no other way for definitions in |
43 should use the corresponding meta-connectives since they simplify the reasoning for |
43 HOL). However, the introduction rules and induction principles derived later |
44 the user. |
44 should use the corresponding meta-connectives since they simplify the |
45 |
45 reasoning for the user. |
46 With this definition, the proof of the induction theorem for the transitive |
46 |
|
47 With this definition, the proof of the induction principle for the transitive |
47 closure is almost immediate. It suffices to convert all the meta-level |
48 closure is almost immediate. It suffices to convert all the meta-level |
48 connectives in the induction rule to object-level connectives using the |
49 connectives in the lemma to object-level connectives using the |
49 @{text atomize} proof method (Line 4), expand the definition of @{text trcl} |
50 proof method @{text atomize} (Line 4), expand the definition of @{text trcl} |
50 (Line 5 and 6), eliminate the universal quantifier contained in it (Line 7), |
51 (Line 5 and 6), eliminate the universal quantifier contained in it (Line 7), |
51 and then solve the goal by assumption (Line 8). |
52 and then solve the goal by assumption (Line 8). |
52 |
53 |
53 *} |
54 *} |
54 |
55 |
62 apply(assumption) |
63 apply(assumption) |
63 done |
64 done |
64 |
65 |
65 text {* |
66 text {* |
66 The proofs for the introduction are slightly more complicated. We need to prove |
67 The proofs for the introduction are slightly more complicated. We need to prove |
67 the goals @{prop "trcl R x x"} and @{prop "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"}. |
68 the facs @{prop "trcl R x x"} and @{prop "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z"}. |
68 In order to prove the first goal, we again unfold the definition and |
69 In order to prove the first goal, we again unfold the definition and |
69 then apply the introdution rules for @{text "\<forall>"} and @{text "\<longrightarrow>"} as often as possible. |
70 then apply the introdution rules for @{text "\<forall>"} and @{text "\<longrightarrow>"} as often as possible. |
70 We then end up in the goal state |
71 We then end up in the goal state: |
71 |
|
72 *} |
72 *} |
73 |
73 |
74 (*<*)lemma "trcl R x x" |
74 (*<*)lemma "trcl R x x" |
75 apply (unfold trcl_def) |
75 apply (unfold trcl_def) |
76 apply (rule allI impI)+(*>*) |
76 apply (rule allI impI)+(*>*) |
90 apply(drule spec) |
90 apply(drule spec) |
91 apply(assumption) |
91 apply(assumption) |
92 done |
92 done |
93 |
93 |
94 text {* |
94 text {* |
95 Since the second introduction rule has premises, its proof is not as easy. After unfolding |
95 Since the second @{text trcl}-rule has premises, the proof of its |
96 the definitions and applying the introduction rules for @{text "\<forall>"} and @{text "\<longrightarrow>"}, we |
96 introduction rule is not as easy. After unfolding the definitions and |
97 get the goal state |
97 applying the introduction rules for @{text "\<forall>"} and @{text "\<longrightarrow>"}, we get the |
|
98 goal state: |
98 *} |
99 *} |
99 |
100 |
100 (*<*)lemma "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z" |
101 (*<*)lemma "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z" |
101 apply (unfold trcl_def) |
102 apply (unfold trcl_def) |
102 apply (rule allI impI)+(*>*) |
103 apply (rule allI impI)+(*>*) |
103 txt {*@{subgoals [display]} *} |
104 txt {*@{subgoals [display]} *} |
104 (*<*)oops(*>*) |
105 (*<*)oops(*>*) |
105 |
106 |
106 text {* |
107 text {* |
107 The third and fourth assumption corresponds to the first and second |
108 The third and fourth assumption correspond to the first and second |
108 introduction rule, respectively, whereas the first and second assumption |
109 introduction rule, respectively, whereas the first and second assumption |
109 corresponds to the pre\-mises of the introduction rule. Since we want to prove |
110 corresponds to the pre\-mises of the introduction rule. Since we want to prove |
110 the second introduction rule, we apply the fourth assumption to the goal |
111 the second introduction rule, we apply the fourth assumption to the goal |
111 @{term "P x z"}. In order for the assumption to be applicable as a rule, we have to |
112 @{term "P x z"}. In order for the assumption to be applicable as a rule, we have to |
112 eliminate the universal quantifier and turn the object-level implications |
113 eliminate the universal quantifier and turn the object-level implications |
147 have a3: "\<forall>x. P x x" by fact |
148 have a3: "\<forall>x. P x x" by fact |
148 have a4: "\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z" by fact |
149 have a4: "\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z" by fact |
149 show "P x z" |
150 show "P x z" |
150 apply(rule a4[rule_format]) |
151 apply(rule a4[rule_format]) |
151 apply(rule a1) |
152 apply(rule a1) |
152 apply(rule a2 [THEN spec[where x=P], THEN mp, THEN mp, OF a3, OF a4]) |
153 apply(rule a2[THEN spec[where x=P], THEN mp, THEN mp, OF a3, OF a4]) |
153 done |
154 done |
154 qed |
155 qed |
155 |
156 |
156 text {* |
157 text {* |
157 It might be surprising that we are not using the automatic tactics in |
158 It might be surprising that we are not using the automatic tactics available in |
158 Isabelle in order to prove the lemmas we are after. After all @{text "blast"} |
159 Isabelle for proving this lemmas. After all @{text "blast"} would easily |
159 would easily dispense of the lemmas. |
160 dispense of it. |
160 *} |
161 *} |
161 |
162 |
162 lemma trcl_step_blast: "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z" |
163 lemma trcl_step_blast: "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z" |
163 apply(unfold trcl_def) |
164 apply(unfold trcl_def) |
164 apply(blast) |
165 apply(blast) |
165 done |
166 done |
166 |
167 |
167 text {* |
168 text {* |
168 Experience has shown that it is generally a bad idea to rely heavily on @{term blast} |
169 Experience has shown that it is generally a bad idea to rely heavily on |
169 and the like in automated proofs. The reason is that you do not have precise control |
170 @{text blast}, @{text auto} and the like in automated proofs. The reason is |
170 over them (the user can, for example, declare new intro- or simplification rules that |
171 that you do not have precise control over them (the user can, for example, |
171 can throw automatic tactics off course) and also it is very hard to debug |
172 declare new intro- or simplification rules that can throw automatic tactics |
172 proofs involving automatic tactics. Therefore whenever possible, automatic tactics |
173 off course) and also it is very hard to debug proofs involving automatic |
173 should be avoided or constrained. |
174 tactics whenever something goes wrong. Therefore if possible, automatic |
174 |
175 tactics should be avoided or sufficiently constrained. |
175 |
176 |
176 This method of defining inductive predicates generalises also to mutually inductive |
177 The method of defining inductive predicates by impredicative quantification |
177 predicates. The next example defines the predicates @{text even} and @{text odd} |
178 also generalises to mutually inductive predicates. The next example defines |
178 characterised by the following rules: |
179 the predicates @{text even} and @{text odd} characterised by the following |
|
180 rules: |
179 |
181 |
180 \begin{center} |
182 \begin{center} |
181 @{term[mode=Axiom] "even (0::nat)"} \hspace{5mm} |
183 @{prop[mode=Axiom] "even (0::nat)"} \hspace{5mm} |
182 @{term[mode=Rule] "odd m \<Longrightarrow> even (Suc m)"} \hspace{5mm} |
184 @{prop[mode=Rule] "odd m \<Longrightarrow> even (Suc m)"} \hspace{5mm} |
183 @{term[mode=Rule] "even m \<Longrightarrow> odd (Suc m)"} |
185 @{prop[mode=Rule] "even m \<Longrightarrow> odd (Suc m)"} |
184 \end{center} |
186 \end{center} |
185 |
187 |
186 Since the predicates are mutually inductive, each definition |
188 Since the predicates are mutually inductive, each definition |
187 quantifies over both predicates, below named @{text P} and @{text Q}. |
189 quantifies over both predicates, below named @{text P} and @{text Q}. |
188 *} |
190 *} |
194 definition "odd n \<equiv> |
196 definition "odd n \<equiv> |
195 \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) |
197 \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) |
196 \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> Q n" |
198 \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> Q n" |
197 |
199 |
198 text {* |
200 text {* |
199 For proving the induction rule, we use exactly the same technique as in the transitive |
201 For proving the induction principles, we use exactly the same technique |
200 closure example: |
202 as in the transitive closure example, namely: |
201 *} |
203 *} |
202 |
204 |
203 lemma even_induct: |
205 lemma even_induct: |
204 assumes asm: "even n" |
206 assumes asm: "even n" |
205 shows "P 0 \<Longrightarrow> |
207 shows "P 0 \<Longrightarrow> |
211 apply(drule spec[where x=Q]) |
213 apply(drule spec[where x=Q]) |
212 apply(assumption) |
214 apply(assumption) |
213 done |
215 done |
214 |
216 |
215 text {* |
217 text {* |
216 We omit the other induction rule having @{term "Q n"} as conclusion. |
218 We omit the other induction principle that has @{term "Q n"} as conclusion. |
217 The proofs of the introduction rules are also very similar to the ones in the |
219 The proofs of the introduction rules are also very similar to the ones in the |
218 @{text "trcl"}-example. We only show the proof of the second introduction rule: |
220 @{text "trcl"}-example. We only show the proof of the second introduction rule. |
219 *} |
221 *} |
220 |
222 |
221 lemma evenS: "odd m \<Longrightarrow> even (Suc m)" |
223 lemma evenS: "odd m \<Longrightarrow> even (Suc m)" |
222 apply (unfold odd_def even_def) |
224 apply (unfold odd_def even_def) |
223 apply (rule allI impI)+ |
225 apply (rule allI impI)+ |
234 THEN mp, THEN mp, THEN mp, OF a2, OF a3, OF a4]) |
236 THEN mp, THEN mp, THEN mp, OF a2, OF a3, OF a4]) |
235 done |
237 done |
236 qed |
238 qed |
237 |
239 |
238 text {* |
240 text {* |
239 As a final example, we definethe accessible part of a relation @{text R} characterised |
241 As a final example, we define the accessible part of a relation @{text R} characterised |
240 by the introduction rule |
242 by the introduction rule |
241 |
243 |
242 \begin{center} |
244 \begin{center} |
243 @{term[mode=Rule] "(\<forall>y. R y x \<longrightarrow> accpart R y) \<Longrightarrow> accpart R x"} |
245 @{term[mode=Rule] "(\<forall>y. R y x \<longrightarrow> accpart R y) \<Longrightarrow> accpart R x"} |
244 \end{center} |
246 \end{center} |
245 |
247 |
246 whose premise involves a universal quantifier and an implication. The |
248 whose premise involves a universal quantifier and an implication. The |
247 definition of @{text accpart} is as follows: |
249 definition of @{text accpart} is: |
248 *} |
250 *} |
249 |
251 |
250 definition "accpart R x \<equiv> \<forall>P. (\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> P x" |
252 definition "accpart R x \<equiv> \<forall>P. (\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> P x" |
251 |
253 |
252 text {* |
254 text {* |
253 The proof of the induction theorem is again straightforward. |
255 The proof of the induction principle is again straightforward. |
254 *} |
256 *} |
255 |
257 |
256 lemma accpart_induct: |
258 lemma accpart_induct: |
257 assumes asm: "accpart R x" |
259 assumes asm: "accpart R x" |
258 shows "(\<And>x. (\<forall>y. R y x \<longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P x" |
260 shows "(\<And>x. (\<forall>y. R y x \<longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P x" |