# HG changeset patch
# User desharna
# Date 1710965629 -3600
# Node ID 33c9a670e29c15d3a62363c75ae12949415f89c6
# Parent  b5cb8d56339f958e1f129e3705d84050329a31ad
added lemma wellorder.wfp_on_less[simp]

diff -r b5cb8d56339f -r 33c9a670e29c NEWS
--- 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
diff -r b5cb8d56339f -r 33c9a670e29c src/HOL/Wellfounded.thy
--- 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>