bag.mlw 3.18 KB
Newer Older
1

MARCHE Claude's avatar
MARCHE Claude committed
2
(** {1 Multisets (aka bags)} *)
3

4
module Bag
5

6
  use int.Int
7 8 9

  type bag 'a

10
  (** whatever `'a`, the type `bag 'a` is always infinite *)
11 12
  meta "infinite_type" type bag

MARCHE Claude's avatar
MARCHE Claude committed
13
  (** the most basic operation is the number of occurrences *)
14 15 16 17 18 19 20

  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

MARCHE Claude's avatar
MARCHE Claude committed
21
  (** equality of bags *)
22 23 24 25 26 27

  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

MARCHE Claude's avatar
MARCHE Claude committed
28
  (** basic constructors of bags *)
29 30 31 32 33 34 35 36 37 38 39 40 41

  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)
42
    (* FIXME? nb_occ y (singleton x) = if x = y then 1 else 0 *)
43 44

  lemma occ_singleton_eq:
45
    forall x y: 'a. x = y -> nb_occ y (singleton x) = 1
46
  lemma occ_singleton_neq:
47
    forall x y: 'a. x <> y -> nb_occ y (singleton x) = 0
48 49 50 51 52 53 54

  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

55
  (** `union` is commutative, associative with identity `empty_bag` *)
56 57 58 59 60 61 62 63

  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

64
  lemma bag_simpl_right:
65 66 67 68 69
    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

MARCHE Claude's avatar
MARCHE Claude committed
70
  (** add operation *)
71 72 73 74 75

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

  lemma occ_add_eq:
    forall b: bag 'a, x y: 'a.
76
    x = y -> nb_occ y (add x b) = nb_occ y b + 1
77 78 79 80

  lemma occ_add_neq: forall b: bag 'a, x y: 'a.
    x <> y -> nb_occ y (add x b) = nb_occ y b

MARCHE Claude's avatar
MARCHE Claude committed
81
  (** cardinality of bags *)
82 83 84

  function card (bag 'a): int

85
  axiom Card_nonneg: forall x: bag 'a. card x >= 0
86 87 88 89 90 91 92
  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

MARCHE Claude's avatar
MARCHE Claude committed
93
  (** bag difference *)
94

95
  use int.MinMax
96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112

  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

113 114 115 116 117 118 119
  (** arbitrary element *)

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

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

120
end