Quelle  Multiset.thy

section ‹Multiset›

text ‹
 \file{Multiset} contains a minimal multiset structure.
 ›

theory Multiset
imports Main
begin

subsection ‹A minimal multiset theory›

text ‹
 Völzer, p. 84, does specify that messages in transit are modelled using
 multisets.
 
 We decided to implement a tiny structure for multisets, just fitting our needs.
 These multisets allow to add new values to them, to check for elements existing
 in a certain multiset, filter elements according to boolean predicates, remove
 elements and to create a new multiset from a single element.
 ›

text ‹
 A multiset for a type is a mapping from the elements of the type to natural
 numbers. So, we record how often a message has to be processed in the future.
 ›

type_synonym 'a multiset = "'a ==> nat"

abbreviation mElem ::
  "'a ==> 'a multiset ==> bool" (‹_ ∈# _› 60)
where 
  "mElem a ms ≡ 0 < ms a"

text ‹
 Hence the union of two multisets is the addition of the number of the
 elements and therefore the associative and the commutative laws holds for
 the union.
 ›

abbreviation mUnion ::
  "'a multiset ==> 'a multiset ==> 'a multiset" (‹_ ∪# _› 70)
where
  "mUnion msA msB v ≡ msA v + msB v"

text ‹
 Correspondingly the subtraction is defined and the commutative law holds.
 ›
abbreviation mRm ::
  "'a multiset ==> 'a ==> 'a multiset" (‹_ -# _› 65)
where
  "mRm ms rm v ≡ if v = rm then ms v - 1 else ms v"

abbreviation mSingleton ::
  "'a ==> 'a multiset"          (‹{# _ }›)
where
  "mSingleton a v ≡ if a = v then 1 else 0"

text ‹
 The lemma \isb{AXc} adds just the fact we need for our proofs about
 the commutativity of the union of multisets while elements are removed.
 ›
lemma AXc:
assumes 
  "c1 ≠ c2" and 
  "c1 ∈# X" and
  "c2 ∈# X"
shows "(A1 ∪# ((A2 ∪# (X -# c2)) -# c1))
      = (A2 ∪# ((A1 ∪# (X -# c1)) -# c2))"
proof- 
  have 
    "(A2 ∪# ((A1 ∪# (X -# c1)) -# c2))
         = (A2 ∪# (A1 ∪# ((X -# c1) -# c2)))" 
    using assms by auto
  also have
    "... = (A1 ∪# ((A2 ∪# (X -# c2)) -# c1)) "
    using assms by auto
  finally show ?thesis by auto
qed

end