Re: [isabelle] Theory of finite maps

In our experience one often (but clearly not always) does not need
finiteness. Hence we only provided a => b option. One should probably provide
a separate theory of finite maps as well - HOL4 has one, afaik, and we have a
theory of association lists in the development version which can serve the
same purpose. But due to HOL's type system, you cannot have finite maps as a
subtype of infinite maps, it needs two separate theories.

> 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.

If you have already completed the proofs, they didn't need any finiteness
assumption, so you won't have to add any either.


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