# HG changeset patch
# User desharna
# Date 1711016643 -3600
# Node ID 233d70cad0cf9722e16994191eb183d110e8bdf8
# Parent  4bcf3d5da98bc25379493ae27ea6b3d2f835c2a3
redefined wfP as an abbreviation for "wfp_on UNIV"

diff -r 4bcf3d5da98b -r 233d70cad0cf NEWS
--- a/NEWS	Fri Mar 22 10:38:35 2024 +0100
+++ b/NEWS	Thu Mar 21 11:24:03 2024 +0100
@@ -103,8 +103,10 @@
       tranclp_less_eq[simp]
 
 * Theory "HOL.Wellfounded":
-  - Added definitions wf_on and wfp_on as restricted versions versions of
-    wf and wfP respectively.
+  - Added predicate wf_on as restricted versions versions of wf.
+  - Added predicate wfp_on and redefined wfP to be an abbreviation.
+    Lemma wfP_def is explicitly provided for backward compatibility but its
+    usage is discouraged. Minor INCOMPATIBILITY.
   - Added wfp as alias for wfP for greater consistency with other predicates
     such as asymp, transp, or totalp.
   - Added lemmas.
diff -r 4bcf3d5da98b -r 233d70cad0cf src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Fri Mar 22 10:38:35 2024 +0100
+++ b/src/HOL/Tools/Function/function_core.ML	Thu Mar 21 11:24:03 2024 +0100
@@ -780,7 +780,7 @@
     val inrel_R = Const (\<^const_name>\<open>Fun_Def.in_rel\<close>,
       HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel
 
-    val wfR' = HOLogic.mk_Trueprop (Const (\<^const_name>\<open>Wellfounded.wfP\<close>,
+    val wfR' = HOLogic.mk_Trueprop (Const (\<^const_abbrev>\<open>Wellfounded.wfP\<close>,
       (domT --> domT --> boolT) --> boolT) $ R')
       |> Thm.cterm_of ctxt' (* "wf R'" *)
 
diff -r 4bcf3d5da98b -r 233d70cad0cf src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Fri Mar 22 10:38:35 2024 +0100
+++ b/src/HOL/Wellfounded.thy	Thu Mar 21 11:24:03 2024 +0100
@@ -23,8 +23,8 @@
 definition wfp_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
   "wfp_on A R \<longleftrightarrow> (\<forall>P. (\<forall>x \<in> A. (\<forall>y \<in> A. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> (\<forall>x \<in> A. P x))"
 
-definition wfP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
-  where "wfP r \<longleftrightarrow> wf {(x, y). r x y}"
+abbreviation wfP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+  "wfP \<equiv> wfp_on UNIV"
 
 alias wfp = wfP
 
@@ -37,12 +37,12 @@
 lemma wf_on_UNIV: "wf_on UNIV r \<longleftrightarrow> wf r"
   by (simp add: wf_on_def wf_def)
 
-lemma wfp_on_UNIV: "wfp_on UNIV R \<longleftrightarrow> wfP R"
-  by (simp add: wfp_on_def wfP_def wf_def)
-
 lemma wfp_on_wf_on_eq[pred_set_conv]: "wfp_on A (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> wf_on A r"
   by (simp add: wfp_on_def wf_on_def)
 
+lemma wfP_def: "wfP r \<longleftrightarrow> wf {(x, y). r x y}"
+  unfolding wf_def wfp_on_def by simp
+
 lemma wfP_wf_eq [pred_set_conv]: "wfP (\<lambda>x y. (x, y) \<in> r) = wf r"
   by (simp add: wfP_def)
 
@@ -226,7 +226,7 @@
   using wf_on_iff_ex_minimal[of A, to_pred] by simp
 
 lemma wfP_iff_ex_minimal: "wfP R \<longleftrightarrow> (\<forall>B. B \<noteq> {} \<longrightarrow> (\<exists>z \<in> B. \<forall>y. R y z \<longrightarrow> y \<notin> B))"
-  using wfp_on_iff_ex_minimal[of UNIV, unfolded wfp_on_UNIV, simplified] .
+  using wfp_on_iff_ex_minimal[of UNIV, simplified] .
 
 lemma wfE_min:
   assumes wf: "wf R" and Q: "x \<in> Q"
@@ -875,9 +875,9 @@
 lemmas not_acc_down = not_accp_down [to_set]
 lemmas acc_downwards_aux = accp_downwards_aux [to_set]
 lemmas acc_downwards = accp_downwards [to_set]
-lemmas acc_wfI = accp_wfPI [to_set]
-lemmas acc_wfD = accp_wfPD [to_set]
-lemmas wf_acc_iff = wfP_accp_iff [to_set]
+lemmas acc_wfI = accp_wfPI [to_set, unfolded wf_on_UNIV]
+lemmas acc_wfD = accp_wfPD [to_set, unfolded wf_on_UNIV]
+lemmas wf_acc_iff = wfP_accp_iff [to_set, unfolded wf_on_UNIV]
 lemmas acc_subset = accp_subset [to_set]
 lemmas acc_subset_induct = accp_subset_induct [to_set]