[isabelle] Local Theory Parameterized by Types Only?



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 <Fetch>

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



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