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
(!!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
This archive was generated by a fusion of
Pipermail (Mailman edition) and