Re: [isabelle] programming with locales



Dear Michael,

----------------------------------------------------------------------
locale globals =
  fixes
    x_address :: nat
  assumes
    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
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






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