author  wenzelm 
Fri, 17 Nov 2006 02:20:03 +0100  
changeset 21404  eb85850d3eb7 
parent 21214  a91bab12b2bd 
child 21417  13c33ad15303 
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 
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
19363
diff
changeset

9 
imports Main 
15131  10 
begin 
10249  11 

12 
subsection {* The type of multisets *} 

13 

14 
typedef 'a multiset = "{f::'a => nat. finite {x . 0 < f x}}" 

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 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21214
diff
changeset

28 
single :: "'a => 'a multiset" ("{#_#}") where 
19086  29 
"{#a#} = Abs_multiset (\<lambda>b. if b = a then 1 else 0)" 
10249  30 

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

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

32 
count :: "'a multiset => 'a => nat" where 
19086  33 
"count = Rep_multiset" 
10249  34 

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

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

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

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

40 
Melem :: "'a => 'a multiset => bool" ("(_/ :# _)" [50, 51] 50) where 
19363  41 
"a :# M == 0 < count M a" 
10249  42 

43 
syntax 

44 
"_MCollect" :: "pttrn => 'a multiset => bool => 'a multiset" ("(1{# _ : _./ _#})") 

45 
translations 

20770  46 
"{#x:M. P#}" == "CONST MCollect M (\<lambda>x. P)" 
10249  47 

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

49 
set_of :: "'a multiset => 'a set" where 
19086  50 
"set_of M = {x. x :# M}" 
10249  51 

14691  52 
instance multiset :: (type) "{plus, minus, zero}" .. 
10249  53 

54 
defs (overloaded) 

11464  55 
union_def: "M + N == Abs_multiset (\<lambda>a. Rep_multiset M a + Rep_multiset N a)" 
56 
diff_def: "M  N == Abs_multiset (\<lambda>a. Rep_multiset M a  Rep_multiset N a)" 

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

57 
Zero_multiset_def [simp]: "0 == {#}" 
10249  58 
size_def: "size M == setsum (count M) (set_of M)" 
59 

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

61 
multiset_inter :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<inter>" 70) where 
19086  62 
"multiset_inter A B = A  (A  B)" 
15869  63 

10249  64 

65 
text {* 

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

67 
*} 

68 

11464  69 
lemma const0_in_multiset [simp]: "(\<lambda>a. 0) \<in> multiset" 
17161  70 
by (simp add: multiset_def) 
10249  71 

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

72 
lemma only1_in_multiset [simp]: "(\<lambda>b. if b = a then 1 else 0) \<in> multiset" 
17161  73 
by (simp add: multiset_def) 
10249  74 

75 
lemma union_preserves_multiset [simp]: 

11464  76 
"M \<in> multiset ==> N \<in> multiset ==> (\<lambda>a. M a + N a) \<in> multiset" 
17161  77 
apply (simp add: multiset_def) 
78 
apply (drule (1) finite_UnI) 

10249  79 
apply (simp del: finite_Un add: Un_def) 
80 
done 

81 

82 
lemma diff_preserves_multiset [simp]: 

11464  83 
"M \<in> multiset ==> (\<lambda>a. M a  N a) \<in> multiset" 
17161  84 
apply (simp add: multiset_def) 
10249  85 
apply (rule finite_subset) 
17161  86 
apply auto 
10249  87 
done 
88 

89 

90 
subsection {* Algebraic properties of multisets *} 

91 

92 
subsubsection {* Union *} 

93 

17161  94 
lemma union_empty [simp]: "M + {#} = M \<and> {#} + M = M" 
95 
by (simp add: union_def Mempty_def) 

10249  96 

17161  97 
lemma union_commute: "M + N = N + (M::'a multiset)" 
98 
by (simp add: union_def add_ac) 

99 

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

101 
by (simp add: union_def add_ac) 

10249  102 

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

105 
have "M + (N + K) = (N + K) + M" 

106 
by (rule union_commute) 

107 
also have "\<dots> = N + (K + M)" 

108 
by (rule union_assoc) 

109 
also have "K + M = M + K" 

110 
by (rule union_commute) 

111 
finally show ?thesis . 

112 
qed 

10249  113 

17161  114 
lemmas union_ac = union_assoc union_commute union_lcomm 
10249  115 

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

118 
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

119 
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

120 
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

121 
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

122 
qed 
10277  123 

10249  124 

125 
subsubsection {* Difference *} 

126 

17161  127 
lemma diff_empty [simp]: "M  {#} = M \<and> {#}  M = {#}" 
128 
by (simp add: Mempty_def diff_def) 

10249  129 

17161  130 
lemma diff_union_inverse2 [simp]: "M + {#a#}  {#a#} = M" 
131 
by (simp add: union_def diff_def) 

10249  132 

133 

134 
subsubsection {* Count of elements *} 

135 

17161  136 
lemma count_empty [simp]: "count {#} a = 0" 
137 
by (simp add: count_def Mempty_def) 

10249  138 

