Add flatMap to the set class in the library

frontends/library/stainless/lang/Set.scala

@@ -39,18 +39,30 @@ object Set {
     @extern @pure
     def mapPost1[B](f: A => B)(a: A): Unit = {
       ()
-   }.ensuring { _ =>
+    }.ensuring { _ =>
       !set.contains(a) || map[B](f).contains(f(a))
     }
 
     @extern @pure
     def mapPost2[B](f: A => B)(b: B): A = {
       require(map[B](f).contains(b))
       (??? : A)
-   }.ensuring { (a:A) =>
+    }.ensuring { (a:A) =>
       b == f(a) && set.contains(a)
     }
 
+    @extern @pure
+    def flatMap[B](f: A => Set[B]): Set[B] = {
+      new Set(set.theSet.flatMap(f(_).theSet))
+    }
+
+    @extern @pure
+    def flatMapPost[B](f: A => Set[B])(b: B) = {
+      (??? : A)
+    }.ensuring { _ =>
+      flatMap(f).contains(b) == set.exists(a => f(a).contains(b))
+    }
+
     @extern @pure
     def filter(p: A => Boolean): Set[A] = {
       new Set(set.theSet.filter(p))
@@ -114,4 +126,7 @@ sealed case class Set[T](theSet: scala.collection.immutable.Set[T]) {
 
   def contains(a: T): Boolean = theSet.contains(a)
   def subsetOf(b: Set[T]): Boolean = theSet.subsetOf(b.theSet)
+
+  def exists(p: T => Boolean): Boolean = theSet.exists(p)
+  def forall(p: T => Boolean): Boolean = theSet.forall(p)
 }