[wp] vset cleanup useless lemmas

src/plugins/wp/Vset.ml

@@ -112,7 +112,7 @@ let typecheck_unop (params:tau option list) : tau =
 let typecheck_range (_:tau option list) : tau =
   tau_of_set Logic.Int
 
-let p_member = Lang.extern_p ~library ~bool:"member_bool" ~prop:"member" ()
+let p_member = Lang.extern_p ~library ~bool:"member_bool" ~prop:"mem" ()
 let f_empty = Lang.extern_f ~library "empty"
 let f_union = Lang.extern_f ~library ~typecheck:typecheck_binop "union"
 let f_inter = Lang.extern_f ~library ~typecheck:typecheck_binop "inter"

src/plugins/wp/share/why3/frama_c_wp/vset.mlw

@@ -35,7 +35,6 @@ theory Vset
   (* -------------------------------------------------------------------------- *)
 
   function member_bool 'a (set 'a) : bool
-  predicate member (elt:'a) (s: set 'a) = mem elt s
   predicate eqset (a : set 'a) (b : set 'a) =
     forall x : 'a. (member x a) <-> (member x b)
 
@@ -48,23 +47,6 @@ theory Vset
 
   axiom member_bool : forall x:'a. forall s:set 'a [member_bool x s].
     if member x s then member_bool x s = True else member_bool x s = False
-  lemma member_empty : forall x:'a [member x empty].
-    not (member x empty)
-
-  lemma member_singleton : forall x:'a,y:'a [member x (singleton y)].
-    member x (singleton y) <-> x=y
-
-  lemma member_union : forall x:'a. forall a:set 'a,b:set 'a [member x (union a b)].
-    member x (union a b) <-> (member x a) \/ (member x b)
-
-  lemma member_inter : forall x:'a. forall a:set 'a,b:set 'a [member x (inter a b)].
-    member x (inter a b) <-> (member x a) /\ (member x b)
-
-  lemma union_empty : forall a:set 'a [(union a empty)|(union empty a)].
-    (union a empty) = a /\ (union empty a) = a
-
-  lemma inter_empty : forall a:set 'a [(inter a empty)|(inter empty a)].
-    (inter a empty) = empty /\ (inter empty a) = empty
 
   axiom member_range : forall x:int,a:int,b:int [member x (range a b)].
     member x (range a b) <-> (a <= x /\ x <= b)