# HG changeset patch
# User haftmann
# Date 1753368292 -7200
# Node ID 04e7c2566f7ed8b69ad616b70aa77fc0bb0cc7f7
# Parent  bd3685e5f8830d69a154975c479f4edb9285f2ee
moved / rearranged lemma

diff -r bd3685e5f883 -r 04e7c2566f7e src/HOL/Finite_Set.thy
--- 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"
diff -r bd3685e5f883 -r 04e7c2566f7e src/HOL/Set.thy
--- 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