Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] defining a constant with a long-identifier name

view this post on Zulip Email Gateway (Aug 18 2022 at 10:10):

From: Michael Norrish <michael.norrish@nicta.com.au>
I want to (programmatically) define constants that live within
different sub-spaces of the same theory, and so might have the same
name. I know this is possible, because it is what the record package
achieves if you write

theory foo
imports Main

begin

record rec1 =
fld1 :: nat
fld2 :: bool

record rec2 =
fld1 :: bool

end;

There are two "fld1" constants after this is executed: foo.rec1.fld1
and foo.rec2.fld1.

However, the function Theory.add_consts_i takes a "bstring", and does
not allow the declaration of qualified names.

So, how does the record package do it? (And, just in case the answers
are not the same, how should I do it myself?)

Michael.

view this post on Zulip Email Gateway (Aug 18 2022 at 10:10):

From: Makarius <makarius@sketis.net>
A quick search through record_package.ML reveals something like this:

...
|> Theory.add_path bname
|> Theory.add_consts_i ...
|> Theory.parent_path

See also section 2.2.4 of the Isabelle/Isar implementation manual.

Makarius

Last updated: May 03 2024 at 04:19 UTC