--- a/NEWS Sat Mar 23 07:59:53 2024 +0100
+++ b/NEWS Sat Mar 23 18:55:38 2024 +0100
@@ -103,19 +103,17 @@
tranclp_less_eq[simp]
* Theory "HOL.Wellfounded":
- - 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 predicates wf_on and wfp_on and redefined wfP to be abbreviations.
+ 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
wf_iff_ex_minimal
wf_onE_pf
wf_onI_pf
- wf_on_UNIV
wf_on_antimono
wf_on_antimono_strong
wf_on_iff_ex_minimal
--- a/src/HOL/Library/Multiset.thy Sat Mar 23 07:59:53 2024 +0100
+++ b/src/HOL/Library/Multiset.thy Sat Mar 23 18:55:38 2024 +0100
@@ -3720,8 +3720,8 @@
lemma wfP_less_multiset[simp]:
assumes wfP_less: "wfP ((<) :: ('a :: preorder) \<Rightarrow> 'a \<Rightarrow> bool)"
shows "wfP ((<) :: 'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool)"
- using wfP_multp[OF wfP_less] less_multiset_def
- by (metis wfPUNIVI wfP_induct)
+ unfolding less_multiset_def
+ using wfP_multp[OF wfP_less] .
subsubsection \<open>Strict total-order properties\<close>
--- a/src/HOL/Library/RBT_Set.thy Sat Mar 23 07:59:53 2024 +0100
+++ b/src/HOL/Library/RBT_Set.thy Sat Mar 23 18:55:38 2024 +0100
@@ -31,7 +31,7 @@
Set.member Set.insert Set.remove UNIV Set.filter image
Set.subset_eq Ball Bex can_select Set.union minus_set_inst.minus_set Set.inter
card the_elem Pow sum prod Product_Type.product Id_on
- Image trancl relcomp wf Min Inf_fin Max Sup_fin
+ Image trancl relcomp wf_on wf_code Min Inf_fin Max Sup_fin
"(Inf :: 'a set set \<Rightarrow> 'a set)" "(Sup :: 'a set set \<Rightarrow> 'a set)"
sorted_list_of_set List.map_project List.Bleast]]
@@ -644,9 +644,11 @@
by (simp add: relcomp_fold finite_fold_fold_keys[OF *])
qed
-lemma wf_set [code]:
- "wf (Set t) = acyclic (Set t)"
-by (simp add: wf_iff_acyclic_if_finite)
+lemma wf_set: "wf (Set t) = acyclic (Set t)"
+ by (simp add: wf_iff_acyclic_if_finite)
+
+lemma wf_code_set[code]: "wf_code (Set t) = acyclic (Set t)"
+ unfolding wf_code_def using wf_set .
lemma Min_fin_set_fold [code]:
"Min (Set t) =
--- a/src/HOL/Library/old_recdef.ML Sat Mar 23 07:59:53 2024 +0100
+++ b/src/HOL/Library/old_recdef.ML Sat Mar 23 18:55:38 2024 +0100
@@ -755,7 +755,7 @@
end handle Bind => raise USYN_ERR "dest_relation" "unexpected term structure"
else raise USYN_ERR "dest_relation" "not a boolean term";
-fun is_WFR (Const(\<^const_name>\<open>Wellfounded.wf\<close>,_)$_) = true
+fun is_WFR \<^Const_>\<open>Wellfounded.wf_on _ for \<^Const_>\<open>top_class.top _\<close> _\<close> = true
| is_WFR _ = false;
fun ARB ty = mk_select{Bvar=Free("v",ty),
--- a/src/HOL/List.thy Sat Mar 23 07:59:53 2024 +0100
+++ b/src/HOL/List.thy Sat Mar 23 18:55:38 2024 +0100
@@ -8151,10 +8151,13 @@
"set xys O set yzs = set ([(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
by auto (auto simp add: Bex_def image_def)
-lemma wf_set [code]:
+lemma wf_set:
"wf (set xs) = acyclic (set xs)"
by (simp add: wf_iff_acyclic_if_finite)
+lemma wf_code_set[code]: "wf_code (set xs) = acyclic (set xs)"
+ unfolding wf_code_def using wf_set .
+
subsection \<open>Setup for Lifting/Transfer\<close>
--- a/src/HOL/Nitpick.thy Sat Mar 23 07:59:53 2024 +0100
+++ b/src/HOL/Nitpick.thy Sat Mar 23 18:55:38 2024 +0100
@@ -222,7 +222,7 @@
[(\<^const_name>\<open>card\<close>, \<^const_name>\<open>card'\<close>),
(\<^const_name>\<open>sum\<close>, \<^const_name>\<open>sum'\<close>),
(\<^const_name>\<open>fold_graph\<close>, \<^const_name>\<open>fold_graph'\<close>),
- (\<^const_name>\<open>wf\<close>, \<^const_name>\<open>wf'\<close>),
+ (\<^const_abbrev>\<open>wf\<close>, \<^const_name>\<open>wf'\<close>),
(\<^const_name>\<open>wf_wfrec\<close>, \<^const_name>\<open>wf_wfrec'\<close>),
(\<^const_name>\<open>wfrec\<close>, \<^const_name>\<open>wfrec'\<close>)]
\<close>
--- a/src/HOL/Tools/Function/induction_schema.ML Sat Mar 23 07:59:53 2024 +0100
+++ b/src/HOL/Tools/Function/induction_schema.ML Sat Mar 23 18:55:38 2024 +0100
@@ -140,7 +140,7 @@
end
fun mk_wf R (IndScheme {T, ...}) =
- HOLogic.Trueprop $ (Const (\<^const_name>\<open>wf\<close>, mk_relT T --> HOLogic.boolT) $ R)
+ HOLogic.Trueprop $ (Const (\<^const_abbrev>\<open>wf\<close>, mk_relT T --> HOLogic.boolT) $ R)
fun mk_ineqs R thesisn (IndScheme {T, cases, branches}) =
let
--- a/src/HOL/Tools/Function/termination.ML Sat Mar 23 07:59:53 2024 +0100
+++ b/src/HOL/Tools/Function/termination.ML Sat Mar 23 18:55:38 2024 +0100
@@ -231,12 +231,8 @@
type ttac = data -> int -> tactic
fun TERMINATION ctxt atac tac =
- SUBGOAL (fn (_ $ (Const (\<^const_name>\<open>wf\<close>, wfT) $ rel), i) =>
- let
- val (T, _) = HOLogic.dest_prodT (HOLogic.dest_setT (domain_type wfT))
- in
- tac (create ctxt atac atac T rel) i
- end)
+ SUBGOAL (fn (_ $ \<^Const_>\<open>wf_on T for \<^Const_>\<open>top_class.top _\<close> rel\<close>, i) =>
+ tac (create ctxt atac atac T rel) i)
(* A tactic to convert open to closed termination goals *)
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Mar 23 07:59:53 2024 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Mar 23 18:55:38 2024 +0100
@@ -2120,7 +2120,7 @@
val rel_T = HOLogic.mk_setT (HOLogic.mk_prodT (binders_T, binders_T))
val j = fold Integer.max (map maxidx_of_term intro_ts) 0 + 1
val rel = (("R", j), rel_T)
- val prop = Const (\<^const_name>\<open>wf\<close>, rel_T --> bool_T) $ Var rel ::
+ val prop = Const (\<^const_abbrev>\<open>wf\<close>, rel_T --> bool_T) $ Var rel ::
map (wf_constraint_for_triple rel) triples
|> foldr1 s_conj |> HOLogic.mk_Trueprop
val _ = if debug then
--- a/src/HOL/Tools/Nunchaku/nunchaku_collect.ML Sat Mar 23 07:59:53 2024 +0100
+++ b/src/HOL/Tools/Nunchaku/nunchaku_collect.ML Sat Mar 23 18:55:38 2024 +0100
@@ -754,7 +754,7 @@
val j = fold (Integer.max o maxidx_of_term) intros 0 + 1;
val rel = (("R", j), rel_T);
val prop =
- Const (\<^const_name>\<open>wf\<close>, rel_T --> HOLogic.boolT) $ Var rel ::
+ Const (\<^const_abbrev>\<open>wf\<close>, rel_T --> HOLogic.boolT) $ Var rel ::
map (wf_constraint_for_triple rel) triples
|> foldr1 HOLogic.mk_conj
|> HOLogic.mk_Trueprop;
--- a/src/HOL/Wellfounded.thy Sat Mar 23 07:59:53 2024 +0100
+++ b/src/HOL/Wellfounded.thy Sat Mar 23 18:55:38 2024 +0100
@@ -14,11 +14,11 @@
subsection \<open>Basic Definitions\<close>
-definition wf_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool"
- where "wf_on A r \<longleftrightarrow> (\<forall>P. (\<forall>x \<in> A. (\<forall>y \<in> A. (y, x) \<in> r \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> (\<forall>x \<in> A. P x))"
+definition wf_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool" where
+ "wf_on A r \<longleftrightarrow> (\<forall>P. (\<forall>x \<in> A. (\<forall>y \<in> A. (y, x) \<in> r \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> (\<forall>x \<in> A. P x))"
-definition wf :: "('a \<times> 'a) set \<Rightarrow> bool"
- where "wf r \<longleftrightarrow> (\<forall>P. (\<forall>x. (\<forall>y. (y, x) \<in> r \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> (\<forall>x. P x))"
+abbreviation wf :: "('a \<times> 'a) set \<Rightarrow> bool" where
+ "wf \<equiv> wf_on UNIV"
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))"
@@ -34,17 +34,17 @@
subsection \<open>Equivalence of Definitions\<close>
-lemma wf_on_UNIV: "wf_on UNIV r \<longleftrightarrow> wf r"
- by (simp add: wf_on_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 wf_def: "wf r \<longleftrightarrow> (\<forall>P. (\<forall>x. (\<forall>y. (y, x) \<in> r \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> (\<forall>x. P x))"
+ unfolding wf_on_def by simp
+
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)
+lemma wfP_wf_eq: "wfP (\<lambda>x y. (x, y) \<in> r) = wf r"
+ using wfp_on_wf_on_eq .
subsection \<open>Induction Principles\<close>
@@ -63,7 +63,7 @@
assumes "wf r"
and "\<And>x. \<forall>y. (y, x) \<in> r \<longrightarrow> P y \<Longrightarrow> P x"
shows "P a"
- using assms by (auto simp: wf_on_UNIV intro: wf_on_induct[of UNIV])
+ using assms by (auto intro: wf_on_induct[of UNIV])
lemmas wfP_induct = wf_induct [to_pred]
@@ -175,7 +175,7 @@
qed
lemma wfE_pf: "wf R \<Longrightarrow> A \<subseteq> R `` A \<Longrightarrow> A = {}"
- using wf_onE_pf[of UNIV, unfolded wf_on_UNIV, simplified] .
+ using wf_onE_pf[of UNIV, simplified] .
lemma wf_onI_pf:
assumes "\<And>B. B \<subseteq> A \<Longrightarrow> B \<subseteq> R `` B \<Longrightarrow> B = {}"
@@ -194,7 +194,7 @@
qed
lemma wfI_pf: "(\<And>A. A \<subseteq> R `` A \<Longrightarrow> A = {}) \<Longrightarrow> wf R"
- using wf_onI_pf[of UNIV, unfolded wf_on_UNIV, simplified] .
+ using wf_onI_pf[of UNIV, simplified] .
subsubsection \<open>Minimal-element characterization of well-foundedness\<close>
@@ -220,7 +220,7 @@
qed
lemma wf_iff_ex_minimal: "wf R \<longleftrightarrow> (\<forall>B. B \<noteq> {} \<longrightarrow> (\<exists>z \<in> B. \<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> B))"
- using wf_on_iff_ex_minimal[of UNIV, unfolded wf_on_UNIV, simplified] .
+ using wf_on_iff_ex_minimal[of UNIV, simplified] .
lemma wfp_on_iff_ex_minimal: "wfp_on A R \<longleftrightarrow> (\<forall>B \<subseteq> A. B \<noteq> {} \<longrightarrow> (\<exists>z \<in> B. \<forall>y. R y z \<longrightarrow> y \<notin> B))"
using wf_on_iff_ex_minimal[of A, to_pred] by simp
@@ -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, 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_wfI = accp_wfPI [to_set]
+lemmas acc_wfD = accp_wfPD [to_set]
+lemmas wf_acc_iff = wfP_accp_iff [to_set]
lemmas acc_subset = accp_subset [to_set]
lemmas acc_subset_induct = accp_subset_induct [to_set]
@@ -1186,4 +1186,18 @@
hide_const (open) acc accp
+
+subsection \<open>Code Generation Setup\<close>
+
+text \<open>Code equations with \<^const>\<open>wf\<close> or \<^const>\<open>wfp\<close> on the left-hand side are not supported by the
+code generation module because of the \<^const>\<open>UNIV\<close> hidden behind the abbreviations. To sidestep this
+problem, we provide the following wrapper definitions and use @{attribute code_abbrev} to register
+the definitions with the pre- and post-processors of the code generator.\<close>
+
+definition wf_code :: "('a \<times> 'a) set \<Rightarrow> bool" where
+ [code_abbrev]: "wf_code r \<longleftrightarrow> wf r"
+
+definition wfp_code :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+ [code_abbrev]: "wfp_code R \<longleftrightarrow> wfp R"
+
end