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.