Lines Matching defs:b1
118 val (b1,b2) = dest_union b;
119 val t1 = mk_image (f, b1)
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;
183 val (finite_thm1, card_thm1) = BAG_CARD_CONV___FINITE b1;
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 =
286 val l1 = fst (strip_insert b1);
293 fun get_resort_positions___pred_pair P b1 b2 =
295 val l1 = fst (strip_insert b1);
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
403 val _ = if null n1L andalso not (bagSyntax.is_empty b1)
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
488 val b1_thm = SIMPLE_BAG_NORMALISE_CONV b1 handle UNCHANGED => REFL b1
491 val b1' = rhs (concl b1_thm)
497 val (b1L,b1_rest) = strip_insert b1'
504 val thm0 = ISPECL [b1',b2'] bag_card_eq_thm
514 val (n1L,n2L) = get_resort_lists___pred_pair aconv b1' b2'