diff -r 6621d91d3c8a -r 240a39af9ec4 src/HOL/Fun_Def.thy
--- a/src/HOL/Fun_Def.thy	Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/Fun_Def.thy	Sat Dec 17 15:22:13 2016 +0100
@@ -278,6 +278,16 @@
   done
 
 
+subsection \<open>Yet another induction principle on the natural numbers\<close>
+
+lemma nat_descend_induct [case_names base descend]:
+  fixes P :: "nat \<Rightarrow> bool"
+  assumes H1: "\<And>k. k > n \<Longrightarrow> P k"
+  assumes H2: "\<And>k. k \<le> n \<Longrightarrow> (\<And>i. i > k \<Longrightarrow> P i) \<Longrightarrow> P k"
+  shows "P m"
+  using assms by induction_schema (force intro!: wf_measure [of "\<lambda>k. Suc n - k"])+
+
+
 subsection \<open>Tool setup\<close>
 
 ML_file "Tools/Function/termination.ML"