author  paulson 
Mon, 22 Oct 2001 11:54:22 +0200  
changeset 11868  56db9f3a6b3e 
parent 11701  3d51fbf81c17 
child 12338  de0f4a63baa5 
permissions  rwrr 
10249  1 
(* Title: HOL/Library/Multiset.thy 
2 
ID: $Id$ 

3 
Author: Tobias Nipkow, TU Muenchen 

4 
Author: Markus Wenzel, TU Muenchen 

5 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

6 
*) 

7 

8 
header {* 

9 
\title{Multisets} 

10 
\author{Tobias Nipkow, Markus Wenzel, and Lawrence C Paulson} 

11 
*} 

12 

13 
theory Multiset = Accessible_Part: 

14 

15 
subsection {* The type of multisets *} 

16 

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

18 
proof 

11464  19 
show "(\<lambda>x. 0::nat) \<in> ?multiset" by simp 
10249  20 
qed 
21 

22 
lemmas multiset_typedef [simp] = 

10277  23 
Abs_multiset_inverse Rep_multiset_inverse Rep_multiset 
24 
and [simp] = Rep_multiset_inject [symmetric] 

10249  25 

26 
constdefs 

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

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

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

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

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

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

34 
"count == Rep_multiset" 

35 

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

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

39 
syntax 

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

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

42 
translations 

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

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

46 
constdefs 

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

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

49 

10313  50 
instance multiset :: ("term") plus .. 
51 
instance multiset :: ("term") minus .. 

52 
instance multiset :: ("term") 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 

60 

61 
text {* 

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

63 
*} 

64 

11464  65 
lemma const0_in_multiset [simp]: "(\<lambda>a. 0) \<in> multiset" 
10249  66 
apply (simp add: multiset_def) 
67 
done 

68 

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

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

72 

73 
lemma union_preserves_multiset [simp]: 

11464  74 
"M \<in> multiset ==> N \<in> multiset ==> (\<lambda>a. M a + N a) \<in> multiset" 
10249  75 
apply (unfold multiset_def) 
76 
apply simp 

77 
apply (drule finite_UnI) 

78 
apply assumption 

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" 
10249  84 
apply (unfold multiset_def) 
85 
apply simp 

86 
apply (rule finite_subset) 

87 
prefer 2 

88 
apply assumption 

89 
apply auto 

90 
done 

91 

92 

93 
subsection {* Algebraic properties of multisets *} 

94 

95 
subsubsection {* Union *} 

96 

11464  97 
theorem union_empty [simp]: "M + {#} = M \<and> {#} + M = M" 
10249  98 
apply (simp add: union_def Mempty_def) 
99 
done 

100 

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

102 
apply (simp add: union_def add_ac) 

103 
done 

104 

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

106 
apply (simp add: union_def add_ac) 

107 
done 

108 

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

110 
apply (rule union_commute [THEN trans]) 

111 
apply (rule union_assoc [THEN trans]) 

112 
apply (rule union_commute [THEN arg_cong]) 

113 
done 

114 

115 
theorems union_ac = union_assoc union_commute union_lcomm 

116 

10277  117 
instance multiset :: ("term") plus_ac0 
118 
apply intro_classes 

119 
apply (rule union_commute) 

120 
apply (rule union_assoc) 

121 
apply simp 

122 
done 

123 

10249  124 

125 
subsubsection {* Difference *} 

126 

11464  127 
theorem diff_empty [simp]: "M  {#} = M \<and> {#}  M = {#}" 
10249  128 
apply (simp add: Mempty_def diff_def) 
129 
done 

130 

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

132 
apply (simp add: union_def diff_def) 

133 
done 

134 

135 

136 
subsubsection {* Count of elements *} 

137 

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

139 
apply (simp add: count_def Mempty_def) 

140 
done 

141 

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

142 
theorem count_single [simp]: "count {#b#} a = (if b = a then 1 else 0)" 
10249  143 
apply (simp add: count_def single_def) 
144 
done 

145 

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

147 
apply (simp add: count_def union_def) 

148 
done 

149 

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

151 
apply (simp add: count_def diff_def) 

152 
done 

153 

154 

155 
subsubsection {* Set of elements *} 

156 

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

158 
apply (simp add: set_of_def) 

159 
done 

160 

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

162 
apply (simp add: set_of_def) 

