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

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)

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)

LIST_TO_BAG_alt

⊢ ∀l x. LIST_TO_BAG l x = LENGTH (FILTER ($= x) 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_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

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)

IN_LIST_TO_BAG

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

LIST_TO_BAG_DISTINCT

⊢ BAG_ALL_DISTINCT (LIST_TO_BAG b) ⇔ ALL_DISTINCT b

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_CARD

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

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

WF_mlt_list

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

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)