|
1 (* Title: HOL/ex/Induction_Scheme.thy |
|
2 ID: $Id$ |
|
3 Author: Alexander Krauss, TU Muenchen |
|
4 *) |
|
5 |
|
6 header {* Examples of automatically derived induction rules *} |
|
7 |
|
8 theory Induction_Scheme |
|
9 imports Main |
|
10 begin |
|
11 |
|
12 subsection {* Some simple induction principles on nat *} |
|
13 |
|
14 lemma nat_standard_induct: (* cf. Nat.thy *) |
|
15 "\<lbrakk>P 0; \<And>n. P n \<Longrightarrow> P (Suc n)\<rbrakk> \<Longrightarrow> P x" |
|
16 by induct_scheme (pat_completeness, lexicographic_order) |
|
17 |
|
18 lemma nat_induct2: (* cf. Nat.thy *) |
|
19 "\<lbrakk> P 0; P (Suc 0); \<And>k. P k ==> P (Suc (Suc k)) \<rbrakk> |
|
20 \<Longrightarrow> P n" |
|
21 by induct_scheme (pat_completeness, lexicographic_order) |
|
22 |
|
23 lemma minus_one_induct: |
|
24 "\<lbrakk>\<And>n::nat. (n \<noteq> 0 \<Longrightarrow> P (n - 1)) \<Longrightarrow> P n\<rbrakk> \<Longrightarrow> P x" |
|
25 by induct_scheme (pat_completeness, lexicographic_order) |
|
26 |
|
27 theorem diff_induct: (* cf. Nat.thy *) |
|
28 "(!!x. P x 0) ==> (!!y. P 0 (Suc y)) ==> |
|
29 (!!x y. P x y ==> P (Suc x) (Suc y)) ==> P m n" |
|
30 by induct_scheme (pat_completeness, lexicographic_order) |
|
31 |
|
32 lemma list_induct2': (* cf. List.thy *) |
|
33 "\<lbrakk> P [] []; |
|
34 \<And>x xs. P (x#xs) []; |
|
35 \<And>y ys. P [] (y#ys); |
|
36 \<And>x xs y ys. P xs ys \<Longrightarrow> P (x#xs) (y#ys) \<rbrakk> |
|
37 \<Longrightarrow> P xs ys" |
|
38 by induct_scheme (pat_completeness, lexicographic_order) |
|
39 |
|
40 theorem even_odd_induct: |
|
41 assumes "R 0" |
|
42 assumes "Q 0" |
|
43 assumes "\<And>n. Q n \<Longrightarrow> R (Suc n)" |
|
44 assumes "\<And>n. R n \<Longrightarrow> Q (Suc n)" |
|
45 shows "R n" "Q n" |
|
46 using assms |
|
47 by induct_scheme (pat_completeness, lexicographic_order) |
|
48 |
|
49 end |