author  nipkow 
Tue, 23 Nov 2004 16:43:03 +0100  
changeset 15316  2a6ff941a115 
parent 15140  322485b816ac 
child 15402  97204f3b4705 
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 
15140  9 
imports Accessible_Part 
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 

23 
constdefs 

24 
Mempty :: "'a multiset" ("{#}") 

11464  25 
"{#} == Abs_multiset (\<lambda>a. 0)" 
10249  26 

27 
single :: "'a => 'a multiset" ("{#_#}") 

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

28 
"{#a#} == Abs_multiset (\<lambda>b. if b = a then 1 else 0)" 
10249  29 

30 
count :: "'a multiset => 'a => nat" 

31 
"count == Rep_multiset" 

32 

33 
MCollect :: "'a multiset => ('a => bool) => 'a multiset" 

11464  34 
"MCollect M P == Abs_multiset (\<lambda>x. if P x then Rep_multiset M x else 0)" 
10249  35 

36 
syntax 

37 
"_Melem" :: "'a => 'a multiset => bool" ("(_/ :# _)" [50, 51] 50) 

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

39 
translations 

40 
"a :# M" == "0 < count M a" 

11464  41 
"{#x:M. P#}" == "MCollect M (\<lambda>x. P)" 
10249  42 

43 
constdefs 

44 
set_of :: "'a multiset => 'a set" 

45 
"set_of M == {x. x :# M}" 

46 

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

49 
defs (overloaded) 

11464  50 
union_def: "M + N == Abs_multiset (\<lambda>a. Rep_multiset M a + Rep_multiset N a)" 
51 
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

52 
Zero_multiset_def [simp]: "0 == {#}" 
10249  53 
size_def: "size M == setsum (count M) (set_of M)" 
54 

55 

56 
text {* 

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

58 
*} 

59 

11464  60 
lemma const0_in_multiset [simp]: "(\<lambda>a. 0) \<in> multiset" 
15072  61 
by (simp add: multiset_def) 
10249  62 

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

63 
lemma only1_in_multiset [simp]: "(\<lambda>b. if b = a then 1 else 0) \<in> multiset" 
15072  64 
by (simp add: multiset_def) 
10249  65 

66 
lemma union_preserves_multiset [simp]: 

11464  67 
"M \<in> multiset ==> N \<in> multiset ==> (\<lambda>a. M a + N a) \<in> multiset" 
15072  68 
apply (unfold multiset_def, simp) 
69 
apply (drule finite_UnI, assumption) 

10249  70 
apply (simp del: finite_Un add: Un_def) 
71 
done 

72 

73 
lemma diff_preserves_multiset [simp]: 

11464  74 
"M \<in> multiset ==> (\<lambda>a. M a  N a) \<in> multiset" 
15072  75 
apply (unfold multiset_def, simp) 
10249  76 
apply (rule finite_subset) 
77 
prefer 2 

78 
apply assumption 

79 
apply auto 

80 
done 

81 

82 

83 
subsection {* Algebraic properties of multisets *} 

84 

85 
subsubsection {* Union *} 

86 

11464  87 
theorem union_empty [simp]: "M + {#} = M \<and> {#} + M = M" 
15072  88 
by (simp add: union_def Mempty_def) 
10249  89 

90 
theorem union_commute: "M + N = N + (M::'a multiset)" 

15072  91 
by (simp add: union_def add_ac) 
10249  92 

93 
theorem union_assoc: "(M + N) + K = M + (N + (K::'a multiset))" 

15072  94 
by (simp add: union_def add_ac) 
10249  95 

96 
theorem union_lcomm: "M + (N + K) = N + (M + (K::'a multiset))" 

97 
apply (rule union_commute [THEN trans]) 

98 
apply (rule union_assoc [THEN trans]) 

99 
apply (rule union_commute [THEN arg_cong]) 

100 
done 

101 

102 
theorems union_ac = union_assoc union_commute union_lcomm 

103 

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

105 
proof 
8e739a6eaf11
replaced applystyle proof for instance Multiset :: plus_ac0 by recommended Isar proof style
obua
parents:
14706
diff
changeset

106 
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

107 
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

108 
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

109 
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

110 
qed 
10277  111 

10249  112 

113 
subsubsection {* Difference *} 

114 

