[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.