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

Last change on this file since 1274 was 1223, checked in by mulligan, 9 years ago

changes

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