# Structure finite_mapLib

signature finite_mapLib =
sig
include Abbrev
(*Expands FEVERY into a conjunction
``FEVERY P (FEMPTY |+ (x1, y1) |+ (x2, y2) |+ (x3, y3) |+ (x4, y4))``
gets for example expanded to
|- FEVERY P (X |+ (x1,y1) |+ (x2,y2) |+ (x3,y3) |+ (x4,y4)) <=>
P (x4,y4) /\
(~(x3 = x4) ==> P (x3,y3)) /\
(~((x2 = x3) \/ (x2 = x4)) ==> P (x2,y2)) /\
(~((x1 = x2) \/ (x1 = x3) \/ (x1 = x4)) ==> P (x1,y1))
*)
val fevery_EXPAND_CONV : Abbrev.conv
(*Simplies fupdate - sequences by removing the ones that are masked by
later appearances.
``f |+ (x1, y1) |+ (x2, y2) |+ (x1, y3) |+ (x4, y4)``
gets for example simplied to to
|- (f |+ (x1, y1) |+ (x2, y2) |+ (x1, y3) |+ (x4, y4)) =
(f |+ (x2, y2) |+ (x1, y3) |+ (x4, y4))
*)
val fupdate_NORMALISE_CONV : Abbrev.conv
val add_finite_map_compset : computeLib.compset -> unit
end

*HOL 4, Kananaskis-14*