Re: [isabelle] Two lemmas about lists constructed from finite sets that I'd like Isabelle to provide

Am 23/05/2013 01:14, schrieb Christoph LANGE:
> 2013-05-22 22:43 Tobias Nipkow:
>> Most of the time, converting from sets to lists is a cloogy workaround because
>> of problems defining some function directly on fnite sets.
> Good point – that's what I tried first, but I couldn't figure out how to
> make it work.
>> I recommend to
>> understand and use the appropriate fold combinator on lists instead.
> You mean "on sets", right?


> Here is what I tried unsuccessfully.  I posted in on stackoverflow, as
> it's a proper question.

if you are not desparate for executability, here is a two stage approach: first
get all the indices where the function has its maximum (which you can get via
Max), then select some element from it via SOME. although SOME can be a bit
tricky to reason about, this is a fairly abstract approach. something like

let M = {x. v x = Max(v ` finite domain of v)}
in SOME x. x : M & some tie breaker

where the tie breaker could be something like ALL y : M. t x y


> Cheers,
> Christoph

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.