Email Gateway (Aug 22 2022 at 20:10): Email Gateway (Aug 22 2022 at 20:10):From: Walter Guttmann <walter.guttmann@canterbury.ac.nz>
Dear Isabelle users,
some abbreviations introduced in locales do not appear when terms or theorems using them are printed in the same context or in a class which is a sublocale. Is there an explanation for this behaviour?
In the following example, I would have expected "ab" in the output for the term and lemma commands in the locale and "s.ab" in the first two outputs for s.ab and s.lem in the class (print_abbrevs contains s.ab after the sublocale command). As expected, "cd" appears in the last two outputs for s.ab and s.lem, though I am not sure why it works now. The behaviour is similar if {True} is replaced with True (or with more complex expressions involving locale parameters, from which this example is abstracted).
theory A
imports Main
begin
locale l begin
abbreviation "ab ≡ {True}"
term ab (* output: "{True}" :: "bool set" *)
lemma lem: "ab = ab" .. (* output: theorem {True} = {True} *)
end
class c begin
sublocale s: l .
term s.ab (* output: "{True}" :: "bool set" *)
thm s.lem (* output: {True} = {True} *)
abbreviation "cd ≡ {True}"
term s.ab (* output: "cd" :: "bool set" *)
thm s.lem (* output: cd = cd *)
end
end
Any insights or workarounds to get ab/s.ab to print would be appreciated.
Cheers,
Walter
Last updated: Nov 21 2024 at 12:39 UTC