*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Two lemmas about lists constructed from finite sets that I'd like Isabelle to provide*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Thu, 23 May 2013 01:56:47 +0200*In-reply-to*: <519D513A.4040109@gmail.com>*References*: <519CFD75.3050506@gmail.com> <519D3BFD.4090600@in.tum.de> <519D513A.4040109@gmail.com>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.8; rv:17.0) Gecko/20130509 Thunderbird/17.0.6

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 >

**References**:**[isabelle] Two lemmas about lists constructed from finite sets that I'd like Isabelle to provide***From:*Christoph LANGE

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

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

- Previous by Date: Re: [isabelle] Two lemmas about lists constructed from finite sets that I'd like Isabelle to provide
- Next by Date: [isabelle] naming conventions (was "Want to use Rep_Integ or lifting after [quot_del] in Int.thy")
- Previous by Thread: Re: [isabelle] Two lemmas about lists constructed from finite sets that I'd like Isabelle to provide
- Next by Thread: [isabelle] SOME-operator
- Cl-isabelle-users May 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list