Re: [isabelle] Variables in locale assumptions



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.

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?)


	Makarius




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