author | paulson |
Fri, 15 Feb 2002 12:07:27 +0100 | |
changeset 12891 | 92af5c3a10fb |
parent 12860 | 7fc3fbfed8ef |
child 14046 | 6616e6c53d48 |
permissions | -rw-r--r-- |
12610 | 1 |
(* Title: ZF/Induct/Multiset.thy |
12089
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
3 |
Author: Sidi O Ehmety, Cambridge University Computer Laboratory |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
4 |
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
5 |
A definitional theory of multisets, |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
6 |
including a wellfoundedness proof for the multiset order. |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
7 |
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
8 |
The theory features ordinal multisets and the usual ordering. |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
9 |
*) |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
10 |
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
11 |
Multiset = FoldSet + Acc + |
12860
7fc3fbfed8ef
Multiset: added the translation Mult(A) => A-||>nat-{0}
paulson
parents:
12610
diff
changeset
|
12 |
consts |
7fc3fbfed8ef
Multiset: added the translation Mult(A) => A-||>nat-{0}
paulson
parents:
12610
diff
changeset
|
13 |
(* Short cut for multiset space *) |
7fc3fbfed8ef
Multiset: added the translation Mult(A) => A-||>nat-{0}
paulson
parents:
12610
diff
changeset
|
14 |
Mult :: i=>i |
7fc3fbfed8ef
Multiset: added the translation Mult(A) => A-||>nat-{0}
paulson
parents:
12610
diff
changeset
|
15 |
translations |
7fc3fbfed8ef
Multiset: added the translation Mult(A) => A-||>nat-{0}
paulson
parents:
12610
diff
changeset
|
16 |
"Mult(A)" => "A-||>nat-{0}" |
7fc3fbfed8ef
Multiset: added the translation Mult(A) => A-||>nat-{0}
paulson
parents:
12610
diff
changeset
|
17 |
|
12089
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
18 |
constdefs |
12891 | 19 |
|
20 |
(* This is the original "restrict" from ZF.thy. |
|
21 |
Restricts the function f to the domain A |
|
22 |
FIXME: adapt Multiset to the new "restrict". *) |
|
23 |
||
24 |
funrestrict :: "[i,i] => i" |
|
25 |
"funrestrict(f,A) == lam x:A. f`x" |
|
26 |
||
12089
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
27 |
(* M is a multiset *) |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
28 |
multiset :: i => o |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
29 |
"multiset(M) == EX A. M:A->nat-{0} & Finite(A)" |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
30 |
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
31 |
mset_of :: "i=>i" |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
32 |
"mset_of(M) == domain(M)" |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
33 |
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
34 |
munion :: "[i, i] => i" (infixl "+#" 65) |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
35 |
"M +# N == lam x:mset_of(M) Un mset_of(N). |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
36 |
if x:mset_of(M) Int mset_of(N) then (M`x) #+ (N`x) |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
37 |
else (if x:mset_of(M) then M`x else N`x)" |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
38 |
|
12860
7fc3fbfed8ef
Multiset: added the translation Mult(A) => A-||>nat-{0}
paulson
parents:
12610
diff
changeset
|
39 |
(* eliminating 0's from a function *) |
12089
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
40 |
normalize :: i => i |
12891 | 41 |
"normalize(M) == funrestrict(M, {x:mset_of(M). 0<M`x})" |
12089
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
42 |
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
43 |
mdiff :: "[i, i] => i" (infixl "-#" 65) |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
44 |
"M -# N == normalize(lam x:mset_of(M). |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
45 |
if x:mset_of(N) then M`x #- N`x else M`x)" |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
46 |
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
47 |
(* set of elements of a multiset *) |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
48 |
msingle :: "i => i" ("{#_#}") |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
49 |
"{#a#} == {<a, 1>}" |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
50 |
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
51 |
MCollect :: [i, i=>o] => i (*comprehension*) |
12891 | 52 |
"MCollect(M, P) == funrestrict(M, {x:mset_of(M). P(x)})" |
12089
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
53 |
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
54 |
(* Counts the number of occurences of an element in a multiset *) |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
55 |
mcount :: [i, i] => i |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
56 |
"mcount(M, a) == if a:mset_of(M) then M`a else 0" |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
57 |
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
58 |
msize :: i => i |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
59 |
"msize(M) == setsum(%a. $# mcount(M,a), mset_of(M))" |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
60 |
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
61 |
syntax |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
62 |
melem :: "[i,i] => o" ("(_/ :# _)" [50, 51] 50) |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
63 |
"@MColl" :: "[pttrn, i, o] => i" ("(1{# _ : _./ _#})") |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
64 |
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
65 |
translations |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
66 |
"a :# M" == "a:mset_of(M)" |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
67 |
"{#x:M. P#}" == "MCollect(M, %x. P)" |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
68 |
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
69 |
(* multiset orderings *) |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
70 |
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
71 |
constdefs |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
72 |
(* multirel1 has to be a set (not a predicate) so that we can form |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
73 |
its transitive closure and reason about wf(.) and acc(.) *) |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
74 |
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
75 |
multirel1 :: "[i,i]=>i" |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
76 |
"multirel1(A, r) == |
12860
7fc3fbfed8ef
Multiset: added the translation Mult(A) => A-||>nat-{0}
paulson
parents:
12610
diff
changeset
|
77 |
{<M, N> : Mult(A)*Mult(A). |
7fc3fbfed8ef
Multiset: added the translation Mult(A) => A-||>nat-{0}
paulson
parents:
12610
diff
changeset
|
78 |
EX a:A. EX M0:Mult(A). EX K:Mult(A). |
7fc3fbfed8ef
Multiset: added the translation Mult(A) => A-||>nat-{0}
paulson
parents:
12610
diff
changeset
|
79 |
N=M0 +# {#a#} & M=M0 +# K & (ALL b:mset_of(K). <b,a>:r)}" |
12089
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
80 |
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
81 |
multirel :: "[i, i] => i" |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
82 |
"multirel(A, r) == multirel1(A, r)^+" |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
83 |
|
12860
7fc3fbfed8ef
Multiset: added the translation Mult(A) => A-||>nat-{0}
paulson
parents:
12610
diff
changeset
|
84 |
(* ordinal multiset orderings *) |
12089
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
85 |
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
86 |
omultiset :: i => o |
12860
7fc3fbfed8ef
Multiset: added the translation Mult(A) => A-||>nat-{0}
paulson
parents:
12610
diff
changeset
|
87 |
"omultiset(M) == EX i. Ord(i) & M:Mult(field(Memrel(i)))" |
12089
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
88 |
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
89 |
mless :: [i, i] => o (infixl "<#" 50) |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
90 |
"M <# N == EX i. Ord(i) & <M, N>:multirel(field(Memrel(i)), Memrel(i))" |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
91 |
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
92 |
mle :: [i, i] => o (infixl "<#=" 50) |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
93 |
"M <#= N == (omultiset(M) & M = N) | M <# N" |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
94 |
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
95 |
end |