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

Last change on this file since 1211 was 1210, checked in by mulligan, 9 years ago

getting rid of typeclass-like records in favour of file-level axioms. much too heavyweight to use effectively

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