1051
|
1 |
(* Title: HOL/IOA/NTP/Multiset.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow & Konrad Slind
|
|
4 |
Copyright 1994 TU Muenchen
|
|
5 |
|
|
6 |
Axiomatic multisets.
|
|
7 |
Should be done as a subtype and moved to a global place.
|
|
8 |
*)
|
|
9 |
|
1328
|
10 |
Multiset = Arith + Lemmas +
|
1051
|
11 |
|
|
12 |
types
|
|
13 |
|
|
14 |
'a multiset
|
|
15 |
|
|
16 |
arities
|
|
17 |
|
|
18 |
multiset :: (term) term
|
|
19 |
|
|
20 |
consts
|
|
21 |
|
1376
|
22 |
"{|}" :: 'a multiset ("{|}")
|
|
23 |
addm :: ['a multiset, 'a] => 'a multiset
|
|
24 |
delm :: ['a multiset, 'a] => 'a multiset
|
|
25 |
countm :: ['a multiset, 'a => bool] => nat
|
|
26 |
count :: ['a multiset, 'a] => nat
|
1051
|
27 |
|
|
28 |
rules
|
|
29 |
|
|
30 |
delm_empty_def
|
|
31 |
"delm {|} x = {|}"
|
|
32 |
|
|
33 |
delm_nonempty_def
|
|
34 |
"delm (addm M x) y == (if x=y then M else addm (delm M y) x)"
|
|
35 |
|
|
36 |
countm_empty_def
|
|
37 |
"countm {|} P == 0"
|
|
38 |
|
|
39 |
countm_nonempty_def
|
|
40 |
"countm (addm M x) P == countm M P + (if P x then Suc 0 else 0)"
|
|
41 |
|
|
42 |
count_def
|
|
43 |
"count M x == countm M (%y.y = x)"
|
|
44 |
|
|
45 |
induction
|
|
46 |
"[| P({|}); !!M x. P(M) ==> P(addm M x) |] ==> P(M)"
|
|
47 |
|
|
48 |
end
|