[isabelle] Definition of Max on finite sets

Dear all,

let me document one Q&A here, as I'm travelling and stackexchange
doesn't have an offline mode, unlike email.

In a private conversation I had asked:

> > How is "Max {}" defined?  I find the definition of "Max = foldl max" strange anyway, as there is no base-case argument for foldl.

And Makarius answered:

> Note that it is fold1 (fold-one).  It is intended for non-empty finite sets.  So it will do the right thing under that assumption.  Otherwise it is also defined, but it might produce non-sense, or we just don't know about what it produces. 

@Makarius: Thanks for pointing out the difference between "one" and
"ell".  These looked to similar in my font.

I don't fully understand the definition of fold1, but I'm happy to
believe that it works :-)



Christoph Lange, School of Computer Science, University of Birmingham
http://cs.bham.ac.uk/~langec/, Skype duke4701

→ SePublica Workshop @ ESWC 2013.  Montpellier, France, 26-30 May.
  Deadline 4 Mar; http://sepublica.mywikipaper.org
→ Intelligent Computer Mathematics, 7–12 Jul, Bath, UK; Deadline 8 Mar
→ Enabling Domain Experts to use Formalised Reasoning @ AISB 2013
  3–5 April 2013, Exeter, UK.  3 Hands-on Tutorials on Economics

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