include "basics/types.ma".

include "utilities/adt/set_adt.ma".
include "utilities/adt/table_adt.ma".

axiom set_table: Type[0] → Type[0] → Type[0].

axiom set_tbl_empty: ∀key_type, a. set_table key_type a.
axiom set_tbl_find: ∀key_type, a. key_type → set_table key_type (set a) → option (set a).
axiom set_tbl_add: ∀key_type, a. key_type → set a
                     → set_table key_type (set a) → set_table key_type (set a).
axiom set_tbl_update: ∀key_type, a. key_type → (set a → set a) → set_table key_type (set a)
                     → set_table key_type (set a).
axiom set_tbl_mkedge: ∀key_type, a. key_type → a → set_table key_type (set a) →
                         set_table key_type (set a).
axiom set_tbl_rmedge: ∀key_type, a. key_type → a → set_table key_type (set a) →
                         set_table key_type (set a).
axiom set_tbl_iter: ∀key_type, a. (key_type → a → a) → 
                      set_table key_type (set a) → set_table key_type (set a).
axiom set_tbl_fold: ∀key_type, a, b: Type[0]. (key_type → a → b → b)
                      → set_table key_type a -> b -> b.
axiom set_tbl_pick: ∀key_type, a. set_table key_type (set a) →
                      ((key_type × a) → bool) → option (key_type × a).


axiom set_tbl_homo_mkbiedge: ∀key_type. key_type → key_type → set_table key_type (set key_type) → set_table key_type (set key_type).
axiom set_tbl_homo_rmbiedge: ∀key_type. key_type → key_type → set_table key_type (set key_type) → set_table key_type (set key_type).
axiom set_tbl_homo_reverse: ∀key_type. set_table key_type (set key_type) → set_table key_type (set key_type).
axiom set_tbl_homo_restrict: ∀key_type. (key_type → bool) → set_table key_type (set key_type) → set_table key_type (set key_type).