# Structure bagSimps

signature bagSimps =
sig
include Abbrev
type cache = Cache.cache
type ssfrag = simpLib.ssfrag
val BAG_AC_ss : ssfrag (* AC-normalises BAG_UNION terms *)
val CANCEL_CONV : conv
(* cancels out common sub-terms in SUB_BAG, equalities and
BAG_DIFFs between BAG_UNION terms. Will return the reflexive
equation when both arguments are {| |}. *)
val BAG_ss : ssfrag
(* includes CANCEL_CONV and a bunch of rewriting theorems, mainly those
to do with the standard operators and empty bags. For example:
{| |} + b = b
(b + c = {| |}) = (b = {| |}) /\ (c = {| |})
*)
val SBAG_SOLVE_ss : ssfrag
(* includes a decision procedure to automatically prove sub-bag and
equality terms by using the arithmetic decision procedure. Can
only prove positive instances, and will not attempt proofs of
terms that involve BAG_DIFF because these are too slow with
arithLib's treatment of subtraction. *)
val SBAG_SOLVE : thm list -> term -> thm
(* the underlying conversion for doing the proofs in the ssfrag value
above *)
val sbag_cache : cache
(* the cache used for caching SBAG_SOLVE's results *)
end

*HOL 4, Kananaskis-13*