Email Gateway (Aug 17 2022 at 14:15): Email Gateway (Aug 17 2022 at 14:15):From: jdavis27@uiuc.edu
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
Email Gateway (Aug 17 2022 at 14:15):From: nipkow@in.tum.de
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.
If you have already completed the proofs, they didn't need any finiteness
assumption, so you won't have to add any either.
Tobias
Last updated: May 03 2024 at 12:27 UTC