5628
|
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
|