Theory alist

⊢ ∀k alist. ADELKEY k alist = FILTER (λp. FST p ≠ k) alist

⊢ ∀m. alist_range m = {v | ∃k. ALOOKUP m k = SOME v}

⊢ ∀s. alist_to_fmap s = FOLDR (λ(k,v) f. f⟨k ↦ v⟩) FEMPTY s

⊢ ∀s. fmap_to_alist s = MAP (λk. (k,s⟨k⟩)) (SET_TO_LIST (FDOM s))

⊢ ∀ls f x y.
    x ≠ y ⇒ ADELKEY x (AFUPDKEY y f ls) = AFUPDKEY y f (ADELKEY x ls)

⊢ ∀fd f ls. ADELKEY fd (AFUPDKEY fd f ls) = ADELKEY fd ls

⊢ ∀x ls. ADELKEY x ls = ls ⇔ ¬MEM x (MAP FST ls)

⊢ ALOOKUP (AFUPDKEY k2 f al) k1 =
  case ALOOKUP al k1 of
    NONE => NONE
  | SOME v => if k1 = k2 then SOME (f v) else SOME v

⊢ AFUPDKEY n I = I

⊢ ∀k1 k2 f1 f2 l.
    k1 ≠ k2 ⇒
    AFUPDKEY k2 f2 (AFUPDKEY k1 f1 l) = AFUPDKEY k1 f1 (AFUPDKEY k2 f2 l)

⊢ (∀k f. AFUPDKEY k f [] = []) ∧
  ∀v rest k' k f.
    AFUPDKEY k f ((k',v)::rest) =
    if k = k' then (k,f v)::rest else (k',v)::AFUPDKEY k f rest

⊢ ∀k f1 l f2.
    (∀v. ALOOKUP l k = SOME v ⇒ f1 v = f2 v) ⇒
    AFUPDKEY k f1 l = AFUPDKEY k f2 l

⊢ ∀P. (∀k f. P k f []) ∧
      (∀k f k' v rest. (k ≠ k' ⇒ P k f rest) ⇒ P k f ((k',v)::rest)) ⇒
      ∀v v1 v2. P v v1 v2

⊢ AFUPDKEY k f1 (AFUPDKEY k f2 al) = AFUPDKEY k (f1 ∘ f2) al

⊢ ∀k f alist.
    (∀v. ALOOKUP alist k = SOME v ⇒ f v = v) ⇒ AFUPDKEY k f alist = alist

⊢ ALL_DISTINCT (MAP FST ls) ⇒ (FEVERY P (alist_to_fmap ls) ⇔ EVERY P ls)

⊢ ∀fm. ALL_DISTINCT (MAP FST (fmap_to_alist fm))

⊢ ∀al. ALOOKUP (ADELKEY k1 al) k2 = if k1 = k2 then NONE else ALOOKUP al k2

⊢ ∀ls n.
    n < LENGTH ls ∧ ALL_DISTINCT (MAP FST ls) ⇒
    ALOOKUP ls (FST ls❲n❳) = SOME (SND ls❲n❳)

⊢ ALL_DISTINCT (MAP FST al) ∧ MEM (k,v) al ⇒ ALOOKUP al k = SOME v

⊢ ∀l1 l2.
    ALL_DISTINCT (MAP FST l1) ∧ PERM (MAP FST l1) (MAP FST l2) ∧
    set l1 = set l2 ⇒
    ALOOKUP l1 = ALOOKUP l2

⊢ ∀l1 l2 k.
    ALOOKUP (l1 ⧺ l2) k =
    case ALOOKUP l1 k of NONE => ALOOKUP l2 k | SOME v => SOME v

⊢ ∀l1 l2 l. ALOOKUP l1 = ALOOKUP l2 ⇒ ALOOKUP (l1 ⧺ l) = ALOOKUP (l2 ⧺ l)

⊢ FLOOKUP (alist_to_fmap al) = ALOOKUP al ∧
  ALOOKUP (fmap_to_alist fm) = FLOOKUP fm

⊢ ALOOKUP l x = NONE ⇔ ∀k v. MEM (k,v) l ⇒ k ≠ x

⊢ ∀ls x.
    ALOOKUP (FILTER (λ(k,v). P k) ls) x =
    if P x then ALOOKUP ls x else NONE

⊢ ∀ls k v. ALOOKUP ls k = SOME v ⇒ v ∈ FRANGE (alist_to_fmap ls)

⊢ ∀ls k.
    ALOOKUP ls k =
    if MEM k (MAP FST ls) then
      SOME (MAP SND ls)❲(LEAST n. (MAP FST ls)❲n❳ = k)❳
    else NONE

⊢ ∀f al. ALOOKUP (MAP (λ(x,y). (x,f y)) al) = OPTION_MAP f ∘ ALOOKUP al

⊢ ∀f al x.
    ALOOKUP (MAP (λ(x,y). (x,f x y)) al) x =
    OPTION_MAP (f x) (ALOOKUP al x)

⊢ ∀al k v. ALOOKUP al k = SOME v ⇒ MEM (k,v) al

⊢ ∀l x. ALOOKUP l x = NONE ⇔ ¬MEM x (MAP FST l)

⊢ ∀al k v. ALOOKUP al k = SOME v ⇒ (alist_to_fmap al)⟨k⟩ = v

⊢ MEM x l ⇒ ALOOKUP (MAP (λk. (k,f k)) l) x = SOME (f x)

⊢ ∀l1 l2 k f.
    LENGTH l1 = LENGTH l2 ⇒
    ALOOKUP (ZIP (l1,MAP f l2)) = OPTION_MAP f ∘ ALOOKUP (ZIP (l1,l2))

⊢ (∀q. ALOOKUP [] q = NONE) ∧
  ∀y x t q. ALOOKUP ((x,y)::t) q = if x = q then SOME y else ALOOKUP t q

⊢ ∀P. (∀q. P [] q) ∧ (∀x y t q. (x ≠ q ⇒ P t q) ⇒ P ((x,y)::t) q) ⇒
      ∀v v1. P v v1

⊢ ∀ls k ls2.
    (ALOOKUP ls k = SOME v ⇒ ALOOKUP (ls ⧺ ls2) k = SOME v) ∧
    (ALOOKUP ls k = NONE ⇒ ALOOKUP (ls ⧺ ls2) k = ALOOKUP ls2 k)

⊢ ∀al. FDOM (alist_to_fmap al) = set (MAP FST al)

⊢ EVERY P ls ⇒ FEVERY P (alist_to_fmap ls)

⊢ ∀xs k m.
    FLOOKUP (m |++ xs) k =
    case ALOOKUP (REVERSE xs) k of NONE => FLOOKUP m k | SOME x => SOME x

⊢ ALOOKUP ls k = NONE ⇒ FLOOKUP (fm |++ REVERSE ls) k = FLOOKUP fm k

⊢ ALOOKUP ls k = SOME v ⇒ FLOOKUP (fm |++ REVERSE ls) k = SOME v

⊢ FRANGE (alist_to_fmap ls) ⊆ IMAGE SND (set ls)

⊢ ∀ls fm. alist_to_fmap ls ⊌ fm = fm |++ REVERSE ls

⊢ ∀ls fm. fm |++ ls = alist_to_fmap (REVERSE ls ⧺ fmap_to_alist fm)

⊢ (∀v. MEM v (MAP SND ls) ⇒ P v) ⇒ ∀v. v ∈ FRANGE (alist_to_fmap ls) ⇒ P v

⊢ ∀ls. LENGTH (AFUPDKEY k f ls) = LENGTH ls

⊢ ∀fm. LENGTH (fmap_to_alist fm) = CARD (FDOM fm)

⊢ MAP FST (AFUPDKEY f k alist) = MAP FST alist

⊢ ∀fm. MAP_KEYS I fm = fm

⊢ ∀f fm.
    MAP (λ(k,v). (k,f v)) (fmap_to_alist fm) = fmap_to_alist (f o_f fm)

⊢ ∀al. MEM (k1,v) (ADELKEY k2 al) ⇔ k1 ≠ k2 ∧ MEM (k1,v) al

⊢ MEM (x,y) (fmap_to_alist fm) ⇔ x ∈ FDOM fm ∧ fm⟨x⟩ = y

⊢ ∀p fm. MEM p (fmap_to_alist fm) ⇔ FLOOKUP fm (FST p) = SOME (SND p)

⊢ ∀x y fm. MEM (x,y) (fmap_to_alist fm) ⇔ FLOOKUP fm x = SOME y

⊢ PERM (fmap_to_alist fm1) (fmap_to_alist fm2) ⇔ fm1 = fm2

⊢ ∀l1 l2. alist_to_fmap (l1 ⧺ l2) = alist_to_fmap l1 ⊌ alist_to_fmap l2

⊢ ∀al z. z ∈ FDOM (alist_to_fmap al) ⇒ MEM (z,(alist_to_fmap al)⟨z⟩) al

⊢ ∀f1 f2 al.
    INJ f1 (set (MAP FST al)) 𝕌(:β) ⇒
    alist_to_fmap (MAP (λ(x,y). (f1 x,f2 y)) al) =
    MAP_KEYS f1 (f2 o_f alist_to_fmap al)

⊢ ∀f1 f2 al mal v.
    INJ f1 (set (MAP FST al)) 𝕌(:β) ∧ mal = MAP (λ(x,y). (f1 x,f2 y)) al ∧
    v = MAP_KEYS f1 (f2 o_f alist_to_fmap al) ⇒
    alist_to_fmap mal = v

⊢ ∀f al. alist_to_fmap (MAP (λ(k,v). (k,f v)) al) = f o_f alist_to_fmap al

⊢ ∀l1 l2.
    PERM l1 l2 ∧ ALL_DISTINCT (MAP FST l1) ⇒
    alist_to_fmap l1 = alist_to_fmap l2

⊢ ∀ls l1 l2.
    alist_to_fmap l1 = alist_to_fmap l2 ⇒
    alist_to_fmap (ls ⧺ l1) = alist_to_fmap (ls ⧺ l2)

⊢ alist_to_fmap [] = FEMPTY ∧
  alist_to_fmap ((k,v)::t) = (alist_to_fmap t)⟨k ↦ v⟩

⊢ ∀al.
    fmap_to_alist (alist_to_fmap al) =
    MAP (λk. (k,THE (ALOOKUP al k))) (SET_TO_LIST (set (MAP FST al)))

⊢ ∀al.
    ALL_DISTINCT (MAP FST al) ⇒ PERM (fmap_to_alist (alist_to_fmap al)) al

⊢ ∀l k. ALL_DISTINCT (MAP FST l) ⇒ ALOOKUP (REVERSE l) k = ALOOKUP l k

⊢ ∀f l x. ALOOKUP l x = ALOOKUP (FILTER (λ(x',y). x = x') l) x

⊢ ∀R sort x l.
    transitive R ∧ total R ∧ STABLE sort (inv_image R FST) ⇒
    ALOOKUP (sort (inv_image R FST) l) x = ALOOKUP l x

⊢ ∀l k m.
    FLOOKUP (m |++ l) k =
    case ALOOKUP (REVERSE l) k of NONE => FLOOKUP m k | SOME v => SOME v

⊢ fmap_to_alist FEMPTY = []

⊢ ∀f1 f2. fmap_to_alist f1 = fmap_to_alist f2 ⇒ f1 = f2

⊢ ∀fm1 fm2.
    FDOM fm1 = FDOM fm2 ⇒
    MAP FST (fmap_to_alist fm1) = MAP FST (fmap_to_alist fm2)

⊢ alist_to_fmap (fmap_to_alist fm) = fm

⊢ ∀m l. m |++ l = FEMPTY |++ l ⊌ m

⊢ ∀x y l.
    ALL_DISTINCT (MAP FST l) ∧ MEM (x,y) l ⇒
    FLOOKUP (FEMPTY |++ l) x = SOME y

⊢ set (MAP FST (fmap_to_alist fm)) = FDOM fm