mset Theory

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