# [isabelle] Parametric theories

• To: <isabelle-users at cl.cam.ac.uk>
• Subject: [isabelle] Parametric theories
• From: Daniel Schoepe <daniel at schoepe.org>
• Date: Wed, 11 Apr 2012 21:01:17 +0200
• User-agent: Notmuch/0.12+112~gcb5e016 (http://notmuchmail.org) Emacs/24.1.50.1 (x86_64-pc-linux-gnu)

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.