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?

yes

> Here is what I tried unsuccessfully.  I posted in on stackoverflow, as
> it's a proper question.
> 
> http://stackoverflow.com/questions/16702866/defining-an-arg-max-like-function-over-finite-sets-and-proving-some-of-its-pr

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

tobias

> Cheers,
> 
> Christoph
> 




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