src/HOL/Library/multiset_simprocs.ML
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 65029 00731700e54f
child 69593 3dda49e08b9d
permissions -rw-r--r--
executable domain membership checks
Mathias@63793
     1
(* Author: Mathias Fleury, MPII
Mathias@63793
     2
Mathias@63793
     3
Mathias@63793
     4
Simprocs for multisets, based on Larry Paulson's simprocs for
Mathias@63793
     5
natural numbers and numerals.
Mathias@63793
     6
*)
Mathias@63793
     7
Mathias@63793
     8
signature MULTISET_SIMPROCS =
Mathias@63793
     9
sig
Mathias@63793
    10
  val subset_cancel_msets: Proof.context -> cterm -> thm option
Mathias@63793
    11
  val subseteq_cancel_msets: Proof.context -> cterm -> thm option
Mathias@63793
    12
end;
Mathias@63793
    13
Mathias@63793
    14
structure Multiset_Simprocs : MULTISET_SIMPROCS =
Mathias@63793
    15
struct
Mathias@63793
    16
Mathias@65029
    17
structure Subset_Cancel_Multiset = Cancel_Fun
Mathias@65029
    18
 (open Cancel_Data
Mathias@63793
    19
  val mk_bal   = HOLogic.mk_binrel @{const_name subset_mset}
Mathias@63793
    20
  val dest_bal = HOLogic.dest_bin @{const_name subset_mset} dummyT
Mathias@65029
    21
  val bal_add1 = @{thm mset_subset_add_iff1[unfolded repeat_mset_iterate_add]} RS trans
Mathias@65029
    22
  val bal_add2 = @{thm mset_subset_add_iff2[unfolded repeat_mset_iterate_add]} RS trans
Mathias@63793
    23
);
Mathias@63793
    24
Mathias@65029
    25
structure Subseteq_Cancel_Multiset = Cancel_Fun
Mathias@65029
    26
 (open Cancel_Data
Mathias@63793
    27
  val mk_bal   = HOLogic.mk_binrel @{const_name subseteq_mset}
Mathias@63793
    28
  val dest_bal = HOLogic.dest_bin @{const_name subseteq_mset} dummyT
Mathias@65029
    29
  val bal_add1 = @{thm mset_subseteq_add_iff1[unfolded repeat_mset_iterate_add]} RS trans
Mathias@65029
    30
  val bal_add2 = @{thm mset_subseteq_add_iff2[unfolded repeat_mset_iterate_add]} RS trans
Mathias@63793
    31
);
Mathias@63793
    32
Mathias@65029
    33
val subset_cancel_msets = Subset_Cancel_Multiset.proc;
Mathias@65029
    34
val subseteq_cancel_msets = Subseteq_Cancel_Multiset.proc;
Mathias@63793
    35
Mathias@63793
    36
end