# HG changeset patch # User haftmann # Date 1510425215 0 # Node ID 1e29e2666a158f136671e442647f6c8de52a9041 # Parent 0bb8369d10d6bf016fcfe2a65792e8d402c79f40 more induct rules on nat diff -r 0bb8369d10d6 -r 1e29e2666a15 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Sat Nov 11 19:39:47 2017 +0100 +++ b/src/HOL/Nat.thy Sat Nov 11 18:33:35 2017 +0000 @@ -2087,6 +2087,34 @@ using mult_strict_left_mono [of 1 m n] by simp +text \Induction starting beyond zero\ + +lemma nat_induct_at_least [consumes 1, case_names base Suc]: + "P n" if "n \ m" "P m" "\n. n \ m \ P n \ P (Suc n)" +proof - + define q where "q = n - m" + with \n \ m\ have "n = m + q" + by simp + moreover have "P (m + q)" + by (induction q) (use that in simp_all) + ultimately show "P n" + by simp +qed + +lemma nat_induct_non_zero [consumes 1, case_names 1 Suc]: + "P n" if "n > 0" "P 1" "\n. n > 0 \ P n \ P (Suc n)" +proof - + from \n > 0\ have "n \ 1" + by (cases n) simp_all + moreover note \P 1\ + moreover have "\n. n \ 1 \ P n \ P (Suc n)" + using \\n. n > 0 \ P n \ P (Suc n)\ + by (simp add: Suc_le_eq) + ultimately show "P n" + by (rule nat_induct_at_least) +qed + + text \Specialized induction principles that work "backwards":\ lemma inc_induct [consumes 1, case_names base step]: