*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] finite order allows maxima*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Tue, 6 Oct 2020 21:47:00 +0200*In-reply-to*: <586f552a-9cde-befa-ffc4-618b110cee3b@karlin.mff.cuni.cz>*References*: <mailman.13596.1601974990.3984.cl-isabelle-users@lists.cam.ac.uk> <586f552a-9cde-befa-ffc4-618b110cee3b@karlin.mff.cuni.cz>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.14; rv:68.0) Gecko/20100101 Thunderbird/68.12.1

See here: http://isabelle.in.tum.de/repos/isabelle/rev/b037517c815b If anybody has additional suggestions... Tobias On 06/10/2020 11:53, Stepan Holub wrote:

Dear Tobias,the absence of the simpler lemma is even more surprising. It seems to memoreover that the version for minimum is not easily obtained either.Nevertheless, I understood two things, thank to this mailing list:1. Dmitriy pointed out that any acyclic relation on a finite list is known to bewf, whence both maxima and minima are obtained. Which leads much better proof(posted by Dmitriy up the thread) than the mine is.2. Manuel pointed out that arg_max/arg_min can be used. Indeed, for minima wehave ex_min_if_finite in Lattices_Big:lemma "⟦ finite S; S ≠ {} ⟧ ⟹ ∃m∈S. ¬(∃x∈S. x < (m::'a::order))" (a side issue: I do not understand why I cannot get alternative lemma (in order) "⟦ finite S; S ≠ {} ⟧ ⟹ ∃m∈S. ¬(∃x∈S. x < m)" ) while for maxima a similar claim is missing at the moment.Altogether, it seems to me that a lacking synchronization between "order""relation" and possibly "Lattices_Big" is somehow at play here. Therefore, Ireally cannot tellwhether adding the lemma is the cleanest solution strategically, although, ofcourse, it would be handy practically.Stepan On 06-Oct-20 11:03 AM, cl-isabelle-users-request at lists.cam.ac.uk wrote:On 03/10/2020 10:37, Stepan Holub wrote:Dear all, in need (of a particular instance of) the following obvious fact: lemma (in order) fin_max: "finite A ⟹ a ∈ A ⟹ ∃ s ∈ A. a ≤ s ∧ (∀ b ∈ A. s ≤ b ⟶ s = b)"This is a useful theorem and I am happy to add it. However, it seems more modular to prove the simpler lemma (in order) finite_has_max: "finite A ⟹ A ≠ {} ⟹ ∃ s ∈ A. (∀ b ∈ A. s ≤ b ⟶ s = b)"

**Attachment:
smime.p7s**

**References**:**Re: [isabelle] finite order allows maxima***From:*Stepan Holub

- Previous by Date: [isabelle] Questions on locales - structure keyword and local definitions
- Next by Date: [isabelle] Error in Eisbach syntax diagram
- Previous by Thread: Re: [isabelle] finite order allows maxima
- Next by Thread: [isabelle] How to make Eisbach's match functionality available from Isabelle/ML?
- Cl-isabelle-users October 2020 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