1.1 --- a/src/HOL/Finite_Set.thy	Thu Sep 24 18:29:28 2009 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Thu Sep 24 18:29:29 2009 +0200
     1.3 @@ -2615,6 +2615,23 @@
     1.4    finally show ?case .
     1.5  qed
     1.6  
     1.7 +lemma fold1_eq_fold_idem:
     1.8 +  assumes "finite A"
     1.9 +  shows "fold1 times (insert a A) = fold times a A"
    1.10 +proof (cases "a \<in> A")
    1.11 +  case False
    1.12 +  with assms show ?thesis by (simp add: fold1_eq_fold)
    1.13 +next
    1.14 +  interpret fun_left_comm_idem times by (fact fun_left_comm_idem)
    1.15 +  case True then obtain b B
    1.16 +    where A: "A = insert a B" and "a \<notin> B" by (rule set_insert)
    1.17 +  with assms have "finite B" by auto
    1.18 +  then have "fold times a (insert a B) = fold times (a * a) B"
    1.19 +    using `a \<notin> B` by (rule fold_insert2)
    1.20 +  then show ?thesis
    1.21 +    using `a \<notin> B` `finite B` by (simp add: fold1_eq_fold A)
    1.22 +qed
    1.23 +
    1.24  end
    1.25  
    1.26