11464  115 
theorem diff_empty [simp]: "M  {#} = M \<and> {#}  M = {#}" 
15072  116 
by (simp add: Mempty_def diff_def) 
10249  117 

118 
theorem diff_union_inverse2 [simp]: "M + {#a#}  {#a#} = M" 

15072  119 
by (simp add: union_def diff_def) 
10249  120 

121 

122 
subsubsection {* Count of elements *} 

123 

124 
theorem count_empty [simp]: "count {#} a = 0" 

15072  125 
by (simp add: count_def Mempty_def) 
10249  126 

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

127 
theorem count_single [simp]: "count {#b#} a = (if b = a then 1 else 0)" 
15072  128 
by (simp add: count_def single_def) 
10249  129 

130 
theorem count_union [simp]: "count (M + N) a = count M a + count N a" 

15072  131 
by (simp add: count_def union_def) 
10249  132 

133 
theorem count_diff [simp]: "count (M  N) a = count M a  count N a" 

15072  134 
by (simp add: count_def diff_def) 
10249  135 

136 

137 
subsubsection {* Set of elements *} 

138 

139 
theorem set_of_empty [simp]: "set_of {#} = {}" 

15072  140 
by (simp add: set_of_def) 
10249  141 

142 
theorem set_of_single [simp]: "set_of {#b#} = {b}" 

15072  143 
by (simp add: set_of_def) 
10249  144 

11464  145 
theorem set_of_union [simp]: "set_of (M + N) = set_of M \<union> set_of N" 
15072  146 
by (auto simp add: set_of_def) 
10249  147 

148 
theorem set_of_eq_empty_iff [simp]: "(set_of M = {}) = (M = {#})" 

15072  149 
by (auto simp add: set_of_def Mempty_def count_def expand_fun_eq) 
10249  150 

11464  151 
theorem mem_set_of_iff [simp]: "(x \<in> set_of M) = (x :# M)" 
15072  152 
by (auto simp add: set_of_def) 
10249  153 

154 

155 
subsubsection {* Size *} 

156 

157 
theorem size_empty [simp]: "size {#} = 0" 

15072  158 
by (simp add: size_def) 
10249  159 

160 
theorem size_single [simp]: "size {#b#} = 1" 

15072  161 
by (simp add: size_def) 
10249  162 

163 
theorem finite_set_of [iff]: "finite (set_of M)" 

164 
apply (cut_tac x = M in Rep_multiset) 

165 
apply (simp add: multiset_def set_of_def count_def) 

166 
done 

167 

168 
theorem setsum_count_Int: 

11464  169 
"finite A ==> setsum (count N) (A \<inter> set_of N) = setsum (count N) A" 
15072  170 
apply (erule finite_induct, simp) 
10249  171 
apply (simp add: Int_insert_left set_of_def) 
172 
done 

173 

174 
theorem size_union [simp]: "size (M + N::'a multiset) = size M + size N" 

175 
apply (unfold size_def) 

11464  176 
apply (subgoal_tac "count (M + N) = (\<lambda>a. count M a + count N a)") 
10249  177 
prefer 2 
15072  178 
apply (rule ext, simp) 
10249  179 
apply (simp (no_asm_simp) add: setsum_Un setsum_addf setsum_count_Int) 
180 
apply (subst Int_commute) 

181 
apply (simp (no_asm_simp) add: setsum_count_Int) 

182 
done 

183 

184 
theorem size_eq_0_iff_empty [iff]: "(size M = 0) = (M = {#})" 

15072  185 
apply (unfold size_def Mempty_def count_def, auto) 
10249  186 
apply (simp add: set_of_def count_def expand_fun_eq) 
187 
done 

188 

11464  189 
theorem size_eq_Suc_imp_elem: "size M = Suc n ==> \<exists>a. a :# M" 
10249  190 
apply (unfold size_def) 
15072  191 
apply (drule setsum_SucD, auto) 
10249  192 
done 
193 

194 

195 
subsubsection {* Equality of multisets *} 

196 

11464  197 
theorem multiset_eq_conv_count_eq: "(M = N) = (\<forall>a. count M a = count N a)" 
15072  198 
by (simp add: count_def expand_fun_eq) 
10249  199 

