author  haftmann 
Mon, 07 Jul 2008 08:47:17 +0200  
changeset 27487  c8a6ce181805 
parent 27368  9f90ac19e32b 
child 27611  2c01c0bdb385 
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 
27487  9 
imports Plain "~~/src/HOL/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 = {#})" 
26818
b4a24433154e
Instantiated rule expand_fun_eq in proof of set_of_eq_empty_iff, to avoid that
berghofe
parents:
26567
diff
changeset

199 
by (auto simp: set_of_def Mempty_def in_multiset count_def expand_fun_eq [where f="Rep_multiset M"]) 
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 
27106  503 
[code func del]:"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 

26567
7bcebb8c2d33
instantiation replacing primitive instance plus overloaded defs; more conservative type arities
haftmann
parents:
26178
diff
changeset

715 
instantiation multiset :: (order) order 
7bcebb8c2d33
instantiation replacing primitive instance plus overloaded defs; more conservative type arities
haftmann
parents:
26178
diff
changeset

716 
begin 
10249  717 

26567
7bcebb8c2d33
instantiation replacing primitive instance plus overloaded defs; more conservative type arities
haftmann
parents:
26178
diff
changeset

718 
definition 
27106  719 
less_multiset_def [code func del]: "M' < M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}" 
26567
7bcebb8c2d33
instantiation replacing primitive instance plus overloaded defs; more conservative type arities
haftmann
parents:
26178
diff
changeset

720 

7bcebb8c2d33
instantiation replacing primitive instance plus overloaded defs; more conservative type arities
haftmann
parents:
26178
diff
changeset

721 
definition 
27106  722 
le_multiset_def [code func del]: "M' <= M \<longleftrightarrow> M' = M \<or> M' < (M::'a multiset)" 
10249  723 

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

727 
text {* 

728 
\medskip Irreflexivity. 

729 
*} 

730 

731 
lemma mult_irrefl_aux: 

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

10249  734 

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

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

739 
apply (simp add: set_of_eq_empty_iff) 

740 
done 

10249  741 

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

26178  743 
using insert mult_less_not_refl by fast 
10249  744 

745 

746 
text {* Transitivity. *} 

747 

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

26178  749 
unfolding less_multiset_def mult_def by (blast intro: trancl_trans) 
10249  750 

751 
text {* Asymmetry. *} 

752 

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

756 
apply (erule mult_less_trans, assumption) 

757 
done 

10249  758 

759 
theorem mult_less_asym: 

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

10249  762 

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

26178  764 
unfolding le_multiset_def by auto 
10249  765 

766 
text {* Antisymmetry. *} 

767 

768 
theorem mult_le_antisym: 

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

10249  771 

772 
text {* Transitivity. *} 

773 

774 
theorem mult_le_trans: 

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

10249  777 

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

26567
7bcebb8c2d33
instantiation replacing primitive instance plus overloaded defs; more conservative type arities
haftmann
parents:
26178
diff
changeset

781 
instance 
26178  782 
apply intro_classes 
783 
apply (rule mult_less_le) 

784 
apply (rule mult_le_refl) 

785 
apply (erule mult_le_trans, assumption) 

786 
apply (erule mult_le_antisym, assumption) 

787 
done 

10277  788 

26567
7bcebb8c2d33
instantiation replacing primitive instance plus overloaded defs; more conservative type arities
haftmann
parents:
26178
diff
changeset

789 
end 
7bcebb8c2d33
instantiation replacing primitive instance plus overloaded defs; more conservative type arities
haftmann
parents:
26178
diff
changeset

790 

10249  791 

792 
subsubsection {* Monotonicity of multiset union *} 

793 

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

797 
apply auto 

798 
apply (rule_tac x = a in exI) 

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

800 
apply (simp add: union_assoc) 

801 
done 

10249  802 

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

26178  804 
apply (unfold less_multiset_def mult_def) 
805 
apply (erule trancl_induct) 

806 
apply (blast intro: mult1_union transI order_less_trans r_into_trancl) 

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

808 
done 

10249  809 

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

26178  811 
apply (subst union_commute [of B C]) 
812 
apply (subst union_commute [of D C]) 

