1.1 --- a/src/HOL/Library/Fset.thy	Wed Dec 02 17:53:34 2009 +0100
     1.2 +++ b/src/HOL/Library/Fset.thy	Wed Dec 02 17:53:34 2009 +0100
     1.3 @@ -210,7 +210,7 @@
     1.4      member (foldl (\<lambda>B A. Fset (member B \<inter> A)) (Coset []) (List.map member As))"
     1.5      by (rule foldl_apply_inv) simp
     1.6    then show "Inter (Set As) = foldl inter (Coset []) As"
     1.7 -    by (simp add: Inter_set image_set inter inter_def_raw foldl_map)
     1.8 +    by (simp add: Inf_set_fold image_set inter inter_def_raw foldl_map)
     1.9    show "Inter (Coset []) = empty"
    1.10      by simp
    1.11  qed
    1.12 @@ -229,7 +229,7 @@
    1.13      member (foldl (\<lambda>B A. Fset (member B \<union> A)) empty (List.map member As))"
    1.14      by (rule foldl_apply_inv) simp
    1.15    then show "Union (Set As) = foldl union empty As"
    1.16 -    by (simp add: Union_set image_set union_def_raw foldl_map)
    1.17 +    by (simp add: Sup_set_fold image_set union_def_raw foldl_map)
    1.18    show "Union (Coset []) = Coset []"
    1.19      by simp
    1.20  qed

     2.1 --- a/src/HOL/Library/List_Set.thy	Wed Dec 02 17:53:34 2009 +0100
     2.2 +++ b/src/HOL/Library/List_Set.thy	Wed Dec 02 17:53:34 2009 +0100
     2.3 @@ -85,6 +85,50 @@
     2.4    "project P (set xs) = set (filter P xs)"
     2.5    by (auto simp add: project_def)
     2.6  
     2.7 +text {* FIXME move the following to @{text Finite_Set.thy} *}
     2.8 +
     2.9 +lemma fun_left_comm_idem_inf:
    2.10 +  "fun_left_comm_idem inf"
    2.11 +proof
    2.12 +qed (auto simp add: inf_left_commute)
    2.13 +
    2.14 +lemma fun_left_comm_idem_sup:
    2.15 +  "fun_left_comm_idem sup"
    2.16 +proof
    2.17 +qed (auto simp add: sup_left_commute)
    2.18 +
    2.19 +lemma inf_Inf_fold_inf:
    2.20 +  fixes A :: "'a::complete_lattice set"
    2.21 +  assumes "finite A"
    2.22 +  shows "inf B (Inf A) = fold inf B A"
    2.23 +proof -
    2.24 +  interpret fun_left_comm_idem inf by (fact fun_left_comm_idem_inf)
    2.25 +  from `finite A` show ?thesis by (induct A arbitrary: B)
    2.26 +    (simp_all add: top_def [symmetric] Inf_insert inf_commute fold_fun_comm)
    2.27 +qed
    2.28 +
    2.29 +lemma sup_Sup_fold_sup:
    2.30 +  fixes A :: "'a::complete_lattice set"
    2.31 +  assumes "finite A"
    2.32 +  shows "sup B (Sup A) = fold sup B A"
    2.33 +proof -
    2.34 +  interpret fun_left_comm_idem sup by (fact fun_left_comm_idem_sup)
    2.35 +  from `finite A` show ?thesis by (induct A arbitrary: B)
    2.36 +    (simp_all add: bot_def [symmetric] Sup_insert sup_commute fold_fun_comm)
    2.37 +qed
    2.38 +
    2.39 +lemma Inf_fold_inf:
    2.40 +  fixes A :: "'a::complete_lattice set"
    2.41 +  assumes "finite A"
    2.42 +  shows "Inf A = fold inf top A"
    2.43 +  using assms inf_Inf_fold_inf [of A top] by (simp add: inf_absorb2)
    2.44 +
    2.45 +lemma Sup_fold_sup:
    2.46 +  fixes A :: "'a::complete_lattice set"
    2.47 +  assumes "finite A"
    2.48 +  shows "Sup A = fold sup bot A"
    2.49 +  using assms sup_Sup_fold_sup [of A bot] by (simp add: sup_absorb2)
    2.50 +
    2.51  
    2.52  subsection {* Functorial set operations *}
    2.53  
    2.54 @@ -105,41 +149,13 @@
    2.55      by (simp add: minus_fold_remove [of _ A] fold_set)
    2.56  qed
    2.57  
    2.58 -lemma Inter_set:
    2.59 -  "Inter (set As) = foldl (op \<inter>) UNIV As"
    2.60 -proof -
    2.61 -  have "fold (op \<inter>) UNIV (set As) = foldl (\<lambda>y x. x \<inter> y) UNIV As"
    2.62 -    by (rule fun_left_comm_idem.fold_set, unfold_locales, auto)
    2.63 -  then show ?thesis
    2.64 -    by (simp only: Inter_fold_inter finite_set Int_commute)
    2.65 -qed
    2.66 +lemma INFI_set_fold: -- "FIXME move to List.thy"
    2.67 +  "INFI (set xs) f = foldl (\<lambda>y x. inf (f x) y) top xs"
    2.68 +  unfolding INFI_def image_set Inf_set_fold foldl_map by (simp add: inf_commute)
    2.69  
    2.70 -lemma Union_set:
    2.71 -  "Union (set As) = foldl (op \<union>) {} As"
    2.72 -proof -
    2.73 -  have "fold (op \<union>) {} (set As) = foldl (\<lambda>y x. x \<union> y) {} As"
    2.74 -    by (rule fun_left_comm_idem.fold_set, unfold_locales, auto)
    2.75 -  then show ?thesis
    2.76 -    by (simp only: Union_fold_union finite_set Un_commute)
    2.77 -qed
    2.78 -
    2.79 -lemma INTER_set:
    2.80 -  "INTER (set As) f = foldl (\<lambda>B A. f A \<inter> B) UNIV As"
    2.81 -proof -
    2.82 -  have "fold (\<lambda>A. op \<inter> (f A)) UNIV (set As) = foldl (\<lambda>B A. f A \<inter> B) UNIV As"
    2.83 -    by (rule fun_left_comm_idem.fold_set, unfold_locales, auto)
    2.84 -  then show ?thesis
    2.85 -    by (simp only: INTER_fold_inter finite_set)
    2.86 -qed
    2.87 -
    2.88 -lemma UNION_set:
    2.89 -  "UNION (set As) f = foldl (\<lambda>B A. f A \<union> B) {} As"
    2.90 -proof -
    2.91 -  have "fold (\<lambda>A. op \<union> (f A)) {} (set As) = foldl (\<lambda>B A. f A \<union> B) {} As"
    2.92 -    by (rule fun_left_comm_idem.fold_set, unfold_locales, auto)
    2.93 -  then show ?thesis
    2.94 -    by (simp only: UNION_fold_union finite_set)
    2.95 -qed
    2.96 +lemma SUPR_set_fold: -- "FIXME move to List.thy"
    2.97 +  "SUPR (set xs) f = foldl (\<lambda>y x. sup (f x) y) bot xs"
    2.98 +  unfolding SUPR_def image_set Sup_set_fold foldl_map by (simp add: sup_commute)
    2.99  
   2.100  
   2.101  subsection {* Derived set operations *}