# 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]: