*To*: Peter Lammich <lammich at in.tum.de>*Subject*: Re: [isabelle] Local Theory Parameterized by Types Only?*From*: scott constable <sdconsta at syr.edu>*Date*: Mon, 14 Nov 2016 16:09:39 -0500*Cc*: "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <201611142048.uAEKm0gE022275@mx2.syr.edu>*References*: <CADYF24fpmk3HkCE-70abs43KPjzPrKCzBHKZnfYvzs+A8SMw3A@mail.gmail.com> <201611142048.uAEKm0gE022275@mx2.syr.edu>

Hi Peter, First of all, thank you for your speedy response. I was able to use "itself" to fix a type variable, but now I'm not sure how to actually use it. For example, I now have: locale ACL = fixes principal :: "'a itself" and command :: "'b itself" begin datatype "princ" = -- {* Principal Expressions *} p_PrincName "'a" -- {* Principal Name *} | p_ConjWith "princ" "princ" -- {* Conjunction With *} | p_Quoting "princ" "princ" -- {* Quoting *} but now Isabelle reports an error: "Extra type variables on right-hand side "'a"". Scott On Mon, Nov 14, 2016 at 3:46 PM, Peter Lammich <lammich at in.tum.de> wrote: > 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 > >

**Follow-Ups**:**Re: [isabelle] Local Theory Parameterized by Types Only?***From:*Lars Hupel

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

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