source: src/utilities/adt/set_adt.ma @ 1208

Last change on this file since 1208 was 1208, checked in by mulligan, 8 years ago

added adts for sets, tables and priority sets in order to make life easier when working on the interference graph code

File size: 3.1 KB
Line 
1include "basics/types.ma".
2include "basics/list.ma".
3include "arithmetics/nat.ma".
4
5include "utilities/adt/ordering.ma".
6
7record set_adt
8  (elt_type: Type[0]) (order: ordered elt_type): Type[1] ≝
9{
10  set        : Type[0] → Type[0];
11 
12  set_empty  : set elt_type;
13  set_size   : set elt_type → nat;
14 
15  set_to_list: set elt_type → list elt_type;
16 
17  set_insert : elt_type → set elt_type → set elt_type;
18  set_remove : elt_type → set elt_type → set elt_type;
19 
20  set_member : elt_type → set elt_type → bool;
21 
22  set_forall : (elt_type → bool) → set elt_type → bool;
23  set_exists : (elt_type → bool) → set elt_type → bool;
24  set_filter : (elt_type → bool) → set elt_type → set elt_type;
25 
26  set_equal  : set elt_type → set elt_type → bool;
27 
28  set_map    : ∀a: Type[0]. (elt_type → a) → set elt_type → set a;
29  set_fold   : ∀a: Type[0]. (elt_type → a → a) → set elt_type  → a → a
30}.
31
32definition set_is_empty ≝
33  λelt_type: Type[0].
34  λorder   : ordered elt_type.
35  λset_adt : set_adt elt_type order.
36  λset     : set elt_type order set_adt elt_type.
37    set_size … set = 0.
38
39definition set_singleton ≝
40  λelt_type: Type[0].
41  λorder   : ordered elt_type.
42  λset_adt : set_adt elt_type order.
43  λelt     : elt_type.
44    set_insert … elt (set_empty elt_type order set_adt).
45
46definition set_from_list ≝
47  λelt_type: Type[0].
48  λorder   : ordered elt_type.
49  λset_adt : set_adt elt_type order.
50  λthe_list: list elt_type.
51    foldr … (set_insert elt_type order set_adt) (set_empty …) the_list.
52
53definition set_split ≝
54  λelt_type: Type[0].
55  λorder   : ordered elt_type.
56  λset_adt : set_adt elt_type order.
57  λpred    : elt_type → bool.
58  λthe_set : set elt_type order set_adt elt_type.
59  let left  ≝ set_filter elt_type order set_adt pred the_set in
60  let npred ≝ λx. ¬ (pred x) in
61  let right ≝ set_filter elt_type order set_adt npred the_set in
62    〈left, right〉.
63
64definition set_subset ≝
65  λelt_type: Type[0].
66  λorder   : ordered elt_type.
67  λset_adt : set_adt elt_type order.
68  λleft    : set elt_type order set_adt elt_type.
69  λright   : set elt_type order set_adt elt_type.
70    set_forall … (λelt. set_member … elt right) left.
71
72definition set_subseteq ≝
73  λelt_type: Type[0].
74  λorder   : ordered elt_type.
75  λset_adt : set_adt elt_type order.
76  λleft    : set elt_type order set_adt elt_type.
77  λright   : set elt_type order set_adt elt_type.
78    set_equal … left right ∧ (set_subset elt_type order set_adt left right).
79
80definition set_union ≝
81  λelt_type: Type[0].
82  λorder   : ordered elt_type.
83  λset_adt : set_adt elt_type order.
84  λleft    : set elt_type order set_adt elt_type.
85  λright   : set elt_type order set_adt elt_type.
86    set_fold … (set_insert elt_type order set_adt) left right.
87
88definition set_intersection ≝
89  λelt_type: Type[0].
90  λelt_type: Type[0].
91  λorder   : ordered elt_type.
92  λset_adt : set_adt elt_type order.
93  λleft    : set elt_type order set_adt elt_type.
94  λright   : set elt_type order set_adt elt_type.
95    set_filter … (λelt. set_member … elt right) left.
Note: See TracBrowser for help on using the repository browser.