Email Gateway (Aug 17 2022 at 14:15): Email Gateway (Aug 17 2022 at 14:15):From: Michael Norrish <Michael.Norrish@nicta.com.au>
Hello all,
I would like to emulate the following locale definition
locale globals =
fixes
x_address :: nat
assumes
x_nzero: "x_address ~= 0" and
x_aligned: "4 dvd x_address"
at the ML level, and then go onto make some definitions within the
locale (i.e., the sort of thing you would write with defines clauses),
but for which I already have ML code using add_consts_defs_i.
What should my ML code look like?
Many thanks,
Michael.
Email Gateway (Aug 17 2022 at 14:15):From: Clemens Ballarin <ballarin@in.tum.de>
Dear Michael,
The function to use is Locale.add_locale(_i):
add_locale do_pred name import elems thy
adds a locale declaration to thy. Do_pred indicates whether predicates
should be defined; this is the default behaviour in theory files, so
do_pred = true
and
name = "globals".
The imported expression is empty,
import = Locale.empty.
The type of elements is declared in Pure/Isar/element.ML. You need
Fixes [("x_address", "nat", NoSyn)],
Assumes [(("x_nzero", []), [("x_address ~= 0", ([], []))]),
(("x_aligned", []), [("4 dvd x_address", ([], [])))])]
Hope this is all type-correct! The _i variant, as usual, certifies
terms rather then readiing strings, so that's probably the version you
want to use.
Add_locale returns (besides of the theory) a context. This is only
used for printing locales in document preparation and should be
discarded. Most recent development versions also return the internal
name of the locale (which is qualified by the theory name).
Note that defines elements are part of the specification. They cannot
be added later.
Hope this gets you started!
Clemens
Last updated: May 03 2024 at 01:09 UTC