# HG changeset patch
# User haftmann
# Date 1748584023 -7200
# Node ID 92afc125f7cde3c3e7f5da032f408e9b8eb74b83
# Parent  cf86e095a439b68c736fbe2e9f8f6e2dcf60a3bf
qualify can_select auxiliary operations

diff -r cf86e095a439 -r 92afc125f7cd NEWS
--- a/NEWS	Thu May 29 14:18:27 2025 +0200
+++ b/NEWS	Fri May 30 07:47:03 2025 +0200
@@ -89,6 +89,9 @@
     const Set.filter
     thm filter_def → Set.filter_eq [simp]
 
+    const [List.]can_select ~> Set.can_select
+    thm can_select_def ~> Set.can_select_iff [simp]
+
 The _def suffix for characteristic theorems is avoided to emphasize that these
 auxiliary operations are candidates for unfolding since they are variants
 of existing logical concepts. The [simp] declarations try to move the attention
diff -r cf86e095a439 -r 92afc125f7cd src/HOL/Enum.thy
--- a/src/HOL/Enum.thy	Thu May 29 14:18:27 2025 +0200
+++ b/src/HOL/Enum.thy	Fri May 30 07:47:03 2025 +0200
@@ -66,7 +66,7 @@
 
 definition card_UNIV :: "'a itself \<Rightarrow> nat"
 where
-  [code del]: "card_UNIV TYPE('a) = card (UNIV :: 'a set)"
+  "card_UNIV TYPE('a) = card (UNIV :: 'a set)"
 
 lemma [code]:
   "card_UNIV TYPE('a :: enum) = card (set (Enum.enum :: 'a list))"
@@ -79,13 +79,13 @@
   by simp
 
 lemma exists1_code [code]: "(\<exists>!x. P x) \<longleftrightarrow> list_ex1 P enum"
-  by (auto simp add: list_ex1_iff enum_UNIV)
+  by (simp add: list_ex1_iff enum_UNIV)
 
 
 subsubsection \<open>An executable choice operator\<close>
 
 definition
-  [code del]: "enum_the = The"
+  "enum_the = The"
 
 lemma [code]:
   "The P = (case filter P enum of [x] \<Rightarrow> x | _ \<Rightarrow> enum_the P)"
diff -r cf86e095a439 -r 92afc125f7cd src/HOL/Library/RBT_Set.thy
--- a/src/HOL/Library/RBT_Set.thy	Thu May 29 14:18:27 2025 +0200
+++ b/src/HOL/Library/RBT_Set.thy	Fri May 30 07:47:03 2025 +0200
@@ -29,7 +29,7 @@
 
 declare [[code drop: Set.empty Set.is_empty uminus_set_inst.uminus_set
   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
+  Set.subset_eq Ball Bex Set.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_on wf_code Min Inf_fin Max Sup_fin
   "(Inf :: 'a set set \<Rightarrow> 'a set)" "(Sup :: 'a set set \<Rightarrow> 'a set)"
diff -r cf86e095a439 -r 92afc125f7cd src/HOL/List.thy
--- a/src/HOL/List.thy	Thu May 29 14:18:27 2025 +0200
+++ b/src/HOL/List.thy	Fri May 30 07:47:03 2025 +0200
@@ -7852,7 +7852,7 @@
 list_ex_iff [code_abbrev]: "list_ex P xs \<longleftrightarrow> Bex (set xs) P"
 
 definition list_ex1 :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
-list_ex1_iff [code_abbrev]: "list_ex1 P xs \<longleftrightarrow> (\<exists>! x. x \<in> set xs \<and> P x)"
+list_ex1_iff [code_abbrev]: "list_ex1 P xs \<longleftrightarrow> Set.can_select P (set xs)"
 
 text \<open>
   Usually you should prefer \<open>\<forall>x\<in>set xs\<close>, \<open>\<exists>x\<in>set xs\<close>
@@ -7913,12 +7913,9 @@
   "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> list_ex f xs = list_ex g ys"
 by (simp add: list_ex_iff)
 
-definition can_select :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" where
-[code_abbrev]: "can_select P A = (\<exists>!x\<in>A. P x)"
-
 lemma can_select_set_list_ex1 [code]:
-  "can_select P (set A) = list_ex1 P A"
-  by (simp add: list_ex1_iff can_select_def)
+  "Set.can_select P (set A) = list_ex1 P A"
+  by (simp add: list_ex1_iff Set.can_select_iff)
 
 
 text \<open>Executable checks for relations on sets\<close>
diff -r cf86e095a439 -r 92afc125f7cd src/HOL/Set.thy
--- a/src/HOL/Set.thy	Thu May 29 14:18:27 2025 +0200
+++ b/src/HOL/Set.thy	Fri May 30 07:47:03 2025 +0200
@@ -1893,6 +1893,9 @@
 qualified definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" \<comment> \<open>only for code generation\<close>
   where filter_eq [code_abbrev, simp]: "filter P A = {a \<in> A. P a}"
 
+qualified definition can_select :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" \<comment> \<open>only for code generation\<close>
+  where can_select_iff [code_abbrev, simp]: "can_select P A = (\<exists>!x\<in>A. P x)"
+
 end
 
 instantiation set :: (equal) equal