1signature bagSyntax =
2sig
3   include Abbrev
4
5  val EMPTY_BAG_tm : term
6  val BAG_DIFF_tm : term
7  val SUB_BAG_tm : term
8  val BAG_INSERT_tm : term
9  val BAG_UNION_tm : term
10  val BAG_IMAGE_tm : term
11  val BAG_CARD_tm : term
12  val BAG_ALL_DISTINCT_tm : term
13  val BAG_EVERY_tm : term
14
15  val is_bag_ty : hol_type -> bool
16  val bag_ty : hol_type
17
18  val base_type : term -> hol_type
19  val list_mk_union : term list -> term
20  val mk_diff : term * term -> term
21  val mk_sub_bag : term * term -> term
22  val dest_sub_bag : term -> term * term
23  val is_sub_bag : term -> bool
24  val is_diff : term -> bool
25  val dest_diff : term -> term * term
26  val mk_union : term * term -> term
27  val list_mk_insert : term list * term -> term
28  val mk_insert : term * term -> term
29  val dest_union : term -> term * term
30  val strip_union : term -> term list
31  val is_insert : term -> bool
32  val dest_insert : term -> term * term
33  val is_union : term -> bool
34  val mk_image : term * term -> term
35  val dest_image : term -> term * term
36  val is_image : term -> bool
37  val is_empty : term -> bool
38  val mk_all_distinct : term -> term
39  val dest_all_distinct : term -> term
40  val is_all_distinct : term -> bool
41  val mk_card : term -> term
42  val dest_card : term -> term
43  val is_card : term -> bool
44  val mk_every : term * term -> term
45  val dest_every : term -> term * term
46  val is_every : term -> bool
47
48  val mk_bag : term list * hol_type -> term
49  val strip_insert : term -> term list * term
50  val dest_bag : term -> term list * hol_type
51
52end
53