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
|
