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

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.
http://stackoverflow.com/questions/16702866/defining-an-arg-max-like-function-over-finite-sets-and-proving-some-of-its-pr
Cheers,
Christoph
--
Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec/, Skype duke4701
→ Intelligent Computer Mathematics, 8–12 July, Bath, UK.
Work-in-progress deadline 7 June; http://cicm-conference.org/2013/
→ OpenMath Workshop, 10 July, Bath, UK.
Submission deadline 7 June; http://cicm-conference.org/2013/openmath/

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