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