Theory "finite_map"

Signature

Definitions

DRESTRICT_DEF

⊢ ∀f r.
    (FDOM (DRESTRICT f r) = FDOM f ∩ r) ∧
    ∀x. DRESTRICT f r ' x = if x ∈ FDOM f ∩ r then f ' x else FEMPTY ' x

FAPPLY_DEF

⊢ ∀f x. f ' x = OUTL (fmap_REP f x)

FCARD_DEF

⊢ ∀fm. FCARD fm = CARD (FDOM fm)

FDIFF_def

⊢ ∀f1 s. FDIFF f1 s = DRESTRICT f1 (COMPL s)

FDOM_DEF

⊢ ∀f x. FDOM f x ⇔ ISL (fmap_REP f x)

FEMPTY_DEF

⊢ FEMPTY = fmap_ABS (λa. INR ())

FEVERY_DEF

⊢ ∀P f. FEVERY P f ⇔ ∀x. x ∈ FDOM f ⇒ P (x,f ' x)

FLOOKUP_DEF

⊢ ∀f x. FLOOKUP f x = if x ∈ FDOM f then SOME (f ' x) else NONE

FMAP_MAP2_def

⊢ ∀f m. FMAP_MAP2 f m = FUN_FMAP (λx. f (x,m ' x)) (FDOM m)

FMERGE_DEF

⊢ ∀m f g.
    (FDOM (FMERGE m f g) = FDOM f ∪ FDOM g) ∧
    ∀x. FMERGE m f g ' x =
        if x ∉ FDOM f then g ' x
        else if x ∉ FDOM g then f ' x
        else m (f ' x) (g ' x)

FRANGE_DEF

⊢ ∀f. FRANGE f = {y | ∃x. x ∈ FDOM f ∧ (f ' x = y)}

FUNION_DEF

⊢ ∀f g.
    (FDOM (f FUNION g) = FDOM f ∪ FDOM g) ∧
    ∀x. (f FUNION g) ' x = if x ∈ FDOM f then f ' x else g ' x

FUN_FMAP_DEF

⊢ ∀f P.
    FINITE P ⇒
    (FDOM (FUN_FMAP f P) = P) ∧ ∀x. x ∈ P ⇒ (FUN_FMAP f P ' x = f x)

FUPDATE_DEF

⊢ ∀f x y. f |+ (x,y) = fmap_ABS (λa. if a = x then INL y else fmap_REP f a)

FUPDATE_LIST

⊢ $|++ = FOLDL $|+

ITFMAPR_def

⊢ ITFMAPR =
  (λf a0 a1 a2.
       ∀ITFMAPR'.
         (∀a0 a1 a2.
            (a0 = FEMPTY) ∧ (a2 = a1) ∨
            (∃A2 k v fm.
               (a0 = fm |+ (k,v)) ∧ (a2 = f k v A2) ∧ k ∉ FDOM fm ∧
               ITFMAPR' fm a1 A2) ⇒
            ITFMAPR' a0 a1 a2) ⇒
         ITFMAPR' a0 a1 a2)

ITFMAP_def

⊢ ∀f fm A0. ITFMAP f fm A0 = @A. ITFMAPR f fm A0 A

MAP_KEYS_def

⊢ ∀f fm.
    (FDOM (MAP_KEYS f fm) = IMAGE f (FDOM fm)) ∧
    (INJ f (FDOM fm) 𝕌(:β) ⇒
     ∀x. x ∈ FDOM fm ⇒ (MAP_KEYS f fm ' (f x) = fm ' x))

RRESTRICT_DEF

⊢ ∀f r.
    (FDOM (RRESTRICT f r) = {x | x ∈ FDOM f ∧ f ' x ∈ r}) ∧
    ∀x. RRESTRICT f r ' x =
        if x ∈ FDOM f ∧ f ' x ∈ r then f ' x else FEMPTY ' x

SUBMAP_DEF

⊢ ∀f g. f ⊑ g ⇔ ∀x. x ∈ FDOM f ⇒ x ∈ FDOM g ∧ (f ' x = g ' x)

f_o_DEF

⊢ ∀f g. f f_o g = f f_o_f FUN_FMAP g {x | g x ∈ FDOM f}

f_o_f_DEF

⊢ ∀f g.
    (FDOM (f f_o_f g) = FDOM g ∩ {x | g ' x ∈ FDOM f}) ∧
    ∀x. x ∈ FDOM (f f_o_f g) ⇒ ((f f_o_f g) ' x = f ' (g ' x))

fmap_EQ_UPTO_def

⊢ ∀f1 f2 vs.
    fmap_EQ_UPTO f1 f2 vs ⇔
    (FDOM f1 ∩ COMPL vs = FDOM f2 ∩ COMPL vs) ∧
    ∀x. x ∈ FDOM f1 ∩ COMPL vs ⇒ (f1 ' x = f2 ' x)

fmap_ISO_DEF

⊢ (∀a. fmap_ABS (fmap_REP a) = a) ∧
  ∀r. is_fmap r ⇔ (fmap_REP (fmap_ABS r) = r)

fmap_TY_DEF

⊢ ∃rep. TYPE_DEFINITION is_fmap rep

fmap_domsub

⊢ ∀fm k. fm \\ k = DRESTRICT fm (COMPL {k})

fmap_inverse_def

⊢ ∀m1 m2.
    fmap_inverse m1 m2 ⇔
    ∀k. k ∈ FDOM m1 ⇒ ∃v. (FLOOKUP m1 k = SOME v) ∧ (FLOOKUP m2 v = SOME k)

fmap_rel_def

⊢ ∀R f1 f2.
    fmap_rel R f1 f2 ⇔
    (FDOM f2 = FDOM f1) ∧ ∀x. x ∈ FDOM f1 ⇒ R (f1 ' x) (f2 ' x)

fmap_size_def

⊢ ∀kz vz fm. fmap_size kz vz fm = ∑ (λk. kz k + vz (fm ' k)) (FDOM fm)

fmlfpR_def

⊢ fmlfpR =
  (λf fm0 a0 a1 a2 a3.
       ∀fmlfpR'.
         (∀a0 a1 a2 a3.
            (a1 = FEMPTY) ∧ (a3 = a0) ∧ (a0 = a2) ∨
            (a1 = FEMPTY) ∧ fmlfpR' a2 fm0 a2 a3 ∧ a0 ≠ a2 ∨
            (∃fm k v. (a1 = fm |+ (k,v)) ∧ fmlfpR' a0 (fm \\ k) (f k v a2) a3) ⇒
            fmlfpR' a0 a1 a2 a3) ⇒
         fmlfpR' a0 a1 a2 a3)

fp_soluble_def

⊢ ∀R P fm f.
    fp_soluble R P fm f ⇔
    transitive R ∧ WF (lbound P Rᵀ) ∧
    (∀k v A.
       (FLOOKUP fm k = SOME v) ∧ RC R A P ⇒
       RC R A (f k v A) ∧ RC R (f k v A) P) ∧
    ∀A. R A P ⇒ ∃k v. (FLOOKUP fm k = SOME v) ∧ f k v A ≠ A

is_fmap_def

⊢ is_fmap =
  (λa0.
       ∀is_fmap'.
         (∀a0.
            (a0 = (λa. INR ())) ∨
            (∃f a b. (a0 = (λx. if x = a then INL b else f x)) ∧ is_fmap' f) ⇒
            is_fmap' a0) ⇒
         is_fmap' a0)

lbound_def

⊢ ∀l R x y. lbound l R x y ⇔ R꙳ l x ∧ R꙳ l y ∧ R x y

o_f_DEF

⊢ ∀f g.
    (FDOM (f o_f g) = FDOM g) ∧
    ∀x. x ∈ FDOM (f o_f g) ⇒ ((f o_f g) ' x = f (g ' x))

Theorems

DISJOINT_FEVERY_FUNION

⊢ DISJOINT (FDOM m1) (FDOM m2) ⇒
  (FEVERY P (m1 FUNION m2) ⇔ FEVERY P m1 ∧ FEVERY P m2)

DOMSUB_COMMUTES

⊢ fm \\ k1 \\ k2 = fm \\ k2 \\ k1

DOMSUB_FAPPLY

⊢ ∀fm k. (fm \\ k) ' k = FEMPTY ' k

DOMSUB_FAPPLY_NEQ

⊢ ∀fm k1 k2. k1 ≠ k2 ⇒ ((fm \\ k1) ' k2 = fm ' k2)

DOMSUB_FAPPLY_THM

⊢ ∀fm k1 k2. (fm \\ k1) ' k2 = if k1 = k2 then FEMPTY ' k2 else fm ' k2

DOMSUB_FEMPTY

⊢ ∀k. FEMPTY \\ k = FEMPTY

DOMSUB_FLOOKUP

⊢ ∀fm k. FLOOKUP (fm \\ k) k = NONE

DOMSUB_FLOOKUP_NEQ

⊢ ∀fm k1 k2. k1 ≠ k2 ⇒ (FLOOKUP (fm \\ k1) k2 = FLOOKUP fm k2)

DOMSUB_FLOOKUP_THM

⊢ ∀fm k1 k2. FLOOKUP (fm \\ k1) k2 = if k1 = k2 then NONE else FLOOKUP fm k2

DOMSUB_FUNION

⊢ (f FUNION g) \\ k = f \\ k FUNION g \\ k

DOMSUB_FUPDATE

⊢ ∀fm k v. fm |+ (k,v) \\ k = fm \\ k

DOMSUB_FUPDATE_NEQ

⊢ ∀fm k1 k2 v. k1 ≠ k2 ⇒ (fm |+ (k1,v) \\ k2 = fm \\ k2 |+ (k1,v))

DOMSUB_FUPDATE_THM

⊢ ∀fm k1 k2 v.
    fm |+ (k1,v) \\ k2 = if k1 = k2 then fm \\ k2 else fm \\ k2 |+ (k1,v)

DOMSUB_IDEM

⊢ fm \\ k \\ k = fm \\ k

DOMSUB_MAP_KEYS

⊢ BIJ f 𝕌(:α) 𝕌(:β) ⇒ (MAP_KEYS f fm \\ f s = MAP_KEYS f (fm \\ s))

DOMSUB_NOT_IN_DOM

⊢ k ∉ FDOM fm ⇒ (fm \\ k = fm)

DOMSUB_SUBMAP

⊢ ∀f g x. f ⊑ g ∧ x ∉ FDOM f ⇒ f ⊑ g \\ x

DRESTRICTED_FUNION

⊢ ∀f1 f2 s.
    DRESTRICT (f1 FUNION f2) s =
    DRESTRICT f1 s FUNION DRESTRICT f2 (s DIFF FDOM f1)

DRESTRICT_DOMSUB

⊢ ∀f s k. DRESTRICT f s \\ k = DRESTRICT f (s DELETE k)

DRESTRICT_DRESTRICT

⊢ ∀f P Q. DRESTRICT (DRESTRICT f P) Q = DRESTRICT f (P ∩ Q)

DRESTRICT_EQ_DRESTRICT

⊢ ∀f1 f2 s1 s2.
    (DRESTRICT f1 s1 = DRESTRICT f2 s2) ⇔
    DRESTRICT f1 s1 ⊑ f2 ∧ DRESTRICT f2 s2 ⊑ f1 ∧
    (s1 ∩ FDOM f1 = s2 ∩ FDOM f2)

DRESTRICT_EQ_DRESTRICT_SAME

⊢ (DRESTRICT f1 s = DRESTRICT f2 s) ⇔
  (s ∩ FDOM f1 = s ∩ FDOM f2) ∧ ∀x. x ∈ FDOM f1 ∧ x ∈ s ⇒ (f1 ' x = f2 ' x)

DRESTRICT_EQ_FUNION

⊢ ∀h h1 h2.
    DISJOINT (FDOM h1) (FDOM h2) ∧ (h1 FUNION h2 = h) ⇒
    (h2 = DRESTRICT h (COMPL (FDOM h1)))

DRESTRICT_FDOM

⊢ ∀f. DRESTRICT f (FDOM f) = f

DRESTRICT_FEMPTY

⊢ ∀r. DRESTRICT FEMPTY r = FEMPTY

DRESTRICT_FUNION

⊢ ∀h s1 s2. DRESTRICT h s1 FUNION DRESTRICT h s2 = DRESTRICT h (s1 ∪ s2)

DRESTRICT_FUNION_DRESTRICT_COMPL

⊢ DRESTRICT f s FUNION DRESTRICT f (COMPL s) = f

DRESTRICT_FUNION_SAME

⊢ ∀fm s. DRESTRICT fm s FUNION fm = fm

DRESTRICT_FUNION_SUBSET

⊢ s2 ⊆ s1 ⇒ ∃h. DRESTRICT f s1 FUNION g = DRESTRICT f s2 FUNION h

DRESTRICT_FUPDATE

⊢ ∀f r x y.
    DRESTRICT (f |+ (x,y)) r =
    if x ∈ r then DRESTRICT f r |+ (x,y) else DRESTRICT f r

DRESTRICT_IDEMPOT

⊢ ∀s vs. DRESTRICT (DRESTRICT s vs) vs = DRESTRICT s vs

DRESTRICT_IS_FEMPTY

⊢ ∀f. DRESTRICT f ∅ = FEMPTY

DRESTRICT_MAP_KEYS_IMAGE

⊢ INJ f 𝕌(:α) 𝕌(:β) ⇒
  (DRESTRICT (MAP_KEYS f fm) (IMAGE f s) = MAP_KEYS f (DRESTRICT fm s))

DRESTRICT_SUBMAP

⊢ ∀f r. DRESTRICT f r ⊑ f

DRESTRICT_SUBMAP_gen

⊢ f ⊑ g ⇒ DRESTRICT f P ⊑ g

DRESTRICT_SUBSET

⊢ ∀f1 f2 s t.
    (DRESTRICT f1 s = DRESTRICT f2 s) ∧ t ⊆ s ⇒
    (DRESTRICT f1 t = DRESTRICT f2 t)

DRESTRICT_SUBSET_SUBMAP

⊢ s1 ⊆ s2 ⇒ DRESTRICT f s1 ⊑ DRESTRICT f s2

DRESTRICT_SUBSET_SUBMAP_gen

⊢ ∀f1 f2 s t.
    DRESTRICT f1 s ⊑ DRESTRICT f2 s ∧ t ⊆ s ⇒ DRESTRICT f1 t ⊑ DRESTRICT f2 t

DRESTRICT_UNIV

⊢ ∀f. DRESTRICT f 𝕌(:α) = f

EQ_FDOM_SUBMAP

⊢ (f = g) ⇔ f ⊑ g ∧ (FDOM f = FDOM g)

FAPPLY_FUPDATE

⊢ ∀f x y. (f |+ (x,y)) ' x = y

FAPPLY_FUPDATE_THM

⊢ ∀f a b x. (f |+ (a,b)) ' x = if x = a then b else f ' x

FAPPLY_f_o

⊢ ∀f g.
    FINITE {x | g x ∈ FDOM f} ⇒
    ∀x. x ∈ FDOM (f f_o g) ⇒ ((f f_o g) ' x = f ' (g x))

FCARD_0_FEMPTY

⊢ ∀f. (FCARD f = 0) ⇔ (f = FEMPTY)

FCARD_FEMPTY

⊢ FCARD FEMPTY = 0

FCARD_FUPDATE

⊢ ∀fm a b.
    FCARD (fm |+ (a,b)) = if a ∈ FDOM fm then FCARD fm else 1 + FCARD fm

FCARD_SUC

⊢ ∀f n.
    (FCARD f = SUC n) ⇔
    ∃f' x y. x ∉ FDOM f' ∧ (FCARD f' = n) ∧ (f = f' |+ (x,y))

FDOM_DOMSUB

⊢ ∀fm k. FDOM (fm \\ k) = FDOM fm DELETE k

FDOM_DRESTRICT

⊢ ∀f r x. FDOM (DRESTRICT f r) = FDOM f ∩ r

FDOM_EQ_EMPTY

⊢ ∀f. (FDOM f = ∅) ⇔ (f = FEMPTY)

FDOM_EQ_EMPTY_SYM

⊢ ∀f. (∅ = FDOM f) ⇔ (f = FEMPTY)

FDOM_EQ_FDOM_FUPDATE

⊢ ∀f x. x ∈ FDOM f ⇒ ∀y. FDOM (f |+ (x,y)) = FDOM f

FDOM_FDIFF

⊢ x ∈ FDOM (FDIFF refs f2) ⇔ x ∈ FDOM refs ∧ x ∉ f2

FDOM_FEMPTY

⊢ FDOM FEMPTY = ∅

FDOM_FINITE

⊢ ∀fm. FINITE (FDOM fm)

FDOM_FMAP

⊢ ∀f s. FINITE s ⇒ (FDOM (FUN_FMAP f s) = s)

FDOM_FMERGE

⊢ ∀m f g. FDOM (FMERGE m f g) = FDOM f ∪ FDOM g

FDOM_FOLDR_DOMSUB

⊢ ∀ls fm. FDOM (FOLDR (λk m. m \\ k) fm ls) = FDOM fm DIFF LIST_TO_SET ls

FDOM_FUNION

⊢ FDOM (f FUNION g) = FDOM f ∪ FDOM g

FDOM_FUPDATE

⊢ ∀f a b. FDOM (f |+ (a,b)) = a INSERT FDOM f

FDOM_FUPDATE_LIST

⊢ ∀kvl fm. FDOM (fm |++ kvl) = FDOM fm ∪ LIST_TO_SET (MAP FST kvl)

FDOM_F_FEMPTY1

⊢ ∀f. (∀a. a ∉ FDOM f) ⇔ (f = FEMPTY)

FDOM_f_o

⊢ ∀f g. FINITE {x | g x ∈ FDOM f} ⇒ (FDOM (f f_o g) = {x | g x ∈ FDOM f})

FDOM_o_f

⊢ ∀f g. FDOM (f o_f g) = FDOM g

FEMPTY_FUPDATE_EQ

⊢ ∀x y. (FEMPTY |+ x = FEMPTY |+ y) ⇔ (x = y)

FEMPTY_SUBMAP

⊢ ∀h. h ⊑ FEMPTY ⇔ (h = FEMPTY)

FEVERY_ALL_FLOOKUP

⊢ ∀P f. FEVERY P f ⇔ ∀k v. (FLOOKUP f k = SOME v) ⇒ P (k,v)

FEVERY_DRESTRICT_COMPL

⊢ FEVERY P (DRESTRICT (f |+ (k,v)) (COMPL s)) ⇔
  (k ∉ s ⇒ P (k,v)) ∧ FEVERY P (DRESTRICT f (COMPL (k INSERT s)))

FEVERY_FEMPTY

⊢ ∀P. FEVERY P FEMPTY

FEVERY_FLOOKUP

⊢ FEVERY P f ∧ (FLOOKUP f k = SOME v) ⇒ P (k,v)

FEVERY_FUPDATE

⊢ ∀P f x y.
    FEVERY P (f |+ (x,y)) ⇔ P (x,y) ∧ FEVERY P (DRESTRICT f (COMPL {x}))

FEVERY_FUPDATE_LIST

⊢ ALL_DISTINCT (MAP FST kvl) ⇒
  (FEVERY P (fm |++ kvl) ⇔
   EVERY P kvl ∧ FEVERY P (DRESTRICT fm (COMPL (LIST_TO_SET (MAP FST kvl)))))

FEVERY_STRENGTHEN_THM

⊢ FEVERY P FEMPTY ∧ (FEVERY P f ∧ P (x,y) ⇒ FEVERY P (f |+ (x,y)))

FEVERY_SUBMAP

⊢ FEVERY P fm ∧ fm0 ⊑ fm ⇒ FEVERY P fm0

FEVERY_o_f

⊢ ∀m P f. FEVERY P (f o_f m) ⇔ FEVERY (λx. P (FST x,f (SND x))) m

FINITE_FRANGE

⊢ ∀fm. FINITE (FRANGE fm)

FINITE_PRED_11

⊢ ∀g. (∀x y. (g x = g y) ⇔ (x = y)) ⇒ ∀f. FINITE {x | g x ∈ FDOM f}

FLOOKUP_DRESTRICT

⊢ ∀fm s k. FLOOKUP (DRESTRICT fm s) k = if k ∈ s then FLOOKUP fm k else NONE

FLOOKUP_EMPTY

⊢ FLOOKUP FEMPTY k = NONE

FLOOKUP_EXT

⊢ (f1 = f2) ⇔ (FLOOKUP f1 = FLOOKUP f2)

FLOOKUP_FOLDR_UPDATE

⊢ ALL_DISTINCT (MAP FST kvl) ∧ DISJOINT (LIST_TO_SET (MAP FST kvl)) (FDOM fm) ⇒
  ((FLOOKUP (FOLDR (flip $|+) fm kvl) k = SOME v) ⇔
   MEM (k,v) kvl ∨ (FLOOKUP fm k = SOME v))

FLOOKUP_FUNION

⊢ FLOOKUP (f1 FUNION f2) k =
  case FLOOKUP f1 k of NONE => FLOOKUP f2 k | SOME v => SOME v

FLOOKUP_FUN_FMAP

⊢ FINITE P ⇒ (FLOOKUP (FUN_FMAP f P) k = if k ∈ P then SOME (f k) else NONE)

FLOOKUP_MAP_KEYS

⊢ INJ f (FDOM m) 𝕌(:β) ⇒
  (FLOOKUP (MAP_KEYS f m) k =
   OPTION_BIND (some x. (k = f x) ∧ x ∈ FDOM m) (FLOOKUP m))

FLOOKUP_MAP_KEYS_MAPPED

⊢ INJ f 𝕌(:α) 𝕌(:β) ⇒ (FLOOKUP (MAP_KEYS f m) (f k) = FLOOKUP m k)

FLOOKUP_SUBMAP

⊢ f ⊑ g ∧ (FLOOKUP f k = SOME v) ⇒ (FLOOKUP g k = SOME v)

FLOOKUP_UPDATE

⊢ FLOOKUP (fm |+ (k1,v)) k2 = if k1 = k2 then SOME v else FLOOKUP fm k2

FLOOKUP_o_f

⊢ FLOOKUP (f o_f fm) k =
  case FLOOKUP fm k of NONE => NONE | SOME v => SOME (f v)

FMAP_MAP2_FEMPTY

⊢ FMAP_MAP2 f FEMPTY = FEMPTY

FMAP_MAP2_FUPDATE

⊢ FMAP_MAP2 f (m |+ (x,v)) = FMAP_MAP2 f m |+ (x,f (x,v))

FMAP_MAP2_THM

⊢ (FDOM (FMAP_MAP2 f m) = FDOM m) ∧
  ∀x. x ∈ FDOM m ⇒ (FMAP_MAP2 f m ' x = f (x,m ' x))

FMEQ_ENUMERATE_CASES

⊢ ∀f1 kvl p. (f1 |+ p = FEMPTY |++ kvl) ⇒ MEM p kvl

FMEQ_SINGLE_SIMPLE_DISJ_ELIM

⊢ ∀fm k v ck cv.
    (fm |+ (k,v) = FEMPTY |+ (ck,cv)) ⇔
    (k = ck) ∧ (v = cv) ∧ ((fm = FEMPTY) ∨ ∃v'. fm = FEMPTY |+ (k,v'))

FMEQ_SINGLE_SIMPLE_ELIM

⊢ ∀P k v ck cv nv.
    (∃fm. (fm |+ (k,v) = FEMPTY |+ (ck,cv)) ∧ P (fm |+ (k,nv))) ⇔
    (k = ck) ∧ (v = cv) ∧ P (FEMPTY |+ (ck,nv))

FMERGE_ASSOC

⊢ ASSOC (FMERGE m) ⇔ ASSOC m

FMERGE_COMM

⊢ COMM (FMERGE m) ⇔ COMM m

FMERGE_DOMSUB

⊢ ∀m m1 m2 k. FMERGE m m1 m2 \\ k = FMERGE m (m1 \\ k) (m2 \\ k)

FMERGE_DRESTRICT

⊢ DRESTRICT (FMERGE f st1 st2) vs =
  FMERGE f (DRESTRICT st1 vs) (DRESTRICT st2 vs)

FMERGE_EQ_FEMPTY

⊢ (FMERGE m f g = FEMPTY) ⇔ (f = FEMPTY) ∧ (g = FEMPTY)

FMERGE_FEMPTY

⊢ (FMERGE m f FEMPTY = f) ∧ (FMERGE m FEMPTY f = f)

FMERGE_FUNION

⊢ $FUNION = FMERGE (λx y. x)

FMERGE_NO_CHANGE

⊢ ((FMERGE m f1 f2 = f1) ⇔
   ∀x. x ∈ FDOM f2 ⇒ x ∈ FDOM f1 ∧ (m (f1 ' x) (f2 ' x) = f1 ' x)) ∧
  ((FMERGE m f1 f2 = f2) ⇔
   ∀x. x ∈ FDOM f1 ⇒ x ∈ FDOM f2 ∧ (m (f1 ' x) (f2 ' x) = f2 ' x))

FM_PULL_APART

⊢ ∀fm k. k ∈ FDOM fm ⇒ ∃fm0 v. (fm = fm0 |+ (k,v)) ∧ k ∉ FDOM fm0

FOLDL2_FUPDATE_LIST

⊢ ∀f1 f2 bs cs a.
    (LENGTH bs = LENGTH cs) ⇒
    (FOLDL2 (λfm b c. fm |+ (f1 b c,f2 b c)) a bs cs =
     a |++ ZIP (MAP2 f1 bs cs,MAP2 f2 bs cs))

FOLDL2_FUPDATE_LIST_paired

⊢ ∀f1 f2 bs cs a.
    (LENGTH bs = LENGTH cs) ⇒
    (FOLDL2 (λfm b (c,d). fm |+ (f1 b c d,f2 b c d)) a bs cs =
     a |++ ZIP (MAP2 (λb. (f1 b)ᴾ) bs cs,MAP2 (λb. (f2 b)ᴾ) bs cs))

FOLDL_FUPDATE_LIST

⊢ ∀f1 f2 ls a.
    FOLDL (λfm k. fm |+ (f1 k,f2 k)) a ls = a |++ MAP (λk. (f1 k,f2 k)) ls

FRANGE_DOMSUB_SUBSET

⊢ FRANGE (fm \\ k) ⊆ FRANGE fm

FRANGE_DRESTRICT_SUBSET

⊢ FRANGE (DRESTRICT fm s) ⊆ FRANGE fm

FRANGE_FEMPTY

⊢ FRANGE FEMPTY = ∅

FRANGE_FLOOKUP

⊢ v ∈ FRANGE f ⇔ ∃k. FLOOKUP f k = SOME v

FRANGE_FMAP

⊢ FINITE P ⇒ (FRANGE (FUN_FMAP f P) = IMAGE f P)

FRANGE_FUNION

⊢ DISJOINT (FDOM fm1) (FDOM fm2) ⇒
  (FRANGE (fm1 FUNION fm2) = FRANGE fm1 ∪ FRANGE fm2)

FRANGE_FUNION_SUBSET

⊢ FRANGE (f1 FUNION f2) ⊆ FRANGE f1 ∪ FRANGE f2

FRANGE_FUPDATE

⊢ ∀f x y. FRANGE (f |+ (x,y)) = y INSERT FRANGE (DRESTRICT f (COMPL {x}))

FRANGE_FUPDATE_DOMSUB

⊢ ∀fm k v. FRANGE (fm |+ (k,v)) = v INSERT FRANGE (fm \\ k)

FRANGE_FUPDATE_LIST_SUBSET

⊢ ∀ls fm. FRANGE (fm |++ ls) ⊆ FRANGE fm ∪ LIST_TO_SET (MAP SND ls)

FRANGE_FUPDATE_SUBSET

⊢ FRANGE (fm |+ kv) ⊆ FRANGE fm ∪ {SND kv}

FUNION_ASSOC

⊢ ∀f g h. f FUNION (g FUNION h) = f FUNION g FUNION h

FUNION_COMM

⊢ ∀f g. DISJOINT (FDOM f) (FDOM g) ⇒ (f FUNION g = g FUNION f)

FUNION_EQ

⊢ ∀f1 f2 f3.
    DISJOINT (FDOM f1) (FDOM f2) ∧ DISJOINT (FDOM f1) (FDOM f3) ⇒
    ((f1 FUNION f2 = f1 FUNION f3) ⇔ (f2 = f3))

FUNION_EQ_FEMPTY

⊢ ∀h1 h2. (h1 FUNION h2 = FEMPTY) ⇔ (h1 = FEMPTY) ∧ (h2 = FEMPTY)

FUNION_EQ_IMPL

⊢ ∀f1 f2 f3.
    DISJOINT (FDOM f1) (FDOM f2) ∧ DISJOINT (FDOM f1) (FDOM f3) ∧ (f2 = f3) ⇒
    (f1 FUNION f2 = f1 FUNION f3)

FUNION_FEMPTY_1

⊢ ∀g. FEMPTY FUNION g = g

FUNION_FEMPTY_2

⊢ ∀f. f FUNION FEMPTY = f

FUNION_FMERGE

⊢ ∀f1 f2 m. DISJOINT (FDOM f1) (FDOM f2) ⇒ (FMERGE m f1 f2 = f1 FUNION f2)

FUNION_FUPDATE_1

⊢ ∀f g x y. f |+ (x,y) FUNION g = (f FUNION g) |+ (x,y)

FUNION_FUPDATE_2

⊢ ∀f g x y.
    f FUNION g |+ (x,y) =
    if x ∈ FDOM f then f FUNION g else (f FUNION g) |+ (x,y)

FUNION_IDEMPOT

⊢ fm FUNION fm = fm

FUN_FMAP_EMPTY

⊢ FUN_FMAP f ∅ = FEMPTY

FUPD11_SAME_BASE

⊢ ∀f k1 v1 k2 v2.
    (f |+ (k1,v1) = f |+ (k2,v2)) ⇔
    (k1 = k2) ∧ (v1 = v2) ∨
    k1 ≠ k2 ∧ k1 ∈ FDOM f ∧ k2 ∈ FDOM f ∧ (f |+ (k1,v1) = f) ∧
    (f |+ (k2,v2) = f)

FUPD11_SAME_KEY_AND_BASE

⊢ ∀f k v1 v2. (f |+ (k,v1) = f |+ (k,v2)) ⇔ (v1 = v2)

FUPD11_SAME_NEW_KEY

⊢ ∀f1 f2 k v1 v2.
    k ∉ FDOM f1 ∧ k ∉ FDOM f2 ⇒
    ((f1 |+ (k,v1) = f2 |+ (k,v2)) ⇔ (f1 = f2) ∧ (v1 = v2))

FUPD11_SAME_UPDATE

⊢ ∀f1 f2 k v.
    (f1 |+ (k,v) = f2 |+ (k,v)) ⇔
    (DRESTRICT f1 (COMPL {k}) = DRESTRICT f2 (COMPL {k}))

FUPDATE_COMMUTES

⊢ ∀f a b c d. a ≠ c ⇒ (f |+ (a,b) |+ (c,d) = f |+ (c,d) |+ (a,b))

FUPDATE_DRESTRICT

⊢ ∀f x y. f |+ (x,y) = DRESTRICT f (COMPL {x}) |+ (x,y)

FUPDATE_ELIM

⊢ ∀k v f. k ∈ FDOM f ∧ (f ' k = v) ⇒ (f |+ (k,v) = f)

FUPDATE_EQ

⊢ ∀f a b c. f |+ (a,b) |+ (a,c) = f |+ (a,c)

FUPDATE_EQ_FUNION

⊢ ∀fm kv. fm |+ kv = FEMPTY |+ kv FUNION fm

FUPDATE_EQ_FUPDATE_LIST

⊢ ∀fm kv. fm |+ kv = fm |++ [kv]

FUPDATE_FUPDATE_LIST_COMMUTES

⊢ ¬MEM k (MAP FST kvl) ⇒ (fm |+ (k,v) |++ kvl = (fm |++ kvl) |+ (k,v))

FUPDATE_FUPDATE_LIST_MEM

⊢ MEM k (MAP FST kvl) ⇒ (fm |+ (k,v) |++ kvl = fm |++ kvl)

FUPDATE_LIST_ALL_DISTINCT_APPLY_MEM

⊢ ∀P ls k v fm.
    ALL_DISTINCT (MAP FST ls) ∧ MEM (k,v) ls ∧ P v ⇒ P ((fm |++ ls) ' k)

FUPDATE_LIST_ALL_DISTINCT_PERM

⊢ ∀ls ls' fm.
    ALL_DISTINCT (MAP FST ls) ∧ PERM ls ls' ⇒ (fm |++ ls = fm |++ ls')

FUPDATE_LIST_ALL_DISTINCT_REVERSE

⊢ ∀ls. ALL_DISTINCT (MAP FST ls) ⇒ ∀fm. fm |++ REVERSE ls = fm |++ ls

FUPDATE_LIST_APPEND

⊢ fm |++ (kvl1 ++ kvl2) = fm |++ kvl1 |++ kvl2

FUPDATE_LIST_APPEND_COMMUTES

⊢ ∀l1 l2 fm.
    DISJOINT (LIST_TO_SET (MAP FST l1)) (LIST_TO_SET (MAP FST l2)) ⇒
    (fm |++ l1 |++ l2 = fm |++ l2 |++ l1)

FUPDATE_LIST_APPLY_HO_THM

⊢ ∀P f kvl k.
    (∃n. n < LENGTH kvl ∧ (k = EL n (MAP FST kvl)) ∧ P (EL n (MAP SND kvl)) ∧
         ∀m. n < m ∧ m < LENGTH kvl ⇒ EL m (MAP FST kvl) ≠ k) ∨
    ¬MEM k (MAP FST kvl) ∧ P (f ' k) ⇒
    P ((f |++ kvl) ' k)

FUPDATE_LIST_APPLY_MEM

⊢ ∀kvl f k v n.
    n < LENGTH kvl ∧ (k = EL n (MAP FST kvl)) ∧ (v = EL n (MAP SND kvl)) ∧
    (∀m. n < m ∧ m < LENGTH kvl ⇒ EL m (MAP FST kvl) ≠ k) ⇒
    ((f |++ kvl) ' k = v)

FUPDATE_LIST_APPLY_NOT_MEM

⊢ ∀kvl f k. ¬MEM k (MAP FST kvl) ⇒ ((f |++ kvl) ' k = f ' k)

FUPDATE_LIST_APPLY_NOT_MEM_matchable

⊢ ∀kvl f k v. ¬MEM k (MAP FST kvl) ∧ (v = f ' k) ⇒ ((f |++ kvl) ' k = v)

FUPDATE_LIST_CANCEL

⊢ ∀ls1 fm ls2.
    (∀k. MEM k (MAP FST ls1) ⇒ MEM k (MAP FST ls2)) ⇒
    (fm |++ ls1 |++ ls2 = fm |++ ls2)

FUPDATE_LIST_EQ_FEMPTY

⊢ ∀fm ls. (fm |++ ls = FEMPTY) ⇔ (fm = FEMPTY) ∧ (ls = [])

FUPDATE_LIST_SAME_KEYS_UNWIND

⊢ ∀f1 f2 kvl1 kvl2.
    (f1 |++ kvl1 = f2 |++ kvl2) ∧ (MAP FST kvl1 = MAP FST kvl2) ∧
    ALL_DISTINCT (MAP FST kvl1) ⇒
    (kvl1 = kvl2) ∧
    ∀kvl. (MAP FST kvl = MAP FST kvl1) ⇒ (f1 |++ kvl = f2 |++ kvl)

FUPDATE_LIST_SAME_UPDATE

⊢ ∀kvl f1 f2.
    (f1 |++ kvl = f2 |++ kvl) ⇔
    (DRESTRICT f1 (COMPL (LIST_TO_SET (MAP FST kvl))) =
     DRESTRICT f2 (COMPL (LIST_TO_SET (MAP FST kvl))))

FUPDATE_LIST_SNOC

⊢ ∀xs x fm. fm |++ SNOC x xs = (fm |++ xs) |+ x

FUPDATE_LIST_THM

⊢ ∀f. (f |++ [] = f) ∧ ∀h t. f |++ (h::t) = f |+ h |++ t

FUPDATE_PURGE

⊢ ∀f x y. f |+ (x,y) = f \\ x |+ (x,y)

FUPDATE_PURGE'

⊢ ∀f x y. f \\ x |+ (x,y) = f |+ (x,y)

FUPDATE_SAME_APPLY

⊢ (x = FST kv) ∨ (fm1 ' x = fm2 ' x) ⇒ ((fm1 |+ kv) ' x = (fm2 |+ kv) ' x)

FUPDATE_SAME_LIST_APPLY

⊢ ∀kvl fm1 fm2 x.
    MEM x (MAP FST kvl) ⇒ ((fm1 |++ kvl) ' x = (fm2 |++ kvl) ' x)

FUPD_SAME_KEY_UNWIND

⊢ ∀f1 f2 k v1 v2.
    (f1 |+ (k,v1) = f2 |+ (k,v2)) ⇒ (v1 = v2) ∧ ∀v. f1 |+ (k,v) = f2 |+ (k,v)

IMAGE_FRANGE

⊢ ∀f fm. IMAGE f (FRANGE fm) = FRANGE (f o_f fm)

IN_FDOM_FOLDR_UNION

⊢ ∀x hL. x ∈ FDOM (FOLDR $FUNION FEMPTY hL) ⇔ ∃h. MEM h hL ∧ x ∈ FDOM h

IN_FRANGE

⊢ ∀f v. v ∈ FRANGE f ⇔ ∃k. k ∈ FDOM f ∧ (f ' k = v)

IN_FRANGE_DOMSUB_suff

⊢ (∀v. v ∈ FRANGE fm ⇒ P v) ⇒ ∀v. v ∈ FRANGE (fm \\ k) ⇒ P v

IN_FRANGE_DRESTRICT_suff

⊢ (∀v. v ∈ FRANGE fm ⇒ P v) ⇒ ∀v. v ∈ FRANGE (DRESTRICT fm s) ⇒ P v

IN_FRANGE_FLOOKUP

⊢ ∀f v. v ∈ FRANGE f ⇔ ∃k. FLOOKUP f k = SOME v

IN_FRANGE_FUNION_suff

⊢ (∀v. v ∈ FRANGE f1 ⇒ P v) ∧ (∀v. v ∈ FRANGE f2 ⇒ P v) ⇒
  ∀v. v ∈ FRANGE (f1 FUNION f2) ⇒ P v

IN_FRANGE_FUPDATE_LIST_suff

⊢ (∀v. v ∈ FRANGE fm ⇒ P v) ∧ (∀v. MEM v (MAP SND ls) ⇒ P v) ⇒
  ∀v. v ∈ FRANGE (fm |++ ls) ⇒ P v

IN_FRANGE_FUPDATE_suff

⊢ (∀v. v ∈ FRANGE fm ⇒ P v) ∧ P (SND kv) ⇒ ∀v. v ∈ FRANGE (fm |+ kv) ⇒ P v

IN_FRANGE_o_f_suff

⊢ (∀v. v ∈ FRANGE fm ⇒ P (f v)) ⇒ ∀v. v ∈ FRANGE (f o_f fm) ⇒ P v

ITFMAPR_FEMPTY

⊢ ITFMAPR f FEMPTY A1 A2 ⇔ (A1 = A2)

ITFMAPR_cases

⊢ ∀f a0 a1 a2.
    ITFMAPR f a0 a1 a2 ⇔
    (a0 = FEMPTY) ∧ (a2 = a1) ∨
    ∃A2 k v fm.
      (a0 = fm |+ (k,v)) ∧ (a2 = f k v A2) ∧ k ∉ FDOM fm ∧ ITFMAPR f fm a1 A2

ITFMAPR_ind

⊢ ∀f ITFMAPR'.
    (∀A. ITFMAPR' FEMPTY A A) ∧
    (∀A1 A2 k v fm.
       k ∉ FDOM fm ∧ ITFMAPR' fm A1 A2 ⇒ ITFMAPR' (fm |+ (k,v)) A1 (f k v A2)) ⇒
    ∀a0 a1 a2. ITFMAPR f a0 a1 a2 ⇒ ITFMAPR' a0 a1 a2

ITFMAPR_rules

⊢ ∀f. (∀A. ITFMAPR f FEMPTY A A) ∧
      ∀A1 A2 k v fm.
        k ∉ FDOM fm ∧ ITFMAPR f fm A1 A2 ⇒
        ITFMAPR f (fm |+ (k,v)) A1 (f k v A2)

ITFMAPR_strongind

⊢ ∀f ITFMAPR'.
    (∀A. ITFMAPR' FEMPTY A A) ∧
    (∀A1 A2 k v fm.
       k ∉ FDOM fm ∧ ITFMAPR f fm A1 A2 ∧ ITFMAPR' fm A1 A2 ⇒
       ITFMAPR' (fm |+ (k,v)) A1 (f k v A2)) ⇒
    ∀a0 a1 a2. ITFMAPR f a0 a1 a2 ⇒ ITFMAPR' a0 a1 a2

ITFMAPR_total

⊢ ∀fm r0. ∃r. ITFMAPR f fm r0 r

ITFMAPR_unique

⊢ (∀k1 k2 v1 v2 A. f k1 v1 (f k2 v2 A) = f k2 v2 (f k1 v1 A)) ⇒
  ∀fm A0 A1 A2. ITFMAPR f fm A0 A1 ∧ ITFMAPR f fm A0 A2 ⇒ (A1 = A2)

ITFMAP_FEMPTY

⊢ ITFMAP f FEMPTY A = A

ITFMAP_thm

⊢ (ITFMAP f FEMPTY A = A) ∧
  ((∀k1 k2 v1 v2 A. f k1 v1 (f k2 v2 A) = f k2 v2 (f k1 v1 A)) ⇒
   (ITFMAP f (fm |+ (k,v)) A = f k v (ITFMAP f (fm \\ k) A)))

LEAST_NOTIN_FDOM

⊢ (LEAST ptr. ptr ∉ FDOM refs) ∉ FDOM refs

MAP_KEYS_BIJ_LINV

⊢ f PERMUTES 𝕌(:num) ⇒ (MAP_KEYS f (MAP_KEYS (LINV f 𝕌(:num)) t) = t)

MAP_KEYS_FEMPTY

⊢ ∀f. MAP_KEYS f FEMPTY = FEMPTY

MAP_KEYS_FUPDATE

⊢ ∀f fm k v.
    INJ f (k INSERT FDOM fm) 𝕌(:β) ⇒
    (MAP_KEYS f (fm |+ (k,v)) = MAP_KEYS f fm |+ (f k,v))

MAP_KEYS_using_LINV

⊢ ∀f fm.
    INJ f (FDOM fm) 𝕌(:β) ⇒
    (MAP_KEYS f fm = fm f_o_f FUN_FMAP (LINV f (FDOM fm)) (IMAGE f (FDOM fm)))

MAP_KEYS_witness

⊢ let
    m f fm =
      if INJ f (FDOM fm) 𝕌(:β) then
        fm f_o_f FUN_FMAP (LINV f (FDOM fm)) (IMAGE f (FDOM fm))
      else FUN_FMAP ARB (IMAGE f (FDOM fm))
  in
    ∀f fm.
      (FDOM (m f fm) = IMAGE f (FDOM fm)) ∧
      (INJ f (FDOM fm) 𝕌(:β) ⇒ ∀x. x ∈ FDOM fm ⇒ (m f fm ' (f x) = fm ' x))

NOT_EQ_FAPPLY

⊢ ∀f a x y. a ≠ x ⇒ ((f |+ (x,y)) ' a = f ' a)

NOT_EQ_FEMPTY_FUPDATE

⊢ ∀f a b. FEMPTY ≠ f |+ (a,b)

NOT_FDOM_DRESTRICT

⊢ ∀f x. x ∉ FDOM f ⇒ (DRESTRICT f (COMPL {x}) = f)

NOT_FDOM_FAPPLY_FEMPTY

⊢ ∀f x. x ∉ FDOM f ⇒ (f ' x = FEMPTY ' x)

NUM_NOT_IN_FDOM

⊢ ∃x. x ∉ FDOM f

RRESTRICT_FEMPTY

⊢ ∀r. RRESTRICT FEMPTY r = FEMPTY

RRESTRICT_FUPDATE

⊢ ∀f r x y.
    RRESTRICT (f |+ (x,y)) r =
    if y ∈ r then RRESTRICT f r |+ (x,y)
    else RRESTRICT (DRESTRICT f (COMPL {x})) r

SAME_KEY_UPDATES_DIFFER

⊢ ∀f1 f2 k v1 v2. v1 ≠ v2 ⇒ f1 |+ (k,v1) ≠ f2 |+ (k,v2)

STRONG_DRESTRICT_FUPDATE

⊢ ∀f r x y.
    x ∈ r ⇒ (DRESTRICT (f |+ (x,y)) r = DRESTRICT f (r DELETE x) |+ (x,y))

STRONG_DRESTRICT_FUPDATE_THM

⊢ ∀f r x y.
    DRESTRICT (f |+ (x,y)) r =
    if x ∈ r then DRESTRICT f (COMPL {x} ∩ r) |+ (x,y)
    else DRESTRICT f (COMPL {x} ∩ r)

SUBMAP_ANTISYM

⊢ ∀f g. f ⊑ g ∧ g ⊑ f ⇔ (f = g)

SUBMAP_DOMSUB

⊢ f \\ k ⊑ f

SUBMAP_DOMSUB_gen

⊢ ∀f g k. f \\ k ⊑ g ⇔ f \\ k ⊑ g \\ k

SUBMAP_DRESTRICT

⊢ DRESTRICT f P ⊑ f

SUBMAP_DRESTRICT_MONOTONE

⊢ f1 ⊑ f2 ∧ s1 ⊆ s2 ⇒ DRESTRICT f1 s1 ⊑ DRESTRICT f2 s2

SUBMAP_FDOM_SUBSET

⊢ f1 ⊑ f2 ⇒ FDOM f1 ⊆ FDOM f2

SUBMAP_FEMPTY

⊢ ∀f. FEMPTY ⊑ f

SUBMAP_FLOOKUP_EQN

⊢ f ⊑ g ⇔ ∀x y. (FLOOKUP f x = SOME y) ⇒ (FLOOKUP g x = SOME y)

SUBMAP_FRANGE

⊢ ∀f g. f ⊑ g ⇒ FRANGE f ⊆ FRANGE g

SUBMAP_FUNION

⊢ ∀f1 f2 f3.
    f1 ⊑ f2 ∨ DISJOINT (FDOM f1) (FDOM f2) ∧ f1 ⊑ f3 ⇒ f1 ⊑ f2 FUNION f3

SUBMAP_FUNION_ABSORPTION

⊢ ∀f g. f ⊑ g ⇔ (f FUNION g = g)

SUBMAP_FUNION_EQ

⊢ (∀f1 f2 f3. DISJOINT (FDOM f1) (FDOM f2) ⇒ (f1 ⊑ f2 FUNION f3 ⇔ f1 ⊑ f3)) ∧
  ∀f1 f2 f3.
    DISJOINT (FDOM f1) (FDOM f3 DIFF FDOM f2) ⇒ (f1 ⊑ f2 FUNION f3 ⇔ f1 ⊑ f2)

SUBMAP_FUNION_ID

⊢ (∀f1 f2. f1 ⊑ f1 FUNION f2) ∧
  ∀f1 f2. DISJOINT (FDOM f1) (FDOM f2) ⇒ f2 ⊑ f1 FUNION f2

SUBMAP_FUPDATE

⊢ ∀f g x y. f |+ (x,y) ⊑ g ⇔ x ∈ FDOM g ∧ (g ' x = y) ∧ f \\ x ⊑ g \\ x

SUBMAP_FUPDATE_EQN

⊢ f ⊑ f |+ (x,y) ⇔ x ∉ FDOM f ∨ (f ' x = y) ∧ x ∈ FDOM f

SUBMAP_FUPDATE_FLOOKUP

⊢ f ⊑ f |+ (x,y) ⇔ (FLOOKUP f x = NONE) ∨ (FLOOKUP f x = SOME y)

SUBMAP_REFL

⊢ ∀f. f ⊑ f

SUBMAP_TRANS

⊢ ∀f g h. f ⊑ g ∧ g ⊑ h ⇒ f ⊑ h

SUBMAP_mono_FUPDATE

⊢ ∀f g x y. f \\ x ⊑ g \\ x ⇒ f |+ (x,y) ⊑ g |+ (x,y)

WF_lbound_inv_SUBSET

⊢ FINITE s ⇒ WF (lbound s $PSUBSETᵀ)

disjoint_drestrict

⊢ ∀s m. DISJOINT s (FDOM m) ⇒ (DRESTRICT m (COMPL s) = m)

drestrict_iter_list

⊢ ∀m l. FOLDR (λk m. m \\ k) m l = DRESTRICT m (COMPL (LIST_TO_SET l))

f_o_ASSOC

⊢ (∀x y. (g x = g y) ⇔ (x = y)) ∧ (∀x y. (h x = h y) ⇔ (x = y)) ⇒
  ((f f_o g) f_o h = f f_o g ∘ h)

f_o_FEMPTY

⊢ ∀g. FEMPTY f_o g = FEMPTY

f_o_FUPDATE

⊢ ∀fm k v g.
    FINITE {x | g x ∈ FDOM fm} ∧ FINITE {x | g x = k} ⇒
    ((fm |+ (k,v)) f_o g =
     FMERGE (flip K) (fm f_o g) (FUN_FMAP (K v) {x | g x = k}))

f_o_f_FEMPTY_1

⊢ ∀f. FEMPTY f_o_f f = FEMPTY

f_o_f_FEMPTY_2

⊢ ∀f. f f_o_f FEMPTY = FEMPTY

f_o_f_FUPDATE_compose

⊢ ∀f1 f2 k x v.
    x ∉ FDOM f1 ∧ x ∉ FRANGE f2 ⇒
    ((f1 |+ (x,v)) f_o_f (f2 |+ (k,x)) = f1 f_o_f f2 |+ (k,v))

fdom_fupdate_list2

⊢ ∀kvl fm.
    FDOM (fm |++ kvl) =
    FDOM fm DIFF LIST_TO_SET (MAP FST kvl) ∪ LIST_TO_SET (MAP FST kvl)

fevery_funion

⊢ ∀P m1 m2. FEVERY P m1 ∧ FEVERY P m2 ⇒ FEVERY P (m1 FUNION m2)

flookup_thm

⊢ ∀f x v.
    ((FLOOKUP f x = NONE) ⇔ x ∉ FDOM f) ∧
    ((FLOOKUP f x = SOME v) ⇔ x ∈ FDOM f ∧ (f ' x = v))

fmap_CASES

⊢ ∀f. (f = FEMPTY) ∨ ∃g x y. f = g |+ (x,y)

fmap_EQ

⊢ ∀f g. (FDOM f = FDOM g) ∧ ($' f = $' g) ⇔ (f = g)

fmap_EQ_THM

⊢ ∀f g. (FDOM f = FDOM g) ∧ (∀x. x ∈ FDOM f ⇒ (f ' x = g ' x)) ⇔ (f = g)

fmap_EQ_UPTO___EMPTY

⊢ ∀f1 f2. fmap_EQ_UPTO f1 f2 ∅ ⇔ (f1 = f2)

fmap_EQ_UPTO___EQ

⊢ ∀vs f. fmap_EQ_UPTO f f vs

fmap_EQ_UPTO___FUPDATE_BOTH

⊢ ∀f1 f2 ks k v.
    fmap_EQ_UPTO f1 f2 ks ⇒
    fmap_EQ_UPTO (f1 |+ (k,v)) (f2 |+ (k,v)) (ks DELETE k)

fmap_EQ_UPTO___FUPDATE_BOTH___NO_DELETE

⊢ ∀f1 f2 ks k v.
    fmap_EQ_UPTO f1 f2 ks ⇒ fmap_EQ_UPTO (f1 |+ (k,v)) (f2 |+ (k,v)) ks

fmap_EQ_UPTO___FUPDATE_SING

⊢ ∀f1 f2 ks k v.
    fmap_EQ_UPTO f1 f2 ks ⇒ fmap_EQ_UPTO (f1 |+ (k,v)) f2 (k INSERT ks)

fmap_EXT

⊢ ∀f g. (f = g) ⇔ (FDOM f = FDOM g) ∧ ∀x. x ∈ FDOM f ⇒ (f ' x = g ' x)

fmap_INDUCT

⊢ ∀P. P FEMPTY ∧ (∀f. P f ⇒ ∀x y. x ∉ FDOM f ⇒ P (f |+ (x,y))) ⇒ ∀f. P f

fmap_SIMPLE_INDUCT

⊢ ∀P. P FEMPTY ∧ (∀f. P f ⇒ ∀x y. P (f |+ (x,y))) ⇒ ∀f. P f

fmap_cases_NOTIN

⊢ ∀fm. (fm = FEMPTY) ∨ ∃k v fm0. k ∉ FDOM fm0 ∧ (fm = fm0 |+ (k,v))

fmap_eq_flookup

⊢ (f1 = f2) ⇔ ∀x. FLOOKUP f1 x = FLOOKUP f2 x

fmap_rel_FEMPTY

⊢ fmap_rel R FEMPTY FEMPTY

fmap_rel_FEMPTY2

⊢ (fmap_rel R FEMPTY f ⇔ (f = FEMPTY)) ∧ (fmap_rel R f FEMPTY ⇔ (f = FEMPTY))

fmap_rel_FLOOKUP_imp

⊢ fmap_rel R f1 f2 ⇒
  (∀k. (FLOOKUP f1 k = NONE) ⇒ (FLOOKUP f2 k = NONE)) ∧
  ∀k v1. (FLOOKUP f1 k = SOME v1) ⇒ ∃v2. (FLOOKUP f2 k = SOME v2) ∧ R v1 v2

fmap_rel_FUNION_rels

⊢ fmap_rel R f1 f2 ∧ fmap_rel R f3 f4 ⇒
  fmap_rel R (f1 FUNION f3) (f2 FUNION f4)

fmap_rel_FUPDATE_I

⊢ fmap_rel R (f1 \\ k) (f2 \\ k) ∧ R v1 v2 ⇒
  fmap_rel R (f1 |+ (k,v1)) (f2 |+ (k,v2))

fmap_rel_FUPDATE_LIST_same

⊢ ∀R ls1 ls2 f1 f2.
    fmap_rel R f1 f2 ∧ (MAP FST ls1 = MAP FST ls2) ∧
    LIST_REL R (MAP SND ls1) (MAP SND ls2) ⇒
    fmap_rel R (f1 |++ ls1) (f2 |++ ls2)

fmap_rel_FUPDATE_same

⊢ fmap_rel R f1 f2 ∧ R v1 v2 ⇒ fmap_rel R (f1 |+ (k,v1)) (f2 |+ (k,v2))

fmap_rel_OPTREL_FLOOKUP

⊢ fmap_rel R f1 f2 ⇔ ∀k. OPTREL R (FLOOKUP f1 k) (FLOOKUP f2 k)

fmap_rel_mono

⊢ (∀x y. R1 x y ⇒ R2 x y) ⇒ fmap_rel R1 f1 f2 ⇒ fmap_rel R2 f1 f2

fmap_rel_refl

⊢ (∀x. R x x) ⇒ fmap_rel R x x

fmap_rel_sym

⊢ (∀x y. R x y ⇒ R y x) ⇒ ∀x y. fmap_rel R x y ⇒ fmap_rel R y x

fmap_rel_trans

⊢ (∀x y z. R x y ∧ R y z ⇒ R x z) ⇒
  ∀x y z. fmap_rel R x y ∧ fmap_rel R y z ⇒ fmap_rel R x z

fmap_to_list

⊢ ∀m. ∃l. ALL_DISTINCT (MAP FST l) ∧ (m = FEMPTY |++ l)

fmlfpR_cases

⊢ ∀f fm0 a0 a1 a2 a3.
    fmlfpR f fm0 a0 a1 a2 a3 ⇔
    (a1 = FEMPTY) ∧ (a3 = a0) ∧ (a0 = a2) ∨
    (a1 = FEMPTY) ∧ fmlfpR f fm0 a2 fm0 a2 a3 ∧ a0 ≠ a2 ∨
    ∃fm k v. (a1 = fm |+ (k,v)) ∧ fmlfpR f fm0 a0 (fm \\ k) (f k v a2) a3

fmlfpR_ind

⊢ ∀f fm0 fmlfpR'.
    (∀A0 A1. (A0 = A1) ⇒ fmlfpR' A0 FEMPTY A1 A0) ∧
    (∀A0 A1 A2. fmlfpR' A1 fm0 A1 A2 ∧ A0 ≠ A1 ⇒ fmlfpR' A0 FEMPTY A1 A2) ∧
    (∀A0 A1 A2 fm k v.
       fmlfpR' A0 (fm \\ k) (f k v A1) A2 ⇒ fmlfpR' A0 (fm |+ (k,v)) A1 A2) ⇒
    ∀a0 a1 a2 a3. fmlfpR f fm0 a0 a1 a2 a3 ⇒ fmlfpR' a0 a1 a2 a3

fmlfpR_lastpass

⊢ (∀k v. (FLOOKUP fm k = SOME v) ⇒ (f k v A = A)) ⇒
  (fmlfpR f fm A fm A B ⇔ (A = B))

fmlfpR_rules

⊢ ∀f fm0.
    (∀A0 A1. (A0 = A1) ⇒ fmlfpR f fm0 A0 FEMPTY A1 A0) ∧
    (∀A0 A1 A2.
       fmlfpR f fm0 A1 fm0 A1 A2 ∧ A0 ≠ A1 ⇒ fmlfpR f fm0 A0 FEMPTY A1 A2) ∧
    ∀A0 A1 A2 fm k v.
      fmlfpR f fm0 A0 (fm \\ k) (f k v A1) A2 ⇒
      fmlfpR f fm0 A0 (fm |+ (k,v)) A1 A2

fmlfpR_strongind

⊢ ∀f fm0 fmlfpR'.
    (∀A0 A1. (A0 = A1) ⇒ fmlfpR' A0 FEMPTY A1 A0) ∧
    (∀A0 A1 A2.
       fmlfpR f fm0 A1 fm0 A1 A2 ∧ fmlfpR' A1 fm0 A1 A2 ∧ A0 ≠ A1 ⇒
       fmlfpR' A0 FEMPTY A1 A2) ∧
    (∀A0 A1 A2 fm k v.
       fmlfpR f fm0 A0 (fm \\ k) (f k v A1) A2 ∧
       fmlfpR' A0 (fm \\ k) (f k v A1) A2 ⇒
       fmlfpR' A0 (fm |+ (k,v)) A1 A2) ⇒
    ∀a0 a1 a2 a3. fmlfpR f fm0 a0 a1 a2 a3 ⇒ fmlfpR' a0 a1 a2 a3

fmlfpR_total

⊢ ∀fm f R P A2 A0.
    fp_soluble R P fm f ⇒ RC R A0 P ⇒ (fmlfpR f fm A0 fm A0 A2 ⇔ (A2 = P))

fmlfpR_total_lemma

⊢ fp_soluble R P fm0 f ⇒
  RC R A0 A1 ∧ RC R A1 P ∧ fm ⊑ fm0 ∧ (A1 = FOLDR fᴾ A0 kvl) ∧
  DISJOINT (LIST_TO_SET (MAP FST kvl)) (FDOM fm) ∧
  ALL_DISTINCT (MAP FST kvl) ∧ (fm0 = FOLDR (flip $|+) fm kvl) ⇒
  (fmlfpR f fm0 A0 fm A1 A2 ⇔ (A2 = P))

fp_soluble_FOLDR1

⊢ fp_soluble R P fm0 f ∧ (fm0 = FOLDR (flip $|+) fm kvl) ∧
  DISJOINT (LIST_TO_SET (MAP FST kvl)) (FDOM fm) ∧ ALL_DISTINCT (MAP FST kvl) ⇒
  (∀s A.
     IS_SUFFIX kvl s ∧ RC R A P ⇒
     RC R A (FOLDR fᴾ A s) ∧ RC R (FOLDR fᴾ A s) P) ∧
  ∀s A k v.
    IS_SUFFIX kvl s ∧ RC R A P ∧ MEM (k,v) s ∧ f k v A ≠ A ⇒ FOLDR fᴾ A s ≠ A

fupdate_list_foldl

⊢ ∀m l. FOLDL (λenv (k,v). env |+ (k,v)) m l = m |++ l

fupdate_list_foldr

⊢ ∀m l. FOLDR (λ(k,v) env. env |+ (k,v)) m l = m |++ REVERSE l

fupdate_list_map

⊢ ∀l f x y.
    x ∈ FDOM (FEMPTY |++ l) ⇒
    ((FEMPTY |++ MAP (λ(a,b). (a,f b)) l) ' x = f ((FEMPTY |++ l) ' x))

is_fmap_cases

⊢ ∀a0.
    is_fmap a0 ⇔
    (a0 = (λa. INR ())) ∨
    ∃f a b. (a0 = (λx. if x = a then INL b else f x)) ∧ is_fmap f

is_fmap_ind

⊢ ∀is_fmap'.
    is_fmap' (λa. INR ()) ∧
    (∀f a b. is_fmap' f ⇒ is_fmap' (λx. if x = a then INL b else f x)) ⇒
    ∀a0. is_fmap a0 ⇒ is_fmap' a0

is_fmap_rules

⊢ is_fmap (λa. INR ()) ∧
  ∀f a b. is_fmap f ⇒ is_fmap (λx. if x = a then INL b else f x)

is_fmap_strongind

⊢ ∀is_fmap'.
    is_fmap' (λa. INR ()) ∧
    (∀f a b.
       is_fmap f ∧ is_fmap' f ⇒ is_fmap' (λx. if x = a then INL b else f x)) ⇒
    ∀a0. is_fmap a0 ⇒ is_fmap' a0

o_f_DOMSUB

⊢ g o_f fm \\ k = g o_f (fm \\ k)

o_f_FAPPLY

⊢ ∀f g x. x ∈ FDOM g ⇒ ((f o_f g) ' x = f (g ' x))

o_f_FDOM

⊢ ∀f g. FDOM g = FDOM (f o_f g)

o_f_FEMPTY

⊢ f o_f FEMPTY = FEMPTY

o_f_FRANGE

⊢ x ∈ FRANGE g ⇒ f x ∈ FRANGE (f o_f g)

o_f_FUNION

⊢ f o_f (f1 FUNION f2) = f o_f f1 FUNION f o_f f2

o_f_FUPDATE

⊢ f o_f (fm |+ (k,v)) = f o_f fm |+ (k,f v)

o_f_cong

⊢ ∀f fm f' fm'.
    (fm = fm') ∧ (∀v. v ∈ FRANGE fm ⇒ (f v = f' v)) ⇒ (f o_f fm = f' o_f fm')

o_f_id

⊢ ∀m. (λx. x) o_f m = m

o_f_o_f

⊢ f o_f g o_f h = (f ∘ g) o_f h