*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Subject*: Re: [isabelle] Variables in locale assumptions*From*: Makarius <makarius at sketis.net>*Date*: Wed, 26 Feb 2014 13:01:07 +0100 (CET)*Cc*: Gerwin Klein <Gerwin.Klein at nicta.com.au>, isabelle-users at cl.cam.ac.uk*In-reply-to*: <530C42CF.9050003@inf.ethz.ch>*References*: <FC4BBC48012AB34DAF828891BA6076320A6BED6F@MBX21.d.ethz.ch>, <D85BDDB5-D8F4-4F4C-A578-35FD64B33584@cantab.net> <FC4BBC48012AB34DAF828891BA6076320A6BEE7C@MBX21.d.ethz.ch> <9B97784B-AE5E-4291-B2C0-4285E7894C11@gmail.com> <5307D560.3010508@inf.ethz.ch> <alpine.LNX.2.00.1402241348450.5131@lxbroy10.informatik.tu-muenchen.de> <6363A4A9-BAD9-44F4-8860-15A89157E23E@nicta.com.au> <alpine.LNX.2.00.1402242255440.26330@lxbroy10.informatik.tu-muenchen.de> <530C42CF.9050003@inf.ethz.ch>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Tue, 25 Feb 2014, Andreas Lochbihler wrote:

On 24/02/14 23:05, Makarius wrote: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.

I know one use case where constrains is more convenient than parameterinstantiation with for, namely to revert the renaming of type variables.I want type variables to have sensible names like 'state, not just 'a,'b, 'c, 'd. Unfortunately, locale inheritance always renames them to 'a,'b, 'c, etc., so I rename them back.

Of course, this can be done with a for clause, too. But a for clausedrops the mixfix syntax associated with the parameter, so would have toredeclare it; with constrains, I need not. And for consistency reasons,I prefer not to redeclare notation if it's not necessary. And if localeinheritance did not rename type variables, I'd not need constrains atall and be much happier.

Makarius

**References**:**[isabelle] Variables in locale assumptions***From:*Van Staden Stephan

**Re: [isabelle] Variables in locale assumptions***From:*John Wickerson

**Re: [isabelle] Variables in locale assumptions***From:*Van Staden Stephan

**Re: [isabelle] Variables in locale assumptions***From:*Jasmin Blanchette

**Re: [isabelle] Variables in locale assumptions***From:*Stephan van Staden

**Re: [isabelle] Variables in locale assumptions***From:*Makarius

**Re: [isabelle] Variables in locale assumptions***From:*Makarius

**Re: [isabelle] Variables in locale assumptions***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Isabelle (JEDIT) seems slower than Isabelle(emacs)
- Next by Date: [isabelle] Code-equations for multisets
- Previous by Thread: Re: [isabelle] Variables in locale assumptions
- Next by Thread: [isabelle] LFMTP 2014: Call for Papers
- Cl-isabelle-users February 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list