| 1 | include "basics/types.ma". |
|---|
| 2 | include "basics/lists/list.ma". |
|---|
| 3 | include "arithmetics/nat.ma". |
|---|
| 4 | include "ASM/Util.ma". |
|---|
| 5 | |
|---|
| 6 | axiom set: Type[0] → Type[0]. |
|---|
| 7 | |
|---|
| 8 | inductive 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 | |
|---|
| 12 | axiom set_empty: ∀elt_type. set elt_type. |
|---|
| 13 | |
|---|
| 14 | axiom set_size: ∀elt_type. set elt_type → nat. |
|---|
| 15 | axiom set_to_list: ∀elt_type. set elt_type → list elt_type. |
|---|
| 16 | axiom set_insert: ∀elt_type. elt_type → set elt_type → set elt_type. |
|---|
| 17 | axiom set_remove: ∀elt_type. elt_type → set elt_type → set elt_type. |
|---|
| 18 | axiom set_member: ∀elt_type. (elt_type → elt_type → bool) → elt_type → set elt_type → bool. |
|---|
| 19 | axiom set_forall: ∀elt_type. (elt_type → bool) → set elt_type → bool. |
|---|
| 20 | axiom set_exists: ∀elt_type. (elt_type → bool) → set elt_type → bool. |
|---|
| 21 | axiom set_filter: ∀elt_type. (elt_type → bool) → set elt_type → set elt_type. |
|---|
| 22 | axiom set_map: ∀elt_type, a. (elt_type → a) → set elt_type → set a. |
|---|
| 23 | axiom set_fold: ∀elt_type, a: Type[0]. (elt_type → a → a) → set elt_type → a → a. |
|---|
| 24 | axiom 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 *) |
|---|
| 28 | axiom set_diff: ∀elt_type: Type[0]. set elt_type → set elt_type → set elt_type. |
|---|
| 29 | |
|---|
| 30 | definition set_is_empty ≝ |
|---|
| 31 | λelt_type: Type[0]. |
|---|
| 32 | λset: set elt_type. |
|---|
| 33 | eq_nat (set_size elt_type set) 0. |
|---|
| 34 | |
|---|
| 35 | definition set_singleton ≝ |
|---|
| 36 | λelt_type: Type[0]. |
|---|
| 37 | λelt : elt_type. |
|---|
| 38 | set_insert elt_type elt (set_empty elt_type). |
|---|
| 39 | |
|---|
| 40 | definition 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 | |
|---|
| 45 | definition 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 | |
|---|
| 54 | definition 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 | |
|---|
| 61 | definition 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 | |
|---|
| 68 | definition 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 | |
|---|
| 74 | definition 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. |
|---|
