Theory "container"

Signature

Definitions

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 bag.
        I
          (if FINITE_BAG bag then
             if bag = {||} then []
             else BAG_CHOICE bag::BAG_TO_LIST (BAG_REST bag)
           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

SET_TO_LIST_THM

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

SET_TO_LIST_IND

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

LIST_TO_SET_THM

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

SET_TO_LIST_INV

|- ∀s. FINITE s ⇒ (LIST_TO_SET (SET_TO_LIST s) = s)

SET_TO_LIST_CARD

|- ∀s. FINITE s ⇒ (LENGTH (SET_TO_LIST s) = CARD s)

SET_TO_LIST_IN_MEM

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

MEM_SET_TO_LIST

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

SET_TO_LIST_SING

|- SET_TO_LIST {x} = [x]

UNION_APPEND

|- ∀l1 l2. LIST_TO_SET l1 ∪ LIST_TO_SET l2 = LIST_TO_SET (l1 ++ l2)

LIST_TO_SET_APPEND

|- ∀l1 l2. LIST_TO_SET (l1 ++ l2) = LIST_TO_SET l1 ∪ LIST_TO_SET l2

FINITE_LIST_TO_SET

|- ∀l. FINITE (LIST_TO_SET l)

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_IND

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

BAG_TO_LIST_INV

|- ∀b. FINITE_BAG b ⇒ (LIST_TO_BAG (BAG_TO_LIST b) = b)

BAG_TO_LIST_CARD

|- ∀b. FINITE_BAG b ⇒ (LENGTH (BAG_TO_LIST b) = BAG_CARD b)

BAG_IN_MEM

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

MEM_BAG_TO_LIST

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

FINITE_LIST_TO_BAG

|- FINITE_BAG (LIST_TO_BAG ls)

EVERY_LIST_TO_BAG

|- BAG_EVERY P (LIST_TO_BAG ls) ⇔ EVERY P ls

LIST_TO_BAG_APPEND

|- ∀l1 l2. LIST_TO_BAG (l1 ++ l2) = LIST_TO_BAG l1 ⊎ LIST_TO_BAG l2

IN_LIST_TO_BAG

|- ∀h l. h ⋲ LIST_TO_BAG l ⇔ MEM h l

LIST_TO_BAG_EQ_EMPTY

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

PERM_LIST_TO_BAG

|- ∀l1 l2. (LIST_TO_BAG l1 = LIST_TO_BAG l2) ⇔ PERM l1 l2

CARD_LIST_TO_BAG

|- BAG_CARD (LIST_TO_BAG ls) = LENGTH ls

BAG_TO_LIST_EQ_NIL

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

LIST_ELEM_COUNT_LIST_TO_BAG

|- LIST_ELEM_COUNT e ls = LIST_TO_BAG ls e

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_BAG_OF_FMAP

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

FINITE_BAG_OF_FMAP

|- ∀f b. FINITE_BAG (BAG_OF_FMAP f b)