# 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 \ j \ P i \ (\n. i \ n \ P n \ P (Suc n)) \ 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"