Re: [isabelle] finite order allows maxima



Note that Min/Max as of course no longer unique for non-linear orders.

Also note that Min/Max are instances of the more general arg_min/arg_max.

There are quite a few missing lemmas for arg_max that do exist for
arg_min, otherwise I would have replied to just use arg_max to the
original question.

Manuel


On 05/10/2020 18:23, Tobias Nipkow wrote:
> Maybe Min/Max (on finite sets) could be defined for arbitrary orders
> instead of just linear orders as currently? Florian?
>
> 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)
>> qed
>>
>>> On 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&amp;data=02%7C01%7Ctraytel%40di.ku.dk%7Cb5d292b5b633419e170208d867784111%7Ca3927f91cda14696af898c9f1ceffa91%7C0%7C0%7C637373113480745757&amp;sdata=bV15%2FPbnqKLKeAz7lm0lITKGKjwbPPRdSSrtwjse9ik%3D&amp;reserved=0
>>>
>>>
>>>
>>
>



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