Email Gateway (Aug 18 2022 at 09:53): Email Gateway (Aug 18 2022 at 09:53):From: Thomas Bleher <bleher@informatik.uni-muenchen.de>
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.
Email Gateway (Aug 18 2022 at 09:53):From: Thomas Bleher <bleher@informatik.uni-muenchen.de>
Thomas
Test.thy
System.thy
Generics.thy
Noninterference.thy
Nonleakage.thy
Noninfluence.thy
Email Gateway (Aug 18 2022 at 09:53):From: Tobias Nipkow <nipkow@in.tum.de>
You cannot instantiate later on types that were only declared. You will
have to modify the generic theory. A relatively simple change is to make
the theory polymorphic in all those types: Remove the typedecls and
replace occurrences of those types by type variables, eg
consts step :: "'action => 'state => 'state"
Datatypes may need to become parameterized, eg
datatype 'action foo = Bar 'action | ...
In a nutshell: generic theories need to be written with genericity in
mind and should be updated if they were not written in that way.
Tobias
Thomas Bleher schrieb:
Email Gateway (Aug 18 2022 at 09:53):From: Makarius <makarius@sketis.net>
On Mon, 6 Nov 2006, Thomas Bleher wrote:
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)
typedecl "state"
typedecl "action"
typedecl "domain"
To do this, I have to instantiate the functions and types.
This technique seems to come from David's Bali theories, e.g. see
http://isabelle.in.tum.de/dist/library/HOL/Bali/Example.html how the
previously declared types tnam, vname etc. are instantiated
(axiomatically!).
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?
The Isabelle framework is able to support specifications depending on
simple type parameters (not general constructors), arbitrary term
parameters, and arbitrary proof parameters (assumptions). The locale
package provides some user-level infrastructure on top of this. There is
ongoing work to turn this into full-blown structured specification
paradigm, where definitions and theorems can depend on type/term/proof
parameters and can be instantiated later on.
Since the HOL/NI material is for Isabelle2004 only, this won't help you
right now, of course. Nevertheless, it would be an interesting case-study
to adapt these theories to our forthcoming structuring concepts, but the
non-free license seems to prevent this, i.e. David has to get involved
directly.
Makarius
Email Gateway (Aug 18 2022 at 09:54):From: Tobias Nipkow <nipkow@in.tum.de>
Since David specifically says that "any non-commercial use is granted",
Thomas is free to use and modify the theories in his research.
Tobias
Email Gateway (Aug 18 2022 at 09:54):From: Makarius <makarius@sketis.net>
The key question is what happens with the modifications.
Makarius
Email Gateway (Aug 18 2022 at 09:54):From: Makarius <makarius@sketis.net>
On Tue, 7 Nov 2006, Thomas Bleher wrote:
Are the "structuring concepts" you're referring to already available in
CVS?
We are still working on it.
I'm already adapting all the theories to work with the latest Isabelle,
so I could look into this as well.
I would recommend using Isabelle2005 at the moment, unless you want to try
catching up with huge amounts of transient changes every few days which
are mostly reflected in the ChangeLog only.
Makarius
Email Gateway (Aug 18 2022 at 09:54):From: John Matthews <matthews@galois.com>
Hi Thomas,
You might also want to consider the AWE extensions pack for Isabelle
2005:
Among other things, it safely provides theory morphisms, so that you
can instantiate constant and type parameters in theories, like the
ones you want. It also allows you to instantiate the *type
constructor* parameters of a theory, which are not supported by
Isabelle's locale mechanism. Type constructor parameters are needed,
for example, to support reusable theories of monads.
You can download the software itself at:
http://www.tzi.de/~cxl/awe/software.html
(Note that I'm not involved with the AWE project, I just like the way
it supports theory morphisms in Isabelle.)
Cheers,
-john
Email Gateway (Aug 18 2022 at 09:54):From: Thomas Bleher <bleher@informatik.uni-muenchen.de>
Are the "structuring concepts" you're referring to already available
in CVS? I'm already adapting all the theories to work with the latest
Isabelle, so I could look into this as well.
Thanks for all your pointers, they really helped me!
Thomas
Last updated: May 03 2024 at 12:27 UTC