Email Gateway (Aug 18 2022 at 12:38): Email Gateway (Aug 18 2022 at 12:38):From: Andreas Lochbihler <lochbihl@ipd.info.uni-karlsruhe.de>
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
Last updated: May 03 2024 at 04:19 UTC