163 
done 

164 

11464  165 
theorem set_of_union [simp]: "set_of (M + N) = set_of M \<union> set_of N" 
10249  166 
apply (auto simp add: set_of_def) 
167 
done 

168 

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

170 
apply (auto simp add: set_of_def Mempty_def count_def expand_fun_eq) 

171 
done 

172 

11464  173 
theorem mem_set_of_iff [simp]: "(x \<in> set_of M) = (x :# M)" 
10249  174 
apply (auto simp add: set_of_def) 
175 
done 

176 

177 

178 
subsubsection {* Size *} 

179 

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

181 
apply (simp add: size_def) 

182 
done 

183 

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

185 
apply (simp add: size_def) 

186 
done 

187 

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

189 
apply (cut_tac x = M in Rep_multiset) 

190 
apply (simp add: multiset_def set_of_def count_def) 

191 
done 

192 

193 
theorem setsum_count_Int: 

11464  194 
"finite A ==> setsum (count N) (A \<inter> set_of N) = setsum (count N) A" 
10249  195 
apply (erule finite_induct) 
196 
apply simp 

197 
apply (simp add: Int_insert_left set_of_def) 

198 
done 

199 

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

201 
apply (unfold size_def) 

11464  202 
apply (subgoal_tac "count (M + N) = (\<lambda>a. count M a + count N a)") 
10249  203 
prefer 2 
204 
apply (rule ext) 

205 
apply simp 

206 
apply (simp (no_asm_simp) add: setsum_Un setsum_addf setsum_count_Int) 

207 
apply (subst Int_commute) 

208 
apply (simp (no_asm_simp) add: setsum_count_Int) 

209 
done 

210 

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

212 
apply (unfold size_def Mempty_def count_def) 

213 
apply auto 

214 
apply (simp add: set_of_def count_def expand_fun_eq) 

215 
done 

216 

11464  217 
theorem size_eq_Suc_imp_elem: "size M = Suc n ==> \<exists>a. a :# M" 
10249  218 
apply (unfold size_def) 
219 
apply (drule setsum_SucD) 

220 
apply auto 

221 
done 

222 

223 

224 
subsubsection {* Equality of multisets *} 

225 

11464  226 
theorem multiset_eq_conv_count_eq: "(M = N) = (\<forall>a. count M a = count N a)" 
10249  227 
apply (simp add: count_def expand_fun_eq) 
228 
done 

229 

11464  230 
theorem single_not_empty [simp]: "{#a#} \<noteq> {#} \<and> {#} \<noteq> {#a#}" 
10249  231 
apply (simp add: single_def Mempty_def expand_fun_eq) 
232 
done 

233 

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

235 
apply (auto simp add: single_def expand_fun_eq) 

236 
done 

237 

11464  238 
theorem union_eq_empty [iff]: "(M + N = {#}) = (M = {#} \<and> N = {#})" 
10249  239 
apply (auto simp add: union_def Mempty_def expand_fun_eq) 
240 
done 

241 

11464  242 
theorem empty_eq_union [iff]: "({#} = M + N) = (M = {#} \<and> N = {#})" 
10249  243 
apply (auto simp add: union_def Mempty_def expand_fun_eq) 
244 
done 

245 

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

247 
apply (simp add: union_def expand_fun_eq) 

248 
done 

249 

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

251 
apply (simp add: union_def expand_fun_eq) 

252 
done 

253 

254 
theorem union_is_single: 

11464  255 
"(M + N = {#a#}) = (M = {#a#} \<and> N={#} \<or> M = {#} \<and> N = {#a#})" 
10249  256 
apply (unfold Mempty_def single_def union_def) 
257 
apply (simp add: add_is_1 expand_fun_eq) 

258 
apply blast 

259 
done 

260 

261 
theorem single_is_union: 

262 
"({#a#} = M + N) = 

