Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Sprache: SML

Original von: Isabelle^©

(* 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: Proof.context -> cterm -> thm option
  val subseteq_cancel_msets: Proof.context -> cterm -> thm option
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

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.