diff -r 2746dfc9ceae -r abb5e57c92a7 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Feb 27 13:46:42 2024 +0100
+++ b/src/HOL/Finite_Set.thy	Wed Mar 06 10:39:45 2024 +0100
@@ -1032,6 +1032,22 @@
 
 text \<open>Other properties of \<^const>\<open>fold\<close>:\<close>
 
+lemma finite_set_fold_single [simp]: "Finite_Set.fold f z {x} = f x z"
+proof -
+  have "fold_graph f z {x} (f x z)"
+    by (auto intro: fold_graph.intros)
+  moreover
+  {
+    fix X y
+    have "fold_graph f z X y \<Longrightarrow> (X = {} \<longrightarrow> y = z) \<and> (X = {x} \<longrightarrow> y = f x z)"
+      by (induct rule: fold_graph.induct) auto
+  }
+  ultimately have "(THE y. fold_graph f z {x} y) = f x z"
+    by blast
+  thus ?thesis
+    by (simp add: Finite_Set.fold_def)
+qed
+
 lemma fold_graph_image:
   assumes "inj_on g A"
   shows "fold_graph f z (g ` A) = fold_graph (f \<circ> g) z A"