generalized lemma fold_image thanks to Peter Lammich

--- a/src/HOL/Finite_Set.thy	Tue Apr 02 20:19:38 2013 +0200
+++ b/src/HOL/Finite_Set.thy	Wed Apr 03 10:15:43 2013 +0200
@@ -715,19 +715,52 @@
   then show ?thesis by simp
 qed
 
+end
+
 text{* Other properties of @{const fold}: *}
 
 lemma fold_image:
-  assumes "finite A" and "inj_on g A"
+  assumes "inj_on g A"
   shows "fold f z (g ` A) = fold (f \<circ> g) z A"
-using assms
-proof induction
-  case (insert a F)
-    interpret comp_fun_commute "\<lambda>x. f (g x)" by default (simp add: comp_fun_commute)
-    from insert show ?case by auto
-qed simp
-
-end
+proof (cases "finite A")
+  case False with assms show ?thesis by (auto dest: finite_imageD simp add: fold_def)
+next
+  case True
+  have "fold_graph f z (g ` A) = fold_graph (f \<circ> g) z A"
+  proof
+    fix w
+    show "fold_graph f z (g ` A) w \<longleftrightarrow> fold_graph (f \<circ> g) z A w" (is "?P \<longleftrightarrow> ?Q")
+    proof
+      assume ?P then show ?Q using assms
+      proof (induct "g ` A" w arbitrary: A)
+        case emptyI then show ?case by (auto intro: fold_graph.emptyI)
+      next
+        case (insertI x A r B)
+        from `inj_on g B` `x \<notin> A` `insert x A = image g B` obtain x' A' where
+          "x' \<notin> A'" and [simp]: "B = insert x' A'" "x = g x'" "A = g ` A'"
+          by (rule inj_img_insertE)
+        from insertI.prems have "fold_graph (f o g) z A' r"
+          by (auto intro: insertI.hyps)
+        with `x' \<notin> A'` have "fold_graph (f \<circ> g) z (insert x' A') ((f \<circ> g) x' r)"
+          by (rule fold_graph.insertI)
+        then show ?case by simp
+      qed
+    next
+      assume ?Q then show ?P using assms
+      proof induct
+        case emptyI thus ?case by (auto intro: fold_graph.emptyI)
+      next
+        case (insertI x A r)
+        from `x \<notin> A` insertI.prems have "g x \<notin> g ` A" by auto
+        moreover from insertI have "fold_graph f z (g ` A) r" by simp
+        ultimately have "fold_graph f z (insert (g x) (g ` A)) (f (g x) r)"
+          by (rule fold_graph.insertI)
+        then show ?case by simp
+      qed
+    qed
+  qed
+  with True assms show ?thesis by (auto simp add: fold_def)
+qed
 
 lemma fold_cong:
   assumes "comp_fun_commute f" "comp_fun_commute g"

--- a/src/HOL/Fun.thy	Tue Apr 02 20:19:38 2013 +0200
+++ b/src/HOL/Fun.thy	Wed Apr 03 10:15:43 2013 +0200
@@ -286,6 +286,22 @@
   "inj_on (f' o f) A \<Longrightarrow> inj_on f A"
 by(auto simp add: comp_inj_on inj_on_def)
 
+lemma inj_img_insertE:
+  assumes "inj_on f A"
+  assumes "x \<notin> B" and "insert x B = f ` A"
+  obtains x' A' where "x' \<notin> A'" and "A = insert x' A'"
+    and "x = f x'" and "B = f ` A'" 
+proof -
+  from assms have "x \<in> f ` A" by auto
+  then obtain x' where *: "x' \<in> A" "x = f x'" by auto
+  then have "A = insert x' (A - {x'})" by auto
+  with assms * have "B = f ` (A - {x'})"
+    by (auto dest: inj_on_contraD)
+  have "x' \<notin> A - {x'}" by simp
+  from `x' \<notin> A - {x'}` `A = insert x' (A - {x'})` `x = f x'` `B = image f (A - {x'})`
+  show ?thesis ..
+qed
+
 lemma surj_def: "surj f \<longleftrightarrow> (\<forall>y. \<exists>x. y = f x)"
   by auto