*To*: Tobias Nipkow <nipkow at in.tum.de>*Subject*: Re: [isabelle] finite order allows maxima*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Tue, 6 Oct 2020 10:38:22 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <7fb0b6b0-7205-cdd6-91d5-75cc87d2ea83@in.tum.de>*References*: <e78e4884-bff9-27fe-2dc0-9dea506e437a@karlin.mff.cuni.cz> <7fb0b6b0-7205-cdd6-91d5-75cc87d2ea83@in.tum.de>

The names should be “maximal” rather than “max”. The latter would suggest the Max function, which is only meaningful for linear orderings. Larry > On 6 Oct 2020, at 08:03, Tobias Nipkow <nipkow at in.tum.de> 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)" > > 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. > > Comments, please. > > 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 >> qed >> qed >

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

**Re: [isabelle] finite order allows maxima***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] finite order allows maxima
- Next by Date: Re: [isabelle] finite order allows maxima
- Previous by Thread: Re: [isabelle] finite order allows maxima
- Next by Thread: Re: [isabelle] finite order allows maxima
- 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