source: src/utilities/adt/priority_set_adt.ma @ 1212

Last change on this file since 1212 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: 1.8 KB
Line 
1include "basics/types.ma".
2include "basics/list.ma".
3include "arithmetics/nat.ma".
4
5include "utilities/adt/ordering.ma".
6include "ASM/Util.ma".
7
8axiom priority_set: Type[0] → Type[0].
9 
10axiom ps_empty: ∀elt_type. priority_set elt_type.
11axiom ps_size: ∀elt_type. priority_set elt_type → nat.
12 
13axiom ps_to_list: ∀elt_type. priority_set elt_type → list (elt_type × nat).
14 
15axiom ps_insert: ∀elt_type. elt_type → nat → priority_set elt_type → priority_set elt_type.
16axiom ps_remove: ∀elt_type. elt_type → priority_set elt_type → priority_set elt_type.
17axiom ps_lookup: ∀elt_type. elt_type → priority_set elt_type → option nat.
18 
19axiom ps_increment: ∀elt_type. elt_type → priority_set elt_type → priority_set elt_type.
20axiom ps_modify: ∀elt_type. elt_type → nat → priority_set elt_type → priority_set elt_type.
21axiom ps_lowest: ∀elt_type. priority_set elt_type → option (elt_type × nat).
22 
23axiom ps_equal: ∀elt_type. priority_set elt_type → priority_set elt_type → bool.
24 
25axiom ps_map: ∀elt_type. ∀a: Type[0]. (elt_type → a) → priority_set elt_type → priority_set a.
26axiom ps_fold: ∀elt_type. ∀a: Type[0]. (elt_type → nat → a → a) → priority_set elt_type → a → a.
27
28definition ps_is_empty ≝
29  λelt_type         : Type[0].
30  λpriority_set     : priority_set elt_type.
31    ps_size … priority_set = 0.
32
33definition ps_singleton ≝
34  λelt_type        : Type[0].
35  λelt             : elt_type.
36  λpriority        : nat.
37    ps_insert … elt priority (ps_empty elt_type).
38
39definition from_list ≝
40  λelt_type        : Type[0].
41  λthe_list        : list (elt_type × nat).
42    foldr … (λelt_priority.
43      let 〈elt, priority〉 ≝ elt_priority in
44        ps_insert elt_type elt priority)
45          (ps_empty …) the_list.
Note: See TracBrowser for help on using the repository browser.