# HG changeset patch
# User desharna
# Date 1711100315 -3600
# Node ID 4bcf3d5da98bc25379493ae27ea6b3d2f835c2a3
# Parent  26592fe88250d01a11c8b855198518c55f9cbac4# Parent  33c9a670e29c15d3a62363c75ae12949415f89c6
merged

diff -r 26592fe88250 -r 4bcf3d5da98b NEWS
--- a/NEWS	Thu Mar 21 21:04:49 2024 +0100
+++ b/NEWS	Fri Mar 22 10:38:35 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
diff -r 26592fe88250 -r 4bcf3d5da98b src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Thu Mar 21 21:04:49 2024 +0100
+++ b/src/HOL/Wellfounded.thy	Fri Mar 22 10:38:35 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>