Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Assumptions of auxiliary context in other cont...

Email Gateway (Aug 18 2022 at 20:21):

From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi all,

I want to nest an auxiliary context inside another local context to factor out a
bunch of assumptions. The assumptions should refer to fixed parameters of the
surrounding context, like in the following example:

locale l = fixes n :: nat begin
context assumes n: "n ~= 0" begin
lemma L: True ..
end
thm L
end

Unfortunately, thm L refers to "(!!n. n ~= 0) ==> True" instead of "n ~= 0 ==>
True", i.e., the assumption n generalises over n instead of taking it as a fixed
parameter. Consequently, L's assumption is unprovable and therefore L unusable.

How can I refer to the fixed parameter n of the surrounding context in the
assumption n?

I tried the following:

locale l = fixes n :: nat begin
definition n' where "n' = n"
context assumes n: "n' ~= 0" begin
lemma L: "True" ..
end
thm L
end

But thm L still contains the unprovable assumption: "(!!n. L.n' n = 0) ==> True"

By the way: The Isar/Ref manual mentions that unnamed contexts may be nested
within other targets and mentions locales, type classes etc. as examples. May I
also nest unnamed contexts inside unnamed contexts? Isabelle2012 does not
complain, if I do so, but is this officially supported?

Andreas

Last updated: Apr 26 2024 at 08:19 UTC