author  nipkow 
Thu, 28 Feb 2008 14:04:29 +0100  
changeset 26178  3396ba6d0823 
parent 26176  038baad81209 
child 26567  7bcebb8c2d33 
permissions  rwrr 
10249  1 
(* Title: HOL/Library/Multiset.thy 
2 
ID: $Id$ 

15072  3 
Author: Tobias Nipkow, Markus Wenzel, Lawrence C Paulson, Norbert Voelker 
10249  4 
*) 
5 

14706  6 
header {* Multisets *} 
10249  7 

15131  8 
theory Multiset 
25595  9 
imports List 
15131  10 
begin 
10249  11 

12 
subsection {* The type of multisets *} 

13 

25162  14 
typedef 'a multiset = "{f::'a => nat. finite {x . f x > 0}}" 
10249  15 
proof 
11464  16 
show "(\<lambda>x. 0::nat) \<in> ?multiset" by simp 
10249  17 
qed 
18 

19 
lemmas multiset_typedef [simp] = 

10277  20 
Abs_multiset_inverse Rep_multiset_inverse Rep_multiset 
21 
and [simp] = Rep_multiset_inject [symmetric] 

10249  22 

19086  23 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21214
diff
changeset

24 
Mempty :: "'a multiset" ("{#}") where 
19086  25 
"{#} = Abs_multiset (\<lambda>a. 0)" 
10249  26 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21214
diff
changeset

27 
definition 
25507  28 
single :: "'a => 'a multiset" where 
29 
"single a = Abs_multiset (\<lambda>b. if b = a then 1 else 0)" 

10249  30 

26016  31 
declare 
32 
Mempty_def[code func del] single_def[code func del] 

33 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21214
diff
changeset

34 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21214
diff
changeset

35 
count :: "'a multiset => 'a => nat" where 
19086  36 
"count = Rep_multiset" 
10249  37 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21214
diff
changeset

38 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21214
diff
changeset

39 
MCollect :: "'a multiset => ('a => bool) => 'a multiset" where 
19086  40 
"MCollect M P = Abs_multiset (\<lambda>x. if P x then Rep_multiset M x else 0)" 
41 

19363  42 
abbreviation 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21214
diff
changeset

43 
Melem :: "'a => 'a multiset => bool" ("(_/ :# _)" [50, 51] 50) where 
25610  44 
"a :# M == 0 < count M a" 
45 

26145  46 
notation (xsymbols) 
47 
Melem (infix "\<in>#" 50) 

10249  48 

49 
syntax 

26033  50 
"_MCollect" :: "pttrn => 'a multiset => bool => 'a multiset" ("(1{# _ :# _./ _#})") 
10249  51 
translations 
26033  52 
"{#x :# M. P#}" == "CONST MCollect M (\<lambda>x. P)" 
10249  53 

19086  54 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21214
diff
changeset

55 
set_of :: "'a multiset => 'a set" where 
19086  56 
"set_of M = {x. x :# M}" 
10249  57 

25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25507
diff
changeset

58 
instantiation multiset :: (type) "{plus, minus, zero, size}" 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25507
diff
changeset

59 
begin 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25507
diff
changeset

60 

c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25507
diff
changeset

61 
definition 
26016  62 
union_def[code func del]: 
26145  63 
"M + N = Abs_multiset (\<lambda>a. Rep_multiset M a + Rep_multiset N a)" 
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25507
diff
changeset

64 

c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25507
diff
changeset

65 
definition 
26145  66 
diff_def: "M  N = Abs_multiset (\<lambda>a. Rep_multiset M a  Rep_multiset N a)" 
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25507
diff
changeset

67 

c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25507
diff
changeset

68 
definition 
26145  69 
Zero_multiset_def [simp]: "0 = {#}" 
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25507
diff
changeset

70 

c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25507
diff
changeset

71 
definition 
26145  72 
size_def[code func del]: "size M = setsum (count M) (set_of M)" 
25571
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25507
diff
changeset

73 

c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25507
diff
changeset

74 
instance .. 
c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25507
diff
changeset

75 

c9e39eafc7a0
instantiation target rather than legacy instance
haftmann
parents:
25507
diff
changeset

76 
end 
10249  77 

19086  78 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21214
diff
changeset

79 
multiset_inter :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<inter>" 70) where 
19086  80 
"multiset_inter A B = A  (A  B)" 
15869  81 

26145  82 
text {* Multiset Enumeration *} 
83 
syntax 

26176  84 
"_multiset" :: "args => 'a multiset" ("{#(_)#}") 
25507  85 
translations 
86 
"{#x, xs#}" == "{#x#} + {#xs#}" 

87 
"{#x#}" == "CONST single x" 

88 

10249  89 

90 
text {* 

91 
\medskip Preservation of the representing set @{term multiset}. 

92 
*} 

93 

26016  94 
lemma const0_in_multiset: "(\<lambda>a. 0) \<in> multiset" 
26178  95 
by (simp add: multiset_def) 
10249  96 

26016  97 
lemma only1_in_multiset: "(\<lambda>b. if b = a then 1 else 0) \<in> multiset" 
26178  98 
by (simp add: multiset_def) 
10249  99 

26016  100 
lemma union_preserves_multiset: 
26178  101 
"M \<in> multiset ==> N \<in> multiset ==> (\<lambda>a. M a + N a) \<in> multiset" 
102 
apply (simp add: multiset_def) 

103 
apply (drule (1) finite_UnI) 

104 
apply (simp del: finite_Un add: Un_def) 

105 
done 

10249  106 

26016  107 
lemma diff_preserves_multiset: 
26178  108 
"M \<in> multiset ==> (\<lambda>a. M a  N a) \<in> multiset" 
109 
apply (simp add: multiset_def) 

110 
apply (rule finite_subset) 

111 
apply auto 

112 
done 

10249  113 

26016  114 
lemma MCollect_preserves_multiset: 
26178  115 
"M \<in> multiset ==> (\<lambda>x. if P x then M x else 0) \<in> multiset" 
116 
apply (simp add: multiset_def) 

117 
apply (rule finite_subset, auto) 

118 
done 

10249  119 

26016  120 
lemmas in_multiset = const0_in_multiset only1_in_multiset 
121 
union_preserves_multiset diff_preserves_multiset MCollect_preserves_multiset 

122 

26145  123 

26016  124 
subsection {* Algebraic properties *} 
10249  125 

126 
subsubsection {* Union *} 

127 

17161  128 
lemma union_empty [simp]: "M + {#} = M \<and> {#} + M = M" 
26178  129 
by (simp add: union_def Mempty_def in_multiset) 
10249  130 

17161  131 
lemma union_commute: "M + N = N + (M::'a multiset)" 
26178  132 
by (simp add: union_def add_ac in_multiset) 
17161  133 

134 
lemma union_assoc: "(M + N) + K = M + (N + (K::'a multiset))" 

26178  135 
by (simp add: union_def add_ac in_multiset) 
10249  136 

17161  137 
lemma union_lcomm: "M + (N + K) = N + (M + (K::'a multiset))" 
138 
proof  

26178  139 
have "M + (N + K) = (N + K) + M" by (rule union_commute) 
140 
also have "\<dots> = N + (K + M)" by (rule union_assoc) 

141 
also have "K + M = M + K" by (rule union_commute) 

17161  142 
finally show ?thesis . 
143 
qed 

10249  144 

17161  145 
lemmas union_ac = union_assoc union_commute union_lcomm 
10249  146 

14738  147 
instance multiset :: (type) comm_monoid_add 
17200  148 
proof 
14722
8e739a6eaf11
replaced applystyle proof for instance Multiset :: plus_ac0 by recommended Isar proof style
obua
parents:
14706
diff
changeset

149 
fix a b c :: "'a multiset" 
8e739a6eaf11
replaced applystyle proof for instance Multiset :: plus_ac0 by recommended Isar proof style
obua
parents:
14706
diff
changeset

150 
show "(a + b) + c = a + (b + c)" by (rule union_assoc) 
8e739a6eaf11
replaced applystyle proof for instance Multiset :: plus_ac0 by recommended Isar proof style
obua
parents:
14706
diff
changeset

151 
show "a + b = b + a" by (rule union_commute) 
8e739a6eaf11
replaced applystyle proof for instance Multiset :: plus_ac0 by recommended Isar proof style
obua
parents:
14706
diff
changeset

152 
show "0 + a = a" by simp 
8e739a6eaf11
replaced applystyle proof for instance Multiset :: plus_ac0 by recommended Isar proof style
obua
parents:
14706
diff
changeset

153 
qed 
10277  154 

10249  155 

156 
subsubsection {* Difference *} 

157 

17161  158 
lemma diff_empty [simp]: "M  {#} = M \<and> {#}  M = {#}" 
26178  159 
by (simp add: Mempty_def diff_def in_multiset) 
10249  160 

