diff -r 9d78b02b5506 -r 1bad08165162 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Jun 26 23:39:28 2018 +0200
+++ b/src/HOL/Finite_Set.thy	Wed Jun 27 10:18:03 2018 +0200
@@ -715,9 +715,45 @@
 
 inductive_cases empty_fold_graphE [elim!]: "fold_graph f z {} x"
 
+lemma fold_graph_closed_lemma:
+  "fold_graph f z A x \<and> x \<in> B"
+  if "fold_graph g z A x"
+    "\<And>a b. a \<in> A \<Longrightarrow> b \<in> B \<Longrightarrow> f a b = g a b"
+    "\<And>a b. a \<in> A \<Longrightarrow> b \<in> B \<Longrightarrow> g a b \<in> B"
+    "z \<in> B"
+  using that(1-3)
+proof (induction rule: fold_graph.induct)
+  case (insertI x A y)
+  have "fold_graph f z A y" "y \<in> B"
+    unfolding atomize_conj
+    by (rule insertI.IH) (auto intro: insertI.prems)
+  then have "g x y \<in> B" and f_eq: "f x y = g x y"
+    by (auto simp: insertI.prems)
+  moreover have "fold_graph f z (insert x A) (f x y)"
+    by (rule fold_graph.insertI; fact)
+  ultimately
+  show ?case
+    by (simp add: f_eq)
+qed (auto intro!: that)
+
+lemma fold_graph_closed_eq:
+  "fold_graph f z A = fold_graph g z A"
+  if "\<And>a b. a \<in> A \<Longrightarrow> b \<in> B \<Longrightarrow> f a b = g a b"
+     "\<And>a b. a \<in> A \<Longrightarrow> b \<in> B \<Longrightarrow> g a b \<in> B"
+     "z \<in> B"
+  using fold_graph_closed_lemma[of f z A _ B g] fold_graph_closed_lemma[of g z A _ B f] that
+  by auto
+
 definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"
   where "fold f z A = (if finite A then (THE y. fold_graph f z A y) else z)"
 
+lemma fold_closed_eq: "fold f z A = fold g z A"
+  if "\<And>a b. a \<in> A \<Longrightarrow> b \<in> B \<Longrightarrow> f a b = g a b"
+     "\<And>a b. a \<in> A \<Longrightarrow> b \<in> B \<Longrightarrow> g a b \<in> B"
+     "z \<in> B"
+  unfolding Finite_Set.fold_def
+  by (subst fold_graph_closed_eq[where B=B and g=g]) (auto simp: that)
+
 text \<open>
   A tempting alternative for the definiens is
   @{term "if finite A then THE y. fold_graph f z A y else e"}.