[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/18.104.22.168 (x86_64-pc-linux-gnu)
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
), 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"
type_synonym bar = "'a \times 'a"
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 , 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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and