Assume that p is a map defined as nat ⇒ string list
or nat ⇀ string list
and I want to append all string list in p's image
As the similar question, if p is a map defined as nat ⇒ string set
or nat ⇀ string set
and I want to union all string list in p's image.
For example, for p: 0 -> ["0.0"]; 1 -> ["1.0","1,1"]
, I want to get the result as ["0.0", "1.0", "1.1"]
for p: 0 -> {"0.0"}; 1 -> {"1.0","1,1"}
, I want to get the result as {"0.0", "1.0", "1.1"}
It seems that in Isabelle has ⋃
to deal with the set union, but I can't find anything about append a set of lists.
p: 0 -> ["0.0"]; 1 -> ["1.0","1,1"]
. What do you want to have? "0.01.01.1"?p: 0 -> ["0.0"]; 1 -> ["1.0","1,1"]
, I want to get the result as["0.0", "1.0", "1.1"]
p: _ -> ["0"]
).fold (@) (map (the o p) (sorted_list_of_set (dom p))) []
might work, but (i) it will be annoying to work with, (ii) it is not executable, and (iii) it will be very very annoying to work with (sledgehammer won't like, auto won't like it, and so on). I strongly advise against, unless really required.