--- a/src/HOL/Fun_Def.thy Mon Feb 12 09:30:22 2024 +0000
+++ b/src/HOL/Fun_Def.thy Tue Feb 13 17:18:50 2024 +0000
@@ -304,7 +304,7 @@
done
-subsection \<open>Yet another induction principle on the natural numbers\<close>
+subsection \<open>Yet more induction principles on the natural numbers\<close>
lemma nat_descend_induct [case_names base descend]:
fixes P :: "nat \<Rightarrow> bool"
@@ -313,6 +313,13 @@
shows "P m"
using assms by induction_schema (force intro!: wf_measure [of "\<lambda>k. Suc n - k"])+
+lemma induct_nat_012[case_names 0 1 ge2]:
+ "P 0 \<Longrightarrow> P (Suc 0) \<Longrightarrow> (\<And>n. P n \<Longrightarrow> P (Suc n) \<Longrightarrow> P (Suc (Suc n))) \<Longrightarrow> P n"
+proof (induction_schema, pat_completeness)
+ show "wf (Wellfounded.measure id)"
+ by simp
+qed auto
+
subsection \<open>Tool setup\<close>