17161  139 
lemma count_single [simp]: "count {#b#} a = (if b = a then 1 else 0)" 
140 
by (simp add: count_def single_def) 

10249  141 

17161  142 
lemma count_union [simp]: "count (M + N) a = count M a + count N a" 
143 
by (simp add: count_def union_def) 

10249  144 

17161  145 
lemma count_diff [simp]: "count (M  N) a = count M a  count N a" 
146 
by (simp add: count_def diff_def) 

10249  147 

148 

149 
subsubsection {* Set of elements *} 

150 

17161  151 
lemma set_of_empty [simp]: "set_of {#} = {}" 
152 
by (simp add: set_of_def) 

10249  153 

17161  154 
lemma set_of_single [simp]: "set_of {#b#} = {b}" 
155 
by (simp add: set_of_def) 

10249  156 

17161  157 
lemma set_of_union [simp]: "set_of (M + N) = set_of M \<union> set_of N" 
158 
by (auto simp add: set_of_def) 

10249  159 

17161  160 
lemma set_of_eq_empty_iff [simp]: "(set_of M = {}) = (M = {#})" 
161 
by (auto simp add: set_of_def Mempty_def count_def expand_fun_eq) 

10249  162 

17161  163 
lemma mem_set_of_iff [simp]: "(x \<in> set_of M) = (x :# M)" 
164 
by (auto simp add: set_of_def) 

10249  165 

166 

167 
subsubsection {* Size *} 

168 

17161  169 
lemma size_empty [simp]: "size {#} = 0" 
170 
by (simp add: size_def) 

10249  171 

17161  172 
lemma size_single [simp]: "size {#b#} = 1" 
173 
by (simp add: size_def) 

10249  174 

17161  175 
lemma finite_set_of [iff]: "finite (set_of M)" 
176 
using Rep_multiset [of M] 

177 
by (simp add: multiset_def set_of_def count_def) 

10249  178 

17161  179 
lemma setsum_count_Int: 
11464  180 
"finite A ==> setsum (count N) (A \<inter> set_of N) = setsum (count N) A" 
18258  181 
apply (induct rule: finite_induct) 
17161  182 
apply simp 
10249  183 
apply (simp add: Int_insert_left set_of_def) 
184 
done 

185 

17161  186 
lemma size_union [simp]: "size (M + N::'a multiset) = size M + size N" 
10249  187 
apply (unfold size_def) 
11464  188 
apply (subgoal_tac "count (M + N) = (\<lambda>a. count M a + count N a)") 
10249  189 
prefer 2 
15072  190 
apply (rule ext, simp) 
15402  191 
apply (simp (no_asm_simp) add: setsum_Un_nat setsum_addf setsum_count_Int) 
10249  192 
apply (subst Int_commute) 
193 
apply (simp (no_asm_simp) add: setsum_count_Int) 

194 
done 

195 

17161  196 
lemma size_eq_0_iff_empty [iff]: "(size M = 0) = (M = {#})" 
15072  197 
apply (unfold size_def Mempty_def count_def, auto) 
10249  198 
apply (simp add: set_of_def count_def expand_fun_eq) 
199 
done 

200 

17161  201 
lemma size_eq_Suc_imp_elem: "size M = Suc n ==> \<exists>a. a :# M" 
10249  202 
apply (unfold size_def) 
15072  203 
apply (drule setsum_SucD, auto) 
10249  204 
done 
205 

206 

207 
subsubsection {* Equality of multisets *} 

208 

17161  209 
lemma multiset_eq_conv_count_eq: "(M = N) = (\<forall>a. count M a = count N a)" 
210 
by (simp add: count_def expand_fun_eq) 

10249  211 

17161  212 
lemma single_not_empty [simp]: "{#a#} \<noteq> {#} \<and> {#} \<noteq> {#a#}" 
213 
by (simp add: single_def Mempty_def expand_fun_eq) 

10249  214 

17161  215 
lemma single_eq_single [simp]: "({#a#} = {#b#}) = (a = b)" 
216 
by (auto simp add: single_def expand_fun_eq) 

10249  217 

17161  218 
lemma union_eq_empty [iff]: "(M + N = {#}) = (M = {#} \<and> N = {#})" 
219 
by (auto simp add: union_def Mempty_def expand_fun_eq) 

10249  220 

17161  221 
lemma empty_eq_union [iff]: "({#} = M + N) = (M = {#} \<and> N = {#})" 
222 
by (auto simp add: union_def Mempty_def expand_fun_eq) 

10249  223 

17161  224 
lemma union_right_cancel [simp]: "(M + K = N + K) = (M = (N::'a multiset))" 
225 
by (simp add: union_def expand_fun_eq) 

10249  226 

17161  227 
lemma union_left_cancel [simp]: "(K + M = K + N) = (M = (N::'a multiset))" 
228 
by (simp add: union_def expand_fun_eq) 

10249  229 

