src/HOL/ex/Induction_Schema.thy
 author wenzelm Wed Jun 22 10:09:20 2016 +0200 (2016-06-22) changeset 63343 fb5d8a50c641 parent 62390 842917225d56 permissions -rw-r--r--
bundle lifting_syntax;
```     1 (*  Title:      HOL/ex/Induction_Schema.thy
```
```     2     Author:     Alexander Krauss, TU Muenchen
```
```     3 *)
```
```     4
```
```     5 section \<open>Examples of automatically derived induction rules\<close>
```
```     6
```
```     7 theory Induction_Schema
```
```     8 imports Main
```
```     9 begin
```
```    10
```
```    11 subsection \<open>Some simple induction principles on nat\<close>
```
```    12
```
```    13 lemma nat_standard_induct: (* cf. Nat.thy *)
```
```    14   "\<lbrakk>P 0; \<And>n. P n \<Longrightarrow> P (Suc n)\<rbrakk> \<Longrightarrow> P x"
```
```    15 by induction_schema (pat_completeness, lexicographic_order)
```
```    16
```
```    17 lemma nat_induct2:
```
```    18   "\<lbrakk> P 0; P (Suc 0); \<And>k. P k ==> P (Suc k) ==> P (Suc (Suc k)) \<rbrakk>
```
```    19   \<Longrightarrow> P n"
```
```    20 by induction_schema (pat_completeness, lexicographic_order)
```
```    21
```
```    22 lemma minus_one_induct:
```
```    23   "\<lbrakk>\<And>n::nat. (n \<noteq> 0 \<Longrightarrow> P (n - 1)) \<Longrightarrow> P n\<rbrakk> \<Longrightarrow> P x"
```
```    24 by induction_schema (pat_completeness, lexicographic_order)
```
```    25
```
```    26 theorem diff_induct: (* cf. Nat.thy *)
```
```    27   "(!!x. P x 0) ==> (!!y. P 0 (Suc y)) ==>
```
```    28     (!!x y. P x y ==> P (Suc x) (Suc y)) ==> P m n"
```
```    29 by induction_schema (pat_completeness, lexicographic_order)
```
```    30
```
```    31 lemma list_induct2': (* cf. List.thy *)
```
```    32   "\<lbrakk> P [] [];
```
```    33   \<And>x xs. P (x#xs) [];
```
```    34   \<And>y ys. P [] (y#ys);
```
```    35    \<And>x xs y ys. P xs ys  \<Longrightarrow> P (x#xs) (y#ys) \<rbrakk>
```
```    36  \<Longrightarrow> P xs ys"
```
```    37 by induction_schema (pat_completeness, lexicographic_order)
```
```    38
```
```    39 theorem even_odd_induct:
```
```    40   assumes "R 0"
```
```    41   assumes "Q 0"
```
```    42   assumes "\<And>n. Q n \<Longrightarrow> R (Suc n)"
```
```    43   assumes "\<And>n. R n \<Longrightarrow> Q (Suc n)"
```
```    44   shows "R n" "Q n"
```
```    45   using assms
```
```    46 by induction_schema (pat_completeness+, lexicographic_order)
```
```    47
```
```    48 end
```