Email Gateway (Aug 18 2022 at 11:05): Email Gateway (Aug 18 2022 at 11:05):From: Revantha Ramanayake <revantha@rsise.anu.edu.au>
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.
Cheers,
Revantha.
Email Gateway (Aug 18 2022 at 11:05):From: Tobias Nipkow <nipkow@in.tum.de>
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.
Tobias
Revantha Ramanayake wrote:
Email Gateway (Aug 18 2022 at 11:06):From: Tobias Nipkow <nipkow@in.tum.de>
Indeed, you cannot define functions by recursion over finite multisets.
Same as for sets. For a general solution of recursion over sets see
http://www4.informatik.tu-muenchen.de/~nipkow/pubs/tphols05.html
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.
Tobias
Revantha Ramanayake schrieb:
Email Gateway (Aug 18 2022 at 11:06):From: Revantha Ramanayake <revantha@rsise.anu.edu.au>
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:
Define
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?
cheers,
revantha.
Tobias Nipkow wrote:
Email Gateway (Aug 18 2022 at 11:07):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
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:
Last updated: May 03 2024 at 01:09 UTC