stdlib/bag.mlw

   1
   2 (** {1 Multisets (aka bags)} *)
   3
   4 module Bag
   5
   6   use int.Int
   7
   8   type bag 'a
   9
  10   (** whatever `'a`, the type `bag 'a` is always infinite *)
  11   meta "infinite_type" type bag
  12
  13   (** the most basic operation is the number of occurrences *)
  14
  15   function nb_occ (x: 'a) (b: bag 'a): int
  16
  17   axiom occ_non_negative: forall b: bag 'a, x: 'a. nb_occ x b >= 0
  18
  19   predicate mem (x: 'a) (b: bag 'a) = nb_occ x b > 0
  20
  21   (** equality of bags *)
  22
  23   predicate (==) (a b: bag 'a) =
  24     forall x:'a. nb_occ x a = nb_occ x b
  25
  26   axiom bag_extensionality: forall a b: bag 'a. a == b -> a = b
  27
  28   (** basic constructors of bags *)
  29
  30   function empty_bag: bag 'a
  31
  32   axiom occ_empty: forall x: 'a. nb_occ x empty_bag = 0
  33
  34   lemma is_empty: forall b: bag 'a.
  35     (forall x: 'a. nb_occ x b = 0) -> b = empty_bag
  36
  37   function singleton (x: 'a) : bag 'a
  38
  39   axiom occ_singleton: forall x y: 'a.
  40     (x = y /\ (nb_occ y (singleton x)) = 1) \/
  41     (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   (** union *)
  50
  51   function union (bag 'a) (bag 'a) : bag 'a
  52
  53   axiom occ_union:
  54     forall x: 'a, a b: bag 'a.
  55     nb_occ x (union a b) = nb_occ x a + nb_occ x b
  56
  57   lemma Union_comm: forall a b: bag 'a. union a b = union b a
  58
  59   lemma Union_identity: forall a: bag 'a. union a empty_bag = a
  60
  61   lemma Union_assoc:
  62     forall a b c: bag 'a. union a (union b c) = union (union a b) c
  63
  64   lemma bag_simpl_right:
  65     forall a b c: bag 'a. union a b = union c b -> a = c
  66
  67   lemma bag_simpl_left:
  68     forall a b c: bag 'a. union a b = union a c -> b = c
  69
  70   (** add operation *)
  71
  72   function add (x: 'a) (b: bag 'a) : bag 'a = union (singleton x) b
  73
  74   lemma occ_add_eq:
  75     forall b: bag 'a, x y: 'a.
  76     x = y -> nb_occ y (add x b) = nb_occ y b + 1
  77
  78   lemma occ_add_neq: forall b: bag 'a, x y: 'a.
  79     x <> y -> nb_occ y (add x b) = nb_occ y b
  80
  81   (** cardinality *)
  82
  83   function card (bag 'a): int
  84
  85   axiom Card_nonneg: forall x: bag 'a. card x >= 0
  86   axiom Card_empty: card (empty_bag: bag 'a) = 0
  87   axiom Card_zero_empty: forall x: bag 'a. card x = 0 -> x = empty_bag
  88
  89   axiom Card_singleton: forall x:'a. card (singleton x) = 1
  90   axiom Card_union: forall x y: bag 'a. card (union x y) = card x + card y
  91   lemma Card_add: forall x: 'a, b: bag 'a. card (add x b) = 1 + card b
  92
  93   (** difference *)
  94
  95   use int.MinMax
  96
  97   function diff (bag 'a) (bag 'a) : bag 'a
  98
  99   axiom Diff_occ: forall b1 b2: bag 'a, x:'a.
 100     nb_occ x (diff b1 b2) = max 0 (nb_occ x b1 - nb_occ x b2)
 101
 102   lemma Diff_empty_right: forall b: bag 'a. diff b empty_bag = b
 103   lemma Diff_empty_left: forall b: bag 'a. diff empty_bag b = empty_bag
 104
 105   lemma Diff_add: forall b: bag 'a, x:'a. diff (add x b) (singleton x) = b
 106
 107   lemma Diff_comm:
 108     forall b b1 b2: bag 'a. diff (diff b b1) b2 = diff (diff b b2) b1
 109
 110   lemma Add_diff: forall b: bag 'a, x:'a.
 111     mem x b -> add x (diff b (singleton x)) = b
 112
 113   (** intersection *)
 114
 115   function inter (a b: bag 'a) : bag 'a
 116
 117   axiom inter:
 118     forall x: 'a, a b: bag 'a.
 119     nb_occ x (inter a b) = min (nb_occ x a) (nb_occ x b)
 120
 121   (** arbitrary element *)
 122
 123   function choose (b: bag 'a) : 'a
 124
 125   axiom choose_mem: forall b: bag 'a.
 126     empty_bag <> b -> mem (choose b) b
 127
 128 end