# HG changeset patch
# User haftmann
# Date 1259772814 -3600
# Node ID fcb50b497763b1a6aa3f5c15a49023603c505784
# Parent  7ed48b28bb7f3de503651c777ebe93cb7ff9af5e
generalized some lemmas

diff -r 7ed48b28bb7f -r fcb50b497763 src/HOL/Library/Fset.thy
--- a/src/HOL/Library/Fset.thy	Wed Dec 02 17:53:34 2009 +0100
+++ b/src/HOL/Library/Fset.thy	Wed Dec 02 17:53:34 2009 +0100
@@ -210,7 +210,7 @@
     member (foldl (\<lambda>B A. Fset (member B \<inter> A)) (Coset []) (List.map member As))"
     by (rule foldl_apply_inv) simp
   then show "Inter (Set As) = foldl inter (Coset []) As"
-    by (simp add: Inter_set image_set inter inter_def_raw foldl_map)
+    by (simp add: Inf_set_fold image_set inter inter_def_raw foldl_map)
   show "Inter (Coset []) = empty"
     by simp
 qed
@@ -229,7 +229,7 @@
     member (foldl (\<lambda>B A. Fset (member B \<union> A)) empty (List.map member As))"
     by (rule foldl_apply_inv) simp
   then show "Union (Set As) = foldl union empty As"
-    by (simp add: Union_set image_set union_def_raw foldl_map)
+    by (simp add: Sup_set_fold image_set union_def_raw foldl_map)
   show "Union (Coset []) = Coset []"
     by simp
 qed
diff -r 7ed48b28bb7f -r fcb50b497763 src/HOL/Library/List_Set.thy
--- a/src/HOL/Library/List_Set.thy	Wed Dec 02 17:53:34 2009 +0100
+++ b/src/HOL/Library/List_Set.thy	Wed Dec 02 17:53:34 2009 +0100
@@ -85,6 +85,50 @@
   "project P (set xs) = set (filter P xs)"
   by (auto simp add: project_def)
 
+text {* FIXME move the following to @{text Finite_Set.thy} *}
+
+lemma fun_left_comm_idem_inf:
+  "fun_left_comm_idem inf"
+proof
+qed (auto simp add: inf_left_commute)
+
+lemma fun_left_comm_idem_sup:
+  "fun_left_comm_idem sup"
+proof
+qed (auto simp add: sup_left_commute)
+
+lemma inf_Inf_fold_inf:
+  fixes A :: "'a::complete_lattice set"
+  assumes "finite A"
+  shows "inf B (Inf A) = fold inf B A"
+proof -
+  interpret fun_left_comm_idem inf by (fact fun_left_comm_idem_inf)
+  from `finite A` show ?thesis by (induct A arbitrary: B)
+    (simp_all add: top_def [symmetric] Inf_insert inf_commute fold_fun_comm)
+qed
+
+lemma sup_Sup_fold_sup:
+  fixes A :: "'a::complete_lattice set"
+  assumes "finite A"
+  shows "sup B (Sup A) = fold sup B A"
+proof -
+  interpret fun_left_comm_idem sup by (fact fun_left_comm_idem_sup)
+  from `finite A` show ?thesis by (induct A arbitrary: B)
+    (simp_all add: bot_def [symmetric] Sup_insert sup_commute fold_fun_comm)
+qed
+
+lemma Inf_fold_inf:
+  fixes A :: "'a::complete_lattice set"
+  assumes "finite A"
+  shows "Inf A = fold inf top A"
+  using assms inf_Inf_fold_inf [of A top] by (simp add: inf_absorb2)
+
+lemma Sup_fold_sup:
+  fixes A :: "'a::complete_lattice set"
+  assumes "finite A"
+  shows "Sup A = fold sup bot A"
+  using assms sup_Sup_fold_sup [of A bot] by (simp add: sup_absorb2)
+
 
 subsection {* Functorial set operations *}
 
@@ -105,41 +149,13 @@
     by (simp add: minus_fold_remove [of _ A] fold_set)
 qed
 
-lemma Inter_set:
-  "Inter (set As) = foldl (op \<inter>) UNIV As"
-proof -
-  have "fold (op \<inter>) UNIV (set As) = foldl (\<lambda>y x. x \<inter> y) UNIV As"
-    by (rule fun_left_comm_idem.fold_set, unfold_locales, auto)
-  then show ?thesis
-    by (simp only: Inter_fold_inter finite_set Int_commute)
-qed
-
-lemma Union_set:
-  "Union (set As) = foldl (op \<union>) {} As"
-proof -
-  have "fold (op \<union>) {} (set As) = foldl (\<lambda>y x. x \<union> y) {} As"
-    by (rule fun_left_comm_idem.fold_set, unfold_locales, auto)
-  then show ?thesis
-    by (simp only: Union_fold_union finite_set Un_commute)
-qed
+lemma INFI_set_fold: -- "FIXME move to List.thy"
+  "INFI (set xs) f = foldl (\<lambda>y x. inf (f x) y) top xs"
+  unfolding INFI_def image_set Inf_set_fold foldl_map by (simp add: inf_commute)
 
-lemma INTER_set:
-  "INTER (set As) f = foldl (\<lambda>B A. f A \<inter> B) UNIV As"
-proof -
-  have "fold (\<lambda>A. op \<inter> (f A)) UNIV (set As) = foldl (\<lambda>B A. f A \<inter> B) UNIV As"
-    by (rule fun_left_comm_idem.fold_set, unfold_locales, auto)
-  then show ?thesis
-    by (simp only: INTER_fold_inter finite_set)
-qed
-
-lemma UNION_set:
-  "UNION (set As) f = foldl (\<lambda>B A. f A \<union> B) {} As"
-proof -
-  have "fold (\<lambda>A. op \<union> (f A)) {} (set As) = foldl (\<lambda>B A. f A \<union> B) {} As"
-    by (rule fun_left_comm_idem.fold_set, unfold_locales, auto)
-  then show ?thesis
-    by (simp only: UNION_fold_union finite_set)
-qed
+lemma SUPR_set_fold: -- "FIXME move to List.thy"
+  "SUPR (set xs) f = foldl (\<lambda>y x. sup (f x) y) bot xs"
+  unfolding SUPR_def image_set Sup_set_fold foldl_map by (simp add: sup_commute)
 
 
 subsection {* Derived set operations *}