Theory "container"

Signature

Definitions

mlt_list_def

⊢ ∀R.
      mlt_list R =
      (λl1 l2.
           ∃h t list. (l1 = list ++ t) ∧ (l2 = h::t) ∧ ∀e. MEM e list ⇒ R e h)

LIST_TO_BAG_def

⊢ (LIST_TO_BAG [] = {||}) ∧
  ∀h t. LIST_TO_BAG (h::t) = BAG_INSERT h (LIST_TO_BAG t)

BAG_TO_LIST_primitive_def

⊢ BAG_TO_LIST =
  WFREC (@R. WF R ∧ ∀bag. FINITE_BAG bag ∧ bag ≠ {||} ⇒ R (BAG_REST bag) bag)
    (λBAG_TO_LIST a.
         I
           (if FINITE_BAG a then
              if a = {||} then [] else BAG_CHOICE a::BAG_TO_LIST (BAG_REST a)
            else ARB))

BAG_OF_FMAP_def

⊢ ∀f b. BAG_OF_FMAP f b = (λx. CARD (λk. k ∈ FDOM b ∧ (x = f k (b ' k))))

Theorems

WF_mlt_list

⊢ ∀R. WF R ⇒ WF (mlt_list R)

UNION_APPEND

⊢ ∀l1 l2. LIST_TO_SET l1 ∪ LIST_TO_SET l2 = LIST_TO_SET (l1 ++ l2)

SET_TO_LIST_THM

⊢ FINITE s ⇒
  (SET_TO_LIST s = if s = ∅ then [] else CHOICE s::SET_TO_LIST (REST s))

SET_TO_LIST_SING

⊢ SET_TO_LIST {x} = [x]

SET_TO_LIST_INV

⊢ ∀s. FINITE s ⇒ (LIST_TO_SET (SET_TO_LIST s) = s)

SET_TO_LIST_IND

⊢ ∀P. (∀s. (FINITE s ∧ s ≠ ∅ ⇒ P (REST s)) ⇒ P s) ⇒ ∀v. P v

SET_TO_LIST_IN_MEM

⊢ ∀s. FINITE s ⇒ ∀x. x ∈ s ⇔ MEM x (SET_TO_LIST s)

SET_TO_LIST_CARD

⊢ ∀s. FINITE s ⇒ (LENGTH (SET_TO_LIST s) = CARD s)

PERM_LIST_TO_BAG

⊢ ∀l1 l2. (LIST_TO_BAG l1 = LIST_TO_BAG l2) ⇔ PERM l1 l2

MEM_SET_TO_LIST

⊢ ∀s. FINITE s ⇒ ∀x. MEM x (SET_TO_LIST s) ⇔ x ∈ s

MEM_BAG_TO_LIST

⊢ ∀b. FINITE_BAG b ⇒ ∀x. MEM x (BAG_TO_LIST b) ⇔ x ⋲ b

LIST_TO_SET_THM

⊢ (LIST_TO_SET [] = ∅) ∧ (LIST_TO_SET (h::t) = h INSERT LIST_TO_SET t)

LIST_TO_SET_APPEND

⊢ ∀l1 l2. LIST_TO_SET (l1 ++ l2) = LIST_TO_SET l1 ∪ LIST_TO_SET l2

LIST_TO_BAG_SUBSET

⊢ ∀l1 l2. LIST_TO_BAG l1 ≤ LIST_TO_BAG l2 ⇒ LIST_TO_SET l1 ⊆ LIST_TO_SET l2

LIST_TO_BAG_SUB_BAG_FLAT_suff

⊢ ∀ls1 ls2.
      LIST_REL (λl1 l2. LIST_TO_BAG l1 ≤ LIST_TO_BAG l2) ls1 ls2 ⇒
      LIST_TO_BAG (FLAT ls1) ≤ LIST_TO_BAG (FLAT ls2)

LIST_TO_BAG_MAP

⊢ LIST_TO_BAG (MAP f b) = BAG_IMAGE f (LIST_TO_BAG b)

LIST_TO_BAG_FILTER

⊢ LIST_TO_BAG (FILTER f b) = BAG_FILTER f (LIST_TO_BAG b)

LIST_TO_BAG_EQ_EMPTY

⊢ ∀l. (LIST_TO_BAG l = {||}) ⇔ (l = [])

LIST_TO_BAG_DISTINCT

⊢ BAG_ALL_DISTINCT (LIST_TO_BAG b) ⇔ ALL_DISTINCT b

LIST_TO_BAG_APPEND

⊢ ∀l1 l2. LIST_TO_BAG (l1 ++ l2) = LIST_TO_BAG l1 ⊎ LIST_TO_BAG l2

LIST_TO_BAG_alt

⊢ ∀l x. LIST_TO_BAG l x = LENGTH (FILTER ($= x) l)

LIST_ELEM_COUNT_LIST_TO_BAG

⊢ LIST_ELEM_COUNT e ls = LIST_TO_BAG ls e

INN_LIST_TO_BAG

⊢ ∀n h l. BAG_INN h n (LIST_TO_BAG l) ⇔ LENGTH (FILTER ($= h) l) ≥ n

IN_LIST_TO_BAG

⊢ ∀h l. h ⋲ LIST_TO_BAG l ⇔ MEM h l

FINITE_LIST_TO_SET

⊢ ∀l. FINITE (LIST_TO_SET l)

FINITE_LIST_TO_BAG

⊢ FINITE_BAG (LIST_TO_BAG ls)

FINITE_BAG_OF_FMAP

⊢ ∀f b. FINITE_BAG (BAG_OF_FMAP f b)

EVERY_LIST_TO_BAG

⊢ BAG_EVERY P (LIST_TO_BAG ls) ⇔ EVERY P ls

CARD_LIST_TO_BAG

⊢ BAG_CARD (LIST_TO_BAG ls) = LENGTH ls

BAG_TO_LIST_THM

⊢ FINITE_BAG bag ⇒
  (BAG_TO_LIST bag =
   if bag = {||} then [] else BAG_CHOICE bag::BAG_TO_LIST (BAG_REST bag))

BAG_TO_LIST_INV

⊢ ∀b. FINITE_BAG b ⇒ (LIST_TO_BAG (BAG_TO_LIST b) = b)

BAG_TO_LIST_IND

⊢ ∀P.
      (∀bag. (FINITE_BAG bag ∧ bag ≠ {||} ⇒ P (BAG_REST bag)) ⇒ P bag) ⇒
      ∀v. P v

BAG_TO_LIST_EQ_NIL

⊢ FINITE_BAG b ⇒
  (([] = BAG_TO_LIST b) ⇔ (b = {||})) ∧ ((BAG_TO_LIST b = []) ⇔ (b = {||}))

BAG_TO_LIST_CARD

⊢ ∀b. FINITE_BAG b ⇒ (LENGTH (BAG_TO_LIST b) = BAG_CARD b)

BAG_OF_FMAP_THM

⊢ (∀f. BAG_OF_FMAP f FEMPTY = {||}) ∧
  ∀f b k v.
      BAG_OF_FMAP f (b |+ (k,v)) = BAG_INSERT (f k v) (BAG_OF_FMAP f (b \\ k))

BAG_IN_MEM

⊢ ∀b. FINITE_BAG b ⇒ ∀x. x ⋲ b ⇔ MEM x (BAG_TO_LIST b)

BAG_IN_BAG_OF_FMAP

⊢ ∀x f b. x ⋲ BAG_OF_FMAP f b ⇔ ∃k. k ∈ FDOM b ∧ (x = f k (b ' k))