bagScript.sml
1Theory bag
2Ancestors
3 list[qualified] divides pred_set arithmetic combin
4Libs
5 boolSimps numLib Prim_rec BasicProvers metisLib mesonLib
6
7fun ARITH q = EQT_ELIM (ARITH_CONV (Parse.Term q));
8
9Type bag = “:'a -> num”
10Type multiset = “:'a -> num”
11
12val _ = print "Defining basic bag operations\n"
13
14Definition EMPTY_BAG[nocompute]:
15 (EMPTY_BAG:'a bag) = K 0
16End
17
18Theorem EMPTY_BAG_alt:
19 EMPTY_BAG:'a bag = \x.0
20Proof
21 SIMP_TAC std_ss [EMPTY_BAG, FUN_EQ_THM]
22QED
23
24Definition BAG_INN[nocompute]:
25 BAG_INN (e:'a) n b <=> b e >= n
26End
27
28Definition SUB_BAG[nocompute]:
29 SUB_BAG b1 b2 = !x n. BAG_INN x n b1 ==> BAG_INN x n b2
30End
31
32Definition PSUB_BAG[nocompute]:
33 PSUB_BAG b1 b2 <=> SUB_BAG b1 b2 /\ ~(b1 = b2)
34End
35
36
37Definition BAG_IN[nocompute]:
38 BAG_IN (e:'a) b <=> BAG_INN e 1 b
39End
40
41val _ = set_fixity "<:" (Infix(NONASSOC, 425))
42Overload "<:" = ``BAG_IN``
43val _ = Unicode.unicode_version {tmnm = "<:", u = UTF8.chr 0x22F2}
44 (* U+22F2 looks like ⋲ in your current font; unfortunately this
45 symbol doesn't seem to correspond to anything in LaTeX... *)
46val _ = TeX_notation {hol = "<:", TeX = ("\\HOLTokenIn{}:",2)}
47val _ = TeX_notation {hol = UTF8.chr 0x22F2, TeX = ("\\HOLTokenIn{}:",2)}
48
49Definition BAG_UNION[nocompute]:
50 BAG_UNION b (c:'a bag) = \x. b x + c x
51End
52Overload "+" = ``BAG_UNION``
53val _ = send_to_back_overload "+" {Name = "BAG_UNION", Thy = "bag"}
54val _ = set_fixity (UTF8.chr 0x228E) (Infixl 500) (* LaTeX's \uplus *)
55val _ = overload_on (UTF8.chr 0x228E, ``BAG_UNION``)
56val _ = TeX_notation {hol = UTF8.chr 0x228E, TeX = ("\\ensuremath{\\uplus}", 1)}
57
58Definition BAG_DIFF[nocompute]:
59 BAG_DIFF b1 (b2:'a bag) = \x. b1 x - b2 x
60End
61Overload "-" = ``BAG_DIFF``
62val _ = send_to_back_overload "-" {Name = "BAG_DIFF", Thy = "bag"}
63
64Definition BAG_INSERT[nocompute]:
65 BAG_INSERT (e:'a) b = (\x. if (x = e) then b e + 1 else b x)
66End
67
68val _ = add_listform {cons = "BAG_INSERT", nilstr = "EMPTY_BAG",
69 separator = [TOK ";", BreakSpace(1,0)],
70 leftdelim = [TOK "{|"], rightdelim = [TOK "|}"],
71 block_info = (PP.INCONSISTENT, 2)};
72val _ = TeX_notation { hol = "{|", TeX = ("\\HOLTokenBagLeft{}", 1) }
73val _ = TeX_notation { hol = "|}", TeX = ("\\HOLTokenBagRight{}", 1) }
74
75Theorem BAG_cases:
76 !b. (b = EMPTY_BAG) \/ (?b0 e. b = BAG_INSERT e b0)
77Proof
78 SIMP_TAC std_ss [EMPTY_BAG, BAG_INSERT, FUN_EQ_THM] THEN Q.X_GEN_TAC `b` THEN
79 Q.ASM_CASES_TAC `!x. b x = 0` THEN SRW_TAC [][] THEN
80 FULL_SIMP_TAC std_ss [] THEN MAP_EVERY Q.EXISTS_TAC [
81 `\y. if (y = x) then b x - 1 else b y`, `x`
82 ] THEN SRW_TAC [ARITH_ss][]
83QED
84
85Definition BAG_INTER[nocompute]:
86 BAG_INTER b1 b2 = (\x. if (b1 x < b2 x) then b1 x else b2 x)
87End
88
89
90val _ = print "Properties and definition of BAG_MERGE\n"
91
92Definition BAG_MERGE[nocompute]:
93 BAG_MERGE b1 b2 = (\x. if (b1 x < b2 x) then b2 x else b1 x)
94End
95
96Theorem BAG_MERGE_IDEM[simp]:
97 !b. BAG_MERGE b b = b
98Proof
99 SIMP_TAC std_ss [BAG_MERGE, FUN_EQ_THM]
100QED
101
102Theorem BAG_MERGE_SUB_BAG_UNION:
103 !s t. (SUB_BAG (BAG_MERGE s t) (s + t))
104Proof simp[SUB_BAG,BAG_MERGE,BAG_UNION,BAG_INN]
105QED
106
107Theorem BAG_MERGE_EMPTY[simp]:
108 !b. ((BAG_MERGE {||} b) = b) /\ ((BAG_MERGE b {||}) = b)
109Proof rw[BAG_MERGE,FUN_EQ_THM,EMPTY_BAG]
110QED
111
112Theorem BAG_MERGE_ELBAG_SUB_BAG_INSERT:
113 !A b. SUB_BAG (BAG_MERGE {|A|} b) (BAG_INSERT A b)
114Proof
115 rw[] >> simp[BAG_MERGE,BAG_INSERT,EMPTY_BAG,SUB_BAG,BAG_INN] >> rw[]
116QED
117
118Theorem BAG_MERGE_EQ_EMPTY[simp]:
119 !a b. (BAG_MERGE a b = {||}) <=> (a = {||}) /\ (b = {||})
120Proof
121 rw[BAG_MERGE,EMPTY_BAG,FUN_EQ_THM] >>
122 EQ_TAC >>
123 rw[] >>
124 first_x_assum (qspec_then `x` mp_tac) >>
125 simp[]
126QED
127
128Theorem BAG_INSERT_EQ_MERGE_DIFF:
129 !a b c e. (BAG_INSERT e a = BAG_MERGE b c)
130 ==> ((BAG_MERGE b c = BAG_INSERT e (BAG_MERGE (b - {|e|}) (c - {|e|}))))
131Proof
132 rw[BAG_DIFF] >>
133 fs[BAG_INSERT,BAG_MERGE,EMPTY_BAG,FUN_EQ_THM] >>
134 reverse(rw[])
135 >- (`b e - 1 + 1 = b e` suffices_by simp[EQ_SYM_EQ] >>
136 irule arithmeticTheory.SUB_ADD >>
137 `c e <= b e` by simp[] >>
138 first_x_assum (qspec_then `e` mp_tac) >>
139 rw[]) >>
140 fs[]
141QED
142
143Theorem BAG_MERGE_BAG_INSERT:
144 !e a b.
145 ((a e <= b e)
146 ==> ((BAG_MERGE a (BAG_INSERT e b)) = (BAG_INSERT e (BAG_MERGE a b)))) /\
147 ((b e < a e) ==> ((BAG_MERGE a (BAG_INSERT e b)) = (BAG_MERGE a b))) /\
148 ((a e < b e) ==> ((BAG_MERGE (BAG_INSERT e a) b) = ((BAG_MERGE a b)))) /\
149 ((b e <= a e)
150 ==> ((BAG_MERGE (BAG_INSERT e a) b) = (BAG_INSERT e (BAG_MERGE a b)))) /\
151 ((a e = b e)
152 ==> ((BAG_MERGE (BAG_INSERT e a) (BAG_INSERT e b))
153 = (BAG_INSERT e (BAG_MERGE a b))))
154Proof
155 rw[]
156 >- (simp[BAG_MERGE,BAG_INSERT,EMPTY_BAG,FUN_EQ_THM] >>
157 rw[] >- (Cases_on `x=e` >> fs[]) >> fs[])
158 >- (simp[BAG_MERGE,BAG_INSERT,EMPTY_BAG,FUN_EQ_THM] >>
159 reverse (rw[]) >- (Cases_on `x=e` >> fs[]) >> fs[])
160 >- (simp[BAG_MERGE,BAG_INSERT,EMPTY_BAG,FUN_EQ_THM] >>
161 rw[] >- (Cases_on `x=e` >> fs[]) >> fs[])
162 >> (simp[BAG_MERGE,BAG_INSERT,EMPTY_BAG,FUN_EQ_THM] >>
163 rw[] >> fs[])
164QED
165
166val _ = print "Properties relating BAG_IN(N) to other functions\n"
167Theorem BAG_INN_0[simp]:
168 !b e:'a. BAG_INN e 0 b
169Proof
170 SIMP_TAC arith_ss [BAG_INN]
171QED
172
173Theorem BAG_INN_LESS:
174 !b e n m. BAG_INN e n b /\ m < n ==> BAG_INN e m b
175Proof
176 SIMP_TAC arith_ss [BAG_INN]
177QED
178
179Theorem BAG_IN_BAG_INSERT[simp]:
180 !b e1 e2:'a.
181 BAG_IN e1 (BAG_INSERT e2 b) <=> (e1 = e2) \/ BAG_IN e1 b
182Proof
183 SIMP_TAC arith_ss [BAG_IN, BAG_INN, BAG_INSERT] THEN
184 REPEAT GEN_TAC THEN COND_CASES_TAC THEN SIMP_TAC arith_ss []
185QED
186
187Theorem BAG_INN_BAG_INSERT:
188 !b e1 e2:'a. BAG_INN e1 n (BAG_INSERT e2 b) <=>
189 BAG_INN e1 (n - 1) b /\ (e1 = e2) \/
190 BAG_INN e1 n b
191Proof SRW_TAC [ARITH_ss][BAG_INSERT, BAG_INN]
192QED
193
194Theorem BAG_INN_BAG_INSERT_STRONG:
195 !b n e1 e2.
196 BAG_INN e1 n (BAG_INSERT e2 b) <=>
197 BAG_INN e1 (n - 1) b /\ (e1 = e2) \/
198 BAG_INN e1 n b /\ e1 <> e2
199Proof
200 REWRITE_TAC [BAG_INN_BAG_INSERT] THEN
201 SRW_TAC [][EQ_IMP_THM] THEN SRW_TAC [][] THEN
202 `(n = 0) \/ ?m. n = SUC m` by (Cases_on `n` THEN METIS_TAC []) THEN
203 SRW_TAC [][] THEN
204 `m < SUC m` by DECIDE_TAC THEN
205 PROVE_TAC[BAG_INN_LESS]
206QED
207
208Theorem BAG_UNION_EQ_LCANCEL1[simp]:
209 (b = BAG_UNION b c) <=> (c = {||})
210Proof
211 rw[BAG_UNION, EMPTY_BAG, FUN_EQ_THM, DECIDE ``(x:num = x + y) <=> (y = 0)``]
212QED
213
214Theorem BAG_UNION_EQ_RCANCEL1[simp]:
215 (b = BAG_UNION c b) <=> (c = {||})
216Proof
217 rw[BAG_UNION, EMPTY_BAG, FUN_EQ_THM, DECIDE ``(x:num = x + y) <=> (y = 0)``]
218QED
219
220Theorem BAG_IN_BAG_UNION[simp]:
221 !b1 b2 e. BAG_IN e (BAG_UNION b1 b2) <=> BAG_IN e b1 \/ BAG_IN e b2
222Proof SRW_TAC [ARITH_ss][BAG_IN, BAG_UNION, BAG_INN]
223QED
224
225Theorem BAG_INN_BAG_UNION:
226 !n e b1 b2. BAG_INN e n (BAG_UNION b1 b2) =
227 ?m1 m2. (n = m1 + m2) /\ BAG_INN e m1 b1 /\ BAG_INN e m2 b2
228Proof
229 SRW_TAC [ARITH_ss][BAG_INN, BAG_UNION, GREATER_EQ, EQ_IMP_THM] THEN
230 Induct_on `n` THEN1 SRW_TAC [][] THEN
231 STRIP_TAC THEN
232 `n <= b1 e + b2 e` by DECIDE_TAC THEN
233 FULL_SIMP_TAC (srw_ss()) [] THEN
234 `m1 < b1 e \/ m2 < b2 e` by DECIDE_TAC THENL [
235 MAP_EVERY Q.EXISTS_TAC [`SUC m1`, `m2`] THEN DECIDE_TAC,
236 MAP_EVERY Q.EXISTS_TAC [`m1`, `SUC m2`] THEN DECIDE_TAC
237 ]
238QED
239
240Theorem BAG_INN_BAG_MERGE:
241 !n e b1 b2. (BAG_INN e n (BAG_MERGE b1 b2)) =
242 (BAG_INN e n b1 \/ BAG_INN e n b2)
243Proof
244 SIMP_TAC arith_ss [BAG_INN, BAG_MERGE]
245QED
246
247
248Theorem BAG_IN_BAG_MERGE[simp]:
249 !e b1 b2. BAG_IN e (BAG_MERGE b1 b2) <=> BAG_IN e b1 \/ BAG_IN e b2
250Proof SIMP_TAC std_ss [BAG_IN, BAG_INN_BAG_MERGE]
251QED
252
253val geq_refl = ARITH_PROVE ``m >= m``
254
255Theorem BAG_EXTENSION:
256 !b1 b2. (b1 = b2) = (!n e:'a. BAG_INN e n b1 = BAG_INN e n b2)
257Proof
258 SRW_TAC [][BAG_INN, FUN_EQ_THM, GREATER_EQ] THEN
259 EQ_TAC THEN1 SRW_TAC [][] THEN
260 METIS_TAC [
261 ARITH_PROVE ``(x = y) <=> (x <= y) /\ (y <= x)``,
262 LESS_EQ_REFL
263 ]
264QED
265
266val _ = print "Properties of BAG_INSERT\n"
267
268Theorem BAG_UNION_INSERT:
269 !e b1 b2.
270 (BAG_UNION (BAG_INSERT e b1) b2 = BAG_INSERT e (BAG_UNION b1 b2)) /\
271 (BAG_UNION b1 (BAG_INSERT e b2) = BAG_INSERT e (BAG_UNION b1 b2))
272Proof
273 SRW_TAC [ARITH_ss][FUN_EQ_THM, BAG_INSERT, BAG_UNION] THEN
274 SRW_TAC [ARITH_ss][]
275QED
276
277Theorem BAG_INSERT_DIFF[simp]:
278 !x b. ~(BAG_INSERT x b = b)
279Proof
280 SRW_TAC [COND_elim_ss][FUN_EQ_THM, BAG_INSERT]
281QED
282
283Theorem BAG_INSERT_NOT_EMPTY[simp]:
284 !x b. ~(BAG_INSERT x b = EMPTY_BAG)
285Proof
286 SRW_TAC [COND_elim_ss][FUN_EQ_THM, BAG_INSERT, EMPTY_BAG, EXISTS_OR_THM]
287QED
288
289val or_cong = REWRITE_RULE [GSYM AND_IMP_INTRO] OR_CONG
290Theorem BAG_INSERT_ONE_ONE[simp]:
291 !b1 b2 x:'a.
292 (BAG_INSERT x b1 = BAG_INSERT x b2) = (b1 = b2)
293Proof
294 SIMP_TAC (srw_ss() ++ COND_elim_ss) [BAG_INSERT, FUN_EQ_THM, EQ_IMP_THM,
295 Cong or_cong, FORALL_AND_THM] THEN
296 METIS_TAC []
297QED
298
299Theorem C_BAG_INSERT_ONE_ONE[simp]:
300 !x y b. (BAG_INSERT x b = BAG_INSERT y b) = (x = y)
301Proof
302 SIMP_TAC (srw_ss() ++ COND_elim_ss ++ ARITH_ss)
303 [BAG_INSERT, FUN_EQ_THM, Cong or_cong] THEN
304 METIS_TAC []
305QED
306
307Theorem BAG_INSERT_commutes:
308 !b e1 e2. BAG_INSERT e1 (BAG_INSERT e2 b) =
309 BAG_INSERT e2 (BAG_INSERT e1 b)
310Proof
311 SIMP_TAC (srw_ss()) [BAG_INSERT, FUN_EQ_THM] THEN
312 REPEAT GEN_TAC THEN
313 REPEAT (COND_CASES_TAC THEN ASM_SIMP_TAC (srw_ss()) []) THEN
314 SRW_TAC [][]
315QED
316
317Theorem BAG_DECOMPOSE:
318 !e b. BAG_IN e b ==> ?b'. b = BAG_INSERT e b'
319Proof
320 REPEAT STRIP_TAC THEN
321 Q.EXISTS_TAC `b - {|e|}` THEN POP_ASSUM MP_TAC THEN
322 SRW_TAC [ARITH_ss, COND_elim_ss]
323 [BAG_INSERT,BAG_DIFF,EMPTY_BAG,FUN_EQ_THM,BAG_IN,BAG_INN]
324QED
325
326val _ = print "Properties of BAG_UNION\n";
327
328Theorem BAG_UNION_LEFT_CANCEL[simp]:
329 !b b1 b2:'a -> num. (BAG_UNION b b1 = BAG_UNION b b2) = (b1 = b2)
330Proof
331 SIMP_TAC arith_ss [BAG_UNION,FUN_EQ_THM]
332QED
333
334Theorem COMM_BAG_UNION:
335 !b1 b2. BAG_UNION b1 b2 = BAG_UNION b2 b1
336Proof
337 SRW_TAC [ARITH_ss][BAG_UNION, FUN_EQ_THM]
338QED
339val bu_comm = COMM_BAG_UNION;
340
341Theorem BAG_UNION_RIGHT_CANCEL[simp]:
342 !b b1 b2:'a bag. (BAG_UNION b1 b = BAG_UNION b2 b) = (b1 = b2)
343Proof
344 METIS_TAC [bu_comm, BAG_UNION_LEFT_CANCEL]
345QED
346
347Theorem ASSOC_BAG_UNION:
348 !b1 b2 b3. BAG_UNION b1 (BAG_UNION b2 b3)
349 =
350 BAG_UNION (BAG_UNION b1 b2) b3
351Proof
352 SRW_TAC [ARITH_ss][BAG_UNION, FUN_EQ_THM]
353QED
354
355Theorem BAG_UNION_EMPTY[simp]:
356 (!b. b + {||} = b) /\
357 (!b. {||} + b = b) /\
358 (!b1 b2. (b1 + b2 = {||}) <=> (b1 = {||}) /\ (b2 = {||}))
359Proof SRW_TAC [][BAG_UNION, EMPTY_BAG, FUN_EQ_THM] THEN METIS_TAC []
360QED
361
362val _ = print "Definition and properties of BAG_DELETE\n"
363Definition BAG_DELETE[nocompute]:
364 BAG_DELETE b0 (e:'a) b = (b0 = BAG_INSERT e b)
365End
366
367Theorem BAG_DELETE_EMPTY:
368 !(e:'a) b. ~(BAG_DELETE EMPTY_BAG e b)
369Proof
370 SIMP_TAC std_ss [BAG_DELETE] THEN
371 ACCEPT_TAC (GSYM BAG_INSERT_NOT_EMPTY)
372QED
373
374Theorem BAG_DELETE_commutes:
375 !b0 b1 b2 e1 e2:'a.
376 BAG_DELETE b0 e1 b1 /\ BAG_DELETE b1 e2 b2 ==>
377 ?b'. BAG_DELETE b0 e2 b' /\ BAG_DELETE b' e1 b2
378Proof
379 SIMP_TAC std_ss [BAG_DELETE] THEN
380 ACCEPT_TAC BAG_INSERT_commutes
381QED
382
383Theorem BAG_DELETE_11:
384 !b0 (e1:'a) e2 b1 b2.
385 BAG_DELETE b0 e1 b1 /\ BAG_DELETE b0 e2 b2 ==>
386 ((e1 = e2) = (b1 = b2))
387Proof
388 SRW_TAC [][BAG_DELETE, EQ_IMP_THM] THEN
389 FULL_SIMP_TAC (srw_ss()) []
390QED
391
392Theorem BAG_INN_BAG_DELETE:
393 !b n e. BAG_INN e n b /\ n > 0 ==> ?b'. BAG_DELETE b e b'
394Proof
395 SRW_TAC [][BAG_DELETE] THEN MATCH_MP_TAC BAG_DECOMPOSE THEN
396 SRW_TAC [][BAG_IN] THEN
397 `(n = 1) \/ 1 < n` by DECIDE_TAC THEN
398 METIS_TAC [BAG_INN_LESS]
399QED
400
401Theorem BAG_IN_BAG_DELETE:
402 !b e:'a. BAG_IN e b ==> ?b'. BAG_DELETE b e b'
403Proof
404 METIS_TAC [BAG_INN_BAG_DELETE, ARITH_PROVE (Term`1 > 0`), BAG_IN]
405QED
406
407val ELIM_TAC = BasicProvers.VAR_EQ_TAC
408val ARWT = SRW_TAC [ARITH_ss][]
409Theorem BAG_DELETE_INSERT:
410 !x y b1 b2.
411 BAG_DELETE (BAG_INSERT x b1) y b2 ==>
412 (x = y) /\ (b1 = b2) \/ (?b3. BAG_DELETE b1 y b3) /\ ~(x = y)
413Proof
414 SIMP_TAC std_ss [BAG_DELETE] THEN REPEAT STRIP_TAC THEN
415 Q.ASM_CASES_TAC `x = y` THEN ARWT THENL [
416 FULL_SIMP_TAC std_ss [BAG_INSERT_ONE_ONE],
417 Q.SUBGOAL_THEN `BAG_IN y b1`
418 (STRIP_ASSUME_TAC o
419 MATCH_MP (REWRITE_RULE [BAG_DELETE] BAG_IN_BAG_DELETE))
420 THENL [
421 ASM_MESON_TAC [BAG_IN_BAG_INSERT],
422 ELIM_TAC THEN SIMP_TAC std_ss [BAG_INSERT_ONE_ONE]
423 ]
424 ]
425QED
426
427Theorem BAG_DELETE_BAG_IN_up:
428 !b0 b e:'a. BAG_DELETE b0 e b ==>
429 !e'. BAG_IN e' b ==> BAG_IN e' b0
430Proof
431 REWRITE_TAC [BAG_DELETE] THEN REPEAT STRIP_TAC THEN ELIM_TAC THEN
432 ASM_REWRITE_TAC [BAG_IN_BAG_INSERT]
433QED
434
435Theorem BAG_DELETE_BAG_IN_down:
436 !b0 b e1 e2:'a.
437 BAG_DELETE b0 e1 b /\ ~(e1 = e2) /\ BAG_IN e2 b0 ==>
438 BAG_IN e2 b
439Proof
440 SIMP_TAC std_ss [BAG_DELETE, BAG_IN_BAG_INSERT, LEFT_AND_OVER_OR,
441 DISJ_IMP_THM]
442QED
443
444Theorem BAG_DELETE_BAG_IN:
445 !b0 b e:'a. BAG_DELETE b0 e b ==> BAG_IN e b0
446Proof
447 SIMP_TAC std_ss [BAG_IN_BAG_INSERT, BAG_DELETE]
448QED
449
450Theorem BAG_DELETE_concrete:
451 !b0 b e. BAG_DELETE b0 e b <=>
452 b0 e > 0 /\ (b = \x. if (x = e) then b0 e - 1 else b0 x)
453Proof
454 SRW_TAC [ARITH_ss][FUN_EQ_THM, BAG_DELETE, BAG_INSERT, EQ_IMP_THM] THEN
455 SRW_TAC [][]
456QED
457
458Theorem add_eq_conv_diff[local]:
459 (M + {|a|} = N + {|b|}) <=>
460 (M = N) /\ (a = b) \/
461 (M = N - {|a|} + {|b|}) /\ (N = M - {|b|} + {|a|})
462Proof
463 SRW_TAC [][BAG_UNION, BAG_DIFF, FUN_EQ_THM, BAG_INSERT, EMPTY_BAG] THEN
464 Cases_on `a = b` THEN SRW_TAC [][] THENL [
465 EQ_TAC THEN1 SRW_TAC [][] THEN STRIP_TAC THEN
466 Q.X_GEN_TAC `x` THEN
467 REPEAT (POP_ASSUM (Q.SPEC_THEN `x` MP_TAC)) THEN SRW_TAC [][] THEN
468 DECIDE_TAC,
469
470 EQ_TAC THEN STRIP_TAC THEN REPEAT CONJ_TAC THEN
471 Q.X_GEN_TAC `x` THEN
472 REPEAT (FIRST_X_ASSUM (Q.SPEC_THEN `x` MP_TAC)) THEN
473 SRW_TAC [][] THEN DECIDE_TAC
474 ]
475QED
476
477Theorem insert_diffM2[local]:
478 BAG_IN x M ==> (M - {|x|} + {|x|} = M)
479Proof
480 SRW_TAC [][BAG_UNION, BAG_DIFF, BAG_INSERT, EMPTY_BAG, FUN_EQ_THM, BAG_IN,
481 BAG_INN] THEN
482 SRW_TAC [][] THEN DECIDE_TAC
483QED
484
485Theorem BAG_UNION_DIFF_eliminate[simp]:
486 (BAG_DIFF (BAG_UNION b c) c = b) /\
487 (BAG_DIFF (BAG_UNION c b) c = b)
488Proof
489 SRW_TAC [][BAG_DIFF, BAG_UNION, FUN_EQ_THM]
490QED
491
492Theorem add_eq_conv_ex[local]:
493 (M + {|a|} = N + {|b|}) <=>
494 (M = N) /\ (a = b) \/
495 ?k. (M = k + {|b|}) /\ (N = k + {|a|})
496Proof
497 SRW_TAC [][add_eq_conv_diff] THEN Cases_on `a = b` THENL [
498 SRW_TAC [][EQ_IMP_THM] THEN
499 FULL_SIMP_TAC (srw_ss()) [insert_diffM2] THEN
500 POP_ASSUM ACCEPT_TAC,
501
502 SRW_TAC [][] THEN EQ_TAC THEN STRIP_TAC THENL [
503 POP_ASSUM SUBST_ALL_TAC THEN SRW_TAC [][] THEN
504 `BAG_IN b M` by METIS_TAC [BAG_IN_BAG_UNION, BAG_IN_BAG_INSERT] THEN
505 SRW_TAC [][insert_diffM2],
506
507 SRW_TAC [][]
508 ]
509 ]
510QED
511
512Theorem BAG_INSERT_EQUAL =
513 SIMP_RULE (srw_ss()) [BAG_UNION_INSERT] add_eq_conv_ex
514
515Theorem BAG_DELETE_TWICE:
516 !b0 e1 e2 b1 b2.
517 BAG_DELETE b0 e1 b1 /\ BAG_DELETE b0 e2 b2 /\ ~(b1 = b2) ==>
518 ?b. BAG_DELETE b1 e2 b /\ BAG_DELETE b2 e1 b
519Proof
520 SRW_TAC [][BAG_DELETE] THEN
521 `b2 + {|e2|} = b1 + {|e1|}` by SRW_TAC [][BAG_UNION_INSERT] THEN
522 POP_ASSUM (STRIP_ASSUME_TAC o REWRITE_RULE [add_eq_conv_ex]) THEN
523 FULL_SIMP_TAC (srw_ss()) [] THEN
524 SRW_TAC [][BAG_UNION_INSERT]
525QED
526
527Definition SING_BAG[nocompute]:
528 SING_BAG (b:'a->num) = ?x. b = BAG_INSERT x EMPTY_BAG
529End
530
531Theorem SING_BAG_THM:
532 !e:'a. SING_BAG (BAG_INSERT e EMPTY_BAG)
533Proof
534 MESON_TAC [SING_BAG]
535QED
536
537Definition EL_BAG[nocompute]:
538 EL_BAG (e:'a) = BAG_INSERT e EMPTY_BAG
539End
540
541Theorem EL_BAG_11:
542 !x y. (EL_BAG x = EL_BAG y) ==> (x = y)
543Proof
544 SRW_TAC [][EL_BAG]
545QED
546
547Theorem EL_BAG_INSERT_squeeze:
548 !x b y. (EL_BAG x = BAG_INSERT y b) ==> (x = y) /\ (b = EMPTY_BAG)
549Proof
550 SIMP_TAC (srw_ss()) [EL_BAG, BAG_INSERT_EQUAL]
551QED
552
553Theorem SING_EL_BAG:
554 !e:'a. SING_BAG (EL_BAG e)
555Proof
556 REWRITE_TAC [EL_BAG, SING_BAG_THM]
557QED
558
559Theorem BAG_INSERT_UNION:
560 !b e. BAG_INSERT e b = BAG_UNION (EL_BAG e) b
561Proof
562 SRW_TAC [][EL_BAG, BAG_UNION_INSERT]
563QED
564
565Theorem BAG_INSERT_EQ_UNION:
566 !e b1 b2 b. (BAG_INSERT e b = BAG_UNION b1 b2) ==>
567 BAG_IN e b1 \/ BAG_IN e b2
568Proof
569 REPEAT STRIP_TAC THEN POP_ASSUM (MP_TAC o Q.AP_TERM `BAG_IN e`) THEN
570 SRW_TAC [][]
571QED
572
573Theorem BAG_DELETE_SING:
574 !b e. BAG_DELETE b e EMPTY_BAG ==> SING_BAG b
575Proof
576 MESON_TAC [SING_BAG, BAG_DELETE]
577QED
578
579Theorem NOT_IN_EMPTY_BAG[simp]:
580 !x:'a. ~(BAG_IN x EMPTY_BAG)
581Proof
582 SIMP_TAC std_ss [BAG_IN, BAG_INN, EMPTY_BAG]
583QED
584
585Theorem BAG_INN_EMPTY_BAG[simp]:
586 !e n. BAG_INN e n EMPTY_BAG = (n = 0)
587Proof
588 SIMP_TAC arith_ss [BAG_INN, EMPTY_BAG, EQ_IMP_THM]
589QED
590
591Theorem BAG_MEMBER_NOT_EMPTY:
592 !b. (?x. BAG_IN x b) <=> b <> EMPTY_BAG
593Proof
594 METIS_TAC [BAG_cases, BAG_IN_BAG_INSERT, NOT_IN_EMPTY_BAG]
595QED
596
597val _ = print "Properties of SUB_BAG\n"
598
599Overload "<=" = ``SUB_BAG``
600Overload "<" = ``PSUB_BAG``
601val _ = send_to_back_overload "<=" {Name = "SUB_BAG", Thy = "bag"}
602val _ = send_to_back_overload "<" {Name = "PSUB_BAG", Thy = "bag"}
603
604Theorem SUB_BAG_LEQ:
605 SUB_BAG b1 b2 = !x. b1 x <= b2 x
606Proof
607 SRW_TAC [][SUB_BAG, BAG_INN, EQ_IMP_THM] THENL [
608 POP_ASSUM (Q.SPECL_THEN [`x`, `b1 x`] MP_TAC) THEN DECIDE_TAC,
609 FIRST_X_ASSUM (Q.SPEC_THEN `x` MP_TAC) THEN DECIDE_TAC
610 ]
611QED
612
613Theorem SUB_BAG_EMPTY[simp]:
614 (!b:'a->num. SUB_BAG {||} b) /\
615 (!b:'a->num. SUB_BAG b {||} = (b = {||}))
616Proof
617 SRW_TAC [][SUB_BAG_LEQ, EMPTY_BAG, FUN_EQ_THM]
618QED
619
620Theorem SUB_BAG_REFL[simp]:
621 !(b:'a -> num). SUB_BAG b b
622Proof
623 REWRITE_TAC [SUB_BAG]
624QED
625
626Theorem PSUB_BAG_IRREFL:
627 !(b:'a -> num). ~(PSUB_BAG b b)
628Proof
629 REWRITE_TAC [PSUB_BAG]
630QED
631
632Theorem SUB_BAG_ANTISYM:
633 !(b1:'a -> num) b2. SUB_BAG b1 b2 /\ SUB_BAG b2 b1 ==> (b1 = b2)
634Proof
635 SRW_TAC [][SUB_BAG_LEQ, FUN_EQ_THM,
636 DECIDE ``(x:num = y) <=> x <= y /\ y <= x``]
637QED
638
639Theorem PSUB_BAG_ANTISYM:
640 !(b1:'a -> num) b2. ~(PSUB_BAG b1 b2 /\ PSUB_BAG b2 b1)
641Proof
642 MESON_TAC [PSUB_BAG, SUB_BAG_ANTISYM]
643QED
644
645Theorem SUB_BAG_TRANS:
646 !b1 b2 b3. SUB_BAG (b1:'a->num) b2 /\ SUB_BAG b2 b3 ==>
647 SUB_BAG b1 b3
648Proof
649 MESON_TAC [SUB_BAG, BAG_INN]
650QED
651
652Theorem PSUB_BAG_TRANS:
653 !(b1:'a -> num) b2 b3. PSUB_BAG b1 b2 /\ PSUB_BAG b2 b3 ==>
654 PSUB_BAG b1 b3
655Proof
656 MESON_TAC [PSUB_BAG, SUB_BAG_TRANS, SUB_BAG_ANTISYM]
657QED
658
659Theorem PSUB_BAG_SUB_BAG:
660 !(b1:'a->num) b2. PSUB_BAG b1 b2 ==> SUB_BAG b1 b2
661Proof
662 SIMP_TAC std_ss [PSUB_BAG]
663QED
664
665Theorem PSUB_BAG_NOT_EQ:
666 !(b1:'a -> num) b2. PSUB_BAG b1 b2 ==> ~(b1 = b2)
667Proof
668 SIMP_TAC std_ss [PSUB_BAG]
669QED
670
671val _ = print "Properties of BAG_DIFF\n";
672
673Theorem BAG_DIFF_EMPTY:
674 (!b. b - b = {||}) /\
675 (!b. b - {||} = b) /\
676 (!b. {||} - b = {||}) /\
677 (!b1 b2.
678 b1 <= b2 ==> (b1 - b2 = {||}))
679Proof
680 SRW_TAC [][SUB_BAG_LEQ, BAG_DIFF, EMPTY_BAG, FUN_EQ_THM]
681QED
682
683Theorem BAG_DIFF_EMPTY_simple[simp] =
684 LIST_CONJ (List.take(CONJUNCTS BAG_DIFF_EMPTY, 3))
685
686Theorem BAG_DIFF_EQ_EMPTY[simp]:
687 (b - c = {||}) <=> b <= c
688Proof
689 simp[BAG_DIFF, FUN_EQ_THM, SUB_BAG_LEQ, EMPTY_BAG]
690QED
691
692Theorem BAG_DIFF_INSERT_same[simp]:
693 !x b1 b2. BAG_DIFF (BAG_INSERT x b1) (BAG_INSERT x b2) =
694 BAG_DIFF b1 b2
695Proof
696 SRW_TAC [COND_elim_ss, ARITH_ss][BAG_DIFF, FUN_EQ_THM, BAG_INSERT]
697QED
698
699Theorem BAG_DIFF_INSERT:
700 !x b1 b2.
701 ~BAG_IN x b1 ==>
702 (BAG_DIFF (BAG_INSERT x b2) b1 = BAG_INSERT x (BAG_DIFF b2 b1))
703Proof
704 SRW_TAC [COND_elim_ss, ARITH_ss][FUN_EQ_THM, BAG_DIFF, BAG_INSERT,
705 Cong or_cong, BAG_IN, BAG_INN]
706QED
707
708Theorem NOT_IN_BAG_DIFF:
709 !x b1 b2. ~BAG_IN x b1 ==>
710 (BAG_DIFF b1 (BAG_INSERT x b2) = BAG_DIFF b1 b2)
711Proof
712 SRW_TAC [COND_elim_ss, ARITH_ss][FUN_EQ_THM, BAG_IN, BAG_INN, BAG_INSERT,
713 BAG_DIFF]
714QED
715
716Theorem BAG_IN_DIFF_I:
717 e <: b1 /\ ~(e <: b2) ==> e <: b1 - b2
718Proof
719 SRW_TAC [ARITH_ss][BAG_IN,BAG_DIFF,BAG_INN]
720QED
721
722Theorem BAG_IN_DIFF_E:
723 e <: b1 - b2 ==> e <: b1
724Proof
725SRW_TAC [ARITH_ss][BAG_IN,BAG_INN,BAG_DIFF]
726QED
727
728Theorem BAG_UNION_DIFF:
729 !X Y Z.
730 SUB_BAG Z Y ==>
731 (BAG_UNION X (BAG_DIFF Y Z) = BAG_DIFF (BAG_UNION X Y) Z) /\
732 (BAG_UNION (BAG_DIFF Y Z) X = BAG_DIFF (BAG_UNION X Y) Z)
733Proof
734 SRW_TAC [][SUB_BAG_LEQ, BAG_UNION, BAG_DIFF, FUN_EQ_THM] THEN
735 POP_ASSUM (fn th => SIMP_TAC arith_ss [SPEC_ALL th])
736QED
737
738Theorem BAG_DIFF_2L:
739 !X Y Z:'a->num.
740 BAG_DIFF (BAG_DIFF X Y) Z = BAG_DIFF X (BAG_UNION Y Z)
741Proof
742 SIMP_TAC arith_ss [BAG_UNION,BAG_INN,SUB_BAG,BAG_DIFF]
743QED
744
745Theorem BAG_DIFF_2R:
746 !A B C:'a->num.
747 SUB_BAG C B ==>
748 (BAG_DIFF A (BAG_DIFF B C) = BAG_DIFF (BAG_UNION A C) B)
749Proof
750 SRW_TAC [][BAG_UNION, BAG_DIFF, SUB_BAG_LEQ, FUN_EQ_THM] THEN
751 ASSUM_LIST (fn thl => SIMP_TAC arith_ss (map SPEC_ALL thl))
752QED
753
754val std_ss = arith_ss
755Theorem SUB_BAG_BAG_DIFF:
756 !X Y Y' Z W:'a->num.
757 SUB_BAG (BAG_DIFF X Y) (BAG_DIFF Z W) ==>
758 SUB_BAG (BAG_DIFF X (BAG_UNION Y Y'))
759 (BAG_DIFF Z (BAG_UNION W Y'))
760Proof
761 SIMP_TAC std_ss [
762 BAG_DIFF, SUB_BAG_LEQ, BAG_INN, BAG_UNION,
763 DISJ_IMP_THM] THEN
764 REPEAT STRIP_TAC THEN
765 FIRST_ASSUM (Q.SPEC_THEN `x` (STRIP_ASSUME_TAC o SIMP_RULE std_ss [])) THEN
766 ASM_SIMP_TAC std_ss []
767QED
768
769local
770 fun bdf (b1, b2) (b3, b4) =
771 let val (b1v, b2v, b3v, b4v) =
772 case map (C (curry mk_var) (==`:'a->num`==)) [b1, b2, b3, b4] of
773 [b1v, b2v, b3v, b4v] => (b1v, b2v, b3v, b4v)
774 | _ => raise Match
775 in
776 ``BAG_DIFF (BAG_UNION ^b1v ^b2v) (BAG_UNION ^b3v ^b4v) =
777 BAG_DIFF b2 b3``
778 end
779in
780Theorem BAG_DIFF_UNION_eliminate[simp]:
781 !(b1:'a->num) (b2:'a->num) (b3:'a->num).
782 ^(bdf ("b1", "b2") ("b1", "b3")) /\
783 ^(bdf ("b1", "b2") ("b3", "b1")) /\
784 ^(bdf ("b2", "b1") ("b1", "b3")) /\
785 ^(bdf ("b2", "b1") ("b3", "b1"))
786Proof
787 REPEAT STRIP_TAC THEN
788 SIMP_TAC std_ss [BAG_DIFF, BAG_UNION, FUN_EQ_THM]
789QED
790end;
791
792local
793 fun bdf (b1, b2) (b3, b4) =
794 let val (b1v, b2v, b3v, b4v) =
795 case map (C (curry mk_var) (==`:'a->num`==)) [b1, b2, b3, b4] of
796 [b1v, b2v, b3v, b4v] => (b1v, b2v, b3v, b4v)
797 | _ => raise Match
798 in
799 ``SUB_BAG (BAG_UNION ^b1v ^b2v) (BAG_UNION ^b3v ^b4v) =
800 SUB_BAG (b2:'a->num) b3``
801 end
802in
803Theorem SUB_BAG_UNION_eliminate[simp]:
804 !(b1:'a->num) (b2:'a->num) (b3:'a->num).
805 ^(bdf ("b1", "b2") ("b1", "b3")) /\
806 ^(bdf ("b1", "b2") ("b3", "b1")) /\
807 ^(bdf ("b2", "b1") ("b1", "b3")) /\
808 ^(bdf ("b2", "b1") ("b3", "b1"))
809Proof
810 SIMP_TAC std_ss [SUB_BAG_LEQ, BAG_UNION, BAG_INN] THEN
811 REPEAT STRIP_TAC THEN EQ_TAC THEN
812 STRIP_TAC THEN
813 POP_ASSUM (fn th => SIMP_TAC std_ss [SPEC_ALL th])
814QED
815end;
816
817Theorem move_BAG_UNION_over_eq:
818 !X Y Z:'a->num. (BAG_UNION X Y = Z) ==> (X = BAG_DIFF Z Y)
819Proof
820 SIMP_TAC (std_ss ++ ETA_ss) [BAG_UNION, BAG_DIFF]
821QED
822
823val std_bag_tac =
824 SIMP_TAC std_ss [BAG_UNION, SUB_BAG_LEQ, BAG_INN] THEN
825 REPEAT STRIP_TAC THEN
826 ASSUM_LIST (fn thl => SIMP_TAC std_ss (map SPEC_ALL thl))
827
828fun bag_thm t = prove(Term t, std_bag_tac);
829
830val simplest_cases = map bag_thm [
831 `!b1 b2:'a->num. SUB_BAG b1 b2 ==> !b. SUB_BAG b1 (BAG_UNION b2 b)`,
832 `!b1 b2:'a->num. SUB_BAG b1 b2 ==> !b. SUB_BAG b1 (BAG_UNION b b2)`
833];
834
835val one_from_assocl = map bag_thm [
836 `!b1 b2 b3:'a->num.
837 SUB_BAG b1 (BAG_UNION b2 b3) ==>
838 !b. SUB_BAG b1 (BAG_UNION (BAG_UNION b2 b) b3)`,
839 `!b1 b2 b3:'a->num.
840 SUB_BAG b1 (BAG_UNION b2 b3) ==>
841 !b. SUB_BAG b1 (BAG_UNION (BAG_UNION b b2) b3)`]
842
843val one_from_assocr =
844 map (ONCE_REWRITE_RULE [bu_comm]) one_from_assocl;
845
846val one_from_assoc = one_from_assocl @ one_from_assocr;
847
848val union_from_union = map bag_thm [
849 `!b1 b2 b3 b4:'a->num.
850 SUB_BAG b1 b3 ==> SUB_BAG b2 b4 ==>
851 SUB_BAG (BAG_UNION b1 b2) (BAG_UNION b3 b4)`,
852 `!b1 b2 b3 b4:'a->num.
853 SUB_BAG b1 b4 ==> SUB_BAG b2 b3 ==>
854 SUB_BAG (BAG_UNION b1 b2) (BAG_UNION b3 b4)`];
855
856val union_union2_assocl = map bag_thm [
857 `!b1 b2 b3 b4 b5:'a->num.
858 SUB_BAG b1 (BAG_UNION b3 b5) ==> SUB_BAG b2 b4 ==>
859 SUB_BAG (BAG_UNION b1 b2) (BAG_UNION (BAG_UNION b3 b4) b5)`,
860 `!b1 b2 b3 b4 b5:'a->num.
861 SUB_BAG b1 (BAG_UNION b4 b5) ==> SUB_BAG b2 b3 ==>
862 SUB_BAG (BAG_UNION b1 b2) (BAG_UNION (BAG_UNION b3 b4) b5)`,
863 `!b1 b2 b3 b4 b5:'a->num.
864 SUB_BAG b2 (BAG_UNION b3 b5) ==> SUB_BAG b1 b4 ==>
865 SUB_BAG (BAG_UNION b1 b2) (BAG_UNION (BAG_UNION b3 b4) b5)`,
866 `!b1 b2 b3 b4 b5:'a->num.
867 SUB_BAG b2 (BAG_UNION b4 b5) ==> SUB_BAG b1 b3 ==>
868 SUB_BAG (BAG_UNION b1 b2) (BAG_UNION (BAG_UNION b3 b4) b5)`];
869
870val union_union2_assocr =
871 map (ONCE_REWRITE_RULE [bu_comm]) union_union2_assocl;
872
873val union_union2_assoc = union_union2_assocl @ union_union2_assocr;
874
875val union2_union_assocl = map bag_thm [
876 `!b1 b2 b3 b4 b5:'a->num.
877 SUB_BAG (BAG_UNION b1 b2) b4 ==> SUB_BAG b3 b5 ==>
878 SUB_BAG (BAG_UNION (BAG_UNION b1 b3) b2) (BAG_UNION b4 b5)`,
879 `!b1 b2 b3 b4 b5:'a->num.
880 SUB_BAG (BAG_UNION b1 b2) b5 ==> SUB_BAG b3 b4 ==>
881 SUB_BAG (BAG_UNION (BAG_UNION b1 b3) b2) (BAG_UNION b4 b5)`,
882 `!b1 b2 b3 b4 b5:'a->num.
883 SUB_BAG (BAG_UNION b3 b2) b4 ==> SUB_BAG b1 b5 ==>
884 SUB_BAG (BAG_UNION (BAG_UNION b1 b3) b2) (BAG_UNION b4 b5)`,
885 `!b1 b2 b3 b4 b5:'a->num.
886 SUB_BAG (BAG_UNION b3 b2) b5 ==> SUB_BAG b1 b4 ==>
887 SUB_BAG (BAG_UNION (BAG_UNION b1 b3) b2) (BAG_UNION b4 b5)`];
888
889val union2_union_assocr =
890 map (ONCE_REWRITE_RULE [bu_comm]) union2_union_assocl;
891
892val union2_union_assoc = union2_union_assocl @ union2_union_assocr;
893
894Theorem SUB_BAG_UNION =
895 LIST_CONJ (simplest_cases @ one_from_assoc @ union_from_union @
896 union_union2_assoc @ union2_union_assoc);
897
898Theorem SUB_BAG_EL_BAG:
899 !e b. SUB_BAG (EL_BAG e) b = BAG_IN e b
900Proof
901 SRW_TAC [COND_elim_ss, ARITH_ss]
902 [SUB_BAG_LEQ, EL_BAG, BAG_IN, BAG_INN, BAG_INSERT, EMPTY_BAG]
903QED
904
905Theorem SUB_BAG_INSERT:
906 !e b1 b2. SUB_BAG (BAG_INSERT e b1) (BAG_INSERT e b2) =
907 SUB_BAG b1 b2
908Proof
909 SRW_TAC [ARITH_ss][BAG_INSERT, SUB_BAG_LEQ, EQ_IMP_THM] THEN
910 POP_ASSUM (Q.SPEC_THEN `x` MP_TAC) THEN SRW_TAC [ARITH_ss][]
911QED
912
913Theorem SUB_BAG_INSERT_I:
914 !b c e. SUB_BAG b c ==> SUB_BAG b (BAG_INSERT e c)
915Proof
916 SRW_TAC[][BAG_INSERT, SUB_BAG_LEQ] THEN
917 POP_ASSUM (Q.SPEC_THEN `x` MP_TAC) THEN SRW_TAC[ARITH_ss][]
918QED
919
920Theorem NOT_IN_SUB_BAG_INSERT:
921 !b1 b2 e. ~(BAG_IN e b1) ==>
922 (SUB_BAG b1 (BAG_INSERT e b2) = SUB_BAG b1 b2)
923Proof
924 SIMP_TAC std_ss [SUB_BAG, BAG_INN_BAG_INSERT, BAG_IN] THEN
925 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [
926 RES_TAC THEN ELIM_TAC THEN
927 STRIP_ASSUME_TAC (ARITH_PROVE (Term`(n = 0) \/ (n = 1) \/ (1 < n)`))
928 THENL [
929 FULL_SIMP_TAC std_ss [],
930 FULL_SIMP_TAC std_ss [],
931 ASM_MESON_TAC [BAG_INN_LESS]
932 ],
933 ASM_MESON_TAC []
934 ]
935QED
936
937Theorem SUB_BAG_BAG_IN:
938 !x b1 b2. SUB_BAG (BAG_INSERT x b1) b2 ==> BAG_IN x b2
939Proof
940 SIMP_TAC std_ss [SUB_BAG_LEQ, BAG_INSERT, BAG_IN, BAG_INN] THEN
941 REPEAT GEN_TAC THEN
942 DISCH_THEN (Q.SPEC_THEN `x` (ASSUME_TAC o SIMP_RULE std_ss [])) THEN
943 ASM_SIMP_TAC std_ss []
944QED
945
946Theorem SUB_BAG_EXISTS:
947 !b1 b2:'a->num. SUB_BAG b1 b2 = ?b. b2 = BAG_UNION b1 b
948Proof
949 SRW_TAC [][SUB_BAG_LEQ, BAG_UNION, FUN_EQ_THM, EQ_IMP_THM] THENL [
950 Q.EXISTS_TAC `\x. b2 x - b1 x` THEN
951 POP_ASSUM (fn th => SIMP_TAC std_ss [SPEC_ALL th]),
952 ASM_SIMP_TAC std_ss []
953 ]
954QED
955
956Theorem SUB_BAG_UNION_DIFF:
957 !b1 b2 b3:'a->num.
958 SUB_BAG b1 b3 ==>
959 (SUB_BAG b2 (BAG_DIFF b3 b1) = SUB_BAG (BAG_UNION b1 b2) b3)
960Proof
961 SIMP_TAC std_ss [SUB_BAG_LEQ,BAG_DIFF,BAG_UNION] THEN
962 REPEAT STRIP_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THEN
963 REPEAT (POP_ASSUM (MP_TAC o SPEC_ALL)) THEN DECIDE_TAC
964QED
965
966Theorem SUB_BAG_UNION_down:
967 !b1 b2 b3:'a->num. SUB_BAG (BAG_UNION b1 b2) b3 ==>
968 SUB_BAG b1 b3 /\ SUB_BAG b2 b3
969Proof
970 SIMP_TAC std_ss [BAG_UNION, SUB_BAG_LEQ] THEN
971 REPEAT STRIP_TAC THEN
972 ASSUM_LIST (fn thl => SIMP_TAC std_ss (map SPEC_ALL thl))
973QED
974
975Theorem SUB_BAG_DIFF:
976 (!b1 b2:'a->num. SUB_BAG b1 b2 ==>
977 (!b3. SUB_BAG (BAG_DIFF b1 b3) b2)) /\
978 (!b1 b2 b3 b4:'a->num.
979 SUB_BAG b2 b1 ==> SUB_BAG b4 b3 ==>
980 (SUB_BAG (BAG_DIFF b1 b2) (BAG_DIFF b3 b4) =
981 SUB_BAG (BAG_UNION b1 b4) (BAG_UNION b2 b3)))
982Proof
983 SRW_TAC [ARITH_ss][BAG_DIFF, BAG_UNION, SUB_BAG_LEQ, EQ_IMP_THM] THEN
984 REPEAT (POP_ASSUM (MP_TAC o SPEC_ALL)) THEN DECIDE_TAC
985QED
986
987Theorem SUB_BAG_PSUB_BAG:
988 !(b1:'a -> num) b2.
989 SUB_BAG b1 b2 = PSUB_BAG b1 b2 \/ (b1 = b2)
990Proof
991 METIS_TAC [PSUB_BAG, SUB_BAG_REFL]
992QED
993
994val mono_cond = COND_RAND
995val mono_cond2 = COND_RATOR
996
997Theorem BAG_DELETE_PSUB_BAG:
998 !b0 (e:'a) b. BAG_DELETE b0 e b ==> PSUB_BAG b b0
999Proof
1000 SIMP_TAC std_ss [BAG_DELETE, SUB_BAG, PSUB_BAG, BAG_INSERT_DIFF,
1001 BAG_INN_BAG_INSERT]
1002QED
1003
1004val _ = print "Relating bags to (pred)sets\n";
1005
1006Definition SET_OF_BAG[nocompute]:
1007 SET_OF_BAG (b:'a->num) = \x. BAG_IN x b
1008End
1009
1010Definition BAG_OF_SET[nocompute]:
1011 BAG_OF_SET (P:'a->bool) = \x. if x IN P then 1 else 0
1012End
1013
1014Theorem BAG_OF_SET_UNION:
1015 !b b'. BAG_OF_SET (b UNION b') = (BAG_MERGE (BAG_OF_SET b) (BAG_OF_SET b'))
1016Proof
1017 rw[UNION_DEF,BAG_OF_SET,BAG_MERGE,FUN_EQ_THM] >> rw[] >> fs[]
1018QED
1019
1020Theorem BAG_OF_SET_DISJOINT_UNION:
1021 !s1 s2. DISJOINT s1 s2 ==>
1022 BAG_OF_SET (s1 UNION s2) = BAG_UNION (BAG_OF_SET s1) (BAG_OF_SET s2)
1023Proof
1024 rw[BAG_OF_SET, BAG_UNION, FUN_EQ_THM, IN_DISJOINT]
1025 \\ rw[] \\ metis_tac[]
1026QED
1027
1028Theorem BAG_OF_SET_INSERT:
1029 !e s. BAG_OF_SET (e INSERT s) = BAG_MERGE {|e|} (BAG_OF_SET s)
1030Proof
1031 rw[BAG_OF_SET,INSERT_DEF,BAG_MERGE,EMPTY_BAG,FUN_EQ_THM,BAG_INSERT] >>
1032 rw[IN_DEF]
1033 >- (fs[] >>
1034 `s e = F` by metis_tac[] >>
1035 fs[COND_CLAUSES])
1036 >- (`(x = e) = F` by metis_tac[] >>
1037 fs[COND_CLAUSES])
1038 >- (`(x = e) = F` by metis_tac[] >>
1039 `(s x) = T` by metis_tac[] >>
1040 fs[COND_CLAUSES])
1041QED
1042
1043Theorem BAG_OF_SET_INSERT_NON_ELEMENT:
1044 !e s. e NOTIN s ==>
1045 BAG_OF_SET (e INSERT s) = BAG_INSERT e (BAG_OF_SET s)
1046Proof
1047 rw[BAG_OF_SET_INSERT]
1048 \\ rw[Once BAG_INSERT, SimpRHS]
1049 \\ rw[BAG_MERGE, FUN_EQ_THM]
1050 \\ rw[]
1051 \\ gs[BAG_INSERT, EMPTY_BAG, BAG_OF_SET]
1052QED
1053
1054Theorem BAG_OF_SET_BAG_DIFF_DIFF:
1055 !b s. (BAG_OF_SET s) - b = (BAG_OF_SET (s DIFF (SET_OF_BAG b)))
1056Proof
1057 simp[BAG_OF_SET,DIFF_DEF,FUN_EQ_THM,BAG_DIFF,SET_OF_BAG] >>
1058 rw[BAG_IN,BAG_INN,IN_DEF] >> fs[]
1059QED
1060
1061Theorem SET_OF_EMPTY[simp]:
1062 BAG_OF_SET (EMPTY:'a->bool) = EMPTY_BAG
1063Proof
1064 SIMP_TAC (srw_ss()) [BAG_OF_SET, EMPTY_BAG, FUN_EQ_THM]
1065QED
1066
1067Theorem BAG_OF_SET_EQ_EMPTY_BAG[simp]:
1068 BAG_OF_SET s = {||} ⇔ s = ∅
1069Proof
1070 simp[EXTENSION] >> simp[FUN_EQ_THM, EMPTY_BAG, BAG_OF_SET, AllCaseEqs()]
1071QED
1072
1073Theorem SET_OF_SINGLETON_BAG[simp]:
1074 !e. SET_OF_BAG {|e|} = {e}
1075Proof rw[SET_OF_BAG,FUN_EQ_THM]
1076QED
1077
1078Theorem BAG_IN_BAG_OF_SET[simp]:
1079 !P p. BAG_IN p (BAG_OF_SET P) <=> p IN P
1080Proof SIMP_TAC std_ss [BAG_OF_SET, BAG_IN, BAG_INN, COND_RAND, COND_RATOR]
1081QED
1082
1083Theorem BAG_OF_EMPTY[simp]:
1084 SET_OF_BAG (EMPTY_BAG:'a->num) = EMPTY
1085Proof
1086 SIMP_TAC std_ss [FUN_EQ_THM, SET_OF_BAG, NOT_IN_EMPTY_BAG, EMPTY_DEF]
1087QED
1088
1089Theorem SET_BAG_I[simp]:
1090 !s:'a->bool. SET_OF_BAG (BAG_OF_SET s) = s
1091Proof
1092 SRW_TAC [][SET_OF_BAG, BAG_OF_SET, FUN_EQ_THM, BAG_IN, BAG_INN, IN_DEF] THEN
1093 SRW_TAC [][]
1094QED
1095
1096Theorem SUB_BAG_SET:
1097 !b1 b2:'a->num.
1098 SUB_BAG b1 b2 ==> (SET_OF_BAG b1) SUBSET (SET_OF_BAG b2)
1099Proof
1100 SIMP_TAC std_ss [SUB_BAG, SET_OF_BAG, BAG_IN, SPECIFICATION,
1101 SUBSET_DEF]
1102QED
1103
1104Theorem SET_OF_BAG_UNION:
1105 !b1 b2:'a->num. SET_OF_BAG (BAG_UNION b1 b2) =
1106 SET_OF_BAG b1 UNION SET_OF_BAG b2
1107Proof
1108 SRW_TAC [][SET_OF_BAG, EXTENSION] THEN SRW_TAC [][IN_DEF]
1109QED
1110
1111Theorem SET_OF_BAG_MERGE:
1112 !b1 b2. SET_OF_BAG (BAG_MERGE b1 b2) =
1113 SET_OF_BAG b1 UNION SET_OF_BAG b2
1114Proof
1115 ONCE_REWRITE_TAC[EXTENSION] THEN
1116 SIMP_TAC std_ss [SET_OF_BAG, IN_UNION, IN_ABS,
1117 BAG_IN_BAG_MERGE]
1118QED
1119
1120Theorem SET_OF_BAG_INSERT:
1121 !e b. SET_OF_BAG (BAG_INSERT e b) = e INSERT (SET_OF_BAG b)
1122Proof
1123 SIMP_TAC std_ss [SET_OF_BAG, BAG_INSERT, INSERT_DEF, BAG_IN,
1124 EXTENSION, GSPECIFICATION, BAG_INN] THEN
1125 SIMP_TAC std_ss [SPECIFICATION] THEN REPEAT GEN_TAC THEN
1126 COND_CASES_TAC THEN SIMP_TAC std_ss []
1127QED
1128
1129Theorem SET_OF_EL_BAG[simp]:
1130 !e. SET_OF_BAG (EL_BAG e) = {e}
1131Proof SIMP_TAC std_ss [EL_BAG, SET_OF_BAG_INSERT, BAG_OF_EMPTY]
1132QED
1133
1134Theorem SET_OF_BAG_DIFF_SUBSET_down:
1135 !b1 b2. (SET_OF_BAG b1) DIFF (SET_OF_BAG b2) SUBSET
1136 SET_OF_BAG (BAG_DIFF b1 b2)
1137Proof
1138 SIMP_TAC std_ss [SUBSET_DEF, IN_DIFF, BAG_DIFF, SET_OF_BAG, BAG_IN,
1139 BAG_INN] THEN
1140 SIMP_TAC std_ss [SPECIFICATION]
1141QED
1142
1143Theorem SET_OF_BAG_DIFF_SUBSET_up:
1144 !b1 b2. SET_OF_BAG (BAG_DIFF b1 b2) SUBSET SET_OF_BAG b1
1145Proof
1146 SIMP_TAC std_ss [SUBSET_DEF, BAG_DIFF, SET_OF_BAG, BAG_IN, BAG_INN]
1147 THEN SIMP_TAC std_ss [SPECIFICATION]
1148QED
1149
1150Theorem IN_SET_OF_BAG[simp]:
1151 !x b. x IN SET_OF_BAG b <=> BAG_IN x b
1152Proof SIMP_TAC std_ss [SET_OF_BAG, SPECIFICATION]
1153QED
1154
1155Theorem SET_OF_BAG_EQ_EMPTY[simp]:
1156 !b. (({} = SET_OF_BAG b) = (b = {||})) /\
1157 ((SET_OF_BAG b = {}) = (b = {||}))
1158Proof
1159 GEN_TAC THEN
1160 Q.SPEC_THEN `b` STRIP_ASSUME_TAC BAG_cases THEN
1161 SRW_TAC [][SET_OF_BAG_INSERT]
1162QED
1163
1164Theorem SET_OF_BAG_SING:
1165 !b e. SET_OF_BAG b = {e} <=> ?n. 0 < n /\ b = \x. if x = e then n else 0
1166Proof
1167 rw[SET_OF_BAG, Once EXTENSION]
1168 \\ rw[EQ_IMP_THM, BAG_IN, BAG_INN] \\ fs[]
1169 \\ pop_assum mp_tac \\ rw[]
1170 \\ qexists_tac`b e`
1171 \\ simp[FUN_EQ_THM] \\ rw[]
1172 >- (first_x_assum(qspec_then`e`mp_tac) \\ rw[])
1173 \\ first_x_assum(qspec_then`x`mp_tac) \\ rw[]
1174QED
1175
1176Theorem BAG_OF_SET_EQ_INSERT:
1177 !e b s. (BAG_INSERT e b = BAG_OF_SET s) ==> (?s'. s = (e INSERT s'))
1178Proof
1179 rw[] >>
1180 qexists_tac `s DELETE e` >>
1181 rw[INSERT_DEF,DELETE_DEF] >>
1182 simp[FUN_EQ_THM] >>
1183 rw[IN_DEF] >>
1184 EQ_TAC
1185 >- simp[]
1186 >- (rw[] >>
1187 `?t. s = (e INSERT t)`
1188 by metis_tac[DECOMPOSITION, BAG_IN_BAG_OF_SET, BAG_IN_BAG_INSERT] >>
1189 fs[])
1190QED
1191
1192
1193val _ = print "Bag disjointness\n"
1194Definition BAG_DISJOINT[nocompute]:
1195 BAG_DISJOINT (b1:'a->num) b2 =
1196 DISJOINT (SET_OF_BAG b1) (SET_OF_BAG b2)
1197End
1198
1199Theorem BAG_DISJOINT_EMPTY[simp]:
1200 !b:'a->num.
1201 BAG_DISJOINT b EMPTY_BAG /\ BAG_DISJOINT EMPTY_BAG b
1202Proof
1203 REWRITE_TAC [BAG_OF_EMPTY, BAG_DISJOINT, DISJOINT_EMPTY]
1204QED
1205
1206Theorem BAG_DISJOINT_DIFF:
1207 !B1 B2:'a->num.
1208 BAG_DISJOINT (BAG_DIFF B1 B2) (BAG_DIFF B2 B1)
1209Proof
1210 SIMP_TAC std_ss [INTER_DEF, DISJOINT_DEF, BAG_DISJOINT, BAG_DIFF,
1211 SET_OF_BAG, BAG_IN, BAG_INN, EXTENSION,
1212 GSPECIFICATION, NOT_IN_EMPTY] THEN
1213 SIMP_TAC std_ss [SPECIFICATION]
1214QED
1215
1216Theorem BAG_DISJOINT_BAG_IN:
1217 !b1 b2. BAG_DISJOINT b1 b2 =
1218 !e. ~(BAG_IN e b1) \/ ~(BAG_IN e b2)
1219Proof
1220 SIMP_TAC std_ss [BAG_DISJOINT, DISJOINT_DEF,
1221 EXTENSION, NOT_IN_EMPTY,
1222 IN_INTER, IN_SET_OF_BAG]
1223QED
1224
1225Theorem BAG_DISJOINT_BAG_INSERT:
1226 (!b1 b2 e1.
1227 BAG_DISJOINT (BAG_INSERT e1 b1) b2 =
1228 (~(BAG_IN e1 b2) /\ (BAG_DISJOINT b1 b2))) /\
1229 (!b1 b2 e2.
1230 BAG_DISJOINT b1 (BAG_INSERT e2 b2) =
1231 (~(BAG_IN e2 b1) /\ (BAG_DISJOINT b1 b2)))
1232Proof
1233 SIMP_TAC std_ss [BAG_DISJOINT_BAG_IN,
1234 BAG_IN_BAG_INSERT] THEN
1235 METIS_TAC[]
1236QED
1237
1238Theorem BAG_DISJOINT_BAG_UNION[simp]:
1239 (BAG_DISJOINT b1 (BAG_UNION b2 b3) <=>
1240 BAG_DISJOINT b1 b2 /\ BAG_DISJOINT b1 b3) /\
1241 (BAG_DISJOINT (BAG_UNION b1 b2) b3 <=>
1242 BAG_DISJOINT b1 b3 /\ BAG_DISJOINT b2 b3)
1243Proof
1244 SIMP_TAC (srw_ss()) [BAG_DISJOINT, SET_OF_BAG_UNION] THEN
1245 METIS_TAC[DISJOINT_SYM]
1246QED
1247
1248val _ = print "Developing theory of finite bags\n"
1249
1250Definition FINITE_BAG[nocompute]:
1251 FINITE_BAG (b:'a->num) =
1252 !P. P EMPTY_BAG /\ (!b. P b ==> (!e. P (BAG_INSERT e b))) ==>
1253 P b
1254End
1255
1256Theorem FINITE_EMPTY_BAG:
1257 FINITE_BAG EMPTY_BAG
1258Proof
1259 SIMP_TAC std_ss [FINITE_BAG]
1260QED
1261
1262Theorem FINITE_BAG_INSERT:
1263 !b. FINITE_BAG b ==> (!e. FINITE_BAG (BAG_INSERT e b))
1264Proof
1265 REWRITE_TAC [FINITE_BAG] THEN MESON_TAC []
1266QED
1267
1268Theorem FINITE_BAG_INDUCT:
1269 !P. P EMPTY_BAG /\
1270 (!b. P b ==> (!e. P (BAG_INSERT e b))) ==>
1271 (!b. FINITE_BAG b ==> P b)
1272Proof
1273 SIMP_TAC std_ss [FINITE_BAG]
1274QED
1275
1276Theorem STRONG_FINITE_BAG_INDUCT =
1277 FINITE_BAG_INDUCT
1278 |> Q.SPEC `\b. FINITE_BAG b /\ P b`
1279 |> SIMP_RULE std_ss [FINITE_EMPTY_BAG, FINITE_BAG_INSERT]
1280 |> GEN_ALL
1281
1282val _ = IndDefLib.export_rule_induction "STRONG_FINITE_BAG_INDUCT";
1283
1284Theorem FINITE_BAG_INSERT_down'[local]:
1285 !b. FINITE_BAG b ==> (!e b0. (b = BAG_INSERT e b0) ==> FINITE_BAG b0)
1286Proof
1287 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN
1288 SIMP_TAC std_ss [BAG_INSERT_NOT_EMPTY] THEN
1289 REPEAT STRIP_TAC THEN Q.ASM_CASES_TAC `e = e'` THENL [
1290 ELIM_TAC THEN IMP_RES_TAC BAG_INSERT_ONE_ONE THEN ELIM_TAC THEN
1291 ASM_SIMP_TAC std_ss [],
1292 ALL_TAC
1293 ] THEN Q.SUBGOAL_THEN `?b'. b = BAG_INSERT e' b'` STRIP_ASSUME_TAC
1294 THENL [
1295 SIMP_TAC std_ss [GSYM BAG_DELETE] THEN
1296 MATCH_MP_TAC BAG_IN_BAG_DELETE THEN
1297 FULL_SIMP_TAC (srw_ss()) [BAG_INSERT_EQUAL],
1298 RES_TAC THEN ELIM_TAC THEN
1299 RULE_ASSUM_TAC (ONCE_REWRITE_RULE [BAG_INSERT_commutes]) THEN
1300 FULL_SIMP_TAC (srw_ss()) [] THEN SRW_TAC [][FINITE_BAG_INSERT]
1301 ]
1302QED
1303
1304Theorem FINITE_BAG_INSERT[local]:
1305 !e b. FINITE_BAG (BAG_INSERT e b) = FINITE_BAG b
1306Proof
1307 MESON_TAC [FINITE_BAG_INSERT, FINITE_BAG_INSERT_down']
1308QED
1309
1310Theorem FINITE_BAG_THM[simp] =
1311 CONJ FINITE_EMPTY_BAG FINITE_BAG_INSERT
1312
1313Theorem FINITE_BAG_DIFF:
1314 !b1. FINITE_BAG b1 ==> !b2. FINITE_BAG (BAG_DIFF b1 b2)
1315Proof
1316 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN
1317 SIMP_TAC std_ss [BAG_DIFF_EMPTY, FINITE_BAG_THM] THEN
1318 REPEAT STRIP_TAC THEN Q.ASM_CASES_TAC `BAG_IN e b2` THENL [
1319 IMP_RES_TAC (REWRITE_RULE [BAG_DELETE] BAG_IN_BAG_DELETE) THEN
1320 ASM_SIMP_TAC std_ss [BAG_DIFF_INSERT_same],
1321 ASM_SIMP_TAC std_ss [BAG_DIFF_INSERT, FINITE_BAG_THM]
1322 ]
1323QED
1324
1325Theorem FINITE_BAG_DIFF_dual:
1326 !b1. FINITE_BAG b1 ==>
1327 !b2. FINITE_BAG (BAG_DIFF b2 b1) ==> FINITE_BAG b2
1328Proof
1329 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN
1330 REWRITE_TAC [BAG_DIFF_EMPTY] THEN
1331 REPEAT STRIP_TAC THEN Q.ASM_CASES_TAC `BAG_IN e b2` THENL [
1332 IMP_RES_TAC (REWRITE_RULE [BAG_DELETE] BAG_IN_BAG_DELETE) THEN
1333 ELIM_TAC THEN ASM_MESON_TAC [FINITE_BAG_THM, BAG_DIFF_INSERT_same],
1334 ASM_MESON_TAC [NOT_IN_BAG_DIFF]
1335 ]
1336QED
1337
1338Theorem FINITE_BAG_UNION_1[local]:
1339 !b1. FINITE_BAG b1 ==>
1340 !b2. FINITE_BAG b2 ==> FINITE_BAG (BAG_UNION b1 b2)
1341Proof
1342 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN
1343 SIMP_TAC std_ss [FINITE_BAG_THM, BAG_UNION_EMPTY, BAG_UNION_INSERT]
1344QED
1345Theorem FINITE_BAG_UNION_2[local]:
1346 !b. FINITE_BAG b ==>
1347 !b1 b2. (b = BAG_UNION b1 b2) ==> FINITE_BAG b1 /\ FINITE_BAG b2
1348Proof
1349 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN SRW_TAC [][] THEN
1350 MAP_EVERY IMP_RES_TAC [BAG_INSERT_EQ_UNION,
1351 REWRITE_RULE [BAG_DELETE] BAG_IN_BAG_DELETE] THEN
1352 ELIM_TAC THEN
1353 FULL_SIMP_TAC std_ss [BAG_UNION_INSERT, BAG_INSERT_ONE_ONE,
1354 FINITE_BAG_THM] THEN METIS_TAC []
1355QED
1356
1357Theorem FINITE_BAG_UNION[simp]:
1358 !b1 b2. FINITE_BAG (BAG_UNION b1 b2) <=>
1359 FINITE_BAG b1 /\ FINITE_BAG b2
1360Proof MESON_TAC [FINITE_BAG_UNION_1, FINITE_BAG_UNION_2]
1361QED
1362
1363Theorem FINITE_SUB_BAG:
1364 !b1. FINITE_BAG b1 ==> !b2. SUB_BAG b2 b1 ==> FINITE_BAG b2
1365Proof
1366 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN
1367 SIMP_TAC std_ss [SUB_BAG_EMPTY, FINITE_BAG_THM] THEN
1368 REPEAT STRIP_TAC THEN Q.ASM_CASES_TAC `BAG_IN e b2` THENL [
1369 IMP_RES_TAC (REWRITE_RULE [BAG_DELETE] BAG_IN_BAG_DELETE) THEN
1370 ELIM_TAC THEN FULL_SIMP_TAC std_ss [SUB_BAG_INSERT, FINITE_BAG_THM],
1371 ASM_MESON_TAC [NOT_IN_SUB_BAG_INSERT]
1372 ]
1373QED
1374
1375Theorem FINITE_BAG_MERGE[simp]:
1376 !a b. FINITE_BAG (BAG_MERGE a b) <=> FINITE_BAG a /\ FINITE_BAG b
1377Proof
1378 rw[] >>
1379 reverse(EQ_TAC)
1380 >- (`BAG_MERGE a b <= a + b` by metis_tac[BAG_MERGE_SUB_BAG_UNION] >>
1381 rw[] >>
1382 `FINITE_BAG (a + b)` by metis_tac[FINITE_BAG_UNION] >>
1383 metis_tac[FINITE_SUB_BAG])
1384 >- (`!c:'a bag. FINITE_BAG c ==> !a b. (c = BAG_MERGE a b)
1385 ==> FINITE_BAG a /\ FINITE_BAG b` suffices_by metis_tac[] >>
1386 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT >>
1387 rw[] >>
1388 `BAG_MERGE a b = BAG_INSERT e (BAG_MERGE (a - {|e|}) (b - {|e|}))`
1389 by metis_tac[BAG_INSERT_EQ_MERGE_DIFF] >>
1390 fs[] >>
1391 rw[] >>
1392 first_x_assum (qspecl_then [`a - {|e|}`,`b - {|e|}`] mp_tac) >>
1393 rw[] >>
1394 metis_tac[FINITE_BAG_DIFF_dual,FINITE_BAG])
1395QED
1396
1397Theorem FINITE_EL_BAG[simp]:
1398 FINITE_BAG (EL_BAG e)
1399Proof
1400 rw[EL_BAG]
1401QED
1402
1403val _ = print "Developing theory of bag cardinality\n"
1404
1405Definition BAG_CARD_RELn[nocompute]:
1406 BAG_CARD_RELn (b:'a->num) n =
1407 !P. P EMPTY_BAG 0 /\
1408 (!b n. P b n ==> (!e. P (BAG_INSERT e b) (SUC n))) ==>
1409 P b n
1410End
1411
1412Theorem BCARD_imps[local]:
1413 (BAG_CARD_RELn EMPTY_BAG 0) /\
1414 (!b n. BAG_CARD_RELn b n ==>
1415 (!e. BAG_CARD_RELn (BAG_INSERT e b) (n + 1)))
1416Proof
1417 REWRITE_TAC [BAG_CARD_RELn, arithmeticTheory.ADD1] THEN MESON_TAC []
1418QED
1419
1420Theorem BCARD_induct[local]:
1421 !P. P EMPTY_BAG 0 /\
1422 (!b n. P b n ==> (!e. P (BAG_INSERT e b) (n + 1))) ==>
1423 (!b n. BAG_CARD_RELn b n ==> P b n)
1424Proof
1425 REWRITE_TAC [BAG_CARD_RELn, arithmeticTheory.ADD1] THEN MESON_TAC []
1426QED
1427
1428val strong_BCARD_induct =
1429 BCARD_induct |> Q.SPEC `\b n. BAG_CARD_RELn b n /\ P b n`
1430 |> SIMP_RULE std_ss [BCARD_imps]
1431
1432Theorem BCARD_R_cases[local]:
1433 !b n. BAG_CARD_RELn b n ==>
1434 (b = EMPTY_BAG) /\ (n = 0) \/
1435 (?b0 e m. (b = BAG_INSERT e b0) /\
1436 BAG_CARD_RELn b0 m /\ (n = m + 1))
1437Proof
1438 HO_MATCH_MP_TAC BCARD_induct THEN SIMP_TAC std_ss [] THEN
1439 REPEAT STRIP_TAC THEN ELIM_TAC THEN ASM_MESON_TAC [BCARD_imps]
1440QED
1441
1442Theorem BCARD_rwts[local]:
1443 !b n. BAG_CARD_RELn b n <=>
1444 (b = EMPTY_BAG) /\ (n = 0) \/
1445 (?b0 e m. (b = BAG_INSERT e b0) /\ (n = m + 1) /\
1446 BAG_CARD_RELn b0 m)
1447Proof
1448 METIS_TAC [BCARD_R_cases, BCARD_imps]
1449QED
1450
1451Theorem BCARD_BINSERT_indifferent[local]:
1452 !b n. BAG_CARD_RELn b n ==>
1453 !b0 e. (b = BAG_INSERT e b0) ==>
1454 BAG_CARD_RELn b0 (n - 1) /\ ~(n = 0)
1455Proof
1456 HO_MATCH_MP_TAC strong_BCARD_induct THEN SRW_TAC [][] THEN
1457 FULL_SIMP_TAC (srw_ss()) [BAG_INSERT_EQUAL] THEN1 SRW_TAC [][] THEN
1458 `BAG_CARD_RELn k (n - 1) /\ n <> 0` by METIS_TAC [] THEN
1459 `n = (n - 1) + 1` by DECIDE_TAC THEN METIS_TAC [BCARD_imps]
1460QED
1461
1462val BCARD_BINSERT' =
1463 SIMP_RULE bool_ss [GSYM RIGHT_FORALL_IMP_THM] BCARD_BINSERT_indifferent
1464
1465Theorem BCARD_EMPTY[local]:
1466 !n. BAG_CARD_RELn EMPTY_BAG n = (n = 0)
1467Proof
1468 ONCE_REWRITE_TAC [BCARD_rwts] THEN
1469 SIMP_TAC std_ss [BAG_INSERT_NOT_EMPTY]
1470QED
1471
1472Theorem BCARD_BINSERT[local]:
1473 !b e n. BAG_CARD_RELn (BAG_INSERT e b) n =
1474 (?m. (n = m + 1) /\ BAG_CARD_RELn b m)
1475Proof
1476 SRW_TAC [][EQ_IMP_THM] THENL [
1477 IMP_RES_TAC BCARD_BINSERT' THEN Q.EXISTS_TAC `n - 1` THEN
1478 ASM_SIMP_TAC std_ss [],
1479 ASM_MESON_TAC [BCARD_imps]
1480 ]
1481QED
1482
1483val BCARD_RWT = CONJ BCARD_EMPTY BCARD_BINSERT
1484
1485Theorem BCARD_R_det[local]:
1486 !b n. BAG_CARD_RELn b n ==>
1487 !n'. BAG_CARD_RELn b n' ==> (n' = n)
1488Proof
1489 HO_MATCH_MP_TAC BCARD_induct THEN CONJ_TAC THENL [
1490 ONCE_REWRITE_TAC [BCARD_rwts] THEN
1491 SIMP_TAC std_ss [BAG_INSERT_NOT_EMPTY],
1492 REPEAT STRIP_TAC THEN IMP_RES_TAC BCARD_BINSERT THEN RES_TAC THEN
1493 ASM_SIMP_TAC std_ss []
1494 ]
1495QED
1496
1497Theorem FINITE_BAGS_BCARD[local]:
1498 !b. FINITE_BAG b ==> ?n. BAG_CARD_RELn b n
1499Proof
1500 HO_MATCH_MP_TAC FINITE_BAG_INDUCT THEN MESON_TAC [BCARD_imps]
1501QED
1502
1503val BAG_CARD = new_specification
1504 ("BAG_CARD",["BAG_CARD"],
1505 CONV_RULE SKOLEM_CONV (
1506 SIMP_RULE std_ss
1507 [GSYM boolTheory.RIGHT_EXISTS_IMP_THM] FINITE_BAGS_BCARD));
1508
1509val BAG_CARD_EMPTY =
1510 BAG_CARD |> Q.SPEC `EMPTY_BAG`
1511 |> SIMP_RULE std_ss [FINITE_EMPTY_BAG]
1512 |> ONCE_REWRITE_RULE [BCARD_rwts]
1513 |> SIMP_RULE std_ss [BAG_INSERT_NOT_EMPTY]
1514Theorem BAG_CARD_EMPTY[simp] = BAG_CARD_EMPTY;
1515
1516Theorem BCARD_0:
1517 !b. FINITE_BAG b ==> ((BAG_CARD b = 0) = (b = EMPTY_BAG))
1518Proof
1519 GEN_TAC THEN STRIP_TAC THEN EQ_TAC THEN
1520 SIMP_TAC std_ss [BAG_CARD_EMPTY] THEN
1521 IMP_RES_TAC BAG_CARD THEN DISCH_THEN SUBST_ALL_TAC THEN
1522 FULL_SIMP_TAC (srw_ss()) [Once BCARD_rwts]
1523QED
1524
1525Theorem BAG_CARD_EL_BAG[local]:
1526 !e. BAG_CARD (EL_BAG e) = 1
1527Proof
1528 GEN_TAC THEN SIMP_TAC std_ss [EL_BAG] THEN
1529 Q.SUBGOAL_THEN `FINITE_BAG (BAG_INSERT e EMPTY_BAG)` ASSUME_TAC
1530 THENL [MESON_TAC [FINITE_BAG_INSERT, FINITE_EMPTY_BAG],
1531 ALL_TAC] THEN IMP_RES_TAC BAG_CARD THEN
1532 FULL_SIMP_TAC std_ss [BCARD_RWT]
1533QED
1534
1535Theorem BAG_CARD_INSERT[local]:
1536 !b. FINITE_BAG b ==>
1537 !e. BAG_CARD (BAG_INSERT e b) = BAG_CARD b + 1
1538Proof
1539 REPEAT STRIP_TAC THEN
1540 Q.SUBGOAL_THEN `FINITE_BAG (BAG_INSERT e b)` ASSUME_TAC THENL [
1541 ASM_MESON_TAC [FINITE_BAG_INSERT], ALL_TAC] THEN
1542 IMP_RES_TAC BAG_CARD THEN
1543 FULL_SIMP_TAC std_ss [BCARD_RWT] THEN IMP_RES_TAC BCARD_R_det
1544QED
1545
1546Theorem BAG_CARD_THM =
1547 CONJ BAG_CARD_EMPTY BAG_CARD_INSERT;
1548
1549Theorem BAG_CARD_UNION[simp]:
1550 !b1 b2. FINITE_BAG b1 /\ FINITE_BAG b2 ==>
1551 (BAG_CARD (BAG_UNION b1 b2) =
1552 (BAG_CARD b1) + (BAG_CARD b2))
1553Proof
1554 SIMP_TAC std_ss [GSYM AND_IMP_INTRO, RIGHT_FORALL_IMP_THM] THEN
1555 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN
1556 SIMP_TAC arith_ss [BAG_UNION_INSERT, BAG_UNION_EMPTY,
1557 BAG_CARD_THM, FINITE_BAG_UNION]
1558QED
1559
1560
1561Theorem BCARD_SUC:
1562 !b. FINITE_BAG b ==>
1563 !n. (BAG_CARD b = SUC n) =
1564 (?b0 e. (b = BAG_INSERT e b0) /\ (BAG_CARD b0 = n))
1565Proof
1566 GEN_TAC THEN STRUCT_CASES_TAC (Q.SPEC `b` BAG_cases) THEN
1567 SIMP_TAC std_ss [BAG_CARD_THM, BAG_INSERT_NOT_EMPTY,
1568 FINITE_BAG_THM, arithmeticTheory.ADD1] THEN
1569 REPEAT STRIP_TAC THEN EQ_TAC THEN STRIP_TAC THENL [
1570 ASM_MESON_TAC [],
1571 FIRST_ASSUM (MP_TAC o Q.AP_TERM `BAG_CARD`) THEN
1572 ASM_SIMP_TAC std_ss [BAG_CARD_THM] THEN
1573 Q.SUBGOAL_THEN `FINITE_BAG b0'` ASSUME_TAC THENL [
1574 ASM_MESON_TAC [FINITE_BAG_THM],
1575 ASM_SIMP_TAC std_ss [BAG_CARD_THM]
1576 ]
1577 ]
1578QED
1579
1580Theorem BAG_CARD_BAG_INN:
1581 !b. FINITE_BAG b ==> !n e. BAG_INN e n b ==> n <= BAG_CARD b
1582Proof
1583 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN
1584 SIMP_TAC std_ss [BAG_CARD_THM, BAG_INN_BAG_INSERT,
1585 BAG_INN_EMPTY_BAG] THEN REPEAT STRIP_TAC
1586 THENL [
1587 ELIM_TAC THEN RES_TAC THEN ASM_SIMP_TAC std_ss [],
1588 RES_TAC THEN ASM_SIMP_TAC std_ss []
1589 ]
1590QED
1591
1592Theorem SUB_BAG_DIFF_EQ:
1593 !b1 b2. SUB_BAG b1 b2 ==> (b2 = BAG_UNION b1 (BAG_DIFF b2 b1))
1594Proof
1595 RW_TAC bool_ss [SUB_BAG,BAG_UNION,BAG_DIFF,BAG_INN,FUN_EQ_THM]
1596 THEN MATCH_MP_TAC (ARITH `a >= b ==> (a = b + (a - b))`)
1597 THEN POP_ASSUM (MP_TAC o Q.SPECL [`x`, `b1 x`])
1598 THEN RW_TAC arith_ss []
1599QED
1600
1601Theorem SUB_BAG_DIFF_EXISTS[local]:
1602 !b1 b2. SUB_BAG b1 b2 ==> ?d. b2 = BAG_UNION b1 d
1603Proof
1604 PROVE_TAC [SUB_BAG_DIFF_EQ]
1605QED
1606
1607Theorem SUB_BAG_CARD:
1608 !b1 b2:'a bag. FINITE_BAG b2 /\ SUB_BAG b1 b2 ==> BAG_CARD b1 <= BAG_CARD b2
1609Proof
1610RW_TAC bool_ss []
1611 THEN `?d. b2 = BAG_UNION b1 d` by PROVE_TAC [SUB_BAG_DIFF_EQ]
1612 THEN RW_TAC bool_ss []
1613 THEN `FINITE_BAG d /\ FINITE_BAG b1` by PROVE_TAC [FINITE_BAG_UNION]
1614 THEN Q.PAT_X_ASSUM `SUB_BAG x y` (K ALL_TAC)
1615 THEN Q.PAT_X_ASSUM `FINITE_BAG (BAG_UNION x y)` (K ALL_TAC)
1616 THEN REPEAT (POP_ASSUM MP_TAC)
1617 THEN Q.ID_SPEC_TAC `d`
1618 THEN HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT
1619 THEN RW_TAC arith_ss [BAG_UNION_EMPTY,BAG_UNION_INSERT]
1620 THEN PROVE_TAC [BAG_CARD_THM,FINITE_BAG_UNION,ARITH `x <=y ==> x <= y+1`]
1621QED
1622
1623Theorem BAG_MERGE_CARD:
1624 !a b. FINITE_BAG a /\ FINITE_BAG b ==>
1625 BAG_CARD (BAG_MERGE a b) <= (BAG_CARD a + BAG_CARD b)
1626Proof
1627 rw[] >>
1628 `(BAG_MERGE a b) <= (a + b)`
1629 by metis_tac[BAG_MERGE_SUB_BAG_UNION] >>
1630 `FINITE_BAG (a + b)` by metis_tac[FINITE_BAG_UNION] >>
1631 `BAG_CARD (BAG_MERGE a b) <= BAG_CARD (a + b)`
1632 by metis_tac[SUB_BAG_CARD] >>
1633 metis_tac[BAG_CARD_UNION]
1634QED
1635
1636val _ = ParseExtras.temp_tight_equality()
1637Theorem BAG_CARD_DIFF:
1638 !b. FINITE_BAG b ==>
1639 !c. c <= b ==> BAG_CARD (b - c) = BAG_CARD b - BAG_CARD c
1640Proof
1641 Induct_on `FINITE_BAG` >> simp[BAG_CARD_THM] >> qx_gen_tac `b` >> strip_tac >>
1642 map_every qx_gen_tac [`e`, `c`] >> strip_tac >>
1643 `FINITE_BAG c` by metis_tac[FINITE_BAG_THM, FINITE_SUB_BAG] >>
1644 Cases_on `BAG_IN e c`
1645 >- (`?c0. c = BAG_INSERT e c0` by metis_tac[BAG_DECOMPOSE] >>
1646 lfs[BAG_CARD_THM, SUB_BAG_INSERT]) >>
1647 simp[BAG_DIFF_INSERT, BAG_CARD_THM, FINITE_BAG_DIFF] >>
1648 lfs[NOT_IN_SUB_BAG_INSERT] >>
1649 `BAG_CARD c <= BAG_CARD b` by simp[SUB_BAG_CARD] >> simp[]
1650QED
1651
1652(* --------------------------------------------------------------------
1653 FILTER for bags (alternatively, intersection with a set)
1654 ---------------------------------------------------------------------- *)
1655
1656Definition BAG_FILTER_DEF[nocompute]:
1657 BAG_FILTER P (b :'a bag) : 'a bag = \e. if P e then b e else 0
1658End
1659
1660Theorem BAG_FILTER_EMPTY[simp]:
1661 BAG_FILTER P {||} = {||}
1662Proof
1663 SRW_TAC [][BAG_FILTER_DEF, FUN_EQ_THM] THEN
1664 SRW_TAC [][EMPTY_BAG]
1665QED
1666
1667Theorem BAG_FILTER_BAG_INSERT[simp]:
1668 BAG_FILTER P (BAG_INSERT e b) = if P e then BAG_INSERT e (BAG_FILTER P b)
1669 else BAG_FILTER P b
1670Proof
1671 SRW_TAC [][BAG_FILTER_DEF, FUN_EQ_THM] THEN
1672 SRW_TAC [][BAG_INSERT] THEN RES_TAC
1673QED
1674
1675Theorem FINITE_BAG_FILTER[simp]:
1676 !b. FINITE_BAG b ==> FINITE_BAG (BAG_FILTER P b)
1677Proof
1678 HO_MATCH_MP_TAC FINITE_BAG_INDUCT THEN SRW_TAC [][] THEN
1679 SRW_TAC [][]
1680QED
1681
1682Theorem BAG_INN_BAG_FILTER[simp]:
1683 BAG_INN e n (BAG_FILTER P b) <=> (n = 0) \/ P e /\ BAG_INN e n b
1684Proof
1685 SRW_TAC [numSimps.ARITH_ss][BAG_FILTER_DEF, BAG_INN]
1686QED
1687
1688Theorem BAG_IN_BAG_FILTER[simp]:
1689 BAG_IN e (BAG_FILTER P b) <=> P e /\ BAG_IN e b
1690Proof
1691 SRW_TAC [][BAG_IN]
1692QED
1693
1694Theorem BAG_FILTER_FILTER:
1695 BAG_FILTER P (BAG_FILTER Q b) = BAG_FILTER (\a. P a /\ Q a) b
1696Proof
1697 simp[BAG_FILTER_DEF] >> simp[FUN_EQ_THM] >> rw[] >> fs[]
1698QED
1699
1700Theorem BAG_FILTER_SUB_BAG[simp]:
1701 !P b. BAG_FILTER P b <= b
1702Proof
1703 dsimp[BAG_FILTER_DEF, SUB_BAG]
1704QED
1705
1706Theorem BAG_FILTER_BAG_UNION:
1707 BAG_FILTER P (BAG_UNION b1 b2) =
1708 BAG_UNION (BAG_FILTER P b1) (BAG_FILTER P b2)
1709Proof
1710 rw[FUN_EQ_THM, BAG_FILTER_DEF, BAG_UNION] \\ rw[]
1711QED
1712
1713Theorem BAG_OF_SET_DIFF:
1714 !b b'. BAG_OF_SET (b DIFF b') = BAG_FILTER (COMPL b') (BAG_OF_SET b)
1715Proof
1716 rw[DIFF_DEF,BAG_OF_SET,BAG_FILTER_DEF] >> metis_tac[]
1717QED
1718
1719Theorem BAG_FILTER_BAG_OF_SET:
1720 !P s. BAG_FILTER P (BAG_OF_SET s) = BAG_OF_SET (s INTER { x | P x })
1721Proof
1722 rw[BAG_FILTER_DEF, FUN_EQ_THM, BAG_OF_SET] \\ rw[] \\ fs[]
1723QED
1724
1725Theorem BAG_FILTER_SPLIT:
1726 !s b. BAG_UNION (BAG_FILTER s b) (BAG_FILTER (COMPL s) b) = b
1727Proof
1728 rw[FUN_EQ_THM, BAG_UNION, BAG_FILTER_DEF, IN_DEF] \\ rw[]
1729QED
1730
1731Theorem SET_OF_BAG_EQ_INSERT:
1732 !b e s.
1733 (e INSERT s = SET_OF_BAG b) =
1734 ?b0 eb. (b = BAG_UNION eb b0) /\
1735 (s = SET_OF_BAG b0) /\
1736 (!e'. BAG_IN e' eb ==> (e' = e)) /\
1737 (~(e IN s) ==> BAG_IN e eb)
1738Proof
1739 REPEAT GEN_TAC THEN EQ_TAC THEN STRIP_TAC THENL [
1740 `BAG_IN e b` by METIS_TAC [IN_INSERT, IN_SET_OF_BAG] THEN
1741 Cases_on `e IN s` THENL [
1742 MAP_EVERY Q.EXISTS_TAC [`b`, `{||}`] THEN
1743 SRW_TAC [][] THEN METIS_TAC [ABSORPTION],
1744 MAP_EVERY Q.EXISTS_TAC [`BAG_FILTER ((~) o (=) e) b`,
1745 `BAG_FILTER ((=) e) b`] THEN
1746 REPEAT CONJ_TAC THENL [
1747 SRW_TAC [boolSimps.DNF_ss, boolSimps.CONJ_ss]
1748 [BAG_EXTENSION, BAG_INN_BAG_UNION] THEN
1749 PROVE_TAC [BAG_INN_0],
1750 FULL_SIMP_TAC (srw_ss()) [EXTENSION] THEN PROVE_TAC [],
1751 SRW_TAC [][],
1752 SRW_TAC [][]
1753 ]
1754 ],
1755 SRW_TAC [][EXTENSION, BAG_IN_BAG_UNION] THEN
1756 FULL_SIMP_TAC (srw_ss()) [] THEN PROVE_TAC []
1757 ]
1758QED
1759
1760Theorem FINITE_SET_OF_BAG[simp]:
1761 !b. FINITE (SET_OF_BAG b) = FINITE_BAG b
1762Proof
1763 Q_TAC SUFF_TAC
1764 `(!b:'a bag. FINITE_BAG b ==> FINITE (SET_OF_BAG b)) /\
1765 (!s:'a set. FINITE s ==>
1766 !b. (s = SET_OF_BAG b) ==> FINITE_BAG b)` THEN1
1767 METIS_TAC [] THEN CONJ_TAC
1768 THENL [
1769 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN
1770 SRW_TAC [][SET_OF_BAG_INSERT],
1771 HO_MATCH_MP_TAC FINITE_INDUCT THEN
1772 SRW_TAC [][SET_OF_BAG_EQ_INSERT, SET_OF_BAG_EQ_EMPTY] THEN
1773 SRW_TAC [][FINITE_BAG_UNION] THEN
1774 Q_TAC SUFF_TAC `!n b e. (b e = n) /\ (!e'. BAG_IN e' b ==> (e' = e)) ==>
1775 FINITE_BAG b` THEN1 METIS_TAC [] THEN
1776 REPEAT (POP_ASSUM (K ALL_TAC)) THEN Induct THENL [
1777 REPEAT STRIP_TAC THEN
1778 Q_TAC SUFF_TAC `b = {||}` THEN1 SRW_TAC [][] THEN
1779 SRW_TAC [][BAG_EXTENSION] THEN
1780 FULL_SIMP_TAC (srw_ss()) [BAG_INN, BAG_IN] THEN EQ_TAC THENL [
1781 SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN
1782 `b e' >= 1`
1783 by PROVE_TAC [numLib.ARITH_PROVE
1784 ``x >= n /\ ~(n = 0) ==> x >= 1n``] THEN
1785 `b e' = 0` by PROVE_TAC [] THEN
1786 FULL_SIMP_TAC (srw_ss()) [],
1787 SIMP_TAC (srw_ss()) []
1788 ],
1789 REPEAT STRIP_TAC THEN
1790 `BAG_IN e b` by SRW_TAC [numSimps.ARITH_ss][BAG_IN, BAG_INN] THEN
1791 `?b0. b = BAG_INSERT e b0`
1792 by PROVE_TAC [BAG_IN_BAG_DELETE, BAG_DELETE] THEN
1793 POP_ASSUM SUBST_ALL_TAC THEN
1794 FULL_SIMP_TAC (srw_ss()) [DISJ_IMP_THM] THEN
1795 `b0 e = n`
1796 by FULL_SIMP_TAC (srw_ss() ++ numSimps.ARITH_ss) [BAG_INSERT] THEN
1797 PROVE_TAC []
1798 ]
1799 ]
1800QED
1801
1802Theorem FINITE_BAG_OF_SET[simp]:
1803 !s. FINITE_BAG (BAG_OF_SET s) <=> FINITE s
1804Proof
1805 rw[] >> EQ_TAC
1806 >- (`!c. FINITE_BAG c ==> !s. (c = BAG_OF_SET s) ==> FINITE s`
1807 suffices_by metis_tac[] >>
1808 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT >>
1809 rpt strip_tac
1810 >- fs[]
1811 >- (`e IN s`
1812 by metis_tac[BAG_IN_BAG_OF_SET,
1813 BAG_DECOMPOSE,BAG_IN_BAG_INSERT] >>
1814 `?t. s = (e INSERT t)`
1815 by metis_tac[DECOMPOSITION] >>
1816 fs[BAG_OF_SET_INSERT] >>
1817 `(BAG_MERGE {|e|} (BAG_OF_SET t))
1818 = (BAG_INSERT e
1819 (BAG_MERGE ({|e|}-{|e|}) ((BAG_OF_SET t)-{|e|})))`
1820 by metis_tac[BAG_INSERT_EQ_MERGE_DIFF] >>
1821 fs[BAG_MERGE_EMPTY] >>
1822 `BAG_OF_SET t - {|e|} = BAG_OF_SET (t DIFF {e})`
1823 by (simp[BAG_OF_SET_BAG_DIFF_DIFF] >>
1824 metis_tac[SET_OF_EL_BAG,EL_BAG]) >>
1825 first_x_assum (qspec_then `t DIFF {e}` mp_tac) >> DISCH_TAC >>
1826 metis_tac[FINITE_DIFF_down,FINITE_DEF]))
1827 >- (rw[] >>
1828 Induct_on `s` >>
1829 simp[SET_OF_EMPTY] >>
1830 rw[] >>
1831 simp[BAG_OF_SET_INSERT] >>
1832 simp[FINITE_BAG_MERGE])
1833QED
1834
1835Theorem BAG_CARD_BAG_OF_SET:
1836 !s. FINITE s ==> BAG_CARD (BAG_OF_SET s) = CARD s
1837Proof
1838 ho_match_mp_tac FINITE_INDUCT
1839 \\ rw[]
1840 \\ rw[BAG_OF_SET_INSERT_NON_ELEMENT]
1841 \\ rw[BAG_CARD_THM]
1842QED
1843
1844Theorem SET_OF_BAG_SING_CARD:
1845 !b e. SET_OF_BAG b = {e} ==> BAG_CARD b = b e
1846Proof
1847 rpt gen_tac THEN
1848 Induct_on`b e` \\ rw[]
1849 >- gs[SET_OF_BAG_SING]
1850 \\ `BAG_IN e b` by simp[BAG_IN, BAG_INN]
1851 \\ drule BAG_DECOMPOSE \\ disch_then(qx_choose_then`b'`strip_assume_tac)
1852 \\ first_x_assum(qspecl_then[`b'`,`e`]mp_tac)
1853 \\ `FINITE {e}` by simp[]
1854 \\ `FINITE_BAG b` by metis_tac[FINITE_SET_OF_BAG]
1855 \\ `FINITE_BAG b'` by metis_tac[FINITE_BAG_THM]
1856 \\ Cases_on`b' = {||}` \\ gs[]
1857 \\ fs[BAG_CARD_THM]
1858 >- simp[BAG_INSERT, EMPTY_BAG]
1859 \\ impl_tac >- fs[BAG_INSERT]
1860 \\ fs[SET_OF_BAG_INSERT]
1861 \\ impl_tac
1862 >- (
1863 fs[EXTENSION]
1864 \\ rw[EQ_IMP_THM]
1865 >- metis_tac[]
1866 \\ qspec_then`b'`strip_assume_tac BAG_cases \\ gs[]
1867 \\ metis_tac[] )
1868 \\ rw[]
1869 \\ last_x_assum(assume_tac o SYM) \\ simp[]
1870 \\ simp[BAG_CARD_THM, arithmeticTheory.ADD1]
1871 \\ fs[BAG_INSERT]
1872QED
1873
1874Theorem BAG_OF_SET_INJ[simp]:
1875 !s1 s2. BAG_OF_SET s1 = BAG_OF_SET s2 <=> s1 = s2
1876Proof
1877 rw[Once FUN_EQ_THM, BAG_OF_SET]
1878 \\ simp[Once EXTENSION]
1879 \\ rw[EQ_IMP_THM]
1880 \\ first_x_assum(qspec_then`x`mp_tac) \\ rw[]
1881QED
1882
1883
1884(* ----------------------------------------------------------------------
1885 IMAGE for bags.
1886
1887 This is complicated by the fact that a taking the image of a
1888 non-injective function over an infinite bag might produce a bag that
1889 wanted to have an infinite number of some element. For example,
1890 BAG_IMAGE (\e. 1) (BAG_OF_SET (UNIV : num set))
1891 would want to populate a bag with an infinite number of ones.
1892
1893 BAG_IMAGE is "safe" if the input bag is finite, or if the function is
1894 only finitely non-injective. I don't want to have these side conditions
1895 hanging around on my theorems, so I've decided to simply make BAG_IMAGE
1896 take elements that want to be infinite to one instead.
1897 ---------------------------------------------------------------------- *)
1898
1899val _ = augment_srw_ss [simpLib.rewrites [LET_THM]]
1900Definition BAG_IMAGE_DEF[nocompute]:
1901 BAG_IMAGE f b = \e. let sb = BAG_FILTER (\e0. f e0 = e) b
1902 in
1903 if FINITE_BAG sb then BAG_CARD sb
1904 else 1
1905End
1906
1907Theorem BAG_IMAGE_EMPTY[simp]:
1908 !f. BAG_IMAGE f {||} = {||}
1909Proof
1910 SRW_TAC [][BAG_IMAGE_DEF] THEN SRW_TAC [][EMPTY_BAG_alt]
1911QED
1912
1913Theorem BAG_IMAGE_FINITE_INSERT[simp]:
1914 !b f e. FINITE_BAG b ==>
1915 (BAG_IMAGE f (BAG_INSERT e b) = BAG_INSERT (f e) (BAG_IMAGE f b))
1916Proof
1917 SRW_TAC [][BAG_IMAGE_DEF] THEN
1918 SRW_TAC [][FUN_EQ_THM] THEN
1919 REPEAT GEN_TAC THEN
1920 Cases_on `f e = e'` THENL [
1921 SRW_TAC [][BAG_CARD_THM] THEN SRW_TAC [][BAG_INSERT],
1922 SRW_TAC [][] THEN SRW_TAC [][BAG_INSERT]
1923 ]
1924QED
1925
1926Theorem BAG_IMAGE_FINITE_UNION[simp]:
1927 !b1 b2 f. (FINITE_BAG b1 /\ FINITE_BAG b2)
1928 ==> (BAG_IMAGE f (BAG_UNION b1 b2)
1929 = (BAG_UNION (BAG_IMAGE f b1) (BAG_IMAGE f b2)))
1930Proof
1931 REPEAT STRIP_TAC THEN
1932 Q.PAT_X_ASSUM `FINITE_BAG b1` MP_TAC THEN
1933 Q.SPEC_TAC (`b1`, `b1`) THEN
1934 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN
1935 ASM_SIMP_TAC std_ss [BAG_UNION_INSERT, BAG_UNION_EMPTY, BAG_IMAGE_EMPTY,
1936 BAG_IMAGE_FINITE_INSERT, FINITE_BAG_UNION]
1937QED
1938
1939Theorem BAG_IMAGE_FINITE[simp]:
1940 !b. FINITE_BAG b ==> FINITE_BAG (BAG_IMAGE f b)
1941Proof
1942 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN SRW_TAC [][]
1943QED
1944
1945Theorem BAG_IMAGE_COMPOSE:
1946 !f g b. FINITE_BAG b ==>
1947 ((BAG_IMAGE (f o g) b = BAG_IMAGE f (BAG_IMAGE g b)))
1948Proof
1949 GEN_TAC THEN GEN_TAC THEN
1950 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN
1951 SIMP_TAC std_ss [BAG_IMAGE_EMPTY, BAG_IMAGE_FINITE_INSERT,
1952 BAG_IMAGE_FINITE]
1953QED
1954
1955Theorem BAG_IMAGE_FINITE_I[simp]:
1956 !b. FINITE_BAG b ==> (BAG_IMAGE I b = b)
1957Proof
1958 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN SRW_TAC [][]
1959QED
1960
1961Theorem BAG_IMAGE_CONG:
1962 !f1 b1 f2 b2.
1963 b1 = b2 /\ (!x. BAG_IN x b1 ==> f1 x = f2 x)
1964 ==>
1965 BAG_IMAGE f1 b1 = BAG_IMAGE f2 b2
1966Proof
1967 rw[]
1968 \\ rw[BAG_IMAGE_DEF, FUN_EQ_THM]
1969 \\ qmatch_goalsub_abbrev_tac`FINITE_BAG c1`
1970 \\ irule EQ_SYM
1971 \\ qmatch_goalsub_abbrev_tac`FINITE_BAG c2`
1972 \\ `c1 = c2` suffices_by rw[]
1973 \\ rw[Abbr`c1`,Abbr`c2`, BAG_FILTER_DEF, FUN_EQ_THM]
1974 \\ fs[BAG_IN, BAG_INN] \\ rw[]
1975 \\ metis_tac[DECIDE``~(x >= 1) ==> x = 0``]
1976QED
1977
1978Theorem BAG_IN_FINITE_BAG_IMAGE[simp]:
1979 FINITE_BAG b ==>
1980 (BAG_IN x (BAG_IMAGE f b) = ?y. (f y = x) /\ BAG_IN y b)
1981Proof
1982 SRW_TAC [][BAG_IMAGE_DEF] THEN EQ_TAC THEN STRIP_TAC THENL [
1983 FULL_SIMP_TAC (srw_ss()) [BAG_IN, BAG_INN] THEN
1984 Q.ABBREV_TAC `bf = BAG_FILTER (\e0. f e0 = x) b` THEN
1985 `FINITE_BAG bf` by (Q.UNABBREV_TAC `bf` THEN SRW_TAC [][]) THEN
1986 `0 < BAG_CARD bf` by SRW_TAC [numSimps.ARITH_ss][] THEN
1987 `?m. BAG_CARD bf = SUC m`
1988 by PROVE_TAC [arithmeticTheory.num_CASES,
1989 arithmeticTheory.NOT_ZERO_LT_ZERO] THEN
1990 `?e bf0. (bf = BAG_INSERT e bf0)` by PROVE_TAC [BCARD_SUC] THEN
1991 `BAG_IN e bf` by simp[] THEN
1992 `BAG_IN e (BAG_FILTER (\e0. f e0 = x) b)` by PROVE_TAC [] THEN
1993 POP_ASSUM (STRIP_ASSUME_TAC o SIMP_RULE bool_ss [BAG_IN_BAG_FILTER]) THEN
1994 PROVE_TAC [BAG_IN, BAG_INN],
1995 `?b0. BAG_DELETE b y b0` by PROVE_TAC [BAG_IN_BAG_DELETE] THEN
1996 `b = BAG_INSERT y b0` by PROVE_TAC [BAG_DELETE] THEN
1997 SIMP_TAC (srw_ss()) [BAG_IN, BAG_INN] THEN SRW_TAC [][] THEN
1998 FULL_SIMP_TAC (srw_ss() ++ numSimps.ARITH_ss) [BAG_CARD_THM]
1999 ]
2000QED
2001
2002Theorem BAG_IN_BAG_IMAGE_IMP:
2003 !x f b. BAG_IN x (BAG_IMAGE f b) ==> ?y. BAG_IN y b /\ f y = x
2004Proof
2005 rpt gen_tac THEN
2006 Cases_on`FINITE_BAG b` \\ rw[]
2007 >- metis_tac[]
2008 \\ fs[BAG_IMAGE_DEF]
2009 \\ pop_assum mp_tac
2010 \\ simp[Once BAG_IN, BAG_INN]
2011 \\ qmatch_goalsub_abbrev_tac`BAG_CARD bb`
2012 \\ qspec_then`bb`strip_assume_tac BAG_cases >- simp[]
2013 \\ fs[markerTheory.Abbrev_def]
2014 \\ strip_tac
2015 \\ qexists_tac`e`
2016 \\ simp[Once CONJ_COMM]
2017 \\ qho_match_abbrev_tac`P e /\ _`
2018 \\ `BAG_IN e (BAG_FILTER P b)` suffices_by metis_tac[BAG_IN_BAG_FILTER]
2019 \\ metis_tac[BAG_IN_BAG_INSERT]
2020QED
2021
2022Theorem BAG_IMAGE_EQ_EMPTY[simp]:
2023 FINITE_BAG b ==> ((BAG_IMAGE f b = {||}) <=> (b = {||}))
2024Proof
2025 qid_spec_tac `b` >> ho_match_mp_tac STRONG_FINITE_BAG_INDUCT >>
2026 simp[]
2027QED
2028
2029Theorem ITSET_BAG_INSERT_BAG_UNION_BAG_IMAGE_BAG_OF_SET:
2030 !f s. FINITE s ==> !a.
2031 ITSET (\x b. BAG_INSERT (f x) b) s a =
2032 BAG_UNION a (BAG_IMAGE f (BAG_OF_SET s))
2033Proof
2034 gen_tac
2035 \\ ho_match_mp_tac FINITE_INDUCT
2036 \\ rw[ITSET_EMPTY]
2037 \\ dep_rewrite.DEP_REWRITE_TAC[COMMUTING_ITSET_INSERT]
2038 \\ rw[] >- metis_tac[BAG_INSERT_commutes]
2039 \\ fs[DELETE_NON_ELEMENT]
2040 \\ fs[GSYM DELETE_NON_ELEMENT]
2041 \\ simp[BAG_OF_SET_INSERT_NON_ELEMENT]
2042 \\ simp[BAG_INSERT_UNION]
2043 \\ simp[AC ASSOC_BAG_UNION COMM_BAG_UNION]
2044QED
2045
2046Theorem BAG_IMAGE_BAG_OF_SET_ITSET_BAG_INSERT:
2047 !f s. FINITE s ==>
2048 BAG_IMAGE f (BAG_OF_SET s) = ITSET (\x b. BAG_INSERT (f x) b) s {||}
2049Proof
2050 rw[ITSET_BAG_INSERT_BAG_UNION_BAG_IMAGE_BAG_OF_SET]
2051QED
2052
2053(*---------------------------------------------------------------------------
2054 CHOICE and REST for bags.
2055 ---------------------------------------------------------------------------*)
2056
2057val BAG_CHOICE_DEF = new_specification
2058 ("BAG_CHOICE_DEF",["BAG_CHOICE"],
2059 Q.prove(`?ch:('a -> num) -> 'a. !b. ~(b = {||}) ==> BAG_IN (ch b) b`,
2060 PROVE_TAC [BAG_MEMBER_NOT_EMPTY]));
2061
2062
2063(* ===================================================================== *)
2064(* The REST of a bag after removing a chosen element. *)
2065(* ===================================================================== *)
2066
2067Definition BAG_REST_DEF[nocompute]:
2068 BAG_REST b = BAG_DIFF b (EL_BAG (BAG_CHOICE b))
2069End
2070
2071
2072Theorem BAG_INSERT_CHOICE_REST:
2073 !b:'a bag. ~(b = {||}) ==> (b = BAG_INSERT (BAG_CHOICE b) (BAG_REST b))
2074Proof
2075 REPEAT STRIP_TAC
2076 THEN IMP_RES_THEN MP_TAC BAG_CHOICE_DEF
2077 THEN NORM_TAC arith_ss
2078 [BAG_INSERT,BAG_REST_DEF,BAG_DIFF,EL_BAG,BAG_IN,BAG_INN,
2079 EMPTY_BAG,combinTheory.K_DEF,FUN_EQ_THM]
2080QED
2081
2082Theorem BAG_CHOICE_SING[simp]:
2083 BAG_CHOICE {|x|} = x
2084Proof
2085 Q.SPEC_THEN `{|x|}` MP_TAC BAG_CHOICE_DEF THEN SRW_TAC [][]
2086QED
2087
2088Theorem BAG_REST_SING[simp]:
2089 BAG_REST {|x|} = {||}
2090Proof
2091 SRW_TAC [][BAG_REST_DEF,EL_BAG]
2092QED
2093
2094Theorem SUB_BAG_REST:
2095 !b:'a bag. SUB_BAG (BAG_REST b) b
2096Proof
2097 NORM_TAC arith_ss [BAG_REST_DEF,SUB_BAG,BAG_INN,BAG_DIFF,EL_BAG,BAG_INSERT,
2098 arithmeticTheory.GREATER_EQ]
2099QED
2100
2101Theorem PSUB_BAG_REST:
2102 !b:'a bag. ~(b = {||}) ==> PSUB_BAG (BAG_REST b) b
2103Proof
2104 REPEAT STRIP_TAC
2105 THEN IMP_RES_THEN MP_TAC BAG_CHOICE_DEF
2106 THEN NORM_TAC arith_ss [BAG_REST_DEF,PSUB_BAG, SUB_BAG,BAG_IN, BAG_INN,
2107 BAG_DIFF,EL_BAG,BAG_INSERT,EMPTY_BAG,combinTheory.K_DEF,FUN_EQ_THM]
2108 THENL [ALL_TAC, Q.EXISTS_TAC `BAG_CHOICE b`]
2109 THEN RW_TAC arith_ss []
2110QED
2111
2112
2113
2114Theorem BAG_UNION_STABLE[local]:
2115 !b1 b2. (b1 = BAG_UNION b1 b2) = (b2 = {||})
2116Proof
2117 RW_TAC bool_ss [BAG_UNION,EMPTY_BAG_alt,FUN_EQ_THM] THEN
2118 EQ_TAC THEN DISCH_THEN (fn th => GEN_TAC THEN MP_TAC(SPEC_ALL th)) THEN
2119 RW_TAC arith_ss []
2120QED
2121
2122Theorem SUB_BAG_UNION_MONO_0[local]:
2123 !x y. SUB_BAG x (BAG_UNION x y)
2124Proof
2125 RW_TAC arith_ss [SUB_BAG,BAG_UNION,BAG_INN]
2126QED
2127Theorem SUB_BAG_UNION_MONO[simp] =
2128 CONJ SUB_BAG_UNION_MONO_0
2129 (ONCE_REWRITE_RULE [COMM_BAG_UNION] SUB_BAG_UNION_MONO_0)
2130
2131Theorem PSUB_BAG_CARD:
2132 !b1 b2:'a bag. FINITE_BAG b2 /\ PSUB_BAG b1 b2 ==> BAG_CARD b1 < BAG_CARD b2
2133Proof
2134RW_TAC bool_ss [PSUB_BAG]
2135 THEN `?d. b2 = BAG_UNION b1 d` by PROVE_TAC [SUB_BAG_DIFF_EQ]
2136 THEN RW_TAC bool_ss []
2137 THEN `~(d = {||})` by PROVE_TAC [BAG_UNION_STABLE]
2138 THEN STRIP_ASSUME_TAC (Q.SPEC`d` BAG_cases)
2139 THEN RW_TAC bool_ss [BAG_UNION_INSERT]
2140 THEN POP_ASSUM (K ALL_TAC)
2141 THEN `FINITE_BAG (BAG_UNION b1 b0)`
2142 by PROVE_TAC[FINITE_BAG_UNION, BAG_UNION_INSERT, FINITE_BAG_THM]
2143 THEN PROVE_TAC [BAG_CARD_THM, ARITH `x < y + 1n <=> x <= y`,
2144 SUB_BAG_CARD, SUB_BAG_UNION_MONO]
2145QED
2146
2147Theorem EL_BAG_BAG_INSERT[simp]:
2148 {|x|} = BAG_INSERT y b <=> x = y /\ b = {||}
2149Proof
2150 simp[EQ_IMP_THM] >>
2151 simp[BAG_EXTENSION, BAG_INN, BAG_INSERT, EMPTY_BAG] >>
2152 strip_tac >>
2153 `x = y`
2154 by (spose_not_then assume_tac >>
2155 first_x_assum (qspecl_then [`1`, `y`] mp_tac) >>
2156 simp[]) >> rw[] >>
2157 simp[EQ_IMP_THM] >> spose_not_then strip_assume_tac >> Cases_on `e = x`
2158 >- (rw[] >> first_x_assum (qspecl_then [`n+1`, `e`] mp_tac) >>
2159 simp[]) >>
2160 first_x_assum (qspecl_then [`n`, `e`] mp_tac) >> simp[]
2161QED
2162
2163Theorem EL_BAG_SUB_BAG[simp]:
2164 {| x |} <= b <=> BAG_IN x b
2165Proof
2166 simp_tac (srw_ss() ++ COND_elim_ss ++ DNF_ss)
2167 [SUB_BAG, BAG_INN, BAG_IN, BAG_INSERT, EMPTY_BAG, EQ_IMP_THM,
2168 arithmeticTheory.GREATER_EQ] >> simp[]
2169QED
2170
2171Theorem FINITE_SUB_BAGS:
2172 !b. FINITE_BAG b ==> FINITE { s | s <= b }
2173Proof
2174 ho_match_mp_tac STRONG_FINITE_BAG_INDUCT
2175 \\ rw[]
2176 \\ qmatch_assum_abbrev_tac`FINITE sb`
2177 \\ qmatch_abbrev_tac`FINITE eb`
2178 \\ `eb = sb UNION (IMAGE (BAG_INSERT e) sb)` suffices_by simp[]
2179 \\ simp[SET_EQ_SUBSET, SUBSET_DEF, Abbr`sb`, Abbr`eb`, PULL_EXISTS]
2180 \\ reverse conj_tac
2181 >- simp[SUB_BAG_INSERT, SUB_BAG_INSERT_I]
2182 \\ rw[]
2183 \\ reverse(Cases_on`BAG_IN e x`)
2184 >- metis_tac[NOT_IN_SUB_BAG_INSERT]
2185 \\ imp_res_tac BAG_DECOMPOSE \\ rw[]
2186 \\ fs[SUB_BAG_INSERT]
2187QED
2188
2189(* ----------------------------------------------------------------------
2190 A "fold"-like operation for bags, ITBAG, by analogy with the set
2191 theory's ITSET.
2192 ---------------------------------------------------------------------- *)
2193
2194val ITBAG_defn = Defn.Hol_defn "ITBAG"
2195 `ITBAG (b: 'a bag) (acc: 'b) =
2196 if FINITE_BAG b then
2197 if b = {||} then acc
2198 else ITBAG (BAG_REST b) (f (BAG_CHOICE b) acc)
2199 else ARB`;
2200
2201(* Termination of above *)
2202val (ITBAG_eqn0, ITBAG_IND) =
2203 Defn.tprove(ITBAG_defn,
2204 TotalDefn.WF_REL_TAC `measure (BAG_CARD o FST)` THEN
2205 PROVE_TAC [PSUB_BAG_CARD, PSUB_BAG_REST]);
2206
2207(* derive the desired recursion equation:
2208 FINITE_BAG b ==>
2209 (ITBAG f b a = if b = {||} then a
2210 else ITBAG f (BAG_REST b) (f (BAG_CHOICE b) a))
2211*)
2212val ITBAG_THM =
2213 GENL [``b: 'a -> num``, ``f:'a -> 'b -> 'b``, ``acc:'b``]
2214 (DISCH_ALL (ASM_REWRITE_RULE [Q.ASSUME `FINITE_BAG b`] ITBAG_eqn0))
2215
2216Theorem ITBAG_IND = ITBAG_IND;
2217Theorem ITBAG_THM = ITBAG_THM;
2218
2219Theorem ITBAG_EMPTY[simp] =
2220 REWRITE_RULE [] (MATCH_MP (Q.SPEC `{||}` ITBAG_THM) FINITE_EMPTY_BAG)
2221
2222Theorem ITBAG_INSERT =
2223 SIMP_RULE (srw_ss())[] (Q.SPEC `BAG_INSERT x b` ITBAG_THM)
2224
2225Theorem COMMUTING_ITBAG_INSERT:
2226 !f b. (!x y z. f x (f y z) = f y (f x z)) /\ FINITE_BAG b ==>
2227 !x a. ITBAG f (BAG_INSERT x b) a = ITBAG f b (f x a)
2228Proof
2229 REPEAT GEN_TAC THEN STRIP_TAC THEN
2230 completeInduct_on `BAG_CARD b` THEN
2231 FULL_SIMP_TAC (srw_ss()) [GSYM RIGHT_FORALL_IMP_THM, AND_IMP_INTRO] THEN
2232 SRW_TAC [][ITBAG_INSERT, BAG_REST_DEF, EL_BAG] THEN
2233 Q.ABBREV_TAC `c = BAG_CHOICE (BAG_INSERT x b)` THEN
2234 `BAG_IN c (BAG_INSERT x b)`
2235 by PROVE_TAC [BAG_CHOICE_DEF, BAG_INSERT_NOT_EMPTY] THEN
2236 `(c = x) \/ BAG_IN c b` by PROVE_TAC [BAG_IN_BAG_INSERT] THENL [
2237 SRW_TAC [][],
2238 `?b0. b = BAG_INSERT c b0`
2239 by PROVE_TAC [BAG_IN_BAG_DELETE, BAG_DELETE] THEN
2240 `BAG_DIFF (BAG_INSERT x b) {| c |} = BAG_INSERT x b0`
2241 by SRW_TAC [][BAG_INSERT_commutes] THEN
2242 ASM_REWRITE_TAC [] THEN
2243 `FINITE_BAG b0` by FULL_SIMP_TAC (srw_ss()) [] THEN
2244 `BAG_CARD b0 < BAG_CARD b`
2245 by SRW_TAC [numSimps.ARITH_ss][BAG_CARD_THM] THEN
2246 SRW_TAC [][]
2247 ]
2248QED
2249
2250Theorem COMMUTING_ITBAG_RECURSES:
2251 !f e b a. (!x y z. f x (f y z) = f y (f x z)) /\ FINITE_BAG b ==>
2252 (ITBAG f (BAG_INSERT e b) a = f e (ITBAG f b a))
2253Proof
2254 Q_TAC SUFF_TAC
2255 `!f. (!x y z. f x (f y z) = f y (f x z)) ==>
2256 !b. FINITE_BAG b ==>
2257 !e a. ITBAG f (BAG_INSERT e b) a = f e (ITBAG f b a)` THEN1
2258 PROVE_TAC [] THEN
2259 GEN_TAC THEN STRIP_TAC THEN
2260 ASM_SIMP_TAC (srw_ss()) [COMMUTING_ITBAG_INSERT] THEN
2261 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN CONJ_TAC THENL [
2262 SRW_TAC [][ITBAG_EMPTY],
2263 SRW_TAC [][COMMUTING_ITBAG_INSERT]
2264 ]
2265QED
2266
2267Theorem ITBAG_SING[simp]:
2268 ITBAG f {|x|} a = f x a
2269Proof
2270 dep_rewrite.DEP_ONCE_REWRITE_TAC[ITBAG_THM] \\ rw[]
2271QED
2272
2273(*---------------------------------------------------------------------------*)
2274(* Sums and products on finite bags *)
2275(*---------------------------------------------------------------------------*)
2276
2277Definition BAG_GEN_SUM_def[nocompute]:
2278 BAG_GEN_SUM bag (n:num) = ITBAG (+) bag n
2279End
2280
2281Definition BAG_GEN_PROD_def[nocompute]:
2282 BAG_GEN_PROD bag n = ITBAG $* bag n
2283End
2284
2285Theorem BAG_GEN_SUM_EMPTY:
2286 !n. BAG_GEN_SUM {||} n = n
2287Proof
2288 RW_TAC bool_ss [BAG_GEN_SUM_def,ITBAG_EMPTY]
2289QED
2290
2291Theorem BAG_GEN_PROD_EMPTY:
2292 !n. BAG_GEN_PROD {||} n = n
2293Proof
2294 RW_TAC bool_ss [BAG_GEN_PROD_def,ITBAG_EMPTY]
2295QED
2296
2297Theorem BAG_GEN_SUM_TAILREC:
2298 !b. FINITE_BAG b ==>
2299 !x a. BAG_GEN_SUM (BAG_INSERT x b) a = BAG_GEN_SUM b (x + a)
2300Proof
2301 GEN_TAC THEN STRIP_TAC THEN
2302 SIMP_TAC bool_ss [BAG_GEN_SUM_def] THEN
2303 HO_MATCH_MP_TAC (SPEC_ALL COMMUTING_ITBAG_INSERT) THEN
2304 RW_TAC std_ss []
2305QED
2306
2307Theorem BAG_GEN_SUM_REC:
2308 !b. FINITE_BAG b ==>
2309 !x a. BAG_GEN_SUM (BAG_INSERT x b) a = x + BAG_GEN_SUM b a
2310Proof
2311 GEN_TAC THEN REPEAT STRIP_TAC THEN
2312 SIMP_TAC bool_ss [BAG_GEN_SUM_def] THEN
2313 HO_MATCH_MP_TAC (SPEC_ALL COMMUTING_ITBAG_RECURSES) THEN
2314 RW_TAC std_ss []
2315QED
2316
2317Theorem BAG_GEN_PROD_TAILREC:
2318 !b. FINITE_BAG b ==>
2319 !x a. BAG_GEN_PROD (BAG_INSERT x b) a = BAG_GEN_PROD b (x * a)
2320Proof
2321 GEN_TAC THEN STRIP_TAC THEN
2322 SIMP_TAC bool_ss [BAG_GEN_PROD_def] THEN
2323 HO_MATCH_MP_TAC (SPEC_ALL COMMUTING_ITBAG_INSERT) THEN
2324 RW_TAC std_ss []
2325QED
2326
2327Theorem BAG_GEN_PROD_REC:
2328 !b. FINITE_BAG b ==>
2329 !x a. BAG_GEN_PROD (BAG_INSERT x b) a = x * BAG_GEN_PROD b a
2330Proof
2331 GEN_TAC THEN REPEAT STRIP_TAC THEN
2332 SIMP_TAC bool_ss [BAG_GEN_PROD_def] THEN
2333 HO_MATCH_MP_TAC (SPEC_ALL COMMUTING_ITBAG_RECURSES) THEN
2334 RW_TAC std_ss []
2335QED
2336
2337Theorem BAG_GEN_PROD_EQ_1:
2338 !b. FINITE_BAG b ==> !e. (BAG_GEN_PROD b e = 1) ==> (e=1)
2339Proof
2340 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN REPEAT STRIP_TAC THENL
2341 [METIS_TAC [BAG_GEN_PROD_EMPTY],
2342 Q.PAT_X_ASSUM `p=q` MP_TAC THEN
2343 RW_TAC std_ss [Once BAG_GEN_PROD_TAILREC] THEN
2344 RES_TAC THEN FULL_SIMP_TAC std_ss []]
2345QED
2346
2347Theorem BAG_GEN_PROD_ALL_ONES:
2348 !b. FINITE_BAG b ==> (BAG_GEN_PROD b 1 = 1) ==> !x. BAG_IN x b ==> (x=1)
2349Proof
2350 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN REPEAT STRIP_TAC THENL
2351 [METIS_TAC [NOT_IN_EMPTY_BAG],
2352 Q.PAT_X_ASSUM `p=q` MP_TAC THEN
2353 RW_TAC std_ss [BAG_GEN_PROD_TAILREC] THEN
2354 `e=1` by METIS_TAC [BAG_GEN_PROD_EQ_1] THEN RW_TAC std_ss [] THEN
2355 `!x. BAG_IN x b ==> (x = 1)` by METIS_TAC[] THEN
2356 METIS_TAC [BAG_IN_BAG_INSERT]]
2357QED
2358
2359Theorem BAG_GEN_PROD_POSITIVE:
2360 !b. FINITE_BAG b ==> (!x. BAG_IN x b ==> 0 < x) ==> 0 < BAG_GEN_PROD b 1
2361Proof
2362 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN REPEAT STRIP_TAC THENL
2363 [METIS_TAC [BAG_GEN_PROD_EMPTY,ARITH `0<1`],
2364 RW_TAC std_ss [BAG_GEN_PROD_REC] THEN
2365 `0 < e` by METIS_TAC [BAG_IN_BAG_INSERT] THEN
2366 `0 < BAG_GEN_PROD b 1` by METIS_TAC [BAG_IN_BAG_INSERT] THEN
2367 METIS_TAC [arithmeticTheory.LESS_MULT2]]
2368QED
2369
2370Definition BAG_EVERY[nocompute]:
2371 BAG_EVERY P b = !e. BAG_IN e b ==> P e
2372End
2373
2374Theorem BAG_EVERY_THM[simp]:
2375 (!P. BAG_EVERY P EMPTY_BAG) /\
2376 (!P e b. BAG_EVERY P (BAG_INSERT e b) <=> P e /\ BAG_EVERY P b)
2377Proof
2378SIMP_TAC (srw_ss()) [BAG_EVERY] THEN METIS_TAC []
2379QED
2380
2381Theorem BAG_EVERY_UNION[simp]:
2382 BAG_EVERY P (b1 + b2) <=> BAG_EVERY P b1 /\ BAG_EVERY P b2
2383Proof
2384SRW_TAC [][BAG_EVERY] THEN METIS_TAC []
2385QED
2386
2387Theorem BAG_EVERY_MERGE[simp]:
2388 BAG_EVERY P (BAG_MERGE b1 b2) <=> BAG_EVERY P b1 /\ BAG_EVERY P b2
2389Proof
2390SRW_TAC [][BAG_EVERY, DISJ_IMP_THM, FORALL_AND_THM]
2391QED
2392
2393Theorem BAG_EVERY_SET:
2394 BAG_EVERY P b <=> SET_OF_BAG b SUBSET {x | P x}
2395Proof
2396SRW_TAC [][BAG_EVERY, SET_OF_BAG, SUBSET_DEF]
2397QED
2398
2399Theorem BAG_FILTER_EQ_EMPTY:
2400 (BAG_FILTER P b = {||}) <=> BAG_EVERY ($~ o P) b
2401Proof
2402 SRW_TAC [][BAG_EXTENSION,BAG_INN_BAG_FILTER,BAG_EVERY,BAG_IN,EQ_IMP_THM] THEN1
2403 (FIRST_X_ASSUM (Q.SPECL_THEN [`1`,`e`] MP_TAC)
2404 THEN SRW_TAC [][] ) THEN
2405 FIRST_X_ASSUM (Q.SPEC_THEN `e` MP_TAC) THEN
2406 SRW_TAC [][] THEN
2407 Cases_on `n < 1` THEN1 DECIDE_TAC THEN
2408 (BAG_INN_LESS |> Q.SPECL [`b`,`e`,`n`,`1`] |> CONTRAPOS |> IMP_RES_TAC) THEN
2409 FULL_SIMP_TAC (srw_ss()) [] THEN
2410 `n = 1` by DECIDE_TAC THEN
2411 SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) []
2412QED
2413
2414Theorem SET_OF_BAG_IMAGE[simp]:
2415 SET_OF_BAG (BAG_IMAGE f b) = IMAGE f (SET_OF_BAG b)
2416Proof
2417 SRW_TAC[][EXTENSION, BAG_IMAGE_DEF, BAG_IN, BAG_INN] >>
2418 Q.ABBREV_TAC `bf = BAG_FILTER (\e0. f e0 = x) b` >>
2419 qspec_then ‘bf’ mp_tac BAG_cases THEN
2420 SRW_TAC [][] THEN SRW_TAC [][] THENL [
2421 FULL_SIMP_TAC (srw_ss()) [BAG_FILTER_EQ_EMPTY,BAG_EVERY,BAG_IN,BAG_INN] THEN
2422 PROVE_TAC [],
2423 fs[BAG_CARD_THM],
2424 FULL_SIMP_TAC (srw_ss()) [],
2425 ALL_TAC
2426 ] THEN
2427 `~BAG_EVERY ($~ o (\e0. f e0 = x)) b`
2428 by PROVE_TAC [BAG_FILTER_EQ_EMPTY,BAG_INSERT_NOT_EMPTY] THEN
2429 FULL_SIMP_TAC (srw_ss()) [BAG_EVERY,BAG_IN,BAG_INN] THEN
2430 PROVE_TAC []
2431QED
2432
2433Theorem BAG_IMAGE_FINITE_RESTRICTED_I:
2434 !b. FINITE_BAG b /\ BAG_EVERY (\e. f e = e) b ==> (BAG_IMAGE f b = b)
2435Proof
2436 REWRITE_TAC [GSYM AND_IMP_INTRO] THEN
2437 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN SRW_TAC [][]
2438QED
2439
2440Definition BAG_ALL_DISTINCT[nocompute]:
2441 BAG_ALL_DISTINCT b = (!e. b e <= 1:num)
2442End
2443
2444Theorem BAG_ALL_DISTINCT_THM[simp]:
2445 BAG_ALL_DISTINCT EMPTY_BAG /\
2446 !e b. BAG_ALL_DISTINCT (BAG_INSERT e b) <=>
2447 ~BAG_IN e b /\ BAG_ALL_DISTINCT b
2448Proof
2449 `(!x. ((x + 1 <= 1) = (x = 0)) /\ (~(x >= 1) = (x = 0))) /\ 0n <= 1`
2450 by bossLib.DECIDE_TAC THEN
2451 SRW_TAC [COND_elim_ss, DNF_ss]
2452 [BAG_ALL_DISTINCT, EMPTY_BAG, BAG_INSERT, BAG_IN, BAG_INN,
2453 EQ_IMP_THM] THEN METIS_TAC []
2454QED
2455
2456Theorem forall_eq_thm[local]:
2457 (!s:'a. (P s = Q s)) ==> ((!s. P s) = (!s. Q s))
2458Proof
2459 STRIP_TAC THEN ASM_REWRITE_TAC[]
2460QED
2461
2462Theorem BAG_ALL_DISTINCT_BAG_MERGE:
2463 !b1 b2. BAG_ALL_DISTINCT (BAG_MERGE b1 b2) =
2464 (BAG_ALL_DISTINCT b1 /\ BAG_ALL_DISTINCT b2)
2465Proof
2466 SIMP_TAC std_ss [BAG_ALL_DISTINCT, BAG_MERGE,
2467 GSYM FORALL_AND_THM, COND_RAND, COND_RATOR,
2468 COND_EXPAND_IMP] THEN
2469 REPEAT STRIP_TAC THEN
2470 HO_MATCH_MP_TAC forall_eq_thm THEN
2471 GEN_TAC THEN bossLib.DECIDE_TAC
2472QED
2473
2474
2475Theorem BAG_ALL_DISTINCT_BAG_UNION:
2476 !b1 b2.
2477 BAG_ALL_DISTINCT (BAG_UNION b1 b2) =
2478 (BAG_ALL_DISTINCT b1 /\ BAG_ALL_DISTINCT b2 /\
2479 BAG_DISJOINT b1 b2)
2480Proof
2481 SIMP_TAC std_ss [BAG_ALL_DISTINCT, BAG_UNION,
2482 BAG_DISJOINT, DISJOINT_DEF, EXTENSION,
2483 NOT_IN_EMPTY, IN_INTER,
2484 IN_SET_OF_BAG, BAG_IN,
2485 BAG_INN, GSYM FORALL_AND_THM] THEN
2486 REPEAT STRIP_TAC THEN
2487 HO_MATCH_MP_TAC forall_eq_thm THEN
2488 GEN_TAC THEN bossLib.DECIDE_TAC
2489QED
2490
2491Theorem BAG_ALL_DISTINCT_DIFF:
2492 !b1 b2.
2493 BAG_ALL_DISTINCT b1 ==>
2494 BAG_ALL_DISTINCT (BAG_DIFF b1 b2)
2495Proof
2496 SIMP_TAC std_ss [BAG_ALL_DISTINCT, BAG_DIFF] THEN
2497 REPEAT STRIP_TAC THEN
2498 `b1 e <= 1` by PROVE_TAC[] THEN
2499 bossLib.DECIDE_TAC
2500QED
2501
2502
2503Theorem BAG_ALL_DISTINCT_DELETE:
2504 BAG_ALL_DISTINCT b = !e. e <: b ==> ~(e <: b - {|e|})
2505Proof
2506 SRW_TAC [][BAG_ALL_DISTINCT, BAG_IN, BAG_INN, BAG_DIFF, BAG_INSERT,
2507 EMPTY_BAG, EQ_IMP_THM] THEN
2508 FIRST_X_ASSUM (Q.SPEC_THEN `e` MP_TAC) THEN DECIDE_TAC
2509QED
2510
2511Theorem BAG_ALL_DISTINCT_SET:
2512 BAG_ALL_DISTINCT b <=> (BAG_OF_SET (SET_OF_BAG b) = b)
2513Proof
2514 SRW_TAC [][BAG_ALL_DISTINCT, FUN_EQ_THM, SET_OF_BAG,
2515 BAG_INN, BAG_IN, BAG_INSERT, EMPTY_BAG, BAG_OF_SET] THEN
2516 EQ_TAC THEN STRIP_TAC THEN Q.X_GEN_TAC `e` THEN
2517 POP_ASSUM (Q.SPEC_THEN `e` MP_TAC) THEN DECIDE_TAC
2518QED
2519
2520Theorem BAG_ALL_DISTINCT_BAG_OF_SET[simp]:
2521 BAG_ALL_DISTINCT (BAG_OF_SET s)
2522Proof
2523 SRW_TAC [][BAG_ALL_DISTINCT_SET]
2524QED
2525
2526
2527Theorem BAG_IN_BAG_DIFF_ALL_DISTINCT:
2528 !b1 b2 e. BAG_ALL_DISTINCT b1 ==>
2529 (BAG_IN e (BAG_DIFF b1 b2) <=> BAG_IN e b1 /\ ~BAG_IN e b2)
2530Proof
2531 SIMP_TAC std_ss [BAG_ALL_DISTINCT, BAG_IN, BAG_INN, BAG_DIFF] THEN
2532 REPEAT STRIP_TAC THEN `b1 e <= 1` by PROVE_TAC[] THEN DECIDE_TAC
2533QED
2534
2535Theorem SUB_BAG_ALL_DISTINCT:
2536 !b1 b2. BAG_ALL_DISTINCT b1 ==>
2537 (SUB_BAG b1 b2 = (!x. BAG_IN x b1 ==> BAG_IN x b2))
2538Proof
2539 SIMP_TAC std_ss [BAG_ALL_DISTINCT, SUB_BAG, BAG_INN, BAG_IN] THEN
2540 REPEAT STRIP_TAC THEN EQ_TAC THEN STRIP_TAC THENL [
2541 PROVE_TAC[],
2542
2543 REPEAT STRIP_TAC THEN
2544 Cases_on `n = 0` THEN FULL_SIMP_TAC std_ss [] THEN
2545 Q.PAT_X_ASSUM `!e. b1 e <= 1` (ASSUME_TAC o Q.SPEC `x`) THEN
2546 `n = 1` by DECIDE_TAC THEN
2547 FULL_SIMP_TAC std_ss []
2548 ]
2549QED
2550
2551Theorem BAG_ALL_DISTINCT_BAG_INN:
2552 !b n e. BAG_ALL_DISTINCT b ==>
2553 (BAG_INN e n b <=> n = 0 \/ n = 1 /\ BAG_IN e b)
2554Proof
2555 SIMP_TAC std_ss [BAG_INN, BAG_ALL_DISTINCT, BAG_IN] THEN
2556 REPEAT STRIP_TAC THEN
2557 Cases_on `n = 0` THEN ASM_SIMP_TAC std_ss [] THEN
2558 Cases_on `n = 1` THEN1 ASM_SIMP_TAC std_ss [] THEN
2559 `b e <= 1` by PROVE_TAC[] THEN
2560 DECIDE_TAC
2561QED
2562
2563
2564Theorem BAG_ALL_DISTINCT_EXTENSION:
2565 !b1 b2. (BAG_ALL_DISTINCT b1 /\ BAG_ALL_DISTINCT b2) ==>
2566 ((b1 = b2) = (!x. BAG_IN x b1 = BAG_IN x b2))
2567Proof
2568 SIMP_TAC std_ss [BAG_EXTENSION, BAG_ALL_DISTINCT_BAG_INN] THEN
2569 SIMP_TAC (std_ss++EQUIV_EXTRACT_ss) []
2570QED
2571
2572Theorem BAG_ALL_DISTINCT_SUB_BAG:
2573 !s t. s <= t /\ BAG_ALL_DISTINCT t ==> BAG_ALL_DISTINCT s
2574Proof
2575 rw[BAG_ALL_DISTINCT,SUB_BAG,BAG_INN] >>
2576 CCONTR_TAC >> `s e >= 2` by fs[] >>
2577 metis_tac[DECIDE “y >= 2 ==> ~(y <= 1)”]
2578QED
2579
2580Theorem BAG_DISJOINT_SUB_BAG:
2581 !b1 b2 b3. b1 <= b2 /\ BAG_DISJOINT b2 b3 ==> BAG_DISJOINT b1 b3
2582Proof
2583 rw [BAG_DISJOINT_BAG_IN] \\ metis_tac [SUB_BAG, BAG_IN]
2584QED
2585
2586Theorem BAG_DISJOINT_SYM:
2587 !b1 b2. BAG_DISJOINT b1 b2 <=> BAG_DISJOINT b2 b1
2588Proof simp [BAG_DISJOINT, DISJOINT_SYM]
2589QED
2590
2591Theorem MONOID_BAG_UNION_EMPTY_BAG: MONOID $+ {||}
2592Proof simp [MONOID_DEF, RIGHT_ID_DEF, LEFT_ID_DEF, ASSOC_DEF, ASSOC_BAG_UNION]
2593QED
2594
2595Theorem BAG_DISJOINT_FOLDR_BAG_UNION:
2596 !ls b0 b1.
2597 BAG_DISJOINT b1 (FOLDR BAG_UNION b0 ls) <=> EVERY (BAG_DISJOINT b1) (b0::ls)
2598Proof Induct \\ rw[] \\ metis_tac[]
2599QED
2600
2601Theorem NOT_BAG_IN:
2602 !b x. (b x = 0) = ~BAG_IN x b
2603Proof
2604 RW_TAC arith_ss [EQ_IMP_THM] THENL
2605 [STRIP_TAC THEN
2606 `?b'. b = BAG_INSERT x b'` by METIS_TAC[BAG_DECOMPOSE] THEN
2607 RW_TAC arith_ss [] THEN FULL_SIMP_TAC arith_ss [BAG_INSERT],
2608 FULL_SIMP_TAC arith_ss [BAG_IN,BAG_INN]]
2609QED
2610
2611Theorem BAG_UNION_EQ_LEFT:
2612 !b c d. (BAG_UNION b c = BAG_UNION b d) ==> (c=d)
2613Proof
2614 RW_TAC arith_ss [BAG_UNION,FUN_EQ_THM]
2615QED
2616
2617Theorem lem[local]:
2618 !b. FINITE_BAG b ==> !x a. BAG_IN x b ==> divides x (BAG_GEN_PROD b a)
2619Proof
2620 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN
2621 RW_TAC arith_ss [NOT_IN_EMPTY_BAG,BAG_IN_BAG_INSERT] THENL
2622 [RW_TAC arith_ss [BAG_GEN_PROD_REC] THEN
2623 METIS_TAC[DIVIDES_REFL,DIVIDES_MULT],
2624 `divides x (BAG_GEN_PROD b a)` by METIS_TAC[] THEN
2625 RW_TAC arith_ss [BAG_GEN_PROD_REC] THEN
2626 METIS_TAC[DIVIDES_MULT,MULT_SYM]]
2627QED
2628
2629Theorem BAG_IN_DIVIDES:
2630 !b x a. FINITE_BAG b /\ BAG_IN x b ==> divides x (BAG_GEN_PROD b a)
2631Proof
2632 METIS_TAC [lem]
2633QED
2634
2635Theorem BAG_GEN_PROD_UNION_LEM:
2636 !b1. FINITE_BAG b1 ==>
2637 !b2 a b. FINITE_BAG b2 ==>
2638 (BAG_GEN_PROD (BAG_UNION b1 b2) (a * b) =
2639 BAG_GEN_PROD b1 a * BAG_GEN_PROD b2 b)
2640Proof
2641 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN CONJ_TAC THENL
2642 [RW_TAC arith_ss [BAG_GEN_PROD_EMPTY,BAG_UNION_EMPTY] THEN
2643 Q.ID_SPEC_TAC `b` THEN Q.ID_SPEC_TAC `a` THEN
2644 POP_ASSUM MP_TAC THEN Q.ID_SPEC_TAC `b2` THEN
2645 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN
2646 RW_TAC arith_ss [BAG_GEN_PROD_EMPTY,BAG_UNION_EMPTY] THEN
2647 RW_TAC arith_ss [BAG_GEN_PROD_REC],
2648 REPEAT STRIP_TAC THEN
2649 RW_TAC arith_ss [BAG_GEN_PROD_REC,BAG_UNION_INSERT] THEN
2650 `FINITE_BAG (BAG_UNION b1 b2)` by METIS_TAC [FINITE_BAG_UNION] THEN
2651 RW_TAC arith_ss [BAG_GEN_PROD_REC] THEN
2652 METIS_TAC [MULT_ASSOC]]
2653QED
2654
2655Theorem BAG_GEN_PROD_UNION:
2656 !b1 b2. FINITE_BAG b1 /\ FINITE_BAG b2 ==>
2657 (BAG_GEN_PROD (BAG_UNION b1 b2) 1 =
2658 BAG_GEN_PROD b1 1 * BAG_GEN_PROD b2 1)
2659Proof
2660 METIS_TAC [BAG_GEN_PROD_UNION_LEM, ARITH `1 * 1 = 1`]
2661QED
2662
2663Theorem BAG_GEN_PROD_EQ_0:
2664 !b. FINITE_BAG b ==>
2665 !e. BAG_GEN_PROD b e = 0 <=> BAG_IN 0 b \/ e = 0
2666Proof
2667 ho_match_mp_tac STRONG_FINITE_BAG_INDUCT
2668 \\ rw[BAG_GEN_PROD_REC]
2669 >- fs[BAG_GEN_PROD_def]
2670 \\ metis_tac[]
2671QED
2672
2673(* BIG_BAG_UNION: the union of all bags in a finite set *)
2674
2675Definition BIG_BAG_UNION_def:
2676 BIG_BAG_UNION sob = \x. SIGMA (\b. b x) sob
2677End
2678
2679Theorem BIG_BAG_UNION_EMPTY[simp]:
2680 BIG_BAG_UNION {} = {||}
2681Proof
2682SRW_TAC [][BIG_BAG_UNION_def,SUM_IMAGE_THM,EMPTY_BAG,FUN_EQ_THM]
2683QED
2684
2685Theorem BIG_BAG_UNION_INSERT:
2686 FINITE sob ==>
2687 (BIG_BAG_UNION (b INSERT sob) = b + BIG_BAG_UNION (sob DELETE b))
2688Proof
2689SRW_TAC [][BIG_BAG_UNION_def,SUM_IMAGE_THM,BAG_UNION,FUN_EQ_THM]
2690QED
2691
2692Theorem BIG_BAG_UNION_DELETE:
2693 FINITE sob ==>
2694(BIG_BAG_UNION (sob DELETE b)
2695 = if b IN sob then BAG_DIFF (BIG_BAG_UNION sob) b else BIG_BAG_UNION sob)
2696Proof
2697SRW_TAC [][BIG_BAG_UNION_def,SUM_IMAGE_THM,
2698 SUM_IMAGE_DELETE,BAG_UNION,BAG_DIFF,FUN_EQ_THM] THEN
2699FULL_SIMP_TAC (srw_ss()) [DELETE_NON_ELEMENT]
2700QED
2701
2702Theorem BIG_BAG_UNION_ITSET_BAG_UNION:
2703 !sob. FINITE sob ==> (BIG_BAG_UNION sob = ITSET BAG_UNION sob {||})
2704Proof
2705HO_MATCH_MP_TAC FINITE_INDUCT THEN
2706SRW_TAC [][ITSET_EMPTY] THEN
2707(COMMUTING_ITSET_RECURSES
2708 |> Q.ISPECL_THEN [`BAG_UNION`,`e`,`sob`,`{||}`] MP_TAC) THEN
2709FULL_SIMP_TAC (srw_ss()) [DELETE_NON_ELEMENT] THEN
2710SRW_TAC [][BIG_BAG_UNION_INSERT] THEN
2711FIRST_X_ASSUM (MATCH_MP_TAC o GSYM) THEN
2712METIS_TAC [COMM_BAG_UNION,ASSOC_BAG_UNION]
2713QED
2714
2715Theorem FINITE_BIG_BAG_UNION:
2716 !sob. FINITE sob /\ (!b. b IN sob ==> FINITE_BAG b) ==> FINITE_BAG
2717(BIG_BAG_UNION sob)
2718Proof
2719SIMP_TAC bool_ss [GSYM AND_IMP_INTRO] THEN
2720 HO_MATCH_MP_TAC FINITE_INDUCT THEN
2721 SRW_TAC [][BIG_BAG_UNION_INSERT] THEN
2722 FULL_SIMP_TAC (srw_ss()) [DELETE_NON_ELEMENT]
2723QED
2724
2725Theorem BAG_IN_BIG_BAG_UNION[simp]:
2726 FINITE P ==> (e <: BIG_BAG_UNION P <=> ?b. e <: b /\ b IN P)
2727Proof
2728SRW_TAC [][BIG_BAG_UNION_def,BAG_IN,BAG_INN,EQ_IMP_THM] THEN1 (
2729 SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN
2730 (SUM_IMAGE_upper_bound
2731 |> Q.GEN `f`
2732 |> Q.ISPEC_THEN `\b:'a bag. b e` (Q.ISPEC_THEN `P` MP_TAC)) THEN
2733 SRW_TAC [][] THEN
2734 Q.EXISTS_TAC `0` THEN
2735 SRW_TAC [ARITH_ss][] THEN
2736 FIRST_X_ASSUM (Q.SPEC_THEN `x` MP_TAC) THEN
2737 SRW_TAC [ARITH_ss][] ) THEN
2738FULL_SIMP_TAC (srw_ss()) [arithmeticTheory.GREATER_EQ] THEN
2739`1 <= SIGMA (\b. b e) {b}` by SRW_TAC [][SUM_IMAGE_THM] THEN
2740MATCH_MP_TAC arithmeticTheory.LESS_EQ_TRANS THEN
2741Q.EXISTS_TAC `SIGMA (\b.b e) {b}` THEN
2742SRW_TAC [][] THEN
2743MATCH_MP_TAC SUM_IMAGE_SUBSET_LE THEN
2744SRW_TAC [][]
2745QED
2746
2747Theorem BIG_BAG_UNION_EQ_EMPTY_BAG:
2748 !sob. FINITE sob ==>
2749((BIG_BAG_UNION sob = {||}) <=> (!b. b IN sob ==> (b = {||})))
2750Proof
2751HO_MATCH_MP_TAC FINITE_INDUCT THEN
2752SRW_TAC [][BIG_BAG_UNION_INSERT] THEN
2753FULL_SIMP_TAC (srw_ss()) [DELETE_NON_ELEMENT] THEN
2754PROVE_TAC []
2755QED
2756
2757Theorem BIG_BAG_UNION_UNION:
2758 FINITE s1 /\ FINITE s2 ==>
2759(BIG_BAG_UNION (s1 UNION s2)
2760 = BIG_BAG_UNION s1 + BIG_BAG_UNION s2 - BIG_BAG_UNION (s1 INTER s2))
2761Proof
2762SRW_TAC [][BIG_BAG_UNION_def,SUM_IMAGE_UNION,FUN_EQ_THM,BAG_UNION,BAG_DIFF]
2763QED
2764
2765Theorem BIG_BAG_UNION_EQ_ELEMENT:
2766 FINITE sob /\ b IN sob ==>
2767 (BIG_BAG_UNION sob = b <=> !b'. b' IN sob ==> b' = b \/ b' = {||})
2768Proof
2769 Cases_on ‘sob’ >>
2770 simp[BIG_BAG_UNION_def, SUM_IMAGE_THM, DELETE_NON_ELEMENT_RWT,
2771 DISJ_IMP_THM, FORALL_AND_THM] >> rw[]
2772 >- (simp[SimpLHS, FUN_EQ_THM, SUM_IMAGE_ZERO] >>
2773 rename [‘b NOTIN sob’] >>
2774 ‘!x. x IN sob ==> x <> b’ by metis_tac[] >> simp[] >>
2775 simp[FUN_EQ_THM, EMPTY_BAG] >> metis_tac[]) >>
2776 rename [‘b NOTIN s’, ‘a IN s’, ‘_ = a’] >>
2777 ‘a <> b’ by metis_tac[] >> simp[] >>
2778 ‘?s0. s = a INSERT s0 /\ a NOTIN s0’ by metis_tac[DECOMPOSITION] >>
2779 fs[SUM_IMAGE_THM, DELETE_NON_ELEMENT_RWT] >>
2780 simp[SimpLHS, FUN_EQ_THM] >> simp[DISJ_IMP_THM, SUM_IMAGE_ZERO] >>
2781 ‘!c. c IN s0 ==> c <> a’ by metis_tac[] >> simp[] >>
2782 simp[EMPTY_BAG, FUN_EQ_THM] >> metis_tac[]
2783QED
2784
2785(* ----------------------------------------------------------------------
2786 Multiset ordering
2787
2788 Taken from Isabelle development of same.
2789 ---------------------------------------------------------------------- *)
2790
2791(* The 1 is from the fact that is one step of the relation, other uses
2792 might want to take the transitive closure of this (overloaded below). *)
2793Definition mlt1_def[nocompute]:
2794 mlt1 r b1 b2 <=> FINITE_BAG b1 /\ FINITE_BAG b2 /\
2795 ?e rep res. (b1 = rep + res) /\ (b2 = res + {|e|}) /\
2796 !e'. BAG_IN e' rep ==> r e' e
2797End
2798
2799Overload mlt = ``\R. TC (mlt1 R)``
2800
2801Theorem BAG_NOT_LESS_EMPTY[simp]:
2802 ~mlt1 r b {||}
2803Proof
2804 SRW_TAC [][mlt1_def]
2805QED
2806
2807Theorem NOT_mlt_EMPTY[simp]:
2808 ~mlt R b {||}
2809Proof
2810 simp[Once relationTheory.TC_CASES2]
2811QED
2812
2813Theorem BAG_LESS_ADD:
2814 mlt1 r N (M0 + {|a|}) ==>
2815 (?M. mlt1 r M M0 /\ (N = M + {|a|})) \/
2816 (?KK. (!b. BAG_IN b KK ==> r b a) /\ (N = M0 + KK))
2817Proof
2818 SRW_TAC [][mlt1_def] THEN
2819 FULL_SIMP_TAC (srw_ss()) [Once add_eq_conv_ex] THENL [
2820 DISJ2_TAC THEN Q.EXISTS_TAC `rep` THEN
2821 METIS_TAC [COMM_BAG_UNION],
2822
2823 SRW_TAC [DNF_ss][] THEN FULL_SIMP_TAC (srw_ss()) [] THEN
2824 METIS_TAC [ASSOC_BAG_UNION]
2825 ]
2826QED
2827
2828Theorem bag_insert_union[local]:
2829 BAG_INSERT e b = b + {|e|}
2830Proof
2831 SRW_TAC [][FUN_EQ_THM, BAG_UNION, BAG_INSERT, EMPTY_BAG] THEN
2832 SRW_TAC [bossLib.ARITH_ss][]
2833QED
2834
2835Theorem tedious_reasoning[local]:
2836 !M0 a.
2837 WFP (mlt1 R) M0 /\
2838 (!b. R b a ==> !M. WFP (mlt1 R) M ==> WFP (mlt1 R) (M + {|b|})) /\
2839 (!M. mlt1 R M M0 ==> WFP (mlt1 R) (M + {|a|}))
2840 ==>
2841 WFP (mlt1 R) (M0 + {|a|})
2842Proof
2843 REPEAT STRIP_TAC THEN MATCH_MP_TAC relationTheory.WFP_RULES THEN
2844 REPEAT STRIP_TAC THEN
2845 `FINITE_BAG y` by FULL_SIMP_TAC (srw_ss()) [mlt1_def] THEN
2846 FIRST_X_ASSUM (STRIP_ASSUME_TAC o MATCH_MP BAG_LESS_ADD)
2847 THEN1 METIS_TAC [] THEN
2848 SRW_TAC [][] THEN
2849 POP_ASSUM MP_TAC THEN
2850 FULL_SIMP_TAC (srw_ss()) [] THEN
2851 Q.PAT_X_ASSUM `FINITE_BAG KK` MP_TAC THEN
2852 Q.ID_SPEC_TAC `KK` THEN
2853 HO_MATCH_MP_TAC FINITE_BAG_INDUCT THEN SRW_TAC [][] THEN
2854 `R e a` by SRW_TAC [][] THEN
2855 `!M. WFP (mlt1 R) M ==> WFP (mlt1 R) (M + {|e|})` by METIS_TAC [] THEN
2856 `WFP (mlt1 R) (M0 + KK)` by METIS_TAC [] THEN
2857 `WFP (mlt1 R) (M0 + KK + {|e|})` by METIS_TAC [] THEN
2858 Q_TAC SUFF_TAC `M0 + BAG_INSERT e KK = M0 + KK + {|e|}`
2859 THEN1 METIS_TAC [] THEN
2860 SRW_TAC [][BAG_UNION, FUN_EQ_THM, BAG_INSERT, EMPTY_BAG] THEN
2861 SRW_TAC [bossLib.ARITH_ss][]
2862QED
2863
2864
2865Theorem mlt1_all_accessible:
2866 WF R ==> !M. WFP (mlt1 R) M
2867Proof
2868 STRIP_TAC THEN Q.X_GEN_TAC `M` THEN Cases_on `FINITE_BAG M` THENL [
2869 POP_ASSUM MP_TAC THEN Q.ID_SPEC_TAC `M` THEN
2870 HO_MATCH_MP_TAC FINITE_BAG_INDUCT THEN
2871 CONJ_TAC THEN1
2872 (MATCH_MP_TAC relationTheory.WFP_RULES THEN SRW_TAC [][]) THEN
2873 Q_TAC SUFF_TAC
2874 `!a M. WFP (mlt1 R) M ==> WFP (mlt1 R) (BAG_INSERT a M)`
2875 THEN1 METIS_TAC [] THEN
2876 FIRST_X_ASSUM
2877 (HO_MATCH_MP_TAC o MATCH_MP relationTheory.WF_INDUCTION_THM) THEN
2878 Q.X_GEN_TAC `a` THEN
2879 DISCH_THEN (ASSUME_TAC o CONV_RULE (RENAME_VARS_CONV ["b"])) THEN
2880 HO_MATCH_MP_TAC relationTheory.WFP_STRONG_INDUCT THEN
2881 ASSUME_TAC tedious_reasoning THEN
2882 FULL_SIMP_TAC (srw_ss()) [GSYM bag_insert_union],
2883
2884 MATCH_MP_TAC relationTheory.WFP_RULES THEN
2885 SRW_TAC [][mlt1_def]
2886 ]
2887QED
2888
2889Theorem WF_mlt1:
2890 WF R ==> WF (mlt1 R)
2891Proof
2892 METIS_TAC [relationTheory.WF_EQ_WFP, mlt1_all_accessible]
2893QED
2894
2895Theorem TC_mlt1_FINITE_BAG:
2896 !b1 b2. TC (mlt1 R) b1 b2 ==> FINITE_BAG b1 /\ FINITE_BAG b2
2897Proof
2898 HO_MATCH_MP_TAC relationTheory.TC_INDUCT THEN SRW_TAC [][] THEN
2899 FULL_SIMP_TAC (srw_ss()) [mlt1_def]
2900QED
2901
2902Theorem TC_mlt1_UNION2_I:
2903 !b2 b1. FINITE_BAG b2 /\ FINITE_BAG b1 /\ b2 <> {||} ==>
2904 (mlt1 R)^+ b1 (b1 + b2)
2905Proof
2906 Q_TAC SUFF_TAC
2907 `!b2. FINITE_BAG b2 ==> !b1. FINITE_BAG b1 /\ b2 <> {||} ==>
2908 (mlt1 R)^+ b1 (b1 + b2)` THEN1 METIS_TAC [] THEN
2909 HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN SRW_TAC [][] THEN
2910 Cases_on `b2 = {||}` THENL [
2911 SRW_TAC [][] THEN
2912 MATCH_MP_TAC relationTheory.TC_SUBSET THEN
2913 SRW_TAC [][mlt1_def] THEN METIS_TAC [BAG_UNION_EMPTY, NOT_IN_EMPTY_BAG],
2914
2915 `(mlt1 R)^+ b1 (b1 + b2)` by METIS_TAC [] THEN
2916 MATCH_MP_TAC (CONJUNCT2 (SPEC_ALL relationTheory.TC_RULES)) THEN
2917 Q.EXISTS_TAC `b1 + b2` THEN SRW_TAC [][] THEN
2918 MATCH_MP_TAC relationTheory.TC_SUBSET THEN
2919 SRW_TAC [][mlt1_def] THEN
2920 MAP_EVERY Q.EXISTS_TAC [`e`, `{||}`, `b1 + b2`] THEN SRW_TAC [][] THEN
2921 METIS_TAC [EL_BAG, BAG_INSERT_UNION, COMM_BAG_UNION, ASSOC_BAG_UNION]
2922 ]
2923QED
2924
2925Theorem TC_mlt1_UNION1_I:
2926 !b2 b1. FINITE_BAG b2 /\ FINITE_BAG b1 /\ b1 <> {||} ==>
2927 (mlt1 R)^+ b2 (b1 + b2)
2928Proof
2929 METIS_TAC [COMM_BAG_UNION,TC_mlt1_UNION2_I]
2930QED
2931
2932Theorem mlt_NOT_REFL[simp]:
2933 WF R ==> ~(mlt R a a)
2934Proof
2935 metis_tac[WF_mlt1, relationTheory.WF_TC_EQN,
2936 relationTheory.WF_NOT_REFL]
2937QED
2938
2939Theorem mlt_INSERT_CANCEL_I:
2940 !a b. mlt R a b ==> mlt R (BAG_INSERT e a) (BAG_INSERT e b)
2941Proof
2942 ho_match_mp_tac relationTheory.TC_lifts_monotonicities >>
2943 simp[mlt1_def] >> rw[] >>
2944 map_every qexists_tac [`e'`, `rep`, `BAG_INSERT e res`] >>
2945 simp[BAG_UNION_INSERT]
2946QED
2947
2948Theorem mlt1_INSERT_CANCEL:
2949 WF R ==> (mlt1 R (BAG_INSERT e a) (BAG_INSERT e b) <=> mlt1 R a b)
2950Proof
2951 simp[mlt1_def, EQ_IMP_THM] >> rpt strip_tac >> dsimp[]
2952 >- (Cases_on `e = e'`
2953 >- (fs[BAG_UNION_INSERT] >>
2954 `~(BAG_IN e' rep)` by metis_tac [relationTheory.WF_NOT_REFL] >>
2955 `BAG_IN e' res` by metis_tac[BAG_IN_BAG_UNION, BAG_IN_BAG_INSERT] >>
2956 `?b0. res = BAG_INSERT e' b0` by metis_tac[BAG_DECOMPOSE] >>
2957 fs[BAG_UNION_INSERT] >> metis_tac[]) >>
2958 `BAG_IN e res` by metis_tac[BAG_IN_BAG_UNION, BAG_IN_BAG_INSERT,
2959 NOT_IN_EMPTY_BAG] >>
2960 `?b0. res = BAG_INSERT e b0` by metis_tac [BAG_DECOMPOSE] >>
2961 fs[BAG_UNION_INSERT] >> fs[Once BAG_INSERT_commutes] >>
2962 metis_tac[]) >>
2963 map_every qexists_tac [`e'`, `rep`, `BAG_INSERT e res`] >>
2964 simp[BAG_UNION_INSERT]
2965QED
2966
2967(* dominates R b1 b2 should be read as "b2 dominates b1 wrt relation R" *)
2968Definition dominates_def:
2969 dominates R s1 s2 = !x. x IN s1 ==> ?y. y IN s2 /\ R x y
2970End
2971
2972Overload bdominates =
2973 ``\R b1 b2. dominates R (SET_OF_BAG b1) (SET_OF_BAG b2)``
2974
2975Theorem dominates_EMPTY[simp]:
2976 dominates R {} b
2977Proof
2978 simp[dominates_def]
2979QED
2980
2981Theorem cycles_exist[local]:
2982 !X. FINITE X ==> (!x. x IN X ==> f x IN X) /\ X <> {}
2983 ==>
2984 ?x n. 0 < n /\ x IN X /\ (FUNPOW f n x = x)
2985Proof
2986 strip_tac >> completeInduct_on `CARD X` >>
2987 full_simp_tac (srw_ss() ++ boolSimps.DNF_ss) [AND_IMP_INTRO] >> rw[] >>
2988 `?e X0. (X = e INSERT X0) /\ e NOTIN X0` by metis_tac[SET_CASES] >>
2989 rw[] >> fs[] >>
2990 Cases_on `?m. FUNPOW f m (f e) = e`
2991 >- (pop_assum strip_assume_tac >>
2992 map_every qexists_tac [`e`, `SUC m`] >> simp[FUNPOW]) >>
2993 fs[] >>
2994 `f e <> e` by (pop_assum (qspec_then `0` mp_tac) >> simp[]) >>
2995 `!n. FUNPOW f n (f e) IN X0`
2996 by (Induct >> simp[] >- metis_tac[] >> metis_tac[FUNPOW_SUC]) >>
2997 qabbrev_tac `XX = { FUNPOW f n (f e) | n | T }` >>
2998 `XX SUBSET X0` by dsimp[Abbr`XX`, SUBSET_DEF] >>
2999 `FINITE XX /\ CARD XX <= CARD X0`
3000 by metis_tac[SUBSET_FINITE, CARD_SUBSET] >>
3001 `CARD XX < SUC (CARD X0)` by decide_tac >>
3002 `!x. x IN XX ==> f x IN XX`
3003 by (dsimp[Abbr`XX`] >> qx_gen_tac `p` >> qexists_tac `SUC p` >>
3004 simp[FUNPOW_SUC]) >>
3005 `XX <> {}` by simp[Abbr`XX`, EXTENSION] >>
3006 metis_tac[SUBSET_DEF]
3007QED
3008
3009Theorem dominates_SUBSET:
3010 transitive R /\ FINITE Y /\ dominates R Y X /\ X SUBSET Y /\ X <> {} ==>
3011 ?x. x IN X /\ R x x
3012Proof
3013 simp[dominates_def] >> rpt strip_tac >>
3014 `?f. !x. x IN Y ==> f x IN X /\ R x (f x)` by metis_tac[] >>
3015 `!x. x IN Y ==> f x IN Y` by metis_tac[SUBSET_DEF] >>
3016 `Y <> {}` by (strip_tac >> fs[]) >>
3017 qspec_then `Y` mp_tac cycles_exist >> simp[] >>
3018 strip_tac >> qexists_tac `x` >>
3019 `!p. 0 < p ==> FUNPOW f p x IN X /\ R x (FUNPOW f p x)`
3020 by (Induct >> simp[FUNPOW_SUC] >>
3021 Cases_on `p` >> fs[FUNPOW_SUC] >>
3022 metis_tac[SUBSET_DEF, relationTheory.transitive_def]) >>
3023 metis_tac[]
3024QED
3025
3026(* the transitivity requirement can be seen in the following example.
3027 Imagine R is (\m n. n = SUC m), whose transitive closure is <.
3028 Then we have
3029 mlt R {|0|} {|2|}
3030 because the first step removes 2 and replaces it with a 1. The next step
3031 then replaces the 1 with a 0.
3032
3033 But the alternative "definition" of mlt below is not satisfied because x has to
3034 be {|2|} and y has to be {|0|}. But y is not dominated by x, because there is
3035 nothing in x that is R-bigger than 0.
3036*)
3037Theorem mlt_dominates_thm1:
3038 transitive R ==>
3039 !b1 b2. mlt R b1 b2 <=>
3040 FINITE_BAG b1 /\ FINITE_BAG b2 /\
3041 ?x y. x <> {||} /\ SUB_BAG x b2 /\
3042 (b1 = (b2 - x) + y) /\
3043 bdominates R y x
3044Proof
3045 simp[EQ_IMP_THM, FORALL_AND_THM] >> strip_tac >> conj_tac
3046 >- (ho_match_mp_tac relationTheory.TC_STRONG_INDUCT_LEFT1 >>
3047 conj_tac
3048 >- (simp[mlt1_def, dominates_def] >> map_every qx_gen_tac [`b1`, `b2`] >>
3049 strip_tac >> map_every qexists_tac [`{|e|}`, `rep`] >>
3050 simp[COMM_BAG_UNION]) >>
3051 rpt strip_tac >>
3052 qmatch_assum_rename_tac `mlt1 R B0 B1` >>
3053 qmatch_assum_rename_tac `mlt R B1 B2` >>
3054 fs[mlt1_def] >>
3055 qmatch_assum_rename_tac `!e'. BAG_IN e' Rep ==> R e' E` >>
3056 qmatch_assum_rename_tac `(B2 - X) + Y = Res + {|E|}` >>
3057 Cases_on `BAG_IN E Y`
3058 >- (map_every qexists_tac [`X`, `Y - {| E |} + Rep`] >>
3059 simp[] >> reverse conj_tac
3060 >- (fs[dominates_def] >>
3061 metis_tac [BAG_IN_DIFF_E, relationTheory.transitive_def]) >>
3062 pop_assum mp_tac >>
3063 qpat_x_assum `B2 - X + Y = Res + {|E|}` mp_tac >>
3064 simp[BAG_DIFF, FUN_EQ_THM, BAG_UNION, BAG_INSERT, EMPTY_BAG,
3065 BAG_IN, BAG_INN] >>
3066 disch_then (fn allth => disch_then
3067 (fn YE => qx_gen_tac `ee` >>
3068 qspec_then `ee` mp_tac allth >>
3069 mp_tac YE)) >>
3070 COND_CASES_TAC >> simp[]) >>
3071 map_every qexists_tac [`BAG_INSERT E X`, `Y + Rep`] >> simp[] >>
3072 reverse (rpt conj_tac)
3073 >- (fs[dominates_def] >> metis_tac[])
3074 >- (pop_assum mp_tac >>
3075 qpat_x_assum `B2 - X + Y = Res + {|E|}` mp_tac >>
3076 simp[BAG_DIFF, FUN_EQ_THM, BAG_UNION, BAG_INSERT, EMPTY_BAG,
3077 BAG_IN, BAG_INN] >>
3078 disch_then (fn allth => disch_then
3079 (fn YE => qx_gen_tac `ee` >>
3080 qspec_then `ee` mp_tac allth >>
3081 mp_tac YE)) >>
3082 COND_CASES_TAC >> simp[]) >>
3083 pop_assum mp_tac >>
3084 qpat_x_assum `X <= B2` mp_tac >>
3085 qpat_x_assum `B2 - X + Y = Res + {|E|}` mp_tac >>
3086 simp[BAG_DIFF, FUN_EQ_THM, BAG_UNION, BAG_INSERT, EMPTY_BAG,
3087 BAG_IN, BAG_INN, SUB_BAG_LEQ] >>
3088 disch_then
3089 (fn allth1 => disch_then
3090 (fn allth2 => disch_then
3091 (fn YE => qx_gen_tac `ee` >>
3092 qspec_then `ee` mp_tac allth1 >>
3093 qspec_then `ee` mp_tac allth2 >>
3094 mp_tac YE))) >>
3095 COND_CASES_TAC >> simp[]) >>
3096 rpt strip_tac >> rw[] >>
3097 `FINITE_BAG x` by metis_tac[FINITE_SUB_BAG] >>
3098 fs[] >> map_every (C qpat_x_assum mp_tac) [
3099 `FINITE_BAG b2`, `FINITE_BAG y`, `bdominates R y x`,
3100 `x <= b2`, `x <> {||}`] >>
3101 map_every qid_spec_tac [`b2`, `y`] >> pop_assum mp_tac >>
3102 pop_assum kall_tac >> qid_spec_tac `x` >>
3103 ho_match_mp_tac STRONG_FINITE_BAG_INDUCT >> simp[] >> rpt strip_tac >>
3104 Cases_on `x = {||}`
3105 >- (rw[] >> fs[dominates_def] >>
3106 match_mp_tac relationTheory.TC_SUBSET >>
3107 simp[mlt1_def, FINITE_BAG_DIFF] >>
3108 map_every qexists_tac [`e`, `y`, `b2 - {|e|}`] >>
3109 simp[COMM_BAG_UNION, SUB_BAG_DIFF_EQ]) >>
3110 match_mp_tac (relationTheory.TC_RULES |> SPEC_ALL |> CONJUNCT2) >>
3111 qexists_tac `b2 - {|e|} + BAG_FILTER (\x. R x e) y` >> reverse conj_tac
3112 >- (match_mp_tac relationTheory.TC_SUBSET >> simp[mlt1_def, FINITE_BAG_DIFF]>>
3113 map_every qexists_tac [`e`, `BAG_FILTER (\x. R x e) y`, `b2 - {|e|}`] >>
3114 simp[] >> simp[COMM_BAG_UNION] >> match_mp_tac SUB_BAG_DIFF_EQ >>
3115 simp[] >> metis_tac[SUB_BAG_BAG_IN]) >>
3116 `b2 - BAG_INSERT e x + y =
3117 b2 - {|e|} + BAG_FILTER (\x. R x e) y - x + BAG_FILTER (\x. ~R x e) y`
3118 by (qpat_x_assum `BAG_INSERT e x <= b2` mp_tac >>
3119 simp_tac bool_ss [FUN_EQ_THM, SUB_BAG_LEQ, BAG_DIFF, BAG_UNION,
3120 EMPTY_BAG, BAG_INSERT, BAG_FILTER_DEF] >> simp[] >>
3121 strip_tac >> qx_gen_tac `a` >> pop_assum (qspec_then `a` mp_tac) >>
3122 rpt COND_CASES_TAC >> simp[] >> fs[]) >>
3123 fs[AND_IMP_INTRO] >> first_x_assum match_mp_tac >> simp[FINITE_BAG_DIFF] >>
3124 conj_tac
3125 >- (fs[SUB_BAG_LEQ, BAG_INSERT, EMPTY_BAG, BAG_FILTER_DEF, BAG_DIFF,
3126 BAG_UNION] >> qx_gen_tac `a` >>
3127 first_x_assum (qspec_then `a` mp_tac) >>
3128 COND_CASES_TAC >> simp[] >> decide_tac) >>
3129 fs[dominates_def] >> metis_tac[]
3130QED
3131
3132Theorem dominates_DIFF:
3133 WF R /\ transitive R /\ dominates R x y /\ FINITE i /\
3134 i SUBSET x /\ i SUBSET y ==>
3135 dominates R (x DIFF i) (y DIFF i)
3136Proof
3137 map_every Cases_on [`WF R`, `transitive R`, `dominates R x y`, `FINITE i`] >>
3138 simp[] >>
3139 pop_assum mp_tac >> qid_spec_tac `i` >> Induct_on `FINITE i` >>
3140 simp[] >> qx_gen_tac `i` >> strip_tac >> qx_gen_tac `e` >> strip_tac >>
3141 strip_tac >> simp[dominates_def] >> fs[] >>
3142 qx_gen_tac `a` >> strip_tac >>
3143 `?b. b IN y /\ b NOTIN i /\ R a b` by (fs[dominates_def] >> metis_tac[]) >>
3144 Cases_on `b = e`
3145 >- (pop_assum SUBST_ALL_TAC >>
3146 `?c. c IN y /\ c NOTIN i /\ R e c`
3147 by (fs[dominates_def] >> metis_tac[]) >>
3148 `c <> e` by metis_tac[relationTheory.WF_NOT_REFL] >>
3149 metis_tac[relationTheory.transitive_def]) >>
3150 metis_tac[]
3151QED
3152
3153Theorem BAG_INSERT_SUB_BAG_E:
3154 BAG_INSERT e b <= c ==> BAG_IN e c /\ b <= c
3155Proof
3156 simp[SUB_BAG_LEQ, BAG_INSERT, BAG_IN, BAG_INN] >> strip_tac >> conj_tac
3157 >- (first_x_assum (qspec_then `e` mp_tac) >> simp[]) >>
3158 qx_gen_tac `a` >> first_x_assum (qspec_then `a` mp_tac) >> rw[] >> simp[]
3159QED
3160
3161Theorem bdominates_BAG_DIFF:
3162 WF R /\ transitive R /\ bdominates R x y /\
3163 FINITE_BAG i /\ i <= x /\ i <= y ==>
3164 bdominates R (x - i) (y - i)
3165Proof
3166 map_every Cases_on [`WF R`, `transitive R`, `bdominates R x y`,
3167 `FINITE_BAG i`] >>
3168 simp[] >>
3169 pop_assum mp_tac >> qid_spec_tac `i` >> Induct_on `FINITE_BAG i` >>
3170 simp[] >> qx_gen_tac `i` >> strip_tac >> qx_gen_tac `e` >> strip_tac >>
3171 imp_res_tac BAG_INSERT_SUB_BAG_E >> fs[] >> simp[dominates_def] >>
3172 qx_gen_tac `a` >> strip_tac >>
3173 `BAG_IN a (x - i)`
3174 by (pop_assum mp_tac >> simp[BAG_IN, BAG_INN, BAG_INSERT, BAG_DIFF] >>
3175 rw[] >> simp[]) >>
3176 `?b. BAG_IN b (y - i) /\ R a b` by metis_tac[dominates_def, IN_SET_OF_BAG] >>
3177 reverse (Cases_on `b = e`)
3178 >- (qexists_tac `b` >>
3179 `y - BAG_INSERT e i = y - i - {| e |}`
3180 by (simp[FUN_EQ_THM, BAG_DIFF, BAG_INSERT, EMPTY_BAG] >> rw[] >>
3181 simp[]) >>
3182 pop_assum SUBST_ALL_TAC >> simp[] >>
3183 match_mp_tac BAG_IN_DIFF_I >> simp[]) >>
3184 pop_assum SUBST_ALL_TAC >>
3185 `BAG_IN e (x - i)`
3186 by (qpat_x_assum `BAG_INSERT e i <= x` mp_tac >>
3187 simp[BAG_DIFF, BAG_INSERT, SUB_BAG_LEQ, BAG_IN,
3188 BAG_INN] >> disch_then (qspec_then `e` mp_tac) >>
3189 simp[]) >>
3190 `?c. BAG_IN c (y - i) /\ R e c` by metis_tac[dominates_def, IN_SET_OF_BAG] >>
3191 `c <> e` by metis_tac[relationTheory.WF_NOT_REFL] >>
3192 `R a c` by metis_tac[relationTheory.transitive_def] >>
3193 qexists_tac `c` >>
3194 `y - BAG_INSERT e i = y - i - {| e |}`
3195 by (simp[FUN_EQ_THM, BAG_DIFF, BAG_INSERT, EMPTY_BAG] >> rw[] >>
3196 simp[]) >>
3197 pop_assum SUBST_ALL_TAC >> simp[] >>
3198 match_mp_tac BAG_IN_DIFF_I >> simp[]
3199QED
3200
3201Theorem BAG_INTER_SUB_BAG[simp]:
3202 SUB_BAG (BAG_INTER b1 b2) b1 /\ SUB_BAG (BAG_INTER b1 b2) b2
3203Proof
3204 simp[BAG_INTER, SUB_BAG_LEQ]
3205QED
3206
3207Theorem BAG_INTER_FINITE:
3208 FINITE_BAG b1 \/ FINITE_BAG b2 ==> FINITE_BAG (BAG_INTER b1 b2)
3209Proof
3210 metis_tac[FINITE_SUB_BAG, BAG_INTER_SUB_BAG]
3211QED
3212
3213Theorem mlt_dominates_thm2:
3214 WF R /\ transitive R ==>
3215 !b1 b2. mlt R b1 b2 <=>
3216 FINITE_BAG b1 /\ FINITE_BAG b2 /\
3217 ?x y. x <> {||} /\ SUB_BAG x b2 /\
3218 BAG_DISJOINT x y /\
3219 (b1 = (b2 - x) + y) /\
3220 bdominates R y x
3221Proof
3222 rpt strip_tac >> simp[mlt_dominates_thm1] >>
3223 map_every Cases_on [`FINITE_BAG b1`, `FINITE_BAG b2`] >> simp[] >>
3224 reverse eq_tac >> strip_tac >- metis_tac[] >>
3225 qabbrev_tac `II = BAG_INTER x y` >>
3226 map_every qexists_tac [`x - II`, `y - II`] >>
3227 `x - II <= b2` by simp[SUB_BAG_DIFF] >>
3228 `II <= x /\ II <= y` by simp[Abbr`II`, BAG_INTER, SUB_BAG_LEQ] >>
3229 simp[] >>
3230 `~(x <= II)`
3231 by (strip_tac >>
3232 `x = II` by simp[SUB_BAG_ANTISYM] >> rw[] >>
3233 qspecl_then [`R`, `SET_OF_BAG II`, `SET_OF_BAG y`] mp_tac
3234 (Q.GENL [`R`, `X`, `Y`] dominates_SUBSET) >> simp[] >>
3235 fs[SUB_BAG_SET] >> qx_gen_tac `e` >> Cases_on `BAG_IN e II` >>
3236 simp[] >> metis_tac[relationTheory.WF_NOT_REFL]) >>
3237 simp[] >>
3238 `BAG_DISJOINT (x - II) (y - II)`
3239 by (simp[BAG_DISJOINT, DISJOINT_DEF, EXTENSION] >>
3240 qx_gen_tac `e` >> Cases_on `BAG_IN e (x - II)` >> simp[] >>
3241 pop_assum mp_tac >>
3242 simp[Abbr`II`, BAG_IN, BAG_INN, BAG_INTER, BAG_DIFF]) >>
3243 simp[] >>
3244 `bdominates R (y - II) (x - II)`
3245 by (match_mp_tac (GEN_ALL bdominates_BAG_DIFF) >> simp[] >>
3246 simp[Abbr`II`] >> metis_tac[FINITE_SUB_BAG, BAG_INTER_FINITE]) >>
3247 simp[] >>
3248 map_every (fn q => qpat_x_assum q mp_tac)
3249 [`x <= b2`, `II <= x`, `II <= y`] >>
3250 simp_tac bool_ss [BAG_DIFF, SUB_BAG_LEQ, BAG_UNION, FUN_EQ_THM] >>
3251 ntac 3 strip_tac >> qx_gen_tac `a` >>
3252 ntac 3 (pop_assum (qspec_then `a` mp_tac)) >> simp[]
3253QED
3254
3255Theorem BAG_DIFF_INSERT_SUB_BAG:
3256 c <= b ==> (BAG_INSERT e b - c = BAG_INSERT e (b - c))
3257Proof
3258 simp[SUB_BAG_LEQ, BAG_INSERT, BAG_DIFF, FUN_EQ_THM] >> strip_tac >>
3259 qx_gen_tac `e2` >> pop_assum (qspec_then `e2` mp_tac) >> rw[] >>
3260 simp[]
3261QED
3262
3263Theorem mlt_INSERT_CANCEL:
3264 transitive R /\ WF R ==>
3265 (mlt R (BAG_INSERT e a) (BAG_INSERT e b) <=> mlt R a b)
3266Proof
3267 simp[mlt_dominates_thm2] >> strip_tac >> eq_tac >> strip_tac >> simp[]
3268 >- (map_every qexists_tac [`x`, `y`] >> simp[] >>
3269 `x <= b`
3270 by (qpat_x_assum `x <= BAG_INSERT e b` mp_tac >>
3271 simp[SUB_BAG_LEQ, BAG_INSERT] >> strip_tac >>
3272 qx_gen_tac `e2` >> pop_assum (qspec_then `e2` mp_tac) >> rw[] >>
3273 spose_not_then strip_assume_tac >>
3274 `x e = b e + 1` by decide_tac >>
3275 `BAG_IN e x` by simp[BAG_IN, BAG_INN] >>
3276 `~BAG_IN e (BAG_INSERT e b - x)`
3277 by simp[BAG_IN, BAG_INSERT, BAG_DIFF, BAG_INN] >>
3278 `BAG_IN e y` by metis_tac[BAG_IN_BAG_INSERT, BAG_IN_BAG_UNION] >>
3279 metis_tac[BAG_DISJOINT_BAG_IN]) >>
3280 `BAG_INSERT e b - x + y = BAG_INSERT e (b - x + y)` suffices_by
3281 metis_tac[BAG_INSERT_ONE_ONE] >>
3282 `BAG_INSERT e b - x = BAG_INSERT e (b - x)`
3283 by metis_tac[BAG_DIFF_INSERT_SUB_BAG] >>
3284 pop_assum SUBST_ALL_TAC >> simp[BAG_UNION_INSERT]) >>
3285 map_every qexists_tac [`x`, `y`] >>
3286 simp[BAG_DIFF_INSERT_SUB_BAG, BAG_UNION_INSERT, SUB_BAG_INSERT_I]
3287QED
3288
3289Theorem mlt_UNION_RCANCEL_I:
3290 mlt R a b /\ FINITE_BAG c ==>
3291 mlt R (BAG_UNION a c) (BAG_UNION b c)
3292Proof
3293 `mlt R a b ==>
3294 !c. FINITE_BAG c ==>
3295 mlt R (BAG_UNION a c) (BAG_UNION b c)`
3296 suffices_by metis_tac[] >> strip_tac >>
3297 ho_match_mp_tac STRONG_FINITE_BAG_INDUCT >>
3298 simp[BAG_UNION_INSERT, mlt_INSERT_CANCEL_I]
3299QED
3300
3301Theorem mlt_UNION_RCANCEL[simp]:
3302 WF R /\ transitive R ==>
3303 (mlt R (BAG_UNION a c) (BAG_UNION b c) <=> mlt R a b /\ FINITE_BAG c)
3304Proof
3305 strip_tac >> reverse (Cases_on `FINITE_BAG c`) >> simp[]
3306 >- (strip_tac >> imp_res_tac TC_mlt1_FINITE_BAG >> fs[]) >>
3307 map_every qid_spec_tac [`a`, `b`] >> pop_assum mp_tac >>
3308 qid_spec_tac `c` >> ho_match_mp_tac STRONG_FINITE_BAG_INDUCT >>
3309 simp[BAG_UNION_INSERT, mlt_INSERT_CANCEL]
3310QED
3311
3312Theorem mlt_UNION_LCANCEL_I =
3313 ONCE_REWRITE_RULE [COMM_BAG_UNION] mlt_UNION_RCANCEL_I;
3314
3315Theorem mlt_UNION_LCANCEL[simp] =
3316 ONCE_REWRITE_RULE [COMM_BAG_UNION] mlt_UNION_RCANCEL
3317
3318Theorem mlt_UNION_lemma[local]:
3319 WF R ==>
3320 (mlt R b1 (BAG_UNION b1 b2) <=>
3321 FINITE_BAG b1 /\ FINITE_BAG b2 /\ b2 <> {||})
3322Proof
3323 strip_tac >> `WF (mlt R)` by simp[relationTheory.WF_TC_EQN, WF_mlt1] >>
3324 reverse eq_tac >- simp[TC_mlt1_UNION2_I] >>
3325 strip_tac >> imp_res_tac TC_mlt1_FINITE_BAG >>
3326 fs[] >> strip_tac >> fs[] >> metis_tac[relationTheory.WF_NOT_REFL]
3327QED
3328
3329Theorem mlt_UNION_CANCEL_EQN[simp]:
3330 WF R ==>
3331 (mlt R b1 (BAG_UNION b1 b2) <=>
3332 FINITE_BAG b1 /\ FINITE_BAG b2 /\ b2 <> {||}) /\
3333 (mlt R b1 (BAG_UNION b2 b1) <=>
3334 FINITE_BAG b1 /\ FINITE_BAG b2 /\ b2 <> {||})
3335Proof
3336 metis_tac[COMM_BAG_UNION, mlt_UNION_lemma]
3337QED
3338
3339Theorem mlt_UNION_EMPTY_EQN =
3340 mlt_UNION_CANCEL_EQN |> Q.INST [`b1` |-> `{||}`]
3341 |> SIMP_RULE (srw_ss()) [];
3342
3343Theorem SUB_BAG_SING[simp]:
3344 b <= {|e|} <=> (b = {||}) \/ (b = {|e|})
3345Proof
3346 simp[SUB_BAG_LEQ, FUN_EQ_THM, EMPTY_BAG, BAG_INSERT, EQ_IMP_THM] >>
3347 rpt strip_tac >> simp[] >> Cases_on `b e = 1`
3348 >- (disj2_tac >> rw[] >> first_x_assum (qspec_then `x` mp_tac) >> simp[]) >>
3349 disj1_tac >> qx_gen_tac `x` >> first_x_assum (qspec_then `x` mp_tac) >>
3350 rw[] >> simp[]
3351QED
3352
3353Theorem SUB_BAG_DIFF_simple[simp]:
3354 b - c <= b:'a bag
3355Proof
3356 simp[SUB_BAG_DIFF]
3357QED
3358
3359Theorem mltLT_SING0:
3360 mlt (<) {|0:num|} b <=> FINITE_BAG b /\ b <> {|0|} /\ b <> {||}
3361Proof
3362 reverse eq_tac
3363 >- (strip_tac >> simp[mlt_dominates_thm1, relationTheory.transitive_def] >>
3364 Cases_on `BAG_IN 0 b`
3365 >- (map_every qexists_tac [`b - {|0|}`, `{||}`] >>
3366 simp[] >>
3367 qpat_x_assum`BAG_IN 0 b` mp_tac >>
3368 simp[BAG_IN, BAG_INN, FUN_EQ_THM, EMPTY_BAG,
3369 BAG_INSERT, BAG_DIFF] >> rw[] >> rw[] >>
3370 simp[]) >>
3371 map_every qexists_tac [`b`, `{|0|}`] >> simp[] >>
3372 simp[dominates_def] >>
3373 `?e b0. b = BAG_INSERT e b0` by metis_tac [BAG_cases] >>
3374 metis_tac[BAG_IN_BAG_INSERT, DECIDE ``x <> 0 <=> 0 < x``]) >>
3375 simp[mlt_dominates_thm2, relationTheory.transitive_def] >>
3376 rpt strip_tac
3377 >- (fs[] >> fs[] >> rw[] >> fs[] >> rw[] >>
3378 metis_tac[BAG_DISJOINT_BAG_IN, BAG_IN_BAG_INSERT]) >>
3379 fs[]
3380QED
3381
3382(*---------------------------------------------------------------------------*)
3383(* Size of a finite multiset is taken to be the sum of the sizes of all the *)
3384(* elements, plus the number of elements. *)
3385(*---------------------------------------------------------------------------*)
3386
3387Definition bag_size_def:
3388 bag_size eltsize b = ITBAG (\e acc. 1 + eltsize e + acc) b 0
3389End
3390
3391Theorem BAG_SIZE_EMPTY:
3392 bag_size eltsize {||} = 0
3393Proof
3394 METIS_TAC [ITBAG_THM,bag_size_def,FINITE_EMPTY_BAG]
3395QED
3396
3397(*---------------------------------------------------------------------------*)
3398(* BAG_SIZE_INSERT = *)
3399(* |- FINITE_BAG b ==> *)
3400(* bag_size eltsize (BAG_INSERT e b) = 1 + eltsize e + bag_size eltsize b *)
3401(*---------------------------------------------------------------------------*)
3402
3403Theorem BAG_SIZE_INSERT = (
3404 let val f = ``\(e:'a) acc. 1 + eltsize e + acc``
3405 val LCOMM_INCR = Q.prove
3406 (`!x y z. ^f x (^f y z) = ^f y (^f x z)`, RW_TAC arith_ss [])
3407 in COMMUTING_ITBAG_RECURSES
3408 |> ISPEC f
3409 |> SIMP_RULE bool_ss [LCOMM_INCR]
3410 |> (ISPEC``0n`` o Q.ID_SPEC o Q.ID_SPEC)
3411 |> SIMP_RULE bool_ss [GSYM bag_size_def]
3412 end)
3413
3414val _ = print "Unibags (bags made all distinct)\n"
3415
3416Overload unibag = ``\b. BAG_OF_SET (SET_OF_BAG b)``
3417
3418Theorem unibag_thm = CONJ BAG_OF_SET SET_OF_BAG;
3419
3420Theorem unibag_INSERT:
3421 !a b. (unibag (BAG_INSERT a b)) = BAG_MERGE {|a|} (unibag b)
3422Proof rw[BAG_OF_SET_INSERT,SET_OF_BAG_INSERT]
3423QED
3424
3425Theorem unibag_UNION:
3426 !a b. unibag (a + b) = BAG_MERGE (unibag a) (unibag b)
3427Proof rw[SET_OF_BAG_UNION,BAG_OF_SET_UNION]
3428QED
3429
3430Theorem unibag_EQ_BAG_INSERT:
3431 !e b b'. (unibag b = BAG_INSERT e b') ==> ?c. (b' = unibag c)
3432Proof
3433 rw[] >>
3434 fs[unibag_thm,BAG_INSERT,FUN_EQ_THM,BAG_IN,BAG_INN] >>
3435 qexists_tac `b'` >>
3436 rw[] >>
3437 first_x_assum (qspec_then `x` mp_tac) >>
3438 rw[] >>
3439 Induct_on `b' e` >>
3440 rw[]
3441QED
3442
3443Theorem unibag_FINITE:
3444 !b. FINITE_BAG (unibag b) = FINITE_BAG b
3445Proof
3446 rw[] >> EQ_TAC >> metis_tac[FINITE_SET_OF_BAG, FINITE_BAG_OF_SET]
3447QED
3448
3449Theorem unibag_ALL_DISTINCT:
3450 !b. BAG_ALL_DISTINCT (unibag b)
3451Proof rw[BAG_ALL_DISTINCT]
3452QED
3453
3454Theorem BAG_IN_unibag[simp]:
3455 !e b. BAG_IN e (unibag b) <=> BAG_IN e b
3456Proof rw[BAG_IN]
3457QED
3458
3459Theorem unibag_EL_MERGE_cases:
3460 !e b. ((BAG_IN e b) ==> (BAG_MERGE {|e|} (unibag b) = (unibag b))) /\
3461 (~(BAG_IN e b) ==> (BAG_MERGE {|e|} (unibag b) = BAG_INSERT e (unibag b)))
3462Proof
3463 rw[]
3464 >- (`BAG_ALL_DISTINCT (unibag b)` by metis_tac[unibag_ALL_DISTINCT] >>
3465 `BAG_ALL_DISTINCT {|e|}` by simp[BAG_ALL_DISTINCT_THM] >>
3466 `BAG_ALL_DISTINCT (BAG_MERGE {|e|} (unibag b))`
3467 by simp[BAG_ALL_DISTINCT_BAG_MERGE] >>
3468 qspecl_then [`BAG_MERGE {|e|} (unibag b)`,`unibag b`] mp_tac
3469 BAG_ALL_DISTINCT_EXTENSION >>
3470 rw[] >>
3471 metis_tac[])
3472 >- (`BAG_ALL_DISTINCT (unibag b)` by metis_tac[unibag_ALL_DISTINCT] >>
3473 `BAG_ALL_DISTINCT {|e|}` by simp[BAG_ALL_DISTINCT_THM] >>
3474 `BAG_ALL_DISTINCT (BAG_MERGE {|e|} (unibag b))`
3475 by simp[BAG_ALL_DISTINCT_BAG_MERGE] >>
3476 `BAG_ALL_DISTINCT (BAG_INSERT e (unibag b))`
3477 by simp[BAG_ALL_DISTINCT] >>
3478 qspecl_then [`BAG_MERGE {|e|} (unibag b)`,`BAG_INSERT e (unibag b)`]
3479 mp_tac BAG_ALL_DISTINCT_EXTENSION >>
3480 rw[])
3481QED
3482
3483Theorem unibag_DECOMPOSE:
3484 unibag g <> g ==> ?A g0. g = {|A;A|} + g0
3485Proof
3486 simp[unibag_thm] >>
3487 simp[SimpL ``$==>``,FUN_EQ_THM,PULL_EXISTS] >>
3488 rw[]
3489 >- (qexists_tac `x` >>
3490 qexists_tac `g (| x |-> g x - 2 |)` >>
3491 fs[BAG_IN,BAG_INN] >>
3492 simp[FUN_EQ_THM,BAG_UNION,
3493 BAG_INSERT,EMPTY_BAG,combinTheory.APPLY_UPDATE_THM] >>
3494 qx_gen_tac `y` >>
3495 Cases_on `x=y` >>
3496 rw[])
3497 >- fs[BAG_IN,BAG_INN]
3498QED
3499
3500Theorem unibag_SUB_BAG:
3501 !b. unibag b <= b
3502Proof rw[unibag_thm,SUB_BAG,BAG_IN,BAG_INN]
3503QED
3504
3505Theorem BAG_OF_SET_IMAGE_INJ:
3506 !f s.
3507 (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y) ==>
3508 BAG_OF_SET (IMAGE f s) = BAG_IMAGE f (BAG_OF_SET s)
3509Proof
3510 rw[FUN_EQ_THM, BAG_OF_SET, BAG_IMAGE_DEF]
3511 \\ rw[] \\ gs[GSYM BAG_OF_SET]
3512 \\ gs[BAG_FILTER_BAG_OF_SET]
3513 \\ simp[BAG_CARD_BAG_OF_SET]
3514 >- (
3515 irule SING_CARD_1
3516 \\ simp[SING_TEST, GSYM pred_setTheory.MEMBER_NOT_EMPTY]
3517 \\ metis_tac[] )
3518 >- simp[EXTENSION]
3519 \\ qmatch_assum_abbrev_tac`INFINITE z`
3520 \\ `z = {}` suffices_by metis_tac[FINITE_EMPTY]
3521 \\ simp[EXTENSION, Abbr`z`]
3522QED
3523
3524(* Theorem: x IN SET_OF_BAG b <=> b x <> 0 *)
3525(* Proof: by definitions *)
3526Theorem IN_SET_OF_BAG_NONZERO:
3527 !b x. x IN SET_OF_BAG b <=> b x <> 0
3528Proof
3529 rw[SET_OF_BAG, BAG_IN, BAG_INN]
3530QED
3531
3532(* Theorem: FINITE_BAG b ==> (!e. BAG_IN e b ==> (b e = 1)) ==> (BAG_CARD b = CARD (SET_OF_BAG b)) *)
3533(* Proof:
3534 By finite induction on b.
3535 Base: BAG_CARD {||} = CARD (SET_OF_BAG {||})
3536 BAG_CARD {||}
3537 = 0 by BAG_CARD_EMPTY
3538 = CARD {} by CARD_EMPTY
3539 = CARD (SET_OF_BAG {||}) by SET_OF_BAG_EQ_EMPTY
3540 Step: (!e. BAG_IN e b ==> (b e = 1)) ==> (BAG_CARD b = CARD (SET_OF_BAG b)) ==>
3541 BAG_CARD (BAG_INSERT e b) = CARD (SET_OF_BAG (BAG_INSERT e b))
3542 After simplication by BAG_CARD_THM, BAG_INSERT, SET_OF_BAG_INSERT, BAG_IN, BAG_INN,
3543 This comes down to:
3544 (1) b e >= 1 ==> BAG_CARD b + 1 = CARD (SET_OF_BAG b)
3545 In this case, b e + 1 = 1 by implication.
3546 Thus b e = 0 by arithmetic
3547 This contradicts b e >= 1.
3548 (2) ~(b e >= 1) ==> BAG_CARD b = CARD (SET_OF_BAG b)
3549 In this case, !e'. b e' >= 1 ==> (b e' = 1) by implication
3550 Applying induction hypothesis, the result follows.
3551*)
3552Theorem BAG_CARD_EQ_CARD_SET_OF_BAG:
3553 !b:'a bag. FINITE_BAG b ==> (!e. BAG_IN e b ==> (b e = 1)) ==> (BAG_CARD b = CARD (SET_OF_BAG b))
3554Proof
3555 Induct_on `FINITE_BAG` >>
3556 rpt strip_tac >-
3557 rw[] >>
3558 rw[BAG_CARD_THM] >>
3559 fs[BAG_INSERT, SET_OF_BAG_INSERT] >>
3560 fs[BAG_IN, BAG_INN, ADD1] >>
3561 rw[] >| [
3562 `b e + 1 = 1` by metis_tac[] >>
3563 decide_tac,
3564 metis_tac[]
3565 ]
3566QED
3567
3568(*---------------------------------------------------------------------------*)
3569(* Add multiset type to the TypeBase. *)
3570(*---------------------------------------------------------------------------*)
3571
3572val _ = TypeBase.export [
3573 TypeBasePure.mk_nondatatype_info
3574 (“:'a -> num”,
3575 {nchotomy = SOME BAG_cases,
3576 induction = SOME STRONG_FINITE_BAG_INDUCT,
3577 size = NONE,
3578 encode=NONE})
3579 ]