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

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"

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


On Mon, Nov 14, 2016 at 3:46 PM, Peter Lammich <lammich at> 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
> 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

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