src/HOL/Library/multiset_order_simprocs.ML
author haftmann
Tue, 07 Feb 2017 22:15:03 +0100
changeset 64995 a7af4045f873
parent 63793 e68a0b651eb5
child 65029 00731700e54f
permissions -rw-r--r--
preprocessing rules must always stem from static context

(* Author: Mathias Fleury, MPII


Simprocs for multisets ordering, based on the simprocs for nat numerals.
*)

signature MULTISET_ORDER_SIMPROCS =
sig
  val less_cancel_msets: Proof.context -> cterm -> thm option
  val le_cancel_msets: Proof.context -> cterm -> thm option
end;

structure Multiset_Order_Simprocs : MULTISET_ORDER_SIMPROCS =
struct

structure LessCancelMultiset = CancelNumeralsFun
 (open Multiset_Cancel_Common
  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} dummyT
  val bal_add1 = @{thm mset_less_add_iff1} RS trans
  val bal_add2 = @{thm mset_less_add_iff2} RS trans
);

structure LeCancelMultiset = CancelNumeralsFun
 (open Multiset_Cancel_Common
  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} dummyT
  val bal_add1 = @{thm mset_le_add_iff1} RS trans
  val bal_add2 = @{thm mset_le_add_iff2} RS trans
);

val less_cancel_msets = LessCancelMultiset.proc;
val le_cancel_msets = LeCancelMultiset.proc;

end