1.1 --- a/src/HOL/List.thy	Tue Dec 27 09:15:26 2011 +0100
     1.2 +++ b/src/HOL/List.thy	Tue Dec 27 09:15:26 2011 +0100
     1.3 @@ -2536,68 +2536,6 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 -lemma (in lattice) Inf_fin_set_fold [code_unfold]:
     1.8 -  "Inf_fin (set (x # xs)) = foldl inf x xs"
     1.9 -proof -
    1.10 -  interpret ab_semigroup_idem_mult "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.11 -    by (fact ab_semigroup_idem_mult_inf)
    1.12 -  show ?thesis
    1.13 -    by (simp add: Inf_fin_def fold1_set del: set.simps)
    1.14 -qed
    1.15 -
    1.16 -lemma (in lattice) Sup_fin_set_fold [code_unfold]:
    1.17 -  "Sup_fin (set (x # xs)) = foldl sup x xs"
    1.18 -proof -
    1.19 -  interpret ab_semigroup_idem_mult "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.20 -    by (fact ab_semigroup_idem_mult_sup)
    1.21 -  show ?thesis
    1.22 -    by (simp add: Sup_fin_def fold1_set del: set.simps)
    1.23 -qed
    1.24 -
    1.25 -lemma (in linorder) Min_fin_set_fold [code_unfold]:
    1.26 -  "Min (set (x # xs)) = foldl min x xs"
    1.27 -proof -
    1.28 -  interpret ab_semigroup_idem_mult "min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.29 -    by (fact ab_semigroup_idem_mult_min)
    1.30 -  show ?thesis
    1.31 -    by (simp add: Min_def fold1_set del: set.simps)
    1.32 -qed
    1.33 -
    1.34 -lemma (in linorder) Max_fin_set_fold [code_unfold]:
    1.35 -  "Max (set (x # xs)) = foldl max x xs"
    1.36 -proof -
    1.37 -  interpret ab_semigroup_idem_mult "max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.38 -    by (fact ab_semigroup_idem_mult_max)
    1.39 -  show ?thesis
    1.40 -    by (simp add: Max_def fold1_set del: set.simps)
    1.41 -qed
    1.42 -
    1.43 -lemma (in complete_lattice) Inf_set_fold [code_unfold]:
    1.44 -  "Inf (set xs) = foldl inf top xs"
    1.45 -proof -
    1.46 -  interpret comp_fun_idem "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.47 -    by (fact comp_fun_idem_inf)
    1.48 -  show ?thesis by (simp add: Inf_fold_inf fold_set inf_commute)
    1.49 -qed
    1.50 -
    1.51 -lemma (in complete_lattice) Sup_set_fold [code_unfold]:
    1.52 -  "Sup (set xs) = foldl sup bot xs"
    1.53 -proof -
    1.54 -  interpret comp_fun_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.55 -    by (fact comp_fun_idem_sup)
    1.56 -  show ?thesis by (simp add: Sup_fold_sup fold_set sup_commute)
    1.57 -qed
    1.58 -
    1.59 -lemma (in complete_lattice) INFI_set_fold:
    1.60 -  "INFI (set xs) f = foldl (\<lambda>y x. inf (f x) y) top xs"
    1.61 -  unfolding INF_def set_map [symmetric] Inf_set_fold foldl_map
    1.62 -    by (simp add: inf_commute)
    1.63 -
    1.64 -lemma (in complete_lattice) SUPR_set_fold:
    1.65 -  "SUPR (set xs) f = foldl (\<lambda>y x. sup (f x) y) bot xs"
    1.66 -  unfolding SUP_def set_map [symmetric] Sup_set_fold foldl_map
    1.67 -    by (simp add: sup_commute)
    1.68 -
    1.69  
    1.70  subsubsection {* @{text upt} *}
    1.71  

     2.1 --- a/src/HOL/More_List.thy	Tue Dec 27 09:15:26 2011 +0100
     2.2 +++ b/src/HOL/More_List.thy	Tue Dec 27 09:15:26 2011 +0100
     2.3 @@ -8,16 +8,6 @@
     2.4  
     2.5  hide_const (open) Finite_Set.fold
     2.6  
     2.7 -text {* Repairing code generator setup *}
     2.8 -
     2.9 -declare (in lattice) Inf_fin_set_fold [code_unfold del]
    2.10 -declare (in lattice) Sup_fin_set_fold [code_unfold del]
    2.11 -declare (in linorder) Min_fin_set_fold [code_unfold del]
    2.12 -declare (in linorder) Max_fin_set_fold [code_unfold del]
    2.13 -declare (in complete_lattice) Inf_set_fold [code_unfold del]
    2.14 -declare (in complete_lattice) Sup_set_fold [code_unfold del]
    2.15 -
    2.16 -
    2.17  text {* Fold combinator with canonical argument order *}
    2.18  
    2.19  primrec fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
    2.20 @@ -238,7 +228,7 @@
    2.21  proof -
    2.22    interpret comp_fun_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
    2.23      by (fact comp_fun_idem_sup)
    2.24 -  show ?thesis by (simp add: Sup_fold_sup fold_set sup_commute)
    2.25 +  show ?thesis by (simp add: Sup_fold_sup fold_set_fold sup_commute)
    2.26  qed
    2.27  
    2.28  lemma (in complete_lattice) Sup_set_foldr [code_unfold]: