--- a/src/HOL/Finite_Set.thy Wed Dec 25 22:35:29 2013 +0100
+++ b/src/HOL/Finite_Set.thy Thu Dec 26 22:47:49 2013 +0100
@@ -1085,6 +1085,9 @@
assumes comp_fun_commute: "f y \<circ> f x = f x \<circ> f y"
begin
+interpretation comp_fun_commute f
+ by default (insert comp_fun_commute, simp add: fun_eq_iff)
+
definition F :: "'a set \<Rightarrow> 'b"
where
eq_fold: "F A = fold f z A"
@@ -1101,8 +1104,6 @@
assumes "finite A" and "x \<notin> A"
shows "F (insert x A) = f x (F A)"
proof -
- interpret comp_fun_commute f
- by default (insert comp_fun_commute, simp add: fun_eq_iff)
from fold_insert assms
have "fold f z (insert x A) = f x (fold f z A)" by simp
with `finite A` show ?thesis by (simp add: eq_fold fun_eq_iff)
@@ -1134,12 +1135,13 @@
declare insert [simp del]
+interpretation comp_fun_idem f
+ by default (insert comp_fun_commute comp_fun_idem, simp add: fun_eq_iff)
+
lemma insert_idem [simp]:
assumes "finite A"
shows "F (insert x A) = f x (F A)"
proof -
- interpret comp_fun_idem f
- by default (insert comp_fun_commute comp_fun_idem, simp add: fun_eq_iff)
from fold_insert_idem assms
have "fold f z (insert x A) = f x (fold f z A)" by simp
with `finite A` show ?thesis by (simp add: eq_fold fun_eq_iff)