source: src/utilities/adt/priority_set_adt.ma

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

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

File size: 1.9 KB
RevLine 
[1208]1include "basics/types.ma".
[1599]2include "basics/lists/list.ma".
[1208]3include "arithmetics/nat.ma".
[1218]4include "common/Integers.ma".
[1208]5
6include "ASM/Util.ma".
7
[1210]8axiom priority_set: Type[0] → Type[0].
[1208]9 
[1218]10axiom pset_empty: ∀elt_type. priority_set elt_type.
11axiom pset_size: ∀elt_type. priority_set elt_type → nat.
[1208]12 
[1218]13axiom pset_to_list: ∀elt_type. priority_set elt_type → list (elt_type × nat).
[1208]14 
[1218]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.
[1208]18 
[1218]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).
[1208]23 
[1218]24axiom pset_equal: ∀elt_type. priority_set elt_type → priority_set elt_type → bool.
[1208]25 
[1218]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.
[1208]28
[1218]29definition pset_is_empty ≝
[1208]30  λelt_type         : Type[0].
[1210]31  λpriority_set     : priority_set elt_type.
[1218]32    pset_size … priority_set = 0.
[1208]33
[1218]34definition pset_singleton ≝
[1208]35  λelt_type        : Type[0].
36  λelt             : elt_type.
37  λpriority        : nat.
[1218]38    pset_insert … elt priority (pset_empty elt_type).
[1208]39
[1218]40definition pset_from_list ≝
[1208]41  λelt_type        : Type[0].
42  λthe_list        : list (elt_type × nat).
43    foldr … (λelt_priority.
44      let 〈elt, priority〉 ≝ elt_priority in
[1218]45        pset_insert elt_type elt priority)
46          (pset_empty …) the_list.
Note: See TracBrowser for help on using the repository browser.