*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*: Mon, 5 Oct 2020 18:23:06 +0200*In-reply-to*: <3B4BFBE9-12C2-4473-A38C-CCB901A2FFA7@di.ku.dk>*References*: <e78e4884-bff9-27fe-2dc0-9dea506e437a@karlin.mff.cuni.cz> <3B4BFBE9-12C2-4473-A38C-CCB901A2FFA7@di.ku.dk>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.14; rv:68.0) Gecko/20100101 Thunderbird/68.12.1

Tobias On 04/10/2020 14:31, Dmitriy Traytel wrote:

Hi Stepan, an alternative is to use the well-foundedness of > restricted to the finite set A. This gives one maximal elements via wf_eq_minimal. Not sure if this qualifies as “more direct”, but at least no explicit induction is needed. Dmitriy lemma (in order) fin_max: assumes "finite A" "a ∈ A" shows "∃s ∈ A. a ≤ s ∧ (∀b ∈ A. s ≤ b ⟶ s = b)" proof - from ‹finite A› have "wf {(x,y). x ∈ A ∧ y ∈ A ∧ x > y}" by (intro finite_acyclic_wf[OF finite_subset[of _ "A × A"]]) (auto intro!: acyclicI_order) with ‹a ∈ A› show ?thesis unfolding wf_eq_minimal using order.trans order.order_iff_strict by (elim allE[of _ "{x ∈ A. a ≤ x}"] allE[of _ a]) (auto 7 0) qedOn 3 Oct 2020, at 10:37, Stepan Holub <holub at karlin.mff.cuni.cz> 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)" 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 -- Tento e-mail byl zkontrolován na viry programem AVG. https://eur02.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.avg.cz%2F&data=02%7C01%7Ctraytel%40di.ku.dk%7Cb5d292b5b633419e170208d867784111%7Ca3927f91cda14696af898c9f1ceffa91%7C0%7C0%7C637373113480745757&sdata=bV15%2FPbnqKLKeAz7lm0lITKGKjwbPPRdSSrtwjse9ik%3D&reserved=0

**Attachment:
smime.p7s**

**Follow-Ups**:**Re: [isabelle] finite order allows maxima***From:*Manuel Eberl

**Re: [isabelle] finite order allows maxima***From:*Florian Haftmann

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

**Re: [isabelle] finite order allows maxima***From:*Dmitriy Traytel

- Previous by Date: [isabelle] Unnecessary assumption in HOL-Analysis.Convex.convex_on_alt
- 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