Theory: finite_map

Parents

• one
• numeral
• pair
• sum

Types

• fmap(Arity = 2)

Constants

• FEMPTY  :'a |-> 'b
• FUNION  :('a |-> 'b) -> ('a |-> 'b) -> ('a |-> 'b)
• FUN_FMAP  :('a -> 'b) -> ('a -> bool) -> ('a |-> 'b)
• f_o  :('b |-> 'c) -> ('a -> 'b) -> ('a |-> 'c)
• FINITE_PRED  :('a -> bool) -> bool
• fmap_ABS  :('a -> 'b + one) -> ('a |-> 'b)
• FUPDATE  :('a |-> 'b) -> 'a # 'b -> ('a |-> 'b)
• o_f  :('b -> 'c) -> ('a |-> 'b) -> ('a |-> 'c)
• rep  :('a |-> 'b) -> 'a -> 'b + one
• FEVERY  :('a # 'b -> bool) -> ('a |-> 'b) -> bool
• f_o_f  :('b |-> 'c) -> ('a |-> 'b) -> ('a |-> 'c)
• FRANGE  :('a |-> 'b) -> 'b -> bool
• fmap_REP  :('a |-> 'b) -> 'a -> 'b + one
• SUBMAP  :('a |-> 'b) -> ('a |-> 'b) -> bool
• RRESTRICT  :('a |-> 'b) -> ('b -> bool) -> ('a |-> 'b)
• DRESTRICT  :('a |-> 'b) -> ('a -> bool) -> ('a |-> 'b)
• FDOMDEL  :('a -> bool) -> 'a -> 'a -> bool
• FAPPLY  :('a |-> 'b) -> 'a -> 'b
• is_fmap  :('a -> 'b + one) -> bool
• FLOOKUP  :('a |-> 'b) -> 'a -> 'b + one
• FCARD  :('a |-> 'b) -> num
• FDOM  :('a |-> 'b) -> 'a -> bool

Definitions

DRESTRICT_DEF

|- !f r.
     (!x. FDOM (DRESTRICT f r) x = FDOM f x /\ r x) /\
     !x.
       FAPPLY (DRESTRICT f r) x =
       (if FDOM f x /\ r x then FAPPLY f x else FAPPLY FEMPTY x)

f_o_DEF

|- !f g. f f_o g = f f_o_f FUN_FMAP g (\x. FDOM f (g x))

f_o_f_DEF

|- !f g.
     (!x. FDOM (f f_o_f g) x = FDOM g x /\ FDOM f (FAPPLY g x)) /\
     !x. FDOM (f f_o_f g) x ==> (FAPPLY (f f_o_f g) x = FAPPLY f (FAPPLY g x))

FAPPLY_DEF

|- !f x. FAPPLY f x = OUTL (fmap_REP f x)

FCARD_DEF

|- (FCARD FEMPTY = 0) /\
   !f x y.
     FCARD (FUPDATE f (x,y)) = (if FDOM f x then FCARD f else SUC (FCARD f))

FDOM_DEF

|- !f x. FDOM f x = ISL (fmap_REP f x)

FDOMDEL_DEF

|- !d x a. FDOMDEL d x a = d a /\ ~(a = x)

FEMPTY_DEF

|- FEMPTY = fmap_ABS (\a. INR one)

FEVERY_DEF

|- !P f. FEVERY P f = !x. FDOM f x ==> P (x,FAPPLY f x)

FINITE_PRED

|- FINITE_PRED =
   (\a0.
      !FINITE_PRED'.
        (!a0.
           (a0 = (\a. F)) \/
           (?f a. (a0 = (\x. (x = a) \/ f x)) /\ FINITE_PRED' f) ==>
           FINITE_PRED' a0) ==>
        FINITE_PRED' a0)

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'

FRANGE_DEF

|- !f y. FRANGE f y = ?x. FDOM f x /\ (FAPPLY f x = y)

FUN_FMAP_DEF

|- !f P.
     FINITE_PRED P ==>
     (!x. FDOM (FUN_FMAP f P) x = P x) /\
     !x. P x ==> (FAPPLY (FUN_FMAP f P) x = f x)

FUNION_DEF

|- !f g.
     (!x. FDOM (FUNION f g) x = FDOM f x \/ FDOM g x) /\
     !x. FAPPLY (FUNION f g) x = (if FDOM f x then FAPPLY f x else FAPPLY g x)

FUPDATE_DEF

|- !f x y.
     FUPDATE f (x,y) = fmap_ABS (\a. (if a = x then INL y else fmap_REP f a))

is_fmap

|- is_fmap =
   (\a0.
      !is_fmap'.
        (!a0.
           (a0 = (\a. INR one)) \/
           (?f a b.
              (a0 = (\x. (if x = a then INL b else f x))) /\ is_fmap' f) ==>
           is_fmap' a0) ==>
        is_fmap' a0)

lookup_DEF

|- !f x. FLOOKUP f x = (if FDOM f x then INL (FAPPLY f x) else INR one)

o_f_DEF

|- !f g.
     (!x. FDOM (f o_f g) x = FDOM g x) /\
     !x. FDOM (f o_f g) x ==> (FAPPLY (f o_f g) x = f (FAPPLY g x))

rep

|- !f. rep f = (\x. (if FDOM f x then INL (FAPPLY f x) else INR one))

RRESTRICT_DEF

|- !f r.
     (!x. FDOM (RRESTRICT f r) x = FDOM f x /\ r (FAPPLY f x)) /\
     !x.
       FAPPLY (RRESTRICT f r) x =
       (if FDOM f x /\ r (FAPPLY f x) then FAPPLY f x else FAPPLY FEMPTY x)

SUBMAP_DEF

|- !f g. f SUBMAP g = !x. FDOM f x ==> FDOM g x /\ (FAPPLY f x = FAPPLY g x)

Theorems

DRESTRICT_DRESTRICT

|- !f P Q. DRESTRICT (DRESTRICT f P) Q = DRESTRICT f (\x. P x /\ Q x)

DRESTRICT_FEMPTY

|- !r. DRESTRICT FEMPTY r = FEMPTY

DRESTRICT_FUNION

|- !f r q.
     DRESTRICT f (\x. r x \/ q x) = FUNION (DRESTRICT f r) (DRESTRICT f q)

DRESTRICT_FUPDATE

|- !f r x y.
     DRESTRICT (FUPDATE f (x,y)) r =
     (if r x then FUPDATE (DRESTRICT f r) (x,y) else DRESTRICT f r)

DRESTRICT_IS_FEMPTY

|- !r. (!x. ~r x) ==> !f. DRESTRICT f r = FEMPTY

DRESTRICT_SUBMAP

|- !f r. DRESTRICT f r SUBMAP f

DRESTRICT_TRUE

|- !f. DRESTRICT f (\x. T) = f

f_o_f_FEMPTY_1

|- !f. FEMPTY f_o_f f = FEMPTY

f_o_f_FEMPTY_2

|- !f. f f_o_f FEMPTY = FEMPTY

FAPPLY_f_o

|- !f g.
     FINITE_PRED (\x. FDOM f (g x)) ==>
     !x. FDOM (f f_o g) x ==> (FAPPLY (f f_o g) x = FAPPLY f (g x))

FAPPLY_FUPDATE

|- !f x y. FAPPLY (FUPDATE f (x,y)) x = y

FAPPLY_FUPDATE_THM

|- !f a b x. FAPPLY (FUPDATE f (a,b)) x = (if x = a then b else FAPPLY f x)

FCARD_0_FEMPTY

|- !f. (FCARD f = 0) = (f = FEMPTY)

FCARD_FEMPTY

|- FCARD FEMPTY = 0

FCARD_FUPDATE

|- !f x y.
     FCARD (FUPDATE f (x,y)) = (if FDOM f x then FCARD f else SUC (FCARD f))

FDOM_DRESTRICT

|- !f r x. ~r x ==> ~FDOM (DRESTRICT f r) x

FDOM_EQ_FDOM_FUPDATE

|- !f x. FDOM f x ==> !y. FDOM (FUPDATE f (x,y)) = FDOM f

FDOM_F_FEMPTY1

|- !f. (!a. ~FDOM f a) = (f = FEMPTY)

FDOM_f_o

|- !f g.
     FINITE_PRED (\x. FDOM f (g x)) ==> !x. FDOM (f f_o g) x = FDOM f (g x)

FDOM_FEMPTY

|- !a. FDOM FEMPTY a = F

FDOM_FUNION

|- !f g x. FDOM (FUNION f g) x = FDOM f x \/ FDOM g x

FDOM_FUPDATE

|- !f a b x. FDOM (FUPDATE f (a,b)) x = (x = a) \/ FDOM f x

FINITE_FMAP

|- !f. ?g n. !x. FDOM f x = ?i. i < n /\ (g i = x)

FINITE_PRED_11

|- !g. (!x y. (g x = g y) = (x = y)) ==> !f. FINITE_PRED (\x. FDOM f (g x))

fmap_EQ

|- !f g. (FDOM f = FDOM g) /\ (FAPPLY f = FAPPLY g) = (f = g)

fmap_EQ_THM

|- !f g.
     (FDOM f = FDOM g) /\ (!x. FDOM f x ==> (FAPPLY f x = FAPPLY g x)) =
     (f = g)

fmap_INDUCT

|- !P.
     P FEMPTY /\ (!f. P f ==> !x y. ~FDOM f x ==> P (FUPDATE f (x,y))) ==>
     !f. P f

fmap_SIMPLE_INDUCT

|- !P. P FEMPTY /\ (!f. P f ==> !x y. P (FUPDATE f (x,y))) ==> !f. P f

FRANGE_FEMPTY

|- !x. ~FRANGE FEMPTY x

FRANGE_FUPDATE

|- !f x y b.
     FRANGE (FUPDATE f (x,y)) b =
     (y = b) \/ FRANGE (DRESTRICT f (\a. ~(a = x))) b

FUNION_FEMPTY_1

|- !g. FUNION FEMPTY g = g

FUNION_FEMPTY_2

|- !f. FUNION f FEMPTY = f

FUNION_FUPDATE_1

|- !f g x y. FUNION (FUPDATE f (x,y)) g = FUPDATE (FUNION f g) (x,y)

FUNION_FUPDATE_2

|- !f g x y.
     FUNION f (FUPDATE g (x,y)) =
     (if FDOM f x then FUNION f g else FUPDATE (FUNION f g) (x,y))

FUPDATE_COMMUTES

|- !f a b c d.
     ~(a = c) ==>
     (FUPDATE (FUPDATE f (a,b)) (c,d) = FUPDATE (FUPDATE f (c,d)) (a,b))

FUPDATE_DRESTRICT

|- !f x y. FUPDATE f (x,y) = FUPDATE (DRESTRICT f (\v. ~(v = x))) (x,y)

FUPDATE_EQ

|- !f a b c. FUPDATE (FUPDATE f (a,b)) (a,c) = FUPDATE f (a,c)

FUPDATE_EXISTING

|- !f v t. FDOM f v /\ (FAPPLY f v = t) = (f = FUPDATE f (v,t))

NOT_EQ_FAPPLY

|- !f a x y. ~(a = x) ==> (FAPPLY (FUPDATE f (x,y)) a = FAPPLY f a)

NOT_EQ_FEMPTY_FUPDATE

|- !f a b. ~(FEMPTY = FUPDATE f (a,b))

NOT_FDOM_DRESTRICT

|- !f x. ~FDOM f x ==> (DRESTRICT f (\a. ~(a = x)) = f)

NOT_FDOM_FAPPLY_FEMPTY

|- !f x. ~FDOM f x ==> (FAPPLY f x = FAPPLY FEMPTY x)

o_f_APPLY

|- !f g x. FDOM g x ==> (FAPPLY (f o_f g) x = f (FAPPLY g x))

o_f_FDOM

|- !f g x. FDOM g x = FDOM (f o_f g) x

RRESTRICT_FEMPTY

|- !r. RRESTRICT FEMPTY r = FEMPTY

RRESTRICT_FUPDATE

|- !f r x y.
     RRESTRICT (FUPDATE f (x,y)) r =
     (if r y then
        FUPDATE (RRESTRICT f r) (x,y)
      else
        RRESTRICT (DRESTRICT f (\a. ~(a = x))) r)

STRONG_DRESTRICT_FUPDATE

|- !f r x y.
     r x ==>
     (DRESTRICT (FUPDATE f (x,y)) r =
      FUPDATE (DRESTRICT f (\v. ~(v = x) /\ r v)) (x,y))

STRONG_DRESTRICT_FUPDATE_THM

|- !f r x y.
     DRESTRICT (FUPDATE f (x,y)) r =
     (if r x then
        FUPDATE (DRESTRICT f (\v. ~(v = x) /\ r v)) (x,y)
      else
        DRESTRICT f (\v. ~(v = x) /\ r v))

SUBMAP_ANTISYM

|- !f g. f SUBMAP g /\ g SUBMAP f = (f = g)

SUBMAP_FEMPTY

|- !f. FEMPTY SUBMAP f

SUBMAP_FRANGE

|- !f g. f SUBMAP g ==> !x. FRANGE f x ==> FRANGE g x

SUBMAP_REFL

|- !f. f SUBMAP f