[isabelle] Theory of finite maps



Hello,

We have been working with the following type specification:
"type foo = 'a => nat option".  However, the
theory-in-progress requires that "foo" partial functions 
have finite domains.  

Is there a finite map theory for Isabelle?  If not, is there a
suggested way of enforcing this restriction at the
type-definition level?  We've already completed many proofs
with the existing definition of "foo", so going back and
adding "finite(dom(fun))" predicates would be a great deal of
trouble.

Thank you,

Justin S. Davis
Formal Methods Research Group
Department of Computer Science
University of Illinois, Urbana-Champaign





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.