1.1 --- a/src/HOL/Finite_Set.thy	Thu Jul 26 15:55:19 2012 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Tue Jul 31 13:55:39 2012 +0200
     1.3 @@ -697,6 +697,18 @@
     1.4    then show ?thesis by simp
     1.5  qed
     1.6  
     1.7 +text{* Other properties of @{const fold}: *}
     1.8 +
     1.9 +lemma fold_image:
    1.10 +  assumes "finite A" and "inj_on g A"
    1.11 +  shows "fold f x (g ` A) = fold (f \<circ> g) x A"
    1.12 +using assms
    1.13 +proof induction
    1.14 +  case (insert a F)
    1.15 +    interpret comp_fun_commute "\<lambda>x. f (g x)" by default (simp add: comp_fun_commute)
    1.16 +    from insert show ?case by auto
    1.17 +qed (simp)
    1.18 +
    1.19  end
    1.20  
    1.21  text{* A simplified version for idempotent functions: *}
    1.22 @@ -777,6 +789,90 @@
    1.23    then show ?thesis ..
    1.24  qed
    1.25  
    1.26 +definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" 
    1.27 +  where "filter P A = fold (\<lambda>x A'. if P x then Set.insert x A' else A') {} A"
    1.28 +
    1.29 +lemma comp_fun_commute_filter_fold: "comp_fun_commute (\<lambda>x A'. if P x then Set.insert x A' else A')"
    1.30 +proof - 
    1.31 +  interpret comp_fun_idem Set.insert by (fact comp_fun_idem_insert)
    1.32 +  show ?thesis by default (auto simp: fun_eq_iff)
    1.33 +qed
    1.34 +
    1.35 +lemma inter_filter:     
    1.36 +  assumes "finite B"
    1.37 +  shows "A \<inter> B = filter (\<lambda>x. x \<in> A) B"
    1.38 +using assms 
    1.39 +by (induct B) (auto simp: filter_def comp_fun_commute.fold_insert[OF comp_fun_commute_filter_fold])
    1.40 +
    1.41 +lemma project_filter:
    1.42 +  assumes "finite A"
    1.43 +  shows "Set.project P A = filter P A"
    1.44 +using assms
    1.45 +by (induct A) 
    1.46 +  (auto simp add: filter_def project_def comp_fun_commute.fold_insert[OF comp_fun_commute_filter_fold])
    1.47 +
    1.48 +lemma image_fold_insert:
    1.49 +  assumes "finite A"
    1.50 +  shows "image f A = fold (\<lambda>k A. Set.insert (f k) A) {} A"
    1.51 +using assms
    1.52 +proof -
    1.53 +  interpret comp_fun_commute "\<lambda>k A. Set.insert (f k) A" by default auto
    1.54 +  show ?thesis using assms by (induct A) auto
    1.55 +qed
    1.56 +
    1.57 +lemma Ball_fold:
    1.58 +  assumes "finite A"
    1.59 +  shows "Ball A P = fold (\<lambda>k s. s \<and> P k) True A"
    1.60 +using assms
    1.61 +proof -
    1.62 +  interpret comp_fun_commute "\<lambda>k s. s \<and> P k" by default auto
    1.63 +  show ?thesis using assms by (induct A) auto
    1.64 +qed
    1.65 +
    1.66 +lemma Bex_fold:
    1.67 +  assumes "finite A"
    1.68 +  shows "Bex A P = fold (\<lambda>k s. s \<or> P k) False A"
    1.69 +using assms
    1.70 +proof -
    1.71 +  interpret comp_fun_commute "\<lambda>k s. s \<or> P k" by default auto
    1.72 +  show ?thesis using assms by (induct A) auto
    1.73 +qed
    1.74 +
    1.75 +lemma comp_fun_commute_Pow_fold: 
    1.76 +  "comp_fun_commute (\<lambda>x A. A \<union> Set.insert x ` A)" 
    1.77 +  by (clarsimp simp: fun_eq_iff comp_fun_commute_def) blast
    1.78 +
    1.79 +lemma Pow_fold:
    1.80 +  assumes "finite A"
    1.81 +  shows "Pow A = fold (\<lambda>x A. A \<union> Set.insert x ` A) {{}} A"
    1.82 +using assms
    1.83 +proof -
    1.84 +  interpret comp_fun_commute "\<lambda>x A. A \<union> Set.insert x ` A" by (rule comp_fun_commute_Pow_fold)
    1.85 +  show ?thesis using assms by (induct A) (auto simp: Pow_insert)
    1.86 +qed
    1.87 +
    1.88 +lemma fold_union_pair:
    1.89 +  assumes "finite B"
    1.90 +  shows "(\<Union>y\<in>B. {(x, y)}) \<union> A = fold (\<lambda>y. Set.insert (x, y)) A B"
    1.91 +proof -
    1.92 +  interpret comp_fun_commute "\<lambda>y. Set.insert (x, y)" by default auto
    1.93 +  show ?thesis using assms  by (induct B arbitrary: A) simp_all
    1.94 +qed
    1.95 +
    1.96 +lemma comp_fun_commute_product_fold: 
    1.97 +  assumes "finite B"
    1.98 +  shows "comp_fun_commute (\<lambda>x A. fold (\<lambda>y. Set.insert (x, y)) A B)" 
    1.99 +by default (auto simp: fold_union_pair[symmetric] assms)
   1.100 +
   1.101 +lemma product_fold:
   1.102 +  assumes "finite A"
   1.103 +  assumes "finite B"
   1.104 +  shows "A \<times> B = fold (\<lambda>x A. fold (\<lambda>y. Set.insert (x, y)) A B) {} A"
   1.105 +using assms unfolding Sigma_def 
   1.106 +by (induct A) 
   1.107 +  (simp_all add: comp_fun_commute.fold_insert[OF comp_fun_commute_product_fold] fold_union_pair)
   1.108 +
   1.109 +
   1.110  context complete_lattice
   1.111  begin
   1.112  
   1.113 @@ -2303,6 +2399,6 @@
   1.114      by simp
   1.115  qed
   1.116  
   1.117 -hide_const (open) Finite_Set.fold
   1.118 +hide_const (open) Finite_Set.fold Finite_Set.filter
   1.119  
   1.120  end

     2.1 --- a/src/HOL/List.thy	Thu Jul 26 15:55:19 2012 +0200
     2.2 +++ b/src/HOL/List.thy	Tue Jul 31 13:55:39 2012 +0200
     2.3 @@ -2458,6 +2458,28 @@
     2.4    "Finite_Set.fold f y (set xs) = fold f (remdups xs) y"
     2.5    by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm insert_absorb)
     2.6  
     2.7 +lemma (in ab_semigroup_mult) fold1_distinct_set_fold:
     2.8 +  assumes "xs \<noteq> []"
     2.9 +  assumes d: "distinct xs"
    2.10 +  shows "Finite_Set.fold1 times (set xs) = List.fold times (tl xs) (hd xs)"
    2.11 +proof -
    2.12 +  interpret comp_fun_commute times by (fact comp_fun_commute)
    2.13 +  from assms obtain y ys where xs: "xs = y # ys"
    2.14 +    by (cases xs) auto
    2.15 +  then have *: "y \<notin> set ys" using assms by simp
    2.16 +  from xs d have **: "remdups ys = ys"  by safe (induct ys, auto)
    2.17 +  show ?thesis
    2.18 +  proof (cases "set ys = {}")
    2.19 +    case True with xs show ?thesis by simp
    2.20 +  next
    2.21 +    case False
    2.22 +    then have "fold1 times (Set.insert y (set ys)) = Finite_Set.fold times y (set ys)"
    2.23 +      by (simp_all add: fold1_eq_fold *)
    2.24 +    with xs show ?thesis
    2.25 +      by (simp add: fold_set_fold_remdups **)
    2.26 +  qed
    2.27 +qed
    2.28 +
    2.29  lemma (in comp_fun_idem) fold_set_fold:
    2.30    "Finite_Set.fold f y (set xs) = fold f xs y"
    2.31    by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm)