equal
deleted
inserted
replaced
31 definition |
31 definition |
32 mset_of :: "i=>i" where |
32 mset_of :: "i=>i" where |
33 "mset_of(M) == domain(M)" |
33 "mset_of(M) == domain(M)" |
34 |
34 |
35 definition |
35 definition |
36 munion :: "[i, i] => i" (infixl "+#" 65) where |
36 munion :: "[i, i] => i" (infixl \<open>+#\<close> 65) where |
37 "M +# N == \<lambda>x \<in> mset_of(M) \<union> mset_of(N). |
37 "M +# N == \<lambda>x \<in> mset_of(M) \<union> mset_of(N). |
38 if x \<in> mset_of(M) \<inter> mset_of(N) then (M`x) #+ (N`x) |
38 if x \<in> mset_of(M) \<inter> mset_of(N) then (M`x) #+ (N`x) |
39 else (if x \<in> mset_of(M) then M`x else N`x)" |
39 else (if x \<in> mset_of(M) then M`x else N`x)" |
40 |
40 |
41 definition |
41 definition |
45 if (\<exists>A. f \<in> A -> nat & Finite(A)) then |
45 if (\<exists>A. f \<in> A -> nat & Finite(A)) then |
46 funrestrict(f, {x \<in> mset_of(f). 0 < f`x}) |
46 funrestrict(f, {x \<in> mset_of(f). 0 < f`x}) |
47 else 0" |
47 else 0" |
48 |
48 |
49 definition |
49 definition |
50 mdiff :: "[i, i] => i" (infixl "-#" 65) where |
50 mdiff :: "[i, i] => i" (infixl \<open>-#\<close> 65) where |
51 "M -# N == normalize(\<lambda>x \<in> mset_of(M). |
51 "M -# N == normalize(\<lambda>x \<in> mset_of(M). |
52 if x \<in> mset_of(N) then M`x #- N`x else M`x)" |
52 if x \<in> mset_of(N) then M`x #- N`x else M`x)" |
53 |
53 |
54 definition |
54 definition |
55 (* set of elements of a multiset *) |
55 (* set of elements of a multiset *) |
56 msingle :: "i => i" ("{#_#}") where |
56 msingle :: "i => i" (\<open>{#_#}\<close>) where |
57 "{#a#} == {<a, 1>}" |
57 "{#a#} == {<a, 1>}" |
58 |
58 |
59 definition |
59 definition |
60 MCollect :: "[i, i=>o] => i" (*comprehension*) where |
60 MCollect :: "[i, i=>o] => i" (*comprehension*) where |
61 "MCollect(M, P) == funrestrict(M, {x \<in> mset_of(M). P(x)})" |
61 "MCollect(M, P) == funrestrict(M, {x \<in> mset_of(M). P(x)})" |
68 definition |
68 definition |
69 msize :: "i => i" where |
69 msize :: "i => i" where |
70 "msize(M) == setsum(%a. $# mcount(M,a), mset_of(M))" |
70 "msize(M) == setsum(%a. $# mcount(M,a), mset_of(M))" |
71 |
71 |
72 abbreviation |
72 abbreviation |
73 melem :: "[i,i] => o" ("(_/ :# _)" [50, 51] 50) where |
73 melem :: "[i,i] => o" (\<open>(_/ :# _)\<close> [50, 51] 50) where |
74 "a :# M == a \<in> mset_of(M)" |
74 "a :# M == a \<in> mset_of(M)" |
75 |
75 |
76 syntax |
76 syntax |
77 "_MColl" :: "[pttrn, i, o] => i" ("(1{# _ \<in> _./ _#})") |
77 "_MColl" :: "[pttrn, i, o] => i" (\<open>(1{# _ \<in> _./ _#})\<close>) |
78 translations |
78 translations |
79 "{#x \<in> M. P#}" == "CONST MCollect(M, \<lambda>x. P)" |
79 "{#x \<in> M. P#}" == "CONST MCollect(M, \<lambda>x. P)" |
80 |
80 |
81 (* multiset orderings *) |
81 (* multiset orderings *) |
82 |
82 |
98 definition |
98 definition |
99 omultiset :: "i => o" where |
99 omultiset :: "i => o" where |
100 "omultiset(M) == \<exists>i. Ord(i) & M \<in> Mult(field(Memrel(i)))" |
100 "omultiset(M) == \<exists>i. Ord(i) & M \<in> Mult(field(Memrel(i)))" |
101 |
101 |
102 definition |
102 definition |
103 mless :: "[i, i] => o" (infixl "<#" 50) where |
103 mless :: "[i, i] => o" (infixl \<open><#\<close> 50) where |
104 "M <# N == \<exists>i. Ord(i) & <M, N> \<in> multirel(field(Memrel(i)), Memrel(i))" |
104 "M <# N == \<exists>i. Ord(i) & <M, N> \<in> multirel(field(Memrel(i)), Memrel(i))" |
105 |
105 |
106 definition |
106 definition |
107 mle :: "[i, i] => o" (infixl "<#=" 50) where |
107 mle :: "[i, i] => o" (infixl \<open><#=\<close> 50) where |
108 "M <#= N == (omultiset(M) & M = N) | M <# N" |
108 "M <#= N == (omultiset(M) & M = N) | M <# N" |
109 |
109 |
110 |
110 |
111 subsection\<open>Properties of the original "restrict" from ZF.thy\<close> |
111 subsection\<open>Properties of the original "restrict" from ZF.thy\<close> |
112 |
112 |