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