--- a/src/HOL/Finite_Set.thy Wed Jul 23 13:22:58 2025 +0200
+++ b/src/HOL/Finite_Set.thy Thu Jul 24 16:44:52 2025 +0200
@@ -2173,12 +2173,21 @@
obtains x where "A = {x}"
using assms by (auto simp: card_Suc_eq)
-lemma is_singleton_altdef: "is_singleton A \<longleftrightarrow> card A = 1"
- unfolding is_singleton_def
- by (auto elim!: card_1_singletonE is_singletonE simp del: One_nat_def)
-
-lemma card_1_singleton_iff: "card A = Suc 0 \<longleftrightarrow> (\<exists>x. A = {x})"
- by (simp add: card_Suc_eq)
+lemma is_singleton_iff_card_eq_Suc_0 [code]:
+ \<open>is_singleton A \<longleftrightarrow> card A = Suc 0\<close>
+ by (simp add: is_singleton_def card_Suc_eq)
+
+lemma is_singleton_altdef:
+ \<open>is_singleton A \<longleftrightarrow> card A = 1\<close>
+ by (simp add: is_singleton_iff_card_eq_Suc_0)
+
+lemma card_eq_Suc_0_iff_is_singleton:
+ \<open>card A = Suc 0 \<longleftrightarrow> is_singleton A\<close>
+ by (simp add: is_singleton_altdef)
+
+lemma card_1_singleton_iff:
+ \<open>card A = Suc 0 \<longleftrightarrow> (\<exists>x. A = {x})\<close>
+ by (simp add: card_eq_Suc_0_iff_is_singleton is_singleton_def)
lemma card_le_Suc0_iff_eq:
assumes "finite A"
--- 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