Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] suppressing abbreviations from sublocales

Email Gateway (Aug 22 2022 at 16:29):

From: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Is it possible to suppress (some) of the abbreviations introduced
by a sublocale command? I have a scenario similar to the following
artificial example:

theory Scratch
imports Main
begin

(* We have a locale with two parameters. *)

locale A = fixes S :: "'a set" and n :: nat
assumes card_S: "card S ≤ n"

(* The locale defines a constant that only depends on one of the parameters. *)

definition (in A) T where "T = S × S"

locale B = A
(* + ... *)
begin

(* A = A S n is a sublocale of B (by declaration), but we can also

• show that A S "Suc n" is a sublocale, essentially for free; the
• point is that the first parameter stays the same but the second one
• changes. *)

sublocale sucA: A S "Suc n"
using card_S by unfold_locales simp_all

(* The sublocale command introduces an abbreviation

• sucA.T = A.T S, shadowing the existing abbreviation T = A.T S,
• so *)

term T

(* is printed as "sucA.T". Can this abbreviation somehow be suppressed?

• We can use a notation as a workaround, of course, as follows. *)

notation (output) sucA.T ("T")

term T

(* now prints "T" again (though in a different color than desired.) *)

end

Cheers,

Bertram

Last updated: Apr 26 2024 at 04:17 UTC