Hanna Lachnitt (Nov 16 2022 at 20:06): Hanna Lachnitt (Nov 16 2022 at 20:06):Hi everyone,
we have a typedecl in an old theory we found:
typedecl mytype
As far as we understand this means that we know nothing about mytype except that there is at least one element of this type. We read in some old documentation that it is only possible to introduce properties about mytype with an axiomatization which is not recommended. It also sounded like other theories could "instantiate" a typedecl but we found out that this is not the case.
We are interested in creating refinements of this type with additional assumptions while automatically having all theorems on the original mytype.
We thought we could use a locale for this and then interpret the type differently. How would we fix a type inside of our locale?
locale MyLocale =
fixes mytype::"'a"
But then mytype is a variable, is that right? Could we just fix 'a and best give it a nicer name?
Mathias Fleury (Nov 16 2022 at 21:04):the trick is to instantiate the variable with TYPE('a)
Mathias Fleury (Nov 16 2022 at 21:05):locale MyLocale =
fixes mytype::"'a itself"
it is not different from what you are saying, but it looks nicer when instantiating
Mathias Fleury (Nov 16 2022 at 21:05):You could use any name instead of 'a
Mathias Fleury (Nov 16 2022 at 21:06):although this will have some conquences on the inferred types on theorems (the default name being 'a)
Last updated: Apr 28 2024 at 12:28 UTC