From 011af15808be6be8cc169d5a1509e3d4873825e4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?C=C3=A9cile=20Ruet-Cros?= <cecile.ruet-cros@cea.fr>
Date: Wed, 3 Jul 2024 16:11:46 +0200
Subject: [PATCH] [wp] vset cleanup useless lemmas
---
src/plugins/wp/Vset.ml | 2 +-
src/plugins/wp/share/why3/frama_c_wp/vset.mlw | 18 ------------------
2 files changed, 1 insertion(+), 19 deletions(-)
diff --git a/src/plugins/wp/Vset.ml b/src/plugins/wp/Vset.ml
index e172b234d26..3627ecc823e 100644
--- a/src/plugins/wp/Vset.ml
+++ b/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"
diff --git a/src/plugins/wp/share/why3/frama_c_wp/vset.mlw b/src/plugins/wp/share/why3/frama_c_wp/vset.mlw
index cf40bacab61..65e6de7179d 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/vset.mlw
+++ b/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)
--
GitLab