17161  230 
lemma union_is_single: 
11464  231 
"(M + N = {#a#}) = (M = {#a#} \<and> N={#} \<or> M = {#} \<and> N = {#a#})" 
15072  232 
apply (simp add: Mempty_def single_def union_def add_is_1 expand_fun_eq) 
10249  233 
apply blast 
234 
done 

235 

17161  236 
lemma single_is_union: 
15072  237 
"({#a#} = M + N) = ({#a#} = M \<and> N = {#} \<or> M = {#} \<and> {#a#} = N)" 
10249  238 
apply (unfold Mempty_def single_def union_def) 
11464  239 
apply (simp add: add_is_1 one_is_add expand_fun_eq) 
10249  240 
apply (blast dest: sym) 
241 
done 

242 

17778  243 
ML"reset use_neq_simproc" 
17161  244 
lemma add_eq_conv_diff: 
10249  245 
"(M + {#a#} = N + {#b#}) = 
15072  246 
(M = N \<and> a = b \<or> M = N  {#a#} + {#b#} \<and> N = M  {#b#} + {#a#})" 
10249  247 
apply (unfold single_def union_def diff_def) 
248 
apply (simp (no_asm) add: expand_fun_eq) 

15072  249 
apply (rule conjI, force, safe, simp_all) 
13601  250 
apply (simp add: eq_sym_conv) 
10249  251 
done 
17778  252 
ML"set use_neq_simproc" 
10249  253 

15869  254 
declare Rep_multiset_inject [symmetric, simp del] 
255 

256 

257 
subsubsection {* Intersection *} 

258 

259 
lemma multiset_inter_count: 

17161  260 
"count (A #\<inter> B) x = min (count A x) (count B x)" 
261 
by (simp add: multiset_inter_def min_def) 

15869  262 

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

17200  264 
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

265 
min_max.inf_commute) 
15869  266 

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

17200  268 
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

269 
min_max.inf_assoc) 
15869  270 

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

272 
by (simp add: multiset_eq_conv_count_eq multiset_inter_count min_def) 

273 

17161  274 
lemmas multiset_inter_ac = 
275 
multiset_inter_commute 

276 
multiset_inter_assoc 

277 
multiset_inter_left_commute 

15869  278 

279 
lemma multiset_union_diff_commute: "B #\<inter> C = {#} \<Longrightarrow> A + B  C = A  C + B" 

17200  280 
apply (simp add: multiset_eq_conv_count_eq multiset_inter_count min_def 
17161  281 
split: split_if_asm) 
15869  282 
apply clarsimp 
17161  283 
apply (erule_tac x = a in allE) 
15869  284 
apply auto 
285 
done 

286 

10249  287 

288 
subsection {* Induction over multisets *} 

289 

290 
lemma setsum_decr: 

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

291 
"finite F ==> (0::nat) < f a ==> 
15072  292 
setsum (f (a := f a  1)) F = (if a\<in>F then setsum f F  1 else setsum f F)" 
18258  293 
apply (induct rule: finite_induct) 
294 
apply auto 

15072  295 
apply (drule_tac a = a in mk_disjoint_insert, auto) 
10249  296 
done 
297 

10313  298 
lemma rep_multiset_induct_aux: 
18730  299 
assumes 1: "P (\<lambda>a. (0::nat))" 
300 
and 2: "!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1))" 

17161  301 
shows "\<forall>f. f \<in> multiset > setsum f {x. 0 < f x} = n > P f" 
18730  302 
apply (unfold multiset_def) 
303 
apply (induct_tac n, simp, clarify) 

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

305 
apply simp 

306 
apply (rule 1) 

307 
apply (rule ext, force, clarify) 

308 
apply (frule setsum_SucD, clarify) 

309 
apply (rename_tac a) 

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

311 
prefer 2 

312 
apply (rule finite_subset) 

313 
prefer 2 

314 
apply assumption 

315 
apply simp 

316 
apply blast 

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

318 
prefer 2 

319 
apply (rule ext) 

320 
apply (simp (no_asm_simp)) 

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

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

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

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

325 
prefer 2 

326 
apply blast 

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

328 
prefer 2 

329 
apply blast 

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

331 
done 

10249  332 

10313  333 
theorem rep_multiset_induct: 
11464  334 
"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

335 
(!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1))) ==> P f" 
17161  336 
using rep_multiset_induct_aux by blast 
10249  337 

18258  338 
theorem multiset_induct [case_names empty add, induct type: multiset]: 
339 
assumes empty: "P {#}" 

340 
and add: "!!M x. P M ==> P (M + {#x#})" 

17161  341 
shows "P M" 
10249  342 
proof  
343 
note defns = union_def single_def Mempty_def 

344 
show ?thesis 

345 
apply (rule Rep_multiset_inverse [THEN subst]) 

