Re: [isabelle] Variables in locale assumptions
On Mon, 24 Feb 2014, Gerwin Klein wrote:
Feasibility and complexity of implementation. In order to move locales
once again some steps forward, one should probably give up rarely used
old features like 'defines' and 'constrains' (which have heavy weight
and little real applications).
I’m fairly fond of those two mechanisms, but maybe I’ve just missed what
you would do instead now.
What should you be doing if you have large terms in the locale that you
need to use in assumes statement or if you need to constrain types?
The 'defines' element predates proper 'definition (in loc)'. Having
axiomatic specifications that are intertwined with quasi-definitional ones
is conceptually very complex, and actually a mess. I know that people
sometimes do that, but one would have to look very closely if that is
really required: normally you should be able to pull out the auxiliary
definitions before the locale specifications. If we would have
understood localized definitions already in 1999, this problem would not
exist, because 'defines' would have never been introduced.
The 'constrains' element is easier to get rid of. I would like to see
some constructive proofs where you "need to constrain types", as you say.
This is usually just a workaround to specify locale type arguments, but if
that would be supported directly, the need would go away.
Anyway, we have just the default situation of inertia: after many years of
getting used to some not-quite-right feature, users find it hard to go
beyond it. This is why certain problems cannot be solved easily, and we
need to explain new users why some things are a bit odd.
This archive was generated by a fusion of
Pipermail (Mailman edition) and