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.


	Makarius


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