more induct rules on nat
authorhaftmann
Sat Nov 11 18:33:35 2017 +0000 (6 months ago)
changeset 670501e29e2666a15
parent 67049 0bb8369d10d6
child 67051 e7e54a0b9197
more induct rules on nat
src/HOL/Nat.thy
     1.1 --- a/src/HOL/Nat.thy	Sat Nov 11 19:39:47 2017 +0100
     1.2 +++ b/src/HOL/Nat.thy	Sat Nov 11 18:33:35 2017 +0000
     1.3 @@ -2087,6 +2087,34 @@
     1.4    using mult_strict_left_mono [of 1 m n] by simp
     1.5  
     1.6  
     1.7 +text \<open>Induction starting beyond zero\<close>
     1.8 +
     1.9 +lemma nat_induct_at_least [consumes 1, case_names base Suc]:
    1.10 +  "P n" if "n \<ge> m" "P m" "\<And>n. n \<ge> m \<Longrightarrow> P n \<Longrightarrow> P (Suc n)"
    1.11 +proof -
    1.12 +  define q where "q = n - m"
    1.13 +  with \<open>n \<ge> m\<close> have "n = m + q"
    1.14 +    by simp
    1.15 +  moreover have "P (m + q)"
    1.16 +    by (induction q) (use that in simp_all)
    1.17 +  ultimately show "P n"
    1.18 +    by simp
    1.19 +qed
    1.20 +
    1.21 +lemma nat_induct_non_zero [consumes 1, case_names 1 Suc]:
    1.22 +  "P n" if "n > 0" "P 1" "\<And>n. n > 0 \<Longrightarrow> P n \<Longrightarrow> P (Suc n)"
    1.23 +proof -
    1.24 +  from \<open>n > 0\<close> have "n \<ge> 1"
    1.25 +    by (cases n) simp_all
    1.26 +  moreover note \<open>P 1\<close>
    1.27 +  moreover have "\<And>n. n \<ge> 1 \<Longrightarrow> P n \<Longrightarrow> P (Suc n)"
    1.28 +    using \<open>\<And>n. n > 0 \<Longrightarrow> P n \<Longrightarrow> P (Suc n)\<close>
    1.29 +    by (simp add: Suc_le_eq)
    1.30 +  ultimately show "P n"
    1.31 +    by (rule nat_induct_at_least)
    1.32 +qed
    1.33 +
    1.34 +
    1.35  text \<open>Specialized induction principles that work "backwards":\<close>
    1.36  
    1.37  lemma inc_induct [consumes 1, case_names base step]: