# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1732291542 0
# Node ID 53e61087bc6f4f5b3bd568fa58d67c508bbe2c0e
# Parent  e43bff789ac0a165e7e79e27e38ae834c880aa35
Introduced the function some_elem for grabbing an element from a non-empty set, and simplified the theorem the_elem_image_unique

diff -r e43bff789ac0 -r 53e61087bc6f src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Fri Nov 22 14:54:00 2024 +0000
+++ b/src/HOL/Hilbert_Choice.thy	Fri Nov 22 16:05:42 2024 +0000
@@ -147,6 +147,34 @@
 qed
 
 
+subsection \<open>Getting an element of a nonempty set\<close>
+
+definition some_elem :: "'a set \<Rightarrow> 'a"
+  where "some_elem A = (SOME x. x \<in> A)"
+
+lemma some_elem_eq [simp]: "some_elem {x} = x"
+  by (simp add: some_elem_def)
+
+lemma some_elem_nonempty: "A \<noteq> {} \<Longrightarrow> some_elem A \<in> A"
+  unfolding some_elem_def by (auto intro: someI)
+
+lemma is_singleton_some_elem: "is_singleton A \<longleftrightarrow> A = {some_elem A}"
+  by (auto simp: is_singleton_def)
+
+lemma some_elem_image_unique:
+  assumes "A \<noteq> {}"
+    and *: "\<And>y. y \<in> A \<Longrightarrow> f y = a"
+  shows "some_elem (f ` A) = a"
+  unfolding some_elem_def
+proof (rule some1_equality)
+  from \<open>A \<noteq> {}\<close> obtain y where "y \<in> A" by auto
+  with * \<open>y \<in> A\<close> have "a \<in> f ` A" by blast
+  then show "a \<in> f ` A" by auto
+  with * show "\<exists>!x. x \<in> f ` A"
+    by auto
+qed
+
+
 subsection \<open>Function Inverse\<close>
 
 lemma inv_def: "inv f = (\<lambda>y. SOME x. f x = y)"
diff -r e43bff789ac0 -r 53e61087bc6f src/HOL/Set.thy
--- a/src/HOL/Set.thy	Fri Nov 22 14:54:00 2024 +0000
+++ b/src/HOL/Set.thy	Fri Nov 22 16:05:42 2024 +0000
@@ -1834,14 +1834,13 @@
 
 lemma the_elem_image_unique:
   assumes "A \<noteq> {}"
-    and *: "\<And>y. y \<in> A \<Longrightarrow> f y = f x"
-  shows "the_elem (f ` A) = f x"
+    and *: "\<And>y. y \<in> A \<Longrightarrow> f y = a"
+  shows "the_elem (f ` A) = a"
   unfolding the_elem_def
 proof (rule the1_equality)
   from \<open>A \<noteq> {}\<close> obtain y where "y \<in> A" by auto
-  with * have "f x = f y" by simp
-  with \<open>y \<in> A\<close> have "f x \<in> f ` A" by blast
-  with * show "f ` A = {f x}" by auto
+  with * \<open>y \<in> A\<close> have "a \<in> f ` A" by blast
+  with * show "f ` A = {a}" by auto
   then show "\<exists>!x. f ` A = {x}" by auto
 qed