Quelle multiset_simprocs.ML Sprache: SML

(* Author: Mathias Fleury, MPII

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

signature MULTISET_SIMPROCS =
sig
  val subset_cancel_msets: Simplifier.proc
  val subseteq_cancel_msets: Simplifier.proc
end;

structure Multiset_Simprocs : MULTISET_SIMPROCS =
struct

structure Subset_Cancel_Multiset = Cancel_Fun
(open Cancel_Data
  val mk_bal   = HOLogic.mk_binrel \<^const_name>\<open>subset_mset\<close>
  val dest_bal = HOLogic.dest_bin \<^const_name>\<open>subset_mset\<close> dummyT
  val bal_add1 = @{thm mset_subset_add_iff1[unfolded repeat_mset_iterate_add]} RS trans
  val bal_add2 = @{thm mset_subset_add_iff2[unfolded repeat_mset_iterate_add]} RS trans
);

structure Subseteq_Cancel_Multiset = Cancel_Fun
(open Cancel_Data
  val mk_bal   = HOLogic.mk_binrel \<^const_name>\<open>subseteq_mset\<close>
  val dest_bal = HOLogic.dest_bin \<^const_name>\<open>subseteq_mset\<close> dummyT
  val bal_add1 = @{thm mset_subseteq_add_iff1[unfolded repeat_mset_iterate_add]} RS trans
  val bal_add2 = @{thm mset_subseteq_add_iff2[unfolded repeat_mset_iterate_add]} RS trans
);

val subset_cancel_msets = Subset_Cancel_Multiset.proc;
val subseteq_cancel_msets = Subseteq_Cancel_Multiset.proc;

end

quality99%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.