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





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


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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