Structure finite_mapTheory
signature finite_mapTheory =
sig
type thm = Thm.thm
(* Definitions *)
val DRESTRICT_DEF : thm
val FAPPLY_DEF : thm
val FCARD_DEF : thm
val FDOM_DEF : thm
val FEMPTY_DEF : thm
val FEVERY_DEF : thm
val FLOOKUP_DEF : thm
val FRANGE_DEF : thm
val FUNION_DEF : thm
val FUN_FMAP_DEF : thm
val FUPDATE_DEF : thm
val FUPDATE_LIST : thm
val RRESTRICT_DEF : thm
val SUBMAP_DEF : thm
val f_o_DEF : thm
val f_o_f_DEF : thm
val fmap_ISO_DEF : thm
val fmap_TY_DEF : thm
val fmap_domsub : thm
val is_fmap : thm
val o_f_DEF : thm
(* Theorems *)
val DOMSUB_FAPPLY : thm
val DOMSUB_FAPPLY_NEQ : thm
val DOMSUB_FAPPLY_THM : thm
val DOMSUB_FEMPTY : thm
val DOMSUB_FUPDATE : thm
val DOMSUB_FUPDATE_NEQ : thm
val DOMSUB_FUPDATE_THM : thm
val DOMSUB_IDEM : thm
val DOMSUB_NOT_IN_DOM : thm
val DRESTRICT_DRESTRICT : thm
val DRESTRICT_FEMPTY : thm
val DRESTRICT_FUNION : thm
val DRESTRICT_FUPDATE : thm
val DRESTRICT_IS_FEMPTY : thm
val DRESTRICT_SUBMAP : thm
val DRESTRICT_UNIV : thm
val FAPPLY_FUPDATE : thm
val FAPPLY_FUPDATE_THM : thm
val FAPPLY_f_o : thm
val FCARD_0_FEMPTY : thm
val FCARD_FEMPTY : thm
val FCARD_FUPDATE : thm
val FCARD_SUC : thm
val FDOM_DOMSUB : thm
val FDOM_DRESTRICT : thm
val FDOM_EQ_EMPTY : thm
val FDOM_EQ_FDOM_FUPDATE : thm
val FDOM_FEMPTY : thm
val FDOM_FINITE : thm
val FDOM_FUNION : thm
val FDOM_FUPDATE : thm
val FDOM_FUPDATE_LIST : thm
val FDOM_F_FEMPTY1 : thm
val FDOM_f_o : thm
val FDOM_o_f : thm
val FEVERY_FEMPTY : thm
val FEVERY_FUPDATE : thm
val FINITE_FRANGE : thm
val FINITE_PRED_11 : thm
val FLOOKUP_EMPTY : thm
val FLOOKUP_UPDATE : thm
val FMEQ_ENUMERATE_CASES : thm
val FMEQ_SINGLE_SIMPLE_DISJ_ELIM : thm
val FMEQ_SINGLE_SIMPLE_ELIM : thm
val FM_PULL_APART : thm
val FRANGE_FEMPTY : thm
val FRANGE_FMAP : thm
val FRANGE_FUPDATE : thm
val FRANGE_FUPDATE_DOMSUB : thm
val FUNION_FEMPTY_1 : thm
val FUNION_FEMPTY_2 : thm
val FUNION_FUPDATE_1 : thm
val FUNION_FUPDATE_2 : thm
val FUN_FMAP_EMPTY : thm
val FUPD11_SAME_BASE : thm
val FUPD11_SAME_KEY_AND_BASE : thm
val FUPD11_SAME_NEW_KEY : thm
val FUPD11_SAME_UPDATE : thm
val FUPDATE_COMMUTES : thm
val FUPDATE_DRESTRICT : thm
val FUPDATE_EQ : thm
val FUPDATE_LIST_APPLY_NOT_MEM : thm
val FUPDATE_LIST_SAME_KEYS_UNWIND : thm
val FUPDATE_LIST_SAME_UPDATE : thm
val FUPDATE_LIST_THM : thm
val FUPD_SAME_KEY_UNWIND : thm
val NOT_EQ_FAPPLY : thm
val NOT_EQ_FEMPTY_FUPDATE : thm
val NOT_FDOM_DRESTRICT : thm
val NOT_FDOM_FAPPLY_FEMPTY : thm
val RRESTRICT_FEMPTY : thm
val RRESTRICT_FUPDATE : thm
val SAME_KEY_UPDATES_DIFFER : thm
val STRONG_DRESTRICT_FUPDATE : thm
val STRONG_DRESTRICT_FUPDATE_THM : thm
val SUBMAP_ANTISYM : thm
val SUBMAP_FEMPTY : thm
val SUBMAP_FRANGE : thm
val SUBMAP_FUPDATE : thm
val SUBMAP_REFL : thm
val SUBMAP_TRANS : thm
val f_o_f_FEMPTY_1 : thm
val f_o_f_FEMPTY_2 : thm
val fmap_CASES : thm
val fmap_EQ : thm
val fmap_EQ_THM : thm
val fmap_EXT : thm
val fmap_INDUCT : thm
val fmap_SIMPLE_INDUCT : thm
val is_fmap_cases : thm
val is_fmap_ind : thm
val is_fmap_rules : thm
val o_f_DOMSUB : thm
val o_f_FAPPLY : thm
val o_f_FDOM : thm
val o_f_FEMPTY : thm
val o_f_FUPDATE : thm
val o_f_o_f : thm
val finite_map_grammars : type_grammar.grammar * term_grammar.grammar
val finite_map_rwts : simpLib.ssfrag
(*
[list] Parent theory of "finite_map"
[pred_set] Parent theory of "finite_map"
[DRESTRICT_DEF] Definition
|- !f r.
(FDOM (DRESTRICT f r) = FDOM f INTER r) /\
!x.
DRESTRICT f r ' x = (if x IN FDOM f INTER r then f ' x else FEMPTY ' x)
[FAPPLY_DEF] Definition
|- !f x. f ' x = OUTL (fmap_REP f x)
[FCARD_DEF] Definition
|- !fm. FCARD fm = CARD (FDOM fm)
[FDOM_DEF] Definition
|- !f x. FDOM f x = ISL (fmap_REP f x)
[FEMPTY_DEF] Definition
|- FEMPTY = fmap_ABS (\a. INR ())
[FEVERY_DEF] Definition
|- !P f. FEVERY P f = !x. x IN FDOM f ==> P (x,f ' x)
[FLOOKUP_DEF] Definition
|- !f x. FLOOKUP f x = (if x IN FDOM f then SOME (f ' x) else NONE)
[FRANGE_DEF] Definition
|- !f. FRANGE f = {y | ?x. x IN FDOM f /\ (f ' x = y)}
[FUNION_DEF] Definition
|- !f g.
(FDOM (FUNION f g) = FDOM f UNION FDOM g) /\
!x. FUNION f g ' x = (if x IN FDOM f then f ' x else g ' x)
[FUN_FMAP_DEF] Definition
|- !f P.
FINITE P ==>
(FDOM (FUN_FMAP f P) = P) /\ !x. x IN P ==> (FUN_FMAP f P ' x = f x)
[FUPDATE_DEF] Definition
|- !f x y. f |+ (x,y) = fmap_ABS (\a. (if a = x then INL y else fmap_REP f a))
[FUPDATE_LIST] Definition
|- $|++ = FOLDL $|+
[RRESTRICT_DEF] Definition
|- !f r.
(FDOM (RRESTRICT f r) = {x | x IN FDOM f /\ f ' x IN r}) /\
!x.
RRESTRICT f r ' x =
(if x IN FDOM f /\ f ' x IN r then f ' x else FEMPTY ' x)
[SUBMAP_DEF] Definition
|- !f g. f SUBMAP g = !x. x IN FDOM f ==> x IN FDOM g /\ (f ' x = g ' x)
[f_o_DEF] Definition
|- !f g. f f_o g = f f_o_f FUN_FMAP g {x | g x IN FDOM f}
[f_o_f_DEF] Definition
|- !f g.
(FDOM (f f_o_f g) = FDOM g INTER {x | g ' x IN FDOM f}) /\
!x. x IN FDOM (f f_o_f g) ==> ((f f_o_f g) ' x = f ' (g ' x))
[fmap_ISO_DEF] Definition
|- (!a. fmap_ABS (fmap_REP a) = a) /\
!r. is_fmap r = (fmap_REP (fmap_ABS r) = r)
[fmap_TY_DEF] Definition
|- ?rep. TYPE_DEFINITION is_fmap rep
[fmap_domsub] Definition
|- !fm k. fm \\ k = DRESTRICT fm (COMPL {k})
[is_fmap] Definition
|- 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)
[o_f_DEF] Definition
|- !f g.
(FDOM (f o_f g) = FDOM g) /\
!x. x IN FDOM (f o_f g) ==> ((f o_f g) ' x = f (g ' x))
[DOMSUB_FAPPLY] Theorem
|- !fm k. (fm \\ k) ' k = FEMPTY ' k
[DOMSUB_FAPPLY_NEQ] Theorem
|- !fm k1 k2. ~(k1 = k2) ==> ((fm \\ k1) ' k2 = fm ' k2)
[DOMSUB_FAPPLY_THM] Theorem
|- !fm k1 k2. (fm \\ k1) ' k2 = (if k1 = k2 then FEMPTY ' k2 else fm ' k2)
[DOMSUB_FEMPTY] Theorem
|- !k. FEMPTY \\ k = FEMPTY
[DOMSUB_FUPDATE] Theorem
|- !fm k v. fm |+ (k,v) \\ k = fm \\ k
[DOMSUB_FUPDATE_NEQ] Theorem
|- !fm k1 k2 v. ~(k1 = k2) ==> (fm |+ (k1,v) \\ k2 = fm \\ k2 |+ (k1,v))
[DOMSUB_FUPDATE_THM] Theorem
|- !fm k1 k2 v.
fm |+ (k1,v) \\ k2 = (if k1 = k2 then fm \\ k2 else fm \\ k2 |+ (k1,v))
[DOMSUB_IDEM] Theorem
|- fm \\ k \\ k = fm \\ k
[DOMSUB_NOT_IN_DOM] Theorem
|- ~(k IN FDOM fm) ==> (fm \\ k = fm)
[DRESTRICT_DRESTRICT] Theorem
|- !f P Q. DRESTRICT (DRESTRICT f P) Q = DRESTRICT f (P INTER Q)
[DRESTRICT_FEMPTY] Theorem
|- !r. DRESTRICT FEMPTY r = FEMPTY
[DRESTRICT_FUNION] Theorem
|- !f r q. DRESTRICT f (r UNION q) = FUNION (DRESTRICT f r) (DRESTRICT f q)
[DRESTRICT_FUPDATE] Theorem
|- !f r x y.
DRESTRICT (f |+ (x,y)) r =
(if x IN r then DRESTRICT f r |+ (x,y) else DRESTRICT f r)
[DRESTRICT_IS_FEMPTY] Theorem
|- !f. DRESTRICT f {} = FEMPTY
[DRESTRICT_SUBMAP] Theorem
|- !f r. DRESTRICT f r SUBMAP f
[DRESTRICT_UNIV] Theorem
|- !f. DRESTRICT f UNIV = f
[FAPPLY_FUPDATE] Theorem
|- !f x y. (f |+ (x,y)) ' x = y
[FAPPLY_FUPDATE_THM] Theorem
|- !f a b x. (f |+ (a,b)) ' x = (if x = a then b else f ' x)
[FAPPLY_f_o] Theorem
|- !f g.
FINITE {x | g x IN FDOM f} ==>
!x. x IN FDOM (f f_o g) ==> ((f f_o g) ' x = f ' (g x))
[FCARD_0_FEMPTY] Theorem
|- !f. (FCARD f = 0) = (f = FEMPTY)
[FCARD_FEMPTY] Theorem
|- FCARD FEMPTY = 0
[FCARD_FUPDATE] Theorem
|- !fm a b.
FCARD (fm |+ (a,b)) = (if a IN FDOM fm then FCARD fm else 1 + FCARD fm)
[FCARD_SUC] Theorem
|- !f n.
(FCARD f = SUC n) =
?f' x y. ~(x IN FDOM f') /\ (FCARD f' = n) /\ (f = f' |+ (x,y))
[FDOM_DOMSUB] Theorem
|- !fm k. FDOM (fm \\ k) = FDOM fm DELETE k
[FDOM_DRESTRICT] Theorem
|- !f r x. FDOM (DRESTRICT f r) = FDOM f INTER r
[FDOM_EQ_EMPTY] Theorem
|- !f. (FDOM f = {}) = (f = FEMPTY)
[FDOM_EQ_FDOM_FUPDATE] Theorem
|- !f x. x IN FDOM f ==> !y. FDOM (f |+ (x,y)) = FDOM f
[FDOM_FEMPTY] Theorem
|- FDOM FEMPTY = {}
[FDOM_FINITE] Theorem
|- !fm. FINITE (FDOM fm)
[FDOM_FUNION] Theorem
|- !f g x. FDOM (FUNION f g) = FDOM f UNION FDOM g
[FDOM_FUPDATE] Theorem
|- !f a b. FDOM (f |+ (a,b)) = a INSERT FDOM f
[FDOM_FUPDATE_LIST] Theorem
|- !kvl fm. FDOM (fm |++ kvl) = FDOM fm UNION LMEM (MAP FST kvl)
[FDOM_F_FEMPTY1] Theorem
|- !f. (!a. ~(a IN FDOM f)) = (f = FEMPTY)
[FDOM_f_o] Theorem
|- !f g. FINITE {x | g x IN FDOM f} ==> (FDOM (f f_o g) = {x | g x IN FDOM f})
[FDOM_o_f] Theorem
|- !f g. FDOM (f o_f g) = FDOM g
[FEVERY_FEMPTY] Theorem
|- !P. FEVERY P FEMPTY
[FEVERY_FUPDATE] Theorem
|- !P f x y.
FEVERY P (f |+ (x,y)) = P (x,y) /\ FEVERY P (DRESTRICT f (COMPL {x}))
[FINITE_FRANGE] Theorem
|- !fm. FINITE (FRANGE fm)
[FINITE_PRED_11] Theorem
|- !g. (!x y. (g x = g y) = (x = y)) ==> !f. FINITE {x | g x IN FDOM f}
[FLOOKUP_EMPTY] Theorem
|- FLOOKUP FEMPTY k = NONE
[FLOOKUP_UPDATE] Theorem
|- FLOOKUP (fm |+ (k1,v)) k2 = (if k1 = k2 then SOME v else FLOOKUP fm k2)
[FMEQ_ENUMERATE_CASES] Theorem
|- !f1 kvl p. (f1 |+ p = FEMPTY |++ kvl) ==> MEM p kvl
[FMEQ_SINGLE_SIMPLE_DISJ_ELIM] Theorem
|- !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] Theorem
|- !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))
[FM_PULL_APART] Theorem
|- !fm k. k IN FDOM fm ==> ?fm0 v. (fm = fm0 |+ (k,v)) /\ ~(k IN FDOM fm0)
[FRANGE_FEMPTY] Theorem
|- FRANGE FEMPTY = {}
[FRANGE_FMAP] Theorem
|- FINITE P ==> (FRANGE (FUN_FMAP f P) = IMAGE f P)
[FRANGE_FUPDATE] Theorem
|- !f x y. FRANGE (f |+ (x,y)) = y INSERT FRANGE (DRESTRICT f (COMPL {x}))
[FRANGE_FUPDATE_DOMSUB] Theorem
|- !fm k v. FRANGE (fm |+ (k,v)) = v INSERT FRANGE (fm \\ k)
[FUNION_FEMPTY_1] Theorem
|- !g. FUNION FEMPTY g = g
[FUNION_FEMPTY_2] Theorem
|- !f. FUNION f FEMPTY = f
[FUNION_FUPDATE_1] Theorem
|- !f g x y. FUNION (f |+ (x,y)) g = FUNION f g |+ (x,y)
[FUNION_FUPDATE_2] Theorem
|- !f g x y.
FUNION f (g |+ (x,y)) =
(if x IN FDOM f then FUNION f g else FUNION f g |+ (x,y))
[FUN_FMAP_EMPTY] Theorem
|- FUN_FMAP f {} = FEMPTY
[FUPD11_SAME_BASE] Theorem
|- !f k1 v1 k2 v2.
(f |+ (k1,v1) = f |+ (k2,v2)) =
(k1 = k2) /\ (v1 = v2) \/
~(k1 = k2) /\ k1 IN FDOM f /\ k2 IN FDOM f /\ (f |+ (k1,v1) = f) /\
(f |+ (k2,v2) = f)
[FUPD11_SAME_KEY_AND_BASE] Theorem
|- !f k v1 v2. (f |+ (k,v1) = f |+ (k,v2)) = (v1 = v2)
[FUPD11_SAME_NEW_KEY] Theorem
|- !f1 f2 k v1 v2.
~(k IN FDOM f1) /\ ~(k IN FDOM f2) ==>
((f1 |+ (k,v1) = f2 |+ (k,v2)) = (f1 = f2) /\ (v1 = v2))
[FUPD11_SAME_UPDATE] Theorem
|- !f1 f2 k v.
(f1 |+ (k,v) = f2 |+ (k,v)) =
(DRESTRICT f1 (COMPL {k}) = DRESTRICT f2 (COMPL {k}))
[FUPDATE_COMMUTES] Theorem
|- !f a b c d. ~(a = c) ==> (f |+ (a,b) |+ (c,d) = f |+ (c,d) |+ (a,b))
[FUPDATE_DRESTRICT] Theorem
|- !f x y. f |+ (x,y) = DRESTRICT f (COMPL {x}) |+ (x,y)
[FUPDATE_EQ] Theorem
|- !f a b c. f |+ (a,b) |+ (a,c) = f |+ (a,c)
[FUPDATE_LIST_APPLY_NOT_MEM] Theorem
|- !kvl f k. ~MEM k (MAP FST kvl) ==> ((f |++ kvl) ' k = f ' k)
[FUPDATE_LIST_SAME_KEYS_UNWIND] Theorem
|- !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] Theorem
|- !kvl f1 f2.
(f1 |++ kvl = f2 |++ kvl) =
(DRESTRICT f1 (COMPL (LMEM (MAP FST kvl))) =
DRESTRICT f2 (COMPL (LMEM (MAP FST kvl))))
[FUPDATE_LIST_THM] Theorem
|- !f. (f |++ [] = f) /\ !h t. f |++ (h::t) = f |+ h |++ t
[FUPD_SAME_KEY_UNWIND] Theorem
|- !f1 f2 k v1 v2.
(f1 |+ (k,v1) = f2 |+ (k,v2)) ==>
(v1 = v2) /\ !v. f1 |+ (k,v) = f2 |+ (k,v)
[NOT_EQ_FAPPLY] Theorem
|- !f a x y. ~(a = x) ==> ((f |+ (x,y)) ' a = f ' a)
[NOT_EQ_FEMPTY_FUPDATE] Theorem
|- !f a b. ~(FEMPTY = f |+ (a,b))
[NOT_FDOM_DRESTRICT] Theorem
|- !f x. ~(x IN FDOM f) ==> (DRESTRICT f (COMPL {x}) = f)
[NOT_FDOM_FAPPLY_FEMPTY] Theorem
|- !f x. ~(x IN FDOM f) ==> (f ' x = FEMPTY ' x)
[RRESTRICT_FEMPTY] Theorem
|- !r. RRESTRICT FEMPTY r = FEMPTY
[RRESTRICT_FUPDATE] Theorem
|- !f r x y.
RRESTRICT (f |+ (x,y)) r =
(if y IN r then
RRESTRICT f r |+ (x,y)
else
RRESTRICT (DRESTRICT f (COMPL {x})) r)
[SAME_KEY_UPDATES_DIFFER] Theorem
|- !f1 f2 k v1 v2. ~(v1 = v2) ==> ~(f1 |+ (k,v1) = f2 |+ (k,v2))
[STRONG_DRESTRICT_FUPDATE] Theorem
|- !f r x y.
x IN r ==> (DRESTRICT (f |+ (x,y)) r = DRESTRICT f (r DELETE x) |+ (x,y))
[STRONG_DRESTRICT_FUPDATE_THM] Theorem
|- !f r x y.
DRESTRICT (f |+ (x,y)) r =
(if x IN r then
DRESTRICT f (COMPL {x} INTER r) |+ (x,y)
else
DRESTRICT f (COMPL {x} INTER r))
[SUBMAP_ANTISYM] Theorem
|- !f g. f SUBMAP g /\ g SUBMAP f = (f = g)
[SUBMAP_FEMPTY] Theorem
|- !f. FEMPTY SUBMAP f
[SUBMAP_FRANGE] Theorem
|- !f g. f SUBMAP g ==> FRANGE f SUBSET FRANGE g
[SUBMAP_FUPDATE] Theorem
|- !f g x y.
f |+ (x,y) SUBMAP g = x IN FDOM g /\ (g ' x = y) /\ f \\ x SUBMAP g \\ x
[SUBMAP_REFL] Theorem
|- !f. f SUBMAP f
[SUBMAP_TRANS] Theorem
|- !f g h. f SUBMAP g /\ g SUBMAP h ==> f SUBMAP h
[f_o_f_FEMPTY_1] Theorem
|- !f. FEMPTY f_o_f f = FEMPTY
[f_o_f_FEMPTY_2] Theorem
|- !f. f f_o_f FEMPTY = FEMPTY
[fmap_CASES] Theorem
|- !f. (f = FEMPTY) \/ ?g x y. f = g |+ (x,y)
[fmap_EQ] Theorem
|- !f g. (FDOM f = FDOM g) /\ ($' f = $' g) = (f = g)
[fmap_EQ_THM] Theorem
|- !f g. (FDOM f = FDOM g) /\ (!x. x IN FDOM f ==> (f ' x = g ' x)) = (f = g)
[fmap_EXT] Theorem
|- !f g. (f = g) = (FDOM f = FDOM g) /\ !x. x IN FDOM f ==> (f ' x = g ' x)
[fmap_INDUCT] Theorem
|- !P.
P FEMPTY /\ (!f. P f ==> !x y. ~(x IN FDOM f) ==> P (f |+ (x,y))) ==>
!f. P f
[fmap_SIMPLE_INDUCT] Theorem
|- !P. P FEMPTY /\ (!f. P f ==> !x y. P (f |+ (x,y))) ==> !f. P f
[is_fmap_cases] Theorem
|- !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] Theorem
|- !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] Theorem
|- is_fmap (\a. INR ()) /\
!f a b. is_fmap f ==> is_fmap (\x. (if x = a then INL b else f x))
[o_f_DOMSUB] Theorem
|- (g o_f fm) \\ k = g o_f fm \\ k
[o_f_FAPPLY] Theorem
|- !f g x. x IN FDOM g ==> ((f o_f g) ' x = f (g ' x))
[o_f_FDOM] Theorem
|- !f g. FDOM g = FDOM (f o_f g)
[o_f_FEMPTY] Theorem
|- f o_f FEMPTY = FEMPTY
[o_f_FUPDATE] Theorem
|- f o_f fm |+ (k,v) = (f o_f fm \\ k) |+ (k,f v)
[o_f_o_f] Theorem
|- f o_f (g o_f h) = f o g o_f h
*)
end
HOL 4, Kananaskis-3