Stream: Mirror: Isabelle Users Mailing List

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

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

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

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.

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

Sure.

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.

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

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.

2. 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.

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.

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

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: Jan 04 2025 at 20:18 UTC