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
     1 (* Author: Mathias Fleury, MPII
     2 
     3 
     4 Simprocs for multisets, based on Larry Paulson's simprocs for
     5 natural numbers and numerals.
     6 *)
     7 
     8 signature MULTISET_SIMPROCS =
     9 sig
    10   val subset_cancel_msets: Proof.context -> cterm -> thm option
    11   val subseteq_cancel_msets: Proof.context -> cterm -> thm option
    12 end;
    13 
    14 structure Multiset_Simprocs : MULTISET_SIMPROCS =
    15 struct
    16 
    17 structure Subset_Cancel_Multiset = Cancel_Fun
    18  (open Cancel_Data
    19   val mk_bal   = HOLogic.mk_binrel @{const_name subset_mset}
    20   val dest_bal = HOLogic.dest_bin @{const_name subset_mset} dummyT
    21   val bal_add1 = @{thm mset_subset_add_iff1[unfolded repeat_mset_iterate_add]} RS trans
    22   val bal_add2 = @{thm mset_subset_add_iff2[unfolded repeat_mset_iterate_add]} RS trans
    23 );
    24 
    25 structure Subseteq_Cancel_Multiset = Cancel_Fun
    26  (open Cancel_Data
    27   val mk_bal   = HOLogic.mk_binrel @{const_name subseteq_mset}
    28   val dest_bal = HOLogic.dest_bin @{const_name subseteq_mset} dummyT
    29   val bal_add1 = @{thm mset_subseteq_add_iff1[unfolded repeat_mset_iterate_add]} RS trans
    30   val bal_add2 = @{thm mset_subseteq_add_iff2[unfolded repeat_mset_iterate_add]} RS trans
    31 );
    32 
    33 val subset_cancel_msets = Subset_Cancel_Multiset.proc;
    34 val subseteq_cancel_msets = Subseteq_Cancel_Multiset.proc;
    35 
    36 end