# HG changeset patch
# User desharna
# Date 1738573499 -3600
# Node ID 361fbb3e21c8323a1207492cf98609a4aea21fa0
# Parent  8fd693bb01c5ed1c4f7ce27469cbcfb2e189f449
added lemma strict_partial_order_wfp_on_finite_set

diff -r 8fd693bb01c5 -r 361fbb3e21c8 NEWS
--- a/NEWS	Sun Feb 02 21:53:08 2025 +0100
+++ b/NEWS	Mon Feb 03 10:04:59 2025 +0100
@@ -302,6 +302,7 @@
       wfP_wf_eq ~> wfp_wf_eq
       wf_acc_iff ~> wf_iff_acc
   - Added lemmas.
+      strict_partial_order_wfp_on_finite_set
       wf_on_antimono_stronger
       wfp_on_antimono_stronger
 
diff -r 8fd693bb01c5 -r 361fbb3e21c8 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Sun Feb 02 21:53:08 2025 +0100
+++ b/src/HOL/Wellfounded.thy	Mon Feb 03 10:04:59 2025 +0100
@@ -307,6 +307,33 @@
 lemmas wfp_eq_minimal = wf_eq_minimal [to_pred]
 
 
+subsubsection \<open>Finite characterization of well-foundedness\<close>
+
+lemma strict_partial_order_wfp_on_finite_set:
+  assumes "transp_on \<X> R" and "asymp_on \<X> R" and "finite \<X>"
+  shows "wfp_on \<X> R"
+  unfolding Wellfounded.wfp_on_iff_ex_minimal
+proof (intro allI impI)
+  fix \<W>
+  assume "\<W> \<subseteq> \<X>" and "\<W> \<noteq> {}"
+
+  have "finite \<W>"
+    using finite_subset[OF \<open>\<W> \<subseteq> \<X>\<close> \<open>finite \<X>\<close>] .
+
+  moreover have "asymp_on \<W> R"
+    using asymp_on_subset[OF \<open>asymp_on \<X> R\<close> \<open>\<W> \<subseteq> \<X>\<close>] .
+
+  moreover have "transp_on \<W> R"
+    using transp_on_subset[OF \<open>transp_on \<X> R\<close> \<open>\<W> \<subseteq> \<X>\<close>] .
+
+  ultimately have "\<exists>m\<in>\<W>. \<forall>x\<in>\<W>. x \<noteq> m \<longrightarrow> \<not> R x m"
+    using \<open>\<W> \<noteq> {}\<close> Finite_Set.bex_min_element[of \<W> R] by iprover
+
+  thus "\<exists>z\<in>\<W>. \<forall>y. R y z \<longrightarrow> y \<notin> \<W>"
+    using asymp_onD[OF \<open>asymp_on \<W> R\<close>] by fast
+qed
+
+
 subsubsection \<open>Antimonotonicity\<close>