author  berghofe 
Wed, 11 Jul 2007 11:24:36 +0200  
changeset 23751  a7c7edf2c5ad 
parent 23611  65b168646309 
child 24035  74c032aea9ed 
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 

21417  52 
instance multiset :: (type) "{plus, minus, zero, size}" 
11464  53 
union_def: "M + N == Abs_multiset (\<lambda>a. Rep_multiset M a + Rep_multiset N a)" 
54 
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

55 
Zero_multiset_def [simp]: "0 == {#}" 
21417  56 
size_def: "size M == setsum (count M) (set_of M)" .. 
10249  57 

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

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

10249  62 

63 
text {* 

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

65 
*} 

66 

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

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

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

73 
lemma union_preserves_multiset [simp]: 

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

10249  77 
apply (simp del: finite_Un add: Un_def) 
78 
done 

79 

80 
lemma diff_preserves_multiset [simp]: 

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

87 

88 
subsection {* Algebraic properties of multisets *} 

89 

90 
subsubsection {* Union *} 

91 

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

10249  94 

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

97 

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

99 
by (simp add: union_def add_ac) 

10249  100 

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

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

104 
by (rule union_commute) 

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

106 
by (rule union_assoc) 

107 
also have "K + M = M + K" 

108 
by (rule union_commute) 

109 
finally show ?thesis . 

110 
qed 

10249  111 

17161  112 
lemmas union_ac = union_assoc union_commute union_lcomm 
10249  113 

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

116 
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

117 
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

118 
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

119 
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

120 
qed 
10277  121 

10249  122 

123 
subsubsection {* Difference *} 

124 

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

10249  127 

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

10249  130 

131 

132 
subsubsection {* Count of elements *} 

133 

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

10249  136 

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

10249  139 

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

10249  142 

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

10249  145 

146 

147 
subsubsection {* Set of elements *} 

148 

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

10249  151 

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

10249  154 

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

10249  157 

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

10249  160 

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

10249  163 

164 

165 
subsubsection {* Size *} 

166 

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

10249  169 

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

10249  172 

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

175 
by (simp add: multiset_def set_of_def count_def) 

10249  176 

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

183 

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

192 
done 

193 

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

198 

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

204 

205 
subsubsection {* Equality of multisets *} 

206 

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

10249  209 

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

10249  212 

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

10249  215 

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

10249  218 

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

10249  221 

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

10249  224 

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

10249  227 

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

233 

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

240 

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

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

15869  252 
declare Rep_multiset_inject [symmetric, simp del] 
253 

23611  254 
instance multiset :: (type) cancel_ab_semigroup_add 
255 
proof 

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

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

258 
qed 

15869  259 

260 
subsubsection {* Intersection *} 

261 

262 
lemma multiset_inter_count: 

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

15869  265 

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

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

268 
min_max.inf_commute) 
15869  269 

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

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

272 
min_max.inf_assoc) 
15869  273 

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

275 
by (simp add: multiset_eq_conv_count_eq multiset_inter_count min_def) 

276 

17161  277 
lemmas multiset_inter_ac = 
278 
multiset_inter_commute 

279 
multiset_inter_assoc 

280 
multiset_inter_left_commute 

15869  281 

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

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

289 

10249  290 

291 
subsection {* Induction over multisets *} 

292 

293 
lemma setsum_decr: 

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

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

15072  298 
apply (drule_tac a = a in mk_disjoint_insert, auto) 
10249  299 
done 
300 

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

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

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

308 
apply simp 

309 
apply (rule 1) 

310 
apply (rule ext, force, clarify) 

311 
apply (frule setsum_SucD, clarify) 

312 
apply (rename_tac a) 

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

314 
prefer 2 

315 
apply (rule finite_subset) 

316 
prefer 2 

317 
apply assumption 

318 
apply simp 

319 
apply blast 

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

321 
prefer 2 

322 
apply (rule ext) 

323 
apply (simp (no_asm_simp)) 

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

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

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

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

328 
prefer 2 

329 
apply blast 

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

331 
prefer 2 

332 
apply blast 

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

334 
done 

10249  335 

10313  336 
theorem rep_multiset_induct: 
11464  337 
"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

338 
(!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1))) ==> P f" 
17161  339 
using rep_multiset_induct_aux by blast 
10249  340 

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

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

17161  344 
shows "P M" 
10249  345 
proof  
346 
note defns = union_def single_def Mempty_def 

347 
show ?thesis 

348 
apply (rule Rep_multiset_inverse [THEN subst]) 

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

354 
apply (erule ssubst) 

17200  355 
apply (erule Abs_multiset_inverse [THEN subst]) 
18258  356 
apply (erule add [unfolded defns, simplified]) 
10249  357 
done 
358 
qed 

359 

