- 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 o 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 ⊌ 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 ⊌ 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 o 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 ⊌ 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)