10313  346 
apply (rule Rep_multiset [THEN rep_multiset_induct]) 
18258  347 
apply (rule empty [unfolded defns]) 
15072  348 
apply (subgoal_tac "f(b := f b + 1) = (\<lambda>a. f a + (if a=b then 1 else 0))") 
10249  349 
prefer 2 
350 
apply (simp add: expand_fun_eq) 

351 
apply (erule ssubst) 

17200  352 
apply (erule Abs_multiset_inverse [THEN subst]) 
18258  353 
apply (erule add [unfolded defns, simplified]) 
10249  354 
done 
355 
qed 

356 

357 
lemma MCollect_preserves_multiset: 

11464  358 
"M \<in> multiset ==> (\<lambda>x. if P x then M x else 0) \<in> multiset" 
10249  359 
apply (simp add: multiset_def) 
15072  360 
apply (rule finite_subset, auto) 
10249  361 
done 
362 

17161  363 
lemma count_MCollect [simp]: 
10249  364 
"count {# x:M. P x #} a = (if P a then count M a else 0)" 
15072  365 
by (simp add: count_def MCollect_def MCollect_preserves_multiset) 
10249  366 

17161  367 
lemma set_of_MCollect [simp]: "set_of {# x:M. P x #} = set_of M \<inter> {x. P x}" 
368 
by (auto simp add: set_of_def) 

10249  369 

17161  370 
lemma multiset_partition: "M = {# x:M. P x #} + {# x:M. \<not> P x #}" 
371 
by (subst multiset_eq_conv_count_eq, auto) 

10249  372 

17161  373 
lemma add_eq_conv_ex: 
374 
"(M + {#a#} = N + {#b#}) = 

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

15072  376 
by (auto simp add: add_eq_conv_diff) 
10249  377 

15869  378 
declare multiset_typedef [simp del] 
10249  379 

17161  380 

10249  381 
subsection {* Multiset orderings *} 
382 

383 
subsubsection {* Wellfoundedness *} 

384 

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

