|
1 (* Title: HOL/Induct/Multiset.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 1998 TUM |
|
5 |
|
6 A definitional theory of multisets, |
|
7 including a wellfoundedness proof for the multiset order. |
|
8 use_thy"Multiset"; |
|
9 |
|
10 *) |
|
11 |
|
12 Multiset = Multiset0 + Acc + |
|
13 |
|
14 typedef |
|
15 'a multiset = "{f :: 'a => nat . finite{x . 0 < f x}}" (multiset_witness) |
|
16 |
|
17 instance multiset :: (term){ord,plus,minus} |
|
18 |
|
19 consts |
|
20 "{#}" :: 'a multiset ("{#}") |
|
21 single :: 'a => 'a multiset ("{#_#}") |
|
22 count :: ['a multiset, 'a] => nat |
|
23 set_of :: 'a multiset => 'a set |
|
24 |
|
25 syntax |
|
26 elem :: ['a multiset, 'a] => bool |
|
27 translations |
|
28 "elem M a" == "0 < count M a" |
|
29 |
|
30 defs |
|
31 count_def "count == Rep_multiset" |
|
32 empty_def "{#} == Abs_multiset(%a. 0)" |
|
33 single_def "{#a#} == Abs_multiset(%b. if b=a then 1 else 0)" |
|
34 union_def "M+N == Abs_multiset(%a. Rep_multiset M a + Rep_multiset N a)" |
|
35 diff_def "M-N == Abs_multiset(%a. Rep_multiset M a - Rep_multiset N a)" |
|
36 set_of_def "set_of M == {x. elem M x}" |
|
37 size_def "size (M) == setsum (count M) (set_of M)" |
|
38 |
|
39 constdefs |
|
40 mult1 :: "('a * 'a)set => ('a multiset * 'a multiset)set" |
|
41 "mult1(r) == {(N,M) . ? a M0 K. M = M0 + {#a#} & N = M0 + K & |
|
42 (!b. elem K b --> (b,a) : r)}" |
|
43 |
|
44 mult :: "('a * 'a)set => ('a multiset * 'a multiset)set" |
|
45 "mult(r) == (mult1 r)^+" |
|
46 |
|
47 locale MSOrd = |
|
48 fixes |
|
49 r :: "('a * 'a)set" |
|
50 W :: "'a multiset set" |
|
51 |
|
52 assumes |
|
53 |
|
54 defines |
|
55 W_def "W == acc(mult1 r)" |
|
56 end |