--- 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
--- 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)"
--- 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)"
--- 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>
--- 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