mset Theory

Nuprl's quotient type is used to construct a type of finite multisets from the type of lists. Standard functions over multisets are introduced, including a summation function that draws indices from finite multisets.

A definition is given of a free abelian monoid ADT, and an instance of this ADT is constructed using the multiset functions.

Finite sets are defined as a subtype of finite multisets, and the usual set operations are introduced.


Summary of Definitions


Typed Definitions

mset *4
mk_mset *3 *5

null_mset *3 *2

mset_inj *2 *4

mset_sum *7
eq_mset *6
mset_mon *14
mset_mem *3
ftype *1
mset_for *4

mset_size *5
mset_fmon *16
mset_map *1
mset_union *6 *6

mset_inter *6 *7

mset_diff *6 *9

mset_count *5
mset_union_mon *11
fset_of_mset *1 *3

fset_map *1
bsubmset *4
bsupmset *1
fset *1
ffor *6
mset_prod *5 *1


Main Theorems

all_mset_elim *5
all_fset_elim *16
mset_sum_comm *9
mset_sum_assoc *6
mk_mset_cons *5
assert_of_eq_mset *12
equal_mset_elim *6
mset_sum_ident_r *5
mset_mem_iff_count_nzero *6
mset_mon_for_elim *7
mset_for_functionality *15
mset_for_mset_sum *5
mset_for_mset_inj *3
mset_for_of_id *2
mset_for_of_op *2
dist_hom_over_mset_for *3
mset_for_swap *2
bmsexists_char *6
bmsexists_char_a *6
bmsexists_char_a_rw *1
bmsexists_char_rw *2
non_neg_mset_size *7
mset_fact *4
mset_mem_char *4
mset_map_char *12
mset_map_id *3
eq_mset_iff_eq_counts *9
mset_count_inj *4
mset_count_sum *5
mset_count_union *5
mset_union_assoc *3
mset_union_comm *3
mset_union_ident_l *5
mset_union_ident_r *5
mset_count_inter *5
mset_inter_assoc *3
mset_inter_comm *3
mset_count_diff *5
fset_mem_union *4
mset_mem_inter *4
mset_mem_sum *2
mset_mem_diff *4
mset_union_bor_mon_hom *4
mset_sum_bor_mon_hom *8
mset_mem_mon_for_union *5
mset_count_bound_for_union *11
mset_mem_map *3
fset_of_mset_count_bound *19
fset_of_mset_mem *17
mset_mem_fmap *2
bsubmset_elim *2
bsubmset_weakening *3
bsubmset_transitivity *3
bsubmset_functionality_wrt_bsubmset *7
count_bsubmset *6
mem_bsubmset *8
mset_mem_functionality_wrt_bsubmset *3
detach_msubset *9
mset_ind_a *17
mset_for_when_none *9
mset_for_when_unique *8
fset_for_when_unique *2
fset_for_when_eq *3
mset_for_when_dom_shift *5
mset_for_dom_shift *6
mset_for_functionality_wrt_bsubmset *4
mset_prod_mem *6
prod_in_mset_prod *11

Listing


Last modified February 24th, 1995

Paul Jackson / jackson@cs.cornell.edu