360 
lemma MCollect_preserves_multiset: 

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

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

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

10249  372 

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

10249  375 

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

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

15072  379 
by (auto simp add: add_eq_conv_diff) 
10249  380 

15869  381 
declare multiset_typedef [simp del] 
10249  382 

17161  383 

10249  384 
subsection {* Multiset orderings *} 
385 

386 
subsubsection {* Wellfoundedness *} 

387 

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

10249  393 

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

394 
definition 
23751  395 
mult :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where 
396 
"mult r = (mult1 r)\<^sup>+" 

10249  397 

23751  398 
lemma not_less_empty [iff]: "(M, {#}) \<notin> mult1 r" 
10277  399 
by (simp add: mult1_def) 
10249  400 

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

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

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

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

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

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

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

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

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

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

430 

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

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

18258  433 
with n have ?case1 by simp then show ?thesis .. 
10249  434 
qed 
435 
qed 

436 
qed 

437 

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

441 
let ?W = "acc ?R" 

442 
{ 

443 
fix M M0 a 

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

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

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

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

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

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

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

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

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

10249  460 
next 
461 
fix K 

462 
assume N: "N = M0 + K" 

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

10249  465 
proof (induct K) 
18730  466 
case empty 
23751  467 
from M0 show "M0 + {#} \<in> ?W" by simp 
18730  468 
next 
469 
case (add K x) 

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

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

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

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

10249  475 
qed 
23751  476 
then show "N \<in> ?W" by (simp only: N) 
10249  477 
qed 
478 
qed 

479 
} note tedious_reasoning = this 

480 

23751  481 
assume wf: "wf r" 
10249  482 
fix M 
23751  483 
show "M \<in> ?W" 
10249  484 
proof (induct M) 
23751  485 
show "{#} \<in> ?W" 
10249  486 
proof (rule accI) 
23751  487 
fix b assume "(b, {#}) \<in> ?R" 
488 
with not_less_empty show "b \<in> ?W" by contradiction 

10249  489 
qed 
490 

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

10249  493 
proof induct 
494 
fix a 

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

10249  497 
proof 
23751  498 
fix M assume "M \<in> ?W" 
499 
then show "M + {#a#} \<in> ?W" 

23373  500 
by (rule acc_induct) (rule tedious_reasoning [OF _ r]) 
10249  501 
qed 
502 
qed 

23751  503 
from this and `M \<in> ?W` show "M + {#a#} \<in> ?W" .. 
10249  504 
qed 
505 
qed 

506 

23751  507 
theorem wf_mult1: "wf r ==> wf (mult1 r)" 
23373  508 
by (rule acc_wfI) (rule all_accessible) 
10249  509 

23751  510 
theorem wf_mult: "wf r ==> wf (mult r)" 
511 
unfolding mult_def by (rule wf_trancl) (rule wf_mult1) 

10249  512 

513 

514 
subsubsection {* Closurefree presentation *} 

515 

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

517 

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

23373  519 
by (simp add: multiset_eq_conv_count_eq) 
10249  520 

521 
text {* One direction. *} 

522 

523 
lemma mult_implies_one_step: 

23751  524 
"trans r ==> (M, N) \<in> mult r ==> 
11464  525 
\<exists>I J K. N = I + J \<and> M = I + K \<and> J \<noteq> {#} \<and> 
23751  526 
(\<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r)" 
10249  527 
apply (unfold mult_def mult1_def set_of_def) 
23751  528 
apply (erule converse_trancl_induct, clarify) 
15072  529 
apply (rule_tac x = M0 in exI, simp, clarify) 
23751  530 
apply (case_tac "a :# K") 
10249  531 
apply (rule_tac x = I in exI) 
532 
apply (simp (no_asm)) 

23751  533 
apply (rule_tac x = "(K  {#a#}) + Ka" in exI) 
10249  534 
apply (simp (no_asm_simp) add: union_assoc [symmetric]) 
11464  535 
apply (drule_tac f = "\<lambda>M. M  {#a#}" in arg_cong) 
10249  536 
apply (simp add: diff_union_single_conv) 
537 
apply (simp (no_asm_use) add: trans_def) 

538 
apply blast 

539 
apply (subgoal_tac "a :# I") 

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

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

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

543 
apply (rule conjI) 

544 
apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split) 

545 
apply (rule conjI) 

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

549 
apply blast 

10277  550 
apply (subgoal_tac "a :# (M0 + {#a#})") 
10249  551 
apply simp 
552 
apply (simp (no_asm)) 

553 
done 

554 

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

23373  556 
by (simp add: multiset_eq_conv_count_eq) 
10249  557 

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

563 
lemma one_step_implies_mult_aux: 

23751  564 
"trans r ==> 
565 
\<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)) 

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

