Re: [isabelle] converting a multiset to a list

Incidentally, I've defined an inductive relation for folding (inspired by Finite_Set.thy) and am in the process of proving some of the relevant lemmas that make it a function. The multisets defined in isabelle are finite already, so the "finite S" assumption can go away.

Is there anyone else doing what I'm doing? It would be a shame to duplicate work unnecessarily.

Rafal Kolanski.

Tobias Nipkow wrote:
Indeed, you cannot define functions by recursion over finite multisets. Same as for sets. For a general solution of recursion over sets see
Similar combinators for multisets would be welcome.

Concerning using "inv": you can do it, but it will be a bit tedious, although probably not too bad. But a general recursion combinator would be nicer.


Revantha Ramanayake schrieb:
Well, my need is the following:

suppose I have a function "f :: form => nat ". I want to define a function "g :: form multiset => nat" like this:

g {# #} = 0
g ({# a #} + M) = f( {# a #}) + g(M).

Basically I want to 'strip away' the multiset, element by element. Of course I gather that the above definition would not work because a multiset is not defined in terms of constructors i.e. it doesn't have the nice structure.

(this is why I wanted to first convert it to a list. for then I could define the function g above, replacing {# #} with [] etc. )

Using "inv multiset_of" I suppose things would look something like this:

f :: form => nat
g' :: form list => nat
g :: form multiset => nat

g' [] = 0
g' (x#ys) = f(x)+g'(ys)

and g(M) = g'(inv multiset_of M)

This seems to do the trick. Is this what you had in mind? and why do you advise against it?



Tobias Nipkow wrote:

Unless you have very specific and good reasons for doing so, I would advise against this and would recommend to go in the other direction. If you absolutely insist, you can always use "inv multiset_of". Good luck.


Revantha Ramanayake wrote:

Hi, this question concerns multisets as defined in the theory file Multisets in the standard distribution.

It is easy to define the function multiset_of :: " 'a list => 'a multiset " which forms a multiset from a list in the obvious way.

How do I define a function (of type " 'a multiset => 'a list ") that accepts a multiset and returns a list (where each occurrence in the multiset is an occurrence in the list and vice versa) ? I realize that there are many possible output lists. I am interested in obtaining one such list.



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