Re: [isabelle] programming with locales

Dear Michael,

locale globals =
    x_address :: nat
    x_nzero:    "x_address ~= 0" and
    x_aligned:  "4 dvd x_address"

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
  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!


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.