Why3 Standard Library index

# Multisets (aka bags)

```theory Bag

use import int.Int

type bag 'a

```

whatever `'a`, the type `bag 'a` is always infinite

```  meta "infinite_type" type bag

```

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)
(* FIXME? nb_occ y (singleton x) = if x = y then 1 else 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_right:
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

```

```  function add (x: 'a) (b: bag 'a) : bag 'a = union (singleton x) b

forall b: bag 'a, x y: 'a.
x = y -> nb_occ y (add x b) = nb_occ y 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_nonneg: forall x: bag 'a. card x >= 0
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

```

arbitrary element

```  function choose (b: bag 'a) : 'a

axiom choose_mem: forall b: bag 'a.
empty_bag <> b -> mem (choose b) b

end
```

Generated by why3doc 0.87.3