why3/stdlib/bag.mlw at master · Cactus-proj/why3 · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130

(** {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