36 \<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" |
37 |
38 |
38 text {* |
39 text {* |
39 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 |
40 object implication @{text "\<longrightarrow>"} and object quantification @{text "\<forall>"} for stating |
41 object implication @{text "\<longrightarrow>"} and object quantification @{text "\<forall>"} for stating |
41 this definition. |
42 this definition. The introduction rules and induction principles derived later |
42 |
43 should use the corresponding meta-connectives since they simplify the reasoning for |
43 With this definition of the transitive closure, the proof of the induction |
44 the user. |
44 theorem is almost immediate. It suffices to convert all the meta-level connectives |
45 |
45 in the induction rule to object-level connectives using the @{text atomize} proof |
46 With this definition, the proof of the induction theorem for the transitive |
46 method, expand the definition of @{text trcl}, eliminate the universal quantifier |
47 closure is almost immediate. It suffices to convert all the meta-level |
47 contained in it, and then solve the goal by assumption. |
48 connectives in the induction rule to object-level connectives using the |
48 |
49 @{text atomize} proof method (Line 4), expand the definition of @{text trcl} |
49 (FIXME: add linenumbers to the proof below and the text above) |
50 (Line 5 and 6), eliminate the universal quantifier contained in it (Line 7), |
|
51 and then solve the goal by assumption (Line 8). |
|
52 |
50 *} |
53 *} |
51 |
54 |
52 lemma %linenos trcl_induct: |
55 lemma %linenos trcl_induct: |
53 assumes asm: "trcl R x y" |
56 assumes asm: "trcl R x y" |
54 shows "(\<And>x. P x x) \<Longrightarrow> (\<And>x y z. R x y \<Longrightarrow> P y z \<Longrightarrow> P x z) \<Longrightarrow> P x y" |
57 shows "(\<And>x. P x x) \<Longrightarrow> (\<And>x y z. R x y \<Longrightarrow> P y z \<Longrightarrow> P x z) \<Longrightarrow> P x y" |
58 apply(drule spec[where x=P]) |
61 apply(drule spec[where x=P]) |
59 apply(assumption) |
62 apply(assumption) |
60 done |
63 done |
61 |
64 |
62 text {* |
65 text {* |
63 We now turn to the proofs of the introduction rules, which are slightly more complicated. |
66 The proofs for the introduction are slightly more complicated. We need to prove |
64 In order to prove the first introduction rule, we again unfold the definition and |
67 the goals @{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 |
65 then apply the introdution rules for @{text "\<forall>"} and @{text "\<longrightarrow>"} as often as possible. |
69 then apply the introdution rules for @{text "\<forall>"} and @{text "\<longrightarrow>"} as often as possible. |
66 We then end up in a proof state of the following form: |
70 We then end up in the goal state |
67 |
71 |
68 *} |
72 *} |
69 |
73 |
70 (*<*)lemma "trcl R x x" |
74 (*<*)lemma "trcl R x x" |
71 apply (unfold trcl_def) |
75 apply (unfold trcl_def) |
72 apply (rule allI impI)+(*>*) |
76 apply (rule allI impI)+(*>*) |
73 txt {* @{subgoals [display]} *} |
77 txt {* @{subgoals [display]} *} |
74 (*<*)oops(*>*) |
78 (*<*)oops(*>*) |
75 |
79 |
76 text {* |
80 text {* |
77 The two assumptions correspond to the introduction rules, where @{text "trcl |
81 The two assumptions correspond to the introduction rules, where @{text "trcl |
78 R"} has been replaced by P. Thus, all we have to do is to eliminate the |
82 R"} has been replaced by P. Thus, all we have to do is to eliminate the |
79 universal quantifier in front of the first assumption, and then solve the |
83 universal quantifier in front of the first assumption, and then solve the |
80 goal by assumption: |
84 goal by assumption. Thus the proof is: |
81 *} |
85 *} |
82 |
|
83 |
86 |
84 lemma trcl_base: "trcl R x x" |
87 lemma trcl_base: "trcl R x x" |
85 apply(unfold trcl_def) |
88 apply(unfold trcl_def) |
86 apply(rule allI impI)+ |
89 apply(rule allI impI)+ |
87 apply(drule spec) |
90 apply(drule spec) |
88 apply(assumption) |
91 apply(assumption) |
89 done |
92 done |
90 |
93 |
91 text {* |
94 text {* |
92 Since the second introduction rule has premises, its proof is not as easy as the previous |
95 Since the second introduction rule has premises, its proof is not as easy. After unfolding |
93 one. After unfolding the definitions and applying the introduction rules for @{text "\<forall>"} |
96 the definitions and applying the introduction rules for @{text "\<forall>"} and @{text "\<longrightarrow>"}, we |
94 and @{text "\<longrightarrow>"}, we get the proof state |
97 get the goal state |
95 *} |
98 *} |
96 |
|
97 |
99 |
98 (*<*)lemma "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z" |
100 (*<*)lemma "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z" |
99 apply (unfold trcl_def) |
101 apply (unfold trcl_def) |
100 apply (rule allI impI)+(*>*) |
102 apply (rule allI impI)+(*>*) |
101 txt {*@{subgoals [display]} *} |
103 txt {*@{subgoals [display]} *} |
102 (*<*)oops(*>*) |
104 (*<*)oops(*>*) |
103 |
105 |
104 text {* |
106 text {* |
105 The third and fourth assumption corresponds to the first and second introduction rule, |
107 The third and fourth assumption corresponds to the first and second |
106 respectively, whereas the first and second assumption corresponds to the premises of |
108 introduction rule, respectively, whereas the first and second assumption |
107 the introduction rule. Since we want to prove the second introduction rule, we apply |
109 corresponds to the pre\-mises of the introduction rule. Since we want to prove |
108 the fourth assumption to the goal @{term "P x z"}. In order for the assumption to |
110 the second introduction rule, we apply the fourth assumption to the goal |
109 be applicable, we have to eliminate the universal quantifiers and turn the object-level |
111 @{term "P x z"}. In order for the assumption to be applicable as a rule, we have to |
110 implications into meta-level ones. This can be accomplished using the @{text rule_format} |
112 eliminate the universal quantifier and turn the object-level implications |
111 attribute. Applying the assumption produces two new subgoals, which can be solved using |
113 into meta-level ones. This can be accomplished using the @{text rule_format} |
112 the first and second assumption. The second assumption again involves a quantifier and |
114 attribute. Applying the assumption produces the two new subgoals |
113 implications that have to be eliminated before it can be applied. To avoid problems |
115 *} |
114 with higher order unification, it is advisable to provide an instantiation for the |
116 |
115 universally quantified predicate variable in the assumption. |
117 (*<*)lemma "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z" |
|
118 apply (unfold trcl_def) |
|
119 apply (rule allI impI)+ |
|
120 proof - |
|
121 case (goal1 P) |
|
122 have a4: "\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z" by fact |
|
123 show ?case |
|
124 apply (rule a4[rule_format])(*>*) |
|
125 txt {*@{subgoals [display]} *} |
|
126 (*<*)oops(*>*) |
|
127 |
|
128 text {* |
|
129 which can be |
|
130 solved using the first and second assumption. The second assumption again |
|
131 involves a quantifier and an implications that have to be eliminated before it |
|
132 can be applied. To avoid potential problems with higher-order unification, |
|
133 we should explcitly instantiate the universally quantified |
|
134 predicate variable to @{text "P"} and also match explicitly the implications |
|
135 with the the third and fourth assumption. This gives the proof: |
116 *} |
136 *} |
117 |
137 |
118 |
138 |
119 lemma trcl_step: "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z" |
139 lemma trcl_step: "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z" |
120 apply (unfold trcl_def) |
140 apply(unfold trcl_def) |
121 apply (rule allI impI)+ |
141 apply(rule allI impI)+ |
122 proof - |
142 proof - |
123 case (goal1 P) |
143 case (goal1 P) |
124 have g1: "R x y" by fact |
144 have a1: "R x y" by fact |
125 have g2: "\<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 y z" by fact |
145 have a2: "\<forall>P. (\<forall>x. P x x) |
126 have g3: "\<forall>x. P x x" by fact |
146 \<longrightarrow> (\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z) \<longrightarrow> P y z" by fact |
127 have g4: "\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z" by fact |
147 have a3: "\<forall>x. P x x" by fact |
128 show ?case |
148 have a4: "\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z" by fact |
129 apply (rule g4 [rule_format]) |
149 show "P x z" |
130 apply (rule g1) |
150 apply(rule a4[rule_format]) |
131 apply (rule g2 [THEN spec [where x=P], THEN mp, THEN mp, OF g3, OF g4]) |
151 apply(rule a1) |
132 done |
152 apply(rule a2 [THEN spec[where x=P], THEN mp, THEN mp, OF a3, OF a4]) |
133 qed |
153 done |
134 |
154 qed |
135 text {* |
155 |
136 |
156 text {* |
137 This method of defining inductive predicates easily generalizes to mutually inductive |
157 It might be surprising that we are not using the automatic tactics in |
138 predicates, like the predicates @{text even} and @{text odd} characterized by the |
158 Isabelle in order to prove the lemmas we are after. After all @{text "blast"} |
139 following introduction rules: |
159 would easily dispense of the lemmas. |
|
160 *} |
|
161 |
|
162 lemma trcl_step_blast: "R x y \<Longrightarrow> trcl R y z \<Longrightarrow> trcl R x z" |
|
163 apply(unfold trcl_def) |
|
164 apply(blast) |
|
165 done |
|
166 |
|
167 text {* |
|
168 Experience has shown that it is generally a bad idea to rely heavily on @{term blast} |
|
169 and the like in automated proofs. The reason is that you do not have precise control |
|
170 over them (the user can, for example, declare new intro- or simplification rules that |
|
171 can throw automatic tactics off course) and also it is very hard to debug |
|
172 proofs involving automatic tactics. Therefore whenever possible, automatic tactics |
|
173 should be avoided or constrained. |
|
174 |
|
175 |
|
176 This method of defining inductive predicates generalises also to mutually inductive |
|
177 predicates. The next example defines the predicates @{text even} and @{text odd} |
|
178 characterised by the following rules: |
140 |
179 |
141 \begin{center} |
180 \begin{center} |
142 @{term[mode=Axiom] "even (0::nat)"} \hspace{5mm} |
181 @{term[mode=Axiom] "even (0::nat)"} \hspace{5mm} |
143 @{term[mode=Rule] "odd m \<Longrightarrow> even (Suc m)"} \hspace{5mm} |
182 @{term[mode=Rule] "odd m \<Longrightarrow> even (Suc m)"} \hspace{5mm} |
144 @{term[mode=Rule] "even m \<Longrightarrow> odd (Suc m)"} |
183 @{term[mode=Rule] "even m \<Longrightarrow> odd (Suc m)"} |
145 \end{center} |
184 \end{center} |
146 |
185 |
147 Since the predicates are mutually inductive, each of the definitions contain two |
186 Since the predicates are mutually inductive, each definition |
148 quantifiers over the predicates @{text P} and @{text Q}. |
187 quantifies over both predicates, below named @{text P} and @{text Q}. |
149 *} |
188 *} |
150 |
189 |
151 definition "even n \<equiv> |
190 definition "even n \<equiv> |
152 \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) |
191 \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) |
153 \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> P n" |
192 \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> P n" |
160 For proving the induction rule, we use exactly the same technique as in the transitive |
199 For proving the induction rule, we use exactly the same technique as in the transitive |
161 closure example: |
200 closure example: |
162 *} |
201 *} |
163 |
202 |
164 lemma even_induct: |
203 lemma even_induct: |
165 assumes even: "even n" |
204 assumes asm: "even n" |
166 shows "P 0 \<Longrightarrow> |
205 shows "P 0 \<Longrightarrow> |
167 (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n" |
206 (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n" |
168 apply (atomize (full)) |
207 apply(atomize (full)) |
169 apply (cut_tac even) |
208 apply(cut_tac asm) |
170 apply (unfold even_def) |
209 apply(unfold even_def) |
171 apply (drule spec [where x=P]) |
210 apply(drule spec[where x=P]) |
172 apply (drule spec [where x=Q]) |
211 apply(drule spec[where x=Q]) |
173 apply assumption |
212 apply(assumption) |
174 done |
213 done |
175 |
214 |
176 text {* |
215 text {* |
177 A similar induction rule having @{term "Q n"} as a conclusion can be proved for |
216 We omit the other induction rule having @{term "Q n"} as conclusion. |
178 the @{text odd} predicate. |
|
179 The proofs of the introduction rules are also very similar to the ones in the |
217 The proofs of the introduction rules are also very similar to the ones in the |
180 previous example. We only show the proof of the second introduction rule, |
218 @{text "trcl"}-example. We only show the proof of the second introduction rule: |
181 since it is almost the same as the one for the third introduction rule, |
|
182 and the proof of the first rule is trivial. |
|
183 *} |
219 *} |
184 |
220 |
185 lemma evenS: "odd m \<Longrightarrow> even (Suc m)" |
221 lemma evenS: "odd m \<Longrightarrow> even (Suc m)" |
186 apply (unfold odd_def even_def) |
222 apply (unfold odd_def even_def) |
187 apply (rule allI impI)+ |
223 apply (rule allI impI)+ |
188 proof - |
224 proof - |
189 case goal1 |
225 case (goal1 P) |
190 show ?case |
226 have a1: "\<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) |
191 apply (rule goal1(3) [rule_format]) |
227 \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> Q m" by fact |
192 apply (rule goal1(1) [THEN spec [where x=P], THEN spec [where x=Q], |
228 have a2: "P 0" by fact |
193 THEN mp, THEN mp, THEN mp, OF goal1(2-4)]) |
229 have a3: "\<forall>m. Q m \<longrightarrow> P (Suc m)" by fact |
194 done |
230 have a4: "\<forall>m. P m \<longrightarrow> Q (Suc m)" by fact |
195 qed |
231 show "P (Suc m)" |
196 (*<*) |
232 apply(rule a3[rule_format]) |
197 lemma even0: "even 0" |
233 apply(rule a1[THEN spec[where x=P], THEN spec[where x=Q], |
198 apply (unfold even_def) |
234 THEN mp, THEN mp, THEN mp, OF a2, OF a3, OF a4]) |
199 apply (rule allI impI)+ |
235 done |
200 apply assumption |
236 qed |
201 done |
237 |
202 |
238 text {* |
203 lemma oddS: "even m \<Longrightarrow> odd (Suc m)" |
239 As a final example, we definethe accessible part of a relation @{text R} characterised |
204 apply (unfold odd_def even_def) |
240 by the introduction rule |
205 apply (rule allI impI)+ |
|
206 proof - |
|
207 case goal1 |
|
208 show ?case |
|
209 apply (rule goal1(4) [rule_format]) |
|
210 apply (rule goal1(1) [THEN spec [where x=P], THEN spec [where x=Q], |
|
211 THEN mp, THEN mp, THEN mp, OF goal1(2-4)]) |
|
212 done |
|
213 qed |
|
214 (*>*) |
|
215 |
|
216 text {* |
|
217 As a final example, we will consider the definition of the accessible |
|
218 part of a relation @{text R} characterized by the introduction rule |
|
219 |
241 |
220 \begin{center} |
242 \begin{center} |
221 @{term[mode=Rule] "(\<forall>y. R y x \<longrightarrow> accpart R y) \<Longrightarrow> accpart R x"} |
243 @{term[mode=Rule] "(\<forall>y. R y x \<longrightarrow> accpart R y) \<Longrightarrow> accpart R x"} |
222 \end{center} |
244 \end{center} |
223 |
245 |
226 *} |
248 *} |
227 |
249 |
228 definition "accpart R x \<equiv> \<forall>P. (\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> P x" |
250 definition "accpart R x \<equiv> \<forall>P. (\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> P x" |
229 |
251 |
230 text {* |
252 text {* |
231 The proof of the induction theorem is again straightforward: |
253 The proof of the induction theorem is again straightforward. |
232 *} |
254 *} |
233 |
255 |
234 lemma accpart_induct: |
256 lemma accpart_induct: |
235 assumes acc: "accpart R x" |
257 assumes asm: "accpart R x" |
236 shows "(\<And>x. (\<And>y. R y x \<Longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P x" |
258 shows "(\<And>x. (\<forall>y. R y x \<longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P x" |
237 apply (atomize (full)) |
259 apply(atomize (full)) |
238 apply (cut_tac acc) |
260 apply(cut_tac asm) |
239 apply (unfold accpart_def) |
261 apply(unfold accpart_def) |
240 apply (drule spec [where x=P]) |
262 apply(drule spec[where x=P]) |
241 apply assumption |
263 apply(assumption) |
242 done |
264 done |
243 (*<*) |
265 |
244 lemma accpartI: "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x" |
266 text {* |
245 apply (unfold accpart_def) |
267 Proving the introduction rule is a little more complicated, because the quantifier |
246 apply (rule allI impI)+ |
|
247 (*>*) |
|
248 |
|
249 txt {* |
|
250 |
|
251 Proving the introduction rule is a little more complicated, due to the quantifier |
|
252 and the implication in the premise. We first convert the meta-level universal quantifier |
268 and the implication in the premise. We first convert the meta-level universal quantifier |
253 and implication to their object-level counterparts. Unfolding the definition of |
269 and implication to their object-level counterparts. Unfolding the definition of |
254 @{text accpart} and applying the introduction rules for @{text "\<forall>"} and @{text "\<longrightarrow>"} |
270 @{text accpart} and applying the introduction rules for @{text "\<forall>"} and @{text "\<longrightarrow>"} |
255 yields the following proof state: |
271 yields the following proof state: |
256 @{subgoals [display]} |
272 *} |
|
273 |
|
274 (*<*)lemma accpartI: "(\<forall>y. R y x \<longrightarrow> accpart R y) \<Longrightarrow> accpart R x" |
|
275 apply (unfold accpart_def) |
|
276 apply (rule allI impI)+(*>*) |
|
277 txt {* @{subgoals [display]} *} |
|
278 (*<*)oops(*>*) |
|
279 |
|
280 text {* |
257 Applying the second assumption produces a proof state with the new local assumption |
281 Applying the second assumption produces a proof state with the new local assumption |
258 @{term "R y x"}, which will then be used to solve the goal @{term "P y"} using the |
282 @{term "R y x"}, which will then be used to solve the goal @{term "P y"} using the |
259 first assumption. |
283 first assumption. |
260 *} |
284 *} |
261 (*<*)oops(*>*) |
285 |
262 |
286 lemma %small accpartI: "(\<forall>y. R y x \<longrightarrow> accpart R y) \<Longrightarrow> accpart R x" |
263 lemma accpartI: "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x" |
287 apply (unfold accpart_def) |
264 apply (unfold accpart_def) |
288 apply (rule allI impI)+ |
265 apply (rule allI impI)+ |
289 proof - |
266 proof - |
290 case (goal1 P) |
267 case goal1 |
291 have a1: "\<forall>y. R y x \<longrightarrow> |
268 note goal1' = this |
292 (\<forall>P. (\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> P y)" by fact |
269 show ?case |
293 have a2: "\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x" by fact |
270 apply (rule goal1'(2) [rule_format]) |
294 show "P x" |
271 proof - |
295 apply(rule a2[rule_format]) |
272 case goal1 |
296 proof - |
273 show ?case |
297 case (goal1 y) |
274 apply (rule goal1'(1) [OF goal1, THEN spec [where x=P], |
298 have a3: "R y x" by fact |
275 THEN mp, OF goal1'(2)]) |
299 show "P y" |
276 done |
300 apply(rule a1[THEN spec[where x=y], THEN mp, OF a3, |
277 qed |
301 THEN spec[where x=P], THEN mp, OF a2]) |
278 qed |
302 done |
|
303 qed |
|
304 qed |
|
305 |
|
306 text {* |
|
307 Now the point is to figure out what the automatic proofs should do. For |
|
308 this it might be instructive to look at the general construction principle |
|
309 of inductive definitions, which we shall do next. |
|
310 *} |
279 |
311 |
280 end |
312 end |