17161  161 
lemma diff_union_inverse2 [simp]: "M + {#a#}  {#a#} = M" 
26178  162 
by (simp add: union_def diff_def in_multiset) 
10249  163 

26143
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

164 
lemma diff_cancel: "A  A = {#}" 
26178  165 
by (simp add: diff_def Mempty_def) 
26143
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

166 

10249  167 

168 
subsubsection {* Count of elements *} 

169 

17161  170 
lemma count_empty [simp]: "count {#} a = 0" 
26178  171 
by (simp add: count_def Mempty_def in_multiset) 
10249  172 

17161  173 
lemma count_single [simp]: "count {#b#} a = (if b = a then 1 else 0)" 
26178  174 
by (simp add: count_def single_def in_multiset) 
10249  175 

17161  176 
lemma count_union [simp]: "count (M + N) a = count M a + count N a" 
26178  177 
by (simp add: count_def union_def in_multiset) 
10249  178 

17161  179 
lemma count_diff [simp]: "count (M  N) a = count M a  count N a" 
26178  180 
by (simp add: count_def diff_def in_multiset) 
26016  181 

182 
lemma count_MCollect [simp]: 

26178  183 
"count {# x:#M. P x #} a = (if P a then count M a else 0)" 
184 
by (simp add: count_def MCollect_def in_multiset) 

10249  185 

186 

187 
subsubsection {* Set of elements *} 

188 

17161  189 
lemma set_of_empty [simp]: "set_of {#} = {}" 
26178  190 
by (simp add: set_of_def) 
10249  191 

17161  192 
lemma set_of_single [simp]: "set_of {#b#} = {b}" 
26178  193 
by (simp add: set_of_def) 
10249  194 

17161  195 
lemma set_of_union [simp]: "set_of (M + N) = set_of M \<union> set_of N" 
26178  196 
by (auto simp add: set_of_def) 
10249  197 

17161  198 
lemma set_of_eq_empty_iff [simp]: "(set_of M = {}) = (M = {#})" 
26178  199 
by (auto simp: set_of_def Mempty_def in_multiset count_def expand_fun_eq) 
10249  200 

17161  201 
lemma mem_set_of_iff [simp]: "(x \<in> set_of M) = (x :# M)" 
26178  202 
by (auto simp add: set_of_def) 
26016  203 

26033  204 
lemma set_of_MCollect [simp]: "set_of {# x:#M. P x #} = set_of M \<inter> {x. P x}" 
26178  205 
by (auto simp add: set_of_def) 
10249  206 

207 

208 
subsubsection {* Size *} 

209 

26016  210 
lemma size_empty [simp,code func]: "size {#} = 0" 
26178  211 
by (simp add: size_def) 
10249  212 

26016  213 
lemma size_single [simp,code func]: "size {#b#} = 1" 
26178  214 
by (simp add: size_def) 
10249  215 

17161  216 
lemma finite_set_of [iff]: "finite (set_of M)" 
26178  217 
using Rep_multiset [of M] by (simp add: multiset_def set_of_def count_def) 
10249  218 

17161  219 
lemma setsum_count_Int: 
26178  220 
"finite A ==> setsum (count N) (A \<inter> set_of N) = setsum (count N) A" 
221 
apply (induct rule: finite_induct) 

222 
apply simp 

223 
apply (simp add: Int_insert_left set_of_def) 

224 
done 

10249  225 

26016  226 
lemma size_union[simp,code func]: "size (M + N::'a multiset) = size M + size N" 
26178  227 
apply (unfold size_def) 
228 
apply (subgoal_tac "count (M + N) = (\<lambda>a. count M a + count N a)") 

229 
prefer 2 

230 
apply (rule ext, simp) 

231 
apply (simp (no_asm_simp) add: setsum_Un_nat setsum_addf setsum_count_Int) 

232 
apply (subst Int_commute) 

233 
apply (simp (no_asm_simp) add: setsum_count_Int) 

234 
done 

10249  235 

17161  236 
lemma size_eq_0_iff_empty [iff]: "(size M = 0) = (M = {#})" 
26178  237 
apply (unfold size_def Mempty_def count_def, auto simp: in_multiset) 
238 
apply (simp add: set_of_def count_def in_multiset expand_fun_eq) 

239 
done 

26016  240 

241 
lemma nonempty_has_size: "(S \<noteq> {#}) = (0 < size S)" 

26178  242 
by (metis gr0I gr_implies_not0 size_empty size_eq_0_iff_empty) 
10249  243 

17161  244 
lemma size_eq_Suc_imp_elem: "size M = Suc n ==> \<exists>a. a :# M" 
26178  245 
apply (unfold size_def) 
246 
apply (drule setsum_SucD) 

247 
apply auto 

248 
done 

10249  249 

26145  250 

10249  251 
subsubsection {* Equality of multisets *} 
252 

17161  253 
lemma multiset_eq_conv_count_eq: "(M = N) = (\<forall>a. count M a = count N a)" 
26178  254 
by (simp add: count_def expand_fun_eq) 
10249  255 

17161  256 
lemma single_not_empty [simp]: "{#a#} \<noteq> {#} \<and> {#} \<noteq> {#a#}" 
26178  257 
by (simp add: single_def Mempty_def in_multiset expand_fun_eq) 
10249  258 

17161  259 
lemma single_eq_single [simp]: "({#a#} = {#b#}) = (a = b)" 
26178  260 
by (auto simp add: single_def in_multiset expand_fun_eq) 
10249  261 

17161  262 
lemma union_eq_empty [iff]: "(M + N = {#}) = (M = {#} \<and> N = {#})" 
26178  263 
by (auto simp add: union_def Mempty_def in_multiset expand_fun_eq) 
10249  264 

17161  265 
lemma empty_eq_union [iff]: "({#} = M + N) = (M = {#} \<and> N = {#})" 
26178  266 
by (auto simp add: union_def Mempty_def in_multiset expand_fun_eq) 
10249  267 

17161  268 
lemma union_right_cancel [simp]: "(M + K = N + K) = (M = (N::'a multiset))" 
26178  269 
by (simp add: union_def in_multiset expand_fun_eq) 
10249  270 

17161  271 
lemma union_left_cancel [simp]: "(K + M = K + N) = (M = (N::'a multiset))" 
26178  272 
by (simp add: union_def in_multiset expand_fun_eq) 
10249  273 

17161  274 
lemma union_is_single: 
26178  275 
"(M + N = {#a#}) = (M = {#a#} \<and> N={#} \<or> M = {#} \<and> N = {#a#})" 
276 
apply (simp add: Mempty_def single_def union_def in_multiset add_is_1 expand_fun_eq) 

277 
apply blast 

278 
done 

10249  279 

17161  280 
lemma single_is_union: 
26178  281 
"({#a#} = M + N) \<longleftrightarrow> ({#a#} = M \<and> N = {#} \<or> M = {#} \<and> {#a#} = N)" 
282 
apply (unfold Mempty_def single_def union_def) 

283 
apply (simp add: add_is_1 one_is_add in_multiset expand_fun_eq) 

284 
apply (blast dest: sym) 

285 
done 

10249  286 

