[isabelle] instantiating typedecls with datatypes?

Hi all,

I'm currently playing with David von Oheimb's Noninterference package
(see http://david.von-oheimb.de/cs/HOL/NI/, all the files are attached)

This package defines some types and functions, and states which
properties these must fulfill in order for the system to be secure.

It looks like this (see System.thy):
  typedecl "state"
  typedecl "action"
  typedecl "domain"
  consts   step :: "action =>  state => state"
  (* many more functions... *)

Now I want to develop a small theory and prove it secure. (see Test.thy)

To do this, I have to instantiate the functions and types.
For functions, this is no problem (I just use primrec), but for types
(where I need something like 'datatype "domain" = H | L' ) I found no
sane solution.

I'd like to do something like:
  datatype "domain2" = H | L
  domaintype: "domain == domain2"
and make domain and domain2 identical, but I found no way to do this.
(And I'm not sure if it's possible without introducing inconsistencies).

I know that I could use axioms to describe the type I want, but this is
awfully hard compared to datatypes.
For now I resorted to modifying 'System.thy' directly, but I don't think
that's a good solution in the long term.

Is what I want possible with Isabelle?
How should I change the theory to make it easy to instantiate it without
modifying the parent theory?

Thanks in advance,

PS: PVS has this neat feature where you can say "theory 'a List begin
... end" and later instantiate the theory with a concrete type ("import
nat List", not sure about the exact syntax). I'm hoping that Isabelle
has something similar.

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