Theory "alist"

Signature

Definitions

fmap_to_alist_def

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

alist_to_fmap_def

⊢ ∀s. alist_to_fmap s = FOLDR (λ(k,v) f. f |+ (k,v)) FEMPTY s

alist_range_def

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

Theorems

fmap_to_alist_FEMPTY

⊢ fmap_to_alist FEMPTY = []

alist_to_fmap_thm

⊢ alist_to_fmap [] = FEMPTY ∧
  alist_to_fmap ((k,v)::t) = alist_to_fmap t |+ (k,v)

ALOOKUP_ind

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

ALOOKUP_def

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

ALOOKUP_FAILS

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

ALOOKUP_NONE

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

ALOOKUP_TABULATE

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

ALOOKUP_EQ_FLOOKUP

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

MEM_fmap_to_alist

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

MEM_fmap_to_alist_FLOOKUP

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

MEM_pair_fmap_to_alist_FLOOKUP

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

LENGTH_fmap_to_alist

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

fmap_to_alist_to_fmap

⊢ alist_to_fmap (fmap_to_alist fm) = fm

ALOOKUP_MEM

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

ALOOKUP_SOME_FAPPLY_alist_to_fmap

⊢ ∀al k v. ALOOKUP al k = SOME v ⇒ alist_to_fmap al ' k = v

alist_to_fmap_FAPPLY_MEM

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

ALOOKUP_MAP

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

FDOM_alist_to_fmap

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

alist_to_fmap_prefix

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

alist_to_fmap_APPEND

⊢ ∀l1 l2. alist_to_fmap (l1 ++ l2) = alist_to_fmap l1 FUNION alist_to_fmap l2

ALOOKUP_prefix

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

ALOOKUP_APPEND

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

FUPDATE_LIST_EQ_APPEND_REVERSE

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

FLOOKUP_FUPDATE_LIST_ALOOKUP_SOME

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

FLOOKUP_FUPDATE_LIST_ALOOKUP_NONE

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

FUNION_alist_to_fmap

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

alist_to_fmap_MAP

⊢ ∀f1 f2 al.
      INJ f1 (LIST_TO_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)

alist_to_fmap_to_alist

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

alist_to_fmap_to_alist_PERM

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

ALOOKUP_LEAST_EL

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

ALOOKUP_ALL_DISTINCT_MEM

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

ALL_DISTINCT_fmap_to_alist_keys

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

fmap_to_alist_inj

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

fmap_to_alist_preserves_FDOM

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

PERM_fmap_to_alist

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

alist_to_fmap_PERM

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

ALOOKUP_ALL_DISTINCT_EL

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

ALOOKUP_ZIP_MAP_SND

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

ALOOKUP_FILTER

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

ALOOKUP_APPEND_same

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

ALOOKUP_IN_FRANGE

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

FRANGE_alist_to_fmap_SUBSET

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

IN_FRANGE_alist_to_fmap_suff

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

alist_to_fmap_MAP_matchable

⊢ ∀f1 f2 al mal v.
      INJ f1 (LIST_TO_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

MAP_values_fmap_to_alist

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

MAP_KEYS_I

⊢ ∀fm. MAP_KEYS I fm = fm

alist_to_fmap_MAP_values

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

set_MAP_FST_fmap_to_alist

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

alookup_distinct_reverse

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

flookup_fupdate_list

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

fupdate_list_funion

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

mem_to_flookup

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

alookup_filter

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

alookup_stable_sorted

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

ALOOKUP_ALL_DISTINCT_PERM_same

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