source: src/utilities/adt/priority_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: 1.9 KB
Line 
1include "basics/types.ma".
2include "basics/lists/list.ma".
3include "arithmetics/nat.ma".
4include "common/Integers.ma".
5
6include "ASM/Util.ma".
7
8axiom priority_set: Type[0] → Type[0].
9 
10axiom pset_empty: ∀elt_type. priority_set elt_type.
11axiom pset_size: ∀elt_type. priority_set elt_type → nat.
12 
13axiom pset_to_list: ∀elt_type. priority_set elt_type → list (elt_type × nat).
14 
15axiom pset_insert: ∀elt_type. elt_type → nat → priority_set elt_type → priority_set elt_type.
16axiom pset_remove: ∀elt_type. elt_type → priority_set elt_type → priority_set elt_type.
17axiom pset_lookup: ∀elt_type. elt_type → priority_set elt_type → option nat.
18 
19axiom pset_increment: ∀elt_type. elt_type → int → priority_set elt_type → priority_set elt_type.
20axiom pset_incrementifx: ∀elt_type. elt_type → int → priority_set elt_type → priority_set elt_type.
21axiom pset_modify: ∀elt_type. elt_type → int → priority_set elt_type → priority_set elt_type.
22axiom pset_lowest: ∀elt_type. priority_set elt_type → option (elt_type × nat).
23 
24axiom pset_equal: ∀elt_type. priority_set elt_type → priority_set elt_type → bool.
25 
26axiom pset_map: ∀elt_type. ∀a: Type[0]. (elt_type → a) → priority_set elt_type → priority_set a.
27axiom pset_fold: ∀elt_type. ∀a: Type[0]. (elt_type → int → a → a) → priority_set elt_type → a → a.
28
29definition pset_is_empty ≝
30  λelt_type         : Type[0].
31  λpriority_set     : priority_set elt_type.
32    pset_size … priority_set = 0.
33
34definition pset_singleton ≝
35  λelt_type        : Type[0].
36  λelt             : elt_type.
37  λpriority        : nat.
38    pset_insert … elt priority (pset_empty elt_type).
39
40definition pset_from_list ≝
41  λelt_type        : Type[0].
42  λthe_list        : list (elt_type × nat).
43    foldr … (λelt_priority.
44      let 〈elt, priority〉 ≝ elt_priority in
45        pset_insert elt_type elt priority)
46          (pset_empty …) the_list.
Note: See TracBrowser for help on using the repository browser.