Re: [isabelle] finite order allows maxima

I have now added some lemmas with succinct proofs (avoiding cardinalities) and followed Manuel's suggestions concerning arg_min.
See here:

If anybody has additional suggestions...


On 06/10/2020 11:53, Stepan Holub wrote:
Dear Tobias,

the absence of the simpler lemma is even more surprising. It seems to me moreover 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 be wf, 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 we have 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, I really cannot tell whether adding the lemma is the cleanest solution strategically, although, of course, it would be handy practically.


On 06-Oct-20 11:03 AM, cl-isabelle-users-request at 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
Description: S/MIME Cryptographic Signature

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