11464  200 
theorem single_not_empty [simp]: "{#a#} \<noteq> {#} \<and> {#} \<noteq> {#a#}" 
15072  201 
by (simp add: single_def Mempty_def expand_fun_eq) 
10249  202 

203 
theorem single_eq_single [simp]: "({#a#} = {#b#}) = (a = b)" 

15072  204 
by (auto simp add: single_def expand_fun_eq) 
10249  205 

11464  206 
theorem union_eq_empty [iff]: "(M + N = {#}) = (M = {#} \<and> N = {#})" 
15072  207 
by (auto simp add: union_def Mempty_def expand_fun_eq) 
10249  208 

11464  209 
theorem empty_eq_union [iff]: "({#} = M + N) = (M = {#} \<and> N = {#})" 
15072  210 
by (auto simp add: union_def Mempty_def expand_fun_eq) 
10249  211 

212 
theorem union_right_cancel [simp]: "(M + K = N + K) = (M = (N::'a multiset))" 

15072  213 
by (simp add: union_def expand_fun_eq) 
10249  214 

215 
theorem union_left_cancel [simp]: "(K + M = K + N) = (M = (N::'a multiset))" 

15072  216 
by (simp add: union_def expand_fun_eq) 
10249  217 

218 
theorem union_is_single: 

11464  219 
"(M + N = {#a#}) = (M = {#a#} \<and> N={#} \<or> M = {#} \<and> N = {#a#})" 
15072  220 
apply (simp add: Mempty_def single_def union_def add_is_1 expand_fun_eq) 
10249  221 
apply blast 
222 
done 

223 

224 
theorem single_is_union: 

15072  225 
"({#a#} = M + N) = ({#a#} = M \<and> N = {#} \<or> M = {#} \<and> {#a#} = N)" 
10249  226 
apply (unfold Mempty_def single_def union_def) 
11464  227 
apply (simp add: add_is_1 one_is_add expand_fun_eq) 
10249  228 
apply (blast dest: sym) 
229 
done 

230 

231 
theorem add_eq_conv_diff: 

232 
"(M + {#a#} = N + {#b#}) = 

15072  233 
(M = N \<and> a = b \<or> M = N  {#a#} + {#b#} \<and> N = M  {#b#} + {#a#})" 
10249  234 
apply (unfold single_def union_def diff_def) 
235 
apply (simp (no_asm) add: expand_fun_eq) 

15072  236 
apply (rule conjI, force, safe, simp_all) 
13601  237 
apply (simp add: eq_sym_conv) 
10249  238 
done 
239 

240 
(* 

241 
val prems = Goal 

242 
"[ !!F. [ finite F; !G. G < F > P G ] ==> P F ] ==> finite F > P F"; 

11464  243 
by (res_inst_tac [("a","F"),("f","\<lambda>A. if finite A then card A else 0")] 
10249  244 
measure_induct 1); 
15072  245 
by (Clarify_tac 1) 
246 
by (resolve_tac prems 1) 

247 
by (assume_tac 1) 

248 
by (Clarify_tac 1) 

249 
by (subgoal_tac "finite G" 1) 

10249  250 
by (fast_tac (claset() addDs [finite_subset,order_less_le RS iffD1]) 2); 
15072  251 
by (etac allE 1) 
252 
by (etac impE 1) 

253 
by (Blast_tac 2) 

10249  254 
by (asm_simp_tac (simpset() addsimps [psubset_card]) 1); 
255 
no_qed(); 

256 
val lemma = result(); 

257 

258 
val prems = Goal 

259 
"[ finite F; !!F. [ finite F; !G. G < F > P G ] ==> P F ] ==> P F"; 

260 
by (rtac (lemma RS mp) 1); 

261 
by (REPEAT(ares_tac prems 1)); 

262 
qed "finite_psubset_induct"; 

263 

264 
Better: use wf_finite_psubset in WF_Rel 

265 
*) 

266 

267 

268 
subsection {* Induction over multisets *} 

269 

270 
lemma setsum_decr: 

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

271 
"finite F ==> (0::nat) < f a ==> 
15072  272 
setsum (f (a := f a  1)) F = (if a\<in>F then setsum f F  1 else setsum f F)" 
273 
apply (erule finite_induct, auto) 

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

10249  275 
done 
276 

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

278 
"P (\<lambda>a. (0::nat)) ==> (!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1))) 
11464  279 
==> \<forall>f. f \<in> multiset > setsum f {x. 0 < f x} = n > P f" 
10249  280 
proof  
11549  281 
case rule_context 
282 
note premises = this [unfolded multiset_def] 

10249  283 
show ?thesis 
284 
apply (unfold multiset_def) 

15072  285 
apply (induct_tac n, simp, clarify) 
11464  286 
apply (subgoal_tac "f = (\<lambda>a.0)") 
10249  287 
apply simp 
11549  288 
apply (rule premises) 
15072  289 
apply (rule ext, force, clarify) 
290 
apply (frule setsum_SucD, clarify) 

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

292 
apply (subgoal_tac "finite {x. 0 < (f (a := f a  1)) x}") 
10249  293 
prefer 2 
294 
apply (rule finite_subset) 

295 
prefer 2 

296 
apply assumption 

297 
apply simp 

298 
apply blast 

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

299 
apply (subgoal_tac "f = (f (a := f a  1))(a := (f (a := f a  1)) a + 1)") 
10249  300 
prefer 2 
301 
apply (rule ext) 

302 
apply (simp (no_asm_simp)) 

15072  303 
apply (erule ssubst, rule premises, blast) 
304 
apply (erule allE, erule impE, erule_tac [2] mp, blast) 

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

305 
apply (simp (no_asm_simp) add: setsum_decr del: fun_upd_apply One_nat_def) 
11464  306 
apply (subgoal_tac "{x. x \<noteq> a > 0 < f x} = {x. 0 < f x}") 
10249  307 
prefer 2 
308 
apply blast 

11464  309 
apply (subgoal_tac "{x. x \<noteq> a \<and> 0 < f x} = {x. 0 < f x}  {a}") 
10249  310 
prefer 2 
311 
apply blast 

15316  312 
apply (simp add: le_imp_diff_is_add setsum_diff1_nat cong: conj_cong) 
10249  313 
done 
314 
qed 

315 

10313  316 
theorem rep_multiset_induct: 
11464  317 
"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

318 
(!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1))) ==> P f" 
15072  319 
by (insert rep_multiset_induct_aux, blast) 
10249  320 

