mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
131 lines
3.3 KiB
Plaintext
131 lines
3.3 KiB
Plaintext
|
|
(** {1 Multisets (aka bags)} *)
|
|
|
|
module Bag
|
|
|
|
use 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 (==) (a b: bag 'a) =
|
|
forall x:'a. nb_occ x a = nb_occ x b
|
|
|
|
axiom bag_extensionality: forall a b: bag 'a. a == b -> a = b
|
|
|
|
meta extensionality predicate (==)
|
|
|
|
(** 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
|
|
|
|
(** union *)
|
|
|
|
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
|
|
|
|
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
|
|
|
|
(** 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 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 *)
|
|
|
|
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
|
|
|
|
(** difference *)
|
|
|
|
use 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
|
|
|
|
(** intersection *)
|
|
|
|
function inter (a b: bag 'a) : bag 'a
|
|
|
|
axiom inter:
|
|
forall x: 'a, a b: bag 'a.
|
|
nb_occ x (inter a b) = min (nb_occ x a) (nb_occ 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
|