src/HOL/Nat.thy
changeset 46351 4a1f743c05b2
parent 46350 a49c89df7c92
child 47108 2a1953f0d20d
equal deleted 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