*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Variables in locale assumptions*From*: Stephan van Staden <Stephan.vanStaden at inf.ethz.ch>*Date*: Fri, 21 Feb 2014 22:28:00 +0000*Cc*: John Wickerson <johnwickerson at cantab.net>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <alpine.LNX.2.00.1402211828050.46463@lxbroy10.informatik.tu-muenchen.de>*References*: <FC4BBC48012AB34DAF828891BA6076320A6BED6F@MBX21.d.ethz.ch>, <D85BDDB5-D8F4-4F4C-A578-35FD64B33584@cantab.net> <FC4BBC48012AB34DAF828891BA6076320A6BEE7C@MBX21.d.ethz.ch> <alpine.LNX.2.00.1402211828050.46463@lxbroy10.informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.2.0

On 21.02.2014 17:33, Makarius wrote:

On Fri, 21 Feb 2014, Van Staden Stephan wrote:It's a free variable in each assumption. I would expect theassumptions to be:(!!S R. pred S R) /\ (!!S R. pred R S) but what happens is apparently: (!!S R. pred S R /\ pred R S)The question is whether the free variables in an assumption are localto the assumption or not. The locale tutorial suggests that theyshould be local, but maybe I'm wrong.The quantification in the first form is what happens logically, butsyntactically the "free" variables share the same scope of the wholespecification. Thus you need to use explicit binders, or evade theproblem by renaming variables apart.

Note that "Test" is a bad name for a locale: lower-case is normallyused. Likewise, theory names are usually capitalized words (insingular), separated by underscore. (You did not show that in theexample, but I guess > 50% that you've had a lowercase test.thy here,or was it justScratch.thy?)

Thanks again, Stephan

**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:*Makarius

- Previous by Date: [isabelle] LFMTP 2014: Call for Papers
- Next by Date: Re: [isabelle] Variables in locale assumptions
- 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