Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Some more polishing of the multiset theory


view this post on Zulip Email Gateway (Feb 13 2021 at 09:51):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,

after the current Isabelle release I want to take up some notes for
things which can still be polished in the multiset theory.

I want to excite feedback especially from those who spent a lot of work
there in recent times (as far as I remember, Jasmin, beside others).

  1. Names not following the *_mset convention
    * Melem → member_mset
    * Mempty → empty_mset

  2. Names of definitions deviating for historic reasons
    * inf_subset_mset → inter_mset
    * sup_subset_mset → union_mset

  3. Names for the multiset ordering
    Names mult1 and mult, in a larger setting, are ambiguous.
    Possible ideas:
    * mult1 → multiset_order_step | Multiset.order_step
    * mult → multiset_order_rel | Multiset.order_rel
    But alternative names must be really convincing to justify such
    a transition.

Cheers,
Florian
signature.asc

view this post on Zulip Email Gateway (Feb 13 2021 at 10:44):

From: Manuel Eberl <eberlm@in.tum.de>
I like the first two and think these are uncontroversial.

I don't really know anything about the multiset ordering so I don't have
any opinions on the third one, but what you propose seems reasonable.

Manuel
smime.p7s

view this post on Zulip Email Gateway (Feb 14 2021 at 17:44):

From: Tobias Nipkow <nipkow@in.tum.de>
On 13/02/2021 10:51, Florian Haftmann wrote:

Hi all,

after the current Isabelle release I want to take up some notes for
things which can still be polished in the multiset theory.

I want to excite feedback especially from those who spent a lot of work
there in recent times (as far as I remember, Jasmin, beside others).

  1. Names not following the *_mset convention
    • Melem → member_mset
    • Mempty → empty_mset

Yes.

  1. Names of definitions deviating for historic reasons
    • inf_subset_mset → inter_mset
    • sup_subset_mset → union_mset

Sure.

  1. Names for the multiset ordering
    Names mult1 and mult, in a larger setting, are ambiguous.
    Possible ideas:
    • mult1 → multiset_order_step | Multiset.order_step
    • mult → multiset_order_rel | Multiset.order_rel
      But alternative names must be really convincing to justify such
      a transition.

I chose the current names and they are clearly bad. Now I would go for
multiset_order and multiset_order_step. But Jasmin and friends may have a more
informed opinion because of their work on extended multiset orders.

Tobias

Cheers,
Florian

smime.p7s

view this post on Zulip Email Gateway (Mar 11 2021 at 10:46):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,

  1. Names not following the *_mset convention
        * Melem → member_mset
        * Mempty → empty_mset

Yes.

  1. Names of definitions deviating for historic reasons
        * inf_subset_mset → inter_mset
        * sup_subset_mset → union_mset

Sure.

these are now done and will be part of the next release.

  1. Names for the multiset ordering
        Names mult1 and mult, in a larger setting, are ambiguous.
        Possible ideas:
        * mult1 → multiset_order_step | Multiset.order_step
        * mult → multiset_order_rel | Multiset.order_rel
        But alternative names must be really convincing to justify such
        a transition.

I chose the current names and they are clearly bad. Now I would go for
multiset_order and multiset_order_step. But Jasmin and friends may have
a more informed opinion because of their work on extended multiset orders.

I'm very happy with multiset_order and multiset_order_step.

Does the silence on Tobias’ proposal so far indicate consent?

Cheers,
Florian
OpenPGP_signature

view this post on Zulip Email Gateway (Mar 11 2021 at 10:50):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
I forgot to mention: I stumbled over theory
Nested_Multisets_Ordinals/Multiset_More.thy which contains a lot of
additional material which experts on multisets could judge whether it
should go to the distribution.

Florian
OpenPGP_signature


Last updated: Sep 25 2021 at 09:17 UTC