11464  263 
({#a#} = M \<and> N = {#} \<or> M = {#} \<and> {#a#} = N)" 
10249  264 
apply (unfold Mempty_def single_def union_def) 
11464  265 
apply (simp add: add_is_1 one_is_add expand_fun_eq) 
10249  266 
apply (blast dest: sym) 
267 
done 

268 

269 
theorem add_eq_conv_diff: 

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

11464  271 
(M = N \<and> a = b \<or> 
272 
M = N  {#a#} + {#b#} \<and> N = M  {#b#} + {#a#})" 

10249  273 
apply (unfold single_def union_def diff_def) 
274 
apply (simp (no_asm) add: expand_fun_eq) 

275 
apply (rule conjI) 

276 
apply force 

11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

277 
apply safe 
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

278 
apply (simp_all add: eq_sym_conv) 
10249  279 
done 
280 

281 
(* 

282 
val prems = Goal 

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

11464  284 
by (res_inst_tac [("a","F"),("f","\<lambda>A. if finite A then card A else 0")] 
10249  285 
measure_induct 1); 
286 
by (Clarify_tac 1); 

287 
by (resolve_tac prems 1); 

288 
by (assume_tac 1); 

289 
by (Clarify_tac 1); 

290 
by (subgoal_tac "finite G" 1); 

291 
by (fast_tac (claset() addDs [finite_subset,order_less_le RS iffD1]) 2); 

292 
by (etac allE 1); 

293 
by (etac impE 1); 

294 
by (Blast_tac 2); 

295 
by (asm_simp_tac (simpset() addsimps [psubset_card]) 1); 

296 
no_qed(); 

297 
val lemma = result(); 

298 

299 
val prems = Goal 

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

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

302 
by (REPEAT(ares_tac prems 1)); 

303 
qed "finite_psubset_induct"; 

304 

305 
Better: use wf_finite_psubset in WF_Rel 

306 
*) 

307 

308 

309 
subsection {* Induction over multisets *} 

310 

311 
lemma setsum_decr: 

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

312 
"finite F ==> (0::nat) < f a ==> 
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11655
diff
changeset

313 
setsum (f (a := f a  1)) F = (if a \<in> F then setsum f F  1 else setsum f F)" 
10249  314 
apply (erule finite_induct) 
315 
apply auto 

316 
apply (drule_tac a = a in mk_disjoint_insert) 

317 
apply auto 

318 
done 

319 

10313  320 
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

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

10249  326 
show ?thesis 
327 
apply (unfold multiset_def) 

328 
apply (induct_tac n) 

329 
apply simp 

330 
apply clarify 

11464  331 
apply (subgoal_tac "f = (\<lambda>a.0)") 
10249  332 
apply simp 
11549  333 
apply (rule premises) 
10249  334 
apply (rule ext) 
335 
apply force 

336 
apply clarify 

337 
apply (frule setsum_SucD) 

338 
apply clarify 

339 
apply (rename_tac a) 

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

340 
apply (subgoal_tac "finite {x. 0 < (f (a := f a  1)) x}") 
10249  341 
prefer 2 
342 
apply (rule finite_subset) 

343 
prefer 2 

344 
apply assumption 

345 
apply simp 

346 
apply blast 

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

347 
apply (subgoal_tac "f = (f (a := f a  1))(a := (f (a := f a  1)) a + 1)") 
10249  348 
prefer 2 
349 
apply (rule ext) 

350 
apply (simp (no_asm_simp)) 

11549  351 
apply (erule ssubst, rule premises) 
10249  352 
apply blast 
353 
apply (erule allE, erule impE, erule_tac [2] mp) 

354 
apply blast 

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

355 
apply (simp (no_asm_simp) add: setsum_decr del: fun_upd_apply One_nat_def) 
11464  356 
apply (subgoal_tac "{x. x \<noteq> a > 0 < f x} = {x. 0 < f x}") 
10249  357 
prefer 2 
358 
apply blast 

11464  359 
apply (subgoal_tac "{x. x \<noteq> a \<and> 0 < f x} = {x. 0 < f x}  {a}") 
10249  360 
prefer 2 
361 
apply blast 

362 
apply (simp add: le_imp_diff_is_add setsum_diff1 cong: conj_cong) 

363 
done 

364 
qed 

365 

10313  366 
theorem rep_multiset_induct: 
11464  367 
"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

368 
(!!f b. f \<in> multiset ==> P f ==> P (f (b := f b + 1))) ==> P f" 
10313  369 
apply (insert rep_multiset_induct_aux) 
10249  370 
apply blast 
371 
done 

372 

373 
theorem multiset_induct [induct type: multiset]: 

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

375 
proof  

376 
note defns = union_def single_def Mempty_def 

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

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

379 
show ?thesis 

380 
apply (rule Rep_multiset_inverse [THEN subst]) 

10313  381 
apply (rule Rep_multiset [THEN rep_multiset_induct]) 
10249  382 
apply (rule prem1) 
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11655
diff
changeset

383 
apply (subgoal_tac "f (b := f b + 1) = (\<lambda>a. f a + (if a = b then 1 else 0))") 
10249  384 
prefer 2 
385 
apply (simp add: expand_fun_eq) 

386 
apply (erule ssubst) 

387 
apply (erule Abs_multiset_inverse [THEN subst]) 

388 
apply (erule prem2 [simplified]) 

389 
done 

390 
qed 

391 

392 

393 
lemma MCollect_preserves_multiset: 

11464  394 
"M \<in> multiset ==> (\<lambda>x. if P x then M x else 0) \<in> multiset" 
10249  395 
apply (simp add: multiset_def) 
396 
apply (rule finite_subset) 

397 
apply auto 

398 
done 

399 

400 
theorem count_MCollect [simp]: 

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

402 
apply (unfold count_def MCollect_def) 

403 
apply (simp add: MCollect_preserves_multiset) 

404 
done 

405 

11464  406 
theorem set_of_MCollect [simp]: "set_of {# x:M. P x #} = set_of M \<inter> {x. P x}" 
10249  407 
apply (auto simp add: set_of_def) 
408 
done 

409 

11464  410 
theorem multiset_partition: "M = {# x:M. P x #} + {# x:M. \<not> P x #}" 
10249  411 
apply (subst multiset_eq_conv_count_eq) 
412 
apply auto 

413 
done 

414 

10277  415 
declare Rep_multiset_inject [symmetric, simp del] 
10249  416 
declare multiset_typedef [simp del] 
417 

418 
theorem add_eq_conv_ex: 

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

11464  420 
(M = N \<and> a = b \<or> (\<exists>K. M = K + {#b#} \<and> N = K + {#a#}))" 
10249  421 
apply (auto simp add: add_eq_conv_diff) 
422 
done 

423 

424 

425 
subsection {* Multiset orderings *} 

426 

427 
subsubsection {* Wellfoundedness *} 

428 

429 
constdefs 

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

10249  434 

11464  435 
mult :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" 
10392  436 
"mult r == (mult1 r)\<^sup>+" 
10249  437 

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

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

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

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

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

10249  448 
let ?case1 = "?case1 {(N, M). ?R N M}" 
449 

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

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

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

10249  454 
proof (elim exE conjE) 
455 
fix a' M0' K 

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

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

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

10249  460 
by (simp only: add_eq_conv_ex) 
461 
thus ?thesis 

462 
proof (elim disjE conjE exE) 

463 
assume "M0 = M0'" "a = a'" 

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

467 
fix K' 

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

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

470 

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

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

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

474 
qed 

475 
qed 

476 
qed 

477 

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

481 
let ?W = "acc ?R" 

482 
{ 

483 
fix M M0 a 

11464  484 
assume M0: "M0 \<in> ?W" 
485 
and wf_hyp: "\<forall>b. (b, a) \<in> r > (\<forall>M \<in> ?W. M + {#b#} \<in> ?W)" 

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

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

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

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

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

10249  493 
by (rule less_add) 
11464  494 
thus "N \<in> ?W" 
10249  495 
proof (elim exE disjE conjE) 
11464  496 
fix M assume "(M, M0) \<in> ?R" and N: "N = M + {#a#}" 
497 
from acc_hyp have "(M, M0) \<in> ?R > M + {#a#} \<in> ?W" .. 

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

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

10249  500 
next 
501 
fix K 

502 
assume N: "N = M0 + K" 

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

10249  505 
proof (induct K) 
11464  506 
from M0 have "M0 + {#} \<in> ?W" by simp 
10249  507 
thus "?P {#}" .. 
508 

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

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

511 
proof 

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

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

10249  515 

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

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

10249  519 
qed 
520 
qed 

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

10249  523 
qed 
524 
qed 

525 
} note tedious_reasoning = this 

526 

527 
assume wf: "wf r" 

528 
fix M 

11464  529 
show "M \<in> ?W" 
10249  530 
proof (induct M) 
11464  531 
show "{#} \<in> ?W" 
10249  532 
proof (rule accI) 
11464  533 
fix b assume "(b, {#}) \<in> ?R" 
534 
with not_less_empty show "b \<in> ?W" by contradiction 

10249  535 
qed 
536 

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

10249  539 
proof induct 
540 
fix a 

11464  541 
assume "\<forall>b. (b, a) \<in> r > (\<forall>M \<in> ?W. M + {#b#} \<in> ?W)" 
542 
show "\<forall>M \<in> ?W. M + {#a#} \<in> ?W" 

10249  543 
proof 
11464  544 
fix M assume "M \<in> ?W" 
545 
thus "M + {#a#} \<in> ?W" 

10249  546 
by (rule acc_induct) (rule tedious_reasoning) 
547 
qed 

548 
qed 

11464  549 
thus "M + {#a#} \<in> ?W" .. 
10249  550 
qed 
551 
qed 

552 

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

554 
by (rule acc_wfI, rule all_accessible) 

555 

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

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

558 

559 

560 
subsubsection {* Closurefree presentation *} 

561 

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

563 

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

565 
apply (simp add: multiset_eq_conv_count_eq) 

566 
done 

567 

568 
text {* One direction. *} 

569 

570 
lemma mult_implies_one_step: 

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

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

10249  574 
apply (unfold mult_def mult1_def set_of_def) 
575 
apply (erule converse_trancl_induct) 

576 
apply clarify 

577 
apply (rule_tac x = M0 in exI) 

578 
apply simp 

579 
apply clarify 

580 
apply (case_tac "a :# K") 

581 
apply (rule_tac x = I in exI) 

582 
apply (simp (no_asm)) 

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

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

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

588 
apply blast 

589 
apply (subgoal_tac "a :# I") 

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

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

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

593 
apply (rule conjI) 

594 
apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split) 

595 
apply (rule conjI) 

11464  596 
apply (drule_tac f = "\<lambda>M. M  {#a#}" in arg_cong) 
10249  597 
apply simp 
598 
apply (simp add: multiset_eq_conv_count_eq split: nat_diff_split) 

599 
apply (simp (no_asm_use) add: trans_def) 

600 
apply blast 

10277  601 
apply (subgoal_tac "a :# (M0 + {#a#})") 
10249  602 
apply simp 
603 
apply (simp (no_asm)) 

604 
done 

605 

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

607 
apply (simp add: multiset_eq_conv_count_eq) 

608 
done 

609 

11464  610 
lemma size_eq_Suc_imp_eq_union: "size M = Suc n ==> \<exists>a N. M = N + {#a#}" 
10249  611 
apply (erule size_eq_Suc_imp_elem [THEN exE]) 
612 
apply (drule elem_imp_eq_diff_union) 

613 
apply auto 

614 
done 

615 

616 
lemma one_step_implies_mult_aux: 

617 
"trans r ==> 

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

10249  620 
apply (induct_tac n) 
621 
apply auto 

622 
apply (frule size_eq_Suc_imp_eq_union) 

623 
apply clarify 

624 
apply (rename_tac "J'") 

625 
apply simp 

626 
apply (erule notE) 

627 
apply auto 

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

629 
apply (simp add: mult_def) 

630 
apply (rule r_into_trancl) 

631 
apply (simp add: mult1_def set_of_def) 

632 
apply blast 

11464  633 
txt {* Now we know @{term "J' \<noteq> {#}"}. *} 
634 
apply (cut_tac M = K and P = "\<lambda>x. (x, a) \<in> r" in multiset_partition) 

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

10249  636 
apply (erule ssubst) 
637 
apply (simp add: Ball_def) 

638 
apply auto 

639 
apply (subgoal_tac 

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

10249  642 
prefer 2 
643 
apply force 

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

645 
apply (erule trancl_trans) 

646 
apply (rule r_into_trancl) 

647 
apply (simp add: mult1_def set_of_def) 

648 
apply (rule_tac x = a in exI) 

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

650 
apply (simp add: union_ac) 

651 
done 

652 

653 
theorem one_step_implies_mult: 

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

10249  656 
apply (insert one_step_implies_mult_aux) 
657 
apply blast 

658 
done 

659 

660 

661 
subsubsection {* Partialorder properties *} 

662 

10313  663 
instance multiset :: ("term") ord .. 
10249  664 

665 
defs (overloaded) 

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

10249  668 

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

670 
apply (unfold trans_def) 

671 
apply (blast intro: order_less_trans) 

672 
done 

673 

674 
text {* 

675 
\medskip Irreflexivity. 

676 
*} 

677 

678 
lemma mult_irrefl_aux: 

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

682 
done 

683 

11464  684 
theorem mult_less_not_refl: "\<not> M < (M::'a::order multiset)" 
10249  685 
apply (unfold less_multiset_def) 
686 
apply auto 

687 
apply (drule trans_base_order [THEN mult_implies_one_step]) 

688 
apply auto 

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

690 
apply (simp add: set_of_eq_empty_iff) 

691 
done 

692 

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

694 
apply (insert mult_less_not_refl) 

695 
apply blast 

696 
done 

697 

698 

699 
text {* Transitivity. *} 

700 

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

702 
apply (unfold less_multiset_def mult_def) 

703 
apply (blast intro: trancl_trans) 

704 
done 

705 

706 
text {* Asymmetry. *} 

707 

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

711 
apply (erule mult_less_trans) 

712 
apply assumption 

713 
done 

714 

715 
theorem mult_less_asym: 

11464  716 
"M < N ==> (\<not> P ==> N < (M::'a::order multiset)) ==> P" 
10249  717 
apply (insert mult_less_not_sym) 
718 
apply blast 

719 
done 

720 

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

722 
apply (unfold le_multiset_def) 

723 
apply auto 

724 
done 

725 

726 
text {* Antisymmetry. *} 

727 

728 
theorem mult_le_antisym: 

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

730 
apply (unfold le_multiset_def) 

731 
apply (blast dest: mult_less_not_sym) 

732 
done 

733 

734 
text {* Transitivity. *} 

735 

736 
theorem mult_le_trans: 

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

738 
apply (unfold le_multiset_def) 

739 
apply (blast intro: mult_less_trans) 

740 
done 

741 

11655  742 
theorem mult_less_le: "(M < N) = (M <= N \<and> M \<noteq> (N::'a::order multiset))" 
10249  743 
apply (unfold le_multiset_def) 
744 
apply auto 

745 
done 

746 

10277  747 
text {* Partial order. *} 
748 

749 
instance multiset :: (order) order 

750 
apply intro_classes 

751 
apply (rule mult_le_refl) 

752 
apply (erule mult_le_trans) 

753 
apply assumption 

754 
apply (erule mult_le_antisym) 

755 
apply assumption 

756 
apply (rule mult_less_le) 

757 
done 

758 

10249  759 

760 
subsubsection {* Monotonicity of multiset union *} 

761 

762 
theorem mult1_union: 

11464  763 
"(B, D) \<in> mult1 r ==> trans r ==> (C + B, C + D) \<in> mult1 r" 
10249  764 
apply (unfold mult1_def) 
765 
apply auto 

766 
apply (rule_tac x = a in exI) 

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

768 
apply (simp add: union_assoc) 

769 
done 

770 

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

772 
apply (unfold less_multiset_def mult_def) 

773 
apply (erule trancl_induct) 

774 
apply (blast intro: mult1_union transI order_less_trans r_into_trancl) 

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

776 
done 

777 

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

779 
apply (subst union_commute [of B C]) 

780 
apply (subst union_commute [of D C]) 

781 
apply (erule union_less_mono2) 

782 
done 

783 

784 
theorem union_less_mono: 

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

786 
apply (blast intro!: union_less_mono1 union_less_mono2 mult_less_trans) 

787 
done 

788 

789 
theorem union_le_mono: 

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

791 
apply (unfold le_multiset_def) 

792 
apply (blast intro: union_less_mono union_less_mono1 union_less_mono2) 

793 
done 

794 

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

796 
apply (unfold le_multiset_def less_multiset_def) 

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

798 
prefer 2 

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

802 
apply (simp only: trans_def) 

803 
apply auto 

804 
apply (blast intro: order_less_trans) 

805 
done 

806 

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

808 
apply (subgoal_tac "A + {#} <= A + B") 

809 
prefer 2 

810 
apply (rule union_le_mono) 

811 
apply auto 

812 
done 

813 

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

815 
apply (subst union_commute, rule union_upper1) 

816 
done 

817 

818 
end 