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

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

a lot added to interference graph calculation

File size: 2.4 KB
Line 
1include "basics/types.ma".
2include "basics/list.ma".
3include "arithmetics/nat.ma".
4include "ASM/Util.ma".
5
6include "utilities/adt/ordering.ma".
7
8axiom set: Type[0] → Type[0].
9axiom set_empty: ∀elt_type. set elt_type.
10
11axiom set_size: ∀elt_type. set elt_type → nat.
12axiom set_to_list: ∀elt_type. set elt_type → list elt_type.
13axiom set_insert: ∀elt_type. elt_type → set elt_type → set elt_type.
14axiom set_remove: ∀elt_type. elt_type → set elt_type → set elt_type.
15axiom set_member: ∀elt_type. elt_type → set elt_type → bool.
16axiom set_forall: ∀elt_type. (elt_type → bool) → set elt_type → bool.
17axiom set_exists: ∀elt_type. (elt_type → bool) → set elt_type → bool.
18axiom set_filter: ∀elt_type. (elt_type → bool) → set elt_type → set elt_type.
19axiom set_equal: ∀elt_type. set elt_type → set elt_type → bool.
20axiom set_map: ∀elt_type, a. (elt_type → a) → set elt_type → set a.
21axiom set_fold: ∀elt_type, a: Type[0]. (elt_type → a → a) → set elt_type  → a → a.
22
23definition set_is_empty ≝
24  λelt_type: Type[0].
25  λset: set elt_type.
26    eq_nat (set_size elt_type set) 0.
27
28definition set_singleton ≝
29  λelt_type: Type[0].
30  λelt     : elt_type.
31    set_insert elt_type elt (set_empty elt_type).
32
33definition set_from_list ≝
34  λelt_type: Type[0].
35  λthe_list: list elt_type.
36    foldr … (set_insert elt_type) (set_empty elt_type) the_list.
37
38definition set_split ≝
39  λelt_type: Type[0].
40  λpred    : elt_type → bool.
41  λthe_set : set elt_type.
42  let left  ≝ set_filter elt_type pred the_set in
43  let npred ≝ λx. ¬ (pred x) in
44  let right ≝ set_filter elt_type npred the_set in
45    〈left, right〉.
46
47definition set_subset ≝
48  λelt_type: Type[0].
49  λleft    : set elt_type.
50  λright   : set elt_type.
51    set_forall elt_type (λelt. set_member elt_type elt right) left.
52
53definition set_subseteq ≝
54  λelt_type: Type[0].
55  λleft    : set elt_type.
56  λright   : set elt_type.
57    set_equal elt_type left right ∧ (set_subset elt_type left right).
58
59definition set_union ≝
60  λelt_type: Type[0].
61  λleft    : set elt_type.
62  λright   : set elt_type.
63    set_fold elt_type (set elt_type) (set_insert elt_type) left right.
64
65definition set_intersection ≝
66  λelt_type: Type[0].
67  λleft    : set elt_type.
68  λright   : set elt_type.
69    set_filter elt_type (λelt. set_member elt_type elt right) left.
Note: See TracBrowser for help on using the repository browser.