17161  287 
lemma add_eq_conv_diff: 
10249  288 
"(M + {#a#} = N + {#b#}) = 
15072  289 
(M = N \<and> a = b \<or> M = N  {#a#} + {#b#} \<and> N = M  {#b#} + {#a#})" 
26178  290 
using [[simproc del: neq]] 
291 
apply (unfold single_def union_def diff_def) 

292 
apply (simp (no_asm) add: in_multiset expand_fun_eq) 

293 
apply (rule conjI, force, safe, simp_all) 

294 
apply (simp add: eq_sym_conv) 

295 
done 

10249  296 

15869  297 
declare Rep_multiset_inject [symmetric, simp del] 
298 

23611  299 
instance multiset :: (type) cancel_ab_semigroup_add 
300 
proof 

301 
fix a b c :: "'a multiset" 

302 
show "a + b = a + c \<Longrightarrow> b = c" by simp 

303 
qed 

15869  304 

25610  305 
lemma insert_DiffM: 
306 
"x \<in># M \<Longrightarrow> {#x#} + (M  {#x#}) = M" 

26178  307 
by (clarsimp simp: multiset_eq_conv_count_eq) 
25610  308 

309 
lemma insert_DiffM2[simp]: 

310 
"x \<in># M \<Longrightarrow> M  {#x#} + {#x#} = M" 

26178  311 
by (clarsimp simp: multiset_eq_conv_count_eq) 
25610  312 

313 
lemma multi_union_self_other_eq: 

314 
"(A::'a multiset) + X = A + Y \<Longrightarrow> X = Y" 

26178  315 
by (induct A arbitrary: X Y) auto 
25610  316 

317 
lemma multi_self_add_other_not_self[simp]: "(A = A + {#x#}) = False" 

26178  318 
by (metis single_not_empty union_empty union_left_cancel) 
25610  319 

320 
lemma insert_noteq_member: 

321 
assumes BC: "B + {#b#} = C + {#c#}" 

322 
and bnotc: "b \<noteq> c" 

323 
shows "c \<in># B" 

324 
proof  

325 
have "c \<in># C + {#c#}" by simp 

326 
have nc: "\<not> c \<in># {#b#}" using bnotc by simp 

26145  327 
then have "c \<in># B + {#b#}" using BC by simp 
328 
then show "c \<in># B" using nc by simp 

25610  329 
qed 
330 

331 

26016  332 
lemma add_eq_conv_ex: 
333 
"(M + {#a#} = N + {#b#}) = 

334 
(M = N \<and> a = b \<or> (\<exists>K. M = K + {#b#} \<and> N = K + {#a#}))" 

26178  335 
by (auto simp add: add_eq_conv_diff) 
26016  336 

337 

338 
lemma empty_multiset_count: 

339 
"(\<forall>x. count A x = 0) = (A = {#})" 

26178  340 
by (metis count_empty multiset_eq_conv_count_eq) 
26016  341 

342 

15869  343 
subsubsection {* Intersection *} 
344 

345 
lemma multiset_inter_count: 

26178  346 
"count (A #\<inter> B) x = min (count A x) (count B x)" 
347 
by (simp add: multiset_inter_def min_def) 

15869  348 

349 
lemma multiset_inter_commute: "A #\<inter> B = B #\<inter> A" 

26178  350 
by (simp add: multiset_eq_conv_count_eq multiset_inter_count 
21214
a91bab12b2bd
adjusted two lemma names due to name change in interpretation
haftmann
parents:
20770
diff
changeset

351 
min_max.inf_commute) 
15869  352 

353 
lemma multiset_inter_assoc: "A #\<inter> (B #\<inter> C) = A #\<inter> B #\<inter> C" 

26178  354 
by (simp add: multiset_eq_conv_count_eq multiset_inter_count 
21214
a91bab12b2bd
adjusted two lemma names due to name change in interpretation
haftmann
parents:
20770
diff
changeset

355 
min_max.inf_assoc) 
15869  356 

357 
lemma multiset_inter_left_commute: "A #\<inter> (B #\<inter> C) = B #\<inter> (A #\<inter> C)" 

26178  358 
by (simp add: multiset_eq_conv_count_eq multiset_inter_count min_def) 
15869  359 

17161  360 
lemmas multiset_inter_ac = 
361 
multiset_inter_commute 

362 
multiset_inter_assoc 

363 
multiset_inter_left_commute 

15869  364 

26143
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

365 
lemma multiset_inter_single: "a \<noteq> b \<Longrightarrow> {#a#} #\<inter> {#b#} = {#}" 
26178  366 
by (simp add: multiset_eq_conv_count_eq multiset_inter_count) 
26143
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

367 

15869  368 
lemma multiset_union_diff_commute: "B #\<inter> C = {#} \<Longrightarrow> A + B  C = A  C + B" 
26178  369 
apply (simp add: multiset_eq_conv_count_eq multiset_inter_count min_def 
17161  370 
split: split_if_asm) 
26178  371 
apply clarsimp 
372 
apply (erule_tac x = a in allE) 

373 
apply auto 

374 
done 

15869  375 

10249  376 

26016  377 
subsubsection {* Comprehension (filter) *} 
378 

379 
lemma MCollect_empty[simp, code func]: "MCollect {#} P = {#}" 

26178  380 
by (simp add: MCollect_def Mempty_def Abs_multiset_inject 
26145  381 
in_multiset expand_fun_eq) 
26016  382 

383 
lemma MCollect_single[simp, code func]: 

26178  384 
"MCollect {#x#} P = (if P x then {#x#} else {#})" 
385 
by (simp add: MCollect_def Mempty_def single_def Abs_multiset_inject 

26145  386 
in_multiset expand_fun_eq) 
26016  387 

388 
lemma MCollect_union[simp, code func]: 

389 
"MCollect (M+N) f = MCollect M f + MCollect N f" 

26178  390 
by (simp add: MCollect_def union_def Abs_multiset_inject 
26145  391 
in_multiset expand_fun_eq) 
26016  392 

393 

394 
subsection {* Induction and case splits *} 

10249  395 

396 
lemma setsum_decr: 

11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11655
diff
changeset

397 
"finite F ==> (0::nat) < f a ==> 
15072  398 
setsum (f (a := f a  1)) F = (if a\<in>F then setsum f F  1 else setsum f F)" 
26178  399 
apply (induct rule: finite_induct) 
400 
apply auto 

401 
apply (drule_tac a = a in mk_disjoint_insert, auto) 

402 
done 

10249  403 

10313  404 
lemma rep_multiset_induct_aux: 
26178  405 
assumes 1: "P (\<lambda>a. (0::nat))" 
406 
and 2: "!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1))" 

407 
shows "\<forall>f. f \<in> multiset > setsum f {x. f x \<noteq> 0} = n > P f" 

408 
apply (unfold multiset_def) 

409 
apply (induct_tac n, simp, clarify) 

410 
apply (subgoal_tac "f = (\<lambda>a.0)") 

411 
apply simp 

412 
apply (rule 1) 

413 
apply (rule ext, force, clarify) 

414 
apply (frule setsum_SucD, clarify) 

415 
apply (rename_tac a) 

416 
apply (subgoal_tac "finite {x. (f (a := f a  1)) x > 0}") 

417 
prefer 2 

418 
apply (rule finite_subset) 

419 
prefer 2 

420 
apply assumption 

421 
apply simp 

422 
apply blast 

423 
apply (subgoal_tac "f = (f (a := f a  1))(a := (f (a := f a  1)) a + 1)") 

424 
prefer 2 

425 
apply (rule ext) 

426 
apply (simp (no_asm_simp)) 

427 
apply (erule ssubst, rule 2 [unfolded multiset_def], blast) 

428 
apply (erule allE, erule impE, erule_tac [2] mp, blast) 

429 
apply (simp (no_asm_simp) add: setsum_decr del: fun_upd_apply One_nat_def) 

430 
apply (subgoal_tac "{x. x \<noteq> a > f x \<noteq> 0} = {x. f x \<noteq> 0}") 

431 
prefer 2 

432 
apply blast 

433 
apply (subgoal_tac "{x. x \<noteq> a \<and> f x \<noteq> 0} = {x. f x \<noteq> 0}  {a}") 

434 
prefer 2 

435 
apply blast 

436 
apply (simp add: le_imp_diff_is_add setsum_diff1_nat cong: conj_cong) 

437 
done 

10249  438 

10313  439 
theorem rep_multiset_induct: 
11464  440 
"f \<in> multiset ==> P (\<lambda>a. 0) ==> 
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11655
diff
changeset

441 
(!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1))) ==> P f" 
26178  442 
using rep_multiset_induct_aux by blast 
10249  443 

18258  444 
theorem multiset_induct [case_names empty add, induct type: multiset]: 
26178  445 
assumes empty: "P {#}" 
446 
and add: "!!M x. P M ==> P (M + {#x#})" 

447 
shows "P M" 

10249  448 
proof  
449 
note defns = union_def single_def Mempty_def 

450 
show ?thesis 

451 
apply (rule Rep_multiset_inverse [THEN subst]) 

10313  452 
apply (rule Rep_multiset [THEN rep_multiset_induct]) 
18258  453 
apply (rule empty [unfolded defns]) 
15072  454 
apply (subgoal_tac "f(b := f b + 1) = (\<lambda>a. f a + (if a=b then 1 else 0))") 
10249  455 
prefer 2 
456 
apply (simp add: expand_fun_eq) 

457 
apply (erule ssubst) 

17200  458 
apply (erule Abs_multiset_inverse [THEN subst]) 
26016  459 
apply (drule add [unfolded defns, simplified]) 
460 
apply(simp add:in_multiset) 

10249  461 
done 
462 
qed 

463 

25610  464 
lemma multi_nonempty_split: "M \<noteq> {#} \<Longrightarrow> \<exists>A a. M = A + {#a#}" 
26178  465 
by (induct M) auto 
25610  466 

467 
lemma multiset_cases [cases type, case_names empty add]: 

26178  468 
assumes em: "M = {#} \<Longrightarrow> P" 
469 
assumes add: "\<And>N x. M = N + {#x#} \<Longrightarrow> P" 

470 
shows "P" 

25610  471 
proof (cases "M = {#}") 
26145  472 
assume "M = {#}" then show ?thesis using em by simp 
25610  473 
next 
474 
assume "M \<noteq> {#}" 

475 
then obtain M' m where "M = M' + {#m#}" 

476 
by (blast dest: multi_nonempty_split) 

26145  477 
then show ?thesis using add by simp 
25610  478 
qed 
479 

480 
lemma multi_member_split: "x \<in># M \<Longrightarrow> \<exists>A. M = A + {#x#}" 

26178  481 
apply (cases M) 
482 
apply simp 

483 
apply (rule_tac x="M  {#x#}" in exI, simp) 

484 
done 

25610  485 

26033  486 
lemma multiset_partition: "M = {# x:#M. P x #} + {# x:#M. \<not> P x #}" 
26178  487 
apply (subst multiset_eq_conv_count_eq) 
488 
apply auto 

489 
done 

10249  490 

15869  491 
declare multiset_typedef [simp del] 
10249  492 

25610  493 
lemma multi_drop_mem_not_eq: "c \<in># B \<Longrightarrow> B  {#c#} \<noteq> B" 
26178  494 
by (cases "B = {#}") (auto dest: multi_member_split) 
26145  495 

17161  496 

26016  497 
subsection {* Orderings *} 
10249  498 

499 
subsubsection {* Wellfoundedness *} 

500 

19086  501 
definition 
23751  502 
mult1 :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where 
19086  503 
"mult1 r = 
23751  504 
{(N, M). \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and> 
505 
(\<forall>b. b :# K > (b, a) \<in> r)}" 

10249  506 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21214
diff
changeset

507 
definition 
23751  508 
mult :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where 
509 
"mult r = (mult1 r)\<^sup>+" 

10249  510 

23751  511 
lemma not_less_empty [iff]: "(M, {#}) \<notin> mult1 r" 
26178  512 
by (simp add: mult1_def) 
10249  513 

23751  514 
lemma less_add: "(N, M0 + {#a#}) \<in> mult1 r ==> 
515 
(\<exists>M. (M, M0) \<in> mult1 r \<and> N = M + {#a#}) \<or> 

516 
(\<exists>K. (\<forall>b. b :# K > (b, a) \<in> r) \<and> N = M0 + K)" 

19582  517 
(is "_ \<Longrightarrow> ?case1 (mult1 r) \<or> ?case2") 
10249  518 
proof (unfold mult1_def) 
23751  519 
let ?r = "\<lambda>K a. \<forall>b. b :# K > (b, a) \<in> r" 
11464  520 
let ?R = "\<lambda>N M. \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and> ?r K a" 
23751  521 
let ?case1 = "?case1 {(N, M). ?R N M}" 
10249  522 

23751  523 
assume "(N, M0 + {#a#}) \<in> {(N, M). ?R N M}" 
18258  524 
then have "\<exists>a' M0' K. 
11464  525 
M0 + {#a#} = M0' + {#a'#} \<and> N = M0' + K \<and> ?r K a'" by simp 
18258  526 
then show "?case1 \<or> ?case2" 
10249  527 
proof (elim exE conjE) 
528 
fix a' M0' K 

529 
assume N: "N = M0' + K" and r: "?r K a'" 

530 
assume "M0 + {#a#} = M0' + {#a'#}" 

18258  531 
then have "M0 = M0' \<and> a = a' \<or> 
11464  532 
(\<exists>K'. M0 = K' + {#a'#} \<and> M0' = K' + {#a#})" 
10249  533 
by (simp only: add_eq_conv_ex) 
18258  534 
then show ?thesis 
10249  535 
proof (elim disjE conjE exE) 
536 
assume "M0 = M0'" "a = a'" 

11464  537 
with N r have "?r K a \<and> N = M0 + K" by simp 
18258  538 
then have ?case2 .. then show ?thesis .. 
10249  539 
next 
540 
fix K' 

541 
assume "M0' = K' + {#a#}" 

542 
with N have n: "N = K' + K + {#a#}" by (simp add: union_ac) 

543 

544 
assume "M0 = K' + {#a'#}" 

545 
with r have "?R (K' + K) M0" by blast 

18258  546 
with n have ?case1 by simp then show ?thesis .. 
10249  547 
qed 
548 
qed 

549 
qed 

550 

23751  551 
lemma all_accessible: "wf r ==> \<forall>M. M \<in> acc (mult1 r)" 
10249  552 
proof 
553 
let ?R = "mult1 r" 

554 
let ?W = "acc ?R" 

555 
{ 

556 
fix M M0 a 

23751  557 
assume M0: "M0 \<in> ?W" 
558 
and wf_hyp: "!!b. (b, a) \<in> r ==> (\<forall>M \<in> ?W. M + {#b#} \<in> ?W)" 

559 
and acc_hyp: "\<forall>M. (M, M0) \<in> ?R > M + {#a#} \<in> ?W" 

560 
have "M0 + {#a#} \<in> ?W" 

561 
proof (rule accI [of "M0 + {#a#}"]) 

10249  562 
fix N 
23751  563 
assume "(N, M0 + {#a#}) \<in> ?R" 
564 
then have "((\<exists>M. (M, M0) \<in> ?R \<and> N = M + {#a#}) \<or> 

565 
(\<exists>K. (\<forall>b. b :# K > (b, a) \<in> r) \<and> N = M0 + K))" 

10249  566 
by (rule less_add) 
23751  567 
then show "N \<in> ?W" 
10249  568 
proof (elim exE disjE conjE) 
23751  569 
fix M assume "(M, M0) \<in> ?R" and N: "N = M + {#a#}" 
570 
from acc_hyp have "(M, M0) \<in> ?R > M + {#a#} \<in> ?W" .. 

571 
from this and `(M, M0) \<in> ?R` have "M + {#a#} \<in> ?W" .. 

572 
then show "N \<in> ?W" by (simp only: N) 

10249  573 
next 
574 
fix K 

575 
assume N: "N = M0 + K" 

23751  576 
assume "\<forall>b. b :# K > (b, a) \<in> r" 
577 
then have "M0 + K \<in> ?W" 

10249  578 
proof (induct K) 
18730  579 
case empty 
23751  580 
from M0 show "M0 + {#} \<in> ?W" by simp 
18730  581 
next 
582 
case (add K x) 

23751  583 
from add.prems have "(x, a) \<in> r" by simp 
584 
with wf_hyp have "\<forall>M \<in> ?W. M + {#x#} \<in> ?W" by blast 

585 
moreover from add have "M0 + K \<in> ?W" by simp 

586 
ultimately have "(M0 + K) + {#x#} \<in> ?W" .. 

587 
then show "M0 + (K + {#x#}) \<in> ?W" by (simp only: union_assoc) 

10249  588 
qed 
23751  589 
then show "N \<in> ?W" by (simp only: N) 
10249  590 
qed 
591 
qed 

592 
} note tedious_reasoning = this 

593 

23751  594 
assume wf: "wf r" 
10249  595 
fix M 
23751  596 
show "M \<in> ?W" 
10249  597 
proof (induct M) 
23751  598 
show "{#} \<in> ?W" 
10249  599 
proof (rule accI) 
23751  600 
fix b assume "(b, {#}) \<in> ?R" 
601 
with not_less_empty show "b \<in> ?W" by contradiction 

10249  602 
qed 
603 

23751  604 
fix M a assume "M \<in> ?W" 
605 
from wf have "\<forall>M \<in> ?W. M + {#a#} \<in> ?W" 

10249  606 
proof induct 
607 
fix a 

23751  608 
assume r: "!!b. (b, a) \<in> r ==> (\<forall>M \<in> ?W. M + {#b#} \<in> ?W)" 
609 
show "\<forall>M \<in> ?W. M + {#a#} \<in> ?W" 

10249  610 
proof 
23751  611 
fix M assume "M \<in> ?W" 
612 
then show "M + {#a#} \<in> ?W" 

23373  613 
by (rule acc_induct) (rule tedious_reasoning [OF _ r]) 
10249  614 
qed 
615 
qed 

23751  616 
from this and `M \<in> ?W` show "M + {#a#} \<in> ?W" .. 
10249  617 
qed 
618 
qed 

619 

23751  620 
theorem wf_mult1: "wf r ==> wf (mult1 r)" 
26178  621 
by (rule acc_wfI) (rule all_accessible) 
10249  622 

23751  623 
theorem wf_mult: "wf r ==> wf (mult r)" 
26178  624 
unfolding mult_def by (rule wf_trancl) (rule wf_mult1) 
10249  625 

626 

627 
subsubsection {* Closurefree presentation *} 

628 

629 
(*Badly needed: a linear arithmetic procedure for multisets*) 

630 

631 
lemma diff_union_single_conv: "a :# J ==> I + J  {#a#} = I + (J  {#a#})" 

26178  632 
by (simp add: multiset_eq_conv_count_eq) 
10249  633 

634 
text {* One direction. *} 

635 

636 
lemma mult_implies_one_step: 

23751  637 
"trans r ==> (M, N) \<in> mult r ==> 
11464  638 
\<exists>I J K. N = I + J \<and> M = I + K \<and> J \<noteq> {#} \<and> 
23751  639 
(\<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r)" 
26178  640 
apply (unfold mult_def mult1_def set_of_def) 
641 
apply (erule converse_trancl_induct, clarify) 

642 
apply (rule_tac x = M0 in exI, simp, clarify) 

643 
apply (case_tac "a :# K") 

644 
apply (rule_tac x = I in exI) 

645 
apply (simp (no_asm)) 

646 
apply (rule_tac x = "(K  {#a#}) + Ka" in exI) 

647 
apply (simp (no_asm_simp) add: union_assoc [symmetric]) 

648 
apply (drule_tac f = "\<lambda>M. M  {#a#}" in arg_cong) 

649 
apply (simp add: diff_union_single_conv) 

650 
apply (simp (no_asm_use) add: trans_def) 

651 
apply blast 

652 
apply (subgoal_tac "a :# I") 

653 
apply (rule_tac x = "I  {#a#}" in exI) 

654 
apply (rule_tac x = "J + {#a#}" in exI) 

655 
apply (rule_tac x = "K + Ka" in exI) 

656 
apply (rule conjI) 

657 
apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split) 

658 
apply (rule conjI) 

659 
apply (drule_tac f = "\<lambda>M. M  {#a#}" in arg_cong, simp) 

660 
apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split) 

661 
apply (simp (no_asm_use) add: trans_def) 

662 
apply blast 

663 
apply (subgoal_tac "a :# (M0 + {#a#})") 

664 
apply simp 

665 
apply (simp (no_asm)) 

666 
done 

10249  667 

668 
lemma elem_imp_eq_diff_union: "a :# M ==> M = M  {#a#} + {#a#}" 

26178  669 
by (simp add: multiset_eq_conv_count_eq) 
10249  670 

11464  671 
lemma size_eq_Suc_imp_eq_union: "size M = Suc n ==> \<exists>a N. M = N + {#a#}" 
26178  672 
apply (erule size_eq_Suc_imp_elem [THEN exE]) 
673 
apply (drule elem_imp_eq_diff_union, auto) 

674 
done 

10249  675 

676 
lemma one_step_implies_mult_aux: 

23751  677 
"trans r ==> 
678 
\<forall>I J K. (size J = n \<and> J \<noteq> {#} \<and> (\<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r)) 

679 
> (I + K, I + J) \<in> mult r" 

26178  680 
apply (induct_tac n, auto) 
681 
apply (frule size_eq_Suc_imp_eq_union, clarify) 

682 
apply (rename_tac "J'", simp) 

683 
apply (erule notE, auto) 

684 
apply (case_tac "J' = {#}") 

685 
apply (simp add: mult_def) 

686 
apply (rule r_into_trancl) 

687 
apply (simp add: mult1_def set_of_def, blast) 

688 
txt {* Now we know @{term "J' \<noteq> {#}"}. *} 

689 
apply (cut_tac M = K and P = "\<lambda>x. (x, a) \<in> r" in multiset_partition) 

690 
apply (erule_tac P = "\<forall>k \<in> set_of K. ?P k" in rev_mp) 

691 
apply (erule ssubst) 

692 
apply (simp add: Ball_def, auto) 

693 
apply (subgoal_tac 

694 
"((I + {# x :# K. (x, a) \<in> r #}) + {# x :# K. (x, a) \<notin> r #}, 

695 
(I + {# x :# K. (x, a) \<in> r #}) + J') \<in> mult r") 

696 
prefer 2 

697 
apply force 

698 
apply (simp (no_asm_use) add: union_assoc [symmetric] mult_def) 

699 
apply (erule trancl_trans) 

700 
apply (rule r_into_trancl) 

701 
apply (simp add: mult1_def set_of_def) 

702 
apply (rule_tac x = a in exI) 

703 
apply (rule_tac x = "I + J'" in exI) 

704 
apply (simp add: union_ac) 

705 
done 

10249  706 

17161  707 
lemma one_step_implies_mult: 
23751  708 
"trans r ==> J \<noteq> {#} ==> \<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r 
709 
==> (I + K, I + J) \<in> mult r" 

26178  710 
using one_step_implies_mult_aux by blast 
10249  711 

712 

713 
subsubsection {* Partialorder properties *} 

714 

12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11868
diff
changeset

715 
instance multiset :: (type) ord .. 
10249  716 

717 
defs (overloaded) 

23751  718 
less_multiset_def: "M' < M == (M', M) \<in> mult {(x', x). x' < x}" 
11464  719 
le_multiset_def: "M' <= M == M' = M \<or> M' < (M::'a multiset)" 
10249  720 

23751  721 
lemma trans_base_order: "trans {(x', x). x' < (x::'a::order)}" 
26178  722 
unfolding trans_def by (blast intro: order_less_trans) 
10249  723 

724 
text {* 

725 
\medskip Irreflexivity. 

726 
*} 

727 

728 
lemma mult_irrefl_aux: 

26178  729 
"finite A ==> (\<forall>x \<in> A. \<exists>y \<in> A. x < (y::'a::order)) \<Longrightarrow> A = {}" 
730 
by (induct rule: finite_induct) (auto intro: order_less_trans) 

10249  731 

17161  732 
lemma mult_less_not_refl: "\<not> M < (M::'a::order multiset)" 
26178  733 
apply (unfold less_multiset_def, auto) 
734 
apply (drule trans_base_order [THEN mult_implies_one_step], auto) 

735 
apply (drule finite_set_of [THEN mult_irrefl_aux [rule_format (no_asm)]]) 

736 
apply (simp add: set_of_eq_empty_iff) 

737 
done 

10249  738 

739 
lemma mult_less_irrefl [elim!]: "M < (M::'a::order multiset) ==> R" 

26178  740 
using insert mult_less_not_refl by fast 
10249  741 

742 

743 
text {* Transitivity. *} 

744 

745 
theorem mult_less_trans: "K < M ==> M < N ==> K < (N::'a::order multiset)" 

26178  746 
unfolding less_multiset_def mult_def by (blast intro: trancl_trans) 
10249  747 

748 
text {* Asymmetry. *} 

749 

11464  750 
theorem mult_less_not_sym: "M < N ==> \<not> N < (M::'a::order multiset)" 
26178  751 
apply auto 
752 
apply (rule mult_less_not_refl [THEN notE]) 

753 
apply (erule mult_less_trans, assumption) 

754 
done 

10249  755 

756 
theorem mult_less_asym: 

26178  757 
"M < N ==> (\<not> P ==> N < (M::'a::order multiset)) ==> P" 
758 
using mult_less_not_sym by blast 

10249  759 

760 
theorem mult_le_refl [iff]: "M <= (M::'a::order multiset)" 

26178  761 
unfolding le_multiset_def by auto 
10249  762 

763 
text {* Antisymmetry. *} 

764 

765 
theorem mult_le_antisym: 

26178  766 
"M <= N ==> N <= M ==> M = (N::'a::order multiset)" 
767 
unfolding le_multiset_def by (blast dest: mult_less_not_sym) 

10249  768 

769 
text {* Transitivity. *} 

770 

771 
theorem mult_le_trans: 

26178  772 
"K <= M ==> M <= N ==> K <= (N::'a::order multiset)" 
773 
unfolding le_multiset_def by (blast intro: mult_less_trans) 

10249  774 

11655  775 
theorem mult_less_le: "(M < N) = (M <= N \<and> M \<noteq> (N::'a::order multiset))" 
26178  776 
unfolding le_multiset_def by auto 
10249  777 

10277  778 
text {* Partial order. *} 
779 

780 
instance multiset :: (order) order 

26178  781 
apply intro_classes 
782 
apply (rule mult_less_le) 

783 
apply (rule mult_le_refl) 

784 
apply (erule mult_le_trans, assumption) 

785 
apply (erule mult_le_antisym, assumption) 

786 
done 

10277  787 

10249  788 

789 
subsubsection {* Monotonicity of multiset union *} 

790 

17161  791 
lemma mult1_union: 
26178  792 
"(B, D) \<in> mult1 r ==> trans r ==> (C + B, C + D) \<in> mult1 r" 
793 
apply (unfold mult1_def) 

794 
apply auto 

795 
apply (rule_tac x = a in exI) 

796 
apply (rule_tac x = "C + M0" in exI) 

797 
apply (simp add: union_assoc) 

798 
done 

10249  799 

800 
lemma union_less_mono2: "B < D ==> C + B < C + (D::'a::order multiset)" 

26178  801 
apply (unfold less_multiset_def mult_def) 
802 
apply (erule trancl_induct) 

803 
apply (blast intro: mult1_union transI order_less_trans r_into_trancl) 

804 
apply (blast intro: mult1_union transI order_less_trans r_into_trancl trancl_trans) 

805 
done 

10249  806 

807 
lemma union_less_mono1: "B < D ==> B + C < D + (C::'a::order multiset)" 

26178  808 
apply (subst union_commute [of B C]) 
809 
apply (subst union_commute [of D C]) 

810 
apply (erule union_less_mono2) 

811 
done 

10249  812 

17161  813 
lemma union_less_mono: 
26178  814 
"A < C ==> B < D ==> A + B < C + (D::'a::order multiset)" 
815 
by (blast intro!: union_less_mono1 union_less_mono2 mult_less_trans) 

10249  816 

17161  817 
lemma union_le_mono: 
26178  818 
"A <= C ==> B <= D ==> A + B <= C + (D::'a::order multiset)" 
819 
unfolding le_multiset_def 

820 
by (blast intro: union_less_mono union_less_mono1 union_less_mono2) 

10249  821 

17161  822 
lemma empty_leI [iff]: "{#} <= (M::'a::order multiset)" 
26178  823 
apply (unfold le_multiset_def less_multiset_def) 
824 
apply (case_tac "M = {#}") 

825 
prefer 2 

826 
apply (subgoal_tac "({#} + {#}, {#} + M) \<in> mult (Collect (split op <))") 

827 
prefer 2 

828 
apply (rule one_step_implies_mult) 

829 
apply (simp only: trans_def) 

830 
apply auto 

831 
done 

10249  832 

17161  833 
lemma union_upper1: "A <= A + (B::'a::order multiset)" 
15072  834 
proof  
17200  835 
have "A + {#} <= A + B" by (blast intro: union_le_mono) 
18258  836 
then show ?thesis by simp 
15072  837 
qed 
838 

17161  839 
lemma union_upper2: "B <= A + (B::'a::order multiset)" 
26178  840 
by (subst union_commute) (rule union_upper1) 
15072  841 

23611  842 
instance multiset :: (order) pordered_ab_semigroup_add 
26178  843 
apply intro_classes 
844 
apply (erule union_le_mono[OF mult_le_refl]) 

845 
done 

26145  846 

15072  847 

17200  848 
subsection {* Link with lists *} 
15072  849 

26016  850 
primrec multiset_of :: "'a list \<Rightarrow> 'a multiset" where 
26145  851 
"multiset_of [] = {#}"  
852 
"multiset_of (a # x) = multiset_of x + {# a #}" 

15072  853 

854 
lemma multiset_of_zero_iff[simp]: "(multiset_of x = {#}) = (x = [])" 

26178  855 
by (induct x) auto 
15072  856 

857 
lemma multiset_of_zero_iff_right[simp]: "({#} = multiset_of x) = (x = [])" 

26178  858 
by (induct x) auto 
15072  859 

860 
lemma set_of_multiset_of[simp]: "set_of(multiset_of x) = set x" 

26178  861 
by (induct x) auto 
15867  862 

863 
lemma mem_set_multiset_eq: "x \<in> set xs = (x :# multiset_of xs)" 

26178  864 
by (induct xs) auto 
15072  865 

18258  866 
lemma multiset_of_append [simp]: 
26178  867 
"multiset_of (xs @ ys) = multiset_of xs + multiset_of ys" 
868 
by (induct xs arbitrary: ys) (auto simp: union_ac) 

18730  869 

15072  870 
lemma surj_multiset_of: "surj multiset_of" 
26178  871 
apply (unfold surj_def) 
872 
apply (rule allI) 

873 
apply (rule_tac M = y in multiset_induct) 

874 
apply auto 

875 
apply (rule_tac x = "x # xa" in exI) 

876 
apply auto 

877 
done 

10249  878 

25162  879 
lemma set_count_greater_0: "set x = {a. count (multiset_of x) a > 0}" 
26178  880 
by (induct x) auto 
15072  881 

17200  882 
lemma distinct_count_atmost_1: 
26178  883 
"distinct x = (! a. count (multiset_of x) a = (if a \<in> set x then 1 else 0))" 
884 
apply (induct x, simp, rule iffI, simp_all) 

885 
apply (rule conjI) 

886 
apply (simp_all add: set_of_multiset_of [THEN sym] del: set_of_multiset_of) 

887 
apply (erule_tac x = a in allE, simp, clarify) 

888 
apply (erule_tac x = aa in allE, simp) 

889 
done 

15072  890 

17200  891 
lemma multiset_of_eq_setD: 
15867  892 
"multiset_of xs = multiset_of ys \<Longrightarrow> set xs = set ys" 
26178  893 
by (rule) (auto simp add:multiset_eq_conv_count_eq set_count_greater_0) 
15867  894 

17200  895 
lemma set_eq_iff_multiset_of_eq_distinct: 
26145  896 
"distinct x \<Longrightarrow> distinct y \<Longrightarrow> 
897 
(set x = set y) = (multiset_of x = multiset_of y)" 

26178  898 
by (auto simp: multiset_eq_conv_count_eq distinct_count_atmost_1) 
15072  899 

17200  900 
lemma set_eq_iff_multiset_of_remdups_eq: 
15072  901 
"(set x = set y) = (multiset_of (remdups x) = multiset_of (remdups y))" 
26178  902 
apply (rule iffI) 
903 
apply (simp add: set_eq_iff_multiset_of_eq_distinct[THEN iffD1]) 

904 
apply (drule distinct_remdups [THEN distinct_remdups 

26145  905 
[THEN set_eq_iff_multiset_of_eq_distinct [THEN iffD2]]]) 
26178  906 
apply simp 
907 
done 

10249  908 

18258  909 
lemma multiset_of_compl_union [simp]: 
26178  910 
"multiset_of [x\<leftarrow>xs. P x] + multiset_of [x\<leftarrow>xs. \<not>P x] = multiset_of xs" 
911 
by (induct xs) (auto simp: union_ac) 

15072  912 

17200  913 
lemma count_filter: 
26178  914 
"count (multiset_of xs) x = length [y \<leftarrow> xs. y = x]" 
915 
by (induct xs) auto 

15867  916 

26143
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

917 
lemma nth_mem_multiset_of: "i < length ls \<Longrightarrow> (ls ! i) :# multiset_of ls" 
26178  918 
apply (induct ls arbitrary: i) 
919 
apply simp 

920 
apply (case_tac i) 

921 
apply auto 

922 
done 

26143
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

923 

314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

924 
lemma multiset_of_remove1: "multiset_of (remove1 a xs) = multiset_of xs  {#a#}" 
26178  925 
by (induct xs) (auto simp add: multiset_eq_conv_count_eq) 
26143
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

926 

314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

927 
lemma multiset_of_eq_length: 
26178  928 
assumes "multiset_of xs = multiset_of ys" 
929 
shows "length xs = length ys" 

930 
using assms 

26143
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

931 
proof (induct arbitrary: ys rule: length_induct) 
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

932 
case (1 xs ys) 
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

933 
show ?case 
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

934 
proof (cases xs) 
26145  935 
case Nil with "1.prems" show ?thesis by simp 
26143
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

936 
next 
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

937 
case (Cons x xs') 
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

938 
note xCons = Cons 
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

939 
show ?thesis 
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

940 
proof (cases ys) 
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

941 
case Nil 
26145  942 
with "1.prems" Cons show ?thesis by simp 
26143
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

943 
next 
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

944 
case (Cons y ys') 
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

945 
have x_in_ys: "x = y \<or> x \<in> set ys'" 
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

946 
proof (cases "x = y") 
26145  947 
case True then show ?thesis .. 
26143
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

948 
next 
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

949 
case False 
26145  950 
from "1.prems" [symmetric] xCons Cons have "x :# multiset_of ys' + {#y#}" by simp 
26143
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

951 
with False show ?thesis by (simp add: mem_set_multiset_eq) 
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

952 
qed 
26145  953 
from "1.hyps" have IH: "length xs' < length xs \<longrightarrow> 
954 
(\<forall>x. multiset_of xs' = multiset_of x \<longrightarrow> length xs' = length x)" by blast 

955 
from "1.prems" x_in_ys Cons xCons have "multiset_of xs' = multiset_of (remove1 x (y#ys'))" 

26143
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

956 
apply  
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

957 
apply (simp add: multiset_of_remove1, simp only: add_eq_conv_diff) 
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

958 
apply fastsimp 
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

959 
done 
26145  960 
with IH xCons have IH': "length xs' = length (remove1 x (y#ys'))" by fastsimp 
961 
from x_in_ys have "x \<noteq> y \<Longrightarrow> length ys' > 0" by auto 

26143
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

962 
with Cons xCons x_in_ys IH' show ?thesis by (auto simp add: length_remove1) 
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

963 
qed 
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

964 
qed 
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

965 
qed 
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

966 

26145  967 
text {* 
968 
This lemma shows which properties suffice to show that a function 

969 
@{text "f"} with @{text "f xs = ys"} behaves like sort. 

970 
*} 

971 
lemma properties_for_sort: 

972 
"multiset_of ys = multiset_of xs \<Longrightarrow> sorted ys \<Longrightarrow> sort xs = ys" 

26143
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

973 
proof (induct xs arbitrary: ys) 
26145  974 
case Nil then show ?case by simp 
26143
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

975 
next 
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

976 
case (Cons x xs) 
26145  977 
then have "x \<in> set ys" 
978 
by (auto simp add: mem_set_multiset_eq intro!: ccontr) 

26143
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

979 
with Cons.prems Cons.hyps [of "remove1 x ys"] show ?case 
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

980 
by (simp add: sorted_remove1 multiset_of_remove1 insort_remove1) 
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

981 
qed 
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

982 

15867  983 

15072  984 
subsection {* Pointwise ordering induced by count *} 
985 

19086  986 
definition 
25610  987 
mset_le :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<le>#" 50) where 
988 
"(A \<le># B) = (\<forall>a. count A a \<le> count B a)" 

26145  989 

23611  990 
definition 
25610  991 
mset_less :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<#" 50) where 
992 
"(A <# B) = (A \<le># B \<and> A \<noteq> B)" 

993 

26145  994 
notation mset_le (infix "\<subseteq>#" 50) 
995 
notation mset_less (infix "\<subset>#" 50) 

15072  996 

23611  997 
lemma mset_le_refl[simp]: "A \<le># A" 
26178  998 
unfolding mset_le_def by auto 
15072  999 

26145  1000 
lemma mset_le_trans: "A \<le># B \<Longrightarrow> B \<le># C \<Longrightarrow> A \<le># C" 
26178  1001 
unfolding mset_le_def by (fast intro: order_trans) 
15072  1002 

26145  1003 
lemma mset_le_antisym: "A \<le># B \<Longrightarrow> B \<le># A \<Longrightarrow> A = B" 
26178  1004 
apply (unfold mset_le_def) 
1005 
apply (rule multiset_eq_conv_count_eq [THEN iffD2]) 

1006 
apply (blast intro: order_antisym) 

1007 
done 

15072  1008 

26145  1009 
lemma mset_le_exists_conv: "(A \<le># B) = (\<exists>C. B = A + C)" 
26178  1010 
apply (unfold mset_le_def, rule iffI, rule_tac x = "B  A" in exI) 
1011 
apply (auto intro: multiset_eq_conv_count_eq [THEN iffD2]) 

1012 
done 

15072  1013 

23611  1014 
lemma mset_le_mono_add_right_cancel[simp]: "(A + C \<le># B + C) = (A \<le># B)" 
26178  1015 
unfolding mset_le_def by auto 
15072  1016 

23611  1017 
lemma mset_le_mono_add_left_cancel[simp]: "(C + A \<le># C + B) = (A \<le># B)" 
26178  1018 
unfolding mset_le_def by auto 
15072  1019 

23611  1020 
lemma mset_le_mono_add: "\<lbrakk> A \<le># B; C \<le># D \<rbrakk> \<Longrightarrow> A + C \<le># B + D" 
26178  1021 
apply (unfold mset_le_def) 
1022 
apply auto 

1023 
apply (erule_tac x = a in allE)+ 

1024 
apply auto 

1025 
done 

15072  1026 

23611  1027 
lemma mset_le_add_left[simp]: "A \<le># A + B" 
26178  1028 
unfolding mset_le_def by auto 
15072  1029 

23611  1030 
lemma mset_le_add_right[simp]: "B \<le># A + B" 
26178  1031 
unfolding mset_le_def by auto 
15072  1032 

26143
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

1033 
lemma mset_le_single: "a :# B \<Longrightarrow> {#a#} \<le># B" 
26178  1034 
by (simp add: mset_le_def) 
26143
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

1035 

314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

1036 
lemma multiset_diff_union_assoc: "C \<le># B \<Longrightarrow> A + B  C = A + (B  C)" 
26178  1037 
by (simp add: multiset_eq_conv_count_eq mset_le_def) 
26143
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

1038 

314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

1039 
lemma mset_le_multiset_union_diff_commute: 
26178  1040 
assumes "B \<le># A" 
1041 
shows "A  B + C = A + C  B" 

26143
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

1042 
proof  
26145  1043 
from mset_le_exists_conv [of "B" "A"] assms have "\<exists>D. A = B + D" .. 
1044 
from this obtain D where "A = B + D" .. 

1045 
then show ?thesis 

1046 
apply simp 

1047 
apply (subst union_commute) 

1048 
apply (subst multiset_diff_union_assoc) 

1049 
apply simp 

1050 
apply (simp add: diff_cancel) 

1051 
apply (subst union_assoc) 

1052 
apply (subst union_commute[of "B" _]) 

1053 
apply (subst multiset_diff_union_assoc) 

1054 
apply simp 

1055 
apply (simp add: diff_cancel) 

1056 
done 

26143
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

1057 
qed 
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

1058 

23611  1059 
lemma multiset_of_remdups_le: "multiset_of (remdups xs) \<le># multiset_of xs" 
26178  1060 
apply (induct xs) 
1061 
apply auto 

1062 
apply (rule mset_le_trans) 

1063 
apply auto 

1064 
done 

23611  1065 

26145  1066 
lemma multiset_of_update: 
1067 
"i < length ls \<Longrightarrow> multiset_of (ls[i := v]) = multiset_of ls  {#ls ! i#} + {#v#}" 

26143
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

1068 
proof (induct ls arbitrary: i) 
26145  1069 
case Nil then show ?case by simp 
26143
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

1070 
next 
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

1071 
case (Cons x xs) 
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

1072 
show ?case 
26145  1073 
proof (cases i) 
1074 
case 0 then show ?thesis by simp 

1075 
next 

1076 
case (Suc i') 

1077 
with Cons show ?thesis 

1078 
apply simp 

1079 
apply (subst union_assoc) 

1080 
apply (subst union_commute [where M = "{#v#}" and N = "{#x#}"]) 

1081 
apply (subst union_assoc [symmetric]) 

1082 
apply simp 

1083 
apply (rule mset_le_multiset_union_diff_commute) 

1084 
apply (simp add: mset_le_single nth_mem_multiset_of) 

1085 
done 

26143
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

1086 
qed 
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

1087 
qed 
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

1088 

26145  1089 
lemma multiset_of_swap: 
1090 
"i < length ls \<Longrightarrow> j < length ls \<Longrightarrow> 

1091 
multiset_of (ls[j := ls ! i, i := ls ! j]) = multiset_of ls" 

26178  1092 
apply (case_tac "i = j") 
1093 
apply simp 

1094 
apply (simp add: multiset_of_update) 

1095 
apply (subst elem_imp_eq_diff_union[symmetric]) 

1096 
apply (simp add: nth_mem_multiset_of) 

1097 
apply simp 

1098 
done 

26143
314c0bcb7df7
Added useful general lemmas from the work with the HeapMonad
bulwahn
parents:
26033
diff
changeset

1099 

26145  1100 
interpretation mset_order: order ["op \<le>#" "op <#"] 
26178  1101 
by (auto intro: order.intro mset_le_refl mset_le_antisym 
25208  1102 
mset_le_trans simp: mset_less_def) 
23611  1103 

1104 
interpretation mset_order_cancel_semigroup: 

26145  1105 
pordered_cancel_ab_semigroup_add ["op +" "op \<le>#" "op <#"] 
26178  1106 
by unfold_locales (erule mset_le_mono_add [OF mset_le_refl]) 
23611  1107 

1108 
interpretation mset_order_semigroup_cancel: 

26145  1109 
pordered_ab_semigroup_add_imp_le ["op +" "op \<le>#" "op <#"] 
26178  1110 
by (unfold_locales) simp 
15072  1111 

25610  1112 

26145  1113 
lemma mset_lessD: "A \<subset># B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B" 
26178  1114 
apply (clarsimp simp: mset_le_def mset_less_def) 
1115 
apply (erule_tac x=x in allE) 

1116 
apply auto 

1117 
done 

25610  1118 

26145  1119 
lemma mset_leD: "A \<subseteq># B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B" 
26178  1120 
apply (clarsimp simp: mset_le_def mset_less_def) 
1121 
apply (erule_tac x = x in allE) 

1122 
apply auto 

1123 
done 

25610  1124 

26145  1125 
lemma mset_less_insertD: "(A + {#x#} \<subset># B) \<Longrightarrow> (x \<in># B \<and> A \<subset># B)" 
26178  1126 
apply (rule conjI) 
1127 
apply (simp add: mset_lessD) 

1128 
apply (clarsimp simp: mset_le_def mset_less_def) 

1129 
apply safe 

1130 
apply (erule_tac x = a in allE) 

1131 
apply (auto split: split_if_asm) 

1132 
done 

25610  1133 

26145  1134 
lemma mset_le_insertD: "(A + {#x#} \<subseteq># B) \<Longrightarrow> (x \<in># B \<and> A \<subseteq># B)" 
26178  1135 
apply (rule conjI) 
1136 
apply (simp add: mset_leD) 

1137 
apply (force simp: mset_le_def mset_less_def split: split_if_asm) 

1138 
done 

25610  1139 

1140 
lemma mset_less_of_empty[simp]: "A \<subset># {#} = False" 

26178  1141 
by (induct A) (auto simp: mset_le_def mset_less_def) 
25610  1142 

1143 
lemma multi_psub_of_add_self[simp]: "A \<subset># A + {#x#}" 

26178  1144 
by (auto simp: mset_le_def mset_less_def) 
25610  1145 

1146 
lemma multi_psub_self[simp]: "A \<subset># A = False" 

26178  1147 
by (auto simp: mset_le_def mset_less_def) 
25610  1148 

1149 
lemma mset_less_add_bothsides: 

1150 
"T + {#x#} \<subset># S + {#x#} \<Longrightarrow> T \<subset># S" 

26178  1151 
by (auto simp: mset_le_def mset_less_def) 
25610  1152 

1153 
lemma mset_less_empty_nonempty: "({#} \<subset># S) = (S \<noteq> {#})" 

26178  1154 
by (auto simp: mset_le_def mset_less_def) 
25610  1155 

1156 
lemma mset_less_size: "A \<subset># B \<Longrightarrow> size A < size B" 

1157 
proof (induct A arbitrary: B) 

1158 
case (empty M) 

26145  1159 
then have "M \<noteq> {#}" by (simp add: mset_less_empty_nonempty) 
25610  1160 
then obtain M' x where "M = M' + {#x#}" 
1161 
by (blast dest: multi_nonempty_split) 

26145  1162 
then show ?case by simp 
25610  1163 
next 
1164 
case (add S x T) 

1165 
have IH: "\<And>B. S \<subset># B \<Longrightarrow> size S < size B" by fact 

1166 
have SxsubT: "S + {#x#} \<subset># T" by fact 

26145  1167 
then have "x \<in># T" and "S \<subset># T" by (auto dest: mset_less_insertD) 
25610  1168 
then obtain T' where T: "T = T' + {#x#}" 
1169 
by (blast dest: multi_member_split) 

26145  1170 
then have "S \<subset># T'" using SxsubT 
25610  1171 
by (blast intro: mset_less_add_bothsides) 
26145  1172 
then have "size S < size T'" using IH by simp 
1173 
then show ?case using T by simp 

25610  1174 
qed 
1175 

1176 
lemmas mset_less_trans = mset_order.less_eq_less.less_trans 

1177 

1178 
lemma mset_less_diff_self: "c \<in># B \<Longrightarrow> B  {#c#} \<subset># B" 

26178  1179 
by (auto simp: mset_le_def mset_less_def multi_drop_mem_not_eq) 
25610  1180 

26145  1181 

25610  1182 
subsection {* Strong induction and subset induction for multisets *} 
1183 

26016  1184 
text {* Wellfoundedness of proper subset operator: *} 
25610  1185 

26145  1186 
text {* proper multiset subset *} 
25610  1187 
definition 
26145  1188 
mset_less_rel :: "('a multiset * 'a multiset) set" where 
1189 
"mset_less_rel = {(A,B). A \<subset># B}" 

25610  1190 

1191 
lemma multiset_add_sub_el_shuffle: 

26145  1192 
assumes "c \<in># B" and "b \<noteq> c" 
25610  1193 
shows "B  {#c#} + {#b#} = B + {#b#}  {#c#}" 
1194 
proof  

26145  1195 
from `c \<in># B` obtain A where B: "B = A + {#c#}" 
25610  1196 
by (blast dest: multi_member_split) 
1197 
have "A + {#b#} = A + {#b#} + {#c#}  {#c#}" by simp 

26145  1198 
then have "A + {#b#} = A + {#c#} + {#b#}  {#c#}" 
25610  1199 
by (simp add: union_ac) 
26145  1200 
then show ?thesis using B by simp 
25610  1201 
qed 
1202 

1203 
lemma wf_mset_less_rel: "wf mset_less_rel" 

26178  1204 
apply (unfold mset_less_rel_def) 
1205 
apply (rule wf_measure [THEN wf_subset, where f1=size]) 

1206 
apply (clarsimp simp: measure_def inv_image_def mset_less_size) 

1207 
done 

25610  1208 

26016  1209 
text {* The induction rules: *} 
25610  1210 

1211 
lemma full_multiset_induct [case_names less]: 

26178  1212 
assumes ih: "\<And>B. \<forall>A. A \<subset># B \<longrightarrow> P A \<Longrightarrow> P B" 
1213 
shows "P B" 

1214 
apply (rule wf_mset_less_rel [THEN wf_induct]) 

1215 
apply (rule ih, auto simp: mset_less_rel_def) 

1216 
done 

25610  1217 

1218 
lemma multi_subset_induct [consumes 2, case_names empty add]: 

26178  1219 
assumes "F \<subseteq># A" 
1220 
and empty: "P {#}" 

1221 
and insert: "\<And>a F. a \<in># A \<Longrightarrow> P F \<Longrightarrow> P (F + {#a#})" 

1222 
shows "P F" 

25610  1223 
proof  
1224 
from `F \<subseteq># A` 

1225 
show ?thesis 

1226 
proof (induct F) 

1227 
show "P {#}" by fact 

1228 
next 

1229 
fix x F 

1230 
assume P: "F \<subseteq># A \<Longrightarrow> P F" and i: "F + {#x#} \<subseteq># A" 

1231 
show "P (F + {#x#})" 

1232 
proof (rule insert) 

1233 
from i show "x \<in># A" by (auto dest: mset_le_insertD) 

26145  1234 
from i have "F \<subseteq># A" by (auto dest: mset_le_insertD) 
25610  1235 
with P show "P F" . 
1236 
qed 

1237 
qed 

1238 
qed 

1239 

26016  1240 
text{* A consequence: Extensionality. *} 
25610  1241 

26145  1242 
lemma multi_count_eq: "(\<forall>x. count A x = count B x) = (A = B)" 
26178  1243 
apply (rule iffI) 
1244 
prefer 2 

1245 
apply clarsimp 

1246 
apply (induct A arbitrary: B rule: full_multiset_induct) 

1247 
apply (rename_tac C) 

1248 
apply (case_tac B rule: multiset_cases) 

1249 
apply (simp add: empty_multiset_count) 

1250 
apply simp 

1251 
apply (case_tac "x \<in># C") 

1252 
apply (force dest: multi_member_split) 

1253 
apply (erule_tac x = x in allE) 

1254 
apply simp 

1255 
done 

25610  1256 

1257 
lemmas multi_count_ext = multi_count_eq [THEN iffD1, rule_format] 

1258 

26145  1259 

25610  1260 
subsection {* The fold combinator *} 
1261 

26145  1262 
text {* 
1263 
The intended behaviour is 

1264 
@{text "fold_mset f z {#x\<^isub>1, ..., x\<^isub>n#} = f x\<^isub>1 (\<dots> (f x\<^isub>n z)\<dots>)"} 

1265 
if @{text f} is associativecommutative. 

25610  1266 
*} 
1267 

26145  1268 
text {* 
1269 
The graph of @{text "fold_mset"}, @{text "z"}: the start element, 

1270 
@{text "f"}: folding function, @{text "A"}: the multiset, @{text 

1271 
"y"}: the result. 

1272 
*} 

25610  1273 
inductive 
25759  1274 
fold_msetG :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a multiset \<Rightarrow> 'b \<Rightarrow> bool" 
25610  1275 
for f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" 
1276 
and z :: 'b 

1277 
where 

25759  1278 
emptyI [intro]: "fold_msetG f z {#} z" 
1279 
 insertI [intro]: "fold_msetG f z A y \<Longrightarrow> fold_msetG f z (A + {#x#}) (f x y)" 

25610  1280 

25759  1281 
inductive_cases empty_fold_msetGE [elim!]: "fold_msetG f z {#} x" 
1282 
inductive_cases insert_fold_msetGE: "fold_msetG f z (A + {#}) y" 

25610  1283 

1284 
definition 

26145  1285 
fold_mset :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a multiset \<Rightarrow> 'b" where 
1286 
"fold_mset f z A = (THE x. fold_msetG f z A x)" 

25610  1287 

25759  1288 
lemma Diff1_fold_msetG: 
26145  1289 
"fold_msetG f z (A  {#x#}) y \<Longrightarrow> x \<in># A \<Longrightarrow> fold_msetG f z A (f x y)" 
26178  1290 
apply (frule_tac x = x in fold_msetG.insertI) 
1291 
apply auto 

1292 
done 

25610  1293 