[isabelle-dev] NEWS: Revision of Big Operators on sets

[Lars Noschinski]

On 23.03.2013 20:58, Florian Haftmann wrote:
> * Revised devices for recursive definitions over finite sets:
>    - Only one fundamental fold combinator on finite set remains:
>      Finite_Set.fold :: ('a =>  'b =>  'b) =>  'b =>  'a set =>  'b
>      This is now identity on infinite sets.
>    - Locales (»mini packages«) for fundamental definitions with
>      Finite_Set.fold: folding, folding_idem.

Before this revision there we had the lemma Min.in_idem. What replaces 
this lemma?

My first try was making min an instance of folding_idem, but apparently 
the F in folding_idem is separate from the one in Min_def. So, what is 
the intended way to recover this lemma?

     interpret Min: folding_idem "min :: ('a :: {bot,linorder} ⇒ 'a ⇒ 
'a)" bot
       by unfold_locales (simp_all add: fun_eq_iff min_max.inf.left_commute)

   -- Lars