Commit c6eaedc1 authored by François Bobot's avatar François Bobot

add set using arrays

parent 4a0368a9
......@@ -335,6 +335,10 @@ clean::
%: %.mlw bin/whyml.opt
bin/whyml.opt $*.mlw
%: %.why bin/why.opt
bin/why.opt $*.why
%.gui: %.mlw bin/whyide.opt
bin/whyide.opt $*.mlw
......
......@@ -22,7 +22,7 @@ transformation "eliminate_algebraic"
transformation "simplify_formula"
transformation "simplify_trivial_quantification"
transformation "encoding_array"
(* transformation "encoding_array" *)
transformation "encoding_smt"
transformation "encoding_sort"
......
theory Bidule
use import set.SetArray
type a
type s = t a
logic a : s
logic b : s
logic c : s
goal Union : forall s1 s2 : s. forall x : a.
mem x (union s1 s2) -> (mem x s1 or mem x s2)
goal Inter : forall s1 s2 : s. forall x : a.
mem x (inter s1 s2) -> (mem x s1 and mem x s2)
goal Union_inter : forall s1 s2 s3 : s. forall x : a.
equal (inter (union s1 s2) s3) (union (inter s1 s3) (inter s2 s3))
lemma Union_assoc : forall s1 s2 s3 : s. forall x : a.
equal (union (union s1 s2) s3) (union s1 (union s2 s3))
clone algebra.Assoc with type t = s, logic op = union, goal Assoc
clone algebra.AC with type t = s, logic op = union, goal Assoc.Assoc, goal Comm.Comm
end
theory Injective
type a
type v
logic f a : v
logic f_1 v : a
axiom Inj : forall x : a. f_1(f x) = x
goal G1 : forall x y : a. f(x)=f(y) -> x = y
goal G2 : forall y : a. exists x : v. f_1(x)=y
end
theory Surjective
type a
type v
logic f a : v
logic f_1 v : a
clone import Injective with type v = a, type a = v,
logic f = f_1, logic f_1 = f
end
theory Bijective
use import Injective
clone Surjective with namespace . = .
end
\ No newline at end of file
......@@ -71,3 +71,52 @@ theory Fset
end
theory SetArray
use import array.Array as A
use import bool.Bool
type t 'a = A.t 'a bool
logic mem (x:'a) (s:t 'a) = get s x = True
logic empty : t 'a = create_const False
logic is_empty (s : t 'a) = forall x : 'a. not mem x s
goal Empty_def1 : is_empty(empty : t 'a)
logic add (x:'a) (s:t 'a) : t 'a = set s x True
logic remove (x:'a) (s:t 'a) : t 'a = set s x False
logic union (t 'a) (t 'a) : t 'a
axiom Union_def :
forall s1 s2 : t 'a. forall x : 'a.
get (union s1 s2) x = orb (get s1 x) (get s2 x)
logic inter (t 'a) (t 'a) : t 'a
axiom Inter_def :
forall s1 s2 : t 'a. forall x : 'a.
get (inter s1 s2) x = andb (get s1 x) (get s2 x)
logic diff (t 'a) (t 'a) : t 'a
axiom Diff_def1 :
forall s1 s2 : t 'a. forall x : 'a.
get (diff s1 s2) x = xorb (get s1 x) (get s2 x)
logic equal(s1 s2 : t 'a) = forall x : 'a. get s1 x = get s2 x
axiom Equal_is_eq : forall s1 s2 : t 'a. equal s1 s2 -> s1 = s2
logic subset(s1 s2 : t 'a) = forall x : 'a. mem x s1 -> mem x s2
logic complement (t 'a) : t 'a
axiom Complement_def :
forall s : t 'a. forall x : 'a.
get (complement s) x = notb (get s x)
end
\ No newline at end of file
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment