src/HOL/Nat.thy
changeset 46351 4a1f743c05b2
parent 46350 a49c89df7c92
child 47108 2a1953f0d20d
     1.1 --- a/src/HOL/Nat.thy	Sat Jan 28 10:22:46 2012 +0100
     1.2 +++ b/src/HOL/Nat.thy	Sat Jan 28 10:35:52 2012 +0100
     1.3 @@ -1680,7 +1680,13 @@
     1.4  lemma zero_induct: "P k ==> (!!n. P (Suc n) ==> P n) ==> P 0"
     1.5    using inc_induct[of 0 k P] by blast
     1.6  
     1.7 +text {* Further induction rule similar to @{thm inc_induct} *}
     1.8  
     1.9 +lemma dec_induct[consumes 1, case_names base step]:
    1.10 +  "i \<le> j \<Longrightarrow> P i \<Longrightarrow> (\<And>n. i \<le> n \<Longrightarrow> P n \<Longrightarrow> P (Suc n)) \<Longrightarrow> P j"
    1.11 +  by (induct j arbitrary: i) (auto simp: le_Suc_eq)
    1.12 +
    1.13 + 
    1.14  subsection {* The divides relation on @{typ nat} *}
    1.15  
    1.16  lemma dvd_1_left [iff]: "Suc 0 dvd k"