--- a/src/HOL/List.thy Sat Dec 05 10:18:23 2009 +0100
+++ b/src/HOL/List.thy Sat Dec 05 20:02:21 2009 +0100
@@ -2359,15 +2359,29 @@
lemma (in complete_lattice) Inf_set_fold [code_unfold]:
"Inf (set xs) = foldl inf top xs"
- by (cases xs)
- (simp_all add: Inf_fin_Inf [symmetric] Inf_fin_set_fold
- inf_commute del: set.simps, simp add: top_def)
+proof -
+ interpret fun_left_comm_idem "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
+ by (fact fun_left_comm_idem_inf)
+ show ?thesis by (simp add: Inf_fold_inf fold_set inf_commute)
+qed
lemma (in complete_lattice) Sup_set_fold [code_unfold]:
"Sup (set xs) = foldl sup bot xs"
- by (cases xs)
- (simp_all add: Sup_fin_Sup [symmetric] Sup_fin_set_fold
- sup_commute del: set.simps, simp add: bot_def)
+proof -
+ interpret fun_left_comm_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
+ by (fact fun_left_comm_idem_sup)
+ show ?thesis by (simp add: Sup_fold_sup fold_set sup_commute)
+qed
+
+lemma (in complete_lattice) INFI_set_fold:
+ "INFI (set xs) f = foldl (\<lambda>y x. inf (f x) y) top xs"
+ unfolding INFI_def set_map [symmetric] Inf_set_fold foldl_map
+ by (simp add: inf_commute)
+
+lemma (in complete_lattice) SUPR_set_fold:
+ "SUPR (set xs) f = foldl (\<lambda>y x. sup (f x) y) bot xs"
+ unfolding SUPR_def set_map [symmetric] Sup_set_fold foldl_map
+ by (simp add: sup_commute)
subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}