*To*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] finite order allows maxima*From*: "Bisping, Benjamin" <benjamin.bisping at tu-berlin.de>*Date*: Tue, 6 Oct 2020 09:27:10 +0000*Accept-language*: de-DE, en-US*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>*Thread-index*: AQHWmWF6qd20rnxKY0uKtJnjvv7KN6mKCUCAgAAoLwA=*Thread-topic*: [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. > 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 qedqed > > > >

**Attachment:
smime.p7s**

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

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

- Previous by Date: Re: [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