Multiset = Arith + "Lemmas" +
types
'a multiset
arities
multiset :: (term) term
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"
rules
delm_empty_def
"delm({|},x) = {|}"
delm_nonempty_def
"delm(addm(M,x),y) == if(x=y,M,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), Suc(0), 0)"
count_def
"count(M,x) == countm(M, %y.y = x)"
induction
"[| P({|}); !!M x. P(M) ==> P(addm(M,x)) |] ==> P(M)"
end