*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 09:03:19 +0200*In-reply-to*: <e78e4884-bff9-27fe-2dc0-9dea506e437a@karlin.mff.cuni.cz>*References*: <e78e4884-bff9-27fe-2dc0-9dea506e437a@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

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)"

first and derive

Comments, please. Tobias

I have proved it for myself (see below). I wonder whether it can be obtainedsomehow more directly from Main.Best regards Stepan proof (induct "card {b ∈ A. a < b}" arbitrary: a rule: nat_less_induct) case 1have 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

**Attachment:
smime.p7s**

**Follow-Ups**:**Re: [isabelle] finite order allows maxima***From:*Bisping, Benjamin

**Re: [isabelle] finite order allows maxima***From:*Lawrence Paulson

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

- Previous by Date: Re: [isabelle] How to make Eisbach's match functionality available from Isabelle/ML?
- Next by Date: [isabelle] quote in mixfix annotation
- 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