Lines Matching refs:b2
32 `SUB_BAG b1 b2 = !x n. BAG_INN x n b1 ==> BAG_INN x n b2`);
36 `PSUB_BAG b1 b2 <=> SUB_BAG b1 b2 /\ ~(b1 = b2)`);
61 ``BAG_DIFF b1 (b2:'a bag) = \x. b1 x - b2 x``);
87 `BAG_INTER b1 b2 = (\x. if (b1 x < b2 x) then b1 x else b2 x)`);
94 `BAG_MERGE b1 b2 = (\x. if (b1 x < b2 x) then b2 x else b1 x)`);
218 !b1 b2 e. BAG_IN e (BAG_UNION b1 b2) <=> BAG_IN e b1 \/ BAG_IN e b2
224 `!n e b1 b2. BAG_INN e n (BAG_UNION b1 b2) =
225 ?m1 m2. (n = m1 + m2) /\ BAG_INN e m1 b1 /\ BAG_INN e m2 b2`,
229 `n <= b1 e + b2 e` by DECIDE_TAC THEN
231 `m1 < b1 e \/ m2 < b2 e` by DECIDE_TAC THENL [
238 `!n e b1 b2. (BAG_INN e n (BAG_MERGE b1 b2)) =
239 (BAG_INN e n b1 \/ BAG_INN e n b2)`,
244 !e b1 b2. BAG_IN e (BAG_MERGE b1 b2) <=> BAG_IN e b1 \/ BAG_IN e b2
252 ``!b1 b2. (b1 = b2) = (!n e:'a. BAG_INN e n b1 = BAG_INN e n b2)``,
264 `!e b1 b2.
265 (BAG_UNION (BAG_INSERT e b1) b2 = BAG_INSERT e (BAG_UNION b1 b2)) /\
266 (BAG_UNION b1 (BAG_INSERT e b2) = BAG_INSERT e (BAG_UNION b1 b2))`,
285 ``!b1 b2 x:'a.
286 (BAG_INSERT x b1 = BAG_INSERT x b2) = (b1 = b2)``,
321 ``!b b1 b2:'a -> num. (BAG_UNION b b1 = BAG_UNION b b2) = (b1 = b2)``,
327 ``!b1 b2. BAG_UNION b1 b2 = BAG_UNION b2 b1``,
333 ``!b b1 b2:'a bag. (BAG_UNION b1 b = BAG_UNION b2 b) = (b1 = b2)``,
339 ``!b1 b2 b3. BAG_UNION b1 (BAG_UNION b2 b3)
341 BAG_UNION (BAG_UNION b1 b2) b3``,
347 (!b1 b2. (b1 + b2 = {||}) <=> (b1 = {||}) /\ (b2 = {||}))
364 ``!b0 b1 b2 e1 e2:'a.
365 BAG_DELETE b0 e1 b1 /\ BAG_DELETE b1 e2 b2 ==>
366 ?b'. BAG_DELETE b0 e2 b' /\ BAG_DELETE b' e1 b2``,
372 ``!b0 (e1:'a) e2 b1 b2.
373 BAG_DELETE b0 e1 b1 /\ BAG_DELETE b0 e2 b2 ==>
374 ((e1 = e2) = (b1 = b2))``,
397 `!x y b1 b2.
398 BAG_DELETE (BAG_INSERT x b1) y b2 ==>
399 (x = y) /\ (b1 = b2) \/ (?b3. BAG_DELETE b1 y b3) /\ ~(x = y)`,
494 ``!b0 e1 e2 b1 b2.
495 BAG_DELETE b0 e1 b1 /\ BAG_DELETE b0 e2 b2 /\ ~(b1 = b2) ==>
496 ?b. BAG_DELETE b1 e2 b /\ BAG_DELETE b2 e1 b``,
498 `b2 + {|e2|} = b1 + {|e1|}` by SRW_TAC [][BAG_UNION_INSERT] THEN
538 `!e b1 b2 b. (BAG_INSERT e b = BAG_UNION b1 b2) ==>
539 BAG_IN e b1 \/ BAG_IN e b2`,
574 ``SUB_BAG b1 b2 = !x. b1 x <= b2 x``,
598 ``!(b1:'a -> num) b2. SUB_BAG b1 b2 /\ SUB_BAG b2 b1 ==> (b1 = b2)``,
604 ``!(b1:'a -> num) b2. ~(PSUB_BAG b1 b2 /\ PSUB_BAG b2 b1)``,
609 ``!b1 b2 b3. SUB_BAG (b1:'a->num) b2 /\ SUB_BAG b2 b3 ==>
615 ``!(b1:'a -> num) b2 b3. PSUB_BAG b1 b2 /\ PSUB_BAG b2 b3 ==>
621 ``!(b1:'a->num) b2. PSUB_BAG b1 b2 ==> SUB_BAG b1 b2``,
626 ``!(b1:'a -> num) b2. PSUB_BAG b1 b2 ==> ~(b1 = b2)``,
636 (!b1 b2.
637 b1 <= b2 ==> (b1 - b2 = {||}))``,
652 ``!x b1 b2. BAG_DIFF (BAG_INSERT x b1) (BAG_INSERT x b2) =
653 BAG_DIFF b1 b2``,
659 `!x b1 b2.
661 (BAG_DIFF (BAG_INSERT x b2) b1 = BAG_INSERT x (BAG_DIFF b2 b1))`,
667 `!x b1 b2. ~BAG_IN x b1 ==>
668 (BAG_DIFF b1 (BAG_INSERT x b2) = BAG_DIFF b1 b2)`,
674 `e <: b1 /\ ~(e <: b2) ==> e <: b1 - b2`,
679 `e <: b1 - b2 ==> e <: b1`,
720 fun bdf (b1, b2) (b3, b4) =
722 case map (C (curry mk_var) (==`:'a->num`==)) [b1, b2, b3, b4] of
727 BAG_DIFF b2 b3``
732 ``!(b1:'a->num) (b2:'a->num) (b3:'a->num).
733 ^(bdf ("b1", "b2") ("b1", "b3")) /\
734 ^(bdf ("b1", "b2") ("b3", "b1")) /\
735 ^(bdf ("b2", "b1") ("b1", "b3")) /\
736 ^(bdf ("b2", "b1") ("b3", "b1"))``,
743 fun bdf (b1, b2) (b3, b4) =
745 case map (C (curry mk_var) (==`:'a->num`==)) [b1, b2, b3, b4] of
750 SUB_BAG (b2:'a->num) b3``
755 ``!(b1:'a->num) (b2:'a->num) (b3:'a->num).
756 ^(bdf ("b1", "b2") ("b1", "b3")) /\
757 ^(bdf ("b1", "b2") ("b3", "b1")) /\
758 ^(bdf ("b2", "b1") ("b1", "b3")) /\
759 ^(bdf ("b2", "b1") ("b3", "b1"))``,
780 `!b1 b2:'a->num. SUB_BAG b1 b2 ==> !b. SUB_BAG b1 (BAG_UNION b2 b)`,
781 `!b1 b2:'a->num. SUB_BAG b1 b2 ==> !b. SUB_BAG b1 (BAG_UNION b b2)`
785 `!b1 b2 b3:'a->num.
786 SUB_BAG b1 (BAG_UNION b2 b3) ==>
787 !b. SUB_BAG b1 (BAG_UNION (BAG_UNION b2 b) b3)`,
788 `!b1 b2 b3:'a->num.
789 SUB_BAG b1 (BAG_UNION b2 b3) ==>
790 !b. SUB_BAG b1 (BAG_UNION (BAG_UNION b b2) b3)`]
798 `!b1 b2 b3 b4:'a->num.
799 SUB_BAG b1 b3 ==> SUB_BAG b2 b4 ==>
800 SUB_BAG (BAG_UNION b1 b2) (BAG_UNION b3 b4)`,
801 `!b1 b2 b3 b4:'a->num.
802 SUB_BAG b1 b4 ==> SUB_BAG b2 b3 ==>
803 SUB_BAG (BAG_UNION b1 b2) (BAG_UNION b3 b4)`];
806 `!b1 b2 b3 b4 b5:'a->num.
807 SUB_BAG b1 (BAG_UNION b3 b5) ==> SUB_BAG b2 b4 ==>
808 SUB_BAG (BAG_UNION b1 b2) (BAG_UNION (BAG_UNION b3 b4) b5)`,
809 `!b1 b2 b3 b4 b5:'a->num.
810 SUB_BAG b1 (BAG_UNION b4 b5) ==> SUB_BAG b2 b3 ==>
811 SUB_BAG (BAG_UNION b1 b2) (BAG_UNION (BAG_UNION b3 b4) b5)`,
812 `!b1 b2 b3 b4 b5:'a->num.
813 SUB_BAG b2 (BAG_UNION b3 b5) ==> SUB_BAG b1 b4 ==>
814 SUB_BAG (BAG_UNION b1 b2) (BAG_UNION (BAG_UNION b3 b4) b5)`,
815 `!b1 b2 b3 b4 b5:'a->num.
816 SUB_BAG b2 (BAG_UNION b4 b5) ==> SUB_BAG b1 b3 ==>
817 SUB_BAG (BAG_UNION b1 b2) (BAG_UNION (BAG_UNION b3 b4) b5)`];
825 `!b1 b2 b3 b4 b5:'a->num.
826 SUB_BAG (BAG_UNION b1 b2) b4 ==> SUB_BAG b3 b5 ==>
827 SUB_BAG (BAG_UNION (BAG_UNION b1 b3) b2) (BAG_UNION b4 b5)`,
828 `!b1 b2 b3 b4 b5:'a->num.
829 SUB_BAG (BAG_UNION b1 b2) b5 ==> SUB_BAG b3 b4 ==>
830 SUB_BAG (BAG_UNION (BAG_UNION b1 b3) b2) (BAG_UNION b4 b5)`,
831 `!b1 b2 b3 b4 b5:'a->num.
832 SUB_BAG (BAG_UNION b3 b2) b4 ==> SUB_BAG b1 b5 ==>
833 SUB_BAG (BAG_UNION (BAG_UNION b1 b3) b2) (BAG_UNION b4 b5)`,
834 `!b1 b2 b3 b4 b5:'a->num.
835 SUB_BAG (BAG_UNION b3 b2) b5 ==> SUB_BAG b1 b4 ==>
836 SUB_BAG (BAG_UNION (BAG_UNION b1 b3) b2) (BAG_UNION b4 b5)`];
856 `!e b1 b2. SUB_BAG (BAG_INSERT e b1) (BAG_INSERT e b2) =
857 SUB_BAG b1 b2`,
869 `!b1 b2 e. ~(BAG_IN e b1) ==>
870 (SUB_BAG b1 (BAG_INSERT e b2) = SUB_BAG b1 b2)`,
885 `!x b1 b2. SUB_BAG (BAG_INSERT x b1) b2 ==> BAG_IN x b2`,
893 ``!b1 b2:'a->num. SUB_BAG b1 b2 = ?b. b2 = BAG_UNION b1 b``,
895 Q.EXISTS_TAC `\x. b2 x - b1 x` THEN
902 ``!b1 b2 b3:'a->num.
904 (SUB_BAG b2 (BAG_DIFF b3 b1) = SUB_BAG (BAG_UNION b1 b2) b3)
912 ``!b1 b2 b3:'a->num. SUB_BAG (BAG_UNION b1 b2) b3 ==>
913 SUB_BAG b1 b3 /\ SUB_BAG b2 b3``,
920 ``(!b1 b2:'a->num. SUB_BAG b1 b2 ==>
921 (!b3. SUB_BAG (BAG_DIFF b1 b3) b2)) /\
922 (!b1 b2 b3 b4:'a->num.
923 SUB_BAG b2 b1 ==> SUB_BAG b4 b3 ==>
924 (SUB_BAG (BAG_DIFF b1 b2) (BAG_DIFF b3 b4) =
925 SUB_BAG (BAG_UNION b1 b4) (BAG_UNION b2 b3)))``,
931 ``!(b1:'a -> num) b2.
932 SUB_BAG b1 b2 = PSUB_BAG b1 b2 \/ (b1 = b2)``,
1013 ``!b1 b2:'a->num.
1014 SUB_BAG b1 b2 ==> (SET_OF_BAG b1) SUBSET (SET_OF_BAG b2)``,
1020 ``!b1 b2:'a->num. SET_OF_BAG (BAG_UNION b1 b2) =
1021 SET_OF_BAG b1 UNION SET_OF_BAG b2``,
1026 ``!b1 b2. SET_OF_BAG (BAG_MERGE b1 b2) =
1027 SET_OF_BAG b1 UNION SET_OF_BAG b2``,
1047 `!b1 b2. (SET_OF_BAG b1) DIFF (SET_OF_BAG b2) SUBSET
1048 SET_OF_BAG (BAG_DIFF b1 b2)`,
1055 `!b1 b2. SET_OF_BAG (BAG_DIFF b1 b2) SUBSET SET_OF_BAG b1`,
1094 ``BAG_DISJOINT (b1:'a->num) b2 =
1095 DISJOINT (SET_OF_BAG b1) (SET_OF_BAG b2)``);
1114 ``!b1 b2. BAG_DISJOINT b1 b2 =
1115 !e. ~(BAG_IN e b1) \/ ~(BAG_IN e b2)``,
1122 ``(!b1 b2 e1.
1123 BAG_DISJOINT (BAG_INSERT e1 b1) b2 =
1124 (~(BAG_IN e1 b2) /\ (BAG_DISJOINT b1 b2))) /\
1125 (!b1 b2 e2.
1126 BAG_DISJOINT b1 (BAG_INSERT e2 b2) =
1127 (~(BAG_IN e2 b1) /\ (BAG_DISJOINT b1 b2)))``,
1134 ``(BAG_DISJOINT b1 (BAG_UNION b2 b3) <=>
1135 BAG_DISJOINT b1 b2 /\ BAG_DISJOINT b1 b3) /\
1136 (BAG_DISJOINT (BAG_UNION b1 b2) b3 <=>
1137 BAG_DISJOINT b1 b3 /\ BAG_DISJOINT b2 b3)``,
1205 `!b1. FINITE_BAG b1 ==> !b2. FINITE_BAG (BAG_DIFF b1 b2)`,
1208 REPEAT STRIP_TAC THEN Q.ASM_CASES_TAC `BAG_IN e b2` THENL [
1217 !b2. FINITE_BAG (BAG_DIFF b2 b1) ==> FINITE_BAG b2`,
1220 REPEAT STRIP_TAC THEN Q.ASM_CASES_TAC `BAG_IN e b2` THENL [
1228 !b2. FINITE_BAG b2 ==> FINITE_BAG (BAG_UNION b1 b2)`,
1233 !b1 b2. (b = BAG_UNION b1 b2) ==> FINITE_BAG b1 /\ FINITE_BAG b2``,
1242 !b1 b2. FINITE_BAG (BAG_UNION b1 b2) <=>
1243 FINITE_BAG b1 /\ FINITE_BAG b2
1249 `!b1. FINITE_BAG b1 ==> !b2. SUB_BAG b2 b1 ==> FINITE_BAG b2`,
1252 REPEAT STRIP_TAC THEN Q.ASM_CASES_TAC `BAG_IN e b2` THENL [
1407 Term `!b1 b2. FINITE_BAG b1 /\ FINITE_BAG b2 ==>
1408 (BAG_CARD (BAG_UNION b1 b2) =
1409 (BAG_CARD b1) + (BAG_CARD b2))`,
1448 `!b1 b2. SUB_BAG b1 b2 ==> (b2 = BAG_UNION b1 (BAG_DIFF b2 b1))`,
1455 (`!b1 b2. SUB_BAG b1 b2 ==> ?d. b2 = BAG_UNION b1 d`,
1460 `!b1 b2:'a bag. FINITE_BAG b2 /\ SUB_BAG b1 b2 ==> BAG_CARD b1 <= BAG_CARD b2`,
1462 THEN `?d. b2 = BAG_UNION b1 d` by PROVE_TAC [SUB_BAG_DIFF_EQ]
1718 ``!b1 b2 f. (FINITE_BAG b1 /\ FINITE_BAG b2)
1719 ==> (BAG_IMAGE f (BAG_UNION b1 b2)
1720 = (BAG_UNION (BAG_IMAGE f b1) (BAG_IMAGE f b2)))``,
1842 (`!b1 b2. (b1 = BAG_UNION b1 b2) = (b2 = {||})`,
1858 `!b1 b2:'a bag. FINITE_BAG b2 /\ PSUB_BAG b1 b2 ==> BAG_CARD b1 < BAG_CARD b2`,
1860 THEN `?d. b2 = BAG_UNION b1 d` by PROVE_TAC [SUB_BAG_DIFF_EQ]
2078 `BAG_EVERY P (b1 + b2) <=> BAG_EVERY P b1 /\ BAG_EVERY P b2`,
2084 `BAG_EVERY P (BAG_MERGE b1 b2) <=> BAG_EVERY P b1 /\ BAG_EVERY P b2`,
2151 ``!b1 b2. BAG_ALL_DISTINCT (BAG_MERGE b1 b2) =
2152 (BAG_ALL_DISTINCT b1 /\ BAG_ALL_DISTINCT b2)``,
2163 ``!b1 b2.
2164 BAG_ALL_DISTINCT (BAG_UNION b1 b2) =
2165 (BAG_ALL_DISTINCT b1 /\ BAG_ALL_DISTINCT b2 /\
2166 BAG_DISJOINT b1 b2)``,
2178 ``!b1 b2.
2180 BAG_ALL_DISTINCT (BAG_DIFF b1 b2)``,
2211 ``!b1 b2 e. BAG_ALL_DISTINCT b1 ==>
2212 (BAG_IN e (BAG_DIFF b1 b2) <=> BAG_IN e b1 /\ ~BAG_IN e b2)``,
2218 ``!b1 b2. BAG_ALL_DISTINCT b1 ==>
2219 (SUB_BAG b1 b2 = (!x. BAG_IN x b1 ==> BAG_IN x b2))``,
2245 ``!b1 b2. (BAG_ALL_DISTINCT b1 /\ BAG_ALL_DISTINCT b2) ==>
2246 ((b1 = b2) = (!x. BAG_IN x b1 = BAG_IN x b2))``,
2259 !b1 b2 b3. b1 <= b2 /\ BAG_DISJOINT b2 b3 ==> BAG_DISJOINT b1 b3
2265 !b1 b2. BAG_DISJOINT b1 b2 <=> BAG_DISJOINT b2 b1
2311 !b2 a b. FINITE_BAG b2 ==>
2312 (BAG_GEN_PROD (BAG_UNION b1 b2) (a * b) =
2313 BAG_GEN_PROD b1 a * BAG_GEN_PROD b2 b)`,
2317 POP_ASSUM MP_TAC THEN Q.ID_SPEC_TAC `b2` THEN
2323 `FINITE_BAG (BAG_UNION b1 b2)` by METIS_TAC [FINITE_BAG_UNION] THEN
2329 `!b1 b2. FINITE_BAG b1 /\ FINITE_BAG b2 ==>
2330 (BAG_GEN_PROD (BAG_UNION b1 b2) 1 =
2331 BAG_GEN_PROD b1 1 * BAG_GEN_PROD b2 1)`,
2449 ``mlt1 r b1 b2 <=> FINITE_BAG b1 /\ FINITE_BAG b2 /\
2450 ?e rep res. (b1 = rep + res) /\ (b2 = res + {|e|}) /\
2544 ``!b1 b2. TC (mlt1 R) b1 b2 ==> FINITE_BAG b1 /\ FINITE_BAG b2``,
2550 ``!b2 b1. FINITE_BAG b2 /\ FINITE_BAG b1 /\ b2 <> {||} ==>
2551 (mlt1 R)^+ b1 (b1 + b2)``,
2553 `!b2. FINITE_BAG b2 ==> !b1. FINITE_BAG b1 /\ b2 <> {||} ==>
2554 (mlt1 R)^+ b1 (b1 + b2)` THEN1 METIS_TAC [] THEN
2556 Cases_on `b2 = {||}` THENL [
2561 `(mlt1 R)^+ b1 (b1 + b2)` by METIS_TAC [] THEN
2563 Q.EXISTS_TAC `b1 + b2` THEN SRW_TAC [][] THEN
2566 MAP_EVERY Q.EXISTS_TAC [`e`, `{||}`, `b1 + b2`] THEN SRW_TAC [][] THEN
2572 ``!b2 b1. FINITE_BAG b2 /\ FINITE_BAG b1 /\ b1 <> {||} ==>
2573 (mlt1 R)^+ b2 (b1 + b2)``,
2608 (* dominates R b1 b2 should be read as "b2 dominates b1 wrt relation R" *)
2614 ``\R b1 b2. dominates R (SET_OF_BAG b1) (SET_OF_BAG b2)``)
2677 !b1 b2. mlt R b1 b2 <=>
2678 FINITE_BAG b1 /\ FINITE_BAG b2 /\
2679 ?x y. x <> {||} /\ SUB_BAG x b2 /\
2680 (b1 = (b2 - x) + y) /\
2685 >- (simp[mlt1_def, dominates_def] >> map_every qx_gen_tac [`b1`, `b2`] >>
2736 `FINITE_BAG b2`, `FINITE_BAG y`, `bdominates R y x`,
2737 `x <= b2`, `x <> {||}`] >>
2738 map_every qid_spec_tac [`b2`, `y`] >> pop_assum mp_tac >>
2745 map_every qexists_tac [`e`, `y`, `b2 - {|e|}`] >>
2748 qexists_tac `b2 - {|e|} + BAG_FILTER (\x. R x e) y` >> reverse conj_tac
2750 map_every qexists_tac [`e`, `BAG_FILTER (\x. R x e) y`, `b2 - {|e|}`] >>
2753 `b2 - BAG_INSERT e x + y =
2754 b2 - {|e|} + BAG_FILTER (\x. R x e) y - x + BAG_FILTER (\x. ~R x e) y`
2755 by (qpat_x_assum `BAG_INSERT e x <= b2` mp_tac >>
2836 ``SUB_BAG (BAG_INTER b1 b2) b1 /\ SUB_BAG (BAG_INTER b1 b2) b2``,
2841 ``FINITE_BAG b1 \/ FINITE_BAG b2 ==> FINITE_BAG (BAG_INTER b1 b2)``,
2847 !b1 b2. mlt R b1 b2 <=>
2848 FINITE_BAG b1 /\ FINITE_BAG b2 /\
2849 ?x y. x <> {||} /\ SUB_BAG x b2 /\
2851 (b1 = (b2 - x) + y) /\
2854 map_every Cases_on [`FINITE_BAG b1`, `FINITE_BAG b2`] >> simp[] >>
2858 `x - II <= b2` by simp[SUB_BAG_DIFF] >>
2880 [`x <= b2`, `II <= x`, `II <= y`] >>
2948 (mlt R b1 (BAG_UNION b1 b2) <=>
2949 FINITE_BAG b1 /\ FINITE_BAG b2 /\ b2 <> {||})``,
2958 (mlt R b1 (BAG_UNION b1 b2) <=>
2959 FINITE_BAG b1 /\ FINITE_BAG b2 /\ b2 <> {||}) /\
2960 (mlt R b1 (BAG_UNION b2 b1) <=>
2961 FINITE_BAG b1 /\ FINITE_BAG b2 /\ b2 <> {||})``,