[isabelle-dev] Multiset insert

Larry Paulson lp15 at cam.ac.uk
Wed Apr 8 11:12:52 CEST 2015


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




More information about the isabelle-dev mailing list