15072  567 
apply (induct_tac n, auto) 
568 
apply (frule size_eq_Suc_imp_eq_union, clarify) 

569 
apply (rename_tac "J'", simp) 

570 
apply (erule notE, auto) 

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

23751  573 
apply (rule r_into_trancl) 
15072  574 
apply (simp add: mult1_def set_of_def, blast) 
11464  575 
txt {* Now we know @{term "J' \<noteq> {#}"}. *} 
23751  576 
apply (cut_tac M = K and P = "\<lambda>x. (x, a) \<in> r" in multiset_partition) 
11464  577 
apply (erule_tac P = "\<forall>k \<in> set_of K. ?P k" in rev_mp) 
10249  578 
apply (erule ssubst) 
15072  579 
apply (simp add: Ball_def, auto) 
10249  580 
apply (subgoal_tac 
23751  581 
"((I + {# x : K. (x, a) \<in> r #}) + {# x : K. (x, a) \<notin> r #}, 
582 
(I + {# x : K. (x, a) \<in> r #}) + J') \<in> mult r") 

10249  583 
prefer 2 
584 
apply force 

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

23751  586 
apply (erule trancl_trans) 
587 
apply (rule r_into_trancl) 

10249  588 
apply (simp add: mult1_def set_of_def) 
589 
apply (rule_tac x = a in exI) 

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

591 
apply (simp add: union_ac) 

592 
done 

593 

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

23373  597 
using one_step_implies_mult_aux by blast 
10249  598 

599 

600 
subsubsection {* Partialorder properties *} 

601 

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

602 
instance multiset :: (type) ord .. 
10249  603 

604 
defs (overloaded) 

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

23751  608 
lemma trans_base_order: "trans {(x', x). x' < (x::'a::order)}" 
18730  609 
unfolding trans_def by (blast intro: order_less_trans) 
10249  610 

611 
text {* 

612 
\medskip Irreflexivity. 

613 
*} 

614 

615 
lemma mult_irrefl_aux: 

18258  616 
"finite A ==> (\<forall>x \<in> A. \<exists>y \<in> A. x < (y::'a::order)) \<Longrightarrow> A = {}" 
23373  617 
by (induct rule: finite_induct) (auto intro: order_less_trans) 
10249  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" 

23373  627 
using insert mult_less_not_refl by fast 
10249  628 

629 

630 
text {* Transitivity. *} 

631 

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

23751  633 
unfolding less_multiset_def mult_def by (blast intro: trancl_trans) 
10249  634 

635 
text {* Asymmetry. *} 

636 

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

15072  640 
apply (erule mult_less_trans, assumption) 
10249  641 
done 
642 

643 
theorem mult_less_asym: 

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

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

18730  648 
unfolding le_multiset_def by auto 
10249  649 

650 
text {* Antisymmetry. *} 

651 

652 
theorem mult_le_antisym: 

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

18730  654 
unfolding le_multiset_def by (blast dest: mult_less_not_sym) 
10249  655 

656 
text {* Transitivity. *} 

657 

658 
theorem mult_le_trans: 

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

18730  660 
unfolding le_multiset_def by (blast intro: mult_less_trans) 
10249  661 

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

10277  665 
text {* Partial order. *} 
666 

667 
instance multiset :: (order) order 

668 
apply intro_classes 

23751  669 
apply (rule mult_less_le) 
670 
apply (rule mult_le_refl) 

671 
apply (erule mult_le_trans, assumption) 

672 
apply (erule mult_le_antisym, assumption) 

10277  673 
done 
674 

10249  675 

676 
subsubsection {* Monotonicity of multiset union *} 

677 

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

683 
apply (simp add: union_assoc) 

684 
done 

685 

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

687 
apply (unfold less_multiset_def mult_def) 

23751  688 
apply (erule trancl_induct) 
689 
apply (blast intro: mult1_union transI order_less_trans r_into_trancl) 

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

10249  691 
done 
692 

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

694 
apply (subst union_commute [of B C]) 

695 
apply (subst union_commute [of D C]) 

696 
apply (erule union_less_mono2) 

697 
done 

698 

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

702 
done 

703 

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

10249  708 

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

712 
prefer 2 

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

23751  716 
apply (simp only: trans_def, auto) 
10249  717 
done 
718 

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

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

23611  728 
instance multiset :: (order) pordered_ab_semigroup_add 
729 
apply intro_classes 

730 
apply(erule union_le_mono[OF mult_le_refl]) 

731 
done 

15072  732 

17200  733 
subsection {* Link with lists *} 
15072  734 

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

738 
"multiset_of [] = {#}" 

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

740 

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

18258  742 
by (induct x) auto 
15072  743 

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

18258  745 
by (induct x) auto 
15072  746 

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

18258  748 
by (induct x) auto 
15867  749 

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

751 
by (induct xs) auto 

15072  752 

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

20503  755 
by (induct xs arbitrary: ys) (auto simp: union_ac) 
18730  756 

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

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

10249  761 
done 
762 

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

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

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

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

778 

17200  779 
lemma set_eq_iff_multiset_of_eq_distinct: 
780 
"\<lbrakk>distinct x; distinct y\<rbrakk> 

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

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

788 
apply (drule distinct_remdups[THEN distinct_remdups 

789 
[THEN set_eq_iff_multiset_of_eq_distinct[THEN iffD2]]]) 

15072  790 
apply simp 
10249  791 
done 
792 

18258  793 
lemma multiset_of_compl_union [simp]: 
23281  794 
"multiset_of [x\<leftarrow>xs. P x] + multiset_of [x\<leftarrow>xs. \<not>P x] = multiset_of xs" 
15630  795 
by (induct xs) (auto simp: union_ac) 
15072  796 

17200  797 
lemma count_filter: 
23281  798 
"count (multiset_of xs) x = length [y \<leftarrow> xs. y = x]" 
18258  799 
by (induct xs) auto 
15867  800 

801 

15072  802 
subsection {* Pointwise ordering induced by count *} 
803 

19086  804 
definition 
23611  805 
mset_le :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<le>#" 50) where 
806 
"(A \<le># B) = (\<forall>a. count A a \<le> count B a)" 

807 
definition 

808 
mset_less :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<#" 50) where 

809 
"(A <# B) = (A \<le># B \<and> A \<noteq> B)" 

15072  810 

23611  811 
lemma mset_le_refl[simp]: "A \<le># A" 
18730  812 
unfolding mset_le_def by auto 
15072  813 

23611  814 
lemma mset_le_trans: "\<lbrakk> A \<le># B; B \<le># C \<rbrakk> \<Longrightarrow> A \<le># C" 
18730  815 
unfolding mset_le_def by (fast intro: order_trans) 
15072  816 

23611  817 
lemma mset_le_antisym: "\<lbrakk> A \<le># B; B \<le># A \<rbrakk> \<Longrightarrow> A = B" 
17200  818 
apply (unfold mset_le_def) 
819 
apply (rule multiset_eq_conv_count_eq[THEN iffD2]) 

15072  820 
apply (blast intro: order_antisym) 
821 
done 

822 

17200  823 
lemma mset_le_exists_conv: 
23611  824 
"(A \<le># B) = (\<exists>C. B = A + C)" 
825 
apply (unfold mset_le_def, rule iffI, rule_tac x = "B  A" in exI) 

15072  826 
apply (auto intro: multiset_eq_conv_count_eq [THEN iffD2]) 
827 
done 

828 

23611  829 
lemma mset_le_mono_add_right_cancel[simp]: "(A + C \<le># B + C) = (A \<le># B)" 
18730  830 
unfolding mset_le_def by auto 
15072  831 

23611  832 
lemma mset_le_mono_add_left_cancel[simp]: "(C + A \<le># C + B) = (A \<le># B)" 
18730  833 
unfolding mset_le_def by auto 
15072  834 

23611  835 
lemma mset_le_mono_add: "\<lbrakk> A \<le># B; C \<le># D \<rbrakk> \<Longrightarrow> A + C \<le># B + D" 
17200  836 
apply (unfold mset_le_def) 
837 
apply auto 

15072  838 
apply (erule_tac x=a in allE)+ 
839 
apply auto 

840 
done 

841 

23611  842 
lemma mset_le_add_left[simp]: "A \<le># A + B" 
18730  843 
unfolding mset_le_def by auto 
15072  844 

23611  845 
lemma mset_le_add_right[simp]: "B \<le># A + B" 
18730  846 
unfolding mset_le_def by auto 
15072  847 

23611  848 
lemma multiset_of_remdups_le: "multiset_of (remdups xs) \<le># multiset_of xs" 
849 
apply (induct xs) 

850 
apply auto 

851 
apply (rule mset_le_trans) 

852 
apply auto 

853 
done 

854 

855 
interpretation mset_order: order["op \<le>#" "op <#"] 

856 
by(auto intro: order.intro mset_le_refl mset_le_antisym mset_le_trans 

857 
simp:mset_less_def) 

858 

859 
interpretation mset_order_cancel_semigroup: 

860 
pordered_cancel_ab_semigroup_add["op +" "op \<le>#" "op <#"] 

861 
apply(unfold_locales) 

862 
apply(erule mset_le_mono_add[OF mset_le_refl]) 

863 
done 

864 

865 
interpretation mset_order_semigroup_cancel: 

866 
pordered_ab_semigroup_add_imp_le["op +" "op \<le>#" "op <#"] 

867 
by (unfold_locales) simp 

868 

15072  869 

10249  870 
end 