# HG changeset patch
# User desharna
# Date 1711216538 -3600
# Node ID 033f90dc441d9699977a5eb860af1392b28678c4
# Parent  f83e9e9a898ec980cd46328f8ed97e461236c1e2
redefined wf as an abbreviation for "wf_on UNIV"

diff -r f83e9e9a898e -r 033f90dc441d NEWS
--- 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
diff -r f83e9e9a898e -r 033f90dc441d src/HOL/Library/Multiset.thy
--- 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>
diff -r f83e9e9a898e -r 033f90dc441d src/HOL/Library/RBT_Set.thy
--- 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) = 
diff -r f83e9e9a898e -r 033f90dc441d src/HOL/Library/old_recdef.ML
--- 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),
diff -r f83e9e9a898e -r 033f90dc441d src/HOL/List.thy
--- 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>
 
diff -r f83e9e9a898e -r 033f90dc441d src/HOL/Nitpick.thy
--- 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>
diff -r f83e9e9a898e -r 033f90dc441d src/HOL/Tools/Function/induction_schema.ML
--- 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
diff -r f83e9e9a898e -r 033f90dc441d src/HOL/Tools/Function/termination.ML
--- 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 *)
diff -r f83e9e9a898e -r 033f90dc441d src/HOL/Tools/Nitpick/nitpick_hol.ML
--- 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
diff -r f83e9e9a898e -r 033f90dc441d src/HOL/Tools/Nunchaku/nunchaku_collect.ML
--- 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;
diff -r f83e9e9a898e -r 033f90dc441d src/HOL/Wellfounded.thy
--- 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