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

Last change on this file since 1599 was 1599, checked in by sacerdot, 8 years ago

Start of merging of stuff into the standard library of Matita.

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