Lines Matching refs:b2
118 val (b1,b2) = dest_union b;
120 val t2 = mk_image (f, b2)
125 val finite_thm = EQ_MP (GSYM (ISPECL [b1,b2] bagTheory.FINITE_BAG_UNION))
127 val bag_thm' = MP (ISPECL [b1,b2,f] bagTheory.BAG_IMAGE_FINITE_UNION) finite_thm12
182 val (b1,b2) = dest_union b;
184 val (finite_thm2, card_thm2) = BAG_CARD_CONV___FINITE b2;
187 val finite_thm = EQ_MP (GSYM (ISPECL [b1,b2] bagTheory.FINITE_BAG_UNION))
189 val card_thm' = MP (ISPECL [b1,b2] bagTheory.BAG_CARD_UNION) finite_thm12
284 fun get_resort_lists___pred_pair p b1 b2 =
287 val l2 = fst (strip_insert b2);
293 fun get_resort_positions___pred_pair P b1 b2 =
296 val l2 = fst (strip_insert b2);
358 val (b1,b2) = bagSyntax.dest_sub_bag tm
359 val (n1L,n2L) = get_resort_lists___pred_pair aconv b1 b2
401 val (b1,b2) = bagSyntax.dest_diff tm
402 val (n1L,n2L) = get_resort_lists___pred_pair aconv b1 b2
404 andalso not (bagSyntax.is_empty b2) then raise UNCHANGED else ();
482 ``!(b1:'a -> num) b2. ~(BAG_CARD b1 = BAG_CARD b2) ==> ((b1 = b2) = F)``,
483 REPEAT GEN_TAC THEN Cases_on `b1 = b2` THEN ASM_REWRITE_TAC[])
487 val (b1,b2) = dest_eq tm
489 val b2_thm = SIMPLE_BAG_NORMALISE_CONV b2 handle UNCHANGED => REFL b2
492 val b2' = rhs (concl b2_thm)
498 val (b2L,b2_rest) = strip_insert b2'
504 val thm0 = ISPECL [b1',b2'] bag_card_eq_thm
514 val (n1L,n2L) = get_resort_lists___pred_pair aconv b1' b2'