321 
theorem multiset_induct [induct type: multiset]: 

322 
"P {#} ==> (!!M x. P M ==> P (M + {#x#})) ==> P M" 

323 
proof  

324 
note defns = union_def single_def Mempty_def 

325 
assume prem1 [unfolded defns]: "P {#}" 

326 
assume prem2 [unfolded defns]: "!!M x. P M ==> P (M + {#x#})" 

327 
show ?thesis 

328 
apply (rule Rep_multiset_inverse [THEN subst]) 

10313  329 
apply (rule Rep_multiset [THEN rep_multiset_induct]) 
10249  330 
apply (rule prem1) 
15072  331 
apply (subgoal_tac "f(b := f b + 1) = (\<lambda>a. f a + (if a=b then 1 else 0))") 
10249  332 
prefer 2 
333 
apply (simp add: expand_fun_eq) 

334 
apply (erule ssubst) 

335 
apply (erule Abs_multiset_inverse [THEN subst]) 

336 
apply (erule prem2 [simplified]) 

337 
done 

338 
qed 

339 

340 

341 
lemma MCollect_preserves_multiset: 

11464  342 
"M \<in> multiset ==> (\<lambda>x. if P x then M x else 0) \<in> multiset" 
10249  343 
apply (simp add: multiset_def) 
15072  344 
apply (rule finite_subset, auto) 
10249  345 
done 
346 

347 
theorem count_MCollect [simp]: 

348 
"count {# x:M. P x #} a = (if P a then count M a else 0)" 

15072  349 
by (simp add: count_def MCollect_def MCollect_preserves_multiset) 
10249  350 

11464  351 
theorem set_of_MCollect [simp]: "set_of {# x:M. P x #} = set_of M \<inter> {x. P x}" 
15072  352 
by (auto simp add: set_of_def) 
10249  353 

11464  354 
theorem multiset_partition: "M = {# x:M. P x #} + {# x:M. \<not> P x #}" 
15072  355 
by (subst multiset_eq_conv_count_eq, auto) 
10249  356 

