src/HOL/Library/multiset_simprocs.ML

clarified modules;

(* Author: Mathias Fleury, MPII


Simprocs for multisets, based on Larry Paulson's simprocs for
natural numbers and numerals.
*)

signature MULTISET_SIMPROCS =
sig
  val eq_cancel_msets: Proof.context -> cterm -> thm option
  val subset_cancel_msets: Proof.context -> cterm -> thm option
  val subseteq_cancel_msets: Proof.context -> cterm -> thm option
  val diff_cancel_msets: Proof.context -> cterm -> thm option
end;

structure Multiset_Simprocs : MULTISET_SIMPROCS =
struct

structure EqCancelMultiset = CancelNumeralsFun
 (open Multiset_Cancel_Common
  val mk_bal   = HOLogic.mk_eq
  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} dummyT
  val bal_add1 = @{thm mset_eq_add_iff1} RS trans
  val bal_add2 = @{thm mset_eq_add_iff2} RS trans
);

structure SubsetCancelMultiset = CancelNumeralsFun
 (open Multiset_Cancel_Common
  val mk_bal   = HOLogic.mk_binrel @{const_name subset_mset}
  val dest_bal = HOLogic.dest_bin @{const_name subset_mset} dummyT
  val bal_add1 = @{thm mset_subset_add_iff1} RS trans
  val bal_add2 = @{thm mset_subset_add_iff2} RS trans
);

structure SubseteqCancelMultiset = CancelNumeralsFun
 (open Multiset_Cancel_Common
  val mk_bal   = HOLogic.mk_binrel @{const_name subseteq_mset}
  val dest_bal = HOLogic.dest_bin @{const_name subseteq_mset} dummyT
  val bal_add1 = @{thm mset_subseteq_add_iff1} RS trans
  val bal_add2 = @{thm mset_subseteq_add_iff2} RS trans
);

structure DiffCancelMultiset = CancelNumeralsFun
 (open Multiset_Cancel_Common
  val mk_bal   = HOLogic.mk_binop @{const_name Groups.minus}
  val dest_bal = HOLogic.dest_bin @{const_name Groups.minus} dummyT
  val bal_add1 = @{thm mset_diff_add_eq1} RS trans
  val bal_add2 = @{thm mset_diff_add_eq2} RS trans
);

val eq_cancel_msets = EqCancelMultiset.proc;
val subset_cancel_msets = SubsetCancelMultiset.proc;
val subseteq_cancel_msets = SubseteqCancelMultiset.proc;
val diff_cancel_msets = DiffCancelMultiset.proc;

end