--- a/NEWS Wed Mar 20 20:45:36 2024 +0100
+++ b/NEWS Wed Mar 20 21:13:49 2024 +0100
@@ -108,6 +108,7 @@
- Added wfp as alias for wfP for greater consistency with other predicates
such as asymp, transp, or totalp.
- Added lemmas.
+ wellorder.wfp_on_less[simp]
wfP_iff_ex_minimal
wf_iff_ex_minimal
wf_onE_pf
--- a/src/HOL/Wellfounded.thy Wed Mar 20 20:45:36 2024 +0100
+++ b/src/HOL/Wellfounded.thy Wed Mar 20 21:13:49 2024 +0100
@@ -133,6 +133,25 @@
lemma (in wellorder) wfP_less[simp]: "wfP (<)"
by (simp add: wf wfP_def)
+lemma (in wellorder) wfp_on_less[simp]: "wfp_on A (<)"
+ unfolding wfp_on_def
+proof (intro allI impI ballI)
+ fix P x
+ assume hyps: "\<forall>x\<in>A. (\<forall>y\<in>A. y < x \<longrightarrow> P y) \<longrightarrow> P x"
+ show "x \<in> A \<Longrightarrow> P x"
+ proof (induction x rule: less_induct)
+ case (less x)
+ show ?case
+ proof (rule hyps[rule_format])
+ show "x \<in> A"
+ using \<open>x \<in> A\<close> .
+ next
+ show "\<And>y. y \<in> A \<Longrightarrow> y < x \<Longrightarrow> P y"
+ using less.IH .
+ qed
+ qed
+qed
+
subsection \<open>Basic Results\<close>