1signature bagLib =
2sig
3  include Abbrev
4  type cache = Cache.cache
5  type ssfrag = simpLib.ssfrag
6
7
8  val EMPTY_BAG_tm : term
9  val BAG_DIFF_tm : term
10  val SUB_BAG_tm : term
11  val BAG_INSERT_tm : term
12  val BAG_UNION_tm : term
13  val BAG_IMAGE_tm : term
14  val BAG_ALL_DISTINCT_tm : term
15  val BAG_EVERY_tm : term
16
17  val is_bag_ty : hol_type -> bool
18  val bag_ty : hol_type
19
20  val base_type : term -> hol_type
21  val list_mk_union : term list -> term
22  val mk_diff : term * term -> term
23  val mk_sub_bag : term * term -> term
24  val dest_sub_bag : term -> term * term
25  val is_sub_bag : term -> bool
26  val is_diff : term -> bool
27  val dest_diff : term -> term * term
28  val mk_union : term * term -> term
29  val list_mk_insert : term list * term -> term
30  val mk_insert : term * term -> term
31  val dest_union : term -> term * term
32  val strip_union : term -> term list
33  val is_insert : term -> bool
34  val dest_insert : term -> term * term
35  val is_union : term -> bool
36  val mk_image : term * term -> term
37  val dest_image : term -> term * term
38  val is_image : term -> bool
39  val is_empty : term -> bool
40  val mk_all_distinct : term -> term
41  val dest_all_distinct : term -> term
42  val is_all_distinct : term -> bool
43  val mk_card : term -> term
44  val dest_card : term -> term
45  val is_card : term -> bool
46  val mk_every : term * term -> term
47  val dest_every : term -> term * term
48  val is_every : term -> bool
49
50  val mk_bag : term list * hol_type -> term
51  val strip_insert : term -> term list * term
52  val dest_bag : term -> term list * hol_type
53
54
55  val BAG_AC_ss     : ssfrag
56  val CANCEL_CONV   : conv
57  val BAG_ss        : ssfrag
58  val SBAG_SOLVE_ss : ssfrag
59  val SBAG_SOLVE    : thm list -> term -> thm
60  val sbag_cache    : cache
61
62  val BAG_RESORT_CONV : int list -> conv
63  val BAG_IMAGE_CONV  : conv
64  val GET_BAG_IN_THMS : term -> thm list
65
66
67  val get_resort_position___pred       : (term -> bool) -> term -> int option
68  val get_resort_list___pred           : (term -> bool) -> term -> int list
69  val get_resort_positions___pred_pair : (term -> term -> bool) -> term -> term -> (int * int) option
70  val get_resort_lists___pred_pair     : (term -> term -> bool) -> term -> term -> (int list * int list)
71
72  val SIMPLE_BAG_NORMALISE_CONV  : conv
73  val BAG_EQ_INSERT_CANCEL_CONV  : conv
74  val BAG_DIFF_INSERT_CANCEL_CONV: conv
75  val SUB_BAG_INSERT_CANCEL_CONV : conv
76  val SUB_BAG_INSERT_SOLVE       : term -> thm
77
78end
79