# Re: [isabelle] finite order allows maxima

```Adding these facts to Fnite_Set already would be great!

I also once spent an afternoon trying to figure out how to directly obtain such maxima browsing theorems around Finite_Set, order, Max and wf, because I assumed it would be somewhere in Main/Finite_Set. (And then I gave up and proved the instance I needed by an ugly detour through lists ... https://coupledsim.bbisping.de/isabelle/Finite_Partial_Order.html ) The lemmas you propose look as if they would have saved me the afternoon back then! :)

Kind regards,

Benjamin Bisping

Am Dienstag, den 06.10.2020, 09:03 +0200 schrieb Tobias Nipkow:
> 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)"
> first and derive
> lemma (in order) finite_has_max2: "finite A ⟹ a ∈ A ⟹ ∃ s ∈ A. a ≤ s
> ∧ (∀ b ∈ A. s ≤ b ⟶ s = b)"
> from it in one line. In fact, I wonder if the second one is basic
> enough to go into Main, but probably yes.
> I would add the lemma(s) to Finite_Set using Stepan's proof because
> that way they are added at the earliest point.
> Tobias
> > I have proved it for myself (see below). I wonder whether it can be
> > obtained somehow more directly from Main.
> > Best regards
> > Stepan
> > proof (induct "card {b ∈ A. a < b}" arbitrary: a rule:
> > nat_less_induct)   case 1   have IH: "⋀ x. x ∈ A ⟹ card {b ∈ A. x <
> > b} < card {b ∈ A. a < b} ⟹ ∃s∈A. x ≤ s ∧ (∀b∈A. s ≤ b ⟶ s = b)"
> > by (simp add: "1.hyps" ‹finite A›)   then show ?case   proof (cases
> > "∀b∈A. a ≤ b ⟶ a = b")     assume "∀b∈A. a ≤ b ⟶ a = b"     thus
> > ?thesis       using ‹a ∈ A› by blast   next     assume "¬ (∀b∈A. a
> > ≤ b ⟶ a = b)"     then obtain a' where "a' ∈ A" and "a < a'"
> > using local.antisym_conv1 by blast     have "{b ∈ A. a' < b} ⊂ {b ∈
> > A. a < b}" (is "?Ma' ⊂  ?Ma")     proof-       have "a' ∈ ?Ma" and
> > "a' ∉ ?Ma'" and "⋀ c. c ∈ ?Ma' ⟹ c ∈ ?Ma"         using ‹a < a'›
> > ‹a' ∈ A› by auto       thus "?Ma' ⊂  ?Ma"         by blast     qed
> >     hence card: "card {b ∈ A. a' < b} < card {b ∈ A. a < b}"
> > by (simp add: ‹finite A› psubset_card_mono)     then obtain s where
> > "s ∈ A" "a' ≤ s ∧ (∀b∈A. s ≤ b ⟶ s = b)"       using IH[OF ‹a' ∈ A›
> > card] by blast     hence "a ≤ s ∧ (∀b∈A. s ≤ b ⟶ s = b)"
> > using ‹a < a'› by auto     thus ?thesis       using ‹s ∈ A› by
> > blast   qedqed
> >
>
>
```

Attachment: smime.p7s
Description: S/MIME cryptographic signature

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