[isabelle-dev] Multiset insert

[Mathias Fleury]

Hello all,

(Relaunching this nearly-one-and-a-half-years-old thread.)


Before I start working on it, has anyone already done some work towards adding insert_mset?


Thanks,
Mathias

> On 08 Apr 2015, at 11:12, Larry Paulson <lp15 at cam.ac.uk> wrote:
> 
> Sounds logical to me.
> Larry
> 
>> On 8 Apr 2015, at 08:13, Tobias Nipkow <nipkow at 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 singleton), it would be nicer to have only two constructors, like for finite sets: empty and insert. In particular, this often avoids the use of ac_simps for union because representations are more canonical. The singleton constructor would be retained as an abbreviation for "insert_mset _ {#}" but "M + {#x#}" would be simplified to "insert_mset x M", like for sets.
>> 
>> Any views?
>> 
>> Tobias
>> 
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev