*To*: Makarius <makarius at sketis.net>, Lawrence Paulson <lp15 at cam.ac.uk>*Subject*: Re: [isabelle] Variables in locale assumptions*From*: "Van Staden Stephan" <stephan.vanstaden at inf.ethz.ch>*Date*: Mon, 24 Feb 2014 12:56:26 +0000*Accept-language*: en-US, de-CH*Cc*: Peter Lammich <lammich at in.tum.de>, "cl-isabelle-users at lists.cam.ac.uk List" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <alpine.LNX.2.00.1402241331170.5131@lxbroy10.informatik.tu-muenchen.de>*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> <1393062477.17875.8.camel@lapbroy33> <BB1863A5-D8C7-41F4-93EC-CA27874FADE5@cam.ac.uk>, <alpine.LNX.2.00.1402241331170.5131@lxbroy10.informatik.tu-muenchen.de>*Thread-index*: Ac8vHtkxnWObjyRgRR64U4+y2zgO/////Y8AgAARDn3///w9AIAAYrUAgACqT4CAABrbAIADOkaAgAAU1sM=*Thread-topic*: [isabelle] Variables in locale assumptions

Thanks for the explanations. It seems wise to keep it the way it is. All the best, Stephan ________________________________________ From: cl-isabelle-users-bounces at lists.cam.ac.uk [cl-isabelle-users-bounces at lists.cam.ac.uk] on behalf of Makarius [makarius at sketis.net] Sent: Monday, February 24, 2014 1:41 PM To: Lawrence Paulson Cc: Peter Lammich; cl-isabelle-users at lists.cam.ac.uk List Subject: Re: [isabelle] Variables in locale assumptions On Sat, 22 Feb 2014, Lawrence Paulson wrote: > Clearly every instance of a variable in a single formula must have the > same type, and it’s natural to expect that every instance in a list of > formulas should also have the same type. The alternative would be very > confusing for readers, also in informal mathematics. > > On 22 Feb 2014, at 09:47, Peter Lammich <lammich at in.tum.de> wrote: > >> >>> It's this type constraint that surprised me. The post by Makarius >>> explains it, but as a user I would prefer to have complete separation. >>> Is there a compelling reason why it's implemented as it is? >>> >> >> I frequently run into another instance of this problem, when writing >> something like: >> >> lemma foo: >> "x & y --> x" >> "x = y --> f x = f y" >> >> Note that foo(2) is: "?x::bool = ?y ...", which is usually not >> what was intended. The observation by Larry is correct. He probably still remembers the time when type-inference would only range over each term separately, causing many strange effects and surprises. When you write a simultaneous statement as above, or a long statement with fixes/assumes/shows, the scope of free variables and their types ranges over the whole clause. This is the intended way -- we have required many years to get there. A slightly different situation occurs in conceptually separate scopes that happen to be written with free variables that share the type-inference scope, but are logically separate. There are two main situations for this: the 'obtains' statement with several disjuctive branches, and the implicit quantification of locale expressions that were encountered here. Here I would prefer to keep type-information separate, according to the logical structure. When I introduced the latter locale convenience about 12 years ago, I was aware of the snag with type-inference, and also aware of the lack of any systematic documentation of type-inference in the Isabelle manuals (even until today). Approximately every 5 years some user stumbles over that detail. The manuals could be improved at some point, but it is probably more helpful to give more feedback about scopes and type-inference errors in the Prover IDE. 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:*Peter Lammich

**Re: [isabelle] Variables in locale assumptions***From:*Lawrence Paulson

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

- Previous by Date: Re: [isabelle] Variables in locale assumptions
- Next by Date: [isabelle] Notation forgets unnamed context inside type class context
- Previous by Thread: Re: [isabelle] Variables in locale assumptions
- Next by Thread: Re: [isabelle] Variables in locale assumptions
- 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