# HG changeset patch
# User bulwahn
# Date 1327743352 -3600
# Node ID 4a1f743c05b20196d0747e6e9124b1dcba9ca4b9
# Parent  a49c89df7c924f1299b91448bdb5ae0f5980dc78
adding yet another induction rule on natural numbers

diff -r a49c89df7c92 -r 4a1f743c05b2 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Sat Jan 28 10:22:46 2012 +0100
+++ b/src/HOL/Nat.thy	Sat Jan 28 10:35:52 2012 +0100
@@ -1680,7 +1680,13 @@
 lemma zero_induct: "P k ==> (!!n. P (Suc n) ==> P n) ==> P 0"
   using inc_induct[of 0 k P] by blast
 
+text {* Further induction rule similar to @{thm inc_induct} *}
 
+lemma dec_induct[consumes 1, case_names base step]:
+  "i \<le> j \<Longrightarrow> P i \<Longrightarrow> (\<And>n. i \<le> n \<Longrightarrow> P n \<Longrightarrow> P (Suc n)) \<Longrightarrow> P j"
+  by (induct j arbitrary: i) (auto simp: le_Suc_eq)
+
+ 
 subsection {* The divides relation on @{typ nat} *}
 
 lemma dvd_1_left [iff]: "Suc 0 dvd k"