[isabelle-dev] Multiset insert

[Jasmin Blanchette]

> On 28.07.2016, at 10:33, Peter Lammich <lammich at in.tum.de> wrote:
> 
>>> How about
>>> 
>>> definition add_mset :: "'a ⇒ 'a multiset ⇒ 'a multiset" ("add#") where
>>> "add# x M = {#x#} + M"
> 
> This, however, may produce confusion with multiset union, which is an
> instance of the plus type classes, i.e., occupying the name
> plus_multiset.

I think that's fair enough, because we operate in a simply typed setting. Logicians and computer scientists frequently use the same symbol for both operations, namely comma, when writing contexts in logical or typing judgments. E.g.

	\Gamma, t : \tau
	\Gamma, \Delta
	t : \tau, \Gamma

Without going quite that far here (nor can we due to the type of +), this shows that two think of "add_mset" and + as "essentially the same thing" is not too far off the mark.

"add1_mset" resp. "add1#" would make things more explicit, but since there's hardly any confusion possible there's also hardly any need to make things explicit.

Jasmin