# HG changeset patch
# User desharna
# Date 1741107430 -3600
# Node ID 3f70b283bea9882f9e173de5e54b4896d0ff19de
# Parent  aedb93833ea8b0f1bdbdbaf04156d8070f174733
added lemma wfp_on_iff_wfp

diff -r aedb93833ea8 -r 3f70b283bea9 NEWS
--- a/NEWS	Tue Mar 04 16:58:46 2025 +0100
+++ b/NEWS	Tue Mar 04 17:57:10 2025 +0100
@@ -14,6 +14,10 @@
       monotone_on_inf_fun
       monotone_on_sup_fun
 
+* Theory "HOL.Wellfounded":
+  - Added lemmas.
+      wfp_on_iff_wfp
+
 * Theory "HOL-Library.Multiset":
   - Renamed lemmas. Minor INCOMPATIBILITY.
       filter_image_mset ~> filter_mset_image_mset
diff -r aedb93833ea8 -r 3f70b283bea9 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Tue Mar 04 16:58:46 2025 +0100
+++ b/src/HOL/Wellfounded.thy	Tue Mar 04 17:57:10 2025 +0100
@@ -393,6 +393,28 @@
   using wfp_on_antimono_strong .
 
 
+subsubsection \<open>Equivalence between \<^const>\<open>wfp_on\<close> and \<^const>\<open>wfp\<close>\<close>
+
+lemma wfp_on_iff_wfp: "wfp_on A R \<longleftrightarrow> wfp (\<lambda>x y. R x y \<and>  x \<in> A \<and> y \<in> A)"
+  (is "?LHS \<longleftrightarrow> ?RHS")
+proof (rule iffI)
+  assume ?LHS
+  then show ?RHS
+    unfolding wfp_on_iff_ex_minimal
+    by force
+next
+  assume ?RHS
+  thus ?LHS
+  proof (rule wfp_on_antimono_strong)
+    show "A \<subseteq> UNIV"
+      using subset_UNIV .
+  next
+    show "\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> R x y \<Longrightarrow> R x y \<and> x \<in> A \<and> y \<in> A"
+      by iprover
+  qed
+qed
+
+
 subsubsection \<open>Well-foundedness of transitive closure\<close>
 
 lemma ex_terminating_rtranclp_strong: