Re: [isabelle] Variables in locale assumptions




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 the assumptions 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 local to the assumption or not. The locale tutorial suggests that they should be local, but maybe I'm wrong.

The quantification in the first form is what happens logically, but syntactically the "free" variables share the same scope of the whole specification. Thus you need to use explicit binders, or evade the problem by renaming variables apart.

Thanks, okay, got it! But for the record I can add that it's not what I expected.

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

Sorry, just wrote a quick and dirty example to show what I found surprising. I don't know what it has to do with the issue really, but I stored the example in Test.thy.

Thanks again,
Stephan




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