[isabelle] Parametric theories



Hi,

I'm trying to build a theory that is parametric in some types and
would like to know the recommended way for doing that. I realize that
this topic has come up before and that this problem is partially(?)
solved by locales. From what I have read on this list (for example in
[1]), my choices are the following:

1. Use type variables everywhere -- this will get very tiresome very
quickly. Locales don't seem to offer a complete way around that either,
at least the following does not seem to work:

locale Foo = fixes x :: "'a"
begin
  type_synonym bar = "'a \times 'a"
end

2. Use typedecl, consts, and similar commands. This seems ideal apart
from instantiating the theory later. Here I think I have two choices:
Use the AWE tool [2], which seems to do exactly what I want, but was
last updated for Isabelle 2009-1, or a post-hoc axiomatization using
directives like type_definition and axioms.

Am I overlooking some possibility, or is that basically it? If so, is
there an up-to-date version of AWE, or does someone know how much work
it would take to update it (I noticed that at least the isar-keywords.el
files of 2011-1 and AWE have diverged, but there are probably more
complicated conflicts than that).

Is there some "convention" on how deal with this issue, as I can imagine
this comes up quite often?

Regards,
Daniel

[1] https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2009-July/msg00111.html
[2] http://www.informatik.uni-bremen.de/~cxl/awe/





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