Commit b483ce86 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

Bags added to the standard library

parent 479621eb
theory Bag
use import int.Int
type bag 'a
(* the most basic operation is the number of occurrences *)
function nb_occ (x: 'a) (b: bag 'a): int
axiom occ_non_negative : forall b: bag 'a, x: 'a. nb_occ x b >= 0
(* equality of bags *)
predicate eq_bag (a b : bag 'a) =
forall x:'a. nb_occ x a = nb_occ x b
axiom bag_extensionality: forall a b : bag 'a. eq_bag a b -> a = b
(* basic constructors of bags *)
function empty_bag : bag 'a
axiom occ_empty : forall x: 'a. nb_occ x empty_bag = 0
lemma is_empty : forall b: bag 'a.
(forall x: 'a. nb_occ x b = 0) -> b = empty_bag
function singleton (x: 'a) : bag 'a
axiom occ_singleton: forall x y: 'a.
(x = y /\ (nb_occ y (singleton x)) = 1) \/
(x <> y /\ (nb_occ y (singleton x)) = 0)
lemma occ_singleton_eq : forall x y: 'a. x = y -> (nb_occ y (singleton x)) = 1
lemma occ_singleton_neq : forall x y: 'a. x <> y -> (nb_occ y (singleton x)) = 0
function union (bag 'a) (bag 'a) : bag 'a
axiom occ_union : forall x: 'a, a b : bag 'a. nb_occ x (union a b) = (nb_occ x a) + (nb_occ x b)
(* union commutative, associative with identity empty_bag *)
lemma Union_comm : forall a b:bag 'a. (union a b) = (union b a)
lemma Union_identity : forall a:bag 'a. (union a empty_bag) = a
lemma Union_assoc : forall a b c:bag 'a.
(union a (union b c)) = (union (union a b) c)
lemma bag_simpl : forall a b c: bag 'a.
(union a b) = (union c b) -> a = c
lemma bag_simpl_left : forall a b c: bag 'a.
(union a b) = (union a c) -> b = c
(* add operation *)
function add (x : 'a) (b: bag 'a) : bag 'a = union (singleton x) b
lemma occ_add_eq : forall b: bag 'a, x y: 'a.
x = y -> nb_occ x (add x b) = (nb_occ x b) + 1
lemma occ_add_neq : forall b: bag 'a, x y: 'a.
x <> y -> nb_occ y (add x b) = (nb_occ y b)
(* cardinality of bags *)
function card (bag 'a) : int
axiom Card_empty : card (empty_bag: bag 'a) = 0
axiom Card_singleton : forall x:'a. card (singleton x) = 1
axiom Card_union: forall x y: bag 'a. card (union x y) = (card x) + (card y)
axiom Card_zero_empty : forall x: bag 'a. card (x) = 0 -> x = empty_bag
(* bag difference *)
use import int.MinMax
function diff (bag 'a) (bag 'a) : bag 'a
axiom Diff_occ: forall b1 b2:bag 'a, x:'a.
nb_occ x (diff b1 b2) = max 0 (nb_occ x b1 - nb_occ x b2)
lemma Diff_empty_right: forall b:bag 'a. diff b empty_bag = b
lemma Diff_empty_left: forall b:bag 'a. diff empty_bag b = empty_bag
lemma Diff_add: forall b:bag 'a, x:'a. diff (add x b) (singleton x) = b
lemma Diff_comm: forall b b1 b2:bag 'a.
diff (diff b b1) b2 = diff (diff b b2) b1
lemma Add_diff: forall b:bag 'a, x:'a.
nb_occ x b > 0 -> add x (diff b (singleton x)) = b
end
(*
Local Variables:
compile-command: "why3ide -I . proofs"
End:
*)
(* Multisets (aka bags) *)
theory Bag
use import int.Int
type bag 'a
(* the most basic operation is the number of occurrences *)
function nb_occ (x: 'a) (b: bag 'a): int
axiom occ_non_negative: forall b: bag 'a, x: 'a. nb_occ x b >= 0
predicate mem (x: 'a) (b: bag 'a) = nb_occ x b > 0
(* equality of bags *)
predicate eq_bag (a b: bag 'a) =
forall x:'a. nb_occ x a = nb_occ x b
axiom bag_extensionality: forall a b: bag 'a. eq_bag a b -> a = b
(* basic constructors of bags *)
function empty_bag: bag 'a
axiom occ_empty: forall x: 'a. nb_occ x empty_bag = 0
lemma is_empty: forall b: bag 'a.
(forall x: 'a. nb_occ x b = 0) -> b = empty_bag
function singleton (x: 'a) : bag 'a
axiom occ_singleton: forall x y: 'a.
(x = y /\ (nb_occ y (singleton x)) = 1) \/
(x <> y /\ (nb_occ y (singleton x)) = 0)
lemma occ_singleton_eq:
forall x y: 'a. x = y -> (nb_occ y (singleton x)) = 1
lemma occ_singleton_neq:
forall x y: 'a. x <> y -> (nb_occ y (singleton x)) = 0
function union (bag 'a) (bag 'a) : bag 'a
axiom occ_union:
forall x: 'a, a b: bag 'a.
nb_occ x (union a b) = nb_occ x a + nb_occ x b
(* union commutative, associative with identity empty_bag *)
lemma Union_comm: forall a b: bag 'a. union a b = union b a
lemma Union_identity: forall a: bag 'a. union a empty_bag = a
lemma Union_assoc:
forall a b c: bag 'a. union a (union b c) = union (union a b) c
lemma bag_simpl:
forall a b c: bag 'a. union a b = union c b -> a = c
lemma bag_simpl_left:
forall a b c: bag 'a. union a b = union a c -> b = c
(* add operation *)
function add (x: 'a) (b: bag 'a) : bag 'a = union (singleton x) b
lemma occ_add_eq:
forall b: bag 'a, x y: 'a.
x = y -> nb_occ x (add x b) = nb_occ x b + 1
lemma occ_add_neq: forall b: bag 'a, x y: 'a.
x <> y -> nb_occ y (add x b) = nb_occ y b
(* cardinality of bags *)
function card (bag 'a): int
axiom Card_empty: card (empty_bag: bag 'a) = 0
axiom Card_zero_empty: forall x: bag 'a. card x = 0 -> x = empty_bag
axiom Card_singleton: forall x:'a. card (singleton x) = 1
axiom Card_union: forall x y: bag 'a. card (union x y) = card x + card y
lemma Card_add: forall x: 'a, b: bag 'a. card (add x b) = 1 + card b
(* bag difference *)
use import int.MinMax
function diff (bag 'a) (bag 'a) : bag 'a
axiom Diff_occ: forall b1 b2: bag 'a, x:'a.
nb_occ x (diff b1 b2) = max 0 (nb_occ x b1 - nb_occ x b2)
lemma Diff_empty_right: forall b: bag 'a. diff b empty_bag = b
lemma Diff_empty_left: forall b: bag 'a. diff empty_bag b = empty_bag
lemma Diff_add: forall b: bag 'a, x:'a. diff (add x b) (singleton x) = b
lemma Diff_comm:
forall b b1 b2: bag 'a. diff (diff b b1) b2 = diff (diff b b2) b1
lemma Add_diff: forall b: bag 'a, x:'a.
mem x b -> add x (diff b (singleton x)) = b
end
(*
Local Variables:
compile-command: "why3ide bag.why"
End:
*)
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