Theory Multiset

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