# Theory Multiset

Up to index of Isabelle/HOLCF/IOA/NTP

theory Multiset
imports Lemmas
uses [Multiset.ML]
begin

    (*  Title:      HOL/IOA/NTP/Multiset.thy
        ID:         $Id: Multiset.thy,v 1.7 2005/09/03 14:50:24 wenzelm Exp $
        Author:     Tobias Nipkow & Konrad Slind
    *)

    header {* Axiomatic multisets *}

    theory Multiset
    imports Lemmas
    begin

    typedecl
      'a multiset

    consts

      "{|}"  :: "'a multiset"                        ("{|}")
      addm   :: "['a multiset, 'a] => 'a multiset"
      delm   :: "['a multiset, 'a] => 'a multiset"
      countm :: "['a multiset, 'a => bool] => nat"
      count  :: "['a multiset, 'a] => nat"

    axioms

    delm_empty_def:
      "delm {|} x = {|}"

    delm_nonempty_def:
      "delm (addm M x) y == (if x=y then M else addm (delm M y) x)"

    countm_empty_def:
       "countm {|} P == 0"

    countm_nonempty_def:
       "countm (addm M x) P == countm M P + (if P x then Suc 0 else 0)"

    count_def:
       "count M x == countm M (%y. y = x)"

    "induction":
       "[| P({|}); !!M x. P(M) ==> P(addm M x) |] ==> P(M)"

    ML {* use_text Context.ml_output true
      ("structure Multiset = struct " ^ legacy_bindings (the_context ()) ^ " end") *}
    ML {* open Multiset *}

    end

theorem count_empty:

      count {|} x = 0

theorem count_addm_simp:

      count (addm M x) y = (if y = x then Suc (count M y) else count M y)

theorem count_leq_addm:

      count M y ≤ count (addm M x) y

theorem count_delm_simp:

      count (delm M x) y = (if y = x then count M y - 1 else count M y)

theorem countm_props:

      ∀x. P x --> Q x ==> countm M P ≤ countm M Q

theorem countm_spurious_delm:

      ¬ P obj ==> countm M P = countm (delm M obj) P

theorem pos_count_imp_pos_countm:

      [| P x; 0 < count M x |] ==> 0 < countm M P

theorem countm_done_delm:

      P x ==> 0 < count M x --> countm (delm M x) P = countm M P - 1