386 
mult1 :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where 
19086  387 
"mult1 r = 
11464  388 
{(N, M). \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and> 
389 
(\<forall>b. b :# K > (b, a) \<in> r)}" 

10249  390 

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

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

392 
mult :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where 
19086  393 
"mult r = (mult1 r)\<^sup>+" 
10249  394 

11464  395 
lemma not_less_empty [iff]: "(M, {#}) \<notin> mult1 r" 
10277  396 
by (simp add: mult1_def) 
10249  397 

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

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

19582  401 
(is "_ \<Longrightarrow> ?case1 (mult1 r) \<or> ?case2") 
10249  402 
proof (unfold mult1_def) 
11464  403 
let ?r = "\<lambda>K a. \<forall>b. b :# K > (b, a) \<in> r" 
404 
let ?R = "\<lambda>N M. \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and> ?r K a" 

10249  405 
let ?case1 = "?case1 {(N, M). ?R N M}" 
406 

11464  407 
assume "(N, M0 + {#a#}) \<in> {(N, M). ?R N M}" 
18258  408 
then have "\<exists>a' M0' K. 
11464  409 
M0 + {#a#} = M0' + {#a'#} \<and> N = M0' + K \<and> ?r K a'" by simp 
18258  410 
then show "?case1 \<or> ?case2" 
10249  411 
proof (elim exE conjE) 
412 
fix a' M0' K 

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

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

18258  415 
then have "M0 = M0' \<and> a = a' \<or> 
11464  416 
(\<exists>K'. M0 = K' + {#a'#} \<and> M0' = K' + {#a#})" 
10249  417 
by (simp only: add_eq_conv_ex) 
18258  418 
then show ?thesis 
10249  419 
proof (elim disjE conjE exE) 
420 
assume "M0 = M0'" "a = a'" 

11464  421 
with N r have "?r K a \<and> N = M0 + K" by simp 
18258  422 
then have ?case2 .. then show ?thesis .. 
10249  423 
next 
424 
fix K' 

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

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

427 

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

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

18258  430 
with n have ?case1 by simp then show ?thesis .. 
10249  431 
qed 
432 
qed 

433 
qed 

434 

11464  435 
lemma all_accessible: "wf r ==> \<forall>M. M \<in> acc (mult1 r)" 
10249  436 
proof 
437 
let ?R = "mult1 r" 

438 
let ?W = "acc ?R" 

439 
{ 

440 
fix M M0 a 

11464  441 
assume M0: "M0 \<in> ?W" 
12399  442 
and wf_hyp: "!!b. (b, a) \<in> r ==> (\<forall>M \<in> ?W. M + {#b#} \<in> ?W)" 
11464  443 
and acc_hyp: "\<forall>M. (M, M0) \<in> ?R > M + {#a#} \<in> ?W" 
444 
have "M0 + {#a#} \<in> ?W" 

10249  445 
proof (rule accI [of "M0 + {#a#}"]) 
446 
fix N 

11464  447 
assume "(N, M0 + {#a#}) \<in> ?R" 
18258  448 
then have "((\<exists>M. (M, M0) \<in> ?R \<and> N = M + {#a#}) \<or> 
11464  449 
(\<exists>K. (\<forall>b. b :# K > (b, a) \<in> r) \<and> N = M0 + K))" 
10249  450 
by (rule less_add) 
18258  451 
then show "N \<in> ?W" 
10249  452 
proof (elim exE disjE conjE) 
11464  453 
fix M assume "(M, M0) \<in> ?R" and N: "N = M + {#a#}" 
454 
from acc_hyp have "(M, M0) \<in> ?R > M + {#a#} \<in> ?W" .. 

18258  455 
then have "M + {#a#} \<in> ?W" .. 
456 
then show "N \<in> ?W" by (simp only: N) 

10249  457 
next 
458 
fix K 

459 
assume N: "N = M0 + K" 

11464  460 
assume "\<forall>b. b :# K > (b, a) \<in> r" 
18730  461 
then have "M0 + K \<in> ?W" 
10249  462 
proof (induct K) 
18730  463 
case empty 
18258  464 
from M0 show "M0 + {#} \<in> ?W" by simp 
18730  465 
next 
466 
case (add K x) 

467 
from add.prems have "(x, a) \<in> r" by simp 

18258  468 
with wf_hyp have "\<forall>M \<in> ?W. M + {#x#} \<in> ?W" by blast 
18730  469 
moreover from add have "M0 + K \<in> ?W" by simp 
18258  470 
ultimately have "(M0 + K) + {#x#} \<in> ?W" .. 
471 
then show "M0 + (K + {#x#}) \<in> ?W" by (simp only: union_assoc) 

10249  472 
qed 
18730  473 
then show "N \<in> ?W" by (simp only: N) 
10249  474 
qed 
475 
qed 

476 
} note tedious_reasoning = this 

477 

478 
assume wf: "wf r" 

479 
fix M 

11464  480 
show "M \<in> ?W" 
10249  481 
proof (induct M) 
11464  482 
show "{#} \<in> ?W" 
10249  483 
proof (rule accI) 
11464  484 
fix b assume "(b, {#}) \<in> ?R" 
485 
with not_less_empty show "b \<in> ?W" by contradiction 

10249  486 
qed 
487 

11464  488 
fix M a assume "M \<in> ?W" 
489 
from wf have "\<forall>M \<in> ?W. M + {#a#} \<in> ?W" 

10249  490 
proof induct 
491 
fix a 

12399  492 
assume "!!b. (b, a) \<in> r ==> (\<forall>M \<in> ?W. M + {#b#} \<in> ?W)" 
11464  493 
show "\<forall>M \<in> ?W. M + {#a#} \<in> ?W" 
10249  494 
proof 
11464  495 
fix M assume "M \<in> ?W" 
18258  496 
then show "M + {#a#} \<in> ?W" 
10249  497 
by (rule acc_induct) (rule tedious_reasoning) 
498 
qed 

499 
qed 

18258  500 
then show "M + {#a#} \<in> ?W" .. 
10249  501 
qed 
502 
qed 

503 

504 
theorem wf_mult1: "wf r ==> wf (mult1 r)" 

505 
by (rule acc_wfI, rule all_accessible) 

506 

507 
theorem wf_mult: "wf r ==> wf (mult r)" 

508 
by (unfold mult_def, rule wf_trancl, rule wf_mult1) 

509 

510 

511 
subsubsection {* Closurefree presentation *} 

512 

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

514 

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

15072  516 
by (simp add: multiset_eq_conv_count_eq) 
10249  517 

518 
text {* One direction. *} 

519 

520 
lemma mult_implies_one_step: 

11464  521 
"trans r ==> (M, N) \<in> mult r ==> 
522 
\<exists>I J K. N = I + J \<and> M = I + K \<and> J \<noteq> {#} \<and> 

523 
(\<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r)" 

10249  524 
apply (unfold mult_def mult1_def set_of_def) 
15072  525 
apply (erule converse_trancl_induct, clarify) 
526 
apply (rule_tac x = M0 in exI, simp, clarify) 

10249  527 
apply (case_tac "a :# K") 
528 
apply (rule_tac x = I in exI) 

529 
apply (simp (no_asm)) 

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

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

11464  532 
apply (drule_tac f = "\<lambda>M. M  {#a#}" in arg_cong) 
10249  533 
apply (simp add: diff_union_single_conv) 
534 
apply (simp (no_asm_use) add: trans_def) 

535 
apply blast 

536 
apply (subgoal_tac "a :# I") 

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

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

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

540 
apply (rule conjI) 

541 
apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split) 

542 
apply (rule conjI) 

15072  543 
apply (drule_tac f = "\<lambda>M. M  {#a#}" in arg_cong, simp) 
10249  544 
apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split) 
545 
apply (simp (no_asm_use) add: trans_def) 

546 
apply blast 

10277  547 
apply (subgoal_tac "a :# (M0 + {#a#})") 
10249  548 
apply simp 
549 
apply (simp (no_asm)) 

550 
done 

551 

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

15072  553 
by (simp add: multiset_eq_conv_count_eq) 
10249  554 

11464  555 
lemma size_eq_Suc_imp_eq_union: "size M = Suc n ==> \<exists>a N. M = N + {#a#}" 
10249  556 
apply (erule size_eq_Suc_imp_elem [THEN exE]) 
15072  557 
apply (drule elem_imp_eq_diff_union, auto) 
10249  558 
done 
559 

560 
lemma one_step_implies_mult_aux: 

561 
"trans r ==> 

11464  562 
\<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)) 
563 
> (I + K, I + J) \<in> mult r" 

15072  564 
apply (induct_tac n, auto) 
565 
apply (frule size_eq_Suc_imp_eq_union, clarify) 

566 
apply (rename_tac "J'", simp) 

567 
apply (erule notE, auto) 

10249  568 
apply (case_tac "J' = {#}") 
569 
apply (simp add: mult_def) 

570 
apply (rule r_into_trancl) 

15072  571 
apply (simp add: mult1_def set_of_def, blast) 
11464  572 
txt {* Now we know @{term "J' \<noteq> {#}"}. *} 
573 
apply (cut_tac M = K and P = "\<lambda>x. (x, a) \<in> r" in multiset_partition) 

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

10249  575 
apply (erule ssubst) 
15072  576 
apply (simp add: Ball_def, auto) 
10249  577 
apply (subgoal_tac 
11464  578 
"((I + {# x : K. (x, a) \<in> r #}) + {# x : K. (x, a) \<notin> r #}, 
579 
(I + {# x : K. (x, a) \<in> r #}) + J') \<in> mult r") 

10249  580 
prefer 2 
581 
apply force 

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

583 
apply (erule trancl_trans) 

584 
apply (rule r_into_trancl) 

585 
apply (simp add: mult1_def set_of_def) 

586 
apply (rule_tac x = a in exI) 

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

588 
apply (simp add: union_ac) 

589 
done 

590 

17161  591 
lemma one_step_implies_mult: 
11464  592 
"trans r ==> J \<noteq> {#} ==> \<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r 
593 
==> (I + K, I + J) \<in> mult r" 

15072  594 
apply (insert one_step_implies_mult_aux, blast) 
10249  595 
done 
596 

597 

598 
subsubsection {* Partialorder properties *} 

599 

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

600 
instance multiset :: (type) ord .. 
10249  601 

602 
defs (overloaded) 

11464  603 
less_multiset_def: "M' < M == (M', M) \<in> mult {(x', x). x' < x}" 
604 
le_multiset_def: "M' <= M == M' = M \<or> M' < (M::'a multiset)" 

10249  605 

606 
lemma trans_base_order: "trans {(x', x). x' < (x::'a::order)}" 

18730  607 
unfolding trans_def by (blast intro: order_less_trans) 
10249  608 

609 
text {* 

610 
\medskip Irreflexivity. 

611 
*} 

612 

613 
lemma mult_irrefl_aux: 

18258  614 
"finite A ==> (\<forall>x \<in> A. \<exists>y \<in> A. x < (y::'a::order)) \<Longrightarrow> A = {}" 
615 
apply (induct rule: finite_induct) 

10249  616 
apply (auto intro: order_less_trans) 
617 
done 

618 

17161  619 
lemma mult_less_not_refl: "\<not> M < (M::'a::order multiset)" 
15072  620 
apply (unfold less_multiset_def, auto) 
621 
apply (drule trans_base_order [THEN mult_implies_one_step], auto) 

10249  622 
apply (drule finite_set_of [THEN mult_irrefl_aux [rule_format (no_asm)]]) 
623 
apply (simp add: set_of_eq_empty_iff) 

624 
done 

625 

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

15072  627 
by (insert mult_less_not_refl, fast) 
10249  628 

629 

630 
text {* Transitivity. *} 

631 

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

633 
apply (unfold less_multiset_def mult_def) 

634 
apply (blast intro: trancl_trans) 

635 
done 

636 

637 
text {* Asymmetry. *} 

638 

11464  639 
theorem mult_less_not_sym: "M < N ==> \<not> N < (M::'a::order multiset)" 
10249  640 
apply auto 
641 
apply (rule mult_less_not_refl [THEN notE]) 

15072  642 
apply (erule mult_less_trans, assumption) 
10249  643 
done 
644 

645 
theorem mult_less_asym: 

11464  646 
"M < N ==> (\<not> P ==> N < (M::'a::order multiset)) ==> P" 
15072  647 
by (insert mult_less_not_sym, blast) 
10249  648 

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

18730  650 
unfolding le_multiset_def by auto 
10249  651 

652 
text {* Antisymmetry. *} 

653 

654 
theorem mult_le_antisym: 

655 
"M <= N ==> N <= M ==> M = (N::'a::order multiset)" 

18730  656 
unfolding le_multiset_def by (blast dest: mult_less_not_sym) 
10249  657 

658 
text {* Transitivity. *} 

659 

660 
theorem mult_le_trans: 

661 
"K <= M ==> M <= N ==> K <= (N::'a::order multiset)" 

18730  662 
unfolding le_multiset_def by (blast intro: mult_less_trans) 
10249  663 

11655  664 
theorem mult_less_le: "(M < N) = (M <= N \<and> M \<noteq> (N::'a::order multiset))" 
18730  665 
unfolding le_multiset_def by auto 
10249  666 

10277  667 
text {* Partial order. *} 
668 

669 
instance multiset :: (order) order 

670 
apply intro_classes 

671 
apply (rule mult_le_refl) 

15072  672 
apply (erule mult_le_trans, assumption) 
673 
apply (erule mult_le_antisym, assumption) 

10277  674 
apply (rule mult_less_le) 
675 
done 

676 

10249  677 

678 
subsubsection {* Monotonicity of multiset union *} 

679 

17161  680 
lemma mult1_union: 
11464  681 
"(B, D) \<in> mult1 r ==> trans r ==> (C + B, C + D) \<in> mult1 r" 
15072  682 
apply (unfold mult1_def, auto) 
10249  683 
apply (rule_tac x = a in exI) 
684 
apply (rule_tac x = "C + M0" in exI) 

685 
apply (simp add: union_assoc) 

686 
done 

687 

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

689 
apply (unfold less_multiset_def mult_def) 

690 
apply (erule trancl_induct) 

691 
apply (blast intro: mult1_union transI order_less_trans r_into_trancl) 

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

693 
done 

694 

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

696 
apply (subst union_commute [of B C]) 

697 
apply (subst union_commute [of D C]) 

698 
apply (erule union_less_mono2) 

699 
done 

700 

17161  701 
lemma union_less_mono: 
10249  702 
"A < C ==> B < D ==> A + B < C + (D::'a::order multiset)" 
703 
apply (blast intro!: union_less_mono1 union_less_mono2 mult_less_trans) 

704 
done 

705 

17161  706 
lemma union_le_mono: 
10249  707 
"A <= C ==> B <= D ==> A + B <= C + (D::'a::order multiset)" 
18730  708 
unfolding le_multiset_def 
709 
by (blast intro: union_less_mono union_less_mono1 union_less_mono2) 

10249  710 

17161  711 
lemma empty_leI [iff]: "{#} <= (M::'a::order multiset)" 
10249  712 
apply (unfold le_multiset_def less_multiset_def) 
713 
apply (case_tac "M = {#}") 

714 
prefer 2 

11464  715 
apply (subgoal_tac "({#} + {#}, {#} + M) \<in> mult (Collect (split op <))") 
10249  716 
prefer 2 
717 
apply (rule one_step_implies_mult) 

15072  718 
apply (simp only: trans_def, auto) 
10249  719 
done 
720 

17161  721 
lemma union_upper1: "A <= A + (B::'a::order multiset)" 
15072  722 
proof  
17200  723 
have "A + {#} <= A + B" by (blast intro: union_le_mono) 
18258  724 
then show ?thesis by simp 
15072  725 
qed 
726 

17161  727 
lemma union_upper2: "B <= A + (B::'a::order multiset)" 
18258  728 
by (subst union_commute) (rule union_upper1) 
15072  729 

730 

17200  731 
subsection {* Link with lists *} 
15072  732 

17200  733 
consts 
15072  734 
multiset_of :: "'a list \<Rightarrow> 'a multiset" 
735 
primrec 

736 
"multiset_of [] = {#}" 

737 
"multiset_of (a # x) = multiset_of x + {# a #}" 

738 

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

18258  740 
by (induct x) auto 
15072  741 

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

18258  743 
by (induct x) auto 
15072  744 

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

18258  746 
by (induct x) auto 
15867  747 

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

749 
by (induct xs) auto 

15072  750 

18258  751 
lemma multiset_of_append [simp]: 
752 
"multiset_of (xs @ ys) = multiset_of xs + multiset_of ys" 

20503  753 
by (induct xs arbitrary: ys) (auto simp: union_ac) 
18730  754 

15072  755 
lemma surj_multiset_of: "surj multiset_of" 
17200  756 
apply (unfold surj_def, rule allI) 
757 
apply (rule_tac M=y in multiset_induct, auto) 

758 
apply (rule_tac x = "x # xa" in exI, auto) 

10249  759 
done 
760 

15072  761 
lemma set_count_greater_0: "set x = {a. 0 < count (multiset_of x) a}" 
18258  762 
by (induct x) auto 
15072  763 

17200  764 
lemma distinct_count_atmost_1: 
15072  765 
"distinct x = (! a. count (multiset_of x) a = (if a \<in> set x then 1 else 0))" 
18258  766 
apply (induct x, simp, rule iffI, simp_all) 
17200  767 
apply (rule conjI) 
768 
apply (simp_all add: set_of_multiset_of [THEN sym] del: set_of_multiset_of) 

15072  769 
apply (erule_tac x=a in allE, simp, clarify) 
17200  770 
apply (erule_tac x=aa in allE, simp) 
15072  771 
done 
772 

17200  773 
lemma multiset_of_eq_setD: 
15867  774 
"multiset_of xs = multiset_of ys \<Longrightarrow> set xs = set ys" 
775 
by (rule) (auto simp add:multiset_eq_conv_count_eq set_count_greater_0) 

776 

17200  777 
lemma set_eq_iff_multiset_of_eq_distinct: 
778 
"\<lbrakk>distinct x; distinct y\<rbrakk> 

15072  779 
\<Longrightarrow> (set x = set y) = (multiset_of x = multiset_of y)" 
17200  780 
by (auto simp: multiset_eq_conv_count_eq distinct_count_atmost_1) 
15072  781 

17200  782 
lemma set_eq_iff_multiset_of_remdups_eq: 
15072  783 
"(set x = set y) = (multiset_of (remdups x) = multiset_of (remdups y))" 
17200  784 
apply (rule iffI) 
785 
apply (simp add: set_eq_iff_multiset_of_eq_distinct[THEN iffD1]) 

786 
apply (drule distinct_remdups[THEN distinct_remdups 

787 
[THEN set_eq_iff_multiset_of_eq_distinct[THEN iffD2]]]) 

15072  788 
apply simp 
10249  789 
done 
790 

18258  791 
lemma multiset_of_compl_union [simp]: 
792 
"multiset_of [x\<in>xs. P x] + multiset_of [x\<in>xs. \<not>P x] = multiset_of xs" 

15630  793 
by (induct xs) (auto simp: union_ac) 
15072  794 

17200  795 
lemma count_filter: 
18258  796 
"count (multiset_of xs) x = length [y \<in> xs. y = x]" 
797 
by (induct xs) auto 

15867  798 

799 

15072  800 
subsection {* Pointwise ordering induced by count *} 
801 

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

803 
mset_le :: "['a multiset, 'a multiset] \<Rightarrow> bool" ("_ \<le># _" [50,51] 50) where 
19086  804 
"(xs \<le># ys) = (\<forall>a. count xs a \<le> count ys a)" 
15072  805 

806 
lemma mset_le_refl[simp]: "xs \<le># xs" 

18730  807 
unfolding mset_le_def by auto 
15072  808 

809 
lemma mset_le_trans: "\<lbrakk> xs \<le># ys; ys \<le># zs \<rbrakk> \<Longrightarrow> xs \<le># zs" 

18730  810 
unfolding mset_le_def by (fast intro: order_trans) 
15072  811 

812 
lemma mset_le_antisym: "\<lbrakk> xs\<le># ys; ys \<le># xs\<rbrakk> \<Longrightarrow> xs = ys" 

17200  813 
apply (unfold mset_le_def) 
814 
apply (rule multiset_eq_conv_count_eq[THEN iffD2]) 

15072  815 
apply (blast intro: order_antisym) 
816 
done 

817 

17200  818 
lemma mset_le_exists_conv: 
819 
"(xs \<le># ys) = (\<exists>zs. ys = xs + zs)" 

820 
apply (unfold mset_le_def, rule iffI, rule_tac x = "ys  xs" in exI) 

15072  821 
apply (auto intro: multiset_eq_conv_count_eq [THEN iffD2]) 
822 
done 

823 

824 
lemma mset_le_mono_add_right_cancel[simp]: "(xs + zs \<le># ys + zs) = (xs \<le># ys)" 

18730  825 
unfolding mset_le_def by auto 
15072  826 

827 
lemma mset_le_mono_add_left_cancel[simp]: "(zs + xs \<le># zs + ys) = (xs \<le># ys)" 

18730  828 
unfolding mset_le_def by auto 
15072  829 

17200  830 
lemma mset_le_mono_add: "\<lbrakk> xs \<le># ys; vs \<le># ws \<rbrakk> \<Longrightarrow> xs + vs \<le># ys + ws" 
831 
apply (unfold mset_le_def) 

832 
apply auto 

15072  833 
apply (erule_tac x=a in allE)+ 
834 
apply auto 

835 
done 

836 

837 
lemma mset_le_add_left[simp]: "xs \<le># xs + ys" 

18730  838 
unfolding mset_le_def by auto 
15072  839 

840 
lemma mset_le_add_right[simp]: "ys \<le># xs + ys" 

18730  841 
unfolding mset_le_def by auto 
15072  842 

843 
lemma multiset_of_remdups_le: "multiset_of (remdups x) \<le># multiset_of x" 

17200  844 
apply (induct x) 
845 
apply auto 

846 
apply (rule mset_le_trans) 

847 
apply auto 

848 
done 

15072  849 

10249  850 
end 