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