Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Immediate target breaks unnamed context

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

From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
According to the Isar-Ref manual (p. 79), immediate target specifications should
suspend the current context only for the given command. However, Isabelle
apparently fails to restore the current (unnamed) context.

In the following example, I would expect that assumption P in the following
example is still available after lemma L, but Isabelle complains that P was
unknown. Similar, fixed parameters get lost. Is this a bug or unintended usage
of unnamed contexts? Note that I still need to use "end" to close the unnamed
context.

locale l = fixes n :: nat

consts P :: bool
context fixes n :: nat assumes P: "P" begin

lemma (in l) L: "True" ..

lemma P': "P" by(rule P) (* Unknown fact P *)
term n (* has type 'a *)
end

Andreas

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

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
According to my understanding of loc_begin in src/Pure/Isar/toplevel.ML,
this is the implemented behaviour. But I doubt it's intended to work
this way.

Florian
signature.asc

Last updated: Apr 23 2024 at 20:15 UTC