*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] instantiating typedecls with datatypes?*From*: Thomas Bleher <bleher at informatik.uni-muenchen.de>*Date*: Mon, 6 Nov 2006 13:01:53 +0100*User-agent*: Mutt/1.5.6+20040907i

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 axioms 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, Thomas 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.

**Follow-Ups**:**Re: [isabelle] instantiating typedecls with datatypes?***From:*Thomas Bleher

**Re: [isabelle] instantiating typedecls with datatypes?***From:*Tobias Nipkow

**Re: [isabelle] instantiating typedecls with datatypes?***From:*Makarius

**Re: [isabelle] instantiating typedecls with datatypes?***From:*John Matthews

- Previous by Date: Re: [isabelle] Library load path
- Next by Date: Re: [isabelle] instantiating typedecls with datatypes?
- Previous by Thread: Re: [isabelle] adding "simp" attribute to programmatically created definitions
- Next by Thread: Re: [isabelle] instantiating typedecls with datatypes?
- Cl-isabelle-users November 2006 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list