Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] abbreviations in locales are not used for prin...


view this post on Zulip 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: Mar 28 2024 at 08:18 UTC