--- 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.
--- 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'" *)
--- 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]