Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/HOL/Library/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 5 kB

Impressum 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.3 Sekunden ¤

*Bot Zugriff

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.