Re: [isabelle-dev] Multiset insert

Hi Bertram, > Will the introduction of add# mean that the induction principle for > multisets will be changed as well? If so, do you have a migration path > for proofs based on the current induction principle? (Currently there > are two cases, {#} and M + {#x#}; note that the singleton multiset >

Re: [isabelle-dev] Multiset insert

> I would also like to point out that for some reason, intersection and union > are #∪ and #∩, whereas all other multiset operations seem to have the # at > the end (e.g. ⊆#). Unless there is some deeper reason for this, I suggest we > change it. Good point. Indeed, I first wrote ∪# in

Re: [isabelle-dev] Multiset insert

I've been using multisets quite a bit myself lately. add# and add1# both sound all right to me. I would also like to point out that for some reason, intersection and union are #∪ and #∩, whereas all other multiset operations seem to have the # at the end (e.g. ⊆#). Unless there is some deeper

Re: [isabelle-dev] Multiset insert

Just an aside: concerning »insert« and »add«, infix syntax would be desirable, e.g. a `insert` X a `add` M similar to Y \union Y N + M which would yield much more readable propositions, esp. wrt. associativity: a `insert` b `insert` X = {a, b} \union X

Re: [isabelle-dev] Multiset insert

>> Tobias 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. To

Re: [isabelle-dev] Multiset insert

On 28/07/2016 10:33, Peter Lammich wrote: On Do, 2016-07-28 at 10:21 +0200, Jasmin Blanchette wrote: Tobias 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

Re: [isabelle-dev] Multiset insert

> On 28.07.2016, at 10:33, Peter Lammich 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

Re: [isabelle-dev] Multiset insert

On Do, 2016-07-28 at 10:21 +0200, Jasmin Blanchette wrote: > Tobias 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

Re: [isabelle-dev] Multiset insert

Tobias wrote: > How about > > definition add_mset :: "'a ⇒ 'a multiset ⇒ 'a multiset" ("add#") where > "add# x M = {#x#} + M" Lovely! Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de

Re: [isabelle-dev] Multiset insert

On 27/07/2016 11:39, Jasmin Blanchette wrote: Tobias wrote: Did we ever discuss the naming issue? "insert_mset" would be the canonical name, but it would make larger expressions hard to read. I'm not so sure "insert_mset" would be the right name. Its set-based terminology might suggest a

Re: [isabelle-dev] Multiset insert

Tobias wrote: > Did we ever discuss the naming issue? "insert_mset" would be the canonical > name, but it would make larger expressions hard to read. I'm not so sure "insert_mset" would be the right name. Its set-based terminology might suggest a definition like insert_mset x M = {#x#} #∪

Re: [isabelle-dev] Multiset insert

No, we keep talking about it (internally), but nobody at TUM has done anything about it. It would be great if you want to take this on. It is potentially tedious because there are many existing uses of multisets. Did we ever discuss the naming issue? "insert_mset" would be the canonical name,

Re: [isabelle-dev] Multiset insert

Sounds logical to me. Larry On 8 Apr 2015, at 08:13, Tobias Nipkow nip...@in.tum.de wrote: Currently the setup in Multiset is geared towards having the 3 basic (non-free) constructors: empty, singleton and union. Although induction already has only two cases (empty and union with

[isabelle-dev] Multiset insert

Currently the setup in Multiset is geared towards having the 3 basic (non-free) constructors: empty, singleton and union. Although induction already has only two cases (empty and union with singleton), it would be nicer to have only two constructors, like for finite sets: empty and insert. In

Re: [isabelle-dev] Multiset insert

The singleton constructor would be retained as an abbreviation for insert_mset _ {#} Maybe even that won't be necessary since there is also explicit enumeration syntax for multisets, AFAIR. Florian -- PGP available: