1.1 --- a/src/HOL/Finite_Set.thy	Fri May 20 11:44:34 2011 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Fri May 20 12:07:17 2011 +0200
     1.3 @@ -779,36 +779,34 @@
     1.4  
     1.5  lemma inf_INFI_fold_inf:
     1.6    assumes "finite A"
     1.7 -  shows "inf B (INFI A f) = fold (\<lambda>A. inf (f A)) B A" (is "?inf = ?fold") 
     1.8 +  shows "inf B (INFI A f) = fold (inf \<circ> f) B A" (is "?inf = ?fold") 
     1.9  proof (rule sym)
    1.10    interpret comp_fun_idem inf by (fact comp_fun_idem_inf)
    1.11    interpret comp_fun_idem "inf \<circ> f" by (fact comp_comp_fun_idem)
    1.12 -  from `finite A` have "fold (inf \<circ> f) B A = ?inf"
    1.13 +  from `finite A` show "?fold = ?inf"
    1.14      by (induct A arbitrary: B)
    1.15        (simp_all add: INFI_def Inf_insert inf_left_commute)
    1.16 -  then show "?fold = ?inf" by (simp add: comp_def)
    1.17  qed
    1.18  
    1.19  lemma sup_SUPR_fold_sup:
    1.20    assumes "finite A"
    1.21 -  shows "sup B (SUPR A f) = fold (\<lambda>A. sup (f A)) B A" (is "?sup = ?fold") 
    1.22 +  shows "sup B (SUPR A f) = fold (sup \<circ> f) B A" (is "?sup = ?fold") 
    1.23  proof (rule sym)
    1.24    interpret comp_fun_idem sup by (fact comp_fun_idem_sup)
    1.25    interpret comp_fun_idem "sup \<circ> f" by (fact comp_comp_fun_idem)
    1.26 -  from `finite A` have "fold (sup \<circ> f) B A = ?sup"
    1.27 +  from `finite A` show "?fold = ?sup"
    1.28      by (induct A arbitrary: B)
    1.29        (simp_all add: SUPR_def Sup_insert sup_left_commute)
    1.30 -  then show "?fold = ?sup" by (simp add: comp_def)
    1.31  qed
    1.32  
    1.33  lemma INFI_fold_inf:
    1.34    assumes "finite A"
    1.35 -  shows "INFI A f = fold (\<lambda>A. inf (f A)) top A"
    1.36 +  shows "INFI A f = fold (inf \<circ> f) top A"
    1.37    using assms inf_INFI_fold_inf [of A top] by simp
    1.38  
    1.39  lemma SUPR_fold_sup:
    1.40    assumes "finite A"
    1.41 -  shows "SUPR A f = fold (\<lambda>A. sup (f A)) bot A"
    1.42 +  shows "SUPR A f = fold (sup \<circ> f) bot A"
    1.43    using assms sup_SUPR_fold_sup [of A bot] by simp
    1.44  
    1.45  end