src/HOL/Nat.thy
 changeset 46351 4a1f743c05b2 parent 46350 a49c89df7c92 child 47108 2a1953f0d20d
equal inserted replaced
46350:a49c89df7c92 46351:4a1f743c05b2
`  1678   using inc_induct[of "k - i" k P, simplified] by blast`
`  1678   using inc_induct[of "k - i" k P, simplified] by blast`
`  1679 `
`  1679 `
`  1680 lemma zero_induct: "P k ==> (!!n. P (Suc n) ==> P n) ==> P 0"`
`  1680 lemma zero_induct: "P k ==> (!!n. P (Suc n) ==> P n) ==> P 0"`
`  1681   using inc_induct[of 0 k P] by blast`
`  1681   using inc_induct[of 0 k P] by blast`
`  1682 `
`  1682 `
`  1683 `
`  1683 text {* Further induction rule similar to @{thm inc_induct} *}`
`       `
`  1684 `
`       `
`  1685 lemma dec_induct[consumes 1, case_names base step]:`
`       `
`  1686   "i \<le> j \<Longrightarrow> P i \<Longrightarrow> (\<And>n. i \<le> n \<Longrightarrow> P n \<Longrightarrow> P (Suc n)) \<Longrightarrow> P j"`
`       `
`  1687   by (induct j arbitrary: i) (auto simp: le_Suc_eq)`
`       `
`  1688 `
`       `
`  1689  `
`  1684 subsection {* The divides relation on @{typ nat} *}`
`  1690 subsection {* The divides relation on @{typ nat} *}`
`  1685 `
`  1691 `
`  1686 lemma dvd_1_left [iff]: "Suc 0 dvd k"`
`  1692 lemma dvd_1_left [iff]: "Suc 0 dvd k"`
`  1687 unfolding dvd_def by simp`
`  1693 unfolding dvd_def by simp`
`  1688 `
`  1694 `