A Theory of Finite Maps

Finite maps, functions defined on only a finite domain, occur often, particularly when reasoning about programming languages. This paper presents a theory of finite maps in HOL. We discuss the choice of representation, present the theory we have defined, and discuss the issue of defining recursive types containing finite maps. We also discuss decision procedures and give an example of the use of finite maps in developing the semantics of a small language.