src/HOL/ex/Induction_Scheme.thy
author haftmann
Wed Mar 12 19:38:14 2008 +0100 (2008-03-12)
changeset 26265 4b63b9e9b10d
parent 25567 5720345ea689
child 27271 ba2a00d35df1
permissions -rw-r--r--
separated Random.thy from Quickcheck.thy
     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