813 
apply (erule union_less_mono2) 

814 
done 

10249  815 

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

10249  819 

17161  820 
lemma union_le_mono: 
26178  821 
"A <= C ==> B <= D ==> A + B <= C + (D::'a::order multiset)" 
822 
unfolding le_multiset_def 

823 
by (blast intro: union_less_mono union_less_mono1 union_less_mono2) 

10249  824 

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

828 
prefer 2 

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

830 
prefer 2 

831 
apply (rule one_step_implies_mult) 

832 
apply (simp only: trans_def) 

833 
apply auto 

834 
done 

10249  835 

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

17161  842 
lemma union_upper2: "B <= A + (B::'a::order multiset)" 
26178  843 
by (subst union_commute) (rule union_upper1) 
15072  844 

23611  845 
instance multiset :: (order) pordered_ab_semigroup_add 
26178  846 
apply intro_classes 
847 
apply (erule union_le_mono[OF mult_le_refl]) 

848 
done 

26145  849 

15072  850 

17200  851 
subsection {* Link with lists *} 
15072  852 

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

15072  856 

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

26178  858 
by (induct x) auto 
15072  859 

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

26178  861 
by (induct x) auto 
15072  862 

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

26178  864 
by (induct x) auto 
15867  865 

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

26178  867 
by (induct xs) auto 
15072  868 

18258  869 
lemma multiset_of_append [simp]: 
26178  870 
"multiset_of (xs @ ys) = multiset_of xs + multiset_of ys" 
871 
by (induct xs arbitrary: ys) (auto simp: union_ac) 

18730  872 

15072  873 
lemma surj_multiset_of: "surj multiset_of" 
26178  874 
apply (unfold surj_def) 
875 
apply (rule allI) 

876 
apply (rule_tac M = y in multiset_induct) 

877 
apply auto 

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

879 
apply auto 

880 
done 

10249  881 

25162  882 
lemma set_count_greater_0: "set x = {a. count (multiset_of x) a > 0}" 
26178  883 
by (induct x) auto 
15072  884 

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

888 
apply (rule conjI) 

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

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

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

892 
done 

15072  893 

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

17200  898 
lemma set_eq_iff_multiset_of_eq_distinct: 
26145  899 
"distinct x \<Longrightarrow> distinct y \<Longrightarrow> 
900 
(set x = set y) = (multiset_of x = multiset_of y)" 

26178  901 
by (auto simp: multiset_eq_conv_count_eq distinct_count_atmost_1) 
15072  902 

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

907 
apply (drule distinct_remdups [THEN distinct_remdups 

26145  908 
[THEN set_eq_iff_multiset_of_eq_distinct [THEN iffD2]]]) 
26178  909 
apply simp 
910 
done 

10249  911 

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

15072  915 

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

15867  919 

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

920 
lemma nth_mem_multiset_of: "i < length ls \<Longrightarrow> (ls ! i) :# multiset_of ls" 
26178  921 
apply (induct ls arbitrary: i) 
922 
apply simp 

923 
apply (case_tac i) 

924 
apply auto 

925 
done 

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_remove1: "multiset_of (remove1 a xs) = multiset_of xs  {#a#}" 
26178  928 
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

929 

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

930 
lemma multiset_of_eq_length: 
26178  931 
assumes "multiset_of xs = multiset_of ys" 
932 
shows "length xs = length ys" 

933 
using assms 

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

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

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

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

937 
proof (cases xs) 
26145  938 
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

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

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

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

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

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

944 
case Nil 
26145  945 
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

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

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

948 
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

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

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

952 
case False 
26145  953 
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

954 
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

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

958 
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

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

960 
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

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

