How to append all list or union all set in a map's image in Isabelle

166 Views Asked by At

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.

0

There are 0 best solutions below