10277  357 
declare Rep_multiset_inject [symmetric, simp del] 
10249  358 
declare multiset_typedef [simp del] 
359 

360 
theorem add_eq_conv_ex: 

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

363 
by (auto simp add: add_eq_conv_diff) 

10249  364 

365 

366 
subsection {* Multiset orderings *} 

367 

368 
subsubsection {* Wellfoundedness *} 

369 

370 
constdefs 

11464  371 
mult1 :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" 
10249  372 
"mult1 r == 
11464  373 
{(N, M). \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and> 
374 
(\<forall>b. b :# K > (b, a) \<in> r)}" 

10249  375 

11464  376 
mult :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" 
10392  377 
"mult r == (mult1 r)\<^sup>+" 
10249  378 

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

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

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

385 
(concl is "?case1 (mult1 r) \<or> ?case2") 

10249  386 
proof (unfold mult1_def) 
11464  387 
let ?r = "\<lambda>K a. \<forall>b. b :# K > (b, a) \<in> r" 
388 
let ?R = "\<lambda>N M. \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and> ?r K a" 

10249  389 
let ?case1 = "?case1 {(N, M). ?R N M}" 
390 

11464  391 
assume "(N, M0 + {#a#}) \<in> {(N, M). ?R N M}" 
392 
hence "\<exists>a' M0' K. 

393 
M0 + {#a#} = M0' + {#a'#} \<and> N = M0' + K \<and> ?r K a'" by simp 

394 
thus "?case1 \<or> ?case2" 

10249  395 
proof (elim exE conjE) 
396 
fix a' M0' K 

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

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

11464  399 
hence "M0 = M0' \<and> a = a' \<or> 
400 
(\<exists>K'. M0 = K' + {#a'#} \<and> M0' = K' + {#a#})" 

10249  401 
by (simp only: add_eq_conv_ex) 
402 
thus ?thesis 

403 
proof (elim disjE conjE exE) 

404 
assume "M0 = M0'" "a = a'" 

11464  405 
with N r have "?r K a \<and> N = M0 + K" by simp 
10249  406 
hence ?case2 .. thus ?thesis .. 
407 
next 

408 
fix K' 

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

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

411 

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

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

414 
with n have ?case1 by simp thus ?thesis .. 

415 
qed 

416 
qed 

417 
qed 

418 

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

422 
let ?W = "acc ?R" 

423 
{ 

424 
fix M M0 a 

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

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

11464  431 
assume "(N, M0 + {#a#}) \<in> ?R" 
432 
hence "((\<exists>M. (M, M0) \<in> ?R \<and> N = M + {#a#}) \<or> 

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

10249  434 
by (rule less_add) 
11464  435 
thus "N \<in> ?W" 
10249  436 
proof (elim exE disjE conjE) 
11464  437 
fix M assume "(M, M0) \<in> ?R" and N: "N = M + {#a#}" 
438 
from acc_hyp have "(M, M0) \<in> ?R > M + {#a#} \<in> ?W" .. 

439 
hence "M + {#a#} \<in> ?W" .. 

440 
thus "N \<in> ?W" by (simp only: N) 

10249  441 
next 
442 
fix K 

443 
assume N: "N = M0 + K" 

11464  444 
assume "\<forall>b. b :# K > (b, a) \<in> r" 
445 
have "?this > M0 + K \<in> ?W" (is "?P K") 

10249  446 
proof (induct K) 
11464  447 
from M0 have "M0 + {#} \<in> ?W" by simp 
10249  448 
thus "?P {#}" .. 
449 

450 
fix K x assume hyp: "?P K" 

451 
show "?P (K + {#x#})" 

452 
proof 

11464  453 
assume a: "\<forall>b. b :# (K + {#x#}) > (b, a) \<in> r" 
454 
hence "(x, a) \<in> r" by simp 

455 
with wf_hyp have b: "\<forall>M \<in> ?W. M + {#x#} \<in> ?W" by blast 

10249  456 

11464  457 
from a hyp have "M0 + K \<in> ?W" by simp 
458 
with b have "(M0 + K) + {#x#} \<in> ?W" .. 

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

10249  460 
qed 
461 
qed 

11464  462 
hence "M0 + K \<in> ?W" .. 
463 
thus "N \<in> ?W" by (simp only: N) 

10249  464 
qed 
465 
qed 

466 
} note tedious_reasoning = this 

467 

468 
assume wf: "wf r" 

469 
fix M 

11464  470 
show "M \<in> ?W" 
10249  471 
proof (induct M) 
11464  472 
show "{#} \<in> ?W" 
10249  473 
proof (rule accI) 
11464  474 
fix b assume "(b, {#}) \<in> ?R" 
475 
with not_less_empty show "b \<in> ?W" by contradiction 

10249  476 
qed 
477 

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

10249  480 
proof induct 
481 
fix a 

12399  482 
assume "!!b. (b, a) \<in> r ==> (\<forall>M \<in> ?W. M + {#b#} \<in> ?W)" 
11464  483 
show "\<forall>M \<in> ?W. M + {#a#} \<in> ?W" 
10249  484 
proof 
11464  485 
fix M assume "M \<in> ?W" 
486 
thus "M + {#a#} \<in> ?W" 

10249  487 
by (rule acc_induct) (rule tedious_reasoning) 
488 
qed 

489 
qed 

11464  490 
thus "M + {#a#} \<in> ?W" .. 
10249  491 
qed 
492 
qed 

493 

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

495 
by (rule acc_wfI, rule all_accessible) 

496 

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

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

499 

500 

501 
subsubsection {* Closurefree presentation *} 

502 

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

504 

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

15072  506 
by (simp add: multiset_eq_conv_count_eq) 
10249  507 

508 
text {* One direction. *} 

509 

510 
lemma mult_implies_one_step: 

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

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

10249  514 
apply (unfold mult_def mult1_def set_of_def) 
15072  515 
apply (erule converse_trancl_induct, clarify) 
516 
apply (rule_tac x = M0 in exI, simp, clarify) 

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

519 
apply (simp (no_asm)) 

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

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

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

525 
apply blast 

526 
apply (subgoal_tac "a :# I") 

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

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

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

530 
apply (rule conjI) 

531 
apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split) 

532 
apply (rule conjI) 

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

536 
apply blast 

10277  537 
apply (subgoal_tac "a :# (M0 + {#a#})") 
10249  538 
apply simp 
539 
apply (simp (no_asm)) 

540 
done 

541 

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

15072  543 
by (simp add: multiset_eq_conv_count_eq) 
10249  544 

11464  545 
lemma size_eq_Suc_imp_eq_union: "size M = Suc n ==> \<exists>a N. M = N + {#a#}" 
10249  546 
apply (erule size_eq_Suc_imp_elem [THEN exE]) 
15072  547 
apply (drule elem_imp_eq_diff_union, auto) 
10249  548 
done 
549 

550 
lemma one_step_implies_mult_aux: 

551 
"trans r ==> 

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

15072  554 
apply (induct_tac n, auto) 
555 
apply (frule size_eq_Suc_imp_eq_union, clarify) 

556 
apply (rename_tac "J'", simp) 

557 
apply (erule notE, auto) 

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

560 
apply (rule r_into_trancl) 

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

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

10249  565 
apply (erule ssubst) 
15072  566 
apply (simp add: Ball_def, auto) 
10249  567 
apply (subgoal_tac 
11464  568 
"((I + {# x : K. (x, a) \<in> r #}) + {# x : K. (x, a) \<notin> r #}, 
569 
(I + {# x : K. (x, a) \<in> r #}) + J') \<in> mult r") 

10249  570 
prefer 2 
571 
apply force 

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

573 
apply (erule trancl_trans) 

574 
apply (rule r_into_trancl) 

575 
apply (simp add: mult1_def set_of_def) 

576 
apply (rule_tac x = a in exI) 

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

578 
apply (simp add: union_ac) 

579 
done 

580 

581 
theorem one_step_implies_mult: 

11464  582 
"trans r ==> J \<noteq> {#} ==> \<forall>k \<in> set_of K. \<exists>j \<in> set_of J. (k, j) \<in> r 
583 
==> (I + K, I + J) \<in> mult r" 

15072  584 
apply (insert one_step_implies_mult_aux, blast) 
10249  585 
done 
586 

587 

588 
subsubsection {* Partialorder properties *} 

589 

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

590 
instance multiset :: (type) ord .. 
10249  591 

592 
defs (overloaded) 

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

10249  595 

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

597 
apply (unfold trans_def) 

598 
apply (blast intro: order_less_trans) 

599 
done 

600 

601 
text {* 

602 
\medskip Irreflexivity. 

603 
*} 

604 

605 
lemma mult_irrefl_aux: 

11464  606 
"finite A ==> (\<forall>x \<in> A. \<exists>y \<in> A. x < (y::'a::order)) > A = {}" 
10249  607 
apply (erule finite_induct) 
608 
apply (auto intro: order_less_trans) 

609 
done 

610 

11464  611 
theorem mult_less_not_refl: "\<not> M < (M::'a::order multiset)" 
15072  612 
apply (unfold less_multiset_def, auto) 
613 
apply (drule trans_base_order [THEN mult_implies_one_step], auto) 

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

616 
done 

617 

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

15072  619 
by (insert mult_less_not_refl, fast) 
10249  620 

621 

622 
text {* Transitivity. *} 

623 

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

625 
apply (unfold less_multiset_def mult_def) 

626 
apply (blast intro: trancl_trans) 

627 
done 

628 

629 
text {* Asymmetry. *} 

630 

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

15072  634 
apply (erule mult_less_trans, assumption) 
10249  635 
done 
636 

637 
theorem mult_less_asym: 

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

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

15072  642 
by (unfold le_multiset_def, auto) 
10249  643 

644 
text {* Antisymmetry. *} 

645 

646 
theorem mult_le_antisym: 

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

648 
apply (unfold le_multiset_def) 

649 
apply (blast dest: mult_less_not_sym) 

650 
done 

651 

652 
text {* Transitivity. *} 

653 

654 
theorem mult_le_trans: 

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

656 
apply (unfold le_multiset_def) 

657 
apply (blast intro: mult_less_trans) 

658 
done 

659 

11655  660 
theorem mult_less_le: "(M < N) = (M <= N \<and> M \<noteq> (N::'a::order multiset))" 
15072  661 
by (unfold le_multiset_def, auto) 
10249  662 

10277  663 
text {* Partial order. *} 
664 

665 
instance multiset :: (order) order 

666 
apply intro_classes 

667 
apply (rule mult_le_refl) 

15072  668 
apply (erule mult_le_trans, assumption) 
669 
apply (erule mult_le_antisym, assumption) 

10277  670 
apply (rule mult_less_le) 
671 
done 

672 

10249  673 

674 
subsubsection {* Monotonicity of multiset union *} 

675 

676 
theorem mult1_union: 

11464  677 
"(B, D) \<in> mult1 r ==> trans r ==> (C + B, C + D) \<in> mult1 r" 
15072  678 
apply (unfold mult1_def, auto) 
10249  679 
apply (rule_tac x = a in exI) 
680 
apply (rule_tac x = "C + M0" in exI) 

681 
apply (simp add: union_assoc) 

682 
done 

683 

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

685 
apply (unfold less_multiset_def mult_def) 

686 
apply (erule trancl_induct) 

687 
apply (blast intro: mult1_union transI order_less_trans r_into_trancl) 

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

689 
done 

690 

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

692 
apply (subst union_commute [of B C]) 

693 
apply (subst union_commute [of D C]) 

694 
apply (erule union_less_mono2) 

695 
done 

696 

697 
theorem union_less_mono: 

698 
"A < C ==> B < D ==> A + B < C + (D::'a::order multiset)" 

699 
apply (blast intro!: union_less_mono1 union_less_mono2 mult_less_trans) 

700 
done 

701 

702 
theorem union_le_mono: 

703 
"A <= C ==> B <= D ==> A + B <= C + (D::'a::order multiset)" 

704 
apply (unfold le_multiset_def) 

705 
apply (blast intro: union_less_mono union_less_mono1 union_less_mono2) 

706 
done 

707 

708 
theorem empty_leI [iff]: "{#} <= (M::'a::order multiset)" 

709 
apply (unfold le_multiset_def less_multiset_def) 

710 
apply (case_tac "M = {#}") 

711 
prefer 2 

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

15072  715 
apply (simp only: trans_def, auto) 
10249  716 
done 
717 

718 
theorem union_upper1: "A <= A + (B::'a::order multiset)" 

15072  719 
proof  
720 
have "A + {#} <= A + B" by (blast intro: union_le_mono) 

721 
thus ?thesis by simp 

722 
qed 

723 

724 
theorem union_upper2: "B <= A + (B::'a::order multiset)" 

725 
by (subst union_commute, rule union_upper1) 

726 

727 

728 
subsection {* Link with lists *} 

729 

730 
consts 

731 
multiset_of :: "'a list \<Rightarrow> 'a multiset" 

732 
primrec 

733 
"multiset_of [] = {#}" 

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

735 

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

737 
by (induct_tac x, auto) 

738 

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

740 
by (induct_tac x, auto) 

741 

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

743 
by (induct_tac x, auto) 

744 

745 
lemma multset_of_append[simp]: 

746 
"multiset_of (xs @ ys) = multiset_of xs + multiset_of ys" 

747 
by (rule_tac x=ys in spec, induct_tac xs, auto simp: union_ac) 

748 

749 
lemma surj_multiset_of: "surj multiset_of" 

750 
apply (unfold surj_def, rule allI) 

751 
apply (rule_tac M=y in multiset_induct, auto) 

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

10249  753 
done 
754 

15072  755 
lemma set_count_greater_0: "set x = {a. 0 < count (multiset_of x) a}" 
756 
by (induct_tac x, auto) 

757 

758 
lemma distinct_count_atmost_1: 

759 
"distinct x = (! a. count (multiset_of x) a = (if a \<in> set x then 1 else 0))" 

760 
apply ( induct_tac x, simp, rule iffI, simp_all) 

761 
apply (rule conjI) 

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

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

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

765 
done 

766 

767 
lemma set_eq_iff_multiset_of_eq_distinct: 

768 
"\<lbrakk>distinct x; distinct y\<rbrakk> 

769 
\<Longrightarrow> (set x = set y) = (multiset_of x = multiset_of y)" 

770 
by (auto simp: multiset_eq_conv_count_eq distinct_count_atmost_1) 

771 

772 
lemma set_eq_iff_multiset_of_remdups_eq: 

773 
"(set x = set y) = (multiset_of (remdups x) = multiset_of (remdups y))" 

774 
apply (rule iffI) 

775 
apply (simp add: set_eq_iff_multiset_of_eq_distinct[THEN iffD1]) 

776 
apply (drule distinct_remdups[THEN distinct_remdups 

777 
[THEN set_eq_iff_multiset_of_eq_distinct[THEN iffD2]]]) 

778 
apply simp 

10249  779 
done 
780 

15072  781 

782 
subsection {* Pointwise ordering induced by count *} 

783 

784 
consts 

785 
mset_le :: "['a multiset, 'a multiset] \<Rightarrow> bool" 

786 

787 
syntax 

788 
"_mset_le" :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" ("_ \<le># _" [50,51] 50) 

789 
translations 

790 
"x \<le># y" == "mset_le x y" 

791 

792 
defs 

793 
mset_le_def: "xs \<le># ys == (! a. count xs a \<le> count ys a)" 

794 

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

796 
by (unfold mset_le_def, auto) 

797 

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

799 
by (unfold mset_le_def, fast intro: order_trans) 

800 

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

802 
apply (unfold mset_le_def) 

803 
apply (rule multiset_eq_conv_count_eq[THEN iffD2]) 

804 
apply (blast intro: order_antisym) 

805 
done 

806 

807 
lemma mset_le_exists_conv: 

808 
"(xs \<le># ys) = (? zs. ys = xs + zs)" 

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

810 
apply (auto intro: multiset_eq_conv_count_eq [THEN iffD2]) 

811 
done 

812 

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

814 
by (unfold mset_le_def, auto) 

815 

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

817 
by (unfold mset_le_def, auto) 

818 

819 
lemma mset_le_mono_add: "\<lbrakk> xs \<le># ys; vs \<le># ws \<rbrakk> \<Longrightarrow> xs + vs \<le># ys + ws" 

820 
apply (unfold mset_le_def, auto) 

821 
apply (erule_tac x=a in allE)+ 

822 
apply auto 

823 
done 

824 

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

826 
by (unfold mset_le_def, auto) 

827 

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

829 
by (unfold mset_le_def, auto) 

830 

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

832 
by (induct_tac x, auto, rule mset_le_trans, auto) 

833 

10249  834 
end 