*To*: scott constable <sdconsta at syr.edu>, "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Local Theory Parameterized by Types Only?*From*: Peter Lammich <lammich at in.tum.de>*Date*: Mon, 14 Nov 2016 21:46:50 +0100*References*: <CADYF24fpmk3HkCE-70abs43KPjzPrKCzBHKZnfYvzs+A8SMw3A@mail.gmail.com>

Hi,

A locale fixes all polymorphic types of its parameters. If you have a type variable not in the type of a fixed term variable, you can fix a variable of type itself: fixes t :: 'a itself

Peter

-------- Originalnachricht --------

Betreff: [isabelle] Local Theory Parameterized by Types Only?

Von: scott constable

An: isabelle-users at cl.cam.ac.uk

Cc:

Hi All,

I'm writing a portable implementation of access control logic (ACL) for

Isabelle, Coq, and HOL4. In broad terms, ACL describes relationships

between principals (e.g. people, organizations, devices, etc.) and commands

which principals can execute. For example, the ACL statement

Alice says

indicates that Alice is executing the command "Fetch." The logic itself is

implemented in terms of inference rules. Ideally, such a theory would be

parameterized on two types: the type of principals and the type of

commands. For example, one interpretation of ACL could represent each

principal as a natural number, another interpretation could make principals

explicit:

datatype MyPrincipal = Alice | Bob

In Coq, I can do this with a module parameterized by some "Principal" and

"Command" each in the universe of types, e.g.

Module Type ACL.

Parameters Principal Command : Type.

...

End ACL.

What is the best practice for doing this in Isabelle?

Thanks in advance,

Scott Constable

**References**:**[isabelle] Local Theory Parameterized by Types Only?***From:*scott constable

- Previous by Date: [isabelle] Local Theory Parameterized by Types Only?
- Next by Date: Re: [isabelle] Local Theory Parameterized by Types Only?
- Previous by Thread: [isabelle] Local Theory Parameterized by Types Only?
- Next by Thread: Re: [isabelle] Local Theory Parameterized by Types Only?
- Cl-isabelle-users November 2016 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