src/HOL/ex/Induction_Schema.thy
author hoelzl
Thu Jan 31 11:31:27 2013 +0100 (2013-01-31)
changeset 50999 3de230ed0547
parent 33471 5aef13872723
child 58889 5b7a9633cfa8
permissions -rw-r--r--
introduce order topology
     1 (*  Title:      HOL/ex/Induction_Schema.thy
     2     Author:     Alexander Krauss, TU Muenchen
     3 *)
     4 
     5 header {* Examples of automatically derived induction rules *}
     6 
     7 theory Induction_Schema
     8 imports Main
     9 begin
    10 
    11 subsection {* Some simple induction principles on nat *}
    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