src/HOL/Library/multiset_simprocs.ML
author fleury <Mathias.Fleury@mpi-inf.mpg.de>
Mon Sep 05 15:47:50 2016 +0200 (2016-09-05)
changeset 63793 e68a0b651eb5
child 65029 00731700e54f
permissions -rw-r--r--
add_mset constructor in multisets
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 eq_cancel_msets: Proof.context -> cterm -> thm option
Mathias@63793
    11
  val subset_cancel_msets: Proof.context -> cterm -> thm option
Mathias@63793
    12
  val subseteq_cancel_msets: Proof.context -> cterm -> thm option
Mathias@63793
    13
  val diff_cancel_msets: Proof.context -> cterm -> thm option
Mathias@63793
    14
end;
Mathias@63793
    15
Mathias@63793
    16
structure Multiset_Simprocs : MULTISET_SIMPROCS =
Mathias@63793
    17
struct
Mathias@63793
    18
Mathias@63793
    19
structure EqCancelMultiset = CancelNumeralsFun
Mathias@63793
    20
 (open Multiset_Cancel_Common
Mathias@63793
    21
  val mk_bal   = HOLogic.mk_eq
Mathias@63793
    22
  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} dummyT
Mathias@63793
    23
  val bal_add1 = @{thm mset_eq_add_iff1} RS trans
Mathias@63793
    24
  val bal_add2 = @{thm mset_eq_add_iff2} RS trans
Mathias@63793
    25
);
Mathias@63793
    26
Mathias@63793
    27
structure SubsetCancelMultiset = CancelNumeralsFun
Mathias@63793
    28
 (open Multiset_Cancel_Common
Mathias@63793
    29
  val mk_bal   = HOLogic.mk_binrel @{const_name subset_mset}
Mathias@63793
    30
  val dest_bal = HOLogic.dest_bin @{const_name subset_mset} dummyT
Mathias@63793
    31
  val bal_add1 = @{thm mset_subset_add_iff1} RS trans
Mathias@63793
    32
  val bal_add2 = @{thm mset_subset_add_iff2} RS trans
Mathias@63793
    33
);
Mathias@63793
    34
Mathias@63793
    35
structure SubseteqCancelMultiset = CancelNumeralsFun
Mathias@63793
    36
 (open Multiset_Cancel_Common
Mathias@63793
    37
  val mk_bal   = HOLogic.mk_binrel @{const_name subseteq_mset}
Mathias@63793
    38
  val dest_bal = HOLogic.dest_bin @{const_name subseteq_mset} dummyT
Mathias@63793
    39
  val bal_add1 = @{thm mset_subseteq_add_iff1} RS trans
Mathias@63793
    40
  val bal_add2 = @{thm mset_subseteq_add_iff2} RS trans
Mathias@63793
    41
);
Mathias@63793
    42
Mathias@63793
    43
structure DiffCancelMultiset = CancelNumeralsFun
Mathias@63793
    44
 (open Multiset_Cancel_Common
Mathias@63793
    45
  val mk_bal   = HOLogic.mk_binop @{const_name Groups.minus}
Mathias@63793
    46
  val dest_bal = HOLogic.dest_bin @{const_name Groups.minus} dummyT
Mathias@63793
    47
  val bal_add1 = @{thm mset_diff_add_eq1} RS trans
Mathias@63793
    48
  val bal_add2 = @{thm mset_diff_add_eq2} RS trans
Mathias@63793
    49
);
Mathias@63793
    50
Mathias@63793
    51
val eq_cancel_msets = EqCancelMultiset.proc;
Mathias@63793
    52
val subset_cancel_msets = SubsetCancelMultiset.proc;
Mathias@63793
    53
val subseteq_cancel_msets = SubseteqCancelMultiset.proc;
Mathias@63793
    54
val diff_cancel_msets = DiffCancelMultiset.proc;
Mathias@63793
    55
Mathias@63793
    56
end