--- 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"