73 and then solve the goal by assumption (Line 8). |
73 and then solve the goal by assumption (Line 8). |
74 |
74 |
75 *} |
75 *} |
76 |
76 |
77 lemma %linenos trcl_induct: |
77 lemma %linenos trcl_induct: |
78 assumes asm: "trcl R x y" |
78 assumes "trcl R x y" |
79 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" |
79 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" |
80 apply(atomize (full)) |
80 apply(atomize (full)) |
81 apply(cut_tac asm) |
81 apply(cut_tac prems) |
82 apply(unfold trcl_def) |
82 apply(unfold trcl_def) |
83 apply(drule spec[where x=P]) |
83 apply(drule spec[where x=P]) |
84 apply(assumption) |
84 apply(assumption) |
85 done |
85 done |
86 |
86 |
210 |
210 |
211 The user will state for this inductive definition the specification: |
211 The user will state for this inductive definition the specification: |
212 *} |
212 *} |
213 |
213 |
214 simple_inductive |
214 simple_inductive |
215 even\<iota> and odd\<iota> |
215 even and odd |
216 where |
216 where |
217 even0: "even\<iota> 0" |
217 even0: "even 0" |
218 | evenS: "odd\<iota> n \<Longrightarrow> even\<iota> (Suc n)" |
218 | evenS: "odd n \<Longrightarrow> even (Suc n)" |
219 | oddS: "even\<iota> n \<Longrightarrow> odd\<iota> (Suc n)" |
219 | oddS: "even n \<Longrightarrow> odd (Suc n)" |
220 |
220 |
221 text {* |
221 text {* |
222 Since the predicates @{term even} and @{term odd} are mutually inductive, each |
222 Since the predicates @{term even} and @{term odd} are mutually inductive, each |
223 corresponding definition must quantify over both predicates (we name them |
223 corresponding definition must quantify over both predicates (we name them |
224 below @{text "P"} and @{text "Q"}). |
224 below @{text "P"} and @{text "Q"}). |
225 *} |
225 *} |
226 |
226 |
227 definition "even \<equiv> |
227 definition "even\<iota> \<equiv> |
228 \<lambda>n. \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) |
228 \<lambda>n. \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) |
229 \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> P n" |
229 \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> P n" |
230 |
230 |
231 definition "odd \<equiv> |
231 definition "odd\<iota> \<equiv> |
232 \<lambda>n. \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) |
232 \<lambda>n. \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) |
233 \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> Q n" |
233 \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> Q n" |
234 |
234 |
235 text {* |
235 text {* |
236 For proving the induction principles, we use exactly the same technique |
236 For proving the induction principles, we use exactly the same technique |
237 as in the transitive closure example, namely: |
237 as in the transitive closure example, namely: |
238 *} |
238 *} |
239 |
239 |
240 lemma even_induct: |
240 lemma even_induct: |
241 assumes asm: "even n" |
241 assumes "even n" |
242 shows "P 0 \<Longrightarrow> |
242 shows "P 0 \<Longrightarrow> |
243 (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n" |
243 (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n" |
244 apply(atomize (full)) |
244 apply(atomize (full)) |
245 apply(cut_tac asm) |
245 apply(cut_tac prems) |
246 apply(unfold even_def) |
246 apply(unfold even_def) |
247 apply(drule spec[where x=P]) |
247 apply(drule spec[where x=P]) |
248 apply(drule spec[where x=Q]) |
248 apply(drule spec[where x=Q]) |
249 apply(assumption) |
249 apply(assumption) |
250 done |
250 done |
261 lemma %linenos evenS: |
261 lemma %linenos evenS: |
262 shows "odd m \<Longrightarrow> even (Suc m)" |
262 shows "odd m \<Longrightarrow> even (Suc m)" |
263 apply (unfold odd_def even_def) |
263 apply (unfold odd_def even_def) |
264 apply (rule allI impI)+ |
264 apply (rule allI impI)+ |
265 proof - |
265 proof - |
266 case (goal1 P) |
266 case (goal1 P Q) |
267 have p1: "\<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) |
267 have p1: "\<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) |
268 \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> Q m" by fact |
268 \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> Q m" by fact |
269 have r1: "P 0" by fact |
269 have r1: "P 0" by fact |
270 have r2: "\<forall>m. Q m \<longrightarrow> P (Suc m)" by fact |
270 have r2: "\<forall>m. Q m \<longrightarrow> P (Suc m)" by fact |
271 have r3: "\<forall>m. P m \<longrightarrow> Q (Suc m)" by fact |
271 have r3: "\<forall>m. P m \<longrightarrow> Q (Suc m)" by fact |
301 text {* |
301 text {* |
302 The proof of the induction principle is again straightforward. |
302 The proof of the induction principle is again straightforward. |
303 *} |
303 *} |
304 |
304 |
305 lemma accpart_induct: |
305 lemma accpart_induct: |
306 assumes asm: "accpart R x" |
306 assumes "accpart R x" |
307 shows "(\<And>x. (\<And>y. R y x \<Longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P x" |
307 shows "(\<And>x. (\<And>y. R y x \<Longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P x" |
308 apply(atomize (full)) |
308 apply(atomize (full)) |
309 apply(cut_tac asm) |
309 apply(cut_tac prems) |
310 apply(unfold accpart_def) |
310 apply(unfold accpart_def) |
311 apply(drule spec[where x=P]) |
311 apply(drule spec[where x=P]) |
312 apply(assumption) |
312 apply(assumption) |
313 done |
313 done |
314 |
314 |