# HG changeset patch
# User desharna
# Date 1711391273 -3600
# Node ID d8320c3a43ec2788cfae1108eb2e0ce9411d14c3
# Parent  4f803ae647814ed360f50f6df83bba3cb1fa7cc7
added lemma wf_on_iff_wf

diff -r 4f803ae64781 -r d8320c3a43ec NEWS
--- a/NEWS	Mon Mar 25 19:27:32 2024 +0100
+++ b/NEWS	Mon Mar 25 19:27:53 2024 +0100
@@ -110,7 +110,7 @@
     Lemmas wf_def and wfP_def are explicitly provided for backward
     compatibility but their usage is discouraged. Minor INCOMPATIBILITY.
   - Added wfp as alias for wfP for greater consistency with other predicates
-    such as asymp, transp, or totalp. 
+    such as asymp, transp, or totalp.
   - Added lemmas.
       wellorder.wfp_on_less[simp]
       wfP_iff_ex_minimal
@@ -120,6 +120,7 @@
       wf_on_antimono
       wf_on_antimono_strong
       wf_on_iff_ex_minimal
+      wf_on_iff_wf
       wf_on_induct
       wf_on_subset
       wfp_on_antimono
diff -r 4f803ae64781 -r d8320c3a43ec src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Mon Mar 25 19:27:32 2024 +0100
+++ b/src/HOL/Wellfounded.thy	Mon Mar 25 19:27:53 2024 +0100
@@ -71,6 +71,57 @@
 
 lemmas wfP_induct_rule = wf_induct_rule [to_pred, induct set: wfP]
 
+lemma wf_on_iff_wf: "wf_on A r \<longleftrightarrow> wf {(x, y) \<in> r. x \<in> A \<and> y \<in> A}"
+proof (rule iffI)
+  assume wf: "wf_on A r"
+  show "wf {(x, y) \<in> r. x \<in> A \<and> y \<in> A}"
+    unfolding wf_def
+  proof (intro allI impI ballI)
+    fix P x
+    assume IH: "\<forall>x. (\<forall>y. (y, x) \<in> {(x, y). (x, y) \<in> r \<and> x \<in> A \<and> y \<in> A} \<longrightarrow> P y) \<longrightarrow> P x"
+    show "P x"
+    proof (cases "x \<in> A")
+      case True
+      show ?thesis
+        using wf
+      proof (induction x rule: wf_on_induct)
+        case in_set
+        thus ?case
+          using True .
+      next
+        case (less x)
+        thus ?case
+          by (auto intro: IH[rule_format])
+      qed
+    next
+      case False
+      then show ?thesis
+        by (auto intro: IH[rule_format])
+    qed
+  qed
+next
+  assume wf: "wf {(x, y). (x, y) \<in> r \<and> x \<in> A \<and> y \<in> A}"
+  show "wf_on A r"
+    unfolding wf_on_def
+  proof (intro allI impI ballI)
+    fix P x
+    assume IH: "\<forall>x\<in>A. (\<forall>y\<in>A. (y, x) \<in> r \<longrightarrow> P y) \<longrightarrow> P x" and "x \<in> A"
+    show "P x"
+      using wf \<open>x \<in> A\<close>
+    proof (induction x rule: wf_on_induct)
+      case in_set
+      show ?case
+        by simp
+    next
+      case (less y)
+      hence "\<And>z. (z, y) \<in> r \<Longrightarrow> z \<in> A \<Longrightarrow> P z"
+        by simp
+      thus ?case
+        using IH[rule_format, OF \<open>y \<in> A\<close>] by simp
+    qed
+  qed
+qed
+
 
 subsection \<open>Introduction Rules\<close>