# Re: [isabelle] type_synonym and fixed type arguments in a locale?

Dear all,

`sorry, no answer. Just a related question (I think). For those who
``prefer stackoverflow, it can also be found here:
`
http://stackoverflow.com/q/16556633/476803
In NEWS I found
* Command 'typedef' now works within a local theory context -- without
introducing dependencies on parameters or assumptions, which is not
possible in Isabelle/Pure/HOL. Note that the logical environment may
contain multiple interpretations of local typedefs (with different
non-emptiness proofs), even in a global theory context.

`(which dates back to Isabelle2009-2). Is this the latest news with
``respect to typedef and local theory contexts? Further, what does the
``restriction "without introducing dependencies on parameters or
``assumptions" actually mean?
`

`If it would mean that I cannot use locale parameters in the defining set
``of a typedef, then I would not consider 'typedef' to be localized at all
``(since the only allowed instances can easily be moved outside the local
``context, or am I missing something?).
`

`Related to Randy's question: is it (or should it, or will it ever be)
``possible to do the following?
`
locale term_algebra =
fixes F :: "'a set"
fixes V :: "'b set"
begin
definition "domain α = {x ∈ V. α x ≠ Var x}"
typedef ('a, 'b) subst =
"{α :: 'b => ('a, 'b) term. finite (domain α)}"
end
for which I currently obtain:
Locally fixed type arguments "'a", "'b" in type declaration "subst"
which sounds similar to what Randy is experiencing.
cheers
chris
On 05/15/2013 06:48 AM, Randy Pollack wrote:

Hi,
Consider the cut-down locale definition:
locale step =
label:lattice where sup = lblsup
for lblsup::"'a => 'a => 'a"
In the context of this locale want a type synonym:
type_synonym 'a atm = "int * 'a"
This is rejected:
*** Locally fixed type arguments "'a" in type declaration "atm"
OK, but the following is also rejected:
type_synonym atm = "int * 'a"
*** Extra variables on rhs: "'a"
Is it possible to make such a type synonym in a locale?
Thanks,
Randy

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