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   meta extensionality predicate (==)
  29
  30   (** basic constructors of bags *)
  31
  32   function empty_bag: bag 'a
  33
  34   axiom occ_empty: forall x: 'a. nb_occ x empty_bag = 0
  35
  36   lemma is_empty: forall b: bag 'a.
  37     (forall x: 'a. nb_occ x b = 0) -> b = empty_bag
  38
  39   function singleton (x: 'a) : bag 'a
  40
  41   axiom occ_singleton: forall x y: 'a.
  42     (x = y /\ (nb_occ y (singleton x)) = 1) \/
  43     (x <> y /\ (nb_occ y (singleton x)) = 0)
  44     (* FIXME? nb_occ y (singleton x) = if x = y then 1 else 0 *)
  45
  46   lemma occ_singleton_eq:
  47     forall x y: 'a. x = y -> nb_occ y (singleton x) = 1
  48   lemma occ_singleton_neq:
  49     forall x y: 'a. x <> y -> nb_occ y (singleton x) = 0
  50
  51   (** union *)
  52
  53   function union (bag 'a) (bag 'a) : bag 'a
  54
  55   axiom occ_union:
  56     forall x: 'a, a b: bag 'a.
  57     nb_occ x (union a b) = nb_occ x a + nb_occ x b
  58
  59   lemma Union_comm: forall a b: bag 'a. union a b = union b a
  60
  61   lemma Union_identity: forall a: bag 'a. union a empty_bag = a
  62
  63   lemma Union_assoc:
  64     forall a b c: bag 'a. union a (union b c) = union (union a b) c
  65
  66   lemma bag_simpl_right:
  67     forall a b c: bag 'a. union a b = union c b -> a = c
  68
  69   lemma bag_simpl_left:
  70     forall a b c: bag 'a. union a b = union a c -> b = c
  71
  72   (** add operation *)
  73
  74   function add (x: 'a) (b: bag 'a) : bag 'a = union (singleton x) b
  75
  76   lemma occ_add_eq:
  77     forall b: bag 'a, x y: 'a.
  78     x = y -> nb_occ y (add x b) = nb_occ y b + 1
  79
  80   lemma occ_add_neq: forall b: bag 'a, x y: 'a.
  81     x <> y -> nb_occ y (add x b) = nb_occ y b
  82
  83   (** cardinality *)
  84
  85   function card (bag 'a): int
  86
  87   axiom Card_nonneg: forall x: bag 'a. card x >= 0
  88   axiom Card_empty: card (empty_bag: bag 'a) = 0
  89   axiom Card_zero_empty: forall x: bag 'a. card x = 0 -> x = empty_bag
  90
  91   axiom Card_singleton: forall x:'a. card (singleton x) = 1
  92   axiom Card_union: forall x y: bag 'a. card (union x y) = card x + card y
  93   lemma Card_add: forall x: 'a, b: bag 'a. card (add x b) = 1 + card b
  94
  95   (** difference *)
  96
  97   use int.MinMax
  98
  99   function diff (bag 'a) (bag 'a) : bag 'a
 100
 101   axiom Diff_occ: forall b1 b2: bag 'a, x:'a.
 102     nb_occ x (diff b1 b2) = max 0 (nb_occ x b1 - nb_occ x b2)
 103
 104   lemma Diff_empty_right: forall b: bag 'a. diff b empty_bag = b
 105   lemma Diff_empty_left: forall b: bag 'a. diff empty_bag b = empty_bag
 106
 107   lemma Diff_add: forall b: bag 'a, x:'a. diff (add x b) (singleton x) = b
 108
 109   lemma Diff_comm:
 110     forall b b1 b2: bag 'a. diff (diff b b1) b2 = diff (diff b b2) b1
 111
 112   lemma Add_diff: forall b: bag 'a, x:'a.
 113     mem x b -> add x (diff b (singleton x)) = b
 114
 115   (** intersection *)
 116
 117   function inter (a b: bag 'a) : bag 'a
 118
 119   axiom inter:
 120     forall x: 'a, a b: bag 'a.
 121     nb_occ x (inter a b) = min (nb_occ x a) (nb_occ x b)
 122
 123   (** arbitrary element *)
 124
 125   function choose (b: bag 'a) : 'a
 126
 127   axiom choose_mem: forall b: bag 'a.
 128     empty_bag <> b -> mem (choose b) b
 129
 130 end