--- a/src/HOL/Set.thy Wed Jul 23 13:22:58 2025 +0200
+++ b/src/HOL/Set.thy Thu Jul 24 16:44:52 2025 +0200
@@ -1825,6 +1825,10 @@
lemma is_singletonE: "is_singleton A \<Longrightarrow> (\<And>x. A = {x} \<Longrightarrow> P) \<Longrightarrow> P"
unfolding is_singleton_def by blast
+lemma is_singleton_iff_ex1:
+ \<open>is_singleton A \<longleftrightarrow> (\<exists>!x. x \<in> A)\<close>
+ by (auto simp add: is_singleton_def)
+
subsubsection \<open>Getting the contents of a singleton set\<close>
@@ -1896,6 +1900,10 @@
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)"
+qualified lemma can_select_iff_is_singleton:
+ \<open>Set.can_select P A \<longleftrightarrow> is_singleton (Set.filter P A)\<close>
+ by (simp add: is_singleton_iff_ex1)
+
end
instantiation set :: (equal) equal