[opentheory-users] Theorem meta-data

[Joe Leslie-Hurd]

I've been doing some thinking about theorem names, which is a
requested feature of articles and up to now I've been resisting,
preferring to keep articles clean of meta-data and unnecessary names.

However, in applications such as exporting theory packages as Haskell
I can see value in assigning meta-data to theorems, and so I'd like to
define a general scheme for it. Here are some constraints:

1. It should be semantically transparent, having no effect at all on
logical dependencies between theories.

2. It should be maintained by tools processing articles (when
possible). Note that pragmas are discarded by the opentheory tool, so
fail this test for encoding meta-data.

3. It should be a standard scheme, not reader-dependent, so pragmas
also fail for this reason.

4. At the theory level merging articles is a common operation, so
there should be a standard way to merge meta-data having the
idempotence property that (merge D D = D).

I propose the thm article command take an additional metadata
argument, where metadata is represented by the following datatype in
ML syntax:

datatype metadata = Metadata of (name, metadata) finite_map;

This can be easily represented using article lists, so for example the metadata

name: head_def
HOLLight:
  name: HD
  simplifier

would be represented as

[["name",[["head_def",[]]]],
 ["HOLLight",[["name",[["HD",[]]],["simplifier",[]]]]]

Merging two pieces of metadata would simply be the union of two finite
maps, where if they map the same name then the inner finite maps are
merged recursively. This has the desired idempotence property.

There's still time to add this to version 6 of the article standard,
if it was deemed a good idea. Any comments?

Cheers,

Joe