diff -r b14c4cb37d99 -r 76a1c0ea6777 src/HOL/Fun_Def.thy
--- 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>