Re: [isabelle] Variables in locale assumptions



On Mon, 24 Feb 2014, Makarius wrote:

On Mon, 24 Feb 2014, Gerwin Klein wrote:

 or if you need to constrain types?

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.

Maybe you have actually missed the important locale expression improvements by Clemens Ballarin from Isabelle2009. See the NEWS, e.g. this one:

  - In locale expressions, instantiation replaces renaming.  Parameters
  must be declared in a for clause.  To aid compatibility with previous
  parameter inheritance, in locale declarations, parameters that are not
  'touched' (instantiation position "_" or omitted) are implicitly added
  with their syntax at the beginning of the for clause.

In most situations a locale expression suffix "for x :: T" can be used to instantiate types in imports. I had cleaned up AFP in this respect already some years ago, but in various newer entries old 'constrains' seem to have come back. Time for spring cleaning?


	Makarius




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