Theory container

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

⊢ 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))

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

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

⊢ ∀x f b. x ⋲ BAG_OF_FMAP f b ⇔ ∃k. k ∈ FDOM b ∧ x = f k b⟨k⟩

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

⊢ (∀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))

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

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

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

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

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

⊢ BAG_CARD (LIST_TO_BAG ls) = LENGTH ls

⊢ BAG_EVERY P (LIST_TO_BAG ls) ⇔ EVERY P ls

⊢ ∀f b. FINITE_BAG (BAG_OF_FMAP f b)

⊢ FINITE_BAG (LIST_TO_BAG ls)

⊢ ∀l. FINITE (set l)

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

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

⊢ LIST_ELEM_COUNT e ls = LIST_TO_BAG ls e

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

⊢ BAG_ALL_DISTINCT (LIST_TO_BAG b) ⇔ ALL_DISTINCT b

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

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

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

⊢ ∀s. FINITE s ⇒ LIST_TO_BAG (SET_TO_LIST s) = BAG_OF_SET s

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

⊢ ∀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)

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

⊢ ∀l1 l2. set (l1 ⧺ l2) = set l1 ∪ set l2

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

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

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

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

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

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

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

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

⊢ SET_TO_LIST {x} = [x]

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

⊢ ∀l1 l2. set l1 ∪ set l2 = set (l1 ⧺ l2)

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