# [isabelle] interpret with free variables

Hi all,

`when interpreting locales on the theory level with the interpretation
``command, free variables in the terms that instantiate the locale
``parameters are automatically universally quantified. How can this be
``done for the interpret command that can be used inside lemmas.
`
For example, take the following artificial locale loc
locale loc = fixes P :: "'a => bool" assumes Pex: "EX x. P x" begin
lemma Pob: obtains x where "P x" using Pex ..
end
and some lemma in which I wish to interpret loc locally:
lemma "True"
proof -
{ fix b :: nat
have "0 < b" sorry }
interpret loc["%n :: nat. n < b"] sorry
thm Pob

`What I want, is to interpret loc not only for a fixed variable b, but
``for all b, i.e. in the interpreted theorem Pob, I want b to be free such
``that I can instantiatite it to whatever suits me later without having to
``interpret loc for every different case again.
`
How can this be done?
Regards and thanks in advance,
Andreas

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