962 
done 
26145  963 
with IH xCons have IH': "length xs' = length (remove1 x (y#ys'))" by fastsimp 
964 
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

965 
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

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

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

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

969 

26145  970 
text {* 
971 
This lemma shows which properties suffice to show that a function 

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

973 
*} 

974 
lemma properties_for_sort: 

975 
"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

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

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

979 
case (Cons x xs) 
26145  980 
then have "x \<in> set ys" 
981 
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

982 
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

983 
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

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

985 

15867  986 

15072  987 
subsection {* Pointwise ordering induced by count *} 
988 

19086  989 
definition 
25610  990 
mset_le :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<le>#" 50) where 
27106  991 
[code func del]: "(A \<le># B) = (\<forall>a. count A a \<le> count B a)" 
26145  992 

23611  993 
definition 
25610  994 
mset_less :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<#" 50) where 
27106  995 
[code func del]: "(A <# B) = (A \<le># B \<and> A \<noteq> B)" 
25610  996 

26145  997 
notation mset_le (infix "\<subseteq>#" 50) 
998 
notation mset_less (infix "\<subset>#" 50) 

15072  999 

23611  1000 
lemma mset_le_refl[simp]: "A \<le># A" 
26178  1001 
unfolding mset_le_def by auto 
15072  1002 

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

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

1009 
apply (blast intro: order_antisym) 

1010 
done 

15072  1011 

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

1015 
done 

15072  1016 

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

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

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

1026 
apply (erule_tac x = a in allE)+ 

1027 
apply auto 

1028 
done 

15072  1029 

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

23611  1033 
lemma mset_le_add_right[simp]: "B \<le># A + B" 
26178  1034 
unfolding mset_le_def by auto 
15072  1035 

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

1036 
lemma mset_le_single: "a :# B \<Longrightarrow> {#a#} \<le># B" 
26178  1037 
by (simp add: 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 multiset_diff_union_assoc: "C \<le># B \<Longrightarrow> A + B  C = A + (B  C)" 
26178  1040 
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

1041 

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

1042 
lemma mset_le_multiset_union_diff_commute: 
26178  1043 
assumes "B \<le># A" 
1044 
shows "A  B + C = A + C  B" 

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

1045 
proof  
26145  1046 
from mset_le_exists_conv [of "B" "A"] assms have "\<exists>D. A = B + D" .. 
1047 
from this obtain D where "A = B + D" .. 

1048 
then show ?thesis 

1049 
apply simp 

1050 
apply (subst union_commute) 

1051 
apply (subst multiset_diff_union_assoc) 

1052 
apply simp 

1053 
apply (simp add: diff_cancel) 

1054 
apply (subst union_assoc) 

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

1056 
apply (subst multiset_diff_union_assoc) 

1057 
apply simp 

1058 
apply (simp add: diff_cancel) 

1059 
done 

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

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

1061 

23611  1062 
lemma multiset_of_remdups_le: "multiset_of (remdups xs) \<le># multiset_of xs" 
26178  1063 
apply (induct xs) 
1064 
apply auto 

1065 
apply (rule mset_le_trans) 

1066 
apply auto 

1067 
done 

23611  1068 

26145  1069 
lemma multiset_of_update: 
1070 
"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

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

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

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

1075 
show ?case 
26145  1076 
proof (cases i) 
1077 
case 0 then show ?thesis by simp 

1078 
next 

1079 
case (Suc i') 

1080 
with Cons show ?thesis 

1081 
apply simp 

1082 
apply (subst union_assoc) 

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

1084 
apply (subst union_assoc [symmetric]) 

1085 
apply simp 

1086 
apply (rule mset_le_multiset_union_diff_commute) 

1087 
apply (simp add: mset_le_single nth_mem_multiset_of) 

1088 
done 

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

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

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

1091 

26145  1092 
lemma multiset_of_swap: 
1093 
"i < length ls \<Longrightarrow> j < length ls \<Longrightarrow> 

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

26178  1095 
apply (case_tac "i = j") 
1096 
apply simp 

1097 
apply (simp add: multiset_of_update) 

1098 
apply (subst elem_imp_eq_diff_union[symmetric]) 

1099 
apply (simp add: nth_mem_multiset_of) 

1100 
apply simp 

1101 
done 

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

1102 

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

1107 
interpretation mset_order_cancel_semigroup: 

26145  1108 
pordered_cancel_ab_semigroup_add ["op +" "op \<le>#" "op <#"] 
26178  1109 
by unfold_locales (erule mset_le_mono_add [OF mset_le_refl]) 
23611  1110 

1111 
interpretation mset_order_semigroup_cancel: 

26145  1112 
pordered_ab_semigroup_add_imp_le ["op +" "op \<le>#" "op <#"] 
26178  1113 
by (unfold_locales) simp 
15072  1114 

25610  1115 

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

1119 
apply auto 

1120 
done 

25610  1121 

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

1125 
apply auto 

1126 
done 

25610  1127 

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

1131 
apply (clarsimp simp: mset_le_def mset_less_def) 

1132 
apply safe 

1133 
apply (erule_tac x = a in allE) 

1134 
apply (auto split: split_if_asm) 

1135 
done 

25610  1136 

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

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

1141 
done 

25610  1142 

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

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

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

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

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

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

1152 
lemma mset_less_add_bothsides: 

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

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

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

26178  1157 
by (auto simp: mset_le_def mset_less_def) 
25610  1158 

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

1160 
proof (induct A arbitrary: B) 

1161 
case (empty M) 

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

26145  1165 
then show ?case by simp 
25610  1166 
next 
1167 
case (add S x T) 

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

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

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

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

25610  1177 
qed 
1178 

1179 
lemmas mset_less_trans = mset_order.less_eq_less.less_trans 

1180 

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

26178  1182 
by (auto simp: mset_le_def mset_less_def multi_drop_mem_not_eq) 
25610  1183 

26145  1184 

25610  1185 
subsection {* Strong induction and subset induction for multisets *} 
1186 

26016  1187 
text {* Wellfoundedness of proper subset operator: *} 
25610  1188 

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

25610  1193 

1194 
lemma multiset_add_sub_el_shuffle: 

26145  1195 
assumes "c \<in># B" and "b \<noteq> c" 
25610  1196 
shows "B  {#c#} + {#b#} = B + {#b#}  {#c#}" 
1197 
proof  

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

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

1206 
lemma wf_mset_less_rel: "wf mset_less_rel" 

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

1209 
apply (clarsimp simp: measure_def inv_image_def mset_less_size) 

1210 
done 

25610  1211 

26016  1212 
text {* The induction rules: *} 
25610  1213 

1214 
lemma full_multiset_induct [case_names less]: 

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

1217 
apply (rule wf_mset_less_rel [THEN wf_induct]) 

1218 
apply (rule ih, auto simp: mset_less_rel_def) 

1219 
done 

25610  1220 

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

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

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

1225 
shows "P F" 

25610  1226 
proof  
1227 
from `F \<subseteq># A` 

1228 
show ?thesis 

1229 
proof (induct F) 

1230 
show "P {#}" by fact 

1231 
next 

1232 
fix x F 

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

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

1235 
proof (rule insert) 

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

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

1240 
qed 

1241 
qed 

1242 

26016  1243 
text{* A consequence: Extensionality. *} 
25610  1244 

26145  1245 
lemma multi_count_eq: "(\<forall>x. count A x = count B x) = (A = B)" 
26178  1246 
apply (rule iffI) 
1247 
prefer 2 

1248 
apply clarsimp 

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

1250 
apply (rename_tac C) 

1251 
apply (case_tac B rule: multiset_cases) 

1252 
apply (simp add: empty_multiset_count) 

1253 
apply simp 

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

1255 
apply (force dest: multi_member_split) 

1256 
apply (erule_tac x = x in allE) 

1257 
apply simp 

1258 
done 

25610  1259 

1260 
lemmas multi_count_ext = multi_count_eq [THEN iffD1, rule_format] 

1261 

26145  1262 

25610  1263 
subsection {* The fold combinator *} 
1264 

26145  1265 
text {* 
1266 
The intended behaviour is 

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

1268 
if @{text f} is associativecommutative. 

25610  1269 
*} 
1270 

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

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

1274 
"y"}: the result. 

1275 
*} 

25610  1276 
inductive 
25759  1277 
fold_msetG :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a multiset \<Rightarrow> 'b \<Rightarrow> bool" 
25610  1278 
for f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" 
1279 
and z :: 'b 

1280 
where 

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

25610  1283 

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

25610  1286 

1287 
definition 

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

25610  1290 

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

1295 
done 

25610
72e1563aee09
a fold operation for multisets + more lemmas
kleing 